Merge

10 files changed, 336 insertions, 114 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 009fb071..33c4e91a 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -2354,9 +2354,10 @@ namespace Microsoft.Boogie {
     public override void Typecheck(TypecheckingContext tc) {

       //Contract.Requires(tc != null);

         bool isAtomicSpecification =

-            QKeyValue.FindIntAttribute(this.Attributes, "atomic", -1) != -1 ||

-            QKeyValue.FindIntAttribute(this.Attributes, "rightmover", -1) != -1 ||

-            QKeyValue.FindIntAttribute(this.Attributes, "leftmover", -1) != -1;

+            QKeyValue.FindBoolAttribute(this.Attributes, "atomic") ||

+            QKeyValue.FindBoolAttribute(this.Attributes, "right") ||

+            QKeyValue.FindBoolAttribute(this.Attributes, "left") ||

+            QKeyValue.FindBoolAttribute(this.Attributes, "both");

       bool oldYields = tc.Yields;

       tc.Yields = isAtomicSpecification;

       this.Condition.Typecheck(tc);

diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs
index f3056e4f..cb6ce689 100644
--- a/Source/Core/DeadVarElim.cs
+++ b/Source/Core/DeadVarElim.cs
@@ -42,6 +42,7 @@ namespace Microsoft.Boogie {
     static Procedure enclosingProc;

     static Dictionary<Procedure/*!*/, HashSet<Variable/*!*/>/*!*/>/*!*/ modSets;

     static HashSet<Procedure> yieldingProcs;

+    static HashSet<Procedure> asyncAndParallelCallTargetProcs;

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(cce.NonNullDictionaryAndValues(modSets));

@@ -69,6 +70,7 @@ namespace Microsoft.Boogie {
 

       modSets = new Dictionary<Procedure/*!*/, HashSet<Variable/*!*/>/*!*/>();

       yieldingProcs = new HashSet<Procedure>();

+      asyncAndParallelCallTargetProcs = new HashSet<Procedure>();

 

       HashSet<Procedure/*!*/> implementedProcs = new HashSet<Procedure/*!*/>();

       foreach (Declaration/*!*/ decl in program.TopLevelDeclarations) {

@@ -118,6 +120,10 @@ namespace Microsoft.Boogie {
           {

               x.AddAttribute("yields");

           }

+          if (asyncAndParallelCallTargetProcs.Contains(x) && !QKeyValue.FindBoolAttribute(x.Attributes, "stable"))

+          {

+              x.AddAttribute("stable");

+          }

       }

 

       if (false /*CommandLineOptions.Clo.Trace*/)      {

@@ -209,6 +215,7 @@ namespace Microsoft.Boogie {
           var curr = callCmd;

           while (curr != null)

           {

+              asyncAndParallelCallTargetProcs.Add(curr.Proc);

               if (!yieldingProcs.Contains(curr.Proc)) 

               {

                   yieldingProcs.Add(curr.Proc);

diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs
index 61b3a322..ad9ecef0 100644
--- a/Source/Core/Inline.cs
+++ b/Source/Core/Inline.cs
@@ -50,6 +50,7 @@ namespace Microsoft.Boogie {
         Inliner codeExprInliner = new Inliner(program, inlineCallback, CommandLineOptions.Clo.InlineDepth);

         codeExprInliner.newLocalVars = new List<Variable>(node.LocVars);

         codeExprInliner.newModifies = new List<IdentifierExpr>();

+        codeExprInliner.inlinedProcLblMap = this.inlinedProcLblMap;

         List<Block> newCodeExprBlocks = codeExprInliner.DoInlineBlocks(node.Blocks, ref inlinedSomething);

         return new CodeExpr(codeExprInliner.newLocalVars, newCodeExprBlocks);

     }

diff --git a/Source/Core/LinearSets.cs b/Source/Core/LinearSets.cs
index 5769cbdf..3a9de5fb 100644
--- a/Source/Core/LinearSets.cs
+++ b/Source/Core/LinearSets.cs
@@ -9,16 +9,16 @@ namespace Microsoft.Boogie
 {

     public class LinearEraser : StandardVisitor

     {

-        private QKeyValue Remove(QKeyValue iter)

+        private QKeyValue RemoveLinearAttribute(QKeyValue iter)

         {

             if (iter == null) return null;

-            iter.Next = Remove(iter.Next);

+            iter.Next = RemoveLinearAttribute(iter.Next);

             return (QKeyValue.FindStringAttribute(iter, "linear") == null) ? iter : iter.Next;

         }

 

         public override Variable VisitVariable(Variable node)

         {

-            node.Attributes = Remove(node.Attributes);

+            node.Attributes = RemoveLinearAttribute(node.Attributes);

             return base.VisitVariable(node);

         }

     }

@@ -29,9 +29,10 @@ namespace Microsoft.Boogie
         public int errorCount;

         public CheckingContext checkingContext;

         public Dictionary<string, Type> domainNameToType;

-        public Dictionary<Absy, HashSet<Variable>> availableLocalLinearVars;

+        public Dictionary<Absy, HashSet<Variable>> availableLinearVars;

         public Dictionary<Variable, string> inoutParamToDomainName;

         public Dictionary<Variable, string> varToDomainName;

+        public Dictionary<Variable, string> globalVarToDomainName;

         public Dictionary<string, LinearDomain> linearDomains;

 

         public LinearTypechecker(Program program)

@@ -41,7 +42,7 @@ namespace Microsoft.Boogie
             this.checkingContext = new CheckingContext(null);

             this.domainNameToType = new Dictionary<string, Type>();

             this.parallelCallInvars = new HashSet<Variable>();

-            this.availableLocalLinearVars = new Dictionary<Absy, HashSet<Variable>>();

+            this.availableLinearVars = new Dictionary<Absy, HashSet<Variable>>();

             this.inoutParamToDomainName = new Dictionary<Variable, string>();

             this.varToDomainName = new Dictionary<Variable, string>();

             this.linearDomains = new Dictionary<string, LinearDomain>();

@@ -59,9 +60,22 @@ namespace Microsoft.Boogie
             checkingContext.Error(node, message);

             errorCount++;

         }

+        public override Program VisitProgram(Program node)

+        {

+            globalVarToDomainName = new Dictionary<Variable, string>();

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

+            {

+                string domainName = FindDomainName(g);

+                if (domainName != null)

+                {

+                    globalVarToDomainName[g] = domainName;

+                }

+            }

+            return base.VisitProgram(node);

+        }

         public override Implementation VisitImplementation(Implementation node)

         {

-            HashSet<Variable> start = new HashSet<Variable>();

+            HashSet<Variable> start = new HashSet<Variable>(globalVarToDomainName.Keys);

             for (int i = 0; i < node.InParams.Count; i++)

             {

                 string domainName = FindDomainName(node.Proc.InParams[i]);

@@ -87,7 +101,7 @@ namespace Microsoft.Boogie
 

             Stack<Block> dfsStack = new Stack<Block>();

             HashSet<Block> dfsStackAsSet = new HashSet<Block>();

-            availableLocalLinearVars[node.Blocks[0]] = start;

+            availableLinearVars[node.Blocks[0]] = start;

             dfsStack.Push(node.Blocks[0]);

             dfsStackAsSet.Add(node.Blocks[0]);

             while (dfsStack.Count > 0)

@@ -97,27 +111,31 @@ namespace Microsoft.Boogie
                 HashSet<Variable> end = PropagateAvailableLinearVarsAcrossBlock(b);

                 if (b.TransferCmd is ReturnCmd)

                 {

+                    foreach (GlobalVariable g in globalVarToDomainName.Keys.Except(end))

+                    {

+                        Error(b, string.Format("Global variable {0} must be available at a return", g.Name));

+                    } 

                     foreach (Variable v in node.OutParams)

                     {

                         if (FindDomainName(v) == null || end.Contains(v)) continue;

-                        Error(b, "output variable must be available at a return");

+                        Error(b, string.Format("Output variable {0} must be available at a return", v.Name));

                     }

+                    continue;

                 }

-                if (b.TransferCmd is ReturnCmd) continue;

                 GotoCmd gotoCmd = b.TransferCmd as GotoCmd;

                 foreach (Block target in gotoCmd.labelTargets)

                 {

-                    if (!availableLocalLinearVars.ContainsKey(target))

+                    if (!availableLinearVars.ContainsKey(target))

                     {

-                        availableLocalLinearVars[target] = new HashSet<Variable>(end);

+                        availableLinearVars[target] = new HashSet<Variable>(end);

                         dfsStack.Push(target);

                         dfsStackAsSet.Add(target);

                     }

                     else

                     {

-                        var savedAvailableVars = new HashSet<Variable>(availableLocalLinearVars[target]);

-                        availableLocalLinearVars[target].IntersectWith(end);

-                        if (savedAvailableVars.IsProperSupersetOf(availableLocalLinearVars[target]) && !dfsStackAsSet.Contains(target))

+                        var savedAvailableVars = new HashSet<Variable>(availableLinearVars[target]);

+                        availableLinearVars[target].IntersectWith(end);

+                        if (savedAvailableVars.IsProperSupersetOf(availableLinearVars[target]) && !dfsStackAsSet.Contains(target))

                         {

                             dfsStack.Push(target);

                             dfsStackAsSet.Add(target);

@@ -128,7 +146,7 @@ namespace Microsoft.Boogie
             return impl;

         }

         private HashSet<Variable> PropagateAvailableLinearVarsAcrossBlock(Block b) {

-            HashSet<Variable> start = new HashSet<Variable>(availableLocalLinearVars[b]);

+            HashSet<Variable> start = new HashSet<Variable>(availableLinearVars[b]);

             foreach (Cmd cmd in b.Cmds)

             {

                 if (cmd is AssignCmd)

@@ -155,6 +173,10 @@ namespace Microsoft.Boogie
                 }

                 else if (cmd is CallCmd)

                 {

+                    foreach (GlobalVariable g in globalVarToDomainName.Keys.Except(start))

+                    {

+                        Error(b, string.Format("Global variable {0} must be available at a call", g.Name));

+                    } 

                     CallCmd callCmd = (CallCmd)cmd;

                     while (callCmd != null)

                     {

@@ -174,7 +196,7 @@ namespace Microsoft.Boogie
                         callCmd = callCmd.InParallelWith;

                     }

                     callCmd = (CallCmd)cmd;

-                    availableLocalLinearVars[callCmd] = new HashSet<Variable>(start);

+                    availableLinearVars[callCmd] = new HashSet<Variable>(start);

                     while (callCmd != null)

                     {

                         foreach (IdentifierExpr ie in callCmd.Outs)

@@ -196,13 +218,19 @@ namespace Microsoft.Boogie
                 }

                 else if (cmd is YieldCmd)

                 {

-                    availableLocalLinearVars[cmd] = new HashSet<Variable>(start);

+                    foreach (GlobalVariable g in globalVarToDomainName.Keys.Except(start))

+                    {

+                        Error(b, string.Format("Global variable {0} must be available at a yield", g.Name));

+                    }

+                    availableLinearVars[cmd] = new HashSet<Variable>(start);

                 }

             }

             return start;

         }

         public string FindDomainName(Variable v)

         {

+            if (globalVarToDomainName.ContainsKey(v))

+                return globalVarToDomainName[v];

             if (inoutParamToDomainName.ContainsKey(v))

                 return inoutParamToDomainName[v];

             return QKeyValue.FindStringAttribute(v.Attributes, "linear");

@@ -233,7 +261,7 @@ namespace Microsoft.Boogie
                 }

                 if (domainNameToType.ContainsKey(domainName) && !domainNameToType[domainName].Equals(type))

                 {

-                    Error(node, "a linear domain must be consistently attached to variables of a particular type");

+                    Error(node, string.Format("Linear domain {0} must be consistently attached to variables of one type", domainName));

                 }

                 else

                 {

@@ -248,44 +276,35 @@ namespace Microsoft.Boogie
             for (int i = 0; i < node.Lhss.Count; i++)

             {

                 AssignLhs lhs = node.Lhss[i];

-                string domainName = FindDomainName(lhs.DeepAssignedVariable);

+                Variable lhsVar = lhs.DeepAssignedVariable;

+                string domainName = FindDomainName(lhsVar);

                 if (domainName == null) continue;

                 SimpleAssignLhs salhs = lhs as SimpleAssignLhs;

                 if (salhs == null)

                 {

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

-                    continue;

-                }

-                if (salhs.DeepAssignedVariable is GlobalVariable)

-                {

-                    Error(node, "Linear global variable cannot be written to");

+                    Error(node, string.Format("Only simple assignment allowed on linear variable {0}", lhsVar.Name));

                     continue;

                 }

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

                 if (rhs == null)

                 {

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

+                    Error(node, string.Format("Only variable can be assigned to linear variable {0}", lhsVar.Name));

                     continue; 

                 }

                 string rhsDomainName = FindDomainName(rhs.Decl);

                 if (rhsDomainName == null)

                 {

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

+                    Error(node, string.Format("Only linear variable can be assigned to linear variable {0}", lhsVar.Name));

                     continue;

                 }

                 if (domainName != rhsDomainName)

                 {

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

+                    Error(node, string.Format("Linear variable of domain {0} cannot be assigned to linear variable of domain {1}", rhsDomainName, domainName));

                     continue;

                 }

                 if (rhsVars.Contains(rhs.Decl))

                 {

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

-                    continue;

-                }

-                if (rhs.Decl is GlobalVariable)

-                {

-                    Error(node, "Linear global variable cannot be read from");

+                    Error(node, string.Format("Linear variable {0} can occur only once in the right-hand-side of an assignment", rhs.Decl.Name));

                     continue;

                 }

                 rhsVars.Add(rhs.Decl);

@@ -304,13 +323,13 @@ namespace Microsoft.Boogie
                 IdentifierExpr actual = node.Ins[i] as IdentifierExpr;

                 if (actual == null)

                 {

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

+                    Error(node, string.Format("Only variable can be passed to linear parameter {0}", formal.Name));

                     continue;

                 }

                 string actualDomainName = FindDomainName(actual.Decl);

                 if (actualDomainName == null)

                 {

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

+                    Error(node, string.Format("Only a linear argument can be passed to linear parameter {0}", formal.Name));

                     continue;

                 }

                 if (domainName != actualDomainName)

@@ -320,7 +339,7 @@ namespace Microsoft.Boogie
                 }

                 if (parallelCallInvars.Contains(actual.Decl))

                 {

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

+                    Error(node, string.Format("Linear variable {0} can occur only once as an input parameter", actual.Decl.Name));

                     continue;

                 }

                 if (actual.Decl is GlobalVariable)

@@ -373,13 +392,7 @@ namespace Microsoft.Boogie
                 domainNameToScope[domainName] = new HashSet<Variable>();

                 domainNameToScope[domainName].Add(domainNameToInputVar[domainName]);

             }

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

-            {

-                var domainName = FindDomainName(v);

-                if (domainName == null) continue;

-                domainNameToScope[domainName].Add(v);

-            }

-            foreach (Variable v in availableLocalLinearVars[absy])

+            foreach (Variable v in availableLinearVars[absy])

             {

                 var domainName = FindDomainName(v);

                 domainNameToScope[domainName].Add(v);

@@ -453,7 +466,7 @@ namespace Microsoft.Boogie
                                 {

                                     domainNameToExpr[domainName] = new IdentifierExpr(Token.NoToken, domainNameToInputVar[domainName]);

                                 }

-                                foreach (Variable v in availableLocalLinearVars[callCmd])

+                                foreach (Variable v in availableLinearVars[callCmd])

                                 {

                                     var domainName = FindDomainName(v);

                                     var domain = linearDomains[domainName];

@@ -510,10 +523,9 @@ namespace Microsoft.Boogie
                     domainNameToOutputScope[domainName] = new HashSet<Variable>();

                     

                 }

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

+                foreach (Variable v in globalVarToDomainName.Keys)

                 {

-                    var domainName = FindDomainName(v);

-                    if (domainName == null) continue;

+                    var domainName = globalVarToDomainName[v];

                     domainNameToInputScope[domainName].Add(v);

                     domainNameToOutputScope[domainName].Add(v);

                 }

diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs
index ed4d8dbb..dd6276c2 100644
--- a/Source/Core/OwickiGries.cs
+++ b/Source/Core/OwickiGries.cs
@@ -67,7 +67,7 @@ namespace Microsoft.Boogie
             newCmds.Add(yieldCallCmd);

         }

 

-        private Dictionary<string, Expr> ComputeAvailableExprs(HashSet<Variable> availableLocalLinearVars, Dictionary<string, Variable> domainNameToInputVar)

+        private Dictionary<string, Expr> ComputeAvailableExprs(HashSet<Variable> availableLinearVars, Dictionary<string, Variable> domainNameToInputVar)

         {

             Dictionary<string, Expr> domainNameToExpr = new Dictionary<string, Expr>();

             foreach (var domainName in linearTypechecker.linearDomains.Keys)

@@ -77,7 +77,7 @@ namespace Microsoft.Boogie
                 expr.Typecheck(new TypecheckingContext(null));

                 domainNameToExpr[domainName] = expr;

             }

-            foreach (Variable v in availableLocalLinearVars)

+            foreach (Variable v in availableLinearVars)

             {

                 var domainName = linearTypechecker.FindDomainName(v);

                 var domain = linearTypechecker.linearDomains[domainName];

@@ -118,7 +118,7 @@ namespace Microsoft.Boogie
             {

                 newCmds.Add(new HavocCmd(Token.NoToken, globalMods));

             }

-            Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(linearTypechecker.availableLocalLinearVars[yieldCmd], domainNameToInputVar);

+            Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(linearTypechecker.availableLinearVars[yieldCmd], domainNameToInputVar);

             AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);

 

             for (int j = 0; j < cmds.Count; j++)

@@ -264,7 +264,7 @@ namespace Microsoft.Boogie
                     PredicateCmd predCmd = (PredicateCmd)cmd;

                     var newExpr = Substituter.ApplyReplacingOldExprs(subst, oldSubst, predCmd.Expr);

                     if (predCmd is AssertCmd)

-                        newCmds.Add(new AssertCmd(predCmd.tok, newExpr));

+                        newCmds.Add(new AssertCmd(predCmd.tok, newExpr, predCmd.Attributes));

                     else

                         newCmds.Add(new AssumeCmd(Token.NoToken, newExpr));

                 }

@@ -440,13 +440,13 @@ namespace Microsoft.Boogie
                         if (callCmd.InParallelWith != null || callCmd.IsAsync ||

                             QKeyValue.FindBoolAttribute(callCmd.Proc.Attributes, "yields"))

                         {

-                            HashSet<Variable> availableLocalLinearVars = new HashSet<Variable>(linearTypechecker.availableLocalLinearVars[callCmd]);

+                            HashSet<Variable> availableLinearVars = new HashSet<Variable>(linearTypechecker.availableLinearVars[callCmd]);

                             foreach (IdentifierExpr ie in callCmd.Outs)

                             {

                                 if (linearTypechecker.FindDomainName(ie.Decl) == null) continue;

-                                availableLocalLinearVars.Add(ie.Decl);

+                                availableLinearVars.Add(ie.Decl);

                             }

-                            Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(availableLocalLinearVars, domainNameToInputVar);

+                            Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(availableLinearVars, domainNameToInputVar);

                             AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);

                         }

                     }

@@ -473,7 +473,7 @@ namespace Microsoft.Boogie
 

             foreach (Block header in yieldingHeaders)

             {

-                Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(linearTypechecker.availableLocalLinearVars[header], domainNameToInputVar);

+                Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(linearTypechecker.availableLinearVars[header], domainNameToInputVar);

                 foreach (Block pred in header.Predecessors)

                 {

                     AddCallToYieldProc(pred.Cmds, ogOldGlobalMap, domainNameToLocalVar);

@@ -582,7 +582,7 @@ namespace Microsoft.Boogie
                     }

                     else

                     {

-                        cmds.Add(new AssertCmd(r.tok, r.Condition));

+                        cmds.Add(new AssertCmd(r.tok, r.Condition, r.Attributes));

                     }

                 }

                 yields.Add(cmds);

@@ -621,7 +621,7 @@ namespace Microsoft.Boogie
                     }

                     else

                     {

-                        cmds.Add(new AssertCmd(e.tok, e.Condition));

+                        cmds.Add(new AssertCmd(e.tok, e.Condition, e.Attributes));

                     }

                 }

                 yields.Add(cmds);

@@ -680,6 +680,13 @@ namespace Microsoft.Boogie
             program.TopLevelDeclarations.Add(yieldImpl);

         }

 

+        private QKeyValue RemoveYieldsAttribute(QKeyValue iter)

+        {

+            if (iter == null) return null;

+            iter.Next = RemoveYieldsAttribute(iter.Next);

+            return (QKeyValue.FindBoolAttribute(iter, "yields")) ? iter.Next : iter;

+        }

+

         public void Transform()

         {

             Program program = linearTypechecker.program;

@@ -708,12 +715,22 @@ namespace Microsoft.Boogie
                 if (proc == null) continue;

                 if (QKeyValue.FindBoolAttribute(proc.Attributes, "yields"))

                 {

+                    HashSet<Variable> modifiedVars = new HashSet<Variable>();

+                    proc.Modifies.Iter(x => modifiedVars.Add(x.Decl));

                     foreach (GlobalVariable g in program.GlobalVariables())

                     {

+                        if (modifiedVars.Contains(g)) continue;

                         proc.Modifies.Add(new IdentifierExpr(Token.NoToken, g));

                     }

+                    proc.Attributes = RemoveYieldsAttribute(proc.Attributes);

                 }

             }

+            foreach (var decl in program.TopLevelDeclarations)

+            {

+                Implementation impl = decl as Implementation;

+                if (impl == null) continue;

+                impl.Attributes = RemoveYieldsAttribute(impl.Attributes);

+            }

         }

     }

 }

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 4ebe17dc..81a2ad39 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -443,6 +443,7 @@ namespace Microsoft.Boogie
           }

         }

 

+        if(CommandLineOptions.Clo.StratifiedInlining == 0)

         {

           OwickiGriesTransform ogTransform = new OwickiGriesTransform(linearTypechecker);

           ogTransform.Transform();

diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index 0b92b1c3..a6b01760 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -47,7 +47,7 @@ namespace Microsoft.Boogie.VCExprAST {
     }

   }

 

-  public delegate VCExpr/*!*/ CodeExprConverter(CodeExpr/*!*/ codeExpr, Hashtable/*<Block, VCExprVar!>*//*!*/ blockVariables, List<VCExprLetBinding> bindings);

+  public delegate VCExpr/*!*/ CodeExprConverter(CodeExpr/*!*/ codeExpr, Hashtable/*<Block, VCExprVar!>*//*!*/ blockVariables, List<VCExprLetBinding> bindings, bool isPositiveContext);

 

   public class Boogie2VCExprTranslator : StandardVisitor, ICloneable {

     // Stack on which the various Visit-methods put the result of the translation

@@ -375,13 +375,42 @@ namespace Microsoft.Boogie.VCExprAST {
       return node;

     }

 

+    public bool isPositiveContext = true;

     private VCExpr TranslateNAryExpr(NAryExpr node) {

       Contract.Requires(node != null);

       Contract.Ensures(Contract.Result<VCExpr>() != null);

+     

+      bool flipContextForArg0 = false;

+      if (node.Fun is UnaryOperator)

+      {

+          UnaryOperator oper = (UnaryOperator)node.Fun;

+          if (oper.Op == UnaryOperator.Opcode.Not)

+              flipContextForArg0 = true;

+      }

+      else if (node.Fun is BinaryOperator)

+      {

+          BinaryOperator oper = (BinaryOperator)node.Fun;

+          if (oper.Op == BinaryOperator.Opcode.Imp)

+              flipContextForArg0 = true;

+          else if (oper.Op == BinaryOperator.Opcode.Iff) {

+              Expr one = new NAryExpr(node.tok, new BinaryOperator(node.tok, BinaryOperator.Opcode.Imp), new List<Expr> { node.Args[0], node.Args[1] });

+              Expr two = new NAryExpr(node.tok, new BinaryOperator(node.tok, BinaryOperator.Opcode.Imp), new List<Expr> { node.Args[1], node.Args[0] });

+              NAryExpr cmpd = new NAryExpr(node.tok, new BinaryOperator(node.tok, BinaryOperator.Opcode.And), new List<Expr> { one, two });

+              TypecheckingContext tc = new TypecheckingContext(null);

+              cmpd.Typecheck(tc);

+              return TranslateNAryExpr(cmpd);

+          }

+      }

+

       int n = node.Args.Count;

       List<VCExpr/*!*/>/*!*/ vcs = new List<VCExpr/*!*/>(n);

+        

       for (int i = 0; i < n; i++) {

+        if (i == 0 && flipContextForArg0)

+            isPositiveContext = !isPositiveContext;

         vcs.Add(Translate(cce.NonNull(node.Args)[i]));

+        if (i == 0 && flipContextForArg0)

+            isPositiveContext = !isPositiveContext;

       }

 

       if (node.Type == null) {

@@ -611,19 +640,18 @@ namespace Microsoft.Boogie.VCExprAST {
       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

-    CodeExprConverter codeExprConverter = null;

+    public CodeExprConverter codeExprConverter = null;

     public void SetCodeExprConverter(CodeExprConverter f) {

       this.codeExprConverter = f;

     }

     public override Expr/*!*/ VisitCodeExpr(CodeExpr/*!*/ codeExpr) {

       //Contract.Requires(codeExpr != null);

       Contract.Ensures(Contract.Result<Expr>() != null);

-

       Contract.Assume(codeExprConverter != null);

 

       Hashtable/*<Block, LetVariable!>*/ blockVariables = new Hashtable/*<Block, LetVariable!!>*/();

       List<VCExprLetBinding/*!*/> bindings = new List<VCExprLetBinding/*!*/>();

-      VCExpr e = codeExprConverter(codeExpr, blockVariables, bindings);

+      VCExpr e = codeExprConverter(codeExpr, blockVariables, bindings, isPositiveContext);

       Push(e);

       return codeExpr;

     }

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 7d8d749c..086dde15 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -266,13 +266,19 @@ namespace VC {
       VCExpressionGenerator gen = proverInterface.VCExprGen;

       var exprGen = proverInterface.Context.ExprGen;

       var translator = proverInterface.Context.BoogieExprTranslator;

+      

       VCExpr controlFlowVariableExpr = null;

       if (!CommandLineOptions.Clo.UseLabels) {

         controlFlowVariable = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "@cfc", Microsoft.Boogie.Type.Int));

         controlFlowVariableExpr = translator.LookupVariable(controlFlowVariable);

         vcgen.InstrumentCallSites(impl);

       }

-      vcexpr = gen.Not(vcgen.GenerateVC(impl, controlFlowVariableExpr, out label2absy, proverInterface.Context));

+      

+      label2absy = new Dictionary<int, Absy>();

+      VCGen.CodeExprConversionClosure cc = new VCGen.CodeExprConversionClosure(label2absy, proverInterface.Context);

+      translator.SetCodeExprConverter(cc.CodeExprToVerificationCondition); 

+      vcexpr = gen.Not(vcgen.GenerateVCAux(impl, controlFlowVariableExpr, label2absy, proverInterface.Context));

+      

       if (controlFlowVariableExpr != null) {

         VCExpr controlFlowFunctionAppl = exprGen.ControlFlowFunctionApplication(controlFlowVariableExpr, exprGen.Integer(BigNum.ZERO));

         VCExpr eqExpr = exprGen.Eq(controlFlowFunctionAppl, exprGen.Integer(BigNum.FromInt(impl.Blocks[0].UniqueId)));

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 85d0fb31..2abe4a1b 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1245,44 +1245,8 @@ namespace VC {
 

         ProverContext ctx = checker.TheoremProver.Context;

         Boogie2VCExprTranslator bet = ctx.BoogieExprTranslator;

-        bet.SetCodeExprConverter(

-          new CodeExprConverter(

-          delegate(CodeExpr codeExpr, Hashtable/*<Block, VCExprVar!>*/ blockVariables, List<VCExprLetBinding/*!*/> bindings)

-          {

-            VCGen vcgen = new VCGen(new Program(), null, false, parent.checkers);

-            vcgen.variable2SequenceNumber = new Dictionary<Variable, int>();

-            vcgen.incarnationOriginMap = new Dictionary<Incarnation, Absy>();

-            vcgen.CurrentLocalVariables = codeExpr.LocVars;

-            // codeExpr.Blocks.PruneUnreachableBlocks();  // This is needed for VCVariety.BlockNested, and is otherwise just an optimization

-

-            ResetPredecessors(codeExpr.Blocks);

-            vcgen.AddBlocksBetween(codeExpr.Blocks);

-            Dictionary<Variable, Expr> gotoCmdOrigins = vcgen.ConvertBlocks2PassiveCmd(codeExpr.Blocks, new List<IdentifierExpr>(), new ModelViewInfo(codeExpr));

-            int ac;  // computed, but then ignored for this CodeExpr

-            VCExpr startCorrect = VCGen.LetVC(codeExpr.Blocks[0], null, label2absy, blockVariables, bindings, ctx, out ac);

-            VCExpr vce = ctx.ExprGen.Let(bindings, startCorrect);

-

-            if (vcgen.CurrentLocalVariables.Count != 0)

-            {

-              Boogie2VCExprTranslator translator = checker.TheoremProver.Context.BoogieExprTranslator;

-              List<VCExprVar> boundVars = new List<VCExprVar>();

-              foreach (Variable v in vcgen.CurrentLocalVariables)

-              {

-                Contract.Assert(v != null);

-                VCExprVar ev = translator.LookupVariable(v);

-                Contract.Assert(ev != null);

-                boundVars.Add(ev);

-                if (v.TypedIdent.Type.Equals(Bpl.Type.Bool))

-                {

-                  // add an antecedent (tickleBool ev) to help the prover find a possible trigger

-                  vce = checker.VCExprGen.Implies(checker.VCExprGen.Function(VCExpressionGenerator.TickleBoolOp, ev), vce);

-                }

-              }

-              vce = checker.VCExprGen.Forall(boundVars, new List<VCTrigger>(), vce);

-            }

-            return vce;

-          }

-        ));

+        CodeExprConversionClosure cc = new CodeExprConversionClosure(label2absy, ctx);

+        bet.SetCodeExprConverter(cc.CodeExprToVerificationCondition);

 

         var exprGen = ctx.ExprGen;

         VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO);

@@ -1370,6 +1334,56 @@ namespace VC {
     }

     #endregion

 

+

+    public class CodeExprConversionClosure

+    {

+        Dictionary<int, Absy> label2absy;

+        ProverContext ctx;

+        public CodeExprConversionClosure(Dictionary<int, Absy> label2absy, ProverContext ctx)

+        {

+            this.label2absy = label2absy;

+            this.ctx = ctx;

+        }

+

+        public VCExpr CodeExprToVerificationCondition(CodeExpr codeExpr, Hashtable blockVariables, List<VCExprLetBinding> bindings, bool isPositiveContext)

+        {

+            VCGen vcgen = new VCGen(new Program(), null, false, new List<Checker>());

+            vcgen.variable2SequenceNumber = new Dictionary<Variable, int>();

+            vcgen.incarnationOriginMap = new Dictionary<Incarnation, Absy>();

+            vcgen.CurrentLocalVariables = codeExpr.LocVars;

+

+            ResetPredecessors(codeExpr.Blocks);

+            vcgen.AddBlocksBetween(codeExpr.Blocks);

+            Dictionary<Variable, Expr> gotoCmdOrigins = vcgen.ConvertBlocks2PassiveCmd(codeExpr.Blocks, new List<IdentifierExpr>(), new ModelViewInfo(codeExpr));

+            int ac;  // computed, but then ignored for this CodeExpr

+            VCExpr startCorrect = VCGen.LetVCIterative(codeExpr.Blocks, null, label2absy, ctx, out ac, isPositiveContext);

+            VCExpr vce = ctx.ExprGen.Let(bindings, startCorrect);

+            if (vcgen.CurrentLocalVariables.Count != 0)

+            {

+                Boogie2VCExprTranslator translator = ctx.BoogieExprTranslator;

+                List<VCExprVar> boundVars = new List<VCExprVar>();

+                foreach (Variable v in vcgen.CurrentLocalVariables)

+                {

+                    Contract.Assert(v != null);

+                    VCExprVar ev = translator.LookupVariable(v);

+                    Contract.Assert(ev != null);

+                    boundVars.Add(ev);

+                    if (v.TypedIdent.Type.Equals(Bpl.Type.Bool))

+                    {

+                        // add an antecedent (tickleBool ev) to help the prover find a possible trigger

+                        vce = ctx.ExprGen.Implies(ctx.ExprGen.Function(VCExpressionGenerator.TickleBoolOp, ev), vce);

+                    }

+                }

+                vce = ctx.ExprGen.Forall(boundVars, new List<VCTrigger>(), vce);

+            }

+            if (isPositiveContext)

+            {

+                vce = ctx.ExprGen.Not(vce);

+            } 

+            return vce;

+        }

+    }

+

     public VCExpr GenerateVC(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, out Dictionary<int, Absy>/*!*/ label2absy, ProverContext proverContext)

     {

       Contract.Requires(impl != null);

@@ -1381,7 +1395,7 @@ namespace VC {
       return GenerateVCAux(impl, controlFlowVariableExpr, label2absy, proverContext);

     }

 

-    protected VCExpr GenerateVCAux(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, Dictionary<int, Absy>/*!*/ label2absy, ProverContext proverContext) {

+    public VCExpr GenerateVCAux(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, Dictionary<int, Absy>/*!*/ label2absy, ProverContext proverContext) {

       Contract.Requires(impl != null);

       Contract.Requires(proverContext != null);

       Contract.Ensures(Contract.Result<VCExpr>() != null);

@@ -1467,6 +1481,133 @@ namespace VC {
       ModelViewInfo mvInfo;

       var gotoCmdOrigins = PassifyImpl(impl, out mvInfo);

 

+      // If "expand" attribute is supplied, expand any assertion of conjunctions into multiple assertions, one per conjunct

+      foreach (var b in impl.Blocks)

+      {

+        List<Cmd> newCmds = new List<Cmd>();

+        bool changed = false;

+        foreach (var c in b.Cmds)

+        {

+          var a = c as AssertCmd;

+          var ar = c as AssertRequiresCmd;

+          var ae = c as AssertEnsuresCmd;

+          var ai = c as LoopInitAssertCmd;

+          var am = c as LoopInvMaintainedAssertCmd;

+          // TODO:

+          //use Duplicator and Substituter rather than new

+          //nested IToken?

+          //document expand attribute (search for {:ignore}, for example)

+          //fix up new CallCmd, new Requires, new Ensures in OwickiGries.cs

+          Func<Expr,Expr,Expr> withType = (Expr from, Expr to) =>

+          {

+            NAryExpr nFrom = from as NAryExpr;

+            NAryExpr nTo = to as NAryExpr;

+            to.Type = from.Type;

+            if (nFrom != null && nTo != null) nTo.TypeParameters = nFrom.TypeParameters;

+            return to;

+          };

+

+          Action<int,Expr,Action<Expr>> traverse = null;

+          traverse = (depth, e, act) =>

+          {

+            ForallExpr forall = e as ForallExpr;

+            NAryExpr nary = e as NAryExpr;

+            if (forall != null)

+            {

+              traverse(depth, forall.Body, e1 => act(withType(forall,

+                new ForallExpr(e1.tok, forall.TypeParameters, forall.Dummies, forall.Attributes, forall.Triggers, e1))));

+              return;

+            }

+            if (nary != null)

+            {

+              var args = nary.Args;

+              IAppliable fun = nary.Fun;

+              BinaryOperator bop = fun as BinaryOperator;

+              FunctionCall call = fun as FunctionCall;

+              if (bop != null)

+              {

+                switch (bop.Op)

+                {

+                  case BinaryOperator.Opcode.And:

+                    traverse(depth, args[0], act);

+                    traverse(depth, args[1], act);

+                    return;

+                  case BinaryOperator.Opcode.Imp:

+                    traverse(depth, args[1], e1 => act(withType(nary,

+                      new NAryExpr(e1.tok, fun, new List<Expr>() { args[0], e1 }))));

+                    return;

+                }

+              }

+              if (depth > 0 && call != null && call.Func != null)

+              {

+                Function cf = call.Func;

+                Expr body = cf.Body;

+                List<Variable> ins = cf.InParams;

+                if (body == null && cf.DefinitionAxiom != null)

+                {

+                  ForallExpr all = cf.DefinitionAxiom.Expr as ForallExpr;

+                  if (all != null)

+                  {

+                    NAryExpr def = all.Body as NAryExpr;

+                    if (def != null && def.Fun is BinaryOperator && ((BinaryOperator) (def.Fun)).Op == BinaryOperator.Opcode.Iff)

+                    {

+                      body = def.Args[1];

+                      ins = all.Dummies;

+                    }

+                  }

+                }

+                if (body != null)

+                {

+                  Func<Expr,Expr> new_f = e1 =>

+                  {

+                    Function f = new Function(cf.tok, "expand<" + cf.Name + ">", cf.TypeParameters, ins, cf.OutParams[0], cf.Comment);

+                    f.Body = e1;

+                    Token tok = new Token(e1.tok.line, e1.tok.col);

+                    tok.filename = e.tok.filename + "(" + e.tok.line + "," + e.tok.col + ") --> " + e1.tok.filename;

+                    return withType(nary, new NAryExpr(tok, new FunctionCall(f), args));

+                  };

+                  traverse(depth - 1, body, e1 => act(new_f(e1)));

+                  return;

+                }

+              }

+            }

+            act(e);

+          };

+

+          if (a != null)

+          {

+            var attr = a.Attributes;

+            if (ar != null && ar.Requires.Attributes != null) attr = ar.Requires.Attributes;

+            if (ar != null && ar.Call.Attributes != null) attr = ar.Call.Attributes;

+            if (ae != null && ae.Ensures.Attributes != null) attr = ae.Ensures.Attributes;

+            if (QKeyValue.FindExprAttribute(attr, "expand") != null || QKeyValue.FindBoolAttribute(attr, "expand"))

+            {

+              int depth = QKeyValue.FindIntAttribute(attr, "expand", 100);

+              Func<Expr,Expr> fe = e => Expr.Or(a.Expr, e);

+              //traverse(depth, a.Expr, e => System.Console.WriteLine(e.GetType() + " :: " + e + " @ " + e.tok.line + ", " + e.tok.col));

+              traverse(depth, a.Expr, e =>

+                {

+                  AssertCmd new_c = 

+                    (ar != null) ? new AssertRequiresCmd(ar.Call, new Requires(e.tok, ar.Requires.Free, fe(e), ar.Requires.Comment)) :

+                    (ae != null) ? new AssertEnsuresCmd(new Ensures(e.tok, ae.Ensures.Free, fe(e), ae.Ensures.Comment)) :

+                    (ai != null) ? new LoopInitAssertCmd(e.tok, fe(e)) :

+                    (am != null) ? new LoopInvMaintainedAssertCmd(e.tok, fe(e)) :

+                    new AssertCmd(e.tok, fe(e));

+                  new_c.Attributes = new QKeyValue(e.tok, "subsumption", new List<object>() { new LiteralExpr(e.tok, BigNum.FromInt(0)) }, a.Attributes);

+                  newCmds.Add(new_c);

+                });

+            }

+            newCmds.Add(c);

+            changed = true;

+          }

+          else

+          {

+            newCmds.Add(c);

+          }

+        }

+        if (changed) b.Cmds = newCmds;

+      }

+

       double max_vc_cost = CommandLineOptions.Clo.VcsMaxCost;

       int tmp_max_vc_cost = -1, max_splits = CommandLineOptions.Clo.VcsMaxSplits, 

           max_kg_splits = CommandLineOptions.Clo.VcsMaxKeepGoingSplits;

@@ -2589,7 +2730,9 @@ namespace VC {
                                  VCExpr controlFlowVariableExpr,

                                  Dictionary<int, Absy> label2absy,

                                  ProverContext proverCtxt,

-                                 out int assertionCount) {

+                                 out int assertionCount,

+                                 bool isPositiveContext = true)

+    {

       Contract.Requires(blocks != null);

       Contract.Requires(proverCtxt != null);

       Contract.Ensures(Contract.Result<VCExpr>() != null);

@@ -2625,6 +2768,10 @@ namespace VC {
           }

           else {

             SuccCorrect = proverCtxt.BoogieExprTranslator.Translate(re.Expr);

+            if (isPositiveContext)

+            {

+                SuccCorrect = gen.Not(SuccCorrect);

+            }

           }

         }

         else {

@@ -2643,7 +2790,7 @@ namespace VC {
           SuccCorrect = gen.NAry(VCExpressionGenerator.AndOp, SuccCorrectVars);

         }

 

-        VCContext context = new VCContext(label2absy, proverCtxt, controlFlowVariableExpr);

+        VCContext context = new VCContext(label2absy, proverCtxt, controlFlowVariableExpr, isPositiveContext);

         VCExpr vc = Wlp.Block(block, SuccCorrect, context);

         assertionCount += context.AssertionCount;

 

diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs
index 277d9a94..bb2a2785 100644
--- a/Source/VCGeneration/Wlp.cs
+++ b/Source/VCGeneration/Wlp.cs
@@ -24,22 +24,24 @@ namespace VC {
     [Rep] public readonly ProverContext Ctxt;

     public readonly VCExpr ControlFlowVariableExpr;

     public int AssertionCount;  // counts the number of assertions for which Wlp has been computed

-    

-    public VCContext(Dictionary<int, Absy> label2absy, ProverContext ctxt)

+    public bool isPositiveContext;

+

+    public VCContext(Dictionary<int, Absy> label2absy, ProverContext ctxt, bool isPositiveContext = true)

     {

       Contract.Requires(ctxt != null);

       this.Label2absy = label2absy;

       this.Ctxt = ctxt;

+      this.isPositiveContext = isPositiveContext;

     }

-    

-    public VCContext(Dictionary<int, Absy> label2absy, ProverContext ctxt, VCExpr controlFlowVariableExpr)

+

+    public VCContext(Dictionary<int, Absy> label2absy, ProverContext ctxt, VCExpr controlFlowVariableExpr, bool isPositiveContext = true)

     {

       Contract.Requires(ctxt != null);

       this.Label2absy = label2absy;

       this.Ctxt = ctxt;

       this.ControlFlowVariableExpr = controlFlowVariableExpr;

+      this.isPositiveContext = isPositiveContext;

     }

-    

   }

 

   #region A class to compute wlp of a passive command program

@@ -95,7 +97,9 @@ namespace VC {
       Contract.Assert(gen != null);

       if (cmd is AssertCmd) {

         AssertCmd ac = (AssertCmd)cmd;

+        ctxt.Ctxt.BoogieExprTranslator.isPositiveContext = !ctxt.Ctxt.BoogieExprTranslator.isPositiveContext;

         VCExpr C = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr);

+        ctxt.Ctxt.BoogieExprTranslator.isPositiveContext = !ctxt.Ctxt.BoogieExprTranslator.isPositiveContext; 

         if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {

           return gen.Implies(C, N);

         } else {

@@ -159,9 +163,7 @@ namespace VC {
             }

           }

         }

-

         return gen.ImpliesSimp(ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr), N);

-

       } else {

         Console.WriteLine(cmd.ToString());

         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected command