From 12c5cf9976f7c4993db5b930bf8bce0b64c428a1 Mon Sep 17 00:00:00 2001 From: rustanleino Date: Thu, 11 Mar 2010 07:08:51 +0000 Subject: Dafny: * Enforce ghost vs. non-ghost separation * Allow ghost parameters and ghost locals * Functions are ghost, but allow the non-ghost "function method" --- Source/Dafny/Dafny.atg | 53 ++++--- Source/Dafny/DafnyAst.ssc | 40 ++++- Source/Dafny/Parser.ssc | 60 +++++--- Source/Dafny/Printer.ssc | 8 + Source/Dafny/Resolver.ssc | 347 ++++++++++++++++++++++++++++++-------------- Source/Dafny/Translator.ssc | 6 +- 6 files changed, 355 insertions(+), 159 deletions(-) (limited to 'Source') diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index d6f3aeae..069c88c3 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -36,10 +36,11 @@ struct MemberModifiers { // helper routine for parsing call statements private static void RecordCallLhs(IdentifierExpr! e, List! lhs, - List! newVars) { + List! newVars) { + int index = lhs.Count; lhs.Add(e); if (parseVarScope.Find(e.Name) == null) { - VarDecl d = new VarDecl(e.tok, e.Name, new InferredTypeProxy(), null); + AutoVarDecl d = new AutoVarDecl(e.tok, e.Name, new InferredTypeProxy(), index); newVars.Add(d); parseVarScope.Push(e.Name, e.Name); } @@ -207,6 +208,14 @@ FieldDecl! mm> ";" . +GIdentType +/* isGhost always returns as false if allowGhost is false */ += (. isGhost = false; .) + [ "ghost" (. if (allowGhost) { isGhost = true; } else { SemErr(token, "formal cannot be declared 'ghost' in this context"); } .) + ] + IdentType + . + IdentType = Ident ":" @@ -276,9 +285,9 @@ MethodDecl Ident [ GenericParameters ] (. parseVarScope.PushMarker(); .) - Formals + Formals [ "returns" - Formals + Formals ] ( ";" { MethodSpec } @@ -307,12 +316,12 @@ MethodSpec! req, List! mod, List! formals> -= (. Token! id; Type! ty; .) +Formals! formals> += (. Token! id; Type! ty; bool isGhost; .) "(" [ - IdentType (. formals.Add(new Formal(id, id.val, ty, incoming)); parseVarScope.Push(id.val, id.val); .) - { "," IdentType (. formals.Add(new Formal(id, id.val, ty, incoming)); parseVarScope.Push(id.val, id.val); .) + GIdentType (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); parseVarScope.Push(id.val, id.val); .) + { "," GIdentType (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); parseVarScope.Push(id.val, id.val); .) } ] ")" @@ -322,8 +331,8 @@ FormalsOptionalIds! formals> = (. Token! id; Type! ty; string! name; .) "(" [ - TypeIdentOptional (. formals.Add(new Formal(id, name, ty, true)); parseVarScope.Push(name, name); .) - { "," TypeIdentOptional (. formals.Add(new Formal(id, name, ty, true)); parseVarScope.Push(name, name); .) + TypeIdentOptional (. formals.Add(new Formal(id, name, ty, true, false)); parseVarScope.Push(name, name); .) + { "," TypeIdentOptional (. formals.Add(new Formal(id, name, ty, true, false)); parseVarScope.Push(name, name); .) } ] ")" @@ -390,15 +399,18 @@ FunctionDecl List reads = new List(); List decreases = new List(); Expression! bb; Expression body = null; + bool isFunctionMethod = false; .) "function" - (. if (mmod.IsGhost) { SemErr(token, "functions cannot be declared 'ghost'"); } + [ "method" (. isFunctionMethod = true; .) + ] + (. if (mmod.IsGhost) { SemErr(token, "functions cannot be declared 'ghost' (they are ghost by default)"); } .) { Attribute } Ident [ GenericParameters ] (. parseVarScope.PushMarker(); .) - Formals + Formals ":" Type ( ";" @@ -407,7 +419,7 @@ FunctionDecl FunctionBody (. body = bb; .) ) (. parseVarScope.PopMarker(); - f = new Function(id, id.val, mmod.IsClass, mmod.IsUse, typeArgs, formals, returnType, reqs, reads, decreases, body, attrs); + f = new Function(id, id.val, mmod.IsClass, !isFunctionMethod, mmod.IsUse, typeArgs, formals, returnType, reqs, reads, decreases, body, attrs); .) . @@ -580,16 +592,17 @@ LhsExpr . VarDeclStmts! ss> -= (. VarDecl! d; .) - [ "ghost" ] += (. VarDecl! d; bool isGhost = false; .) + [ "ghost" (. isGhost = true; .) + ] "var" - IdentTypeRhs (. ss.Add(d); parseVarScope.Push(d.Name, d.Name); .) - { "," IdentTypeRhs (. ss.Add(d); parseVarScope.Push(d.Name, d.Name); .) + IdentTypeRhs (. ss.Add(d); parseVarScope.Push(d.Name, d.Name); .) + { "," IdentTypeRhs (. ss.Add(d); parseVarScope.Push(d.Name, d.Name); .) } ";" . -IdentTypeRhs +IdentTypeRhs = (. Token! id; Type! ty; Expression! e; Expression rhs = null; Type newType = null; Type optionalType = null; DeterminedAssignmentRhs optionalRhs = null; @@ -608,7 +621,7 @@ IdentTypeRhs } else if (optionalType == null) { optionalType = new InferredTypeProxy(); } - d = new VarDecl(id, id.val, optionalType, optionalRhs); + d = new VarDecl(id, id.val, optionalType, isGhost, optionalRhs); .) . @@ -664,7 +677,7 @@ CallStmt = (. Token! x, id; Expression! e; List lhs = new List(); - List newVars = new List(); + List newVars = new List(); .) "call" (. x = token; .) CallStmtSubExpr diff --git a/Source/Dafny/DafnyAst.ssc b/Source/Dafny/DafnyAst.ssc index ca49e940..b73bacc9 100644 --- a/Source/Dafny/DafnyAst.ssc +++ b/Source/Dafny/DafnyAst.ssc @@ -415,6 +415,7 @@ namespace Microsoft.Dafny string! UniqueName { get; } Type! Type { get; } bool IsMutable { get; } + bool IsGhost { get; } } public abstract class NonglobalVariable : IVariable { @@ -440,11 +441,14 @@ namespace Microsoft.Dafny } } } public abstract bool IsMutable { get; } + readonly bool isGhost; + public bool IsGhost { get { return isGhost; } } - public NonglobalVariable(Token! tok, string! name, Type! type) { + public NonglobalVariable(Token! tok, string! name, Type! type, bool isGhost) { this.tok = tok; this.name = name; this.type = type; + this.isGhost = isGhost; } internal static int varIdCount; // this varIdCount is used for both NonglobalVariable's and VarDecl's. @@ -454,9 +458,9 @@ namespace Microsoft.Dafny public readonly bool InParam; // true to in-parameter, false for out-parameter public override bool IsMutable { get { return !InParam; } } - public Formal(Token! tok, string! name, Type! type, bool inParam) { + public Formal(Token! tok, string! name, Type! type, bool inParam, bool isGhost) { InParam = inParam; - base(tok, name, type); + base(tok, name, type, isGhost); } } @@ -464,12 +468,13 @@ namespace Microsoft.Dafny public override bool IsMutable { get { return false; } } public BoundVar(Token! tok, string! name, Type! type) { - base(tok, name, type); + base(tok, name, type, false); } } public class Function : MemberDecl, TypeParameter.ParentType { public readonly bool IsClass; + public readonly bool IsGhost; // functions are "ghost" by default; a non-ghost function is called a "function method" public readonly bool IsUse; public readonly List! TypeArgs; public readonly List! Formals; @@ -479,9 +484,10 @@ namespace Microsoft.Dafny public readonly List! Decreases; public readonly Expression Body; // an extended expression - public Function(Token! tok, string! name, bool isClass, bool isUse, [Captured] List! typeArgs, [Captured] List! formals, Type! resultType, + public Function(Token! tok, string! name, bool isClass, bool isGhost, bool isUse, [Captured] List! typeArgs, [Captured] List! formals, Type! resultType, List! req, List! reads, List! decreases, Expression body, Attributes attributes) { this.IsClass = isClass; + this.IsGhost = isGhost; this.IsUse = isUse; this.TypeArgs = typeArgs; this.Formals = formals; @@ -698,29 +704,47 @@ namespace Microsoft.Dafny } } } public bool IsMutable { get { return true; } } + protected bool isGhost; + public bool IsGhost { get { return isGhost; } } public readonly DeterminedAssignmentRhs Rhs; invariant OptionalType != null || Rhs != null; - public VarDecl(Token! tok, string! name, Type type, DeterminedAssignmentRhs rhs) + public VarDecl(Token! tok, string! name, Type type, bool isGhost, DeterminedAssignmentRhs rhs) requires type != null || rhs != null; { this.name = name; this.OptionalType = type; + this.isGhost = isGhost; this.Rhs = rhs; base(tok); } } + public class AutoVarDecl : VarDecl { + public readonly int Index; + public AutoVarDecl(Token! tok, string! name, Type! type, int index) + { + Index = index; + base(tok, name, type, false, null); + } + /// + /// This method retrospectively makes the VarDecl a ghost. It is to be used only during resolution. + /// + public void MakeGhost() { + isGhost = true; + } + } + public class CallStmt : Statement { - public readonly List! NewVars; + public readonly List! NewVars; public readonly List! Lhs; public readonly Expression! Receiver; public readonly string! MethodName; public readonly List! Args; public Method Method; // filled in by resolution - public CallStmt(Token! tok, List! newVars, List! lhs, Expression! receiver, string! methodName, List! args) { + public CallStmt(Token! tok, List! newVars, List! lhs, Expression! receiver, string! methodName, List! args) { this.NewVars = newVars; this.Lhs = lhs; this.Receiver = receiver; diff --git a/Source/Dafny/Parser.ssc b/Source/Dafny/Parser.ssc index 0560a45b..3a349f43 100644 --- a/Source/Dafny/Parser.ssc +++ b/Source/Dafny/Parser.ssc @@ -34,10 +34,11 @@ struct MemberModifiers { // helper routine for parsing call statements private static void RecordCallLhs(IdentifierExpr! e, List! lhs, - List! newVars) { + List! newVars) { + int index = lhs.Count; lhs.Add(e); if (parseVarScope.Find(e.Name) == null) { - VarDecl d = new VarDecl(e.tok, e.Name, new InferredTypeProxy(), null); + AutoVarDecl d = new AutoVarDecl(e.tok, e.Name, new InferredTypeProxy(), index); newVars.Add(d); parseVarScope.Push(e.Name, e.Name); } @@ -284,9 +285,14 @@ public static int Parse (List! classes) { List reads = new List(); List decreases = new List(); Expression! bb; Expression body = null; + bool isFunctionMethod = false; Expect(30); - if (mmod.IsGhost) { SemErr(token, "functions cannot be declared 'ghost'"); } + if (t.kind == 16) { + Get(); + isFunctionMethod = true; + } + if (mmod.IsGhost) { SemErr(token, "functions cannot be declared 'ghost' (they are ghost by default)"); } while (t.kind == 5) { Attribute(ref attrs); @@ -296,7 +302,7 @@ public static int Parse (List! classes) { GenericParameters(typeArgs); } parseVarScope.PushMarker(); - Formals(true, formals); + Formals(true, false, formals); Expect(13); Type(out returnType); if (t.kind == 10) { @@ -312,7 +318,7 @@ public static int Parse (List! classes) { body = bb; } else Error(95); parseVarScope.PopMarker(); - f = new Function(id, id.val, mmod.IsClass, mmod.IsUse, typeArgs, formals, returnType, reqs, reads, decreases, body, attrs); + f = new Function(id, id.val, mmod.IsClass, !isFunctionMethod, mmod.IsUse, typeArgs, formals, returnType, reqs, reads, decreases, body, attrs); } @@ -339,10 +345,10 @@ public static int Parse (List! classes) { GenericParameters(typeArgs); } parseVarScope.PushMarker(); - Formals(true, ins); + Formals(true, true, ins); if (t.kind == 17) { Get(); - Formals(false, outs); + Formals(false, true, outs); } if (t.kind == 10) { Get(); @@ -389,11 +395,11 @@ public static int Parse (List! classes) { Expect(23); if (StartOf(5)) { TypeIdentOptional(out id, out name, out ty); - formals.Add(new Formal(id, name, ty, true)); parseVarScope.Push(name, name); + formals.Add(new Formal(id, name, ty, true, false)); parseVarScope.Push(name, name); while (t.kind == 12) { Get(); TypeIdentOptional(out id, out name, out ty); - formals.Add(new Formal(id, name, ty, true)); parseVarScope.Push(name, name); + formals.Add(new Formal(id, name, ty, true, false)); parseVarScope.Push(name, name); } } Expect(24); @@ -405,6 +411,15 @@ public static int Parse (List! classes) { Type(out ty); } + static void GIdentType(bool allowGhost, out Token! id, out Type! ty, out bool isGhost) { + isGhost = false; + if (t.kind == 7) { + Get(); + if (allowGhost) { isGhost = true; } else { SemErr(token, "formal cannot be declared 'ghost' in this context"); } + } + IdentType(out id, out ty); + } + static void Type(out Type! ty) { Token! tok; TypeAndToken(out tok, out ty); @@ -477,16 +492,16 @@ public static int Parse (List! classes) { } else Error(97); } - static void Formals(bool incoming, List! formals) { - Token! id; Type! ty; + static void Formals(bool incoming, bool allowGhosts, List! formals) { + Token! id; Type! ty; bool isGhost; Expect(23); - if (t.kind == 1) { - IdentType(out id, out ty); - formals.Add(new Formal(id, id.val, ty, incoming)); parseVarScope.Push(id.val, id.val); + if (t.kind == 1 || t.kind == 7) { + GIdentType(allowGhosts, out id, out ty, out isGhost); + formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); parseVarScope.Push(id.val, id.val); while (t.kind == 12) { Get(); - IdentType(out id, out ty); - formals.Add(new Formal(id, id.val, ty, incoming)); parseVarScope.Push(id.val, id.val); + GIdentType(allowGhosts, out id, out ty, out isGhost); + formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); parseVarScope.Push(id.val, id.val); } } Expect(24); @@ -796,16 +811,17 @@ List! decreases) { } static void VarDeclStmts(List! ss) { - VarDecl! d; + VarDecl! d; bool isGhost = false; if (t.kind == 7) { Get(); + isGhost = true; } Expect(11); - IdentTypeRhs(out d); + IdentTypeRhs(out d, isGhost); ss.Add(d); parseVarScope.Push(d.Name, d.Name); while (t.kind == 12) { Get(); - IdentTypeRhs(out d); + IdentTypeRhs(out d, isGhost); ss.Add(d); parseVarScope.Push(d.Name, d.Name); } Expect(10); @@ -872,7 +888,7 @@ List! decreases) { Token! x, id; Expression! e; List lhs = new List(); - List newVars = new List(); + List newVars = new List(); Expect(46); x = token; @@ -1064,7 +1080,7 @@ List! decreases) { } } - static void IdentTypeRhs(out VarDecl! d) { + static void IdentTypeRhs(out VarDecl! d, bool isGhost) { Token! id; Type! ty; Expression! e; Expression rhs = null; Type newType = null; Type optionalType = null; DeterminedAssignmentRhs optionalRhs = null; @@ -1087,7 +1103,7 @@ List! decreases) { } else if (optionalType == null) { optionalType = new InferredTypeProxy(); } - d = new VarDecl(id, id.val, optionalType, optionalRhs); + d = new VarDecl(id, id.val, optionalType, isGhost, optionalRhs); } diff --git a/Source/Dafny/Printer.ssc b/Source/Dafny/Printer.ssc index 23e6dfce..93b793f2 100644 --- a/Source/Dafny/Printer.ssc +++ b/Source/Dafny/Printer.ssc @@ -128,6 +128,7 @@ namespace Microsoft.Dafny { string k = "function"; if (f.IsUse) { k = "use " + k; } if (f.IsClass) { k = "class " + k; } + if (!f.IsGhost) { k += " method"; } PrintClassMethodHelper(k, f.Attributes, f.Name, f.TypeArgs); PrintFormals(f.Formals); wr.Write(": "); @@ -175,6 +176,7 @@ namespace Microsoft.Dafny { Indent(IndentAmount); string k = "method"; if (method.IsClass) { k = "class " + k; } + if (method.IsGhost) { k = "ghost " + k; } PrintClassMethodHelper(k, method.Attributes, method.Name, method.TypeArgs); PrintFormals(method.Ins); if (method.Outs.Count != 0) { @@ -213,6 +215,9 @@ namespace Microsoft.Dafny { } void PrintFormal(Formal! f) { + if (f.IsGhost) { + wr.Write("ghost "); + } if (!f.Name.StartsWith("#")) { wr.Write("{0}: ", f.Name); } @@ -303,6 +308,9 @@ namespace Microsoft.Dafny { } else if (stmt is VarDecl) { VarDecl s = (VarDecl)stmt; + if (s.IsGhost) { + wr.Write("ghost "); + } wr.Write("var {0}", s.Name); if (s.OptionalType != null) { wr.Write(": "); diff --git a/Source/Dafny/Resolver.ssc b/Source/Dafny/Resolver.ssc index df93aece..11dabf9d 100644 --- a/Source/Dafny/Resolver.ssc +++ b/Source/Dafny/Resolver.ssc @@ -276,7 +276,7 @@ namespace Microsoft.Dafny { for (; attrs != null; attrs = attrs.Prev) { foreach (Attributes.Argument aa in attrs.Args) { if (aa.E != null) { - ResolveExpression(aa.E, twoState); + ResolveExpression(aa.E, twoState, true); } } } @@ -286,7 +286,7 @@ namespace Microsoft.Dafny { // order does not matter for resolution, so resolve them in reverse order for (; trigs != null; trigs = trigs.Prev) { foreach (Expression e in trigs.Terms) { - ResolveExpression(e, twoState); + ResolveExpression(e, twoState, true); } } } @@ -331,14 +331,14 @@ namespace Microsoft.Dafny { scope.Push(p.Name, p); } foreach (Expression r in f.Req) { - ResolveExpression(r, false); + ResolveExpression(r, false, true); assert r.Type != null; // follows from postcondition of ResolveExpression if (!UnifyTypes(r.Type, Type.Bool)) { Error(r, "Precondition must be a boolean (got {0})", r.Type); } } foreach (Expression r in f.Reads) { - ResolveExpression(r, false); + ResolveExpression(r, false, true); Type t = r.Type; assert t != null; // follows from postcondition of ResolveExpression if (t is CollectionType) { @@ -353,11 +353,11 @@ namespace Microsoft.Dafny { } } foreach (Expression r in f.Decreases) { - ResolveExpression(r, false); + ResolveExpression(r, false, true); // any type is fine } if (f.Body != null) { - ResolveExpression(f.Body, false); + ResolveExpression(f.Body, false, f.IsGhost); assert f.Body.Type != null; // follows from postcondition of ResolveExpression if (!UnifyTypes(f.Body.Type, f.ResultType)) { Error(f, "Function body type mismatch (expected {0}, got {1})", f.ResultType, f.Body.Type); @@ -403,14 +403,14 @@ namespace Microsoft.Dafny { // Start resolving specification... foreach (MaybeFreeExpression e in m.Req) { - ResolveExpression(e.E, false); + ResolveExpression(e.E, false, true); assert e.E.Type != null; // follows from postcondition of ResolveExpression if (!UnifyTypes(e.E.Type, Type.Bool)) { Error(e.E, "Precondition must be a boolean (got {0})", e.E.Type); } } foreach (Expression e in m.Mod) { - ResolveExpression(e, false); + ResolveExpression(e, false, true); Type t = e.Type; assert t != null; // follows from postcondition of ResolveExpression if (t is CollectionType) { @@ -425,7 +425,7 @@ namespace Microsoft.Dafny { } } foreach (Expression e in m.Decreases) { - ResolveExpression(e, false); + ResolveExpression(e, false, true); // any type is fine } @@ -436,7 +436,7 @@ namespace Microsoft.Dafny { // ... continue resolving specification foreach (MaybeFreeExpression e in m.Ens) { - ResolveExpression(e.E, true); + ResolveExpression(e.E, true, true); 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); @@ -445,7 +445,7 @@ namespace Microsoft.Dafny { // Resolve body if (m.Body != null) { - ResolveStatement(m.Body); + ResolveStatement(m.Body, m.IsGhost); } scope.PopMarker(); @@ -722,12 +722,12 @@ namespace Microsoft.Dafny { } } - public void ResolveStatement(Statement! stmt) + public void ResolveStatement(Statement! stmt, bool specContextOnly) requires !(stmt is LabelStmt); // these should be handled inside lists of statements { if (stmt is UseStmt) { UseStmt s = (UseStmt)stmt; - ResolveExpression(s.Expr, true); + ResolveExpression(s.Expr, true, true); assert s.Expr.Type != null; // follows from postcondition of ResolveExpression Expression expr = s.Expr; while (true) { @@ -743,7 +743,7 @@ namespace Microsoft.Dafny { } } else if (stmt is PredicateStmt) { PredicateStmt s = (PredicateStmt)stmt; - ResolveExpression(s.Expr, true); + ResolveExpression(s.Expr, true, true); assert s.Expr.Type != null; // follows from postcondition of ResolveExpression if (!UnifyTypes(s.Expr.Type, Type.Bool)) { Error(s.Expr, "condition is expected to be of type {0}, but is {1}", Type.Bool, s.Expr.Type); @@ -765,20 +765,40 @@ namespace Microsoft.Dafny { } else if (stmt is AssignStmt) { AssignStmt s = (AssignStmt)stmt; - ResolveExpression(s.Lhs, true); + int prevErrorCount = ErrorCount; + ResolveExpression(s.Lhs, true, true); // allow ghosts for now, but see FieldSelectExpr LHS case below + bool lhsResolvedSuccessfully = ErrorCount == prevErrorCount; assert s.Lhs.Type != null; // follows from postcondition of ResolveExpression // check that LHS denotes a mutable variable or a field + bool lvalueIsGhost = true; if (s.Lhs is IdentifierExpr) { IVariable var = ((IdentifierExpr)s.Lhs).Var; if (var == null) { // the LHS didn't resolve correctly; some error would already have been reported - } else if (!var.IsMutable) { - Error(stmt, "LHS of assignment must denote a mutable variable or field"); + } else { + lvalueIsGhost = var.IsGhost; + if (!var.IsMutable) { + Error(stmt, "LHS of assignment must denote a mutable variable or field"); + } } } else if (s.Lhs is FieldSelectExpr) { // LHS is fine, but restrict the RHS to ExprRhs if (!(s.Rhs is ExprRhs)) { Error(stmt, "Assignment to field must have an expression RHS; try using a temporary local variable"); + } else { + FieldSelectExpr fse = (FieldSelectExpr)s.Lhs; + lvalueIsGhost = ((!)fse.Field).IsGhost; + if (!lvalueIsGhost) { + if (specContextOnly) { + Error(stmt, "Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)"); + } else { + // It is now that we wish we would have resolved s.Lhs to not allow ghosts. Too late, so we do + // the next best thing. + if (lhsResolvedSuccessfully && UsesSpecFeatures(fse.Obj)) { + Error(stmt, "Assignment to non-ghost field is not allowed to use specification-only expressions in the receiver"); + } + } + } } } else { Error(stmt, "LHS of assignment must denote a mutable variable or field"); @@ -786,7 +806,7 @@ namespace Microsoft.Dafny { if (s.Rhs is ExprRhs) { ExprRhs rr = (ExprRhs)s.Rhs; - ResolveExpression(rr.Expr, true); + ResolveExpression(rr.Expr, true, lvalueIsGhost); assert rr.Expr.Type != null; // follows from postcondition of ResolveExpression if (!UnifyTypes(s.Lhs.Type, rr.Expr.Type)) { Error(stmt, "RHS (of type {0}) not assignable to LHS (of type {1})", rr.Expr.Type, s.Lhs.Type); @@ -815,7 +835,7 @@ namespace Microsoft.Dafny { Type! rhsType; if (s.Rhs is ExprRhs) { ExprRhs rr = (ExprRhs)s.Rhs; - ResolveExpression(rr.Expr, true); + ResolveExpression(rr.Expr, true, s.IsGhost); assert rr.Expr.Type != null; // follows from postcondition of ResolveExpression rhsType = rr.Expr.Type; } else if (s.Rhs is TypeRhs) { @@ -841,72 +861,89 @@ namespace Microsoft.Dafny { } else if (stmt is CallStmt) { CallStmt s = (CallStmt)stmt; - + + // resolve receiver + ResolveReceiver(s.Receiver, true, false); + assert s.Receiver.Type != null; // follows from postcondition of ResolveExpression + // resolve the method name + UserDefinedType ctype; + MemberDecl member = ResolveMember(s.Tok, s.Receiver.Type, s.MethodName, out ctype); + Method method = null; + if (member == null) { + // error has already been reported by ResolveMember + } else if (!(member is Method)) { + Error(s, "member {0} in class {1} does not refer to a method", s.MethodName, ((!)ctype).Name); + } else { + method = (Method)member; + s.Method = method; + if (specContextOnly && !method.IsGhost) { + Error(s, "only ghost methods can be called from this context"); + } + } + // resolve any local variables declared here - foreach (VarDecl local in s.NewVars) { - ResolveStatement(local); + foreach (AutoVarDecl local in s.NewVars) { + // first, fix up the local variables to be ghost variable if the corresponding formal out-parameter is a ghost + if (method != null && local.Index < method.Outs.Count && method.Outs[local.Index].IsGhost) { + local.MakeGhost(); + } + ResolveStatement(local, specContextOnly); } // resolve left-hand side Dictionary lhsNameSet = new Dictionary(); foreach (IdentifierExpr lhs in s.Lhs) { - ResolveExpression(lhs, true); + ResolveExpression(lhs, true, true); if (lhsNameSet.ContainsKey(lhs.Name)) { Error(s, "Duplicate variable in left-hand side of call statement: {0}", lhs.Name); } else { lhsNameSet.Add(lhs.Name, null); } } - // resolve receiver - ResolveReceiver(s.Receiver, true); - assert s.Receiver.Type != null; // follows from postcondition of ResolveExpression // resolve arguments + int j = 0; foreach (Expression e in s.Args) { - ResolveExpression(e, true); + bool allowGhost = method == null || method.Ins.Count <= j || method.Ins[j].IsGhost; + ResolveExpression(e, true, allowGhost); + j++; } - // resolve the method name - UserDefinedType ctype; - MemberDecl member = ResolveMember(s.Tok, s.Receiver.Type, s.MethodName, out ctype); - if (member == null) { - // error has already been reported by ResolveMember - } else if (!(member is Method)) { - Error(s, "member {0} in class {1} does not refer to a method", s.MethodName, ((!)ctype).Name); + if (method == null) { + // error has been reported above + } else if (method.Ins.Count != s.Args.Count) { + Error(s, "wrong number of method arguments (got {0}, expected {1})", s.Args.Count, method.Ins.Count); + } else if (method.Outs.Count != s.Lhs.Count) { + Error(s, "wrong number of method result arguments (got {0}, expected {1})", s.Lhs.Count, method.Outs.Count); } else { - Method method = (Method)member; - s.Method = method; - if (method.Ins.Count != s.Args.Count) { - Error(s, "wrong number of method arguments (got {0}, expected {1})", s.Args.Count, method.Ins.Count); - } else if (method.Outs.Count != s.Lhs.Count) { - Error(s, "wrong number of method result arguments (got {0}, expected {1})", s.Lhs.Count, method.Outs.Count); - } else { - assert ctype != null; // follows from postcondition of ResolveMember - if (!scope.AllowInstance && !method.IsClass && s.Receiver is ThisExpr) { - // The call really needs an instance, but that instance is given as 'this', which is not - // available in this context. For more details, see comment in the resolution of a - // FunctionCallExpr. - Error(s.Receiver, "'this' is not allowed in a 'class' context"); - } - // build the type substitution map - Dictionary subst = new Dictionary(); - for (int i = 0; i < ctype.TypeArgs.Count; i++) { - subst.Add(((!)ctype.ResolvedClass).TypeArgs[i], ctype.TypeArgs[i]); - } - foreach (TypeParameter p in method.TypeArgs) { - subst.Add(p, new ParamTypeProxy(p)); - } - // type check the arguments - for (int i = 0; i < method.Ins.Count; i++) { - Type st = SubstType(method.Ins[i].Type, subst); - if (!UnifyTypes((!)s.Args[i].Type, st)) { - Error(s, "incorrect type of method in-parameter {0} (expected {1}, got {2})", i, st, s.Args[i].Type); - } + assert ctype != null; // follows from postcondition of ResolveMember above + if (!scope.AllowInstance && !method.IsClass && s.Receiver is ThisExpr) { + // The call really needs an instance, but that instance is given as 'this', which is not + // available in this context. For more details, see comment in the resolution of a + // FunctionCallExpr. + Error(s.Receiver, "'this' is not allowed in a 'class' context"); + } + // build the type substitution map + Dictionary subst = new Dictionary(); + for (int i = 0; i < ctype.TypeArgs.Count; i++) { + subst.Add(((!)ctype.ResolvedClass).TypeArgs[i], ctype.TypeArgs[i]); + } + foreach (TypeParameter p in method.TypeArgs) { + subst.Add(p, new ParamTypeProxy(p)); + } + // type check the arguments + for (int i = 0; i < method.Ins.Count; i++) { + Type st = SubstType(method.Ins[i].Type, subst); + if (!UnifyTypes((!)s.Args[i].Type, st)) { + Error(s, "incorrect type of method in-parameter {0} (expected {1}, got {2})", i, st, s.Args[i].Type); } - for (int i = 0; i < method.Outs.Count; i++) { - Type st = SubstType(method.Outs[i].Type, subst); - if (!UnifyTypes((!)s.Lhs[i].Type, st)) { - Error(s, "incorrect type of method out-parameter {0} (expected {1}, got {2})", i, st, s.Lhs[i].Type); - } + } + for (int i = 0; i < method.Outs.Count; i++) { + Type st = SubstType(method.Outs[i].Type, subst); + IdentifierExpr lhs = s.Lhs[i]; + if (!UnifyTypes((!)lhs.Type, st)) { + Error(s, "incorrect type of method out-parameter {0} (expected {1}, got {2})", i, st, lhs.Type); + } else if (!specContextOnly && !((!)lhs.Var).IsGhost && method.Outs[i].IsGhost) { + Error(s, "actual out-parameter {0} is required to be a ghost variable", i); } } } @@ -922,7 +959,7 @@ namespace Microsoft.Dafny { assert b; // since we just pushed a marker, we expect the Push to succeed labelsToPop++; } else { - ResolveStatement(ss); + ResolveStatement(ss, specContextOnly); for (; 0 < labelsToPop; labelsToPop--) { labeledStatements.PopMarker(); } } } @@ -931,39 +968,51 @@ namespace Microsoft.Dafny { } else if (stmt is IfStmt) { IfStmt s = (IfStmt)stmt; + bool branchesAreSpecOnly = specContextOnly; if (s.Guard != null) { - ResolveExpression(s.Guard, true); + int prevErrorCount = ErrorCount; + ResolveExpression(s.Guard, true, true); assert s.Guard.Type != null; // follows from postcondition of ResolveExpression + bool successfullyResolved = ErrorCount == prevErrorCount; if (!UnifyTypes(s.Guard.Type, Type.Bool)) { Error(s.Guard, "condition is expected to be of type {0}, but is {1}", Type.Bool, s.Guard.Type); } + if (!specContextOnly && successfullyResolved) { + branchesAreSpecOnly = UsesSpecFeatures(s.Guard); + } } - ResolveStatement(s.Thn); + ResolveStatement(s.Thn, branchesAreSpecOnly); if (s.Els != null) { - ResolveStatement(s.Els); + ResolveStatement(s.Els, branchesAreSpecOnly); } } else if (stmt is WhileStmt) { WhileStmt s = (WhileStmt)stmt; + bool bodyIsSpecOnly = specContextOnly; if (s.Guard != null) { - ResolveExpression(s.Guard, true); + int prevErrorCount = ErrorCount; + ResolveExpression(s.Guard, true, true); assert s.Guard.Type != null; // follows from postcondition of ResolveExpression + bool successfullyResolved = ErrorCount == prevErrorCount; if (!UnifyTypes(s.Guard.Type, Type.Bool)) { Error(s.Guard, "condition is expected to be of type {0}, but is {1}", Type.Bool, s.Guard.Type); } + if (!specContextOnly && successfullyResolved) { + bodyIsSpecOnly = UsesSpecFeatures(s.Guard); + } } foreach (MaybeFreeExpression inv in s.Invariants) { - ResolveExpression(inv.E, true); + ResolveExpression(inv.E, true, true); assert inv.E.Type != null; // follows from postcondition of ResolveExpression if (!UnifyTypes(inv.E.Type, Type.Bool)) { Error(inv.E, "invariant is expected to be of type {0}, but is {1}", Type.Bool, inv.E.Type); } } foreach (Expression e in s.Decreases) { - ResolveExpression(e, true); + ResolveExpression(e, true, true); // any type is fine } - ResolveStatement(s.Body); + ResolveStatement(s.Body, bodyIsSpecOnly); } else if (stmt is ForeachStmt) { ForeachStmt s = (ForeachStmt)stmt; @@ -971,24 +1020,28 @@ namespace Microsoft.Dafny { bool b = scope.Push(s.BoundVar.Name, s.BoundVar); assert b; // since we just pushed a marker, we expect the Push to succeed ResolveType(s.BoundVar.Type); + int prevErrorCount = ErrorCount; - ResolveExpression(s.Collection, true); + ResolveExpression(s.Collection, true, true); assert s.Collection.Type != null; // follows from postcondition of ResolveExpression if (!UnifyTypes(s.Collection.Type, new CollectionTypeProxy(s.BoundVar.Type))) { Error(s.Collection, "The type is expected to be a collection of {0} (instead got {1})", s.BoundVar.Type, s.Collection.Type); } - ResolveExpression(s.Range, true); + ResolveExpression(s.Range, true, true); assert s.Range.Type != null; // follows from postcondition of ResolveExpression if (!UnifyTypes(s.Range.Type, Type.Bool)) { Error(s.Range, "range condition is expected to be of type {0}, but is {1}", Type.Bool, s.Range.Type); } + bool successfullyResolvedCollectionAndRange = ErrorCount == prevErrorCount; foreach (PredicateStmt ss in s.BodyPrefix) { - ResolveStatement(ss); + ResolveStatement(ss, specContextOnly); } if (s.BodyAssign != null) { - ResolveStatement(s.BodyAssign); + bool specOnly = specContextOnly || + (successfullyResolvedCollectionAndRange && (UsesSpecFeatures(s.Collection) || UsesSpecFeatures(s.Range))); + ResolveStatement(s.BodyAssign, specOnly); // check for correct usage of BoundVar in LHS and RHS of this assignment FieldSelectExpr lhs = s.BodyAssign.Lhs as FieldSelectExpr; IdentifierExpr obj = lhs == null ? null : lhs.Obj as IdentifierExpr; @@ -1101,7 +1154,7 @@ namespace Microsoft.Dafny { /// /// "twoState" implies that "old" and "fresh" expressions are allowed /// - void ResolveExpression(Expression! expr, bool twoState) + void ResolveExpression(Expression! expr, bool twoState, bool specContext) requires currentClass != null; ensures expr.Type != null; { @@ -1140,6 +1193,9 @@ namespace Microsoft.Dafny { Error(expr, "Identifier does not denote a local variable, parameter, or bound variable: {0}", e.Name); } else { expr.Type = e.Var.Type; + if (!specContext && e.Var.IsGhost) { + Error(expr, "ghost variables are allowed only in specification contexts"); + } } } else if (expr is DatatypeValue) { @@ -1178,7 +1234,7 @@ namespace Microsoft.Dafny { } int j = 0; foreach (Expression arg in dtv.Arguments) { - ResolveExpression(arg, twoState); + ResolveExpression(arg, twoState, specContext); assert arg.Type != null; // follows from postcondition of ResolveExpression if (ctor != null && j < ctor.Formals.Count) { Type st = SubstType(ctor.Formals[j].Type, subst); @@ -1194,7 +1250,7 @@ namespace Microsoft.Dafny { DisplayExpression e = (DisplayExpression)expr; Type elementType = new InferredTypeProxy(); foreach (Expression ee in e.Elements) { - ResolveExpression(ee, twoState); + ResolveExpression(ee, twoState, specContext); assert ee.Type != null; // follows from postcondition of ResolveExpression if (!UnifyTypes(elementType, ee.Type)) { Error(ee, "All elements of display must be of the same type (got {0}, but type of previous elements is {1})", ee.Type, elementType); @@ -1208,7 +1264,7 @@ namespace Microsoft.Dafny { } else if (expr is FieldSelectExpr) { FieldSelectExpr e = (FieldSelectExpr)expr; - ResolveExpression(e.Obj, twoState); + ResolveExpression(e.Obj, twoState, specContext); assert e.Obj.Type != null; // follows from postcondition of ResolveExpression UserDefinedType ctype; MemberDecl member = ResolveMember(expr.tok, e.Obj.Type, e.FieldName, out ctype); @@ -1225,12 +1281,15 @@ namespace Microsoft.Dafny { subst.Add(ctype.ResolvedClass.TypeArgs[i], ctype.TypeArgs[i]); } e.Type = SubstType(e.Field.Type, subst); + if (!specContext && e.Field.IsGhost) { + Error(expr, "ghost fields are allowed only in specification contexts"); + } } } else if (expr is SeqSelectExpr) { SeqSelectExpr e = (SeqSelectExpr)expr; bool seqErr = false; - ResolveExpression(e.Seq, twoState); + ResolveExpression(e.Seq, twoState, specContext); assert e.Seq.Type != null; // follows from postcondition of ResolveExpression Type elementType = new InferredTypeProxy(); if (!UnifyTypes(e.Seq.Type, new SeqType(elementType))) { @@ -1238,14 +1297,14 @@ namespace Microsoft.Dafny { seqErr = true; } if (e.E0 != null) { - ResolveExpression(e.E0, twoState); + ResolveExpression(e.E0, twoState, specContext); assert e.E0.Type != null; // follows from postcondition of ResolveExpression if (!UnifyTypes(e.E0.Type, Type.Int)) { Error(e.E0, "sequence selection requires integer indices (got {0})", e.E0.Type); } } if (e.E1 != null) { - ResolveExpression(e.E1, twoState); + ResolveExpression(e.E1, twoState, specContext); assert e.E1.Type != null; // follows from postcondition of ResolveExpression if (!UnifyTypes(e.E1.Type, Type.Int)) { Error(e.E1, "sequence selection requires integer indices (got {0})", e.E1.Type); @@ -1262,19 +1321,19 @@ namespace Microsoft.Dafny { } else if (expr is SeqUpdateExpr) { SeqUpdateExpr e = (SeqUpdateExpr)expr; bool seqErr = false; - ResolveExpression(e.Seq, twoState); + ResolveExpression(e.Seq, twoState, specContext); assert e.Seq.Type != null; // follows from postcondition of ResolveExpression Type elementType = new InferredTypeProxy(); if (!UnifyTypes(e.Seq.Type, new SeqType(elementType))) { Error(expr, "sequence update requires a sequence (got {0})", e.Seq.Type); seqErr = true; } - ResolveExpression(e.Index, twoState); + ResolveExpression(e.Index, twoState, specContext); assert e.Index.Type != null; // follows from postcondition of ResolveExpression if (!UnifyTypes(e.Index.Type, Type.Int)) { Error(e.Index, "sequence update requires integer index (got {0})", e.Index.Type); } - ResolveExpression(e.Value, twoState); + ResolveExpression(e.Value, twoState, specContext); assert e.Value.Type != null; // follows from postcondition of ResolveExpression if (!UnifyTypes(e.Value.Type, elementType)) { Error(e.Value, "sequence update requires the value to have the element type of the sequence (got {0})", e.Value.Type); @@ -1285,7 +1344,7 @@ namespace Microsoft.Dafny { } else if (expr is FunctionCallExpr) { FunctionCallExpr e = (FunctionCallExpr)expr; - ResolveReceiver(e.Receiver, twoState); + ResolveReceiver(e.Receiver, twoState, specContext); assert e.Receiver.Type != null; // follows from postcondition of ResolveExpression UserDefinedType ctype; MemberDecl member = ResolveMember(expr.tok, e.Receiver.Type, e.Name, out ctype); @@ -1296,6 +1355,9 @@ namespace Microsoft.Dafny { } else { Function function = (Function)member; e.Function = function; + if (!specContext && function.IsGhost) { + Error(expr, "function calls are allowed only in specification contexts (consider declaring the function a 'function method')"); + } if (function.Formals.Count != e.Args.Count) { Error(expr, "wrong number of function arguments (got {0}, expected {1})", e.Args.Count, function.Formals.Count); } else { @@ -1321,7 +1383,7 @@ namespace Microsoft.Dafny { // type check the arguments for (int i = 0; i < function.Formals.Count; i++) { Expression farg = e.Args[i]; - ResolveExpression(farg, twoState); + ResolveExpression(farg, twoState, specContext); assert farg.Type != null; // follows from postcondition of ResolveExpression Type s = SubstType(function.Formals[i].Type, subst); if (!UnifyTypes(farg.Type, s)) { @@ -1337,7 +1399,7 @@ namespace Microsoft.Dafny { if (!twoState) { Error(expr, "old expressions are not allowed in this context"); } - ResolveExpression(e.E, twoState); + ResolveExpression(e.E, twoState, specContext); expr.Type = e.E.Type; } else if (expr is FreshExpr) { @@ -1345,7 +1407,7 @@ namespace Microsoft.Dafny { if (!twoState) { Error(expr, "fresh expressions are not allowed in this context"); } - ResolveExpression(e.E, twoState); + ResolveExpression(e.E, twoState, specContext); // the type of e.E must be either an object or a collection of objects Type t = e.E.Type; assert t != null; // follows from postcondition of ResolveExpression @@ -1363,7 +1425,7 @@ namespace Microsoft.Dafny { } else if (expr is UnaryExpr) { UnaryExpr e = (UnaryExpr)expr; - ResolveExpression(e.E, twoState); + ResolveExpression(e.E, twoState, specContext); assert e.E.Type != null; // follows from postcondition of ResolveExpression switch (e.Op) { case UnaryExpr.Opcode.Not: @@ -1384,9 +1446,9 @@ namespace Microsoft.Dafny { } else if (expr is BinaryExpr) { BinaryExpr e = (BinaryExpr)expr; - ResolveExpression(e.E0, twoState); + ResolveExpression(e.E0, twoState, specContext); assert e.E0.Type != null; // follows from postcondition of ResolveExpression - ResolveExpression(e.E1, twoState); + ResolveExpression(e.E1, twoState, specContext); assert e.E1.Type != null; // follows from postcondition of ResolveExpression switch (e.Op) { case BinaryExpr.Opcode.Iff: @@ -1490,13 +1552,16 @@ namespace Microsoft.Dafny { } else if (expr is QuantifierExpr) { QuantifierExpr e = (QuantifierExpr)expr; scope.PushMarker(); + if (!specContext) { + Error(expr, "quantifiers are allowed only in specification contexts"); + } foreach (BoundVar v in e.BoundVars) { if (!scope.Push(v.Name, v)) { - Error(v, "Duplicate parameter name: {0}", v.Name); + Error(v, "Duplicate bound-variable name: {0}", v.Name); } ResolveType(v.Type); } - ResolveExpression(e.Body, twoState); + ResolveExpression(e.Body, twoState, specContext); assert e.Body.Type != null; // follows from postcondition of ResolveExpression if (!UnifyTypes(e.Body.Type, Type.Bool)) { Error(expr, "body of quantifier must be of type bool (instead got {0})", e.Body.Type); @@ -1513,11 +1578,11 @@ namespace Microsoft.Dafny { } else if (expr is ITEExpr) { ITEExpr e = (ITEExpr)expr; - ResolveExpression(e.Test, twoState); + ResolveExpression(e.Test, twoState, specContext); assert e.Test.Type != null; // follows from postcondition of ResolveExpression - ResolveExpression(e.Thn, twoState); + ResolveExpression(e.Thn, twoState, specContext); assert e.Thn.Type != null; // follows from postcondition of ResolveExpression - ResolveExpression(e.Els, twoState); + ResolveExpression(e.Els, twoState, specContext); assert e.Els.Type != null; // follows from postcondition of ResolveExpression if (!UnifyTypes(e.Test.Type, Type.Bool)) { Error(expr, "guard condition in if-then-else expression must be a boolean (instead got {0})", e.Test.Type); @@ -1531,7 +1596,7 @@ namespace Microsoft.Dafny { } else if (expr is MatchExpr) { MatchExpr me = (MatchExpr)expr; assert !twoState; // currently, match expressions are allowed only at the outermost level of function bodies - ResolveExpression(me.Source, twoState); + ResolveExpression(me.Source, twoState, specContext); assert me.Source.Type != null; // follows from postcondition of ResolveExpression UserDefinedType sourceType = null; DatatypeDecl dtd = null; @@ -1602,7 +1667,7 @@ namespace Microsoft.Dafny { } i++; } - ResolveExpression(mc.Body, twoState); + ResolveExpression(mc.Body, twoState, specContext); assert mc.Body.Type != null; // follows from postcondition of ResolveExpression if (!UnifyTypes(expr.Type, mc.Body.Type)) { Error(mc.Body.tok, "type of case bodies do not agree (found {0}, previous types {1})", mc.Body.Type, expr.Type); @@ -1623,7 +1688,7 @@ namespace Microsoft.Dafny { } } - void ResolveReceiver(Expression! expr, bool twoState) + void ResolveReceiver(Expression! expr, bool twoState, bool specContext) requires currentClass != null; ensures expr.Type != null; { @@ -1632,7 +1697,7 @@ namespace Microsoft.Dafny { // making sure 'this' does not really get used when it's not available. expr.Type = GetThisType(expr.tok, currentClass); } else { - ResolveExpression(expr, twoState); + ResolveExpression(expr, twoState, specContext); } } @@ -1729,8 +1794,78 @@ namespace Microsoft.Dafny { assert false; // unexpected operator } } + + /// + /// Returns whether or not 'expr' has any subexpression that uses some feature (like a ghost or quantifier) + /// that is allowed only in specification contexts. + /// Requires 'expr' to be a successfully resolved expression. + /// + bool UsesSpecFeatures(Expression! expr) + requires currentClass != null; + { + if (expr is LiteralExpr) { + return false; + } else if (expr is ThisExpr) { + return false; + } else if (expr is IdentifierExpr) { + IdentifierExpr e = (IdentifierExpr)expr; + return ((!)e.Var).IsGhost; + } else if (expr is DatatypeValue) { + DatatypeValue dtv = (DatatypeValue)expr; + return exists{Expression arg in dtv.Arguments; UsesSpecFeatures(arg)}; + } else if (expr is DisplayExpression) { + DisplayExpression e = (DisplayExpression)expr; + return exists{Expression ee in e.Elements; UsesSpecFeatures(ee)}; + } else if (expr is FieldSelectExpr) { + FieldSelectExpr e = (FieldSelectExpr)expr; + return ((!)e.Field).IsGhost || UsesSpecFeatures(e.Obj); + } else if (expr is SeqSelectExpr) { + SeqSelectExpr e = (SeqSelectExpr)expr; + return UsesSpecFeatures(e.Seq) || + (e.E0 != null && UsesSpecFeatures(e.E0)) || + (e.E1 != null && UsesSpecFeatures(e.E1)); + } else if (expr is SeqUpdateExpr) { + SeqUpdateExpr e = (SeqUpdateExpr)expr; + return UsesSpecFeatures(e.Seq) || + (e.Index != null && UsesSpecFeatures(e.Index)) || + (e.Value != null && UsesSpecFeatures(e.Value)); + } else if (expr is FunctionCallExpr) { + FunctionCallExpr e = (FunctionCallExpr)expr; + if (((!)e.Function).IsGhost) { + return true; + } + return exists{Expression arg in e.Args; UsesSpecFeatures(arg)}; + } else if (expr is OldExpr) { + OldExpr e = (OldExpr)expr; + return UsesSpecFeatures(e.E); + } else if (expr is FreshExpr) { + FreshExpr e = (FreshExpr)expr; + return UsesSpecFeatures(e.E); + } else if (expr is UnaryExpr) { + UnaryExpr e = (UnaryExpr)expr; + return UsesSpecFeatures(e.E); + } else if (expr is BinaryExpr) { + BinaryExpr e = (BinaryExpr)expr; + return UsesSpecFeatures(e.E0) || UsesSpecFeatures(e.E1); + } else if (expr is QuantifierExpr) { + return true; + } else if (expr is WildcardExpr) { + return false; + } else if (expr is ITEExpr) { + ITEExpr e = (ITEExpr)expr; + return UsesSpecFeatures(e.Test) || UsesSpecFeatures(e.Thn) || UsesSpecFeatures(e.Els); + } else if (expr is MatchExpr) { + MatchExpr me = (MatchExpr)expr; + if (UsesSpecFeatures(me.Source)) { + return true; + } + return exists{MatchCase mc in me.Cases; UsesSpecFeatures(mc.Body)}; + } else { + assert false; // unexpected expression + } + } } - + class Scope where Thing : class { [Rep] readonly List! names = new List(); // a null means a marker [Rep] readonly List! things = new List(); diff --git a/Source/Dafny/Translator.ssc b/Source/Dafny/Translator.ssc index 185a81ee..0615f644 100644 --- a/Source/Dafny/Translator.ssc +++ b/Source/Dafny/Translator.ssc @@ -1127,7 +1127,7 @@ namespace Microsoft.Dafny { Dictionary substMap = new Dictionary(); for (int i = 0; i < e.Function.Formals.Count; i++) { Formal p = e.Function.Formals[i]; - VarDecl local = new VarDecl(p.tok, p.Name, p.Type, null); + VarDecl local = new VarDecl(p.tok, p.Name, p.Type, p.IsGhost, null); local.type = local.OptionalType; // resolve local here IdentifierExpr ie = new IdentifierExpr(local.Tok, local.UniqueName); ie.Var = local; ie.Type = ie.Var.Type; // resolve ie here @@ -1207,7 +1207,7 @@ namespace Microsoft.Dafny { QuantifierExpr e = (QuantifierExpr)expr; Dictionary substMap = new Dictionary(); foreach (BoundVar bv in e.BoundVars) { - VarDecl local = new VarDecl(bv.tok, bv.Name, bv.Type, null); + VarDecl local = new VarDecl(bv.tok, bv.Name, bv.Type, bv.IsGhost, null); local.type = local.OptionalType; // resolve local here IdentifierExpr ie = new IdentifierExpr(local.Tok, local.UniqueName); ie.Var = local; ie.Type = ie.Var.Type; // resolve ie here @@ -1742,7 +1742,7 @@ namespace Microsoft.Dafny { Dictionary substMap = new Dictionary(); for (int i = 0; i < s.Method.Ins.Count; i++) { Formal p = s.Method.Ins[i]; - VarDecl local = new VarDecl(p.tok, p.Name, p.Type, null); + VarDecl local = new VarDecl(p.tok, p.Name, p.Type, p.IsGhost, null); local.type = local.OptionalType; // resolve local here IdentifierExpr ie = new IdentifierExpr(local.Tok, local.UniqueName); ie.Var = local; ie.Type = ie.Var.Type; // resolve ie here -- cgit v1.2.3