CIVL: better refinement error messages (#312)

boogie-org · Dec 2, 2020 · 7934c32 · 7934c32
1 parent e88af75
commit 7934c32
Show file tree

Hide file tree

Showing 7 changed files with 67 additions and 57 deletions.
diff --git a/Source/Concurrency/RefinementInstrumentation.cs b/Source/Concurrency/RefinementInstrumentation.cs
@@ -27,12 +27,7 @@ public virtual List<Cmd> CreateReturnAssertCmds()
       return new List<Cmd>();
     }
 
-    public virtual List<Cmd> CreateUnchangedGlobalsAssertCmds()
-    {
-      return new List<Cmd>();
-    }
-
-    public virtual List<Cmd> CreateUnchangedOutputsAssertCmds()
+    public virtual List<Cmd> CreateUnchangedAssertCmds()
     {
       return new List<Cmd>();
     }
@@ -59,6 +54,7 @@ class ActionRefinementInstrumentation : RefinementInstrumentation
     private Expr gate;
     private Expr transitionRelation;
     private IToken tok;
+    private int layerNum;
 
     private Dictionary<AtomicAction, Expr> transitionRelationCache;
 
@@ -72,7 +68,7 @@ public ActionRefinementInstrumentation(
       this.tok = impl.tok;
       this.oldGlobalMap = new Dictionary<Variable, Variable>();
       ActionProc actionProc = civlTypeChecker.procToYieldingProc[originalImpl.Proc] as ActionProc;
-      int layerNum = actionProc.upperLayer;
+      this.layerNum = actionProc.upperLayer;
       foreach (Variable v in civlTypeChecker.GlobalVariables)
       {
         var layerRange = civlTypeChecker.GlobalVariableLayerRange(v);
@@ -173,14 +169,14 @@ public override List<Cmd> CreateAssertCmds()
       var skipOrTransitionRelationAssertCmd = CmdHelper.AssertCmd(
         tok,
         Expr.Or(Expr.Ident(pc), Expr.Or(OldEqualityExprForGlobals(), transitionRelation)),
-        "Transition invariant violated in initial state");
+        $"A yield-to-yield fragment modifies layer-{layerNum + 1} state in a way that does not match the refined atomic action");
       CivlUtil.ResolveAndTypecheck(skipOrTransitionRelationAssertCmd);
 
       // assert pc ==> g_old == g && o_old == o;
       AssertCmd skipAssertCmd = CmdHelper.AssertCmd(
         tok,
         Expr.Imp(Expr.Ident(pc), Expr.And(OldEqualityExprForGlobals(), OldEqualityExprForOutputs())),
-        "Transition invariant violated in final state");
+        $"A yield-to-yield fragment modifies layer-{layerNum + 1} state subsequent to a yield-to-yield fragment that already modified layer-{layerNum + 1} state");
       CivlUtil.ResolveAndTypecheck(skipAssertCmd);
 
       return new List<Cmd> {skipOrTransitionRelationAssertCmd, skipAssertCmd};
@@ -191,29 +187,26 @@ public override List<Cmd> CreateReturnAssertCmds()
       AssertCmd assertCmd = CmdHelper.AssertCmd(
         tok,
         Expr.Ident(ok),
-        "Failed to execute atomic action before procedure return");
+        "On some path no yield-to-yield fragment matched the refined atomic action");
       return new List<Cmd> {assertCmd};
     }
 
-    public override List<Cmd> CreateUnchangedGlobalsAssertCmds()
+    public override List<Cmd> CreateUnchangedAssertCmds()
     {
-      AssertCmd skipAssertCmd = CmdHelper.AssertCmd(
+      AssertCmd globalsAssertCmd = CmdHelper.AssertCmd(
         tok,
         Expr.And(this.oldGlobalMap.Select(kvPair => Expr.Eq(Expr.Ident(kvPair.Key), Expr.Ident(kvPair.Value)))),
-        "Globals must not be modified");
-      CivlUtil.ResolveAndTypecheck(skipAssertCmd);
-      return new List<Cmd> {skipAssertCmd};
-    }
+        $"A yield-to-yield fragment illegally modifies layer-{layerNum + 1} globals");
+      CivlUtil.ResolveAndTypecheck(globalsAssertCmd);
 
-    public override List<Cmd> CreateUnchangedOutputsAssertCmds()
-    {
       // assert pc ==> o_old == o;
-      AssertCmd skipAssertCmd = CmdHelper.AssertCmd(
+      AssertCmd outputsAssertCmd = CmdHelper.AssertCmd(
         tok,
         Expr.Imp(Expr.Ident(pc), OldEqualityExprForOutputs()),
-        "Outputs must not be modified");
-      CivlUtil.ResolveAndTypecheck(skipAssertCmd);
-      return new List<Cmd> {skipAssertCmd};
+        $"A yield-to-yield fragment illegally modifies layer-{layerNum + 1} outputs");
+      CivlUtil.ResolveAndTypecheck(outputsAssertCmd);
+
+      return new List<Cmd> {globalsAssertCmd, outputsAssertCmd};
     }
 
     public override List<Cmd> CreateUpdatesToRefinementVars(bool isMarkedCall)
@@ -224,7 +217,7 @@ public override List<Cmd> CreateUpdatesToRefinementVars(bool isMarkedCall)
       {
         // assert !pc;
         // pc, ok := true, true;
-        cmds.Add(CmdHelper.AssertCmd(tok, Expr.Not(Expr.Ident(pc)), "Visible state changed before marked call"));
+        cmds.Add(CmdHelper.AssertCmd(tok, Expr.Not(Expr.Ident(pc)), $"Layer-{layerNum + 1} state modified before marked call"));
         var pcOkUpdateRHS = new List<Expr> {Expr.True, Expr.True};
         cmds.Add(CmdHelper.AssignCmd(pcOkUpdateLHS, pcOkUpdateRHS));
       }

diff --git a/Source/Concurrency/YieldingProcInstrumentation.cs b/Source/Concurrency/YieldingProcInstrumentation.cs
@@ -412,7 +412,7 @@ private void DesugarConcurrency(Implementation impl, List<Cmd> preconditions)
     {
       var noninterferenceCheckerBlock = CreateNoninterferenceCheckerBlock();
       var refinementCheckerBlock = CreateRefinementCheckerBlock();
-      var refinementCheckerForYieldingLoopsBlock = CreateRefinementCheckerBlockForYieldingLoops();
+      var unchangedCheckerBlock = CreateUnchangedCheckerBlock();
       var returnCheckerBlock = CreateReturnCheckerBlock();
       var returnBlock = BlockHelper.Block(civlTypeChecker.AddNamePrefix("UnifiedReturn"), new List<Cmd>());
       SplitBlocks(impl);
@@ -428,7 +428,7 @@ private void DesugarConcurrency(Implementation impl, List<Cmd> preconditions)
           AddEdge(gotoCmd, noninterferenceCheckerBlock);
           if (blocksInYieldingLoops.Contains(pred))
           {
-            AddEdge(gotoCmd, refinementCheckerForYieldingLoopsBlock);
+            AddEdge(gotoCmd, unchangedCheckerBlock);
           }
           else
           {
@@ -479,7 +479,7 @@ private void DesugarConcurrency(Implementation impl, List<Cmd> preconditions)
                     FixUpImplRefinementCheckingBlock(targetBlock,
                       IsCallMarked(callCmd)
                         ? returnCheckerBlock
-                        : refinementCheckerForYieldingLoopsBlock);
+                        : unchangedCheckerBlock);
                     targetBlocks.Add(targetBlock);
                     implRefinementCheckingBlocks.Add(targetBlock);
                   }
@@ -496,7 +496,7 @@ private void DesugarConcurrency(Implementation impl, List<Cmd> preconditions)
             AddEdge(gotoCmd, noninterferenceCheckerBlock);
             AddEdge(gotoCmd,
               blocksInYieldingLoops.Contains(b)
-                ? refinementCheckerForYieldingLoopsBlock
+                ? unchangedCheckerBlock
                 : refinementCheckerBlock);
           }
         }
@@ -526,7 +526,7 @@ private void DesugarConcurrency(Implementation impl, List<Cmd> preconditions)
 
       impl.Blocks.Add(noninterferenceCheckerBlock);
       impl.Blocks.Add(refinementCheckerBlock);
