From b8fad094ad74180ca16670bebe602737d856b5da Mon Sep 17 00:00:00 2001 From: qunyanm Date: Wed, 25 Nov 2015 10:27:02 -0800 Subject: Fix issue 103. Emit the quantifiers for ForallStmt before AutoTrigger so that the auto-triggers can be computed for ForallStmt. --- Source/Dafny/Cloner.cs | 4 +- Source/Dafny/DafnyAst.cs | 1 + Source/Dafny/Printer.cs | 15 +- Source/Dafny/Resolver.cs | 1 + Source/Dafny/Rewriter.cs | 273 +++++++++++++++++++++ Source/Dafny/Translator.cs | 340 +++++++------------------- Source/Dafny/Triggers/QuantifierSplitter.cs | 12 + Source/Dafny/Triggers/QuantifiersCollector.cs | 13 + Test/dafny0/SmallTests.dfy.expect | 1 + Test/dafny4/Bug103.dfy | 20 ++ Test/dafny4/Bug103.dfy.expect | 2 + 11 files changed, 424 insertions(+), 258 deletions(-) create mode 100644 Test/dafny4/Bug103.dfy create mode 100644 Test/dafny4/Bug103.dfy.expect diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index 1a6dfecb..6b3b0caa 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -552,7 +552,9 @@ namespace Microsoft.Dafny } else if (stmt is ForallStmt) { var s = (ForallStmt)stmt; r = new ForallStmt(Tok(s.Tok), Tok(s.EndTok), s.BoundVars.ConvertAll(CloneBoundVar), null, CloneExpr(s.Range), s.Ens.ConvertAll(CloneMayBeFreeExpr), CloneStmt(s.Body)); - + if (s.ForallExpressions != null) { + ((ForallStmt)r).ForallExpressions = s.ForallExpressions.ConvertAll(CloneExpr); + } } else if (stmt is CalcStmt) { var s = (CalcStmt)stmt; // calc statements have the unusual property that the last line is duplicated. If that is the case (which diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 847617aa..4c1e2bd7 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -4693,6 +4693,7 @@ namespace Microsoft.Dafny { public readonly Expression Range; public readonly List Ens; public readonly Statement Body; + public List ForallExpressions; // fill in by rewriter. public List Bounds; // initialized and filled in by resolver // invariant: if successfully resolved, Bounds.Count == BoundVars.Count; diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 145e82e7..0a25b941 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -841,11 +841,22 @@ namespace Microsoft.Dafny { wr.Write("}"); } else if (stmt is ForallStmt) { - var s = (ForallStmt)stmt; + var s = (ForallStmt)stmt; + Attributes attributes = s.Attributes; + if (attributes == null && s.ForallExpressions != null) { + foreach (Expression expr in s.ForallExpressions) { + ForallExpr e = (ForallExpr)expr; + while (e != null && attributes == null) { + attributes = e.Attributes; + e = (ForallExpr)e.SplitQuantifierExpression; + } + if (attributes != null) { break; } + } + } wr.Write("forall"); if (s.BoundVars.Count != 0) { wr.Write(" "); - PrintQuantifierDomain(s.BoundVars, s.Attributes, s.Range); + PrintQuantifierDomain(s.BoundVars, attributes, s.Range); } if (s.Ens.Count == 0) { wr.Write(" "); diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 315b823a..eff7d97d 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -235,6 +235,7 @@ namespace Microsoft.Dafny rewriters.Add(new AutoReqFunctionRewriter(this.reporter, opaqueRewriter)); rewriters.Add(opaqueRewriter); rewriters.Add(new TimeLimitRewriter(reporter)); + rewriters.Add(new ForallStmtRewriter(reporter)); if (DafnyOptions.O.AutoTriggers) { rewriters.Add(new QuantifierSplittingRewriter(reporter)); diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index 39c8f667..802b1918 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -72,6 +72,279 @@ namespace Microsoft.Dafny } } + // write out the quantifier for ForallStmt + public class ForallStmtRewriter : IRewriter + { + public ForallStmtRewriter(ErrorReporter reporter) : base(reporter) { + Contract.Requires(reporter != null); + } + + internal override void PostResolve(ModuleDefinition m) { + var forallvisiter = new ForAllStmtVisitor(); + foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) { + forallvisiter.Visit(decl, true); + } + } + + internal class ForAllStmtVisitor : TopDownVisitor + { + protected override bool VisitOneStmt(Statement stmt, ref bool st) { + Contract.Requires(stmt != null); + if (stmt is ForallStmt) { + ForallStmt s = (ForallStmt)stmt; + if (s.Kind == ForallStmt.ParBodyKind.Proof) { + Expression term = s.Ens.Count != 0 ? s.Ens[0].E : new LiteralExpr(s.Tok, true); + for (int i = 1; i < s.Ens.Count; i++) { + term = new BinaryExpr(s.Tok, BinaryExpr.ResolvedOpcode.And, term, s.Ens[i].E); + } + List exprList = new List(); + ForallExpr expr = new ForallExpr(s.Tok, s.BoundVars, s.Range, term, s.Attributes); + expr.Type = Type.Bool; // resolve here + exprList.Add(expr); + s.ForallExpressions = exprList; + } else if (s.Kind == ForallStmt.ParBodyKind.Assign) { + if (s.BoundVars.Count != 0) { + var s0 = (AssignStmt)s.S0; + if (s0.Rhs is ExprRhs) { + List exprList = new List(); + Expression Fi = null; + Func lhsBuilder = null; + var lhs = s0.Lhs.Resolved; + var i = s.BoundVars[0]; + if (s.BoundVars.Count == 1) { + //var lhsContext = null; + // Detect the following cases: + // 0: forall i | R(i) { F(i).f := E(i); } + // 1: forall i | R(i) { A[F(i)] := E(i); } + // 2: forall i | R(i) { F(i)[N] := E(i); } + if (lhs is MemberSelectExpr) { + var ll = (MemberSelectExpr)lhs; + Fi = ll.Obj; + lhsBuilder = e => { var l = new MemberSelectExpr(ll.tok, e, ll.MemberName); l.Member = ll.Member; l.Type = ll.Type; return l; }; + } else if (lhs is SeqSelectExpr) { + var ll = (SeqSelectExpr)lhs; + Contract.Assert(ll.SelectOne); + if (!Translator.ContainsFreeVariable(ll.Seq, false, i)) { + Fi = ll.E0; + lhsBuilder = e => { var l = new SeqSelectExpr(ll.tok, true, ll.Seq, e, null); l.Type = ll.Type; return l; }; + } else if (!Translator.ContainsFreeVariable(ll.E0, false, i)) { + Fi = ll.Seq; + lhsBuilder = e => { var l = new SeqSelectExpr(ll.tok, true, e, ll.E0, null); l.Type = ll.Type; return l; }; + } + } + } + var rhs = ((ExprRhs)s0.Rhs).Expr; + bool usedInversion = false; + if (Fi != null) { + var j = new BoundVar(i.tok, i.Name + "#inv", Fi.Type); + var jj = Expression.CreateIdentExpr(j); + var jList = new List() { j }; + var vals = InvertExpression(i, j, s.Range, Fi); +#if DEBUG_PRINT + Console.WriteLine("DEBUG: Trying to invert:"); + Console.WriteLine("DEBUG: " + Printer.ExprToString(s.Range) + " && " + j.Name + " == " + Printer.ExprToString(Fi)); + if (vals == null) { + Console.WriteLine("DEBUG: Can't"); + } else { + Console.WriteLine("DEBUG: The inverse is the disjunction of the following:"); + foreach (var val in vals) { + Console.WriteLine("DEBUG: " + Printer.ExprToString(val.Range) + " && " + Printer.ExprToString(val.FInverse) + " == " + i.Name); + } + } +#endif + if (vals != null) { + foreach (var val in vals) { + lhs = lhsBuilder(jj); + Attributes attributes = new Attributes("trigger", new List() { lhs }, s.Attributes); + var expr = new ForallExpr(s.Tok, jList, val.Range, new BinaryExpr(s.Tok, BinaryExpr.ResolvedOpcode.EqCommon, lhs, Substitute(rhs, i, val.FInverse)), attributes); + expr.Type = Type.Bool; //resolve here + exprList.Add(expr); + } + usedInversion = true; + } + } + if (!usedInversion) { + var expr = new ForallExpr(s.Tok, s.BoundVars, s.Range, new BinaryExpr(s.Tok, BinaryExpr.ResolvedOpcode.EqCommon, lhs, rhs), s.Attributes); + expr.Type = Type.Bool; // resolve here + exprList.Add(expr); + } + s.ForallExpressions = exprList; + } + } + } else if (s.Kind == ForallStmt.ParBodyKind.Call) { + var s0 = (CallStmt)s.S0; + Expression term = s0.Method.Ens.Count != 0 ? s0.Method.Ens[0].E : new LiteralExpr(s.Tok, true); + for (int i = 1; i < s0.Method.Ens.Count; i++) { + term = new BinaryExpr(s.Tok, BinaryExpr.ResolvedOpcode.And, term, s0.Method.Ens[i].E); + } + List exprList = new List(); + ForallExpr expr = new ForallExpr(s.Tok, s.BoundVars, s.Range, term, s.Attributes); + expr.Type = Type.Bool; // resolve here + exprList.Add(expr); + } else { + Contract.Assert(false); // unexpected kind + } + } + return true; //visit the sub-parts with the same "st" + } + + internal class ForallStmtTranslationValues + { + public readonly Expression Range; + public readonly Expression FInverse; + public ForallStmtTranslationValues(Expression range, Expression fInverse) { + Contract.Requires(range != null); + Contract.Requires(fInverse != null); + Range = range; + FInverse = fInverse; + } + public ForallStmtTranslationValues Subst(IVariable j, Expression e) { + Contract.Requires(j != null); + Contract.Requires(e != null); + Dictionary typeMap = new Dictionary(); + var substMap = new Dictionary(); + substMap.Add(j, e); + Translator.Substituter sub = new Translator.Substituter(null, substMap, typeMap, null); + var v = new ForallStmtTranslationValues(sub.Substitute(Range), sub.Substitute(FInverse)); + return v; + } + } + + /// + /// Find piecewise inverse of F under R. More precisely, find lists of expressions P and F-1 + /// such that + /// R(i) && j == F(i) + /// holds iff the disjunction of the following predicates holds: + /// P_0(j) && F-1_0(j) == i + /// ... + /// P_{n-1}(j) && F-1_{n-1}(j) == i + /// If no such disjunction is found, return null. + /// If such a disjunction is found, return for each disjunct: + /// * The predicate P_k(j), which is an expression that may have free occurrences of j (but no free occurrences of i) + /// * The expression F-1_k(j), which also may have free occurrences of j but not of i + /// + private List InvertExpression(BoundVar i, BoundVar j, Expression R, Expression F) { + Contract.Requires(i != null); + Contract.Requires(j != null); + Contract.Requires(R != null); + Contract.Requires(F != null); + var vals = new List(InvertExpressionIter(i, j, R, F)); + if (vals.Count == 0) { + return null; + } else { + return vals; + } + } + /// + /// See InvertExpression. + /// + private IEnumerable InvertExpressionIter(BoundVar i, BoundVar j, Expression R, Expression F) { + Contract.Requires(i != null); + Contract.Requires(j != null); + Contract.Requires(R != null); + Contract.Requires(F != null); + F = F.Resolved; + if (!Translator.ContainsFreeVariable(F, false, i)) { + // We're looking at R(i) && j == K. + // We cannot invert j == K, but if we're lucky, R(i) contains a conjunct i==G. + Expression r = Expression.CreateBoolLiteral(R.tok, true); + Expression G = null; + foreach (var c in Expression.Conjuncts(R)) { + if (G == null && c is BinaryExpr) { + var bin = (BinaryExpr)c; + if (BinaryExpr.IsEqualityOp(bin.ResolvedOp)) { + var id = bin.E0.Resolved as IdentifierExpr; + if (id != null && id.Var == i) { + G = bin.E1; + continue; + } + id = bin.E1.Resolved as IdentifierExpr; + if (id != null && id.Var == i) { + G = bin.E0; + continue; + } + } + } + r = Expression.CreateAnd(r, c); + } + if (G != null) { + var jIsK = Expression.CreateEq(Expression.CreateIdentExpr(j), F, j.Type); + var rr = Substitute(r, i, G); + yield return new ForallStmtTranslationValues(Expression.CreateAnd(rr, jIsK), G); + } + } else if (F is IdentifierExpr) { + var e = (IdentifierExpr)F; + if (e.Var == i) { + // We're looking at R(i) && j == i, which is particularly easy to invert: R(j) && j == i + var jj = Expression.CreateIdentExpr(j); + yield return new ForallStmtTranslationValues(Substitute(R, i, jj), jj); + } + } else if (F is BinaryExpr) { + var bin = (BinaryExpr)F; + if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Add && (bin.E0.Type.IsIntegerType || bin.E0.Type.IsRealType)) { + if (!Translator.ContainsFreeVariable(bin.E1, false, i)) { + // We're looking at: R(i) && j == f(i) + K. + // By a recursive call, we'll ask to invert: R(i) && j' == f(i). + // For each P_0(j') && f-1_0(j') == i we get back, we yield: + // P_0(j - K) && f-1_0(j - K) == i + var jMinusK = Expression.CreateSubtract(Expression.CreateIdentExpr(j), bin.E1); + foreach (var val in InvertExpression(i, j, R, bin.E0)) { + yield return val.Subst(j, jMinusK); + } + } else if (!Translator.ContainsFreeVariable(bin.E0, false, i)) { + // We're looking at: R(i) && j == K + f(i) + // Do as in previous case, but with operands reversed. + var jMinusK = Expression.CreateSubtract(Expression.CreateIdentExpr(j), bin.E0); + foreach (var val in InvertExpression(i, j, R, bin.E1)) { + yield return val.Subst(j, jMinusK); + } + } + } else if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Sub && (bin.E0.Type.IsIntegerType || bin.E0.Type.IsRealType)) { + if (!Translator.ContainsFreeVariable(bin.E1, false, i)) { + // We're looking at: R(i) && j == f(i) - K + // Recurse on f(i) and then replace j := j + K + var jPlusK = Expression.CreateAdd(Expression.CreateIdentExpr(j), bin.E1); + foreach (var val in InvertExpression(i, j, R, bin.E0)) { + yield return val.Subst(j, jPlusK); + } + } else if (!Translator.ContainsFreeVariable(bin.E0, false, i)) { + // We're looking at: R(i) && j == K - f(i) + // Recurse on f(i) and then replace j := K - j + var kMinusJ = Expression.CreateAdd(Expression.CreateIdentExpr(j), bin.E0); + foreach (var val in InvertExpression(i, j, R, bin.E1)) { + yield return val.Subst(j, kMinusJ); + } + } + } + } else if (F is ITEExpr) { + var ife = (ITEExpr)F; + // We're looking at R(i) && j == if A(i) then B(i) else C(i), which is equivalent to the disjunction of: + // R(i) && A(i) && j == B(i) + // R(i) && !A(i) && j == C(i) + // We recurse on each one, yielding the results + var r = Expression.CreateAnd(R, ife.Test); + var valsThen = InvertExpression(i, j, r, ife.Thn); + if (valsThen != null) { + r = Expression.CreateAnd(R, Expression.CreateNot(ife.tok, ife.Test)); + var valsElse = InvertExpression(i, j, r, ife.Els); + if (valsElse != null) { + foreach (var val in valsThen) { yield return val; } + foreach (var val in valsElse) { yield return val; } + } + } + } + } + + Expression Substitute(Expression expr, IVariable v, Expression e) { + Dictionary substMap = new Dictionary(); + Dictionary typeMap = new Dictionary(); + substMap.Add(v, e); + Translator.Substituter sub = new Translator.Substituter(null, substMap, typeMap, null); + return sub.Substitute(expr); + } + } + } + /// /// AutoContracts is an experimental feature that will fill much of the dynamic-frames boilerplate /// into a class. From the user's perspective, what needs to be done is simply: diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 8e8c3c19..37408aa1 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -2860,11 +2860,11 @@ namespace Microsoft.Dafny { #if VERIFY_CORRECTNESS_OF_TRANSLATION_FORALL_STATEMENT_RANGE var definedness = new Bpl.StmtListBuilder(); var exporter = new Bpl.StmtListBuilder(); - TrForallStmtCall(m.tok, parBoundVars, parRange, decrCheck, recursiveCall, definedness, exporter, localVariables, etran); + TrForallStmtCall(m.tok, parBoundVars, parRange, decrCheck, null, recursiveCall, definedness, exporter, localVariables, etran); // All done, so put the two pieces together builder.Add(new Bpl.IfCmd(m.tok, null, definedness.Collect(m.tok), null, exporter.Collect(m.tok))); #else - TrForallStmtCall(m.tok, parBoundVars, parRange, decrCheck, recursiveCall, null, builder, localVariables, etran); + TrForallStmtCall(m.tok, parBoundVars, parRange, decrCheck, null, recursiveCall, null, builder, localVariables, etran); #endif } // translate the body of the method @@ -7413,7 +7413,7 @@ namespace Microsoft.Dafny { var s0 = (CallStmt)s.S0; var definedness = new Bpl.StmtListBuilder(); var exporter = new Bpl.StmtListBuilder(); - TrForallStmtCall(s.Tok, s.BoundVars, s.Range, null, s0, definedness, exporter, locals, etran); + TrForallStmtCall(s.Tok, s.BoundVars, s.Range, null, s.ForallExpressions, s0, definedness, exporter, locals, etran); // All done, so put the two pieces together builder.Add(new Bpl.IfCmd(s.Tok, null, definedness.Collect(s.Tok), null, exporter.Collect(s.Tok))); builder.Add(CaptureState(stmt)); @@ -8038,65 +8038,16 @@ namespace Microsoft.Dafny { Bpl.Expr qq = new Bpl.ForallExpr(s.Tok, new List { alpha }, new List { oVar, fVar }, null, tr, body); updater.Add(new Bpl.AssumeCmd(s.Tok, qq)); - if (s0.Rhs is ExprRhs) { - Expression Fi = null; - Func lhsBuilder = null; - lhs = s0.Lhs.Resolved; - var i = s.BoundVars[0]; - if (s.BoundVars.Count == 1) { - //var lhsContext = null; - // Detect the following cases: - // 0: forall i | R(i) { F(i).f := E(i); } - // 1: forall i | R(i) { A[F(i)] := E(i); } - // 2: forall i | R(i) { F(i)[N] := E(i); } - if (lhs is MemberSelectExpr) { - var ll = (MemberSelectExpr)lhs; - Fi = ll.Obj; - lhsBuilder = e => { var l = new MemberSelectExpr(ll.tok, e, ll.MemberName); l.Member = ll.Member; l.Type = ll.Type; return l; }; - } else if (lhs is SeqSelectExpr) { - var ll = (SeqSelectExpr)lhs; - Contract.Assert(ll.SelectOne); - if (!ContainsFreeVariable(ll.Seq, false, i)) { - Fi = ll.E0; - lhsBuilder = e => { var l = new SeqSelectExpr(ll.tok, true, ll.Seq, e, null); l.Type = ll.Type; return l; }; - } else if (!ContainsFreeVariable(ll.E0, false, i)) { - Fi = ll.Seq; - lhsBuilder = e => { var l = new SeqSelectExpr(ll.tok, true, e, ll.E0, null); l.Type = ll.Type; return l; }; - } - } - } - var rhs = ((ExprRhs)s0.Rhs).Expr; - bool usedInversion = false; - if (Fi != null) { - var j = new BoundVar(i.tok, i.Name + "#inv", Fi.Type); - var jj = Expression.CreateIdentExpr(j); - var jList = new List() { j }; - var vals = InvertExpression(i, j, s.Range, Fi); -#if DEBUG_PRINT - Console.WriteLine("DEBUG: Trying to invert:"); - Console.WriteLine("DEBUG: " + Printer.ExprToString(s.Range) + " && " + j.Name + " == " + Printer.ExprToString(Fi)); - if (vals == null) { - Console.WriteLine("DEBUG: Can't"); - } else { - Console.WriteLine("DEBUG: The inverse is the disjunction of the following:"); - foreach (var val in vals) { - Console.WriteLine("DEBUG: " + Printer.ExprToString(val.Range) + " && " + Printer.ExprToString(val.FInverse) + " == " + i.Name); - } - } -#endif - if (vals != null) { - foreach (var val in vals) { - qq = TrForall_NewValueAssumption(s.Tok, jList, val.Range, lhsBuilder(jj), Substitute(rhs, i, val.FInverse), true, etran, prevEtran); - updater.Add(new Bpl.AssumeCmd(s.Tok, qq)); - } - usedInversion = true; - } - } - if (!usedInversion) { - qq = TrForall_NewValueAssumption(s.Tok, s.BoundVars, s.Range, lhs, rhs, false, etran, prevEtran); + if (s.ForallExpressions != null) { + foreach (ForallExpr expr in s.ForallExpressions) { + BinaryExpr term = (BinaryExpr)expr.Term; + Contract.Assert(term != null); + var e0 = Substitute(((BinaryExpr)term).E0.Resolved, null, substMap); + var e1 = Substitute(((BinaryExpr)term).E1, null, substMap); + qq = TrForall_NewValueAssumption(expr.tok, expr.BoundVars, expr.Range, e0, e1, expr.Attributes, etran, prevEtran); updater.Add(new Bpl.AssumeCmd(s.Tok, qq)); } - } + } } /// @@ -8110,7 +8061,7 @@ namespace Microsoft.Dafny { /// G is rhs /// If lhsAsTrigger is true, then use the LHS of the equality above as the trigger; otherwise, don't specify any trigger. /// - private Bpl.Expr TrForall_NewValueAssumption(IToken tok, List boundVars, Expression range, Expression lhs, Expression rhs, bool lhsAsTrigger, ExpressionTranslator etran, ExpressionTranslator prevEtran) { + private Bpl.Expr TrForall_NewValueAssumption(IToken tok, List boundVars, Expression range, Expression lhs, Expression rhs, Attributes attributes, ExpressionTranslator etran, ExpressionTranslator prevEtran) { Contract.Requires(tok != null); Contract.Requires(boundVars != null); Contract.Requires(range != null); @@ -8130,159 +8081,27 @@ namespace Microsoft.Dafny { Type lhsType = lhs is MemberSelectExpr ? ((MemberSelectExpr)lhs).Type : null; g = CondApplyBox(rhs.tok, g, rhs.Type, lhsType); - Trigger tr = lhsAsTrigger ? new Trigger(tok, true, new List() { xHeapOF }) : null; - return new Bpl.ForallExpr(tok, xBvars, tr, Bpl.Expr.Imp(xAnte, Bpl.Expr.Eq(xHeapOF, g))); - } - - class ForallStmtTranslationValues - { - public readonly Expression Range; - public readonly Expression FInverse; - public ForallStmtTranslationValues(Expression range, Expression fInverse) { - Contract.Requires(range != null); - Contract.Requires(fInverse != null); - Range = range; - FInverse = fInverse; - } - public ForallStmtTranslationValues Subst(IVariable j, Expression e, Translator translator) { - Contract.Requires(j != null); - Contract.Requires(e != null); - Contract.Requires(translator != null); - var substMap = new Dictionary(); - substMap.Add(j, e); - var v = new ForallStmtTranslationValues(translator.Substitute(Range, null, substMap), translator.Substitute(FInverse, null, substMap)); - return v; - } - } - - /// - /// Find piecewise inverse of F under R. More precisely, find lists of expressions P and F-1 - /// such that - /// R(i) && j == F(i) - /// holds iff the disjunction of the following predicates holds: - /// P_0(j) && F-1_0(j) == i - /// ... - /// P_{n-1}(j) && F-1_{n-1}(j) == i - /// If no such disjunction is found, return null. - /// If such a disjunction is found, return for each disjunct: - /// * The predicate P_k(j), which is an expression that may have free occurrences of j (but no free occurrences of i) - /// * The expression F-1_k(j), which also may have free occurrences of j but not of i - /// - private List InvertExpression(BoundVar i, BoundVar j, Expression R, Expression F) { - Contract.Requires(i != null); - Contract.Requires(j != null); - Contract.Requires(R != null); - Contract.Requires(F != null); - var vals = new List(InvertExpressionIter(i, j, R, F)); - if (vals.Count == 0) { - return null; - } else { - return vals; - } - } - /// - /// See InvertExpression. - /// - private IEnumerable InvertExpressionIter(BoundVar i, BoundVar j, Expression R, Expression F) { - Contract.Requires(i != null); - Contract.Requires(j != null); - Contract.Requires(R != null); - Contract.Requires(F != null); - F = F.Resolved; - if (!ContainsFreeVariable(F, false, i)) { - // We're looking at R(i) && j == K. - // We cannot invert j == K, but if we're lucky, R(i) contains a conjunct i==G. - Expression r = Expression.CreateBoolLiteral(R.tok, true); - Expression G = null; - foreach (var c in Expression.Conjuncts(R)) { - if (G == null && c is BinaryExpr) { - var bin = (BinaryExpr)c; - if (BinaryExpr.IsEqualityOp(bin.ResolvedOp)) { - var id = bin.E0.Resolved as IdentifierExpr; - if (id != null && id.Var == i) { - G = bin.E1; - continue; - } - id = bin.E1.Resolved as IdentifierExpr; - if (id != null && id.Var == i) { - G = bin.E0; - continue; - } + Bpl.Trigger tr = null; + var argsEtran = etran.WithNoLits(); + foreach (var aa in attributes.AsEnumerable()) { + if (aa.Name == "trigger") { + List tt = new List(); + foreach (var arg in aa.Args) { + if (arg == lhs) { + tt.Add(xHeapOF); + } else { + tt.Add(argsEtran.TrExpr(arg)); } } - r = Expression.CreateAnd(r, c); - } - if (G != null) { - var jIsK = Expression.CreateEq(Expression.CreateIdentExpr(j), F, j.Type); - var rr = Substitute(r, i, G); - yield return new ForallStmtTranslationValues(Expression.CreateAnd(rr, jIsK), G); - } - } else if (F is IdentifierExpr) { - var e = (IdentifierExpr)F; - if (e.Var == i) { - // We're looking at R(i) && j == i, which is particularly easy to invert: R(j) && j == i - var jj = Expression.CreateIdentExpr(j); - yield return new ForallStmtTranslationValues(Substitute(R, i, jj), jj); - } - } else if (F is BinaryExpr) { - var bin = (BinaryExpr)F; - if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Add && (bin.E0.Type.IsIntegerType || bin.E0.Type.IsRealType)) { - if (!ContainsFreeVariable(bin.E1, false, i)) { - // We're looking at: R(i) && j == f(i) + K. - // By a recursive call, we'll ask to invert: R(i) && j' == f(i). - // For each P_0(j') && f-1_0(j') == i we get back, we yield: - // P_0(j - K) && f-1_0(j - K) == i - var jMinusK = Expression.CreateSubtract(Expression.CreateIdentExpr(j), bin.E1); - foreach (var val in InvertExpression(i, j, R, bin.E0)) { - yield return val.Subst(j, jMinusK, this); - } - } else if (!ContainsFreeVariable(bin.E0, false, i)) { - // We're looking at: R(i) && j == K + f(i) - // Do as in previous case, but with operands reversed. - var jMinusK = Expression.CreateSubtract(Expression.CreateIdentExpr(j), bin.E0); - foreach (var val in InvertExpression(i, j, R, bin.E1)) { - yield return val.Subst(j, jMinusK, this); - } - } - } else if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Sub && (bin.E0.Type.IsIntegerType || bin.E0.Type.IsRealType)) { - if (!ContainsFreeVariable(bin.E1, false, i)) { - // We're looking at: R(i) && j == f(i) - K - // Recurse on f(i) and then replace j := j + K - var jPlusK = Expression.CreateAdd(Expression.CreateIdentExpr(j), bin.E1); - foreach (var val in InvertExpression(i, j, R, bin.E0)) { - yield return val.Subst(j, jPlusK, this); - } - } else if (!ContainsFreeVariable(bin.E0, false, i)) { - // We're looking at: R(i) && j == K - f(i) - // Recurse on f(i) and then replace j := K - j - var kMinusJ = Expression.CreateAdd(Expression.CreateIdentExpr(j), bin.E0); - foreach (var val in InvertExpression(i, j, R, bin.E1)) { - yield return val.Subst(j, kMinusJ, this); - } - } - } - } else if (F is ITEExpr) { - var ife = (ITEExpr)F; - // We're looking at R(i) && j == if A(i) then B(i) else C(i), which is equivalent to the disjunction of: - // R(i) && A(i) && j == B(i) - // R(i) && !A(i) && j == C(i) - // We recurse on each one, yielding the results - var r = Expression.CreateAnd(R, ife.Test); - var valsThen = InvertExpression(i, j, r, ife.Thn); - if (valsThen != null) { - r = Expression.CreateAnd(R, Expression.CreateNot(ife.tok, ife.Test)); - var valsElse = InvertExpression(i, j, r, ife.Els); - if (valsElse != null) { - foreach (var val in valsThen) { yield return val; } - foreach (var val in valsElse) { yield return val; } - } + tr = new Bpl.Trigger(tok, true, tt, tr); } } + return new Bpl.ForallExpr(tok, xBvars, tr, Bpl.Expr.Imp(xAnte, Bpl.Expr.Eq(xHeapOF, g))); } delegate Bpl.Expr ExpressionConverter(Dictionary substMap, ExpressionTranslator etran); - void TrForallStmtCall(IToken tok, List boundVars, Expression range, ExpressionConverter additionalRange, CallStmt s0, + void TrForallStmtCall(IToken tok, List boundVars, Expression range, ExpressionConverter additionalRange, List forallExpressions, CallStmt s0, Bpl.StmtListBuilder definedness, Bpl.StmtListBuilder exporter, List locals, ExpressionTranslator etran) { Contract.Requires(tok != null); Contract.Requires(boundVars != null); @@ -8365,38 +8184,56 @@ namespace Microsoft.Dafny { RecordNewObjectsIn_New(tok, iter, initHeap, heapIdExpr, exporter, locals, etran); } - var bvars = new List(); - Dictionary substMap; - var ante = initEtran.TrBoundVariablesRename(boundVars, bvars, out substMap); - ante = BplAnd(ante, initEtran.TrExpr(Substitute(range, null, substMap))); - if (additionalRange != null) { - ante = BplAnd(ante, additionalRange(substMap, initEtran)); - } - // Note, in the following, we need to do a bit of a song and dance. The actual arguments of the // call should be translated using "initEtran", whereas the method postcondition should be translated // using "callEtran". To accomplish this, we translate the argument and then tuck the resulting // Boogie expressions into BoogieExprWrappers that are used in the DafnyExpr-to-DafnyExpr substitution. - // TODO - var argsSubstMap = new Dictionary(); // maps formal arguments to actuals - Contract.Assert(s0.Method.Ins.Count == s0.Args.Count); - for (int i = 0; i < s0.Method.Ins.Count; i++) { - var arg = Substitute(s0.Args[i], null, substMap, s0.MethodSelect.TypeArgumentSubstitutions()); // substitute the renamed bound variables for the declared ones - argsSubstMap.Add(s0.Method.Ins[i], new BoogieWrapper(initEtran.TrExpr(arg), s0.Args[i].Type)); - } - var receiver = new BoogieWrapper(initEtran.TrExpr(Substitute(s0.Receiver, null, substMap, s0.MethodSelect.TypeArgumentSubstitutions())), s0.Receiver.Type); - var callEtran = new ExpressionTranslator(this, predef, etran.HeapExpr, initHeap); - Bpl.Expr post = Bpl.Expr.True; - foreach (var ens in s0.Method.Ens) { - var p = Substitute(ens.E, receiver, argsSubstMap, s0.MethodSelect.TypeArgumentSubstitutions()); // substitute the call's actuals for the method's formals - post = BplAnd(post, callEtran.TrExpr(p)); - } - - // TRIG (forall $ih#s0#0: Seq Box :: $Is($ih#s0#0, TSeq(TChar)) && $IsAlloc($ih#s0#0, TSeq(TChar), $initHeapForallStmt#0) && Seq#Length($ih#s0#0) != 0 && Seq#Rank($ih#s0#0) < Seq#Rank(s#0) ==> (forall i#2: int :: true ==> LitInt(0) <= i#2 && i#2 < Seq#Length($ih#s0#0) ==> char#ToInt(_module.CharChar.MinChar($LS($LZ), $Heap, this, $ih#s0#0)) <= char#ToInt($Unbox(Seq#Index($ih#s0#0, i#2)): char))) - // TRIG (forall $ih#pat0#0: Seq Box, $ih#a0#0: Seq Box :: $Is($ih#pat0#0, TSeq(_module._default.Same0$T)) && $IsAlloc($ih#pat0#0, TSeq(_module._default.Same0$T), $initHeapForallStmt#0) && $Is($ih#a0#0, TSeq(_module._default.Same0$T)) && $IsAlloc($ih#a0#0, TSeq(_module._default.Same0$T), $initHeapForallStmt#0) && Seq#Length($ih#pat0#0) <= Seq#Length($ih#a0#0) && Seq#SameUntil($ih#pat0#0, $ih#a0#0, Seq#Length($ih#pat0#0)) && (Seq#Rank($ih#pat0#0) < Seq#Rank(pat#0) || (Seq#Rank($ih#pat0#0) == Seq#Rank(pat#0) && Seq#Rank($ih#a0#0) < Seq#Rank(a#0))) ==> _module.__default.IsRelaxedPrefixAux(_module._default.Same0$T, $LS($LZ), $Heap, $ih#pat0#0, $ih#a0#0, LitInt(1)))' - // TRIG (forall $ih#m0#0: DatatypeType, $ih#n0#0: DatatypeType :: $Is($ih#m0#0, Tclass._module.Nat()) && $IsAlloc($ih#m0#0, Tclass._module.Nat(), $initHeapForallStmt#0) && $Is($ih#n0#0, Tclass._module.Nat()) && $IsAlloc($ih#n0#0, Tclass._module.Nat(), $initHeapForallStmt#0) && Lit(true) && (DtRank($ih#m0#0) < DtRank(m#0) || (DtRank($ih#m0#0) == DtRank(m#0) && DtRank($ih#n0#0) < DtRank(n#0))) ==> _module.__default.mult($LS($LZ), $Heap, $ih#m0#0, _module.__default.plus($LS($LZ), $Heap, $ih#n0#0, $ih#n0#0)) == _module.__default.mult($LS($LZ), $Heap, _module.__default.plus($LS($LZ), $Heap, $ih#m0#0, $ih#m0#0), $ih#n0#0)) - Bpl.Expr qq = new Bpl.ForallExpr(tok, bvars, Bpl.Expr.Imp(ante, post)); // SMART_TRIGGER - exporter.Add(new Bpl.AssumeCmd(tok, qq)); + // TODO + Bpl.Expr qq; + if (forallExpressions != null) { + var callEtran = new ExpressionTranslator(this, predef, etran.HeapExpr, initHeap); + foreach (Expression expr in forallExpressions) { + Dictionary substMap = new Dictionary(); + var e = Substitute(expr, null, substMap, null); + var argsSubstMap = new Dictionary(); + Contract.Assert(s0.Method.Ins.Count == s0.Args.Count); + for (int i = 0; i < s0.Method.Ins.Count; i++) { + var arg = Substitute(s0.Args[i], null, substMap, s0.MethodSelect.TypeArgumentSubstitutions()); // substitute the renamed bound variables for the declared ones + argsSubstMap.Add(s0.Method.Ins[i], new BoogieWrapper(initEtran.TrExpr(arg), s0.Args[i].Type)); + } + var receiver = new BoogieWrapper(initEtran.TrExpr(Substitute(s0.Receiver, null, substMap, s0.MethodSelect.TypeArgumentSubstitutions())), s0.Receiver.Type); + var p = Substitute(e, receiver, argsSubstMap, s0.MethodSelect.TypeArgumentSubstitutions()); // substitute the call's actuals for the method's formals + qq = callEtran.TrExpr(p, initEtran); + exporter.Add(new Bpl.AssumeCmd(tok, qq)); + } + } else { + var bvars = new List(); + Dictionary substMap; + var ante = initEtran.TrBoundVariablesRename(boundVars, bvars, out substMap); + var argsSubstMap = new Dictionary(); // maps formal arguments to actuals + Contract.Assert(s0.Method.Ins.Count == s0.Args.Count); + for (int i = 0; i < s0.Method.Ins.Count; i++) { + var arg = Substitute(s0.Args[i], null, substMap, s0.MethodSelect.TypeArgumentSubstitutions()); // substitute the renamed bound variables for the declared ones + argsSubstMap.Add(s0.Method.Ins[i], new BoogieWrapper(initEtran.TrExpr(arg), s0.Args[i].Type)); + } + var callEtran = new ExpressionTranslator(this, predef, etran.HeapExpr, initHeap); + ante = BplAnd(ante, initEtran.TrExpr(Substitute(range, null, substMap))); + if (additionalRange != null) { + ante = BplAnd(ante, additionalRange(substMap, initEtran)); + } + var receiver = new BoogieWrapper(initEtran.TrExpr(Substitute(s0.Receiver, null, substMap, s0.MethodSelect.TypeArgumentSubstitutions())), s0.Receiver.Type); + Bpl.Expr post = Bpl.Expr.True; + foreach (var ens in s0.Method.Ens) { + var p = Substitute(ens.E, receiver, argsSubstMap, s0.MethodSelect.TypeArgumentSubstitutions()); // substitute the call's actuals for the method's formals + post = BplAnd(post, callEtran.TrExpr(p)); + } + + // TRIG (forall $ih#s0#0: Seq Box :: $Is($ih#s0#0, TSeq(TChar)) && $IsAlloc($ih#s0#0, TSeq(TChar), $initHeapForallStmt#0) && Seq#Length($ih#s0#0) != 0 && Seq#Rank($ih#s0#0) < Seq#Rank(s#0) ==> (forall i#2: int :: true ==> LitInt(0) <= i#2 && i#2 < Seq#Length($ih#s0#0) ==> char#ToInt(_module.CharChar.MinChar($LS($LZ), $Heap, this, $ih#s0#0)) <= char#ToInt($Unbox(Seq#Index($ih#s0#0, i#2)): char))) + // TRIG (forall $ih#pat0#0: Seq Box, $ih#a0#0: Seq Box :: $Is($ih#pat0#0, TSeq(_module._default.Same0$T)) && $IsAlloc($ih#pat0#0, TSeq(_module._default.Same0$T), $initHeapForallStmt#0) && $Is($ih#a0#0, TSeq(_module._default.Same0$T)) && $IsAlloc($ih#a0#0, TSeq(_module._default.Same0$T), $initHeapForallStmt#0) && Seq#Length($ih#pat0#0) <= Seq#Length($ih#a0#0) && Seq#SameUntil($ih#pat0#0, $ih#a0#0, Seq#Length($ih#pat0#0)) && (Seq#Rank($ih#pat0#0) < Seq#Rank(pat#0) || (Seq#Rank($ih#pat0#0) == Seq#Rank(pat#0) && Seq#Rank($ih#a0#0) < Seq#Rank(a#0))) ==> _module.__default.IsRelaxedPrefixAux(_module._default.Same0$T, $LS($LZ), $Heap, $ih#pat0#0, $ih#a0#0, LitInt(1)))' + // TRIG (forall $ih#m0#0: DatatypeType, $ih#n0#0: DatatypeType :: $Is($ih#m0#0, Tclass._module.Nat()) && $IsAlloc($ih#m0#0, Tclass._module.Nat(), $initHeapForallStmt#0) && $Is($ih#n0#0, Tclass._module.Nat()) && $IsAlloc($ih#n0#0, Tclass._module.Nat(), $initHeapForallStmt#0) && Lit(true) && (DtRank($ih#m0#0) < DtRank(m#0) || (DtRank($ih#m0#0) == DtRank(m#0) && DtRank($ih#n0#0) < DtRank(n#0))) ==> _module.__default.mult($LS($LZ), $Heap, $ih#m0#0, _module.__default.plus($LS($LZ), $Heap, $ih#n0#0, $ih#n0#0)) == _module.__default.mult($LS($LZ), $Heap, _module.__default.plus($LS($LZ), $Heap, $ih#m0#0, $ih#m0#0), $ih#n0#0)) + qq = new Bpl.ForallExpr(tok, bvars, Bpl.Expr.Imp(ante, post)); // SMART_TRIGGER + exporter.Add(new Bpl.AssumeCmd(tok, qq)); + } } } @@ -8501,24 +8338,14 @@ namespace Microsoft.Dafny { } } - var bvars = new List(); - Dictionary substMap; - var ante = initEtran.TrBoundVariablesRename(s.BoundVars, bvars, out substMap); - var range = Substitute(s.Range, null, substMap); - ante = BplAnd(ante, initEtran.TrExpr(range)); - - Bpl.Expr post = Bpl.Expr.True; - foreach (var ens in s.Ens) { - var p = Substitute(ens.E, null, substMap); - post = BplAnd(post, etran.TrExpr(p)); - } - - Bpl.Expr qq = Bpl.Expr.Imp(ante, post); - if (bvars.Count != 0) { - var triggers = TrTrigger(etran, s.Attributes, s.Tok, substMap); - qq = new Bpl.ForallExpr(s.Tok, bvars, triggers, qq); + Dictionary substMap = new Dictionary(); + var p = Substitute(s.ForallExpressions[0], null, substMap); + Bpl.Expr qq = etran.TrExpr(p, initEtran); + if (s.BoundVars.Count != 0) { + exporter.Add(new Bpl.AssumeCmd(s.Tok, qq)); + } else { + exporter.Add(new Bpl.AssumeCmd(s.Tok, ((Bpl.ForallExpr)qq).Body)); } - exporter.Add(new Bpl.AssumeCmd(s.Tok, qq)); } private string GetObjFieldDetails(Expression lhs, ExpressionTranslator etran, out Bpl.Expr obj, out Bpl.Expr F) { @@ -10868,7 +10695,10 @@ namespace Microsoft.Dafny { /// filled in, but it is really necessary for anything that may show up in a Boogie assert, since that location may /// then show up in an error message). /// - public Bpl.Expr TrExpr(Expression expr) + public Bpl.Expr TrExpr(Expression expr) { + return TrExpr(expr, null); + } + public Bpl.Expr TrExpr(Expression expr, ExpressionTranslator etran) { Contract.Requires(expr != null); Contract.Requires(predef != null); @@ -11683,7 +11513,7 @@ namespace Microsoft.Dafny { List tyvars = translator.MkTyParamBinders(e.TypeArgs); List bvars = new List(); - var initEtran = this; + var initEtran = (etran == null) ? this : etran; var bodyEtran = this; bool _scratch = true; @@ -11704,7 +11534,7 @@ namespace Microsoft.Dafny { }); } - antecedent = BplAnd(antecedent, bodyEtran.TrBoundVariables(e.BoundVars, bvars)); + antecedent = BplAnd(antecedent, initEtran.TrBoundVariables(e.BoundVars, bvars)); Bpl.QKeyValue kv = TrAttributes(e.Attributes, "trigger"); Bpl.Trigger tr = null; @@ -11719,7 +11549,7 @@ namespace Microsoft.Dafny { } } if (e.Range != null) { - antecedent = BplAnd(antecedent, bodyEtran.TrExpr(e.Range)); + antecedent = BplAnd(antecedent, initEtran.TrExpr(e.Range)); } Bpl.Expr body = bodyEtran.TrExpr(e.Term); diff --git a/Source/Dafny/Triggers/QuantifierSplitter.cs b/Source/Dafny/Triggers/QuantifierSplitter.cs index 865aa33e..e46b64fb 100644 --- a/Source/Dafny/Triggers/QuantifierSplitter.cs +++ b/Source/Dafny/Triggers/QuantifierSplitter.cs @@ -114,6 +114,18 @@ namespace Microsoft.Dafny.Triggers { } } + protected override void VisitOneStmt(Statement stmt) { + Contract.Requires(stmt != null); + if (stmt is ForallStmt) { + ForallStmt s = (ForallStmt)stmt; + if (s.ForallExpressions != null) { + foreach (Expression expr in s.ForallExpressions) { + VisitOneExpr(expr); + } + } + } + } + /// /// See comments above definition of splits for reason why this method exists /// diff --git a/Source/Dafny/Triggers/QuantifiersCollector.cs b/Source/Dafny/Triggers/QuantifiersCollector.cs index 1f37dcfa..789e7614 100644 --- a/Source/Dafny/Triggers/QuantifiersCollector.cs +++ b/Source/Dafny/Triggers/QuantifiersCollector.cs @@ -40,5 +40,18 @@ namespace Microsoft.Dafny.Triggers { return true; } + + protected override bool VisitOneStmt(Statement stmt, ref bool st) { + Contract.Requires(stmt != null); + if (stmt is ForallStmt) { + ForallStmt s = (ForallStmt)stmt; + if (s.ForallExpressions != null) { + foreach (Expression expr in s.ForallExpressions) { + VisitOneExpr(expr, ref st); + } + } + } + return true; + } } } diff --git a/Test/dafny0/SmallTests.dfy.expect b/Test/dafny0/SmallTests.dfy.expect index 4bd12096..6161c3dd 100644 --- a/Test/dafny0/SmallTests.dfy.expect +++ b/Test/dafny0/SmallTests.dfy.expect @@ -1,3 +1,4 @@ +SmallTests.dfy(507,4): Warning: /!\ No trigger covering all quantified variables found. SmallTests.dfy(34,10): Error: index out of range Execution trace: (0,0): anon0 diff --git a/Test/dafny4/Bug103.dfy b/Test/dafny4/Bug103.dfy new file mode 100644 index 00000000..559a361c --- /dev/null +++ b/Test/dafny4/Bug103.dfy @@ -0,0 +1,20 @@ +// RUN: %dafny /compile:0 /autoTriggers:1 /print:"%t.print" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +predicate IsLessThanSuccesor(i:int) +{ + i < i + 1 +} + +lemma LemmaWithoutTriggerOnForallStatement() +{ + forall i + ensures IsLessThanSuccesor(i); + { + } +} + + + + + diff --git a/Test/dafny4/Bug103.dfy.expect b/Test/dafny4/Bug103.dfy.expect new file mode 100644 index 00000000..52595bf9 --- /dev/null +++ b/Test/dafny4/Bug103.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 3 verified, 0 errors -- cgit v1.2.3