From e10098cde7bac9a7a1576000fa29d15f1fcd8970 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Thu, 2 Jul 2015 16:06:02 -0700 Subject: Type parameters in method/function signatures are no longer auto-declared. Although convenient and concise, the auto-declare behavior has on many occasions caused confusion when a type name has accidentally been mistyped (and Dafny had then accepted and auto-declared the name). Note, the behavior of filling in missing type parameters is still supported. This mode, although unusual (even original?) in languages, is different from the auto- declare behavior. For auto-declare, identifiers could be used in the program without having a declaration. For fill-in parameters, the implicitly declared type parameters remain anonymous. --- Test/dafny0/ResolutionErrors.dfy | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'Test/dafny0/ResolutionErrors.dfy') diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 761cffa0..8c910959 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -1253,14 +1253,14 @@ module SignatureCompletion { datatype Dt = Ctor(X -> Dt) // error: X is not a declared type datatype Et = Ctor(X -> Et, Y) // error: X is not a declared type - // For methods and functions, signatures can auto-declare type parameters - method My0(s: set, x: A -> B) - method My1(x: A -> B, s: set) + + method My0(s: set, x: A -> B) + method My1(x: A -> B, s: set) method My2(s: set, x: A -> B) method My3(x: A -> B, s: set) - function F0(s: set, x: A -> B): int - function F1(x: A -> B, s: set): int + function F0(s: set, x: A -> B): int + function F1(x: A -> B, s: set): int function F2(s: set, x: A -> B): int function F3(x: A -> B, s: set): int } -- cgit v1.2.3 From 7e7eb1a4177e03f6bb22411b7246db1d26f5ed27 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Wed, 29 Jul 2015 17:35:18 -0700 Subject: Fixed crash in resolution where, after reporting an error, the cases #type and #module were not handled --- Source/Dafny/Resolver.cs | 4 ++++ Test/dafny0/ResolutionErrors.dfy | 24 ++++++++++++++++++++++++ Test/dafny0/ResolutionErrors.dfy.expect | 16 +++++++++++++++- 3 files changed, 43 insertions(+), 1 deletion(-) (limited to 'Test/dafny0/ResolutionErrors.dfy') diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index e3083133..e977dbd5 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -4491,6 +4491,10 @@ namespace Microsoft.Dafny // something is wrong; either aa or bb wasn't properly resolved, or they don't unify return false; } + } else if (a is Resolver_IdentifierExpr.ResolverType_Type) { + return b is Resolver_IdentifierExpr.ResolverType_Type; + } else if (a is Resolver_IdentifierExpr.ResolverType_Module) { + return b is Resolver_IdentifierExpr.ResolverType_Module; } else { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type } diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 8c910959..900c7459 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -1349,3 +1349,27 @@ module TupleEqualitySupport { datatype GoodRecord = GoodRecord(set<(int,int)>) datatype BadRecord = BadRecord(set<(int, int->bool)>) // error: this tuple type does not support equality } + +// ------------------- non-type variable names ------------------- + +module NonTypeVariableNames { + type X = int + + module Y { } + + method M(m: map) + { + assert X == X; // error (x2): type name used as variable + assert Y == Y; // error (x2): module name used as variable + assert X in m; // error (x2): type name used as variable + assert Y in m; // error (x2): module name used as variable + } + + method N(k: int) + { + assert k == X; // error (x2): type name used as variable + assert k == Y; // error (x2): module name used as variable + X := k; // error: type name used as variable + Y := k; // error: module name used as variable + } +} diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index ae3e8cbf..481b47e0 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -90,6 +90,20 @@ ResolutionErrors.dfy(1329,15): Error: The name Inner ambiguously refers to a typ ResolutionErrors.dfy(1339,29): Error: ghost variables are allowed only in specification contexts ResolutionErrors.dfy(1341,49): Error: ghost variables are allowed only in specification contexts ResolutionErrors.dfy(1341,54): Error: ghost variables are allowed only in specification contexts +ResolutionErrors.dfy(1362,11): Error: name of type (X) is used as a variable +ResolutionErrors.dfy(1362,16): Error: name of type (X) is used as a variable +ResolutionErrors.dfy(1363,11): Error: name of module (Y) is used as a variable +ResolutionErrors.dfy(1363,16): Error: name of module (Y) is used as a variable +ResolutionErrors.dfy(1364,11): Error: name of type (X) is used as a variable +ResolutionErrors.dfy(1364,13): Error: second argument to "in" must be a set, multiset, or sequence with elements of type #type, or a map with domain #type (instead got map) +ResolutionErrors.dfy(1365,11): Error: name of module (Y) is used as a variable +ResolutionErrors.dfy(1365,13): Error: second argument to "in" must be a set, multiset, or sequence with elements of type #module, or a map with domain #module (instead got map) +ResolutionErrors.dfy(1370,16): Error: name of type (X) is used as a variable +ResolutionErrors.dfy(1370,13): Error: arguments must have the same type (got int and #type) +ResolutionErrors.dfy(1371,16): Error: name of module (Y) is used as a variable +ResolutionErrors.dfy(1371,13): Error: arguments must have the same type (got int and #module) +ResolutionErrors.dfy(1372,4): Error: name of type (X) is used as a variable +ResolutionErrors.dfy(1373,4): Error: name of module (Y) is used as a variable ResolutionErrors.dfy(432,2): Error: More than one anonymous constructor ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context ResolutionErrors.dfy(87,14): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny') @@ -182,4 +196,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) 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 -184 resolution/type errors detected in ResolutionErrors.dfy +198 resolution/type errors detected in ResolutionErrors.dfy -- cgit v1.2.3 From d023b0e19f7bf886801a3a059511b8449d8ab223 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 31 Jul 2015 16:58:36 -0700 Subject: Bug fix: check that assign-such-that constraint is of type boolean --- Source/Dafny/Resolver.cs | 3 +++ Test/dafny0/ResolutionErrors.dfy | 15 +++++++++++++++ Test/dafny0/ResolutionErrors.dfy.expect | 6 +++++- 3 files changed, 23 insertions(+), 1 deletion(-) (limited to 'Test/dafny0/ResolutionErrors.dfy') diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index e977dbd5..a58d6e6c 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -6100,6 +6100,9 @@ namespace Microsoft.Dafny s.IsGhost = s.Lhss.TrueForAll(AssignStmt.LhsIsToGhost); var ec = ErrorCount; ResolveExpression(s.Expr, new ResolveOpts(codeContext, true, specContextOnly)); + if (!UnifyTypes(s.Expr.Type, Type.Bool)) { + Error(s.Expr, "type of RHS of assign-such-that statement must be boolean (got {0})", s.Expr.Type); + } if (ec == ErrorCount && !s.IsGhost && s.AssumeToken == null && !specContextOnly) { CheckIsNonGhost(s.Expr); diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 900c7459..1354e533 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -1373,3 +1373,18 @@ module NonTypeVariableNames { Y := k; // error: module name used as variable } } + +// ------------------- assign-such-that and let-such-that ------------------- + +module SuchThat { + method M() { + var x: int; + x :| 5 + 7; // error: constraint should be boolean + x :| x; // error: constraint should be boolean + var y :| 4; // error: constraint should be boolean + } + function F(): int { + var w :| 6 + 8; // error: constraint should be boolean + w + } +} diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index 481b47e0..b5c93ac1 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -104,6 +104,10 @@ ResolutionErrors.dfy(1371,16): Error: name of module (Y) is used as a variable ResolutionErrors.dfy(1371,13): Error: arguments must have the same type (got int and #module) ResolutionErrors.dfy(1372,4): Error: name of type (X) is used as a variable ResolutionErrors.dfy(1373,4): Error: name of module (Y) is used as a variable +ResolutionErrors.dfy(1382,11): Error: type of RHS of assign-such-that statement must be boolean (got int) +ResolutionErrors.dfy(1383,9): Error: type of RHS of assign-such-that statement must be boolean (got int) +ResolutionErrors.dfy(1384,13): Error: type of RHS of assign-such-that statement must be boolean (got int) +ResolutionErrors.dfy(1387,15): Error: type of RHS of let-such-that expression must be boolean (got int) ResolutionErrors.dfy(432,2): Error: More than one anonymous constructor ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context ResolutionErrors.dfy(87,14): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny') @@ -196,4 +200,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) 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 -198 resolution/type errors detected in ResolutionErrors.dfy +202 resolution/type errors detected in ResolutionErrors.dfy -- cgit v1.2.3 From 800885b4d7d0164803c0c2f117b78c65479283f9 Mon Sep 17 00:00:00 2001 From: leino Date: Sun, 20 Sep 2015 21:51:42 -0700 Subject: Preliminary refactoring of ghost-statement computations to after type checking --- Source/Dafny/DafnyAst.cs | 84 +++-- Source/Dafny/Resolver.cs | 478 +++++++++++++++++++++++---- Test/dafny0/AssumptionVariables0.dfy | 8 +- Test/dafny0/AssumptionVariables0.dfy.expect | 5 +- Test/dafny0/ParallelResolveErrors.dfy | 4 +- Test/dafny0/ParallelResolveErrors.dfy.expect | 5 +- Test/dafny0/ResolutionErrors.dfy | 16 +- Test/dafny0/ResolutionErrors.dfy.expect | 13 +- Test/dafny0/TypeTests.dfy.expect | 2 +- 9 files changed, 495 insertions(+), 120 deletions(-) (limited to 'Test/dafny0/ResolutionErrors.dfy') 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); @@ -4051,18 +4067,42 @@ namespace Microsoft.Dafny { /// This method assumes "lhs" has been successfully resolved. /// 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 + } + } + /// + /// This method assumes "lhs" has been successfully resolved. + /// + 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 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 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 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 missingBounds; - var vars = new List(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 nativeTypeMap = new Dictionary(); foreach (var nativeType in NativeTypes) { @@ -1546,6 +1510,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 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 missingBounds; + var vars = new List(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)) { @@ -2972,6 +2972,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); + } + /// + /// 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. + /// + 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 --------------------------------------------------------------------- // ------------------------------------------------------------------------------------------------------ @@ -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 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