//----------------------------------------------------------------------------- // // Copyright (C) Microsoft Corporation. All Rights Reserved. // //----------------------------------------------------------------------------- using System; using System.IO; using System.Collections.Generic; using System.Diagnostics.Contracts; using System.Numerics; using System.Linq; using Bpl = Microsoft.Boogie; namespace Microsoft.Dafny { public class Printer { TextWriter wr; DafnyOptions.PrintModes printMode; [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(wr!=null); } public Printer(TextWriter wr, DafnyOptions.PrintModes printMode = DafnyOptions.PrintModes.Everything) { Contract.Requires(wr != null); this.wr = wr; this.printMode = printMode; } public static string ExprToString(Expression expr) { Contract.Requires(expr != null); using (var wr = new System.IO.StringWriter()) { var pr = new Printer(wr); pr.PrintExpression(expr, false); return wr.ToString(); } } public static string GuardToString(Expression expr) { using (var wr = new System.IO.StringWriter()) { var pr = new Printer(wr); pr.PrintGuard(expr); return wr.ToString(); } } public static string ExtendedExprToString(Expression expr) { Contract.Requires(expr != null); using (var wr = new System.IO.StringWriter()) { var pr = new Printer(wr); pr.PrintExtendedExpr(expr, 0, true, false); return wr.ToString(); } } public static string FrameExprListToString(List fexprs) { Contract.Requires(fexprs != null); using (var wr = new System.IO.StringWriter()) { var pr = new Printer(wr); pr.PrintFrameExpressionList(fexprs); return wr.ToString(); } } public static string StatementToString(Statement stmt) { Contract.Requires(stmt != null); using (var wr = new System.IO.StringWriter()) { var pr = new Printer(wr); pr.PrintStatement(stmt, 0); return ToStringWithoutNewline(wr); } } public static string IteratorClassToString(IteratorDecl iter) { Contract.Requires(iter != null); using (var wr = new System.IO.StringWriter()) { var pr = new Printer(wr); pr.PrintIteratorClass(iter, 0, null); return ToStringWithoutNewline(wr); } } public static string IteratorSignatureToString(IteratorDecl iter) { Contract.Requires(iter != null); using (var wr = new System.IO.StringWriter()) { var pr = new Printer(wr); pr.PrintIteratorSignature(iter, 0); return ToStringWithoutNewline(wr); } } public static string FunctionSignatureToString(Function f) { Contract.Requires(f != null); using (var wr = new System.IO.StringWriter()) { var pr = new Printer(wr); pr.PrintFunction(f, 0, true); return ToStringWithoutNewline(wr); } } public static string MethodSignatureToString(Method m) { Contract.Requires(m != null); using (var wr = new System.IO.StringWriter()) { var pr = new Printer(wr); pr.PrintMethod(m, 0, true); return ToStringWithoutNewline(wr); } } public static string ToStringWithoutNewline(System.IO.StringWriter wr) { Contract.Requires(wr != null); var sb = wr.GetStringBuilder(); var len = sb.Length; while (len > 0 && (sb[len - 1] == '\n' || sb[len - 1] == '\r')) { len--; } return sb.ToString(0, len); } public void PrintProgram(Program prog) { Contract.Requires(prog != null); if (Bpl.CommandLineOptions.Clo.ShowEnv != Bpl.CommandLineOptions.ShowEnvironment.Never) { wr.WriteLine("// " + Bpl.CommandLineOptions.Clo.Version); wr.WriteLine("// " + Bpl.CommandLineOptions.Clo.Environment); } wr.WriteLine("// {0}", prog.Name); if (DafnyOptions.O.DafnyPrintResolvedFile != null) { wr.WriteLine(); wr.WriteLine("/*"); PrintModuleDefinition(prog.BuiltIns.SystemModule, 0, Path.GetFullPath(DafnyOptions.O.DafnyPrintResolvedFile)); wr.WriteLine("*/"); } wr.WriteLine(); PrintCallGraph(prog.DefaultModuleDef, 0); PrintTopLevelDecls(prog.DefaultModuleDef.TopLevelDecls, 0, Path.GetFullPath(prog.FullName)); wr.Flush(); } public void PrintCallGraph(ModuleDefinition module, int indent) { Contract.Requires(module != null); Contract.Requires(0 <= indent); if (DafnyOptions.O.DafnyPrintResolvedFile != null) { // print call graph Indent(indent); wr.WriteLine("/* CALL GRAPH for module {0}:", module.Name); var SCCs = module.CallGraph.TopologicallySortedComponents(); SCCs.Reverse(); foreach (var clbl in SCCs) { Indent(indent); wr.WriteLine(" * SCC at height {0}:", module.CallGraph.GetSCCRepresentativeId(clbl)); var r = module.CallGraph.GetSCC(clbl); foreach (var m in r) { Indent(indent); wr.WriteLine(" * {0}", m.NameRelativeToModule); } } Indent(indent); wr.WriteLine(" */"); } } public void PrintTopLevelDecls(List decls, int indent, string fileBeingPrinted) { Contract.Requires(decls!= null); int i = 0; foreach (TopLevelDecl d in decls) { Contract.Assert(d != null); if (PrintModeSkipGeneral(d.tok, fileBeingPrinted)) { continue; } if (d is OpaqueTypeDecl) { var at = (OpaqueTypeDecl)d; if (i++ != 0) { wr.WriteLine(); } Indent(indent); PrintClassMethodHelper("type", at.Attributes, at.Name, new List()); wr.Write(EqualitySupportSuffix(at.EqualitySupport)); wr.WriteLine(); } else if (d is NewtypeDecl) { var dd = (NewtypeDecl)d; if (i++ != 0) { wr.WriteLine(); } Indent(indent); PrintClassMethodHelper("newtype", dd.Attributes, dd.Name, new List()); wr.Write(" = "); if (dd.Var == null) { PrintType(dd.BaseType); } else { wr.Write(dd.Var.DisplayName); if (!(dd.Var.Type is TypeProxy) || DafnyOptions.O.DafnyPrintResolvedFile != null) { wr.Write(": "); PrintType(dd.BaseType); } wr.Write(" | "); PrintExpression(dd.Constraint, true); } wr.WriteLine(); } else if (d is TypeSynonymDecl) { var syn = (TypeSynonymDecl)d; if (i++ != 0) { wr.WriteLine(); } Indent(indent); PrintClassMethodHelper("type", syn.Attributes, syn.Name, syn.TypeArgs); wr.Write(" = "); PrintType(syn.Rhs); wr.WriteLine(); } else if (d is DatatypeDecl) { if (i++ != 0) { wr.WriteLine(); } PrintDatatype((DatatypeDecl)d, indent); } else if (d is IteratorDecl) { var iter = (IteratorDecl)d; PrintIteratorSignature(iter, indent); if (iter.Body != null) { Indent(indent); PrintStatement(iter.Body, indent); wr.WriteLine(); } if (DafnyOptions.O.DafnyPrintResolvedFile != null) { // also print the members that were created as part of the interpretation of the iterator Contract.Assert(iter.Members.Count != 0); // filled in during resolution wr.WriteLine("/*---------- iterator members ----------"); PrintIteratorClass(iter, indent, fileBeingPrinted); wr.WriteLine("---------- iterator members ----------*/"); } } else if (d is ClassDecl) { ClassDecl cl = (ClassDecl)d; if (!cl.IsDefaultClass) { if (i++ != 0) { wr.WriteLine(); } PrintClass(cl, indent, fileBeingPrinted); } else if (cl.Members.Count == 0) { // print nothing } else { if (i++ != 0) { wr.WriteLine(); } PrintMembers(cl.Members, indent, fileBeingPrinted); } } else if (d is ModuleDecl) { wr.WriteLine(); Indent(indent); if (d is LiteralModuleDecl) { ModuleDefinition module = ((LiteralModuleDecl)d).ModuleDef; PrintModuleDefinition(module, indent, fileBeingPrinted); } else if (d is AliasModuleDecl) { wr.Write("import"); if (((AliasModuleDecl)d).Opened) wr.Write(" opened"); wr.Write(" {0} ", ((AliasModuleDecl)d).Name); wr.WriteLine("= {0}", Util.Comma(".", ((AliasModuleDecl)d).Path, id => id.val)); } else if (d is ModuleFacadeDecl) { wr.Write("import"); if (((ModuleFacadeDecl)d).Opened) wr.Write(" opened"); wr.Write(" {0} ", ((ModuleFacadeDecl)d).Name); wr.WriteLine("as {0}", Util.Comma(".", ((ModuleFacadeDecl)d).Path, id => id.val)); } } else { Contract.Assert(false); // unexpected TopLevelDecl } } } void PrintModuleDefinition(ModuleDefinition module, int indent, string fileBeingPrinted) { Contract.Requires(module != null); Contract.Requires(0 <= indent); if (module.IsAbstract) { wr.Write("abstract "); } wr.Write("module"); PrintAttributes(module.Attributes); wr.Write(" {0} ", module.Name); if (module.RefinementBaseName != null) { wr.Write("refines {0} ", Util.Comma(".", module.RefinementBaseName, id => id.val)); } if (module.TopLevelDecls.Count == 0) { wr.WriteLine("{ }"); } else { wr.WriteLine("{"); PrintCallGraph(module, indent + IndentAmount); PrintTopLevelDecls(module.TopLevelDecls, indent + IndentAmount, fileBeingPrinted); Indent(indent); wr.WriteLine("}"); } } void PrintIteratorSignature(IteratorDecl iter, int indent) { Indent(indent); PrintClassMethodHelper("iterator", iter.Attributes, iter.Name, iter.TypeArgs); if (iter.SignatureIsOmitted) { wr.WriteLine(" ..."); } else { PrintFormals(iter.Ins); if (iter.Outs.Count != 0) { if (iter.Ins.Count + iter.Outs.Count <= 3) { wr.Write(" yields "); } else { wr.WriteLine(); Indent(indent + 2 * IndentAmount); wr.Write("yields "); } PrintFormals(iter.Outs); } wr.WriteLine(); } int ind = indent + IndentAmount; PrintSpec("requires", iter.Requires, ind); if (iter.Reads.Expressions != null) { PrintFrameSpecLine("reads", iter.Reads.Expressions, ind, iter.Reads.HasAttributes() ? iter.Reads.Attributes : null); } if (iter.Modifies.Expressions != null) { PrintFrameSpecLine("modifies", iter.Modifies.Expressions, ind, iter.Modifies.HasAttributes() ? iter.Modifies.Attributes : null); } PrintSpec("yield requires", iter.YieldRequires, ind); PrintSpec("yield ensures", iter.YieldEnsures, ind); PrintSpec("ensures", iter.Ensures, ind); PrintDecreasesSpec(iter.Decreases, ind); } private void PrintIteratorClass(IteratorDecl iter, int indent, string fileBeingPrinted) { PrintClassMethodHelper("class", null, iter.Name, iter.TypeArgs); wr.WriteLine(" {"); PrintMembers(iter.Members, indent + IndentAmount, fileBeingPrinted); Indent(indent); wr.WriteLine("}"); } public void PrintClass(ClassDecl c, int indent, string fileBeingPrinted) { Contract.Requires(c != null); Indent(indent); PrintClassMethodHelper((c is TraitDecl) ? "trait" : "class", c.Attributes, c.Name, c.TypeArgs); string sep = " extends "; foreach (var trait in c.TraitsTyp) { wr.Write(sep); PrintType(trait); sep = ", "; } if (c.Members.Count == 0) { wr.WriteLine(" { }"); } else { wr.WriteLine(" {"); PrintMembers(c.Members, indent + IndentAmount, fileBeingPrinted); Indent(indent); wr.WriteLine("}"); } } public void PrintMembers(List members, int indent, string fileBeingPrinted) { Contract.Requires(members != null); int state = 0; // 0 - no members yet; 1 - previous member was a field; 2 - previous member was non-field foreach (MemberDecl m in members) { if (PrintModeSkipGeneral(m.tok, fileBeingPrinted)) { continue; } if (m is Method) { if (state != 0) { wr.WriteLine(); } PrintMethod((Method)m, indent, false); var com = m as FixpointLemma; if (com != null && com.PrefixLemma != null) { Indent(indent); wr.WriteLine("/***"); PrintMethod(com.PrefixLemma, indent, false); Indent(indent); wr.WriteLine("***/"); } state = 2; } else if (m is Field) { if (state == 2) { wr.WriteLine(); } PrintField((Field)m, indent); state = 1; } else if (m is Function) { if (state != 0) { wr.WriteLine(); } PrintFunction((Function)m, indent, false); var fixp = m as FixpointPredicate; if (fixp != null && fixp.PrefixPredicate != null) { Indent(indent); wr.WriteLine("/***"); PrintFunction(fixp.PrefixPredicate, indent, false); Indent(indent); wr.WriteLine("***/"); } state = 2; } else { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected member } } } /// /// Prints no space before "kind", but does print a space before "attrs" and "name". /// void PrintClassMethodHelper(string kind, Attributes attrs, string name, List typeArgs) { Contract.Requires(kind != null); Contract.Requires(name != null); Contract.Requires(typeArgs != null); if (kind.Length != 0) { wr.Write(kind); } PrintAttributes(attrs); wr.Write(" {0}", name); PrintTypeParams(typeArgs); } private void PrintTypeParams(List typeArgs) { Contract.Requires(typeArgs != null); if (typeArgs.Count != 0) { wr.Write("<" + Util.Comma(", ", typeArgs, tp => tp.Name + EqualitySupportSuffix(tp.EqualitySupport)) + ">"); } } private void PrintTypeInstantiation(List typeArgs) { Contract.Requires(typeArgs == null || typeArgs.Count != 0); if (typeArgs != null) { wr.Write("<{0}>", Util.Comma(",", typeArgs, ty => ty.ToString())); } } public void PrintDatatype(DatatypeDecl dt, int indent) { Contract.Requires(dt != null); Indent(indent); PrintClassMethodHelper(dt is IndDatatypeDecl ? "datatype" : "codatatype", dt.Attributes, dt.Name, dt.TypeArgs); wr.Write(" ="); string sep = ""; foreach (DatatypeCtor ctor in dt.Ctors) { wr.Write(sep); PrintClassMethodHelper("", ctor.Attributes, ctor.Name, new List()); if (ctor.Formals.Count != 0) { PrintFormals(ctor.Formals); } sep = " |"; } wr.WriteLine(); } /// /// Prints a space before each attribute. /// public void PrintAttributes(Attributes a) { if (a != null) { PrintAttributes(a.Prev); wr.Write(" {{:{0}", a.Name); if (a.Args != null) { PrintAttributeArgs(a.Args, false); } wr.Write("}"); } } public void PrintAttributeArgs(List args, bool isFollowedBySemicolon) { Contract.Requires(args != null); string prefix = " "; foreach (var arg in args) { Contract.Assert(arg != null); wr.Write(prefix); prefix = ", "; PrintExpression(arg, isFollowedBySemicolon); } } public void PrintField(Field field, int indent) { Contract.Requires(field != null); Indent(indent); if (field.IsGhost) { wr.Write("ghost "); } wr.Write("var"); PrintAttributes(field.Attributes); wr.Write(" {0}: ", field.Name); PrintType(field.Type); if (field.IsUserMutable) { // nothing more to say } else if (field.IsMutable) { wr.Write(" // non-assignable"); } else { wr.Write(" // immutable"); } wr.WriteLine(); } public void PrintFunction(Function f, int indent, bool printSignatureOnly) { Contract.Requires(f != null); if (PrintModeSkipFunctionOrMethod(f.IsGhost, f.Attributes, f.Name)) { return; } var isPredicate = f is Predicate || f is PrefixPredicate; Indent(indent); string k = isPredicate ? "predicate" : f is InductivePredicate ? "inductive predicate" : f is CoPredicate ? "copredicate" : "function"; if (f.IsProtected) { k = "protected " + k; } if (f.HasStaticKeyword) { k = "static " + k; } if (!f.IsGhost) { k += " method"; } PrintClassMethodHelper(k, f.Attributes, f.Name, f.TypeArgs); if (f.SignatureIsOmitted) { wr.WriteLine(" ..."); } else { PrintFormals(f.Formals, f.Name); if (!isPredicate) { wr.Write(": "); PrintType(f.ResultType); } wr.WriteLine(); } int ind = indent + IndentAmount; PrintSpec("requires", f.Req, ind); PrintFrameSpecLine("reads", f.Reads, ind, null); PrintSpec("ensures", f.Ens, ind); PrintDecreasesSpec(f.Decreases, ind); if (f.Body != null && !printSignatureOnly) { Indent(indent); wr.WriteLine("{"); PrintExtendedExpr(f.Body, ind, true, false); Indent(indent); wr.WriteLine("}"); } } // ----------------------------- PrintMethod ----------------------------- const int IndentAmount = 2; // The amount of indent for each new scope const string BunchaSpaces = " "; void Indent(int amount) { Contract.Requires(0 <= amount); while (0 < amount) { wr.Write(BunchaSpaces.Substring(0, amount)); amount -= BunchaSpaces.Length; } } private bool PrintModeSkipFunctionOrMethod(bool IsGhost, Attributes attributes, string name) { if (printMode == DafnyOptions.PrintModes.NoGhost && IsGhost) { return true; } if (printMode == DafnyOptions.PrintModes.NoIncludes || printMode == DafnyOptions.PrintModes.NoGhost) { bool verify = true; if (Attributes.ContainsBool(attributes, "verify", ref verify) && !verify) { return true; } if (name.Contains("INTERNAL") || name.StartsWith("reveal_")) { return true; } } return false; } private bool PrintModeSkipGeneral(Bpl.IToken tok, string fileBeingPrinted) { return (printMode == DafnyOptions.PrintModes.NoIncludes || printMode == DafnyOptions.PrintModes.NoGhost) && (tok.filename != null && fileBeingPrinted != null && Path.GetFullPath(tok.filename) != fileBeingPrinted); } public void PrintMethod(Method method, int indent, bool printSignatureOnly) { Contract.Requires(method != null); if (PrintModeSkipFunctionOrMethod(method.IsGhost, method.Attributes, method.Name)) { return; } Indent(indent); string k = method is Constructor ? "constructor" : method is InductiveLemma ? "inductive lemma" : method is CoLemma ? "colemma" : method is Lemma ? "lemma" : "method"; if (method.HasStaticKeyword) { k = "static " + k; } if (method.IsGhost && !(method is Lemma) && !(method is FixpointLemma)) { k = "ghost " + k; } string nm = method is Constructor && !((Constructor)method).HasName ? "" : method.Name; PrintClassMethodHelper(k, method.Attributes, nm, method.TypeArgs); if (method.SignatureIsOmitted) { wr.WriteLine(" ..."); } else { PrintFormals(method.Ins, method.Name); if (method.Outs.Count != 0) { if (method.Ins.Count + method.Outs.Count <= 3) { wr.Write(" returns "); } else { wr.WriteLine(); Indent(indent + 2 * IndentAmount); wr.Write("returns "); } PrintFormals(method.Outs); } wr.WriteLine(); } int ind = indent + IndentAmount; PrintSpec("requires", method.Req, ind); if (method.Mod.Expressions != null) { PrintFrameSpecLine("modifies", method.Mod.Expressions, ind, method.Mod.HasAttributes() ? method.Mod.Attributes : null); } PrintSpec("ensures", method.Ens, ind); PrintDecreasesSpec(method.Decreases, ind); if (method.Body != null && !printSignatureOnly) { Indent(indent); PrintStatement(method.Body, indent); wr.WriteLine(); } } internal void PrintFormals(List ff, string name = null) { Contract.Requires(ff != null); if (name != null && name.EndsWith("#")) { wr.Write("["); PrintFormal(ff[0]); wr.Write("]"); ff = new List(ff.Skip(1)); } wr.Write("("); string sep = ""; foreach (Formal f in ff) { Contract.Assert(f != null); wr.Write(sep); sep = ", "; PrintFormal(f); } wr.Write(")"); } void PrintFormal(Formal f) { Contract.Requires(f != null); if (f.IsGhost) { wr.Write("ghost "); } if (f.HasName) { wr.Write("{0}: ", f.DisplayName); } PrintType(f.Type); } internal void PrintSpec(string kind, List ee, int indent) { Contract.Requires(kind != null); Contract.Requires(ee != null); foreach (Expression e in ee) { Contract.Assert(e != null); Indent(indent); wr.Write("{0} ", kind); PrintExpression(e, true); wr.WriteLine(); } } internal void PrintDecreasesSpec(Specification decs, int indent, bool newLine = true) { Contract.Requires(decs != null); if (printMode == DafnyOptions.PrintModes.NoGhost) { return; } if (decs.Expressions != null && decs.Expressions.Count != 0) { Indent(indent); wr.Write("decreases"); if (decs.HasAttributes()) { PrintAttributes(decs.Attributes); } wr.Write(" "); PrintExpressionList(decs.Expressions, true); if (newLine) { wr.WriteLine(); } else { wr.Write(" "); } } } internal void PrintFrameSpecLine(string kind, List ee, int indent, Attributes attrs, bool newLine = true) { Contract.Requires(kind != null); Contract.Requires(cce.NonNullElements(ee)); if (ee != null && ee.Count != 0) { Indent(indent); wr.Write("{0}", kind); if (attrs != null) { PrintAttributes(attrs); } wr.Write(" "); PrintFrameExpressionList(ee); if (newLine) { wr.WriteLine(); } else { wr.Write(" "); } } } internal void PrintSpec(string kind, List ee, int indent, bool newLine = true) { Contract.Requires(kind != null); Contract.Requires(ee != null); if (printMode == DafnyOptions.PrintModes.NoGhost) { return; } foreach (MaybeFreeExpression e in ee) { Contract.Assert(e != null); Indent(indent); wr.Write("{0}{1}", e.IsFree ? "free " : "", kind); if (e.HasAttributes()) { PrintAttributes(e.Attributes); } wr.Write(" "); PrintExpression(e.E, true); if (newLine) { wr.WriteLine(); } else { wr.Write(" "); } } } // ----------------------------- PrintType ----------------------------- public void PrintType(Type ty) { Contract.Requires(ty != null); wr.Write(ty.ToString()); } public void PrintType(string prefix, Type ty) { Contract.Requires(prefix != null); Contract.Requires(ty != null); string s = ty.ToString(); if (s != "?") { wr.Write("{0}{1}", prefix, s); } } string EqualitySupportSuffix(TypeParameter.EqualitySupportValue es) { if (es == TypeParameter.EqualitySupportValue.Required || (es == TypeParameter.EqualitySupportValue.InferredRequired && DafnyOptions.O.DafnyPrintResolvedFile != null)) { return "(==)"; } else { return ""; } } // ----------------------------- PrintStatement ----------------------------- /// /// Prints from the current position of the current line. /// If the statement requires several lines, subsequent lines are indented at "indent". /// No newline is printed after the statement. /// public void PrintStatement(Statement stmt, int indent) { Contract.Requires(stmt != null); if (stmt.IsGhost && printMode == DafnyOptions.PrintModes.NoGhost) { return; } for (LList