summaryrefslogtreecommitdiff
path: root/Source/ExecutionEngine/ExecutionEngine.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/ExecutionEngine/ExecutionEngine.cs')
-rw-r--r--Source/ExecutionEngine/ExecutionEngine.cs3586
1 files changed, 1826 insertions, 1760 deletions
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 31a69c6e..9bc855be 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -1,1760 +1,1826 @@
-using System;
-using System.Collections.Concurrent;
-using System.Collections.Generic;
-using System.Diagnostics.Contracts;
-using System.IO;
-using System.Linq;
-using System.Text.RegularExpressions;
-using System.Threading;
-using System.Threading.Tasks;
-using VC;
-using BoogiePL = Microsoft.Boogie;
-using System.Diagnostics;
-using System.Runtime.Caching;
-
-namespace Microsoft.Boogie
-{
-
- #region Output printing
-
- public interface OutputPrinter
- {
- 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, TextWriter tw);
- void WriteTrailer(PipelineStatistics stats);
- 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(TextWriter tw, string s)
- {
- Contract.Requires(s != null);
- if (!s.Contains("Error: ") && !s.Contains("Error BP"))
- {
- tw.WriteLine(s);
- return;
- }
-
- // split the string up into its first line and the remaining lines
- string remaining = null;
- int i = s.IndexOf('\r');
- if (0 <= i)
- {
- remaining = s.Substring(i + 1);
- if (remaining.StartsWith("\n"))
- {
- remaining = remaining.Substring(1);
- }
- s = s.Substring(0, i);
- }
-
- ConsoleColor col = Console.ForegroundColor;
- Console.ForegroundColor = ConsoleColor.Red;
- tw.WriteLine(s);
- Console.ForegroundColor = col;
-
- if (remaining != null)
- {
- tw.WriteLine(remaining);
- }
- }
-
-
- public void ErrorWriteLine(TextWriter tw, string format, params object[] args)
- {
- Contract.Requires(format != null);
- string s = string.Format(format, args);
- ErrorWriteLine(tw, s);
- }
-
-
- public void AdvisoryWriteLine(string format, params object[] args)
- {
- Contract.Requires(format != null);
- ConsoleColor col = Console.ForegroundColor;
- Console.ForegroundColor = ConsoleColor.Yellow;
- Console.WriteLine(format, args);
- Console.ForegroundColor = col;
- }
-
-
- /// <summary>
- /// Inform the user about something and proceed with translation normally.
- /// Print newline after the message.
- /// </summary>
- public void Inform(string s, TextWriter tw)
- {
- if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.TraceProofObligations)
- {
- tw.WriteLine(s);
- }
- }
-
-
- public void WriteTrailer(PipelineStatistics stats)
- {
- Contract.Requires(stats != null);
- Contract.Requires(0 <= stats.VerifiedCount && 0 <= stats.ErrorCount && 0 <= stats.InconclusiveCount && 0 <= stats.TimeoutCount && 0 <= stats.OutOfMemoryCount);
-
- Console.WriteLine();
- if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed)
- {
- Console.Write("{0} finished with {1} credible, {2} doomed{3}", CommandLineOptions.Clo.DescriptiveToolName, stats.VerifiedCount, stats.ErrorCount, stats.ErrorCount == 1 ? "" : "s");
- }
- else
- {
- Console.Write("{0} finished with {1} verified, {2} error{3}", CommandLineOptions.Clo.DescriptiveToolName, stats.VerifiedCount, stats.ErrorCount, stats.ErrorCount == 1 ? "" : "s");
- }
- if (stats.InconclusiveCount != 0)
- {
- Console.Write(", {0} inconclusive{1}", stats.InconclusiveCount, stats.InconclusiveCount == 1 ? "" : "s");
- }
- if (stats.TimeoutCount != 0)
- {
- Console.Write(", {0} time out{1}", stats.TimeoutCount, stats.TimeoutCount == 1 ? "" : "s");
- }
- if (stats.OutOfMemoryCount != 0)
- {
- Console.Write(", {0} out of memory", stats.OutOfMemoryCount);
- }
- Console.WriteLine();
- Console.Out.Flush();
- }
-
-
- public void WriteErrorInformation(ErrorInformation errorInfo, TextWriter tw, bool skipExecutionTrace = true)
- {
- Contract.Requires(errorInfo != null);
-
- ReportBplError(errorInfo.Tok, errorInfo.FullMsg, true, tw);
-
- foreach (var e in errorInfo.Aux)
- {
- if (!(skipExecutionTrace && e.Category.Contains("Execution trace")))
- {
- ReportBplError(e.Tok, e.FullMsg, false, tw);
- }
- }
-
- tw.Write(errorInfo.Out.ToString());
- tw.Write(errorInfo.Model.ToString());
- tw.Flush();
- }
-
-
- public virtual void ReportBplError(IToken tok, string message, bool error, TextWriter tw, string category = null)
- {
- Contract.Requires(message != null);
-
- if (category != null)
- {
- message = string.Format("{0}: {1}", category, message);
- }
- string s;
- if (tok != null)
- {
- s = string.Format("{0}({1},{2}): {3}", ExecutionEngine.GetFileNameForConsole(tok.filename), tok.line, tok.col, message);
- }
- else
- {
- s = message;
- }
- if (error)
- {
- ErrorWriteLine(tw, s);
- }
- else
- {
- tw.WriteLine(s);
- }
- }
- }
-
- #endregion
-
-
- public enum PipelineOutcome
- {
- Done,
- ResolutionError,
- TypeCheckingError,
- ResolvedAndTypeChecked,
- FatalError,
- VerificationCompleted
- }
-
-
- public class PipelineStatistics
- {
- public int ErrorCount;
- public int VerifiedCount;
- public int InconclusiveCount;
- public int TimeoutCount;
- public int OutOfMemoryCount;
- public long[] CachingActionCounts;
- public int CachedErrorCount;
- public int CachedVerifiedCount;
- public int CachedInconclusiveCount;
- public int CachedTimeoutCount;
- public int CachedOutOfMemoryCount;
- }
-
-
- #region Error reporting
-
- public delegate void ErrorReporterDelegate(ErrorInformation errInfo);
-
-
- public enum ErrorKind
- {
- Assertion,
- Precondition,
- Postcondition,
- InvariantEntry,
- InvariantMaintainance
- }
-
-
- public class ErrorInformationFactory
- {
- public virtual ErrorInformation CreateErrorInformation(IToken tok, string msg, string requestId = null, string originalRequestId = null, string category = null)
- {
- Contract.Requires(1 <= tok.line && 1 <= tok.col);
- Contract.Requires(msg != null);
-
- return ErrorInformation.CreateErrorInformation(tok, msg, requestId, originalRequestId, category);
- }
- }
-
-
- public class ErrorInformation
- {
- public readonly IToken Tok;
- public string Msg;
- public string Category { get; set; }
- public string BoogieErrorCode { get; set; }
- public readonly List<AuxErrorInfo> Aux = new List<AuxErrorInfo>();
- public string OriginalRequestId { get; set; }
- public string RequestId { get; set; }
- public ErrorKind Kind { get; set; }
- public string ImplementationName { get; set; }
- public TextWriter Out = new StringWriter();
- public TextWriter Model = new StringWriter();
-
- public string FullMsg
- {
- get
- {
- var prefix = Category;
- if (BoogieErrorCode != null)
- {
- prefix = prefix == null ? BoogieErrorCode : prefix + " " + BoogieErrorCode;
- }
- return prefix != null ? string.Format("{0}: {1}", prefix, Msg) : Msg;
- }
- }
-
- public struct AuxErrorInfo
- {
- public readonly IToken Tok;
- public readonly string Msg;
- public readonly string Category;
-
- public string FullMsg
- {
- get
- {
- return Category != null ? string.Format("{0}: {1}", Category, Msg) : Msg;
- }
- }
-
- public AuxErrorInfo(IToken tok, string msg, string category = null)
- {
- Tok = tok;
- Msg = CleanUp(msg);
- Category = category;
- }
- }
-
- protected ErrorInformation(IToken tok, string msg)
- {
- Contract.Requires(tok != null);
- Contract.Requires(1 <= tok.line && 1 <= tok.col);
- Contract.Requires(msg != null);
-
- Tok = tok;
- Msg = CleanUp(msg);
- }
-
- internal static ErrorInformation CreateErrorInformation(IToken tok, string msg, string requestId = null, string originalRequestId = null, string category = null)
- {
- var result = new ErrorInformation(tok, msg);
- result.RequestId = requestId;
- result.OriginalRequestId = originalRequestId;
- result.Category = category;
- return result;
- }
-
- public virtual void AddAuxInfo(IToken tok, string msg, string category = null)
- {
- Contract.Requires(tok != null);
- Contract.Requires(1 <= tok.line && 1 <= tok.col);
- Contract.Requires(msg != null);
- Aux.Add(new AuxErrorInfo(tok, msg, category));
- }
-
- protected static string CleanUp(string msg)
- {
- if (msg.ToLower().StartsWith("error: "))
- {
- return msg.Substring(7);
- }
- else
- {
- return msg;
- }
- }
- }
-
- #endregion
-
-
- public sealed class VerificationResult
- {
- public readonly string RequestId;
- public readonly string Checksum;
- public readonly string DependeciesChecksum;
- public readonly string ImplementationName;
- public readonly IToken ImplementationToken;
- public readonly string ProgramId;
-
- public DateTime Start { get; set; }
- public DateTime End { get; set; }
-
- public int ProofObligationCount { get { return ProofObligationCountAfter - ProofObligationCountBefore; } }
- public int ProofObligationCountBefore { get; set; }
- public int ProofObligationCountAfter { get; set; }
-
- public ConditionGeneration.Outcome Outcome { get; set; }
- public List<Counterexample> Errors;
-
- public ISet<byte[]> AssertionChecksums { get; private set; }
-
- public VerificationResult(string requestId, Implementation implementation, string programId = null)
- {
- Checksum = implementation.Checksum;
- DependeciesChecksum = implementation.DependencyChecksum;
- RequestId = requestId;
- ImplementationName = implementation.Name;
- ImplementationToken = implementation.tok;
- ProgramId = programId;
- AssertionChecksums = implementation.AssertionChecksums;
- }
- }
-
-
- public class PolymorphismChecker : ReadOnlyVisitor
- {
- bool isMonomorphic = true;
-
- public override DeclWithFormals VisitDeclWithFormals(DeclWithFormals node)
- {
- if (node.TypeParameters.Count > 0)
- isMonomorphic = false;
- return base.VisitDeclWithFormals(node);
- }
-
- public override BinderExpr VisitBinderExpr(BinderExpr node)
- {
- if (node.TypeParameters.Count > 0)
- isMonomorphic = false;
- return base.VisitBinderExpr(node);
- }
-
- public override MapType VisitMapType(MapType node)
- {
- if (node.TypeParameters.Count > 0)
- isMonomorphic = false;
- return base.VisitMapType(node);
- }
-
- public override Expr VisitNAryExpr(NAryExpr node)
- {
- BinaryOperator op = node.Fun as BinaryOperator;
- if (op != null && op.Op == BinaryOperator.Opcode.Subtype)
- isMonomorphic = false;
- return base.VisitNAryExpr(node);
- }
-
- public static bool IsMonomorphic(Program program)
- {
- var checker = new PolymorphismChecker();
- checker.VisitProgram(program);
- return checker.isMonomorphic;
- }
- }
-
- public class ExecutionEngine
- {
- public static OutputPrinter printer;
-
- public static ErrorInformationFactory errorInformationFactory = new ErrorInformationFactory();
-
- static int autoRequestIdCount;
-
- static readonly string AutoRequestIdPrefix = "auto_request_id_";
-
- public static string FreshRequestId()
- {
- var id = Interlocked.Increment(ref autoRequestIdCount);
- return AutoRequestIdPrefix + id;
- }
-
- public static int AutoRequestId(string id)
- {
- if (id.StartsWith(AutoRequestIdPrefix))
- {
- int result;
- if (int.TryParse(id.Substring(AutoRequestIdPrefix.Length), out result))
- {
- return result;
- }
- }
- return -1;
- }
-
- public readonly static VerificationResultCache Cache = new VerificationResultCache();
-
- static readonly MemoryCache programCache = new MemoryCache("ProgramCache");
- static readonly CacheItemPolicy policy = new CacheItemPolicy { SlidingExpiration = new TimeSpan(0, 10, 0), Priority = CacheItemPriority.Default };
-
- public static Program CachedProgram(string programId)
- {
- var result = programCache.Get(programId) as Program;
- return result;
- }
-
- static List<Checker> Checkers = new List<Checker>();
-
- static DateTime FirstRequestStart;
-
- static readonly ConcurrentDictionary<string, TimeSpan> TimePerRequest = new ConcurrentDictionary<string, TimeSpan>();
- static readonly ConcurrentDictionary<string, PipelineStatistics> StatisticsPerRequest = new ConcurrentDictionary<string, PipelineStatistics>();
-
- static readonly ConcurrentDictionary<string, CancellationTokenSource> ImplIdToCancellationTokenSource = new ConcurrentDictionary<string, CancellationTokenSource>();
-
- static readonly ConcurrentDictionary<string, CancellationTokenSource> RequestIdToCancellationTokenSource = new ConcurrentDictionary<string, CancellationTokenSource>();
-
- public static void ProcessFiles(List<string> fileNames, bool lookForSnapshots = true, string programId = null)
- {
- Contract.Requires(cce.NonNullElements(fileNames));
-
- if (programId == null)
- {
- programId = "main_program_id";
- }
-
- if (CommandLineOptions.Clo.VerifySeparately && 1 < fileNames.Count)
- {
- foreach (var f in fileNames)
- {
- ProcessFiles(new List<string> { f }, lookForSnapshots, f);
- }
- return;
- }
-
- if (0 <= CommandLineOptions.Clo.VerifySnapshots && lookForSnapshots)
- {
- var snapshotsByVersion = LookForSnapshots(fileNames);
- foreach (var s in snapshotsByVersion)
- {
- ProcessFiles(new List<string>(s), false, programId);
- }
- return;
- }
-
- using (XmlFileScope xf = new XmlFileScope(CommandLineOptions.Clo.XmlSink, fileNames[fileNames.Count - 1]))
- {
- Program program = ParseBoogieProgram(fileNames, false);
- if (program == null)
- return;
- if (CommandLineOptions.Clo.PrintFile != null)
- {
- PrintBplFile(CommandLineOptions.Clo.PrintFile, program, false, true, CommandLineOptions.Clo.PrettyPrint);
- }
-
- LinearTypeChecker linearTypeChecker;
- MoverTypeChecker moverTypeChecker;
- PipelineOutcome oc = ResolveAndTypecheck(program, fileNames[fileNames.Count - 1], out linearTypeChecker, out moverTypeChecker);
- if (oc != PipelineOutcome.ResolvedAndTypeChecked)
- return;
-
- if (CommandLineOptions.Clo.PrintCFGPrefix != null)
- {
- foreach (var impl in program.Implementations)
- {
- using (StreamWriter sw = new StreamWriter(CommandLineOptions.Clo.PrintCFGPrefix + "." + impl.Name + ".dot"))
- {
- sw.Write(program.ProcessLoops(impl).ToDot());
- }
- }
- }
-
- if (CommandLineOptions.Clo.StratifiedInlining == 0)
- {
- Concurrency.Transform(linearTypeChecker, moverTypeChecker);
- (new LinearEraser()).VisitProgram(program);
- if (CommandLineOptions.Clo.OwickiGriesDesugaredOutputFile != null)
- {
- int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured;
- CommandLineOptions.Clo.PrintUnstructured = 1;
- PrintBplFile(CommandLineOptions.Clo.OwickiGriesDesugaredOutputFile, program, false, false, CommandLineOptions.Clo.PrettyPrint);
- CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured;
- }
- }
-
- EliminateDeadVariables(program);
-
- CoalesceBlocks(program);
-
- Inline(program);
-
- var stats = new PipelineStatistics();
- oc = InferAndVerify(program, stats, 1 < CommandLineOptions.Clo.VerifySnapshots ? programId : null);
- switch (oc)
- {
- case PipelineOutcome.Done:
- case PipelineOutcome.VerificationCompleted:
- printer.WriteTrailer(stats);
- break;
- default:
- break;
- }
- }
- }
-
- public static IList<IList<string>> LookForSnapshots(IList<string> fileNames)
- {
- Contract.Requires(fileNames != null);
-
- var result = new List<IList<string>>();
- for (int version = 0; true; version++)
- {
- var nextSnapshot = new List<string>();
- 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())
- {
- result.Add(nextSnapshot);
- }
- else
- {
- break;
- }
- }
- return result;
- }
-
-
- public static void CoalesceBlocks(Program program)
- {
- if (CommandLineOptions.Clo.CoalesceBlocks)
- {
- if (CommandLineOptions.Clo.Trace)
- Console.WriteLine("Coalescing blocks...");
- Microsoft.Boogie.BlockCoalescer.CoalesceBlocks(program);
- }
- }
-
-
- public static void CollectModSets(Program program)
- {
- if (CommandLineOptions.Clo.DoModSetAnalysis)
- {
- new ModSetCollector().DoModSetAnalysis(program);
- }
- }
-
-
- public static void EliminateDeadVariables(Program program)
- {
- Microsoft.Boogie.UnusedVarEliminator.Eliminate(program);
- }
-
-
- public static void PrintBplFile(string filename, Program program, bool allowPrintDesugaring, bool setTokens = true, bool pretty = false)
- {
- 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>", Console.Out, setTokens, pretty) :
- new TokenTextWriter(filename, setTokens, pretty))
- {
- 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;
- }
-
-
- /// <summary>
- /// 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.
- /// </summary>
- public static Program ParseBoogieProgram(List<string> fileNames, bool suppressTraceOutput)
- {
- Contract.Requires(cce.NonNullElements(fileNames));
-
- 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 " + GetFileNameForConsole(bplFileName));
- }
- }
-
- Program programSnippet;
- int errorCount;
- try
- {
- var defines = new List<string>() { "FILE_" + fileId };
- errorCount = Parser.Parse(bplFileName, defines, out programSnippet, CommandLineOptions.Clo.UseBaseNameForFileName);
- if (programSnippet == null || errorCount != 0)
- {
- Console.WriteLine("{0} parse errors detected in {1}", errorCount, GetFileNameForConsole(bplFileName));
- okay = false;
- continue;
- }
- }
- catch (IOException e)
- {
- printer.ErrorWriteLine(Console.Out, "Error opening file \"{0}\": {1}", GetFileNameForConsole(bplFileName), e.Message);
- okay = false;
- continue;
- }
- if (program == null)
- {
- program = programSnippet;
- }
- else if (programSnippet != null)
- {
- program.AddTopLevelDeclarations(programSnippet.TopLevelDeclarations);
- }
- }
- if (!okay)
- {
- return null;
- }
- else if (program == null)
- {
- return new Program();
- }
- else
- {
- return program;
- }
- }
-
- internal static string GetFileNameForConsole(string filename)
- {
- return (CommandLineOptions.Clo.UseBaseNameForFileName && !string.IsNullOrEmpty(filename) && filename != "<console>") ? System.IO.Path.GetFileName(filename) : filename;
- }
-
-
- /// <summary>
- /// 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
- /// </summary>
- public static PipelineOutcome ResolveAndTypecheck(Program program, string bplFileName, out LinearTypeChecker linearTypeChecker, out MoverTypeChecker moverTypeChecker)
- {
- Contract.Requires(program != null);
- Contract.Requires(bplFileName != null);
-
- linearTypeChecker = null;
- moverTypeChecker = 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, GetFileNameForConsole(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, GetFileNameForConsole(bplFileName));
- return PipelineOutcome.TypeCheckingError;
- }
-
- if (PolymorphismChecker.IsMonomorphic(program))
- {
- CommandLineOptions.Clo.TypeEncodingMethod = CommandLineOptions.TypeEncoding.Monomorphic;
- }
-
- CollectModSets(program);
-
- moverTypeChecker = new MoverTypeChecker(program);
- moverTypeChecker.TypeCheck();
- if (moverTypeChecker.errorCount != 0)
- {
- Console.WriteLine("{0} type checking errors detected in {1}", moverTypeChecker.errorCount, GetFileNameForConsole(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, GetFileNameForConsole(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, true, CommandLineOptions.Clo.PrettyPrint);
- }
-
- return PipelineOutcome.ResolvedAndTypeChecked;
- }
-
-
- public static void Inline(Program program)
- {
- Contract.Requires(program != null);
-
- if (CommandLineOptions.Clo.Trace)
- Console.WriteLine("Inlining...");
-
- // Inline
- var TopLevelDeclarations = cce.NonNull(program.TopLevelDeclarations);
-
- if (CommandLineOptions.Clo.ProcedureInlining != CommandLineOptions.Inlining.None)
- {
- bool inline = false;
- foreach (var d in TopLevelDeclarations)
- {
- if ((d is Procedure || d is Implementation) && d.FindExprAttribute("inline") != null)
- {
- inline = true;
- }
- }
- if (inline)
- {
- foreach (var impl in TopLevelDeclarations.OfType<Implementation>())
- {
- impl.OriginalBlocks = impl.Blocks;
- impl.OriginalLocVars = impl.LocVars;
- }
- foreach (var impl in TopLevelDeclarations.OfType<Implementation>())
- {
- if (CommandLineOptions.Clo.UserWantsToCheckRoutine(impl.Name) && !impl.SkipVerification)
- {
- Inliner.ProcessImplementation(program, impl);
- }
- }
- foreach (var impl in TopLevelDeclarations.OfType<Implementation>())
- {
- impl.OriginalBlocks = null;
- impl.OriginalLocVars = null;
- }
- }
- }
- }
-
-
- /// <summary>
- /// 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
- /// </summary>
- public static PipelineOutcome InferAndVerify(Program program,
- PipelineStatistics stats,
- string programId = null,
- ErrorReporterDelegate er = null, string requestId = null)
- {
- Contract.Requires(program != null);
- Contract.Requires(stats != null);
- Contract.Ensures(0 <= Contract.ValueAtReturn(out stats.InconclusiveCount) && 0 <= Contract.ValueAtReturn(out stats.TimeoutCount));
-
- if (requestId == null)
- {
- requestId = FreshRequestId();
- }
-
- var start = DateTime.UtcNow;
-
- #region Do some pre-abstract-interpretation preprocessing on the program
- // Doing lambda expansion before abstract interpretation means that the abstract interpreter
- // never needs to see any lambda expressions. (On the other hand, if it were useful for it
- // to see lambdas, then it would be better to more lambda expansion until after infererence.)
- if (CommandLineOptions.Clo.ExpandLambdas) {
- LambdaHelper.ExpandLambdas(program);
- //PrintBplFile ("-", program, true);
- }
- #endregion
-
- #region Infer invariants using 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);
-
- #endregion
-
- #region Do some post-abstract-interpretation preprocessing on the program (e.g., loop unrolling)
-
- if (CommandLineOptions.Clo.LoopUnrollCount != -1)
- {
- program.UnrollLoops(CommandLineOptions.Clo.LoopUnrollCount, CommandLineOptions.Clo.SoundLoopUnrolling);
- }
-
- Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo = null;
- if (CommandLineOptions.Clo.ExtractLoops)
- {
- extractLoopMappingInfo = program.ExtractLoops();
- }
-
- if (CommandLineOptions.Clo.PrintInstrumented)
- {
- program.Emit(new TokenTextWriter(Console.Out, CommandLineOptions.Clo.PrettyPrint));
- }
- #endregion
-
- if (!CommandLineOptions.Clo.Verify)
- {
- return PipelineOutcome.Done;
- }
-
- #region Run Houdini and verify
- if (CommandLineOptions.Clo.ContractInfer)
- {
- return RunHoudini(program, stats, er);
- }
- #endregion
-
- #region Select and prioritize implementations that should be verified
-
- var impls = program.Implementations.Where(
- impl => impl != null && CommandLineOptions.Clo.UserWantsToCheckRoutine(cce.NonNull(impl.Name)) && !impl.SkipVerification);
-
- // operate on a stable copy, in case it gets updated while we're running
- Implementation[] stablePrioritizedImpls = null;
- if (0 < CommandLineOptions.Clo.VerifySnapshots)
- {
- OtherDefinitionAxiomsCollector.Collect(program.Axioms);
- DependencyCollector.Collect(program);
- stablePrioritizedImpls = impls.OrderByDescending(
- impl => impl.Priority != 1 ? impl.Priority : Cache.VerificationPriority(impl)).ToArray();
- }
- else
- {
- stablePrioritizedImpls = impls.OrderByDescending(impl => impl.Priority).ToArray();
- }
-
- #endregion
-
- if (1 < CommandLineOptions.Clo.VerifySnapshots)
- {
- CachedVerificationResultInjector.Inject(program, stablePrioritizedImpls, requestId, programId, out stats.CachingActionCounts);
- }
-
- #region Verify each implementation
-
- var outputCollector = new OutputCollector(stablePrioritizedImpls);
- var outcome = PipelineOutcome.VerificationCompleted;
-
- try
- {
- var cts = new CancellationTokenSource();
- RequestIdToCancellationTokenSource.AddOrUpdate(requestId, cts, (k, ov) => cts);
-
- var tasks = new Task[stablePrioritizedImpls.Length];
- // We use this semaphore to limit the number of tasks that are currently executing.
- var semaphore = new SemaphoreSlim(CommandLineOptions.Clo.VcsCores);
-
- // Create a task per implementation.
- for (int i = 0; i < stablePrioritizedImpls.Length; i++)
- {
- var taskIndex = i;
- var id = stablePrioritizedImpls[taskIndex].Id;
-
- CancellationTokenSource old;
- if (ImplIdToCancellationTokenSource.TryGetValue(id, out old))
- {
- old.Cancel();
- }
- ImplIdToCancellationTokenSource.AddOrUpdate(id, cts, (k, ov) => cts);
-
- var t = new Task((dummy) =>
- {
- try
- {
- if (outcome == PipelineOutcome.FatalError)
- {
- return;
- }
- if (cts.Token.IsCancellationRequested)
- {
- cts.Token.ThrowIfCancellationRequested();
- }
- VerifyImplementation(program, stats, er, requestId, extractLoopMappingInfo, stablePrioritizedImpls, taskIndex, outputCollector, Checkers, programId);
- ImplIdToCancellationTokenSource.TryRemove(id, out old);
- }
- finally
- {
- semaphore.Release();
- }
- }, cts.Token, TaskCreationOptions.LongRunning);
- tasks[taskIndex] = t;
- }
-
- // Execute the tasks.
- int j = 0;
- for (; j < stablePrioritizedImpls.Length && outcome != PipelineOutcome.FatalError; j++)
- {
- try
- {
- semaphore.Wait(cts.Token);
- }
- catch (OperationCanceledException)
- {
- break;
- }
- tasks[j].Start(TaskScheduler.Default);
- }
-
- // Don't wait for tasks that haven't been started yet.
- tasks = tasks.Take(j).ToArray();
- Task.WaitAll(tasks);
- }
- catch (AggregateException ae)
- {
- ae.Handle(e =>
- {
- var pe = e as ProverException;
- if (pe != null)
- {
- printer.ErrorWriteLine(Console.Out, "Fatal Error: ProverException: {0}", e);
- outcome = PipelineOutcome.FatalError;
- return true;
- }
- var oce = e as OperationCanceledException;
- if (oce != null)
- {
- return true;
- }
- return false;
- });
- }
- finally
- {
- CleanupCheckers(requestId);
- }
-
- cce.NonNull(CommandLineOptions.Clo.TheProverFactory).Close();
-
- outputCollector.WriteMoreOutput();
-
- if (1 < CommandLineOptions.Clo.VerifySnapshots && programId != null)
- {
- program.FreezeTopLevelDeclarations();
- programCache.Set(programId, program, policy);
- }
-
- if (0 <= CommandLineOptions.Clo.VerifySnapshots && CommandLineOptions.Clo.TraceCachingForBenchmarking)
- {
- var end = DateTime.UtcNow;
- if (TimePerRequest.Count == 0)
- {
- FirstRequestStart = start;
- }
- TimePerRequest[requestId] = end.Subtract(start);
- StatisticsPerRequest[requestId] = stats;
-
- var printTimes = true;
-
- Console.Out.WriteLine(CachedVerificationResultInjector.Statistics.Output(printTimes));
-
- Console.Out.WriteLine("Statistics per request as CSV:");
- var actions = string.Join(", ", Enum.GetNames(typeof(VC.ConditionGeneration.CachingAction)));
- Console.Out.WriteLine("Request ID{0}, Error, E (C), Inconclusive, I (C), Out of Memory, OoM (C), Timeout, T (C), Verified, V (C), {1}", printTimes ? ", Time (ms)" : "", actions);
- foreach (var kv in TimePerRequest.OrderBy(kv => ExecutionEngine.AutoRequestId(kv.Key)))
- {
- var s = StatisticsPerRequest[kv.Key];
- var cacs = s.CachingActionCounts;
- var c = cacs != null ? ", " + cacs.Select(ac => string.Format("{0,3}", ac)).Concat(", ") : "";
- var t = printTimes ? string.Format(", {0,8:F0}", kv.Value.TotalMilliseconds) : "";
- Console.Out.WriteLine("{0,-19}{1}, {2,2}, {3,2}, {4,2}, {5,2}, {6,2}, {7,2}, {8,2}, {9,2}, {10,2}, {11,2}{12}", kv.Key, t, s.ErrorCount, s.CachedErrorCount, s.InconclusiveCount, s.CachedInconclusiveCount, s.OutOfMemoryCount, s.CachedOutOfMemoryCount, s.TimeoutCount, s.CachedTimeoutCount, s.VerifiedCount, s.CachedVerifiedCount, c);
- }
-
- if (printTimes)
- {
- Console.Out.WriteLine();
- Console.Out.WriteLine("Total time (ms) since first request: {0:F0}", end.Subtract(FirstRequestStart).TotalMilliseconds);
- }
- }
-
- #endregion
-
- if (SecureVCGen.outfile != null)
- SecureVCGen.outfile.Close();
-
- return outcome;
- }
-
- public static void CancelRequest(string requestId)
- {
- Contract.Requires(requestId != null);
-
- CancellationTokenSource cts;
- if (RequestIdToCancellationTokenSource.TryGetValue(requestId, out cts))
- {
- cts.Cancel();
-
- CleanupCheckers(requestId);
- }
- }
-
-
- private static void CleanupCheckers(string requestId)
- {
- if (requestId != null)
- {
- CancellationTokenSource old;
- RequestIdToCancellationTokenSource.TryRemove(requestId, out old);
- }
- lock (RequestIdToCancellationTokenSource)
- {
- if (RequestIdToCancellationTokenSource.IsEmpty)
- {
- lock (Checkers)
- {
- foreach (Checker checker in Checkers)
- {
- Contract.Assert(checker != null);
- checker.Close();
- }
- }
- }
- }
- }
-
-
- private static void VerifyImplementation(Program program, PipelineStatistics stats, ErrorReporterDelegate er, string requestId, Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo, Implementation[] stablePrioritizedImpls, int index, OutputCollector outputCollector, List<Checker> checkers, string programId)
- {
- Implementation impl = stablePrioritizedImpls[index];
- VerificationResult verificationResult = null;
- var output = new StringWriter();
-
- printer.Inform("", output); // newline
- printer.Inform(string.Format("Verifying {0} ...", impl.Name), output);
-
- int priority = 0;
- if (0 < CommandLineOptions.Clo.VerifySnapshots)
- {
- verificationResult = Cache.Lookup(impl, out priority);
- }
-
- var wasCached = false;
- if (verificationResult != null && priority == Priority.SKIP)
- {
- 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), output);
- wasCached = true;
- }
- else
- {
- #region Verify the implementation
-
- verificationResult = new VerificationResult(requestId, impl, programId);
-
- using (var vcgen = CreateVCGen(program, checkers))
- {
- vcgen.CachingActionCounts = stats.CachingActionCounts;
- verificationResult.ProofObligationCountBefore = vcgen.CumulativeAssertionCount;
- verificationResult.Start = DateTime.UtcNow;
-
- if (CommandLineOptions.Clo.XmlSink != null)
- {
- CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, verificationResult.Start);
- }
- try
- {
- if (CommandLineOptions.Clo.inferLeastForUnsat != null)
- {
- var svcgen = vcgen as VC.StratifiedVCGen;
- Contract.Assert(svcgen != null);
- var ss = new HashSet<string>();
- foreach (var c in program.Constants)
- {
- if (!c.Name.StartsWith(CommandLineOptions.Clo.inferLeastForUnsat)) continue;
- ss.Add(c.Name);
- }
- verificationResult.Outcome = svcgen.FindLeastToVerify(impl, ref ss);
- verificationResult.Errors = new List<Counterexample>();
- 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, output);
- if (er != null)
- {
- lock (er)
- {
- er(errorInfo);
- }
- }
- 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;
- }
-
- verificationResult.ProofObligationCountAfter = vcgen.CumulativeAssertionCount;
- verificationResult.End = DateTime.UtcNow;
- }
-
- #endregion
-
- #region Cache the verification result
-
- if (0 < CommandLineOptions.Clo.VerifySnapshots && !string.IsNullOrEmpty(impl.Checksum))
- {
- Cache.Insert(impl, verificationResult);
- }
-
- #endregion
- }
-
- #region Process the verification results and statistics
-
- ProcessOutcome(verificationResult.Outcome, verificationResult.Errors, TimeIndication(verificationResult), stats, output, impl.TimeLimit, er, verificationResult.ImplementationName, verificationResult.ImplementationToken, verificationResult.RequestId, wasCached);
-
- ProcessErrors(verificationResult.Errors, verificationResult.Outcome, output, er, impl);
-
- if (CommandLineOptions.Clo.XmlSink != null)
- {
- CommandLineOptions.Clo.XmlSink.WriteEndMethod(verificationResult.Outcome.ToString().ToLowerInvariant(), verificationResult.End, verificationResult.End - verificationResult.Start);
- }
-
- outputCollector.Add(index, output);
-
- outputCollector.WriteMoreOutput();
-
- if (verificationResult.Outcome == VCGen.Outcome.Errors || CommandLineOptions.Clo.Trace)
- {
- Console.Out.Flush();
- }
-
- #endregion
- }
-
-
- class OutputCollector
- {
- StringWriter[] outputs;
-
- int nextPrintableIndex = 0;
-
- public OutputCollector(Implementation[] implementations)
- {
- outputs = new StringWriter[implementations.Length];
- }
-
- public void WriteMoreOutput()
- {
- lock (outputs)
- {
- for (; nextPrintableIndex < outputs.Length && outputs[nextPrintableIndex] != null; nextPrintableIndex++)
- {
- Console.Write(outputs[nextPrintableIndex].ToString());
- outputs[nextPrintableIndex] = null;
- Console.Out.Flush();
- }
- }
- }
-
- public void Add(int index, StringWriter output)
- {
- Contract.Requires(0 <= index && index < outputs.Length);
- Contract.Requires(output != null);
-
- lock (this)
- {
- outputs[index] = output;
- }
- }
- }
-
-
- private static ConditionGeneration CreateVCGen(Program program, List<Checker> checkers)
- {
- ConditionGeneration vcgen = null;
- if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed)
- {
- vcgen = new DCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, checkers);
- }
- else if (CommandLineOptions.Clo.FixedPointEngine != null)
- {
- vcgen = new FixedpointVC(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, checkers);
- }
- else if (CommandLineOptions.Clo.StratifiedInlining > 0)
- {
- vcgen = new StratifiedVCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, checkers);
- }
- else if (CommandLineOptions.Clo.SecureVcGen != null)
- {
- vcgen = new SecureVCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, checkers);
- }
- else
- {
- vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, checkers);
- }
- return vcgen;
- }
-
-
- #region Houdini
-
- private static PipelineOutcome RunHoudini(Program program, PipelineStatistics stats, ErrorReporterDelegate er)
- {
- Contract.Requires(stats != null);
-
- if (CommandLineOptions.Clo.AbstractHoudini != null)
- {
- return RunAbstractHoudini(program, stats, er);
- }
-
- if (CommandLineOptions.Clo.StagedHoudini != null)
- {
- return RunStagedHoudini(program, stats, er);
- }
-
- Houdini.HoudiniSession.HoudiniStatistics houdiniStats = new Houdini.HoudiniSession.HoudiniStatistics();
- Houdini.Houdini houdini = new Houdini.Houdini(program, houdiniStats);
- Houdini.HoudiniOutcome outcome = houdini.PerformHoudiniInference();
- houdini.Close();
-
- 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 = " + houdiniStats.proverTime.ToString("F2"));
- Console.WriteLine("Unsat core prover time = " + houdiniStats.unsatCoreProverTime.ToString("F2"));
- Console.WriteLine("Number of prover queries = " + houdiniStats.numProverQueries);
- Console.WriteLine("Number of unsat core prover queries = " + houdiniStats.numUnsatCoreProverQueries);
- Console.WriteLine("Number of unsat core prunings = " + houdiniStats.numUnsatCorePrunings);
- }
-
- foreach (Houdini.VCGenOutcome x in outcome.implementationOutcomes.Values)
- {
- ProcessOutcome(x.outcome, x.errors, "", stats, Console.Out, CommandLineOptions.Clo.ProverKillTime, er);
- ProcessErrors(x.errors, x.outcome, Console.Out, er);
- }
-
- return PipelineOutcome.Done;
- }
-
- public static Program ProgramFromFile(string filename) {
- Program p = ParseBoogieProgram(new List<string> { filename }, false);
- System.Diagnostics.Debug.Assert(p != null);
- LinearTypeChecker linearTypeChecker;
- MoverTypeChecker moverTypeChecker;
- PipelineOutcome oc = ExecutionEngine.ResolveAndTypecheck(p, filename, out linearTypeChecker, out moverTypeChecker);
- System.Diagnostics.Debug.Assert(oc == PipelineOutcome.ResolvedAndTypeChecked);
- return p;
- }
-
- private static PipelineOutcome RunStagedHoudini(Program program, PipelineStatistics stats, ErrorReporterDelegate er)
- {
- Houdini.HoudiniSession.HoudiniStatistics houdiniStats = new Houdini.HoudiniSession.HoudiniStatistics();
- Houdini.StagedHoudini stagedHoudini = new Houdini.StagedHoudini(program, houdiniStats, ProgramFromFile);
- Houdini.HoudiniOutcome outcome = stagedHoudini.PerformStagedHoudiniInference();
-
- 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 = " + houdiniStats.proverTime.ToString("F2"));
- Console.WriteLine("Unsat core prover time = " + houdiniStats.unsatCoreProverTime.ToString("F2"));
- Console.WriteLine("Number of prover queries = " + houdiniStats.numProverQueries);
- Console.WriteLine("Number of unsat core prover queries = " + houdiniStats.numUnsatCoreProverQueries);
- Console.WriteLine("Number of unsat core prunings = " + houdiniStats.numUnsatCorePrunings);
- }
-
- foreach (Houdini.VCGenOutcome x in outcome.implementationOutcomes.Values)
- {
- ProcessOutcome(x.outcome, x.errors, "", stats, Console.Out, CommandLineOptions.Clo.ProverKillTime, er);
- ProcessErrors(x.errors, x.outcome, Console.Out, er);
- }
-
- return PipelineOutcome.Done;
-
- }
-
-
- private static PipelineOutcome RunAbstractHoudini(Program program, PipelineStatistics stats, ErrorReporterDelegate er)
- {
- Contract.Requires(stats != 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(program);
- 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, "", stats, Console.Out, CommandLineOptions.Clo.ProverKillTime, er);
- ProcessErrors(absout.errors, absout.outcome, Console.Out, er);
-
- //Houdini.PredicateAbs.Initialize(program);
- //var abs = new Houdini.AbstractHoudini(program);
- //abs.computeSummaries(new Houdini.PredicateAbs(program.TopLevelDeclarations.OfType<Implementation>().First().Name));
-
- return PipelineOutcome.Done;
- }
-
- #endregion
-
-
- private static string TimeIndication(VerificationResult verificationResult)
- {
- var result = "";
- if (CommandLineOptions.Clo.Trace)
- {
- result = string.Format(" [{0:F3} s, {1} proof obligation{2}] ", (verificationResult.End - verificationResult.Start).TotalSeconds, verificationResult.ProofObligationCount, verificationResult.ProofObligationCount == 1 ? "" : "s");
- }
- else if (CommandLineOptions.Clo.TraceProofObligations)
- {
- result = string.Format(" [{0} proof obligation{1}] ", verificationResult.ProofObligationCount, verificationResult.ProofObligationCount == 1 ? "" : "s");
- }
- return result;
- }
-
-
- private static void ProcessOutcome(VC.VCGen.Outcome outcome, List<Counterexample> errors, string timeIndication,
- PipelineStatistics stats, TextWriter tw, int timeLimit, ErrorReporterDelegate er = null, string implName = null, IToken implTok = null, string requestId = null, bool wasCached = false)
- {
- Contract.Requires(stats != null);
-
- UpdateStatistics(stats, outcome, errors, wasCached);
-
- printer.Inform(timeIndication + OutcomeIndication(outcome, errors), tw);
-
- ReportOutcome(outcome, er, implName, implTok, requestId, tw, timeLimit);
- }
-
-
- private static void ReportOutcome(VC.VCGen.Outcome outcome, ErrorReporterDelegate er, string implName, IToken implTok, string requestId, TextWriter tw, int timeLimit)
- {
- ErrorInformation errorInfo = null;
-
- switch (outcome)
- {
- case VCGen.Outcome.ReachedBound:
- tw.WriteLine(string.Format("Stratified Inlining: Reached recursion bound of {0}", CommandLineOptions.Clo.RecursionBound));
- break;
- case VCGen.Outcome.TimedOut:
- if (implName != null && implTok != null)
- {
- errorInfo = errorInformationFactory.CreateErrorInformation(implTok, string.Format("Verification timed out after {0} seconds ({1})", timeLimit, implName), requestId);
- }
- break;
- case VCGen.Outcome.OutOfMemory:
- if (implName != null && implTok != null)
- {
- errorInfo = errorInformationFactory.CreateErrorInformation(implTok, "Verification out of memory (" + implName + ")", requestId);
- }
- break;
- case VCGen.Outcome.Inconclusive:
- if (implName != null && implTok != null)
- {
- errorInfo = errorInformationFactory.CreateErrorInformation(implTok, "Verification inconclusive (" + implName + ")", requestId);
- }
- break;
- }
-
- if (errorInfo != null)
- {
- errorInfo.ImplementationName = implName;
- if (er != null)
- {
- lock (er)
- {
- er(errorInfo);
- }
- }
- }
- }
-
-
- private static string OutcomeIndication(VC.VCGen.Outcome outcome, List<Counterexample> errors)
- {
- string traceOutput = "";
- switch (outcome)
- {
- default:
- Contract.Assert(false); // unexpected outcome
- throw new cce.UnreachableException();
- case VCGen.Outcome.ReachedBound:
- traceOutput = "verified";
- break;
- case VCGen.Outcome.Correct:
- traceOutput = (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed ? "credible" : "verified");
- break;
- case VCGen.Outcome.TimedOut:
- traceOutput = "timed out";
- break;
- case VCGen.Outcome.OutOfMemory:
- traceOutput = "out of memory";
- break;
- case VCGen.Outcome.Inconclusive:
- traceOutput = "inconclusive";
- break;
- case VCGen.Outcome.Errors:
- Contract.Assert(errors != null);
- traceOutput = (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed ? "doomed" : string.Format("error{0}", errors.Count == 1 ? "" : "s"));
- break;
- }
- return traceOutput;
- }
-
-
- private static void UpdateStatistics(PipelineStatistics stats, VC.VCGen.Outcome outcome, List<Counterexample> errors, bool wasCached)
- {
- Contract.Requires(stats != null);
-
- switch (outcome)
- {
- default:
- Contract.Assert(false); // unexpected outcome
- throw new cce.UnreachableException();
- case VCGen.Outcome.ReachedBound:
- Interlocked.Increment(ref stats.VerifiedCount);
- if (wasCached) { Interlocked.Increment(ref stats.CachedVerifiedCount); }
- break;
- case VCGen.Outcome.Correct:
- Interlocked.Increment(ref stats.VerifiedCount);
- if (wasCached) { Interlocked.Increment(ref stats.CachedVerifiedCount); }
- break;
- case VCGen.Outcome.TimedOut:
- Interlocked.Increment(ref stats.TimeoutCount);
- if (wasCached) { Interlocked.Increment(ref stats.CachedTimeoutCount); }
- break;
- case VCGen.Outcome.OutOfMemory:
- Interlocked.Increment(ref stats.OutOfMemoryCount);
- if (wasCached) { Interlocked.Increment(ref stats.CachedOutOfMemoryCount); }
- break;
- case VCGen.Outcome.Inconclusive:
- Interlocked.Increment(ref stats.InconclusiveCount);
- if (wasCached) { Interlocked.Increment(ref stats.CachedInconclusiveCount); }
- break;
- case VCGen.Outcome.Errors:
- if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed)
- {
- Interlocked.Increment(ref stats.ErrorCount);
- if (wasCached) { Interlocked.Increment(ref stats.CachedErrorCount); }
- }
- else
- {
- Interlocked.Add(ref stats.ErrorCount, errors.Count);
- if (wasCached) { Interlocked.Add(ref stats.CachedErrorCount, errors.Count); }
- }
- break;
- }
- }
-
-
- private static void ProcessErrors(List<Counterexample> errors, VC.VCGen.Outcome outcome, TextWriter tw, ErrorReporterDelegate er, Implementation impl = null)
- {
- var implName = impl != null ? impl.Name : null;
-
- if (errors != null)
- {
- errors.Sort(new CounterexampleComparer());
- foreach (Counterexample error in errors)
- {
- var errorInfo = CreateErrorInformation(error, outcome);
- errorInfo.ImplementationName = implName;
-
- if (CommandLineOptions.Clo.XmlSink != null)
- {
- WriteErrorInformationToXmlSink(errorInfo, error.Trace);
- }
-
- if (CommandLineOptions.Clo.EnhancedErrorMessages == 1)
- {
- foreach (string info in error.relatedInformation)
- {
- Contract.Assert(info != null);
- errorInfo.Out.WriteLine(" " + info);
- }
- }
- if (CommandLineOptions.Clo.ErrorTrace > 0)
- {
- 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(errorInfo.Model);
- }
-
- printer.WriteErrorInformation(errorInfo, tw);
-
- if (er != null)
- {
- lock (er)
- {
- er(errorInfo);
- }
- }
- }
- }
- }
-
-
- private static ErrorInformation CreateErrorInformation(Counterexample error, VC.VCGen.Outcome outcome)
- {
- // BP1xxx: Parsing errors
- // BP2xxx: Name resolution errors
- // BP3xxx: Typechecking errors
- // BP4xxx: Abstract interpretation errors (Is there such a thing?)
- // BP5xxx: Verification errors
-
- ErrorInformation errorInfo;
- var cause = "Error";
- if (outcome == VCGen.Outcome.TimedOut)
- {
- cause = "Timed out on";
- }
- else if (outcome == VCGen.Outcome.OutOfMemory)
- {
- cause = "Out of memory on";
- }
-
- var callError = error as CallCounterexample;
- var returnError = error as ReturnCounterexample;
- var assertError = error as AssertCounterexample;
- if (callError != null)
- {
- errorInfo = errorInformationFactory.CreateErrorInformation(callError.FailingCall.tok, callError.FailingCall.ErrorData as string ?? "A precondition for this call might not hold.", callError.RequestId, callError.OriginalRequestId, cause);
- errorInfo.BoogieErrorCode = "BP5002";
- errorInfo.Kind = ErrorKind.Precondition;
- errorInfo.AddAuxInfo(callError.FailingRequires.tok, callError.FailingRequires.ErrorData as string ?? "This is the precondition that might not hold.", "Related location");
-
- if (!CommandLineOptions.Clo.ForceBplErrors && callError.FailingRequires.ErrorMessage != null)
- {
- errorInfo = errorInformationFactory.CreateErrorInformation(null, callError.FailingRequires.ErrorMessage, callError.RequestId, callError.OriginalRequestId, cause);
- }
- }
- else if (returnError != null)
- {
- errorInfo = errorInformationFactory.CreateErrorInformation(returnError.FailingReturn.tok, "A postcondition might not hold on this return path.", returnError.RequestId, returnError.OriginalRequestId, cause);
- errorInfo.BoogieErrorCode = "BP5003";
- errorInfo.Kind = ErrorKind.Postcondition;
- errorInfo.AddAuxInfo(returnError.FailingEnsures.tok, returnError.FailingEnsures.ErrorData as string ?? "This is the postcondition that might not hold.", "Related location");
-
- if (!CommandLineOptions.Clo.ForceBplErrors && returnError.FailingEnsures.ErrorMessage != null)
- {
- errorInfo = errorInformationFactory.CreateErrorInformation(null, returnError.FailingEnsures.ErrorMessage, returnError.RequestId, returnError.OriginalRequestId, cause);
- }
- }
- else // error is AssertCounterexample
- {
- if (assertError.FailingAssert is LoopInitAssertCmd)
- {
- errorInfo = errorInformationFactory.CreateErrorInformation(assertError.FailingAssert.tok, "This loop invariant might not hold on entry.", assertError.RequestId, assertError.OriginalRequestId, cause);
- errorInfo.BoogieErrorCode = "BP5004";
- errorInfo.Kind = ErrorKind.InvariantEntry;
- }
- else if (assertError.FailingAssert is LoopInvMaintainedAssertCmd)
- {
- errorInfo = errorInformationFactory.CreateErrorInformation(assertError.FailingAssert.tok, "This loop invariant might not be maintained by the loop.", assertError.RequestId, assertError.OriginalRequestId, cause);
- errorInfo.BoogieErrorCode = "BP5005";
- errorInfo.Kind = ErrorKind.InvariantMaintainance;
- }
- else
- {
- var msg = assertError.FailingAssert.ErrorData as string;
- var tok = assertError.FailingAssert.tok;
- if (!CommandLineOptions.Clo.ForceBplErrors && assertError.FailingAssert.ErrorMessage != null)
- {
- msg = assertError.FailingAssert.ErrorMessage;
- tok = null;
- if (cause == "Error")
- {
- cause = null;
- }
- }
- string bec = null;
- if (msg == null)
- {
- msg = "This assertion might not hold.";
- bec = "BP5001";
- }
-
- errorInfo = errorInformationFactory.CreateErrorInformation(tok, msg, assertError.RequestId, assertError.OriginalRequestId, cause);
- errorInfo.BoogieErrorCode = bec;
- errorInfo.Kind = ErrorKind.Assertion;
- }
- }
-
- return errorInfo;
- }
-
-
- private static void WriteErrorInformationToXmlSink(ErrorInformation errorInfo, List<Block> trace)
- {
- var msg = "assertion violation";
- switch (errorInfo.Kind)
- {
- case ErrorKind.Precondition:
- msg = "precondition violation";
- break;
-
- case ErrorKind.Postcondition:
- msg = "postcondition violation";
- break;
-
- case ErrorKind.InvariantEntry:
- msg = "loop invariant entry violation";
- break;
-
- case ErrorKind.InvariantMaintainance:
- msg = "loop invariant maintenance violation";
- break;
- }
-
- var relatedError = errorInfo.Aux.FirstOrDefault();
- CommandLineOptions.Clo.XmlSink.WriteError(msg, errorInfo.Tok, relatedError.Tok, trace);
- }
-
- }
-
-}
+using System;
+using System.Collections.Concurrent;
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+using System.IO;
+using System.Linq;
+using System.Text.RegularExpressions;
+using System.Threading;
+using System.Threading.Tasks;
+using VC;
+using BoogiePL = Microsoft.Boogie;
+using System.Diagnostics;
+using System.Runtime.Caching;
+
+namespace Microsoft.Boogie
+{
+
+ #region Output printing
+
+ public interface OutputPrinter
+ {
+ 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, TextWriter tw);
+ void WriteTrailer(PipelineStatistics stats);
+ 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(TextWriter tw, string s)
+ {
+ Contract.Requires(s != null);
+ if (!s.Contains("Error: ") && !s.Contains("Error BP"))
+ {
+ tw.WriteLine(s);
+ return;
+ }
+
+ // split the string up into its first line and the remaining lines
+ string remaining = null;
+ int i = s.IndexOf('\r');
+ if (0 <= i)
+ {
+ remaining = s.Substring(i + 1);
+ if (remaining.StartsWith("\n"))
+ {
+ remaining = remaining.Substring(1);
+ }
+ s = s.Substring(0, i);
+ }
+
+ ConsoleColor col = Console.ForegroundColor;
+ Console.ForegroundColor = ConsoleColor.Red;
+ tw.WriteLine(s);
+ Console.ForegroundColor = col;
+
+ if (remaining != null)
+ {
+ tw.WriteLine(remaining);
+ }
+ }
+
+
+ public void ErrorWriteLine(TextWriter tw, string format, params object[] args)
+ {
+ Contract.Requires(format != null);
+ string s = string.Format(format, args);
+ ErrorWriteLine(tw, s);
+ }
+
+
+ public void AdvisoryWriteLine(string format, params object[] args)
+ {
+ Contract.Requires(format != null);
+ ConsoleColor col = Console.ForegroundColor;
+ Console.ForegroundColor = ConsoleColor.Yellow;
+ Console.WriteLine(format, args);
+ Console.ForegroundColor = col;
+ }
+
+
+ /// <summary>
+ /// Inform the user about something and proceed with translation normally.
+ /// Print newline after the message.
+ /// </summary>
+ public void Inform(string s, TextWriter tw)
+ {
+ if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.TraceProofObligations)
+ {
+ tw.WriteLine(s);
+ }
+ }
+
+
+ public void WriteTrailer(PipelineStatistics stats)
+ {
+ Contract.Requires(stats != null);
+ Contract.Requires(0 <= stats.VerifiedCount && 0 <= stats.ErrorCount && 0 <= stats.InconclusiveCount && 0 <= stats.TimeoutCount && 0 <= stats.OutOfMemoryCount);
+
+ Console.WriteLine();
+ if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed)
+ {
+ Console.Write("{0} finished with {1} credible, {2} doomed{3}", CommandLineOptions.Clo.DescriptiveToolName, stats.VerifiedCount, stats.ErrorCount, stats.ErrorCount == 1 ? "" : "s");
+ }
+ else
+ {
+ Console.Write("{0} finished with {1} verified, {2} error{3}", CommandLineOptions.Clo.DescriptiveToolName, stats.VerifiedCount, stats.ErrorCount, stats.ErrorCount == 1 ? "" : "s");
+ }
+ if (stats.InconclusiveCount != 0)
+ {
+ Console.Write(", {0} inconclusive{1}", stats.InconclusiveCount, stats.InconclusiveCount == 1 ? "" : "s");
+ }
+ if (stats.TimeoutCount != 0)
+ {
+ Console.Write(", {0} time out{1}", stats.TimeoutCount, stats.TimeoutCount == 1 ? "" : "s");
+ }
+ if (stats.OutOfMemoryCount != 0)
+ {
+ Console.Write(", {0} out of memory", stats.OutOfMemoryCount);
+ }
+ Console.WriteLine();
+ Console.Out.Flush();
+ }
+
+
+ public void WriteErrorInformation(ErrorInformation errorInfo, TextWriter tw, bool skipExecutionTrace = true)
+ {
+ Contract.Requires(errorInfo != null);
+
+ ReportBplError(errorInfo.Tok, errorInfo.FullMsg, true, tw);
+
+ foreach (var e in errorInfo.Aux)
+ {
+ if (!(skipExecutionTrace && e.Category != null && e.Category.Contains("Execution trace")))
+ {
+ ReportBplError(e.Tok, e.FullMsg, false, tw);
+ }
+ }
+
+ tw.Write(errorInfo.Out.ToString());
+ tw.Write(errorInfo.Model.ToString());
+ tw.Flush();
+ }
+
+
+ public virtual void ReportBplError(IToken tok, string message, bool error, TextWriter tw, string category = null)
+ {
+ Contract.Requires(message != null);
+
+ if (category != null) {
+ message = string.Format("{0}: {1}", category, message);
+ }
+ string s;
+ if (tok != null) {
+ s = string.Format("{0}({1},{2}): {3}", ExecutionEngine.GetFileNameForConsole(tok.filename), tok.line, tok.col, message);
+ } else {
+ s = message;
+ }
+ if (error) {
+ ErrorWriteLine(tw, s);
+ } else {
+ tw.WriteLine(s);
+ }
+ }
+ }
+
+ #endregion
+
+
+ public enum PipelineOutcome
+ {
+ Done,
+ ResolutionError,
+ TypeCheckingError,
+ ResolvedAndTypeChecked,
+ FatalError,
+ VerificationCompleted
+ }
+
+
+ public class PipelineStatistics
+ {
+ public int ErrorCount;
+ public int VerifiedCount;
+ public int InconclusiveCount;
+ public int TimeoutCount;
+ public int OutOfMemoryCount;
+ public long[] CachingActionCounts;
+ public int CachedErrorCount;
+ public int CachedVerifiedCount;
+ public int CachedInconclusiveCount;
+ public int CachedTimeoutCount;
+ public int CachedOutOfMemoryCount;
+ }
+
+
+ #region Error reporting
+
+ public delegate void ErrorReporterDelegate(ErrorInformation errInfo);
+
+
+ public enum ErrorKind
+ {
+ Assertion,
+ Precondition,
+ Postcondition,
+ InvariantEntry,
+ InvariantMaintainance
+ }
+
+
+ public class ErrorInformationFactory
+ {
+ public virtual ErrorInformation CreateErrorInformation(IToken tok, string msg, string requestId = null, string originalRequestId = null, string category = null)
+ {
+ Contract.Requires(1 <= tok.line && 1 <= tok.col);
+ Contract.Requires(msg != null);
+
+ return ErrorInformation.CreateErrorInformation(tok, msg, requestId, originalRequestId, category);
+ }
+ }
+
+
+ public class ErrorInformation
+ {
+ public readonly IToken Tok;
+ public string Msg;
+ public string Category { get; set; }
+ public string BoogieErrorCode { get; set; }
+ public readonly List<AuxErrorInfo> Aux = new List<AuxErrorInfo>();
+ public string OriginalRequestId { get; set; }
+ public string RequestId { get; set; }
+ public ErrorKind Kind { get; set; }
+ public string ImplementationName { get; set; }
+ public TextWriter Out = new StringWriter();
+ public TextWriter Model = new StringWriter();
+
+ public string FullMsg
+ {
+ get
+ {
+ var prefix = Category;
+ if (BoogieErrorCode != null)
+ {
+ prefix = prefix == null ? BoogieErrorCode : prefix + " " + BoogieErrorCode;
+ }
+ return prefix != null ? string.Format("{0}: {1}", prefix, Msg) : Msg;
+ }
+ }
+
+ public struct AuxErrorInfo
+ {
+ public readonly IToken Tok;
+ public readonly string Msg;
+ public readonly string Category;
+
+ public string FullMsg
+ {
+ get
+ {
+ return Category != null ? string.Format("{0}: {1}", Category, Msg) : Msg;
+ }
+ }
+
+ public AuxErrorInfo(IToken tok, string msg, string category = null)
+ {
+ Tok = tok;
+ Msg = CleanUp(msg);
+ Category = category;
+ }
+ }
+
+ protected ErrorInformation(IToken tok, string msg)
+ {
+ Contract.Requires(tok != null);
+ Contract.Requires(1 <= tok.line && 1 <= tok.col);
+ Contract.Requires(msg != null);
+
+ Tok = tok;
+ Msg = CleanUp(msg);
+ }
+
+ internal static ErrorInformation CreateErrorInformation(IToken tok, string msg, string requestId = null, string originalRequestId = null, string category = null)
+ {
+ var result = new ErrorInformation(tok, msg);
+ result.RequestId = requestId;
+ result.OriginalRequestId = originalRequestId;
+ result.Category = category;
+ return result;
+ }
+
+ public virtual void AddAuxInfo(IToken tok, string msg, string category = null)
+ {
+ Contract.Requires(tok != null);
+ Contract.Requires(1 <= tok.line && 1 <= tok.col);
+ Contract.Requires(msg != null);
+ Aux.Add(new AuxErrorInfo(tok, msg, category));
+ }
+
+ protected static string CleanUp(string msg)
+ {
+ if (msg.ToLower().StartsWith("error: "))
+ {
+ return msg.Substring(7);
+ }
+ else
+ {
+ return msg;
+ }
+ }
+ }
+
+ #endregion
+
+
+ public sealed class VerificationResult
+ {
+ public readonly string RequestId;
+ public readonly string Checksum;
+ public readonly string DependeciesChecksum;
+ public readonly string ImplementationName;
+ public readonly IToken ImplementationToken;
+ public readonly string ProgramId;
+
+ public DateTime Start { get; set; }
+ public DateTime End { get; set; }
+
+ public int ProofObligationCount { get { return ProofObligationCountAfter - ProofObligationCountBefore; } }
+ public int ProofObligationCountBefore { get; set; }
+ public int ProofObligationCountAfter { get; set; }
+
+ public ConditionGeneration.Outcome Outcome { get; set; }
+ public List<Counterexample> Errors;
+
+ public ISet<byte[]> AssertionChecksums { get; private set; }
+
+ public VerificationResult(string requestId, Implementation implementation, string programId = null)
+ {
+ Checksum = implementation.Checksum;
+ DependeciesChecksum = implementation.DependencyChecksum;
+ RequestId = requestId;
+ ImplementationName = implementation.Name;
+ ImplementationToken = implementation.tok;
+ ProgramId = programId;
+ AssertionChecksums = implementation.AssertionChecksums;
+ }
+ }
+
+
+ public class PolymorphismChecker : ReadOnlyVisitor
+ {
+ bool isMonomorphic = true;
+
+ public override DeclWithFormals VisitDeclWithFormals(DeclWithFormals node)
+ {
+ if (node.TypeParameters.Count > 0)
+ isMonomorphic = false;
+ return base.VisitDeclWithFormals(node);
+ }
+
+ public override BinderExpr VisitBinderExpr(BinderExpr node)
+ {
+ if (node.TypeParameters.Count > 0)
+ isMonomorphic = false;
+ return base.VisitBinderExpr(node);
+ }
+
+ public override MapType VisitMapType(MapType node)
+ {
+ if (node.TypeParameters.Count > 0)
+ isMonomorphic = false;
+ return base.VisitMapType(node);
+ }
+
+ public override Expr VisitNAryExpr(NAryExpr node)
+ {
+ BinaryOperator op = node.Fun as BinaryOperator;
+ if (op != null && op.Op == BinaryOperator.Opcode.Subtype)
+ isMonomorphic = false;
+ return base.VisitNAryExpr(node);
+ }
+
+ public static bool IsMonomorphic(Program program)
+ {
+ var checker = new PolymorphismChecker();
+ checker.VisitProgram(program);
+ return checker.isMonomorphic;
+ }
+ }
+
+ public class ExecutionEngine
+ {
+ public static OutputPrinter printer;
+
+ public static ErrorInformationFactory errorInformationFactory = new ErrorInformationFactory();
+
+ static int autoRequestIdCount;
+
+ static readonly string AutoRequestIdPrefix = "auto_request_id_";
+
+ public static string FreshRequestId()
+ {
+ var id = Interlocked.Increment(ref autoRequestIdCount);
+ return AutoRequestIdPrefix + id;
+ }
+
+ public static int AutoRequestId(string id)
+ {
+ if (id.StartsWith(AutoRequestIdPrefix))
+ {
+ int result;
+ if (int.TryParse(id.Substring(AutoRequestIdPrefix.Length), out result))
+ {
+ return result;
+ }
+ }
+ return -1;
+ }
+
+ public readonly static VerificationResultCache Cache = new VerificationResultCache();
+
+ static readonly MemoryCache programCache = new MemoryCache("ProgramCache");
+ static readonly CacheItemPolicy policy = new CacheItemPolicy { SlidingExpiration = new TimeSpan(0, 10, 0), Priority = CacheItemPriority.Default };
+
+ public static Program CachedProgram(string programId)
+ {
+ var result = programCache.Get(programId) as Program;
+ return result;
+ }
+
+ static List<Checker> Checkers = new List<Checker>();
+
+ static DateTime FirstRequestStart;
+
+ static readonly ConcurrentDictionary<string, TimeSpan> TimePerRequest = new ConcurrentDictionary<string, TimeSpan>();
+ static readonly ConcurrentDictionary<string, PipelineStatistics> StatisticsPerRequest = new ConcurrentDictionary<string, PipelineStatistics>();
+
+ static readonly ConcurrentDictionary<string, CancellationTokenSource> ImplIdToCancellationTokenSource = new ConcurrentDictionary<string, CancellationTokenSource>();
+
+ static readonly ConcurrentDictionary<string, CancellationTokenSource> RequestIdToCancellationTokenSource = new ConcurrentDictionary<string, CancellationTokenSource>();
+
+ public static void ProcessFiles(List<string> fileNames, bool lookForSnapshots = true, string programId = null)
+ {
+ Contract.Requires(cce.NonNullElements(fileNames));
+
+ if (programId == null)
+ {
+ programId = "main_program_id";
+ }
+
+ if (CommandLineOptions.Clo.VerifySeparately && 1 < fileNames.Count)
+ {
+ foreach (var f in fileNames)
+ {
+ ProcessFiles(new List<string> { f }, lookForSnapshots, f);
+ }
+ return;
+ }
+
+ if (0 <= CommandLineOptions.Clo.VerifySnapshots && lookForSnapshots)
+ {
+ var snapshotsByVersion = LookForSnapshots(fileNames);
+ foreach (var s in snapshotsByVersion)
+ {
+ ProcessFiles(new List<string>(s), false, programId);
+ }
+ return;
+ }
+
+ using (XmlFileScope xf = new XmlFileScope(CommandLineOptions.Clo.XmlSink, fileNames[fileNames.Count - 1]))
+ {
+ Program program = ParseBoogieProgram(fileNames, false);
+ if (program == null)
+ return;
+ if (CommandLineOptions.Clo.PrintFile != null)
+ {
+ PrintBplFile(CommandLineOptions.Clo.PrintFile, program, false, true, CommandLineOptions.Clo.PrettyPrint);
+ }
+
+ LinearTypeChecker linearTypeChecker;
+ CivlTypeChecker civlTypeChecker;
+ PipelineOutcome oc = ResolveAndTypecheck(program, fileNames[fileNames.Count - 1], out linearTypeChecker, out civlTypeChecker);
+ if (oc != PipelineOutcome.ResolvedAndTypeChecked)
+ return;
+
+ if (CommandLineOptions.Clo.PrintCFGPrefix != null)
+ {
+ foreach (var impl in program.Implementations)
+ {
+ using (StreamWriter sw = new StreamWriter(CommandLineOptions.Clo.PrintCFGPrefix + "." + impl.Name + ".dot"))
+ {
+ sw.Write(program.ProcessLoops(impl).ToDot());
+ }
+ }
+ }
+
+ if (CommandLineOptions.Clo.StratifiedInlining == 0)
+ {
+ Concurrency.Transform(linearTypeChecker, civlTypeChecker);
+ (new LinearEraser()).VisitProgram(program);
+ if (CommandLineOptions.Clo.CivlDesugaredFile != null)
+ {
+ int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured;
+ CommandLineOptions.Clo.PrintUnstructured = 1;
+ PrintBplFile(CommandLineOptions.Clo.CivlDesugaredFile, program, false, false, CommandLineOptions.Clo.PrettyPrint);
+ CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured;
+ }
+ }
+
+ EliminateDeadVariables(program);
+
+ CoalesceBlocks(program);
+
+ Inline(program);
+
+ var stats = new PipelineStatistics();
+ oc = InferAndVerify(program, stats, 1 < CommandLineOptions.Clo.VerifySnapshots ? programId : null);
+ switch (oc)
+ {
+ case PipelineOutcome.Done:
+ case PipelineOutcome.VerificationCompleted:
+ printer.WriteTrailer(stats);
+ break;
+ default:
+ break;
+ }
+ }
+ }
+
+ public static IList<IList<string>> LookForSnapshots(IList<string> fileNames)
+ {
+ Contract.Requires(fileNames != null);
+
+ var result = new List<IList<string>>();
+ for (int version = 0; true; version++)
+ {
+ var nextSnapshot = new List<string>();
+ 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())
+ {
+ result.Add(nextSnapshot);
+ }
+ else
+ {
+ break;
+ }
+ }
+ return result;
+ }
+
+
+ public static void CoalesceBlocks(Program program)
+ {
+ if (CommandLineOptions.Clo.CoalesceBlocks)
+ {
+ if (CommandLineOptions.Clo.Trace)
+ Console.WriteLine("Coalescing blocks...");
+ Microsoft.Boogie.BlockCoalescer.CoalesceBlocks(program);
+ }
+ }
+
+
+ public static void CollectModSets(Program program)
+ {
+ if (CommandLineOptions.Clo.DoModSetAnalysis)
+ {
+ new ModSetCollector().DoModSetAnalysis(program);
+ }
+ }
+
+
+ public static void EliminateDeadVariables(Program program)
+ {
+ Microsoft.Boogie.UnusedVarEliminator.Eliminate(program);
+ }
+
+
+ public static void PrintBplFile(string filename, Program program, bool allowPrintDesugaring, bool setTokens = true, bool pretty = false)
+ {
+ 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>", Console.Out, setTokens, pretty) :
+ new TokenTextWriter(filename, setTokens, pretty))
+ {
+ 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;
+ }
+
+
+ /// <summary>
+ /// 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.
+ /// </summary>
+ public static Program ParseBoogieProgram(List<string> fileNames, bool suppressTraceOutput)
+ {
+ Contract.Requires(cce.NonNullElements(fileNames));
+
+ 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 " + GetFileNameForConsole(bplFileName));
+ }
+ }
+
+ Program programSnippet;
+ int errorCount;
+ try
+ {
+ var defines = new List<string>() { "FILE_" + fileId };
+ errorCount = Parser.Parse(bplFileName, defines, out programSnippet, CommandLineOptions.Clo.UseBaseNameForFileName);
+ if (programSnippet == null || errorCount != 0)
+ {
+ Console.WriteLine("{0} parse errors detected in {1}", errorCount, GetFileNameForConsole(bplFileName));
+ okay = false;
+ continue;
+ }
+ }
+ catch (IOException e)
+ {
+ printer.ErrorWriteLine(Console.Out, "Error opening file \"{0}\": {1}", GetFileNameForConsole(bplFileName), e.Message);
+ okay = false;
+ continue;
+ }
+ if (program == null)
+ {
+ program = programSnippet;
+ }
+ else if (programSnippet != null)
+ {
+ program.AddTopLevelDeclarations(programSnippet.TopLevelDeclarations);
+ }
+ }
+ if (!okay)
+ {
+ return null;
+ }
+ else if (program == null)
+ {
+ return new Program();
+ }
+ else
+ {
+ return program;
+ }
+ }
+
+ internal static string GetFileNameForConsole(string filename)
+ {
+ return (CommandLineOptions.Clo.UseBaseNameForFileName && !string.IsNullOrEmpty(filename) && filename != "<console>") ? System.IO.Path.GetFileName(filename) : filename;
+ }
+
+
+ /// <summary>
+ /// 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
+ /// </summary>
+ public static PipelineOutcome ResolveAndTypecheck(Program program, string bplFileName, out LinearTypeChecker linearTypeChecker, out CivlTypeChecker civlTypeChecker)
+ {
+ Contract.Requires(program != null);
+ Contract.Requires(bplFileName != null);
+
+ linearTypeChecker = null;
+ civlTypeChecker = 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, GetFileNameForConsole(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, GetFileNameForConsole(bplFileName));
+ return PipelineOutcome.TypeCheckingError;
+ }
+
+ if (PolymorphismChecker.IsMonomorphic(program))
+ {
+ CommandLineOptions.Clo.TypeEncodingMethod = CommandLineOptions.TypeEncoding.Monomorphic;
+ }
+
+ CollectModSets(program);
+
+ civlTypeChecker = new CivlTypeChecker(program);
+ civlTypeChecker.TypeCheck();
+ if (civlTypeChecker.errorCount != 0)
+ {
+ Console.WriteLine("{0} type checking errors detected in {1}", civlTypeChecker.errorCount, GetFileNameForConsole(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, GetFileNameForConsole(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, true, CommandLineOptions.Clo.PrettyPrint);
+ }
+
+ return PipelineOutcome.ResolvedAndTypeChecked;
+ }
+
+
+ public static void Inline(Program program)
+ {
+ Contract.Requires(program != null);
+
+ if (CommandLineOptions.Clo.Trace)
+ Console.WriteLine("Inlining...");
+
+ // Inline
+ var TopLevelDeclarations = cce.NonNull(program.TopLevelDeclarations);
+
+ if (CommandLineOptions.Clo.ProcedureInlining != CommandLineOptions.Inlining.None)
+ {
+ bool inline = false;
+ foreach (var d in TopLevelDeclarations)
+ {
+ if ((d is Procedure || d is Implementation) && d.FindExprAttribute("inline") != null)
+ {
+ inline = true;
+ }
+ }
+ if (inline)
+ {
+ foreach (var impl in TopLevelDeclarations.OfType<Implementation>())
+ {
+ impl.OriginalBlocks = impl.Blocks;
+ impl.OriginalLocVars = impl.LocVars;
+ }
+ foreach (var impl in TopLevelDeclarations.OfType<Implementation>())
+ {
+ if (CommandLineOptions.Clo.UserWantsToCheckRoutine(impl.Name) && !impl.SkipVerification)
+ {
+ Inliner.ProcessImplementation(program, impl);
+ }
+ }
+ foreach (var impl in TopLevelDeclarations.OfType<Implementation>())
+ {
+ impl.OriginalBlocks = null;
+ impl.OriginalLocVars = null;
+ }
+ }
+ }
+ }
+
+
+ /// <summary>
+ /// 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
+ /// </summary>
+ public static PipelineOutcome InferAndVerify(Program program,
+ PipelineStatistics stats,
+ string programId = null,
+ ErrorReporterDelegate er = null, string requestId = null)
+ {
+ Contract.Requires(program != null);
+ Contract.Requires(stats != null);
+ Contract.Ensures(0 <= Contract.ValueAtReturn(out stats.InconclusiveCount) && 0 <= Contract.ValueAtReturn(out stats.TimeoutCount));
+
+ if (requestId == null)
+ {
+ requestId = FreshRequestId();
+ }
+
+ var start = DateTime.UtcNow;
+
+ #region Do some pre-abstract-interpretation preprocessing on the program
+ // Doing lambda expansion before abstract interpretation means that the abstract interpreter
+ // never needs to see any lambda expressions. (On the other hand, if it were useful for it
+ // to see lambdas, then it would be better to more lambda expansion until after infererence.)
+ if (CommandLineOptions.Clo.ExpandLambdas) {
+ LambdaHelper.ExpandLambdas(program);
+ //PrintBplFile ("-", program, true);
+ }
+ #endregion
+
+ #region Infer invariants using 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);
+
+ #endregion
+
+ #region Do some post-abstract-interpretation preprocessing on the program (e.g., loop unrolling)
+
+ if (CommandLineOptions.Clo.LoopUnrollCount != -1)
+ {
+ program.UnrollLoops(CommandLineOptions.Clo.LoopUnrollCount, CommandLineOptions.Clo.SoundLoopUnrolling);
+ }
+
+ Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo = null;
+ if (CommandLineOptions.Clo.ExtractLoops)
+ {
+ extractLoopMappingInfo = program.ExtractLoops();
+ }
+
+ if (CommandLineOptions.Clo.PrintInstrumented)
+ {
+ program.Emit(new TokenTextWriter(Console.Out, CommandLineOptions.Clo.PrettyPrint));
+ }
+ #endregion
+
+ if (!CommandLineOptions.Clo.Verify)
+ {
+ return PipelineOutcome.Done;
+ }
+
+ #region Run Houdini and verify
+ if (CommandLineOptions.Clo.ContractInfer)
+ {
+ return RunHoudini(program, stats, er);
+ }
+ #endregion
+
+ #region Select and prioritize implementations that should be verified
+
+ var impls = program.Implementations.Where(
+ impl => impl != null && CommandLineOptions.Clo.UserWantsToCheckRoutine(cce.NonNull(impl.Name)) && !impl.SkipVerification);
+
+ // operate on a stable copy, in case it gets updated while we're running
+ Implementation[] stablePrioritizedImpls = null;
+ if (0 < CommandLineOptions.Clo.VerifySnapshots)
+ {
+ OtherDefinitionAxiomsCollector.Collect(program.Axioms);
+ DependencyCollector.Collect(program);
+ stablePrioritizedImpls = impls.OrderByDescending(
+ impl => impl.Priority != 1 ? impl.Priority : Cache.VerificationPriority(impl)).ToArray();
+ }
+ else
+ {
+ stablePrioritizedImpls = impls.OrderByDescending(impl => impl.Priority).ToArray();
+ }
+
+ #endregion
+
+ if (1 < CommandLineOptions.Clo.VerifySnapshots)
+ {
+ CachedVerificationResultInjector.Inject(program, stablePrioritizedImpls, requestId, programId, out stats.CachingActionCounts);
+ }
+
+ #region Verify each implementation
+
+ var outputCollector = new OutputCollector(stablePrioritizedImpls);
+ var outcome = PipelineOutcome.VerificationCompleted;
+
+ try
+ {
+ var cts = new CancellationTokenSource();
+ RequestIdToCancellationTokenSource.AddOrUpdate(requestId, cts, (k, ov) => cts);
+
+ var tasks = new Task[stablePrioritizedImpls.Length];
+ // We use this semaphore to limit the number of tasks that are currently executing.
+ var semaphore = new SemaphoreSlim(CommandLineOptions.Clo.VcsCores);
+
+ // Create a task per implementation.
+ for (int i = 0; i < stablePrioritizedImpls.Length; i++)
+ {
+ var taskIndex = i;
+ var id = stablePrioritizedImpls[taskIndex].Id;
+
+ CancellationTokenSource old;
+ if (ImplIdToCancellationTokenSource.TryGetValue(id, out old))
+ {
+ old.Cancel();
+ }
+ ImplIdToCancellationTokenSource.AddOrUpdate(id, cts, (k, ov) => cts);
+
+ var t = new Task((dummy) =>
+ {
+ try
+ {
+ if (outcome == PipelineOutcome.FatalError)
+ {
+ return;
+ }
+ if (cts.Token.IsCancellationRequested)
+ {
+ cts.Token.ThrowIfCancellationRequested();
+ }
+ VerifyImplementation(program, stats, er, requestId, extractLoopMappingInfo, stablePrioritizedImpls, taskIndex, outputCollector, Checkers, programId);
+ ImplIdToCancellationTokenSource.TryRemove(id, out old);
+ }
+ finally
+ {
+ semaphore.Release();
+ }
+ }, cts.Token, TaskCreationOptions.None);
+ tasks[taskIndex] = t;
+ }
+
+ // Execute the tasks.
+ int j = 0;
+ for (; j < stablePrioritizedImpls.Length && outcome != PipelineOutcome.FatalError; j++)
+ {
+ try
+ {
+ semaphore.Wait(cts.Token);
+ }
+ catch (OperationCanceledException)
+ {
+ break;
+ }
+ tasks[j].Start(TaskScheduler.Default);
+ }
+
+ // Don't wait for tasks that haven't been started yet.
+ tasks = tasks.Take(j).ToArray();
+ Task.WaitAll(tasks);
+ }
+ catch (AggregateException ae)
+ {
+ ae.Handle(e =>
+ {
+ var pe = e as ProverException;
+ if (pe != null)
+ {
+ printer.ErrorWriteLine(Console.Out, "Fatal Error: ProverException: {0}", e);
+ outcome = PipelineOutcome.FatalError;
+ return true;
+ }
+ var oce = e as OperationCanceledException;
+ if (oce != null)
+ {
+ return true;
+ }
+ return false;
+ });
+ }
+ finally
+ {
+ CleanupCheckers(requestId);
+ }
+
+ if (CommandLineOptions.Clo.PrintNecessaryAssumes && program.NecessaryAssumes.Any())
+ {
+ Console.WriteLine("Necessary assume command(s): {0}", string.Join(", ", program.NecessaryAssumes));
+ }
+
+ cce.NonNull(CommandLineOptions.Clo.TheProverFactory).Close();
+
+ outputCollector.WriteMoreOutput();
+
+ if (1 < CommandLineOptions.Clo.VerifySnapshots && programId != null)
+ {
+ program.FreezeTopLevelDeclarations();
+ programCache.Set(programId, program, policy);
+ }
+
+ if (0 <= CommandLineOptions.Clo.VerifySnapshots && CommandLineOptions.Clo.TraceCachingForBenchmarking)
+ {
+ var end = DateTime.UtcNow;
+ if (TimePerRequest.Count == 0)
+ {
+ FirstRequestStart = start;
+ }
+ TimePerRequest[requestId] = end.Subtract(start);
+ StatisticsPerRequest[requestId] = stats;
+
+ var printTimes = true;
+
+ Console.Out.WriteLine(CachedVerificationResultInjector.Statistics.Output(printTimes));
+
+ Console.Out.WriteLine("Statistics per request as CSV:");
+ var actions = string.Join(", ", Enum.GetNames(typeof(VC.ConditionGeneration.CachingAction)));
+ Console.Out.WriteLine("Request ID{0}, Error, E (C), Inconclusive, I (C), Out of Memory, OoM (C), Timeout, T (C), Verified, V (C), {1}", printTimes ? ", Time (ms)" : "", actions);
+ foreach (var kv in TimePerRequest.OrderBy(kv => ExecutionEngine.AutoRequestId(kv.Key)))
+ {
+ var s = StatisticsPerRequest[kv.Key];
+ var cacs = s.CachingActionCounts;
+ var c = cacs != null ? ", " + cacs.Select(ac => string.Format("{0,3}", ac)).Concat(", ") : "";
+ var t = printTimes ? string.Format(", {0,8:F0}", kv.Value.TotalMilliseconds) : "";
+ Console.Out.WriteLine("{0,-19}{1}, {2,2}, {3,2}, {4,2}, {5,2}, {6,2}, {7,2}, {8,2}, {9,2}, {10,2}, {11,2}{12}", kv.Key, t, s.ErrorCount, s.CachedErrorCount, s.InconclusiveCount, s.CachedInconclusiveCount, s.OutOfMemoryCount, s.CachedOutOfMemoryCount, s.TimeoutCount, s.CachedTimeoutCount, s.VerifiedCount, s.CachedVerifiedCount, c);
+ }
+
+ if (printTimes)
+ {
+ Console.Out.WriteLine();
+ Console.Out.WriteLine("Total time (ms) since first request: {0:F0}", end.Subtract(FirstRequestStart).TotalMilliseconds);
+ }
+ }
+
+ #endregion
+
+ if (SecureVCGen.outfile != null)
+ SecureVCGen.outfile.Close();
+
+ return outcome;
+ }
+
+ public static void CancelRequest(string requestId)
+ {
+ Contract.Requires(requestId != null);
+
+ CancellationTokenSource cts;
+ if (RequestIdToCancellationTokenSource.TryGetValue(requestId, out cts))
+ {
+ cts.Cancel();
+
+ CleanupCheckers(requestId);
+ }
+ }
+
+
+ private static void CleanupCheckers(string requestId)
+ {
+ if (requestId != null)
+ {
+ CancellationTokenSource old;
+ RequestIdToCancellationTokenSource.TryRemove(requestId, out old);
+ }
+ lock (RequestIdToCancellationTokenSource)
+ {
+ if (RequestIdToCancellationTokenSource.IsEmpty)
+ {
+ lock (Checkers)
+ {
+ foreach (Checker checker in Checkers)
+ {
+ Contract.Assert(checker != null);
+ checker.Close();
+ }
+ }
+ }
+ }
+ }
+
+
+ private static void VerifyImplementation(Program program, PipelineStatistics stats, ErrorReporterDelegate er, string requestId, Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo, Implementation[] stablePrioritizedImpls, int index, OutputCollector outputCollector, List<Checker> checkers, string programId)
+ {
+ Implementation impl = stablePrioritizedImpls[index];
+ VerificationResult verificationResult = null;
+ var output = new StringWriter();
+
+ printer.Inform("", output); // newline
+ printer.Inform(string.Format("Verifying {0} ...", impl.Name), output);
+
+ int priority = 0;
+ var wasCached = false;
+ if (0 < CommandLineOptions.Clo.VerifySnapshots) {
+ var cachedResults = Cache.Lookup(impl, out priority);
+ if (cachedResults != null && priority == Priority.SKIP) {
+ if (CommandLineOptions.Clo.XmlSink != null) {
+ CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, cachedResults.Start);
+ }
+
+ printer.Inform(string.Format("Retrieving cached verification result for implementation {0}...", impl.Name), output);
+ if (CommandLineOptions.Clo.VerifySnapshots < 3 || cachedResults.Outcome == ConditionGeneration.Outcome.Correct) {
+ verificationResult = cachedResults;
+ wasCached = true;
+ }
+ }
+ }
+
+ if (!wasCached)
+ {
+ #region Verify the implementation
+
+ verificationResult = new VerificationResult(requestId, impl, programId);
+
+ using (var vcgen = CreateVCGen(program, checkers))
+ {
+ vcgen.CachingActionCounts = stats.CachingActionCounts;
+ verificationResult.ProofObligationCountBefore = vcgen.CumulativeAssertionCount;
+ verificationResult.Start = DateTime.UtcNow;
+
+ if (CommandLineOptions.Clo.XmlSink != null)
+ {
+ CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, verificationResult.Start);
+ }
+ try
+ {
+ if (CommandLineOptions.Clo.inferLeastForUnsat != null)
+ {
+ var svcgen = vcgen as VC.StratifiedVCGen;
+ Contract.Assert(svcgen != null);
+ var ss = new HashSet<string>();
+ foreach (var c in program.Constants)
+ {
+ if (!c.Name.StartsWith(CommandLineOptions.Clo.inferLeastForUnsat)) continue;
+ ss.Add(c.Name);
+ }
+ verificationResult.Outcome = svcgen.FindLeastToVerify(impl, ref ss);
+ verificationResult.Errors = new List<Counterexample>();
+ 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, output);
+ if (er != null)
+ {
+ lock (er)
+ {
+ er(errorInfo);
+ }
+ }
+ 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;
+ }
+
+ verificationResult.ProofObligationCountAfter = vcgen.CumulativeAssertionCount;
+ verificationResult.End = DateTime.UtcNow;
+ }
+
+ #endregion
+
+ #region Cache the verification result
+
+ if (0 < CommandLineOptions.Clo.VerifySnapshots && !string.IsNullOrEmpty(impl.Checksum))
+ {
+ Cache.Insert(impl, verificationResult);
+ }
+
+ #endregion
+ }
+
+ #region Process the verification results and statistics
+
+ ProcessOutcome(verificationResult.Outcome, verificationResult.Errors, TimeIndication(verificationResult), stats, output, impl.TimeLimit, er, verificationResult.ImplementationName, verificationResult.ImplementationToken, verificationResult.RequestId, wasCached);
+
+ ProcessErrors(verificationResult.Errors, verificationResult.Outcome, output, er, impl);
+
+ if (CommandLineOptions.Clo.XmlSink != null)
+ {
+ CommandLineOptions.Clo.XmlSink.WriteEndMethod(verificationResult.Outcome.ToString().ToLowerInvariant(), verificationResult.End, verificationResult.End - verificationResult.Start);
+ }
+
+ outputCollector.Add(index, output);
+
+ outputCollector.WriteMoreOutput();
+
+ if (verificationResult.Outcome == VCGen.Outcome.Errors || CommandLineOptions.Clo.Trace)
+ {
+ Console.Out.Flush();
+ }
+
+ #endregion
+ }
+
+
+ class OutputCollector
+ {
+ StringWriter[] outputs;
+
+ int nextPrintableIndex = 0;
+
+ public OutputCollector(Implementation[] implementations)
+ {
+ outputs = new StringWriter[implementations.Length];
+ }
+
+ public void WriteMoreOutput()
+ {
+ lock (outputs)
+ {
+ for (; nextPrintableIndex < outputs.Length && outputs[nextPrintableIndex] != null; nextPrintableIndex++)
+ {
+ Console.Write(outputs[nextPrintableIndex].ToString());
+ outputs[nextPrintableIndex] = null;
+ Console.Out.Flush();
+ }
+ }
+ }
+
+ public void Add(int index, StringWriter output)
+ {
+ Contract.Requires(0 <= index && index < outputs.Length);
+ Contract.Requires(output != null);
+
+ lock (this)
+ {
+ outputs[index] = output;
+ }
+ }
+ }
+
+
+ private static ConditionGeneration CreateVCGen(Program program, List<Checker> checkers)
+ {
+ ConditionGeneration vcgen = null;
+ if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed)
+ {
+ vcgen = new DCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, checkers);
+ }
+ else if (CommandLineOptions.Clo.FixedPointEngine != null)
+ {
+ vcgen = new FixedpointVC(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, checkers);
+ }
+ else if (CommandLineOptions.Clo.StratifiedInlining > 0)
+ {
+ vcgen = new StratifiedVCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, checkers);
+ }
+ else if (CommandLineOptions.Clo.SecureVcGen != null)
+ {
+ vcgen = new SecureVCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, checkers);
+ }
+ else
+ {
+ vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, checkers);
+ }
+ return vcgen;
+ }
+
+
+ #region Houdini
+
+ private static PipelineOutcome RunHoudini(Program program, PipelineStatistics stats, ErrorReporterDelegate er)
+ {
+ Contract.Requires(stats != null);
+
+ if (CommandLineOptions.Clo.AbstractHoudini != null)
+ {
+ return RunAbstractHoudini(program, stats, er);
+ }
+
+ if (CommandLineOptions.Clo.StagedHoudini != null)
+ {
+ return RunStagedHoudini(program, stats, er);
+ }
+
+ Houdini.HoudiniSession.HoudiniStatistics houdiniStats = new Houdini.HoudiniSession.HoudiniStatistics();
+ Houdini.Houdini houdini = new Houdini.Houdini(program, houdiniStats);
+ Houdini.HoudiniOutcome outcome = houdini.PerformHoudiniInference();
+ houdini.Close();
+
+ 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 = " + houdiniStats.proverTime.ToString("F2"));
+ Console.WriteLine("Unsat core prover time = " + houdiniStats.unsatCoreProverTime.ToString("F2"));
+ Console.WriteLine("Number of prover queries = " + houdiniStats.numProverQueries);
+ Console.WriteLine("Number of unsat core prover queries = " + houdiniStats.numUnsatCoreProverQueries);
+ Console.WriteLine("Number of unsat core prunings = " + houdiniStats.numUnsatCorePrunings);
+ }
+
+ foreach (Houdini.VCGenOutcome x in outcome.implementationOutcomes.Values)
+ {
+ ProcessOutcome(x.outcome, x.errors, "", stats, Console.Out, CommandLineOptions.Clo.ProverKillTime, er);
+ ProcessErrors(x.errors, x.outcome, Console.Out, er);
+ }
+
+ return PipelineOutcome.Done;
+ }
+
+ public static Program ProgramFromFile(string filename) {
+ Program p = ParseBoogieProgram(new List<string> { filename }, false);
+ System.Diagnostics.Debug.Assert(p != null);
+ LinearTypeChecker linearTypeChecker;
+ CivlTypeChecker civlTypeChecker;
+ PipelineOutcome oc = ExecutionEngine.ResolveAndTypecheck(p, filename, out linearTypeChecker, out civlTypeChecker);
+ System.Diagnostics.Debug.Assert(oc == PipelineOutcome.ResolvedAndTypeChecked);
+ return p;
+ }
+
+ private static PipelineOutcome RunStagedHoudini(Program program, PipelineStatistics stats, ErrorReporterDelegate er)
+ {
+ Houdini.HoudiniSession.HoudiniStatistics houdiniStats = new Houdini.HoudiniSession.HoudiniStatistics();
+ Houdini.StagedHoudini stagedHoudini = new Houdini.StagedHoudini(program, houdiniStats, ProgramFromFile);
+ Houdini.HoudiniOutcome outcome = stagedHoudini.PerformStagedHoudiniInference();
+
+ 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 = " + houdiniStats.proverTime.ToString("F2"));
+ Console.WriteLine("Unsat core prover time = " + houdiniStats.unsatCoreProverTime.ToString("F2"));
+ Console.WriteLine("Number of prover queries = " + houdiniStats.numProverQueries);
+ Console.WriteLine("Number of unsat core prover queries = " + houdiniStats.numUnsatCoreProverQueries);
+ Console.WriteLine("Number of unsat core prunings = " + houdiniStats.numUnsatCorePrunings);
+ }
+
+ foreach (Houdini.VCGenOutcome x in outcome.implementationOutcomes.Values)
+ {
+ ProcessOutcome(x.outcome, x.errors, "", stats, Console.Out, CommandLineOptions.Clo.ProverKillTime, er);
+ ProcessErrors(x.errors, x.outcome, Console.Out, er);
+ }
+
+ return PipelineOutcome.Done;
+
+ }
+
+
+ private static PipelineOutcome RunAbstractHoudini(Program program, PipelineStatistics stats, ErrorReporterDelegate er)
+ {
+ Contract.Requires(stats != 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(program);
+ 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, "", stats, Console.Out, CommandLineOptions.Clo.ProverKillTime, er);
+ ProcessErrors(absout.errors, absout.outcome, Console.Out, er);
+
+ //Houdini.PredicateAbs.Initialize(program);
+ //var abs = new Houdini.AbstractHoudini(program);
+ //abs.computeSummaries(new Houdini.PredicateAbs(program.TopLevelDeclarations.OfType<Implementation>().First().Name));
+
+ return PipelineOutcome.Done;
+ }
+
+ #endregion
+
+
+ private static string TimeIndication(VerificationResult verificationResult)
+ {
+ var result = "";
+ if (CommandLineOptions.Clo.Trace)
+ {
+ result = string.Format(" [{0:F3} s, {1} proof obligation{2}] ", (verificationResult.End - verificationResult.Start).TotalSeconds, verificationResult.ProofObligationCount, verificationResult.ProofObligationCount == 1 ? "" : "s");
+ }
+ else if (CommandLineOptions.Clo.TraceProofObligations)
+ {
+ result = string.Format(" [{0} proof obligation{1}] ", verificationResult.ProofObligationCount, verificationResult.ProofObligationCount == 1 ? "" : "s");
+ }
+ return result;
+ }
+
+
+ private static void ProcessOutcome(VC.VCGen.Outcome outcome, List<Counterexample> errors, string timeIndication,
+ PipelineStatistics stats, TextWriter tw, int timeLimit, ErrorReporterDelegate er = null, string implName = null, IToken implTok = null, string requestId = null, bool wasCached = false)
+ {
+ Contract.Requires(stats != null);
+
+ UpdateStatistics(stats, outcome, errors, wasCached);
+
+ printer.Inform(timeIndication + OutcomeIndication(outcome, errors), tw);
+
+ ReportOutcome(outcome, er, implName, implTok, requestId, tw, timeLimit, errors);
+ }
+
+
+ private static void ReportOutcome(VC.VCGen.Outcome outcome, ErrorReporterDelegate er, string implName, IToken implTok, string requestId, TextWriter tw, int timeLimit, List<Counterexample> errors)
+ {
+ ErrorInformation errorInfo = null;
+
+ switch (outcome)
+ {
+ case VCGen.Outcome.ReachedBound:
+ tw.WriteLine(string.Format("Stratified Inlining: Reached recursion bound of {0}", CommandLineOptions.Clo.RecursionBound));
+ break;
+ case VCGen.Outcome.Errors:
+ case VCGen.Outcome.TimedOut:
+ if (implName != null && implTok != null)
+ {
+ if (outcome == ConditionGeneration.Outcome.TimedOut || (errors != null && errors.Any(e => e.IsAuxiliaryCexForDiagnosingTimeouts)))
+ {
+ errorInfo = errorInformationFactory.CreateErrorInformation(implTok, string.Format("Verification of '{1}' timed out after {0} seconds", timeLimit, implName), requestId);
+ }
+
+ // Report timed out assertions as auxiliary info.
+ if (errors != null)
+ {
+ var cmpr = new CounterexampleComparer();
+ var timedOutAssertions = errors.Where(e => e.IsAuxiliaryCexForDiagnosingTimeouts).Distinct(cmpr).ToList();
+ timedOutAssertions.Sort(cmpr);
+ if (0 < timedOutAssertions.Count)
+ {
+ errorInfo.Msg += string.Format(" with {0} check(s) that timed out individually", timedOutAssertions.Count);
+ }
+ foreach (Counterexample error in timedOutAssertions)
+ {
+ var callError = error as CallCounterexample;
+ var returnError = error as ReturnCounterexample;
+ var assertError = error as AssertCounterexample;
+ IToken tok = null;
+ string msg = null;
+ if (callError != null)
+ {
+ tok = callError.FailingCall.tok;
+ msg = callError.FailingCall.ErrorData as string ?? "A precondition for this call might not hold.";
+ }
+ else if (returnError != null)
+ {
+ tok = returnError.FailingReturn.tok;
+ msg = "A postcondition might not hold on this return path.";
+ }
+ else
+ {
+ tok = assertError.FailingAssert.tok;
+ if (assertError.FailingAssert is LoopInitAssertCmd)
+ {
+ msg = "This loop invariant might not hold on entry.";
+ }
+ else if (assertError.FailingAssert is LoopInvMaintainedAssertCmd)
+ {
+ msg = "This loop invariant might not be maintained by the loop.";
+ }
+ else
+ {
+ msg = assertError.FailingAssert.ErrorData as string;
+ if (!CommandLineOptions.Clo.ForceBplErrors && assertError.FailingAssert.ErrorMessage != null)
+ {
+ msg = assertError.FailingAssert.ErrorMessage;
+ }
+ if (msg == null)
+ {
+ msg = "This assertion might not hold.";
+ }
+ }
+ }
+ errorInfo.AddAuxInfo(tok, msg, "Unverified check due to timeout");
+ }
+ }
+ }
+ break;
+ case VCGen.Outcome.OutOfMemory:
+ if (implName != null && implTok != null)
+ {
+ errorInfo = errorInformationFactory.CreateErrorInformation(implTok, "Verification out of memory (" + implName + ")", requestId);
+ }
+ break;
+ case VCGen.Outcome.Inconclusive:
+ if (implName != null && implTok != null)
+ {
+ errorInfo = errorInformationFactory.CreateErrorInformation(implTok, "Verification inconclusive (" + implName + ")", requestId);
+ }
+ break;
+ }
+
+ if (errorInfo != null)
+ {
+ errorInfo.ImplementationName = implName;
+ if (er != null)
+ {
+ lock (er)
+ {
+ er(errorInfo);
+ }
+ }
+ else
+ {
+ printer.WriteErrorInformation(errorInfo, tw);
+ }
+ }
+ }
+
+
+ private static string OutcomeIndication(VC.VCGen.Outcome outcome, List<Counterexample> errors)
+ {
+ string traceOutput = "";
+ switch (outcome)
+ {
+ default:
+ Contract.Assert(false); // unexpected outcome
+ throw new cce.UnreachableException();
+ case VCGen.Outcome.ReachedBound:
+ traceOutput = "verified";
+ break;
+ case VCGen.Outcome.Correct:
+ traceOutput = (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed ? "credible" : "verified");
+ break;
+ case VCGen.Outcome.TimedOut:
+ traceOutput = "timed out";
+ break;
+ case VCGen.Outcome.OutOfMemory:
+ traceOutput = "out of memory";
+ break;
+ case VCGen.Outcome.Inconclusive:
+ traceOutput = "inconclusive";
+ break;
+ case VCGen.Outcome.Errors:
+ Contract.Assert(errors != null);
+ traceOutput = (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed ? "doomed" : string.Format("error{0}", errors.Count == 1 ? "" : "s"));
+ break;
+ }
+ return traceOutput;
+ }
+
+
+ private static void UpdateStatistics(PipelineStatistics stats, VC.VCGen.Outcome outcome, List<Counterexample> errors, bool wasCached)
+ {
+ Contract.Requires(stats != null);
+
+ switch (outcome)
+ {
+ default:
+ Contract.Assert(false); // unexpected outcome
+ throw new cce.UnreachableException();
+ case VCGen.Outcome.ReachedBound:
+ Interlocked.Increment(ref stats.VerifiedCount);
+ if (wasCached) { Interlocked.Increment(ref stats.CachedVerifiedCount); }
+ break;
+ case VCGen.Outcome.Correct:
+ Interlocked.Increment(ref stats.VerifiedCount);
+ if (wasCached) { Interlocked.Increment(ref stats.CachedVerifiedCount); }
+ break;
+ case VCGen.Outcome.TimedOut:
+ Interlocked.Increment(ref stats.TimeoutCount);
+ if (wasCached) { Interlocked.Increment(ref stats.CachedTimeoutCount); }
+ break;
+ case VCGen.Outcome.OutOfMemory:
+ Interlocked.Increment(ref stats.OutOfMemoryCount);
+ if (wasCached) { Interlocked.Increment(ref stats.CachedOutOfMemoryCount); }
+ break;
+ case VCGen.Outcome.Inconclusive:
+ Interlocked.Increment(ref stats.InconclusiveCount);
+ if (wasCached) { Interlocked.Increment(ref stats.CachedInconclusiveCount); }
+ break;
+ case VCGen.Outcome.Errors:
+ if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed)
+ {
+ Interlocked.Increment(ref stats.ErrorCount);
+ if (wasCached) { Interlocked.Increment(ref stats.CachedErrorCount); }
+ }
+ else
+ {
+ int cnt = errors.Where(e => !e.IsAuxiliaryCexForDiagnosingTimeouts).Count();
+ Interlocked.Add(ref stats.ErrorCount, cnt);
+ if (wasCached) { Interlocked.Add(ref stats.CachedErrorCount, cnt); }
+ }
+ break;
+ }
+ }
+
+
+ private static void ProcessErrors(List<Counterexample> errors, VC.VCGen.Outcome outcome, TextWriter tw, ErrorReporterDelegate er, Implementation impl = null)
+ {
+ var implName = impl != null ? impl.Name : null;
+
+ if (errors != null)
+ {
+ errors.Sort(new CounterexampleComparer());
+ foreach (Counterexample error in errors)
+ {
+ if (error.IsAuxiliaryCexForDiagnosingTimeouts)
+ {
+ continue;
+ }
+ var errorInfo = CreateErrorInformation(error, outcome);
+ errorInfo.ImplementationName = implName;
+
+ if (CommandLineOptions.Clo.XmlSink != null)
+ {
+ WriteErrorInformationToXmlSink(errorInfo, error.Trace);
+ }
+
+ if (CommandLineOptions.Clo.EnhancedErrorMessages == 1)
+ {
+ foreach (string info in error.relatedInformation)
+ {
+ Contract.Assert(info != null);
+ errorInfo.Out.WriteLine(" " + info);
+ }
+ }
+ if (CommandLineOptions.Clo.ErrorTrace > 0)
+ {
+ 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(errorInfo.Model);
+ }
+
+ printer.WriteErrorInformation(errorInfo, tw);
+
+ if (er != null)
+ {
+ lock (er)
+ {
+ er(errorInfo);
+ }
+ }
+ }
+ }
+ }
+
+
+ private static ErrorInformation CreateErrorInformation(Counterexample error, VC.VCGen.Outcome outcome)
+ {
+ // BP1xxx: Parsing errors
+ // BP2xxx: Name resolution errors
+ // BP3xxx: Typechecking errors
+ // BP4xxx: Abstract interpretation errors (Is there such a thing?)
+ // BP5xxx: Verification errors
+
+ ErrorInformation errorInfo;
+ var cause = "Error";
+ if (outcome == VCGen.Outcome.TimedOut)
+ {
+ cause = "Timed out on";
+ }
+ else if (outcome == VCGen.Outcome.OutOfMemory)
+ {
+ cause = "Out of memory on";
+ }
+
+ var callError = error as CallCounterexample;
+ var returnError = error as ReturnCounterexample;
+ var assertError = error as AssertCounterexample;
+ if (callError != null)
+ {
+ errorInfo = errorInformationFactory.CreateErrorInformation(callError.FailingCall.tok, callError.FailingCall.ErrorData as string ?? "A precondition for this call might not hold.", callError.RequestId, callError.OriginalRequestId, cause);
+ errorInfo.BoogieErrorCode = "BP5002";
+ errorInfo.Kind = ErrorKind.Precondition;
+ errorInfo.AddAuxInfo(callError.FailingRequires.tok, callError.FailingRequires.ErrorData as string ?? "This is the precondition that might not hold.", "Related location");
+
+ if (!CommandLineOptions.Clo.ForceBplErrors && callError.FailingRequires.ErrorMessage != null)
+ {
+ errorInfo = errorInformationFactory.CreateErrorInformation(null, callError.FailingRequires.ErrorMessage, callError.RequestId, callError.OriginalRequestId, cause);
+ }
+ }
+ else if (returnError != null)
+ {
+ errorInfo = errorInformationFactory.CreateErrorInformation(returnError.FailingReturn.tok, "A postcondition might not hold on this return path.", returnError.RequestId, returnError.OriginalRequestId, cause);
+ errorInfo.BoogieErrorCode = "BP5003";
+ errorInfo.Kind = ErrorKind.Postcondition;
+ errorInfo.AddAuxInfo(returnError.FailingEnsures.tok, returnError.FailingEnsures.ErrorData as string ?? "This is the postcondition that might not hold.", "Related location");
+
+ if (!CommandLineOptions.Clo.ForceBplErrors && returnError.FailingEnsures.ErrorMessage != null)
+ {
+ errorInfo = errorInformationFactory.CreateErrorInformation(null, returnError.FailingEnsures.ErrorMessage, returnError.RequestId, returnError.OriginalRequestId, cause);
+ }
+ }
+ else // error is AssertCounterexample
+ {
+ if (assertError.FailingAssert is LoopInitAssertCmd)
+ {
+ errorInfo = errorInformationFactory.CreateErrorInformation(assertError.FailingAssert.tok, "This loop invariant might not hold on entry.", assertError.RequestId, assertError.OriginalRequestId, cause);
+ errorInfo.BoogieErrorCode = "BP5004";
+ errorInfo.Kind = ErrorKind.InvariantEntry;
+ }
+ else if (assertError.FailingAssert is LoopInvMaintainedAssertCmd)
+ {
+ errorInfo = errorInformationFactory.CreateErrorInformation(assertError.FailingAssert.tok, "This loop invariant might not be maintained by the loop.", assertError.RequestId, assertError.OriginalRequestId, cause);
+ errorInfo.BoogieErrorCode = "BP5005";
+ errorInfo.Kind = ErrorKind.InvariantMaintainance;
+ }
+ else
+ {
+ var msg = assertError.FailingAssert.ErrorData as string;
+ var tok = assertError.FailingAssert.tok;
+ if (!CommandLineOptions.Clo.ForceBplErrors && assertError.FailingAssert.ErrorMessage != null)
+ {
+ msg = assertError.FailingAssert.ErrorMessage;
+ tok = null;
+ if (cause == "Error")
+ {
+ cause = null;
+ }
+ }
+ string bec = null;
+ if (msg == null)
+ {
+ msg = "This assertion might not hold.";
+ bec = "BP5001";
+ }
+
+ errorInfo = errorInformationFactory.CreateErrorInformation(tok, msg, assertError.RequestId, assertError.OriginalRequestId, cause);
+ errorInfo.BoogieErrorCode = bec;
+ errorInfo.Kind = ErrorKind.Assertion;
+ }
+ }
+
+ return errorInfo;
+ }
+
+
+ private static void WriteErrorInformationToXmlSink(ErrorInformation errorInfo, List<Block> trace)
+ {
+ var msg = "assertion violation";
+ switch (errorInfo.Kind)
+ {
+ case ErrorKind.Precondition:
+ msg = "precondition violation";
+ break;
+
+ case ErrorKind.Postcondition:
+ msg = "postcondition violation";
+ break;
+
+ case ErrorKind.InvariantEntry:
+ msg = "loop invariant entry violation";
+ break;
+
+ case ErrorKind.InvariantMaintainance:
+ msg = "loop invariant maintenance violation";
+ break;
+ }
+
+ var relatedError = errorInfo.Aux.FirstOrDefault();
+ CommandLineOptions.Clo.XmlSink.WriteError(msg, errorInfo.Tok, relatedError.Tok, trace);
+ }
+
+ }
+
+}
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 05:46:41 +0000