[Civl] Remove pending asyncs and inductive sequentialization (#1091)

This PR removes the implementation of pending asyncs and inductive
sequentialization from Civl. The only aspect that remains is the notion
of action refinement.

Author: shazqadeer

Source/Concurrency/ActionRefinement.cs

@@ -0,0 +1,70 @@
+using System.Collections.Generic;
+using System.Linq;
+
+namespace Microsoft.Boogie
+{
+  public class ActionRefinement
+  {
+    private CivlTypeChecker civlTypeChecker;
+    private Action targetAction;
+    private Implementation inlinedImpl;
+
+    public static void AddCheckers(CivlTypeChecker civlTypeChecker, List<Declaration> decls)
+    {
+      foreach (var x in civlTypeChecker.ActionRefinements)
+      {
+        decls.AddRange([x.inlinedImpl, x.inlinedImpl.Proc]);
+      }
+    }
+
+    public ActionRefinement(CivlTypeChecker civlTypeChecker, Action targetAction)
+    {
+      this.civlTypeChecker = civlTypeChecker;
+      this.targetAction = targetAction;
+      inlinedImpl = CreateInlinedImplementation();
+      var refinedAction = targetAction.RefinedAction;
+      Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
+      for (int i = 0; i < refinedAction.Impl.InParams.Count; i++)
+      {
+        map[refinedAction.Impl.InParams[i]] = Expr.Ident(inlinedImpl.Proc.InParams[i]);
+      }
+      for (int i = 0; i < refinedAction.Impl.OutParams.Count; i++)
+      {
+        map[refinedAction.Impl.OutParams[i]] = Expr.Ident(inlinedImpl.Proc.OutParams[i]);
+      }
+      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, frame)))
+          { Description = new FailureOnlyDescription($"Refinement check of {targetAction.Name} failed") }
+      });
+    }
+
+    private Implementation CreateInlinedImplementation()
+    {
+      var decls = new List<Declaration>();
+      var inlinedImpl = Action.CreateDuplicateImplementation(targetAction.ActionDecl.Impl,
+        $"{targetAction.ActionDecl.Name}_RefinementCheck");
+      CivlAttributes.RemoveAttributes(inlinedImpl.Proc, new HashSet<string> { "inline" });
+      decls.Add(inlinedImpl);
+      decls.Add(inlinedImpl.Proc);
+      var oldTopLevelDeclarations = new List<Declaration>(civlTypeChecker.program.TopLevelDeclarations);
+      civlTypeChecker.program.AddTopLevelDeclarations(decls);
+      decls.OfType<Implementation>().ForEach(impl =>
+      {
+        impl.OriginalBlocks = impl.Blocks;
+        impl.OriginalLocVars = impl.LocVars;
+      });
+      Inliner.ProcessImplementation(civlTypeChecker.Options, civlTypeChecker.program, inlinedImpl);
+      civlTypeChecker.program.TopLevelDeclarations = oldTopLevelDeclarations;
+      decls.OfType<Implementation>().ForEach(impl =>
+      {
+        impl.OriginalBlocks = null;
+        impl.OriginalLocVars = null;
+      });
+      return inlinedImpl;
+    }
+  }
+}

Source/Concurrency/CivlCoreTypes.cs

@@ -1,5 +1,4 @@
 using System.Collections.Generic;
-using System.Diagnostics;
 using System.Linq;
 
 namespace Microsoft.Boogie
@@ -20,36 +19,12 @@ public class Action
     public List<AssertCmd> SecondGate;
     public Implementation SecondImpl;
     public Dictionary<Variable, Function> TriggerFunctions;
-    
-    public DatatypeTypeCtorDecl ChoiceDatatypeTypeCtorDecl;
-    public Implementation ImplWithChoice;
-    public Function InputOutputRelationWithChoice;
 
-    public Action(CivlTypeChecker civlTypeChecker, ActionDecl actionDecl, Action refinedAction, bool isInvariant)
+    public Action(CivlTypeChecker civlTypeChecker, ActionDecl actionDecl, Action refinedAction)
     {
       ActionDecl = actionDecl;
       RefinedAction = refinedAction;
       Impl = CreateDuplicateImplementation(actionDecl.Impl, actionDecl.Name);
-      if (PendingAsyncs.Any())
-      {
-        DesugarCreateAsyncs(civlTypeChecker, Impl, ActionDecl);
-        if (isInvariant)
-        {
-          ImplWithChoice = CreateDuplicateImplementation(Impl, $"{Name}_With_Choice");
-          var choiceDatatypeName = $"Choice_{Name}";
-          ChoiceDatatypeTypeCtorDecl =
-            new DatatypeTypeCtorDecl(Token.NoToken, choiceDatatypeName, new List<TypeVariable>(), null);
-          PendingAsyncs.ForEach(elim =>
-          {
-            var field = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, elim.Name, elim.PendingAsyncType), true);
-            ChoiceDatatypeTypeCtorDecl.AddConstructor(Token.NoToken, $"{choiceDatatypeName}_{elim.Name}",
-              new List<Variable>() { field });
-          });
-          civlTypeChecker.program.AddTopLevelDeclaration(ChoiceDatatypeTypeCtorDecl);
-          DesugarSetChoice(civlTypeChecker, ImplWithChoice);
-        }
-        DropSetChoice(Impl);
-      }
 
       AddGateSufficiencyCheckerAndHoistAsserts(civlTypeChecker);
 
