[Civl] Fixed bug in refinement check for actions (#853)

The refinement check for actions was handling the frame condition correctly. Now the frame condition is handled in the same manner as the refinement check for procedures. Co-authored-by: Shaz Qadeer <[email protected]>
boogie-org · Mar 1, 2024 · d7b1041 · d7b1041
1 parent 9ae690e
commit d7b1041
Show file tree

Hide file tree

Showing 8 changed files with 69 additions and 12 deletions.
diff --git a/Source/Concurrency/CivlCoreTypes.cs b/Source/Concurrency/CivlCoreTypes.cs
@@ -74,8 +74,6 @@ public Action(CivlTypeChecker civlTypeChecker, ActionDecl actionDecl, Action ref
 
     public LayerRange LayerRange => ActionDecl.LayerRange;
 
-    public int LowerLayer => LayerRange.LowerLayer;
-
     public IEnumerable<ActionDecl> PendingAsyncs => ActionDecl.CreateActionDecls;
 
     public bool HasPendingAsyncs => PendingAsyncs.Any();

diff --git a/Source/Concurrency/CivlTypeChecker.cs b/Source/Concurrency/CivlTypeChecker.cs
@@ -462,6 +462,11 @@ private void MatchFormals(List<Variable> formals1, List<Variable> formals2, stri
 
     public IEnumerable<Variable> GlobalVariables => program.GlobalVariables;
 
+    public IEnumerable<Variable> GlobalVariablesAtLayer(int layerNum)
+    {
+      return GlobalVariables.Where(v => v.LayerRange.LowerLayer <= layerNum && layerNum < v.LayerRange.UpperLayer);
+    }
+
     public IEnumerable<Action> MoverActions => actionDeclToAction.Keys
       .Where(actionDecl => actionDecl.HasMoverType).Select(actionDecl => actionDeclToAction[actionDecl]);
 

diff --git a/Source/Concurrency/InductiveSequentialization.cs b/Source/Concurrency/InductiveSequentialization.cs
@@ -90,10 +90,11 @@ public InlineSequentialization(CivlTypeChecker civlTypeChecker, Action targetAct
       }
       var subst = Substituter.SubstitutionFromDictionary(map);
       inlinedImpl.Proc.Requires = refinedAction.Gate.Select(g => new Requires(false, Substituter.Apply(subst, g.Expr))).ToList();
+      var frame = new HashSet<Variable>(civlTypeChecker.GlobalVariablesAtLayer(targetAction.LayerRange.UpperLayer));
       inlinedImpl.Proc.Ensures = new List<Ensures>(new[]
       {
-        new Ensures(false, Substituter.Apply(subst, refinedAction.GetTransitionRelation(civlTypeChecker, inlinedImpl.Proc.ModifiedVars.ToHashSet())),
-          $"Refinement check of {targetAction.Name} failed")
+        new Ensures(false, Substituter.Apply(subst, refinedAction.GetTransitionRelation(civlTypeChecker, frame)))
+          { Description = new FailureOnlyDescription($"Refinement check of {targetAction.Name} failed") }
       });
     }
 
@@ -245,7 +246,7 @@ private List<Declaration> GenerateConclusionChecker()
       cmds.Add(CmdHelper.CallCmd(invariantAction.Impl.Proc, invariantAction.Impl.InParams,
         invariantAction.Impl.OutParams));
       cmds.Add(CmdHelper.AssumeCmd(NoPendingAsyncs));
-      var frame = new HashSet<Variable>(refinedAction.ModifiedGlobalVars);
+      var frame = new HashSet<Variable>(civlTypeChecker.GlobalVariablesAtLayer(targetAction.LayerRange.UpperLayer));
       cmds.Add(GetCheck(targetAction.tok, Substituter.Apply(subst, refinedAction.GetTransitionRelation(civlTypeChecker, frame)),
         $"IS conclusion of {targetAction.Name} failed"));
 

diff --git a/Source/Concurrency/RefinementInstrumentation.cs b/Source/Concurrency/RefinementInstrumentation.cs
@@ -74,15 +74,10 @@ public ActionRefinementInstrumentation(
       this.tok = impl.tok;
       this.oldGlobalMap = new Dictionary<Variable, Variable>();
       var yieldProcedureDecl = (YieldProcedureDecl)originalImpl.Proc;
-      //ActionProc actionProc = civlTypeChecker.procToYieldingProc[originalImpl.Proc] as ActionProc;
       this.layerNum = yieldProcedureDecl.Layer;
-      foreach (Variable v in civlTypeChecker.GlobalVariables)
+      foreach (Variable v in civlTypeChecker.GlobalVariablesAtLayer(layerNum))
       {
-        var layerRange = v.LayerRange;
-        if (layerRange.LowerLayer <= layerNum && layerNum < layerRange.UpperLayer)
-        {
-          this.oldGlobalMap[v] = oldGlobalMap[v];
-        }
+        this.oldGlobalMap[v] = oldGlobalMap[v];
       }
 
       this.newLocalVars = new List<Variable>();

diff --git a/Test/civl/async/simple-fail.bpl b/Test/civl/async/simple-fail.bpl
@@ -0,0 +1,25 @@
+// RUN: %parallel-boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+var {:layer 0,2} x: int;
+var {:layer 0,2} y: int;
+
+atomic action {:layer 1} A()
+modifies x, y;
+refines B;
+{
+    x := x + 1;
+    call X();
+}
+
+action {:layer 1} X()
+modifies y;
+{
+    y := y + 1;
+}
+
+atomic action {:layer 2} B()
+modifies x;
+{
+    havoc x;
+}
diff --git a/Test/civl/async/simple-fail.bpl.expect b/Test/civl/async/simple-fail.bpl.expect
@@ -0,0 +1,6 @@
+simple-fail.bpl(13,1): Error: a postcondition could not be proved on this return path
+(0,0): Related location: Refinement check of A failed
+Execution trace:
+    simple-fail.bpl(11,7): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/civl/async/simple.bpl b/Test/civl/async/simple.bpl
@@ -0,0 +1,25 @@
+// RUN: %parallel-boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+var {:layer 0,2} x: int;
+var {:layer 0,1} y: int;
+
+atomic action {:layer 1} A()
+modifies x, y;
+refines B;
+{
+    x := x + 1;
+    call X();
+}
+
+action {:layer 1} X()
+modifies y;
+{
+    y := y + 1;
+}
+
+atomic action {:layer 2} B()
+modifies x;
+{
+    havoc x;
+}
diff --git a/Test/civl/async/simple.bpl.expect b/Test/civl/async/simple.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors