diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Core/Absy.cs | 45 | ||||
| -rw-r--r-- | Source/Core/AbsyCmd.cs | 87 | ||||
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 5 | ||||
| -rw-r--r-- | Source/Core/Duplicator.cs | 39 | ||||
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 56 | ||||
| -rw-r--r-- | Source/ExecutionEngine/VerificationResultCache.cs | 212 | ||||
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 39 |
7 files changed, 441 insertions, 42 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 3b517c51..0026a3fe 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -2664,6 +2664,51 @@ namespace Microsoft.Boogie { }
}
+ // TODO(wuestholz): Make this a 'List<Counterexample>'.
+ public IList<object> ErrorsInCachedSnapshot { get; set; }
+
+ public bool NoErrorsInCachedSnapshot
+ {
+ get
+ {
+ return ErrorsInCachedSnapshot != null && !ErrorsInCachedSnapshot.Any();
+ }
+ }
+
+ public bool AnyErrorsInCachedSnapshot
+ {
+ get
+ {
+ return ErrorsInCachedSnapshot != null && ErrorsInCachedSnapshot.Any();
+ }
+ }
+
+ IList<LocalVariable> injectedAssumptionVariables;
+ public IList<LocalVariable> InjectedAssumptionVariables
+ {
+ get
+ {
+ return injectedAssumptionVariables;
+ }
+ }
+
+ public Expr ConjunctionOfInjectedAssumptionVariables()
+ {
+ Contract.Requires(InjectedAssumptionVariables != null && InjectedAssumptionVariables.Any());
+
+ return LiteralExpr.BinaryTreeAnd(injectedAssumptionVariables.Select(v => (Expr)(new IdentifierExpr(Token.NoToken, v))).ToList());
+ }
+
+ public void InjectAssumptionVariable(LocalVariable variable)
+ {
+ if (injectedAssumptionVariables == null)
+ {
+ injectedAssumptionVariables = new List<LocalVariable>();
+ }
+ injectedAssumptionVariables.Add(variable);
+ LocVars.Add(variable);
+ }
+
public Implementation(IToken tok, string name, List<TypeVariable> typeParams, List<Variable> inParams, List<Variable> outParams, List<Variable> localVariables, [Captured] StmtList structuredStmts, QKeyValue kv)
: this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, kv, new Errors()) {
Contract.Requires(structuredStmts != null);
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index 1922f977..c7ad0f11 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -1682,6 +1682,24 @@ namespace Microsoft.Boogie { }
protected abstract Cmd/*!*/ ComputeDesugaring();
+ public void ExtendDesugaring(IEnumerable<Cmd> before, IEnumerable<Cmd> after)
+ {
+ var desug = Desugaring;
+ var stCmd = desug as StateCmd;
+ if (stCmd != null)
+ {
+ stCmd.Cmds.InsertRange(0, before);
+ stCmd.Cmds.AddRange(after);
+ }
+ else if (desug != null)
+ {
+ var cmds = new List<Cmd>(before);
+ cmds.Add(desug);
+ cmds.AddRange(after);
+ desugaring = new StateCmd(Token.NoToken, new List<Variable>(), cmds);
+ }
+ }
+
public override void Emit(TokenTextWriter stream, int level) {
//Contract.Requires(stream != null);
if (CommandLineOptions.Clo.PrintDesugarings) {
@@ -2336,11 +2354,11 @@ namespace Microsoft.Boogie { #endregion
#region assume Post[ins, outs, old(frame) := cins, couts, cframe]
- Substitution s2 = Substituter.SubstitutionFromHashtable(substMap);
- Substitution s2old = Substituter.SubstitutionFromHashtable(substMapOld);
+ calleeSubstitution = Substituter.SubstitutionFromHashtable(substMap);
+ calleeSubstitutionOld = Substituter.SubstitutionFromHashtable(substMapOld);
foreach (Ensures/*!*/ e in this.Proc.Ensures) {
Contract.Assert(e != null);
- Expr copy = Substituter.ApplyReplacingOldExprs(s2, s2old, e.Condition);
+ Expr copy = Substituter.ApplyReplacingOldExprs(calleeSubstitution, calleeSubstitutionOld, e.Condition);
AssumeCmd assume = new AssumeCmd(this.tok, copy);
#region stratified inlining support
if (QKeyValue.FindBoolAttribute(e.Attributes, "si_fcall"))
@@ -2373,6 +2391,69 @@ namespace Microsoft.Boogie { return new StateCmd(this.tok, tempVars, newBlockBody);
}
+ class NameEqualityComparer : EqualityComparer<IdentifierExpr>
+ {
+ public override bool Equals(IdentifierExpr x, IdentifierExpr y)
+ {
+ return x.Name.Equals(y.Name);
+ }
+
+ public override int GetHashCode(IdentifierExpr obj)
+ {
+ return obj.Name.GetHashCode();
+ }
+ }
+
+ NameEqualityComparer comparer = new NameEqualityComparer();
+
+ Substitution calleeSubstitution;
+ Substitution calleeSubstitutionOld;
+
+ public IEnumerable<IdentifierExpr> UnmodifiedBefore(Procedure oldProcedure)
+ {
+ Contract.Requires(oldProcedure != null);
+
+ return Proc.Modifies.Except(oldProcedure.Modifies, comparer).Select(e => new IdentifierExpr(Token.NoToken, e.Decl));
+ }
+
+ public Expr Postcondition(Procedure procedure, Program program)
+ {
+ Contract.Requires(calleeSubstitution != null && calleeSubstitutionOld != null && program != null);
+
+ var ensures = procedure.Ensures.Select(e => Substituter.FunctionCallReresolvingApplyReplacingOldExprs(calleeSubstitution, calleeSubstitutionOld, e.Condition, program));
+ return Conjunction(ensures);
+ }
+
+ public Expr Precondition(Procedure procedure, Program program)
+ {
+ Contract.Requires(calleeSubstitution != null && calleeSubstitutionOld != null && program != null);
+
+ var requires = procedure.Requires.Select(r => Substituter.FunctionCallReresolvingApplyReplacingOldExprs(calleeSubstitution, calleeSubstitutionOld, r.Condition, program));
+ return Conjunction(requires);
+ }
+
+ private static Expr Conjunction(IEnumerable<Expr> conjuncts)
+ {
+ // TODO(wuestholz): Should we use 'LiteralExpr.BinaryTreeAnd' instead?
+ Expr result = null;
+ foreach (var c in conjuncts)
+ {
+ if (result != null)
+ {
+ result = LiteralExpr.And(result, c);
+ }
+ else
+ {
+ result = c;
+ }
+ }
+ if (result == null)
+ {
+ result = new LiteralExpr(Token.NoToken, true);
+ }
+ return result;
+ }
+
public override Absy StdDispatch(StandardVisitor visitor) {
//Contract.Requires(visitor != null);
Contract.Ensures(Contract.Result<Absy>() != null);
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 2a995fc2..4f9488a3 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -1314,7 +1314,7 @@ namespace Microsoft.Boogie { return true;
case "verifySnapshots":
- ps.GetNumericArgument(ref VerifySnapshots, 2);
+ ps.GetNumericArgument(ref VerifySnapshots, 3);
return true;
case "useSmtOutputFormat": {
@@ -1750,7 +1750,8 @@ namespace Microsoft.Boogie { verify several program snapshots (named <filename>.v0.bpl
to <filename>.vN.bpl) using verification result caching:
0 - do not use any verification result caching (default)
- 1 - use verification result caching
+ 1 - use the basic verification result caching
+ 2 - use the more advanced verification result caching
/verifySeparately
verify each input program separately
/removeEmptyBlocks:<c>
diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs index 70018a1a..86311d18 100644 --- a/Source/Core/Duplicator.cs +++ b/Source/Core/Duplicator.cs @@ -10,6 +10,7 @@ using System.Collections;
using System.Collections.Generic;
using System.Diagnostics.Contracts;
+using System.Linq;
namespace Microsoft.Boogie {
public class Duplicator : StandardVisitor {
@@ -476,6 +477,15 @@ namespace Microsoft.Boogie { return (Expr)new ReplacingOldSubstituter(always, forOld).Visit(expr);
}
+ public static Expr FunctionCallReresolvingApplyReplacingOldExprs(Substitution always, Substitution forOld, Expr expr, Program program)
+ {
+ Contract.Requires(always != null);
+ Contract.Requires(forOld != null);
+ Contract.Requires(expr != null);
+ Contract.Ensures(Contract.Result<Expr>() != null);
+ return (Expr)new FunctionCallReresolvingReplacingOldSubstituter(program, always, forOld).Visit(expr);
+ }
+
// ----------------------------- Substitutions for Cmd -------------------------------
/// <summary>
@@ -611,7 +621,34 @@ namespace Microsoft.Boogie { }
}
- private sealed class ReplacingOldSubstituter : Duplicator {
+ private sealed class FunctionCallReresolvingReplacingOldSubstituter : ReplacingOldSubstituter
+ {
+ readonly Program Program;
+
+ public FunctionCallReresolvingReplacingOldSubstituter(Program program, Substitution always, Substitution forold)
+ : base(always, forold)
+ {
+ Program = program;
+ }
+
+ public override Expr VisitNAryExpr(NAryExpr node)
+ {
+ var result = base.VisitNAryExpr(node);
+ var nAryExpr = result as NAryExpr;
+ if (nAryExpr != null)
+ {
+ var funCall = nAryExpr.Fun as FunctionCall;
+ if (funCall != null)
+ {
+ // TODO(wuestholz): Maybe we should speed up this lookup.
+ funCall.Func = Program.TopLevelDeclarations.OfType<Function>().FirstOrDefault(f => f.Name == funCall.FunctionName);
+ }
+ }
+ return result;
+ }
+ }
+
+ private class ReplacingOldSubstituter : Duplicator {
private readonly Substitution/*!*/ always;
private readonly Substitution/*!*/ forold;
[ContractInvariantMethod]
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 6a4dbc07..925b414b 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -317,9 +317,32 @@ namespace Microsoft.Boogie public class VerificationResult
{
+ public readonly string RequestId;
public readonly string Checksum;
public readonly string DependeciesChecksum;
- public readonly string RequestId;
+ public readonly string ImplementationName;
+ public readonly IToken ImplementationToken;
+
+ private readonly WeakReference program;
+ public Program Program
+ {
+ get
+ {
+ if (program == null)
+ {
+ return null;
+ }
+ try
+ {
+ var p = program.Target as Program;
+ return p;
+ }
+ catch (InvalidOperationException)
+ {
+ return null;
+ }
+ }
+ }
public DateTime Start { get; set; }
public DateTime End { get; set; }
@@ -328,24 +351,20 @@ namespace Microsoft.Boogie public int ProofObligationCountBefore { get; set; }
public int ProofObligationCountAfter { get; set; }
- public ConditionGeneration.Outcome Outcome;
+ public ConditionGeneration.Outcome Outcome { get; set; }
public List<Counterexample> Errors;
- public string ImplementationName { get; set; }
- public IToken ImplementationToken { get; set; }
-
- public VerificationResult(string requestId, string checksum, string depsChecksum, ConditionGeneration.Outcome outcome, List<Counterexample> errors)
- : this(requestId, checksum, depsChecksum)
- {
- Outcome = outcome;
- Errors = errors;
- }
-
- public VerificationResult(string requestId, string checksum, string depsChecksum)
+ public VerificationResult(string requestId, string checksum, string depsChecksum, string implementationName, IToken implementationToken, Program program = null)
{
Checksum = checksum;
DependeciesChecksum = depsChecksum;
RequestId = requestId;
+ ImplementationName = implementationName;
+ ImplementationToken = implementationToken;
+ if (program != null)
+ {
+ this.program = new WeakReference(program);
+ }
}
}
@@ -844,7 +863,7 @@ namespace Microsoft.Boogie Implementation[] stablePrioritizedImpls = null;
if (0 < CommandLineOptions.Clo.VerifySnapshots)
{
- impls.Iter(impl => { impl.DependenciesChecksum = DependencyCollector.DependenciesChecksum(impl); });
+ impls.Iter(impl => { DependencyCollector.DependenciesChecksum(impl); });
stablePrioritizedImpls = impls.OrderByDescending(
impl => impl.Priority != 1 ? impl.Priority : Cache.VerificationPriority(impl)).ToArray();
}
@@ -855,6 +874,11 @@ namespace Microsoft.Boogie #endregion
+ if (1 < CommandLineOptions.Clo.VerifySnapshots)
+ {
+ CachedVerificationResultInjector.Inject(program, stablePrioritizedImpls);
+ }
+
#region Verify each implementation
var outputCollector = new OutputCollector(stablePrioritizedImpls);
@@ -995,9 +1019,7 @@ namespace Microsoft.Boogie {
#region Verify the implementation
- verificationResult = new VerificationResult(requestId, impl.Checksum, impl.DependenciesChecksum);
- verificationResult.ImplementationName = impl.Name;
- verificationResult.ImplementationToken = impl.tok;
+ verificationResult = new VerificationResult(requestId, impl.Checksum, impl.DependenciesChecksum, impl.Name, impl.tok, 1 < CommandLineOptions.Clo.VerifySnapshots ? program : null);
using (var vcgen = CreateVCGen(program, checkers))
{
diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs index 044d84fe..a0dba9d2 100644 --- a/Source/ExecutionEngine/VerificationResultCache.cs +++ b/Source/ExecutionEngine/VerificationResultCache.cs @@ -10,40 +10,204 @@ using VC; namespace Microsoft.Boogie
{
+ class CachedVerificationResultInjector : StandardVisitor
+ {
+ readonly IEnumerable<Implementation> Implementations;
+ readonly Program Program;
+ Program programInCachedSnapshot;
+ Implementation currentImplementation;
+ int assumptionVariableCount;
+ int temporaryVariableCount;
+
+ int FreshAssumptionVariableName
+ {
+ get
+ {
+ return assumptionVariableCount++;
+ }
+ }
+
+ int FreshTemporaryVariableName
+ {
+ get
+ {
+ return temporaryVariableCount++;
+ }
+ }
+
+ protected CachedVerificationResultInjector(Program program, IEnumerable<Implementation> implementations)
+ {
+ Implementations = implementations;
+ Program = program;
+ }
+
+ public Implementation Inject(Implementation implementation, Program programInCachedSnapshot)
+ {
+ Contract.Requires(implementation != null && programInCachedSnapshot != null);
+
+ this.programInCachedSnapshot = programInCachedSnapshot;
+ assumptionVariableCount = 0;
+ temporaryVariableCount = 0;
+ currentImplementation = implementation;
+ var result = VisitImplementation(implementation);
+ currentImplementation = null;
+ this.programInCachedSnapshot = null;
+ return result;
+ }
+
+ public static void Inject(Program program, IEnumerable<Implementation> implementations)
+ {
+ var eai = new CachedVerificationResultInjector(program, implementations);
+
+ foreach (var impl in implementations)
+ {
+ if (ExecutionEngine.Cache.VerificationPriority(impl) == Priority.LOW)
+ {
+ var vr = ExecutionEngine.Cache.Lookup(impl.Id);
+ // TODO(wuestholz): We should probably increase the threshold to something like 2 seconds.
+ if (vr != null && 0.0 < vr.End.Subtract(vr.Start).TotalMilliseconds)
+ {
+ if (vr.Errors != null)
+ {
+ impl.ErrorsInCachedSnapshot = vr.Errors.ToList<object>();
+ }
+ else if (vr.Outcome == ConditionGeneration.Outcome.Correct)
+ {
+ impl.ErrorsInCachedSnapshot = new List<object>();
+ }
+ var p = vr.Program;
+ if (p != null)
+ {
+ eai.Inject(impl, p);
+ }
+ }
+ }
+ }
+ }
+
+ public override Cmd VisitCallCmd(CallCmd node)
+ {
+ var result = base.VisitCallCmd(node);
+
+ // TODO(wuestholz): Maybe we should speed up this lookup.
+ var oldProc = programInCachedSnapshot.TopLevelDeclarations.OfType<Procedure>().FirstOrDefault(p => p.Name == node.Proc.Name);
+ if (oldProc != null
+ && DependencyCollector.DependenciesChecksum(oldProc) != DependencyCollector.DependenciesChecksum(node.Proc)
+ && DependencyCollector.AllFunctionDependenciesAreDefinedAndUnchanged(oldProc, Program))
+ {
+ var lv = new LocalVariable(Token.NoToken,
+ new TypedIdent(Token.NoToken, string.Format("a##post##{0}", FreshAssumptionVariableName), Type.Bool),
+ new QKeyValue(Token.NoToken, "assumption", new List<object>(), null));
+ currentImplementation.InjectAssumptionVariable(lv);
+
+ var before = new List<Cmd>();
+ if (currentImplementation.NoErrorsInCachedSnapshot
+ && oldProc.Requires.Any())
+ {
+ var pre = node.Precondition(oldProc, Program);
+ var assume = new AssumeCmd(Token.NoToken, pre, new QKeyValue(Token.NoToken, "precondition_previous_snapshot", new List<object>(), null));
+ before.Add(assume);
+ }
+ else if (currentImplementation.AnyErrorsInCachedSnapshot)
+ {
+ // TODO(wuestholz): Add an assume statement if the precondition was verified in the previous snapshot.
+ }
+
+ var post = node.Postcondition(oldProc, Program);
+ var mods = node.UnmodifiedBefore(oldProc);
+ foreach (var m in mods)
+ {
+ var mPre = new LocalVariable(Token.NoToken,
+ new TypedIdent(Token.NoToken, string.Format("{0}##pre##{1}", m.Name, FreshTemporaryVariableName), m.Type));
+ before.Add(new AssignCmd(Token.NoToken,
+ new List<AssignLhs> { new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, mPre)) },
+ new List<Expr> { new IdentifierExpr(Token.NoToken, m.Decl) }));
+ var eq = LiteralExpr.Eq(new IdentifierExpr(Token.NoToken, mPre), new IdentifierExpr(Token.NoToken, m.Decl));
+ post = LiteralExpr.And(post, eq);
+ }
+ var lhs = new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, lv));
+ var rhs = LiteralExpr.And(new IdentifierExpr(Token.NoToken, lv), post);
+ var assumed = new AssignCmd(Token.NoToken, new List<AssignLhs> { lhs }, new List<Expr> { rhs });
+
+ node.ExtendDesugaring(before, new List<Cmd> { assumed });
+ }
+
+ return result;
+ }
+ }
+
+
class DependencyCollector : ReadOnlyVisitor
{
- private HashSet<DeclWithFormals> dependencies;
+ private HashSet<Procedure> procedureDependencies;
+ private HashSet<Function> functionDependencies;
+ private bool allDependenciesHaveChecksum = true;
public DependencyCollector()
{
- dependencies = new HashSet<DeclWithFormals>();
+ procedureDependencies = new HashSet<Procedure>();
+ functionDependencies = new HashSet<Function>();
}
- public static void Collect(Absy node, out List<DeclWithFormals> dependencies)
+ static bool Collect(Absy node, out ISet<Procedure> procedureDependencies, out ISet<Function> functionDependencies)
{
var dc = new DependencyCollector();
dc.Visit(node);
- dependencies = dc.dependencies.ToList();
+ procedureDependencies = dc.procedureDependencies;
+ functionDependencies = dc.functionDependencies;
+ return dc.allDependenciesHaveChecksum;
+ }
+
+ static bool Collect(Procedure proc, out ISet<Function> functionDependencies)
+ {
+ var dc = new DependencyCollector();
+ dc.Visit(proc);
+ functionDependencies = dc.functionDependencies;
+ return dc.allDependenciesHaveChecksum;
+ }
+
+ public static bool AllFunctionDependenciesAreDefinedAndUnchanged(Procedure oldProc, Program newProg)
+ {
+ Contract.Requires(oldProc != null && newProg != null);
+
+ ISet<Function> oldDeps;
+ if (!Collect(oldProc, out oldDeps))
+ {
+ return false;
+ }
+ // TODO(wuestholz): Maybe we should speed up this lookup.
+ var funcs = newProg.TopLevelDeclarations.OfType<Function>();
+ return oldDeps.All(dep => funcs.Any(f => f.Name == dep.Name && f.Checksum == dep.Checksum));
}
- public static string DependenciesChecksum(Implementation impl)
+ public static string DependenciesChecksum(DeclWithFormals decl)
{
- List<DeclWithFormals> deps;
- DependencyCollector.Collect(impl, out deps);
- if (deps.Any(dep => dep.Checksum == null))
+ if (decl.DependenciesChecksum != null)
+ {
+ return decl.DependenciesChecksum;
+ }
+
+ ISet<Procedure> procDeps;
+ ISet<Function> funcDeps;
+ if (!DependencyCollector.Collect(decl, out procDeps, out funcDeps))
{
return null;
}
var md5 = System.Security.Cryptography.MD5.Create();
- var data = Encoding.UTF8.GetBytes(deps.MapConcat(dep => dep.Checksum, ""));
+ var procChecksums = procDeps.MapConcat(dep => dep.Checksum, "");
+ var funcChecksums = funcDeps.MapConcat(dep => dep.Checksum, "");
+ var data = Encoding.UTF8.GetBytes(procChecksums + funcChecksums);
var hashedData = md5.ComputeHash(data);
- return BitConverter.ToString(hashedData);
+ var result = BitConverter.ToString(hashedData);
+ decl.DependenciesChecksum = result;
+ return result;
}
public override Procedure VisitProcedure(Procedure node)
{
- dependencies.Add(node);
+ procedureDependencies.Add(node);
+ allDependenciesHaveChecksum &= node.Checksum != null;
foreach (var param in node.InParams)
{
@@ -58,7 +222,8 @@ namespace Microsoft.Boogie public override Function VisitFunction(Function node)
{
- dependencies.Add(node);
+ functionDependencies.Add(node);
+ allDependenciesHaveChecksum &= node.Checksum != null;
if (node.DefinitionAxiom != null)
{
@@ -70,7 +235,7 @@ namespace Microsoft.Boogie public override Cmd VisitCallCmd(CallCmd node)
{
- var visited = dependencies.Contains(node.Proc);
+ var visited = procedureDependencies.Contains(node.Proc);
if (!visited)
{
VisitProcedure(node.Proc);
@@ -84,7 +249,7 @@ namespace Microsoft.Boogie var funCall = node.Fun as FunctionCall;
if (funCall != null)
{
- var visited = dependencies.Contains(funCall.Func);
+ var visited = functionDependencies.Contains(funCall.Func);
if (!visited)
{
VisitFunction(funCall.Func);
@@ -96,6 +261,15 @@ namespace Microsoft.Boogie }
+ static internal class Priority
+ {
+ public static int LOW = 1;
+ public static int MEDIUM = 2;
+ public static int HIGH = 3;
+ public static int SKIP = int.MaxValue;
+ }
+
+
public class VerificationResultCache
{
private readonly ConcurrentDictionary<string, VerificationResult> Cache = new ConcurrentDictionary<string, VerificationResult>();
@@ -152,7 +326,7 @@ namespace Microsoft.Boogie public bool NeedsToBeVerified(Implementation impl)
{
- return VerificationPriority(impl) < int.MaxValue;
+ return VerificationPriority(impl) < Priority.SKIP;
}
@@ -160,19 +334,19 @@ namespace Microsoft.Boogie {
if (!Cache.ContainsKey(impl.Id))
{
- return 3; // high priority (has been never verified before)
+ return Priority.HIGH; // high priority (has been never verified before)
}
else if (Cache[impl.Id].Checksum != impl.Checksum)
{
- return 2; // medium priority (old snapshot has been verified before)
+ return Priority.MEDIUM; // medium priority (old snapshot has been verified before)
}
else if (impl.DependenciesChecksum == null || Cache[impl.Id].DependeciesChecksum != impl.DependenciesChecksum)
{
- return 1; // low priority (the same snapshot has been verified before, but a callee has changed)
+ return Priority.LOW; // low priority (the same snapshot has been verified before, but a callee has changed)
}
else
{
- return int.MaxValue; // skip verification (highest priority to get them done as soon as possible)
+ return Priority.SKIP; // skip verification (highest priority to get them done as soon as possible)
}
}
}
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 8fe4a5c6..afd2d3e6 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -576,6 +576,8 @@ namespace VC { private bool _disposed;
+ protected Implementation currentImplementation;
+
protected List<Variable> CurrentLocalVariables = null;
// shared across each implementation; created anew for each implementation
@@ -1309,7 +1311,9 @@ namespace VC { Contract.Requires(impl != null);
Contract.Requires(mvInfo != null);
+ currentImplementation = impl;
Dictionary<Variable, Expr> r = ConvertBlocks2PassiveCmd(impl.Blocks, impl.Proc.Modifies, mvInfo);
+ currentImplementation = null;
RestoreParamWhereClauses(impl);
@@ -1448,6 +1452,28 @@ namespace VC { ((AssertCmd)pc).OrigExpr = pc.Expr;
Contract.Assert(((AssertCmd)pc).IncarnationMap == null);
((AssertCmd)pc).IncarnationMap = (Dictionary<Variable, Expr>)cce.NonNull(new Dictionary<Variable, Expr>(incarnationMap));
+
+ if (currentImplementation != null
+ && currentImplementation.NoErrorsInCachedSnapshot
+ && currentImplementation.InjectedAssumptionVariables != null
+ && 2 <= currentImplementation.InjectedAssumptionVariables.Count)
+ {
+ // TODO(wuestholz): Maybe store the assertion expression in a local variable.
+ var expr = LiteralExpr.Imp(currentImplementation.ConjunctionOfInjectedAssumptionVariables(), copy);
+ passiveCmds.Add(new AssumeCmd(Token.NoToken, expr));
+ }
+ else if (currentImplementation != null
+ && currentImplementation.AnyErrorsInCachedSnapshot)
+ {
+ // TODO(wuestholz): Add an assume statement if the assertion was verified in the previous snapshot.
+ }
+ }
+ else if (pc is AssumeCmd
+ && QKeyValue.FindStringAttribute(pc.Attributes, "precondition_previous_snapshot") != null
+ && currentImplementation.InjectedAssumptionVariables != null
+ && currentImplementation.InjectedAssumptionVariables.Any())
+ {
+ copy = LiteralExpr.Imp(currentImplementation.ConjunctionOfInjectedAssumptionVariables(), copy);
}
pc.Expr = copy;
passiveCmds.Add(pc);
@@ -1521,6 +1547,19 @@ namespace VC { }
passiveCmds.Add(new AssumeCmd(c.tok, assumption));
}
+
+ if (currentImplementation != null
+ && currentImplementation.NoErrorsInCachedSnapshot
+ && currentImplementation.InjectedAssumptionVariables != null
+ && currentImplementation.InjectedAssumptionVariables.Count == 1
+ && assign.Lhss.Count == 1)
+ {
+ var identExpr = assign.Lhss[0].AsExpr as IdentifierExpr;
+ if (identExpr != null && identExpr.Decl != null && QKeyValue.FindBoolAttribute(identExpr.Decl.Attributes, "assumption"))
+ {
+ passiveCmds.Add(new AssumeCmd(c.tok, new IdentifierExpr(Token.NoToken, currentImplementation.InjectedAssumptionVariables.First())));
+ }
+ }
}
#endregion
#region havoc w |--> assume whereClauses, out := in( w |-> w' )
|