From a3325de0835308c293e999b574a804366f37d936 Mon Sep 17 00:00:00 2001 From: wuestholz Date: Fri, 16 Jan 2015 12:21:49 +0100 Subject: Worked on the verification result caching (use native support for partially verified assertions). --- Source/VCGeneration/ConditionGeneration.cs | 92 +++--------------------------- Source/VCGeneration/Wlp.cs | 51 ++++++----------- 2 files changed, 25 insertions(+), 118 deletions(-) (limited to 'Source/VCGeneration') diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 454a2f30..bc535404 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -608,19 +608,6 @@ namespace VC { protected Implementation currentImplementation; - private LocalVariable currentTemporaryVariableForAssertions; - protected LocalVariable CurrentTemporaryVariableForAssertions - { - get - { - if (currentTemporaryVariableForAssertions == null) - { - currentTemporaryVariableForAssertions = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "##assertion", Microsoft.Boogie.Type.Bool)); - } - return currentTemporaryVariableForAssertions; - } - } - protected List CurrentLocalVariables = null; // shared across each implementation; created anew for each implementation @@ -1334,7 +1321,6 @@ namespace VC { Contract.Requires(mvInfo != null); currentImplementation = impl; - currentTemporaryVariableForAssertions = null; var start = DateTime.UtcNow; @@ -1361,7 +1347,6 @@ namespace VC { } } - currentTemporaryVariableForAssertions = null; currentImplementation = null; RestoreParamWhereClauses(impl); @@ -1552,7 +1537,6 @@ namespace VC { ac.IncarnationMap = (Dictionary)cce.NonNull(new Dictionary(incarnationMap)); var subsumption = Wlp.Subsumption(ac); - var alwaysUseSubsumption = subsumption == CommandLineOptions.SubsumptionOption.Always; if (relevantDoomedAssumpVars.Any()) { TraceCachingAction(pc, CachingAction.DoNothingToAssert); @@ -1573,59 +1557,15 @@ namespace VC { { bool isTrue; var assmVars = currentImplementation.ConjunctionOfInjectedAssumptionVariables(incarnationMap, out isTrue); - if (!isTrue && alwaysUseSubsumption) + TraceCachingAction(pc, !isTrue ? CachingAction.MarkAsPartiallyVerified : CachingAction.MarkAsFullyVerified); + var litExpr = ac.Expr as LiteralExpr; + if (litExpr == null || !litExpr.IsTrue) { - TraceCachingAction(pc, CachingAction.MarkAsPartiallyVerified); - var litExpr = ac.Expr as LiteralExpr; - if (litExpr == null || !litExpr.IsTrue) - { - // Bind the assertion expression to a local variable. - var incarnation = CreateIncarnation(CurrentTemporaryVariableForAssertions, containingBlock); - var identExpr = new IdentifierExpr(Token.NoToken, incarnation); - incarnationMap[incarnation] = identExpr; - ac.IncarnationMap[incarnation] = identExpr; - passiveCmds.Add(new AssumeCmd(Token.NoToken, LiteralExpr.Eq(identExpr, copy))); - copy = identExpr; - passiveCmds.Add(new AssumeCmd(Token.NoToken, LiteralExpr.Imp(assmVars, identExpr))); - - // TODO(wuestholz): Try to use this instead: - // ac.MarkAsVerifiedUnder(assmVars); - } - else - { - dropCmd = true; - } - } - else if (isTrue) - { - if (alwaysUseSubsumption) - { - TraceCachingAction(pc, CachingAction.MarkAsFullyVerified); - var litExpr = ac.Expr as LiteralExpr; - if (litExpr == null || !litExpr.IsTrue) - { - // Turn it into an assume statement. - pc = new AssumeCmd(ac.tok, copy); - pc.Attributes = new QKeyValue(Token.NoToken, "verified_assertion", new List(), pc.Attributes); - } - else - { - dropCmd = true; - } - } - else if (subsumption == CommandLineOptions.SubsumptionOption.Never) - { - TraceCachingAction(pc, CachingAction.MarkAsFullyVerified); - dropCmd = true; - } - else - { - TraceCachingAction(pc, CachingAction.DoNothingToAssert); - } + ac.MarkAsVerifiedUnder(assmVars); } else { - TraceCachingAction(pc, CachingAction.DoNothingToAssert); + dropCmd = true; } } } @@ -1636,24 +1576,10 @@ namespace VC { && currentImplementation.IsAssertionChecksumInCachedSnapshot(checksum) && currentImplementation.IsErrorChecksumInCachedSnapshot(checksum)) { - if (alwaysUseSubsumption) - { - // Turn it into an assume statement. - TraceCachingAction(pc, CachingAction.RecycleError); - pc = new AssumeCmd(ac.tok, copy); - pc.Attributes = new QKeyValue(Token.NoToken, "recycled_failing_assertion", new List(), pc.Attributes); - currentImplementation.AddRecycledFailingAssertion(ac); - } - else if (subsumption == CommandLineOptions.SubsumptionOption.Never) - { - TraceCachingAction(pc, CachingAction.RecycleError); - dropCmd = true; - currentImplementation.AddRecycledFailingAssertion(ac); - } - else - { - TraceCachingAction(pc, CachingAction.DoNothingToAssert); - } + TraceCachingAction(pc, CachingAction.RecycleError); + ac.MarkAsVerifiedUnder(Expr.True); + currentImplementation.AddRecycledFailingAssertion(ac); + pc.Attributes = new QKeyValue(Token.NoToken, "recycled_failing_assertion", new List(), pc.Attributes); } else { diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index 6f6326d1..cd735501 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -106,17 +106,12 @@ namespace VC { AssertCmd ac = (AssertCmd)cmd; ctxt.Ctxt.BoogieExprTranslator.isPositiveContext = !ctxt.Ctxt.BoogieExprTranslator.isPositiveContext; VCExpr C = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr); - ctxt.Ctxt.BoogieExprTranslator.isPositiveContext = !ctxt.Ctxt.BoogieExprTranslator.isPositiveContext; - - VCExprLetBinding LB = null; VCExpr VU = null; if (ac.VerifiedUnder != null) { - var V = gen.Variable(ctxt.FreshLetBindingName(), Microsoft.Boogie.Type.Bool); - LB = gen.LetBinding(V, C); - C = V; VU = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.VerifiedUnder); } + ctxt.Ctxt.BoogieExprTranslator.isPositiveContext = !ctxt.Ctxt.BoogieExprTranslator.isPositiveContext; VCExpr R = null; if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) { @@ -127,28 +122,24 @@ namespace VC { ctxt.Label2absy[id] = ac; } - switch (Subsumption(ac)) { - case CommandLineOptions.SubsumptionOption.Never: - break; - case CommandLineOptions.SubsumptionOption.Always: - N = gen.Implies(C, N); - break; - case CommandLineOptions.SubsumptionOption.NotForQuantifiers: - if (!(C is VCExprQuantifier)) { - N = gen.Implies(C, N); - } - break; - default: - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected case + var subsumption = Subsumption(ac); + if (subsumption == CommandLineOptions.SubsumptionOption.Always + || (subsumption == CommandLineOptions.SubsumptionOption.NotForQuantifiers && !(C is VCExprQuantifier))) + { + N = gen.ImpliesSimp(C, N); } - ctxt.AssertionCount++; + if (VU != null) + { + var litExpr = ac.VerifiedUnder as LiteralExpr; + if (litExpr != null && litExpr.IsTrue) + { + return N; + } + C = gen.OrSimp(VU, C); + } - // TODO(wuestholz): Try to weaken the assertion instead of assuming the property that has already been verified: - // if (VU != null) - // { - // C = gen.OrSimp(VU, C); - // } + ctxt.AssertionCount++; if (ctxt.ControlFlowVariableExpr == null) { Contract.Assert(ctxt.Label2absy != null); @@ -164,16 +155,6 @@ namespace VC { } } } - - if (VU != null) - { - R = gen.ImpliesSimp(gen.ImpliesSimp(VU, C), R); - } - - if (LB != null) - { - R = gen.Let(R, LB); - } return R; } else if (cmd is AssumeCmd) { AssumeCmd ac = (AssumeCmd)cmd; -- cgit v1.2.3