From a297fb4b9e6c0b915b5bb5bd85050b26a9ed7e3b Mon Sep 17 00:00:00 2001 From: Michael Lowell Roberts Date: Fri, 12 Jun 2015 11:12:35 -0700 Subject: added -optimize option to compiler. --- Binaries/DafnyRuntime.cs | 506 +++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 449 insertions(+), 57 deletions(-) (limited to 'Binaries/DafnyRuntime.cs') diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs index fd680a0b..7d3799d8 100644 --- a/Binaries/DafnyRuntime.cs +++ b/Binaries/DafnyRuntime.cs @@ -4,39 +4,430 @@ using System.Numerics; namespace Dafny { using System.Collections.Generic; +// set this option if you want to use System.Collections.Immutable and if you know what you're doing. +#if DAFNY_USE_SYSTEM_COLLECTIONS_IMMUTABLE + using System.Collections.Immutable; + using System.Linq; public class Set { - Dictionary dict; - Set(Dictionary d) { + readonly ImmutableHashSet setImpl; + Set(ImmutableHashSet d) { + this.setImpl = d; + } + public static readonly Set Empty = new Set(ImmutableHashSet.Empty); + public static Set FromElements(params T[] values) { + return FromElements((IEnumerable)values); + } + public static Set FromElements(IEnumerable values) { + var d = ImmutableHashSet.Empty.ToBuilder(); + foreach (T t in values) + d.Add(t); + return new Set(d.ToImmutable()); + } + public static Set FromCollection(ICollection values) { + var d = ImmutableHashSet.Empty.ToBuilder(); + foreach (T t in values) + d.Add(t); + return new Set(d.ToImmutable()); + } + public int Length { + get { return this.setImpl.Count; } + } + public long LongLength { + get { return this.setImpl.Count; } + } + public IEnumerable Elements { + get { + return this.setImpl; + } + } + /// + /// This is an inefficient iterator for producing all subsets of "this". Each set returned is the same + /// Set object (but this Set object is fresh; in particular, it is not "this"). + /// + public IEnumerable> AllSubsets { + get { + // Start by putting all set elements into a list + var elmts = new List(); + elmts.AddRange(this.setImpl); + var n = elmts.Count; + var which = new bool[n]; + var s = ImmutableHashSet.Empty.ToBuilder(); + while (true) { + yield return new Set(s.ToImmutable()); + // "add 1" to "which", as if doing a carry chain. For every digit changed, change the membership of the corresponding element in "s". + int i = 0; + for (; i < n && which[i]; i++) { + which[i] = false; + s.Remove(elmts[i]); + } + if (i == n) { + // we have cycled through all the subsets + break; + } + which[i] = true; + s.Add(elmts[i]); + } + } + } + public bool Equals(Set other) { + return this.setImpl.Equals(other.setImpl); + } + public override bool Equals(object other) { + var otherSet = other as Set; + return otherSet != null && Equals(otherSet); + } + public override int GetHashCode() { + var hashCode = 1; + foreach (var t in this.setImpl) { + hashCode = hashCode * (t.GetHashCode()+3); + } + return hashCode; + } + public override string ToString() { + var s = "{"; + var sep = ""; + foreach (var t in this.setImpl) { + s += sep + t.ToString(); + sep = ", "; + } + return s + "}"; + } + public bool IsProperSubsetOf(Set other) { + return IsProperSubsetOf(other); + } + public bool IsSubsetOf(Set other) { + return IsSubsetOf(other); + } + public bool IsSupersetOf(Set other) { + return other.IsSupersetOf(this); + } + public bool IsProperSupersetOf(Set other) { + return other.IsProperSupersetOf(this); + } + public bool IsDisjointFrom(Set other) { + ImmutableHashSet a, b; + if (this.setImpl.Count < other.setImpl.Count) { + a = this.setImpl; b = other.setImpl; + } else { + a = other.setImpl; b = this.setImpl; + } + foreach (T t in a) { + if (b.Contains(t)) + return false; + } + return true; + } + public bool Contains(T t) { + return this.setImpl.Contains(t); + } + public Set Union(Set other) { + return new Set(this.setImpl.Union(other.setImpl)); + } + public Set Intersect(Set other) { + return new Set(this.setImpl.Intersect(other.setImpl)); + } + public Set Difference(Set other) { + return new Set(this.setImpl.Except(other.setImpl)); + } + } + public partial class MultiSet + { + + readonly ImmutableDictionary dict; + MultiSet(ImmutableDictionary d) { dict = d; } + public static readonly MultiSet Empty = new MultiSet(ImmutableDictionary.Empty); + public static MultiSet FromElements(params T[] values) { + var d = ImmutableDictionary.Empty.ToBuilder(); + foreach (T t in values) { + var i = 0; + if (!d.TryGetValue(t, out i)) { + i = 0; + } + d[t] = i + 1; + } + return new MultiSet(d.ToImmutable()); + } + public static MultiSet FromCollection(ICollection values) { + var d = ImmutableDictionary.Empty.ToBuilder(); + foreach (T t in values) { + var i = 0; + if (!d.TryGetValue(t, out i)) { + i = 0; + } + d[t] = i + 1; + } + return new MultiSet(d.ToImmutable()); + } + public static MultiSet FromSeq(Sequence values) { + var d = ImmutableDictionary.Empty.ToBuilder(); + foreach (T t in values.Elements) { + var i = 0; + if (!d.TryGetValue(t, out i)) { + i = 0; + } + d[t] = i + 1; + } + return new MultiSet(d.ToImmutable()); + } + public static MultiSet FromSet(Set values) { + var d = ImmutableDictionary.Empty.ToBuilder(); + foreach (T t in values.Elements) { + d[t] = 1; + } + return new MultiSet(d.ToImmutable()); + } + + public bool Equals(MultiSet other) { + return other.IsSubsetOf(this) && this.IsSubsetOf(other); + } + public override bool Equals(object other) { + return other is MultiSet && Equals((MultiSet)other); + } + public override int GetHashCode() { + var hashCode = 1; + foreach (var kv in dict) { + var key = kv.Key.GetHashCode(); + key = (key << 3) | (key >> 29) ^ kv.Value.GetHashCode(); + hashCode = hashCode * (key + 3); + } + return hashCode; + } + public override string ToString() { + var s = "multiset{"; + var sep = ""; + foreach (var kv in dict) { + var t = kv.Key.ToString(); + for (int i = 0; i < kv.Value; i++) { + s += sep + t.ToString(); + sep = ", "; + } + } + return s + "}"; + } + public bool IsProperSubsetOf(MultiSet other) { + return !Equals(other) && IsSubsetOf(other); + } + public bool IsSubsetOf(MultiSet other) { + foreach (T t in dict.Keys) { + if (!other.dict.ContainsKey(t) || other.dict[t] < dict[t]) + return false; + } + return true; + } + public bool IsSupersetOf(MultiSet other) { + return other.IsSubsetOf(this); + } + public bool IsProperSupersetOf(MultiSet other) { + return other.IsProperSubsetOf(this); + } + public bool IsDisjointFrom(MultiSet other) { + foreach (T t in dict.Keys) { + if (other.dict.ContainsKey(t)) + return false; + } + foreach (T t in other.dict.Keys) { + if (dict.ContainsKey(t)) + return false; + } + return true; + } + public bool Contains(T t) { + return dict.ContainsKey(t); + } + public MultiSet Union(MultiSet other) { + if (dict.Count == 0) + return other; + else if (other.dict.Count == 0) + return this; + var r = ImmutableDictionary.Empty.ToBuilder(); + foreach (T t in dict.Keys) { + var i = 0; + if (!r.TryGetValue(t, out i)) { + i = 0; + } + r[t] = i + dict[t]; + } + foreach (T t in other.dict.Keys) { + var i = 0; + if (!r.TryGetValue(t, out i)) { + i = 0; + } + r[t] = i + other.dict[t]; + } + return new MultiSet(r.ToImmutable()); + } + public MultiSet Intersect(MultiSet other) { + if (dict.Count == 0) + return this; + else if (other.dict.Count == 0) + return other; + var r = ImmutableDictionary.Empty.ToBuilder(); + foreach (T t in dict.Keys) { + if (other.dict.ContainsKey(t)) { + r[t] = other.dict[t] < dict[t] ? other.dict[t] : dict[t]; + } + } + return new MultiSet(r.ToImmutable()); + } + public MultiSet Difference(MultiSet other) { // \result == this - other + if (dict.Count == 0) + return this; + else if (other.dict.Count == 0) + return this; + var r = ImmutableDictionary.Empty.ToBuilder(); + foreach (T t in dict.Keys) { + if (!other.dict.ContainsKey(t)) { + r[t] = dict[t]; + } else if (other.dict[t] < dict[t]) { + r[t] = dict[t] - other.dict[t]; + } + } + return new MultiSet(r.ToImmutable()); + } + public IEnumerable Elements { + get { + foreach (T t in dict.Keys) { + int n; + dict.TryGetValue(t, out n); + for (int i = 0; i < n; i ++) { + yield return t; + } + } + } + } + } + + public partial class Map + { + readonly ImmutableDictionary dict; + Map(ImmutableDictionary d) { + dict = d; + } + public static readonly Map Empty = new Map(ImmutableDictionary.Empty); + public static Map FromElements(params Pair[] values) { + var d = ImmutableDictionary.Empty.ToBuilder(); + foreach (Pair p in values) { + d[p.Car] = p.Cdr; + } + return new Map(d.ToImmutable()); + } + public static Map FromCollection(List> values) { + var d = ImmutableDictionary.Empty.ToBuilder(); + foreach (Pair p in values) { + d[p.Car] = p.Cdr; + } + return new Map(d.ToImmutable()); + } + public int Length { + get { return dict.Count; } + } + public long LongLength { + get { return dict.Count; } + } + public bool Equals(Map other) { + foreach (U u in dict.Keys) { + V v1, v2; + if (!dict.TryGetValue(u, out v1)) { + return false; // this shouldn't happen + } + if (!other.dict.TryGetValue(u, out v2)) { + return false; // other dictionary does not contain this element + } + if (!v1.Equals(v2)) { + return false; + } + } + foreach (U u in other.dict.Keys) { + if (!dict.ContainsKey(u)) { + return false; // this shouldn't happen + } + } + return true; + } + public override bool Equals(object other) { + return other is Map && Equals((Map)other); + } + public override int GetHashCode() { + var hashCode = 1; + foreach (var kv in dict) { + var key = kv.Key.GetHashCode(); + key = (key << 3) | (key >> 29) ^ kv.Value.GetHashCode(); + hashCode = hashCode * (key + 3); + } + return hashCode; + } + public override string ToString() { + var s = "map["; + var sep = ""; + foreach (var kv in dict) { + s += sep + kv.Key.ToString() + " := " + kv.Value.ToString(); + sep = ", "; + } + return s + "]"; + } + public bool IsDisjointFrom(Map other) { + foreach (U u in dict.Keys) { + if (other.dict.ContainsKey(u)) + return false; + } + foreach (U u in other.dict.Keys) { + if (dict.ContainsKey(u)) + return false; + } + return true; + } + public bool Contains(U u) { + return dict.ContainsKey(u); + } + public V Select(U index) { + return dict[index]; + } + public Map Update(U index, V val) { + return new Map(dict.SetItem(index, val)); + } + public IEnumerable Domain { + get { + return dict.Keys; + } + } + } +#else // !def DAFNY_USE_SYSTEM_COLLECTIONS_IMMUTABLE + public class Set + { + HashSet set; + Set(HashSet s) { + this.set = s; + } public static Set Empty { get { - return new Set(new Dictionary(0)); + return new Set(new HashSet()); } } public static Set FromElements(params T[] values) { - Dictionary d = new Dictionary(values.Length); + var s = new HashSet(); foreach (T t in values) - d[t] = true; - return new Set(d); + s.Add(t); + return new Set(s); } public static Set FromCollection(ICollection values) { - Dictionary d = new Dictionary(); + HashSet s = new HashSet(); foreach (T t in values) - d[t] = true; - return new Set(d); + s.Add(t); + return new Set(s); } public int Length { - get { return dict.Count; } + get { return this.set.Count; } } public long LongLength { - get { return dict.Count; } + get { return this.set.Count; } } public IEnumerable Elements { get { - return dict.Keys; + return this.set; } } /// @@ -47,36 +438,36 @@ namespace Dafny get { // Start by putting all set elements into a list var elmts = new List(); - elmts.AddRange(dict.Keys); + elmts.AddRange(this.set); var n = elmts.Count; var which = new bool[n]; - var s = new Set(new Dictionary(0)); + var s = new Set(new HashSet()); while (true) { yield return s; // "add 1" to "which", as if doing a carry chain. For every digit changed, change the membership of the corresponding element in "s". int i = 0; for (; i < n && which[i]; i++) { which[i] = false; - s.dict.Remove(elmts[i]); + s.set.Remove(elmts[i]); } if (i == n) { // we have cycled through all the subsets break; } which[i] = true; - s.dict.Add(elmts[i], true); + s.set.Add(elmts[i]); } } } public bool Equals(Set other) { - return dict.Count == other.dict.Count && IsSubsetOf(other); + return this.set.Count == other.set.Count && IsSubsetOf(other); } public override bool Equals(object other) { return other is Set && Equals((Set)other); } public override int GetHashCode() { var hashCode = 1; - foreach (var t in dict.Keys) { + foreach (var t in this.set) { hashCode = hashCode * (t.GetHashCode()+3); } return hashCode; @@ -84,20 +475,20 @@ namespace Dafny public override string ToString() { var s = "{"; var sep = ""; - foreach (var t in dict.Keys) { + foreach (var t in this.set) { s += sep + t.ToString(); sep = ", "; } return s + "}"; } public bool IsProperSubsetOf(Set other) { - return dict.Count < other.dict.Count && IsSubsetOf(other); + return this.set.Count < other.set.Count && IsSubsetOf(other); } public bool IsSubsetOf(Set other) { - if (other.dict.Count < dict.Count) + if (other.set.Count < this.set.Count) return false; - foreach (T t in dict.Keys) { - if (!other.dict.ContainsKey(t)) + foreach (T t in this.set) { + if (!other.set.Contains(t)) return false; } return true; @@ -109,66 +500,66 @@ namespace Dafny return other.IsProperSubsetOf(this); } public bool IsDisjointFrom(Set other) { - Dictionary a, b; - if (dict.Count < other.dict.Count) { - a = dict; b = other.dict; + HashSet a, b; + if (this.set.Count < other.set.Count) { + a = this.set; b = other.set; } else { - a = other.dict; b = dict; + a = other.set; b = this.set; } - foreach (T t in a.Keys) { - if (b.ContainsKey(t)) + foreach (T t in a) { + if (b.Contains(t)) return false; } return true; } public bool Contains(T t) { - return dict.ContainsKey(t); + return this.set.Contains(t); } public Set Union(Set other) { - if (dict.Count == 0) + if (this.set.Count == 0) return other; - else if (other.dict.Count == 0) + else if (other.set.Count == 0) return this; - Dictionary a, b; - if (dict.Count < other.dict.Count) { - a = dict; b = other.dict; + HashSet a, b; + if (this.set.Count < other.set.Count) { + a = this.set; b = other.set; } else { - a = other.dict; b = dict; + a = other.set; b = this.set; } - Dictionary r = new Dictionary(); - foreach (T t in b.Keys) - r[t] = true; - foreach (T t in a.Keys) - r[t] = true; + var r = new HashSet(); + foreach (T t in b) + r.Add(t); + foreach (T t in a) + r.Add(t); return new Set(r); } public Set Intersect(Set other) { - if (dict.Count == 0) + if (this.set.Count == 0) return this; - else if (other.dict.Count == 0) + else if (other.set.Count == 0) return other; - Dictionary a, b; - if (dict.Count < other.dict.Count) { - a = dict; b = other.dict; + HashSet a, b; + if (this.set.Count < other.set.Count) { + a = this.set; b = other.set; } else { - a = other.dict; b = dict; + a = other.set; b = this.set; } - var r = new Dictionary(); - foreach (T t in a.Keys) { - if (b.ContainsKey(t)) - r.Add(t, true); + var r = new HashSet(); + foreach (T t in a) { + if (b.Contains(t)) + r.Add(t); } return new Set(r); } public Set Difference(Set other) { - if (dict.Count == 0) + if (this.set.Count == 0) return this; - else if (other.dict.Count == 0) + else if (other.set.Count == 0) return this; - var r = new Dictionary(); - foreach (T t in dict.Keys) { - if (!other.dict.ContainsKey(t)) - r.Add(t, true); + var r = new HashSet(); + foreach (T t in this.set) { + if (!other.set.Contains(t)) + r.Add(t); } return new Set(r); } @@ -447,6 +838,7 @@ namespace Dafny } } } +#endif public class Sequence { T[] elmts; -- cgit v1.2.3 From 566fdf1676e0d7d6060767febbfa7a0378300e99 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Thu, 20 Aug 2015 17:23:24 -0700 Subject: Fixed compilation that involve enumeration over native-type newtype values. --- Binaries/DafnyRuntime.cs | 5 +++ Source/Dafny/Compiler.cs | 76 +++++++++++++++++++++------------ Source/Dafny/DafnyAst.cs | 6 ++- Test/dafny0/RangeCompilation.dfy | 25 +++++++++++ Test/dafny0/RangeCompilation.dfy.expect | 6 +++ 5 files changed, 89 insertions(+), 29 deletions(-) create mode 100644 Test/dafny0/RangeCompilation.dfy create mode 100644 Test/dafny0/RangeCompilation.dfy.expect (limited to 'Binaries/DafnyRuntime.cs') diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs index 7d3799d8..dfb8cf38 100644 --- a/Binaries/DafnyRuntime.cs +++ b/Binaries/DafnyRuntime.cs @@ -1060,6 +1060,11 @@ namespace Dafny } } } + public static IEnumerable IntegerRange(BigInteger lo, BigInteger hi) { + for (var j = lo; j < hi; j++) { + yield return j; + } + } // pre: b != 0 // post: result == a/b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation) public static sbyte EuclideanDivision_sbyte(sbyte a, sbyte b) { diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index f2cc5d23..8bfa5fa9 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -117,7 +117,19 @@ namespace Microsoft.Dafny { } else if (d is TypeSynonymDecl) { // do nothing, just bypass type synonyms in the compiler } else if (d is NewtypeDecl) { - // do nothing, just bypass newtypes in the compiler + var nt = (NewtypeDecl)d; + Indent(indent); + wr.WriteLine("public class @{0} {{", nt.CompileName); + if (nt.NativeType != null) { + Indent(indent + IndentAmount); + wr.WriteLine("public static System.Collections.Generic.IEnumerable<{0}> IntegerRange(BigInteger lo, BigInteger hi) {{", nt.NativeType.Name); + Indent(indent + 2 * IndentAmount); + wr.WriteLine("for (var j = lo; j < hi; j++) {{ yield return ({0})j; }}", nt.NativeType.Name); + Indent(indent + IndentAmount); + wr.WriteLine("}"); + } + Indent(indent); + wr.WriteLine("}"); } else if (d is DatatypeDecl) { var dt = (DatatypeDecl)d; Indent(indent); @@ -676,7 +688,7 @@ namespace Microsoft.Dafny { } string DtName(DatatypeDecl decl) { - return decl.Module.IsDefaultModule ? decl.CompileName : decl.FullCompileName; + return decl.FullCompileName; } string DtCtorName(DatatypeCtor ctor) { Contract.Requires(ctor != null); @@ -1560,11 +1572,15 @@ namespace Microsoft.Dafny { } else if (bound is ComprehensionExpr.IntBoundedPool) { var b = (ComprehensionExpr.IntBoundedPool)bound; Indent(ind); - wr.Write("for (var @{0} = ", bv.CompileName); + if (AsNativeType(bv.Type) != null) { + wr.Write("foreach (var @{0} in @{1}.IntegerRange(", bv.CompileName, bv.Type.AsNewtype.FullCompileName); + } else { + wr.Write("foreach (var @{0} in Dafny.Helpers.IntegerRange(", bv.CompileName); + } TrExpr(b.LowerBound); - wr.Write("; @{0} < ", bv.CompileName); + wr.Write(", "); TrExpr(b.UpperBound); - wr.Write("; @{0}++) {{ ", bv.CompileName); + wr.Write(")) { "); } else if (bound is ComprehensionExpr.SetBoundedPool) { var b = (ComprehensionExpr.SetBoundedPool)bound; Indent(ind); @@ -1766,27 +1782,23 @@ namespace Microsoft.Dafny { wr.WriteLine("foreach (var {0} in Dafny.Helpers.AllBooleans) {{ @{1} = {0};", tmpVar, bv.CompileName); } else if (bound is ComprehensionExpr.IntBoundedPool) { var b = (ComprehensionExpr.IntBoundedPool)bound; - // (tmpVar is not used in this case) - if (b.LowerBound != null) { - wr.Write("@{0} = ", bv.CompileName); + if (AsNativeType(bv.Type) != null) { + wr.Write("foreach (var @{0} in @{1}.IntegerRange(", tmpVar, bv.Type.AsNewtype.FullCompileName); + } else { + wr.Write("foreach (var @{0} in Dafny.Helpers.IntegerRange(", tmpVar); + } + if (b.LowerBound == null) { + wr.Write("null"); + } else { TrExpr(b.LowerBound); - wr.WriteLine(";"); - Indent(ind); - if (b.UpperBound != null) { - wr.Write("for (; @{0} < ", bv.CompileName); - TrExpr(b.UpperBound); - wr.WriteLine("; @{0}++) {{ ", bv.CompileName); - } else { - wr.WriteLine("for (;; @{0}++) {{ ", bv.CompileName); - } + } + wr.Write(", "); + if (b.UpperBound == null) { + wr.Write("null"); } else { - Contract.Assert(b.UpperBound != null); - wr.Write("@{0} = ", bv.CompileName); TrExpr(b.UpperBound); - wr.WriteLine(";"); - Indent(ind); - wr.WriteLine("for (;; @{0}--) {{ ", bv.CompileName); } + wr.WriteLine(")) {{ @{1} = {0};", tmpVar, bv.CompileName); } else if (bound is AssignSuchThatStmt.WiggleWaggleBound) { wr.WriteLine("foreach (var {0} in Dafny.Helpers.AllIntegers) {{ @{1} = {0};", tmpVar, bv.CompileName); } else if (bound is ComprehensionExpr.SetBoundedPool) { @@ -2891,11 +2903,15 @@ namespace Microsoft.Dafny { wr.Write("foreach (var @{0} in Dafny.Helpers.AllBooleans) {{ ", bv.CompileName); } else if (bound is ComprehensionExpr.IntBoundedPool) { var b = (ComprehensionExpr.IntBoundedPool)bound; - wr.Write("for (var @{0} = ", bv.CompileName); + if (AsNativeType(bv.Type) != null) { + wr.Write("foreach (var @{0} in @{1}.IntegerRange(", bv.CompileName, bv.Type.AsNewtype.FullCompileName); + } else { + wr.Write("foreach (var @{0} in Dafny.Helpers.IntegerRange(", bv.CompileName); + } TrExpr(b.LowerBound); - wr.Write("; @{0} < ", bv.CompileName); + wr.Write(", "); TrExpr(b.UpperBound); - wr.Write("; @{0}++) {{ ", bv.CompileName); + wr.Write(")) { "); } else if (bound is ComprehensionExpr.SetBoundedPool) { var b = (ComprehensionExpr.SetBoundedPool)bound; wr.Write("foreach (var @{0} in (", bv.CompileName); @@ -2960,11 +2976,15 @@ namespace Microsoft.Dafny { wr.Write("foreach (var @{0} in Dafny.Helpers.AllBooleans) {{ ", bv.CompileName); } else if (bound is ComprehensionExpr.IntBoundedPool) { var b = (ComprehensionExpr.IntBoundedPool)bound; - wr.Write("for (var @{0} = ", bv.CompileName); + if (AsNativeType(bv.Type) != null) { + wr.Write("foreach (var @{0} in @{1}.IntegerRange(", bv.CompileName, bv.Type.AsNewtype.FullCompileName); + } else { + wr.Write("foreach (var @{0} in Dafny.Helpers.IntegerRange(", bv.CompileName); + } TrExpr(b.LowerBound); - wr.Write("; @{0} < ", bv.CompileName); + wr.Write(", "); TrExpr(b.UpperBound); - wr.Write("; @{0}++) {{ ", bv.CompileName); + wr.Write(")) { "); } else if (bound is ComprehensionExpr.SetBoundedPool) { var b = (ComprehensionExpr.SetBoundedPool)bound; wr.Write("foreach (var @{0} in (", bv.CompileName); diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 7328d8dd..d78ae170 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -1967,7 +1967,11 @@ namespace Microsoft.Dafny { } public string FullCompileName { get { - return Module.CompileName + ".@" + CompileName; + if (!Module.IsDefaultModule) { + return Module.CompileName + ".@" + CompileName; + } else { + return CompileName; + } } } } diff --git a/Test/dafny0/RangeCompilation.dfy b/Test/dafny0/RangeCompilation.dfy new file mode 100644 index 00000000..de8ca68e --- /dev/null +++ b/Test/dafny0/RangeCompilation.dfy @@ -0,0 +1,25 @@ +// RUN: %dafny /compile:3 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +newtype Byte = x | 0 <= x < 256 +predicate method GoodByte(b: Byte) { + b % 3 == 2 +} +predicate method GoodInteger(i: int) { + i % 5 == 4 +} + +method Main() { + assert GoodByte(11) && GoodInteger(24); + var b: Byte :| GoodByte(b); + var i: int :| 0 <= i < 256 && GoodInteger(i); + print "b=", b, " i=", i, "\n"; + var m0 := new MyClass; + var m17 := new M17.AnotherClass; +} + +class MyClass { } + +module M17 { + class AnotherClass { } +} diff --git a/Test/dafny0/RangeCompilation.dfy.expect b/Test/dafny0/RangeCompilation.dfy.expect new file mode 100644 index 00000000..c3275d12 --- /dev/null +++ b/Test/dafny0/RangeCompilation.dfy.expect @@ -0,0 +1,6 @@ + +Dafny program verifier finished with 5 verified, 0 errors +Program compiled successfully +Running... + +b=2 i=4 -- cgit v1.2.3 From 2a442cedb2d920cb45382af4add7f05270e31207 Mon Sep 17 00:00:00 2001 From: Michael Lowell Roberts Date: Mon, 31 Aug 2015 10:54:41 -0700 Subject: fix for comparison error in prelude when using /optimize. --- Binaries/DafnyRuntime.cs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Binaries/DafnyRuntime.cs') diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs index dfb8cf38..d1a3c092 100644 --- a/Binaries/DafnyRuntime.cs +++ b/Binaries/DafnyRuntime.cs @@ -72,11 +72,11 @@ namespace Dafny } } public bool Equals(Set other) { - return this.setImpl.Equals(other.setImpl); + return this.setImpl.SetEquals(other.setImpl); } public override bool Equals(object other) { var otherSet = other as Set; - return otherSet != null && Equals(otherSet); + return otherSet != null && this.Equals(otherSet); } public override int GetHashCode() { var hashCode = 1; -- cgit v1.2.3 From 96590cb8329d0c902b06d22b6cbecfdbe68cf654 Mon Sep 17 00:00:00 2001 From: Michael Lowell Roberts Date: Thu, 17 Sep 2015 15:00:57 -0700 Subject: Fix for soundness bug discovered in SeqFromArray. --- Binaries/DafnyRuntime.cs | 2622 +++++++++++++++++++++++----------------------- 1 file changed, 1311 insertions(+), 1311 deletions(-) (limited to 'Binaries/DafnyRuntime.cs') diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs index d1a3c092..e040402d 100644 --- a/Binaries/DafnyRuntime.cs +++ b/Binaries/DafnyRuntime.cs @@ -1,1311 +1,1311 @@ -using System; // for Func -using System.Numerics; - -namespace Dafny -{ - using System.Collections.Generic; -// set this option if you want to use System.Collections.Immutable and if you know what you're doing. -#if DAFNY_USE_SYSTEM_COLLECTIONS_IMMUTABLE - using System.Collections.Immutable; - using System.Linq; - - public class Set - { - readonly ImmutableHashSet setImpl; - Set(ImmutableHashSet d) { - this.setImpl = d; - } - public static readonly Set Empty = new Set(ImmutableHashSet.Empty); - public static Set FromElements(params T[] values) { - return FromElements((IEnumerable)values); - } - public static Set FromElements(IEnumerable values) { - var d = ImmutableHashSet.Empty.ToBuilder(); - foreach (T t in values) - d.Add(t); - return new Set(d.ToImmutable()); - } - public static Set FromCollection(ICollection values) { - var d = ImmutableHashSet.Empty.ToBuilder(); - foreach (T t in values) - d.Add(t); - return new Set(d.ToImmutable()); - } - public int Length { - get { return this.setImpl.Count; } - } - public long LongLength { - get { return this.setImpl.Count; } - } - public IEnumerable Elements { - get { - return this.setImpl; - } - } - /// - /// This is an inefficient iterator for producing all subsets of "this". Each set returned is the same - /// Set object (but this Set object is fresh; in particular, it is not "this"). - /// - public IEnumerable> AllSubsets { - get { - // Start by putting all set elements into a list - var elmts = new List(); - elmts.AddRange(this.setImpl); - var n = elmts.Count; - var which = new bool[n]; - var s = ImmutableHashSet.Empty.ToBuilder(); - while (true) { - yield return new Set(s.ToImmutable()); - // "add 1" to "which", as if doing a carry chain. For every digit changed, change the membership of the corresponding element in "s". - int i = 0; - for (; i < n && which[i]; i++) { - which[i] = false; - s.Remove(elmts[i]); - } - if (i == n) { - // we have cycled through all the subsets - break; - } - which[i] = true; - s.Add(elmts[i]); - } - } - } - public bool Equals(Set other) { - return this.setImpl.SetEquals(other.setImpl); - } - public override bool Equals(object other) { - var otherSet = other as Set; - return otherSet != null && this.Equals(otherSet); - } - public override int GetHashCode() { - var hashCode = 1; - foreach (var t in this.setImpl) { - hashCode = hashCode * (t.GetHashCode()+3); - } - return hashCode; - } - public override string ToString() { - var s = "{"; - var sep = ""; - foreach (var t in this.setImpl) { - s += sep + t.ToString(); - sep = ", "; - } - return s + "}"; - } - public bool IsProperSubsetOf(Set other) { - return IsProperSubsetOf(other); - } - public bool IsSubsetOf(Set other) { - return IsSubsetOf(other); - } - public bool IsSupersetOf(Set other) { - return other.IsSupersetOf(this); - } - public bool IsProperSupersetOf(Set other) { - return other.IsProperSupersetOf(this); - } - public bool IsDisjointFrom(Set other) { - ImmutableHashSet a, b; - if (this.setImpl.Count < other.setImpl.Count) { - a = this.setImpl; b = other.setImpl; - } else { - a = other.setImpl; b = this.setImpl; - } - foreach (T t in a) { - if (b.Contains(t)) - return false; - } - return true; - } - public bool Contains(T t) { - return this.setImpl.Contains(t); - } - public Set Union(Set other) { - return new Set(this.setImpl.Union(other.setImpl)); - } - public Set Intersect(Set other) { - return new Set(this.setImpl.Intersect(other.setImpl)); - } - public Set Difference(Set other) { - return new Set(this.setImpl.Except(other.setImpl)); - } - } - public partial class MultiSet - { - - readonly ImmutableDictionary dict; - MultiSet(ImmutableDictionary d) { - dict = d; - } - public static readonly MultiSet Empty = new MultiSet(ImmutableDictionary.Empty); - public static MultiSet FromElements(params T[] values) { - var d = ImmutableDictionary.Empty.ToBuilder(); - foreach (T t in values) { - var i = 0; - if (!d.TryGetValue(t, out i)) { - i = 0; - } - d[t] = i + 1; - } - return new MultiSet(d.ToImmutable()); - } - public static MultiSet FromCollection(ICollection values) { - var d = ImmutableDictionary.Empty.ToBuilder(); - foreach (T t in values) { - var i = 0; - if (!d.TryGetValue(t, out i)) { - i = 0; - } - d[t] = i + 1; - } - return new MultiSet(d.ToImmutable()); - } - public static MultiSet FromSeq(Sequence values) { - var d = ImmutableDictionary.Empty.ToBuilder(); - foreach (T t in values.Elements) { - var i = 0; - if (!d.TryGetValue(t, out i)) { - i = 0; - } - d[t] = i + 1; - } - return new MultiSet(d.ToImmutable()); - } - public static MultiSet FromSet(Set values) { - var d = ImmutableDictionary.Empty.ToBuilder(); - foreach (T t in values.Elements) { - d[t] = 1; - } - return new MultiSet(d.ToImmutable()); - } - - public bool Equals(MultiSet other) { - return other.IsSubsetOf(this) && this.IsSubsetOf(other); - } - public override bool Equals(object other) { - return other is MultiSet && Equals((MultiSet)other); - } - public override int GetHashCode() { - var hashCode = 1; - foreach (var kv in dict) { - var key = kv.Key.GetHashCode(); - key = (key << 3) | (key >> 29) ^ kv.Value.GetHashCode(); - hashCode = hashCode * (key + 3); - } - return hashCode; - } - public override string ToString() { - var s = "multiset{"; - var sep = ""; - foreach (var kv in dict) { - var t = kv.Key.ToString(); - for (int i = 0; i < kv.Value; i++) { - s += sep + t.ToString(); - sep = ", "; - } - } - return s + "}"; - } - public bool IsProperSubsetOf(MultiSet other) { - return !Equals(other) && IsSubsetOf(other); - } - public bool IsSubsetOf(MultiSet other) { - foreach (T t in dict.Keys) { - if (!other.dict.ContainsKey(t) || other.dict[t] < dict[t]) - return false; - } - return true; - } - public bool IsSupersetOf(MultiSet other) { - return other.IsSubsetOf(this); - } - public bool IsProperSupersetOf(MultiSet other) { - return other.IsProperSubsetOf(this); - } - public bool IsDisjointFrom(MultiSet other) { - foreach (T t in dict.Keys) { - if (other.dict.ContainsKey(t)) - return false; - } - foreach (T t in other.dict.Keys) { - if (dict.ContainsKey(t)) - return false; - } - return true; - } - public bool Contains(T t) { - return dict.ContainsKey(t); - } - public MultiSet Union(MultiSet other) { - if (dict.Count == 0) - return other; - else if (other.dict.Count == 0) - return this; - var r = ImmutableDictionary.Empty.ToBuilder(); - foreach (T t in dict.Keys) { - var i = 0; - if (!r.TryGetValue(t, out i)) { - i = 0; - } - r[t] = i + dict[t]; - } - foreach (T t in other.dict.Keys) { - var i = 0; - if (!r.TryGetValue(t, out i)) { - i = 0; - } - r[t] = i + other.dict[t]; - } - return new MultiSet(r.ToImmutable()); - } - public MultiSet Intersect(MultiSet other) { - if (dict.Count == 0) - return this; - else if (other.dict.Count == 0) - return other; - var r = ImmutableDictionary.Empty.ToBuilder(); - foreach (T t in dict.Keys) { - if (other.dict.ContainsKey(t)) { - r[t] = other.dict[t] < dict[t] ? other.dict[t] : dict[t]; - } - } - return new MultiSet(r.ToImmutable()); - } - public MultiSet Difference(MultiSet other) { // \result == this - other - if (dict.Count == 0) - return this; - else if (other.dict.Count == 0) - return this; - var r = ImmutableDictionary.Empty.ToBuilder(); - foreach (T t in dict.Keys) { - if (!other.dict.ContainsKey(t)) { - r[t] = dict[t]; - } else if (other.dict[t] < dict[t]) { - r[t] = dict[t] - other.dict[t]; - } - } - return new MultiSet(r.ToImmutable()); - } - public IEnumerable Elements { - get { - foreach (T t in dict.Keys) { - int n; - dict.TryGetValue(t, out n); - for (int i = 0; i < n; i ++) { - yield return t; - } - } - } - } - } - - public partial class Map - { - readonly ImmutableDictionary dict; - Map(ImmutableDictionary d) { - dict = d; - } - public static readonly Map Empty = new Map(ImmutableDictionary.Empty); - public static Map FromElements(params Pair[] values) { - var d = ImmutableDictionary.Empty.ToBuilder(); - foreach (Pair p in values) { - d[p.Car] = p.Cdr; - } - return new Map(d.ToImmutable()); - } - public static Map FromCollection(List> values) { - var d = ImmutableDictionary.Empty.ToBuilder(); - foreach (Pair p in values) { - d[p.Car] = p.Cdr; - } - return new Map(d.ToImmutable()); - } - public int Length { - get { return dict.Count; } - } - public long LongLength { - get { return dict.Count; } - } - public bool Equals(Map other) { - foreach (U u in dict.Keys) { - V v1, v2; - if (!dict.TryGetValue(u, out v1)) { - return false; // this shouldn't happen - } - if (!other.dict.TryGetValue(u, out v2)) { - return false; // other dictionary does not contain this element - } - if (!v1.Equals(v2)) { - return false; - } - } - foreach (U u in other.dict.Keys) { - if (!dict.ContainsKey(u)) { - return false; // this shouldn't happen - } - } - return true; - } - public override bool Equals(object other) { - return other is Map && Equals((Map)other); - } - public override int GetHashCode() { - var hashCode = 1; - foreach (var kv in dict) { - var key = kv.Key.GetHashCode(); - key = (key << 3) | (key >> 29) ^ kv.Value.GetHashCode(); - hashCode = hashCode * (key + 3); - } - return hashCode; - } - public override string ToString() { - var s = "map["; - var sep = ""; - foreach (var kv in dict) { - s += sep + kv.Key.ToString() + " := " + kv.Value.ToString(); - sep = ", "; - } - return s + "]"; - } - public bool IsDisjointFrom(Map other) { - foreach (U u in dict.Keys) { - if (other.dict.ContainsKey(u)) - return false; - } - foreach (U u in other.dict.Keys) { - if (dict.ContainsKey(u)) - return false; - } - return true; - } - public bool Contains(U u) { - return dict.ContainsKey(u); - } - public V Select(U index) { - return dict[index]; - } - public Map Update(U index, V val) { - return new Map(dict.SetItem(index, val)); - } - public IEnumerable Domain { - get { - return dict.Keys; - } - } - } -#else // !def DAFNY_USE_SYSTEM_COLLECTIONS_IMMUTABLE - public class Set - { - HashSet set; - Set(HashSet s) { - this.set = s; - } - public static Set Empty { - get { - return new Set(new HashSet()); - } - } - public static Set FromElements(params T[] values) { - var s = new HashSet(); - foreach (T t in values) - s.Add(t); - return new Set(s); - } - public static Set FromCollection(ICollection values) { - HashSet s = new HashSet(); - foreach (T t in values) - s.Add(t); - return new Set(s); - } - public int Length { - get { return this.set.Count; } - } - public long LongLength { - get { return this.set.Count; } - } - public IEnumerable Elements { - get { - return this.set; - } - } - /// - /// This is an inefficient iterator for producing all subsets of "this". Each set returned is the same - /// Set object (but this Set object is fresh; in particular, it is not "this"). - /// - public IEnumerable> AllSubsets { - get { - // Start by putting all set elements into a list - var elmts = new List(); - elmts.AddRange(this.set); - var n = elmts.Count; - var which = new bool[n]; - var s = new Set(new HashSet()); - while (true) { - yield return s; - // "add 1" to "which", as if doing a carry chain. For every digit changed, change the membership of the corresponding element in "s". - int i = 0; - for (; i < n && which[i]; i++) { - which[i] = false; - s.set.Remove(elmts[i]); - } - if (i == n) { - // we have cycled through all the subsets - break; - } - which[i] = true; - s.set.Add(elmts[i]); - } - } - } - public bool Equals(Set other) { - return this.set.Count == other.set.Count && IsSubsetOf(other); - } - public override bool Equals(object other) { - return other is Set && Equals((Set)other); - } - public override int GetHashCode() { - var hashCode = 1; - foreach (var t in this.set) { - hashCode = hashCode * (t.GetHashCode()+3); - } - return hashCode; - } - public override string ToString() { - var s = "{"; - var sep = ""; - foreach (var t in this.set) { - s += sep + t.ToString(); - sep = ", "; - } - return s + "}"; - } - public bool IsProperSubsetOf(Set other) { - return this.set.Count < other.set.Count && IsSubsetOf(other); - } - public bool IsSubsetOf(Set other) { - if (other.set.Count < this.set.Count) - return false; - foreach (T t in this.set) { - if (!other.set.Contains(t)) - return false; - } - return true; - } - public bool IsSupersetOf(Set other) { - return other.IsSubsetOf(this); - } - public bool IsProperSupersetOf(Set other) { - return other.IsProperSubsetOf(this); - } - public bool IsDisjointFrom(Set other) { - HashSet a, b; - if (this.set.Count < other.set.Count) { - a = this.set; b = other.set; - } else { - a = other.set; b = this.set; - } - foreach (T t in a) { - if (b.Contains(t)) - return false; - } - return true; - } - public bool Contains(T t) { - return this.set.Contains(t); - } - public Set Union(Set other) { - if (this.set.Count == 0) - return other; - else if (other.set.Count == 0) - return this; - HashSet a, b; - if (this.set.Count < other.set.Count) { - a = this.set; b = other.set; - } else { - a = other.set; b = this.set; - } - var r = new HashSet(); - foreach (T t in b) - r.Add(t); - foreach (T t in a) - r.Add(t); - return new Set(r); - } - public Set Intersect(Set other) { - if (this.set.Count == 0) - return this; - else if (other.set.Count == 0) - return other; - HashSet a, b; - if (this.set.Count < other.set.Count) { - a = this.set; b = other.set; - } else { - a = other.set; b = this.set; - } - var r = new HashSet(); - foreach (T t in a) { - if (b.Contains(t)) - r.Add(t); - } - return new Set(r); - } - public Set Difference(Set other) { - if (this.set.Count == 0) - return this; - else if (other.set.Count == 0) - return this; - var r = new HashSet(); - foreach (T t in this.set) { - if (!other.set.Contains(t)) - r.Add(t); - } - return new Set(r); - } - } - public class MultiSet - { - Dictionary dict; - MultiSet(Dictionary d) { - dict = d; - } - public static MultiSet Empty { - get { - return new MultiSet(new Dictionary(0)); - } - } - public static MultiSet FromElements(params T[] values) { - Dictionary d = new Dictionary(values.Length); - foreach (T t in values) { - var i = 0; - if (!d.TryGetValue(t, out i)) { - i = 0; - } - d[t] = i + 1; - } - return new MultiSet(d); - } - public static MultiSet FromCollection(ICollection values) { - Dictionary d = new Dictionary(); - foreach (T t in values) { - var i = 0; - if (!d.TryGetValue(t, out i)) { - i = 0; - } - d[t] = i + 1; - } - return new MultiSet(d); - } - public static MultiSet FromSeq(Sequence values) { - Dictionary d = new Dictionary(); - foreach (T t in values.Elements) { - var i = 0; - if (!d.TryGetValue(t, out i)) { - i = 0; - } - d[t] = i + 1; - } - return new MultiSet(d); - } - public static MultiSet FromSet(Set values) { - Dictionary d = new Dictionary(); - foreach (T t in values.Elements) { - d[t] = 1; - } - return new MultiSet(d); - } - - public bool Equals(MultiSet other) { - return other.IsSubsetOf(this) && this.IsSubsetOf(other); - } - public override bool Equals(object other) { - return other is MultiSet && Equals((MultiSet)other); - } - public override int GetHashCode() { - var hashCode = 1; - foreach (var kv in dict) { - var key = kv.Key.GetHashCode(); - key = (key << 3) | (key >> 29) ^ kv.Value.GetHashCode(); - hashCode = hashCode * (key + 3); - } - return hashCode; - } - public override string ToString() { - var s = "multiset{"; - var sep = ""; - foreach (var kv in dict) { - var t = kv.Key.ToString(); - for (int i = 0; i < kv.Value; i++) { - s += sep + t.ToString(); - sep = ", "; - } - } - return s + "}"; - } - public bool IsProperSubsetOf(MultiSet other) { - return !Equals(other) && IsSubsetOf(other); - } - public bool IsSubsetOf(MultiSet other) { - foreach (T t in dict.Keys) { - if (!other.dict.ContainsKey(t) || other.dict[t] < dict[t]) - return false; - } - return true; - } - public bool IsSupersetOf(MultiSet other) { - return other.IsSubsetOf(this); - } - public bool IsProperSupersetOf(MultiSet other) { - return other.IsProperSubsetOf(this); - } - public bool IsDisjointFrom(MultiSet other) { - foreach (T t in dict.Keys) { - if (other.dict.ContainsKey(t)) - return false; - } - foreach (T t in other.dict.Keys) { - if (dict.ContainsKey(t)) - return false; - } - return true; - } - public bool Contains(T t) { - return dict.ContainsKey(t); - } - public MultiSet Union(MultiSet other) { - if (dict.Count == 0) - return other; - else if (other.dict.Count == 0) - return this; - var r = new Dictionary(); - foreach (T t in dict.Keys) { - var i = 0; - if (!r.TryGetValue(t, out i)) { - i = 0; - } - r[t] = i + dict[t]; - } - foreach (T t in other.dict.Keys) { - var i = 0; - if (!r.TryGetValue(t, out i)) { - i = 0; - } - r[t] = i + other.dict[t]; - } - return new MultiSet(r); - } - public MultiSet Intersect(MultiSet other) { - if (dict.Count == 0) - return this; - else if (other.dict.Count == 0) - return other; - var r = new Dictionary(); - foreach (T t in dict.Keys) { - if (other.dict.ContainsKey(t)) { - r.Add(t, other.dict[t] < dict[t] ? other.dict[t] : dict[t]); - } - } - return new MultiSet(r); - } - public MultiSet Difference(MultiSet other) { // \result == this - other - if (dict.Count == 0) - return this; - else if (other.dict.Count == 0) - return this; - var r = new Dictionary(); - foreach (T t in dict.Keys) { - if (!other.dict.ContainsKey(t)) { - r.Add(t, dict[t]); - } else if (other.dict[t] < dict[t]) { - r.Add(t, dict[t] - other.dict[t]); - } - } - return new MultiSet(r); - } - public IEnumerable Elements { - get { - List l = new List(); - foreach (T t in dict.Keys) { - int n; - dict.TryGetValue(t, out n); - for (int i = 0; i < n; i ++) { - l.Add(t); - } - } - return l; - } - } - } - - public class Map - { - Dictionary dict; - Map(Dictionary d) { - dict = d; - } - public static Map Empty { - get { - return new Map(new Dictionary()); - } - } - public static Map FromElements(params Pair[] values) { - Dictionary d = new Dictionary(values.Length); - foreach (Pair p in values) { - d[p.Car] = p.Cdr; - } - return new Map(d); - } - public static Map FromCollection(List> values) { - Dictionary d = new Dictionary(values.Count); - foreach (Pair p in values) { - d[p.Car] = p.Cdr; - } - return new Map(d); - } - public int Length { - get { return dict.Count; } - } - public long LongLength { - get { return dict.Count; } - } - public bool Equals(Map other) { - foreach (U u in dict.Keys) { - V v1, v2; - if (!dict.TryGetValue(u, out v1)) { - return false; // this shouldn't happen - } - if (!other.dict.TryGetValue(u, out v2)) { - return false; // other dictionary does not contain this element - } - if (!v1.Equals(v2)) { - return false; - } - } - foreach (U u in other.dict.Keys) { - if (!dict.ContainsKey(u)) { - return false; // this shouldn't happen - } - } - return true; - } - public override bool Equals(object other) { - return other is Map && Equals((Map)other); - } - public override int GetHashCode() { - var hashCode = 1; - foreach (var kv in dict) { - var key = kv.Key.GetHashCode(); - key = (key << 3) | (key >> 29) ^ kv.Value.GetHashCode(); - hashCode = hashCode * (key + 3); - } - return hashCode; - } - public override string ToString() { - var s = "map["; - var sep = ""; - foreach (var kv in dict) { - s += sep + kv.Key.ToString() + " := " + kv.Value.ToString(); - sep = ", "; - } - return s + "]"; - } - public bool IsDisjointFrom(Map other) { - foreach (U u in dict.Keys) { - if (other.dict.ContainsKey(u)) - return false; - } - foreach (U u in other.dict.Keys) { - if (dict.ContainsKey(u)) - return false; - } - return true; - } - public bool Contains(U u) { - return dict.ContainsKey(u); - } - public V Select(U index) { - return dict[index]; - } - public Map Update(U index, V val) { - Dictionary d = new Dictionary(dict); - d[index] = val; - return new Map(d); - } - public IEnumerable Domain { - get { - return dict.Keys; - } - } - } -#endif - public class Sequence - { - T[] elmts; - public Sequence(T[] ee) { - elmts = ee; - } - public static Sequence Empty { - get { - return new Sequence(new T[0]); - } - } - public static Sequence FromElements(params T[] values) { - return new Sequence(values); - } - public static Sequence FromString(string s) { - return new Sequence(s.ToCharArray()); - } - public int Length { - get { return elmts.Length; } - } - public long LongLength { - get { return elmts.LongLength; } - } - public T[] Elements { - get { - return elmts; - } - } - public IEnumerable UniqueElements { - get { - var st = Set.FromElements(elmts); - return st.Elements; - } - } - public T Select(ulong index) { - return elmts[index]; - } - public T Select(long index) { - return elmts[index]; - } - public T Select(uint index) { - return elmts[index]; - } - public T Select(int index) { - return elmts[index]; - } - public T Select(BigInteger index) { - return elmts[(int)index]; - } - public Sequence Update(long index, T t) { - T[] a = (T[])elmts.Clone(); - a[index] = t; - return new Sequence(a); - } - public Sequence Update(ulong index, T t) { - return Update((long)index, t); - } - public Sequence Update(BigInteger index, T t) { - return Update((long)index, t); - } - public bool Equals(Sequence other) { - int n = elmts.Length; - return n == other.elmts.Length && EqualUntil(other, n); - } - public override bool Equals(object other) { - return other is Sequence && Equals((Sequence)other); - } - public override int GetHashCode() { - if (elmts == null || elmts.Length == 0) - return 0; - var hashCode = 0; - for (var i = 0; i < elmts.Length; i++) { - hashCode = (hashCode << 3) | (hashCode >> 29) ^ elmts[i].GetHashCode(); - } - return hashCode; - } - public override string ToString() { - if (elmts is char[]) { - var s = ""; - foreach (var t in elmts) { - s += t.ToString(); - } - return s; - } else { - var s = "["; - var sep = ""; - foreach (var t in elmts) { - s += sep + t.ToString(); - sep = ", "; - } - return s + "]"; - } - } - bool EqualUntil(Sequence other, int n) { - for (int i = 0; i < n; i++) { - if (!elmts[i].Equals(other.elmts[i])) - return false; - } - return true; - } - public bool IsProperPrefixOf(Sequence other) { - int n = elmts.Length; - return n < other.elmts.Length && EqualUntil(other, n); - } - public bool IsPrefixOf(Sequence other) { - int n = elmts.Length; - return n <= other.elmts.Length && EqualUntil(other, n); - } - public Sequence Concat(Sequence other) { - if (elmts.Length == 0) - return other; - else if (other.elmts.Length == 0) - return this; - T[] a = new T[elmts.Length + other.elmts.Length]; - System.Array.Copy(elmts, 0, a, 0, elmts.Length); - System.Array.Copy(other.elmts, 0, a, elmts.Length, other.elmts.Length); - return new Sequence(a); - } - public bool Contains(T t) { - int n = elmts.Length; - for (int i = 0; i < n; i++) { - if (t.Equals(elmts[i])) - return true; - } - return false; - } - public Sequence Take(long m) { - if (elmts.LongLength == m) - return this; - T[] a = new T[m]; - System.Array.Copy(elmts, a, m); - return new Sequence(a); - } - public Sequence Take(ulong n) { - return Take((long)n); - } - public Sequence Take(BigInteger n) { - return Take((long)n); - } - public Sequence Drop(long m) { - if (m == 0) - return this; - T[] a = new T[elmts.Length - m]; - System.Array.Copy(elmts, m, a, 0, elmts.Length - m); - return new Sequence(a); - } - public Sequence Drop(ulong n) { - return Drop((long)n); - } - public Sequence Drop(BigInteger n) { - if (n.IsZero) - return this; - return Drop((long)n); - } - } - public struct Pair - { - public readonly A Car; - public readonly B Cdr; - public Pair(A a, B b) { - this.Car = a; - this.Cdr = b; - } - } - public partial class Helpers { - // Computing forall/exists quantifiers - public static bool QuantBool(bool frall, System.Predicate pred) { - if (frall) { - return pred(false) && pred(true); - } else { - return pred(false) || pred(true); - } - } - public static bool QuantInt(BigInteger lo, BigInteger hi, bool frall, System.Predicate pred) { - for (BigInteger i = lo; i < hi; i++) { - if (pred(i) != frall) { return !frall; } - } - return frall; - } - public static bool QuantSet(Dafny.Set set, bool frall, System.Predicate pred) { - foreach (var u in set.Elements) { - if (pred(u) != frall) { return !frall; } - } - return frall; - } - public static bool QuantMap(Dafny.Map map, bool frall, System.Predicate pred) { - foreach (var u in map.Domain) { - if (pred(u) != frall) { return !frall; } - } - return frall; - } - public static bool QuantSeq(Dafny.Sequence seq, bool frall, System.Predicate pred) { - foreach (var u in seq.Elements) { - if (pred(u) != frall) { return !frall; } - } - return frall; - } - public static bool QuantDatatype(IEnumerable set, bool frall, System.Predicate pred) { - foreach (var u in set) { - if (pred(u) != frall) { return !frall; } - } - return frall; - } - // Enumerating other collections - public delegate Dafny.Set ComprehensionDelegate(); - public delegate Dafny.Map MapComprehensionDelegate(); - public static IEnumerable AllBooleans { - get { - yield return false; - yield return true; - } - } - public static IEnumerable AllIntegers { - get { - yield return new BigInteger(0); - for (var j = new BigInteger(1);; j++) { - yield return j; - yield return -j; - } - } - } - public static IEnumerable IntegerRange(BigInteger lo, BigInteger hi) { - for (var j = lo; j < hi; j++) { - yield return j; - } - } - // pre: b != 0 - // post: result == a/b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation) - public static sbyte EuclideanDivision_sbyte(sbyte a, sbyte b) { - return (sbyte)EuclideanDivision_int(a, b); - } - public static short EuclideanDivision_short(short a, short b) { - return (short)EuclideanDivision_int(a, b); - } - public static int EuclideanDivision_int(int a, int b) { - if (0 <= a) { - if (0 <= b) { - // +a +b: a/b - return (int)(((uint)(a)) / ((uint)(b))); - } else { - // +a -b: -(a/(-b)) - return -((int)(((uint)(a)) / ((uint)(unchecked(-b))))); - } - } else { - if (0 <= b) { - // -a +b: -((-a-1)/b) - 1 - return -((int)(((uint)(-(a + 1))) / ((uint)(b)))) - 1; - } else { - // -a -b: ((-a-1)/(-b)) + 1 - return ((int)(((uint)(-(a + 1))) / ((uint)(unchecked(-b))))) + 1; - } - } - } - public static long EuclideanDivision_long(long a, long b) { - if (0 <= a) { - if (0 <= b) { - // +a +b: a/b - return (long)(((ulong)(a)) / ((ulong)(b))); - } else { - // +a -b: -(a/(-b)) - return -((long)(((ulong)(a)) / ((ulong)(unchecked(-b))))); - } - } else { - if (0 <= b) { - // -a +b: -((-a-1)/b) - 1 - return -((long)(((ulong)(-(a + 1))) / ((ulong)(b)))) - 1; - } else { - // -a -b: ((-a-1)/(-b)) + 1 - return ((long)(((ulong)(-(a + 1))) / ((ulong)(unchecked(-b))))) + 1; - } - } - } - public static BigInteger EuclideanDivision(BigInteger a, BigInteger b) { - if (0 <= a.Sign) { - if (0 <= b.Sign) { - // +a +b: a/b - return BigInteger.Divide(a, b); - } else { - // +a -b: -(a/(-b)) - return BigInteger.Negate(BigInteger.Divide(a, BigInteger.Negate(b))); - } - } else { - if (0 <= b.Sign) { - // -a +b: -((-a-1)/b) - 1 - return BigInteger.Negate(BigInteger.Divide(BigInteger.Negate(a) - 1, b)) - 1; - } else { - // -a -b: ((-a-1)/(-b)) + 1 - return BigInteger.Divide(BigInteger.Negate(a) - 1, BigInteger.Negate(b)) + 1; - } - } - } - // pre: b != 0 - // post: result == a%b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation) - public static sbyte EuclideanModulus_sbyte(sbyte a, sbyte b) { - return (sbyte)EuclideanModulus_int(a, b); - } - public static short EuclideanModulus_short(short a, short b) { - return (short)EuclideanModulus_int(a, b); - } - public static int EuclideanModulus_int(int a, int b) { - uint bp = (0 <= b) ? (uint)b : (uint)(unchecked(-b)); - if (0 <= a) { - // +a: a % b' - return (int)(((uint)a) % bp); - } else { - // c = ((-a) % b') - // -a: b' - c if c > 0 - // -a: 0 if c == 0 - uint c = ((uint)(unchecked(-a))) % bp; - return (int)(c == 0 ? c : bp - c); - } - } - public static long EuclideanModulus_long(long a, long b) { - ulong bp = (0 <= b) ? (ulong)b : (ulong)(unchecked(-b)); - if (0 <= a) { - // +a: a % b' - return (long)(((ulong)a) % bp); - } else { - // c = ((-a) % b') - // -a: b' - c if c > 0 - // -a: 0 if c == 0 - ulong c = ((ulong)(unchecked(-a))) % bp; - return (long)(c == 0 ? c : bp - c); - } - } - public static BigInteger EuclideanModulus(BigInteger a, BigInteger b) { - var bp = BigInteger.Abs(b); - if (0 <= a.Sign) { - // +a: a % b' - return BigInteger.Remainder(a, bp); - } else { - // c = ((-a) % b') - // -a: b' - c if c > 0 - // -a: 0 if c == 0 - var c = BigInteger.Remainder(BigInteger.Negate(a), bp); - return c.IsZero ? c : BigInteger.Subtract(bp, c); - } - } - public static Sequence SeqFromArray(T[] array) { - return new Sequence(array); - } - // In .NET version 4.5, it it possible to mark a method with "AggressiveInlining", which says to inline the - // method if possible. Method "ExpressionSequence" would be a good candidate for it: - // [System.Runtime.CompilerServices.MethodImpl(System.Runtime.CompilerServices.MethodImplOptions.AggressiveInlining)] - public static U ExpressionSequence(T t, U u) - { - return u; - } - - public static U Let(T t, Func f) { - return f(t); - } - - public delegate Result Function(Input input); - - public static A Id(A a) { - return a; - } - } - - public struct BigRational - { - public static readonly BigRational ZERO = new BigRational(0); - - BigInteger num, den; // invariant 1 <= den - public override string ToString() { - return string.Format("({0}.0 / {1}.0)", num, den); - } - public BigRational(int n) { - num = new BigInteger(n); - den = BigInteger.One; - } - public BigRational(BigInteger n, BigInteger d) { - // requires 1 <= d - num = n; - den = d; - } - public BigInteger ToBigInteger() { - if (0 <= num) { - return num / den; - } else { - return (num - den + 1) / den; - } - } - /// - /// Returns values such that aa/dd == a and bb/dd == b. - /// - private static void Normalize(BigRational a, BigRational b, out BigInteger aa, out BigInteger bb, out BigInteger dd) { - var gcd = BigInteger.GreatestCommonDivisor(a.den, b.den); - var xx = a.den / gcd; - var yy = b.den / gcd; - // We now have a == a.num / (xx * gcd) and b == b.num / (yy * gcd). - aa = a.num * yy; - bb = b.num * xx; - dd = a.den * yy; - } - public int CompareTo(BigRational that) { - // simple things first - int asign = this.num.Sign; - int bsign = that.num.Sign; - if (asign < 0 && 0 <= bsign) { - return 1; - } else if (asign <= 0 && 0 < bsign) { - return 1; - } else if (bsign < 0 && 0 <= asign) { - return -1; - } else if (bsign <= 0 && 0 < asign) { - return -1; - } - BigInteger aa, bb, dd; - Normalize(this, that, out aa, out bb, out dd); - return aa.CompareTo(bb); - } - public override int GetHashCode() { - return num.GetHashCode() + 29 * den.GetHashCode(); - } - public override bool Equals(object obj) { - if (obj is BigRational) { - return this == (BigRational)obj; - } else { - return false; - } - } - public static bool operator ==(BigRational a, BigRational b) { - return a.CompareTo(b) == 0; - } - public static bool operator !=(BigRational a, BigRational b) { - return a.CompareTo(b) != 0; - } - public static bool operator >(BigRational a, BigRational b) { - return 0 < a.CompareTo(b); - } - public static bool operator >=(BigRational a, BigRational b) { - return 0 <= a.CompareTo(b); - } - public static bool operator <(BigRational a, BigRational b) { - return a.CompareTo(b) < 0; - } - public static bool operator <=(BigRational a, BigRational b) { - return a.CompareTo(b) <= 0; - } - public static BigRational operator +(BigRational a, BigRational b) { - BigInteger aa, bb, dd; - Normalize(a, b, out aa, out bb, out dd); - return new BigRational(aa + bb, dd); - } - public static BigRational operator -(BigRational a, BigRational b) { - BigInteger aa, bb, dd; - Normalize(a, b, out aa, out bb, out dd); - return new BigRational(aa - bb, dd); - } - public static BigRational operator -(BigRational a) { - return new BigRational(-a.num, a.den); - } - public static BigRational operator *(BigRational a, BigRational b) { - return new BigRational(a.num * b.num, a.den * b.den); - } - public static BigRational operator /(BigRational a, BigRational b) { - // Compute the reciprocal of b - BigRational bReciprocal; - if (0 < b.num) { - bReciprocal = new BigRational(b.den, b.num); - } else { - // this is the case b.num < 0 - bReciprocal = new BigRational(-b.den, -b.num); - } - return a * bReciprocal; - } - } -} +using System; // for Func +using System.Numerics; + +namespace Dafny +{ + using System.Collections.Generic; +// set this option if you want to use System.Collections.Immutable and if you know what you're doing. +#if DAFNY_USE_SYSTEM_COLLECTIONS_IMMUTABLE + using System.Collections.Immutable; + using System.Linq; + + public class Set + { + readonly ImmutableHashSet setImpl; + Set(ImmutableHashSet d) { + this.setImpl = d; + } + public static readonly Set Empty = new Set(ImmutableHashSet.Empty); + public static Set FromElements(params T[] values) { + return FromElements((IEnumerable)values); + } + public static Set FromElements(IEnumerable values) { + var d = ImmutableHashSet.Empty.ToBuilder(); + foreach (T t in values) + d.Add(t); + return new Set(d.ToImmutable()); + } + public static Set FromCollection(ICollection values) { + var d = ImmutableHashSet.Empty.ToBuilder(); + foreach (T t in values) + d.Add(t); + return new Set(d.ToImmutable()); + } + public int Length { + get { return this.setImpl.Count; } + } + public long LongLength { + get { return this.setImpl.Count; } + } + public IEnumerable Elements { + get { + return this.setImpl; + } + } + /// + /// This is an inefficient iterator for producing all subsets of "this". Each set returned is the same + /// Set object (but this Set object is fresh; in particular, it is not "this"). + /// + public IEnumerable> AllSubsets { + get { + // Start by putting all set elements into a list + var elmts = new List(); + elmts.AddRange(this.setImpl); + var n = elmts.Count; + var which = new bool[n]; + var s = ImmutableHashSet.Empty.ToBuilder(); + while (true) { + yield return new Set(s.ToImmutable()); + // "add 1" to "which", as if doing a carry chain. For every digit changed, change the membership of the corresponding element in "s". + int i = 0; + for (; i < n && which[i]; i++) { + which[i] = false; + s.Remove(elmts[i]); + } + if (i == n) { + // we have cycled through all the subsets + break; + } + which[i] = true; + s.Add(elmts[i]); + } + } + } + public bool Equals(Set other) { + return this.setImpl.SetEquals(other.setImpl); + } + public override bool Equals(object other) { + var otherSet = other as Set; + return otherSet != null && this.Equals(otherSet); + } + public override int GetHashCode() { + var hashCode = 1; + foreach (var t in this.setImpl) { + hashCode = hashCode * (t.GetHashCode()+3); + } + return hashCode; + } + public override string ToString() { + var s = "{"; + var sep = ""; + foreach (var t in this.setImpl) { + s += sep + t.ToString(); + sep = ", "; + } + return s + "}"; + } + public bool IsProperSubsetOf(Set other) { + return IsProperSubsetOf(other); + } + public bool IsSubsetOf(Set other) { + return IsSubsetOf(other); + } + public bool IsSupersetOf(Set other) { + return other.IsSupersetOf(this); + } + public bool IsProperSupersetOf(Set other) { + return other.IsProperSupersetOf(this); + } + public bool IsDisjointFrom(Set other) { + ImmutableHashSet a, b; + if (this.setImpl.Count < other.setImpl.Count) { + a = this.setImpl; b = other.setImpl; + } else { + a = other.setImpl; b = this.setImpl; + } + foreach (T t in a) { + if (b.Contains(t)) + return false; + } + return true; + } + public bool Contains(T t) { + return this.setImpl.Contains(t); + } + public Set Union(Set other) { + return new Set(this.setImpl.Union(other.setImpl)); + } + public Set Intersect(Set other) { + return new Set(this.setImpl.Intersect(other.setImpl)); + } + public Set Difference(Set other) { + return new Set(this.setImpl.Except(other.setImpl)); + } + } + public partial class MultiSet + { + + readonly ImmutableDictionary dict; + MultiSet(ImmutableDictionary d) { + dict = d; + } + public static readonly MultiSet Empty = new MultiSet(ImmutableDictionary.Empty); + public static MultiSet FromElements(params T[] values) { + var d = ImmutableDictionary.Empty.ToBuilder(); + foreach (T t in values) { + var i = 0; + if (!d.TryGetValue(t, out i)) { + i = 0; + } + d[t] = i + 1; + } + return new MultiSet(d.ToImmutable()); + } + public static MultiSet FromCollection(ICollection values) { + var d = ImmutableDictionary.Empty.ToBuilder(); + foreach (T t in values) { + var i = 0; + if (!d.TryGetValue(t, out i)) { + i = 0; + } + d[t] = i + 1; + } + return new MultiSet(d.ToImmutable()); + } + public static MultiSet FromSeq(Sequence values) { + var d = ImmutableDictionary.Empty.ToBuilder(); + foreach (T t in values.Elements) { + var i = 0; + if (!d.TryGetValue(t, out i)) { + i = 0; + } + d[t] = i + 1; + } + return new MultiSet(d.ToImmutable()); + } + public static MultiSet FromSet(Set values) { + var d = ImmutableDictionary.Empty.ToBuilder(); + foreach (T t in values.Elements) { + d[t] = 1; + } + return new MultiSet(d.ToImmutable()); + } + + public bool Equals(MultiSet other) { + return other.IsSubsetOf(this) && this.IsSubsetOf(other); + } + public override bool Equals(object other) { + return other is MultiSet && Equals((MultiSet)other); + } + public override int GetHashCode() { + var hashCode = 1; + foreach (var kv in dict) { + var key = kv.Key.GetHashCode(); + key = (key << 3) | (key >> 29) ^ kv.Value.GetHashCode(); + hashCode = hashCode * (key + 3); + } + return hashCode; + } + public override string ToString() { + var s = "multiset{"; + var sep = ""; + foreach (var kv in dict) { + var t = kv.Key.ToString(); + for (int i = 0; i < kv.Value; i++) { + s += sep + t.ToString(); + sep = ", "; + } + } + return s + "}"; + } + public bool IsProperSubsetOf(MultiSet other) { + return !Equals(other) && IsSubsetOf(other); + } + public bool IsSubsetOf(MultiSet other) { + foreach (T t in dict.Keys) { + if (!other.dict.ContainsKey(t) || other.dict[t] < dict[t]) + return false; + } + return true; + } + public bool IsSupersetOf(MultiSet other) { + return other.IsSubsetOf(this); + } + public bool IsProperSupersetOf(MultiSet other) { + return other.IsProperSubsetOf(this); + } + public bool IsDisjointFrom(MultiSet other) { + foreach (T t in dict.Keys) { + if (other.dict.ContainsKey(t)) + return false; + } + foreach (T t in other.dict.Keys) { + if (dict.ContainsKey(t)) + return false; + } + return true; + } + public bool Contains(T t) { + return dict.ContainsKey(t); + } + public MultiSet Union(MultiSet other) { + if (dict.Count == 0) + return other; + else if (other.dict.Count == 0) + return this; + var r = ImmutableDictionary.Empty.ToBuilder(); + foreach (T t in dict.Keys) { + var i = 0; + if (!r.TryGetValue(t, out i)) { + i = 0; + } + r[t] = i + dict[t]; + } + foreach (T t in other.dict.Keys) { + var i = 0; + if (!r.TryGetValue(t, out i)) { + i = 0; + } + r[t] = i + other.dict[t]; + } + return new MultiSet(r.ToImmutable()); + } + public MultiSet Intersect(MultiSet other) { + if (dict.Count == 0) + return this; + else if (other.dict.Count == 0) + return other; + var r = ImmutableDictionary.Empty.ToBuilder(); + foreach (T t in dict.Keys) { + if (other.dict.ContainsKey(t)) { + r[t] = other.dict[t] < dict[t] ? other.dict[t] : dict[t]; + } + } + return new MultiSet(r.ToImmutable()); + } + public MultiSet Difference(MultiSet other) { // \result == this - other + if (dict.Count == 0) + return this; + else if (other.dict.Count == 0) + return this; + var r = ImmutableDictionary.Empty.ToBuilder(); + foreach (T t in dict.Keys) { + if (!other.dict.ContainsKey(t)) { + r[t] = dict[t]; + } else if (other.dict[t] < dict[t]) { + r[t] = dict[t] - other.dict[t]; + } + } + return new MultiSet(r.ToImmutable()); + } + public IEnumerable Elements { + get { + foreach (T t in dict.Keys) { + int n; + dict.TryGetValue(t, out n); + for (int i = 0; i < n; i ++) { + yield return t; + } + } + } + } + } + + public partial class Map + { + readonly ImmutableDictionary dict; + Map(ImmutableDictionary d) { + dict = d; + } + public static readonly Map Empty = new Map(ImmutableDictionary.Empty); + public static Map FromElements(params Pair[] values) { + var d = ImmutableDictionary.Empty.ToBuilder(); + foreach (Pair p in values) { + d[p.Car] = p.Cdr; + } + return new Map(d.ToImmutable()); + } + public static Map FromCollection(List> values) { + var d = ImmutableDictionary.Empty.ToBuilder(); + foreach (Pair p in values) { + d[p.Car] = p.Cdr; + } + return new Map(d.ToImmutable()); + } + public int Length { + get { return dict.Count; } + } + public long LongLength { + get { return dict.Count; } + } + public bool Equals(Map other) { + foreach (U u in dict.Keys) { + V v1, v2; + if (!dict.TryGetValue(u, out v1)) { + return false; // this shouldn't happen + } + if (!other.dict.TryGetValue(u, out v2)) { + return false; // other dictionary does not contain this element + } + if (!v1.Equals(v2)) { + return false; + } + } + foreach (U u in other.dict.Keys) { + if (!dict.ContainsKey(u)) { + return false; // this shouldn't happen + } + } + return true; + } + public override bool Equals(object other) { + return other is Map && Equals((Map)other); + } + public override int GetHashCode() { + var hashCode = 1; + foreach (var kv in dict) { + var key = kv.Key.GetHashCode(); + key = (key << 3) | (key >> 29) ^ kv.Value.GetHashCode(); + hashCode = hashCode * (key + 3); + } + return hashCode; + } + public override string ToString() { + var s = "map["; + var sep = ""; + foreach (var kv in dict) { + s += sep + kv.Key.ToString() + " := " + kv.Value.ToString(); + sep = ", "; + } + return s + "]"; + } + public bool IsDisjointFrom(Map other) { + foreach (U u in dict.Keys) { + if (other.dict.ContainsKey(u)) + return false; + } + foreach (U u in other.dict.Keys) { + if (dict.ContainsKey(u)) + return false; + } + return true; + } + public bool Contains(U u) { + return dict.ContainsKey(u); + } + public V Select(U index) { + return dict[index]; + } + public Map Update(U index, V val) { + return new Map(dict.SetItem(index, val)); + } + public IEnumerable Domain { + get { + return dict.Keys; + } + } + } +#else // !def DAFNY_USE_SYSTEM_COLLECTIONS_IMMUTABLE + public class Set + { + HashSet set; + Set(HashSet s) { + this.set = s; + } + public static Set Empty { + get { + return new Set(new HashSet()); + } + } + public static Set FromElements(params T[] values) { + var s = new HashSet(); + foreach (T t in values) + s.Add(t); + return new Set(s); + } + public static Set FromCollection(ICollection values) { + HashSet s = new HashSet(); + foreach (T t in values) + s.Add(t); + return new Set(s); + } + public int Length { + get { return this.set.Count; } + } + public long LongLength { + get { return this.set.Count; } + } + public IEnumerable Elements { + get { + return this.set; + } + } + /// + /// This is an inefficient iterator for producing all subsets of "this". Each set returned is the same + /// Set object (but this Set object is fresh; in particular, it is not "this"). + /// + public IEnumerable> AllSubsets { + get { + // Start by putting all set elements into a list + var elmts = new List(); + elmts.AddRange(this.set); + var n = elmts.Count; + var which = new bool[n]; + var s = new Set(new HashSet()); + while (true) { + yield return s; + // "add 1" to "which", as if doing a carry chain. For every digit changed, change the membership of the corresponding element in "s". + int i = 0; + for (; i < n && which[i]; i++) { + which[i] = false; + s.set.Remove(elmts[i]); + } + if (i == n) { + // we have cycled through all the subsets + break; + } + which[i] = true; + s.set.Add(elmts[i]); + } + } + } + public bool Equals(Set other) { + return this.set.Count == other.set.Count && IsSubsetOf(other); + } + public override bool Equals(object other) { + return other is Set && Equals((Set)other); + } + public override int GetHashCode() { + var hashCode = 1; + foreach (var t in this.set) { + hashCode = hashCode * (t.GetHashCode()+3); + } + return hashCode; + } + public override string ToString() { + var s = "{"; + var sep = ""; + foreach (var t in this.set) { + s += sep + t.ToString(); + sep = ", "; + } + return s + "}"; + } + public bool IsProperSubsetOf(Set other) { + return this.set.Count < other.set.Count && IsSubsetOf(other); + } + public bool IsSubsetOf(Set other) { + if (other.set.Count < this.set.Count) + return false; + foreach (T t in this.set) { + if (!other.set.Contains(t)) + return false; + } + return true; + } + public bool IsSupersetOf(Set other) { + return other.IsSubsetOf(this); + } + public bool IsProperSupersetOf(Set other) { + return other.IsProperSubsetOf(this); + } + public bool IsDisjointFrom(Set other) { + HashSet a, b; + if (this.set.Count < other.set.Count) { + a = this.set; b = other.set; + } else { + a = other.set; b = this.set; + } + foreach (T t in a) { + if (b.Contains(t)) + return false; + } + return true; + } + public bool Contains(T t) { + return this.set.Contains(t); + } + public Set Union(Set other) { + if (this.set.Count == 0) + return other; + else if (other.set.Count == 0) + return this; + HashSet a, b; + if (this.set.Count < other.set.Count) { + a = this.set; b = other.set; + } else { + a = other.set; b = this.set; + } + var r = new HashSet(); + foreach (T t in b) + r.Add(t); + foreach (T t in a) + r.Add(t); + return new Set(r); + } + public Set Intersect(Set other) { + if (this.set.Count == 0) + return this; + else if (other.set.Count == 0) + return other; + HashSet a, b; + if (this.set.Count < other.set.Count) { + a = this.set; b = other.set; + } else { + a = other.set; b = this.set; + } + var r = new HashSet(); + foreach (T t in a) { + if (b.Contains(t)) + r.Add(t); + } + return new Set(r); + } + public Set Difference(Set other) { + if (this.set.Count == 0) + return this; + else if (other.set.Count == 0) + return this; + var r = new HashSet(); + foreach (T t in this.set) { + if (!other.set.Contains(t)) + r.Add(t); + } + return new Set(r); + } + } + public class MultiSet + { + Dictionary dict; + MultiSet(Dictionary d) { + dict = d; + } + public static MultiSet Empty { + get { + return new MultiSet(new Dictionary(0)); + } + } + public static MultiSet FromElements(params T[] values) { + Dictionary d = new Dictionary(values.Length); + foreach (T t in values) { + var i = 0; + if (!d.TryGetValue(t, out i)) { + i = 0; + } + d[t] = i + 1; + } + return new MultiSet(d); + } + public static MultiSet FromCollection(ICollection values) { + Dictionary d = new Dictionary(); + foreach (T t in values) { + var i = 0; + if (!d.TryGetValue(t, out i)) { + i = 0; + } + d[t] = i + 1; + } + return new MultiSet(d); + } + public static MultiSet FromSeq(Sequence values) { + Dictionary d = new Dictionary(); + foreach (T t in values.Elements) { + var i = 0; + if (!d.TryGetValue(t, out i)) { + i = 0; + } + d[t] = i + 1; + } + return new MultiSet(d); + } + public static MultiSet FromSet(Set values) { + Dictionary d = new Dictionary(); + foreach (T t in values.Elements) { + d[t] = 1; + } + return new MultiSet(d); + } + + public bool Equals(MultiSet other) { + return other.IsSubsetOf(this) && this.IsSubsetOf(other); + } + public override bool Equals(object other) { + return other is MultiSet && Equals((MultiSet)other); + } + public override int GetHashCode() { + var hashCode = 1; + foreach (var kv in dict) { + var key = kv.Key.GetHashCode(); + key = (key << 3) | (key >> 29) ^ kv.Value.GetHashCode(); + hashCode = hashCode * (key + 3); + } + return hashCode; + } + public override string ToString() { + var s = "multiset{"; + var sep = ""; + foreach (var kv in dict) { + var t = kv.Key.ToString(); + for (int i = 0; i < kv.Value; i++) { + s += sep + t.ToString(); + sep = ", "; + } + } + return s + "}"; + } + public bool IsProperSubsetOf(MultiSet other) { + return !Equals(other) && IsSubsetOf(other); + } + public bool IsSubsetOf(MultiSet other) { + foreach (T t in dict.Keys) { + if (!other.dict.ContainsKey(t) || other.dict[t] < dict[t]) + return false; + } + return true; + } + public bool IsSupersetOf(MultiSet other) { + return other.IsSubsetOf(this); + } + public bool IsProperSupersetOf(MultiSet other) { + return other.IsProperSubsetOf(this); + } + public bool IsDisjointFrom(MultiSet other) { + foreach (T t in dict.Keys) { + if (other.dict.ContainsKey(t)) + return false; + } + foreach (T t in other.dict.Keys) { + if (dict.ContainsKey(t)) + return false; + } + return true; + } + public bool Contains(T t) { + return dict.ContainsKey(t); + } + public MultiSet Union(MultiSet other) { + if (dict.Count == 0) + return other; + else if (other.dict.Count == 0) + return this; + var r = new Dictionary(); + foreach (T t in dict.Keys) { + var i = 0; + if (!r.TryGetValue(t, out i)) { + i = 0; + } + r[t] = i + dict[t]; + } + foreach (T t in other.dict.Keys) { + var i = 0; + if (!r.TryGetValue(t, out i)) { + i = 0; + } + r[t] = i + other.dict[t]; + } + return new MultiSet(r); + } + public MultiSet Intersect(MultiSet other) { + if (dict.Count == 0) + return this; + else if (other.dict.Count == 0) + return other; + var r = new Dictionary(); + foreach (T t in dict.Keys) { + if (other.dict.ContainsKey(t)) { + r.Add(t, other.dict[t] < dict[t] ? other.dict[t] : dict[t]); + } + } + return new MultiSet(r); + } + public MultiSet Difference(MultiSet other) { // \result == this - other + if (dict.Count == 0) + return this; + else if (other.dict.Count == 0) + return this; + var r = new Dictionary(); + foreach (T t in dict.Keys) { + if (!other.dict.ContainsKey(t)) { + r.Add(t, dict[t]); + } else if (other.dict[t] < dict[t]) { + r.Add(t, dict[t] - other.dict[t]); + } + } + return new MultiSet(r); + } + public IEnumerable Elements { + get { + List l = new List(); + foreach (T t in dict.Keys) { + int n; + dict.TryGetValue(t, out n); + for (int i = 0; i < n; i ++) { + l.Add(t); + } + } + return l; + } + } + } + + public class Map + { + Dictionary dict; + Map(Dictionary d) { + dict = d; + } + public static Map Empty { + get { + return new Map(new Dictionary()); + } + } + public static Map FromElements(params Pair[] values) { + Dictionary d = new Dictionary(values.Length); + foreach (Pair p in values) { + d[p.Car] = p.Cdr; + } + return new Map(d); + } + public static Map FromCollection(List> values) { + Dictionary d = new Dictionary(values.Count); + foreach (Pair p in values) { + d[p.Car] = p.Cdr; + } + return new Map(d); + } + public int Length { + get { return dict.Count; } + } + public long LongLength { + get { return dict.Count; } + } + public bool Equals(Map other) { + foreach (U u in dict.Keys) { + V v1, v2; + if (!dict.TryGetValue(u, out v1)) { + return false; // this shouldn't happen + } + if (!other.dict.TryGetValue(u, out v2)) { + return false; // other dictionary does not contain this element + } + if (!v1.Equals(v2)) { + return false; + } + } + foreach (U u in other.dict.Keys) { + if (!dict.ContainsKey(u)) { + return false; // this shouldn't happen + } + } + return true; + } + public override bool Equals(object other) { + return other is Map && Equals((Map)other); + } + public override int GetHashCode() { + var hashCode = 1; + foreach (var kv in dict) { + var key = kv.Key.GetHashCode(); + key = (key << 3) | (key >> 29) ^ kv.Value.GetHashCode(); + hashCode = hashCode * (key + 3); + } + return hashCode; + } + public override string ToString() { + var s = "map["; + var sep = ""; + foreach (var kv in dict) { + s += sep + kv.Key.ToString() + " := " + kv.Value.ToString(); + sep = ", "; + } + return s + "]"; + } + public bool IsDisjointFrom(Map other) { + foreach (U u in dict.Keys) { + if (other.dict.ContainsKey(u)) + return false; + } + foreach (U u in other.dict.Keys) { + if (dict.ContainsKey(u)) + return false; + } + return true; + } + public bool Contains(U u) { + return dict.ContainsKey(u); + } + public V Select(U index) { + return dict[index]; + } + public Map Update(U index, V val) { + Dictionary d = new Dictionary(dict); + d[index] = val; + return new Map(d); + } + public IEnumerable Domain { + get { + return dict.Keys; + } + } + } +#endif + public class Sequence + { + T[] elmts; + public Sequence(T[] ee) { + elmts = ee; + } + public static Sequence Empty { + get { + return new Sequence(new T[0]); + } + } + public static Sequence FromElements(params T[] values) { + return new Sequence(values); + } + public static Sequence FromString(string s) { + return new Sequence(s.ToCharArray()); + } + public int Length { + get { return elmts.Length; } + } + public long LongLength { + get { return elmts.LongLength; } + } + public T[] Elements { + get { + return elmts; + } + } + public IEnumerable UniqueElements { + get { + var st = Set.FromElements(elmts); + return st.Elements; + } + } + public T Select(ulong index) { + return elmts[index]; + } + public T Select(long index) { + return elmts[index]; + } + public T Select(uint index) { + return elmts[index]; + } + public T Select(int index) { + return elmts[index]; + } + public T Select(BigInteger index) { + return elmts[(int)index]; + } + public Sequence Update(long index, T t) { + T[] a = (T[])elmts.Clone(); + a[index] = t; + return new Sequence(a); + } + public Sequence Update(ulong index, T t) { + return Update((long)index, t); + } + public Sequence Update(BigInteger index, T t) { + return Update((long)index, t); + } + public bool Equals(Sequence other) { + int n = elmts.Length; + return n == other.elmts.Length && EqualUntil(other, n); + } + public override bool Equals(object other) { + return other is Sequence && Equals((Sequence)other); + } + public override int GetHashCode() { + if (elmts == null || elmts.Length == 0) + return 0; + var hashCode = 0; + for (var i = 0; i < elmts.Length; i++) { + hashCode = (hashCode << 3) | (hashCode >> 29) ^ elmts[i].GetHashCode(); + } + return hashCode; + } + public override string ToString() { + if (elmts is char[]) { + var s = ""; + foreach (var t in elmts) { + s += t.ToString(); + } + return s; + } else { + var s = "["; + var sep = ""; + foreach (var t in elmts) { + s += sep + t.ToString(); + sep = ", "; + } + return s + "]"; + } + } + bool EqualUntil(Sequence other, int n) { + for (int i = 0; i < n; i++) { + if (!elmts[i].Equals(other.elmts[i])) + return false; + } + return true; + } + public bool IsProperPrefixOf(Sequence other) { + int n = elmts.Length; + return n < other.elmts.Length && EqualUntil(other, n); + } + public bool IsPrefixOf(Sequence other) { + int n = elmts.Length; + return n <= other.elmts.Length && EqualUntil(other, n); + } + public Sequence Concat(Sequence other) { + if (elmts.Length == 0) + return other; + else if (other.elmts.Length == 0) + return this; + T[] a = new T[elmts.Length + other.elmts.Length]; + System.Array.Copy(elmts, 0, a, 0, elmts.Length); + System.Array.Copy(other.elmts, 0, a, elmts.Length, other.elmts.Length); + return new Sequence(a); + } + public bool Contains(T t) { + int n = elmts.Length; + for (int i = 0; i < n; i++) { + if (t.Equals(elmts[i])) + return true; + } + return false; + } + public Sequence Take(long m) { + if (elmts.LongLength == m) + return this; + T[] a = new T[m]; + System.Array.Copy(elmts, a, m); + return new Sequence(a); + } + public Sequence Take(ulong n) { + return Take((long)n); + } + public Sequence Take(BigInteger n) { + return Take((long)n); + } + public Sequence Drop(long m) { + if (m == 0) + return this; + T[] a = new T[elmts.Length - m]; + System.Array.Copy(elmts, m, a, 0, elmts.Length - m); + return new Sequence(a); + } + public Sequence Drop(ulong n) { + return Drop((long)n); + } + public Sequence Drop(BigInteger n) { + if (n.IsZero) + return this; + return Drop((long)n); + } + } + public struct Pair + { + public readonly A Car; + public readonly B Cdr; + public Pair(A a, B b) { + this.Car = a; + this.Cdr = b; + } + } + public partial class Helpers { + // Computing forall/exists quantifiers + public static bool QuantBool(bool frall, System.Predicate pred) { + if (frall) { + return pred(false) && pred(true); + } else { + return pred(false) || pred(true); + } + } + public static bool QuantInt(BigInteger lo, BigInteger hi, bool frall, System.Predicate pred) { + for (BigInteger i = lo; i < hi; i++) { + if (pred(i) != frall) { return !frall; } + } + return frall; + } + public static bool QuantSet(Dafny.Set set, bool frall, System.Predicate pred) { + foreach (var u in set.Elements) { + if (pred(u) != frall) { return !frall; } + } + return frall; + } + public static bool QuantMap(Dafny.Map map, bool frall, System.Predicate pred) { + foreach (var u in map.Domain) { + if (pred(u) != frall) { return !frall; } + } + return frall; + } + public static bool QuantSeq(Dafny.Sequence seq, bool frall, System.Predicate pred) { + foreach (var u in seq.Elements) { + if (pred(u) != frall) { return !frall; } + } + return frall; + } + public static bool QuantDatatype(IEnumerable set, bool frall, System.Predicate pred) { + foreach (var u in set) { + if (pred(u) != frall) { return !frall; } + } + return frall; + } + // Enumerating other collections + public delegate Dafny.Set ComprehensionDelegate(); + public delegate Dafny.Map MapComprehensionDelegate(); + public static IEnumerable AllBooleans { + get { + yield return false; + yield return true; + } + } + public static IEnumerable AllIntegers { + get { + yield return new BigInteger(0); + for (var j = new BigInteger(1);; j++) { + yield return j; + yield return -j; + } + } + } + public static IEnumerable IntegerRange(BigInteger lo, BigInteger hi) { + for (var j = lo; j < hi; j++) { + yield return j; + } + } + // pre: b != 0 + // post: result == a/b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation) + public static sbyte EuclideanDivision_sbyte(sbyte a, sbyte b) { + return (sbyte)EuclideanDivision_int(a, b); + } + public static short EuclideanDivision_short(short a, short b) { + return (short)EuclideanDivision_int(a, b); + } + public static int EuclideanDivision_int(int a, int b) { + if (0 <= a) { + if (0 <= b) { + // +a +b: a/b + return (int)(((uint)(a)) / ((uint)(b))); + } else { + // +a -b: -(a/(-b)) + return -((int)(((uint)(a)) / ((uint)(unchecked(-b))))); + } + } else { + if (0 <= b) { + // -a +b: -((-a-1)/b) - 1 + return -((int)(((uint)(-(a + 1))) / ((uint)(b)))) - 1; + } else { + // -a -b: ((-a-1)/(-b)) + 1 + return ((int)(((uint)(-(a + 1))) / ((uint)(unchecked(-b))))) + 1; + } + } + } + public static long EuclideanDivision_long(long a, long b) { + if (0 <= a) { + if (0 <= b) { + // +a +b: a/b + return (long)(((ulong)(a)) / ((ulong)(b))); + } else { + // +a -b: -(a/(-b)) + return -((long)(((ulong)(a)) / ((ulong)(unchecked(-b))))); + } + } else { + if (0 <= b) { + // -a +b: -((-a-1)/b) - 1 + return -((long)(((ulong)(-(a + 1))) / ((ulong)(b)))) - 1; + } else { + // -a -b: ((-a-1)/(-b)) + 1 + return ((long)(((ulong)(-(a + 1))) / ((ulong)(unchecked(-b))))) + 1; + } + } + } + public static BigInteger EuclideanDivision(BigInteger a, BigInteger b) { + if (0 <= a.Sign) { + if (0 <= b.Sign) { + // +a +b: a/b + return BigInteger.Divide(a, b); + } else { + // +a -b: -(a/(-b)) + return BigInteger.Negate(BigInteger.Divide(a, BigInteger.Negate(b))); + } + } else { + if (0 <= b.Sign) { + // -a +b: -((-a-1)/b) - 1 + return BigInteger.Negate(BigInteger.Divide(BigInteger.Negate(a) - 1, b)) - 1; + } else { + // -a -b: ((-a-1)/(-b)) + 1 + return BigInteger.Divide(BigInteger.Negate(a) - 1, BigInteger.Negate(b)) + 1; + } + } + } + // pre: b != 0 + // post: result == a%b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation) + public static sbyte EuclideanModulus_sbyte(sbyte a, sbyte b) { + return (sbyte)EuclideanModulus_int(a, b); + } + public static short EuclideanModulus_short(short a, short b) { + return (short)EuclideanModulus_int(a, b); + } + public static int EuclideanModulus_int(int a, int b) { + uint bp = (0 <= b) ? (uint)b : (uint)(unchecked(-b)); + if (0 <= a) { + // +a: a % b' + return (int)(((uint)a) % bp); + } else { + // c = ((-a) % b') + // -a: b' - c if c > 0 + // -a: 0 if c == 0 + uint c = ((uint)(unchecked(-a))) % bp; + return (int)(c == 0 ? c : bp - c); + } + } + public static long EuclideanModulus_long(long a, long b) { + ulong bp = (0 <= b) ? (ulong)b : (ulong)(unchecked(-b)); + if (0 <= a) { + // +a: a % b' + return (long)(((ulong)a) % bp); + } else { + // c = ((-a) % b') + // -a: b' - c if c > 0 + // -a: 0 if c == 0 + ulong c = ((ulong)(unchecked(-a))) % bp; + return (long)(c == 0 ? c : bp - c); + } + } + public static BigInteger EuclideanModulus(BigInteger a, BigInteger b) { + var bp = BigInteger.Abs(b); + if (0 <= a.Sign) { + // +a: a % b' + return BigInteger.Remainder(a, bp); + } else { + // c = ((-a) % b') + // -a: b' - c if c > 0 + // -a: 0 if c == 0 + var c = BigInteger.Remainder(BigInteger.Negate(a), bp); + return c.IsZero ? c : BigInteger.Subtract(bp, c); + } + } + public static Sequence SeqFromArray(T[] array) { + return new Sequence((T[])array.Clone()); + } + // In .NET version 4.5, it it possible to mark a method with "AggressiveInlining", which says to inline the + // method if possible. Method "ExpressionSequence" would be a good candidate for it: + // [System.Runtime.CompilerServices.MethodImpl(System.Runtime.CompilerServices.MethodImplOptions.AggressiveInlining)] + public static U ExpressionSequence(T t, U u) + { + return u; + } + + public static U Let(T t, Func f) { + return f(t); + } + + public delegate Result Function(Input input); + + public static A Id(A a) { + return a; + } + } + + public struct BigRational + { + public static readonly BigRational ZERO = new BigRational(0); + + BigInteger num, den; // invariant 1 <= den + public override string ToString() { + return string.Format("({0}.0 / {1}.0)", num, den); + } + public BigRational(int n) { + num = new BigInteger(n); + den = BigInteger.One; + } + public BigRational(BigInteger n, BigInteger d) { + // requires 1 <= d + num = n; + den = d; + } + public BigInteger ToBigInteger() { + if (0 <= num) { + return num / den; + } else { + return (num - den + 1) / den; + } + } + /// + /// Returns values such that aa/dd == a and bb/dd == b. + /// + private static void Normalize(BigRational a, BigRational b, out BigInteger aa, out BigInteger bb, out BigInteger dd) { + var gcd = BigInteger.GreatestCommonDivisor(a.den, b.den); + var xx = a.den / gcd; + var yy = b.den / gcd; + // We now have a == a.num / (xx * gcd) and b == b.num / (yy * gcd). + aa = a.num * yy; + bb = b.num * xx; + dd = a.den * yy; + } + public int CompareTo(BigRational that) { + // simple things first + int asign = this.num.Sign; + int bsign = that.num.Sign; + if (asign < 0 && 0 <= bsign) { + return 1; + } else if (asign <= 0 && 0 < bsign) { + return 1; + } else if (bsign < 0 && 0 <= asign) { + return -1; + } else if (bsign <= 0 && 0 < asign) { + return -1; + } + BigInteger aa, bb, dd; + Normalize(this, that, out aa, out bb, out dd); + return aa.CompareTo(bb); + } + public override int GetHashCode() { + return num.GetHashCode() + 29 * den.GetHashCode(); + } + public override bool Equals(object obj) { + if (obj is BigRational) { + return this == (BigRational)obj; + } else { + return false; + } + } + public static bool operator ==(BigRational a, BigRational b) { + return a.CompareTo(b) == 0; + } + public static bool operator !=(BigRational a, BigRational b) { + return a.CompareTo(b) != 0; + } + public static bool operator >(BigRational a, BigRational b) { + return 0 < a.CompareTo(b); + } + public static bool operator >=(BigRational a, BigRational b) { + return 0 <= a.CompareTo(b); + } + public static bool operator <(BigRational a, BigRational b) { + return a.CompareTo(b) < 0; + } + public static bool operator <=(BigRational a, BigRational b) { + return a.CompareTo(b) <= 0; + } + public static BigRational operator +(BigRational a, BigRational b) { + BigInteger aa, bb, dd; + Normalize(a, b, out aa, out bb, out dd); + return new BigRational(aa + bb, dd); + } + public static BigRational operator -(BigRational a, BigRational b) { + BigInteger aa, bb, dd; + Normalize(a, b, out aa, out bb, out dd); + return new BigRational(aa - bb, dd); + } + public static BigRational operator -(BigRational a) { + return new BigRational(-a.num, a.den); + } + public static BigRational operator *(BigRational a, BigRational b) { + return new BigRational(a.num * b.num, a.den * b.den); + } + public static BigRational operator /(BigRational a, BigRational b) { + // Compute the reciprocal of b + BigRational bReciprocal; + if (0 < b.num) { + bReciprocal = new BigRational(b.den, b.num); + } else { + // this is the case b.num < 0 + bReciprocal = new BigRational(-b.den, -b.num); + } + return a * bReciprocal; + } + } +} -- cgit v1.2.3 From 0c1ec594e68dab4fcd458a00f9f7a1ac6de2e218 Mon Sep 17 00:00:00 2001 From: leino Date: Mon, 28 Sep 2015 13:16:15 -0700 Subject: Changed computation of ghosts until pass 2 of resolution. Other clean-up in resolution passes, like: Include everything of type "char" into bounds that are discovered, and likewise for reference types. Allow more set comprehensions, determining if they are finite based on their argument type. Changed CalcExpr.SubExpressions to not include computed expressions. --- Binaries/DafnyRuntime.cs | 13 + Source/Dafny/Cloner.cs | 14 +- Source/Dafny/Compiler.cs | 11 + Source/Dafny/DafnyAst.cs | 172 +++++++- Source/Dafny/Resolver.cs | 562 ++++++++++++++++----------- Test/dafny0/AssumptionVariables0.dfy.expect | 4 +- Test/dafny0/CallStmtTests.dfy | 34 +- Test/dafny0/CallStmtTests.dfy.expect | 4 +- Test/dafny0/DiscoverBounds.dfy.expect | 6 +- Test/dafny0/NonGhostQuantifiers.dfy | 7 + Test/dafny0/NonGhostQuantifiers.dfy.expect | 22 +- Test/dafny0/ParallelResolveErrors.dfy | 13 +- Test/dafny0/ParallelResolveErrors.dfy.expect | 36 +- Test/dafny0/ResolutionErrors.dfy | 278 +++++++++++-- Test/dafny0/ResolutionErrors.dfy.expect | 87 +++-- Test/dafny0/TypeTests.dfy | 50 +-- Test/dafny0/TypeTests.dfy.expect | 14 +- Test/dafny4/set-compr.dfy.expect | 4 +- 18 files changed, 925 insertions(+), 406 deletions(-) (limited to 'Binaries/DafnyRuntime.cs') diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs index d1a3c092..4dda19fe 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 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 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 AllChars { + get { + for (int i = 0; i < 0x10000; i++) { + yield return (char)i; + } + } + } public static IEnumerable AllIntegers { get { yield return new BigInteger(0); diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index dd2eed69..032e30a0 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(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 477acabf..cdd968cf 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -1566,6 +1566,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); @@ -1777,6 +1780,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) { @@ -2831,6 +2836,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("); @@ -2898,6 +2905,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) { @@ -2971,6 +2980,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 2a98d5c2..b460d9b4 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -509,6 +509,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; } } @@ -2376,6 +2397,48 @@ namespace Microsoft.Dafny { YieldCountVariable.type = YieldCountVariable.OptionalType; // resolve YieldCountVariable here } + /// + /// 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. + /// + public virtual IEnumerable 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; + } + } + } + /// /// 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 @@ -2475,6 +2538,11 @@ namespace Microsoft.Dafny { return EnclosingClass.FullCompileName + ".@" + CompileName; } } + public virtual IEnumerable SubExpressions { + get { + yield break; + } + } } public class Field : MemberDecl { @@ -2999,6 +3067,26 @@ namespace Microsoft.Dafny { public bool IsBuiltin; public Function OverriddenFunction; + public override IEnumerable 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 @@ -3213,6 +3301,24 @@ namespace Microsoft.Dafny { public readonly ISet AssignedAssumptionVariables = new HashSet(); public Method OverriddenMethod; + public override IEnumerable 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)); @@ -4821,18 +4927,32 @@ namespace Microsoft.Dafny { } public override IEnumerable 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 AllCalcOps { + get { + if (Op != null) { + yield return Op; } - if (Result != null) { - yield return Result; + foreach (var stepop in StepOps) { + yield return stepop; + } + if (ResultOp != null) { + yield return ResultOp; } } } @@ -6637,7 +6757,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 Constraint_Bounds; // initialized and filled in by resolver; null for Exact=true and for a ghost statement + public List 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 Constraint_MissingBounds; // filled in during resolution; remains "null" if Exact==true or if bounds can be found // invariant Constraint_Bounds == null || Constraint_MissingBounds == null; @@ -6790,6 +6910,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; @@ -6864,6 +7000,24 @@ namespace Microsoft.Dafny { public List MissingBounds; // filled in during resolution; remains "null" if bounds can be found // invariant Bounds == null || MissingBounds == null; + public List UncompilableBoundVars() { + var bvs = new List(); + 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 bvars, Expression range, Expression term, Attributes attrs) : base(tok) { Contract.Requires(tok != null); diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index d82d7d1f..ec3a69c9 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1313,16 +1313,6 @@ namespace Microsoft.Dafny } } - private readonly List needFiniteBoundsChecks_SetComprehension = new List(); - private readonly List needBoundsDiscovery_AssignSuchThatStmt = new List(); - private readonly List needFiniteBoundsChecks_LetSuchThatExpr = new List(); - 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 NativeTypes = new List() { new NativeType("byte", 0, 0x100, "", true), new NativeType("sbyte", -0x80, 0x80, "", true), @@ -1338,13 +1328,23 @@ namespace Microsoft.Dafny Contract.Requires(declarations != null); Contract.Requires(cce.NonNullElements(datatypeDependencies)); Contract.Requires(cce.NonNullElements(codatatypeDependencies)); - Contract.Requires(NFBC_Count == 0); Contract.Requires(AllTypeConstraints.Count == 0); - Contract.Ensures(NFBC_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. + // Some bounds are discovered during this pass [is this necessary? can they be + // moved to pass 1 like the other bounds discovery? --KRML], namely: + // - forall statements + // - quantifier expressions + // - map comprehensions + // 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 @@ -1403,172 +1403,80 @@ namespace Microsoft.Dafny allTypeParameters.PopMarker(); } + // ---------------------------------- 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: + // - set comprehensions + // - 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 nativeTypeMap = new Dictionary(); 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); + 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); foreach (var member in cl.Members) { - var m = member as Method; - if (m != null && m.Body != null) { - DetermineTailRecursion(m); + 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) { + CheckIsNonGhost(f.Body); + } + DetermineTailRecursion(f); + } + if (prevErrCnt == reporter.Count(ErrorLevel.Error) && member is ICodeContext) { + member.SubExpressions.Iter(e => CheckExpression(e, this, (ICodeContext)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); - } - } - } - 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) { Contract.Assert(dd.Constraint != null); - CheckTypeInference(dd.Constraint); - - Func 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 potentialNativeTypes = - (stringNativeType != null) ? new List { stringNativeType } : - (boolNativeType == false) ? new List() : - 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); } } } - if (reporter.Count(ErrorLevel.Error) == prevErrorCount) { - // At this point, it is necessary to know for each statement and expression if it is ghost or not - foreach (var e in needFiniteBoundsChecks_SetComprehension) { - CheckTypeInference(e.Range); // we need to resolve operators before the call to DiscoverBounds - List missingBounds; - e.Bounds = DiscoverBestBounds_MultipleVars(e.BoundVars, e.Range, true, true, out missingBounds); - if (missingBounds.Count != 0) { - e.MissingBounds = missingBounds; - if (e.Finite) { - foreach (var bv in e.MissingBounds) { - reporter.Error(MessageSource.Resolver, e, "a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name); - } - } - } - } - foreach (AssignSuchThatStmt s in needBoundsDiscovery_AssignSuchThatStmt) { - Contract.Assert(!s.IsGhost); - var varLhss = new List(); - foreach (var lhs in s.Lhss) { - var ide = (IdentifierExpr)lhs.Resolved; // successful resolution above implies all LHS's are IdentifierExpr's - varLhss.Add(ide.Var); - } - - List 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; - } - } - foreach (var e in needFiniteBoundsChecks_LetSuchThatExpr) { - Contract.Assert(!e.Exact); // only let-such-that expressions are ever added to the list - Contract.Assert(e.RHSs.Count == 1); // if we got this far, the resolver will have checked this condition successfully - var constraint = e.RHSs[0]; - CheckTypeInference(constraint); // we need to resolve operators before the call to DiscoverBounds - List missingBounds; - var vars = new List(e.BoundVars); - var bestBounds = DiscoverBestBounds_MultipleVars(vars, constraint, true, false, out missingBounds); - if (missingBounds.Count != 0) { - e.Constraint_MissingBounds = missingBounds; - foreach (var bv in e.Constraint_MissingBounds) { - reporter.Error(MessageSource.Resolver, e, "a non-ghost let-such-that constraint must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name); - } - } else { - e.Constraint_Bounds = bestBounds; - } - } - } - needFiniteBoundsChecks_SetComprehension.Clear(); - needFiniteBoundsChecks_LetSuchThatExpr.Clear(); + // ---------------------------------- Pass 2 ---------------------------------- + // This pass fills in various additional information. + // ---------------------------------------------------------------------------- if (reporter.Count(ErrorLevel.Error) == prevErrorCount) { // fill in the postconditions and bodies of prefix lemmas @@ -1894,6 +1802,93 @@ namespace Microsoft.Dafny } } + private void FigureOutNativeType(NewtypeDecl dd, Dictionary 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 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 potentialNativeTypes = + (stringNativeType != null) ? new List { stringNativeType } : + (boolNativeType == false) ? new List() : + 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 + "\"}"); + } + } + } + /// /// 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. @@ -2123,16 +2118,60 @@ namespace Microsoft.Dafny } else if (stmt is ForallStmt) { var s = (ForallStmt)stmt; s.BoundVars.Iter(bv => CheckTypeIsDetermined(bv.tok, bv.Type, "bound variable")); + } else if (stmt is AssignSuchThatStmt) { + var s = (AssignSuchThatStmt)stmt; + if (s.AssumeToken == null) { + var varLhss = new List(); + 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 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); + } + } + if (e is SetComprehension) { + var sc = (SetComprehension)e; + if (sc.Finite) { + // A set must be finite. Discover bounds for the Range expression, but report an error only if the Term is not + // of a finite-individuals type. + List missingBounds; + sc.Bounds = DiscoverBestBounds_MultipleVars(sc.BoundVars, sc.Range, true, true, out missingBounds); + if (missingBounds.Count != 0) { + sc.MissingBounds = missingBounds; + if (sc.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 { + foreach (var bv in sc.MissingBounds) { + resolver.reporter.Error(MessageSource.Resolver, sc, "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); + } + } } } } @@ -2172,6 +2211,7 @@ namespace Microsoft.Dafny var bin = expr as BinaryExpr; if (bin != null) { bin.ResolvedOp = ResolveOp(bin.Op, bin.E1.Type); + } } } @@ -2249,6 +2289,58 @@ namespace Microsoft.Dafny } #endregion CheckTypeInference + // ------------------------------------------------------------------------------------------------------ + // ----- CheckExpression -------------------------------------------------------------------------------- + // ------------------------------------------------------------------------------------------------------ + #region CheckExpression + /// + /// This method computes ghost interests in the statement portion of StmtExpr's and + /// checks for hint restrictions in any CalcStmt. + /// + 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); + } + /// + /// This method computes ghost interests in the statement portion of StmtExpr's and + /// checks for hint restrictions in any CalcStmt. + /// + 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()); + } + } + } + } + #endregion + // ------------------------------------------------------------------------------------------------------ // ----- CheckTailRecursive ----------------------------------------------------------------------------- // ------------------------------------------------------------------------------------------------------ @@ -3009,11 +3101,11 @@ namespace Microsoft.Dafny // ----- ComputeGhostInterest --------------------------------------------------------------------------- // ------------------------------------------------------------------------------------------------------ #region ComputeGhostInterest - public void ComputeGhostInterest(Statement stmt, ICodeContext codeContext) { + 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, codeContext.IsGhost); + visitor.Visit(stmt, mustBeErasable); } class GhostInterest_Visitor { @@ -3037,12 +3129,6 @@ namespace Microsoft.Dafny Contract.Requires(msgArgs != null); resolver.reporter.Error(MessageSource.Resolver, expr, msg, msgArgs); } - protected void Error(IToken tok, string msg, params object[] msgArgs) { - Contract.Requires(tok != null); - Contract.Requires(msg != null); - Contract.Requires(msgArgs != null); - resolver.reporter.Error(MessageSource.Resolver, tok, msg, msgArgs); - } /// /// This method does three things: /// 0. Reports an error if "mustBeErasable" and the statement assigns to a non-ghost field @@ -3057,6 +3143,7 @@ namespace Microsoft.Dafny /// because break statements look at the ghost status of its enclosing statements. /// 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) { @@ -3107,9 +3194,6 @@ namespace Microsoft.Dafny } } } - if (!s.IsGhost) { - resolver.needBoundsDiscovery_AssignSuchThatStmt.Add(s); - } } else if (stmt is UpdateStmt) { var s = (UpdateStmt)stmt; @@ -3124,13 +3208,6 @@ namespace Microsoft.Dafny local.IsGhost = true; } } - foreach (var local in s.Locals) { - if (Attributes.Contains(local.Attributes, "assumption")) { - if (!local.IsGhost) { - Error(local.Tok, "assumption variable must be ghost"); - } - } - } s.IsGhost = (s.Update == null || s.Update.IsGhost) && s.Locals.All(v => v.IsGhost); if (s.Update != null) { Visit(s.Update, mustBeErasable); @@ -4040,14 +4117,10 @@ namespace Microsoft.Dafny var prevErrorCount = reporter.Count(ErrorLevel.Error); ResolveExpression(f.Body, new ResolveOpts(f, false)); SolveAllTypeConstraints(); - if (!f.IsGhost && prevErrorCount == reporter.Count(ErrorLevel.Error)) { - CheckIsNonGhost(f.Body); - } Contract.Assert(f.Body.Type != null); // follows from postcondition of ResolveExpression ConstrainTypes(f.Body.Type, f.ResultType, f, "Function body type mismatch (expected {0}, got {1})", f.ResultType, f.Body.Type); } scope.PopMarker(); - DetermineTailRecursion(f); } /// @@ -4187,7 +4260,7 @@ namespace Microsoft.Dafny ResolveBlockStatement(m.Body, m.IsGhost, m); SolveAllTypeConstraints(); if (reporter.Count(ErrorLevel.Error) == prevErrorCount) { - ComputeGhostInterest(m.Body, m); +//KRML ComputeGhostInterest(m.Body, m); } } @@ -4308,7 +4381,7 @@ namespace Microsoft.Dafny if (iter.Body != null) { ResolveBlockStatement(iter.Body, false, iter); if (reporter.Count(ErrorLevel.Error) == postSpecErrorCount) { - ComputeGhostInterest(iter.Body, iter); + //KRML ComputeGhostInterest(iter.Body, iter); } } @@ -5290,7 +5363,10 @@ namespace Microsoft.Dafny } 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"); } } } @@ -5599,7 +5675,6 @@ namespace Microsoft.Dafny loopStack = new List(); foreach (var h in s.Hints) { ResolveStatement(h, true, codeContext); - CheckHintRestrictions(h); } labeledStatements = prevLblStmts; loopStack = prevLoopStack; @@ -6347,9 +6422,6 @@ 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"); } - 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) { @@ -6633,8 +6705,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? /// - public void CheckHintRestrictions(Statement stmt) { + public void CheckHintRestrictions(Statement stmt, ISet localsAllowedInUpdates) { Contract.Requires(stmt != null); + Contract.Requires(localsAllowedInUpdates != null); if (stmt is PredicateStmt) { // cool } else if (stmt is PrintStmt) { @@ -6648,11 +6721,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) { @@ -6661,33 +6734,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(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); } } @@ -6697,14 +6770,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); } } @@ -6726,14 +6799,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()); } } 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); } } @@ -6742,11 +6815,14 @@ namespace Microsoft.Dafny } } - void CheckHintLhs(IToken tok, Expression lhs) { + void CheckHintLhs(IToken tok, Expression lhs, ISet 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"); } } @@ -7768,9 +7844,6 @@ namespace Microsoft.Dafny ResolveExpression(rhs, opts); ConstrainTypes(rhs.Type, Type.Bool, 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); - } } ResolveExpression(e.Body, opts); ResolveAttributes(e.Attributes, new ResolveOpts(opts, true)); @@ -7819,21 +7892,17 @@ namespace Microsoft.Dafny List 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(); // (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); - } + e.MissingBounds = missingBounds; + } + if (opts.codeContext is Function && e.Bounds != null) { + 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]; + 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); } } - if (mb.Count != 0) { - e.MissingBounds = mb; - } } } @@ -7855,12 +7924,6 @@ namespace Microsoft.Dafny 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); @@ -9329,17 +9392,47 @@ namespace Microsoft.Dafny CheckIsNonGhost(e.RHSs[0]); } CheckIsNonGhost(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 missingBounds; + var vars = new List(e.BoundVars); + var bestBounds = DiscoverBestBounds_MultipleVars(vars, constraint, true, false, out missingBounds); + if (missingBounds.Count != 0) { + e.Constraint_MissingBounds = missingBounds; + foreach (var bv in e.Constraint_MissingBounds) { + reporter.Error(MessageSource.Resolver, e, "a non-ghost let-such-that constraint must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name); + } + } else { + e.Constraint_Bounds = bestBounds; + } } 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; + CheckIsNonGhost(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) { @@ -9358,10 +9451,6 @@ namespace Microsoft.Dafny var e = (ChainingExpression)expr; e.Operands.ForEach(CheckIsNonGhost); return; - } else if (expr is LambdaExpr) { - var e = expr as LambdaExpr; - CheckIsNonGhost(e.Body); - return; } foreach (var ee in expr.SubExpressions) { @@ -9520,8 +9609,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)) { diff --git a/Test/dafny0/AssumptionVariables0.dfy.expect b/Test/dafny0/AssumptionVariables0.dfy.expect index 16572961..83eb8a73 100644 --- a/Test/dafny0/AssumptionVariables0.dfy.expect +++ b/Test/dafny0/AssumptionVariables0.dfy.expect @@ -1,13 +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 && " 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 && " -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 && " 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 && " 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 && " 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 && " 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 && " 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 && " -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 && " 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/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 61956651..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; { } @@ -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 00030994..4d25ba11 100644 --- a/Test/dafny0/ParallelResolveErrors.dfy.expect +++ b/Test/dafny0/ParallelResolveErrors.dfy.expect @@ -1,23 +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(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(44,6): Error: body of forall statement is attempting to update a variable declared outside the forall statement -ParallelResolveErrors.dfy(56,13): Error: new allocation not supported in forall statements +ParallelResolveErrors.dfy(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 +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 2fab6bf3..d3514b2b 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -102,7 +102,7 @@ class EE { } // --------------- ghost tests ------------------------------------- - +module HereAreMoreGhostTests { datatype GhostDt = Nil(ghost extraInfo: int) | Cons(data: int, tail: GhostDt, ghost moreInfo: int) @@ -154,7 +154,7 @@ class GhostTests { ensures false; { while (true) - decreases *; // error: not allowed in ghost context +//KRML-confirmed decreases *; // error: not allowed in ghost context { } } @@ -228,7 +228,7 @@ 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 +//KRML-confirmed break break break; // error: tries to break out of more loop levels than there are } q := q + 1; } @@ -238,7 +238,7 @@ class GhostTests { p := p + 1; } } -method BreakMayNotBeFineHere_Ghost(ghost t: int) + method BreakMayNotBeFineHere_Ghost(ghost t: int) { var n := 0; ghost var k := 0; @@ -297,7 +297,7 @@ method BreakMayNotBeFineHere_Ghost(ghost t: int) } } } - +} //HereAreMoreGhostTests method DuplicateLabels(n: int) { var x; if (n < 7) { @@ -364,17 +364,17 @@ method DatatypeDestructors(d: DTD_List) { } } method DatatypeDestructors_Ghost(d: DTD_List) { - var g1 := d.g; // error: cannot use ghost member in non-ghost code + var g1 := d.g; // error: cannot use ghost member in non-ghost code//KRML-confirmed } // ------------------- 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 { var data: T; } @@ -439,11 +439,11 @@ 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 + { print n + m; } // error: non-ghost statements are not allowed in hints//KRML-confirmed m + n; } } - +module MyOwnModule { class SideEffectChecks { ghost var ycalc: int; @@ -461,11 +461,11 @@ class SideEffectChecks { var x: int; calc { 0; - { Mod(0); } // methods with side-effects are not allowed + { Mod(0); } // error: methods with side-effects are not allowed ycalc; - { ycalc := 1; } // heap updates are not allowed + { ycalc := 1; } // error: heap updates are not allowed 1; - { x := 1; } // updates to locals defined outside of the hint are not allowed + { x := 1; } // error: updates to locals defined outside of the hint are not allowed x; { var x: int; @@ -475,7 +475,7 @@ class SideEffectChecks { } } } - +} // ------------------- nameless constructors ------------------------------ class YHWH { @@ -523,13 +523,13 @@ method AssignSuchThatFromGhost() var x: int; ghost var g: int; - x := g; // error: ghost cannot flow into non-ghost + x := g; // error: ghost cannot flow into non-ghost//KRML-confirmed 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 :| x == g; // error: left-side has non-ghost, so RHS must be non-ghost as well//KRML-confirmed x :| assume x == g; // this is cool, since it's an assume (but, of course, the // compiler will complain) @@ -605,7 +605,7 @@ method LetSuchThat(ghost z: int, n: nat) } method LetSuchThat_Ghost(ghost z: int, n: nat) { - var x := var y :| y < z; y; // error: contraint depend on ghost (z) + var x := var y :| y < z; y; // error: contraint depend on ghost (z)//KRML-confirmed } // ------------ quantified variables whose types are not inferred ---------- @@ -677,9 +677,9 @@ module GhostAllocationTests { 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 + { if n != 0 { GhostNew4(n-1); } } // error: cannot call non-ghost method in a ghost context//KRML-confirmed 1 + 4; - { GhostNew5(g); } // error: cannot call method with nonempty modifies + { GhostNew5(g); } // error: cannot call method with nonempty modifies//KRML-confirmed -5 + 10; } } @@ -735,7 +735,7 @@ module StatementsInExpressions { { calc { 5; - { SideEffect(); } // error: cannot call method with side effects + { SideEffect(); } // error: cannot call method with side effects//KRML 5; } } @@ -745,7 +745,7 @@ module StatementsInExpressions { calc { 6; { assert 6 < 8; } - { NonGhostMethod(); } // error: cannot call non-ghost method + { NonGhostMethod(); } // error: cannot call non-ghost method//KRML-confirmed { var x := 8; while x != 0 decreases *; // error: cannot use 'decreases *' in a ghost context @@ -759,12 +759,12 @@ module StatementsInExpressions { 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 + { MyField := 12; } // error: cannot assign to a field//KRML-confirmed + { MyGhostField := 12; } // error: cannot assign to any field//KRML-confirmed + { SideEffect(); } // error: cannot call (ghost) method with a modifies clause//KRML-confirmed { var x := 8; while x != 0 - modifies this; // error: cannot use a modifies clause on a loop + modifies this; // error: cannot use a modifies clause on a loop//KRML-confirmed { x := x - 1; } @@ -783,7 +783,7 @@ module StatementsInExpressions { calc { 6; { assert 6 < 8; } - { NonGhostMethod(); } // error: cannot call non-ghost method + { NonGhostMethod(); } // error: cannot call non-ghost method//KRML-confirmed { var x := 8; while x != 0 decreases *; // error: cannot use 'decreases *' in a ghost context @@ -791,12 +791,12 @@ module StatementsInExpressions { 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 + { MyField := 12; } // error: cannot assign to a field//KRML-confirmed + { MyGhostField := 12; } // error: cannot assign to any field//KRML-confirmed + { M(); } // error: cannot call (ghost) method with a modifies clause//KRML-confirmed { var x := 8; while x != 0 - modifies this; // error: cannot use a modifies clause on a loop + modifies this; // error: cannot use a modifies clause on a loop//KRML-confirmed { x := x - 1; } @@ -822,7 +822,7 @@ module StatementsInExpressions { { MyLemma(); MyGhostMethod(); // error: modifi2es state - OrdinaryMethod(); // error: not a ghost + OrdinaryMethod(); // error: not a ghost//KRML-confirmed OutParamMethod(); // error: has out-parameters 10 } @@ -1446,3 +1446,219 @@ module SuchThat { w } } + +// ---------------------- NEW STUFF ---------------------------------------- + +module GhostTests { + class G { } + + method GhostNew4(n: nat) + { + var g := new G; + calc { + 5; + 2 + 3; + { if n != 0 { GhostNew4(n-1); } } // error: cannot call non-ghost method in a ghost context//ADD:680 + 1 + 4; + { GhostNew5(g); } // error: cannot call method with nonempty modifies//ADD:682 + -5 + 10; + } + } + + ghost method GhostNew5(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//ADD:738 + 5; + } + } + function F(): int + { + calc { + 6; + { assert 6 < 8; } + { NonGhostMethod(); } // error: cannot call non-ghost method//ADD:748 + { 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//ADD:762 + { MyGhostField := 12; } // error: cannot assign to any field//ADD:763 + { SideEffect(); } // error: cannot call (ghost) method with a modifies clause//ADD:764 + { var x := 8; + while x != 0 + modifies this; // error: cannot use a modifies clause on a loop//ADD:767 + { + 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//ADD:786 + { var x := 8; + while x != 0 + { + x := x - 1; + } + } + { MyField := 12; } // error: cannot assign to a field, and especially not a non-ghost field//ADD:794 + { MyGhostField := 12; } // error: cannot assign to any field//ADD:795 + { M(); } // error: cannot call (ghost) method with a modifies clause//ADD:796 + { var x := 8; + while x != 0 + modifies this; // error: cannot use a modifies clause on a loop//ADD:799 + { + 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//ADD:825 + 10 + } + } +} + +module EvenMoreGhostTests { + ghost method NiceTry() + ensures false; + { + while (true) + decreases *; // error: not allowed in ghost context//ADD:157 + { + } + } + 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//ADD:231 + } + } + } + } + } + ghost method Bad() + { + var x: int; + calc { + 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; + } + } +} + +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//ADD:367 + } + method AssignSuchThatFromGhost() + { + var x: int; + ghost var g: int; + + x := g; // error: ghost cannot flow into non-ghost//ADD:526 + + 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//ADD:532 + + 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//ADD:442 + 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)//ADD:608 + } +} diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index 0286778b..ee2dd5f7 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -1,3 +1,21 @@ +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 +ResolutionErrors.dfy(119,10): Error: actual out-parameter 0 is required to be a ghost variable +ResolutionErrors.dfy(126,15): Error: ghost variables are allowed only in specification contexts +ResolutionErrors.dfy(130,23): Error: ghost variables are allowed only in specification contexts +ResolutionErrors.dfy(137,4): Error: ghost variables are allowed only in specification contexts +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(251,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure +ResolutionErrors.dfy(274,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop +ResolutionErrors.dfy(288,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop +ResolutionErrors.dfy(293,8): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression) +ResolutionErrors.dfy(375,15): Error: ghost variables are allowed only in specification contexts +ResolutionErrors.dfy(464,11): Error: calls to methods with side-effects are not allowed inside a hint +ResolutionErrors.dfy(466,14): Error: a hint is not allowed to update heap locations +ResolutionErrors.dfy(468,10): Error: a hint is not allowed to update a variable declared outside the hint ResolutionErrors.dfy(558,7): Error: RHS (of type List) not assignable to LHS (of type List) ResolutionErrors.dfy(563,7): Error: RHS (of type List) not assignable to LHS (of type List) ResolutionErrors.dfy(577,23): Error: type of case bodies do not agree (found Tree<_T1,_T0>, previous types Tree<_T0,_T1>) @@ -13,26 +31,11 @@ ResolutionErrors.dfy(652,11): Error: the body of the enclosing forall statement ResolutionErrors.dfy(652,14): Error: new allocation not allowed in ghost context ResolutionErrors.dfy(662,23): Error: 'new' is not allowed in ghost contexts ResolutionErrors.dfy(669,15): Error: 'new' is not allowed in ghost contexts -ResolutionErrors.dfy(669,15): Error: only ghost methods can be called from this context ResolutionErrors.dfy(678,17): Error: 'new' is not allowed in ghost contexts -ResolutionErrors.dfy(680,29): Error: only ghost methods can be called from this context -ResolutionErrors.dfy(682,17): Error: calls to methods with side-effects are not allowed inside a hint ResolutionErrors.dfy(700,21): Error: the type of this variable is underspecified -ResolutionErrors.dfy(738,20): Error: calls to methods with side-effects are not allowed inside a hint -ResolutionErrors.dfy(748,24): Error: only ghost methods can be called from this context ResolutionErrors.dfy(751,22): Error: 'decreases *' is not allowed on ghost loops -ResolutionErrors.dfy(762,18): Error: a hint is not allowed to update heap locations -ResolutionErrors.dfy(763,23): Error: a hint is not allowed to update heap locations -ResolutionErrors.dfy(764,20): Error: calls to methods with side-effects are not allowed inside a hint -ResolutionErrors.dfy(767,21): Error: a while statement used inside a hint is not allowed to have a modifies clause -ResolutionErrors.dfy(786,24): Error: only ghost methods can be called from this context ResolutionErrors.dfy(789,22): Error: 'decreases *' is not allowed on ghost loops -ResolutionErrors.dfy(794,18): Error: a hint is not allowed to update heap locations -ResolutionErrors.dfy(795,23): Error: a hint is not allowed to update heap locations -ResolutionErrors.dfy(796,11): Error: calls to methods with side-effects are not allowed inside a hint -ResolutionErrors.dfy(799,21): Error: a while statement used inside a hint is not allowed to have a modifies clause ResolutionErrors.dfy(824,19): Error: calls to methods with side-effects are not allowed inside a statement expression -ResolutionErrors.dfy(825,20): Error: only ghost methods can be called from this context ResolutionErrors.dfy(826,20): Error: wrong number of method result arguments (got 0, expected 1) ResolutionErrors.dfy(838,23): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method') ResolutionErrors.dfy(848,4): Error: ghost variables are allowed only in specification contexts @@ -74,8 +77,8 @@ ResolutionErrors.dfy(1146,6): Error: RHS (of type P) not assignable to LHS ResolutionErrors.dfy(1151,13): Error: arguments must have the same type (got P and P) ResolutionErrors.dfy(1152,13): Error: arguments must have the same type (got P and P) ResolutionErrors.dfy(1153,13): Error: arguments must have the same type (got P and P) -ResolutionErrors.dfy(1176,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(1178,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(1176,38): 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(1178,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(1283,26): Error: the type of this variable is underspecified ResolutionErrors.dfy(1284,31): Error: the type of this variable is underspecified ResolutionErrors.dfy(1285,29): Error: the type of this variable is underspecified @@ -106,6 +109,29 @@ ResolutionErrors.dfy(1440,11): Error: type of RHS of assign-such-that statement ResolutionErrors.dfy(1441,9): Error: type of RHS of assign-such-that statement must be boolean (got int) ResolutionErrors.dfy(1442,13): Error: type of RHS of assign-such-that statement must be boolean (got int) ResolutionErrors.dfy(1445,15): Error: type of RHS of let-such-that expression must be boolean (got int) +ResolutionErrors.dfy(1488,20): Error: calls to methods with side-effects are not allowed inside a hint +ResolutionErrors.dfy(1510,18): Error: a hint is not allowed to update heap locations +ResolutionErrors.dfy(1511,23): Error: a hint is not allowed to update heap locations +ResolutionErrors.dfy(1512,20): Error: calls to methods with side-effects are not allowed inside a hint +ResolutionErrors.dfy(1515,21): Error: a while statement used inside a hint is not allowed to have a modifies clause +ResolutionErrors.dfy(1497,24): Error: only ghost methods can be called from this context +ResolutionErrors.dfy(1510,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(1539,18): Error: a hint is not allowed to update heap locations +ResolutionErrors.dfy(1540,23): Error: a hint is not allowed to update heap locations +ResolutionErrors.dfy(1541,11): Error: calls to methods with side-effects are not allowed inside a hint +ResolutionErrors.dfy(1544,21): Error: a while statement used inside a hint is not allowed to have a modifies clause +ResolutionErrors.dfy(1532,24): Error: only ghost methods can be called from this context +ResolutionErrors.dfy(1539,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(1568,20): Error: only ghost methods can be called from this context +ResolutionErrors.dfy(1461,29): Error: only ghost methods can be called from this context +ResolutionErrors.dfy(1463,17): Error: calls to methods with side-effects are not allowed inside a hint +ResolutionErrors.dfy(1579,16): Error: 'decreases *' is not allowed on ghost loops +ResolutionErrors.dfy(1597,12): Error: trying to break out of more loop levels than there are enclosing loops +ResolutionErrors.dfy(1623,16): Error: ghost fields are allowed only in specification contexts +ResolutionErrors.dfy(1630,9): Error: ghost variables are allowed only in specification contexts +ResolutionErrors.dfy(1636,4): Error: non-ghost variable cannot be assigned a value that depends on a ghost +ResolutionErrors.dfy(1653,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(1662,26): Error: ghost variables are allowed only in specification contexts ResolutionErrors.dfy(488,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') @@ -113,25 +139,6 @@ ResolutionErrors.dfy(92,14): Error: the name 'David' denotes a datatype construc 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 -ResolutionErrors.dfy(119,10): Error: actual out-parameter 0 is required to be a ghost variable -ResolutionErrors.dfy(126,15): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(130,23): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(137,4): Error: ghost variables are allowed only in specification contexts -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(231,12): Error: trying to break out of more loop levels than there are enclosing loops -ResolutionErrors.dfy(251,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure -ResolutionErrors.dfy(274,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop -ResolutionErrors.dfy(288,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop -ResolutionErrors.dfy(293,8): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression) -ResolutionErrors.dfy(464,11): Error: calls to methods with side-effects are not allowed inside a hint -ResolutionErrors.dfy(466,14): Error: a hint is not allowed to update heap locations -ResolutionErrors.dfy(468,10): Error: a hint is not allowed to update a variable declared outside the hint ResolutionErrors.dfy(494,14): Error: when allocating an object of type 'YHWH', one of its constructor methods must be called ResolutionErrors.dfy(499,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called ResolutionErrors.dfy(500,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called @@ -168,8 +175,6 @@ ResolutionErrors.dfy(345,9): Error: a constructor is allowed to be called only w ResolutionErrors.dfy(359,16): Error: arguments must have the same type (got int and DTD_List) ResolutionErrors.dfy(360,16): Error: arguments must have the same type (got DTD_List and int) ResolutionErrors.dfy(361,25): Error: arguments must have the same type (got bool and int) -ResolutionErrors.dfy(367,14): Error: ghost fields are allowed only in specification contexts -ResolutionErrors.dfy(375,15): Error: ghost variables are allowed only in specification contexts ResolutionErrors.dfy(400,5): Error: incorrect type of method in-parameter 1 (expected GenericClass, got GenericClass) ResolutionErrors.dfy(412,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList) ResolutionErrors.dfy(420,6): Error: arguments to + must be of a numeric type or a collection type (instead got bool) @@ -180,11 +185,7 @@ ResolutionErrors.dfy(429,10): Error: first argument to ==> must be of type bool ResolutionErrors.dfy(429,10): Error: second argument to ==> must be of type bool (instead got int) ResolutionErrors.dfy(434,10): Error: first argument to ==> must be of type bool (instead got int) ResolutionErrors.dfy(434,10): Error: second argument to ==> must be of type bool (instead got int) -ResolutionErrors.dfy(442,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(526,7): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(532,2): Error: non-ghost variable cannot be assigned a value that depends on a ghost ResolutionErrors.dfy(603,18): Error: unresolved identifier: w -ResolutionErrors.dfy(608,24): Error: ghost variables are allowed only in specification contexts ResolutionErrors.dfy(714,11): Error: lemmas are not allowed to have modifies clauses ResolutionErrors.dfy(976,9): Error: unresolved identifier: s ResolutionErrors.dfy(987,32): Error: RHS (of type (int,int,real)) not assignable to LHS (of type (int,real,int)) @@ -198,4 +199,4 @@ ResolutionErrors.dfy(1164,8): Error: new cannot be applied to a trait ResolutionErrors.dfy(1185,13): Error: first argument to / must be of numeric type (instead got set) ResolutionErrors.dfy(1192,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(1207,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating -200 resolution/type errors detected in ResolutionErrors.dfy +201 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 = // --------------------- -class ArrayTests { +module ArrayTests { ghost method G(a: array) 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 8206fd43..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,5): Error: non-ghost variable cannot be assigned a value that depends on a ghost -TypeTests.dfy(187,4): Error: cannot assign to non-ghost variable in a ghost context -TypeTests.dfy(188,7): Error: cannot assign to non-ghost variable in a ghost context TypeTests.dfy(21,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed 62 resolution/type errors detected in TypeTests.dfy diff --git a/Test/dafny4/set-compr.dfy.expect b/Test/dafny4/set-compr.dfy.expect index b31c6ac0..615ee2bc 100644 --- a/Test/dafny4/set-compr.dfy.expect +++ b/Test/dafny4/set-compr.dfy.expect @@ -1,3 +1,3 @@ -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' +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(51,13): 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' 2 resolution/type errors detected in set-compr.dfy -- cgit v1.2.3 From 074172a069d77888f232d44660b72e07579296ae Mon Sep 17 00:00:00 2001 From: qunyanm Date: Fri, 1 Apr 2016 14:36:56 -0700 Subject: Fix issue 148. The results for sign comparison for BigRational.CompareTo was wrong. --- Binaries/DafnyRuntime.cs | 8 ++++---- Test/dafny4/Bug148.dfy | 25 +++++++++++++++++++++++++ Test/dafny4/Bug148.dfy.expect | 17 +++++++++++++++++ 3 files changed, 46 insertions(+), 4 deletions(-) create mode 100644 Test/dafny4/Bug148.dfy create mode 100644 Test/dafny4/Bug148.dfy.expect (limited to 'Binaries/DafnyRuntime.cs') diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs index 3002d832..587d5159 100644 --- a/Binaries/DafnyRuntime.cs +++ b/Binaries/DafnyRuntime.cs @@ -1253,13 +1253,13 @@ namespace Dafny int asign = this.num.Sign; int bsign = that.num.Sign; if (asign < 0 && 0 <= bsign) { - return 1; + return -1; } else if (asign <= 0 && 0 < bsign) { - return 1; - } else if (bsign < 0 && 0 <= asign) { return -1; + } else if (bsign < 0 && 0 <= asign) { + return 1; } else if (bsign <= 0 && 0 < asign) { - return -1; + return 1; } BigInteger aa, bb, dd; Normalize(this, that, out aa, out bb, out dd); diff --git a/Test/dafny4/Bug148.dfy b/Test/dafny4/Bug148.dfy new file mode 100644 index 00000000..b7a08952 --- /dev/null +++ b/Test/dafny4/Bug148.dfy @@ -0,0 +1,25 @@ +// RUN: %dafny /compile:3 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +method Main() +{ + var zero : real := 0.0; + var three : real := 3.0; + var fifteen : real := 15.0; + var negone : real := -1.0; + var negthree : real := -3.0; + + print zero <= fifteen, "\n"; // true + print fifteen <= zero, "\n"; // false + print negone <= zero, "\n"; // true + print zero <= negone, "\n"; // false + print negone <= fifteen, "\n"; // true + print fifteen <= negone, "\n"; // false + + print zero >= fifteen, "\n"; // false + print fifteen >= zero, "\n"; // true + print negone >= zero, "\n"; // false + print zero >= negone, "\n"; // true + print negone >= fifteen, "\n"; // false + print fifteen >= negone, "\n"; // true +} diff --git a/Test/dafny4/Bug148.dfy.expect b/Test/dafny4/Bug148.dfy.expect new file mode 100644 index 00000000..7acfb169 --- /dev/null +++ b/Test/dafny4/Bug148.dfy.expect @@ -0,0 +1,17 @@ + +Dafny program verifier finished with 2 verified, 0 errors +Program compiled successfully +Running... + +True +False +True +False +True +False +False +True +False +True +False +True -- cgit v1.2.3