summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Dafny/DafnyAst.cs37
-rw-r--r--Source/Dafny/Resolver.cs1
-rw-r--r--Source/Dafny/Translator.cs151
-rw-r--r--Test/dafny4/Bug75.dfy50
-rw-r--r--Test/dafny4/Bug75.dfy.expect2
5 files changed, 169 insertions, 72 deletions
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; }
}
/// <summary>
/// An ICallable is a Function, Method, IteratorDecl, or RedirectingTypeDecl.
@@ -2392,6 +2393,7 @@ namespace Microsoft.Dafny {
/// </summary>
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(); }
+ }
}
/// <summary>
/// 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<TypeParameter> typeArgs,
List<Formal> ins, List<Formal> outs,
Specification<FrameExpression> reads, Specification<FrameExpression> mod, Specification<Expression> 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<Expression> SubExpressions {
get {
@@ -3438,6 +3467,7 @@ namespace Microsoft.Dafny {
public bool IsTailRecursive; // filled in during resolution
public readonly ISet<IVariable> AssignedAssumptionVariables = new HashSet<IVariable>();
public Method OverriddenMethod;
+ public bool containsQuantifier;
public override IEnumerable<Expression> 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<IVariable, Expression> substMap = new Dictionary<IVariable, Expression>();
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).
/// </summary>
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<Expression, Bpl.Expr> TrArg = arg => translator.BoxIfUnboxed(TrExpr(arg), arg.Type);
+ Func<Expression, Bpl.Expr> 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<Variable> { 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<Variable> tyvars = translator.MkTyParamBinders(e.TypeArgs);
List<Variable> bvars = new List<Variable>();
- 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<Bpl.Expr> {
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<Bpl.Expr> tt = new List<Bpl.Expr>();
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<TypeVariable>(), 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<IVariable, Expression> subst = new Dictionary<IVariable,Expression>();
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<TypeVariable>(), new List<Variable> { 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<TypeVariable>(), new List<Variable> { 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<Bpl.Expr> { 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<int>, n: nat)
+ requires n <= |s|
+{
+ n < 2 ||
+ (s[n-2] < s[n-1] && Increasing(s, n-1))
+}
+
+method Extend(s: seq<int>, 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-22 08:47:15 +0000