Skip to content

Commit

Permalink
Add support for base field in project files (#5359)
Browse files Browse the repository at this point in the history 
Fixes #5337

### Description
- Add the field `base` to Dafny project files, which allows a project
file to inherit fields from another one. Options from the current file
override options from the base. Includes from the current file override
excludes from the base, and excludes from the current file override
includes from the base. The base may itself also have a base.
- Small improvements to project file error reporting. See the updates in
existing tests for more information.

### How has this been tested?
 - Added the test `cli/projectFile/base/included.dfy`

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
  • Loading branch information
@keyboardDrummer
keyboardDrummer committed May 1, 2024
1 parent 88808ee commit 8ed91c4
Show file tree
Hide file tree
Showing 16 changed files with 185 additions and 112 deletions.
21 changes: 9 additions & 12 deletions Source/DafnyCore.Test/DafnyProjectTest.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,25 +6,22 @@ public class DafnyProjectTest {
[Fact]
public void Equality() {
var randomFileName = Path.GetTempFileName();
var first = new DafnyProject() {
Uri = new Uri(randomFileName, UriKind.Absolute),
Includes = new[] { "a", "a2" },
Excludes = new[] { "b", "b2" },
Options = new Dictionary<string, object>() {
var first = new DafnyProject(new Uri(randomFileName, UriKind.Absolute), null,
new[] { "a", "a2" }.ToHashSet(),
new[] { "b", "b2" }.ToHashSet(), new Dictionary<string, object>() {
{ "c", "d" },
{ "e", "f" }
}
};
);

var second = new DafnyProject() {
Uri = new Uri(randomFileName, UriKind.Absolute),
Includes = new[] { "a2", "a" },
Excludes = new[] { "b2", "b" },
Options = new Dictionary<string, object>() {
var second = new DafnyProject(new Uri(randomFileName, UriKind.Absolute), null,
new[] { "a2", "a" }.ToHashSet(),
new[] { "b2", "b" }.ToHashSet(),
new Dictionary<string, object>() {
{ "e", "f" },
{ "c", "d" },
}
};
);

Assert.Equal(first, second);

Expand Down
176 changes: 113 additions & 63 deletions Source/DafnyCore/Options/DafnyProject.cs
View file
Original file line number Diff line number Diff line change
@@ -1,17 +1,14 @@
#nullable enable
using System;
using System.Collections;
using System.Collections.Generic;
using System.CommandLine;
using System.CommandLine.Parsing;
using System.Diagnostics.CodeAnalysis;
using System.IO;
using System.Linq;
using System.Reflection;
using System.Runtime.Serialization;
using System.Text;
using System.Text.RegularExpressions;
using System.Threading.Tasks;
using DafnyCore.Options;
using JetBrains.Annotations;
using Microsoft.Extensions.FileSystemGlobbing;
using Tomlyn;
using Tomlyn.Model;
Expand All @@ -24,14 +21,16 @@ public class DafnyProject : IEquatable<DafnyProject> {

public string ProjectName => Uri.ToString();

[IgnoreDataMember]
public BatchErrorReporter Errors { get; init; } = new(DafnyOptions.Default);

[IgnoreDataMember]
public Uri Uri { get; set; }
public string[] Includes { get; set; }
public string[] Excludes { get; set; }
public Dictionary<string, object> Options { get; set; }

public Uri? Base { get; set; }

public ISet<string> Includes { get; }
public ISet<string> Excludes { get; }
public IDictionary<string, object> Options { get; }

public bool UsesProjectFile => Path.GetFileName(Uri.LocalPath) == FileName;
public bool ImplicitFromCli;

Expand All @@ -41,38 +40,92 @@ public class DafnyProject : IEquatable<DafnyProject> {
col = 1
};

public DafnyProject() {
public DafnyProject(Uri uri, Uri? @base, ISet<string> includes, ISet<string>? excludes = null, IDictionary<string, object>? options = null) {
Uri = uri;
Base = @base;
Includes = includes;
Excludes = excludes ?? new HashSet<string>();
Options = options ?? new Dictionary<string, object>();
}

public static async Task<DafnyProject> Open(IFileSystem fileSystem, DafnyOptions dafnyOptions, Uri uri) {
public static async Task<DafnyProject> Open(IFileSystem fileSystem, DafnyOptions dafnyOptions, Uri uri, bool defaultIncludes = true) {

var emptyProject = new DafnyProject {
Uri = uri
};
var emptyProject = new DafnyProject(uri, null, new HashSet<string>(), new HashSet<string>(),
new Dictionary<string, object>());

DafnyProject result;
try {
using var textReader = fileSystem.ReadFile(uri);
var text = await textReader.ReadToEndAsync();
var model = Toml.ToModel<DafnyProject>(text, null, new TomlModelOptions());
model.Uri = uri;
result = model;
var model = Toml.ToModel<DafnyProjectFile>(text, null, new TomlModelOptions());
var directory = Path.GetDirectoryName(uri.LocalPath)!;

result = new DafnyProject(uri, model.Base == null ? null : new Uri(Path.GetFullPath(model.Base, directory!)),
model.Includes?.Select(p => Path.GetFullPath(p, directory)).ToHashSet() ?? new HashSet<string>(),
model.Excludes?.Select(p => Path.GetFullPath(p, directory)).ToHashSet() ?? new HashSet<string>(),
model.Options ?? new Dictionary<string, object>());

if (result.Base != null) {
var baseProject = await Open(fileSystem, dafnyOptions, result.Base, false);
baseProject.Errors.CopyDiagnostics(result.Errors);
foreach (var include in baseProject.Includes) {
if (!result.Excludes.Contains(include)) {
result.Includes.Add(include);
}
}

foreach (var include in baseProject.Excludes) {
if (!result.Includes.Contains(include)) {
result.Excludes.Add(include);
}
}

foreach (var option in baseProject.Options) {
if (!result.Options.ContainsKey(option.Key)) {
result.Options.Add(option.Key, option.Value);
}
}
}
if (defaultIncludes && model.Includes == null && !result.Includes.Any()) {
result.Includes.Add("**/*.dfy");
}
} catch (IOException e) {
result = emptyProject;
result.Errors.Error(MessageSource.Project, result.StartingToken, e.Message);
} catch (TomlException tomlException) {
var regex = new Regex(
var propertyNotFoundRegex = new Regex(
@$"\((\d+),(\d+)\) : error : The property `(\w+)` was not found on object type {typeof(DafnyProject).FullName}");
var newMessage = regex.Replace(tomlException.Message,
match =>
$"({match.Groups[1].Value},{match.Groups[2].Value}): the property {match.Groups[3].Value} does not exist.");
result = emptyProject;
var path = dafnyOptions.GetPrintPath(uri.LocalPath);
result.Errors.Error(MessageSource.Project, result.StartingToken, $"The Dafny project file {path} contains the following errors: {newMessage}");
var propertyNotFoundMatch = propertyNotFoundRegex.Match(tomlException.Message);
if (propertyNotFoundMatch.Success) {
var line = int.Parse(propertyNotFoundMatch.Groups[1].Value);
var column = int.Parse(propertyNotFoundMatch.Groups[2].Value);
var property = propertyNotFoundMatch.Groups[3].Value;
result = emptyProject;
var token = new Token(line, column) {
Uri = uri
};
result.Errors.Error(MessageSource.Project, token,
$"Dafny project files do not have the property {property}");
} else {
var genericRegex = new Regex(@$"\((\d+),(\d+)\) : error : (.*)");
var genericMatch = genericRegex.Match(tomlException.Message);
if (genericMatch.Success) {
var line = int.Parse(genericMatch.Groups[1].Value);
var column = int.Parse(genericMatch.Groups[2].Value);
var message = genericMatch.Groups[3].Value;
result = emptyProject;
var token = new Token(line, column) {
Uri = uri
};
result.Errors.Error(MessageSource.Project, token, message);
} else {
throw new Exception("Could not parse Tomlyn error");
}
}
}

if (Path.GetFileName(uri.LocalPath) != FileName) {
result.Errors.Warning(MessageSource.Project, (string)null, result.StartingToken, $"only Dafny project files named {FileName} are recognised by the Dafny IDE.");
result.Errors.Warning(MessageSource.Project, "", result.StartingToken, $"only Dafny project files named {FileName} are recognised by the Dafny IDE.");
}

return result;
Expand Down Expand Up @@ -100,8 +153,8 @@ public class DafnyProject : IEquatable<DafnyProject> {
var projectRoot = Path.GetDirectoryName(Uri.LocalPath)!;
var diskRoot = Path.GetPathRoot(Uri.LocalPath)!;

var includes = Includes ?? new[] { "**/*.dfy" };
var excludes = Excludes ?? Array.Empty<string>();
var includes = Includes;
var excludes = Excludes;
var fullPaths = includes.Concat(excludes).Select(p => Path.GetFullPath(p, projectRoot)).ToList();
commonRoot = GetCommonParentDirectory(fullPaths) ?? diskRoot;
var matcher = new Matcher();
Expand All @@ -116,11 +169,11 @@ public class DafnyProject : IEquatable<DafnyProject> {
return matcher;
}

string GetCommonParentDirectory(IReadOnlyList<string> strings) {
string? GetCommonParentDirectory(IReadOnlyList<string> strings) {
if (!strings.Any()) {
return null;
}
var commonPrefix = strings.FirstOrDefault() ?? "";
string commonPrefix = strings.FirstOrDefault() ?? "";

foreach (var newString in strings) {
var potentialMatchLength = Math.Min(newString.Length, commonPrefix.Length);
Expand All @@ -138,16 +191,13 @@ public class DafnyProject : IEquatable<DafnyProject> {
}

if (!Path.EndsInDirectorySeparator(commonPrefix)) {
commonPrefix = Path.GetDirectoryName(commonPrefix);
commonPrefix = Path.GetDirectoryName(commonPrefix)!;
}

return commonPrefix;
}

public void Validate(TextWriter outputWriter, IEnumerable<Option> possibleOptions) {
if (Options == null) {
return;
}

var possibleNames = possibleOptions.Select(o => o.Name).ToHashSet();
foreach (var optionThatDoesNotExist in Options.Where(option => !possibleNames.Contains(option.Key))) {
Expand All @@ -156,12 +206,7 @@ public class DafnyProject : IEquatable<DafnyProject> {
}
}

public bool TryGetValue(Option option, out object value) {
if (Options == null) {
value = null;
return false;
}

public bool TryGetValue(Option option, out object? value) {
if (!Options.TryGetValue(option.Name, out var tomlValue)) {
value = null;
return false;
Expand All @@ -180,22 +225,21 @@ public class DafnyProject : IEquatable<DafnyProject> {
return true;
}

[ItemCanBeNull]
IEnumerable<string> PrintTomlOptionToCliValue(object value, Option valueType) {
var projectDirectory = Path.GetDirectoryName(Uri.LocalPath);
var projectDirectory = Path.GetDirectoryName(Uri.LocalPath)!;

if (value is TomlArray array) {
List<string> elements;
if (valueType.ValueType.IsAssignableTo(typeof(IEnumerable<FileInfo>))) {
elements = array.Select(element => {
if (element is string elementString) {
return Path.GetFullPath(elementString, projectDirectory!);
return Path.GetFullPath(elementString, projectDirectory);
}
return element.ToString();
return element + "";
}).ToList();
} else {
elements = array.Select(o => o.ToString()).ToList();
elements = array.Select(o => o + "").ToList();
}

return elements.SelectMany(e => new[] { valueType.Aliases.First(), e });
Expand All @@ -205,10 +249,10 @@ public class DafnyProject : IEquatable<DafnyProject> {
value = Path.GetFullPath(stringValue, projectDirectory);
}

return new[] { valueType.Aliases.First(), value.ToString() };
return new[] { valueType.Aliases.First(), value + "" };
}

public bool Equals(DafnyProject other) {
public bool Equals(DafnyProject? other) {
if (ReferenceEquals(null, other)) {
return false;
}
Expand All @@ -217,18 +261,19 @@ public class DafnyProject : IEquatable<DafnyProject> {
return true;
}

var orderedOptions = Options?.OrderBy(kv => kv.Key) ?? Enumerable.Empty<KeyValuePair<string, object>>();
var otherOrderedOptions = other.Options?.OrderBy(kv => kv.Key) ?? Enumerable.Empty<KeyValuePair<string, object>>();
var orderedOptions = Options.OrderBy(kv => kv.Key);
var otherOrderedOptions = other.Options.OrderBy(kv => kv.Key);

return Equals(Uri, other.Uri) &&
NullableSetEqual(Includes?.ToHashSet(), other.Includes) &&
NullableSetEqual(Excludes?.ToHashSet(), other.Excludes) &&
NullableSetEqual(Includes, other.Includes) &&
NullableSetEqual(Excludes, other.Excludes) &&
orderedOptions.SequenceEqual(otherOrderedOptions, new LambdaEqualityComparer<KeyValuePair<string, object>>(
(kv1, kv2) => kv1.Key == kv2.Key && GenericEquals(kv1.Value, kv2.Value),
kv => kv.GetHashCode()));
}

public static bool GenericEquals(object first, object second) {
[SuppressMessage("ReSharper", "NotDisposedResource")]
public static bool GenericEquals(object? first, object? second) {
if (first == null && second == null) {
return true;
}
Expand Down Expand Up @@ -261,7 +306,7 @@ public class DafnyProject : IEquatable<DafnyProject> {
return first.Equals(second);
}

private static bool NullableSetEqual(ISet<string> first, IReadOnlyCollection<string> second) {
private static bool NullableSetEqual(ISet<string>? first, ICollection<string>? second) {
if (first == null && second == null) {
return true;
}
Expand All @@ -272,21 +317,19 @@ public class DafnyProject : IEquatable<DafnyProject> {
return first.Count == second.Count && second.All(first.Contains);
}

private static bool NullableSequenceEqual(IEnumerable<string> first, IEnumerable<string> second) {
return first?.SequenceEqual(second) ?? (second == null);
public DafnyProject(DafnyProject original) {
Uri = original.Uri;
Includes = original.Includes.ToHashSet();
Excludes = original.Excludes.ToHashSet();
Options = original.Options.ToDictionary(kv => kv.Key, kv => kv.Value);
Errors = original.Errors;
}

public DafnyProject Clone() {
return new DafnyProject() {
Uri = Uri,
Includes = Includes?.ToArray(),
Excludes = Excludes?.ToArray(),
Options = Options?.ToDictionary(kv => kv.Key, kv => kv.Value),
Errors = Errors
};
return new DafnyProject(this);
}

public override bool Equals(object obj) {
public override bool Equals(object? obj) {
if (ReferenceEquals(null, obj)) {
return false;
}
Expand All @@ -302,8 +345,15 @@ public class DafnyProject : IEquatable<DafnyProject> {
return Equals((DafnyProject)obj);
}

[SuppressMessage("ReSharper", "NonReadonlyMemberInGetHashCode")]
public override int GetHashCode() {
return HashCode.Combine(Uri, Includes, Excludes, Options);
}
}

class DafnyProjectFile {
public string? Base { get; set; }
public string[]? Includes { get; set; }
public string[]? Excludes { get; set; }
public Dictionary<string, object>? Options { get; set; }
}
6 changes: 2 additions & 4 deletions Source/DafnyDriver/CliCompilation.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,6 @@
using System;
using System.Collections.Concurrent;
using System.Collections.Generic;
using System.Globalization;
using System.IO;
using System.Linq;
using System.Text.RegularExpressions;
Expand Down Expand Up @@ -37,9 +36,8 @@ public class CliCompilation {
if (options.DafnyProject == null) {
var firstFile = options.CliRootSourceUris.FirstOrDefault();
var uri = firstFile ?? new Uri(Directory.GetCurrentDirectory());
options.DafnyProject = new DafnyProject {
Includes = Array.Empty<string>(),
Uri = uri,
options.DafnyProject = new DafnyProject(uri, null, new HashSet<string>(), new HashSet<string>(),
new Dictionary<string, object>()) {
ImplicitFromCli = true
};
}
Expand Down
Loading

0 comments on commit 8ed91c4

Please sign in to comment.