From 191ff327c49796e8a64fae893520d878b32d3268 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Sun, 7 Jun 2015 12:38:31 -0700 Subject: Fix the UseBaseNameForFileName flag; it shouldn't set the return code to zero. The test suite relies on error codes all being zero (except for preprocessing errors), so add a flag for that (as suggested in a source comment). --- Source/Dafny/DafnyOptions.cs | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) (limited to 'Source/Dafny/DafnyOptions.cs') diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 4fc2de96..a6827d5f 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -54,6 +54,7 @@ namespace Microsoft.Dafny public string AutoReqPrintFile = null; public bool ignoreAutoReq = false; public bool AllowGlobals = false; + public bool CountVerificationErrors = true; protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) { var args = ps.args; // convenient synonym @@ -171,6 +172,14 @@ namespace Microsoft.Dafny AllowGlobals = true; return true; + case "countVerificationErrors": { + int countErrors = 1; // defaults to reporting verification errors + if (ps.GetNumericArgument(ref countErrors, 2)) { + CountVerificationErrors = countErrors == 1; + } + return true; + } + default: break; } @@ -245,7 +254,7 @@ namespace Microsoft.Dafny how discriminating they are: 0 < 1 < 2 < (3,4) < 5 < 6 6 (default) - most discriminating /noIncludes Ignore include directives - /noNLarith Reduce Z3's knowledge of non-linear arithmetic (*,/,%). + /noNLarith Reduce Z3's knowledge of non-linear arithmetic (*,/,%). Results in more manual work, but also produces more predictable behavior. /autoReqPrint: Print out requirements that were automatically generated by autoReq. @@ -256,6 +265,11 @@ namespace Microsoft.Dafny a transition from the behavior in the language prior to version 1.9.3, from which point onward all functions and methods declared at the module scope are implicitly static and fields declarations are not allowed at the module scope. + /countVerificationErrors: + 0 - If preprocessing succeeds, set exit code to 0 regardless of the number + of verification errors. + 1 (default) - If preprocessing succeeds, set exit code to the number of + verification errors. "); base.Usage(); // also print the Boogie options } -- cgit v1.2.3 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 +++++++++++++++++++++++++++++++---- Source/Dafny/DafnyOptions.cs | 12 + Source/DafnyDriver/DafnyDriver.cs | 13 +- Test/irondafny0/optimize0.dfy | 6 + Test/irondafny0/optimize0.dfy.expect | 6 + 5 files changed, 485 insertions(+), 58 deletions(-) create mode 100644 Test/irondafny0/optimize0.dfy create mode 100644 Test/irondafny0/optimize0.dfy.expect (limited to 'Source/Dafny/DafnyOptions.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; diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index a6827d5f..125ab11e 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -55,6 +55,7 @@ namespace Microsoft.Dafny public bool ignoreAutoReq = false; public bool AllowGlobals = false; public bool CountVerificationErrors = true; + public bool Optimize = false; protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) { var args = ps.args; // convenient synonym @@ -180,6 +181,11 @@ namespace Microsoft.Dafny return true; } + case "optimize": { + Optimize = true; + return true; + } + default: break; } @@ -270,6 +276,12 @@ namespace Microsoft.Dafny of verification errors. 1 (default) - If preprocessing succeeds, set exit code to the number of verification errors. + /optimize Produce optimized C# code, meaning: + - selects optimized C# prelude by passing + /define:DAFNY_USE_SYSTEM_COLLECTIONS_IMMUTABLE to csc.exe (requires + System.Collections.Immutable.dll in the source directory to successfully + compile). + - passes /optimize flag to csc.exe. "); base.Usage(); // also print the Boogie options } diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index a769b829..cf464754 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -15,6 +15,8 @@ namespace Microsoft.Dafny using System.Collections.Generic; using System.Diagnostics.Contracts; using System.IO; + using System.Reflection; + using Microsoft.Boogie; using Bpl = Microsoft.Boogie; @@ -330,7 +332,7 @@ namespace Microsoft.Dafny } else { - var provider = CodeDomProvider.CreateProvider("CSharp"); + var provider = CodeDomProvider.CreateProvider("CSharp", new Dictionary { { "CompilerVersion", "v4.0" } }); var cp = new System.CodeDom.Compiler.CompilerParameters(); cp.GenerateExecutable = hasMain; if (DafnyOptions.O.RunAfterCompile) { @@ -344,6 +346,15 @@ namespace Microsoft.Dafny } cp.CompilerOptions = "/debug /nowarn:0164 /nowarn:0219"; // warning CS0164 complains about unreferenced labels, CS0219 is about unused variables cp.ReferencedAssemblies.Add("System.Numerics.dll"); + cp.ReferencedAssemblies.Add("System.Core.dll"); + cp.ReferencedAssemblies.Add("System.dll"); + + if (DafnyOptions.O.Optimize) { + var libPath = Path.GetDirectoryName(dafnyProgramName); + cp.CompilerOptions += string.Format(" /optimize /define:DAFNY_USE_SYSTEM_COLLECTIONS_IMMUTABLE /lib:{0}", libPath); + cp.ReferencedAssemblies.Add("System.Collections.Immutable.dll"); + cp.ReferencedAssemblies.Add("System.Runtime.dll"); + } var cr = provider.CompileAssemblyFromSource(cp, csharpProgram); var assemblyName = Path.GetFileName(cr.PathToAssembly); diff --git a/Test/irondafny0/optimize0.dfy b/Test/irondafny0/optimize0.dfy new file mode 100644 index 00000000..865d8707 --- /dev/null +++ b/Test/irondafny0/optimize0.dfy @@ -0,0 +1,6 @@ +// RUN: %dafny /compile:3 /optimize /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +method Main() { + print "o hai!"; +} diff --git a/Test/irondafny0/optimize0.dfy.expect b/Test/irondafny0/optimize0.dfy.expect new file mode 100644 index 00000000..6b3e13c5 --- /dev/null +++ b/Test/irondafny0/optimize0.dfy.expect @@ -0,0 +1,6 @@ + +Dafny program verifier finished with 2 verified, 0 errors +Program compiled successfully +Running... + +o hai! \ No newline at end of file -- cgit v1.2.3 From f057d2ec10bdf93bb8ef73cbb3ea80d56159faeb Mon Sep 17 00:00:00 2001 From: Bryan Parno Date: Wed, 1 Jul 2015 11:53:59 -0700 Subject: Add code to calculate various interesting statistics about Dafny files. --- Source/Dafny/DafnyOptions.cs | 14 +++- Source/Dafny/SccGraph.cs | 10 ++- Source/Dafny/Util.cs | 149 +++++++++++++++++++++++++++++++++++++- Source/DafnyDriver/DafnyDriver.cs | 7 ++ 4 files changed, 175 insertions(+), 5 deletions(-) (limited to 'Source/Dafny/DafnyOptions.cs') diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 125ab11e..af940439 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -56,6 +56,8 @@ namespace Microsoft.Dafny public bool AllowGlobals = false; public bool CountVerificationErrors = true; public bool Optimize = false; + public bool PrintStats = false; + public bool PrintFunctionCallGraph = false; protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) { var args = ps.args; // convenient synonym @@ -172,6 +174,14 @@ namespace Microsoft.Dafny case "allowGlobals": AllowGlobals = true; return true; + + case "stats": + PrintStats = true; + return true; + + case "funcCallGraph": + PrintFunctionCallGraph = true; + return true; case "countVerificationErrors": { int countErrors = 1; // defaults to reporting verification errors @@ -267,7 +277,7 @@ namespace Microsoft.Dafny /noAutoReq Ignore autoReq attributes /allowGlobals Allow the implicit class '_default' to contain fields, instance functions, and instance methods. These class members are declared at the module scope, - outside of explicit classes. This command-line option is provided to simply + outside of explicit classes. This command-line option is provided to simplify a transition from the behavior in the language prior to version 1.9.3, from which point onward all functions and methods declared at the module scope are implicitly static and fields declarations are not allowed at the module scope. @@ -282,6 +292,8 @@ namespace Microsoft.Dafny System.Collections.Immutable.dll in the source directory to successfully compile). - passes /optimize flag to csc.exe. + /stats Print interesting statistics about the Dafny files supplied. + /funcCallGraph Print out the function call graph. Format is: func,mod=callee* "); base.Usage(); // also print the Boogie options } diff --git a/Source/Dafny/SccGraph.cs b/Source/Dafny/SccGraph.cs index 01a72fc5..20b4f65e 100644 --- a/Source/Dafny/SccGraph.cs +++ b/Source/Dafny/SccGraph.cs @@ -6,8 +6,8 @@ namespace Microsoft.Dafny { public class Graph where Node : class { - enum VisitedStatus { Unvisited, OnStack, Visited } - class Vertex { + public enum VisitedStatus { Unvisited, OnStack, Visited } + public class Vertex { public readonly Node N; public readonly List/*!*/ Successors = new List(); public List SccMembers; // non-null only for the representative of the SCC @@ -65,6 +65,10 @@ namespace Microsoft.Dafny { { } + public IEnumerable GetVertices() { + return vertices.Values; + } + /// /// Idempotently adds a vertex 'n' to the graph. /// @@ -97,7 +101,7 @@ namespace Microsoft.Dafny { /// /// Returns the vertex for 'n' if 'n' is in the graph. Otherwise, returns null. /// - Vertex FindVertex(Node n) { + public Vertex FindVertex(Node n) { Vertex v; if (vertices.TryGetValue(n, out v)) { Contract.Assert(v != null); // follows from postcondition of TryGetValue (since 'vertices' maps to the type Vertex!) diff --git a/Source/Dafny/Util.cs b/Source/Dafny/Util.cs index f9421659..63659696 100644 --- a/Source/Dafny/Util.cs +++ b/Source/Dafny/Util.cs @@ -8,7 +8,7 @@ using Microsoft.Boogie; namespace Microsoft.Dafny { - class Util + public class Util { public static string Comma(IEnumerable l, Func f) { return Comma(",", l, f); @@ -175,5 +175,152 @@ namespace Microsoft.Dafny { } } + /// + /// Class dedicated to traversing the function call graph + /// + class FunctionCallFinder : TopDownVisitor> { + protected override bool VisitOneExpr(Expression expr, ref List calls) { + if (expr is FunctionCallExpr) { + calls.Add(((FunctionCallExpr)expr).Function); + } + return true; + } + } + + static Graph BuildFunctionCallGraph(Dafny.Program program) { + Graph functionCallGraph = new Graph(); + FunctionCallFinder callFinder = new FunctionCallFinder(); + + foreach (var module in program.Modules) { + foreach (var decl in module.TopLevelDecls) { + if (decl is ClassDecl) { + var c = (ClassDecl)decl; + foreach (var member in c.Members) { + if (member is Function) { + var f = (Function)member; + + List calls = new List(); + foreach (var e in f.Reads) { if (e != null && e.E != null) { callFinder.Visit(e.E, calls); } } + foreach (var e in f.Req) { if (e != null) { callFinder.Visit(e, calls); } } + foreach (var e in f.Ens) { if (e != null) { callFinder.Visit(e, calls); } } + if (f.Body != null) { + callFinder.Visit(f.Body, calls); + } + + foreach (var callee in calls) { + functionCallGraph.AddEdge(f, callee); + } + } + } + } + } + } + + return functionCallGraph; + } + + /// + /// Prints the program's function call graph in a format suitable for consumption in other tools + /// + public static void PrintFunctionCallGraph(Dafny.Program program) { + var functionCallGraph = BuildFunctionCallGraph(program); + + foreach (var vertex in functionCallGraph.GetVertices()) { + var func = vertex.N; + Console.Write("{0},{1}=", func.CompileName, func.EnclosingClass.Module.CompileName); + foreach (var callee in vertex.Successors) { + Console.Write("{0} ", callee.N.CompileName); + } + Console.Write("\n"); + } + } + + /// + /// Generic statistic counter + /// + static void IncrementStat(IDictionary stats, string stat) { + ulong currentValue; + if (stats.TryGetValue(stat, out currentValue)) { + stats[stat] += 1; + } else { + stats.Add(stat, 1); + } + } + + /// + /// Track the maximum value of some statistic + /// + static void UpdateMax(IDictionary stats, string stat, ulong val) { + ulong currentValue; + if (stats.TryGetValue(stat, out currentValue)) { + if (val > currentValue) { + stats[stat] = val; + } + } else { + stats.Add(stat, val); + } + } + + /// + /// Compute various interesting statistics about the Dafny program + /// + public static void PrintStats(Dafny.Program program) { + SortedDictionary stats = new SortedDictionary(); + + foreach (var module in program.Modules) { + IncrementStat(stats, "Modules"); + UpdateMax(stats, "Module height (max)", (ulong)module.Height); + + ulong num_scc = (ulong)module.CallGraph.TopologicallySortedComponents().Count; + UpdateMax(stats, "Call graph width (max)", num_scc); + + foreach (var decl in module.TopLevelDecls) { + if (decl is DatatypeDecl) { + IncrementStat(stats, "Datatypes"); + } else if (decl is ClassDecl) { + var c = (ClassDecl)decl; + if (c.Name != "_default") { + IncrementStat(stats, "Classes"); + } + + foreach (var member in c.Members) { + if (member is Function) { + IncrementStat(stats, "Functions (total)"); + var f = (Function)member; + if (f.IsRecursive) { + IncrementStat(stats, "Functions recursive"); + } + } else if (member is Method) { + IncrementStat(stats, "Methods (total)"); + var method = (Method)member; + if (method.IsRecursive) { + IncrementStat(stats, "Methods recursive"); + } + if (method.IsGhost) { + IncrementStat(stats, "Methods ghost"); + } + } + } + } + } + } + + // Print out the results, with some nice formatting + Console.WriteLine(""); + Console.WriteLine("Statistics"); + Console.WriteLine("----------"); + + int max_key_length = 0; + foreach (var key in stats.Keys) { + if (key.Length > max_key_length) { + max_key_length = key.Length; + } + } + + foreach (var keypair in stats) { + string keyString = keypair.Key.PadRight(max_key_length + 2); + Console.WriteLine("{0} {1,4}", keyString, keypair.Value); + } + } } } diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index ce4d726f..9fdc9320 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -199,6 +199,13 @@ namespace Microsoft.Dafny } exitValue = allOk ? ExitValue.VERIFIED : ExitValue.NOT_VERIFIED; } + + if (err == null && dafnyProgram != null && DafnyOptions.O.PrintStats) { + Util.PrintStats(dafnyProgram); + } + if (err == null && dafnyProgram != null && DafnyOptions.O.PrintFunctionCallGraph) { + Util.PrintFunctionCallGraph(dafnyProgram); + } } return exitValue; } -- cgit v1.2.3 From 4d11b8d19bab3c4b37914f12226e19ac6d68ffb1 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Thu, 2 Jul 2015 20:00:11 -0700 Subject: Added command-line option /warnShadowing, which emits warnings if variables shadow other variables (Issue #86) --- Source/Dafny/DafnyOptions.cs | 7 +++ Source/Dafny/Resolver.cs | 109 ++++++++++++++++++++++++----------------- Test/dafny0/Shadows.dfy | 42 ++++++++++++++++ Test/dafny0/Shadows.dfy.expect | 12 +++++ 4 files changed, 124 insertions(+), 46 deletions(-) create mode 100644 Test/dafny0/Shadows.dfy create mode 100644 Test/dafny0/Shadows.dfy.expect (limited to 'Source/Dafny/DafnyOptions.cs') diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index af940439..a3b26f2a 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -58,6 +58,7 @@ namespace Microsoft.Dafny public bool Optimize = false; public bool PrintStats = false; public bool PrintFunctionCallGraph = false; + public bool WarnShadowing = false; protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) { var args = ps.args; // convenient synonym @@ -183,6 +184,10 @@ namespace Microsoft.Dafny PrintFunctionCallGraph = true; return true; + case "warnShadowing": + WarnShadowing = true; + return true; + case "countVerificationErrors": { int countErrors = 1; // defaults to reporting verification errors if (ps.GetNumericArgument(ref countErrors, 2)) { @@ -294,6 +299,8 @@ namespace Microsoft.Dafny - passes /optimize flag to csc.exe. /stats Print interesting statistics about the Dafny files supplied. /funcCallGraph Print out the function call graph. Format is: func,mod=callee* + /warnShadowing Emits a warning if the name of a declared variable caused another variable + to be shadowed "); base.Usage(); // also print the Boogie options } diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 7c78c1e2..91570a1e 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1374,7 +1374,7 @@ namespace Microsoft.Dafny Contract.Assert(dd.Constraint != null); // follows from NewtypeDecl invariant scope.PushMarker(); var added = scope.Push(dd.Var.Name, dd.Var); - Contract.Assert(added); + Contract.Assert(added == Scope.PushResult.Success); ResolveType(dd.Var.tok, dd.Var.Type, dd, ResolveTypeOptionEnum.DontInfer, null); ResolveExpression(dd.Constraint, new ResolveOpts(dd, false, true)); Contract.Assert(dd.Constraint.Type != null); // follows from postcondition of ResolveExpression @@ -3533,12 +3533,43 @@ namespace Microsoft.Dafny tp.Parent = parent; tp.PositionalIndex = index; } - if (!allTypeParameters.Push(tp.Name, tp) && emitErrors) { - Error(tp, "Duplicate type-parameter name: {0}", tp.Name); + var r = allTypeParameters.Push(tp.Name, tp); + if (emitErrors) { + if (r == Scope.PushResult.Duplicate) { + Error(tp, "Duplicate type-parameter name: {0}", tp.Name); + } else if (r == Scope.PushResult.Shadow) { + Warning(tp.tok, "Shadowed type-parameter name: {0}", tp.Name); + } } } } + void ScopePushAndReport(Scope scope, IVariable v, string kind) { + Contract.Requires(scope != null); + Contract.Requires(v != null); + Contract.Requires(kind != null); + ScopePushAndReport(scope, v.Name, v, v.Tok, kind); + } + + void ScopePushAndReport(Scope scope, string name, Thing thing, IToken tok, string kind) where Thing : class { + Contract.Requires(scope != null); + Contract.Requires(name != null); + Contract.Requires(thing != null); + Contract.Requires(tok != null); + Contract.Requires(kind != null); + var r = scope.Push(name, thing); + switch (r) { + case Scope.PushResult.Success: + break; + case Scope.PushResult.Duplicate: + Error(tok, "Duplicate {0} name: {1}", kind, name); + break; + case Scope.PushResult.Shadow: + Warning(tok, "Shadowed {0} name: {1}", kind, name); + break; + } + } + /// /// Assumes type parameters have already been pushed /// @@ -3550,9 +3581,7 @@ namespace Microsoft.Dafny } var option = f.TypeArgs.Count == 0 ? new ResolveTypeOption(f) : new ResolveTypeOption(ResolveTypeOptionEnum.AllowPrefix); foreach (Formal p in f.Formals) { - if (!scope.Push(p.Name, p)) { - Error(p, "Duplicate parameter name: {0}", p.Name); - } + ScopePushAndReport(scope, p, "parameter"); ResolveType(p.tok, p.Type, f, option, f.TypeArgs); } ResolveType(f.tok, f.ResultType, f, option, f.TypeArgs); @@ -3660,16 +3689,12 @@ namespace Microsoft.Dafny var option = m.TypeArgs.Count == 0 ? new ResolveTypeOption(m) : new ResolveTypeOption(ResolveTypeOptionEnum.AllowPrefix); // resolve in-parameters foreach (Formal p in m.Ins) { - if (!scope.Push(p.Name, p)) { - Error(p, "Duplicate parameter name: {0}", p.Name); - } + ScopePushAndReport(scope, p, "parameter"); ResolveType(p.tok, p.Type, m, option, m.TypeArgs); } // resolve out-parameters foreach (Formal p in m.Outs) { - if (!scope.Push(p.Name, p)) { - Error(p, "Duplicate parameter name: {0}", p.Name); - } + ScopePushAndReport(scope, p, "parameter"); ResolveType(p.tok, p.Type, m, option, m.TypeArgs); } scope.PopMarker(); @@ -4828,9 +4853,7 @@ namespace Microsoft.Dafny } // Add the locals to the scope foreach (var local in s.Locals) { - if (!scope.Push(local.Name, local)) { - Error(local.Tok, "Duplicate local-variable name: {0}", local.Name); - } + ScopePushAndReport(scope, local, "local-variable"); } // With the new locals in scope, it's now time to resolve the attributes on all the locals foreach (var local in s.Locals) { @@ -5121,9 +5144,7 @@ namespace Microsoft.Dafny int prevErrorCount = ErrorCount; scope.PushMarker(); foreach (BoundVar v in s.BoundVars) { - if (!scope.Push(v.Name, v)) { - Error(v, "Duplicate bound-variable name: {0}", v.Name); - } + ScopePushAndReport(scope, v, "local-variable"); ResolveType(v.tok, v.Type, codeContext, ResolveTypeOptionEnum.InferTypeProxies, null); } ResolveExpression(s.Range, new ResolveOpts(codeContext, true, specContextOnly)); @@ -5586,9 +5607,7 @@ namespace Microsoft.Dafny if (pat.Var != null) { BoundVar v = pat.Var; if (topLevel) { - if (!scope.Push(v.Name, v)) { - Error(v, "Duplicate parameter name: {0}", v.Name); - } + ScopePushAndReport(scope, v, "parameter"); } else { if (scope.Find(v.Name) != null) { Error(v, "Duplicate parameter name: {0}", v.Name); @@ -6202,8 +6221,8 @@ namespace Microsoft.Dafny } else if (prev != null) { Error(lnode.Tok, "label shadows an enclosing label"); } else { - bool b = labeledStatements.Push(lnode.Name, ss); - Contract.Assert(b); // since we just checked for duplicates, we expect the Push to succeed + var r = labeledStatements.Push(lnode.Name, ss); + Contract.Assert(r == Scope.PushResult.Success); // since we just checked for duplicates, we expect the Push to succeed if (l == ss.Labels) { // add it only once inSpecOnlyContext.Add(ss, specContextOnly); } @@ -7541,9 +7560,7 @@ namespace Microsoft.Dafny // Check for duplicate names now, because not until after resolving the case pattern do we know if identifiers inside it refer to bound variables or nullary constructors var c = 0; foreach (var v in lhs.Vars) { - if (!scope.Push(v.Name, v)) { - Error(v, "Duplicate let-variable name: {0}", v.Name); - } + ScopePushAndReport(scope, v, "let-variable"); c++; } if (c == 0) { @@ -7562,9 +7579,7 @@ namespace Microsoft.Dafny foreach (var lhs in e.LHSs) { Contract.Assert(lhs.Var != null); // the parser already checked that every LHS is a BoundVar, not a general pattern var v = lhs.Var; - if (!scope.Push(v.Name, v)) { - Error(v, "Duplicate let-variable name: {0}", v.Name); - } + ScopePushAndReport(scope, v, "let-variable"); ResolveType(v.tok, v.Type, opts.codeContext, ResolveTypeOptionEnum.InferTypeProxies, null); } foreach (var rhs in e.RHSs) { @@ -7596,9 +7611,7 @@ namespace Microsoft.Dafny ResolveTypeParameters(e.TypeArgs, true, e); scope.PushMarker(); foreach (BoundVar v in e.BoundVars) { - if (!scope.Push(v.Name, v)) { - Error(v, "Duplicate bound-variable name: {0}", v.Name); - } + ScopePushAndReport(scope, v, "bound-variable"); var option = typeQuantifier ? new ResolveTypeOption(e) : new ResolveTypeOption(ResolveTypeOptionEnum.InferTypeProxies); ResolveType(v.tok, v.Type, opts.codeContext, option, typeQuantifier ? e.TypeArgs : null); } @@ -7652,9 +7665,7 @@ namespace Microsoft.Dafny int prevErrorCount = ErrorCount; scope.PushMarker(); foreach (BoundVar v in e.BoundVars) { - if (!scope.Push(v.Name, v)) { - Error(v, "Duplicate bound-variable name: {0}", v.Name); - } + ScopePushAndReport(scope, v, "bound-variable"); ResolveType(v.tok, v.Type, opts.codeContext, ResolveTypeOptionEnum.InferTypeProxies, null); } ResolveExpression(e.Range, opts); @@ -7683,9 +7694,7 @@ namespace Microsoft.Dafny Error(e.tok, "a map comprehension must have exactly one bound variable."); } foreach (BoundVar v in e.BoundVars) { - if (!scope.Push(v.Name, v)) { - Error(v, "Duplicate bound-variable name: {0}", v.Name); - } + ScopePushAndReport(scope, v, "bound-variable"); ResolveType(v.tok, v.Type, opts.codeContext, ResolveTypeOptionEnum.InferTypeProxies, null); } ResolveExpression(e.Range, opts); @@ -7718,9 +7727,7 @@ namespace Microsoft.Dafny int prevErrorCount = ErrorCount; scope.PushMarker(); foreach (BoundVar v in e.BoundVars) { - if (!scope.Push(v.Name, v)) { - Error(v, "Duplicate bound-variable name: {0}", v.Name); - } + ScopePushAndReport(scope, v, "bound-variable"); ResolveType(v.tok, v.Type, opts.codeContext, ResolveTypeOptionEnum.InferTypeProxies, null); } @@ -10439,17 +10446,27 @@ namespace Microsoft.Dafny } } - // Pushes name-->thing association and returns "true", if name has not already been pushed since the last marker. - // If name already has been pushed since the last marker, does nothing and returns "false". - public bool Push(string name, Thing thing) { + public enum PushResult { Duplicate, Shadow, Success } + + /// + /// Pushes name-->thing association and returns "Success", if name has not already been pushed since the last marker. + /// If name already has been pushed since the last marker, does nothing and returns "Duplicate". + /// If the appropriate command-line option is supplied, then this method will also check if "name" shadows a previous + /// name; if it does, then it will return "Shadow" instead of "Success". + /// + public PushResult Push(string name, Thing thing) { Contract.Requires(name != null); Contract.Requires(thing != null); if (Find(name, true) != null) { - return false; + return PushResult.Duplicate; } else { + var r = PushResult.Success; + if (DafnyOptions.O.WarnShadowing && Find(name, false) != null) { + r = PushResult.Shadow; + } names.Add(name); things.Add(thing); - return true; + return r; } } diff --git a/Test/dafny0/Shadows.dfy b/Test/dafny0/Shadows.dfy new file mode 100644 index 00000000..da1e74d6 --- /dev/null +++ b/Test/dafny0/Shadows.dfy @@ -0,0 +1,42 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /warnShadowing "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +module Module0 { + class C { + method M(x: beta) // error: duplicate type parameter + method P(x: alpha) // shadowed type parameter + function F(x: beta): int // error: duplicate type parameter + function G(x: alpha): int // shadowed type parameter + + method Q0(x: int) returns (x: int) // error: duplicate variable name + } +} +module Module1 { + class D { + method Q1(x: int) returns (y: int) + { + var x; // shadowed + var y; // error: duplicate + } + + var f: int + method R() + { + var f; // okay + var f; // error: duplicate + } + method S() + { + var x; + { + var x; // shadow + } + } + method T() + { + var x; + ghost var b := forall x :: x < 10; // shadow + ghost var c := forall y :: forall y :: y != y + 1; // shadow + } + } +} diff --git a/Test/dafny0/Shadows.dfy.expect b/Test/dafny0/Shadows.dfy.expect new file mode 100644 index 00000000..5083ac64 --- /dev/null +++ b/Test/dafny0/Shadows.dfy.expect @@ -0,0 +1,12 @@ +Shadows.dfy(6,19): Error: Duplicate type-parameter name: beta +Shadows.dfy(7,13): Warning: Shadowed type-parameter name: alpha +Shadows.dfy(8,21): Error: Duplicate type-parameter name: beta +Shadows.dfy(9,15): Warning: Shadowed type-parameter name: alpha +Shadows.dfy(11,31): Error: Duplicate parameter name: x +Shadows.dfy(18,10): Warning: Shadowed local-variable name: x +Shadows.dfy(19,10): Error: Duplicate local-variable name: y +Shadows.dfy(26,10): Error: Duplicate local-variable name: f +Shadows.dfy(32,12): Warning: Shadowed local-variable name: x +Shadows.dfy(38,28): Warning: Shadowed bound-variable name: x +Shadows.dfy(39,40): Warning: Shadowed bound-variable name: y +5 resolution/type errors detected in Shadows.dfy -- cgit v1.2.3 From fe501d243c0413db8ae85bda174d0761da00d330 Mon Sep 17 00:00:00 2001 From: Michael Lowell Roberts Date: Mon, 13 Jul 2015 10:40:35 -0700 Subject: [IronDafny] implemented workaround for "import opened" bug(s). --- Source/Dafny/Cloner.cs | 8 ++-- Source/Dafny/Dafny.atg | 16 ++++---- Source/Dafny/DafnyAst.cs | 52 +++++++++++++++++++----- Source/Dafny/DafnyOptions.cs | 27 +++++++++++- Source/Dafny/Parser.cs | 16 ++++---- Source/Dafny/Resolver.cs | 61 ++++++++++++++++++++-------- Test/irondafny0/FIFO.dfy | 2 +- Test/irondafny0/LIFO.dfy | 2 +- Test/irondafny0/opened_workaround.dfy | 21 ++++++++++ Test/irondafny0/opened_workaround.dfy.expect | 3 ++ Test/irondafny0/xrefine0.dfy | 2 +- Test/irondafny0/xrefine1.dfy | 2 +- Test/irondafny0/xrefine2.dfy | 2 +- Test/irondafny0/xrefine3.dfy | 2 +- 14 files changed, 161 insertions(+), 55 deletions(-) create mode 100644 Test/irondafny0/opened_workaround.dfy create mode 100644 Test/irondafny0/opened_workaround.dfy.expect (limited to 'Source/Dafny/DafnyOptions.cs') diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index 6e64c7ec..fe9795d3 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -44,9 +44,9 @@ namespace Microsoft.Dafny } else if (d is NewtypeDecl) { var dd = (NewtypeDecl)d; if (dd.Var == null) { - return new NewtypeDecl(Tok(dd.tok), dd.Name, m, CloneType(dd.BaseType), CloneAttributes(dd.Attributes)); + return new NewtypeDecl(Tok(dd.tok), dd.Name, m, CloneType(dd.BaseType), CloneAttributes(dd.Attributes), dd); } else { - return new NewtypeDecl(Tok(dd.tok), dd.Name, m, CloneBoundVar(dd.Var), CloneExpr(dd.Constraint), CloneAttributes(dd.Attributes)); + return new NewtypeDecl(Tok(dd.tok), dd.Name, m, CloneBoundVar(dd.Var), CloneExpr(dd.Constraint), CloneAttributes(dd.Attributes), dd); } } else if (d is TupleTypeDecl) { var dd = (TupleTypeDecl)d; @@ -55,7 +55,7 @@ namespace Microsoft.Dafny var dd = (IndDatatypeDecl)d; var tps = dd.TypeArgs.ConvertAll(CloneTypeParam); var ctors = dd.Ctors.ConvertAll(CloneCtor); - var dt = new IndDatatypeDecl(Tok(dd.tok), dd.Name, m, tps, ctors, CloneAttributes(dd.Attributes)); + var dt = new IndDatatypeDecl(Tok(dd.tok), dd.Name, m, tps, ctors, CloneAttributes(dd.Attributes), dd); return dt; } else if (d is CoDatatypeDecl) { var dd = (CoDatatypeDecl)d; @@ -108,7 +108,7 @@ namespace Microsoft.Dafny if (d is DefaultClassDecl) { return new DefaultClassDecl(m, mm); } else { - return new ClassDecl(Tok(dd.tok), dd.Name, m, tps, mm, CloneAttributes(dd.Attributes), dd.TraitsTyp.ConvertAll(CloneType)); + return new ClassDecl(Tok(dd.tok), dd.Name, m, tps, mm, CloneAttributes(dd.Attributes), dd.TraitsTyp.ConvertAll(CloneType), dd); } } else if (d is ModuleDecl) { if (d is LiteralModuleDecl) { diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 7b51fb5e..6e939968 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -515,7 +515,7 @@ Dafny | OtherTypeDecl (. defaultModule.TopLevelDecls.Add(td); .) | IteratorDecl (. defaultModule.TopLevelDecls.Add(iter); .) | TraitDecl (. defaultModule.TopLevelDecls.Add(trait); .) - | ClassMemberDecl + | ClassMemberDecl } (. // find the default class in the default module, then append membersDefaultClass to its member list DefaultClassDecl defaultClass = null; @@ -561,7 +561,7 @@ SubModuleDecl | NewtypeDecl (. module.TopLevelDecls.Add(td); .) | OtherTypeDecl (. module.TopLevelDecls.Add(td); .) | IteratorDecl (. module.TopLevelDecls.Add(iter); .) - | ClassMemberDecl + | ClassMemberDecl } "}" (. module.BodyEndTok = t; module.TopLevelDecls.Add(new DefaultClassDecl(module, namedModuleDefaultClassMembers)); @@ -618,7 +618,7 @@ ClassDecl {"," Type (. traits.Add(trait); .) } ] "{" (. bodyStart = t; .) - { ClassMemberDecl + { ClassMemberDecl } "}" (. c = new ClassDecl(id, id.val, module, typeArgs, members, attrs, traits); @@ -642,7 +642,7 @@ ClassDecl NoUSIdent [ GenericParameters ] "{" (. bodyStart = t; .) - { ClassMemberDecl + { ClassMemberDecl } "}" (. trait = new TraitDecl(id, id.val, module, typeArgs, members, attrs); @@ -651,7 +651,7 @@ ClassDecl .) . -ClassMemberDecl<.List mm, bool allowConstructors, bool moduleLevelDecl.> +ClassMemberDecl<.List mm, bool allowConstructors, bool moduleLevelDecl, bool permitAbstractDecl.> = (. Contract.Requires(cce.NonNullElements(mm)); Method/*!*/ m; Function/*!*/ f; @@ -685,7 +685,7 @@ ClassMemberDecl<.List mm, bool allowConstructors, bool moduleLevelDe mmod.IsProtected = false; } .) - MethodDecl (. mm.Add(m); .) + MethodDecl (. mm.Add(m); .) ) . DatatypeDecl @@ -937,7 +937,7 @@ GenericParameters<.List/*!*/ typeArgs.> ">" . /*------------------------------------------------------------------------*/ -MethodDecl +MethodDecl = (. Contract.Ensures(Contract.ValueAtReturn(out m) !=null); IToken/*!*/ id = Token.NoToken; bool hasName = false; IToken keywordToken; @@ -1018,7 +1018,7 @@ MethodDecl [ BlockStmt ] (. - if (DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom") && !Attributes.Contains(attrs, "imported") && !Attributes.Contains(attrs, "decl") && theVerifyThisFile) { + if (!permitAbstractDecl && DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom") && !Attributes.Contains(attrs, "imported") && !Attributes.Contains(attrs, "decl") && theVerifyThisFile) { SemErr(t, "a method with an ensures clause must have a body, unless given the :axiom attribute"); } diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index d14d82a3..c90755a3 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -1777,6 +1777,14 @@ namespace Microsoft.Dafny { this.refinementBase = null; Includes = new List(); IsBuiltinName = isBuiltinName; + + if (isExclusiveRefinement && !DafnyOptions.O.IronDafny) { + parser.errors.SynErr( + tok.filename, + tok.line, + tok.col, + "The exclusively keyword is experimental and only available when IronDafny features are enabled (/ironDafny)."); + } } public virtual bool IsDefaultModule { get { @@ -1990,8 +1998,8 @@ namespace Microsoft.Dafny { } public ClassDecl(IToken tok, string name, ModuleDefinition module, - List typeArgs, [Captured] List members, Attributes attributes, List traits) - : base(tok, name, module, typeArgs, attributes) { + List typeArgs, [Captured] List members, Attributes attributes, List traits, ClassDecl clonedFrom = null) + : base(tok, name, module, typeArgs, attributes, clonedFrom) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(module != null); @@ -2005,6 +2013,12 @@ namespace Microsoft.Dafny { return false; } } + + public new ClassDecl ClonedFrom { + get { + return (ClassDecl)base.ClonedFrom; + } + } } public class DefaultClassDecl : ClassDecl { @@ -2067,8 +2081,8 @@ namespace Microsoft.Dafny { } public DatatypeDecl(IToken tok, string name, ModuleDefinition module, List typeArgs, - [Captured] List ctors, Attributes attributes) - : base(tok, name, module, typeArgs, attributes) { + [Captured] List ctors, Attributes attributes, DatatypeDecl clonedFrom = null) + : base(tok, name, module, typeArgs, attributes, clonedFrom) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(module != null); @@ -2082,6 +2096,12 @@ namespace Microsoft.Dafny { return (TypeArgs.Count == 0 && Ctors.TrueForAll(ctr => ctr.Formals.Count == 0)); } } + + public new DatatypeDecl ClonedFrom { + get { + return (DatatypeDecl)base.ClonedFrom; + } + } } public class IndDatatypeDecl : DatatypeDecl @@ -2094,8 +2114,8 @@ namespace Microsoft.Dafny { public ES EqualitySupport = ES.NotYetComputed; public IndDatatypeDecl(IToken tok, string name, ModuleDefinition module, List typeArgs, - [Captured] List ctors, Attributes attributes) - : base(tok, name, module, typeArgs, ctors, attributes) { + [Captured] List ctors, Attributes attributes, IndDatatypeDecl clonedFrom = null) + : base(tok, name, module, typeArgs, ctors, attributes, clonedFrom) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(module != null); @@ -2103,6 +2123,12 @@ namespace Microsoft.Dafny { Contract.Requires(cce.NonNullElements(ctors)); Contract.Requires(1 <= ctors.Count); } + + public new IndDatatypeDecl ClonedFrom { + get { + return (IndDatatypeDecl)base.ClonedFrom; + } + } } public class TupleTypeDecl : IndDatatypeDecl @@ -2578,16 +2604,16 @@ namespace Microsoft.Dafny { public readonly BoundVar Var; // can be null (if non-null, then object.ReferenceEquals(Var.Type, BaseType)) public readonly Expression Constraint; // is null iff Var is public NativeType NativeType; // non-null for fixed-size representations (otherwise, use BigIntegers for integers) - public NewtypeDecl(IToken tok, string name, ModuleDefinition module, Type baseType, Attributes attributes) - : base(tok, name, module, new List(), attributes) { + public NewtypeDecl(IToken tok, string name, ModuleDefinition module, Type baseType, Attributes attributes, NewtypeDecl clonedFrom = null) + : base(tok, name, module, new List(), attributes, clonedFrom) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(module != null); Contract.Requires(baseType != null); BaseType = baseType; } - public NewtypeDecl(IToken tok, string name, ModuleDefinition module, BoundVar bv, Expression constraint, Attributes attributes) - : base(tok, name, module, new List(), attributes) { + public NewtypeDecl(IToken tok, string name, ModuleDefinition module, BoundVar bv, Expression constraint, Attributes attributes, NewtypeDecl clonedFrom = null) + : base(tok, name, module, new List(), attributes, clonedFrom) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(module != null); @@ -2618,6 +2644,12 @@ namespace Microsoft.Dafny { get { throw new cce.UnreachableException(); } // see comment above about ICallable.Decreases set { throw new cce.UnreachableException(); } // see comment above about ICallable.Decreases } + + public new NewtypeDecl ClonedFrom { + get { + return (NewtypeDecl)base.ClonedFrom; + } + } } public class TypeSynonymDecl : TopLevelDecl, RedirectingTypeDecl diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index a3b26f2a..978525f3 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -15,7 +15,11 @@ namespace Microsoft.Dafny public override string VersionNumber { get { - return System.Diagnostics.FileVersionInfo.GetVersionInfo(System.Reflection.Assembly.GetExecutingAssembly().Location).FileVersion; + return System.Diagnostics.FileVersionInfo.GetVersionInfo(System.Reflection.Assembly.GetExecutingAssembly().Location).FileVersion +#if ENABLE_IRONDAFNY + + "[IronDafny]" +#endif + ; } } public override string VersionSuffix { @@ -59,6 +63,13 @@ namespace Microsoft.Dafny public bool PrintStats = false; public bool PrintFunctionCallGraph = false; public bool WarnShadowing = false; + public bool IronDafny = +#if ENABLE_IRONDAFNY + true +#else + false +#endif + ; protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) { var args = ps.args; // convenient synonym @@ -201,6 +212,16 @@ namespace Microsoft.Dafny return true; } + case "noIronDafny": { + IronDafny = false; + return true; + } + + case "ironDafny": { + IronDafny = true; + return true; + } + default: break; } @@ -301,6 +322,10 @@ namespace Microsoft.Dafny /funcCallGraph Print out the function call graph. Format is: func,mod=callee* /warnShadowing Emits a warning if the name of a declared variable caused another variable to be shadowed + /ironDafny Enable experimental features needed to support Ironclad/Ironfleet. Use of + these features may cause your code to become incompatible with future + releases of Dafny. + /noIronDafny Disable Ironclad/Ironfleet features, if enabled by default. "); base.Usage(); // also print the Boogie options } diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index a90e650a..0c88cc22 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -576,7 +576,7 @@ bool IsType(ref IToken pt) { break; } case 37: case 38: case 39: case 40: case 41: case 72: case 73: case 74: case 77: case 83: case 84: case 85: case 86: { - ClassMemberDecl(membersDefaultClass, false, !DafnyOptions.O.AllowGlobals); + ClassMemberDecl(membersDefaultClass, false, !DafnyOptions.O.AllowGlobals, false); break; } } @@ -672,7 +672,7 @@ bool IsType(ref IToken pt) { break; } case 37: case 38: case 39: case 40: case 41: case 72: case 73: case 74: case 77: case 83: case 84: case 85: case 86: { - ClassMemberDecl(namedModuleDefaultClassMembers, false, !DafnyOptions.O.AllowGlobals); + ClassMemberDecl(namedModuleDefaultClassMembers, false, !DafnyOptions.O.AllowGlobals, true); break; } } @@ -750,7 +750,7 @@ bool IsType(ref IToken pt) { Expect(45); bodyStart = t; while (StartOf(2)) { - ClassMemberDecl(members, true, false); + ClassMemberDecl(members, true, false, false); } Expect(46); c = new ClassDecl(id, id.val, module, typeArgs, members, attrs, traits); @@ -961,7 +961,7 @@ bool IsType(ref IToken pt) { Expect(45); bodyStart = t; while (StartOf(2)) { - ClassMemberDecl(members, true, false); + ClassMemberDecl(members, true, false, false); } Expect(46); trait = new TraitDecl(id, id.val, module, typeArgs, members, attrs); @@ -970,7 +970,7 @@ bool IsType(ref IToken pt) { } - void ClassMemberDecl(List mm, bool allowConstructors, bool moduleLevelDecl) { + void ClassMemberDecl(List mm, bool allowConstructors, bool moduleLevelDecl, bool permitAbstractDecl) { Contract.Requires(cce.NonNullElements(mm)); Method/*!*/ m; Function/*!*/ f; @@ -1015,7 +1015,7 @@ bool IsType(ref IToken pt) { mmod.IsProtected = false; } - MethodDecl(mmod, allowConstructors, out m); + MethodDecl(mmod, allowConstructors, permitAbstractDecl, out m); mm.Add(m); } else SynErr(151); } @@ -1273,7 +1273,7 @@ bool IsType(ref IToken pt) { } - void MethodDecl(MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m) { + void MethodDecl(MemberModifiers mmod, bool allowConstructor, bool permitAbstractDecl, out Method/*!*/ m) { Contract.Ensures(Contract.ValueAtReturn(out m) !=null); IToken/*!*/ id = Token.NoToken; bool hasName = false; IToken keywordToken; @@ -1393,7 +1393,7 @@ bool IsType(ref IToken pt) { if (la.kind == 45) { BlockStmt(out body, out bodyStart, out bodyEnd); } - if (DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom") && !Attributes.Contains(attrs, "imported") && !Attributes.Contains(attrs, "decl") && theVerifyThisFile) { + if (!permitAbstractDecl && DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom") && !Attributes.Contains(attrs, "imported") && !Attributes.Contains(attrs, "decl") && theVerifyThisFile) { SemErr(t, "a method with an ensures clause must have a body, unless given the :axiom attribute"); } diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 3e308e76..460859db 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -919,20 +919,27 @@ namespace Microsoft.Dafny sig.IsGhost = moduleDef.IsAbstract; List declarations = moduleDef.TopLevelDecls; - if (useImports) { - // First go through and add anything from the opened imports - foreach (var im in declarations) { - if (im is ModuleDecl && ((ModuleDecl)im).Opened) { - var s = GetSignature(((ModuleDecl)im).Signature); + // First go through and add anything from the opened imports + foreach (var im in declarations) { + if (im is ModuleDecl && ((ModuleDecl)im).Opened) { + var s = GetSignature(((ModuleDecl)im).Signature); + + if (useImports || DafnyOptions.O.IronDafny) { // classes: foreach (var kv in s.TopLevels) { - TopLevelDecl d; - if (sig.TopLevels.TryGetValue(kv.Key, out d)) { - sig.TopLevels[kv.Key] = AmbiguousTopLevelDecl.Create(moduleDef, d, kv.Value); - } else { - sig.TopLevels.Add(kv.Key, kv.Value); + // IronDafny: we need to pull the members of the opened module's _default class in so that they can be merged. + if (useImports || string.Equals(kv.Key, "_default", StringComparison.InvariantCulture)) { + TopLevelDecl d; + if (sig.TopLevels.TryGetValue(kv.Key, out d)) { + sig.TopLevels[kv.Key] = AmbiguousTopLevelDecl.Create(moduleDef, d, kv.Value); + } else { + sig.TopLevels.Add(kv.Key, kv.Value); + } } } + } + + if (useImports) { // constructors: foreach (var kv in s.Ctors) { Tuple pair; @@ -948,6 +955,9 @@ namespace Microsoft.Dafny sig.Ctors.Add(kv.Key, kv.Value); } } + } + + if (useImports || DafnyOptions.O.IronDafny) { // static members: foreach (var kv in s.StaticMembers) { MemberDecl md; @@ -957,7 +967,7 @@ namespace Microsoft.Dafny // add new sig.StaticMembers.Add(kv.Key, kv.Value); } - } + } } } } @@ -4406,8 +4416,23 @@ namespace Microsoft.Dafny return false; } var aa = (UserDefinedType)a; + var rca = aa.ResolvedClass; var bb = (UserDefinedType)b; - if (aa.ResolvedClass != null && aa.ResolvedClass == bb.ResolvedClass) { + var rcb = bb.ResolvedClass; + if (DafnyOptions.O.IronDafny) + { + while (rca != null && rca.Module.IsAbstract && rca.ClonedFrom != null) + { + // todo: should ClonedFrom be a TopLevelDecl? + // todo: should ClonedFrom be moved to TopLevelDecl? + rca = (TopLevelDecl)rca.ClonedFrom; + } + while (rcb != null && rcb.Module.IsAbstract && rcb.ClonedFrom != null) + { + rcb = (TopLevelDecl)rcb.ClonedFrom; + } + } + if (rca != null && rca == rcb) { // these are both resolved class/datatype types Contract.Assert(aa.TypeArgs.Count == bb.TypeArgs.Count); bool successSoFar = true; @@ -4416,12 +4441,12 @@ namespace Microsoft.Dafny } return successSoFar; } - else if ((bb.ResolvedClass is TraitDecl) && (aa.ResolvedClass is TraitDecl)) { - return ((TraitDecl)bb.ResolvedClass).FullCompileName == ((TraitDecl)aa.ResolvedClass).FullCompileName; - } else if ((bb.ResolvedClass is ClassDecl) && (aa.ResolvedClass is TraitDecl)) { - return ((ClassDecl)bb.ResolvedClass).TraitsObj.Any(tr => tr.FullCompileName == ((TraitDecl)aa.ResolvedClass).FullCompileName); - } else if ((aa.ResolvedClass is ClassDecl) && (bb.ResolvedClass is TraitDecl)) { - return ((ClassDecl)aa.ResolvedClass).TraitsObj.Any(tr => tr.FullCompileName == ((TraitDecl)bb.ResolvedClass).FullCompileName); + else if ((rcb is TraitDecl) && (rca is TraitDecl)) { + return ((TraitDecl)rcb).FullCompileName == ((TraitDecl)rca).FullCompileName; + } else if ((rcb is ClassDecl) && (rca is TraitDecl)) { + return ((ClassDecl)rcb).TraitsObj.Any(tr => tr.FullCompileName == ((TraitDecl)rca).FullCompileName); + } else if ((rca is ClassDecl) && (rcb is TraitDecl)) { + return ((ClassDecl)rca).TraitsObj.Any(tr => tr.FullCompileName == ((TraitDecl)rcb).FullCompileName); } else if (aa.ResolvedParam != null && aa.ResolvedParam == bb.ResolvedParam) { // type parameters if (aa.TypeArgs.Count != bb.TypeArgs.Count) { diff --git a/Test/irondafny0/FIFO.dfy b/Test/irondafny0/FIFO.dfy index 1256b55d..ded8f567 100644 --- a/Test/irondafny0/FIFO.dfy +++ b/Test/irondafny0/FIFO.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /ironDafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" include "Queue.dfyi" diff --git a/Test/irondafny0/LIFO.dfy b/Test/irondafny0/LIFO.dfy index bac08fba..8c0a08e8 100644 --- a/Test/irondafny0/LIFO.dfy +++ b/Test/irondafny0/LIFO.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /ironDafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" include "Queue.dfyi" diff --git a/Test/irondafny0/opened_workaround.dfy b/Test/irondafny0/opened_workaround.dfy new file mode 100644 index 00000000..7464c346 --- /dev/null +++ b/Test/irondafny0/opened_workaround.dfy @@ -0,0 +1,21 @@ +// RUN: %dafny /ironDafny /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +module A { + + predicate P() + + class C + { + static method{:axiom} M() + ensures P(); + } +} + +abstract module B { + import opened A +} + +abstract module C { + import Bee as B // Works +} diff --git a/Test/irondafny0/opened_workaround.dfy.expect b/Test/irondafny0/opened_workaround.dfy.expect new file mode 100644 index 00000000..0be94b4c --- /dev/null +++ b/Test/irondafny0/opened_workaround.dfy.expect @@ -0,0 +1,3 @@ + +Dafny program verifier finished with 3 verified, 0 errors +Compilation error: Function _0_A_Compile._default.P has no body diff --git a/Test/irondafny0/xrefine0.dfy b/Test/irondafny0/xrefine0.dfy index 35993ce8..b849111c 100644 --- a/Test/irondafny0/xrefine0.dfy +++ b/Test/irondafny0/xrefine0.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /ironDafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" abstract module Delicious {} diff --git a/Test/irondafny0/xrefine1.dfy b/Test/irondafny0/xrefine1.dfy index 10d25f53..4b085e6b 100644 --- a/Test/irondafny0/xrefine1.dfy +++ b/Test/irondafny0/xrefine1.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /ironDafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" abstract module ProtocolSpec { diff --git a/Test/irondafny0/xrefine2.dfy b/Test/irondafny0/xrefine2.dfy index 7578b424..1de4e201 100644 --- a/Test/irondafny0/xrefine2.dfy +++ b/Test/irondafny0/xrefine2.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /ironDafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" abstract module ProtocolSpec { diff --git a/Test/irondafny0/xrefine3.dfy b/Test/irondafny0/xrefine3.dfy index 69c5bc27..44add7cc 100644 --- a/Test/irondafny0/xrefine3.dfy +++ b/Test/irondafny0/xrefine3.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /ironDafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" abstract module AlphaSpec { -- cgit v1.2.3 From 64495ae998749da057b3a717aba6ef53a3e8006e Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Mon, 13 Jul 2015 21:04:11 +0100 Subject: Add /printTooltips and /autoTriggers to the CLI --- Source/Dafny/DafnyOptions.cs | 21 +++++++++++++++++++++ Source/Dafny/Resolver.cs | 22 ++++++++++++++++++---- 2 files changed, 39 insertions(+), 4 deletions(-) (limited to 'Source/Dafny/DafnyOptions.cs') diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 125ab11e..b2593705 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -56,6 +56,8 @@ namespace Microsoft.Dafny public bool AllowGlobals = false; public bool CountVerificationErrors = true; public bool Optimize = false; + public bool AutoTriggers = true; + public bool PrintTooltips = false; protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) { var args = ps.args; // convenient synonym @@ -181,6 +183,18 @@ namespace Microsoft.Dafny return true; } + case "printTooltips": + PrintTooltips = true; + return true; + + case "autoTriggers": { + int autoTriggers = 1; // defaults to reporting verification errors + if (ps.GetNumericArgument(ref autoTriggers, 2)) { + AutoTriggers = autoTriggers == 1; + } + return true; + } + case "optimize": { Optimize = true; return true; @@ -276,12 +290,19 @@ namespace Microsoft.Dafny of verification errors. 1 (default) - If preprocessing succeeds, set exit code to the number of verification errors. + /autoTriggers: + 0 - Do not generate {:trigger} annotations for user-level quantifiers. + 1 (default) - Add a {:trigger} to each user-level quantifier. Existing + annotations are preserved. /optimize Produce optimized C# code, meaning: - selects optimized C# prelude by passing /define:DAFNY_USE_SYSTEM_COLLECTIONS_IMMUTABLE to csc.exe (requires System.Collections.Immutable.dll in the source directory to successfully compile). - passes /optimize flag to csc.exe. + /printTooltips + Dump additional positional information (displayed as mouse-over tooltips by + the VS plugin) to stdout as 'Info' messages. "); base.Usage(); // also print the Boogie options } diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index c5535808..300d4985 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -25,7 +25,7 @@ namespace Microsoft.Dafny ConsoleColor col = Console.ForegroundColor; Console.ForegroundColor = ConsoleColor.Red; Console.WriteLine("{0}({1},{2}): Error: {3}", - DafnyOptions.Clo.UseBaseNameForFileName ? System.IO.Path.GetFileName(tok.filename) : tok.filename, tok.line, tok.col - 1, + DafnyOptions.Clo.UseBaseNameForFileName ? System.IO.Path.GetFileName(tok.filename) : tok.filename, tok.line, tok.col, string.Format(msg, args)); Console.ForegroundColor = col; ErrorCount++; @@ -254,6 +254,10 @@ namespace Microsoft.Dafny // Populate the members of the basic types var trunc = new SpecialField(Token.NoToken, "Trunc", "ToBigInteger()", "", "", false, false, false, Type.Int, null); basicTypeMembers[(int)BasicTypeVariety.Real].Add(trunc.Name, trunc); + + if (DafnyOptions.O.PrintTooltips) { + AdditionalInformationReporter = DefaultInformationReporter; + } } [ContractInvariantMethod] @@ -264,6 +268,12 @@ namespace Microsoft.Dafny Contract.Invariant(cce.NonNullDictionaryAndValues(datatypeCtors) && Contract.ForAll(datatypeCtors.Values, v => cce.NonNullDictionaryAndValues(v))); } + public void DefaultInformationReporter(AdditionalInformation info) { + Console.WriteLine("{0}({1},{2}): Info: {3}", + DafnyOptions.Clo.UseBaseNameForFileName ? System.IO.Path.GetFileName(info.Token.filename) : info.Token.filename, + info.Token.line, info.Token.col, info.Text); + } + public void ResolveProgram(Program prog) { Contract.Requires(prog != null); var origErrorCount = ErrorCount; @@ -303,6 +313,10 @@ namespace Microsoft.Dafny rewriters.Add(opaqueRewriter); rewriters.Add(new TimeLimitRewriter()); + if (DafnyOptions.O.AutoTriggers) { + rewriters.Add(new TriggersRewriter(this)); + } + systemNameInfo = RegisterTopLevelDecls(prog.BuiltIns.SystemModule, false); prog.CompileModules.Add(prog.BuiltIns.SystemModule); foreach (var decl in sortedDecls) { @@ -2048,7 +2062,7 @@ namespace Microsoft.Dafny foreach (var p in e.TypeArgumentSubstitutions) { if (!IsDetermined(p.Value.Normalize())) { Error(e.tok, "type variable '{0}' in the function call to '{1}' could not be determined{2}", p.Key.Name, e.Name, - (e.Name.Contains("reveal_") || e.Name.Contains("_FULL")) + (e.Name.Contains("reveal_") || e.Name.Contains("_FULL")) //CLEMENT should this be StartsWith and EndsWith? ? ". If you are making an opaque function, make sure that the function can be called." : "" ); @@ -8135,7 +8149,7 @@ namespace Microsoft.Dafny Contract.Requires(!expr.WasResolved()); Contract.Requires(opts != null); Contract.Ensures(Contract.Result() == null || args != null); - + if (expr.OptTypeArguments != null) { foreach (var ty in expr.OptTypeArguments) { ResolveType(expr.tok, ty, opts.codeContext, ResolveTypeOptionEnum.InferTypeProxies, null); @@ -8175,7 +8189,7 @@ namespace Microsoft.Dafny receiver = new StaticReceiverExpr(expr.tok, (ClassDecl)member.EnclosingClass, true); } else { if (!scope.AllowInstance) { - Error(expr.tok, "'this' is not allowed in a 'static' context"); + Error(expr.tok, "'this' is not allowed in a 'static' context"); //FIXME: Rephrase this // nevertheless, set "receiver" to a value so we can continue resolution } receiver = new ImplicitThisExpr(expr.tok); -- cgit v1.2.3 From a22d071b3eac50ce1fd6c759c58873ae6c584ced Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Thu, 16 Jul 2015 17:44:17 -0700 Subject: Clean up a few thing and set proper defaults before merging --- Source/Dafny/DafnyOptions.cs | 8 ++++---- Source/Dafny/TriggerGenerator.cs | 4 ++-- 2 files changed, 6 insertions(+), 6 deletions(-) (limited to 'Source/Dafny/DafnyOptions.cs') diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index b2593705..a809cbd6 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -56,7 +56,7 @@ namespace Microsoft.Dafny public bool AllowGlobals = false; public bool CountVerificationErrors = true; public bool Optimize = false; - public bool AutoTriggers = true; + public bool AutoTriggers = false; public bool PrintTooltips = false; protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) { @@ -188,7 +188,7 @@ namespace Microsoft.Dafny return true; case "autoTriggers": { - int autoTriggers = 1; // defaults to reporting verification errors + int autoTriggers = 0; if (ps.GetNumericArgument(ref autoTriggers, 2)) { AutoTriggers = autoTriggers == 1; } @@ -291,8 +291,8 @@ namespace Microsoft.Dafny 1 (default) - If preprocessing succeeds, set exit code to the number of verification errors. /autoTriggers: - 0 - Do not generate {:trigger} annotations for user-level quantifiers. - 1 (default) - Add a {:trigger} to each user-level quantifier. Existing + 0 (default) - Do not generate {:trigger} annotations for user-level quantifiers. + 1 - Add a {:trigger} to each user-level quantifier. Existing annotations are preserved. /optimize Produce optimized C# code, meaning: - selects optimized C# prelude by passing diff --git a/Source/Dafny/TriggerGenerator.cs b/Source/Dafny/TriggerGenerator.cs index d8a29d75..a777b4ae 100644 --- a/Source/Dafny/TriggerGenerator.cs +++ b/Source/Dafny/TriggerGenerator.cs @@ -25,7 +25,7 @@ using System.Diagnostics; */ namespace Microsoft.Dafny { - class TriggerCandidate { // TODO Hashing is broken (duplicates can pop up) + class TriggerCandidate { internal Expression Expr; internal ISet Variables; internal List MatchesInQuantifierBody; @@ -35,7 +35,7 @@ namespace Microsoft.Dafny { } } - class TriggerCandidateComparer : IEqualityComparer { + class TriggerCandidateComparer : IEqualityComparer { //FIXME: There is a bunch of these comparers. private static TriggerCandidateComparer singleton; internal static TriggerCandidateComparer Instance { get { return singleton == null ? (singleton = new TriggerCandidateComparer()) : singleton; } -- cgit v1.2.3 From 6eeaf689c0ae81bf9df46f975b014b2b9e465f0a Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Fri, 31 Jul 2015 16:45:02 -0700 Subject: Add a Linux z3 binary to the repo, and use that or z3.exe based on the OS --- Binaries/z3 | Bin 0 -> 16438468 bytes Source/Dafny/DafnyOptions.cs | 10 ++++++++++ 2 files changed, 10 insertions(+) create mode 100644 Binaries/z3 (limited to 'Source/Dafny/DafnyOptions.cs') diff --git a/Binaries/z3 b/Binaries/z3 new file mode 100644 index 00000000..7c60feb4 Binary files /dev/null and b/Binaries/z3 differ diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 8972c490..66cf639f 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -11,6 +11,7 @@ namespace Microsoft.Dafny { public DafnyOptions() : base("Dafny", "Dafny program verifier") { + SetZ3ExecutableName(); } public override string VersionNumber { @@ -255,6 +256,15 @@ namespace Microsoft.Dafny // TODO: provide attribute help here } + private void SetZ3ExecutableName() { + var platform = (int)System.Environment.OSVersion.Platform; + var isLinux = platform == 4 || platform == 128; // http://www.mono-project.com/docs/faq/technical/ + + //TODO should we also vendor an OSX build? + var binDir = System.IO.Path.GetDirectoryName(System.Reflection.Assembly.GetExecutingAssembly().Location); + Z3ExecutablePath = System.IO.Path.Combine(binDir, isLinux ? "z3" : "z3.exe"); + } + public override void Usage() { Console.WriteLine(@" ---- Dafny options --------------------------------------------------------- -- cgit v1.2.3 From 3bf4b44b821dca5017017e99502f263e636d5e84 Mon Sep 17 00:00:00 2001 From: leino Date: Tue, 11 Aug 2015 19:07:42 -0700 Subject: Moved discovery of induction variables into a Rewriter. Generate warnings for malformed :induction arguments. Removed the functionality that allowed induction on 'this'. --- Source/Dafny/DafnyOptions.cs | 2 +- Source/Dafny/Printer.cs | 8 +- Source/Dafny/Resolver.cs | 1 + Source/Dafny/Rewriter.cs | 343 ++++++++++++++++++++++++++++- Source/Dafny/Translator.cs | 513 ++++++++++--------------------------------- 5 files changed, 466 insertions(+), 401 deletions(-) (limited to 'Source/Dafny/DafnyOptions.cs') diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 66cf639f..2eea5717 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -312,7 +312,7 @@ namespace Microsoft.Dafny 2 - apply induction as requested (by attributes) and also for heuristically chosen quantifiers 3 (default) - apply induction as requested, and for - heuristically chosen quantifiers and ghost methods + heuristically chosen quantifiers and lemmas /inductionHeuristic: 0 - least discriminating induction heuristic (that is, lean toward applying induction more often) diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 1fa90e41..7a93a140 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -109,11 +109,11 @@ namespace Microsoft.Dafny { } } - public static string OneAttributeToString(Attributes a) { + public static string OneAttributeToString(Attributes a, string nameSubstitution = null) { Contract.Requires(a != null); using (var wr = new System.IO.StringWriter()) { var pr = new Printer(wr); - pr.PrintOneAttribute(a); + pr.PrintOneAttribute(a, nameSubstitution); return ToStringWithoutNewline(wr); } } @@ -441,9 +441,9 @@ namespace Microsoft.Dafny { PrintOneAttribute(a); } } - public void PrintOneAttribute(Attributes a) { + public void PrintOneAttribute(Attributes a, string nameSubstitution = null) { Contract.Requires(a != null); - wr.Write(" {{:{0}", a.Name); + wr.Write(" {{:{0}", nameSubstitution ?? a.Name); if (a.Args != null) { PrintAttributeArgs(a.Args, false); } diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index a58d6e6c..75d171ac 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -322,6 +322,7 @@ namespace Microsoft.Dafny if (DafnyOptions.O.AutoTriggers) { rewriters.Add(new TriggersRewriter(this)); } + rewriters.Add(new InductionRewriter(this)); systemNameInfo = RegisterTopLevelDecls(prog.BuiltIns.SystemModule, false); prog.CompileModules.Add(prog.BuiltIns.SystemModule); diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index 4223fb7f..ffd808c5 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -1266,6 +1266,347 @@ namespace Microsoft.Dafny return new AutoGeneratedToken(tok); } } -} + // =========================================================================================== + + public class InductionRewriter : IRewriter + { + Resolver Resolver; + internal InductionRewriter(Resolver resolver) { + Contract.Requires(resolver != null); + this.Resolver = resolver; + } + public void PreResolve(ModuleDefinition m) { + } + public void PostResolve(ModuleDefinition m) { + } + public void PostCyclicityResolve(ModuleDefinition m) { + if (DafnyOptions.O.Induction == 0) { + // Don't bother inferring :induction attributes. This will also have the effect of not warning about malformed :induction attributes + } else { + foreach (var decl in m.TopLevelDecls) { + if (decl is ClassDecl) { + var cl = (ClassDecl)decl; + foreach (var member in cl.Members) { + if (member is FixpointLemma) { + var method = (FixpointLemma)member; + ProcessMethodExpressions(method); + ComputeLemmaInduction(method.PrefixLemma); + ProcessMethodExpressions(method.PrefixLemma); + } else if (member is Method) { + var method = (Method)member; + ComputeLemmaInduction(method); + ProcessMethodExpressions(method); + } else if (member is FixpointPredicate) { + var function = (FixpointPredicate)member; + ProcessFunctionExpressions(function); + ProcessFunctionExpressions(function.PrefixPredicate); + } else if (member is Function) { + var function = (Function)member; + ProcessFunctionExpressions(function); + } + } + } else if (decl is NewtypeDecl) { + var nt = (NewtypeDecl)decl; + if (nt.Constraint != null) { + var visitor = new Induction_Visitor(this); + visitor.Visit(nt.Constraint); + } + } + } + } + } + void ProcessMethodExpressions(Method method) { + Contract.Requires(method != null); + var visitor = new Induction_Visitor(this); + method.Req.ForEach(mfe => visitor.Visit(mfe.E)); + method.Ens.ForEach(mfe => visitor.Visit(mfe.E)); + if (method.Body != null) { + visitor.Visit(method.Body); + } + } + void ProcessFunctionExpressions(Function function) { + Contract.Requires(function != null); + var visitor = new Induction_Visitor(this); + function.Req.ForEach(visitor.Visit); + function.Ens.ForEach(visitor.Visit); + if (function.Body != null) { + visitor.Visit(function.Body); + } + } + void ComputeLemmaInduction(Method method) { + Contract.Requires(method != null); + if (method.IsGhost && method.Mod.Expressions.Count == 0 && method.Outs.Count == 0 && !(method is FixpointLemma)) { + var posts = new List(); + method.Ens.ForEach(mfe => posts.Add(mfe.E)); + ComputeInductionVariables(method.tok, method.Ins, posts, ref method.Attributes); + } + } + void ComputeInductionVariables(IToken tok, List boundVars, List searchExprs, ref Attributes attributes) where VarType : class, IVariable { + Contract.Requires(tok != null); + Contract.Requires(boundVars != null); + Contract.Requires(searchExprs != null); + Contract.Requires(DafnyOptions.O.Induction != 0); + bool forLemma = boundVars is List; + + var args = Attributes.FindExpressions(attributes, "induction"); // we only look at the first one we find, since it overrides any other ones + if (args == null) { + if (DafnyOptions.O.Induction < 2) { + // No explicit induction variables and we're asked not to infer anything, so we're done + return; + } else if (DafnyOptions.O.Induction == 2 && forLemma) { + // We're asked to infer induction variables only for quantifiers, not for lemmas + return; + } + // GO INFER below (only select boundVars) + } else if (args.Count == 0) { + // {:induction} is treated the same as {:induction true}, which says to automatically infer induction variables + // GO INFER below (all boundVars) + } else if (args.Count == 1 && args[0] is LiteralExpr && ((LiteralExpr)args[0]).Value is bool) { + // {:induction false} or {:induction true} + if (!(bool)((LiteralExpr)args[0]).Value) { + // we're told not to infer anything + return; + } + // GO INFER below (all boundVars) + } else { + // Here, we're expecting the arguments to {:induction args} to be a sublist of "boundVars". + var goodArguments = new List(); + var i = 0; + foreach (var arg in args) { + var ie = arg.Resolved as IdentifierExpr; + if (ie != null) { + var j = boundVars.FindIndex(i, v => v == ie.Var); + if (i <= j) { + goodArguments.Add(ie); + i = j; + continue; + } + if (0 <= boundVars.FindIndex(v => v == ie.Var)) { + Resolver.Warning(arg.tok, "{0}s given as :induction arguments must be given in the same order as in the {1}; ignoring attribute", + forLemma ? "lemma parameter" : "bound variable", forLemma ? "lemma" : "quantifier"); + return; + } + } + Resolver.Warning(arg.tok, "invalid :induction attribute argument; expected {0}{1}; ignoring attribute", + i == 0 ? "'false' or 'true' or " : "", + forLemma ? "lemma parameter" : "bound variable"); + return; + } + // The argument list was legal, so let's use it for the _induction attribute + attributes = new Attributes("_induction", goodArguments, attributes); + return; + } + + // Okay, here we go, coming up with good induction setting for the given situation + var inductionVariables = new List(); + foreach (IVariable n in boundVars) { + if (!n.Type.IsTypeParameter && (args != null || searchExprs.Exists(expr => VarOccursInArgumentToRecursiveFunction(expr, n)))) { + inductionVariables.Add(new IdentifierExpr(n)); + } + } + if (inductionVariables.Count != 0) { + // We found something usable, so let's record that in an attribute + attributes = new Attributes("_induction", inductionVariables, attributes); + // And since we're inferring something, let's also report that in a hover text. + var s = Printer.OneAttributeToString(attributes, "induction"); + Resolver.ReportAdditionalInformation(tok, s, s.Length); + } + } + class Induction_Visitor : BottomUpVisitor + { + readonly InductionRewriter IndRewriter; + public Induction_Visitor(InductionRewriter inductionRewriter) { + Contract.Requires(inductionRewriter != null); + IndRewriter = inductionRewriter; + } + protected override void VisitOneExpr(Expression expr) { + var q = expr as QuantifierExpr; + if (q != null) { + IndRewriter.ComputeInductionVariables(q.tok, q.BoundVars, new List() { q.LogicalBody() }, ref q.Attributes); + } + } + void VisitInductionStmt(Statement stmt) { + Contract.Requires(stmt != null); + // visit a selection of subexpressions + if (stmt is AssertStmt) { + var s = (AssertStmt)stmt; + Visit(s.Expr); + } + // recursively visit all substatements + foreach (var s in stmt.SubStatements) { + VisitInductionStmt(s); + } + } + } + + /// + /// Returns 'true' iff by looking at 'expr' the Induction Heuristic determines that induction should be applied to 'n'. + /// More precisely: + /// DafnyInductionHeuristic Return 'true' + /// ----------------------- ------------- + /// 0 always + /// 1 if 'n' occurs as any subexpression (of 'expr') + /// 2 if 'n' occurs as any subexpression of any index argument of an array/sequence select expression or any argument to a recursive function + /// 3 if 'n' occurs as a prominent subexpression of any index argument of an array/sequence select expression or any argument to a recursive function + /// 4 if 'n' occurs as any subexpression of any argument to a recursive function + /// 5 if 'n' occurs as a prominent subexpression of any argument to a recursive function + /// 6 if 'n' occurs as a prominent subexpression of any decreases-influencing argument to a recursive function + /// Parameter 'n' is allowed to be a ThisSurrogate. + /// + public static bool VarOccursInArgumentToRecursiveFunction(Expression expr, IVariable n) { + switch (DafnyOptions.O.InductionHeuristic) { + case 0: return true; + case 1: return Translator.ContainsFreeVariable(expr, false, n); + default: return VarOccursInArgumentToRecursiveFunction(expr, n, false); + } + } + + /// + /// Worker routine for VarOccursInArgumentToRecursiveFunction(expr,n), where the additional parameter 'exprIsProminent' says whether or + /// not 'expr' has prominent status in its context. + /// DafnyInductionHeuristic cases 0 and 1 are assumed to be handled elsewhere (i.e., a precondition of this method is DafnyInductionHeuristic is at least 2). + /// Parameter 'n' is allowed to be a ThisSurrogate. + /// + static bool VarOccursInArgumentToRecursiveFunction(Expression expr, IVariable n, bool exprIsProminent) { + Contract.Requires(expr != null); + Contract.Requires(n != null); + + // The following variable is what gets passed down to recursive calls if the subexpression does not itself acquire prominent status. + var subExprIsProminent = DafnyOptions.O.InductionHeuristic == 2 || DafnyOptions.O.InductionHeuristic == 4 ? /*once prominent, always prominent*/exprIsProminent : /*reset the prominent status*/false; + + if (expr is ThisExpr) { + return exprIsProminent && n is ThisSurrogate; + } else if (expr is IdentifierExpr) { + var e = (IdentifierExpr)expr; + return exprIsProminent && e.Var == n; + } else if (expr is SeqSelectExpr) { + var e = (SeqSelectExpr)expr; + var q = DafnyOptions.O.InductionHeuristic < 4 || subExprIsProminent; + return VarOccursInArgumentToRecursiveFunction(e.Seq, n, subExprIsProminent) || // this subexpression does not acquire "prominent" status + (e.E0 != null && VarOccursInArgumentToRecursiveFunction(e.E0, n, q)) || // this one does (unless arrays/sequences are excluded) + (e.E1 != null && VarOccursInArgumentToRecursiveFunction(e.E1, n, q)); // ditto + } else if (expr is MultiSelectExpr) { + var e = (MultiSelectExpr)expr; + var q = DafnyOptions.O.InductionHeuristic < 4 || subExprIsProminent; + return VarOccursInArgumentToRecursiveFunction(e.Array, n, subExprIsProminent) || + e.Indices.Exists(exp => VarOccursInArgumentToRecursiveFunction(exp, n, q)); + } else if (expr is FunctionCallExpr) { + var e = (FunctionCallExpr)expr; + // For recursive functions: arguments are "prominent" + // For non-recursive function: arguments are "prominent" if the call is + var rec = e.Function.IsRecursive && e.CoCall != FunctionCallExpr.CoCallResolution.Yes; + var decr = e.Function.Decreases.Expressions; + bool variantArgument; + if (DafnyOptions.O.InductionHeuristic < 6) { + variantArgument = rec; + } else { + // The receiver is considered to be "variant" if the function is recursive and the receiver participates + // in the effective decreases clause of the function. The receiver participates if it's a free variable + // of a term in the explicit decreases clause. + variantArgument = rec && decr.Exists(ee => Translator.ContainsFreeVariable(ee, true, null)); + } + if (VarOccursInArgumentToRecursiveFunction(e.Receiver, n, variantArgument || subExprIsProminent)) { + return true; + } + Contract.Assert(e.Function.Formals.Count == e.Args.Count); + for (int i = 0; i < e.Function.Formals.Count; i++) { + var f = e.Function.Formals[i]; + var exp = e.Args[i]; + if (DafnyOptions.O.InductionHeuristic < 6) { + variantArgument = rec; + } else if (rec) { + // The argument position is considered to be "variant" if the function is recursive and... + // ... it has something to do with why the callee is well-founded, which happens when... + if (f is ImplicitFormal) { + // ... it is the argument is the implicit _k parameter, which is always first in the effective decreases clause of a prefix lemma, or + variantArgument = true; + } else if (decr.Exists(ee => Translator.ContainsFreeVariable(ee, false, f))) { + // ... it participates in the effective decreases clause of the function, which happens when it is + // a free variable of a term in the explicit decreases clause, or + variantArgument = true; + } else { + // ... the callee is a prefix predicate. + variantArgument = true; + } + } + if (VarOccursInArgumentToRecursiveFunction(exp, n, variantArgument || subExprIsProminent)) { + return true; + } + } + return false; + } else if (expr is TernaryExpr) { + var e = (TernaryExpr)expr; + switch (e.Op) { + case TernaryExpr.Opcode.PrefixEqOp: + case TernaryExpr.Opcode.PrefixNeqOp: + return VarOccursInArgumentToRecursiveFunction(e.E0, n, true) || + VarOccursInArgumentToRecursiveFunction(e.E1, n, subExprIsProminent) || + VarOccursInArgumentToRecursiveFunction(e.E2, n, subExprIsProminent); + default: + Contract.Assert(false); throw new cce.UnreachableException(); // unexpected ternary expression + } + } else if (expr is DatatypeValue) { + var e = (DatatypeValue)expr; + var q = n.Type.IsDatatype ? exprIsProminent : subExprIsProminent; // prominent status continues, if we're looking for a variable whose type is a datatype + return e.Arguments.Exists(exp => VarOccursInArgumentToRecursiveFunction(exp, n, q)); + } else if (expr is UnaryExpr) { + var e = (UnaryExpr)expr; + // both Not and SeqLength preserve prominence + return VarOccursInArgumentToRecursiveFunction(e.E, n, exprIsProminent); + } else if (expr is BinaryExpr) { + var e = (BinaryExpr)expr; + bool q; + switch (e.ResolvedOp) { + case BinaryExpr.ResolvedOpcode.Add: + case BinaryExpr.ResolvedOpcode.Sub: + case BinaryExpr.ResolvedOpcode.Mul: + case BinaryExpr.ResolvedOpcode.Div: + case BinaryExpr.ResolvedOpcode.Mod: + case BinaryExpr.ResolvedOpcode.Union: + case BinaryExpr.ResolvedOpcode.Intersection: + case BinaryExpr.ResolvedOpcode.SetDifference: + case BinaryExpr.ResolvedOpcode.Concat: + // these operators preserve prominence + q = exprIsProminent; + break; + default: + // whereas all other binary operators do not + q = subExprIsProminent; + break; + } + return VarOccursInArgumentToRecursiveFunction(e.E0, n, q) || + VarOccursInArgumentToRecursiveFunction(e.E1, n, q); + } else if (expr is StmtExpr) { + var e = (StmtExpr)expr; + // ignore the statement + return VarOccursInArgumentToRecursiveFunction(e.E, n); + + } else if (expr is ITEExpr) { + var e = (ITEExpr)expr; + return VarOccursInArgumentToRecursiveFunction(e.Test, n, subExprIsProminent) || // test is not "prominent" + VarOccursInArgumentToRecursiveFunction(e.Thn, n, exprIsProminent) || // but the two branches are + VarOccursInArgumentToRecursiveFunction(e.Els, n, exprIsProminent); + } else if (expr is OldExpr || + expr is ConcreteSyntaxExpression || + expr is BoxingCastExpr || + expr is UnboxingCastExpr) { + foreach (var exp in expr.SubExpressions) { + if (VarOccursInArgumentToRecursiveFunction(exp, n, exprIsProminent)) { // maintain prominence + return true; + } + } + return false; + } else { + // in all other cases, reset the prominence status and recurse on the subexpressions + foreach (var exp in expr.SubExpressions) { + if (VarOccursInArgumentToRecursiveFunction(exp, n, subExprIsProminent)) { + return true; + } + } + return false; + } + } + } +} diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index b8c4b8ec..cdfb1a32 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -2756,126 +2756,117 @@ namespace Microsoft.Dafny { Bpl.StmtList stmts; if (!wellformednessProc) { - if (3 <= DafnyOptions.O.Induction && m.IsGhost && m.Mod.Expressions.Count == 0 && m.Outs.Count == 0 && !(m is FixpointLemma)) { - var posts = new List(); - m.Ens.ForEach(mfe => posts.Add(mfe.E)); - var allIns = new List(); - if (!m.IsStatic) { - allIns.Add(new ThisSurrogate(m.tok, Resolver.GetThisType(m.tok, (ClassDecl)m.EnclosingClass))); - } - allIns.AddRange(m.Ins); - var inductionVars = ApplyInduction(allIns, m.Attributes, posts, delegate(System.IO.TextWriter wr) { wr.Write(m.FullName); }); - if (inductionVars.Count != 0) { - // Let the parameters be this,x,y of the method M and suppose ApplyInduction returns this,y. - // Also, let Pre be the precondition and VF be the decreases clause. - // Then, insert into the method body what amounts to: - // assume case-analysis-on-parameter[[ y' ]]; - // forall (this', y' | Pre(this', x, y') && VF(this', x, y') << VF(this, x, y)) { - // this'.M(x, y'); - // } - // Generate bound variables for the forall statement, and a substitution for the Pre and VF - - // assume case-analysis-on-parameter[[ y' ]]; - foreach (var inFormal in m.Ins) { - var dt = inFormal.Type.AsDatatype; - if (dt != null) { - var funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(inFormal.tok, "$IsA#" + dt.FullSanitizedName, Bpl.Type.Bool)); - var f = new Bpl.IdentifierExpr(inFormal.tok, inFormal.AssignUniqueName(m.IdGenerator), TrType(inFormal.Type)); - builder.Add(new Bpl.AssumeCmd(inFormal.tok, new Bpl.NAryExpr(inFormal.tok, funcID, new List { f }))); - } - } - - var parBoundVars = new List(); - Expression receiverReplacement = null; - var substMap = new Dictionary(); - foreach (var iv in inductionVars) { - BoundVar bv; - IdentifierExpr ie; - CloneVariableAsBoundVar(iv.tok, iv, "$ih#" + iv.Name, out bv, out ie); - parBoundVars.Add(bv); - if (iv is ThisSurrogate) { - Contract.Assert(receiverReplacement == null && substMap.Count == 0); // the receiver comes first, if at all - receiverReplacement = ie; - } else { - substMap.Add(iv, ie); - } + var inductionVars = ApplyInduction(m.Ins, m.Attributes); + if (inductionVars.Count != 0) { + // Let the parameters be this,x,y of the method M and suppose ApplyInduction returns y. + // Also, let Pre be the precondition and VF be the decreases clause. + // Then, insert into the method body what amounts to: + // assume case-analysis-on-parameter[[ y' ]]; + // forall (y' | Pre(this, x, y') && VF(this, x, y') << VF(this, x, y)) { + // this.M(x, y'); + // } + // Generate bound variables for the forall statement, and a substitution for the Pre and VF + + // assume case-analysis-on-parameter[[ y' ]]; + foreach (var inFormal in m.Ins) { + var dt = inFormal.Type.AsDatatype; + if (dt != null) { + var funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(inFormal.tok, "$IsA#" + dt.FullSanitizedName, Bpl.Type.Bool)); + var f = new Bpl.IdentifierExpr(inFormal.tok, inFormal.AssignUniqueName(m.IdGenerator), TrType(inFormal.Type)); + builder.Add(new Bpl.AssumeCmd(inFormal.tok, new Bpl.NAryExpr(inFormal.tok, funcID, new List { f }))); + } + } + + var parBoundVars = new List(); + Expression receiverReplacement = null; + var substMap = new Dictionary(); + foreach (var iv in inductionVars) { + BoundVar bv; + IdentifierExpr ie; + CloneVariableAsBoundVar(iv.tok, iv, "$ih#" + iv.Name, out bv, out ie); + parBoundVars.Add(bv); + if (iv is ThisSurrogate) { + Contract.Assert(receiverReplacement == null && substMap.Count == 0); // the receiver comes first, if at all + receiverReplacement = ie; + } else { + substMap.Add(iv, ie); } + } - // Generate a CallStmt for the recursive call - Expression recursiveCallReceiver; - if (receiverReplacement != null) { - recursiveCallReceiver = receiverReplacement; - } else if (m.IsStatic) { - recursiveCallReceiver = new StaticReceiverExpr(m.tok, (ClassDecl)m.EnclosingClass, true); // this also resolves it + // Generate a CallStmt for the recursive call + Expression recursiveCallReceiver; + if (receiverReplacement != null) { + recursiveCallReceiver = receiverReplacement; + } else if (m.IsStatic) { + recursiveCallReceiver = new StaticReceiverExpr(m.tok, (ClassDecl)m.EnclosingClass, true); // this also resolves it + } else { + recursiveCallReceiver = new ImplicitThisExpr(m.tok); + recursiveCallReceiver.Type = Resolver.GetThisType(m.tok, (ClassDecl)m.EnclosingClass); // resolve here + } + var recursiveCallArgs = new List(); + foreach (var inFormal in m.Ins) { + Expression inE; + if (substMap.TryGetValue(inFormal, out inE)) { + recursiveCallArgs.Add(inE); } else { - recursiveCallReceiver = new ImplicitThisExpr(m.tok); - recursiveCallReceiver.Type = Resolver.GetThisType(m.tok, (ClassDecl)m.EnclosingClass); // resolve here - } - var recursiveCallArgs = new List(); - foreach (var inFormal in m.Ins) { - Expression inE; - if (substMap.TryGetValue(inFormal, out inE)) { - recursiveCallArgs.Add(inE); - } else { - var ie = new IdentifierExpr(inFormal.tok, inFormal.Name); - ie.Var = inFormal; // resolve here - ie.Type = inFormal.Type; // resolve here - recursiveCallArgs.Add(ie); - } - } - var methodSel = new MemberSelectExpr(m.tok, recursiveCallReceiver, m.Name); - methodSel.Member = m; // resolve here - methodSel.TypeApplication = new List(); - methodSel.TypeApplication.AddRange(recursiveCallReceiver.Type.TypeArgs); - m.TypeArgs.ForEach(tp => methodSel.TypeApplication.Add(new UserDefinedType(tp))); - methodSel.Type = new InferredTypeProxy(); // this is the last step in resolving 'methodSel' - var recursiveCall = new CallStmt(m.tok, m.tok, new List(), methodSel, recursiveCallArgs); - recursiveCall.IsGhost = m.IsGhost; // resolve here - - Expression parRange = new LiteralExpr(m.tok, true); - parRange.Type = Type.Bool; // resolve here - if (receiverReplacement != null) { - // add "this' != null" to the range - var nil = new LiteralExpr(receiverReplacement.tok); - nil.Type = receiverReplacement.Type; // resolve here - var neqNull = new BinaryExpr(receiverReplacement.tok, BinaryExpr.Opcode.Neq, receiverReplacement, nil); - neqNull.ResolvedOp = BinaryExpr.ResolvedOpcode.NeqCommon; // resolve here - neqNull.Type = Type.Bool; // resolve here - parRange = Expression.CreateAnd(parRange, neqNull); - } - foreach (var pre in m.Req) { - if (!pre.IsFree) { - parRange = Expression.CreateAnd(parRange, Substitute(pre.E, receiverReplacement, substMap)); - } - } - // construct an expression (generator) for: VF' << VF - ExpressionConverter decrCheck = delegate(Dictionary decrSubstMap, ExpressionTranslator exprTran) { - var decrToks = new List(); - var decrTypes = new List(); - var decrCallee = new List(); - var decrCaller = new List(); - foreach (var ee in m.Decreases.Expressions) { - decrToks.Add(ee.tok); - decrTypes.Add(ee.Type.NormalizeExpand()); - decrCaller.Add(exprTran.TrExpr(ee)); - Expression es = Substitute(ee, receiverReplacement, substMap); - es = Substitute(es, null, decrSubstMap); - decrCallee.Add(exprTran.TrExpr(es)); - } - return DecreasesCheck(decrToks, decrTypes, decrTypes, decrCallee, decrCaller, null, null, false, true); - }; + var ie = new IdentifierExpr(inFormal.tok, inFormal.Name); + ie.Var = inFormal; // resolve here + ie.Type = inFormal.Type; // resolve here + recursiveCallArgs.Add(ie); + } + } + var methodSel = new MemberSelectExpr(m.tok, recursiveCallReceiver, m.Name); + methodSel.Member = m; // resolve here + methodSel.TypeApplication = new List(); + methodSel.TypeApplication.AddRange(recursiveCallReceiver.Type.TypeArgs); + m.TypeArgs.ForEach(tp => methodSel.TypeApplication.Add(new UserDefinedType(tp))); + methodSel.Type = new InferredTypeProxy(); // this is the last step in resolving 'methodSel' + var recursiveCall = new CallStmt(m.tok, m.tok, new List(), methodSel, recursiveCallArgs); + recursiveCall.IsGhost = m.IsGhost; // resolve here + + Expression parRange = new LiteralExpr(m.tok, true); + parRange.Type = Type.Bool; // resolve here + if (receiverReplacement != null) { + // add "this' != null" to the range + var nil = new LiteralExpr(receiverReplacement.tok); + nil.Type = receiverReplacement.Type; // resolve here + var neqNull = new BinaryExpr(receiverReplacement.tok, BinaryExpr.Opcode.Neq, receiverReplacement, nil); + neqNull.ResolvedOp = BinaryExpr.ResolvedOpcode.NeqCommon; // resolve here + neqNull.Type = Type.Bool; // resolve here + parRange = Expression.CreateAnd(parRange, neqNull); + } + foreach (var pre in m.Req) { + if (!pre.IsFree) { + parRange = Expression.CreateAnd(parRange, Substitute(pre.E, receiverReplacement, substMap)); + } + } + // construct an expression (generator) for: VF' << VF + ExpressionConverter decrCheck = delegate(Dictionary decrSubstMap, ExpressionTranslator exprTran) { + var decrToks = new List(); + var decrTypes = new List(); + var decrCallee = new List(); + var decrCaller = new List(); + foreach (var ee in m.Decreases.Expressions) { + decrToks.Add(ee.tok); + decrTypes.Add(ee.Type.NormalizeExpand()); + decrCaller.Add(exprTran.TrExpr(ee)); + Expression es = Substitute(ee, receiverReplacement, substMap); + es = Substitute(es, null, decrSubstMap); + decrCallee.Add(exprTran.TrExpr(es)); + } + return DecreasesCheck(decrToks, decrTypes, decrTypes, decrCallee, decrCaller, null, null, false, true); + }; #if VERIFY_CORRECTNESS_OF_TRANSLATION_FORALL_STATEMENT_RANGE - var definedness = new Bpl.StmtListBuilder(); - var exporter = new Bpl.StmtListBuilder(); - TrForallStmtCall(m.tok, parBoundVars, parRange, decrCheck, recursiveCall, definedness, exporter, localVariables, etran); - // All done, so put the two pieces together - builder.Add(new Bpl.IfCmd(m.tok, null, definedness.Collect(m.tok), null, exporter.Collect(m.tok))); + var definedness = new Bpl.StmtListBuilder(); + var exporter = new Bpl.StmtListBuilder(); + TrForallStmtCall(m.tok, parBoundVars, parRange, decrCheck, recursiveCall, definedness, exporter, localVariables, etran); + // All done, so put the two pieces together + builder.Add(new Bpl.IfCmd(m.tok, null, definedness.Collect(m.tok), null, exporter.Collect(m.tok))); #else - TrForallStmtCall(m.tok, parBoundVars, parRange, decrCheck, recursiveCall, null, builder, localVariables, etran); + TrForallStmtCall(m.tok, parBoundVars, parRange, decrCheck, recursiveCall, null, builder, localVariables, etran); #endif - } } // translate the body of the method Contract.Assert(m.Body != null); // follows from method precondition and the if guard @@ -12965,8 +12956,8 @@ namespace Microsoft.Dafny { /* NB: only for type arg less quantifiers for now: */ && ((QuantifierExpr)expr).TypeArgs.Count == 0) { var e = (QuantifierExpr)expr; - var inductionVariables = ApplyInduction(e); - if (apply_induction && 2 <= DafnyOptions.O.Induction && inductionVariables.Count != 0) { + var inductionVariables = ApplyInduction(e.BoundVars, e.Attributes); + if (apply_induction && inductionVariables.Count != 0) { // From the given quantifier (forall n :: P(n)), generate the seemingly weaker proof obligation // (forall n :: (forall k :: k < n ==> P(k)) ==> P(n)) // For an existential (exists n :: P(n)), it is @@ -13165,297 +13156,29 @@ namespace Microsoft.Dafny { return RefinementToken.IsInherited(expr.tok, currentModule) && (codeContext == null || !codeContext.MustReverify) && RefinementTransformer.ContainsChange(expr, currentModule); } - List ApplyInduction(QuantifierExpr e) { - Contract.Requires(e.TypeArgs.Count == 0); - return ApplyInduction(e.BoundVars, e.Attributes, new List() { e.LogicalBody() }, - delegate(System.IO.TextWriter wr) { new Printer(wr).PrintExpression(e, true); }); - } - - delegate void TracePrinter(System.IO.TextWriter wr); - /// /// Return a subset of "boundVars" (in the order giving in "boundVars") to which to apply induction to, - /// according to :induction attributes in "attributes" and heuristically interesting subexpressions of - /// "searchExprs". + /// according to :_induction attribute in "attributes". /// - List ApplyInduction(List boundVars, Attributes attributes, List searchExprs, TracePrinter tracePrinter) where VarType : class, IVariable + List ApplyInduction(List boundVars, Attributes attributes) where VarType : class, IVariable { Contract.Requires(boundVars != null); - Contract.Requires(searchExprs != null); - Contract.Requires(tracePrinter != null); Contract.Ensures(Contract.Result>() != null); - if (DafnyOptions.O.Induction == 0) { + var args = Attributes.FindExpressions(attributes, "_induction"); + if (args == null) { return new List(); // don't apply induction } - foreach (var a in attributes.AsEnumerable()) { - if (a.Name == "induction") { - // Here are the supported forms of the :induction attribute. - // :induction -- apply induction to all bound variables - // :induction false -- suppress induction, that is, don't apply it to any bound variable - // :induction L where L is a list consisting entirely of bound variables: - // -- apply induction to the specified bound variables - // :induction X where X is anything else - // -- treat the same as {:induction}, that is, apply induction to all - // bound variables - - // Handle {:induction false} - if (a.Args.Count == 1) { - var arg = a.Args[0] as LiteralExpr; - if (arg != null && arg.Value is bool && !(bool)arg.Value) { - if (CommandLineOptions.Clo.Trace) { - Console.Write("Suppressing automatic induction for: "); - tracePrinter(Console.Out); - Console.WriteLine(); - } - return new List(); - } - } - - // Handle {:induction L} - if (a.Args.Count != 0) { - // check that all attribute arguments refer to bound variables; otherwise, go to default_form - var argsAsVars = new List(); - foreach (var arg in a.Args) { - var theArg = arg.Resolved; - if (theArg is ThisExpr) { - foreach (var bv in boundVars) { - if (bv is ThisSurrogate) { - argsAsVars.Add(bv); - goto TRY_NEXT_ATTRIBUTE_ARGUMENT; - } - } - } else if (theArg is IdentifierExpr) { - var id = (IdentifierExpr)theArg; - var bv = id.Var as VarType; - if (bv != null && boundVars.Contains(bv)) { - argsAsVars.Add(bv); - goto TRY_NEXT_ATTRIBUTE_ARGUMENT; - } - } - // the attribute argument was not one of the possible induction variables - goto USE_DEFAULT_FORM; - TRY_NEXT_ATTRIBUTE_ARGUMENT: - ; - } - // so, all attribute arguments are variables; add them to L in the order of the bound variables (not necessarily the order in the attribute) - var L = new List(); - foreach (var bv in boundVars) { - if (argsAsVars.Contains(bv)) { - L.Add(bv); - } - } - if (CommandLineOptions.Clo.Trace) { - string sep = "Applying requested induction on "; - foreach (var bv in L) { - Console.Write("{0}{1}", sep, bv.Name); - sep = ", "; - } - Console.Write(" of: "); - tracePrinter(Console.Out); - Console.WriteLine(); - } - return L; - USE_DEFAULT_FORM: ; - } - - // We have the {:induction} case, or something to be treated in the same way - if (CommandLineOptions.Clo.Trace) { - Console.Write("Applying requested induction on all bound variables of: "); - tracePrinter(Console.Out); - Console.WriteLine(); - } - return boundVars; - } - } - - if (DafnyOptions.O.Induction < 2) { - return new List(); // don't apply induction - } - - // consider automatically applying induction - var inductionVariables = new List(); - foreach (var n in boundVars) { - if (!n.Type.IsTypeParameter && searchExprs.Exists(expr => VarOccursInArgumentToRecursiveFunction(expr, n))) { - if (CommandLineOptions.Clo.Trace) { - Console.Write("Applying automatic induction on variable '{0}' of: ", n.Name); - tracePrinter(Console.Out); - Console.WriteLine(); - } - inductionVariables.Add(n); - } - } - - return inductionVariables; - } - - /// - /// Returns 'true' iff by looking at 'expr' the Induction Heuristic determines that induction should be applied to 'n'. - /// More precisely: - /// DafnyInductionHeuristic Return 'true' - /// ----------------------- ------------- - /// 0 always - /// 1 if 'n' occurs as any subexpression (of 'expr') - /// 2 if 'n' occurs as any subexpression of any index argument of an array/sequence select expression or any argument to a recursive function - /// 3 if 'n' occurs as a prominent subexpression of any index argument of an array/sequence select expression or any argument to a recursive function - /// 4 if 'n' occurs as any subexpression of any argument to a recursive function - /// 5 if 'n' occurs as a prominent subexpression of any argument to a recursive function - /// 6 if 'n' occurs as a prominent subexpression of any decreases-influencing argument to a recursive function - /// Parameter 'n' is allowed to be a ThisSurrogate. - /// - bool VarOccursInArgumentToRecursiveFunction(Expression expr, IVariable n) { - switch (DafnyOptions.O.InductionHeuristic) { - case 0: return true; - case 1: return ContainsFreeVariable(expr, false, n); - default: return VarOccursInArgumentToRecursiveFunction(expr, n, false); - } - } - - /// - /// Worker routine for VarOccursInArgumentToRecursiveFunction(expr,n), where the additional parameter 'exprIsProminent' says whether or - /// not 'expr' has prominent status in its context. - /// DafnyInductionHeuristic cases 0 and 1 are assumed to be handled elsewhere (i.e., a precondition of this method is DafnyInductionHeuristic is at least 2). - /// Parameter 'n' is allowed to be a ThisSurrogate. - /// - bool VarOccursInArgumentToRecursiveFunction(Expression expr, IVariable n, bool exprIsProminent) { - Contract.Requires(expr != null); - Contract.Requires(n != null); - - // The following variable is what gets passed down to recursive calls if the subexpression does not itself acquire prominent status. - var subExprIsProminent = DafnyOptions.O.InductionHeuristic == 2 || DafnyOptions.O.InductionHeuristic == 4 ? /*once prominent, always prominent*/exprIsProminent : /*reset the prominent status*/false; - - if (expr is ThisExpr) { - return exprIsProminent && n is ThisSurrogate; - } else if (expr is IdentifierExpr) { - var e = (IdentifierExpr)expr; - return exprIsProminent && e.Var == n; - } else if (expr is SeqSelectExpr) { - var e = (SeqSelectExpr)expr; - var q = DafnyOptions.O.InductionHeuristic < 4 || subExprIsProminent; - return VarOccursInArgumentToRecursiveFunction(e.Seq, n, subExprIsProminent) || // this subexpression does not acquire "prominent" status - (e.E0 != null && VarOccursInArgumentToRecursiveFunction(e.E0, n, q)) || // this one does (unless arrays/sequences are excluded) - (e.E1 != null && VarOccursInArgumentToRecursiveFunction(e.E1, n, q)); // ditto - } else if (expr is MultiSelectExpr) { - var e = (MultiSelectExpr)expr; - var q = DafnyOptions.O.InductionHeuristic < 4 || subExprIsProminent; - return VarOccursInArgumentToRecursiveFunction(e.Array, n, subExprIsProminent) || - e.Indices.Exists(exp => VarOccursInArgumentToRecursiveFunction(exp, n, q)); - } else if (expr is FunctionCallExpr) { - var e = (FunctionCallExpr)expr; - // For recursive functions: arguments are "prominent" - // For non-recursive function: arguments are "prominent" if the call is - var rec = e.Function.IsRecursive && e.CoCall != FunctionCallExpr.CoCallResolution.Yes; - var decr = e.Function.Decreases.Expressions; - bool variantArgument; - if (DafnyOptions.O.InductionHeuristic < 6) { - variantArgument = rec; - } else { - // The receiver is considered to be "variant" if the function is recursive and the receiver participates - // in the effective decreases clause of the function. The receiver participates if it's a free variable - // of a term in the explicit decreases clause. - variantArgument = rec && decr.Exists(ee => ContainsFreeVariable(ee, true, null)); - } - if (VarOccursInArgumentToRecursiveFunction(e.Receiver, n, variantArgument || subExprIsProminent)) { - return true; - } - Contract.Assert(e.Function.Formals.Count == e.Args.Count); - for (int i = 0; i < e.Function.Formals.Count; i++) { - var f = e.Function.Formals[i]; - var exp = e.Args[i]; - if (DafnyOptions.O.InductionHeuristic < 6) { - variantArgument = rec; - } else if (rec) { - // The argument position is considered to be "variant" if the function is recursive and... - // ... it has something to do with why the callee is well-founded, which happens when... - if (f is ImplicitFormal) { - // ... it is the argument is the implicit _k parameter, which is always first in the effective decreases clause of a prefix lemma, or - variantArgument = true; - } else if (decr.Exists(ee => ContainsFreeVariable(ee, false, f))) { - // ... it participates in the effective decreases clause of the function, which happens when it is - // a free variable of a term in the explicit decreases clause, or - variantArgument = true; - } else { - // ... the callee is a prefix predicate. - variantArgument = true; - } - } - if (VarOccursInArgumentToRecursiveFunction(exp, n, variantArgument || subExprIsProminent)) { - return true; - } - } - return false; - } else if (expr is TernaryExpr) { - var e = (TernaryExpr)expr; - switch (e.Op) { - case TernaryExpr.Opcode.PrefixEqOp: - case TernaryExpr.Opcode.PrefixNeqOp: - return VarOccursInArgumentToRecursiveFunction(e.E0, n, true) || - VarOccursInArgumentToRecursiveFunction(e.E1, n, subExprIsProminent) || - VarOccursInArgumentToRecursiveFunction(e.E2, n, subExprIsProminent); - default: - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected ternary expression - } - } else if (expr is DatatypeValue) { - var e = (DatatypeValue)expr; - var q = n.Type.IsDatatype ? exprIsProminent : subExprIsProminent; // prominent status continues, if we're looking for a variable whose type is a datatype - return e.Arguments.Exists(exp => VarOccursInArgumentToRecursiveFunction(exp, n, q)); - } else if (expr is UnaryExpr) { - var e = (UnaryExpr)expr; - // both Not and SeqLength preserve prominence - return VarOccursInArgumentToRecursiveFunction(e.E, n, exprIsProminent); - } else if (expr is BinaryExpr) { - var e = (BinaryExpr)expr; - bool q; - switch (e.ResolvedOp) { - case BinaryExpr.ResolvedOpcode.Add: - case BinaryExpr.ResolvedOpcode.Sub: - case BinaryExpr.ResolvedOpcode.Mul: - case BinaryExpr.ResolvedOpcode.Div: - case BinaryExpr.ResolvedOpcode.Mod: - case BinaryExpr.ResolvedOpcode.Union: - case BinaryExpr.ResolvedOpcode.Intersection: - case BinaryExpr.ResolvedOpcode.SetDifference: - case BinaryExpr.ResolvedOpcode.Concat: - // these operators preserve prominence - q = exprIsProminent; - break; - default: - // whereas all other binary operators do not - q = subExprIsProminent; - break; - } - return VarOccursInArgumentToRecursiveFunction(e.E0, n, q) || - VarOccursInArgumentToRecursiveFunction(e.E1, n, q); - } else if (expr is StmtExpr) { - var e = (StmtExpr)expr; - // ignore the statement - return VarOccursInArgumentToRecursiveFunction(e.E, n); - - } else if (expr is ITEExpr) { - var e = (ITEExpr)expr; - return VarOccursInArgumentToRecursiveFunction(e.Test, n, subExprIsProminent) || // test is not "prominent" - VarOccursInArgumentToRecursiveFunction(e.Thn, n, exprIsProminent) || // but the two branches are - VarOccursInArgumentToRecursiveFunction(e.Els, n, exprIsProminent); - } else if (expr is OldExpr || - expr is ConcreteSyntaxExpression || - expr is BoxingCastExpr || - expr is UnboxingCastExpr) { - foreach (var exp in expr.SubExpressions) { - if (VarOccursInArgumentToRecursiveFunction(exp, n, exprIsProminent)) { // maintain prominence - return true; - } - } - return false; - } else { - // in all other cases, reset the prominence status and recurse on the subexpressions - foreach (var exp in expr.SubExpressions) { - if (VarOccursInArgumentToRecursiveFunction(exp, n, subExprIsProminent)) { - return true; - } - } - return false; + var argsAsVars = new List(); + foreach (var arg in args) { + // We expect each "arg" to be an IdentifierExpr among "boundVars" + var id = (IdentifierExpr)arg; + var bv = (VarType)id.Var; + Contract.Assume(boundVars.Contains(bv)); + argsAsVars.Add(bv); } + return argsAsVars; } IEnumerable InductionCases(Type ty, Bpl.Expr expr, ExpressionTranslator etran) { @@ -13502,7 +13225,7 @@ namespace Microsoft.Dafny { /// Parameter 'v' is allowed to be a ThisSurrogate, in which case the method return true iff 'this' /// occurs in 'expr'. /// - static bool ContainsFreeVariable(Expression expr, bool lookForReceiver, IVariable v) { + public static bool ContainsFreeVariable(Expression expr, bool lookForReceiver, IVariable v) { Contract.Requires(expr != null); Contract.Requires(lookForReceiver || v != null); -- cgit v1.2.3 From 4b3fc0e7413424e27131dd8dd919423711f097ad Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Tue, 18 Aug 2015 08:46:35 -0700 Subject: Use a nice warning symbol in some warning messages This is useful because trigger-related messages can contain quite a bit of information, especially if they include info about multiple split quantifiers. --- Source/Dafny/DafnyOptions.cs | 1 + Source/Dafny/Triggers/QuantifiersCollection.cs | 58 +++++++++++++++----------- Source/DafnyServer/Server.cs | 4 +- Source/DafnyServer/Utilities.cs | 5 ++- 4 files changed, 40 insertions(+), 28 deletions(-) (limited to 'Source/Dafny/DafnyOptions.cs') diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 66cf639f..245632ad 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -40,6 +40,7 @@ namespace Microsoft.Dafny Bpl.CommandLineOptions.Install(options); } + public bool UnicodeOutput = false; public bool DisallowSoundnessCheating = false; public bool Dafnycc = false; public int Induction = 3; diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs index 828e0e18..cbc212d2 100644 --- a/Source/Dafny/Triggers/QuantifiersCollection.cs +++ b/Source/Dafny/Triggers/QuantifiersCollection.cs @@ -132,55 +132,63 @@ namespace Microsoft.Dafny.Triggers { //FIXME } - private void CommitOne(QuantifierWithTriggers q, object conjunctId) { + private void CommitOne(QuantifierWithTriggers q, bool addHeader) { var errorLevel = ErrorLevel.Info; var msg = new StringBuilder(); - var indent = conjunctId != null ? " " : " "; - var header = conjunctId != null ? String.Format(" For conjunct {0}:{1}", conjunctId, Environment.NewLine) : ""; + var indent = addHeader ? " " : " "; //FIXME if multiline messages were properly supported, this indentation wouldn't be needed - if (!TriggerUtils.NeedsAutoTriggers(q.quantifier)) { //FIXME: no_trigger is passed down to Boogie - msg.Append(indent).AppendLine("Not generating triggers for this quantifier."); + if (!TriggerUtils.NeedsAutoTriggers(q.quantifier)) { //FIXME: matchingloop and autotriggers attributes are passed down to Boogie + msg.AppendFormat(" Not generating triggers for {{{0}}}.", Printer.ExprToString(q.quantifier.Term)).AppendLine(); + // FIXME This shouldn't be printed for autoReqs. (see autoReq.dfy) + // FIXME typeQuantifier? } else { - foreach (var candidate in q.Candidates) { - q.quantifier.Attributes = new Attributes("trigger", candidate.Terms.Select(t => t.Expr).ToList(), q.quantifier.Attributes); + if (addHeader) { + msg.AppendFormat(" For expression {{{0}}}:", Printer.ExprToString(q.quantifier.Term)).AppendLine(); } - if (q.Candidates.Any()) { - msg.Append(indent).AppendLine("Selected triggers:"); - foreach (var mc in q.Candidates) { - msg.Append(indent).Append(" ").AppendLine(mc.ToString()); - } + foreach (var candidate in q.Candidates) { //FIXME make this _trigger instead of trigger + q.quantifier.Attributes = new Attributes("trigger", candidate.Terms.Select(t => t.Expr).ToList(), q.quantifier.Attributes); } - if (q.RejectedCandidates.Any()) { - msg.Append(indent).AppendLine("Rejected triggers:"); - foreach (var mc in q.RejectedCandidates) { - msg.Append(indent).Append(" ").AppendLine(mc.ToString()); - } - } + AddTriggersToMessage("Selected triggers:", q.Candidates, msg, indent); + AddTriggersToMessage("Rejected triggers:", q.RejectedCandidates, msg, indent, true); #if QUANTIFIER_WARNINGS + string WARN = DafnyOptions.O.UnicodeOutput ? "⚠ " : "(!) "; //FIXME set unicodeoutput in extension if (!q.CandidateTerms.Any()) { errorLevel = ErrorLevel.Warning; - msg.Append(indent).AppendLine("No terms found to trigger on."); + msg.Append(indent).Append(WARN).AppendLine("No terms found to trigger on."); } else if (!q.Candidates.Any()) { errorLevel = ErrorLevel.Warning; - msg.Append(indent).AppendLine("No trigger covering all quantified variables found."); - } else if (!q.CouldSuppressLoops) { + msg.Append(indent).Append(WARN).AppendLine("No trigger covering all quantified variables found."); + } else if (!q.CouldSuppressLoops && !q.AllowsLoops) { errorLevel = ErrorLevel.Warning; - msg.Append(indent).AppendLine("Suppressing loops would leave this quantifier without triggers."); + msg.Append(indent).Append(WARN).AppendLine("Suppressing loops would leave this expression without triggers."); } #endif } - + if (msg.Length > 0) { - reporter.Message(MessageSource.Rewriter, errorLevel, q.quantifier.tok, header + msg.ToString()); + reporter.Message(MessageSource.Rewriter, errorLevel, q.quantifier.tok, msg.ToString().TrimEnd("\r\n".ToCharArray())); + } + } + + private static void AddTriggersToMessage(string header, List triggers, StringBuilder msg, string indent, bool newlines = false) { + if (triggers.Any()) { + msg.Append(indent).Append(header); + if (triggers.Count == 1) { + msg.Append(" "); + } else if (triggers.Count > 1) { + msg.AppendLine().Append(indent).Append(" "); + } + var separator = newlines && triggers.Count > 1 ? Environment.NewLine + indent + " " : ", "; + msg.AppendLine(String.Join(separator, triggers)); } } internal void CommitTriggers() { foreach (var q in quantifiers) { - CommitOne(q, quantifiers.Count > 1 ? q.quantifier : null); + CommitOne(q, quantifiers.Count > 1); } } } diff --git a/Source/DafnyServer/Server.cs b/Source/DafnyServer/Server.cs index 74cdd8c2..bdfd66b4 100644 --- a/Source/DafnyServer/Server.cs +++ b/Source/DafnyServer/Server.cs @@ -33,11 +33,13 @@ namespace Microsoft.Dafny { public Server() { this.running = true; Console.CancelKeyPress += this.CancelKeyPress; + Console.InputEncoding = System.Text.Encoding.UTF8; + Console.OutputEncoding = System.Text.Encoding.UTF8; ExecutionEngine.printer = new DafnyConsolePrinter(); } void CancelKeyPress(object sender, ConsoleCancelEventArgs e) { - e.Cancel = true; + // e.Cancel = true; // FIXME TerminateProver and RunningProverFromCommandLine // Cancel the current verification? TerminateProver() ? Or kill entirely? } diff --git a/Source/DafnyServer/Utilities.cs b/Source/DafnyServer/Utilities.cs index 8fb03b05..4b06e9f5 100644 --- a/Source/DafnyServer/Utilities.cs +++ b/Source/DafnyServer/Utilities.cs @@ -45,13 +45,14 @@ namespace Microsoft.Dafny { internal static void ApplyArgs(string[] args) { Dafny.DafnyOptions.Install(new Dafny.DafnyOptions()); + Dafny.DafnyOptions.O.ProverKillTime = 10; if (CommandLineOptions.Clo.Parse(args)) { // Dafny.DafnyOptions.O.ErrorTrace = 0; //FIXME // Dafny.DafnyOptions.O.ModelViewFile = "-"; - Dafny.DafnyOptions.O.ProverKillTime = 10; - Dafny.DafnyOptions.O.VcsCores = Math.Max(1, System.Environment.ProcessorCount - 1); + Dafny.DafnyOptions.O.UnicodeOutput = true; Dafny.DafnyOptions.O.VerifySnapshots = 2; + Dafny.DafnyOptions.O.VcsCores = Math.Max(1, System.Environment.ProcessorCount - 1); } else { throw new ServerException("Invalid command line options"); } -- cgit v1.2.3 From 8ede9fda35767f083899940886b69f53640891c9 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Thu, 27 Aug 2015 18:59:10 -0700 Subject: Look for z3 in Binaries/z3/bin (but keep the vendored version for convenience) Dafny now first looks for a z3 binary in z3/bin, and if it can't find one it looks for one in Binaries/z3.exe (mostly for backwards-compatibility with already set-up source installations). --- Binaries/z3 | Bin 16438468 -> 0 bytes Source/Dafny/DafnyOptions.cs | 37 ++++++++++++++++++++++++++++----- Source/Dafny/Reporting.cs | 2 +- Source/DafnyDriver/DafnyDriver.cs | 14 ++++++------- Source/DafnyServer/DafnyHelper.cs | 5 ++++- Source/DafnyServer/Utilities.cs | 4 ++-- Source/DafnyServer/VerificationTask.cs | 3 +-- 7 files changed, 47 insertions(+), 18 deletions(-) delete mode 100755 Binaries/z3 (limited to 'Source/Dafny/DafnyOptions.cs') diff --git a/Binaries/z3 b/Binaries/z3 deleted file mode 100755 index 7c60feb4..00000000 Binary files a/Binaries/z3 and /dev/null differ diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 1986ea6d..08e53d5c 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -9,8 +9,11 @@ namespace Microsoft.Dafny { public class DafnyOptions : Bpl.CommandLineOptions { - public DafnyOptions() + private ErrorReporter errorReporter; + + public DafnyOptions(ErrorReporter errorReporter = null) : base("Dafny", "Dafny program verifier") { + this.errorReporter = errorReporter; SetZ3ExecutableName(); } @@ -257,13 +260,37 @@ namespace Microsoft.Dafny // TODO: provide attribute help here } + + /// + /// Dafny comes with it's own copy of z3, to save new users the trouble of having to install extra dependency. + /// For this to work, Dafny makes the Z3ExecutablePath point to the path were Z3 is put by our release script. + /// For developers though (and people getting this from source), it's convenient to be able to run right away, + /// so we vendor a Windows version. + /// private void SetZ3ExecutableName() { var platform = (int)System.Environment.OSVersion.Platform; - var isLinux = platform == 4 || platform == 128; // http://www.mono-project.com/docs/faq/technical/ - //TODO should we also vendor an OSX build? - var binDir = System.IO.Path.GetDirectoryName(System.Reflection.Assembly.GetExecutingAssembly().Location); - Z3ExecutablePath = System.IO.Path.Combine(binDir, isLinux ? "z3" : "z3.exe"); + // http://www.mono-project.com/docs/faq/technical/ + var isUnix = platform == 4 || platform == 128; + + var z3binName = isUnix ? "z3" : "z3.exe"; + var dafnyBinDir = System.IO.Path.GetDirectoryName(System.Reflection.Assembly.GetExecutingAssembly().Location); + var z3BinDir = System.IO.Path.Combine(dafnyBinDir, "z3", "bin"); + var z3BinPath = System.IO.Path.Combine(z3BinDir, z3binName); + + if (!System.IO.File.Exists(z3BinPath) && !isUnix) { + // This is most likely a Windows user running from source without downloading z3 + // separately; this is ok, since we vendor z3.exe. + z3BinPath = System.IO.Path.Combine(dafnyBinDir, z3binName); + } + + if (!System.IO.File.Exists(z3BinPath) && errorReporter != null) { + var tok = new Bpl.Token(1, 1) { filename = "*** " }; + errorReporter.Warning(MessageSource.Other, tok, "Could not find '{0}' in '{1}'.{2}Downloading and extracting a Z3 distribution to Dafny's 'Binaries' folder would solve this issue; for now, we'll rely on Boogie to find Z3.", + z3binName, z3BinDir, System.Environment.NewLine); + } else { + Z3ExecutablePath = z3BinPath; + } } public override void Usage() { diff --git a/Source/Dafny/Reporting.cs b/Source/Dafny/Reporting.cs index 4cfbf20e..760392ca 100644 --- a/Source/Dafny/Reporting.cs +++ b/Source/Dafny/Reporting.cs @@ -143,7 +143,7 @@ namespace Microsoft.Dafny { } public override bool Message(MessageSource source, ErrorLevel level, IToken tok, string msg) { - if (base.Message(source, level, tok, msg) && (DafnyOptions.O.PrintTooltips || level != ErrorLevel.Info)) { + if (base.Message(source, level, tok, msg) && ((DafnyOptions.O != null && DafnyOptions.O.PrintTooltips) || level != ErrorLevel.Info)) { // Extra indent added to make it easier to distinguish multiline error messages for clients that rely on the CLI msg = msg.Replace(Environment.NewLine, Environment.NewLine + " "); diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index 4b5ae8d8..c45d66fc 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -40,10 +40,11 @@ namespace Microsoft.Dafny public static int ThreadMain(string[] args) { Contract.Requires(cce.NonNullElements(args)); - + + ErrorReporter reporter = new ConsoleErrorReporter(); ExecutionEngine.printer = new DafnyConsolePrinter(); // For boogie errors - DafnyOptions.Install(new DafnyOptions()); + DafnyOptions.Install(new DafnyOptions(reporter)); ExitValue exitValue = ExitValue.VERIFIED; CommandLineOptions.Clo.RunningBoogieFromCommandLine = true; @@ -92,7 +93,7 @@ namespace Microsoft.Dafny goto END; } } - exitValue = ProcessFiles(CommandLineOptions.Clo.Files); + exitValue = ProcessFiles(CommandLineOptions.Clo.Files, reporter); END: if (CommandLineOptions.Clo.XmlSink != null) { @@ -112,7 +113,7 @@ namespace Microsoft.Dafny } - static ExitValue ProcessFiles(IList/*!*/ fileNames, bool lookForSnapshots = true, string programId = null) + static ExitValue ProcessFiles(IList/*!*/ fileNames, ErrorReporter reporter, bool lookForSnapshots = true, string programId = null) { Contract.Requires(cce.NonNullElements(fileNames)); @@ -128,7 +129,7 @@ namespace Microsoft.Dafny { Console.WriteLine(); Console.WriteLine("-------------------- {0} --------------------", f); - var ev = ProcessFiles(new List { f }, lookForSnapshots, f); + var ev = ProcessFiles(new List { f }, reporter, lookForSnapshots, f); if (exitValue != ev && ev != ExitValue.VERIFIED) { exitValue = ev; @@ -142,7 +143,7 @@ namespace Microsoft.Dafny var snapshotsByVersion = ExecutionEngine.LookForSnapshots(fileNames); foreach (var s in snapshotsByVersion) { - var ev = ProcessFiles(new List(s), false, programId); + var ev = ProcessFiles(new List(s), reporter, false, programId); if (exitValue != ev && ev != ExitValue.VERIFIED) { exitValue = ev; @@ -153,7 +154,6 @@ namespace Microsoft.Dafny using (XmlFileScope xf = new XmlFileScope(CommandLineOptions.Clo.XmlSink, fileNames[fileNames.Count-1])) { Dafny.Program dafnyProgram; - ErrorReporter reporter = new ConsoleErrorReporter(); string programName = fileNames.Count == 1 ? fileNames[0] : "the program"; string err = Dafny.Main.ParseCheck(fileNames, programName, reporter, out dafnyProgram); if (err != null) { diff --git a/Source/DafnyServer/DafnyHelper.cs b/Source/DafnyServer/DafnyHelper.cs index 3204fdb3..e54e2b48 100644 --- a/Source/DafnyServer/DafnyHelper.cs +++ b/Source/DafnyServer/DafnyHelper.cs @@ -29,18 +29,21 @@ namespace Microsoft.Dafny { class DafnyHelper { private string fname; private string source; + private string[] args; private readonly Dafny.ErrorReporter reporter; private Dafny.Program dafnyProgram; private Bpl.Program boogieProgram; - public DafnyHelper(string fname, string source) { + public DafnyHelper(string[] args, string fname, string source) { + this.args = args; this.fname = fname; this.source = source; this.reporter = new Dafny.ConsoleErrorReporter(); } public bool Verify() { + ServerUtils.ApplyArgs(args, reporter); return Parse() && Resolve() && Translate() && Boogie(); } diff --git a/Source/DafnyServer/Utilities.cs b/Source/DafnyServer/Utilities.cs index 59b3abb9..5e2c6f96 100644 --- a/Source/DafnyServer/Utilities.cs +++ b/Source/DafnyServer/Utilities.cs @@ -43,8 +43,8 @@ namespace Microsoft.Dafny { } } - internal static void ApplyArgs(string[] args) { - Dafny.DafnyOptions.Install(new Dafny.DafnyOptions()); + internal static void ApplyArgs(string[] args, ErrorReporter reporter) { + Dafny.DafnyOptions.Install(new Dafny.DafnyOptions(reporter)); Dafny.DafnyOptions.O.ProverKillTime = 15; //This is just a default; it can be overriden if (CommandLineOptions.Clo.Parse(args)) { diff --git a/Source/DafnyServer/VerificationTask.cs b/Source/DafnyServer/VerificationTask.cs index a00688b1..eb740e70 100644 --- a/Source/DafnyServer/VerificationTask.cs +++ b/Source/DafnyServer/VerificationTask.cs @@ -52,8 +52,7 @@ namespace Microsoft.Dafny { } internal void Run() { - ServerUtils.ApplyArgs(args); - new DafnyHelper(filename, ProgramSource).Verify(); + new DafnyHelper(args, filename, ProgramSource).Verify(); } } } -- cgit v1.2.3 From 2196e226c6a1c1cca5cb70b8dbdd89088751c525 Mon Sep 17 00:00:00 2001 From: Michael Lowell Roberts Date: Thu, 17 Sep 2015 15:00:02 -0700 Subject: Only print extraneous comments if asked. --- Source/Dafny/DafnyOptions.cs | 785 +++++---- Source/Dafny/Printer.cs | 4020 +++++++++++++++++++++--------------------- 2 files changed, 2403 insertions(+), 2402 deletions(-) (limited to 'Source/Dafny/DafnyOptions.cs') diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 08e53d5c..dd25e3c4 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -1,392 +1,393 @@ -using System; -using System.Collections.Generic; -using System.Linq; -using System.Text; -using System.Diagnostics.Contracts; -using Bpl = Microsoft.Boogie; - -namespace Microsoft.Dafny -{ - public class DafnyOptions : Bpl.CommandLineOptions - { - private ErrorReporter errorReporter; - - public DafnyOptions(ErrorReporter errorReporter = null) - : base("Dafny", "Dafny program verifier") { - this.errorReporter = errorReporter; - SetZ3ExecutableName(); - } - - public override string VersionNumber { - get { - return System.Diagnostics.FileVersionInfo.GetVersionInfo(System.Reflection.Assembly.GetExecutingAssembly().Location).FileVersion -#if ENABLE_IRONDAFNY - + "[IronDafny]" -#endif - ; - } - } - public override string VersionSuffix { - get { - return " version " + VersionNumber + ", Copyright (c) 2003-2015, Microsoft."; - } - } - - private static DafnyOptions clo; - public static DafnyOptions O { - get { return clo; } - } - - public static void Install(DafnyOptions options) { - Contract.Requires(options != null); - clo = options; - Bpl.CommandLineOptions.Install(options); - } - - public bool UnicodeOutput = false; - public bool DisallowSoundnessCheating = false; - public bool Dafnycc = false; - public int Induction = 3; - public int InductionHeuristic = 6; - public string DafnyPrelude = null; - public string DafnyPrintFile = null; - public enum PrintModes { Everything, NoIncludes, NoGhost }; - public PrintModes PrintMode; - public bool DafnyVerify = true; - public string DafnyPrintResolvedFile = null; - public bool Compile = true; - public bool ForceCompile = false; - public bool RunAfterCompile = false; - public bool SpillTargetCode = false; - public bool DisallowIncludes = false; - public bool DisableNLarith = false; - public string AutoReqPrintFile = null; - public bool ignoreAutoReq = false; - public bool AllowGlobals = false; - public bool CountVerificationErrors = true; - public bool Optimize = false; - public bool AutoTriggers = false; - public bool PrintTooltips = false; - public bool PrintStats = false; - public bool PrintFunctionCallGraph = false; - public bool WarnShadowing = false; - public bool IronDafny = -#if ENABLE_IRONDAFNY - true -#else - false -#endif - ; - - protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) { - var args = ps.args; // convenient synonym - - switch (name) { - case "dprelude": - if (ps.ConfirmArgumentCount(1)) { - DafnyPrelude = args[ps.i]; - } - return true; - - case "dprint": - if (ps.ConfirmArgumentCount(1)) { - DafnyPrintFile = args[ps.i]; - } - return true; - - case "printMode": - if (ps.ConfirmArgumentCount(1)) { - if (args[ps.i].Equals("Everything")) { - PrintMode = PrintModes.Everything; - } - else if (args[ps.i].Equals("NoIncludes")) - { - PrintMode = PrintModes.NoIncludes; - } - else if (args[ps.i].Equals("NoGhost")) - { - PrintMode = PrintModes.NoGhost; - } - else - { - throw new Exception("Invalid value for printMode"); - } - } - return true; - - case "rprint": - if (ps.ConfirmArgumentCount(1)) { - DafnyPrintResolvedFile = args[ps.i]; - } - return true; - - case "compile": { - int compile = 0; - if (ps.GetNumericArgument(ref compile, 4)) { - // convert option to two booleans - Compile = compile != 0; - ForceCompile = compile == 2; - RunAfterCompile = compile == 3; - } - return true; - } - - case "dafnyVerify": - { - int verify = 0; - if (ps.GetNumericArgument(ref verify, 2)) { - DafnyVerify = verify != 0; // convert to boolean - } - return true; - } - - case "spillTargetCode": { - int spill = 0; - if (ps.GetNumericArgument(ref spill, 2)) { - SpillTargetCode = spill != 0; // convert to a boolean - } - return true; - } - - case "dafnycc": - Dafnycc = true; - Induction = 0; - Compile = false; - UseAbstractInterpretation = false; // /noinfer - return true; - - case "noCheating": { - int cheat = 0; // 0 is default, allows cheating - if (ps.GetNumericArgument(ref cheat, 2)) { - DisallowSoundnessCheating = cheat == 1; - } - return true; - } - - case "induction": - ps.GetNumericArgument(ref Induction, 4); - return true; - - case "inductionHeuristic": - ps.GetNumericArgument(ref InductionHeuristic, 7); - return true; - - case "noIncludes": - DisallowIncludes = true; - return true; - - case "noNLarith": - DisableNLarith = true; - this.AddZ3Option("NL_ARITH=false"); - return true; - - case "autoReqPrint": - if (ps.ConfirmArgumentCount(1)) { - AutoReqPrintFile = args[ps.i]; - } - return true; - - case "noAutoReq": - ignoreAutoReq = true; - return true; - - case "allowGlobals": - AllowGlobals = true; - return true; - - case "stats": - PrintStats = true; - return true; - - case "funcCallGraph": - PrintFunctionCallGraph = true; - return true; - - case "warnShadowing": - WarnShadowing = true; - return true; - - case "countVerificationErrors": { - int countErrors = 1; // defaults to reporting verification errors - if (ps.GetNumericArgument(ref countErrors, 2)) { - CountVerificationErrors = countErrors == 1; - } - return true; - } - - case "printTooltips": - PrintTooltips = true; - return true; - - case "autoTriggers": { - int autoTriggers = 0; - if (ps.GetNumericArgument(ref autoTriggers, 2)) { - AutoTriggers = autoTriggers == 1; - } - return true; - } - - case "optimize": { - Optimize = true; - return true; - } - - case "noIronDafny": { - IronDafny = false; - return true; - } - - case "ironDafny": { - IronDafny = true; - return true; - } - - default: - break; - } - // not a Dafny-specific option, so defer to superclass - return base.ParseOption(name, ps); - } - - public override void ApplyDefaultOptions() { - base.ApplyDefaultOptions(); - - // expand macros in filenames, now that LogPrefix is fully determined - ExpandFilename(ref DafnyPrelude, LogPrefix, FileTimestamp); - ExpandFilename(ref DafnyPrintFile, LogPrefix, FileTimestamp); - } - - public override void AttributeUsage() { - // TODO: provide attribute help here - } - - - /// - /// Dafny comes with it's own copy of z3, to save new users the trouble of having to install extra dependency. - /// For this to work, Dafny makes the Z3ExecutablePath point to the path were Z3 is put by our release script. - /// For developers though (and people getting this from source), it's convenient to be able to run right away, - /// so we vendor a Windows version. - /// - private void SetZ3ExecutableName() { - var platform = (int)System.Environment.OSVersion.Platform; - - // http://www.mono-project.com/docs/faq/technical/ - var isUnix = platform == 4 || platform == 128; - - var z3binName = isUnix ? "z3" : "z3.exe"; - var dafnyBinDir = System.IO.Path.GetDirectoryName(System.Reflection.Assembly.GetExecutingAssembly().Location); - var z3BinDir = System.IO.Path.Combine(dafnyBinDir, "z3", "bin"); - var z3BinPath = System.IO.Path.Combine(z3BinDir, z3binName); - - if (!System.IO.File.Exists(z3BinPath) && !isUnix) { - // This is most likely a Windows user running from source without downloading z3 - // separately; this is ok, since we vendor z3.exe. - z3BinPath = System.IO.Path.Combine(dafnyBinDir, z3binName); - } - - if (!System.IO.File.Exists(z3BinPath) && errorReporter != null) { - var tok = new Bpl.Token(1, 1) { filename = "*** " }; - errorReporter.Warning(MessageSource.Other, tok, "Could not find '{0}' in '{1}'.{2}Downloading and extracting a Z3 distribution to Dafny's 'Binaries' folder would solve this issue; for now, we'll rely on Boogie to find Z3.", - z3binName, z3BinDir, System.Environment.NewLine); - } else { - Z3ExecutablePath = z3BinPath; - } - } - - public override void Usage() { - Console.WriteLine(@" ---- Dafny options --------------------------------------------------------- - - Multiple .dfy files supplied on the command line are concatenated into one - Dafny program. - - /dprelude: - choose Dafny prelude file - /dprint: - print Dafny program after parsing it - (use - as to print to console) - /printMode: - NoIncludes disables printing of {:verify false} methods incorporated via the - include mechanism, as well as datatypes and fields included from other files. - NoGhost disables printing of functions, ghost methods, and proof statements in - implementation methods. It also disables anything NoIncludes disables. - /rprint: - print Dafny program after resolving it - (use - as to print to console) - /dafnyVerify: - 0 - stop after typechecking - 1 - continue on to translation, verification, and compilation - /compile: 0 - do not compile Dafny program - 1 (default) - upon successful verification of the Dafny - program, compile Dafny program to .NET assembly - Program.exe (if the program has a Main method) or - Program.dll (othewise), where Program.dfy is the name - of the last .dfy file on the command line - 2 - always attempt to compile Dafny program to C# program - out.cs, regardless of verification outcome - 3 - if there is a Main method and there are no verification - errors, compiles program in memory (i.e., does not write - an output file) and runs it - /spillTargetCode: - 0 (default) - don't write the compiled Dafny program (but - still compile it, if /compile indicates to do so) - 1 - write the compiled Dafny program as a .cs file - /dafnycc Disable features not supported by DafnyCC - /noCheating: - 0 (default) - allow assume statements and free invariants - 1 - treat all assumptions as asserts, and drop free. - /induction: - 0 - never do induction, not even when attributes request it - 1 - only apply induction when attributes request it - 2 - apply induction as requested (by attributes) and also - for heuristically chosen quantifiers - 3 (default) - apply induction as requested, and for - heuristically chosen quantifiers and lemmas - /inductionHeuristic: - 0 - least discriminating induction heuristic (that is, lean - toward applying induction more often) - 1,2,3,4,5 - levels in between, ordered as follows as far as - how discriminating they are: 0 < 1 < 2 < (3,4) < 5 < 6 - 6 (default) - most discriminating - /noIncludes Ignore include directives - /noNLarith Reduce Z3's knowledge of non-linear arithmetic (*,/,%). - Results in more manual work, but also produces more predictable behavior. - /autoReqPrint: - Print out requirements that were automatically generated by autoReq. - /noAutoReq Ignore autoReq attributes - /allowGlobals Allow the implicit class '_default' to contain fields, instance functions, - and instance methods. These class members are declared at the module scope, - outside of explicit classes. This command-line option is provided to simplify - a transition from the behavior in the language prior to version 1.9.3, from - which point onward all functions and methods declared at the module scope are - implicitly static and fields declarations are not allowed at the module scope. - /countVerificationErrors: - 0 - If preprocessing succeeds, set exit code to 0 regardless of the number - of verification errors. - 1 (default) - If preprocessing succeeds, set exit code to the number of - verification errors. - /autoTriggers: - 0 (default) - Do not generate {:trigger} annotations for user-level quantifiers. - 1 - Add a {:trigger} to each user-level quantifier. Existing - annotations are preserved. - /optimize Produce optimized C# code, meaning: - - selects optimized C# prelude by passing - /define:DAFNY_USE_SYSTEM_COLLECTIONS_IMMUTABLE to csc.exe (requires - System.Collections.Immutable.dll in the source directory to successfully - compile). - - passes /optimize flag to csc.exe. - /stats Print interesting statistics about the Dafny files supplied. - /funcCallGraph Print out the function call graph. Format is: func,mod=callee* - /warnShadowing Emits a warning if the name of a declared variable caused another variable - to be shadowed - /ironDafny Enable experimental features needed to support Ironclad/Ironfleet. Use of - these features may cause your code to become incompatible with future - releases of Dafny. - /noIronDafny Disable Ironclad/Ironfleet features, if enabled by default. - /printTooltips - Dump additional positional information (displayed as mouse-over tooltips by - the VS plugin) to stdout as 'Info' messages. -"); - base.Usage(); // also print the Boogie options - } - } -} +using System; +using System.Collections.Generic; +using System.Linq; +using System.Text; +using System.Diagnostics.Contracts; +using Bpl = Microsoft.Boogie; + +namespace Microsoft.Dafny +{ + public class DafnyOptions : Bpl.CommandLineOptions + { + private ErrorReporter errorReporter; + + public DafnyOptions(ErrorReporter errorReporter = null) + : base("Dafny", "Dafny program verifier") { + this.errorReporter = errorReporter; + SetZ3ExecutableName(); + } + + public override string VersionNumber { + get { + return System.Diagnostics.FileVersionInfo.GetVersionInfo(System.Reflection.Assembly.GetExecutingAssembly().Location).FileVersion +#if ENABLE_IRONDAFNY + + "[IronDafny]" +#endif + ; + } + } + public override string VersionSuffix { + get { + return " version " + VersionNumber + ", Copyright (c) 2003-2015, Microsoft."; + } + } + + private static DafnyOptions clo; + public static DafnyOptions O { + get { return clo; } + } + + public static void Install(DafnyOptions options) { + Contract.Requires(options != null); + clo = options; + Bpl.CommandLineOptions.Install(options); + } + + public bool UnicodeOutput = false; + public bool DisallowSoundnessCheating = false; + public bool Dafnycc = false; + public int Induction = 3; + public int InductionHeuristic = 6; + public string DafnyPrelude = null; + public string DafnyPrintFile = null; + public enum PrintModes { Everything, NoIncludes, NoGhost }; + public PrintModes PrintMode = PrintModes.Everything; // Default to printing everything + public bool DafnyVerify = true; + public string DafnyPrintResolvedFile = null; + public bool Compile = true; + public bool ForceCompile = false; + public bool RunAfterCompile = false; + public bool SpillTargetCode = false; + public bool DisallowIncludes = false; + public bool DisableNLarith = false; + public string AutoReqPrintFile = null; + public bool ignoreAutoReq = false; + public bool AllowGlobals = false; + public bool CountVerificationErrors = true; + public bool Optimize = false; + public bool AutoTriggers = false; + public bool PrintTooltips = false; + public bool PrintStats = false; + public bool PrintFunctionCallGraph = false; + public bool WarnShadowing = false; + public bool IronDafny = +#if ENABLE_IRONDAFNY + true +#else + false +#endif + ; + + protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) { + var args = ps.args; // convenient synonym + + switch (name) { + case "dprelude": + if (ps.ConfirmArgumentCount(1)) { + DafnyPrelude = args[ps.i]; + } + return true; + + case "dprint": + if (ps.ConfirmArgumentCount(1)) { + DafnyPrintFile = args[ps.i]; + } + return true; + + case "printMode": + if (ps.ConfirmArgumentCount(1)) { + if (args[ps.i].Equals("Everything")) { + PrintMode = PrintModes.Everything; + } + else if (args[ps.i].Equals("NoIncludes")) + { + PrintMode = PrintModes.NoIncludes; + } + else if (args[ps.i].Equals("NoGhost")) + { + PrintMode = PrintModes.NoGhost; + } + else + { + throw new Exception("Invalid value for printMode"); + } + } + return true; + + case "rprint": + if (ps.ConfirmArgumentCount(1)) { + DafnyPrintResolvedFile = args[ps.i]; + } + return true; + + case "compile": { + int compile = 0; + if (ps.GetNumericArgument(ref compile, 4)) { + // convert option to two booleans + Compile = compile != 0; + ForceCompile = compile == 2; + RunAfterCompile = compile == 3; + } + return true; + } + + case "dafnyVerify": + { + int verify = 0; + if (ps.GetNumericArgument(ref verify, 2)) { + DafnyVerify = verify != 0; // convert to boolean + } + return true; + } + + case "spillTargetCode": { + int spill = 0; + if (ps.GetNumericArgument(ref spill, 2)) { + SpillTargetCode = spill != 0; // convert to a boolean + } + return true; + } + + case "dafnycc": + Dafnycc = true; + Induction = 0; + Compile = false; + UseAbstractInterpretation = false; // /noinfer + return true; + + case "noCheating": { + int cheat = 0; // 0 is default, allows cheating + if (ps.GetNumericArgument(ref cheat, 2)) { + DisallowSoundnessCheating = cheat == 1; + } + return true; + } + + case "induction": + ps.GetNumericArgument(ref Induction, 4); + return true; + + case "inductionHeuristic": + ps.GetNumericArgument(ref InductionHeuristic, 7); + return true; + + case "noIncludes": + DisallowIncludes = true; + return true; + + case "noNLarith": + DisableNLarith = true; + this.AddZ3Option("NL_ARITH=false"); + return true; + + case "autoReqPrint": + if (ps.ConfirmArgumentCount(1)) { + AutoReqPrintFile = args[ps.i]; + } + return true; + + case "noAutoReq": + ignoreAutoReq = true; + return true; + + case "allowGlobals": + AllowGlobals = true; + return true; + + case "stats": + PrintStats = true; + return true; + + case "funcCallGraph": + PrintFunctionCallGraph = true; + return true; + + case "warnShadowing": + WarnShadowing = true; + return true; + + case "countVerificationErrors": { + int countErrors = 1; // defaults to reporting verification errors + if (ps.GetNumericArgument(ref countErrors, 2)) { + CountVerificationErrors = countErrors == 1; + } + return true; + } + + case "printTooltips": + PrintTooltips = true; + return true; + + case "autoTriggers": { + int autoTriggers = 0; + if (ps.GetNumericArgument(ref autoTriggers, 2)) { + AutoTriggers = autoTriggers == 1; + } + return true; + } + + case "optimize": { + Optimize = true; + return true; + } + + case "noIronDafny": { + IronDafny = false; + return true; + } + + case "ironDafny": { + IronDafny = true; + return true; + } + + default: + break; + } + // not a Dafny-specific option, so defer to superclass + return base.ParseOption(name, ps); + } + + public override void ApplyDefaultOptions() { + base.ApplyDefaultOptions(); + + // expand macros in filenames, now that LogPrefix is fully determined + ExpandFilename(ref DafnyPrelude, LogPrefix, FileTimestamp); + ExpandFilename(ref DafnyPrintFile, LogPrefix, FileTimestamp); + } + + public override void AttributeUsage() { + // TODO: provide attribute help here + } + + + /// + /// Dafny comes with it's own copy of z3, to save new users the trouble of having to install extra dependency. + /// For this to work, Dafny makes the Z3ExecutablePath point to the path were Z3 is put by our release script. + /// For developers though (and people getting this from source), it's convenient to be able to run right away, + /// so we vendor a Windows version. + /// + private void SetZ3ExecutableName() { + var platform = (int)System.Environment.OSVersion.Platform; + + // http://www.mono-project.com/docs/faq/technical/ + var isUnix = platform == 4 || platform == 128; + + var z3binName = isUnix ? "z3" : "z3.exe"; + var dafnyBinDir = System.IO.Path.GetDirectoryName(System.Reflection.Assembly.GetExecutingAssembly().Location); + var z3BinDir = System.IO.Path.Combine(dafnyBinDir, "z3", "bin"); + var z3BinPath = System.IO.Path.Combine(z3BinDir, z3binName); + + if (!System.IO.File.Exists(z3BinPath) && !isUnix) { + // This is most likely a Windows user running from source without downloading z3 + // separately; this is ok, since we vendor z3.exe. + z3BinPath = System.IO.Path.Combine(dafnyBinDir, z3binName); + } + + if (!System.IO.File.Exists(z3BinPath) && errorReporter != null) { + var tok = new Bpl.Token(1, 1) { filename = "*** " }; + errorReporter.Warning(MessageSource.Other, tok, "Could not find '{0}' in '{1}'.{2}Downloading and extracting a Z3 distribution to Dafny's 'Binaries' folder would solve this issue; for now, we'll rely on Boogie to find Z3.", + z3binName, z3BinDir, System.Environment.NewLine); + } else { + Z3ExecutablePath = z3BinPath; + } + } + + public override void Usage() { + Console.WriteLine(@" ---- Dafny options --------------------------------------------------------- + + Multiple .dfy files supplied on the command line are concatenated into one + Dafny program. + + /dprelude: + choose Dafny prelude file + /dprint: + print Dafny program after parsing it + (use - as to print to console) + /printMode: + Everything is the default. + NoIncludes disables printing of {:verify false} methods incorporated via the + include mechanism, as well as datatypes and fields included from other files. + NoGhost disables printing of functions, ghost methods, and proof statements in + implementation methods. It also disables anything NoIncludes disables. + /rprint: + print Dafny program after resolving it + (use - as to print to console) + /dafnyVerify: + 0 - stop after typechecking + 1 - continue on to translation, verification, and compilation + /compile: 0 - do not compile Dafny program + 1 (default) - upon successful verification of the Dafny + program, compile Dafny program to .NET assembly + Program.exe (if the program has a Main method) or + Program.dll (othewise), where Program.dfy is the name + of the last .dfy file on the command line + 2 - always attempt to compile Dafny program to C# program + out.cs, regardless of verification outcome + 3 - if there is a Main method and there are no verification + errors, compiles program in memory (i.e., does not write + an output file) and runs it + /spillTargetCode: + 0 (default) - don't write the compiled Dafny program (but + still compile it, if /compile indicates to do so) + 1 - write the compiled Dafny program as a .cs file + /dafnycc Disable features not supported by DafnyCC + /noCheating: + 0 (default) - allow assume statements and free invariants + 1 - treat all assumptions as asserts, and drop free. + /induction: + 0 - never do induction, not even when attributes request it + 1 - only apply induction when attributes request it + 2 - apply induction as requested (by attributes) and also + for heuristically chosen quantifiers + 3 (default) - apply induction as requested, and for + heuristically chosen quantifiers and lemmas + /inductionHeuristic: + 0 - least discriminating induction heuristic (that is, lean + toward applying induction more often) + 1,2,3,4,5 - levels in between, ordered as follows as far as + how discriminating they are: 0 < 1 < 2 < (3,4) < 5 < 6 + 6 (default) - most discriminating + /noIncludes Ignore include directives + /noNLarith Reduce Z3's knowledge of non-linear arithmetic (*,/,%). + Results in more manual work, but also produces more predictable behavior. + /autoReqPrint: + Print out requirements that were automatically generated by autoReq. + /noAutoReq Ignore autoReq attributes + /allowGlobals Allow the implicit class '_default' to contain fields, instance functions, + and instance methods. These class members are declared at the module scope, + outside of explicit classes. This command-line option is provided to simplify + a transition from the behavior in the language prior to version 1.9.3, from + which point onward all functions and methods declared at the module scope are + implicitly static and fields declarations are not allowed at the module scope. + /countVerificationErrors: + 0 - If preprocessing succeeds, set exit code to 0 regardless of the number + of verification errors. + 1 (default) - If preprocessing succeeds, set exit code to the number of + verification errors. + /autoTriggers: + 0 (default) - Do not generate {:trigger} annotations for user-level quantifiers. + 1 - Add a {:trigger} to each user-level quantifier. Existing + annotations are preserved. + /optimize Produce optimized C# code, meaning: + - selects optimized C# prelude by passing + /define:DAFNY_USE_SYSTEM_COLLECTIONS_IMMUTABLE to csc.exe (requires + System.Collections.Immutable.dll in the source directory to successfully + compile). + - passes /optimize flag to csc.exe. + /stats Print interesting statistics about the Dafny files supplied. + /funcCallGraph Print out the function call graph. Format is: func,mod=callee* + /warnShadowing Emits a warning if the name of a declared variable caused another variable + to be shadowed + /ironDafny Enable experimental features needed to support Ironclad/Ironfleet. Use of + these features may cause your code to become incompatible with future + releases of Dafny. + /noIronDafny Disable Ironclad/Ironfleet features, if enabled by default. + /printTooltips + Dump additional positional information (displayed as mouse-over tooltips by + the VS plugin) to stdout as 'Info' messages. +"); + base.Usage(); // also print the Boogie options + } + } +} diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index ce8b54bb..e242c8bb 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -1,2010 +1,2010 @@ -//----------------------------------------------------------------------------- -// -// Copyright (C) Microsoft Corporation. All Rights Reserved. -// -//----------------------------------------------------------------------------- -using System; -using System.IO; -using System.Collections.Generic; -using System.Diagnostics.Contracts; -using System.Numerics; -using System.Linq; -using Bpl = Microsoft.Boogie; - -namespace Microsoft.Dafny { - public class Printer { - TextWriter wr; - DafnyOptions.PrintModes printMode; - - [ContractInvariantMethod] - void ObjectInvariant() - { - Contract.Invariant(wr!=null); - } - - public Printer(TextWriter wr, DafnyOptions.PrintModes printMode = DafnyOptions.PrintModes.Everything) { - Contract.Requires(wr != null); - this.wr = wr; - this.printMode = printMode; - } - - public static string ExprToString(Expression expr) - { - Contract.Requires(expr != null); - using (var wr = new System.IO.StringWriter()) { - var pr = new Printer(wr); - pr.PrintExpression(expr, false); - return wr.ToString(); - } - } - - public static string GuardToString(Expression expr) { - using (var wr = new System.IO.StringWriter()) { - var pr = new Printer(wr); - pr.PrintGuard(expr); - return wr.ToString(); - } - } - - public static string ExtendedExprToString(Expression expr) { - Contract.Requires(expr != null); - using (var wr = new System.IO.StringWriter()) { - var pr = new Printer(wr); - pr.PrintExtendedExpr(expr, 0, true, false); - return wr.ToString(); - } - } - - public static string FrameExprListToString(List fexprs) { - Contract.Requires(fexprs != null); - using (var wr = new System.IO.StringWriter()) { - var pr = new Printer(wr); - pr.PrintFrameExpressionList(fexprs); - return wr.ToString(); - } - } - - public static string StatementToString(Statement stmt) { - Contract.Requires(stmt != null); - using (var wr = new System.IO.StringWriter()) { - var pr = new Printer(wr); - pr.PrintStatement(stmt, 0); - return ToStringWithoutNewline(wr); - } - } - - public static string IteratorClassToString(IteratorDecl iter) { - Contract.Requires(iter != null); - using (var wr = new System.IO.StringWriter()) { - var pr = new Printer(wr); - pr.PrintIteratorClass(iter, 0, null); - return ToStringWithoutNewline(wr); - } - } - - public static string IteratorSignatureToString(IteratorDecl iter) { - Contract.Requires(iter != null); - using (var wr = new System.IO.StringWriter()) { - var pr = new Printer(wr); - pr.PrintIteratorSignature(iter, 0); - return ToStringWithoutNewline(wr); - } - } - - public static string FunctionSignatureToString(Function f) { - Contract.Requires(f != null); - using (var wr = new System.IO.StringWriter()) { - var pr = new Printer(wr); - pr.PrintFunction(f, 0, true); - return ToStringWithoutNewline(wr); - } - } - - public static string MethodSignatureToString(Method m) { - Contract.Requires(m != null); - using (var wr = new System.IO.StringWriter()) { - var pr = new Printer(wr); - pr.PrintMethod(m, 0, true); - return ToStringWithoutNewline(wr); - } - } - - public static string OneAttributeToString(Attributes a, string nameSubstitution = null) { - Contract.Requires(a != null); - using (var wr = new System.IO.StringWriter()) { - var pr = new Printer(wr); - pr.PrintOneAttribute(a, nameSubstitution); - return ToStringWithoutNewline(wr); - } - } - - public static string ToStringWithoutNewline(System.IO.StringWriter wr) { - Contract.Requires(wr != null); - var sb = wr.GetStringBuilder(); - var len = sb.Length; - while (len > 0 && (sb[len - 1] == '\n' || sb[len - 1] == '\r')) { - len--; - } - return sb.ToString(0, len); - } - - public void PrintProgram(Program prog) { - Contract.Requires(prog != null); - if (Bpl.CommandLineOptions.Clo.ShowEnv != Bpl.CommandLineOptions.ShowEnvironment.Never) { - wr.WriteLine("// " + Bpl.CommandLineOptions.Clo.Version); - wr.WriteLine("// " + Bpl.CommandLineOptions.Clo.Environment); - } - wr.WriteLine("// {0}", prog.Name); - if (DafnyOptions.O.DafnyPrintResolvedFile != null) { - wr.WriteLine(); - wr.WriteLine("/*"); - PrintModuleDefinition(prog.BuiltIns.SystemModule, 0, Path.GetFullPath(DafnyOptions.O.DafnyPrintResolvedFile)); - wr.WriteLine("*/"); - } - wr.WriteLine(); - PrintCallGraph(prog.DefaultModuleDef, 0); - PrintTopLevelDecls(prog.DefaultModuleDef.TopLevelDecls, 0, Path.GetFullPath(prog.FullName)); - wr.Flush(); - } - - public void PrintCallGraph(ModuleDefinition module, int indent) { - Contract.Requires(module != null); - Contract.Requires(0 <= indent); - if (DafnyOptions.O.DafnyPrintResolvedFile != null) { - // print call graph - Indent(indent); wr.WriteLine("/* CALL GRAPH for module {0}:", module.Name); - var SCCs = module.CallGraph.TopologicallySortedComponents(); - SCCs.Reverse(); - foreach (var clbl in SCCs) { - Indent(indent); wr.WriteLine(" * SCC at height {0}:", module.CallGraph.GetSCCRepresentativeId(clbl)); - var r = module.CallGraph.GetSCC(clbl); - foreach (var m in r) { - Indent(indent); wr.WriteLine(" * {0}", m.NameRelativeToModule); - } - } - Indent(indent); wr.WriteLine(" */"); - } - } - - public void PrintTopLevelDecls(List decls, int indent, string fileBeingPrinted) { - Contract.Requires(decls!= null); - int i = 0; - foreach (TopLevelDecl d in decls) { - Contract.Assert(d != null); - if (PrintModeSkipGeneral(d.tok, fileBeingPrinted)) { continue; } - if (d is OpaqueTypeDecl) { - var at = (OpaqueTypeDecl)d; - if (i++ != 0) { wr.WriteLine(); } - Indent(indent); - PrintClassMethodHelper("type", at.Attributes, at.Name, new List()); - wr.Write(EqualitySupportSuffix(at.EqualitySupport)); - wr.WriteLine(); - } else if (d is NewtypeDecl) { - var dd = (NewtypeDecl)d; - if (i++ != 0) { wr.WriteLine(); } - Indent(indent); - PrintClassMethodHelper("newtype", dd.Attributes, dd.Name, new List()); - wr.Write(" = "); - if (dd.Var == null) { - PrintType(dd.BaseType); - } else { - wr.Write(dd.Var.DisplayName); - if (!(dd.Var.Type is TypeProxy) || DafnyOptions.O.DafnyPrintResolvedFile != null) { - wr.Write(": "); - PrintType(dd.BaseType); - } - wr.Write(" | "); - PrintExpression(dd.Constraint, true); - } - wr.WriteLine(); - } else if (d is TypeSynonymDecl) { - var syn = (TypeSynonymDecl)d; - if (i++ != 0) { wr.WriteLine(); } - Indent(indent); - PrintClassMethodHelper("type", syn.Attributes, syn.Name, syn.TypeArgs); - wr.Write(" = "); - PrintType(syn.Rhs); - wr.WriteLine(); - } else if (d is DatatypeDecl) { - if (i++ != 0) { wr.WriteLine(); } - PrintDatatype((DatatypeDecl)d, indent); - } else if (d is IteratorDecl) { - var iter = (IteratorDecl)d; - PrintIteratorSignature(iter, indent); - - if (iter.Body != null) { - Indent(indent); - PrintStatement(iter.Body, indent); - wr.WriteLine(); - } - - if (DafnyOptions.O.DafnyPrintResolvedFile != null) { - // also print the members that were created as part of the interpretation of the iterator - Contract.Assert(iter.Members.Count != 0); // filled in during resolution - wr.WriteLine("/*---------- iterator members ----------"); - PrintIteratorClass(iter, indent, fileBeingPrinted); - wr.WriteLine("---------- iterator members ----------*/"); - } - - } else if (d is ClassDecl) { - ClassDecl cl = (ClassDecl)d; - if (!cl.IsDefaultClass) { - if (i++ != 0) { wr.WriteLine(); } - PrintClass(cl, indent, fileBeingPrinted); - } else if (cl.Members.Count == 0) { - // print nothing - } else { - if (i++ != 0) { wr.WriteLine(); } - PrintMembers(cl.Members, indent, fileBeingPrinted); - } - - } else if (d is ModuleDecl) { - wr.WriteLine(); - Indent(indent); - if (d is LiteralModuleDecl) { - ModuleDefinition module = ((LiteralModuleDecl)d).ModuleDef; - PrintModuleDefinition(module, indent, fileBeingPrinted); - } else if (d is AliasModuleDecl) { - wr.Write("import"); if (((AliasModuleDecl)d).Opened) wr.Write(" opened"); - wr.Write(" {0} ", ((AliasModuleDecl)d).Name); - wr.WriteLine("= {0}", Util.Comma(".", ((AliasModuleDecl)d).Path, id => id.val)); - } else if (d is ModuleFacadeDecl) { - wr.Write("import"); if (((ModuleFacadeDecl)d).Opened) wr.Write(" opened"); - wr.Write(" {0} ", ((ModuleFacadeDecl)d).Name); - wr.WriteLine("as {0}", Util.Comma(".", ((ModuleFacadeDecl)d).Path, id => id.val)); - } - - } else { - Contract.Assert(false); // unexpected TopLevelDecl - } - } - } - - void PrintModuleDefinition(ModuleDefinition module, int indent, string fileBeingPrinted) { - Contract.Requires(module != null); - Contract.Requires(0 <= indent); - if (module.IsAbstract) { - wr.Write("abstract "); - } - wr.Write("module"); - PrintAttributes(module.Attributes); - wr.Write(" {0} ", module.Name); - if (module.RefinementBaseName != null) { - wr.Write("refines {0} ", Util.Comma(".", module.RefinementBaseName, id => id.val)); - } - if (module.TopLevelDecls.Count == 0) { - wr.WriteLine("{ }"); - } else { - wr.WriteLine("{"); - PrintCallGraph(module, indent + IndentAmount); - PrintTopLevelDecls(module.TopLevelDecls, indent + IndentAmount, fileBeingPrinted); - Indent(indent); - wr.WriteLine("}"); - } - } - - void PrintIteratorSignature(IteratorDecl iter, int indent) { - Indent(indent); - PrintClassMethodHelper("iterator", iter.Attributes, iter.Name, iter.TypeArgs); - if (iter.SignatureIsOmitted) { - wr.WriteLine(" ..."); - } else { - PrintFormals(iter.Ins); - if (iter.Outs.Count != 0) { - if (iter.Ins.Count + iter.Outs.Count <= 3) { - wr.Write(" yields "); - } else { - wr.WriteLine(); - Indent(indent + 2 * IndentAmount); - wr.Write("yields "); - } - PrintFormals(iter.Outs); - } - wr.WriteLine(); - } - - int ind = indent + IndentAmount; - PrintSpec("requires", iter.Requires, ind); - if (iter.Reads.Expressions != null) { - PrintFrameSpecLine("reads", iter.Reads.Expressions, ind, iter.Reads.HasAttributes() ? iter.Reads.Attributes : null); - } - if (iter.Modifies.Expressions != null) { - PrintFrameSpecLine("modifies", iter.Modifies.Expressions, ind, iter.Modifies.HasAttributes() ? iter.Modifies.Attributes : null); - } - PrintSpec("yield requires", iter.YieldRequires, ind); - PrintSpec("yield ensures", iter.YieldEnsures, ind); - PrintSpec("ensures", iter.Ensures, ind); - PrintDecreasesSpec(iter.Decreases, ind); - } - - private void PrintIteratorClass(IteratorDecl iter, int indent, string fileBeingPrinted) { - PrintClassMethodHelper("class", null, iter.Name, iter.TypeArgs); - wr.WriteLine(" {"); - PrintMembers(iter.Members, indent + IndentAmount, fileBeingPrinted); - Indent(indent); wr.WriteLine("}"); - } - - public void PrintClass(ClassDecl c, int indent, string fileBeingPrinted) { - Contract.Requires(c != null); - Indent(indent); - PrintClassMethodHelper((c is TraitDecl) ? "trait" : "class", c.Attributes, c.Name, c.TypeArgs); - string sep = " extends "; - foreach (var trait in c.TraitsTyp) { - wr.Write(sep); - PrintType(trait); - sep = ", "; - } - if (c.Members.Count == 0) { - wr.WriteLine(" { }"); - } else { - wr.WriteLine(" {"); - PrintMembers(c.Members, indent + IndentAmount, fileBeingPrinted); - Indent(indent); - wr.WriteLine("}"); - } - } - - public void PrintMembers(List members, int indent, string fileBeingPrinted) - { - Contract.Requires(members != null); - - int state = 0; // 0 - no members yet; 1 - previous member was a field; 2 - previous member was non-field - foreach (MemberDecl m in members) { - if (PrintModeSkipGeneral(m.tok, fileBeingPrinted)) { continue; } - if (m is Method) { - if (state != 0) { wr.WriteLine(); } - PrintMethod((Method)m, indent, false); - var com = m as FixpointLemma; - if (com != null && com.PrefixLemma != null) { - Indent(indent); wr.WriteLine("/***"); - PrintMethod(com.PrefixLemma, indent, false); - Indent(indent); wr.WriteLine("***/"); - } - state = 2; - } else if (m is Field) { - if (state == 2) { wr.WriteLine(); } - PrintField((Field)m, indent); - state = 1; - } else if (m is Function) { - if (state != 0) { wr.WriteLine(); } - PrintFunction((Function)m, indent, false); - var fixp = m as FixpointPredicate; - if (fixp != null && fixp.PrefixPredicate != null) { - Indent(indent); wr.WriteLine("/***"); - PrintFunction(fixp.PrefixPredicate, indent, false); - Indent(indent); wr.WriteLine("***/"); - } - state = 2; - } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected member - } - } - } - - /// - /// Prints no space before "kind", but does print a space before "attrs" and "name". - /// - void PrintClassMethodHelper(string kind, Attributes attrs, string name, List typeArgs) { - Contract.Requires(kind != null); - Contract.Requires(name != null); - Contract.Requires(typeArgs != null); - if (kind.Length != 0) { - wr.Write(kind); - } - - PrintAttributes(attrs); - - wr.Write(" {0}", name); - PrintTypeParams(typeArgs); - } - - private void PrintTypeParams(List typeArgs) { - Contract.Requires(typeArgs != null); - if (typeArgs.Count != 0) { - wr.Write("<" + - Util.Comma(", ", typeArgs, - tp => tp.Name + EqualitySupportSuffix(tp.EqualitySupport)) - + ">"); - } - } - - private void PrintTypeInstantiation(List typeArgs) { - Contract.Requires(typeArgs == null || typeArgs.Count != 0); - if (typeArgs != null) { - wr.Write("<{0}>", Util.Comma(",", typeArgs, ty => ty.ToString())); - } - } - - public void PrintDatatype(DatatypeDecl dt, int indent) { - Contract.Requires(dt != null); - Indent(indent); - PrintClassMethodHelper(dt is IndDatatypeDecl ? "datatype" : "codatatype", dt.Attributes, dt.Name, dt.TypeArgs); - wr.Write(" ="); - string sep = ""; - foreach (DatatypeCtor ctor in dt.Ctors) { - wr.Write(sep); - PrintClassMethodHelper("", ctor.Attributes, ctor.Name, new List()); - if (ctor.Formals.Count != 0) { - PrintFormals(ctor.Formals); - } - sep = " |"; - } - wr.WriteLine(); - } - - /// - /// Prints a space before each attribute. - /// - public void PrintAttributes(Attributes a) { - if (a != null) { - PrintAttributes(a.Prev); - wr.Write(" "); - PrintOneAttribute(a); - } - } - public void PrintOneAttribute(Attributes a, string nameSubstitution = null) { - Contract.Requires(a != null); - var name = nameSubstitution ?? a.Name; - var usAttribute = name.StartsWith("_"); - wr.Write("{1}{{:{0}", name, usAttribute ? "/*" : ""); - if (a.Args != null) { - PrintAttributeArgs(a.Args, false); - } - wr.Write("}}{0}", usAttribute ? "*/" : ""); - } - - public void PrintAttributeArgs(List args, bool isFollowedBySemicolon) { - Contract.Requires(args != null); - string prefix = " "; - foreach (var arg in args) { - Contract.Assert(arg != null); - wr.Write(prefix); - prefix = ", "; - PrintExpression(arg, isFollowedBySemicolon); - } - } - - public void PrintField(Field field, int indent) { - Contract.Requires(field != null); - Indent(indent); - if (field.IsGhost) { - wr.Write("ghost "); - } - wr.Write("var"); - PrintAttributes(field.Attributes); - wr.Write(" {0}: ", field.Name); - PrintType(field.Type); - if (field.IsUserMutable) { - // nothing more to say - } else if (field.IsMutable) { - wr.Write(" // non-assignable"); - } else { - wr.Write(" // immutable"); - } - wr.WriteLine(); - } - - public void PrintFunction(Function f, int indent, bool printSignatureOnly) { - Contract.Requires(f != null); - - if (PrintModeSkipFunctionOrMethod(f.IsGhost, f.Attributes, f.Name)) { return; } - var isPredicate = f is Predicate || f is PrefixPredicate; - Indent(indent); - string k = isPredicate ? "predicate" : f is InductivePredicate ? "inductive predicate" : f is CoPredicate ? "copredicate" : "function"; - if (f.IsProtected) { k = "protected " + k; } - if (f.HasStaticKeyword) { k = "static " + k; } - if (!f.IsGhost) { k += " method"; } - PrintClassMethodHelper(k, f.Attributes, f.Name, f.TypeArgs); - if (f.SignatureIsOmitted) { - wr.WriteLine(" ..."); - } else { - PrintFormals(f.Formals, f.Name); - if (!isPredicate) { - wr.Write(": "); - PrintType(f.ResultType); - } - wr.WriteLine(); - } - - int ind = indent + IndentAmount; - PrintSpec("requires", f.Req, ind); - PrintFrameSpecLine("reads", f.Reads, ind, null); - PrintSpec("ensures", f.Ens, ind); - PrintDecreasesSpec(f.Decreases, ind); - if (f.Body != null && !printSignatureOnly) { - Indent(indent); - wr.WriteLine("{"); - PrintExtendedExpr(f.Body, ind, true, false); - Indent(indent); - wr.WriteLine("}"); - } - } - - // ----------------------------- PrintMethod ----------------------------- - - const int IndentAmount = 2; // The amount of indent for each new scope - const string BunchaSpaces = " "; - void Indent(int amount) - { - Contract.Requires(0 <= amount); - - while (0 < amount) { - wr.Write(BunchaSpaces.Substring(0, amount)); - amount -= BunchaSpaces.Length; - } - } - - private bool PrintModeSkipFunctionOrMethod(bool IsGhost, Attributes attributes, string name) - { - if (printMode == DafnyOptions.PrintModes.NoGhost && IsGhost) - { return true; } - if (printMode == DafnyOptions.PrintModes.NoIncludes || printMode == DafnyOptions.PrintModes.NoGhost) - { - bool verify = true; - if (Attributes.ContainsBool(attributes, "verify", ref verify) && !verify) - { return true; } - if (name.Contains("INTERNAL") || name.StartsWith("reveal_")) - { return true; } - } - return false; - } - - private bool PrintModeSkipGeneral(Bpl.IToken tok, string fileBeingPrinted) - { - return (printMode == DafnyOptions.PrintModes.NoIncludes || printMode == DafnyOptions.PrintModes.NoGhost) - && (tok.filename != null && fileBeingPrinted != null && Path.GetFullPath(tok.filename) != fileBeingPrinted); - } - - public void PrintMethod(Method method, int indent, bool printSignatureOnly) { - Contract.Requires(method != null); - - if (PrintModeSkipFunctionOrMethod(method.IsGhost, method.Attributes, method.Name)) { return; } - Indent(indent); - string k = method is Constructor ? "constructor" : - method is InductiveLemma ? "inductive lemma" : - method is CoLemma ? "colemma" : - method is Lemma ? "lemma" : - "method"; - if (method.HasStaticKeyword) { k = "static " + k; } - if (method.IsGhost && !(method is Lemma) && !(method is FixpointLemma)) { k = "ghost " + k; } - string nm = method is Constructor && !((Constructor)method).HasName ? "" : method.Name; - PrintClassMethodHelper(k, method.Attributes, nm, method.TypeArgs); - if (method.SignatureIsOmitted) { - wr.WriteLine(" ..."); - } else { - PrintFormals(method.Ins, method.Name); - if (method.Outs.Count != 0) { - if (method.Ins.Count + method.Outs.Count <= 3) { - wr.Write(" returns "); - } else { - wr.WriteLine(); - Indent(indent + 2 * IndentAmount); - wr.Write("returns "); - } - PrintFormals(method.Outs); - } - wr.WriteLine(); - } - - int ind = indent + IndentAmount; - PrintSpec("requires", method.Req, ind); - if (method.Mod.Expressions != null) - { - PrintFrameSpecLine("modifies", method.Mod.Expressions, ind, method.Mod.HasAttributes() ? method.Mod.Attributes : null); - } - PrintSpec("ensures", method.Ens, ind); - PrintDecreasesSpec(method.Decreases, ind); - - if (method.Body != null && !printSignatureOnly) { - Indent(indent); - PrintStatement(method.Body, indent); - wr.WriteLine(); - } - } - - internal void PrintFormals(List ff, string name = null) { - Contract.Requires(ff != null); - if (name != null && name.EndsWith("#")) { - wr.Write("["); - PrintFormal(ff[0]); - wr.Write("]"); - ff = new List(ff.Skip(1)); - } - wr.Write("("); - string sep = ""; - foreach (Formal f in ff) { - Contract.Assert(f != null); - wr.Write(sep); - sep = ", "; - PrintFormal(f); - } - wr.Write(")"); - } - - void PrintFormal(Formal f) { - Contract.Requires(f != null); - if (f.IsGhost) { - wr.Write("ghost "); - } - if (f.HasName) { - wr.Write("{0}: ", f.DisplayName); - } - PrintType(f.Type); - } - - internal void PrintSpec(string kind, List ee, int indent) { - Contract.Requires(kind != null); - Contract.Requires(ee != null); - foreach (Expression e in ee) { - Contract.Assert(e != null); - Indent(indent); - wr.Write("{0} ", kind); - PrintExpression(e, true); - wr.WriteLine(); - } - } - - internal void PrintDecreasesSpec(Specification decs, int indent, bool newLine = true) { - Contract.Requires(decs != null); - if (printMode == DafnyOptions.PrintModes.NoGhost) { return; } - if (decs.Expressions != null && decs.Expressions.Count != 0) { - Indent(indent); - wr.Write("decreases"); - if (decs.HasAttributes()) - { - PrintAttributes(decs.Attributes); - } - wr.Write(" "); - PrintExpressionList(decs.Expressions, true); - if (newLine) { - wr.WriteLine(); - } else { - wr.Write(" "); - } - } - } - - internal void PrintFrameSpecLine(string kind, List ee, int indent, Attributes attrs, bool newLine = true) { - Contract.Requires(kind != null); - Contract.Requires(cce.NonNullElements(ee)); - if (ee != null && ee.Count != 0) { - Indent(indent); - wr.Write("{0}", kind); - if (attrs != null) { - PrintAttributes(attrs); - } - wr.Write(" "); - PrintFrameExpressionList(ee); - if (newLine) { - wr.WriteLine(); - } else { - wr.Write(" "); - } - } - } - - internal void PrintSpec(string kind, List ee, int indent, bool newLine = true) { - Contract.Requires(kind != null); - Contract.Requires(ee != null); - if (printMode == DafnyOptions.PrintModes.NoGhost) { return; } - foreach (MaybeFreeExpression e in ee) - { - Contract.Assert(e != null); - Indent(indent); - wr.Write("{0}{1}", e.IsFree ? "free " : "", kind); - - if (e.HasAttributes()) - { - PrintAttributes(e.Attributes); - } - - wr.Write(" "); - PrintExpression(e.E, true); - if (newLine) { - wr.WriteLine(); - } else { - wr.Write(" "); - } - } - } - - // ----------------------------- PrintType ----------------------------- - - public void PrintType(Type ty) { - Contract.Requires(ty != null); - wr.Write(ty.ToString()); - } - - public void PrintType(string prefix, Type ty) { - Contract.Requires(prefix != null); - Contract.Requires(ty != null); - string s = ty.ToString(); - if (s != "?") { - wr.Write("{0}{1}", prefix, s); - } - } - - string EqualitySupportSuffix(TypeParameter.EqualitySupportValue es) { - if (es == TypeParameter.EqualitySupportValue.Required || - (es == TypeParameter.EqualitySupportValue.InferredRequired && DafnyOptions.O.DafnyPrintResolvedFile != null)) { - return "(==)"; - } else { - return ""; - } - } - - // ----------------------------- PrintStatement ----------------------------- - - /// - /// Prints from the current position of the current line. - /// If the statement requires several lines, subsequent lines are indented at "indent". - /// No newline is printed after the statement. - /// - public void PrintStatement(Statement stmt, int indent) { - Contract.Requires(stmt != null); - - if (stmt.IsGhost && printMode == DafnyOptions.PrintModes.NoGhost) { return; } - for (LList