-      impl.Blocks.Add(refinementCheckerForYieldingLoopsBlock);
+      impl.Blocks.Add(unchangedCheckerBlock);
       impl.Blocks.Add(returnCheckerBlock);
       impl.Blocks.Add(returnBlock);
       impl.Blocks.AddRange(implRefinementCheckingBlocks);
@@ -614,13 +614,12 @@ private Block CreateRefinementCheckerBlock()
       return BlockHelper.Block(civlTypeChecker.AddNamePrefix("RefinementChecker"), newCmds);
     }
 
-    private Block CreateRefinementCheckerBlockForYieldingLoops()
+    private Block CreateUnchangedCheckerBlock()
     {
       var newCmds = new List<Cmd>();
-      newCmds.AddRange(refinementInstrumentation.CreateUnchangedGlobalsAssertCmds());
-      newCmds.AddRange(refinementInstrumentation.CreateUnchangedOutputsAssertCmds());
+      newCmds.AddRange(refinementInstrumentation.CreateUnchangedAssertCmds());
       newCmds.Add(CmdHelper.AssumeCmd(Expr.False));
-      return BlockHelper.Block(civlTypeChecker.AddNamePrefix("RefinementCheckerForYieldingLoops"), newCmds);
+      return BlockHelper.Block(civlTypeChecker.AddNamePrefix("UnchangedChecker"), newCmds);
     }
 
     private Block CreateReturnCheckerBlock()

diff --git a/Test/civl/parallel6.bpl.expect b/Test/civl/parallel6.bpl.expect
@@ -1,4 +1,4 @@
-parallel6.bpl(8,64): Error BP5001: Transition invariant violated in final state
+parallel6.bpl(8,64): Error BP5001: A yield-to-yield fragment modifies layer-2 state subsequent to a yield-to-yield fragment that already modified layer-2 state
 Execution trace:
     parallel6.bpl(10,5): anon0
     parallel6.bpl(28,7): inline$atomic_incr$0$anon0

diff --git a/Test/civl/pending-async-1.bpl.expect b/Test/civl/pending-async-1.bpl.expect
@@ -1,4 +1,4 @@
-pending-async-1.bpl(48,49): Error BP5001: Failed to execute atomic action before procedure return
+pending-async-1.bpl(48,49): Error BP5001: On some path no yield-to-yield fragment matched the refined atomic action
 Execution trace:
     pending-async-1.bpl(50,3): anon0
     pending-async-1.bpl(16,7): inline$B$0$anon0

diff --git a/Test/civl/r2.bpl.expect b/Test/civl/r2.bpl.expect
@@ -1,15 +1,15 @@
-r2.bpl(10,57): Error BP5001: Failed to execute atomic action before procedure return
+r2.bpl(10,57): Error BP5001: On some path no yield-to-yield fragment matched the refined atomic action
 Execution trace:
     r2.bpl(11,5): anon0
     (0,0): Civl_call_refinement_4
     r2.bpl(21,34): inline$atomic_nop$0$Return
     (0,0): Civl_ReturnChecker
-r2.bpl(10,57): Error BP5001: Globals must not be modified
+r2.bpl(10,57): Error BP5001: A yield-to-yield fragment illegally modifies layer-2 globals
 Execution trace:
     r2.bpl(11,5): anon0
     (0,0): Civl_call_refinement_3
     r2.bpl(17,7): inline$atomic_incr$0$anon0
     r2.bpl(14,34): inline$atomic_incr$0$Return
-    (0,0): Civl_RefinementCheckerForYieldingLoops
+    (0,0): Civl_UnchangedChecker
 
 Boogie program verifier finished with 1 verified, 2 errors
