From 6d5ddf853694b2b8014585dd1e40cc10efbaddea Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Sun, 17 May 2015 13:06:58 +0200 Subject: Make caching of verification results more fine-grained for changes that affect preconditions. --- Source/Core/Absy.cs | 24 ++++++++++++++++++++++++ Source/Core/AbsyCmd.cs | 33 ++++++++++----------------------- Source/Core/AbsyExpr.cs | 23 +++++++++++++++++++++++ Source/Core/DeadVarElim.cs | 2 +- Source/Core/Duplicator.cs | 37 ++++++++++++++++++++++++++++++++++++- 5 files changed, 94 insertions(+), 25 deletions(-) (limited to 'Source/Core') diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index a1a54024..56bfc90f 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -2427,6 +2427,28 @@ namespace Microsoft.Boogie { functionDependencies.Add(function); } + public bool SignatureEquals(DeclWithFormals other) + { + Contract.Requires(other != null); + + string sig = null; + string otherSig = null; + using (var strWr = new System.IO.StringWriter()) + using (var tokTxtWr = new TokenTextWriter("", strWr, false, false)) + { + EmitSignature(tokTxtWr, this is Function); + sig = strWr.ToString(); + } + + using (var otherStrWr = new System.IO.StringWriter()) + using (var otherTokTxtWr = new TokenTextWriter("", otherStrWr, false, false)) + { + EmitSignature(otherTokTxtWr, other is Function); + otherSig = otherStrWr.ToString(); + } + return sig == otherSig; + } + protected void EmitSignature(TokenTextWriter stream, bool shortRet) { Contract.Requires(stream != null); Type.EmitOptionalTypeParams(stream, TypeParameters); @@ -3295,6 +3317,8 @@ namespace Microsoft.Boogie { RecycledFailingAssertions.Add(assertion); } + public Cmd ExplicitAssumptionAboutCachedPrecondition { get; set; } + // Strongly connected components private StronglyConnectedComponents scc; [ContractInvariantMethod] diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index 137e2363..eb8b8e1e 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -1144,6 +1144,12 @@ namespace Microsoft.Boogie { return; } + if (cmd.IrrelevantForChecksumComputation) + { + cmd.Checksum = currentChecksum; + return; + } + var assumeCmd = cmd as AssumeCmd; if (assumeCmd != null && QKeyValue.FindBoolAttribute(assumeCmd.Attributes, "assumption_variable_initialization")) @@ -1161,7 +1167,7 @@ namespace Microsoft.Boogie { if (havocCmd != null) { tokTxtWr.Write("havoc "); - var relevantVars = havocCmd.Vars.Where(e => usedVariables.Contains(e.Decl) && !e.Decl.Name.StartsWith("a##post##")).OrderBy(e => e.Name).ToList(); + var relevantVars = havocCmd.Vars.Where(e => usedVariables.Contains(e.Decl) && !e.Decl.Name.StartsWith("a##cached##")).OrderBy(e => e.Name).ToList(); relevantVars.Emit(tokTxtWr, true); tokTxtWr.WriteLine(";"); } @@ -1244,6 +1250,7 @@ namespace Microsoft.Boogie { public abstract class Cmd : Absy { public byte[] Checksum { get; internal set; } public byte[] SugaredCmdChecksum { get; internal set; } + public bool IrrelevantForChecksumComputation { get; set; } public Cmd(IToken/*!*/ tok) : base(tok) { @@ -2849,7 +2856,7 @@ namespace Microsoft.Boogie { var clauses = procedure.Ensures.Select(e => Substituter.FunctionCallReresolvingApplyReplacingOldExprs(calleeSubstitution, substOldCombined, e.Condition, program)).Concat(modifies); // TODO(wuestholz): Try extracting a function for each clause: // return Conjunction(clauses.Select(c => extract(c))); - var conj = Conjunction(clauses); + var conj = Expr.And(clauses, true); return conj != null ? extract(conj) : conj; } @@ -2860,30 +2867,10 @@ namespace Microsoft.Boogie { var clauses = procedure.Requires.Where(r => !r.Free).Select(r => Substituter.FunctionCallReresolvingApplyReplacingOldExprs(calleeSubstitution, calleeSubstitutionOld, r.Condition, program)); // TODO(wuestholz): Try extracting a function for each clause: // return Conjunction(clauses.Select(c => extract(c))); - var conj = Conjunction(clauses); + var conj = Expr.And(clauses, true); return conj != null ? extract(conj) : conj; } - private static Expr Conjunction(IEnumerable conjuncts) - { - // TODO(wuestholz): Maybe we should use 'LiteralExpr.BinaryTreeAnd' instead. - Expr result = null; - foreach (var c in conjuncts) - { - if (result != null) - { - result = LiteralExpr.And(result, c); - result.Type = Type.Bool; - } - else - { - result = c; - result.Type = Type.Bool; - } - } - return result; - } - public override Absy StdDispatch(StandardVisitor visitor) { //Contract.Requires(visitor != null); Contract.Ensures(Contract.Result() != null); diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index f3a943b8..c19140d7 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -467,6 +467,29 @@ namespace Microsoft.Boogie { var mid = (start + end) / 2; return Expr.And(BinaryTreeAnd(terms, start, mid), BinaryTreeAnd(terms, mid + 1, end)); } + + public static Expr And(IEnumerable conjuncts, bool returnNullIfEmpty = false) + { + Expr result = null; + foreach (var c in conjuncts) + { + if (result != null) + { + result = LiteralExpr.And(result, c); + result.Type = Type.Bool; + } + else + { + result = c; + result.Type = Type.Bool; + } + } + if (result == null && !returnNullIfEmpty) + { + result = Expr.True; + } + return result; + } } [ContractClassFor(typeof(Expr))] public abstract class ExprContracts : Expr { diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs index 77086f0f..0feb5e35 100644 --- a/Source/Core/DeadVarElim.cs +++ b/Source/Core/DeadVarElim.cs @@ -539,7 +539,7 @@ namespace Microsoft.Boogie { HavocCmd/*!*/ havocCmd = (HavocCmd)cmd; foreach (IdentifierExpr/*!*/ expr in havocCmd.Vars) { Contract.Assert(expr != null); - if (expr.Decl != null && !(QKeyValue.FindBoolAttribute(expr.Decl.Attributes, "assumption") && expr.Decl.Name.StartsWith("a##post##"))) { + if (expr.Decl != null && !(QKeyValue.FindBoolAttribute(expr.Decl.Attributes, "assumption") && expr.Decl.Name.StartsWith("a##cached##"))) { liveSet.Remove(expr.Decl); } } diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs index 181b80a1..7f021c43 100644 --- a/Source/Core/Duplicator.cs +++ b/Source/Core/Duplicator.cs @@ -583,6 +583,15 @@ namespace Microsoft.Boogie { return (Expr)new FunctionCallReresolvingReplacingOldSubstituter(program, always, forOld).Visit(expr); } + public static Expr FunctionCallReresolvingApply(Substitution always, Substitution forOld, Expr expr, Program program) + { + Contract.Requires(always != null); + Contract.Requires(forOld != null); + Contract.Requires(expr != null); + Contract.Ensures(Contract.Result() != null); + return (Expr)new FunctionCallReresolvingNormalSubstituter(program, always, forOld).Visit(expr); + } + // ----------------------------- Substitutions for Cmd ------------------------------- /// @@ -660,7 +669,7 @@ namespace Microsoft.Boogie { // ------------------------------------------------------------ - private sealed class NormalSubstituter : Duplicator + private class NormalSubstituter : Duplicator { private readonly Substitution/*!*/ always; private readonly Substitution/*!*/ forold; @@ -744,6 +753,32 @@ namespace Microsoft.Boogie { } } + private sealed class FunctionCallReresolvingNormalSubstituter : NormalSubstituter + { + readonly Program Program; + + public FunctionCallReresolvingNormalSubstituter(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) + { + funCall.Func = Program.FindFunction(funCall.FunctionName); + } + } + return result; + } + } + private class ReplacingOldSubstituter : Duplicator { private readonly Substitution/*!*/ always; private readonly Substitution/*!*/ forold; -- cgit v1.2.3