diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 86735f524..e556913b8 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -6,6 +6,7 @@ on: env: SOLUTION: source/Corral.sln + BOOGIESOLUTION: boogie/Source/Boogie.sln jobs: job0: @@ -29,6 +30,8 @@ jobs: cd $GITHUB_WORKSPACE # Restore dotnet tools dotnet tool restore + # Build custom Boogie + dotnet build ${BOOGIESOLUTION} # Build Corral dotnet build -p:Version=$VERSION -c Release ${SOLUTION} # Create packages diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 3952441c4..b803d2b2a 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -4,6 +4,7 @@ on: [push, pull_request, workflow_dispatch] env: SOLUTION: source/Corral.sln + BOOGIESOLUTION: boogie/Source/Boogie.sln Z3URL: https://github.com/Z3Prover/z3/releases/download/z3-4.8.8/z3-4.8.8-x64-ubuntu-16.04.zip jobs: @@ -32,6 +33,8 @@ jobs: cd $GITHUB_WORKSPACE # Restore dotnet tools dotnet tool restore + # Build custom Boogie + dotnet build ${BOOGIESOLUTION} # Build Corral dotnet build -c ${{ matrix.configuration }} ${SOLUTION} # Run regression tests diff --git a/.gitignore b/.gitignore index b51e57128..29e703f68 100644 Binary files a/.gitignore and b/.gitignore differ diff --git a/.gitmodules b/.gitmodules new file mode 100644 index 000000000..0e40dd9f0 --- /dev/null +++ b/.gitmodules @@ -0,0 +1,4 @@ +[submodule "boogie"] + path = boogie + url = https://github.com/Dargones/boogie.git + branch = SyncWithCorral diff --git a/boogie b/boogie new file mode 160000 index 000000000..9c7cdeb41 --- /dev/null +++ b/boogie @@ -0,0 +1 @@ +Subproject commit 9c7cdeb41a90a79df1872e01ccca35882bcad95d diff --git a/source/CoreLib/AbstractHoudini.cs b/source/CoreLib/AbstractHoudini.cs index 1fb179e09..8bc910745 100644 --- a/source/CoreLib/AbstractHoudini.cs +++ b/source/CoreLib/AbstractHoudini.cs @@ -11,7 +11,10 @@ using Bpl = Microsoft.Boogie; using System.Diagnostics; using System.Diagnostics.Contracts; +using System.IO; +using System.Threading; using Microsoft.Boogie.GraphUtil; +using Microsoft.Boogie.SMTLib; namespace CoreLib { @@ -48,8 +51,9 @@ public AbstractHoudini(Program program) this.impl2Summary = new Dictionary(); this.name2Impl = BoogieUtil.nameImplMapping(program); - this.vcgen = new VCGen(program, CommandLineOptions.Clo.ProverLogFilePath, CommandLineOptions.Clo.ProverLogFileAppend, new List()); - this.prover = ProverInterface.CreateProver(program, CommandLineOptions.Clo.ProverLogFilePath, CommandLineOptions.Clo.ProverLogFileAppend, CommandLineOptions.Clo.TimeLimit); + var checkerPool = new CheckerPool(CommandLineOptions.Clo); + this.vcgen = new VCGen(program, checkerPool); + this.prover = ProverInterface.CreateProver(CommandLineOptions.Clo, program, CommandLineOptions.Clo.ProverLogFilePath, CommandLineOptions.Clo.ProverLogFileAppend, CommandLineOptions.Clo.TimeLimit); this.reporter = new AbstractHoudiniErrorReporter(); var impls = new List( @@ -180,8 +184,7 @@ private bool ProcessImpl(Implementation impl) //Console.WriteLine("Checking: {0}", vc); - prover.BeginCheck(impl.Name, vc, reporter); - ProverInterface.Outcome proverOutcome = prover.CheckOutcome(reporter); + ProverInterface.Outcome proverOutcome= prover.Check(impl.Name, vc, reporter, 1, CancellationToken.None).Result; if (reporter.model == null) break; @@ -312,13 +315,13 @@ private void attachEnsures(Implementation impl) private void GenVC(Implementation impl) { ModelViewInfo mvInfo; - Dictionary label2absy; + ControlFlowIdMap label2absy = new ControlFlowIdMap(); vcgen.ConvertCFG2DAG(impl); - vcgen.PassifyImpl(impl, out mvInfo); + vcgen.PassifyImpl(new ImplementationRun(impl, TextWriter.Null), out mvInfo); var gen = prover.VCExprGen; - var vcexpr = vcgen.GenerateVC(impl, null, out label2absy, prover.Context); + var vcexpr = vcgen.GenerateVC(impl, null, label2absy, prover.Context); // Create a macro so that the VC can sit with the theorem prover Macro macro = new Macro(Token.NoToken, impl.Name + "Macro", new List(), new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Bpl.Type.Bool), false)); @@ -803,7 +806,7 @@ class AbstractHoudiniErrorReporter : ProverInterface.ErrorHandler { public Model model; - public AbstractHoudiniErrorReporter() + public AbstractHoudiniErrorReporter(): base(CommandLineOptions.Clo) { model = null; } diff --git a/source/CoreLib/BoogieVerify.cs b/source/CoreLib/BoogieVerify.cs index e517ea014..3ac80d4f0 100644 --- a/source/CoreLib/BoogieVerify.cs +++ b/source/CoreLib/BoogieVerify.cs @@ -7,6 +7,7 @@ //using BoogiePL; using System.Diagnostics.Contracts; using System.IO; +using System.Threading; using VC; using cba.Util; @@ -116,7 +117,8 @@ public static ReturnStatus Verify(Program program, CommandLineOptions.Clo.RecursionBound = BoogieVerify.irreducibleLoopUnroll; // Do loop extraction - var extractionInfo = program.ExtractLoops(); + var extractionInfo = LoopExtractor + .ExtractLoops(CommandLineOptions.Clo, program).loops; // restore RB CommandLineOptions.Clo.RecursionBound = rb; @@ -191,7 +193,9 @@ public static ReturnStatus Verify(Program program, { var start = DateTime.Now; - outcome = vcgen.VerifyImplementation(impl, out errors); + var verificationResult = vcgen.VerifyImplementation(new ImplementationRun(impl, TextWriter.Null), CancellationToken.None).Result; + outcome = verificationResult.Item1; + errors = verificationResult.errors; var end = DateTime.Now; @@ -242,7 +246,7 @@ public static ReturnStatus Verify(Program program, Log.WriteLine(Log.Debug, outcome.ToString()); Log.WriteLine(Log.Debug, (errors == null ? 0 : errors.Count) + " counterexamples."); - if (errors != null) ret = ReturnStatus.NOK; + if (errors != null && errors.Count > 0) ret = ReturnStatus.NOK; // Print model if (errors != null && errors.Count > 0 && errors[0].Model != null && CommandLineOptions.Clo.ModelViewFile != null) @@ -272,7 +276,7 @@ public static ReturnStatus Verify(Program program, // Map the trace across loop extraction if (vcgen is VC.VCGen) { - errors[i] = (vcgen as VC.VCGen).extractLoopTrace(errors[i], impl.Name, program, extractionInfo); + errors[i] = (vcgen as VC.VCGen).ExtractLoopTrace(errors[i], impl.Name, program, extractionInfo); } if (errors[i] is AssertCounterexample) @@ -626,7 +630,7 @@ public static Counterexample ReconstructTrace(Counterexample trace, string currP { // find the corresponding call in origBlock var calleeInfo = trace.calleeCounterexamples[currLocation]; - var calleeName = trace.getCalledProcName(trace.Trace[currLocation.numBlock].Cmds[currLocation.numInstr]); + var calleeName = trace.GetCalledProcName(trace.Trace[currLocation.numBlock].Cmds[currLocation.numInstr]); while (currOrigInstr < currOrigBlock.Cmds.Count) { var cmd = currOrigBlock.Cmds[currOrigInstr] as CallCmd; @@ -649,7 +653,7 @@ public static Counterexample ReconstructTrace(Counterexample trace, string currP break; } - var ret = new AssertCounterexample(newTrace, null, null, trace.Model, trace.MvInfo, trace.Context); + var ret = new AssertCounterexample(CommandLineOptions.Clo, newTrace, null, null, trace.Model, trace.MvInfo, trace.Context, null); ret.calleeCounterexamples = newTraceCallees; return ret; @@ -703,7 +707,7 @@ public static void ReconstructImperativeTrace(Counterexample trace, string currP if (trace.calleeCounterexamples.ContainsKey(loc)) { Cmd c = b.Cmds[numInstr]; - var calleeName = trace.getCalledProcName(c); + var calleeName = trace.GetCalledProcName(c); var calleeTrace = trace.calleeCounterexamples[loc].counterexample; ReconstructImperativeTrace(calleeTrace, calleeName, origProg); calleeTraces.Add( diff --git a/source/CoreLib/CBAPasses.cs b/source/CoreLib/CBAPasses.cs index 8f24a7328..9dd75dc94 100644 --- a/source/CoreLib/CBAPasses.cs +++ b/source/CoreLib/CBAPasses.cs @@ -1120,16 +1120,19 @@ public override CBAProgram runCBAPass(CBAProgram p) foreach (var impl in BoogieUtil.GetImplementations(p)) { - impl.PruneUnreachableBlocks(); + impl.PruneUnreachableBlocks(CommandLineOptions.Clo); } // save RB var rb = CommandLineOptions.Clo.RecursionBound; if (BoogieVerify.irreducibleLoopUnroll >= 0) CommandLineOptions.Clo.RecursionBound = BoogieVerify.irreducibleLoopUnroll; - - var procsWithIrreducibleLoops = new HashSet(); - var passInfo = p.ExtractLoops(out procsWithIrreducibleLoops); + + var loopExtractionResult = LoopExtractor.ExtractLoops(CommandLineOptions.Clo, p); + var passInfo = loopExtractionResult.loops; + var procsWithIrreducibleLoops = + loopExtractionResult.procsWithIrreducibleLoops + .Select(implementation => implementation.Name).ToHashSet(); // restore RB CommandLineOptions.Clo.RecursionBound = rb; diff --git a/source/CoreLib/CompilerPass.cs b/source/CoreLib/CompilerPass.cs index 7846d65d8..0477d03a3 100644 --- a/source/CoreLib/CompilerPass.cs +++ b/source/CoreLib/CompilerPass.cs @@ -450,7 +450,7 @@ public static string mergeRecCalls(Implementation impl) .Iter(cc => { var str = new System.IO.StringWriter(); - var tt = new TokenTextWriter(str); + var tt = new TokenTextWriter(str, CommandLineOptions.Clo); cc.Emit(tt, 0); tt.Close(); callStr.Add(str.ToString()); @@ -538,9 +538,9 @@ public override CBAProgram runCBAPass(CBAProgram p) // Type information is needed in some cases. For instance, the Command // Mem[x] := untracked-expr is converted to havoc temp; Mem[x] := temp. Here // we need the type of "untracked-expr" or of "Mem[x]" - if (p.Typecheck() != 0) + if (p.Typecheck(CommandLineOptions.Clo) != 0) { - p.Emit(new TokenTextWriter("error.bpl")); + p.Emit(new TokenTextWriter("error.bpl", CommandLineOptions.Clo)); throw new InternalError("Type errors"); } vslice.VisitProgram(p as Program); @@ -712,9 +712,9 @@ private void doInlining(CBAProgram p) foreach (Declaration d in TopLevelDeclarations) { Implementation impl = d as Implementation; - if (impl != null && !impl.SkipVerification) + if (impl != null && !impl.IsSkipVerification(CommandLineOptions.Clo)) { - Inliner.ProcessImplementation(p as Program, impl); + Inliner.ProcessImplementation(CommandLineOptions.Clo, p, impl); } } foreach (Declaration d in TopLevelDeclarations) @@ -766,7 +766,7 @@ public static void InlineToDepth(Program program) } foreach (Implementation impl in impls) { - Inliner.ProcessImplementationForHoudini(program, impl); + Inliner.ProcessImplementationForHoudini(CommandLineOptions.Clo, program, impl); } foreach (Implementation impl in impls) { diff --git a/source/CoreLib/ConcurrentTrace.cs b/source/CoreLib/ConcurrentTrace.cs index 4d1874ab4..92d184f31 100644 --- a/source/CoreLib/ConcurrentTrace.cs +++ b/source/CoreLib/ConcurrentTrace.cs @@ -359,7 +359,7 @@ public static void printCTrace(PersistentCBAProgram program, ErrorTrace trace, s private static void setupPrint(PersistentCBAProgram program, ErrorTrace trace, string file) { // Set output files - pathFile = file == null ? null : new TokenTextWriter(file + "_trace.txt"); + pathFile = file == null ? null : new TokenTextWriter(file + "_trace.txt", CommandLineOptions.Clo); if(pathFile != null) program.writeToFile(file + ".bpl"); Program prog = program.getProgram(); diff --git a/source/CoreLib/ErrorTrace.cs b/source/CoreLib/ErrorTrace.cs index eec141420..8cdcd998b 100644 --- a/source/CoreLib/ErrorTrace.cs +++ b/source/CoreLib/ErrorTrace.cs @@ -1327,7 +1327,7 @@ public static void PrintStackTrace(Program p, ErrorTrace trace, string filename) stack = new List(); program = p; nameImplMap = BoogieUtil.nameImplMapping(program); - pathFile = new TokenTextWriter(filename); + pathFile = new TokenTextWriter(filename, CommandLineOptions.Clo); gcnt = 1; abortMessage = null; @@ -1506,8 +1506,8 @@ public static void Print(Program p, ErrorTrace trace, HashSet recorded, { program = p; nameImplMap = BoogieUtil.nameImplMapping(program); - pathFile = new TokenTextWriter(filename); - stackFile = new TokenTextWriter(stackFileName); + pathFile = new TokenTextWriter(filename, CommandLineOptions.Clo); + stackFile = new TokenTextWriter(stackFileName, CommandLineOptions.Clo); gcnt = 1; abortMessage = null; abortMessageLocation = null; @@ -1544,7 +1544,7 @@ public static void Print(Program p, ErrorTrace trace, HashSet recorded, if (scalarWrites.Count > 0) { - var scalarFile = new TokenTextWriter("scalars.txt"); + var scalarFile = new TokenTextWriter("scalars.txt", CommandLineOptions.Clo); scalarWrites.Iter(kvp => { scalarFile.Write("{0}: ", kvp.Key); @@ -1575,7 +1575,7 @@ public static void Print(Program p, ErrorTrace trace, HashSet recorded, memWrites.Iter(kvp => kvp.Value.Iter(line => lineWrites.InitAndAdd(line, kvp.Key))); - var memFile = new TokenTextWriter("mem1.txt"); + var memFile = new TokenTextWriter("mem1.txt", CommandLineOptions.Clo); var lines = new HashSet(); lineReads.Keys.Iter(line => lines.Add(line)); @@ -1592,7 +1592,7 @@ public static void Print(Program p, ErrorTrace trace, HashSet recorded, memFile.Close(); - memFile = new TokenTextWriter("mem2.txt"); + memFile = new TokenTextWriter("mem2.txt", CommandLineOptions.Clo); var addresses = new HashSet(); memReads.Keys.Iter(a => addresses.Add(a)); @@ -1619,7 +1619,7 @@ public static void Print(Program p, ErrorTrace trace, HashSet recorded, memWritesCS.Iter(kvp => kvp.Value.Iter(cs => stateWrites.InitAndAdd(cs, kvp.Key))); - memFile = new TokenTextWriter("mem3.txt"); + memFile = new TokenTextWriter("mem3.txt", CommandLineOptions.Clo); var states = new HashSet(); stateReads.Keys.Iter(s => states.Add(s)); @@ -1636,7 +1636,7 @@ public static void Print(Program p, ErrorTrace trace, HashSet recorded, memFile.Close(); - memFile = new TokenTextWriter("mem4.txt"); + memFile = new TokenTextWriter("mem4.txt", CommandLineOptions.Clo); foreach (var add in addresses) { @@ -1924,7 +1924,7 @@ public static void print(PersistentProgram program, ErrorTrace trace, string fil private static void setupPrint(PersistentProgram program, ErrorTrace trace, string file) { // Set output files - pathFile = new TokenTextWriter(file + "_trace.txt"); + pathFile = new TokenTextWriter(file + "_trace.txt", CommandLineOptions.Clo); program.writeToFile(file + ".bpl"); Program prog = program.getProgram(); @@ -2049,7 +2049,7 @@ public class InlineToTrace : Inliner private static Stack> traceStack = new Stack>(); public InlineToTrace(Program program, InlineCallback cb) - :base(program, cb, -1) + :base(program, cb, -1, CommandLineOptions.Clo) { } // Return callCmd -> callee trace @@ -2112,7 +2112,7 @@ public static void Inline(Program program, ErrorTrace trace) var inliner = new InlineToTrace(program, null); traceStack.Push(FindCallsOnTrace(entryPoint, trace)); - Inliner.ProcessImplementation(program, entryPoint, inliner); + Inliner.ProcessImplementation(CommandLineOptions.Clo, program, entryPoint); foreach (var impl in program.TopLevelDeclarations.OfType()) { diff --git a/source/CoreLib/HoudiniLite.cs b/source/CoreLib/HoudiniLite.cs index 7ce659bd8..8708255b1 100644 --- a/source/CoreLib/HoudiniLite.cs +++ b/source/CoreLib/HoudiniLite.cs @@ -4,12 +4,14 @@ using System.Text; using System.Threading.Tasks; using System.Diagnostics; +using System.Threading; using Microsoft.Boogie; using Microsoft.Boogie.VCExprAST; using VC; using Outcome = VC.VCGen.Outcome; using cba.Util; using Microsoft.Boogie.GraphUtil; +using Microsoft.Boogie.SMTLib; namespace CoreLib { @@ -150,6 +152,7 @@ public static HashSet RunHoudini(Program program, bool RobustAgainstEval HoudiniStats.Start("VCGen"); // VC Gen + VC.CheckerPool checkerPool = new CheckerPool(CommandLineOptions.Clo); var hi = new HoudiniInlining(program, CommandLineOptions.Clo.ProverLogFilePath, CommandLineOptions.Clo.ProverLogFileAppend, RewriteAssumedToAssertedAction); HoudiniStats.Stop("VCGen"); @@ -392,7 +395,7 @@ static HashSet ProveCandidates(ProverInterface prover, Dictionary ProveCandidates(ProverInterface prover, Dictionary ProveCandidates(ProverInterface prover, Dictionary var p = upperProg.getCBAProgram(); - if (p.Typecheck() != 0) + if (p.Typecheck(CommandLineOptions.Clo) != 0) { - p.Emit(new TokenTextWriter("error.bpl")); + p.Emit(new TokenTextWriter("error.bpl", CommandLineOptions.Clo)); throw new InternalError("Type errors"); } //BoogieUtil.PrintProgram(p, "RefineUp.bpl"); @@ -246,7 +246,7 @@ private void doRefinementInZ3Helper(out Program faProgProg, out HashSet //faProg.writeToFile("error.bpl"); faProgProg = faProg.getProgram(); - var t = faProgProg.Typecheck(); + var t = faProgProg.Typecheck(CommandLineOptions.Clo); Debug.Assert(t == 0); //BoogieUtil.PrintProgram(faProgProg, "refine.bpl"); @@ -305,9 +305,9 @@ public void doRefinement1() var upperProg = vp1.run(program); var p = upperProg.getCBAProgram(); - if (p.Typecheck() != 0) + if (p.Typecheck(CommandLineOptions.Clo) != 0) { - p.Emit(new TokenTextWriter("error.bpl")); + p.Emit(new TokenTextWriter("error.bpl", CommandLineOptions.Clo)); throw new InternalError("Type errors"); } @@ -319,7 +319,7 @@ public void doRefinement1() var faProgProg = faProg.getProgram(); - var t = faProgProg.Typecheck(); + var t = faProgProg.Typecheck(CommandLineOptions.Clo); Debug.Assert(t == 0); boolVars = BoogieVerify.FindLeastToVerify(faProgProg, boolVars); diff --git a/source/CoreLib/SdvUtils.cs b/source/CoreLib/SdvUtils.cs index 809e243ad..5fbd89b80 100644 --- a/source/CoreLib/SdvUtils.cs +++ b/source/CoreLib/SdvUtils.cs @@ -37,7 +37,7 @@ public SDVConcretizePathPass() public override CBAProgram runCBAPass(CBAProgram p) { - p.Typecheck(); + p.Typecheck(CommandLineOptions.Clo); p.TopLevelDeclarations.OfType().Iter(proc => procsWithoutBody.Add(proc.Name)); p.TopLevelDeclarations.OfType().Iter(impl => procsWithoutBody.Remove(impl.Name)); diff --git a/source/CoreLib/StratifiedInlining.cs b/source/CoreLib/StratifiedInlining.cs index 2c9b377c0..920317b73 100644 --- a/source/CoreLib/StratifiedInlining.cs +++ b/source/CoreLib/StratifiedInlining.cs @@ -4,12 +4,16 @@ using System.Linq; using System.Text; using System.Diagnostics; -using Microsoft.Boogie; + using System.IO; + using System.Threading; + using Microsoft.Boogie; using Microsoft.Boogie.VCExprAST; using VC; using Outcome = VC.VCGen.Outcome; using cba.Util; using Microsoft.Boogie.GraphUtil; + using Microsoft.Boogie.SMTLib; +using System.Threading.Tasks; namespace CoreLib { @@ -255,7 +259,7 @@ public void RunInitialAnalyses(Program prog) } public StratifiedInlining(Program program, string logFilePath, bool appendLogFile, Action PassiveImplInstrumentation) : - base(program, logFilePath, appendLogFile, new List(), PassiveImplInstrumentation) + base(TextWriter.Null, CommandLineOptions.Clo, program, logFilePath, appendLogFile, new CheckerPool(CommandLineOptions.Clo), PassiveImplInstrumentation) { stats = new Stats(); @@ -1304,7 +1308,7 @@ public List> AssertMustReach(StratifiedVC svc, HashSe var ret = new List>(); // This is most likely redundant - prover.Assert(svc.MustReach(svc.info.impl.Blocks[0]), true); + prover.Assert(svc.MustReach(svc.info.Implementation.Blocks[0], svc.info.absyIds), true); if (!attachedVCInv.ContainsKey(svc)) return ret; @@ -1318,28 +1322,28 @@ public List> AssertMustReach(StratifiedVC svc, HashSe var key = Tuple.Create(vc, callblock); if (prevAsserted != null && !prevAsserted.Contains(key)) { - prover.Assert(vc.MustReach(callblock), true); + prover.Assert(vc.MustReach(callblock, svc.info.absyIds), true); ret.Add(key); } iter = parent[iter]; } - prover.Assert(mainVC.MustReach(mainVC.callSites.First(tup => tup.Value.Contains(iter)).Key), true); + prover.Assert(mainVC.MustReach(mainVC.callSites.First(tup => tup.Value.Contains(iter)).Key, svc.info.absyIds), true); return ret; } public Outcome Bck(StratifiedVC svc, HashSet openCallSites, StratifiedInliningErrorReporter reporter, Dictionary backboneRecDepth) { - var outcome = Fwd(openCallSites, reporter, svc.info.impl.Name == mainProc.Name, CommandLineOptions.Clo.RecursionBound); + var outcome = Fwd(openCallSites, reporter, svc.info.Implementation.Name == mainProc.Name, CommandLineOptions.Clo.RecursionBound); if (outcome != Outcome.Errors) return outcome; - if (svc.info.impl.Name == mainProc.Name) + if (svc.info.Implementation.Name == mainProc.Name) return outcome; outcome = Outcome.Correct; var boundHit = false; - foreach (var caller in callGraph.callers[svc.info.impl.Proc]) + foreach (var caller in callGraph.callers[svc.info.Implementation.Proc]) { if (backboneRecDepth[caller.Name] == CommandLineOptions.Clo.RecursionBound) { @@ -1358,7 +1362,7 @@ public Outcome Bck(StratifiedVC svc, HashSet openCallSites, callerOpenCallSites.UnionWith(callerVC.CallSites); //Console.WriteLine("Adding call-sites: {0}", callerVC.CallSites.Select(s => s.callSiteExpr.ToString()).Concat(" ")); - foreach (var cs in callerVC.CallSites.Where(s => s.callSite.calleeName == svc.info.impl.Name)) + foreach (var cs in callerVC.CallSites.Where(s => s.callSite.calleeName == svc.info.Implementation.Name)) { Push(); @@ -1509,9 +1513,10 @@ void MustNotFail(StratifiedCallSite scs, StratifiedVC svc) /* verification */ - public override Outcome VerifyImplementation(Implementation impl, VerifierCallback callback) + public override Task VerifyImplementation(ImplementationRun run, VerifierCallback callback, CancellationToken cancellationToken) { startTime = DateTime.UtcNow; + var impl = run.Implementation; procsHitRecBound = new HashSet(); @@ -1528,11 +1533,11 @@ public override Outcome VerifyImplementation(Implementation impl, VerifierCallba * Otherwise, use forward approach */ if (cba.Util.BoogieVerify.options.useFwdBck && assertMethods.Count > 0) { - return FwdBckVerify(impl, callback); + return Task.FromResult(FwdBckVerify(impl, callback)); } else if (cba.Util.BoogieVerify.options.newStratifiedInliningAlgo.ToLower() == "duality") { - return DepthFirstStyle(impl, callback); + return Task.FromResult(DepthFirstStyle(impl, callback)); } MacroSI.PRINT_DEBUG("Starting forward approach..."); @@ -1714,7 +1719,7 @@ public override Outcome VerifyImplementation(Implementation impl, VerifierCallba } #endregion - return outcome; + return Task.FromResult(outcome); } static int dumpCnt = 0; @@ -1759,7 +1764,7 @@ private StratifiedVC Expand(StratifiedCallSite scs, string name, bool DoSubst, b toassert = prover.VCExprGen.And(prover.VCExprGen.Implies(cb, svc.vcexpr), toassert); } - prover.LogComment("Inlining " + scs.callSite.calleeName + " from " + (parent.ContainsKey(scs) ? attachedVC[parent[scs]].info.impl.Name : "main")); + prover.LogComment("Inlining " + scs.callSite.calleeName + " from " + (parent.ContainsKey(scs) ? attachedVC[parent[scs]].info.Implementation.Name : "main")); di.Expanded(scs, svc); stats.vcSize += SizeComputingVisitor.ComputeSize(toassert); @@ -1834,7 +1839,7 @@ private string GetPersistentID(StratifiedVC vc) var scs = attachedVCInv[vc]; ret = GetPersistentID(scs); } - return string.Format("{0}_262_{1}", ret, vc.info.impl.Name); + return string.Format("{0}_262_{1}", ret, vc.info.Implementation.Name); } // 'Attach' inlined from Boogie/StratifiedVC.cs (and made static) @@ -1865,20 +1870,20 @@ private Outcome CheckVC(ProverInterface.ErrorHandler reporter) { stats.calls++; var stopwatch = Stopwatch.StartNew(); - prover.Check(); + (prover as SMTLibInteractiveTheoremProver).currentErrorHandler = reporter; + ProverInterface.Outcome outcome = (prover as SMTLibInteractiveTheoremProver).CheckSat(CancellationToken.None, 1).Result; stats.time += stopwatch.ElapsedTicks; - ProverInterface.Outcome outcome = prover.CheckOutcomeCore(reporter); return ConditionGeneration.ProverInterfaceOutcomeToConditionGenerationOutcome(outcome); } private Outcome CheckVC(List softAssumptions, ProverInterface.ErrorHandler reporter) { - List unsatCore; stats.calls++; var stopwatch = Stopwatch.StartNew(); - ProverInterface.Outcome outcome = - prover.CheckAssumptions(new List(), softAssumptions, out unsatCore, reporter); + var task = prover.CheckAssumptions(new List(), softAssumptions, reporter, CancellationToken.None); + var unsatCore = task.Result.Item2; + ProverInterface.Outcome outcome = task.Result.Item1; stats.time += stopwatch.ElapsedTicks; return ConditionGeneration.ProverInterfaceOutcomeToConditionGenerationOutcome(outcome); } @@ -2170,7 +2175,7 @@ public DI(StratifiedInlining SI, bool disabled) { IndexC = new IndexComputer(SI.program); var impls = new Dictionary(); - SI.implName2StratifiedInliningInfo.Iter(tup => impls.Add(tup.Key, tup.Value.impl)); + SI.implName2StratifiedInliningInfo.Iter(tup => impls.Add(tup.Key, tup.Value.Implementation)); Disj = new ProgramDisjointness(impls); currentDag = new DagOracle(SI.program, Disj, SI.extraRecBound); @@ -2320,11 +2325,11 @@ public void RegisterMain(StratifiedVC vc) Debug.Assert(currentDag.Nodes.Count == 0); var rv = IndexC.GetMainRv(); - var index = IndexC.GetIndex(vc.info.impl.Name, rv); + var index = IndexC.GetIndex(vc.info.Implementation.Name, rv); vcToRecVector.Add(vc, rv); // Add to dag - var node = new DagOracle.DagNode(index, vc.info.impl.Name, 1); + var node = new DagOracle.DagNode(index, vc.info.Implementation.Name, 1); vcNodeMap.Add(vc, node); currentDag.AddNode(node); @@ -2348,7 +2353,7 @@ public void Expanded(StratifiedCallSite cs, StratifiedVC vc) RegisterVC(vc); if (disabled) return; - Debug.Assert(cs.callSite.calleeName == vc.info.impl.Name); + Debug.Assert(cs.callSite.calleeName == vc.info.Implementation.Name); var n1 = vcNodeMap[containingVC[cs]]; @@ -2357,7 +2362,7 @@ public void Expanded(StratifiedCallSite cs, StratifiedVC vc) vcToRecVector.Add(vc, rv2); // create node - var n2 = new DagOracle.DagNode(id2, vc.info.impl.Name, 1); + var n2 = new DagOracle.DagNode(id2, vc.info.Implementation.Name, 1); vcNodeMap.Add(vc, n2); currentDag.AddNode(n2); @@ -4072,6 +4077,10 @@ public int ComputeDagSizes() public class EmptyErrorReporter : ProverInterface.ErrorHandler { public override void OnModel(IList labels, Model model, ProverInterface.Outcome proverOutcome) { } + + public EmptyErrorReporter() : base(CommandLineOptions.Clo) + { + } } public class InsufficientDetailsToConstructCexPath : Exception @@ -4093,7 +4102,7 @@ public class StratifiedInliningErrorReporter : ProverInterface.ErrorHandler public List callSitesToExpand; List> orderedStateIds; - public StratifiedInliningErrorReporter(VerifierCallback callback, StratifiedInlining si, StratifiedVC mainVC) + public StratifiedInliningErrorReporter(VerifierCallback callback, StratifiedInlining si, StratifiedVC mainVC): base(CommandLineOptions.Clo) { this.callback = callback; this.si = si; @@ -4110,8 +4119,7 @@ public override int StartingProcId() private Absy Label2Absy(string procName, string label) { int id = int.Parse(label); - var l2a = si.implName2StratifiedInliningInfo[procName].label2absy; - return (Absy)l2a[id]; + return si.implName2StratifiedInliningInfo[procName].absyIds.fromId[id]; } public override void OnProverError(string message) @@ -4172,12 +4180,13 @@ private List GetAbsyTraceControlFlowVariable(StratifiedVC svc, IList(); foreach (var label in labels) { - ret.Add(Label2Absy(svc.info.impl.Name, label)); + ret.Add(Label2Absy(svc.info.Implementation.Name, label)); } return ret; } @@ -4187,7 +4196,7 @@ private List GetAbsyTraceBoolControlVC(StratifiedVC svc) Debug.Assert(CommandLineOptions.Clo.UseProverEvaluate, "Must use prover evaluate option with boolControlVC"); var ret = new List(); - var impl = svc.info.impl; + var impl = svc.info.Implementation; var block = impl.Blocks[0]; while (true) @@ -4198,7 +4207,7 @@ private List GetAbsyTraceBoolControlVC(StratifiedVC svc) Block next = null; foreach (var succ in gc.labelTargets) { - var succtaken = (bool)svc.info.vcgen.prover.Evaluate(svc.blockToControlVar[succ]); + var succtaken = (bool)svc.info.vcgen.prover.Evaluate(svc.blockToControlVar[succ]).Result; if (succtaken) { next = succ; @@ -4303,7 +4312,7 @@ calleeCounterexamples[new TraceLocation(trace.Count - 1, scs.callSite.numInstr)] } Block lastBlock = (Block)absyList[absyList.Count - 2]; - Counterexample newCounterexample = VC.VCGen.AssertCmdToCounterexample(assertCmd, lastBlock.TransferCmd, trace, null, model, svc.info.mvInfo, si.prover.Context); + Counterexample newCounterexample = VC.VCGen.AssertCmdToCounterexample(CommandLineOptions.Clo, assertCmd, lastBlock.TransferCmd, trace, null, model, svc.info.mvInfo, si.prover.Context, null); newCounterexample.AddCalleeCounterexample(calleeCounterexamples); return newCounterexample; } diff --git a/source/CoreLib/VariableSlice.cs b/source/CoreLib/VariableSlice.cs index 3f53a7919..623532bd5 100644 --- a/source/CoreLib/VariableSlice.cs +++ b/source/CoreLib/VariableSlice.cs @@ -147,7 +147,7 @@ public override Program VisitProgram(Program node) rest[i] = this.VisitDeclaration(rest[i]); // Remove globals that are not tracked - node.TopLevelDeclarations = globals.Where(x => isTrackedVariable(x as GlobalVariable)); + node.TopLevelDeclarations = globals.Where(x => isTrackedVariable(x as GlobalVariable)).ToList(); node.AddTopLevelDeclarations(rest); @@ -423,7 +423,7 @@ private Block sliceBlock(Block block) } else { - cmd.Emit(new TokenTextWriter(Console.Out), 0); + cmd.Emit(new TokenTextWriter(Console.Out, CommandLineOptions.Clo), 0); throw new InternalError("Unkown Cmd type encountered during variable slicing"); } @@ -552,7 +552,7 @@ private static IdentifierExpr getAssignedVariable(AssignLhs lhs) } else { - lhs.Emit(new TokenTextWriter(Console.Out)); + lhs.Emit(new TokenTextWriter(Console.Out, CommandLineOptions.Clo)); throw new InternalError("Unknown type of AssignLhs"); } @@ -645,7 +645,7 @@ public Program run(Program node) globalsRead = new HashSet(); // Typecheck -- needed for variable abstraction - if (node.Typecheck() != 0) + if (node.Typecheck(CommandLineOptions.Clo) != 0) { BoogieUtil.PrintProgram(node, "error.bpl"); throw new InternalError("Type errors"); diff --git a/source/CoreLib/VerificationPasses.cs b/source/CoreLib/VerificationPasses.cs index ba9fc3654..03a1cbef4 100644 --- a/source/CoreLib/VerificationPasses.cs +++ b/source/CoreLib/VerificationPasses.cs @@ -4,6 +4,7 @@ using System.Text; using Microsoft.Boogie; using System.Diagnostics; +using System.IO; using cba.Util; using Microsoft.Boogie.Houdini; @@ -1383,7 +1384,8 @@ private void RunHoudini(CBAProgram program, Dictionary= 0) { - Inliner.ProcessImplementation(program, impl); + Inliner.ProcessImplementation(CommandLineOptions.Clo, program, impl); } else { @@ -1650,7 +1654,7 @@ protected void inline(Program program) public class CallInliner : Inliner { public CallInliner(Program program) - : base(program, null, -1) + : base(program, null, -1, CommandLineOptions.Clo) { } new public static void ProcessImplementation(Program program, Implementation impl) @@ -1688,7 +1692,7 @@ protected void PruneIrrelevantImpls(Program program) }); program.TopLevelDeclarations = - program.TopLevelDeclarations.Where(decl => !(decl is Implementation) || (implHasEnsures(decl as Implementation) && !ignoreImpl(decl as Implementation))); + program.TopLevelDeclarations.Where(decl => !(decl is Implementation) || (implHasEnsures(decl as Implementation) && !ignoreImpl(decl as Implementation))).ToList(); } public override ErrorTrace mapBackTrace(ErrorTrace trace) @@ -1734,7 +1738,7 @@ public override CBAProgram runCBAPass(CBAProgram program) CommandLineOptions.Clo.RecursionBound = 2; // Unroll loops - program.ExtractLoops(); + LoopExtractor.ExtractLoops(CommandLineOptions.Clo, program); CommandLineOptions.Clo.RecursionBound = rb; } @@ -1806,7 +1810,7 @@ private void RunHoudini(CBAProgram program) CommandLineOptions.Clo.InlineDepth = InlineDepth; var old = CommandLineOptions.Clo.ProcedureInlining; - CommandLineOptions.Clo.ProcedureInlining = CommandLineOptions.Inlining.Spec; + CommandLineOptions.Clo.ProcedureInlining = CoreOptions.Inlining.Spec; var si = CommandLineOptions.Clo.StratifiedInlining; CommandLineOptions.Clo.StratifiedInlining = 0; var oldErrorLimit = CommandLineOptions.Clo.ErrorLimit; @@ -1866,8 +1870,9 @@ private void RunHoudini(CBAProgram program) { var houdiniStats = new HoudiniSession.HoudiniStatistics(); - Houdini houdini = new Houdini(program, houdiniStats); - outcome = houdini.PerformHoudiniInference(); + Houdini houdini = new Houdini(TextWriter.Null, CommandLineOptions.Clo, program, houdiniStats); + var task = houdini.PerformHoudiniInference(); + outcome = task.Result; Debug.Assert(outcome.ErrorCount == 0, "Something wrong with houdini"); if (!fastRequiresInference) @@ -1897,8 +1902,9 @@ private void RunHoudini(CBAProgram program) CommandLineOptions.Clo.ReverseHoudiniWorklist = true; var houdiniStats = new HoudiniSession.HoudiniStatistics(); - Houdini houdini = new Houdini(origProg, houdiniStats); - HoudiniOutcome outcomeReq = houdini.PerformHoudiniInference(); + Houdini houdini = new Houdini(TextWriter.Null, CommandLineOptions.Clo, origProg, houdiniStats); + var task = houdini.PerformHoudiniInference(); + var outcomeReq = task.Result; Debug.Assert(outcomeReq.ErrorCount == 0, "Something wrong with houdini"); CommandLineOptions.Clo.ReverseHoudiniWorklist = false; diff --git a/source/CoreLib/WeightDomains.cs b/source/CoreLib/WeightDomains.cs index ef245294d..923be1c96 100644 --- a/source/CoreLib/WeightDomains.cs +++ b/source/CoreLib/WeightDomains.cs @@ -369,7 +369,7 @@ public void Print() public void Print(bool forSummary) { var expr = ToExpr(forSummary); - expr.Iter(e => { e.Emit(new TokenTextWriter(Console.Out)); Console.WriteLine(); }); + expr.Iter(e => { e.Emit(new TokenTextWriter(Console.Out, CommandLineOptions.Clo)); Console.WriteLine(); }); } public IEnumerable ToExpr(bool forSummary) @@ -598,7 +598,7 @@ public override string ToString() foreach (var e in constExprs) { var sb = new System.IO.StringWriter(); - e.Emit(new TokenTextWriter(sb)); + e.Emit(new TokenTextWriter(sb, CommandLineOptions.Clo)); sb.Close(); exprs += "," + sb.ToString(); } diff --git a/source/Corral/ConstLoop.cs b/source/Corral/ConstLoop.cs index 0dc14abd8..a3c871d00 100644 --- a/source/Corral/ConstLoop.cs +++ b/source/Corral/ConstLoop.cs @@ -393,7 +393,7 @@ private bool ReachableProcedure(string proc, out int depth, out HashSet graph.AddEdge(kvp.Key, tgt); })); - if (!Graph.Acyclic(graph, proc)) + if (!Graph.Acyclic(graph)) return false; return true; diff --git a/source/Corral/Corral.csproj b/source/Corral/Corral.csproj index 66d083f7e..51d19e28b 100644 --- a/source/Corral/Corral.csproj +++ b/source/Corral/Corral.csproj @@ -22,6 +22,11 @@ + + + + + diff --git a/source/Corral/Driver.cs b/source/Corral/Driver.cs index 97c620a67..8e270d95a 100644 --- a/source/Corral/Driver.cs +++ b/source/Corral/Driver.cs @@ -152,8 +152,10 @@ public static void Initialize(Configs config) // Initialize Boogie CommandLineOptions.Clo.PrintInstrumented = true; - CommandLineOptions.Clo.ProcedureInlining = CommandLineOptions.Inlining.Assume; - CommandLineOptions.Clo.TypeEncodingMethod = CommandLineOptions.TypeEncoding.Monomorphic; + CommandLineOptions.Clo.ProcedureInlining = + CoreOptions.Inlining.Assume; + CommandLineOptions.Clo.TypeEncodingMethod = + CoreOptions.TypeEncoding.Monomorphic; // /noRemoveEmptyBlocks is needed for field refinement. It ensures that // we get an actual path in the program (so that we can concretize it) @@ -213,7 +215,7 @@ public static int run(string[] args) Console.WriteLine("Corral program verifier version {0}", VersionInfo()); Configs config = Configs.parseCommandLine(args); - CommandLineOptions.Install(new CommandLineOptions()); + CommandLineOptions.Clo = new CommandLineOptions(new ConsolePrinter()); if (!System.IO.File.Exists(config.inputFile)) { @@ -595,7 +597,7 @@ public static PersistentCBAProgram GetInputProgram(Configs config) { BoogieVerify.removeAsserts = false; var err = new List(); - init.Typecheck(); + init.Typecheck(CommandLineOptions.Clo); BoogieVerify.options = new BoogieVerifyOptions(); BoogieVerify.options.NonUniformUnfolding = config.NonUniformUnfolding; @@ -777,7 +779,8 @@ public static void PreProcessCodeExpr(Program program) } foreach (var impl in program.TopLevelDeclarations.OfType()) { - if (CommandLineOptions.Clo.UserWantsToCheckRoutine(impl.Name) && !impl.SkipVerification) + if ((CommandLineOptions.Clo as ExecutionEngineOptions).UserWantsToCheckRoutine(impl.Name) && + !impl.IsSkipVerification(CommandLineOptions.Clo)) { CodeExprInliner.ProcessImplementation(program, impl); } @@ -795,7 +798,7 @@ class CodeExprInliner : Inliner Dictionary declToAnnotations; public CodeExprInliner(Program program) - : base(program, null, -1) + : base(program, null, -1, CommandLineOptions.Clo) { this.declToAnnotations = new Dictionary(); // save annotation @@ -849,8 +852,9 @@ public static void InlineProcedures(Program program) { var si = CommandLineOptions.Clo.StratifiedInlining; CommandLineOptions.Clo.StratifiedInlining = 0; - ExecutionEngine.EliminateDeadVariables(program); - ExecutionEngine.Inline(program); + var executionEngine = new ExecutionEngine(CommandLineOptions.Clo, new VerificationResultCache()); + executionEngine.EliminateDeadVariables(program); + executionEngine.Inline(program); CommandLineOptions.Clo.StratifiedInlining = si; } diff --git a/source/Corral/WellFormedProg.cs b/source/Corral/WellFormedProg.cs index ebbb4914c..3b991a539 100644 --- a/source/Corral/WellFormedProg.cs +++ b/source/Corral/WellFormedProg.cs @@ -66,13 +66,13 @@ private static void checkProc(Procedure proc, HashSet procsWithImpl, Has if (used.globalsUsed.Any(v => LanguageSemantics.isShared(v))) { - re.Emit(new TokenTextWriter(Console.Out), 0); + re.Emit(new TokenTextWriter(Console.Out, CommandLineOptions.Clo), 0); throw new InvalidInput("Requires has a shared global"); } if (used.oldVarsUsed.Any(v => LanguageSemantics.isShared(v))) { - re.Emit(new TokenTextWriter(Console.Out), 0); + re.Emit(new TokenTextWriter(Console.Out, CommandLineOptions.Clo), 0); throw new InvalidInput("Requires has an \"old\" shared global"); } @@ -89,7 +89,7 @@ private static void checkProc(Procedure proc, HashSet procsWithImpl, Has if (re.Free == false) { - re.Emit(new TokenTextWriter(Console.Out), 0); + re.Emit(new TokenTextWriter(Console.Out, CommandLineOptions.Clo), 0); throw new InvalidInput("A non-free requires has a non-shared global (not yet supported)"); } @@ -102,13 +102,13 @@ private static void checkProc(Procedure proc, HashSet procsWithImpl, Has if (used.globalsUsed.Any(v => LanguageSemantics.isShared(v))) { - re.Emit(new TokenTextWriter(Console.Out), 0); + re.Emit(new TokenTextWriter(Console.Out, CommandLineOptions.Clo), 0); throw new InvalidInput("Ensures has a shared global"); } if (used.oldVarsUsed.Any(v => LanguageSemantics.isShared(v))) { - re.Emit(new TokenTextWriter(Console.Out), 0); + re.Emit(new TokenTextWriter(Console.Out, CommandLineOptions.Clo), 0); throw new InvalidInput("Ensures has an \"old\" shared global"); } @@ -122,7 +122,7 @@ private static void checkProc(Procedure proc, HashSet procsWithImpl, Has // "Ensures" in procs without implementation are considered free if (re.Free == false && procsWithImpl.Contains(proc.Name)) { - re.Emit(new TokenTextWriter(Console.Out), 0); + re.Emit(new TokenTextWriter(Console.Out, CommandLineOptions.Clo), 0); throw new InvalidInput("A non-free ensures is not yet supported"); } @@ -143,7 +143,7 @@ private static void checkOld(Implementation impl) used.Visit(cmd); if (used.oldVarsUsed.Any()) { - cmd.Emit(new TokenTextWriter(Console.Out), 0); + cmd.Emit(new TokenTextWriter(Console.Out, CommandLineOptions.Clo), 0); throw new InvalidInput("Command has an \"old\" variable"); } } @@ -155,7 +155,7 @@ private static void checkBaseTypes(Declaration decl) { if (decl is TypeCtorDecl) { - decl.Emit(new TokenTextWriter(Console.Out), 0); + decl.Emit(new TokenTextWriter(Console.Out, CommandLineOptions.Clo), 0); throw new InvalidInput("Program has a user-defined type (cannot use with ArrayTheory)"); } } diff --git a/source/Directory.Build.props b/source/Directory.Build.props index e0473b760..e4e98c283 100644 --- a/source/Directory.Build.props +++ b/source/Directory.Build.props @@ -2,7 +2,7 @@ - net5.0;net6.0 + net6.0 false Corral https://github.com/boogie-org/corral @@ -15,8 +15,12 @@ + + - + diff --git a/source/ExplainError/ControlFlowDependency.cs b/source/ExplainError/ControlFlowDependency.cs index fda084612..1170be7a3 100644 --- a/source/ExplainError/ControlFlowDependency.cs +++ b/source/ExplainError/ControlFlowDependency.cs @@ -32,7 +32,7 @@ public ControlFlowDependency(Program prog, bool coarseProcedureLevelOnly=false) public void Run() { Console.WriteLine("Performing ControlFlowDependencyPrePass.....\n"); - (new ModSetCollector()).DoModSetAnalysis(prog); + (new ModSetCollector(CommandLineOptions.Clo)).DoModSetAnalysis(prog); prog.Implementations.Iter(impl => (new SplitBranchBlocks(impl)).Run()); prog.Implementations.Iter(impl => (new IntraProcModSetComputerPerImpl(this, impl)).Run()); // Add place holders for variables/blocks @@ -183,7 +183,7 @@ private void PerformFineGrainedControlDependency() private void FindBranchJoinPairs() { impl.ComputePredecessorsForBlocks(); - var blockGraph = parent.prog.ProcessLoops(impl); + var blockGraph = parent.prog.ProcessLoops(CommandLineOptions.Clo, impl); //(branch node) n -> all nodes for which n is the immediate dominator (then, else, join-if-not-return) var immDomMap = blockGraph.ImmediateDominatorMap; #region Other dominator datastructures, not used diff --git a/source/ExplainError/program.cs b/source/ExplainError/program.cs index 6853761ef..03715a462 100644 --- a/source/ExplainError/program.cs +++ b/source/ExplainError/program.cs @@ -6,6 +6,7 @@ using System.Threading.Tasks; using System.IO; using System.Diagnostics; +using System.Threading; using Microsoft.Boogie; using Microsoft.Boogie.VCExprAST; using VC; @@ -86,7 +87,7 @@ public class Toplevel static private VCGen vcgen; static private ProverInterface proverInterface; //static private ProverInterface.ErrorHandler handler; - static private ConditionGeneration.CounterexampleCollector collector; + static private ConditionGeneration.VerificationResultCollector collector; static private Boogie2VCExprTranslator translator; static private VCExpressionGenerator exprGen; @@ -481,7 +482,7 @@ private static void SimplifyAssumesUsingForwardPass() oldExpr.ToString().Contains("!="))) continue; assumeCmd.Expr = Expr.Not(oldExpr); - prog.Resolve(); prog.Typecheck(); //TODO: perhaps move this inside MyVerifyImplementation? + prog.Resolve(CommandLineOptions.Clo); prog.Typecheck(CommandLineOptions.Clo); //TODO: perhaps move this inside MyVerifyImplementation? Console.WriteLine("Checking the assume {0} ", assumeCmd); if (VCVerifier.MyVerifyImplementation(currImpl) == ConditionGeneration.Outcome.Correct) { @@ -1155,9 +1156,9 @@ public static bool ParseCommandLine(string clo) string[] args; //Custom parser to look and remove RootCause specific options var help = ParseArgs(oldArgs, out args); - CommandLineOptions.Install(new CommandLineOptions()); + CommandLineOptions.Clo = new CommandLineOptions(new ConsolePrinter()); CommandLineOptions.Clo.RunningBoogieFromCommandLine = true; - CommandLineOptions.Clo.TypeEncodingMethod = CommandLineOptions.TypeEncoding.Monomorphic; + CommandLineOptions.Clo.TypeEncodingMethod = CoreOptions.TypeEncoding.Monomorphic; CommandLineOptions.Clo.Parse(args); return !help; } @@ -1255,13 +1256,13 @@ public static bool ParseProgram(string fname, out Program prog) Console.WriteLine("WARNING: Error opening file \"{0}\": {1}", fname, e.Message); return false; } - errCount = prog.Resolve(); + errCount = prog.Resolve(CommandLineOptions.Clo); if (errCount > 0) { Console.WriteLine("WARNING: {0} name resolution errors in {1}", errCount, fname); return false; } - errCount = prog.Typecheck(); + errCount = prog.Typecheck(CommandLineOptions.Clo); if (errCount > 0) { Console.WriteLine("WARNING: {0} type checking errors in {1}", errCount, fname); @@ -1273,7 +1274,7 @@ public static bool ParseProgram(string fname, out Program prog) private static bool CheckSanity(Implementation impl) { if (impl == null) { returnStatus = STATUS.ILLEGAL; return false; } - if (!CommandLineOptions.Clo.UserWantsToCheckRoutine(impl.Name)) + if (!(CommandLineOptions.Clo as ExecutionEngineOptions).UserWantsToCheckRoutine(impl.Name)) { returnStatus = STATUS.ILLEGAL; return false; } @@ -1302,15 +1303,15 @@ private static bool CheckSanity(Implementation impl) #endregion #region Invoking Verifier for semantic queries - private static void CreateProver() + /*private static void CreateProver() { //create vcgen/proverInterface vcgen = new VCGen(prog, CommandLineOptions.Clo.ProverLogFilePath, CommandLineOptions.Clo.ProverLogFileAppend, new List()); proverInterface = ProverInterface.CreateProver(prog, CommandLineOptions.Clo.ProverLogFilePath, CommandLineOptions.Clo.ProverLogFileAppend, CommandLineOptions.Clo.TimeLimit); translator = proverInterface.Context.BoogieExprTranslator; exprGen = proverInterface.Context.ExprGen; - collector = new ConditionGeneration.CounterexampleCollector(); - } + collector = new ConditionGeneration.VerificationResultCollector(); + }*/ /// /// Class for asking semantic questions for the verifier (carried over from almost correct specs) /// @@ -1335,13 +1336,13 @@ public static bool CheckIfExprFalse(Implementation impl, Expr e) var cexList = new List(); prog.AddTopLevelDeclaration(i); prog.AddTopLevelDeclaration(p); - prog.Resolve(); - prog.Typecheck(); + prog.Resolve(CommandLineOptions.Clo); + prog.Typecheck(CommandLineOptions.Clo); var result = (MyVerifyImplementation(i, ref cexList) == VC.ConditionGeneration.Outcome.Correct); prog.RemoveTopLevelDeclaration(i); prog.RemoveTopLevelDeclaration(p); - prog.Resolve(); - prog.Typecheck(); + prog.Resolve(CommandLineOptions.Clo); + prog.Typecheck(CommandLineOptions.Clo); Console.Write("."); if (verbose) Console.WriteLine("CheckIfExprFalse: input {0}, output {1}", e.ToString(), result); checkIfExprFalseCalled = true; @@ -1352,8 +1353,8 @@ public static VC.ConditionGeneration.Outcome MyVerifyImplementation(Implementati ref List cexList) { //this creates a z3 process per vcgen - var checkers = new List(); - VC.VCGen vcgen = new VC.VCGen(prog, CommandLineOptions.Clo.ProverLogFilePath, CommandLineOptions.Clo.ProverLogFileAppend, checkers); + var checkers = new CheckerPool(CommandLineOptions.Clo); + VC.VCGen vcgen = new VC.VCGen(prog, checkers); //make deep copy of the blocks var tmpBlocks = new List(); foreach (Block b in i.Blocks) @@ -1369,14 +1370,12 @@ public static VC.ConditionGeneration.Outcome MyVerifyImplementation(Implementati i.Blocks = i.OriginalBlocks; i.LocVars = i.OriginalLocVars; } - var outcome = vcgen.VerifyImplementation((Implementation)i, out cexList); + + var run = new ImplementationRun(i, TextWriter.Null); + var outcome = vcgen.VerifyImplementation(run, CancellationToken.None).Result.Item1; var reset = new ResetVerificationState(); reset.Visit(i); - foreach (Checker checker in checkers) - { - //Contract.Assert(checker != null); - checker.Close(); - } + checkers.Dispose(); vcgen.Close(); i.Blocks = tmpBlocks; i.LocVars = tmpLocVars; diff --git a/source/ProgTransformation/PersistentProgram.cs b/source/ProgTransformation/PersistentProgram.cs index e3a8c59e0..439166c50 100644 --- a/source/ProgTransformation/PersistentProgram.cs +++ b/source/ProgTransformation/PersistentProgram.cs @@ -180,14 +180,14 @@ private void readInProgram(Program p) count++; StreamWriter writer = new StreamWriter(programStream as FileStream); - p.Emit(new TokenTextWriter(writer)); + p.Emit(new TokenTextWriter(writer, CommandLineOptions.Clo)); writer.Flush(); } else if (useStrings) { fileName = ""; var sw = new StringWriter(); - p.Emit(new TokenTextWriter(sw)); + p.Emit(new TokenTextWriter(sw, CommandLineOptions.Clo)); sw.Flush(); programStream = sw.ToString(); } @@ -197,7 +197,7 @@ private void readInProgram(Program p) programStream = new MemoryStream(); StreamWriter writer = new StreamWriter(programStream as MemoryStream); - p.Emit(new TokenTextWriter(writer)); + p.Emit(new TokenTextWriter(writer, CommandLineOptions.Clo)); writer.Flush(); } @@ -273,7 +273,7 @@ public override Program getProgram() } } - if (ret.Resolve() != 0) + if (ret.Resolve(CommandLineOptions.Clo) != 0) { writeToFile("error.bpl"); throw new InternalError("Illegal program given to PersistentProgram"); @@ -325,7 +325,7 @@ public override Program getProgram() FixedDuplicator dup = new FixedDuplicator(); Program ret = dup.VisitProgram(program); - if (ret.Resolve() != 0 || ret.Typecheck() != 0) + if (ret.Resolve(CommandLineOptions.Clo) != 0 || ret.Typecheck(CommandLineOptions.Clo) != 0) { BoogieUtil.PrintProgram(ret, "error.bpl"); throw new InternalError("Illegal program given to PersistentProgram"); diff --git a/source/Util/BoogieUtil.cs b/source/Util/BoogieUtil.cs index ebd871c26..4787fb958 100644 --- a/source/Util/BoogieUtil.cs +++ b/source/Util/BoogieUtil.cs @@ -50,19 +50,19 @@ public static bool InitializeBoogie(string clo) public static void DoModSetAnalysis(Program p) { - (new ModSetCollector()).DoModSetAnalysis(p); + (new ModSetCollector(CommandLineOptions.Clo)).DoModSetAnalysis(p); } public static void PrintProgram(Program p, string filename) { - var outFile = new TokenTextWriter(filename); + var outFile = new TokenTextWriter(filename, CommandLineOptions.Clo); p.Emit(outFile); outFile.Close(); } public static bool ResolveProgram(Program p, string filename) { - int errorCount = p.Resolve(); + int errorCount = p.Resolve(CommandLineOptions.Clo); if (errorCount != 0) Console.WriteLine(errorCount + " name resolution errors in " + filename); return errorCount != 0; @@ -70,7 +70,7 @@ public static bool ResolveProgram(Program p, string filename) public static bool TypecheckProgram(Program p, string filename) { - int errorCount = p.Typecheck(); + int errorCount = p.Typecheck(CommandLineOptions.Clo); if (errorCount != 0) { PrintProgram(p, "error.bpl"); @@ -454,7 +454,7 @@ public static Program ReResolveInMem(Program p, bool doTypecheck = true) using (var writer = new System.IO.MemoryStream()) { var st = new System.IO.StreamWriter(writer); - var tt = new TokenTextWriter(st); + var tt = new TokenTextWriter(st, CommandLineOptions.Clo); p.Emit(tt); writer.Flush(); st.Flush(); @@ -485,7 +485,7 @@ public static Program ReResolve(Program p, string filename, bool doTypecheck = t public static void PrintGlobalVariables(Program p) { - TokenTextWriter log = new TokenTextWriter(Console.Out); + TokenTextWriter log = new TokenTextWriter(Console.Out, CommandLineOptions.Clo); foreach (Declaration d in p.TopLevelDeclarations) { if (d is GlobalVariable) @@ -1598,8 +1598,10 @@ public static Program Compute(Program program, PhiFunctionEncoding encoding, Has var op = CommandLineOptions.Clo.ExtractLoopsUnrollIrreducible; CommandLineOptions.Clo.ExtractLoopsUnrollIrreducible = false; - // Extract loops, we don't want cycles in the CFG - program.ExtractLoops(out irreducible); + // Extract loops, we don't want cycles in the CFG + irreducible = LoopExtractor.ExtractLoops(CommandLineOptions.Clo, program) + .procsWithIrreducibleLoops + .Select(implementation => implementation.Name).ToHashSet(); RemoveVarsFromAttributes.Prune(program); if (GVN.doGVN) @@ -1663,7 +1665,7 @@ private void SSARename(Implementation impl) } // Remove unreachble blocks - impl.PruneUnreachableBlocks(); + impl.PruneUnreachableBlocks(CommandLineOptions.Clo); // Live variable analysis CbaLiveVariableAnalysis.ClearLiveVariables(impl); diff --git a/source/Util/Duplicator.cs b/source/Util/Duplicator.cs index 06b46300d..1e6ff6747 100644 --- a/source/Util/Duplicator.cs +++ b/source/Util/Duplicator.cs @@ -454,7 +454,6 @@ public override Function VisitFunction(Function node) { node = (Function)node.Clone(); node.Attributes = CopyAttr(node.Attributes); - node.doingExpansion = false; return base.VisitFunction(node); } diff --git a/source/Util/LiveVariableAnalysis.cs b/source/Util/LiveVariableAnalysis.cs index d534a5dfa..f2c92759d 100644 --- a/source/Util/LiveVariableAnalysis.cs +++ b/source/Util/LiveVariableAnalysis.cs @@ -231,7 +231,7 @@ public static void Propagate(Cmd cmd, HashSet/*!*/ liveSet, bool else if (cmd is SugaredCmd) { SugaredCmd/*!*/ sugCmd = (SugaredCmd)cce.NonNull(cmd); - Propagate(sugCmd.Desugaring, liveSet, allGlobalsAreLive); + Propagate(sugCmd.GetDesugaring(CommandLineOptions.Clo), liveSet, allGlobalsAreLive); } else if (cmd is StateCmd) { diff --git a/source/Util/Util.cs b/source/Util/Util.cs index c246273ad..1908c28dd 100644 --- a/source/Util/Util.cs +++ b/source/Util/Util.cs @@ -120,7 +120,7 @@ private static void init() if (debugOut == null) { - debugOut = new TokenTextWriter("corraldebug.out"); + debugOut = new TokenTextWriter("corraldebug.out", CommandLineOptions.Clo); } } @@ -141,7 +141,7 @@ public static TokenTextWriter getWriter(int level) init(); return debugOut; } - return new TokenTextWriter(Console.Out); + return new TokenTextWriter(Console.Out, CommandLineOptions.Clo); } public static bool Write(int level, string msg, params object[] args) diff --git a/source/Util/Visitor.cs b/source/Util/Visitor.cs index fb8ed7c44..52fd65f64 100644 --- a/source/Util/Visitor.cs +++ b/source/Util/Visitor.cs @@ -570,7 +570,7 @@ public override Declaration VisitDeclaration(Declaration node) node = this.VisitDeclWithFormals((DeclWithFormals)node); else { - node.Emit(new TokenTextWriter(Console.Out), 0); + node.Emit(new TokenTextWriter(Console.Out, CommandLineOptions.Clo), 0); throw new InvalidInput("Unknown declaration type"); } @@ -591,7 +591,7 @@ public override DeclWithFormals VisitDeclWithFormals(DeclWithFormals node) node = this.VisitProcedure((Procedure)node); else { - node.Emit(new TokenTextWriter(Console.Out), 0); + node.Emit(new TokenTextWriter(Console.Out, CommandLineOptions.Clo), 0); throw new InvalidInput("Unknown declaration type"); }