From c0578efe1ff17e30eb33e60e279a9a14a7a836a5 Mon Sep 17 00:00:00 2001 From: wuestholz Date: Mon, 3 Jun 2013 15:32:05 -0700 Subject: Did some refactoring in the Boogie driver. --- Source/BoogieDriver/BoogieDriver.cs | 807 +------------------------------- Source/BoogieDriver/BoogieDriver.csproj | 4 + 2 files changed, 16 insertions(+), 795 deletions(-) (limited to 'Source/BoogieDriver') diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 95f67b71..d35ac5f2 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -22,7 +22,6 @@ namespace Microsoft.Boogie { using System.Linq; using VC; using BoogiePL = Microsoft.Boogie; - using Core; /* The following assemblies are referenced because they are needed at runtime, not at compile time: @@ -31,10 +30,15 @@ namespace Microsoft.Boogie { System.Compiler.Framework */ - public class OnlyBoogie { + public class OnlyBoogie + { - public static void Main(string[] args) { + public static void Main(string[] args) + { Contract.Requires(cce.NonNullElements(args)); + + ExecutionEngine.printer = new ConsolePrinter(); + CommandLineOptions.Install(new CommandLineOptions()); CommandLineOptions.Clo.RunningBoogieFromCommandLine = true; @@ -42,13 +46,13 @@ namespace Microsoft.Boogie { goto END; } if (CommandLineOptions.Clo.Files.Count == 0) { - printer.ErrorWriteLine("*** Error: No input files were specified."); + ExecutionEngine.printer.ErrorWriteLine("*** Error: No input files were specified."); goto END; } if (CommandLineOptions.Clo.XmlSink != null) { string errMsg = CommandLineOptions.Clo.XmlSink.Open(); if (errMsg != null) { - printer.ErrorWriteLine("*** Error: " + errMsg); + ExecutionEngine.printer.ErrorWriteLine("*** Error: " + errMsg); goto END; } } @@ -89,12 +93,12 @@ namespace Microsoft.Boogie { extension = extension.ToLower(); } if (extension != ".bpl") { - printer.ErrorWriteLine("*** Error: '{0}': Filename extension '{1}' is not supported. Input files must be BoogiePL programs (.bpl).", file, + ExecutionEngine.printer.ErrorWriteLine("*** Error: '{0}': Filename extension '{1}' is not supported. Input files must be BoogiePL programs (.bpl).", file, extension == null ? "" : extension); goto END; } } - ProcessFiles(fileList); + ExecutionEngine.ProcessFiles(fileList); END: if (CommandLineOptions.Clo.XmlSink != null) { @@ -105,793 +109,7 @@ namespace Microsoft.Boogie { Console.ReadLine(); } } - - - static void ProcessFiles(List fileNames, bool lookForSnapshots = true) { - Contract.Requires(cce.NonNullElements(fileNames)); - - if (CommandLineOptions.Clo.VerifySnapshots && lookForSnapshots) - { - var snapshotsByVersion = new List>(); - for (int version = 0; true; version++) - { - var nextSnapshot = new List(); - foreach (var name in fileNames) - { - var versionedName = name.Replace(Path.GetExtension(name), ".v" + version + Path.GetExtension(name)); - if (File.Exists(versionedName)) - { - nextSnapshot.Add(versionedName); - } - } - if (nextSnapshot.Any()) - { - snapshotsByVersion.Add(nextSnapshot); - } - else - { - break; - } - } - - foreach (var s in snapshotsByVersion) - { - ProcessFiles(new List(s), false); - } - return; - } - - using (XmlFileScope xf = new XmlFileScope(CommandLineOptions.Clo.XmlSink, fileNames[fileNames.Count - 1])) - { - //BoogiePL.Errors.count = 0; - Program program = ParseBoogieProgram(fileNames, false); - if (program == null) - return; - if (CommandLineOptions.Clo.PrintFile != null) - { - PrintBplFile(CommandLineOptions.Clo.PrintFile, program, false); - } - - PipelineOutcome oc = ResolveAndTypecheck(program, fileNames[fileNames.Count - 1]); - if (oc != PipelineOutcome.ResolvedAndTypeChecked) - return; - //BoogiePL.Errors.count = 0; - - // Do bitvector analysis - if (CommandLineOptions.Clo.DoBitVectorAnalysis) - { - Microsoft.Boogie.BitVectorAnalysis.DoBitVectorAnalysis(program); - PrintBplFile(CommandLineOptions.Clo.BitVectorAnalysisOutputBplFile, program, false); - return; - } - - if (CommandLineOptions.Clo.PrintCFGPrefix != null) - { - foreach (var impl in program.TopLevelDeclarations.OfType()) - { - using (StreamWriter sw = new StreamWriter(CommandLineOptions.Clo.PrintCFGPrefix + "." + impl.Name + ".dot")) - { - sw.Write(program.ProcessLoops(impl).ToDot()); - } - } - } - - if (CommandLineOptions.Clo.OwickiGriesDesugaredOutputFile != null) - { - OwickiGriesTransform ogTransform = new OwickiGriesTransform(linearTypechecker); - ogTransform.Transform(); - var eraser = new LinearEraser(); - eraser.VisitProgram(program); - int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured; - CommandLineOptions.Clo.PrintUnstructured = 1; - PrintBplFile(CommandLineOptions.Clo.OwickiGriesDesugaredOutputFile, program, false, false); - CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured; - } - - EliminateDeadVariablesAndInline(program); - - if (CommandLineOptions.Clo.StagedHoudini > 0) - { - var candidateDependenceAnalyser = new CandidateDependenceAnalyser(program); - candidateDependenceAnalyser.Analyse(); - candidateDependenceAnalyser.ApplyStages(); - if (CommandLineOptions.Clo.Trace) - { - candidateDependenceAnalyser.dump(); - int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured; - CommandLineOptions.Clo.PrintUnstructured = 2; - PrintBplFile("staged.bpl", program, false, false); - CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured; - } - } - - int errorCount, verified, inconclusives, timeOuts, outOfMemories; - oc = InferAndVerify(program, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories); - switch (oc) - { - case PipelineOutcome.Done: - case PipelineOutcome.VerificationCompleted: - printer.WriteTrailer(verified, errorCount, inconclusives, timeOuts, outOfMemories); - break; - default: - break; - } - } - } - - - static void PrintBplFile(string filename, Program program, bool allowPrintDesugaring, bool setTokens = true) { - Contract.Requires(program != null); - Contract.Requires(filename != null); - bool oldPrintDesugaring = CommandLineOptions.Clo.PrintDesugarings; - if (!allowPrintDesugaring) { - CommandLineOptions.Clo.PrintDesugarings = false; - } - using (TokenTextWriter writer = filename == "-" ? - new TokenTextWriter("", Console.Out, setTokens) : - new TokenTextWriter(filename, setTokens)) { - if (CommandLineOptions.Clo.ShowEnv != CommandLineOptions.ShowEnvironment.Never) { - writer.WriteLine("// " + CommandLineOptions.Clo.Version); - writer.WriteLine("// " + CommandLineOptions.Clo.Environment); - } - writer.WriteLine(); - program.Emit(writer); - } - CommandLineOptions.Clo.PrintDesugarings = oldPrintDesugaring; - } - - - static void ReportBplError(Absy node, string message, bool error, bool showBplLocation) { - Contract.Requires(message != null); - Contract.Requires(node != null); - IToken tok = node.tok; - string s; - if (tok != null && showBplLocation) { - s = string.Format("{0}({1},{2}): {3}", tok.filename, tok.line, tok.col, message); - } else { - s = message; - } - if (error) { - printer.ErrorWriteLine(s); - } else { - Console.WriteLine(s); - } - } - - - /// - /// Parse the given files into one Boogie program. If an I/O or parse error occurs, an error will be printed - /// and null will be returned. On success, a non-null program is returned. - /// - static Program ParseBoogieProgram(List fileNames, bool suppressTraceOutput) { - Contract.Requires(cce.NonNullElements(fileNames)); - //BoogiePL.Errors.count = 0; - Program program = null; - bool okay = true; - for (int fileId = 0; fileId < fileNames.Count; fileId++) { - string bplFileName = fileNames[fileId]; - if (!suppressTraceOutput) { - if (CommandLineOptions.Clo.XmlSink != null) { - CommandLineOptions.Clo.XmlSink.WriteFileFragment(bplFileName); - } - if (CommandLineOptions.Clo.Trace) { - Console.WriteLine("Parsing " + bplFileName); - } - } - - Program programSnippet; - int errorCount; - try { - var defines = new List() { "FILE_" + fileId }; - errorCount = BoogiePL.Parser.Parse(bplFileName, defines, out programSnippet); - if (programSnippet == null || errorCount != 0) { - Console.WriteLine("{0} parse errors detected in {1}", errorCount, bplFileName); - okay = false; - continue; - } - } catch (IOException e) { - printer.ErrorWriteLine("Error opening file \"{0}\": {1}", bplFileName, e.Message); - okay = false; - continue; - } - if (program == null) { - program = programSnippet; - } else if (programSnippet != null) { - program.TopLevelDeclarations.AddRange(programSnippet.TopLevelDeclarations); - } - } - if (!okay) { - return null; - } else if (program == null) { - return new Program(); - } else { - return program; - } - } - - - static LinearTypechecker linearTypechecker; - - - /// - /// Resolves and type checks the given Boogie program. Any errors are reported to the - /// console. Returns: - /// - Done if no errors occurred, and command line specified no resolution or no type checking. - /// - ResolutionError if a resolution error occurred - /// - TypeCheckingError if a type checking error occurred - /// - ResolvedAndTypeChecked if both resolution and type checking succeeded - /// - static PipelineOutcome ResolveAndTypecheck(Program program, string bplFileName) { - Contract.Requires(program != null); - Contract.Requires(bplFileName != null); - // ---------- Resolve ------------------------------------------------------------ - - if (CommandLineOptions.Clo.NoResolve) { - return PipelineOutcome.Done; - } - - int errorCount = program.Resolve(); - if (errorCount != 0) { - Console.WriteLine("{0} name resolution errors detected in {1}", errorCount, bplFileName); - return PipelineOutcome.ResolutionError; - } - - // ---------- Type check ------------------------------------------------------------ - - if (CommandLineOptions.Clo.NoTypecheck) { - return PipelineOutcome.Done; - } - - errorCount = program.Typecheck(); - if (errorCount != 0) { - Console.WriteLine("{0} type checking errors detected in {1}", errorCount, bplFileName); - return PipelineOutcome.TypeCheckingError; - } - - linearTypechecker = new LinearTypechecker(program); - linearTypechecker.Typecheck(); - if (linearTypechecker.errorCount == 0) - { - linearTypechecker.Transform(); - } - else - { - Console.WriteLine("{0} type checking errors detected in {1}", linearTypechecker.errorCount, bplFileName); - return PipelineOutcome.TypeCheckingError; - } - - if (CommandLineOptions.Clo.PrintFile != null && CommandLineOptions.Clo.PrintDesugarings) { - // if PrintDesugaring option is engaged, print the file here, after resolution and type checking - PrintBplFile(CommandLineOptions.Clo.PrintFile, program, true); - } - - return PipelineOutcome.ResolvedAndTypeChecked; - } - - - static void EliminateDeadVariablesAndInline(Program program) { - Contract.Requires(program != null); - // Eliminate dead variables - Microsoft.Boogie.UnusedVarEliminator.Eliminate(program); - - // Collect mod sets - if (CommandLineOptions.Clo.DoModSetAnalysis) { - Microsoft.Boogie.ModSetCollector.DoModSetAnalysis(program); - } - - // Coalesce blocks - if (CommandLineOptions.Clo.CoalesceBlocks) { - if (CommandLineOptions.Clo.Trace) - Console.WriteLine("Coalescing blocks..."); - Microsoft.Boogie.BlockCoalescer.CoalesceBlocks(program); - } - - // Inline - var TopLevelDeclarations = cce.NonNull(program.TopLevelDeclarations); - - if (CommandLineOptions.Clo.ProcedureInlining != CommandLineOptions.Inlining.None) { - bool inline = false; - foreach (var d in TopLevelDeclarations) { - if (d.FindExprAttribute("inline") != null) { - inline = true; - } - } - if (inline) { - foreach (var d in TopLevelDeclarations) { - var impl = d as Implementation; - if (impl != null) { - impl.OriginalBlocks = impl.Blocks; - impl.OriginalLocVars = impl.LocVars; - } - } - foreach (var d in TopLevelDeclarations) { - var impl = d as Implementation; - if (impl != null && !impl.SkipVerification) { - Inliner.ProcessImplementation(program, impl); - } - } - foreach (var d in TopLevelDeclarations) { - var impl = d as Implementation; - if (impl != null) { - impl.OriginalBlocks = null; - impl.OriginalLocVars = null; - } - } - } - } - } - - - static void ProcessOutcome(VC.VCGen.Outcome outcome, List errors, string timeIndication, - ref int errorCount, ref int verified, ref int inconclusives, ref int timeOuts, ref int outOfMemories) { - switch (outcome) { - default: - Contract.Assert(false); // unexpected outcome - throw new cce.UnreachableException(); - case VCGen.Outcome.ReachedBound: - printer.Inform(String.Format("{0}verified", timeIndication)); - Console.WriteLine(string.Format("Stratified Inlining: Reached recursion bound of {0}", CommandLineOptions.Clo.RecursionBound)); - verified++; - break; - case VCGen.Outcome.Correct: - if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) { - printer.Inform(String.Format("{0}credible", timeIndication)); - verified++; - } - else { - printer.Inform(String.Format("{0}verified", timeIndication)); - verified++; - } - break; - case VCGen.Outcome.TimedOut: - timeOuts++; - printer.Inform(String.Format("{0}timed out", timeIndication)); - break; - case VCGen.Outcome.OutOfMemory: - outOfMemories++; - printer.Inform(String.Format("{0}out of memory", timeIndication)); - break; - case VCGen.Outcome.Inconclusive: - inconclusives++; - printer.Inform(String.Format("{0}inconclusive", timeIndication)); - break; - case VCGen.Outcome.Errors: - if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) { - printer.Inform(String.Format("{0}doomed", timeIndication)); - errorCount++; - } - Contract.Assert(errors != null); // guaranteed by postcondition of VerifyImplementation - break; - } - if (errors != null) - { - // BP1xxx: Parsing errors - // BP2xxx: Name resolution errors - // BP3xxx: Typechecking errors - // BP4xxx: Abstract interpretation errors (Is there such a thing?) - // BP5xxx: Verification errors - - var cause = "Error"; - if (outcome == VCGen.Outcome.TimedOut) - { - cause = "Timed out on"; - } - else if (outcome == VCGen.Outcome.OutOfMemory) - { - cause = "Out of memory on"; - } - // TODO(wuestholz): Take the error cause into account when writing to the XML sink. - - errors.Sort(new CounterexampleComparer()); - foreach (Counterexample error in errors) - { - if (error is CallCounterexample) - { - CallCounterexample err = (CallCounterexample)error; - if (!CommandLineOptions.Clo.ForceBplErrors && err.FailingRequires.ErrorMessage != null) - { - ReportBplError(err.FailingRequires, err.FailingRequires.ErrorMessage, true, false); - } - else - { - ReportBplError(err.FailingCall, cause + " BP5002: A precondition for this call might not hold.", true, true); - ReportBplError(err.FailingRequires, "Related location: This is the precondition that might not hold.", false, true); - } - if (CommandLineOptions.Clo.XmlSink != null) - { - CommandLineOptions.Clo.XmlSink.WriteError("precondition violation", err.FailingCall.tok, err.FailingRequires.tok, error.Trace); - } - } - else if (error is ReturnCounterexample) - { - ReturnCounterexample err = (ReturnCounterexample)error; - if (!CommandLineOptions.Clo.ForceBplErrors && err.FailingEnsures.ErrorMessage != null) - { - ReportBplError(err.FailingEnsures, err.FailingEnsures.ErrorMessage, true, false); - } - else - { - ReportBplError(err.FailingReturn, cause + " BP5003: A postcondition might not hold on this return path.", true, true); - ReportBplError(err.FailingEnsures, "Related location: This is the postcondition that might not hold.", false, true); - } - if (CommandLineOptions.Clo.XmlSink != null) - { - CommandLineOptions.Clo.XmlSink.WriteError("postcondition violation", err.FailingReturn.tok, err.FailingEnsures.tok, error.Trace); - } - } - else // error is AssertCounterexample - { - AssertCounterexample err = (AssertCounterexample)error; - if (err.FailingAssert is LoopInitAssertCmd) - { - ReportBplError(err.FailingAssert, cause + " BP5004: This loop invariant might not hold on entry.", true, true); - if (CommandLineOptions.Clo.XmlSink != null) - { - CommandLineOptions.Clo.XmlSink.WriteError("loop invariant entry violation", err.FailingAssert.tok, null, error.Trace); - } - } - else if (err.FailingAssert is LoopInvMaintainedAssertCmd) - { - // this assertion is a loop invariant which is not maintained - ReportBplError(err.FailingAssert, cause + " BP5005: This loop invariant might not be maintained by the loop.", true, true); - if (CommandLineOptions.Clo.XmlSink != null) - { - CommandLineOptions.Clo.XmlSink.WriteError("loop invariant maintenance violation", err.FailingAssert.tok, null, error.Trace); - } - } - else - { - if (!CommandLineOptions.Clo.ForceBplErrors && err.FailingAssert.ErrorMessage != null) - { - ReportBplError(err.FailingAssert, err.FailingAssert.ErrorMessage, true, false); - } - else if (err.FailingAssert.ErrorData is string) - { - ReportBplError(err.FailingAssert, (string)err.FailingAssert.ErrorData, true, true); - } - else - { - ReportBplError(err.FailingAssert, cause + " BP5001: This assertion might not hold.", true, true); - } - if (CommandLineOptions.Clo.XmlSink != null) - { - CommandLineOptions.Clo.XmlSink.WriteError("assertion violation", err.FailingAssert.tok, null, error.Trace); - } - } - } - if (CommandLineOptions.Clo.EnhancedErrorMessages == 1) - { - foreach (string info in error.relatedInformation) - { - Contract.Assert(info != null); - Console.WriteLine(" " + info); - } - } - if (CommandLineOptions.Clo.ErrorTrace > 0) - { - Console.WriteLine("Execution trace:"); - error.Print(4); - } - if (CommandLineOptions.Clo.ModelViewFile != null) - { - error.PrintModel(); - } - if (cause == "Error") - { - errorCount++; - } - } - if (cause == "Error") - { - printer.Inform(String.Format("{0}error{1}", timeIndication, errors.Count == 1 ? "" : "s")); - } - } - } - - - /// - /// Given a resolved and type checked Boogie program, infers invariants for the program - /// and then attempts to verify it. Returns: - /// - Done if command line specified no verification - /// - FatalError if a fatal error occurred, in which case an error has been printed to console - /// - VerificationCompleted if inference and verification completed, in which the out - /// parameters contain meaningful values - /// - static PipelineOutcome InferAndVerify(Program program, - out int errorCount, out int verified, out int inconclusives, out int timeOuts, out int outOfMemories) { - Contract.Requires(program != null); - Contract.Ensures(0 <= Contract.ValueAtReturn(out inconclusives) && 0 <= Contract.ValueAtReturn(out timeOuts)); - - errorCount = verified = inconclusives = timeOuts = outOfMemories = 0; - - // ---------- Infer invariants -------------------------------------------------------- - - // Abstract interpretation -> Always use (at least) intervals, if not specified otherwise (e.g. with the "/noinfer" switch) - if (CommandLineOptions.Clo.UseAbstractInterpretation) { - if (!CommandLineOptions.Clo.Ai.J_Intervals && !CommandLineOptions.Clo.Ai.J_Trivial) { - // use /infer:j as the default - CommandLineOptions.Clo.Ai.J_Intervals = true; - } - } - Microsoft.Boogie.AbstractInterpretation.NativeAbstractInterpretation.RunAbstractInterpretation(program); - - if (CommandLineOptions.Clo.LoopUnrollCount != -1) { - program.UnrollLoops(CommandLineOptions.Clo.LoopUnrollCount, CommandLineOptions.Clo.SoundLoopUnrolling); - } - - Dictionary> extractLoopMappingInfo = null; - if (CommandLineOptions.Clo.ExtractLoops) - { - extractLoopMappingInfo = program.ExtractLoops(); - } - - if (CommandLineOptions.Clo.PrintInstrumented) { - program.Emit(new TokenTextWriter(Console.Out)); - } - - if (CommandLineOptions.Clo.ExpandLambdas) { - LambdaHelper.ExpandLambdas(program); - //PrintBplFile ("-", program, true); - } - - // ---------- Verify ------------------------------------------------------------ - - if (!CommandLineOptions.Clo.Verify) { - return PipelineOutcome.Done; - } - - #region Run Houdini and verify - if (CommandLineOptions.Clo.ContractInfer) - { - if (CommandLineOptions.Clo.AbstractHoudini != null) - { - //CommandLineOptions.Clo.PrintErrorModel = 1; - CommandLineOptions.Clo.UseProverEvaluate = true; - CommandLineOptions.Clo.ModelViewFile = "z3model"; - CommandLineOptions.Clo.UseArrayTheory = true; - CommandLineOptions.Clo.TypeEncodingMethod = CommandLineOptions.TypeEncoding.Monomorphic; - Houdini.AbstractDomainFactory.Initialize(); - var domain = Houdini.AbstractDomainFactory.GetInstance(CommandLineOptions.Clo.AbstractHoudini); - - // Run Abstract Houdini - var abs = new Houdini.AbsHoudini(program, domain); - var absout = abs.ComputeSummaries(); - ProcessOutcome(absout.outcome, absout.errors, "", ref errorCount, ref verified, ref inconclusives, ref timeOuts, ref outOfMemories); - - //Houdini.PredicateAbs.Initialize(program); - //var abs = new Houdini.AbstractHoudini(program); - //abs.computeSummaries(new Houdini.PredicateAbs(program.TopLevelDeclarations.OfType().First().Name)); - - return PipelineOutcome.Done; - } - Houdini.Houdini houdini = new Houdini.Houdini(program); - Houdini.HoudiniOutcome outcome = houdini.PerformHoudiniInference(); - if (CommandLineOptions.Clo.PrintAssignment) - { - Console.WriteLine("Assignment computed by Houdini:"); - foreach (var x in outcome.assignment) - { - Console.WriteLine(x.Key + " = " + x.Value); - } - } - if (CommandLineOptions.Clo.Trace) - { - int numTrueAssigns = 0; - foreach (var x in outcome.assignment) - { - if (x.Value) - numTrueAssigns++; - } - Console.WriteLine("Number of true assignments = " + numTrueAssigns); - Console.WriteLine("Number of false assignments = " + (outcome.assignment.Count - numTrueAssigns)); - Console.WriteLine("Prover time = " + Houdini.HoudiniSession.proverTime.ToString("F2")); - Console.WriteLine("Unsat core prover time = " + Houdini.HoudiniSession.unsatCoreProverTime.ToString("F2")); - Console.WriteLine("Number of prover queries = " + Houdini.HoudiniSession.numProverQueries); - Console.WriteLine("Number of unsat core prover queries = " + Houdini.HoudiniSession.numUnsatCoreProverQueries); - Console.WriteLine("Number of unsat core prunings = " + Houdini.HoudiniSession.numUnsatCorePrunings); - } - - foreach (Houdini.VCGenOutcome x in outcome.implementationOutcomes.Values) - { - ProcessOutcome(x.outcome, x.errors, "", ref errorCount, ref verified, ref inconclusives, ref timeOuts, ref outOfMemories); - } - //errorCount = outcome.ErrorCount; - //verified = outcome.Verified; - //inconclusives = outcome.Inconclusives; - //timeOuts = outcome.TimeOuts; - //outOfMemories = 0; - return PipelineOutcome.Done; - } - #endregion - - #region Verify each implementation - - ConditionGeneration vcgen = null; - try { - if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) { - vcgen = new DCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend); - } - else if (CommandLineOptions.Clo.FixedPointEngine != null) - { - vcgen = new FixedpointVC(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend); - } - else if (CommandLineOptions.Clo.StratifiedInlining > 0) - { - vcgen = new StratifiedVCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend); - } - else - { - vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend); - } - } catch (ProverException e) { - printer.ErrorWriteLine("Fatal Error: ProverException: {0}", e); - return PipelineOutcome.FatalError; - } - - // operate on a stable copy, in case it gets updated while we're running - var decls = program.TopLevelDeclarations.ToArray(); - - var impls = - from d in decls - where d != null && d is Implementation && CommandLineOptions.Clo.UserWantsToCheckRoutine(cce.NonNull(((Implementation)d).Name)) && !((Implementation)d).SkipVerification - select (Implementation)d; - - var prioritizedImpls = - from i in impls - orderby i.Priority descending - select i; - - foreach (var impl in prioritizedImpls) - { - int prevAssertionCount = vcgen.CumulativeAssertionCount; - List/*?*/ errors; - - DateTime start = new DateTime(); // to please compiler's definite assignment rules - if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.TraceProofObligations || CommandLineOptions.Clo.XmlSink != null) - { - start = DateTime.UtcNow; - if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.TraceProofObligations) - { - Console.WriteLine(); - Console.WriteLine("Verifying {0} ...", impl.Name); - } - if (CommandLineOptions.Clo.XmlSink != null) - { - CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, start); - } - } - - VCGen.Outcome outcome; - try - { - if (CommandLineOptions.Clo.inferLeastForUnsat != null) - { - var svcgen = vcgen as VC.StratifiedVCGen; - Contract.Assert(svcgen != null); - var ss = new HashSet(); - foreach (var tdecl in program.TopLevelDeclarations) - { - var c = tdecl as Constant; - if (c == null || !c.Name.StartsWith(CommandLineOptions.Clo.inferLeastForUnsat)) continue; - ss.Add(c.Name); - } - outcome = svcgen.FindLeastToVerify(impl, ref ss); - errors = new List(); - Console.Write("Result: "); - foreach (var s in ss) - { - Console.Write("{0} ", s); - } - Console.WriteLine(); - } - else - { - if (!VerificationResultCache.ContainsKey(impl.Id) || VerificationResultCache[impl.Id].Checksum != impl.Checksum) - { - outcome = vcgen.VerifyImplementation(impl, out errors); - } - else - { - if (CommandLineOptions.Clo.Trace) - { - Console.WriteLine("Retrieving cached verification result for implementation {0}...", impl.Name); - } - var result = VerificationResultCache[impl.Id]; - outcome = result.Outcome; - errors = result.Errors; - } - if (CommandLineOptions.Clo.ExtractLoops && vcgen is VCGen && errors != null) - { - for (int i = 0; i < errors.Count; i++) - { - errors[i] = (vcgen as VCGen).extractLoopTrace(errors[i], impl.Name, program, extractLoopMappingInfo); - } - } - } - } - catch (VCGenException e) - { - ReportBplError(impl, String.Format("Error BP5010: {0} Encountered in implementation {1}.", e.Message, impl.Name), true, true); - errors = null; - outcome = VCGen.Outcome.Inconclusive; - } - catch (UnexpectedProverOutputException upo) - { - printer.AdvisoryWriteLine("Advisory: {0} SKIPPED because of internal error: unexpected prover output: {1}", impl.Name, upo.Message); - errors = null; - outcome = VCGen.Outcome.Inconclusive; - } - - string timeIndication = ""; - DateTime end = DateTime.UtcNow; - TimeSpan elapsed = end - start; - if (CommandLineOptions.Clo.Trace) - { - int poCount = vcgen.CumulativeAssertionCount - prevAssertionCount; - timeIndication = string.Format(" [{0:F3} s, {1} proof obligation{2}] ", elapsed.TotalSeconds, poCount, poCount == 1 ? "" : "s"); - } - else if (CommandLineOptions.Clo.TraceProofObligations) - { - int poCount = vcgen.CumulativeAssertionCount - prevAssertionCount; - timeIndication = string.Format(" [{0} proof obligation{1}] ", poCount, poCount == 1 ? "" : "s"); - } - - if (CommandLineOptions.Clo.VerifySnapshots && !string.IsNullOrEmpty(impl.Checksum)) - { - var result = new VerificationResult(impl.Checksum, outcome, errors); - VerificationResultCache[impl.Id] = result; - } - - ProcessOutcome(outcome, errors, timeIndication, ref errorCount, ref verified, ref inconclusives, ref timeOuts, ref outOfMemories); - - if (CommandLineOptions.Clo.XmlSink != null) - { - CommandLineOptions.Clo.XmlSink.WriteEndMethod(outcome.ToString().ToLowerInvariant(), end, elapsed); - } - if (outcome == VCGen.Outcome.Errors || CommandLineOptions.Clo.Trace) - { - Console.Out.Flush(); - } - } - - vcgen.Close(); - cce.NonNull(CommandLineOptions.Clo.TheProverFactory).Close(); - - - #endregion - - return PipelineOutcome.VerificationCompleted; - } - - - #region Console output - - static OutputPrinter printer = new ConsolePrinter(); - - #endregion - - - #region Verification result caching - - private struct VerificationResult - { - internal VerificationResult(string checksum, ConditionGeneration.Outcome outcome, List errors) - { - Checksum = checksum; - Outcome = outcome; - Errors = errors; - } - - public readonly string Checksum; - public readonly ConditionGeneration.Outcome Outcome; - public readonly List Errors; - } - - - private static readonly ConcurrentDictionary VerificationResultCache = new ConcurrentDictionary(); - - #endregion - + #region // TODO: Is this still used? @@ -913,6 +131,5 @@ namespace Microsoft.Boogie { } #endregion - } } diff --git a/Source/BoogieDriver/BoogieDriver.csproj b/Source/BoogieDriver/BoogieDriver.csproj index 2478a7d4..9f71e5bd 100644 --- a/Source/BoogieDriver/BoogieDriver.csproj +++ b/Source/BoogieDriver/BoogieDriver.csproj @@ -230,6 +230,10 @@ {884386a3-58e9-40bb-a273-b24976775553} Doomed + + {eaa5eb79-d475-4601-a59b-825c191cd25f} + ExecutionEngine + {69A2B0B8-BCAC-4101-AE7A-556FCC58C06E} Graph -- cgit v1.2.3