Rename VCGen

Source/ExecutionEngine/ExecutionEngine.cs

@@ -19,7 +19,7 @@
 
 namespace Microsoft.Boogie
 {
- public record ProcessedProgram(Program Program, Action<VCGen, Implementation, ImplementationRunResult> PostProcessResult) {
+ public record ProcessedProgram(Program Program, Action<VerificationConditionGenerator, Implementation, ImplementationRunResult> PostProcessResult) {
  public ProcessedProgram(Program program) : this(program, (_, _, _) => { }) {
  }
  }
@@ -880,7 +880,7 @@ private IObservable<IVerificationStatus> VerifyImplementationWithoutCaching(Proc
  var batchCompleted = new Subject<(Split split, VerificationRunResult vcResult)>();
  var completeVerification = largeThreadTaskFactory.StartNew(async () =>
  {
- var vcgen = new VCGen(processedProgram.Program, checkerPool);
+ var vcgen = new VerificationConditionGenerator(processedProgram.Program, checkerPool);
  vcgen.CachingActionCounts = stats.CachingActionCounts;
  verificationResult.ProofObligationCountBefore = vcgen.CumulativeAssertionCount;
  verificationResult.Start = DateTime.UtcNow;

Source/Houdini/Houdini.cs

@@ -393,7 +393,7 @@ public class Houdini : ObservableHoudini
  {
  protected Program program;
  protected HashSet<Variable> houdiniConstants;
- protected VCGen vcgen;
+ protected VerificationConditionGenerator vcgen;
  protected ProverInterface proverInterface;
  protected Graph<Implementation> callGraph;
  protected HashSet<Implementation> vcgenFailures;
@@ -470,7 +470,7 @@ protected void Initialize(TextWriter traceWriter, Program program, HoudiniSessio
  */
 
  var checkerPool = new CheckerPool(Options);
- this.vcgen = new VCGen(program, checkerPool);
+ this.vcgen = new VerificationConditionGenerator(program, checkerPool);
  this.proverInterface = ProverInterface.CreateProver(Options, program, Options.ProverLogFilePath,
  Options.ProverLogFileAppend, Options.TimeLimit, taskID: GetTaskID());
 

Source/Houdini/HoudiniSession.cs

@@ -156,7 +156,7 @@ public bool InUnsatCore(Variable constant)
  return false;
  }
 
- public HoudiniSession(Houdini houdini, VCGen vcgen, ProverInterface proverInterface, Program program,
+ public HoudiniSession(Houdini houdini, VerificationConditionGenerator vcgen, ProverInterface proverInterface, Program program,
  ImplementationRun run, HoudiniStatistics stats, int taskID = -1)
  {
  var impl = run.Implementation;
@@ -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, impl.debugInfos, collector,
+ handler = new VerificationConditionGenerator.ErrorReporter(this.houdini.Options, gotoCmdOrigins, absyIds, impl.Blocks, impl.debugInfos, collector,
  mvInfo, proverInterface.Context, program, this);
  }
 

Source/VCGeneration/CommandTransformations.cs

@@ -9,7 +9,7 @@ public static Cmd AssertIntoAssume(VCGenOptions options, Cmd c)
  {
  if (c is AssertCmd assrt)
  {
- return VCGen.AssertTurnedIntoAssume(options, assrt);
+ return VerificationConditionGenerator.AssertTurnedIntoAssume(options, assrt);
  }
 
  return c;

Source/VCGeneration/Counterexample.cs

@@ -196,7 +196,7 @@ public void Print(int indent, TextWriter tw, Action<Block> blockAction = null)
  {
  var cmd = GetTraceCmd(loc);
  var calleeName = GetCalledProcName(cmd);
- if (calleeName.StartsWith(VC.StratifiedVCGenBase.recordProcName) &&
+ if (calleeName.StartsWith(VC.StratifiedVerificationConditionGeneratorBase.recordProcName) &&
  options.StratifiedInlining > 0)
  {
  Contract.Assert(calleeCounterexamples[loc].args.Count == 1);

Source/VCGeneration/FocusAttribute.cs

@@ -15,7 +15,7 @@ namespace VCGeneration;
 
 public static class FocusAttribute
 {
- public static List<Split> FocusImpl(VCGenOptions options, ImplementationRun run, Dictionary<TransferCmd, ReturnCmd> gotoCmdOrigins, VCGen par)
+ public static List<Split> FocusImpl(VCGenOptions options, ImplementationRun run, Dictionary<TransferCmd, ReturnCmd> gotoCmdOrigins, VerificationConditionGenerator par)
  {
  bool IsFocusCmd(Cmd c) {
  return c is PredicateCmd p && QKeyValue.FindBoolAttribute(p.Attributes, "focus");

Source/VCGeneration/ManualSplitFinder.cs

@@ -9,7 +9,7 @@ namespace VCGeneration;
 public static class ManualSplitFinder
 {
 
- public static List<Split> FocusAndSplit(VCGenOptions options, ImplementationRun run, Dictionary<TransferCmd, ReturnCmd> gotoCmdOrigins, VCGen par, bool splitOnEveryAssert)
+ public static List<Split> FocusAndSplit(VCGenOptions options, ImplementationRun run, Dictionary<TransferCmd, ReturnCmd> gotoCmdOrigins, VerificationConditionGenerator par, bool splitOnEveryAssert)
  {
  List<Split> focussedImpl = FocusAttribute.FocusImpl(options, run, gotoCmdOrigins, par);
  var splits = focussedImpl.Select(s => FindManualSplits(s, splitOnEveryAssert)).SelectMany(x => x).ToList();

Source/VCGeneration/SmokeTester.cs

@@ -24,15 +24,15 @@ void ObjectInvariant()
  Contract.Invariant(callback != null);
  }
 
- VCGen parent;
+ VerificationConditionGenerator parent;
  ImplementationRun run;
  Block initial;
  int id;
  Dictionary<Block, Block> copies = new Dictionary<Block, Block>();
  HashSet<Block> visited = new HashSet<Block>();
  VerifierCallback callback;
 
- internal SmokeTester(VCGen par, ImplementationRun run, VerifierCallback callback)
+ internal SmokeTester(VerificationConditionGenerator par, ImplementationRun run, VerifierCallback callback)
  {
  Contract.Requires(par != null);
  Contract.Requires(run != null);
@@ -130,7 +130,7 @@ Block CopyBlock(Block b)
  }
  else
  {
- seq.Add(VCGen.AssertTurnedIntoAssume(Options, turn));
+ seq.Add(VerificationConditionGenerator.AssertTurnedIntoAssume(Options, turn));
  }
  }
 

Source/VCGeneration/Split.cs

@@ -64,7 +64,7 @@ void ObjectInvariant()
 
  public Dictionary<TransferCmd, ReturnCmd> GotoCmdOrigins { get; }
 
- public readonly VCGen /*!*/ parent;
+ public readonly VerificationConditionGenerator /*!*/ parent;
 
  public Implementation /*!*/ Implementation => Run.Implementation;
 
@@ -84,11 +84,11 @@ void ObjectInvariant()
 
  // async interface
  public int SplitIndex { get; set; }
- internal VCGen.ErrorReporter reporter;
+ internal VerificationConditionGenerator.ErrorReporter reporter;
 
  public Split(VCGenOptions options, List<Block /*!*/> /*!*/ blocks,
  Dictionary<TransferCmd, ReturnCmd> /*!*/ gotoCmdOrigins,
- VCGen /*!*/ par, ImplementationRun run)
+ VerificationConditionGenerator /*!*/ par, ImplementationRun run)
  {
  Contract.Requires(cce.NonNullElements(blocks));
  Contract.Requires(gotoCmdOrigins != null);
@@ -616,7 +616,7 @@ List<Cmd> SliceCmds(Block b)
 
  if (swap)
  {
- theNewCmd = VCGen.AssertTurnedIntoAssume(Options, a);
+ theNewCmd = VerificationConditionGenerator.AssertTurnedIntoAssume(Options, a);
  }
  }
 
@@ -756,7 +756,7 @@ public Counterexample ToCounterexample(ProverContext context)
  Contract.Assert(c != null);
  if (c is AssertCmd)
  {
- var counterexample = VCGen.AssertCmdToCounterexample(Options, (AssertCmd) c, cce.NonNull(b.TransferCmd), trace, null, null, null, context, this);
+ var counterexample = VerificationConditionGenerator.AssertCmdToCounterexample(Options, (AssertCmd) c, cce.NonNull(b.TransferCmd), trace, null, null, null, context, this);
  Counterexamples.Add(counterexample);
  return counterexample;
  }
@@ -943,7 +943,7 @@ public async Task BeginCheck(TextWriter traceWriter, Checker checker, VerifierCa
 
  ProverContext ctx = checker.TheoremProver.Context;
  Boogie2VCExprTranslator bet = ctx.BoogieExprTranslator;
- var cc = new VCGen.CodeExprConversionClosure(traceWriter, checker.Pool.Options, absyIds, ctx);
+ var cc = new VerificationConditionGenerator.CodeExprConversionClosure(traceWriter, checker.Pool.Options, absyIds, ctx);
  bet.SetCodeExprConverter(cc.CodeExprToVerificationCondition);
 
  var exprGen = ctx.ExprGen;
@@ -957,7 +957,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, Implementation.debugInfos, callback,
+ reporter = new VerificationConditionGenerator.ErrorReporter(Options, GotoCmdOrigins, absyIds, Implementation.Blocks, Implementation.debugInfos, callback,
  mvInfo, checker.TheoremProver.Context, parent.program, this);
  }
 

Source/VCGeneration/SplitAndVerifyWorker.cs

@@ -31,7 +31,7 @@ class SplitAndVerifyWorker
  private bool TrackingProgress => DoSplitting && (callback.OnProgress != null || options.Trace); 
  private bool KeepGoing => maxKeepGoingSplits > 1;
 
- private VCGen vcGen;
+ private VerificationConditionGenerator verificationConditionGenerator;
  private VcOutcome vcOutcome;
  private double remainingCost;
  private double provenCost;
@@ -40,7 +40,7 @@ class SplitAndVerifyWorker
 
  private int totalResourceCount;
 
- public SplitAndVerifyWorker(VCGenOptions options, VCGen vcGen, ImplementationRun run,
+ public SplitAndVerifyWorker(VCGenOptions options, VerificationConditionGenerator verificationConditionGenerator, ImplementationRun run,
  Dictionary<TransferCmd, ReturnCmd> gotoCmdOrigins, VerifierCallback callback, ModelViewInfo mvInfo,
  VcOutcome vcOutcome)
  {
@@ -49,16 +49,16 @@ public SplitAndVerifyWorker(VCGenOptions options, VCGen vcGen, ImplementationRun
  this.mvInfo = mvInfo;
  this.run = run;
  this.vcOutcome = vcOutcome;
- this.vcGen = vcGen;
+ this.verificationConditionGenerator = verificationConditionGenerator;
  var maxSplits = options.VcsMaxSplits;
- VCGen.CheckIntAttributeOnImpl(run, "vcs_max_splits", ref maxSplits);
+ VerificationConditionGenerator.CheckIntAttributeOnImpl(run, "vcs_max_splits", ref maxSplits);
 
  maxKeepGoingSplits = options.VcsMaxKeepGoingSplits;
- VCGen.CheckIntAttributeOnImpl(run, "vcs_max_keep_going_splits", ref maxKeepGoingSplits);
+ VerificationConditionGenerator.CheckIntAttributeOnImpl(run, "vcs_max_keep_going_splits", ref maxKeepGoingSplits);
 
  maxVcCost = options.VcsMaxCost;
  var tmpMaxVcCost = -1;
- VCGen.CheckIntAttributeOnImpl(run, "vcs_max_cost", ref tmpMaxVcCost);
+ VerificationConditionGenerator.CheckIntAttributeOnImpl(run, "vcs_max_cost", ref tmpMaxVcCost);
  if (tmpMaxVcCost >= 0)
  {
  maxVcCost = tmpMaxVcCost;
@@ -68,7 +68,7 @@ public SplitAndVerifyWorker(VCGenOptions options, VCGen vcGen, ImplementationRun
  Implementation.CheckBooleanAttribute("vcs_split_on_every_assert", ref splitOnEveryAssert);
 
  ResetPredecessors(Implementation.Blocks);
- manualSplits = ManualSplitFinder.FocusAndSplit(options, run, gotoCmdOrigins, vcGen, splitOnEveryAssert);
+ manualSplits = ManualSplitFinder.FocusAndSplit(options, run, gotoCmdOrigins, verificationConditionGenerator, splitOnEveryAssert);
 
  if (manualSplits.Count == 1 && maxSplits > 1) {
  manualSplits = Split.DoSplit(manualSplits[0], maxVcCost, maxSplits);

Source/VCGeneration/StratifiedVC.cs

@@ -348,7 +348,7 @@ public override string ToString()
  public class StratifiedInliningInfo
  {
  private VCGenOptions options;
- public StratifiedVCGenBase vcgen;
+ public StratifiedVerificationConditionGeneratorBase vcgen;
  public ImplementationRun run;
  public Function function;
  public Variable controlFlowVariable;
@@ -370,10 +370,10 @@ public class StratifiedInliningInfo
 
  public Implementation Implementation => run.Implementation;
 
- public StratifiedInliningInfo(VCGenOptions options, ImplementationRun run, StratifiedVCGenBase stratifiedVcGen,
+ public StratifiedInliningInfo(VCGenOptions options, ImplementationRun run, StratifiedVerificationConditionGeneratorBase stratifiedVerificationConditionGenerator,
  Action<Implementation> PassiveImplInstrumentation)
  {
- vcgen = stratifiedVcGen;
+ vcgen = stratifiedVerificationConditionGenerator;
  this.PassiveImplInstrumentation = PassiveImplInstrumentation;
  this.run = run;
  this.options = options;
@@ -655,7 +655,7 @@ public void GenerateVC()
 
  var absyIds = new ControlFlowIdMap<Absy>();
 
- VCGen.CodeExprConversionClosure cc = new VCGen.CodeExprConversionClosure(run.OutputWriter, options, absyIds, proverInterface.Context);
+ VerificationConditionGenerator.CodeExprConversionClosure cc = new VerificationConditionGenerator.CodeExprConversionClosure(run.OutputWriter, options, absyIds, proverInterface.Context);
  translator.SetCodeExprConverter(cc.CodeExprToVerificationCondition);
  vcexpr = gen.Not(vcgen.GenerateVCAux(Implementation, controlFlowVariableExpr, absyIds, proverInterface.Context));
 
@@ -702,14 +702,14 @@ public void GenerateVC()
  }
 
  // This class is derived and used by Corral to create VCs for Stratified Inlining.
- public abstract class StratifiedVCGenBase : VCGen
+ public abstract class StratifiedVerificationConditionGeneratorBase : VerificationConditionGenerator
  {
  public readonly static string recordProcName = "boogie_si_record";
  public readonly static string callSiteVarAttr = "callSiteVar";
  public Dictionary<string, StratifiedInliningInfo> implName2StratifiedInliningInfo;
  public ProverInterface prover;
 
- public StratifiedVCGenBase(TextWriter traceWriter, VCGenOptions options, Program program, string logFilePath /*?*/, bool appendLogFile, CheckerPool checkerPool,
+ public StratifiedVerificationConditionGeneratorBase(TextWriter traceWriter, VCGenOptions options, Program program, string logFilePath /*?*/, bool appendLogFile, CheckerPool checkerPool,
  Action<Implementation> PassiveImplInstrumentation)
  : base(program, checkerPool)
  {

Source/VCGeneration/VCGen.cs → Source/VCGeneration/VerificationConditionGenerator.cs

@@ -18,14 +18,14 @@ namespace VC
  using Bpl = Microsoft.Boogie;
  using System.Threading.Tasks;
 
- public class VCGen : ConditionGeneration
+ public class VerificationConditionGenerator : ConditionGeneration
  {
 
  /// <summary>
  /// Constructor. Initializes the theorem prover.
  /// </summary>
  [NotDelayed]
- public VCGen(Program program, CheckerPool checkerPool)
+ public VerificationConditionGenerator(Program program, CheckerPool checkerPool)
  : base(program, checkerPool)
  {
  Contract.Requires(program != null);
@@ -89,7 +89,7 @@ public CodeExprConversionClosure(TextWriter traceWriter, VCGenOptions options, C
 
  public VCExpr CodeExprToVerificationCondition(CodeExpr codeExpr, List<VCExprLetBinding> bindings, bool isPositiveContext, Dictionary<Cmd, List<object>> debugInfos)
  {
- VCGen vcgen = new VCGen(new Program(), new CheckerPool(options));
+ VerificationConditionGenerator vcgen = new VerificationConditionGenerator(new Program(), new CheckerPool(options));
  vcgen.variable2SequenceNumber = new Dictionary<Variable, int>();
  vcgen.incarnationOriginMap = new Dictionary<Incarnation, Absy>();
  vcgen.CurrentLocalVariables = codeExpr.LocVars;