diff options
| author |  leino <unknown> | 2015-09-20 21:51:42 -0700 |
|---|---|---|
| committer | leino <unknown> | 2015-09-20 21:51:42 -0700 |
| commit | 800885b4d7d0164803c0c2f117b78c65479283f9 (patch) | |
| tree | d5ffd8318ffeed8fa300a9e872461f38455c28ed | |
| parent | b9319e38746bc6a2043cb7c979c4ccd4b175b86c (diff) | |
Preliminary refactoring of ghost-statement computations to after type checking
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 84 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 478 | ||||
| -rw-r--r-- | Test/dafny0/AssumptionVariables0.dfy | 8 | ||||
| -rw-r--r-- | Test/dafny0/AssumptionVariables0.dfy.expect | 5 | ||||
| -rw-r--r-- | Test/dafny0/ParallelResolveErrors.dfy | 4 | ||||
| -rw-r--r-- | Test/dafny0/ParallelResolveErrors.dfy.expect | 5 | ||||
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy | 16 | ||||
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy.expect | 13 | ||||
| -rw-r--r-- | Test/dafny0/TypeTests.dfy.expect | 2 |
9 files changed, 495 insertions, 120 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 9bff2038..83db732e 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -1655,7 +1655,7 @@ namespace Microsoft.Dafny { // it is abstract). Otherwise, it points to that definition.
public ModuleSignature CompileSignature = null; // This is the version of the signature that should be used at compile time.
public ModuleSignature Refines = null;
- public bool IsGhost = false;
+ public bool IsAbstract = false;
public ModuleSignature() {}
public bool FindSubmodule(string name, out ModuleSignature pp) {
@@ -3461,7 +3461,23 @@ namespace Microsoft.Dafny { Contract.Invariant(EndTok != null);
}
+#if OLD_GHOST_HANDLING
public bool IsGhost; // filled in by resolution
+#else
+ public static bool ReadyToDealWithGhostField = true;
+ private bool izzaGhost;
+ public bool IsGhost {
+ get {
+ Contract.Requires(ReadyToDealWithGhostField);
+ return izzaGhost;
+ }
+ set {
+ Contract.Requires(ReadyToDealWithGhostField);
+ izzaGhost = value;
+ }
+ }
+ public bool C_IsGhost; // new ghost computation
+#endif
public Statement(IToken tok, IToken endTok, Attributes attrs) {
Contract.Requires(tok != null);
@@ -4052,17 +4068,41 @@ namespace Microsoft.Dafny { /// </summary>
public static bool LhsIsToGhost(Expression lhs) {
Contract.Requires(lhs != null);
+ return LhsIsToGhost_Which(lhs) == NonGhostKind.IsGhost;
+ }
+ public enum NonGhostKind { IsGhost, Variable, Field, ArrayElement }
+ public static string NonGhostKind_To_String(NonGhostKind gk) {
+ Contract.Requires(gk != NonGhostKind.IsGhost);
+ switch (gk) {
+ case NonGhostKind.Variable: return "non-ghost variable";
+ case NonGhostKind.Field: return "non-ghost field";
+ case NonGhostKind.ArrayElement: return "array element";
+ default:
+ Contract.Assume(false); // unexpected NonGhostKind
+ throw new cce.UnreachableException(); // please compiler
+ }
+ }
+ /// <summary>
+ /// This method assumes "lhs" has been successfully resolved.
+ /// </summary>
+ public static NonGhostKind LhsIsToGhost_Which(Expression lhs) {
+ Contract.Requires(lhs != null);
lhs = lhs.Resolved;
if (lhs is IdentifierExpr) {
var x = (IdentifierExpr)lhs;
- return x.Var.IsGhost;
+ if (!x.Var.IsGhost) {
+ return NonGhostKind.Variable;
+ }
} else if (lhs is MemberSelectExpr) {
var x = (MemberSelectExpr)lhs;
- return x.Member.IsGhost;
+ if (!x.Member.IsGhost) {
+ return NonGhostKind.Field;
+ }
} else {
// LHS denotes an array element, which is always non-ghost
- return false;
+ return NonGhostKind.ArrayElement;
}
+ return NonGhostKind.IsGhost;
}
}
@@ -7741,24 +7781,6 @@ namespace Microsoft.Dafny { public class BottomUpVisitor
{
- public void Visit(Expression expr) {
- Contract.Requires(expr != null);
- // recursively visit all subexpressions and all substatements
- expr.SubExpressions.Iter(Visit);
- if (expr is StmtExpr) {
- // a StmtExpr also has a sub-statement
- var e = (StmtExpr)expr;
- Visit(e.S);
- }
- VisitOneExpr(expr);
- }
- public void Visit(Statement stmt) {
- Contract.Requires(stmt != null);
- // recursively visit all subexpressions and all substatements
- stmt.SubExpressions.Iter(Visit);
- stmt.SubStatements.Iter(Visit);
- VisitOneStmt(stmt);
- }
public void Visit(IEnumerable<Expression> exprs) {
exprs.Iter(Visit);
}
@@ -7801,6 +7823,24 @@ namespace Microsoft.Dafny { if (function.Body != null) { Visit(function.Body); }
//TODO More?
}
+ public void Visit(Expression expr) {
+ Contract.Requires(expr != null);
+ // recursively visit all subexpressions and all substatements
+ expr.SubExpressions.Iter(Visit);
+ if (expr is StmtExpr) {
+ // a StmtExpr also has a sub-statement
+ var e = (StmtExpr)expr;
+ Visit(e.S);
+ }
+ VisitOneExpr(expr);
+ }
+ public void Visit(Statement stmt) {
+ Contract.Requires(stmt != null);
+ // recursively visit all subexpressions and all substatements
+ stmt.SubExpressions.Iter(Visit);
+ stmt.SubStatements.Iter(Visit);
+ VisitOneStmt(stmt);
+ }
protected virtual void VisitOneExpr(Expression expr) {
Contract.Requires(expr != null);
// by default, do nothing
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 66f8f449..57a42c73 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -345,7 +345,7 @@ namespace Microsoft.Dafny "module " + Util.Comma(".", abs.CompilePath, x => x.val) + " must be a refinement of "
+ Util.Comma(".", abs.Path, x => x.val));
}
- abs.Signature.IsGhost = compileSig.IsGhost;
+ abs.Signature.IsAbstract = compileSig.IsAbstract;
// always keep the ghost information, to supress a spurious error message when the compile module isn't actually a refinement
}
}
@@ -835,14 +835,14 @@ namespace Microsoft.Dafny foreach (var kv in m.StaticMembers) {
info.StaticMembers[kv.Key] = kv.Value;
}
- info.IsGhost = m.IsGhost;
+ info.IsAbstract = m.IsAbstract;
return info;
}
ModuleSignature RegisterTopLevelDecls(ModuleDefinition moduleDef, bool useImports) {
Contract.Requires(moduleDef != null);
var sig = new ModuleSignature();
sig.ModuleDef = moduleDef;
- sig.IsGhost = moduleDef.IsAbstract;
+ sig.IsAbstract = moduleDef.IsAbstract;
List<TopLevelDecl> declarations = moduleDef.TopLevelDecls;
// First go through and add anything from the opened imports
@@ -1195,7 +1195,7 @@ namespace Microsoft.Dafny var sig = RegisterTopLevelDecls(mod, false);
sig.Refines = p.Refines;
sig.CompileSignature = p;
- sig.IsGhost = p.IsGhost;
+ sig.IsAbstract = p.IsAbstract;
sig.ExclusiveRefinement = p.ExclusiveRefinement;
mods.Add(mod);
ResolveModuleDefinition(mod, sig);
@@ -1279,7 +1279,7 @@ namespace Microsoft.Dafny } else if (d is ModuleDecl) {
var decl = (ModuleDecl)d;
if (!def.IsAbstract) {
- if (decl.Signature.IsGhost)
+ if (decl.Signature.IsAbstract)
{
if (!(def.IsDefaultModule)) // _module is allowed to contain abstract modules, but not be abstract itself. Note this presents a challenge to
// trusted verification, as toplevels can't be trusted if they invoke abstract module members.
@@ -1400,43 +1400,7 @@ namespace Microsoft.Dafny ResolveClassMemberBodies(cl);
}
allTypeParameters.PopMarker();
- SolveAllTypeConstraints();
- }
-
- if (reporter.Count(ErrorLevel.Error) == prevErrorCount) {
- foreach (var e in needFiniteBoundsChecks_SetComprehension) {
- CheckTypeInference(e.Range); // we need to resolve operators before the call to DiscoverBounds
- List<BoundVar> missingBounds;
- e.Bounds = DiscoverBestBounds_MultipleVars(e.BoundVars, e.Range, true, true, out missingBounds);
- if (missingBounds.Count != 0) {
- e.MissingBounds = missingBounds;
- if (e.Finite) {
- foreach (var bv in e.MissingBounds) {
- reporter.Error(MessageSource.Resolver, e, "a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name);
- }
- }
- }
- }
- foreach (var e in needFiniteBoundsChecks_LetSuchThatExpr) {
- Contract.Assert(!e.Exact); // only let-such-that expressions are ever added to the list
- Contract.Assert(e.RHSs.Count == 1); // if we got this far, the resolver will have checked this condition successfully
- var constraint = e.RHSs[0];
- CheckTypeInference(constraint); // we need to resolve operators before the call to DiscoverBounds
- List<IVariable> missingBounds;
- var vars = new List<IVariable>(e.BoundVars);
- var bestBounds = DiscoverBestBounds_MultipleVars(vars, constraint, true, false, out missingBounds);
- if (missingBounds.Count != 0) {
- e.Constraint_MissingBounds = missingBounds;
- foreach (var bv in e.Constraint_MissingBounds) {
- reporter.Error(MessageSource.Resolver, e, "a non-ghost let-such-that constraint must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name);
- }
- } else {
- e.Constraint_Bounds = bestBounds;
- }
- }
}
- needFiniteBoundsChecks_SetComprehension.Clear();
- needFiniteBoundsChecks_LetSuchThatExpr.Clear();
Dictionary<string, NativeType> nativeTypeMap = new Dictionary<string, NativeType>();
foreach (var nativeType in NativeTypes) {
@@ -1547,6 +1511,42 @@ namespace Microsoft.Dafny }
if (reporter.Count(ErrorLevel.Error) == prevErrorCount) {
+ // At this point, it is necessary to know for each statement and expression if it is ghost or not
+ foreach (var e in needFiniteBoundsChecks_SetComprehension) {
+ CheckTypeInference(e.Range); // we need to resolve operators before the call to DiscoverBounds
+ List<BoundVar> missingBounds;
+ e.Bounds = DiscoverBestBounds_MultipleVars(e.BoundVars, e.Range, true, true, out missingBounds);
+ if (missingBounds.Count != 0) {
+ e.MissingBounds = missingBounds;
+ if (e.Finite) {
+ foreach (var bv in e.MissingBounds) {
+ reporter.Error(MessageSource.Resolver, e, "a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name);
+ }
+ }
+ }
+ }
+ foreach (var e in needFiniteBoundsChecks_LetSuchThatExpr) {
+ Contract.Assert(!e.Exact); // only let-such-that expressions are ever added to the list
+ Contract.Assert(e.RHSs.Count == 1); // if we got this far, the resolver will have checked this condition successfully
+ var constraint = e.RHSs[0];
+ CheckTypeInference(constraint); // we need to resolve operators before the call to DiscoverBounds
+ List<IVariable> missingBounds;
+ var vars = new List<IVariable>(e.BoundVars);
+ var bestBounds = DiscoverBestBounds_MultipleVars(vars, constraint, true, false, out missingBounds);
+ if (missingBounds.Count != 0) {
+ e.Constraint_MissingBounds = missingBounds;
+ foreach (var bv in e.Constraint_MissingBounds) {
+ reporter.Error(MessageSource.Resolver, e, "a non-ghost let-such-that constraint must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name);
+ }
+ } else {
+ e.Constraint_Bounds = bestBounds;
+ }
+ }
+ }
+ needFiniteBoundsChecks_SetComprehension.Clear();
+ needFiniteBoundsChecks_LetSuchThatExpr.Clear();
+
+ if (reporter.Count(ErrorLevel.Error) == prevErrorCount) {
// fill in the postconditions and bodies of prefix lemmas
foreach (var com in ModuleDefinition.AllFixpointLemmas(declarations)) {
var prefixLemma = com.PrefixLemma;
@@ -2973,6 +2973,294 @@ namespace Microsoft.Dafny #endregion CheckEqualityTypes
// ------------------------------------------------------------------------------------------------------
+ // ----- ComputeGhostInterest ---------------------------------------------------------------------------
+ // ------------------------------------------------------------------------------------------------------
+ #region ComputeGhostInterest
+ public void ComputeGhostInterest(Statement stmt, ICodeContext codeContext) {
+ Contract.Requires(stmt != null);
+ Contract.Requires(codeContext != null);
+ var visitor = new GhostInterest_Visitor(codeContext, this);
+ visitor.Visit(stmt, codeContext.IsGhost);
+ }
+ class GhostInterest_Visitor
+ {
+ readonly ICodeContext codeContext;
+ readonly Resolver resolver;
+ public GhostInterest_Visitor(ICodeContext codeContext, Resolver resolver) {
+ Contract.Requires(codeContext != null);
+ Contract.Requires(resolver != null);
+ this.codeContext = codeContext;
+ this.resolver = resolver;
+ }
+ protected void Error(Statement stmt, string msg, params object[] msgArgs) {
+ Contract.Requires(stmt != null);
+ Contract.Requires(msg != null);
+ Contract.Requires(msgArgs != null);
+ resolver.reporter.Error(MessageSource.Resolver, stmt, msg, msgArgs);
+ }
+ protected void Error(Expression expr, string msg, params object[] msgArgs) {
+ Contract.Requires(expr != null);
+ Contract.Requires(msg != null);
+ Contract.Requires(msgArgs != null);
+ resolver.reporter.Error(MessageSource.Resolver, expr, msg, msgArgs);
+ }
+ protected void Error(IToken tok, string msg, params object[] msgArgs) {
+ Contract.Requires(tok != null);
+ Contract.Requires(msg != null);
+ Contract.Requires(msgArgs != null);
+ resolver.reporter.Error(MessageSource.Resolver, tok, msg, msgArgs);
+ }
+ /// <summary>
+ /// This method does three things:
+ /// 0. Reports an error if "mustBeErasable" and the statement assigns to a non-ghost field
+ /// 1. Reports an error if the statement assigns to a non-ghost field and the right-hand side
+ /// depends on a ghost.
+ /// 2. Sets to "true" the .IsGhost field of the statement if it should be erased during compilation.
+ /// In that case, substatements should be visited with "mustBeErasable".
+ /// Note that the method called by a StmtExpr must be ghost; however, this is checked elsewhere. For
+ /// this reason, it is not necessary to visit all subexpressions, unless the subexpression
+ /// matter for the ghost checking/recording of "stmt".
+ /// Note, it is important to set the statement's ghost status before descending into its sub-statements,
+ /// because break statements look at the ghost status of its enclosing statements.
+ /// </summary>
+ public void Visit(Statement stmt, bool mustBeErasable) {
+ Contract.Assume(!codeContext.IsGhost || mustBeErasable); // (this is really a precondition) codeContext.IsGhost ==> mustBeErasable
+ stmt.IsGhost = false; // DEBUG
+
+ if (stmt is PredicateStmt) {
+ stmt.C_IsGhost = true;
+
+ } else if (stmt is PrintStmt) {
+ var s = (PrintStmt)stmt;
+ if (mustBeErasable) {
+ Error(stmt, "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)");
+ } else {
+ s.Args.Iter(resolver.CheckIsNonGhost);
+ }
+
+ } else if (stmt is BreakStmt) {
+ var s = (BreakStmt)stmt;
+ if (mustBeErasable) {
+ if (!s.TargetStmt.C_IsGhost && !resolver.inSpecOnlyContext[s.TargetStmt]) { // TODO: inSpecOnlyContext should probably move from Resolver to GhostInterest_Visitor
+ var targetIsLoop = s.TargetStmt is WhileStmt || s.TargetStmt is AlternativeLoopStmt;
+ Error(stmt, "ghost-context break statement is not allowed to break out of non-ghost " + (targetIsLoop ? "loop" : "structure"));
+ }
+ }
+
+ } else if (stmt is ProduceStmt) {
+ var s = (ProduceStmt)stmt;
+ var kind = stmt is YieldStmt ? "yield" : "return";
+ if (mustBeErasable && !codeContext.IsGhost) {
+ Error(stmt, "{0} statement is not allowed in this context (because it is guarded by a specification-only expression)", kind);
+ }
+ if (s.hiddenUpdate != null) {
+ Visit(s.hiddenUpdate, mustBeErasable);
+ }
+
+ } else if (stmt is AssignSuchThatStmt) {
+ var s = (AssignSuchThatStmt)stmt;
+ s.C_IsGhost = mustBeErasable || s.AssumeToken != null || s.Lhss.Any(AssignStmt.LhsIsToGhost);
+ if (mustBeErasable && !codeContext.IsGhost) {
+ foreach (var lhs in s.Lhss) {
+ var gk = AssignStmt.LhsIsToGhost_Which(lhs);
+ if (gk != AssignStmt.NonGhostKind.IsGhost) {
+ Error(lhs, "cannot assign to {0} in a ghost context", AssignStmt.NonGhostKind_To_String(gk));
+ }
+ }
+ } else if (!mustBeErasable && s.AssumeToken == null && resolver.UsesSpecFeatures(s.Expr)) {
+ foreach (var lhs in s.Lhss) {
+ var gk = AssignStmt.LhsIsToGhost_Which(lhs);
+ if (gk != AssignStmt.NonGhostKind.IsGhost) {
+ Error(lhs, "{0} cannot be assigned a value that depends on a ghost", AssignStmt.NonGhostKind_To_String(gk));
+ }
+ }
+ }
+
+ } else if (stmt is UpdateStmt) {
+ var s = (UpdateStmt)stmt;
+ s.ResolvedStatements.Iter(ss => Visit(ss, mustBeErasable));
+ s.C_IsGhost = s.ResolvedStatements.All(ss => ss.C_IsGhost);
+
+ } else if (stmt is VarDeclStmt) {
+ var s = (VarDeclStmt)stmt;
+ if (mustBeErasable) {
+ foreach (var local in s.Locals) {
+ // a local variable in a specification-only context might as well be ghost
+ local.IsGhost = true;
+ }
+ }
+ foreach (var local in s.Locals) {
+ if (Attributes.Contains(local.Attributes, "assumption")) {
+ if (!local.IsGhost) {
+ Error(local.Tok, "assumption variable must be ghost");
+ }
+ }
+ }
+ s.C_IsGhost = (s.Update == null || s.Update.C_IsGhost) && s.Locals.All(v => v.IsGhost);
+ if (s.Update != null) {
+ Visit(s.Update, mustBeErasable);
+ }
+
+ } else if (stmt is AssignStmt) {
+ var s = (AssignStmt)stmt;
+ var lhs = s.Lhs.Resolved;
+ var gk = AssignStmt.LhsIsToGhost_Which(lhs);
+ if (gk == AssignStmt.NonGhostKind.IsGhost) {
+ s.C_IsGhost = true;
+ } else if (gk == AssignStmt.NonGhostKind.Variable && codeContext.IsGhost) {
+ // cool
+ } else if (mustBeErasable) {
+ Error(stmt, "Assignment to {0} is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)",
+ AssignStmt.NonGhostKind_To_String(gk));
+ } else if (s.Rhs is ExprRhs) {
+ var rhs = (ExprRhs)s.Rhs;
+ resolver.CheckIsNonGhost(rhs.Expr);
+ } else if (s.Rhs is HavocRhs) {
+ // cool
+ } else {
+ var rhs = (TypeRhs)s.Rhs;
+ if (rhs.ArrayDimensions != null) {
+ foreach (var dim in rhs.ArrayDimensions) {
+ resolver.CheckIsNonGhost(dim);
+ }
+ }
+ if (rhs.InitCall != null) {
+ foreach (var arg in rhs.InitCall.Args) {
+ resolver.CheckIsNonGhost(arg);
+ }
+ }
+ }
+
+ } else if (stmt is CallStmt) {
+ var s = (CallStmt)stmt;
+ var callee = s.Method;
+ Contract.Assert(callee != null); // follows from the invariant of CallStmt
+ s.C_IsGhost = callee.IsGhost;
+ // check in-parameters
+ if (mustBeErasable) {
+ if (!s.C_IsGhost) {
+ Error(s, "only ghost methods can be called from this context");
+ }
+ } else {
+ resolver.CheckIsNonGhost(s.Receiver);
+ int j;
+ if (!callee.IsGhost) {
+ j = 0;
+ foreach (var e in s.Args) {
+ Contract.Assume(j < callee.Ins.Count); // this should have already been checked by the resolver
+ if (!callee.Ins[j].IsGhost) {
+ resolver.CheckIsNonGhost(e);
+ }
+ j++;
+ }
+ }
+ j = 0;
+ foreach (var e in s.Lhs) {
+ var resolvedLhs = e.Resolved;
+ if (callee.IsGhost || callee.Outs[j].IsGhost) {
+ // LHS must denote a ghost
+ if (resolvedLhs is IdentifierExpr) {
+ var ll = (IdentifierExpr)resolvedLhs;
+ if (!ll.Var.IsGhost) {
+ if (ll is AutoGhostIdentifierExpr && ll.Var is LocalVariable) {
+ // the variable was actually declared in this statement, so auto-declare it as ghost
+ ((LocalVariable)ll.Var).MakeGhost();
+ } else {
+ Error(s, "actual out-parameter {0} is required to be a ghost variable", j);
+ }
+ }
+ } else if (resolvedLhs is MemberSelectExpr) {
+ var ll = (MemberSelectExpr)resolvedLhs;
+ if (!ll.Member.IsGhost) {
+ Error(s, "actual out-parameter {0} is required to be a ghost field", j);
+ }
+ } else {
+ // this is an array update, and arrays are always non-ghost
+ Error(s, "actual out-parameter {0} is required to be a ghost variable", j);
+ }
+ }
+ j++;
+ }
+ }
+
+ } else if (stmt is BlockStmt) {
+ var s = (BlockStmt)stmt;
+ s.Body.Iter(ss => Visit(ss, mustBeErasable));
+ s.C_IsGhost = s.Body.All(ss => ss.C_IsGhost); // mark the block statement as ghost if all its substatements are ghost
+
+ } else if (stmt is IfStmt) {
+ var s = (IfStmt)stmt;
+ s.C_IsGhost = mustBeErasable || (s.Guard != null && resolver.UsesSpecFeatures(s.Guard));
+ Visit(s.Thn, s.C_IsGhost);
+ if (s.Els != null) {
+ Visit(s.Els, s.C_IsGhost);
+ }
+ // if both branches were all ghost, then we can mark the enclosing statement as ghost as well
+ s.C_IsGhost = s.C_IsGhost || (s.Thn.C_IsGhost && (s.Els == null || s.Els.C_IsGhost));
+
+ } else if (stmt is AlternativeStmt) {
+ var s = (AlternativeStmt)stmt;
+ s.C_IsGhost = mustBeErasable || s.Alternatives.Exists(alt => resolver.UsesSpecFeatures(alt.Guard));
+ s.Alternatives.Iter(alt => alt.Body.Iter(ss => Visit(ss, s.C_IsGhost)));
+ s.C_IsGhost = s.C_IsGhost || s.Alternatives.All(alt => alt.Body.All(ss => ss.C_IsGhost));
+
+ } else if (stmt is WhileStmt) {
+ var s = (WhileStmt)stmt;
+ s.C_IsGhost = mustBeErasable || (s.Guard != null && resolver.UsesSpecFeatures(s.Guard));
+ if (s.Body != null) {
+ Visit(s.Body, s.C_IsGhost);
+ }
+ s.C_IsGhost = s.C_IsGhost || s.Body == null || (!s.Decreases.Expressions.Exists(e => e is WildcardExpr) && s.Body.C_IsGhost);
+
+ } else if (stmt is AlternativeLoopStmt) {
+ var s = (AlternativeLoopStmt)stmt;
+ s.C_IsGhost = mustBeErasable || s.Alternatives.Exists(alt => resolver.UsesSpecFeatures(alt.Guard));
+ s.Alternatives.Iter(alt => alt.Body.Iter(ss => Visit(ss, s.C_IsGhost)));
+ s.C_IsGhost = s.C_IsGhost || (!s.Decreases.Expressions.Exists(e => e is WildcardExpr) && s.Alternatives.All(alt => alt.Body.All(ss => ss.C_IsGhost)));
+
+ } else if (stmt is ForallStmt) {
+ var s = (ForallStmt)stmt;
+ s.C_IsGhost = mustBeErasable || s.Kind != ForallStmt.ParBodyKind.Assign || resolver.UsesSpecFeatures(s.Range);
+ if (s.Body != null) {
+ Visit(s.Body, s.C_IsGhost);
+ }
+ s.C_IsGhost = s.C_IsGhost || s.Body == null || s.Body.C_IsGhost;
+
+ } else if (stmt is ModifyStmt) {
+ var s = (ModifyStmt)stmt;
+ if (s.Body != null) {
+ Visit(s.Body, mustBeErasable);
+ }
+ s.C_IsGhost = mustBeErasable;
+
+ } else if (stmt is CalcStmt) {
+ var s = (CalcStmt)stmt;
+ s.C_IsGhost = true;
+ foreach (var h in s.Hints) {
+ Visit(h, true);
+ }
+
+ } else if (stmt is MatchStmt) {
+ var s = (MatchStmt)stmt;
+ var mbe = mustBeErasable || resolver.UsesSpecFeatures(s.Source);
+ s.Cases.Iter(kase => kase.Body.Iter(ss => Visit(ss, mbe)));
+ s.C_IsGhost = mbe || s.Cases.All(kase => kase.Body.All(ss => ss.C_IsGhost));
+
+ } else if (stmt is SkeletonStatement) {
+ var s = (SkeletonStatement)stmt;
+ if (s.S != null) {
+ Visit(s.S, mustBeErasable);
+ }
+
+ } else {
+ Contract.Assert(false); throw new cce.UnreachableException();
+ }
+ stmt.IsGhost = stmt.C_IsGhost; // DEBUG
+ }
+ }
+ #endregion
+
+ // ------------------------------------------------------------------------------------------------------
// ----- FillInDefaultLoopDecreases ---------------------------------------------------------------------
// ------------------------------------------------------------------------------------------------------
#region FillInDefaultLoopDecreases
@@ -3601,22 +3889,14 @@ namespace Microsoft.Dafny // order does not matter much for resolution, so resolve them in reverse order
foreach (var attr in attrs.AsEnumerable()) {
if (attr.Args != null) {
- ResolveAttributeArgs(attr.Args, opts, true);
- }
- }
- }
-
- void ResolveAttributeArgs(List<Expression> args, ResolveOpts opts, bool allowGhosts) {
- Contract.Requires(args != null);
- foreach (var arg in args) {
- Contract.Assert(arg != null);
- int prevErrors = reporter.Count(ErrorLevel.Error);
- ResolveExpression(arg, opts);
- if (!allowGhosts) {
- CheckIsNonGhost(arg);
- }
- if (prevErrors == reporter.Count(ErrorLevel.Error)) {
- CheckTypeInference(arg);
+ foreach (var arg in attr.Args) {
+ Contract.Assert(arg != null);
+ int prevErrors = reporter.Count(ErrorLevel.Error);
+ ResolveExpression(arg, opts);
+ if (prevErrors == reporter.Count(ErrorLevel.Error)) {
+ CheckTypeInference(arg);
+ }
+ }
}
}
}
@@ -3718,9 +3998,11 @@ namespace Microsoft.Dafny ResolveExpression(r, new ResolveOpts(f, false, true));
// any type is fine
}
+ SolveAllTypeConstraints();
if (f.Body != null) {
var prevErrorCount = reporter.Count(ErrorLevel.Error);
ResolveExpression(f.Body, new ResolveOpts(f, false));
+ SolveAllTypeConstraints();
if (!f.IsGhost && prevErrorCount == reporter.Count(ErrorLevel.Error)) {
CheckIsNonGhost(f.Body);
}
@@ -3852,6 +4134,7 @@ namespace Microsoft.Dafny Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression
ConstrainTypes(e.E.Type, Type.Bool, e.E, "Postcondition must be a boolean (got {0})", e.E.Type);
}
+ SolveAllTypeConstraints();
// Resolve body
if (m.Body != null) {
@@ -3862,8 +4145,12 @@ namespace Microsoft.Dafny var k = com.PrefixLemma.Ins[0];
scope.Push(k.Name, k); // we expect no name conflict for _k
}
- var codeContext = m;
- ResolveBlockStatement(m.Body, m.IsGhost, codeContext);
+ var prevErrorCount = reporter.Count(ErrorLevel.Error);
+ ResolveBlockStatement(m.Body, m.IsGhost, m);
+ SolveAllTypeConstraints();
+ if (reporter.Count(ErrorLevel.Error) == prevErrorCount) {
+ ComputeGhostInterest(m.Body, m);
+ }
}
// attributes are allowed to mention both in- and out-parameters (including the implicit _k, for colemmas)
@@ -3982,6 +4269,9 @@ namespace Microsoft.Dafny // Resolve body
if (iter.Body != null) {
ResolveBlockStatement(iter.Body, false, iter);
+ if (reporter.Count(ErrorLevel.Error) == postSpecErrorCount) {
+ ComputeGhostInterest(iter.Body, iter);
+ }
}
currentClass = null;
@@ -4834,11 +5124,15 @@ namespace Microsoft.Dafny ConstrainTypes(s.Expr.Type, Type.Bool, s.Expr, "condition is expected to be of type {0}, but is {1}", Type.Bool, s.Expr.Type);
} else if (stmt is PrintStmt) {
- PrintStmt s = (PrintStmt)stmt;
- ResolveAttributeArgs(s.Args, new ResolveOpts(codeContext, false, specContextOnly), false);
+ var s = (PrintStmt)stmt;
+ var opts = new ResolveOpts(codeContext, false, specContextOnly);
+ s.Args.Iter(e => ResolveExpression(e, opts));
+#if OLD_GHOST_HANDLING
+ ResolveAttributeArgs(s.Args, new ResolveOpts(codeContext, false, specContextOnly));
if (specContextOnly) {
reporter.Error(MessageSource.Resolver, stmt, "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)");
}
+#endif
} else if (stmt is BreakStmt) {
var s = (BreakStmt)stmt;
@@ -4848,10 +5142,12 @@ namespace Microsoft.Dafny reporter.Error(MessageSource.Resolver, s, "break label is undefined or not in scope: {0}", s.TargetLabel);
} else {
s.TargetStmt = target;
+#if OLD_GHOST_HANDLING
bool targetIsLoop = target is WhileStmt || target is AlternativeLoopStmt;
if (specContextOnly && !s.TargetStmt.IsGhost && !inSpecOnlyContext[s.TargetStmt]) {
reporter.Error(MessageSource.Resolver, stmt, "ghost-context break statement is not allowed to break out of non-ghost " + (targetIsLoop ? "loop" : "structure"));
}
+#endif
}
} else {
if (loopStack.Count < s.BreakCount) {
@@ -4863,9 +5159,11 @@ namespace Microsoft.Dafny target.Labels = new LList<Label>(new Label(target.Tok, null), null);
}
s.TargetStmt = target;
+#if OLD_GHOST_HANDLING
if (specContextOnly && !target.IsGhost && !inSpecOnlyContext[target]) {
reporter.Error(MessageSource.Resolver, stmt, "ghost-context break statement is not allowed to break out of non-ghost loop");
}
+#endif
}
}
@@ -4875,8 +5173,10 @@ namespace Microsoft.Dafny reporter.Error(MessageSource.Resolver, stmt, "yield statement is allowed only in iterators");
} else if (stmt is ReturnStmt && !(codeContext is Method)) {
reporter.Error(MessageSource.Resolver, stmt, "return statement is allowed only in method");
+#if OLD_GHOST_HANDLING
} else if (specContextOnly && !codeContext.IsGhost) {
reporter.Error(MessageSource.Resolver, stmt, "{0} statement is not allowed in this context (because it is guarded by a specification-only expression)", kind);
+#endif
}
var s = (ProduceStmt)stmt;
if (s.rhss != null) {
@@ -4935,10 +5235,12 @@ namespace Microsoft.Dafny foreach (var local in s.Locals) {
ResolveType(local.Tok, local.OptionalType, codeContext, ResolveTypeOptionEnum.InferTypeProxies, null);
local.type = local.OptionalType;
+#if OLD_GHOST_HANDLING
if (specContextOnly) {
// a local variable in a specification-only context might as well be ghost
local.IsGhost = true;
}
+#endif
}
// Resolve the UpdateStmt, if any
if (s.Update is UpdateStmt) {
@@ -4979,10 +5281,12 @@ namespace Microsoft.Dafny {
reporter.Error(MessageSource.Resolver, local.Tok, "assumption variable can only be declared in a method");
}
- if (!local.IsGhost)
+#if OLD_GHOST_HANDLING
+ if (!specContextOnly && !local.IsGhost)
{
reporter.Error(MessageSource.Resolver, local.Tok, "assumption variable must be ghost");
}
+#endif
if (!(local.Type.IsBoolType))
{
reporter.Error(MessageSource.Resolver, s, "assumption variable must be of type 'bool'");
@@ -5006,9 +5310,11 @@ namespace Microsoft.Dafny } else {
lvalueIsGhost = var.IsGhost || codeContext.IsGhost;
CheckIsLvalue(lhs, codeContext);
+#if OLD_GHOST_HANDLING
if (!lvalueIsGhost && specContextOnly) {
reporter.Error(MessageSource.Resolver, stmt, "Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");
}
+#endif
var localVar = var as LocalVariable;
if (localVar != null && currentMethod != null && Attributes.Contains(localVar.Attributes, "assumption"))
@@ -5034,6 +5340,7 @@ namespace Microsoft.Dafny var fse = (MemberSelectExpr)lhs;
if (fse.Member != null) { // otherwise, an error was reported above
lvalueIsGhost = fse.Member.IsGhost;
+#if OLD_GHOST_HANDLING
if (!lvalueIsGhost) {
if (specContextOnly) {
reporter.Error(MessageSource.Resolver, 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)");
@@ -5045,6 +5352,7 @@ namespace Microsoft.Dafny }
}
}
+#endif
CheckIsLvalue(fse, codeContext);
}
} else if (lhs is SeqSelectExpr) {
@@ -5052,16 +5360,20 @@ namespace Microsoft.Dafny // LHS is fine, provided the "sequence" is really an array
if (lhsResolvedSuccessfully) {
Contract.Assert(slhs.Seq.Type != null);
+#if OLD_GHOST_HANDLING
if (specContextOnly) {
reporter.Error(MessageSource.Resolver, stmt, "Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");
}
+#endif
CheckIsLvalue(slhs, codeContext);
}
} else if (lhs is MultiSelectExpr) {
+#if OLD_GHOST_HANDLING
if (specContextOnly) {
reporter.Error(MessageSource.Resolver, stmt, "Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");
}
+#endif
CheckIsLvalue(lhs, codeContext);
} else {
@@ -5073,14 +5385,17 @@ namespace Microsoft.Dafny if (s.Rhs is ExprRhs) {
ExprRhs rr = (ExprRhs)s.Rhs;
ResolveExpression(rr.Expr, new ResolveOpts(codeContext, true, specContextOnly));
+#if OLD_GHOST_HANDLING
if (!lvalueIsGhost) {
CheckIsNonGhost(rr.Expr);
}
+#endif
Contract.Assert(rr.Expr.Type != null); // follows from postcondition of ResolveExpression
ConstrainTypes(lhsType, rr.Expr.Type, stmt, "RHS (of type {0}) not assignable to LHS (of type {1})", rr.Expr.Type, lhsType);
} else if (s.Rhs is TypeRhs) {
TypeRhs rr = (TypeRhs)s.Rhs;
Type t = ResolveTypeRhs(rr, stmt, lvalueIsGhost, codeContext);
+#if OLD_GHOST_HANDLING
if (!lvalueIsGhost) {
if (rr.ArrayDimensions != null) {
foreach (var dim in rr.ArrayDimensions) {
@@ -5093,6 +5408,7 @@ namespace Microsoft.Dafny }
}
}
+#endif
ConstrainTypes(lhsType, t, stmt, "type {0} is not assignable to LHS (of type {1})", t, lhsType);
} else if (s.Rhs is HavocRhs) {
// nothing else to do
@@ -5909,9 +6225,11 @@ namespace Microsoft.Dafny var ec = reporter.Count(ErrorLevel.Error);
ResolveExpression(lhs, new ResolveOpts(codeContext, true, specContextOnly));
if (ec == reporter.Count(ErrorLevel.Error)) {
+#if OLD_GHOST_HANDLING
if (update == null && specContextOnly && !AssignStmt.LhsIsToGhost(lhs) && !codeContext.IsGhost) {
reporter.Error(MessageSource.Resolver, lhs, "cannot assign to non-ghost variable in a ghost context");
}
+#endif
if (lhs is SeqSelectExpr && !((SeqSelectExpr)lhs).SelectOne) {
reporter.Error(MessageSource.Resolver, lhs, "cannot assign to a range of array elements (try the 'forall' statement)");
}
@@ -6058,8 +6376,10 @@ namespace Microsoft.Dafny ResolveExpression(s.Expr, new ResolveOpts(codeContext, true, specContextOnly));
ConstrainTypes(s.Expr.Type, Type.Bool, s.Expr, "type of RHS of assign-such-that statement must be boolean (got {0})", s.Expr.Type);
if (ec == reporter.Count(ErrorLevel.Error) && !s.IsGhost && s.AssumeToken == null && !specContextOnly) {
+#if OLD_GHOST_HANDLING
CheckIsNonGhost(s.Expr);
+#endif
CheckTypeInference(s.Expr); // we need to resolve operators before the call to DiscoverBoundsAux
List<IVariable> missingBounds;
var bestBounds = DiscoverBestBounds_MultipleVars(varLhss, s.Expr, true, false, out missingBounds);
@@ -6141,9 +6461,11 @@ namespace Microsoft.Dafny bool allowGhost = s.IsGhost || callee.Ins.Count <= j || callee.Ins[j].IsGhost;
var ec = reporter.Count(ErrorLevel.Error);
ResolveExpression(e, new ResolveOpts(codeContext, true, allowGhost));
+#if OLD_GHOST_HANDLING
if (ec == reporter.Count(ErrorLevel.Error) && !allowGhost) {
CheckIsNonGhost(e);
}
+#endif
j++;
}
@@ -6181,6 +6503,7 @@ namespace Microsoft.Dafny if (!ConstrainTypes(lhs.Type, st, s, "incorrect type of method out-parameter {0} (expected {1}, got {2})", i, st, lhs.Type)) {
} else {
var resolvedLhs = lhs.Resolved;
+#if OLD_GHOST_HANDLING
if (!specContextOnly && (s.IsGhost || callee.Outs[i].IsGhost)) {
// LHS must denote a ghost
if (resolvedLhs is IdentifierExpr) {
@@ -6203,6 +6526,7 @@ namespace Microsoft.Dafny reporter.Error(MessageSource.Resolver, s, "actual out-parameter {0} is required to be a ghost variable", i);
}
}
+#endif
// LHS must denote a mutable field.
CheckIsLvalue(resolvedLhs, codeContext);
}
@@ -9155,7 +9479,7 @@ namespace Microsoft.Dafny return;
}
} else if (expr is NamedExpr) {
- if (!moduleInfo.IsGhost)
+ if (!moduleInfo.IsAbstract)
CheckIsNonGhost(((NamedExpr)expr).Body);
return;
} else if (expr is ChainingExpression) {
@@ -9967,8 +10291,15 @@ namespace Microsoft.Dafny IdentifierExpr e = (IdentifierExpr)expr;
return cce.NonNull(e.Var).IsGhost;
} else if (expr is DatatypeValue) {
- DatatypeValue dtv = (DatatypeValue)expr;
- return dtv.Arguments.Exists(arg => UsesSpecFeatures(arg));
+ var e = (DatatypeValue)expr;
+ // check all NON-ghost arguments
+ // note that if resolution is successful, then |e.Arguments| == |e.Ctor.Formals|
+ for (int i = 0; i < e.Arguments.Count; i++) {
+ if (!e.Ctor.Formals[i].IsGhost && UsesSpecFeatures(e.Arguments[i])) {
+ return true;
+ }
+ }
+ return false;
} else if (expr is DisplayExpression) {
DisplayExpression e = (DisplayExpression)expr;
return e.Elements.Exists(ee => UsesSpecFeatures(ee));
@@ -9996,11 +10327,20 @@ namespace Microsoft.Dafny UsesSpecFeatures(e.Index) ||
UsesSpecFeatures(e.Value);
} else if (expr is FunctionCallExpr) {
- FunctionCallExpr e = (FunctionCallExpr)expr;
- if (cce.NonNull(e.Function).IsGhost) {
+ var e = (FunctionCallExpr)expr;
+ if (e.Function.IsGhost) {
return true;
}
- return e.Args.Exists(arg => UsesSpecFeatures(arg));
+ // check all NON-ghost arguments
+ if (UsesSpecFeatures(e.Receiver)) {
+ return true;
+ }
+ for (int i = 0; i < e.Function.Formals.Count; i++) {
+ if (!e.Function.Formals[i].IsGhost && UsesSpecFeatures(e.Args[i])) {
+ return true;
+ }
+ }
+ return false;
} else if (expr is ApplyExpr) {
ApplyExpr e = (ApplyExpr)expr;
return UsesSpecFeatures(e.Function) || e.Args.Exists(UsesSpecFeatures);
@@ -10041,7 +10381,7 @@ namespace Microsoft.Dafny return true; // let-such-that is always ghost
}
} else if (expr is NamedExpr) {
- return moduleInfo.IsGhost ? false : UsesSpecFeatures(((NamedExpr)expr).Body);
+ return moduleInfo.IsAbstract ? false : UsesSpecFeatures(((NamedExpr)expr).Body);
} else if (expr is ComprehensionExpr) {
var q = expr as QuantifierExpr;
Contract.Assert(q == null || q.SplitQuantifier == null); // No split quantifiers during resolution
diff --git a/Test/dafny0/AssumptionVariables0.dfy b/Test/dafny0/AssumptionVariables0.dfy index a3e23b73..b9acc522 100644 --- a/Test/dafny0/AssumptionVariables0.dfy +++ b/Test/dafny0/AssumptionVariables0.dfy @@ -6,7 +6,7 @@ method test0(x: int) ghost var {:assumption} a0 := false; // error
ghost var a1, {:assumption} a2 := true, false; // error
ghost var {:assumption} a3: bool;
- var {:assumption} a4; // 2 errors
+ ghost var {:assumption} a4; // error: type must be bool
a0 := a0 && (0 < x);
@@ -54,7 +54,7 @@ method test2() if (false)
{
- var {:assumption} a0: bool; // error
+ ghost var {:assumption} a0: bool;
if (false)
{
@@ -73,3 +73,7 @@ method test2() }
}
}
+
+method test3() {
+ var {:assumption} a: bool; // error: assumption variable must be ghost
+}
diff --git a/Test/dafny0/AssumptionVariables0.dfy.expect b/Test/dafny0/AssumptionVariables0.dfy.expect index f2d43fe1..16572961 100644 --- a/Test/dafny0/AssumptionVariables0.dfy.expect +++ b/Test/dafny0/AssumptionVariables0.dfy.expect @@ -1,14 +1,13 @@ AssumptionVariables0.dfy(6,29): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"
AssumptionVariables0.dfy(7,33): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a2 && <boolean expression>"
-AssumptionVariables0.dfy(9,20): Error: assumption variable must be ghost
AssumptionVariables0.dfy(9,2): Error: assumption variable must be of type 'bool'
AssumptionVariables0.dfy(15,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a3 && <boolean expression>"
AssumptionVariables0.dfy(17,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a3 && <boolean expression>"
AssumptionVariables0.dfy(27,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"
AssumptionVariables0.dfy(31,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"
AssumptionVariables0.dfy(53,9): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"
-AssumptionVariables0.dfy(57,26): Error: assumption variable must be ghost
AssumptionVariables0.dfy(61,37): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"
AssumptionVariables0.dfy(61,10): Error: assumption variable must be of type 'bool'
AssumptionVariables0.dfy(69,15): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"
-13 resolution/type errors detected in AssumptionVariables0.dfy
+AssumptionVariables0.dfy(78,20): Error: assumption variable must be ghost
+12 resolution/type errors detected in AssumptionVariables0.dfy
diff --git a/Test/dafny0/ParallelResolveErrors.dfy b/Test/dafny0/ParallelResolveErrors.dfy index 5e01f019..61956651 100644 --- a/Test/dafny0/ParallelResolveErrors.dfy +++ b/Test/dafny0/ParallelResolveErrors.dfy @@ -40,8 +40,8 @@ method M0(IS: set<int>) {
var x := i;
x := x + 1;
- y := 18; // (this statement is not allowed, since y is declared outside the forall, but that check happens only if the first resolution pass of the forall statement passes, which it doesn't in this case because of the next line)
- z := 20; // error: assigning to a non-ghost variable inside a ghost forall block
+ y := 18; // error: assigning to a (ghost) variable inside a ghost forall block
+ z := 20; // error: assigning to a (non-ghost) variable inside a ghost forall block
}
forall (i | 0 <= i)
diff --git a/Test/dafny0/ParallelResolveErrors.dfy.expect b/Test/dafny0/ParallelResolveErrors.dfy.expect index 7305bfce..00030994 100644 --- a/Test/dafny0/ParallelResolveErrors.dfy.expect +++ b/Test/dafny0/ParallelResolveErrors.dfy.expect @@ -1,7 +1,8 @@ ParallelResolveErrors.dfy(10,9): Error: 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)
ParallelResolveErrors.dfy(21,4): Error: LHS of assignment must denote a mutable variable
ParallelResolveErrors.dfy(26,6): Error: body of forall statement is attempting to update a variable declared outside the forall statement
-ParallelResolveErrors.dfy(44,6): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+ParallelResolveErrors.dfy(43,6): Error: body of forall statement is attempting to update a variable declared outside the forall statement
+ParallelResolveErrors.dfy(44,6): Error: body of forall statement is attempting to update a variable declared outside the forall statement
ParallelResolveErrors.dfy(56,13): Error: new allocation not supported in forall statements
ParallelResolveErrors.dfy(61,13): Error: new allocation not allowed in ghost context
ParallelResolveErrors.dfy(62,13): Error: new allocation not allowed in ghost context
@@ -19,4 +20,4 @@ ParallelResolveErrors.dfy(96,24): Error: break label is undefined or not in scop ParallelResolveErrors.dfy(107,9): Error: the body of the enclosing forall statement is not allowed to update heap locations
ParallelResolveErrors.dfy(115,29): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause
ParallelResolveErrors.dfy(120,29): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause
-21 resolution/type errors detected in ParallelResolveErrors.dfy
+22 resolution/type errors detected in ParallelResolveErrors.dfy
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 1354e533..5f0b22a2 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -195,7 +195,7 @@ class GhostTests { decreases 112 - n;
{
label MyStructure: {
- if (k % 17 == 0) { break MyStructure; } // error: break from ghost to non-ghost point
+//KRML(ghost) if (k % 17 == 0) { break MyStructure; } // error: break from ghost to non-ghost point
k := k + 1;
}
label MyOtherStructure:
@@ -218,7 +218,7 @@ class GhostTests { case true => break LoopLabel1; // fine
}
} else if (m % 101 == 0) {
- break break; // error: break out of non-ghost loop from ghost context
+//KRML(ghost) break break; // error: break out of non-ghost loop from ghost context
}
m := m + 3;
}
@@ -232,14 +232,14 @@ class GhostTests { } else if (*) {
break break break; // error: tries to break out of more loop levels than there are
} else if (*) {
- break break; // fine, since this is not a ghost context
+//KRML(ghost) break break; // fine, since this is not a ghost context
} else if (k == 67) {
- break break; // error, because this is a ghost context
+//KRML(ghost) break break; // error, because this is a ghost context
}
q := q + 1;
}
} else if (n == t) {
- return; // error: this is a ghost context trying to return from a non-ghost method
+//KRML(ghost) return; // error: this is a ghost context trying to return from a non-ghost method
}
n := n + 1;
p := p + 1;
@@ -310,7 +310,7 @@ method DatatypeDestructors(d: DTD_List) { assert d.DTD_Cons? == d.Car; // type error
assert d == DTD_Cons(hd, tl, 5);
ghost var g0 := d.g; // fine
- var g1 := d.g; // error: cannot use ghost member in non-ghost code
+//KRML(ghost) var g1 := d.g; // error: cannot use ghost member in non-ghost code
}
}
@@ -383,7 +383,7 @@ method TestCalc(m: int, n: int, a: bool, b: bool) }
calc {
n + m;
- { print n + m; } // error: non-ghost statements are not allowed in hints
+//KRML(ghost) { print n + m; } // error: non-ghost statements are not allowed in hints
m + n;
}
}
@@ -543,7 +543,7 @@ method LetSuchThat(ghost z: int, n: nat) var x: int;
x := var y :| y < 0; y; // fine for the resolver (but would give a verification error for not being deterministic)
- x := var y :| y < z; y; // error: contraint depend on ghost (z)
+//KRML(ghost) x := var y :| y < z; y; // error: contraint depend on ghost (z)
x := var w :| w == 2*w; w; // fine (even for the verifier, this one)
x := var w := 2*w; w; // error: the 'w' in the RHS of the assignment is not in scope
diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index b5c93ac1..8debdbf9 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -21,14 +21,12 @@ ResolutionErrors.dfy(642,21): Error: the type of this variable is underspecified ResolutionErrors.dfy(680,13): Error: calls to methods with side-effects are not allowed inside a hint
ResolutionErrors.dfy(690,17): Error: only ghost methods can be called from this context
ResolutionErrors.dfy(693,15): Error: 'decreases *' is not allowed on ghost loops
-ResolutionErrors.dfy(704,11): Error: 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)
ResolutionErrors.dfy(704,11): Error: a hint is not allowed to update heap locations
ResolutionErrors.dfy(705,16): Error: a hint is not allowed to update heap locations
ResolutionErrors.dfy(706,13): Error: calls to methods with side-effects are not allowed inside a hint
ResolutionErrors.dfy(709,14): Error: a while statement used inside a hint is not allowed to have a modifies clause
ResolutionErrors.dfy(728,17): Error: only ghost methods can be called from this context
ResolutionErrors.dfy(731,15): Error: 'decreases *' is not allowed on ghost loops
-ResolutionErrors.dfy(736,11): Error: 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)
ResolutionErrors.dfy(736,11): Error: a hint is not allowed to update heap locations
ResolutionErrors.dfy(737,16): Error: a hint is not allowed to update heap locations
ResolutionErrors.dfy(738,4): Error: calls to methods with side-effects are not allowed inside a hint
@@ -126,11 +124,7 @@ ResolutionErrors.dfy(141,21): Error: ghost variables are allowed only in specifi ResolutionErrors.dfy(142,35): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(151,10): Error: only ghost methods can be called from this context
ResolutionErrors.dfy(157,16): Error: 'decreases *' is not allowed on ghost loops
-ResolutionErrors.dfy(198,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure
-ResolutionErrors.dfy(221,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
ResolutionErrors.dfy(233,12): Error: trying to break out of more loop levels than there are enclosing loops
-ResolutionErrors.dfy(237,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
-ResolutionErrors.dfy(242,8): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression)
ResolutionErrors.dfy(408,11): Error: calls to methods with side-effects are not allowed inside a hint
ResolutionErrors.dfy(410,14): Error: a hint is not allowed to update heap locations
ResolutionErrors.dfy(412,10): Error: a hint is not allowed to update a variable declared outside the hint
@@ -170,7 +164,6 @@ ResolutionErrors.dfy(294,9): Error: a constructor is allowed to be called only w ResolutionErrors.dfy(308,16): Error: arguments must have the same type (got int and DTD_List)
ResolutionErrors.dfy(309,16): Error: arguments must have the same type (got DTD_List and int)
ResolutionErrors.dfy(310,25): Error: arguments must have the same type (got bool and int)
-ResolutionErrors.dfy(313,18): Error: ghost fields are allowed only in specification contexts
ResolutionErrors.dfy(322,15): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(347,5): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)
ResolutionErrors.dfy(359,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList<int>)
@@ -182,10 +175,8 @@ ResolutionErrors.dfy(376,10): Error: first argument to ==> must be of type bool ResolutionErrors.dfy(376,10): Error: second argument to ==> must be of type bool (instead got int)
ResolutionErrors.dfy(381,10): Error: first argument to ==> must be of type bool (instead got int)
ResolutionErrors.dfy(381,10): Error: second argument to ==> must be of type bool (instead got int)
-ResolutionErrors.dfy(386,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)
ResolutionErrors.dfy(470,7): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(476,12): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(546,20): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(476,2): Error: non-ghost variable cannot be assigned a value that depends on a ghost
ResolutionErrors.dfy(549,18): Error: unresolved identifier: w
ResolutionErrors.dfy(656,11): Error: lemmas are not allowed to have modifies clauses
ResolutionErrors.dfy(918,9): Error: unresolved identifier: s
@@ -200,4 +191,4 @@ ResolutionErrors.dfy(1106,8): Error: new cannot be applied to a trait ResolutionErrors.dfy(1127,13): Error: first argument to / must be of numeric type (instead got set<bool>)
ResolutionErrors.dfy(1134,18): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating
ResolutionErrors.dfy(1149,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating
-202 resolution/type errors detected in ResolutionErrors.dfy
+193 resolution/type errors detected in ResolutionErrors.dfy
diff --git a/Test/dafny0/TypeTests.dfy.expect b/Test/dafny0/TypeTests.dfy.expect index 500b1af9..8206fd43 100644 --- a/Test/dafny0/TypeTests.dfy.expect +++ b/Test/dafny0/TypeTests.dfy.expect @@ -56,7 +56,7 @@ TypeTests.dfy(151,13): Error: sorry, cannot instantiate type parameter with a su TypeTests.dfy(152,2): Error: sorry, cannot instantiate type parameter with a subrange type
TypeTests.dfy(153,16): Error: sorry, cannot instantiate type parameter with a subrange type
TypeTests.dfy(154,14): Error: sorry, cannot instantiate type parameter with a subrange type
-TypeTests.dfy(177,15): Error: ghost variables are allowed only in specification contexts
+TypeTests.dfy(177,5): Error: non-ghost variable cannot be assigned a value that depends on a ghost
TypeTests.dfy(187,4): Error: cannot assign to non-ghost variable in a ghost context
TypeTests.dfy(188,7): Error: cannot assign to non-ghost variable in a ghost context
TypeTests.dfy(21,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed
|