Merge branch 'master' into tc-crash-fix

Source/Core/AST/Absy.cs

@@ -3510,6 +3510,9 @@ public class Implementation : DeclWithFormals {
     // Both are used only when /inline is set.
     public List<Block> OriginalBlocks;
     public List<Variable> OriginalLocVars;
+
+    // Map filled in during passification to allow augmented error trace reporting
+    public Dictionary<Cmd, List<object>> debugInfos = new();
 
     public readonly ISet<byte[]> AssertionChecksums = new HashSet<byte[]>(ChecksumComparer.Default);
 

Source/Houdini/HoudiniSession.cs

@@ -195,7 +195,7 @@ public HoudiniSession(Houdini houdini, VCGen vcgen, ProverInterface proverInterf
         new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Type.Bool), false));
       proverInterface.DefineMacro(macro, conjecture);
       conjecture = exprGen.Function(macro);
-      handler = new VCGen.ErrorReporter(this.houdini.Options, gotoCmdOrigins, absyIds, impl.Blocks, vcgen.debugInfos, collector,
+      handler = new VCGen.ErrorReporter(this.houdini.Options, gotoCmdOrigins, absyIds, impl.Blocks, impl.debugInfos, collector,
         mvInfo, proverInterface.Context, program, this);
     }
 

Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs

@@ -380,6 +380,33 @@ public async Task SolverCrash()
     Assert.IsTrue(outcome2 is Completed completed2 && completed2.Result.Outcome == ConditionGeneration.Outcome.Correct);
   }
 
+  [Test]
+  public async Task ConsistentErrorTraceAfterMultipleVerificationAttempts() {
+    const string augmentedTraceNonce = "12345"; // will appear in execution trace
+    const string programString = @"
+procedure Test() {
+  assume {:print " + augmentedTraceNonce + @"} true;
+  assert false;
+}";
+    Parser.Parse(programString, "fakeFilename", out var program);
+    var options = CommandLineOptions.FromArguments(TextWriter.Null);
+    options.EnhancedErrorMessages = 1;
+    var output = await ProcessProgramAndGetOutput(program, options);
+    Assert.True(output.Contains(augmentedTraceNonce));
+    // Now repeat verification again and make sure the augmented trace still shows up
+    output = await ProcessProgramAndGetOutput(program, options);
+    Assert.True(output.Contains(augmentedTraceNonce));
+  }
+
+  private static async Task<string> ProcessProgramAndGetOutput(Program program, CommandLineOptions options) {
+    var writer = new StringWriter();
+    using (var engine = ExecutionEngine.CreateWithoutSharedCache(options)) {
+      await engine.ProcessProgram(writer, program, "fakeFilename");
+    }
+    await writer.DisposeAsync();
+    return writer.ToString();
+  }
+
   private readonly string fast = @"
 procedure easy() ensures 1 + 1 == 0; {
 }

Source/VCExpr/Boogie2VCExpr.cs

@@ -41,7 +41,7 @@ public VCGenerationOptions(CoreOptions options, List<string> supportedProverComm
     }
   }
 
-  public delegate VCExpr CodeExprConverter(CodeExpr codeExpr, List<VCExprLetBinding> bindings, bool isPositiveContext);
+  public delegate VCExpr CodeExprConverter(CodeExpr codeExpr, List<VCExprLetBinding> bindings, bool isPositiveContext, Dictionary<Cmd, List<object>> debugInfos);
 
   public class Boogie2VCExprTranslator : ReadOnlyVisitor, ICloneable
   {
@@ -876,7 +876,7 @@ public override Expr VisitCodeExpr(CodeExpr codeExpr)
       Contract.Assume(codeExprConverter != null);
 
       List<VCExprLetBinding> bindings = new List<VCExprLetBinding>();
-      VCExpr e = codeExprConverter(codeExpr, bindings, isPositiveContext);
+      VCExpr e = codeExprConverter(codeExpr, bindings, isPositiveContext, new());
       Push(e);
       return codeExpr;
     }

Source/VCGeneration/ConditionGeneration.cs

@@ -100,8 +100,6 @@ void ObjectInvariant()
 
     public Dictionary<Incarnation, Absy> incarnationOriginMap = new Dictionary<Incarnation, Absy>();
 
-    public Dictionary<Cmd, List<object>> debugInfos = new Dictionary<Cmd, List<object>>();
-
     public Program program;
     public CheckerPool CheckerPool { get; }
 
