diff options
| -rw-r--r-- | Source/Dafny/Compiler.cs | 8 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 232 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 11 | ||||
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy | 24 | ||||
| -rw-r--r-- | Test/dafny0/SmallTests.dfy | 4 | ||||
| -rw-r--r-- | Test/dafny0/TypeTests.dfy | 4 | ||||
| -rw-r--r-- | Test/dafny2/StoreAndRetrieve.dfy | 4 |
7 files changed, 158 insertions, 129 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 4c334033..dd50c4eb 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -1065,13 +1065,7 @@ namespace Microsoft.Dafny { } else if (stmt is AssignSuchThatStmt) {
var s = (AssignSuchThatStmt)stmt;
- foreach (var lhs in s.Lhss) {
- // assigning to a local ghost variable or to a ghost field is okay
- if (!AssignStmt.LhsIsToGhost(lhs)) {
- Error("compiling an assign-such-that statement with a non-ghost left-hand side is currently not supported (line {0})", stmt.Tok.line);
- break; // no need to say more
- }
- }
+ Error("compilation of assign-such-that statements is currently not supported (line {0})", stmt.Tok.line);
} else if (stmt is VarDecl) {
TrVarDecl((VarDecl)stmt, true, indent);
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) {
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 370e3c38..e7fda470 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -91,10 +91,11 @@ TypeTests.dfy(90,6): Error: sorry, cannot instantiate collection type with a sub TypeTests.dfy(91,9): Error: sorry, cannot instantiate type parameter with a subrange type
TypeTests.dfy(92,8): Error: sorry, cannot instantiate 'array' type with a subrange type
TypeTests.dfy(93,8): Error: sorry, cannot instantiate 'array' type with a subrange type
-TypeTests.dfy(117,4): Error: cannot assign to non-ghost variable in a ghost context
-TypeTests.dfy(118,7): Error: cannot assign to non-ghost variable in a ghost context
+TypeTests.dfy(105,15): Error: ghost variables are allowed only in specification contexts
+TypeTests.dfy(115,4): Error: cannot assign to non-ghost variable in a ghost context
+TypeTests.dfy(116,7): Error: cannot assign to non-ghost variable in a ghost context
TypeTests.dfy(18,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed
-36 resolution/type errors detected in TypeTests.dfy
+37 resolution/type errors detected in TypeTests.dfy
-------------------- NatTypes.dfy --------------------
NatTypes.dfy(7,5): Error: value assigned to a nat must be non-negative
@@ -556,7 +557,9 @@ ResolutionErrors.dfy(372,10): Error: second argument to ==> must be of type bool ResolutionErrors.dfy(377,10): Error: first argument to ==> must be of type bool (instead got int)
ResolutionErrors.dfy(377,10): Error: second argument to ==> must be of type bool (instead got int)
ResolutionErrors.dfy(382,6): Error: print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
-62 resolution/type errors detected in ResolutionErrors.dfy
+ResolutionErrors.dfy(434,7): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(440,12): Error: ghost variables are allowed only in specification contexts
+64 resolution/type errors detected in ResolutionErrors.dfy
-------------------- ParseErrors.dfy --------------------
ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 7c919b2a..d5fecdf8 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -423,3 +423,27 @@ class Lamb { method Jesus() { }
method Gwen() { }
}
+
+// ------------------- assign-such-that and ghosts ------------------------------
+
+method AssignSuchThatFromGhost()
+{
+ var x: int;
+ ghost var g: int;
+
+ x := g; // error: ghost cannot flow into non-ghost
+
+ x := *;
+ assume x == g; // this mix of ghosts and non-ghosts is cool (but, of course,
+ // the compiler will complain)
+
+ x :| x == g; // error: left-side has non-ghost, so RHS must be non-ghost as well
+
+ x :| assume x == g; // this is cool, since it's an assume (but, of course, the
+ // compiler will complain)
+
+ x :| x == 5;
+ g :| g <= g;
+ g :| assume g < g; // the compiler will complain here, despite the LHS being
+ // ghost -- and rightly so, since an assume is used
+}
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index 7b409a67..43ee1d8e 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -530,7 +530,7 @@ method AssignSuchThat0(a: int, b: int) returns (x: int, y: int) method AssignSuchThat1(a: int, b: int) returns (x: int, y: int)
{
- var k :| assume 0 <= k < a - b; // this acts like an 'assume 0 < a - b;'
+ ghost var k :| assume 0 <= k < a - b; // this acts like an 'assume 0 < a - b;'
assert b < a;
k :| k == old(2*k); // note, the 'old' has no effect on local variables like k
assert k == 0;
@@ -571,7 +571,7 @@ method AssignSuchThat4() method AssignSuchThat5()
{
- var n := new Node;
+ ghost var n := new Node;
n :| fresh(n); // fine
assert false; // error
}
diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy index 2dea7a52..42457918 100644 --- a/Test/dafny0/TypeTests.dfy +++ b/Test/dafny0/TypeTests.dfy @@ -101,10 +101,8 @@ method M() ghost var k: int, l: int;
var m: int;
- // These three statements are allowed by the resolver, but the compiler will complain
- // if it ever gets them.
k :| k < 10;
- k, m :| 0 <= k < m;
+ k, m :| 0 <= k < m; // error: LHS has non-ghost and RHS has ghost
m :| m < 10;
// Because of the ghost guard, these 'if' statements are ghost contexts, so only
diff --git a/Test/dafny2/StoreAndRetrieve.dfy b/Test/dafny2/StoreAndRetrieve.dfy index da62f91c..d8938aa7 100644 --- a/Test/dafny2/StoreAndRetrieve.dfy +++ b/Test/dafny2/StoreAndRetrieve.dfy @@ -19,7 +19,7 @@ ghost module A { ensures Contents == old(Contents);
ensures thing in Contents && L.Function.Apply(matchCriterion, thing);
{
- var k :| k in Contents && L.Function.Apply(matchCriterion, k);
+ var k :| assume k in Contents && L.Function.Apply(matchCriterion, k);
thing := k;
}
}
@@ -52,7 +52,7 @@ module B refines A { }
var k := arr[i];
...;
- var a :| Contents == set x | x in a;
+ var a :| assume Contents == set x | x in a;
arr := a;
}
}
|