Skip to content

Commit

Permalink
Merge remote-tracking branch 'origin/master' into pruneAssumptions
Browse files Browse the repository at this point in the history
  • Loading branch information
@keyboardDrummer
keyboardDrummer committed Jul 24, 2024
2 parents c00149d + f1b0c01 commit 6317327
Show file tree
Hide file tree
Showing 13 changed files with 202 additions and 65 deletions.
8 changes: 4 additions & 4 deletions Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ public partial class Printer {
public void PrintStatement(Statement stmt, int indent) {
Contract.Requires(stmt != null);

if (stmt.IsGhost && printMode == PrintModes.NoGhost) { return; }
if (stmt.IsGhost && printMode == PrintModes.NoGhostOrIncludes) { return; }
for (LList<Label> label = stmt.Labels; label != null; label = label.Next) {
if (label.Data.Name != null) {
wr.WriteLine("label {0}:", label.Data.Name);
Expand All @@ -38,7 +38,7 @@ public void PrintStatement(Statement stmt, int indent) {
}

if (stmt is PredicateStmt) {
if (printMode == PrintModes.NoGhost) { return; }
if (printMode == PrintModes.NoGhostOrIncludes) { return; }
Expression expr = ((PredicateStmt)stmt).Expr;
var assertStmt = stmt as AssertStmt;
var expectStmt = stmt as ExpectStmt;
Expand Down Expand Up @@ -220,7 +220,7 @@ public void PrintStatement(Statement stmt, int indent) {

} else if (stmt is CalcStmt) {
CalcStmt s = (CalcStmt)stmt;
if (printMode == PrintModes.NoGhost) { return; } // Calcs don't get a "ghost" attribute, but they are.
if (printMode == PrintModes.NoGhostOrIncludes) { return; } // Calcs don't get a "ghost" attribute, but they are.
wr.Write("calc");
PrintAttributes(stmt.Attributes);
wr.Write(" ");
Expand Down Expand Up @@ -374,7 +374,7 @@ public void PrintStatement(Statement stmt, int indent) {

} else if (stmt is VarDeclStmt) {
var s = (VarDeclStmt)stmt;
if (s.Locals.Exists(v => v.IsGhost) && printMode == PrintModes.NoGhost) { return; }
if (s.Locals.Exists(v => v.IsGhost) && printMode == PrintModes.NoGhostOrIncludes) { return; }
if (s.Locals.TrueForAll((v => v.IsGhost))) {
// Emit the "ghost" modifier if all of the variables are ghost. If some are ghost, but not others,
// then some of these ghosts are auto-converted to ghost, so we should not emit the "ghost" keyword.
Expand Down
81 changes: 41 additions & 40 deletions Source/DafnyCore/AST/Grammar/Printer/Printer.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,10 +23,9 @@ public enum PrintModes {
Everything,
Serialization, // Serializing the program to a file for lossless loading later
NoIncludes,
NoGhost
NoGhostOrIncludes
}


public record PrintFlags(bool UseOriginalDafnyNames = false);

public partial class Printer {
Expand Down Expand Up @@ -207,7 +206,7 @@ public void PrintProgram(Program prog, bool afterResolver) {
if (options.DafnyPrintResolvedFile != null && options.PrintMode == PrintModes.Everything) {
wr.WriteLine();
wr.WriteLine("/*");
PrintModuleDefinition(prog.Compilation, prog.SystemModuleManager.SystemModule, null, 0, null, Path.GetFullPath(options.DafnyPrintResolvedFile));
PrintModuleDefinition(prog.Compilation, prog.SystemModuleManager.SystemModule, null, 0, null);
wr.Write("// bitvector types in use:");
foreach (var w in prog.SystemModuleManager.Bitwidths) {
wr.Write(" bv{0}", w);
Expand All @@ -217,10 +216,10 @@ public void PrintProgram(Program prog, bool afterResolver) {
}
wr.WriteLine();
PrintCallGraph(prog.DefaultModuleDef, 0);
PrintTopLevelDecls(prog.Compilation, prog.DefaultModuleDef.TopLevelDecls, 0, null, Path.GetFullPath(prog.FullName));
PrintTopLevelDecls(prog.Compilation, prog.DefaultModuleDef.TopLevelDecls, 0, null);
foreach (var tup in prog.DefaultModuleDef.PrefixNamedModules) {
var decls = new List<TopLevelDecl>() { tup.Module };
PrintTopLevelDecls(prog.Compilation, decls, 0, tup.Parts, Path.GetFullPath(prog.FullName));
PrintTopLevelDecls(prog.Compilation, decls, 0, tup.Parts);
}
wr.Flush();
}
Expand Down Expand Up @@ -266,12 +265,14 @@ public void PrintCallGraph(ModuleDefinition module, int indent) {
}
}

public void PrintTopLevelDecls(CompilationData compilation, IEnumerable<TopLevelDecl> decls, int indent, IEnumerable<IToken>/*?*/ prefixIds, string fileBeingPrinted) {
public void PrintTopLevelDecls(CompilationData compilation, IEnumerable<TopLevelDecl> decls, int indent,
IEnumerable<IToken>/*?*/ prefixIds) {
Contract.Requires(decls != null);
int i = 0;
foreach (TopLevelDecl d in decls) {
Contract.Assert(d != null);
if (PrintModeSkipGeneral(d.tok, fileBeingPrinted)) { continue; }
var project = compilation.Options.DafnyProject;
if (PrintModeSkipGeneral(project, d.tok)) { continue; }
if (d is AbstractTypeDecl) {
var at = (AbstractTypeDecl)d;
if (i++ != 0) { wr.WriteLine(); }
Expand All @@ -282,7 +283,7 @@ public void PrintTopLevelDecls(CompilationData compilation, IEnumerable<TopLevel
wr.WriteLine();
} else {
wr.WriteLine(" {");
PrintMembers(at.Members, indent + IndentAmount, fileBeingPrinted);
PrintMembers(at.Members, indent + IndentAmount, project);
Indent(indent);
wr.WriteLine("}");
}
Expand Down Expand Up @@ -316,7 +317,7 @@ public void PrintTopLevelDecls(CompilationData compilation, IEnumerable<TopLevel
if (dd.Members.Count != 0) {
Indent(indent);
wr.WriteLine("{");
PrintMembers(dd.Members, indent + IndentAmount, fileBeingPrinted);
PrintMembers(dd.Members, indent + IndentAmount, project);
Indent(indent);
wr.WriteLine("}");
}
Expand All @@ -335,7 +336,7 @@ public void PrintTopLevelDecls(CompilationData compilation, IEnumerable<TopLevel
} else if (d is DatatypeDecl) {
var dd = (DatatypeDecl)d;
if (i++ != 0) { wr.WriteLine(); }
PrintDatatype(dd, indent, fileBeingPrinted);
PrintDatatype(dd, indent, project);
} else if (d is IteratorDecl) {
var iter = (IteratorDecl)d;
if (i++ != 0) { wr.WriteLine(); }
Expand All @@ -351,7 +352,7 @@ public void PrintTopLevelDecls(CompilationData compilation, IEnumerable<TopLevel
// 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
Indent(indent); wr.WriteLine("/*---------- iterator members ----------");
Indent(indent); PrintIteratorClass(iter, indent, fileBeingPrinted);
Indent(indent); PrintIteratorClass(iter, indent, project);
Indent(indent); wr.WriteLine("---------- iterator members ----------*/");
}

Expand All @@ -360,17 +361,17 @@ public void PrintTopLevelDecls(CompilationData compilation, IEnumerable<TopLevel
// print nothing
} else {
if (i++ != 0) { wr.WriteLine(); }
PrintMembers(defaultClassDecl.Members, indent, fileBeingPrinted);
PrintMembers(defaultClassDecl.Members, indent, project);
}
} else if (d is ClassLikeDecl) {
var cl = (ClassLikeDecl)d;
if (i++ != 0) { wr.WriteLine(); }
PrintClass(cl, indent, fileBeingPrinted);
PrintClass(cl, indent, project);

} else if (d is ClassLikeDecl) {
var cl = (ClassLikeDecl)d;
if (i++ != 0) { wr.WriteLine(); }
PrintClass(cl, indent, fileBeingPrinted);
PrintClass(cl, indent, project);

} else if (d is ValuetypeDecl) {
var vtd = (ValuetypeDecl)d;
Expand All @@ -381,7 +382,7 @@ public void PrintTopLevelDecls(CompilationData compilation, IEnumerable<TopLevel
wr.WriteLine(" { }");
} else {
wr.WriteLine(" {");
PrintMembers(vtd.Members, indent + IndentAmount, fileBeingPrinted);
PrintMembers(vtd.Members, indent + IndentAmount, project);
Indent(indent);
wr.WriteLine("}");
}
Expand All @@ -401,7 +402,7 @@ public void PrintTopLevelDecls(CompilationData compilation, IEnumerable<TopLevel
if (modDecl.Signature != null) {
scope = modDecl.Signature.VisibilityScope;
}
PrintModuleDefinition(compilation, modDecl.ModuleDef, scope, indent, prefixIds, fileBeingPrinted);
PrintModuleDefinition(compilation, modDecl.ModuleDef, scope, indent, prefixIds);
} else if (d is AliasModuleDecl) {
var dd = (AliasModuleDecl)d;

Expand Down Expand Up @@ -450,7 +451,7 @@ public void PrintTopLevelDecls(CompilationData compilation, IEnumerable<TopLevel
}

wr.WriteLine();
PrintModuleExportDecl(compilation, e, indent + IndentAmount, fileBeingPrinted);
PrintModuleExportDecl(compilation, e, indent + IndentAmount, project);
wr.WriteLine();
} else {
Contract.Assert(false); // unexpected ModuleDecl
Expand Down Expand Up @@ -519,7 +520,7 @@ private void PrintWitnessClause(RedirectingTypeDecl dd) {
}
}

void PrintModuleExportDecl(CompilationData compilation, ModuleExportDecl m, int indent, string fileBeingPrinted) {
void PrintModuleExportDecl(CompilationData compilation, ModuleExportDecl m, int indent, DafnyProject project) {
Contract.Requires(m != null);

if (m.RevealAll) {
Expand Down Expand Up @@ -550,9 +551,9 @@ void PrintModuleExportDecl(CompilationData compilation, ModuleExportDecl m, int
for (int j = start; j < i; j++) {
var id = m.Exports[j];
if (id.Decl is TopLevelDecl) {
PrintTopLevelDecls(compilation, new List<TopLevelDecl> { (TopLevelDecl)id.Decl }, indent + IndentAmount, null, fileBeingPrinted);
PrintTopLevelDecls(compilation, new List<TopLevelDecl> { (TopLevelDecl)id.Decl }, indent + IndentAmount, null);
} else if (id.Decl is MemberDecl) {
PrintMembers(new List<MemberDecl> { (MemberDecl)id.Decl }, indent + IndentAmount, fileBeingPrinted);
PrintMembers(new List<MemberDecl> { (MemberDecl)id.Decl }, indent + IndentAmount, project);
}
}
Indent(indent);
Expand All @@ -563,7 +564,7 @@ void PrintModuleExportDecl(CompilationData compilation, ModuleExportDecl m, int
}
}

public void PrintModuleDefinition(CompilationData compilation, ModuleDefinition module, VisibilityScope scope, int indent, IEnumerable<IToken>/*?*/ prefixIds, string fileBeingPrinted) {
public void PrintModuleDefinition(CompilationData compilation, ModuleDefinition module, VisibilityScope scope, int indent, IEnumerable<IToken>/*?*/ prefixIds) {
Contract.Requires(module != null);
Contract.Requires(0 <= indent);
Type.PushScope(scope);
Expand Down Expand Up @@ -595,23 +596,23 @@ public void PrintModuleDefinition(CompilationData compilation, ModuleDefinition
} else {
wr.WriteLine("{");
PrintCallGraph(module, indent + IndentAmount);
PrintTopLevelDeclsOrExportedView(compilation, module, indent, fileBeingPrinted);
PrintTopLevelDeclsOrExportedView(compilation, module, indent);
Indent(indent);
wr.WriteLine("}");
}
Type.PopScope(scope);
}

void PrintTopLevelDeclsOrExportedView(CompilationData compilation, ModuleDefinition module, int indent, string fileBeingPrinted) {
void PrintTopLevelDeclsOrExportedView(CompilationData compilation, ModuleDefinition module, int indent) {
var decls = module.TopLevelDecls;
// only filter based on view name after resolver.
if (afterResolver && options.DafnyPrintExportedViews.Count != 0) {
var views = options.DafnyPrintExportedViews.ToHashSet();
decls = decls.Where(d => views.Contains(d.FullName));
}
PrintTopLevelDecls(compilation, decls, indent + IndentAmount, null, fileBeingPrinted);
PrintTopLevelDecls(compilation, decls, indent + IndentAmount, null);
foreach (var tup in module.PrefixNamedModules) {
PrintTopLevelDecls(compilation, new TopLevelDecl[] { tup.Module }, indent + IndentAmount, tup.Parts, fileBeingPrinted);
PrintTopLevelDecls(compilation, new TopLevelDecl[] { tup.Module }, indent + IndentAmount, tup.Parts);
}
}

Expand Down Expand Up @@ -649,17 +650,17 @@ void PrintIteratorSignature(IteratorDecl iter, int indent) {
wr.WriteLine();
}

private void PrintIteratorClass(IteratorDecl iter, int indent, string fileBeingPrinted) {
private void PrintIteratorClass(IteratorDecl iter, int indent, DafnyProject project) {
PrintClassMethodHelper("class", null, iter.Name, iter.TypeArgs);
wr.WriteLine(" {");
PrintMembers(iter.Members, indent + IndentAmount, fileBeingPrinted);
PrintMembers(iter.Members, indent + IndentAmount, project);
Indent(indent); wr.WriteLine("}");

Contract.Assert(iter.NonNullTypeDecl != null);
PrintSubsetTypeDecl(iter.NonNullTypeDecl, indent);
}

public void PrintClass(ClassLikeDecl c, int indent, string fileBeingPrinted) {
public void PrintClass(ClassLikeDecl c, int indent, DafnyProject project) {
Contract.Requires(c != null);

Indent(indent);
Expand All @@ -674,7 +675,7 @@ public void PrintClass(ClassLikeDecl c, int indent, string fileBeingPrinted) {
wr.WriteLine(" { }");
} else {
wr.WriteLine(" {");
PrintMembers(c.Members, indent + IndentAmount, fileBeingPrinted);
PrintMembers(c.Members, indent + IndentAmount, project);
Indent(indent);
wr.WriteLine("}");
}
Expand All @@ -699,12 +700,12 @@ private void PrintExtendsClause(TopLevelDeclWithMembers c) {
}
}

public void PrintMembers(List<MemberDecl> members, int indent, string fileBeingPrinted) {
public void PrintMembers(List<MemberDecl> members, int indent, DafnyProject project) {
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 (PrintModeSkipGeneral(project, m.tok)) { continue; }
if (printMode == PrintModes.Serialization && Attributes.Contains(m.Attributes, "auto_generated")) {
// omit this declaration
} else if (m is Method) {
Expand Down Expand Up @@ -824,7 +825,7 @@ private void PrintTypeInstantiation(List<Type> typeArgs) {
wr.Write(Type.TypeArgsToString(options, typeArgs));
}

public void PrintDatatype(DatatypeDecl dt, int indent, string fileBeingPrinted) {
public void PrintDatatype(DatatypeDecl dt, int indent, DafnyProject dafnyProject) {
Contract.Requires(dt != null);
Indent(indent);
PrintClassMethodHelper(dt is IndDatatypeDecl ? "datatype" : "codatatype", dt.Attributes, dt.Name, dt.TypeArgs);
Expand All @@ -843,7 +844,7 @@ public void PrintDatatype(DatatypeDecl dt, int indent, string fileBeingPrinted)
wr.WriteLine();
} else {
wr.WriteLine(" {");
PrintMembers(dt.Members, indent + IndentAmount, fileBeingPrinted);
PrintMembers(dt.Members, indent + IndentAmount, dafnyProject);
Indent(indent);
wr.WriteLine("}");
}
Expand Down Expand Up @@ -974,18 +975,18 @@ void Indent(int amount) {
}

private bool PrintModeSkipFunctionOrMethod(bool IsGhost, Attributes attributes, string name) {
if (printMode == PrintModes.NoGhost && IsGhost) { return true; }
if (printMode == PrintModes.NoIncludes || printMode == PrintModes.NoGhost) {
if (printMode == PrintModes.NoGhostOrIncludes && IsGhost) { return true; }
if (printMode == PrintModes.NoIncludes || printMode == PrintModes.NoGhostOrIncludes) {
bool verify = true;
if (Attributes.ContainsBool(attributes, "verify", ref verify) && !verify) { return true; }
if (name.Contains("INTERNAL") || name.StartsWith(RevealStmt.RevealLemmaPrefix)) { return true; }
}
return false;
}

private bool PrintModeSkipGeneral(IToken tok, string fileBeingPrinted) {
return (printMode == PrintModes.NoIncludes || printMode == PrintModes.NoGhost)
&& tok.Uri != null && fileBeingPrinted != null && tok.Uri.LocalPath != fileBeingPrinted;
private bool PrintModeSkipGeneral(DafnyProject project, IToken tok) {
return (printMode == PrintModes.NoIncludes || printMode == PrintModes.NoGhostOrIncludes)
&& tok.Uri != null && !project.ContainsSourceFile(tok.Uri);
}

public void PrintMethod(Method method, int indent, bool printSignatureOnly) {
Expand Down Expand Up @@ -1110,7 +1111,7 @@ void PrintFormal(Formal f, bool showNewKeyword) {

internal void PrintDecreasesSpec(Specification<Expression> decs, int indent) {
Contract.Requires(decs != null);
if (printMode == PrintModes.NoGhost) { return; }
if (printMode == PrintModes.NoGhostOrIncludes) { return; }
if (decs.Expressions != null && decs.Expressions.Count != 0) {
wr.WriteLine();
Indent(indent);
Expand Down Expand Up @@ -1139,7 +1140,7 @@ internal void PrintFrameSpecLine(string kind, Specification<FrameExpression> ee,
internal void PrintSpec(string kind, List<AttributedExpression> ee, int indent) {
Contract.Requires(kind != null);
Contract.Requires(ee != null);
if (printMode == PrintModes.NoGhost) { return; }
if (printMode == PrintModes.NoGhostOrIncludes) { return; }
foreach (AttributedExpression e in ee) {
Contract.Assert(e != null);
wr.WriteLine();
Expand Down
2 changes: 1 addition & 1 deletion Source/DafnyCore/Options/CommonOptionBag.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -461,7 +461,7 @@ void ParsePrintMode(Option<PrintModes> option, Boogie.CommandLineParseState ps,
} else if (ps.args[ps.i].Equals("NoIncludes")) {
options.Set(option, PrintModes.NoIncludes);
} else if (ps.args[ps.i].Equals("NoGhost")) {
options.Set(option, PrintModes.NoGhost);
options.Set(option, PrintModes.NoGhostOrIncludes);
} else if (ps.args[ps.i].Equals("DllEmbed")) {
// This is called DllEmbed because it was previously only used inside Dafny-compiled .dll files for C#,
// but it is now used by the LibraryBackend when building .doo files as well.
Expand Down
25 changes: 17 additions & 8 deletions Source/DafnyCore/Pipeline/Compilation.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -140,23 +140,32 @@ private async Task<IReadOnlyList<DafnyFile>> DetermineRootFiles() {
await started.Task;

var result = new List<DafnyFile>();
var includedFiles = new List<DafnyFile>();
foreach (var uri in Input.Project.GetRootSourceUris(fileSystem)) {
await foreach (var file in DafnyFile.CreateAndValidate(fileSystem, errorReporter, Options, uri,
Project.StartingToken)) {
result.Add(file);
includedFiles.Add(file);
}
}

var handledInput = new HashSet<Uri>();
foreach (var uri in Options.CliRootSourceUris) {
if (!handledInput.Add(uri)) {
continue;
}
var shortPath = Path.GetRelativePath(Directory.GetCurrentDirectory(), uri.LocalPath);
await foreach (var file in DafnyFile.CreateAndValidate(fileSystem, errorReporter, Options, uri, Token.Cli,
false,
$"command-line argument '{shortPath}' is neither a recognized option nor a Dafny input file (.dfy, .doo, or .toml).")) {
result.Add(file);
}
}

var includedFiles = new List<DafnyFile>();
foreach (var uri in Input.Project.GetRootSourceUris(fileSystem)) {
if (!handledInput.Add(uri)) {
continue;
}
await foreach (var file in DafnyFile.CreateAndValidate(fileSystem, errorReporter, Options, uri,
Project.StartingToken)) {
result.Add(file);
includedFiles.Add(file);
}
}

if (Options.UseStdin) {
result.Add(DafnyFile.HandleStandardInput(Options, Token.Cli));
}
Expand Down
2 changes: 1 addition & 1 deletion Source/DafnyCore/Resolver/ModuleResolver.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -548,7 +548,7 @@ public void CheckModuleExportConsistency(CompilationData compilation, ModuleDefi
var wr = Options.OutputWriter;
wr.WriteLine("/* ===== export set {0}", exportDecl.FullName);
var pr = new Printer(wr, Options);
pr.PrintTopLevelDecls(compilation, exportView.TopLevelDecls, 0, null, null);
pr.PrintTopLevelDecls(compilation, exportView.TopLevelDecls, 0, null);
wr.WriteLine("*/");
}

Expand Down
Loading

0 comments on commit 6317327

Please sign in to comment.