diff options
| author |  Pantazis Deligiannis <pdeligia@me.com> | 2013-07-06 11:29:20 +0100 |
|---|---|---|
| committer | Pantazis Deligiannis <pdeligia@me.com> | 2013-07-06 11:29:20 +0100 |
| commit | 5dcb1f8e4f28db2f449cb318fc8f114e2982cc7c (patch) | |
| tree | d1a47b7f223d2db43fbb589e5f6dddc2d03c3a44 | |
| parent | 6e773bb7b5dff32ca7ba552b2562ccc18b02fece (diff) | |
| parent | 5fe9141ded93f6eab4e213c1d082b68ac557d81a (diff) | |
merge
34 files changed, 2280 insertions, 779 deletions
diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs index be62eb58..c024a62a 100644 --- a/Source/AbsInt/IntervalDomain.cs +++ b/Source/AbsInt/IntervalDomain.cs @@ -857,6 +857,14 @@ namespace Microsoft.Boogie.AbstractInterpretation Lo = Node.Min(lo0, lo1, false);
Hi = Node.Max(hi0, hi1, false);
}
+ } else if (node.Fun is FunctionCall) {
+ var call = (FunctionCall)node.Fun;
+ // See if this is an identity function, which we do by checking: that the function has
+ // exactly one argument and the function has been marked by the user with the attribute {:identity}
+ bool claimsToBeIdentity = false;
+ if (call.ArgumentCount == 1 && call.Func.CheckBooleanAttribute("identity", ref claimsToBeIdentity) && claimsToBeIdentity && node.Args[0].Type.Equals(node.Type)) {
+ VisitExpr(node.Args[0]);
+ }
}
return node;
}
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 7eacf697..12a6084f 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -37,13 +37,13 @@ namespace Microsoft.Boogie { goto END;
}
if (CommandLineOptions.Clo.Files.Count == 0) {
- ExecutionEngine.printer.ErrorWriteLine("*** Error: No input files were specified.");
+ ExecutionEngine.printer.ErrorWriteLine(Console.Out, "*** Error: No input files were specified.");
goto END;
}
if (CommandLineOptions.Clo.XmlSink != null) {
string errMsg = CommandLineOptions.Clo.XmlSink.Open();
if (errMsg != null) {
- ExecutionEngine.printer.ErrorWriteLine("*** Error: " + errMsg);
+ ExecutionEngine.printer.ErrorWriteLine(Console.Out, "*** Error: " + errMsg);
goto END;
}
}
@@ -84,7 +84,7 @@ namespace Microsoft.Boogie { extension = extension.ToLower();
}
if (extension != ".bpl") {
- ExecutionEngine.printer.ErrorWriteLine("*** Error: '{0}': Filename extension '{1}' is not supported. Input files must be BoogiePL programs (.bpl).", file,
+ ExecutionEngine.printer.ErrorWriteLine(Console.Out, "*** Error: '{0}': Filename extension '{1}' is not supported. Input files must be BoogiePL programs (.bpl).", file,
extension == null ? "" : extension);
goto END;
}
@@ -100,27 +100,5 @@ namespace Microsoft.Boogie { Console.ReadLine();
}
}
-
-
- #region // TODO: Is this still used?
-
- enum FileType
- {
- Unknown,
- Cil,
- Bpl,
- Dafny
- };
-
-
- static bool ProgramHasDebugInfo(Program program)
- {
- Contract.Requires(program != null);
- // We inspect the last declaration because the first comes from the prelude and therefore always has source context.
- return program.TopLevelDeclarations.Count > 0 &&
- ((cce.NonNull(program.TopLevelDeclarations)[program.TopLevelDeclarations.Count - 1]).tok.IsValid);
- }
-
- #endregion
}
}
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 021897f0..39343e6f 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -979,21 +979,43 @@ namespace Microsoft.Boogie { }
}
- // Look for {:name true} or {:name false} in list of attributes. Return result in 'result'
- // (which is not touched if there is no attribute specified).
- //
- // Returns false is there was an error processing the flag, true otherwise.
+ /// <summary>
+ /// If the declaration has an attribute {:name} or {:name true}, then set "result" to "true" and return "true".
+ /// If the declaration has an attribute {:name false}, then set "result" to "false" and return "true".
+ /// Otherwise, return "false" and leave "result" unchanged (which gives the caller an easy way to indicate
+ /// a default value if the attribute is not mentioned).
+ /// If there is more than one attribute called :name, then the last attribute rules.
+ /// </summary>
public bool CheckBooleanAttribute(string name, ref bool result) {
Contract.Requires(name != null);
- Expr expr = FindExprAttribute(name);
- if (expr != null) {
- if (expr is LiteralExpr && ((LiteralExpr)expr).isBool) {
- result = ((LiteralExpr)expr).asBool;
- } else {
- return false;
+ var kv = FindAttribute(name);
+ if (kv != null) {
+ if (kv.Params.Count == 0) {
+ result = true;
+ return true;
+ } else if (kv.Params.Count == 1) {
+ var lit = kv.Params[0] as LiteralExpr;
+ if (lit != null && lit.isBool) {
+ result = lit.asBool;
+ return true;
+ }
}
}
- return true;
+ return false;
+ }
+
+ /// <summary>
+ /// Find and return the last occurrence of an attribute with the name "name", if any. If none, return null.
+ /// </summary>
+ public QKeyValue FindAttribute(string name) {
+ Contract.Requires(name != null);
+ QKeyValue res = null;
+ for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next) {
+ if (kv.Key == name) {
+ res = kv;
+ }
+ }
+ return res;
}
// Look for {:name expr} in list of attributes.
@@ -1802,6 +1824,8 @@ namespace Microsoft.Boogie { }
}
+ public string DependenciesChecksum { get; set; }
+
protected void EmitSignature(TokenTextWriter stream, bool shortRet) {
Contract.Requires(stream != null);
Type.EmitOptionalTypeParams(stream, TypeParameters);
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index cea7d4c4..df49740e 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -399,6 +399,7 @@ namespace Microsoft.Boogie { public int StagedHoudini = 0;
public bool DebugStagedHoudini = false;
public bool StagedHoudiniReachabilityAnalysis = false;
+ public bool StagedHoudiniMergeIgnoredCandidates = false;
public string VariableDependenceIgnore = null;
public string AbstractHoudini = null;
public bool UseUnsatCoreForContractInfer = false;
@@ -889,7 +890,7 @@ namespace Microsoft.Boogie { case "stagedHoudini": {
int sh = 0;
- if (ps.GetNumericArgument(ref sh, 3)) {
+ if (ps.GetNumericArgument(ref sh, 4)) {
StagedHoudini = sh;
}
return true;
@@ -902,6 +903,13 @@ namespace Microsoft.Boogie { return true;
}
+ case "stagedHoudiniMergeIgnoredCandidates": {
+ if (ps.ConfirmArgumentCount(0)) {
+ StagedHoudiniMergeIgnoredCandidates = true;
+ }
+ return true;
+ }
+
case "debugStagedHoudini": {
if (ps.ConfirmArgumentCount(0)) {
DebugStagedHoudini = true;
@@ -1450,6 +1458,9 @@ namespace Microsoft.Boogie { one of them to keep; otherwise, Boogie ignore the :extern declaration
and keeps the other.
+ {:checksum <string>}
+ Attach a checksum to be used for verification result caching.
+
---- On implementations and procedures -------------------------------------
{:inline N}
@@ -1477,6 +1488,14 @@ namespace Microsoft.Boogie { of ""assume false;"": the first one disables all verification before
it, and the second one disables all verification after.
+ {:priority N}
+ Assign a positive priority 'N' to an implementation to control the order
+ in which implementations are verified (default: N = 1).
+
+ {:id <string>}
+ Assign a unique ID to an implementation to be used for verification
+ result caching (default: ""<impl. name>:0"").
+
---- On functions ----------------------------------------------------------
{:builtin ""spec""}
@@ -1494,6 +1513,14 @@ namespace Microsoft.Boogie { trigger annotations. Internally it works by adding {:nopats ...}
annotations to quantifiers.
+ {:identity}
+ {:identity true}
+ If the function has 1 argument and the use of it has type X->X for
+ some X, then the abstract interpreter will treat the function as an
+ identity function. Note, the abstract interpreter trusts the
+ attribute--it does not try to verify that the function really is an
+ identity function.
+
---- On variables ----------------------------------------------------------
{:existential true}
@@ -1618,6 +1645,9 @@ namespace Microsoft.Boogie { 1 = perform live variable analysis (default)
2 = perform interprocedural live variable analysis
/noVerify skip VC generation and invocation of the theorem prover
+ /verifySnapshots
+ verify several program snapshots (named <filename>.v0.bpl
+ to <filename>.vN.bpl) using verification result caching
/removeEmptyBlocks:<c>
0 - do not remove empty blocks during VC generation
1 - remove empty blocks (default)
diff --git a/Source/Core/VariableDependenceAnalyser.cs b/Source/Core/VariableDependenceAnalyser.cs index e48ec90f..fd69d911 100644 --- a/Source/Core/VariableDependenceAnalyser.cs +++ b/Source/Core/VariableDependenceAnalyser.cs @@ -17,6 +17,7 @@ namespace Microsoft.Boogie { void dump();
void ShowDependencyChain(VariableDescriptor source, VariableDescriptor target);
bool VariableRelevantToAnalysis(Variable v, string proc);
+ bool Ignoring(Variable v, string proc);
}
@@ -209,7 +210,7 @@ namespace Microsoft.Boogie { Console.Write(v);
}
}
- Console.WriteLine("\n");
+ Console.WriteLine(); Console.WriteLine();
}
public void Analyse() {
@@ -380,27 +381,28 @@ namespace Microsoft.Boogie { private HashSet<VariableDescriptor> IgnoredVariables = null;
- public bool VariableRelevantToAnalysis(Variable v, string proc) {
- if (v is Constant) {
- return false;
- }
+ public bool Ignoring(Variable v, string proc) {
if (IgnoredVariables == null) {
MakeIgnoreList();
}
if(proc != null && IgnoredVariables.Contains(new LocalDescriptor(proc, v.Name))) {
- return false;
+ return true;
}
if(IgnoredVariables.Contains(new GlobalDescriptor(v.Name))) {
- return false;
+ return true;
}
- return true;
+ return false;
}
+ public bool VariableRelevantToAnalysis(Variable v, string proc) {
+ return !(v is Constant || Ignoring(v, proc));
+ }
+
private void MakeIgnoreList()
{
IgnoredVariables = new HashSet<VariableDescriptor>();
diff --git a/Source/Doomed/DoomCheck.cs b/Source/Doomed/DoomCheck.cs index 1cbbeabf..7e2ec984 100644 --- a/Source/Doomed/DoomCheck.cs +++ b/Source/Doomed/DoomCheck.cs @@ -117,10 +117,11 @@ void ObjectInvariant() outcome = ProverInterface.Outcome.Undetermined;
Contract.Assert( m_ErrorHandler !=null);
m_Checker.BeginCheck(lv[0].Name, vc, m_ErrorHandler);
- m_Checker.ProverDone.WaitOne();
+ m_Checker.ProverTask.Wait();
try {
outcome = m_Checker.ReadOutcome();
+ m_Checker.GoBackToIdle();
} catch (UnexpectedProverOutputException e)
{
if (CommandLineOptions.Clo.TraceVerify) {
diff --git a/Source/Doomed/VCDoomed.cs b/Source/Doomed/VCDoomed.cs index fadb2ea7..778ae767 100644 --- a/Source/Doomed/VCDoomed.cs +++ b/Source/Doomed/VCDoomed.cs @@ -34,8 +34,8 @@ namespace VC { /// <summary>
/// Constructor. Initializes the theorem prover.
/// </summary>
- public DCGen(Program program, string/*?*/ logFilePath, bool appendLogFile)
- : base(program) {
+ public DCGen(Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers)
+ : base(program, checkers) {
Contract.Requires(program != null);
this.appendLogFile = appendLogFile;
@@ -115,7 +115,7 @@ namespace VC { //Impl2Dot(impl, String.Format("c:/dot/{0}_fin.dot", impl.Name));
- Checker checker = FindCheckerFor(impl, 1000);
+ Checker checker = FindCheckerFor(1000);
Contract.Assert(checker != null);
int assertionCount;
DoomCheck dc = new DoomCheck(impl, this.exitBlock, checker, m_UncheckableBlocks, out assertionCount);
@@ -173,7 +173,7 @@ namespace VC { if (restartTP)
{
checker.Close();
- checker = FindCheckerFor(impl, 1000);
+ checker = FindCheckerFor(1000);
dc.RespawnChecker(impl, checker);
dc.ErrorHandler = new DoomErrorHandler(dc.Label2Absy, callback);
}
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 110480b9..21d0c014 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -5,6 +5,8 @@ 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;
@@ -16,23 +18,24 @@ namespace Microsoft.Boogie public interface OutputPrinter
{
- void ErrorWriteLine(string s);
- void ErrorWriteLine(string format, params object[] args);
+ void ErrorWriteLine(TextWriter tw, string s);
+ void ErrorWriteLine(TextWriter tw, string format, params object[] args);
void AdvisoryWriteLine(string format, params object[] args);
- void Inform(string s);
- void WriteTrailer(int verified, int errors, int inconclusives, int timeOuts, int outOfMemories);
- void ReportBplError(IToken tok, string message, bool error, bool showBplLocation);
+ 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(string s)
+ public void ErrorWriteLine(TextWriter tw, string s)
{
Contract.Requires(s != null);
if (!s.Contains("Error: ") && !s.Contains("Error BP"))
{
- Console.WriteLine(s);
+ tw.WriteLine(s);
return;
}
@@ -51,21 +54,21 @@ namespace Microsoft.Boogie ConsoleColor col = Console.ForegroundColor;
Console.ForegroundColor = ConsoleColor.Red;
- Console.WriteLine(s);
+ tw.WriteLine(s);
Console.ForegroundColor = col;
if (remaining != null)
{
- Console.WriteLine(remaining);
+ tw.WriteLine(remaining);
}
}
- public void ErrorWriteLine(string format, params object[] args)
+ public void ErrorWriteLine(TextWriter tw, string format, params object[] args)
{
Contract.Requires(format != null);
string s = string.Format(format, args);
- ErrorWriteLine(s);
+ ErrorWriteLine(tw, s);
}
@@ -83,49 +86,75 @@ namespace Microsoft.Boogie /// Inform the user about something and proceed with translation normally.
/// Print newline after the message.
/// </summary>
- public void Inform(string s)
+ public void Inform(string s, TextWriter tw)
{
if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.TraceProofObligations)
{
- Console.WriteLine(s);
+ tw.WriteLine(s);
}
}
- public void WriteTrailer(int verified, int errors, int inconclusives, int timeOuts, int outOfMemories)
+ public void WriteTrailer(PipelineStatistics stats)
{
- Contract.Requires(0 <= errors && 0 <= inconclusives && 0 <= timeOuts && 0 <= outOfMemories);
+ 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, verified, errors, errors == 1 ? "" : "s");
+ 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, verified, errors, errors == 1 ? "" : "s");
+ Console.Write("{0} finished with {1} verified, {2} error{3}", CommandLineOptions.Clo.DescriptiveToolName, stats.VerifiedCount, stats.ErrorCount, stats.ErrorCount == 1 ? "" : "s");
}
- if (inconclusives != 0)
+ if (stats.InconclusiveCount != 0)
{
- Console.Write(", {0} inconclusive{1}", inconclusives, inconclusives == 1 ? "" : "s");
+ Console.Write(", {0} inconclusive{1}", stats.InconclusiveCount, stats.InconclusiveCount == 1 ? "" : "s");
}
- if (timeOuts != 0)
+ if (stats.TimeoutCount != 0)
{
- Console.Write(", {0} time out{1}", timeOuts, timeOuts == 1 ? "" : "s");
+ Console.Write(", {0} time out{1}", stats.TimeoutCount, stats.TimeoutCount == 1 ? "" : "s");
}
- if (outOfMemories != 0)
+ if (stats.OutOfMemoryCount != 0)
{
- Console.Write(", {0} out of memory", outOfMemories);
+ Console.Write(", {0} out of memory", stats.OutOfMemoryCount);
}
Console.WriteLine();
Console.Out.Flush();
}
- public virtual void ReportBplError(IToken tok, string message, bool error, bool showBplLocation)
+ 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.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 && showBplLocation)
+ if (tok != null)
{
s = string.Format("{0}({1},{2}): {3}", tok.filename, tok.line, tok.col, message);
}
@@ -135,11 +164,11 @@ namespace Microsoft.Boogie }
if (error)
{
- ErrorWriteLine(s);
+ ErrorWriteLine(tw, s);
}
else
{
- Console.WriteLine(s);
+ tw.WriteLine(s);
}
}
}
@@ -158,40 +187,87 @@ namespace Microsoft.Boogie }
+ public class PipelineStatistics
+ {
+ public int ErrorCount;
+ public int VerifiedCount;
+ public int InconclusiveCount;
+ public int TimeoutCount;
+ public int OutOfMemoryCount;
+ }
+
+
#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)
+ public virtual ErrorInformation CreateErrorInformation(IToken tok, string msg, string requestId = null, string category = null)
{
- Contract.Requires(tok != null);
Contract.Requires(1 <= tok.line && 1 <= tok.col);
Contract.Requires(msg != null);
- return ErrorInformation.CreateErrorInformation(tok, msg, requestId);
+ return ErrorInformation.CreateErrorInformation(tok, msg, requestId, category);
}
}
public class ErrorInformation
{
- public IToken Tok;
+ 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 RequestId { get; set; }
+ public ErrorKind Kind { get; set; }
+ public string ImplementationName { get; set; }
+ public TextWriter Out = 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 AuxErrorInfo(IToken tok, string msg)
+ 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;
}
}
@@ -205,19 +281,20 @@ namespace Microsoft.Boogie Msg = CleanUp(msg);
}
- internal static ErrorInformation CreateErrorInformation(IToken tok, string msg, string requestId = null)
+ internal static ErrorInformation CreateErrorInformation(IToken tok, string msg, string requestId = null, string category = null)
{
var result = new ErrorInformation(tok, msg);
result.RequestId = requestId;
+ result.Category = category;
return result;
}
- public virtual void AddAuxInfo(IToken tok, string msg)
+ 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));
+ Aux.Add(new AuxErrorInfo(tok, msg, category));
}
protected static string CleanUp(string msg)
@@ -236,6 +313,41 @@ namespace Microsoft.Boogie #endregion
+ public class VerificationResult
+ {
+ public readonly string Checksum;
+ public readonly string DependeciesChecksum;
+ public readonly string RequestId;
+
+ 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;
+ public List<Counterexample> Errors;
+
+ public string ImplementationName { get; set; }
+ public IToken ImplementationToken { get; set; }
+
+ public VerificationResult(string requestId, string checksum, string depsChecksum, ConditionGeneration.Outcome outcome, List<Counterexample> errors)
+ : this(requestId, checksum, depsChecksum)
+ {
+ Outcome = outcome;
+ Errors = errors;
+ }
+
+ public VerificationResult(string requestId, string checksum, string depsChecksum)
+ {
+ Checksum = checksum;
+ DependeciesChecksum = depsChecksum;
+ RequestId = requestId;
+ }
+ }
+
+
public class ExecutionEngine
{
public static OutputPrinter printer;
@@ -284,7 +396,6 @@ namespace Microsoft.Boogie using (XmlFileScope xf = new XmlFileScope(CommandLineOptions.Clo.XmlSink, fileNames[fileNames.Count - 1]))
{
- //BoogiePL.Errors.count = 0;
Program program = ParseBoogieProgram(fileNames, false);
if (program == null)
return;
@@ -296,7 +407,6 @@ namespace Microsoft.Boogie PipelineOutcome oc = ResolveAndTypecheck(program, fileNames[fileNames.Count - 1]);
if (oc != PipelineOutcome.ResolvedAndTypeChecked)
return;
- //BoogiePL.Errors.count = 0;
// Do bitvector analysis
if (CommandLineOptions.Clo.DoBitVectorAnalysis)
@@ -346,13 +456,13 @@ namespace Microsoft.Boogie }
}
- int errorCount, verified, inconclusives, timeOuts, outOfMemories;
- oc = InferAndVerify(program, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories);
+ var stats = new PipelineStatistics();
+ oc = InferAndVerify(program, stats);
switch (oc)
{
case PipelineOutcome.Done:
case PipelineOutcome.VerificationCompleted:
- printer.WriteTrailer(verified, errorCount, inconclusives, timeOuts, outOfMemories);
+ printer.WriteTrailer(stats);
break;
default:
break;
@@ -393,7 +503,7 @@ namespace Microsoft.Boogie public static Program ParseBoogieProgram(List<string> fileNames, bool suppressTraceOutput)
{
Contract.Requires(cce.NonNullElements(fileNames));
- //BoogiePL.Errors.count = 0;
+
Program program = null;
bool okay = true;
for (int fileId = 0; fileId < fileNames.Count; fileId++)
@@ -426,7 +536,7 @@ namespace Microsoft.Boogie }
catch (IOException e)
{
- printer.ErrorWriteLine("Error opening file \"{0}\": {1}", bplFileName, e.Message);
+ printer.ErrorWriteLine(Console.Out, "Error opening file \"{0}\": {1}", bplFileName, e.Message);
okay = false;
continue;
}
@@ -551,31 +661,22 @@ namespace Microsoft.Boogie }
if (inline)
{
- foreach (var d in TopLevelDeclarations)
+ foreach (var impl in TopLevelDeclarations.OfType<Implementation>())
{
- var impl = d as Implementation;
- if (impl != null)
- {
- impl.OriginalBlocks = impl.Blocks;
- impl.OriginalLocVars = impl.LocVars;
- }
+ impl.OriginalBlocks = impl.Blocks;
+ impl.OriginalLocVars = impl.LocVars;
}
- foreach (var d in TopLevelDeclarations)
+ foreach (var impl in TopLevelDeclarations.OfType<Implementation>())
{
- var impl = d as Implementation;
- if (impl != null && !impl.SkipVerification)
+ if (!impl.SkipVerification)
{
Inliner.ProcessImplementation(program, impl);
}
}
- foreach (var d in TopLevelDeclarations)
+ foreach (var impl in TopLevelDeclarations.OfType<Implementation>())
{
- var impl = d as Implementation;
- if (impl != null)
- {
- impl.OriginalBlocks = null;
- impl.OriginalLocVars = null;
- }
+ impl.OriginalBlocks = null;
+ impl.OriginalLocVars = null;
}
}
}
@@ -591,17 +692,16 @@ namespace Microsoft.Boogie /// parameters contain meaningful values
/// </summary>
public static PipelineOutcome InferAndVerify(Program program,
- out int errorCount, out int verified, out int inconclusives, out int timeOuts, out int outOfMemories,
+ PipelineStatistics stats,
ErrorReporterDelegate er = null, string requestId = null)
{
Contract.Requires(program != null);
- Contract.Ensures(0 <= Contract.ValueAtReturn(out inconclusives) && 0 <= Contract.ValueAtReturn(out timeOuts));
-
- errorCount = verified = inconclusives = timeOuts = outOfMemories = 0;
+ Contract.Requires(stats != null);
+ Contract.Ensures(0 <= Contract.ValueAtReturn(out stats.InconclusiveCount) && 0 <= Contract.ValueAtReturn(out stats.TimeoutCount));
- // ---------- Infer invariants --------------------------------------------------------
+ #region Infer invariants using Abstract Interpretation
- // Abstract interpretation -> Always use (at least) intervals, if not specified otherwise (e.g. with the "/noinfer" switch)
+ // 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)
@@ -612,6 +712,10 @@ namespace Microsoft.Boogie }
Microsoft.Boogie.AbstractInterpretation.NativeAbstractInterpretation.RunAbstractInterpretation(program);
+ #endregion
+
+ #region Do some preprocessing on the program (e.g., loop unrolling, lambda expansion)
+
if (CommandLineOptions.Clo.LoopUnrollCount != -1)
{
program.UnrollLoops(CommandLineOptions.Clo.LoopUnrollCount, CommandLineOptions.Clo.SoundLoopUnrolling);
@@ -634,7 +738,7 @@ namespace Microsoft.Boogie //PrintBplFile ("-", program, true);
}
- // ---------- Verify ------------------------------------------------------------
+ #endregion
if (!CommandLineOptions.Clo.Verify)
{
@@ -644,453 +748,666 @@ namespace Microsoft.Boogie #region Run Houdini and verify
if (CommandLineOptions.Clo.ContractInfer)
{
- if (CommandLineOptions.Clo.AbstractHoudini != null)
- {
- //CommandLineOptions.Clo.PrintErrorModel = 1;
- CommandLineOptions.Clo.UseProverEvaluate = true;
- CommandLineOptions.Clo.ModelViewFile = "z3model";
- CommandLineOptions.Clo.UseArrayTheory = true;
- CommandLineOptions.Clo.TypeEncodingMethod = CommandLineOptions.TypeEncoding.Monomorphic;
- Houdini.AbstractDomainFactory.Initialize();
- var domain = Houdini.AbstractDomainFactory.GetInstance(CommandLineOptions.Clo.AbstractHoudini);
-
- // Run Abstract Houdini
- var abs = new Houdini.AbsHoudini(program, domain);
- var absout = abs.ComputeSummaries();
- ProcessOutcome(absout.outcome, absout.errors, "", ref errorCount, ref verified, ref inconclusives, ref timeOuts, ref outOfMemories, 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;
- }
- Houdini.Houdini houdini = new Houdini.Houdini(program);
- Houdini.HoudiniOutcome outcome = houdini.PerformHoudiniInference();
- if (CommandLineOptions.Clo.PrintAssignment)
- {
- Console.WriteLine("Assignment computed by Houdini:");
- foreach (var x in outcome.assignment)
- {
- Console.WriteLine(x.Key + " = " + x.Value);
- }
- }
- if (CommandLineOptions.Clo.Trace)
- {
- int numTrueAssigns = 0;
- foreach (var x in outcome.assignment)
- {
- if (x.Value)
- numTrueAssigns++;
- }
- Console.WriteLine("Number of true assignments = " + numTrueAssigns);
- Console.WriteLine("Number of false assignments = " + (outcome.assignment.Count - numTrueAssigns));
- Console.WriteLine("Prover time = " + Houdini.HoudiniSession.proverTime.ToString("F2"));
- Console.WriteLine("Unsat core prover time = " + Houdini.HoudiniSession.unsatCoreProverTime.ToString("F2"));
- Console.WriteLine("Number of prover queries = " + Houdini.HoudiniSession.numProverQueries);
- Console.WriteLine("Number of unsat core prover queries = " + Houdini.HoudiniSession.numUnsatCoreProverQueries);
- Console.WriteLine("Number of unsat core prunings = " + Houdini.HoudiniSession.numUnsatCorePrunings);
- }
-
- foreach (Houdini.VCGenOutcome x in outcome.implementationOutcomes.Values)
- {
- ProcessOutcome(x.outcome, x.errors, "", ref errorCount, ref verified, ref inconclusives, ref timeOuts, ref outOfMemories, er);
- }
- //errorCount = outcome.ErrorCount;
- //verified = outcome.Verified;
- //inconclusives = outcome.Inconclusives;
- //timeOuts = outcome.TimeOuts;
- //outOfMemories = 0;
- return PipelineOutcome.Done;
+ return RunHoudini(program, stats, er);
}
#endregion
- #region Verify each implementation
+ #region Select and prioritize implementations that should be verified
- ConditionGeneration vcgen = null;
- try
+ var impls = program.TopLevelDeclarations.OfType<Implementation>().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 (CommandLineOptions.Clo.VerifySnapshots)
{
- if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed)
- {
- vcgen = new DCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
- }
- else if (CommandLineOptions.Clo.FixedPointEngine != null)
- {
- vcgen = new FixedpointVC(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
- }
- else if (CommandLineOptions.Clo.StratifiedInlining > 0)
- {
- vcgen = new StratifiedVCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
- }
- else
- {
- vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
- }
+ impls.Iter(impl => { impl.DependenciesChecksum = DependencyCollector.DependenciesChecksum(impl); });
+ stablePrioritizedImpls = impls.OrderByDescending(
+ impl => impl.Priority != 1 ? impl.Priority : Cache.VerificationPriority(impl)).ToArray();
}
- catch (ProverException e)
+ else
{
- printer.ErrorWriteLine("Fatal Error: ProverException: {0}", e);
- return PipelineOutcome.FatalError;
+ stablePrioritizedImpls = impls.OrderByDescending(impl => impl.Priority).ToArray();
}
- // operate on a stable copy, in case it gets updated while we're running
- var decls = program.TopLevelDeclarations.ToArray();
-
- var impls =
- from d in decls
- where d != null && d is Implementation && CommandLineOptions.Clo.UserWantsToCheckRoutine(cce.NonNull(((Implementation)d).Name)) && !((Implementation)d).SkipVerification
- select (Implementation)d;
+ #endregion
- var prioritizedImpls =
- from i in impls
- orderby i.Priority descending
- select i;
+ #region Verify each implementation
- foreach (var impl in prioritizedImpls)
+ var outputCollector = new OutputCollector(stablePrioritizedImpls);
+ var outcome = PipelineOutcome.VerificationCompleted;
+ var checkers = new List<Checker>();
+ var tasks = new Task[stablePrioritizedImpls.Length];
+ for (int i = 0; i < stablePrioritizedImpls.Length && outcome != PipelineOutcome.FatalError; i++)
{
- int prevAssertionCount = vcgen.CumulativeAssertionCount;
- List<Counterexample/*!*/>/*?*/ errors;
-
- DateTime start = new DateTime(); // to please compiler's definite assignment rules
- if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.TraceProofObligations || CommandLineOptions.Clo.XmlSink != null)
+ var taskIndex = i;
+ var t = Task.Factory.StartNew(() =>
{
- start = DateTime.UtcNow;
- if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.TraceProofObligations)
+ VerifyImplementation(program, stats, er, requestId, extractLoopMappingInfo, stablePrioritizedImpls, taskIndex, outputCollector, checkers);
+ }, TaskCreationOptions.LongRunning);
+ tasks[taskIndex] = t;
+ }
+ try
+ {
+ Task.WaitAll(tasks);
+ }
+ catch (AggregateException ae)
+ {
+ ae.Handle(e =>
+ {
+ var pe = e as ProverException;
+ if (pe != null)
{
- Console.WriteLine();
- Console.WriteLine("Verifying {0} ...", impl.Name);
+ printer.ErrorWriteLine(Console.Out, "Fatal Error: ProverException: {0}", e);
+ outcome = PipelineOutcome.FatalError;
+ return true;
}
- if (CommandLineOptions.Clo.XmlSink != null)
+ return false;
+ });
+ }
+ finally
+ {
+ lock (checkers)
+ {
+ foreach (Checker checker in checkers)
{
- CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, start);
+ Contract.Assert(checker != null);
+ checker.Close();
}
}
+ }
+
+ cce.NonNull(CommandLineOptions.Clo.TheProverFactory).Close();
+
+ outputCollector.WriteMoreOutput();
+
+ #endregion
+
+ return outcome;
+ }
+
+
+ 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)
+ {
+ Implementation impl = stablePrioritizedImpls[index];
+ VerificationResult verificationResult = null;
+ var output = new StringWriter();
+
+ printer.Inform("", output); // newline
+ printer.Inform(string.Format("Verifying {0} ...", impl.Name), output);
- VCGen.Outcome outcome;
- string depsChecksum = null;
- if (CommandLineOptions.Clo.VerifySnapshots)
+ if (CommandLineOptions.Clo.VerifySnapshots)
+ {
+ verificationResult = Cache.Lookup(impl);
+ }
+
+ if (verificationResult != null)
+ {
+ if (CommandLineOptions.Clo.XmlSink != null)
{
- depsChecksum = DependencyCollector.DependenciesChecksum(impl);
+ CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, verificationResult.Start);
}
- try
+
+ printer.Inform(string.Format("Retrieving cached verification result for implementation {0}...", impl.Name), output);
+ }
+ else
+ {
+ #region Verify the implementation
+
+ verificationResult = new VerificationResult(requestId, impl.Checksum, impl.DependenciesChecksum);
+ verificationResult.ImplementationName = impl.Name;
+ verificationResult.ImplementationToken = impl.tok;
+
+ using (var vcgen = CreateVCGen(program, checkers))
{
- if (CommandLineOptions.Clo.inferLeastForUnsat != null)
+ verificationResult.ProofObligationCountBefore = vcgen.CumulativeAssertionCount;
+ verificationResult.Start = DateTime.UtcNow;
+
+ if (CommandLineOptions.Clo.XmlSink != null)
{
- var svcgen = vcgen as VC.StratifiedVCGen;
- Contract.Assert(svcgen != null);
- var ss = new HashSet<string>();
- foreach (var tdecl in program.TopLevelDeclarations)
- {
- var c = tdecl as Constant;
- if (c == null || !c.Name.StartsWith(CommandLineOptions.Clo.inferLeastForUnsat)) continue;
- ss.Add(c.Name);
- }
- outcome = svcgen.FindLeastToVerify(impl, ref ss);
- errors = new List<Counterexample>();
- Console.Write("Result: ");
- foreach (var s in ss)
- {
- Console.Write("{0} ", s);
- }
- Console.WriteLine();
+ CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, verificationResult.Start);
}
- else
+ try
{
- if (!CommandLineOptions.Clo.VerifySnapshots || Cache.NeedsToBeVerified(impl))
+ if (CommandLineOptions.Clo.inferLeastForUnsat != null)
{
- outcome = vcgen.VerifyImplementation(impl, out errors, requestId);
+ var svcgen = vcgen as VC.StratifiedVCGen;
+ Contract.Assert(svcgen != null);
+ var ss = new HashSet<string>();
+ foreach (var tdecl in program.TopLevelDeclarations)
+ {
+ var c = tdecl as Constant;
+ if (c == null || !c.Name.StartsWith(CommandLineOptions.Clo.inferLeastForUnsat)) continue;
+ ss.Add(c.Name);
+ }
+ verificationResult.Outcome = svcgen.FindLeastToVerify(impl, ref ss);
+ verificationResult.Errors = new List<Counterexample>();
+ output.WriteLine("Result: {0}", string.Join(" ", ss));
}
else
{
- if (CommandLineOptions.Clo.Trace)
+ verificationResult.Outcome = vcgen.VerifyImplementation(impl, out verificationResult.Errors, requestId);
+ if (CommandLineOptions.Clo.ExtractLoops && verificationResult.Errors != null)
{
- Console.WriteLine("Retrieving cached verification result for implementation {0}...", impl.Name);
+ 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);
+ }
+ }
}
- var result = Cache.Lookup(impl.Id);
- Contract.Assert(result != null);
- outcome = result.Outcome;
- errors = result.Errors;
}
- if (CommandLineOptions.Clo.ExtractLoops && vcgen is VCGen && errors != null)
+ }
+ 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)
{
- for (int i = 0; i < errors.Count; i++)
+ lock (er)
{
- errors[i] = (vcgen as VCGen).extractLoopTrace(errors[i], impl.Name, program, extractLoopMappingInfo);
+ er(errorInfo);
}
}
+ verificationResult.Errors = null;
+ verificationResult.Outcome = VCGen.Outcome.Inconclusive;
}
- }
- catch (VCGenException e)
- {
- printer.ReportBplError(impl.tok, String.Format("Error BP5010: {0} Encountered in implementation {1}.", e.Message, impl.Name), true, true);
- errors = null;
- outcome = VCGen.Outcome.Inconclusive;
- }
- catch (UnexpectedProverOutputException upo)
- {
- printer.AdvisoryWriteLine("Advisory: {0} SKIPPED because of internal error: unexpected prover output: {1}", impl.Name, upo.Message);
- errors = null;
- outcome = VCGen.Outcome.Inconclusive;
+ 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;
}
- string timeIndication = "";
- DateTime end = DateTime.UtcNow;
- TimeSpan elapsed = end - start;
- if (CommandLineOptions.Clo.Trace)
+ #endregion
+
+ #region Cache the verification result
+
+ if (CommandLineOptions.Clo.VerifySnapshots && !string.IsNullOrEmpty(impl.Checksum))
{
- int poCount = vcgen.CumulativeAssertionCount - prevAssertionCount;
- timeIndication = string.Format(" [{0:F3} s, {1} proof obligation{2}] ", elapsed.TotalSeconds, poCount, poCount == 1 ? "" : "s");
+ Cache.Insert(impl.Id, verificationResult);
}
- else if (CommandLineOptions.Clo.TraceProofObligations)
+
+ #endregion
+ }
+
+ #region Process the verification results and statistics
+
+ ProcessOutcome(verificationResult.Outcome, verificationResult.Errors, TimeIndication(verificationResult), stats, output, er, verificationResult.ImplementationName, verificationResult.ImplementationToken, verificationResult.RequestId);
+
+ 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)
{
- int poCount = vcgen.CumulativeAssertionCount - prevAssertionCount;
- timeIndication = string.Format(" [{0} proof obligation{1}] ", poCount, poCount == 1 ? "" : "s");
+ for (; nextPrintableIndex < outputs.Count() && outputs[nextPrintableIndex] != null; nextPrintableIndex++)
+ {
+ Console.Write(outputs[nextPrintableIndex].ToString());
+ Console.Out.Flush();
+ }
}
+ }
- if (CommandLineOptions.Clo.VerifySnapshots && !string.IsNullOrEmpty(impl.Checksum))
+ public void Add(int index, StringWriter output)
+ {
+ Contract.Requires(0 <= index && index < outputs.Length);
+ Contract.Requires(output != null);
+
+ lock (this)
{
- var result = new VerificationResult(requestId, impl.Checksum, depsChecksum, outcome, errors);
- Cache.Insert(impl.Id, result);
+ outputs[index] = output;
}
+ }
+ }
- ProcessOutcome(outcome, errors, timeIndication, ref errorCount, ref verified, ref inconclusives, ref timeOuts, ref outOfMemories, er, impl, requestId);
- if (CommandLineOptions.Clo.XmlSink != null)
+ 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
+ {
+ 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);
+ }
+
+ Houdini.Houdini houdini = new Houdini.Houdini(program);
+ Houdini.HoudiniOutcome outcome = houdini.PerformHoudiniInference();
+
+ if (CommandLineOptions.Clo.PrintAssignment)
+ {
+ Console.WriteLine("Assignment computed by Houdini:");
+ foreach (var x in outcome.assignment)
{
- CommandLineOptions.Clo.XmlSink.WriteEndMethod(outcome.ToString().ToLowerInvariant(), end, elapsed);
+ Console.WriteLine(x.Key + " = " + x.Value);
}
- if (outcome == VCGen.Outcome.Errors || CommandLineOptions.Clo.Trace)
+ }
+
+ if (CommandLineOptions.Clo.Trace)
+ {
+ int numTrueAssigns = 0;
+ foreach (var x in outcome.assignment)
{
- Console.Out.Flush();
+ if (x.Value)
+ numTrueAssigns++;
}
+ Console.WriteLine("Number of true assignments = " + numTrueAssigns);
+ Console.WriteLine("Number of false assignments = " + (outcome.assignment.Count - numTrueAssigns));
+ Console.WriteLine("Prover time = " + Houdini.HoudiniSession.proverTime.ToString("F2"));
+ Console.WriteLine("Unsat core prover time = " + Houdini.HoudiniSession.unsatCoreProverTime.ToString("F2"));
+ Console.WriteLine("Number of prover queries = " + Houdini.HoudiniSession.numProverQueries);
+ Console.WriteLine("Number of unsat core prover queries = " + Houdini.HoudiniSession.numUnsatCoreProverQueries);
+ Console.WriteLine("Number of unsat core prunings = " + Houdini.HoudiniSession.numUnsatCorePrunings);
}
- vcgen.Close();
- cce.NonNull(CommandLineOptions.Clo.TheProverFactory).Close();
+ foreach (Houdini.VCGenOutcome x in outcome.implementationOutcomes.Values)
+ {
+ ProcessOutcome(x.outcome, x.errors, "", stats, Console.Out, er);
+ ProcessErrors(x.errors, x.outcome, Console.Out, er);
+ }
+ //errorCount = outcome.ErrorCount;
+ //verified = outcome.Verified;
+ //inconclusives = outcome.Inconclusives;
+ //timeOuts = outcome.TimeOuts;
+ //outOfMemories = 0;
+ return PipelineOutcome.Done;
+ }
- #endregion
- return PipelineOutcome.VerificationCompleted;
+ 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, 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, ErrorReporterDelegate er = null, string implName = null, IToken implTok = null, string requestId = null)
+ {
+ Contract.Requires(stats != null);
+
+ UpdateStatistics(stats, outcome, errors);
+
+ printer.Inform(timeIndication + OutcomeIndication(outcome, errors), tw);
+
+ ReportOutcome(outcome, er, implName, implTok, requestId, tw);
}
- static void ProcessOutcome(VC.VCGen.Outcome outcome, List<Counterexample> errors, string timeIndication,
- ref int errorCount, ref int verified, ref int inconclusives, ref int timeOuts, ref int outOfMemories, ErrorReporterDelegate er = null, Implementation impl = null, string requestId = null)
+ private static void ReportOutcome(VC.VCGen.Outcome outcome, ErrorReporterDelegate er, string implName, IToken implTok, string requestId, TextWriter tw)
{
+ ErrorInformation errorInfo = null;
+
switch (outcome)
{
- default:
- Contract.Assert(false); // unexpected outcome
- throw new cce.UnreachableException();
case VCGen.Outcome.ReachedBound:
- printer.Inform(String.Format("{0}verified", timeIndication));
- Console.WriteLine(string.Format("Stratified Inlining: Reached recursion bound of {0}", CommandLineOptions.Clo.RecursionBound));
- verified++;
+ tw.WriteLine(string.Format("Stratified Inlining: Reached recursion bound of {0}", CommandLineOptions.Clo.RecursionBound));
break;
- case VCGen.Outcome.Correct:
- if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed)
+ case VCGen.Outcome.TimedOut:
+ if (implName != null && implTok != null)
{
- printer.Inform(String.Format("{0}credible", timeIndication));
- verified++;
+ errorInfo = errorInformationFactory.CreateErrorInformation(implTok, string.Format("Verification timed out after {0} seconds ({1})", CommandLineOptions.Clo.ProverKillTime, implName), requestId);
}
- else
+ break;
+ case VCGen.Outcome.OutOfMemory:
+ if (implName != null && implTok != null)
{
- printer.Inform(String.Format("{0}verified", timeIndication));
- verified++;
+ errorInfo = errorInformationFactory.CreateErrorInformation(implTok, "Verification out of memory (" + implName + ")", requestId);
}
break;
- case VCGen.Outcome.TimedOut:
- timeOuts++;
- printer.Inform(String.Format("{0}timed out", timeIndication));
- if (er != null && impl != null)
+ case VCGen.Outcome.Inconclusive:
+ if (implName != null && implTok != null)
{
- er(errorInformationFactory.CreateErrorInformation(impl.tok, string.Format("Verification timed out after {0} seconds ({1})", CommandLineOptions.Clo.ProverKillTime, impl.Name), requestId));
+ errorInfo = errorInformationFactory.CreateErrorInformation(implTok, "Verification inconclusive (" + implName + ")", requestId);
}
break;
- case VCGen.Outcome.OutOfMemory:
- outOfMemories++;
- printer.Inform(String.Format("{0}out of memory", timeIndication));
- if (er != null && impl != null)
+ }
+
+ if (errorInfo != null)
+ {
+ errorInfo.ImplementationName = implName;
+ if (er != null)
+ {
+ lock (er)
{
- er(errorInformationFactory.CreateErrorInformation(impl.tok, "Verification out of memory (" + impl.Name + ")", requestId));
+ 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:
- inconclusives++;
- printer.Inform(String.Format("{0}inconclusive", timeIndication));
- if (er != null && impl != null)
- {
- er(errorInformationFactory.CreateErrorInformation(impl.tok, "Verification inconclusive (" + impl.Name + ")", requestId));
- }
+ 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)
+ {
+ 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);
+ break;
+ case VCGen.Outcome.Correct:
+ Interlocked.Increment(ref stats.VerifiedCount);
+ break;
+ case VCGen.Outcome.TimedOut:
+ Interlocked.Increment(ref stats.TimeoutCount);
+ break;
+ case VCGen.Outcome.OutOfMemory:
+ Interlocked.Increment(ref stats.OutOfMemoryCount);
+ break;
+ case VCGen.Outcome.Inconclusive:
+ Interlocked.Increment(ref stats.InconclusiveCount);
break;
case VCGen.Outcome.Errors:
if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed)
{
- printer.Inform(String.Format("{0}doomed", timeIndication));
- errorCount++;
+ Interlocked.Increment(ref stats.ErrorCount);
+ }
+ else
+ {
+ Interlocked.Add(ref stats.ErrorCount, errors.Count);
}
- Contract.Assert(errors != null); // guaranteed by postcondition of VerifyImplementation
break;
}
- if (errors != null)
- {
- // BP1xxx: Parsing errors
- // BP2xxx: Name resolution errors
- // BP3xxx: Typechecking errors
- // BP4xxx: Abstract interpretation errors (Is there such a thing?)
- // BP5xxx: Verification errors
+ }
- var cause = "Error";
- if (outcome == VCGen.Outcome.TimedOut)
- {
- cause = "Timed out on";
- }
- else if (outcome == VCGen.Outcome.OutOfMemory)
- {
- cause = "Out of memory on";
- }
- // TODO(wuestholz): Take the error cause into account when writing to the XML sink.
+ 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)
{
- ErrorInformation errorInfo;
+ var errorInfo = CreateErrorInformation(error, outcome);
+ errorInfo.ImplementationName = implName;
- if (error is CallCounterexample)
+ if (CommandLineOptions.Clo.XmlSink != null)
{
- CallCounterexample err = (CallCounterexample)error;
- if (!CommandLineOptions.Clo.ForceBplErrors && err.FailingRequires.ErrorMessage != null)
- {
- printer.ReportBplError(err.FailingRequires.tok, err.FailingRequires.ErrorMessage, true, false);
- }
- else
- {
- printer.ReportBplError(err.FailingCall.tok, cause + " BP5002: A precondition for this call might not hold.", true, true);
- printer.ReportBplError(err.FailingRequires.tok, "Related location: This is the precondition that might not hold.", false, true);
- }
-
- errorInfo = errorInformationFactory.CreateErrorInformation(err.FailingCall.tok, cause + ": " + (err.FailingCall.ErrorData as string ?? "A precondition for this call might not hold."), err.RequestId);
- errorInfo.AddAuxInfo(err.FailingRequires.tok, err.FailingRequires.ErrorData as string ?? "Related location: This is the precondition that might not hold.");
+ WriteErrorInformationToXmlSink(errorInfo, error.Trace);
+ }
- if (CommandLineOptions.Clo.XmlSink != null)
+ if (CommandLineOptions.Clo.EnhancedErrorMessages == 1)
+ {
+ foreach (string info in error.relatedInformation)
{
- CommandLineOptions.Clo.XmlSink.WriteError("precondition violation", err.FailingCall.tok, err.FailingRequires.tok, error.Trace);
+ Contract.Assert(info != null);
+ errorInfo.Out.WriteLine(" " + info);
}
}
- else if (error is ReturnCounterexample)
+ if (CommandLineOptions.Clo.ErrorTrace > 0)
{
- ReturnCounterexample err = (ReturnCounterexample)error;
- if (!CommandLineOptions.Clo.ForceBplErrors && err.FailingEnsures.ErrorMessage != null)
- {
- printer.ReportBplError(err.FailingEnsures.tok, err.FailingEnsures.ErrorMessage, true, false);
- }
- else
- {
- printer.ReportBplError(err.FailingReturn.tok, cause + " BP5003: A postcondition might not hold on this return path.", true, true);
- printer.ReportBplError(err.FailingEnsures.tok, "Related location: This is the postcondition that might not hold.", false, true);
- }
+ 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.Out);
+ }
- errorInfo = errorInformationFactory.CreateErrorInformation(err.FailingReturn.tok, cause + ": " + "A postcondition might not hold on this return path.", err.RequestId);
- errorInfo.AddAuxInfo(err.FailingEnsures.tok, err.FailingEnsures.ErrorData as string ?? "Related location: This is the postcondition that might not hold.");
+ printer.WriteErrorInformation(errorInfo, tw);
- if (CommandLineOptions.Clo.XmlSink != null)
+ if (er != null)
+ {
+ lock (er)
{
- CommandLineOptions.Clo.XmlSink.WriteError("postcondition violation", err.FailingReturn.tok, err.FailingEnsures.tok, error.Trace);
+ er(errorInfo);
}
}
- else // error is AssertCounterexample
- {
- AssertCounterexample err = (AssertCounterexample)error;
- if (err.FailingAssert is LoopInitAssertCmd)
- {
- printer.ReportBplError(err.FailingAssert.tok, cause + " BP5004: This loop invariant might not hold on entry.", true, true);
-
- errorInfo = errorInformationFactory.CreateErrorInformation(err.FailingAssert.tok, cause + ": " + "This loop invariant might not hold on entry.", err.RequestId);
+ }
+ }
+ }
- if (CommandLineOptions.Clo.XmlSink != null)
- {
- CommandLineOptions.Clo.XmlSink.WriteError("loop invariant entry violation", err.FailingAssert.tok, null, error.Trace);
- }
- }
- else if (err.FailingAssert is LoopInvMaintainedAssertCmd)
- {
- // this assertion is a loop invariant which is not maintained
- printer.ReportBplError(err.FailingAssert.tok, cause + " BP5005: This loop invariant might not be maintained by the loop.", true, true);
- errorInfo = errorInformationFactory.CreateErrorInformation(err.FailingAssert.tok, cause + ": " + "This loop invariant might not be maintained by the loop.", err.RequestId);
+ 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";
+ }
- if (CommandLineOptions.Clo.XmlSink != null)
- {
- CommandLineOptions.Clo.XmlSink.WriteError("loop invariant maintenance violation", err.FailingAssert.tok, null, error.Trace);
- }
- }
- else
- {
- if (!CommandLineOptions.Clo.ForceBplErrors && err.FailingAssert.ErrorMessage != null)
- {
- printer.ReportBplError(err.FailingAssert.tok, err.FailingAssert.ErrorMessage, true, false);
- }
- else if (err.FailingAssert.ErrorData is string)
- {
- printer.ReportBplError(err.FailingAssert.tok, (string)err.FailingAssert.ErrorData, true, true);
- }
- else
- {
- printer.ReportBplError(err.FailingAssert.tok, cause + " BP5001: This assertion might not hold.", true, true);
- }
+ 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, 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");
- var msg = err.FailingAssert.ErrorData as string;
- if (msg == null)
- {
- msg = "This assertion might not hold.";
- }
- errorInfo = errorInformationFactory.CreateErrorInformation(err.FailingAssert.tok, cause + ": " + msg, err.RequestId);
+ if (!CommandLineOptions.Clo.ForceBplErrors && callError.FailingRequires.ErrorMessage != null)
+ {
+ errorInfo = errorInformationFactory.CreateErrorInformation(null, callError.FailingRequires.ErrorMessage, callError.RequestId, cause);
+ }
+ }
+ else if (returnError != null)
+ {
+ errorInfo = errorInformationFactory.CreateErrorInformation(returnError.FailingReturn.tok, "A postcondition might not hold on this return path.", returnError.RequestId, 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.XmlSink != null)
- {
- CommandLineOptions.Clo.XmlSink.WriteError("assertion violation", err.FailingAssert.tok, null, error.Trace);
- }
- }
- }
- if (CommandLineOptions.Clo.EnhancedErrorMessages == 1)
- {
- foreach (string info in error.relatedInformation)
- {
- Contract.Assert(info != null);
- Console.WriteLine(" " + info);
- }
- }
- if (CommandLineOptions.Clo.ErrorTrace > 0)
+ if (!CommandLineOptions.Clo.ForceBplErrors && returnError.FailingEnsures.ErrorMessage != null)
+ {
+ errorInfo = errorInformationFactory.CreateErrorInformation(null, returnError.FailingEnsures.ErrorMessage, returnError.RequestId, 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, 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, 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)
{
- Console.WriteLine("Execution trace:");
- error.Print(4);
-
- foreach (Block b in error.Trace)
+ msg = assertError.FailingAssert.ErrorMessage;
+ tok = null;
+ if (cause == "Error")
{
- if (!(CommandLineOptions.Clo.ErrorTrace == 1 && b.tok.line == -17 && b.tok.col == -4))
- {
- errorInfo.AddAuxInfo(b.tok, "Execution trace: " + b.Label);
- }
+ cause = null;
}
}
- if (CommandLineOptions.Clo.ModelViewFile != null)
- {
- error.PrintModel();
- }
- if (cause == "Error")
+ string bec = null;
+ if (msg == null)
{
- errorCount++;
+ msg = "This assertion might not hold.";
+ bec = "BP5001";
}
- if (er != null)
- {
- er(errorInfo);
- }
- }
- if (cause == "Error")
- {
- printer.Inform(String.Format("{0}error{1}", timeIndication, errors.Count == 1 ? "" : "s"));
+
+ errorInfo = errorInformationFactory.CreateErrorInformation(tok, msg, assertError.RequestId, cause);
+ errorInfo.BoogieErrorCode = bec;
+ errorInfo.Kind = ErrorKind.Assertion;
}
}
+
+ return errorInfo;
+ }
+
+
+ private static void WriteErrorInformationToXmlSink(ErrorInformation errorInfo, BlockSeq 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/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs index 14bb39ba..e3d3d109 100644 --- a/Source/ExecutionEngine/VerificationResultCache.cs +++ b/Source/ExecutionEngine/VerificationResultCache.cs @@ -91,25 +91,6 @@ namespace Microsoft.Boogie }
- public class VerificationResult
- {
- public readonly string Checksum;
- public readonly string DependeciesChecksum;
- public readonly string RequestId;
- public readonly ConditionGeneration.Outcome Outcome;
- public readonly List<Counterexample> Errors;
-
- public VerificationResult(string requestId, string checksum, string depsChecksum, ConditionGeneration.Outcome outcome, List<Counterexample> errors)
- {
- Checksum = checksum;
- DependeciesChecksum = depsChecksum;
- Outcome = outcome;
- Errors = errors;
- RequestId = requestId;
- }
- }
-
-
public class VerificationResultCache
{
private readonly ConcurrentDictionary<string, VerificationResult> Cache = new ConcurrentDictionary<string, VerificationResult>();
@@ -132,6 +113,19 @@ namespace Microsoft.Boogie }
+ public VerificationResult Lookup(Implementation impl)
+ {
+ if (!NeedsToBeVerified(impl))
+ {
+ return Lookup(impl.Id);
+ }
+ else
+ {
+ return null;
+ }
+ }
+
+
public void Clear()
{
Cache.Clear();
@@ -153,16 +147,29 @@ namespace Microsoft.Boogie public bool NeedsToBeVerified(Implementation impl)
{
- if (!Cache.ContainsKey(impl.Id)
- || Cache[impl.Id].Checksum != impl.Checksum)
+ return VerificationPriority(impl) < int.MaxValue;
+ }
+
+
+ public int VerificationPriority(Implementation impl)
+ {
+ if (!Cache.ContainsKey(impl.Id))
{
- return true;
+ return 3; // high priority (has been never verified before)
+ }
+ else if (Cache[impl.Id].Checksum != impl.Checksum)
+ {
+ return 2; // medium priority (old snapshot has been verified before)
+ }
+ else if (impl.DependenciesChecksum == null || Cache[impl.Id].DependeciesChecksum != impl.DependenciesChecksum)
+ {
+ return 1; // low priority (the same snapshot has been verified before, but a callee has changed)
+ }
+ else
+ {
+ return int.MaxValue; // skip verification (highest priority to get them done as soon as possible)
}
-
- var depsChecksum = DependencyCollector.DependenciesChecksum(impl);
- return depsChecksum == null || Cache[impl.Id].DependeciesChecksum != depsChecksum;
}
-
}
}
diff --git a/Source/Graph/Graph.cs b/Source/Graph/Graph.cs index 4d81e741..b6fe8cfc 100644 --- a/Source/Graph/Graph.cs +++ b/Source/Graph/Graph.cs @@ -866,25 +866,56 @@ namespace Microsoft.Boogie.GraphUtil { s.AppendLine("}");
return s.ToString();
}
+
+ public ICollection<Node> ComputeReachable() {
+ ICollection<Node> result = new HashSet<Node>();
+ Stack<Node> stack = new Stack<Node>();
+ stack.Push(source);
+ while(!(stack.Count() == 0)) {
+ Node n = stack.Pop();
+ result.Add(n);
+ foreach(var m in Successors(n)) {
+ if(!result.Contains(m)) {
+ stack.Push(m);
+ }
+ }
+ }
+ return result;
+ }
+
} // end: class Graph
public static class GraphAlgorithms
{
+
public static Graph<Node> Dual<Node>(this Graph<Node> g, Node dummySource)
{
var exits = g.Nodes.Where(n => g.Successors(n).Count() == 0).ToList();
+ Node source;
if (exits.Count == 0)
- return null;
+ exits.Add(dummySource);
var dual = new Graph<Node>(new HashSet<Tuple<Node, Node>>(g.Edges.Select(e => new Tuple<Node, Node>(e.Item2, e.Item1))));
if (exits.Count == 1)
+ {
dual.AddSource(exits[0]);
+ source = exits[0];
+ }
else
{
dual.AddSource(dummySource);
+ source = dummySource;
foreach (var exit in exits)
dual.AddEdge(dummySource, exit);
}
+
+ #region Dual graph may not be connected, so add an edge from the dual graph's soure node to any unreachable node
+ foreach (var n in dual.Nodes.Where(Item => !dual.ComputeReachable().Contains(Item)))
+ {
+ dual.AddEdge(source, n);
+ }
+ #endregion
+
return dual;
}
diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs index dd680509..24a3c708 100644 --- a/Source/Houdini/AbstractHoudini.cs +++ b/Source/Houdini/AbstractHoudini.cs @@ -98,7 +98,7 @@ namespace Microsoft.Boogie.Houdini { Inline();
- this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
+ this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, new List<Checker>());
this.prover = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, -1);
this.proverTime = TimeSpan.Zero;
@@ -402,12 +402,14 @@ namespace Microsoft.Boogie.Houdini { private Model.Element getValue(VCExpr arg, Model model)
{
-
+
+
if (arg is VCExprLiteral)
{
//return model.GetElement(arg.ToString());
return model.MkElement(arg.ToString());
}
+
else if (arg is VCExprVar)
{
var el = model.TryGetFunc(prover.Context.Lookup(arg as VCExprVar));
@@ -427,19 +429,27 @@ namespace Microsoft.Boogie.Houdini { return null;
}
}
- else
+ else if (arg is VCExprNAry && (arg as VCExprNAry).Op is VCExprBvOp)
{
- var val = prover.Evaluate(arg);
- if (val is int || val is bool || val is Microsoft.Basetypes.BigNum)
- {
- return model.MkElement(val.ToString());
- }
- else
+ // support for BV constants
+ var bvc = (arg as VCExprNAry)[0] as VCExprLiteral;
+ if (bvc != null)
{
- Debug.Assert(false);
+ var ret = model.TryMkElement(bvc.ToString() + arg.Type.ToString());
+ if (ret != null && (ret is Model.BitVector)) return ret;
}
- return null;
}
+
+ var val = prover.Evaluate(arg);
+ if (val is int || val is bool || val is Microsoft.Basetypes.BigNum)
+ {
+ return model.MkElement(val.ToString());
+ }
+ else
+ {
+ Debug.Assert(false);
+ }
+ return null;
}
// Remove functions AbsHoudiniConstant from the expressions and substitute them with "true"
@@ -625,9 +635,11 @@ namespace Microsoft.Boogie.Houdini { // the right thing.
foreach (var tup in fv.functionsUsed)
{
- //var tt = prover.Context.BoogieExprTranslator.Translate(tup.Item3);
- //tt = prover.VCExprGen.Or(VCExpressionGenerator.True, tt);
- //prover.Assert(tt, true);
+ // Ignore ones with bound varibles
+ if (tup.Item2.InParams.Count > 0) continue;
+ var tt = prover.Context.BoogieExprTranslator.Translate(tup.Item3);
+ tt = prover.VCExprGen.Or(VCExpressionGenerator.True, tt);
+ prover.Assert(tt, true);
}
}
@@ -1443,6 +1455,279 @@ namespace Microsoft.Boogie.Houdini { }
}
+ // foo(x) = x < 2^j for some j <= 16
+ public class PowDomain : IAbstractDomain
+ {
+ enum Val { FALSE, NEITHER, TRUE };
+ Val tlevel;
+ bool isBottom { get { return tlevel == Val.FALSE; } }
+ bool isTop { get { return tlevel == Val.TRUE; } }
+
+ readonly int Max = 16;
+
+ int upper; // <= Max
+
+ private PowDomain(Val tlevel) :
+ this(tlevel, 0) { }
+
+ private PowDomain(Val tlevel, int upper)
+ {
+ this.tlevel = tlevel;
+ this.upper = upper;
+ }
+
+ public static IAbstractDomain GetBottom()
+ {
+ return new PowDomain(Val.FALSE) as IAbstractDomain;
+ }
+
+ IAbstractDomain IAbstractDomain.Bottom()
+ {
+ return GetBottom();
+ }
+
+ IAbstractDomain IAbstractDomain.Join(List<Model.Element> state)
+ {
+ if (isTop) return this;
+
+ int v = 0;
+ if (state[0] is Model.BitVector)
+ v = (state[0] as Model.BitVector).AsInt();
+ else if (state[0] is Model.Integer)
+ v = (state[0] as Model.Integer).AsInt();
+ else Debug.Assert(false);
+
+ var nupper = upper;
+ while ((1 << nupper) < v) nupper++;
+ var ntlevel = Val.NEITHER;
+ if (nupper > Max) ntlevel = Val.TRUE;
+ return new PowDomain(ntlevel, nupper);
+ }
+
+ Expr IAbstractDomain.Gamma(List<Expr> vars)
+ {
+ if (isBottom) return Expr.False;
+ if (isTop) return Expr.True;
+ var v = vars[0];
+ if (v.Type.IsBv)
+ {
+ var bits = v.Type.BvBits;
+ if (!AbstractDomainFactory.bvslt.ContainsKey(bits))
+ throw new AbsHoudiniInternalError("No builtin function found for bv" + bits.ToString());
+ var bvslt = AbstractDomainFactory.bvslt[bits];
+ return new NAryExpr(Token.NoToken, new FunctionCall(bvslt), new ExprSeq(v,
+ new LiteralExpr(Token.NoToken, Basetypes.BigNum.FromInt(1 << (upper+1)), 32)));
+ }
+ else
+ {
+ return Expr.Lt(v, Expr.Literal(1 << (upper+1)));
+ }
+ }
+
+ bool IAbstractDomain.TypeCheck(List<Type> argTypes, out string msg)
+ {
+ msg = "";
+ if (argTypes.Count != 1)
+ {
+ msg = "Illegal number of arguments, expecting 1";
+ return false;
+ }
+ if (argTypes.Any(tt => !tt.IsInt && !tt.IsBv))
+ {
+ msg = "Illegal type, expecting int or bv";
+ return false;
+ }
+ return true;
+ }
+ }
+
+ // foo(x_i) = all equalities that hold
+ public class EqualitiesDomain : IAbstractDomain
+ {
+ bool isBottom;
+ List<HashSet<int>> equalities;
+
+ public EqualitiesDomain(bool isBottom, List<HashSet<int>> eq)
+ {
+ this.isBottom = isBottom;
+ this.equalities = eq;
+ }
+
+ public static IAbstractDomain GetBottom()
+ {
+ return new EqualitiesDomain(true, new List<HashSet<int>>());
+ }
+
+ IAbstractDomain IAbstractDomain.Bottom()
+ {
+ return GetBottom();
+ }
+
+ IAbstractDomain IAbstractDomain.Join(List<Model.Element> state)
+ {
+ // find the guys that are equal
+ var eq = new List<HashSet<int>>();
+ for (int i = 0; i < state.Count; i++)
+ {
+ var added = false;
+ foreach (var s in eq)
+ {
+ var sv = s.First();
+ if (state[i].ToString() == state[sv].ToString())
+ {
+ s.Add(i);
+ added = true;
+ break;
+ }
+ }
+ if (!added) eq.Add(new HashSet<int>(new int[] { i }));
+ }
+
+ if (isBottom)
+ {
+ return new EqualitiesDomain(false, eq);
+ }
+
+ // intersect two partitions equalities and eq
+ var m1 = GetMap(equalities, state.Count);
+ var m2 = GetMap(eq, state.Count);
+
+ for (int i = 0; i < state.Count; i++)
+ m2[i] = new HashSet<int>(m2[i].Intersect(m1[i]));
+
+
+ // map from representative to set
+ var repToSet = new Dictionary<int, HashSet<int>>();
+
+ for (int i = 0; i < state.Count; i++)
+ {
+ var rep = m2[i].Min();
+ if (!repToSet.ContainsKey(rep))
+ repToSet[rep] = m2[i];
+ }
+
+ var ret = new List<HashSet<int>>();
+ repToSet.Values.Iter(s => ret.Add(s));
+
+ return new EqualitiesDomain(false, ret);
+ }
+
+ Expr IAbstractDomain.Gamma(List<Expr> vars)
+ {
+ if (isBottom) return Expr.False;
+ Expr ret = Expr.True;
+ foreach (var eq in equalities.Select(hs => hs.ToList()))
+ {
+ if (eq.Count == 1) continue;
+ var prev = eq[0];
+ for (int i = 1; i < eq.Count; i++)
+ {
+ ret = Expr.And(ret, Expr.Eq(vars[prev], vars[eq[i]]));
+ prev = eq[i];
+ }
+ }
+ return ret;
+ }
+
+ bool IAbstractDomain.TypeCheck(List<Type> argTypes, out string msg)
+ {
+ msg = "";
+ if (argTypes.Count == 0) return true;
+ var ot = argTypes[0];
+
+ if (argTypes.Any(tt => !tt.Equals(ot)))
+ {
+ msg = string.Format("Illegal type, expecting type {0}, got {1}", ot, argTypes.First(tt => !tt.Equals(ot)));
+ return false;
+ }
+ return true;
+ }
+
+ private HashSet<int>[] GetMap(List<HashSet<int>> eq, int n)
+ {
+ var ret = new HashSet<int>[n];
+ foreach (var s in eq)
+ {
+ foreach (var i in s)
+ ret[i] = s;
+ }
+ return ret;
+ }
+ }
+
+ // foo(a,b) \in {false, \not a, a ==> b, true}
+ public class ImplicationDomain : IAbstractDomain
+ {
+ enum Val {FALSE, NOT_A, A_IMP_B, TRUE};
+ Val val;
+
+ private ImplicationDomain(Val val)
+ {
+ this.val = val;
+ }
+
+ public static ImplicationDomain GetBottom()
+ {
+ return new ImplicationDomain(Val.FALSE);
+ }
+
+ public IAbstractDomain Bottom()
+ {
+ return GetBottom();
+ }
+
+ public IAbstractDomain Join(List<Model.Element> states)
+ {
+ Debug.Assert(states.Count == 2);
+ var v1 = (states[0] as Model.Boolean).Value;
+ var v2 = (states[1] as Model.Boolean).Value;
+
+ if (val == Val.TRUE) return this;
+
+ var that = Val.TRUE;
+ if (!v1) that = Val.NOT_A;
+ else if (!v1 || v2) that = Val.A_IMP_B;
+
+ if (that == Val.TRUE || val == Val.FALSE)
+ return new ImplicationDomain(that);
+
+ // Now, neither this or that is FALSE or TRUE
+ if (val == that)
+ return this;
+
+ Debug.Assert(val == Val.A_IMP_B || that == Val.A_IMP_B);
+ return new ImplicationDomain(Val.A_IMP_B);
+ }
+
+ public Expr Gamma(List<Expr> vars)
+ {
+ Debug.Assert(vars.Count == 2);
+
+ var v1 = vars[0];
+ var v2 = vars[1];
+
+ if (val == Val.FALSE) return Expr.False;
+ if (val == Val.TRUE) return Expr.True;
+ if (val == Val.NOT_A) return Expr.Not(v1);
+ return Expr.Imp(v1, v2);
+ }
+
+ public bool TypeCheck(List<Type> argTypes, out string msg)
+ {
+ msg = "";
+ if (argTypes.Count != 2)
+ {
+ msg = "Illegal number of arguments, expecting 2";
+ return false;
+ }
+ if (argTypes.Any(tt => !tt.IsBool))
+ {
+ msg = "Illegal type, expecting bool";
+ return false;
+ }
+ return true;
+ }
+ }
public class ConstantProp : IAbstractDomain
{
@@ -1653,6 +1938,9 @@ namespace Microsoft.Boogie.Houdini { // Type name -> Instance
private static Dictionary<string, IAbstractDomain> abstractDomainInstances = new Dictionary<string, IAbstractDomain>();
private static Dictionary<string, IAbstractDomain> abstractDomainInstancesFriendly = new Dictionary<string, IAbstractDomain>();
+
+ // bitvector operations
+ public static Dictionary<int, Function> bvslt = new Dictionary<int, Function>();
public static void Register(string friendlyName, IAbstractDomain instance)
{
@@ -1681,7 +1969,7 @@ namespace Microsoft.Boogie.Houdini { return abstractDomainInstancesFriendly[friendlyName] as IAbstractDomain;
}
- public static void Initialize()
+ public static void Initialize(Program program)
{
// Declare abstract domains
var domains = new List<System.Tuple<string, IAbstractDomain>>(new System.Tuple<string, IAbstractDomain>[] {
@@ -1689,14 +1977,26 @@ namespace Microsoft.Boogie.Houdini { System.Tuple.Create("Intervals", new Intervals() as IAbstractDomain),
System.Tuple.Create("ConstantProp", ConstantProp.GetBottom() as IAbstractDomain),
System.Tuple.Create("PredicateAbs", new PredicateAbsElem() as IAbstractDomain),
+ System.Tuple.Create("ImplicationDomain", ImplicationDomain.GetBottom() as IAbstractDomain),
+ System.Tuple.Create("PowDomain", PowDomain.GetBottom() as IAbstractDomain),
+ System.Tuple.Create("EqualitiesDomain", EqualitiesDomain.GetBottom() as IAbstractDomain),
System.Tuple.Create("IA[HoudiniConst]", new IndependentAttribute<HoudiniConst>() as IAbstractDomain),
System.Tuple.Create("IA[ConstantProp]", new IndependentAttribute<ConstantProp>() as IAbstractDomain),
- System.Tuple.Create("IA[Intervals]", new IndependentAttribute<Intervals>() as IAbstractDomain)
+ System.Tuple.Create("IA[Intervals]", new IndependentAttribute<Intervals>() as IAbstractDomain),
+ System.Tuple.Create("IA[PowDomain]", new IndependentAttribute<PowDomain>() as IAbstractDomain),
});
domains.Iter(tup => AbstractDomainFactory.Register(tup.Item1, tup.Item2));
+ program.TopLevelDeclarations.OfType<Function>()
+ .Iter(RegisterFunction);
}
+ private static void RegisterFunction(Function func)
+ {
+ var attr = QKeyValue.FindStringAttribute(func.Attributes, "bvbuiltin");
+ if (attr != null && attr == "bvslt" && func.InParams.Count == 2 && func.InParams[0].TypedIdent.Type.IsBv)
+ bvslt.Add(func.InParams[0].TypedIdent.Type.BvBits, func);
+ }
}
public interface IAbstractDomain
@@ -1753,7 +2053,7 @@ namespace Microsoft.Boogie.Houdini { if (CommandLineOptions.Clo.ProverKillTime > 0)
CommandLineOptions.Clo.ProverOptions.Add(string.Format("TIME_LIMIT={0}", CommandLineOptions.Clo.ProverKillTime));
- this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
+ this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, new List<Checker>());
this.prover = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, -1);
this.reporter = new AbstractHoudiniErrorReporter();
diff --git a/Source/Houdini/CandidateDependenceAnalyser.cs b/Source/Houdini/CandidateDependenceAnalyser.cs index f00514cf..09cef241 100644 --- a/Source/Houdini/CandidateDependenceAnalyser.cs +++ b/Source/Houdini/CandidateDependenceAnalyser.cs @@ -12,6 +12,7 @@ namespace Microsoft.Boogie { private const int COARSE_STAGES = 1;
private const int FINE_STAGES = 2;
+ private const int BALANCED_STAGES = 3;
private Program prog;
private IVariableDependenceAnalyser varDepAnalyser;
@@ -120,6 +121,44 @@ namespace Microsoft.Boogie { }
}
}
+
+ if(CommandLineOptions.Clo.StagedHoudiniMergeIgnoredCandidates) {
+ MergeIgnoredCandidates();
+ }
+
+ }
+
+ private void MergeIgnoredCandidates()
+ {
+ var IgnoredCandidatesToVariables = new Dictionary<string, HashSet<Variable>>();
+ foreach(var c in candidates) {
+ IgnoredCandidatesToVariables[c] = new HashSet<Variable>();
+ }
+ foreach(var ci in CandidateInstances()) {
+ if(!IgnoredCandidatesToVariables.ContainsKey(ci.Candidate)) {
+ continue;
+ }
+ VariableCollector vc = new VariableCollector();
+ vc.Visit(ci.Expr);
+ if(vc.usedVars.Select(Item => varDepAnalyser.VariableRelevantToAnalysis(Item, ci.Proc)).Count() != 0) {
+ continue;
+ }
+ foreach(var v in vc.usedVars) {
+ if(varDepAnalyser.Ignoring(v, ci.Proc)) {
+ IgnoredCandidatesToVariables[ci.Candidate].Add(v);
+ }
+ }
+ }
+ foreach(var c in IgnoredCandidatesToVariables.Keys) {
+ foreach(var d in IgnoredCandidatesToVariables.Keys) {
+ if(c == d) {
+ continue;
+ }
+ if(IgnoredCandidatesToVariables[c].Equals(IgnoredCandidatesToVariables[d])) {
+ CandidateDependences.AddEdge(c, d);
+ }
+ }
+ }
}
@@ -137,17 +176,26 @@ namespace Microsoft.Boogie { candidateDependsOn[c] = new HashSet<VariableDescriptor>();
}
- // Candidate loop invariants
+ foreach(var candidateInstance in CandidateInstances()) {
+ AddDependences(candidateInstance);
+ }
+
+ }
+
+ private IEnumerable<CandidateInstance> CandidateInstances()
+ {
foreach (var impl in prog.TopLevelDeclarations.OfType<Implementation>())
{
- foreach (var b in impl.Blocks)
- {
- foreach (Cmd c in b.Cmds)
+ foreach (var b in impl.Blocks) {
+ foreach (Cmd cmd in b.Cmds)
{
- var p = c as PredicateCmd;
+ var p = cmd as PredicateCmd;
if (p != null)
{
- CheckExpr(impl.Name, p.Expr);
+ string c;
+ if(Houdini.Houdini.MatchCandidate(p.Expr, candidates, out c)) {
+ yield return new CandidateInstance(c, impl.Name, p.Expr);
+ }
}
}
}
@@ -157,11 +205,17 @@ namespace Microsoft.Boogie { {
foreach (Requires r in proc.Requires)
{
- CheckExpr(proc.Name, r.Condition);
+ string c;
+ if(Houdini.Houdini.MatchCandidate(r.Condition, candidates, out c)) {
+ yield return new CandidateInstance(c, proc.Name, r.Condition);
+ }
}
foreach (Ensures e in proc.Ensures)
{
- CheckExpr(proc.Name, e.Condition);
+ string c;
+ if(Houdini.Houdini.MatchCandidate(e.Condition, candidates, out c)) {
+ yield return new CandidateInstance(c, proc.Name, e.Condition);
+ }
}
}
}
@@ -178,24 +232,20 @@ namespace Microsoft.Boogie { return false;
}
- private void CheckExpr(string proc, Expr e) {
- string candidate;
- Houdini.Houdini.MatchCandidate(e, candidates, out candidate);
- if (candidate != null) {
- VariableCollector vc = new VariableCollector();
- vc.VisitExpr(e);
+ private void AddDependences(CandidateInstance ci) {
+ VariableCollector vc = new VariableCollector();
+ vc.VisitExpr(ci.Expr);
- foreach (var v in vc.usedVars.Where(Item => varDepAnalyser.VariableRelevantToAnalysis(Item, proc))) {
- VariableDescriptor vd =
- varDepAnalyser.MakeDescriptor(proc, v);
- if (!variableDirectlyReferredToByCandidates.ContainsKey(vd)) {
- variableDirectlyReferredToByCandidates[vd] = new HashSet<string>();
- }
- variableDirectlyReferredToByCandidates[vd].Add(candidate);
+ foreach (var v in vc.usedVars.Where(Item => varDepAnalyser.VariableRelevantToAnalysis(Item, ci.Proc))) {
+ VariableDescriptor vd =
+ varDepAnalyser.MakeDescriptor(ci.Proc, v);
+ if (!variableDirectlyReferredToByCandidates.ContainsKey(vd)) {
+ variableDirectlyReferredToByCandidates[vd] = new HashSet<string>();
+ }
+ variableDirectlyReferredToByCandidates[vd].Add(ci.Candidate);
- foreach (var w in varDepAnalyser.DependsOn(vd)) {
- candidateDependsOn[candidate].Add(w);
- }
+ foreach (var w in varDepAnalyser.DependsOn(vd)) {
+ candidateDependsOn[ci.Candidate].Add(w);
}
}
}
@@ -260,7 +310,7 @@ namespace Microsoft.Boogie { for (int i = 0; i < Components.Count(); i++) {
Console.Write(i + ": ");
DumpSCC(Components[i]);
- Console.WriteLine("\n");
+ Console.WriteLine(); Console.WriteLine();
}
Console.WriteLine("Stages DAG");
@@ -313,11 +363,24 @@ namespace Microsoft.Boogie { }
#region Assign candidates to stages at a given level of granularity
- Debug.Assert(CommandLineOptions.Clo.StagedHoudini == COARSE_STAGES ||
- CommandLineOptions.Clo.StagedHoudini == FINE_STAGES);
- Dictionary<string, int> candidateToStage =
- (CommandLineOptions.Clo.StagedHoudini == COARSE_STAGES) ? ComputeCoarseStages()
- : ComputeFineStages();
+
+ Dictionary<string, int> candidateToStage;
+
+ switch(CommandLineOptions.Clo.StagedHoudini) {
+ case COARSE_STAGES:
+ candidateToStage = ComputeCoarseStages();
+ break;
+ case FINE_STAGES:
+ candidateToStage = ComputeFineStages();
+ break;
+ case BALANCED_STAGES:
+ candidateToStage = ComputeBalancedStages();
+ break;
+ default:
+ Debug.Assert(false);
+ candidateToStage = null;
+ break;
+ }
foreach(var c in candidates) {
Debug.Assert(candidateToStage.ContainsKey(c));
@@ -421,6 +484,60 @@ namespace Microsoft.Boogie { }
+ private int FindLargestStage() {
+ return StagesDAG.Nodes.Select(Item => Item.Count()).Max();
+ }
+
+
+ private Dictionary<string, int> ComputeCoarseStages()
+ {
+ var result = new Dictionary<string, int>();
+ HashSet<SCC<string>> done = new HashSet<SCC<string>> { GetStartNodeOfStagesDAG() };
+ for(int stageId = 0; done.Count() != StagesDAG.Nodes.Count(); stageId++)
+ {
+ foreach (var n in StagesDAG.Nodes.Where(Item => !done.Contains(Item)))
+ {
+ if(StagesDAG.Successors(n).Where(Item => !done.Contains(Item)).Count() == 0) {
+ foreach (var c in n)
+ {
+ result[c] = stageId;
+ }
+ done.Add(n);
+ }
+ }
+ }
+ return result;
+ }
+
+ private Dictionary<string, int> ComputeBalancedStages()
+ {
+ int maxStageSize = 200;
+ var result = new Dictionary<string, int>();
+ HashSet<SCC<string>> done = new HashSet<SCC<string>> { GetStartNodeOfStagesDAG() };
+ for(int stageId = 0; done.Count() != StagesDAG.Nodes.Count(); stageId++)
+ {
+ int stageSize = 0;
+ foreach (var n in StagesDAG.Nodes.Where(Item => !done.Contains(Item)))
+ {
+ if(stageSize + n.Count() > maxStageSize) {
+ continue;
+ }
+ if(StagesDAG.Successors(n).Where(Item => !done.Contains(Item)).Count() == 0) {
+ foreach (var c in n)
+ {
+ result[c] = stageId;
+ stageSize++;
+ }
+ done.Add(n);
+ }
+ }
+ if(stageSize == 0) {
+ maxStageSize *= 2;
+ }
+ }
+ return result;
+ }
+
private Dictionary<string, int> ComputeFineStages()
{
@@ -446,62 +563,10 @@ namespace Microsoft.Boogie { }
- private Dictionary<string, int> ComputeCoarseStages()
+ private SCC<string> GetStartNodeOfStagesDAG()
{
- var result = new Dictionary<string, int>();
- SCC<string> start = null;
- foreach (var n in StagesDAG.Nodes)
- {
- if (StagesDAG.Successors(n).Count() == 0)
- {
- start = n;
- break;
- }
- }
- System.Diagnostics.Debug.Assert(start != null);
-
- HashSet<SCC<string>> done = new HashSet<SCC<string>>();
- done.Add(start);
-
- bool finished = false;
- int stageId = 0;
- while (!finished)
- {
- finished = true;
- HashSet<SCC<string>> stage = new HashSet<SCC<string>>();
- foreach (var n in StagesDAG.Nodes)
- {
- if (!done.Contains(n))
- {
- finished = false;
- bool ready = true;
- foreach (var m in StagesDAG.Successors(n))
- {
- if (!done.Contains(m))
- {
- ready = false;
- break;
- }
- }
- if (ready)
- {
- stage.Add(n);
- done.Add(n);
- }
- }
- }
-
- foreach (var scc in stage)
- {
- foreach (var c in scc)
- {
- result[c] = stageId;
- }
- }
-
- stageId++;
- }
- return result;
+ return StagesDAG.Nodes.Where(Item => StagesDAG.Successors(Item).Count() == 0).
+ ToList()[0];
}
private bool NoStages()
@@ -536,7 +601,7 @@ namespace Microsoft.Boogie { this.candidates = candidates;
this.reachabilityGraph = new InterproceduralReachabilityGraph(prog);
this.candidateToOccurences = new Dictionary<string,HashSet<object>>();
-
+
// Add all candidate occurrences in blocks
foreach(Block b in prog.TopLevelDeclarations.OfType<Implementation>().Select(Item => Item.Blocks).SelectMany(Item => Item)) {
foreach(Cmd cmd in b.Cmds) {
@@ -621,4 +686,16 @@ namespace Microsoft.Boogie { }
}
+ class CandidateInstance {
+ public string Candidate;
+ public string Proc;
+ public Expr Expr;
+
+ internal CandidateInstance(string Candidate, string Proc, Expr Expr) {
+ this.Candidate = Candidate;
+ this.Proc = Proc;
+ this.Expr = Expr;
+ }
+ }
+
}
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index 4f1e2a8b..abc5a7e8 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -349,7 +349,7 @@ namespace Microsoft.Boogie.Houdini { Inline();
- this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
+ this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, new List<Checker>());
this.proverInterface = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, CommandLineOptions.Clo.ProverKillTime);
vcgenFailures = new HashSet<Implementation>();
@@ -548,6 +548,28 @@ namespace Microsoft.Boogie.Houdini { return false;
}
+ public static bool GetCandidateWithoutConstant(Expr boogieExpr, IEnumerable<string> candidates, out string candidateConstant, out Expr exprWithoutConstant) {
+ candidateConstant = null;
+ exprWithoutConstant = null;
+ NAryExpr e = boogieExpr as NAryExpr;
+ if (e != null && e.Fun is BinaryOperator && ((BinaryOperator)e.Fun).Op == BinaryOperator.Opcode.Imp) {
+ Expr antecedent = e.Args[0];
+ Expr consequent = e.Args[1];
+
+ IdentifierExpr id = antecedent as IdentifierExpr;
+ if (id != null && id.Decl is Constant && candidates.Contains(id.Decl.Name)) {
+ candidateConstant = id.Decl.Name;
+ exprWithoutConstant = consequent;
+ return true;
+ }
+
+ if (GetCandidateWithoutConstant(consequent, candidates, out candidateConstant, out exprWithoutConstant))
+ exprWithoutConstant = Expr.Imp(antecedent, exprWithoutConstant);
+ return true;
+ }
+ return false;
+ }
+
private static Expr AddConditionToCandidateRec(Expr boogieExpr, Expr condition, string candidateConstant, List<Expr> implicationStack)
{
NAryExpr e = boogieExpr as NAryExpr;
diff --git a/Source/Predication/UniformityAnalyser.cs b/Source/Predication/UniformityAnalyser.cs index 2e0f4074..ca5a0df6 100644 --- a/Source/Predication/UniformityAnalyser.cs +++ b/Source/Predication/UniformityAnalyser.cs @@ -232,6 +232,17 @@ namespace Microsoft.Boogie SetNonUniform(Impl.Name, v.Name);
}
}
+
+ foreach (Block b in Impl.Blocks) {
+ foreach (Cmd c in b.Cmds) {
+ CallCmd callCmd = c as CallCmd;
+ if (callCmd != null) {
+ if (IsUniform(callCmd.callee)) {
+ SetNonUniform(callCmd.callee);
+ }
+ }
+ }
+ }
return;
}
@@ -243,6 +254,12 @@ namespace Microsoft.Boogie ctrlDep.TransitiveClosure();
var nonUniformBlockSet = new HashSet<Block>();
+ /*// If procedure is non-uniform, so are all of its blocks
+ if (!uniformityInfo[Impl.Name].Key) {
+ foreach (var block in Impl.Blocks) {
+ nonUniformBlockSet.Add(block);
+ }
+ }*/
nonUniformBlocks[Impl.Name] = nonUniformBlockSet;
bool changed;
@@ -314,32 +331,32 @@ namespace Microsoft.Boogie DeclWithFormals Callee = GetProcedure(callCmd.callee);
Debug.Assert(Callee != null);
- if (!ControlFlowIsUniform)
+ if (!ControlFlowIsUniform)
+ {
+ if (IsUniform(callCmd.callee))
{
- if (IsUniform(callCmd.callee))
- {
- SetNonUniform(callCmd.callee);
- }
+ SetNonUniform(callCmd.callee);
}
+ }
for (int i = 0; i < Callee.InParams.Length; i++)
- {
+ {
if (IsUniform(callCmd.callee, Callee.InParams[i].Name)
- && !IsUniform(impl.Name, callCmd.Ins[i]))
- {
+ && !IsUniform(impl.Name, callCmd.Ins[i]))
+ {
SetNonUniform(callCmd.callee, Callee.InParams[i].Name);
- }
}
+ }
for (int i = 0; i < Callee.OutParams.Length; i++)
+ {
+ if (IsUniform(impl.Name, callCmd.Outs[i].Name)
+ && !IsUniform(callCmd.callee, Callee.OutParams[i].Name))
{
- if (IsUniform(impl.Name, callCmd.Outs[i].Name)
- && !IsUniform(callCmd.callee, Callee.OutParams[i].Name))
- {
- SetNonUniform(impl.Name, callCmd.Outs[i].Name);
- }
+ SetNonUniform(impl.Name, callCmd.Outs[i].Name);
}
-
}
+
+ }
else if (c is AssumeCmd)
{
var ac = (AssumeCmd)c;
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index eaa42b38..4cb85435 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -395,6 +395,21 @@ namespace Microsoft.Boogie.SMTLib FlushLogFile();
}
+ public override void Reset()
+ {
+ SendThisVC("(reset)");
+ Process.Send(common.ToString());
+ }
+
+ public override void FullReset()
+ {
+ SendThisVC("(reset)");
+ common.Clear();
+ AxiomsAreSetup = false;
+ ctx.Clear();
+ DeclCollector.Reset();
+ }
+
private RPFP.Node SExprToCex(SExpr resp, ErrorHandler handler,
Dictionary<int,Dictionary<string,string>> varSubst)
{
@@ -423,6 +438,12 @@ namespace Microsoft.Boogie.SMTLib var labs = line[4];
var refs = line[5];
var predName = conseq.Name;
+ {
+ string spacer = "@@"; // Hack! UniqueNamer is adding these and I can't stop it!
+ int pos = predName.LastIndexOf(spacer);
+ if (pos >= 0)
+ predName = predName.Substring(0, pos);
+ }
RPFP.Node node = null;
if (!pmap.TryGetValue(predName, out node))
{
@@ -461,7 +482,7 @@ namespace Microsoft.Boogie.SMTLib return null;
}
int ruleNum = Convert.ToInt32(rule.Name.Substring(5)) - 1;
- if(ruleNum < 0 || ruleNum > rpfp.edges.Count)
+ if (ruleNum < 0 || ruleNum > rpfp.edges.Count)
{
HandleProverError("bad rule name from prover: " + refs.ToString());
return null;
@@ -489,7 +510,7 @@ namespace Microsoft.Boogie.SMTLib varSubst[e.number] = dict;
foreach (var s in subst.Arguments)
{
- if(s.Name != "=" || s.Arguments.Length != 2)
+ if (s.Name != "=" || s.Arguments.Length != 2)
{
HandleProverError("bad equation from prover: " + s.ToString());
return null;
@@ -573,6 +594,7 @@ namespace Microsoft.Boogie.SMTLib currentLogFile.Write(common.ToString());
}
+ Push();
SendThisVC("(fixedpoint-push)");
foreach (var node in rpfp.nodes)
{
@@ -588,7 +610,15 @@ namespace Microsoft.Boogie.SMTLib string ruleString = "(rule " + QuantifiedVCExpr2String(rpfp.GetRule(edge)) + "\n)";
ruleStrings.Add(ruleString);
}
- string queryString = "(query " + QuantifiedVCExpr2String(rpfp.GetQuery()) + "\n :engine duality\n :print-certificate true\n)";
+ string queryString = "(query " + QuantifiedVCExpr2String(rpfp.GetQuery()) + "\n :engine duality\n :print-certificate true\n";
+
+#if true
+ if (CommandLineOptions.Clo.StratifiedInlining != 0)
+ queryString += " :stratified-inlining true\n";
+ if (CommandLineOptions.Clo.RecursionBound > 0)
+ queryString += " :recursion-bound " + Convert.ToString(CommandLineOptions.Clo.RecursionBound) + "\n";
+#endif
+ queryString += ")";
LineariserOptions.Default.LabelsBelowQuantifiers = false;
FlushAxioms();
@@ -672,6 +702,8 @@ namespace Microsoft.Boogie.SMTLib #endif
}
SendThisVC("(fixedpoint-pop)");
+ Pop();
+ AxiomsAreSetup = false;
return result;
}
@@ -806,7 +838,7 @@ namespace Microsoft.Boogie.SMTLib if (!options.MultiTraces)
posLabels = Enumerable.Empty<string>();
var conjuncts = posLabels.Select(s => "(not " + lbl(s) + ")").Concat(negLabels.Select(lbl)).ToArray();
- var expr = conjuncts.Length == 1 ? conjuncts[0] : ("(or " + conjuncts.Concat(" ") + ")");
+ string expr = conjuncts.Length == 1 ? conjuncts[0] : ("(or " + conjuncts.Concat(" ") + ")"); ;
if (!conjuncts.Any())
{
expr = "false";
@@ -983,7 +1015,7 @@ namespace Microsoft.Boogie.SMTLib result = Outcome.OutOfMemory;
Process.NeedsRestart = true;
break;
- case "timeout":
+ case "timeout": case "canceled":
currentErrorHandler.OnResourceExceeded("timeout");
result = Outcome.TimeOut;
break;
@@ -1178,7 +1210,7 @@ namespace Microsoft.Boogie.SMTLib public override void SetTimeOut(int ms)
{
- SendThisVC("(set-option :SOFT_TIMEOUT " + ms.ToString() + ")\n");
+ SendThisVC("(set-option :" + Z3.SetTimeoutOption() + " " + ms.ToString() + ")");
}
public override object Evaluate(VCExpr expr)
diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs index f4fa5e75..2374a157 100644 --- a/Source/Provers/SMTLib/SMTLibProcess.cs +++ b/Source/Provers/SMTLib/SMTLibProcess.cs @@ -63,12 +63,14 @@ namespace Microsoft.Boogie.SMTLib try {
- prover = Process.Start(psi);
+ prover = new Process();
+ prover.StartInfo = psi;
prover.ErrorDataReceived += prover_ErrorDataReceived;
- prover.OutputDataReceived += prover_OutputDataReceived;
- prover.BeginErrorReadLine();
- prover.BeginOutputReadLine();
+ prover.OutputDataReceived += prover_OutputDataReceived;
+ prover.Start();
toProver = prover.StandardInput;
+ prover.BeginErrorReadLine();
+ prover.BeginOutputReadLine();
} catch (System.ComponentModel.Win32Exception e) {
throw new ProverException(string.Format("Unable to start the process {0}: {1}", psi.FileName, e.Message));
}
diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs index 9d908138..2bbe4978 100644 --- a/Source/Provers/SMTLib/TypeDeclCollector.cs +++ b/Source/Provers/SMTLib/TypeDeclCollector.cs @@ -101,6 +101,19 @@ void ObjectInvariant() _KnownLBL.Push(new HashSet<string>());
}
+ public void Reset()
+ {
+ _KnownFunctions.Clear();
+ _KnownVariables.Clear();
+ _KnownTypes.Clear();
+ _KnownStoreFunctions.Clear();
+ _KnownSelectFunctions.Clear();
+ _KnownLBL.Clear();
+ AllDecls.Clear();
+ IncDecls.Clear();
+ InitializeKnownDecls();
+ }
+
public void Push()
{
Contract.Assert(_KnownFunctions.Count > 0);
diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs index 04bdc0df..66b1809a 100644 --- a/Source/Provers/SMTLib/Z3.cs +++ b/Source/Provers/SMTLib/Z3.cs @@ -160,10 +160,10 @@ namespace Microsoft.Boogie.SMTLib proc.StartInfo.UseShellExecute = false;
proc.StartInfo.CreateNoWindow = true;
proc.Start();
+ string answer = proc.StandardOutput.ReadToEnd();
proc.WaitForExit();
if (proc.ExitCode == 0)
- {
- string answer = proc.StandardOutput.ReadToEnd();
+ {
var firstdot = answer.IndexOf('.');
if (firstdot >= 0)
{
@@ -187,6 +187,16 @@ namespace Microsoft.Boogie.SMTLib minor = Z3MinorVersion;
}
+ public static string SetTimeoutOption()
+ {
+ int major, minor;
+ GetVersion(out major, out minor);
+ if (major > 4 || major == 4 && minor >= 3)
+ return "TIMEOUT";
+ else
+ return "SOFT_TIMEOUT";
+ }
+
// options that work only on the command line
static string[] commandLineOnly = { "TRACE", "PROOF_MODE" };
@@ -251,7 +261,7 @@ namespace Microsoft.Boogie.SMTLib if (options.TimeLimit > 0)
{
- options.AddWeakSmtOption("SOFT_TIMEOUT", options.TimeLimit.ToString());
+ options.AddWeakSmtOption("TIMEOUT", options.TimeLimit.ToString());
// This kills the Z3 *instance* after the specified time, not a particular query, so we cannot use it.
// options.AddSolverArgument("/T:" + (options.TimeLimit + 1000) / 1000);
}
@@ -261,9 +271,8 @@ namespace Microsoft.Boogie.SMTLib if (CommandLineOptions.Clo.WeakArrayTheory)
{
- // TODO: these options don't seem to exist in recent Z3
- // options.AddWeakSmtOption("ARRAY_WEAK", "true");
- // options.AddWeakSmtOption("ARRAY_EXTENSIONAL", "false");
+ options.AddWeakSmtOption("smt.array.weak", "true");
+ options.AddWeakSmtOption("smt.array.extensional", "false");
}
}
else
diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs index d08a4d4b..2ff93c54 100644 --- a/Source/VCExpr/Boogie2VCExpr.cs +++ b/Source/VCExpr/Boogie2VCExpr.cs @@ -272,7 +272,10 @@ namespace Microsoft.Boogie.VCExprAST { // global variables, local variables, incarnations, etc. are
// bound the first time they occur
if (!UnboundVariables.TryGetValue(boogieVar, out res)) {
- res = new VCExprVar(boogieVar.Name, boogieVar.TypedIdent.Type);
+ if (boogieVar is Constant)
+ res = new VCExprConstant(boogieVar.Name, boogieVar.TypedIdent.Type);
+ else
+ res = new VCExprVar(boogieVar.Name, boogieVar.TypedIdent.Type);
UnboundVariables.Bind(boogieVar, res);
}
return cce.NonNull(res);
diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs index 82bdebbe..f56b6978 100644 --- a/Source/VCExpr/VCExprAST.cs +++ b/Source/VCExpr/VCExprAST.cs @@ -1868,6 +1868,14 @@ namespace Microsoft.Boogie.VCExprAST { }
}
+ public class VCExprConstant : VCExprVar
+ {
+ internal VCExprConstant(string name, Type type) : base(name,type) {
+ Contract.Requires(type != null);
+ Contract.Requires(name != null);
+ }
+ }
+
public abstract class VCExprBinder : VCExpr {
public readonly VCExpr/*!*/ Body;
public readonly List<TypeVariable/*!*/>/*!*/ TypeParameters;
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index e88c000e..a3f266ef 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -4,6 +4,7 @@ //
//-----------------------------------------------------------------------------
using System;
+using System.Linq;
using System.Collections;
using System.Collections.Generic;
using System.Threading;
@@ -14,8 +15,18 @@ using System.Diagnostics.Contracts; using Microsoft.Boogie.AbstractInterpretation;
using Microsoft.Boogie.VCExprAST;
using Microsoft.Basetypes;
+using System.Threading.Tasks;
namespace Microsoft.Boogie {
+
+ enum CheckerStatus
+ {
+ Idle,
+ Ready,
+ Busy,
+ Closed
+ }
+
/// <summary>
/// Interface to the theorem prover specialized to Boogie.
///
@@ -27,7 +38,6 @@ namespace Microsoft.Boogie { void ObjectInvariant() {
Contract.Invariant(gen != null);
Contract.Invariant(thmProver != null);
- Contract.Invariant(ProverDone != null);
}
private readonly VCExpressionGenerator gen;
@@ -37,18 +47,32 @@ namespace Microsoft.Boogie { // state for the async interface
private volatile ProverInterface.Outcome outcome;
- private volatile bool busy;
private volatile bool hasOutput;
private volatile UnexpectedProverOutputException outputExn;
private DateTime proverStart;
private TimeSpan proverRunTime;
private volatile ProverInterface.ErrorHandler handler;
- private volatile bool closed;
+ private volatile CheckerStatus status;
+ public readonly Program Program;
+
+ public void GetReady()
+ {
+ Contract.Requires(status == CheckerStatus.Idle);
+
+ status = CheckerStatus.Ready;
+ }
- public readonly AutoResetEvent ProverDone = new AutoResetEvent(false);
+ public void GoBackToIdle()
+ {
+ Contract.Requires(IsBusy);
- public bool WillingToHandle(Implementation impl, int timeout) {
- return !closed && timeout == this.timeout;
+ status = CheckerStatus.Idle;
+ }
+
+ public Task ProverTask { get; set; }
+
+ public bool WillingToHandle(int timeout, Program prog) {
+ return status == CheckerStatus.Idle && timeout == this.timeout && (prog == null || Program == prog);
}
public VCExpressionGenerator VCExprGen {
@@ -106,6 +130,7 @@ namespace Microsoft.Boogie { Contract.Requires(vcgen != null);
Contract.Requires(prog != null);
this.timeout = timeout;
+ this.Program = prog;
ProverOptions options = cce.NonNull(CommandLineOptions.Clo.TheProverFactory).BlankProverOptions();
@@ -137,40 +162,7 @@ namespace Microsoft.Boogie { } else {
if (ctx == null) ctx = (ProverContext)CommandLineOptions.Clo.TheProverFactory.NewProverContext(options);
- // set up the context
- foreach (Declaration decl in prog.TopLevelDeclarations) {
- Contract.Assert(decl != null);
- TypeCtorDecl t = decl as TypeCtorDecl;
- if (t != null) {
- ctx.DeclareType(t, null);
- }
- }
- foreach (Declaration decl in prog.TopLevelDeclarations) {
- Contract.Assert(decl != null);
- Constant c = decl as Constant;
- if (c != null) {
- ctx.DeclareConstant(c, c.Unique, null);
- } else {
- Function f = decl as Function;
- if (f != null) {
- ctx.DeclareFunction(f, null);
- }
- }
- }
- foreach (Declaration decl in prog.TopLevelDeclarations) {
- Contract.Assert(decl != null);
- Axiom ax = decl as Axiom;
- if (ax != null) {
- ctx.AddAxiom(ax, null);
- }
- }
- foreach (Declaration decl in prog.TopLevelDeclarations) {
- Contract.Assert(decl != null);
- GlobalVariable v = decl as GlobalVariable;
- if (v != null) {
- ctx.DeclareGlobalVariable(v, null);
- }
- }
+ Setup(prog, ctx);
// we first generate the prover and then store a clone of the
// context in the cache, so that the prover can setup stuff in
@@ -184,13 +176,61 @@ namespace Microsoft.Boogie { this.gen = prover.VCExprGen;
}
+ public void Retarget(Program prog, ProverContext ctx, int timeout = 0)
+ {
+ ctx.Clear();
+ Setup(prog, ctx);
+ if (0 < timeout)
+ {
+ TheoremProver.SetTimeOut(timeout * 1000);
+ }
+ else
+ {
+ TheoremProver.SetTimeOut(0);
+ }
+ TheoremProver.FullReset();
+ }
+
+ private static void Setup(Program prog, ProverContext ctx)
+ {
+ // set up the context
+ foreach (Declaration decl in prog.TopLevelDeclarations.ToList())
+ {
+ Contract.Assert(decl != null);
+ var typeDecl = decl as TypeCtorDecl;
+ var constDecl = decl as Constant;
+ var funDecl = decl as Function;
+ var axiomDecl = decl as Axiom;
+ var glVarDecl = decl as GlobalVariable;
+ if (typeDecl != null)
+ {
+ ctx.DeclareType(typeDecl, null);
+ }
+ else if (constDecl != null)
+ {
+ ctx.DeclareConstant(constDecl, constDecl.Unique, null);
+ }
+ else if (funDecl != null)
+ {
+ ctx.DeclareFunction(funDecl, null);
+ }
+ else if (axiomDecl != null)
+ {
+ ctx.AddAxiom(axiomDecl, null);
+ }
+ else if (glVarDecl != null)
+ {
+ ctx.DeclareGlobalVariable(glVarDecl, null);
+ }
+ }
+ }
/// <summary>
/// Clean-up.
/// </summary>
- public void Close() {
- this.closed = true;
+ public void Close() {
thmProver.Close();
+ status = CheckerStatus.Closed;
}
/// <summary>
@@ -205,13 +245,21 @@ namespace Microsoft.Boogie { public bool IsBusy {
get {
- return busy;
+ return status == CheckerStatus.Busy;
}
}
- public bool Closed {
+ public bool IsClosed {
get {
- return closed;
+ return status == CheckerStatus.Closed;
+ }
+ }
+
+ public bool IsIdle
+ {
+ get
+ {
+ return status == CheckerStatus.Idle;
}
}
@@ -252,39 +300,35 @@ namespace Microsoft.Boogie { break;
}
- Contract.Assert(busy);
hasOutput = true;
proverRunTime = DateTime.UtcNow - proverStart;
-
- ProverDone.Set();
}
public void BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler) {
Contract.Requires(descriptiveName != null);
Contract.Requires(vc != null);
Contract.Requires(handler != null);
+ Contract.Requires(status == CheckerStatus.Ready);
- Contract.Requires(!IsBusy);
- Contract.Assert(!busy);
- busy = true;
+ status = CheckerStatus.Busy;
hasOutput = false;
outputExn = null;
this.handler = handler;
+ thmProver.Reset();
proverStart = DateTime.UtcNow;
thmProver.BeginCheck(descriptiveName, vc, handler);
// gen.ClearSharedFormulas(); PR: don't know yet what to do with this guy
- ThreadPool.QueueUserWorkItem(WaitForOutput);
+ ProverTask = Task.Factory.StartNew(() => { WaitForOutput(null); } , TaskCreationOptions.LongRunning);
}
public ProverInterface.Outcome ReadOutcome() {
-
Contract.Requires(IsBusy);
Contract.Requires(HasOutput);
Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
+
hasOutput = false;
- busy = false;
if (outputExn != null) {
throw outputExn;
@@ -423,6 +467,10 @@ namespace Microsoft.Boogie { public virtual void Close() {
}
+ public abstract void Reset();
+
+ public abstract void FullReset();
+
/// <summary>
/// MSchaef: Allows to Push a VCExpression as Axiom on the prover stack (beta)
/// for now it is only implemented by ProcessTheoremProver and still requires some
@@ -541,6 +589,16 @@ namespace Microsoft.Boogie { Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
throw new NotImplementedException();
}
+
+ public override void Reset()
+ {
+ throw new NotImplementedException();
+ }
+
+ public override void FullReset()
+ {
+ throw new NotImplementedException();
+ }
}
public class ProverException : Exception {
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index a8a95f22..05e79fb0 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -4,6 +4,7 @@ //
//-----------------------------------------------------------------------------
using System;
+using System.Linq;
using System.Collections;
using System.Collections.Generic;
using System.Diagnostics;
@@ -147,20 +148,26 @@ namespace Microsoft.Boogie { return naryExpr.Fun.FunctionName;
}
- public void Print(int indent) {
+ public void Print(int indent, TextWriter tw, Action<Block> blockAction = null) {
int numBlock = -1;
string ind = new string(' ', indent);
foreach (Block b in Trace) {
Contract.Assert(b != null);
numBlock++;
if (b.tok == null) {
- Console.WriteLine("{0}<intermediate block>", ind);
+ tw.WriteLine("{0}<intermediate block>", ind);
} else {
// for ErrorTrace == 1 restrict the output;
// do not print tokens with -17:-4 as their location because they have been
// introduced in the translation and do not give any useful feedback to the user
if (!(CommandLineOptions.Clo.ErrorTrace == 1 && b.tok.line == -17 && b.tok.col == -4)) {
- Console.WriteLine("{4}{0}({1},{2}): {3}", b.tok.filename, b.tok.line, b.tok.col, b.Label, ind);
+ if (blockAction != null)
+ {
+ blockAction(b);
+ }
+
+ tw.WriteLine("{4}{0}({1},{2}): {3}", b.tok.filename, b.tok.line, b.tok.col, b.Label, ind);
+
for (int numInstr = 0; numInstr < b.Cmds.Length; numInstr++)
{
var loc = new TraceLocation(numBlock, numInstr);
@@ -172,13 +179,13 @@ namespace Microsoft.Boogie { {
Contract.Assert(calleeCounterexamples[loc].args.Count == 1);
var arg = calleeCounterexamples[loc].args[0];
- Console.WriteLine("{0}value = {1}", ind, arg.ToString());
+ tw.WriteLine("{0}value = {1}", ind, arg.ToString());
}
else
{
- Console.WriteLine("{1}Inlined call to procedure {0} begins", calleeName, ind);
- calleeCounterexamples[loc].counterexample.Print(indent + 4);
- Console.WriteLine("{1}Inlined call to procedure {0} ends", calleeName, ind);
+ tw.WriteLine("{1}Inlined call to procedure {0} begins", calleeName, ind);
+ calleeCounterexamples[loc].counterexample.Print(indent + 4, tw);
+ tw.WriteLine("{1}Inlined call to procedure {0} ends", calleeName, ind);
}
}
}
@@ -191,7 +198,7 @@ namespace Microsoft.Boogie { public bool ModelHasStatesAlready = false;
- public void PrintModel()
+ public void PrintModel(TextWriter tw)
{
var filename = CommandLineOptions.Clo.ModelViewFile;
if (Model == null || filename == null || CommandLineOptions.Clo.StratifiedInlining > 0) return;
@@ -199,8 +206,8 @@ namespace Microsoft.Boogie { var m = ModelHasStatesAlready ? Model : this.GetModelWithStates();
if (filename == "-") {
- m.Write(Console.Out);
- Console.Out.Flush();
+ m.Write(tw);
+ tw.Flush();
} else {
using (var wr = new StreamWriter(filename, !firstModelFile)) {
firstModelFile = false;
@@ -520,13 +527,13 @@ namespace VC { Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
throw new NotImplementedException();
}
- public ConditionGenerationContracts(Program p)
- : base(p) {
+ public ConditionGenerationContracts(Program p, List<Checker> checkers)
+ : base(p, checkers) {
}
}
[ContractClass(typeof(ConditionGenerationContracts))]
- public abstract class ConditionGeneration {
+ public abstract class ConditionGeneration : IDisposable {
protected internal object CheckerCommonState;
public enum Outcome {
@@ -563,7 +570,10 @@ namespace VC { public int CumulativeAssertionCount; // for statistics
- protected readonly List<Checker>/*!>!*/ checkers = new List<Checker>();
+ protected readonly List<Checker>/*!>!*/ checkers;
+
+ private bool _disposed;
+
protected VariableSeq CurrentLocalVariables = null;
// shared across each implementation; created anew for each implementation
@@ -576,9 +586,11 @@ namespace VC { public static List<Model> errorModelList;
- public ConditionGeneration(Program p) {
- Contract.Requires(p != null);
+ public ConditionGeneration(Program p, List<Checker> checkers) {
+ Contract.Requires(p != null && checkers != null && cce.NonNullElements(checkers));
program = p;
+ this.checkers = checkers;
+ Cores = 1;
}
/// <summary>
@@ -960,35 +972,61 @@ namespace VC { #endregion
- protected Checker FindCheckerFor(Implementation impl, int timeout) {
+ protected Checker FindCheckerFor(int timeout)
+ {
Contract.Ensures(Contract.Result<Checker>() != null);
- int i = 0;
- while (i < checkers.Count) {
- if (checkers[i].Closed) {
- checkers.RemoveAt(i);
- continue;
- } else {
- if (!checkers[i].IsBusy && checkers[i].WillingToHandle(impl, timeout))
- return checkers[i];
+ lock (checkers)
+ {
+ retry:
+ // Look for existing checker.
+ for (int i = 0; i < checkers.Count; i++)
+ {
+ var c = checkers.ElementAt(i);
+ lock (c)
+ {
+ if (c.WillingToHandle(timeout, program))
+ {
+ c.GetReady();
+ return c;
+ }
+ else if (c.IsIdle || c.IsClosed)
+ {
+ if (c.IsIdle)
+ {
+ c.Retarget(program, c.TheoremProver.Context, timeout);
+ return c;
+ }
+ else
+ {
+ checkers.RemoveAt(i);
+ }
+ continue;
+ }
+ }
}
- ++i;
- }
- string log = logFilePath;
- if (log != null && !log.Contains("@PROC@") && checkers.Count > 0)
- log = log + "." + checkers.Count;
- Checker ch = new Checker(this, program, log, appendLogFile, timeout);
- Contract.Assert(ch != null);
- checkers.Add(ch);
- return ch;
+
+ if (Cores <= checkers.Count)
+ {
+ Monitor.Wait(checkers, 50);
+ goto retry;
+ }
+
+ // Create a new checker.
+ string log = logFilePath;
+ if (log != null && !log.Contains("@PROC@") && checkers.Count > 0)
+ {
+ log = log + "." + checkers.Count;
+ }
+ Checker ch = new Checker(this, program, log, appendLogFile, timeout);
+ ch.GetReady();
+ checkers.Add(ch);
+ return ch;
+ }
}
virtual public void Close() {
- foreach (Checker checker in checkers) {
- Contract.Assert(checker != null);
- checker.Close();
- }
}
@@ -1620,6 +1658,26 @@ namespace VC { #endregion
}
+
+ public void Dispose()
+ {
+ Dispose(true);
+ GC.SuppressFinalize(this);
+ }
+
+ protected virtual void Dispose(bool disposing)
+ {
+ if (!_disposed)
+ {
+ if (disposing)
+ {
+ Close();
+ }
+ _disposed = true;
+ }
+ }
+
+ public int Cores { get; set; }
}
public class ModelViewInfo
@@ -1637,10 +1695,10 @@ namespace VC { Contract.Requires(impl != null);
// global variables
- foreach (Declaration d in program.TopLevelDeclarations) {
- if (d is Constant) continue;
- if (d is Variable) {
- AllVariables.Add((Variable)d);
+ foreach (Variable v in program.TopLevelDeclarations.OfType<Variable>()) {
+ if (!(v is Constant))
+ {
+ AllVariables.Add(v);
}
}
// implementation parameters
diff --git a/Source/VCGeneration/Context.cs b/Source/VCGeneration/Context.cs index bf27144b..484ce226 100644 --- a/Source/VCGeneration/Context.cs +++ b/Source/VCGeneration/Context.cs @@ -34,6 +34,7 @@ namespace Microsoft.Boogie public abstract Boogie2VCExprTranslator BoogieExprTranslator { get; }
public abstract VCGenerationOptions VCGenOptions { get; }
public abstract object Clone();
+ public abstract void Clear();
}
[ContractClassFor(typeof(ProverContext))]
@@ -114,6 +115,12 @@ public abstract class ProverContextContracts:ProverContext{ exprTranslator = null;
}
+ public override void Clear()
+ {
+ distincts = new List<Variable>();
+ axiomConjuncts = new List<VCExpr>();
+ }
+
protected DeclFreeProverContext(DeclFreeProverContext ctxt) {
Contract.Requires(ctxt != null);
this.gen = ctxt.gen;
diff --git a/Source/VCGeneration/ExprExtensions.cs b/Source/VCGeneration/ExprExtensions.cs index d63f4fc2..7ebba061 100644 --- a/Source/VCGeneration/ExprExtensions.cs +++ b/Source/VCGeneration/ExprExtensions.cs @@ -21,6 +21,35 @@ using Microsoft.Boogie.VCExprAST; namespace Microsoft.Boogie.ExprExtensions
{
+ class ReferenceComparer<T> : IEqualityComparer<T> where T : class
+ {
+ private static ReferenceComparer<T> m_instance;
+
+ public static ReferenceComparer<T> Instance
+ {
+ get
+ {
+ return m_instance ?? (m_instance = new ReferenceComparer<T>());
+ }
+ }
+
+ public bool Equals(T x, T y)
+ {
+ return ReferenceEquals(x, y);
+ }
+
+ public int GetHashCode(T obj)
+ {
+ return System.Runtime.CompilerServices.RuntimeHelpers.GetHashCode(obj);
+ }
+ }
+
+ public class TermDict<T> : Dictionary<Term, T>
+ {
+ public TermDict() : base(ReferenceComparer<Term>.Instance) { }
+ }
+
+
public enum TermKind { App, Other };
@@ -229,9 +258,9 @@ namespace Microsoft.Boogie.ExprExtensions {
public int cnt = 0;
}
- Dictionary<Term, counter> refcnt = new Dictionary<Term, counter>();
+ TermDict<counter> refcnt = new TermDict<counter>();
List<VCExprLetBinding> bindings = new List<VCExprLetBinding>();
- Dictionary<Term, VCExprVar> bindingMap = new Dictionary<Term, VCExprVar>();
+ TermDict< VCExprVar> bindingMap = new TermDict< VCExprVar>();
int letcnt = 0;
Context ctx;
diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs index e96499fe..3299ef76 100644 --- a/Source/VCGeneration/FixedpointVC.cs +++ b/Source/VCGeneration/FixedpointVC.cs @@ -76,8 +76,10 @@ namespace Microsoft.Boogie Mode mode;
AnnotationStyle style;
- public FixedpointVC( Program _program, string/*?*/ logFilePath, bool appendLogFile)
- : base(_program, logFilePath, appendLogFile)
+ private static Checker old_checker = null;
+
+ public FixedpointVC( Program _program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers)
+ : base(_program, logFilePath, appendLogFile, checkers)
{
switch (CommandLineOptions.Clo.FixedPointMode)
{
@@ -106,7 +108,13 @@ namespace Microsoft.Boogie rpfp = new RPFP(RPFP.CreateLogicSolver(ctx));
program = _program;
gen = ctx;
- checker = new Checker(this, program, logFilePath, appendLogFile, 0, null);
+ if(old_checker == null)
+ checker = new Checker(this, program, logFilePath, appendLogFile, 0, null);
+ else {
+ checker = old_checker;
+ checker.Retarget(program,checker.TheoremProver.Context);
+ }
+ old_checker = checker;
boogieContext = checker.TheoremProver.Context;
linOptions = null; // new Microsoft.Boogie.Z3.Z3LineariserOptions(false, options, new List<VCExprVar>());
}
@@ -660,7 +668,7 @@ namespace Microsoft.Boogie }
}
- private Term ExtractSmallerVCsRec(Dictionary<Term, Term> memo, Term t, List<Term> small, Term lbl = null)
+ private Term ExtractSmallerVCsRec(TermDict< Term> memo, Term t, List<Term> small, Term lbl = null)
{
Term res;
if (memo.TryGetValue(t, out res))
@@ -733,7 +741,7 @@ namespace Microsoft.Boogie }
private void ExtractSmallerVCs(Term t, List<Term> small){
- Dictionary<Term, Term> memo = new Dictionary<Term, Term>();
+ TermDict< Term> memo = new TermDict< Term>();
Term top = ExtractSmallerVCsRec(memo, t, small);
small.Add(top);
}
@@ -763,7 +771,7 @@ namespace Microsoft.Boogie return ctx.MkImplies(ctx.MkAnd(eqns), ctx.MkApp(label, ctx.MkApp(f, tvars)));
}
- private Term MergeGoalsRec(Dictionary<Term, Term> memo, Term t)
+ private Term MergeGoalsRec(TermDict< Term> memo, Term t)
{
Term res;
if (memo.TryGetValue(t, out res))
@@ -803,11 +811,11 @@ namespace Microsoft.Boogie private Term MergeGoals(Term t)
{
- Dictionary<Term, Term> memo = new Dictionary<Term, Term>();
+ TermDict< Term> memo = new TermDict< Term>();
return MergeGoalsRec(memo, t);
}
- private Term CollectGoalsRec(Dictionary<Term, Term> memo, Term t, List<Term> goals, List<Term> cruft)
+ private Term CollectGoalsRec(TermDict< Term> memo, Term t, List<Term> goals, List<Term> cruft)
{
Term res;
if (memo.TryGetValue(t, out res))
@@ -869,11 +877,11 @@ namespace Microsoft.Boogie private void CollectGoals(Term t, List<Term> goals, List<Term> cruft)
{
- Dictionary<Term, Term> memo = new Dictionary<Term, Term>();
+ TermDict< Term> memo = new TermDict< Term>();
CollectGoalsRec(memo, t.GetAppArgs()[1], goals, cruft);
}
- private Term SubstRec(Dictionary<Term, Term> memo, Term t)
+ private Term SubstRec(TermDict< Term> memo, Term t)
{
Term res;
if (memo.TryGetValue(t, out res))
@@ -890,7 +898,7 @@ namespace Microsoft.Boogie return res;
}
- private Term SubstRecGoals(Dictionary<Term, Term> memo, Term t)
+ private Term SubstRecGoals(TermDict< Term> memo, Term t)
{
Term res;
if (memo.TryGetValue(t, out res))
@@ -957,7 +965,7 @@ namespace Microsoft.Boogie CollectGoals(sm, goals,cruft);
foreach (var goal in goals)
{
- Dictionary<Term, Term> memo = new Dictionary<Term, Term>();
+ TermDict< Term> memo = new TermDict< Term>();
foreach (var othergoal in goals)
memo.Add(othergoal, othergoal.Equals(goal) ? ctx.MkFalse() : ctx.MkTrue());
foreach (var thing in cruft)
@@ -967,7 +975,7 @@ namespace Microsoft.Boogie vcs.Add(vc);
}
{
- Dictionary<Term, Term> memo = new Dictionary<Term, Term>();
+ TermDict< Term> memo = new TermDict< Term>();
foreach (var othergoal in goals)
memo.Add(othergoal, ctx.MkTrue());
var vc = SubstRecGoals(memo, sm);
@@ -1078,7 +1086,7 @@ namespace Microsoft.Boogie // Collect the relational paremeters
- private Term CollectParamsRec(Dictionary<Term, Term> memo, Term t, List<FuncDecl> parms, List<RPFP.Node> nodes)
+ private Term CollectParamsRec(TermDict<Term> memo, Term t, List<FuncDecl> parms, List<RPFP.Node> nodes, Dictionary<Term,Term> done)
{
Term res;
if (memo.TryGetValue(t, out res))
@@ -1088,14 +1096,20 @@ namespace Microsoft.Boogie {
var f = t.GetAppDecl();
var args = t.GetAppArgs();
- args = args.Select(x => CollectParamsRec(memo, x, parms, nodes)).ToArray();
+ args = args.Select(x => CollectParamsRec(memo, x, parms, nodes, done)).ToArray();
StratifiedInliningInfo info;
if (relationToProc.TryGetValue(f, out info))
{
- f = SuffixFuncDecl(t, parms.Count);
- parms.Add(f);
- nodes.Add(info.node);
- res = ctx.MkApp(f, args);
+ if (done.ContainsKey(t))
+ res = done[t];
+ else
+ {
+ f = SuffixFuncDecl(t, parms.Count);
+ parms.Add(f);
+ nodes.Add(info.node);
+ res = ctx.MkApp(f, args);
+ done.Add(t,res); // don't count same expression twice!
+ }
}
else
res = ctx.CloneApp(t, args);
@@ -1111,8 +1125,9 @@ namespace Microsoft.Boogie Term[] paramTerms = info.interfaceExprVars.Select(x => boogieContext.VCExprToTerm(x, linOptions)).ToArray();
var relParams = new List<FuncDecl>();
var nodeParams = new List<RPFP.Node>();
- var memo = new Dictionary<Term, Term>();
- vcTerm = CollectParamsRec(memo, vcTerm, relParams, nodeParams);
+ var memo = new TermDict< Term>();
+ var done = new Dictionary<Term,Term>(); // note this hashes on equality, not reference!
+ vcTerm = CollectParamsRec(memo, vcTerm, relParams, nodeParams,done);
// var ops = new Util.ContextOps(ctx);
// var foo = ops.simplify_lhs(vcTerm);
// vcTerm = foo.Item1;
@@ -1430,7 +1445,7 @@ namespace Microsoft.Boogie // start = DateTime.Now;
Counterexample cex = CreateBoogieCounterExample(cexroot.owner, cexroot, impl);
// cexroot.owner.DisposeDualModel();
- cex.Print(0); // TODO: just for testing
+ // cex.Print(0); // just for testing
collector.OnCounterexample(cex, "assertion failure");
Console.WriteLine("cex: {0}s", (DateTime.Now - start).TotalSeconds);
return VC.ConditionGeneration.Outcome.Errors;
@@ -1471,7 +1486,7 @@ namespace Microsoft.Boogie labels = new Dictionary<string, Term>();
foreach(var e in rpfp.edges){
int id = e.number;
- HashSet<Term> memo = new HashSet<Term>();
+ HashSet<Term> memo = new HashSet<Term>(ReferenceComparer<Term>.Instance);
FindLabelsRec(memo, e.F.Formula, labels);
}
}
diff --git a/Source/VCGeneration/RPFP.cs b/Source/VCGeneration/RPFP.cs index f6a42a43..e7df7be6 100644 --- a/Source/VCGeneration/RPFP.cs +++ b/Source/VCGeneration/RPFP.cs @@ -159,7 +159,7 @@ namespace Microsoft.Boogie public Edge map;
public HashSet<string> labels;
internal Term dual;
- internal Dictionary<Term,Term> valuation;
+ internal TermDict<Term> valuation;
}
@@ -263,7 +263,7 @@ namespace Microsoft.Boogie public Term Eval(Edge e, Term t)
{
if (e.valuation == null)
- e.valuation = new Dictionary<Term, Term>();
+ e.valuation = new TermDict< Term>();
if (e.valuation.ContainsKey(t))
return e.valuation[t];
return null; // TODO
@@ -275,7 +275,7 @@ namespace Microsoft.Boogie public void SetValue(Edge e, Term variable, Term value)
{
if (e.valuation == null)
- e.valuation = new Dictionary<Term, Term>();
+ e.valuation = new TermDict< Term>();
e.valuation.Add(variable, value);
}
@@ -369,8 +369,8 @@ namespace Microsoft.Boogie // Collect the relational paremeters
Dictionary<FuncDecl, Node> relationToNode = new Dictionary<FuncDecl, Node>();
-
- private Term CollectParamsRec(Dictionary<Term, Term> memo, Term t, List<FuncDecl> parms, List<RPFP.Node> nodes)
+
+ private Term CollectParamsRec(TermDict<Term> memo, Term t, List<FuncDecl> parms, List<RPFP.Node> nodes, Dictionary<Term, Term> done)
{
Term res;
if (memo.TryGetValue(t, out res))
@@ -381,12 +381,18 @@ namespace Microsoft.Boogie Node node;
if (relationToNode.TryGetValue(f, out node))
{
- f = SuffixFuncDecl(t, parms.Count);
- parms.Add(f);
- nodes.Add(node);
+ if (done.ContainsKey(t))
+ res = done[t];
+ else
+ {
+ f = SuffixFuncDecl(t, parms.Count);
+ parms.Add(f);
+ nodes.Add(node);
+ done.Add(t,res); // don't count same expression twice!
+ }
}
var args = t.GetAppArgs();
- args = args.Select(x => CollectParamsRec(memo, x, parms, nodes)).ToArray();
+ args = args.Select(x => CollectParamsRec(memo, x, parms, nodes, done)).ToArray();
res = ctx.CloneApp(t, args);
} // TODO: handle quantifiers
else
@@ -399,7 +405,7 @@ namespace Microsoft.Boogie {
// TODO: is this right?
// return t.IsFunctionApp() && t.GetAppArgs().Length == 0;
- return t is VCExprVar;
+ return t is VCExprVar && !(t is VCExprConstant);
}
private Edge GetEdgeFromClause(Term t, FuncDecl failName)
@@ -428,8 +434,9 @@ namespace Microsoft.Boogie }
var relParams = new List<FuncDecl>();
var nodeParams = new List<RPFP.Node>();
- var memo = new Dictionary<Term, Term>();
- body = CollectParamsRec(memo, body, relParams, nodeParams);
+ var memo = new TermDict< Term>();
+ var done = new Dictionary<Term, Term>(); // note this hashes on equality, not reference!
+ body = CollectParamsRec(memo, body, relParams, nodeParams,done);
Transformer F = CreateTransformer(relParams.ToArray(), _IndParams, body);
Node parent = relationToNode[Name];
return CreateEdge(parent, F, nodeParams.ToArray());
@@ -504,7 +511,7 @@ namespace Microsoft.Boogie return query;
}
- private void CollectVariables(Dictionary<Term, bool> memo, Term t, List<Term> vars)
+ private void CollectVariables(TermDict< bool> memo, Term t, List<Term> vars)
{
if (memo.ContainsKey(t))
return;
@@ -520,13 +527,13 @@ namespace Microsoft.Boogie private Term BindVariables(Term t, bool universal = true)
{
- Dictionary<Term, bool> memo = new Dictionary<Term,bool>();
+ TermDict< bool> memo = new TermDict<bool>();
List<Term> vars = new List<Term>();
CollectVariables(memo,t,vars);
return universal ? ctx.MkForall(vars.ToArray(), t) : ctx.MkExists(vars.ToArray(), t);
}
- private Term SubstPredsRec(Dictionary<Term, Term> memo, Dictionary<FuncDecl,FuncDecl> subst, Term t)
+ private Term SubstPredsRec(TermDict< Term> memo, Dictionary<FuncDecl,FuncDecl> subst, Term t)
{
Term res;
if (memo.TryGetValue(t, out res))
@@ -554,7 +561,7 @@ namespace Microsoft.Boogie private Term SubstPreds(Dictionary<FuncDecl, FuncDecl> subst, Term t)
{
- Dictionary<Term, Term> memo = new Dictionary<Term, Term>();
+ TermDict< Term> memo = new TermDict< Term>();
return SubstPredsRec(memo, subst, t);
}
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 81c37d8d..f90788d7 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -309,8 +309,8 @@ namespace VC { public Dictionary<string, StratifiedInliningInfo> implName2StratifiedInliningInfo;
public ProverInterface prover;
- public StratifiedVCGenBase(Program program, string/*?*/ logFilePath, bool appendLogFile)
- : base(program, logFilePath, appendLogFile) {
+ public StratifiedVCGenBase(Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers)
+ : base(program, logFilePath, appendLogFile, checkers) {
implName2StratifiedInliningInfo = new Dictionary<string, StratifiedInliningInfo>();
prover = ProverInterface.CreateProver(program, logFilePath, appendLogFile, CommandLineOptions.Clo.ProverKillTime);
foreach (Declaration decl in program.TopLevelDeclarations) {
@@ -510,8 +510,8 @@ namespace VC { public StratifiedVCGen(bool usePrevCallTree, Dictionary<string, int> prevCallTree,
HashSet<string> procsToSkip, Dictionary<string, int> extraRecBound,
- Program program, string/*?*/ logFilePath, bool appendLogFile)
- : this(program, logFilePath, appendLogFile)
+ Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers)
+ : this(program, logFilePath, appendLogFile, checkers)
{
this.procsToSkip = new HashSet<string>(procsToSkip);
this.extraRecBound = new Dictionary<string, int>(extraRecBound);
@@ -525,8 +525,8 @@ namespace VC { }
}
- public StratifiedVCGen(Program program, string/*?*/ logFilePath, bool appendLogFile)
- : base(program, logFilePath, appendLogFile) {
+ public StratifiedVCGen(Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers)
+ : base(program, logFilePath, appendLogFile, checkers) {
PersistCallTree = false;
useSummary = false;
procsThatReachedRecBound = new HashSet<string>();
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 6a0891b8..48b73bce 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -18,6 +18,7 @@ using Microsoft.Boogie.VCExprAST; namespace VC {
using Bpl = Microsoft.Boogie;
+ using System.Threading.Tasks;
public class VCGen : ConditionGeneration {
private const bool _print_time = false;
@@ -25,8 +26,8 @@ namespace VC { /// Constructor. Initializes the theorem prover.
/// </summary>
[NotDelayed]
- public VCGen(Program program, string/*?*/ logFilePath, bool appendLogFile)
- : base(program)
+ public VCGen(Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers)
+ : base(program, checkers)
{
Contract.Requires(program != null);
this.appendLogFile = appendLogFile;
@@ -290,7 +291,7 @@ namespace VC { ModelViewInfo mvInfo;
parent.PassifyImpl(impl, out mvInfo);
Hashtable label2Absy;
- Checker ch = parent.FindCheckerFor(impl, CommandLineOptions.Clo.SmokeTimeout);
+ Checker ch = parent.FindCheckerFor(CommandLineOptions.Clo.SmokeTimeout);
Contract.Assert(ch != null);
var exprGen = ch.TheoremProver.Context.ExprGen;
@@ -312,8 +313,9 @@ namespace VC { Emit();
}
ch.BeginCheck(cce.NonNull(impl.Name + "_smoke" + id++), vc, new ErrorHandler(label2Absy, this.callback));
- ch.ProverDone.WaitOne();
+ ch.ProverTask.Wait();
ProverInterface.Outcome outcome = ch.ReadOutcome();
+ ch.GoBackToIdle();
parent.CurrentLocalVariables = null;
DateTime end = DateTime.UtcNow;
@@ -1135,10 +1137,10 @@ namespace VC { }
}
- public WaitHandle ProverDone {
+ public Task ProverTask {
get {
Contract.Assert(checker != null);
- return checker.ProverDone;
+ return checker.ProverTask;
}
}
@@ -1191,7 +1193,7 @@ namespace VC { impl.Blocks = blocks;
- checker = parent.FindCheckerFor(impl, timeout);
+ checker = parent.FindCheckerFor(timeout);
Hashtable/*<int, Absy!>*/ label2absy = new Hashtable/*<int, Absy!>*/();
ProverInterface tp = checker.TheoremProver;
@@ -1200,7 +1202,7 @@ namespace VC { bet.SetCodeExprConverter(
new CodeExprConverter(
delegate (CodeExpr codeExpr, Hashtable/*<Block, VCExprVar!>*/ blockVariables, List<VCExprLetBinding/*!*/> bindings) {
- VCGen vcgen = new VCGen(new Program(), null, false);
+ VCGen vcgen = new VCGen(new Program(), null, false, parent.checkers);
vcgen.variable2SequenceNumber = new Hashtable/*Variable -> int*/();
vcgen.incarnationOriginMap = new Dictionary<Incarnation, Absy>();
vcgen.CurrentLocalVariables = codeExpr.LocVars;
@@ -1410,7 +1412,11 @@ namespace VC { }
ModelViewInfo mvInfo;
- Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = PassifyImpl(impl, out mvInfo);
+ Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins;
+ lock (program)
+ {
+ gotoCmdOrigins = PassifyImpl(impl, out mvInfo);
+ }
double max_vc_cost = CommandLineOptions.Clo.VcsMaxCost;
int tmp_max_vc_cost = -1, max_splits = CommandLineOptions.Clo.VcsMaxSplits,
@@ -1424,7 +1430,7 @@ namespace VC { Outcome outcome = Outcome.Correct;
- int cores = CommandLineOptions.Clo.VcsCores;
+ Cores = CommandLineOptions.Clo.VcsCores;
Stack<Split> work = new Stack<Split>();
List<Split> currently_running = new List<Split>();
ResetPredecessors(impl.Blocks);
@@ -1441,11 +1447,11 @@ namespace VC { remaining_cost = work.Peek().Cost;
}
- while (work.Count > 0 || currently_running.Count > 0) {
+ while (work.Any() || currently_running.Any()) {
bool prover_failed = false;
Split s;
- if (work.Count > 0 && currently_running.Count < cores) {
+ if (work.Any() && currently_running.Count < Cores) {
s = work.Pop();
if (first_round && max_splits > 1) {
@@ -1459,21 +1465,22 @@ namespace VC { callback.OnProgress("VCprove", no < 0 ? 0 : no, total, proven_cost / (remaining_cost + proven_cost));
Contract.Assert(s.parent == this);
- s.BeginCheck(callback, mvInfo, no,
- (keep_going && s.LastChance) ? CommandLineOptions.Clo.VcsFinalAssertTimeout :
- keep_going ? CommandLineOptions.Clo.VcsKeepGoingTimeout :
- CommandLineOptions.Clo.ProverKillTime);
+ lock (program)
+ {
+ s.BeginCheck(callback, mvInfo, no,
+ (keep_going && s.LastChance) ? CommandLineOptions.Clo.VcsFinalAssertTimeout :
+ keep_going ? CommandLineOptions.Clo.VcsKeepGoingTimeout :
+ CommandLineOptions.Clo.ProverKillTime);
+ }
no++;
currently_running.Add(s);
}
} else {
- WaitHandle[] handles = new WaitHandle[currently_running.Count];
- for (int i = 0; i < currently_running.Count; ++i) {
- handles[i] = currently_running[i].ProverDone;
- }
- int index = WaitHandle.WaitAny(handles);
+ // Wait for one split to terminate.
+ var tasks = currently_running.Select(splt => splt.ProverTask).ToArray();
+ int index = Task.WaitAny(tasks);
s = currently_running[index];
currently_running.RemoveAt(index);
@@ -1504,6 +1511,8 @@ namespace VC { break;
}
+ s.Checker.GoBackToIdle();
+
Contract.Assert( prover_failed || outcome == Outcome.Correct || outcome == Outcome.Errors || outcome == Outcome.Inconclusive);
}
@@ -1547,7 +1556,10 @@ namespace VC { }
if (outcome == Outcome.Correct && smoke_tester != null) {
- smoke_tester.Test();
+ lock (program)
+ {
+ smoke_tester.Test();
+ }
}
callback.OnProgress("done", 0, 0, 1.0);
diff --git a/Test/AbsHoudini/imp1.bpl b/Test/AbsHoudini/imp1.bpl new file mode 100644 index 00000000..29cbf567 --- /dev/null +++ b/Test/AbsHoudini/imp1.bpl @@ -0,0 +1,21 @@ +function {:existential true} {:absdomain "ImplicationDomain"} b1(x1: bool, x2: bool) : bool;
+function {:existential true} {:absdomain "ImplicationDomain"} b2(x1: bool, x2: bool) : bool;
+
+var x: int;
+var flag: bool;
+
+procedure foo ()
+ modifies x, flag;
+ ensures b1(flag, x == 0);
+{
+ flag := true;
+ x := 0;
+}
+
+procedure bar()
+ modifies x, flag;
+ ensures b2(flag, x == 0);
+{
+ flag := false;
+ x := 0;
+}
diff --git a/Test/AbsHoudini/multi.bpl b/Test/AbsHoudini/multi.bpl new file mode 100644 index 00000000..a33817ac --- /dev/null +++ b/Test/AbsHoudini/multi.bpl @@ -0,0 +1,67 @@ +function {:existential true} {:absdomain "ImplicationDomain"} b1(x1: bool, x2: bool) : bool;
+function {:existential true} {:absdomain "ImplicationDomain"} b2(x1: bool, x2: bool) : bool;
+function {:existential true} {:absdomain "PowDomain"} b3(x1: int) : bool;
+function {:existential true} {:absdomain "PowDomain"} b4(x1: bv32) : bool;
+function {:existential true} {:absdomain "EqualitiesDomain"} b5(x: int, y: int, z: int, w:int) : bool;
+
+function {:builtin "bvslt"} BV_SLT(x: bv32, y: bv32) : bool;
+
+var x: int;
+var flag: bool;
+
+// Test implication domain
+procedure foo ()
+ modifies x, flag;
+{
+ flag := true;
+ x := 0;
+ assert b1(flag, x == 0);
+ flag := false;
+ assert b2(flag, x == 0);
+}
+
+// Test for PowDomain(int)
+procedure bar1 ()
+ modifies x, flag;
+{
+ x := 2;
+ if(*) { x := 16; }
+ assert b3(x);
+}
+
+// Test for PowDomain(bv32)
+procedure bar2 ()
+ modifies x, flag;
+{
+ var s: bv32;
+
+ s := 2bv32;
+ if(*) { s := 16bv32; }
+ assert b4(s);
+}
+
+// Test for EqualitiesDomain
+procedure baz ()
+ modifies x, flag;
+{
+ var y: int;
+ var z: int;
+ var w: int;
+
+ assume x == y;
+ assume x == z;
+
+ if(*) {
+ x := x + 1;
+ y := y + 1;
+ } else {
+ x := x + 2;
+ y := y + 2;
+ }
+
+ assume x == w;
+
+ assert b5(x,y,z,w);
+}
+
+
diff --git a/Test/aitest0/Answer b/Test/aitest0/Answer index dabe9710..961b3c33 100644 --- a/Test/aitest0/Answer +++ b/Test/aitest0/Answer @@ -124,5 +124,45 @@ Execution trace: Intervals.bpl(87,5): anon0
Intervals.bpl(88,3): loop_head
Intervals.bpl(91,3): after_loop
+Intervals.bpl(138,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Intervals.bpl(133,5): anon0
+ Intervals.bpl(134,3): anon3_LoopHead
+ Intervals.bpl(134,3): anon3_LoopDone
+Intervals.bpl(149,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Intervals.bpl(144,5): anon0
+ Intervals.bpl(145,3): anon3_LoopHead
+ Intervals.bpl(145,3): anon3_LoopDone
+Intervals.bpl(200,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Intervals.bpl(190,8): anon0
+ Intervals.bpl(191,3): anon4_LoopHead
+ Intervals.bpl(191,3): anon4_LoopDone
+Intervals.bpl(238,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Intervals.bpl(233,5): anon0
+ Intervals.bpl(234,3): anon3_LoopHead
+ Intervals.bpl(234,3): anon3_LoopDone
+Intervals.bpl(250,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Intervals.bpl(244,8): anon0
+ Intervals.bpl(245,3): anon3_LoopHead
+ Intervals.bpl(245,3): anon3_LoopDone
+Intervals.bpl(261,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Intervals.bpl(256,5): anon0
+ Intervals.bpl(257,3): anon3_LoopHead
+ Intervals.bpl(257,3): anon3_LoopDone
+Intervals.bpl(283,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Intervals.bpl(278,5): anon0
+ Intervals.bpl(279,3): anon3_LoopHead
+ Intervals.bpl(279,3): anon3_LoopDone
+Intervals.bpl(305,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Intervals.bpl(300,5): anon0
+ Intervals.bpl(301,3): anon3_LoopHead
+ Intervals.bpl(301,3): anon3_LoopDone
-Boogie program verifier finished with 5 verified, 3 errors
+Boogie program verifier finished with 15 verified, 11 errors
diff --git a/Test/aitest0/Intervals.bpl b/Test/aitest0/Intervals.bpl index 4520a032..6a588bbe 100644 --- a/Test/aitest0/Intervals.bpl +++ b/Test/aitest0/Intervals.bpl @@ -91,3 +91,228 @@ procedure UnaryNegation1() returns (x: int) // this was once buggy after_loop:
assert x == 1; // error
}
+
+// --------------------------- test {:identity} annotation --------------------
+
+function {:identity} MyId(x: int): int;
+function MyStealthyId(x: int): int; // this one messes up the abstract interpretation
+function {:identity false} {:identity}/*the last attribute rules*/ MyPolyId<T>(x: T): T;
+function {:identity /*this is a lie*/} MyBogusId(x: int): int { -x }
+function {:identity /*ignored, since the function takes more than one argument*/} MultipleArgs(x: int, y: int): int;
+function {:identity /*ignored, since the return type is not equal to the argument type*/} BoolToInt(b: bool): int;
+function {:identity true/*in some contexts, the type of this function makes sense as an identity*/} SometimesId0<T>(x: T): int;
+function {:identity true/*in some contexts, the type of this function makes sense as an identity*/} SometimesId1<T>(x: int): T;
+function {:identity true/*in some contexts, the type of this function makes sense as an identity*/} SometimesId2<T,U>(x: T): U;
+
+
+procedure Id0(n: int)
+{
+ var i: int;
+ i := 0;
+ while (i < n)
+ {
+ i := i + 1;
+ }
+ assert 0 <= i;
+}
+
+procedure Id1(n: int)
+{
+ var i: int;
+ i := MyId(0);
+ while (i < n)
+ {
+ i := i + MyId(1);
+ }
+ assert 0 <= i;
+}
+
+procedure Id2(n: int)
+{
+ var i: int;
+ i := MyStealthyId(0);
+ while (i < n)
+ {
+ i := i + 1;
+ }
+ assert 0 <= i; // error: abstract interpreter does not figure this one out
+}
+
+procedure Id3(n: int)
+{
+ var i: int;
+ i := 0;
+ while (i < n)
+ {
+ i := i + MyStealthyId(1);
+ }
+ assert 0 <= i; // error: abstract interpreter does not figure this one out
+}
+
+procedure Id4(n: int)
+{
+ var i: int;
+ i := MyPolyId(0);
+ while (i < n)
+ {
+ i := i + MyPolyId(1);
+ }
+ assert 0 <= i;
+}
+
+procedure Id5(n: int)
+{
+ var i: int;
+ var b: bool;
+ i, b := 0, false;
+ while (i < n)
+ {
+ i, b := i + 1, false;
+ }
+ assert !b;
+}
+
+procedure Id6(n: int)
+{
+ var i: int;
+ var b: bool;
+ i, b := 0, MyPolyId(false);
+ while (i < n)
+ {
+ i, b := i + 1, false;
+ }
+ assert !b;
+}
+
+procedure Id7(n: int)
+{
+ var i, k, y, z: int;
+ i, k := 0, 0;
+ while (i < n)
+ {
+ i := i + 1;
+ y, z := MyBogusId(5), -5;
+ k := k + z;
+ if (*) {
+ assert y == z; // fine
+ }
+ }
+ assert 0 <= k; // error: this does not hold -- k may very well be negative
+}
+
+procedure Id8(n: int)
+{
+ var i, k: int;
+ i, k := 0, 0;
+ while (i < n)
+ {
+ i := i + 1;
+ k := k + MyBogusId(5);
+ }
+ assert 0 <= k; // since we lied about MyBogusId being an {:identity} function, the abstract interpreter gives us this bogus invariant
+}
+
+procedure Id9(n: int)
+ requires 0 < n;
+{
+ var i, k: int;
+ i, k := 0, 0;
+ while (i < n)
+ invariant i <= n && -k == 5*i;
+ {
+ i := i + 1;
+ k := k + MyBogusId(5);
+ }
+ assert -k == 5*n;
+ assert false; // this just shows the effect of MyBogusId even more; there is no complaint about this assert
+}
+
+procedure Id10(n: int)
+{
+ var i: int;
+ i := 0;
+ while (i < n)
+ {
+ i := i + MultipleArgs(19, 23);
+ }
+ assert 0 <= i; // error: no information is known about i
+}
+
+procedure Id11(n: int)
+{
+ var i, k: int;
+ i, k := 0, 0;
+ while (i < n)
+ {
+ i := i + 1;
+ k := k + BoolToInt(false); // this should not be treated as an identity function, since it goes from one type to another
+ }
+ assert 0 <= k; // error: no information is known about k
+}
+
+procedure Id12(n: int)
+{
+ var i: int;
+ i := 0;
+ while (i < n)
+ {
+ i := i + SometimesId0(false);
+ }
+ assert 0 <= i; // error: no information is known about i
+}
+
+procedure Id13(n: int)
+{
+ var i: int;
+ i := 0;
+ while (i < n)
+ {
+ i := i + SometimesId0(1);
+ }
+ assert 0 <= i;
+}
+
+procedure Id14(n: int)
+{
+ var i: int;
+ i := 0;
+ while (i < n)
+ {
+ i := i + SometimesId0(-1);
+ }
+ assert 0 <= i; // error: this does not hold
+}
+
+procedure Id15(n: int)
+{
+ var i: int;
+ i := 0;
+ while (i < n)
+ {
+ i := i + SometimesId1(1);
+ }
+ assert 0 <= i; // fine: SometimesId1 claims to be an identity and the use of it is int->int
+}
+
+procedure Id16(n: int)
+{
+ var i: int;
+ i := 0;
+ while (i < n)
+ {
+ i := i + SometimesId2(false);
+ }
+ assert 0 <= i; // error: no information is known about i
+}
+
+procedure Id17(n: int)
+{
+ var i: int;
+ i := 0;
+ while (i < n)
+ {
+ i := i + SometimesId2(1);
+ }
+ assert 0 <= i; // fine: SometimesId2 claims to be an identity and the use of it is int->int
+}
+
diff --git a/Test/snapshots/Snapshots4.v0.bpl b/Test/snapshots/Snapshots4.v0.bpl new file mode 100644 index 00000000..430aee99 --- /dev/null +++ b/Test/snapshots/Snapshots4.v0.bpl @@ -0,0 +1,36 @@ +procedure {:checksum "P0$proc#0"} P0();
+// Action: verify
+implementation {:checksum "P0$impl#0"} P0()
+{
+}
+
+
+procedure {:checksum "P1$proc#0"} P1();
+// Action: verify
+implementation {:checksum "P1$impl#0"} P1()
+{
+ call P2();
+}
+
+
+procedure {:checksum "P2$proc#0"} P2();
+ ensures G();
+
+
+procedure {:checksum "P3$proc#0"} P3();
+// Action: verify
+implementation {:checksum "P3$impl#0"} P3()
+{
+}
+
+
+function {:checksum "G#0"} G() : bool
+{
+ F()
+}
+
+
+function {:checksum "F#0"} F() : bool
+{
+ true
+}
diff --git a/Test/snapshots/Snapshots4.v1.bpl b/Test/snapshots/Snapshots4.v1.bpl new file mode 100644 index 00000000..025a3f5f --- /dev/null +++ b/Test/snapshots/Snapshots4.v1.bpl @@ -0,0 +1,45 @@ +procedure {:checksum "P0$proc#0"} P0();
+// Action: skip
+// Priority: 0
+implementation {:checksum "P0$impl#0"} P0()
+{
+}
+
+
+procedure {:checksum "P1$proc#0"} P1();
+// Action: verify
+// Priority: 1
+implementation {:checksum "P1$impl#0"} P1()
+{
+ call P2();
+}
+
+
+procedure {:checksum "P3$proc#0"} P3();
+// Action: verify
+// Priority: 2
+implementation {:checksum "P3$impl#1"} P3()
+{
+ assert false;
+}
+
+
+procedure {:checksum "P2$proc#0"} P2();
+ ensures G();
+// Action: verify
+// Priority: 3
+implementation {:checksum "P2$impl#0"} P2()
+{
+}
+
+
+function {:checksum "G#0"} G() : bool
+{
+ F()
+}
+
+
+function {:checksum "F#1"} F() : bool
+{
+ false
+}
|