added owicki-gries and linear-set to boogiedriver

cleaned up the async type checking

4 files changed, 52 insertions, 40 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index a626de7f..133dc33f 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -186,6 +186,11 @@ namespace Microsoft.Boogie {
           }

         }

 

+        OwickiGriesTransform ogTransform = new OwickiGriesTransform(program);

+        ogTransform.Transform();

+        LinearSetTransform linearTransform = new LinearSetTransform(program);

+        linearTransform.Transform();

+

         EliminateDeadVariablesAndInline(program);

 

         int errorCount, verified, inconclusives, timeOuts, outOfMemories;

@@ -201,7 +206,6 @@ namespace Microsoft.Boogie {
       }

     }

 

-

     static void PrintBplFile(string filename, Program program, bool allowPrintDesugaring) {

       Contract.Requires(program != null);

       Contract.Requires(filename != null);

@@ -376,6 +380,14 @@ namespace Microsoft.Boogie {
         return PipelineOutcome.TypeCheckingError;

       }

 

+      LinearTypechecker linearTypechecker = new LinearTypechecker();

+      linearTypechecker.VisitProgram(program);

+      if (linearTypechecker.errorCount > 0)

+      {

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

+          return PipelineOutcome.TypeCheckingError;

+      }

+

       if (CommandLineOptions.Clo.PrintFile != null && CommandLineOptions.Clo.PrintDesugarings) {

         // if PrintDesugaring option is engaged, print the file here, after resolution and type checking

         PrintBplFile(CommandLineOptions.Clo.PrintFile, program, true);

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index b1c213fa..1220d812 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -1834,8 +1834,8 @@ namespace Microsoft.Boogie {
         return;

       }

       if (QKeyValue.FindBoolAttribute(this.Attributes, "async")) {

-        if (Proc.OutParams.Length > 1) {

-          rc.Error(this.tok, "a procedure called asynchronously can have at most one output parameter");

+        if (Proc.OutParams.Length > 0) {

+          rc.Error(this.tok, "a procedure called asynchronously can have no output parameters");

           return;

         }

       }

@@ -1916,17 +1916,6 @@ namespace Microsoft.Boogie {
         }

       }

 

-      if (QKeyValue.FindBoolAttribute(this.Attributes, "async") && Outs.Count > 0) {

-        Type returnType = null;

-        if (Outs[0] == null && Proc.OutParams.Length > 0) returnType = Proc.OutParams[0].TypedIdent.Type;

-        else returnType = Outs[0].ShallowType;

-        //Type returnType = cce.NonNull(Outs[0]).ShallowType;

-        if (!returnType.Equals(Type.Int) && !returnType.Equals(Type.GetBvType(32))) {

-          tc.Error(this.tok, "the return from an asynchronous call should be either int or bv32");

-          return;

-        }

-      }

-

       // match actuals with formals

       List<Type/*!*/>/*!*/ actualTypeParams;

       Type.CheckArgumentTypes(Proc.TypeParameters,

diff --git a/Source/Core/LinearSets.cs b/Source/Core/LinearSets.cs
index 94d3c734..6ccbcee0 100644
--- a/Source/Core/LinearSets.cs
+++ b/Source/Core/LinearSets.cs
@@ -7,12 +7,19 @@ using Microsoft.Boogie;
 

 namespace Microsoft.Boogie

 {

-    class LinearTypechecker : StandardVisitor

+    public class LinearTypechecker : StandardVisitor

     {

+        public int errorCount;

         CheckingContext checkingContext;

         public LinearTypechecker()

         {

-            checkingContext = new CheckingContext(null);

+            this.errorCount = 0;

+            this.checkingContext = new CheckingContext(null);

+        }

+        private void Error(Absy node, string message)

+        {

+            checkingContext.Error(node, message);

+            errorCount++;

         }

 

         public override Cmd VisitAssignCmd(AssignCmd node)

@@ -26,13 +33,13 @@ namespace Microsoft.Boogie
                 SimpleAssignLhs salhs = lhs as SimpleAssignLhs;

                 if (salhs == null)

                 {

-                    checkingContext.Error(node, "Only simple assignment allowed on linear sets");

+                    Error(node, "Only simple assignment allowed on linear sets");

                     continue;

                 }

                 IdentifierExpr rhs = node.Rhss[i] as IdentifierExpr;

                 if (rhs == null)

                 {

-                    checkingContext.Error(node, "Only variable can be assigned to a linear set");

+                    Error(node, "Only variable can be assigned to a linear set");

                     continue;

                 }

                 string rhsDomainName = QKeyValue.FindStringAttribute(rhs.Decl.Attributes, "linear");

@@ -43,17 +50,17 @@ namespace Microsoft.Boogie
                 }

                 if (rhsDomainName == null)

                 {

-                    checkingContext.Error(node, "Only linear variable can be assigned to another linear variable");

+                    Error(node, "Only linear variable can be assigned to another linear variable");

                     continue;

                 }

                 if (domainName != rhsDomainName)

                 {

-                    checkingContext.Error(node, "Variable of one domain being assigned to a variable of another domain");

+                    Error(node, "Variable of one domain being assigned to a variable of another domain");

                     continue;

                 }

                 if (rhsVars.Contains(rhs.Decl))

                 {

-                    checkingContext.Error(node, "A linear set can occur only once in the rhs");

+                    Error(node, "A linear set can occur only once in the rhs");

                     continue;

                 }

                 rhsVars.Add(rhs.Decl);

@@ -73,7 +80,7 @@ namespace Microsoft.Boogie
                 IdentifierExpr actual = node.Ins[i] as IdentifierExpr;

                 if (actual == null)

                 {

-                    checkingContext.Error(node, "Only variable can be assigned to a linear set");

+                    Error(node, "Only variable can be assigned to a linear set");

                     continue;

                 }

                 string actualDomainName = QKeyValue.FindStringAttribute(actual.Decl.Attributes, "linear");

@@ -84,17 +91,17 @@ namespace Microsoft.Boogie
                 }

                 if (actualDomainName == null)

                 {

-                    checkingContext.Error(node, "Only a linear argument can be passed to a linear parameter");

+                    Error(node, "Only a linear argument can be passed to a linear parameter");

                     continue;

                 }

                 if (domainName != actualDomainName)

                 {

-                    checkingContext.Error(node, "The domains of formal and actual parameters must be the same");

+                    Error(node, "The domains of formal and actual parameters must be the same");

                     continue;

                 }

                 if (inVars.Contains(actual.Decl))

                 {

-                    checkingContext.Error(node, "A linear set can occur only once as an in parameter");

+                    Error(node, "A linear set can occur only once as an in parameter");

                     continue;

                 }

                 inVars.Add(actual.Decl);

@@ -109,19 +116,19 @@ namespace Microsoft.Boogie
                 string domainName = QKeyValue.FindStringAttribute(formal.Attributes, "linear");

                 if (domainName == null)

                 {

-                    checkingContext.Error(node, "Only a linear variable can be passed to a linear parameter");

+                    Error(node, "Only a linear variable can be passed to a linear parameter");

                     continue;

                 }

                 if (domainName != actualDomainName)

                 {

-                    checkingContext.Error(node, "The domains of formal and actual parameters must be the same");

+                    Error(node, "The domains of formal and actual parameters must be the same");

                 }

             }

             return base.VisitCallCmd(node);

         }

     }

 

-    class LinearSetTransform

+    public class LinearSetTransform

     {

         private Program program;

         private Dictionary<Variable, string> varToDomainName;

@@ -169,7 +176,7 @@ namespace Microsoft.Boogie
             domainNameToScope[domainName].Add(v);

         }

 

-        public void Transform(Program program)

+        public void Transform()

         {

             foreach (var decl in program.TopLevelDeclarations)

             {

@@ -232,7 +239,9 @@ namespace Microsoft.Boogie
 

                 {

                     // Loops

-                    Microsoft.Boogie.GraphUtil.Graph<Block> g = Program.GraphFromImpl(impl);

+                    impl.PruneUnreachableBlocks();

+                    impl.ComputePredecessorsForBlocks();

+                    GraphUtil.Graph<Block> g = Program.GraphFromImpl(impl);

                     g.ComputeLoops();

                     if (g.Reducible)

                     {

@@ -247,10 +256,6 @@ namespace Microsoft.Boogie
                             header.Cmds = newCmds;

                         }

                     }

-                    else

-                    {

-                        Console.WriteLine("Warning: implementation {0} is not reducible", impl.Name);

-                    }

                 }

 

                 {

diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs
index 8fa66704..29eae051 100644
--- a/Source/Core/OwickiGries.cs
+++ b/Source/Core/OwickiGries.cs
@@ -139,23 +139,29 @@ namespace Microsoft.Boogie
         }

     }

 

-    class OwickiGriesTransform

+    public class OwickiGriesTransform

     {

         Dictionary<string, ProcedureInfo> procNameToInfo;

         IdentifierExprSeq globalMods;

         Hashtable globalMap;

+        Program program;

 

         public OwickiGriesTransform(Program program)

         {

+            this.program = program;

             procNameToInfo = AsyncAndYieldTraverser.Traverse(program);

             AtomicTraverser.Traverse(program, procNameToInfo);

             globalMap = new Hashtable();

             globalMods = new IdentifierExprSeq();

-            foreach (Variable g in program.GlobalVariables())

+            bool workTodo = procNameToInfo.Values.Aggregate<ProcedureInfo, bool>(false, (b, info) => (b || (info.hasImplementation && !info.isAtomic)));

+            if (workTodo)

             {

-                var oldg = new GlobalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("old_{0}", g.Name), g.TypedIdent.Type));

-                globalMap[g] = new IdentifierExpr(Token.NoToken, oldg);

-                globalMods.Add(new IdentifierExpr(Token.NoToken, g));

+                foreach (Variable g in program.GlobalVariables())

+                {

+                    var oldg = new GlobalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("old_{0}", g.Name), g.TypedIdent.Type));

+                    globalMap[g] = new IdentifierExpr(Token.NoToken, oldg);

+                    globalMods.Add(new IdentifierExpr(Token.NoToken, g));

+                }

             }

         }

 

@@ -199,7 +205,7 @@ namespace Microsoft.Boogie
             }

         }

 

-        public void Transform(Program program)

+        public void Transform()

         {

             foreach (var decl in program.TopLevelDeclarations)

             {