From 31ec9bc299901a1a85abbd091c3293af00354030 Mon Sep 17 00:00:00 2001 From: qunyanm Date: Thu, 31 Mar 2016 09:10:34 -0700 Subject: Fix issue 75. Adjust the fuel for existentials to use more fuel in an assume context and less in an assert. --- Source/Dafny/DafnyAst.cs | 37 ++++++++++- Source/Dafny/Resolver.cs | 1 + Source/Dafny/Translator.cs | 151 +++++++++++++++++++++++-------------------- Test/dafny4/Bug75.dfy | 50 ++++++++++++++ Test/dafny4/Bug75.dfy.expect | 2 + 5 files changed, 169 insertions(+), 72 deletions(-) create mode 100644 Test/dafny4/Bug75.dfy create mode 100644 Test/dafny4/Bug75.dfy.expect diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 0e4c4751..ab1a411a 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -2375,6 +2375,7 @@ namespace Microsoft.Dafny { bool MustReverify { get; } string FullSanitizedName { get; } bool AllowsNontermination { get; } + bool ContainsQuantifier { get; set; } } /// /// An ICallable is a Function, Method, IteratorDecl, or RedirectingTypeDecl. @@ -2392,6 +2393,7 @@ namespace Microsoft.Dafny { /// bool InferredDecreases { get; set; } } + public class DontUseICallable : ICallable { public string WhatKind { get { throw new cce.UnreachableException(); } } @@ -2409,6 +2411,10 @@ namespace Microsoft.Dafny { get { throw new cce.UnreachableException(); } set { throw new cce.UnreachableException(); } } + public bool ContainsQuantifier { + get { throw new cce.UnreachableException(); } + set { throw new cce.UnreachableException(); } + } } /// /// An IMethodCodeContext is a Method or IteratorDecl. @@ -2437,6 +2443,11 @@ namespace Microsoft.Dafny { bool ICodeContext.MustReverify { get { Contract.Assume(false, "should not be called on NoContext"); throw new cce.UnreachableException(); } } public string FullSanitizedName { get { Contract.Assume(false, "should not be called on NoContext"); throw new cce.UnreachableException(); } } public bool AllowsNontermination { get { Contract.Assume(false, "should not be called on NoContext"); throw new cce.UnreachableException(); } } + public bool ContainsQuantifier { + get { Contract.Assume(false, "should not be called on NoContext"); throw new cce.UnreachableException(); } + set { Contract.Assume(false, "should not be called on NoContext"); throw new cce.UnreachableException(); } + } + } public class IteratorDecl : ClassDecl, IMethodCodeContext @@ -2464,6 +2475,8 @@ namespace Microsoft.Dafny { public Predicate Member_Valid; // created during registration phase of resolution; its specification is filled in during resolution public Method Member_MoveNext; // created during registration phase of resolution; its specification is filled in during resolution public readonly LocalVariable YieldCountVariable; + bool containsQuantifier; + public IteratorDecl(IToken tok, string name, ModuleDefinition module, List typeArgs, List ins, List outs, Specification reads, Specification mod, Specification decreases, @@ -2579,6 +2592,10 @@ namespace Microsoft.Dafny { set { _inferredDecr = value; } get { return _inferredDecr; } } + bool ICodeContext.ContainsQuantifier { + set { containsQuantifier = value; } + get { return containsQuantifier; } + } ModuleDefinition ICodeContext.EnclosingModule { get { return this.Module; } } bool ICodeContext.MustReverify { get { return false; } } public bool AllowsNontermination { @@ -2832,7 +2849,10 @@ namespace Microsoft.Dafny { get { throw new cce.UnreachableException(); } // see comment above about ICallable.Decreases set { throw new cce.UnreachableException(); } // see comment above about ICallable.Decreases } - + bool ICodeContext.ContainsQuantifier { + get { throw new cce.UnreachableException(); } + set { throw new cce.UnreachableException(); } + } public new NewtypeDecl ClonedFrom { get { return (NewtypeDecl)base.ClonedFrom; @@ -2890,6 +2910,10 @@ namespace Microsoft.Dafny { get { throw new cce.UnreachableException(); } // see comment above about ICallable.Decreases set { throw new cce.UnreachableException(); } // see comment above about ICallable.Decreases } + bool ICodeContext.ContainsQuantifier { + get { throw new cce.UnreachableException(); } + set { throw new cce.UnreachableException(); } + } } [ContractClass(typeof(IVariableContracts))] @@ -3184,6 +3208,11 @@ namespace Microsoft.Dafny { public readonly IToken SignatureEllipsis; public bool IsBuiltin; public Function OverriddenFunction; + public bool containsQuantifier; + public bool ContainsQuantifier { + set { containsQuantifier = value; } + get { return containsQuantifier; } + } public override IEnumerable SubExpressions { get { @@ -3438,6 +3467,7 @@ namespace Microsoft.Dafny { public bool IsTailRecursive; // filled in during resolution public readonly ISet AssignedAssumptionVariables = new HashSet(); public Method OverriddenMethod; + public bool containsQuantifier; public override IEnumerable SubExpressions { get { @@ -3512,6 +3542,11 @@ namespace Microsoft.Dafny { set { _inferredDecr = value; } get { return _inferredDecr; } } + bool ICodeContext.ContainsQuantifier { + set { containsQuantifier = value; } + get { return containsQuantifier; } + } + ModuleDefinition ICodeContext.EnclosingModule { get { Contract.Assert(this.EnclosingClass != null); // this getter is supposed to be called only after signature-resolution is complete diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index aa9ce148..b6e783b4 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -8173,6 +8173,7 @@ namespace Microsoft.Dafny e.Type = e.Body.Type; } else if (expr is QuantifierExpr) { var e = (QuantifierExpr)expr; + opts.codeContext.ContainsQuantifier = true; Contract.Assert(e.SplitQuantifier == null); // No split quantifiers during resolution int prevErrorCount = reporter.Count(ErrorLevel.Error); bool _val = true; diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 9466f18a..b2b63a07 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -7232,7 +7232,9 @@ namespace Microsoft.Dafny { AddComment(builder, stmt, "assume statement"); AssumeStmt s = (AssumeStmt)stmt; TrStmt_CheckWellformed(s.Expr, builder, locals, etran, false); - builder.Add(TrAssumeCmd(stmt.Tok, etran.TrExpr(s.Expr), etran.TrAttributes(stmt.Attributes, null))); + // we need to increase fuel for quantifier expr and functions that contain quantifier expr in the assume context. + var existEtran = etran.LayerOffset(1); + builder.Add(TrAssumeCmd(stmt.Tok, etran.TrExpr(s.Expr, null, existEtran, existEtran), etran.TrAttributes(stmt.Attributes, null))); } this.fuelContext = FuelSetting.PopFuelContext(); } else if (stmt is PrintStmt) { @@ -8348,7 +8350,7 @@ namespace Microsoft.Dafny { } 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); + qq = callEtran.TrExpr(p, initEtran, null, null); exporter.Add(TrAssumeCmd(tok, qq)); } } else { @@ -8485,7 +8487,7 @@ namespace Microsoft.Dafny { Dictionary substMap = new Dictionary(); var p = Substitute(s.ForallExpressions[0], null, substMap); - Bpl.Expr qq = etran.TrExpr(p, initEtran); + Bpl.Expr qq = etran.TrExpr(p, initEtran, null, null); if (s.BoundVars.Count != 0) { exporter.Add(TrAssumeCmd(s.Tok, qq)); } else { @@ -10916,9 +10918,9 @@ namespace Microsoft.Dafny { /// then show up in an error message). /// public Bpl.Expr TrExpr(Expression expr) { - return TrExpr(expr, null); + return TrExpr(expr, null, null, null); } - public Bpl.Expr TrExpr(Expression expr, ExpressionTranslator etran) + public Bpl.Expr TrExpr(Expression expr, ExpressionTranslator initEtran, ExpressionTranslator funcEtran, ExpressionTranslator existEtran) { Contract.Requires(expr != null); Contract.Requires(predef != null); @@ -10982,7 +10984,7 @@ namespace Microsoft.Dafny { args.Add(Old.HeapExpr); } foreach (var arg in e.Args) { - args.Add(TrExpr(arg)); + args.Add(TrExpr(arg, initEtran, funcEtran, existEtran)); } return new Bpl.NAryExpr(e.tok, new Bpl.FunctionCall(id), args); @@ -10990,7 +10992,7 @@ namespace Microsoft.Dafny { SetDisplayExpr e = (SetDisplayExpr)expr; Bpl.Expr s = translator.FunctionCall(expr.tok, e.Finite ? BuiltinFunction.SetEmpty : BuiltinFunction.ISetEmpty, predef.BoxType); foreach (Expression ee in e.Elements) { - Bpl.Expr ss = BoxIfNecessary(expr.tok, TrExpr(ee), cce.NonNull(ee.Type)); + Bpl.Expr ss = BoxIfNecessary(expr.tok, TrExpr(ee, initEtran, funcEtran, existEtran), cce.NonNull(ee.Type)); s = translator.FunctionCall(expr.tok, e.Finite ? BuiltinFunction.SetUnionOne : BuiltinFunction.ISetUnionOne, predef.BoxType, s, ss); } return s; @@ -10999,7 +11001,7 @@ namespace Microsoft.Dafny { MultiSetDisplayExpr e = (MultiSetDisplayExpr)expr; Bpl.Expr s = translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetEmpty, predef.BoxType); foreach (Expression ee in e.Elements) { - Bpl.Expr ss = BoxIfNecessary(expr.tok, TrExpr(ee), cce.NonNull(ee.Type)); + Bpl.Expr ss = BoxIfNecessary(expr.tok, TrExpr(ee, initEtran, funcEtran, existEtran), cce.NonNull(ee.Type)); s = translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetUnionOne, predef.BoxType, s, ss); } return s; @@ -11010,7 +11012,7 @@ namespace Microsoft.Dafny { Bpl.Expr s = translator.FunctionCall(expr.tok, BuiltinFunction.SeqEmpty, predef.BoxType); bool isLit = true; foreach (Expression ee in e.Elements) { - var rawElement = TrExpr(ee); + var rawElement = TrExpr(ee, initEtran, funcEtran, existEtran); isLit = isLit && translator.IsLit(rawElement); Bpl.Expr elt = BoxIfNecessary(expr.tok, rawElement, ee.Type); s = translator.FunctionCall(expr.tok, BuiltinFunction.SeqBuild, predef.BoxType, s, elt); @@ -11026,8 +11028,8 @@ namespace Microsoft.Dafny { Bpl.Type maptype = predef.MapType(expr.tok, e.Finite, predef.BoxType, predef.BoxType); Bpl.Expr s = translator.FunctionCall(expr.tok, e.Finite ? BuiltinFunction.MapEmpty : BuiltinFunction.IMapEmpty, predef.BoxType); foreach (ExpressionPair p in e.Elements) { - Bpl.Expr elt = BoxIfNecessary(expr.tok, TrExpr(p.A), cce.NonNull(p.A.Type)); - Bpl.Expr elt2 = BoxIfNecessary(expr.tok, TrExpr(p.B), cce.NonNull(p.B.Type)); + Bpl.Expr elt = BoxIfNecessary(expr.tok, TrExpr(p.A, initEtran, funcEtran, existEtran), cce.NonNull(p.A.Type)); + Bpl.Expr elt2 = BoxIfNecessary(expr.tok, TrExpr(p.B, initEtran, funcEtran, existEtran), cce.NonNull(p.B.Type)); s = translator.FunctionCall(expr.tok, e.Finite ? "Map#Build" : "IMap#Build", maptype, s, elt, elt2); } return s; @@ -11036,7 +11038,7 @@ namespace Microsoft.Dafny { var e = (MemberSelectExpr)expr; return e.MemberSelectCase( field => { - Bpl.Expr obj = TrExpr(e.Obj); + Bpl.Expr obj = TrExpr(e.Obj, initEtran, funcEtran, existEtran); Bpl.Expr result; if (field.IsMutable) { result = ReadHeap(expr.tok, HeapExpr, obj, new Bpl.IdentifierExpr(expr.tok, translator.GetField(field))); @@ -11063,7 +11065,7 @@ namespace Microsoft.Dafny { }); } else if (expr is SeqSelectExpr) { SeqSelectExpr e = (SeqSelectExpr)expr; - Bpl.Expr seq = TrExpr(e.Seq); + Bpl.Expr seq = TrExpr(e.Seq, initEtran, funcEtran, existEtran); var seqType = e.Seq.Type.NormalizeExpand(); Type elmtType = null; Type domainType = null; @@ -11083,14 +11085,14 @@ namespace Microsoft.Dafny { } else { Contract.Assert(false); } Bpl.Type elType = translator.TrType(elmtType); Bpl.Type dType = translator.TrType(domainType); - Bpl.Expr e0 = e.E0 == null ? null : TrExpr(e.E0); - Bpl.Expr e1 = e.E1 == null ? null : TrExpr(e.E1); + Bpl.Expr e0 = e.E0 == null ? null : TrExpr(e.E0, initEtran, funcEtran, existEtran); + Bpl.Expr e1 = e.E1 == null ? null : TrExpr(e.E1, initEtran, funcEtran, existEtran); if (e.SelectOne) { Contract.Assert(e1 == null); Bpl.Expr x; if (seqType.IsArrayType) { Bpl.Expr fieldName = translator.FunctionCall(expr.tok, BuiltinFunction.IndexField, null, e0); - x = ReadHeap(expr.tok, HeapExpr, TrExpr(e.Seq), fieldName); + x = ReadHeap(expr.tok, HeapExpr, TrExpr(e.Seq, initEtran, funcEtran, existEtran), fieldName); } else if (seqType is SeqType) { x = translator.FunctionCall(expr.tok, BuiltinFunction.SeqIndex, predef.BoxType, seq, e0); } else if (seqType is MapType) { @@ -11099,7 +11101,7 @@ namespace Microsoft.Dafny { x = translator.FunctionCall(expr.tok, f, predef.MapType(e.tok, finite, predef.BoxType, predef.BoxType), seq); x = Bpl.Expr.Select(x, BoxIfNecessary(e.tok, e0, domainType)); } else if (seqType is MultiSetType) { - x = Bpl.Expr.SelectTok(expr.tok, TrExpr(e.Seq), BoxIfNecessary(expr.tok, e0, domainType)); + x = Bpl.Expr.SelectTok(expr.tok, TrExpr(e.Seq, initEtran, funcEtran, existEtran), BoxIfNecessary(expr.tok, e0, domainType)); } else { Contract.Assert(false); x = null; } if (!ModeledAsBoxType(elmtType) && !(seqType is MultiSetType)) { x = translator.FunctionCall(expr.tok, BuiltinFunction.Unbox, elType, x); @@ -11130,32 +11132,32 @@ namespace Microsoft.Dafny { SeqUpdateExpr e = (SeqUpdateExpr)expr; if (e.ResolvedUpdateExpr != null) { - return TrExpr(e.ResolvedUpdateExpr); + return TrExpr(e.ResolvedUpdateExpr, initEtran, funcEtran, existEtran); } else { - Bpl.Expr seq = TrExpr(e.Seq); + Bpl.Expr seq = TrExpr(e.Seq, initEtran, funcEtran, existEtran); var seqType = e.Seq.Type.NormalizeExpand(); if (seqType is SeqType) { Type elmtType = cce.NonNull((SeqType)seqType).Arg; - Bpl.Expr index = TrExpr(e.Index); - Bpl.Expr val = BoxIfNecessary(expr.tok, TrExpr(e.Value), elmtType); + Bpl.Expr index = TrExpr(e.Index, initEtran, funcEtran, existEtran); + Bpl.Expr val = BoxIfNecessary(expr.tok, TrExpr(e.Value, initEtran, funcEtran, existEtran), elmtType); return translator.FunctionCall(expr.tok, BuiltinFunction.SeqUpdate, predef.BoxType, seq, index, val); } else if (seqType is MapType) { MapType mt = (MapType)seqType; Bpl.Type maptype = predef.MapType(expr.tok, mt.Finite, predef.BoxType, predef.BoxType); - Bpl.Expr index = BoxIfNecessary(expr.tok, TrExpr(e.Index), mt.Domain); - Bpl.Expr val = BoxIfNecessary(expr.tok, TrExpr(e.Value), mt.Range); + Bpl.Expr index = BoxIfNecessary(expr.tok, TrExpr(e.Index, initEtran, funcEtran, existEtran), mt.Domain); + Bpl.Expr val = BoxIfNecessary(expr.tok, TrExpr(e.Value, initEtran, funcEtran, existEtran), mt.Range); return translator.FunctionCall(expr.tok, mt.Finite ? "Map#Build" : "IMap#Build", maptype, seq, index, val); } else if (seqType is MultiSetType) { Type elmtType = cce.NonNull((MultiSetType)seqType).Arg; - Bpl.Expr index = BoxIfNecessary(expr.tok, TrExpr(e.Index), elmtType); - Bpl.Expr val = TrExpr(e.Value); + Bpl.Expr index = BoxIfNecessary(expr.tok, TrExpr(e.Index, initEtran, funcEtran, existEtran), elmtType); + Bpl.Expr val = TrExpr(e.Value, initEtran, funcEtran, existEtran); return Bpl.Expr.StoreTok(expr.tok, seq, index, val); } else @@ -11171,7 +11173,7 @@ namespace Microsoft.Dafny { Bpl.Type elType = translator.TrType(elmtType); Bpl.Expr fieldName = GetArrayIndexFieldName(expr.tok, e.Indices); - Bpl.Expr x = ReadHeap(expr.tok, HeapExpr, TrExpr(e.Array), fieldName); + Bpl.Expr x = ReadHeap(expr.tok, HeapExpr, TrExpr(e.Array, initEtran, funcEtran, existEtran), fieldName); if (!ModeledAsBoxType(elmtType)) { x = translator.FunctionCall(expr.tok, BuiltinFunction.Unbox, elType, x); } @@ -11195,30 +11197,34 @@ namespace Microsoft.Dafny { Function = fn, Type = e.Type, TypeArgumentSubstitutions = Util.Dict(GetTypeParams(fn), mem.TypeApplication) - }); + }, initEtran, funcEtran, existEtran); } } - Func TrArg = arg => translator.BoxIfUnboxed(TrExpr(arg), arg.Type); + Func TrArg = arg => translator.BoxIfUnboxed(TrExpr(arg, initEtran, funcEtran, existEtran), arg.Type); var applied = translator.FunctionCall(expr.tok, translator.Apply(arity), predef.BoxType, Concat(Map(tt.TypeArgs,translator.TypeToTy), - Cons(TrExpr(e.Function), Cons(HeapExpr, e.Args.ConvertAll(arg => TrArg(arg)))))); + Cons(TrExpr(e.Function, initEtran, funcEtran, existEtran), Cons(HeapExpr, e.Args.ConvertAll(arg => TrArg(arg)))))); return translator.UnboxIfBoxed(applied, tt.Result); } else if (expr is FunctionCallExpr) { FunctionCallExpr e = (FunctionCallExpr)expr; Bpl.Expr layerArgument; + var etran = this; + if (e.Function.ContainsQuantifier && funcEtran != null) { + etran = funcEtran; + } if (e.Function.IsFuelAware()) { Statistics_CustomLayerFunctionCount++; ModuleDefinition module = e.Function.EnclosingClass.Module; - if (this.applyLimited_CurrentFunction != null && - this.layerIntraCluster != null && + if (etran.applyLimited_CurrentFunction != null && + etran.layerIntraCluster != null && ModuleDefinition.InSameSCC(e.Function, applyLimited_CurrentFunction)) { - layerArgument = this.layerIntraCluster.GetFunctionFuel(e.Function); + layerArgument = etran.layerIntraCluster.GetFunctionFuel(e.Function); } else { - layerArgument = this.layerInterCluster.GetFunctionFuel(e.Function); + layerArgument = etran.layerInterCluster.GetFunctionFuel(e.Function); } } else { layerArgument = null; @@ -11253,7 +11259,7 @@ namespace Microsoft.Dafny { for (int i = 0; i < dtv.Arguments.Count; i++) { Expression arg = dtv.Arguments[i]; Type t = dtv.Ctor.Formals[i].Type; - var bArg = TrExpr(arg); + var bArg = TrExpr(arg, initEtran, funcEtran, existEtran); argsAreLit = argsAreLit && translator.IsLit(bArg); args.Add(translator.CondApplyBox(expr.tok, bArg, cce.NonNull(arg.Type), t)); } @@ -11266,7 +11272,7 @@ namespace Microsoft.Dafny { return ret; } else if (expr is OldExpr) { OldExpr e = (OldExpr)expr; - return Old.TrExpr(e.E); + return Old.TrExpr(e.E, initEtran, funcEtran, existEtran); } else if (expr is MultiSetFormingExpr) { MultiSetFormingExpr e = (MultiSetFormingExpr)expr; @@ -11281,7 +11287,7 @@ namespace Microsoft.Dafny { } else if (expr is UnaryOpExpr) { var e = (UnaryOpExpr)expr; - Bpl.Expr arg = TrExpr(e.E); + Bpl.Expr arg = TrExpr(e.E, initEtran, funcEtran, existEtran); switch (e.Op) { case UnaryOpExpr.Opcode.Lit: return MaybeLit(arg); @@ -11321,8 +11327,8 @@ namespace Microsoft.Dafny { // generate: (forall $i: int :: 0 <= $i && $i < Seq#Length(X) && Unbox(Seq#Index(X,$i)) != null ==> !old($Heap)[Unbox(Seq#Index(X,$i)),alloc]) Bpl.Variable iVar = new Bpl.BoundVariable(expr.tok, new Bpl.TypedIdent(expr.tok, "$i", Bpl.Type.Int)); Bpl.Expr i = new Bpl.IdentifierExpr(expr.tok, iVar); - Bpl.Expr iBounds = translator.InSeqRange(expr.tok, i, TrExpr(e.E), true, null, false); - Bpl.Expr XsubI = translator.FunctionCall(expr.tok, BuiltinFunction.SeqIndex, predef.RefType, TrExpr(e.E), i); + Bpl.Expr iBounds = translator.InSeqRange(expr.tok, i, TrExpr(e.E, initEtran, funcEtran, existEtran), true, null, false); + Bpl.Expr XsubI = translator.FunctionCall(expr.tok, BuiltinFunction.SeqIndex, predef.RefType, TrExpr(e.E, initEtran, funcEtran, existEtran), i); XsubI = translator.FunctionCall(expr.tok, BuiltinFunction.Unbox, predef.RefType, XsubI); Bpl.Expr oNotFresh = Old.IsAlloced(expr.tok, XsubI); Bpl.Expr oIsFresh = Bpl.Expr.Not(oNotFresh); @@ -11334,12 +11340,12 @@ namespace Microsoft.Dafny { return new Bpl.ForallExpr(expr.tok, new List { iVar }, body); } else if (eeType.IsDatatype) { // translator.FunctionCall(e.tok, BuiltinFunction.DtAlloc, null, TrExpr(e.E), Old.HeapExpr); - Bpl.Expr alloc = translator.MkIsAlloc(TrExpr(e.E), eeType, Old.HeapExpr); + Bpl.Expr alloc = translator.MkIsAlloc(TrExpr(e.E, initEtran, funcEtran, existEtran), eeType, Old.HeapExpr); return Bpl.Expr.Unary(expr.tok, UnaryOperator.Opcode.Not, alloc); } else { // generate: x != null && !old($Heap)[x] - Bpl.Expr oNull = Bpl.Expr.Neq(TrExpr(e.E), predef.Null); - Bpl.Expr oIsFresh = Bpl.Expr.Not(Old.IsAlloced(expr.tok, TrExpr(e.E))); + Bpl.Expr oNull = Bpl.Expr.Neq(TrExpr(e.E, initEtran, funcEtran, existEtran), predef.Null); + Bpl.Expr oIsFresh = Bpl.Expr.Not(Old.IsAlloced(expr.tok, TrExpr(e.E, initEtran, funcEtran, existEtran))); return Bpl.Expr.Binary(expr.tok, BinaryOperator.Opcode.And, oNull, oIsFresh); } default: @@ -11359,14 +11365,14 @@ namespace Microsoft.Dafny { ct = BuiltinFunction.RealToInt; } else { Contract.Assert(fromInt == toInt); - return TrExpr(e.E); + return TrExpr(e.E, initEtran, funcEtran, existEtran); } - return translator.FunctionCall(e.tok, ct, null, TrExpr(e.E)); + return translator.FunctionCall(e.tok, ct, null, TrExpr(e.E, initEtran, funcEtran, existEtran)); } else if (expr is BinaryExpr) { BinaryExpr e = (BinaryExpr)expr; bool isReal = e.E0.Type.IsNumericBased(Type.NumericPersuation.Real); - Bpl.Expr e0 = TrExpr(e.E0); + Bpl.Expr e0 = TrExpr(e.E0, initEtran, funcEtran, existEtran); if (e.ResolvedOp == BinaryExpr.ResolvedOpcode.InSet) { return TrInSet(expr.tok, e0, e.E1, cce.NonNull(e.E0.Type)); // let TrInSet translate e.E1 } else if (e.ResolvedOp == BinaryExpr.ResolvedOpcode.NotInSet) { @@ -11378,7 +11384,7 @@ namespace Microsoft.Dafny { Bpl.Expr arg = TrInMultiSet(expr.tok, e0, e.E1, cce.NonNull(e.E0.Type)); // let TrInMultiSet translate e.E1 return Bpl.Expr.Unary(expr.tok, UnaryOperator.Opcode.Not, arg); } - Bpl.Expr e1 = TrExpr(e.E1); + Bpl.Expr e1 = TrExpr(e.E1, initEtran, funcEtran, existEtran); BinaryOperator.Opcode bOpcode; Bpl.Type typ; var oe0 = e0; @@ -11695,9 +11701,9 @@ namespace Microsoft.Dafny { return re; } else if (expr is TernaryExpr) { var e = (TernaryExpr)expr; - var e0 = TrExpr(e.E0); - var e1 = TrExpr(e.E1); - var e2 = TrExpr(e.E2); + var e0 = TrExpr(e.E0, initEtran, funcEtran, existEtran); + var e1 = TrExpr(e.E1, initEtran, funcEtran, existEtran); + var e2 = TrExpr(e.E2, initEtran, funcEtran, existEtran); switch (e.Op) { case TernaryExpr.Opcode.PrefixEqOp: case TernaryExpr.Opcode.PrefixNeqOp: @@ -11717,24 +11723,25 @@ namespace Microsoft.Dafny { } else if (expr is LetExpr) { var e = (LetExpr)expr; if (e.Exact) { - return TrExpr(GetSubstitutedBody(e)); + return TrExpr(GetSubstitutedBody(e), initEtran, funcEtran, existEtran); } else { var d = translator.LetDesugaring(e); - return TrExpr(d); + return TrExpr(d, initEtran, funcEtran, existEtran); } } else if (expr is NamedExpr) { - return TrExpr(((NamedExpr)expr).Body); + return TrExpr(((NamedExpr)expr).Body, initEtran, funcEtran, existEtran); } else if (expr is QuantifierExpr) { QuantifierExpr e = (QuantifierExpr)expr; if (e.SplitQuantifier != null) { - return TrExpr(e.SplitQuantifierExpression); + return TrExpr(e.SplitQuantifierExpression, initEtran, existEtran, existEtran); } else { List tyvars = translator.MkTyParamBinders(e.TypeArgs); List bvars = new List(); - var initEtran = (etran == null) ? this : etran; + var etran = initEtran ?? this; var bodyEtran = this; + existEtran = e is ForallExpr ? this : existEtran; bool _scratch = true; Bpl.Expr antecedent = Bpl.Expr.True; @@ -11750,11 +11757,11 @@ namespace Microsoft.Dafny { antecedent = BplAnd(new List { antecedent, translator.FunctionCall(e.tok, BuiltinFunction.IsGoodHeap, null, h), - translator.HeapSameOrSucc(initEtran.HeapExpr, h) + translator.HeapSameOrSucc(etran.HeapExpr, h) }); } - antecedent = BplAnd(antecedent, initEtran.TrBoundVariables(e.BoundVars, bvars)); + antecedent = BplAnd(antecedent, etran.TrBoundVariables(e.BoundVars, bvars)); Bpl.QKeyValue kv = TrAttributes(e.Attributes, "trigger"); Bpl.Trigger tr = null; @@ -11763,15 +11770,15 @@ namespace Microsoft.Dafny { if (aa.Name == "trigger") { List tt = new List(); foreach (var arg in aa.Args) { - tt.Add(argsEtran.TrExpr(arg)); + tt.Add(argsEtran.TrExpr(arg, initEtran, existEtran, existEtran)); } tr = new Bpl.Trigger(expr.tok, true, tt, tr); } } if (e.Range != null) { - antecedent = BplAnd(antecedent, initEtran.TrExpr(e.Range)); + antecedent = BplAnd(antecedent, etran.TrExpr(e.Range, initEtran, existEtran, existEtran)); } - Bpl.Expr body = bodyEtran.TrExpr(e.Term); + Bpl.Expr body = bodyEtran.TrExpr(e.Term, initEtran, existEtran, existEtran); if (e is ForallExpr) { return new Bpl.ForallExpr(expr.tok, new List(), Concat(tyvars, bvars), kv, tr, Bpl.Expr.Imp(antecedent, body)); @@ -11790,8 +11797,8 @@ namespace Microsoft.Dafny { var yVar = new Bpl.BoundVariable(expr.tok, new Bpl.TypedIdent(expr.tok, translator.CurrentIdGenerator.FreshId("$y#"), predef.BoxType)); Bpl.Expr y = new Bpl.IdentifierExpr(expr.tok, yVar); - var eq = Bpl.Expr.Eq(y, BoxIfNecessary(expr.tok, TrExpr(e.Term), e.Term.Type)); - var ebody = Bpl.Expr.And(BplAnd(typeAntecedent, TrExpr(e.Range)), eq); + var eq = Bpl.Expr.Eq(y, BoxIfNecessary(expr.tok, TrExpr(e.Term, initEtran, funcEtran, existEtran), e.Term.Type)); + var ebody = Bpl.Expr.And(BplAnd(typeAntecedent, TrExpr(e.Range, initEtran, funcEtran, existEtran)), eq); var triggers = translator.TrTrigger(this, e.Attributes, e.tok); var exst = new Bpl.ExistsExpr(expr.tok, bvars, triggers, ebody); @@ -11818,9 +11825,9 @@ namespace Microsoft.Dafny { Dictionary subst = new Dictionary(); subst.Add(e.BoundVars[0], new BoogieWrapper(unboxy,e.BoundVars[0].Type)); - var ebody = BplAnd(typeAntecedent ?? Bpl.Expr.True, TrExpr(translator.Substitute(e.Range, null, subst))); + var ebody = BplAnd(typeAntecedent ?? Bpl.Expr.True, TrExpr(translator.Substitute(e.Range, null, subst), initEtran, funcEtran, existEtran)); Bpl.Expr l1 = new Bpl.LambdaExpr(e.tok, new List(), new List { yVar }, kv, ebody); - ebody = TrExpr(translator.Substitute(e.Term, null, subst)); + ebody = TrExpr(translator.Substitute(e.Term, null, subst), initEtran, funcEtran, existEtran); Bpl.Expr l2 = new Bpl.LambdaExpr(e.tok, new List(), new List { yVar }, kv, BoxIfNecessary(expr.tok, ebody, e.Term.Type)); bool finite = e.Finite; @@ -11833,31 +11840,31 @@ namespace Microsoft.Dafny { } else if (expr is StmtExpr) { var e = (StmtExpr)expr; - return TrExpr(e.E); + return TrExpr(e.E, initEtran, funcEtran, existEtran); } else if (expr is ITEExpr) { ITEExpr e = (ITEExpr)expr; - var g = translator.RemoveLit(TrExpr(e.Test)); - var thn = translator.RemoveLit(TrExpr(e.Thn)); - var els = translator.RemoveLit(TrExpr(e.Els)); + var g = translator.RemoveLit(TrExpr(e.Test, initEtran, funcEtran, existEtran)); + var thn = translator.RemoveLit(TrExpr(e.Thn, initEtran, funcEtran, existEtran)); + var els = translator.RemoveLit(TrExpr(e.Els, initEtran, funcEtran, existEtran)); return new NAryExpr(expr.tok, new IfThenElse(expr.tok), new List { g, thn, els }); } else if (expr is MatchExpr) { var e = (MatchExpr)expr; var ite = DesugarMatchExpr(e); - return TrExpr(ite); + return TrExpr(ite, initEtran, funcEtran, existEtran); } else if (expr is ConcreteSyntaxExpression) { var e = (ConcreteSyntaxExpression)expr; - return TrExpr(e.ResolvedExpression); + return TrExpr(e.ResolvedExpression, initEtran, funcEtran, existEtran); } else if (expr is BoxingCastExpr) { BoxingCastExpr e = (BoxingCastExpr)expr; - return translator.CondApplyBox(e.tok, TrExpr(e.E), e.FromType, e.ToType); + return translator.CondApplyBox(e.tok, TrExpr(e.E, initEtran, funcEtran, existEtran), e.FromType, e.ToType); } else if (expr is UnboxingCastExpr) { UnboxingCastExpr e = (UnboxingCastExpr)expr; - return translator.CondApplyUnbox(e.tok, TrExpr(e.E), e.FromType, e.ToType); + return translator.CondApplyUnbox(e.tok, TrExpr(e.E, initEtran, funcEtran, existEtran), e.FromType, e.ToType); } else { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression @@ -13314,8 +13321,10 @@ namespace Microsoft.Dafny { translatedExpression = etran.TrExpr(expr); splitHappened = false; } else { + // for quantifierExpr, we don't want to increase fuel in assert context + var existEtran = etran; etran = etran.LayerOffset(1); - translatedExpression = etran.TrExpr(expr); + translatedExpression = etran.TrExpr(expr, null, etran, existEtran); splitHappened = etran.Statistics_CustomLayerFunctionCount != 0; // return true if the LayerOffset(1) came into play } if (TrSplitNeedsTokenAdjustment(expr)) { diff --git a/Test/dafny4/Bug75.dfy b/Test/dafny4/Bug75.dfy new file mode 100644 index 00000000..37d35f77 --- /dev/null +++ b/Test/dafny4/Bug75.dfy @@ -0,0 +1,50 @@ +// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +predicate R1(x:int, y:int) { x > 0 ==> R2(x - 1) } +predicate R2(x:int) { exists y :: R1(x, y) } + +lemma L1(x:int) +{ + assume R2(x); + assert exists y :: R1(x, y); // FAILS +} + +lemma L2(x:int) + requires R2(x); // Oddly, adding this requires fixes the problem +{ + assume R2(x); + assert exists y :: R1(x, y); // SUCCEEDS +} + +// this predicate says that the first "n" elements of "s" + +// are in strictly increasing order + +predicate method Increasing(s: seq, n: nat) + requires n <= |s| +{ + n < 2 || + (s[n-2] < s[n-1] && Increasing(s, n-1)) +} + +method Extend(s: seq, n: nat) returns (n': nat) + requires n < |s| + requires forall i :: 0 <= i < n ==> Increasing(s, i) + ensures n <= n' <= |s| + ensures forall j :: 0 <= j < n' ==> Increasing(s, j) +{ + if 2 <= n && s[n-2] < s[n-1] { + n' := n + 1; + } else { + n' := n; + } +} + +function pred(i:int):int { i - 1 } +predicate f(a:int, s:int) { (a <= 0 || (exists s0 :: f(pred(a), s0))) } + +lemma Fuel1(a:int, s:int) +{ + assert f(a, s) <==> (a <= 0 || (exists s0 :: f(pred(a), s0))); // FAILS +} diff --git a/Test/dafny4/Bug75.dfy.expect b/Test/dafny4/Bug75.dfy.expect new file mode 100644 index 00000000..aeb37948 --- /dev/null +++ b/Test/dafny4/Bug75.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 13 verified, 0 errors -- cgit v1.2.3