From 06c6bfd2134bd9412b909d77887673b47a88b72b Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Tue, 2 Oct 2012 22:53:29 -0700 Subject: Dafny: changed iterator body to resolve to implicit fields rather than to the formal in- and yield-parameters --- Dafny/DafnyAst.cs | 18 ++---- Dafny/Resolver.cs | 175 ++++++++++++++++++++++------------------------------ Dafny/Translator.cs | 153 +++++++++++++++++++++++---------------------- 3 files changed, 157 insertions(+), 189 deletions(-) (limited to 'Dafny') diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs index 277cb282..fb47f020 100644 --- a/Dafny/DafnyAst.cs +++ b/Dafny/DafnyAst.cs @@ -1163,8 +1163,8 @@ namespace Microsoft.Dafny { { public readonly List Ins; public readonly List Outs; - public readonly List OutsHistory; // these are the 'xs' variables - public readonly List ExtraVars; // _reads, _modifies, _new + public readonly List OutsFields; + public readonly List OutsHistoryFields; // these are the 'xs' variables public readonly List DecreasesFields; // filled in during resolution public readonly Specification Reads; public readonly Specification Modifies; @@ -1214,18 +1214,8 @@ namespace Microsoft.Dafny { Body = body; SignatureIsOmitted = signatureIsOmitted; - OutsHistory = new List(); - foreach (var p in Outs) { - var tp = p.Type; - if (tp.IsSubrangeType) { - tp = new IntType(); // because SeqType(NatType) is now allowed (despite the fact that the history variable is readonly, which is unfortunate) - } - OutsHistory.Add(new Formal(p.tok, p.Name + "s", new SeqType(tp), false, true)); - } - ExtraVars = new List(); - ExtraVars.Add(new Formal(tok, "_reads", new SetType(new ObjectType()), true, true)); - ExtraVars.Add(new Formal(tok, "_modifies", new SetType(new ObjectType()), true, true)); - ExtraVars.Add(new Formal(tok, "_new", new SetType(new ObjectType()), false, true)); + OutsFields = new List(); + OutsHistoryFields = new List(); DecreasesFields = new List(); } diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs index 8f005368..dc49013d 100644 --- a/Dafny/Resolver.cs +++ b/Dafny/Resolver.cs @@ -520,30 +520,36 @@ namespace Microsoft.Dafny if (members.ContainsKey(p.Name)) { Error(p, "Name of yield-parameter is used by another member of the iterator: {0}", p.Name); } else { - var field = new SpecialField(p.tok, p.Name, p.CompileName, "", "", p.IsGhost, true, false, p.Type, null); + var field = new SpecialField(p.tok, p.Name, p.CompileName, "", "", p.IsGhost, true, true, p.Type, null); field.EnclosingClass = iter; // resolve here + iter.OutsFields.Add(field); members.Add(p.Name, field); iter.Members.Add(field); } } - var yieldHistoryVariables = new List(); - foreach (var p in iter.OutsHistory) { - if (members.ContainsKey(p.Name)) { + foreach (var p in iter.Outs) { + var nm = p.Name + "s"; + if (members.ContainsKey(nm)) { Error(p.tok, "Name of implicit yield-history variable '{0}' is already used by another member of the iterator", p.Name); } else { - var field = new SpecialField(p.tok, p.Name, p.CompileName, "", "", true, true, false, p.Type, null); + var tp = new SeqType(p.Type.IsSubrangeType ? new IntType() : p.Type); + var field = new SpecialField(p.tok, nm, nm, "", "", true, true, false, tp, null); field.EnclosingClass = iter; // resolve here - yieldHistoryVariables.Add(field); // just record this field for now (until all parameters have been added as members) + iter.OutsHistoryFields.Add(field); // for now, just record this field (until all parameters have been added as members) } } - // now that already-used 'xs' names have been checked for, add these yield-history variables - yieldHistoryVariables.ForEach(f => { + // now that already-used 'ys' names have been checked for, add these yield-history variables + iter.OutsHistoryFields.ForEach(f => { members.Add(f.Name, f); iter.Members.Add(f); }); // add the additional special variables as fields - foreach (var p in iter.ExtraVars) { - var field = new SpecialField(p.tok, p.Name, p.CompileName, "", "", p.IsGhost, !p.InParam, false, p.Type, null); + foreach (var p in new List>() { + new Tuple("_reads", false), + new Tuple("_modifies", false), + new Tuple("_new", true) }) + { + var field = new SpecialField(iter.tok, p.Item1, p.Item1, "", "", true, p.Item2, p.Item2, new SetType(new ObjectType()), null); field.EnclosingClass = iter; // resolve here members.Add(field.Name, field); iter.Members.Add(field); @@ -562,9 +568,9 @@ namespace Microsoft.Dafny var nm = "_decreases" + i; var field = new SpecialField(p.tok, nm, nm, "", "", true, false, false, new InferredTypeProxy(), null); field.EnclosingClass = iter; // resolve here + iter.DecreasesFields.Add(field); members.Add(field.Name, field); iter.Members.Add(field); - iter.DecreasesFields.Add(field); i++; } @@ -2516,25 +2522,12 @@ namespace Microsoft.Dafny Error(iter, "iterator signature can be omitted only in refining methods"); } var defaultTypeArguments = iter.TypeArgs.Count == 0 ? iter.TypeArgs : null; - // resolve in-parameters - foreach (Formal p in iter.Ins) { - if (!scope.Push(p.Name, p)) { - Error(p, "Duplicate parameter name: {0}", p.Name); - } + // resolve the types of the parameters + foreach (var p in iter.Ins.Concat(iter.Outs)) { ResolveType(p.tok, p.Type, defaultTypeArguments, true); } - // resolve yield-parameters - foreach (Formal p in iter.Outs) { - if (!scope.Push(p.Name, p)) { - Error(p, "Duplicate parameter name: {0}", p.Name); - } - ResolveType(p.tok, p.Type, defaultTypeArguments, true); - } - // resolve yield-history variables - foreach (Formal p in iter.OutsHistory) { - if (!scope.Push(p.Name, p)) { - Error(p, "Name conflict with yield-history variable: {0}", p.Name); - } + // resolve the types of the added fields (in case some of these types would cause the addition of default type arguments) + foreach (var p in iter.OutsHistoryFields) { ResolveType(p.tok, p.Type, defaultTypeArguments, true); } scope.PopMarker(); @@ -2545,6 +2538,8 @@ namespace Microsoft.Dafny /// void ResolveIterator(IteratorDecl iter) { Contract.Requires(iter != null); + Contract.Requires(currentClass == null); + Contract.Ensures(currentClass == null); var initialErrorCount = ErrorCount; @@ -2554,6 +2549,20 @@ namespace Microsoft.Dafny iter.Ins.ForEach(p => scope.Push(p.Name, p)); // Start resolving specification... + // we start with the decreases clause, because the _decreases fields were only given type proxies before; we'll know + // the types only after resolving the decreases clause (and it may be that some of resolution has already seen uses of + // these fields; so, with no further ado, here we go + Contract.Assert(iter.Decreases.Expressions.Count == iter.DecreasesFields.Count); + for (int i = 0; i < iter.Decreases.Expressions.Count; i++) { + var e = iter.Decreases.Expressions[i]; + ResolveExpression(e, false); + // any type is fine, but associate this type with the corresponding _decreases field + var d = iter.DecreasesFields[i]; + if (!UnifyTypes(d.Type, e.Type)) { + // bummer, there was a use--and a bad use--of the field before, so this won't be the best of error messages + Error(e, "type of field {0} is {1}, but has been constrained elsewhere to be of type {2}", d.Name, e.Type, d.Type); + } + } foreach (FrameExpression fe in iter.Reads.Expressions) { ResolveFrameExpression(fe, "reads"); } @@ -2567,19 +2576,14 @@ namespace Microsoft.Dafny Error(e.E, "Precondition must be a boolean (got {0})", e.E.Type); } } - Contract.Assert(iter.Decreases.Expressions.Count == iter.DecreasesFields.Count); - for (int i = 0; i < iter.Decreases.Expressions.Count; i++) { - var e = iter.Decreases.Expressions[i]; - ResolveExpression(e, false); - // any type is fine, but associate this type with the corresponding _decreases field - var d = iter.DecreasesFields[i]; - if (!UnifyTypes(d.Type, e.Type)) { - Error(e, "type of field {0} is {1}, but has been constrained elsewhere to be of type {2}", d.Name, e.Type, d.Type); - } - } - // Now add the yield-history variables to the scope - iter.OutsHistory.ForEach(p => scope.Push(p.Name, p)); + scope.PopMarker(); // for the in-parameters + + // We resolve the rest of the specification in an instance context. So mentions of the in- or yield-parameters + // get resolved as field dereferences (with an implicit "this") + scope.PushMarker(); + currentClass = iter; + Contract.Assert(scope.AllowInstance); foreach (MaybeFreeExpression e in iter.YieldRequires) { ResolveExpression(e.E, false); @@ -2588,29 +2592,23 @@ namespace Microsoft.Dafny Error(e.E, "Yield precondition must be a boolean (got {0})", e.E.Type); } } - foreach (MaybeFreeExpression e in iter.Ensures) { + foreach (MaybeFreeExpression e in iter.YieldEnsures) { ResolveExpression(e.E, true); Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression if (!UnifyTypes(e.E.Type, Type.Bool)) { - Error(e.E, "Postcondition must be a boolean (got {0})", e.E.Type); + Error(e.E, "Yield postcondition must be a boolean (got {0})", e.E.Type); } } - - // Finally, add the yield-parameters and extra variables to the scope - scope.PushMarker(); // make the yield-parameters appear in the same scope as the outer-most locals of the body (since this is what is done for methods) - iter.Outs.ForEach(p => scope.Push(p.Name, p)); - iter.ExtraVars.ForEach(p => scope.Push(p.Name, p)); - - ResolveAttributes(iter.Attributes, false); - - foreach (MaybeFreeExpression e in iter.YieldEnsures) { + foreach (MaybeFreeExpression e in iter.Ensures) { ResolveExpression(e.E, true); Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression if (!UnifyTypes(e.E.Type, Type.Bool)) { - Error(e.E, "Yield postcondition must be a boolean (got {0})", e.E.Type); + Error(e.E, "Postcondition must be a boolean (got {0})", e.E.Type); } } + ResolveAttributes(iter.Attributes, false); + var postSpecErrorCount = ErrorCount; // Resolve body @@ -2618,8 +2616,8 @@ namespace Microsoft.Dafny ResolveBlockStatement(iter.Body, false, iter); } - scope.PopMarker(); // for the yield-parameters, extra variables, and outermost-level locals - scope.PopMarker(); // for the in-parameters and yield-history variables + currentClass = null; + scope.PopMarker(); // pop off the AllowInstance setting if (postSpecErrorCount == initialErrorCount) { CreateIteratorMethodSpecs(iter); @@ -2630,10 +2628,7 @@ namespace Microsoft.Dafny /// Assumes the specification of the iterator itself has been successfully resolved. /// void CreateIteratorMethodSpecs(IteratorDecl iter) { - if (iter.Outs.Count != iter.OutsHistory.Count) { - // something must have gone wrong during registration, so don't worry about filling in the specs - return; - } + Contract.Requires(iter != null); // ---------- here comes the constructor ---------- // same requires clause as the iterator itself @@ -2646,7 +2641,7 @@ namespace Microsoft.Dafny ens.Add(new MaybeFreeExpression(new BinaryExpr(p.tok, BinaryExpr.Opcode.Eq, new FieldSelectExpr(p.tok, new ThisExpr(p.tok), p.Name), new IdentifierExpr(p.tok, p.Name)))); } - foreach (var p in iter.OutsHistory) { + foreach (var p in iter.OutsHistoryFields) { // ensures this.ys == []; ens.Add(new MaybeFreeExpression(new BinaryExpr(p.tok, BinaryExpr.Opcode.Eq, new FieldSelectExpr(p.tok, new ThisExpr(p.tok), p.Name), new SeqDisplayExpr(p.tok, new List())))); @@ -2695,7 +2690,6 @@ namespace Microsoft.Dafny new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), iter.DecreasesFields[i].Name), new OldExpr(iter.tok, p)))); } - // ---------- here comes predicate Valid() ---------- var reads = iter.Member_Valid.Reads; @@ -2704,50 +2698,31 @@ namespace Microsoft.Dafny reads.Add(new FrameExpression(iter.tok, new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), "_new"), null)); // reads this._new; // ---------- here comes method MoveNext() ---------- - // Build a substitution from the formals/variables to the corresponding fields. Note, because these substitutions - // will be applied to an already resolved expression, the recursive idempotent Resolve operation on these method - // specifications may not reach down to these new parts. Hence, these must be resolved right away (and they had better - // produce the same types as the subexpression they are replacing). - var substMap = new Dictionary(); - foreach (var p in iter.Ins.Concat(iter.Outs.Concat(iter.OutsHistory.Concat(iter.ExtraVars)))) { - var f = (Field)iter.Members.Find(member => member is Field && member.Name == p.Name); - if (f == null) { - // something must have gone wrong during registration, so don't worry about adding this parameter to the substitution map - } else { - var th = new ThisExpr(p.tok); - th.Type = GetThisType(p.tok, iter); // resolve here - var pe = new FieldSelectExpr(p.tok, th, p.Name); - pe.Field = f; pe.Type = p.Type; // resolve here - substMap.Add(p, pe); - } - } - var subst = new Translator.Substituter(null, substMap); // requires this.Valid(); var req = iter.Member_MoveNext.Req; req.Add(new MaybeFreeExpression(new FunctionCallExpr(iter.tok, "Valid", new ThisExpr(iter.tok), iter.tok, new List()))); - // requires YieldRequires[subst]; - foreach (var yp in iter.YieldRequires) { - req.Add(new MaybeFreeExpression(subst.Substitute(yp.E), yp.IsFree, subst.SubstAttributes(yp.Attributes))); - } + // requires YieldRequires; + req.AddRange(iter.YieldRequires); // modifies this, this._modifies, this._new; - iter.Member_MoveNext.Mod.Expressions.Add(new FrameExpression(iter.tok, new ThisExpr(iter.tok), null)); - iter.Member_MoveNext.Mod.Expressions.Add(new FrameExpression(iter.tok, new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), "_modifies"), null)); - iter.Member_MoveNext.Mod.Expressions.Add(new FrameExpression(iter.tok, new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), "_new"), null)); - // ensures more ==> this.Valid(); - ens = iter.Member_MoveNext.Ens; - ens.Add(new MaybeFreeExpression(new BinaryExpr(iter.tok, BinaryExpr.Opcode.Imp, - new IdentifierExpr(iter.tok, "more"), - new FunctionCallExpr(iter.tok, "Valid", new ThisExpr(iter.tok), iter.tok, new List())))); + var mod = iter.Member_MoveNext.Mod.Expressions; + mod.Add(new FrameExpression(iter.tok, new ThisExpr(iter.tok), null)); + mod.Add(new FrameExpression(iter.tok, new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), "_modifies"), null)); + mod.Add(new FrameExpression(iter.tok, new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), "_new"), null)); // ensures fresh(_new - old(_new)); + ens = iter.Member_MoveNext.Ens; ens.Add(new MaybeFreeExpression(new FreshExpr(iter.tok, new BinaryExpr(iter.tok, BinaryExpr.Opcode.Sub, new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), "_new"), new OldExpr(iter.tok, new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), "_new")))))); + // ensures more ==> this.Valid(); + ens.Add(new MaybeFreeExpression(new BinaryExpr(iter.tok, BinaryExpr.Opcode.Imp, + new IdentifierExpr(iter.tok, "more"), + new FunctionCallExpr(iter.tok, "Valid", new ThisExpr(iter.tok), iter.tok, new List())))); // ensures this.ys == if more then old(this.ys) + [this.y] else old(this.ys); - Contract.Assert(iter.Outs.Count == iter.OutsHistory.Count); - for (int i = 0; i < iter.Outs.Count; i++) { - var y = iter.Outs[i]; - var ys = iter.OutsHistory[i]; + Contract.Assert(iter.OutsFields.Count == iter.OutsHistoryFields.Count); + for (int i = 0; i < iter.OutsFields.Count; i++) { + var y = iter.OutsFields[i]; + var ys = iter.OutsHistoryFields[i]; var ite = new ITEExpr(iter.tok, new IdentifierExpr(iter.tok, "more"), new BinaryExpr(iter.tok, BinaryExpr.Opcode.Add, new OldExpr(iter.tok, new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), ys.Name)), @@ -2756,17 +2731,17 @@ namespace Microsoft.Dafny var eq = new BinaryExpr(iter.tok, BinaryExpr.Opcode.Eq, new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), ys.Name), ite); ens.Add(new MaybeFreeExpression(eq)); } - // ensures more ==> YieldEnsures[subst]; + // ensures more ==> YieldEnsures; foreach (var ye in iter.YieldEnsures) { - ens.Add(new MaybeFreeExpression(new BinaryExpr(iter.tok, BinaryExpr.Opcode.Imp, - new IdentifierExpr(iter.tok, "more"), subst.Substitute(ye.E)), + ens.Add(new MaybeFreeExpression( + new BinaryExpr(iter.tok, BinaryExpr.Opcode.Imp, new IdentifierExpr(iter.tok, "more"), ye.E), ye.IsFree)); } - // ensures !more ==> Ensures[subst]; + // ensures !more ==> Ensures; foreach (var e in iter.Ensures) { ens.Add(new MaybeFreeExpression(new BinaryExpr(iter.tok, BinaryExpr.Opcode.Imp, new UnaryExpr(iter.tok, UnaryExpr.Opcode.Not, new IdentifierExpr(iter.tok, "more")), - subst.Substitute(e.E)), + e.E), e.IsFree)); } // decreases this._decreases0, this._decreases1, ...; @@ -2775,7 +2750,7 @@ namespace Microsoft.Dafny var p = iter.Decreases.Expressions[i]; iter.Member_MoveNext.Decreases.Expressions.Add(new FieldSelectExpr(p.tok, new ThisExpr(p.tok), iter.DecreasesFields[i].Name)); } - iter.Member_MoveNext.Decreases.Attributes = subst.SubstAttributes(iter.Decreases.Attributes); + iter.Member_MoveNext.Decreases.Attributes = iter.Decreases.Attributes; } /// diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs index bb998e1b..a65da1ca 100644 --- a/Dafny/Translator.cs +++ b/Dafny/Translator.cs @@ -715,7 +715,7 @@ namespace Microsoft.Dafny { ExpressionTranslator etran = new ExpressionTranslator(this, predef, iter.tok); Bpl.VariableSeq inParams, outParams; - GenerateMethodParameters(iter.tok, iter, etran, out inParams, out outParams); + GenerateMethodParametersChoose(iter.tok, iter, true, true, false, etran, out inParams, out outParams); var req = new Bpl.RequiresSeq(); var mod = new Bpl.IdentifierExprSeq(); @@ -787,25 +787,12 @@ namespace Microsoft.Dafny { Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(iter.TypeArgs); Bpl.VariableSeq inParams = Bpl.Formal.StripWhereClauses(proc.InParams); - Bpl.VariableSeq outParams = Bpl.Formal.StripWhereClauses(proc.OutParams); + Contract.Assert(1 <= inParams.Length); // there should at least be a receiver parameter + Contract.Assert(proc.OutParams.Length == 0); var builder = new Bpl.StmtListBuilder(); var etran = new ExpressionTranslator(this, predef, iter.tok); var localVariables = new Bpl.VariableSeq(); - GenerateIteratorImplPrelude(iter, inParams, outParams, builder, localVariables); - - foreach (var p in iter.OutsHistory) { - // var ys: seq<...>; - // TODO: should this variable have a 'where' clause? - localVariables.Add(new Bpl.LocalVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type)))); - } - foreach (var p in iter.ExtraVars) { - // var extra: T; - // TODO: should this variable have a 'where' clause? - localVariables.Add(new Bpl.LocalVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type)))); - } - - Bpl.StmtList stmts; // check well-formedness of the preconditions, and then assume each one of them @@ -813,18 +800,23 @@ namespace Microsoft.Dafny { CheckWellformed(p.E, new WFOptions(), localVariables, builder, etran); builder.Add(new Bpl.AssumeCmd(p.E.tok, etran.TrExpr(p.E))); } + // check well-formedness of the decreases clauses + foreach (var p in iter.Decreases.Expressions) { + CheckWellformed(p, new WFOptions(), localVariables, builder, etran); + } // Note: the reads and modifies clauses are not checked for well-formedness (is that sound?), because it used to // be that the syntax was not rich enough for programmers to specify modifies clauses and always being // absolutely well-defined. - // check well-formedness of the decreases clauses - foreach (var p in iter.Decreases.Expressions) - { - CheckWellformed(p, new WFOptions(), localVariables, builder, etran); + + // Next, we assume about this.* whatever we said that the iterator constructor promises + foreach (var p in iter.Member_Init.Ens) { + builder.Add(new Bpl.AssumeCmd(p.E.tok, etran.TrExpr(p.E))); } - // play havoc with the heap according to the modifies clause and inverse of the reads clause - // TODO: something like: builder.Add(new Bpl.HavocCmd(m.tok, new Bpl.IdentifierExprSeq((Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr))); + // play havoc with the heap, except at the locations prescribed by (this._reads - this._modifies) + builder.Add(new Bpl.HavocCmd(iter.tok, new Bpl.IdentifierExprSeq((Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr))); // assume the usual two-state boilerplate information + // TODO: the following line does not do exactly what we want: foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(iter.tok, iter.Modifies.Expressions/*TODO: should this also include the Reads clause?*/, etran.Old, etran, etran.Old)) { if (tri.IsFree) { @@ -832,23 +824,22 @@ namespace Microsoft.Dafny { } } - // also play havoc with the out parameters - if (outParams.Length != 0) { // don't create an empty havoc statement - Bpl.IdentifierExprSeq outH = new Bpl.IdentifierExprSeq(); - foreach (Bpl.Variable b in outParams) { - Contract.Assert(b != null); - outH.Add(new Bpl.IdentifierExpr(b.tok, b)); - } - builder.Add(new Bpl.HavocCmd(iter.tok, outH)); - } + // assume the automatic yield-requires precondition (which is always well-formed): this.Valid() + var th = new ThisExpr(iter.tok); + th.Type = Resolver.GetThisType(iter.tok, iter); // resolve here + var validCall = new FunctionCallExpr(iter.tok, "Valid", th, iter.tok, new List()); + validCall.Function = iter.Member_Valid; // resolve here + validCall.Type = Type.Bool; // resolve here + builder.Add(new Bpl.AssumeCmd(iter.tok, etran.TrExpr(validCall))); - // check wellformedness of yield requires + // check well-formedness of the user-defined part of the yield-requires foreach (var p in iter.YieldRequires) { CheckWellformed(p.E, new WFOptions(), localVariables, builder, etran); builder.Add(new Bpl.AssumeCmd(p.E.tok, etran.TrExpr(p.E))); } - // TODO: do another havoc + // simulate a modifies this, this._modifies, this._new; + // TODO // check wellformedness of postconditions var yeBuilder = new Bpl.StmtListBuilder(); @@ -868,7 +859,7 @@ namespace Microsoft.Dafny { QKeyValue kv = etran.TrAttributes(iter.Attributes, null); Bpl.Implementation impl = new Bpl.Implementation(iter.tok, proc.Name, - typeParams, inParams, outParams, + typeParams, inParams, new VariableSeq(), localVariables, stmts, kv); sink.TopLevelDeclarations.Add(impl); @@ -892,27 +883,24 @@ namespace Microsoft.Dafny { Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(iter.TypeArgs); Bpl.VariableSeq inParams = Bpl.Formal.StripWhereClauses(proc.InParams); - Bpl.VariableSeq outParams = Bpl.Formal.StripWhereClauses(proc.OutParams); + Contract.Assert(1 <= inParams.Length); // there should at least be a receiver parameter + Contract.Assert(proc.OutParams.Length == 0); Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder(); ExpressionTranslator etran = new ExpressionTranslator(this, predef, iter.tok); Bpl.VariableSeq localVariables = new Bpl.VariableSeq(); - GenerateIteratorImplPrelude(iter, inParams, outParams, builder, localVariables); + GenerateIteratorImplPrelude(iter, inParams, new VariableSeq(), builder, localVariables); + // add locals for the yield-history variables and the extra variables - foreach (var p in iter.OutsHistory) { - // var ys: seq<...>; - // TODO: should this variable have a 'where' clause? - localVariables.Add(new Bpl.LocalVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type)))); - // ys := []; - var ys = etran.TrVar(p.tok, p); - builder.Add(Bpl.Cmd.SimpleAssign(p.tok, ys, FunctionCall(p.tok, BuiltinFunction.SeqEmpty, predef.BoxType))); - } - foreach (var p in iter.ExtraVars) { - // var extra: T; - // TODO: should this variable have a 'where' clause? - localVariables.Add(new Bpl.LocalVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type)))); - } - // also add the _yieldCount variable, and assume its initial value to be 0 + // Assume the precondition and postconditions of the iterator constructor method + foreach (var p in iter.Member_Init.Req) { + builder.Add(new Bpl.AssumeCmd(p.E.tok, etran.TrExpr(p.E))); + } + foreach (var p in iter.Member_Init.Ens) { + // these postconditions are two-state predicates, but that's okay, because we haven't changed anything yet + builder.Add(new Bpl.AssumeCmd(p.E.tok, etran.TrExpr(p.E))); + } + // add the _yieldCount variable, and assume its initial value to be 0 yieldCountVariable = new Bpl.LocalVariable(iter.tok, new Bpl.TypedIdent(iter.tok, "_yieldCount", Bpl.Type.Int)); yieldCountVariable.TypedIdent.WhereExpr = YieldCountAssumption(iter, etran); // by doing this after setting "yieldCountVariable", the variable can be used by YieldCountAssumption localVariables.Add(yieldCountVariable); @@ -930,7 +918,7 @@ namespace Microsoft.Dafny { QKeyValue kv = etran.TrAttributes(iter.Attributes, null); Bpl.Implementation impl = new Bpl.Implementation(iter.tok, proc.Name, - typeParams, inParams, outParams, + typeParams, inParams, new VariableSeq(), localVariables, stmts, kv); sink.TopLevelDeclarations.Add(impl); @@ -947,11 +935,13 @@ namespace Microsoft.Dafny { Contract.Requires(etran != null); Contract.Requires(yieldCountVariable != null); Bpl.Expr wh = Bpl.Expr.True; - foreach (var ys in iter.OutsHistory) { - // add the conjunct: _yieldCount == |ys| + foreach (var ys in iter.OutsHistoryFields) { + // add the conjunct: _yieldCount == |this.ys| wh = Bpl.Expr.And(wh, Bpl.Expr.Eq(new Bpl.IdentifierExpr(iter.tok, yieldCountVariable), - FunctionCall(iter.tok, BuiltinFunction.SeqLength, null, etran.TrVar(iter.tok, ys)))); - + FunctionCall(iter.tok, BuiltinFunction.SeqLength, null, + ExpressionTranslator.ReadHeap(iter.tok, etran.HeapExpr, + new Bpl.IdentifierExpr(iter.tok, etran.This, predef.RefType), + new Bpl.IdentifierExpr(iter.tok, GetField(ys)))))); } return wh; } @@ -3718,9 +3708,14 @@ namespace Microsoft.Dafny { } private void GenerateMethodParameters(IToken tok, ICodeContext m, ExpressionTranslator etran, out Bpl.VariableSeq inParams, out Bpl.VariableSeq outParams) { + GenerateMethodParametersChoose(tok, m, !m.IsStatic, true, true, etran, out inParams, out outParams); + } + + private void GenerateMethodParametersChoose(IToken tok, ICodeContext m, bool includeReceiver, bool includeInParams, bool includeOutParams, + ExpressionTranslator etran, out Bpl.VariableSeq inParams, out Bpl.VariableSeq outParams) { inParams = new Bpl.VariableSeq(); outParams = new Bpl.VariableSeq(); - if (!m.IsStatic) { + if (includeReceiver) { var receiverType = m is MemberDecl ? Resolver.GetReceiverType(tok, (MemberDecl)m) : Resolver.GetThisType(tok, (IteratorDecl)m); Bpl.Expr wh = Bpl.Expr.And( Bpl.Expr.Neq(new Bpl.IdentifierExpr(tok, "this", predef.RefType), predef.Null), @@ -3728,19 +3723,24 @@ namespace Microsoft.Dafny { Bpl.Formal thVar = new Bpl.Formal(tok, new Bpl.TypedIdent(tok, "this", predef.RefType, wh), true); inParams.Add(thVar); } - foreach (Formal p in m.Ins) { - Bpl.Type varType = TrType(p.Type); - Bpl.Expr wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.UniqueName, varType), p.Type, etran); - inParams.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, varType, wh), true)); + if (includeInParams) { + foreach (Formal p in m.Ins) { + Bpl.Type varType = TrType(p.Type); + Bpl.Expr wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.UniqueName, varType), p.Type, etran); + inParams.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, varType, wh), true)); + } } - foreach (Formal p in m.Outs) { - Bpl.Type varType = TrType(p.Type); - Bpl.Expr wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.UniqueName, varType), p.Type, etran); - outParams.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, varType, wh), false)); + if (includeOutParams) { + foreach (Formal p in m.Outs) { + Bpl.Type varType = TrType(p.Type); + Bpl.Expr wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.UniqueName, varType), p.Type, etran); + outParams.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, varType, wh), false)); + } } } - class BoilerplateTriple { // a triple that is now a quintuple + class BoilerplateTriple + { // a triple that is now a quintuple [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(tok != null); @@ -4103,21 +4103,24 @@ namespace Microsoft.Dafny { AddComment(builder, s, "yield statement"); Contract.Assert(codeContext is IteratorDecl); var iter = (IteratorDecl)codeContext; - // ys := ys + [y]; - Contract.Assert(iter.Outs.Count == iter.OutsHistory.Count); - for (int i = 0; i < iter.Outs.Count; i++) { - var y = iter.Outs[i]; - var dafnyY = new IdentifierExpr(s.Tok, y.Name); - dafnyY.Var = y; dafnyY.Type = y.Type; // resolve here - var ys = iter.OutsHistory[i]; - var dafnyYs = new IdentifierExpr(s.Tok, ys.Name); - dafnyYs.Var = ys; dafnyYs.Type = ys.Type; // resolve here + // this.ys := this.ys + [this.y]; + var th = new ThisExpr(iter.tok); + th.Type = Resolver.GetThisType(iter.tok, iter); // resolve here + Contract.Assert(iter.OutsFields.Count == iter.OutsHistoryFields.Count); + for (int i = 0; i < iter.OutsFields.Count; i++) { + var y = iter.OutsFields[i]; + var dafnyY = new FieldSelectExpr(s.Tok, th, y.Name); + dafnyY.Field = y; dafnyY.Type = y.Type; // resolve here + var ys = iter.OutsHistoryFields[i]; + var dafnyYs = new FieldSelectExpr(s.Tok, th, ys.Name); + dafnyYs.Field = ys; dafnyYs.Type = ys.Type; // resolve here var dafnySingletonY = new SeqDisplayExpr(s.Tok, new List() { dafnyY }); dafnySingletonY.Type = ys.Type; // resolve here var rhs = new BinaryExpr(s.Tok, BinaryExpr.Opcode.Add, dafnyYs, dafnySingletonY); rhs.ResolvedOp = BinaryExpr.ResolvedOpcode.Concat; rhs.Type = ys.Type; // resolve here - var cmd = Bpl.Cmd.SimpleAssign(s.Tok, etran.TrVar(s.Tok, ys), etran.TrExpr(rhs)); + var cmd = Bpl.Cmd.SimpleAssign(s.Tok, (Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr, + ExpressionTranslator.UpdateHeap(s.Tok, etran.HeapExpr, etran.TrExpr(th), new Bpl.IdentifierExpr(s.Tok, GetField(ys)), etran.TrExpr(rhs))); builder.Add(cmd); } // yieldCount := yieldCount + 1; assume yieldCount == |ys|; -- cgit v1.2.3