updated the mover checks

3 files changed, 64 insertions, 3 deletions

diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs
index 4957c829..73c1163a 100644
--- a/Source/Concurrency/MoverCheck.cs
+++ b/Source/Concurrency/MoverCheck.cs
@@ -562,6 +562,10 @@ namespace Microsoft.Boogie
             blocks.AddRange(firstBlocks);

             blocks.AddRange(secondBlocks);

             List<Requires> requires = DisjointnessRequires(program, first, second);

+            foreach (AssertCmd assertCmd in first.thatGate)

+                requires.Add(new Requires(false, assertCmd.Expr));

+            foreach (AssertCmd assertCmd in second.thisGate)

+                requires.Add(new Requires(false, assertCmd.Expr));

             List<Ensures> ensures = new List<Ensures>();

             Expr transitionRelation = (new TransitionRelationComputation(program, first, second)).TransitionRelationCompute();

             Ensures ensureCheck = new Ensures(false, transitionRelation);

@@ -604,6 +608,8 @@ namespace Microsoft.Boogie
                 ensureCheck.ErrorData = string.Format("Gate not preserved by {0}", second.proc.Name);

                 ensures.Add(ensureCheck);

             }

+            foreach (AssertCmd assertCmd in second.thisGate)

+                requires.Add(new Requires(false, assertCmd.Expr));

             string checkerName = string.Format("GatePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name);

             List<IdentifierExpr> globalVars = new List<IdentifierExpr>();

             program.GlobalVariables().Iter(x => globalVars.Add(Expr.Ident(x)));

@@ -618,6 +624,48 @@ namespace Microsoft.Boogie
         {

             if (first.gateUsedGlobalVars.Intersect(second.modifiedGlobalVars).Count() == 0)

                 return;

+            Tuple<ActionInfo, ActionInfo> actionPair = new Tuple<ActionInfo, ActionInfo>(first, second);

+            if (failurePreservationCheckerCache.Contains(actionPair))

+                return;

+            failurePreservationCheckerCache.Add(actionPair);

+

+            List<Variable> inputs = new List<Variable>();

+            inputs.AddRange(first.thatInParams);

+            inputs.AddRange(second.thisInParams);

+            List<Variable> outputs = new List<Variable>();

+            outputs.AddRange(first.thatOutParams);

+            outputs.AddRange(second.thisOutParams);

+            List<Variable> locals = new List<Variable>();

+            locals.AddRange(second.thisAction.LocVars);

+            List<Block> secondBlocks = CloneBlocks(second.thisAction.Blocks);

+            List<Requires> requires = DisjointnessRequires(program, first, second);

+            Expr gateExpr = Expr.True;

+            foreach (AssertCmd assertCmd in first.thatGate)

+            {

+                gateExpr = Expr.And(gateExpr, assertCmd.Expr);

+            }

+            requires.Add(new Requires(false, Expr.Not(gateExpr)));

+            List<Ensures> ensures = new List<Ensures>();

+            Ensures ensureCheck = new Ensures(false, Expr.Not(gateExpr));

+            ensureCheck.ErrorData = string.Format("Gate failure of {0} not preserved by {1}", first.proc.Name, second.proc.Name);

+            ensures.Add(ensureCheck);

+            foreach (AssertCmd assertCmd in second.thisGate)

+                requires.Add(new Requires(false, assertCmd.Expr));

+            string checkerName = string.Format("FailurePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name);

+            List<IdentifierExpr> globalVars = new List<IdentifierExpr>();

+            program.GlobalVariables().Iter(x => globalVars.Add(Expr.Ident(x)));

+            Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, globalVars, ensures);

+            Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, secondBlocks);

+            impl.Proc = proc;

+            this.decls.Add(impl);

+            this.decls.Add(proc);

+        }

+

+        /*

+        private void CreateFailurePreservationChecker(Program program, ActionInfo first, ActionInfo second)

+        {

+            if (first.gateUsedGlobalVars.Intersect(second.modifiedGlobalVars).Count() == 0)

+                return;

 

             Tuple<ActionInfo, ActionInfo> actionPair = new Tuple<ActionInfo, ActionInfo>(first, second); 

             if (failurePreservationCheckerCache.Contains(actionPair))

@@ -660,7 +708,8 @@ namespace Microsoft.Boogie
             this.decls.Add(impl);

             this.decls.Add(proc);

         }

-

+        */

+        

         private void CreateNonBlockingChecker(Program program, ActionInfo second)

         {

             List<Variable> inputs = new List<Variable>();

diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs
index b646e8cf..9ec07854 100644
--- a/Source/Concurrency/OwickiGries.cs
+++ b/Source/Concurrency/OwickiGries.cs
@@ -1283,7 +1283,19 @@ namespace Microsoft.Boogie
                         duplicateProc.Modifies = new List<IdentifierExpr>();

                         program.GlobalVariables().Iter(x => duplicateProc.Modifies.Add(Expr.Ident(x)));

                         CodeExpr action = (CodeExpr)duplicator.VisitCodeExpr(moverTypeChecker.procToActionInfo[proc].thisAction);

-                        Implementation impl = new Implementation(Token.NoToken, duplicateProc.Name, proc.TypeParameters, proc.InParams, proc.OutParams, action.LocVars, action.Blocks);

+

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

+                        foreach (AssertCmd assertCmd in moverTypeChecker.procToActionInfo[proc].thisGate)

+                        {

+                            cmds.Add(new AssumeCmd(Token.NoToken, (Expr)duplicator.Visit(assertCmd.Expr)));

+                        }

+                        Block newInitBlock = new Block(Token.NoToken, "_init", cmds, 

+                            new GotoCmd(Token.NoToken, new List<string>(new string[] { action.Blocks[0].Label }), 

+                                                       new List<Block>(new Block[] { action.Blocks[0] })));

+                        List<Block> newBlocks = new List<Block>();

+                        newBlocks.Add(newInitBlock);

+                        newBlocks.AddRange(action.Blocks);

+                        Implementation impl = new Implementation(Token.NoToken, duplicateProc.Name, proc.TypeParameters, proc.InParams, proc.OutParams, action.LocVars, newBlocks);

                         impl.Proc = duplicateProc;

                         impl.Proc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));

                         impl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));

diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs
index 5a15c707..5a8c81f6 100644
--- a/Source/Concurrency/TypeCheck.cs
+++ b/Source/Concurrency/TypeCheck.cs
@@ -84,7 +84,7 @@ namespace Microsoft.Boogie
                 AssertCmd assertCmd = cmds[i] as AssertCmd;

                 if (assertCmd == null) break;

                 thisGate.Add(assertCmd);

-                cmds[i] = new AssumeCmd(assertCmd.tok, assertCmd.Expr);

+                cmds[i] = new AssumeCmd(assertCmd.tok, Expr.True);

             }

 

             Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();