summaryrefslogtreecommitdiff
path: root/Source/ExecutionEngine
diff options
context:
space:
mode:
Diffstat (limited to 'Source/ExecutionEngine')
-rw-r--r--Source/ExecutionEngine/ExecutionEngine.cs3586
-rw-r--r--Source/ExecutionEngine/ExecutionEngine.csproj386
-rw-r--r--Source/ExecutionEngine/Properties/AssemblyInfo.cs72
-rw-r--r--Source/ExecutionEngine/VerificationResultCache.cs1332
4 files changed, 2747 insertions, 2629 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);
+ }
+
+ }
+
+}
diff --git a/Source/ExecutionEngine/ExecutionEngine.csproj b/Source/ExecutionEngine/ExecutionEngine.csproj
index 09393f09..b17b1139 100644
--- a/Source/ExecutionEngine/ExecutionEngine.csproj
+++ b/Source/ExecutionEngine/ExecutionEngine.csproj
@@ -1,194 +1,194 @@
-<?xml version="1.0" encoding="utf-8"?>
-<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
- <Import Project="$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props" Condition="Exists('$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props')" />
- <PropertyGroup>
- <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
- <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
- <ProjectGuid>{EAA5EB79-D475-4601-A59B-825C191CD25F}</ProjectGuid>
- <OutputType>Library</OutputType>
- <AppDesignerFolder>Properties</AppDesignerFolder>
- <RootNamespace>ExecutionEngine</RootNamespace>
- <AssemblyName>ExecutionEngine</AssemblyName>
- <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
- <FileAlignment>512</FileAlignment>
- <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'">
- </TargetFrameworkProfile>
- <SignAssembly>true</SignAssembly>
- <AssemblyOriginatorKeyFile>..\InterimKey.snk</AssemblyOriginatorKeyFile>
- <ProductVersion>12.0.0</ProductVersion>
- <SchemaVersion>2.0</SchemaVersion>
- <CodeContractsAssemblyMode>0</CodeContractsAssemblyMode>
- </PropertyGroup>
- <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
- <DebugSymbols>true</DebugSymbols>
- <DebugType>full</DebugType>
- <Optimize>false</Optimize>
- <OutputPath>..\..\Binaries\</OutputPath>
- <DefineConstants>DEBUG;TRACE</DefineConstants>
- <ErrorReport>prompt</ErrorReport>
- <WarningLevel>4</WarningLevel>
- <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>
- <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
- <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
- <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
- <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
- <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
- <CodeContractsNonNullObligations>True</CodeContractsNonNullObligations>
- <CodeContractsBoundsObligations>True</CodeContractsBoundsObligations>
- <CodeContractsArithmeticObligations>True</CodeContractsArithmeticObligations>
- <CodeContractsEnumObligations>True</CodeContractsEnumObligations>
- <CodeContractsRedundantAssumptions>True</CodeContractsRedundantAssumptions>
- <CodeContractsAssertsToContractsCheckBox>True</CodeContractsAssertsToContractsCheckBox>
- <CodeContractsRedundantTests>True</CodeContractsRedundantTests>
- <CodeContractsMissingPublicRequiresAsWarnings>True</CodeContractsMissingPublicRequiresAsWarnings>
- <CodeContractsMissingPublicEnsuresAsWarnings>False</CodeContractsMissingPublicEnsuresAsWarnings>
- <CodeContractsInferRequires>True</CodeContractsInferRequires>
- <CodeContractsInferEnsures>False</CodeContractsInferEnsures>
- <CodeContractsInferEnsuresAutoProperties>True</CodeContractsInferEnsuresAutoProperties>
- <CodeContractsInferObjectInvariants>False</CodeContractsInferObjectInvariants>
- <CodeContractsSuggestAssumptions>False</CodeContractsSuggestAssumptions>
- <CodeContractsSuggestAssumptionsForCallees>False</CodeContractsSuggestAssumptionsForCallees>
- <CodeContractsSuggestRequires>False</CodeContractsSuggestRequires>
- <CodeContractsNecessaryEnsures>True</CodeContractsNecessaryEnsures>
- <CodeContractsSuggestObjectInvariants>False</CodeContractsSuggestObjectInvariants>
- <CodeContractsSuggestReadonly>True</CodeContractsSuggestReadonly>
- <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
- <CodeContractsShowSquigglies>True</CodeContractsShowSquigglies>
- <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
- <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
- <CodeContractsCustomRewriterAssembly />
- <CodeContractsCustomRewriterClass />
- <CodeContractsLibPaths />
- <CodeContractsExtraRewriteOptions />
- <CodeContractsExtraAnalysisOptions />
- <CodeContractsSQLServerOption />
- <CodeContractsBaseLineFile />
- <CodeContractsCacheAnalysisResults>True</CodeContractsCacheAnalysisResults>
- <CodeContractsSkipAnalysisIfCannotConnectToCache>False</CodeContractsSkipAnalysisIfCannotConnectToCache>
- <CodeContractsFailBuildOnWarnings>False</CodeContractsFailBuildOnWarnings>
- <CodeContractsBeingOptimisticOnExternal>True</CodeContractsBeingOptimisticOnExternal>
- <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
- <CodeContractsReferenceAssembly>DoNotBuild</CodeContractsReferenceAssembly>
- <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
- </PropertyGroup>
- <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
- <DebugType>pdbonly</DebugType>
- <Optimize>true</Optimize>
- <OutputPath>..\..\Binaries\</OutputPath>
- <DefineConstants>TRACE</DefineConstants>
- <ErrorReport>prompt</ErrorReport>
- <WarningLevel>4</WarningLevel>
- <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>
- <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
- <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
- <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
- <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
- <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
- <CodeContractsNonNullObligations>True</CodeContractsNonNullObligations>
- <CodeContractsBoundsObligations>True</CodeContractsBoundsObligations>
- <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
- <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
- <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
- <CodeContractsMissingPublicRequiresAsWarnings>True</CodeContractsMissingPublicRequiresAsWarnings>
- <CodeContractsInferRequires>True</CodeContractsInferRequires>
- <CodeContractsInferEnsures>False</CodeContractsInferEnsures>
- <CodeContractsInferObjectInvariants>False</CodeContractsInferObjectInvariants>
- <CodeContractsSuggestAssumptions>False</CodeContractsSuggestAssumptions>
- <CodeContractsSuggestRequires>True</CodeContractsSuggestRequires>
- <CodeContractsSuggestObjectInvariants>False</CodeContractsSuggestObjectInvariants>
- <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
- <CodeContractsShowSquigglies>True</CodeContractsShowSquigglies>
- <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
- <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
- <CodeContractsCustomRewriterAssembly />
- <CodeContractsCustomRewriterClass />
- <CodeContractsLibPaths />
- <CodeContractsExtraRewriteOptions />
- <CodeContractsExtraAnalysisOptions />
- <CodeContractsSQLServerOption />
- <CodeContractsBaseLineFile />
- <CodeContractsCacheAnalysisResults>True</CodeContractsCacheAnalysisResults>
- <CodeContractsFailBuildOnWarnings>False</CodeContractsFailBuildOnWarnings>
- <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
- <CodeContractsReferenceAssembly>DoNotBuild</CodeContractsReferenceAssembly>
- <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
- </PropertyGroup>
- <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'QED|AnyCPU'">
- <DebugSymbols>true</DebugSymbols>
- <OutputPath>bin\QED\</OutputPath>
- <DefineConstants>TRACE;DEBUG;QED</DefineConstants>
- <DebugType>full</DebugType>
- <PlatformTarget>AnyCPU</PlatformTarget>
- <ErrorReport>prompt</ErrorReport>
- <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
- </PropertyGroup>
- <ItemGroup>
- <Reference Include="System" />
- <Reference Include="System.Core" />
- <Reference Include="System.Runtime.Caching" />
- <Reference Include="System.Xml.Linq" />
- </ItemGroup>
- <ItemGroup>
- <Compile Include="ExecutionEngine.cs" />
- <Compile Include="Properties\AssemblyInfo.cs" />
- <Compile Include="VerificationResultCache.cs" />
- </ItemGroup>
- <ItemGroup>
- <ProjectReference Include="..\AbsInt\AbsInt.csproj">
- <Project>{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}</Project>
- <Name>AbsInt</Name>
- </ProjectReference>
- <ProjectReference Include="..\Basetypes\Basetypes.csproj">
- <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>
- <Name>Basetypes</Name>
- </ProjectReference>
- <ProjectReference Include="..\CodeContractsExtender\CodeContractsExtender.csproj">
- <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project>
- <Name>CodeContractsExtender</Name>
- </ProjectReference>
- <ProjectReference Include="..\Concurrency\Concurrency.csproj">
- <Project>{d07b8e38-e172-47f4-ad02-0373014a46d3}</Project>
- <Name>Concurrency</Name>
- </ProjectReference>
- <ProjectReference Include="..\Core\Core.csproj">
- <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>
- <Name>Core</Name>
- </ProjectReference>
- <ProjectReference Include="..\Doomed\Doomed.csproj">
- <Project>{884386A3-58E9-40BB-A273-B24976775553}</Project>
- <Name>Doomed</Name>
- </ProjectReference>
- <ProjectReference Include="..\Graph\Graph.csproj">
- <Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project>
- <Name>Graph</Name>
- </ProjectReference>
- <ProjectReference Include="..\Houdini\Houdini.csproj">
- <Project>{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}</Project>
- <Name>Houdini</Name>
- </ProjectReference>
- <ProjectReference Include="..\Model\Model.csproj">
- <Project>{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}</Project>
- <Name>Model</Name>
- </ProjectReference>
- <ProjectReference Include="..\ParserHelper\ParserHelper.csproj">
- <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>
- <Name>ParserHelper</Name>
- </ProjectReference>
- <ProjectReference Include="..\Predication\Predication.csproj">
- <Project>{AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}</Project>
- <Name>Predication</Name>
- </ProjectReference>
- <ProjectReference Include="..\VCGeneration\VCGeneration.csproj">
- <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project>
- <Name>VCGeneration</Name>
- </ProjectReference>
- </ItemGroup>
- <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
- <!-- To modify your build process, add your task inside one of the targets below and uncomment it.
- Other similar extension points exist, see Microsoft.Common.targets.
- <Target Name="BeforeBuild">
- </Target>
- <Target Name="AfterBuild">
- </Target>
- -->
+<?xml version="1.0" encoding="utf-8"?>
+<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
+ <Import Project="$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props" Condition="Exists('$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props')" />
+ <PropertyGroup>
+ <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
+ <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
+ <ProjectGuid>{EAA5EB79-D475-4601-A59B-825C191CD25F}</ProjectGuid>
+ <OutputType>Library</OutputType>
+ <AppDesignerFolder>Properties</AppDesignerFolder>
+ <RootNamespace>ExecutionEngine</RootNamespace>
+ <AssemblyName>BoogieExecutionEngine</AssemblyName>
+ <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
+ <FileAlignment>512</FileAlignment>
+ <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'">
+ </TargetFrameworkProfile>
+ <SignAssembly>true</SignAssembly>
+ <AssemblyOriginatorKeyFile>..\InterimKey.snk</AssemblyOriginatorKeyFile>
+ <ProductVersion>12.0.0</ProductVersion>
+ <SchemaVersion>2.0</SchemaVersion>
+ <CodeContractsAssemblyMode>0</CodeContractsAssemblyMode>
+ </PropertyGroup>
+ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
+ <DebugSymbols>true</DebugSymbols>
+ <DebugType>full</DebugType>
+ <Optimize>false</Optimize>
+ <OutputPath>..\..\Binaries\</OutputPath>
+ <DefineConstants>DEBUG;TRACE</DefineConstants>
+ <ErrorReport>prompt</ErrorReport>
+ <WarningLevel>4</WarningLevel>
+ <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>
+ <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
+ <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
+ <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
+ <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
+ <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
+ <CodeContractsNonNullObligations>True</CodeContractsNonNullObligations>
+ <CodeContractsBoundsObligations>True</CodeContractsBoundsObligations>
+ <CodeContractsArithmeticObligations>True</CodeContractsArithmeticObligations>
+ <CodeContractsEnumObligations>True</CodeContractsEnumObligations>
+ <CodeContractsRedundantAssumptions>True</CodeContractsRedundantAssumptions>
+ <CodeContractsAssertsToContractsCheckBox>True</CodeContractsAssertsToContractsCheckBox>
+ <CodeContractsRedundantTests>True</CodeContractsRedundantTests>
+ <CodeContractsMissingPublicRequiresAsWarnings>True</CodeContractsMissingPublicRequiresAsWarnings>
+ <CodeContractsMissingPublicEnsuresAsWarnings>False</CodeContractsMissingPublicEnsuresAsWarnings>
+ <CodeContractsInferRequires>True</CodeContractsInferRequires>
+ <CodeContractsInferEnsures>False</CodeContractsInferEnsures>
+ <CodeContractsInferEnsuresAutoProperties>True</CodeContractsInferEnsuresAutoProperties>
+ <CodeContractsInferObjectInvariants>False</CodeContractsInferObjectInvariants>
+ <CodeContractsSuggestAssumptions>False</CodeContractsSuggestAssumptions>
+ <CodeContractsSuggestAssumptionsForCallees>False</CodeContractsSuggestAssumptionsForCallees>
+ <CodeContractsSuggestRequires>False</CodeContractsSuggestRequires>
+ <CodeContractsNecessaryEnsures>True</CodeContractsNecessaryEnsures>
+ <CodeContractsSuggestObjectInvariants>False</CodeContractsSuggestObjectInvariants>
+ <CodeContractsSuggestReadonly>True</CodeContractsSuggestReadonly>
+ <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
+ <CodeContractsShowSquigglies>True</CodeContractsShowSquigglies>
+ <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
+ <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
+ <CodeContractsCustomRewriterAssembly />
+ <CodeContractsCustomRewriterClass />
+ <CodeContractsLibPaths />
+ <CodeContractsExtraRewriteOptions />
+ <CodeContractsExtraAnalysisOptions />
+ <CodeContractsSQLServerOption />
+ <CodeContractsBaseLineFile />
+ <CodeContractsCacheAnalysisResults>True</CodeContractsCacheAnalysisResults>
+ <CodeContractsSkipAnalysisIfCannotConnectToCache>False</CodeContractsSkipAnalysisIfCannotConnectToCache>
+ <CodeContractsFailBuildOnWarnings>False</CodeContractsFailBuildOnWarnings>
+ <CodeContractsBeingOptimisticOnExternal>True</CodeContractsBeingOptimisticOnExternal>
+ <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
+ <CodeContractsReferenceAssembly>DoNotBuild</CodeContractsReferenceAssembly>
+ <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
+ </PropertyGroup>
+ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
+ <DebugType>pdbonly</DebugType>
+ <Optimize>true</Optimize>
+ <OutputPath>..\..\Binaries\</OutputPath>
+ <DefineConstants>TRACE</DefineConstants>
+ <ErrorReport>prompt</ErrorReport>
+ <WarningLevel>4</WarningLevel>
+ <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>
+ <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
+ <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
+ <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
+ <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
+ <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
+ <CodeContractsNonNullObligations>True</CodeContractsNonNullObligations>
+ <CodeContractsBoundsObligations>True</CodeContractsBoundsObligations>
+ <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
+ <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
+ <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
+ <CodeContractsMissingPublicRequiresAsWarnings>True</CodeContractsMissingPublicRequiresAsWarnings>
+ <CodeContractsInferRequires>True</CodeContractsInferRequires>
+ <CodeContractsInferEnsures>False</CodeContractsInferEnsures>
+ <CodeContractsInferObjectInvariants>False</CodeContractsInferObjectInvariants>
+ <CodeContractsSuggestAssumptions>False</CodeContractsSuggestAssumptions>
+ <CodeContractsSuggestRequires>True</CodeContractsSuggestRequires>
+ <CodeContractsSuggestObjectInvariants>False</CodeContractsSuggestObjectInvariants>
+ <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
+ <CodeContractsShowSquigglies>True</CodeContractsShowSquigglies>
+ <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
+ <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
+ <CodeContractsCustomRewriterAssembly />
+ <CodeContractsCustomRewriterClass />
+ <CodeContractsLibPaths />
+ <CodeContractsExtraRewriteOptions />
+ <CodeContractsExtraAnalysisOptions />
+ <CodeContractsSQLServerOption />
+ <CodeContractsBaseLineFile />
+ <CodeContractsCacheAnalysisResults>True</CodeContractsCacheAnalysisResults>
+ <CodeContractsFailBuildOnWarnings>False</CodeContractsFailBuildOnWarnings>
+ <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
+ <CodeContractsReferenceAssembly>DoNotBuild</CodeContractsReferenceAssembly>
+ <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
+ </PropertyGroup>
+ <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'QED|AnyCPU'">
+ <DebugSymbols>true</DebugSymbols>
+ <OutputPath>bin\QED\</OutputPath>
+ <DefineConstants>TRACE;DEBUG;QED</DefineConstants>
+ <DebugType>full</DebugType>
+ <PlatformTarget>AnyCPU</PlatformTarget>
+ <ErrorReport>prompt</ErrorReport>
+ <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
+ </PropertyGroup>
+ <ItemGroup>
+ <Reference Include="System" />
+ <Reference Include="System.Core" />
+ <Reference Include="System.Runtime.Caching" />
+ <Reference Include="System.Xml.Linq" />
+ </ItemGroup>
+ <ItemGroup>
+ <Compile Include="ExecutionEngine.cs" />
+ <Compile Include="Properties\AssemblyInfo.cs" />
+ <Compile Include="VerificationResultCache.cs" />
+ </ItemGroup>
+ <ItemGroup>
+ <ProjectReference Include="..\AbsInt\AbsInt.csproj">
+ <Project>{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}</Project>
+ <Name>AbsInt</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\Basetypes\Basetypes.csproj">
+ <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>
+ <Name>Basetypes</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\CodeContractsExtender\CodeContractsExtender.csproj">
+ <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project>
+ <Name>CodeContractsExtender</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\Concurrency\Concurrency.csproj">
+ <Project>{d07b8e38-e172-47f4-ad02-0373014a46d3}</Project>
+ <Name>Concurrency</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\Core\Core.csproj">
+ <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>
+ <Name>Core</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\Doomed\Doomed.csproj">
+ <Project>{884386A3-58E9-40BB-A273-B24976775553}</Project>
+ <Name>Doomed</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\Graph\Graph.csproj">
+ <Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project>
+ <Name>Graph</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\Houdini\Houdini.csproj">
+ <Project>{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}</Project>
+ <Name>Houdini</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\Model\Model.csproj">
+ <Project>{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}</Project>
+ <Name>Model</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\ParserHelper\ParserHelper.csproj">
+ <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>
+ <Name>ParserHelper</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\Predication\Predication.csproj">
+ <Project>{AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}</Project>
+ <Name>Predication</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\VCGeneration\VCGeneration.csproj">
+ <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project>
+ <Name>VCGeneration</Name>
+ </ProjectReference>
+ </ItemGroup>
+ <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
+ <!-- To modify your build process, add your task inside one of the targets below and uncomment it.
+ Other similar extension points exist, see Microsoft.Common.targets.
+ <Target Name="BeforeBuild">
+ </Target>
+ <Target Name="AfterBuild">
+ </Target>
+ -->
</Project> \ No newline at end of file
diff --git a/Source/ExecutionEngine/Properties/AssemblyInfo.cs b/Source/ExecutionEngine/Properties/AssemblyInfo.cs
index 5977e799..ea288b03 100644
--- a/Source/ExecutionEngine/Properties/AssemblyInfo.cs
+++ b/Source/ExecutionEngine/Properties/AssemblyInfo.cs
@@ -1,36 +1,36 @@
-using System.Reflection;
-using System.Runtime.CompilerServices;
-using System.Runtime.InteropServices;
-
-// General Information about an assembly is controlled through the following
-// set of attributes. Change these attribute values to modify the information
-// associated with an assembly.
-[assembly: AssemblyTitle("ExecutionEngine")]
-[assembly: AssemblyDescription("")]
-[assembly: AssemblyConfiguration("")]
-[assembly: AssemblyCompany("")]
-[assembly: AssemblyProduct("ExecutionEngine")]
-[assembly: AssemblyCopyright("Copyright © 2013")]
-[assembly: AssemblyTrademark("")]
-[assembly: AssemblyCulture("")]
-
-// Setting ComVisible to false makes the types in this assembly not visible
-// to COM components. If you need to access a type in this assembly from
-// COM, set the ComVisible attribute to true on that type.
-[assembly: ComVisible(false)]
-
-// The following GUID is for the ID of the typelib if this project is exposed to COM
-[assembly: Guid("03fff764-c3f0-4e42-a897-a1c151b3fe6d")]
-
-// Version information for an assembly consists of the following four values:
-//
-// Major Version
-// Minor Version
-// Build Number
-// Revision
-//
-// You can specify all the values or you can default the Build and Revision Numbers
-// by using the '*' as shown below:
-// [assembly: AssemblyVersion("1.0.*")]
-[assembly: AssemblyVersion("1.0.0.0")]
-[assembly: AssemblyFileVersion("1.0.0.0")]
+using System.Reflection;
+using System.Runtime.CompilerServices;
+using System.Runtime.InteropServices;
+
+// General Information about an assembly is controlled through the following
+// set of attributes. Change these attribute values to modify the information
+// associated with an assembly.
+[assembly: AssemblyTitle("ExecutionEngine")]
+[assembly: AssemblyDescription("")]
+[assembly: AssemblyConfiguration("")]
+[assembly: AssemblyCompany("")]
+[assembly: AssemblyProduct("ExecutionEngine")]
+[assembly: AssemblyCopyright("Copyright © 2013")]
+[assembly: AssemblyTrademark("")]
+[assembly: AssemblyCulture("")]
+
+// Setting ComVisible to false makes the types in this assembly not visible
+// to COM components. If you need to access a type in this assembly from
+// COM, set the ComVisible attribute to true on that type.
+[assembly: ComVisible(false)]
+
+// The following GUID is for the ID of the typelib if this project is exposed to COM
+[assembly: Guid("03fff764-c3f0-4e42-a897-a1c151b3fe6d")]
+
+// Version information for an assembly consists of the following four values:
+//
+// Major Version
+// Minor Version
+// Build Number
+// Revision
+//
+// You can specify all the values or you can default the Build and Revision Numbers
+// by using the '*' as shown below:
+// [assembly: AssemblyVersion("1.0.*")]
+[assembly: AssemblyVersion("1.0.0.0")]
+[assembly: AssemblyFileVersion("1.0.0.0")]
diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index 5d20e6e8..3159238c 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -1,640 +1,692 @@
-using System;
-using System.Collections.Concurrent;
-using System.Collections.Generic;
-using System.Diagnostics.Contracts;
-using System.IO;
-using System.Linq;
-using System.Runtime.Caching;
-using System.Text;
-using System.Text.RegularExpressions;
-using VC;
-
-namespace Microsoft.Boogie
-{
-
- struct CachedVerificationResultInjectorRun
- {
- public DateTime Start { get; internal set; }
- public DateTime End { get; internal set; }
- public int TransformedImplementationCount { get; internal set; }
- public int ImplementationCount { get; internal set; }
- public int SkippedImplementationCount { get; set; }
- public int LowPriorityImplementationCount { get; set; }
- public int MediumPriorityImplementationCount { get; set; }
- public int HighPriorityImplementationCount { get; set; }
- public long[] CachingActionCounts { get; set; }
- }
-
-
- sealed class CachedVerificationResultInjectorStatistics
- {
- ConcurrentDictionary<string, CachedVerificationResultInjectorRun> runs = new ConcurrentDictionary<string, CachedVerificationResultInjectorRun>();
-
- public bool AddRun(string requestId, CachedVerificationResultInjectorRun run)
- {
- return runs.TryAdd(requestId, run);
- }
-
- public string Output(bool printTime = false)
- {
- var wr = new StringWriter();
- if (runs.Any())
- {
- wr.WriteLine("Cached verification result injector statistics as CSV:");
- wr.WriteLine("Request ID, Transformed, Low, Medium, High, Skipped{0}", printTime ? ", Time (ms)" : "");
- foreach (var kv in runs.OrderBy(kv => ExecutionEngine.AutoRequestId(kv.Key)))
- {
- var t = printTime ? string.Format(", {0,8:F0}", kv.Value.End.Subtract(kv.Value.Start).TotalMilliseconds) : "";
- wr.WriteLine("{0,-19}, {1,3}, {2,3}, {3,3}, {4,3}, {5,3}{6}", kv.Key, kv.Value.TransformedImplementationCount, kv.Value.LowPriorityImplementationCount, kv.Value.MediumPriorityImplementationCount, kv.Value.HighPriorityImplementationCount, kv.Value.SkippedImplementationCount, t);
- }
- }
- return wr.ToString();
- }
- }
-
-
- sealed class CachedVerificationResultInjector : StandardVisitor
- {
- readonly IEnumerable<Implementation> Implementations;
- readonly Program Program;
- // TODO(wuestholz): We should probably increase the threshold to something like 2 seconds.
- static readonly double TimeThreshold = -1.0d;
- Program programInCachedSnapshot;
- Implementation currentImplementation;
- int assumptionVariableCount;
- int temporaryVariableCount;
-
- public static readonly CachedVerificationResultInjectorStatistics Statistics = new CachedVerificationResultInjectorStatistics();
-
- int FreshAssumptionVariableName
- {
- get
- {
- return assumptionVariableCount++;
- }
- }
-
- int FreshTemporaryVariableName
- {
- get
- {
- return temporaryVariableCount++;
- }
- }
-
- CachedVerificationResultInjector(Program program, IEnumerable<Implementation> implementations)
- {
- Implementations = implementations;
- Program = program;
- }
-
- public Implementation Inject(Implementation implementation, Program programInCachedSnapshot)
- {
- Contract.Requires(implementation != null && programInCachedSnapshot != null);
-
- this.programInCachedSnapshot = programInCachedSnapshot;
- assumptionVariableCount = 0;
- temporaryVariableCount = 0;
- currentImplementation = implementation;
- var result = VisitImplementation(implementation);
- currentImplementation = null;
- this.programInCachedSnapshot = null;
- return result;
- }
-
- public static void Inject(Program program, IEnumerable<Implementation> implementations, string requestId, string programId, out long[] cachingActionCounts)
- {
- var eai = new CachedVerificationResultInjector(program, implementations);
-
- cachingActionCounts = new long[Enum.GetNames(typeof(VC.ConditionGeneration.CachingAction)).Length];
- var run = new CachedVerificationResultInjectorRun { Start = DateTime.UtcNow, ImplementationCount = implementations.Count(), CachingActionCounts = cachingActionCounts };
- foreach (var impl in implementations)
- {
- int priority;
- var vr = ExecutionEngine.Cache.Lookup(impl, out priority);
- if (vr != null && vr.ProgramId == programId)
- {
- if (priority == Priority.LOW)
- {
- run.LowPriorityImplementationCount++;
- if (TimeThreshold < vr.End.Subtract(vr.Start).TotalMilliseconds)
- {
- SetErrorAndAssertionChecksumsInCachedSnapshot(impl, vr);
- if (vr.ProgramId != null)
- {
- var p = ExecutionEngine.CachedProgram(vr.ProgramId);
- if (p != null)
- {
- eai.Inject(impl, p);
- run.TransformedImplementationCount++;
- }
- }
- }
- }
- else if (priority == Priority.MEDIUM)
- {
- run.MediumPriorityImplementationCount++;
- if (TimeThreshold < vr.End.Subtract(vr.Start).TotalMilliseconds)
- {
- SetErrorAndAssertionChecksumsInCachedSnapshot(impl, vr);
- if (vr.ProgramId != null)
- {
- var p = ExecutionEngine.CachedProgram(vr.ProgramId);
- if (p != null)
- {
- eai.Inject(impl, p);
- run.TransformedImplementationCount++;
- }
- }
- }
- }
- else if (priority == Priority.HIGH)
- {
- run.HighPriorityImplementationCount++;
- }
- else if (priority == Priority.SKIP)
- {
- run.SkippedImplementationCount++;
- }
- }
- }
- run.End = DateTime.UtcNow;
- Statistics.AddRun(requestId, run);
- }
-
- private static void SetErrorAndAssertionChecksumsInCachedSnapshot(Implementation implementation, VerificationResult result)
- {
- if (result.Outcome == ConditionGeneration.Outcome.Errors && result.Errors != null && result.Errors.Count < CommandLineOptions.Clo.ProverCCLimit)
- {
- implementation.SetErrorChecksumToCachedError(result.Errors.Select(cex => new Tuple<byte[], byte[], object>(cex.Checksum, cex.SugaredCmdChecksum, cex)));
- implementation.AssertionChecksumsInCachedSnapshot = result.AssertionChecksums;
- }
- else if (result.Outcome == ConditionGeneration.Outcome.Correct)
- {
- implementation.SetErrorChecksumToCachedError(new List<Tuple<byte[], byte[], object>>());
- implementation.AssertionChecksumsInCachedSnapshot = result.AssertionChecksums;
- }
- }
-
- public override Cmd VisitCallCmd(CallCmd node)
- {
- var result = base.VisitCallCmd(node);
-
- var oldProc = programInCachedSnapshot.FindProcedure(node.Proc.Name);
- if (oldProc != null
- && oldProc.DependencyChecksum != node.Proc.DependencyChecksum
- && node.AssignedAssumptionVariable == null)
- {
- var before = new List<Cmd>();
- var beforePrecondtionCheck = new List<Cmd>();
- var after = new List<Cmd>();
- var axioms = new List<Axiom>();
- Expr assumedExpr = new LiteralExpr(Token.NoToken, false);
- // TODO(wuestholz): Try out two alternatives: only do this for low priority implementations or not at all.
- var canUseSpecs = DependencyCollector.CanExpressOldSpecs(oldProc, Program);
- if (canUseSpecs)
- {
- var desugaring = node.Desugaring;
- Contract.Assert(desugaring != null);
- var precond = node.CheckedPrecondition(oldProc, Program, e => FunctionExtractor.Extract(e, Program, axioms));
- if (precond != null)
- {
- var assume = new AssumeCmd(node.tok, precond, new QKeyValue(Token.NoToken, "precondition_previous_snapshot", new List<object>(), null));
- beforePrecondtionCheck.Add(assume);
- }
-
- var unmods = node.UnmodifiedBefore(oldProc);
- var eqs = new List<Expr>();
- foreach (var unmod in unmods)
- {
- var oldUnmod = new LocalVariable(Token.NoToken,
- new TypedIdent(Token.NoToken, string.Format("{0}##old##{1}", unmod.Name, FreshTemporaryVariableName), unmod.Type));
- var lhs = new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, oldUnmod));
- var rhs = new IdentifierExpr(Token.NoToken, unmod.Decl);
- before.Add(new AssignCmd(Token.NoToken, new List<AssignLhs> { lhs }, new List<Expr> { rhs }));
- var eq = LiteralExpr.Eq(new IdentifierExpr(Token.NoToken, oldUnmod), new IdentifierExpr(Token.NoToken, unmod.Decl));
- eq.Type = Type.Bool;
- eq.TypeParameters = SimpleTypeParamInstantiation.EMPTY;
- eqs.Add(eq);
- }
-
- var mods = node.ModifiedBefore(oldProc);
- var oldSubst = new Dictionary<Variable, Expr>();
- foreach (var mod in mods)
- {
- var oldMod = new LocalVariable(Token.NoToken,
- new TypedIdent(Token.NoToken, string.Format("{0}##old##{1}", mod.Name, FreshTemporaryVariableName), mod.Type));
- oldSubst[mod.Decl] = new IdentifierExpr(Token.NoToken, oldMod);
- var lhs = new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, oldMod));
- var rhs = new IdentifierExpr(Token.NoToken, mod.Decl);
- before.Add(new AssignCmd(Token.NoToken, new List<AssignLhs> { lhs }, new List<Expr> { rhs }));
- }
-
- assumedExpr = node.Postcondition(oldProc, eqs, oldSubst, Program, e => FunctionExtractor.Extract(e, Program, axioms));
- }
-
- if (assumedExpr != null)
- {
- var lv = new LocalVariable(Token.NoToken,
- new TypedIdent(Token.NoToken, string.Format("a##post##{0}", FreshAssumptionVariableName), Type.Bool),
- new QKeyValue(Token.NoToken, "assumption", new List<object>(), null));
- node.AssignedAssumptionVariable = lv;
- currentImplementation.InjectAssumptionVariable(lv, !canUseSpecs);
- var lhs = new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, lv));
- var rhs = LiteralExpr.And(new IdentifierExpr(Token.NoToken, lv), assumedExpr);
- var assumed = new AssignCmd(node.tok, new List<AssignLhs> { lhs }, new List<Expr> { rhs });
- after.Add(assumed);
- }
-
- node.ExtendDesugaring(before, beforePrecondtionCheck, after);
- if (CommandLineOptions.Clo.TraceCachingForTesting || CommandLineOptions.Clo.TraceCachingForBenchmarking)
- {
- using (var tokTxtWr = new TokenTextWriter("<console>", Console.Out, false, false))
- {
- var loc = node.tok != null && node.tok != Token.NoToken ? string.Format("{0}({1},{2})", node.tok.filename, node.tok.line, node.tok.col) : "<unknown location>";
- Console.Out.WriteLine("Processing call to procedure {0} in implementation {1} (at {2}):", node.Proc.Name, currentImplementation.Name, loc);
- foreach (var a in axioms)
- {
- Console.Out.Write(" >>> added axiom: ");
- a.Expr.Emit(tokTxtWr);
- Console.Out.WriteLine();
- }
- foreach (var b in before)
- {
- Console.Out.Write(" >>> added before: ");
- b.Emit(tokTxtWr, 0);
- }
- foreach (var b in beforePrecondtionCheck)
- {
- Console.Out.Write(" >>> added before precondition check: ");
- b.Emit(tokTxtWr, 0);
- }
- foreach (var a in after)
- {
- Console.Out.Write(" >>> added after: ");
- a.Emit(tokTxtWr, 0);
- }
- }
- }
- }
-
- return result;
- }
- }
-
-
- sealed class FunctionExtractor : StandardVisitor
- {
- readonly Dictionary<Variable, BoundVariable> Substitutions = new Dictionary<Variable, BoundVariable>();
-
- public override Expr VisitIdentifierExpr(IdentifierExpr node)
- {
- if (node.Decl == null || !(node.Decl is LocalVariable || node.Decl is Formal || node.Decl is GlobalVariable))
- {
- return node;
- }
- else
- {
- BoundVariable boundVar;
- if (!Substitutions.TryGetValue(node.Decl, out boundVar))
- {
- boundVar = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, node.Name, node.Type));
- Substitutions[node.Decl] = boundVar;
- }
- return new IdentifierExpr(node.tok, boundVar);
- }
- }
-
- public static Expr Extract(Expr expr, Program program, List<Axiom> axioms)
- {
- Contract.Requires(expr != null && program != null && !program.TopLevelDeclarationsAreFrozen && axioms != null);
-
- if (expr is LiteralExpr)
- {
- return expr;
- }
-
- var extractor = new FunctionExtractor();
-
- var body = extractor.VisitExpr(expr);
-
- var name = program.FreshExtractedFunctionName();
- var originalVars = extractor.Substitutions.Keys.ToList();
- var formalInArgs = originalVars.Select(v => new Formal(Token.NoToken, new TypedIdent(Token.NoToken, extractor.Substitutions[v].Name, extractor.Substitutions[v].TypedIdent.Type), true)).ToList<Variable>();
- var formalOutArg = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, name + "$result$", expr.Type), false);
- var func = new Function(Token.NoToken, name, formalInArgs, formalOutArg);
- func.AddAttribute("never_pattern");
-
- var boundVars = originalVars.Select(k => extractor.Substitutions[k]);
- var axiomCall = new NAryExpr(Token.NoToken, new FunctionCall(func), boundVars.Select(b => new IdentifierExpr(Token.NoToken, b)).ToList<Expr>());
- axiomCall.Type = expr.Type;
- axiomCall.TypeParameters = SimpleTypeParamInstantiation.EMPTY;
- var eq = LiteralExpr.Eq(axiomCall, body);
- eq.Type = body.Type;
- eq.TypeParameters = SimpleTypeParamInstantiation.EMPTY;
- if (0 < formalInArgs.Count)
- {
- var forallExpr = new ForallExpr(Token.NoToken, boundVars.ToList<Variable>(), new Trigger(Token.NoToken, true, new List<Expr> { axiomCall }), eq);
- body = forallExpr;
- forallExpr.Attributes = new QKeyValue(Token.NoToken, "weight", new List<object> { new LiteralExpr(Token.NoToken, Basetypes.BigNum.FromInt(30)) }, null);
- body.Type = Type.Bool;
- }
- else
- {
- body = eq;
- }
-
- var axiom = new Axiom(Token.NoToken, body);
- func.DefinitionAxiom = axiom;
- program.AddTopLevelDeclaration(func);
- program.AddTopLevelDeclaration(axiom);
- axioms.Add(axiom);
-
- var call = new NAryExpr(Token.NoToken, new FunctionCall(func), originalVars.Select(v => new IdentifierExpr(Token.NoToken, v)).ToList<Expr>());
- call.Type = expr.Type;
- call.TypeParameters = SimpleTypeParamInstantiation.EMPTY;
- return call;
- }
- }
-
-
- sealed class OtherDefinitionAxiomsCollector : ReadOnlyVisitor
- {
- Axiom currentAxiom;
- Trigger currentTrigger;
-
- public static void Collect(IEnumerable<Axiom> axioms)
- {
- var start = DateTime.UtcNow;
-
- var v = new OtherDefinitionAxiomsCollector();
- foreach (var a in axioms)
- {
- v.currentAxiom = a;
- v.VisitExpr(a.Expr);
- v.currentAxiom = null;
- }
-
- var end = DateTime.UtcNow;
- if (CommandLineOptions.Clo.TraceCachingForDebugging)
- {
- Console.Out.WriteLine("Collected other definition axioms within {0:F0} ms.", end.Subtract(start).TotalMilliseconds);
- }
- }
-
- public override QuantifierExpr VisitQuantifierExpr(QuantifierExpr node)
- {
- currentTrigger = node.Triggers;
- while (currentTrigger != null)
- {
- foreach (var e in currentTrigger.Tr)
- {
- VisitExpr(e);
- }
- currentTrigger = currentTrigger.Next;
- }
- return base.VisitQuantifierExpr(node);
- }
-
- public override Expr VisitNAryExpr(NAryExpr node)
- {
- if (currentTrigger != null)
- {
- // We found a function call within a trigger of a quantifier expression.
- var funCall = node.Fun as FunctionCall;
- if (funCall != null && funCall.Func != null && funCall.Func.Checksum != null && funCall.Func.Checksum != "stable")
- {
- funCall.Func.AddOtherDefinitionAxiom(currentAxiom);
- }
- }
- return base.VisitNAryExpr(node);
- }
- }
-
-
- sealed class DependencyCollector : ReadOnlyVisitor
- {
- private DeclWithFormals currentDeclaration;
- private Axiom currentAxiom;
-
- public static void Collect(Program program)
- {
- var start = DateTime.UtcNow;
-
- var dc = new DependencyCollector();
- dc.VisitProgram(program);
-
- var end = DateTime.UtcNow;
- if (CommandLineOptions.Clo.TraceCachingForDebugging)
- {
- Console.Out.WriteLine("Collected dependencies within {0:F0} ms.", end.Subtract(start).TotalMilliseconds);
- }
- }
-
- public static bool CanExpressOldSpecs(Procedure oldProc, Program newProg)
- {
- Contract.Requires(oldProc != null && newProg != null);
-
- var funcs = newProg.Functions;
- var globals = newProg.GlobalVariables;
- return oldProc.DependenciesCollected
- && (oldProc.FunctionDependencies == null || oldProc.FunctionDependencies.All(dep => funcs.Any(f => f.Name == dep.Name && f.DependencyChecksum == dep.DependencyChecksum)))
- && oldProc.Modifies.All(m => globals.Any(g => g.Name == m.Name));
- }
-
- public override Procedure VisitProcedure(Procedure node)
- {
- currentDeclaration = node;
-
- foreach (var param in node.InParams)
- {
- if (param.TypedIdent != null && param.TypedIdent.WhereExpr != null)
- {
- VisitExpr(param.TypedIdent.WhereExpr);
- }
- }
-
- var result = base.VisitProcedure(node);
- node.DependenciesCollected = true;
- currentDeclaration = null;
- return result;
- }
-
- public override Implementation VisitImplementation(Implementation node)
- {
- currentDeclaration = node;
-
- foreach (var param in node.InParams)
- {
- if (param.TypedIdent != null && param.TypedIdent.WhereExpr != null)
- {
- VisitExpr(param.TypedIdent.WhereExpr);
- }
- }
-
- if (node.Proc != null)
- {
- node.AddProcedureDependency(node.Proc);
- }
-
- var result = base.VisitImplementation(node);
- node.DependenciesCollected = true;
- currentDeclaration = null;
- return result;
- }
-
- public override Axiom VisitAxiom(Axiom node)
- {
- if (node.DependenciesCollected)
- {
- if (currentDeclaration != null && node.FunctionDependencies != null)
- {
- foreach (var f in node.FunctionDependencies)
- {
- currentDeclaration.AddFunctionDependency(f);
- }
- }
- return node;
- }
- currentAxiom = node;
- var result = base.VisitAxiom(node);
- node.DependenciesCollected = true;
- currentAxiom = null;
- return result;
- }
-
- public override Function VisitFunction(Function node)
- {
- currentDeclaration = node;
-
- if (node.DefinitionAxiom != null)
- {
- VisitAxiom(node.DefinitionAxiom);
- }
- if (node.OtherDefinitionAxioms != null)
- {
- foreach (var a in node.OtherDefinitionAxioms)
- {
- if (a != node.DefinitionAxiom)
- {
- VisitAxiom(a);
- }
- }
- }
-
- var result = base.VisitFunction(node);
- node.DependenciesCollected = true;
- currentDeclaration = null;
- return result;
- }
-
- public override Cmd VisitCallCmd(CallCmd node)
- {
- if (currentDeclaration != null)
- {
- currentDeclaration.AddProcedureDependency(node.Proc);
- }
-
- return base.VisitCallCmd(node);
- }
-
- public override Expr VisitNAryExpr(NAryExpr node)
- {
- var funCall = node.Fun as FunctionCall;
- if (funCall != null)
- {
- if (currentDeclaration != null)
- {
- currentDeclaration.AddFunctionDependency(funCall.Func);
- }
- if (currentAxiom != null)
- {
- currentAxiom.AddFunctionDependency(funCall.Func);
- }
- }
-
- return base.VisitNAryExpr(node);
- }
- }
-
-
- static internal class Priority
- {
- public static readonly int LOW = 1; // the same snapshot has been verified before, but a callee has changed
- public static readonly int MEDIUM = 2; // old snapshot has been verified before
- public static readonly int HIGH = 3; // has been never verified before
- public static readonly int SKIP = int.MaxValue; // highest priority to get them done as soon as possible
- }
-
-
- public sealed class VerificationResultCache
- {
- private readonly MemoryCache Cache = new MemoryCache("VerificationResultCache");
- private readonly CacheItemPolicy Policy = new CacheItemPolicy { SlidingExpiration = new TimeSpan(0, 10, 0), Priority = CacheItemPriority.Default };
-
-
- public void Insert(Implementation impl, VerificationResult result)
- {
- Contract.Requires(impl != null);
- Contract.Requires(result != null);
-
- Cache.Set(impl.Id, result, Policy);
- }
-
-
- public VerificationResult Lookup(Implementation impl, out int priority)
- {
- Contract.Requires(impl != null);
-
- var result = Cache.Get(impl.Id) as VerificationResult;
- if (result == null)
- {
- priority = Priority.HIGH;
- }
- else if (result.Checksum != impl.Checksum)
- {
- priority = Priority.MEDIUM;
- }
- else if (impl.DependencyChecksum == null || result.DependeciesChecksum != impl.DependencyChecksum)
- {
- priority = Priority.LOW;
- }
- else
- {
- priority = Priority.SKIP;
- }
- return result;
- }
-
-
- public void Clear()
- {
- Cache.Trim(100);
- }
-
-
- public void RemoveMatchingKeys(Regex keyRegexp)
- {
- Contract.Requires(keyRegexp != null);
-
- foreach (var kv in Cache)
- {
- if (keyRegexp.IsMatch(kv.Key))
- {
- Cache.Remove(kv.Key);
- }
- }
- }
-
-
- public int VerificationPriority(Implementation impl)
- {
- Contract.Requires(impl != null);
-
- int priority;
- Lookup(impl, out priority);
- return priority;
- }
- }
-
-}
+using System;
+using System.Collections.Concurrent;
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+using System.IO;
+using System.Linq;
+using System.Runtime.Caching;
+using System.Text;
+using System.Text.RegularExpressions;
+using VC;
+
+namespace Microsoft.Boogie
+{
+
+ struct CachedVerificationResultInjectorRun
+ {
+ public DateTime Start { get; internal set; }
+ public DateTime End { get; internal set; }
+ public int TransformedImplementationCount { get; internal set; }
+ public int ImplementationCount { get; internal set; }
+ public int SkippedImplementationCount { get; set; }
+ public int LowPriorityImplementationCount { get; set; }
+ public int MediumPriorityImplementationCount { get; set; }
+ public int HighPriorityImplementationCount { get; set; }
+ public long[] CachingActionCounts { get; set; }
+ }
+
+
+ sealed class CachedVerificationResultInjectorStatistics
+ {
+ ConcurrentDictionary<string, CachedVerificationResultInjectorRun> runs = new ConcurrentDictionary<string, CachedVerificationResultInjectorRun>();
+
+ public bool AddRun(string requestId, CachedVerificationResultInjectorRun run)
+ {
+ return runs.TryAdd(requestId, run);
+ }
+
+ public string Output(bool printTime = false)
+ {
+ var wr = new StringWriter();
+ if (runs.Any())
+ {
+ wr.WriteLine("Cached verification result injector statistics as CSV:");
+ wr.WriteLine("Request ID, Transformed, Low, Medium, High, Skipped{0}", printTime ? ", Time (ms)" : "");
+ foreach (var kv in runs.OrderBy(kv => ExecutionEngine.AutoRequestId(kv.Key)))
+ {
+ var t = printTime ? string.Format(", {0,8:F0}", kv.Value.End.Subtract(kv.Value.Start).TotalMilliseconds) : "";
+ wr.WriteLine("{0,-19}, {1,3}, {2,3}, {3,3}, {4,3}, {5,3}{6}", kv.Key, kv.Value.TransformedImplementationCount, kv.Value.LowPriorityImplementationCount, kv.Value.MediumPriorityImplementationCount, kv.Value.HighPriorityImplementationCount, kv.Value.SkippedImplementationCount, t);
+ }
+ }
+ return wr.ToString();
+ }
+ }
+
+
+ sealed class CachedVerificationResultInjector : StandardVisitor
+ {
+ readonly IEnumerable<Implementation> Implementations;
+ readonly Program Program;
+ // TODO(wuestholz): We should probably increase the threshold to something like 2 seconds.
+ static readonly double TimeThreshold = -1.0d;
+ Program programInCachedSnapshot;
+ Implementation currentImplementation;
+ int assumptionVariableCount;
+ int temporaryVariableCount;
+
+ public static readonly CachedVerificationResultInjectorStatistics Statistics = new CachedVerificationResultInjectorStatistics();
+
+ int FreshAssumptionVariableName
+ {
+ get
+ {
+ return assumptionVariableCount++;
+ }
+ }
+
+ int FreshTemporaryVariableName
+ {
+ get
+ {
+ return temporaryVariableCount++;
+ }
+ }
+
+ CachedVerificationResultInjector(Program program, IEnumerable<Implementation> implementations)
+ {
+ Implementations = implementations;
+ Program = program;
+ }
+
+ public Implementation Inject(Implementation implementation, Program programInCachedSnapshot)
+ {
+ Contract.Requires(implementation != null && programInCachedSnapshot != null);
+
+ this.programInCachedSnapshot = programInCachedSnapshot;
+ assumptionVariableCount = 0;
+ temporaryVariableCount = 0;
+ currentImplementation = implementation;
+
+ #region Introduce explict assumption about the precondition.
+
+ var oldProc = programInCachedSnapshot.FindProcedure(currentImplementation.Proc.Name);
+ if (oldProc != null
+ && oldProc.DependencyChecksum != currentImplementation.Proc.DependencyChecksum
+ && currentImplementation.ExplicitAssumptionAboutCachedPrecondition == null)
+ {
+ var axioms = new List<Axiom>();
+ var after = new List<Cmd>();
+ Expr assumedExpr = new LiteralExpr(Token.NoToken, false);
+ var canUseSpecs = DependencyCollector.CanExpressOldSpecs(oldProc, Program, true);
+ if (canUseSpecs && oldProc.SignatureEquals(currentImplementation.Proc))
+ {
+ var always = Substituter.SubstitutionFromHashtable(currentImplementation.GetImplFormalMap(), true, currentImplementation.Proc);
+ var forOld = Substituter.SubstitutionFromHashtable(new Dictionary<Variable, Expr>());
+ var clauses = oldProc.Requires.Select(r => Substituter.FunctionCallReresolvingApply(always, forOld, r.Condition, Program));
+ var conj = Expr.And(clauses, true);
+ assumedExpr = conj != null ? FunctionExtractor.Extract(conj, Program, axioms) : new LiteralExpr(Token.NoToken, true);
+ }
+
+ if (assumedExpr != null)
+ {
+ var lv = new LocalVariable(Token.NoToken,
+ new TypedIdent(Token.NoToken, string.Format("a##cached##{0}", FreshAssumptionVariableName), Type.Bool),
+ new QKeyValue(Token.NoToken, "assumption", new List<object>(), null));
+ currentImplementation.InjectAssumptionVariable(lv, !canUseSpecs);
+ var lhs = new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, lv));
+ var rhs = LiteralExpr.And(new IdentifierExpr(Token.NoToken, lv), assumedExpr);
+ var assumed = new AssignCmd(currentImplementation.tok, new List<AssignLhs> { lhs }, new List<Expr> { rhs });
+ assumed.IrrelevantForChecksumComputation = true;
+ currentImplementation.ExplicitAssumptionAboutCachedPrecondition = assumed;
+ after.Add(assumed);
+ }
+
+ if (CommandLineOptions.Clo.TraceCachingForTesting || CommandLineOptions.Clo.TraceCachingForBenchmarking)
+ {
+ using (var tokTxtWr = new TokenTextWriter("<console>", Console.Out, false, false))
+ {
+ var loc = currentImplementation.tok != null && currentImplementation.tok != Token.NoToken ? string.Format("{0}({1},{2})", currentImplementation.tok.filename, currentImplementation.tok.line, currentImplementation.tok.col) : "<unknown location>";
+ Console.Out.WriteLine("Processing implementation {0} (at {1}):", currentImplementation.Name, loc);
+ foreach (var a in axioms)
+ {
+ Console.Out.Write(" >>> added axiom: ");
+ a.Expr.Emit(tokTxtWr);
+ Console.Out.WriteLine();
+ }
+ foreach (var b in after)
+ {
+ Console.Out.Write(" >>> added after assuming the current precondition: ");
+ b.Emit(tokTxtWr, 0);
+ }
+ }
+ }
+ }
+
+ #endregion
+
+ var result = VisitImplementation(currentImplementation);
+ currentImplementation = null;
+ this.programInCachedSnapshot = null;
+ return result;
+ }
+
+ public static void Inject(Program program, IEnumerable<Implementation> implementations, string requestId, string programId, out long[] cachingActionCounts)
+ {
+ var eai = new CachedVerificationResultInjector(program, implementations);
+
+ cachingActionCounts = new long[Enum.GetNames(typeof(VC.ConditionGeneration.CachingAction)).Length];
+ var run = new CachedVerificationResultInjectorRun { Start = DateTime.UtcNow, ImplementationCount = implementations.Count(), CachingActionCounts = cachingActionCounts };
+ foreach (var impl in implementations)
+ {
+ int priority;
+ var vr = ExecutionEngine.Cache.Lookup(impl, out priority);
+ if (vr != null && vr.ProgramId == programId)
+ {
+ if (priority == Priority.LOW) {
+ run.LowPriorityImplementationCount++;
+ } else if (priority == Priority.MEDIUM) {
+ run.MediumPriorityImplementationCount++;
+ } else if (priority == Priority.HIGH) {
+ run.HighPriorityImplementationCount++;
+ } else if (priority == Priority.SKIP) {
+ run.SkippedImplementationCount++;
+ }
+
+ if (priority == Priority.LOW || priority == Priority.MEDIUM || 3 <= CommandLineOptions.Clo.VerifySnapshots) {
+ if (TimeThreshold < vr.End.Subtract(vr.Start).TotalMilliseconds) {
+ SetErrorAndAssertionChecksumsInCachedSnapshot(impl, vr);
+ if (vr.ProgramId != null) {
+ var p = ExecutionEngine.CachedProgram(vr.ProgramId);
+ if (p != null) {
+ eai.Inject(impl, p);
+ run.TransformedImplementationCount++;
+ }
+ }
+ }
+ }
+ }
+ }
+ run.End = DateTime.UtcNow;
+ Statistics.AddRun(requestId, run);
+ }
+
+ private static void SetErrorAndAssertionChecksumsInCachedSnapshot(Implementation implementation, VerificationResult result)
+ {
+ if (result.Outcome == ConditionGeneration.Outcome.Errors && result.Errors != null && result.Errors.Count < CommandLineOptions.Clo.ProverCCLimit)
+ {
+ implementation.SetErrorChecksumToCachedError(result.Errors.Select(cex => new Tuple<byte[], byte[], object>(cex.Checksum, cex.SugaredCmdChecksum, cex)));
+ implementation.AssertionChecksumsInCachedSnapshot = result.AssertionChecksums;
+ }
+ else if (result.Outcome == ConditionGeneration.Outcome.Correct)
+ {
+ implementation.SetErrorChecksumToCachedError(new List<Tuple<byte[], byte[], object>>());
+ implementation.AssertionChecksumsInCachedSnapshot = result.AssertionChecksums;
+ }
+ }
+
+ public override Cmd VisitCallCmd(CallCmd node)
+ {
+ var result = base.VisitCallCmd(node);
+
+ var oldProc = programInCachedSnapshot.FindProcedure(node.Proc.Name);
+ if (oldProc != null
+ && oldProc.DependencyChecksum != node.Proc.DependencyChecksum
+ && node.AssignedAssumptionVariable == null)
+ {
+ var before = new List<Cmd>();
+ var beforePrecondtionCheck = new List<Cmd>();
+ var after = new List<Cmd>();
+ var axioms = new List<Axiom>();
+ Expr assumedExpr = new LiteralExpr(Token.NoToken, false);
+ // TODO(wuestholz): Try out two alternatives: only do this for low priority implementations or not at all.
+ var canUseSpecs = DependencyCollector.CanExpressOldSpecs(oldProc, Program);
+ if (canUseSpecs && oldProc.SignatureEquals(node.Proc))
+ {
+ var desugaring = node.Desugaring;
+ Contract.Assert(desugaring != null);
+ var precond = node.CheckedPrecondition(oldProc, Program, e => FunctionExtractor.Extract(e, Program, axioms));
+ if (precond != null)
+ {
+ var assume = new AssumeCmd(node.tok, precond, new QKeyValue(Token.NoToken, "precondition_previous_snapshot", new List<object>(), null));
+ assume.IrrelevantForChecksumComputation = true;
+ beforePrecondtionCheck.Add(assume);
+ }
+
+ var unmods = node.UnmodifiedBefore(oldProc);
+ var eqs = new List<Expr>();
+ foreach (var unmod in unmods)
+ {
+ var oldUnmod = new LocalVariable(Token.NoToken,
+ new TypedIdent(Token.NoToken, string.Format("{0}##old##{1}", unmod.Name, FreshTemporaryVariableName), unmod.Type));
+ var lhs = new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, oldUnmod));
+ var rhs = new IdentifierExpr(Token.NoToken, unmod.Decl);
+ var cmd = new AssignCmd(Token.NoToken, new List<AssignLhs> { lhs }, new List<Expr> { rhs });
+ cmd.IrrelevantForChecksumComputation = true;
+ before.Add(cmd);
+ var eq = LiteralExpr.Eq(new IdentifierExpr(Token.NoToken, oldUnmod), new IdentifierExpr(Token.NoToken, unmod.Decl));
+ eq.Type = Type.Bool;
+ eq.TypeParameters = SimpleTypeParamInstantiation.EMPTY;
+ eqs.Add(eq);
+ }
+
+ var mods = node.ModifiedBefore(oldProc);
+ var oldSubst = new Dictionary<Variable, Expr>();
+ foreach (var mod in mods)
+ {
+ var oldMod = new LocalVariable(Token.NoToken,
+ new TypedIdent(Token.NoToken, string.Format("{0}##old##{1}", mod.Name, FreshTemporaryVariableName), mod.Type));
+ oldSubst[mod.Decl] = new IdentifierExpr(Token.NoToken, oldMod);
+ var lhs = new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, oldMod));
+ var rhs = new IdentifierExpr(Token.NoToken, mod.Decl);
+ var cmd = new AssignCmd(Token.NoToken, new List<AssignLhs> { lhs }, new List<Expr> { rhs });
+ cmd.IrrelevantForChecksumComputation = true;
+ before.Add(cmd);
+ }
+
+ assumedExpr = node.Postcondition(oldProc, eqs, oldSubst, Program, e => FunctionExtractor.Extract(e, Program, axioms));
+ if (assumedExpr == null)
+ {
+ assumedExpr = new LiteralExpr(Token.NoToken, true);
+ }
+ }
+
+ if (assumedExpr != null)
+ {
+ var lv = new LocalVariable(Token.NoToken,
+ new TypedIdent(Token.NoToken, string.Format("a##cached##{0}", FreshAssumptionVariableName), Type.Bool),
+ new QKeyValue(Token.NoToken, "assumption", new List<object>(), null));
+ node.AssignedAssumptionVariable = lv;
+ currentImplementation.InjectAssumptionVariable(lv, !canUseSpecs);
+ var lhs = new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, lv));
+ var rhs = LiteralExpr.And(new IdentifierExpr(Token.NoToken, lv), assumedExpr);
+ var assumed = new AssignCmd(node.tok, new List<AssignLhs> { lhs }, new List<Expr> { rhs });
+ assumed.IrrelevantForChecksumComputation = true;
+ after.Add(assumed);
+ }
+
+ node.ExtendDesugaring(before, beforePrecondtionCheck, after);
+ if (CommandLineOptions.Clo.TraceCachingForTesting || CommandLineOptions.Clo.TraceCachingForBenchmarking)
+ {
+ using (var tokTxtWr = new TokenTextWriter("<console>", Console.Out, false, false))
+ {
+ var loc = node.tok != null && node.tok != Token.NoToken ? string.Format("{0}({1},{2})", node.tok.filename, node.tok.line, node.tok.col) : "<unknown location>";
+ Console.Out.WriteLine("Processing call to procedure {0} in implementation {1} (at {2}):", node.Proc.Name, currentImplementation.Name, loc);
+ foreach (var a in axioms)
+ {
+ Console.Out.Write(" >>> added axiom: ");
+ a.Expr.Emit(tokTxtWr);
+ Console.Out.WriteLine();
+ }
+ foreach (var b in before)
+ {
+ Console.Out.Write(" >>> added before: ");
+ b.Emit(tokTxtWr, 0);
+ }
+ foreach (var b in beforePrecondtionCheck)
+ {
+ Console.Out.Write(" >>> added before precondition check: ");
+ b.Emit(tokTxtWr, 0);
+ }
+ foreach (var a in after)
+ {
+ Console.Out.Write(" >>> added after: ");
+ a.Emit(tokTxtWr, 0);
+ }
+ }
+ }
+ }
+
+ return result;
+ }
+ }
+
+
+ sealed class FunctionExtractor : StandardVisitor
+ {
+ readonly Dictionary<Variable, BoundVariable> Substitutions = new Dictionary<Variable, BoundVariable>();
+
+ public override Expr VisitIdentifierExpr(IdentifierExpr node)
+ {
+ if (node.Decl == null || !(node.Decl is LocalVariable || node.Decl is Formal || node.Decl is GlobalVariable))
+ {
+ return node;
+ }
+ else
+ {
+ BoundVariable boundVar;
+ if (!Substitutions.TryGetValue(node.Decl, out boundVar))
+ {
+ boundVar = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, node.Name, node.Type));
+ Substitutions[node.Decl] = boundVar;
+ }
+ return new IdentifierExpr(node.tok, boundVar);
+ }
+ }
+
+ public static Expr Extract(Expr expr, Program program, List<Axiom> axioms)
+ {
+ Contract.Requires(expr != null && program != null && !program.TopLevelDeclarationsAreFrozen && axioms != null);
+
+ if (expr is LiteralExpr)
+ {
+ return expr;
+ }
+
+ var extractor = new FunctionExtractor();
+
+ var body = extractor.VisitExpr(expr);
+
+ var name = program.FreshExtractedFunctionName();
+ var originalVars = extractor.Substitutions.Keys.ToList();
+ var formalInArgs = originalVars.Select(v => new Formal(Token.NoToken, new TypedIdent(Token.NoToken, extractor.Substitutions[v].Name, extractor.Substitutions[v].TypedIdent.Type), true)).ToList<Variable>();
+ var formalOutArg = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, name + "$result$", expr.Type), false);
+ var func = new Function(Token.NoToken, name, formalInArgs, formalOutArg);
+ func.AddAttribute("never_pattern");
+
+ var boundVars = originalVars.Select(k => extractor.Substitutions[k]);
+ var axiomCall = new NAryExpr(Token.NoToken, new FunctionCall(func), boundVars.Select(b => new IdentifierExpr(Token.NoToken, b)).ToList<Expr>());
+ axiomCall.Type = expr.Type;
+ axiomCall.TypeParameters = SimpleTypeParamInstantiation.EMPTY;
+ var eq = LiteralExpr.Eq(axiomCall, body);
+ eq.Type = body.Type;
+ eq.TypeParameters = SimpleTypeParamInstantiation.EMPTY;
+ if (0 < formalInArgs.Count)
+ {
+ var forallExpr = new ForallExpr(Token.NoToken, boundVars.ToList<Variable>(), new Trigger(Token.NoToken, true, new List<Expr> { axiomCall }), eq);
+ body = forallExpr;
+ forallExpr.Attributes = new QKeyValue(Token.NoToken, "weight", new List<object> { new LiteralExpr(Token.NoToken, Basetypes.BigNum.FromInt(30)) }, null);
+ body.Type = Type.Bool;
+ }
+ else
+ {
+ body = eq;
+ }
+
+ var axiom = new Axiom(Token.NoToken, body);
+ func.DefinitionAxiom = axiom;
+ program.AddTopLevelDeclaration(func);
+ program.AddTopLevelDeclaration(axiom);
+ axioms.Add(axiom);
+
+ var call = new NAryExpr(Token.NoToken, new FunctionCall(func), originalVars.Select(v => new IdentifierExpr(Token.NoToken, v)).ToList<Expr>());
+ call.Type = expr.Type;
+ call.TypeParameters = SimpleTypeParamInstantiation.EMPTY;
+ return call;
+ }
+ }
+
+
+ sealed class OtherDefinitionAxiomsCollector : ReadOnlyVisitor
+ {
+ Axiom currentAxiom;
+ Trigger currentTrigger;
+
+ public static void Collect(IEnumerable<Axiom> axioms)
+ {
+ var start = DateTime.UtcNow;
+
+ var v = new OtherDefinitionAxiomsCollector();
+ foreach (var a in axioms)
+ {
+ v.currentAxiom = a;
+ v.VisitExpr(a.Expr);
+ v.currentAxiom = null;
+ }
+
+ var end = DateTime.UtcNow;
+ if (CommandLineOptions.Clo.TraceCachingForDebugging)
+ {
+ Console.Out.WriteLine("Collected other definition axioms within {0:F0} ms.", end.Subtract(start).TotalMilliseconds);
+ }
+ }
+
+ public override QuantifierExpr VisitQuantifierExpr(QuantifierExpr node)
+ {
+ currentTrigger = node.Triggers;
+ while (currentTrigger != null)
+ {
+ foreach (var e in currentTrigger.Tr)
+ {
+ VisitExpr(e);
+ }
+ currentTrigger = currentTrigger.Next;
+ }
+ return base.VisitQuantifierExpr(node);
+ }
+
+ public override Expr VisitNAryExpr(NAryExpr node)
+ {
+ if (currentTrigger != null)
+ {
+ // We found a function call within a trigger of a quantifier expression.
+ var funCall = node.Fun as FunctionCall;
+ if (funCall != null && funCall.Func != null && funCall.Func.Checksum != null && funCall.Func.Checksum != "stable")
+ {
+ funCall.Func.AddOtherDefinitionAxiom(currentAxiom);
+ }
+ }
+ return base.VisitNAryExpr(node);
+ }
+ }
+
+
+ sealed class DependencyCollector : ReadOnlyVisitor
+ {
+ private DeclWithFormals currentDeclaration;
+ private Axiom currentAxiom;
+
+ public static void Collect(Program program)
+ {
+ var start = DateTime.UtcNow;
+
+ var dc = new DependencyCollector();
+ dc.VisitProgram(program);
+
+ var end = DateTime.UtcNow;
+ if (CommandLineOptions.Clo.TraceCachingForDebugging)
+ {
+ Console.Out.WriteLine("Collected dependencies within {0:F0} ms.", end.Subtract(start).TotalMilliseconds);
+ }
+ }
+
+ public static bool CanExpressOldSpecs(Procedure oldProc, Program newProg, bool ignoreModifiesClauses = false)
+ {
+ Contract.Requires(oldProc != null && newProg != null);
+
+ var funcs = newProg.Functions;
+ var globals = newProg.GlobalVariables;
+ return oldProc.DependenciesCollected
+ && (oldProc.FunctionDependencies == null || oldProc.FunctionDependencies.All(dep => funcs.Any(f => f.Name == dep.Name && f.DependencyChecksum == dep.DependencyChecksum)))
+ && (ignoreModifiesClauses || oldProc.Modifies.All(m => globals.Any(g => g.Name == m.Name)));
+ }
+
+ public override Procedure VisitProcedure(Procedure node)
+ {
+ currentDeclaration = node;
+
+ foreach (var param in node.InParams)
+ {
+ if (param.TypedIdent != null && param.TypedIdent.WhereExpr != null)
+ {
+ VisitExpr(param.TypedIdent.WhereExpr);
+ }
+ }
+
+ var result = base.VisitProcedure(node);
+ node.DependenciesCollected = true;
+ currentDeclaration = null;
+ return result;
+ }
+
+ public override Implementation VisitImplementation(Implementation node)
+ {
+ currentDeclaration = node;
+
+ foreach (var param in node.InParams)
+ {
+ if (param.TypedIdent != null && param.TypedIdent.WhereExpr != null)
+ {
+ VisitExpr(param.TypedIdent.WhereExpr);
+ }
+ }
+
+ if (node.Proc != null)
+ {
+ node.AddProcedureDependency(node.Proc);
+ }
+
+ var result = base.VisitImplementation(node);
+ node.DependenciesCollected = true;
+ currentDeclaration = null;
+ return result;
+ }
+
+ public override Axiom VisitAxiom(Axiom node)
+ {
+ if (node.DependenciesCollected)
+ {
+ if (currentDeclaration != null && node.FunctionDependencies != null)
+ {
+ foreach (var f in node.FunctionDependencies)
+ {
+ currentDeclaration.AddFunctionDependency(f);
+ }
+ }
+ return node;
+ }
+ currentAxiom = node;
+ var result = base.VisitAxiom(node);
+ node.DependenciesCollected = true;
+ currentAxiom = null;
+ return result;
+ }
+
+ public override Function VisitFunction(Function node)
+ {
+ currentDeclaration = node;
+
+ if (node.DefinitionAxiom != null)
+ {
+ VisitAxiom(node.DefinitionAxiom);
+ }
+ if (node.OtherDefinitionAxioms != null)
+ {
+ foreach (var a in node.OtherDefinitionAxioms)
+ {
+ if (a != node.DefinitionAxiom)
+ {
+ VisitAxiom(a);
+ }
+ }
+ }
+
+ var result = base.VisitFunction(node);
+ node.DependenciesCollected = true;
+ currentDeclaration = null;
+ return result;
+ }
+
+ public override Cmd VisitCallCmd(CallCmd node)
+ {
+ if (currentDeclaration != null)
+ {
+ currentDeclaration.AddProcedureDependency(node.Proc);
+ }
+
+ return base.VisitCallCmd(node);
+ }
+
+ public override Expr VisitNAryExpr(NAryExpr node)
+ {
+ var funCall = node.Fun as FunctionCall;
+ if (funCall != null)
+ {
+ if (currentDeclaration != null)
+ {
+ currentDeclaration.AddFunctionDependency(funCall.Func);
+ }
+ if (currentAxiom != null)
+ {
+ currentAxiom.AddFunctionDependency(funCall.Func);
+ }
+ }
+
+ return base.VisitNAryExpr(node);
+ }
+ }
+
+
+ static internal class Priority
+ {
+ public static readonly int LOW = 1; // the same snapshot has been verified before, but a callee has changed
+ public static readonly int MEDIUM = 2; // old snapshot has been verified before
+ public static readonly int HIGH = 3; // has been never verified before
+ public static readonly int SKIP = int.MaxValue; // highest priority to get them done as soon as possible
+ }
+
+
+ public sealed class VerificationResultCache
+ {
+ private readonly MemoryCache Cache = new MemoryCache("VerificationResultCache");
+ private readonly CacheItemPolicy Policy = new CacheItemPolicy { SlidingExpiration = new TimeSpan(0, 10, 0), Priority = CacheItemPriority.Default };
+
+
+ public void Insert(Implementation impl, VerificationResult result)
+ {
+ Contract.Requires(impl != null);
+ Contract.Requires(result != null);
+
+ Cache.Set(impl.Id, result, Policy);
+ }
+
+
+ public VerificationResult Lookup(Implementation impl, out int priority)
+ {
+ Contract.Requires(impl != null);
+
+ var result = Cache.Get(impl.Id) as VerificationResult;
+ if (result == null)
+ {
+ priority = Priority.HIGH;
+ }
+ else if (result.Checksum != impl.Checksum)
+ {
+ priority = Priority.MEDIUM;
+ }
+ else if (impl.DependencyChecksum == null || result.DependeciesChecksum != impl.DependencyChecksum)
+ {
+ priority = Priority.LOW;
+ }
+ else if (result.Outcome == ConditionGeneration.Outcome.TimedOut && CommandLineOptions.Clo.RunDiagnosticsOnTimeout)
+ {
+ priority = Priority.MEDIUM;
+ }
+ else
+ {
+ priority = Priority.SKIP;
+ }
+ return result;
+ }
+
+
+ public void Clear()
+ {
+ Cache.Trim(100);
+ }
+
+
+ public void RemoveMatchingKeys(Regex keyRegexp)
+ {
+ Contract.Requires(keyRegexp != null);
+
+ foreach (var kv in Cache)
+ {
+ if (keyRegexp.IsMatch(kv.Key))
+ {
+ Cache.Remove(kv.Key);
+ }
+ }
+ }
+
+
+ public int VerificationPriority(Implementation impl)
+ {
+ Contract.Requires(impl != null);
+
+ int priority;
+ Lookup(impl, out priority);
+ return priority;
+ }
+ }
+
+}
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 19:09:51 +0000