From ad063dfd62db2b7f147e4f8abbcd7b8a7f575dae Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 26 Feb 2016 13:45:53 -0800 Subject: Changes to CanCall assumptions: - various peephole optimizations of formulas, to generate fewer tautologies - removed unused bound variables in CanCall quantifications (this addresses Issue #135) - added type- and precondition-antecedent in quantified CanCall assumption for lambda expressions, thus fixing an unsoundness --- Source/Dafny/Translator.cs | 164 ++++++++++++++++++++++++++++++++------------- 1 file changed, 117 insertions(+), 47 deletions(-) diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 52f52abf..e164d8ee 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -4293,12 +4293,7 @@ namespace Microsoft.Dafny { return CanCallAssumption(l, etran); } else if (expr is MemberSelectExpr) { MemberSelectExpr e = (MemberSelectExpr)expr; - Bpl.Expr r; - if (e.Obj is ThisExpr) { - r = Bpl.Expr.True; - } else { - r = CanCallAssumption(e.Obj, etran); - } + var r = CanCallAssumption(e.Obj, etran); if (e.Member is DatatypeDestructor) { var dtor = (DatatypeDestructor)e.Member; if (dtor.EnclosingCtor.EnclosingDatatype.Ctors.Count == 1) { @@ -4311,10 +4306,7 @@ namespace Microsoft.Dafny { } else if (expr is SeqSelectExpr) { SeqSelectExpr e = (SeqSelectExpr)expr; Bpl.Expr total = CanCallAssumption(e.Seq, etran); - Bpl.Expr seq = etran.TrExpr(e.Seq); - Bpl.Expr e0 = null; if (e.E0 != null) { - e0 = etran.TrExpr(e.E0); total = BplAnd(total, CanCallAssumption(e.E0, etran)); } if (e.E1 != null) { @@ -4335,8 +4327,6 @@ namespace Microsoft.Dafny { return CanCallAssumption(e.ResolvedUpdateExpr, etran); } Bpl.Expr total = CanCallAssumption(e.Seq, etran); - Bpl.Expr seq = etran.TrExpr(e.Seq); - Bpl.Expr index = etran.TrExpr(e.Index); total = BplAnd(total, CanCallAssumption(e.Index, etran)); total = BplAnd(total, CanCallAssumption(e.Value, etran)); return total; @@ -4347,18 +4337,13 @@ namespace Microsoft.Dafny { e.Args.ConvertAll(ee => CanCallAssumption(ee, etran)))); } else if (expr is FunctionCallExpr) { FunctionCallExpr e = (FunctionCallExpr)expr; - // check well-formedness of receiver Bpl.Expr r = CanCallAssumption(e.Receiver, etran); - // check well-formedness of the other parameters r = BplAnd(r, CanCallAssumption(e.Args, etran)); - // if (e.Name != "requires" && e.Name != "reads") { - Contract.Assert(e.Function != null); // follows from the fact that expr has been successfully resolved - // get to assume canCall - Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(expr.tok, e.Function.FullSanitizedName + "#canCall", Bpl.Type.Bool); - List args = etran.FunctionInvocationArguments(e, null); - Bpl.Expr canCallFuncAppl = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(canCallFuncID), args); - r = BplAnd(r, canCallFuncAppl); - // } + // get to assume canCall + Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(expr.tok, e.Function.FullSanitizedName + "#canCall", Bpl.Type.Bool); + List args = etran.FunctionInvocationArguments(e, null); + Bpl.Expr canCallFuncAppl = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(canCallFuncID), args); + r = BplAnd(r, canCallFuncAppl); return r; } else if (expr is DatatypeValue) { DatatypeValue dtv = (DatatypeValue)expr; @@ -4379,10 +4364,10 @@ namespace Microsoft.Dafny { switch (e.ResolvedOp) { case BinaryExpr.ResolvedOpcode.And: case BinaryExpr.ResolvedOpcode.Imp: - t1 = Bpl.Expr.Imp(etran.TrExpr(e.E0), t1); + t1 = BplImp(etran.TrExpr(e.E0), t1); break; case BinaryExpr.ResolvedOpcode.Or: - t1 = Bpl.Expr.Imp(Bpl.Expr.Not(etran.TrExpr(e.E0)), t1); + t1 = BplImp(Bpl.Expr.Not(etran.TrExpr(e.E0)), t1); break; default: break; @@ -4419,12 +4404,10 @@ namespace Microsoft.Dafny { LetDesugaring(e); // call LetDesugaring to prepare the desugaring and populate letSuchThatExprInfo with something for e var info = letSuchThatExprInfo[e]; // $let$canCall(g) - //var canCall = FunctionCall(e.tok, info.CanCallFunctionName(), Bpl.Type.Bool, gExprs); var canCall = info.CanCallFunctionCall(this, etran); Dictionary substMap = new Dictionary(); foreach (var bv in e.BoundVars) { // create a call to $let$x(g) - //var call = FunctionCall(e.tok, info.SkolemFunctionName(bv), TrType(bv.Type), gExprs); var args = info.SkolemFunctionArgs(bv, this, etran); var call = new BoogieFunctionCall(bv.tok, info.SkolemFunctionName(bv), info.UsesHeap, info.UsesOldHeap, args.Item1, args.Item2); call.Type = bv.Type; @@ -4441,54 +4424,64 @@ namespace Microsoft.Dafny { if (e.Contract != null) return BplAnd(canCall, CanCallAssumption(e.Contract, etran)); else return canCall; + } else if (expr is LambdaExpr) { var e = (LambdaExpr)expr; - List bvars = new List(); - + var bvarsAndAntecedents = new List>(); var varNameGen = CurrentIdGenerator.NestedFreshIdGenerator("$l#"); Bpl.Expr heap; var hVar = BplBoundVar(varNameGen.FreshId("#heap#"), predef.HeapType, out heap); - bvars.Add(hVar); + var et = new ExpressionTranslator(etran, heap); Dictionary subst = new Dictionary(); foreach (var bv in e.BoundVars) { Bpl.Expr ve; var yVar = BplBoundVar(varNameGen.FreshId(string.Format("#{0}#", bv.Name)), TrType(bv.Type), out ve); - bvars.Add(yVar); + var wh = GetWhereClause(bv.tok, new Bpl.IdentifierExpr(bv.tok, yVar), bv.Type, et); + bvarsAndAntecedents.Add(Tuple.Create(yVar, wh)); subst[bv] = new BoogieWrapper(ve, bv.Type); } - ExpressionTranslator et = new ExpressionTranslator(etran, heap); - var ebody = CanCallAssumption(Substitute(e.Body, null, subst), et); + var canCall = CanCallAssumption(Substitute(e.Body, null, subst), et); + if (e.Range != null) { + var range = Substitute(e.Range, null, subst); + canCall = BplAnd(CanCallAssumption(range, etran), BplImp(etran.TrExpr(range), canCall)); + } + + // It's important to add the heap last to "bvarsAndAntecedents", because the heap may occur in the antecedents of + // the other variables and BplForallTrim processes the given tuples in order. + var goodHeap = FunctionCall(e.tok, BuiltinFunction.IsGoodHeap, null, heap); + bvarsAndAntecedents.Add(Tuple.Create(hVar, goodHeap)); //TRIG (forall $l#0#heap#0: Heap, $l#0#x#0: int :: true) //TRIG (forall $l#0#heap#0: Heap, $l#0#t#0: DatatypeType :: _module.__default.TMap#canCall(_module._default.TMap$A, _module._default.TMap$B, $l#0#heap#0, $l#0#t#0, f#0)) //TRIG (forall $l#4#heap#0: Heap, $l#4#x#0: Box :: _0_Monad.__default.Bind#canCall(Monad._default.Associativity$B, Monad._default.Associativity$C, $l#4#heap#0, Apply1(Monad._default.Associativity$A, #$M$B, f#0, $l#4#heap#0, $l#4#x#0), g#0)) - return BplForall(bvars, ebody); // L_TRIGGER + return BplForallTrim(bvarsAndAntecedents, null, canCall); // L_TRIGGER + } else if (expr is ComprehensionExpr) { var e = (ComprehensionExpr)expr; - var canCall = CanCallAssumption(e.Term, etran); var q = e as QuantifierExpr; - if (q != null && q.SplitQuantifier != null) { return CanCallAssumption(q.SplitQuantifierExpression, etran); } - var tyvars = MkTyParamBinders(q != null ? q.TypeArgs : new List()); + // Determine the CanCall's for the range and term + var canCall = CanCallAssumption(e.Term, etran); if (e.Range != null) { canCall = BplAnd(CanCallAssumption(e.Range, etran), BplImp(etran.TrExpr(e.Range), canCall)); } - if (canCall != Bpl.Expr.True) { - List bvars = new List(); - Bpl.Expr typeAntecedent = etran.TrBoundVariables(e.BoundVars, bvars); - if (Attributes.Contains(e.Attributes, "trigger")) { - Bpl.Trigger tr = TrTrigger(etran, e.Attributes, expr.tok); - canCall = new Bpl.ForallExpr(expr.tok, Concat(tyvars, bvars), tr, Bpl.Expr.Imp(typeAntecedent, canCall)); - } else { - canCall = new Bpl.ForallExpr(expr.tok, Concat(tyvars, bvars), Bpl.Expr.Imp(typeAntecedent, canCall)); // SMART_TRIGGER + // Create a list of all possible bound variables + var bvarsAndAntecedents = etran.TrBoundVariables_SeparateWhereClauses(e.BoundVars); + if (q != null) { + var tyvars = MkTyParamBinders(q.TypeArgs); + foreach (var tv in tyvars) { + bvarsAndAntecedents.Add(Tuple.Create(tv, null)); } } - return canCall; + // Produce the quantified CanCall expression, with a suitably reduced set of bound variables + var tr = TrTrigger(etran, e.Attributes, expr.tok); + return BplForallTrim(bvarsAndAntecedents, tr, canCall); + } else if (expr is StmtExpr) { var e = (StmtExpr)expr; return CanCallAssumption(e.E, etran); @@ -4496,8 +4489,8 @@ namespace Microsoft.Dafny { ITEExpr e = (ITEExpr)expr; Bpl.Expr total = CanCallAssumption(e.Test, etran); Bpl.Expr test = etran.TrExpr(e.Test); - total = BplAnd(total, Bpl.Expr.Imp(test, CanCallAssumption(e.Thn, etran))); - total = BplAnd(total, Bpl.Expr.Imp(Bpl.Expr.Not(test), CanCallAssumption(e.Els, etran))); + total = BplAnd(total, BplImp(test, CanCallAssumption(e.Thn, etran))); + total = BplAnd(total, BplImp(Bpl.Expr.Not(test), CanCallAssumption(e.Els, etran))); return total; } else if (expr is ConcreteSyntaxExpression) { var e = (ConcreteSyntaxExpression)expr; @@ -4909,7 +4902,7 @@ namespace Microsoft.Dafny { var fieldName = FunctionCall(e.tok, BuiltinFunction.IndexField, null, i); var allowedToRead = Bpl.Expr.SelectTok(e.tok, etran.TheFrame(e.tok), seq, fieldName); var trigger = BplTrigger(allowedToRead); // Note, the assertion we're about to produce only seems useful in the check-only mode (that is, with subsumption 0), but if it were to be assumed, we'll use this entire RHS as the trigger - var qq = new Bpl.ForallExpr(e.tok, new List { iVar }, trigger, Bpl.Expr.Imp(range, allowedToRead)); + var qq = new Bpl.ForallExpr(e.tok, new List { iVar }, trigger, BplImp(range, allowedToRead)); options.AssertSink(this, builder)(expr.tok, qq, "insufficient reads clause to read the indicated range of array elements", options.AssertKv); } } @@ -11789,6 +11782,20 @@ namespace Microsoft.Dafny { return typeAntecedent; } + public List> TrBoundVariables_SeparateWhereClauses(List boundVars) { + Contract.Requires(boundVars != null); + Contract.Ensures(Contract.Result>>() != null); + + var varsAndAntecedents = new List>(); + foreach (BoundVar bv in boundVars) { + var tid = new Bpl.TypedIdent(bv.tok, bv.AssignUniqueName(translator.currentDeclaration.IdGenerator), translator.TrType(bv.Type)); + var bvar = new Bpl.BoundVariable(bv.tok, tid); + var wh = translator.GetWhereClause(bv.tok, new Bpl.IdentifierExpr(bv.tok, bvar), bv.Type, this); + varsAndAntecedents.Add(Tuple.Create(bvar, wh)); + } + return varsAndAntecedents; + } + public Bpl.Expr TrBoundVariablesRename(List boundVars, List bvars, out Dictionary substMap) { Contract.Requires(boundVars != null); Contract.Requires(bvars != null); @@ -14205,6 +14212,69 @@ namespace Microsoft.Dafny { // Bpl-making-utilities + /// + /// Create a Boogie quantifier with body "A ==> body" and triggers "trg", but use only the subset of bound + /// variables from "varsAndAntecedents" that actually occur free in "body" or "trg", and "A" is the conjunction of + /// antecedents for those corresponding bound variables. If none of the bound variables is used, "body" + /// is returned. + /// The order of the contents of "varsAndAntecedents" matters: For any index "i" into "varsAndAntecedents", the + /// antecedent varsAndAntecedents[i].Item2 may depend on a variable varsAndAntecedents[j].Item1 if "j GREATER-OR-EQUAL i" + /// but not if "j LESS i". + /// Caution: if "trg" is null, makes a forall without any triggers. + /// + static Bpl.Expr BplForallTrim(IEnumerable> varsAndAntecedents, Bpl.Trigger trg, Bpl.Expr body) { + Contract.Requires(varsAndAntecedents != null); + Contract.Requires(body != null); + + // We'd like to compute the free variables if "body" and "trg". It would be nice to use the Boogie + // routine Bpl.Expr.ComputeFreeVariables for this purpose. However, calling it requires the Boogie + // expression to be resolved. Instead, we do the cheesy thing of computing the set of names of + // free variables in "body" and "trg". + var vis = new VariableNameVisitor(); + vis.Visit(body); + for (var tt = trg; tt != null; tt = tt.Next) { + tt.Tr.Iter(ee => vis.Visit(ee)); + } + + var args = new List(); + Bpl.Expr typeAntecedent = Bpl.Expr.True; + foreach (var pair in varsAndAntecedents) { + var bv = pair.Item1; + var wh = pair.Item2; + if (vis.Names.Contains(bv.Name)) { + args.Add(bv); + if (wh != null) { + typeAntecedent = BplAnd(typeAntecedent, wh); + vis.Visit(wh); // this adds to "vis.Names" the free variables of "wh" + } + } + } + if (args.Count == 0) { + return body; + } else { + return new Bpl.ForallExpr(body.tok, args, trg, BplImp(typeAntecedent, body)); + } + } + class VariableNameVisitor : Boogie.StandardVisitor + { + public readonly HashSet Names = new HashSet(); + public override Expr VisitIdentifierExpr(Bpl.IdentifierExpr node) { + Names.Add(node.Name); + return base.VisitIdentifierExpr(node); + } + public override BinderExpr VisitBinderExpr(BinderExpr node) { + var vis = new VariableNameVisitor(); + vis.Visit(node.Body); + var dummyNames = new HashSet(node.Dummies.Select(v => v.Name)); + foreach (var nm in vis.Names) { + if (!dummyNames.Contains(nm)) { + Names.Add(nm); + } + } + return base.VisitBinderExpr(node); + } + } + static Bpl.Expr BplForall(IEnumerable args_in, Bpl.Expr body) { Contract.Requires(args_in != null); Contract.Requires(body != null); -- cgit v1.2.3