Boogie: added features to help with modular verification. In particular, define FILE_n when parsing file n on the command line, and support :extern and :ignore attributes on top-level declarations.

4 files changed, 89 insertions, 100 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 3929e237..dcc007fe 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -261,7 +261,8 @@ namespace Microsoft.Boogie {
       //BoogiePL.Errors.count = 0;

       Program program = null;

       bool okay = true;

-      foreach (string bplFileName in fileNames) {

+      for (int fileId = 0; fileId < fileNames.Count; fileId++) {

+        string bplFileName = fileNames[fileId];

         if (!suppressTraceOutput) {

           if (CommandLineOptions.Clo.XmlSink != null) {

             CommandLineOptions.Clo.XmlSink.WriteFileFragment(bplFileName);

@@ -274,7 +275,8 @@ namespace Microsoft.Boogie {
         Program programSnippet;

         int errorCount;

         try {

-          errorCount = BoogiePL.Parser.Parse(bplFileName, null, out programSnippet);

+          var defines = new List<string>() { "FILE_" + fileId };

+          errorCount = BoogiePL.Parser.Parse(bplFileName, defines, out programSnippet);

           if (programSnippet == null || errorCount != 0) {

             Console.WriteLine("{0} parse errors detected in {1}", errorCount, bplFileName);

             okay = false;

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index cde8fc3f..67500c88 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -235,30 +235,26 @@ namespace Microsoft.Boogie {
 

       ResolveTypes(rc);

 

-      List<Declaration/*!*/> prunedTopLevelDecls = CommandLineOptions.Clo.OverlookBoogieTypeErrors ? new List<Declaration/*!*/>() : null;

-

+      var prunedTopLevelDecls = new List<Declaration/*!*/>();

       foreach (Declaration d in TopLevelDeclarations) {

+        if (QKeyValue.FindBoolAttribute(d.Attributes, "ignore")) {

+          continue;

+        }

         // resolve all the non-type-declarations

         if (d is TypeCtorDecl || d is TypeSynonymDecl) {

-          if (prunedTopLevelDecls != null)

-            prunedTopLevelDecls.Add(d);

         } else {

           int e = rc.ErrorCount;

           d.Resolve(rc);

-          if (prunedTopLevelDecls != null) {

-            if (rc.ErrorCount != e && d is Implementation) {

-              // ignore this implementation

-              System.Console.WriteLine("Warning: Ignoring implementation {0} because of translation resolution errors", ((Implementation)d).Name);

-              rc.ErrorCount = e;

-            } else {

-              prunedTopLevelDecls.Add(d);

-            }

+          if (CommandLineOptions.Clo.OverlookBoogieTypeErrors && rc.ErrorCount != e && d is Implementation) {

+            // ignore this implementation

+            System.Console.WriteLine("Warning: Ignoring implementation {0} because of translation resolution errors", ((Implementation)d).Name);

+            rc.ErrorCount = e;

+            continue;

           }

         }

+        prunedTopLevelDecls.Add(d);

       }

-      if (prunedTopLevelDecls != null) {

-        TopLevelDeclarations = prunedTopLevelDecls;

-      }

+      TopLevelDeclarations = prunedTopLevelDecls;

 

       foreach (Declaration d in TopLevelDeclarations) {

         Variable v = d as Variable;

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 5094fb9e..84ecce6d 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -1875,6 +1875,21 @@ namespace Microsoft.Boogie {
       Console.WriteLine(

 @"Boogie: The following attributes are supported by this implementation.

 

+  ---- On top-level declarations ---------------------------------------------

+

+    {:ignore}

+      Ignore the declaration (after checking for duplicate names).

+      See also below for more options when :ignore is used with axioms.

+

+    {:extern}

+      If two top-level declarations introduce the same name (for example, two

+      constants with the same name or two procedures with the same name), then

+      Boogie usually produces an error message.  However, if at least one of

+      the declarations is declared with :extern, one of the declarations is

+      ignored.  If both declarations are :extern, Boogie arbitrarily chooses

+      one of them to keep; otherwise, Boogie ignore the :extern declaration

+      and keeps the other.

+

   ---- On axioms -------------------------------------------------------------

 

     {:inline true}

diff --git a/Source/Core/ResolutionContext.cs b/Source/Core/ResolutionContext.cs
index d4b353ef..803b1f8b 100644
--- a/Source/Core/ResolutionContext.cs
+++ b/Source/Core/ResolutionContext.cs
@@ -170,15 +170,22 @@ namespace Microsoft.Boogie {
     public void AddType(NamedDeclaration td) {

       Contract.Requires(td != null);

       Contract.Assert((td is TypeCtorDecl) || (td is TypeSynonymDecl));

+      Contract.Requires(td.Name != null);

 

-      string name = cce.NonNull(td.Name);

+      string name = td.Name;

       if (CheckBvNameClashes(td, name))

         return;  // error has already been reported

 

-      if (types[name] != null) {

-        Error(td, "more than one declaration of type name: {0}", name);

-      } else {

+      var previous = (NamedDeclaration)types[name];

+      if (previous == null) {

         types.Add(name, td);

+      } else {

+        var r = (NamedDeclaration)SelectNonExtern(td, previous);

+        if (r == null) {

+          Error(td, "more than one declaration of type name: {0}", name);

+        } else {

+          types[name] = r;

+        }

       }

     }

 

@@ -247,79 +254,6 @@ namespace Microsoft.Boogie {
       return null;  // not present

     }

 

-    // ------------------------------  Types  ------------------------------

-

-    // user-defined types

-    //      Hashtable /*string->TypeDecl*/! types = new Hashtable /*string->TypeDecl*/ ();

-    /*

-            public void AddType(TypeDecl td){

-    Contract.Requires(td != null);

-                string! name = (!)td.Name;

-

-                if (name.StartsWith("bv") && name.Length > 2) {

-                    bool isBv = true;

-                    for (int i = 2; i < name.Length; ++i)

-                        if (!char.IsDigit(name[i])) isBv = false;

-                    if (isBv)

-                        Error(td, "type name: {0} is registered for bitvectors", name);

-                }

-

-                if (types[name] != null) 

-                {

-                    Error(td, "more than one declaration of type name: {0}", name);

-                } 

-                else 

-                {

-                    types.Add(name, td);

-                }

-            }

-    */

-    /// <summary>

-    /// Returns the declaration of the named type, or null if

-    /// no such type is declared.

-    /// </summary>

-    /// <param name="name"></param>

-    /// <returns></returns>

-    /*    public TypeDecl LookUpType(string name){

-Contract.Requires(name != null);

-            return (TypeDecl)types[name];

-        }

-      */

-    // ------------------------------  Type Binders  ------------------------------

-    /*

-            List<TypeBinderDecl!>! typeBinders = new List<TypeBinderDecl!>(5);

-        

-            public void AddTypeBinder(TypeBinderDecl td){

-    Contract.Requires(td != null);

-              for (int i = 0; i < typeBinders.Count; i++) {

-                if (typeBinders[i].Name == td.Name) {

-                  Error(td, "more than one declaration of type binder name: {0}", td.Name);

-                  return;

-                }

-              }

-              typeBinders.Add(td);

-            }

-        

-            public int TypeBinderState {

-              get { return typeBinders.Count; }

-              set { typeBinders.RemoveRange(value, typeBinders.Count - value); }

-            }

-        

-            /// <summary>

-            /// Returns the declaration of the named type binder, or null if

-            /// no such binder is declared.

-            /// </summary>

-            public TypeDecl LookUpTypeBinder(string name){

-    Contract.Requires(name != null);

-              for (int i = typeBinders.Count; 0 <= --i; ) {

-                TypeBinderDecl td = typeBinders[i];

-                if (td.Name == name) {

-                  return td;

-                }

-              }

-              return null;  // not present

-            }

-      */

     // ------------------------------  Variables  ------------------------------

 

     class VarContextNode {

@@ -365,10 +299,16 @@ Contract.Requires(name != null);
 

     public void AddVariable(Variable var, bool global) {

       Contract.Requires(var != null);

-      if (FindVariable(cce.NonNull(var.Name), !global) != null) {

-        Error(var, "more than one declaration of variable name: {0}", var.Name);

-      } else {

+      var previous = FindVariable(cce.NonNull(var.Name), !global);

+      if (previous == null) {

         varContext.VarSymbols.Add(var.Name, var);

+      } else {

+        var r = (Variable)SelectNonExtern(var, previous);

+        if (r == null) {

+          Error(var, "more than one declaration of variable name: {0}", var.Name);

+        } else {

+          varContext.VarSymbols[var.Name] = r;

+        }

       }

     }

 

@@ -417,11 +357,47 @@ Contract.Requires(name != null);
 

     public void AddProcedure(DeclWithFormals proc) {

       Contract.Requires(proc != null);

-      if (funcdures[cce.NonNull(proc.Name)] != null) {

-        Error(proc, "more than one declaration of function/procedure name: {0}", proc.Name);

+      Contract.Requires(proc.Name != null);

+

+      string name = proc.Name;

+      var previous = (DeclWithFormals)funcdures[name];

+      if (previous == null) {

+        funcdures.Add(name, proc);

+      } else {

+        var r = (DeclWithFormals)SelectNonExtern(proc, previous);

+        if (r == null) {

+          Error(proc, "more than one declaration of function/procedure name: {0}", name);

+        } else {

+          funcdures[name] = r;

+        }

+      }

+    }

+

+    /// <summary>

+    /// If both "a" and "b" have an ":extern" attribute, returns either one.

+    /// If one of "a" and "b" has an ":extern" attribute, returns that one.

+    /// If neither of "a" and "b" has an ":extern" attribute, returns null.

+    /// If a non-value value is returned, this method also adds the ":ignore"

+    /// attribute to the declaration NOT returned.

+    /// </summary>

+    Declaration SelectNonExtern(Declaration a, Declaration b) {

+      Contract.Requires(a != null);

+      Contract.Requires(b != null);

+      Contract.Ensures(Contract.Result<Declaration>() == null || Contract.Result<Declaration>() == a || Contract.Result<Declaration>() == b);

+

+      Declaration ignore, keep;

+      if (QKeyValue.FindBoolAttribute(a.Attributes, "extern")) {

+        ignore = a;

+        keep = b;

+      } else if (QKeyValue.FindBoolAttribute(b.Attributes, "extern")) {

+        ignore = b;

+        keep = a;

       } else {

-        funcdures.Add(proc.Name, proc);

+        return null;

       }

+      // prepend :ignore attribute

+      ignore.Attributes = new QKeyValue(ignore.tok, "ignore", new List<object/*!*/>(), ignore.Attributes);

+      return keep;

     }

 

     /// <summary>