From 19610bec1f67716bf31ab34eca5d16120972e739 Mon Sep 17 00:00:00 2001 From: wuestholz Date: Thu, 13 Jun 2013 16:03:25 -0700 Subject: Removed unused code. --- Source/BoogieDriver/BoogieDriver.cs | 22 ---------------------- 1 file changed, 22 deletions(-) (limited to 'Source/BoogieDriver') diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 7eacf697..7e0e9732 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -100,27 +100,5 @@ namespace Microsoft.Boogie { Console.ReadLine(); } } - - - #region // TODO: Is this still used? - - enum FileType - { - Unknown, - Cil, - Bpl, - Dafny - }; - - - static bool ProgramHasDebugInfo(Program program) - { - Contract.Requires(program != null); - // We inspect the last declaration because the first comes from the prelude and therefore always has source context. - return program.TopLevelDeclarations.Count > 0 && - ((cce.NonNull(program.TopLevelDeclarations)[program.TopLevelDeclarations.Count - 1]).tok.IsValid); - } - - #endregion } } -- cgit v1.2.3 From 3019c32b81e0077e8d7dea93207869ab7b356b48 Mon Sep 17 00:00:00 2001 From: wuestholz Date: Fri, 21 Jun 2013 16:27:08 -0700 Subject: Did some refactoring in the execution engine and worked on the parallelization. --- Source/BoogieDriver/BoogieDriver.cs | 6 +- Source/ExecutionEngine/ExecutionEngine.cs | 384 ++++++++++++++++------------- Source/VCGeneration/Check.cs | 61 ++--- Source/VCGeneration/ConditionGeneration.cs | 52 ++-- Source/VCGeneration/VC.cs | 6 +- 5 files changed, 275 insertions(+), 234 deletions(-) (limited to 'Source/BoogieDriver') diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 7e0e9732..12a6084f 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -37,13 +37,13 @@ namespace Microsoft.Boogie { goto END; } if (CommandLineOptions.Clo.Files.Count == 0) { - ExecutionEngine.printer.ErrorWriteLine("*** Error: No input files were specified."); + ExecutionEngine.printer.ErrorWriteLine(Console.Out, "*** Error: No input files were specified."); goto END; } if (CommandLineOptions.Clo.XmlSink != null) { string errMsg = CommandLineOptions.Clo.XmlSink.Open(); if (errMsg != null) { - ExecutionEngine.printer.ErrorWriteLine("*** Error: " + errMsg); + ExecutionEngine.printer.ErrorWriteLine(Console.Out, "*** Error: " + errMsg); goto END; } } @@ -84,7 +84,7 @@ namespace Microsoft.Boogie { extension = extension.ToLower(); } if (extension != ".bpl") { - ExecutionEngine.printer.ErrorWriteLine("*** Error: '{0}': Filename extension '{1}' is not supported. Input files must be BoogiePL programs (.bpl).", file, + ExecutionEngine.printer.ErrorWriteLine(Console.Out, "*** Error: '{0}': Filename extension '{1}' is not supported. Input files must be BoogiePL programs (.bpl).", file, extension == null ? "" : extension); goto END; } diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 347642d1..a2eb52c8 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -6,6 +6,7 @@ using System.IO; using System.Linq; using System.Text.RegularExpressions; using System.Threading; +using System.Threading.Tasks; using VC; using BoogiePL = Microsoft.Boogie; @@ -17,24 +18,24 @@ namespace Microsoft.Boogie public interface OutputPrinter { - void ErrorWriteLine(string s); - void ErrorWriteLine(string format, params object[] args); + void ErrorWriteLine(TextWriter tw, string s); + void ErrorWriteLine(TextWriter tw, string format, params object[] args); void AdvisoryWriteLine(string format, params object[] args); - void Inform(string s); + void Inform(string s, TextWriter tw); void WriteTrailer(PipelineStatistics stats); - void WriteErrorInformation(ErrorInformation errorInfo); - void ReportBplError(IToken tok, string message, bool error, string category = null); + void WriteErrorInformation(ErrorInformation errorInfo, TextWriter tw, bool skipExecutionTrace = true); + void ReportBplError(IToken tok, string message, bool error, TextWriter tw, string category = null); } public class ConsolePrinter : OutputPrinter { - public void ErrorWriteLine(string s) + public void ErrorWriteLine(TextWriter tw, string s) { Contract.Requires(s != null); if (!s.Contains("Error: ") && !s.Contains("Error BP")) { - Console.WriteLine(s); + tw.WriteLine(s); return; } @@ -53,21 +54,21 @@ namespace Microsoft.Boogie ConsoleColor col = Console.ForegroundColor; Console.ForegroundColor = ConsoleColor.Red; - Console.WriteLine(s); + tw.WriteLine(s); Console.ForegroundColor = col; if (remaining != null) { - Console.WriteLine(remaining); + tw.WriteLine(remaining); } } - public void ErrorWriteLine(string format, params object[] args) + public void ErrorWriteLine(TextWriter tw, string format, params object[] args) { Contract.Requires(format != null); string s = string.Format(format, args); - ErrorWriteLine(s); + ErrorWriteLine(tw, s); } @@ -85,11 +86,11 @@ namespace Microsoft.Boogie /// Inform the user about something and proceed with translation normally. /// Print newline after the message. /// - public void Inform(string s) + public void Inform(string s, TextWriter tw) { if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.TraceProofObligations) { - Console.WriteLine(s); + tw.WriteLine(s); } } @@ -125,20 +126,26 @@ namespace Microsoft.Boogie } - public void WriteErrorInformation(ErrorInformation errorInfo) + public void WriteErrorInformation(ErrorInformation errorInfo, TextWriter tw, bool skipExecutionTrace = true) { Contract.Requires(errorInfo != null); - ReportBplError(errorInfo.Tok, errorInfo.FullMsg, true); + ReportBplError(errorInfo.Tok, errorInfo.FullMsg, true, tw); foreach (var e in errorInfo.Aux) { - ReportBplError(e.Tok, e.FullMsg, false); + if (!(skipExecutionTrace && e.Category.Contains("Execution trace"))) + { + ReportBplError(e.Tok, e.FullMsg, false, tw); + } } + + tw.Write(errorInfo.Out.ToString()); + tw.Flush(); } - public virtual void ReportBplError(IToken tok, string message, bool error, string category = null) + public virtual void ReportBplError(IToken tok, string message, bool error, TextWriter tw, string category = null) { Contract.Requires(message != null); @@ -157,11 +164,11 @@ namespace Microsoft.Boogie } if (error) { - ErrorWriteLine(s); + ErrorWriteLine(tw, s); } else { - Console.WriteLine(s); + tw.WriteLine(s); } } } @@ -227,6 +234,7 @@ namespace Microsoft.Boogie public string RequestId { get; set; } public ErrorKind Kind { get; set; } public string ImplementationName { get; set; } + public TextWriter Out = new StringWriter(); public string FullMsg { @@ -497,7 +505,7 @@ namespace Microsoft.Boogie public 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++) @@ -530,7 +538,7 @@ namespace Microsoft.Boogie } catch (IOException e) { - printer.ErrorWriteLine("Error opening file \"{0}\": {1}", bplFileName, e.Message); + printer.ErrorWriteLine(Console.Out, "Error opening file \"{0}\": {1}", bplFileName, e.Message); okay = false; continue; } @@ -655,31 +663,22 @@ namespace Microsoft.Boogie } if (inline) { - foreach (var d in TopLevelDeclarations) + foreach (var impl in TopLevelDeclarations.OfType()) { - var impl = d as Implementation; - if (impl != null) - { - impl.OriginalBlocks = impl.Blocks; - impl.OriginalLocVars = impl.LocVars; - } + impl.OriginalBlocks = impl.Blocks; + impl.OriginalLocVars = impl.LocVars; } - foreach (var d in TopLevelDeclarations) + foreach (var impl in TopLevelDeclarations.OfType()) { - var impl = d as Implementation; - if (impl != null && !impl.SkipVerification) + if (!impl.SkipVerification) { Inliner.ProcessImplementation(program, impl); } } - foreach (var d in TopLevelDeclarations) + foreach (var impl in TopLevelDeclarations.OfType()) { - var impl = d as Implementation; - if (impl != null) - { - impl.OriginalBlocks = null; - impl.OriginalLocVars = null; - } + impl.OriginalBlocks = null; + impl.OriginalLocVars = null; } } } @@ -755,36 +754,6 @@ namespace Microsoft.Boogie } #endregion - #region Set up the VC generation - - 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; - } - - #endregion - #region Select and prioritize implementations that should be verified var impls = program.TopLevelDeclarations.OfType().Where( @@ -807,141 +776,198 @@ namespace Microsoft.Boogie #region Verify each implementation - foreach (var impl in stablePrioritizedImpls) - { - VerificationResult verificationResult = null; - - printer.Inform(string.Format("\nVerifying {0} ...", impl.Name)); - - if (CommandLineOptions.Clo.VerifySnapshots) - { - verificationResult = Cache.Lookup(impl); - } + var outputs = new StringWriter[stablePrioritizedImpls.Count()]; + var nextPrintableIndex = 0; - if (verificationResult != null) - { - if (CommandLineOptions.Clo.XmlSink != null) - { - CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, verificationResult.Start); - } - - printer.Inform(string.Format("Retrieving cached verification result for implementation {0}...", impl.Name)); - } - else + try + { + Parallel.For(0, stablePrioritizedImpls.Count(), new ParallelOptions { MaxDegreeOfParallelism = 1 }, index => { - #region Verify the implementation + Implementation impl = stablePrioritizedImpls[index]; + VerificationResult verificationResult = null; + var output = new StringWriter(); - verificationResult = new VerificationResult(requestId, impl.Checksum, impl.DependenciesChecksum); - verificationResult.ImplementationName = impl.Name; - verificationResult.ImplementationToken = impl.tok; - verificationResult.ProofObligationCountBefore = vcgen.CumulativeAssertionCount; - verificationResult.Start = DateTime.UtcNow; + printer.Inform(string.Format("\nVerifying {0} ...", impl.Name), output); - if (CommandLineOptions.Clo.XmlSink != null) + if (CommandLineOptions.Clo.VerifySnapshots) { - CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, verificationResult.Start); + verificationResult = Cache.Lookup(impl); } - try + if (verificationResult != null) { - if (CommandLineOptions.Clo.inferLeastForUnsat != null) + if (CommandLineOptions.Clo.XmlSink != 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); - } - verificationResult.Outcome = svcgen.FindLeastToVerify(impl, ref ss); - verificationResult.Errors = new List(); - Console.WriteLine("Result: {0}", string.Join(" ", ss)); + CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, verificationResult.Start); } - else + + printer.Inform(string.Format("Retrieving cached verification result for implementation {0}...", impl.Name), output); + } + else + { + #region Verify the implementation + + verificationResult = new VerificationResult(requestId, impl.Checksum, impl.DependenciesChecksum); + verificationResult.ImplementationName = impl.Name; + verificationResult.ImplementationToken = impl.tok; + + using (var vcgen = CreateVCGen(program)) { - verificationResult.Outcome = vcgen.VerifyImplementation(impl, out verificationResult.Errors, requestId); + verificationResult.ProofObligationCountBefore = vcgen.CumulativeAssertionCount; + verificationResult.Start = DateTime.UtcNow; - if (CommandLineOptions.Clo.ExtractLoops && verificationResult.Errors != null) + if (CommandLineOptions.Clo.XmlSink != null) { - var vcg = vcgen as VCGen; - if (vcg != null) + CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, verificationResult.Start); + } + try + { + if (CommandLineOptions.Clo.inferLeastForUnsat != null) { - for (int i = 0; i < verificationResult.Errors.Count; i++) + var svcgen = vcgen as VC.StratifiedVCGen; + Contract.Assert(svcgen != null); + var ss = new HashSet(); + foreach (var tdecl in program.TopLevelDeclarations) { - verificationResult.Errors[i] = vcg.extractLoopTrace(verificationResult.Errors[i], impl.Name, program, extractLoopMappingInfo); + var c = tdecl as Constant; + if (c == null || !c.Name.StartsWith(CommandLineOptions.Clo.inferLeastForUnsat)) continue; + ss.Add(c.Name); + } + verificationResult.Outcome = svcgen.FindLeastToVerify(impl, ref ss); + verificationResult.Errors = new List(); + output.WriteLine("Result: {0}", string.Join(" ", ss)); + } + else + { + verificationResult.Outcome = vcgen.VerifyImplementation(impl, out verificationResult.Errors, requestId); + if (CommandLineOptions.Clo.ExtractLoops && verificationResult.Errors != null) + { + var vcg = vcgen as VCGen; + if (vcg != null) + { + for (int i = 0; i < verificationResult.Errors.Count; i++) + { + verificationResult.Errors[i] = vcg.extractLoopTrace(verificationResult.Errors[i], impl.Name, program, extractLoopMappingInfo); + } + } } } } - } - } - catch (VCGenException e) - { - var errorInfo = errorInformationFactory.CreateErrorInformation(impl.tok, String.Format("{0} (encountered in implementation {1}).", e.Message, impl.Name), requestId, "Error"); - errorInfo.BoogieErrorCode = "BP5010"; - errorInfo.ImplementationName = impl.Name; - printer.WriteErrorInformation(errorInfo); - if (er != null) - { - lock (er) + catch (VCGenException e) + { + var errorInfo = errorInformationFactory.CreateErrorInformation(impl.tok, String.Format("{0} (encountered in implementation {1}).", e.Message, impl.Name), requestId, "Error"); + errorInfo.BoogieErrorCode = "BP5010"; + errorInfo.ImplementationName = impl.Name; + printer.WriteErrorInformation(errorInfo, output); + if (er != null) + { + lock (er) + { + er(errorInfo); + } + } + verificationResult.Errors = null; + verificationResult.Outcome = VCGen.Outcome.Inconclusive; + } + catch (UnexpectedProverOutputException upo) { - er(errorInfo); + printer.AdvisoryWriteLine("Advisory: {0} SKIPPED because of internal error: unexpected prover output: {1}", impl.Name, upo.Message); + verificationResult.Errors = null; + verificationResult.Outcome = VCGen.Outcome.Inconclusive; } + + verificationResult.ProofObligationCountAfter = vcgen.CumulativeAssertionCount; + verificationResult.End = DateTime.UtcNow; } - verificationResult.Errors = null; - verificationResult.Outcome = VCGen.Outcome.Inconclusive; - } - catch (UnexpectedProverOutputException upo) - { - printer.AdvisoryWriteLine("Advisory: {0} SKIPPED because of internal error: unexpected prover output: {1}", impl.Name, upo.Message); - verificationResult.Errors = null; - verificationResult.Outcome = VCGen.Outcome.Inconclusive; + + #endregion + + #region Cache the verification result + + if (CommandLineOptions.Clo.VerifySnapshots && !string.IsNullOrEmpty(impl.Checksum)) + { + Cache.Insert(impl.Id, verificationResult); + } + + #endregion } - verificationResult.ProofObligationCountAfter = vcgen.CumulativeAssertionCount; - verificationResult.End = DateTime.UtcNow; + #region Process the verification results and statistics - #endregion + ProcessOutcome(verificationResult.Outcome, verificationResult.Errors, TimeIndication(verificationResult), stats, output, er, verificationResult.ImplementationName, verificationResult.ImplementationToken, verificationResult.RequestId); - #region Cache the verification result + ProcessErrors(verificationResult.Errors, verificationResult.Outcome, output, er, impl); - if (CommandLineOptions.Clo.VerifySnapshots && !string.IsNullOrEmpty(impl.Checksum)) + if (CommandLineOptions.Clo.XmlSink != null) { - Cache.Insert(impl.Id, verificationResult); + CommandLineOptions.Clo.XmlSink.WriteEndMethod(verificationResult.Outcome.ToString().ToLowerInvariant(), verificationResult.End, verificationResult.End - verificationResult.Start); } - #endregion - } + outputs[index] = output; - #region Process the verification results and statistics + lock (outputs) + { + for (; nextPrintableIndex < stablePrioritizedImpls.Count() && outputs[nextPrintableIndex] != null; nextPrintableIndex++) + { + Console.Write(outputs[nextPrintableIndex].ToString()); + Console.Out.Flush(); + } + } - ProcessOutcome(verificationResult.Outcome, verificationResult.Errors, TimeIndication(verificationResult), stats, er, verificationResult.ImplementationName, verificationResult.ImplementationToken, verificationResult.RequestId); + if (verificationResult.Outcome == VCGen.Outcome.Errors || CommandLineOptions.Clo.Trace) + { + Console.Out.Flush(); + } - ProcessErrors(verificationResult.Errors, verificationResult.Outcome, er, impl); + #endregion + }); + } + catch (ProverException e) + { + printer.ErrorWriteLine(Console.Out, "Fatal Error: ProverException: {0}", e); + return PipelineOutcome.FatalError; + } - if (CommandLineOptions.Clo.XmlSink != null) - { - CommandLineOptions.Clo.XmlSink.WriteEndMethod(verificationResult.Outcome.ToString().ToLowerInvariant(), verificationResult.End, verificationResult.End - verificationResult.Start); - } + cce.NonNull(CommandLineOptions.Clo.TheProverFactory).Close(); - if (verificationResult.Outcome == VCGen.Outcome.Errors || CommandLineOptions.Clo.Trace) + lock (outputs) + { + for (; nextPrintableIndex < stablePrioritizedImpls.Count() && nextPrintableIndex != null; nextPrintableIndex++) { + Console.Write(outputs[nextPrintableIndex].ToString()); Console.Out.Flush(); } - - #endregion } - vcgen.Close(); - cce.NonNull(CommandLineOptions.Clo.TheProverFactory).Close(); - #endregion return PipelineOutcome.VerificationCompleted; } + private static ConditionGeneration CreateVCGen(Program program) + { + ConditionGeneration vcgen = null; + 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); + } + return vcgen; + } + + #region Houdini private static PipelineOutcome RunHoudini(Program program, PipelineStatistics stats, ErrorReporterDelegate er) @@ -984,8 +1010,8 @@ namespace Microsoft.Boogie foreach (Houdini.VCGenOutcome x in outcome.implementationOutcomes.Values) { - ProcessOutcome(x.outcome, x.errors, "", stats, er); - ProcessErrors(x.errors, x.outcome, er); + ProcessOutcome(x.outcome, x.errors, "", stats, Console.Out, er); + ProcessErrors(x.errors, x.outcome, Console.Out, er); } //errorCount = outcome.ErrorCount; //verified = outcome.Verified; @@ -1011,8 +1037,8 @@ namespace Microsoft.Boogie // Run Abstract Houdini var abs = new Houdini.AbsHoudini(program, domain); var absout = abs.ComputeSummaries(); - ProcessOutcome(absout.outcome, absout.errors, "", stats, er); - ProcessErrors(absout.errors, absout.outcome, er); + ProcessOutcome(absout.outcome, absout.errors, "", stats, Console.Out, er); + ProcessErrors(absout.errors, absout.outcome, Console.Out, er); //Houdini.PredicateAbs.Initialize(program); //var abs = new Houdini.AbstractHoudini(program); @@ -1040,26 +1066,26 @@ namespace Microsoft.Boogie private static void ProcessOutcome(VC.VCGen.Outcome outcome, List errors, string timeIndication, - PipelineStatistics stats, ErrorReporterDelegate er = null, string implName = null, IToken implTok = null, string requestId = null) + PipelineStatistics stats, TextWriter tw, ErrorReporterDelegate er = null, string implName = null, IToken implTok = null, string requestId = null) { Contract.Requires(stats != null); UpdateStatistics(stats, outcome, errors); - printer.Inform(timeIndication + OutcomeIndication(outcome, errors)); + printer.Inform(timeIndication + OutcomeIndication(outcome, errors), tw); - ReportOutcome(outcome, er, implName, implTok, requestId); + ReportOutcome(outcome, er, implName, implTok, requestId, tw); } - private static void ReportOutcome(VC.VCGen.Outcome outcome, ErrorReporterDelegate er, string implName, IToken implTok, string requestId) + private static void ReportOutcome(VC.VCGen.Outcome outcome, ErrorReporterDelegate er, string implName, IToken implTok, string requestId, TextWriter tw) { ErrorInformation errorInfo = null; switch (outcome) { case VCGen.Outcome.ReachedBound: - Console.WriteLine(string.Format("Stratified Inlining: Reached recursion bound of {0}", CommandLineOptions.Clo.RecursionBound)); + tw.WriteLine(string.Format("Stratified Inlining: Reached recursion bound of {0}", CommandLineOptions.Clo.RecursionBound)); break; case VCGen.Outcome.TimedOut: if (implName != null && implTok != null) @@ -1081,12 +1107,15 @@ namespace Microsoft.Boogie break; } - if (er != null && errorInfo != null) + if (errorInfo != null) { errorInfo.ImplementationName = implName; - lock (er) + if (er != null) { - er(errorInfo); + lock (er) + { + er(errorInfo); + } } } } @@ -1162,7 +1191,7 @@ namespace Microsoft.Boogie } - private static void ProcessErrors(List errors, VC.VCGen.Outcome outcome, ErrorReporterDelegate er, Implementation impl = null) + private static void ProcessErrors(List errors, VC.VCGen.Outcome outcome, TextWriter tw, ErrorReporterDelegate er, Implementation impl = null) { var implName = impl != null ? impl.Name : null; @@ -1174,8 +1203,6 @@ namespace Microsoft.Boogie var errorInfo = CreateErrorInformation(error, outcome); errorInfo.ImplementationName = implName; - printer.WriteErrorInformation(errorInfo); - if (CommandLineOptions.Clo.XmlSink != null) { WriteErrorInformationToXmlSink(errorInfo, error.Trace); @@ -1186,18 +1213,21 @@ namespace Microsoft.Boogie foreach (string info in error.relatedInformation) { Contract.Assert(info != null); - Console.WriteLine(" " + info); + errorInfo.Out.WriteLine(" " + info); } } if (CommandLineOptions.Clo.ErrorTrace > 0) { - Console.WriteLine("Execution trace:"); - error.Print(4, b => { errorInfo.AddAuxInfo(b.tok, b.Label, "Execution trace"); }); + errorInfo.Out.WriteLine("Execution trace:"); + error.Print(4, errorInfo.Out, b => { errorInfo.AddAuxInfo(b.tok, b.Label, "Execution trace"); }); } if (CommandLineOptions.Clo.ModelViewFile != null) { - error.PrintModel(); + error.PrintModel(errorInfo.Out); } + + printer.WriteErrorInformation(errorInfo, tw); + if (er != null) { lock (er) diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index 6897a982..a0454229 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -4,6 +4,7 @@ // //----------------------------------------------------------------------------- using System; +using System.Linq; using System.Collections; using System.Collections.Generic; using System.Threading; @@ -159,54 +160,38 @@ namespace Microsoft.Boogie { private static void Setup(Program prog, ProverContext ctx) { - // set up the context - foreach (Declaration decl in prog.TopLevelDeclarations) + // set up the context + foreach (Declaration decl in prog.TopLevelDeclarations.ToList()) + { + Contract.Assert(decl != null); + var typeDecl = decl as TypeCtorDecl; + var constDecl = decl as Constant; + var funDecl = decl as Function; + var axiomDecl = decl as Axiom; + var glVarDecl = decl as GlobalVariable; + if (typeDecl != null) { - Contract.Assert(decl != null); - TypeCtorDecl t = decl as TypeCtorDecl; - if (t != null) - { - ctx.DeclareType(t, null); - } + ctx.DeclareType(typeDecl, null); } - foreach (Declaration decl in prog.TopLevelDeclarations) + else if (constDecl != null) { - Contract.Assert(decl != null); - Constant c = decl as Constant; - if (c != null) - { - ctx.DeclareConstant(c, c.Unique, null); - } - else - { - Function f = decl as Function; - if (f != null) - { - ctx.DeclareFunction(f, null); - } - } + ctx.DeclareConstant(constDecl, constDecl.Unique, null); } - foreach (Declaration decl in prog.TopLevelDeclarations) + else if (funDecl != null) { - Contract.Assert(decl != null); - Axiom ax = decl as Axiom; - if (ax != null) - { - ctx.AddAxiom(ax, null); - } + ctx.DeclareFunction(funDecl, null); } - foreach (Declaration decl in prog.TopLevelDeclarations) + else if (axiomDecl != null) { - Contract.Assert(decl != null); - GlobalVariable v = decl as GlobalVariable; - if (v != null) - { - ctx.DeclareGlobalVariable(v, null); - } + ctx.AddAxiom(axiomDecl, null); } + else if (glVarDecl != null) + { + ctx.DeclareGlobalVariable(glVarDecl, null); + } + } } - /// /// Clean-up. /// diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 3ae97bdd..bcafb9cb 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -4,6 +4,7 @@ // //----------------------------------------------------------------------------- using System; +using System.Linq; using System.Collections; using System.Collections.Generic; using System.Diagnostics; @@ -147,14 +148,14 @@ namespace Microsoft.Boogie { return naryExpr.Fun.FunctionName; } - public void Print(int indent, Action blockAction = null) { + public void Print(int indent, TextWriter tw, Action blockAction = null) { int numBlock = -1; string ind = new string(' ', indent); foreach (Block b in Trace) { Contract.Assert(b != null); numBlock++; if (b.tok == null) { - Console.WriteLine("{0}", ind); + tw.WriteLine("{0}", ind); } else { // for ErrorTrace == 1 restrict the output; // do not print tokens with -17:-4 as their location because they have been @@ -165,7 +166,7 @@ namespace Microsoft.Boogie { blockAction(b); } - Console.WriteLine("{4}{0}({1},{2}): {3}", b.tok.filename, b.tok.line, b.tok.col, b.Label, ind); + tw.WriteLine("{4}{0}({1},{2}): {3}", b.tok.filename, b.tok.line, b.tok.col, b.Label, ind); for (int numInstr = 0; numInstr < b.Cmds.Length; numInstr++) { @@ -178,13 +179,13 @@ namespace Microsoft.Boogie { { Contract.Assert(calleeCounterexamples[loc].args.Count == 1); var arg = calleeCounterexamples[loc].args[0]; - Console.WriteLine("{0}value = {1}", ind, arg.ToString()); + tw.WriteLine("{0}value = {1}", ind, arg.ToString()); } else { - Console.WriteLine("{1}Inlined call to procedure {0} begins", calleeName, ind); - calleeCounterexamples[loc].counterexample.Print(indent + 4); - Console.WriteLine("{1}Inlined call to procedure {0} ends", calleeName, ind); + tw.WriteLine("{1}Inlined call to procedure {0} begins", calleeName, ind); + calleeCounterexamples[loc].counterexample.Print(indent + 4, tw); + tw.WriteLine("{1}Inlined call to procedure {0} ends", calleeName, ind); } } } @@ -197,7 +198,7 @@ namespace Microsoft.Boogie { public bool ModelHasStatesAlready = false; - public void PrintModel() + public void PrintModel(TextWriter tw) { var filename = CommandLineOptions.Clo.ModelViewFile; if (Model == null || filename == null || CommandLineOptions.Clo.StratifiedInlining > 0) return; @@ -205,8 +206,8 @@ namespace Microsoft.Boogie { var m = ModelHasStatesAlready ? Model : this.GetModelWithStates(); if (filename == "-") { - m.Write(Console.Out); - Console.Out.Flush(); + m.Write(tw); + tw.Flush(); } else { using (var wr = new StreamWriter(filename, !firstModelFile)) { firstModelFile = false; @@ -532,7 +533,7 @@ namespace VC { } [ContractClass(typeof(ConditionGenerationContracts))] - public abstract class ConditionGeneration { + public abstract class ConditionGeneration : IDisposable { protected internal object CheckerCommonState; public enum Outcome { @@ -570,6 +571,9 @@ namespace VC { public int CumulativeAssertionCount; // for statistics protected readonly List/*!>!*/ checkers = new List(); + + private bool _disposed; + protected VariableSeq CurrentLocalVariables = null; // shared across each implementation; created anew for each implementation @@ -1626,6 +1630,24 @@ namespace VC { #endregion } + + public void Dispose() + { + Dispose(true); + GC.SuppressFinalize(this); + } + + protected virtual void Dispose(bool disposing) + { + if (!_disposed) + { + if (disposing) + { + Close(); + } + _disposed = true; + } + } } public class ModelViewInfo @@ -1643,10 +1665,10 @@ namespace VC { Contract.Requires(impl != null); // global variables - foreach (Declaration d in program.TopLevelDeclarations) { - if (d is Constant) continue; - if (d is Variable) { - AllVariables.Add((Variable)d); + foreach (Variable v in program.TopLevelDeclarations.OfType()) { + if (!(v is Constant)) + { + AllVariables.Add(v); } } // implementation parameters diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 6a0891b8..bea79f13 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1410,7 +1410,11 @@ namespace VC { } ModelViewInfo mvInfo; - Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = PassifyImpl(impl, out mvInfo); + Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins; + lock (program) + { + gotoCmdOrigins = PassifyImpl(impl, out mvInfo); + } double max_vc_cost = CommandLineOptions.Clo.VcsMaxCost; int tmp_max_vc_cost = -1, max_splits = CommandLineOptions.Clo.VcsMaxSplits, -- cgit v1.2.3