[Civl] Add support for preconditions to actions (#872)

This PR adds preconditions to actions for the purpose of providing extra
contextual information in left mover checks for inductive
sequentialization. These preconditions are proved to be
interference-free just like other preconditions. Their initiation is
established by the IS invariant during the step condition check for the
action being moved left. As a result of this enhancement, the use of
abstractions (and the eliminates clause) is eliminated from Civl
benchmarks, the strengthening achieved by the extra gates of the
abstractions now achieved by the preconditions.

The intention is to eliminate abstractions and the eliminates clause
from Civl. But that will be done in a separate PR.

---------

Co-authored-by: Shaz Qadeer <[email protected]>

Source/Concurrency/CivlTypeChecker.cs

@@ -24,9 +24,13 @@ public CivlTypeChecker(ConcurrencyOptions options, Program program)
       this.program = program;
       this.Options = options;
       this.linearTypeChecker = new LinearTypeChecker(this);
-      this.AllRefinementLayers = program.TopLevelDeclarations.OfType<Implementation>()
+      var yieldingProcRefinementLayers = program.TopLevelDeclarations.OfType<Implementation>()
         .Where(impl => impl.Proc is YieldProcedureDecl)
-        .Select(decl => ((YieldProcedureDecl)decl.Proc).Layer)
+        .Select(decl => ((YieldProcedureDecl)decl.Proc).Layer);
+      var actionRefinementLayers = program.TopLevelDeclarations.OfType<ActionDecl>()
+        .Where(actionDecl => actionDecl.RefinedAction != null)
+        .Select(actionDecl => actionDecl.LayerRange.UpperLayer);
+      this.AllRefinementLayers = yieldingProcRefinementLayers.Union(actionRefinementLayers)
         .OrderBy(layer => layer).Distinct().ToList();
 
       this.actionDeclToAction = new Dictionary<ActionDecl, Action>();
@@ -48,7 +52,7 @@ public CivlTypeChecker(ConcurrencyOptions options, Program program)
       }
 
       SkipActionDecl = new ActionDecl(Token.NoToken, AddNamePrefix("Skip"), MoverType.Both, new List<Variable>(),
-        new List<Variable>(), true, new List<ActionDeclRef>(), null, null, new List<ElimDecl>(),
+        new List<Variable>(), true, new List<ActionDeclRef>(), null, null, new List<ElimDecl>(), new List<Requires>(), new List<CallCmd>(),
         new List<IdentifierExpr>(), null, null);
       var skipImplementation = DeclHelper.Implementation(
         SkipActionDecl,

Source/Concurrency/InductiveSequentialization.cs

@@ -28,10 +28,33 @@ protected Sequentialization(CivlTypeChecker civlTypeChecker, Action targetAction
 
     protected abstract List<Declaration> GenerateCheckers();
 
-    public virtual Expr GenerateMoverCheckAssumption(Action action, List<Variable> actionArgs, Action leftMover,
+    public virtual IEnumerable<Expr> GenerateMoverCheckAssumptions(Action action, List<Variable> actionArgs, Action leftMover,
       List<Variable> leftMoverArgs)
     {
-      return Expr.True;
+      return new List<Expr>();
+    }
+
+    public IEnumerable<AssertCmd> Preconditions(Action pendingAsync, Substitution subst)
+    {
+      var cmds = new List<AssertCmd>();
+      pendingAsync.ActionDecl.Requires.Where(req => req.Layers.Contains(Layer)).ForEach(req =>
+      {
+        cmds.Add(CmdHelper.AssertCmd(req.tok, Substituter.Apply(subst, req.Condition), ""));
+      });
+      foreach (var callCmd in pendingAsync.ActionDecl.YieldRequires)
+      {
+        var yieldInvariant = (YieldInvariantDecl)callCmd.Proc;
+        if (Layer == yieldInvariant.Layer)
+        {
+          Substitution callFormalsToActuals = Substituter.SubstitutionFromDictionary(yieldInvariant.InParams
+              .Zip(callCmd.Ins)
+              .ToDictionary(x => x.Item1, x => x.Item2));
+          yieldInvariant.Requires.ForEach(req =>
+            cmds.Add(CmdHelper.AssertCmd(req.tok,
+                  Substituter.Apply(subst, Substituter.Apply(callFormalsToActuals, req.Condition)), "")));
+        }
+      }
+      return cmds;
     }
 
     public static void AddCheckers(CivlTypeChecker civlTypeChecker, List<Declaration> decls)
@@ -269,17 +292,14 @@ private List<Declaration> GenerateStepChecker(Action pendingAsync)
       cmds.Add(RemoveChoice(pendingAsyncType));
 
       Action abs = elim[pendingAsync];
-      Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
       List<Expr> inputExprs = new List<Expr>();
       for (int i = 0; i < abs.Impl.InParams.Count; i++)
       {
-        var pendingAsyncParam = ExprHelper.FieldAccess(Choice(pendingAsyncType), pendingAsyncCtor.InParams[i].Name);
-        map[abs.Impl.InParams[i]] = pendingAsyncParam;
-        inputExprs.Add(pendingAsyncParam);
+        inputExprs.Add(ExprHelper.FieldAccess(Choice(pendingAsyncType), pendingAsyncCtor.InParams[i].Name));
       }
-      var subst = Substituter.SubstitutionFromDictionary(map);
-      cmds.AddRange(abs.GetGateAsserts(subst,
+      cmds.AddRange(abs.GetGateAsserts(Substituter.SubstitutionFromDictionary(abs.Impl.InParams.Zip(inputExprs).ToDictionary(x => x.Item1, x => x.Item2)),
         $"Gate of {abs.Name} fails in IS induction step for invariant {invariantAction.Name}"));
+      cmds.AddRange(Preconditions(abs, Substituter.SubstitutionFromDictionary(abs.ActionDecl.InParams.Zip(inputExprs).ToDictionary(x => x.Item1, x => x.Item2))));
 
       List<IdentifierExpr> outputExprs = new List<IdentifierExpr>();
       if (abs.HasPendingAsyncs)
@@ -325,7 +345,7 @@ private List<Declaration> GenerateStepChecker(Action pendingAsync)
      *   (1) the permissions in the invocation are disjoint from the permissions in the invariant invocation, or
      *   (2) the permissions in the invocation is contained in the permissions of one of the pending asyncs created by the invariant invocation.
      */
-    public override Expr GenerateMoverCheckAssumption(Action action, List<Variable> actionArgs, Action leftMover,
+    public override IEnumerable<Expr> GenerateMoverCheckAssumptions(Action action, List<Variable> actionArgs, Action leftMover,
       List<Variable> leftMoverArgs)
     {
       var invariantFormalMap =
@@ -336,13 +356,20 @@ public override Expr GenerateMoverCheckAssumption(Action action, List<Variable>
       var invariantTransitionRelationExpr = ExprHelper.FunctionCall(invariantAction.InputOutputRelationWithChoice,
         invariantAction.ImplWithChoice.InParams.Concat(invariantAction.ImplWithChoice.OutParams)
           .Select(v => invariantFormalMap[v]).ToList());
-      return ExprHelper.ExistsExpr(
+
+      Substitution subst = Substituter.SubstitutionFromDictionary(
+        leftMover.ActionDecl.InParams.Zip(leftMoverArgs.Select(x => (Expr)Expr.Ident(x))).ToDictionary(x => x.Item1, x => x.Item2));
+
+      return new List<Expr>(Preconditions(leftMover, subst).Select(assertCmd => assertCmd.Expr))
+      {
+        ExprHelper.ExistsExpr(
         invariantFormalMap.Values.OfType<IdentifierExpr>().Select(ie => ie.Decl).ToList(),
         Expr.And(new[]
         {
           invariantTransitionRelationExpr, ActionExpr(action, actionArgs, invariantFormalSubst),
           LeftMoverExpr(leftMover, leftMoverArgs, invariantFormalSubst)
-        }));
+        }))
+      };
     }
 
     private Expr ActionExpr(Action action, List<Variable> actionArgs, Substitution invariantFormalSubst)