@@ -827,7 +825,7 @@ protected Dictionary<Variable, Expr> ComputeIncarnationMap(Block b,
         null; // null = the previous command was not an HashCmd. Otherwise, a *copy* of the map before the havoc statement
 
     protected void TurnIntoPassiveBlock(TextWriter traceWriter, Block b, Dictionary<Variable, Expr> incarnationMap, ModelViewInfo mvInfo,
-      Substitution oldFrameSubst, MutableVariableCollector variableCollector, byte[] currentChecksum = null)
+      Substitution oldFrameSubst, MutableVariableCollector variableCollector, Dictionary<Cmd, List<object>> debugInfos, byte[] currentChecksum = null)
     {
       Contract.Requires(b != null);
       Contract.Requires(incarnationMap != null);
@@ -844,7 +842,7 @@ protected void TurnIntoPassiveBlock(TextWriter traceWriter, Block b, Dictionary<
         ChecksumHelper.ComputeChecksums(Options, c, currentImplementation, variableCollector.UsedVariables, currentChecksum);
         variableCollector.Visit(c);
         currentChecksum = c.Checksum;
-        TurnIntoPassiveCmd(traceWriter, c, b, incarnationMap, oldFrameSubst, passiveCmds, mvInfo);
+        TurnIntoPassiveCmd(traceWriter, c, b, incarnationMap, oldFrameSubst, passiveCmds, mvInfo, debugInfos);
       }
 
       b.Checksum = currentChecksum;
@@ -871,7 +869,7 @@ protected Dictionary<Variable, Expr> Convert2PassiveCmd(ImplementationRun run, M
 
       var start = DateTime.UtcNow;
 
-      Dictionary<Variable, Expr> r = ConvertBlocks2PassiveCmd(run.OutputWriter, implementation.Blocks, implementation.Proc.Modifies, mvInfo);
+      Dictionary<Variable, Expr> r = ConvertBlocks2PassiveCmd(run.OutputWriter, implementation.Blocks, implementation.Proc.Modifies, mvInfo, implementation.debugInfos);
 
       var end = DateTime.UtcNow;
 
@@ -908,7 +906,7 @@ protected Dictionary<Variable, Expr> Convert2PassiveCmd(ImplementationRun run, M
     }
 
     protected Dictionary<Variable, Expr> ConvertBlocks2PassiveCmd(TextWriter traceWriter, List<Block> blocks, List<IdentifierExpr> modifies,
-      ModelViewInfo mvInfo)
+      ModelViewInfo mvInfo, Dictionary<Cmd, List<object>> debugInfos)
     {
       Contract.Requires(blocks != null);
       Contract.Requires(modifies != null);
@@ -988,7 +986,7 @@ protected Dictionary<Variable, Expr> ConvertBlocks2PassiveCmd(TextWriter traceWr
 
         #endregion Each block's map needs to be available to successor blocks
 
-        TurnIntoPassiveBlock(traceWriter, b, incarnationMap, mvInfo, oldFrameSubst, mvc, currentChecksum);
+        TurnIntoPassiveBlock(traceWriter, b, incarnationMap, mvInfo, oldFrameSubst, mvc, debugInfos, currentChecksum);
         exitBlock = b;
         exitIncarnationMap = incarnationMap;
       }
@@ -1052,7 +1050,7 @@ void TraceCachingAction(TextWriter traceWriter, Cmd cmd, CachingAction action)
       }
     }
 
