Turn into passive cmd splitup

Source/Core/AST/Absy.cs

@@ -280,6 +280,33 @@ public List<int> FindLayers()
       }
       return layers.Distinct().OrderBy(l => l).ToList();
     }
+
+    // Look for {:name string} in list of attributes.
+    public string FindStringAttribute(string name)
+    {
+      return QKeyValue.FindStringAttribute(Attributes, name);
+    }
+
+    public void AddStringAttribute(IToken tok, string name, string parameter)
+    {
+      Attributes = new QKeyValue(tok, name, new List<object>() {parameter}, Attributes);
+    }
+
+    public void CopyIdFrom(IToken tok, ICarriesAttributes src)
+    {
+      var id = src.FindStringAttribute("id");
+      if (id is not null) {
+        AddStringAttribute(tok, "id", id);
+      }
+    }
+
+    public void CopyIdWithSuffixFrom(IToken tok, ICarriesAttributes src, string suffix)
+    {
+      var id = src.FindStringAttribute("id");
+      if (id is not null) {
+        AddStringAttribute(tok, "id", id + suffix);
+      }
+    }
   }
 
   [ContractClassFor(typeof(Absy))]
@@ -410,13 +437,6 @@ public Expr FindExprAttribute(string name)
       return res;
     }
 
-    // Look for {:name string} in list of attributes.
-    public string FindStringAttribute(string name)
-    {
-      Contract.Requires(name != null);
-      return QKeyValue.FindStringAttribute(this.Attributes, name);
-    }
-
     // Look for {:name N} in list of attributes. Return false if attribute
     // 'name' does not exist or if N is not an integer constant.  Otherwise,
     // return true and update 'result' with N.
@@ -1810,7 +1830,7 @@ public byte[] MD5DependencyChecksum
 
     public string Checksum
     {
-      get { return FindStringAttribute("checksum"); }
+      get { return (this as ICarriesAttributes).FindStringAttribute("checksum"); }
     }
 
     string dependencyChecksum;
@@ -3616,7 +3636,7 @@ public string Id
     {
       get
       {
-        var id = FindStringAttribute("id");
+        var id = (this as ICarriesAttributes).FindStringAttribute("id");
         if (id == null)
         {
           id = Name + GetHashCode().ToString() + ":0";

Source/Core/AST/AbsyCmd.cs

@@ -3720,6 +3720,7 @@ protected override Cmd ComputeDesugaring(PrintOptions options)
       Dictionary<Variable, Expr> substMapBound = new Dictionary<Variable, Expr>();
       List<Variable> /*!*/
         tempVars = new List<Variable>();
+      string callId = (this as ICarriesAttributes).FindStringAttribute("id");
 
       // proc P(ins) returns (outs)
       //   requires Pre
@@ -3838,6 +3839,7 @@ protected override Cmd ComputeDesugaring(PrintOptions options)
             AssertCmd /*!*/
               a = new AssertRequiresCmd(this, reqCopy);
             Contract.Assert(a != null);
+
             if (Attributes != null)
             {
               // Inherit attributes of call.
@@ -3846,6 +3848,11 @@ protected override Cmd ComputeDesugaring(PrintOptions options)
               a.Attributes = attrCopy;
             }
 
+            // Do this after copying the attributes so it doesn't get overwritten
+            if (callId is not null) {
+              (a as ICarriesAttributes).CopyIdWithSuffixFrom(tok, req,  $"${callId}$requires");
+            }
+
             a.ErrorDataEnhanced = reqCopy.ErrorDataEnhanced;
             newBlockBody.Add(a);
           }
@@ -3857,6 +3864,11 @@ protected override Cmd ComputeDesugaring(PrintOptions options)
           AssumeCmd /*!*/
             a = new AssumeCmd(req.tok, Substituter.Apply(s, req.Condition));
           Contract.Assert(a != null);
+          // These probably won't have IDs, but copy if they do.
+          if (callId is not null) {
+            (a as ICarriesAttributes).CopyIdWithSuffixFrom(tok, req, $"${callId}$requires_assumed");
+          }
+
           newBlockBody.Add(a);
         }
       }
@@ -4019,6 +4031,10 @@ protected override Cmd ComputeDesugaring(PrintOptions options)
 
         #endregion
 
+        if (callId is not null) {
+          (assume as ICarriesAttributes).CopyIdWithSuffixFrom(tok, e, $"${callId}$ensures");
+        }
+
         newBlockBody.Add(assume);
       }
 
