diff options
29 files changed, 2532 insertions, 1461 deletions
diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs index e040402d..3002d832 100644 --- a/Binaries/DafnyRuntime.cs +++ b/Binaries/DafnyRuntime.cs @@ -1012,6 +1012,12 @@ namespace Dafny return pred(false) || pred(true); } } + public static bool QuantChar(bool frall, System.Predicate<char> pred) { + for (int i = 0; i < 0x10000; i++) { + if (pred((char)i) != frall) { return !frall; } + } + return frall; + } public static bool QuantInt(BigInteger lo, BigInteger hi, bool frall, System.Predicate<BigInteger> pred) { for (BigInteger i = lo; i < hi; i++) { if (pred(i) != frall) { return !frall; } @@ -1051,6 +1057,13 @@ namespace Dafny yield return true; } } + public static IEnumerable<char> AllChars { + get { + for (int i = 0; i < 0x10000; i++) { + yield return (char)i; + } + } + } public static IEnumerable<BigInteger> AllIntegers { get { yield return new BigInteger(0); @@ -27,7 +27,7 @@ Dafny's sources. 3. Download and build Dafny:
hg clone https://hg.codeplex.com/dafny
- cd dafny/Sources/
+ cd dafny/Source/
xbuild Dafny.sln
4. Download and unpack z3 (Dafny looks for `z3` in Binaries/z3/bin/)
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index 7046f9a4..c94c697d 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -550,13 +550,21 @@ namespace Microsoft.Dafny r = new ForallStmt(Tok(s.Tok), Tok(s.EndTok), s.BoundVars.ConvertAll(CloneBoundVar), null, CloneExpr(s.Range), s.Ens.ConvertAll(CloneMayBeFreeExpr), CloneStmt(s.Body));
} else if (stmt is CalcStmt) {
- var s = (CalcStmt)stmt;
- r = new CalcStmt(Tok(s.Tok), Tok(s.EndTok), CloneCalcOp(s.Op), s.Lines.ConvertAll(CloneExpr), s.Hints.ConvertAll(CloneBlockStmt), s.StepOps.ConvertAll(CloneCalcOp), CloneCalcOp(s.ResultOp), CloneAttributes(s.Attributes));
+ var s = (CalcStmt)stmt;
+ // calc statements have the unusual property that the last line is duplicated. If that is the case (which
+ // we expect it to be here), we share the clone of that line as well.
+ var lineCount = s.Lines.Count;
+ var lines = new List<Expression>(lineCount);
+ for (int i = 0; i < lineCount; i++) {
+ lines.Add(i == lineCount - 1 && 2 <= lineCount && s.Lines[i] == s.Lines[i - 1] ? lines[i - 1] : CloneExpr(s.Lines[i]));
+ }
+ Contract.Assert(lines.Count == lineCount);
+ r = new CalcStmt(Tok(s.Tok), Tok(s.EndTok), CloneCalcOp(s.Op), lines, s.Hints.ConvertAll(CloneBlockStmt), s.StepOps.ConvertAll(CloneCalcOp), CloneCalcOp(s.ResultOp), CloneAttributes(s.Attributes));
} else if (stmt is MatchStmt) {
var s = (MatchStmt)stmt;
r = new MatchStmt(Tok(s.Tok), Tok(s.EndTok), CloneExpr(s.Source),
- s.Cases.ConvertAll(CloneMatchCaseStmt), s.UsesOptionalBraces);
+ s.Cases.ConvertAll(CloneMatchCaseStmt), s.UsesOptionalBraces);
} else if (stmt is AssignSuchThatStmt) {
var s = (AssignSuchThatStmt)stmt;
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 123433bc..13381cc7 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -1610,6 +1610,9 @@ namespace Microsoft.Dafny { if (bound is ComprehensionExpr.BoolBoundedPool) {
Indent(ind);
wr.Write("foreach (var @{0} in Dafny.Helpers.AllBooleans) {{ ", bv.CompileName);
+ } else if (bound is ComprehensionExpr.CharBoundedPool) {
+ Indent(ind);
+ wr.Write("foreach (var @{0} in Dafny.Helpers.AllChars) {{ ", bv.CompileName);
} else if (bound is ComprehensionExpr.IntBoundedPool) {
var b = (ComprehensionExpr.IntBoundedPool)bound;
Indent(ind);
@@ -1821,6 +1824,8 @@ namespace Microsoft.Dafny { Indent(ind);
if (bound is ComprehensionExpr.BoolBoundedPool) {
wr.WriteLine("foreach (var {0} in Dafny.Helpers.AllBooleans) {{ @{1} = {0};", tmpVar, bv.CompileName);
+ } else if (bound is ComprehensionExpr.CharBoundedPool) {
+ wr.WriteLine("foreach (var {0} in Dafny.Helpers.AllChars) {{ @{1} = {0};", tmpVar, bv.CompileName);
} else if (bound is ComprehensionExpr.IntBoundedPool) {
var b = (ComprehensionExpr.IntBoundedPool)bound;
if (AsNativeType(bv.Type) != null) {
@@ -2875,6 +2880,8 @@ namespace Microsoft.Dafny { // emit: Dafny.Helpers.QuantX(boundsInformation, isForall, bv => body)
if (bound is ComprehensionExpr.BoolBoundedPool) {
wr.Write("Dafny.Helpers.QuantBool(");
+ } else if (bound is ComprehensionExpr.CharBoundedPool) {
+ wr.Write("Dafny.Helpers.QuantChar(");
} else if (bound is ComprehensionExpr.IntBoundedPool) {
var b = (ComprehensionExpr.IntBoundedPool)bound;
wr.Write("Dafny.Helpers.QuantInt(");
@@ -2942,6 +2949,8 @@ namespace Microsoft.Dafny { var bv = e.BoundVars[i];
if (bound is ComprehensionExpr.BoolBoundedPool) {
wr.Write("foreach (var @{0} in Dafny.Helpers.AllBooleans) {{ ", bv.CompileName);
+ } else if (bound is ComprehensionExpr.CharBoundedPool) {
+ wr.Write("foreach (var @{0} in Dafny.Helpers.AllChars) {{ ", bv.CompileName);
} else if (bound is ComprehensionExpr.IntBoundedPool) {
var b = (ComprehensionExpr.IntBoundedPool)bound;
if (AsNativeType(bv.Type) != null) {
@@ -3015,6 +3024,8 @@ namespace Microsoft.Dafny { var bv = e.BoundVars[0];
if (bound is ComprehensionExpr.BoolBoundedPool) {
wr.Write("foreach (var @{0} in Dafny.Helpers.AllBooleans) {{ ", bv.CompileName);
+ } else if (bound is ComprehensionExpr.CharBoundedPool) {
+ wr.Write("foreach (var @{0} in Dafny.Helpers.AllChars) {{ ", bv.CompileName);
} else if (bound is ComprehensionExpr.IntBoundedPool) {
var b = (ComprehensionExpr.IntBoundedPool)bound;
if (AsNativeType(bv.Type) != null) {
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 116b9004..4fc48f2f 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -526,6 +526,27 @@ namespace Microsoft.Dafny { }
}
+ public bool HasFinitePossibleValues {
+ get {
+ if (IsBoolType || IsCharType || IsRefType) {
+ return true;
+ }
+ var st = AsSetType;
+ if (st != null && st.Arg.HasFinitePossibleValues) {
+ return true;
+ }
+ var mt = AsMapType;
+ if (mt != null && mt.Domain.HasFinitePossibleValues) {
+ return true;
+ }
+ var dt = AsDatatype;
+ if (dt != null && dt.HasFinitePossibleValues) {
+ return true;
+ }
+ return false;
+ }
+ }
+
public CollectionType AsCollectionType { get { return NormalizeExpand() as CollectionType; } }
public SetType AsSetType { get { return NormalizeExpand() as SetType; } }
public MultiSetType AsMultiSetType { get { return NormalizeExpand() as MultiSetType; } }
@@ -1676,7 +1697,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) {
@@ -2417,6 +2438,48 @@ namespace Microsoft.Dafny { }
/// <summary>
+ /// Returns the non-null expressions of this declaration proper (that is, do not include the expressions of substatements).
+ /// Does not include the generated class members.
+ /// </summary>
+ public virtual IEnumerable<Expression> SubExpressions {
+ get {
+ foreach (var e in Attributes.SubExpressions(Attributes)) {
+ yield return e;
+ }
+ foreach (var e in Attributes.SubExpressions(Reads.Attributes)) {
+ yield return e;
+ }
+ foreach (var e in Reads.Expressions) {
+ yield return e.E;
+ }
+ foreach (var e in Attributes.SubExpressions(Modifies.Attributes)) {
+ yield return e;
+ }
+ foreach (var e in Modifies.Expressions) {
+ yield return e.E;
+ }
+ foreach (var e in Attributes.SubExpressions(Decreases.Attributes)) {
+ yield return e;
+ }
+ foreach (var e in Decreases.Expressions) {
+ yield return e;
+ }
+ foreach (var e in Requires) {
+ yield return e.E;
+ }
+ foreach (var e in Ensures) {
+ yield return e.E;
+ }
+ foreach (var e in YieldRequires) {
+ yield return e.E;
+ }
+ foreach (var e in YieldEnsures) {
+ yield return e.E;
+ }
+ }
+ }
+
+ /// <summary>
/// This Dafny type exists only for the purpose of giving the yield-count variable a type, so
/// that the type can be recognized during translation of Dafny into Boogie. It represents
/// an integer component in a "decreases" clause whose order is (\lambda x,y :: x GREATER y),
@@ -2523,6 +2586,11 @@ namespace Microsoft.Dafny { return EnclosingClass.FullCompileName + ".@" + CompileName;
}
}
+ public virtual IEnumerable<Expression> SubExpressions {
+ get {
+ yield break;
+ }
+ }
}
public class Field : MemberDecl {
@@ -3047,6 +3115,26 @@ namespace Microsoft.Dafny { public bool IsBuiltin;
public Function OverriddenFunction;
+ public override IEnumerable<Expression> SubExpressions {
+ get {
+ foreach (var e in Req) {
+ yield return e;
+ }
+ foreach (var e in Reads) {
+ yield return e.E;
+ }
+ foreach (var e in Ens) {
+ yield return e;
+ }
+ foreach (var e in Decreases.Expressions) {
+ yield return e;
+ }
+ if (Body != null) {
+ yield return Body;
+ }
+ }
+ }
+
public Type Type {
get {
// Note, the following returned type can contain type parameters from the function and its enclosing class
@@ -3261,6 +3349,24 @@ namespace Microsoft.Dafny { public readonly ISet<IVariable> AssignedAssumptionVariables = new HashSet<IVariable>();
public Method OverriddenMethod;
+ public override IEnumerable<Expression> SubExpressions {
+ get {
+ foreach (var e in Req) {
+ yield return e.E;
+ }
+ foreach (var e in Mod.Expressions) {
+ yield return e.E;
+ }
+ foreach (var e in Ens) {
+ yield return e.E;
+ }
+ foreach (var e in Decreases.Expressions) {
+ yield return e;
+ }
+ }
+ }
+
+
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(cce.NonNullElements(TypeArgs));
@@ -4100,17 +4206,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;
}
}
@@ -4845,18 +4975,32 @@ namespace Microsoft.Dafny { }
public override IEnumerable<Expression> SubExpressions
{
- get { // FIXME: This can return duplicates; this could confuse BottomUpVisitors that modify the AST in place
+ get {
foreach (var e in base.SubExpressions) { yield return e; }
foreach (var e in Attributes.SubExpressions(Attributes)) { yield return e; }
-
- foreach (var l in Lines) {
- yield return l;
+
+ for (int i = 0; i < Lines.Count - 1; i++) { // note, we skip the duplicated line at the end
+ yield return Lines[i];
}
- foreach (var e in Steps) {
- yield return e;
+ foreach (var calcop in AllCalcOps) {
+ var o3 = calcop as TernaryCalcOp;
+ if (o3 != null) {
+ yield return o3.Index;
+ }
+ }
+ }
+ }
+
+ IEnumerable<CalcOp> AllCalcOps {
+ get {
+ if (Op != null) {
+ yield return Op;
+ }
+ foreach (var stepop in StepOps) {
+ yield return stepop;
}
- if (Result != null) {
- yield return Result;
+ if (ResultOp != null) {
+ yield return ResultOp;
}
}
}
@@ -6670,7 +6814,7 @@ namespace Microsoft.Dafny { public readonly Expression Body;
public readonly bool Exact; // Exact==true means a regular let expression; Exact==false means an assign-such-that expression
public readonly Attributes Attributes;
- public List<ComprehensionExpr.BoundedPool> Constraint_Bounds; // initialized and filled in by resolver; null for Exact=true and for a ghost statement
+ public List<ComprehensionExpr.BoundedPool> Constraint_Bounds; // initialized and filled in by resolver; null for Exact=true and for when expression is in a ghost context
// invariant Constraint_Bounds == null || Constraint_Bounds.Count == BoundVars.Count;
public List<IVariable> Constraint_MissingBounds; // filled in during resolution; remains "null" if Exact==true or if bounds can be found
// invariant Constraint_Bounds == null || Constraint_MissingBounds == null;
@@ -6823,6 +6967,22 @@ namespace Microsoft.Dafny { return 5;
}
}
+ public class CharBoundedPool : BoundedPool
+ {
+ public override int Preference() {
+ return 4;
+ }
+ }
+ public class RefBoundedPool : BoundedPool
+ {
+ public Type Type;
+ public RefBoundedPool(Type t) {
+ Type = t;
+ }
+ public override int Preference() {
+ return 2;
+ }
+ }
public class IntBoundedPool : BoundedPool
{
public readonly Expression LowerBound;
@@ -6897,6 +7057,24 @@ namespace Microsoft.Dafny { public List<BoundVar> MissingBounds; // filled in during resolution; remains "null" if bounds can be found
// invariant Bounds == null || MissingBounds == null;
+ public List<BoundVar> UncompilableBoundVars() {
+ var bvs = new List<BoundVar>();
+ if (MissingBounds != null) {
+ bvs.AddRange(MissingBounds);
+ }
+ if (Bounds != null) {
+ Contract.Assert(Bounds.Count == BoundVars.Count);
+ for (int i = 0; i < Bounds.Count; i++) {
+ var bound = Bounds[i];
+ if (bound is RefBoundedPool) {
+ // yes, this is in principle a bound, but it's not one we'd like to compile
+ bvs.Add(BoundVars[i]);
+ }
+ }
+ }
+ return bvs;
+ }
+
public ComprehensionExpr(IToken tok, List<BoundVar> bvars, Expression range, Expression term, Attributes attrs)
: base(tok) {
Contract.Requires(tok != null);
@@ -7798,24 +7976,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);
}
@@ -7858,6 +8018,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 210cd4ac..0b0bbf26 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
}
}
@@ -667,13 +667,17 @@ namespace Microsoft.Dafny }
private void ResolveModuleDefinition(ModuleDefinition m, ModuleSignature sig) {
+ Contract.Requires(AllTypeConstraints.Count == 0);
+ Contract.Ensures(AllTypeConstraints.Count == 0);
moduleInfo = MergeSignature(sig, systemNameInfo);
// resolve
var datatypeDependencies = new Graph<IndDatatypeDecl>();
var codatatypeDependencies = new Graph<CoDatatypeDecl>();
int prevErrorCount = reporter.Count(ErrorLevel.Error);
ResolveTopLevelDecls_Signatures(m, m.TopLevelDecls, datatypeDependencies, codatatypeDependencies);
+ Contract.Assert(AllTypeConstraints.Count == 0); // signature resolution does not add any type constraints
ResolveAttributes(m.Attributes, new ResolveOpts(new NoContext(m.Module), false)); // Must follow ResolveTopLevelDecls_Signatures, in case attributes refer to members
+ SolveAllTypeConstraints(); // solve any type constraints entailed by the attributes
if (reporter.Count(ErrorLevel.Error) == prevErrorCount) {
ResolveTopLevelDecls_Core(m.TopLevelDecls, datatypeDependencies, codatatypeDependencies);
}
@@ -831,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
@@ -1260,7 +1264,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);
@@ -1352,7 +1356,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 (// _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.
@@ -1390,15 +1394,6 @@ namespace Microsoft.Dafny }
}
- private readonly List<SetComprehension> needFiniteBoundsChecks_SetComprehension = new List<SetComprehension>();
- private readonly List<LetExpr> needFiniteBoundsChecks_LetSuchThatExpr = new List<LetExpr>();
- public int NFBC_Count {
- // provided just for the purpose of conveniently writing contracts for ResolveTopLevelDecl_Meat
- get {
- return needFiniteBoundsChecks_SetComprehension.Count + needFiniteBoundsChecks_LetSuchThatExpr.Count;
- }
- }
-
static readonly List<NativeType> NativeTypes = new List<NativeType>() {
new NativeType("byte", 0, 0x100, "", true),
new NativeType("sbyte", -0x80, 0x80, "", true),
@@ -1414,11 +1409,18 @@ namespace Microsoft.Dafny Contract.Requires(declarations != null);
Contract.Requires(cce.NonNullElements(datatypeDependencies));
Contract.Requires(cce.NonNullElements(codatatypeDependencies));
- Contract.Requires(NFBC_Count == 0);
- Contract.Ensures(NFBC_Count == 0);
+ Contract.Requires(AllTypeConstraints.Count == 0);
+ Contract.Ensures(AllTypeConstraints.Count == 0);
int prevErrorCount = reporter.Count(ErrorLevel.Error);
+ // ---------------------------------- Pass 0 ----------------------------------
+ // This pass resolves names, introduces (and may solve) type constraints, and
+ // builds the module's call graph.
+ // For 'newtype' declarations, it also checks that all types were fully
+ // determined.
+ // ----------------------------------------------------------------------------
+
// Resolve the meat of classes and iterators, the definitions of type synonyms, and the type parameters of all top-level type declarations
// First, resolve the newtype declarations and the constraint clauses, including filling in .ResolvedOp fields. This is needed for the
// resolution of the other declarations, because those other declarations may invoke DiscoverBounds, which looks at the .Constraint field
@@ -1442,21 +1444,21 @@ namespace Microsoft.Dafny var added = scope.Push(dd.Var.Name, dd.Var);
Contract.Assert(added == Scope<IVariable>.PushResult.Success);
ResolveType(dd.Var.tok, dd.Var.Type, dd, ResolveTypeOptionEnum.DontInfer, null);
- ResolveExpression(dd.Constraint, new ResolveOpts(dd, false, true));
+ ResolveExpression(dd.Constraint, new ResolveOpts(dd, false));
Contract.Assert(dd.Constraint.Type != null); // follows from postcondition of ResolveExpression
- if (!UnifyTypes(dd.Constraint.Type, Type.Bool)) {
- reporter.Error(MessageSource.Resolver, dd.Constraint, "newtype constraint must be of type bool (instead got {0})", dd.Constraint.Type);
- }
+ ConstrainTypes(dd.Constraint.Type, Type.Bool, dd.Constraint, "newtype constraint must be of type bool (instead got {0})", dd.Constraint.Type);
+ SolveAllTypeConstraints();
if (!CheckTypeInference_Visitor.IsDetermined(dd.BaseType.NormalizeExpand())) {
reporter.Error(MessageSource.Resolver, dd.tok, "newtype's base type is not fully determined; add an explicit type for '{0}'", dd.Var.Name);
}
- CheckTypeInference(dd.Constraint);
+ CheckTypeInference(dd.Constraint, dd);
scope.PopMarker();
}
}
}
// Now, we're ready for the other declarations.
foreach (TopLevelDecl d in declarations) {
+ Contract.Assert(AllTypeConstraints.Count == 0);
if (d is TraitDecl && d.TypeArgs.Count > 0) {
reporter.Error(MessageSource.Resolver, d, "sorry, traits with type parameters are not supported");
}
@@ -1477,149 +1479,84 @@ namespace Microsoft.Dafny allTypeParameters.PopMarker();
}
- 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();
+ // ---------------------------------- Pass 1 ----------------------------------
+ // This pass:
+ // * checks that type inference was able to determine all types
+ // * fills in the .ResolvedOp field of binary expressions
+ // * discovers bounds for:
+ // - forall statements
+ // - set comprehensions
+ // - map comprehensions
+ // - quantifier expressions
+ // - assign-such-that statements
+ // - compilable let-such-that expressions
+ // - newtype constraints
+ // For each statement body that it successfully typed, this pass also:
+ // * computes ghost interests
+ // * determines/checks tail-recursion.
+ // ----------------------------------------------------------------------------
Dictionary<string, NativeType> nativeTypeMap = new Dictionary<string, NativeType>();
foreach (var nativeType in NativeTypes) {
nativeTypeMap.Add(nativeType.Name, nativeType);
}
-
if (reporter.Count(ErrorLevel.Error) == prevErrorCount) {
// Check that type inference went well everywhere; this will also fill in the .ResolvedOp field in binary expressions
foreach (TopLevelDecl d in declarations) {
if (d is IteratorDecl) {
var iter = (IteratorDecl)d;
+ var prevErrCnt = reporter.Count(ErrorLevel.Error);
iter.Members.Iter(CheckTypeInference_Member);
+ if (prevErrCnt == reporter.Count(ErrorLevel.Error)) {
+ iter.SubExpressions.Iter(e => CheckExpression(e, this, iter));
+ }
if (iter.Body != null) {
- CheckTypeInference(iter.Body);
+ CheckTypeInference(iter.Body, iter);
+ if (prevErrCnt == reporter.Count(ErrorLevel.Error)) {
+ ComputeGhostInterest(iter.Body, false, iter);
+ CheckExpression(iter.Body, this, iter);
+ }
}
} else if (d is ClassDecl) {
var cl = (ClassDecl)d;
- cl.Members.Iter(CheckTypeInference_Member);
- } else if (d is NewtypeDecl) {
- var dd = (NewtypeDecl)d;
- bool? boolNativeType = null;
- NativeType stringNativeType = null;
- object nativeTypeAttr = true;
- bool hasNativeTypeAttr = Attributes.ContainsMatchingValue(dd.Attributes, "nativeType", ref nativeTypeAttr,
- new Attributes.MatchingValueOption[] {
- Attributes.MatchingValueOption.Empty,
- Attributes.MatchingValueOption.Bool,
- Attributes.MatchingValueOption.String },
- err => reporter.Error(MessageSource.Resolver, dd, err));
- if (hasNativeTypeAttr) {
- if (nativeTypeAttr is bool) {
- boolNativeType = (bool)nativeTypeAttr;
- } else {
- string keyString = (string)nativeTypeAttr;
- if (nativeTypeMap.ContainsKey(keyString)) {
- stringNativeType = nativeTypeMap[keyString];
- } else {
- reporter.Error(MessageSource.Resolver, dd, "Unsupported nativeType {0}", keyString);
+ foreach (var member in cl.Members) {
+ var prevErrCnt = reporter.Count(ErrorLevel.Error);
+ CheckTypeInference_Member(member);
+ if (prevErrCnt == reporter.Count(ErrorLevel.Error)) {
+ if (member is Method) {
+ var m = (Method)member;
+ if (m.Body != null) {
+ ComputeGhostInterest(m.Body, m.IsGhost, m);
+ CheckExpression(m.Body, this, m);
+ DetermineTailRecursion(m);
+ }
+ } else if (member is Function) {
+ var f = (Function)member;
+ if (!f.IsGhost && f.Body != null) {
+ CheckIsCompilable(f.Body);
+ }
+ DetermineTailRecursion(f);
+ }
+ if (prevErrCnt == reporter.Count(ErrorLevel.Error) && member is ICodeContext) {
+ member.SubExpressions.Iter(e => CheckExpression(e, this, (ICodeContext)member));
}
}
}
- if (stringNativeType != null || boolNativeType == true) {
- if (!dd.BaseType.IsNumericBased(Type.NumericPersuation.Int)) {
- reporter.Error(MessageSource.Resolver, dd, "nativeType can only be used on integral types");
- }
- if (dd.Var == null) {
- reporter.Error(MessageSource.Resolver, dd, "nativeType can only be used if newtype specifies a constraint");
- }
- }
+ } else if (d is NewtypeDecl) {
+ var dd = (NewtypeDecl)d;
if (dd.Var != null) {
Contract.Assert(dd.Constraint != null);
- CheckTypeInference(dd.Constraint);
-
- Func<Expression, BigInteger?> GetConst = null;
- GetConst = (Expression e) => {
- int m = 1;
- BinaryExpr bin = e as BinaryExpr;
- if (bin != null && bin.Op == BinaryExpr.Opcode.Sub && GetConst(bin.E0) == BigInteger.Zero) {
- m = -1;
- e = bin.E1;
- }
- LiteralExpr l = e as LiteralExpr;
- if (l != null && l.Value is BigInteger) {
- return m * (BigInteger)l.Value;
- }
- return null;
- };
- var bounds = DiscoverAllBounds_SingleVar(dd.Var, dd.Constraint);
- List<NativeType> potentialNativeTypes =
- (stringNativeType != null) ? new List<NativeType> { stringNativeType } :
- (boolNativeType == false) ? new List<NativeType>() :
- NativeTypes;
- foreach (var nt in potentialNativeTypes) {
- bool lowerOk = false;
- bool upperOk = false;
- foreach (var bound in bounds) {
- if (bound is ComprehensionExpr.IntBoundedPool) {
- var bnd = (ComprehensionExpr.IntBoundedPool)bound;
- if (bnd.LowerBound != null) {
- BigInteger? lower = GetConst(bnd.LowerBound);
- if (lower != null && nt.LowerBound <= lower) {
- lowerOk = true;
- }
- }
- if (bnd.UpperBound != null) {
- BigInteger? upper = GetConst(bnd.UpperBound);
- if (upper != null && upper <= nt.UpperBound) {
- upperOk = true;
- }
- }
- }
- }
- if (lowerOk && upperOk) {
- dd.NativeType = nt;
- break;
- }
- }
- if (dd.NativeType == null && (boolNativeType == true || stringNativeType != null)) {
- reporter.Error(MessageSource.Resolver, dd, "Dafny's heuristics cannot find a compatible native type. " +
- "Hint: try writing a newtype constraint of the form 'i:int | lowerBound <= i < upperBound && (...any additional constraints...)'");
- }
- if (dd.NativeType != null && stringNativeType == null) {
- reporter.Info(MessageSource.Resolver, dd.tok, "{:nativeType \"" + dd.NativeType.Name + "\"}");
- }
+ CheckExpression(dd.Constraint, this, dd);
}
+ FigureOutNativeType(dd, nativeTypeMap);
}
}
}
+ // ---------------------------------- Pass 2 ----------------------------------
+ // This pass fills in various additional information.
+ // ----------------------------------------------------------------------------
+
if (reporter.Count(ErrorLevel.Error) == prevErrorCount) {
// fill in the postconditions and bodies of prefix lemmas
foreach (var com in ModuleDefinition.AllFixpointLemmas(declarations)) {
@@ -1944,6 +1881,222 @@ namespace Microsoft.Dafny }
}
+ private void FigureOutNativeType(NewtypeDecl dd, Dictionary<string, NativeType> nativeTypeMap) {
+ Contract.Requires(dd != null);
+ Contract.Requires(nativeTypeMap != null);
+ bool? boolNativeType = null;
+ NativeType stringNativeType = null;
+ object nativeTypeAttr = true;
+ bool hasNativeTypeAttr = Attributes.ContainsMatchingValue(dd.Attributes, "nativeType", ref nativeTypeAttr,
+ new Attributes.MatchingValueOption[] {
+ Attributes.MatchingValueOption.Empty,
+ Attributes.MatchingValueOption.Bool,
+ Attributes.MatchingValueOption.String },
+ err => reporter.Error(MessageSource.Resolver, dd, err));
+ if (hasNativeTypeAttr) {
+ if (nativeTypeAttr is bool) {
+ boolNativeType = (bool)nativeTypeAttr;
+ } else {
+ string keyString = (string)nativeTypeAttr;
+ if (nativeTypeMap.ContainsKey(keyString)) {
+ stringNativeType = nativeTypeMap[keyString];
+ } else {
+ reporter.Error(MessageSource.Resolver, dd, "Unsupported nativeType {0}", keyString);
+ }
+ }
+ }
+ if (stringNativeType != null || boolNativeType == true) {
+ if (!dd.BaseType.IsNumericBased(Type.NumericPersuation.Int)) {
+ reporter.Error(MessageSource.Resolver, dd, "nativeType can only be used on integral types");
+ }
+ if (dd.Var == null) {
+ reporter.Error(MessageSource.Resolver, dd, "nativeType can only be used if newtype specifies a constraint");
+ }
+ }
+ if (dd.Var != null) {
+ Func<Expression, BigInteger?> GetConst = null;
+ GetConst = (Expression e) => {
+ int m = 1;
+ BinaryExpr bin = e as BinaryExpr;
+ if (bin != null && bin.Op == BinaryExpr.Opcode.Sub && GetConst(bin.E0) == BigInteger.Zero) {
+ m = -1;
+ e = bin.E1;
+ }
+ LiteralExpr l = e as LiteralExpr;
+ if (l != null && l.Value is BigInteger) {
+ return m * (BigInteger)l.Value;
+ }
+ return null;
+ };
+ var bounds = DiscoverAllBounds_SingleVar(dd.Var, dd.Constraint);
+ List<NativeType> potentialNativeTypes =
+ (stringNativeType != null) ? new List<NativeType> { stringNativeType } :
+ (boolNativeType == false) ? new List<NativeType>() :
+ NativeTypes;
+ foreach (var nt in potentialNativeTypes) {
+ bool lowerOk = false;
+ bool upperOk = false;
+ foreach (var bound in bounds) {
+ if (bound is ComprehensionExpr.IntBoundedPool) {
+ var bnd = (ComprehensionExpr.IntBoundedPool)bound;
+ if (bnd.LowerBound != null) {
+ BigInteger? lower = GetConst(bnd.LowerBound);
+ if (lower != null && nt.LowerBound <= lower) {
+ lowerOk = true;
+ }
+ }
+ if (bnd.UpperBound != null) {
+ BigInteger? upper = GetConst(bnd.UpperBound);
+ if (upper != null && upper <= nt.UpperBound) {
+ upperOk = true;
+ }
+ }
+ }
+ }
+ if (lowerOk && upperOk) {
+ dd.NativeType = nt;
+ break;
+ }
+ }
+ if (dd.NativeType == null && (boolNativeType == true || stringNativeType != null)) {
+ reporter.Error(MessageSource.Resolver, dd, "Dafny's heuristics cannot find a compatible native type. " +
+ "Hint: try writing a newtype constraint of the form 'i:int | lowerBound <= i < upperBound && (...any additional constraints...)'");
+ }
+ if (dd.NativeType != null && stringNativeType == null) {
+ reporter.Info(MessageSource.Resolver, dd.tok, "{:nativeType \"" + dd.NativeType.Name + "\"}");
+ }
+ }
+ }
+
+ /// <summary>
+ /// Adds the type constraint ty==expected, eventually printing the error message "msg" if this is found to be
+ /// untenable. If this is immediately known not to be untenable, false is returned.
+ /// </summary>
+ private bool ConstrainTypes(Type ty, Type expected, TopLevelDecl declForToken, string msg, params object[] args) {
+ Contract.Requires(ty != null);
+ Contract.Requires(expected != null);
+ Contract.Requires(declForToken != null);
+ Contract.Requires(msg != null);
+ Contract.Requires(args != null);
+ return ConstrainTypes(ty, expected, declForToken.tok, msg, args);
+ }
+ /// <summary>
+ /// Adds the type constraint ty==expected, eventually printing the error message "msg" if this is found to be
+ /// untenable. If this is immediately known not to be untenable, false is returned.
+ /// </summary>
+ private bool ConstrainTypes(Type ty, Type expected, MemberDecl declForToken, string msg, params object[] args) {
+ Contract.Requires(ty != null);
+ Contract.Requires(expected != null);
+ Contract.Requires(declForToken != null);
+ Contract.Requires(msg != null);
+ Contract.Requires(args != null);
+ return ConstrainTypes(ty, expected, declForToken.tok, msg, args);
+ }
+ /// <summary>
+ /// Adds the type constraint ty==expected, eventually printing the error message "msg" if this is found to be
+ /// untenable. If this is immediately known not to be untenable, false is returned.
+ /// </summary>
+ private bool ConstrainTypes(Type ty, Type expected, Statement stmtForToken, string msg, params object[] args) {
+ Contract.Requires(ty != null);
+ Contract.Requires(expected != null);
+ Contract.Requires(stmtForToken != null);
+ Contract.Requires(msg != null);
+ Contract.Requires(args != null);
+ return ConstrainTypes(ty, expected, stmtForToken.Tok, msg, args);
+ }
+ /// <summary>
+ /// Adds the type constraint ty==expected, eventually printing the error message "msg" if this is found to be
+ /// untenable. If this is immediately known not to be untenable, false is returned.
+ /// </summary>
+ private bool ConstrainTypes(Type ty, Type expected, Expression exprForToken, string msg, params object[] args) {
+ Contract.Requires(ty != null);
+ Contract.Requires(expected != null);
+ Contract.Requires(exprForToken != null);
+ Contract.Requires(msg != null);
+ Contract.Requires(args != null);
+ return ConstrainTypes(ty, expected, exprForToken.tok, msg, args);
+ }
+ /// <summary>
+ /// Adds the type constraint ty==expected, eventually printing the error message "msg" if this is found to be
+ /// untenable. If this is immediately known not to be untenable, false is returned.
+ /// </summary>
+ private bool ConstrainTypes(Type ty, Type expected, IToken tok, string msg, params object[] args) {
+ Contract.Requires(ty != null);
+ Contract.Requires(expected != null);
+ Contract.Requires(tok != null);
+ Contract.Requires(msg != null);
+ Contract.Requires(args != null);
+#if LAZY_TYPE_CHECKING
+ var c = new TypeConstraint(ty, expected, tok, msg, args);
+ AllTypeConstraints.Add(c);
+ return true;
+#else
+ if (!UnifyTypes(ty, expected)) {
+ reporter.Error(MessageSource.Resolver, tok, msg, args);
+ return false;
+ }
+ return true;
+#endif
+ }
+
+ public List<TypeConstraint> AllTypeConstraints = new List<TypeConstraint>();
+
+ /// <summary>
+ /// Solves or simplifies as many type constraints as possible
+ /// </summary>
+ void PartiallySolveTypeConstraints() {
+ var remainingConstraints = new List<TypeConstraint>();
+ foreach (var constraint in AllTypeConstraints) {
+ if (!constraint.CheckTenable(this)) {
+ remainingConstraints.Add(constraint);
+ }
+ }
+ AllTypeConstraints = remainingConstraints;
+ }
+
+ /// <summary>
+ /// Attempts to fully solve all type constraints. Upon success, returns "true".
+ /// Upon failure, reports errors and returns "false".
+ /// Clears all constraints.
+ /// </summary>
+ bool SolveAllTypeConstraints() {
+ PartiallySolveTypeConstraints();
+ foreach (var constraint in AllTypeConstraints) {
+ constraint.ReportAsError(reporter);
+ }
+ var success = AllTypeConstraints.Count == 0;
+ AllTypeConstraints.Clear();
+ return success;
+ }
+
+ public class TypeConstraint
+ {
+ readonly Type Ty;
+ readonly Type Expected;
+ readonly IToken Tok;
+ readonly string Msg;
+ readonly object[] MsgArgs;
+ public TypeConstraint(Type ty, Type expected, IToken tok, string msg, object[] msgArgs) {
+ Ty = ty;
+ Expected = expected;
+ Tok = tok;
+ Msg = msg;
+ MsgArgs = msgArgs;
+ }
+ /// <summary>
+ /// Returns "true" if constraint is tenable, "false" otherwise.
+ /// </summary>
+ /// <returns></returns>
+ public bool CheckTenable(Resolver resolver) {
+ Contract.Requires(resolver != null);
+ return resolver.UnifyTypes(Ty, Expected);
+ }
+ public void ReportAsError(ErrorReporter reporter) {
+ Contract.Requires(reporter != null);
+ reporter.Error(MessageSource.Resolver, Tok, Msg, MsgArgs);
+ }
+ }
+
// ------------------------------------------------------------------------------------------------------
// ----- Visitors ---------------------------------------------------------------------------------------
// ------------------------------------------------------------------------------------------------------
@@ -1973,49 +2126,22 @@ namespace Microsoft.Dafny private void CheckTypeInference_Member(MemberDecl member) {
if (member is Method) {
var m = (Method)member;
- m.Req.Iter(CheckTypeInference_MaybeFreeExpression);
- m.Ens.Iter(CheckTypeInference_MaybeFreeExpression);
- CheckTypeInference_Specification_FrameExpr(m.Mod);
- CheckTypeInference_Specification_Expr(m.Decreases);
+ m.Req.Iter(mfe => CheckTypeInference_MaybeFreeExpression(mfe, m));
+ m.Ens.Iter(mfe => CheckTypeInference_MaybeFreeExpression(mfe, m));
+ CheckTypeInference_Specification_FrameExpr(m.Mod, m);
+ CheckTypeInference_Specification_Expr(m.Decreases, m);
if (m.Body != null) {
- CheckTypeInference(m.Body);
- bool tail = true;
- bool hasTailRecursionPreference = Attributes.ContainsBool(m.Attributes, "tailrecursion", ref tail);
- if (hasTailRecursionPreference && !tail) {
- // the user specifically requested no tail recursion, so do nothing else
- } else if (hasTailRecursionPreference && tail && m.IsGhost) {
- reporter.Error(MessageSource.Resolver, m.tok, "tail recursion can be specified only for methods that will be compiled, not for ghost methods");
- } else {
- var module = m.EnclosingClass.Module;
- var sccSize = module.CallGraph.GetSCCSize(m);
- if (hasTailRecursionPreference && 2 <= sccSize) {
- reporter.Error(MessageSource.Resolver, m.tok, "sorry, tail-call optimizations are not supported for mutually recursive methods");
- } else if (hasTailRecursionPreference || sccSize == 1) {
- CallStmt tailCall = null;
- var status = CheckTailRecursive(m.Body.Body, m, ref tailCall, hasTailRecursionPreference);
- if (status != TailRecursionStatus.NotTailRecursive) {
- m.IsTailRecursive = true;
- if (tailCall != null) {
- // this means there was at least one recursive call
- reporter.Info(MessageSource.Resolver, m.tok, "tail recursive");
- }
- }
- }
- }
+ CheckTypeInference(m.Body, m);
}
} else if (member is Function) {
var f = (Function)member;
var errorCount = reporter.Count(ErrorLevel.Error);
- f.Req.Iter(CheckTypeInference);
- f.Ens.Iter(CheckTypeInference);
- f.Reads.Iter(fe => CheckTypeInference(fe.E));
- CheckTypeInference_Specification_Expr(f.Decreases);
+ f.Req.Iter(e => CheckTypeInference(e, f));
+ f.Ens.Iter(e => CheckTypeInference(e, f));
+ f.Reads.Iter(fe => CheckTypeInference(fe.E, f));
+ CheckTypeInference_Specification_Expr(f.Decreases, f);
if (f.Body != null) {
- CheckTypeInference(f.Body);
- bool tail = true;
- if (Attributes.ContainsBool(f.Attributes, "tailrecursion", ref tail) && tail) {
- reporter.Error(MessageSource.Resolver, f.tok, "sorry, tail-call functions are not supported");
- }
+ CheckTypeInference(f.Body, f);
}
if (errorCount == reporter.Count(ErrorLevel.Error) && f is FixpointPredicate) {
var cop = (FixpointPredicate)f;
@@ -2023,42 +2149,52 @@ namespace Microsoft.Dafny }
}
}
- private void CheckTypeInference_MaybeFreeExpression(MaybeFreeExpression mfe) {
+
+ private void CheckTypeInference_MaybeFreeExpression(MaybeFreeExpression mfe, ICodeContext codeContext) {
Contract.Requires(mfe != null);
+ Contract.Requires(codeContext != null);
foreach (var e in Attributes.SubExpressions(mfe.Attributes)) {
- CheckTypeInference(e);
+ CheckTypeInference(e, codeContext);
}
- CheckTypeInference(mfe.E);
+ CheckTypeInference(mfe.E, codeContext);
}
- private void CheckTypeInference_Specification_Expr(Specification<Expression> spec) {
+ private void CheckTypeInference_Specification_Expr(Specification<Expression> spec, ICodeContext codeContext) {
Contract.Requires(spec != null);
+ Contract.Requires(codeContext != null);
foreach (var e in Attributes.SubExpressions(spec.Attributes)) {
- CheckTypeInference(e);
+ CheckTypeInference(e, codeContext);
}
- spec.Expressions.Iter(CheckTypeInference);
+ spec.Expressions.Iter(e => CheckTypeInference(e, codeContext));
}
- private void CheckTypeInference_Specification_FrameExpr(Specification<FrameExpression> spec) {
+ private void CheckTypeInference_Specification_FrameExpr(Specification<FrameExpression> spec, ICodeContext codeContext) {
Contract.Requires(spec != null);
+ Contract.Requires(codeContext != null);
foreach (var e in Attributes.SubExpressions(spec.Attributes)) {
- CheckTypeInference(e);
+ CheckTypeInference(e, codeContext);
}
- spec.Expressions.Iter(fe => CheckTypeInference(fe.E));
+ spec.Expressions.Iter(fe => CheckTypeInference(fe.E, codeContext));
}
- void CheckTypeInference(Expression expr) {
+ void CheckTypeInference(Expression expr, ICodeContext codeContext) {
Contract.Requires(expr != null);
- var c = new CheckTypeInference_Visitor(this);
+ Contract.Requires(codeContext != null);
+ PartiallySolveTypeConstraints();
+ var c = new CheckTypeInference_Visitor(this, codeContext);
c.Visit(expr);
}
- void CheckTypeInference(Statement stmt) {
+ void CheckTypeInference(Statement stmt, ICodeContext codeContext) {
Contract.Requires(stmt != null);
- var c = new CheckTypeInference_Visitor(this);
+ Contract.Requires(codeContext != null);
+ var c = new CheckTypeInference_Visitor(this, codeContext);
c.Visit(stmt);
}
class CheckTypeInference_Visitor : ResolverBottomUpVisitor
{
- public CheckTypeInference_Visitor(Resolver resolver)
+ readonly ICodeContext codeContext;
+ public CheckTypeInference_Visitor(Resolver resolver, ICodeContext codeContext)
: base(resolver) {
Contract.Requires(resolver != null);
+ Contract.Requires(codeContext != null);
+ this.codeContext = codeContext;
}
protected override void VisitOneStmt(Statement stmt) {
if (stmt is VarDeclStmt) {
@@ -2069,19 +2205,94 @@ namespace Microsoft.Dafny } else if (stmt is ForallStmt) {
var s = (ForallStmt)stmt;
s.BoundVars.Iter(bv => CheckTypeIsDetermined(bv.tok, bv.Type, "bound variable"));
+ List<BoundVar> missingBounds;
+ s.Bounds = DiscoverBestBounds_MultipleVars(s.BoundVars, s.Range, true, true, out missingBounds);
+
+ } else if (stmt is AssignSuchThatStmt) {
+ var s = (AssignSuchThatStmt)stmt;
+ if (s.AssumeToken == null) {
+ var varLhss = new List<IVariable>();
+ foreach (var lhs in s.Lhss) {
+ var ide = (IdentifierExpr)lhs.Resolved; // successful resolution implies all LHS's are IdentifierExpr's
+ varLhss.Add(ide.Var);
+ }
+ List<IVariable> missingBounds;
+ var bestBounds = DiscoverBestBounds_MultipleVars(varLhss, s.Expr, true, false, out missingBounds);
+ if (missingBounds.Count != 0) {
+ s.MissingBounds = missingBounds; // so that an error message can be produced during compilation
+ } else {
+ Contract.Assert(bestBounds != null);
+ s.Bounds = bestBounds;
+ }
+ }
+ } else if (stmt is CalcStmt) {
+ var s = (CalcStmt)stmt;
+ // The resolution of the calc statement builds up .Steps and .Result, which are of the form E0 OP E1, where
+ // E0 and E1 are expressions from .Lines. These additional expressions still need to have their .ResolvedOp
+ // fields filled in, so we visit them (but not their subexpressions) here.
+ foreach (var e in s.Steps) {
+ VisitOneExpr(e);
+ }
+ VisitOneExpr(s.Result);
}
}
protected override void VisitOneExpr(Expression expr) {
if (expr is ComprehensionExpr) {
var e = (ComprehensionExpr)expr;
- if (e != null) {
- foreach (var bv in e.BoundVars) {
- if (!IsDetermined(bv.Type.Normalize())) {
- resolver.reporter.Error(MessageSource.Resolver, bv.tok, "type of bound variable '{0}' could not be determined; please specify the type explicitly",
- bv.Name);
+ foreach (var bv in e.BoundVars) {
+ if (!IsDetermined(bv.Type.Normalize())) {
+ resolver.reporter.Error(MessageSource.Resolver, bv.tok, "type of bound variable '{0}' could not be determined; please specify the type explicitly", bv.Name);
+ }
+ }
+ // apply bounds discovery to quantifiers, finite sets, and finite maps
+ string what = null;
+ Expression whereToLookForBounds = null;
+ bool polarity = true;
+ if (e is QuantifierExpr) {
+ what = "quantifier";
+ whereToLookForBounds = ((QuantifierExpr)e).LogicalBody();
+ polarity = e is ExistsExpr;
+ } else if (e is SetComprehension && ((SetComprehension)e).Finite) {
+ what = "set comprehension";
+ whereToLookForBounds = e.Range;
+ } else if (e is MapComprehension && ((MapComprehension)e).Finite) {
+ what = "map comprehension";
+ whereToLookForBounds = e.Range;
+ }
+ if (whereToLookForBounds != null) {
+ List<BoundVar> missingBounds;
+ e.Bounds = DiscoverBestBounds_MultipleVars(e.BoundVars, whereToLookForBounds, polarity, true, out missingBounds);
+ if (missingBounds.Count != 0) {
+ e.MissingBounds = missingBounds;
+
+ if ((e is SetComprehension && !((SetComprehension)e).Finite) || (e is MapComprehension && !((MapComprehension)e).Finite)) {
+ // a possibly infinite set/map has no restrictions on its range
+ } else if (e is QuantifierExpr) {
+ // don't report any errors at this time (instead, wait to see if the quantifier is used in a non-ghost context)
+ } else if (e is SetComprehension && e.Type.HasFinitePossibleValues) {
+ // This means the set is finite, regardless of if the Range is bounded. So, we don't give any error here.
+ // However, if this expression is used in a non-ghost context (which is not yet known at this stage of
+ // resolution), the resolver will generate an error about that later.
+ } else {
+ // we cannot be sure that the set/map really is finite
+ foreach (var bv in missingBounds) {
+ resolver.reporter.Error(MessageSource.Resolver, e, "a {0} must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{1}'", what, bv.Name);
+ }
+ }
+ }
+ if (codeContext is Function && e.Bounds != null) {
+ // functions are not allowed to depend on the set of allocated objects
+ Contract.Assert(e.Bounds.Count == e.BoundVars.Count);
+ for (int i = 0; i < e.Bounds.Count; i++) {
+ var bound = e.Bounds[i] as ComprehensionExpr.RefBoundedPool;
+ if (bound != null) {
+ var bv = e.BoundVars[i];
+ resolver.reporter.Error(MessageSource.Resolver, expr, "a {0} involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of '{1}'", what, bv.Name);
+ }
}
}
}
+
} else if (expr is MemberSelectExpr) {
var e = (MemberSelectExpr)expr;
if (e.Member is Function || e.Member is Method) {
@@ -2118,6 +2329,7 @@ namespace Microsoft.Dafny var bin = expr as BinaryExpr;
if (bin != null) {
bin.ResolvedOp = ResolveOp(bin.Op, bin.E1.Type);
+
}
}
}
@@ -2196,6 +2408,58 @@ namespace Microsoft.Dafny #endregion CheckTypeInference
// ------------------------------------------------------------------------------------------------------
+ // ----- CheckExpression --------------------------------------------------------------------------------
+ // ------------------------------------------------------------------------------------------------------
+ #region CheckExpression
+ /// <summary>
+ /// This method computes ghost interests in the statement portion of StmtExpr's and
+ /// checks for hint restrictions in any CalcStmt.
+ /// </summary>
+ void CheckExpression(Expression expr, Resolver resolver, ICodeContext codeContext) {
+ Contract.Requires(expr != null);
+ Contract.Requires(resolver != null);
+ Contract.Requires(codeContext != null);
+ var v = new CheckExpression_Visitor(resolver, codeContext);
+ v.Visit(expr);
+ }
+ /// <summary>
+ /// This method computes ghost interests in the statement portion of StmtExpr's and
+ /// checks for hint restrictions in any CalcStmt.
+ /// </summary>
+ void CheckExpression(Statement stmt, Resolver resolver, ICodeContext codeContext) {
+ Contract.Requires(stmt != null);
+ Contract.Requires(resolver != null);
+ Contract.Requires(codeContext != null);
+ var v = new CheckExpression_Visitor(resolver, codeContext);
+ v.Visit(stmt);
+ }
+ class CheckExpression_Visitor : ResolverBottomUpVisitor
+ {
+ readonly ICodeContext CodeContext;
+ public CheckExpression_Visitor(Resolver resolver, ICodeContext codeContext)
+ : base(resolver) {
+ Contract.Requires(resolver != null);
+ Contract.Requires(codeContext != null);
+ CodeContext = codeContext;
+ }
+ protected override void VisitOneExpr(Expression expr) {
+ if (expr is StmtExpr) {
+ var e = (StmtExpr)expr;
+ resolver.ComputeGhostInterest(e.S, true, CodeContext);
+ }
+ }
+ protected override void VisitOneStmt(Statement stmt) {
+ if (stmt is CalcStmt) {
+ var s = (CalcStmt)stmt;
+ foreach (var h in s.Hints) {
+ resolver.CheckHintRestrictions(h, new HashSet<LocalVariable>());
+ }
+ }
+ }
+ }
+ #endregion
+
+ // ------------------------------------------------------------------------------------------------------
// ----- CheckTailRecursive -----------------------------------------------------------------------------
// ------------------------------------------------------------------------------------------------------
#region CheckTailRecursive
@@ -2244,6 +2508,41 @@ namespace Microsoft.Dafny return status;
}
+ void DetermineTailRecursion(Function f) {
+ Contract.Requires(f != null);
+ bool tail = true;
+ if (Attributes.ContainsBool(f.Attributes, "tailrecursion", ref tail) && tail) {
+ reporter.Error(MessageSource.Resolver, f.tok, "sorry, tail-call functions are not supported");
+ }
+ }
+
+ void DetermineTailRecursion(Method m) {
+ Contract.Requires(m != null);
+ bool tail = true;
+ bool hasTailRecursionPreference = Attributes.ContainsBool(m.Attributes, "tailrecursion", ref tail);
+ if (hasTailRecursionPreference && !tail) {
+ // the user specifically requested no tail recursion, so do nothing else
+ } else if (hasTailRecursionPreference && tail && m.IsGhost) {
+ reporter.Error(MessageSource.Resolver, m.tok, "tail recursion can be specified only for methods that will be compiled, not for ghost methods");
+ } else {
+ var module = m.EnclosingClass.Module;
+ var sccSize = module.CallGraph.GetSCCSize(m);
+ if (hasTailRecursionPreference && 2 <= sccSize) {
+ reporter.Error(MessageSource.Resolver, m.tok, "sorry, tail-call optimizations are not supported for mutually recursive methods");
+ } else if (hasTailRecursionPreference || sccSize == 1) {
+ CallStmt tailCall = null;
+ var status = CheckTailRecursive(m.Body.Body, m, ref tailCall, hasTailRecursionPreference);
+ if (status != TailRecursionStatus.NotTailRecursive) {
+ m.IsTailRecursive = true;
+ if (tailCall != null) {
+ // this means there was at least one recursive call
+ reporter.Info(MessageSource.Resolver, m.tok, "tail recursive");
+ }
+ }
+ }
+ }
+ }
+
/// <summary>
/// See CheckTailRecursive(List Statement, ...), including its description of "tailCall".
/// In the current implementation, "enclosingMethod" is not allowed to be a mutually recursive method.
@@ -2917,6 +3216,312 @@ namespace Microsoft.Dafny #endregion CheckEqualityTypes
// ------------------------------------------------------------------------------------------------------
+ // ----- ComputeGhostInterest ---------------------------------------------------------------------------
+ // ------------------------------------------------------------------------------------------------------
+ #region ComputeGhostInterest
+ public void ComputeGhostInterest(Statement stmt, bool mustBeErasable, ICodeContext codeContext) {
+ Contract.Requires(stmt != null);
+ Contract.Requires(codeContext != null);
+ var visitor = new GhostInterest_Visitor(codeContext, this);
+ visitor.Visit(stmt, mustBeErasable);
+ }
+ 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, in order:
+ /// 0. Sets .IsGhost to "true" if the statement is ghost. This often depends on some guard of the statement
+ /// (like the guard of an "if" statement) or the LHS of the statement (if it is an assignment).
+ /// Note, if "mustBeErasable", then the statement is already in a ghost context.
+ /// statement itself is ghost) or and the statement assigns to a non-ghost field
+ /// 1. Determines if the statement and all its subparts are legal under its computed .IsGhost setting.
+ /// 2. ``Upgrades'' .IsGhost to "true" if, after investigation of the substatements of the statement, it
+ /// turns out that the statement can be erased during compilation.
+ /// Notes:
+ /// * Both step (0) and step (2) sets the .IsGhost field. What step (0) does affects only the
+ /// rules of resolution, whereas step (2) makes a note for the later compilation phase.
+ /// * It is important to do step (0) before step (1)--that is, 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.
+ /// * 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".
+ /// </summary>
+ public void Visit(Statement stmt, bool mustBeErasable) {
+ Contract.Requires(stmt != null);
+ Contract.Assume(!codeContext.IsGhost || mustBeErasable); // (this is really a precondition) codeContext.IsGhost ==> mustBeErasable
+
+ if (stmt is PredicateStmt) {
+ stmt.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.CheckIsCompilable);
+ }
+
+ } else if (stmt is BreakStmt) {
+ var s = (BreakStmt)stmt;
+ s.IsGhost = mustBeErasable;
+ if (s.IsGhost && !s.TargetStmt.IsGhost) {
+ 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.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.IsGhost = s.ResolvedStatements.All(ss => ss.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;
+ }
+ }
+ s.IsGhost = (s.Update == null || s.Update.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.IsGhost = true;
+ if (s.Rhs is TypeRhs) {
+ Error(s.Rhs.Tok, "'new' is not allowed in ghost contexts");
+ }
+ } 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.CheckIsCompilable(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.CheckIsCompilable(dim);
+ }
+ }
+ if (rhs.InitCall != null) {
+ foreach (var arg in rhs.InitCall.Args) {
+ resolver.CheckIsCompilable(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.IsGhost = callee.IsGhost;
+ // check in-parameters
+ if (mustBeErasable) {
+ if (!s.IsGhost) {
+ Error(s, "only ghost methods can be called from this context");
+ }
+ } else {
+ resolver.CheckIsCompilable(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.CheckIsCompilable(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.IsGhost = mustBeErasable; // set .IsGhost before descending into substatements (since substatements may do a 'break' out of this block)
+ s.Body.Iter(ss => Visit(ss, mustBeErasable));
+ s.IsGhost = s.IsGhost || s.Body.All(ss => ss.IsGhost); // mark the block statement as ghost if all its substatements are ghost
+
+ } else if (stmt is IfStmt) {
+ var s = (IfStmt)stmt;
+ s.IsGhost = mustBeErasable || (s.Guard != null && resolver.UsesSpecFeatures(s.Guard));
+ Visit(s.Thn, s.IsGhost);
+ if (s.Els != null) {
+ Visit(s.Els, s.IsGhost);
+ }
+ // if both branches were all ghost, then we can mark the enclosing statement as ghost as well
+ s.IsGhost = s.IsGhost || (s.Thn.IsGhost && (s.Els == null || s.Els.IsGhost));
+
+ } else if (stmt is AlternativeStmt) {
+ var s = (AlternativeStmt)stmt;
+ s.IsGhost = mustBeErasable || s.Alternatives.Exists(alt => resolver.UsesSpecFeatures(alt.Guard));
+ s.Alternatives.Iter(alt => alt.Body.Iter(ss => Visit(ss, s.IsGhost)));
+ s.IsGhost = s.IsGhost || s.Alternatives.All(alt => alt.Body.All(ss => ss.IsGhost));
+
+ } else if (stmt is WhileStmt) {
+ var s = (WhileStmt)stmt;
+ s.IsGhost = mustBeErasable || (s.Guard != null && resolver.UsesSpecFeatures(s.Guard));
+ if (s.IsGhost && s.Decreases.Expressions.Exists(e => e is WildcardExpr)) {
+ Error(s, "'decreases *' is not allowed on ghost loops");
+ }
+ if (s.IsGhost && s.Mod.Expressions != null) {
+ s.Mod.Expressions.Iter(resolver.DisallowNonGhostFieldSpecifiers);
+ }
+ if (s.Body != null) {
+ Visit(s.Body, s.IsGhost);
+ }
+ s.IsGhost = s.IsGhost || s.Body == null || (!s.Decreases.Expressions.Exists(e => e is WildcardExpr) && s.Body.IsGhost);
+
+ } else if (stmt is AlternativeLoopStmt) {
+ var s = (AlternativeLoopStmt)stmt;
+ s.IsGhost = mustBeErasable || s.Alternatives.Exists(alt => resolver.UsesSpecFeatures(alt.Guard));
+ if (s.IsGhost && s.Decreases.Expressions.Exists(e => e is WildcardExpr)) {
+ Error(s, "'decreases *' is not allowed on ghost loops");
+ }
+ if (s.IsGhost && s.Mod.Expressions != null) {
+ s.Mod.Expressions.Iter(resolver.DisallowNonGhostFieldSpecifiers);
+ }
+ s.Alternatives.Iter(alt => alt.Body.Iter(ss => Visit(ss, s.IsGhost)));
+ s.IsGhost = s.IsGhost || (!s.Decreases.Expressions.Exists(e => e is WildcardExpr) && s.Alternatives.All(alt => alt.Body.All(ss => ss.IsGhost)));
+
+ } else if (stmt is ForallStmt) {
+ var s = (ForallStmt)stmt;
+ s.IsGhost = mustBeErasable || s.Kind != ForallStmt.ParBodyKind.Assign || resolver.UsesSpecFeatures(s.Range);
+ if (s.Body != null) {
+ Visit(s.Body, s.IsGhost);
+ }
+ s.IsGhost = s.IsGhost || s.Body == null || s.Body.IsGhost;
+
+ } else if (stmt is ModifyStmt) {
+ var s = (ModifyStmt)stmt;
+ s.IsGhost = mustBeErasable;
+ if (s.IsGhost) {
+ s.Mod.Expressions.Iter(resolver.DisallowNonGhostFieldSpecifiers);
+ }
+ if (s.Body != null) {
+ Visit(s.Body, mustBeErasable);
+ }
+
+ } else if (stmt is CalcStmt) {
+ var s = (CalcStmt)stmt;
+ s.IsGhost = true;
+ foreach (var h in s.Hints) {
+ Visit(h, true);
+ }
+
+ } else if (stmt is MatchStmt) {
+ var s = (MatchStmt)stmt;
+ s.IsGhost = mustBeErasable || resolver.UsesSpecFeatures(s.Source);
+ s.Cases.Iter(kase => kase.Body.Iter(ss => Visit(ss, s.IsGhost)));
+ s.IsGhost = s.IsGhost || s.Cases.All(kase => kase.Body.All(ss => ss.IsGhost));
+
+ } else if (stmt is SkeletonStatement) {
+ var s = (SkeletonStatement)stmt;
+ s.IsGhost = mustBeErasable;
+ if (s.S != null) {
+ Visit(s.S, mustBeErasable);
+ s.IsGhost = s.IsGhost || s.S.IsGhost;
+ }
+
+ } else {
+ Contract.Assert(false); throw new cce.UnreachableException();
+ }
+ }
+ }
+ #endregion
+
+ // ------------------------------------------------------------------------------------------------------
// ----- FillInDefaultLoopDecreases ---------------------------------------------------------------------
// ------------------------------------------------------------------------------------------------------
#region FillInDefaultLoopDecreases
@@ -3030,7 +3635,6 @@ namespace Microsoft.Dafny readonly Scope<IVariable>/*!*/ scope = new Scope<IVariable>();
Scope<Statement>/*!*/ labeledStatements = new Scope<Statement>();
List<Statement> loopStack = new List<Statement>(); // the enclosing loops (from which it is possible to break out)
- readonly Dictionary<Statement, bool> inSpecOnlyContext = new Dictionary<Statement, bool>(); // invariant: domain contain union of the domains of "labeledStatements" and "loopStack"
/// <summary>
/// This method resolves the types that have been given after the 'extends' keyword. Then, it populates
@@ -3541,26 +4145,17 @@ namespace Microsoft.Dafny void ResolveAttributes(Attributes attrs, ResolveOpts opts) {
Contract.Requires(opts != null);
- Contract.Requires(opts.DontCareAboutCompilation); // attributes are never compiled
// 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, opts.codeContext);
+ }
+ }
}
}
}
@@ -3643,39 +4238,32 @@ namespace Microsoft.Dafny foreach (Formal p in f.Formals) {
scope.Push(p.Name, p);
}
- ResolveAttributes(f.Attributes, new ResolveOpts(f, false, true));
+ ResolveAttributes(f.Attributes, new ResolveOpts(f, false));
foreach (Expression r in f.Req) {
- ResolveExpression(r, new ResolveOpts(f, false, true));
+ ResolveExpression(r, new ResolveOpts(f, false));
Contract.Assert(r.Type != null); // follows from postcondition of ResolveExpression
- if (!UnifyTypes(r.Type, Type.Bool)) {
- reporter.Error(MessageSource.Resolver, r, "Precondition must be a boolean (got {0})", r.Type);
- }
+ ConstrainTypes(r.Type, Type.Bool, r, "Precondition must be a boolean (got {0})", r.Type);
}
foreach (FrameExpression fr in f.Reads) {
- ResolveFrameExpression(fr, true, f.IsGhost, f);
+ ResolveFrameExpression(fr, true, f);
}
foreach (Expression r in f.Ens) {
- ResolveExpression(r, new ResolveOpts(f, false, true)); // since this is a function, the postcondition is still a one-state predicate
+ ResolveExpression(r, new ResolveOpts(f, false)); // since this is a function, the postcondition is still a one-state predicate
Contract.Assert(r.Type != null); // follows from postcondition of ResolveExpression
- if (!UnifyTypes(r.Type, Type.Bool)) {
- reporter.Error(MessageSource.Resolver, r, "Postcondition must be a boolean (got {0})", r.Type);
- }
+ ConstrainTypes(r.Type, Type.Bool, r, "Postcondition must be a boolean (got {0})", r.Type);
}
- ResolveAttributes(f.Decreases.Attributes, new ResolveOpts(f, false, true));
+ ResolveAttributes(f.Decreases.Attributes, new ResolveOpts(f, false));
foreach (Expression r in f.Decreases.Expressions) {
- ResolveExpression(r, new ResolveOpts(f, false, true));
+ ResolveExpression(r, new ResolveOpts(f, false));
// any type is fine
}
+ SolveAllTypeConstraints();
if (f.Body != null) {
var prevErrorCount = reporter.Count(ErrorLevel.Error);
ResolveExpression(f.Body, new ResolveOpts(f, false));
- if (!f.IsGhost && prevErrorCount == reporter.Count(ErrorLevel.Error)) {
- CheckIsNonGhost(f.Body);
- }
+ SolveAllTypeConstraints();
Contract.Assert(f.Body.Type != null); // follows from postcondition of ResolveExpression
- if (!UnifyTypes(f.Body.Type, f.ResultType)) {
- reporter.Error(MessageSource.Resolver, f, "Function body type mismatch (expected {0}, got {1})", f.ResultType, f.Body.Type);
- }
+ ConstrainTypes(f.Body.Type, f.ResultType, f, "Function body type mismatch (expected {0}, got {1})", f.ResultType, f.Body.Type);
}
scope.PopMarker();
}
@@ -3683,14 +4271,11 @@ namespace Microsoft.Dafny /// <summary>
///
/// </summary>
- /// <param name="fe"></param>
/// <param name="readsFrame">True indicates "reads", false indicates "modifies".</param>
- /// <param name="isGhostContext"></param>
- /// <param name="codeContext"></param>
- void ResolveFrameExpression(FrameExpression fe, bool readsFrame, bool isGhostContext, ICodeContext codeContext) {
+ void ResolveFrameExpression(FrameExpression fe, bool readsFrame, ICodeContext codeContext) {
Contract.Requires(fe != null);
Contract.Requires(codeContext != null);
- ResolveExpression(fe.E, new ResolveOpts(codeContext, false, true /* yes, this is ghost */));
+ ResolveExpression(fe.E, new ResolveOpts(codeContext, false));
Type t = fe.E.Type;
Contract.Assert(t != null); // follows from postcondition of ResolveExpression
var arrTy = t.AsArrowType;
@@ -3701,8 +4286,7 @@ namespace Microsoft.Dafny if (collType != null) {
t = collType.Arg;
}
- if (!UnifyTypes(t, new ObjectType())) {
- reporter.Error(MessageSource.Resolver, fe.E, "a {0}-clause expression must denote an object or a collection of objects (instead got {1})", readsFrame ? "reads" : "modifies", fe.E.Type);
+ if (!ConstrainTypes(t, new ObjectType(), fe.E, "a {0}-clause expression must denote an object or a collection of objects (instead got {1})", readsFrame ? "reads" : "modifies", fe.E.Type)) {
} else if (fe.FieldName != null) {
NonProxyType nptype;
MemberDecl member = ResolveMember(fe.E.tok, t, fe.FieldName, out nptype);
@@ -3711,8 +4295,6 @@ namespace Microsoft.Dafny // error has already been reported by ResolveMember
} else if (!(member is Field)) {
reporter.Error(MessageSource.Resolver, fe.E, "member {0} in type {1} does not refer to a field", fe.FieldName, ctype.Name);
- } else if (!readsFrame && isGhostContext && !member.IsGhost) {
- reporter.Error(MessageSource.Resolver, fe.E, "in a ghost context, only ghost fields can be mentioned as modifies frame targets ({0})", fe.FieldName);
} else {
Contract.Assert(ctype != null && ctype.ResolvedClass != null); // follows from postcondition of ResolveMember
fe.Field = (Field)member;
@@ -3721,6 +4303,17 @@ namespace Microsoft.Dafny }
/// <summary>
+ /// This method can be called even if the resolution of "fe" failed; in that case, this method will
+ /// not issue any error message.
+ /// </summary>
+ void DisallowNonGhostFieldSpecifiers(FrameExpression fe) {
+ Contract.Requires(fe != null);
+ if (fe.Field != null && !fe.Field.IsGhost) {
+ reporter.Error(MessageSource.Resolver, fe.E, "in a ghost context, only ghost fields can be mentioned as modifies frame targets ({0})", fe.FieldName);
+ }
+ }
+
+ /// <summary>
/// Assumes type parameters have already been pushed
/// </summary>
void ResolveMethodSignature(Method m) {
@@ -3764,27 +4357,24 @@ namespace Microsoft.Dafny // Start resolving specification...
foreach (MaybeFreeExpression e in m.Req) {
- ResolveAttributes(e.Attributes, new ResolveOpts(m, false, true));
- ResolveExpression(e.E, new ResolveOpts(m, false, true));
+ ResolveAttributes(e.Attributes, new ResolveOpts(m, false));
+ ResolveExpression(e.E, new ResolveOpts(m, false));
Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression
- if (!UnifyTypes(e.E.Type, Type.Bool)) {
- reporter.Error(MessageSource.Resolver, e.E, "Precondition must be a boolean (got {0})", e.E.Type);
- }
+ ConstrainTypes(e.E.Type, Type.Bool, e.E, "Precondition must be a boolean (got {0})", e.E.Type);
}
- ResolveAttributes(m.Mod.Attributes, new ResolveOpts(m, false, true));
+ ResolveAttributes(m.Mod.Attributes, new ResolveOpts(m, false));
foreach (FrameExpression fe in m.Mod.Expressions) {
- ResolveFrameExpression(fe, false, m.IsGhost, m);
+ ResolveFrameExpression(fe, false, m);
if (m is Lemma || m is FixpointLemma) {
reporter.Error(MessageSource.Resolver, fe.tok, "{0}s are not allowed to have modifies clauses", m.WhatKind);
+ } else if (m.IsGhost) {
+ DisallowNonGhostFieldSpecifiers(fe);
}
}
- ResolveAttributes(m.Decreases.Attributes, new ResolveOpts(m, false, true));
+ ResolveAttributes(m.Decreases.Attributes, new ResolveOpts(m, false));
foreach (Expression e in m.Decreases.Expressions) {
- ResolveExpression(e, new ResolveOpts(m, false, true));
+ ResolveExpression(e, new ResolveOpts(m, false));
// any type is fine
- if (m.IsGhost && e is WildcardExpr) {
- reporter.Error(MessageSource.Resolver, e, "'decreases *' is not allowed on ghost methods");
- }
}
// Add out-parameters to a new scope that will also include the outermost-level locals of the body
@@ -3800,13 +4390,12 @@ namespace Microsoft.Dafny // ... continue resolving specification
foreach (MaybeFreeExpression e in m.Ens) {
- ResolveAttributes(e.Attributes, new ResolveOpts(m, true, true));
- ResolveExpression(e.E, new ResolveOpts(m, true, true));
+ ResolveAttributes(e.Attributes, new ResolveOpts(m, true));
+ ResolveExpression(e.E, new ResolveOpts(m, true));
Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression
- if (!UnifyTypes(e.E.Type, Type.Bool)) {
- reporter.Error(MessageSource.Resolver, e.E, "Postcondition must be a boolean (got {0})", e.E.Type);
- }
+ 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) {
@@ -3817,12 +4406,16 @@ 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);
+ SolveAllTypeConstraints();
+ if (reporter.Count(ErrorLevel.Error) == prevErrorCount) {
+//KRML ComputeGhostInterest(m.Body, m);
+ }
}
// attributes are allowed to mention both in- and out-parameters (including the implicit _k, for colemmas)
- ResolveAttributes(m.Attributes, new ResolveOpts(m, false, true));
+ ResolveAttributes(m.Attributes, new ResolveOpts(m, false));
scope.PopMarker(); // for the out-parameters and outermost-level locals
scope.PopMarker(); // for the in-parameters
@@ -3888,26 +4481,22 @@ namespace Microsoft.Dafny Contract.Assert(iter.Decreases.Expressions.Count == iter.DecreasesFields.Count);
for (int i = 0; i < iter.Decreases.Expressions.Count; i++) {
var e = iter.Decreases.Expressions[i];
- ResolveExpression(e, new ResolveOpts(iter, false, true));
+ ResolveExpression(e, new ResolveOpts(iter, false));
// any type is fine, but associate this type with the corresponding _decreases<n> field
var d = iter.DecreasesFields[i];
- if (!UnifyTypes(d.Type, e.Type)) {
- // bummer, there was a use--and a bad use--of the field before, so this won't be the best of error messages
- reporter.Error(MessageSource.Resolver, e, "type of field {0} is {1}, but has been constrained elsewhere to be of type {2}", d.Name, e.Type, d.Type);
- }
+ // If the following type constraint does not hold, then: Bummer, there was a use--and a bad use--of the field before, so this won't be the best of error messages
+ ConstrainTypes(d.Type, e.Type, e, "type of field {0} is {1}, but has been constrained elsewhere to be of type {2}", d.Name, e.Type, d.Type);
}
foreach (FrameExpression fe in iter.Reads.Expressions) {
- ResolveFrameExpression(fe, true, false, iter);
+ ResolveFrameExpression(fe, true, iter);
}
foreach (FrameExpression fe in iter.Modifies.Expressions) {
- ResolveFrameExpression(fe, false, false, iter);
+ ResolveFrameExpression(fe, false, iter);
}
foreach (MaybeFreeExpression e in iter.Requires) {
- ResolveExpression(e.E, new ResolveOpts(iter, false, true));
+ ResolveExpression(e.E, new ResolveOpts(iter, false));
Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression
- if (!UnifyTypes(e.E.Type, Type.Bool)) {
- reporter.Error(MessageSource.Resolver, e.E, "Precondition must be a boolean (got {0})", e.E.Type);
- }
+ ConstrainTypes(e.E.Type, Type.Bool, e.E, "Precondition must be a boolean (got {0})", e.E.Type);
}
scope.PopMarker(); // for the in-parameters
@@ -3919,34 +4508,31 @@ namespace Microsoft.Dafny Contract.Assert(scope.AllowInstance);
foreach (MaybeFreeExpression e in iter.YieldRequires) {
- ResolveExpression(e.E, new ResolveOpts(iter, false, true));
+ ResolveExpression(e.E, new ResolveOpts(iter, false));
Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression
- if (!UnifyTypes(e.E.Type, Type.Bool)) {
- reporter.Error(MessageSource.Resolver, e.E, "Yield precondition must be a boolean (got {0})", e.E.Type);
- }
+ ConstrainTypes(e.E.Type, Type.Bool, e.E, "Yield precondition must be a boolean (got {0})", e.E.Type);
}
foreach (MaybeFreeExpression e in iter.YieldEnsures) {
- ResolveExpression(e.E, new ResolveOpts(iter, true, true));
+ ResolveExpression(e.E, new ResolveOpts(iter, true));
Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression
- if (!UnifyTypes(e.E.Type, Type.Bool)) {
- reporter.Error(MessageSource.Resolver, e.E, "Yield postcondition must be a boolean (got {0})", e.E.Type);
- }
+ ConstrainTypes(e.E.Type, Type.Bool, e.E, "Yield postcondition must be a boolean (got {0})", e.E.Type);
}
foreach (MaybeFreeExpression e in iter.Ensures) {
- ResolveExpression(e.E, new ResolveOpts(iter, true, true));
+ ResolveExpression(e.E, new ResolveOpts(iter, true));
Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression
- if (!UnifyTypes(e.E.Type, Type.Bool)) {
- reporter.Error(MessageSource.Resolver, e.E, "Postcondition must be a boolean (got {0})", e.E.Type);
- }
+ ConstrainTypes(e.E.Type, Type.Bool, e.E, "Postcondition must be a boolean (got {0})", e.E.Type);
}
- ResolveAttributes(iter.Attributes, new ResolveOpts(iter, false, true));
+ ResolveAttributes(iter.Attributes, new ResolveOpts(iter, false));
var postSpecErrorCount = reporter.Count(ErrorLevel.Error);
// Resolve body
if (iter.Body != null) {
- ResolveBlockStatement(iter.Body, false, iter);
+ ResolveBlockStatement(iter.Body, iter);
+ if (reporter.Count(ErrorLevel.Error) == postSpecErrorCount) {
+ //KRML ComputeGhostInterest(iter.Body, iter);
+ }
}
currentClass = null;
@@ -4251,13 +4837,13 @@ namespace Microsoft.Dafny }
var prevErrorCount = reporter.Count(ErrorLevel.Error);
if (t.NamePath is ExprDotName) {
- var ret = ResolveDotSuffix_Type((ExprDotName)t.NamePath, new ResolveOpts(context, true, true), allowDanglingDotName, option, defaultTypeArguments);
+ var ret = ResolveDotSuffix_Type((ExprDotName)t.NamePath, new ResolveOpts(context, true), allowDanglingDotName, option, defaultTypeArguments);
if (ret != null) {
return ret;
}
} else {
var s = (NameSegment)t.NamePath;
- ResolveNameSegment_Type(s, new ResolveOpts(context, true, true), option, defaultTypeArguments);
+ ResolveNameSegment_Type(s, new ResolveOpts(context, true), option, defaultTypeArguments);
}
if (reporter.Count(ErrorLevel.Error) == prevErrorCount) {
var r = t.NamePath.Resolved as Resolver_IdentifierExpr;
@@ -4818,31 +5404,22 @@ namespace Microsoft.Dafny return at;
}
- /// <summary>
- /// "specContextOnly" means that the statement must be erasable, that is, it should be okay to omit it
- /// at run time. That means it must not have any side effects on non-ghost variables, for example.
- /// </summary>
- public void ResolveStatement(Statement stmt, bool specContextOnly, ICodeContext codeContext) {
+ public void ResolveStatement(Statement stmt, ICodeContext codeContext) {
Contract.Requires(stmt != null);
Contract.Requires(codeContext != null);
if (!(stmt is ForallStmt)) { // forall statements do their own attribute resolution below
- ResolveAttributes(stmt.Attributes, new ResolveOpts(codeContext, true, true));
+ ResolveAttributes(stmt.Attributes, new ResolveOpts(codeContext, true));
}
if (stmt is PredicateStmt) {
PredicateStmt s = (PredicateStmt)stmt;
- s.IsGhost = true;
- ResolveExpression(s.Expr, new ResolveOpts(codeContext, true, true));
+ ResolveExpression(s.Expr, new ResolveOpts(codeContext, true));
Contract.Assert(s.Expr.Type != null); // follows from postcondition of ResolveExpression
- if (!UnifyTypes(s.Expr.Type, Type.Bool)) {
- reporter.Error(MessageSource.Resolver, s.Expr, "condition is expected to be of type {0}, but is {1}", Type.Bool, s.Expr.Type);
- }
+ 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);
- 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)");
- }
+ var s = (PrintStmt)stmt;
+ var opts = new ResolveOpts(codeContext, false);
+ s.Args.Iter(e => ResolveExpression(e, opts));
} else if (stmt is BreakStmt) {
var s = (BreakStmt)stmt;
@@ -4852,10 +5429,6 @@ namespace Microsoft.Dafny reporter.Error(MessageSource.Resolver, s, "break label is undefined or not in scope: {0}", s.TargetLabel);
} else {
s.TargetStmt = target;
- 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"));
- }
}
} else {
if (loopStack.Count < s.BreakCount) {
@@ -4867,9 +5440,6 @@ namespace Microsoft.Dafny target.Labels = new LList<Label>(new Label(target.Tok, null), null);
}
s.TargetStmt = target;
- 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");
- }
}
}
@@ -4879,8 +5449,6 @@ 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");
- } 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);
}
var s = (ProduceStmt)stmt;
if (s.rhss != null) {
@@ -4911,13 +5479,13 @@ namespace Microsoft.Dafny }
s.hiddenUpdate = new UpdateStmt(s.Tok, s.EndTok, formals, s.rhss, true);
// resolving the update statement will check for return/yield statement specifics.
- ResolveStatement(s.hiddenUpdate, specContextOnly, codeContext);
+ ResolveStatement(s.hiddenUpdate, codeContext);
}
} else {// this is a regular return/yield statement.
s.hiddenUpdate = null;
}
} else if (stmt is ConcreteUpdateStatement) {
- ResolveConcreteUpdateStmt((ConcreteUpdateStatement)stmt, specContextOnly, codeContext);
+ ResolveConcreteUpdateStmt((ConcreteUpdateStatement)stmt, codeContext);
} else if (stmt is VarDeclStmt) {
var s = (VarDeclStmt)stmt;
// We have three cases.
@@ -4939,10 +5507,6 @@ namespace Microsoft.Dafny foreach (var local in s.Locals) {
ResolveType(local.Tok, local.OptionalType, codeContext, ResolveTypeOptionEnum.InferTypeProxies, null);
local.type = local.OptionalType;
- if (specContextOnly) {
- // a local variable in a specification-only context might as well be ghost
- local.IsGhost = true;
- }
}
// Resolve the UpdateStmt, if any
if (s.Update is UpdateStmt) {
@@ -4957,7 +5521,7 @@ namespace Microsoft.Dafny lhs.Type = local.Type;
}
// resolve the whole thing
- ResolveConcreteUpdateStmt(s.Update, specContextOnly, codeContext);
+ ResolveConcreteUpdateStmt(s.Update, codeContext);
}
// Add the locals to the scope
foreach (var local in s.Locals) {
@@ -4965,16 +5529,13 @@ namespace Microsoft.Dafny }
// With the new locals in scope, it's now time to resolve the attributes on all the locals
foreach (var local in s.Locals) {
- ResolveAttributes(local.Attributes, new ResolveOpts(codeContext, true, true));
+ ResolveAttributes(local.Attributes, new ResolveOpts(codeContext, true));
}
// Resolve the AssignSuchThatStmt, if any
if (s.Update is AssignSuchThatStmt) {
- ResolveConcreteUpdateStmt(s.Update, specContextOnly, codeContext);
+ ResolveConcreteUpdateStmt(s.Update, codeContext);
}
// Update the VarDeclStmt's ghost status according to its components
- if (!s.IsGhost) {
- s.IsGhost = (s.Update == null || s.Update.IsGhost) && s.Locals.All(v => v.IsGhost);
- }
foreach (var local in s.Locals)
{
if (Attributes.Contains(local.Attributes, "assumption"))
@@ -4983,13 +5544,12 @@ namespace Microsoft.Dafny {
reporter.Error(MessageSource.Resolver, local.Tok, "assumption variable can only be declared in a method");
}
- if (!local.IsGhost)
- {
- reporter.Error(MessageSource.Resolver, local.Tok, "assumption variable must be ghost");
- }
if (!(local.Type.IsBoolType))
{
- reporter.Error(MessageSource.Resolver, s, "assumption variable must be of type 'bool'");
+ reporter.Error(MessageSource.Resolver, local.Tok, "assumption variable must be of type 'bool'");
+ }
+ if (!local.IsGhost) {
+ reporter.Error(MessageSource.Resolver, local.Tok, "assumption variable must be ghost");
}
}
}
@@ -4997,22 +5557,17 @@ namespace Microsoft.Dafny } else if (stmt is AssignStmt) {
AssignStmt s = (AssignStmt)stmt;
int prevErrorCount = reporter.Count(ErrorLevel.Error);
- ResolveExpression(s.Lhs, new ResolveOpts(codeContext, true, specContextOnly)); // allow ghosts for now, tighted up below
+ ResolveExpression(s.Lhs, new ResolveOpts(codeContext, true)); // allow ghosts for now, tighted up below
bool lhsResolvedSuccessfully = reporter.Count(ErrorLevel.Error) == prevErrorCount;
Contract.Assert(s.Lhs.Type != null); // follows from postcondition of ResolveExpression
// check that LHS denotes a mutable variable or a field
- bool lvalueIsGhost = false;
var lhs = s.Lhs.Resolved;
if (lhs is IdentifierExpr) {
IVariable var = ((IdentifierExpr)lhs).Var;
if (var == null) {
// the LHS didn't resolve correctly; some error would already have been reported
} else {
- lvalueIsGhost = var.IsGhost || codeContext.IsGhost;
CheckIsLvalue(lhs, codeContext);
- 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)");
- }
var localVar = var as LocalVariable;
if (localVar != null && currentMethod != null && Attributes.Contains(localVar.Attributes, "assumption"))
@@ -5037,18 +5592,6 @@ namespace Microsoft.Dafny } else if (lhs is MemberSelectExpr) {
var fse = (MemberSelectExpr)lhs;
if (fse.Member != null) { // otherwise, an error was reported above
- lvalueIsGhost = fse.Member.IsGhost;
- 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)");
- } else {
- // It is now that we wish we would have resolved s.Lhs to not allow ghosts. Too late, so we do
- // the next best thing.
- if (lhsResolvedSuccessfully && UsesSpecFeatures(fse.Obj)) {
- reporter.Error(MessageSource.Resolver, stmt, "Assignment to non-ghost field is not allowed to use specification-only expressions in the receiver");
- }
- }
- }
CheckIsLvalue(fse, codeContext);
}
} else if (lhs is SeqSelectExpr) {
@@ -5056,52 +5599,26 @@ namespace Microsoft.Dafny // LHS is fine, provided the "sequence" is really an array
if (lhsResolvedSuccessfully) {
Contract.Assert(slhs.Seq.Type != null);
- 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)");
- }
CheckIsLvalue(slhs, codeContext);
}
} else if (lhs is MultiSelectExpr) {
- 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)");
- }
CheckIsLvalue(lhs, codeContext);
} else {
CheckIsLvalue(lhs, codeContext);
}
- s.IsGhost = lvalueIsGhost;
Type lhsType = s.Lhs.Type;
if (s.Rhs is ExprRhs) {
ExprRhs rr = (ExprRhs)s.Rhs;
- ResolveExpression(rr.Expr, new ResolveOpts(codeContext, true, specContextOnly));
- if (!lvalueIsGhost) {
- CheckIsNonGhost(rr.Expr);
- }
+ ResolveExpression(rr.Expr, new ResolveOpts(codeContext, true));
Contract.Assert(rr.Expr.Type != null); // follows from postcondition of ResolveExpression
- if (!UnifyTypes(lhsType, rr.Expr.Type)) {
- reporter.Error(MessageSource.Resolver, stmt, "RHS (of type {0}) not assignable to LHS (of type {1})", rr.Expr.Type, lhsType);
- }
+ 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 (!lvalueIsGhost) {
- if (rr.ArrayDimensions != null) {
- foreach (var dim in rr.ArrayDimensions) {
- CheckIsNonGhost(dim);
- }
- }
- if (rr.InitCall != null) {
- foreach (var arg in rr.InitCall.Args) {
- CheckIsNonGhost(arg);
- }
- }
- }
- if (!UnifyTypes(lhsType, t)) {
- reporter.Error(MessageSource.Resolver, stmt, "type {0} is not assignable to LHS (of type {1})", t, lhsType);
- }
+ Type t = ResolveTypeRhs(rr, stmt, codeContext);
+ 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
} else {
@@ -5110,105 +5627,45 @@ namespace Microsoft.Dafny } else if (stmt is CallStmt) {
CallStmt s = (CallStmt)stmt;
- ResolveCallStmt(s, specContextOnly, codeContext, null);
+ ResolveCallStmt(s, codeContext, null);
} else if (stmt is BlockStmt) {
var s = (BlockStmt)stmt;
scope.PushMarker();
- ResolveBlockStatement(s, specContextOnly, codeContext);
- if (!s.IsGhost) {
- s.IsGhost = s.Body.All(ss => ss.IsGhost); // mark the block statement as ghost if all its substatements are ghost
- }
+ ResolveBlockStatement(s, codeContext);
scope.PopMarker();
} else if (stmt is IfStmt) {
IfStmt s = (IfStmt)stmt;
- bool branchesAreSpecOnly = specContextOnly;
if (s.Guard != null) {
- int prevErrorCount = reporter.Count(ErrorLevel.Error);
- ResolveExpression(s.Guard, new ResolveOpts(codeContext, true, specContextOnly));
+ ResolveExpression(s.Guard, new ResolveOpts(codeContext, true));
Contract.Assert(s.Guard.Type != null); // follows from postcondition of ResolveExpression
- bool successfullyResolved = reporter.Count(ErrorLevel.Error) == prevErrorCount;
- if (!UnifyTypes(s.Guard.Type, Type.Bool)) {
- reporter.Error(MessageSource.Resolver, s.Guard, "condition is expected to be of type {0}, but is {1}", Type.Bool, s.Guard.Type);
- }
- if (!specContextOnly && successfullyResolved) {
- branchesAreSpecOnly = UsesSpecFeatures(s.Guard);
- }
+ ConstrainTypes(s.Guard.Type, Type.Bool, s.Guard, "condition is expected to be of type {0}, but is {1}", Type.Bool, s.Guard.Type);
}
- s.IsGhost = branchesAreSpecOnly;
- ResolveStatement(s.Thn, branchesAreSpecOnly, codeContext);
+ ResolveStatement(s.Thn, codeContext);
if (s.Els != null) {
- ResolveStatement(s.Els, branchesAreSpecOnly, codeContext);
- }
- if (!s.IsGhost && s.Thn.IsGhost && (s.Els == null || s.Els.IsGhost)) {
- // mark the entire 'if' statement as ghost if its branches are ghost
- s.IsGhost = true;
+ ResolveStatement(s.Els, codeContext);
}
} else if (stmt is AlternativeStmt) {
var s = (AlternativeStmt)stmt;
- s.IsGhost = ResolveAlternatives(s.Alternatives, specContextOnly, null, codeContext);
- if (!s.IsGhost) {
- s.IsGhost = s.Alternatives.All(alt => alt.Body.All(ss => ss.IsGhost));
- }
+ ResolveAlternatives(s.Alternatives, null, codeContext);
} else if (stmt is WhileStmt) {
WhileStmt s = (WhileStmt)stmt;
- bool bodyMustBeSpecOnly = specContextOnly;
var fvs = new HashSet<IVariable>();
if (s.Guard != null) {
- int prevErrorCount = reporter.Count(ErrorLevel.Error);
- ResolveExpression(s.Guard, new ResolveOpts(codeContext, true, specContextOnly));
+ ResolveExpression(s.Guard, new ResolveOpts(codeContext, true));
Contract.Assert(s.Guard.Type != null); // follows from postcondition of ResolveExpression
- bool successfullyResolved = reporter.Count(ErrorLevel.Error) == prevErrorCount;
Translator.ComputeFreeVariables(s.Guard, fvs);
- if (!UnifyTypes(s.Guard.Type, Type.Bool)) {
- reporter.Error(MessageSource.Resolver, s.Guard, "condition is expected to be of type {0}, but is {1}", Type.Bool, s.Guard.Type);
- }
- if (!specContextOnly && successfullyResolved) {
- bodyMustBeSpecOnly = UsesSpecFeatures(s.Guard);
- }
+ ConstrainTypes(s.Guard.Type, Type.Bool, s.Guard, "condition is expected to be of type {0}, but is {1}", Type.Bool, s.Guard.Type);
}
- foreach (MaybeFreeExpression inv in s.Invariants) {
- ResolveAttributes(inv.Attributes, new ResolveOpts(codeContext, true, true));
- ResolveExpression(inv.E, new ResolveOpts(codeContext, true, true));
- Contract.Assert(inv.E.Type != null); // follows from postcondition of ResolveExpression
- Translator.ComputeFreeVariables(inv.E, fvs);
- if (!UnifyTypes(inv.E.Type, Type.Bool)) {
- reporter.Error(MessageSource.Resolver, inv.E, "invariant is expected to be of type {0}, but is {1}", Type.Bool, inv.E.Type);
- }
- }
+ ResolveLoopSpecificationComponents(s.Invariants, s.Decreases, s.Mod, codeContext, fvs);
- ResolveAttributes(s.Decreases.Attributes, new ResolveOpts(codeContext, true, true));
- foreach (Expression e in s.Decreases.Expressions) {
- ResolveExpression(e, new ResolveOpts(codeContext, true, true));
- if (e is WildcardExpr) {
- if (bodyMustBeSpecOnly) {
- reporter.Error(MessageSource.Resolver, e, "'decreases *' is not allowed on ghost loops");
- } else if (!codeContext.AllowsNontermination && !DafnyOptions.O.Dafnycc) {
- reporter.Error(MessageSource.Resolver, e, "a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating");
- }
- }
- // any type is fine
- }
-
- if (s.Mod.Expressions != null) {
- ResolveAttributes(s.Mod.Attributes, new ResolveOpts(codeContext, true, true));
- foreach (FrameExpression fe in s.Mod.Expressions) {
- ResolveFrameExpression(fe, false, bodyMustBeSpecOnly, codeContext);
- Translator.ComputeFreeVariables(fe.E, fvs);
- }
- }
- s.IsGhost = s.Body == null || bodyMustBeSpecOnly;
if (s.Body != null) {
loopStack.Add(s); // push
- if (s.Labels == null) { // otherwise, "s" is already in "inSpecOnlyContext" map
- inSpecOnlyContext.Add(s, specContextOnly);
- }
-
- ResolveStatement(s.Body, bodyMustBeSpecOnly, codeContext);
+ ResolveStatement(s.Body, codeContext);
loopStack.RemoveAt(loopStack.Count - 1); // pop
} else {
string text = "havoc {" + Util.Comma(", ", fvs, fv => fv.Name) + "};"; // always terminate with a semi-colon
@@ -5217,26 +5674,8 @@ namespace Microsoft.Dafny } else if (stmt is AlternativeLoopStmt) {
var s = (AlternativeLoopStmt)stmt;
- s.IsGhost = ResolveAlternatives(s.Alternatives, specContextOnly, s, codeContext);
- foreach (MaybeFreeExpression inv in s.Invariants) {
- ResolveExpression(inv.E, new ResolveOpts(codeContext, true, true));
- Contract.Assert(inv.E.Type != null); // follows from postcondition of ResolveExpression
- if (!UnifyTypes(inv.E.Type, Type.Bool)) {
- reporter.Error(MessageSource.Resolver, inv.E, "invariant is expected to be of type {0}, but is {1}", Type.Bool, inv.E.Type);
- }
- }
-
- foreach (Expression e in s.Decreases.Expressions) {
- ResolveExpression(e, new ResolveOpts(codeContext, true, true));
- if (e is WildcardExpr) {
- if (s.IsGhost) {
- reporter.Error(MessageSource.Resolver, e, "'decreases *' is not allowed on ghost loops");
- } else if (!codeContext.AllowsNontermination && !DafnyOptions.O.Dafnycc) {
- reporter.Error(MessageSource.Resolver, e, "a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating");
- }
- }
- // any type is fine
- }
+ ResolveAlternatives(s.Alternatives, s, codeContext);
+ ResolveLoopSpecificationComponents(s.Invariants, s.Decreases, s.Mod, codeContext, null);
} else if (stmt is ForallStmt) {
var s = (ForallStmt)stmt;
@@ -5247,32 +5686,17 @@ namespace Microsoft.Dafny ScopePushAndReport(scope, v, "local-variable");
ResolveType(v.tok, v.Type, codeContext, ResolveTypeOptionEnum.InferTypeProxies, null);
}
- ResolveExpression(s.Range, new ResolveOpts(codeContext, true, specContextOnly));
+ ResolveExpression(s.Range, new ResolveOpts(codeContext, true));
Contract.Assert(s.Range.Type != null); // follows from postcondition of ResolveExpression
- if (!UnifyTypes(s.Range.Type, Type.Bool)) {
- reporter.Error(MessageSource.Resolver, stmt, "range restriction in forall statement must be of type bool (instead got {0})", s.Range.Type);
- }
+ ConstrainTypes(s.Range.Type, Type.Bool, stmt, "range restriction in forall statement must be of type bool (instead got {0})", s.Range.Type);
foreach (var ens in s.Ens) {
- ResolveExpression(ens.E, new ResolveOpts(codeContext, true, true));
+ ResolveExpression(ens.E, new ResolveOpts(codeContext, true));
Contract.Assert(ens.E.Type != null); // follows from postcondition of ResolveExpression
- if (!UnifyTypes(ens.E.Type, Type.Bool)) {
- reporter.Error(MessageSource.Resolver, ens.E, "ensures condition is expected to be of type {0}, but is {1}", Type.Bool, ens.E.Type);
- }
+ ConstrainTypes(ens.E.Type, Type.Bool, ens.E, "ensures condition is expected to be of type {0}, but is {1}", Type.Bool, ens.E.Type);
}
// Since the range and postconditions are more likely to infer the types of the bound variables, resolve them
// first (above) and only then resolve the attributes (below).
- ResolveAttributes(s.Attributes, new ResolveOpts(codeContext, true, true));
-
- bool bodyMustBeSpecOnly = specContextOnly || (prevErrorCount == reporter.Count(ErrorLevel.Error) && UsesSpecFeatures(s.Range));
- if (!bodyMustBeSpecOnly && prevErrorCount == reporter.Count(ErrorLevel.Error)) {
- CheckTypeInference(s.Range); // we need to resolve operators before the call to DiscoverBounds
- List<BoundVar> missingBounds;
- s.Bounds = DiscoverBestBounds_MultipleVars(s.BoundVars, s.Range, true, true, out missingBounds);
- if (missingBounds.Count != 0) {
- bodyMustBeSpecOnly = true;
- }
- }
- s.IsGhost = s.Body == null || bodyMustBeSpecOnly;
+ ResolveAttributes(s.Attributes, new ResolveOpts(codeContext, true));
if (s.Body != null) {
// clear the labels for the duration of checking the body, because break statements are not allowed to leave a forall statement
@@ -5280,7 +5704,7 @@ namespace Microsoft.Dafny var prevLoopStack = loopStack;
labeledStatements = new Scope<Statement>();
loopStack = new List<Statement>();
- ResolveStatement(s.Body, bodyMustBeSpecOnly, codeContext);
+ ResolveStatement(s.Body, codeContext);
labeledStatements = prevLblStmts;
loopStack = prevLoopStack;
}
@@ -5327,34 +5751,30 @@ namespace Microsoft.Dafny } else if (stmt is ModifyStmt) {
var s = (ModifyStmt)stmt;
- ResolveAttributes(s.Mod.Attributes, new ResolveOpts(codeContext, true, true));
+ ResolveAttributes(s.Mod.Attributes, new ResolveOpts(codeContext, true));
foreach (FrameExpression fe in s.Mod.Expressions) {
- // (yes, say "modifies", not "modify", in the next line -- it seems to give a more readable error message
- ResolveFrameExpression(fe, false, specContextOnly, codeContext);
+ ResolveFrameExpression(fe, false, codeContext);
}
if (s.Body != null) {
- ResolveBlockStatement(s.Body, specContextOnly, codeContext);
+ ResolveBlockStatement(s.Body, codeContext);
}
- s.IsGhost = specContextOnly;
} else if (stmt is CalcStmt) {
var prevErrorCount = reporter.Count(ErrorLevel.Error);
CalcStmt s = (CalcStmt)stmt;
- s.IsGhost = true;
if (s.Lines.Count > 0) {
var e0 = s.Lines.First();
- ResolveExpression(e0, new ResolveOpts(codeContext, true, true));
+ ResolveExpression(e0, new ResolveOpts(codeContext, true));
Contract.Assert(e0.Type != null); // follows from postcondition of ResolveExpression
for (int i = 1; i < s.Lines.Count; i++) {
if (i < s.Lines.Count - 1 || prevErrorCount == reporter.Count(ErrorLevel.Error)) { // do not resolve the dummy step if there were errors, it might generate more errors
var e1 = s.Lines[i];
- ResolveExpression(e1, new ResolveOpts(codeContext, true, true));
+ ResolveExpression(e1, new ResolveOpts(codeContext, true));
Contract.Assert(e1.Type != null); // follows from postcondition of ResolveExpression
- if (!UnifyTypes(e0.Type, e1.Type)) {
- reporter.Error(MessageSource.Resolver, e1, "all lines in a calculation must have the same type (got {0} after {1})", e1.Type, e0.Type);
+ if (!ConstrainTypes(e0.Type, e1.Type, e1, "all lines in a calculation must have the same type (got {0} after {1})", e1.Type, e0.Type)) {
} else {
var step = s.StepOps[i - 1].StepExpr(e0, e1); // Use custom line operator
- ResolveExpression(step, new ResolveOpts(codeContext, true, true));
+ ResolveExpression(step, new ResolveOpts(codeContext, true));
s.Steps.Add(step);
}
e0 = e1;
@@ -5367,8 +5787,7 @@ namespace Microsoft.Dafny labeledStatements = new Scope<Statement>();
loopStack = new List<Statement>();
foreach (var h in s.Hints) {
- ResolveStatement(h, true, codeContext);
- CheckHintRestrictions(h);
+ ResolveStatement(h, codeContext);
}
labeledStatements = prevLblStmts;
loopStack = prevLoopStack;
@@ -5380,36 +5799,68 @@ namespace Microsoft.Dafny } else {
s.Result = CalcStmt.DefaultOp.StepExpr(Expression.CreateIntLiteral(s.Tok, 0), Expression.CreateIntLiteral(s.Tok, 0));
}
- ResolveExpression(s.Result, new ResolveOpts(codeContext, true, true));
+ ResolveExpression(s.Result, new ResolveOpts(codeContext, true));
Contract.Assert(s.Result != null);
Contract.Assert(prevErrorCount != reporter.Count(ErrorLevel.Error) || s.Steps.Count == s.Hints.Count);
} else if (stmt is MatchStmt) {
- ResolveMatchStmt(stmt, specContextOnly, codeContext);
+ ResolveMatchStmt(stmt, codeContext);
} else if (stmt is SkeletonStatement) {
var s = (SkeletonStatement)stmt;
reporter.Error(MessageSource.Resolver, s.Tok, "skeleton statements are allowed only in refining methods");
// nevertheless, resolve the underlying statement; hey, why not
if (s.S != null) {
- ResolveStatement(s.S, specContextOnly, codeContext);
+ ResolveStatement(s.S, codeContext);
}
} else {
Contract.Assert(false); throw new cce.UnreachableException();
}
}
- void ResolveMatchStmt(Statement stmt, bool specContextOnly, ICodeContext codeContext) {
+ private void ResolveLoopSpecificationComponents(List<MaybeFreeExpression> invariants, Specification<Expression> decreases, Specification<FrameExpression> modifies, ICodeContext codeContext, HashSet<IVariable> fvs) {
+ Contract.Requires(invariants != null);
+ Contract.Requires(decreases != null);
+ Contract.Requires(modifies != null);
+ Contract.Requires(codeContext != null);
+
+ foreach (MaybeFreeExpression inv in invariants) {
+ ResolveAttributes(inv.Attributes, new ResolveOpts(codeContext, true));
+ ResolveExpression(inv.E, new ResolveOpts(codeContext, true));
+ Contract.Assert(inv.E.Type != null); // follows from postcondition of ResolveExpression
+ if (fvs != null) {
+ Translator.ComputeFreeVariables(inv.E, fvs);
+ }
+ ConstrainTypes(inv.E.Type, Type.Bool, inv.E, "invariant is expected to be of type {0}, but is {1}", Type.Bool, inv.E.Type);
+ }
+
+ ResolveAttributes(decreases.Attributes, new ResolveOpts(codeContext, true));
+ foreach (Expression e in decreases.Expressions) {
+ ResolveExpression(e, new ResolveOpts(codeContext, true));
+ if (e is WildcardExpr) {
+ if (!codeContext.AllowsNontermination && !DafnyOptions.O.Dafnycc) {
+ reporter.Error(MessageSource.Resolver, e, "a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating");
+ }
+ }
+ // any type is fine
+ }
+
+ ResolveAttributes(modifies.Attributes, new ResolveOpts(codeContext, true));
+ if (modifies.Expressions != null) {
+ foreach (FrameExpression fe in modifies.Expressions) {
+ ResolveFrameExpression(fe, false, codeContext);
+ if (fvs != null) {
+ Translator.ComputeFreeVariables(fe.E, fvs);
+ }
+ }
+ }
+ }
+
+ void ResolveMatchStmt(Statement stmt, ICodeContext codeContext) {
MatchStmt s = (MatchStmt)stmt;
DesugarMatchStmtWithTupleExpression(s);
- bool bodyIsSpecOnly = specContextOnly;
- int prevErrorCount = reporter.Count(ErrorLevel.Error);
- ResolveExpression(s.Source, new ResolveOpts(codeContext, true, specContextOnly));
+ ResolveExpression(s.Source, new ResolveOpts(codeContext, true));
Contract.Assert(s.Source.Type != null); // follows from postcondition of ResolveExpression
- bool successfullyResolved = reporter.Count(ErrorLevel.Error) == prevErrorCount;
- if (!specContextOnly && successfullyResolved) {
- bodyIsSpecOnly = UsesSpecFeatures(s.Source);
- }
UserDefinedType sourceType = null;
DatatypeDecl dtd = null;
if (s.Source.Type.IsDatatype) {
@@ -5431,7 +5882,6 @@ namespace Microsoft.Dafny subst.Add(dtd.TypeArgs[i], sourceType.TypeArgs[i]);
}
}
- s.IsGhost = bodyIsSpecOnly;
// convert CasePattern in MatchCaseExpr to BoundVar and flatten the MatchCaseExpr.
Type type = new InferredTypeProxy();
@@ -5472,16 +5922,14 @@ namespace Microsoft.Dafny if (ctor != null && i < ctor.Formals.Count) {
Formal formal = ctor.Formals[i];
Type st = SubstType(formal.Type, subst);
- if (!UnifyTypes(v.Type, st)) {
- reporter.Error(MessageSource.Resolver, stmt, "the declared type of the formal ({0}) does not agree with the corresponding type in the constructor's signature ({1})", v.Type, st);
- }
+ ConstrainTypes(v.Type, st, stmt, "the declared type of the formal ({0}) does not agree with the corresponding type in the constructor's signature ({1})", v.Type, st);
v.IsGhost = formal.IsGhost;
// update the type of the boundvars in the MatchCaseToken
if (v.tok is MatchCaseToken) {
MatchCaseToken mt = (MatchCaseToken)v.tok;
foreach (Tuple<IToken, BoundVar, bool> entry in mt.varList) {
- UnifyTypes(entry.Item2.Type, v.Type);
+ UnifyTypes(entry.Item2.Type, v.Type); // TODO: What if this unification fails? Can it? --KRML
}
}
}
@@ -5489,7 +5937,7 @@ namespace Microsoft.Dafny }
}
foreach (Statement ss in mc.Body) {
- ResolveStatement(ss, bodyIsSpecOnly, codeContext);
+ ResolveStatement(ss, codeContext);
}
// substitute body to replace the case pat with v. This needs to happen
// after the body is resolved so we can scope the bv correctly.
@@ -5499,7 +5947,7 @@ namespace Microsoft.Dafny foreach (Statement ss in mc.Body) {
Statement clone = cloner.CloneStmt(ss);
// resolve it again since we just cloned it.
- ResolveStatement(clone, bodyIsSpecOnly, codeContext);
+ ResolveStatement(clone, codeContext);
list.Add(clone);
}
mc.UpdateBody(list);
@@ -5519,9 +5967,6 @@ namespace Microsoft.Dafny }
Contract.Assert(memberNamesUsed.Count + s.MissingCases.Count == dtd.Ctors.Count);
}
- if (!s.IsGhost) {
- s.IsGhost = s.Cases.All(cs => cs.Body.All(ss => ss.IsGhost));
- }
}
/*
@@ -5920,7 +6365,7 @@ namespace Microsoft.Dafny reporter.Info(MessageSource.Resolver, loopStmt.Tok, s);
}
}
- private void ResolveConcreteUpdateStmt(ConcreteUpdateStatement s, bool specContextOnly, ICodeContext codeContext) {
+ private void ResolveConcreteUpdateStmt(ConcreteUpdateStatement s, ICodeContext codeContext) {
Contract.Requires(codeContext != null);
// First, resolve all LHS's and expression-looking RHS's.
@@ -5930,11 +6375,8 @@ namespace Microsoft.Dafny var lhsNameSet = new HashSet<string>(); // used to check for duplicate identifiers on the left (full duplication checking for references and the like is done during verification)
foreach (var lhs in s.Lhss) {
var ec = reporter.Count(ErrorLevel.Error);
- ResolveExpression(lhs, new ResolveOpts(codeContext, true, specContextOnly));
+ ResolveExpression(lhs, new ResolveOpts(codeContext, true));
if (ec == reporter.Count(ErrorLevel.Error)) {
- if (update == null && specContextOnly && !AssignStmt.LhsIsToGhost(lhs) && !codeContext.IsGhost) {
- reporter.Error(MessageSource.Resolver, lhs, "cannot assign to non-ghost variable in a ghost context");
- }
if (lhs is SeqSelectExpr && !((SeqSelectExpr)lhs).SelectOne) {
reporter.Error(MessageSource.Resolver, lhs, "cannot assign to a range of array elements (try the 'forall' statement)");
}
@@ -5944,18 +6386,18 @@ namespace Microsoft.Dafny // Resolve RHSs
if (update == null) {
var suchThat = (AssignSuchThatStmt)s; // this is the other possible subclass
- ResolveAssignSuchThatStmt(suchThat, specContextOnly, codeContext);
+ ResolveAssignSuchThatStmt(suchThat, codeContext);
} else {
- ResolveUpdateStmt(update, specContextOnly, codeContext, errorCountBeforeCheckingLhs);
+ ResolveUpdateStmt(update, codeContext, errorCountBeforeCheckingLhs);
}
- ResolveAttributes(s.Attributes, new ResolveOpts(codeContext, true, true));
+ ResolveAttributes(s.Attributes, new ResolveOpts(codeContext, true));
}
/// <summary>
/// Resolve the RHSs and entire UpdateStmt (LHSs should already have been checked by the caller).
/// errorCountBeforeCheckingLhs is passed in so that this method can determined if any resolution errors were found during
/// LHS or RHS checking, because only if no errors were found is update.ResolvedStmt changed.
/// </summary>
- private void ResolveUpdateStmt(UpdateStmt update, bool specContextOnly, ICodeContext codeContext, int errorCountBeforeCheckingLhs) {
+ private void ResolveUpdateStmt(UpdateStmt update, ICodeContext codeContext, int errorCountBeforeCheckingLhs) {
Contract.Requires(update != null);
Contract.Requires(codeContext != null);
IToken firstEffectfulRhs = null;
@@ -5965,7 +6407,7 @@ namespace Microsoft.Dafny bool isEffectful;
if (rhs is TypeRhs) {
var tr = (TypeRhs)rhs;
- ResolveTypeRhs(tr, update, specContextOnly, codeContext);
+ ResolveTypeRhs(tr, update, codeContext);
isEffectful = tr.InitCall != null;
} else if (rhs is HavocRhs) {
isEffectful = false;
@@ -5973,17 +6415,11 @@ namespace Microsoft.Dafny var er = (ExprRhs)rhs;
if (er.Expr is ApplySuffix) {
var a = (ApplySuffix)er.Expr;
- // Note, in the following line, the dontCareAboutCompilation could be more precise. It could be computed as in the else
- // branch if the ApplySuffix is really just the RHS of an assignment. However, if "update" is really a call statement,
- // then we should not let the LHS influence the call to ResolveApplySuffix. Unfortunately, we don't know which case
- // we're in until ResolveApplySuffix has returned (where a non-null cRhs indicates that "update" is a call statement).
- // So, we'll be conservative and will simply pass in specContextOnly here.
- var cRhs = ResolveApplySuffix(a, new ResolveOpts(codeContext, true, specContextOnly/*see note on previous line*/), true);
+ var cRhs = ResolveApplySuffix(a, new ResolveOpts(codeContext, true), true);
isEffectful = cRhs != null;
methodCallInfo = methodCallInfo ?? cRhs;
} else {
- var dontCareAboutCompilation = specContextOnly || (j < update.Lhss.Count && AssignStmt.LhsIsToGhost(update.Lhss[j]));
- ResolveExpression(er.Expr, new ResolveOpts(codeContext, true, dontCareAboutCompilation));
+ ResolveExpression(er.Expr, new ResolveOpts(codeContext, true));
isEffectful = false;
}
}
@@ -6054,12 +6490,11 @@ namespace Microsoft.Dafny }
foreach (var a in update.ResolvedStatements) {
- ResolveStatement(a, specContextOnly, codeContext);
+ ResolveStatement(a, codeContext);
}
- update.IsGhost = update.ResolvedStatements.TrueForAll(ss => ss.IsGhost);
}
- private void ResolveAssignSuchThatStmt(AssignSuchThatStmt s, bool specContextOnly, ICodeContext codeContext) {
+ private void ResolveAssignSuchThatStmt(AssignSuchThatStmt s, ICodeContext codeContext) {
Contract.Requires(s != null);
Contract.Requires(codeContext != null);
@@ -6076,71 +6511,44 @@ namespace Microsoft.Dafny }
}
- s.IsGhost = s.Lhss.TrueForAll(AssignStmt.LhsIsToGhost);
var ec = reporter.Count(ErrorLevel.Error);
- ResolveExpression(s.Expr, new ResolveOpts(codeContext, true, specContextOnly));
- if (!UnifyTypes(s.Expr.Type, Type.Bool)) {
- reporter.Error(MessageSource.Resolver, 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) {
- CheckIsNonGhost(s.Expr);
-
- 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);
- if (missingBounds.Count != 0) {
- s.MissingBounds = missingBounds; // so that an error message can be produced during compilation
- } else {
- Contract.Assert(bestBounds != null);
- s.Bounds = bestBounds;
- }
- }
+ ResolveExpression(s.Expr, new ResolveOpts(codeContext, true));
+ ConstrainTypes(s.Expr.Type, Type.Bool, s.Expr, "type of RHS of assign-such-that statement must be boolean (got {0})", s.Expr.Type);
}
- bool ResolveAlternatives(List<GuardedAlternative> alternatives, bool specContextOnly, AlternativeLoopStmt loopToCatchBreaks, ICodeContext codeContext) {
+ void ResolveAlternatives(List<GuardedAlternative> alternatives, AlternativeLoopStmt loopToCatchBreaks, ICodeContext codeContext) {
Contract.Requires(alternatives != null);
Contract.Requires(codeContext != null);
- bool isGhost = specContextOnly;
// first, resolve the guards, which tells us whether or not the entire statement is a ghost statement
foreach (var alternative in alternatives) {
int prevErrorCount = reporter.Count(ErrorLevel.Error);
- ResolveExpression(alternative.Guard, new ResolveOpts(codeContext, true, specContextOnly));
+ ResolveExpression(alternative.Guard, new ResolveOpts(codeContext, true));
Contract.Assert(alternative.Guard.Type != null); // follows from postcondition of ResolveExpression
bool successfullyResolved = reporter.Count(ErrorLevel.Error) == prevErrorCount;
- if (!UnifyTypes(alternative.Guard.Type, Type.Bool)) {
- reporter.Error(MessageSource.Resolver, alternative.Guard, "condition is expected to be of type {0}, but is {1}", Type.Bool, alternative.Guard.Type);
- }
- if (!specContextOnly && successfullyResolved) {
- isGhost = isGhost || UsesSpecFeatures(alternative.Guard);
- }
+ ConstrainTypes(alternative.Guard.Type, Type.Bool, alternative.Guard, "condition is expected to be of type {0}, but is {1}", Type.Bool, alternative.Guard.Type);
}
if (loopToCatchBreaks != null) {
loopStack.Add(loopToCatchBreaks); // push
- if (loopToCatchBreaks.Labels == null) { // otherwise, "loopToCatchBreak" is already in "inSpecOnlyContext" map
- inSpecOnlyContext.Add(loopToCatchBreaks, specContextOnly);
- }
}
foreach (var alternative in alternatives) {
scope.PushMarker();
foreach (Statement ss in alternative.Body) {
- ResolveStatement(ss, isGhost, codeContext);
+ ResolveStatement(ss, codeContext);
}
scope.PopMarker();
}
if (loopToCatchBreaks != null) {
loopStack.RemoveAt(loopStack.Count - 1); // pop
}
-
- return isGhost;
}
/// <summary>
/// Resolves the given call statement.
/// Assumes all LHSs have already been resolved (and checked for mutability).
/// </summary>
- void ResolveCallStmt(CallStmt s, bool specContextOnly, ICodeContext codeContext, Type receiverType) {
+ void ResolveCallStmt(CallStmt s, ICodeContext codeContext, Type receiverType) {
Contract.Requires(s != null);
Contract.Requires(codeContext != null);
bool isInitCall = receiverType != null;
@@ -6150,27 +6558,15 @@ namespace Microsoft.Dafny if (!isInitCall && callee is Constructor) {
reporter.Error(MessageSource.Resolver, s, "a constructor is allowed to be called only when an object is being allocated");
}
- s.IsGhost = callee.IsGhost;
- if (specContextOnly && !callee.IsGhost) {
- reporter.Error(MessageSource.Resolver, s, "only ghost methods can be called from this context");
- }
// resolve left-hand sides
foreach (var lhs in s.Lhs) {
Contract.Assume(lhs.Type != null); // a sanity check that LHSs have already been resolved
}
// resolve arguments
- if (!s.IsGhost && s.Receiver.WasResolved()) {
- CheckIsNonGhost(s.Receiver);
- }
int j = 0;
foreach (Expression e in s.Args) {
- 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 (ec == reporter.Count(ErrorLevel.Error) && !allowGhost) {
- CheckIsNonGhost(e);
- }
+ ResolveExpression(e, new ResolveOpts(codeContext, true));
j++;
}
@@ -6200,39 +6596,14 @@ namespace Microsoft.Dafny // type check the arguments
for (int i = 0; i < callee.Ins.Count; i++) {
Type st = SubstType(callee.Ins[i].Type, s.MethodSelect.TypeArgumentSubstitutions());
- if (!UnifyTypes(cce.NonNull(s.Args[i].Type), st)) {
- reporter.Error(MessageSource.Resolver, s, "incorrect type of method in-parameter {0} (expected {1}, got {2})", i, st, s.Args[i].Type);
- }
+ ConstrainTypes(s.Args[i].Type, st, s, "incorrect type of method in-parameter {0} (expected {1}, got {2})", i, st, s.Args[i].Type);
}
for (int i = 0; i < callee.Outs.Count; i++) {
Type st = SubstType(callee.Outs[i].Type, s.MethodSelect.TypeArgumentSubstitutions());
var lhs = s.Lhs[i];
- if (!UnifyTypes(cce.NonNull(lhs.Type), st)) {
- reporter.Error(MessageSource.Resolver, s, "incorrect type of method out-parameter {0} (expected {1}, got {2})", i, st, lhs.Type);
+ 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 (!specContextOnly && (s.IsGhost || callee.Outs[i].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 {
- reporter.Error(MessageSource.Resolver, s, "actual out-parameter {0} is required to be a ghost variable", i);
- }
- }
- } else if (resolvedLhs is MemberSelectExpr) {
- var ll = (MemberSelectExpr)resolvedLhs;
- if (!ll.Member.IsGhost) {
- reporter.Error(MessageSource.Resolver, s, "actual out-parameter {0} is required to be a ghost field", i);
- }
- } else {
- // this is an array update, and arrays are always non-ghost
- reporter.Error(MessageSource.Resolver, s, "actual out-parameter {0} is required to be a ghost variable", i);
- }
- }
// LHS must denote a mutable field.
CheckIsLvalue(resolvedLhs, codeContext);
}
@@ -6282,9 +6653,7 @@ namespace Microsoft.Dafny }
} else if (lhs is SeqSelectExpr) {
var ll = (SeqSelectExpr)lhs;
- if (!UnifyTypes(ll.Seq.Type, ResolvedArrayType(ll.Seq.tok, 1, new InferredTypeProxy(), codeContext))) {
- reporter.Error(MessageSource.Resolver, ll.Seq, "LHS of array assignment must denote an array element (found {0})", ll.Seq.Type);
- }
+ ConstrainTypes(ll.Seq.Type, ResolvedArrayType(ll.Seq.tok, 1, new InferredTypeProxy(), codeContext), ll.Seq, "LHS of array assignment must denote an array element (found {0})", ll.Seq.Type);
if (!ll.SelectOne) {
reporter.Error(MessageSource.Resolver, ll.Seq, "cannot assign to a range of array elements (try the 'forall' statement)");
}
@@ -6295,7 +6664,7 @@ namespace Microsoft.Dafny }
}
- void ResolveBlockStatement(BlockStmt blockStmt, bool specContextOnly, ICodeContext codeContext) {
+ void ResolveBlockStatement(BlockStmt blockStmt, ICodeContext codeContext) {
Contract.Requires(blockStmt != null);
Contract.Requires(codeContext != null);
@@ -6313,12 +6682,9 @@ namespace Microsoft.Dafny } else {
var r = labeledStatements.Push(lnode.Name, ss);
Contract.Assert(r == Scope<Statement>.PushResult.Success); // since we just checked for duplicates, we expect the Push to succeed
- if (l == ss.Labels) { // add it only once
- inSpecOnlyContext.Add(ss, specContextOnly);
- }
}
}
- ResolveStatement(ss, specContextOnly, codeContext);
+ ResolveStatement(ss, codeContext);
labeledStatements.PopMarker();
}
}
@@ -6471,8 +6837,9 @@ namespace Microsoft.Dafny /// Check that a statment is a valid hint for a calculation.
/// ToDo: generalize the part for compound statements to take a delegate?
/// </summary>
- public void CheckHintRestrictions(Statement stmt) {
+ public void CheckHintRestrictions(Statement stmt, ISet<LocalVariable> localsAllowedInUpdates) {
Contract.Requires(stmt != null);
+ Contract.Requires(localsAllowedInUpdates != null);
if (stmt is PredicateStmt) {
// cool
} else if (stmt is PrintStmt) {
@@ -6486,11 +6853,11 @@ namespace Microsoft.Dafny } else if (stmt is AssignSuchThatStmt) {
var s = (AssignSuchThatStmt)stmt;
foreach (var lhs in s.Lhss) {
- CheckHintLhs(s.Tok, lhs.Resolved);
+ CheckHintLhs(s.Tok, lhs.Resolved, localsAllowedInUpdates);
}
} else if (stmt is AssignStmt) {
var s = (AssignStmt)stmt;
- CheckHintLhs(s.Tok, s.Lhs.Resolved);
+ CheckHintLhs(s.Tok, s.Lhs.Resolved, localsAllowedInUpdates);
} else if (stmt is CallStmt) {
var s = (CallStmt)stmt;
if (s.Method.Mod.Expressions.Count != 0) {
@@ -6499,33 +6866,33 @@ namespace Microsoft.Dafny } else if (stmt is UpdateStmt) {
var s = (UpdateStmt)stmt;
foreach (var ss in s.ResolvedStatements) {
- CheckHintRestrictions(ss);
+ CheckHintRestrictions(ss, localsAllowedInUpdates);
}
} else if (stmt is VarDeclStmt) {
var s = (VarDeclStmt)stmt;
+ s.Locals.Iter(local => localsAllowedInUpdates.Add(local));
if (s.Update != null) {
- CheckHintRestrictions(s.Update);
+ CheckHintRestrictions(s.Update, localsAllowedInUpdates);
}
} else if (stmt is BlockStmt) {
var s = (BlockStmt)stmt;
- scope.PushMarker();
+ var newScopeForLocals = new HashSet<LocalVariable>(localsAllowedInUpdates);
foreach (var ss in s.Body) {
- CheckHintRestrictions(ss);
+ CheckHintRestrictions(ss, newScopeForLocals);
}
- scope.PopMarker();
} else if (stmt is IfStmt) {
var s = (IfStmt)stmt;
- CheckHintRestrictions(s.Thn);
+ CheckHintRestrictions(s.Thn, localsAllowedInUpdates);
if (s.Els != null) {
- CheckHintRestrictions(s.Els);
+ CheckHintRestrictions(s.Els, localsAllowedInUpdates);
}
} else if (stmt is AlternativeStmt) {
var s = (AlternativeStmt)stmt;
foreach (var alt in s.Alternatives) {
foreach (var ss in alt.Body) {
- CheckHintRestrictions(ss);
+ CheckHintRestrictions(ss, localsAllowedInUpdates);
}
}
@@ -6535,14 +6902,14 @@ namespace Microsoft.Dafny reporter.Error(MessageSource.Resolver, s.Mod.Expressions[0].tok, "a while statement used inside a hint is not allowed to have a modifies clause");
}
if (s.Body != null) {
- CheckHintRestrictions(s.Body);
+ CheckHintRestrictions(s.Body, localsAllowedInUpdates);
}
} else if (stmt is AlternativeLoopStmt) {
var s = (AlternativeLoopStmt)stmt;
foreach (var alt in s.Alternatives) {
foreach (var ss in alt.Body) {
- CheckHintRestrictions(ss);
+ CheckHintRestrictions(ss, localsAllowedInUpdates);
}
}
@@ -6564,14 +6931,14 @@ namespace Microsoft.Dafny } else if (stmt is CalcStmt) {
var s = (CalcStmt)stmt;
foreach (var h in s.Hints) {
- CheckHintRestrictions(h);
+ CheckHintRestrictions(h, new HashSet<LocalVariable>());
}
} else if (stmt is MatchStmt) {
var s = (MatchStmt)stmt;
foreach (var kase in s.Cases) {
foreach (var ss in kase.Body) {
- CheckHintRestrictions(ss);
+ CheckHintRestrictions(ss, localsAllowedInUpdates);
}
}
@@ -6580,25 +6947,24 @@ namespace Microsoft.Dafny }
}
- void CheckHintLhs(IToken tok, Expression lhs) {
+ void CheckHintLhs(IToken tok, Expression lhs, ISet<LocalVariable> localsAllowedInUpdates) {
+ Contract.Requires(tok != null);
+ Contract.Requires(lhs != null);
+ Contract.Requires(localsAllowedInUpdates != null);
var idExpr = lhs as IdentifierExpr;
if (idExpr == null) {
reporter.Error(MessageSource.Resolver, tok, "a hint is not allowed to update heap locations");
- } else if (scope.ContainsDecl(idExpr.Var)) {
+ } else if (!localsAllowedInUpdates.Contains(idExpr.Var)) {
reporter.Error(MessageSource.Resolver, tok, "a hint is not allowed to update a variable declared outside the hint");
}
}
- Type ResolveTypeRhs(TypeRhs rr, Statement stmt, bool specContextOnly, ICodeContext codeContext) {
+ Type ResolveTypeRhs(TypeRhs rr, Statement stmt, ICodeContext codeContext) {
Contract.Requires(rr != null);
Contract.Requires(stmt != null);
Contract.Requires(codeContext != null);
Contract.Ensures(Contract.Result<Type>() != null);
- // "new" is not allowed in ghost contexts
- if (specContextOnly) {
- reporter.Error(MessageSource.Resolver, rr.Tok, "'new' is not allowed in ghost contexts");
- }
if (rr.Type == null) {
if (rr.ArrayDimensions != null) {
// ---------- new T[EE]
@@ -6608,9 +6974,7 @@ namespace Microsoft.Dafny foreach (Expression dim in rr.ArrayDimensions) {
Contract.Assert(dim != null);
ResolveExpression(dim, new ResolveOpts(codeContext, true));
- if (!UnifyTypes(dim.Type, new OperationTypeProxy(true, false, false, false, false, false))) {
- reporter.Error(MessageSource.Resolver, stmt, "new must use an integer-based expression for the array size (got {0} for index {1})", dim.Type, i);
- }
+ ConstrainTypes(dim.Type, new OperationTypeProxy(true, false, false, false, false, false), stmt, "new must use an integer-based expression for the array size (got {0} for index {1})", dim.Type, i);
i++;
}
rr.Type = ResolvedArrayType(stmt.Tok, rr.ArrayDimensions.Count, rr.EType, codeContext);
@@ -6652,13 +7016,13 @@ namespace Microsoft.Dafny // type, create an dot-suffix expression around this receiver, and then resolve it in the usual way for dot-suffix expressions.
var lhs = new ImplicitThisExpr(initCallTok) { Type = rr.EType };
var callLhs = new ExprDotName(initCallTok, lhs, initCallName, ret == null ? null : ret.LastComponent.OptTypeArguments);
- ResolveDotSuffix(callLhs, true, rr.Arguments, new ResolveOpts(codeContext, true, specContextOnly), true);
+ ResolveDotSuffix(callLhs, true, rr.Arguments, new ResolveOpts(codeContext, true), true);
if (prevErrorCount == reporter.Count(ErrorLevel.Error)) {
Contract.Assert(callLhs.ResolvedExpression is MemberSelectExpr); // since ResolveApplySuffix succeeded and call.Lhs denotes an expression (not a module or a type)
var methodSel = (MemberSelectExpr)callLhs.ResolvedExpression;
if (methodSel.Member is Method) {
rr.InitCall = new CallStmt(initCallTok, stmt.EndTok, new List<Expression>(), methodSel, rr.Arguments);
- ResolveCallStmt(rr.InitCall, specContextOnly, codeContext, rr.EType);
+ ResolveCallStmt(rr.InitCall, codeContext, rr.EType);
if (rr.InitCall.Method is Constructor) {
callsConstructor = true;
}
@@ -6692,6 +7056,8 @@ namespace Microsoft.Dafny Contract.Requires(memberName != null);
Contract.Ensures(Contract.Result<MemberDecl>() == null || Contract.ValueAtReturn(out nptype) != null);
+ PartiallySolveTypeConstraints(); // so that we can try to pick up the type of the receiver
+
nptype = null; // prepare for the worst
receiverType = receiverType.NormalizeExpand();
var opProxy = receiverType as OperationTypeProxy;
@@ -6932,24 +7298,10 @@ namespace Microsoft.Dafny {
public readonly ICodeContext codeContext;
public readonly bool twoState;
- public readonly bool DontCareAboutCompilation;
public ResolveOpts(ICodeContext codeContext, bool twoState) {
Contract.Requires(codeContext != null);
this.codeContext = codeContext;
this.twoState = twoState;
- DontCareAboutCompilation = codeContext.IsGhost;
- }
- public ResolveOpts(ICodeContext codeContext, bool twoState, bool dontCareAboutCompilation) {
- Contract.Requires(codeContext != null);
- this.codeContext = codeContext;
- this.twoState = twoState;
- this.DontCareAboutCompilation = dontCareAboutCompilation;
- }
- public ResolveOpts(ResolveOpts r, bool dontCareAboutCompilation) {
- Contract.Requires(r != null);
- this.codeContext = r.codeContext;
- this.twoState = r.twoState;
- this.DontCareAboutCompilation = dontCareAboutCompilation;
}
}
@@ -7083,9 +7435,7 @@ namespace Microsoft.Dafny foreach (Expression ee in e.Elements) {
ResolveExpression(ee, opts);
Contract.Assert(ee.Type != null); // follows from postcondition of ResolveExpression
- if (!UnifyTypes(elementType, ee.Type)) {
- reporter.Error(MessageSource.Resolver, ee, "All elements of display must be of the same type (got {0}, but type of previous elements is {1})", ee.Type, elementType);
- }
+ ConstrainTypes(elementType, ee.Type, ee, "All elements of display must be of the same type (got {0}, but type of previous elements is {1})", ee.Type, elementType);
}
if (expr is SetDisplayExpr) {
var se = (SetDisplayExpr)expr;
@@ -7102,14 +7452,10 @@ namespace Microsoft.Dafny foreach (ExpressionPair p in e.Elements) {
ResolveExpression(p.A, opts);
Contract.Assert(p.A.Type != null); // follows from postcondition of ResolveExpression
- if (!UnifyTypes(domainType, p.A.Type)) {
- reporter.Error(MessageSource.Resolver, p.A, "All elements of display must be of the same type (got {0}, but type of previous elements is {1})", p.A.Type, domainType);
- }
+ ConstrainTypes(domainType, p.A.Type, p.A, "All elements of display must be of the same type (got {0}, but type of previous elements is {1})", p.A.Type, domainType);
ResolveExpression(p.B, opts);
Contract.Assert(p.B.Type != null); // follows from postcondition of ResolveExpression
- if (!UnifyTypes(rangeType, p.B.Type)) {
- reporter.Error(MessageSource.Resolver, p.B, "All elements of display must be of the same type (got {0}, but type of previous elements is {1})", p.B.Type, rangeType);
- }
+ ConstrainTypes(rangeType, p.B.Type, p.B, "All elements of display must be of the same type (got {0}, but type of previous elements is {1})", p.B.Type, rangeType);
}
expr.Type = new MapType(e.Finite, domainType, rangeType);
} else if (expr is NameSegment) {
@@ -7192,17 +7538,13 @@ namespace Microsoft.Dafny ResolveExpression(e.Array, opts);
Contract.Assert(e.Array.Type != null); // follows from postcondition of ResolveExpression
Type elementType = new InferredTypeProxy();
- if (!UnifyTypes(e.Array.Type, ResolvedArrayType(e.Array.tok, e.Indices.Count, elementType, opts.codeContext))) {
- reporter.Error(MessageSource.Resolver, e.Array, "array selection requires an array{0} (got {1})", e.Indices.Count, e.Array.Type);
- }
+ ConstrainTypes(e.Array.Type, ResolvedArrayType(e.Array.tok, e.Indices.Count, elementType, opts.codeContext), e.Array, "array selection requires an array{0} (got {1})", e.Indices.Count, e.Array.Type);
int i = 0;
foreach (Expression idx in e.Indices) {
Contract.Assert(idx != null);
ResolveExpression(idx, opts);
Contract.Assert(idx.Type != null); // follows from postcondition of ResolveExpression
- if (!UnifyTypes(idx.Type, new OperationTypeProxy(true, false, false, false, false, false))) {
- reporter.Error(MessageSource.Resolver, idx, "array selection requires integer-based numeric indices (got {0} for index {1})", idx.Type, i);
- }
+ ConstrainTypes(idx.Type, new OperationTypeProxy(true, false, false, false, false, false), idx, "array selection requires integer-based numeric indices (got {0} for index {1})", idx.Type, i);
i++;
}
e.Type = elementType;
@@ -7217,44 +7559,28 @@ namespace Microsoft.Dafny if (UnifyTypes(e.Seq.Type, new SeqType(elementType))) {
ResolveExpression(e.Index, opts);
Contract.Assert(e.Index.Type != null); // follows from postcondition of ResolveExpression
- if (!UnifyTypes(e.Index.Type, Type.Int)) {
- reporter.Error(MessageSource.Resolver, e.Index, "sequence update requires integer index (got {0})", e.Index.Type);
- }
+ ConstrainTypes(e.Index.Type, Type.Int, e.Index, "sequence update requires integer index (got {0})", e.Index.Type);
ResolveExpression(e.Value, opts);
Contract.Assert(e.Value.Type != null); // follows from postcondition of ResolveExpression
- if (!UnifyTypes(e.Value.Type, elementType)) {
- reporter.Error(MessageSource.Resolver, e.Value, "sequence update requires the value to have the element type of the sequence (got {0})", e.Value.Type);
- }
+ ConstrainTypes(e.Value.Type, elementType, e.Value, "sequence update requires the value to have the element type of the sequence (got {0})", e.Value.Type);
expr.Type = e.Seq.Type;
} else if (UnifyTypes(e.Seq.Type, new MapType(true, domainType, rangeType))) {
ResolveExpression(e.Index, opts);
- if (!UnifyTypes(e.Index.Type, domainType)) {
- reporter.Error(MessageSource.Resolver, e.Index, "map update requires domain element to be of type {0} (got {1})", domainType, e.Index.Type);
- }
+ ConstrainTypes(e.Index.Type, domainType, e.Index, "map update requires domain element to be of type {0} (got {1})", domainType, e.Index.Type);
ResolveExpression(e.Value, opts);
- if (!UnifyTypes(e.Value.Type, rangeType)) {
- reporter.Error(MessageSource.Resolver, e.Value, "map update requires the value to have the range type {0} (got {1})", rangeType, e.Value.Type);
- }
+ ConstrainTypes(e.Value.Type, rangeType, e.Value, "map update requires the value to have the range type {0} (got {1})", rangeType, e.Value.Type);
expr.Type = e.Seq.Type;
} else if (UnifyTypes(e.Seq.Type, new MapType(false, domainType, rangeType))) {
ResolveExpression(e.Index, opts);
- if (!UnifyTypes(e.Index.Type, domainType)) {
- reporter.Error(MessageSource.Resolver, e.Index, "imap update requires domain element to be of type {0} (got {1})", domainType, e.Index.Type);
- }
+ ConstrainTypes(e.Index.Type, domainType, e.Index, "imap update requires domain element to be of type {0} (got {1})", domainType, e.Index.Type);
ResolveExpression(e.Value, opts);
- if (!UnifyTypes(e.Value.Type, rangeType)) {
- reporter.Error(MessageSource.Resolver, e.Value, "imap update requires the value to have the range type {0} (got {1})", rangeType, e.Value.Type);
- }
+ ConstrainTypes(e.Value.Type, rangeType, e.Value, "imap update requires the value to have the range type {0} (got {1})", rangeType, e.Value.Type);
expr.Type = e.Seq.Type;
} else if (UnifyTypes(e.Seq.Type, new MultiSetType(elementType))) {
ResolveExpression(e.Index, opts);
- if (!UnifyTypes(e.Index.Type, elementType)) {
- reporter.Error(MessageSource.Resolver, e.Index, "multiset update requires domain element to be of type {0} (got {1})", elementType, e.Index.Type);
- }
+ ConstrainTypes(e.Index.Type, elementType, e.Index, "multiset update requires domain element to be of type {0} (got {1})", elementType, e.Index.Type);
ResolveExpression(e.Value, opts);
- if (!UnifyTypes(e.Value.Type, new OperationTypeProxy(true, false, false, false, false, false))) {
- reporter.Error(MessageSource.Resolver, e.Value, "multiset update requires integer-based numeric value (got {0})", e.Value.Type);
- }
+ ConstrainTypes(e.Value.Type, new OperationTypeProxy(true, false, false, false, false, false), e.Value, "multiset update requires integer-based numeric value (got {0})", e.Value.Type);
expr.Type = e.Seq.Type;
} else if (e.Seq.Type.IsDatatype) {
@@ -7363,9 +7689,7 @@ namespace Microsoft.Dafny reporter.Error(MessageSource.Resolver, e.tok, "wrong number of arguments to function application (function type '{0}' expects {1}, got {2})", fnType, fnType.Arity, e.Args.Count);
} else {
for (var i = 0; i < fnType.Arity; i++) {
- if (!UnifyTypes(fnType.Args[i], e.Args[i].Type)) {
- reporter.Error(MessageSource.Resolver, e.Args[i].tok, "type mismatch for argument {0} (function expects {1}, got {2})", i, fnType.Args[i], e.Args[i].Type);
- }
+ ConstrainTypes(fnType.Args[i], e.Args[i].Type, e.Args[i].tok, "type mismatch for argument {0} (function expects {1}, got {2})", i, fnType.Args[i], e.Args[i].Type);
}
}
expr.Type = fnType == null ? new InferredTypeProxy() : fnType.Result;
@@ -7392,15 +7716,11 @@ namespace Microsoft.Dafny Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression
switch (e.Op) {
case UnaryOpExpr.Opcode.Not:
- if (!UnifyTypes(e.E.Type, Type.Bool)) {
- reporter.Error(MessageSource.Resolver, expr, "logical negation expects a boolean argument (instead got {0})", e.E.Type);
- }
+ ConstrainTypes(e.E.Type, Type.Bool, expr, "logical negation expects a boolean argument (instead got {0})", e.E.Type);
expr.Type = Type.Bool;
break;
case UnaryOpExpr.Opcode.Cardinality:
- if (!UnifyTypes(e.E.Type, new CollectionTypeProxy(new InferredTypeProxy(), false, false))) {
- reporter.Error(MessageSource.Resolver, expr, "size operator expects a collection argument (instead got {0})", e.E.Type);
- }
+ ConstrainTypes(e.E.Type, new CollectionTypeProxy(new InferredTypeProxy(), false, false), expr, "size operator expects a collection argument (instead got {0})", e.E.Type);
expr.Type = Type.Int;
break;
case UnaryOpExpr.Opcode.Fresh:
@@ -7433,13 +7753,9 @@ namespace Microsoft.Dafny ResolveType(e.tok, e.ToType, opts.codeContext, new ResolveTypeOption(ResolveTypeOptionEnum.DontInfer), null);
ResolveExpression(e.E, opts);
if (e.ToType.IsNumericBased(Type.NumericPersuation.Int)) {
- if (!UnifyTypes(e.E.Type, new OperationTypeProxy(true, true, false, false, false, false))) {
- reporter.Error(MessageSource.Resolver, expr, "type conversion to an int-based type is allowed only from numeric types (got {0})", e.E.Type);
- }
+ ConstrainTypes(e.E.Type, new OperationTypeProxy(true, true, false, false, false, false), expr, "type conversion to an int-based type is allowed only from numeric types (got {0})", e.E.Type);
} else if (e.ToType.IsNumericBased(Type.NumericPersuation.Real)) {
- if (!UnifyTypes(e.E.Type, new OperationTypeProxy(true, true, false, false, false, false))) {
- reporter.Error(MessageSource.Resolver, expr, "type conversion to a real-based type is allowed only from numeric types (got {0})", e.E.Type);
- }
+ ConstrainTypes(e.E.Type, new OperationTypeProxy(true, true, false, false, false, false), expr, "type conversion to a real-based type is allowed only from numeric types (got {0})", e.E.Type);
} else {
reporter.Error(MessageSource.Resolver, expr, "type conversions are not supported to this type (got {0})", e.ToType);
}
@@ -7457,12 +7773,8 @@ namespace Microsoft.Dafny case BinaryExpr.Opcode.Exp:
case BinaryExpr.Opcode.And:
case BinaryExpr.Opcode.Or:
- if (!UnifyTypes(e.E0.Type, Type.Bool)) {
- reporter.Error(MessageSource.Resolver, expr, "first argument to {0} must be of type bool (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type);
- }
- if (!UnifyTypes(e.E1.Type, Type.Bool)) {
- reporter.Error(MessageSource.Resolver, expr, "second argument to {0} must be of type bool (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E1.Type);
- }
+ ConstrainTypes(e.E0.Type, Type.Bool, expr, "first argument to {0} must be of type bool (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type);
+ ConstrainTypes(e.E1.Type, Type.Bool, expr, "second argument to {0} must be of type bool (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E1.Type);
expr.Type = Type.Bool;
break;
@@ -7489,9 +7801,7 @@ namespace Microsoft.Dafny case BinaryExpr.Opcode.Disjoint:
// TODO: the error messages are backwards from what (ideally) they should be. this is necessary because UnifyTypes can't backtrack.
- if (!UnifyTypes(e.E0.Type, e.E1.Type)) {
- reporter.Error(MessageSource.Resolver, expr, "arguments must have the same type (got {0} and {1})", e.E0.Type, e.E1.Type);
- }
+ ConstrainTypes(e.E0.Type, e.E1.Type, expr, "arguments must have the same type (got {0} and {1})", e.E0.Type, e.E1.Type);
if (!UnifyTypes(e.E0.Type, new SetType(true, new InferredTypeProxy())) &&
!UnifyTypes(e.E0.Type, new MultiSetType(new InferredTypeProxy())) &&
!UnifyTypes(e.E0.Type, new MapType(true, new InferredTypeProxy(), new InferredTypeProxy()))) {
@@ -7504,34 +7814,25 @@ namespace Microsoft.Dafny case BinaryExpr.Opcode.Le:
case BinaryExpr.Opcode.Add: {
if (e.Op == BinaryExpr.Opcode.Lt && (e.E0.Type.NormalizeExpand().IsIndDatatype || e.E0.Type.IsTypeParameter)) {
- if (UnifyTypes(e.E1.Type, new DatatypeProxy(false, false))) {
+ if (ConstrainTypes(e.E1.Type, new DatatypeProxy(false, false), expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E1.Type)) {
e.ResolvedOp = BinaryExpr.ResolvedOpcode.RankLt;
- } else {
- reporter.Error(MessageSource.Resolver, expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E1.Type);
}
expr.Type = Type.Bool;
} else if (e.Op == BinaryExpr.Opcode.Lt && e.E1.Type.NormalizeExpand().IsIndDatatype) {
- if (UnifyTypes(e.E0.Type, new DatatypeProxy(false, true))) {
+ if (ConstrainTypes(e.E0.Type, new DatatypeProxy(false, true), expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E0.Type)) {
e.ResolvedOp = BinaryExpr.ResolvedOpcode.RankLt;
- } else {
- reporter.Error(MessageSource.Resolver, expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E0.Type);
}
expr.Type = Type.Bool;
} else {
- bool err = false;
bool isComparison = e.Op != BinaryExpr.Opcode.Add;
- if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(true, true, isComparison, true, true, true))) {
- reporter.Error(MessageSource.Resolver, expr, "arguments to {0} must be of a numeric type{2} or a collection type (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type,
- isComparison ? ", char," : "");
- err = true;
- }
- if (!UnifyTypes(e.E1.Type, e.E0.Type)) {
- reporter.Error(MessageSource.Resolver, expr, "arguments to {0} must have the same type (got {1} and {2})", BinaryExpr.OpcodeString(e.Op), e.E0.Type, e.E1.Type);
- err = true;
- }
+ var good0 = ConstrainTypes(e.E0.Type, new OperationTypeProxy(true, true, isComparison, true, true, true),
+ expr, "arguments to {0} must be of a numeric type{2} or a collection type (instead got {1})",
+ BinaryExpr.OpcodeString(e.Op), e.E0.Type, isComparison ? ", char," : "");
+ var good1 = ConstrainTypes(e.E1.Type, e.E0.Type,
+ expr, "arguments to {0} must have the same type (got {1} and {2})", BinaryExpr.OpcodeString(e.Op), e.E0.Type, e.E1.Type);
if (isComparison) {
expr.Type = Type.Bool;
- } else if (!err) {
+ } else if (good0 && good1) {
expr.Type = e.E0.Type;
}
}
@@ -7543,34 +7844,24 @@ namespace Microsoft.Dafny case BinaryExpr.Opcode.Gt:
case BinaryExpr.Opcode.Ge: {
if (e.Op == BinaryExpr.Opcode.Gt && e.E0.Type.NormalizeExpand().IsIndDatatype) {
- if (UnifyTypes(e.E1.Type, new DatatypeProxy(false, true))) {
+ if (ConstrainTypes(e.E1.Type, new DatatypeProxy(false, true), expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E1.Type)) {
e.ResolvedOp = BinaryExpr.ResolvedOpcode.RankGt;
- } else {
- reporter.Error(MessageSource.Resolver, expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E1.Type);
}
expr.Type = Type.Bool;
} else if (e.Op == BinaryExpr.Opcode.Gt && (e.E1.Type.NormalizeExpand().IsIndDatatype || e.E1.Type.IsTypeParameter)) {
- if (UnifyTypes(e.E0.Type, new DatatypeProxy(false, false))) {
+ if (ConstrainTypes(e.E0.Type, new DatatypeProxy(false, false), expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E0.Type)) {
e.ResolvedOp = BinaryExpr.ResolvedOpcode.RankGt;
- } else {
- reporter.Error(MessageSource.Resolver, expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E0.Type);
}
expr.Type = Type.Bool;
} else {
- bool err = false;
bool isComparison = e.Op == BinaryExpr.Opcode.Gt || e.Op == BinaryExpr.Opcode.Ge;
- if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(true, true, isComparison, false, true, true))) {
- reporter.Error(MessageSource.Resolver, expr, "arguments to {0} must be of a numeric type{2} or a set type (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type,
- isComparison ? ", char, " : "");
- err = true;
- }
- if (!UnifyTypes(e.E1.Type, e.E0.Type)) {
- reporter.Error(MessageSource.Resolver, expr, "arguments to {0} must have the same type (got {1} and {2})", BinaryExpr.OpcodeString(e.Op), e.E0.Type, e.E1.Type);
- err = true;
- }
+ var good0 = ConstrainTypes(e.E0.Type, new OperationTypeProxy(true, true, isComparison, false, true, true),
+ expr, "arguments to {0} must be of a numeric type{2} or a set type (instead got {1})",
+ BinaryExpr.OpcodeString(e.Op), e.E0.Type, isComparison ? ", char, " : "");
+ var good1 = ConstrainTypes(e.E1.Type, e.E0.Type, expr, "arguments to {0} must have the same type (got {1} and {2})", BinaryExpr.OpcodeString(e.Op), e.E0.Type, e.E1.Type);
if (isComparison) {
expr.Type = Type.Bool;
- } else if (!err) {
+ } else if (good0 && good1) {
expr.Type = e.E0.Type;
}
}
@@ -7579,29 +7870,23 @@ namespace Microsoft.Dafny case BinaryExpr.Opcode.In:
case BinaryExpr.Opcode.NotIn:
- if (!UnifyTypes(e.E1.Type, new CollectionTypeProxy(e.E0.Type, true, true))) {
- reporter.Error(MessageSource.Resolver, expr, "second argument to \"{0}\" must be a set, multiset, or sequence with elements of type {1}, or a map with domain {1} (instead got {2})", BinaryExpr.OpcodeString(e.Op), e.E0.Type, e.E1.Type);
- }
+ ConstrainTypes(e.E1.Type, new CollectionTypeProxy(e.E0.Type, true, true), expr, "second argument to \"{0}\" must be a set, multiset, or sequence with elements of type {1}, or a map with domain {1} (instead got {2})", BinaryExpr.OpcodeString(e.Op), e.E0.Type, e.E1.Type);
expr.Type = Type.Bool;
break;
case BinaryExpr.Opcode.Div:
- if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(true, true, false, false, false, false))) {
- reporter.Error(MessageSource.Resolver, expr, "first argument to {0} must be of numeric type (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type);
- }
- if (!UnifyTypes(e.E1.Type, e.E0.Type)) {
- reporter.Error(MessageSource.Resolver, expr, "arguments to {0} must have the same type (got {1} and {2})", BinaryExpr.OpcodeString(e.Op), e.E0.Type, e.E1.Type);
- }
+ ConstrainTypes(e.E0.Type, new OperationTypeProxy(true, true, false, false, false, false),
+ expr, "first argument to {0} must be of numeric type (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type);
+ ConstrainTypes(e.E1.Type, e.E0.Type,
+ expr, "arguments to {0} must have the same type (got {1} and {2})", BinaryExpr.OpcodeString(e.Op), e.E0.Type, e.E1.Type);
expr.Type = e.E0.Type;
break;
case BinaryExpr.Opcode.Mod:
- if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(true, false, false, false, false, false))) {
- reporter.Error(MessageSource.Resolver, expr, "first argument to {0} must be of type int (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type);
- }
- if (!UnifyTypes(e.E1.Type, e.E0.Type)) {
- reporter.Error(MessageSource.Resolver, expr, "second argument to {0} must be of type int (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E1.Type);
- }
+ ConstrainTypes(e.E0.Type, new OperationTypeProxy(true, false, false, false, false, false),
+ expr, "first argument to {0} must be of type int (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type);
+ ConstrainTypes(e.E1.Type, e.E0.Type,
+ expr, "second argument to {0} must be of type int (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E1.Type);
expr.Type = e.E0.Type;
break;
@@ -7619,15 +7904,12 @@ namespace Microsoft.Dafny switch (e.Op) {
case TernaryExpr.Opcode.PrefixEqOp:
case TernaryExpr.Opcode.PrefixNeqOp:
- if (!UnifyTypes(e.E0.Type, Type.Int)) {
- reporter.Error(MessageSource.Resolver, e.E0, "prefix-equality limit argument must be an integer expression (got {0})", e.E0.Type);
- }
- if (!UnifyTypes(e.E1.Type, new DatatypeProxy(true))) {
- reporter.Error(MessageSource.Resolver, expr, "arguments to prefix equality must be codatatypes (instead of {0})", e.E1.Type);
- }
- if (!UnifyTypes(e.E1.Type, e.E2.Type)) {
- reporter.Error(MessageSource.Resolver, expr, "arguments must have the same type (got {0} and {1})", e.E1.Type, e.E2.Type);
- }
+ ConstrainTypes(e.E0.Type, Type.Int,
+ e.E0, "prefix-equality limit argument must be an integer expression (got {0})", e.E0.Type);
+ ConstrainTypes(e.E1.Type, new DatatypeProxy(true),
+ expr, "arguments to prefix equality must be codatatypes (instead of {0})", e.E1.Type);
+ ConstrainTypes(e.E1.Type, e.E2.Type,
+ expr, "arguments must have the same type (got {0} and {1})", e.E1.Type, e.E2.Type);
expr.Type = Type.Bool;
break;
default:
@@ -7676,16 +7958,11 @@ namespace Microsoft.Dafny }
foreach (var rhs in e.RHSs) {
ResolveExpression(rhs, opts);
- if (!UnifyTypes(rhs.Type, Type.Bool)) {
- reporter.Error(MessageSource.Resolver, rhs.tok, "type of RHS of let-such-that expression must be boolean (got {0})", rhs.Type);
- }
- }
- if (!opts.DontCareAboutCompilation && !e.BoundVars.All(bv => bv.IsGhost)) {
- needFiniteBoundsChecks_LetSuchThatExpr.Add(e);
+ ConstrainTypes(rhs.Type, Type.Bool, rhs.tok, "type of RHS of let-such-that expression must be boolean (got {0})", rhs.Type);
}
}
ResolveExpression(e.Body, opts);
- ResolveAttributes(e.Attributes, new ResolveOpts(opts, true));
+ ResolveAttributes(e.Attributes, opts);
scope.PopMarker();
expr.Type = e.Body.Type;
@@ -7712,47 +7989,20 @@ namespace Microsoft.Dafny reporter.Error(MessageSource.Resolver, expr, "a quantifier cannot quantify over types. Possible fix: use the experimental attribute :typeQuantifier");
}
if (e.Range != null) {
- ResolveExpression(e.Range, new ResolveOpts(opts, true));
+ ResolveExpression(e.Range, opts);
Contract.Assert(e.Range.Type != null); // follows from postcondition of ResolveExpression
- if (!UnifyTypes(e.Range.Type, Type.Bool)) {
- reporter.Error(MessageSource.Resolver, expr, "range of quantifier must be of type bool (instead got {0})", e.Range.Type);
- }
+ ConstrainTypes(e.Range.Type, Type.Bool, expr, "range of quantifier must be of type bool (instead got {0})", e.Range.Type);
}
- ResolveExpression(e.Term, new ResolveOpts(opts, true));
+ ResolveExpression(e.Term, opts);
Contract.Assert(e.Term.Type != null); // follows from postcondition of ResolveExpression
- if (!UnifyTypes(e.Term.Type, Type.Bool)) {
- reporter.Error(MessageSource.Resolver, expr, "body of quantifier must be of type bool (instead got {0})", e.Term.Type);
- }
+ ConstrainTypes(e.Term.Type, Type.Bool, expr, "body of quantifier must be of type bool (instead got {0})", e.Term.Type);
// Since the body is more likely to infer the types of the bound variables, resolve it
// first (above) and only then resolve the attributes (below).
- ResolveAttributes(e.Attributes, new ResolveOpts(opts, true));
+ ResolveAttributes(e.Attributes, opts);
scope.PopMarker();
allTypeParameters.PopMarker();
expr.Type = Type.Bool;
- if (prevErrorCount == reporter.Count(ErrorLevel.Error)) {
- CheckTypeInference(e.LogicalBody()); // we need to resolve operators before the call to DiscoverBounds
- List<BoundVar> missingBounds;
- e.Bounds = DiscoverBestBounds_MultipleVars(e.BoundVars, e.LogicalBody(), e is ExistsExpr, true, out missingBounds);
- if (missingBounds.Count != 0) {
- // Report errors here about quantifications that depend on the allocation state.
- var mb = missingBounds;
- if (opts.codeContext is Function) {
- mb = new List<BoundVar>(); // (who cares if we allocate another array; this happens only in the case of a resolution error anyhow)
- foreach (var bv in missingBounds) {
- if (bv.Type.IsRefType) {
- reporter.Error(MessageSource.Resolver, expr, "a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of '{0}'", bv.Name);
- } else {
- mb.Add(bv);
- }
- }
- }
- if (mb.Count != 0) {
- e.MissingBounds = mb;
- }
- }
- }
-
} else if (expr is SetComprehension) {
var e = (SetComprehension)expr;
int prevErrorCount = reporter.Count(ErrorLevel.Error);
@@ -7763,22 +8013,14 @@ namespace Microsoft.Dafny }
ResolveExpression(e.Range, opts);
Contract.Assert(e.Range.Type != null); // follows from postcondition of ResolveExpression
- if (!UnifyTypes(e.Range.Type, Type.Bool)) {
- reporter.Error(MessageSource.Resolver, expr, "range of comprehension must be of type bool (instead got {0})", e.Range.Type);
- }
+ ConstrainTypes(e.Range.Type, Type.Bool, expr, "range of comprehension must be of type bool (instead got {0})", e.Range.Type);
ResolveExpression(e.Term, opts);
Contract.Assert(e.Term.Type != null); // follows from postcondition of ResolveExpression
- ResolveAttributes(e.Attributes, new ResolveOpts(opts, true));
+ ResolveAttributes(e.Attributes, opts);
scope.PopMarker();
expr.Type = new SetType(e.Finite, e.Term.Type);
- if (opts.DontCareAboutCompilation && (e.Term.Type.IsRefType || e.Term.Type.IsBoolType) || e.Term.Type.IsCharType) {
- // ok, term type is finite and we're in a ghost context
- } else {
- needFiniteBoundsChecks_SetComprehension.Add(e);
- }
-
} else if (expr is MapComprehension) {
var e = (MapComprehension)expr;
int prevErrorCount = reporter.Count(ErrorLevel.Error);
@@ -7792,29 +8034,14 @@ namespace Microsoft.Dafny }
ResolveExpression(e.Range, opts);
Contract.Assert(e.Range.Type != null); // follows from postcondition of ResolveExpression
- if (!UnifyTypes(e.Range.Type, Type.Bool)) {
- reporter.Error(MessageSource.Resolver, expr, "range of comprehension must be of type bool (instead got {0})", e.Range.Type);
- }
+ ConstrainTypes(e.Range.Type, Type.Bool, expr, "range of comprehension must be of type bool (instead got {0})", e.Range.Type);
ResolveExpression(e.Term, opts);
Contract.Assert(e.Term.Type != null); // follows from postcondition of ResolveExpression
- ResolveAttributes(e.Attributes, new ResolveOpts(opts, true));
+ ResolveAttributes(e.Attributes, opts);
scope.PopMarker();
expr.Type = new MapType(e.Finite, e.BoundVars[0].Type, e.Term.Type);
- if (prevErrorCount == reporter.Count(ErrorLevel.Error)) {
- 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, expr, "a map comprehension must produce a finite domain, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name);
- }
- }
- }
- }
} else if (expr is LambdaExpr) {
var e = (LambdaExpr)expr;
int prevErrorCount = reporter.Count(ErrorLevel.Error);
@@ -7827,13 +8054,11 @@ namespace Microsoft.Dafny if (e.Range != null) {
ResolveExpression(e.Range, opts);
Contract.Assert(e.Range.Type != null); // follows from postcondition of ResolveExpression
- if (!UnifyTypes(e.Range.Type, Type.Bool)) {
- reporter.Error(MessageSource.Resolver, expr, "Precondition must be boolean (got {0})", e.Range.Type);
- }
+ ConstrainTypes(e.Range.Type, Type.Bool, expr, "Precondition must be boolean (got {0})", e.Range.Type);
}
foreach (var read in e.Reads) {
- ResolveFrameExpression(read, true, false, opts.codeContext);
+ ResolveFrameExpression(read, true, opts.codeContext);
}
ResolveExpression(e.Term, opts);
@@ -7845,7 +8070,7 @@ namespace Microsoft.Dafny } else if (expr is StmtExpr) {
var e = (StmtExpr)expr;
int prevErrorCount = reporter.Count(ErrorLevel.Error);
- ResolveStatement(e.S, true, opts.codeContext);
+ ResolveStatement(e.S, opts.codeContext);
if (reporter.Count(ErrorLevel.Error) == prevErrorCount) {
var r = e.S as UpdateStmt;
if (r != null && r.ResolvedStatements.Count == 1) {
@@ -7867,13 +8092,9 @@ namespace Microsoft.Dafny Contract.Assert(e.Thn.Type != null); // follows from postcondition of ResolveExpression
ResolveExpression(e.Els, opts);
Contract.Assert(e.Els.Type != null); // follows from postcondition of ResolveExpression
- if (!UnifyTypes(e.Test.Type, Type.Bool)) {
- reporter.Error(MessageSource.Resolver, expr, "guard condition in if-then-else expression must be a boolean (instead got {0})", e.Test.Type);
- }
- if (UnifyTypes(e.Thn.Type, e.Els.Type)) {
+ ConstrainTypes(e.Test.Type, Type.Bool, expr, "guard condition in if-then-else expression must be a boolean (instead got {0})", e.Test.Type);
+ if (ConstrainTypes(e.Thn.Type, e.Els.Type, expr, "the two branches of an if-then-else expression must have the same type (got {0} and {1})", e.Thn.Type, e.Els.Type)) {
expr.Type = e.Thn.Type;
- } else {
- reporter.Error(MessageSource.Resolver, expr, "the two branches of an if-then-else expression must have the same type (got {0} and {1})", e.Thn.Type, e.Els.Type);
}
} else if (expr is MatchExpr) {
@@ -7955,16 +8176,15 @@ namespace Microsoft.Dafny if (ctor != null && i < ctor.Formals.Count) {
Formal formal = ctor.Formals[i];
Type st = SubstType(formal.Type, subst);
- if (!UnifyTypes(v.Type, st)) {
- reporter.Error(MessageSource.Resolver, expr, "the declared type of the formal ({0}) does not agree with the corresponding type in the constructor's signature ({1})", v.Type, st);
- }
+ ConstrainTypes(v.Type, st,
+ expr, "the declared type of the formal ({0}) does not agree with the corresponding type in the constructor's signature ({1})", v.Type, st);
v.IsGhost = formal.IsGhost;
// update the type of the boundvars in the MatchCaseToken
if (v.tok is MatchCaseToken) {
MatchCaseToken mt = (MatchCaseToken)v.tok;
foreach (Tuple<IToken, BoundVar, bool> entry in mt.varList) {
- UnifyTypes(entry.Item2.Type, v.Type);
+ UnifyTypes(entry.Item2.Type, v.Type); // TODO: What to do if this unification fails? Or can it? --KRML
}
}
}
@@ -7982,9 +8202,7 @@ namespace Microsoft.Dafny }
Contract.Assert(mc.Body.Type != null); // follows from postcondition of ResolveExpression
- if (!UnifyTypes(expr.Type, mc.Body.Type)) {
- reporter.Error(MessageSource.Resolver, mc.Body.tok, "type of case bodies do not agree (found {0}, previous types {1})", mc.Body.Type, expr.Type);
- }
+ ConstrainTypes(expr.Type, mc.Body.Type, mc.Body.tok, "type of case bodies do not agree (found {0}, previous types {1})", mc.Body.Type, expr.Type);
scope.PopMarker();
}
if (dtd != null && memberNamesUsed.Count != dtd.Ctors.Count) {
@@ -8318,9 +8536,7 @@ namespace Microsoft.Dafny // this is a simple resolution
var v = pat.Var;
ResolveType(v.tok, v.Type, context, ResolveTypeOptionEnum.InferTypeProxies, null);
- if (!UnifyTypes(v.Type, sourceType)) {
- reporter.Error(MessageSource.Resolver, v.tok, "type of corresponding source/RHS ({0}) does not match type of bound variable ({1})", sourceType, v.Type);
- }
+ ConstrainTypes(v.Type, sourceType, v.tok, "type of corresponding source/RHS ({0}) does not match type of bound variable ({1})", sourceType, v.Type);
pat.AssembleExpr(null);
} else if (dtd == null) {
reporter.Error(MessageSource.Resolver, pat.tok, "to use a pattern, the type of the source/RHS expression must be a datatype (instead found {0})", sourceType);
@@ -9038,9 +9254,8 @@ namespace Microsoft.Dafny reporter.Error(MessageSource.Resolver, e.tok, "wrong number of arguments to function application ({0} expects {1}, got {2})", what, fnType.Arity, e.Args.Count);
} else {
for (var i = 0; i < fnType.Arity; i++) {
- if (!UnifyTypes(fnType.Args[i], e.Args[i].Type)) {
- reporter.Error(MessageSource.Resolver, e.Args[i].tok, "type mismatch for argument {0} (function expects {1}, got {2})", i, fnType.Args[i], e.Args[i].Type);
- }
+ ConstrainTypes(fnType.Args[i], e.Args[i].Type,
+ e.Args[i].tok, "type mismatch for argument {0} (function expects {1}, got {2})", i, fnType.Args[i], e.Args[i].Type);
}
if (errorCount != reporter.Count(ErrorLevel.Error)) {
// do nothing else; error has been reported
@@ -9066,9 +9281,7 @@ namespace Microsoft.Dafny ResolveExpression(farg, opts);
Contract.Assert(farg.Type != null); // follows from postcondition of ResolveExpression
Type s = SubstType(callee.Formals[i].Type, rr.TypeArgumentSubstitutions);
- if (!UnifyTypes(farg.Type, s)) {
- reporter.Error(MessageSource.Resolver, rr, "incorrect type of function argument {0} (expected {1}, got {2})", i, s, farg.Type);
- }
+ ConstrainTypes(farg.Type, s, rr, "incorrect type of function argument {0} (expected {1}, got {2})", i, s, farg.Type);
}
rr.Type = SubstType(callee.ResultType, rr.TypeArgumentSubstitutions);
// further bookkeeping
@@ -9124,9 +9337,7 @@ namespace Microsoft.Dafny Contract.Assert(arg.Type != null); // follows from postcondition of ResolveExpression
if (formal != null) {
Type st = SubstType(formal.Type, subst);
- if (!UnifyTypes(arg.Type, st)) {
- reporter.Error(MessageSource.Resolver, arg.tok, "incorrect type of datatype constructor argument (found {0}, expected {1})", arg.Type, st);
- }
+ ConstrainTypes(arg.Type, st, arg.tok, "incorrect type of datatype constructor argument (found {0}, expected {1})", arg.Type, st);
}
j++;
}
@@ -9162,7 +9373,7 @@ namespace Microsoft.Dafny /// Generate an error for every non-ghost feature used in "expr".
/// Requires "expr" to have been successfully resolved.
/// </summary>
- void CheckIsNonGhost(Expression expr) {
+ void CheckIsCompilable(Expression expr) {
Contract.Requires(expr != null);
Contract.Requires(expr.WasResolved()); // this check approximates the requirement that "expr" be resolved
@@ -9188,10 +9399,10 @@ namespace Microsoft.Dafny return;
}
// function is okay, so check all NON-ghost arguments
- CheckIsNonGhost(e.Receiver);
+ CheckIsCompilable(e.Receiver);
for (int i = 0; i < e.Function.Formals.Count; i++) {
if (!e.Function.Formals[i].IsGhost) {
- CheckIsNonGhost(e.Args[i]);
+ CheckIsCompilable(e.Args[i]);
}
}
}
@@ -9203,7 +9414,7 @@ namespace Microsoft.Dafny // 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) {
- CheckIsNonGhost(e.Arguments[i]);
+ CheckIsCompilable(e.Arguments[i]);
}
}
return;
@@ -9222,7 +9433,7 @@ namespace Microsoft.Dafny } else if (expr is StmtExpr) {
var e = (StmtExpr)expr;
// ignore the statement
- CheckIsNonGhost(e.E);
+ CheckIsCompilable(e.E);
return;
} else if (expr is BinaryExpr) {
@@ -9253,29 +9464,59 @@ namespace Microsoft.Dafny var i = 0;
foreach (var ee in e.RHSs) {
if (!e.LHSs[i].Vars.All(bv => bv.IsGhost)) {
- CheckIsNonGhost(ee);
+ CheckIsCompilable(ee);
}
i++;
}
- CheckIsNonGhost(e.Body);
+ CheckIsCompilable(e.Body);
} else {
Contract.Assert(e.RHSs.Count == 1);
var lhsVarsAreAllGhost = e.BoundVars.All(bv => bv.IsGhost);
if (!lhsVarsAreAllGhost) {
- CheckIsNonGhost(e.RHSs[0]);
+ CheckIsCompilable(e.RHSs[0]);
+ }
+ CheckIsCompilable(e.Body);
+
+ // fill in bounds for this to-be-compiled let-such-that expression
+ Contract.Assert(e.RHSs.Count == 1); // if we got this far, the resolver will have checked this condition successfully
+ var constraint = e.RHSs[0];
+ 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;
}
- CheckIsNonGhost(e.Body);
}
return;
- } else if (expr is QuantifierExpr) {
- var e = (QuantifierExpr)expr;
- Contract.Assert(e.SplitQuantifier == null); // No split quantifiers during resolution
- if (e.MissingBounds != null) {
- foreach (var bv in e.MissingBounds) {
- reporter.Error(MessageSource.Resolver, expr, "quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name);
+ } else if (expr is LambdaExpr) {
+ var e = expr as LambdaExpr;
+ CheckIsCompilable(e.Body);
+ return;
+ } else if (expr is ComprehensionExpr) {
+ var e = (ComprehensionExpr)expr;
+ var uncompilableBoundVars = e.UncompilableBoundVars();
+ if (uncompilableBoundVars.Count != 0) {
+ string what;
+ if (e is SetComprehension) {
+ what = "set comprehensions";
+ } else if (e is MapComprehension) {
+ what = "map comprehensions";
+ } else {
+ Contract.Assume(e is QuantifierExpr); // otherwise, unexpected ComprehensionExpr (since LambdaExpr is handled separately above)
+ Contract.Assert(((QuantifierExpr)e).SplitQuantifier == null); // No split quantifiers during resolution
+ what = "quantifiers";
+ }
+ foreach (var bv in uncompilableBoundVars) {
+ reporter.Error(MessageSource.Resolver, expr, "{0} in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for '{1}'", what, bv.Name);
}
return;
}
+
} else if (expr is MapComprehension) {
var e = (MapComprehension)expr;
if (e.MissingBounds != null && !e.Finite) {
@@ -9285,23 +9526,19 @@ namespace Microsoft.Dafny return;
}
} else if (expr is NamedExpr) {
- if (!moduleInfo.IsGhost)
- CheckIsNonGhost(((NamedExpr)expr).Body);
+ if (!moduleInfo.IsAbstract)
+ CheckIsCompilable(((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;
- } else if (expr is LambdaExpr) {
- var e = expr as LambdaExpr;
- CheckIsNonGhost(e.Body);
+ e.Operands.ForEach(CheckIsCompilable);
return;
}
foreach (var ee in expr.SubExpressions) {
- CheckIsNonGhost(ee);
+ CheckIsCompilable(ee);
}
}
@@ -9361,9 +9598,7 @@ namespace Microsoft.Dafny ResolveExpression(farg, opts);
Contract.Assert(farg.Type != null); // follows from postcondition of ResolveExpression
Type s = SubstType(function.Formals[i].Type, e.TypeArgumentSubstitutions);
- if (!UnifyTypes(farg.Type, s)) {
- reporter.Error(MessageSource.Resolver, e, "incorrect type of function argument {0} (expected {1}, got {2})", i, s, farg.Type);
- }
+ ConstrainTypes(farg.Type, s, e, "incorrect type of function argument {0} (expected {1}, got {2})", i, s, farg.Type);
}
e.Type = SubstType(function.ResultType, e.TypeArgumentSubstitutions);
}
@@ -9416,7 +9651,7 @@ namespace Microsoft.Dafny /// </summary>
public static List<ComprehensionExpr.BoundedPool> DiscoverBestBounds_MultipleVars<VT>(List<VT> bvars, Expression expr, bool polarity, bool onlyFiniteBounds, out List<VT> missingBounds) where VT : IVariable {
foreach (var bv in bvars) {
- var c = TypeConstraint(bv, bv.Type, null);
+ var c = GetImpliedTypeConstraint(bv, bv.Type, null);
expr = polarity ? Expression.CreateAnd(c, expr) : Expression.CreateImplies(c, expr);
}
var all = DiscoverAllBounds_Aux_MultipleVars(bvars, expr, polarity);
@@ -9431,7 +9666,7 @@ namespace Microsoft.Dafny }
public static List<ComprehensionExpr.BoundedPool> DiscoverAllBounds_SingleVar<VT>(VT v, Expression expr) where VT : IVariable {
- expr = Expression.CreateAnd(TypeConstraint(v, v.Type, null), expr);
+ expr = Expression.CreateAnd(GetImpliedTypeConstraint(v, v.Type, null), expr);
return DiscoverAllBounds_Aux_SingleVar(new List<VT> { v }, 0, expr, true);
}
@@ -9458,8 +9693,11 @@ namespace Microsoft.Dafny // Maybe the type itself gives a bound
if (bv.Type.IsBoolType) {
- // easy
bounds.Add(new ComprehensionExpr.BoolBoundedPool());
+ } else if (bv.Type.IsCharType) {
+ bounds.Add(new ComprehensionExpr.CharBoundedPool());
+ } else if (bv.Type.IsRefType) {
+ bounds.Add(new ComprehensionExpr.RefBoundedPool(bv.Type));
} else if (bv.Type.IsIndDatatype && bv.Type.AsIndDatatype.HasFinitePossibleValues) {
bounds.Add(new ComprehensionExpr.DatatypeBoundedPool(bv.Type.AsIndDatatype));
} else if (bv.Type.IsNumericBased(Type.NumericPersuation.Int)) {
@@ -9545,13 +9783,13 @@ namespace Microsoft.Dafny return bounds;
}
- static Expression TypeConstraint(IVariable bv, Type ty, ErrorReporter reporter) {
+ static Expression GetImpliedTypeConstraint(IVariable bv, Type ty, ErrorReporter reporter) {
Contract.Requires(bv != null);
Contract.Requires(ty != null);
ty = ty.NormalizeExpand();
var dd = ty.AsNewtype;
if (dd != null) {
- var c = TypeConstraint(bv, dd.BaseType, reporter);
+ var c = GetImpliedTypeConstraint(bv, dd.BaseType, reporter);
if (dd.Var != null) {
c = Expression.CreateAnd(c, new Translator(reporter).Substitute(dd.Constraint, dd.Var, Expression.CreateIdentExpr(bv)));
}
@@ -9898,17 +10136,14 @@ namespace Microsoft.Dafny Type argType = new InferredTypeProxy();
IndexableTypeProxy expectedType = new IndexableTypeProxy(domainType, elementType, argType, true, true, true);
- if (!UnifyTypes(e.Seq.Type, expectedType)) {
- reporter.Error(MessageSource.Resolver, e, "sequence/array/multiset/map selection requires a sequence, array, multiset, or map (got {0})", e.Seq.Type);
+ if (!ConstrainTypes(e.Seq.Type, expectedType, e, "sequence/array/multiset/map selection requires a sequence, array, multiset, or map (got {0})", e.Seq.Type)) {
seqErr = true;
}
if (!e.SelectOne) // require sequence or array
{
if (!allowNonUnitArraySelection) {
// require seq
- if (!UnifyTypes(expectedType, new SeqType(new InferredTypeProxy()))) {
- reporter.Error(MessageSource.Resolver, e, "selection requires a sequence (got {0})", e.Seq.Type);
- }
+ ConstrainTypes(expectedType, new SeqType(new InferredTypeProxy()), e, "selection requires a sequence (got {0})", e.Seq.Type);
} else {
if (UnifyTypes(expectedType, new MapType(true, new InferredTypeProxy(), new InferredTypeProxy()))) {
reporter.Error(MessageSource.Resolver, e, "cannot multiselect a map (got {0} as map type)", e.Seq.Type);
@@ -9920,17 +10155,13 @@ namespace Microsoft.Dafny if (e.E0 != null) {
ResolveExpression(e.E0, opts);
Contract.Assert(e.E0.Type != null); // follows from postcondition of ResolveExpression
- if (!UnifyTypes(e.E0.Type, domainType)) {
- reporter.Error(MessageSource.Resolver, e.E0, "sequence/array/multiset/map selection requires {1} indices (got {0})", e.E0.Type, domainType);
- }
+ ConstrainTypes(e.E0.Type, domainType, e.E0, "sequence/array/multiset/map selection requires {1} indices (got {0})", e.E0.Type, domainType);
}
if (e.E1 != null) {
ResolveExpression(e.E1, opts);
Contract.Assert(e.E1.Type != null); // follows from postcondition of ResolveExpression
var domType = e.E0 == null ? domainType : new OperationTypeProxy(true, false, false, false, false, false); // reuse 'domainType' if .E0 did not use it; otherwise, create a new proxy to allow .E1 to be any integer-based numeric type, independent of the integer-based numeric type used by .E0
- if (!UnifyTypes(e.E1.Type, domType)) {
- reporter.Error(MessageSource.Resolver, e.E1, "sequence/array/multiset/map selection requires {1} indices (got {0})", e.E1.Type, domType);
- }
+ ConstrainTypes(e.E1.Type, domType, e.E1, "sequence/array/multiset/map selection requires {1} indices (got {0})", e.E1.Type, domType);
}
if (!seqErr) {
if (e.SelectOne) {
@@ -10106,8 +10337,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));
@@ -10135,11 +10373,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);
@@ -10180,22 +10427,20 @@ namespace Microsoft.Dafny return true; // let-such-that is always ghost
}
} else if (expr is NamedExpr) {
- return moduleInfo.IsGhost ? 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
- if (q != null && q.Bounds.Contains(null)) {
- return true; // the quantifier cannot be compiled if the resolver found no bounds
- }
- return Contract.Exists(expr.SubExpressions, se => UsesSpecFeatures(se));
+ return moduleInfo.IsAbstract ? false : UsesSpecFeatures(((NamedExpr)expr).Body);
+ } else if (expr is QuantifierExpr) {
+ var e = (QuantifierExpr)expr;
+ Contract.Assert(e.SplitQuantifier == null); // No split quantifiers during resolution
+ return e.UncompilableBoundVars().Count != 0;
} else if (expr is SetComprehension) {
var e = (SetComprehension)expr;
- return (e.Range != null && UsesSpecFeatures(e.Range)) || (e.Term != null && UsesSpecFeatures(e.Term));
+ return !e.Finite || e.UncompilableBoundVars().Count != 0 || (e.Range != null && UsesSpecFeatures(e.Range)) || (e.Term != null && UsesSpecFeatures(e.Term));
} else if (expr is MapComprehension) {
var e = (MapComprehension)expr;
- return (UsesSpecFeatures(e.Range)) || (UsesSpecFeatures(e.Term));
+ return !e.Finite || e.UncompilableBoundVars().Count != 0 || UsesSpecFeatures(e.Range) || UsesSpecFeatures(e.Term);
} else if (expr is LambdaExpr) {
- return Contract.Exists(expr.SubExpressions, UsesSpecFeatures);
+ var e = (LambdaExpr)expr;
+ return UsesSpecFeatures(e.Term);
} else if (expr is WildcardExpr) {
return false;
} else if (expr is StmtExpr) {
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..83eb8a73 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(9,26): 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(61,34): 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/CallStmtTests.dfy b/Test/dafny0/CallStmtTests.dfy index 67e66b34..46c466ff 100644 --- a/Test/dafny0/CallStmtTests.dfy +++ b/Test/dafny0/CallStmtTests.dfy @@ -1,23 +1,27 @@ // RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
-method testing1(t: int)
-{
- t := m(); // error: should be checked at the Dafny level, not fall to Boogie.
-}
+module M0 {
+ method testing1(t: int)
+ {
+ t := m(); // error: should be checked at the Dafny level, not fall to Boogie.
+ }
-method m() returns (r: int)
-{
- return 3;
+ method m() returns (r: int)
+ {
+ return 3;
+ }
}
-method testing2()
-{
- var v;
- v := m2(); // error: v needs to be ghost because r is.
-}
+module M1 {
+ method testing2()
+ {
+ var v;
+ v := m2(); // error: v needs to be ghost because r is.
+ }
-method m2() returns (ghost r: int)
-{
- r := 23;
+ method m2() returns (ghost r: int)
+ {
+ r := 23;
+ }
}
diff --git a/Test/dafny0/CallStmtTests.dfy.expect b/Test/dafny0/CallStmtTests.dfy.expect index 8a334754..246b89f8 100644 --- a/Test/dafny0/CallStmtTests.dfy.expect +++ b/Test/dafny0/CallStmtTests.dfy.expect @@ -1,3 +1,3 @@ -CallStmtTests.dfy(6,3): Error: LHS of assignment must denote a mutable variable
-CallStmtTests.dfy(17,10): Error: actual out-parameter 0 is required to be a ghost variable
+CallStmtTests.dfy(7,4): Error: LHS of assignment must denote a mutable variable
+CallStmtTests.dfy(20,11): Error: actual out-parameter 0 is required to be a ghost variable
2 resolution/type errors detected in CallStmtTests.dfy
diff --git a/Test/dafny0/CoPrefix.dfy b/Test/dafny0/CoPrefix.dfy index 0becb24d..3b6bd670 100644 --- a/Test/dafny0/CoPrefix.dfy +++ b/Test/dafny0/CoPrefix.dfy @@ -192,3 +192,35 @@ module Recursion { }
}
}
+
+module PrefixEquality {
+ codatatype Stream<T> = Cons(head: T, Stream)
+
+ colemma Test0(s: Stream, t: Stream)
+ requires s.head == t.head
+ {
+ calc {
+ s;
+ ==#[_k-1]
+ t; // error: this step might not hold
+ ==#[if 2 <= _k then _k-2 else _k-1]
+ s; // error: this step might not hold
+ ==#[0]
+ t;
+ }
+ }
+
+ colemma Test1(s: Stream, t: Stream)
+ requires s == t
+ {
+ calc {
+ s;
+ ==#[_k-1]
+ t;
+ ==#[_k-2] // error: prefix-equality limit must be at least 0
+ s;
+ ==#[0]
+ t;
+ }
+ }
+}
diff --git a/Test/dafny0/CoPrefix.dfy.expect b/Test/dafny0/CoPrefix.dfy.expect index a7295367..b42f2593 100644 --- a/Test/dafny0/CoPrefix.dfy.expect +++ b/Test/dafny0/CoPrefix.dfy.expect @@ -12,6 +12,21 @@ CoPrefix.dfy(176,10): Error: cannot prove termination; try supplying a decreases Execution trace:
(0,0): anon0
(0,0): anon3_Then
+CoPrefix.dfy(205,6): Error: the calculation step between the previous line and this line might not hold
+Execution trace:
+ (0,0): anon0
+ (0,0): anon8_Then
+ (0,0): anon10_Then
+CoPrefix.dfy(207,6): Error: the calculation step between the previous line and this line might not hold
+Execution trace:
+ (0,0): anon0
+ (0,0): anon8_Then
+ (0,0): anon11_Then
+CoPrefix.dfy(220,12): Error: prefix-equality limit must be at least 0
+Execution trace:
+ (0,0): anon0
+ (0,0): anon8_Then
+ (0,0): anon11_Then
CoPrefix.dfy(63,56): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
@@ -47,4 +62,4 @@ Execution trace: (0,0): anon0
(0,0): anon3_Else
-Dafny program verifier finished with 41 verified, 9 errors
+Dafny program verifier finished with 43 verified, 12 errors
diff --git a/Test/dafny0/DiscoverBounds.dfy.expect b/Test/dafny0/DiscoverBounds.dfy.expect index ee816683..34003053 100644 --- a/Test/dafny0/DiscoverBounds.dfy.expect +++ b/Test/dafny0/DiscoverBounds.dfy.expect @@ -1,4 +1,4 @@ -DiscoverBounds.dfy(36,7): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o''
-DiscoverBounds.dfy(39,7): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'r'
-DiscoverBounds.dfy(40,7): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'r''
+DiscoverBounds.dfy(36,7): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'o''
+DiscoverBounds.dfy(39,7): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'r'
+DiscoverBounds.dfy(40,7): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'r''
3 resolution/type errors detected in DiscoverBounds.dfy
diff --git a/Test/dafny0/NonGhostQuantifiers.dfy b/Test/dafny0/NonGhostQuantifiers.dfy index bff1d65b..e522d0fc 100644 --- a/Test/dafny0/NonGhostQuantifiers.dfy +++ b/Test/dafny0/NonGhostQuantifiers.dfy @@ -181,6 +181,12 @@ module DependencyOnAllAllocatedObjects { forall c: SomeClass :: true // error: not allowed to dependend on which objects are allocated
}
+ class SomeClass {
+ var f: int;
+ }
+}
+
+module DependencyOnAllAllocatedObjects_More {
method M()
{
var b := forall c: SomeClass :: c != null ==> c.f == 0; // error: non-ghost code requires bounds
@@ -192,3 +198,4 @@ module DependencyOnAllAllocatedObjects { var f: int;
}
}
+
diff --git a/Test/dafny0/NonGhostQuantifiers.dfy.expect b/Test/dafny0/NonGhostQuantifiers.dfy.expect index 1e2fce17..6b737add 100644 --- a/Test/dafny0/NonGhostQuantifiers.dfy.expect +++ b/Test/dafny0/NonGhostQuantifiers.dfy.expect @@ -6,16 +6,16 @@ NonGhostQuantifiers.dfy(167,4): Error: a quantifier involved in a function defin NonGhostQuantifiers.dfy(171,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
NonGhostQuantifiers.dfy(176,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
NonGhostQuantifiers.dfy(181,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
-NonGhostQuantifiers.dfy(186,13): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'c'
-NonGhostQuantifiers.dfy(16,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'
-NonGhostQuantifiers.dfy(45,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'
-NonGhostQuantifiers.dfy(49,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'd'
-NonGhostQuantifiers.dfy(53,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'
-NonGhostQuantifiers.dfy(77,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'i'
-NonGhostQuantifiers.dfy(81,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
-NonGhostQuantifiers.dfy(91,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
-NonGhostQuantifiers.dfy(106,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
-NonGhostQuantifiers.dfy(114,10): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'y'
-NonGhostQuantifiers.dfy(123,8): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'x'
+NonGhostQuantifiers.dfy(192,13): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'c'
+NonGhostQuantifiers.dfy(16,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'n'
+NonGhostQuantifiers.dfy(45,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'n'
+NonGhostQuantifiers.dfy(49,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'd'
+NonGhostQuantifiers.dfy(53,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'n'
+NonGhostQuantifiers.dfy(77,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'i'
+NonGhostQuantifiers.dfy(81,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'j'
+NonGhostQuantifiers.dfy(91,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'j'
+NonGhostQuantifiers.dfy(106,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'j'
+NonGhostQuantifiers.dfy(114,10): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'y'
+NonGhostQuantifiers.dfy(123,8): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'x'
NonGhostQuantifiers.dfy(140,8): 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)
20 resolution/type errors detected in NonGhostQuantifiers.dfy
diff --git a/Test/dafny0/ParallelResolveErrors.dfy b/Test/dafny0/ParallelResolveErrors.dfy index 5e01f019..8c48487d 100644 --- a/Test/dafny0/ParallelResolveErrors.dfy +++ b/Test/dafny0/ParallelResolveErrors.dfy @@ -7,7 +7,6 @@ class C { ghost method Init_ModifyNothing() { }
ghost method Init_ModifyThis() modifies this;
{
- data := 6; // error: assignment to a non-ghost field
gdata := 7;
}
ghost method Init_ModifyStuff(c: C) modifies this, c; { }
@@ -40,8 +39,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)
@@ -120,3 +119,15 @@ method M3(c: C) c.GhostMethodWithModifies(x); // error: not allowed to call method with nonempty modifies clause
}
}
+
+module AnotherModule {
+ class C {
+ var data: int;
+ ghost var gdata: int;
+ ghost method Init_ModifyThis() modifies this;
+ {
+ data := 6; // error: assignment to a non-ghost field
+ gdata := 7;
+ }
+ }
+}
diff --git a/Test/dafny0/ParallelResolveErrors.dfy.expect b/Test/dafny0/ParallelResolveErrors.dfy.expect index 7305bfce..4d25ba11 100644 --- a/Test/dafny0/ParallelResolveErrors.dfy.expect +++ b/Test/dafny0/ParallelResolveErrors.dfy.expect @@ -1,22 +1,23 @@ -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(56,13): Error: new allocation not supported in forall statements
+ParallelResolveErrors.dfy(129,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)
+ParallelResolveErrors.dfy(20,4): Error: LHS of assignment must denote a mutable variable
+ParallelResolveErrors.dfy(25,6): Error: body of forall statement is attempting to update a variable declared outside the forall statement
+ParallelResolveErrors.dfy(42,6): Error: body of forall statement is attempting to update a variable declared outside the forall statement
+ParallelResolveErrors.dfy(43,6): Error: body of forall statement is attempting to update a variable declared outside the forall statement
+ParallelResolveErrors.dfy(55,13): Error: new allocation not supported in forall statements
+ParallelResolveErrors.dfy(60,13): Error: new allocation not allowed in ghost context
ParallelResolveErrors.dfy(61,13): Error: new allocation not allowed in ghost context
ParallelResolveErrors.dfy(62,13): Error: new allocation not allowed in ghost context
ParallelResolveErrors.dfy(63,13): Error: new allocation not allowed in ghost context
-ParallelResolveErrors.dfy(64,13): Error: new allocation not allowed in ghost context
-ParallelResolveErrors.dfy(65,22): 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(66,20): Error: the body of the enclosing forall statement is not allowed to call non-ghost methods
-ParallelResolveErrors.dfy(73,19): Error: trying to break out of more loop levels than there are enclosing loops
-ParallelResolveErrors.dfy(77,18): Error: return statement is not allowed inside a forall statement
-ParallelResolveErrors.dfy(84,21): Error: trying to break out of more loop levels than there are enclosing loops
-ParallelResolveErrors.dfy(85,20): Error: trying to break out of more loop levels than there are enclosing loops
-ParallelResolveErrors.dfy(86,20): Error: break label is undefined or not in scope: OutsideLoop
-ParallelResolveErrors.dfy(95,24): Error: trying to break out of more loop levels than there are enclosing loops
-ParallelResolveErrors.dfy(96,24): Error: break label is undefined or not in scope: OutsideLoop
-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
+ParallelResolveErrors.dfy(64,22): 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(65,20): Error: the body of the enclosing forall statement is not allowed to call non-ghost methods
+ParallelResolveErrors.dfy(72,19): Error: trying to break out of more loop levels than there are enclosing loops
+ParallelResolveErrors.dfy(76,18): Error: return statement is not allowed inside a forall statement
+ParallelResolveErrors.dfy(83,21): Error: trying to break out of more loop levels than there are enclosing loops
+ParallelResolveErrors.dfy(84,20): Error: trying to break out of more loop levels than there are enclosing loops
+ParallelResolveErrors.dfy(85,20): Error: break label is undefined or not in scope: OutsideLoop
+ParallelResolveErrors.dfy(94,24): Error: trying to break out of more loop levels than there are enclosing loops
+ParallelResolveErrors.dfy(95,24): Error: break label is undefined or not in scope: OutsideLoop
+ParallelResolveErrors.dfy(106,9): Error: the body of the enclosing forall statement is not allowed to update heap locations
+ParallelResolveErrors.dfy(114,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(119,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
+22 resolution/type errors detected in ParallelResolveErrors.dfy
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 1354e533..e935c83d 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -9,9 +9,9 @@ method GhostDivergentLoop() a[1] := -1;
ghost var i := 0;
while (i < 2)
- decreases *; // error: not allowed on a ghost loop
- invariant i <= 2;
- invariant (forall j :: 0 <= j && j < i ==> a[j] > 0);
+ decreases * // error: not allowed on a ghost loop
+ invariant i <= 2
+ invariant (forall j :: 0 <= j && j < i ==> a[j] > 0)
{
i := 0;
}
@@ -91,9 +91,9 @@ class EE { var b3 := Benny;
var d0 := David(20); // error: constructor name David is ambiguous
var d1 := David; // error: constructor name David is ambiguous (never mind that the signature does
- // not match either of them)
+ // not match either of them)
var d2 := David(20, 40); // error: constructor name Davis is ambiguous (never mind that the given
- // parameters match the signature of only one of those constructors)
+ // parameters match the signature of only one of those constructors)
var d3 := Abc.David(20, 40); // error: wrong number of parameters
var d4 := Rst.David(20, 40);
var e := Eleanor; // this resolves to the field, not the Abc datatype constructor
@@ -102,7 +102,7 @@ class EE { }
// --------------- ghost tests -------------------------------------
-
+module HereAreMoreGhostTests {
datatype GhostDt =
Nil(ghost extraInfo: int) |
Cons(data: int, tail: GhostDt, ghost moreInfo: int)
@@ -150,14 +150,6 @@ class GhostTests { r := r + g; // fine, for the same reason
r := N(20, 20); // error: call to non-ghost method from ghost method is not okay
}
- ghost method NiceTry()
- ensures false;
- {
- while (true)
- decreases *; // error: not allowed in ghost context
- {
- }
- }
ghost method BreaksAreFineHere(t: int)
{
var n := 0;
@@ -195,6 +187,57 @@ class GhostTests { decreases 112 - n;
{
label MyStructure: {
+ k := k + 1;
+ }
+ label MyOtherStructure:
+ if (k % 17 == 0) {
+ break MyOtherStructure; // this break is fine
+ } else {
+ k := k + 1;
+ }
+
+ var dontKnow;
+ if (n == 112) {
+ ghost var m := 0;
+ label LoopLabel0:
+ label LoopLabel1:
+ while (m < 200) {
+ if (m % 103 == 0) {
+ if {
+ case true => break; // fine, since this breaks out of the enclosing ghost loop
+ case true => break LoopLabel0; // fine
+ case true => break LoopLabel1; // fine
+ }
+ } else if (m % 101 == 0) {
+ }
+ m := m + 3;
+ }
+ break;
+ } else if (dontKnow == 708) {
+ var q := 0;
+ while (q < 1) {
+ label IfNest:
+ if (p == 67) {
+ break break; // fine, since this is not a ghost context
+ }
+ q := q + 1;
+ }
+ } else if (n == t) {
+ }
+ n := n + 1;
+ p := p + 1;
+ }
+ }
+ method BreakMayNotBeFineHere_Ghost(ghost t: int)
+ {
+ var n := 0;
+ ghost var k := 0;
+ var p := 0;
+ while (true)
+ invariant n <= 112;
+ decreases 112 - n;
+ {
+ label MyStructure: {
if (k % 17 == 0) { break MyStructure; } // error: break from ghost to non-ghost point
k := k + 1;
}
@@ -230,8 +273,6 @@ class GhostTests { if (p == 67) {
break break; // fine, since this is not a ghost context
} 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
} else if (k == 67) {
break break; // error, because this is a ghost context
@@ -246,7 +287,7 @@ class GhostTests { }
}
}
-
+} //HereAreMoreGhostTests
method DuplicateLabels(n: int) {
var x;
if (n < 7) {
@@ -310,18 +351,17 @@ 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
}
}
// ------------------- print statements ---------------------------------------
-
+module GhostPrintAttempts {
method PrintOnlyNonGhosts(a: int, ghost b: int)
{
print "a: ", a, "\n";
print "b: ", b, "\n"; // error: print statement cannot take ghosts
}
-
+}
// ------------------- auto-added type arguments ------------------------------
class GenericClass<T> { var data: T; }
@@ -381,45 +421,42 @@ method TestCalc(m: int, n: int, a: bool, b: bool) n + m + 1;
==> n + m + 2; // error: ==> operator requires boolean lines
}
- calc {
- n + m;
- { print n + m; } // error: non-ghost statements are not allowed in hints
- m + n;
- }
}
-class SideEffectChecks {
- ghost var ycalc: int;
+module MyOwnModule {
+ class SideEffectChecks {
+ ghost var ycalc: int;
- ghost method Mod(a: int)
- modifies this;
- ensures ycalc == a;
- {
- ycalc := a;
- }
+ ghost method Mod(a: int)
+ modifies this;
+ ensures ycalc == a;
+ {
+ ycalc := a;
+ }
- ghost method Bad()
- modifies this;
- ensures 0 == 1;
- {
- var x: int;
- calc {
- 0;
- { Mod(0); } // methods with side-effects are not allowed
- ycalc;
- { ycalc := 1; } // heap updates are not allowed
- 1;
- { x := 1; } // updates to locals defined outside of the hint are not allowed
- x;
- {
- var x: int;
- x := 1; // this is OK
+ ghost method Bad()
+ modifies this;
+ ensures 0 == 1;
+ {
+ var x: int;
+ calc {
+ 0;
+ { Mod(0); } // error: methods with side-effects are not allowed
+ ycalc;
+ { ycalc := 1; } // error: heap updates are not allowed
+ 1;
+ { x := 1; } // error: updates to locals defined outside of the hint are not allowed
+ x;
+ {
+ var x: int;
+ x := 1; // this is OK
+ }
+ 1;
}
- 1;
}
}
}
-
+
// ------------------- nameless constructors ------------------------------
class YHWH {
@@ -467,14 +504,10 @@ 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)
@@ -543,8 +576,6 @@ 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)
-
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
ghost var xg := var w :| w == 2*w; w;
@@ -555,16 +586,16 @@ method LetSuchThat(ghost z: int, n: nat) module NonInferredType {
predicate P<T>(x: T)
- method NonInferredType0(x: int)
+ method InferredType(x: int)
{
var t;
- assume forall z :: P(z) && z == t; // It would be nice to allow the following example, but the implementation calls DiscoverBounds before CheckInference for quantifiers.
+ assume forall z :: P(z) && z == t;
assume t == x; // this statement determines the type of t and z
}
- method NonInferredType1(x: int)
+ method NonInferredType(x: int)
{
- var t;
+ var t; // error: the type of t is not determined
assume forall z :: P(z) && z == t; // error: the type of z is not determined
}
}
@@ -582,20 +613,7 @@ module GhostAllocationTests { p := new G; // error: ditto
}
- method GhostNew1(n: nat)
- {
- var a := new G[n];
- forall i | 0 <= i < n {
- a[i] := new G; // error: 'new' is currently not supported in forall statements
- }
- forall i | 0 <= i < n
- ensures true; // this makes the whole 'forall' statement into a ghost statement
- {
- a[i] := new G; // error: 'new' not allowed in ghost contexts, and proof-forall cannot update state
- }
- }
-
- method GhostNew2(n: nat, ghost g: int) returns (t: G, z: int)
+ method GhostNew1(n: nat, ghost g: int) returns (t: G, z: int)
{
if n < 0 {
z, t := 5, new G; // fine
@@ -605,33 +623,45 @@ module GhostAllocationTests { }
}
- method GhostNew3(ghost b: bool)
+ method GhostNew2(ghost b: bool)
{
if (b) {
var y := new GIter(); // error: 'new' not allowed in ghost contexts (and a non-ghost method is not allowed to be called here either)
}
}
- method GhostNew4(n: nat)
+ method GhostNew3(n: nat)
{
var g := new G;
calc {
5;
{ var y := new G; } // error: 'new' not allowed in ghost contexts
2 + 3;
- { if n != 0 { GhostNew4(n-1); } } // error: cannot call non-ghost method in a ghost context
- 1 + 4;
- { GhostNew5(g); } // error: cannot call method with nonempty modifies
- -5 + 10;
}
}
- ghost method GhostNew5(g: G)
+ ghost method GhostNew4(g: G)
modifies g;
{
}
}
+module NewForall {
+ class G { }
+ method NewForallTest(n: nat)
+ {
+ var a := new G[n];
+ forall i | 0 <= i < n {
+ a[i] := new G; // error: 'new' is currently not supported in forall statements
+ }
+ forall i | 0 <= i < n
+ ensures true; // this makes the whole 'forall' statement into a ghost statement
+ {
+ a[i] := new G; // error: 'new' not allowed in ghost contexts, and proof-forall cannot update state
+ }
+ }
+}
+
// ------------------------- underspecified types ------------------------------
module UnderspecifiedTypes {
@@ -672,46 +702,31 @@ module StatementsInExpressions { {
}
- ghost method M()
- modifies this;
- {
- calc {
- 5;
- { SideEffect(); } // error: cannot call method with side effects
- 5;
- }
- }
-
function F(): int
{
calc {
- 6;
- { assert 6 < 8; }
- { NonGhostMethod(); } // error: cannot call non-ghost method
- { var x := 8;
- while x != 0
- decreases *; // error: cannot use 'decreases *' in a ghost context
- {
- x := x - 1;
- }
- }
- { var x := 8;
- while x != 0
- {
- x := x - 1;
- }
- }
- { MyField := 12; } // error: cannot assign to a field
- { MyGhostField := 12; } // error: cannot assign to any field
- { SideEffect(); } // error: cannot call (ghost) method with a modifies clause
- { var x := 8;
- while x != 0
- modifies this; // error: cannot use a modifies clause on a loop
- {
- x := x - 1;
- }
- }
- 6;
+ 6;
+ { assert 6 < 8; }
+ { var x := 8;
+ while x != 0
+ decreases * // error: cannot use 'decreases *' here
+ {
+ x := x - 1;
+ }
+ }
+ { var x := 8;
+ while x != 0
+ {
+ x := x - 1;
+ }
+ }
+ { var x := 8;
+ while x != 0
+ {
+ x := x - 1;
+ }
+ }
+ 6;
}
5
}
@@ -723,33 +738,28 @@ module StatementsInExpressions { {
var y :=
calc {
- 6;
- { assert 6 < 8; }
- { NonGhostMethod(); } // error: cannot call non-ghost method
- { var x := 8;
- while x != 0
- decreases *; // error: cannot use 'decreases *' in a ghost context
- {
- x := x - 1;
- }
- }
- { MyField := 12; } // error: cannot assign to a field
- { MyGhostField := 12; } // error: cannot assign to any field
- { M(); } // error: cannot call (ghost) method with a modifies clause
- { var x := 8;
- while x != 0
- modifies this; // error: cannot use a modifies clause on a loop
- {
- x := x - 1;
- }
- }
- { var x := 8;
- while x != 0
- {
- x := x - 1;
- }
- }
- 6;
+ 6;
+ { assert 6 < 8; }
+ { var x := 8;
+ while x != 0
+ decreases * // error: cannot use 'decreases *' here
+ {
+ x := x - 1;
+ }
+ }
+ { var x := 8;
+ while x != 0
+ {
+ x := x - 1;
+ }
+ }
+ { var x := 8;
+ while x != 0
+ {
+ x := x - 1;
+ }
+ }
+ 6;
}
5;
}
@@ -764,7 +774,6 @@ module StatementsInExpressions { {
MyLemma();
MyGhostMethod(); // error: modifi2es state
- OrdinaryMethod(); // error: not a ghost
OutParamMethod(); // error: has out-parameters
10
}
@@ -846,40 +855,48 @@ class ModifyStatementClass { ghost method G0()
modifies `g;
modifies `x; // error: non-ghost field mentioned in ghost context
- {
- modify `g;
- modify `x; // error: non-ghost field mentioned in ghost context
- }
- method G1()
- modifies this;
- {
- modify `x;
- if g < 100 {
- // we are now in a ghost context
+}
+module ModifyStatementClass_More {
+ class C {
+ var x: int;
+ ghost var g: int;
+ ghost method G0()
+ modifies `g;
+ {
+ modify `g;
modify `x; // error: non-ghost field mentioned in ghost context
}
- }
- method G2(y: nat)
- modifies this;
- {
- if g < 100 {
- // we're now in a ghost context
- var n := 0;
- while n < y
- modifies `x; // error: non-ghost field mentioned in ghost context
- {
- if * {
- g := g + 1; // if we got as far as verification, this would be flagged as an error too
- }
- n := n + 1;
+ method G1()
+ modifies this;
+ {
+ modify `x;
+ if g < 100 {
+ // we are now in a ghost context
+ modify `x; // error: non-ghost field mentioned in ghost context
}
}
- modify `x; // fine
- ghost var i := 0;
- while i < y
- modifies `x; // error: non-ghost field mentioned in ghost context
+ method G2(y: nat)
+ modifies this;
{
- i := i + 1;
+ if g < 100 {
+ // we're now in a ghost context
+ var n := 0;
+ while n < y
+ modifies `x; // error: non-ghost field mentioned in ghost context
+ {
+ if * {
+ g := g + 1; // if we got as far as verification, this would be flagged as an error too
+ }
+ n := n + 1;
+ }
+ }
+ modify `x; // fine
+ ghost var i := 0;
+ while i < y
+ modifies `x; // error: non-ghost field mentioned in ghost context
+ {
+ i := i + 1;
+ }
}
}
}
@@ -1109,15 +1126,15 @@ method TraitSynonym() // ----- set comprehensions where the term type is finite -----
module ObjectSetComprehensions {
- // allowed in non-ghost context:
- function A() : set<object> { set o : object | true :: o }
+ // the following set comprehensions are known to be finite
+ function A() : set<object> { set o : object | true :: o } // error: a function is not allowed to depend on the allocated state
- lemma B() { var x := set o : object | true :: o; }
+ function method B() : set<object> { set o : object | true :: o } // error: a function is not allowed to depend on the allocated state
- // not allowed in non-ghost context:
- function method C() : set<object> { set o : object | true :: o }
+ // outside functions, the comprehension is permitted, but it cannot be compiled
+ lemma C() { var x := set o : object | true :: o; }
- method D() { var x := set o : object | true :: o; }
+ method D() { var x := set o : object | true :: o; } // error: not (easily) compilable
}
// ------ regression test for type checking of integer division -----
@@ -1211,9 +1228,9 @@ module NonInferredTypeVariables { method BadClient(n: nat)
{
var p := P(n); // error: cannot infer the type argument for P
- ghost var q := Q(n); // error: cannot infer the type argument for Q
+ ghost var q := Q(n); // error: cannot infer the type argument for Q (and thus q's type cannot be determined either)
M(n); // error: cannot infer the type argument for M
- var x := N(n); // error: cannot infer the type argument for N
+ var x := N(n); // error: cannot infer the type argument for N (and thus x's type cannot be determined either)
var a := new array; // error: cannot infer the type argument for 'array'
var c := new C; // error: cannot infer the type argument for 'C'
var s: set; // type argument for 'set'
@@ -1231,7 +1248,7 @@ module NonInferredTypeVariables { ghost var d0 := forall s :: s == {7} ==> s != {};
var d1 := forall s: set :: s in S ==> s == {};
var ggcc0: C;
- var ggcc1: C;
+ var ggcc1: C; // error: full type cannot be determined
ghost var d2 := forall c: C :: c != null ==> c.f == 10;
ghost var d2' := forall c :: c == ggcc0 && c != null ==> c.f == 10;
ghost var d2'' := forall c :: c == ggcc1 && c != null ==> c.f == c.f; // error: here, type of c is not determined
@@ -1292,7 +1309,7 @@ module FrameTargetFields { modifies `z // cool
{
}
-
+} } module FrameTargetFields_More { class C { var x: int var y: int ghost var z: int
method P()
modifies this
{
@@ -1388,3 +1405,290 @@ module SuchThat { w
}
}
+
+// ---------------------- NEW STUFF ----------------------------------------
+
+module GhostTests {
+ class G { }
+
+ method GhostNew3(n: nat)
+ {
+ var g := new G;
+ calc {
+ 5;
+ 2 + 3;
+ { if n != 0 { GhostNew3(n-1); } } // error: cannot call non-ghost method in a ghost context
+ 1 + 4;
+ { GhostNew4(g); } // error: cannot call method with nonempty modifies
+ -5 + 10;
+ }
+ }
+
+ ghost method GhostNew4(g: G)
+ modifies g;
+ {
+ }
+
+ class MyClass {
+ ghost method SideEffect()
+ modifies this;
+ {
+ }
+
+ method NonGhostMethod()
+ {
+ }
+
+ ghost method M()
+ modifies this;
+ {
+ calc {
+ 5;
+ { SideEffect(); } // error: cannot call method with side effects
+ 5;
+ }
+ }
+ function F(): int
+ {
+ calc {
+ 6;
+ { assert 6 < 8; }
+ { NonGhostMethod(); } // error: cannot call non-ghost method
+ { var x := 8;
+ while x != 0
+ {
+ x := x - 1;
+ }
+ }
+ { var x := 8;
+ while x != 0
+ {
+ x := x - 1;
+ }
+ }
+ { MyField := 12; } // error: cannot assign to a field, and especially not a non-ghost field
+ { MyGhostField := 12; } // error: cannot assign to any field
+ { SideEffect(); } // error: cannot call (ghost) method with a modifies clause
+ { var x := 8;
+ while x != 0
+ modifies this; // error: cannot use a modifies clause on a loop
+ {
+ x := x - 1;
+ }
+ }
+ 6;
+ }
+ 5
+ }
+ var MyField: int;
+ ghost var MyGhostField: int;
+ method N()
+ {
+ var y :=
+ calc {
+ 6;
+ { assert 6 < 8; }
+ { NonGhostMethod(); } // error: cannot call non-ghost method
+ { var x := 8;
+ while x != 0
+ {
+ x := x - 1;
+ }
+ }
+ { MyField := 12; } // error: cannot assign to a field, and especially not a non-ghost field
+ { MyGhostField := 12; } // error: cannot assign to any field
+ { M(); } // error: cannot call (ghost) method with a modifies clause
+ { var x := 8;
+ while x != 0
+ modifies this; // error: cannot use a modifies clause on a loop
+ {
+ x := x - 1;
+ }
+ }
+ { var x := 8;
+ while x != 0
+ {
+ x := x - 1;
+ }
+ }
+ 6;
+ }
+ 5;
+ }
+ ghost method MyLemma()
+ ghost method MyGhostMethod()
+ modifies this;
+ method OrdinaryMethod()
+ ghost method OutParamMethod() returns (y: int)
+
+ function UseLemma(): int
+ {
+ MyLemma();
+ OrdinaryMethod(); // error: not a ghost
+ 10
+ }
+ }
+}
+
+module EvenMoreGhostTests {
+ ghost method NiceTry()
+ ensures false;
+ {
+ while (true)
+ decreases * // error: not allowed here
+ {
+ }
+ }
+ method BreakMayNotBeFineHere()
+ {
+ var n := 0;
+ var p := 0;
+ while (true)
+ {
+ var dontKnow;
+ if (n == 112) {
+ } else if (dontKnow == 708) {
+ while * {
+ label IfNest:
+ if (p == 67) {
+ break break; // fine, since this is not a ghost context
+ } else if (*) {
+ break break break; // error: tries to break out of more loop levels than there are
+ }
+ }
+ }
+ }
+ }
+}
+
+module BadGhostTransfer {
+ datatype DTD_List = DTD_Nil | DTD_Cons(Car: int, Cdr: DTD_List, ghost g: int)
+
+ method DatatypeDestructors_Ghost(d: DTD_List) {
+ var g1 := d.g; // error: cannot use ghost member in non-ghost code
+ }
+ 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
+ }
+}
+
+module MoreGhostPrintAttempts {
+ method TestCalc_Ghost(m: int, n: int, a: bool, b: bool)
+ {
+ calc {
+ n + m;
+ { print n + m; } // error: non-ghost statements are not allowed in hints
+ m + n;
+ }
+ }
+}
+
+module MoreLetSuchThatExpr {
+ method LetSuchThat_Ghost(ghost z: int, n: nat)
+ {
+ var x := var y :| y < z; y; // error: contraint depend on ghost (z)
+ }
+}
+
+module UnderspecifiedTypedShouldBeResolvedOnlyOnce {
+ method CalcTest0(s: seq<int>) {
+ calc {
+ 2;
+ var t :| true; 2; // error: type of 't' is underspecified
+ }
+ }
+}
+
+module LoopResolutionTests {
+ class C {
+ var x: int
+ ghost var y: int
+ }
+
+ ghost method M(c: C)
+ requires c != null
+ modifies c
+ {
+ var n := 0;
+ while n < 100
+ modifies c`y
+ modifies c`x // error: not allowed to mention non-ghost field in modifies clause of ghost loops
+ {
+ c.x := c.x + 1; // error: assignment to non-ghost field not allowed here
+ }
+ }
+
+ method MM(c: C)
+ requires c != null
+ modifies c
+ {
+ var n := 0;
+ while
+ invariant n <= 100
+ modifies c // regression test
+ {
+ case n < 100 => n := n + 1;
+ }
+ }
+
+ method MMX(c: C, ghost g: int)
+ requires c != null
+ modifies c
+ {
+ var n := 0;
+ while
+ invariant n <= 100
+ modifies c`y
+ modifies c`x // error: not allowed to mention non-ghost field in modifies clause of ghost loops
+ {
+ case n < 100 => n := n + 1; // error: cannot assign to non-ghost in a ghost loop
+ case g < 56 && n != 100 => n := n + 1; // error: cannot assign to non-ghost in a ghost loop
+ }
+ }
+
+ method MD0(c: C, ghost g: nat)
+ requires c != null
+ modifies c
+ decreases *
+ {
+ var n := 0;
+ while n + g < 100
+ invariant n <= 100
+ decreases * // error: disallowed on ghost loops
+ {
+ n := n + 1; // error: cannot assign to non-ghost in a ghost loop
+ }
+ }
+
+ method MD1(c: C, ghost g: nat)
+ requires c != null
+ modifies c
+ decreases *
+ {
+ var n := 0;
+ while
+ invariant n <= 100
+ decreases * // error: disallowed on ghost loops
+ {
+ case n + g < 100 => n := n + 1; // error: cannot assign to non-ghost in a ghost loop
+ }
+ }
+}
diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index b5c93ac1..be19eeac 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -1,120 +1,3 @@ -ResolutionErrors.dfy(502,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)
-ResolutionErrors.dfy(507,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)
-ResolutionErrors.dfy(521,23): Error: type of case bodies do not agree (found Tree<_T1,_T0>, previous types Tree<_T0,_T1>)
-ResolutionErrors.dfy(533,24): Error: Wrong number of type arguments (0 instead of 2) passed to datatype: Tree
-ResolutionErrors.dfy(561,25): Error: the type of this variable is underspecified
-ResolutionErrors.dfy(561,23): Error: type variable 'T' in the function call to 'P' could not be determined
-ResolutionErrors.dfy(568,25): Error: the type of this variable is underspecified
-ResolutionErrors.dfy(568,23): Error: type variable 'T' in the function call to 'P' could not be determined
-ResolutionErrors.dfy(581,13): Error: 'new' is not allowed in ghost contexts
-ResolutionErrors.dfy(582,9): Error: 'new' is not allowed in ghost contexts
-ResolutionErrors.dfy(589,14): Error: new allocation not supported in forall statements
-ResolutionErrors.dfy(594,11): Error: the body of the enclosing forall statement is not allowed to update heap locations
-ResolutionErrors.dfy(594,14): Error: new allocation not allowed in ghost context
-ResolutionErrors.dfy(604,23): Error: 'new' is not allowed in ghost contexts
-ResolutionErrors.dfy(611,15): Error: 'new' is not allowed in ghost contexts
-ResolutionErrors.dfy(611,15): Error: only ghost methods can be called from this context
-ResolutionErrors.dfy(620,17): Error: 'new' is not allowed in ghost contexts
-ResolutionErrors.dfy(622,29): Error: only ghost methods can be called from this context
-ResolutionErrors.dfy(624,17): Error: calls to methods with side-effects are not allowed inside a hint
-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
-ResolutionErrors.dfy(741,14): Error: a while statement used inside a hint is not allowed to have a modifies clause
-ResolutionErrors.dfy(766,19): Error: calls to methods with side-effects are not allowed inside a statement expression
-ResolutionErrors.dfy(767,20): Error: only ghost methods can be called from this context
-ResolutionErrors.dfy(768,20): Error: wrong number of method result arguments (got 0, expected 1)
-ResolutionErrors.dfy(780,23): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
-ResolutionErrors.dfy(790,4): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(801,36): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(810,17): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
-ResolutionErrors.dfy(824,6): Error: RHS (of type B) not assignable to LHS (of type object)
-ResolutionErrors.dfy(825,6): Error: RHS (of type int) not assignable to LHS (of type object)
-ResolutionErrors.dfy(826,6): Error: RHS (of type B) not assignable to LHS (of type object)
-ResolutionErrors.dfy(831,6): Error: RHS (of type G) not assignable to LHS (of type object)
-ResolutionErrors.dfy(832,6): Error: RHS (of type Dt) not assignable to LHS (of type object)
-ResolutionErrors.dfy(833,6): Error: RHS (of type CoDt) not assignable to LHS (of type object)
-ResolutionErrors.dfy(895,4): Error: LHS of array assignment must denote an array element (found seq<int>)
-ResolutionErrors.dfy(896,4): Error: LHS of array assignment must denote an array element (found seq<int>)
-ResolutionErrors.dfy(901,10): Error: LHS of assignment must denote a mutable field
-ResolutionErrors.dfy(902,10): Error: LHS of assignment must denote a mutable field
-ResolutionErrors.dfy(903,9): Error: cannot assign to a range of array elements (try the 'forall' statement)
-ResolutionErrors.dfy(904,9): Error: cannot assign to a range of array elements (try the 'forall' statement)
-ResolutionErrors.dfy(905,5): Error: cannot assign to a range of array elements (try the 'forall' statement)
-ResolutionErrors.dfy(906,5): Error: cannot assign to a range of array elements (try the 'forall' statement)
-ResolutionErrors.dfy(987,11): Error: Wrong number of type arguments (2 instead of 1) passed to array type: array3
-ResolutionErrors.dfy(988,11): Error: Wrong number of type arguments (2 instead of 1) passed to class: C
-ResolutionErrors.dfy(999,7): Error: Duplicate name of top-level declaration: BadSyn2
-ResolutionErrors.dfy(996,17): Error: Wrong number of type arguments (0 instead of 1) passed to datatype: List
-ResolutionErrors.dfy(997,17): Error: Undeclared top-level type or type parameter: badName (did you forget to qualify a name or declare a module import 'opened?')
-ResolutionErrors.dfy(998,22): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name or declare a module import 'opened?')
-ResolutionErrors.dfy(1005,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> A
-ResolutionErrors.dfy(1008,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
-ResolutionErrors.dfy(1012,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
-ResolutionErrors.dfy(1021,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed
-ResolutionErrors.dfy(1024,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
-ResolutionErrors.dfy(1029,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
-ResolutionErrors.dfy(1048,21): Error: unresolved identifier: x
-ResolutionErrors.dfy(1055,35): Error: Wrong number of type arguments (2 instead of 1) passed to opaque type: P
-ResolutionErrors.dfy(1067,13): Error: Undeclared top-level type or type parameter: BX (did you forget to qualify a name or declare a module import 'opened?')
-ResolutionErrors.dfy(1077,6): Error: RHS (of type P<int>) not assignable to LHS (of type P<bool>)
-ResolutionErrors.dfy(1082,6): Error: RHS (of type P<A>) not assignable to LHS (of type P<B>)
-ResolutionErrors.dfy(1087,6): Error: RHS (of type P<A>) not assignable to LHS (of type P<int>)
-ResolutionErrors.dfy(1088,6): Error: RHS (of type P<int>) not assignable to LHS (of type P<A>)
-ResolutionErrors.dfy(1093,13): Error: arguments must have the same type (got P<int> and P<X>)
-ResolutionErrors.dfy(1094,13): Error: arguments must have the same type (got P<bool> and P<X>)
-ResolutionErrors.dfy(1095,13): Error: arguments must have the same type (got P<int> and P<bool>)
-ResolutionErrors.dfy(1118,38): Error: 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 'o'
-ResolutionErrors.dfy(1120,24): Error: 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 'o'
-ResolutionErrors.dfy(1225,26): Error: the type of this variable is underspecified
-ResolutionErrors.dfy(1226,31): Error: the type of this variable is underspecified
-ResolutionErrors.dfy(1227,29): Error: the type of this variable is underspecified
-ResolutionErrors.dfy(1237,34): Error: the type of this variable is underspecified
-ResolutionErrors.dfy(1253,21): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name or declare a module import 'opened?')
-ResolutionErrors.dfy(1254,24): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name or declare a module import 'opened?')
-ResolutionErrors.dfy(1291,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (y)
-ResolutionErrors.dfy(1301,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
-ResolutionErrors.dfy(1329,15): Error: The name Inner ambiguously refers to a type in one of the modules A, B (try qualifying the type name with the module name)
-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<real, string>)
-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<real, string>)
-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(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')
-ResolutionErrors.dfy(92,14): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
-ResolutionErrors.dfy(93,14): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
-ResolutionErrors.dfy(95,14): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
-ResolutionErrors.dfy(97,18): Error: wrong number of arguments to datatype constructor David (found 2, expected 1)
ResolutionErrors.dfy(113,9): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(114,9): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
ResolutionErrors.dfy(118,11): Error: ghost variables are allowed only in specification contexts
@@ -125,31 +8,178 @@ ResolutionErrors.dfy(137,4): Error: ghost variables are allowed only in specific ResolutionErrors.dfy(141,21): Error: ghost variables are allowed only in specification contexts
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
-ResolutionErrors.dfy(438,14): Error: when allocating an object of type 'YHWH', one of its constructor methods must be called
-ResolutionErrors.dfy(443,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called
-ResolutionErrors.dfy(444,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called
-ResolutionErrors.dfy(446,9): Error: class Lamb does not have an anonymous constructor
-ResolutionErrors.dfy(844,11): Error: a modifies-clause expression must denote an object or a collection of objects (instead got int)
-ResolutionErrors.dfy(848,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
-ResolutionErrors.dfy(851,12): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
-ResolutionErrors.dfy(859,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
-ResolutionErrors.dfy(869,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
-ResolutionErrors.dfy(880,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
-ResolutionErrors.dfy(1036,23): Error: unresolved identifier: x
-ResolutionErrors.dfy(1039,20): Error: unresolved identifier: x
-ResolutionErrors.dfy(1042,23): Error: unresolved identifier: x
-ResolutionErrors.dfy(1044,19): Error: unresolved identifier: x
-ResolutionErrors.dfy(1046,19): Error: unresolved identifier: x
-ResolutionErrors.dfy(12,16): Error: 'decreases *' is not allowed on ghost loops
+ResolutionErrors.dfy(241,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure
+ResolutionErrors.dfy(264,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
+ResolutionErrors.dfy(278,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
+ResolutionErrors.dfy(283,8): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression)
+ResolutionErrors.dfy(362,15): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(444,13): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(446,16): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(448,12): Error: a hint is not allowed to update a variable declared outside the hint
+ResolutionErrors.dfy(535,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)
+ResolutionErrors.dfy(540,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)
+ResolutionErrors.dfy(554,23): Error: type of case bodies do not agree (found Tree<_T1,_T0>, previous types Tree<_T0,_T1>)
+ResolutionErrors.dfy(566,24): Error: Wrong number of type arguments (0 instead of 2) passed to datatype: Tree
+ResolutionErrors.dfy(598,8): Error: the type of this local variable is underspecified
+ResolutionErrors.dfy(599,23): Error: type variable 'T' in the function call to 'P' could not be determined
+ResolutionErrors.dfy(599,18): Error: type of bound variable 'z' could not be determined; please specify the type explicitly
+ResolutionErrors.dfy(612,13): Error: 'new' is not allowed in ghost contexts
+ResolutionErrors.dfy(613,9): Error: 'new' is not allowed in ghost contexts
+ResolutionErrors.dfy(622,23): Error: 'new' is not allowed in ghost contexts
+ResolutionErrors.dfy(629,15): Error: 'new' is not allowed in ghost contexts
+ResolutionErrors.dfy(638,17): Error: 'new' is not allowed in ghost contexts
+ResolutionErrors.dfy(655,14): Error: new allocation not supported in forall statements
+ResolutionErrors.dfy(660,11): Error: the body of the enclosing forall statement is not allowed to update heap locations
+ResolutionErrors.dfy(660,14): Error: new allocation not allowed in ghost context
+ResolutionErrors.dfy(672,21): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(712,22): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating
+ResolutionErrors.dfy(745,22): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating
+ResolutionErrors.dfy(776,19): Error: calls to methods with side-effects are not allowed inside a statement expression
+ResolutionErrors.dfy(777,20): Error: wrong number of method result arguments (got 0, expected 1)
+ResolutionErrors.dfy(789,23): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
+ResolutionErrors.dfy(799,4): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(810,36): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(819,17): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
+ResolutionErrors.dfy(833,6): Error: RHS (of type B) not assignable to LHS (of type object)
+ResolutionErrors.dfy(834,6): Error: RHS (of type int) not assignable to LHS (of type object)
+ResolutionErrors.dfy(835,6): Error: RHS (of type B) not assignable to LHS (of type object)
+ResolutionErrors.dfy(840,6): Error: RHS (of type G) not assignable to LHS (of type object)
+ResolutionErrors.dfy(841,6): Error: RHS (of type Dt) not assignable to LHS (of type object)
+ResolutionErrors.dfy(842,6): Error: RHS (of type CoDt) not assignable to LHS (of type object)
+ResolutionErrors.dfy(867,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(875,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(885,20): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(896,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(912,4): Error: LHS of array assignment must denote an array element (found seq<int>)
+ResolutionErrors.dfy(913,4): Error: LHS of array assignment must denote an array element (found seq<int>)
+ResolutionErrors.dfy(918,10): Error: LHS of assignment must denote a mutable field
+ResolutionErrors.dfy(919,10): Error: LHS of assignment must denote a mutable field
+ResolutionErrors.dfy(920,9): Error: cannot assign to a range of array elements (try the 'forall' statement)
+ResolutionErrors.dfy(921,9): Error: cannot assign to a range of array elements (try the 'forall' statement)
+ResolutionErrors.dfy(922,5): Error: cannot assign to a range of array elements (try the 'forall' statement)
+ResolutionErrors.dfy(923,5): Error: cannot assign to a range of array elements (try the 'forall' statement)
+ResolutionErrors.dfy(1004,11): Error: Wrong number of type arguments (2 instead of 1) passed to array type: array3
+ResolutionErrors.dfy(1005,11): Error: Wrong number of type arguments (2 instead of 1) passed to class: C
+ResolutionErrors.dfy(1016,7): Error: Duplicate name of top-level declaration: BadSyn2
+ResolutionErrors.dfy(1013,17): Error: Wrong number of type arguments (0 instead of 1) passed to datatype: List
+ResolutionErrors.dfy(1014,17): Error: Undeclared top-level type or type parameter: badName (did you forget to qualify a name or declare a module import 'opened?')
+ResolutionErrors.dfy(1015,22): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name or declare a module import 'opened?')
+ResolutionErrors.dfy(1022,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> A
+ResolutionErrors.dfy(1025,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
+ResolutionErrors.dfy(1029,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
+ResolutionErrors.dfy(1038,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed
+ResolutionErrors.dfy(1041,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
+ResolutionErrors.dfy(1046,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
+ResolutionErrors.dfy(1065,21): Error: unresolved identifier: x
+ResolutionErrors.dfy(1072,35): Error: Wrong number of type arguments (2 instead of 1) passed to opaque type: P
+ResolutionErrors.dfy(1084,13): Error: Undeclared top-level type or type parameter: BX (did you forget to qualify a name or declare a module import 'opened?')
+ResolutionErrors.dfy(1094,6): Error: RHS (of type P<int>) not assignable to LHS (of type P<bool>)
+ResolutionErrors.dfy(1099,6): Error: RHS (of type P<A>) not assignable to LHS (of type P<B>)
+ResolutionErrors.dfy(1104,6): Error: RHS (of type P<A>) not assignable to LHS (of type P<int>)
+ResolutionErrors.dfy(1105,6): Error: RHS (of type P<int>) not assignable to LHS (of type P<A>)
+ResolutionErrors.dfy(1110,13): Error: arguments must have the same type (got P<int> and P<X>)
+ResolutionErrors.dfy(1111,13): Error: arguments must have the same type (got P<bool> and P<X>)
+ResolutionErrors.dfy(1112,13): Error: arguments must have the same type (got P<int> and P<bool>)
+ResolutionErrors.dfy(1130,31): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'o'
+ResolutionErrors.dfy(1132,38): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'o'
+ResolutionErrors.dfy(1137,24): Error: set comprehensions in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'o'
+ResolutionErrors.dfy(1230,13): Error: type variable 'PT' in the function call to 'P' could not be determined
+ResolutionErrors.dfy(1231,14): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(1231,19): Error: type variable 'QT' in the function call to 'Q' could not be determined
+ResolutionErrors.dfy(1232,4): Error: type '?' to the method 'M' is not determined
+ResolutionErrors.dfy(1233,8): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(1233,13): Error: type '?' to the method 'N' is not determined
+ResolutionErrors.dfy(1234,8): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(1235,8): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(1236,8): Error: the type of this local variable is underspecified
+ResolutionErrors.dfy(1237,8): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(1238,8): Error: the type of this local variable is underspecified
+ResolutionErrors.dfy(1242,26): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(1242,21): Error: type of bound variable 's' could not be determined; please specify the type explicitly
+ResolutionErrors.dfy(1243,31): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(1243,21): Error: type of bound variable 's' could not be determined; please specify the type explicitly
+ResolutionErrors.dfy(1244,29): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(1244,21): Error: type of bound variable 'c' could not be determined; please specify the type explicitly
+ResolutionErrors.dfy(1251,8): Error: the type of this local variable is underspecified
+ResolutionErrors.dfy(1254,29): Error: type of bound variable 'c' could not be determined; please specify the type explicitly
+ResolutionErrors.dfy(1270,21): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name or declare a module import 'opened?')
+ResolutionErrors.dfy(1271,24): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name or declare a module import 'opened?')
+ResolutionErrors.dfy(1308,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (y)
+ResolutionErrors.dfy(1318,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(1346,15): Error: The name Inner ambiguously refers to a type in one of the modules A, B (try qualifying the type name with the module name)
+ResolutionErrors.dfy(1356,29): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(1358,49): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(1358,54): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(1379,11): Error: name of type (X) is used as a variable
+ResolutionErrors.dfy(1379,16): Error: name of type (X) is used as a variable
+ResolutionErrors.dfy(1380,11): Error: name of module (Y) is used as a variable
+ResolutionErrors.dfy(1380,16): Error: name of module (Y) is used as a variable
+ResolutionErrors.dfy(1381,11): Error: name of type (X) is used as a variable
+ResolutionErrors.dfy(1381,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<real, string>)
+ResolutionErrors.dfy(1382,11): Error: name of module (Y) is used as a variable
+ResolutionErrors.dfy(1382,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<real, string>)
+ResolutionErrors.dfy(1387,16): Error: name of type (X) is used as a variable
+ResolutionErrors.dfy(1387,13): Error: arguments must have the same type (got int and #type)
+ResolutionErrors.dfy(1388,16): Error: name of module (Y) is used as a variable
+ResolutionErrors.dfy(1388,13): Error: arguments must have the same type (got int and #module)
+ResolutionErrors.dfy(1389,4): Error: name of type (X) is used as a variable
+ResolutionErrors.dfy(1390,4): Error: name of module (Y) is used as a variable
+ResolutionErrors.dfy(1399,11): Error: type of RHS of assign-such-that statement must be boolean (got int)
+ResolutionErrors.dfy(1400,9): Error: type of RHS of assign-such-that statement must be boolean (got int)
+ResolutionErrors.dfy(1401,13): Error: type of RHS of assign-such-that statement must be boolean (got int)
+ResolutionErrors.dfy(1404,15): Error: type of RHS of let-such-that expression must be boolean (got int)
+ResolutionErrors.dfy(1447,20): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(1469,18): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(1470,23): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(1471,20): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(1474,21): Error: a while statement used inside a hint is not allowed to have a modifies clause
+ResolutionErrors.dfy(1456,24): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(1469,18): 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(1498,18): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(1499,23): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(1500,11): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(1503,21): Error: a while statement used inside a hint is not allowed to have a modifies clause
+ResolutionErrors.dfy(1491,24): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(1498,18): 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(1527,20): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(1420,29): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(1422,17): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(1538,16): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating
+ResolutionErrors.dfy(1556,12): Error: trying to break out of more loop levels than there are enclosing loops
+ResolutionErrors.dfy(1568,16): Error: ghost fields are allowed only in specification contexts
+ResolutionErrors.dfy(1575,9): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(1581,4): Error: non-ghost variable cannot be assigned a value that depends on a ghost
+ResolutionErrors.dfy(1598,8): 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(1607,26): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(1615,6): Error: the type of the bound variable 't' could not be determined
+ResolutionErrors.dfy(1633,15): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(1635,10): 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(1660,15): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(1662,25): 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)
+ResolutionErrors.dfy(1663,35): 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)
+ResolutionErrors.dfy(1673,4): Error: 'decreases *' is not allowed on ghost loops
+ResolutionErrors.dfy(1677,8): 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)
+ResolutionErrors.dfy(1687,4): Error: 'decreases *' is not allowed on ghost loops
+ResolutionErrors.dfy(1691,29): 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)
+ResolutionErrors.dfy(469,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')
+ResolutionErrors.dfy(92,14): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
+ResolutionErrors.dfy(93,14): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
+ResolutionErrors.dfy(95,14): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
+ResolutionErrors.dfy(97,18): Error: wrong number of arguments to datatype constructor David (found 2, expected 1)
+ResolutionErrors.dfy(475,14): Error: when allocating an object of type 'YHWH', one of its constructor methods must be called
+ResolutionErrors.dfy(480,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called
+ResolutionErrors.dfy(481,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called
+ResolutionErrors.dfy(483,9): Error: class Lamb does not have an anonymous constructor
+ResolutionErrors.dfy(853,11): Error: a modifies-clause expression must denote an object or a collection of objects (instead got int)
+ResolutionErrors.dfy(857,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(1053,23): Error: unresolved identifier: x
+ResolutionErrors.dfy(1056,20): Error: unresolved identifier: x
+ResolutionErrors.dfy(1059,23): Error: unresolved identifier: x
+ResolutionErrors.dfy(1061,19): Error: unresolved identifier: x
+ResolutionErrors.dfy(1063,19): Error: unresolved identifier: x
+ResolutionErrors.dfy(12,16): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating
ResolutionErrors.dfy(24,11): Error: array selection requires an array2 (got array3<T>)
ResolutionErrors.dfy(25,12): Error: sequence/array/multiset/map selection requires a sequence, array, multiset, or map (got array3<T>)
ResolutionErrors.dfy(26,11): Error: array selection requires an array4 (got array<T>)
@@ -162,42 +192,36 @@ ResolutionErrors.dfy(62,14): Error: accessing member 'M' requires an instance ex ResolutionErrors.dfy(63,7): Error: unresolved identifier: N
ResolutionErrors.dfy(66,8): Error: non-function expression (of type int) is called with parameters
ResolutionErrors.dfy(67,14): Error: member 'z' does not exist in type 'Global'
-ResolutionErrors.dfy(260,4): Error: label shadows an enclosing label
-ResolutionErrors.dfy(265,2): Error: duplicate label
-ResolutionErrors.dfy(291,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
-ResolutionErrors.dfy(292,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
-ResolutionErrors.dfy(294,9): Error: a constructor is allowed to be called only when an object is being allocated
-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>)
-ResolutionErrors.dfy(367,6): Error: arguments to + must be of a numeric type or a collection type (instead got bool)
-ResolutionErrors.dfy(372,6): Error: all lines in a calculation must have the same type (got int after bool)
-ResolutionErrors.dfy(375,6): Error: first argument to ==> must be of type bool (instead got int)
-ResolutionErrors.dfy(375,6): Error: second argument to ==> must be of type bool (instead got int)
-ResolutionErrors.dfy(376,10): Error: first argument to ==> must be of type bool (instead got int)
-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(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
-ResolutionErrors.dfy(929,32): Error: RHS (of type (int,int,real)) not assignable to LHS (of type (int,real,int))
-ResolutionErrors.dfy(930,37): Error: RHS (of type (int,real,int)) not assignable to LHS (of type (int,real,int,real))
-ResolutionErrors.dfy(936,16): Error: condition is expected to be of type bool, but is int
-ResolutionErrors.dfy(937,16): Error: member 3 does not exist in datatype _tuple#3
-ResolutionErrors.dfy(937,26): Error: member x does not exist in datatype _tuple#2
-ResolutionErrors.dfy(960,15): Error: arguments to / must have the same type (got real and int)
-ResolutionErrors.dfy(961,10): Error: second argument to % must be of type int (instead got real)
-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
+ResolutionErrors.dfy(301,4): Error: label shadows an enclosing label
+ResolutionErrors.dfy(306,2): Error: duplicate label
+ResolutionErrors.dfy(332,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
+ResolutionErrors.dfy(333,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
+ResolutionErrors.dfy(335,9): Error: a constructor is allowed to be called only when an object is being allocated
+ResolutionErrors.dfy(349,16): Error: arguments must have the same type (got int and DTD_List)
+ResolutionErrors.dfy(350,16): Error: arguments must have the same type (got DTD_List and int)
+ResolutionErrors.dfy(351,25): Error: arguments must have the same type (got bool and int)
+ResolutionErrors.dfy(387,5): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)
+ResolutionErrors.dfy(399,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList<int>)
+ResolutionErrors.dfy(407,6): Error: arguments to + must be of a numeric type or a collection type (instead got bool)
+ResolutionErrors.dfy(412,6): Error: all lines in a calculation must have the same type (got int after bool)
+ResolutionErrors.dfy(415,6): Error: first argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(415,6): Error: second argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(416,10): Error: first argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(416,10): Error: second argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(421,10): Error: first argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(421,10): Error: second argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(580,18): Error: unresolved identifier: w
+ResolutionErrors.dfy(686,11): Error: lemmas are not allowed to have modifies clauses
+ResolutionErrors.dfy(935,9): Error: unresolved identifier: s
+ResolutionErrors.dfy(946,32): Error: RHS (of type (int,int,real)) not assignable to LHS (of type (int,real,int))
+ResolutionErrors.dfy(947,37): Error: RHS (of type (int,real,int)) not assignable to LHS (of type (int,real,int,real))
+ResolutionErrors.dfy(953,16): Error: condition is expected to be of type bool, but is int
+ResolutionErrors.dfy(954,16): Error: member 3 does not exist in datatype _tuple#3
+ResolutionErrors.dfy(954,26): Error: member x does not exist in datatype _tuple#2
+ResolutionErrors.dfy(977,15): Error: arguments to / must have the same type (got real and int)
+ResolutionErrors.dfy(978,10): Error: second argument to % must be of type int (instead got real)
+ResolutionErrors.dfy(1123,8): Error: new cannot be applied to a trait
+ResolutionErrors.dfy(1144,13): Error: first argument to / must be of numeric type (instead got set<bool>)
+ResolutionErrors.dfy(1151,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(1166,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating
+226 resolution/type errors detected in ResolutionErrors.dfy
diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy index b44f4d68..a9d473f6 100644 --- a/Test/dafny0/TypeTests.dfy +++ b/Test/dafny0/TypeTests.dfy @@ -39,7 +39,7 @@ datatype ReverseOrder_TheCounterpart<T> = // ---------------------
-class ArrayTests {
+module ArrayTests {
ghost method G(a: array<int>)
requires a != null && 10 <= a.Length;
modifies a;
@@ -167,31 +167,33 @@ module Expl_Module { // --------------------- more ghost tests, for assign-such-that statements
-method M()
-{
- ghost var b: bool;
- ghost var k: int, l: int;
- var m: int;
-
- k :| k < 10;
- 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
- // assignments to ghosts are allowed.
- if (b) {
- k :| k < 10; // should be allowed
- k, l :| 0 <= k < l; // ditto
- }
- if (b) {
- m :| m < 10; // error: not allowed in ghost context
- k, m :| 0 <= k < m; // error: not allowed in ghost context
+module MoreGhostTests {
+ method M()
+ {
+ ghost var b: bool;
+ ghost var k: int, l: int;
+ var m: int;
+
+ k :| k < 10;
+ 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
+ // assignments to ghosts are allowed.
+ if (b) {
+ k :| k < 10; // should be allowed
+ k, l :| 0 <= k < l; // ditto
+ }
+ if (b) {
+ m :| m < 10; // error: not allowed in ghost context
+ k, m :| 0 <= k < m; // error: not allowed in ghost context
+ }
}
-}
-ghost method GhostM() returns (x: int)
-{
- x :| true; // no problem (but there once was a problem with this case, where an error was generated for no reason)
+ ghost method GhostM() returns (x: int)
+ {
+ x :| true; // no problem (but there once was a problem with this case, where an error was generated for no reason)
+ }
}
// ------------------ cycles that could arise from proxy assignments ---------
diff --git a/Test/dafny0/TypeTests.dfy.expect b/Test/dafny0/TypeTests.dfy.expect index 500b1af9..de0bfbed 100644 --- a/Test/dafny0/TypeTests.dfy.expect +++ b/Test/dafny0/TypeTests.dfy.expect @@ -1,6 +1,10 @@ -TypeTests.dfy(205,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt<?>)
-TypeTests.dfy(211,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt<?>)
-TypeTests.dfy(218,6): Error: RHS (of type set<?>) not assignable to LHS (of type ?)
+TypeTests.dfy(47,9): Error: 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)
+TypeTests.dfy(178,7): Error: non-ghost variable cannot be assigned a value that depends on a ghost
+TypeTests.dfy(188,6): Error: cannot assign to non-ghost variable in a ghost context
+TypeTests.dfy(189,9): Error: cannot assign to non-ghost variable in a ghost context
+TypeTests.dfy(207,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt<?>)
+TypeTests.dfy(213,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt<?>)
+TypeTests.dfy(220,6): Error: RHS (of type set<?>) not assignable to LHS (of type ?)
TypeTests.dfy(7,17): Error: type mismatch for argument 0 (function expects C, got D)
TypeTests.dfy(7,20): Error: type mismatch for argument 1 (function expects D, got C)
TypeTests.dfy(8,15): Error: type mismatch for argument 0 (function expects C, got int)
@@ -8,7 +12,6 @@ TypeTests.dfy(8,18): Error: type mismatch for argument 1 (function expects D, go TypeTests.dfy(14,16): Error: incorrect type of method in-parameter 0 (expected int, got bool)
TypeTests.dfy(15,12): Error: incorrect type of method out-parameter 0 (expected int, got C)
TypeTests.dfy(15,12): Error: incorrect type of method out-parameter 1 (expected C, got int)
-TypeTests.dfy(47,9): Error: 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)
TypeTests.dfy(56,6): Error: Duplicate local-variable name: z
TypeTests.dfy(58,6): Error: Duplicate local-variable name: x
TypeTests.dfy(61,8): Error: Duplicate local-variable name: x
@@ -56,8 +59,5 @@ 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(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
62 resolution/type errors detected in TypeTests.dfy
diff --git a/Test/dafny1/MoreInduction.dfy.expect b/Test/dafny1/MoreInduction.dfy.expect index 7da5e2ec..5de0ace6 100644 --- a/Test/dafny1/MoreInduction.dfy.expect +++ b/Test/dafny1/MoreInduction.dfy.expect @@ -1,6 +1,5 @@ MoreInduction.dfy(78,0): Error BP5003: A postcondition might not hold on this return path.
MoreInduction.dfy(77,10): Related location: This is the postcondition that might not hold.
-MoreInduction.dfy(77,32): Related location
Execution trace:
(0,0): anon0
MoreInduction.dfy(83,0): Error BP5003: A postcondition might not hold on this return path.
@@ -9,7 +8,6 @@ Execution trace: (0,0): anon0
MoreInduction.dfy(88,0): Error BP5003: A postcondition might not hold on this return path.
MoreInduction.dfy(87,10): Related location: This is the postcondition that might not hold.
-MoreInduction.dfy(87,43): Related location
Execution trace:
(0,0): anon0
MoreInduction.dfy(93,0): Error BP5003: A postcondition might not hold on this return path.
diff --git a/Test/dafny4/Leq.dfy b/Test/dafny4/Leq.dfy new file mode 100644 index 00000000..0491dd00 --- /dev/null +++ b/Test/dafny4/Leq.dfy @@ -0,0 +1,174 @@ +// RUN: %dafny /rprint:"%t.rprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// Rustan Leino, 22 Sep 2015.
+// This file considers two definitions of Leq on naturals+infinity. One
+// definition uses the least fixpoint, the other the greatest fixpoint.
+
+// Nat represents natural numbers extended with infinity
+codatatype Nat = Z | S(pred: Nat)
+
+function Num(n: nat): Nat
+{
+ if n == 0 then Z else S(Num(n-1))
+}
+
+predicate IsFinite(a: Nat)
+{
+ exists m:nat :: a == Num(m)
+}
+
+copredicate IsInfinity(a: Nat)
+{
+ a.S? && IsInfinity(a.pred)
+}
+
+lemma NatCases(a: Nat)
+ ensures IsFinite(a) || IsInfinity(a)
+{
+ if IsFinite(a) {
+ } else {
+ NatCasesAux(a);
+ }
+}
+colemma NatCasesAux(a: Nat)
+ requires !IsFinite(a)
+ ensures IsInfinity(a)
+{
+ assert a != Num(0);
+ if IsFinite(a.pred) {
+ // going for a contradiction
+ var m:nat :| a.pred == Num(m);
+ assert a == Num(m+1);
+ assert false; // the case is absurd
+ }
+ NatCasesAux(a.pred);
+}
+
+// ----------- inductive semantics (more precisely, a least-fixpoint definition of Leq)
+
+inductive predicate Leq(a: Nat, b: Nat)
+{
+ a == Z ||
+ (a.S? && b.S? && Leq(a.pred, b.pred))
+}
+
+lemma LeqTheorem(a: Nat, b: Nat)
+ ensures Leq(a, b) <==>
+ exists m:nat :: a == Num(m) &&
+ (IsInfinity(b) || exists n:nat :: b == Num(n) && m <= n)
+{
+ if exists m:nat,n:nat :: a == Num(m) && b == Num(n) && m <= n {
+ var m:nat,n:nat :| a == Num(m) && b == Num(n) && m <= n;
+ Leq0_finite(m, n);
+ }
+ if (exists m:nat :: a == Num(m)) && IsInfinity(b) {
+ var m:nat :| a == Num(m);
+ Leq0_infinite(m, b);
+ }
+ if Leq(a, b) {
+ var k:nat :| Leq#[k](a, b);
+ var m, n := Leq1(k, a, b);
+ }
+}
+
+lemma Leq0_finite(m: nat, n: nat)
+ requires m <= n
+ ensures Leq(Num(m), Num(n))
+{
+ // proof is automatic
+}
+
+lemma Leq0_infinite(m: nat, b: Nat)
+ requires IsInfinity(b)
+ ensures Leq(Num(m), b)
+{
+ // proof is automatic
+}
+
+lemma Leq1(k: nat, a: Nat, b: Nat) returns (m: nat, n: nat)
+ requires Leq#[k](a, b)
+ ensures a == Num(m)
+ ensures IsInfinity(b) || (b == Num(n) && m <= n)
+{
+ if a == Z {
+ m := 0;
+ NatCases(b);
+ if !IsInfinity(b) {
+ n :| b == Num(n);
+ }
+ } else {
+ assert a.S? && b.S? && Leq(a.pred, b.pred);
+ m,n := Leq1(k-1, a.pred, b.pred);
+ m, n := m + 1, n + 1;
+ }
+}
+
+// ----------- co-inductive semantics (more precisely, a greatest-fixpoint definition of Leq)
+
+copredicate CoLeq(a: Nat, b: Nat)
+{
+ a == Z ||
+ (a.S? && b.S? && CoLeq(a.pred, b.pred))
+}
+
+lemma CoLeqTheorem(a: Nat, b: Nat)
+ ensures CoLeq(a, b) <==>
+ IsInfinity(b) ||
+ exists m:nat,n:nat :: a == Num(m) && b == Num(n) && m <= n
+{
+ if IsInfinity(b) {
+ CoLeq0_infinite(a, b);
+ }
+ if exists m:nat,n:nat :: a == Num(m) && b == Num(n) && m <= n {
+ var m:nat,n:nat :| a == Num(m) && b == Num(n) && m <= n;
+ CoLeq0_finite(m, n);
+ }
+ if CoLeq(a, b) {
+ CoLeq1(a, b);
+ }
+}
+
+lemma CoLeq0_finite(m: nat, n: nat)
+ requires m <= n
+ ensures CoLeq(Num(m), Num(n))
+{
+ // proof is automatic
+}
+
+colemma CoLeq0_infinite(a: Nat, b: Nat)
+ requires IsInfinity(b)
+ ensures CoLeq(a, b)
+{
+ // proof is automatic
+}
+
+lemma CoLeq1(a: Nat, b: Nat)
+ requires CoLeq(a, b)
+ ensures IsInfinity(b) || exists m:nat,n:nat :: a == Num(m) && b == Num(n) && m <= n
+{
+ var m,n := CoLeq1'(a, b);
+}
+
+lemma CoLeq1'(a: Nat, b: Nat) returns (m: nat, n: nat)
+ requires CoLeq(a, b)
+ ensures IsInfinity(b) || (a == Num(m) && b == Num(n) && m <= n)
+{
+ if !IsInfinity(b) {
+ NatCases(b);
+ n :| b == Num(n);
+ m := CoLeq1Aux(a, n);
+ }
+}
+
+lemma CoLeq1Aux(a: Nat, n: nat) returns (m: nat)
+ requires CoLeq(a, Num(n))
+ ensures a == Num(m) && m <= n
+{
+ if a == Z {
+ m := 0;
+ } else {
+ m := CoLeq1Aux(a.pred, n-1);
+ m := m + 1;
+ }
+}
diff --git a/Test/dafny4/Leq.dfy.expect b/Test/dafny4/Leq.dfy.expect new file mode 100644 index 00000000..754c1e55 --- /dev/null +++ b/Test/dafny4/Leq.dfy.expect @@ -0,0 +1,3 @@ +
+Dafny program verifier finished with 29 verified, 0 errors
+Compiled assembly into Leq.dll
diff --git a/Test/dafny4/Regression0.dfy b/Test/dafny4/Regression0.dfy index be092261..666d9575 100644 --- a/Test/dafny4/Regression0.dfy +++ b/Test/dafny4/Regression0.dfy @@ -4,10 +4,10 @@ // This once crashed Dafny
method M() {
- var s := [1, "2"];
+ var s := [1, "2"]; // error: all elements must have the same type
if * {
- assert exists n :: n in s && n != 1;
+ assert exists n :: n in s && n != 1; // the type of n is inferred to be int
} else {
- assert "2" in s;
+ assert "2" in s; // error: since the type of s wasn't determined
}
}
diff --git a/Test/dafny4/Regression0.dfy.expect b/Test/dafny4/Regression0.dfy.expect index 9d1e3019..566b3e3f 100644 --- a/Test/dafny4/Regression0.dfy.expect +++ b/Test/dafny4/Regression0.dfy.expect @@ -1,4 +1,3 @@ Regression0.dfy(7,15): Error: All elements of display must be of the same type (got string, but type of previous elements is int)
-Regression0.dfy(9,28): Error: the type of this variable is underspecified
Regression0.dfy(11,15): Error: second argument to "in" must be a set, multiset, or sequence with elements of type string, or a map with domain string (instead got ?)
-3 resolution/type errors detected in Regression0.dfy
+2 resolution/type errors detected in Regression0.dfy
diff --git a/Test/dafny4/set-compr.dfy b/Test/dafny4/set-compr.dfy index 71a07f3d..d093a924 100644 --- a/Test/dafny4/set-compr.dfy +++ b/Test/dafny4/set-compr.dfy @@ -22,7 +22,7 @@ method O() returns (ghost p: set<object>) method P() returns (p: set<object>)
{
- p := set o: object | true; // not allowed -- not in a ghost context
+ p := set o: object | true; // error: not (easily) compilable
}
ghost method Q() returns (p: set<object>)
@@ -30,26 +30,54 @@ ghost method Q() returns (p: set<object>) p := set o: object | true; // allowed, since the whole method is ghost
}
-function F(): int
+function F(p: object): int
+ requires p in set o: object | true // error: function is not allowed to depend on allocation state
+ ensures p in set o: object | true // error: ditto (although one could argue that this would be okay)
+ reads set o: object | true // error: same as for 'requires'
+ decreases set o: object | true // error: same as for 'ensures'
+{
+ if p in set o: object | true then // error: function is not allowed to depend on allocation state
+ F(p)
+ else
+ 0
+}
+
+function method G(p: object): int
+ requires p in set o: object | true // error (see F)
+ ensures p in set o: object | true // error (see F)
+ reads set o: object | true // error (see F)
+ decreases set o: object | true // error (see F)
+{
+ if p in set o: object | true then // error (see F)
+ G(p)
+ else
+ 0
+}
+
+method M0() returns (ghost r: int, s: int)
requires null in set o: object | true // allowed
ensures null in set o: object | true // allowed
- reads set o: object | true // allowed
+ modifies set o: object | true // allowed
decreases set o: object | true // allowed
{
- if null in set o: object | true then // allowed -- in a ghost context
- F()
- else
- 0
+ if null in set o: object | true { // this makes the "if" a ghost
+ r := G(null);
+ s := G(null); // error: assignment of non-ghost not allowed inside ghost "if"
+ } else {
+ r := 0;
+ }
}
-function method G(): int
+method M1() returns (ghost r: int, s: int)
requires null in set o: object | true // (X) allowed
ensures null in set o: object | true // (X) allowed
- reads set o: object | true // allowed
+ modifies set o: object | true // allowed
decreases set o: object | true // (X) allowed
{
- if null in set o: object | true then // not allowed, since this is not a ghost context
- G()
- else
- 0
+ if null in set o: object | true { // this makes the "if" a ghost
+ r := G(null);
+ s := G(null); // error: assignment of non-ghost not allowed inside ghost "if"
+ } else {
+ r := 0;
+ }
}
diff --git a/Test/dafny4/set-compr.dfy.expect b/Test/dafny4/set-compr.dfy.expect index b31c6ac0..b0490a11 100644 --- a/Test/dafny4/set-compr.dfy.expect +++ b/Test/dafny4/set-compr.dfy.expect @@ -1,3 +1,14 @@ -set-compr.dfy(25,7): Error: 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 'o'
-set-compr.dfy(51,13): Error: 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 'o'
-2 resolution/type errors detected in set-compr.dfy
+set-compr.dfy(25,7): Error: set comprehensions in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'o'
+set-compr.dfy(34,16): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'o'
+set-compr.dfy(35,15): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'o'
+set-compr.dfy(36,8): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'o'
+set-compr.dfy(37,12): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'o'
+set-compr.dfy(39,10): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'o'
+set-compr.dfy(46,16): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'o'
+set-compr.dfy(47,15): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'o'
+set-compr.dfy(48,8): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'o'
+set-compr.dfy(49,12): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'o'
+set-compr.dfy(51,10): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'o'
+set-compr.dfy(65,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)
+set-compr.dfy(79,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)
+13 resolution/type errors detected in set-compr.dfy
diff --git a/Test/hofs/ReadsReads.dfy b/Test/hofs/ReadsReads.dfy index a6f8d922..60ac35f5 100644 --- a/Test/hofs/ReadsReads.dfy +++ b/Test/hofs/ReadsReads.dfy @@ -105,14 +105,14 @@ module WhatWeKnowAboutReads { module ReadsAll { function A(f: int -> int) : int - reads set o,x | o in f.reads(x) :: o + reads set x,o | o in f.reads(x) :: o // note, with "set o,x ..." instead, Dafny complains (this is perhaps less than ideal) requires forall x :: f.requires(x) { f(0) + f(1) + f(2) } function method B(f: int -> int) : int - reads set o,x | o in f.reads(x) :: o + reads set x,o | o in f.reads(x) :: o // note, with "set o,x ..." instead, Dafny complains (this is perhaps less than ideal) requires forall x :: f.requires(x) { f(0) + f(1) + f(2) |