From d7b10418d96d478ee07e42750cba028a36d3c962 Mon Sep 17 00:00:00 2001
From: Shaz Qadeer <shaz.qadeer@gmail.com>
Date: Fri, 1 Mar 2024 13:04:24 -0800
Subject: [PATCH] [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 <shaz@meta.com>
---
 Source/Concurrency/CivlCoreTypes.cs           |  2 --
 Source/Concurrency/CivlTypeChecker.cs         |  5 ++++
 .../Concurrency/InductiveSequentialization.cs |  7 +++---
 .../Concurrency/RefinementInstrumentation.cs  |  9 ++-----
 Test/civl/async/simple-fail.bpl               | 25 +++++++++++++++++++
 Test/civl/async/simple-fail.bpl.expect        |  6 +++++
 Test/civl/async/simple.bpl                    | 25 +++++++++++++++++++
 Test/civl/async/simple.bpl.expect             |  2 ++
 8 files changed, 69 insertions(+), 12 deletions(-)
 create mode 100644 Test/civl/async/simple-fail.bpl
 create mode 100644 Test/civl/async/simple-fail.bpl.expect
 create mode 100644 Test/civl/async/simple.bpl
 create mode 100644 Test/civl/async/simple.bpl.expect

diff --git a/Source/Concurrency/CivlCoreTypes.cs b/Source/Concurrency/CivlCoreTypes.cs
index 1de8518fe..8e227220b 100644
--- 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
index b554a80b6..8e43c87af 100644
--- 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
index 457910ead..2664205a8 100644
--- 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
index 07c3f55c4..e0d37ecdb 100644
--- 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
new file mode 100644
index 000000000..5d55236b5
--- /dev/null
+++ 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;
+}
\ No newline at end of file
diff --git a/Test/civl/async/simple-fail.bpl.expect b/Test/civl/async/simple-fail.bpl.expect
new file mode 100644
index 000000000..2574ed7ee
--- /dev/null
+++ 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
new file mode 100644
index 000000000..755f30e48
--- /dev/null
+++ 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;
+}
\ No newline at end of file
diff --git a/Test/civl/async/simple.bpl.expect b/Test/civl/async/simple.bpl.expect
new file mode 100644
index 000000000..37fad75c9
--- /dev/null
+++ b/Test/civl/async/simple.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors