Skip to content

Commit

Permalink
Merge branch 'master' into release-4.6.0
Browse files Browse the repository at this point in the history
  • Loading branch information
@robin-aws
robin-aws committed May 1, 2024
2 parents 59f25d6 + 8ed91c4 commit 7c03e58
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 7c03e58

Please sign in to comment.