diff options
| -rw-r--r-- | Source/Core/Absy.cs | 11 | ||||
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 9 | ||||
| -rw-r--r-- | Source/Core/LinearSets.cs | 63 | ||||
| -rw-r--r-- | Source/Core/OwickiGries.cs | 12 | ||||
| -rw-r--r-- | Source/Doomed/DoomCheck.cs | 23 | ||||
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 124 | ||||
| -rw-r--r-- | Source/Houdini/Checker.cs | 2 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 1300 | ||||
| -rw-r--r-- | Source/VCExpr/Boogie2VCExpr.cs | 75 | ||||
| -rw-r--r-- | Source/VCExpr/NameClashResolver.cs | 18 | ||||
| -rw-r--r-- | Source/VCGeneration/Check.cs | 155 | ||||
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 58 | ||||
| -rw-r--r-- | Source/VCGeneration/Context.cs | 23 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.cs | 313 | ||||
| -rw-r--r-- | Test/linear/typecheck.bpl | 21 | ||||
| -rw-r--r-- | Test/og/Answer | 9 | ||||
| -rw-r--r-- | Test/og/async.bpl | 16 | ||||
| -rw-r--r-- | Test/og/runtest.bat | 2 | ||||
| -rw-r--r-- | Test/snapshots/Answer | 8 | ||||
| -rw-r--r-- | Test/snapshots/runtest.bat | 7 | ||||
| -rw-r--r-- | Test/test2/Answer | 44 | ||||
| -rw-r--r-- | Test/test2/Timeouts0.bpl | 58 |
22 files changed, 1355 insertions, 996 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 39343e6f..5e69b179 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -1186,6 +1186,15 @@ namespace Microsoft.Boogie { }
}
+ public int TimeLimit
+ {
+ get
+ {
+ int tl = CommandLineOptions.Clo.ProverKillTime;
+ CheckIntAttribute("timeLimit", ref tl);
+ return tl;
+ }
+ }
public NamedDeclaration(IToken/*!*/ tok, string/*!*/ name)
: base(tok) {
@@ -2608,7 +2617,7 @@ namespace Microsoft.Boogie { var id = FindStringAttribute("id");
if (id == null)
{
- id = Name + ":0";
+ id = Name + GetHashCode().ToString() + ":0";
}
return id;
}
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index df49740e..a1a4d740 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -364,6 +364,7 @@ namespace Microsoft.Boogie { }
public bool VerifySnapshots;
+ public bool VerifySeparately;
public string PrintFile = null;
public int PrintUnstructured = 0;
public int DoomStrategy = -1;
@@ -1328,7 +1329,8 @@ namespace Microsoft.Boogie { ps.CheckBooleanFlag("useProverEvaluate", ref UseProverEvaluate) ||
ps.CheckBooleanFlag("nonUniformUnfolding", ref NonUniformUnfolding) ||
ps.CheckBooleanFlag("deterministicExtractLoops", ref DeterministicExtractLoops) ||
- ps.CheckBooleanFlag("verifySnapshots", ref VerifySnapshots)
+ ps.CheckBooleanFlag("verifySnapshots", ref VerifySnapshots) ||
+ ps.CheckBooleanFlag("verifySeparately", ref VerifySeparately)
) {
// one of the boolean flags matched
return true;
@@ -1496,6 +1498,9 @@ namespace Microsoft.Boogie { Assign a unique ID to an implementation to be used for verification
result caching (default: ""<impl. name>:0"").
+ {:timeLimit N}
+ Set the time limit for a given implementation.
+
---- On functions ----------------------------------------------------------
{:builtin ""spec""}
@@ -1648,6 +1653,8 @@ namespace Microsoft.Boogie { /verifySnapshots
verify several program snapshots (named <filename>.v0.bpl
to <filename>.vN.bpl) using verification result caching
+ /verifySeparately
+ verify each input program separately
/removeEmptyBlocks:<c>
0 - do not remove empty blocks during VC generation
1 - remove empty blocks (default)
diff --git a/Source/Core/LinearSets.cs b/Source/Core/LinearSets.cs index 84ce264d..27312f38 100644 --- a/Source/Core/LinearSets.cs +++ b/Source/Core/LinearSets.cs @@ -156,24 +156,33 @@ namespace Microsoft.Boogie else if (cmd is CallCmd)
{
CallCmd callCmd = (CallCmd)cmd;
- for (int i = 0; i < callCmd.Proc.InParams.Count; i++)
+ while (callCmd != null)
{
- if (FindDomainName(callCmd.Proc.InParams[i]) == null) continue;
- IdentifierExpr ie = callCmd.Ins[i] as IdentifierExpr;
- if (start.Contains(ie.Decl))
- {
- start.Remove(ie.Decl);
- }
- else
+ for (int i = 0; i < callCmd.Proc.InParams.Count; i++)
{
- Error(ie, "unavailable source for a linear read");
+ if (FindDomainName(callCmd.Proc.InParams[i]) == null) continue;
+ IdentifierExpr ie = callCmd.Ins[i] as IdentifierExpr;
+ if (start.Contains(ie.Decl))
+ {
+ start.Remove(ie.Decl);
+ }
+ else
+ {
+ Error(ie, "unavailable source for a linear read");
+ }
}
+ callCmd = callCmd.InParallelWith;
}
+ callCmd = (CallCmd)cmd;
availableLocalLinearVars[callCmd] = new HashSet<Variable>(start);
- foreach (IdentifierExpr ie in callCmd.Outs)
+ while (callCmd != null)
{
- if (FindDomainName(ie.Decl) == null) continue;
- start.Add(ie.Decl);
+ foreach (IdentifierExpr ie in callCmd.Outs)
+ {
+ if (FindDomainName(ie.Decl) == null) continue;
+ start.Add(ie.Decl);
+ }
+ callCmd = callCmd.InParallelWith;
}
}
else if (cmd is HavocCmd)
@@ -356,19 +365,6 @@ namespace Microsoft.Boogie return base.VisitCallCmd(node);
}
- private void TransformCallCmd(CallCmd callCmd, Dictionary<string, Expr> domainNameToExpr)
- {
- foreach (var domainName in linearDomains.Keys)
- {
- callCmd.Ins.Add(domainNameToExpr[domainName]);
- }
- CallCmd parallelCallCmd = callCmd.InParallelWith;
- if (parallelCallCmd != null)
- {
- TransformCallCmd(parallelCallCmd, domainNameToExpr);
- }
- }
-
private void AddDisjointnessExpr(CmdSeq newCmds, Absy absy, Dictionary<string, Variable> domainNameToInputVar)
{
Dictionary<string, HashSet<Variable>> domainNameToScope = new Dictionary<string, HashSet<Variable>>();
@@ -427,6 +423,18 @@ namespace Microsoft.Boogie callCmd.Ins.Add(new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new ExprSeq(Expr.False)));
}
}
+ else if (callCmd.InParallelWith != null)
+ {
+ while (callCmd != null)
+ {
+ foreach (var domainName in linearDomains.Keys)
+ {
+ var domain = linearDomains[domainName];
+ callCmd.Ins.Add(new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new ExprSeq(Expr.False)));
+ }
+ callCmd = callCmd.InParallelWith;
+ }
+ }
else
{
Dictionary<string, Expr> domainNameToExpr = new Dictionary<string, Expr>();
@@ -441,7 +449,10 @@ namespace Microsoft.Boogie IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v);
domainNameToExpr[domainName] = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new ExprSeq(v.TypedIdent.Type is MapType ? ie : Singleton(ie, domainName), domainNameToExpr[domainName]));
}
- TransformCallCmd(callCmd, domainNameToExpr);
+ foreach (var domainName in linearDomains.Keys)
+ {
+ callCmd.Ins.Add(domainNameToExpr[domainName]);
+ }
}
}
else if (cmd is YieldCmd)
diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs index 14f5f328..e353700f 100644 --- a/Source/Core/OwickiGries.cs +++ b/Source/Core/OwickiGries.cs @@ -131,7 +131,7 @@ namespace Microsoft.Boogie public override Cmd VisitCallCmd(CallCmd node)
{
ProcedureInfo info = procNameToInfo[node.callee];
- if (!node.IsAsync && !info.isAtomic)
+ if (node.InParallelWith != null || node.IsAsync || !info.isAtomic)
{
procNameToInfo[currentImpl.Name].isAtomic = false;
moreProcessingRequired = true;
@@ -487,6 +487,10 @@ namespace Microsoft.Boogie CallCmd callCmd = cmd as CallCmd;
if (callCmd != null)
{
+ if (callCmd.InParallelWith != null || callCmd.IsAsync || !procNameToInfo[callCmd.callee].isAtomic)
+ {
+ AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar);
+ }
if (callCmd.InParallelWith != null)
{
List<Expr> ins;
@@ -507,14 +511,12 @@ namespace Microsoft.Boogie dummyCallCmd.Proc = dummyAsyncTargetProc;
newCmds.Add(dummyCallCmd);
}
- else if (procNameToInfo[callCmd.callee].isAtomic)
+ else
{
newCmds.Add(callCmd);
}
- else
+ if (callCmd.InParallelWith != null || callCmd.IsAsync || !procNameToInfo[callCmd.callee].isAtomic)
{
- AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar);
- newCmds.Add(callCmd);
HashSet<Variable> availableLocalLinearVars = new HashSet<Variable>(linearTypechecker.availableLocalLinearVars[callCmd]);
foreach (IdentifierExpr ie in callCmd.Outs)
{
diff --git a/Source/Doomed/DoomCheck.cs b/Source/Doomed/DoomCheck.cs index 7e2ec984..b317dc71 100644 --- a/Source/Doomed/DoomCheck.cs +++ b/Source/Doomed/DoomCheck.cs @@ -115,21 +115,26 @@ void ObjectInvariant() // Todo: Check if vc is trivial true or false
outcome = ProverInterface.Outcome.Undetermined;
- Contract.Assert( m_ErrorHandler !=null);
- m_Checker.BeginCheck(lv[0].Name, vc, m_ErrorHandler);
- m_Checker.ProverTask.Wait();
-
- try {
+ Contract.Assert(m_ErrorHandler != null);
+ try
+ {
+ m_Checker.BeginCheck(lv[0].Name, vc, m_ErrorHandler);
+ m_Checker.ProverTask.Wait();
outcome = m_Checker.ReadOutcome();
- m_Checker.GoBackToIdle();
- } catch (UnexpectedProverOutputException e)
+ }
+ catch (UnexpectedProverOutputException e)
{
- if (CommandLineOptions.Clo.TraceVerify) {
+ if (CommandLineOptions.Clo.TraceVerify)
+ {
Console.WriteLine("Prover is unable to check {0}! Reason:", lv[0].Name);
Console.WriteLine(e.ToString());
}
return false;
- }
+ }
+ finally
+ {
+ m_Checker.GoBackToIdle();
+ }
return true;
}
}
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 21d0c014..96c294ea 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -141,6 +141,7 @@ namespace Microsoft.Boogie }
tw.Write(errorInfo.Out.ToString());
+ tw.Write(errorInfo.Model.ToString());
tw.Flush();
}
@@ -235,6 +236,7 @@ namespace Microsoft.Boogie public ErrorKind Kind { get; set; }
public string ImplementationName { get; set; }
public TextWriter Out = new StringWriter();
+ public TextWriter Model = new StringWriter();
public string FullMsg
{
@@ -355,14 +357,27 @@ namespace Microsoft.Boogie public static ErrorInformationFactory errorInformationFactory = new ErrorInformationFactory();
public readonly static VerificationResultCache Cache = new VerificationResultCache();
+
+ static List<Checker> Checkers = new List<Checker>();
- static LinearTypechecker linearTypechecker;
+ static IDictionary<string, CancellationTokenSource> ImplIdToCancellationTokenSource = new ConcurrentDictionary<string, CancellationTokenSource>();
+
+ static IDictionary<string, IList<CancellationTokenSource>> RequestIdToCancellationTokenSources = new ConcurrentDictionary<string, IList<CancellationTokenSource>>();
public static void ProcessFiles(List<string> fileNames, bool lookForSnapshots = true)
{
Contract.Requires(cce.NonNullElements(fileNames));
+ if (CommandLineOptions.Clo.VerifySeparately && 1 < fileNames.Count)
+ {
+ foreach (var f in fileNames)
+ {
+ ProcessFiles(new List<string> { f }, lookForSnapshots);
+ }
+ return;
+ }
+
if (CommandLineOptions.Clo.VerifySnapshots && lookForSnapshots)
{
var snapshotsByVersion = new List<List<string>>();
@@ -404,7 +419,8 @@ namespace Microsoft.Boogie PrintBplFile(CommandLineOptions.Clo.PrintFile, program, false);
}
- PipelineOutcome oc = ResolveAndTypecheck(program, fileNames[fileNames.Count - 1]);
+ LinearTypechecker linearTypechecker;
+ PipelineOutcome oc = ResolveAndTypecheck(program, fileNames[fileNames.Count - 1], out linearTypechecker);
if (oc != PipelineOutcome.ResolvedAndTypeChecked)
return;
@@ -572,10 +588,13 @@ namespace Microsoft.Boogie /// - TypeCheckingError if a type checking error occurred
/// - ResolvedAndTypeChecked if both resolution and type checking succeeded
/// </summary>
- public static PipelineOutcome ResolveAndTypecheck(Program program, string bplFileName)
+ public static PipelineOutcome ResolveAndTypecheck(Program program, string bplFileName, out LinearTypechecker linearTypechecker)
{
Contract.Requires(program != null);
Contract.Requires(bplFileName != null);
+
+ linearTypechecker = null;
+
// ---------- Resolve ------------------------------------------------------------
if (CommandLineOptions.Clo.NoResolve)
@@ -693,12 +712,18 @@ namespace Microsoft.Boogie /// </summary>
public static PipelineOutcome InferAndVerify(Program program,
PipelineStatistics stats,
- ErrorReporterDelegate er = null, string requestId = null)
+ ErrorReporterDelegate er = null, string requestId = "unknown")
{
Contract.Requires(program != null);
Contract.Requires(stats != null);
Contract.Ensures(0 <= Contract.ValueAtReturn(out stats.InconclusiveCount) && 0 <= Contract.ValueAtReturn(out stats.TimeoutCount));
+ if (requestId == null)
+ {
+ requestId = "unknown";
+ }
+ RequestIdToCancellationTokenSources[requestId] = new List<CancellationTokenSource>();
+
#region Infer invariants using Abstract Interpretation
// Always use (at least) intervals, if not specified otherwise (e.g. with the "/noinfer" switch)
@@ -776,15 +801,24 @@ namespace Microsoft.Boogie 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++)
{
var taskIndex = i;
- var t = Task.Factory.StartNew(() =>
+ var id = stablePrioritizedImpls[i].Id;
+ CancellationTokenSource src;
+ if (ImplIdToCancellationTokenSource.TryGetValue(id, out src))
{
- VerifyImplementation(program, stats, er, requestId, extractLoopMappingInfo, stablePrioritizedImpls, taskIndex, outputCollector, checkers);
- }, TaskCreationOptions.LongRunning);
+ src.Cancel();
+ }
+ src = new CancellationTokenSource();
+ RequestIdToCancellationTokenSources[requestId].Add(src);
+ ImplIdToCancellationTokenSource[id] = src;
+ var t = Task.Factory.StartNew((dummy) =>
+ {
+ VerifyImplementation(program, stats, er, requestId, extractLoopMappingInfo, stablePrioritizedImpls, taskIndex, outputCollector, Checkers, src.Token);
+ ImplIdToCancellationTokenSource.Remove(id);
+ }, src.Token, TaskCreationOptions.LongRunning);
tasks[taskIndex] = t;
}
try
@@ -802,19 +836,17 @@ namespace Microsoft.Boogie outcome = PipelineOutcome.FatalError;
return true;
}
+ var oce = e as OperationCanceledException;
+ if (oce != null)
+ {
+ return true;
+ }
return false;
});
}
finally
{
- lock (checkers)
- {
- foreach (Checker checker in checkers)
- {
- Contract.Assert(checker != null);
- checker.Close();
- }
- }
+ CleanupCheckers(requestId);
}
cce.NonNull(CommandLineOptions.Clo.TheProverFactory).Close();
@@ -827,8 +859,50 @@ namespace Microsoft.Boogie }
- 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)
+ public static void CancelRequest(string requestId)
+ {
+ Contract.Requires(requestId != null);
+
+ IList<CancellationTokenSource> ctss;
+ if (RequestIdToCancellationTokenSources.TryGetValue(requestId, out ctss))
+ {
+ ctss.Iter(cts => cts.Cancel());
+
+ CleanupCheckers(requestId);
+ }
+ }
+
+
+ private static void CleanupCheckers(string requestId)
{
+ lock (RequestIdToCancellationTokenSources)
+ {
+ if (RequestIdToCancellationTokenSources.Count == 1)
+ {
+ lock (Checkers)
+ {
+ foreach (Checker checker in Checkers)
+ {
+ Contract.Assert(checker != null);
+ checker.Close();
+ }
+ }
+ }
+ if (requestId != null)
+ {
+ RequestIdToCancellationTokenSources.Remove(requestId);
+ }
+ }
+ }
+
+
+ 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, CancellationToken ct)
+ {
+ if (ct.IsCancellationRequested)
+ {
+ ct.ThrowIfCancellationRequested();
+ }
+
Implementation impl = stablePrioritizedImpls[index];
VerificationResult verificationResult = null;
var output = new StringWriter();
@@ -941,7 +1015,7 @@ namespace Microsoft.Boogie #region Process the verification results and statistics
- ProcessOutcome(verificationResult.Outcome, verificationResult.Errors, TimeIndication(verificationResult), stats, output, er, verificationResult.ImplementationName, verificationResult.ImplementationToken, verificationResult.RequestId);
+ ProcessOutcome(verificationResult.Outcome, verificationResult.Errors, TimeIndication(verificationResult), stats, output, impl.TimeLimit, er, verificationResult.ImplementationName, verificationResult.ImplementationToken, verificationResult.RequestId);
ProcessErrors(verificationResult.Errors, verificationResult.Outcome, output, er, impl);
@@ -1064,7 +1138,7 @@ namespace Microsoft.Boogie foreach (Houdini.VCGenOutcome x in outcome.implementationOutcomes.Values)
{
- ProcessOutcome(x.outcome, x.errors, "", stats, Console.Out, er);
+ ProcessOutcome(x.outcome, x.errors, "", stats, Console.Out, CommandLineOptions.Clo.ProverKillTime, er);
ProcessErrors(x.errors, x.outcome, Console.Out, er);
}
//errorCount = outcome.ErrorCount;
@@ -1091,7 +1165,7 @@ namespace Microsoft.Boogie // Run Abstract Houdini
var abs = new Houdini.AbsHoudini(program, domain);
var absout = abs.ComputeSummaries();
- ProcessOutcome(absout.outcome, absout.errors, "", stats, Console.Out, er);
+ ProcessOutcome(absout.outcome, absout.errors, "", stats, Console.Out, CommandLineOptions.Clo.ProverKillTime, er);
ProcessErrors(absout.errors, absout.outcome, Console.Out, er);
//Houdini.PredicateAbs.Initialize(program);
@@ -1120,7 +1194,7 @@ namespace Microsoft.Boogie 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)
+ PipelineStatistics stats, TextWriter tw, int timeLimit, ErrorReporterDelegate er = null, string implName = null, IToken implTok = null, string requestId = null)
{
Contract.Requires(stats != null);
@@ -1128,11 +1202,11 @@ namespace Microsoft.Boogie printer.Inform(timeIndication + OutcomeIndication(outcome, errors), tw);
- ReportOutcome(outcome, er, implName, implTok, requestId, tw);
+ ReportOutcome(outcome, er, implName, implTok, requestId, tw, timeLimit);
}
- private static void ReportOutcome(VC.VCGen.Outcome outcome, ErrorReporterDelegate er, string implName, IToken implTok, string requestId, TextWriter tw)
+ private static void ReportOutcome(VC.VCGen.Outcome outcome, ErrorReporterDelegate er, string implName, IToken implTok, string requestId, TextWriter tw, int timeLimit)
{
ErrorInformation errorInfo = null;
@@ -1144,7 +1218,7 @@ namespace Microsoft.Boogie case VCGen.Outcome.TimedOut:
if (implName != null && implTok != null)
{
- errorInfo = errorInformationFactory.CreateErrorInformation(implTok, string.Format("Verification timed out after {0} seconds ({1})", CommandLineOptions.Clo.ProverKillTime, implName), requestId);
+ errorInfo = errorInformationFactory.CreateErrorInformation(implTok, string.Format("Verification timed out after {0} seconds ({1})", timeLimit, implName), requestId);
}
break;
case VCGen.Outcome.OutOfMemory:
@@ -1277,7 +1351,7 @@ namespace Microsoft.Boogie }
if (CommandLineOptions.Clo.ModelViewFile != null)
{
- error.PrintModel(errorInfo.Out);
+ error.PrintModel(errorInfo.Model);
}
printer.WriteErrorInformation(errorInfo, tw);
diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs index b5775424..a64cece0 100644 --- a/Source/Houdini/Checker.cs +++ b/Source/Houdini/Checker.cs @@ -134,7 +134,7 @@ namespace Microsoft.Boogie.Houdini { vcgen.ConvertCFG2DAG(impl);
ModelViewInfo mvInfo;
- Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = vcgen.PassifyImpl(impl, out mvInfo);
+ var gotoCmdOrigins = vcgen.PassifyImpl(impl, out mvInfo);
ExistentialConstantCollector ecollector;
ExistentialConstantCollector.CollectHoudiniConstants(houdini, impl, out ecollector);
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 7c42df01..815e5a45 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -8,6 +8,7 @@ using System.Collections; using System.Collections.Generic;
using System.Threading;
using System.IO;
+
//using ExternalProver;
using System.Linq;
using System.Diagnostics;
@@ -18,541 +19,509 @@ using Microsoft.Boogie.VCExprAST; using Microsoft.Boogie.Clustering;
using Microsoft.Boogie.TypeErasure;
using System.Text;
-
using RPFP = Microsoft.Boogie.RPFP;
namespace Microsoft.Boogie.SMTLib
{
- public class SMTLibProcessTheoremProver : ProverInterface
- {
- private readonly SMTLibProverContext ctx;
- private readonly VCExpressionGenerator gen;
- private readonly SMTLibProverOptions options;
- private bool usingUnsatCore;
- private RPFP rpfp = null;
-
- [ContractInvariantMethod]
- void ObjectInvariant()
- {
- Contract.Invariant(ctx != null);
- Contract.Invariant(AxBuilder != null);
- Contract.Invariant(Namer != null);
- Contract.Invariant(DeclCollector != null);
- Contract.Invariant(cce.NonNullElements(Axioms));
- Contract.Invariant(cce.NonNullElements(TypeDecls));
- Contract.Invariant(_backgroundPredicates != null);
+ public class SMTLibProcessTheoremProver : ProverInterface
+ {
+ private readonly SMTLibProverContext ctx;
+ private readonly VCExpressionGenerator gen;
+ private readonly SMTLibProverOptions options;
+ private bool usingUnsatCore;
+ private RPFP rpfp = null;
+
+ [ContractInvariantMethod]
+ void ObjectInvariant ()
+ {
+ Contract.Invariant (ctx != null);
+ Contract.Invariant (AxBuilder != null);
+ Contract.Invariant (Namer != null);
+ Contract.Invariant (DeclCollector != null);
+ Contract.Invariant (cce.NonNullElements (Axioms));
+ Contract.Invariant (cce.NonNullElements (TypeDecls));
+ Contract.Invariant (_backgroundPredicates != null);
- }
+ }
+ [NotDelayed]
+ public SMTLibProcessTheoremProver (ProverOptions options, VCExpressionGenerator gen,
+ SMTLibProverContext ctx)
+ {
+ Contract.Requires (options != null);
+ Contract.Requires (gen != null);
+ Contract.Requires (ctx != null);
+ InitializeGlobalInformation ("UnivBackPred2.smt2");
- [NotDelayed]
- public SMTLibProcessTheoremProver(ProverOptions options, VCExpressionGenerator gen,
- SMTLibProverContext ctx)
- {
- Contract.Requires(options != null);
- Contract.Requires(gen != null);
- Contract.Requires(ctx != null);
- InitializeGlobalInformation("UnivBackPred2.smt2");
+ this.options = (SMTLibProverOptions)options;
+ this.ctx = ctx;
+ this.gen = gen;
+ this.usingUnsatCore = false;
- this.options = (SMTLibProverOptions)options;
- this.ctx = ctx;
- this.gen = gen;
- this.usingUnsatCore = false;
+ SetupAxiomBuilder (gen);
- TypeAxiomBuilder axBuilder;
- switch (CommandLineOptions.Clo.TypeEncodingMethod) {
- case CommandLineOptions.TypeEncoding.Arguments:
- axBuilder = new TypeAxiomBuilderArguments(gen);
- axBuilder.Setup();
- break;
- case CommandLineOptions.TypeEncoding.Monomorphic:
- axBuilder = new TypeAxiomBuilderPremisses(gen);
- break;
- default:
- axBuilder = new TypeAxiomBuilderPremisses(gen);
- axBuilder.Setup();
- break;
- }
-
- AxBuilder = axBuilder;
- Namer = new SMTLibNamer();
- ctx.parent = this;
- this.DeclCollector = new TypeDeclCollector((SMTLibProverOptions)options, Namer);
+ Namer = new SMTLibNamer ();
+ ctx.parent = this;
+ this.DeclCollector = new TypeDeclCollector ((SMTLibProverOptions)options, Namer);
- SetupProcess();
+ SetupProcess ();
- if (CommandLineOptions.Clo.StratifiedInlining > 0 || CommandLineOptions.Clo.ContractInfer)
- {
- // Prepare for ApiChecker usage
- if (options.LogFilename != null && currentLogFile == null)
- {
- currentLogFile = OpenOutputFile("");
- }
- if (CommandLineOptions.Clo.ContractInfer)
- {
- SendThisVC("(set-option :produce-unsat-cores true)");
- this.usingUnsatCore = true;
- }
- PrepareCommon();
- }
- }
+ if (CommandLineOptions.Clo.StratifiedInlining > 0 || CommandLineOptions.Clo.ContractInfer) {
+ // Prepare for ApiChecker usage
+ if (options.LogFilename != null && currentLogFile == null) {
+ currentLogFile = OpenOutputFile ("");
+ }
+ if (CommandLineOptions.Clo.ContractInfer) {
+ SendThisVC ("(set-option :produce-unsat-cores true)");
+ this.usingUnsatCore = true;
+ }
+ PrepareCommon ();
+ }
+ }
- ProcessStartInfo ComputeProcessStartInfo()
- {
- var path = this.options.ProverPath;
- var solverOptions = "";
+ private void SetupAxiomBuilder (VCExpressionGenerator gen)
+ {
+ switch (CommandLineOptions.Clo.TypeEncodingMethod) {
+ case CommandLineOptions.TypeEncoding.Arguments:
+ AxBuilder = new TypeAxiomBuilderArguments (gen);
+ AxBuilder.Setup ();
+ break;
+ case CommandLineOptions.TypeEncoding.Monomorphic:
+ AxBuilder = new TypeAxiomBuilderPremisses (gen);
+ break;
+ default:
+ AxBuilder = new TypeAxiomBuilderPremisses (gen);
+ AxBuilder.Setup ();
+ break;
+ }
+ }
- switch (options.Solver) {
+ ProcessStartInfo ComputeProcessStartInfo ()
+ {
+ var path = this.options.ProverPath;
+ switch (options.Solver) {
case SolverKind.Z3:
- solverOptions = "AUTO_CONFIG=false -smt2 -in";
- if (path == null)
- path = Z3.ExecutablePath();
- return SMTLibProcess.ComputerProcessStartInfo(path, solverOptions);
+ if (path == null)
+ path = Z3.ExecutablePath ();
+ return SMTLibProcess.ComputerProcessStartInfo (path, "AUTO_CONFIG=false -smt2 -in");
case SolverKind.CVC4:
- solverOptions = "--lang=smt --no-strict-parsing --no-condense-function-values --incremental";
- if (path == null)
- path = CVC4.ExecutablePath();
- return SMTLibProcess.ComputerProcessStartInfo(path, solverOptions);
+ if (path == null)
+ path = "cvc4";
+ return SMTLibProcess.ComputerProcessStartInfo (path, "--lang=smt --no-strict-parsing --no-condense-function-values --incremental");
default:
- Debug.Assert(false);
- return null;
+ Debug.Assert (false);
+ return null;
+ }
}
- }
-
- void SetupProcess()
- {
- if (Process != null) return;
-
- var psi = ComputeProcessStartInfo();
- Process = new SMTLibProcess(psi, this.options);
- Process.ErrorHandler += this.HandleProverError;
- }
-
- void PossiblyRestart()
- {
- if (Process != null && Process.NeedsRestart) {
- Process.Close();
- Process = null;
- SetupProcess();
- Process.Send(common.ToString());
- }
- }
+ void SetupProcess ()
+ {
+ if (Process != null)
+ return;
- public override ProverContext Context
- {
- get
- {
- Contract.Ensures(Contract.Result<ProverContext>() != null);
+ var psi = ComputeProcessStartInfo ();
+ Process = new SMTLibProcess (psi, this.options);
+ Process.ErrorHandler += this.HandleProverError;
+ }
- return ctx;
- }
- }
+ void PossiblyRestart ()
+ {
+ if (Process != null && Process.NeedsRestart) {
+ Process.Close ();
+ Process = null;
+ SetupProcess ();
+ Process.Send (common.ToString ());
+ }
+ }
- internal readonly TypeAxiomBuilder AxBuilder;
- internal readonly UniqueNamer Namer;
- readonly TypeDeclCollector DeclCollector;
- SMTLibProcess Process;
- readonly List<string> proverErrors = new List<string>();
- readonly List<string> proverWarnings = new List<string>();
- readonly StringBuilder common = new StringBuilder();
- TextWriter currentLogFile;
- volatile ErrorHandler currentErrorHandler;
-
- private void FeedTypeDeclsToProver()
- {
- foreach (string s in DeclCollector.GetNewDeclarations()) {
- Contract.Assert(s != null);
- AddTypeDecl(s);
- }
- }
+ public override ProverContext Context {
+ get {
+ Contract.Ensures (Contract.Result<ProverContext> () != null);
- private string Sanitize(string msg)
- {
- var idx = msg.IndexOf('\n');
- if (idx > 0)
- msg = msg.Replace("\r", "").Replace("\n", "\r\n");
- return msg;
- }
-
- private void SendCommon(string s)
- {
- Send(s, true);
- }
+ return ctx;
+ }
+ }
- private void SendThisVC(string s)
- {
- Send(s, false);
- }
+ internal TypeAxiomBuilder AxBuilder { get; private set; }
+
+ internal readonly UniqueNamer Namer;
+ readonly TypeDeclCollector DeclCollector;
+ SMTLibProcess Process;
+ readonly List<string> proverErrors = new List<string> ();
+ readonly List<string> proverWarnings = new List<string> ();
+ readonly StringBuilder common = new StringBuilder ();
+ TextWriter currentLogFile;
+ volatile ErrorHandler currentErrorHandler;
+
+ private void FeedTypeDeclsToProver ()
+ {
+ foreach (string s in DeclCollector.GetNewDeclarations()) {
+ Contract.Assert (s != null);
+ AddTypeDecl (s);
+ }
+ }
- private void Send(string s, bool isCommon)
- {
- s = Sanitize(s);
+ private string Sanitize (string msg)
+ {
+ var idx = msg.IndexOf ('\n');
+ if (idx > 0)
+ msg = msg.Replace ("\r", "").Replace ("\n", "\r\n");
+ return msg;
+ }
- if (isCommon)
- common.Append(s).Append("\r\n");
+ private void SendCommon (string s)
+ {
+ Send (s, true);
+ }
- if (Process != null)
- Process.Send(s);
- if (currentLogFile != null)
- currentLogFile.WriteLine(s);
- }
+ private void SendThisVC (string s)
+ {
+ Send (s, false);
+ }
- private void FindDependentTypes(Type type, List<CtorType> dependentTypes)
- {
- MapType mapType = type as MapType;
- if (mapType != null)
- {
- foreach (Type t in mapType.Arguments)
- {
- FindDependentTypes(t, dependentTypes);
- }
- FindDependentTypes(mapType.Result, dependentTypes);
- }
- CtorType ctorType = type as CtorType;
- if (ctorType != null && ctx.KnownDatatypeConstructors.ContainsKey(ctorType))
- {
- dependentTypes.Add(ctorType);
- }
- }
+ private void Send (string s, bool isCommon)
+ {
+ s = Sanitize (s);
- private void PrepareCommon()
- {
- if (common.Length == 0)
- {
- SendCommon("(set-option :print-success false)");
- SendCommon("(set-info :smt-lib-version 2.0)");
- if (options.ProduceModel())
- SendCommon("(set-option :produce-models true)");
- foreach (var opt in options.SmtOptions)
- {
- SendCommon("(set-option :" + opt.Option + " " + opt.Value + ")");
- }
+ if (isCommon)
+ common.Append (s).Append ("\r\n");
- if (!string.IsNullOrEmpty(options.Logic))
- {
- SendCommon("(set-logic " + options.Logic + ")");
- }
+ if (Process != null)
+ Process.Send (s);
+ if (currentLogFile != null)
+ currentLogFile.WriteLine (s);
+ }
- SendCommon("; done setting options\n");
- SendCommon(_backgroundPredicates);
+ private void FindDependentTypes (Type type, List<CtorType> dependentTypes)
+ {
+ MapType mapType = type as MapType;
+ if (mapType != null) {
+ foreach (Type t in mapType.Arguments) {
+ FindDependentTypes (t, dependentTypes);
+ }
+ FindDependentTypes (mapType.Result, dependentTypes);
+ }
+ CtorType ctorType = type as CtorType;
+ if (ctorType != null && ctx.KnownDatatypeConstructors.ContainsKey (ctorType)) {
+ dependentTypes.Add (ctorType);
+ }
+ }
- if (options.UseTickleBool)
- {
- SendCommon("(declare-fun tickleBool (Bool) Bool)");
- SendCommon("(assert (and (tickleBool true) (tickleBool false)))");
- }
+ private void PrepareCommon ()
+ {
+ if (common.Length == 0) {
+ SendCommon ("(set-option :print-success false)");
+ SendCommon ("(set-info :smt-lib-version 2.0)");
+ if (options.ProduceModel ())
+ SendCommon ("(set-option :produce-models true)");
+ foreach (var opt in options.SmtOptions) {
+ SendCommon ("(set-option :" + opt.Option + " " + opt.Value + ")");
+ }
- if (ctx.KnownDatatypeConstructors.Count > 0)
- {
- GraphUtil.Graph<CtorType> dependencyGraph = new GraphUtil.Graph<CtorType>();
- foreach (CtorType datatype in ctx.KnownDatatypeConstructors.Keys)
- {
- dependencyGraph.AddSource(datatype);
- foreach (Function f in ctx.KnownDatatypeConstructors[datatype])
- {
- List<CtorType> dependentTypes = new List<CtorType>();
- foreach (Variable v in f.InParams)
- {
- FindDependentTypes(v.TypedIdent.Type, dependentTypes);
- }
- foreach (CtorType result in dependentTypes)
- {
- dependencyGraph.AddEdge(datatype, result);
- }
- }
- }
- GraphUtil.StronglyConnectedComponents<CtorType> sccs = new GraphUtil.StronglyConnectedComponents<CtorType>(dependencyGraph.Nodes, dependencyGraph.Predecessors, dependencyGraph.Successors);
- sccs.Compute();
- foreach (GraphUtil.SCC<CtorType> scc in sccs)
- {
- string datatypeString = "";
- foreach (CtorType datatype in scc)
- {
- datatypeString += "(" + SMTLibExprLineariser.TypeToString(datatype) + " ";
- foreach (Function f in ctx.KnownDatatypeConstructors[datatype])
- {
- string quotedConstructorName = Namer.GetQuotedName(f, f.Name);
- if (f.InParams.Length == 0)
- {
- datatypeString += quotedConstructorName + " ";
- }
- else
- {
- datatypeString += "(" + quotedConstructorName + " ";
- foreach (Variable v in f.InParams)
- {
- string quotedSelectorName = Namer.GetQuotedName(v, v.Name + "#" + f.Name);
- datatypeString += "(" + quotedSelectorName + " " + DeclCollector.TypeToStringReg(v.TypedIdent.Type) + ") ";
- }
- datatypeString += ") ";
- }
- }
- datatypeString += ") ";
- }
- List<string> decls = DeclCollector.GetNewDeclarations();
- foreach (string decl in decls)
- {
- SendCommon(decl);
- }
- SendCommon("(declare-datatypes () (" + datatypeString + "))");
- }
- }
- }
+ if (!string.IsNullOrEmpty (options.Logic)) {
+ SendCommon ("(set-logic " + options.Logic + ")");
+ }
- if (!AxiomsAreSetup)
- {
- var axioms = ctx.Axioms;
- var nary = axioms as VCExprNAry;
- if (nary != null && nary.Op == VCExpressionGenerator.AndOp)
- foreach (var expr in nary.UniformArguments)
- {
- var str = VCExpr2String(expr, -1);
- if (str != "true")
- AddAxiom(str);
- }
- else
- AddAxiom(VCExpr2String(axioms, -1));
- AxiomsAreSetup = true;
- }
- }
+ SendCommon ("; done setting options\n");
+ SendCommon (_backgroundPredicates);
- public override int FlushAxiomsToTheoremProver()
- {
- // we feed the axioms when begincheck is called.
- return 0;
- }
+ if (options.UseTickleBool) {
+ SendCommon ("(declare-fun tickleBool (Bool) Bool)");
+ SendCommon ("(assert (and (tickleBool true) (tickleBool false)))");
+ }
- private void FlushAxioms()
- {
- TypeDecls.Iter(SendCommon);
- TypeDecls.Clear();
- foreach (string s in Axioms) {
- Contract.Assert(s != null);
- if (s != "true")
- SendCommon("(assert " + s + ")");
- }
- Axioms.Clear();
- //FlushPushedAssertions();
- }
+ if (ctx.KnownDatatypeConstructors.Count > 0) {
+ GraphUtil.Graph<CtorType> dependencyGraph = new GraphUtil.Graph<CtorType> ();
+ foreach (CtorType datatype in ctx.KnownDatatypeConstructors.Keys) {
+ dependencyGraph.AddSource (datatype);
+ foreach (Function f in ctx.KnownDatatypeConstructors[datatype]) {
+ List<CtorType> dependentTypes = new List<CtorType> ();
+ foreach (Variable v in f.InParams) {
+ FindDependentTypes (v.TypedIdent.Type, dependentTypes);
+ }
+ foreach (CtorType result in dependentTypes) {
+ dependencyGraph.AddEdge (datatype, result);
+ }
+ }
+ }
+ GraphUtil.StronglyConnectedComponents<CtorType> sccs = new GraphUtil.StronglyConnectedComponents<CtorType> (dependencyGraph.Nodes, dependencyGraph.Predecessors, dependencyGraph.Successors);
+ sccs.Compute ();
+ foreach (GraphUtil.SCC<CtorType> scc in sccs) {
+ string datatypeString = "";
+ foreach (CtorType datatype in scc) {
+ datatypeString += "(" + SMTLibExprLineariser.TypeToString (datatype) + " ";
+ foreach (Function f in ctx.KnownDatatypeConstructors[datatype]) {
+ string quotedConstructorName = Namer.GetQuotedName (f, f.Name);
+ if (f.InParams.Length == 0) {
+ datatypeString += quotedConstructorName + " ";
+ } else {
+ datatypeString += "(" + quotedConstructorName + " ";
+ foreach (Variable v in f.InParams) {
+ string quotedSelectorName = Namer.GetQuotedName (v, v.Name + "#" + f.Name);
+ datatypeString += "(" + quotedSelectorName + " " + DeclCollector.TypeToStringReg (v.TypedIdent.Type) + ") ";
+ }
+ datatypeString += ") ";
+ }
+ }
+ datatypeString += ") ";
+ }
+ List<string> decls = DeclCollector.GetNewDeclarations ();
+ foreach (string decl in decls) {
+ SendCommon (decl);
+ }
+ SendCommon ("(declare-datatypes () (" + datatypeString + "))");
+ }
+ }
+ }
+
+ if (!AxiomsAreSetup) {
+ var axioms = ctx.Axioms;
+ var nary = axioms as VCExprNAry;
+ if (nary != null && nary.Op == VCExpressionGenerator.AndOp)
+ foreach (var expr in nary.UniformArguments) {
+ var str = VCExpr2String (expr, -1);
+ if (str != "true")
+ AddAxiom (str);
+ }
+ else
+ AddAxiom (VCExpr2String (axioms, -1));
+ AxiomsAreSetup = true;
+ }
+ }
- private void CloseLogFile()
- {
- if (currentLogFile != null) {
- currentLogFile.Close();
- currentLogFile = null;
- }
- }
+ public override int FlushAxiomsToTheoremProver ()
+ {
+ // we feed the axioms when begincheck is called.
+ return 0;
+ }
- private void FlushLogFile()
- {
- if (currentLogFile != null) {
- currentLogFile.Flush();
- }
- }
+ private void FlushAxioms ()
+ {
+ TypeDecls.Iter (SendCommon);
+ TypeDecls.Clear ();
+ foreach (string s in Axioms) {
+ Contract.Assert (s != null);
+ if (s != "true")
+ SendCommon ("(assert " + s + ")");
+ }
+ Axioms.Clear ();
+ //FlushPushedAssertions();
+ }
- public override void Close()
- {
- base.Close();
- CloseLogFile();
- if (Process != null)
- Process.Close();
- }
+ private void CloseLogFile ()
+ {
+ if (currentLogFile != null) {
+ currentLogFile.Close ();
+ currentLogFile = null;
+ }
+ }
- public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler)
- {
- //Contract.Requires(descriptiveName != null);
- //Contract.Requires(vc != null);
- //Contract.Requires(handler != null);
- rpfp = null;
+ private void FlushLogFile ()
+ {
+ if (currentLogFile != null) {
+ currentLogFile.Flush ();
+ }
+ }
- if (options.SeparateLogFiles) CloseLogFile(); // shouldn't really happen
+ public override void Close ()
+ {
+ base.Close ();
+ CloseLogFile ();
+ if (Process != null)
+ Process.Close ();
+ }
- if (options.LogFilename != null && currentLogFile == null) {
- currentLogFile = OpenOutputFile(descriptiveName);
- currentLogFile.Write(common.ToString());
- }
+ public override void BeginCheck (string descriptiveName, VCExpr vc, ErrorHandler handler)
+ {
+ //Contract.Requires(descriptiveName != null);
+ //Contract.Requires(vc != null);
+ //Contract.Requires(handler != null);
+ rpfp = null;
- PrepareCommon();
- string vcString = "(assert (not\n" + VCExpr2String(vc, 1) + "\n))";
- FlushAxioms();
+ if (options.SeparateLogFiles)
+ CloseLogFile (); // shouldn't really happen
- PossiblyRestart();
+ if (options.LogFilename != null && currentLogFile == null) {
+ currentLogFile = OpenOutputFile (descriptiveName);
+ currentLogFile.Write (common.ToString ());
+ }
- SendThisVC("(push 1)");
- SendThisVC("(set-info :boogie-vc-id " + SMTLibNamer.QuoteId(descriptiveName) + ")");
- SendThisVC(vcString);
- FlushLogFile();
+ PrepareCommon ();
+ string vcString = "(assert (not\n" + VCExpr2String (vc, 1) + "\n))";
+ FlushAxioms ();
- if (Process != null) {
- Process.PingPong(); // flush any errors
+ PossiblyRestart ();
- if (Process.Inspector != null)
- Process.Inspector.NewProblem(descriptiveName, vc, handler);
- }
+ SendThisVC ("(push 1)");
+ SendThisVC ("(set-info :boogie-vc-id " + SMTLibNamer.QuoteId (descriptiveName) + ")");
+ SendThisVC (vcString);
+ FlushLogFile ();
- SendThisVC("(check-sat)");
- FlushLogFile();
- }
+ if (Process != null) {
+ Process.PingPong (); // flush any errors
- public override void Reset()
- {
- if (options.Solver == SolverKind.Z3)
- {
- SendThisVC("(reset)");
- Process.Send(common.ToString());
- }
- }
+ if (Process.Inspector != null)
+ Process.Inspector.NewProblem (descriptiveName, vc, handler);
+ }
- public override void FullReset()
- {
- if (options.Solver == SolverKind.Z3)
- {
- SendThisVC("(reset)");
- common.Clear();
- AxiomsAreSetup = false;
- ctx.Clear();
- DeclCollector.Reset();
- }
- }
+ SendThisVC ("(check-sat)");
+ FlushLogFile ();
+ }
- private RPFP.Node SExprToCex(SExpr resp, ErrorHandler handler,
- Dictionary<int,Dictionary<string,string>> varSubst)
- {
- Dictionary<string, RPFP.Node> nmap = new Dictionary<string,RPFP.Node>();
- Dictionary<string, RPFP.Node> pmap = new Dictionary<string,RPFP.Node>();
+ public override void Reset ()
+ {
+ if (options.Solver == SolverKind.Z3) {
+ SendThisVC ("(reset)");
+
+ if (0 < common.Length) {
+ var c = common.ToString ();
+ Process.Send (c);
+ if (currentLogFile != null) {
+ currentLogFile.WriteLine (c);
+ }
+ }
+ }
+ }
- foreach(var node in rpfp.nodes)
- pmap.Add((node.Name as VCExprBoogieFunctionOp).Func.Name,node);
+ public override void FullReset ()
+ {
+ if (options.Solver == SolverKind.Z3) {
+ Namer.Reset ();
+ common.Clear ();
+ SetupAxiomBuilder (gen);
+ Axioms.Clear ();
+ TypeDecls.Clear ();
+ AxiomsAreSetup = false;
+ ctx.Reset ();
+ ctx.KnownDatatypeConstructors.Clear ();
+ ctx.parent = this;
+ DeclCollector.Reset ();
+ SendThisVC ("; doing a full reset...");
+ }
+ }
- RPFP.Node topnode = null;
- var lines = resp.Arguments;
+ private RPFP.Node SExprToCex (SExpr resp, ErrorHandler handler,
+ Dictionary<int,Dictionary<string,string>> varSubst)
+ {
+ Dictionary<string, RPFP.Node> nmap = new Dictionary<string,RPFP.Node> ();
+ Dictionary<string, RPFP.Node> pmap = new Dictionary<string,RPFP.Node> ();
- // last line of derivation is from query, skip it
- for (int i = 0; i < lines.Length-1; i++)
- {
- var line = lines[i];
- if (line.ArgCount != 6)
- {
- HandleProverError("bad derivation line from prover: " + line.ToString());
- return null;
- }
- var name = line[0];
- var conseq = line[1];
- var rule = line[2];
- var subst = line[3];
- 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))
- {
- HandleProverError("unknown predicate from prover: " + predName.ToString());
- return null;
- }
- RPFP.Node cexnode = rpfp.CloneNode(node);
- cexnode.map = node;
- nmap.Add(name.Name, cexnode);
- List<RPFP.Node> Chs = new List<RPFP.Node>();
+ foreach (var node in rpfp.nodes)
+ pmap.Add ((node.Name as VCExprBoogieFunctionOp).Func.Name, node);
- if (refs.Name != "ref")
- {
- HandleProverError("bad references from prover: " + refs.ToString());
- return null;
- }
- foreach (var c in refs.Arguments)
- {
- if (c.Name == "true")
- Chs.Add(null);
- else
- {
- RPFP.Node ch = null;
- if (!nmap.TryGetValue(c.Name, out ch))
- {
- HandleProverError("unknown reference from prover: " + c.ToString());
- return null;
- }
- Chs.Add(ch);
- }
- }
+ RPFP.Node topnode = null;
+ var lines = resp.Arguments;
- if (!rule.Name.StartsWith("rule!"))
- {
- HandleProverError("bad rule name from prover: " + refs.ToString());
- return null;
- }
- int ruleNum = Convert.ToInt32(rule.Name.Substring(5)) - 1;
- if (ruleNum < 0 || ruleNum > rpfp.edges.Count)
- {
- HandleProverError("bad rule name from prover: " + refs.ToString());
- return null;
- }
- RPFP.Edge orig_edge = rpfp.edges[ruleNum];
- RPFP.Edge e = rpfp.CreateEdge(cexnode, orig_edge.F, Chs.ToArray());
- e.map = orig_edge;
- topnode = cexnode;
+ // last line of derivation is from query, skip it
+ for (int i = 0; i < lines.Length-1; i++) {
+ var line = lines [i];
+ if (line.ArgCount != 6) {
+ HandleProverError ("bad derivation line from prover: " + line.ToString ());
+ return null;
+ }
+ var name = line [0];
+ var conseq = line [1];
+ var rule = line [2];
+ var subst = line [3];
+ 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)) {
+ HandleProverError ("unknown predicate from prover: " + predName.ToString ());
+ return null;
+ }
+ RPFP.Node cexnode = rpfp.CloneNode (node);
+ cexnode.map = node;
+ nmap.Add (name.Name, cexnode);
+ List<RPFP.Node> Chs = new List<RPFP.Node> ();
+
+ if (refs.Name != "ref") {
+ HandleProverError ("bad references from prover: " + refs.ToString ());
+ return null;
+ }
+ foreach (var c in refs.Arguments) {
+ if (c.Name == "true")
+ Chs.Add (null);
+ else {
+ RPFP.Node ch = null;
+ if (!nmap.TryGetValue (c.Name, out ch)) {
+ HandleProverError ("unknown reference from prover: " + c.ToString ());
+ return null;
+ }
+ Chs.Add (ch);
+ }
+ }
- if (labs.Name != "labels")
- {
- HandleProverError("bad labels from prover: " + labs.ToString());
- return null;
- }
- e.labels = new HashSet<string>();
- foreach (var l in labs.Arguments)
- e.labels.Add(l.Name);
+ if (!rule.Name.StartsWith ("rule!")) {
+ HandleProverError ("bad rule name from prover: " + refs.ToString ());
+ return null;
+ }
+ int ruleNum = Convert.ToInt32 (rule.Name.Substring (5)) - 1;
+ if (ruleNum < 0 || ruleNum > rpfp.edges.Count) {
+ HandleProverError ("bad rule name from prover: " + refs.ToString ());
+ return null;
+ }
+ RPFP.Edge orig_edge = rpfp.edges [ruleNum];
+ RPFP.Edge e = rpfp.CreateEdge (cexnode, orig_edge.F, Chs.ToArray ());
+ e.map = orig_edge;
+ topnode = cexnode;
+
+ if (labs.Name != "labels") {
+ HandleProverError ("bad labels from prover: " + labs.ToString ());
+ return null;
+ }
+ e.labels = new HashSet<string> ();
+ foreach (var l in labs.Arguments)
+ e.labels.Add (l.Name);
- if (subst.Name != "subst")
- {
- HandleProverError("bad subst from prover: " + subst.ToString());
- return null;
- }
- Dictionary<string, string> dict = new Dictionary<string, string>();
- varSubst[e.number] = dict;
- foreach (var s in subst.Arguments)
- {
- if (s.Name != "=" || s.Arguments.Length != 2)
- {
- HandleProverError("bad equation from prover: " + s.ToString());
- return null;
- }
- string uniqueName = s.Arguments[0].Name;
- string spacer = "@@"; // Hack! UniqueNamer is adding these and I can't stop it!
- int pos = uniqueName.LastIndexOf(spacer);
- if (pos >= 0)
- uniqueName = uniqueName.Substring(0, pos);
- dict.Add(uniqueName, s.Arguments[1].ToString());
- }
+ if (subst.Name != "subst") {
+ HandleProverError ("bad subst from prover: " + subst.ToString ());
+ return null;
+ }
+ Dictionary<string, string> dict = new Dictionary<string, string> ();
+ varSubst [e.number] = dict;
+ foreach (var s in subst.Arguments) {
+ if (s.Name != "=" || s.Arguments.Length != 2) {
+ HandleProverError ("bad equation from prover: " + s.ToString ());
+ return null;
+ }
+ string uniqueName = s.Arguments [0].Name;
+ string spacer = "@@"; // Hack! UniqueNamer is adding these and I can't stop it!
+ int pos = uniqueName.LastIndexOf (spacer);
+ if (pos >= 0)
+ uniqueName = uniqueName.Substring (0, pos);
+ dict.Add (uniqueName, s.Arguments [1].ToString ());
+ }
- }
- if (topnode == null)
- {
- HandleProverError("empty derivation from prover: " + resp.ToString());
- }
- return topnode;
- }
+ }
+ if (topnode == null) {
+ HandleProverError ("empty derivation from prover: " + resp.ToString ());
+ }
+ return topnode;
+ }
- private Model SExprToModel(SExpr resp, ErrorHandler handler)
- {
- // Concatenate all the arguments
- string modelString = resp[0].Name;
- // modelString = modelString.Substring(7, modelString.Length - 8); // remove "(model " and final ")"
- var models = Model.ParseModels(new StringReader("Z3 error model: \n" + modelString),"");
- if (models == null || models.Count == 0)
- {
- HandleProverError("no model from prover: " + resp.ToString());
- }
- return models[0];
- }
+ private Model SExprToModel (SExpr resp, ErrorHandler handler)
+ {
+ // Concatenate all the arguments
+ string modelString = resp [0].Name;
+ // modelString = modelString.Substring(7, modelString.Length - 8); // remove "(model " and final ")"
+ var models = Model.ParseModels (new StringReader ("Z3 error model: \n" + modelString), "");
+ if (models == null || models.Count == 0) {
+ HandleProverError ("no model from prover: " + resp.ToString ());
+ }
+ return models [0];
+ }
- private string QuantifiedVCExpr2String(VCExpr x)
- {
- return VCExpr2String(x, 1);
+ private string QuantifiedVCExpr2String (VCExpr x)
+ {
+ return VCExpr2String (x, 1);
#if false
if (!(x is VCExprQuantifier))
return VCExpr2String(x, 1);
@@ -580,122 +549,112 @@ namespace Microsoft.Boogie.SMTLib string res = wr.ToString();
return res;
#endif
- }
-
- public override Outcome CheckRPFP(string descriptiveName, RPFP _rpfp, ErrorHandler handler,
- out RPFP.Node cex,
- Dictionary<int,Dictionary<string,string>> varSubst)
- {
- //Contract.Requires(descriptiveName != null);
- //Contract.Requires(vc != null);
- //Contract.Requires(handler != null);
- rpfp = _rpfp;
- cex = null;
-
- if (options.SeparateLogFiles) CloseLogFile(); // shouldn't really happen
-
- if (options.LogFilename != null && currentLogFile == null)
- {
- currentLogFile = OpenOutputFile(descriptiveName);
- currentLogFile.Write(common.ToString());
- }
-
- Push();
- SendThisVC("(fixedpoint-push)");
- foreach (var node in rpfp.nodes)
- {
- DeclCollector.RegisterRelation((node.Name as VCExprBoogieFunctionOp).Func);
- }
-
- PrepareCommon();
+ }
- LineariserOptions.Default.LabelsBelowQuantifiers = true;
- List<string> ruleStrings = new List<string>();
- foreach (var edge in rpfp.edges)
- {
- 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";
+ public override Outcome CheckRPFP (string descriptiveName, RPFP _rpfp, ErrorHandler handler,
+ out RPFP.Node cex,
+ Dictionary<int,Dictionary<string,string>> varSubst)
+ {
+ //Contract.Requires(descriptiveName != null);
+ //Contract.Requires(vc != null);
+ //Contract.Requires(handler != null);
+ rpfp = _rpfp;
+ cex = null;
+
+ if (options.SeparateLogFiles)
+ CloseLogFile (); // shouldn't really happen
+
+ if (options.LogFilename != null && currentLogFile == null) {
+ currentLogFile = OpenOutputFile (descriptiveName);
+ currentLogFile.Write (common.ToString ());
+ }
+
+ Push ();
+ SendThisVC ("(fixedpoint-push)");
+ foreach (var node in rpfp.nodes) {
+ DeclCollector.RegisterRelation ((node.Name as VCExprBoogieFunctionOp).Func);
+ }
+
+ PrepareCommon ();
+
+ LineariserOptions.Default.LabelsBelowQuantifiers = true;
+ List<string> ruleStrings = new List<string> ();
+ foreach (var edge in rpfp.edges) {
+ 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";
#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";
+ 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();
+ queryString += ")";
+ LineariserOptions.Default.LabelsBelowQuantifiers = false;
+ FlushAxioms ();
- PossiblyRestart();
+ PossiblyRestart ();
- SendThisVC("(set-info :boogie-vc-id " + SMTLibNamer.QuoteId(descriptiveName) + ")");
- foreach(var rs in ruleStrings)
- SendThisVC(rs);
- FlushLogFile();
+ SendThisVC ("(set-info :boogie-vc-id " + SMTLibNamer.QuoteId (descriptiveName) + ")");
+ foreach (var rs in ruleStrings)
+ SendThisVC (rs);
+ FlushLogFile ();
- if (Process != null)
- {
- Process.PingPong(); // flush any errors
+ if (Process != null) {
+ Process.PingPong (); // flush any errors
#if false
// TODO: this is not going to work
if (Process.Inspector != null)
Process.Inspector.NewProblem(descriptiveName, vc, handler);
#endif
- }
+ }
- SendThisVC(queryString);
- FlushLogFile();
+ SendThisVC (queryString);
+ FlushLogFile ();
- var result = Outcome.Undetermined;
+ var result = Outcome.Undetermined;
- if (Process != null)
- {
+ if (Process != null) {
- var resp = Process.GetProverResponse();
+ var resp = Process.GetProverResponse ();
- switch (resp.Name)
- {
- case "unsat":
- result = Outcome.Valid;
- break;
- case "sat":
- result = Outcome.Invalid;
- break;
- case "unknown":
- result = Outcome.Invalid;
- break;
- default:
- HandleProverError("Unexpected prover response: " + resp.ToString());
- break;
- }
+ switch (resp.Name) {
+ case "unsat":
+ result = Outcome.Valid;
+ break;
+ case "sat":
+ result = Outcome.Invalid;
+ break;
+ case "unknown":
+ result = Outcome.Invalid;
+ break;
+ default:
+ HandleProverError ("Unexpected prover response: " + resp.ToString ());
+ break;
+ }
- switch (result)
- {
- case Outcome.Invalid:
- {
- resp = Process.GetProverResponse();
- if (resp.Name == "derivation")
- {
- cex = SExprToCex(resp, handler,varSubst);
- }
- else
- HandleProverError("Unexpected prover response: " + resp.ToString());
- resp = Process.GetProverResponse();
- if (resp.Name == "model")
- {
- var model = SExprToModel(resp, handler);
- cex.owner.SetBackgroundModel(model);
- }
- else
- HandleProverError("Unexpected prover response: " + resp.ToString());
- break;
- }
- default:
- break;
- }
+ switch (result) {
+ case Outcome.Invalid:
+ {
+ resp = Process.GetProverResponse ();
+ if (resp.Name == "derivation") {
+ cex = SExprToCex (resp, handler, varSubst);
+ } else
+ HandleProverError ("Unexpected prover response: " + resp.ToString ());
+ resp = Process.GetProverResponse ();
+ if (resp.Name == "model") {
+ var model = SExprToModel (resp, handler);
+ cex.owner.SetBackgroundModel (model);
+ } else
+ HandleProverError ("Unexpected prover response: " + resp.ToString ());
+ break;
+ }
+ default:
+ break;
+ }
#if false
while (true)
@@ -706,121 +665,121 @@ namespace Microsoft.Boogie.SMTLib HandleProverError("Unexpected prover response: " + resp.ToString());
}
#endif
- }
- SendThisVC("(fixedpoint-pop)");
- Pop();
- AxiomsAreSetup = false;
- return result;
- }
+ }
+ SendThisVC ("(fixedpoint-pop)");
+ Pop ();
+ AxiomsAreSetup = false;
+ return result;
+ }
- private static HashSet<string> usedLogNames = new HashSet<string>();
+ private static HashSet<string> usedLogNames = new HashSet<string> ();
- private TextWriter OpenOutputFile(string descriptiveName)
- {
- Contract.Requires(descriptiveName != null);
- Contract.Ensures(Contract.Result<TextWriter>() != null);
+ private TextWriter OpenOutputFile (string descriptiveName)
+ {
+ Contract.Requires (descriptiveName != null);
+ Contract.Ensures (Contract.Result<TextWriter> () != null);
- string filename = options.LogFilename;
- filename = Helpers.SubstituteAtPROC(descriptiveName, cce.NonNull(filename));
- var curFilename = filename;
+ string filename = options.LogFilename;
+ filename = Helpers.SubstituteAtPROC (descriptiveName, cce.NonNull (filename));
+ var curFilename = filename;
- lock (usedLogNames) {
- int n = 1;
- while (usedLogNames.Contains(curFilename)) {
- curFilename = filename + "." + n++;
- }
- usedLogNames.Add(curFilename);
- }
+ lock (usedLogNames) {
+ int n = 1;
+ while (usedLogNames.Contains(curFilename)) {
+ curFilename = filename + "." + n++;
+ }
+ usedLogNames.Add (curFilename);
+ }
- return new StreamWriter(curFilename, false);
- }
+ return new StreamWriter (curFilename, false);
+ }
- private void FlushProverWarnings()
- {
- var handler = currentErrorHandler;
- if (handler != null) {
- lock (proverWarnings) {
- proverWarnings.Iter(handler.OnProverWarning);
- proverWarnings.Clear();
- }
- }
- }
+ private void FlushProverWarnings ()
+ {
+ var handler = currentErrorHandler;
+ if (handler != null) {
+ lock (proverWarnings) {
+ proverWarnings.Iter (handler.OnProverWarning);
+ proverWarnings.Clear ();
+ }
+ }
+ }
- private void HandleProverError(string s)
- {
- s = s.Replace("\r", "");
- lock (proverWarnings) {
- while (s.StartsWith("WARNING: ")) {
- var idx = s.IndexOf('\n');
- var warn = s;
- if (idx > 0) {
- warn = s.Substring(0, idx);
- s = s.Substring(idx + 1);
- } else {
- s = "";
- }
- warn = warn.Substring(9);
- proverWarnings.Add(warn);
- }
- }
+ private void HandleProverError (string s)
+ {
+ s = s.Replace ("\r", "");
+ lock (proverWarnings) {
+ while (s.StartsWith("WARNING: ")) {
+ var idx = s.IndexOf ('\n');
+ var warn = s;
+ if (idx > 0) {
+ warn = s.Substring (0, idx);
+ s = s.Substring (idx + 1);
+ } else {
+ s = "";
+ }
+ warn = warn.Substring (9);
+ proverWarnings.Add (warn);
+ }
+ }
- FlushProverWarnings();
+ FlushProverWarnings ();
- if (s == "") return;
+ if (s == "")
+ return;
- lock (proverErrors) {
- proverErrors.Add(s);
- Console.WriteLine("Prover error: " + s);
- }
- }
+ lock (proverErrors) {
+ proverErrors.Add (s);
+ Console.WriteLine ("Prover error: " + s);
+ }
+ }
- [NoDefaultContract]
- public override Outcome CheckOutcome(ErrorHandler handler)
- {
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
+ [NoDefaultContract]
+ public override Outcome CheckOutcome (ErrorHandler handler)
+ {
+ Contract.EnsuresOnThrow<UnexpectedProverOutputException> (true);
- var result = CheckOutcomeCore(handler);
- SendThisVC("(pop 1)");
- FlushLogFile();
+ var result = CheckOutcomeCore (handler);
+ SendThisVC ("(pop 1)");
+ FlushLogFile ();
- return result;
- }
+ return result;
+ }
- [NoDefaultContract]
- public override Outcome CheckOutcomeCore(ErrorHandler handler)
- {
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
+ [NoDefaultContract]
+ public override Outcome CheckOutcomeCore (ErrorHandler handler)
+ {
+ Contract.EnsuresOnThrow<UnexpectedProverOutputException> (true);
- var result = Outcome.Undetermined;
+ var result = Outcome.Undetermined;
- if (Process == null)
- return result;
+ if (Process == null)
+ return result;
- try {
- currentErrorHandler = handler;
- FlushProverWarnings();
+ try {
+ currentErrorHandler = handler;
+ FlushProverWarnings ();
- var errorsLeft = CommandLineOptions.Clo.ProverCCLimit;
- if (errorsLeft < 1)
- errorsLeft = 1;
+ var errorsLeft = CommandLineOptions.Clo.ProverCCLimit;
+ if (errorsLeft < 1)
+ errorsLeft = 1;
- var globalResult = Outcome.Undetermined;
+ var globalResult = Outcome.Undetermined;
- while (true) {
- errorsLeft--;
- string[] labels = null;
-
- result = GetResponse();
- if (globalResult == Outcome.Undetermined)
- globalResult = result;
-
- if (result == Outcome.Invalid || result == Outcome.TimeOut || result == Outcome.OutOfMemory) {
- IList<string> xlabels;
- if (CommandLineOptions.Clo.UseLabels) {
- labels = GetLabelsInfo();
- if (labels == null)
- {
- xlabels = new string[] { };
+ while (true) {
+ errorsLeft--;
+ string[] labels = null;
+
+ result = GetResponse ();
+ if (globalResult == Outcome.Undetermined)
+ globalResult = result;
+
+ if (result == Outcome.Invalid || result == Outcome.TimeOut || result == Outcome.OutOfMemory) {
+ IList<string> xlabels;
+ if (CommandLineOptions.Clo.UseLabels) {
+ labels = GetLabelsInfo ();
+ if (labels == null) {
+ xlabels = new string[] { };
}
else
{
@@ -1220,7 +1179,12 @@ namespace Microsoft.Boogie.SMTLib public override void SetTimeOut(int ms)
{
- SendThisVC("(set-option :" + Z3.SetTimeoutOption() + " " + ms.ToString() + ")");
+ var name = Z3.SetTimeoutOption();
+ var value = ms.ToString();
+ options.TimeLimit = ms;
+ options.SmtOptions.RemoveAll(ov => ov.Option == name);
+ options.AddSmtOption(name, value);
+ SendThisVC(string.Format("(set-option :{0} {1})", name, value));
}
public override object Evaluate(VCExpr expr)
diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs index 2ff93c54..cac6d95b 100644 --- a/Source/VCExpr/Boogie2VCExpr.cs +++ b/Source/VCExpr/Boogie2VCExpr.cs @@ -1125,43 +1125,50 @@ namespace Microsoft.Boogie.VCExprAST { Contract.Requires(cce.NonNullElements(typeArgs));
Contract.Assert(app.Func != null); // resolution must have happened
- if (app.Func.doingExpansion) {
- System.Console.WriteLine("*** detected expansion loop on {0}", app.Func);
- return null;
- }
+ lock (app.Func)
+ {
+ if (app.Func.doingExpansion)
+ {
+ System.Console.WriteLine("*** detected expansion loop on {0}", app.Func);
+ return null;
+ }
- var exp = app.Func.Body;
- if (exp == null)
- return null;
+ var exp = app.Func.Body;
+ if (exp == null)
+ return null;
- VCExpr/*!*/ translatedBody;
- VCExprSubstitution/*!*/ subst = new VCExprSubstitution();
- try {
- BaseTranslator.PushFormalsScope();
- BaseTranslator.PushBoundVariableScope();
- app.Func.doingExpansion = true;
-
- // first bind the formals to VCExpr variables, which are later
- // substituted with the actual parameters
- var inParams = app.Func.InParams;
- for (int i = 0; i < inParams.Length; ++i)
- subst[BaseTranslator.BindVariable(inParams[i])] = args[i];
-
- // recursively translate the body of the expansion
- translatedBody = BaseTranslator.Translate(exp);
- } finally {
- BaseTranslator.PopFormalsScope();
- BaseTranslator.PopBoundVariableScope();
- app.Func.doingExpansion = false;
- }
+ VCExpr/*!*/ translatedBody;
+ VCExprSubstitution/*!*/ subst = new VCExprSubstitution();
+ try
+ {
+ BaseTranslator.PushFormalsScope();
+ BaseTranslator.PushBoundVariableScope();
+ app.Func.doingExpansion = true;
+
+ // first bind the formals to VCExpr variables, which are later
+ // substituted with the actual parameters
+ var inParams = app.Func.InParams;
+ for (int i = 0; i < inParams.Length; ++i)
+ subst[BaseTranslator.BindVariable(inParams[i])] = args[i];
+
+ // recursively translate the body of the expansion
+ translatedBody = BaseTranslator.Translate(exp);
+ }
+ finally
+ {
+ BaseTranslator.PopFormalsScope();
+ BaseTranslator.PopBoundVariableScope();
+ app.Func.doingExpansion = false;
+ }
- // substitute the formals with the actual parameters in the body
- var tparms = app.Func.TypeParameters;
- Contract.Assert(typeArgs.Count == tparms.Length);
- for (int i = 0; i < typeArgs.Count; ++i)
- subst[tparms[i]] = typeArgs[i];
- SubstitutingVCExprVisitor/*!*/ substituter = new SubstitutingVCExprVisitor(Gen);
- return substituter.Mutate(translatedBody, subst);
+ // substitute the formals with the actual parameters in the body
+ var tparms = app.Func.TypeParameters;
+ Contract.Assert(typeArgs.Count == tparms.Length);
+ for (int i = 0; i < typeArgs.Count; ++i)
+ subst[tparms[i]] = typeArgs[i];
+ SubstitutingVCExprVisitor/*!*/ substituter = new SubstitutingVCExprVisitor(Gen);
+ return substituter.Mutate(translatedBody, subst);
+ }
}
}
}
diff --git a/Source/VCExpr/NameClashResolver.cs b/Source/VCExpr/NameClashResolver.cs index a78a6103..a46105f8 100644 --- a/Source/VCExpr/NameClashResolver.cs +++ b/Source/VCExpr/NameClashResolver.cs @@ -33,15 +33,13 @@ namespace Microsoft.Boogie.VCExprAST { private UniqueNamer(UniqueNamer namer) {
Contract.Requires(namer != null);
+
Spacer = namer.Spacer;
GlobalNames = new Dictionary<Object, string>(namer.GlobalNames);
-
- List<IDictionary<Object/*!*/, string/*!*/>/*!*/>/*!*/ localNames =
- new List<IDictionary<Object, string>>();
- LocalNames = localNames;
+ LocalNames = new List<IDictionary<Object, string>>();
foreach (IDictionary<Object/*!*/, string/*!*/>/*!*/ d in namer.LocalNames)
- localNames.Add(new Dictionary<Object/*!*/, string/*!*/>(d));
+ LocalNames.Add(new Dictionary<Object/*!*/, string/*!*/>(d));
UsedNames = new HashSet<string>(namer.UsedNames);
CurrentCounters = new Dictionary<string, int>(namer.CurrentCounters);
@@ -53,6 +51,16 @@ namespace Microsoft.Boogie.VCExprAST { return new UniqueNamer(this);
}
+ public void Reset()
+ {
+ GlobalNames.Clear();
+ LocalNames.Clear();
+ LocalNames.Add(new Dictionary<Object/*!*/, string/*!*/>());
+ UsedNames.Clear();
+ CurrentCounters.Clear();
+ GlobalPlusLocalNames.Clear();
+ }
+
////////////////////////////////////////////////////////////////////////////
private readonly IDictionary<Object/*!*/, string/*!*/>/*!*/ GlobalNames;
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index a3f266ef..3a8a1af9 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -53,7 +53,7 @@ namespace Microsoft.Boogie { private TimeSpan proverRunTime;
private volatile ProverInterface.ErrorHandler handler;
private volatile CheckerStatus status;
- public readonly Program Program;
+ public volatile Program Program;
public void GetReady()
{
@@ -178,49 +178,68 @@ namespace Microsoft.Boogie { 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);
- }
+ lock (this)
+ {
+ hasOutput = default(bool);
+ outcome = default(ProverInterface.Outcome);
+ outputExn = default(UnexpectedProverOutputException);
+ handler = default(ProverInterface.ErrorHandler);
TheoremProver.FullReset();
+ ctx.Reset();
+ Setup(prog, ctx);
+ this.timeout = timeout;
+ SetTimeout();
+ }
}
- private static void Setup(Program prog, ProverContext ctx)
+ public void SetTimeout()
{
- // set up the context
- foreach (Declaration decl in prog.TopLevelDeclarations.ToList())
+ if (0 < timeout)
{
- 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)
+ TheoremProver.SetTimeOut(timeout * 1000);
+ }
+ else
+ {
+ TheoremProver.SetTimeOut(0);
+ }
+ }
+
+ /// <summary>
+ /// Set up the context.
+ /// </summary>
+ private void Setup(Program prog, ProverContext ctx)
+ {
+ Program = prog;
+ lock (Program.TopLevelDeclarations)
+ {
+ foreach (Declaration decl in Program.TopLevelDeclarations)
{
- ctx.DeclareGlobalVariable(glVarDecl, null);
+ 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);
+ }
}
}
}
@@ -276,32 +295,39 @@ namespace Microsoft.Boogie { }
private void WaitForOutput(object dummy) {
- try {
- outcome = thmProver.CheckOutcome(cce.NonNull(handler));
- } catch (UnexpectedProverOutputException e) {
- outputExn = e;
- }
-
- switch (outcome) {
- case ProverInterface.Outcome.Valid:
- thmProver.LogComment("Valid");
- break;
- case ProverInterface.Outcome.Invalid:
- thmProver.LogComment("Invalid");
- break;
- case ProverInterface.Outcome.TimeOut:
- thmProver.LogComment("Timed out");
- break;
- case ProverInterface.Outcome.OutOfMemory:
- thmProver.LogComment("Out of memory");
- break;
- case ProverInterface.Outcome.Undetermined:
- thmProver.LogComment("Undetermined");
- break;
- }
-
- hasOutput = true;
- proverRunTime = DateTime.UtcNow - proverStart;
+ lock (this)
+ {
+ try
+ {
+ outcome = thmProver.CheckOutcome(cce.NonNull(handler));
+ }
+ catch (UnexpectedProverOutputException e)
+ {
+ outputExn = e;
+ }
+
+ switch (outcome)
+ {
+ case ProverInterface.Outcome.Valid:
+ thmProver.LogComment("Valid");
+ break;
+ case ProverInterface.Outcome.Invalid:
+ thmProver.LogComment("Invalid");
+ break;
+ case ProverInterface.Outcome.TimeOut:
+ thmProver.LogComment("Timed out");
+ break;
+ case ProverInterface.Outcome.OutOfMemory:
+ thmProver.LogComment("Out of memory");
+ break;
+ case ProverInterface.Outcome.Undetermined:
+ thmProver.LogComment("Undetermined");
+ break;
+ }
+
+ hasOutput = true;
+ proverRunTime = DateTime.UtcNow - proverStart;
+ }
}
public void BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler) {
@@ -316,6 +342,7 @@ namespace Microsoft.Boogie { this.handler = handler;
thmProver.Reset();
+ SetTimeout();
proverStart = DateTime.UtcNow;
thmProver.BeginCheck(descriptiveName, vc, handler);
// gen.ClearSharedFormulas(); PR: don't know yet what to do with this guy
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 05e79fb0..ad2b7e68 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -972,44 +972,60 @@ namespace VC { #endregion
- protected Checker FindCheckerFor(int timeout)
+ protected Checker FindCheckerFor(int timeout, bool isBlocking = true)
{
Contract.Ensures(Contract.Result<Checker>() != null);
+ var maxRetries = 3;
lock (checkers)
{
retry:
// Look for existing checker.
for (int i = 0; i < checkers.Count; i++)
{
- var c = checkers.ElementAt(i);
- lock (c)
+ var c = checkers[i];
+ if (Monitor.TryEnter(c))
{
- if (c.WillingToHandle(timeout, program))
+ try
{
- c.GetReady();
- return c;
- }
- else if (c.IsIdle || c.IsClosed)
- {
- if (c.IsIdle)
+ if (c.WillingToHandle(timeout, program))
{
- c.Retarget(program, c.TheoremProver.Context, timeout);
+ c.GetReady();
return c;
}
- else
+ else if (c.IsIdle || c.IsClosed)
{
- checkers.RemoveAt(i);
+ if (c.IsIdle)
+ {
+ c.Retarget(program, c.TheoremProver.Context, timeout);
+ c.GetReady();
+ return c;
+ }
+ else
+ {
+ checkers.RemoveAt(i);
+ }
}
- continue;
+ }
+ finally
+ {
+ Monitor.Exit(c);
}
}
}
if (Cores <= checkers.Count)
{
- Monitor.Wait(checkers, 50);
- goto retry;
+ if (isBlocking || 0 < maxRetries)
+ {
+ Monitor.Wait(checkers, 50);
+ maxRetries--;
+ goto retry;
+ }
+ else
+ {
+ return null;
+ }
}
// Create a new checker.
@@ -1695,10 +1711,14 @@ namespace VC { Contract.Requires(impl != null);
// global variables
- foreach (Variable v in program.TopLevelDeclarations.OfType<Variable>()) {
- if (!(v is Constant))
+ lock (program.TopLevelDeclarations)
+ {
+ foreach (Variable v in program.TopLevelDeclarations.OfType<Variable>())
{
- AllVariables.Add(v);
+ if (!(v is Constant))
+ {
+ AllVariables.Add(v);
+ }
}
}
// implementation parameters
diff --git a/Source/VCGeneration/Context.cs b/Source/VCGeneration/Context.cs index 484ce226..7931a042 100644 --- a/Source/VCGeneration/Context.cs +++ b/Source/VCGeneration/Context.cs @@ -34,7 +34,7 @@ namespace Microsoft.Boogie public abstract Boogie2VCExprTranslator BoogieExprTranslator { get; }
public abstract VCGenerationOptions VCGenOptions { get; }
public abstract object Clone();
- public abstract void Clear();
+ public abstract void Reset();
}
[ContractClassFor(typeof(ProverContext))]
@@ -104,10 +104,8 @@ public abstract class ProverContextContracts:ProverContext{ this.genOptions = genOptions;
Boogie2VCExprTranslator t = new Boogie2VCExprTranslator (gen, genOptions);
this.translator = t;
- OrderingAxiomBuilder oab = new OrderingAxiomBuilder(gen, t);
- Contract.Assert(oab != null);
- oab.Setup();
- this.orderingAxiomBuilder = oab;
+
+ SetupOrderingAxiomBuilder(gen, t);
distincts = new List<Variable>();
axiomConjuncts = new List<VCExpr>();
@@ -115,10 +113,19 @@ public abstract class ProverContextContracts:ProverContext{ exprTranslator = null;
}
- public override void Clear()
+ private void SetupOrderingAxiomBuilder(VCExpressionGenerator gen, Boogie2VCExprTranslator t)
+ {
+ OrderingAxiomBuilder oab = new OrderingAxiomBuilder(gen, t);
+ Contract.Assert(oab != null);
+ oab.Setup();
+ this.orderingAxiomBuilder = oab;
+ }
+
+ public override void Reset()
{
- distincts = new List<Variable>();
- axiomConjuncts = new List<VCExpr>();
+ SetupOrderingAxiomBuilder(gen, translator);
+ distincts = new List<Variable>();
+ axiomConjuncts = new List<VCExpr>();
}
protected DeclFreeProverContext(DeclFreeProverContext ctxt) {
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 48b73bce..80ffa072 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -66,7 +66,6 @@ namespace VC { Contract.Invariant(parent != null);
Contract.Invariant(impl != null);
Contract.Invariant(initial != null);
- Contract.Invariant(program != null);
Contract.Invariant(cce.NonNullDictionaryAndValues(copies));
Contract.Invariant(cce.NonNull(visited));
Contract.Invariant(callback != null);
@@ -75,21 +74,18 @@ namespace VC { VCGen parent;
Implementation impl;
Block initial;
- Program program;
int id;
Dictionary<Block, Block> copies = new Dictionary<Block, Block>();
HashSet<Block> visited = new HashSet<Block>();
VerifierCallback callback;
- internal SmokeTester(VCGen par, Implementation i, Program prog, VerifierCallback callback) {
+ internal SmokeTester(VCGen par, Implementation i, VerifierCallback callback) {
Contract.Requires(par != null);
Contract.Requires(i != null);
- Contract.Requires(prog != null);
Contract.Requires(callback != null);
parent = par;
impl = i;
initial = i.Blocks[0];
- program = prog;
this.callback = callback;
}
@@ -256,18 +252,21 @@ namespace VC { return BooleanEval(e, ref val) && !val;
}
- bool CheckUnreachable(Block cur, CmdSeq seq) {
+ bool CheckUnreachable(Block cur, CmdSeq seq)
+ {
Contract.Requires(cur != null);
Contract.Requires(seq != null);
Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- foreach (Cmd cmd in seq) {
+ foreach (Cmd cmd in seq)
+ {
AssertCmd assrt = cmd as AssertCmd;
if (assrt != null && QKeyValue.FindBoolAttribute(assrt.Attributes, "PossiblyUnreachable"))
return false;
}
DateTime start = DateTime.UtcNow;
- if (CommandLineOptions.Clo.Trace) {
+ if (CommandLineOptions.Clo.Trace)
+ {
System.Console.Write(" soundness smoke test #{0} ... ", id);
}
callback.OnProgress("smoke", id, id, 0.0);
@@ -282,7 +281,8 @@ namespace VC { Contract.Assert(backup != null);
impl.Blocks = GetCopiedBlocks();
copy.TransferCmd = new ReturnCmd(Token.NoToken);
- if (CommandLineOptions.Clo.TraceVerify) {
+ if (CommandLineOptions.Clo.TraceVerify)
+ {
System.Console.WriteLine();
System.Console.WriteLine(" --- smoke #{0}, before passify", id);
Emit();
@@ -294,39 +294,60 @@ namespace VC { Checker ch = parent.FindCheckerFor(CommandLineOptions.Clo.SmokeTimeout);
Contract.Assert(ch != null);
- var exprGen = ch.TheoremProver.Context.ExprGen;
- VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO);
+ ProverInterface.Outcome outcome = ProverInterface.Outcome.Undetermined;
+ try
+ {
+ lock (ch)
+ {
+ var exprGen = ch.TheoremProver.Context.ExprGen;
+ VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO);
- VCExpr vc = parent.GenerateVC(impl, controlFlowVariableExpr, out label2Absy, ch.TheoremProver.Context);
- Contract.Assert(vc != null);
+ VCExpr vc = parent.GenerateVC(impl, controlFlowVariableExpr, out label2Absy, ch.TheoremProver.Context);
+ Contract.Assert(vc != null);
- if (!CommandLineOptions.Clo.UseLabels) {
- VCExpr controlFlowFunctionAppl = exprGen.ControlFlowFunctionApplication(exprGen.Integer(BigNum.ZERO), exprGen.Integer(BigNum.ZERO));
- VCExpr eqExpr = exprGen.Eq(controlFlowFunctionAppl, exprGen.Integer(BigNum.FromInt(impl.Blocks[0].UniqueId)));
- vc = exprGen.Implies(eqExpr, vc);
- }
+ if (!CommandLineOptions.Clo.UseLabels)
+ {
+ VCExpr controlFlowFunctionAppl = exprGen.ControlFlowFunctionApplication(exprGen.Integer(BigNum.ZERO), exprGen.Integer(BigNum.ZERO));
+ VCExpr eqExpr = exprGen.Eq(controlFlowFunctionAppl, exprGen.Integer(BigNum.FromInt(impl.Blocks[0].UniqueId)));
+ vc = exprGen.Implies(eqExpr, vc);
+ }
- impl.Blocks = backup;
+ impl.Blocks = backup;
- if (CommandLineOptions.Clo.TraceVerify) {
- System.Console.WriteLine(" --- smoke #{0}, after passify", id);
- Emit();
+ if (CommandLineOptions.Clo.TraceVerify)
+ {
+ System.Console.WriteLine(" --- smoke #{0}, after passify", id);
+ Emit();
+ }
+
+ ch.BeginCheck(cce.NonNull(impl.Name + "_smoke" + id++), vc, new ErrorHandler(label2Absy, this.callback));
+ }
+
+ ch.ProverTask.Wait();
+
+ lock (ch)
+ {
+ outcome = ch.ReadOutcome();
+ }
}
- ch.BeginCheck(cce.NonNull(impl.Name + "_smoke" + id++), vc, new ErrorHandler(label2Absy, this.callback));
- ch.ProverTask.Wait();
- ProverInterface.Outcome outcome = ch.ReadOutcome();
- ch.GoBackToIdle();
+ finally
+ {
+ ch.GoBackToIdle();
+ }
+
parent.CurrentLocalVariables = null;
DateTime end = DateTime.UtcNow;
TimeSpan elapsed = end - start;
- if (CommandLineOptions.Clo.Trace) {
+ if (CommandLineOptions.Clo.Trace)
+ {
System.Console.WriteLine(" [{0} s] {1}", elapsed.TotalSeconds,
outcome == ProverInterface.Outcome.Valid ? "OOPS" :
"OK" + (outcome == ProverInterface.Outcome.Invalid ? "" : " (" + outcome + ")"));
}
- if (outcome == ProverInterface.Outcome.Valid) {
+ if (outcome == ProverInterface.Outcome.Valid)
+ {
// copy it again, so we get the version with calls, assignments and such
copy = CopyBlock(cur);
copy.Cmds = seq;
@@ -1187,21 +1208,25 @@ namespace VC { /// <summary>
/// As a side effect, updates "this.parent.CumulativeAssertionCount".
/// </summary>
- public void BeginCheck(VerifierCallback callback, ModelViewInfo mvInfo, int no, int timeout) {
+ public void BeginCheck(Checker checker, VerifierCallback callback, ModelViewInfo mvInfo, int no, int timeout)
+ {
+ Contract.Requires(checker != null);
Contract.Requires(callback != null);
+
splitNo = no;
impl.Blocks = blocks;
- checker = parent.FindCheckerFor(timeout);
+ this.checker = checker;
+
Hashtable/*<int, Absy!>*/ label2absy = new Hashtable/*<int, Absy!>*/();
- ProverInterface tp = checker.TheoremProver;
- ProverContext ctx = tp.Context;
+ ProverContext ctx = checker.TheoremProver.Context;
Boogie2VCExprTranslator bet = ctx.BoogieExprTranslator;
bet.SetCodeExprConverter(
new CodeExprConverter(
- delegate (CodeExpr codeExpr, Hashtable/*<Block, VCExprVar!>*/ blockVariables, List<VCExprLetBinding/*!*/> bindings) {
+ delegate(CodeExpr codeExpr, Hashtable/*<Block, VCExprVar!>*/ blockVariables, List<VCExprLetBinding/*!*/> bindings)
+ {
VCGen vcgen = new VCGen(new Program(), null, false, parent.checkers);
vcgen.variable2SequenceNumber = new Hashtable/*Variable -> int*/();
vcgen.incarnationOriginMap = new Dictionary<Incarnation, Absy>();
@@ -1215,15 +1240,18 @@ namespace VC { VCExpr startCorrect = VCGen.LetVC(codeExpr.Blocks[0], null, label2absy, blockVariables, bindings, ctx, out ac);
VCExpr vce = ctx.ExprGen.Let(bindings, startCorrect);
- if (vcgen.CurrentLocalVariables.Length != 0) {
+ if (vcgen.CurrentLocalVariables.Length != 0)
+ {
Boogie2VCExprTranslator translator = checker.TheoremProver.Context.BoogieExprTranslator;
List<VCExprVar> boundVars = new List<VCExprVar>();
- foreach (Variable v in vcgen.CurrentLocalVariables) {
+ foreach (Variable v in vcgen.CurrentLocalVariables)
+ {
Contract.Assert(v != null);
VCExprVar ev = translator.LookupVariable(v);
Contract.Assert(ev != null);
boundVars.Add(ev);
- if (v.TypedIdent.Type.Equals(Bpl.Type.Bool)) {
+ if (v.TypedIdent.Type.Equals(Bpl.Type.Bool))
+ {
// add an antecedent (tickleBool ev) to help the prover find a possible trigger
vce = checker.VCExprGen.Implies(checker.VCExprGen.Function(VCExpressionGenerator.TickleBoolOp, ev), vce);
}
@@ -1232,7 +1260,7 @@ namespace VC { }
return vce;
}
- ));
+ ));
var exprGen = ctx.ExprGen;
VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO);
@@ -1240,19 +1268,24 @@ namespace VC { VCExpr vc = parent.GenerateVCAux(impl, controlFlowVariableExpr, label2absy, checker.TheoremProver.Context);
Contract.Assert(vc != null);
- if (!CommandLineOptions.Clo.UseLabels) {
+ if (!CommandLineOptions.Clo.UseLabels)
+ {
VCExpr controlFlowFunctionAppl = exprGen.ControlFlowFunctionApplication(exprGen.Integer(BigNum.ZERO), exprGen.Integer(BigNum.ZERO));
VCExpr eqExpr = exprGen.Eq(controlFlowFunctionAppl, exprGen.Integer(BigNum.FromInt(impl.Blocks[0].UniqueId)));
vc = exprGen.Implies(eqExpr, vc);
}
-
- if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local) {
+
+ if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local)
+ {
reporter = new ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, parent.incarnationOriginMap, callback, mvInfo, cce.NonNull(this.Checker.TheoremProver.Context), parent.program);
- } else {
+ }
+ else
+ {
reporter = new ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, parent.incarnationOriginMap, callback, mvInfo, this.Checker.TheoremProver.Context, parent.program);
}
- if (CommandLineOptions.Clo.TraceVerify && no >= 0) {
+ if (CommandLineOptions.Clo.TraceVerify && no >= 0)
+ {
Console.WriteLine("-- after split #{0}", no);
Print();
}
@@ -1407,16 +1440,12 @@ namespace VC { SmokeTester smoke_tester = null;
if (CommandLineOptions.Clo.SoundnessSmokeTest) {
- smoke_tester = new SmokeTester(this, impl, program, callback);
+ smoke_tester = new SmokeTester(this, impl, callback);
smoke_tester.Copy();
}
ModelViewInfo mvInfo;
- Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins;
- lock (program)
- {
- gotoCmdOrigins = PassifyImpl(impl, out mvInfo);
- }
+ var gotoCmdOrigins = PassifyImpl(impl, out mvInfo);
double max_vc_cost = CommandLineOptions.Clo.VcsMaxCost;
int tmp_max_vc_cost = -1, max_splits = CommandLineOptions.Clo.VcsMaxSplits,
@@ -1447,104 +1476,157 @@ namespace VC { remaining_cost = work.Peek().Cost;
}
- while (work.Any() || currently_running.Any()) {
+ while (work.Any() || currently_running.Any())
+ {
bool prover_failed = false;
- Split s;
+ Split s = null;
+ var isWaiting = !work.Any();
- if (work.Any() && currently_running.Count < Cores) {
- s = work.Pop();
+ if (!isWaiting)
+ {
+ s = work.Peek();
- if (first_round && max_splits > 1) {
+ if (first_round && max_splits > 1)
+ {
prover_failed = true;
remaining_cost -= s.Cost;
- } else {
- if (CommandLineOptions.Clo.Trace && no >= 0) {
- System.Console.WriteLine(" checking split {1}/{2}, {3:0.00}%, {0} ...",
+ }
+ else
+ {
+ var timeout = (keep_going && s.LastChance) ? CommandLineOptions.Clo.VcsFinalAssertTimeout :
+ keep_going ? CommandLineOptions.Clo.VcsKeepGoingTimeout :
+ impl.TimeLimit;
+
+ var checker = s.parent.FindCheckerFor(timeout, false);
+ if (checker == null)
+ {
+ isWaiting = true;
+ goto waiting;
+ }
+ else
+ {
+ s = work.Pop();
+ }
+
+ if (CommandLineOptions.Clo.Trace && no >= 0)
+ {
+ System.Console.WriteLine(" checking split {1}/{2}, {3:0.00}%, {0} ...",
s.Stats, no + 1, total, 100 * proven_cost / (proven_cost + remaining_cost));
}
callback.OnProgress("VCprove", no < 0 ? 0 : no, total, proven_cost / (remaining_cost + proven_cost));
Contract.Assert(s.parent == this);
- lock (program)
+ lock (checker)
{
- s.BeginCheck(callback, mvInfo, no,
- (keep_going && s.LastChance) ? CommandLineOptions.Clo.VcsFinalAssertTimeout :
- keep_going ? CommandLineOptions.Clo.VcsKeepGoingTimeout :
- CommandLineOptions.Clo.ProverKillTime);
+ s.BeginCheck(checker, callback, mvInfo, no, timeout);
}
no++;
currently_running.Add(s);
}
- } else {
+ }
+
+ waiting:
+ if (isWaiting)
+ {
// 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);
- if (do_splitting) {
- remaining_cost -= s.Cost;
- }
+ if (tasks.Any())
+ {
+ try
+ {
+ int index = Task.WaitAny(tasks);
+ s = currently_running[index];
+ currently_running.RemoveAt(index);
- s.ReadOutcome(ref outcome, out prover_failed);
+ if (do_splitting)
+ {
+ remaining_cost -= s.Cost;
+ }
- if (do_splitting) {
- if (prover_failed) {
- // even if the prover fails, we have learned something, i.e., it is
- // annoying to watch Boogie say Timeout, 0.00% a couple of times
- proven_cost += s.Cost / 100;
- } else {
- proven_cost += s.Cost;
- }
- }
- callback.OnProgress("VCprove", no < 0 ? 0 : no, total, proven_cost / (remaining_cost + proven_cost));
+ lock (s.Checker)
+ {
+ s.ReadOutcome(ref outcome, out prover_failed);
+ }
- if (prover_failed && !first_round && s.LastChance) {
- string msg = "some timeout";
- if (s.reporter != null && s.reporter.resourceExceededMessage != null) {
- msg = s.reporter.resourceExceededMessage;
- }
- callback.OnCounterexample(s.ToCounterexample(s.Checker.TheoremProver.Context), msg);
- outcome = Outcome.Errors;
- break;
- }
+ if (do_splitting)
+ {
+ if (prover_failed)
+ {
+ // even if the prover fails, we have learned something, i.e., it is
+ // annoying to watch Boogie say Timeout, 0.00% a couple of times
+ proven_cost += s.Cost / 100;
+ }
+ else
+ {
+ proven_cost += s.Cost;
+ }
+ }
+ callback.OnProgress("VCprove", no < 0 ? 0 : no, total, proven_cost / (remaining_cost + proven_cost));
- s.Checker.GoBackToIdle();
+ if (prover_failed && !first_round && s.LastChance)
+ {
+ string msg = "some timeout";
+ if (s.reporter != null && s.reporter.resourceExceededMessage != null)
+ {
+ msg = s.reporter.resourceExceededMessage;
+ }
+ callback.OnCounterexample(s.ToCounterexample(s.Checker.TheoremProver.Context), msg);
+ outcome = Outcome.Errors;
+ break;
+ }
+ }
+ finally
+ {
+ s.Checker.GoBackToIdle();
+ }
- Contract.Assert( prover_failed || outcome == Outcome.Correct || outcome == Outcome.Errors || outcome == Outcome.Inconclusive);
+ Contract.Assert(prover_failed || outcome == Outcome.Correct || outcome == Outcome.Errors || outcome == Outcome.Inconclusive);
+ }
}
- if (prover_failed) {
+ if (prover_failed)
+ {
int splits = first_round && max_splits > 1 ? max_splits : max_kg_splits;
- if (splits > 1) {
+ if (splits > 1)
+ {
List<Split> tmp = Split.DoSplit(s, max_vc_cost, splits);
Contract.Assert(tmp != null);
max_vc_cost = 1.0; // for future
first_round = false;
//tmp.Sort(new Comparison<Split!>(Split.Compare));
- foreach (Split a in tmp) {
+ foreach (Split a in tmp)
+ {
Contract.Assert(a != null);
work.Push(a);
total++;
remaining_cost += a.Cost;
}
- if (outcome != Outcome.Errors) {
+ if (outcome != Outcome.Errors)
+ {
outcome = Outcome.Correct;
}
- } else {
- Contract.Assert( outcome != Outcome.Correct);
- if (outcome == Outcome.TimedOut) {
+ }
+ else
+ {
+ Contract.Assert(outcome != Outcome.Correct);
+ if (outcome == Outcome.TimedOut)
+ {
string msg = "some timeout";
- if (s.reporter != null && s.reporter.resourceExceededMessage != null) {
+ if (s.reporter != null && s.reporter.resourceExceededMessage != null)
+ {
msg = s.reporter.resourceExceededMessage;
}
callback.OnTimeout(msg);
- } else if (outcome == Outcome.OutOfMemory) {
+ }
+ else if (outcome == Outcome.OutOfMemory)
+ {
string msg = "out of memory";
- if (s.reporter != null && s.reporter.resourceExceededMessage != null) {
+ if (s.reporter != null && s.reporter.resourceExceededMessage != null)
+ {
msg = s.reporter.resourceExceededMessage;
}
callback.OnOutOfMemory(msg);
@@ -1556,10 +1638,7 @@ namespace VC { }
if (outcome == Outcome.Correct && smoke_tester != null) {
- lock (program)
- {
- smoke_tester.Test();
- }
+ smoke_tester.Test();
}
callback.OnProgress("done", 0, 0, 1.0);
@@ -1661,7 +1740,7 @@ namespace VC { Contract.Assert(traceNodes.Contains(entryBlock));
trace.Add(entryBlock);
- Counterexample newCounterexample = TraceCounterexample(entryBlock, traceNodes, trace, model, MvInfo, incarnationOriginMap, context, program, new Dictionary<TraceLocation, CalleeCounterexampleInfo>());
+ Counterexample newCounterexample = TraceCounterexample(entryBlock, traceNodes, trace, model, MvInfo, incarnationOriginMap, context, new Dictionary<TraceLocation, CalleeCounterexampleInfo>());
if (newCounterexample == null)
return;
@@ -2039,11 +2118,15 @@ namespace VC { {
CmdSeq cc = new CmdSeq();
// where clauses of global variables
- foreach (Declaration d in program.TopLevelDeclarations) {
- GlobalVariable gvar = d as GlobalVariable;
- if (gvar != null && gvar.TypedIdent.WhereExpr != null) {
- Cmd c = new AssumeCmd(gvar.tok, gvar.TypedIdent.WhereExpr);
- cc.Add(c);
+ lock (program.TopLevelDeclarations)
+ {
+ foreach (var gvar in program.TopLevelDeclarations.OfType<GlobalVariable>())
+ {
+ if (gvar != null && gvar.TypedIdent.WhereExpr != null)
+ {
+ Cmd c = new AssumeCmd(gvar.tok, gvar.TypedIdent.WhereExpr);
+ cc.Add(c);
+ }
}
}
// where clauses of in- and out-parameters
@@ -2118,7 +2201,10 @@ namespace VC { List<Expr> axioms;
List<Function> functions;
LambdaHelper.Desugar(impl, out axioms, out functions);
- program.TopLevelDeclarations.AddRange(functions);
+ lock (program.TopLevelDeclarations)
+ {
+ program.TopLevelDeclarations.AddRange(functions);
+ }
if (axioms.Count > 0) {
CmdSeq cmds = new CmdSeq();
@@ -2364,7 +2450,7 @@ namespace VC { static Counterexample TraceCounterexample(
Block/*!*/ b, Hashtable/*!*/ traceNodes, BlockSeq/*!*/ trace, Model errModel, ModelViewInfo mvInfo,
Dictionary<Incarnation, Absy/*!*/>/*!*/ incarnationOriginMap,
- ProverContext/*!*/ context, Program/*!*/ program,
+ ProverContext/*!*/ context,
Dictionary<TraceLocation/*!*/, CalleeCounterexampleInfo/*!*/>/*!*/ calleeCounterexamples)
{
Contract.Requires(b != null);
@@ -2372,7 +2458,6 @@ namespace VC { Contract.Requires(trace != null);
Contract.Requires(cce.NonNullDictionaryAndValues(incarnationOriginMap));
Contract.Requires(context != null);
- Contract.Requires(program != null);
Contract.Requires(cce.NonNullDictionaryAndValues(calleeCounterexamples));
// After translation, all potential errors come from asserts.
CmdSeq cmds = b.Cmds;
@@ -2400,7 +2485,7 @@ namespace VC { Contract.Assert(bb != null);
if (traceNodes.Contains(bb)){
trace.Add(bb);
- return TraceCounterexample(bb, traceNodes, trace, errModel, mvInfo, incarnationOriginMap, context, program, calleeCounterexamples);
+ return TraceCounterexample(bb, traceNodes, trace, errModel, mvInfo, incarnationOriginMap, context, calleeCounterexamples);
}
}
}
diff --git a/Test/linear/typecheck.bpl b/Test/linear/typecheck.bpl index 7bdb339e..ebd3d07d 100644 --- a/Test/linear/typecheck.bpl +++ b/Test/linear/typecheck.bpl @@ -80,3 +80,24 @@ modifies g; {
g := r;
}
+
+procedure I({:linear ""} x:int) returns({:linear ""} x':int)
+{
+ x' := x;
+}
+
+procedure J()
+{
+}
+
+procedure P1({:linear ""} x:int) returns({:linear ""} x':int)
+{
+ call x' := I(x) | J();
+ call x' := I(x');
+}
+
+procedure P2({:linear ""} x:int) returns({:linear ""} x':int)
+{
+ call x' := I(x);
+ call x' := I(x') | J();
+}
diff --git a/Test/og/Answer b/Test/og/Answer index c29d38dc..d663de9a 100644 --- a/Test/og/Answer +++ b/Test/og/Answer @@ -98,3 +98,12 @@ Boogie program verifier finished with 2 verified, 0 errors -------------------- perm.bpl --------------------
Boogie program verifier finished with 2 verified, 0 errors
+
+-------------------- async.bpl --------------------
+async.bpl(13,1): Error BP5001: This assertion might not hold.
+Execution trace:
+ async.bpl(6,3): anon0
+ async.bpl(6,3): anon0$1
+ (0,0): inline$Proc_YieldChecker_P$1$L0
+
+Boogie program verifier finished with 1 verified, 1 error
diff --git a/Test/og/async.bpl b/Test/og/async.bpl new file mode 100644 index 00000000..15f89bae --- /dev/null +++ b/Test/og/async.bpl @@ -0,0 +1,16 @@ +var x: int;
+var y: int;
+
+procedure {:entrypoint} foo()
+{
+ assume x == y;
+ x := x + 1;
+ async call P();
+ y := y + 1;
+}
+
+procedure P()
+requires x != y;
+{
+ assert x != y;
+}
\ No newline at end of file diff --git a/Test/og/runtest.bat b/Test/og/runtest.bat index dd07b4a4..5915a206 100644 --- a/Test/og/runtest.bat +++ b/Test/og/runtest.bat @@ -9,7 +9,7 @@ for %%f in (foo.bpl bar.bpl one.bpl parallel1.bpl parallel3.bpl) do ( %BGEXE% %* /nologo /noinfer /doModSetAnalysis /OwickiGries:OwickiGriesDesugared.bpl %%f
)
-for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl DeviceCacheSimplified.bpl parallel2.bpl parallel4.bpl parallel5.bpl parallel6.bpl parallel7.bpl akash.bpl t1.bpl new1.bpl perm.bpl) do (
+for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl DeviceCacheSimplified.bpl parallel2.bpl parallel4.bpl parallel5.bpl parallel6.bpl parallel7.bpl akash.bpl t1.bpl new1.bpl perm.bpl async.bpl) do (
echo.
echo -------------------- %%f --------------------
%BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory /doModSetAnalysis /OwickiGries:OwickiGriesDesugared.bpl %%f
diff --git a/Test/snapshots/Answer b/Test/snapshots/Answer index 676f0323..dc0ee8c1 100644 --- a/Test/snapshots/Answer +++ b/Test/snapshots/Answer @@ -1,5 +1,3 @@ -
--------------------- Snapshots0 --------------------
Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold.
Execution trace:
Snapshots0.v0.bpl(41,5): anon0
@@ -27,8 +25,6 @@ Execution trace: Snapshots0.v0.bpl(41,5): anon0
Boogie program verifier finished with 2 verified, 1 error
-
--------------------- Snapshots1 --------------------
Snapshots1.v0.bpl(13,5): Error BP5001: This assertion might not hold.
Execution trace:
Snapshots1.v0.bpl(13,5): anon0
@@ -46,8 +42,6 @@ Execution trace: Boogie program verifier finished with 1 verified, 1 error
--------------------- Snapshots2 --------------------
-
Boogie program verifier finished with 1 verified, 0 errors
Boogie program verifier finished with 1 verified, 0 errors
@@ -60,8 +54,6 @@ Boogie program verifier finished with 1 verified, 0 errors Boogie program verifier finished with 1 verified, 0 errors
--------------------- Snapshots3 --------------------
-
Boogie program verifier finished with 1 verified, 0 errors
Snapshots3.v1.bpl(6,1): Error BP5003: A postcondition might not hold on this return path.
Snapshots3.v1.bpl(2,1): Related location: This is the postcondition that might not hold.
diff --git a/Test/snapshots/runtest.bat b/Test/snapshots/runtest.bat index 663cef07..e54a19bc 100644 --- a/Test/snapshots/runtest.bat +++ b/Test/snapshots/runtest.bat @@ -4,8 +4,5 @@ setlocal set BOOGIEDIR=..\..\Binaries
set BGEXE=%BOOGIEDIR%\Boogie.exe
-for %%f in (Snapshots0 Snapshots1 Snapshots2 Snapshots3) do (
- echo.
- echo -------------------- %%f --------------------
- %BGEXE% %* /verifySnapshots %%f.bpl
-)
+%BGEXE% %* /verifySnapshots /verifySeparately Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl
+
diff --git a/Test/test2/Answer b/Test/test2/Answer index 5f8642e1..e9390250 100644 --- a/Test/test2/Answer +++ b/Test/test2/Answer @@ -502,5 +502,45 @@ Execution trace: Timeouts0.bpl(10,5): anon4_LoopDone
Timeouts0.bpl(19,5): anon5_LoopHead
Timeouts0.bpl(23,11): anon5_LoopBody
-
-Boogie program verifier finished with 0 verified, 0 errors, 1 time out
+Timeouts0.bpl(41,7): Timed out on BP5005: This loop invariant might not be maintained by the loop.
+Execution trace:
+ Timeouts0.bpl(37,7): anon0
+ Timeouts0.bpl(39,5): anon4_LoopHead
+ Timeouts0.bpl(43,20): anon4_LoopBody
+Timeouts0.bpl(48,5): Timed out on BP5003: A postcondition might not hold on this return path.
+Timeouts0.bpl(31,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ Timeouts0.bpl(37,7): anon0
+ Timeouts0.bpl(39,5): anon4_LoopHead
+ Timeouts0.bpl(39,5): anon4_LoopDone
+ Timeouts0.bpl(48,5): anon5_LoopHead
+ Timeouts0.bpl(48,5): anon5_LoopDone
+Timeouts0.bpl(50,7): Timed out on BP5005: This loop invariant might not be maintained by the loop.
+Execution trace:
+ Timeouts0.bpl(37,7): anon0
+ Timeouts0.bpl(39,5): anon4_LoopHead
+ Timeouts0.bpl(39,5): anon4_LoopDone
+ Timeouts0.bpl(48,5): anon5_LoopHead
+ Timeouts0.bpl(52,11): anon5_LoopBody
+Timeouts0.bpl(70,7): Timed out on BP5005: This loop invariant might not be maintained by the loop.
+Execution trace:
+ Timeouts0.bpl(66,7): anon0
+ Timeouts0.bpl(68,5): anon4_LoopHead
+ Timeouts0.bpl(72,20): anon4_LoopBody
+Timeouts0.bpl(77,5): Timed out on BP5003: A postcondition might not hold on this return path.
+Timeouts0.bpl(60,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ Timeouts0.bpl(66,7): anon0
+ Timeouts0.bpl(68,5): anon4_LoopHead
+ Timeouts0.bpl(68,5): anon4_LoopDone
+ Timeouts0.bpl(77,5): anon5_LoopHead
+ Timeouts0.bpl(77,5): anon5_LoopDone
+Timeouts0.bpl(79,7): Timed out on BP5005: This loop invariant might not be maintained by the loop.
+Execution trace:
+ Timeouts0.bpl(66,7): anon0
+ Timeouts0.bpl(68,5): anon4_LoopHead
+ Timeouts0.bpl(68,5): anon4_LoopDone
+ Timeouts0.bpl(77,5): anon5_LoopHead
+ Timeouts0.bpl(81,11): anon5_LoopBody
+
+Boogie program verifier finished with 0 verified, 0 errors, 3 time outs
diff --git a/Test/test2/Timeouts0.bpl b/Test/test2/Timeouts0.bpl index c74e9320..c874a1c1 100644 --- a/Test/test2/Timeouts0.bpl +++ b/Test/test2/Timeouts0.bpl @@ -23,3 +23,61 @@ procedure TestTimeouts0(in: [int]int, len: int) returns (out: [int]int) i := i + 1;
}
}
+
+
+procedure TestTimeouts1(in: [int]int, len: int) returns (out: [int]int);
+ requires in[0] == 0 && (forall i: int :: 0 <= i ==> in[i + 1] == in[i] + 1);
+ requires 0 < len;
+ ensures (forall j: int :: 0 <= j && j < len ==> out[j] == j);
+
+implementation {:timeLimit 8} TestTimeouts1(in: [int]int, len: int) returns (out: [int]int)
+{
+ var i : int;
+
+ i := 0;
+ out[i] := 0;
+ while (i < len)
+ invariant 0 <= i && i <= len;
+ invariant out[0] == 0 && (forall j: int :: 0 <= j && j < i ==> out[j + 1] == out[j] + 1);
+ {
+ out[i + 1] := out[i] + 1;
+ i := i + 1;
+ }
+
+ i := 0;
+ while (i < len)
+ invariant 0 <= i && i <= len;
+ invariant (forall j: int :: 0 <= j && j < i ==> out[j] == in[j]);
+ {
+ i := i + 1;
+ }
+}
+
+
+procedure TestTimeouts2(in: [int]int, len: int) returns (out: [int]int);
+ requires in[0] == 0 && (forall i: int :: 0 <= i ==> in[i + 1] == in[i] + 1);
+ requires 0 < len;
+ ensures (forall j: int :: 0 <= j && j < len ==> out[j] == j);
+
+implementation {:timeLimit 2} TestTimeouts2(in: [int]int, len: int) returns (out: [int]int)
+{
+ var i : int;
+
+ i := 0;
+ out[i] := 0;
+ while (i < len)
+ invariant 0 <= i && i <= len;
+ invariant out[0] == 0 && (forall j: int :: 0 <= j && j < i ==> out[j + 1] == out[j] + 1);
+ {
+ out[i + 1] := out[i] + 1;
+ i := i + 1;
+ }
+
+ i := 0;
+ while (i < len)
+ invariant 0 <= i && i <= len;
+ invariant (forall j: int :: 0 <= j && j < i ==> out[j] == in[j]);
+ {
+ i := i + 1;
+ }
+}
|