Skip to content

Commit

Permalink
Fix: Generated Rust docstring no longer crashes cargo doc
Browse files Browse the repository at this point in the history 
Fixes #6084

Previously, Dafny docstring was literally transformed to Rust docstring. However, Rust docstring follows a markdown syntax where non-labelled code blocks are interpreted and checked as Rust code when running `cargo doc`.
Rather than creating a flag to avoid the docstring, this PR does a lightweight parsing on the docstring to ensures that:
* In docstrings, Code blocks without label are written using the "dafny" label so that they are not interpreted as Rust
* In docstrings, text that has a certain level of indentation has its first space replaced by a vertical bar so that we make sure it's not interpreted as Rust code.

I added Dafny tests for the new function that converts docstrings, and also an integration test that verifies that 'cargo doc' works on the already existing but modified docstring.dfy test.
  • Loading branch information
@MikaelMayer
MikaelMayer committed Jan 28, 2025
1 parent 18c538a commit 175ee9f
Show file tree
Hide file tree
Showing 8 changed files with 516 additions and 12 deletions.
131 changes: 131 additions & 0 deletions Source/DafnyCore.Test/GeneratedFromDafny/RASTCoverage.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,14 +20,142 @@ public static void AssertCoverage(bool x)
if (!(x)) {
throw new Dafny.HaltException("Backends/Rust/Dafny-compiler-rust-coverage.dfy(26,4): " + Dafny.Sequence<Dafny.Rune>.UnicodeFromString("expectation violation").ToVerbatimString(false));}
}
public static void AssertEq<__T>(__T x, __T y)
{
if (!(object.Equals(x, y))) {
throw new Dafny.HaltException("Backends/Rust/Dafny-compiler-rust-coverage.dfy(30,4): " + Dafny.Sequence<Dafny.Rune>.UnicodeFromString("expectation violation").ToVerbatimString(false));}
}
public static void TestExpr()
{
RASTCoverage.__default.TestOptimizeToString();
RASTCoverage.__default.TestPrintingInfo();
RASTCoverage.__default.TestNoExtraSemicolonAfter();
RASTCoverage.__default.TestDocstring();
}
public static Dafny.ISequence<Dafny.Rune> CanonicalNewlines(Dafny.ISequence<Dafny.Rune> s) {
Dafny.ISequence<Dafny.Rune> _0___accumulator = Dafny.Sequence<Dafny.Rune>.FromElements();
TAIL_CALL_START: ;
if ((new BigInteger((s).Count)).Sign == 0) {
return Dafny.Sequence<Dafny.Rune>.Concat(_0___accumulator, Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""));
} else if (((s).Select(BigInteger.Zero)) == (new Dafny.Rune('\r'))) {
if (((new BigInteger((s).Count)) > (BigInteger.One)) && (((s).Select(BigInteger.One)) == (new Dafny.Rune('\n')))) {
_0___accumulator = Dafny.Sequence<Dafny.Rune>.Concat(_0___accumulator, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("\n"));
Dafny.ISequence<Dafny.Rune> _in0 = (s).Drop(new BigInteger(2));
s = _in0;
goto TAIL_CALL_START;
} else {
_0___accumulator = Dafny.Sequence<Dafny.Rune>.Concat(_0___accumulator, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("\n"));
Dafny.ISequence<Dafny.Rune> _in1 = (s).Drop(BigInteger.One);
s = _in1;
goto TAIL_CALL_START;
}
} else {
_0___accumulator = Dafny.Sequence<Dafny.Rune>.Concat(_0___accumulator, (s).Take(BigInteger.One));
Dafny.ISequence<Dafny.Rune> _in2 = (s).Drop(BigInteger.One);
s = _in2;
goto TAIL_CALL_START;
}
}
public static void TestOneDocstring(Dafny.ISequence<Dafny.Rune> dafnyDocstring, Dafny.ISequence<Dafny.Rune> rustDocstring, Dafny.ISequence<Dafny.Rune> indent)
{
RASTCoverage.__default.AssertEq<Dafny.ISequence<Dafny.Rune>>(RAST.__default.ConvertDocstring(RASTCoverage.__default.CanonicalNewlines(dafnyDocstring), indent, true, Std.Wrappers.Option<Dafny.ISequence<Dafny.Rune>>.create_None()), RASTCoverage.__default.CanonicalNewlines(rustDocstring));
}
public static void TestDocstring()
{
RASTCoverage.__default.TestOneDocstring(Dafny.Sequence<Dafny.Rune>.UnicodeFromString(@"
Hello
World"), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(@"
/// Hello
/// World"), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(" "));
RASTCoverage.__default.TestOneDocstring(Dafny.Sequence<Dafny.Rune>.UnicodeFromString(@"
Title
```rs
let mut x = 1;
```
End comment"), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(@"
/// Title
/// ```
/// let mut x = 1;
/// ```
/// End comment"), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(" "));
RASTCoverage.__default.TestOneDocstring(Dafny.Sequence<Dafny.Rune>.UnicodeFromString(@"
Title
`````rs
let mut x = 1;
`````
End comment"), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(@"
/// Title
/// `````
/// let mut x = 1;
/// `````
/// End comment"), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(" "));
RASTCoverage.__default.TestOneDocstring(Dafny.Sequence<Dafny.Rune>.UnicodeFromString(@"
Title
```
var x := 1;
```
End comment"), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(@"
/// Title
/// ```dafny
/// var x := 1;
/// ```
/// End comment"), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(" "));
RASTCoverage.__default.TestOneDocstring(Dafny.Sequence<Dafny.Rune>.UnicodeFromString(@"
Title
`````
var x := 1;
`````
End comment"), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(@"
/// Title
/// `````dafny
/// var x := 1;
/// `````
/// End comment"), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(" "));
RASTCoverage.__default.TestOneDocstring(Dafny.Sequence<Dafny.Rune>.UnicodeFromString(@"
Title
`````md
# title
```
code
```
Outside of code
`````
```
dafnycode
```
End comment"), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(@"
/// Title
/// `````md
/// # title
/// ```
/// code
/// ```
/// Outside of code
/// `````
/// ```dafny
/// dafnycode
/// ```
/// End comment"), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(" "));
RASTCoverage.__default.TestOneDocstring(Dafny.Sequence<Dafny.Rune>.UnicodeFromString(@"
Title
Indented code
More indented code
Back to normal
Normal as well
Also normal
But this one indented"), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(@"
/// Title
/// | Indented code
/// | More indented code
/// Back to normal
/// Normal as well
/// Also normal
/// | But this one indented"), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(" "));
}
public static void TestNoOptimize(RAST._IExpr e)
{
if (!(object.Equals((RASTCoverage.__default.ExprSimp).ReplaceExpr(e), e))) {
throw new Dafny.HaltException("Backends/Rust/Dafny-compiler-rust-coverage.dfy(157,4): " + Dafny.Sequence<Dafny.Rune>.UnicodeFromString("expectation violation").ToVerbatimString(false));}
}
public static RAST._IExpr ConversionNum(RAST._IType t, RAST._IExpr x)
{
Expand Down Expand Up @@ -161,5 +289,8 @@ public static void TestNoExtraSemicolonAfter()
RASTCoverage.__default.AssertCoverage((RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("x"), Std.Wrappers.Option<RAST._IType>.create_None(), Std.Wrappers.Option<RAST._IExpr>.create_None())).NoExtraSemicolonAfter());
RASTCoverage.__default.AssertCoverage(!((RAST.Expr.create_Identifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("x"))).NoExtraSemicolonAfter()));
}
public static RAST._IRASTBottomUpReplacer ExprSimp { get {
return ExpressionOptimization.__default.ExprSimplifier();
} }
}
} // end of namespace RASTCoverage
122 changes: 121 additions & 1 deletion Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-coverage.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,16 +25,136 @@ module RASTCoverage {
{
expect x;
}
method AssertEq<T(==)>(x: T, y: T)
{
expect x == y;
}


method TestExpr() {
TestOptimizeToString();
TestPrintingInfo();
TestNoExtraSemicolonAfter();
TestDocstring();
}

function CanonicalNewlines(s: string): string {
if |s| == 0 then "" else
if s[0] == '\r' then
if |s| > 1 && s[1] == '\n' then
"\n" + CanonicalNewlines(s[2..])
else
"\n" + CanonicalNewlines(s[1..])
else
s[..1] + CanonicalNewlines(s[1..])
}

method TestOneDocstring(dafnyDocstring: string, rustDocstring: string, indent: string := " ") {
AssertEq(
ConvertDocstring(
CanonicalNewlines(dafnyDocstring),
indent
), CanonicalNewlines(rustDocstring));
}

method TestDocstring() {
TestOneDocstring(@"
Hello
World",
@"
/// Hello
/// World");
TestOneDocstring(@"
Title
```rs
let mut x = 1;
```
End comment", @"
/// Title
/// ```
/// let mut x = 1;
/// ```
/// End comment");
TestOneDocstring(@"
Title
`````rs
let mut x = 1;
`````
End comment", @"
/// Title
/// `````
/// let mut x = 1;
/// `````
/// End comment");
TestOneDocstring(@"
Title
```
var x := 1;
```
End comment", @"
/// Title
/// ```dafny
/// var x := 1;
/// ```
/// End comment");
TestOneDocstring(@"
Title
`````
var x := 1;
`````
End comment", @"
/// Title
/// `````dafny
/// var x := 1;
/// `````
/// End comment");
TestOneDocstring(@"
Title
`````md
# title
```
code
```
Outside of code
`````
```
dafnycode
```
End comment", @"
/// Title
/// `````md
/// # title
/// ```
/// code
/// ```
/// Outside of code
/// `````
/// ```dafny
/// dafnycode
/// ```
/// End comment");
TestOneDocstring(@"
Title
Indented code
More indented code
Back to normal
Normal as well
Also normal
But this one indented", @"
/// Title
/// | Indented code
/// | More indented code
/// Back to normal
/// Normal as well
/// Also normal
/// | But this one indented");
}

const ExprSimp := ExpressionOptimization.ExprSimplifier()

method TestNoOptimize(e: Expr)
//requires e.Optimize() == e // Too expensive
{
expect ExprSimp.ReplaceExpr(e) == e;
}

function ConversionNum(t: Type, x: Expr): Expr {
Expand Down
23 changes: 22 additions & 1 deletion Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-proofs.dfy
View file
Original file line number Diff line number Diff line change
@@ -1,8 +1,29 @@
include "../Dafny/AST.dfy"

/*This module does not contain any compiled code because it
/*These modules do not contain any compiled code because they
only proves properties about DCOMP. In a sense, it's a test file. */
@Compile(false)
module {:extern "RASTProofs"} RASTProofs {
import opened RAST
lemma AboutGatherSimpleQuotes(docstring: string, acc: string)
ensures
var r := GatherSimpleQuotes(docstring, acc);
&& |acc| <= |r|
&& |r[|acc|..]| <= |docstring|
&& r == acc + docstring[..|r[|acc|..]|]
&& (forall i | |acc| <= i < |r| :: r[i] == '`')
&& (|docstring| > |r[|acc|..]| ==>
docstring[|r[|acc|..]|] != '`')
{
var r := GatherSimpleQuotes(docstring, acc);
if |docstring| == 0 || docstring[0] != '`' {

} else {

}
}
}
@Compile(false)
module {:extern "DafnyToRustCompilerProofs"} DafnyToRustCompilerProofs {
import opened DafnyToRustCompiler
import opened DafnyToRustCompilerDefinitions
Expand Down
56 changes: 55 additions & 1 deletion Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-rast.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,8 @@ module RAST
// Default Rust-like indentation
const IND := " "

const DocStringPrefix: string := "/// "

datatype RASTTopDownVisitor<!T(!new)> =
RASTTopDownVisitor(
nameonly VisitTypeSingle: (T, Type) -> T,
Expand Down Expand Up @@ -351,9 +353,61 @@ module RAST
else FoldLeft(f, f(init, xs[0]), xs[1..])
}

function GatherSimpleQuotes(docstring: string, acc: string := ""): (r: string)
ensures |r| <= |acc| + |docstring|
{
if |docstring| == 0 || docstring[0] != '`' then acc else
GatherSimpleQuotes(docstring[1..], acc + "`")
}

// Converts Dafny docstring into Rust docstring that won't normally cause issue with `cargo doc`
// - Escape blocks ```...``` to ```dafny ...``` but keep ```rs...``` intact
// - Every line starting with 4 or more spaces gets its first space replaced by a `|`
function ConvertDocstring(dafnyDocstring: string, ind: string, newlineStarted: bool := true, codeMarker: Option<string> := None): string {
if |dafnyDocstring| == 0 then dafnyDocstring
else if dafnyDocstring[0] == '\n' then
"\n" + ind + DocStringPrefix + ConvertDocstring(dafnyDocstring[1..], ind, true, codeMarker)
else if dafnyDocstring[0] == ' ' then
if codeMarker.None? && newlineStarted && |dafnyDocstring| > 4 && dafnyDocstring[..4] == " " then
"| " + ConvertDocstring(dafnyDocstring[4..], ind, false, codeMarker)
else
" " + ConvertDocstring(dafnyDocstring[1..], ind, newlineStarted, codeMarker)
else if newlineStarted then
if && codeMarker.Some?
&& |dafnyDocstring| >= |codeMarker.value| + 1
&& dafnyDocstring[..|codeMarker.value| + 1] == codeMarker.value + "\n" then
// End of code delimiter
codeMarker.value + ConvertDocstring(dafnyDocstring[|codeMarker.value|..], ind, false, None)
else if codeMarker.None? && |dafnyDocstring| >= 3 then
var prefix := dafnyDocstring[..3];
if prefix == "```" then
var prefix := GatherSimpleQuotes(dafnyDocstring);
var remaining := dafnyDocstring[|prefix|..];
if |remaining| == 0 || remaining[0] == ' ' || remaining[0] == '\n' then
// ``` becomes ```dafny
// It's Dafny docstring, we want to ensure we add the Dafny identifier there
prefix + "dafny" + ConvertDocstring(dafnyDocstring[|prefix|..], ind, false, Some(prefix))
else if && |remaining| >= 3
&& remaining[..2] == "rs"
&& (remaining[2] == ' ' || remaining[2] == '\n') then
// ```rs becomes ```
prefix + ConvertDocstring(dafnyDocstring[|prefix|+2..], ind, false, Some(prefix))
else
prefix + ConvertDocstring(dafnyDocstring[|prefix|..], ind, false, Some(prefix))
else
dafnyDocstring[..1] + ConvertDocstring(dafnyDocstring[1..], ind, false, codeMarker)
else if && codeMarker.Some?
&& |codeMarker.value| <= |dafnyDocstring|
&& dafnyDocstring[..|codeMarker.value|] == codeMarker.value then
codeMarker.value + ConvertDocstring(dafnyDocstring[|codeMarker.value|..], ind, false, None)
else
dafnyDocstring[..1] + ConvertDocstring(dafnyDocstring[1..], ind, false, codeMarker)
else
dafnyDocstring[..1] + ConvertDocstring(dafnyDocstring[1..], ind, false, codeMarker)
}
function ToDocstringPrefix(docString: string, ind: string): string {
if docString == "" then "" else
"/// " + AddIndent(docString, ind + "/// ") + "\n" + ind
DocStringPrefix + ConvertDocstring(docString, ind) + "\n" + ind
}

datatype Mod =
Expand Down
Loading

0 comments on commit 175ee9f

Please sign in to comment.