added more information to assert messages

2 files changed, 57 insertions, 22 deletions

diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs
index 75e1f7e3..e8b7fa3c 100644
--- a/Source/Concurrency/MoverCheck.cs
+++ b/Source/Concurrency/MoverCheck.cs
@@ -416,7 +416,9 @@ namespace Microsoft.Boogie
             List<Requires> requires = DisjointnessRequires(program, first, second);

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

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

-            ensures.Add(new Ensures(false, transitionRelation));

+            Ensures ensureCheck = new Ensures(false, transitionRelation);

+            ensureCheck.ErrorData = string.Format("Commutativity check between {0} and {1} failed", first.proc.Name, second.proc.Name);

+            ensures.Add(ensureCheck);

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

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

             program.GlobalVariables().Iter(x => globalVars.Add(new IdentifierExpr(Token.NoToken, x)));

@@ -450,7 +452,9 @@ namespace Microsoft.Boogie
             foreach (AssertCmd assertCmd in first.thatGate)

             {

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

-                ensures.Add(new Ensures(false, assertCmd.Expr));

+                Ensures ensureCheck = new Ensures(assertCmd.tok, false, assertCmd.Expr, null);

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

+                ensures.Add(ensureCheck);

             }

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

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

@@ -487,7 +491,9 @@ namespace Microsoft.Boogie
             requires.Add(new Requires(false, failureExpr));

 

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

-            ensures.Add(new Ensures(false, failureExpr));

+            Ensures ensureCheck = new Ensures(false, failureExpr);

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

+            ensures.Add(ensureCheck);

 

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

             outputs.AddRange(first.thatOutParams);

@@ -565,7 +571,10 @@ namespace Microsoft.Boogie
                 ensuresExpr = new ExistsExpr(Token.NoToken, boundVars, ensuresExpr);

             }

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

-            ensures.Add(new Ensures(false, ensuresExpr));

+            Ensures ensureCheck = new Ensures(false, ensuresExpr);

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

+            ensures.Add(ensureCheck);

+

             List<Block> blocks = new List<Block>();

             blocks.Add(new Block(Token.NoToken, "L", new List<Cmd>(), new ReturnCmd(Token.NoToken)));

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

diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs
index 0fdb01e6..c190ec08 100644
--- a/Source/Concurrency/OwickiGries.cs
+++ b/Source/Concurrency/OwickiGries.cs
@@ -266,7 +266,7 @@ namespace Microsoft.Boogie
             return linearTypeChecker.availableLinearVars[absyMap[absy]];

         }

 

-        private void AddCallToYieldProc(List<Cmd> newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar)

+        private void AddCallToYieldProc(IToken tok, List<Cmd> newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar)

         {

             List<Expr> exprSeq = new List<Expr>();

             foreach (string domainName in linearTypeChecker.linearDomains.Keys)

@@ -302,12 +302,15 @@ namespace Microsoft.Boogie
             {

                 Expr bb = OldEqualityExpr(ogOldGlobalMap);

 

-                // assert pc ==> o_old == o && g_old == g;

-                newCmds.Add(new AssertCmd(Token.NoToken, Expr.Imp(Expr.Ident(pc), bb)));

-

                 // assert (o_old == o && g_old == g) || beta(i, g_old, o, g);

-                AssertCmd betaAssertCmd = new AssertCmd(Token.NoToken, Expr.Or(bb, beta));

-                newCmds.Add(betaAssertCmd);

+                AssertCmd skipOrBetaAssertCmd = new AssertCmd(tok, Expr.Or(bb, beta));

+                skipOrBetaAssertCmd.ErrorData = "Transition invariant in initial state violated";

+                newCmds.Add(skipOrBetaAssertCmd);

+

+                // assert pc ==> o_old == o && g_old == g;

+                AssertCmd skipAssertCmd = new AssertCmd(tok, Expr.Imp(Expr.Ident(pc), bb));

+                skipAssertCmd.ErrorData = "Transition invariant in final state violated"; ;

+                newCmds.Add(skipAssertCmd);

 

                 // pc, ok := ite(o_old == o && g_old == g, pc, true), ok || beta(i, g_old, o, g);

                 List<Expr> iteArgs = new List<Expr>(new Expr[] { bb, Expr.Ident(pc), Expr.True });

@@ -385,7 +388,7 @@ namespace Microsoft.Boogie
 

         private void DesugarYield(YieldCmd yieldCmd, List<Cmd> cmds, List<Cmd> newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToInputVar, Dictionary<string, Variable> domainNameToLocalVar)

         {

-            AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar);

+            AddCallToYieldProc(yieldCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar);

 

             if (globalMods.Count > 0)

             {

@@ -544,9 +547,15 @@ namespace Microsoft.Boogie
             {

                 var newExpr = Substituter.ApplyReplacingOldExprs(subst, oldGlobalSubst, ensures.Condition);

                 if (ensures.Free)

+                {

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

+                }

                 else

-                    newCmds.Add(new AssertCmd(Token.NoToken, newExpr));

+                {

+                    AssertCmd assertCmd = new AssertCmd(ensures.tok, newExpr);

+                    assertCmd.ErrorData = "Backwards non-interference check failed";

+                    newCmds.Add(assertCmd);

+                }

             }

             newCmds.Add(new AssumeCmd(Token.NoToken, Expr.False));

             yieldCheckerBlock = new Block(Token.NoToken, "L", newCmds, new ReturnCmd(Token.NoToken));

@@ -641,9 +650,15 @@ 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, predCmd.Attributes));

+                    {

+                        AssertCmd assertCmd = new AssertCmd(predCmd.tok, newExpr, predCmd.Attributes);

+                        assertCmd.ErrorData = "Non-interference check failed";

+                        newCmds.Add(assertCmd);

+                    }

                     else

+                    {

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

+                    }

                 }

                 newCmds.Add(new AssumeCmd(Token.NoToken, Expr.False));

                 yieldCheckerBlock = new Block(Token.NoToken, "L" + yieldCount++, newCmds, new ReturnCmd(Token.NoToken));

