From f6a0c9295984d8e90db0ee6592e338fd051c8f05 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Sun, 22 May 2011 12:48:45 -0700 Subject: Dafny: refactored code into separate method ResolveIdentifierSequence and allow for a return of CallRhs --- Source/Dafny/DafnyAst.cs | 39 ++++++++++ Source/Dafny/Resolver.cs | 187 ++++++++++++++++++++++++++--------------------- 2 files changed, 144 insertions(+), 82 deletions(-) (limited to 'Source') diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index f6d96bab..79f20d5d 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -1365,6 +1365,45 @@ namespace Microsoft.Dafny { } } + public class CallRhs : AssignmentRhs + { + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(Receiver != null); + Contract.Invariant(MethodName != null); + Contract.Invariant(cce.NonNullElements(Args)); + } + + public readonly IToken Tok; + public readonly Expression/*!*/ Receiver; + public readonly string/*!*/ MethodName; + public readonly List/*!*/ Args; + public Method Method; // filled in by resolution + + public CallRhs(IToken tok, Expression/*!*/ receiver, string/*!*/ methodName, List/*!*/ args) + { + Contract.Requires(tok != null); + Contract.Requires(receiver != null); + Contract.Requires(methodName != null); + Contract.Requires(cce.NonNullElements(args)); + + this.Tok = tok; + this.Receiver = receiver; + this.MethodName = methodName; + this.Args = args; + } + public override bool CanAffectPreviouslyKnownExpressions { + get { + foreach (var mod in Method.Mod) { + if (!(mod.E is ThisExpr)) { + return true; + } + } + return false; + } + } + } + public class HavocRhs : AssignmentRhs { public override bool CanAffectPreviouslyKnownExpressions { get { return false; } } } diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index d0b5ab60..6165c9a5 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1850,83 +1850,7 @@ namespace Microsoft.Dafny { } else if (expr is IdentifierSequence) { var e = (IdentifierSequence)expr; - // Look up "id" as follows: - // - local variable, parameter, or bound variable (if this clashes with something of interest, one can always rename the local variable locally) - // - type name (class or datatype) - // - unambiguous constructor name of a datatype (if two constructors have the same name, an error message is produced here) - // - field name (with implicit receiver) (if the field is ocluded by anything above, one can use an explicit "this.") - // Note, at present, modules do not give rise to new namespaces, which is something that should - // be changed in the language when modules are given more attention. - Expression r = null; // resolved version of e - - TopLevelDecl decl; - Tuple pair; - Dictionary members; - MemberDecl member; - var id = e.Tokens[0]; - if (scope.Find(id.val) != null) { - // ----- root is a local variable, parameter, or bound variable - r = new IdentifierExpr(id, id.val); - ResolveExpression(r, twoState, specContext); - r = ResolveSuffix(r, e, 1, twoState, specContext); - - } else if (classes.TryGetValue(id.val, out decl)) { - if (e.Tokens.Count == 1 && e.Arguments == null) { - Error(id, "name of type ('{0}') is used as a variable", id.val); - } else if (e.Tokens.Count == 1 && e.Arguments != null) { - Error(id, "name of type ('{0}') is used as a function", id.val); - // resolve the arguments nonetheless - foreach (var arg in e.Arguments) { - ResolveExpression(arg, twoState, specContext); - } - } else if (decl is ClassDecl) { - // ----- root is a class - var cd = (ClassDecl)decl; - r = ResolveSuffix(new StaticReceiverExpr(id, cd), e, 1, twoState, specContext); - - } else { - // ----- root is a datatype - var dt = (DatatypeDecl)decl; // otherwise, unexpected TopLevelDecl - var args = (e.Tokens.Count == 2 ? e.Arguments : null) ?? new List(); - r = new DatatypeValue(id, id.val, e.Tokens[1].val, args); - ResolveExpression(r, twoState, specContext); - if (e.Tokens.Count != 2) { - r = ResolveSuffix(r, e, 2, twoState, specContext); - } - } - - } else if (allDatatypeCtors.TryGetValue(id.val, out pair)) { - // ----- root is a datatype constructor - if (pair.Item2) { - // there is more than one constructor with this name - Error(id, "the name '{0}' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, '{1}.{0}')", id.val, pair.Item1.EnclosingDatatype.Name); - } else { - var args = (e.Tokens.Count == 1 ? e.Arguments : null) ?? new List(); - r = new DatatypeValue(id, pair.Item1.EnclosingDatatype.Name, id.val, args); - ResolveExpression(r, twoState, specContext); - if (e.Tokens.Count != 1) { - r = ResolveSuffix(r, e, 1, twoState, specContext); - } - } - - } else if (classMembers.TryGetValue(currentClass, out members) && members.TryGetValue(id.val, out member)) { - // ----- field, function, or method - r = ResolveSuffix(new ImplicitThisExpr(id), e, 0, twoState, specContext); - - } else { - Error(id, "unresolved identifier: {0}", id.val); - // resolve arguments, if any - if (e.Arguments != null) { - foreach (var arg in e.Arguments) { - ResolveExpression(arg, twoState, specContext); - } - } - } - - if (r != null) { - e.ResolvedExpression = r; - e.Type = r.Type; - } + ResolveIdentifierSequence(e, twoState, specContext, false); } else if (expr is LiteralExpr) { LiteralExpr e = (LiteralExpr)expr; @@ -2554,17 +2478,107 @@ namespace Microsoft.Dafny { } } + /// + /// If "!allowMethodCall", or if "e" does not designate a method call, resolves "e" and returns "null". + /// Otherwise, resolves all sub-parts of "e" and returns a (resolved) CallRhs expression representing the call. + /// + CallRhs ResolveIdentifierSequence(IdentifierSequence e, bool twoState, bool specContext, bool allowMethodCall) { + // Look up "id" as follows: + // - local variable, parameter, or bound variable (if this clashes with something of interest, one can always rename the local variable locally) + // - type name (class or datatype) + // - unambiguous constructor name of a datatype (if two constructors have the same name, an error message is produced here) + // - field name (with implicit receiver) (if the field is ocluded by anything above, one can use an explicit "this.") + // Note, at present, modules do not give rise to new namespaces, which is something that should + // be changed in the language when modules are given more attention. + Expression r = null; // resolved version of e + CallRhs call = null; + + TopLevelDecl decl; + Tuple pair; + Dictionary members; + MemberDecl member; + var id = e.Tokens[0]; + if (scope.Find(id.val) != null) { + // ----- root is a local variable, parameter, or bound variable + r = new IdentifierExpr(id, id.val); + ResolveExpression(r, twoState, specContext); + r = ResolveSuffix(r, e, 1, twoState, specContext, allowMethodCall, out call); + + } else if (classes.TryGetValue(id.val, out decl)) { + if (e.Tokens.Count == 1 && e.Arguments == null) { + Error(id, "name of type ('{0}') is used as a variable", id.val); + } else if (e.Tokens.Count == 1 && e.Arguments != null) { + Error(id, "name of type ('{0}') is used as a function", id.val); + // resolve the arguments nonetheless + foreach (var arg in e.Arguments) { + ResolveExpression(arg, twoState, specContext); + } + } else if (decl is ClassDecl) { + // ----- root is a class + var cd = (ClassDecl)decl; + r = ResolveSuffix(new StaticReceiverExpr(id, cd), e, 1, twoState, specContext, allowMethodCall, out call); + + } else { + // ----- root is a datatype + var dt = (DatatypeDecl)decl; // otherwise, unexpected TopLevelDecl + var args = (e.Tokens.Count == 2 ? e.Arguments : null) ?? new List(); + r = new DatatypeValue(id, id.val, e.Tokens[1].val, args); + ResolveExpression(r, twoState, specContext); + if (e.Tokens.Count != 2) { + r = ResolveSuffix(r, e, 2, twoState, specContext, allowMethodCall, out call); + } + } + + } else if (allDatatypeCtors.TryGetValue(id.val, out pair)) { + // ----- root is a datatype constructor + if (pair.Item2) { + // there is more than one constructor with this name + Error(id, "the name '{0}' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, '{1}.{0}')", id.val, pair.Item1.EnclosingDatatype.Name); + } else { + var args = (e.Tokens.Count == 1 ? e.Arguments : null) ?? new List(); + r = new DatatypeValue(id, pair.Item1.EnclosingDatatype.Name, id.val, args); + ResolveExpression(r, twoState, specContext); + if (e.Tokens.Count != 1) { + r = ResolveSuffix(r, e, 1, twoState, specContext, allowMethodCall, out call); + } + } + + } else if (classMembers.TryGetValue(currentClass, out members) && members.TryGetValue(id.val, out member)) { + // ----- field, function, or method + r = ResolveSuffix(new ImplicitThisExpr(id), e, 0, twoState, specContext, allowMethodCall, out call); + + } else { + Error(id, "unresolved identifier: {0}", id.val); + // resolve arguments, if any + if (e.Arguments != null) { + foreach (var arg in e.Arguments) { + ResolveExpression(arg, twoState, specContext); + } + } + } + + if (r != null) { + e.ResolvedExpression = r; + e.Type = r.Type; + } + return call; + } + /// /// Given resolved expression "r" and unresolved expressions e.Tokens[p..] and e.Arguments. /// Returns a resolved version of the expression: /// r . e.Tokens[p] . e.Tokens[p+1] ... . e.Tokens[e.Tokens.Count-1] ( e.Arguments ) + /// Except, if "allowMethodCall" is "true" and the would-be-returned value designates a method + /// call, instead returns null and returns "call" as a non-null value. /// - Expression ResolveSuffix(Expression r, IdentifierSequence e, int p, bool twoState, bool specContext) { + Expression ResolveSuffix(Expression r, IdentifierSequence e, int p, bool twoState, bool specContext, bool allowMethodCall, out CallRhs call) { Contract.Requires(r != null); Contract.Requires(e != null); Contract.Requires(0 <= p && p <= e.Tokens.Count); - Contract.Ensures(Contract.Result() != null); + Contract.Ensures((Contract.Result() != null && Contract.ValueAtReturn(out call) == null) || + (allowMethodCall && Contract.Result() == null && Contract.ValueAtReturn(out call) != null)); + call = null; int nonCallArguments = e.Arguments == null ? e.Tokens.Count : e.Tokens.Count - 1; for (; p < nonCallArguments; p++) { r = new FieldSelectExpr(e.Tokens[p], r, e.Tokens[p].val); @@ -2573,9 +2587,18 @@ namespace Microsoft.Dafny { if (p < e.Tokens.Count) { Contract.Assert(e.Arguments != null); - // TODO: treat differently if what is being called is a method - r = new FunctionCallExpr(e.Tokens[p], e.Tokens[p].val, r, e.Arguments); - ResolveExpression(r, twoState, specContext); + + Dictionary members; + MemberDecl member; + if (classMembers.TryGetValue(currentClass, out members) && members.TryGetValue(e.Tokens[p].val, out member) && member is Method) { + // method + call = new CallRhs(e.Tokens[p], r, e.Tokens[p].val, e.Arguments); + // TODO: resolve call, and sometimes return an error message if a call is not allowed here + r = null; + } else { + r = new FunctionCallExpr(e.Tokens[p], e.Tokens[p].val, r, e.Arguments); + ResolveExpression(r, twoState, specContext); + } } else if (e.Arguments != null) { Contract.Assert(p == e.Tokens.Count); Error(e.OpenParen, "non-function expression is called with parameters"); -- cgit v1.2.3