summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
Diffstat (limited to 'Source')
-rw-r--r--Source/Dafny/Dafny.atg53
-rw-r--r--Source/Dafny/DafnyAst.ssc40
-rw-r--r--Source/Dafny/Parser.ssc60
-rw-r--r--Source/Dafny/Printer.ssc8
-rw-r--r--Source/Dafny/Resolver.ssc347
-rw-r--r--Source/Dafny/Translator.ssc6
6 files changed, 355 insertions, 159 deletions
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<IdentifierExpr!>! lhs,
- List<VarDecl!>! newVars) {
+ List<AutoVarDecl!>! 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<MemberModifiers mmod, List<MemberDecl!\>! mm>
";"
.
+GIdentType<bool allowGhost, out Token! id, out Type! ty, out bool isGhost>
+/* 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<out id, out ty>
+ .
+
IdentType<out Token! id, out Type! ty>
= Ident<out id>
":"
@@ -276,9 +285,9 @@ MethodDecl<MemberModifiers mmod, out Method! m>
Ident<out id>
[ GenericParameters<typeArgs> ]
(. parseVarScope.PushMarker(); .)
- Formals<true, ins>
+ Formals<true, true, ins>
[ "returns"
- Formals<false, outs>
+ Formals<false, true, outs>
]
( ";" { MethodSpec<req, mod, ens, dec> }
@@ -307,12 +316,12 @@ MethodSpec<List<MaybeFreeExpression!\>! req, List<Expression!\>! mod, List<Maybe
)
.
-Formals<bool incoming, List<Formal!\>! formals>
-= (. Token! id; Type! ty; .)
+Formals<bool incoming, bool allowGhosts, List<Formal!\>! formals>
+= (. Token! id; Type! ty; bool isGhost; .)
"("
[
- IdentType<out id, out ty> (. formals.Add(new Formal(id, id.val, ty, incoming)); parseVarScope.Push(id.val, id.val); .)
- { "," 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); .)
+ { "," GIdentType<allowGhosts, out id, out ty, out isGhost> (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); parseVarScope.Push(id.val, id.val); .)
}
]
")"
@@ -322,8 +331,8 @@ FormalsOptionalIds<List<Formal!\>! formals>
= (. Token! id; Type! ty; string! name; .)
"("
[
- TypeIdentOptional<out id, out name, out ty> (. formals.Add(new Formal(id, name, ty, true)); parseVarScope.Push(name, name); .)
- { "," TypeIdentOptional<out id, out name, out ty> (. formals.Add(new Formal(id, name, ty, true)); parseVarScope.Push(name, name); .)
+ TypeIdentOptional<out id, out name, out ty> (. formals.Add(new Formal(id, name, ty, true, false)); parseVarScope.Push(name, name); .)
+ { "," TypeIdentOptional<out id, out name, out ty> (. formals.Add(new Formal(id, name, ty, true, false)); parseVarScope.Push(name, name); .)
}
]
")"
@@ -390,15 +399,18 @@ FunctionDecl<MemberModifiers mmod, out Function! f>
List<Expression!> reads = new List<Expression!>();
List<Expression!> decreases = new List<Expression!>();
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<ref attrs> }
Ident<out id>
[ GenericParameters<typeArgs> ]
(. parseVarScope.PushMarker(); .)
- Formals<true, formals>
+ Formals<true, false, formals>
":"
Type<out returnType>
( ";"
@@ -407,7 +419,7 @@ FunctionDecl<MemberModifiers mmod, out Function! f>
FunctionBody<out bb> (. 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<out Expression! e>
.
VarDeclStmts<List<Statement!\>! ss>
-= (. VarDecl! d; .)
- [ "ghost" ]
+= (. VarDecl! d; bool isGhost = false; .)
+ [ "ghost" (. isGhost = true; .)
+ ]
"var"
- IdentTypeRhs<out d> (. ss.Add(d); parseVarScope.Push(d.Name, d.Name); .)
- { "," IdentTypeRhs<out d> (. ss.Add(d); parseVarScope.Push(d.Name, d.Name); .)
+ IdentTypeRhs<out d, isGhost> (. ss.Add(d); parseVarScope.Push(d.Name, d.Name); .)
+ { "," IdentTypeRhs<out d, isGhost> (. ss.Add(d); parseVarScope.Push(d.Name, d.Name); .)
}
";"
.
-IdentTypeRhs<out VarDecl! d>
+IdentTypeRhs<out VarDecl! d, bool isGhost>
= (. Token! id; Type! ty; Expression! e;
Expression rhs = null; Type newType = null;
Type optionalType = null; DeterminedAssignmentRhs optionalRhs = null;
@@ -608,7 +621,7 @@ IdentTypeRhs<out VarDecl! d>
} 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<out Statement! s>
= (. Token! x, id;
Expression! e;
List<IdentifierExpr!> lhs = new List<IdentifierExpr!>();
- List<VarDecl!> newVars = new List<VarDecl!>();
+ List<AutoVarDecl!> newVars = new List<AutoVarDecl!>();
.)
"call" (. x = token; .)
CallStmtSubExpr<out e>
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<TypeParameter!>! TypeArgs;
public readonly List<Formal!>! Formals;
@@ -479,9 +484,10 @@ namespace Microsoft.Dafny
public readonly List<Expression!>! Decreases;
public readonly Expression Body; // an extended expression
- public Function(Token! tok, string! name, bool isClass, bool isUse, [Captured] List<TypeParameter!>! typeArgs, [Captured] List<Formal!>! formals, Type! resultType,
+ public Function(Token! tok, string! name, bool isClass, bool isGhost, bool isUse, [Captured] List<TypeParameter!>! typeArgs, [Captured] List<Formal!>! formals, Type! resultType,
List<Expression!>! req, List<Expression!>! reads, List<Expression!>! 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);
+ }
+ /// <summary>
+ /// This method retrospectively makes the VarDecl a ghost. It is to be used only during resolution.
+ /// </summary>
+ public void MakeGhost() {
+ isGhost = true;
+ }
+ }
+
public class CallStmt : Statement {
- public readonly List<VarDecl!>! NewVars;
+ public readonly List<AutoVarDecl!>! NewVars;
public readonly List<IdentifierExpr!>! Lhs;
public readonly Expression! Receiver;
public readonly string! MethodName;
public readonly List<Expression!>! Args;
public Method Method; // filled in by resolution
- public CallStmt(Token! tok, List<VarDecl!>! newVars, List<IdentifierExpr!>! lhs, Expression! receiver, string! methodName, List<Expression!>! args) {
+ public CallStmt(Token! tok, List<AutoVarDecl!>! newVars, List<IdentifierExpr!>! lhs, Expression! receiver, string! methodName, List<Expression!>! 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<IdentifierExpr!>! lhs,
- List<VarDecl!>! newVars) {
+ List<AutoVarDecl!>! 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<TopLevelDecl!>! classes) {
List<Expression!> reads = new List<Expression!>();
List<Expression!> decreases = new List<Expression!>();
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<TopLevelDecl!>! 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<TopLevelDecl!>! 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<TopLevelDecl!>! 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<TopLevelDecl!>! 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<TopLevelDecl!>! 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<TopLevelDecl!>! classes) {
} else Error(97);
}
- static void Formals(bool incoming, List<Formal!>! formals) {
- Token! id; Type! ty;
+ static void Formals(bool incoming, bool allowGhosts, List<Formal!>! 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<Expression!>! decreases) {
}
static void VarDeclStmts(List<Statement!>! 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<Expression!>! decreases) {
Token! x, id;
Expression! e;
List<IdentifierExpr!> lhs = new List<IdentifierExpr!>();
- List<VarDecl!> newVars = new List<VarDecl!>();
+ List<AutoVarDecl!> newVars = new List<AutoVarDecl!>();
Expect(46);
x = token;
@@ -1064,7 +1080,7 @@ List<Expression!>! 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<Expression!>! 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<string!,object> lhsNameSet = new Dictionary<string!,object>();
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<TypeParameter!,Type!> subst = new Dictionary<TypeParameter!,Type!>();
- 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<TypeParameter!,Type!> subst = new Dictionary<TypeParameter!,Type!>();
+ 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 {
/// <summary>
/// "twoState" implies that "old" and "fresh" expressions are allowed
/// </summary>
- 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
}
}
+
+ /// <summary>
+ /// 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.
+ /// </summary>
+ 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<Thing> where Thing : class {
[Rep] readonly List<string>! names = new List<string>(); // a null means a marker
[Rep] readonly List<Thing?>! things = new List<Thing?>();
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<IVariable,Expression!> substMap = new Dictionary<IVariable,Expression!>();
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<IVariable,Expression!> substMap = new Dictionary<IVariable,Expression!>();
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<IVariable,Expression!> substMap = new Dictionary<IVariable,Expression!>();
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-23 01:08:12 +0000