diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Dafny/Resolver.cs | 273 |
1 files changed, 145 insertions, 128 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 0baff42f..780e04d9 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1232,141 +1232,15 @@ namespace Microsoft.Dafny { i++;
}
s.hiddenUpdate = new UpdateStmt(s.Tok, formals, s.rhss, true);
- ResolveStatement(s.hiddenUpdate, specContextOnly, method);
// resolving the update statement will check for return statement specifics.
+ ResolveStatement(s.hiddenUpdate, specContextOnly, method);
}
}
else {// this is a regular return statement.
s.hiddenUpdate = null;
}
} else if (stmt is UpdateStmt) {
- var s = (UpdateStmt)stmt;
- int prevErrorCount = ErrorCount;
- // First, resolve all LHS's and expression-looking RHS's.
- SeqSelectExpr arrayRangeLhs = null;
- foreach (var lhs in s.Lhss) {
- if (lhs is SeqSelectExpr) {
- var sse = (SeqSelectExpr)lhs;
- ResolveSeqSelectExpr(sse, true, true);
- if (arrayRangeLhs == null && !sse.SelectOne) {
- arrayRangeLhs = sse;
- }
- } else {
- ResolveExpression(lhs, true);
- }
- }
- IToken firstEffectfulRhs = null;
- CallRhs callRhs = null;
- // Resolve RHSs
- foreach (var rhs in s.Rhss) {
- bool isEffectful;
- if (rhs is TypeRhs) {
- var tr = (TypeRhs)rhs;
- ResolveTypeRhs(tr, stmt, specContextOnly, method);
- isEffectful = tr.InitCall != null;
- } else if (rhs is HavocRhs) {
- isEffectful = false;
- } else {
- var er = (ExprRhs)rhs;
- if (er.Expr is IdentifierSequence) {
- var cRhs = ResolveIdentifierSequence((IdentifierSequence)er.Expr, true, true);
- isEffectful = cRhs != null;
- callRhs = callRhs ?? cRhs;
- } else if (er.Expr is FunctionCallExpr) {
- var cRhs = ResolveFunctionCallExpr((FunctionCallExpr)er.Expr, true, true);
- isEffectful = cRhs != null;
- callRhs = callRhs ?? cRhs;
- } else {
- ResolveExpression(er.Expr, true);
- isEffectful = false;
- }
- }
- if (isEffectful && firstEffectfulRhs == null) {
- firstEffectfulRhs = rhs.Tok;
- }
- }
- // check for duplicate identifiers on the left (full duplication checking for references and the like is done during verification)
- var lhsNameSet = new Dictionary<string, object>();
- foreach (var lhs in s.Lhss) {
- var ie = lhs.Resolved as IdentifierExpr;
- if (ie != null) {
- if (lhsNameSet.ContainsKey(ie.Name)) {
- Error(s, "Duplicate variable in left-hand side of {1} statement: {0}", ie.Name, callRhs != null ? "call" : "assignment");
- } else {
- lhsNameSet.Add(ie.Name, null);
- }
- }
- }
-
- // figure out what kind of UpdateStmt this is
- if (firstEffectfulRhs == null) {
- if (s.Lhss.Count == 0) {
- Contract.Assert(s.Rhss.Count == 1); // guaranteed by the parser
- Error(s, "expected method call, found expression");
- } else if (s.Lhss.Count != s.Rhss.Count) {
- Error(s, "the number of left-hand sides ({0}) and right-hand sides ({1}) must match for a multi-assignment", s.Lhss.Count, s.Rhss.Count);
- } else if (arrayRangeLhs != null && s.Lhss.Count != 1) {
- Error(arrayRangeLhs, "array-range may not be used as LHS of multi-assignment; use separate assignment statements for each array-range assignment");
- } else if (ErrorCount == prevErrorCount) {
- // add the statements here in a sequence, but don't use that sequence later for translation (instead, should translated properly as multi-assignment)
- for (int i = 0; i < s.Lhss.Count; i++) {
- var a = new AssignStmt(s.Tok, s.Lhss[i].Resolved, s.Rhss[i]);
- s.ResolvedStatements.Add(a);
- }
- }
- } else {
- if (s.CanMutateKnownState) {
- if (1 < s.Rhss.Count)
- Error(firstEffectfulRhs, "cannot have effectful parameter in multi-return statement.");
- else { // it might be ok, if it is a TypeExpr
- Contract.Assert(s.Rhss.Count == 1);
- if (callRhs != null) {
- Error(callRhs.Tok, "cannot have method call in return statement.");
- }
- else {
- // we have a TypeExpr
- Contract.Assert(s.Rhss[0] is TypeRhs);
- var tr = (TypeRhs)s.Rhss[0];
- Contract.Assert(tr.InitCall != null); // there were effects, so this must have been a call.
- if (tr.CanAffectPreviouslyKnownExpressions) {
- Error(tr.Tok, "can only have initialization methods which modify at most 'this'.");
- }
- }
- }
- }
- else {
- // if there was an effectful RHS, that must be the only RHS
- if (s.Rhss.Count != 1) {
- Error(firstEffectfulRhs, "an update statement is allowed an effectful RHS only if there is just one RHS");
- } else if (arrayRangeLhs != null) {
- Error(arrayRangeLhs, "Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable");
- } else if (callRhs == null) {
- // must be a single TypeRhs
- if (s.Lhss.Count != 1) {
- Contract.Assert(2 <= s.Lhss.Count); // the parser allows 0 Lhss only if the whole statement looks like an expression (not a TypeRhs)
- Error(s.Lhss[1].tok, "the number of left-hand sides ({0}) and right-hand sides ({1}) must match for a multi-assignment", s.Lhss.Count, s.Rhss.Count);
- } else if (ErrorCount == prevErrorCount) {
- var a = new AssignStmt(s.Tok, s.Lhss[0].Resolved, s.Rhss[0]);
- s.ResolvedStatements.Add(a);
- }
- } else {
- // a call statement
- if (ErrorCount == prevErrorCount) {
- var resolvedLhss = new List<Expression>();
- foreach (var ll in s.Lhss) {
- resolvedLhss.Add(ll.Resolved);
- }
- var a = new CallStmt(callRhs.Tok, resolvedLhss, callRhs.Receiver, callRhs.MethodName, callRhs.Args);
- s.ResolvedStatements.Add(a);
- }
- }
- }
- }
-
- foreach (var a in s.ResolvedStatements) {
- ResolveStatement(a, specContextOnly, method);
- }
- // end of UpdateStmt
+ ResolveUpdateStmt((UpdateStmt)stmt, specContextOnly, method);
} else if (stmt is VarDeclStmt) {
var s = (VarDeclStmt)stmt;
foreach (var vd in s.Lhss) {
@@ -1748,6 +1622,149 @@ namespace Microsoft.Dafny { }
}
+ private void ResolveUpdateStmt(UpdateStmt s, bool specContextOnly, Method method)
+ {
+ int prevErrorCount = ErrorCount;
+ // First, resolve all LHS's and expression-looking RHS's.
+ SeqSelectExpr arrayRangeLhs = null;
+ foreach (var lhs in s.Lhss) {
+ if (lhs is SeqSelectExpr) {
+ var sse = (SeqSelectExpr)lhs;
+ ResolveSeqSelectExpr(sse, true, true);
+ if (arrayRangeLhs == null && !sse.SelectOne) {
+ arrayRangeLhs = sse;
+ }
+ }
+ else {
+ ResolveExpression(lhs, true);
+ }
+ }
+ IToken firstEffectfulRhs = null;
+ CallRhs callRhs = null;
+ // Resolve RHSs
+ foreach (var rhs in s.Rhss) {
+ bool isEffectful;
+ if (rhs is TypeRhs) {
+ var tr = (TypeRhs)rhs;
+ ResolveTypeRhs(tr, s, specContextOnly, method);
+ isEffectful = tr.InitCall != null;
+ }
+ else if (rhs is HavocRhs) {
+ isEffectful = false;
+ }
+ else {
+ var er = (ExprRhs)rhs;
+ if (er.Expr is IdentifierSequence) {
+ var cRhs = ResolveIdentifierSequence((IdentifierSequence)er.Expr, true, true);
+ isEffectful = cRhs != null;
+ callRhs = callRhs ?? cRhs;
+ }
+ else if (er.Expr is FunctionCallExpr) {
+ var cRhs = ResolveFunctionCallExpr((FunctionCallExpr)er.Expr, true, true);
+ isEffectful = cRhs != null;
+ callRhs = callRhs ?? cRhs;
+ }
+ else {
+ ResolveExpression(er.Expr, true);
+ isEffectful = false;
+ }
+ }
+ if (isEffectful && firstEffectfulRhs == null) {
+ firstEffectfulRhs = rhs.Tok;
+ }
+ }
+ // check for duplicate identifiers on the left (full duplication checking for references and the like is done during verification)
+ var lhsNameSet = new Dictionary<string, object>();
+ foreach (var lhs in s.Lhss) {
+ var ie = lhs.Resolved as IdentifierExpr;
+ if (ie != null) {
+ if (lhsNameSet.ContainsKey(ie.Name)) {
+ Error(s, "Duplicate variable in left-hand side of {1} statement: {0}", ie.Name, callRhs != null ? "call" : "assignment");
+ }
+ else {
+ lhsNameSet.Add(ie.Name, null);
+ }
+ }
+ }
+
+ // figure out what kind of UpdateStmt this is
+ if (firstEffectfulRhs == null) {
+ if (s.Lhss.Count == 0) {
+ Contract.Assert(s.Rhss.Count == 1); // guaranteed by the parser
+ Error(s, "expected method call, found expression");
+ }
+ else if (s.Lhss.Count != s.Rhss.Count) {
+ Error(s, "the number of left-hand sides ({0}) and right-hand sides ({1}) must match for a multi-assignment", s.Lhss.Count, s.Rhss.Count);
+ }
+ else if (arrayRangeLhs != null && s.Lhss.Count != 1) {
+ Error(arrayRangeLhs, "array-range may not be used as LHS of multi-assignment; use separate assignment statements for each array-range assignment");
+ }
+ else if (ErrorCount == prevErrorCount) {
+ // add the statements here in a sequence, but don't use that sequence later for translation (instead, should translated properly as multi-assignment)
+ for (int i = 0; i < s.Lhss.Count; i++) {
+ var a = new AssignStmt(s.Tok, s.Lhss[i].Resolved, s.Rhss[i]);
+ s.ResolvedStatements.Add(a);
+ }
+ }
+ }
+ else {
+ if (s.CanMutateKnownState) {
+ if (1 < s.Rhss.Count)
+ Error(firstEffectfulRhs, "cannot have effectful parameter in multi-return statement.");
+ else { // it might be ok, if it is a TypeExpr
+ Contract.Assert(s.Rhss.Count == 1);
+ if (callRhs != null) {
+ Error(callRhs.Tok, "cannot have method call in return statement.");
+ }
+ else {
+ // we have a TypeExpr
+ Contract.Assert(s.Rhss[0] is TypeRhs);
+ var tr = (TypeRhs)s.Rhss[0];
+ Contract.Assert(tr.InitCall != null); // there were effects, so this must have been a call.
+ if (tr.CanAffectPreviouslyKnownExpressions) {
+ Error(tr.Tok, "can only have initialization methods which modify at most 'this'.");
+ }
+ }
+ }
+ }
+ else {
+ // if there was an effectful RHS, that must be the only RHS
+ if (s.Rhss.Count != 1) {
+ Error(firstEffectfulRhs, "an update statement is allowed an effectful RHS only if there is just one RHS");
+ }
+ else if (arrayRangeLhs != null) {
+ Error(arrayRangeLhs, "Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable");
+ }
+ else if (callRhs == null) {
+ // must be a single TypeRhs
+ if (s.Lhss.Count != 1) {
+ Contract.Assert(2 <= s.Lhss.Count); // the parser allows 0 Lhss only if the whole statement looks like an expression (not a TypeRhs)
+ Error(s.Lhss[1].tok, "the number of left-hand sides ({0}) and right-hand sides ({1}) must match for a multi-assignment", s.Lhss.Count, s.Rhss.Count);
+ }
+ else if (ErrorCount == prevErrorCount) {
+ var a = new AssignStmt(s.Tok, s.Lhss[0].Resolved, s.Rhss[0]);
+ s.ResolvedStatements.Add(a);
+ }
+ }
+ else {
+ // a call statement
+ if (ErrorCount == prevErrorCount) {
+ var resolvedLhss = new List<Expression>();
+ foreach (var ll in s.Lhss) {
+ resolvedLhss.Add(ll.Resolved);
+ }
+ var a = new CallStmt(callRhs.Tok, resolvedLhss, callRhs.Receiver, callRhs.MethodName, callRhs.Args);
+ s.ResolvedStatements.Add(a);
+ }
+ }
+ }
+ }
+
+ foreach (var a in s.ResolvedStatements) {
+ ResolveStatement(a, specContextOnly, method);
+ }
+ }
+
bool ResolveAlternatives(List<GuardedAlternative> alternatives, bool specContextOnly, AlternativeLoopStmt loopToCatchBreaks, Method method) {
Contract.Requires(alternatives != null);
Contract.Requires(method != null);
|