diff options
| author |  rustanleino <unknown> | 2010-05-06 20:28:29 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-05-06 20:28:29 +0000 |
| commit | a2f70f46e1a4dfb513df45657178399269cec67d (patch) | |
| tree | bacc4d411170492170faa80fd619a009da602650 | |
| parent | e9c25e761ad3a5e31e077f7bb595bfc10618c2bb (diff) | |
Dafny:
* First crack at a compiler (/compile:1 writes out.cs, if Dafny program verifies)
* Added "print" statement (to make running compiled programs more interesting)
* Changed name of default class from $default to _default
Boogie:
* Included "lambda" as a keyword in emacs and latex style files
28 files changed, 1938 insertions, 474 deletions
diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs new file mode 100644 index 00000000..982683b9 --- /dev/null +++ b/Binaries/DafnyRuntime.cs @@ -0,0 +1,221 @@ +using System.Numerics;
+using System.Collections.Generic;
+
+namespace Dafny
+{
+ public class Set<T>
+ {
+ Dictionary<T, bool> dict;
+ public Set() { }
+ Set(Dictionary<T, bool> d) {
+ dict = d;
+ }
+ public static Set<T> Empty {
+ get {
+ return new Set<T>(new Dictionary<T, bool>(0));
+ }
+ }
+ public static Set<T> FromElements(params T[] values) {
+ Dictionary<T, bool> d = new Dictionary<T, bool>(values.Length);
+ foreach (T t in values)
+ d.Add(t, true);
+ return new Set<T>(d);
+ }
+ public IEnumerable<T> Elements {
+ get {
+ return dict.Keys;
+ }
+ }
+ public bool Equals(Set<T> other) {
+ return dict.Count == other.dict.Count && IsSubsetOf(other);
+ }
+ public override bool Equals(object other) {
+ return other is Set<T> && Equals((Set<T>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsProperSubsetOf(Set<T> other) {
+ return dict.Count < other.dict.Count && IsSubsetOf(other);
+ }
+ public bool IsSubsetOf(Set<T> other) {
+ if (other.dict.Count < dict.Count)
+ return false;
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool IsSupersetOf(Set<T> other) {
+ return other.IsSubsetOf(this);
+ }
+ public bool IsProperSupersetOf(Set<T> other) {
+ return other.IsProperSubsetOf(this);
+ }
+ public bool IsDisjointFrom(Set<T> other) {
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ foreach (T t in a.Keys) {
+ if (b.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(T t) {
+ return dict.ContainsKey(t);
+ }
+ public Set<T> Union(Set<T> other) {
+ if (dict.Count == 0)
+ return other;
+ else if (other.dict.Count == 0)
+ return this;
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ Dictionary<T, bool> r = new Dictionary<T, bool>();
+ foreach (T t in b.Keys)
+ r[t] = true;
+ foreach (T t in a.Keys)
+ r[t] = true;
+ return new Set<T>(r);
+ }
+ public Set<T> Intersect(Set<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return other;
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ Dictionary<T, bool> r = new Dictionary<T, bool>();
+ foreach (T t in a.Keys) {
+ if (b.ContainsKey(t))
+ r.Add(t, true);
+ }
+ return new Set<T>(r);
+ }
+ public Set<T> Difference(Set<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return this;
+ Dictionary<T, bool> r = new Dictionary<T, bool>();
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t))
+ r.Add(t, true);
+ }
+ return new Set<T>(r);
+ }
+ }
+ public class Sequence<T>
+ {
+ T[] elmts;
+ public Sequence() { }
+ Sequence(T[] ee) {
+ elmts = ee;
+ }
+ public static Sequence<T> Empty {
+ get {
+ return new Sequence<T>(new T[0]);
+ }
+ }
+ public static Sequence<T> FromElements(params T[] values) {
+ return new Sequence<T>(values);
+ }
+ public BigInteger Length {
+ get { return new BigInteger(elmts.Length); }
+ }
+ public T[] Elements {
+ get {
+ return elmts;
+ }
+ }
+ public T Select(BigInteger index) {
+ return elmts[(int)index];
+ }
+ public Sequence<T> Update(BigInteger index, T t) {
+ T[] a = (T[])elmts.Clone();
+ a[(int)index] = t;
+ return new Sequence<T>(a);
+ }
+ public bool Equals(Sequence<T> other) {
+ int n = elmts.Length;
+ return n == other.elmts.Length && EqualUntil(other, n);
+ }
+ public override bool Equals(object other) {
+ return other is Sequence<T> && Equals((Sequence<T>)other);
+ }
+ public override int GetHashCode() {
+ return elmts.GetHashCode();
+ }
+ bool EqualUntil(Sequence<T> other, int n) {
+ for (int i = 0; i < n; i++) {
+ if (!elmts[i].Equals(other.elmts[i]))
+ return false;
+ }
+ return true;
+ }
+ public bool IsProperPrefixOf(Sequence<T> other) {
+ int n = elmts.Length;
+ return n < other.elmts.Length && EqualUntil(other, n);
+ }
+ public bool IsPrefixOf(Sequence<T> other) {
+ int n = elmts.Length;
+ return n <= other.elmts.Length && EqualUntil(other, n);
+ }
+ public Sequence<T> Concat(Sequence<T> other) {
+ if (elmts.Length == 0)
+ return other;
+ else if (other.elmts.Length == 0)
+ return this;
+ T[] a = new T[elmts.Length + other.elmts.Length];
+ System.Array.Copy(elmts, 0, a, 0, elmts.Length);
+ System.Array.Copy(other.elmts, 0, a, elmts.Length, other.elmts.Length);
+ return new Sequence<T>(a);
+ }
+ public bool Contains(T t) {
+ int n = elmts.Length;
+ for (int i = 0; i < n; i++) {
+ if (t.Equals(elmts[i]))
+ return true;
+ }
+ return false;
+ }
+ public Sequence<T> Take(BigInteger n) {
+ int m = (int)n;
+ if (elmts.Length == m)
+ return this;
+ T[] a = new T[m];
+ System.Array.Copy(elmts, a, m);
+ return new Sequence<T>(a);
+ }
+ public Sequence<T> Drop(BigInteger n) {
+ if (n.IsZero)
+ return this;
+ int m = (int)n;
+ T[] a = new T[elmts.Length - m];
+ System.Array.Copy(elmts, m, a, 0, elmts.Length - m);
+ return new Sequence<T>(a);
+ }
+ }
+ public struct Pair<A, B>
+ {
+ public readonly A Car;
+ public readonly B Cdr;
+ public Pair(A a, B b) {
+ this.Car = a;
+ this.Cdr = b;
+ }
+ }
+}
diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc index 3645e7a3..07a21627 100644 --- a/Source/Core/CommandLineOptions.ssc +++ b/Source/Core/CommandLineOptions.ssc @@ -106,6 +106,7 @@ namespace Microsoft.Boogie }
public string DafnyPrintFile = null;
+ public bool Compile = true;
public enum ProverWarnings { None, Stdout, Stderr }
public ProverWarnings PrintProverWarnings = ProverWarnings.None;
@@ -534,6 +535,15 @@ namespace Microsoft.Boogie }
break;
+ case "-compile":
+ case "/compile": {
+ int compile = 0;
+ if (ps.GetNumericArgument(ref compile, 2)) {
+ Compile = compile == 1;
+ }
+ break;
+ }
+
case "-contracts":
case "/contracts":
case "-c":
@@ -1840,6 +1850,9 @@ namespace Microsoft.Boogie /dprint:<file> : print Dafny program after parsing it
(use - as <file> to print to console)
+ /compile:<n> : 0 (default) - do not compile Dafny program
+ 1 - upon successful verification of the Dafny program,
+ compile Dafny program to C# program out.cs
---- Boogie options --------------------------------------------------------
diff --git a/Source/Dafny/Compiler.ssc b/Source/Dafny/Compiler.ssc new file mode 100644 index 00000000..decbcdaa --- /dev/null +++ b/Source/Dafny/Compiler.ssc @@ -0,0 +1,1051 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Collections.Generic;
+using System.Numerics;
+using System.IO;
+using Microsoft.Contracts;
+using Bpl = Microsoft.Boogie;
+using System.Text;
+
+namespace Microsoft.Dafny {
+ public class Compiler {
+ public Compiler(TextWriter! wr) {
+ this.wr = wr;
+ }
+
+ TextWriter! wr;
+
+ public int ErrorCount;
+ void Error(string! msg, params object[] args) {
+ string s = string.Format("Compilation error: " + msg, args);
+ Console.WriteLine(s);
+ wr.WriteLine("/* {0} */", s);
+ ErrorCount++;
+ }
+
+ void ReadRuntimeSystem() {
+ string! codebase = (!) System.IO.Path.GetDirectoryName((!)System.Reflection.Assembly.GetExecutingAssembly().Location);
+ string! path = System.IO.Path.Combine(codebase, "DafnyRuntime.cs");
+ using (TextReader rd = new StreamReader(new FileStream(path, System.IO.FileMode.Open, System.IO.FileAccess.Read)))
+ {
+ while (true) {
+ string s = rd.ReadLine();
+ if (s == null)
+ return;
+ wr.WriteLine(s);
+ }
+ }
+ }
+
+ readonly int IndentAmount = 2;
+ void Indent(int ind) {
+ string spaces = " ";
+ for (; spaces.Length < ind; ind -= spaces.Length) {
+ wr.Write(spaces);
+ }
+ wr.Write(spaces.Substring(0, ind));
+ }
+
+ public void Compile(Program! program) {
+ wr.WriteLine("// Dafny program {0} compiled into C#", program.Name);
+ wr.WriteLine();
+ ReadRuntimeSystem();
+
+ foreach (ModuleDecl m in program.Modules) {
+ int indent = 0;
+ if (!m.IsDefaultModule) {
+ wr.WriteLine("namespace {0} {{", m.Name);
+ indent += IndentAmount;
+ }
+ foreach (TopLevelDecl d in m.TopLevelDecls) {
+ wr.WriteLine();
+ if (d is DatatypeDecl) {
+ DatatypeDecl dt = (DatatypeDecl)d;
+ Indent(indent);
+ wr.Write("public abstract class Base_{0}", dt.Name);
+ if (dt.TypeArgs.Count != 0) {
+ wr.Write("<{0}>", TypeParameters(dt.TypeArgs));
+ }
+ wr.WriteLine(" { }");
+ CompileDatatypeConstructors(dt, indent);
+ CompileDatatypeStruct(dt, indent);
+ } else {
+ ClassDecl cl = (ClassDecl)d;
+ Indent(indent);
+ wr.Write("public class {0}", cl.IsDefaultClass ? "_DefaultClass" : cl.Name);
+ if (cl.TypeArgs.Count != 0) {
+ wr.Write("<{0}>", TypeParameters(cl.TypeArgs));
+ }
+ wr.WriteLine(" {");
+ CompileClassMembers(cl, indent+IndentAmount);
+ Indent(indent); wr.WriteLine("}");
+ }
+ }
+ if (!m.IsDefaultModule) {
+ wr.WriteLine("}} // end of namespace {0}", m.Name);
+ }
+ }
+ }
+
+ void CompileDatatypeConstructors(DatatypeDecl! dt, int indent)
+ {
+ foreach (DatatypeCtor ctor in dt.Ctors) {
+ // class Dt_Ctor<T,U> : Base_Dt<T> {
+ // Fields;
+ // public Dt_Ctor(arguments) {
+ // Fields = arguments;
+ // }
+ // }
+ Indent(indent);
+ wr.Write("public class {0}", DtCtorName(ctor));
+ if (dt.TypeArgs.Count != 0 || ctor.TypeArgs.Count != 0) {
+ wr.Write("<");
+ string sep = "";
+ if (dt.TypeArgs.Count != 0) {
+ wr.Write("{0}", TypeParameters(dt.TypeArgs));
+ sep = ",";
+ }
+ if (ctor.TypeArgs.Count != 0) {
+ wr.Write("{0}{1}", sep, TypeParameters(ctor.TypeArgs));
+ }
+ wr.Write(">");
+ }
+ wr.Write(" : Base_{0}", dt.Name);
+ wr.WriteLine(" {");
+ if (dt.TypeArgs.Count != 0) {
+ wr.Write("<{0}>", TypeParameters(dt.TypeArgs));
+ }
+ int ind = indent + IndentAmount;
+
+ int i = 0;
+ foreach (Formal arg in ctor.Formals) {
+ if (!arg.IsGhost) {
+ Indent(ind);
+ wr.WriteLine("public readonly {0} {1};", TypeName(arg.Type), FormalName(arg, i));
+ i++;
+ }
+ }
+
+ Indent(ind);
+ wr.Write("public {0}(", DtCtorName(ctor));
+ WriteFormals(ctor.Formals);
+ wr.WriteLine(") {");
+ i = 0;
+ foreach (Formal arg in ctor.Formals) {
+ if (!arg.IsGhost) {
+ Indent(ind + IndentAmount);
+ wr.WriteLine("this.{0} = {0};", FormalName(arg, i));
+ i++;
+ }
+ }
+ Indent(ind); wr.WriteLine("}");
+
+ Indent(indent); wr.WriteLine("}");
+ }
+ }
+
+ void CompileDatatypeStruct(DatatypeDecl! dt, int indent) {
+ // public struct Dt<T> {
+ // Base_Dt<T> d;
+ // public Base_Dt<T> D {
+ // get { if (d == null) { d = Default; } return d; }
+ // }
+ // public Dt(Base_Dt<T> d) { this.d = d; }
+ // public static Base_Dt<T> Default {
+ // get { return ...; }
+ // }
+ // public override bool Equals(object other) {
+ // return other is Dt<T> && D.Equals(((Dt<T>)other).D);
+ // }
+ // public override int GetHashCode() { return D.GetHashCode(); }
+ // }
+ string DtT = dt.Name;
+ if (dt.TypeArgs.Count != 0) {
+ DtT += "<" + TypeParameters(dt.TypeArgs) + ">";
+ }
+
+ Indent(indent);
+ wr.WriteLine("public struct {0} {{", DtT);
+ int ind = indent + IndentAmount;
+
+ Indent(ind);
+ wr.WriteLine("Base_{0} d;", DtT);
+
+ Indent(ind);
+ wr.WriteLine("public Base_{0} D {{", DtT);
+ Indent(ind + IndentAmount);
+ wr.WriteLine("get { if (d == null) { d = Default; } return d; }");
+ Indent(ind); wr.WriteLine("}");
+
+ Indent(ind);
+ wr.WriteLine("public {0}(Base_{1} d) {{ this.d = d; }}", dt.Name, DtT);
+
+ Indent(ind);
+ wr.WriteLine("public static Base_{0} Default {{", DtT);
+ Indent(ind + IndentAmount);
+ wr.Write("get { return ");
+ wr.Write("new {0}", DtCtorName((!)dt.DefaultCtor));
+ // todo: type parameters
+ wr.Write("(");
+ string sep = "";
+ foreach (Formal f in dt.DefaultCtor.Formals) {
+ if (!f.IsGhost) {
+ wr.Write("{0}{1}", sep, DefaultValue(f.Type));
+ sep = ", ";
+ }
+ }
+ wr.Write(")");
+ wr.WriteLine("; }");
+ Indent(ind); wr.WriteLine("}");
+
+ Indent(ind); wr.WriteLine("public override bool Equals(object other) {");
+ Indent(ind + IndentAmount);
+ wr.WriteLine("return other is {0} && D.Equals((({0})other).D);", DtT);
+ Indent(ind); wr.WriteLine("}");
+
+ Indent(ind);
+ wr.WriteLine("public override int GetHashCode() { return D.GetHashCode(); }");
+
+ Indent(indent);
+ wr.WriteLine("}");
+ }
+
+ void WriteFormals(List<Formal!>! formals)
+ {
+ int i = 0;
+ string sep = "";
+ foreach (Formal arg in formals) {
+ if (!arg.IsGhost) {
+ string name = FormalName(arg, i);
+ wr.Write("{0}{1}{2} {3}", sep, arg.InParam ? "" : "out ", TypeName(arg.Type), name);
+ sep = ", ";
+ i++;
+ }
+ }
+ }
+
+ string! FormalName(Formal! formal, int i) {
+ return formal.Name.StartsWith("#") ? "a" + i : formal.Name;
+ }
+
+ string! DtCtorName(DatatypeCtor! ctor) {
+ return ((!)ctor.EnclosingDatatype).Name + "_" + ctor.Name;
+ }
+
+ void CompileClassMembers(ClassDecl! c, int indent)
+ {
+ foreach (MemberDecl member in c.Members) {
+ if (member is Field) {
+ Field f = (Field)member;
+ if (!f.IsGhost) {
+ Indent(indent);
+ wr.WriteLine("public {0} {1} = {2};", TypeName(f.Type), f.Name, DefaultValue(f.Type));
+ }
+
+ } else if (member is Function) {
+ Function f = (Function)member;
+ if (f.IsGhost) {
+ // nothing to compile
+ } else if (f.Body == null) {
+ Error("Function {0} has no body", f.FullName);
+ } else {
+ Indent(indent);
+ wr.Write("public {0}{1} {2}", f.IsStatic ? "static " : "", TypeName(f.ResultType), f.Name);
+ if (f.TypeArgs.Count != 0) {
+ wr.Write("<{0}>", TypeParameters(f.TypeArgs));
+ }
+ wr.Write("(");
+ WriteFormals(f.Formals);
+ wr.WriteLine(") {");
+ if (f.Body is MatchExpr) {
+ MatchExpr me = (MatchExpr)f.Body;
+ // Type source = e;
+ // if (source.D is Dt_Ctor0) {
+ // FormalType f0 = ((Dt_Ctor0)source.D).a0;
+ // ...
+ // return Body0;
+ // } else if (...) {
+ // ...
+ // } else if (true) {
+ // ...
+ // }
+
+ string source = "_source" + tmpVarCount;
+ tmpVarCount++;
+ Indent(indent);
+ wr.Write("{0} {1} = ", TypeName((!)me.Source.Type), source);
+ TrExpr(me.Source);
+ wr.WriteLine(";");
+
+ int i = 0;
+ foreach (MatchCaseExpr mc in me.Cases) {
+ MatchCasePrelude(source, (!)mc.Ctor, mc.Arguments, i, me.Cases.Count, indent + IndentAmount);
+
+ Indent(indent + 2*IndentAmount);
+ wr.Write("return ");
+ TrExpr(mc.Body);
+ wr.WriteLine(";");
+ i++;
+ }
+
+ Indent(indent); wr.WriteLine("}");
+
+ } else {
+ Indent(indent + IndentAmount);
+ wr.Write("return ");
+ TrExpr(f.Body);
+ wr.WriteLine(";");
+ }
+ Indent(indent); wr.WriteLine("}");
+ }
+
+ } else if (member is Method) {
+ Method m = (Method)member;
+ if (!m.IsGhost) {
+ Indent(indent);
+ wr.Write("public {0}void {1}", m.IsStatic ? "static " : "", m.Name);
+ if (m.TypeArgs.Count != 0) {
+ wr.Write("<{0}>", TypeParameters(m.TypeArgs));
+ }
+ wr.Write("(");
+ WriteFormals(m.Ins);
+ if (m.Ins.Count != 0 && m.Outs.Count != 0) {
+ wr.Write(", ");
+ }
+ WriteFormals(m.Outs);
+ wr.WriteLine(")");
+ Indent(indent); wr.WriteLine("{");
+ foreach (Formal p in m.Outs) {
+ if (!p.IsGhost) {
+ Indent(indent + IndentAmount);
+ wr.WriteLine("{0} = {1};", p.Name, DefaultValue(p.Type));
+ }
+ }
+ if (m.Body == null) {
+ Error("Method {0} has no body", m.FullName);
+ } else {
+ TrStmtList(m.Body.Body, indent);
+ }
+ Indent(indent); wr.WriteLine("}");
+
+ // allow the Main method to be an instance method
+ if (m.Name == "Main" && m.Ins.Count == 0 && m.Outs.Count == 0) {
+ Indent(indent);
+ wr.WriteLine("public static void Main(string[] args) {");
+ ClassDecl cl = (!)m.EnclosingClass;
+ Indent(indent + IndentAmount);
+ wr.Write("{0} b = new {0}", cl.Name);
+ if (cl.TypeArgs.Count != 0) {
+ // instantiate every parameter, it doesn't particularly matter how
+ wr.Write("<");
+ string sep = "";
+ for (int i = 0; i < cl.TypeArgs.Count; i++) {
+ wr.Write("{0}int", sep);
+ sep = ", ";
+ }
+ wr.Write(">");
+ }
+ wr.WriteLine("();");
+ Indent(indent + IndentAmount); wr.WriteLine("b.Main();");
+ Indent(indent); wr.WriteLine("}");
+ }
+ }
+
+ } else {
+ assert false; // unexpected member
+ }
+ }
+ }
+
+ // ----- Type ---------------------------------------------------------------------------------
+
+ readonly string! DafnySetClass = "Dafny.Set";
+ readonly string! DafnySeqClass = "Dafny.Sequence";
+
+ string! TypeName(Type! type)
+ {
+ while (true) {
+ TypeProxy tp = type as TypeProxy;
+ if (tp == null) {
+ break;
+ } else if (tp.T == null) {
+ // unresolved proxy; just treat as ref, since no particular type information is apparently needed for this type
+ return "object";
+ } else {
+ type = tp.T;
+ }
+ }
+
+ if (type is BoolType) {
+ return "bool";
+ } else if (type is IntType) {
+ return "BigInteger";
+ } else if (type is ObjectType) {
+ return "object";
+ } else if (type is UserDefinedType) {
+ UserDefinedType udt = (UserDefinedType)type;
+ string s = udt.Name;
+ if (udt.TypeArgs.Count != 0) {
+ if (exists{Type argType in udt.TypeArgs; argType is ObjectType}) {
+ Error("compilation does not support type 'object' as a type parameter; consider introducing a ghost");
+ }
+ s += "<" + TypeNames(udt.TypeArgs) + ">";
+ }
+ return s;
+ } else if (type is SetType) {
+ Type argType = ((SetType)type).Arg;
+ if (argType is ObjectType) {
+ Error("compilation of set<object> is not supported; consider introducing a ghost");
+ }
+ return DafnySetClass + "<" + TypeName(argType) + ">";
+ } else if (type is SeqType) {
+ Type argType = ((SeqType)type).Arg;
+ if (argType is ObjectType) {
+ Error("compilation of seq<object> is not supported; consider introducing a ghost");
+ }
+ return DafnySeqClass + "<" + TypeName(argType) + ">";
+ } else {
+ assert false; // unexpected type
+ }
+ }
+
+ string! TypeNames(List<Type!>! types) {
+ string s = "";
+ string sep = "";
+ foreach (Type t in types) {
+ s += sep + TypeName(t);
+ sep = ",";
+ }
+ return s;
+ }
+
+ string! TypeParameters(List<TypeParameter!>! targs) {
+ string s = "";
+ string sep = "";
+ foreach (TypeParameter tp in targs) {
+ s += sep + tp.Name;
+ sep = ",";
+ }
+ return s;
+ }
+
+ string! DefaultValue(Type! type)
+ {
+ while (true) {
+ TypeProxy tp = type as TypeProxy;
+ if (tp == null) {
+ break;
+ } else if (tp.T == null) {
+ // unresolved proxy; just treat as ref, since no particular type information is apparently needed for this type
+ return "null";
+ } else {
+ type = tp.T;
+ }
+ }
+
+ if (type is BoolType) {
+ return "false";
+ } else if (type is IntType) {
+ return "new BigInteger(0)";
+ } else if (type.IsRefType) {
+ return "null";
+ } else if (type.IsDatatype) {
+ UserDefinedType udt = (UserDefinedType)type;
+ string s = udt.Name;
+ if (udt.TypeArgs.Count != 0) {
+ s += "<" + TypeNames(udt.TypeArgs) + ">";
+ }
+ return s + ".Default";
+ } else if (type.IsTypeParameter) {
+ UserDefinedType udt = (UserDefinedType)type;
+ return "default(" + udt.Name + ")";
+ } else if (type is SetType) {
+ return DafnySetClass + "<" + TypeName(((SetType)type).Arg) + ">.Empty";
+ } else if (type is SeqType) {
+ return DafnySeqClass + "<" + TypeName(((SeqType)type).Arg) + ">.Empty";
+ } else {
+ assert false; // unexpected type
+ }
+ }
+
+ // ----- Stmt ---------------------------------------------------------------------------------
+
+ void TrStmt(Statement! stmt, int indent)
+ {
+ if (stmt.IsGhost) {
+ return;
+ }
+
+ if (stmt is PrintStmt) {
+ PrintStmt s = (PrintStmt)stmt;
+ foreach (Attributes.Argument arg in s.Args) {
+ Indent(indent);
+ wr.Write("System.Console.Write(");
+ if (arg.S != null) {
+ wr.Write("\"{0}\"", arg.S);
+ } else {
+ assert arg.E != null;
+ TrExpr(arg.E);
+ }
+ wr.WriteLine(");");
+ }
+ } else if (stmt is BreakStmt) {
+ BreakStmt s = (BreakStmt)stmt;
+ Indent(indent);
+ if (s.TargetLabel == null) {
+ // use the scoping rules of C#
+ wr.WriteLine("break;");
+ } else {
+ wr.WriteLine("goto after_{0};", s.TargetLabel);
+ }
+ } else if (stmt is ReturnStmt) {
+ Indent(indent);
+ wr.WriteLine("return;");
+ } else if (stmt is AssignStmt) {
+ AssignStmt s = (AssignStmt)stmt;
+ Indent(indent);
+ TrExpr(s.Lhs);
+ if (!(s.Rhs is HavocRhs)) {
+ wr.Write(" = ");
+ TrAssignmentRhs(s.Rhs);
+ }
+ wr.WriteLine(";");
+
+ } else if (stmt is VarDecl) {
+ TrVarDecl((VarDecl)stmt, true, indent);
+
+ } else if (stmt is CallStmt) {
+ CallStmt s = (CallStmt)stmt;
+
+ foreach (VarDecl local in s.NewVars) {
+ TrVarDecl(local, false, indent);
+ }
+
+ assert s.Method != null; // follows from the fact that stmt has been successfully resolved
+ Indent(indent);
+ if (s.Method.IsStatic) {
+ wr.Write(TypeName((!)s.Receiver.Type));
+ } else {
+ TrParenExpr(s.Receiver);
+ }
+ wr.Write(".{0}(", s.Method.Name);
+
+ string sep = "";
+ for (int i = 0; i < s.Method.Ins.Count; i++) {
+ Formal p = s.Method.Ins[i];
+ if (!p.IsGhost) {
+ wr.Write(sep);
+ TrExpr(s.Args[i]);
+ sep = ", ";
+ }
+ }
+ for (int i = 0; i < s.Method.Outs.Count; i++) {
+ Formal p = s.Method.Outs[i];
+ if (!p.IsGhost) {
+ wr.Write("{0}out ", sep);
+ TrExpr(s.Lhs[i]);
+ sep = ", ";
+ }
+ }
+
+ wr.WriteLine(");");
+
+ } else if (stmt is BlockStmt) {
+ Indent(indent); wr.WriteLine("{");
+ TrStmtList(((BlockStmt)stmt).Body, indent);
+ Indent(indent); wr.WriteLine("}");
+
+ } else if (stmt is IfStmt) {
+ IfStmt s = (IfStmt)stmt;
+ Indent(indent);
+ if (s.Guard == null) {
+ wr.WriteLine("if (true)");
+ } else {
+ wr.Write("if (");
+ TrExpr(s.Guard);
+ wr.WriteLine(")");
+ }
+
+ TrStmt(s.Thn, indent);
+ if (s.Els != null) {
+ Indent(indent); wr.WriteLine("else");
+ TrStmt(s.Els, indent);
+ }
+
+ } else if (stmt is WhileStmt) {
+ WhileStmt s = (WhileStmt)stmt;
+ if (s.Guard == null) {
+ Indent(indent);
+ wr.WriteLine("while (false) { }");
+ } else {
+ Indent(indent);
+ wr.Write("while (");
+ TrExpr(s.Guard);
+ wr.WriteLine(")");
+ TrStmt(s.Body, indent);
+ }
+
+ } else if (stmt is ForeachStmt) {
+ ForeachStmt s = (ForeachStmt)stmt;
+ // List<Pair<TType,RhsType>> pendingUpdates = new List<Pair<TType,RhsType>>();
+ // foreach (TType x in S) {
+ // if (Range(x)) {
+ // assert/assume ...;
+ // pendingUpdates.Add(new Pair(x,RHS));
+ // }
+ // }
+ // foreach (Pair<TType,RhsType> p in pendingUpdates) {
+ // p.Car.m = p.Cdr;
+ // }
+ string pu = "_pendingUpdates" + tmpVarCount;
+ string pr = "_pair" + tmpVarCount;
+ tmpVarCount++;
+ string TType = TypeName(s.BoundVar.Type);
+ string RhsType = TypeName((!)s.BodyAssign.Lhs.Type);
+
+ Indent(indent);
+ wr.WriteLine("List<Pair<{0},{1}>> {2} = new List<Pair<{0},{1}>>();", TType, RhsType, pu);
+
+ Indent(indent);
+ wr.Write("foreach ({0} {1} in (", TType, s.BoundVar.Name);
+ TrExpr(s.Collection);
+ wr.WriteLine(").Elements) {");
+
+ Indent(indent + IndentAmount);
+ wr.Write("if (");
+ TrExpr(s.Range);
+ wr.WriteLine(") {");
+
+ foreach (PredicateStmt p in s.BodyPrefix) {
+ TrStmt(p, indent + 2*IndentAmount);
+ }
+ Indent(indent + 2*IndentAmount);
+ wr.Write("{0}.Add(new Pair<{1},{2}>({3}, ", pu, TType, RhsType, s.BoundVar.Name);
+ ExprRhs rhsExpr = s.BodyAssign.Rhs as ExprRhs;
+ if (rhsExpr != null) {
+ TrExpr(rhsExpr.Expr);
+ } else {
+ wr.Write(DefaultValue(s.BodyAssign.Lhs.Type));
+ }
+ wr.WriteLine("))");
+
+ Indent(indent + IndentAmount); wr.WriteLine("}");
+ Indent(indent); wr.WriteLine("}");
+
+ Indent(indent); wr.WriteLine("foreach (Pair<{0},{1}> {2} in {3}) {{", TType, RhsType, pr, pu);
+ Indent(indent + IndentAmount);
+ FieldSelectExpr fse = (FieldSelectExpr)s.BodyAssign.Lhs;
+ wr.WriteLine("{0}.Car.{1} = {0}.Cdr;", pr, fse.FieldName);
+ Indent(indent); wr.WriteLine("}");
+
+ } else if (stmt is MatchStmt) {
+ MatchStmt s = (MatchStmt)stmt;
+ // Type source = e;
+ // if (source.D is Dt_Ctor0) {
+ // FormalType f0 = ((Dt_Ctor0)source.D).a0;
+ // ...
+ // Body0;
+ // } else if (...) {
+ // ...
+ // } else if (true) {
+ // ...
+ // }
+
+ string source = "_source" + tmpVarCount;
+ tmpVarCount++;
+ Indent(indent);
+ wr.Write("{0} {1} = ", TypeName((!)s.Source.Type), source);
+ TrExpr(s.Source);
+ wr.WriteLine(";");
+
+ int i = 0;
+ foreach (MatchCaseStmt mc in s.Cases) {
+ MatchCasePrelude(source, (!)mc.Ctor, mc.Arguments, i, s.Cases.Count, indent);
+ TrStmtList(mc.Body, indent);
+ i++;
+ }
+ Indent(indent); wr.WriteLine("}");
+
+ } else {
+ assert false; // unexpected statement
+ }
+ }
+
+ int tmpVarCount = 0;
+
+ void TrAssignmentRhs(AssignmentRhs! rhs)
+ requires !(rhs is HavocRhs);
+ {
+ if (rhs is ExprRhs) {
+ ExprRhs e = (ExprRhs)rhs;
+ TrExpr(e.Expr);
+
+ } else {
+ TypeRhs tp = (TypeRhs)rhs;
+ wr.Write("new {0}()", TypeName(tp.Type));
+ }
+ }
+
+ void TrStmtList(List<Statement!>! stmts, int indent) {
+ List<string!> currentLabels = null;
+ foreach (Statement ss in stmts) {
+ if (ss is LabelStmt) {
+ LabelStmt s = (LabelStmt)ss;
+ if (currentLabels == null) {
+ currentLabels = new List<string!>();
+ }
+ currentLabels.Add(s.Label);
+ } else {
+ TrStmt(ss, indent + IndentAmount);
+ SpillLabels(currentLabels, indent);
+ currentLabels = null;
+ }
+ }
+ SpillLabels(currentLabels, indent);
+ }
+
+ void SpillLabels(List<string!> labels, int indent) {
+ if (labels != null) {
+ foreach (string label in labels) {
+ Indent(indent);
+ wr.WriteLine("after_{0}: ;", label);
+ }
+ }
+ }
+
+ void TrVarDecl(VarDecl! s, bool alwaysInitialize, int indent) {
+ Indent(indent);
+ wr.Write("{0} {1}", TypeName(s.Type), s.Name);
+ if (s.Rhs != null) {
+ wr.Write(" = ");
+ TrAssignmentRhs(s.Rhs);
+ } else if (alwaysInitialize) {
+ // produce a default value
+ wr.Write(" = {0}", DefaultValue(s.Type));
+ }
+ wr.WriteLine(";");
+ }
+
+ void MatchCasePrelude(string! source, DatatypeCtor! ctor, List<BoundVar!>! arguments, int caseIndex, int caseCount, int indent) {
+ // if (source.D is Dt_Ctor0) {
+ // FormalType f0 = ((Dt_Ctor0)source.D).a0;
+ // ...
+ Indent(indent);
+ wr.Write("{0}if (", caseIndex == 0 ? "" : "} else ");
+ if (caseIndex == caseCount - 1) {
+ wr.Write("true");
+ } else {
+ wr.Write("{0}.D is {1}", source, DtCtorName(ctor));
+ }
+ wr.WriteLine(") {");
+
+ int k = 0; // number of processed non-ghost arguments
+ for (int m = 0; m < ctor.Formals.Count; m++) {
+ Formal arg = ctor.Formals[m];
+ if (!arg.IsGhost) {
+ BoundVar bv = arguments[m];
+ // FormalType f0 = ((Dt_Ctor0)source.D).a0;
+ Indent(indent + IndentAmount);
+ wr.WriteLine("{0} {1} = (({2}){3}.D).{4};",
+ TypeName(bv.Type), bv.Name, DtCtorName(ctor), source, FormalName(arg, k));
+ k++;
+ }
+ }
+ }
+
+ // ----- Expression ---------------------------------------------------------------------------
+
+ void TrParenExpr(string! prefix, Expression! expr) {
+ wr.Write(prefix);
+ TrParenExpr(expr);
+ }
+
+ void TrParenExpr(Expression! expr) {
+ wr.Write("(");
+ TrExpr(expr);
+ wr.Write(")");
+ }
+
+ void TrExprList(List<Expression!>! exprs) {
+ wr.Write("(");
+ string sep = "";
+ foreach (Expression e in exprs) {
+ wr.Write(sep);
+ TrExpr(e);
+ sep = ", ";
+ }
+ wr.Write(")");
+ }
+
+ void TrExpr(Expression! expr)
+ {
+ if (expr is LiteralExpr) {
+ LiteralExpr e = (LiteralExpr)expr;
+ if (e.Value == null) {
+ wr.Write("null");
+ } else if (e.Value is bool) {
+ wr.Write((bool)e.Value ? "true" : "false");
+ } else if (e.Value is BigInteger) {
+ BigInteger i = (BigInteger)e.Value;
+ if (new BigInteger(int.MinValue) <= i && i <= new BigInteger(int.MaxValue)) {
+ wr.Write("new BigInteger({0})", i);
+ } else {
+ wr.Write("BigInteger.Parse(\"{0}\")", i);
+ }
+ } else {
+ assert false; // unexpected literal
+ }
+
+ } else if (expr is ThisExpr) {
+ wr.Write("this");
+
+ } else if (expr is IdentifierExpr) {
+ IdentifierExpr e = (IdentifierExpr)expr;
+ wr.Write(((!)e.Var).Name);
+
+ } else if (expr is SetDisplayExpr) {
+ SetDisplayExpr e = (SetDisplayExpr)expr;
+ Type elType = ((SetType!)e.Type).Arg;
+ wr.Write("{0}<{1}>.FromElements", DafnySetClass, TypeName(elType));
+ TrExprList(e.Elements);
+
+ } else if (expr is SeqDisplayExpr) {
+ SeqDisplayExpr e = (SeqDisplayExpr)expr;
+ Type elType = ((SeqType!)e.Type).Arg;
+ wr.Write("{0}<{1}>.FromElements", DafnySeqClass, TypeName(elType));
+ TrExprList(e.Elements);
+
+ } else if (expr is FieldSelectExpr) {
+ FieldSelectExpr e = (FieldSelectExpr)expr;
+ TrParenExpr(e.Obj);
+ wr.Write(".{0}", e.FieldName);
+
+ } else if (expr is SeqSelectExpr) {
+ SeqSelectExpr e = (SeqSelectExpr)expr;
+ TrParenExpr(e.Seq);
+ if (e.SelectOne) {
+ assert e.E0 != null;
+ assert e.E1 == null;
+ TrParenExpr(".Select", e.E0);
+ } else {
+ if (e.E1 != null) {
+ TrParenExpr(".Take", e.E1);
+ }
+ if (e.E0 != null) {
+ TrParenExpr(".Drop", e.E0);
+ }
+ }
+
+ } else if (expr is SeqUpdateExpr) {
+ SeqUpdateExpr e = (SeqUpdateExpr)expr;
+ TrParenExpr(e.Seq);
+ wr.Write(".Update(");
+ TrExpr(e.Index);
+ wr.Write(", ");
+ TrExpr(e.Value);
+ wr.Write(")");
+
+ } else if (expr is FunctionCallExpr) {
+ FunctionCallExpr e = (FunctionCallExpr)expr;
+ Function f = (!)e.Function;
+ if (f.IsStatic) {
+ wr.Write(TypeName((!)e.Receiver.Type));
+ } else {
+ TrParenExpr(e.Receiver);
+ }
+ wr.Write(".{0}", f.Name);
+ wr.Write("(");
+ string sep = "";
+ for (int i = 0; i < e.Args.Count; i++) {
+ if (!e.Function.Formals[i].IsGhost) {
+ wr.Write(sep);
+ TrExpr(e.Args[i]);
+ sep = ", ";
+ }
+ }
+ wr.Write(")");
+
+ } else if (expr is DatatypeValue) {
+ DatatypeValue dtv = (DatatypeValue)expr;
+ assert dtv.Ctor != null; // since dtv has been successfully resolved
+ wr.Write("new {0}(new {0}", dtv.DatatypeName, DtCtorName(dtv.Ctor));
+ if (dtv.InferredTypeArgs.Count != 0) {
+ wr.Write("<{0}>", TypeNames(dtv.InferredTypeArgs));
+ }
+ wr.Write("(");
+ string sep = "";
+ for (int i = 0; i < dtv.Arguments.Count; i++) {
+ Formal formal = dtv.Ctor.Formals[i];
+ if (!formal.IsGhost) {
+ wr.Write(sep);
+ TrExpr(dtv.Arguments[i]);
+ sep = ", ";
+ }
+ }
+ wr.Write("))");
+
+ } else if (expr is OldExpr) {
+ assert false; // 'old' is always a ghost (right?)
+
+ } else if (expr is FreshExpr) {
+ assert false; // 'fresh' is always a ghost
+
+ } else if (expr is UnaryExpr) {
+ UnaryExpr e = (UnaryExpr)expr;
+ switch (e.Op) {
+ case UnaryExpr.Opcode.Not:
+ wr.Write("!");
+ TrParenExpr(e.E);
+ break;
+ case UnaryExpr.Opcode.SeqLength:
+ TrParenExpr(e.E);
+ wr.Write(".Length");
+ break;
+ default:
+ assert false; // unexpected unary expression
+ }
+
+ } else if (expr is BinaryExpr) {
+ BinaryExpr e = (BinaryExpr)expr;
+ string opString = null;
+ string preOpString = "";
+ string callString = null;
+
+ switch (e.ResolvedOp) {
+ case BinaryExpr.ResolvedOpcode.Iff:
+ opString = "=="; break;
+ case BinaryExpr.ResolvedOpcode.Imp:
+ preOpString = "!"; opString = "||"; break;
+ case BinaryExpr.ResolvedOpcode.Or:
+ opString = "||"; break;
+ case BinaryExpr.ResolvedOpcode.And:
+ opString = "&&"; break;
+
+ case BinaryExpr.ResolvedOpcode.EqCommon: {
+ Type t = (!)e.E0.Type;
+ if (t.IsDatatype || t.IsTypeParameter) {
+ callString = "Equals";
+ } else {
+ opString = "==";
+ }
+ break;
+ }
+ case BinaryExpr.ResolvedOpcode.NeqCommon: {
+ Type t = (!)e.E0.Type;
+ if (t.IsDatatype || t.IsTypeParameter) {
+ preOpString = "!";
+ callString = "Equals";
+ } else {
+ opString = "!=";
+ }
+ break;
+ }
+
+ case BinaryExpr.ResolvedOpcode.Lt:
+ opString = "<"; break;
+ case BinaryExpr.ResolvedOpcode.Le:
+ opString = "<="; break;
+ case BinaryExpr.ResolvedOpcode.Ge:
+ opString = ">="; break;
+ case BinaryExpr.ResolvedOpcode.Gt:
+ opString = ">"; break;
+ case BinaryExpr.ResolvedOpcode.Add:
+ opString = "+"; break;
+ case BinaryExpr.ResolvedOpcode.Sub:
+ opString = "-"; break;
+ case BinaryExpr.ResolvedOpcode.Mul:
+ opString = "*"; break;
+ case BinaryExpr.ResolvedOpcode.Div:
+ opString = "/"; break;
+ case BinaryExpr.ResolvedOpcode.Mod:
+ opString = "%"; break;
+
+ case BinaryExpr.ResolvedOpcode.SetEq:
+ case BinaryExpr.ResolvedOpcode.SeqEq:
+ callString = "Equals"; break;
+ case BinaryExpr.ResolvedOpcode.SetNeq:
+ case BinaryExpr.ResolvedOpcode.SeqNeq:
+ preOpString = "!"; callString = "Equals"; break;
+
+ case BinaryExpr.ResolvedOpcode.ProperSubset:
+ callString = "IsProperSubsetOf"; break;
+ case BinaryExpr.ResolvedOpcode.Subset:
+ callString = "IsSubsetOf"; break;
+ case BinaryExpr.ResolvedOpcode.Superset:
+ callString = "IsSupersetOf"; break;
+ case BinaryExpr.ResolvedOpcode.ProperSuperset:
+ callString = "IsProperSupersetOf"; break;
+ case BinaryExpr.ResolvedOpcode.Disjoint:
+ callString = "IsDisjointFrom"; break;
+ case BinaryExpr.ResolvedOpcode.InSet:
+ TrParenExpr(e.E1);
+ wr.Write(".Contains(");
+ TrExpr(e.E0);
+ wr.Write(")");
+ break;
+ case BinaryExpr.ResolvedOpcode.Union:
+ callString = "Union"; break;
+ case BinaryExpr.ResolvedOpcode.Intersection:
+ callString = "Intersect"; break;
+ case BinaryExpr.ResolvedOpcode.SetDifference:
+ callString = "Difference"; break;
+
+ case BinaryExpr.ResolvedOpcode.ProperPrefix:
+ callString = "IsProperPrefixOf"; break;
+ case BinaryExpr.ResolvedOpcode.Prefix:
+ callString = "IsPrefixOf"; break;
+ case BinaryExpr.ResolvedOpcode.Concat:
+ callString = "Concat"; break;
+ case BinaryExpr.ResolvedOpcode.InSeq:
+ TrParenExpr(e.E1);
+ wr.Write(".Contains(");
+ TrExpr(e.E0);
+ wr.Write(")");
+ break;
+ case BinaryExpr.ResolvedOpcode.NotInSeq:
+ wr.Write("!");
+ TrParenExpr(e.E1);
+ wr.Write(".Contains(");
+ TrExpr(e.E0);
+ wr.Write(")");
+ break;
+
+ default:
+ assert false; // unexpected binary expression
+ }
+ if (opString != null) {
+ wr.Write(preOpString);
+ TrParenExpr(e.E0);
+ wr.Write(" {0} ", opString);
+ TrParenExpr(e.E1);
+ } else if (callString != null) {
+ wr.Write(preOpString);
+ TrParenExpr(e.E0);
+ wr.Write(".{0}(", callString);
+ TrExpr(e.E1);
+ wr.Write(")");
+ }
+
+ } else if (expr is QuantifierExpr) {
+ assert false; // a quantifier is always a ghost
+
+ } else if (expr is ITEExpr) {
+ ITEExpr e = (ITEExpr)expr;
+ wr.Write("(");
+ TrExpr(e.Test);
+ wr.Write(") ? (");
+ TrExpr(e.Thn);
+ wr.Write(") : (");
+ TrExpr(e.Els);
+ wr.Write(")");
+
+ } else {
+ assert false; // unexpected expression
+ }
+ }
+ }
+}
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 3d07af57..351905e1 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -252,8 +252,10 @@ IdentTypeOptional<out BoundVar! var> (. var = new BoundVar(id, id.val, optType == null ? new InferredTypeProxy() : optType); .)
.
-TypeIdentOptional<out Token! id, out string! identName, out Type! ty>
-= (. string name = null; .)
+TypeIdentOptional<out Token! id, out string! identName, out Type! ty, out bool isGhost>
+= (. string name = null; isGhost = false; .)
+ [ "ghost" (. isGhost = true; .)
+ ]
TypeAndToken<out id, out ty>
[ ":"
(. /* try to convert ty to an identifier */
@@ -297,7 +299,7 @@ MethodDecl<MemberModifiers mmod, out Method! m> List<Expression!> mod = new List<Expression!>();
List<MaybeFreeExpression!> ens = new List<MaybeFreeExpression!>();
List<Expression!> dec = new List<Expression!>();
- Statement! bb; Statement body = null;
+ Statement! bb; BlockStmt body = null;
.)
"method"
(. if (mmod.IsUse) { SemErr(token, "methods cannot be declared 'use'"); }
@@ -312,7 +314,7 @@ MethodDecl<MemberModifiers mmod, out Method! m> ]
( ";" { MethodSpec<req, mod, ens, dec> }
- | { MethodSpec<req, mod, ens, dec> } BlockStmt<out bb> (. body = bb; .)
+ | { MethodSpec<req, mod, ens, dec> } BlockStmt<out bb> (. body = (BlockStmt)bb; .)
)
(. parseVarScope.PopMarker();
@@ -349,11 +351,11 @@ Formals<bool incoming, bool allowGhosts, List<Formal!\>! formals> .
FormalsOptionalIds<List<Formal!\>! formals>
-= (. Token! id; Type! ty; string! name; .)
+= (. Token! id; Type! ty; string! name; bool isGhost; .)
"("
[
- TypeIdentOptional<out id, out name, out ty> (. formals.Add(new Formal(id, name, ty, true, false)); parseVarScope.Push(name, name); .)
- { "," TypeIdentOptional<out id, out name, out ty> (. formals.Add(new Formal(id, name, ty, true, false)); parseVarScope.Push(name, name); .)
+ TypeIdentOptional<out id, out name, out ty, out isGhost> (. formals.Add(new Formal(id, name, ty, true, isGhost)); parseVarScope.Push(name, name); .)
+ { "," TypeIdentOptional<out id, out name, out ty, out isGhost> (. formals.Add(new Formal(id, name, ty, true, isGhost)); parseVarScope.Push(name, name); .)
}
]
")"
@@ -549,6 +551,7 @@ OneStmt<out Statement! s> ( AssertStmt<out s>
| AssumeStmt<out s>
| UseStmt<out s>
+ | PrintStmt<out s>
| AssignStmt<out s>
| HavocStmt<out s>
| CallStmt<out s>
@@ -828,6 +831,17 @@ UseStmt<out Statement! s> Expression<out e> ";" (. s = new UseStmt(x, e); .)
.
+PrintStmt<out Statement! s>
+= (. Token! x; Attributes.Argument! arg;
+ List<Attributes.Argument!> args = new List<Attributes.Argument!>();
+ .)
+ "print" (. x = token; .)
+ AttributeArg<out arg> (. args.Add(arg); .)
+ { "," AttributeArg<out arg> (. args.Add(arg); .)
+ }
+ ";" (. s = new PrintStmt(x, args); .)
+ .
+
/*------------------------------------------------------------------------*/
Expression<out Expression! e>
= (. Token! x; Expression! e0; Expression! e1 = dummyExpr;
diff --git a/Source/Dafny/DafnyAst.ssc b/Source/Dafny/DafnyAst.ssc index a317155c..ae07c84a 100644 --- a/Source/Dafny/DafnyAst.ssc +++ b/Source/Dafny/DafnyAst.ssc @@ -353,7 +353,7 @@ namespace Microsoft.Dafny public class DefaultModuleDecl : ModuleDecl {
public DefaultModuleDecl() {
- base(Token.NoToken, "$default", new List<string!>(), null);
+ base(Token.NoToken, "_default", new List<string!>(), null);
}
public override bool IsDefaultModule {
get { return true; }
@@ -385,7 +385,7 @@ namespace Microsoft.Dafny public class DefaultClassDecl : ClassDecl {
public DefaultClassDecl(DefaultModuleDecl! module, [Captured] List<MemberDecl!>! members) {
- base(Token.NoToken, "$default", module, new List<TypeParameter!>(), members, null);
+ base(Token.NoToken, "_default", module, new List<TypeParameter!>(), members, null);
}
public override bool IsDefaultClass {
get { return true; }
@@ -394,6 +394,7 @@ namespace Microsoft.Dafny public class DatatypeDecl : TopLevelDecl {
public readonly List<DatatypeCtor!>! Ctors;
+ public DatatypeCtor DefaultCtor; // set during resolution
public DatatypeDecl(Token! tok, string! name, ModuleDecl! module, List<TypeParameter!>! typeArgs, [Captured] List<DatatypeCtor!>! ctors, Attributes attributes) {
Ctors = ctors;
@@ -483,8 +484,11 @@ namespace Microsoft.Dafny }
} }
public abstract bool IsMutable { get; }
- readonly bool isGhost;
- public bool IsGhost { get { return isGhost; } }
+ bool isGhost; // readonly, except for BoundVar's of match expressions/statements during resolution
+ public bool IsGhost {
+ get { return isGhost; }
+ set { isGhost = value; }
+ }
public NonglobalVariable(Token! tok, string! name, Type! type, bool isGhost) {
this.tok = tok;
@@ -552,7 +556,7 @@ namespace Microsoft.Dafny public readonly List<Expression!>! Mod;
public readonly List<MaybeFreeExpression!>! Ens;
public readonly List<Expression!>! Decreases;
- public readonly Statement Body;
+ public readonly BlockStmt Body;
public Method(Token! tok, string! name,
bool isStatic, bool isGhost,
@@ -560,7 +564,7 @@ namespace Microsoft.Dafny [Captured] List<Formal!>! ins, [Captured] List<Formal!>! outs,
[Captured] List<MaybeFreeExpression!>! req, [Captured] List<Expression!>! mod, [Captured] List<MaybeFreeExpression!>! ens,
[Captured] List<Expression!>! decreases,
- [Captured] Statement body,
+ [Captured] BlockStmt body,
Attributes attributes) {
this.IsStatic = isStatic;
this.IsGhost = isGhost;
@@ -580,6 +584,7 @@ namespace Microsoft.Dafny public abstract class Statement {
public readonly Token! Tok;
+ public bool IsGhost; // filled in by resolution
public Statement(Token! tok) {
this.Tok = tok;
}
@@ -653,6 +658,15 @@ namespace Microsoft.Dafny }
}
+ public class PrintStmt : Statement {
+ public readonly List<Attributes.Argument!>! Args;
+ public PrintStmt(Token! tok, List<Attributes.Argument!>! args)
+ {
+ base(tok);
+ Args = args;
+ }
+ }
+
public class LabelStmt : Statement {
public readonly string! Label;
public LabelStmt(Token! tok, string! label) {
@@ -746,8 +760,7 @@ namespace Microsoft.Dafny }
} }
public bool IsMutable { get { return true; } }
- protected bool isGhost;
- public bool IsGhost { get { return isGhost; } }
+ bool IVariable.IsGhost { get { return base.IsGhost; } }
public readonly DeterminedAssignmentRhs Rhs;
invariant OptionalType != null || Rhs != null;
@@ -757,7 +770,7 @@ namespace Microsoft.Dafny {
this.name = name;
this.OptionalType = type;
- this.isGhost = isGhost;
+ this.IsGhost = isGhost;
this.Rhs = rhs;
base(tok);
}
@@ -774,7 +787,7 @@ namespace Microsoft.Dafny /// This method retrospectively makes the VarDecl a ghost. It is to be used only during resolution.
/// </summary>
public void MakeGhost() {
- isGhost = true;
+ base.IsGhost = true;
}
}
@@ -968,6 +981,7 @@ namespace Microsoft.Dafny public readonly string! MemberName;
public readonly List<Expression!>! Arguments;
public DatatypeCtor Ctor; // filled in by resolution
+ public List<Type!>! InferredTypeArgs = new List<Type!>(); // filled in by resolution
public DatatypeValue(Token! tok, string! datatypeName, string! memberName, [Captured] List<Expression!>! arguments) {
this.DatatypeName = datatypeName;
diff --git a/Source/Dafny/DafnyPipeline.sscproj b/Source/Dafny/DafnyPipeline.sscproj index 18653957..3bbf5366 100644 --- a/Source/Dafny/DafnyPipeline.sscproj +++ b/Source/Dafny/DafnyPipeline.sscproj @@ -131,6 +131,10 @@ SubType="Code"
RelPath="SccGraph.ssc"
/>
+ <File BuildAction="Compile"
+ SubType="Code"
+ RelPath="Compiler.ssc"
+ />
</Include>
</Files>
</XEN>
diff --git a/Source/Dafny/Parser.ssc b/Source/Dafny/Parser.ssc index 9551f031..0792f6bb 100644 --- a/Source/Dafny/Parser.ssc +++ b/Source/Dafny/Parser.ssc @@ -6,7 +6,7 @@ using Microsoft.Contracts; namespace Microsoft.Dafny {
public class Parser {
- const int maxT = 96;
+ const int maxT = 97;
const bool T = true;
const bool x = false;
@@ -285,7 +285,7 @@ public static int Parse (List<ModuleDecl!>! modules) { } else if (t.kind == 19) {
MethodDecl(mmod, out m);
mm.Add(m);
- } else Error(97);
+ } else Error(98);
}
static void GenericParameters(List<TypeParameter!>! typeArgs) {
@@ -363,7 +363,7 @@ public static int Parse (List<ModuleDecl!>! modules) { }
FunctionBody(out bb);
body = bb;
- } else Error(98);
+ } else Error(99);
parseVarScope.PopMarker();
f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUse, typeArgs, formals, returnType, reqs, reads, decreases, body, attrs);
@@ -379,7 +379,7 @@ public static int Parse (List<ModuleDecl!>! modules) { List<Expression!> mod = new List<Expression!>();
List<MaybeFreeExpression!> ens = new List<MaybeFreeExpression!>();
List<Expression!> dec = new List<Expression!>();
- Statement! bb; Statement body = null;
+ Statement! bb; BlockStmt body = null;
Expect(19);
if (mmod.IsUse) { SemErr(token, "methods cannot be declared 'use'"); }
@@ -407,8 +407,8 @@ public static int Parse (List<ModuleDecl!>! modules) { MethodSpec(req, mod, ens, dec);
}
BlockStmt(out bb);
- body = bb;
- } else Error(99);
+ body = (BlockStmt)bb;
+ } else Error(100);
parseVarScope.PopMarker();
m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
@@ -438,15 +438,15 @@ public static int Parse (List<ModuleDecl!>! modules) { }
static void FormalsOptionalIds(List<Formal!>! formals) {
- Token! id; Type! ty; string! name;
+ Token! id; Type! ty; string! name; bool isGhost;
Expect(26);
if (StartOf(6)) {
- TypeIdentOptional(out id, out name, out ty);
- formals.Add(new Formal(id, name, ty, true, false)); parseVarScope.Push(name, name);
+ TypeIdentOptional(out id, out name, out ty, out isGhost);
+ formals.Add(new Formal(id, name, ty, true, isGhost)); parseVarScope.Push(name, name);
while (t.kind == 15) {
Get();
- TypeIdentOptional(out id, out name, out ty);
- formals.Add(new Formal(id, name, ty, true, false)); parseVarScope.Push(name, name);
+ TypeIdentOptional(out id, out name, out ty, out isGhost);
+ formals.Add(new Formal(id, name, ty, true, isGhost)); parseVarScope.Push(name, name);
}
}
Expect(27);
@@ -484,8 +484,12 @@ public static int Parse (List<ModuleDecl!>! modules) { var = new BoundVar(id, id.val, optType == null ? new InferredTypeProxy() : optType);
}
- static void TypeIdentOptional(out Token! id, out string! identName, out Type! ty) {
- string name = null;
+ static void TypeIdentOptional(out Token! id, out string! identName, out Type! ty, out bool isGhost) {
+ string name = null; isGhost = false;
+ if (t.kind == 9) {
+ Get();
+ isGhost = true;
+ }
TypeAndToken(out id, out ty);
if (t.kind == 16) {
Get();
@@ -536,7 +540,7 @@ public static int Parse (List<ModuleDecl!>! modules) { } else if (t.kind == 1 || t.kind == 32) {
ReferenceType(out tok, out ty);
- } else Error(100);
+ } else Error(101);
}
static void Formals(bool incoming, bool allowGhosts, List<Formal!>! formals) {
@@ -585,12 +589,12 @@ List<Expression!>! decreases) { Expression(out e);
Expect(13);
ens.Add(new MaybeFreeExpression(e, isFree));
- } else Error(101);
+ } else Error(102);
} else if (t.kind == 25) {
Get();
Expressions(decreases);
Expect(13);
- } else Error(102);
+ } else Error(103);
}
static void BlockStmt(out Statement! block) {
@@ -617,14 +621,14 @@ List<Expression!>! decreases) { Get();
x = token;
Expression(out e);
- Expect(55);
+ Expect(56);
Expression(out e0);
Expect(46);
Expression(out e1);
e = new ITEExpr(x, e, e0, e1);
} else if (StartOf(9)) {
EquivExpression(out e);
- } else Error(103);
+ } else Error(104);
}
static void Expressions(List<Expression!>! args) {
@@ -665,7 +669,7 @@ List<Expression!>! decreases) { GenericInstantiation(gt);
}
ty = new UserDefinedType(tok, tok.val, gt);
- } else Error(104);
+ } else Error(105);
}
static void FunctionSpec(List<Expression!>! reqs, List<Expression!>! reads, List<Expression!>! decreases) {
@@ -685,7 +689,7 @@ List<Expression!>! decreases) { Get();
Expressions(decreases);
Expect(13);
- } else Error(105);
+ } else Error(106);
}
static void FunctionBody(out Expression! e) {
@@ -695,7 +699,7 @@ List<Expression!>! decreases) { MatchExpression(out e);
} else if (StartOf(7)) {
Expression(out e);
- } else Error(106);
+ } else Error(107);
Expect(7);
}
@@ -717,7 +721,7 @@ List<Expression!>! decreases) { e = new WildcardExpr(token);
} else if (StartOf(7)) {
Expression(out e);
- } else Error(107);
+ } else Error(108);
}
static void MatchExpression(out Expression! e) {
@@ -772,7 +776,7 @@ List<Expression!>! decreases) { ss.Add(s);
} else if (t.kind == 9 || t.kind == 14) {
VarDeclStmts(ss);
- } else Error(108);
+ } else Error(109);
}
static void OneStmt(out Statement! s) {
@@ -792,7 +796,11 @@ List<Expression!>! decreases) { UseStmt(out s);
break;
}
- case 1: case 26: case 88: case 89: {
+ case 55: {
+ PrintStmt(out s);
+ break;
+ }
+ case 1: case 26: case 89: case 90: {
AssignStmt(out s);
break;
}
@@ -846,7 +854,7 @@ List<Expression!>! decreases) { s = new ReturnStmt(x);
break;
}
- default: Error(109); break;
+ default: Error(110); break;
}
}
@@ -894,6 +902,23 @@ List<Expression!>! decreases) { s = new UseStmt(x, e);
}
+ static void PrintStmt(out Statement! s) {
+ Token! x; Attributes.Argument! arg;
+ List<Attributes.Argument!> args = new List<Attributes.Argument!>();
+
+ Expect(55);
+ x = token;
+ AttributeArg(out arg);
+ args.Add(arg);
+ while (t.kind == 15) {
+ Get();
+ AttributeArg(out arg);
+ args.Add(arg);
+ }
+ Expect(13);
+ s = new PrintStmt(x, args);
+ }
+
static void AssignStmt(out Statement! s) {
Token! x;
Expression! lhs;
@@ -998,7 +1023,7 @@ List<Expression!>! decreases) { } else if (t.kind == 6) {
BlockStmt(out s);
els = s;
- } else Error(110);
+ } else Error(111);
}
ifStmt = new IfStmt(x, guard, thn, els);
}
@@ -1098,7 +1123,7 @@ List<Expression!>! decreases) { } else if (t.kind == 44) {
HavocStmt(out s);
if (s is AssignStmt) { bodyAssign = (AssignStmt)s; }
- } else Error(111);
+ } else Error(112);
Expect(7);
if (bodyAssign != null) {
s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign);
@@ -1124,7 +1149,7 @@ List<Expression!>! decreases) { } else if (StartOf(7)) {
Expression(out ee);
e = ee;
- } else Error(112);
+ } else Error(113);
if (e == null && ty == null) { e = dummyExpr; }
}
@@ -1132,10 +1157,10 @@ List<Expression!>! decreases) { Token! id; e = dummyExpr;
if (t.kind == 1) {
IdentOrFuncExpression(out e);
- } else if (t.kind == 26 || t.kind == 88 || t.kind == 89) {
+ } else if (t.kind == 26 || t.kind == 89 || t.kind == 90) {
ObjectExpression(out e);
- } else Error(113);
- while (t.kind == 83 || t.kind == 85) {
+ } else Error(114);
+ while (t.kind == 84 || t.kind == 86) {
SelectOrCallSuffix(ref e);
}
}
@@ -1176,7 +1201,7 @@ List<Expression!>! decreases) { } else if (StartOf(7)) {
Expression(out ee);
e = ee;
- } else Error(114);
+ } else Error(115);
Expect(27);
}
@@ -1215,19 +1240,30 @@ List<Expression!>! decreases) { e = dummyExpr;
if (t.kind == 1) {
IdentOrFuncExpression(out e);
- } else if (t.kind == 26 || t.kind == 88 || t.kind == 89) {
+ } else if (t.kind == 26 || t.kind == 89 || t.kind == 90) {
ObjectExpression(out e);
SelectOrCallSuffix(ref e);
- } else Error(115);
- while (t.kind == 83 || t.kind == 85) {
+ } else Error(116);
+ while (t.kind == 84 || t.kind == 86) {
SelectOrCallSuffix(ref e);
}
}
+ static void AttributeArg(out Attributes.Argument! arg) {
+ Expression! e; arg = dummyAttrArg;
+ if (t.kind == 3) {
+ Get();
+ arg = new Attributes.Argument(token.val.Substring(1, token.val.Length-2));
+ } else if (StartOf(7)) {
+ Expression(out e);
+ arg = new Attributes.Argument(e);
+ } else Error(117);
+ }
+
static void EquivExpression(out Expression! e0) {
Token! x; Expression! e1;
ImpliesExpression(out e0);
- while (t.kind == 56 || t.kind == 57) {
+ while (t.kind == 57 || t.kind == 58) {
EquivOp();
x = token;
ImpliesExpression(out e1);
@@ -1238,7 +1274,7 @@ List<Expression!>! decreases) { static void ImpliesExpression(out Expression! e0) {
Token! x; Expression! e1;
LogicalExpression(out e0);
- if (t.kind == 58 || t.kind == 59) {
+ if (t.kind == 59 || t.kind == 60) {
ImpliesOp();
x = token;
ImpliesExpression(out e1);
@@ -1247,23 +1283,23 @@ List<Expression!>! decreases) { }
static void EquivOp() {
- if (t.kind == 56) {
+ if (t.kind == 57) {
Get();
- } else if (t.kind == 57) {
+ } else if (t.kind == 58) {
Get();
- } else Error(116);
+ } else Error(118);
}
static void LogicalExpression(out Expression! e0) {
Token! x; Expression! e1;
RelationalExpression(out e0);
if (StartOf(13)) {
- if (t.kind == 60 || t.kind == 61) {
+ if (t.kind == 61 || t.kind == 62) {
AndOp();
x = token;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1);
- while (t.kind == 60 || t.kind == 61) {
+ while (t.kind == 61 || t.kind == 62) {
AndOp();
x = token;
RelationalExpression(out e1);
@@ -1274,7 +1310,7 @@ List<Expression!>! decreases) { x = token;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1);
- while (t.kind == 62 || t.kind == 63) {
+ while (t.kind == 63 || t.kind == 64) {
OrOp();
x = token;
RelationalExpression(out e1);
@@ -1285,11 +1321,11 @@ List<Expression!>! decreases) { }
static void ImpliesOp() {
- if (t.kind == 58) {
+ if (t.kind == 59) {
Get();
- } else if (t.kind == 59) {
+ } else if (t.kind == 60) {
Get();
- } else Error(117);
+ } else Error(119);
}
static void RelationalExpression(out Expression! e0) {
@@ -1303,25 +1339,25 @@ List<Expression!>! decreases) { }
static void AndOp() {
- if (t.kind == 60) {
+ if (t.kind == 61) {
Get();
- } else if (t.kind == 61) {
+ } else if (t.kind == 62) {
Get();
- } else Error(118);
+ } else Error(120);
}
static void OrOp() {
- if (t.kind == 62) {
+ if (t.kind == 63) {
Get();
- } else if (t.kind == 63) {
+ } else if (t.kind == 64) {
Get();
- } else Error(119);
+ } else Error(121);
}
static void Term(out Expression! e0) {
Token! x; Expression! e1; BinaryExpr.Opcode op;
Factor(out e0);
- while (t.kind == 73 || t.kind == 74) {
+ while (t.kind == 74 || t.kind == 75) {
AddOp(out x, out op);
Factor(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -1331,7 +1367,7 @@ List<Expression!>! decreases) { static void RelOp(out Token! x, out BinaryExpr.Opcode op) {
x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/;
switch (t.kind) {
- case 64: {
+ case 65: {
Get();
x = token; op = BinaryExpr.Opcode.Eq;
break;
@@ -1346,22 +1382,22 @@ List<Expression!>! decreases) { x = token; op = BinaryExpr.Opcode.Gt;
break;
}
- case 65: {
+ case 66: {
Get();
x = token; op = BinaryExpr.Opcode.Le;
break;
}
- case 66: {
+ case 67: {
Get();
x = token; op = BinaryExpr.Opcode.Ge;
break;
}
- case 67: {
+ case 68: {
Get();
x = token; op = BinaryExpr.Opcode.Neq;
break;
}
- case 68: {
+ case 69: {
Get();
x = token; op = BinaryExpr.Opcode.Disjoint;
break;
@@ -1371,34 +1407,34 @@ List<Expression!>! decreases) { x = token; op = BinaryExpr.Opcode.In;
break;
}
- case 69: {
+ case 70: {
Get();
x = token; op = BinaryExpr.Opcode.NotIn;
break;
}
- case 70: {
+ case 71: {
Get();
x = token; op = BinaryExpr.Opcode.Neq;
break;
}
- case 71: {
+ case 72: {
Get();
x = token; op = BinaryExpr.Opcode.Le;
break;
}
- case 72: {
+ case 73: {
Get();
x = token; op = BinaryExpr.Opcode.Ge;
break;
}
- default: Error(120); break;
+ default: Error(122); break;
}
}
static void Factor(out Expression! e0) {
Token! x; Expression! e1; BinaryExpr.Opcode op;
UnaryExpression(out e0);
- while (t.kind == 35 || t.kind == 75 || t.kind == 76) {
+ while (t.kind == 35 || t.kind == 76 || t.kind == 77) {
MulOp(out x, out op);
UnaryExpression(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -1407,23 +1443,23 @@ List<Expression!>! decreases) { static void AddOp(out Token! x, out BinaryExpr.Opcode op) {
x = Token.NoToken; op=BinaryExpr.Opcode.Add/*(dummy)*/;
- if (t.kind == 73) {
+ if (t.kind == 74) {
Get();
x = token; op = BinaryExpr.Opcode.Add;
- } else if (t.kind == 74) {
+ } else if (t.kind == 75) {
Get();
x = token; op = BinaryExpr.Opcode.Sub;
- } else Error(121);
+ } else Error(123);
}
static void UnaryExpression(out Expression! e) {
Token! x; e = dummyExpr;
- if (t.kind == 74) {
+ if (t.kind == 75) {
Get();
x = token;
UnaryExpression(out e);
e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e);
- } else if (t.kind == 77 || t.kind == 78) {
+ } else if (t.kind == 78 || t.kind == 79) {
NegOp();
x = token;
UnaryExpression(out e);
@@ -1432,7 +1468,7 @@ List<Expression!>! decreases) { SelectExpression(out e);
} else if (StartOf(15)) {
ConstAtomExpression(out e);
- } else Error(122);
+ } else Error(124);
}
static void MulOp(out Token! x, out BinaryExpr.Opcode op) {
@@ -1440,21 +1476,21 @@ List<Expression!>! decreases) { if (t.kind == 35) {
Get();
x = token; op = BinaryExpr.Opcode.Mul;
- } else if (t.kind == 75) {
+ } else if (t.kind == 76) {
Get();
x = token; op = BinaryExpr.Opcode.Div;
- } else if (t.kind == 76) {
+ } else if (t.kind == 77) {
Get();
x = token; op = BinaryExpr.Opcode.Mod;
- } else Error(123);
+ } else Error(125);
}
static void NegOp() {
- if (t.kind == 77) {
+ if (t.kind == 78) {
Get();
- } else if (t.kind == 78) {
+ } else if (t.kind == 79) {
Get();
- } else Error(124);
+ } else Error(126);
}
static void ConstAtomExpression(out Expression! e) {
@@ -1462,17 +1498,17 @@ List<Expression!>! decreases) { e = dummyExpr;
switch (t.kind) {
- case 79: {
+ case 80: {
Get();
e = new LiteralExpr(token, false);
break;
}
- case 80: {
+ case 81: {
Get();
e = new LiteralExpr(token, true);
break;
}
- case 81: {
+ case 82: {
Get();
e = new LiteralExpr(token);
break;
@@ -1482,11 +1518,11 @@ List<Expression!>! decreases) { e = new LiteralExpr(token, n);
break;
}
- case 82: {
+ case 83: {
Get();
x = token;
Ident(out dtName);
- Expect(83);
+ Expect(84);
Ident(out id);
elements = new List<Expression!>();
if (t.kind == 26) {
@@ -1499,7 +1535,7 @@ List<Expression!>! decreases) { e = new DatatypeValue(token, dtName.val, id.val, elements);
break;
}
- case 84: {
+ case 85: {
Get();
x = token;
Expect(26);
@@ -1526,17 +1562,17 @@ List<Expression!>! decreases) { Expect(7);
break;
}
- case 85: {
+ case 86: {
Get();
x = token; elements = new List<Expression!>();
if (StartOf(7)) {
Expressions(elements);
}
e = new SeqDisplayExpr(x, elements);
- Expect(86);
+ Expect(87);
break;
}
- default: Error(125); break;
+ default: Error(127); break;
}
}
@@ -1575,10 +1611,10 @@ List<Expression!>! decreases) { static void ObjectExpression(out Expression! e) {
Token! x; e = dummyExpr;
- if (t.kind == 88) {
+ if (t.kind == 89) {
Get();
e = new ThisExpr(token);
- } else if (t.kind == 89) {
+ } else if (t.kind == 90) {
Get();
x = token;
Expect(26);
@@ -1591,9 +1627,9 @@ List<Expression!>! decreases) { QuantifierGuts(out e);
} else if (StartOf(7)) {
Expression(out e);
- } else Error(126);
+ } else Error(128);
Expect(27);
- } else Error(127);
+ } else Error(129);
}
static void SelectOrCallSuffix(ref Expression! e) {
@@ -1601,7 +1637,7 @@ List<Expression!>! decreases) { Expression e0 = null; Expression e1 = null; Expression! ee; bool anyDots = false;
bool func = false;
- if (t.kind == 83) {
+ if (t.kind == 84) {
Get();
Ident(out id);
if (t.kind == 26) {
@@ -1614,14 +1650,14 @@ List<Expression!>! decreases) { e = new FunctionCallExpr(id, id.val, e, args);
}
if (!func) { e = new FieldSelectExpr(id, e, id.val); }
- } else if (t.kind == 85) {
+ } else if (t.kind == 86) {
Get();
x = token;
if (StartOf(7)) {
Expression(out ee);
e0 = ee;
- if (t.kind == 42 || t.kind == 87) {
- if (t.kind == 87) {
+ if (t.kind == 42 || t.kind == 88) {
+ if (t.kind == 88) {
Get();
anyDots = true;
if (StartOf(7)) {
@@ -1634,11 +1670,11 @@ List<Expression!>! decreases) { e1 = ee;
}
}
- } else if (t.kind == 87) {
+ } else if (t.kind == 88) {
Get();
Expression(out ee);
anyDots = true; e1 = ee;
- } else Error(128);
+ } else Error(130);
assert !anyDots ==> e0 != null;
if (anyDots) {
assert e0 != null || e1 != null;
@@ -1651,8 +1687,8 @@ List<Expression!>! decreases) { e = new SeqUpdateExpr(x, e, e0, e1);
}
- Expect(86);
- } else Error(129);
+ Expect(87);
+ } else Error(131);
}
static void QuantifierGuts(out Expression! q) {
@@ -1665,13 +1701,13 @@ List<Expression!>! decreases) { Triggers trigs = null;
Expression! body;
- if (t.kind == 90 || t.kind == 91) {
+ if (t.kind == 91 || t.kind == 92) {
Forall();
x = token; univ = true;
- } else if (t.kind == 92 || t.kind == 93) {
+ } else if (t.kind == 93 || t.kind == 94) {
Exists();
x = token;
- } else Error(130);
+ } else Error(132);
parseVarScope.PushMarker();
IdentTypeOptional(out bv);
bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name);
@@ -1695,19 +1731,19 @@ List<Expression!>! decreases) { }
static void Forall() {
- if (t.kind == 90) {
+ if (t.kind == 91) {
Get();
- } else if (t.kind == 91) {
+ } else if (t.kind == 92) {
Get();
- } else Error(131);
+ } else Error(133);
}
static void Exists() {
- if (t.kind == 92) {
+ if (t.kind == 93) {
Get();
- } else if (t.kind == 93) {
+ } else if (t.kind == 94) {
Get();
- } else Error(132);
+ } else Error(134);
}
static void AttributeOrTrigger(ref Attributes attrs, ref Triggers trigs) {
@@ -1720,16 +1756,16 @@ List<Expression!>! decreases) { es = new List<Expression!>();
Expressions(es);
trigs = new Triggers(es, trigs);
- } else Error(133);
+ } else Error(135);
Expect(7);
}
static void QSep() {
- if (t.kind == 94) {
+ if (t.kind == 95) {
Get();
- } else if (t.kind == 95) {
+ } else if (t.kind == 96) {
Get();
- } else Error(134);
+ } else Error(136);
}
static void AttributeBody(ref Attributes attrs) {
@@ -1752,17 +1788,6 @@ List<Expression!>! decreases) { attrs = new Attributes(aName, aArgs, attrs);
}
- static void AttributeArg(out Attributes.Argument! arg) {
- Expression! e; arg = dummyAttrArg;
- if (t.kind == 3) {
- Get();
- arg = new Attributes.Argument(token.val.Substring(1, token.val.Length-2));
- } else if (StartOf(7)) {
- Expression(out e);
- arg = new Attributes.Argument(e);
- } else Error(135);
- }
-
public static void Parse() {
@@ -1834,87 +1859,88 @@ List<Expression!>! decreases) { case 52: s = "| expected"; break;
case 53: s = "assert expected"; break;
case 54: s = "assume expected"; break;
- case 55: s = "then expected"; break;
- case 56: s = "<==> expected"; break;
- case 57: s = "\\u21d4 expected"; break;
- case 58: s = "==> expected"; break;
- case 59: s = "\\u21d2 expected"; break;
- case 60: s = "&& expected"; break;
- case 61: s = "\\u2227 expected"; break;
- case 62: s = "|| expected"; break;
- case 63: s = "\\u2228 expected"; break;
- case 64: s = "== expected"; break;
- case 65: s = "<= expected"; break;
- case 66: s = ">= expected"; break;
- case 67: s = "!= expected"; break;
- case 68: s = "!! expected"; break;
- case 69: s = "!in expected"; break;
- case 70: s = "\\u2260 expected"; break;
- case 71: s = "\\u2264 expected"; break;
- case 72: s = "\\u2265 expected"; break;
- case 73: s = "+ expected"; break;
- case 74: s = "- expected"; break;
- case 75: s = "/ expected"; break;
- case 76: s = "% expected"; break;
- case 77: s = "! expected"; break;
- case 78: s = "\\u00ac expected"; break;
- case 79: s = "false expected"; break;
- case 80: s = "true expected"; break;
- case 81: s = "null expected"; break;
- case 82: s = "# expected"; break;
- case 83: s = ". expected"; break;
- case 84: s = "fresh expected"; break;
- case 85: s = "[ expected"; break;
- case 86: s = "] expected"; break;
- case 87: s = ".. expected"; break;
- case 88: s = "this expected"; break;
- case 89: s = "old expected"; break;
- case 90: s = "forall expected"; break;
- case 91: s = "\\u2200 expected"; break;
- case 92: s = "exists expected"; break;
- case 93: s = "\\u2203 expected"; break;
- case 94: s = ":: expected"; break;
- case 95: s = "\\u2022 expected"; break;
- case 96: s = "??? expected"; break;
- case 97: s = "invalid ClassMemberDecl"; break;
- case 98: s = "invalid FunctionDecl"; break;
- case 99: s = "invalid MethodDecl"; break;
- case 100: s = "invalid TypeAndToken"; break;
- case 101: s = "invalid MethodSpec"; break;
+ case 55: s = "print expected"; break;
+ case 56: s = "then expected"; break;
+ case 57: s = "<==> expected"; break;
+ case 58: s = "\\u21d4 expected"; break;
+ case 59: s = "==> expected"; break;
+ case 60: s = "\\u21d2 expected"; break;
+ case 61: s = "&& expected"; break;
+ case 62: s = "\\u2227 expected"; break;
+ case 63: s = "|| expected"; break;
+ case 64: s = "\\u2228 expected"; break;
+ case 65: s = "== expected"; break;
+ case 66: s = "<= expected"; break;
+ case 67: s = ">= expected"; break;
+ case 68: s = "!= expected"; break;
+ case 69: s = "!! expected"; break;
+ case 70: s = "!in expected"; break;
+ case 71: s = "\\u2260 expected"; break;
+ case 72: s = "\\u2264 expected"; break;
+ case 73: s = "\\u2265 expected"; break;
+ case 74: s = "+ expected"; break;
+ case 75: s = "- expected"; break;
+ case 76: s = "/ expected"; break;
+ case 77: s = "% expected"; break;
+ case 78: s = "! expected"; break;
+ case 79: s = "\\u00ac expected"; break;
+ case 80: s = "false expected"; break;
+ case 81: s = "true expected"; break;
+ case 82: s = "null expected"; break;
+ case 83: s = "# expected"; break;
+ case 84: s = ". expected"; break;
+ case 85: s = "fresh expected"; break;
+ case 86: s = "[ expected"; break;
+ case 87: s = "] expected"; break;
+ case 88: s = ".. expected"; break;
+ case 89: s = "this expected"; break;
+ case 90: s = "old expected"; break;
+ case 91: s = "forall expected"; break;
+ case 92: s = "\\u2200 expected"; break;
+ case 93: s = "exists expected"; break;
+ case 94: s = "\\u2203 expected"; break;
+ case 95: s = ":: expected"; break;
+ case 96: s = "\\u2022 expected"; break;
+ case 97: s = "??? expected"; break;
+ case 98: s = "invalid ClassMemberDecl"; break;
+ case 99: s = "invalid FunctionDecl"; break;
+ case 100: s = "invalid MethodDecl"; break;
+ case 101: s = "invalid TypeAndToken"; break;
case 102: s = "invalid MethodSpec"; break;
- case 103: s = "invalid Expression"; break;
- case 104: s = "invalid ReferenceType"; break;
- case 105: s = "invalid FunctionSpec"; break;
- case 106: s = "invalid FunctionBody"; break;
- case 107: s = "invalid PossiblyWildExpression"; break;
- case 108: s = "invalid Stmt"; break;
- case 109: s = "invalid OneStmt"; break;
- case 110: s = "invalid IfStmt"; break;
- case 111: s = "invalid ForeachStmt"; break;
- case 112: s = "invalid AssignRhs"; break;
- case 113: s = "invalid SelectExpression"; break;
- case 114: s = "invalid Guard"; break;
- case 115: s = "invalid CallStmtSubExpr"; break;
- case 116: s = "invalid EquivOp"; break;
- case 117: s = "invalid ImpliesOp"; break;
- case 118: s = "invalid AndOp"; break;
- case 119: s = "invalid OrOp"; break;
- case 120: s = "invalid RelOp"; break;
- case 121: s = "invalid AddOp"; break;
- case 122: s = "invalid UnaryExpression"; break;
- case 123: s = "invalid MulOp"; break;
- case 124: s = "invalid NegOp"; break;
- case 125: s = "invalid ConstAtomExpression"; break;
- case 126: s = "invalid ObjectExpression"; break;
- case 127: s = "invalid ObjectExpression"; break;
- case 128: s = "invalid SelectOrCallSuffix"; break;
- case 129: s = "invalid SelectOrCallSuffix"; break;
- case 130: s = "invalid QuantifierGuts"; break;
- case 131: s = "invalid Forall"; break;
- case 132: s = "invalid Exists"; break;
- case 133: s = "invalid AttributeOrTrigger"; break;
- case 134: s = "invalid QSep"; break;
- case 135: s = "invalid AttributeArg"; break;
+ case 103: s = "invalid MethodSpec"; break;
+ case 104: s = "invalid Expression"; break;
+ case 105: s = "invalid ReferenceType"; break;
+ case 106: s = "invalid FunctionSpec"; break;
+ case 107: s = "invalid FunctionBody"; break;
+ case 108: s = "invalid PossiblyWildExpression"; break;
+ case 109: s = "invalid Stmt"; break;
+ case 110: s = "invalid OneStmt"; break;
+ case 111: s = "invalid IfStmt"; break;
+ case 112: s = "invalid ForeachStmt"; break;
+ case 113: s = "invalid AssignRhs"; break;
+ case 114: s = "invalid SelectExpression"; break;
+ case 115: s = "invalid Guard"; break;
+ case 116: s = "invalid CallStmtSubExpr"; break;
+ case 117: s = "invalid AttributeArg"; break;
+ case 118: s = "invalid EquivOp"; break;
+ case 119: s = "invalid ImpliesOp"; break;
+ case 120: s = "invalid AndOp"; break;
+ case 121: s = "invalid OrOp"; break;
+ case 122: s = "invalid RelOp"; break;
+ case 123: s = "invalid AddOp"; break;
+ case 124: s = "invalid UnaryExpression"; break;
+ case 125: s = "invalid MulOp"; break;
+ case 126: s = "invalid NegOp"; break;
+ case 127: s = "invalid ConstAtomExpression"; break;
+ case 128: s = "invalid ObjectExpression"; break;
+ case 129: s = "invalid ObjectExpression"; break;
+ case 130: s = "invalid SelectOrCallSuffix"; break;
+ case 131: s = "invalid SelectOrCallSuffix"; break;
+ case 132: s = "invalid QuantifierGuts"; break;
+ case 133: s = "invalid Forall"; break;
+ case 134: s = "invalid Exists"; break;
+ case 135: s = "invalid AttributeOrTrigger"; break;
+ case 136: s = "invalid QSep"; break;
default: s = "error " + n; break;
}
@@ -1922,24 +1948,24 @@ List<Expression!>! decreases) { }
static bool[,]! set = {
- {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, T,x,x,x, T,T,T,T, T,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,T,T,T, x,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,x, T,T,x,x, T,T,x,x, x,x,x,x, x,x},
- {x,T,x,x, x,x,T,x, x,T,x,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,x,x, T,T,x,T, x,T,T,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,x, T,T,x,x, T,T,x,x, x,x,x,x, x,x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,x, T,T,x,x, T,T,x,x, x,x,x,x, x,x},
- {x,T,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,x,x, T,T,x,T, x,T,T,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x},
- {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x},
- {x,T,T,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,x, T,T,x,x, T,T,x,x, x,x,x,x, x,x}
+ {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, T,x,x,x, T,T,T,T, T,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,x, x,T,T,T, x,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,T,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, x,T,T,x, x,T,T,x, x,x,x,x, x,x,x},
+ {x,T,x,x, x,x,T,x, x,T,x,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,x,x, T,T,x,T, x,T,T,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, x,T,T,x, x,T,T,x, x,x,x,x, x,x,x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, x,T,T,x, x,T,T,x, x,x,x,x, x,x,x},
+ {x,T,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,x,x, T,T,x,T, x,T,T,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x},
+ {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, x,x,x},
+ {x,T,T,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, x,T,T,x, x,T,T,x, x,x,x,x, x,x,x}
};
diff --git a/Source/Dafny/Printer.ssc b/Source/Dafny/Printer.ssc index 6f3629d6..1779f46b 100644 --- a/Source/Dafny/Printer.ssc +++ b/Source/Dafny/Printer.ssc @@ -143,21 +143,25 @@ namespace Microsoft.Dafny { PrintAttributes(a.Prev);
wr.Write("{ :{0}", a.Name);
- string prefix = " ";
- foreach (Attributes.Argument arg in a.Args) {
- wr.Write(prefix);
- prefix = ", ";
- if (arg.S != null) {
- wr.Write("\"{0}\"", arg.S);
- } else {
- assert arg.E != null;
- PrintExpression(arg.E);
- }
- }
+ PrintAttributeArgs(a.Args);
wr.Write(" } ");
}
}
+ public void PrintAttributeArgs(List<Attributes.Argument!>! args) {
+ string prefix = " ";
+ foreach (Attributes.Argument arg in args) {
+ wr.Write(prefix);
+ prefix = ", ";
+ if (arg.S != null) {
+ wr.Write("\"{0}\"", arg.S);
+ } else {
+ assert arg.E != null;
+ PrintExpression(arg.E);
+ }
+ }
+ }
+
public void PrintField(Field! field, int indent) {
Indent(indent);
if (field.IsGhost) {
@@ -333,6 +337,12 @@ namespace Microsoft.Dafny { PrintExpression(((UseStmt)stmt).Expr);
wr.Write(";");
+ } else if (stmt is PrintStmt) {
+ PrintStmt s = (PrintStmt)stmt;
+ wr.Write("print");
+ PrintAttributeArgs(s.Args);
+ wr.Write(";");
+
} else if (stmt is LabelStmt) {
wr.Write("label {0}:", ((LabelStmt)stmt).Label);
diff --git a/Source/Dafny/Resolver.ssc b/Source/Dafny/Resolver.ssc index 430714d3..db6e667a 100644 --- a/Source/Dafny/Resolver.ssc +++ b/Source/Dafny/Resolver.ssc @@ -303,7 +303,7 @@ namespace Microsoft.Dafny { /// <summary>
/// Check that the datatype has some constructor all whose argument types go to a lower stratum, which means
/// go to a different SCC or to a type in 'goodOnes'.
- /// Returns 'true' if that is the case.
+ /// Returns 'true' and sets dt.DefaultCtor if that is the case.
/// </summary>
bool StratosphereCheck(DatatypeDecl! dt, Graph<DatatypeDecl!>! dependencies, List<DatatypeDecl!>! goodOnes) {
// Stated differently, check that there is some constuctor where no argument type goes to the same stratum.
@@ -324,6 +324,7 @@ namespace Microsoft.Dafny { }
}
// this constructor satisfies the requirements, so the datatype is allowed
+ dt.DefaultCtor = ctor;
return true;
NEXT_OUTER_ITERATION: {}
}
@@ -334,10 +335,14 @@ namespace Microsoft.Dafny { void ResolveAttributes(Attributes attrs, bool twoState) {
// order does not matter for resolution, so resolve them in reverse order
for (; attrs != null; attrs = attrs.Prev) {
- foreach (Attributes.Argument aa in attrs.Args) {
- if (aa.E != null) {
- ResolveExpression(aa.E, twoState, true);
- }
+ ResolveAttributeArgs(attrs.Args, twoState, true);
+ }
+ }
+
+ void ResolveAttributeArgs(List<Attributes.Argument!>! args, bool twoState, bool specContext) {
+ foreach (Attributes.Argument aa in args) {
+ if (aa.E != null) {
+ ResolveExpression(aa.E, twoState, specContext);
}
}
}
@@ -792,6 +797,7 @@ namespace Microsoft.Dafny { {
if (stmt is UseStmt) {
UseStmt s = (UseStmt)stmt;
+ s.IsGhost = true;
ResolveExpression(s.Expr, true, true);
assert s.Expr.Type != null; // follows from postcondition of ResolveExpression
Expression expr = s.Expr;
@@ -808,12 +814,17 @@ namespace Microsoft.Dafny { }
} else if (stmt is PredicateStmt) {
PredicateStmt s = (PredicateStmt)stmt;
+ s.IsGhost = true;
ResolveExpression(s.Expr, true, true);
assert s.Expr.Type != null; // follows from postcondition of ResolveExpression
if (!UnifyTypes(s.Expr.Type, Type.Bool)) {
Error(s.Expr, "condition is expected to be of type {0}, but is {1}", Type.Bool, s.Expr.Type);
}
-
+
+ } else if (stmt is PrintStmt) {
+ PrintStmt s = (PrintStmt)stmt;
+ ResolveAttributeArgs(s.Args, false, false);
+
} else if (stmt is BreakStmt) {
BreakStmt s = (BreakStmt)stmt;
if (s.TargetLabel != null) {
@@ -852,15 +863,17 @@ namespace Microsoft.Dafny { Error(stmt, "Assignment to field must have an expression RHS; try using a temporary local variable");
} else {
FieldSelectExpr fse = (FieldSelectExpr)s.Lhs;
- lvalueIsGhost = ((!)fse.Field).IsGhost;
- if (!lvalueIsGhost) {
- if (specContextOnly) {
- Error(stmt, "Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");
- } else {
- // It is now that we wish we would have resolved s.Lhs to not allow ghosts. Too late, so we do
- // the next best thing.
- if (lhsResolvedSuccessfully && UsesSpecFeatures(fse.Obj)) {
- Error(stmt, "Assignment to non-ghost field is not allowed to use specification-only expressions in the receiver");
+ if (fse.Field != null) { // otherwise, an error was reported above
+ lvalueIsGhost = fse.Field.IsGhost;
+ if (!lvalueIsGhost) {
+ if (specContextOnly) {
+ Error(stmt, "Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");
+ } else {
+ // It is now that we wish we would have resolved s.Lhs to not allow ghosts. Too late, so we do
+ // the next best thing.
+ if (lhsResolvedSuccessfully && UsesSpecFeatures(fse.Obj)) {
+ Error(stmt, "Assignment to non-ghost field is not allowed to use specification-only expressions in the receiver");
+ }
}
}
}
@@ -869,6 +882,7 @@ namespace Microsoft.Dafny { Error(stmt, "LHS of assignment must denote a mutable variable or field");
}
+ s.IsGhost = lvalueIsGhost;
if (s.Rhs is ExprRhs) {
ExprRhs rr = (ExprRhs)s.Rhs;
ResolveExpression(rr.Expr, true, lvalueIsGhost);
@@ -941,6 +955,7 @@ namespace Microsoft.Dafny { } else {
callee = (Method)member;
s.Method = callee;
+ s.IsGhost = callee.IsGhost;
if (specContextOnly && !callee.IsGhost) {
Error(s, "only ghost methods can be called from this context");
}
@@ -1062,6 +1077,7 @@ namespace Microsoft.Dafny { branchesAreSpecOnly = UsesSpecFeatures(s.Guard);
}
}
+ s.IsGhost = branchesAreSpecOnly;
ResolveStatement(s.Thn, branchesAreSpecOnly, method);
if (s.Els != null) {
ResolveStatement(s.Els, branchesAreSpecOnly, method);
@@ -1093,6 +1109,7 @@ namespace Microsoft.Dafny { ResolveExpression(e, true, true);
// any type is fine
}
+ s.IsGhost = bodyIsSpecOnly;
ResolveStatement(s.Body, bodyIsSpecOnly, method);
} else if (stmt is ForeachStmt) {
@@ -1123,6 +1140,7 @@ namespace Microsoft.Dafny { bool specOnly = specContextOnly ||
(successfullyResolvedCollectionAndRange && (UsesSpecFeatures(s.Collection) || UsesSpecFeatures(s.Range)));
+ s.IsGhost = specOnly;
ResolveStatement(s.BodyAssign, specOnly, method);
// check for correct usage of BoundVar in LHS and RHS of this assignment
FieldSelectExpr lhs = s.BodyAssign.Lhs as FieldSelectExpr;
@@ -1166,6 +1184,7 @@ namespace Microsoft.Dafny { subst.Add(dtd.TypeArgs[i], sourceType.TypeArgs[i]);
}
}
+ s.IsGhost = bodyIsSpecOnly;
Dictionary<string!,object> memberNamesUsed = new Dictionary<string!,object>(); // this is really a set
foreach (MatchCaseStmt mc in s.Cases) {
@@ -1201,10 +1220,12 @@ namespace Microsoft.Dafny { }
ResolveType(v.Type);
if (ctor != null && i < ctor.Formals.Count) {
- Type st = SubstType(ctor.Formals[i].Type, subst);
+ Formal formal = ctor.Formals[i];
+ Type st = SubstType(formal.Type, subst);
if (!UnifyTypes(v.Type, st)) {
Error(stmt, "the declared type of the formal ({0}) does not agree with the corresponding type in the constructor's signature ({1})", v.Type, st);
}
+ v.IsGhost = formal.IsGhost;
}
i++;
}
@@ -1378,6 +1399,7 @@ namespace Microsoft.Dafny { for (int i = 0; i < dt.TypeArgs.Count; i++) {
Type t = new InferredTypeProxy();
gt.Add(t);
+ dtv.InferredTypeArgs.Add(t);
subst.Add(dt.TypeArgs[i], t);
}
expr.Type = new UserDefinedType(dtv.tok, dtv.DatatypeName, gt);
@@ -1394,15 +1416,18 @@ namespace Microsoft.Dafny { }
// add the constructor's own type parameters to the substitution map
foreach (TypeParameter p in ctor.TypeArgs) {
- subst.Add(p, new ParamTypeProxy(p));
+ Type t = new ParamTypeProxy(p);
+ dtv.InferredTypeArgs.Add(t);
+ subst.Add(p, t);
}
}
int j = 0;
foreach (Expression arg in dtv.Arguments) {
- ResolveExpression(arg, twoState, specContext);
+ Formal formal = ctor != null && j < ctor.Formals.Count ? ctor.Formals[j] : null;
+ ResolveExpression(arg, twoState, specContext || (formal != null && formal.IsGhost));
assert arg.Type != null; // follows from postcondition of ResolveExpression
- if (ctor != null && j < ctor.Formals.Count) {
- Type st = SubstType(ctor.Formals[j].Type, subst);
+ if (formal != null) {
+ Type st = SubstType(formal.Type, subst);
if (!UnifyTypes(arg.Type, st)) {
Error(arg.tok, "incorrect type of datatype constructor argument (found {0}, expected {1})", arg.Type, st);
}
@@ -1841,10 +1866,12 @@ namespace Microsoft.Dafny { }
ResolveType(v.Type);
if (ctor != null && i < ctor.Formals.Count) {
- Type st = SubstType(ctor.Formals[i].Type, subst);
+ Formal formal = ctor.Formals[i];
+ Type st = SubstType(formal.Type, subst);
if (!UnifyTypes(v.Type, st)) {
Error(expr, "the declared type of the formal ({0}) does not agree with the corresponding type in the constructor's signature ({1})", v.Type, st);
}
+ v.IsGhost = formal.IsGhost;
}
i++;
}
diff --git a/Source/Dafny/Scanner.ssc b/Source/Dafny/Scanner.ssc index 8c7a1b15..7e954005 100644 --- a/Source/Dafny/Scanner.ssc +++ b/Source/Dafny/Scanner.ssc @@ -133,7 +133,7 @@ public class Scanner { start[8804] = 38;
start[8805] = 39;
}
- const int noSym = 96;
+ const int noSym = 97;
static short[] start = new short[16385];
@@ -313,15 +313,16 @@ public class Scanner { case "in": t.kind = 51; break;
case "assert": t.kind = 53; break;
case "assume": t.kind = 54; break;
- case "then": t.kind = 55; break;
- case "false": t.kind = 79; break;
- case "true": t.kind = 80; break;
- case "null": t.kind = 81; break;
- case "fresh": t.kind = 84; break;
- case "this": t.kind = 88; break;
- case "old": t.kind = 89; break;
- case "forall": t.kind = 90; break;
- case "exists": t.kind = 92; break;
+ case "print": t.kind = 55; break;
+ case "then": t.kind = 56; break;
+ case "false": t.kind = 80; break;
+ case "true": t.kind = 81; break;
+ case "null": t.kind = 82; break;
+ case "fresh": t.kind = 85; break;
+ case "this": t.kind = 89; break;
+ case "old": t.kind = 90; break;
+ case "forall": t.kind = 91; break;
+ case "exists": t.kind = 93; break;
default: break;
}
@@ -387,83 +388,83 @@ public class Scanner { else {t.kind = 52; goto done;}
case 19:
if (ch == '=') {buf.Append(ch); NextCh(); goto case 20;}
- else {t.kind = 65; goto done;}
+ else {t.kind = 66; goto done;}
case 20:
if (ch == '>') {buf.Append(ch); NextCh(); goto case 21;}
else {t.kind = noSym; goto done;}
case 21:
- {t.kind = 56; goto done;}
- case 22:
{t.kind = 57; goto done;}
+ case 22:
+ {t.kind = 58; goto done;}
case 23:
if (ch == '>') {buf.Append(ch); NextCh(); goto case 24;}
- else {t.kind = 64; goto done;}
+ else {t.kind = 65; goto done;}
case 24:
- {t.kind = 58; goto done;}
- case 25:
{t.kind = 59; goto done;}
+ case 25:
+ {t.kind = 60; goto done;}
case 26:
if (ch == '&') {buf.Append(ch); NextCh(); goto case 27;}
else {t.kind = noSym; goto done;}
case 27:
- {t.kind = 60; goto done;}
- case 28:
{t.kind = 61; goto done;}
- case 29:
+ case 28:
{t.kind = 62; goto done;}
- case 30:
+ case 29:
{t.kind = 63; goto done;}
+ case 30:
+ {t.kind = 64; goto done;}
case 31:
- {t.kind = 66; goto done;}
+ {t.kind = 67; goto done;}
case 32:
if (ch == '=') {buf.Append(ch); NextCh(); goto case 33;}
else if (ch == '!') {buf.Append(ch); NextCh(); goto case 34;}
else if (ch == 'i') {buf.Append(ch); NextCh(); goto case 35;}
- else {t.kind = 77; goto done;}
+ else {t.kind = 78; goto done;}
case 33:
- {t.kind = 67; goto done;}
- case 34:
{t.kind = 68; goto done;}
+ case 34:
+ {t.kind = 69; goto done;}
case 35:
if (ch == 'n') {buf.Append(ch); NextCh(); goto case 36;}
else {t.kind = noSym; goto done;}
case 36:
- {t.kind = 69; goto done;}
- case 37:
{t.kind = 70; goto done;}
- case 38:
+ case 37:
{t.kind = 71; goto done;}
- case 39:
+ case 38:
{t.kind = 72; goto done;}
- case 40:
+ case 39:
{t.kind = 73; goto done;}
- case 41:
+ case 40:
{t.kind = 74; goto done;}
- case 42:
+ case 41:
{t.kind = 75; goto done;}
- case 43:
+ case 42:
{t.kind = 76; goto done;}
+ case 43:
+ {t.kind = 77; goto done;}
case 44:
- {t.kind = 78; goto done;}
+ {t.kind = 79; goto done;}
case 45:
- {t.kind = 82; goto done;}
+ {t.kind = 83; goto done;}
case 46:
if (ch == '.') {buf.Append(ch); NextCh(); goto case 49;}
- else {t.kind = 83; goto done;}
+ else {t.kind = 84; goto done;}
case 47:
- {t.kind = 85; goto done;}
- case 48:
{t.kind = 86; goto done;}
- case 49:
+ case 48:
{t.kind = 87; goto done;}
+ case 49:
+ {t.kind = 88; goto done;}
case 50:
- {t.kind = 91; goto done;}
+ {t.kind = 92; goto done;}
case 51:
- {t.kind = 93; goto done;}
- case 52:
{t.kind = 94; goto done;}
- case 53:
+ case 52:
{t.kind = 95; goto done;}
+ case 53:
+ {t.kind = 96; goto done;}
case 54: {t.kind = 0; goto done;}
}
done:
diff --git a/Source/Dafny/Translator.ssc b/Source/Dafny/Translator.ssc index 58350c24..763ed8c9 100644 --- a/Source/Dafny/Translator.ssc +++ b/Source/Dafny/Translator.ssc @@ -1797,6 +1797,15 @@ namespace Microsoft.Dafny { // Skip the totality check. This makes the 'use' statement easier to use and it has no executable analog anyhow
// builder.Add(Assert(stmt.Tok, IsTotal(s.Expr, etran), "use expression must be well defined")); // totality check
builder.Add(new Bpl.AssumeCmd(stmt.Tok, (s.EvalInOld ? etran.Old : etran).TrUseExpr(s.FunctionCallExpr)));
+ } else if (stmt is PrintStmt) {
+ AddComment(builder, stmt, "print statement");
+ PrintStmt s = (PrintStmt)stmt;
+ foreach (Attributes.Argument arg in s.Args) {
+ if (arg.E != null) {
+ builder.Add(AssertNS(stmt.Tok, IsTotal(arg.E, etran), "print expression must be well defined")); // totality check
+ }
+ }
+
} else if (stmt is LabelStmt) {
AddComment(builder, stmt, "label statement"); // TODO: ouch, comments probably mess up what the label labels in the Boogie program
builder.AddLabelCmd(((LabelStmt)stmt).Label);
diff --git a/Source/DafnyDriver/DafnyDriver.ssc b/Source/DafnyDriver/DafnyDriver.ssc index dc6e20b4..f6e10e59 100644 --- a/Source/DafnyDriver/DafnyDriver.ssc +++ b/Source/DafnyDriver/DafnyDriver.ssc @@ -229,8 +229,24 @@ namespace Microsoft.Boogie int errorCount, verified, inconclusives, timeOuts, outOfMemories;
PipelineOutcome oc = BoogiePipelineWithRerun(boogieProgram, bplFilename, null/*new ErrorReporter()*/, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories);
switch (oc) {
- case PipelineOutcome.Done:
case PipelineOutcome.VerificationCompleted:
+ if (CommandLineOptions.Clo.Compile) {
+ string targetFilename = "out.cs";
+ using (TextWriter target = new StreamWriter(new FileStream(targetFilename, System.IO.FileMode.Create))) {
+ Dafny.Compiler compiler = new Dafny.Compiler(target);
+ compiler.Compile(dafnyProgram);
+ WriteTrailer(verified, errorCount, inconclusives, timeOuts, outOfMemories);
+ if (compiler.ErrorCount == 0) {
+ Console.WriteLine("Compiled program written to {0}", targetFilename);
+ } else {
+ Console.WriteLine("File {0} contains the partially compiled program", targetFilename);
+ }
+ }
+ } else {
+ WriteTrailer(verified, errorCount, inconclusives, timeOuts, outOfMemories);
+ }
+ break;
+ case PipelineOutcome.Done:
WriteTrailer(verified, errorCount, inconclusives, timeOuts, outOfMemories);
break;
default:
diff --git a/Test/VSI-Benchmarks/Answer b/Test/VSI-Benchmarks/Answer index a0ae9d01..926a4da3 100644 --- a/Test/VSI-Benchmarks/Answer +++ b/Test/VSI-Benchmarks/Answer @@ -1,11 +1,11 @@ -------------------- b1.dfy --------------------
-Dafny program verifier finished with 4 verified, 0 errors
+Dafny program verifier finished with 10 verified, 0 errors
-------------------- b2.dfy --------------------
-Dafny program verifier finished with 6 verified, 0 errors
+Dafny program verifier finished with 8 verified, 0 errors
-------------------- b3.dfy --------------------
diff --git a/Test/VSI-Benchmarks/b1.dfy b/Test/VSI-Benchmarks/b1.dfy index 70522aaf..1ab76a78 100644 --- a/Test/VSI-Benchmarks/b1.dfy +++ b/Test/VSI-Benchmarks/b1.dfy @@ -47,4 +47,29 @@ class Benchmark1 { call r := Add(r, y);
}
}
+
+ method Main() {
+ call TestAdd(3, 180);
+ call TestAdd(3, -180);
+ call TestAdd(0, 1);
+
+ call TestMul(3, 180);
+ call TestMul(3, -180);
+ call TestMul(180, 3);
+ call TestMul(-180, 3);
+ call TestMul(0, 1);
+ call TestMul(1, 0);
+ }
+
+ method TestAdd(x: int, y: int) {
+ print x, " + ", y, " = ";
+ call z := Add(x, y);
+ print z, "\n";
+ }
+
+ method TestMul(x: int, y: int) {
+ print x, " * ", y, " = ";
+ call z := Mul(x, y);
+ print z, "\n";
+ }
}
diff --git a/Test/VSI-Benchmarks/b2.dfy b/Test/VSI-Benchmarks/b2.dfy index 7d964061..0cae993a 100644 --- a/Test/VSI-Benchmarks/b2.dfy +++ b/Test/VSI-Benchmarks/b2.dfy @@ -1,6 +1,4 @@ -// Note: There is a bug in the well-formedness of functions. In particular,
-// it doesn't look at the requires clause (in the proper way). Fixed!
// Note:Implemented arrays as Dafny does not provide them
class Benchmark2 {
@@ -40,10 +38,21 @@ class Benchmark2 { class Array {
var contents: seq<int>;
- method Init(n: int);
+ method Init(n: int)
requires 0 <= n;
modifies this;
ensures |contents| == n;
+ {
+ var i := 0;
+ contents := [];
+ while (i < n)
+ invariant i <= n && i == |contents|;
+ decreases n - i;
+ {
+ contents := contents + [0];
+ i := i + 1;
+ }
+ }
function method Length(): int
reads this;
{ |contents| }
@@ -51,11 +60,47 @@ class Array { requires 0 <= i && i < |contents|;
reads this;
{ contents[i] }
- method Set(i: int, x: int);
+ method Set(i: int, x: int)
requires 0 <= i && i < |contents|;
modifies this;
ensures |contents| == |old(contents)|;
ensures contents[..i] == old(contents[..i]);
ensures contents[i] == x;
ensures contents[i+1..] == old(contents[i+1..]);
+ {
+ contents := contents[i := x];
+ }
+}
+
+/******
+method Main() {
+ var a := new Array;
+ call a.Init(5);
+ call a.Set(0, -4);
+ call a.Set(1, -2);
+ call a.Set(2, -2);
+ call a.Set(3, 0);
+ call a.Set(4, 25);
+ call TestSearch(a, 4);
+ call TestSearch(a, -8);
+ call TestSearch(a, -2);
+ call TestSearch(a, 0);
+ call TestSearch(a, 23);
+ call TestSearch(a, 25);
+ call TestSearch(a, 27);
+}
+
+method TestSearch(a: Array, key: int)
+ requires a != null;
+ requires (forall i, j ::
+ 0 <= i && i < j && j < a.Length() ==> a.Get(i) <= a.Get(j));
+{
+ assert (forall i, j ::
+ 0 <= i && i < j && j < a.Length() ==> a.Get(i) <= a.Get(j));
+ var b := new Benchmark2;
+ assert (forall i, j ::
+ 0 <= i && i < j && j < a.Length() ==> a.Get(i) <= a.Get(j));
+ call r := b.BinarySearch(a, key);
+ print "Looking for key=", key, ", result=", r, "\n";
}
+******/
diff --git a/Test/VSI-Benchmarks/b5.dfy b/Test/VSI-Benchmarks/b5.dfy index 2e274845..94fe1eaa 100644 --- a/Test/VSI-Benchmarks/b5.dfy +++ b/Test/VSI-Benchmarks/b5.dfy @@ -4,9 +4,9 @@ class Queue<T> { var head: Node<T>;
var tail: Node<T>;
- var contents: seq<T>;
- var footprint: set<object>;
- var spine: set<Node<T>>;
+ ghost var contents: seq<T>;
+ ghost var footprint: set<object>;
+ ghost var spine: set<Node<T>>;
function Valid(): bool
reads this, footprint;
@@ -124,8 +124,8 @@ class Node<T> { var data: T;
var next: Node<T>;
- var tailContents: seq<T>;
- var footprint: set<object>;
+ ghost var tailContents: seq<T>;
+ ghost var footprint: set<object>;
function Valid(): bool
reads this, footprint;
diff --git a/Test/VSI-Benchmarks/b6.dfy b/Test/VSI-Benchmarks/b6.dfy index 90f484bd..9b244e69 100644 --- a/Test/VSI-Benchmarks/b6.dfy +++ b/Test/VSI-Benchmarks/b6.dfy @@ -1,51 +1,51 @@ class Collection<T> {
- var footprint:set<object>;
+ ghost var footprint:set<object>;
var elements:seq<T>;
function Valid():bool
- reads this, footprint;
+ reads this, footprint;
{
this in footprint
}
method GetCount() returns (c:int)
- requires Valid();
- ensures 0<=c;
+ requires Valid();
+ ensures 0<=c;
{
c:=|elements|;
}
method Init()
- modifies this;
- ensures Valid() && fresh(footprint -{this});
+ modifies this;
+ ensures Valid() && fresh(footprint -{this});
{
elements := [];
footprint := {this};
}
method GetItem(i:int ) returns (x:T)
- requires Valid();
- requires 0<=i && i<|elements|;
- ensures elements[i] ==x;
+ requires Valid();
+ requires 0<=i && i<|elements|;
+ ensures elements[i] ==x;
{
x:=elements[i];
}
method Add(x:T )
- requires Valid();
- modifies footprint;
- ensures Valid() && fresh(footprint - old(footprint));
- ensures elements == old(elements) + [x];
+ requires Valid();
+ modifies footprint;
+ ensures Valid() && fresh(footprint - old(footprint));
+ ensures elements == old(elements) + [x];
{
elements:= elements + [x];
}
method GetIterator() returns (iter:Iterator<T>)
- requires Valid();
- ensures iter != null && iter.Valid();
- ensures fresh(iter.footprint) && iter.pos == -1;
- ensures iter.c == this;
+ requires Valid();
+ ensures iter != null && iter.Valid();
+ ensures fresh(iter.footprint) && iter.pos == -1;
+ ensures iter.c == this;
{
iter:= new Iterator<T>;
call iter.Init(this);
@@ -58,49 +58,48 @@ class Iterator<T> { var c:Collection<T>;
var pos:int;
- var footprint:set<object>;
+ ghost var footprint:set<object>;
function Valid():bool
- reads this, footprint;
+ reads this, footprint;
{
- this in footprint && c!= null && -1<= pos && null !in footprint
+ this in footprint && c != null && -1 <= pos && null !in footprint
}
method Init(coll:Collection<T>)
- requires coll != null;
- modifies this;
- ensures Valid() && fresh(footprint -{this}) && pos ==-1;
- ensures c == coll;
+ requires coll != null;
+ modifies this;
+ ensures Valid() && fresh(footprint - {this}) && pos == -1;
+ ensures c == coll;
{
- c:= coll;
- pos:=-1;
+ c := coll;
+ pos := -1;
footprint := {this};
}
method MoveNext() returns (b:bool)
- requires Valid();
- modifies footprint;
- ensures fresh(footprint - old(footprint)) && Valid() && pos == old(pos) + 1;
- ensures b == HasCurrent() && c == old(c);
+ requires Valid();
+ modifies footprint;
+ ensures fresh(footprint - old(footprint)) && Valid() && pos == old(pos) + 1;
+ ensures b == HasCurrent() && c == old(c);
{
- pos:= pos+1;
- b:= pos < |c.elements|;
+ pos := pos+1;
+ b := pos < |c.elements|;
}
- function HasCurrent():bool //???
- requires Valid();
- reads this, c;
- {
- 0<= pos && pos < |c.elements|
- }
-
- method GetCurrent() returns (x:T)
- requires Valid() && HasCurrent();
- ensures c.elements[pos] == x;
+ function HasCurrent():bool //???
+ requires Valid();
+ reads this, c;
{
- x:=c.elements[pos];
+ 0 <= pos && pos < |c.elements|
}
+ method GetCurrent() returns (x:T)
+ requires Valid() && HasCurrent();
+ ensures c.elements[pos] == x;
+ {
+ x := c.elements[pos];
+ }
}
class Client
@@ -108,13 +107,13 @@ class Client method Main()
{
- var c:= new Collection<int>;
+ var c := new Collection<int>;
call c.Init();
call c.Add(33);
call c.Add(45);
call c.Add(78);
- var s:= [ ];
+ var s := [];
call iter := c.GetIterator();
call b := iter.MoveNext();
@@ -126,9 +125,9 @@ class Client invariant iter.c == c;
decreases |c.elements| - iter.pos;
{
- call x:= iter.GetCurrent();
- s:= s + [x];
- call b:= iter.MoveNext();
+ call x := iter.GetCurrent();
+ s := s + [x];
+ call b := iter.MoveNext();
}
assert s == c.elements; //verifies that the iterator returns the correct things
@@ -136,4 +135,3 @@ class Client }
}
-
diff --git a/Test/VSI-Benchmarks/b7.dfy b/Test/VSI-Benchmarks/b7.dfy index ddad7599..e5af6357 100644 --- a/Test/VSI-Benchmarks/b7.dfy +++ b/Test/VSI-Benchmarks/b7.dfy @@ -29,84 +29,78 @@ class Queue<T> { }
class Stream {
- var footprint:set<object>;
+ ghost var footprint:set<object>;
var stream:seq<int>;
var isOpen:bool;
function Valid():bool
- reads this, footprint;
+ reads this, footprint;
{
- null !in footprint && this in footprint && isOpen
+ null !in footprint && this in footprint && isOpen
}
method GetCount() returns (c:int)
- requires Valid();
- ensures 0<=c;
+ requires Valid();
+ ensures 0 <= c;
{
- c:=|stream|;
+ c := |stream|;
}
method Create() //writing
- modifies this;
- ensures Valid() && fresh(footprint -{this});
- ensures stream == [];
+ modifies this;
+ ensures Valid() && fresh(footprint - {this});
+ ensures stream == [];
{
- stream := [];
- footprint := {this};
- isOpen:= true;
+ stream := [];
+ footprint := {this};
+ isOpen := true;
}
method Open() //reading
- modifies this;
- ensures Valid() && fresh(footprint -{this});
+ modifies this;
+ ensures Valid() && fresh(footprint - {this});
{
- footprint := {this};
- isOpen :=true;
+ footprint := {this};
+ isOpen := true;
}
method PutChar(x:int )
- requires Valid();
- modifies footprint;
- ensures Valid() && fresh(footprint - old(footprint));
- ensures stream == old(stream) + [x];
+ requires Valid();
+ modifies footprint;
+ ensures Valid() && fresh(footprint - old(footprint));
+ ensures stream == old(stream) + [x];
{
- stream:= stream + [x];
+ stream:= stream + [x];
}
method GetChar()returns(x:int)
- requires Valid() && 0< |stream|;
- modifies footprint;
- ensures Valid() && fresh(footprint - old(footprint));
- ensures x ==old(stream)[0];
- ensures stream == old(stream)[1..];
+ requires Valid() && 0 < |stream|;
+ modifies footprint;
+ ensures Valid() && fresh(footprint - old(footprint));
+ ensures x ==old(stream)[0];
+ ensures stream == old(stream)[1..];
{
- x := stream[0];
- stream:= stream[1..];
-
+ x := stream[0];
+ stream := stream[1..];
}
- method AtEndOfStream() returns(eos:bool)
- requires Valid();
- ensures eos <==> |stream| ==0;
- {
- eos:= |stream| ==0;
- }
-
- method Close()
- requires Valid();
- modifies footprint;
- {
- isOpen := false;
-
- }
+ method AtEndOfStream() returns(eos:bool)
+ requires Valid();
+ ensures eos <==> |stream| == 0;
+ {
+ eos := |stream| == 0;
+ }
+ method Close()
+ requires Valid();
+ modifies footprint;
+ {
+ isOpen := false;
+ }
}
-
class Client {
-
-
method Sort(q: Queue<int>) returns (r: Queue<int>, perm:seq<int>);
requires q != null;
modifies q;
@@ -115,49 +109,44 @@ class Client { ensures (forall i, j :: 0 <= i && i < j && j < |r.contents| ==>
r.Get(i) <= r.Get(j));
//perm is a permutation
- ensures |perm| == |r.contents|; // ==|pperm|
- ensures (forall i: int :: 0 <= i && i < |perm|==> 0 <= perm[i] && perm[i] < |perm| );
- ensures (forall i, j: int :: 0 <= i && i < j && j < |perm| ==> perm[i] != perm[j]);
- // the final Queue is a permutation of the input Queue
- ensures (forall i: int :: 0 <= i && i < |perm| ==> r.contents[i] == old(q.contents)[perm[i]]);
+ ensures |perm| == |r.contents|; // ==|pperm|
+ ensures (forall i: int :: 0 <= i && i < |perm|==> 0 <= perm[i] && perm[i] < |perm| );
+ ensures (forall i, j: int :: 0 <= i && i < j && j < |perm| ==> perm[i] != perm[j]);
+ // the final Queue is a permutation of the input Queue
+ ensures (forall i: int :: 0 <= i && i < |perm| ==> r.contents[i] == old(q.contents)[perm[i]]);
-
- method Main()
- {
- var rd:= new Stream;
- call rd.Open();
-
- var q:= new Queue<int>;
- while (true)
- invariant rd.Valid() && fresh(rd.footprint) && fresh(q);
- decreases |rd.stream|;
- {
- call eos := rd.AtEndOfStream();
- if (eos)
- {
- break;
- }
-
- call ch := rd.GetChar();
- call q.Enqueue(ch);
- }
-
- call rd.Close();
- call q,perm := Sort(q);
-
- var wr:= new Stream;
- call wr.Create();
- while (0<|q.contents|)
- invariant wr.Valid() && fresh(wr.footprint) && fresh(q) && q !in wr.footprint;
- decreases |q.contents|;
- {
- call ch:= q.Dequeue();
- call wr.PutChar(ch);
- }
- call wr.Close();
-
- }
-
+ method Main()
+ {
+ var rd := new Stream;
+ call rd.Open();
+
+ var q := new Queue<int>;
+ while (true)
+ invariant rd.Valid() && fresh(rd.footprint) && fresh(q);
+ decreases |rd.stream|;
+ {
+ call eos := rd.AtEndOfStream();
+ if (eos) {
+ break;
+ }
+
+ call ch := rd.GetChar();
+ call q.Enqueue(ch);
+ }
+
+ call rd.Close();
+ call q,perm := Sort(q);
+
+ var wr:= new Stream;
+ call wr.Create();
+ while (0 < |q.contents|)
+ invariant wr.Valid() && fresh(wr.footprint) && fresh(q) && q !in wr.footprint;
+ decreases |q.contents|;
+ {
+ call ch := q.Dequeue();
+ call wr.PutChar(ch);
+ }
+ call wr.Close();
+ }
}
-
diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy index fec36c29..d8ee2013 100644 --- a/Test/VSI-Benchmarks/b8.dfy +++ b/Test/VSI-Benchmarks/b8.dfy @@ -155,7 +155,7 @@ class Word }
class ReaderStream {
- var footprint:set<object>;
+ ghost var footprint:set<object>;
var isOpen:bool;
function Valid():bool
@@ -188,7 +188,7 @@ class ReaderStream { }
class WriterStream {
- var footprint:set<object>;
+ ghost var footprint:set<object>;
var stream:seq<int>;
var isOpen:bool;
diff --git a/Test/VSI-Benchmarks/runtest.bat b/Test/VSI-Benchmarks/runtest.bat index fa737dca..0cd898c4 100644 --- a/Test/VSI-Benchmarks/runtest.bat +++ b/Test/VSI-Benchmarks/runtest.bat @@ -11,5 +11,5 @@ for %%f in ( b1.dfy b2.dfy b3.dfy b4.dfy b5.dfy b6.dfy b7.dfy b8.dfy ) do (
echo.
echo -------------------- %%f --------------------
- %DAFNY_EXE% %* %%f
+ %DAFNY_EXE% /compile:0 %* %%f
)
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 0a419802..3718618e 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -272,7 +272,7 @@ Modules0.dfy(24,7): Error: import graph contains a cycle: H -> I -> J -> G Modules0.dfy(51,6): Error: inter-module calls must follow the module import relation (so module X2 must transitively import YY)
Modules0.dfy(62,6): Error: inter-module calls must follow the module import relation (so module X1 must transitively import X2)
Modules0.dfy(72,6): Error: inter-module calls must follow the module import relation (so module X0 must transitively import X1)
-Modules0.dfy(91,4): Error: inter-module calls must follow the module import relation (so module $default must transitively import YY)
+Modules0.dfy(91,4): Error: inter-module calls must follow the module import relation (so module _default must transitively import YY)
7 resolution/type errors detected in Modules0.dfy
-------------------- Modules1.dfy --------------------
diff --git a/Test/dafny0/Queue.dfy b/Test/dafny0/Queue.dfy index a87bfc0d..42b7dd64 100644 --- a/Test/dafny0/Queue.dfy +++ b/Test/dafny0/Queue.dfy @@ -6,9 +6,9 @@ class Queue<T> { var head: Node<T>;
var tail: Node<T>;
- var contents: seq<T>;
- var footprint: set<object>;
- var spine: set<Node<T>>;
+ ghost var contents: seq<T>;
+ ghost var footprint: set<object>;
+ ghost var spine: set<Node<T>>;
function Valid(): bool
reads this, footprint;
@@ -124,8 +124,8 @@ class Node<T> { var data: T;
var next: Node<T>;
- var tailContents: seq<T>;
- var footprint: set<object>;
+ ghost var tailContents: seq<T>;
+ ghost var footprint: set<object>;
function Valid(): bool
reads this, footprint;
diff --git a/Test/dafny0/Substitution.dfy b/Test/dafny0/Substitution.dfy index f68d7eea..195c9257 100644 --- a/Test/dafny0/Substitution.dfy +++ b/Test/dafny0/Substitution.dfy @@ -46,7 +46,7 @@ static ghost method Lemma(l: List, v: int, val: int) case Nil =>
case Cons(e, tail) =>
call Theorem(e, v, val);
- call Lemma(tail, v, val);
+ call Lemma(tail, v, val);
}
}
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index e467fd43..fd90e479 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -26,5 +26,5 @@ for %%f in (TypeTests.dfy SmallTests.dfy Definedness.dfy Tree.dfy) do (
echo.
echo -------------------- %%f --------------------
- %DAFNY_EXE% %* %%f
+ %DAFNY_EXE% /compile:0 %* %%f
)
diff --git a/Util/Emacs/boogie-mode.el b/Util/Emacs/boogie-mode.el index 1d8ffb05..d4902a74 100644 --- a/Util/Emacs/boogie-mode.el +++ b/Util/Emacs/boogie-mode.el @@ -36,7 +36,7 @@ )) . font-lock-builtin-face)
`(,(boogie-regexp-opt '(
"assert" "assume" "break" "call" "else" "havoc" "if" "goto" "return" "while"
- "old" "forall" "exists" "cast"
+ "old" "forall" "exists" "lambda" "cast"
"false" "true")) . font-lock-keyword-face)
`(,(boogie-regexp-opt '("bool" "int"
"bv0" "bv1" "bv2" "bv3" "bv4" "bv5" "bv6" "bv7" "bv8" "bv9"
diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el index da7e59e7..34fc96f2 100644 --- a/Util/Emacs/dafny-mode.el +++ b/Util/Emacs/dafny-mode.el @@ -36,7 +36,7 @@ "invariant" "decreases"
)) . font-lock-builtin-face)
`(,(dafny-regexp-opt '(
- "assert" "assume" "break" "call" "then" "else" "havoc" "if" "label" "return" "while"
+ "assert" "assume" "break" "call" "then" "else" "havoc" "if" "label" "return" "while" "print"
"old" "forall" "exists" "new" "foreach" "in" "this" "fresh" "use"
"match" "case" "false" "true" "null")) . font-lock-keyword-face)
`(,(dafny-regexp-opt '("bool" "int" "object" "set" "seq")) . font-lock-type-face)
diff --git a/Util/latex/boogie.sty b/Util/latex/boogie.sty index bda9f10a..30a18b82 100644 --- a/Util/latex/boogie.sty +++ b/Util/latex/boogie.sty @@ -53,6 +53,7 @@ {<==>}{$\Longleftrightarrow$}4
{forall}{$\forall$}1
{exists}{$\exists$}1
+ {lambda}{$\lambda$}1
% the following isn't actually Boogie, but it gives the option to produce nicer latex
{<<}{$\langle$}1
{>>}{$\rangle$}1
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty index 641584b6..2b9918f9 100644 --- a/Util/latex/dafny.sty +++ b/Util/latex/dafny.sty @@ -13,7 +13,7 @@ % expressions
match,case,false,true,null,old,fresh,this,
% statements
- assert,assume,new,havoc,call,if,then,else,while,invariant,break,return,foreach,
+ assert,assume,print,new,havoc,call,if,then,else,while,invariant,break,return,foreach,
},
literate=%
{:}{$\colon$}1
|