diff options
Diffstat (limited to 'Source/Dafny/Resolver.cs')
| -rw-r--r-- | Source/Dafny/Resolver.cs | 232 |
1 files changed, 121 insertions, 111 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 945bf5c2..573cdfa7 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -3754,135 +3754,119 @@ namespace Microsoft.Dafny Error(lhs, "cannot assign to non-ghost variable in a ghost context");
}
}
- IToken firstEffectfulRhs = null;
- CallRhs callRhs = null;
// Resolve RHSs
if (update == null) {
var suchThat = (AssignSuchThatStmt)s; // this is the other possible subclass
- ResolveExpression(suchThat.Expr, true);
- if (suchThat.AssumeToken == null) {
- // to ease in the verification, only allow local variables as LHSs
- var lhsNames = new Dictionary<string, object>();
- foreach (var lhs in s.Lhss) {
- if (!(lhs.Resolved is IdentifierExpr)) {
- Error(lhs, "the assign-such-that statement currently only supports local-variable LHSs");
- } else {
- var ie = (IdentifierExpr)lhs.Resolved;
- if (lhsNames.ContainsKey(ie.Name)) {
- // disallow same LHS.
- Error(s, "duplicate variable in left-hand side of assign-such-that statement: {0}", ie.Name);
- } else {
- lhsNames.Add(ie.Name, null);
- }
- }
- }
- }
- } else {
- foreach (var rhs in update.Rhss) {
- bool isEffectful;
- if (rhs is TypeRhs) {
- var tr = (TypeRhs)rhs;
- ResolveTypeRhs(tr, s, specContextOnly, codeContext);
- isEffectful = tr.InitCall != null;
- } else if (rhs is HavocRhs) {
- isEffectful = false;
+ ResolveAssignSuchThatStmt(suchThat, specContextOnly);
+ return;
+ }
+
+ IToken firstEffectfulRhs = null;
+ CallRhs callRhs = null;
+ foreach (var rhs in update.Rhss) {
+ bool isEffectful;
+ if (rhs is TypeRhs) {
+ var tr = (TypeRhs)rhs;
+ ResolveTypeRhs(tr, s, specContextOnly, codeContext);
+ 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 {
- 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;
+ 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)) {
- if (callRhs != null)
- // only allow same LHS in a multiassignment, not a call statement
+ // syntactically disallow duplicate LHSs for call statements
+ if (callRhs != null) {
+ // 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 call statement: {0}", ie.Name);
- } else {
- lhsNameSet.Add(ie.Name, null);
+ } else {
+ lhsNameSet.Add(ie.Name, null);
+ }
}
}
}
- if (update != null) {
- // figure out what kind of UpdateStmt this is
- if (firstEffectfulRhs == null) {
- if (s.Lhss.Count == 0) {
- Contract.Assert(update.Rhss.Count == 1); // guaranteed by the parser
- Error(s, "expected method call, found expression");
- } else if (s.Lhss.Count != update.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, update.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, update.Rhss[i]);
- s.ResolvedStatements.Add(a);
- }
+
+ // figure out what kind of UpdateStmt this is
+ if (firstEffectfulRhs == null) {
+ if (s.Lhss.Count == 0) {
+ Contract.Assert(update.Rhss.Count == 1); // guaranteed by the parser
+ Error(s, "expected method call, found expression");
+ } else if (s.Lhss.Count != update.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, update.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, update.Rhss[i]);
+ s.ResolvedStatements.Add(a);
}
+ }
- } else if (update.CanMutateKnownState) {
- if (1 < update.Rhss.Count) {
- Error(firstEffectfulRhs, "cannot have effectful parameter in multi-return statement.");
- } else { // it might be ok, if it is a TypeRhs
- Contract.Assert(update.Rhss.Count == 1);
- if (callRhs != null) {
- Error(callRhs.Tok, "cannot have method call in return statement.");
- } else {
- // we have a TypeRhs
- Contract.Assert(update.Rhss[0] is TypeRhs);
- var tr = (TypeRhs)update.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'.");
- }
- var a = new AssignStmt(s.Tok, s.Lhss[0].Resolved, tr);
- s.ResolvedStatements.Add(a);
+ } else if (update.CanMutateKnownState) {
+ if (1 < update.Rhss.Count) {
+ Error(firstEffectfulRhs, "cannot have effectful parameter in multi-return statement.");
+ } else { // it might be ok, if it is a TypeRhs
+ Contract.Assert(update.Rhss.Count == 1);
+ if (callRhs != null) {
+ Error(callRhs.Tok, "cannot have method call in return statement.");
+ } else {
+ // we have a TypeRhs
+ Contract.Assert(update.Rhss[0] is TypeRhs);
+ var tr = (TypeRhs)update.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'.");
}
+ var a = new AssignStmt(s.Tok, s.Lhss[0].Resolved, tr);
+ s.ResolvedStatements.Add(a);
}
+ }
+ } else {
+ // if there was an effectful RHS, that must be the only RHS
+ if (update.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, update.Rhss.Count);
+ } else if (ErrorCount == prevErrorCount) {
+ var a = new AssignStmt(s.Tok, s.Lhss[0].Resolved, update.Rhss[0]);
+ s.ResolvedStatements.Add(a);
+ }
} else {
- // if there was an effectful RHS, that must be the only RHS
- if (update.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, update.Rhss.Count);
- } else if (ErrorCount == prevErrorCount) {
- var a = new AssignStmt(s.Tok, s.Lhss[0].Resolved, update.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);
+ // 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);
}
}
}
@@ -3893,6 +3877,26 @@ namespace Microsoft.Dafny s.IsGhost = s.ResolvedStatements.TrueForAll(ss => ss.IsGhost);
}
+ private void ResolveAssignSuchThatStmt(AssignSuchThatStmt s, bool specContextOnly) {
+ Contract.Requires(s != null);
+
+ if (s.AssumeToken == null) {
+ // to ease in the verification of the existence check, only allow local variables as LHSs
+ foreach (var lhs in s.Lhss) {
+ if (!(lhs.Resolved is IdentifierExpr)) {
+ Error(lhs, "the assign-such-that statement currently only supports local-variable LHSs");
+ }
+ }
+ }
+
+ s.IsGhost = s.Lhss.TrueForAll(AssignStmt.LhsIsToGhost);
+ var ec = ErrorCount;
+ ResolveExpression(s.Expr, true);
+ if (ec == ErrorCount && !s.IsGhost && s.AssumeToken == null && !specContextOnly) {
+ CheckIsNonGhost(s.Expr);
+ }
+ }
+
bool ResolveAlternatives(List<GuardedAlternative> alternatives, bool specContextOnly, AlternativeLoopStmt loopToCatchBreaks, ICodeContext codeContext) {
Contract.Requires(alternatives != null);
Contract.Requires(codeContext != null);
@@ -5371,6 +5375,12 @@ namespace Microsoft.Dafny if (!moduleInfo.IsGhost)
CheckIsNonGhost(((NamedExpr)expr).Body);
return;
+ } else if (expr is ChainingExpression) {
+ // We don't care about the different operators; we only want the operands, so let's get them directly from
+ // the chaining expression
+ var e = (ChainingExpression)expr;
+ e.Operands.ForEach(CheckIsNonGhost);
+ return;
}
foreach (var ee in expr.SubExpressions) {
|