@@ -4036,6 +4052,9 @@ protected override Cmd ComputeDesugaring(PrintOptions options)
             cout_exp = new IdentifierExpr(cce.NonNull(couts[i]).tok, cce.NonNull(couts[i]));
           Contract.Assert(cout_exp != null);
           AssignCmd assign = Cmd.SimpleAssign(param_i.tok, cce.NonNull(this.Outs[i]), cout_exp);
+          if (callId is not null) {
+            Attributes = new QKeyValue(param_i.tok, "id", new List<object>(){ $"{callId}$out{i}" }, Attributes);
+          }
           newBlockBody.Add(assign);
         }
       }

Source/Core/AST/AbsyType.cs

@@ -3604,7 +3604,7 @@ public override bool IsSeq
     // be represented using the provided string (and also does not need to be explicitly declared).
     public string GetBuiltin()
     {
-      return this.Decl.FindStringAttribute("builtin");
+      return (this.Decl as ICarriesAttributes).FindStringAttribute("builtin");
     }
 
     //-----------  Cloning  ----------------------------------

Source/Core/AST/Program.cs

@@ -395,7 +395,7 @@ public List<GlobalVariable /*!*/> /*!*/ GlobalVariables
     }
   }
 
-  public readonly ISet<string> NecessaryAssumes = new HashSet<string>();
+  public readonly ISet<string> AllCoveredElements = new HashSet<string>();
 
   public IEnumerable<Block> Blocks()
   {

Source/Core/Monomorphization.cs

@@ -13,7 +13,7 @@ public class MonomorphismChecker : ReadOnlyVisitor
 
     public static bool DoesTypeCtorDeclNeedMonomorphization(TypeCtorDecl typeCtorDecl)
     {
-      return typeCtorDecl.Arity > 0 && typeCtorDecl.FindStringAttribute("builtin") == null;
+      return typeCtorDecl.Arity > 0 && (typeCtorDecl as ICarriesAttributes).FindStringAttribute("builtin") == null;
     }
 
     public static bool IsMonomorphic(Program program)

Source/ExecutionEngine/CommandLineOptions.cs

@@ -201,7 +201,8 @@ public bool NormalizeDeclarationOrder
 
     public bool ImmediatelyAcceptCommands => StratifiedInlining > 0 || ContractInfer;
 
-    public bool ProduceUnsatCores => PrintNecessaryAssumes || EnableUnSatCoreExtract == 1 ||
+    public bool ProduceUnsatCores => TrackVerificationCoverage ||
+                                     EnableUnSatCoreExtract == 1 ||
                                      ContractInfer && (UseUnsatCoreForContractInfer || ExplainHoudini);
 
     public bool BatchModeSolver { get; set; }
@@ -279,10 +280,9 @@ public bool UseUnsatCoreForContractInfer {
 
     public bool PrintAssignment  { get; set; }
 
-    // TODO(wuestholz): Add documentation for this flag.
-    public bool PrintNecessaryAssumes {
-      get => printNecessaryAssumes;
-      set => printNecessaryAssumes = value;
+    public bool TrackVerificationCoverage {
+      get => trackVerificationCoverage;
+      set => trackVerificationCoverage = value;
     }
 
     public int InlineDepth  { get; set; } = -1;
@@ -544,7 +544,7 @@ void ObjectInvariant5()
     private bool reverseHoudiniWorklist = false;
     private bool houdiniUseCrossDependencies = false;
     private bool useUnsatCoreForContractInfer = false;
-    private bool printNecessaryAssumes = false;
+    private bool trackVerificationCoverage = false;
     private bool useProverEvaluate;
     private bool trustMoverTypes = false;
     private bool trustNoninterference = false;
@@ -1297,7 +1297,7 @@ protected override bool ParseOption(string name, CommandLineParseState ps)
               ps.CheckBooleanFlag("crossDependencies", x => houdiniUseCrossDependencies = x) ||
               ps.CheckBooleanFlag("useUnsatCoreForContractInfer", x => useUnsatCoreForContractInfer = x) ||
               ps.CheckBooleanFlag("printAssignment", x => PrintAssignment = x) ||
-              ps.CheckBooleanFlag("printNecessaryAssumes", x => printNecessaryAssumes = x) ||
+              ps.CheckBooleanFlag("trackVerificationCoverage", x => trackVerificationCoverage = x) ||
               ps.CheckBooleanFlag("useProverEvaluate", x => useProverEvaluate = x) ||
               ps.CheckBooleanFlag("deterministicExtractLoops", x => DeterministicExtractLoops = x) ||
               ps.CheckBooleanFlag("verifySeparately", x => VerifySeparately = x) ||
@@ -1508,7 +1508,10 @@ order in which implementations are verified (default: N = 1).
 
      {:id <string>}
        Assign a unique ID to an implementation to be used for verification
-       result caching (default: ""<impl. name>:0"").
+       result caching (default: ""<impl. name>:0""), or assign a unique ID
+       to a statement or contract clause for use in identifying which program
+       elements were necessary to complete verification. The latter form is
+       used by the `/trackVerificationCoverage` option.
 
      {:timeLimit N}
        Set the time limit for verifying a given implementation.
@@ -1896,6 +1899,13 @@ without requiring the user to actually make those changes.
                 This option is implemented by renaming variables and reordering
                 declarations in the input, and by setting solver options that have
                 similar effects.
+  /trackVerificationCoverage
+                Track and report which program elements labeled with an
+                `{:id ...}` attribute were necessary to complete verification.
+                Assumptions, assertions, requires clauses, ensures clauses,
+                assignments, and calls can be labeled for inclusion in this
+                report. This generalizes and replaces the previous
+                (undocumented) `/printNecessaryAssertions` option.
 
   ---- Verification-condition splitting --------------------------------------
 

Source/ExecutionEngine/ExecutionEngine.cs

@@ -673,8 +673,8 @@ private async Task<PipelineOutcome> VerifyEachImplementation(TextWriter output,
         CleanupRequest(requestId);
       }
 
-      if (Options.PrintNecessaryAssumes && processedProgram.Program.NecessaryAssumes.Any()) {
-        Options.OutputWriter.WriteLine("Necessary assume command(s): {0}", string.Join(", ", processedProgram.Program.NecessaryAssumes.OrderBy(s => s)));
+      if (Options.TrackVerificationCoverage && processedProgram.Program.AllCoveredElements.Any()) {
+        Options.OutputWriter.WriteLine("Elements covered by verification: {0}", string.Join(", ", processedProgram.Program.AllCoveredElements.OrderBy(s => s)));
       }
 
       cce.NonNull(Options.TheProverFactory).Close();

Source/ExecutionEngine/ExecutionEngine.csproj

@@ -21,6 +21,7 @@
     <ProjectReference Include="..\Houdini\Houdini.csproj" />
     <ProjectReference Include="..\Model\Model.csproj" />
     <ProjectReference Include="..\VCGeneration\VCGeneration.csproj" />
+    <ProjectReference Include="..\Provers\SMTLib\SMTLib.csproj" />
   </ItemGroup>
 
 </Project>

Source/ExecutionEngine/VerificationResult.cs

@@ -11,7 +11,7 @@ public sealed class VerificationResult
 {
   private readonly Implementation implementation;
   public readonly string ProgramId;
-  public string MessageIfVerifies => implementation.FindStringAttribute("msg_if_verifies");
+  public string MessageIfVerifies => (implementation as ICarriesAttributes).FindStringAttribute("msg_if_verifies");
   public string Checksum => implementation.Checksum;
   public string DependenciesChecksum => implementation.DependencyChecksum;
 

Source/Houdini/HoudiniSession.cs

@@ -126,6 +126,7 @@ public class HoudiniStatistics
     private readonly Houdini houdini;
     public HoudiniStatistics stats;
     public List<Counterexample> Counterexamples { get; } = new();
+    public HashSet<string> CoveredElements { get; } = new();
     private VCExpr conjecture;
     private ProverInterface.ErrorHandler handler;
     ConditionGeneration.VerificationResultCollector collector;

Source/Provers/SMTLib/ProverInterface.cs

@@ -112,7 +112,7 @@ protected ErrorHandler(SMTLibOptions options)
       this.options = options;
     }
 
-    public virtual void AddNecessaryAssume(string id)
+    public virtual void AddCoveredElement(string id)
     {
       throw new System.NotImplementedException();
     }

Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs

@@ -223,18 +223,18 @@ public async Task<Outcome> CheckSat(CancellationToken cancellationToken,
               if (resp.Name != "")
               {
                 usedNamedAssumes.Add(resp.Name);
-                if (libOptions.PrintNecessaryAssumes)
+                if (libOptions.TrackVerificationCoverage)
                 {
-                  reporter.AddNecessaryAssume(resp.Name.Substring("aux$$assume$$".Length));
+                  reporter.AddCoveredElement(resp.Name.Substring("aux$$assume$$".Length));
                 }
               }
 
               foreach (var arg in resp.Arguments)
               {
                 usedNamedAssumes.Add(arg.Name);
-                if (libOptions.PrintNecessaryAssumes)
+                if (libOptions.TrackVerificationCoverage)
                 {
-                  reporter.AddNecessaryAssume(arg.Name.Substring("aux$$assume$$".Length));
+                  reporter.AddCoveredElement(arg.Name.Substring("aux$$assume$$".Length));
                 }
               }
             }

Source/Provers/SMTLib/SMTLibLineariser.cs

@@ -239,7 +239,7 @@ public string ExtractBuiltin(Function f)
     {
       Contract.Requires(f != null);
       string retVal = null;
-      retVal = f.FindStringAttribute("bvbuiltin");
+      retVal = (f as ICarriesAttributes).FindStringAttribute("bvbuiltin");
 
       // It used to be "sign_extend 12" in Simplify, and is "(_ sign_extend 12)" with SMT
       if (retVal != null && (retVal.StartsWith("sign_extend ") || retVal.StartsWith("zero_extend ")))
@@ -249,7 +249,7 @@ public string ExtractBuiltin(Function f)
 
       if (retVal == null)
       {
-        retVal = f.FindStringAttribute("builtin");
+        retVal = (f as ICarriesAttributes).FindStringAttribute("builtin");
       }
 
       if (retVal != null && !LibOptions.UseArrayTheory && SMTLibOpLineariser.ArrayOps.Contains(retVal))
@@ -398,7 +398,7 @@ public bool Visit(VCExprNAry node, LineariserOptions options)
         return true;
       }
 
-      if (node.Op.Equals(VCExpressionGenerator.NamedAssumeOp))
+      if (node.Op.Equals(VCExpressionGenerator.NamedAssumeOp) || node.Op.Equals(VCExpressionGenerator.NamedAssertOp))
       {
         var exprVar = node[0] as VCExprVar;
         NamedAssumes.Add(exprVar);

Source/Provers/SMTLib/SMTLibOptions.cs

@@ -14,7 +14,7 @@ public interface SMTLibOptions : CoreOptions
     bool ProduceUnsatCores { get; }
     bool ImmediatelyAcceptCommands { get; }
     bool RunningBoogieFromCommandLine { get; }
-    bool PrintNecessaryAssumes { get; }
+    bool TrackVerificationCoverage { get; }
     string ProverPreamble { get; }
     bool TraceDiagnosticsOnTimeout { get; }
     uint TimeLimitPerAssertionInPercent { get; }

Source/Provers/SMTLib/TypeDeclCollector.cs

@@ -212,11 +212,11 @@ public override bool Visit(VCExprNAry node, bool arg)
         AddDeclaration(string.Format("(declare-fun {0} () Bool)", exprVar.Name));
         AddDeclaration(string.Format("(assert-soft {0} :weight {1})", exprVar.Name, ((VCExprSoftOp) node.Op).Weight));
       }
-      else if (node.Op.Equals(VCExpressionGenerator.NamedAssumeOp))
+      else if (node.Op.Equals(VCExpressionGenerator.NamedAssumeOp) || node.Op.Equals(VCExpressionGenerator.NamedAssertOp))
       {
         var exprVar = node[0] as VCExprVar;
         AddDeclaration(string.Format("(declare-fun {0} () Bool)", exprVar.Name));
-        if (options.PrintNecessaryAssumes)
+        if (options.TrackVerificationCoverage)
         {
           AddDeclaration(string.Format("(assert (! {0} :named {1}))", exprVar.Name, "aux$$" + exprVar.Name));
         }
@@ -270,8 +270,7 @@ public override bool Visit(VCExprVar node, bool arg)
         RegisterType(node.Type);
         string decl =
           "(declare-fun " + printedName + " () " + TypeToString(node.Type) + ")";
-        if (!(printedName.StartsWith("assume$$") || printedName.StartsWith("soft$$") ||
-              printedName.StartsWith("try$$")))
+        if (node.VarKind == VCExprVarKind.Normal)
         {
           AddDeclaration(decl);
         }

Source/VCExpr/QuantifierInstantiationEngine.cs

@@ -1,4 +1,5 @@
 using System;
+using System.Collections.Concurrent;
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
 using System.Linq;
@@ -50,7 +51,7 @@ public QuantifierInstantiationInfo(Dictionary<VCExprVar, HashSet<string>> boundV
     private string skolemConstantNamePrefix;
     internal VCExpressionGenerator vcExprGen;
     private Boogie2VCExprTranslator exprTranslator;
-    internal static Dictionary<string, Type> labelToType = new();
+    internal static ConcurrentDictionary<string, Type> labelToType = new();
 
     public static VCExpr Instantiate(Implementation impl, VCExpressionGenerator vcExprGen, Boogie2VCExprTranslator exprTranslator, VCExpr vcExpr)
     {