[Civl] Fix to heuristic for variable elimination in transition relation computation

Source/Concurrency/CivlCoreTypes.cs

@@ -290,15 +290,43 @@ private void DeclareTriggerFunctions()
       }
     }
 
-    public void AddTriggerAssumes(Program program)
+    /*
+     * This method adds triggers for each local variable at the beginning of the atomic
+     * action and after every havoc of the variable.
+     * As an optimization, the injection of the trigger is performed only if the variable
+     * is live at the point of injection.
+     */
+    public void AddTriggerAssumes(Program program, ConcurrencyOptions options)
     {
+      var liveVariableAnalysis = new AtomicActionLiveVariableAnalysis(impl, options);
+      liveVariableAnalysis.Compute();
       foreach (Variable v in impl.LocVars)
       {
         var f = triggerFunctions[v];
         program.AddTopLevelDeclaration(f);
-        var assume = CmdHelper.AssumeCmd(ExprHelper.FunctionCall(f, Expr.Ident(v)));
-        impl.Blocks[0].Cmds.Insert(0, assume);
+        if (liveVariableAnalysis.IsLiveBefore(v, impl.Blocks[0]))
+        {
+          var assume = CmdHelper.AssumeCmd(ExprHelper.FunctionCall(f, Expr.Ident(v)));
+          impl.Blocks[0].Cmds.Insert(0, assume);
+        }
       }
+      impl.Blocks.Iter(block =>
+      {
+        block.Cmds = block.Cmds.SelectMany(cmd =>
+        {
+          var newCmds = new List<Cmd> { cmd };
+          if (cmd is HavocCmd havocCmd)
+          {
+            var liveHavocVars = new HashSet<Variable>(havocCmd.Vars.Select(x => x.Decl)
+              .Where(v => liveVariableAnalysis.IsLiveAfter(v, havocCmd)));
+            impl.LocVars.Intersect(liveHavocVars).Iter(v =>
+            {
+              newCmds.Add(CmdHelper.AssumeCmd(ExprHelper.FunctionCall(triggerFunctions[v], Expr.Ident(v))));
+            });
+          }
+          return newCmds;
+        }).ToList();
+      });
     }
   }
 

Source/Concurrency/CivlRewriter.cs

@@ -40,7 +40,7 @@ public static void Transform(ConcurrencyOptions options, CivlTypeChecker civlTyp
       foreach (AtomicAction action in civlTypeChecker.procToAtomicAction.Values.Union(civlTypeChecker
         .procToIsAbstraction.Values))
       {
-        action.AddTriggerAssumes(program);
+        action.AddTriggerAssumes(program, options);
       }
 
       // Remove original declarations and add new checkers generated above

Source/Concurrency/CivlUtil.cs

@@ -4,6 +4,114 @@
 
 namespace Microsoft.Boogie
 {
+  public class AtomicActionLiveVariableAnalysis
+  {
+    private Implementation impl;
+    private ConcurrencyOptions options;
+    private Dictionary<Block, HashSet<Variable>> liveVarsBefore;
+    private Dictionary<Cmd, HashSet<Variable>> liveVarsAfter;
+
+    public AtomicActionLiveVariableAnalysis(Implementation impl, ConcurrencyOptions options)
+    {
+      this.impl = impl;
+      this.options = options;
+      this.liveVarsBefore = new Dictionary<Block, HashSet<Variable>>();
+      this.liveVarsAfter = new Dictionary<Cmd, HashSet<Variable>>();
+    }
+
+    public void Compute()
+    {
+      var graph = Program.GraphFromImpl(impl, false);
+      foreach (var block in graph.TopologicalSort())
+      {
+        if (block.TransferCmd is ReturnCmd)
+        {
+          liveVarsBefore[block] = Propagate(block.Cmds,
+            impl.Proc.Modifies.Select(x => x.Decl).Concat(impl.OutParams).ToHashSet());
+        }
+        else if (block.TransferCmd is GotoCmd gotoCmd)
+        {
+          liveVarsBefore[block] =
+            Propagate(block.Cmds, gotoCmd.labelTargets.SelectMany(x => liveVarsBefore[x]).ToHashSet());
+        }
+        else
+        {
+          throw new cce.UnreachableException();
+        }
+      }
+    }
+
+    public bool IsLiveAfter(Variable v, Cmd cmd)
+    {
+      return liveVarsAfter[cmd].Contains(v);
+    }
+
+    public bool IsLiveBefore(Variable v, Block block)
+    {
+      return liveVarsBefore[block].Contains(v);
+    }
+
+    private HashSet<Variable> Propagate(List<Cmd> cmds, HashSet<Variable> liveVars)
+    {
+      for (int i = cmds.Count - 1; i >= 0; i--)
+      {
+        var cmd = cmds[i];
+        liveVarsAfter[cmd] = new HashSet<Variable>(liveVars);
+        liveVars = Propagate(cmd, liveVars);
+      }
+      return liveVars;
+    }
+
+    private HashSet<Variable> Propagate(Cmd cmd, HashSet<Variable> liveVars)
+    {
+      if (cmd is HavocCmd havocCmd)
+      {
+        liveVars.ExceptWith(havocCmd.Vars.Select(v => v.Decl));
+        return liveVars;
+      }
+      if (cmd is AssignCmd assignCmd)
+      {
+        var usedVars = new HashSet<Variable>();
+        for (int i = 0; i < assignCmd.Lhss.Count; i++)
+        {
+          var lhs = assignCmd.Lhss[i];
+          var rhs = assignCmd.Rhss[i];
+          if (liveVars.Contains(lhs.DeepAssignedVariable))
+          {
+            liveVars.Remove(lhs.DeepAssignedVariable);
+            var variableCollector = new VariableCollector();
+            variableCollector.VisitExpr(rhs);
+            usedVars.UnionWith(variableCollector.usedVars);
+          }
+        }
+        liveVars.UnionWith(usedVars);
+        return liveVars;
+      }
+      if (cmd is PredicateCmd predicateCmd)
+      {
+        var variableCollector = new VariableCollector();
+        variableCollector.VisitExpr(predicateCmd.Expr);
+        liveVars.UnionWith(variableCollector.usedVars);
+        return liveVars;
+      }
+      if (cmd is SugaredCmd sugaredCmd)
+      {
+        return Propagate(sugaredCmd.GetDesugaring(options), liveVars);
+      }
+      if (cmd is CommentCmd)
+      {
+        return liveVars;
+      }
+      if (cmd is StateCmd stateCmd)
+      {
+        liveVars = Propagate(stateCmd.Cmds, liveVars);
+        liveVars.ExceptWith(stateCmd.Locals);
+        return liveVars;
+      }
+      throw new cce.UnreachableException();
+    }
+  }
+
   public class CivlUtil
   {
     public static void AddInlineAttribute(Declaration decl)

Source/Concurrency/TransitionRelationComputation.cs

@@ -347,8 +347,13 @@ private void SetDefinedVariables()
 
       private void EliminateIntermediateVariables()
       {
+        // The first attempt eliminates temporaries using the defined variables set up in SetDefinedVariables above.
         TryElimination(Enumerable.Empty<Variable>());
-        TryElimination(trc.allLocVars.Select(v => varCopies[v][0]));
+
+        // The second attempt eliminates temporaries considering as defined the subset that is not defined by assignments.
+        TryElimination(trc.allLocVars.SelectMany(v => varCopies[v]).Except(assignments.Select(x => x.Var)));
+
+        // The third attempt eliminates temporaries considering as defined the subset that has pool annotations.
         TryElimination(trc.allLocVars.Where(v => v.FindAttribute("pool") != null).SelectMany(v => varCopies[v]));
 
         if (trc.ignorePostState)
@@ -410,7 +415,7 @@ private void ComputeTransitionRelationExpr()
             foreach (var v in existsVarMap.Keys)
             {
               var orig = copyToOriginalVar[v];
-              if (v == varCopies[orig].First() && trc.triggers.ContainsKey(orig))
+              if (trc.triggers.ContainsKey(orig))
               {
                 var f = trc.triggers[orig];
                 exprs.Add(ExprHelper.FunctionCall(f, Expr.Ident(existsVarMap[v])));

Source/Provers/SMTLib/SMTLibLineariser.cs

@@ -784,8 +784,8 @@ public bool VisitIsConstructorOp(VCExprNAry node, LineariserOptions options)
       {
         var op = (VCExprIsConstructorOp)node.Op;
         var constructor = op.DatatypeTypeCtorDecl.Constructors[op.ConstructorIndex];
-        var name = "is-" + constructor.Name;
-        name = ExprLineariser.Namer.GetQuotedName(name, name);
+        var constructorName = ExprLineariser.Namer.GetQuotedName(constructor, constructor.Name);
+        var name = "is-" + constructorName;
         WriteApplication(name, node, options);
         return true;
       }

Test/civl/inductive-sequentialization/BroadcastConsensus.bpl

@@ -47,13 +47,11 @@ function max(CH:[val]int) : val;
 function card(CH:[val]int) : int;
 
 axiom card(MultisetEmpty) == 0;
-axiom (forall v:val :: card(MultisetSingleton(v)) == 1);
-axiom (forall CH:[val]int, v:val :: card(MultisetPlus(CH, MultisetSingleton(v))) == card(CH) + 1);
-axiom (forall CH:[val]int, v:val :: {CH[v := CH[v] + 1]} card(CH[v := CH[v] + 1]) == card(CH) + 1);
-axiom (forall m:[val]int, m':[val]int :: {card(m), card(m')} MultisetSubsetEq(m, m') && card(m) == card(m') ==> m == m');
+axiom (forall CH:[val]int, v:val, x:int :: card(CH[v := x]) == card(CH) + x - CH[v]);
+axiom (forall m:[val]int, m':[val]int :: MultisetSubsetEq(m, m') && card(m) == card(m') ==> m == m');
 
 axiom (forall v:val :: max(MultisetSingleton(v)) == v);
-axiom (forall CH:[val]int, v:val :: { CH[v := CH[v] + 1] } max(CH[v := CH[v] + 1]) == (if v > max(CH) then v else max(CH)));
+axiom (forall CH:[val]int, v:val, x:int :: x > 0 ==> max(CH[v := x]) == (if v > max(CH) then v else max(CH)));
 
 function value_card(v:val, value:[pid]val, i:pid, j:pid) : int
 {

Test/civl/inductive-sequentialization/ChangRoberts_pendingAsyncs.bpl

@@ -104,40 +104,8 @@ P' ({:linear_in "pid"} pid:int)
 returns ({:pending_async "P"} PAs:[PA]int)
 modifies channel, pendingAsyncs, leader;
 {
-  var msg:int;
-
-  assert pid(pid);
-  assert pendingAsyncs[P(pid)] > 0;
-  assert (forall m:int :: channel[pid][m] > 0 ==> m <= id[max(id)]);
-
   assert (forall j:int :: pid(j) && between(max(id), j, pid) ==> pendingAsyncs[P(j)] == 0);
-
-  if (*)
-  {
-    PAs := NoPAs();
-  }
-  else
-  {
-    assume channel[pid][msg] > 0;
-    channel[pid][msg] := channel[pid][msg] - 1;
-
-    if (msg == id[pid])
-    {
-      leader[pid] := true;
-      PAs := NoPAs();
-    }
-    else
-    {
-      if (msg > id[pid])
-      {
-        channel[next(pid)][msg] := channel[next(pid)][msg] + 1;
-      }
-      PAs := NoPAs()[P(pid) := 1];
-    }
-  }
-
-  pendingAsyncs := MapAdd(pendingAsyncs, PAs);
-  pendingAsyncs := MapSub(pendingAsyncs, SingletonPA(P(pid)));
+  call PAs := P(pid);
 }
 
 ////////////////////////////////////////////////////////////////////////////////