@@ -832,7 +847,7 @@ namespace Microsoft.Boogie
                         CallCmd callCmd = cmd as CallCmd; 

                         if (callCmd.IsAsync || QKeyValue.FindBoolAttribute(callCmd.Proc.Attributes, "yields"))

                         {

-                            AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar);

+                            AddCallToYieldProc(callCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar);

                         }

                         if (callCmd.IsAsync)

                         {

@@ -864,7 +879,7 @@ namespace Microsoft.Boogie
                     else if (cmd is ParCallCmd)

                     {

                         ParCallCmd parCallCmd = cmd as ParCallCmd;

-                        AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar);

+                        AddCallToYieldProc(parCallCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar);

                         DesugarParallelCallCmd(newCmds, parCallCmd);

                         HashSet<Variable> availableLinearVars = new HashSet<Variable>(AvailableLinearVars(parCallCmd));

                         foreach (CallCmd callCmd in parCallCmd.CallCmds)

@@ -894,10 +909,12 @@ namespace Microsoft.Boogie
                 }

                 if (b.TransferCmd is ReturnCmd && QKeyValue.FindBoolAttribute(impl.Proc.Attributes, "yields"))

                 {

-                    AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar);

+                    AddCallToYieldProc(b.TransferCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar);

                     if (pc != null)

                     {

-                        newCmds.Add(new AssertCmd(Token.NoToken, Expr.Ident(ok)));

+                        AssertCmd assertCmd = new AssertCmd(b.TransferCmd.tok, Expr.Ident(ok));

+                        assertCmd.ErrorData = "Failed to execute atomic action before procedure return";

+                        newCmds.Add(assertCmd);

                     }

                 }

                 b.Cmds = newCmds;

@@ -917,7 +934,7 @@ namespace Microsoft.Boogie
                 Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(AvailableLinearVars(header), domainNameToInputVar);

                 foreach (Block pred in header.Predecessors)

                 {

-                    AddCallToYieldProc(pred.Cmds, ogOldGlobalMap, domainNameToLocalVar);

+                    AddCallToYieldProc(header.tok, pred.Cmds, ogOldGlobalMap, domainNameToLocalVar);

                     if (pc != null && !graph.BackEdgeNodes(header).Contains(pred))

                     {

                         pred.Cmds.Add(new AssignCmd(Token.NoToken, new List<AssignLhs>(

@@ -929,8 +946,13 @@ namespace Microsoft.Boogie
                 List<Cmd> newCmds = new List<Cmd>();

                 if (pc != null)

                 {

-                    newCmds.Add(new AssertCmd(Token.NoToken, Expr.Eq(Expr.Ident(oldPc), Expr.Ident(pc))));

-                    newCmds.Add(new AssertCmd(Token.NoToken, Expr.Imp(Expr.Ident(oldOk), Expr.Ident(ok))));

+                    AssertCmd assertCmd;

+                    assertCmd = new AssertCmd(header.tok, Expr.Eq(Expr.Ident(oldPc), Expr.Ident(pc)));

+                    assertCmd.ErrorData = "Specification state must not change for transitions ending in loop headers";

+                    newCmds.Add(assertCmd);

+                    assertCmd = new AssertCmd(header.tok, Expr.Imp(Expr.Ident(oldOk), Expr.Ident(ok)));

+                    assertCmd.ErrorData = "Specification state must not change for transitions ending in loop headers";

+                    newCmds.Add(assertCmd);

                 } 

                 foreach (string domainName in linearTypeChecker.linearDomains.Keys)

                 {

@@ -1041,7 +1063,9 @@ namespace Microsoft.Boogie
                     }

                     else

                     {

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

+                        AssertCmd assertCmd = new AssertCmd(r.tok, r.Condition, r.Attributes);

+                        assertCmd.ErrorData = "Non-interference check failed";

+                        cmds.Add(assertCmd);

                     }

                 }

                 yields.Add(cmds);

@@ -1080,7 +1104,9 @@ namespace Microsoft.Boogie
                     }

                     else

                     {

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

+                        AssertCmd assertCmd = new AssertCmd(e.tok, e.Condition, e.Attributes);

+                        assertCmd.ErrorData = "Non-interference check failed";

+                        cmds.Add(assertCmd);

                     }

                 }

                 yields.Add(cmds);