diff --git a/Test/civl/refinement.bpl b/Test/civl/refinement.bpl
@@ -7,15 +7,14 @@ procedure {:yields}{:layer 1}{:refines "INCR"} p ()
 {
   call incr(); // Refined action INCR occurred
   yield;
-  call incr(); // State changed again
-               // Error: Transition invariant in final state violated
+  call incr(); // Error: State changed again
 }
 
 procedure {:yields}{:layer 1}{:refines "INCR"} q ()
 {
-  call decr(); // State changed, but not according to INCR
-  yield;       // Error: Transition invariant in initial state violated
-  call incr();
+  call decr(); // Error: State changed, but not according to INCR
+  yield;
+  call incr(); // Error: State changed again
 }
 
 procedure {:yields}{:layer 1}{:refines "INCR"} r ()
@@ -33,7 +32,18 @@ procedure {:yields}{:layer 1}{:refines "INCR"} r ()
 
 procedure {:yields}{:layer 1}{:refines "INCR"} s ()
 {
-  // Error: Failed to execute atomic action before procedure return
+  // Error: Refined action INCR never occurs
+}
+
+procedure {:yields}{:layer 1}{:refines "INCR"} t ()
+{
+  call incr();
+  yield;
+  while (*)
+  invariant {:layer 1}{:yields} true;
+  {
+    call incr(); // Error: State change inside yielding loop
+  }
 }
 
 procedure {:both} {:layer 1,2} INCR ()

diff --git a/Test/civl/refinement.bpl.expect b/Test/civl/refinement.bpl.expect
@@ -1,25 +1,33 @@
-refinement.bpl(6,48): Error BP5001: Transition invariant violated in final state
+refinement.bpl(6,48): Error BP5001: A yield-to-yield fragment modifies layer-2 state subsequent to a yield-to-yield fragment that already modified layer-2 state
 Execution trace:
     refinement.bpl(8,3): anon0
-    refinement.bpl(42,5): inline$INCR$0$anon0
+    refinement.bpl(52,5): inline$INCR$0$anon0
     refinement.bpl(8,3): anon0_0
-    refinement.bpl(42,5): inline$INCR$1$anon0
+    refinement.bpl(52,5): inline$INCR$1$anon0
     (0,0): Civl_ReturnChecker
-refinement.bpl(14,48): Error BP5001: Transition invariant violated in initial state
+refinement.bpl(13,48): Error BP5001: A yield-to-yield fragment modifies layer-2 state in a way that does not match the refined atomic action
 Execution trace:
-    refinement.bpl(16,3): anon0
-    refinement.bpl(48,5): inline$DECR$0$anon0
+    refinement.bpl(15,3): anon0
+    refinement.bpl(58,5): inline$DECR$0$anon0
     (0,0): Civl_RefinementChecker
-refinement.bpl(14,48): Error BP5001: Transition invariant violated in final state
+refinement.bpl(13,48): Error BP5001: A yield-to-yield fragment modifies layer-2 state subsequent to a yield-to-yield fragment that already modified layer-2 state
 Execution trace:
-    refinement.bpl(16,3): anon0
-    refinement.bpl(48,5): inline$DECR$0$anon0
-    refinement.bpl(16,3): anon0_0
-    refinement.bpl(42,5): inline$INCR$0$anon0
+    refinement.bpl(15,3): anon0
+    refinement.bpl(58,5): inline$DECR$0$anon0
+    refinement.bpl(15,3): anon0_0
+    refinement.bpl(52,5): inline$INCR$0$anon0
     (0,0): Civl_ReturnChecker
-refinement.bpl(34,48): Error BP5001: Failed to execute atomic action before procedure return
+refinement.bpl(33,48): Error BP5001: On some path no yield-to-yield fragment matched the refined atomic action
 Execution trace:
-    refinement.bpl(37,1): anon0
+    refinement.bpl(36,1): anon0
     (0,0): Civl_ReturnChecker
+refinement.bpl(38,48): Error BP5001: A yield-to-yield fragment illegally modifies layer-2 globals
+Execution trace:
+    refinement.bpl(40,3): anon0
+    refinement.bpl(52,5): inline$INCR$0$anon0
+    refinement.bpl(40,3): anon0_0
+    refinement.bpl(42,3): anon2_LoopHead
+    refinement.bpl(52,5): inline$INCR$1$anon0
+    (0,0): Civl_UnchangedChecker
 
-Boogie program verifier finished with 3 verified, 4 errors
+Boogie program verifier finished with 3 verified, 5 errors