Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Warn when using non doo file as a library #5313

Merged
merged 26 commits into from
Apr 11, 2024
Merged

Warn when using non doo file as a library #5313

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
26 commits
Select commit Hold shift + click to select a range
27948b8
Include libraries of projects referenced through source or libraries
keyboardDrummer Apr 4, 2024
942394e
Add warning when using non-doo files with --library
keyboardDrummer Apr 4, 2024
e4f9a0d
Update tests
keyboardDrummer Apr 4, 2024
d827340
Add release note
keyboardDrummer Apr 4, 2024
6919db7
Update warning
keyboardDrummer Apr 4, 2024
5f1d9fb
Couple of fixes
keyboardDrummer Apr 5, 2024
3b06f43
Async fixes
keyboardDrummer Apr 5, 2024
3bdbe2a
Resolve warnings
keyboardDrummer Apr 5, 2024
f2c0cec
Tiny refactor
keyboardDrummer Apr 5, 2024
379700f
One fix to Server.Main
keyboardDrummer Apr 5, 2024
cf8e18b
Fix tests
keyboardDrummer Apr 5, 2024
13eaf8e
Fix ProducerLibrary test
keyboardDrummer Apr 5, 2024
c08ac17
Merge branch 'master' into projectAsLibrary
robin-aws Apr 8, 2024
d3da45f
Merge remote-tracking branch 'origin/master' into projectAsLibrary
keyboardDrummer Apr 9, 2024
17fa4c9
Fix warning
keyboardDrummer Apr 9, 2024
f804f17
Merge branch 'master' into projectAsLibrary
keyboardDrummer Apr 9, 2024
3f49b9c
Stop accepting project files as source files
keyboardDrummer Apr 10, 2024
946ccfa
Slightly more refactoring
keyboardDrummer Apr 10, 2024
b6078e4
Merge branch 'master' into warnNonDooLibrary
keyboardDrummer Apr 10, 2024
48e7d10
Merge remote-tracking branch 'origin/master' into warnNonDooLibrary
keyboardDrummer Apr 10, 2024
969b504
Code review
keyboardDrummer Apr 10, 2024
74e3329
Rename .feat file
keyboardDrummer Apr 10, 2024
ea414fa
Bring back null checks
keyboardDrummer Apr 10, 2024
db82322
Update message
keyboardDrummer Apr 11, 2024
51d1f1c
Merge remote-tracking branch 'origin/master' into warnNonDooLibrary
keyboardDrummer Apr 11, 2024
493c8b1
Merge branch 'master' into warnNonDooLibrary
keyboardDrummer Apr 11, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 5 additions & 5 deletions Source/DafnyCore.Test/DooFileTest.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,16 +7,16 @@ namespace DafnyCore.Test;

