diff options
Diffstat (limited to 'Source/Dafny/Translator.cs')
| -rw-r--r-- | Source/Dafny/Translator.cs | 284 |
1 files changed, 175 insertions, 109 deletions
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 37f80bf1..88f95f30 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -259,7 +259,7 @@ namespace Microsoft.Dafny { }
static Bpl.Program ReadPrelude() {
- string preludePath = Bpl.CommandLineOptions.Clo.DafnyPrelude;
+ string preludePath = DafnyOptions.O.DafnyPrelude;
if (preludePath == null)
{
//using (System.IO.Stream stream = cce.NonNull( System.Reflection.Assembly.GetExecutingAssembly().GetManifestResourceStream("DafnyPrelude.bpl")) // Use this once Spec#/VSIP supports designating a non-.resx project item as an embedded resource
@@ -1054,7 +1054,7 @@ namespace Microsoft.Dafny { Bpl.StmtList stmts;
if (!wellformednessProc) {
- if (3 <= CommandLineOptions.Clo.DafnyInduction && m.IsGhost && m.Mod.Count == 0 && m.Outs.Count == 0) {
+ if (3 <= DafnyOptions.O.Induction && m.IsGhost && m.Mod.Count == 0 && m.Outs.Count == 0) {
var posts = new List<Expression>();
m.Ens.ForEach(mfe => posts.Add(mfe.E));
var allIns = new List<Formal>();
@@ -1650,6 +1650,9 @@ namespace Microsoft.Dafny { var t = IsTotal(e.Obj, etran);
if (e.Obj.Type.IsRefType) {
t = BplAnd(t, Bpl.Expr.Neq(etran.TrExpr(e.Obj), predef.Null));
+ } else if (e.Field is DatatypeDestructor) {
+ var dtor = (DatatypeDestructor)e.Field;
+ t = BplAnd(t, FunctionCall(e.tok, dtor.EnclosingCtor.QueryField.FullName, Bpl.Type.Bool, etran.TrExpr(e.Obj)));
}
return t;
}
@@ -1735,7 +1738,7 @@ namespace Microsoft.Dafny { return r;
} else if (expr is OldExpr) {
OldExpr e = (OldExpr)expr;
- return new Bpl.OldExpr(expr.tok, IsTotal(e.E, etran));
+ return IsTotal(e.E, etran.Old);
} else if (expr is MultiSetFormingExpr) {
MultiSetFormingExpr e = (MultiSetFormingExpr)expr;
return IsTotal(e.E, etran);
@@ -1777,6 +1780,14 @@ namespace Microsoft.Dafny { }
Bpl.Expr r = BplAnd(t0, t1);
return z == null ? r : BplAnd(r, z);
+ } else if (expr is LetExpr) {
+ var e = (LetExpr)expr;
+ Bpl.Expr total = Bpl.Expr.True;
+ foreach (var rhs in e.RHSs) {
+ total = BplAnd(total, IsTotal(rhs, etran));
+ }
+ return BplAnd(total, IsTotal(etran.GetSubstitutedBody(e), etran));
+
} else if (expr is ComprehensionExpr) {
var e = (ComprehensionExpr)expr;
var total = IsTotal(e.Term, etran);
@@ -1794,7 +1805,7 @@ namespace Microsoft.Dafny { Bpl.Expr gTotal = IsTotal(e.Guard, etran);
Bpl.Expr g = etran.TrExpr(e.Guard);
Bpl.Expr bTotal = IsTotal(e.Body, etran);
- if (e is AssertExpr) {
+ if (e is AssertExpr || DafnyOptions.O.DisallowSoundnessCheating) {
return BplAnd(gTotal, BplAnd(g, bTotal));
} else {
return BplAnd(gTotal, Bpl.Expr.Imp(g, bTotal));
@@ -1893,7 +1904,7 @@ namespace Microsoft.Dafny { return CanCallAssumption(dtv.Arguments, etran);
} else if (expr is OldExpr) {
OldExpr e = (OldExpr)expr;
- return new Bpl.OldExpr(expr.tok, CanCallAssumption(e.E, etran));
+ return CanCallAssumption(e.E, etran.Old);
} else if (expr is MultiSetFormingExpr) {
MultiSetFormingExpr e = (MultiSetFormingExpr)expr;
return CanCallAssumption(e.E, etran);
@@ -1923,6 +1934,14 @@ namespace Microsoft.Dafny { break;
}
return BplAnd(t0, t1);
+ } else if (expr is LetExpr) {
+ var e = (LetExpr)expr;
+ Bpl.Expr canCall = Bpl.Expr.True;
+ foreach (var rhs in e.RHSs) {
+ canCall = BplAnd(canCall, CanCallAssumption(rhs, etran));
+ }
+ return BplAnd(canCall, CanCallAssumption(etran.GetSubstitutedBody(e), etran));
+
} else if (expr is ComprehensionExpr) {
var e = (ComprehensionExpr)expr;
var total = CanCallAssumption(e.Term, etran);
@@ -1938,11 +1957,11 @@ namespace Microsoft.Dafny { } else if (expr is PredicateExpr) {
var e = (PredicateExpr)expr;
Bpl.Expr gCanCall = CanCallAssumption(e.Guard, etran);
- Bpl.Expr g = etran.TrExpr(e.Guard);
Bpl.Expr bCanCall = CanCallAssumption(e.Body, etran);
- if (e is AssertExpr) {
- return BplAnd(gCanCall, BplAnd(g, bCanCall));
+ if (e is AssertExpr || DafnyOptions.O.DisallowSoundnessCheating) {
+ return BplAnd(gCanCall, bCanCall);
} else {
+ Bpl.Expr g = etran.TrExpr(e.Guard);
return BplAnd(gCanCall, Bpl.Expr.Imp(g, bCanCall));
}
} else if (expr is ITEExpr) {
@@ -2110,6 +2129,10 @@ namespace Microsoft.Dafny { CheckWellformed(e.Obj, options, locals, builder, etran);
if (e.Obj.Type.IsRefType) {
CheckNonNull(expr.tok, e.Obj, builder, etran, options.AssertKv);
+ } else if (e.Field is DatatypeDestructor) {
+ var dtor = (DatatypeDestructor)e.Field;
+ builder.Add(Assert(expr.tok, FunctionCall(e.tok, dtor.EnclosingCtor.QueryField.FullName, Bpl.Type.Bool, etran.TrExpr(e.Obj)),
+ string.Format("destructor '{0}' can only be applied to datatype values constructed by '{1}'", dtor.Name, dtor.EnclosingCtor.Name)));
}
if (options.DoReadsChecks && e.Field.IsMutable) {
builder.Add(Assert(expr.tok, Bpl.Expr.SelectTok(expr.tok, etran.TheFrame(expr.tok), etran.TrExpr(e.Obj), GetField(e)), "insufficient reads clause to read field", options.AssertKv));
@@ -2321,6 +2344,13 @@ namespace Microsoft.Dafny { break;
}
+ } else if (expr is LetExpr) {
+ var e = (LetExpr)expr;
+ foreach (var rhs in e.RHSs) {
+ CheckWellformed(rhs, options, locals, builder, etran);
+ }
+ CheckWellformedWithResult(etran.GetSubstitutedBody(e), options, result, resultType, locals, builder, etran);
+
} else if (expr is ComprehensionExpr) {
var e = (ComprehensionExpr)expr;
var substMap = SetupBoundVarsAsLocals(e.BoundVars, builder, locals, etran);
@@ -2339,7 +2369,7 @@ namespace Microsoft.Dafny { } else if (expr is PredicateExpr) {
var e = (PredicateExpr)expr;
CheckWellformed(e.Guard, options, locals, builder, etran);
- if (e is AssertExpr) {
+ if (e is AssertExpr || DafnyOptions.O.DisallowSoundnessCheating) {
bool splitHappened;
var ss = TrSplitExpr(e.Guard, etran, out splitHappened);
if (!splitHappened) {
@@ -2813,7 +2843,7 @@ namespace Microsoft.Dafny { if (!wellformednessProc) {
string comment = "user-defined preconditions";
foreach (MaybeFreeExpression p in m.Req) {
- if (p.IsFree && !CommandLineOptions.Clo.DisallowSoundnessCheating) {
+ if (p.IsFree && !DafnyOptions.O.DisallowSoundnessCheating) {
req.Add(Requires(p.E.tok, true, etran.TrExpr(p.E), null, comment));
} else {
bool splitHappened; // we actually don't care
@@ -2826,7 +2856,7 @@ namespace Microsoft.Dafny { }
comment = "user-defined postconditions";
if (!skipEnsures) foreach (MaybeFreeExpression p in m.Ens) {
- if (p.IsFree && !CommandLineOptions.Clo.DisallowSoundnessCheating) {
+ if (p.IsFree && !DafnyOptions.O.DisallowSoundnessCheating) {
ens.Add(Ensures(p.E.tok, true, etran.TrExpr(p.E), null, comment));
} else {
bool splitHappened; // we actually don't care
@@ -3300,7 +3330,7 @@ namespace Microsoft.Dafny { Contract.Requires(etran != null);
Contract.Requires(currentMethod != null && predef != null);
if (stmt is PredicateStmt) {
- if (stmt is AssertStmt || CommandLineOptions.Clo.DisallowSoundnessCheating) {
+ if (stmt is AssertStmt || DafnyOptions.O.DisallowSoundnessCheating) {
AddComment(builder, stmt, "assert statement");
PredicateStmt s = (PredicateStmt)stmt;
TrStmt_CheckWellformed(s.Expr, builder, locals, etran, false);
@@ -3928,7 +3958,7 @@ namespace Microsoft.Dafny { invDefinednessBuilder.Add(new Bpl.AssumeCmd(loopInv.E.tok, etran.TrExpr(loopInv.E)));
invariants.Add(new Bpl.AssumeCmd(loopInv.E.tok, Bpl.Expr.Imp(w, CanCallAssumption(loopInv.E, etran))));
- if (loopInv.IsFree && !CommandLineOptions.Clo.DisallowSoundnessCheating) {
+ if (loopInv.IsFree && !DafnyOptions.O.DisallowSoundnessCheating) {
invariants.Add(new Bpl.AssumeCmd(loopInv.E.tok, Bpl.Expr.Imp(w, etran.TrExpr(loopInv.E))));
} else {
bool splitHappened;
@@ -4139,7 +4169,7 @@ namespace Microsoft.Dafny { Contract.Requires(locals != null);
Contract.Requires(etran != null);
- Expression receiver = bReceiver == null ? dafnyReceiver : new BoogieWrapper(bReceiver);
+ Expression receiver = bReceiver == null ? dafnyReceiver : new BoogieWrapper(bReceiver, dafnyReceiver.Type);
Bpl.ExprSeq ins = new Bpl.ExprSeq();
if (!method.IsStatic) {
if (bReceiver == null) {
@@ -4995,11 +5025,13 @@ namespace Microsoft.Dafny { internal class BoogieWrapper : Expression
{
public readonly Bpl.Expr Expr;
- public BoogieWrapper(Bpl.Expr expr)
+ public BoogieWrapper(Bpl.Expr expr, Type dafnyType)
: base(expr.tok)
{
Contract.Requires(expr != null);
+ Contract.Requires(dafnyType != null);
Expr = expr;
+ Type = dafnyType; // resolve immediately
}
}
@@ -5009,7 +5041,7 @@ namespace Microsoft.Dafny { public readonly PredefinedDecls predef;
public readonly Translator translator;
public readonly string This;
- public readonly string modifiesFrame = "$_Frame"; // the name of the context's frame variable.
+ public readonly string modifiesFrame; // the name of the context's frame variable.
readonly Function applyLimited_CurrentFunction;
public readonly int layerOffset = 0;
public int Statistics_CustomLayerFunctionCount = 0;
@@ -5020,66 +5052,60 @@ namespace Microsoft.Dafny { Contract.Invariant(predef != null);
Contract.Invariant(translator != null);
Contract.Invariant(This != null);
+ Contract.Invariant(modifiesFrame != null);
Contract.Invariant(layerOffset == 0 || layerOffset == 1);
Contract.Invariant(0 <= Statistics_CustomLayerFunctionCount);
}
- public ExpressionTranslator(Translator translator, PredefinedDecls predef, IToken heapToken) {
+ /// <summary>
+ /// This is the most general constructor. It is private and takes all the parameters. Whenever
+ /// one ExpressionTranslator is constructed from another, unchanged parameters are just copied in.
+ /// </summary>
+ ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap, string thisVar,
+ Function applyLimited_CurrentFunction, int layerOffset, string modifiesFrame) {
+
Contract.Requires(translator != null);
Contract.Requires(predef != null);
- Contract.Requires(heapToken != null);
+ Contract.Requires(heap != null);
+ Contract.Requires(thisVar != null);
+ Contract.Invariant(layerOffset == 0 || layerOffset == 1);
+ Contract.Invariant(modifiesFrame != null);
+
this.translator = translator;
this.predef = predef;
- this.HeapExpr = new Bpl.IdentifierExpr(heapToken, predef.HeapVarName, predef.HeapType);
- this.This = "this";
+ this.HeapExpr = heap;
+ this.This = thisVar;
+ this.applyLimited_CurrentFunction = applyLimited_CurrentFunction;
+ this.layerOffset = layerOffset;
+ this.modifiesFrame = modifiesFrame;
}
- public ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap) {
+ public ExpressionTranslator(Translator translator, PredefinedDecls predef, IToken heapToken)
+ : this(translator, predef, new Bpl.IdentifierExpr(heapToken, predef.HeapVarName, predef.HeapType)) {
Contract.Requires(translator != null);
Contract.Requires(predef != null);
- Contract.Requires(heap != null);
- this.translator = translator;
- this.predef = predef;
- this.HeapExpr = heap;
- this.This = "this";
+ Contract.Requires(heapToken != null);
}
- public ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap, string thisVar) {
+ public ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap)
+ : this(translator, predef, heap, "this") {
Contract.Requires(translator != null);
Contract.Requires(predef != null);
Contract.Requires(heap != null);
- Contract.Requires(thisVar != null);
- this.translator = translator;
- this.predef = predef;
- this.HeapExpr = heap;
- this.This = thisVar;
}
- ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap, Function applyLimited_CurrentFunction, int layerOffset)
- {
- Contract.Requires(translator != null);
- Contract.Requires(predef != null);
- Contract.Requires(heap != null);
- this.translator = translator;
- this.predef = predef;
- this.HeapExpr = heap;
- this.applyLimited_CurrentFunction = applyLimited_CurrentFunction;
- this.This = "this";
- this.layerOffset = layerOffset;
+ public ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap, string thisVar)
+ : this(translator, predef, heap, thisVar, null, 0, "$_Frame") {
+ Contract.Requires(translator != null);
+ Contract.Requires(predef != null);
+ Contract.Requires(heap != null);
+ Contract.Requires(thisVar != null);
}
public ExpressionTranslator(ExpressionTranslator etran, string modifiesFrame)
- {
- Contract.Requires(etran != null);
- Contract.Requires(modifiesFrame != null);
- this.translator = etran.translator;
- this.HeapExpr = etran.HeapExpr;
- this.predef = etran.predef;
- this.This = etran.This;
- this.applyLimited_CurrentFunction = etran.applyLimited_CurrentFunction;
- this.layerOffset = etran.layerOffset;
- this.oldEtran = etran.oldEtran;
- this.modifiesFrame = modifiesFrame;
+ : this(etran.translator, etran.predef, etran.HeapExpr, etran.This, etran.applyLimited_CurrentFunction, etran.layerOffset, modifiesFrame) {
+ Contract.Requires(etran != null);
+ Contract.Requires(modifiesFrame != null);
}
ExpressionTranslator oldEtran;
@@ -5088,7 +5114,7 @@ namespace Microsoft.Dafny { Contract.Ensures(Contract.Result<ExpressionTranslator>() != null);
if (oldEtran == null) {
- oldEtran = new ExpressionTranslator(translator, predef, new Bpl.OldExpr(HeapExpr.tok, HeapExpr), applyLimited_CurrentFunction, layerOffset);
+ oldEtran = new ExpressionTranslator(translator, predef, new Bpl.OldExpr(HeapExpr.tok, HeapExpr), This, applyLimited_CurrentFunction, layerOffset, modifiesFrame);
}
return oldEtran;
}
@@ -5104,7 +5130,7 @@ namespace Microsoft.Dafny { Contract.Requires(applyLimited_CurrentFunction != null);
Contract.Ensures(Contract.Result<ExpressionTranslator>() != null);
- return new ExpressionTranslator(translator, predef, HeapExpr, applyLimited_CurrentFunction, layerOffset);
+ return new ExpressionTranslator(translator, predef, HeapExpr, This, applyLimited_CurrentFunction, layerOffset, modifiesFrame);
}
public ExpressionTranslator LayerOffset(int offset) {
@@ -5112,7 +5138,7 @@ namespace Microsoft.Dafny { Contract.Requires(layerOffset + offset <= 1);
Contract.Ensures(Contract.Result<ExpressionTranslator>() != null);
- return new ExpressionTranslator(translator, predef, HeapExpr, applyLimited_CurrentFunction, layerOffset + offset);
+ return new ExpressionTranslator(translator, predef, HeapExpr, This, applyLimited_CurrentFunction, layerOffset + offset, modifiesFrame);
}
public Bpl.IdentifierExpr TheFrame(IToken tok)
@@ -5124,7 +5150,7 @@ namespace Microsoft.Dafny { Bpl.TypeVariable alpha = new Bpl.TypeVariable(tok, "beta");
Bpl.Type fieldAlpha = predef.FieldName(tok, alpha);
Bpl.Type ty = new Bpl.MapType(tok, new Bpl.TypeVariableSeq(alpha), new Bpl.TypeSeq(predef.RefType, fieldAlpha), Bpl.Type.Bool);
- return new Bpl.IdentifierExpr(tok, this.modifiesFrame ?? "$_Frame", ty);
+ return new Bpl.IdentifierExpr(tok, this.modifiesFrame, ty);
}
public Bpl.IdentifierExpr Tick() {
@@ -5134,24 +5160,33 @@ namespace Microsoft.Dafny { return new Bpl.IdentifierExpr(Token.NoToken, "$Tick", predef.TickType);
}
- public Bpl.IdentifierExpr ModuleContextHeight()
- {
- Contract.Ensures(Contract.Result<Bpl.IdentifierExpr>().Type != null);
+ public Bpl.IdentifierExpr ModuleContextHeight() {
+ Contract.Ensures(Contract.Result<Bpl.IdentifierExpr>().Type != null);
return new Bpl.IdentifierExpr(Token.NoToken, "$ModuleContextHeight", Bpl.Type.Int);
}
- public Bpl.IdentifierExpr FunctionContextHeight()
- {
- Contract.Ensures(Contract.Result<Bpl.IdentifierExpr>().Type != null);
+ public Bpl.IdentifierExpr FunctionContextHeight() {
+ Contract.Ensures(Contract.Result<Bpl.IdentifierExpr>().Type != null);
return new Bpl.IdentifierExpr(Token.NoToken, "$FunctionContextHeight", Bpl.Type.Int);
}
- public Bpl.IdentifierExpr InMethodContext()
- {
- Contract.Ensures(Contract.Result<Bpl.IdentifierExpr>().Type != null);
+ public Bpl.IdentifierExpr InMethodContext() {
+ Contract.Ensures(Contract.Result<Bpl.IdentifierExpr>().Type != null);
return new Bpl.IdentifierExpr(Token.NoToken, "$InMethodContext", Bpl.Type.Bool);
}
+ public Expression GetSubstitutedBody(LetExpr e) {
+ Contract.Requires(e != null);
+ var substMap = new Dictionary<IVariable, Expression>();
+ Contract.Assert(e.Vars.Count == e.RHSs.Count); // checked by resolution
+ for (int i = 0; i < e.Vars.Count; i++) {
+ Expression rhs = e.RHSs[i];
+ substMap.Add(e.Vars[i], new BoogieWrapper(TrExpr(rhs), rhs.Type));
+ }
+ return Translator.Substitute(e.Body, null, substMap);
+ }
+
+
/// <summary>
/// Translates Dafny expression "expr" into a Boogie expression. If the type of "expr" can be a boolean, then the
/// token (source location) of the resulting expression is filled in (it wouldn't hurt if the token were always
@@ -5322,7 +5357,7 @@ namespace Microsoft.Dafny { } else if (expr is OldExpr) {
OldExpr e = (OldExpr)expr;
- return new Bpl.OldExpr(expr.tok, TrExpr(e.E));
+ return Old.TrExpr(e.E);
} else if (expr is MultiSetFormingExpr) {
MultiSetFormingExpr e = (MultiSetFormingExpr)expr;
@@ -5337,7 +5372,6 @@ namespace Microsoft.Dafny { } else if (expr is FreshExpr) {
FreshExpr e = (FreshExpr)expr;
- Bpl.Expr oldHeap = new Bpl.OldExpr(expr.tok, HeapExpr);
if (e.E.Type is SetType) {
// generate: (forall $o: ref :: $o != null && X[Box($o)] ==> !old($Heap)[$o,alloc])
// TODO: trigger?
@@ -5345,7 +5379,7 @@ namespace Microsoft.Dafny { Bpl.Expr o = new Bpl.IdentifierExpr(expr.tok, oVar);
Bpl.Expr oNotNull = Bpl.Expr.Neq(o, predef.Null);
Bpl.Expr oInSet = TrInSet(expr.tok, o, e.E, ((SetType)e.E.Type).Arg);
- Bpl.Expr oIsFresh = Bpl.Expr.Not(IsAlloced(expr.tok, o, oldHeap));
+ Bpl.Expr oIsFresh = Bpl.Expr.Not(Old.IsAlloced(expr.tok, o));
Bpl.Expr body = Bpl.Expr.Imp(Bpl.Expr.And(oNotNull, oInSet), oIsFresh);
return new Bpl.ForallExpr(expr.tok, new Bpl.VariableSeq(oVar), body);
} else if (e.E.Type is SeqType) {
@@ -5355,14 +5389,14 @@ namespace Microsoft.Dafny { 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 oIsFresh = Bpl.Expr.Not(IsAlloced(expr.tok, XsubI, oldHeap));
+ Bpl.Expr oIsFresh = Bpl.Expr.Not(Old.IsAlloced(expr.tok, XsubI));
Bpl.Expr xsubiNotNull = Bpl.Expr.Neq(translator.FunctionCall(expr.tok, BuiltinFunction.Unbox, predef.RefType, XsubI), predef.Null);
Bpl.Expr body = Bpl.Expr.Imp(Bpl.Expr.And(iBounds, xsubiNotNull), oIsFresh);
return new Bpl.ForallExpr(expr.tok, new Bpl.VariableSeq(iVar), body);
} else {
// generate: x == null || !old($Heap)[x]
Bpl.Expr oNull = Bpl.Expr.Eq(TrExpr(e.E), predef.Null);
- Bpl.Expr oIsFresh = Bpl.Expr.Not(IsAlloced(expr.tok, TrExpr(e.E), oldHeap));
+ Bpl.Expr oIsFresh = Bpl.Expr.Not(Old.IsAlloced(expr.tok, TrExpr(e.E)));
return Bpl.Expr.Binary(expr.tok, BinaryOperator.Opcode.Or, oNull, oIsFresh);
}
@@ -5539,6 +5573,10 @@ namespace Microsoft.Dafny { }
return Bpl.Expr.Binary(expr.tok, bOpcode, e0, e1);
+ } else if (expr is LetExpr) {
+ var e = (LetExpr)expr;
+ return TrExpr(GetSubstitutedBody(e));
+
} else if (expr is QuantifierExpr) {
QuantifierExpr e = (QuantifierExpr)expr;
Bpl.VariableSeq bvars = new Bpl.VariableSeq();
@@ -5923,16 +5961,7 @@ namespace Microsoft.Dafny { Contract.Requires(e != null);
Contract.Ensures(Contract.Result<Bpl.Expr>() != null);
- return IsAlloced(tok, e, HeapExpr);
- }
-
- Bpl.Expr IsAlloced(IToken tok, Bpl.Expr e, Bpl.Expr heap) {
- Contract.Requires(tok != null);
- Contract.Requires(e != null);
- Contract.Requires(heap != null);
- Contract.Ensures(Contract.Result<Bpl.Expr>() != null);
-
- return ReadHeap(tok, heap, e, predef.Alloc(tok));
+ return ReadHeap(tok, HeapExpr, e, predef.Alloc(tok));
}
public Bpl.Expr GoodRef(IToken tok, Bpl.Expr e, Type type) {
@@ -6394,9 +6423,9 @@ namespace Microsoft.Dafny { var e = (ConcreteSyntaxExpression)expr;
return TrSplitExpr(e.ResolvedExpression, splits, position, expandFunctions, etran);
- } else if (expr is PredicateExpr) {
- var e = (PredicateExpr)expr;
- return TrSplitExpr(e.Body, splits, position, expandFunctions, etran);
+ } else if (expr is LetExpr) {
+ var e = (LetExpr)expr;
+ return TrSplitExpr(etran.GetSubstitutedBody(e), splits, position, expandFunctions, etran);
} else if (expr is UnaryExpr) {
var e = (UnaryExpr)expr;
@@ -6467,15 +6496,33 @@ namespace Microsoft.Dafny { return true;
}
- } else if (expr is OldExpr) {
- var e = (OldExpr)expr;
- var ss = new List<SplitExprInfo>();
- if (TrSplitExpr(e.E, ss, position, expandFunctions, etran)) {
+ } else if (expr is PredicateExpr) {
+ var e = (PredicateExpr)expr;
+ // For a predicate expression in split position, the predicate can be used as an assumption. Unfortunately,
+ // this assumption is not generated in non-split positions (because I don't know how.)
+ // So, treat "assert/assume P; E" like "P ==> E".
+ if (position) {
+ var guard = etran.TrExpr(e.Guard);
+ var ss = new List<SplitExprInfo>();
+ TrSplitExpr(e.Body, ss, position, expandFunctions, etran);
+ foreach (var s in ss) {
+ // as the source location in the following implication, use that of the translated "s"
+ splits.Add(new SplitExprInfo(s.IsFree, Bpl.Expr.Binary(s.E.tok, BinaryOperator.Opcode.Imp, guard, s.E)));
+ }
+ } else {
+ var ss = new List<SplitExprInfo>();
+ TrSplitExpr(e.Guard, ss, !position, expandFunctions, etran);
+ var rhs = etran.TrExpr(e.Body);
foreach (var s in ss) {
- splits.Add(new SplitExprInfo(s.IsFree, new Bpl.OldExpr(s.E.tok, s.E)));
+ // as the source location in the following implication, use that of the translated "s"
+ splits.Add(new SplitExprInfo(s.IsFree, Bpl.Expr.Binary(s.E.tok, BinaryOperator.Opcode.Imp, s.E, rhs)));
}
- return true;
}
+ return true;
+
+ } else if (expr is OldExpr) {
+ var e = (OldExpr)expr;
+ return TrSplitExpr(e.E, splits, position, expandFunctions, etran.Old);
} else if (expandFunctions && position && expr is FunctionCallExpr) {
var fexp = (FunctionCallExpr)expr;
@@ -6531,7 +6578,7 @@ namespace Microsoft.Dafny { } else if ((position && expr is ForallExpr) || (!position && expr is ExistsExpr)) {
var e = (QuantifierExpr)expr;
var inductionVariables = ApplyInduction(e);
- if (2 <= CommandLineOptions.Clo.DafnyInduction && inductionVariables.Count != 0) {
+ if (2 <= DafnyOptions.O.Induction && inductionVariables.Count != 0) {
// From the given quantifier (forall n :: P(n)), generate the seemingly weaker proof obligation
// (forall n :: (forall k :: k < n ==> P(k)) ==> P(n))
// For an existential (exists n :: P(n)), it is
@@ -6642,7 +6689,7 @@ namespace Microsoft.Dafny { Contract.Requires(tracePrinter != null);
Contract.Ensures(Contract.Result<List<VarType>>() != null);
- if (CommandLineOptions.Clo.DafnyInduction == 0) {
+ if (DafnyOptions.O.Induction == 0) {
return new List<VarType>(); // don't apply induction
}
@@ -6727,7 +6774,7 @@ namespace Microsoft.Dafny { }
}
- if (CommandLineOptions.Clo.DafnyInduction < 2) {
+ if (DafnyOptions.O.Induction < 2) {
return new List<VarType>(); // don't apply induction
}
@@ -6762,7 +6809,7 @@ namespace Microsoft.Dafny { /// Parameter 'n' is allowed to be a ThisSurrogate.
/// </summary>
bool VarOccursInArgumentToRecursiveFunction(Expression expr, IVariable n) {
- switch (CommandLineOptions.Clo.DafnyInductionHeuristic) {
+ switch (DafnyOptions.O.InductionHeuristic) {
case 0: return true;
case 1: return ContainsFreeVariable(expr, false, n);
default: return VarOccursInArgumentToRecursiveFunction(expr, n, false);
@@ -6780,7 +6827,7 @@ namespace Microsoft.Dafny { Contract.Requires(n != null);
// The following variable is what gets passed down to recursive calls if the subexpression does not itself acquire prominent status.
- var subExprIsProminent = CommandLineOptions.Clo.DafnyInductionHeuristic == 2 || CommandLineOptions.Clo.DafnyInductionHeuristic == 4 ? /*once prominent, always prominent*/exprIsProminent : /*reset the prominent status*/false;
+ var subExprIsProminent = DafnyOptions.O.InductionHeuristic == 2 || DafnyOptions.O.InductionHeuristic == 4 ? /*once prominent, always prominent*/exprIsProminent : /*reset the prominent status*/false;
if (expr is ThisExpr) {
return exprIsProminent && n is ThisSurrogate;
@@ -6789,13 +6836,13 @@ namespace Microsoft.Dafny { return exprIsProminent && e.Var == n;
} else if (expr is SeqSelectExpr) {
var e = (SeqSelectExpr)expr;
- var q = CommandLineOptions.Clo.DafnyInductionHeuristic < 4 || subExprIsProminent;
+ var q = DafnyOptions.O.InductionHeuristic < 4 || subExprIsProminent;
return VarOccursInArgumentToRecursiveFunction(e.Seq, n, subExprIsProminent) || // this subexpression does not acquire "prominent" status
(e.E0 != null && VarOccursInArgumentToRecursiveFunction(e.E0, n, q)) || // this one does (unless arrays/sequences are excluded)
(e.E1 != null && VarOccursInArgumentToRecursiveFunction(e.E1, n, q)); // ditto
} else if (expr is MultiSelectExpr) {
var e = (MultiSelectExpr)expr;
- var q = CommandLineOptions.Clo.DafnyInductionHeuristic < 4 || subExprIsProminent;
+ var q = DafnyOptions.O.InductionHeuristic < 4 || subExprIsProminent;
return VarOccursInArgumentToRecursiveFunction(e.Array, n, subExprIsProminent) ||
e.Indices.Exists(exp => VarOccursInArgumentToRecursiveFunction(exp, n, q));
} else if (expr is FunctionCallExpr) {
@@ -6806,7 +6853,7 @@ namespace Microsoft.Dafny { bool inferredDecreases; // we don't actually care
var decr = FunctionDecreasesWithDefault(e.Function, out inferredDecreases);
bool variantArgument;
- if (CommandLineOptions.Clo.DafnyInductionHeuristic < 6) {
+ if (DafnyOptions.O.InductionHeuristic < 6) {
variantArgument = rec;
} else {
// The receiver is considered to be "variant" if the function is recursive and the receiver participates
@@ -6821,7 +6868,7 @@ namespace Microsoft.Dafny { for (int i = 0; i < e.Function.Formals.Count; i++) {
var f = e.Function.Formals[i];
var exp = e.Args[i];
- if (CommandLineOptions.Clo.DafnyInductionHeuristic < 6) {
+ if (DafnyOptions.O.InductionHeuristic < 6) {
variantArgument = rec;
} else {
// The argument position is considered to be "variant" if the function is recursive and the argument participates
@@ -6838,9 +6885,6 @@ namespace Microsoft.Dafny { var e = (DatatypeValue)expr;
var q = n.Type.IsDatatype ? exprIsProminent : subExprIsProminent; // prominent status continues, if we're looking for a variable whose type is a datatype
return e.Arguments.Exists(exp => VarOccursInArgumentToRecursiveFunction(exp, n, q));
- } else if (expr is OldExpr) {
- var e = (OldExpr)expr;
- return VarOccursInArgumentToRecursiveFunction(e.E, n, exprIsProminent); // prominent status continues
} else if (expr is UnaryExpr) {
var e = (UnaryExpr)expr;
// both Not and SeqLength preserve prominence
@@ -6958,7 +7002,7 @@ namespace Microsoft.Dafny { }
}
- static Expression Substitute(Expression expr, Expression receiverReplacement, Dictionary<IVariable, Expression/*!*/>/*!*/ substMap) {
+ public static Expression Substitute(Expression expr, Expression receiverReplacement, Dictionary<IVariable, Expression/*!*/>/*!*/ substMap) {
Contract.Requires(expr != null);
Contract.Requires(cce.NonNullDictionaryAndValues(substMap));
Contract.Ensures(Contract.Result<Expression>() != null);
@@ -7044,7 +7088,11 @@ namespace Microsoft.Dafny { } else if (expr is OldExpr) {
OldExpr e = (OldExpr)expr;
- Expression se = Substitute(e.E, receiverReplacement, substMap); // TODO: whoa, won't this do improper variable capture?
+ // Note, it is up to the caller to avoid variable capture. In most cases, this is not a
+ // problem, since variables have unique declarations. However, it is an issue if the substitution
+ // takes place inside an OldExpr. In those cases (see LetExpr), the caller can use a
+ // BoogieWrapper before calling Substitute.
+ Expression se = Substitute(e.E, receiverReplacement, substMap);
if (se != e.E) {
newExpr = new OldExpr(expr.tok, se);
}
@@ -7076,6 +7124,22 @@ namespace Microsoft.Dafny { newExpr = newBin;
}
+ } else if (expr is LetExpr) {
+ var e = (LetExpr)expr;
+ var rhss = new List<Expression>();
+ bool anythingChanged = false;
+ foreach (var rhs in e.RHSs) {
+ var r = Substitute(rhs, receiverReplacement, substMap);
+ if (r != rhs) {
+ anythingChanged = true;
+ }
+ rhss.Add(r);
+ }
+ var body = Substitute(e.Body, receiverReplacement, substMap);
+ if (anythingChanged || body != e.Body) {
+ newExpr = new LetExpr(e.tok, e.Vars, rhss, body);
+ }
+
} else if (expr is ComprehensionExpr) {
var e = (ComprehensionExpr)expr;
Expression newRange = e.Range == null ? null : Substitute(e.Range, receiverReplacement, substMap);
@@ -7102,10 +7166,12 @@ namespace Microsoft.Dafny { var e = (PredicateExpr)expr;
Expression g = Substitute(e.Guard, receiverReplacement, substMap);
Expression b = Substitute(e.Body, receiverReplacement, substMap);
- if (expr is AssertExpr) {
- newExpr = new AssertExpr(e.tok, g, b);
- } else {
- newExpr = new AssumeExpr(e.tok, g, b);
+ if (g != e.Guard || b != e.Body) {
+ if (expr is AssertExpr) {
+ newExpr = new AssertExpr(e.tok, g, b);
+ } else {
+ newExpr = new AssumeExpr(e.tok, g, b);
+ }
}
} else if (expr is ITEExpr) {
|