From 97098d6c4bb8958c0f89edb059010c0e3e195bf1 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 26 Jan 2024 15:36:38 +0100 Subject: [PATCH] Rename VCGen --- Source/ExecutionEngine/ExecutionEngine.cs | 4 ++-- Source/Houdini/Houdini.cs | 4 ++-- Source/Houdini/HoudiniSession.cs | 4 ++-- Source/VCGeneration/CommandTransformations.cs | 2 +- Source/VCGeneration/Counterexample.cs | 2 +- Source/VCGeneration/FocusAttribute.cs | 2 +- Source/VCGeneration/ManualSplitFinder.cs | 2 +- Source/VCGeneration/SmokeTester.cs | 6 +++--- Source/VCGeneration/Split.cs | 14 +++++++------- Source/VCGeneration/SplitAndVerifyWorker.cs | 14 +++++++------- Source/VCGeneration/StratifiedVC.cs | 12 ++++++------ ...{VCGen.cs => VerificationConditionGenerator.cs} | 6 +++--- 12 files changed, 36 insertions(+), 36 deletions(-) rename Source/VCGeneration/{VCGen.cs => VerificationConditionGenerator.cs} (99%) diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 467cca178..127763000 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -19,7 +19,7 @@ namespace Microsoft.Boogie { - public record ProcessedProgram(Program Program, Action PostProcessResult) { + public record ProcessedProgram(Program Program, Action PostProcessResult) { public ProcessedProgram(Program program) : this(program, (_, _, _) => { }) { } } @@ -880,7 +880,7 @@ private IObservable 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; diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index 81b82c0cb..11a51b434 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -393,7 +393,7 @@ public class Houdini : ObservableHoudini { protected Program program; protected HashSet houdiniConstants; - protected VCGen vcgen; + protected VerificationConditionGenerator vcgen; protected ProverInterface proverInterface; protected Graph callGraph; protected HashSet 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()); diff --git a/Source/Houdini/HoudiniSession.cs b/Source/Houdini/HoudiniSession.cs index 2d14561af..5c1032115 100644 --- a/Source/Houdini/HoudiniSession.cs +++ b/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); } diff --git a/Source/VCGeneration/CommandTransformations.cs b/Source/VCGeneration/CommandTransformations.cs index a39bac235..74daf7195 100644 --- a/Source/VCGeneration/CommandTransformations.cs +++ b/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; diff --git a/Source/VCGeneration/Counterexample.cs b/Source/VCGeneration/Counterexample.cs index 457568fdd..11e5ff3d9 100644 --- a/Source/VCGeneration/Counterexample.cs +++ b/Source/VCGeneration/Counterexample.cs @@ -196,7 +196,7 @@ public void Print(int indent, TextWriter tw, Action 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); diff --git a/Source/VCGeneration/FocusAttribute.cs b/Source/VCGeneration/FocusAttribute.cs index e08874579..72c3c76c8 100644 --- a/Source/VCGeneration/FocusAttribute.cs +++ b/Source/VCGeneration/FocusAttribute.cs @@ -15,7 +15,7 @@ namespace VCGeneration; public static class FocusAttribute { - public static List FocusImpl(VCGenOptions options, ImplementationRun run, Dictionary gotoCmdOrigins, VCGen par) + public static List FocusImpl(VCGenOptions options, ImplementationRun run, Dictionary gotoCmdOrigins, VerificationConditionGenerator par) { bool IsFocusCmd(Cmd c) { return c is PredicateCmd p && QKeyValue.FindBoolAttribute(p.Attributes, "focus"); diff --git a/Source/VCGeneration/ManualSplitFinder.cs b/Source/VCGeneration/ManualSplitFinder.cs index 76c3922d6..5646d71fa 100644 --- a/Source/VCGeneration/ManualSplitFinder.cs +++ b/Source/VCGeneration/ManualSplitFinder.cs @@ -9,7 +9,7 @@ namespace VCGeneration; public static class ManualSplitFinder { - public static List FocusAndSplit(VCGenOptions options, ImplementationRun run, Dictionary gotoCmdOrigins, VCGen par, bool splitOnEveryAssert) + public static List FocusAndSplit(VCGenOptions options, ImplementationRun run, Dictionary gotoCmdOrigins, VerificationConditionGenerator par, bool splitOnEveryAssert) { List focussedImpl = FocusAttribute.FocusImpl(options, run, gotoCmdOrigins, par); var splits = focussedImpl.Select(s => FindManualSplits(s, splitOnEveryAssert)).SelectMany(x => x).ToList(); diff --git a/Source/VCGeneration/SmokeTester.cs b/Source/VCGeneration/SmokeTester.cs index 7d46790d9..a56cd5ff6 100644 --- a/Source/VCGeneration/SmokeTester.cs +++ b/Source/VCGeneration/SmokeTester.cs @@ -24,7 +24,7 @@ void ObjectInvariant() Contract.Invariant(callback != null); } - VCGen parent; + VerificationConditionGenerator parent; ImplementationRun run; Block initial; int id; @@ -32,7 +32,7 @@ void ObjectInvariant() HashSet visited = new HashSet(); 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)); } } diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Split.cs index 2a78cd4dd..fdcf1e80f 100644 --- a/Source/VCGeneration/Split.cs +++ b/Source/VCGeneration/Split.cs @@ -64,7 +64,7 @@ void ObjectInvariant() public Dictionary 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 /*!*/ blocks, Dictionary /*!*/ gotoCmdOrigins, - VCGen /*!*/ par, ImplementationRun run) + VerificationConditionGenerator /*!*/ par, ImplementationRun run) { Contract.Requires(cce.NonNullElements(blocks)); Contract.Requires(gotoCmdOrigins != null); @@ -616,7 +616,7 @@ List 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); } diff --git a/Source/VCGeneration/SplitAndVerifyWorker.cs b/Source/VCGeneration/SplitAndVerifyWorker.cs index a74eefaac..7409ca17e 100644 --- a/Source/VCGeneration/SplitAndVerifyWorker.cs +++ b/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 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); diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index beb082cb5..5a296ffc4 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/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 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(); - 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 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 PassiveImplInstrumentation) : base(program, checkerPool) { diff --git a/Source/VCGeneration/VCGen.cs b/Source/VCGeneration/VerificationConditionGenerator.cs similarity index 99% rename from Source/VCGeneration/VCGen.cs rename to Source/VCGeneration/VerificationConditionGenerator.cs index bbf7dc0ce..a74738744 100644 --- a/Source/VCGeneration/VCGen.cs +++ b/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 { /// /// Constructor. Initializes the theorem prover. /// [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 bindings, bool isPositiveContext, Dictionary> debugInfos) { - VCGen vcgen = new VCGen(new Program(), new CheckerPool(options)); + VerificationConditionGenerator vcgen = new VerificationConditionGenerator(new Program(), new CheckerPool(options)); vcgen.variable2SequenceNumber = new Dictionary(); vcgen.incarnationOriginMap = new Dictionary(); vcgen.CurrentLocalVariables = codeExpr.LocVars;