@@ -58,10 +33,6 @@ public Action(CivlTypeChecker civlTypeChecker, ActionDecl actionDecl, Action ref
       UsedGlobalVarsInAction = new HashSet<Variable>(VariableCollector.Collect(Impl).Where(x => x is GlobalVariable));
 
       InputOutputRelation = ComputeInputOutputRelation(civlTypeChecker, Impl);
-      if (ImplWithChoice != null)
-      {
-        InputOutputRelationWithChoice = ComputeInputOutputRelation(civlTypeChecker, ImplWithChoice);
-      }
 
       AtomicActionDuplicator.SetupCopy(this, ref FirstGate, ref FirstImpl, "first_");
       AtomicActionDuplicator.SetupCopy(this, ref SecondGate, ref SecondImpl, "second_");
@@ -76,10 +47,6 @@ public Action(CivlTypeChecker civlTypeChecker, ActionDecl actionDecl, Action ref
 
     public LayerRange LayerRange => ActionDecl.LayerRange;
 
-    public IEnumerable<ActionDecl> PendingAsyncs => ActionDecl.CreateActionDecls;
-    
-    public bool HasPendingAsyncs => PendingAsyncs.Any();
-
     public bool IsRightMover => ActionDecl.MoverType == MoverType.Right || ActionDecl.MoverType == MoverType.Both;
 
     public bool IsLeftMover => ActionDecl.MoverType == MoverType.Left || ActionDecl.MoverType == MoverType.Both;
@@ -88,27 +55,14 @@ public Action(CivlTypeChecker civlTypeChecker, ActionDecl actionDecl, Action ref
 
     public bool IsUnconditionalLeftMover => IsLeftMover && !ActionDecl.HasPreconditions;
 
-    public int PendingAsyncStartIndex => ActionDecl.OutParams.Count;
-
     public bool TriviallyCommutesWith(Action other)
     {
       return !this.ModifiedGlobalVars.Intersect(other.UsedGlobalVarsInAction).Any() &&
              !this.UsedGlobalVarsInAction.Intersect(other.ModifiedGlobalVars).Any();
     }
 
-    public Variable PAs(CtorType pendingAsyncType)
-    {
-      var pendingAsyncMultisetType = TypeHelper.MapType(pendingAsyncType, Type.Int);
-      return Impl.OutParams.Skip(PendingAsyncStartIndex).First(v => v.TypedIdent.Type.Equals(pendingAsyncMultisetType));
-    }
-
     public bool HasAssumeCmd => Impl.Blocks.Any(b => b.Cmds.Any(c => c is AssumeCmd));
 
-    public DatatypeConstructor ChoiceConstructor(CtorType pendingAsyncType)
-    {
-      return ChoiceDatatypeTypeCtorDecl.Constructors.First(x => x.InParams[0].TypedIdent.Type.Equals(pendingAsyncType));
-    }
-
     public IEnumerable<AssertCmd> GetGateAsserts(Substitution subst, string msg)
     {
       foreach (var gate in Gate)
@@ -124,30 +78,6 @@ public Expr GetTransitionRelation(CivlTypeChecker civlTypeChecker, HashSet<Varia
       return TransitionRelationComputation.Refinement(civlTypeChecker, Impl, frame);
     }
 
-    public Substitution GetSubstitution(Action to)
-    {
-      Debug.Assert(PendingAsyncStartIndex == to.PendingAsyncStartIndex);
-      Debug.Assert(Impl.InParams.Count == to.Impl.InParams.Count);
-      Debug.Assert(Impl.OutParams.Count <= to.Impl.OutParams.Count);
-
-      Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
-      for (int i = 0; i < Impl.InParams.Count; i++)
-      {
-        map[Impl.InParams[i]] = Expr.Ident(to.Impl.InParams[i]);
-      }
-      for (int i = 0; i < PendingAsyncStartIndex; i++)
-      {
-        map[Impl.OutParams[i]] = Expr.Ident(to.Impl.OutParams[i]);
-      }
-      for (int i = PendingAsyncStartIndex; i < Impl.OutParams.Count; i++)
-      {
-        var formal = Impl.OutParams[i];
-        var pendingAsyncType = (CtorType)((MapType)formal.TypedIdent.Type).Arguments[0];
-        map[formal] = Expr.Ident(to.PAs(pendingAsyncType));
-      }
-      return Substituter.SubstitutionFromDictionary(map);
-    }
-
     public IEnumerable<AssertCmd> Preconditions(int layerNum, Substitution subst)
     {
       var errorMessage = $"this precondition of {Name} could not be proved";
@@ -265,133 +195,6 @@ private Function ComputeInputOutputRelation(CivlTypeChecker civlTypeChecker, Imp
       CivlUtil.ResolveAndTypecheck(civlTypeChecker.Options, inputOutputRelation.Body);
       return inputOutputRelation;
     }
-
-    public static void DesugarCreateAsyncs(CivlTypeChecker civlTypeChecker, Implementation impl, ActionDecl actionDecl)
-    {
-      Debug.Assert(impl.OutParams.Count == actionDecl.OutParams.Count);
-      var pendingAsyncTypeToActionDecl = new Dictionary<CtorType, ActionDecl>();
-      var lhss = new List<IdentifierExpr>();
-      var rhss = new List<Expr>();
-      actionDecl.CreateActionDecls.ForEach(decl =>
-      {
-        pendingAsyncTypeToActionDecl[decl.PendingAsyncType] = decl;
-        var pa = civlTypeChecker.Formal($"PAs_{decl.Name}", decl.PendingAsyncMultisetType, false);
-        impl.Proc.OutParams.Add(pa);
-        impl.OutParams.Add(pa);
-        lhss.Add(Expr.Ident(pa));
-        rhss.Add(ExprHelper.FunctionCall(decl.PendingAsyncConst, Expr.Literal(0)));
-      });
-      var tc = new TypecheckingContext(null, civlTypeChecker.Options);
-      var initAssignCmd = CmdHelper.AssignCmd(lhss, rhss);
-      initAssignCmd.Typecheck(tc);
-      impl.Blocks[0].Cmds.Insert(0, initAssignCmd);
-      impl.Blocks.ForEach(block =>
-      {
-        var newCmds = new List<Cmd>();
-        foreach (var cmd in block.Cmds)
-        {
-          if (cmd is CallCmd callCmd)
-          {
-            var originalProc = (Procedure)Monomorphizer.GetOriginalDecl(callCmd.Proc);
-            if (callCmd.IsAsync)
-            {
-              var actionDecl = (ActionDecl)callCmd.Proc;
-              var pendingAsyncMultiset = 
-                Expr.Store(
-                  ExprHelper.FunctionCall(actionDecl.PendingAsyncConst, Expr.Literal(0)),
-                  ExprHelper.FunctionCall(actionDecl.PendingAsyncCtor, callCmd.Ins),
-                  Expr.Literal(1));
-              var pendingAsyncMultisetType = TypeHelper.MapType(actionDecl.PendingAsyncType, Type.Int);
-              var pendingAsyncCollector = impl.OutParams.Skip(actionDecl.OutParams.Count).First(v => v.TypedIdent.Type.Equals(pendingAsyncMultisetType));
-              var updateAssignCmd = CmdHelper.AssignCmd(pendingAsyncCollector,
-                ExprHelper.FunctionCall(actionDecl.PendingAsyncAdd, Expr.Ident(pendingAsyncCollector), pendingAsyncMultiset));
-              updateAssignCmd.Typecheck(tc);
-              newCmds.Add(updateAssignCmd);
-              continue;
-            }
-            else if (originalProc.Name == "create_asyncs" || originalProc.Name == "create_multi_asyncs")
-            {
-              var pendingAsyncType =
-                (CtorType)civlTypeChecker.program.monomorphizer.GetTypeInstantiation(callCmd.Proc)["T"];
-              var pendingAsync = pendingAsyncTypeToActionDecl[pendingAsyncType];
-              var pendingAsyncMultiset = originalProc.Name == "create_asyncs"
-                  ? ExprHelper.FunctionCall(pendingAsync.PendingAsyncIte, callCmd.Ins[0],
-                    ExprHelper.FunctionCall(pendingAsync.PendingAsyncConst, Expr.Literal(1)),
-                    ExprHelper.FunctionCall(pendingAsync.PendingAsyncConst, Expr.Literal(0)))
-                  : callCmd.Ins[0];
-              var pendingAsyncMultisetType = TypeHelper.MapType(pendingAsyncType, Type.Int);
-              var pendingAsyncCollector = impl.OutParams.Skip(actionDecl.OutParams.Count).First(v => v.TypedIdent.Type.Equals(pendingAsyncMultisetType));
-              var updateAssignCmd = CmdHelper.AssignCmd(pendingAsyncCollector,
-                ExprHelper.FunctionCall(pendingAsync.PendingAsyncAdd, Expr.Ident(pendingAsyncCollector), pendingAsyncMultiset));
-              updateAssignCmd.Typecheck(tc);
-              newCmds.Add(updateAssignCmd);
-              continue;
-            }
-          }
-          newCmds.Add(cmd);
-        }
-        block.Cmds = newCmds;
-      });
-    }
-
-    private void DropSetChoice(Implementation impl)
-    {
-      impl.Blocks.ForEach(block =>
-      {
-        var newCmds = new List<Cmd>();
-        foreach (var cmd in block.Cmds)
-        {
-          if (cmd is CallCmd callCmd)
-          {
-            var originalProcName = Monomorphizer.GetOriginalDecl(callCmd.Proc).Name;
-            if (originalProcName == "set_choice")
-            {
-              continue;
-            }
-          }
-          newCmds.Add(cmd);
-        }
-        block.Cmds = newCmds;
-      });
-    }
-
-    private void DesugarSetChoice(CivlTypeChecker civlTypeChecker, Implementation impl)
-    {
-      var choice = civlTypeChecker.Formal("choice", TypeHelper.CtorType(ChoiceDatatypeTypeCtorDecl), false);
-      impl.Proc.OutParams.Add(choice);
-      impl.OutParams.Add(choice);
-      impl.Blocks.ForEach(block =>
-      {
-        var newCmds = new List<Cmd>();
-        foreach (var cmd in block.Cmds)
-        {
-          if (cmd is CallCmd callCmd)
-          {
-            var originalProcName = Monomorphizer.GetOriginalDecl(callCmd.Proc).Name;
-            if (originalProcName == "set_choice")
-            {
-              var pendingAsyncType = (CtorType)civlTypeChecker.program.monomorphizer.GetTypeInstantiation(callCmd.Proc)["T"];
-              var pendingAsync = PendingAsyncs.First(decl => decl.PendingAsyncType.Equals(pendingAsyncType));
-              var tc = new TypecheckingContext(null, civlTypeChecker.Options);
-              var emptyExpr = Expr.Eq(Expr.Ident(PAs(pendingAsyncType)),
-                ExprHelper.FunctionCall(pendingAsync.PendingAsyncConst, Expr.Literal(0)));
-              var memberExpr = Expr.Gt(Expr.Select(Expr.Ident(PAs(pendingAsyncType)), callCmd.Ins[0]),
-                Expr.Literal(0));
-              var assertCmd = CmdHelper.AssertCmd(cmd.tok, Expr.Or(emptyExpr, memberExpr),
-                "Choice is not a created pending async");
-              assertCmd.Typecheck(tc);
-              newCmds.Add(assertCmd);
-              var assignCmd = CmdHelper.AssignCmd(CmdHelper.FieldAssignLhs(Expr.Ident(choice), pendingAsyncType.Decl.Name), callCmd.Ins[0]);
-              assignCmd.Typecheck(tc);
-              newCmds.Add(assignCmd);
-              continue;
-            }
-          }
-          newCmds.Add(cmd);
-        }
-        block.Cmds = newCmds;
-      });
-    }
 
     private void DeclareTriggerFunctions()
     {

Source/Concurrency/CivlRewriter.cs

@@ -29,11 +29,6 @@ public static void Transform(ConcurrencyOptions options, CivlTypeChecker civlTyp
       civlTypeChecker.AtomicActions.ForEach(x =>
       {
         decls.AddRange(new Declaration[] { x.Impl, x.Impl.Proc, x.InputOutputRelation });
-        if (x.ImplWithChoice != null)
-        {
-          decls.AddRange(new Declaration[]
-            { x.ImplWithChoice, x.ImplWithChoice.Proc, x.InputOutputRelationWithChoice });
-        }
       });
 
       // Commutativity checks
@@ -51,10 +46,7 @@ public static void Transform(ConcurrencyOptions options, CivlTypeChecker civlTyp
       if (!options.TrustRefinement)
       {
          YieldingProcChecker.AddRefinementCheckers(civlTypeChecker, decls);
-         if (!options.TrustSequentialization)
-         {
-            Sequentialization.AddCheckers(civlTypeChecker, decls);
-         }
+         ActionRefinement.AddCheckers(civlTypeChecker, decls);
       }
 
       foreach (var action in civlTypeChecker.AtomicActions)