Docstring + sources for generated Rust code (#5945)

### Description - Dafny now emits the Dafny docstring as a Rust docstring - The Rust docstring also includes the filename as a relative path (with / for folders on all OS) for everything that support docstring (except datatype constructors) - Rules for parsing Docstring have been unified across all declarations and definitions. Previously, simple `//` comments after declarations were interpreted as multi-line docstrings, when it could be ambiguously referring to the next declaration. The new rules are as follow: - Trailing trivia now parses at most one single-line comment. - If there is a `/**` comment right before a declaration, it's the docstring - Else if there is one or more comment between the declaration and the definition (when there is one), it's the docstring - Else if there is one comment in the trailing trivia of the entire declaration + definition, it's the docstring. ## Refactorings and minor edits - Where clauses of functions have been removed - `AsRefDatatypeImpl`, `DefaultDatatypeImpl` have been moved to the definitions files. - Use of the constant `R.NoAttr` in places where an empty attribute sequence is provided. Same for the new `R.NoDoc` ### How has this been tested? - I added tests covering all the cases I could think of for docstring for every Dafny construct supporting docstring - I added a test verifying that the generated Rust code contains the docstring as well as at least one file location <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small> --------- Co-authored-by: Fabio Madge <[email protected]>
dafny-lang · Dec 4, 2024 · 81b8216 · 81b8216
1 parent 1ce0682
commit 81b8216
Show file tree

Hide file tree

Showing 54 changed files with 1,871 additions and 803 deletions.
diff --git a/Source/DafnyCore.Test/GeneratedFromDafny/DefsCoverage.cs b/Source/DafnyCore.Test/GeneratedFromDafny/DefsCoverage.cs
@@ -18,7 +18,7 @@ public partial class __default {
     public static void Expect(bool x)
     {
       if (!(x)) {
-        throw new Dafny.HaltException("Backends/Rust/Dafny-compiler-rust-definitions.dfy(789,4): " + Dafny.Sequence<Dafny.Rune>.UnicodeFromString("expectation violation").ToVerbatimString(false));}
+        throw new Dafny.HaltException("Backends/Rust/Dafny-compiler-rust-definitions-coverage.dfy(17,4): " + Dafny.Sequence<Dafny.Rune>.UnicodeFromString("expectation violation").ToVerbatimString(false));}
     }
     public static void Tests()
     {

diff --git a/Source/DafnyCore.Test/GeneratedFromDafny/FactorPathsOptimizationTest.cs b/Source/DafnyCore.Test/GeneratedFromDafny/FactorPathsOptimizationTest.cs
diff --git a/Source/DafnyCore/AST/Members/Field.cs b/Source/DafnyCore/AST/Members/Field.cs
@@ -91,11 +91,21 @@ public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) {
   }
 
   public string GetTriviaContainingDocstring() {
-    if (EndToken.TrailingTrivia.Trim() != "") {
-      return EndToken.TrailingTrivia;
+    if (GetStartTriviaDocstring(out var triviaFound)) {
+      return triviaFound;
+    }
+    foreach (var token in OwnedTokens) {
+      if (token.val == ":=") {
+        if ((token.Prev.TrailingTrivia + (token.LeadingTrivia ?? "")).Trim() is { } tentativeTrivia and not "") {
+          return tentativeTrivia;
+        }
+      }
+    }
+    if (EndToken.TrailingTrivia.Trim() is { } tentativeTrivia2 and not "") {
+      return tentativeTrivia2;
     }
 
-    return GetTriviaContainingDocstringFromStartTokenOrNull();
+    return null;
   }
 
   public override SymbolKind? Kind => SymbolKind.Field;

diff --git a/Source/DafnyCore/AST/Members/Function.cs b/Source/DafnyCore/AST/Members/Function.cs
@@ -483,17 +483,30 @@ public override void Resolve(ModuleResolver resolver) {
   }
 
   public string GetTriviaContainingDocstring() {
+    if (GetStartTriviaDocstring(out var triviaFound)) {
+      return triviaFound;
+    }
 
     var endTokenDefinition =
-      OwnedTokens.LastOrDefault(token => token.val == ")" || token.pos == ResultType.EndToken.pos)
-      ?? EndToken;
-    if (endTokenDefinition.TrailingTrivia.Trim() != "") {
-      return endTokenDefinition.TrailingTrivia;
+      OwnedTokens.LastOrDefault(token => token.val == ")" || token.pos == ResultType.EndToken.pos);
+    var tentativeTrivia = "";
+    if (endTokenDefinition != null) {
+      if (endTokenDefinition.pos < this.EndToken.pos) { // All comments are docstring
+        tentativeTrivia = (endTokenDefinition.TrailingTrivia + endTokenDefinition.Next.LeadingTrivia).Trim();
+      } else {
+        // Comments at the end of bodiless functions
+        tentativeTrivia = endTokenDefinition.TrailingTrivia.Trim();
+      }
+      if (tentativeTrivia != "") {
+        return tentativeTrivia;
+      }
     }
 
-    if (StartToken.LeadingTrivia.Trim() != "") {
-      return StartToken.LeadingTrivia;
+    tentativeTrivia = EndToken.TrailingTrivia.Trim();
+    if (tentativeTrivia != "") {
+      return tentativeTrivia;
     }
+
     return null;
   }
 

diff --git a/Source/DafnyCore/AST/Members/Method.cs b/Source/DafnyCore/AST/Members/Method.cs
@@ -386,18 +386,36 @@ public override void Resolve(ModuleResolver resolver) {
   }
 
   public string GetTriviaContainingDocstring() {
+    if (GetStartTriviaDocstring(out var triviaFound)) {
+      return triviaFound;
+    }
+
     IOrigin lastClosingParenthesis = null;
     foreach (var token in OwnedTokens) {
       if (token.val == ")") {
         lastClosingParenthesis = token;
       }
     }
 
-    if (lastClosingParenthesis != null && lastClosingParenthesis.TrailingTrivia.Trim() != "") {
-      return lastClosingParenthesis.TrailingTrivia;
+    var tentativeTrivia = "";
+    if (lastClosingParenthesis != null) {
+      if (lastClosingParenthesis.pos < EndToken.pos) {
+        tentativeTrivia = (lastClosingParenthesis.TrailingTrivia + lastClosingParenthesis.Next.LeadingTrivia).Trim();
+      } else {
+        tentativeTrivia = lastClosingParenthesis.TrailingTrivia.Trim();
+      }
+
+      if (tentativeTrivia != "") {
+        return tentativeTrivia;
+      }
+    }
+
+    tentativeTrivia = EndToken.TrailingTrivia.Trim();
+    if (tentativeTrivia != "") {
+      return tentativeTrivia;
     }
 
-    return GetTriviaContainingDocstringFromStartTokenOrNull();
+    return null;
   }
 
   public override SymbolKind? Kind => SymbolKind.Method;

diff --git a/Source/DafnyCore/AST/Modules/LiteralModuleDecl.cs b/Source/DafnyCore/AST/Modules/LiteralModuleDecl.cs
@@ -42,14 +42,13 @@ public LiteralModuleDecl(Cloner cloner, LiteralModuleDecl original, ModuleDefini
     ModuleDef = newModuleDefinition;
     DefaultExport = original.DefaultExport;
     BodyStartTok = ModuleDef.BodyStartTok;
-    TokenWithTrailingDocString = ModuleDef.TokenWithTrailingDocString;
   }
 
   public LiteralModuleDecl(DafnyOptions options, ModuleDefinition module, ModuleDefinition parent, Guid cloneId)
     : base(options, module.RangeToken, module.NameNode, parent, false, false, cloneId) {
     ModuleDef = module;
     BodyStartTok = module.BodyStartTok;
-    TokenWithTrailingDocString = module.TokenWithTrailingDocString;
+    module.EnclosingLiteralModuleDecl = this;
   }
 
   public override object Dereference() { return ModuleDef; }

diff --git a/Source/DafnyCore/AST/Modules/ModuleDecl.cs b/Source/DafnyCore/AST/Modules/ModuleDecl.cs
@@ -61,24 +61,24 @@ public override bool IsEssentiallyEmpty() {
   }
 
   public virtual string GetTriviaContainingDocstring() {
-    IOrigin candidate = null;
+    if (GetStartTriviaDocstring(out var triviaFound)) {
+      return triviaFound;
+    }
     var tokens = OwnedTokens.Any() ?
       OwnedTokens :
       PreResolveChildren.Any() ? PreResolveChildren.First().OwnedTokens : Enumerable.Empty<IOrigin>();
     foreach (var token in tokens) {
       if (token.val == "{") {
-        candidate = token.Prev;
-        if (candidate.TrailingTrivia.Trim() != "") {
-          return candidate.TrailingTrivia;
+        if ((token.Prev.TrailingTrivia + token.LeadingTrivia).Trim() is { } tentativeTrivia and not "") {
+          return tentativeTrivia;
         }
       }
     }
-
-    if (candidate == null && EndToken.TrailingTrivia.Trim() != "") {
-      return EndToken.TrailingTrivia;
+    if (EndToken.TrailingTrivia.Trim() is { } tentativeTrivia2 and not "") {
+      return tentativeTrivia2;
     }
 
-    return GetTriviaContainingDocstringFromStartTokenOrNull();
+    return null;
   }
 
   public override SymbolKind? Kind => SymbolKind.Namespace;

diff --git a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs
@@ -41,7 +41,6 @@ static ModuleDefinition() {
   }
 
   public IOrigin BodyStartTok = Token.NoToken;
-  public IOrigin TokenWithTrailingDocString = Token.NoToken;
   public string DafnyName => NameNode.StartToken.val; // The (not-qualified) name as seen in Dafny source code
   public Name NameNode; // (Last segment of the) module name
 
@@ -1078,6 +1077,8 @@ bool InheritsFromObject(TraitDecl traitDecl) {
   });
 
   public SymbolKind? Kind => SymbolKind.Namespace;
+  public LiteralModuleDecl EnclosingLiteralModuleDecl { get; set; }
+
   public string GetDescription(DafnyOptions options) {
     return $"module {Name}";
   }

diff --git a/Source/DafnyCore/AST/Modules/ModuleExportDecl.cs b/Source/DafnyCore/AST/Modules/ModuleExportDecl.cs
@@ -98,10 +98,25 @@ public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) {
   }
 
   public override string GetTriviaContainingDocstring() {
-    if (Tok.TrailingTrivia.Trim() != "") {
-      return Tok.TrailingTrivia;
+    if (GetStartTriviaDocstring(out var triviaFound)) {
+      return triviaFound;
     }
 
-    return GetTriviaContainingDocstringFromStartTokenOrNull();
+    var tentativeTrivia = "";
+    if (Tok.pos < EndToken.pos) {
+      tentativeTrivia = (Tok.TrailingTrivia + Tok.Next.LeadingTrivia).Trim();
+    } else {
+      tentativeTrivia = Tok.TrailingTrivia.Trim();
+    }
+    if (tentativeTrivia != "") {
+      return tentativeTrivia;
+    }
+
+    tentativeTrivia = EndToken.TrailingTrivia.Trim();
+    if (tentativeTrivia != "") {
+      return tentativeTrivia;
+    }
+
+    return null;
   }
 }
diff --git a/Source/DafnyCore/AST/TypeDeclarations/AbstractTypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/AbstractTypeDecl.cs
@@ -88,21 +88,29 @@ public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) {
   }
 
   public string GetTriviaContainingDocstring() {
+    if (GetStartTriviaDocstring(out var triviaFound)) {
+      return triviaFound;
+    }
     IOrigin openingBlock = null;
     foreach (var token in OwnedTokens) {
       if (token.val == "{") {
         openingBlock = token;
       }
     }
 
-    if (openingBlock != null && openingBlock.Prev.TrailingTrivia.Trim() != "") {
-      return openingBlock.Prev.TrailingTrivia;
+    var tentativeTrivia = "";
+    if (openingBlock != null) {
+      tentativeTrivia = (openingBlock.Prev.TrailingTrivia + openingBlock.LeadingTrivia).Trim();
+      if (tentativeTrivia != "") {
+        return tentativeTrivia;
+      }
     }
 
-    if (openingBlock == null && EndToken.TrailingTrivia.Trim() != "") {
-      return EndToken.TrailingTrivia;
+    tentativeTrivia = EndToken.TrailingTrivia.Trim();
+    if (tentativeTrivia != "") {
+      return tentativeTrivia;
     }
 
-    return GetTriviaContainingDocstringFromStartTokenOrNull();
+    return null;
   }
 }
diff --git a/Source/DafnyCore/AST/TypeDeclarations/ClassLikeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/ClassLikeDecl.cs
@@ -78,20 +78,22 @@ public virtual bool SetIndent(int indentBefore, TokenNewIndentCollector formatte
   }
 
   public virtual string GetTriviaContainingDocstring() {
-    IOrigin candidate = null;
+    if (GetStartTriviaDocstring(out var triviaFound)) {
+      return triviaFound;
+    }
+
     foreach (var token in OwnedTokens) {
       if (token.val == "{") {
-        candidate = token.Prev;
-        if (candidate.TrailingTrivia.Trim() != "") {
-          return candidate.TrailingTrivia;
+        if ((token.Prev.TrailingTrivia + token.LeadingTrivia).Trim() is { } tentativeTrivia and not "") {
+          return tentativeTrivia;
         }
       }
     }
 
-    if (candidate == null && EndToken.TrailingTrivia.Trim() != "") {
-      return EndToken.TrailingTrivia;
+    if (EndToken.TrailingTrivia.Trim() is { } tentativeTrivia2 and not "") {
+      return tentativeTrivia2;
     }
 
-    return GetTriviaContainingDocstringFromStartTokenOrNull();
+    return null;
   }
 }
diff --git a/Source/DafnyCore/AST/TypeDeclarations/DatatypeCtor.cs b/Source/DafnyCore/AST/TypeDeclarations/DatatypeCtor.cs
@@ -43,11 +43,16 @@ public string FullName {
   }
 
   public string GetTriviaContainingDocstring() {
-    if (EndToken.TrailingTrivia.Trim() != "") {
-      return EndToken.TrailingTrivia;
+    if (GetStartTriviaDocstring(out var triviaFound)) {
+      return triviaFound;
     }
 
-    return GetTriviaContainingDocstringFromStartTokenOrNull();
+    var tentativeTrivia = EndToken.TrailingTrivia.Trim();
+    if (tentativeTrivia != "") {
+      return tentativeTrivia;
+    }
+
+    return null;
   }
 
   public override SymbolKind? Kind => SymbolKind.EnumMember;

diff --git a/Source/DafnyCore/AST/TypeDeclarations/DatatypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/DatatypeDecl.cs
@@ -180,13 +180,18 @@ public bool SetIndent(int indent, TokenNewIndentCollector formatter) {
   }
 
   public string GetTriviaContainingDocstring() {
+    if (GetStartTriviaDocstring(out var triviaFound)) {
+      return triviaFound;
+    }
     foreach (var token in OwnedTokens) {
-      if (token.val == "=" && token.TrailingTrivia.Trim() != "") {
-        return token.TrailingTrivia;
+      if (token.val == "=") {
+        if ((token.Prev.TrailingTrivia + (token.LeadingTrivia ?? "")).Trim() is { } tentativeTrivia and not "") {
+          return tentativeTrivia;
+        }
       }
     }
 
-    return GetTriviaContainingDocstringFromStartTokenOrNull();
+    return null;
   }
 
   public void AutoRevealDependencies(AutoRevealFunctionDependencies Rewriter, DafnyOptions Options, ErrorReporter Reporter) {

diff --git a/Source/DafnyCore/AST/TypeDeclarations/Declaration.cs b/Source/DafnyCore/AST/TypeDeclarations/Declaration.cs
@@ -13,7 +13,6 @@ void ObjectInvariant() {
   }
 
   public IOrigin BodyStartTok = Token.NoToken;
-  public IOrigin TokenWithTrailingDocString = Token.NoToken;
   public Name NameNode;
 
   public override IOrigin Tok => NameNode.StartToken;

diff --git a/Source/DafnyCore/AST/TypeDeclarations/IteratorDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/IteratorDecl.cs
@@ -501,18 +501,36 @@ public void Resolve(ModuleResolver resolver) {
   }
 
   public override string GetTriviaContainingDocstring() {
+    if (GetStartTriviaDocstring(out var triviaFound)) {
+      return triviaFound;
+    }
+
     IOrigin lastClosingParenthesis = null;
     foreach (var token in OwnedTokens) {
       if (token.val == ")") {
         lastClosingParenthesis = token;
       }
     }
 
-    if (lastClosingParenthesis != null && lastClosingParenthesis.TrailingTrivia.Trim() != "") {
-      return lastClosingParenthesis.TrailingTrivia;
+    var tentativeTrivia = "";
+    if (lastClosingParenthesis != null) {
+      if (lastClosingParenthesis.pos < EndToken.pos) {
+        tentativeTrivia = (lastClosingParenthesis.TrailingTrivia + lastClosingParenthesis.Next.LeadingTrivia).Trim();
+      } else {
+        tentativeTrivia = lastClosingParenthesis.TrailingTrivia.Trim();
+      }
+
+      if (tentativeTrivia != "") {
+        return tentativeTrivia;
+      }
+    }
+
+    tentativeTrivia = EndToken.TrailingTrivia.Trim();
+    if (tentativeTrivia != "") {
+      return tentativeTrivia;
     }
 
-    return GetTriviaContainingDocstringFromStartTokenOrNull();
+    return null;
   }
   public bool ShouldVerify => true; // This could be made more accurate
   public ModuleDefinition ContainingModule => EnclosingModuleDefinition;

diff --git a/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs
@@ -151,21 +151,23 @@ public override bool IsEssentiallyEmpty() {
   }
 
   public string GetTriviaContainingDocstring() {
-    IOrigin candidate = null;
+    if (GetStartTriviaDocstring(out var triviaFound)) {
+      return triviaFound;
+    }
+
     foreach (var token in OwnedTokens) {
-      if (token.val == "{") {
-        candidate = token.Prev;
-        if (candidate.TrailingTrivia.Trim() != "") {
-          return candidate.TrailingTrivia;
+      if (token.val == "=") {
+        if ((token.Prev.TrailingTrivia + token.LeadingTrivia).Trim() is { } tentativeTrivia1 and not "") {
+          return tentativeTrivia1;
         }
       }
     }
 
-    if (candidate == null && EndToken.TrailingTrivia.Trim() != "") {
-      return EndToken.TrailingTrivia;
+    if (EndToken.TrailingTrivia.Trim() is { } tentativeTrivia and not "") {
+      return tentativeTrivia;
     }
 
-    return GetTriviaContainingDocstringFromStartTokenOrNull();
+    return null;
   }
 
   public ModuleDefinition ContainingModule => EnclosingModuleDefinition;