From c8b3dace6ff23f5554423b41c03d87e024ed1147 Mon Sep 17 00:00:00 2001 From: wuestholz Date: Tue, 25 Nov 2014 10:52:54 +0100 Subject: Worked on the verification result caching (extracted functions). --- Source/ExecutionEngine/VerificationResultCache.cs | 90 ++++++++++++++++++++++- 1 file changed, 87 insertions(+), 3 deletions(-) (limited to 'Source/ExecutionEngine') diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs index d8a446a7..86a614e9 100644 --- a/Source/ExecutionEngine/VerificationResultCache.cs +++ b/Source/ExecutionEngine/VerificationResultCache.cs @@ -188,6 +188,7 @@ namespace Microsoft.Boogie var before = new List(); var beforePrecondtionCheck = new List(); var after = new List(); + var axioms = new List(); Expr assumedExpr = new LiteralExpr(Token.NoToken, false); // TODO(wuestholz): Try out two alternatives: only do this for low priority implementations or not at all. var canUseSpecs = DependencyCollector.CanExpressOldSpecs(oldProc, Program); @@ -198,7 +199,7 @@ namespace Microsoft.Boogie var precond = node.CheckedPrecondition(oldProc, Program); if (precond != null) { - var assume = new AssumeCmd(node.tok, precond, new QKeyValue(Token.NoToken, "precondition_previous_snapshot", new List(), null)); + var assume = new AssumeCmd(node.tok, FunctionExtractor.Extract(precond, Program, axioms), new QKeyValue(Token.NoToken, "precondition_previous_snapshot", new List(), null)); beforePrecondtionCheck.Add(assume); } @@ -211,7 +212,10 @@ namespace Microsoft.Boogie var lhs = new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, oldUnmod)); var rhs = new IdentifierExpr(Token.NoToken, unmod.Decl); before.Add(new AssignCmd(Token.NoToken, new List { lhs }, new List { rhs })); - eqs.Add(LiteralExpr.Eq(new IdentifierExpr(Token.NoToken, oldUnmod), new IdentifierExpr(Token.NoToken, unmod.Decl))); + var eq = LiteralExpr.Eq(new IdentifierExpr(Token.NoToken, oldUnmod), new IdentifierExpr(Token.NoToken, unmod.Decl)); + eq.Type = Type.Bool; + eq.TypeParameters = SimpleTypeParamInstantiation.EMPTY; + eqs.Add(eq); } var mods = node.ModifiedBefore(oldProc); @@ -237,7 +241,8 @@ namespace Microsoft.Boogie node.AssignedAssumptionVariable = lv; currentImplementation.InjectAssumptionVariable(lv, !canUseSpecs); var lhs = new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, lv)); - var rhs = LiteralExpr.And(new IdentifierExpr(Token.NoToken, lv), assumedExpr); + // TODO(wuestholz): Try to extract functions for each clause. + var rhs = LiteralExpr.And(new IdentifierExpr(Token.NoToken, lv), FunctionExtractor.Extract(assumedExpr, Program, axioms)); var assumed = new AssignCmd(node.tok, new List { lhs }, new List { rhs }); after.Add(assumed); } @@ -249,6 +254,12 @@ namespace Microsoft.Boogie { var loc = node.tok != null && node.tok != Token.NoToken ? string.Format("{0}({1},{2})", node.tok.filename, node.tok.line, node.tok.col) : ""; Console.Out.WriteLine("Processing call to procedure {0} in implementation {1} (at {2}):", node.Proc.Name, currentImplementation.Name, loc); + foreach (var a in axioms) + { + Console.Out.Write(" >>> added axiom: "); + a.Expr.Emit(tokTxtWr); + Console.Out.WriteLine(); + } foreach (var b in before) { Console.Out.Write(" >>> added before: "); @@ -273,6 +284,79 @@ namespace Microsoft.Boogie } + sealed class FunctionExtractor : StandardVisitor + { + readonly Dictionary Substitutions = new Dictionary(); + + public override Expr VisitIdentifierExpr(IdentifierExpr node) + { + if (node.Decl == null || !(node.Decl is LocalVariable || node.Decl is Formal)) + { + return node; + } + else + { + BoundVariable boundVar; + if (!Substitutions.TryGetValue(node.Decl, out boundVar)) + { + boundVar = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, node.Name, node.Type)); + Substitutions[node.Decl] = boundVar; + } + return new IdentifierExpr(node.tok, boundVar); + } + } + + public static Expr Extract(Expr expr, Program program, List axioms) + { + Contract.Requires(expr != null && program != null && !program.TopLevelDeclarationsAreFrozen && axioms != null); + + if (expr is LiteralExpr) + { + return expr; + } + + var extractor = new FunctionExtractor(); + + var body = extractor.VisitExpr(expr); + + var name = program.FreshExtractedFunctionName(); + var originalVars = extractor.Substitutions.Keys.ToList(); + var formalInArgs = originalVars.Select(v => new Formal(Token.NoToken, new TypedIdent(Token.NoToken, extractor.Substitutions[v].Name, extractor.Substitutions[v].TypedIdent.Type), true)).ToList(); + var formalOutArg = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, name + "$result$", expr.Type), false); + var func = new Function(Token.NoToken, name, formalInArgs, formalOutArg); + func.AddAttribute("never_pattern"); + + var boundVars = originalVars.Select(k => extractor.Substitutions[k]); + var axiomCall = new NAryExpr(Token.NoToken, new FunctionCall(func), boundVars.Select(b => new IdentifierExpr(Token.NoToken, b)).ToList()); + axiomCall.Type = expr.Type; + axiomCall.TypeParameters = SimpleTypeParamInstantiation.EMPTY; + var eq = LiteralExpr.Eq(axiomCall, body); + eq.Type = body.Type; + eq.TypeParameters = SimpleTypeParamInstantiation.EMPTY; + if (0 < formalInArgs.Count) + { + body = new ForallExpr(Token.NoToken, boundVars.ToList(), new Trigger(Token.NoToken, true, new List { axiomCall }), eq); + body.Type = Type.Bool; + } + else + { + body = eq; + } + + var axiom = new Axiom(Token.NoToken, body); + func.DefinitionAxiom = axiom; + program.AddTopLevelDeclaration(func); + program.AddTopLevelDeclaration(axiom); + axioms.Add(axiom); + + var call = new NAryExpr(Token.NoToken, new FunctionCall(func), originalVars.Select(v => new IdentifierExpr(Token.NoToken, v)).ToList()); + call.Type = expr.Type; + call.TypeParameters = SimpleTypeParamInstantiation.EMPTY; + return call; + } + } + + sealed class OtherDefinitionAxiomsCollector : ReadOnlyVisitor { Axiom currentAxiom; -- cgit v1.2.3