-    private void AddDebugInfo(Cmd c, Dictionary<Variable, Expr> incarnationMap, List<Cmd> passiveCmds)
+    private void AddDebugInfo(Cmd c, Dictionary<Variable, Expr> incarnationMap, List<Cmd> passiveCmds, Dictionary<Cmd, List<object>> debugInfos)
     {
       if (c is ICarriesAttributes cmd)
       {
@@ -1100,7 +1098,7 @@ private void AddDebugInfo(Cmd c, Dictionary<Variable, Expr> incarnationMap, List
     /// Meanwhile, record any information needed to later reconstruct a model view.
     /// </summary>
     protected void TurnIntoPassiveCmd(TextWriter traceWriter, Cmd c, Block enclosingBlock, Dictionary<Variable, Expr> incarnationMap, Substitution oldFrameSubst,
-      List<Cmd> passiveCmds, ModelViewInfo mvInfo)
+      List<Cmd> passiveCmds, ModelViewInfo mvInfo, Dictionary<Cmd, List<object>> debugInfos)
     {
       Contract.Requires(c != null);
       Contract.Requires(enclosingBlock != null);
@@ -1109,7 +1107,7 @@ protected void TurnIntoPassiveCmd(TextWriter traceWriter, Cmd c, Block enclosing
       Contract.Requires(passiveCmds != null);
       Contract.Requires(mvInfo != null);
 
-      AddDebugInfo(c, incarnationMap, passiveCmds);
+      AddDebugInfo(c, incarnationMap, passiveCmds, debugInfos);
       Substitution incarnationSubst = Substituter.SubstitutionFromDictionary(incarnationMap);
 
       Microsoft.Boogie.VCExprAST.QuantifierInstantiationEngine.SubstituteIncarnationInInstantiationSources(c, incarnationSubst);
@@ -1485,7 +1483,7 @@ protected void TurnIntoPassiveCmd(TextWriter traceWriter, Cmd c, Block enclosing
       {
         Cmd cmd = sug.GetDesugaring(Options);
         Contract.Assert(cmd != null);
-        TurnIntoPassiveCmd(traceWriter, cmd, enclosingBlock, incarnationMap, oldFrameSubst, passiveCmds, mvInfo);
+        TurnIntoPassiveCmd(traceWriter, cmd, enclosingBlock, incarnationMap, oldFrameSubst, passiveCmds, mvInfo, debugInfos);
       }
       else if (c is StateCmd st)
       {
@@ -1506,7 +1504,7 @@ protected void TurnIntoPassiveCmd(TextWriter traceWriter, Cmd c, Block enclosing
         foreach (Cmd s in st.Cmds)
         {
           Contract.Assert(s != null);
-          TurnIntoPassiveCmd(traceWriter, s, enclosingBlock, incarnationMap, oldFrameSubst, passiveCmds, mvInfo);
+          TurnIntoPassiveCmd(traceWriter, s, enclosingBlock, incarnationMap, oldFrameSubst, passiveCmds, mvInfo, debugInfos);
         }
 
         // remove the local variables from the incarnation map

Source/VCGeneration/Split.cs

@@ -1343,7 +1343,7 @@ public async Task BeginCheck(TextWriter traceWriter, Checker checker, VerifierCa
             exprGen.ControlFlowFunctionApplication(exprGen.Integer(BigNum.ZERO), exprGen.Integer(BigNum.ZERO));
           VCExpr eqExpr = exprGen.Eq(controlFlowFunctionAppl, exprGen.Integer(BigNum.FromInt(absyIds.GetId(Implementation.Blocks[0]))));
           vc = exprGen.Implies(eqExpr, vc);
-          reporter = new VCGen.ErrorReporter(options, gotoCmdOrigins, absyIds, Implementation.Blocks, parent.debugInfos, callback,
+          reporter = new VCGen.ErrorReporter(options, gotoCmdOrigins, absyIds, Implementation.Blocks, Implementation.debugInfos, callback,
             mvInfo, checker.TheoremProver.Context, parent.program, this);
         }
 

Source/VCGeneration/VCGen.cs

@@ -84,7 +84,7 @@ public CodeExprConversionClosure(TextWriter traceWriter, VCGenOptions options, C
         this.ctx = ctx;
       }
 
-      public VCExpr CodeExprToVerificationCondition(CodeExpr codeExpr, List<VCExprLetBinding> bindings, bool isPositiveContext)
+      public VCExpr CodeExprToVerificationCondition(CodeExpr codeExpr, List<VCExprLetBinding> bindings, bool isPositiveContext, Dictionary<Cmd, List<object>> debugInfos)
       {
         VCGen vcgen = new VCGen(new Program(), new CheckerPool(options));
         vcgen.variable2SequenceNumber = new Dictionary<Variable, int>();
@@ -94,7 +94,7 @@ public VCExpr CodeExprToVerificationCondition(CodeExpr codeExpr, List<VCExprLetB
         ResetPredecessors(codeExpr.Blocks);
         vcgen.AddBlocksBetween(codeExpr.Blocks);
         Dictionary<Variable, Expr> gotoCmdOrigins = vcgen.ConvertBlocks2PassiveCmd(traceWriter, codeExpr.Blocks,
-          new List<IdentifierExpr>(), new ModelViewInfo(codeExpr));
+          new List<IdentifierExpr>(), new ModelViewInfo(codeExpr), debugInfos);
         VCExpr startCorrect = vcgen.LetVC(codeExpr.Blocks, null, absyIds, ctx, out var ac, isPositiveContext);
         VCExpr vce = ctx.ExprGen.Let(bindings, startCorrect);
         if (vcgen.CurrentLocalVariables.Count != 0)

Test/civl/samples/coherence.bpl

@@ -1,3 +1,4 @@
+// RUN: %parallel-boogie "%s" > "%t"
 type MemAddr;
 type Value;
 datatype State {