diff --git a/Binaries/.gitignore b/Binaries/.gitignore deleted file mode 100644 index 1e1e2a09ca6..00000000000 --- a/Binaries/.gitignore +++ /dev/null @@ -1 +0,0 @@ -DafnyRuntime.jar diff --git a/Scripts/dafny b/Scripts/dafny index ab813e0ca37..2b84c32dc1b 100755 --- a/Scripts/dafny +++ b/Scripts/dafny @@ -17,7 +17,7 @@ if [ "${MY_OS:0:5}" == "MINGW" ] || [ "${MY_OS:0:6}" == "CYGWIN" ]; then else DAFNY_EXE_NAME="Dafny.dll" fi -DAFNY="$DAFNY_ROOT/Binaries/$DAFNY_EXE_NAME" +DAFNY="$DAFNY_ROOT/Binaries/net8.0/$DAFNY_EXE_NAME" if [[ ! -e "$DAFNY" ]]; then echo "Error: $DAFNY_EXE_NAME not found at $DAFNY." exit 1 diff --git a/Source/AutoExtern.Test/AutoExtern.Test.csproj b/Source/AutoExtern.Test/AutoExtern.Test.csproj index 0c4e1dc0b51..4947cc7ecaf 100644 --- a/Source/AutoExtern.Test/AutoExtern.Test.csproj +++ b/Source/AutoExtern.Test/AutoExtern.Test.csproj @@ -2,7 +2,7 @@ Exe - net6.0 + net8.0 enable enable false diff --git a/Source/AutoExtern.Test/Minimal/Library.csproj b/Source/AutoExtern.Test/Minimal/Library.csproj index 132c02c59c2..30402ac0e7a 100644 --- a/Source/AutoExtern.Test/Minimal/Library.csproj +++ b/Source/AutoExtern.Test/Minimal/Library.csproj @@ -1,7 +1,7 @@ - net6.0 + net8.0 enable enable diff --git a/Source/AutoExtern.Test/Tutorial/ClientApp/ClientApp.csproj b/Source/AutoExtern.Test/Tutorial/ClientApp/ClientApp.csproj index 86b01ff865f..16692440fb3 100644 --- a/Source/AutoExtern.Test/Tutorial/ClientApp/ClientApp.csproj +++ b/Source/AutoExtern.Test/Tutorial/ClientApp/ClientApp.csproj @@ -2,7 +2,7 @@ Exe - net6.0 + net8.0 enable CS3021; CS0162 diff --git a/Source/AutoExtern.Test/Tutorial/Library/Library.csproj b/Source/AutoExtern.Test/Tutorial/Library/Library.csproj index 132c02c59c2..30402ac0e7a 100644 --- a/Source/AutoExtern.Test/Tutorial/Library/Library.csproj +++ b/Source/AutoExtern.Test/Tutorial/Library/Library.csproj @@ -1,7 +1,7 @@ - net6.0 + net8.0 enable enable diff --git a/Source/AutoExtern/AutoExtern.csproj b/Source/AutoExtern/AutoExtern.csproj index 0c00890cffc..f44de5524b4 100644 --- a/Source/AutoExtern/AutoExtern.csproj +++ b/Source/AutoExtern/AutoExtern.csproj @@ -2,7 +2,7 @@ Exe - net6.0 + net8.0 enable enable false diff --git a/Source/CompilerBuilder.Test/CompilerBuilder.Test.csproj b/Source/CompilerBuilder.Test/CompilerBuilder.Test.csproj new file mode 100644 index 00000000000..d6b0a1e8f3b --- /dev/null +++ b/Source/CompilerBuilder.Test/CompilerBuilder.Test.csproj @@ -0,0 +1,27 @@ + + + + net8.0 + enable + enable + + false + true + + + + + + + + + + + + + + + + + + diff --git a/Source/CompilerBuilder.Test/TestGrammars.cs b/Source/CompilerBuilder.Test/TestGrammars.cs new file mode 100644 index 00000000000..614978cc376 --- /dev/null +++ b/Source/CompilerBuilder.Test/TestGrammars.cs @@ -0,0 +1,117 @@ +using CompilerBuilder.Grammars; + +namespace CompilerBuilder.Test; + +using static GrammarBuilder; + +public class TestGrammars { + + [Fact] + public void TestNumber() { + var number = Number; + var parsed = number.ToParser().Parse("123124").Success!.Value; + Assert.Equal(123124, parsed); + } + + [Fact] + public void TestIdentifier() { + var number = Identifier; + var parsed = number.ToParser().Parse("abcdefg").Success!.Value; + Assert.Equal("abcdefg", parsed); + } + + [Fact] + public void TestKeyword() { + var parser = Keyword("hello").Then(Constant(true)); + var parsed = parser.ToParser().Parse("hello").Success!.Value; + Assert.True(parsed); + + var byeResult = parser.ToParser().Parse("bye"); + Assert.Contains("Expected", byeResult.Failure!.Message); + } + + [Fact] + public void TestChoice() { + var numberOrIdentifier = Number.UpCast().Or(Identifier.UpCast()); + Assert.Equal(123124, numberOrIdentifier.ToParser().Parse("123124").Success!.Value); + Assert.Equal("abcefg", numberOrIdentifier.ToParser().Parse("abcefg").Success!.Value); + Assert.Null(numberOrIdentifier.ToParser().Parse("!@!@$#").Success); + } + + record Person { + public int Age; + public string Name; + } + + [Fact] + public void TestSequence() { + var person = + Constructor(). + Then(Number, (p) => p.Age). + Then(Identifier, (p) => p.Name); + var result = person.ToParser().Parse("123124Jan"); + Assert.Equal(123124, result.Success!.Value.Age); + Assert.Equal("Jan", result.Success!.Value.Name); + Assert.Null(person.ToParser().Parse("1231").Success); + } + + [Fact] + public void TestMany() { + var person = + Constructor(). + Then(Number, (p) => p.Age). + Then(Identifier, (p) => p.Name); + var persons = person.Many(); + var parser = persons.ToParser(); + var goodResult = parser.Parse("123124Jan12313Henk12Remy"); + Assert.Equal(3, goodResult.Success!.Value.Count()); + Assert.Equal("Remy", goodResult.Success!.Value.ElementAt(2).Name); + var badResult = parser.Parse("123124Jan12313Henk12"); + Assert.Null(badResult.Success); + } + + [Fact] + public void LeftRecursive() { + var parser = Recursive(self => Number.Or(self.Then("^")), "LeftRecursiveTest"); + var result = parser.ToParser().Parse("13^^^"); + Assert.Equal(13, result.Success!.Value); + } + + record PersonWithTrivia { + public int Age; + public string Name; + public List Trivia = new(); + + public PersonWithTrivia() { + Age = 0; + Name = null; + } + } + + [Fact] + public void ManualTrivia() { + var trivia = Comments.SlashSlashLineComment().Or(Whitespace).Or(Comments.BlockComment()).Many(); + var person = + Constructor(). + Then(Number, (p) => p.Age). + Then(trivia, (p) => p.Trivia). + Then(Identifier, (p) => p.Name); + var input = "123 Remy"; + var result = person.ToParser().Parse(input); + Assert.NotNull(result.Success); + Assert.Equal(" ", result.Success?.Value.Trivia[0]); + + var input2 = @"123// line comment + +// another linecomment +/** block + +comment +*/ +Remy"; + var result2 = person.ToParser().Parse(input2); + Assert.NotNull(result2.Success); + Assert.Equal("// another linecomment\n", result2.Success?.Value.Trivia[2]); + } + +} \ No newline at end of file diff --git a/Source/CompilerBuilder.Test/TestParsing.cs b/Source/CompilerBuilder.Test/TestParsing.cs new file mode 100644 index 00000000000..ad326b5a68e --- /dev/null +++ b/Source/CompilerBuilder.Test/TestParsing.cs @@ -0,0 +1,133 @@ +namespace CompilerBuilder.Test; + +using static ParserBuilder; + +public class TestParsing { + + [Fact] + public void TestNumber() { + var number = Number; + var parsed = number.Parse("123124").ForceSuccess.Value; + Assert.Equal(123124, parsed); + } + + [Fact] + public void TestChar() { + var parsed = CharInSingleQuotes.Parse("'d'").ForceSuccess.Value; + Assert.Equal("d", parsed); + } + + [Fact] + public void TestIdentifier() { + var number = Identifier; + var result = number.Parse("abcdefg"); + var parsed = result.ForceSuccess.Value; + Assert.Equal("abcdefg", parsed); + } + + [Fact] + public void TestKeyword() { + var parser = Keyword("hello").Then(Constant(true)); + var parsed = parser.Parse("hello").Success!.Value; + Assert.True(parsed); + + var byeResult = parser.Parse("bye"); + Assert.Contains("Expected", byeResult.Failure!.Message); + } + + [Fact] + public void TestChoice() { + var numberOrIdentifier = Fail("a number or identifier"). + Or(Number.Map(i => (object)i).Or(Identifier.Map(s => (object)s))); + Assert.Equal(123124, numberOrIdentifier.Parse("123124").Success!.Value); + Assert.Equal("abcefg", numberOrIdentifier.Parse("abcefg").Success!.Value); + Assert.Null(numberOrIdentifier.Parse("!@!@$#").Success); + + Assert.Equal("'!@#!@' is not the end of the text", numberOrIdentifier.Parse("123124!@#!@#").Failure!.Message); + Assert.Equal("'!@#!@' is not a number or identifier", numberOrIdentifier.Parse("!@#!@#").Failure!.Message); + } + + record Person { + public int Age; + public string Name; + } + + [Fact] + public void TestSequence() { + var person = + Value(() => new Person()). + Then(Number, (p, v) => p.Age = v). + Then(Identifier, (p, v) => p.Name = v); + var result = person.Parse("123124Jan"); + Assert.Equal(123124, result.Success!.Value.Age); + Assert.Equal("Jan", result.Success!.Value.Name); + Assert.Null(person.Parse("1231").Success); + + Assert.Equal("'!@#!@' is not an identifier", person.Parse("123124!@#!@#").Failure!.Message); + } + + [Fact] + public void TestMany() { + var person = + Value(() => new Person()). + Then("^"). + Then(Number, (p, v) => p.Age = v). + Then(Identifier, (p, v) => p.Name = v); + var persons = person.Many(); + var goodResult = persons.Parse("^123124Jan^12313Henk^12Remy"); + Assert.Equal(3, goodResult.ForceSuccess.Value.Count); + Assert.Equal("Remy", goodResult.ForceSuccess.Value[2].Name); + var badResult = persons.Parse("^123124Jan^12313Henk^12"); + Assert.Null(badResult.Success); + } + + [Fact] + public void LeftRecursive() { + var parser = Recursive(self => Number.Or(self.Then("^")), "LeftRecursiveTest"); + var result = parser.Parse("13^^^"); + Assert.Equal(13, result.ForceSuccess.Value); + } + + class PersonWithTrivia { + public int Age; + public string Name; + public List Trivia = new(); + + public PersonWithTrivia() { + Age = 0; + Name = null; + } + } + + [Fact] + public void ManualTrivia() { + var trivia = SlashSlashLineComment.Or(Whitespace).Many(); + var person = + Value(() => new PersonWithTrivia()). + Then(Number, (p, v) => p.Age = v). + Then(trivia, (p, newTrivia) => p.Trivia.AddRange(newTrivia)). + Then(Identifier, (p, v) => p.Name = v); + var input = "123 Remy"; + var result = person.Parse(input); + Assert.NotNull(result.Success); + Assert.Equal(123, result.Success?.Value.Age); + Assert.Equal(" ", result.Success?.Value.Trivia[0]); + + var input2 = @"123// line comment + +// another linecomment +Remy"; + var result2 = person.Parse(input2); + Assert.NotNull(result2.Success); + Assert.Equal("// another linecomment\n", result2.Success?.Value.Trivia[2]); + } + + // There were a lot of issues in the following that this file should test, but did not. + // Things like nested recursive things + // And not dropping intermediate results when growing a seed. + // class Div { + // int Foo(int x) { + // return 3 / x; + // } + // } +} \ No newline at end of file diff --git a/Source/CompilerBuilder.Test/TestPrinting.cs b/Source/CompilerBuilder.Test/TestPrinting.cs new file mode 100644 index 00000000000..3a7b64d0775 --- /dev/null +++ b/Source/CompilerBuilder.Test/TestPrinting.cs @@ -0,0 +1,6 @@ +namespace CompilerBuilder.Test; + + +public class TestPrinting { + +} \ No newline at end of file diff --git a/Source/CompilerBuilder/CompilerBuilder.csproj b/Source/CompilerBuilder/CompilerBuilder.csproj new file mode 100644 index 00000000000..2ff995d1a8b --- /dev/null +++ b/Source/CompilerBuilder/CompilerBuilder.csproj @@ -0,0 +1,15 @@ + + + + Library + net8.0 + enable + enable + + + + + + + + diff --git a/Source/DafnyCore/Rewriters/AutoGeneratedToken.cs b/Source/CompilerBuilder/Generic/AutoGeneratedToken.cs similarity index 83% rename from Source/DafnyCore/Rewriters/AutoGeneratedToken.cs rename to Source/CompilerBuilder/Generic/AutoGeneratedToken.cs index 40c638628c6..275c01e76c4 100644 --- a/Source/DafnyCore/Rewriters/AutoGeneratedToken.cs +++ b/Source/CompilerBuilder/Generic/AutoGeneratedToken.cs @@ -26,10 +26,6 @@ public static bool Is(IToken tok) { return false; } - public static Expression WrapExpression(Expression expr) { - return Expression.CreateParensExpression(new AutoGeneratedToken(expr.tok), expr); - } - public override IToken WithVal(string newVal) { return new AutoGeneratedToken(WrappedToken.WithVal(newVal)); } diff --git a/Source/DafnyCore/Generic/CombinedDirectoryInfo.cs b/Source/CompilerBuilder/Generic/CombinedDirectoryInfo.cs similarity index 100% rename from Source/DafnyCore/Generic/CombinedDirectoryInfo.cs rename to Source/CompilerBuilder/Generic/CombinedDirectoryInfo.cs diff --git a/Source/DafnyCore/Generic/Dictionaries.cs b/Source/CompilerBuilder/Generic/Dictionaries.cs similarity index 100% rename from Source/DafnyCore/Generic/Dictionaries.cs rename to Source/CompilerBuilder/Generic/Dictionaries.cs diff --git a/Source/DafnyCore/Generic/ErrorRegistry.cs b/Source/CompilerBuilder/Generic/ErrorRegistry.cs similarity index 100% rename from Source/DafnyCore/Generic/ErrorRegistry.cs rename to Source/CompilerBuilder/Generic/ErrorRegistry.cs diff --git a/Source/CompilerBuilder/Generic/ExpressionTreeExtensions.cs b/Source/CompilerBuilder/Generic/ExpressionTreeExtensions.cs new file mode 100644 index 00000000000..74cd11d31fa --- /dev/null +++ b/Source/CompilerBuilder/Generic/ExpressionTreeExtensions.cs @@ -0,0 +1,41 @@ +using System.Linq.Expressions; +using System.Reflection; + +namespace CompilerBuilder.Generic; + +public static class ExpressionTreeExtensions { + public static Property GetProperty(this Expression> expr) { + MemberExpression? memberExpression = null; + + var instanceExpr = Expression.Parameter(typeof(TContainer), "instance"); + + if (expr.Body is MemberExpression { Member: FieldInfo field }) { + memberExpression = Expression.Field(instanceExpr, field); + if (field.IsInitOnly) { + throw new ArgumentException($"Field {field.Name} is not writeable"); + } + } + + if (expr.Body is MemberExpression { Member: PropertyInfo property }) { + memberExpression = Expression.Property(instanceExpr, property); + if (!property.CanRead) { + throw new ArgumentException($"Property {property.Name} of type {typeof(TContainer).Name} is not readable"); + } + if (!property.CanWrite) { + throw new ArgumentException($"Property {property.Name} of type {typeof(TContainer).Name} is not writeable"); + } + } + + if (memberExpression == null) { + throw new ArgumentException(); + } + + var propertyObjExpr = Expression.Convert(memberExpression, typeof(TField)); + var getter = Expression.Lambda>(propertyObjExpr, instanceExpr).Compile(); + + var parameter = Expression.Parameter(typeof(TField), "value"); + var setterBody = Expression.Assign(memberExpression, parameter); + var setter = Expression.Lambda>(setterBody, instanceExpr, parameter).Compile(); + return new Property(getter, setter); + } +} \ No newline at end of file diff --git a/Source/DafnyCore/Generic/GenericErrors.cs b/Source/CompilerBuilder/Generic/GenericErrors.cs similarity index 100% rename from Source/DafnyCore/Generic/GenericErrors.cs rename to Source/CompilerBuilder/Generic/GenericErrors.cs diff --git a/Source/DafnyCore/Generic/IPointer.cs b/Source/CompilerBuilder/Generic/IPointer.cs similarity index 89% rename from Source/DafnyCore/Generic/IPointer.cs rename to Source/CompilerBuilder/Generic/IPointer.cs index 73d2252bf77..7a79b159f04 100644 --- a/Source/DafnyCore/Generic/IPointer.cs +++ b/Source/CompilerBuilder/Generic/IPointer.cs @@ -10,7 +10,7 @@ public interface IPointer { void Set(T value); } -record Pointer(Func Get, Action Set) : IPointer { +public record Pointer(Func Get, Action Set) : IPointer { T IPointer.Get() { return Get(); } diff --git a/Source/DafnyCore/AST/Statements/LList.cs b/Source/CompilerBuilder/Generic/LList.cs similarity index 100% rename from Source/DafnyCore/AST/Statements/LList.cs rename to Source/CompilerBuilder/Generic/LList.cs diff --git a/Source/DafnyCore/Generic/LambdaEqualityComparer.cs b/Source/CompilerBuilder/Generic/LambdaEqualityComparer.cs similarity index 100% rename from Source/DafnyCore/Generic/LambdaEqualityComparer.cs rename to Source/CompilerBuilder/Generic/LambdaEqualityComparer.cs diff --git a/Source/DafnyCore/Generic/LazyConcurrentDictionary.cs b/Source/CompilerBuilder/Generic/LazyConcurrentDictionary.cs similarity index 100% rename from Source/DafnyCore/Generic/LazyConcurrentDictionary.cs rename to Source/CompilerBuilder/Generic/LazyConcurrentDictionary.cs diff --git a/Source/DafnyCore/Generic/Lists.cs b/Source/CompilerBuilder/Generic/Lists.cs similarity index 100% rename from Source/DafnyCore/Generic/Lists.cs rename to Source/CompilerBuilder/Generic/Lists.cs diff --git a/Source/CompilerBuilder/Generic/Node.cs b/Source/CompilerBuilder/Generic/Node.cs new file mode 100644 index 00000000000..11f4931a225 --- /dev/null +++ b/Source/CompilerBuilder/Generic/Node.cs @@ -0,0 +1,15 @@ +namespace Microsoft.Dafny; + +public interface INode { + bool SingleFileToken { get; } + public IToken StartToken => RangeToken.StartToken; + public IToken EndToken => RangeToken.EndToken; + IEnumerable OwnedTokens { get; } + RangeToken RangeToken { get; } + IToken Tok { get; } + IEnumerable Children { get; } + IEnumerable PreResolveChildren { get; } +} + + + diff --git a/Source/CompilerBuilder/Generic/NodeExtensions.cs b/Source/CompilerBuilder/Generic/NodeExtensions.cs new file mode 100644 index 00000000000..d473c0ed42a --- /dev/null +++ b/Source/CompilerBuilder/Generic/NodeExtensions.cs @@ -0,0 +1,95 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using System.Reflection.Metadata.Ecma335; +using System.Text.RegularExpressions; + +namespace Microsoft.Dafny; + +public interface IHasDocstring { + /// + /// Unfiltered version that only returns the trivia containing the docstring + /// + public string GetTriviaContainingDocstring(); +} + +public static class NodeExtensions { + + + public static IEnumerable Descendants(this INode node) { + return node.Children.Concat(node.Children.SelectMany(n => n.Descendants())); + } + + public static T FindNode(this INode root, Uri uri, DafnyPosition position) { + return (T)root.FindNodeChain(uri, position, null, node => node is T)?.Data; + } + + public static INode FindNode(this INode node, Uri uri, DafnyPosition position, Func predicate) { + return node.FindNodeChain(uri, position, null, predicate)?.Data; + } + + public static IEnumerable FindNodesInUris(this INode node, Uri uri) { + return node.FindNodeChainsInUri(uri, null).Select(c => c.Data); + } + + public static IEnumerable> FindNodeChainsInUri(this INode node, Uri uri, LList parent) { + if (node.RangeToken.Uri != null) { + if (node.RangeToken.Uri == uri) { + return new[] { new LList(node, parent) }; + } + + return new LList[] { }; + } + + var newParent = new LList(node, parent); + return node.Children.SelectMany(child => child.FindNodeChainsInUri(uri, newParent)); + } + + private static LList FindNodeChain(this INode node, Uri uri, DafnyPosition position, LList parent, + Func predicate) { + if (node.RangeToken.Uri != null) { + if (node.RangeToken.Uri == uri) { + return node.FindNodeChain(position, parent, predicate); + } + + if (node.SingleFileToken) { + return null; + } + } + + var newParent = new LList(node, parent); + foreach (var child in node.Children) { + var result = child.FindNodeChain(uri, position, newParent, predicate); + if (result != null) { + return result; + } + } + + return null; + } + + public static LList FindNodeChain(this INode node, DafnyPosition position, Func predicate) { + return FindNodeChain(node, position, new LList(node, null), predicate); + } + + private static LList FindNodeChain(this INode node, DafnyPosition position, LList parent, + Func predicate) { + if (node.Tok is AutoGeneratedToken || (node.Tok != Token.NoToken && !node.RangeToken.ToDafnyRange().Contains(position))) { + return null; + } + + var newParent = new LList(node, parent); + foreach (var child in node.Children) { + var result = child.FindNodeChain(position, newParent, predicate); + if (result != null) { + return result; + } + } + + if (node.Tok == Token.NoToken || !predicate(node)) { + return null; + } + + return new LList(node, parent); + } +} \ No newline at end of file diff --git a/Source/DafnyCore/Generic/PredicateEqualityComparer.cs b/Source/CompilerBuilder/Generic/PredicateEqualityComparer.cs similarity index 100% rename from Source/DafnyCore/Generic/PredicateEqualityComparer.cs rename to Source/CompilerBuilder/Generic/PredicateEqualityComparer.cs diff --git a/Source/DafnyCore/Generic/SccGraph.cs b/Source/CompilerBuilder/Generic/SccGraph.cs similarity index 100% rename from Source/DafnyCore/Generic/SccGraph.cs rename to Source/CompilerBuilder/Generic/SccGraph.cs diff --git a/Source/CompilerBuilder/Generic/SinglyLinkedList.cs b/Source/CompilerBuilder/Generic/SinglyLinkedList.cs new file mode 100644 index 00000000000..c325ca0a076 --- /dev/null +++ b/Source/CompilerBuilder/Generic/SinglyLinkedList.cs @@ -0,0 +1,100 @@ +using System.Collections; + +namespace Microsoft.Dafny; + +class LinkedListEnumerator(SinglyLinkedList remainder) : IEnumerator { + private T? current; + + public bool MoveNext() { + return remainder.Fold((head, tail) => { + current = head; + remainder = tail; + return true; + }, () => false); + } + + public void Reset() { + throw new NotSupportedException(); + } + + public T Current => current!; + + object IEnumerator.Current => Current!; + + public void Dispose() { + } +} + +public abstract record SinglyLinkedList : IEnumerable { + public IEnumerator GetEnumerator() { + return new LinkedListEnumerator(this); + } + + IEnumerator IEnumerable.GetEnumerator() { + return GetEnumerator(); + } + + public abstract bool Any(); + + public (T, SinglyLinkedList)? ToNullable() { + return Fold((head, tail) => (head, tail), () => ((T,SinglyLinkedList)?)null); + } + + public abstract U Fold(Func, U> cons, Func nil); +} + +public static class LinkedLists { + public static SinglyLinkedList Concat(SinglyLinkedList left, SinglyLinkedList right) { + return left.Fold( + (head, tail) => new Cons(head, Concat(tail, right)), + () => right); + } + + + public static SinglyLinkedList FromList(IReadOnlyList values, SinglyLinkedList? tail = null) { + SinglyLinkedList result = tail ?? new Nil(); + for (int i = values.Count - 1; i >= 0; i--) { + result = new Cons(values[i], result); + } + return result; + } + + public static SinglyLinkedList Create(params T[] values) { + return FromList(values); + } +} + + +public record Cons(T Head, SinglyLinkedList Tail) : SinglyLinkedList { + public override bool Any() { + return true; + } + + public override U Fold(Func, U> cons, Func nil) { + return cons(Head, Tail); + } +} + +public record Nil : SinglyLinkedList { + public override bool Any() { + return false; + } + + public override U Fold(Func, U> cons, Func nil) { + return nil(); + } +} + +record LinkedListFromList(IReadOnlyList Source, int Offset = 0) : SinglyLinkedList { + public override bool Any() { + return Source.Count > Offset; + } + + public override U Fold(Func, U> cons, Func nil) { + if (Source.Count > Offset) { + return cons(Source[Offset], new LinkedListFromList(Source, Offset + 1)); + } + + return nil(); + } +} diff --git a/Source/DafnyCore/Generic/Stringify.cs b/Source/CompilerBuilder/Generic/Stringify.cs similarity index 100% rename from Source/DafnyCore/Generic/Stringify.cs rename to Source/CompilerBuilder/Generic/Stringify.cs diff --git a/Source/DafnyCore/AST/Tokens.cs b/Source/CompilerBuilder/Generic/Tokens.cs similarity index 91% rename from Source/DafnyCore/AST/Tokens.cs rename to Source/CompilerBuilder/Generic/Tokens.cs index ac755b994f8..fc814b6ce26 100644 --- a/Source/DafnyCore/AST/Tokens.cs +++ b/Source/CompilerBuilder/Generic/Tokens.cs @@ -57,6 +57,7 @@ public class Token : IToken { public Token peekedTokens; // Used only internally by Coco when the scanner "peeks" tokens. Normally null at the end of parsing public static readonly Token NoToken = new(); + public static readonly Token Parsing = new(); public static readonly Token Cli = new(1, 1); public static readonly Token Ide = new(1, 1); public Token() : this(0, 0) { } @@ -208,27 +209,6 @@ public static class TokenExtensions { public static bool IsSet(this IToken token) => token.Uri != null; - public static string TokenToString(this IToken tok, DafnyOptions options) { - if (tok == Token.Cli) { - return "CLI"; - } - - if (tok.Uri == null) { - return $"({tok.line},{tok.col - 1})"; - } - - var currentDirectory = Directory.GetCurrentDirectory(); - string filename = tok.Uri.Scheme switch { - "stdin" => "", - "transcript" => Path.GetFileName(tok.Filepath), - _ => options.UseBaseNameForFileName - ? Path.GetFileName(tok.Filepath) - : (tok.Filepath.StartsWith(currentDirectory) ? Path.GetRelativePath(currentDirectory, tok.Filepath) : tok.Filepath) - }; - - return $"{filename}({tok.line},{tok.col - 1})"; - } - public static RangeToken ToRange(this IToken token) { if (token is BoogieRangeToken boogieRangeToken) { return new RangeToken(boogieRangeToken.StartToken, boogieRangeToken.EndToken); @@ -289,14 +269,6 @@ public int Length() { return EndToken.pos - StartToken.pos; } - public RangeToken MakeAutoGenerated() { - return new RangeToken(new AutoGeneratedToken(StartToken), EndToken); - } - - public RangeToken MakeRefined(ModuleDefinition module) { - return new RangeToken(new RefinementToken(StartToken, module), EndToken); - } - // TODO rename to Generated, and Token.NoToken to Token.Generated, and remove AutoGeneratedToken. public static RangeToken NoToken = new(Token.NoToken, Token.NoToken); private readonly IToken endToken; diff --git a/Source/CompilerBuilder/Generic/Util.cs b/Source/CompilerBuilder/Generic/Util.cs new file mode 100644 index 00000000000..91f58c73897 --- /dev/null +++ b/Source/CompilerBuilder/Generic/Util.cs @@ -0,0 +1,430 @@ +// Copyright by the contributors to the Dafny Project +// SPDX-License-Identifier: MIT + +using System.Diagnostics.Contracts; +using System.Text; +using System.Text.RegularExpressions; + +namespace Microsoft.Dafny { + public static class Sets { + public static ISet Empty() { + return new HashSet(); + } + } + + public static class Util { + + public static T Identity(T value) { + return value; + } + + public static readonly Regex Utf16Escape = new Regex(@"\\u([0-9a-fA-F]{4})"); + public static readonly Regex UnicodeEscape = new Regex(@"\\U\{([0-9a-fA-F_]+)\}"); + private static readonly Regex NullEscape = new Regex(@"\\0"); + + private static string ToUtf16Escape(char c, bool addBraces = false) { + if (addBraces) { + return $"\\u{{{(int)c:x4}}}"; + } else { + return $"\\u{(int)c:x4}"; + } + } + + public static string ReplaceNullEscapesWithCharacterEscapes(string s) { + return ReplaceTokensWithEscapes(s, NullEscape, match => "\\u0000"); + } + public static string ExpandUnicodeEscapes(string s, bool lowerCaseU) { + return ReplaceTokensWithEscapes(s, UnicodeEscape, match => { + var hexDigits = Util.RemoveUnderscores(match.Groups[1].Value); + var padChars = 8 - hexDigits.Length; + return (lowerCaseU ? "\\u" : "\\U") + new string('0', padChars) + hexDigits; + }); + } + + public static string UnicodeEscapesToLowercase(string s) { + return ReplaceTokensWithEscapes(s, UnicodeEscape, match => + $"\\u{{{RemoveUnderscores(match.Groups[1].Value)}}}"); + } + + public static string UnicodeEscapesToUtf16Escapes(string s) { + return ReplaceTokensWithEscapes(s, UnicodeEscape, match => { + var utf16CodeUnits = new char[2]; + var hexDigits = RemoveUnderscores(match.Groups[1].Value); + var codePoint = new Rune(Convert.ToInt32(hexDigits, 16)); + var codeUnits = codePoint.EncodeToUtf16(utf16CodeUnits); + if (codeUnits == 2) { + return ToUtf16Escape(utf16CodeUnits[0]) + ToUtf16Escape(utf16CodeUnits[1]); ; + } else { + return ToUtf16Escape(utf16CodeUnits[0]); + } + }); + } + + + public static string ReplaceTokensWithEscapes(string s, Regex pattern, MatchEvaluator evaluator) { + return string.Join("", + TokensWithEscapes(s, false) + .Select(token => pattern.Replace(token, evaluator))); + } + + public static bool MightContainNonAsciiCharacters(string s, bool isVerbatimString) { + // This is conservative since \u and \U escapes could be ASCII characters, + // but that's fine since this method is just used as a conservative guard. + return TokensWithEscapes(s, isVerbatimString).Any(e => + e.Any(c => !char.IsAscii(c)) || e.StartsWith(@"\u") || e.StartsWith(@"\U")); + } + + /// + /// Enumerates the sequence of regular characters and escape sequences in the given well-parsed string. + /// For example, "ab\tuv\u12345" may be broken up as ["a", "b", "\t", "u", "v", "\u1234", "5"]. + /// Consecutive non-escaped characters may or may not be enumerated as a single string. + /// + public static IEnumerable TokensWithEscapes(string p, bool isVerbatimString) { + Contract.Requires(p != null); + if (isVerbatimString) { + var skipNext = false; + foreach (var ch in p) { + if (skipNext) { + skipNext = false; + } else { + if (ch == '"') { + skipNext = true; + yield return "\""; + } else { + yield return ch.ToString(); + } + } + } + } else { + var i = 0; + while (i < p.Length) { + if (p[i] == '\\') { + switch (p[i + 1]) { + case 'u': + yield return p[i..(i + 6)]; + i += 6; + break; + case 'U': + var escapeEnd = p.IndexOf('}', i + 2) + 1; + yield return p[i..escapeEnd]; + i = escapeEnd; + continue; + default: + yield return p[i..(i + 2)]; + i += 2; + break; + } + } else if (char.IsHighSurrogate(p[i])) { + yield return p[i..(i + 2)]; + i += 2; + } else { + yield return p[i].ToString(); + i++; + } + } + } + } + + + /// + /// Returns the characters of the well-parsed string p, replacing any + /// escaped characters by the actual characters. + /// + /// It also converts surrogate pairs to their equivalent code points + /// if --unicode-char is enabled - these are synthesized by the parser when + /// reading the original UTF-8 source, but don't represent the true character values. + /// + public static IEnumerable UnescapedCharacters(bool unicodeChars, string p, bool isVerbatimString) { + if (isVerbatimString) { + foreach (var s in TokensWithEscapes(p, true)) { + if (s == "\"\"") { + yield return '"'; + } else { + foreach (var c in s) { + yield return c; + } + } + } + } else { + foreach (var s in TokensWithEscapes(p, false)) { + switch (s) { + case @"\'": yield return '\''; break; + case @"\""": yield return '"'; break; + case @"\\": yield return '\\'; break; + case @"\0": yield return '\0'; break; + case @"\n": yield return '\n'; break; + case @"\r": yield return '\r'; break; + case @"\t": yield return '\t'; break; + case { } when s.StartsWith(@"\u"): + yield return Convert.ToInt32(s[2..], 16); + break; + case { } when s.StartsWith(@"\U"): + yield return Convert.ToInt32(Util.RemoveUnderscores(s[3..^1]), 16); + break; + case { } when unicodeChars && char.IsHighSurrogate(s[0]): + yield return char.ConvertToUtf32(s[0], s[1]); + break; + default: + foreach (var c in s) { + yield return c; + } + break; + } + } + } + } + + public static Task WaitForComplete(this IObservable observable) { + var result = new TaskCompletionSource(); + observable.Subscribe(_ => { }, e => result.SetException(e), () => result.SetResult()); + return result.Task; + } + + public static string CapitaliseFirstLetter(this string input) { + if (input.Length > 0) { + return char.ToUpper(input[0]) + input.Substring(1); + } + + return input; + } + + public static bool LessThanOrEquals(this T first, T second) + where T : IComparable { + return first.CompareTo(second) != 1; + } + + public static Task SelectMany(this Task task, Func> f) { +#pragma warning disable VSTHRD003 + return Select(task, f).Unwrap(); +#pragma warning restore VSTHRD003 + } + + public static Task Select(this Task task, Func f) { +#pragma warning disable VSTHRD105 + return task.ContinueWith(completedTask => f(completedTask.Result), TaskContinuationOptions.OnlyOnRanToCompletion); +#pragma warning restore VSTHRD105 + } + + public static string Comma(this IEnumerable l) { + return Comma(l, s => s.ToString()); + } + + public static string Comma(this IEnumerable l, Func f) { + return Comma(", ", l, (element, index) => f(element)); + } + + public static string Comma(this IEnumerable l, Func f) { + return Comma(", ", l, f); + } + + public static string Comma(string comma, IEnumerable l, Func f) { + return Comma(comma, l, (element, index) => f(element)); + } + + public static string Comma(string comma, IEnumerable l, Func f) { + Contract.Requires(comma != null); + string res = ""; + string c = ""; + int index = 0; + foreach (var t in l) { + res += c + f(t, index); + c = comma; + index++; + } + return res; + } + + public static string Comma(int count, Func f) { + Contract.Requires(0 <= count); + return Comma(", ", count, f); + } + + public static string Comma(string comma, int count, Func f) { + Contract.Requires(comma != null); + Contract.Requires(0 <= count); + string res = ""; + string c = ""; + for (int i = 0; i < count; i++) { + res += c + f(i); + c = comma; + } + return res; + } + + public static IEnumerable<(T, int)> Indexed(this IEnumerable enumerable) { + return enumerable.Select((value, index) => (value, index)); + } + + public static string PrintableNameList(List names, string grammaticalConjunction) { + Contract.Requires(names != null); + Contract.Requires(1 <= names.Count); + Contract.Requires(grammaticalConjunction != null); + var n = names.Count; + if (n == 1) { + return string.Format("'{0}'", names[0]); + } else if (n == 2) { + return string.Format("'{0}' {1} '{2}'", names[0], grammaticalConjunction, names[1]); + } else { + var s = ""; + for (int i = 0; i < n - 1; i++) { + s += string.Format("'{0}', ", names[i]); + } + return s + string.Format("{0} '{1}'", grammaticalConjunction, names[n - 1]); + } + } + + public static string Repeat(int count, string s) { + Contract.Requires(0 <= count); + Contract.Requires(s != null); + // special-case trivial cases + if (count == 0) { + return ""; + } else if (count == 1) { + return s; + } else { + return Comma("", count, _ => s); + } + } + + public static string Plural(int n) { + Contract.Requires(0 <= n); + return n == 1 ? "" : "s"; + } + + public static List Map(IEnumerable xs, Func f) { + List ys = new List(); + foreach (A x in xs) { + ys.Add(f(x)); + } + return ys; + } + + public static List Nil() { + return new List(); + } + + public static List Singleton(A x) { + return new List { x }; + } + + public static List List(params A[] xs) { + return xs.ToList(); + } + + public static List Cons(A x, List xs) { + return Concat(Singleton(x), xs); + } + + public static List Snoc(List xs, A x) { + return Concat(xs, Singleton(x)); + } + + public static List Concat(List xs, List ys) { + List cpy = new List(xs); + cpy.AddRange(ys); + return cpy; + } + + public static Dictionary Dict(IEnumerable xs, IEnumerable ys) { + return Dict(Enumerable.Zip(xs, ys).Select(x => new Tuple(x.First, x.Second))); + } + + public static Dictionary Dict(IEnumerable> xys) { + Dictionary res = new Dictionary(); + foreach (var p in xys) { + res[p.Item1] = p.Item2; + } + return res; + } + + public static void AddToDict(Dictionary dict, List xs, List ys) { + Contract.Requires(dict != null); + Contract.Requires(xs != null); + Contract.Requires(ys != null); + Contract.Requires(xs.Count == ys.Count); + for (var i = 0; i < xs.Count; i++) { + dict.Add(xs[i], ys[i]); + } + } + + /// + /// Returns s but with all occurrences of '_' removed. + /// + public static string RemoveUnderscores(string s) { + Contract.Requires(s != null); + return s.Replace("_", ""); + } + + /// + /// For "S" returns S and false. + /// For @"S" return S and true. + /// Assumes that s has one of these forms. + /// + public static string RemoveParsedStringQuotes(string s, out bool isVerbatimString) { + Contract.Requires(s != null); + var len = s.Length; + if (s[0] == '@') { + isVerbatimString = true; + return s.Substring(2, len - 3); + } else { + isVerbatimString = false; + return s.Substring(1, len - 2); + } + } + + + + public static V GetOrDefault(this IReadOnlyDictionary dictionary, K key, Func createValue) + where V2 : V { + if (dictionary.TryGetValue(key, out var result)) { + return result; + } + + return createValue(); + } + + public static Action Concat(Action first, Action second) { + return v => { + first(v); + second(v); + }; + } + + public static V AddOrUpdate(this IDictionary dictionary, K key, V newValue, Func update) { + if (dictionary.TryGetValue(key, out var existingValue)) { + var updated = update(existingValue, newValue); + dictionary[key] = updated; + return updated; + } + + dictionary[key] = newValue; + return newValue; + } + + public static V GetOrCreate(this IDictionary dictionary, K key, Func createValue) { + if (dictionary.TryGetValue(key, out var result)) { + return result; + } + + result = createValue(); + dictionary[key] = result; + return result; + } + + } + + public class IEnumerableComparer : IEqualityComparer> { + public bool Equals(IEnumerable x, IEnumerable y) { + return x.SequenceEqual(y); + } + + public int GetHashCode(IEnumerable obj) { + var hash = new HashCode(); + foreach (T t in obj) { + hash.Add(t); + } + return hash.ToHashCode(); + } + } + +} diff --git a/Source/CompilerBuilder/Grammars/Comments.cs b/Source/CompilerBuilder/Grammars/Comments.cs new file mode 100644 index 00000000000..c9ed533749e --- /dev/null +++ b/Source/CompilerBuilder/Grammars/Comments.cs @@ -0,0 +1,58 @@ +// See https://aka.ms/new-console-template for more information + +namespace CompilerBuilder.Grammars; + +interface ITriviaContainer { + List Trivia { get; set; } +} + +public static class Comments { + + public static Grammar> JavaTrivia() { + return GrammarBuilder.Whitespace.Or(SlashSlashLineComment()).Or(BlockComment()).Many(debugString: "javaTrivia"); + } + + public static Grammar SlashSlashLineComment() { + return new ExplicitGrammar(ParserBuilder.SlashSlashLineComment, VerbatimW.Instance); + } + + public static Grammar BlockComment() { + return new ExplicitGrammar(ParserBuilder.BlockComment, VerbatimW.Instance); + } + + /* + * Identify all SequenceG. If both sides are non-empty, then insert trivia in between + * by replacing the left with another SequenceG that has trivia on its right, + * If the type of the left side can carry trivia, insert them there + */ + public static Grammar AddTrivia(Grammar root, Grammar> triviaGrammar) { + var grammars = root.SelfAndDescendants(); + var voidTrivia = new ParseOnly>(triviaGrammar); + foreach (var grammar in grammars) { + if (grammar is not ISequenceLikeG sequence) { + continue; + } + + if (sequence.FirstType == typeof(ITriviaContainer)) { + sequence.First = new SequenceG, ITriviaContainer>( + (Grammar)sequence.First, + triviaGrammar, + sequence.Mode, + (c, trivia) => { + c.Trivia = trivia.ToList(); + return c; + }, + c => (c, c.Trivia) + ); + } else { + if (sequence.FirstType == typeof(Unit)) { + sequence.Second = GrammarExtensions.Then(voidTrivia, (dynamic)sequence.Second, Separator.Nothing); + } else { + sequence.First = GrammarExtensions.Then((dynamic)sequence.First, voidTrivia, Separator.Nothing); + } + } + } + + return voidTrivia.Then(root).Then(voidTrivia); + } +} \ No newline at end of file diff --git a/Source/CompilerBuilder/Grammars/Grammar.cs b/Source/CompilerBuilder/Grammars/Grammar.cs new file mode 100644 index 00000000000..f86cdc33afe --- /dev/null +++ b/Source/CompilerBuilder/Grammars/Grammar.cs @@ -0,0 +1,528 @@ +// See https://aka.ms/new-console-template for more information + +using System.Linq.Expressions; +using CompilerBuilder.Generic; +using Microsoft.Boogie; +using Microsoft.Dafny; +using Util = Microsoft.Dafny.Util; + +namespace CompilerBuilder; + +public interface Grammar { + internal Parser ToGenParser(Func recurse); + internal Printer ToGenPrinter(Func recurse); + + public IEnumerable Children { get; } + public string? Name { get; set; } +} + +public abstract class VoidGrammar : Grammar { + public static implicit operator VoidGrammar(string keyword) => new TextG(keyword); + + public abstract VoidPrinter ToPrinter(Func recurse); + public abstract VoidParser ToParser(Func recurse); + public Parser ToGenParser(Func recurse) { + return ToParser(recurse); + } + + public Printer ToGenPrinter(Func recurse) { + return ToPrinter(recurse); + } + + public abstract IEnumerable Children { get; } + public string? Name { get; set; } +} + +class IndentG(Grammar inner, int amount) : Grammar { + + public override IEnumerable Children => inner.Children; + + internal override Printer ToPrinter(Func recurse) { + return new IndentW((Printer)recurse(inner), amount); + } + + internal override Parser ToParser(Func recurse) { + return inner.ToParser(recurse); + } +} + +public abstract class Grammar : Grammar +{ + public abstract IEnumerable Children { get; } + + public string? Name { get; set; } + + internal abstract Printer ToPrinter(Func recurse); + + public Parser ToParser() { + var map = new Dictionary(); + Func? recurse = null; + recurse = grammar => { + return Util.GetOrCreate(map, grammar, () => grammar.ToGenParser(recurse!)); + }; + return (Parser)recurse(this); + } + + public Printer ToPrinter() { + var map = new Dictionary(); + Func? recurse = null; + recurse = grammar => { + return Util.GetOrCreate(map, grammar, () => grammar.ToGenPrinter(recurse!)); + }; + return (Printer)recurse(this); + } + + internal abstract Parser ToParser(Func recurse); + + Parser Grammar.ToGenParser(Func recurse) { + return ToParser(recurse); + } + + Printer Grammar.ToGenPrinter(Func recurse) { + return ToPrinter(recurse); + } +} + +public class RecursiveG(Func> get, string debugName) : Grammar { + private Grammar? inner; + + public Grammar Inner => inner ??= get(); + + internal override Printer ToPrinter(Func recurse) { + return new RecursiveW(() => (Printer)recurse(Inner)); + } + + internal override Parser ToParser(Func recurse) { + return new RecursiveR(() => (Parser)recurse(Inner), debugName); + } + + public override IEnumerable Children => [Inner]; +} + +class TextG(string value) : VoidGrammar { + public string Value => value; + + public override VoidPrinter ToPrinter(Func recurse) { + return new TextW(value); + } + + public override VoidParser ToParser(Func recurse) { + return new TextR(value); + } + + public override IEnumerable Children => []; + + public override string ToString() { + return Value; + } +} + +internal class NumberG : Grammar { + internal override Printer ToPrinter(Func recurse) { + return new NumberW(); + } + + internal override Parser ToParser(Func recurse) { + return new NumberR(); + } + + public override IEnumerable Children => []; +} + +internal class IdentifierG : Grammar { + internal override Printer ToPrinter(Func recurse) { + return VerbatimW.Instance; + } + + internal override Parser ToParser(Func recurse) { + return new IdentifierR(); + } + + public override IEnumerable Children => []; +} + +class WithRangeG(Grammar grammar, Func> construct, Func> destruct) : Grammar { + + public Grammar Grammar { get; set; } = grammar; + + internal override Printer ToPrinter(Func recurse) { + return ((Printer)recurse(Grammar)).Map(destruct); + } + + internal override Parser ToParser(Func recurse) { + return new WithRangeR((Parser)recurse(Grammar), construct); + } + + public override IEnumerable Children => [Grammar]; +} + +class Choice(Grammar first, Grammar second) : Grammar { + public Grammar First { get; set; } = first; + public Grammar Second { get; set; } = second; + + internal override Printer ToPrinter(Func recurse) { + return new ChoiceW((Printer)recurse(First), (Printer)recurse(Second)); + // Reverse order, on purpose. Needs testing. + // return new ChoiceW((Printer)recurse(Second), (Printer)recurse(First)); + } + + internal override Parser ToParser(Func recurse) { + return new ChoiceR((Parser)recurse(First), (Parser)recurse(Second)); + } + + public override IEnumerable Children => [First, Second]; +} + +class Constructor(Func construct) : Grammar { + + internal override Printer ToPrinter(Func recurse) { + // TODO this is wrong. It'll succeed too easily. + return new IgnoreW(EmptyW.Instance); + } + + internal override Parser ToParser(Func recurse) { + return new ValueR(construct); + } + + public override IEnumerable Children => []; +} + +class ValueG(T value, Func? isExpected = null) : Grammar { + public T Value => value; + + internal override Printer ToPrinter(Func recurse) { + return new ValueW(isExpected ?? (t => Equals(value, t)), EmptyW.Instance); + } + + internal override Parser ToParser(Func recurse) { + return new ValueR(() => value); + } + + public override IEnumerable Children => []; +} + +class ParseOnly(Grammar grammar) : VoidGrammar { + public override VoidPrinter ToPrinter(Func recurse) { + return EmptyW.Instance; + } + + public override VoidParser ToParser(Func recurse) { + return new IgnoreR(grammar.ToParser(recurse)); + } + + public override IEnumerable Children => grammar.Children; +} + +public static class GrammarExtensions { + + + public static IEnumerable SelfAndDescendants(this Grammar grammar) { + var visited = new HashSet(); + var toVisit = new Stack(); + var result = new List(); + toVisit.Push(grammar); + while (toVisit.Any()) { + var current = toVisit.Pop(); + if (!visited.Add(current)) { + continue; + } + + result.Add(current); + foreach (var child in current.Children.Reverse()) { + toVisit.Push(child); + } + } + return result; + } + + public static Grammar Default(this Grammar grammar, T value) { + return grammar.Or(GrammarBuilder.Constant(value)); + } + + public static Grammar Named(this Grammar grammar, string name) { + grammar.Name = name; + return grammar; + } + + public static Grammar OrCast(this Grammar grammar, Grammar other, string? otherName = null) + where U : class, T { + if (otherName != null) { + other.Name = otherName; + } + return new Choice(grammar, other.UpCast()); + } + + public static Grammar Or(this Grammar grammar, Grammar other) + { + return new Choice(grammar, other); + } + + public static VoidGrammar InParens(this VoidGrammar grammar) { + return GrammarBuilder.Keyword("(").Then(grammar, Separator.Nothing).Then(")", Separator.Nothing); + } + + public static Grammar InParens(this Grammar grammar) { + return GrammarBuilder.Keyword("(").Then(grammar, Separator.Nothing).Then(")", Separator.Nothing); + } + + public static Grammar InBraces(this Grammar grammar, bool indent = true) { + var inner = indent ? new IndentG(grammar, 1) : grammar; + return GrammarBuilder.Keyword("{").Then(inner, Separator.Linebreak).Then("}", Separator.Linebreak); + } + + public static Grammar Then(this Grammar left, VoidGrammar right, Separator separator = Separator.Space) { + return new SkipRightG(left, right, separator); + } + + public static VoidGrammar Then(this VoidGrammar left, VoidGrammar right, Separator separator = Separator.Space) { + return new NeitherG(left, right, separator); + } + + public static Grammar Then(this VoidGrammar left, Grammar right, Separator separator = Separator.Space) { + return new SkipLeftG(left, right, separator); + } + + public static Grammar> CommaSeparated(this Grammar inner) { + return inner.Separated(",", Separator.Nothing); + } + + public static Grammar> Separated(this Grammar inner, VoidGrammar separator, + Separator beforeSep = Separator.Space, + Separator afterSep = Separator.Space) { + var some = inner.Then, SinglyLinkedList>( + ManyLinkedList(separator.Then(inner, afterSep), beforeSep, "separated"), + (e, l) => new Cons(e, l), + l => l.Fold((head, tail) => (head, tail), () => ((T, SinglyLinkedList)?)null), beforeSep); + var someOrNone = some.Or(new ValueG>(new Nil(), ll => ll.Any())); + return someOrNone.Map(e => e.ToList(), l => new LinkedListFromList(l)); + } + + public static Grammar> Many(this Grammar one, Separator separator = Separator.Space, string debugString = "many") { + var numerable = ManyLinkedList(one, separator, debugString); + return numerable.Map(e => e.ToList(), l => new LinkedListFromList(l)); + } + + private static Grammar> ManyLinkedList(Grammar one, Separator separator, string debugString) + { + return GrammarBuilder.Recursive>(self => { + var nil = new ValueG>(new Nil(), ll => !ll.Any()); + var cons = one.Then(self, + (head, tail) => (SinglyLinkedList)new Cons(head, tail), + l => l.Fold( + (head, tail) => (head, tail), + () => ((T, SinglyLinkedList)?)null), separator); + return cons.Or(nil); + }, debugString); + } + + public static Grammar Where(this Grammar grammar, Func filter) { + return new WithRangeG(grammar, (_, v) => filter(v) ? new MapSuccess(v) : new MapFail(), + x => new MapSuccess(x)); + } + + public static Grammar Map(this Grammar grammar, Func construct, + Func destruct) { + return new WithRangeG(grammar, (r,v) => new MapSuccess(construct(r,v)), + v => new MapSuccess(destruct(v))); + } + + public static Grammar Map(this Grammar grammar, Func construct, + Func> destruct) { + return new WithRangeG(grammar, (r,v) => new MapSuccess(construct(r,v)), + destruct); + } + + public static Grammar DownCast(this Grammar grammar) + where TSub : class, TSuper { + // TODO fix t as TSub + return grammar.Map(t => t as TSub, u => u); + } + + public static Grammar UpCast(this Grammar grammar) + where TSub : TSuper + { + return grammar.Map(t => t, + u => u is TSub s ? new MapSuccess(s) : new MapFail($"{u} is not a {typeof(TSub)}")); + } + + public static Grammar Map(this Grammar grammar, Func construct, Func destruct) + { + return new WithRangeG(grammar, (_, original) => new MapSuccess(construct(original)), v => { + var d = destruct(v); + return d == null ? new MapFail() : new MapSuccess(d); + }); + } + + public static Grammar Map(this Grammar grammar, Func construct, Func> destruct) { + return new WithRangeG(grammar, (_, original) => new MapSuccess(construct(original)), destruct); + } + + public static Grammar> Singleton(this Grammar grammar) where T : notnull { + return grammar.Map(o => new List() { o }, + l => l.FirstOrDefault()); + } + + public static Grammar> OptionToList(this Grammar grammar) { + return grammar.Map(o => o == null ? [] : new List { o }, + l => new MapSuccess(l.FirstOrDefault())); + } + + public static Grammar Then( + this Grammar left, + Grammar right, + Func construct, + Func destruct, + Separator mode) { + return new SequenceG(left, right, mode, construct, destruct); + } + + public static Grammar Then( + this Grammar containerGrammar, + Grammar value, + Func get, + Action set, + Separator mode = Separator.Space) { + return new SequenceG(containerGrammar, value, mode, + (c, v) => { + set(c, v); + return c; + }, c => (c, get(c))); + } + + public static Grammar Then( + this Grammar containerGrammar, + Grammar value, + Expression> get, Separator mode = Separator.Space) { + var property = get.GetProperty(); + return containerGrammar.Then(value, property.Get, property.Set, mode); + } + + public static Grammar Assign( + this Grammar value, + Expression> getExpression, Separator mode = Separator.Space) + where TContainer : new() { + var property = getExpression.GetProperty(); + return value.Map(v => { + var container = new TContainer(); + property.Set(container, v); + return container; + }, container => property.Get(container)); + } + + public static Grammar Assign( + this Grammar value, + Func createContainer, + Expression> getExpression, Separator mode = Separator.Space) { + var property = getExpression.GetProperty(); + return value.Map(v => { + var container = createContainer(); + property.Set(container, v); + return container; + }, container => property.Get(container)); + } + + public static Grammar Indent(this Grammar grammar, int amount = 1) { + return new IndentG(grammar, amount); + } + + public static Grammar SetRange(this Grammar grammar, Action set, string? name = null) { + var result = grammar.Map((t, v) => { + set(v, t); + return v; + }, x => x); + result.Name = name; + return result; + } + + public static Grammar Option(this Grammar grammar) { + return grammar.Map(t => t, t => t).Or(new Constructor(() => default)); + } + + public static Grammar Option(this Grammar grammar, VoidGrammar fallback) { + var r = fallback.Then(GrammarBuilder.Constant(default)); + return grammar.Map(t => t, t => t).Or(r); + } + + public static VoidGrammar Ignore(this Grammar grammar) { + return new ParseOnly(grammar); + } +} + +public interface MapResult { + public static MapResult FromNullable(T? nullable) { + if (nullable == null) { + return new MapFail(); + } + return new MapSuccess(nullable); + } +} + +public record MapSuccess(T Value) : MapResult; +public record MapFail(string Message = null) : MapResult; + +class Fail(string expectation) : Grammar { + internal override Printer ToPrinter(Func recurse) { + return new FailW(expectation); + } + + internal override Parser ToParser(Func recurse) { + return new FailR(expectation); + } + + public override IEnumerable Children => []; +} + +class ExplicitGrammar(Parser parser, Printer printer) : Grammar { + internal override Printer ToPrinter(Func recurse) { + return printer; + } + + internal override Parser ToParser(Func recurse) { + return parser; + } + + public override IEnumerable Children => []; +} + +public static class GrammarBuilder { + + + public static Grammar Recursive(Func, Grammar> build, string debugName) { + RecursiveG? result = null; + // ReSharper disable once AccessToModifiedClosure + result = new RecursiveG(() => build(result!), debugName); + var resolved = result.Inner; + return result; + } + + public static Grammar Constructor() where T : new() => new Constructor(() => new T()); + public static Grammar Constant(T value) => new ValueG(value); + public static VoidGrammar Keyword(string keyword) => new TextG(keyword); + public static Grammar Modifier(string keyword) => new TextG(keyword).Then(Constant(true)).Or(Constant(false)); + + public static Grammar Fail(string expectation) => new Fail(expectation); + public static readonly VoidGrammar Empty = new EmptyG(); + public static readonly Grammar Identifier = new IdentifierG(); + public static readonly Grammar Number = new NumberG(); + public static readonly Grammar CharInSingleQuotes = new ExplicitGrammar(ParserBuilder.CharInSingleQuotes, + VerbatimW.Instance.Map(s => $"'{s}'")); + public static readonly Grammar StringInDoubleQuotes = new ExplicitGrammar(ParserBuilder.StringInDoubleQuotes, + VerbatimW.Instance.Map(s => $"\"{s}\"")); + + public static readonly Grammar Whitespace = new ExplicitGrammar(ParserBuilder.Whitespace, VerbatimW.Instance); + + public static readonly Grammar Position = + new ExplicitGrammar(PositionR.Instance, new IgnoreW(EmptyW.Instance)); +} + +public class EmptyG : VoidGrammar { + public override VoidPrinter ToPrinter(Func recurse) { + return EmptyW.Instance; + } + + public override VoidParser ToParser(Func recurse) { + return EmptyR.Instance; + } + + public override IEnumerable Children => []; +} diff --git a/Source/CompilerBuilder/Grammars/GrammarReflection.cs b/Source/CompilerBuilder/Grammars/GrammarReflection.cs new file mode 100644 index 00000000000..0a31c6cbd3a --- /dev/null +++ b/Source/CompilerBuilder/Grammars/GrammarReflection.cs @@ -0,0 +1,24 @@ +namespace CompilerBuilder; + +interface GrammarPath { + Grammar Current { get; } + GrammarPath? Parent { get; } + + IEnumerable SelfAndDescendants { get; } +} + +class GrammarPathRoot(Grammar root) : GrammarPath { + public Grammar Current => root; + public GrammarPath? Parent => null; + public IEnumerable SelfAndDescendants => [this]; +} + +class GrammarPathChild(GrammarPath parent, Property property) : GrammarPath { + private Grammar? current; + public Grammar Current => current ??= property.Get(parent.Current); + + public GrammarPath? Parent => parent; + public IEnumerable SelfAndDescendants => throw new NotImplementedException(); +} + +public record Property(Func Get, Action Set); \ No newline at end of file diff --git a/Source/CompilerBuilder/Grammars/ISequenceLikeG.cs b/Source/CompilerBuilder/Grammars/ISequenceLikeG.cs new file mode 100644 index 00000000000..78a5af17f12 --- /dev/null +++ b/Source/CompilerBuilder/Grammars/ISequenceLikeG.cs @@ -0,0 +1,141 @@ +namespace CompilerBuilder; + +interface ISequenceLikeG { + Type FirstType { get; } + Type SecondType { get; } + Type Type { get; } + public Grammar First { get; set; } + public Grammar Second { get; set; } + public Separator Mode { get; set; } +} + +class SequenceG(Grammar first, Grammar second, Separator mode, + Func construct, Func destruct) : Grammar, ISequenceLikeG { + public Type FirstType => typeof(TFirst); + public Type SecondType => typeof(TSecond); + public Type Type => typeof(T); + + Grammar ISequenceLikeG.First { + get => First; + set => First = (Grammar)value; + } + + Grammar ISequenceLikeG.Second { + get => Second; + set => Second = (Grammar)value; + } + + Separator ISequenceLikeG.Mode { get; set; } + public Grammar First { get; set; } = first; + public Grammar Second { get; set; } = second; + + public Separator Mode => mode; + + internal override Printer ToPrinter(Func recurse) { + var firstPrinter = (Printer)recurse(First); + var secondPrinter = (Printer)recurse(Second); + return new SequenceW(firstPrinter, secondPrinter, destruct, mode); + } + + internal override Parser ToParser(Func recurse) { + var leftParser = (Parser)recurse(First); + var rightParser = (Parser)recurse(Second); + return new SequenceR(leftParser, rightParser, construct); + } + + public override IEnumerable Children => [First, Second]; +} + +class SkipLeftG(VoidGrammar first, Grammar second, Separator mode = Separator.Space) : Grammar, ISequenceLikeG { + public Type FirstType => typeof(Unit); + public Type SecondType => typeof(T); + public Type Type => typeof(T); + Grammar ISequenceLikeG.First { + get => First; + set => First = (VoidGrammar)value; + } + + Grammar ISequenceLikeG.Second { + get => Second; + set => Second = (Grammar)value; + } + + public Separator Mode { get; set; } + public VoidGrammar First { get; set; } = first; + public Grammar Second { get; set; } = second; + + internal override Printer ToPrinter(Func recurse) { + var first = (VoidPrinter)recurse(First); + var second = (Printer)recurse(Second); + return new SkipLeftW(first, second, mode); + } + + internal override Parser ToParser(Func recurse) { + return new SkipLeft((VoidParser)recurse(First), (Parser)recurse(Second)); + } + + public override IEnumerable Children => [First, Second]; +} + +class NeitherG(VoidGrammar first, VoidGrammar second, Separator separator = Separator.Space) : VoidGrammar, ISequenceLikeG { + public Type FirstType => typeof(Unit); + public Type SecondType => typeof(Unit); + public Type Type => typeof(Unit); + Grammar ISequenceLikeG.First { + get => First; + set => First = (VoidGrammar)value; + } + + Grammar ISequenceLikeG.Second { + get => Second; + set => Second = (VoidGrammar)value; + } + + public Separator Mode { get; set; } + public VoidGrammar First { get; set; } = first; + public VoidGrammar Second { get; set; } = second; + + public override VoidPrinter ToPrinter(Func recurse) { + var first = (VoidPrinter)recurse(First); + var second = (VoidPrinter)recurse(Second); + return new NeitherW(first, second, separator); + } + + public override VoidParser ToParser(Func recurse) { + return new NeitherR((VoidParser)recurse(First), (VoidParser)recurse(Second)); + } + + public override IEnumerable Children => [First, Second]; +} + +class SkipRightG(Grammar first, VoidGrammar second, Separator mode = Separator.Space) : Grammar, ISequenceLikeG { + public Type FirstType => typeof(T); + public Type SecondType => typeof(Unit); + public Type Type => typeof(T); + + Grammar ISequenceLikeG.First { + get => First; + set => First = (Grammar)value; + } + + Grammar ISequenceLikeG.Second { + get => Second; + set => Second = (VoidGrammar)value; + } + + public Separator Mode { get; set; } + public Grammar First { get; set; } = first; + public VoidGrammar Second { get; set; } = second; + + internal override Printer ToPrinter(Func recurse) { + var firstParser = (Printer)recurse(First); + var secondParser = (VoidPrinter)recurse(Second); + return new SkipRightW(firstParser, secondParser, mode); + } + + internal override Parser ToParser(Func recurse) { + return new SkipRight((Parser)recurse(First), (VoidParser)recurse(Second)); + } + + public override IEnumerable Children => [First, Second]; +} \ No newline at end of file diff --git a/Source/CompilerBuilder/Parsers/ITextPointer.cs b/Source/CompilerBuilder/Parsers/ITextPointer.cs new file mode 100644 index 00000000000..eddf38231d6 --- /dev/null +++ b/Source/CompilerBuilder/Parsers/ITextPointer.cs @@ -0,0 +1,33 @@ +namespace CompilerBuilder; + +public interface IPosition { + int Offset { get; } + int Line { get; } + int Column { get; } +} + +public record ParseRange(IPosition From, IPosition Until); + +public interface ITextPointer : IPosition { + + ITextPointer Drop(int amount); + + string LocationDescription => Length == 0 ? "end of text" : SubSequence(5).ToString(); + + char First { get; } + int Length { get; } + char At(int offset); + + ReadOnlySpan Remainder { get; } + ReadOnlySpan SubSequence(int length); + + FailureResult Fail(string expected) { + return new FailureResult($"'{LocationDescription}' is not {expected}", this); + } + + ParseResult ParseWithCache(VoidParser parser, string reason); + ParseResult ParseWithCache(Parser parser, string reason); + + void Ref(); + void UnRef(); +} \ No newline at end of file diff --git a/Source/CompilerBuilder/Parsers/ParseResult.cs b/Source/CompilerBuilder/Parsers/ParseResult.cs new file mode 100644 index 00000000000..8328af5440c --- /dev/null +++ b/Source/CompilerBuilder/Parsers/ParseResult.cs @@ -0,0 +1,142 @@ +namespace CompilerBuilder; + +public interface ParseResult; + +public interface ParseResult : ParseResult { + internal ParseResult Continue(Func, ParseResult> f); + + internal ConcreteResult? Concrete => Success as ConcreteResult ?? Failure; + + public ConcreteSuccess? Success { get; } + public ConcreteSuccess ForceSuccess { + get { + if (Success != null) { + return Success; + } + + throw new InvalidOperationException(Failure!.Message + $", at ({Failure.Location.Line},{Failure.Location.Column})"); + } + } + + public FailureResult? Failure { get; } + + internal IFoundRecursion? FoundRecursion { get; } + + R? Combine(R? left, R? right, Func combine) { + if (left == null) { + return right; + } + + if (right == null) { + return left; + } + + return combine(left, right); + } + internal ParseResult Combine(ParseResult other) { + var recursion = Combine(FoundRecursion, other.FoundRecursion, (l, r) => { + dynamic ld = l; + dynamic rd = r; + return ld.Combine(rd); + }); + + var concreteSuccess = Combine(Success, other.Success, (l,r) => + l.Remainder.Offset >= r.Remainder.Offset ? l : r); + + var failure = Combine(Failure, other.Failure, (l,r) => + l.Location.Offset >= r.Location.Offset ? l : r); + + if (concreteSuccess != null && failure != null && failure.Location.Offset <= concreteSuccess.Remainder.Offset) { + // TODO consider keeping the failure if it's at the same offset, because it might have been how you wanted to continue + failure = null; + } + + return new Aggregate(concreteSuccess, failure, recursion); + } +} + +public interface ConcreteResult : ParseResult; + +internal record Aggregate(ConcreteSuccess? Success, FailureResult? Failure, IFoundRecursion? FoundRecursion) : ParseResult { + public ParseResult Continue(Func, ParseResult> f) {; + var newFailure = Failure == null ? null : new FailureResult(Failure.Message, Failure.Location); + var newRecursion = (IFoundRecursion?)FoundRecursion?.Continue(f); + var noConcrete = new Aggregate(null, newFailure, newRecursion); + if (Success != null) { + var concreteResult = Success.Continue(f); + return concreteResult.Combine(noConcrete); + } + + return noConcrete; + } +} + +public record ConcreteSuccess(T Value, ITextPointer Remainder) : ConcreteResult { + public ParseResult Continue(Func, ParseResult> f) { + var result = f(this); + return result; + } + + public ConcreteSuccess? Success => this; + public FailureResult? Failure => null; + IFoundRecursion? ParseResult.FoundRecursion => null; +} + +interface IFoundRecursion : ParseResult { +} + +/// +/// Parsers that do not have recursive children have the same result regardless of whether they're a recursion on the stack. +/// A parser that has a recursive child, will have a different result if that child is already on its stack. +/// +/// TODO do a little analysis to see how often a particular parser is in a cache with different seens +/// +/// +record FoundRecursion(Func, ParseResult> Recursion) : IFoundRecursion { + public ParseResult Continue(Func, ParseResult> f) { + return new FoundRecursion(concrete => { + var inner = Recursion(concrete); + var continued = inner.Continue(f); + return continued; + }); + } + + public ConcreteSuccess? Success => null; + public FailureResult? Failure => null; + IFoundRecursion? ParseResult.FoundRecursion => this; + public IEnumerable> Recursions => new IFoundRecursion[]{ this }; + + public ParseResult Apply(TA value, ITextPointer remainder) { + return Recursion(new ConcreteSuccess(value, remainder)); + } + public ParseResult Combine(FoundRecursion other) { + return new FoundRecursion(s => Apply(s.Value, s.Remainder).Combine( + other.Apply(s.Value, s.Remainder))); + } +} + +public record FailureResult : ConcreteResult { + public FailureResult(string Message, ITextPointer Location) { + this.Message = Message; + this.Location = Location; + } + + public FailureResult Cast() { + return new FailureResult(Message, Location); + } + + public ParseResult Continue(Func, ParseResult> f) { + return new FailureResult(Message, Location); + } + + public ConcreteSuccess? Success => null; + public FailureResult Failure => this; + IFoundRecursion? ParseResult.FoundRecursion => null; + public string Message { get; init; } + public ITextPointer Location { get; init; } + + public void Deconstruct(out string Message, out ITextPointer Location) { + Message = this.Message; + Location = this.Location; + } +} \ No newline at end of file diff --git a/Source/CompilerBuilder/Parsers/Parser.cs b/Source/CompilerBuilder/Parsers/Parser.cs new file mode 100644 index 00000000000..3f68217dcd1 --- /dev/null +++ b/Source/CompilerBuilder/Parsers/Parser.cs @@ -0,0 +1,328 @@ +using System.Diagnostics; +using System.Text.RegularExpressions; + +namespace CompilerBuilder; + +public record Unit { + public static readonly Unit Instance = new(); + + private Unit() { } +} +public abstract class VoidParser : Parser { + public static implicit operator VoidParser(string keyword) => new TextR(keyword); + + internal abstract ParseResult Parse(ITextPointer text); +} + +class NeitherR(VoidParser left, VoidParser right) : VoidParser { + internal override ParseResult Parse(ITextPointer text) { + return text.ParseWithCache(left, "neitherLeft"). + Continue(r => r.Remainder.ParseWithCache(right, "neitherRight")); + } +} + +class EmptyR : VoidParser { + public static readonly EmptyR Instance = new(); + + private EmptyR() { } + + internal override ParseResult Parse(ITextPointer text) { + return new ConcreteSuccess(Unit.Instance, text); + } +} + +class IgnoreR(Parser parser) : VoidParser { + public Parser Parser => parser; + + internal override ParseResult Parse(ITextPointer text) { + return text.ParseWithCache(parser, "ignoreInner").Continue( + s => new ConcreteSuccess(Unit.Instance, s.Remainder)); + } +} + +public abstract class Parser +{ + public override string ToString() { + return "Parser"; + } +} + +public abstract class Parser : Parser +{ + public abstract ParseResult Parse(ITextPointer text); + + public ConcreteResult Parse(string text) { + ITextPointer pointer = new PointerFromString(text); + var withEnd = new EndOfText(this); + return withEnd.Parse(pointer).Concrete!; + } +} + +class EndOfText(Parser inner) : Parser { + public override ParseResult Parse(ITextPointer text) { + var innerResult = inner.Parse(text); + if (innerResult.Success == null) { + return innerResult; + } + + var end = innerResult.Success.Remainder; + if (end.Length <= 0) { + return innerResult.Success; + } + + var endFail = end.Fail("the end of the text"); + if (innerResult.Failure != null) { + return innerResult.Failure.Location.Offset > innerResult.Success.Remainder.Offset + ? innerResult.Failure + : end.Fail("the end of the text"); + } + + return endFail; + } +} + +public class SequenceR(Parser first, Parser second, Func combine) : Parser { + + public Parser First { get; set; } = first; + public Parser Second { get; set; } = second; + + public override ParseResult Parse(ITextPointer text) { + var leftResult = text.ParseWithCache(First, "sequenceLeft"); + return leftResult.Continue(leftConcrete => { + var rightResult = leftConcrete.Remainder.ParseWithCache(Second, "sequenceRight"); + return rightResult.Continue(rightConcrete => { + var value = combine(leftConcrete.Value, rightConcrete.Value); + return new ConcreteSuccess(value, rightConcrete.Remainder); + }); + }); + } +} + +/// +/// Prefer the first over the second choice, also when it comes to error messages +/// +class ChoiceR(Parser first, Parser second): Parser { + + public Parser First { get; set; } = first; + public Parser Second { get; set; } = second; + + public override ParseResult Parse(ITextPointer text) { + text.Ref(); + var firstResult = First.Parse(text); + text.UnRef(); + var secondResult = Second.Parse(text); + return firstResult.Combine(secondResult); + } +} + +class FailR(string expectation) : Parser { + public override ParseResult Parse(ITextPointer text) { + return text.Fail(expectation); + } +} + +class PositionR : Parser { + public static readonly PositionR Instance = new(); + + private PositionR() + { + } + + public override ParseResult Parse(ITextPointer text) { + return new ConcreteSuccess(text, text); + } +} + +class WithRangeR(Parser parser, Func> map) : Parser { + + public Parser Parser { get; set; } = parser; + + public override ParseResult Parse(ITextPointer text) { + var start = text; + var innerResult = text.ParseWithCache(Parser, "withRange"); + return innerResult.Continue(success => { + var end = success.Remainder; + var newValue = map(new ParseRange(start, end), success.Value); + if (newValue is MapSuccess s) { + return new ConcreteSuccess(s.Value, success.Remainder); + } + return new FailureResult("Mapping failure", end); + }); + } +} + +class SkipLeft(VoidParser first, Parser second) : Parser { + + public VoidParser First { get; set; } = first; + public Parser Second { get; set; } = second; + + public override ParseResult Parse(ITextPointer text) { + var leftResult = text.ParseWithCache(First, "skipLeftLeft"); + return leftResult.Continue(leftConcrete => leftConcrete.Remainder.ParseWithCache(Second, "skipLeftRight")); + } +} + +class SkipRight(Parser first, VoidParser second) : Parser { + + public Parser First { get; set; } = first; + public VoidParser Second { get; set; } = second; + + public override ParseResult Parse(ITextPointer text) { + var leftResult = text.ParseWithCache(First, "skipRightLeft"); + return leftResult.Continue(leftConcrete => leftConcrete.Remainder.ParseWithCache(Second, "skipRightRight"). + Continue(rightSuccess => leftConcrete with { Remainder = rightSuccess.Remainder })); + } +} + +class TextR(string value) : VoidParser { + public string Value => value; + + public override string ToString() { + return Value; + } + + internal override ParseResult Parse(ITextPointer text) { + var actual = text.SubSequence(value.Length).ToString(); + if (actual.Equals(value)) { + return new ConcreteSuccess(Unit.Instance, text.Drop(value.Length)); + } + + return new FailureResult($"Expected '{value}' but found '{text.LocationDescription}'", text); + } +} + +class RegexR(string regex, string description) : Parser { + private Regex r = new("^" + regex); + public override ParseResult Parse(ITextPointer text) { + var matches = r.EnumerateMatches(text.Remainder); + while (matches.MoveNext()) { + var match = matches.Current; + Debug.Assert(match.Index == 0); + var remainder = text.Drop(match.Length); + return new ConcreteSuccess(text.SubSequence(match.Length).ToString(), remainder); + } + + return text.Fail(description); + } +} + +internal class Whitespace : Parser { + public override ParseResult Parse(ITextPointer text) { + var offset = 0; + while (text.Length > offset) { + var c = text.At(offset); + if (Char.IsWhiteSpace(c)) { + offset++; + } else { + break; + } + } + + if (offset > 0) { + var result = text.SubSequence(offset); + return new ConcreteSuccess(result.ToString(), text.Drop(offset)); + } + + return text.Fail("whitespace"); + } +} + +internal class Comment(string opener, string closer, string description) : Parser { + bool Find(string expectation, ITextPointer text, int offset = 0) { + if (text.Length < expectation.Length) { + return false; + } + + for (int index = 0; index < expectation.Length; index++) { + if (text.At(offset + index) != expectation[index]) { + return false; + } + } + + return true; + } + + public override ParseResult Parse(ITextPointer text) { + if (!Find(opener, text)) { + return text.Fail(description); + } + + bool foundExit = false; + int offset = opener.Length; + while (text.Length > offset) { + if (Find(closer, text, offset)) { + foundExit = true; + offset += closer.Length; + break; + } + + offset++; + } + + if (foundExit) { + var comment = text.SubSequence(offset); + return new ConcreteSuccess(comment.ToString(), text.Drop(offset)); + } + + return text.Fail(description); + } +} + +internal class NumberR : Parser { + public override ParseResult Parse(ITextPointer text) { + var offset = 0; + while (text.Length > offset) { + var c = text.At(offset); + if (Char.IsDigit(c)) { + offset++; + } else { + break; + } + } + + if (offset > 0) { + var sequence = text.SubSequence(offset); + if (int.TryParse(sequence, out var parsed)) + { + return new ConcreteSuccess(parsed, text.Drop(offset)); + } + return new FailureResult($"'{sequence}' is not a number", text); + } + + return text.Fail("a digit"); + } +} + +internal class IdentifierR : Parser { + public override ParseResult Parse(ITextPointer text) { + var offset = 0; + var allowOthers = false; + while (text.Length > offset) { + var c = text.At(offset); + if (Char.IsLetter(c)) { + allowOthers = true; + offset++; + } + else if (allowOthers && (char.IsDigit(c) || c == '\'') || c == '_') { + offset++; + } else { + break; + } + } + + if (offset > 0) { + var sequence = text.SubSequence(offset).ToString(); + return new ConcreteSuccess(sequence, text.Drop(offset)); + } + + return text.Fail("an identifier"); + } +} + +class ValueR(Func value) : Parser { + public T Evaluated => value(); + + public override ParseResult Parse(ITextPointer text) { + return new ConcreteSuccess(value(), text); + } +} \ No newline at end of file diff --git a/Source/CompilerBuilder/Parsers/ParserBuilder.cs b/Source/CompilerBuilder/Parsers/ParserBuilder.cs new file mode 100644 index 00000000000..1a39da20342 --- /dev/null +++ b/Source/CompilerBuilder/Parsers/ParserBuilder.cs @@ -0,0 +1,32 @@ +using System.Text.RegularExpressions; + +namespace CompilerBuilder; + +public static class ParserBuilder { + + public static Parser Recursive(Func, Parser> build, string debugName) { + Parser? result = null; + // ReSharper disable once AccessToModifiedClosure + result = new RecursiveR(() => build(result!), debugName); + return result; + + } + + public static Parser Value(Func value) => new ValueR(value); + + // TODO should this exist? Could be dangerous + public static Parser Constant(T value) => new ValueR(() => value); + public static VoidParser Keyword(string keyword) => new TextR(keyword); + public static readonly Parser Identifier = new RegexR(@"[a-zA-Z]\w*", "an identifier"); + public static readonly Parser Number = new RegexR(@"\d+", "number").MapValue(s => + int.TryParse(s, out var result) ? result : default(int?)); + public static readonly Parser CharInSingleQuotes = new RegexR(@"'.'", "char"). + Map(s => s.Substring(1, s.Length - 2)); + public static readonly Parser StringInDoubleQuotes = + new RegexR("\".+\"", "string").Map(s => s.Substring(1, s.Length - 2)); + + public static Parser Fail(string expectation) => new FailR(expectation); + public static readonly Parser SlashSlashLineComment = new Comment("//", "\n", "a line comment"); + public static readonly Parser BlockComment = new Comment("/**", "*/", "a block comment"); + public static readonly Parser Whitespace = new Whitespace(); +} \ No newline at end of file diff --git a/Source/CompilerBuilder/Parsers/ParserExtensions.cs b/Source/CompilerBuilder/Parsers/ParserExtensions.cs new file mode 100644 index 00000000000..3a0e24d5f83 --- /dev/null +++ b/Source/CompilerBuilder/Parsers/ParserExtensions.cs @@ -0,0 +1,65 @@ +using Microsoft.Dafny; + +namespace CompilerBuilder; + +public static class ParserExtensions { + public static Parser InBraces(this Parser parser) { + return ParserBuilder.Keyword("{").Then(parser).Then("}"); + } + + public static Parser Then(this Parser left, VoidParser right) { + return new SkipRight(left, right); + } + + public static Parser Then(this VoidParser left, Parser right) { + return new SkipLeft(left, right); + } + + public static Parser Or(this Parser left, Parser right) { + return new ChoiceR(left, right); + } + + public static Parser OrCast(this Parser grammar, Parser other) + where U : T + { + return new ChoiceR(grammar, other.UpCast()); + } + + public static Parser UpCast(this Parser grammar) + where TSub : TSuper + { + return grammar.Map(t => t); + } + + public static Parser> Many(this Parser one) { + return ParserBuilder.Recursive>(self => + ParserBuilder.Value(() => new List()).Or(self.Then(one, (l, e) => l.Add(e))), "many"); + } + + public static Parser Map(this Parser parser, Func map) { + return new WithRangeR(parser, (a,b) => new MapSuccess(map(a,b))); + } + + public static Parser Map(this Parser parser, Func map) { + return new WithRangeR(parser, (_, original) => new MapSuccess(map(original))); + } + + public static Parser MapValue(this Parser parser, Func map) + where U : struct + { + return new WithRangeR(parser, (_, original) => { + var result = map(original); + return result.HasValue ? new MapSuccess(result.Value) : new MapFail(); + }); + } + + public static Parser Then( + this Parser containerParser, + Parser value, + Action set) { + return new SequenceR(containerParser, value, (c, v) => { + set(c, v); + return c; + }); + } +} \ No newline at end of file diff --git a/Source/CompilerBuilder/Parsers/PointerFromString.cs b/Source/CompilerBuilder/Parsers/PointerFromString.cs new file mode 100644 index 00000000000..5801eea43b9 --- /dev/null +++ b/Source/CompilerBuilder/Parsers/PointerFromString.cs @@ -0,0 +1,138 @@ +using System.Collections.Immutable; + +namespace CompilerBuilder; + +/* + * TODO + * it might be a cool idea to use PointerFromString to determine which parts of the cache to keep + * However, when you call Drop, you do not know if the old pointer is still used. + * We make have to introduce .Ref() and .DropAndUnref() methods + * That enable the cache to know when a text pointer is disposed + * Or maybe we can use the C# dispose mechanic + */ +public class PointerFromString : ITextPointer { + + public PointerFromString(string text) { + Text = text; + seen = ImmutableHashSet.Empty; + cache = new(); + pointerCache = new(); + } + + public PointerFromString(string text, int offset, int line, int column, + Dictionary pointerCache, + Dictionary cache, + ImmutableHashSet seen) { + Offset = offset; + Line = line; + Column = column; + this.seen = seen; + Text = text; + this.cache = cache; + this.pointerCache = pointerCache; + } + + public string Upcoming => SubSequence(5).ToString(); + + public string Text { get; } + + public int Offset { get; } + public int Line { get; } + public int Column { get; } + private readonly ImmutableHashSet seen; + + public bool FindingRecursionFor(Parser parser) { + return false; + } + + public ITextPointer Add(Parser parser) { + var newSeen = seen.Add(parser); + return new PointerFromString(Text, Offset, Line, Column, pointerCache, cache, newSeen); + } + + public ITextPointer Remove(Parser parser) { + var newSeen = seen.Remove(parser); + if (pointerCache.TryGetValue(Offset, out var existingPointer)) { + return existingPointer; + } + return new PointerFromString(Text, Offset, Line, Column, pointerCache, cache, newSeen); + } + + public ITextPointer Drop(int amount) { + // if (references == 0) { + // cache.Clear(); + // }) + var newOffset = Offset + amount; + if (pointerCache.TryGetValue(newOffset, out var existingPointer)) { + return existingPointer; + } else { + var sequence = SubSequence(amount); + var lines = sequence.ToString().Split("\n"); // TODO optimize + var result = new PointerFromString(Text, newOffset, + Line + lines.Length - 1, + lines.Length > 1 ? lines.Last().Length : Column + amount, + pointerCache, + new(), + ImmutableHashSet.Empty); + pointerCache[newOffset] = result; + return result; + } + } + + public char First => At(0); + public int Length => Text.Length - Offset; + + public char At(int offset) { + return Text[Offset + offset]; + } + + public ReadOnlySpan Remainder => Text.AsSpan(Offset); + + public ReadOnlySpan SubSequence(int length) { + return Text.AsSpan(Offset, Math.Min(Length, length)); + } + + private int references = 0; + public void Ref() { + references++; + } + + public void UnRef() { + references--; + } + + private readonly Dictionary cache; + private readonly Dictionary pointerCache; + + public static HashSet hitReasons = new(); + public static HashSet misReasons = new(); + public ParseResult ParseWithCache(VoidParser parser, string reason) { + if (cache.TryGetValue(parser, out var result)) { + hitReasons.Add(reason); + return (ParseResult)result; + } + + misReasons.Add(reason); + + result = parser.Parse(this); + cache[parser] = result; + + return (ParseResult)result; + } + + public ParseResult ParseWithCache(Parser parser, string reason) { + if (cache.TryGetValue(parser, out var result)) { + hitReasons.Add(reason); + if (reason == "sequenceRight") { + var d = 3; + } + return (ParseResult)result; + } + misReasons.Add(reason); + + result = parser.Parse(this); + cache[parser] = result; + + return (ParseResult)result; + } +} \ No newline at end of file diff --git a/Source/CompilerBuilder/Parsers/RecursiveR.cs b/Source/CompilerBuilder/Parsers/RecursiveR.cs new file mode 100644 index 00000000000..b5f1c315476 --- /dev/null +++ b/Source/CompilerBuilder/Parsers/RecursiveR.cs @@ -0,0 +1,142 @@ +using Microsoft.Dafny; + +namespace CompilerBuilder; + +class EmptyResult : ParseResult { + public ParseResult Continue(Func, ParseResult> f) { + return new EmptyResult(); + } + + public ConcreteSuccess? Success => null; + public FailureResult? Failure => null; + public IFoundRecursion? FoundRecursion => null; + public IEnumerable> Recursions => []; +} + +class DeadPointer : ITextPointer { + public int Offset => 0; + public int Line => 0; + public int Column => 0; + public ITextPointer Drop(int amount) { + return this; + } + + public char First => throw new InvalidOperationException(); + public int Length => 0; + public char At(int offset) { + throw new InvalidOperationException(); + } + + public ReadOnlySpan Remainder => ReadOnlySpan.Empty; + public ReadOnlySpan SubSequence(int length) { + return ReadOnlySpan.Empty; + } + + public ParseResult ParseWithCache(VoidParser parser, string reason) { + return parser.Parse(this); + } + + public ParseResult ParseWithCache(Parser parser, string reason) { + return parser.Parse(this); + } + + public void Ref() { + } + + public void UnRef() { + } +} + +class RecursiveR(Func> get, string debugName) : Parser { + private readonly string debugName = debugName; + private Parser? inner; + + public Parser Inner => inner ??= get(); + + /// + /// It grows the seed result by building a "ParseResult -> ParseResult" using a 'IFoundRecursion' + /// + /// Alternatively, we could try to transform the grammar to get a separate base and grow grammar, + /// which would avoid hitting 'recursive calls' while determining the base + /// + /// However, transforming the grammar is difficult, partly due to empty parts + /// The only way to do it is the gather all the paths in the grammar + /// And then separate the left recursive ones from the others + /// expr = (empty | 'a') (expr | 'b') 'c' + /// path1 = expr 'c' + /// path2 = 'bc' + /// path3 = 'a' expr 'c' + /// path4 = 'abc' + /// base = 'bc' | 'a' expr 'c' | 'abc' + /// grow = grow 'c' + /// + private FoundRecursion? leftRecursion; + private bool checkedLeftRecursion; + enum RecursionState { FindingLeftRecursions, Parsing } + private readonly ThreadLocal findingRecursionState = new(() => RecursionState.Parsing); + + /// + /// Alternatively we could store the 'entered' state either in the ITextPointer, so we would store which parsers + /// we've entered instead of which offsets. + /// + /// Or we could pass this enteredParsers set down through the calls to 'Parse' + /// However, I didn't want to let recursion effect either ITextPointer or the interface of Parse. + /// If we had access to the call-stack, we would inspect it instead of using this field. + /// + /// I'm hoping that when we move to a stackless system, we'll have access to the 'stack', + /// and then we no longer need this field. + /// + private readonly ThreadLocal> enteredStack = new(() => new Nil()); + + public override ParseResult Parse(ITextPointer text) { + + var recursionState = findingRecursionState.Value; + if (recursionState == RecursionState.FindingLeftRecursions) { + return new FoundRecursion(Util.Identity); + } + + if (!checkedLeftRecursion) { + if (typeof(T).Name == "Statement") { + var d = 3; + } + findingRecursionState.Value = RecursionState.FindingLeftRecursions; + leftRecursion = (FoundRecursion?)Inner.Parse(new DeadPointer()).FoundRecursion; + findingRecursionState.Value = RecursionState.Parsing; + checkedLeftRecursion = true; + } + + var startingStack = enteredStack.Value!; + if (startingStack is Cons cons && cons.Head == text.Offset) { + // Hit left recursion + return new EmptyResult(); + } + + if (leftRecursion == null) { + return Inner.Parse(text); + } + + enteredStack.Value = new Cons(text.Offset, startingStack!); + // TODO caching here seems pointless + var seedResult = Inner.Parse(text); + enteredStack.Value = startingStack; + if (seedResult.Success == null) { + return seedResult; + } + + ParseResult combinedResult = seedResult; + ConcreteSuccess? bestSuccess = seedResult.Success; + + while (bestSuccess != null) { + // after a few iterations a binaryExpr 3 / x, is built + // now the binaryExpr itself is available as a seed, + // And the FoundRecursion that built it still holds a pionter to the BinaryExpr that was used to construct the initial one. + // Constructors should be on the right of self expressions + var newResult = leftRecursion.Apply(bestSuccess.Value!, bestSuccess.Remainder); + + combinedResult = combinedResult.Combine(newResult); + bestSuccess = newResult.Success; + } + + return combinedResult; + } +} \ No newline at end of file diff --git a/Source/CompilerBuilder/Parsers/Usage.cs b/Source/CompilerBuilder/Parsers/Usage.cs new file mode 100644 index 00000000000..101b5c6c9dc --- /dev/null +++ b/Source/CompilerBuilder/Parsers/Usage.cs @@ -0,0 +1,20 @@ +// See https://aka.ms/new-console-template for more information + +namespace CompilerBuilder; + +using static ParserBuilder; + +class Person() { + public string FirstName { get; set; } + public int Age { get; set; } + public string LastName { get; set; } +} + +class Test { + void ParseExample() { + var g = Value(() => new Person()) + .Then(Identifier, (p, v) => p.FirstName = v) + .Then(Number, (p, v) => p.Age = v) + .Then(Identifier, (p, v) => p.LastName = v); + } +} \ No newline at end of file diff --git a/Source/CompilerBuilder/Printers/Documents.cs b/Source/CompilerBuilder/Printers/Documents.cs new file mode 100644 index 00000000000..0b892516628 --- /dev/null +++ b/Source/CompilerBuilder/Printers/Documents.cs @@ -0,0 +1,142 @@ +namespace CompilerBuilder; + +public interface Document { + public void Render(TextWriter writer, int desiredWidth = 120) { + Render(desiredWidth, new IndentationWriter(writer, 2)); + } + + public string RenderAsString() { + var writer = new StringWriter(); + Render(writer); + return writer.ToString(); + } + + // TODO make internal + public void Render(int desiredWidth, IndentationWriter writer); + public bool IsEmpty { get; } + public int Size { get; } + + public Document Indent(int amount) { + return this is Empty ? this : new IndentD(this, amount); + } + + public Document Then(Document next, Separator separator) { + if (this is Empty) { + return next; + } + + if (next is Empty) { + return this; + } + + return new SequenceD(this, next, separator); + } +} + +record Verbatim(string Value) : Document { + + public void Render(int desiredWidth, IndentationWriter writer) { + writer.Write(Value); + } + + public bool IsEmpty => !Value.Any(); + public int Size => Value.Length; +} + +record IndentD(Document Inner, int Amount) : Document { + public override string ToString() { + return ((Document)this).RenderAsString(); + } + + public void Render(int desiredWidth, IndentationWriter writer) { + writer.Indent(); + Inner.Render(desiredWidth, writer); + writer.Undent(); + } + + public bool IsEmpty => Inner.IsEmpty; + public int Size => Inner.Size; +} + +record Empty : Document { + public static readonly Document Instance = new Empty(); + + private Empty() { } + + public void Render(int desiredWidth, IndentationWriter writer) { + } + + public bool IsEmpty => true; + public int Size => 0; +} + +public enum Separator { + Nothing, + Space, + Linebreak, + EmptyLine, + SpaceOrLinebreak, +} + +public class IndentationWriter(TextWriter writer, int spacesPerTick) { + private bool startOfLine = true; + private int indentationTicks = 0; + public int LineWidth { get; private set; } = 0; + + public void Write(string value) { + if (startOfLine) { + var spaces = new string(' ', indentationTicks * spacesPerTick); + LineWidth += spaces.Length; + writer.Write(spaces); + } + writer.Write(value); + LineWidth += value.Length; + startOfLine = false; + } + + public void WriteLine() { + writer.WriteLine(); + startOfLine = true; + LineWidth = 0; + } + + public void Indent() { + indentationTicks++; + } + + public void Undent() { + indentationTicks--; + } +} + +record SequenceD(Document Left, Document Right, Separator Separator) : Document { + public override string ToString() { + return ((Document)this).RenderAsString(); + } + + public void Render(int desiredWidth, IndentationWriter writer) { + Left.Render(desiredWidth, writer); + if (Separator == Separator.Nothing) { + } else if (Separator == Separator.Space) { + if (!Left.IsEmpty && !Right.IsEmpty) { + writer.Write(" "); + } + } else if (Separator == Separator.Linebreak || Separator == Separator.EmptyLine) { + if (Separator == Separator.EmptyLine) { + writer.WriteLine(); + } + writer.WriteLine(); + } else if (Separator == Separator.SpaceOrLinebreak) { + throw new NotImplementedException(); + // if (writer.LineWidth + Right.Width > desiredWidth) { + // writer.WriteLine(); + // } + } else { + throw new NotSupportedException(); + } + Right.Render(desiredWidth, writer); + } + + public bool IsEmpty => Left.IsEmpty && Right.IsEmpty; + public int Size { get; } = Left.Size + Right.Size; +} \ No newline at end of file diff --git a/Source/CompilerBuilder/Printers/Printer.cs b/Source/CompilerBuilder/Printers/Printer.cs new file mode 100644 index 00000000000..fe1ecd2a32a --- /dev/null +++ b/Source/CompilerBuilder/Printers/Printer.cs @@ -0,0 +1,260 @@ +// See https://aka.ms/new-console-template for more information + +namespace CompilerBuilder; + +record IndentW(Printer Inner, int Amount) : Printer { + public PrintResult Print(T value) { + var innerValue = Inner.Print(value); + return innerValue.Continue(v => v.Indent(Amount)); + } +} + +public record Failure(object? Value, Printer Printer, Document SoFar, string Message) { + public static Failure? Max(Failure? first, Failure? second) { + if (first == null) { + return second; + } + + if (second == null) { + return first; + } + return first.SoFar.Size >= second.SoFar.Size ? first : second; + } +} + +public record PrintResult(Document? Success, Failure? LongestFailure) { + + public Document ForceSuccess { + get { + if (Success == null) { + var soFarString = LongestFailure!.SoFar.RenderAsString(); + throw new Exception($"Printing failed with message {LongestFailure!.Message}. Longest print was:\n{soFarString}"); + } + + return Success; + } + } + public PrintResult(object? value, Printer printer, string message) : this(null, new Failure(value, printer, Empty.Instance, message)) { } + + public PrintResult(Document Success) : this(Success, null) { } + + public PrintResult Continue(Func f) { + return new PrintResult(Success == null ? null : f(Success), LongestFailure == null ? null : LongestFailure with { SoFar = f(LongestFailure.SoFar) }); + } + + public PrintResult WithFailure(Failure? failure, bool priority) { + if (failure == null) { + return this; + } + + if (Success != null) { + // TODO we have a curious situation with "true" -> Constant(true) leading to a longer SoFar than a success + if (Success.Size >= failure.SoFar.Size) { + return this; + } + } + + return this with { LongestFailure = priority ? Failure.Max(failure, LongestFailure) : Failure.Max(LongestFailure, failure) }; + } +} + +public interface Printer : Printer { + + public PrintResult Print(T value); +} + +class FailW(string message) : Printer { + public string Message => message; + + public PrintResult Print(T value) { + return new PrintResult(value, this, message); + } +} + +class RecursiveW(Func> get) : Printer { + private Printer? inner; + public Printer Inner => inner ??= get(); + + public PrintResult Print(T value) { + return Inner.Print(value); + } +} + +class ChoiceW(Printer first, Printer second): Printer { + + public Printer First => first; + public Printer Second => second; + + public PrintResult Print(T value) { + var firstResult = First.Print(value); + var secondResult = Second.Print(value); + if (firstResult.Success == null) { + return secondResult.WithFailure(firstResult.LongestFailure, true); + } + + return firstResult.WithFailure(secondResult.LongestFailure, false); + } +} + +class Cast(Printer printer) : Printer { + public PrintResult Print(U value) { + if (value is T t) { + return printer.Print(t); + } + + return new PrintResult(value, this, $"Value {value + ""} was not of type {typeof(T)}"); + } +} + +public interface Printer; + +public interface VoidPrinter : Printer { + + public Document Print(); +} + +class EmptyW : VoidPrinter { + public static readonly EmptyW Instance = new(); + + private EmptyW() { } + public Document Print() { + return Empty.Instance; + } +} + +class VerbatimW : Printer { + public static readonly Printer Instance = new VerbatimW(); + + private VerbatimW() { } + public PrintResult Print(string value) { + return new PrintResult(new Verbatim(value)); + } +} + +class MapWithoutFailW(Printer printer, Func map) : Printer { + public PrintResult Print(U value) { + var newValue = map(value); + return printer.Print(newValue); + } +} + +class MapW(Printer printer, Func map) : Printer { + public PrintResult Print(U value) { + return printer.Print(map(value)); + } +} + +class OptionMapW(Printer printer, Func> map) : Printer { + + public Printer Printer => printer; + + public PrintResult Print(U value) { + var newValue = map(value); + if (newValue is MapSuccess success) { + return printer.Print(success.Value); + } + + if (value?.ToString() == "i := i + 1;") { + var e = 3; + } + return new PrintResult(value, this, "OptionMap failure"); + } +} + +class ValueW(Func check, VoidPrinter printer) : Printer { + + public Func Check => check; + + public PrintResult Print(T value) { + if (check(value)) { + return new PrintResult(printer.Print()); + } + + return new PrintResult(value, this, "ValueW check failure"); + } +} + +class IgnoreW(VoidPrinter printer) : Printer { + public PrintResult Print(T value) { + return new PrintResult(printer.Print()); + } +} + +// TODO rename TextW and VerbatimW to make the difference more clear? +internal class TextW(string value) : VoidPrinter { + public Document Print() { + return new Verbatim(value); + } +} + +// TODO replace by map and VerbatimW? +internal class NumberW : Printer { + public PrintResult Print(int value) { + return new PrintResult(new Verbatim(value.ToString())); + } +} + +class SequenceW(Printer first, Printer second, + Func destruct, Separator separator) : Printer { + + public Printer First => first; + public Printer Second => second; + + public PrintResult Print(T value) { + var t = destruct(value); + if (t == null) { + return new PrintResult(value, this, "sequence destruct failure"); + } + + var (firstValue, secondValue) = t.Value; + var firstDoc = first.Print(firstValue); + if (firstDoc.Success == null) { + return firstDoc; + } + + var secondResult = second.Print(secondValue); + var printResult = secondResult.Continue(s => firstDoc.Success.Then(s, separator)); + return printResult.WithFailure(firstDoc.LongestFailure, false); + } +} + +class SkipLeftW(VoidPrinter first, Printer second, Separator separator) : Printer { + public VoidPrinter First => first; + public Printer Second => second; + + public PrintResult Print(T value) { + var firstValue = first.Print(); + var secondValue = second.Print(value); + return secondValue.Continue(s => firstValue.Then(s, separator)); + } +} + +class SkipRightW(Printer first, VoidPrinter second, Separator separator) : Printer { + public Printer First => first; + public VoidPrinter Second => second; + + public PrintResult Print(T value) { + var firstValue = first.Print(value); + if (firstValue.Success == null) { + return firstValue; + } + // TODO maybe we should not copy the firstValue to the LongestFailure here, because in a way it failed as well. + return firstValue.Continue(f => f.Then(second.Print(), separator)); + } +} + +class NeitherW(VoidPrinter first, VoidPrinter second, Separator separator) : VoidPrinter { + public Document Print() { + return first.Print().Then(second.Print(), separator); + } +} + +public static class PrinterExtensions { + public static Printer Map(this Printer printer, Func> map) { + return new OptionMapW(printer, map); + } + + public static Printer Map(this Printer printer, Func map) { + return new MapW(printer, map); + } +} \ No newline at end of file diff --git a/Source/Dafny.sln b/Source/Dafny.sln index 23297b185ed..63f03b43276 100644 --- a/Source/Dafny.sln +++ b/Source/Dafny.sln @@ -43,6 +43,14 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyDriver.Test", "DafnyDr EndProject Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyCore.Test", "DafnyCore.Test\DafnyCore.Test.csproj", "{33C29F26-A27B-474D-B436-83EA615B09FC}" EndProject +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "CompilerBuilder", "CompilerBuilder\CompilerBuilder.csproj", "{E1271309-8A75-4172-BEE4-035272362B2D}" +EndProject +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "JavaSupport", "JavaSupport\JavaSupport.csproj", "{78FD5A82-DA93-4840-82C6-052E0EA5C67A}" +EndProject +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "CompilerBuilder.Test", "CompilerBuilder.Test\CompilerBuilder.Test.csproj", "{A1F4A6C3-F0DE-4D4E-B37B-2F5DFC0541A2}" +EndProject +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "JavaSupport.Test", "JavaSupport.Test\JavaSupport.Test.csproj", "{C3615FE2-46B3-487F-9925-9965E7DEBC94}" +EndProject EndProject Global GlobalSection(SolutionConfigurationPlatforms) = preSolution @@ -130,6 +138,22 @@ Global {96B8ADA8-6190-49F7-8C38-CDA60DC92293}.Debug|Any CPU.Build.0 = Debug|Any CPU {96B8ADA8-6190-49F7-8C38-CDA60DC92293}.Release|Any CPU.ActiveCfg = Release|Any CPU {96B8ADA8-6190-49F7-8C38-CDA60DC92293}.Release|Any CPU.Build.0 = Release|Any CPU + {E1271309-8A75-4172-BEE4-035272362B2D}.Debug|Any CPU.ActiveCfg = Debug|Any CPU + {E1271309-8A75-4172-BEE4-035272362B2D}.Debug|Any CPU.Build.0 = Debug|Any CPU + {E1271309-8A75-4172-BEE4-035272362B2D}.Release|Any CPU.ActiveCfg = Release|Any CPU + {E1271309-8A75-4172-BEE4-035272362B2D}.Release|Any CPU.Build.0 = Release|Any CPU + {78FD5A82-DA93-4840-82C6-052E0EA5C67A}.Debug|Any CPU.ActiveCfg = Debug|Any CPU + {78FD5A82-DA93-4840-82C6-052E0EA5C67A}.Debug|Any CPU.Build.0 = Debug|Any CPU + {78FD5A82-DA93-4840-82C6-052E0EA5C67A}.Release|Any CPU.ActiveCfg = Release|Any CPU + {78FD5A82-DA93-4840-82C6-052E0EA5C67A}.Release|Any CPU.Build.0 = Release|Any CPU + {A1F4A6C3-F0DE-4D4E-B37B-2F5DFC0541A2}.Debug|Any CPU.ActiveCfg = Debug|Any CPU + {A1F4A6C3-F0DE-4D4E-B37B-2F5DFC0541A2}.Debug|Any CPU.Build.0 = Debug|Any CPU + {A1F4A6C3-F0DE-4D4E-B37B-2F5DFC0541A2}.Release|Any CPU.ActiveCfg = Release|Any CPU + {A1F4A6C3-F0DE-4D4E-B37B-2F5DFC0541A2}.Release|Any CPU.Build.0 = Release|Any CPU + {C3615FE2-46B3-487F-9925-9965E7DEBC94}.Debug|Any CPU.ActiveCfg = Debug|Any CPU + {C3615FE2-46B3-487F-9925-9965E7DEBC94}.Debug|Any CPU.Build.0 = Debug|Any CPU + {C3615FE2-46B3-487F-9925-9965E7DEBC94}.Release|Any CPU.ActiveCfg = Release|Any CPU + {C3615FE2-46B3-487F-9925-9965E7DEBC94}.Release|Any CPU.Build.0 = Release|Any CPU EndGlobalSection GlobalSection(SolutionProperties) = preSolution HideSolutionNode = FALSE diff --git a/Source/Dafny/Dafny.csproj b/Source/Dafny/Dafny.csproj index ff383440c30..422750bf6d6 100644 --- a/Source/Dafny/Dafny.csproj +++ b/Source/Dafny/Dafny.csproj @@ -5,7 +5,7 @@ Dafny true TRACE - net6.0 + net8.0 Major ..\..\Binaries\ false diff --git a/Source/DafnyBenchmarkingPlugin/BenchmarkInstrumentation.cs b/Source/DafnyBenchmarkingPlugin/BenchmarkInstrumentation.cs index 9a8291c09f3..70a72b406cc 100644 --- a/Source/DafnyBenchmarkingPlugin/BenchmarkInstrumentation.cs +++ b/Source/DafnyBenchmarkingPlugin/BenchmarkInstrumentation.cs @@ -6,7 +6,7 @@ public class BenchmarkingCompilerInstrumenter : CompilerInstrumenter { public BenchmarkingCompilerInstrumenter(ErrorReporter reporter) : base(reporter) { } - public override void Instrument(IExecutableBackend backend, SinglePassCodeGenerator codeGenerator, Program program) { + public override void Instrument(IExecutableBackend backend, CodeGenerator codeGenerator, Program program) { if (codeGenerator is JavaCodeGenerator javaCompiler) { javaCompiler.AddInstrumenter(new JavaBenchmarkCompilationInstrumenter(Reporter)); } else { diff --git a/Source/DafnyBenchmarkingPlugin/DafnyBenchmarkingPlugin.csproj b/Source/DafnyBenchmarkingPlugin/DafnyBenchmarkingPlugin.csproj index 9cf987817bc..32aacffb139 100644 --- a/Source/DafnyBenchmarkingPlugin/DafnyBenchmarkingPlugin.csproj +++ b/Source/DafnyBenchmarkingPlugin/DafnyBenchmarkingPlugin.csproj @@ -1,7 +1,7 @@ - net6.0 + net8.0 Major enable enable diff --git a/Source/DafnyCore.Test/DafnyCore.Test.csproj b/Source/DafnyCore.Test/DafnyCore.Test.csproj index 8e9d3e8aeba..635725c74cf 100644 --- a/Source/DafnyCore.Test/DafnyCore.Test.csproj +++ b/Source/DafnyCore.Test/DafnyCore.Test.csproj @@ -1,7 +1,7 @@ - net6.0 + net8.0 enable enable diff --git a/Source/DafnyCore.Test/Languages/JavaPrinterTest.cs b/Source/DafnyCore.Test/Languages/JavaPrinterTest.cs new file mode 100644 index 00000000000..e4312a3e6e2 --- /dev/null +++ b/Source/DafnyCore.Test/Languages/JavaPrinterTest.cs @@ -0,0 +1,26 @@ +using Microsoft.Dafny; + +namespace DafnyCore.Test.Languages; + +public class JavaPrinterTest { + + [Fact] + public void ParseAndPrint() { + var input = @" +class Div { + int Foo(int x) + requires x != 0 + { + return 3 / x; + } +}".TrimStart(); + var grammarBuilder = new JavaGrammar(new Uri(Directory.GetCurrentDirectory()), DafnyOptions.Default); + var grammar = grammarBuilder.GetFinalGrammar(); + var parser = grammar.ToParser(); + var printer = grammar.ToPrinter(); + + var parsed = parser.Parse(input).Success!.Value; + var output = printer.Print(parsed).ForceSuccess.RenderAsString(); + Assert.Equal(input, output); + } +} \ No newline at end of file diff --git a/Source/DafnyCore/AST/Cloner.cs b/Source/DafnyCore/AST/Cloner.cs index fcceee43562..1e856edd927 100644 --- a/Source/DafnyCore/AST/Cloner.cs +++ b/Source/DafnyCore/AST/Cloner.cs @@ -13,7 +13,7 @@ interface ICloneable { T Clone(Cloner cloner); } - public class Cloner { + public class Cloner : ICloner { public bool CloneResolvedFields { get; } private readonly Dictionary statementClones = new(); private readonly Dictionary clones = new(); diff --git a/Source/DafnyCore/AST/Expressions/Applications/ApplySuffix.cs b/Source/DafnyCore/AST/Expressions/Applications/ApplySuffix.cs index 15a703bec34..fadf4b4634c 100644 --- a/Source/DafnyCore/AST/Expressions/Applications/ApplySuffix.cs +++ b/Source/DafnyCore/AST/Expressions/Applications/ApplySuffix.cs @@ -10,7 +10,7 @@ namespace Microsoft.Dafny; public class ApplySuffix : SuffixExpr, ICloneable, ICanFormat { public readonly IToken/*?*/ AtTok; public readonly IToken CloseParen; - public readonly ActualBindings Bindings; + public ActualBindings Bindings; public List Args => Bindings.Arguments; [FilledInDuringResolution] public MethodCallInformation MethodCallInfo = null; // resolution will set to a non-null value if ApplySuffix makes a method call @@ -27,6 +27,9 @@ public ApplySuffix Clone(Cloner cloner) { return new ApplySuffix(cloner, this); } + public ApplySuffix() : base(Token.Parsing, null) { + } + public ApplySuffix(Cloner cloner, ApplySuffix original) : base(cloner, original) { AtTok = original.AtTok == null ? null : cloner.Tok(original.AtTok); diff --git a/Source/DafnyCore/AST/Expressions/Applications/ExprDotName.cs b/Source/DafnyCore/AST/Expressions/Applications/ExprDotName.cs index 4c24490cdd1..5aace8eec07 100644 --- a/Source/DafnyCore/AST/Expressions/Applications/ExprDotName.cs +++ b/Source/DafnyCore/AST/Expressions/Applications/ExprDotName.cs @@ -7,7 +7,7 @@ namespace Microsoft.Dafny; /// An ExprDotName desugars into either an IdentifierExpr (if the Lhs is a static name) or a MemberSelectExpr (if the Lhs is a computed expression). /// public class ExprDotName : SuffixExpr, ICloneable { - public readonly string SuffixName; + public string SuffixName; public readonly List OptTypeArguments; /// @@ -27,6 +27,10 @@ public ExprDotName Clone(Cloner cloner) { return new ExprDotName(cloner, this); } + public ExprDotName() : base(Token.Parsing, null) { + // OptTypeArguments = []; + } + public ExprDotName(Cloner cloner, ExprDotName original) : base(cloner, original) { SuffixName = original.SuffixName; OptTypeArguments = original.OptTypeArguments?.ConvertAll(cloner.CloneType); diff --git a/Source/DafnyCore/AST/Expressions/Applications/NameSegment.cs b/Source/DafnyCore/AST/Expressions/Applications/NameSegment.cs index e99628ddadc..3521c4be024 100644 --- a/Source/DafnyCore/AST/Expressions/Applications/NameSegment.cs +++ b/Source/DafnyCore/AST/Expressions/Applications/NameSegment.cs @@ -15,7 +15,7 @@ public NameSegment(IToken tok, string name, List optTypeArguments) Name = name; OptTypeArguments = optTypeArguments; } - + public NameSegment(Cloner cloner, NameSegment original) : base(cloner, original) { Name = original.Name; OptTypeArguments = original.OptTypeArguments?.ConvertAll(cloner.CloneType); diff --git a/Source/DafnyCore/AST/Expressions/Applications/SeqSelectExpr.cs b/Source/DafnyCore/AST/Expressions/Applications/SeqSelectExpr.cs index 5c629bc582a..4f537b2c378 100644 --- a/Source/DafnyCore/AST/Expressions/Applications/SeqSelectExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Applications/SeqSelectExpr.cs @@ -5,9 +5,9 @@ namespace Microsoft.Dafny; public class SeqSelectExpr : Expression, ICloneable { public readonly bool SelectOne; // false means select a range - public readonly Expression Seq; - public readonly Expression E0; - public readonly Expression E1; + public Expression Seq; + public Expression E0; + public Expression E1; public readonly IToken CloseParen; public SeqSelectExpr(Cloner cloner, SeqSelectExpr original) : base(cloner, original) { @@ -24,6 +24,10 @@ void ObjectInvariant() { Contract.Invariant(!SelectOne || E1 == null); } + public SeqSelectExpr(bool selectOne) : base(Token.Parsing) { + SelectOne = selectOne; + } + public SeqSelectExpr(IToken tok, bool selectOne, Expression seq, Expression e0, Expression e1, IToken closeParen) : base(tok) { Contract.Requires(tok != null); diff --git a/Source/DafnyCore/AST/Expressions/Applications/SuffixExpr.cs b/Source/DafnyCore/AST/Expressions/Applications/SuffixExpr.cs index 7deb3808106..0592ddfdfba 100644 --- a/Source/DafnyCore/AST/Expressions/Applications/SuffixExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Applications/SuffixExpr.cs @@ -36,7 +36,7 @@ namespace Microsoft.Dafny; /// seem more natural to refactor these into 3: IndexSuffixExpr and 4: RangeSuffixExpr. /// public abstract class SuffixExpr : ConcreteSyntaxExpression { - public readonly Expression Lhs; + public Expression Lhs; protected SuffixExpr(Cloner cloner, SuffixExpr original) : base(cloner, original) { Lhs = cloner.CloneExpr(original.Lhs); diff --git a/Source/DafnyCore/AST/Expressions/Applications/ThisExpr.cs b/Source/DafnyCore/AST/Expressions/Applications/ThisExpr.cs index fadf6162007..213f7c2f9b9 100644 --- a/Source/DafnyCore/AST/Expressions/Applications/ThisExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Applications/ThisExpr.cs @@ -46,6 +46,10 @@ public class ImplicitThisExpr : ThisExpr, ICloneable { public ImplicitThisExpr(Cloner cloner, ImplicitThisExpr original) : base(cloner, original) { } + public ImplicitThisExpr() + : base(Token.Parsing) { + } + public ImplicitThisExpr(IToken tok) : base(new AutoGeneratedToken(tok)) { Contract.Requires(tok != null); diff --git a/Source/DafnyCore/AST/Expressions/Comprehensions/ComprehensionExpr.cs b/Source/DafnyCore/AST/Expressions/Comprehensions/ComprehensionExpr.cs index 0abfc1614cd..33184094685 100644 --- a/Source/DafnyCore/AST/Expressions/Comprehensions/ComprehensionExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Comprehensions/ComprehensionExpr.cs @@ -25,7 +25,7 @@ namespace Microsoft.Dafny; /// public abstract partial class ComprehensionExpr : Expression, IAttributeBearingDeclaration, IBoundVarsBearingExpression, ICanFormat { public virtual string WhatKind => "comprehension"; - public readonly List BoundVars; + public List BoundVars; public readonly Expression Range; public Expression Term; diff --git a/Source/DafnyCore/AST/Expressions/Comprehensions/LambdaExpr.cs b/Source/DafnyCore/AST/Expressions/Comprehensions/LambdaExpr.cs index add5306ab3a..5b6e7f53e76 100644 --- a/Source/DafnyCore/AST/Expressions/Comprehensions/LambdaExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Comprehensions/LambdaExpr.cs @@ -10,6 +10,10 @@ public class LambdaExpr : ComprehensionExpr, ICloneable, IFrameScope public readonly Specification Reads; + public LambdaExpr() : base(Token.Parsing, RangeToken.NoToken, new List(), null, null, null) { + + } + public LambdaExpr(IToken tok, RangeToken rangeToken, List bvars, Expression requires, Specification reads, Expression body) : base(tok, rangeToken, bvars, requires, body, null) { Contract.Requires(reads != null); diff --git a/Source/DafnyCore/AST/Expressions/Conditional/ITEExpr.cs b/Source/DafnyCore/AST/Expressions/Conditional/ITEExpr.cs index aa6e606c27c..cbafd51833f 100644 --- a/Source/DafnyCore/AST/Expressions/Conditional/ITEExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Conditional/ITEExpr.cs @@ -5,10 +5,15 @@ namespace Microsoft.Dafny; public class ITEExpr : Expression, ICanFormat, ICloneable { public readonly bool IsBindingGuard; - public readonly Expression Test; - public readonly Expression Thn; - public readonly Expression Els; + public Expression Test; + public Expression Thn; + public Expression Els; + /// + /// Constructor for the parser + /// + public ITEExpr() : base(Token.Parsing) { } + public ITEExpr(Cloner cloner, ITEExpr original) : base(cloner, original) { IsBindingGuard = original.IsBindingGuard; Test = cloner.CloneExpr(original.Test); diff --git a/Source/DafnyCore/AST/Expressions/Expression.cs b/Source/DafnyCore/AST/Expressions/Expression.cs index 2b5d5d31bef..e55621fe9f9 100644 --- a/Source/DafnyCore/AST/Expressions/Expression.cs +++ b/Source/DafnyCore/AST/Expressions/Expression.cs @@ -2,6 +2,7 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; using System.Numerics; +using DafnyCore.Generic; namespace Microsoft.Dafny; diff --git a/Source/DafnyCore/AST/Expressions/Heap/FrameExpression.cs b/Source/DafnyCore/AST/Expressions/Heap/FrameExpression.cs index d946addaa92..ca3c738aaa4 100644 --- a/Source/DafnyCore/AST/Expressions/Heap/FrameExpression.cs +++ b/Source/DafnyCore/AST/Expressions/Heap/FrameExpression.cs @@ -1,11 +1,12 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; using System.Linq; +using DafnyCore.Generic; namespace Microsoft.Dafny; public class FrameExpression : TokenNode, IHasReferences { - public readonly Expression OriginalExpression; // may be a WildcardExpr + public Expression OriginalExpression; // may be a WildcardExpr [FilledInDuringResolution] public Expression DesugaredExpression; // may be null for modifies clauses, even after resolution /// @@ -13,13 +14,17 @@ public class FrameExpression : TokenNode, IHasReferences { /// public Expression E => DesugaredExpression ?? OriginalExpression; + public FrameExpression() { + + } + [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(E != null); Contract.Invariant(!(E is WildcardExpr) || (FieldName == null && Field == null)); } - public readonly string FieldName; + public string FieldName; [FilledInDuringResolution] public Field Field; // null if FieldName is /// diff --git a/Source/DafnyCore/AST/Expressions/Heap/WildcardExpr.cs b/Source/DafnyCore/AST/Expressions/Heap/WildcardExpr.cs index c39d47f0817..a8a87181516 100644 --- a/Source/DafnyCore/AST/Expressions/Heap/WildcardExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Heap/WildcardExpr.cs @@ -7,10 +7,15 @@ public class WildcardExpr : Expression, ICloneable { // a Wildcar public WildcardExpr(Cloner cloner, WildcardExpr original) : base(cloner, original) { } + public WildcardExpr() + : base(Token.Parsing) { + } + public WildcardExpr(IToken tok) : base(tok) { Contract.Requires(tok != null); } + public WildcardExpr Clone(Cloner cloner) { return new WildcardExpr(cloner, this); diff --git a/Source/DafnyCore/AST/Expressions/LiteralExpr.cs b/Source/DafnyCore/AST/Expressions/LiteralExpr.cs index 9d5cc860c0c..fc74682720b 100644 --- a/Source/DafnyCore/AST/Expressions/LiteralExpr.cs +++ b/Source/DafnyCore/AST/Expressions/LiteralExpr.cs @@ -100,6 +100,33 @@ public LiteralExpr(Cloner cloner, LiteralExpr original) : base(cloner, original) public LiteralExpr Clone(Cloner cloner) { return new LiteralExpr(cloner, this); } + + protected bool Equals(LiteralExpr other) + { + return Equals(Value, other.Value); + } + + public override bool Equals(object obj) + { + if (ReferenceEquals(null, obj)) { + return false; + } + + if (ReferenceEquals(this, obj)) { + return true; + } + + if (obj.GetType() != this.GetType()) { + return false; + } + + return Equals((LiteralExpr)obj); + } + + public override int GetHashCode() + { + return (Value != null ? Value.GetHashCode() : 0); + } } public class CharLiteralExpr : LiteralExpr, ICloneable { diff --git a/Source/DafnyCore/AST/Expressions/Operators/BinaryExpr.cs b/Source/DafnyCore/AST/Expressions/Operators/BinaryExpr.cs index b81c90e4840..f35a604ed79 100644 --- a/Source/DafnyCore/AST/Expressions/Operators/BinaryExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Operators/BinaryExpr.cs @@ -33,7 +33,7 @@ public enum Opcode { BitwiseOr, BitwiseXor } - public readonly Opcode Op; + public Opcode Op; public enum ResolvedOpcode { YetUndetermined, // the value before resolution has determined the value; .ResolvedOp should never be read in this state @@ -299,7 +299,12 @@ public static string OpcodeString(Opcode op) { throw new cce.UnreachableException(); // unexpected operator } } - public Expression E0; + + public Expression E0 { + get; + set; + } + public Expression E1; public enum AccumulationOperand { None, Left, Right } public AccumulationOperand AccumulatesForTailRecursion = AccumulationOperand.None; // set by Resolver @@ -315,6 +320,8 @@ public BinaryExpr Clone(Cloner cloner) { return new BinaryExpr(cloner, this); } + public BinaryExpr() : base(Token.Parsing) { } + public BinaryExpr(Cloner cloner, BinaryExpr original) : base(cloner, original) { this.Op = original.Op; this.E0 = cloner.CloneExpr(original.E0); diff --git a/Source/DafnyCore/AST/Expressions/Operators/UnaryExpr.cs b/Source/DafnyCore/AST/Expressions/Operators/UnaryExpr.cs index bcc7cf05a61..d79de66797f 100644 --- a/Source/DafnyCore/AST/Expressions/Operators/UnaryExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Operators/UnaryExpr.cs @@ -4,7 +4,7 @@ namespace Microsoft.Dafny; public abstract class UnaryExpr : Expression, ICanFormat { - public readonly Expression E; + public Expression E; [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(E != null); diff --git a/Source/DafnyCore/AST/Expressions/Operators/UnaryOpExpr.cs b/Source/DafnyCore/AST/Expressions/Operators/UnaryOpExpr.cs index bf1f6d82a85..45205eaccfa 100644 --- a/Source/DafnyCore/AST/Expressions/Operators/UnaryOpExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Operators/UnaryOpExpr.cs @@ -1,4 +1,5 @@ using System.Diagnostics.Contracts; +using System.Reflection.Emit; namespace Microsoft.Dafny; @@ -11,7 +12,7 @@ public enum Opcode { Lit, // there is no syntax for this operator, but it is sometimes introduced during translation Assigned, } - public readonly Opcode Op; + public Opcode Op; public enum ResolvedOpcode { YetUndetermined, @@ -59,6 +60,13 @@ public void SetResolveOp(ResolvedOpcode resolvedOpcode) { _ResolvedOp = resolvedOpcode; } + public UnaryOpExpr(Opcode op) : base(Token.Parsing, null) { + Op = op; + } + + public UnaryOpExpr() : base(Token.Parsing, null) { + } + public UnaryOpExpr(IToken tok, Opcode op, Expression e) : base(tok, e) { Contract.Requires(tok != null); diff --git a/Source/DafnyCore/AST/Expressions/Types/ConversionExpr.cs b/Source/DafnyCore/AST/Expressions/Types/ConversionExpr.cs index 710b98fe58c..964204e0c3d 100644 --- a/Source/DafnyCore/AST/Expressions/Types/ConversionExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Types/ConversionExpr.cs @@ -5,6 +5,9 @@ namespace Microsoft.Dafny; public class ConversionExpr : TypeUnaryExpr, ICloneable { public readonly string messagePrefix; + public ConversionExpr() : base(Token.Parsing, null, null) { + } + public ConversionExpr(Cloner cloner, ConversionExpr original) : base(cloner, original) { messagePrefix = original.messagePrefix; } diff --git a/Source/DafnyCore/AST/Expressions/Types/TypeUnaryExpr.cs b/Source/DafnyCore/AST/Expressions/Types/TypeUnaryExpr.cs index e270e5d04c8..d275261b1aa 100644 --- a/Source/DafnyCore/AST/Expressions/Types/TypeUnaryExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Types/TypeUnaryExpr.cs @@ -5,7 +5,7 @@ namespace Microsoft.Dafny; public abstract class TypeUnaryExpr : UnaryExpr { - public readonly Type ToType; + public Type ToType; protected TypeUnaryExpr(Cloner cloner, TypeUnaryExpr original) : base(cloner, original) { ToType = cloner.CloneType(original.ToType); diff --git a/Source/DafnyCore/AST/Expressions/Variables/AutoGhostIdentifierExpr.cs b/Source/DafnyCore/AST/Expressions/Variables/AutoGhostIdentifierExpr.cs index a4c64255745..e5c35d71a94 100644 --- a/Source/DafnyCore/AST/Expressions/Variables/AutoGhostIdentifierExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Variables/AutoGhostIdentifierExpr.cs @@ -7,6 +7,10 @@ namespace Microsoft.Dafny; /// parser and parts of the resolver. /// public class AutoGhostIdentifierExpr : IdentifierExpr, ICloneable { + + public AutoGhostIdentifierExpr() : base(Token.Parsing, (string)null) { + } + public AutoGhostIdentifierExpr(IToken tok, string name) : base(new AutoGeneratedToken(tok), name) { } diff --git a/Source/DafnyCore/AST/Expressions/Variables/BoundVar.cs b/Source/DafnyCore/AST/Expressions/Variables/BoundVar.cs index db914c9c9f6..60da9d87838 100644 --- a/Source/DafnyCore/AST/Expressions/Variables/BoundVar.cs +++ b/Source/DafnyCore/AST/Expressions/Variables/BoundVar.cs @@ -7,6 +7,10 @@ namespace Microsoft.Dafny; [DebuggerDisplay("Bound<{name}>")] public class BoundVar : NonglobalVariable { public override bool IsMutable => false; + + public BoundVar() : base(Token.Parsing, null, null, false) { + + } public BoundVar(IToken tok, string name, Type type) : base(tok, name, type, false) { Contract.Requires(tok != null); diff --git a/Source/DafnyCore/AST/Expressions/Variables/Formal.cs b/Source/DafnyCore/AST/Expressions/Variables/Formal.cs index cdbff00e752..3ccfddafdc2 100644 --- a/Source/DafnyCore/AST/Expressions/Variables/Formal.cs +++ b/Source/DafnyCore/AST/Expressions/Variables/Formal.cs @@ -7,13 +7,17 @@ namespace Microsoft.Dafny; public class Formal : NonglobalVariable { public Attributes Attributes { get; set; } - public readonly bool InParam; // true to in-parameter, false for out-parameter + public bool InParam; // true to in-parameter, false for out-parameter public override bool IsMutable => !InParam; public readonly bool IsOld; public Expression DefaultValue; public readonly bool IsNameOnly; public readonly bool IsOlder; - public readonly string NameForCompilation; + public string NameForCompilation => nameForCompilation ?? Name; + + public Formal() : base(Token.Parsing, null, null, false) + { + } public Formal(IToken tok, string name, Type type, bool inParam, bool isGhost, Expression defaultValue, Attributes attributes = null, @@ -30,12 +34,14 @@ public Formal(IToken tok, string name, Type type, bool inParam, bool isGhost, Ex Attributes = attributes; IsNameOnly = isNameOnly; IsOlder = isOlder; - NameForCompilation = nameForCompilation ?? name; + this.nameForCompilation = nameForCompilation; } public bool HasName => !Name.StartsWith("#"); private string sanitizedName; + private readonly string nameForCompilation; + public override string SanitizedName => sanitizedName ??= SanitizeName(Name); // No unique-ification public override string CompileName => diff --git a/Source/DafnyCore/AST/Expressions/Variables/IdentifierExpr.cs b/Source/DafnyCore/AST/Expressions/Variables/IdentifierExpr.cs index c1c3777b450..82426ee0dcf 100644 --- a/Source/DafnyCore/AST/Expressions/Variables/IdentifierExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Variables/IdentifierExpr.cs @@ -10,7 +10,7 @@ void ObjectInvariant() { Contract.Invariant(Name != null); } - public readonly string Name; + public string Name; [FilledInDuringResolution] public IVariable Var; public string DafnyName => tok.line > 0 ? RangeToken.PrintOriginal() : Name; diff --git a/Source/DafnyCore/AST/Expressions/Variables/NonglobalVariable.cs b/Source/DafnyCore/AST/Expressions/Variables/NonglobalVariable.cs index 88aa24aa10f..64c82b62bdf 100644 --- a/Source/DafnyCore/AST/Expressions/Variables/NonglobalVariable.cs +++ b/Source/DafnyCore/AST/Expressions/Variables/NonglobalVariable.cs @@ -6,7 +6,7 @@ namespace Microsoft.Dafny; public abstract class NonglobalVariable : TokenNode, IVariable { - readonly string name; + string name; protected NonglobalVariable(IToken tok, string name, Type type, bool isGhost) { Contract.Requires(tok != null); @@ -30,6 +30,7 @@ public string Name { Contract.Ensures(Contract.Result() != null); return name; } + set => name = value; } public string DafnyName => RangeToken == null || tok.line == 0 ? Name : RangeToken.PrintOriginal(); public string DisplayName => @@ -108,6 +109,7 @@ public Type Type { Contract.Ensures(Contract.Result() != null); return type.Normalize(); } + set => type = value; } /// diff --git a/Source/DafnyCore/AST/Grammar/ProgramParser.cs b/Source/DafnyCore/AST/Grammar/ProgramParser.cs index 8c6ea9f3a4e..1d678b6e6b8 100644 --- a/Source/DafnyCore/AST/Grammar/ProgramParser.cs +++ b/Source/DafnyCore/AST/Grammar/ProgramParser.cs @@ -4,10 +4,10 @@ using System.Diagnostics.Contracts; using System.IO; using System.Linq; -using System.Runtime.CompilerServices; using System.Text; using System.Threading; using System.Threading.Tasks; +using CompilerBuilder; using Microsoft.Dafny.Compilers; using Microsoft.Extensions.Logging; using Microsoft.Extensions.Logging.Abstractions; @@ -266,8 +266,24 @@ protected virtual DfyParseResult ParseFile(DafnyOptions options, Func()); - return ParseFile(options, text, uri, cancellationToken); + if (uri.LocalPath.EndsWith(DafnyFile.DafnyFileExtension)) { + var text = SourcePreprocessor.ProcessDirectives(reader, new List()); + return ParseFile(options, text, uri, cancellationToken); + } else if (uri.LocalPath.EndsWith(DafnyFile.VerifiedJavaExtension)) { + var jGrammarBuilder = new JavaGrammar(uri, options); + var javaGrammar = jGrammarBuilder.GetFinalGrammar(); + ConcreteResult result = javaGrammar.ToParser().Parse(reader.ReadToEnd()); + if (result is ConcreteSuccess success) { + return new DfyParseResult(new BatchErrorReporter(options), success.Value, []); + } else { + var failure = (FailureResult)result; + var reporter = new BatchErrorReporter(options); + reporter.Error(MessageSource.Parser, jGrammarBuilder.Convert(failure.Location), failure.Message); + return new DfyParseResult(reporter, new FileModuleDefinition(RangeToken.NoToken), []); + } + } + + throw new NotSupportedException(); } /// diff --git a/Source/DafnyCore/AST/Grammar/TokenExtensions.cs b/Source/DafnyCore/AST/Grammar/TokenExtensions.cs new file mode 100644 index 00000000000..9f4d6537cbf --- /dev/null +++ b/Source/DafnyCore/AST/Grammar/TokenExtensions.cs @@ -0,0 +1,48 @@ +using System.IO; +using Microsoft.Dafny; +using OmniSharp.Extensions.LanguageServer.Protocol.Models; + +namespace Microsoft.Dafny; + + +public interface ICanFormat : INode { + /// Sets the indentation of individual tokens owned by this node, given + /// the new indentation set by the tokens preceding this node + /// Returns if further traverse needs to occur (true) or if it already happened (false) + bool SetIndent(int indentBefore, TokenNewIndentCollector formatter); +} + +public static class TokenExtensions { + + public static RangeToken MakeAutoGenerated(this RangeToken rangeToken) { + return new RangeToken(new AutoGeneratedToken(rangeToken.StartToken), rangeToken.EndToken); + } + + public static RangeToken MakeRefined(this RangeToken rangeToken, ModuleDefinition module) { + return new RangeToken(new RefinementToken(rangeToken.StartToken, module), rangeToken.EndToken); + } + public static Name Prepend(this Name name, string prefix) { + return new Name(name.RangeToken.MakeAutoGenerated(), prefix + name.Value); + } + + public static string TokenToString(this IToken tok, DafnyOptions options) { + if (tok == Token.Cli) { + return "CLI"; + } + + if (tok.Uri == null) { + return $"({tok.line},{tok.col - 1})"; + } + + var currentDirectory = Directory.GetCurrentDirectory(); + string filename = tok.Uri.Scheme switch { + "stdin" => "", + "transcript" => Path.GetFileName(tok.Filepath), + _ => options.UseBaseNameForFileName + ? Path.GetFileName(tok.Filepath) + : (tok.Filepath.StartsWith(currentDirectory) ? Path.GetRelativePath(currentDirectory, tok.Filepath) : tok.Filepath) + }; + + return $"{filename}({tok.line},{tok.col - 1})"; + } +} \ No newline at end of file diff --git a/Source/DafnyCore/AST/Members/Function.cs b/Source/DafnyCore/AST/Members/Function.cs index 3e20e201691..90f5c515bcf 100644 --- a/Source/DafnyCore/AST/Members/Function.cs +++ b/Source/DafnyCore/AST/Members/Function.cs @@ -93,9 +93,9 @@ public TailStatus public bool IsTailRecursive => TailRecursion != TailStatus.NotTailRecursive; public bool IsAccumulatorTailRecursive => IsTailRecursive && TailRecursion != TailStatus.TailRecursive; [FilledInDuringResolution] public bool IsFueled; // if anyone tries to adjust this function's fuel - public readonly Formal Result; + public Formal Result; public PreType ResultPreType; - public readonly Type ResultType; + public Type ResultType; public Type OriginalResultTypeWithRenamings() { if (OverriddenFunction == null) { return ResultType; @@ -225,6 +225,11 @@ void ObjectInvariant() { Contract.Invariant(Decreases != null); } + + public Function() + : base(RangeToken.NoToken, null, false, false, null, false) { + } + public Function(RangeToken range, Name name, bool hasStaticKeyword, bool isGhost, bool isOpaque, List typeArgs, List ins, Formal result, Type resultType, List req, Specification reads, List ens, Specification decreases, diff --git a/Source/DafnyCore/AST/Members/MemberDecl.cs b/Source/DafnyCore/AST/Members/MemberDecl.cs index 4c8a515c46e..b3c0d35c090 100644 --- a/Source/DafnyCore/AST/Members/MemberDecl.cs +++ b/Source/DafnyCore/AST/Members/MemberDecl.cs @@ -16,6 +16,7 @@ public virtual bool IsStatic { get { return HasStaticKeyword || EnclosingClass is DefaultClassDecl; } + set => hasStaticKeyword = value; } public virtual bool IsOpaque => false; diff --git a/Source/DafnyCore/AST/Members/Method.cs b/Source/DafnyCore/AST/Members/Method.cs index e8dd717a039..601b8513448 100644 --- a/Source/DafnyCore/AST/Members/Method.cs +++ b/Source/DafnyCore/AST/Members/Method.cs @@ -34,8 +34,8 @@ static Method() { public readonly bool IsByMethod; public bool MustReverify; public bool IsEntryPoint = false; - public readonly List Outs; - public readonly Specification Mod; + public List Outs; + public Specification Mod; [FilledInDuringResolution] public bool IsRecursive; [FilledInDuringResolution] public bool IsTailRecursive; [FilledInDuringResolution] public Function FunctionFromWhichThisIsByMethodDecl; @@ -119,6 +119,11 @@ void ObjectInvariant() { Contract.Invariant(Decreases != null); } + public Method() + : base(RangeToken.NoToken, null, false, false, null, false) { + Mod = new Specification([], null); + } + public Method(Cloner cloner, Method original) : base(cloner, original) { if (original.Outs != null) { this.Outs = original.Outs.ConvertAll(p => cloner.CloneFormal(p, false)); diff --git a/Source/DafnyCore/AST/Members/MethodOrFunction.cs b/Source/DafnyCore/AST/Members/MethodOrFunction.cs index eef6b372148..2ce2d32d0fe 100644 --- a/Source/DafnyCore/AST/Members/MethodOrFunction.cs +++ b/Source/DafnyCore/AST/Members/MethodOrFunction.cs @@ -17,11 +17,21 @@ static MethodOrFunction() { [FilledInDuringResolution] public bool ContainsHide { get; set; } public readonly List TypeArgs; - public readonly List Req; - public readonly List Ens; + public List Req; + public List Ens; public readonly Specification Decreases; - public readonly List Ins; - + public List Ins; + + protected MethodOrFunction(RangeToken tok, Name name, bool hasStaticKeyword, bool isGhost, Attributes attributes, bool isRefining) + : base(tok, name, hasStaticKeyword, isGhost, attributes, isRefining) { + TypeArgs = []; + Req = []; + Ens = []; + Ins = []; + Decreases = new Specification([], null); + Reads = new Specification([], null); + } + protected MethodOrFunction(RangeToken rangeToken, Name name, bool hasStaticKeyword, bool isGhost, Attributes attributes, bool isRefining, List typeArgs, List ins, List req, @@ -95,8 +105,5 @@ public void ResolveMethodOrFunction(INewOrOldResolver resolver) { // The following check is incomplete, which is a bug. || Ins.Any(f => f.Type.AsSubsetType is not null); - protected MethodOrFunction(RangeToken tok, Name name, bool hasStaticKeyword, bool isGhost, Attributes attributes, bool isRefining) : base(tok, name, hasStaticKeyword, isGhost, attributes, isRefining) { - } - public Specification Reads { get; set; } } \ No newline at end of file diff --git a/Source/DafnyCore/AST/Modules/FileModuleDefinition.cs b/Source/DafnyCore/AST/Modules/FileModuleDefinition.cs index ace0a2e8c94..cd9bb423257 100644 --- a/Source/DafnyCore/AST/Modules/FileModuleDefinition.cs +++ b/Source/DafnyCore/AST/Modules/FileModuleDefinition.cs @@ -10,7 +10,10 @@ namespace Microsoft.Dafny; /// https://github.com/dafny-lang/dafny/issues/3027 /// public class FileModuleDefinition : ModuleDefinition { - public List Includes { get; } = new(); + public List Includes { get; set; } = new(); + + public FileModuleDefinition() : this(Token.Parsing) { + } public FileModuleDefinition(IToken token) : base(token.ToRange(), new Name("_module"), new List(), diff --git a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs index c7da3bee900..a39e95e56e5 100644 --- a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs +++ b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs @@ -64,7 +64,7 @@ public string FullName { public DefaultClassDecl DefaultClass { get; set; } - public readonly List SourceDecls = new(); + public List SourceDecls = new(); [FilledInDuringResolution] public readonly List ResolvedPrefixNamedModules = new(); [FilledInDuringResolution] diff --git a/Source/DafnyCore/AST/Modules/ModuleQualifiedId.cs b/Source/DafnyCore/AST/Modules/ModuleQualifiedId.cs index 4b807d82025..e5273a3522d 100644 --- a/Source/DafnyCore/AST/Modules/ModuleQualifiedId.cs +++ b/Source/DafnyCore/AST/Modules/ModuleQualifiedId.cs @@ -6,7 +6,7 @@ namespace Microsoft.Dafny; public class ModuleQualifiedId : Node, IHasReferences { - public readonly List Path; // Path != null && Path.Count > 0 + public List Path; // Path != null && Path.Count > 0 // The following are filled in during resolution // Note that the root (first path segment) is resolved initially, diff --git a/Source/DafnyCore/AST/Program.cs b/Source/DafnyCore/AST/Program.cs index b46d731cc86..0c76fa51252 100644 --- a/Source/DafnyCore/AST/Program.cs +++ b/Source/DafnyCore/AST/Program.cs @@ -2,6 +2,7 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; using System.Linq; +using System.Threading.Tasks; using Microsoft.Dafny.Auditor; namespace Microsoft.Dafny; @@ -121,6 +122,7 @@ public IToken GetFirstTokenForUri(Uri uri) { public override IEnumerable Children => new[] { DefaultModule }; public override IEnumerable PreResolveChildren => DefaultModuleDef.Includes.Concat(Files); + public Program AfterParsing { get; set; } public override IEnumerable Assumptions(Declaration decl) { return Modules().SelectMany(m => m.Assumptions(decl)); diff --git a/Source/DafnyCore/AST/ShouldCompileOrVerify.cs b/Source/DafnyCore/AST/ShouldCompileOrVerify.cs index c63699e789a..a5f7bb6ec05 100644 --- a/Source/DafnyCore/AST/ShouldCompileOrVerify.cs +++ b/Source/DafnyCore/AST/ShouldCompileOrVerify.cs @@ -31,7 +31,10 @@ public static bool ShouldCompile(this ModuleDefinition module, CompilationData p } } - return program.UrisToCompile.Contains(module.Tok.Uri); + if (!program.UrisToCompile.Contains(module.Tok.Uri)) { + return false; + } + return !module.Tok.FromIncludeDirective(program); } public static bool ShouldVerify(this INode declaration, CompilationData compilation) { diff --git a/Source/DafnyCore/AST/Statements/Assignment/AssignSuchThatStmt.cs b/Source/DafnyCore/AST/Statements/Assignment/AssignSuchThatStmt.cs index 1d1db731578..a6d4a4280dd 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/AssignSuchThatStmt.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/AssignSuchThatStmt.cs @@ -5,6 +5,9 @@ namespace Microsoft.Dafny; +/// +/// Created using ":-" +/// public class AssignSuchThatStmt : ConcreteUpdateStatement, ICloneable, ICanResolveNewAndOld { public readonly Expression Expr; public readonly AttributedToken AssumeToken; diff --git a/Source/DafnyCore/AST/Statements/Assignment/ConcreteUpdateStatement.cs b/Source/DafnyCore/AST/Statements/Assignment/ConcreteUpdateStatement.cs index 159ddb223fa..7dcc406b561 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/ConcreteUpdateStatement.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/ConcreteUpdateStatement.cs @@ -8,7 +8,7 @@ namespace Microsoft.Dafny; /// Common superclass of UpdateStmt, AssignSuchThatStmt and AssignOrReturnStmt /// public abstract class ConcreteUpdateStatement : Statement, ICanFormat { - public readonly List Lhss; + public List Lhss; protected ConcreteUpdateStatement(Cloner cloner, ConcreteUpdateStatement original) : base(cloner, original) { Lhss = original.Lhss.Select(cloner.CloneExpr).ToList(); diff --git a/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs b/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs index e90f93964c2..e98d01a4ac9 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs @@ -6,7 +6,7 @@ namespace Microsoft.Dafny; public class LocalVariable : RangeNode, IVariable, IAttributeBearingDeclaration { - readonly string name; + string name; public string DafnyName => Name; public Attributes Attributes; Attributes IAttributeBearingDeclaration.Attributes => Attributes; @@ -31,6 +31,8 @@ public LocalVariable(Cloner cloner, LocalVariable original) } } + public LocalVariable() : base(RangeToken.NoToken) { } + public LocalVariable(RangeToken rangeToken, string name, Type type, bool isGhost) : base(rangeToken) { Contract.Requires(name != null); @@ -50,6 +52,7 @@ public string Name { Contract.Ensures(Contract.Result() != null); return name; } + set => name = value; } public static bool HasWildcardName(IVariable v) { Contract.Requires(v != null); @@ -84,7 +87,7 @@ public string AssignUniqueName(FreshIdGenerator generator) { compileName ??= SanitizedName; // TODO rename and update comment? Or make it nullable? - public readonly Type SyntacticType; // this is the type mentioned in the declaration, if any + public Type SyntacticType; // this is the type mentioned in the declaration, if any Type IVariable.OptionalType => SyntacticType; [FilledInDuringResolution] @@ -96,6 +99,7 @@ public Type Type { Contract.Assume(type != null); /* we assume object has been resolved */ return type.Normalize(); } + set => type = value; } /// diff --git a/Source/DafnyCore/AST/Statements/Assignment/UpdateStmt.cs b/Source/DafnyCore/AST/Statements/Assignment/UpdateStmt.cs index cc3fe0507f1..0415a02203c 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/UpdateStmt.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/UpdateStmt.cs @@ -5,14 +5,14 @@ namespace Microsoft.Dafny; public class UpdateStmt : ConcreteUpdateStatement, ICloneable, ICanResolve { - public readonly List Rhss; + public List Rhss; public readonly bool CanMutateKnownState; public Expression OriginalInitialLhs = null; public override IToken Tok { get { var firstRhs = Rhss.First(); - if (firstRhs.StartToken != StartToken) { + if (firstRhs.StartToken != StartToken && firstRhs.StartToken.Prev != null) { // If there is an operator, use it as a token return firstRhs.StartToken.Prev; } @@ -21,6 +21,10 @@ public override IToken Tok { } } + public UpdateStmt() : base(RangeToken.NoToken, []) { + + } + [FilledInDuringResolution] public List ResolvedStatements; public override IEnumerable SubStatements => Children.OfType(); diff --git a/Source/DafnyCore/AST/Statements/BlockStmt.cs b/Source/DafnyCore/AST/Statements/BlockStmt.cs index 7cac730b458..0132167baf6 100644 --- a/Source/DafnyCore/AST/Statements/BlockStmt.cs +++ b/Source/DafnyCore/AST/Statements/BlockStmt.cs @@ -1,16 +1,21 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; using System.Linq; +using Microsoft.Boogie; namespace Microsoft.Dafny; public class BlockStmt : Statement, ICloneable, ICanFormat { - public readonly List Body; + public List Body; public BlockStmt Clone(Cloner cloner) { return new BlockStmt(cloner, this); } + public BlockStmt() : base(RangeToken.NoToken) { + + } + protected BlockStmt(Cloner cloner, BlockStmt original) : base(cloner, original) { Body = original.Body.Select(stmt => cloner.CloneStmt(stmt, false)).ToList(); } diff --git a/Source/DafnyCore/AST/Statements/ControlFlow/IfStmt.cs b/Source/DafnyCore/AST/Statements/ControlFlow/IfStmt.cs index 78b9ed3bbaf..a01e34bc37a 100644 --- a/Source/DafnyCore/AST/Statements/ControlFlow/IfStmt.cs +++ b/Source/DafnyCore/AST/Statements/ControlFlow/IfStmt.cs @@ -5,9 +5,9 @@ namespace Microsoft.Dafny; public class IfStmt : Statement, ICloneable, ICanFormat { public readonly bool IsBindingGuard; - public readonly Expression Guard; - public readonly BlockStmt Thn; - public readonly Statement Els; + public Expression Guard; + public BlockStmt Thn; + public Statement Els; [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(!IsBindingGuard || (Guard is ExistsExpr && ((ExistsExpr)Guard).Range == null)); @@ -15,6 +15,8 @@ void ObjectInvariant() { Contract.Invariant(Els == null || Els is BlockStmt || Els is IfStmt || Els is SkeletonStatement); } + public IfStmt() : base(RangeToken.NoToken) { } + public IfStmt Clone(Cloner cloner) { return new IfStmt(cloner, this); } diff --git a/Source/DafnyCore/AST/Statements/ControlFlow/LoopStmt.cs b/Source/DafnyCore/AST/Statements/ControlFlow/LoopStmt.cs index 551a031aaf2..7589e32f40c 100644 --- a/Source/DafnyCore/AST/Statements/ControlFlow/LoopStmt.cs +++ b/Source/DafnyCore/AST/Statements/ControlFlow/LoopStmt.cs @@ -4,8 +4,8 @@ namespace Microsoft.Dafny; public abstract class LoopStmt : Statement, IHasNavigationToken { - public readonly List Invariants; - public readonly Specification Decreases; + public List Invariants; + public Specification Decreases; [FilledInDuringResolution] public bool InferredDecreases; // says that no explicit "decreases" clause was given and an attempt was made to find one automatically (which may or may not have produced anything) public readonly Specification Mod; diff --git a/Source/DafnyCore/AST/Statements/ControlFlow/OneBodyLoopStmt.cs b/Source/DafnyCore/AST/Statements/ControlFlow/OneBodyLoopStmt.cs index 251662cdd18..3386d84a9fb 100644 --- a/Source/DafnyCore/AST/Statements/ControlFlow/OneBodyLoopStmt.cs +++ b/Source/DafnyCore/AST/Statements/ControlFlow/OneBodyLoopStmt.cs @@ -6,7 +6,7 @@ namespace Microsoft.Dafny; public abstract class OneBodyLoopStmt : LoopStmt { - public readonly BlockStmt/*?*/ Body; + public BlockStmt/*?*/ Body; [FilledInDuringResolution] public WhileStmt.LoopBodySurrogate/*?*/ BodySurrogate; // set by Resolver; remains null unless Body==null diff --git a/Source/DafnyCore/AST/Statements/ControlFlow/WhileStmt.cs b/Source/DafnyCore/AST/Statements/ControlFlow/WhileStmt.cs index 8357aa8fc03..a87e3b305bb 100644 --- a/Source/DafnyCore/AST/Statements/ControlFlow/WhileStmt.cs +++ b/Source/DafnyCore/AST/Statements/ControlFlow/WhileStmt.cs @@ -3,7 +3,7 @@ namespace Microsoft.Dafny; public class WhileStmt : OneBodyLoopStmt, ICloneable, ICanFormat { - public readonly Expression/*?*/ Guard; + public Expression/*?*/ Guard; public class LoopBodySurrogate { public readonly List LocalLoopTargets; @@ -15,6 +15,12 @@ public LoopBodySurrogate(List localLoopTargets, bool usesHeap) { } } + public WhileStmt() : base(Dafny.RangeToken.NoToken, [], + new Specification(), + new Specification(), null, null) { + + } + public WhileStmt Clone(Cloner cloner) { return new WhileStmt(cloner, this); } diff --git a/Source/DafnyCore/AST/Statements/Methods/CallStmt.cs b/Source/DafnyCore/AST/Statements/Methods/CallStmt.cs index fc52debc2a6..b4d8ba5eb31 100644 --- a/Source/DafnyCore/AST/Statements/Methods/CallStmt.cs +++ b/Source/DafnyCore/AST/Statements/Methods/CallStmt.cs @@ -29,7 +29,8 @@ void ObjectInvariant() { public Expression Receiver { get { return MethodSelect.Obj; } } public Method Method { get { return (Method)MethodSelect.Member; } } - public CallStmt(RangeToken rangeToken, List lhs, MemberSelectExpr memSel, List args, IToken overrideToken = null) + public CallStmt(RangeToken rangeToken, List lhs, MemberSelectExpr memSel, + List args, IToken overrideToken = null) : base(rangeToken) { Contract.Requires(rangeToken != null); Contract.Requires(cce.NonNullElements(lhs)); diff --git a/Source/DafnyCore/AST/Statements/Verification/AssertStmt.cs b/Source/DafnyCore/AST/Statements/Verification/AssertStmt.cs index 295803e9e6e..ee784cd6aa5 100644 --- a/Source/DafnyCore/AST/Statements/Verification/AssertStmt.cs +++ b/Source/DafnyCore/AST/Statements/Verification/AssertStmt.cs @@ -35,6 +35,9 @@ public AssertStmt(RangeToken rangeToken, Expression expr, BlockStmt/*?*/ proof, Label = label; } + public AssertStmt() : base(RangeToken.NoToken, null) { + } + public override IEnumerable SubStatements { get { if (Proof != null) { diff --git a/Source/DafnyCore/AST/Statements/Verification/PredicateStmt.cs b/Source/DafnyCore/AST/Statements/Verification/PredicateStmt.cs index a8c7717aa5a..cda244c3600 100644 --- a/Source/DafnyCore/AST/Statements/Verification/PredicateStmt.cs +++ b/Source/DafnyCore/AST/Statements/Verification/PredicateStmt.cs @@ -3,7 +3,7 @@ namespace Microsoft.Dafny; public abstract class PredicateStmt : Statement, ICanResolveNewAndOld { - public readonly Expression Expr; + public Expression Expr; [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(Expr != null); diff --git a/Source/DafnyCore/AST/SystemModuleManager.cs b/Source/DafnyCore/AST/SystemModuleManager.cs index d7d946b7b2d..f1b4f5813cd 100644 --- a/Source/DafnyCore/AST/SystemModuleManager.cs +++ b/Source/DafnyCore/AST/SystemModuleManager.cs @@ -16,7 +16,7 @@ public class SystemModuleManager { public readonly Dictionary ArrowTypeDecls = new(); public readonly Dictionary PartialArrowTypeDecls = new(); // same keys as arrowTypeDecl public readonly Dictionary TotalArrowTypeDecls = new(); // same keys as arrowTypeDecl - readonly Dictionary, TupleTypeDecl> tupleTypeDecls = new(new Dafny.IEnumerableComparer()); + readonly Dictionary, TupleTypeDecl> tupleTypeDecls = new(new IEnumerableComparer()); internal readonly ValuetypeDecl[] valuetypeDecls; diff --git a/Source/DafnyCore/AST/TypeDeclarations/ClassDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/ClassDecl.cs index e4d9677aa12..2a48f5fc5b0 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/ClassDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/ClassDecl.cs @@ -1,5 +1,6 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; +using Newtonsoft.Json.Serialization; namespace Microsoft.Dafny; @@ -15,6 +16,11 @@ void ObjectInvariant() { Contract.Invariant(ParentTraits != null); } + public ClassDecl() + : base(null, null, null, [], new(), null, false, null) + { + } + public ClassDecl(RangeToken rangeToken, Name name, ModuleDefinition module, List typeArgs, [Captured] List members, Attributes attributes, bool isRefining, List/*?*/ traits) : base(rangeToken, name, module, typeArgs, members, attributes, isRefining, traits) { diff --git a/Source/DafnyCore/AST/TypeDeclarations/TopLevelDeclWithMembers.cs b/Source/DafnyCore/AST/TypeDeclarations/TopLevelDeclWithMembers.cs index 52c691164ac..c12612fc5c0 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/TopLevelDeclWithMembers.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/TopLevelDeclWithMembers.cs @@ -8,7 +8,7 @@ namespace Microsoft.Dafny; public abstract class TopLevelDeclWithMembers : TopLevelDecl, IHasSymbolChildren { - public readonly List Members; + public List Members; // TODO remove this and instead clone the AST after parsing. public ImmutableList MembersBeforeResolution; diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index 7c9eaa7c000..09abe6d1cb6 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -219,8 +219,8 @@ Dafny Uri parsedFile = scanner.Uri; bool isVerbatimString; string includedFile = Util.RemoveParsedStringQuotes(t.val, out isVerbatimString); - Util.ValidateEscaping(theOptions, t, includedFile, isVerbatimString, errors); - includedFile = Util.RemoveEscaping(theOptions, includedFile, isVerbatimString); + DafnyUtils.ValidateEscaping(theOptions, t, includedFile, isVerbatimString, errors); + includedFile = DafnyUtils.RemoveEscaping(theOptions, includedFile, isVerbatimString); if (!Path.IsPathRooted(includedFile)) { string basePath = parsedFile.Scheme == "stdin" ? "" : Path.GetDirectoryName(parsedFile.LocalPath); includedFile = Path.Combine(basePath, includedFile); @@ -1324,8 +1324,8 @@ ModifiesClause<.ref List mod, ref Attributes attrs, mod = mod ?? new List(); .) { Attribute } - FrameExpression (. Util.AddFrameExpression(mod, fe, performThisDeprecatedCheck, errors); .) - { "," FrameExpression (. Util.AddFrameExpression(mod, fe, performThisDeprecatedCheck, errors); .) + FrameExpression (. DafnyUtils.AddFrameExpression(mod, fe, performThisDeprecatedCheck, errors); .) + { "," FrameExpression (. DafnyUtils.AddFrameExpression(mod, fe, performThisDeprecatedCheck, errors); .) } OldSemi . @@ -3713,14 +3713,14 @@ LiteralExpression | Nat (. e = new LiteralExpr(t, n); .) | Dec (. e = new LiteralExpr(t, d); .) | charToken (. string s = t.val.Substring(1, t.val.Length - 2); - Util.ValidateEscaping(theOptions, t, s, false, errors); - if (Util.UnescapedCharacters(theOptions, s, false).Count() > 1) { + DafnyUtils.ValidateEscaping(theOptions, t, s, false, errors); + if (DafnyUtils.UnescapedCharacters(theOptions, s, false).Count() > 1) { errors.SemErr(ErrorId.p_invalid_char_literal, t, "too many characters in character literal"); } e = new CharLiteralExpr(t, s); .) | stringToken (. bool isVerbatimString; string s = Util.RemoveParsedStringQuotes(t.val, out isVerbatimString); - Util.ValidateEscaping(theOptions, t, s, isVerbatimString, errors); + DafnyUtils.ValidateEscaping(theOptions, t, s, isVerbatimString, errors); e = new StringLiteralExpr(t, s, isVerbatimString); .) ) (. e.RangeToken = new RangeToken(t, t); .) diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj index a7f2c8eb1fe..19243f411e1 100644 --- a/Source/DafnyCore/DafnyCore.csproj +++ b/Source/DafnyCore/DafnyCore.csproj @@ -17,7 +17,7 @@ true ..\..\Binaries\ TRACE - net6.0 + net8.0 Major MIT @@ -49,6 +49,7 @@ + diff --git a/Source/DafnyCore/DafnyFile.cs b/Source/DafnyCore/DafnyFile.cs index d0e2b404cd2..a403c78fcc6 100644 --- a/Source/DafnyCore/DafnyFile.cs +++ b/Source/DafnyCore/DafnyFile.cs @@ -16,6 +16,7 @@ namespace Microsoft.Dafny; public class DafnyFile { public const string DafnyFileExtension = ".dfy"; + public const string VerifiedJavaExtension = ".vjava"; public string FilePath => CanonicalPath; public string Extension { get; private set; } public string CanonicalPath { get; } @@ -74,7 +75,7 @@ public static async IAsyncEnumerable CreateAndValidate(IFileSystem fi extension = DafnyFileExtension; } - if (uri.Scheme == "untitled" || extension == DafnyFileExtension || extension == ".dfyi") { + if (uri.Scheme == "untitled" || extension == DafnyFileExtension || extension == VerifiedJavaExtension || extension == ".dfyi") { var file = HandleDafnyFile(fileSystem, reporter, options, uri, uriOrigin, asLibrary); if (file != null) { yield return file; diff --git a/Source/DafnyCore/DafnyMain.cs b/Source/DafnyCore/DafnyMain.cs index 4074baaf226..2c2dc32a459 100644 --- a/Source/DafnyCore/DafnyMain.cs +++ b/Source/DafnyCore/DafnyMain.cs @@ -53,6 +53,8 @@ public static void MaybePrintProgram(Program program, string filename, bool afte return (program, err); } + var cloner = new Cloner(true); + program.AfterParsing = new Program(cloner, program); return (program, Resolve(program)); } diff --git a/Source/DafnyCore/Generic/NodeExtensions.cs b/Source/DafnyCore/Generic/DafnyNodeExtensions.cs similarity index 54% rename from Source/DafnyCore/Generic/NodeExtensions.cs rename to Source/DafnyCore/Generic/DafnyNodeExtensions.cs index 08f5a17187a..e9b248cf972 100644 --- a/Source/DafnyCore/Generic/NodeExtensions.cs +++ b/Source/DafnyCore/Generic/DafnyNodeExtensions.cs @@ -1,20 +1,16 @@ using System; using System.Collections.Generic; -using System.Linq; -using System.Reflection.Metadata.Ecma335; using System.Text.RegularExpressions; +using Microsoft.Dafny; namespace Microsoft.Dafny; -public interface IHasDocstring { - /// - /// Unfiltered version that only returns the trivia containing the docstring - /// - public string GetTriviaContainingDocstring(); -} - -public static class NodeExtensions { - +public static class DafnyNodeExtensions { + + public static Expression WrapExpression(Expression expr) { + return Expression.CreateParensExpression(new AutoGeneratedToken(expr.tok), expr); + } + /// /// // Applies plugin-defined docstring filters /// @@ -92,81 +88,4 @@ private static string ExtractDocstring(string trivia) { return string.Join("\n", rawDocstring); } - - public static IEnumerable Descendants(this INode node) { - return node.Children.Concat(node.Children.SelectMany(n => n.Descendants())); - } - - public static T FindNode(this INode root, Uri uri, DafnyPosition position) { - return (T)root.FindNodeChain(uri, position, null, node => node is T)?.Data; - } - - public static INode FindNode(this INode node, Uri uri, DafnyPosition position, Func predicate) { - return node.FindNodeChain(uri, position, null, predicate)?.Data; - } - - public static IEnumerable FindNodesInUris(this INode node, Uri uri) { - return node.FindNodeChainsInUri(uri, null).Select(c => c.Data); - } - - public static IEnumerable> FindNodeChainsInUri(this INode node, Uri uri, LList parent) { - if (node.RangeToken.Uri != null) { - if (node.RangeToken.Uri == uri) { - return new[] { new LList(node, parent) }; - } - - return new LList[] { }; - } - - var newParent = new LList(node, parent); - return node.Children.SelectMany(child => child.FindNodeChainsInUri(uri, newParent)); - } - - private static LList FindNodeChain(this INode node, Uri uri, DafnyPosition position, LList parent, - Func predicate) { - if (node.RangeToken.Uri != null) { - if (node.RangeToken.Uri == uri) { - return node.FindNodeChain(position, parent, predicate); - } - - if (node.SingleFileToken) { - return null; - } - } - - var newParent = new LList(node, parent); - foreach (var child in node.Children) { - var result = child.FindNodeChain(uri, position, newParent, predicate); - if (result != null) { - return result; - } - } - - return null; - } - - public static LList FindNodeChain(this INode node, DafnyPosition position, Func predicate) { - return FindNodeChain(node, position, new LList(node, null), predicate); - } - - private static LList FindNodeChain(this INode node, DafnyPosition position, LList parent, - Func predicate) { - if (node.Tok is AutoGeneratedToken || (node.Tok != Token.NoToken && !node.RangeToken.ToDafnyRange().Contains(position))) { - return null; - } - - var newParent = new LList(node, parent); - foreach (var child in node.Children) { - var result = child.FindNodeChain(position, newParent, predicate); - if (result != null) { - return result; - } - } - - if (node.Tok == Token.NoToken || !predicate(node)) { - return null; - } - - return new LList(node, parent); - } } \ No newline at end of file diff --git a/Source/DafnyCore/Generic/DafnyUtils.cs b/Source/DafnyCore/Generic/DafnyUtils.cs new file mode 100644 index 00000000000..9270ce29db6 --- /dev/null +++ b/Source/DafnyCore/Generic/DafnyUtils.cs @@ -0,0 +1,347 @@ +using System; +using System.Collections; +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.IO; +using System.Linq; +using System.Text; +using System.Text.RegularExpressions; +using Microsoft.Dafny; + +using static Microsoft.Dafny.GenericErrors; + +namespace Microsoft.Dafny; + +public static class DafnyUtils { + + + /// + /// Replaced any escaped characters in s by the actual character that the escaping represents. + /// Assumes s to be a well-parsed string. + /// + public static string RemoveEscaping(DafnyOptions options, string s, bool isVerbatimString) { + Contract.Requires(s != null); + var sb = new StringBuilder(); + if (options.Get(CommonOptionBag.UnicodeCharacters)) { + foreach (var ch in UnescapedCharacters(options, s, isVerbatimString)) { + sb.Append(new Rune(ch)); + } + } else { + foreach (var ch in UnescapedCharacters(options, s, isVerbatimString)) { + sb.Append((char)ch); + } + } + return sb.ToString(); + } + + public static IEnumerable UnescapedCharacters(DafnyOptions options, string p, bool isVerbatimString) { + return Util.UnescapedCharacters(options.Get(CommonOptionBag.UnicodeCharacters), p, isVerbatimString); + } + + public static void ValidateEscaping(DafnyOptions options, IToken t, string s, bool isVerbatimString, Errors errors) { + if (options.Get(CommonOptionBag.UnicodeCharacters)) { + foreach (var token in Util.TokensWithEscapes(s, isVerbatimString)) { + if (token.StartsWith("\\u")) { + errors.SemErr(ErrorId.g_no_old_unicode_char, t, "\\u escape sequences are not permitted when Unicode chars are enabled"); + } + + if (token.StartsWith("\\U")) { + var hexDigits = Util.RemoveUnderscores(token[3..^1]); + if (hexDigits.Length > 6) { + errors.SemErr(ErrorId.g_unicode_escape_must_have_six_digits, t, "\\U{X..X} escape sequence must have at most six hex digits"); + } else { + var codePoint = Convert.ToInt32(hexDigits, 16); + if (codePoint >= 0x11_0000) { + errors.SemErr(ErrorId.g_unicode_escape_is_too_large, t, "\\U{X..X} escape sequence must be less than 0x110000"); + } + if (codePoint is >= 0xD800 and < 0xE000) { + errors.SemErr(ErrorId.g_unicode_escape_may_not_be_surrogate, t, "\\U{X..X} escape sequence must not be a surrogate"); + } + } + } + } + } else { + foreach (var token2 in Util.TokensWithEscapes(s, isVerbatimString)) { + if (token2.StartsWith("\\U")) { + errors.SemErr(ErrorId.g_U_unicode_chars_are_disallowed, t, "\\U escape sequences are not permitted when Unicode chars are disabled"); + } + } + } + } + + /// + /// Converts a hexadecimal digit to an integer. + /// Assumes ch does represent a hexadecimal digit; alphabetic digits can be in either case. + /// + public static int HexValue(char ch) { + if ('a' <= ch && ch <= 'f') { + return ch - 'a' + 10; + } else if ('A' <= ch && ch <= 'F') { + return ch - 'A' + 10; + } else { + return ch - '0'; + } + } + + /// + /// Add "fe" to "mod", if "performThisDeprecationCheck" is "false". + /// Otherwise, first strip "fe" of certain easy occurrences of "this", and for each one giving a warning about + /// that "this" is deprecated in modifies clauses of constructors. + /// This method may modify "fe" and the subexpressions contained within "fe". + /// + public static void AddFrameExpression(List mod, FrameExpression fe, bool performThisDeprecationCheck, Errors errors) { + Contract.Requires(mod != null); + Contract.Requires(fe != null); + Contract.Requires(errors != null); + if (performThisDeprecationCheck) { + if (fe.E is ThisExpr) { + errors.Deprecated(ErrorId.g_deprecated_this_in_constructor_modifies_clause, fe.E.tok, "constructors no longer need 'this' to be listed in modifies clauses"); + return; + } else if (fe.E is SetDisplayExpr) { + var s = (SetDisplayExpr)fe.E; + var deprecated = s.Elements.FindAll(e => e is ThisExpr); + if (deprecated.Count != 0) { + foreach (var e in deprecated) { + errors.Deprecated(ErrorId.g_deprecated_this_in_constructor_modifies_clause, e.tok, "constructors no longer need 'this' to be listed in modifies clauses"); + } + s.Elements.RemoveAll(e => e is ThisExpr); + if (s.Elements.Count == 0) { + return; + } + } + } + } + mod.Add(fe); + } + + static Graph BuildFunctionCallGraph(Program program) { + Graph functionCallGraph = new Graph(); + FunctionCallFinder callFinder = new FunctionCallFinder(); + + foreach (var module in program.Modules()) { + foreach (var decl in module.TopLevelDecls) { + if (decl is TopLevelDeclWithMembers c) { + foreach (var member in c.Members) { + if (member is Function f) { + List calls = new List(); + foreach (var e in f.Reads.Expressions) { if (e != null && e.E != null) { callFinder.Visit(e.E, calls); } } + foreach (var e in f.Req) { if (e != null) { callFinder.Visit(e, calls); } } + foreach (var e in f.Ens) { if (e != null) { callFinder.Visit(e, calls); } } + if (f.Body != null) { + callFinder.Visit(f.Body, calls); + } + + foreach (var callee in calls) { + functionCallGraph.AddEdge(f, callee); + } + } + } + } + } + } + + return functionCallGraph; + } + + /// + /// Prints the program's function call graph in a format suitable for consumption in other tools + /// + public static void PrintFunctionCallGraph(Program program) { + var functionCallGraph = BuildFunctionCallGraph(program); + + foreach (var vertex in functionCallGraph.GetVertices()) { + var func = vertex.N; + program.Options.OutputWriter.Write("{0},{1}=", func.SanitizedName, func.EnclosingClass.EnclosingModuleDefinition.SanitizedName); + foreach (var callee in vertex.Successors) { + program.Options.OutputWriter.Write("{0} ", callee.N.SanitizedName); + } + program.Options.OutputWriter.Write("\n"); + } + } + + /// + /// Compute various interesting statistics about the Dafny program + /// + public static void PrintStats(Program program) { + SortedDictionary stats = new SortedDictionary(); + + foreach (var module in program.Modules()) { + IncrementStat(stats, "Modules"); + UpdateMax(stats, "Module height (max)", (ulong)module.Height); + + ulong num_scc = (ulong)module.CallGraph.TopologicallySortedComponents().Count; + UpdateMax(stats, "Call graph width (max)", num_scc); + + foreach (var decl in module.TopLevelDecls) { + if (decl is DatatypeDecl) { + IncrementStat(stats, "Datatypes"); + } else if (decl is ClassLikeDecl) { + var c = (ClassLikeDecl)decl; + if (c.Name != "_default") { + IncrementStat(stats, "Classes"); + } + + foreach (var member in c.Members) { + if (member is Function) { + IncrementStat(stats, "Functions (total)"); + var f = (Function)member; + if (f.IsRecursive) { + IncrementStat(stats, "Functions recursive"); + } + } else if (member is Method) { + IncrementStat(stats, "Methods (total)"); + var method = (Method)member; + if (method.IsRecursive) { + IncrementStat(stats, "Methods recursive"); + } + if (method.IsGhost) { + IncrementStat(stats, "Methods ghost"); + } + } + } + } + } + } + + // Print out the results, with some nice formatting + program.Options.OutputWriter.WriteLine(""); + program.Options.OutputWriter.WriteLine("Statistics"); + program.Options.OutputWriter.WriteLine("----------"); + + int max_key_length = 0; + foreach (var key in stats.Keys) { + if (key.Length > max_key_length) { + max_key_length = key.Length; + } + } + + foreach (var keypair in stats) { + string keyString = keypair.Key.PadRight(max_key_length + 2); + program.Options.OutputWriter.WriteLine("{0} {1,4}", keyString, keypair.Value); + } + } + /// + /// Generic statistic counter + /// + static void IncrementStat(IDictionary stats, string stat) { + if (stats.TryGetValue(stat, out var currentValue)) { + stats[stat] += 1; + } else { + stats.Add(stat, 1); + } + } + + /// + /// Track the maximum value of some statistic + /// + static void UpdateMax(IDictionary stats, string stat, ulong val) { + if (stats.TryGetValue(stat, out var currentValue)) { + if (val > currentValue) { + stats[stat] = val; + } + } else { + stats.Add(stat, val); + } + } + + public static IEnumerable Lines(TextReader reader) { + return new LinesEnumerable(reader); + } +} + +/// +/// Class dedicated to traversing the function call graph +/// +class FunctionCallFinder : TopDownVisitor> { + protected override bool VisitOneExpr(Expression expr, ref List calls) { + if (expr is FunctionCallExpr) { + calls.Add(((FunctionCallExpr)expr).Function); + } + return true; + } +} + +class LinesEnumerable : IEnumerable { + private readonly TextReader Reader; + + public LinesEnumerable(TextReader reader) { + Reader = reader; + } + + public IEnumerator GetEnumerator() { + return new LinesEnumerator(Reader); + } + + IEnumerator IEnumerable.GetEnumerator() { + return GetEnumerator(); + } +} + +class LinesEnumerator : IEnumerator { + + private readonly TextReader Reader; + + public LinesEnumerator(TextReader reader) { + Reader = reader; + } + + public bool MoveNext() { + Current = Reader.ReadLine(); + return Current != null; + } + + public void Reset() { + throw new NotImplementedException(); + } + + public string Current { get; internal set; } + + object IEnumerator.Current => Current; + + public void Dispose() { + } +} + +public class DependencyMap { + private Dictionary> dependencies; + + public DependencyMap() { + dependencies = new Dictionary>(); + } + + public void AddInclude(Include include) { + SortedSet existingDependencies = null; + string key = include.IncluderFilename.LocalPath ?? "roots"; + bool found = dependencies.TryGetValue(key, out existingDependencies); + if (found) { + existingDependencies.Add(include.CanonicalPath); + } else { + dependencies[key] = new SortedSet() { include.CanonicalPath }; + } + } + + public void AddIncludes(IEnumerable includes) { + // Reconstruct the dependency map + Dictionary> dependencies = new Dictionary>(); + foreach (Include include in includes) { + AddInclude(include); + } + } + + public void PrintMap(DafnyOptions options) { + SortedSet leaves = new SortedSet(); // Files that don't themselves include any files + foreach (string target in dependencies.Keys) { + options.OutputWriter.Write(target); + foreach (string dependency in dependencies[target]) { + options.OutputWriter.Write(";" + dependency); + if (!dependencies.ContainsKey(dependency)) { + leaves.Add(dependency); + } + } + options.OutputWriter.WriteLine(); + } + foreach (string leaf in leaves) { + options.OutputWriter.WriteLine(leaf); + } + } +} \ No newline at end of file diff --git a/Source/DafnyCore/Generic/Name.cs b/Source/DafnyCore/Generic/Name.cs index adee7f15212..4face8b4f49 100644 --- a/Source/DafnyCore/Generic/Name.cs +++ b/Source/DafnyCore/Generic/Name.cs @@ -11,10 +11,6 @@ namespace Microsoft.Dafny; /// public class Name : RangeNode { - public Name Prepend(string prefix) { - return new Name(RangeToken.MakeAutoGenerated(), prefix + Value); - } - public Name Append(string suffix) { return new Name(RangeToken, Value + suffix); } @@ -42,9 +38,13 @@ public Name(string value) : base(RangeToken.NoToken) { public override IEnumerable Children => Enumerable.Empty(); public override IEnumerable PreResolveChildren => Children; - public Name Clone(Cloner cloner) { + public Name Clone(ICloner cloner) { return new Name(cloner.Tok(RangeToken), Value); } public override string ToString() => Value; +} + +public interface ICloner { + RangeToken Tok(RangeToken rangeToken); } \ No newline at end of file diff --git a/Source/DafnyCore/Generic/Node.cs b/Source/DafnyCore/Generic/Node.cs index 4567eaa2bfd..35d08133c28 100644 --- a/Source/DafnyCore/Generic/Node.cs +++ b/Source/DafnyCore/Generic/Node.cs @@ -4,30 +4,10 @@ using System.Diagnostics.Contracts; using System.Linq; using System.Text.RegularExpressions; -using Microsoft.Boogie; using Microsoft.Dafny.Auditor; namespace Microsoft.Dafny; -public interface INode { - bool SingleFileToken { get; } - public IToken StartToken => RangeToken.StartToken; - public IToken EndToken => RangeToken.EndToken; - IEnumerable OwnedTokens { get; } - RangeToken RangeToken { get; } - IToken Tok { get; } - IEnumerable Children { get; } - IEnumerable PreResolveChildren { get; } -} - -public interface ICanFormat : INode { - /// Sets the indentation of individual tokens owned by this node, given - /// the new indentation set by the tokens preceding this node - /// Returns if further traverse needs to occur (true) or if it already happened (false) - bool SetIndent(int indentBefore, TokenNewIndentCollector formatter); -} - - public abstract class Node : INode { private static readonly Regex StartDocstringExtractor = new Regex($@"/\*\*(?{TriviaFormatterHelper.MultilineCommentContent})\*/"); @@ -201,7 +181,7 @@ public abstract class TokenNode : Node { // Contains tokens that did not make it in the AST but are part of the expression, // Enables ranges to be correct. // TODO: Re-add format tokens where needed until we put all the formatting to replace the tok of every expression - internal IToken[] FormatTokens = null; + public IToken[] FormatTokens = null; protected RangeToken rangeToken = null; @@ -247,7 +227,9 @@ void UpdateStartEndTokRecursive(INode node) { } } - PreResolveChildren.ForEach(UpdateStartEndTokRecursive); + foreach (var child in PreResolveChildren) { + UpdateStartEndTokRecursive(child); + } if (FormatTokens != null) { foreach (var token in FormatTokens) { @@ -280,4 +262,4 @@ protected RangeNode(Cloner cloner, RangeNode original) { protected RangeNode(RangeToken rangeToken) { RangeToken = rangeToken; } -} +} \ No newline at end of file diff --git a/Source/DafnyCore/Generic/ProgramTraverser.cs b/Source/DafnyCore/Generic/ProgramTraverser.cs new file mode 100644 index 00000000000..56f2e0d1a09 --- /dev/null +++ b/Source/DafnyCore/Generic/ProgramTraverser.cs @@ -0,0 +1,289 @@ +using System.Collections.Generic; +using System.Linq; +using JetBrains.Annotations; +using Microsoft.Dafny; + +namespace Microsoft.Dafny; + +// Class to traverse a program top-down, especially aimed at identifying expressions and statements, +// and in their context +// How to use: +// - Define a subclass of ProgramTraverser +// - Implement the methods (TopDown|BottomUp)(Enter|Exit), override Traverse if needed. +// - Call any Traverse() method. +public class ProgramTraverser { + public enum ContinuationStatus { + Ok, // Continue exploration + Skip, // Skip this node and its descendants (valid only on entering a node) + Stop, // Stop the entire traversal here, but traverse ancestors in bottom-up + } + protected const ContinuationStatus ok = ContinuationStatus.Ok; + protected const ContinuationStatus skip = ContinuationStatus.Skip; + protected const ContinuationStatus stop = ContinuationStatus.Stop; + // Returns true if statement needs to be traversed + protected virtual ContinuationStatus OnEnter(Statement stmt, [CanBeNull] string field, [CanBeNull] object parent) { + return ok; + } + // Returns true if expression needs to be traversed + protected virtual ContinuationStatus OnEnter(Expression expr, [CanBeNull] string field, [CanBeNull] object parent) { + return ok; + } + + // Returns true if need to stop the traversal entirely + protected virtual bool OnExit(Statement stmt, [CanBeNull] string field, [CanBeNull] object parent) { + return false; + } + // Returns true if need to stop the traversal entirely + protected virtual bool OnExit(Expression expr, [CanBeNull] string field, [CanBeNull] object parent) { + return false; + } + + protected virtual ContinuationStatus OnEnter(MemberDecl memberDecl, [CanBeNull] string field, [CanBeNull] object parent) { + return ok; + } + + // Traverse methods retun true to interrupt. + public bool Traverse(Program program) { + if (program == null) { + return false; + } + + return program.Modules().Any(Traverse); + } + + public bool Traverse(ModuleDefinition moduleDefinition) { + if (moduleDefinition == null) { + return false; + } + + return Traverse(moduleDefinition.TopLevelDecls); + } + + public bool Traverse(IEnumerable topLevelDecls) { + if (topLevelDecls == null) { + return false; + } + + foreach (var topLevelDecl in topLevelDecls) { + if (Traverse(topLevelDecl)) { + return true; + } + } + + return false; + } + + public bool Traverse(ModuleDecl moduleDecl) { + if (moduleDecl == null) { + return false; + } + + if (moduleDecl is LiteralModuleDecl l) { + return Traverse(l.ModuleDef); + } else if (moduleDecl is AbstractModuleDecl a) { + return Traverse(a.CompileRoot); + }/* else if (moduleDecl is AliasModuleDecl a) { + + } else if (moduleDecl is ModuleExportDecl m) { + + }*/ + + return false; + } + + public bool Traverse(Formal formal) { + if (formal == null) { + return false; + } + + if (formal.DefaultValue != null && Traverse(formal.DefaultValue, "DefaultValue", formal)) { + return true; + } + + return false; + } + + public bool Traverse(DatatypeCtor ctor) { + if (ctor == null) { + return false; + } + + if (ctor.Formals.Any(Traverse)) { + return true; + } + + return false; + } + + public bool Traverse(TopLevelDecl topd) { + if (topd == null) { + return false; + } + + var d = topd is ClassLikeDecl classDecl && classDecl.NonNullTypeDecl != null ? classDecl.NonNullTypeDecl : topd; + + if (d is TopLevelDeclWithMembers tdm) { + // ClassDecl, DatatypeDecl, AbstractTypeDecl, NewtypeDecl + if (tdm.Members.Any(memberDecl => Traverse(memberDecl, "Members", tdm))) { + return true; + } + + if (tdm is IteratorDecl iter) { + // TODO: Import this + if (Attributes.SubExpressions(iter.Attributes).Any(e => Traverse(e, "Attributes.SubExpressions", iter))) { + return true; + } + if (Attributes.SubExpressions(iter.Reads.Attributes).Any(e => Traverse(e, "Reads.Attributes.SubExpressions", iter))) { + return true; + } + if (iter.Reads.Expressions.Any(e => Traverse(e.E, "Reads.Expressions.E", iter))) { + return true; + } + if (Attributes.SubExpressions(iter.Modifies.Attributes).Any(e => Traverse(e, "Modifies.Attributes.SubExpressions", iter))) { + return true; + } + if (iter.Modifies.Expressions.Any(e => Traverse(e.E, "Modifies.Expressions.E", iter))) { + return true; + } + if (Attributes.SubExpressions(iter.Decreases.Attributes).Any(e => Traverse(e, "Decreases.Attributes.SubExpressions", iter))) { + return true; + } + if (iter.Decreases.Expressions.Any(e => Traverse(e, "Decreases.Expressions.E", iter))) { + return true; + } + if (iter.Requires.Any(e => Traverse(e.E, "Requires.E", iter))) { + return true; + } + if (iter.Ensures.Any(e => Traverse(e.E, "Ensures.E", iter))) { + return true; + } + if (iter.YieldRequires.Any(e => Traverse(e.E, "YieldRequires.E", iter))) { + return true; + } + if (iter.YieldEnsures.Any(e => Traverse(e.E, "YieldEnsures.E", iter))) { + return true; + } + if (Traverse(iter.Body, "Body", iter)) { + return true; + } + } + + if (tdm is DatatypeDecl dtd) { + if (dtd.Ctors.Any(Traverse)) { + return true; + } + } + } else if (d is ModuleDecl md) { + return Traverse(md); + } else if (d is TypeSynonymDecl tsd) { + // Nothing here. + } + + return false; + } + + public bool Traverse(MemberDecl memberDeclaration, [CanBeNull] string field, [CanBeNull] object parent) { + if (memberDeclaration == null) { + return false; + } + + var enterResult = OnEnter(memberDeclaration, field, parent); + if (enterResult is stop or skip) { + return enterResult == stop; + } + + if (memberDeclaration is Field fi) { + if (fi.SubExpressions.Any(expr => Traverse(expr, "SubExpressions", fi))) { + return true; + } + } else if (memberDeclaration is Function f) { + if (f.Ins.Any(Traverse)) { + return true; + } + if (f.Result != null && f.Result.DefaultValue != null && Traverse(f.Result.DefaultValue, "Result.DefaultValue", f)) { + return true; + } + if (f.Req.Any(e => Traverse(e.E, "Req.E", f))) { + return true; + } + if (f.Reads.Expressions.Any(e => Traverse(e.E, "Reads.E", f))) { + return true; + } + if (f.Ens.Any(e => Traverse(e.E, "Ens.E", f))) { + return true; + } + if (f.Decreases.Expressions.Any(e => Traverse(e, "Decreases.Expressions", f))) { + return true; + } + if (Traverse(f.Body, "Body", f)) { + return true; + } + + if (f.ByMethodDecl != null && Traverse(f.ByMethodDecl, "ByMethodDecl", f)) { + return true; + } + + if (f.ByMethodDecl == null || f.ByMethodDecl.Body != f.ByMethodBody) { + if (f.ByMethodBody != null && Traverse(f.ByMethodBody, "ByMethodBody", f)) { + return true; + } + } + } else if (memberDeclaration is Method m) { + // For example, default value of formals is non-ghost + if (m.Ins.Any(formal => formal.DefaultValue != null + && Traverse(formal.DefaultValue, "Ins.DefaultValue", m))) { + return true; + } + if (m.Req.Any(e => Traverse(e.E, "Req.E", m))) { + return true; + } + if (m.Reads.Expressions.Any(e => Traverse(e.E, "Reads.E", m))) { + return true; + } + if (m.Mod.Expressions.Any(e => Traverse(e.E, "Mod.E", m) == true)) { + return true; + } + if (m.Ens.Any(e => Traverse(e.E, "Ens.E", m))) { + return true; + } + if (m.Decreases.Expressions.Any(e => Traverse(e, "Decreases.Expressions", m))) { + return true; + } + if (Traverse(m.Body, "Body", m)) { + return true; + } + } + + return false; + } + + public virtual bool Traverse(Statement stmt, [CanBeNull] string field, [CanBeNull] object parent) { + if (stmt == null) { + return false; + } + + var enterResult = OnEnter(stmt, field, parent); + if (enterResult is stop or skip) { + return enterResult == stop; + } + + return stmt.NonSpecificationSubExpressions.Any(subExpr => Traverse(subExpr, "NonSpecificationSubExpressions", stmt)) || + stmt.SpecificationSubExpressions.Any(subExpr => Traverse(subExpr, "SpecificationSubExpressions", stmt)) || + stmt.SubStatements.Any(subStmt => Traverse(subStmt, "SubStatements", stmt)) || + OnExit(stmt, field, parent); + } + + public virtual bool Traverse(Expression expr, [CanBeNull] string field, [CanBeNull] object parent) { + if (expr == null) { + return false; + } + + var enterResult = OnEnter(expr, field, parent); + if (enterResult is stop or skip) { + return enterResult == stop; + } + + return expr.SubExpressions.Any(subExpr => Traverse(subExpr, "SubExpression", expr)) || + OnExit(expr, field, parent); + } +} \ No newline at end of file diff --git a/Source/DafnyCore/Generic/SinglyLinkedList.cs b/Source/DafnyCore/Generic/SinglyLinkedList.cs deleted file mode 100644 index 0e77c90f74e..00000000000 --- a/Source/DafnyCore/Generic/SinglyLinkedList.cs +++ /dev/null @@ -1,80 +0,0 @@ -using System; -using System.Collections; -using System.Collections.Generic; -using System.Linq; - -namespace Microsoft.Dafny; - -class LinkedListEnumerator : IEnumerator { - private Cons list; - - public LinkedListEnumerator(Cons list) { - this.list = new Cons(default, list); - } - - public bool MoveNext() { - if (list.Tail is Cons tailCons) { - list = tailCons; - return true; - } - - return false; - } - - public void Reset() { - throw new System.NotSupportedException(); - } - - public T Current => list.Head; - - object IEnumerator.Current => Current; - - public void Dispose() { - } -} - -public abstract record SinglyLinkedList : IEnumerable { - public abstract IEnumerator GetEnumerator(); - IEnumerator IEnumerable.GetEnumerator() { - return GetEnumerator(); - } - - public bool Any() { - return this is not Nil; - } -} - -public static class LinkedLists { - public static SinglyLinkedList Concat(SinglyLinkedList left, SinglyLinkedList right) { - return left switch { - Nil => right, - Cons cons => new Cons(cons.Head, Concat(cons.Tail, right)), - _ => throw new ArgumentOutOfRangeException(nameof(left)) - }; - } - - - public static SinglyLinkedList FromList(IReadOnlyList values, SinglyLinkedList tail = null) { - SinglyLinkedList result = tail ?? new Nil(); - for (int i = values.Count - 1; i >= 0; i--) { - result = new Cons(values[i], result); - } - return result; - } - - public static SinglyLinkedList Create(params T[] values) { - return FromList(values); - } -} - -public record Cons(T Head, SinglyLinkedList Tail) : SinglyLinkedList { - public override IEnumerator GetEnumerator() { - return new LinkedListEnumerator(this); - } -} - -public record Nil() : SinglyLinkedList { - public override IEnumerator GetEnumerator() { - return Enumerable.Empty().GetEnumerator(); - } -} diff --git a/Source/DafnyCore/Generic/Util.cs b/Source/DafnyCore/Generic/Util.cs deleted file mode 100644 index d52650ab2d2..00000000000 --- a/Source/DafnyCore/Generic/Util.cs +++ /dev/null @@ -1,1043 +0,0 @@ -// Copyright by the contributors to the Dafny Project -// SPDX-License-Identifier: MIT - -using System; -using System.Collections; -using System.Collections.Generic; -using System.Linq; -using System.Text; -using System.Diagnostics.Contracts; -using System.IO; -using System.Reactive.Disposables; -using System.Reactive.Linq; -using System.Text.RegularExpressions; -using System.Threading.Tasks; -using JetBrains.Annotations; -using Microsoft.Boogie; -using static Microsoft.Dafny.GenericErrors; - - -namespace Microsoft.Dafny { - public static class Sets { - public static ISet Empty() { - return new HashSet(); - } - } - - public static class Util { - - public static Task WaitForComplete(this IObservable observable) { - var result = new TaskCompletionSource(); - observable.Subscribe(_ => { }, e => result.SetException(e), () => result.SetResult()); - return result.Task; - } - - public static string CapitaliseFirstLetter(this string input) { - if (input.Length > 0) { - return char.ToUpper(input[0]) + input.Substring(1); - } - - return input; - } - - public static bool LessThanOrEquals(this T first, T second) - where T : IComparable { - return first.CompareTo(second) != 1; - } - - public static Task SelectMany(this Task task, Func> f) { -#pragma warning disable VSTHRD003 - return Select(task, f).Unwrap(); -#pragma warning restore VSTHRD003 - } - - public static Task Select(this Task task, Func f) { -#pragma warning disable VSTHRD105 - return task.ContinueWith(completedTask => f(completedTask.Result), TaskContinuationOptions.OnlyOnRanToCompletion); -#pragma warning restore VSTHRD105 - } - - public static string Comma(this IEnumerable l) { - return Comma(l, s => s.ToString()); - } - - public static string Comma(this IEnumerable l, Func f) { - return Comma(", ", l, (element, index) => f(element)); - } - - public static string Comma(this IEnumerable l, Func f) { - return Comma(", ", l, f); - } - - public static string Comma(string comma, IEnumerable l, Func f) { - return Comma(comma, l, (element, index) => f(element)); - } - - public static string Comma(string comma, IEnumerable l, Func f) { - Contract.Requires(comma != null); - string res = ""; - string c = ""; - int index = 0; - foreach (var t in l) { - res += c + f(t, index); - c = comma; - index++; - } - return res; - } - - public static string Comma(int count, Func f) { - Contract.Requires(0 <= count); - return Comma(", ", count, f); - } - - public static string Comma(string comma, int count, Func f) { - Contract.Requires(comma != null); - Contract.Requires(0 <= count); - string res = ""; - string c = ""; - for (int i = 0; i < count; i++) { - res += c + f(i); - c = comma; - } - return res; - } - - public static IEnumerable<(T, int)> Indexed(this IEnumerable enumerable) { - return enumerable.Select((value, index) => (value, index)); - } - - public static string PrintableNameList(List names, string grammaticalConjunction) { - Contract.Requires(names != null); - Contract.Requires(1 <= names.Count); - Contract.Requires(grammaticalConjunction != null); - var n = names.Count; - if (n == 1) { - return string.Format("'{0}'", names[0]); - } else if (n == 2) { - return string.Format("'{0}' {1} '{2}'", names[0], grammaticalConjunction, names[1]); - } else { - var s = ""; - for (int i = 0; i < n - 1; i++) { - s += string.Format("'{0}', ", names[i]); - } - return s + string.Format("{0} '{1}'", grammaticalConjunction, names[n - 1]); - } - } - - public static string Repeat(int count, string s) { - Contract.Requires(0 <= count); - Contract.Requires(s != null); - // special-case trivial cases - if (count == 0) { - return ""; - } else if (count == 1) { - return s; - } else { - return Comma("", count, _ => s); - } - } - - public static string Plural(int n) { - Contract.Requires(0 <= n); - return n == 1 ? "" : "s"; - } - - public static List Map(IEnumerable xs, Func f) { - List ys = new List(); - foreach (A x in xs) { - ys.Add(f(x)); - } - return ys; - } - - public static List Nil() { - return new List(); - } - - public static List Singleton(A x) { - return new List { x }; - } - - public static List List(params A[] xs) { - return xs.ToList(); - } - - public static List Cons(A x, List xs) { - return Concat(Singleton(x), xs); - } - - public static List Snoc(List xs, A x) { - return Concat(xs, Singleton(x)); - } - - public static List Concat(List xs, List ys) { - List cpy = new List(xs); - cpy.AddRange(ys); - return cpy; - } - - public static Dictionary Dict(IEnumerable xs, IEnumerable ys) { - return Dict(Enumerable.Zip(xs, ys).Select(x => new Tuple(x.First, x.Second))); - } - - public static Dictionary Dict(IEnumerable> xys) { - Dictionary res = new Dictionary(); - foreach (var p in xys) { - res[p.Item1] = p.Item2; - } - return res; - } - - public static void AddToDict(Dictionary dict, List xs, List ys) { - Contract.Requires(dict != null); - Contract.Requires(xs != null); - Contract.Requires(ys != null); - Contract.Requires(xs.Count == ys.Count); - for (var i = 0; i < xs.Count; i++) { - dict.Add(xs[i], ys[i]); - } - } - - /// - /// Returns s but with all occurrences of '_' removed. - /// - public static string RemoveUnderscores(string s) { - Contract.Requires(s != null); - return s.Replace("_", ""); - } - - /// - /// For "S" returns S and false. - /// For @"S" return S and true. - /// Assumes that s has one of these forms. - /// - public static string RemoveParsedStringQuotes(string s, out bool isVerbatimString) { - Contract.Requires(s != null); - var len = s.Length; - if (s[0] == '@') { - isVerbatimString = true; - return s.Substring(2, len - 3); - } else { - isVerbatimString = false; - return s.Substring(1, len - 2); - } - } - - public static void ValidateEscaping(DafnyOptions options, IToken t, string s, bool isVerbatimString, Errors errors) { - if (options.Get(CommonOptionBag.UnicodeCharacters)) { - foreach (var token in TokensWithEscapes(s, isVerbatimString)) { - if (token.StartsWith("\\u")) { - errors.SemErr(ErrorId.g_no_old_unicode_char, t, "\\u escape sequences are not permitted when Unicode chars are enabled"); - } - - if (token.StartsWith("\\U")) { - var hexDigits = RemoveUnderscores(token[3..^1]); - if (hexDigits.Length > 6) { - errors.SemErr(ErrorId.g_unicode_escape_must_have_six_digits, t, "\\U{X..X} escape sequence must have at most six hex digits"); - } else { - var codePoint = Convert.ToInt32(hexDigits, 16); - if (codePoint >= 0x11_0000) { - errors.SemErr(ErrorId.g_unicode_escape_is_too_large, t, "\\U{X..X} escape sequence must be less than 0x110000"); - } - if (codePoint is >= 0xD800 and < 0xE000) { - errors.SemErr(ErrorId.g_unicode_escape_may_not_be_surrogate, t, "\\U{X..X} escape sequence must not be a surrogate"); - } - } - } - } - } else { - foreach (var token2 in TokensWithEscapes(s, isVerbatimString)) { - if (token2.StartsWith("\\U")) { - errors.SemErr(ErrorId.g_U_unicode_chars_are_disallowed, t, "\\U escape sequences are not permitted when Unicode chars are disabled"); - } - } - } - } - - public static bool MightContainNonAsciiCharacters(string s, bool isVerbatimString) { - // This is conservative since \u and \U escapes could be ASCII characters, - // but that's fine since this method is just used as a conservative guard. - return TokensWithEscapes(s, isVerbatimString).Any(e => - e.Any(c => !char.IsAscii(c)) || e.StartsWith(@"\u") || e.StartsWith(@"\U")); - } - - /// - /// Replaced any escaped characters in s by the actual character that the escaping represents. - /// Assumes s to be a well-parsed string. - /// - public static string RemoveEscaping(DafnyOptions options, string s, bool isVerbatimString) { - Contract.Requires(s != null); - var sb = new StringBuilder(); - if (options.Get(CommonOptionBag.UnicodeCharacters)) { - UnescapedCharacters(options, s, isVerbatimString).ForEach(ch => sb.Append(new Rune(ch))); - } else { - UnescapedCharacters(options, s, isVerbatimString).ForEach(ch => sb.Append((char)ch)); - } - return sb.ToString(); - } - - public static readonly Regex Utf16Escape = new Regex(@"\\u([0-9a-fA-F]{4})"); - public static readonly Regex UnicodeEscape = new Regex(@"\\U\{([0-9a-fA-F_]+)\}"); - private static readonly Regex NullEscape = new Regex(@"\\0"); - - private static string ToUtf16Escape(char c, bool addBraces = false) { - if (addBraces) { - return $"\\u{{{(int)c:x4}}}"; - } else { - return $"\\u{(int)c:x4}"; - } - } - - public static string ReplaceTokensWithEscapes(string s, Regex pattern, MatchEvaluator evaluator) { - return string.Join("", - TokensWithEscapes(s, false) - .Select(token => pattern.Replace(token, evaluator))); - } - - public static string ExpandUnicodeEscapes(string s, bool lowerCaseU) { - return ReplaceTokensWithEscapes(s, UnicodeEscape, match => { - var hexDigits = RemoveUnderscores(match.Groups[1].Value); - var padChars = 8 - hexDigits.Length; - return (lowerCaseU ? "\\u" : "\\U") + new string('0', padChars) + hexDigits; - }); - } - - public static string UnicodeEscapesToLowercase(string s) { - return ReplaceTokensWithEscapes(s, UnicodeEscape, match => - $"\\u{{{RemoveUnderscores(match.Groups[1].Value)}}}"); - } - - public static string UnicodeEscapesToUtf16Escapes(string s) { - return ReplaceTokensWithEscapes(s, UnicodeEscape, match => { - var utf16CodeUnits = new char[2]; - var hexDigits = RemoveUnderscores(match.Groups[1].Value); - var codePoint = new Rune(Convert.ToInt32(hexDigits, 16)); - var codeUnits = codePoint.EncodeToUtf16(utf16CodeUnits); - if (codeUnits == 2) { - return ToUtf16Escape(utf16CodeUnits[0]) + ToUtf16Escape(utf16CodeUnits[1]); ; - } else { - return ToUtf16Escape(utf16CodeUnits[0]); - } - }); - } - - public static string ReplaceNullEscapesWithCharacterEscapes(string s) { - return ReplaceTokensWithEscapes(s, NullEscape, match => "\\u0000"); - } - - public static IEnumerable UnescapedCharacters(DafnyOptions options, string p, bool isVerbatimString) { - return UnescapedCharacters(options.Get(CommonOptionBag.UnicodeCharacters), p, isVerbatimString); - } - - /// - /// Returns the characters of the well-parsed string p, replacing any - /// escaped characters by the actual characters. - /// - /// It also converts surrogate pairs to their equivalent code points - /// if --unicode-char is enabled - these are synthesized by the parser when - /// reading the original UTF-8 source, but don't represent the true character values. - /// - public static IEnumerable UnescapedCharacters(bool unicodeChars, string p, bool isVerbatimString) { - if (isVerbatimString) { - foreach (var s in TokensWithEscapes(p, true)) { - if (s == "\"\"") { - yield return '"'; - } else { - foreach (var c in s) { - yield return c; - } - } - } - } else { - foreach (var s in TokensWithEscapes(p, false)) { - switch (s) { - case @"\'": yield return '\''; break; - case @"\""": yield return '"'; break; - case @"\\": yield return '\\'; break; - case @"\0": yield return '\0'; break; - case @"\n": yield return '\n'; break; - case @"\r": yield return '\r'; break; - case @"\t": yield return '\t'; break; - case { } when s.StartsWith(@"\u"): - yield return Convert.ToInt32(s[2..], 16); - break; - case { } when s.StartsWith(@"\U"): - yield return Convert.ToInt32(Util.RemoveUnderscores(s[3..^1]), 16); - break; - case { } when unicodeChars && char.IsHighSurrogate(s[0]): - yield return char.ConvertToUtf32(s[0], s[1]); - break; - default: - foreach (var c in s) { - yield return c; - } - break; - } - } - } - } - - /// - /// Enumerates the sequence of regular characters and escape sequences in the given well-parsed string. - /// For example, "ab\tuv\u12345" may be broken up as ["a", "b", "\t", "u", "v", "\u1234", "5"]. - /// Consecutive non-escaped characters may or may not be enumerated as a single string. - /// - public static IEnumerable TokensWithEscapes(string p, bool isVerbatimString) { - Contract.Requires(p != null); - if (isVerbatimString) { - var skipNext = false; - foreach (var ch in p) { - if (skipNext) { - skipNext = false; - } else { - if (ch == '"') { - skipNext = true; - yield return "\""; - } else { - yield return ch.ToString(); - } - } - } - } else { - var i = 0; - while (i < p.Length) { - if (p[i] == '\\') { - switch (p[i + 1]) { - case 'u': - yield return p[i..(i + 6)]; - i += 6; - break; - case 'U': - var escapeEnd = p.IndexOf('}', i + 2) + 1; - yield return p[i..escapeEnd]; - i = escapeEnd; - continue; - default: - yield return p[i..(i + 2)]; - i += 2; - break; - } - } else if (char.IsHighSurrogate(p[i])) { - yield return p[i..(i + 2)]; - i += 2; - } else { - yield return p[i].ToString(); - i++; - } - } - } - } - - /// - /// Converts a hexadecimal digit to an integer. - /// Assumes ch does represent a hexadecimal digit; alphabetic digits can be in either case. - /// - public static int HexValue(char ch) { - if ('a' <= ch && ch <= 'f') { - return ch - 'a' + 10; - } else if ('A' <= ch && ch <= 'F') { - return ch - 'A' + 10; - } else { - return ch - '0'; - } - } - - /// - /// Add "fe" to "mod", if "performThisDeprecationCheck" is "false". - /// Otherwise, first strip "fe" of certain easy occurrences of "this", and for each one giving a warning about - /// that "this" is deprecated in modifies clauses of constructors. - /// This method may modify "fe" and the subexpressions contained within "fe". - /// - public static void AddFrameExpression(List mod, FrameExpression fe, bool performThisDeprecationCheck, Errors errors) { - Contract.Requires(mod != null); - Contract.Requires(fe != null); - Contract.Requires(errors != null); - if (performThisDeprecationCheck) { - if (fe.E is ThisExpr) { - errors.Deprecated(ErrorId.g_deprecated_this_in_constructor_modifies_clause, fe.E.tok, "constructors no longer need 'this' to be listed in modifies clauses"); - return; - } else if (fe.E is SetDisplayExpr) { - var s = (SetDisplayExpr)fe.E; - var deprecated = s.Elements.FindAll(e => e is ThisExpr); - if (deprecated.Count != 0) { - foreach (var e in deprecated) { - errors.Deprecated(ErrorId.g_deprecated_this_in_constructor_modifies_clause, e.tok, "constructors no longer need 'this' to be listed in modifies clauses"); - } - s.Elements.RemoveAll(e => e is ThisExpr); - if (s.Elements.Count == 0) { - return; - } - } - } - } - mod.Add(fe); - } - - /// - /// Class dedicated to traversing the function call graph - /// - class FunctionCallFinder : TopDownVisitor> { - protected override bool VisitOneExpr(Expression expr, ref List calls) { - if (expr is FunctionCallExpr) { - calls.Add(((FunctionCallExpr)expr).Function); - } - return true; - } - } - - static Graph BuildFunctionCallGraph(Dafny.Program program) { - Graph functionCallGraph = new Graph(); - FunctionCallFinder callFinder = new FunctionCallFinder(); - - foreach (var module in program.Modules()) { - foreach (var decl in module.TopLevelDecls) { - if (decl is TopLevelDeclWithMembers c) { - foreach (var member in c.Members) { - if (member is Function f) { - List calls = new List(); - foreach (var e in f.Reads.Expressions) { if (e != null && e.E != null) { callFinder.Visit(e.E, calls); } } - foreach (var e in f.Req) { if (e != null) { callFinder.Visit(e, calls); } } - foreach (var e in f.Ens) { if (e != null) { callFinder.Visit(e, calls); } } - if (f.Body != null) { - callFinder.Visit(f.Body, calls); - } - - foreach (var callee in calls) { - functionCallGraph.AddEdge(f, callee); - } - } - } - } - } - } - - return functionCallGraph; - } - - /// - /// Prints the program's function call graph in a format suitable for consumption in other tools - /// - public static void PrintFunctionCallGraph(Dafny.Program program) { - var functionCallGraph = BuildFunctionCallGraph(program); - - foreach (var vertex in functionCallGraph.GetVertices()) { - var func = vertex.N; - program.Options.OutputWriter.Write("{0},{1}=", func.SanitizedName, func.EnclosingClass.EnclosingModuleDefinition.SanitizedName); - foreach (var callee in vertex.Successors) { - program.Options.OutputWriter.Write("{0} ", callee.N.SanitizedName); - } - program.Options.OutputWriter.Write("\n"); - } - } - - public static V GetOrDefault(this IReadOnlyDictionary dictionary, K key, Func createValue) - where V2 : V { - if (dictionary.TryGetValue(key, out var result)) { - return result; - } - - return createValue(); - } - - public static Action Concat(Action first, Action second) { - return v => { - first(v); - second(v); - }; - } - - public static V AddOrUpdate(this IDictionary dictionary, K key, V newValue, Func update) { - if (dictionary.TryGetValue(key, out var existingValue)) { - var updated = update(existingValue, newValue); - dictionary[key] = updated; - return updated; - } - - dictionary[key] = newValue; - return newValue; - } - - public static V GetOrCreate(this IDictionary dictionary, K key, Func createValue) { - if (dictionary.TryGetValue(key, out var result)) { - return result; - } - - result = createValue(); - dictionary[key] = result; - return result; - } - - /// - /// Generic statistic counter - /// - static void IncrementStat(IDictionary stats, string stat) { - if (stats.TryGetValue(stat, out var currentValue)) { - stats[stat] += 1; - } else { - stats.Add(stat, 1); - } - } - - /// - /// Track the maximum value of some statistic - /// - static void UpdateMax(IDictionary stats, string stat, ulong val) { - if (stats.TryGetValue(stat, out var currentValue)) { - if (val > currentValue) { - stats[stat] = val; - } - } else { - stats.Add(stat, val); - } - } - - /// - /// Compute various interesting statistics about the Dafny program - /// - public static void PrintStats(Dafny.Program program) { - SortedDictionary stats = new SortedDictionary(); - - foreach (var module in program.Modules()) { - IncrementStat(stats, "Modules"); - UpdateMax(stats, "Module height (max)", (ulong)module.Height); - - ulong num_scc = (ulong)module.CallGraph.TopologicallySortedComponents().Count; - UpdateMax(stats, "Call graph width (max)", num_scc); - - foreach (var decl in module.TopLevelDecls) { - if (decl is DatatypeDecl) { - IncrementStat(stats, "Datatypes"); - } else if (decl is ClassLikeDecl) { - var c = (ClassLikeDecl)decl; - if (c.Name != "_default") { - IncrementStat(stats, "Classes"); - } - - foreach (var member in c.Members) { - if (member is Function) { - IncrementStat(stats, "Functions (total)"); - var f = (Function)member; - if (f.IsRecursive) { - IncrementStat(stats, "Functions recursive"); - } - } else if (member is Method) { - IncrementStat(stats, "Methods (total)"); - var method = (Method)member; - if (method.IsRecursive) { - IncrementStat(stats, "Methods recursive"); - } - if (method.IsGhost) { - IncrementStat(stats, "Methods ghost"); - } - } - } - } - } - } - - // Print out the results, with some nice formatting - program.Options.OutputWriter.WriteLine(""); - program.Options.OutputWriter.WriteLine("Statistics"); - program.Options.OutputWriter.WriteLine("----------"); - - int max_key_length = 0; - foreach (var key in stats.Keys) { - if (key.Length > max_key_length) { - max_key_length = key.Length; - } - } - - foreach (var keypair in stats) { - string keyString = keypair.Key.PadRight(max_key_length + 2); - program.Options.OutputWriter.WriteLine("{0} {1,4}", keyString, keypair.Value); - } - } - - public static IEnumerable Lines(TextReader reader) { - return new LinesEnumerable(reader); - } - } - - public class DependencyMap { - private Dictionary> dependencies; - - public DependencyMap() { - dependencies = new Dictionary>(); - } - - public void AddInclude(Include include) { - SortedSet existingDependencies = null; - string key = include.IncluderFilename.LocalPath ?? "roots"; - bool found = dependencies.TryGetValue(key, out existingDependencies); - if (found) { - existingDependencies.Add(include.CanonicalPath); - } else { - dependencies[key] = new SortedSet() { include.CanonicalPath }; - } - } - - public void AddIncludes(IEnumerable includes) { - // Reconstruct the dependency map - Dictionary> dependencies = new Dictionary>(); - foreach (Include include in includes) { - AddInclude(include); - } - } - - public void PrintMap(DafnyOptions options) { - SortedSet leaves = new SortedSet(); // Files that don't themselves include any files - foreach (string target in dependencies.Keys) { - options.OutputWriter.Write(target); - foreach (string dependency in dependencies[target]) { - options.OutputWriter.Write(";" + dependency); - if (!dependencies.ContainsKey(dependency)) { - leaves.Add(dependency); - } - } - options.OutputWriter.WriteLine(); - } - foreach (string leaf in leaves) { - options.OutputWriter.WriteLine(leaf); - } - } - } - - class IEnumerableComparer : IEqualityComparer> { - public bool Equals(IEnumerable x, IEnumerable y) { - return x.SequenceEqual(y); - } - - public int GetHashCode(IEnumerable obj) { - var hash = new HashCode(); - foreach (T t in obj) { - hash.Add(t); - } - return hash.ToHashCode(); - } - } - - // Class to traverse a program top-down, especially aimed at identifying expressions and statements, - // and in their context - // How to use: - // - Define a subclass of ProgramTraverser - // - Implement the methods (TopDown|BottomUp)(Enter|Exit), override Traverse if needed. - // - Call any Traverse() method. - public class ProgramTraverser { - public enum ContinuationStatus { - Ok, // Continue exploration - Skip, // Skip this node and its descendants (valid only on entering a node) - Stop, // Stop the entire traversal here, but traverse ancestors in bottom-up - } - protected const ContinuationStatus ok = ContinuationStatus.Ok; - protected const ContinuationStatus skip = ContinuationStatus.Skip; - protected const ContinuationStatus stop = ContinuationStatus.Stop; - // Returns true if statement needs to be traversed - protected virtual ContinuationStatus OnEnter(Statement stmt, [CanBeNull] string field, [CanBeNull] object parent) { - return ok; - } - // Returns true if expression needs to be traversed - protected virtual ContinuationStatus OnEnter(Expression expr, [CanBeNull] string field, [CanBeNull] object parent) { - return ok; - } - - // Returns true if need to stop the traversal entirely - protected virtual bool OnExit(Statement stmt, [CanBeNull] string field, [CanBeNull] object parent) { - return false; - } - // Returns true if need to stop the traversal entirely - protected virtual bool OnExit(Expression expr, [CanBeNull] string field, [CanBeNull] object parent) { - return false; - } - - protected virtual ContinuationStatus OnEnter(MemberDecl memberDecl, [CanBeNull] string field, [CanBeNull] object parent) { - return ok; - } - - // Traverse methods retun true to interrupt. - public bool Traverse(Program program) { - if (program == null) { - return false; - } - - return program.Modules().Any(Traverse); - } - - public bool Traverse(ModuleDefinition moduleDefinition) { - if (moduleDefinition == null) { - return false; - } - - return Traverse(moduleDefinition.TopLevelDecls); - } - - public bool Traverse(IEnumerable topLevelDecls) { - if (topLevelDecls == null) { - return false; - } - - foreach (var topLevelDecl in topLevelDecls) { - if (Traverse(topLevelDecl)) { - return true; - } - } - - return false; - } - - public bool Traverse(ModuleDecl moduleDecl) { - if (moduleDecl == null) { - return false; - } - - if (moduleDecl is LiteralModuleDecl l) { - return Traverse(l.ModuleDef); - } else if (moduleDecl is AbstractModuleDecl a) { - return Traverse(a.CompileRoot); - }/* else if (moduleDecl is AliasModuleDecl a) { - - } else if (moduleDecl is ModuleExportDecl m) { - - }*/ - - return false; - } - - public bool Traverse(Formal formal) { - if (formal == null) { - return false; - } - - if (formal.DefaultValue != null && Traverse(formal.DefaultValue, "DefaultValue", formal)) { - return true; - } - - return false; - } - - public bool Traverse(DatatypeCtor ctor) { - if (ctor == null) { - return false; - } - - if (ctor.Formals.Any(Traverse)) { - return true; - } - - return false; - } - - public bool Traverse(TopLevelDecl topd) { - if (topd == null) { - return false; - } - - var d = topd is ClassLikeDecl classDecl && classDecl.NonNullTypeDecl != null ? classDecl.NonNullTypeDecl : topd; - - if (d is TopLevelDeclWithMembers tdm) { - // ClassDecl, DatatypeDecl, AbstractTypeDecl, NewtypeDecl - if (tdm.Members.Any(memberDecl => Traverse(memberDecl, "Members", tdm))) { - return true; - } - - if (tdm is IteratorDecl iter) { - // TODO: Import this - if (Attributes.SubExpressions(iter.Attributes).Any(e => Traverse(e, "Attributes.SubExpressions", iter))) { - return true; - } - if (Attributes.SubExpressions(iter.Reads.Attributes).Any(e => Traverse(e, "Reads.Attributes.SubExpressions", iter))) { - return true; - } - if (iter.Reads.Expressions.Any(e => Traverse(e.E, "Reads.Expressions.E", iter))) { - return true; - } - if (Attributes.SubExpressions(iter.Modifies.Attributes).Any(e => Traverse(e, "Modifies.Attributes.SubExpressions", iter))) { - return true; - } - if (iter.Modifies.Expressions.Any(e => Traverse(e.E, "Modifies.Expressions.E", iter))) { - return true; - } - if (Attributes.SubExpressions(iter.Decreases.Attributes).Any(e => Traverse(e, "Decreases.Attributes.SubExpressions", iter))) { - return true; - } - if (iter.Decreases.Expressions.Any(e => Traverse(e, "Decreases.Expressions.E", iter))) { - return true; - } - if (iter.Requires.Any(e => Traverse(e.E, "Requires.E", iter))) { - return true; - } - if (iter.Ensures.Any(e => Traverse(e.E, "Ensures.E", iter))) { - return true; - } - if (iter.YieldRequires.Any(e => Traverse(e.E, "YieldRequires.E", iter))) { - return true; - } - if (iter.YieldEnsures.Any(e => Traverse(e.E, "YieldEnsures.E", iter))) { - return true; - } - if (Traverse(iter.Body, "Body", iter)) { - return true; - } - } - - if (tdm is DatatypeDecl dtd) { - if (dtd.Ctors.Any(Traverse)) { - return true; - } - } - } else if (d is ModuleDecl md) { - return Traverse(md); - } else if (d is TypeSynonymDecl tsd) { - // Nothing here. - } - - return false; - } - - public bool Traverse(MemberDecl memberDeclaration, [CanBeNull] string field, [CanBeNull] object parent) { - if (memberDeclaration == null) { - return false; - } - - var enterResult = OnEnter(memberDeclaration, field, parent); - if (enterResult is stop or skip) { - return enterResult == stop; - } - - if (memberDeclaration is Field fi) { - if (fi.SubExpressions.Any(expr => Traverse(expr, "SubExpressions", fi))) { - return true; - } - } else if (memberDeclaration is Function f) { - if (f.Ins.Any(Traverse)) { - return true; - } - if (f.Result != null && f.Result.DefaultValue != null && Traverse(f.Result.DefaultValue, "Result.DefaultValue", f)) { - return true; - } - if (f.Req.Any(e => Traverse(e.E, "Req.E", f))) { - return true; - } - if (f.Reads.Expressions.Any(e => Traverse(e.E, "Reads.E", f))) { - return true; - } - if (f.Ens.Any(e => Traverse(e.E, "Ens.E", f))) { - return true; - } - if (f.Decreases.Expressions.Any(e => Traverse(e, "Decreases.Expressions", f))) { - return true; - } - if (Traverse(f.Body, "Body", f)) { - return true; - } - - if (f.ByMethodDecl != null && Traverse(f.ByMethodDecl, "ByMethodDecl", f)) { - return true; - } - - if (f.ByMethodDecl == null || f.ByMethodDecl.Body != f.ByMethodBody) { - if (f.ByMethodBody != null && Traverse(f.ByMethodBody, "ByMethodBody", f)) { - return true; - } - } - } else if (memberDeclaration is Method m) { - // For example, default value of formals is non-ghost - if (m.Ins.Any(formal => formal.DefaultValue != null - && Traverse(formal.DefaultValue, "Ins.DefaultValue", m))) { - return true; - } - if (m.Req.Any(e => Traverse(e.E, "Req.E", m))) { - return true; - } - if (m.Reads.Expressions.Any(e => Traverse(e.E, "Reads.E", m))) { - return true; - } - if (m.Mod.Expressions.Any(e => Traverse(e.E, "Mod.E", m) == true)) { - return true; - } - if (m.Ens.Any(e => Traverse(e.E, "Ens.E", m))) { - return true; - } - if (m.Decreases.Expressions.Any(e => Traverse(e, "Decreases.Expressions", m))) { - return true; - } - if (Traverse(m.Body, "Body", m)) { - return true; - } - } - - return false; - } - - public virtual bool Traverse(Statement stmt, [CanBeNull] string field, [CanBeNull] object parent) { - if (stmt == null) { - return false; - } - - var enterResult = OnEnter(stmt, field, parent); - if (enterResult is stop or skip) { - return enterResult == stop; - } - - return stmt.NonSpecificationSubExpressions.Any(subExpr => Traverse(subExpr, "NonSpecificationSubExpressions", stmt)) || - stmt.SpecificationSubExpressions.Any(subExpr => Traverse(subExpr, "SpecificationSubExpressions", stmt)) || - stmt.SubStatements.Any(subStmt => Traverse(subStmt, "SubStatements", stmt)) || - OnExit(stmt, field, parent); - } - - public virtual bool Traverse(Expression expr, [CanBeNull] string field, [CanBeNull] object parent) { - if (expr == null) { - return false; - } - - var enterResult = OnEnter(expr, field, parent); - if (enterResult is stop or skip) { - return enterResult == stop; - } - - return expr.SubExpressions.Any(subExpr => Traverse(subExpr, "SubExpression", expr)) || - OnExit(expr, field, parent); - } - } - - class LinesEnumerable : IEnumerable { - private readonly TextReader Reader; - - public LinesEnumerable(TextReader reader) { - Reader = reader; - } - - public IEnumerator GetEnumerator() { - return new LinesEnumerator(Reader); - } - - IEnumerator IEnumerable.GetEnumerator() { - return GetEnumerator(); - } - } - - class LinesEnumerator : IEnumerator { - - private readonly TextReader Reader; - - public LinesEnumerator(TextReader reader) { - Reader = reader; - } - - public bool MoveNext() { - Current = Reader.ReadLine(); - return Current != null; - } - - public void Reset() { - throw new NotImplementedException(); - } - - public string Current { get; internal set; } - - object IEnumerator.Current => Current; - - public void Dispose() { - } - } -} diff --git a/Source/DafnyCore/Backends/CSharp/CsharpBackend.cs b/Source/DafnyCore/Languages/CSharp/CsharpBackend.cs similarity index 98% rename from Source/DafnyCore/Backends/CSharp/CsharpBackend.cs rename to Source/DafnyCore/Languages/CSharp/CsharpBackend.cs index 56a91d83ae7..0f98d70a2f6 100644 --- a/Source/DafnyCore/Backends/CSharp/CsharpBackend.cs +++ b/Source/DafnyCore/Languages/CSharp/CsharpBackend.cs @@ -9,7 +9,7 @@ namespace Microsoft.Dafny.Compilers; public class CsharpBackend : ExecutableBackend { - protected override SinglePassCodeGenerator CreateCodeGenerator() { + protected override CodeGenerator CreateCodeGenerator() { return new CsharpCodeGenerator(Options, Reporter); } @@ -90,7 +90,7 @@ public override string GetCompileName(bool isDefaultModule, string moduleName, s {outputType} - net6.0 + net8.0 enable false CS8600;CS8603;CS8604;CS8605;CS8625;CS8629;CS8714;CS8765;CS8769;CS8981 diff --git a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs b/Source/DafnyCore/Languages/CSharp/CsharpCodeGenerator.cs similarity index 99% rename from Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs rename to Source/DafnyCore/Languages/CSharp/CsharpCodeGenerator.cs index 076c247c6de..feae13623e5 100644 --- a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs +++ b/Source/DafnyCore/Languages/CSharp/CsharpCodeGenerator.cs @@ -2222,7 +2222,7 @@ protected override void EmitLiteralExpr(ConcreteSyntaxTree wr, LiteralExpr e) { } else if (e is CharLiteralExpr) { var v = (string)e.Value; if (UnicodeCharEnabled) { - var codePoint = Util.UnescapedCharacters(Options, v, false).Single(); + var codePoint = DafnyUtils.UnescapedCharacters(Options, v, false).Single(); if (codePoint > char.MaxValue) { // C# supports \U, but doesn't allow values that require two UTF-16 code units in character literals. // For such values we construct the Rune value directly from the unescaped codepoint. diff --git a/Source/DafnyCore/Backends/CSharp/CsharpSynthesizer.cs b/Source/DafnyCore/Languages/CSharp/CsharpSynthesizer.cs similarity index 100% rename from Source/DafnyCore/Backends/CSharp/CsharpSynthesizer.cs rename to Source/DafnyCore/Languages/CSharp/CsharpSynthesizer.cs diff --git a/Source/DafnyCore/Backends/CodeGeneratorTypeExtensions.cs b/Source/DafnyCore/Languages/CodeGeneratorTypeExtensions.cs similarity index 100% rename from Source/DafnyCore/Backends/CodeGeneratorTypeExtensions.cs rename to Source/DafnyCore/Languages/CodeGeneratorTypeExtensions.cs diff --git a/Source/DafnyCore/Backends/CoverageInstrumenter.cs b/Source/DafnyCore/Languages/CoverageInstrumenter.cs similarity index 100% rename from Source/DafnyCore/Backends/CoverageInstrumenter.cs rename to Source/DafnyCore/Languages/CoverageInstrumenter.cs diff --git a/Source/DafnyCore/Backends/Cplusplus/CppBackend.cs b/Source/DafnyCore/Languages/Cplusplus/CppBackend.cs similarity index 97% rename from Source/DafnyCore/Backends/Cplusplus/CppBackend.cs rename to Source/DafnyCore/Languages/Cplusplus/CppBackend.cs index 095412d24e2..769ff4776a2 100644 --- a/Source/DafnyCore/Backends/Cplusplus/CppBackend.cs +++ b/Source/DafnyCore/Languages/Cplusplus/CppBackend.cs @@ -9,7 +9,7 @@ namespace Microsoft.Dafny.Compilers; public class CppBackend : ExecutableBackend { - protected override SinglePassCodeGenerator CreateCodeGenerator() { + protected override CodeGenerator CreateCodeGenerator() { return new CppCodeGenerator(Options, Reporter, OtherFileNames); } diff --git a/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs b/Source/DafnyCore/Languages/Cplusplus/CppCodeGenerator.cs similarity index 100% rename from Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs rename to Source/DafnyCore/Languages/Cplusplus/CppCodeGenerator.cs diff --git a/Source/DafnyCore/Backends/Dafny/AST.dfy b/Source/DafnyCore/Languages/Dafny/AST.dfy similarity index 100% rename from Source/DafnyCore/Backends/Dafny/AST.dfy rename to Source/DafnyCore/Languages/Dafny/AST.dfy diff --git a/Source/DafnyCore/Backends/Dafny/ASTBuilder.cs b/Source/DafnyCore/Languages/Dafny/ASTBuilder.cs similarity index 100% rename from Source/DafnyCore/Backends/Dafny/ASTBuilder.cs rename to Source/DafnyCore/Languages/Dafny/ASTBuilder.cs diff --git a/Source/DafnyCore/Backends/Dafny/BuilderSyntaxTree.cs b/Source/DafnyCore/Languages/Dafny/BuilderSyntaxTree.cs similarity index 100% rename from Source/DafnyCore/Backends/Dafny/BuilderSyntaxTree.cs rename to Source/DafnyCore/Languages/Dafny/BuilderSyntaxTree.cs diff --git a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs b/Source/DafnyCore/Languages/Dafny/DafnyCodeGenerator.cs similarity index 99% rename from Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs rename to Source/DafnyCore/Languages/Dafny/DafnyCodeGenerator.cs index 572bd8ad845..74625a5b4cf 100644 --- a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs +++ b/Source/DafnyCore/Languages/Dafny/DafnyCodeGenerator.cs @@ -1389,7 +1389,7 @@ protected override void EmitLiteralExpr(ConcreteSyntaxTree wr, LiteralExpr e) { switch (e) { case CharLiteralExpr c: - var codePoint = Util.UnescapedCharacters(Options, (string)c.Value, false).Single(); + var codePoint = DafnyUtils.UnescapedCharacters(Options, (string)c.Value, false).Single(); if (Rune.IsRune(new BigInteger(codePoint))) { // More readable version in the generated code. baseExpr = (DAST.Expression)DAST.Expression.create_Literal(DAST.Literal.create_CharLiteral( new Rune(codePoint) diff --git a/Source/DafnyCore/Backends/Dafny/PrettyPrinter.dfy b/Source/DafnyCore/Languages/Dafny/PrettyPrinter.dfy similarity index 100% rename from Source/DafnyCore/Backends/Dafny/PrettyPrinter.dfy rename to Source/DafnyCore/Languages/Dafny/PrettyPrinter.dfy diff --git a/Source/DafnyCore/Backends/Dafny/UnsupportedFeatureException.dfy b/Source/DafnyCore/Languages/Dafny/UnsupportedFeatureException.dfy similarity index 100% rename from Source/DafnyCore/Backends/Dafny/UnsupportedFeatureException.dfy rename to Source/DafnyCore/Languages/Dafny/UnsupportedFeatureException.dfy diff --git a/Source/DafnyCore/Backends/Dafny/WrapException.cs b/Source/DafnyCore/Languages/Dafny/WrapException.cs similarity index 100% rename from Source/DafnyCore/Backends/Dafny/WrapException.cs rename to Source/DafnyCore/Languages/Dafny/WrapException.cs diff --git a/Source/DafnyCore/Backends/DafnyExecutableBackend.cs b/Source/DafnyCore/Languages/DafnyExecutableBackend.cs similarity index 96% rename from Source/DafnyCore/Backends/DafnyExecutableBackend.cs rename to Source/DafnyCore/Languages/DafnyExecutableBackend.cs index 19ed5bf777e..518825bcb9f 100644 --- a/Source/DafnyCore/Backends/DafnyExecutableBackend.cs +++ b/Source/DafnyCore/Languages/DafnyExecutableBackend.cs @@ -15,7 +15,7 @@ public abstract class DafnyExecutableBackend : ExecutableBackend { protected DafnyExecutableBackend(DafnyOptions options) : base(options) { } - protected override SinglePassCodeGenerator CreateCodeGenerator() { + protected override CodeGenerator CreateCodeGenerator() { // becomes this.compiler return new DafnyCodeGenerator(Options, Reporter, InternalFieldPrefix, PreventShadowing, CanEmitUncompilableCode); } diff --git a/Source/DafnyCore/Backends/DafnyWrittenCodeGenerator.cs b/Source/DafnyCore/Languages/DafnyWrittenCodeGenerator.cs similarity index 100% rename from Source/DafnyCore/Backends/DafnyWrittenCodeGenerator.cs rename to Source/DafnyCore/Languages/DafnyWrittenCodeGenerator.cs diff --git a/Source/DafnyCore/Backends/DatatypeWrapperEraser.cs b/Source/DafnyCore/Languages/DatatypeWrapperEraser.cs similarity index 100% rename from Source/DafnyCore/Backends/DatatypeWrapperEraser.cs rename to Source/DafnyCore/Languages/DatatypeWrapperEraser.cs diff --git a/Source/DafnyCore/Backends/ExecutableBackend.cs b/Source/DafnyCore/Languages/ExecutableBackend.cs similarity index 98% rename from Source/DafnyCore/Backends/ExecutableBackend.cs rename to Source/DafnyCore/Languages/ExecutableBackend.cs index 78aba798902..bd478416af5 100644 --- a/Source/DafnyCore/Backends/ExecutableBackend.cs +++ b/Source/DafnyCore/Languages/ExecutableBackend.cs @@ -15,7 +15,7 @@ namespace Microsoft.Dafny; public abstract class ExecutableBackend : IExecutableBackend { // May be null for backends that don't use the single-pass compiler logic - protected SinglePassCodeGenerator codeGenerator; + protected CodeGenerator codeGenerator; protected ExecutableBackend(DafnyOptions options) : base(options) { } @@ -124,7 +124,7 @@ public override void OnPreCompile(ErrorReporter reporter, ReadOnlyCollection OnPostGenerate(string dafnyProgramName, string targetDirectory, TextWriter outputWriter) { - CodeGenerator.Coverage.WriteLegendFile(); + CodeGenerator.Coverage?.WriteLegendFile(); return Task.FromResult(true); } - protected abstract SinglePassCodeGenerator CreateCodeGenerator(); + protected abstract CodeGenerator CreateCodeGenerator(); public override string PublicIdProtect(string name) { return CodeGenerator.PublicIdProtect(name); diff --git a/Source/DafnyCore/Backends/ExternExtensions.cs b/Source/DafnyCore/Languages/ExternExtensions.cs similarity index 100% rename from Source/DafnyCore/Backends/ExternExtensions.cs rename to Source/DafnyCore/Languages/ExternExtensions.cs diff --git a/Source/DafnyCore/Backends/GeneratorErrors.cs b/Source/DafnyCore/Languages/GeneratorErrors.cs similarity index 100% rename from Source/DafnyCore/Backends/GeneratorErrors.cs rename to Source/DafnyCore/Languages/GeneratorErrors.cs diff --git a/Source/DafnyCore/Backends/GenericCompilationInstrumenter.cs b/Source/DafnyCore/Languages/GenericCompilationInstrumenter.cs similarity index 100% rename from Source/DafnyCore/Backends/GenericCompilationInstrumenter.cs rename to Source/DafnyCore/Languages/GenericCompilationInstrumenter.cs diff --git a/Source/DafnyCore/Backends/GoLang/GoBackend.cs b/Source/DafnyCore/Languages/GoLang/GoBackend.cs similarity index 99% rename from Source/DafnyCore/Backends/GoLang/GoBackend.cs rename to Source/DafnyCore/Languages/GoLang/GoBackend.cs index 2772a36b90a..062e607e516 100644 --- a/Source/DafnyCore/Backends/GoLang/GoBackend.cs +++ b/Source/DafnyCore/Languages/GoLang/GoBackend.cs @@ -45,7 +45,7 @@ static GoBackend() { }); } - protected override SinglePassCodeGenerator CreateCodeGenerator() { + protected override CodeGenerator CreateCodeGenerator() { var goModuleName = Options.Get(GoModuleNameCliOption); GoModuleMode = goModuleName != null; if (GoModuleMode) { diff --git a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs b/Source/DafnyCore/Languages/GoLang/GoCodeGenerator.cs similarity index 99% rename from Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs rename to Source/DafnyCore/Languages/GoLang/GoCodeGenerator.cs index 856bd85ce5d..e86be6200a8 100644 --- a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs +++ b/Source/DafnyCore/Languages/GoLang/GoCodeGenerator.cs @@ -2295,7 +2295,7 @@ protected void TrCharLiteral(CharLiteralExpr chr, ConcreteSyntaxTree wr) { wr.Write($"{CharTypeName}("); // See comment in TrStringLiteral for why we can't just translate directly sometimes. if (!UnicodeCharEnabled && Util.MightContainNonAsciiCharacters(v, false)) { - var c = Util.UnescapedCharacters(Options, v, false).Single(); + var c = DafnyUtils.UnescapedCharacters(Options, v, false).Single(); wr.Write($"{c}"); } else { wr.Write("'{0}'", TranslateEscapes(v, isChar: true)); @@ -2323,7 +2323,7 @@ protected override void TrStringLiteral(StringLiteralExpr str, ConcreteSyntaxTre if (Util.MightContainNonAsciiCharacters(s, false)) { wr.Write($"_dafny.SeqOfChars("); var comma = ""; - foreach (var c in Util.UnescapedCharacters(Options, s, str.IsVerbatim)) { + foreach (var c in DafnyUtils.UnescapedCharacters(Options, s, str.IsVerbatim)) { wr.Write(comma); wr.Write($"{c}"); comma = ", "; diff --git a/Source/DafnyCore/Backends/InternalBackendsPluginConfiguration.cs b/Source/DafnyCore/Languages/InternalBackendsPluginConfiguration.cs similarity index 94% rename from Source/DafnyCore/Backends/InternalBackendsPluginConfiguration.cs rename to Source/DafnyCore/Languages/InternalBackendsPluginConfiguration.cs index ebd3651fad5..5aac5e43bcd 100644 --- a/Source/DafnyCore/Backends/InternalBackendsPluginConfiguration.cs +++ b/Source/DafnyCore/Languages/InternalBackendsPluginConfiguration.cs @@ -11,6 +11,7 @@ public override IExecutableBackend[] GetCompilers(DafnyOptions options) { new JavaScriptBackend(options), new GoBackend(options), new JavaBackend(options), + new VerifiedJavaBackend(options), new PythonBackend(options), new CppBackend(options), new LibraryBackend(options), diff --git a/Source/DafnyCore/Languages/Java/Frontend/JavaGrammar.cs b/Source/DafnyCore/Languages/Java/Frontend/JavaGrammar.cs new file mode 100644 index 00000000000..182da4dc0c4 --- /dev/null +++ b/Source/DafnyCore/Languages/Java/Frontend/JavaGrammar.cs @@ -0,0 +1,582 @@ +// See https://aka.ms/new-console-template for more information + +#nullable enable +using System; +using System.Collections.Generic; +using System.IO; +using System.Linq; +using System.Linq.Expressions; +using System.Numerics; +using CompilerBuilder; +using CompilerBuilder.Grammars; +using static CompilerBuilder.GrammarBuilder; + +namespace Microsoft.Dafny; + +public class JavaGrammar { + + private readonly Grammar expression; + private readonly Grammar name; + private readonly Uri uri; + private readonly DafnyOptions options; + private readonly Grammar type; + private readonly Grammar statement; + private Grammar block; + private Grammar call; + private readonly Grammar attributedExpression; + + private readonly ISet keywords = new HashSet { "return", "true", "false" }; + private readonly Grammar identifier; + + public JavaGrammar(Uri uri, DafnyOptions options) { + this.uri = uri; + this.options = options; + identifier = Identifier.Where(i => !keywords.Contains(i)); + name = GetNameGrammar(); + type = TypeGrammar(); + expression = Recursive(self => { + var t = GetExpressionGrammar(self); + call = t.call; + return t.expression; + }, "expression"); + attributedExpression = expression.Map( + e => new AttributedExpression(e), + ae => ae.E); + statement = Recursive(self => { + var r = StatementGrammar(self); + block = r.Block; + return r.Statement; + }, "statement"); + } + + public Grammar GetFinalGrammar() + { + var result = File(); + return Comments.AddTrivia(result, Comments.JavaTrivia()); + } + + + public IToken ConvertValue(IPosition position, string value) { + return new Token { + col = position.Column + 1, + line = position.Line + 1, + pos = position.Offset, + Uri = uri, + val = value + }; + } + + public IToken ConvertToken(ParseRange position) { + return new Token { + col = position.From.Column + 1, + line = position.From.Line + 1, + pos = position.From.Offset, + Uri = uri, + val = new string('f', position.Until.Offset - position.From.Offset) + }; + } + + public IToken Convert(IPosition position) { + return new Token { + col = position.Column + 1, + line = position.Line + 1, + pos = position.Offset, + Uri = uri, + }; + } + + public RangeToken Convert(ParseRange parseRange) { + return new RangeToken(Convert(parseRange.From), Convert(parseRange.Until)); + } + + public Grammar File() { + var package = Keyword("package").Then(identifier.CommaSeparated()).Then(";").Ignore(); + + var include = Keyword("include").Then(StringInDoubleQuotes).Map((r, s) => + new Include(ConvertToken(r), uri, new Uri(Path.GetFullPath(s, Path.GetDirectoryName(uri.LocalPath)!)), options), + i => i.IncludedFilename.LocalPath); + var includes = include.Many(Separator.Linebreak); + + var qualifiedId = name.Map(n => new ModuleQualifiedId([n]), q => q.Path[0]); + var import = Keyword("import").Then(qualifiedId).Then(";", Separator.Nothing).Map( + (t, a) => new AliasModuleDecl(DafnyOptions.Default, + Convert(t), a, a.Path[^1], null, true, [], Guid.NewGuid()), + a => a.TargetQId); + + var classes = Class().Many(Separator.EmptyLine); + var imports = import.Many(Separator.Linebreak); + return Constructor().Then(package). + Then(includes, f => f.Includes). + Then(imports, f => f.SourceDecls.OfType().ToList(), + (f, a) => f.SourceDecls.AddRange(a), Separator.EmptyLine). + Then(classes, + f => f.SourceDecls.OfType().ToList(), + (f, c) => f.SourceDecls.AddRange(c), Separator.EmptyLine); + } + + Grammar Class() { + var header = Constructor(). + Then(Modifier("final").Ignore()). // TODO Bind to attribute + Then("class"). + Then(name, cl => cl.NameNode); + + var body = Member().Many(Separator.EmptyLine).InBraces(); + + return header. + Then(body, cl => cl.Members). + FinishRangeNode(uri); + } + + Grammar Member() { + var (method, function) = MethodAndFunction(); + return method.UpCast().OrCast(function); + } + + (Grammar Method, Grammar Function) MethodAndFunction() { + // Need something special for a unordered bag of keywords + var staticc = Keyword("static").Then(Constant(true)).Default(false); + + var parameter = Constructor(). + Then(type, f => f.Type). + Then(name, f => new Name(f.Name), (f,v) => { + f.Name = v.Value; + f.tok = v.tok; + }). + SetRange((f, t) => { + f.RangeToken = Convert(t); + f.tok = ConvertToken(t); + f.InParam = true; + }); + + var parameters = parameter.CommaSeparated().InParens(); + var require = Keyword("requires").Then(attributedExpression); + var requires = require.Many(Separator.Linebreak); + + var ensure = Keyword("ensures").Then(attributedExpression); + var ensures = ensure.Many(Separator.Linebreak); + + var returnParameter = type.Map( + t => new Formal(t.Tok,"_returnName", t, false, false, null), + f=> f.Type); + var voidReturnType = Keyword("void").Then(Constant(null)); + var outs = voidReturnType.OrCast(returnParameter).OptionToList(); + + var frameField = Keyword("`").Then(identifier); + + var wildcardFrame = Constructor().Then( + Keyword("*").Then(Constructor()).UpCast(), f => f.OriginalExpression); + var receiverFrame = Constructor().Then(expression, f => f.OriginalExpression) + .Then(frameField.Option(), f => f.FieldName); + var implicitThisFrame = Constructor().Then( + Constructor().UpCast(), f => f.OriginalExpression); + + var frameExpression = wildcardFrame.Or(receiverFrame.Or(implicitThisFrame)); + + var modify = Keyword("modifies").Then(frameExpression); + var modifies = modify.Many(Separator.Linebreak).Map(xs => new Specification(xs, null), + s => s.Expressions); + var method = Constructor(). + Then(staticc, m => m.IsStatic). + Then(outs, m => m.Outs). + Then(name, m => m.NameNode). + Then(parameters, m => m.Ins, Separator.Nothing). + // TODO optional: allow unordered required and modifies + Then(requires.Indent(), m => m.Req, Separator.Linebreak). + Then(modifies.Indent(), m => m.Mod, Separator.Linebreak). + Then(ensures.Indent(), m => m.Ens, Separator.Linebreak). + Then(block, m => m.Body, Separator.Linebreak). + FinishRangeNode(uri); + + var expressionBody = Keyword("return"). + Then(expression). + Then(";", Separator.Nothing).InBraces(); + var function = Constructor(). + Then(Keyword("@Function")). + Then(staticc, m => m.IsStatic, Separator.Linebreak). + Then(type, m => m.ResultType). + Then(name, m => m.NameNode). + Then(parameters, m => m.Ins, Separator.Nothing). + Then(requires.Indent(), f => f.Req, Separator.Linebreak). + Then(ensures.Indent(), f => f.Ens, Separator.Linebreak). + Then(expressionBody, m => m.Body). + FinishRangeNode(uri); + + return (method, function); + } + + (Grammar Statement, Grammar Block) StatementGrammar(Grammar self) { + var blockResult = self.Many(Separator.Linebreak).InBraces(). + Assign>(b => b.Body).FinishRangeNode(uri); + + var returnStatement = Keyword("return").Then(expression).Then(";", Separator.Nothing). + Map((r, e) => + new ReturnStmt(Convert(r), [new ExprRhs(e)]), r => ((ExprRhs)r.Rhss.First()).Expr); + var ifStatement = Constructor(). + Then("if").Then(expression.InParens(), s => s.Guard). + Then(blockResult, s => s.Thn). + Then(Keyword("else").Then(self).Option(), s => s.Els); + + // TODO why does call here not work instead of expression? + // Seems like call can't be used at all because it's not a Recursive + var voidCallStatement = expression.DownCast(). + Then(";", Separator.Nothing).Map( + (t, a) => new UpdateStmt(Convert(t), new List(), [new ExprRhs(a) { + tok = Convert(t.From) + }]), + updateStmt => { + if (updateStmt.Lhss.Any()) { + return new MapFail(); + } + return MapResult.FromNullable((updateStmt.Rhss[0] as ExprRhs)?.Expr as ApplySuffix); + }); + + var oneLiteral = Expression.CreateIntLiteral(Token.NoToken, 1); + + var incrementStatement = expression.Then("++", Separator.Nothing).Then(";", Separator.Nothing).Map( + (t, e) => new UpdateStmt(Convert(t), [e], [new ExprRhs(new BinaryExpr(ConvertToken(t), + BinaryExpr.Opcode.Add, e, oneLiteral)) { + tok = Convert(t.From) + }]), + updateStmt => updateStmt.Rhss.Count == 1 && ((updateStmt.Rhss[0] as ExprRhs)?.Expr + is BinaryExpr { Op: BinaryExpr.Opcode.Add } binaryExpr) && binaryExpr.E1.Equals(oneLiteral) + ? new MapSuccess(updateStmt.Lhss[0]) : new MapFail()); + + var initializer = Keyword("=").Then(expression).Option(); + var ghostModifier = Modifier("ghost"); + var localStart = Constructor(). + Then(ghostModifier, s => s.IsGhost). + Then(type, s => s.SyntacticType). + Then(identifier, s => s.Name). + FinishRangeNode(uri); + var assert = Constructor(). + Then(Keyword("assert")). + Then(expression, a => a.Expr). + Then(";", Separator.Nothing); + + var varDecl = Constructor(). + Then(localStart, s => s.Local). + Then(initializer, s => s.Initializer).Then(";", Separator.Nothing). + Map((t, data) => { + var locals = new List { + data.Local + }; + + ConcreteUpdateStatement? update = null; + if (data.Initializer != null) { + var local = locals[0]; + update = CreateSingleUpdate(new Name(local.RangeToken, local.Name), data.Initializer); + } + return new VarDeclStmt(Convert(t), locals, update); + }, varDeclStmt => new VarDeclData { + Initializer = ((varDeclStmt.Update as UpdateStmt)?.Rhss[0] as ExprRhs)?.Expr, + Local = varDeclStmt.Locals[0] + }); + + var autoGhostidentifier = Constructor(). + Then(identifier, g => g.Name).FinishTokenNode(uri); + + var assignmentRhs = expression.Map(e => new ExprRhs(e), e => e.Expr).FinishTokenNode(uri); + var assignmentStatement = Constructor(). + Then(autoGhostidentifier.UpCast().Singleton(), s => s.Lhss). + Then(Keyword("=")).Then(assignmentRhs.UpCast().Singleton(), s => s.Rhss). + Then(";", Separator.Nothing).FinishRangeNode(uri); + + var invariant = Keyword("invariant").Then(attributedExpression); + var invariants = invariant.Many(Separator.Linebreak).Indent(); + + var decrease = Keyword("decreases").Then(expression); + var decreases = decrease.Many(Separator.Linebreak).Map( + (r, xs) => new Specification(xs, null) { + RangeToken = Convert(r), + tok = ConvertToken(r) + }, + s => s.Expressions).Indent(); + var whileStatement = Constructor().Then(Keyword("while")). + Then(expression.InParens(), w => w.Guard). + Then(invariants, w => w.Invariants, Separator.Linebreak). + Then(decreases, w => w.Decreases, Separator.Linebreak). + Then(blockResult, w => w.Body, Separator.Linebreak).FinishRangeNode(uri); + + var result = Fail("a statement").OrCast(returnStatement). + OrCast(ifStatement).OrCast(blockResult).OrCast(voidCallStatement).OrCast(assert).OrCast(varDecl). + OrCast(whileStatement).OrCast(assignmentStatement).OrCast(incrementStatement); + return (result, blockResult); + } + + private static ConcreteUpdateStatement CreateSingleUpdate(Name name, Expression value) + { + return new UpdateStmt(value.RangeToken, [ + new AutoGhostIdentifierExpr(name.Tok, name.Value) { RangeToken = name.RangeToken }], + [new ExprRhs(value)]); + } + + (Grammar expression, Grammar call) GetExpressionGrammar(Grammar self) { + // Precedence of Java operators: https://introcs.cs.princeton.edu/java/11precedence/ + + var variableRef = identifier.Map( + (r, v) => new NameSegment(Convert(r), v, null), + ie => ie.Name); + var number = Number.Map( + (r, v) => new LiteralExpr(Convert(r), v), + l => l.Value is BigInteger value ? new MapSuccess((int)value) : new MapFail()); + var nonGhostBinding = self.Map((t, e) => new ActualBinding(null, e) { + RangeToken = Convert(t), + tok = ConvertToken(t) + }, a => a.Actual); + var nonGhostBindings = nonGhostBinding.CommaSeparated(). + Map((t, b) => new ActualBindings(b) { + RangeToken = Convert(t) + }, a => a.ArgumentBindings); + + Grammar SpecificMethodCall(string methodName, Func constructor, Expression> bodyGetter, + Expression> firstArgument) where T : TokenNode { + return self.Assign(constructor, bodyGetter). + Then(".", Separator.Nothing).Then(methodName, Separator.Nothing). + Then(self.InParens(), firstArgument, Separator.Nothing). + FinishTokenNode(uri); + } + + var drop = SpecificMethodCall("drop", () => new SeqSelectExpr(false), + s => s.Seq, + s => s.E0); + + var take = SpecificMethodCall("take", () => new SeqSelectExpr(false), + s => s.Seq, + s => s.E1); + + var get = SpecificMethodCall("get", () => new SeqSelectExpr(true), + s => s.Seq, + s => s.E0); + + var length = self.Assign(() => new UnaryOpExpr(), s => s.E). + Then(Constant(UnaryOpExpr.Opcode.Cardinality), e => e.Op). + Then(".", Separator.Nothing).Then("size", Separator.Nothing). + Then(Empty.InParens(), Separator.Nothing). + FinishTokenNode(uri); + + var callExpression = self.Assign(() => new ApplySuffix(), s => s.Lhs) + .Then(nonGhostBindings.InParens(), s => s.Bindings, Separator.Nothing). + FinishTokenNode(uri); + + var exprDotName = self.Assign(() => new ExprDotName(), c => c.Lhs). + Then(".", Separator.Nothing). + Then(identifier, c => c.SuffixName, Separator.Nothing). + FinishTokenNode(uri); + + var lambdaParameter = Constructor(). + Then(type.Option(), f => f.Type). + Then(name, f => new Name(f.Name), (f,v) => { + f.Name = v.Value; + f.tok = v.tok; + }). + FinishTokenNode(uri); + var parameters = lambdaParameter.CommaSeparated(); + var lambda = Constructor(). + Then(parameters, e => e.BoundVars). + Then("->"). + Then(self, l => l.Term); + + var charLiteral = CharInSingleQuotes.Map( + (r, c) => new CharLiteralExpr(ConvertToken(r), c), + e => (string)e.Value); + + var parenthesis = self.InParens().Map( + (t, e) => new ParensExpression(ConvertToken(t), e), + p => p.E); + + // TODO fix position + var truee = Constant(Expression.CreateBoolLiteral(Token.Parsing, true)).Then("true"); + // TODO fix position + var falsee = Constant(Expression.CreateBoolLiteral(Token.Parsing, false)).Then("false"); + + Grammar code = Fail("an expression"). + OrCast(variableRef).OrCast(number).OrCast(lambda).OrCast(charLiteral).OrCast(truee).OrCast(falsee). + OrCast(drop).OrCast(take).OrCast(get).OrCast(parenthesis).OrCast(length).OrCast(exprDotName).OrCast(callExpression); + + + // postfix expr++ expr-- + + // unary ++expr --expr +expr -expr ~ ! + var unary = Recursive(unarySelf => { + var unicodeOpcode = + Constant(UnaryOpExpr.Opcode.Not).Then("!"); + var prefixUnary = unicodeOpcode.Assign(() => new UnaryOpExpr(), b => b.Op). + Then(unarySelf, u => u.E, Separator.Nothing); + + return code.OrCast(prefixUnary); + }, "unary"); + + // cast + var downcast = Recursive(castSelf => { + var cast = Constructor(). + Then(type.InParens(), c => c.ToType). + Then(castSelf, c => c.E, Separator.Nothing); + return unary.OrCast(cast); + }, "cast"); + + // multiplicative * / % + var multiplicative = Recursive(multiplicativeSelf => { + var opCodes = Constant(BinaryExpr.Opcode.Mul).Then("*").Or( + Constant(BinaryExpr.Opcode.Div).Then("/")).Or( + Constant(BinaryExpr.Opcode.Mod).Then("%")); + return downcast.OrCast(CreateBinary(multiplicativeSelf, downcast, opCodes, true)); + }, "multiplicative"); + + // additive + - + var additive = Recursive(additiveSelf => { + var opCodes = Constant(BinaryExpr.Opcode.Sub).Then("-").Or( + Constant(BinaryExpr.Opcode.Add).Then("+")); + return multiplicative.OrCast(CreateBinary(additiveSelf, multiplicative, opCodes, true)); + }, "additive"); + + // shift << >> >>> + var shift = additive; + + // relational < > <= >= instanceof + var relational = Recursive(relationalSelf => { + var opCodes = Constant(BinaryExpr.Opcode.Le).Then("<=").Or( + Constant(BinaryExpr.Opcode.Lt).Then("<")); + return shift.OrCast(CreateBinary(relationalSelf, shift, opCodes, true)); + }, "relational"); + + // equality == != + var equality = Recursive(equalitySelf => { + var opCodes = Constant(BinaryExpr.Opcode.Eq).Then("==").Or( + Constant(BinaryExpr.Opcode.Neq).Then("!=")); + return relational.OrCast(CreateBinary(equalitySelf, relational, opCodes, true)); + }, "equality"); + + // bitwise AND & + var bitwiseAnd = equality; + + // bitwise exclusive OR ^ + var bitwiseExclusiveOr = bitwiseAnd; + + // bitwise inclusive OR | + var bitwiseInclusiveOr = bitwiseExclusiveOr; + + var logicalAnd = Recursive(logicalAndSelf => { + var opCodes = Constant(BinaryExpr.Opcode.And).Then("&&"); + return bitwiseInclusiveOr.OrCast(CreateBinary(logicalAndSelf, bitwiseInclusiveOr, opCodes)); + }, "logicalAnd"); + + var logicalOr = Recursive(logicalAndSelf => { + var opCodes = Constant(BinaryExpr.Opcode.Or).Then("||"); + return logicalAnd.OrCast(CreateBinary(logicalAndSelf, logicalAnd, opCodes)); + }, "logicalOr"); + + // TODO consider not adding ==> + var implies = Recursive(impliesSelf => { + var opCodes = Constant(BinaryExpr.Opcode.Imp).Then("==>"); + return logicalOr.OrCast(CreateBinary(impliesSelf, logicalOr, opCodes)); + }, "implies"); + + var ternary = Recursive(ternarySelf => { + var t = ternarySelf.Assign(() => new ITEExpr(), e => e.Test). + Then("?"). + Then(ternarySelf, e => e.Thn).Then(":"). + Then(ternarySelf, e => e.Els); + return implies.OrCast(t); + }, "ternary"); + + // assignment = += -= *= /= %= &= ^= |= <<= >>= >>>= + + // var opCode = + //Keyword("<==>").Then(Constant(BinaryExpr.Opcode.Iff))).Or( + // Keyword("==>").Then(Constant(BinaryExpr.Opcode.Imp))).Or( + + Grammar CreateBinary(Grammar withSelf, Grammar withoutSelf, + Grammar opCode, bool leftToRight = true) { + if (leftToRight) { + return withSelf.Assign(() => new BinaryExpr(), b => b.E0). + Then(Position, e => null, (e, p) => e.tok = Convert(p)). + Then(opCode, b => b.Op). + Then(withoutSelf, b => b.E1); + } else { + return withoutSelf.Assign(() => new BinaryExpr(), b => b.E0). + Then(Position, e => null, (e, p) => e.tok = Convert(p)). + Then(opCode, b => b.Op). + Then(withSelf, b => b.E1); + } + } + + + return (ternary, callExpression); + } + + private Grammar TypeGrammar() + { + var nameSegmentForTypeName = + identifier.Map((t, i) => new NameSegment(Convert(t), i, new List()), + ns => ns.Name); + // OptGenericInstantiation + var intGrammar = Keyword("int").Then(Constant(Type.Int)); + var boolGrammar = Keyword("boolean").Then(Constant(Type.Bool)); + var userDefinedType = nameSegmentForTypeName.UpCast(). + Map(n => new UserDefinedType(n.Tok, n), udt => udt.NamePath).UpCast(); + + // { "." + // TypeNameOrCtorSuffix (. List typeArgs; .) + // OptGenericInstantiation + // (. e = new ExprDotName(tok, e, tok.val, typeArgs); .) + // } + return Fail("a type").OrCast(boolGrammar).OrCast(intGrammar).OrCast(userDefinedType); + } + + + private Grammar GetNameGrammar() => + identifier.Map((t, value) => new Name(ConvertValue(t.From, value)), n => n.Value); +} + +public static class DafnyGrammarExtensions { + public static Grammar FinishRangeNode(this Grammar grammar, Uri uri) + where T : RangeNode { + return grammar.SetRange((v, r) => v.RangeToken = Convert(r, uri)); + } + + public static Grammar FinishTokenNode(this Grammar grammar, Uri uri) + where T : TokenNode { + return grammar.SetRange((v, r) => { + v.RangeToken = Convert(r, uri); + v.tok = ConvertToken(r, uri); + }); + } + + public static IToken ConvertValue(IPosition position, string value, Uri uri) { + return new Token { + col = position.Column + 1, + line = position.Line + 1, + pos = position.Offset, + Uri = uri, + val = value + }; + } + + public static IToken ConvertToken(ParseRange position, Uri uri) { + return new Token { + col = position.From.Column + 1, + line = position.From.Line + 1, + pos = position.From.Offset, + Uri = uri, + val = new string('f', position.Until.Offset - position.From.Offset) + }; + } + + public static IToken Convert(IPosition position, Uri uri) { + return new Token { + col = position.Column + 1, + line = position.Line + 1, + pos = position.Offset, + Uri = uri, + }; + } + + public static RangeToken Convert(ParseRange parseRange, Uri uri) { + return new RangeToken(Convert(parseRange.From, uri), Convert(parseRange.Until, uri)); + } +} + +public class VarDeclData { + public LocalVariable Local { get; set; } + public Expression? Initializer { get; set; } +} \ No newline at end of file diff --git a/Source/DafnyCore/Backends/Java/JavaBackend.cs b/Source/DafnyCore/Languages/Java/JavaBackend.cs similarity index 96% rename from Source/DafnyCore/Backends/Java/JavaBackend.cs rename to Source/DafnyCore/Languages/Java/JavaBackend.cs index f0de140c466..8a634ae2c01 100644 --- a/Source/DafnyCore/Backends/Java/JavaBackend.cs +++ b/Source/DafnyCore/Languages/Java/JavaBackend.cs @@ -49,7 +49,7 @@ public override void CleanSourceDirectory(string sourceDirectory) { } } - protected override SinglePassCodeGenerator CreateCodeGenerator() { + protected override CodeGenerator CreateCodeGenerator() { return new JavaCodeGenerator(Options, Reporter); } @@ -179,7 +179,7 @@ bool CopyExternLibraryIntoPlace(string externFilename, string mainProgram, TextW string baseName = Path.GetFileNameWithoutExtension(externFilename); var mainDir = Path.GetDirectoryName(mainProgram); Contract.Assert(mainDir != null); - var tgtDir = Path.Combine(mainDir, pkgName); + var tgtDir = Path.Combine(mainDir, Path.Combine(pkgName.ToArray())); var tgtFilename = Path.Combine(tgtDir, baseName + ".java"); Directory.CreateDirectory(tgtDir); FileInfo file = new FileInfo(externFilename); @@ -190,18 +190,18 @@ bool CopyExternLibraryIntoPlace(string externFilename, string mainProgram, TextW return true; } - private static string FindPackageName(string externFilename) { + private static IList FindPackageName(string externFilename) { using var rd = new StreamReader(new FileStream(externFilename, FileMode.Open, FileAccess.Read)); - while (rd.ReadLine() is string line) { + while (rd.ReadLine() is { } line) { var match = PackageLine.Match(line); if (match.Success) { - return match.Groups[1].Value; + return match.Groups[1].Value.Split("."); } } return null; } - private static readonly Regex PackageLine = new Regex(@"^\s*package\s+([a-zA-Z0-9_]+)\s*;$"); + private static readonly Regex PackageLine = new Regex(@"^\s*package\s+([a-zA-Z0-9_\.]+)\s*;$"); public JavaBackend(DafnyOptions options) : base(options) { } diff --git a/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs b/Source/DafnyCore/Languages/Java/JavaCodeGenerator.cs similarity index 99% rename from Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs rename to Source/DafnyCore/Languages/Java/JavaCodeGenerator.cs index 45fb88a9ada..44ae0ab3538 100644 --- a/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs +++ b/Source/DafnyCore/Languages/Java/JavaCodeGenerator.cs @@ -1133,7 +1133,7 @@ protected override void EmitLiteralExpr(ConcreteSyntaxTree wr, LiteralExpr e) { } else if (e is CharLiteralExpr) { var v = (string)e.Value; if (UnicodeCharEnabled && Util.MightContainNonAsciiCharacters(v, false)) { - wr.Write($"{Util.UnescapedCharacters(Options, v, false).Single()}"); + wr.Write($"{DafnyUtils.UnescapedCharacters(Options, v, false).Single()}"); } else { wr.Write($"'{TranslateEscapes(v)}'"); } diff --git a/Source/DafnyCore/Languages/Java/VerifiedJavaBackend.cs b/Source/DafnyCore/Languages/Java/VerifiedJavaBackend.cs new file mode 100644 index 00000000000..0c4fb554bb8 --- /dev/null +++ b/Source/DafnyCore/Languages/Java/VerifiedJavaBackend.cs @@ -0,0 +1,125 @@ +using System; +using System.Collections.Generic; +using System.IO; +using System.Linq; +using System.Reactive; + +namespace Microsoft.Dafny.Compilers; + +public class VerifiedJavaBackend : JavaBackend { + + public override string TargetId => "vjava"; + + public override void Compile(Program dafnyProgram, string dafnyProgramName, ConcreteSyntaxTree output) { + + CodeGenerator.Compile(dafnyProgram, output); + } + + protected override CodeGenerator CreateCodeGenerator() { + return new VerifiedJavaCodeGenerator(); + } + + class VerifiedJavaCodeGenerator : CodeGenerator { + public string ModuleSeparator { get; } + public CoverageInstrumenter Coverage { get; } + public IReadOnlySet UnsupportedFeatures { get; } + public bool SupportsDatatypeWrapperErasure { get; } + + public void Compile(Program dafnyProgram, ConcreteSyntaxTree output) { + var fileModuleDefinition = new FileModuleDefinition(Token.NoToken); + + var parsed = false; + Program programToCompile; + if (parsed) { + programToCompile = dafnyProgram.AfterParsing; + } else { + programToCompile = dafnyProgram; + } + RemoveGhost(programToCompile); + + fileModuleDefinition.SourceDecls.AddRange( + programToCompile.DefaultModuleDef.SourceDecls.Where(td => !td.IsExtern(programToCompile.Options))); + + var grammar = new JavaGrammar(dafnyProgram.GetStartOfFirstFileToken().Uri, dafnyProgram.Options).GetFinalGrammar(); + var outputStringWriter = new StringWriter(); + grammar.ToPrinter().Print(fileModuleDefinition).ForceSuccess.Render(outputStringWriter); + output.Write(outputStringWriter.ToString()); + } + + public string PublicIdProtect(string name) { + throw new NotImplementedException(); + } + + public void EmitCallToMain(Method mainMethod, string baseName, ConcreteSyntaxTree callToMainTree) { + } + } + + static void RemoveGhost(Program program) { + var visitor = new RemoveGhostVisitor(); + + IEnumerable GetDefs(ModuleDefinition def) { + return def.TopLevelDecls.OfType().SelectMany(m => { + if (m is LiteralModuleDecl literalModuleDecl) { + return GetDefs(literalModuleDecl.ModuleDef); + } + + return []; + }).Concat([def]); + } + var modules = GetDefs(program.DefaultModuleDef); + foreach (var module in modules) { + if (!module.ShouldCompile(program.Compilation)) { + continue; + } + + foreach (var withMembers in module.TopLevelDecls.OfType()) { + foreach (var member in withMembers.Members.OfType()) { + if (member is Method method) { + visitor.Visit(method, Unit.Default); + } + + if (member is Function function) { + visitor.Visit(function, Unit.Default); + } + } + } + } + } + + class RemoveGhostVisitor : TopDownVisitor { + + public override void Visit(Method method, Unit st) { + method.Req.Clear(); + method.Ens.Clear(); + method.Decreases.Expressions.Clear(); + method.Reads.Expressions.Clear(); + method.Mod.Expressions.Clear(); + base.Visit(method, st); + } + + public override void Visit(Function function, Unit st) { + function.Req.Clear(); + function.Reads.Expressions.Clear(); + function.Ens.Clear(); + base.Visit(function, st); + } + + protected override bool VisitOneStmt(Statement stmt, ref Unit st) { + if (stmt is BlockStmt blockStmt) { + blockStmt.Body = blockStmt.Body.Where(s => { + var isGhost = s.IsGhost; + return !isGhost; + }).ToList(); + } + + if (stmt is LoopStmt loopStmt) { + loopStmt.Decreases.Expressions.Clear(); + loopStmt.Invariants.Clear(); + } + return base.VisitOneStmt(stmt, ref st); + } + } + + public VerifiedJavaBackend(DafnyOptions options) : base(options) { + } +} diff --git a/Source/DafnyCore/Backends/JavaScript/JavaScriptBackend.cs b/Source/DafnyCore/Languages/JavaScript/JavaScriptBackend.cs similarity index 98% rename from Source/DafnyCore/Backends/JavaScript/JavaScriptBackend.cs rename to Source/DafnyCore/Languages/JavaScript/JavaScriptBackend.cs index 443c3ad50b0..14b0531b0d6 100644 --- a/Source/DafnyCore/Backends/JavaScript/JavaScriptBackend.cs +++ b/Source/DafnyCore/Languages/JavaScript/JavaScriptBackend.cs @@ -23,7 +23,7 @@ public class JavaScriptBackend : ExecutableBackend { public override IReadOnlySet SupportedNativeTypes => new HashSet(new List { "number" }); - protected override SinglePassCodeGenerator CreateCodeGenerator() { + protected override CodeGenerator CreateCodeGenerator() { return new JavaScriptCodeGenerator(Options, Reporter); } diff --git a/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs b/Source/DafnyCore/Languages/JavaScript/JavaScriptCodeGenerator.cs similarity index 100% rename from Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs rename to Source/DafnyCore/Languages/JavaScript/JavaScriptCodeGenerator.cs diff --git a/Source/DafnyCore/Backends/Library/LibraryBackend.cs b/Source/DafnyCore/Languages/Library/LibraryBackend.cs similarity index 98% rename from Source/DafnyCore/Backends/Library/LibraryBackend.cs rename to Source/DafnyCore/Languages/Library/LibraryBackend.cs index b95976a046a..0ef3562f185 100644 --- a/Source/DafnyCore/Backends/Library/LibraryBackend.cs +++ b/Source/DafnyCore/Languages/Library/LibraryBackend.cs @@ -41,7 +41,7 @@ public override string TargetBaseDir(string dafnyProgramName) => public string DooPath { get; set; } - protected override SinglePassCodeGenerator CreateCodeGenerator() { + protected override CodeGenerator CreateCodeGenerator() { return null; } diff --git a/Source/DafnyCore/Backends/Python/PythonBackend.cs b/Source/DafnyCore/Languages/Python/PythonBackend.cs similarity index 98% rename from Source/DafnyCore/Backends/Python/PythonBackend.cs rename to Source/DafnyCore/Languages/Python/PythonBackend.cs index 4dc2f5a7c8b..b1ac91afe6f 100644 --- a/Source/DafnyCore/Backends/Python/PythonBackend.cs +++ b/Source/DafnyCore/Languages/Python/PythonBackend.cs @@ -45,7 +45,7 @@ static PythonBackend() { public override IReadOnlySet SupportedNativeTypes => new HashSet { "byte", "sbyte", "ushort", "short", "uint", "int", "number", "ulong", "long" }; - protected override SinglePassCodeGenerator CreateCodeGenerator() { + protected override CodeGenerator CreateCodeGenerator() { var pythonModuleName = Options.Get(PythonModuleNameCliOption); PythonModuleMode = pythonModuleName != null; if (PythonModuleMode) { diff --git a/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs b/Source/DafnyCore/Languages/Python/PythonCodeGenerator.cs similarity index 100% rename from Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs rename to Source/DafnyCore/Languages/Python/PythonCodeGenerator.cs diff --git a/Source/DafnyCore/Backends/Python/PythonExtensions.cs b/Source/DafnyCore/Languages/Python/PythonExtensions.cs similarity index 100% rename from Source/DafnyCore/Backends/Python/PythonExtensions.cs rename to Source/DafnyCore/Languages/Python/PythonExtensions.cs diff --git a/Source/DafnyCore/Backends/ResolvedDesugaredExecutableDafny/Dafny-compiler-fdafny.dfy b/Source/DafnyCore/Languages/ResolvedDesugaredExecutableDafny/Dafny-compiler-fdafny.dfy similarity index 100% rename from Source/DafnyCore/Backends/ResolvedDesugaredExecutableDafny/Dafny-compiler-fdafny.dfy rename to Source/DafnyCore/Languages/ResolvedDesugaredExecutableDafny/Dafny-compiler-fdafny.dfy diff --git a/Source/DafnyCore/Backends/ResolvedDesugaredExecutableDafny/ResolvedDesugaredExecutableDafnyBackend.cs b/Source/DafnyCore/Languages/ResolvedDesugaredExecutableDafny/ResolvedDesugaredExecutableDafnyBackend.cs similarity index 100% rename from Source/DafnyCore/Backends/ResolvedDesugaredExecutableDafny/ResolvedDesugaredExecutableDafnyBackend.cs rename to Source/DafnyCore/Languages/ResolvedDesugaredExecutableDafny/ResolvedDesugaredExecutableDafnyBackend.cs diff --git a/Source/DafnyCore/Backends/ResolvedDesugaredExecutableDafny/ResolvedDesugaredExecutableDafnyCodeGenerator.cs b/Source/DafnyCore/Languages/ResolvedDesugaredExecutableDafny/ResolvedDesugaredExecutableDafnyCodeGenerator.cs similarity index 100% rename from Source/DafnyCore/Backends/ResolvedDesugaredExecutableDafny/ResolvedDesugaredExecutableDafnyCodeGenerator.cs rename to Source/DafnyCore/Languages/ResolvedDesugaredExecutableDafny/ResolvedDesugaredExecutableDafnyCodeGenerator.cs diff --git a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-coverage.dfy b/Source/DafnyCore/Languages/Rust/Dafny-compiler-rust-coverage.dfy similarity index 100% rename from Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-coverage.dfy rename to Source/DafnyCore/Languages/Rust/Dafny-compiler-rust-coverage.dfy diff --git a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-proofs.dfy b/Source/DafnyCore/Languages/Rust/Dafny-compiler-rust-proofs.dfy similarity index 100% rename from Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-proofs.dfy rename to Source/DafnyCore/Languages/Rust/Dafny-compiler-rust-proofs.dfy diff --git a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy b/Source/DafnyCore/Languages/Rust/Dafny-compiler-rust.dfy similarity index 100% rename from Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy rename to Source/DafnyCore/Languages/Rust/Dafny-compiler-rust.dfy diff --git a/Source/DafnyCore/Backends/Rust/RustBackend.cs b/Source/DafnyCore/Languages/Rust/RustBackend.cs similarity index 100% rename from Source/DafnyCore/Backends/Rust/RustBackend.cs rename to Source/DafnyCore/Languages/Rust/RustBackend.cs diff --git a/Source/DafnyCore/Backends/Rust/RustCodeGenerator.cs b/Source/DafnyCore/Languages/Rust/RustCodeGenerator.cs similarity index 100% rename from Source/DafnyCore/Backends/Rust/RustCodeGenerator.cs rename to Source/DafnyCore/Languages/Rust/RustCodeGenerator.cs diff --git a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs b/Source/DafnyCore/Languages/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs similarity index 100% rename from Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs rename to Source/DafnyCore/Languages/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs diff --git a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs b/Source/DafnyCore/Languages/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs similarity index 100% rename from Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs rename to Source/DafnyCore/Languages/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs diff --git a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs b/Source/DafnyCore/Languages/SinglePassCodeGenerator/SinglePassCodeGenerator.cs similarity index 99% rename from Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs rename to Source/DafnyCore/Languages/SinglePassCodeGenerator/SinglePassCodeGenerator.cs index 798ccae90ca..f18118ad25c 100644 --- a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs +++ b/Source/DafnyCore/Languages/SinglePassCodeGenerator/SinglePassCodeGenerator.cs @@ -24,7 +24,17 @@ public static bool CanCompile(this ModuleDefinition module) { } } - public abstract partial class SinglePassCodeGenerator { + public interface CodeGenerator { + string ModuleSeparator { get; } + CoverageInstrumenter Coverage { get; } + IReadOnlySet UnsupportedFeatures { get; } + bool SupportsDatatypeWrapperErasure { get; } + void Compile(Program dafnyProgram, ConcreteSyntaxTree output); + string PublicIdProtect(string name); + void EmitCallToMain(Method mainMethod, string baseName, ConcreteSyntaxTree callToMainTree); + } + + public abstract partial class SinglePassCodeGenerator : CodeGenerator { // Dafny names cannot start with "_". Hence, if an internal Dafny name is problematic in the target language, // we can prefix it with "_". // This prefix can be overridden as necessary by backends. @@ -83,7 +93,7 @@ int GetUniqueAstNumber(Expression expr) { return n; } - public readonly CoverageInstrumenter Coverage; + public CoverageInstrumenter Coverage { get; } // Common limits on the size of builtins: tuple, arrow, and array types. // Some backends have to enforce limits so that all built-ins can be pre-compiled diff --git a/Source/DafnyCore/Options/TranslationRecord.cs b/Source/DafnyCore/Options/TranslationRecord.cs index 7d422376d15..bedf577d89b 100644 --- a/Source/DafnyCore/Options/TranslationRecord.cs +++ b/Source/DafnyCore/Options/TranslationRecord.cs @@ -1,3 +1,4 @@ +using System; using System.Collections.Generic; using System.CommandLine; using System.IO; @@ -85,7 +86,13 @@ private static TranslationRecord Read(TextReader reader) { } public void Write(TextWriter writer) { - writer.Write(Toml.FromModel(this, new TomlModelOptions()).Replace("\r\n", "\n")); + string content; + try { + content = Toml.FromModel(this, new TomlModelOptions()); + } catch (InvalidCastException) { + content = ""; // Seems like a toml bug that we need to do this for + } + writer.Write(content.Replace("\r\n", "\n")); } public void Write(ConcreteSyntaxTree writer) { diff --git a/Source/DafnyCore/Pipeline/Compilation.cs b/Source/DafnyCore/Pipeline/Compilation.cs index 266c5ee30f8..da7aca2819f 100644 --- a/Source/DafnyCore/Pipeline/Compilation.cs +++ b/Source/DafnyCore/Pipeline/Compilation.cs @@ -237,10 +237,12 @@ private async Task> DetermineRootFiles() { } private async Task ResolveAsync() { - await ParsedProgram; + var parsed = await ParsedProgram; if (transformedProgram == null) { return null; } + + transformedProgram.AfterParsing = parsed; var resolution = await documentLoader.ResolveAsync(this, transformedProgram!, cancellationSource.Token); if (resolution == null) { return null; diff --git a/Source/DafnyCore/Plugins/CompilerInstrumenter.cs b/Source/DafnyCore/Plugins/CompilerInstrumenter.cs index 252b18ea8b6..5ba469a3589 100644 --- a/Source/DafnyCore/Plugins/CompilerInstrumenter.cs +++ b/Source/DafnyCore/Plugins/CompilerInstrumenter.cs @@ -20,6 +20,6 @@ public CompilerInstrumenter(ErrorReporter reporter) : base(reporter) { } /// and downcast to interface with them, /// possibly reporting an error if they don't recognize the compiler. /// - public virtual void Instrument(IExecutableBackend backend, SinglePassCodeGenerator codeGenerator, Program program) { + public virtual void Instrument(IExecutableBackend backend, CodeGenerator codeGenerator, Program program) { } } \ No newline at end of file diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.ActualParameters.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.ActualParameters.cs index 6b6a9af13a9..d8a3ae6891d 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.ActualParameters.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.ActualParameters.cs @@ -126,6 +126,9 @@ void ResolveActualParameters(ActualBindings bindings, List formals, ITok bindings.ArgumentBindings.Count, bindings.ArgumentBindings.IndexOf(b), whatKind + (context is Method ? " in-parameter" : " parameter")); + if (callTok.line <= 0) { + var t = 3; + } Constraints.AddSubtypeConstraint( formal.PreType.Substitute(typeMap), b.Actual.PreType, callTok, $"incorrect argument type {what} (expected {{0}}, found {{1}})"); diff --git a/Source/DafnyCore/Rewriters/AutoReqFunctionRewriter.cs b/Source/DafnyCore/Rewriters/AutoReqFunctionRewriter.cs index 311d89d3825..56690f0fb82 100644 --- a/Source/DafnyCore/Rewriters/AutoReqFunctionRewriter.cs +++ b/Source/DafnyCore/Rewriters/AutoReqFunctionRewriter.cs @@ -1,6 +1,7 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; using System.Linq; +using DafnyCore.Generic; namespace Microsoft.Dafny; @@ -130,7 +131,7 @@ Expression Andify(IToken tok, List exprs) { } static AttributedExpression CreateAutoAttributedExpression(Expression e, Attributes attrs = null) { - return new AttributedExpression(AutoGeneratedToken.WrapExpression(e), attrs); + return new AttributedExpression(DafnyNodeExtensions.WrapExpression(e), attrs); } List gatherReqs(Function f, List args, List typeArguments, Expression f_this) { diff --git a/Source/DafnyCore/Rewriters/RefinementTransformer.cs b/Source/DafnyCore/Rewriters/RefinementTransformer.cs index 6239675d231..31532315e6d 100644 --- a/Source/DafnyCore/Rewriters/RefinementTransformer.cs +++ b/Source/DafnyCore/Rewriters/RefinementTransformer.cs @@ -16,10 +16,8 @@ using System; using System.Collections.Generic; -using System.Numerics; using System.Diagnostics.Contracts; using System.Linq; -using Microsoft.Dafny.Plugins; using static Microsoft.Dafny.RefinementErrors; namespace Microsoft.Dafny { diff --git a/Source/DafnyCore/Snippets.cs b/Source/DafnyCore/Snippets.cs index 5432562f818..622236f5e81 100644 --- a/Source/DafnyCore/Snippets.cs +++ b/Source/DafnyCore/Snippets.cs @@ -5,6 +5,7 @@ using System.IO; using System.Linq; using System.Runtime.CompilerServices; +using DafnyCore.Generic; using Microsoft.Dafny; namespace DafnyCore; @@ -49,7 +50,7 @@ private static string GetFileLine(DafnyOptions options, Uri uri, int lineIndex) // an in-memory version of each file it parses. var file = DafnyFile.HandleDafnyFile(OnDiskFileSystem.Instance, new ErrorReporterSink(options), options, uri, Token.NoToken); using var reader = file.GetContent(); - lines = Util.Lines(reader).ToList(); + lines = DafnyUtils.Lines(reader).ToList(); } catch (Exception) { lines = new List(); } diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs index 455c313b9d2..df47ca43014 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs @@ -334,7 +334,7 @@ public Boogie.Expr TrExpr(Expression expr) { } else if (e is CharLiteralExpr) { // we expect e.Value to be a string representing exactly one char Boogie.Expr rawElement = null; // assignment to please compiler's definite assignment rule - foreach (var ch in Util.UnescapedCharacters(options, (string)e.Value, false)) { + foreach (var ch in DafnyUtils.UnescapedCharacters(options, (string)e.Value, false)) { Contract.Assert(rawElement == null); // we should get here only once rawElement = BoogieGenerator.FunctionCall(GetToken(literalExpr), BuiltinFunction.CharFromInt, null, Boogie.Expr.Literal(ch)); } @@ -343,7 +343,7 @@ public Boogie.Expr TrExpr(Expression expr) { } else if (e is StringLiteralExpr) { var str = (StringLiteralExpr)e; Boogie.Expr seq = BoogieGenerator.FunctionCall(GetToken(literalExpr), BuiltinFunction.SeqEmpty, predef.BoxType); - foreach (var ch in Util.UnescapedCharacters(options, (string)e.Value, str.IsVerbatim)) { + foreach (var ch in DafnyUtils.UnescapedCharacters(options, (string)e.Value, str.IsVerbatim)) { var rawElement = BoogieGenerator.FunctionCall(GetToken(literalExpr), BuiltinFunction.CharFromInt, null, Boogie.Expr.Literal(ch)); Boogie.Expr elt = BoxIfNecessary(GetToken(literalExpr), rawElement, Type.Char); seq = BoogieGenerator.FunctionCall(GetToken(literalExpr), BuiltinFunction.SeqBuild, predef.BoxType, seq, elt); diff --git a/Source/DafnyDriver.Test/DafnyDriver.Test.csproj b/Source/DafnyDriver.Test/DafnyDriver.Test.csproj index b1681b47cb1..61b7d2790dd 100644 --- a/Source/DafnyDriver.Test/DafnyDriver.Test.csproj +++ b/Source/DafnyDriver.Test/DafnyDriver.Test.csproj @@ -1,7 +1,7 @@ - net6.0 + net8.0 enable enable diff --git a/Source/DafnyDriver/DafnyDriver.csproj b/Source/DafnyDriver/DafnyDriver.csproj index d7655e67674..411458ff3a2 100644 --- a/Source/DafnyDriver/DafnyDriver.csproj +++ b/Source/DafnyDriver/DafnyDriver.csproj @@ -5,7 +5,7 @@ DafnyDriver false TRACE - net6.0 + net8.0 Major ..\..\Binaries\ false diff --git a/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs b/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs index 6c7a02f9b60..ec5a26ce3aa 100644 --- a/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs +++ b/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs @@ -332,10 +332,10 @@ public async Task ProcessFilesAsync(IReadOnlyList/*!* } if (err == null && dafnyProgram != null && options.PrintStats) { - Util.PrintStats(dafnyProgram); + DafnyUtils.PrintStats(dafnyProgram); } if (err == null && dafnyProgram != null && options.PrintFunctionCallGraph) { - Util.PrintFunctionCallGraph(dafnyProgram); + DafnyUtils.PrintFunctionCallGraph(dafnyProgram); } if (dafnyProgram != null && options.ExtractCounterexample && exitValue == ExitValue.VERIFICATION_ERROR) { PrintCounterexample(options); diff --git a/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj b/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj index e25f0c91a99..4005d15710e 100644 --- a/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj +++ b/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj @@ -1,7 +1,7 @@  - net6.0 + net8.0 false Microsoft.Dafny.LanguageServer.IntegrationTest diff --git a/Source/DafnyLanguageServer.Test/Java/JavaIdeTest.cs b/Source/DafnyLanguageServer.Test/Java/JavaIdeTest.cs new file mode 100644 index 00000000000..db102e79c9c --- /dev/null +++ b/Source/DafnyLanguageServer.Test/Java/JavaIdeTest.cs @@ -0,0 +1,83 @@ +using System.Threading.Tasks; +using Microsoft.Dafny.LanguageServer.IntegrationTest.Util; +using Microsoft.Extensions.Logging; +using Xunit; +using Xunit.Abstractions; + +namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Java; + +public class JavaIdeTest : ClientBasedLanguageServerTest { + + [Fact] + public async Task Division() { + var input = @" +class Div { + int Foo(int x) { + return 3 / x; + } +}".TrimStart(); + var document = CreateAndOpenTestDocument(input, "Division.vjava"); + var diagnostics = await GetLastDiagnostics(document); + Assert.Single(diagnostics); + Assert.Equal(13, diagnostics[0].Range.Start.Character); + Assert.Equal("possible division by zero", diagnostics[0].Message); + } + + [Fact] + public async Task GotoDefinitionJava() { + var source = @" +class Div { + int Foo(int [>x<]) { + return 3 / >x<]; + } +}".TrimStart(); + + await AssertReferences(source, "FindReferencesJava.vjava"); + } + + [Fact] + public async Task SafeDivision() { + var input = @" +class Div { + int Foo(int x) { + if (x != 0) { + return 3 / x; + } + return 0; + } +}".TrimStart(); + var document = CreateAndOpenTestDocument(input, "Division.vjava"); + await AssertNoDiagnosticsAreComing(CancellationToken, document); + } + + + [Fact] + public async Task Requires() { + var input = @" +class Div { + int Foo(int x) + requires x != 0 + { + return 3 / x; + } +}".TrimStart(); + var document = CreateAndOpenTestDocument(input, "Requires.vjava"); + await AssertNoDiagnosticsAreComing(CancellationToken, document); + } + + public JavaIdeTest(ITestOutputHelper output, LogLevel dafnyLogLevel = LogLevel.Information) : base(output, dafnyLogLevel) + { + } +} \ No newline at end of file diff --git a/Source/DafnyLanguageServer.Test/Lookup/DocumentSymbolTest.cs b/Source/DafnyLanguageServer.Test/Navigation/DocumentSymbolTest.cs similarity index 100% rename from Source/DafnyLanguageServer.Test/Lookup/DocumentSymbolTest.cs rename to Source/DafnyLanguageServer.Test/Navigation/DocumentSymbolTest.cs diff --git a/Source/DafnyLanguageServer.Test/Lookup/GoToDefinitionTest.cs b/Source/DafnyLanguageServer.Test/Navigation/GoToDefinitionTest.cs similarity index 96% rename from Source/DafnyLanguageServer.Test/Lookup/GoToDefinitionTest.cs rename to Source/DafnyLanguageServer.Test/Navigation/GoToDefinitionTest.cs index 19c3c6a5d71..2dee56bb0d7 100644 --- a/Source/DafnyLanguageServer.Test/Lookup/GoToDefinitionTest.cs +++ b/Source/DafnyLanguageServer.Test/Navigation/GoToDefinitionTest.cs @@ -23,7 +23,7 @@ import Us>Used<] { const x: bool := 3 }".TrimStart(); - await AssertPositionsLineUpWithRanges(source); + await AssertGotoDefinition(source); } [Fact] @@ -60,7 +60,7 @@ import Used module Used { const [>x<] := 3 }".TrimStart(); - await AssertPositionsLineUpWithRanges(source); + await AssertGotoDefinition(source); } [Fact] @@ -76,7 +76,7 @@ module Used { const [>y<] := 3 const x: bool := >Used<] { const x := 3 }".TrimStart(); - await AssertPositionsLineUpWithRanges(source); + await AssertGotoDefinition(source); } [Fact] @@ -106,7 +106,7 @@ import Used module [>Used<] { const x := 3 }".TrimStart(); - await AssertPositionsLineUpWithRanges(source); + await AssertGotoDefinition(source); } [Fact] @@ -142,7 +142,7 @@ method HasLoop() { } ".TrimStart(); - await AssertPositionsLineUpWithRanges(source); + await AssertGotoDefinition(source); } [Fact] @@ -169,7 +169,7 @@ requires Err? } ".TrimStart(); - await AssertPositionsLineUpWithRanges(source); + await AssertGotoDefinition(source); } [Fact] @@ -186,7 +186,7 @@ function Bar(): Zaz.E { } ".TrimStart(); - await AssertPositionsLineUpWithRanges(source); + await AssertGotoDefinition(source); } [Fact] @@ -331,7 +331,7 @@ import Provider type A2 = Pro> RequestReferences( - TextDocumentItem documentItem, Position position, bool includeDeclaration = false) { - // We don't want resolution errors, but other diagnostics (like a cyclic-include warning) are okay - await AssertNoResolutionErrors(documentItem); - - return await client.RequestReferences( - new ReferenceParams { - TextDocument = documentItem.Uri, - Position = position, - Context = new ReferenceContext() { - IncludeDeclaration = includeDeclaration - } - }, CancellationToken).AsTask(); - } - - /// - /// Assert that when finding-references at each cursor position and each regular span, - /// the client returns all ranges marked with regular spans. - /// - private async Task AssertReferences(string source, string fileName, bool includeDeclaration = false) { - MarkupTestFile.GetPositionsAndRanges( - source, out var cleanSource, out var explicitPositions, out var expectedRangesArray); - var expectedRanges = new HashSet(expectedRangesArray); - - var positionsFromRanges = expectedRangesArray.SelectMany(r => new[] { r.Start, r.End }); - var allPositions = explicitPositions.Concat(positionsFromRanges); - - var documentItem = CreateTestDocument(cleanSource, fileName); - await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - await AssertNoResolutionErrors(documentItem); - - foreach (var position in allPositions) { - var result = await RequestReferences(documentItem, position, includeDeclaration); - var resultRanges = result.Select(location => location.Range).ToHashSet(); - Assert.Equal(expectedRanges, resultRanges); - } - } [Fact] public async Task UnusedModule() { diff --git a/Source/DafnyLanguageServer.Test/Lookup/SignatureHelpTest.cs b/Source/DafnyLanguageServer.Test/Navigation/SignatureHelpTest.cs similarity index 100% rename from Source/DafnyLanguageServer.Test/Lookup/SignatureHelpTest.cs rename to Source/DafnyLanguageServer.Test/Navigation/SignatureHelpTest.cs diff --git a/Source/DafnyLanguageServer.Test/Lookup/TestFiles/ProofDependencies/LSPProofDependencyTest.dfy b/Source/DafnyLanguageServer.Test/Navigation/TestFiles/ProofDependencies/LSPProofDependencyTest.dfy similarity index 100% rename from Source/DafnyLanguageServer.Test/Lookup/TestFiles/ProofDependencies/LSPProofDependencyTest.dfy rename to Source/DafnyLanguageServer.Test/Navigation/TestFiles/ProofDependencies/LSPProofDependencyTest.dfy diff --git a/Source/DafnyLanguageServer.Test/Lookup/TestFiles/ProofDependencies/dfyconfig.toml b/Source/DafnyLanguageServer.Test/Navigation/TestFiles/ProofDependencies/dfyconfig.toml similarity index 100% rename from Source/DafnyLanguageServer.Test/Lookup/TestFiles/ProofDependencies/dfyconfig.toml rename to Source/DafnyLanguageServer.Test/Navigation/TestFiles/ProofDependencies/dfyconfig.toml diff --git a/Source/DafnyLanguageServer.Test/Lookup/TestFiles/defines-foo.dfy b/Source/DafnyLanguageServer.Test/Navigation/TestFiles/defines-foo.dfy similarity index 100% rename from Source/DafnyLanguageServer.Test/Lookup/TestFiles/defines-foo.dfy rename to Source/DafnyLanguageServer.Test/Navigation/TestFiles/defines-foo.dfy diff --git a/Source/DafnyLanguageServer.Test/Lookup/TestFiles/find-refs-a.dfy b/Source/DafnyLanguageServer.Test/Navigation/TestFiles/find-refs-a.dfy similarity index 100% rename from Source/DafnyLanguageServer.Test/Lookup/TestFiles/find-refs-a.dfy rename to Source/DafnyLanguageServer.Test/Navigation/TestFiles/find-refs-a.dfy diff --git a/Source/DafnyLanguageServer.Test/Lookup/TestFiles/find-refs-b.dfy b/Source/DafnyLanguageServer.Test/Navigation/TestFiles/find-refs-b.dfy similarity index 100% rename from Source/DafnyLanguageServer.Test/Lookup/TestFiles/find-refs-b.dfy rename to Source/DafnyLanguageServer.Test/Navigation/TestFiles/find-refs-b.dfy diff --git a/Source/DafnyLanguageServer.Test/Lookup/TestFiles/foreign-verify.dfy b/Source/DafnyLanguageServer.Test/Navigation/TestFiles/foreign-verify.dfy similarity index 100% rename from Source/DafnyLanguageServer.Test/Lookup/TestFiles/foreign-verify.dfy rename to Source/DafnyLanguageServer.Test/Navigation/TestFiles/foreign-verify.dfy diff --git a/Source/DafnyLanguageServer.Test/Lookup/TestFiles/foreign.dfy b/Source/DafnyLanguageServer.Test/Navigation/TestFiles/foreign.dfy similarity index 100% rename from Source/DafnyLanguageServer.Test/Lookup/TestFiles/foreign.dfy rename to Source/DafnyLanguageServer.Test/Navigation/TestFiles/foreign.dfy diff --git a/Source/DafnyLanguageServer.Test/Lookup/TestFiles/includes-foo.dfy b/Source/DafnyLanguageServer.Test/Navigation/TestFiles/includes-foo.dfy similarity index 100% rename from Source/DafnyLanguageServer.Test/Lookup/TestFiles/includes-foo.dfy rename to Source/DafnyLanguageServer.Test/Navigation/TestFiles/includes-foo.dfy diff --git a/Source/DafnyLanguageServer.Test/Lookup/WorkspaceSymbolTest.cs b/Source/DafnyLanguageServer.Test/Navigation/WorkspaceSymbolTest.cs similarity index 100% rename from Source/DafnyLanguageServer.Test/Lookup/WorkspaceSymbolTest.cs rename to Source/DafnyLanguageServer.Test/Navigation/WorkspaceSymbolTest.cs diff --git a/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs b/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs index 836b8d0c59b..c4bdb3e5d45 100644 --- a/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs +++ b/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs @@ -434,7 +434,7 @@ protected async Task GetDocumentItem(string source, string fil /// assert that a RequestDefinition at position K /// returns either the Kth range, or the range with key K (as a string). /// - protected async Task AssertPositionsLineUpWithRanges(string source, string filePath = null) { + protected async Task AssertGotoDefinition(string source, string filePath = null) { MarkupTestFile.GetPositionsAndNamedRanges(source, out var cleanSource, out var positions, out var ranges); @@ -446,4 +446,42 @@ protected async Task AssertPositionsLineUpWithRanges(string source, string fileP Assert.Equal(range, result.Location!.Range); } } + + protected async Task RequestReferences( + TextDocumentItem documentItem, Position position, bool includeDeclaration = false) { + // We don't want resolution errors, but other diagnostics (like a cyclic-include warning) are okay + await AssertNoResolutionErrors(documentItem); + + return await client.RequestReferences( + new ReferenceParams { + TextDocument = documentItem.Uri, + Position = position, + Context = new ReferenceContext() { + IncludeDeclaration = includeDeclaration + } + }, CancellationToken).AsTask(); + } + + /// + /// Assert that when finding-references at each cursor position and each regular span, + /// the client returns all ranges marked with regular spans. + /// + protected async Task AssertReferences(string source, string fileName, bool includeDeclaration = false) { + MarkupTestFile.GetPositionsAndRanges( + source, out var cleanSource, out var explicitPositions, out var expectedRangesArray); + var expectedRanges = new HashSet(expectedRangesArray); + + var positionsFromRanges = expectedRangesArray.SelectMany(r => new[] { r.Start, r.End }); + var allPositions = explicitPositions.Concat(positionsFromRanges); + + var documentItem = CreateTestDocument(cleanSource, fileName); + await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); + await AssertNoResolutionErrors(documentItem); + + foreach (var position in allPositions) { + var result = await RequestReferences(documentItem, position, includeDeclaration); + var resultRanges = result.Select(location => location.Range).ToHashSet(); + Assert.Equal(expectedRanges, resultRanges); + } + } } \ No newline at end of file diff --git a/Source/DafnyLanguageServer/DafnyLanguageServer.csproj b/Source/DafnyLanguageServer/DafnyLanguageServer.csproj index 2f6b6597870..8fee50a9a8a 100644 --- a/Source/DafnyLanguageServer/DafnyLanguageServer.csproj +++ b/Source/DafnyLanguageServer/DafnyLanguageServer.csproj @@ -1,7 +1,7 @@  - net6.0 + net8.0 Major true enable diff --git a/Source/DafnyLanguageServer/Handlers/DafnyCodeActionHandler.cs b/Source/DafnyLanguageServer/Handlers/DafnyCodeActionHandler.cs index c545318402a..047ce6ba45c 100644 --- a/Source/DafnyLanguageServer/Handlers/DafnyCodeActionHandler.cs +++ b/Source/DafnyLanguageServer/Handlers/DafnyCodeActionHandler.cs @@ -33,7 +33,7 @@ public record DafnyCodeActionWithId(DafnyCodeAction DafnyCodeAction, int Id); protected override CodeActionRegistrationOptions CreateRegistrationOptions(CodeActionCapability capability, ClientCapabilities clientCapabilities) { return new CodeActionRegistrationOptions { - DocumentSelector = DocumentSelector.ForLanguage("dafny"), + DocumentSelector = DocumentSelector.ForLanguage("dafny", "vjava"), ResolveProvider = true, CodeActionKinds = Container.From( CodeActionKind.QuickFix diff --git a/Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs b/Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs index 9bf8edc6313..a8ff4caec4d 100644 --- a/Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs +++ b/Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs @@ -30,7 +30,7 @@ public DafnyCompletionHandler(ILogger logger, IProjectDa protected override CompletionRegistrationOptions CreateRegistrationOptions(CompletionCapability capability, ClientCapabilities clientCapabilities) { return new CompletionRegistrationOptions { - DocumentSelector = DocumentSelector.ForLanguage("dafny"), + DocumentSelector = DocumentSelector.ForLanguage("dafny", "vjava"), ResolveProvider = false, TriggerCharacters = new Container(".") }; diff --git a/Source/DafnyLanguageServer/Handlers/DafnyDocumentSymbolHandler.cs b/Source/DafnyLanguageServer/Handlers/DafnyDocumentSymbolHandler.cs index e4db375af42..09fb0a7349e 100644 --- a/Source/DafnyLanguageServer/Handlers/DafnyDocumentSymbolHandler.cs +++ b/Source/DafnyLanguageServer/Handlers/DafnyDocumentSymbolHandler.cs @@ -30,7 +30,7 @@ public DafnyDocumentSymbolHandler(ILogger logger, IP protected override DocumentSymbolRegistrationOptions CreateRegistrationOptions(DocumentSymbolCapability capability, ClientCapabilities clientCapabilities) { return new DocumentSymbolRegistrationOptions { - DocumentSelector = DocumentSelector.ForLanguage("dafny") + DocumentSelector = DocumentSelector.ForLanguage("dafny", "vjava") }; } diff --git a/Source/DafnyLanguageServer/Handlers/DafnyFormattingHandler.cs b/Source/DafnyLanguageServer/Handlers/DafnyFormattingHandler.cs index 39ca15bdd89..720fd5bc0d6 100644 --- a/Source/DafnyLanguageServer/Handlers/DafnyFormattingHandler.cs +++ b/Source/DafnyLanguageServer/Handlers/DafnyFormattingHandler.cs @@ -21,7 +21,7 @@ public DafnyFormattingHandler(ILogger logger, IProjectDa protected override DocumentFormattingRegistrationOptions CreateRegistrationOptions(DocumentFormattingCapability capability, ClientCapabilities clientCapabilities) { return new DocumentFormattingRegistrationOptions() { - DocumentSelector = DocumentSelector.ForLanguage("dafny") + DocumentSelector = DocumentSelector.ForLanguage("dafny", "vjava") }; } diff --git a/Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs b/Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs index 0fda0ac80bc..4665ba709e9 100644 --- a/Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs +++ b/Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs @@ -34,7 +34,7 @@ public DafnyHoverHandler(ILogger logger, IProjectDatabase pro protected override HoverRegistrationOptions CreateRegistrationOptions(HoverCapability capability, ClientCapabilities clientCapabilities) { return new HoverRegistrationOptions { - DocumentSelector = DocumentSelector.ForLanguage("dafny") + DocumentSelector = DocumentSelector.ForLanguage("dafny", "vjava") }; } diff --git a/Source/DafnyLanguageServer/Handlers/DafnyReferencesHandler.cs b/Source/DafnyLanguageServer/Handlers/DafnyReferencesHandler.cs index 439464ec788..edce27cfdad 100644 --- a/Source/DafnyLanguageServer/Handlers/DafnyReferencesHandler.cs +++ b/Source/DafnyLanguageServer/Handlers/DafnyReferencesHandler.cs @@ -23,7 +23,7 @@ public DafnyReferencesHandler(ILogger logger, IProjectDa protected override ReferenceRegistrationOptions CreateRegistrationOptions( ReferenceCapability capability, ClientCapabilities clientCapabilities) { return new ReferenceRegistrationOptions { - DocumentSelector = DocumentSelector.ForLanguage("dafny") + DocumentSelector = DocumentSelector.ForLanguage("dafny", "vjava") }; } diff --git a/Source/DafnyLanguageServer/Handlers/DafnyRenameHandler.cs b/Source/DafnyLanguageServer/Handlers/DafnyRenameHandler.cs index 49959112bc7..3cd961e94ec 100644 --- a/Source/DafnyLanguageServer/Handlers/DafnyRenameHandler.cs +++ b/Source/DafnyLanguageServer/Handlers/DafnyRenameHandler.cs @@ -24,7 +24,7 @@ public DafnyRenameHandler(ILogger logger, IProjectDatabase p protected override RenameRegistrationOptions CreateRegistrationOptions( RenameCapability capability, ClientCapabilities clientCapabilities) { return new RenameRegistrationOptions { - DocumentSelector = DocumentSelector.ForLanguage("dafny") + DocumentSelector = DocumentSelector.ForLanguage("dafny", "vjava") }; } diff --git a/Source/DafnyLanguageServer/Handlers/DafnySignatureHelpHandler.cs b/Source/DafnyLanguageServer/Handlers/DafnySignatureHelpHandler.cs index 742e271b042..bcc8ca06f7f 100644 --- a/Source/DafnyLanguageServer/Handlers/DafnySignatureHelpHandler.cs +++ b/Source/DafnyLanguageServer/Handlers/DafnySignatureHelpHandler.cs @@ -26,7 +26,7 @@ public DafnySignatureHelpHandler(ILogger logger, IPro protected override SignatureHelpRegistrationOptions CreateRegistrationOptions(SignatureHelpCapability capability, ClientCapabilities clientCapabilities) { return new SignatureHelpRegistrationOptions { - DocumentSelector = DocumentSelector.ForLanguage("dafny"), + DocumentSelector = DocumentSelector.ForLanguage("dafny", "vjava"), TriggerCharacters = new Container("(") }; } diff --git a/Source/DafnyLanguageServer/Handlers/DafnyTextDocumentHandler.cs b/Source/DafnyLanguageServer/Handlers/DafnyTextDocumentHandler.cs index 7bfb738d174..46bdbc9e796 100644 --- a/Source/DafnyLanguageServer/Handlers/DafnyTextDocumentHandler.cs +++ b/Source/DafnyLanguageServer/Handlers/DafnyTextDocumentHandler.cs @@ -50,13 +50,16 @@ public DafnyTextDocumentHandler( protected override TextDocumentSyncRegistrationOptions CreateRegistrationOptions(SynchronizationCapability capability, ClientCapabilities clientCapabilities) { return new TextDocumentSyncRegistrationOptions { - DocumentSelector = new DocumentSelector(DocumentFilter.ForLanguage(DafnyLanguage), DocumentFilter.ForPattern("**/*dfyconfig.toml")), + DocumentSelector = new DocumentSelector(DocumentFilter.ForLanguage(DafnyLanguage), + DocumentFilter.ForPattern("**/*dfyconfig.toml"), + DocumentFilter.ForLanguage("vjava")), Change = TextDocumentSyncKind.Incremental }; } public override TextDocumentAttributes GetTextDocumentAttributes(DocumentUri uri) { - return new TextDocumentAttributes(uri, uri.Path.EndsWith(DafnyProject.FileName) ? "toml" : DafnyLanguage); + return new TextDocumentAttributes(uri, uri.Path.EndsWith(DafnyProject.FileName) ? "toml" : + uri.Path.EndsWith(".vjava") ? "vjava": DafnyLanguage); } public override async Task Handle(DidOpenTextDocumentParams notification, CancellationToken cancellationToken) { diff --git a/Source/DafnyLanguageServer/Handlers/DafnyDefinitionHandler.cs b/Source/DafnyLanguageServer/Handlers/GotoDefinitionHandler.cs similarity index 88% rename from Source/DafnyLanguageServer/Handlers/DafnyDefinitionHandler.cs rename to Source/DafnyLanguageServer/Handlers/GotoDefinitionHandler.cs index dbb3683275e..63e5f61a465 100644 --- a/Source/DafnyLanguageServer/Handlers/DafnyDefinitionHandler.cs +++ b/Source/DafnyLanguageServer/Handlers/GotoDefinitionHandler.cs @@ -12,17 +12,17 @@ namespace Microsoft.Dafny.LanguageServer.Handlers { /// /// LSP handler responsible to resolve the location of a designator at the specified position. /// - public class DafnyDefinitionHandler : DefinitionHandlerBase { + public class GotoDefinitionHandler : DefinitionHandlerBase { private readonly ILogger logger; private readonly IProjectDatabase projects; - public DafnyDefinitionHandler(ILogger logger, IProjectDatabase projects) { + public GotoDefinitionHandler(ILogger logger, IProjectDatabase projects) { this.logger = logger; this.projects = projects; } protected override DefinitionRegistrationOptions CreateRegistrationOptions(DefinitionCapability capability, ClientCapabilities clientCapabilities) { return new DefinitionRegistrationOptions { - DocumentSelector = DocumentSelector.ForLanguage("dafny") + DocumentSelector = DocumentSelector.ForLanguage("dafny", "vjava") }; } diff --git a/Source/DafnyLanguageServer/Handlers/LanguageServerExtensions.cs b/Source/DafnyLanguageServer/Handlers/LanguageServerExtensions.cs index b7c9bba9ebd..1ff67abffab 100644 --- a/Source/DafnyLanguageServer/Handlers/LanguageServerExtensions.cs +++ b/Source/DafnyLanguageServer/Handlers/LanguageServerExtensions.cs @@ -22,7 +22,7 @@ public static LanguageServerOptions WithDafnyHandlers(this LanguageServerOptions .WithHandler() .WithHandler() .WithHandler() - .WithHandler() + .WithHandler() .WithHandler() .WithHandler() .WithHandler() diff --git a/Source/DafnyPipeline.Test/DafnyPipeline.Test.csproj b/Source/DafnyPipeline.Test/DafnyPipeline.Test.csproj index a98109bebaf..b7f5d13de5e 100644 --- a/Source/DafnyPipeline.Test/DafnyPipeline.Test.csproj +++ b/Source/DafnyPipeline.Test/DafnyPipeline.Test.csproj @@ -1,7 +1,7 @@ - net6.0 + net8.0 false diff --git a/Source/DafnyPipeline/DafnyPipeline.csproj b/Source/DafnyPipeline/DafnyPipeline.csproj index 35baf4ddff4..8dd6816186f 100644 --- a/Source/DafnyPipeline/DafnyPipeline.csproj +++ b/Source/DafnyPipeline/DafnyPipeline.csproj @@ -7,7 +7,7 @@ false ..\..\Binaries\ TRACE - net6.0 + net8.0 Major MIT diff --git a/Source/DafnyRuntime.Tests/DafnyRuntime.Tests.csproj b/Source/DafnyRuntime.Tests/DafnyRuntime.Tests.csproj index f90c85ef0bf..ee3d4cd8477 100644 --- a/Source/DafnyRuntime.Tests/DafnyRuntime.Tests.csproj +++ b/Source/DafnyRuntime.Tests/DafnyRuntime.Tests.csproj @@ -1,7 +1,7 @@ - net6.0 + net8.0 enable false diff --git a/Source/DafnyServer/DafnyServer.csproj b/Source/DafnyServer/DafnyServer.csproj index 38ee3311f28..c204599687d 100644 --- a/Source/DafnyServer/DafnyServer.csproj +++ b/Source/DafnyServer/DafnyServer.csproj @@ -5,7 +5,7 @@ DafnyServer false TRACE - net6.0 + net8.0 Major ..\..\Binaries\ MIT diff --git a/Source/DafnyTestGeneration.Test/DafnyTestGeneration.Test.csproj b/Source/DafnyTestGeneration.Test/DafnyTestGeneration.Test.csproj index b4920e58810..e12eab90d72 100644 --- a/Source/DafnyTestGeneration.Test/DafnyTestGeneration.Test.csproj +++ b/Source/DafnyTestGeneration.Test/DafnyTestGeneration.Test.csproj @@ -1,7 +1,7 @@ - net6.0 + net8.0 false diff --git a/Source/DafnyTestGeneration/DafnyTestGeneration.csproj b/Source/DafnyTestGeneration/DafnyTestGeneration.csproj index 6631561a0ed..ca8c71a7deb 100644 --- a/Source/DafnyTestGeneration/DafnyTestGeneration.csproj +++ b/Source/DafnyTestGeneration/DafnyTestGeneration.csproj @@ -8,7 +8,7 @@ ..\..\Binaries\ true TRACE - net6.0 + net8.0 Major enable false diff --git a/Source/IntegrationTests/IntegrationTests.csproj b/Source/IntegrationTests/IntegrationTests.csproj index 5370699a473..2d90bc485ca 100644 --- a/Source/IntegrationTests/IntegrationTests.csproj +++ b/Source/IntegrationTests/IntegrationTests.csproj @@ -1,7 +1,7 @@ - net6.0 + net8.0 true false enable diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/DafnyTests/RunAllTests/RunAllTests.csproj b/Source/IntegrationTests/TestFiles/LitTests/LitTest/DafnyTests/RunAllTests/RunAllTests.csproj index d8b5e8b41ad..eefc01ebbeb 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/DafnyTests/RunAllTests/RunAllTests.csproj +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/DafnyTests/RunAllTests/RunAllTests.csproj @@ -2,7 +2,7 @@ Exe - net6.0 + net8.0 false diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/DafnyTests/TestAttribute/TestAttribute.csproj b/Source/IntegrationTests/TestFiles/LitTests/LitTest/DafnyTests/TestAttribute/TestAttribute.csproj index 768e4f6f829..58a723cd452 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/DafnyTests/TestAttribute/TestAttribute.csproj +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/DafnyTests/TestAttribute/TestAttribute.csproj @@ -1,7 +1,7 @@  - net6.0 + net8.0 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/manualcompile/ManualCompile.csproj b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/manualcompile/ManualCompile.csproj index 41f1d5ad4b2..a269962b552 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/manualcompile/ManualCompile.csproj +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/manualcompile/ManualCompile.csproj @@ -2,7 +2,7 @@ Exe - net6.0 + net8.0 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/consumer/Consumer.csproj b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/consumer/Consumer.csproj index e6bb653223b..b32966d460e 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/consumer/Consumer.csproj +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/consumer/Consumer.csproj @@ -2,7 +2,7 @@ - net6.0 + net8.0 Exe diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/Simple_compiler/csharp/SimpleCompiler.csproj b/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/Simple_compiler/csharp/SimpleCompiler.csproj index c3a9eccf93e..5afee869737 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/Simple_compiler/csharp/SimpleCompiler.csproj +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/Simple_compiler/csharp/SimpleCompiler.csproj @@ -2,7 +2,7 @@ Exe - net6.0 + net8.0 enable CS3021; CS0162; CS0164 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/java/run/__default.java b/Source/IntegrationTests/TestFiles/LitTests/LitTest/java/run/__default.java new file mode 100644 index 00000000000..cceee038188 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/java/run/__default.java @@ -0,0 +1,7 @@ +package out; + +public class __default { + public static void println(int x) { + System.out.println(x); + } +} \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/java/run/run.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/java/run/run.dfy new file mode 100644 index 00000000000..55c37e0c555 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/java/run/run.dfy @@ -0,0 +1,36 @@ +// RUN: %run %S/run.vjava --input %S/run.dfy --input %S/__default.java --target=java > "%t" +// RUN: %translate vjava %S/run.vjava %S/run.dfy >> %t +// RUN: %diff "%s.expect" "%t" + +module {:extern} out { + newtype int32 = x: int | -0x8000_0000 <= x <= 0x7fff_ffff + method {:extern "println" } println(value: int32) +} + +// import opened Out + +// method Main() { +// println(3); +// } + +// import opened Java.Lang + +// method Main() { +// System.out.println(3); +// } + +// module {:extern "java"} Java { + +// module Base { +// newtype int32 = x: int | -0x8000_0000 <= x <= 0x7fff_ffff +// } + +// module {:extern "lang"} Lang { +// module {:extern} System { +// module {:extern "externs", "" } out { +// import opened Base +// method {:extern "println" } println(x: int32) +// } +// } +// } +// } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/java/run/run.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/java/run/run.dfy.expect new file mode 100644 index 00000000000..0071586d7f4 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/java/run/run.dfy.expect @@ -0,0 +1,3 @@ + +Dafny program verifier finished with 3 verified, 0 errors +3 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/java/run/run.vjava b/Source/IntegrationTests/TestFiles/LitTests/LitTest/java/run/run.vjava new file mode 100644 index 00000000000..89dbbb78073 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/java/run/run.vjava @@ -0,0 +1,14 @@ +import out; + +class Div { + static void Main() { + println(Foo(2)); // Should be System.out.println, issue with Java's {:externs} + } + + @Function + static int32 Foo(int32 x) // int32 should be int. Parser needs to map int to int32, but that requires inserting a JavaStdLib file + requires x != 0 + { + return 6 / x; + } +} \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/java/translate/translate.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/java/translate/translate.dfy new file mode 100644 index 00000000000..084372fb2ac --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/java/translate/translate.dfy @@ -0,0 +1,3 @@ +// RUN: %translate vjava %S/translate.vjava +// RUN: %diff "%s.expect" "%t" + diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/java/translate/translate.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/java/translate/translate.dfy.expect new file mode 100644 index 00000000000..89dbbb78073 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/java/translate/translate.dfy.expect @@ -0,0 +1,14 @@ +import out; + +class Div { + static void Main() { + println(Foo(2)); // Should be System.out.println, issue with Java's {:externs} + } + + @Function + static int32 Foo(int32 x) // int32 should be int. Parser needs to map int to int32, but that requires inserting a JavaStdLib file + requires x != 0 + { + return 6 / x; + } +} \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/java/translate/translate.vjava b/Source/IntegrationTests/TestFiles/LitTests/LitTest/java/translate/translate.vjava new file mode 100644 index 00000000000..d5bc53c7cb2 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/java/translate/translate.vjava @@ -0,0 +1,8 @@ +class Div { + @Function + static int32 Foo(int32 x) // int32 should be int. Parser needs to map int to int32, but that requires inserting a JavaStdLib file + requires x != 0 + { + return 6 / x; + } +} \ No newline at end of file diff --git a/Source/JavaSupport.Test/JavaSupport.Test.csproj b/Source/JavaSupport.Test/JavaSupport.Test.csproj new file mode 100644 index 00000000000..26edf9f1fc1 --- /dev/null +++ b/Source/JavaSupport.Test/JavaSupport.Test.csproj @@ -0,0 +1,27 @@ + + + + net8.0 + enable + enable + + false + true + + + + + + + + + + + + + + + + + + diff --git a/Source/JavaSupport.Test/TestJavaParsing.cs b/Source/JavaSupport.Test/TestJavaParsing.cs new file mode 100644 index 00000000000..28a56d0d08c --- /dev/null +++ b/Source/JavaSupport.Test/TestJavaParsing.cs @@ -0,0 +1,87 @@ +using CompilerBuilder; +using Microsoft.Dafny; +using Microsoft.VisualStudio.TestPlatform.Utilities; + +namespace JavaSupport.Test; + +public class TestJavaParsing { + [Fact] + public void TestFirstExample() { + var input = @" +package bar; + +class Div { + int Foo(int x) { + return 3 / x; + } +}"; + var jg = new JavaGrammar(new Uri(Directory.GetCurrentDirectory()), DafnyOptions.Default); + var programGrammar = jg.GetFinalGrammar(); + var parser = programGrammar.ToParser(); + var parseResult = parser.Parse(input); + Assert.NotNull(parseResult.ForceSuccess.Value); + } + + + // TODO mixed recursives should be part of the Java-agnostic test suite + [Fact] + public void TestRegression() { + var input = @" +package bar; + +class Foo { + int Foo() { + return a.b(c, d); + } +}".TrimStart(); + var jg = new JavaGrammar(new Uri(Directory.GetCurrentDirectory()), DafnyOptions.Default); + var programGrammar = jg.GetFinalGrammar(); + var parser = programGrammar.ToParser(); + var parseResult = parser.Parse(input); + Assert.NotNull(parseResult.ForceSuccess.Value); + } + + [Fact] + public void TestSecondExample() { + var input = @" +package bar; + +class Fib { + static int FibonacciSpec(int n) { + return n < 2 ? n : FibonacciSpec(n - 1) + FibonacciSpec(n - 2); + } + + static int Fibonacci(int n) + // ensures result == FibonacciSpec(n) + { + if (n == 0) { + return 0; + } + + int iMinMinResult = 0; + int iResult = 1; + int i = 1; + while(i < n) + // invariant iResult == FibonacciSpec(i) + // invariant iMinMinResult == FibonacciSpec(i - 1) + // invariant i <= n + { + i = i + 1; + int temp = iResult + iMinMinResult; + iMinMinResult = iResult; + iResult = temp; + } + return iResult; + } +}"; + var jg = new JavaGrammar(new Uri(Directory.GetCurrentDirectory()), DafnyOptions.Default); + var programGrammar = jg.GetFinalGrammar(); + var parser = programGrammar.ToParser(); + var parseResult = parser.Parse(input); + Assert.NotNull(parseResult.ForceSuccess.Value); + var cloner = new Cloner(); + var cloned = new FileModuleDefinition(cloner, parseResult.ForceSuccess.Value); + var printer = programGrammar.ToPrinter(); + var s = printer.Print(cloned).ForceSuccess.RenderAsString(); + } +} \ No newline at end of file diff --git a/Source/JavaSupport/JavaSupport.csproj b/Source/JavaSupport/JavaSupport.csproj new file mode 100644 index 00000000000..4699b6c5cc1 --- /dev/null +++ b/Source/JavaSupport/JavaSupport.csproj @@ -0,0 +1,15 @@ + + + + Library + net8.0 + enable + enable + + + + + + + + diff --git a/Source/TestDafny/TestDafny.csproj b/Source/TestDafny/TestDafny.csproj index 83f292e7923..4865653669c 100644 --- a/Source/TestDafny/TestDafny.csproj +++ b/Source/TestDafny/TestDafny.csproj @@ -2,7 +2,7 @@ Exe - net6.0 + net8.0 enable enable false diff --git a/Source/XUnitExtensions/XUnitExtensions.csproj b/Source/XUnitExtensions/XUnitExtensions.csproj index 3ff901352c0..3ee91d23d07 100644 --- a/Source/XUnitExtensions/XUnitExtensions.csproj +++ b/Source/XUnitExtensions/XUnitExtensions.csproj @@ -1,7 +1,7 @@ - net6.0 + net8.0 false enable