public class DooFileTest {
[Fact]
public void RoundTripCurrentVersion() {
public async Task RoundTripCurrentVersion() {
var options = DafnyOptions.Default;
options.ApplyDefaultOptionsWithoutSettingsDefault();
var program = ParseProgram("module MyModule { function TheAnswer(): int { 42 } }", options);
var program = await ParseProgram("module MyModule { function TheAnswer(): int { 42 } }", options);
options.ProcessSolverOptions(program.Reporter, Token.Cli);
var dooFile = new DooFile(program);

var path = Path.GetTempFileName();
dooFile.Write(path);
var loadedDooFile = DooFile.Read(path);
var loadedDooFile = await DooFile.Read(path);

Assert.Equal(loadedDooFile.Manifest.DooFileVersion, DooFile.ManifestData.CurrentDooFileVersion);
Assert.Equal(loadedDooFile.Manifest.DafnyVersion, options.VersionNumber);
Expand All @@ -31,12 +31,12 @@ public void UnknownManifestEntries() {
Assert.Throws<TomlException>(() => DooFile.ManifestData.Read(new StringReader(source)));
}

private static Program ParseProgram(string dafnyProgramText, DafnyOptions options) {
private static async Task<Program> ParseProgram(string dafnyProgramText, DafnyOptions options) {
const string fullFilePath = "untitled:foo";
var rootUri = new Uri(fullFilePath);
Microsoft.Dafny.Type.ResetScopes();
var errorReporter = new ConsoleErrorReporter(options);
var program = new ProgramParser().Parse(dafnyProgramText, rootUri, errorReporter);
var program = await new ProgramParser().Parse(dafnyProgramText, rootUri, errorReporter);
Assert.Equal(0, errorReporter.ErrorCount);
return program;
}
Expand Down
22 changes: 11 additions & 11 deletions Source/DafnyCore/AST/Grammar/ProgramParser.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@
using System.Linq;
using System.Text;
using System.Threading;
using DafnyCore;
using System.Threading.Tasks;
using Microsoft.Dafny.Compilers;
using Microsoft.Extensions.Logging;
using Microsoft.Extensions.Logging.Abstractions;
Expand All @@ -32,7 +32,7 @@ public ProgramParser(ILogger<ProgramParser> logger, IFileSystem fileSystem) {
this.fileSystem = fileSystem;
}

public virtual Program ParseFiles(string programName, IReadOnlyList<DafnyFile> files,
public virtual async Task<Program> ParseFiles(string programName, IReadOnlyList<DafnyFile> files,
ErrorReporter errorReporter,
CancellationToken cancellationToken) {
var options = errorReporter.Options;
Expand All @@ -54,7 +54,7 @@ public virtual Program ParseFiles(string programName, IReadOnlyList<DafnyFile> f
foreach (var dafnyFile in files) {
cancellationToken.ThrowIfCancellationRequested();
if (options.Trace) {
options.OutputWriter.WriteLine("Parsing " + dafnyFile.FilePath);
await options.OutputWriter.WriteLineAsync("Parsing " + dafnyFile.FilePath);
}

if (options.XmlSink is { IsOpen: true } && dafnyFile.Uri.IsFile) {
Expand All @@ -75,7 +75,7 @@ public virtual Program ParseFiles(string programName, IReadOnlyList<DafnyFile> f
}

if (!(options.DisallowIncludes || options.PrintIncludesMode == DafnyOptions.IncludesModes.Immediate)) {
var includedModules = TryParseIncludes(files, defaultModule.Includes.ToList(),
var includedModules = await TryParseIncludes(files, defaultModule.Includes.ToList(),
builtIns, errorReporter, cancellationToken);

foreach (var module in includedModules) {
Expand Down Expand Up @@ -205,7 +205,7 @@ public static void MoveModuleContents(ModuleDefinition sourceModule, ModuleDefin
}
}

public IList<DfyParseResult> TryParseIncludes(
public async Task<IList<DfyParseResult>> TryParseIncludes(
IReadOnlyList<DafnyFile> files,
IEnumerable<Include> roots,
SystemModuleManager systemModuleManager,
Expand All @@ -220,7 +220,7 @@ CancellationToken cancellationToken
}

foreach (var root in roots) {
var dafnyFile = IncludeToDafnyFile(systemModuleManager, errorReporter, root);
var dafnyFile = await IncludeToDafnyFile(systemModuleManager, errorReporter, root);
if (dafnyFile != null) {
stack.Push(dafnyFile);
}
Expand All @@ -242,7 +242,7 @@ CancellationToken cancellationToken
result.Add(parseIncludeResult);

foreach (var include in parseIncludeResult.Module.Includes) {
var dafnyFile = IncludeToDafnyFile(systemModuleManager, errorReporter, include);
var dafnyFile = await IncludeToDafnyFile(systemModuleManager, errorReporter, include);
if (dafnyFile != null) {
stack.Push(dafnyFile);
}
Expand All @@ -252,7 +252,7 @@ CancellationToken cancellationToken
return result;
}

private DafnyFile IncludeToDafnyFile(SystemModuleManager systemModuleManager, ErrorReporter errorReporter, Include include) {
private Task<DafnyFile> IncludeToDafnyFile(SystemModuleManager systemModuleManager, ErrorReporter errorReporter, Include include) {
return DafnyFile.CreateAndValidate(errorReporter, fileSystem, systemModuleManager.Options, include.IncludedFilename, include.tok);
}

Expand Down Expand Up @@ -307,10 +307,10 @@ private static Parser SetupParser(string s /*!*/, Uri uri /*!*/,
return new Parser(errorReporter.Options, scanner, errors, cancellationToken);
}

public Program Parse(string source, Uri uri, ErrorReporter reporter) {
public async Task<Program> Parse(string source, Uri uri, ErrorReporter reporter) {
var fs = new InMemoryFileSystem(ImmutableDictionary<Uri, string>.Empty.Add(uri, source));
var file = DafnyFile.CreateAndValidate(reporter, fs, reporter.Options, uri, Token.NoToken);
var file = await DafnyFile.CreateAndValidate(reporter, fs, reporter.Options, uri, Token.NoToken);
var files = file == null ? Array.Empty<DafnyFile>() : new[] { file };
return ParseFiles(uri.ToString(), files, reporter, CancellationToken.None);
return await ParseFiles(uri.ToString(), files, reporter, CancellationToken.None);
}
}
10 changes: 6 additions & 4 deletions Source/DafnyCore/DafnyFile.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,11 @@
using System;
using System.Collections.Generic;
using System.IO;
using System.Linq;
using System.Reflection;
using System.Reflection.Metadata;
using System.Reflection.PortableExecutable;
using System.Threading.Tasks;
using DafnyCore;
using JetBrains.Annotations;

Expand All @@ -29,12 +31,12 @@ public static Uri ExposeInternalUri(string externalName, Uri internalUri) {
return externalUri;
}

public static DafnyFile CreateAndValidate(ErrorReporter reporter, IFileSystem fileSystem,
public static async Task<DafnyFile> CreateAndValidate(ErrorReporter reporter, IFileSystem fileSystem,
DafnyOptions options, Uri uri, IToken origin, string errorOnNotRecognized = null) {

var embeddedFile = ExternallyVisibleEmbeddedFiles.GetValueOrDefault(uri);
if (embeddedFile != null) {
var result = CreateAndValidate(reporter, fileSystem, options, embeddedFile, origin, errorOnNotRecognized);
var result = await CreateAndValidate(reporter, fileSystem, options, embeddedFile, origin, errorOnNotRecognized);
if (result != null) {
result.Uri = uri;
}
Expand Down Expand Up @@ -106,15 +108,15 @@ public static DafnyFile CreateAndValidate(ErrorReporter reporter, IFileSystem fi
throw new Exception($"Cannot find embedded resource: {resourceName}");
}

dooFile = DooFile.Read(stream);
dooFile = await DooFile.Read(stream);
} else {
if (!fileSystem.Exists(uri)) {
reporter.Error(MessageSource.Project, origin, $"file {filePathForErrors} not found");
return null;
}

try {
dooFile = DooFile.Read(filePath);
dooFile = await DooFile.Read(filePath);
} catch (InvalidDataException) {
reporter.Error(MessageSource.Project, origin, $"malformed doo file {options.GetPrintPath(filePath)}");
return null;
Expand Down
22 changes: 11 additions & 11 deletions Source/DafnyCore/DafnyMain.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,36 +40,36 @@ public static void MaybePrintProgram(Program program, string filename, bool afte
/// <summary>
/// Returns null on success, or an error string otherwise.
/// </summary>
public static string ParseCheck(TextReader stdIn, IReadOnlyList<DafnyFile /*!*/> /*!*/ files, string /*!*/ programName,
DafnyOptions options, out Program program)
public static async Task<(Program Program, string Error)> ParseCheck(TextReader stdIn,
IReadOnlyList<DafnyFile /*!*/> /*!*/ files, string /*!*/ programName,
DafnyOptions options)
//modifies Bpl.options.XmlSink.*;
{
string err = Parse(files, programName, options, out program);
var (program, err) = await Parse(files, programName, options);
if (err != null) {
return err;
return (program, err);
}

return Resolve(program);
return (program, Resolve(program));
}

public static string Parse(IReadOnlyList<DafnyFile> files, string programName, DafnyOptions options,
out Program program) {
public static async Task<(Program Program, string Error)> Parse(IReadOnlyList<DafnyFile> files,
string programName, DafnyOptions options) {
Contract.Requires(programName != null);
Contract.Requires(files != null);
program = null;

ErrorReporter reporter = options.DiagnosticsFormat switch {
DafnyOptions.DiagnosticsFormats.PlainText => new ConsoleErrorReporter(options),
DafnyOptions.DiagnosticsFormats.JSON => new JsonConsoleErrorReporter(options),
_ => throw new ArgumentOutOfRangeException()
};

program = new ProgramParser().ParseFiles(programName, files, reporter, CancellationToken.None);
var program = await new ProgramParser().ParseFiles(programName, files, reporter, CancellationToken.None);
var errorCount = program.Reporter.ErrorCount;
if (errorCount != 0) {
return $"{errorCount} parse errors detected in {program.Name}";
return (program, $"{errorCount} parse errors detected in {program.Name}");
}
return null;
return (program, null);
}

public static readonly CustomStackSizePoolTaskScheduler LargeThreadScheduler =
Expand Down
15 changes: 9 additions & 6 deletions Source/DafnyCore/DooFile.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@
using System.IO.Compression;
using System.Linq;
using System.Text;
using System.Threading.Tasks;
using DafnyCore.Generic;
using Microsoft.Dafny;
using Tomlyn;
Expand Down Expand Up @@ -69,34 +70,36 @@ public void Write(TextWriter writer) {
// this must be configured to stay the same.
private static DafnyOptions ProgramSerializationOptions => DafnyOptions.Default;

public static DooFile Read(string path) {
public static Task<DooFile> Read(string path) {
using var archive = ZipFile.Open(path, ZipArchiveMode.Read);
return Read(archive);
}

public static DooFile Read(Stream stream) {
public static Task<DooFile> Read(Stream stream) {
using var archive = new ZipArchive(stream);
return Read(archive);
}

private static DooFile Read(ZipArchive archive) {
private static async Task<DooFile> Read(ZipArchive archive) {
var result = new DooFile();

var manifestEntry = archive.GetEntry(ManifestFileEntry);
if (manifestEntry == null) {
throw new ArgumentException(".doo file missing manifest entry");
}
using (var manifestStream = manifestEntry.Open()) {

await using (var manifestStream = manifestEntry.Open()) {
result.Manifest = ManifestData.Read(new StreamReader(manifestStream, Encoding.UTF8));
}

var programTextEntry = archive.GetEntry(ProgramFileEntry);
if (programTextEntry == null) {
throw new ArgumentException(".doo file missing program text entry");
}
using (var programTextStream = programTextEntry.Open()) {

await using (var programTextStream = programTextEntry.Open()) {
var reader = new StreamReader(programTextStream, Encoding.UTF8);
result.ProgramText = reader.ReadToEnd();
result.ProgramText = await reader.ReadToEndAsync();
}

return result;
Expand Down
47 changes: 35 additions & 12 deletions Source/DafnyCore/Pipeline/Compilation.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,7 @@ public class Compilation : IDisposable {

public ErrorReporter Reporter => errorReporter;

public IReadOnlyList<DafnyFile>? RootFiles { get; set; }
public Task<IReadOnlyList<DafnyFile>> RootFiles { get; set; }
public bool HasErrors { get; private set; }

public Compilation(
Expand Down Expand Up @@ -105,6 +105,7 @@ CompilationInput input

verificationTickets.Enqueue(Unit.Default);

RootFiles = DetermineRootFiles();
ParsedProgram = ParseAsync();
Resolution = ResolveAsync();
}
Expand All @@ -115,9 +116,7 @@ public void Start() {
}

Project.Errors.CopyDiagnostics(errorReporter);
RootFiles = DetermineRootFiles();

updates.OnNext(new DeterminedRootFiles(Project, RootFiles!, GetDiagnosticsCopyAndClear()));
started.TrySetResult();
}

Expand All @@ -128,19 +127,23 @@ private ImmutableList<FileDiagnostic> GetDiagnosticsCopyAndClear() {
return result;
}

private IReadOnlyList<DafnyFile> DetermineRootFiles() {


private async Task<IReadOnlyList<DafnyFile>> DetermineRootFiles() {
await started.Task;

var result = new List<DafnyFile>();

foreach (var uri in Input.Project.GetRootSourceUris(fileSystem)) {
var file = DafnyFile.CreateAndValidate(errorReporter, fileSystem, Options, uri, Project.StartingToken);
var file = await DafnyFile.CreateAndValidate(errorReporter, fileSystem, Options, uri, Project.StartingToken);
if (file != null) {
result.Add(file);
}
}

foreach (var uri in Options.CliRootSourceUris) {
var shortPath = Path.GetRelativePath(Directory.GetCurrentDirectory(), uri.LocalPath);
var file = DafnyFile.CreateAndValidate(errorReporter, fileSystem, Options, uri, Token.Cli,
var file = await DafnyFile.CreateAndValidate(errorReporter, fileSystem, Options, uri, Token.Cli,
$"command-line argument '{shortPath}' is neither a recognized option nor a Dafny input file (.dfy, .doo, or .toml).");
if (file != null) {
result.Add(file);
Expand All @@ -150,29 +153,46 @@ private IReadOnlyList<DafnyFile> DetermineRootFiles() {
}
if (Options.UseStdin) {
var uri = new Uri("stdin:///");
result.Add(DafnyFile.CreateAndValidate(errorReporter, fileSystem, Options, uri, Token.Cli));
result.Add(await DafnyFile.CreateAndValidate(errorReporter, fileSystem, Options, uri, Token.Cli));
}

if (Options.Get(CommonOptionBag.UseStandardLibraries)) {
if (Options.CompilerName is null or "cs" or "java" or "go" or "py" or "js") {
var targetName = Options.CompilerName ?? "notarget";
var stdlibDooUri = DafnyMain.StandardLibrariesDooUriTarget[targetName];
result.Add(DafnyFile.CreateAndValidate(errorReporter, OnDiskFileSystem.Instance, Options, stdlibDooUri, Project.StartingToken));
var targetSpecificFile = await DafnyFile.CreateAndValidate(errorReporter, OnDiskFileSystem.Instance, Options, stdlibDooUri, Project.StartingToken);
if (targetSpecificFile != null) {
result.Add(targetSpecificFile);
}
}

result.Add(DafnyFile.CreateAndValidate(errorReporter, fileSystem, Options, DafnyMain.StandardLibrariesDooUri, Project.StartingToken));
var file = await DafnyFile.CreateAndValidate(errorReporter, fileSystem, Options, DafnyMain.StandardLibrariesDooUri, Project.StartingToken);
if (file != null) {
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is a bit dangerous though, isn't it? If there's some packaging error and the main stdlib doo file is missing, we'll silently ignore it. Better to throw a description internal exception I think.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oof, I don't recall why this was needed. Well, fastest way to remember is to remove it again ^,^

Copy link
Member Author

@keyboardDrummer keyboardDrummer Apr 10, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Without it, the tests fail:

  Failed stdlibs/StandardLibraries_Errors.dfy [52 s]
  Error Message:
   System.AggregateException : One or more errors occurred. (Command returned non-zero exit code (1): DiffCommand TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_Errors.dfy.expect /home/runner/work/dafny/dafny/dafny/Source/IntegrationTests/bin/Debug/net6.0/TestFiles/LitTests/LitTest/stdlibs/Output/StandardLibraries_Errors.dfy.tmp
Output:
AssertEqualWithDiff() Failure
Diff (changing expected into actual):
 
 Dafny program verifier finished with 1 verified, 0 errors
 
 Dafny program verifier finished with 1 verified, 0 errors
 StandardLibraries_Errors.dfy(20,20): Error: module Std does not exist (position 0 in path Std.Wrappers)
 1 resolution/type errors detected in StandardLibraries_Errors.dfy
 CLI: Error: cannot load DafnyStandardLibraries-notarget.doo: --unicode-char is set locally to False, but the library was built with True
 CLI: Error: cannot load DafnyStandardLibraries.doo: --unicode-char is set locally to False, but the library was built with True
+Encountered internal compilation exception: Object reference not set to an instance of an object.
 Please use the '--check' and/or '--print' option as doo files cannot be formatted in place.
 Please use the '--check' and/or '--print' option as doo files cannot be formatted in place.

Seems there is no custom check to prevent --unicode-char false and --standard-libraries from being used together. This is discovered and reported in the call to DafnyFile.CreateAndValidate, after which it still returns null and should not crash because of that.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah that's fair, if the file is missing it should fail more loudly. I forgot that CreateAndValidate only returns null if the file wasn't valid.

result.Add(file);
}
}

string? unverifiedLibrary = null;
var libraryFiles = CommonOptionBag.SplitOptionValueIntoFiles(Options.Get(CommonOptionBag.Libraries).Select(f => f.FullName));
foreach (var library in libraryFiles) {
var file = DafnyFile.CreateAndValidate(errorReporter, fileSystem, Options, new Uri(library), Project.StartingToken);
var file = await DafnyFile.CreateAndValidate(errorReporter, fileSystem, Options, new Uri(library), Project.StartingToken);
if (file != null) {
if (!file.IsPreverified) {
unverifiedLibrary = library;
}
file.IsPreverified = true;
file.IsPrecompiled = true;
result.Add(file);
}
}

if (unverifiedLibrary != null) {
errorReporter.Warning(MessageSource.Project, "", Project.StartingToken,
$"The file '{Options.GetPrintPath(unverifiedLibrary)}' was passed to --library. " +
$"Verification for that file might have used options incompatible with the current ones, or might have been skipped entirely. " +
$"Use a .doo file to enable Dafny to check that compatible options were used");
}

var projectPath = Project.Uri.LocalPath;
if (projectPath.EndsWith(DafnyProject.FileName)) {
var projectDirectory = Path.GetDirectoryName(projectPath)!;
Expand All @@ -188,12 +208,15 @@ private IReadOnlyList<DafnyFile> DetermineRootFiles() {
}

// Allow specifying the same file twice on the CLI
return result.DistinctBy(d => d.Uri).ToList();
var distinctResults = result.DistinctBy(d => d.Uri).ToList();

updates.OnNext(new DeterminedRootFiles(Project, distinctResults, GetDiagnosticsCopyAndClear()));
return distinctResults;
}

private async Task<Program?> ParseAsync() {
try {
await started.Task;
await RootFiles;
if (HasErrors) {
return null;
}
Expand Down
Loading