[Civl] Change failure preservation check

Source/Concurrency/CivlCoreTypes.cs

@@ -1,7 +1,6 @@
 using System.Collections.Generic;
 using System.Diagnostics;
 using System.Linq;
-using Microsoft.Boogie.GraphUtil;
 
 namespace Microsoft.Boogie
 {
@@ -171,7 +170,7 @@ private void AddGateSufficiencyCheckerAndHoistAsserts(CivlTypeChecker civlTypeCh
     {
       if (ActionDecl.Asserts.Count == 0)
       {
-        Gate = HoistAsserts(Impl, civlTypeChecker.Options);
+        Gate = Wlp.HoistAsserts(Impl, civlTypeChecker.Options);
         return;
       }
 
@@ -199,7 +198,7 @@ private void AddGateSufficiencyCheckerAndHoistAsserts(CivlTypeChecker civlTypeCh
         proc.OutParams, proc.IsPure, requires, proc.Modifies, new List<Ensures>());
       gateSufficiencyCheckerDecls.AddRange(new Declaration[] { checkerImpl.Proc, checkerImpl });
 
-      HoistAsserts(Impl, civlTypeChecker.Options);
+      Wlp.HoistAsserts(Impl, civlTypeChecker.Options);
 
       Gate = ActionDecl.Asserts.Select(
         assertCmd => new AssertCmd(assertCmd.tok, Substituter.Apply(gateSubst, assertCmd.Expr),
@@ -367,103 +366,7 @@ private void DesugarSetChoice(CivlTypeChecker civlTypeChecker, Implementation im
         block.Cmds = newCmds;
       });
     }
-
-    /*
-     * HoistAsserts computes the weakest liberal precondition (wlp) of the body
-     * of impl as a collection of AssertCmd's. As a side effect, all AssertCmd's
-     * in any block of impl are removed.
-     *
-     * HoistAsserts assumes that the body of impl does not contain any loops or
-     * calls. The blocks in impl are sorted from entry to exit and processed in
-     * reverse order, thus ensuring that a block is processed only once the wlp
-     * of all its successors has been computed.
-     */
-    private List<AssertCmd> HoistAsserts(Implementation impl, ConcurrencyOptions options)
-    {
-      Dictionary<Block, List<AssertCmd>> wlps = new Dictionary<Block, List<AssertCmd>>();
-      Graph<Block> dag = Program.GraphFromBlocks(impl.Blocks, false);
-      foreach (var block in dag.TopologicalSort())
-      {
-        if (block.TransferCmd is ReturnCmd)
-        {
-          var wlp = HoistAsserts(block.Cmds, new List<AssertCmd>(), options);
-          wlps.Add(block, wlp);
-        }
-        else if (block.TransferCmd is GotoCmd gotoCmd)
-        {
-          var wlp =
-            HoistAsserts(block.Cmds, gotoCmd.LabelTargets.SelectMany(b => wlps[b]).ToList(), options);
-          wlps.Add(block, wlp);
-        }
-        else
-        {
-          throw new Cce.UnreachableException();
-        }
-      }
-      return wlps[impl.Blocks[0]].Select(assertCmd => Forall(impl.LocVars.Union(impl.OutParams), assertCmd)).ToList();
-    }
-
-    private List<AssertCmd> HoistAsserts(List<Cmd> cmds, List<AssertCmd> postconditions, ConcurrencyOptions options)
-    {
-      for (int i = cmds.Count - 1; i >= 0; i--)
-      {
-        var cmd = cmds[i];
-        if (cmd is AssertCmd assertCmd)
-        {
-          postconditions.Add(assertCmd);
-        } 
-        else if (cmd is AssumeCmd assumeCmd)
-        {
-          postconditions = postconditions
-            .Select(assertCmd => new AssertCmd(assertCmd.tok, Expr.Imp(assumeCmd.Expr, assertCmd.Expr))).ToList();
-        }
-        else if (cmd is AssignCmd assignCmd)
-        {
-          var varToExpr = new Dictionary<Variable, Expr>();
-          var simpleAssignCmd = assignCmd.AsSimpleAssignCmd;
-          for (var j = 0; j < simpleAssignCmd.Lhss.Count; j++)
-          {
-            var lhs = simpleAssignCmd.Lhss[j];
-            var rhs = simpleAssignCmd.Rhss[j];
-            varToExpr.Add(lhs.DeepAssignedVariable, rhs);
-          }
-          postconditions = postconditions.Select(assertCmd =>
-            new AssertCmd(assertCmd.tok, SubstitutionHelper.Apply(varToExpr, assertCmd.Expr))).ToList();
-        }
-        else if (cmd is HavocCmd havocCmd)
-        {
-          postconditions = postconditions.Select(assertCmd => Forall(havocCmd.Vars.Select(ie => ie.Decl), assertCmd))
-            .ToList();
-        }
-        else if (cmd is UnpackCmd unpackCmd)
-        {
-          var desugaredCmd = (StateCmd) unpackCmd.GetDesugaring(options);
-          postconditions = HoistAsserts(desugaredCmd.Cmds, postconditions, options); // removes precondition assert from desugaredCmd.Cmds
-        }
-        else
-        {
-          throw new Cce.UnreachableException();
-        }
-      }
-      cmds.RemoveAll(cmd => cmd is AssertCmd);
-      return postconditions;
-    }
-
-    private static AssertCmd Forall(IEnumerable<Variable> vars, AssertCmd assertCmd)
-    {
-      var freeObjects = new GSet<object>();
-      assertCmd.Expr.ComputeFreeVariables(freeObjects);
-      var quantifiedVars = freeObjects.OfType<Variable>().Intersect(vars);
-      if (quantifiedVars.Count() == 0)
-      {
-        return assertCmd;
-      }
-      var varMapping = quantifiedVars.ToDictionary(v => v,
-        v => (Variable) VarHelper.BoundVariable(v.Name, v.TypedIdent.Type));
-      return new AssertCmd(assertCmd.tok,
-        ExprHelper.ForallExpr(varMapping.Values.ToList(), SubstitutionHelper.Apply(varMapping, assertCmd.Expr)));
-    }
-
+
     private void DeclareTriggerFunctions()
     {
       TriggerFunctions = new Dictionary<Variable, Function>();

Source/Concurrency/CivlUtil.cs

@@ -344,9 +344,9 @@ public static LocalVariable LocalVariable(string name, Type type)
       return new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, name, type));
     }
 
-    public static BoundVariable BoundVariable(string name, Type type)
+    public static BoundVariable BoundVariable(string name, Type type, QKeyValue kv = null)
     {
-      return new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, name, type));
+      return new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, name, type), kv);
     }
 
     public static Formal Formal(string name, Type type, bool incoming)
@@ -430,6 +430,14 @@ public static IEnumerable<Cmd> Apply(Dictionary<Variable, Variable> map, IEnumer
     }
   }
 
+  public static class RequiresHelper
+  {
+    public static Requires Requires(Expr expr, QKeyValue kv = null)
+    {
+      return new Requires(Token.NoToken, false, expr, null, kv);
+    }
+  }
+
   public static class LinqExtensions
   {
     public static IEnumerable<IEnumerable<T>> CartesianProduct<T>(this IEnumerable<IEnumerable<T>> sequences)

Source/Concurrency/InductiveSequentialization.cs

@@ -5,30 +5,6 @@
 
 namespace Microsoft.Boogie
 {
-  public class LinearityCheck
-  {
-    public LinearDomain domain;
-    public Expr assume;
-    public Expr assert;
-    public string message;
-    public string checkName;
-
-    public LinearityCheck(LinearDomain domain, Expr assume, Expr assert, string message, string checkName)
-    {
-      this.domain = domain;
-      this.assume = assume;
-      this.assert = assert;
-      this.message = message;
-      this.checkName = checkName;
-    }
-  }
-
-  public enum InductiveSequentializationRule
-  {
-    ISL,
-    ISR
-  }
-
   public abstract class Sequentialization
   {
     protected CivlTypeChecker civlTypeChecker;
@@ -47,7 +23,7 @@ protected Sequentialization(CivlTypeChecker civlTypeChecker, Action targetAction
     public IEnumerable<Action> EliminatedActions => eliminatedActions;
 
     public int Layer => targetAction.LayerRange.UpperLayer;
-    public Action TargetAction => targetAction;
+
     protected virtual List<Declaration> GenerateCheckers()
     {
       return new List<Declaration>();
@@ -100,98 +76,6 @@ protected AssertCmd GetCheck(IToken tok, Expr expr, string msg)
       expr.Typecheck(new TypecheckingContext(null, civlTypeChecker.Options));
       return CmdHelper.AssertCmd(tok, expr, msg);
     }
-
-    protected List<Declaration> GeneratePartitionChecker(Action action)
-    {
-      var inputDisjointnessExpr = civlTypeChecker.linearTypeChecker.DisjointnessExprForEachDomain(
-        action.Impl.InParams.Union(action.ModifiedGlobalVars)
-        .Where(x => LinearTypeChecker.InKinds.Contains(LinearTypeChecker.FindLinearKind(x))));
-
-      var requires = action.Gate.Select(a => new Requires(false, a.Expr))
-          .Concat(inputDisjointnessExpr.Select(expr => new Requires(false, expr)))
-          .ToList();
-
-      var eliminatedActionDecls = EliminatedActionDecls.ToHashSet();
-      var lhsExprs = new List<Expr>();
-      var rhsExprs = new List<Expr>();
-      foreach (var pendingAsync in action.PendingAsyncs)
-      {
-        var pendingAsyncExpr = Expr.Ident(action.PAs(pendingAsync.PendingAsyncType));
-        var emptyExpr = ExprHelper.FunctionCall(pendingAsync.PendingAsyncConst, Expr.Literal(0));
-        if (eliminatedActionDecls.Contains(pendingAsync))
-        {
-          lhsExprs.Add(Expr.Neq(pendingAsyncExpr, emptyExpr));
-        }
-        else
-        {
-          rhsExprs.Add(Expr.Eq(pendingAsyncExpr, emptyExpr));
-        }
-      }
-      var cmds = new List<Cmd>() {
-        CmdHelper.CallCmd(action.Impl.Proc, action.Impl.InParams, action.Impl.OutParams),
-        GetCheck(action.tok, Expr.Imp(Expr.Or(lhsExprs), Expr.And(rhsExprs)), "Partition checker failed")
-      };
-
-      List<Block> checkerBlocks = new List<Block>();
-      var locals = new List<Variable>();
-      foreach (var pendingAsync in action.PendingAsyncs.Intersect(eliminatedActionDecls))
-      {
-        var pendingAsyncType = pendingAsync.PendingAsyncType;
-        var pendingAsyncCtor = pendingAsync.PendingAsyncCtor;
-        var pendingAsyncVar = action.PAs(pendingAsyncType);
-        var pendingAsyncExpr = Expr.Ident(pendingAsyncVar);
-        var pendingAsyncAction = civlTypeChecker.Action(pendingAsync);
-
-        var paLocal = civlTypeChecker.LocalVariable($"local_{pendingAsyncVar.Name}", pendingAsyncType);
-        locals.Add(paLocal);
-
-        List<Cmd> blockCmds = new List<Cmd>
-        {
-          CmdHelper.AssumeCmd(Expr.Ge(Expr.Select(pendingAsyncExpr, Expr.Ident(paLocal)), Expr.Literal(1)))
-        };
-
-        var substMap = new Dictionary<Variable, Expr>();
-        for (int i = 0; i < pendingAsyncAction.Impl.InParams.Count; i++)
-        {
-          substMap[pendingAsyncAction.Impl.InParams[i]] = ExprHelper.FieldAccess(Expr.Ident(paLocal), pendingAsyncCtor.InParams[i].Name);
-        }
-        blockCmds.AddRange(pendingAsyncAction.GetGateAsserts(
-          Substituter.SubstitutionFromDictionary(substMap),
-          $"Gate of {pendingAsyncAction.Name} in partition checker failed"));
-
-        var block = BlockHelper.Block($"label_{pendingAsyncVar.Name}", blockCmds);
-        checkerBlocks.Add(block);
-      }
-
-      string checkerName = civlTypeChecker.AddNamePrefix($"PartitionChecker_{action.Name}");
-      var blocks = new List<Block>(checkerBlocks.Count + 1);
-      if (checkerBlocks.Count != 0)
-      {
-        blocks.Add(BlockHelper.Block(checkerName, cmds, checkerBlocks));
-        blocks.AddRange(checkerBlocks);
-      }
-      else
-      {
-        blocks.Add(BlockHelper.Block(checkerName, cmds));
-      }
-      CivlUtil.ResolveAndTypecheck(civlTypeChecker.Options, blocks, ResolutionContext.State.Two);
-
-      Procedure proc = DeclHelper.Procedure(
-        checkerName,
-        action.Impl.InParams,
-        action.Impl.OutParams,
-        requires,
-        action.ModifiedGlobalVars.Select(Expr.Ident).ToList(),
-        new List<Ensures>());
-      Implementation impl = DeclHelper.Implementation(
-        proc,
-        proc.InParams,
-        proc.OutParams,
-        locals,
-        blocks);
-
-      return new List<Declaration>(new Declaration[] { proc, impl });
-    }
   }
 
   public class InlineSequentialization : Sequentialization