Skip to content

Commit 00cae51

Browse files
MikaelMayerMikaelMayer
authored
Fix: Generated Rust docstring no longer crashes cargo doc (#6085)
Fixes #6084 ### What was changed? 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, code blocks with the `rs` are written without this label to ensure it's possible to write tested Rust docstring that can be executed with `cargo test --doc` * 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. ### How has this been tested? 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. <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>
1 parent 89e44cc commit 00cae51

File tree

8 files changed

+516
-12
lines changed

8 files changed

+516
-12
lines changed

Diff for: ‎Source/DafnyCore.Test/GeneratedFromDafny/RASTCoverage.cs

+131
Original file line numberDiff line numberDiff line change
@@ -20,14 +20,142 @@ public static void AssertCoverage(bool x)
2020
if (!(x)) {
2121
throw new Dafny.HaltException("Backends/Rust/Dafny-compiler-rust-coverage.dfy(26,4): " + Dafny.Sequence<Dafny.Rune>.UnicodeFromString("expectation violation").ToVerbatimString(false));}
2222
}
23+
public static void AssertEq<__T>(__T x, __T y)
24+
{
25+
if (!(object.Equals(x, y))) {
26+
throw new Dafny.HaltException("Backends/Rust/Dafny-compiler-rust-coverage.dfy(30,4): " + Dafny.Sequence<Dafny.Rune>.UnicodeFromString("expectation violation").ToVerbatimString(false));}
27+
}
2328
public static void TestExpr()
2429
{
2530
RASTCoverage.__default.TestOptimizeToString();
2631
RASTCoverage.__default.TestPrintingInfo();
2732
RASTCoverage.__default.TestNoExtraSemicolonAfter();
33+
RASTCoverage.__default.TestDocstring();
34+
}
35+
public static Dafny.ISequence<Dafny.Rune> CanonicalNewlines(Dafny.ISequence<Dafny.Rune> s) {
36+
Dafny.ISequence<Dafny.Rune> _0___accumulator = Dafny.Sequence<Dafny.Rune>.FromElements();
37+
TAIL_CALL_START: ;
38+
if ((new BigInteger((s).Count)).Sign == 0) {
39+
return Dafny.Sequence<Dafny.Rune>.Concat(_0___accumulator, Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""));
40+
} else if (((s).Select(BigInteger.Zero)) == (new Dafny.Rune('\r'))) {
41+
if (((new BigInteger((s).Count)) > (BigInteger.One)) && (((s).Select(BigInteger.One)) == (new Dafny.Rune('\n')))) {
42+
_0___accumulator = Dafny.Sequence<Dafny.Rune>.Concat(_0___accumulator, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("\n"));
43+
Dafny.ISequence<Dafny.Rune> _in0 = (s).Drop(new BigInteger(2));
44+
s = _in0;
45+
goto TAIL_CALL_START;
46+
} else {
47+
_0___accumulator = Dafny.Sequence<Dafny.Rune>.Concat(_0___accumulator, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("\n"));
48+
Dafny.ISequence<Dafny.Rune> _in1 = (s).Drop(BigInteger.One);
49+
s = _in1;
50+
goto TAIL_CALL_START;
51+
}
52+
} else {
53+
_0___accumulator = Dafny.Sequence<Dafny.Rune>.Concat(_0___accumulator, (s).Take(BigInteger.One));
54+
Dafny.ISequence<Dafny.Rune> _in2 = (s).Drop(BigInteger.One);
55+
s = _in2;
56+
goto TAIL_CALL_START;
57+
}
58+
}
59+
public static void TestOneDocstring(Dafny.ISequence<Dafny.Rune> dafnyDocstring, Dafny.ISequence<Dafny.Rune> rustDocstring, Dafny.ISequence<Dafny.Rune> indent)
60+
{
61+
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));
62+
}
63+
public static void TestDocstring()
64+
{
65+
RASTCoverage.__default.TestOneDocstring(Dafny.Sequence<Dafny.Rune>.UnicodeFromString(@"
66+
Hello
67+
World"), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(@"
68+
/// Hello
69+
/// World"), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(" "));
70+
RASTCoverage.__default.TestOneDocstring(Dafny.Sequence<Dafny.Rune>.UnicodeFromString(@"
71+
Title
72+
```rs
73+
let mut x = 1;
74+
```
75+
End comment"), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(@"
76+
/// Title
77+
/// ```
78+
/// let mut x = 1;
79+
/// ```
80+
/// End comment"), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(" "));
81+
RASTCoverage.__default.TestOneDocstring(Dafny.Sequence<Dafny.Rune>.UnicodeFromString(@"
82+
Title
83+
`````rs
84+
let mut x = 1;
85+
`````
86+
End comment"), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(@"
87+
/// Title
88+
/// `````
89+
/// let mut x = 1;
90+
/// `````
91+
/// End comment"), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(" "));
92+
RASTCoverage.__default.TestOneDocstring(Dafny.Sequence<Dafny.Rune>.UnicodeFromString(@"
93+
Title
94+
```
95+
var x := 1;
96+
```
97+
End comment"), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(@"
98+
/// Title
99+
/// ```dafny
100+
/// var x := 1;
101+
/// ```
102+
/// End comment"), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(" "));
103+
RASTCoverage.__default.TestOneDocstring(Dafny.Sequence<Dafny.Rune>.UnicodeFromString(@"
104+
Title
105+
`````
106+
var x := 1;
107+
`````
108+
End comment"), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(@"
109+
/// Title
110+
/// `````dafny
111+
/// var x := 1;
112+
/// `````
113+
/// End comment"), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(" "));
114+
RASTCoverage.__default.TestOneDocstring(Dafny.Sequence<Dafny.Rune>.UnicodeFromString(@"
115+
Title
116+
`````md
117+
# title
118+
```
119+
code
120+
```
121+
Outside of code
122+
`````
123+
```
124+
dafnycode
125+
```
126+
End comment"), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(@"
127+
/// Title
128+
/// `````md
129+
/// # title
130+
/// ```
131+
/// code
132+
/// ```
133+
/// Outside of code
134+
/// `````
135+
/// ```dafny
136+
/// dafnycode
137+
/// ```
138+
/// End comment"), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(" "));
139+
RASTCoverage.__default.TestOneDocstring(Dafny.Sequence<Dafny.Rune>.UnicodeFromString(@"
140+
Title
141+
Indented code
142+
More indented code
143+
Back to normal
144+
Normal as well
145+
Also normal
146+
But this one indented"), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(@"
147+
/// Title
148+
/// | Indented code
149+
/// | More indented code
150+
/// Back to normal
151+
/// Normal as well
152+
/// Also normal
153+
/// | But this one indented"), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(" "));
28154
}
29155
public static void TestNoOptimize(RAST._IExpr e)
30156
{
157+
if (!(object.Equals((RASTCoverage.__default.ExprSimp).ReplaceExpr(e), e))) {
158+
throw new Dafny.HaltException("Backends/Rust/Dafny-compiler-rust-coverage.dfy(157,4): " + Dafny.Sequence<Dafny.Rune>.UnicodeFromString("expectation violation").ToVerbatimString(false));}
31159
}
32160
public static RAST._IExpr ConversionNum(RAST._IType t, RAST._IExpr x)
33161
{
@@ -161,5 +289,8 @@ public static void TestNoExtraSemicolonAfter()
161289
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());
162290
RASTCoverage.__default.AssertCoverage(!((RAST.Expr.create_Identifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("x"))).NoExtraSemicolonAfter()));
163291
}
292+
public static RAST._IRASTBottomUpReplacer ExprSimp { get {
293+
return ExpressionOptimization.__default.ExprSimplifier();
294+
} }
164295
}
165296
} // end of namespace RASTCoverage

Diff for: ‎Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-coverage.dfy

+121-1
Original file line numberDiff line numberDiff line change
@@ -25,16 +25,136 @@ module RASTCoverage {
2525
{
2626
expect x;
2727
}
28+
method AssertEq<T(==)>(x: T, y: T)
29+
{
30+
expect x == y;
31+
}
32+
2833

2934
method TestExpr() {
3035
TestOptimizeToString();
3136
TestPrintingInfo();
3237
TestNoExtraSemicolonAfter();
38+
TestDocstring();
39+
}
40+
41+
function CanonicalNewlines(s: string): string {
42+
if |s| == 0 then "" else
43+
if s[0] == '\r' then
44+
if |s| > 1 && s[1] == '\n' then
45+
"\n" + CanonicalNewlines(s[2..])
46+
else
47+
"\n" + CanonicalNewlines(s[1..])
48+
else
49+
s[..1] + CanonicalNewlines(s[1..])
3350
}
3451

52+
method TestOneDocstring(dafnyDocstring: string, rustDocstring: string, indent: string := " ") {
53+
AssertEq(
54+
ConvertDocstring(
55+
CanonicalNewlines(dafnyDocstring),
56+
indent
57+
), CanonicalNewlines(rustDocstring));
58+
}
59+
60+
method TestDocstring() {
61+
TestOneDocstring(@"
62+
Hello
63+
World",
64+
@"
65+
/// Hello
66+
/// World");
67+
TestOneDocstring(@"
68+
Title
69+
```rs
70+
let mut x = 1;
71+
```
72+
End comment", @"
73+
/// Title
74+
/// ```
75+
/// let mut x = 1;
76+
/// ```
77+
/// End comment");
78+
TestOneDocstring(@"
79+
Title
80+
`````rs
81+
let mut x = 1;
82+
`````
83+
End comment", @"
84+
/// Title
85+
/// `````
86+
/// let mut x = 1;
87+
/// `````
88+
/// End comment");
89+
TestOneDocstring(@"
90+
Title
91+
```
92+
var x := 1;
93+
```
94+
End comment", @"
95+
/// Title
96+
/// ```dafny
97+
/// var x := 1;
98+
/// ```
99+
/// End comment");
100+
TestOneDocstring(@"
101+
Title
102+
`````
103+
var x := 1;
104+
`````
105+
End comment", @"
106+
/// Title
107+
/// `````dafny
108+
/// var x := 1;
109+
/// `````
110+
/// End comment");
111+
TestOneDocstring(@"
112+
Title
113+
`````md
114+
# title
115+
```
116+
code
117+
```
118+
Outside of code
119+
`````
120+
```
121+
dafnycode
122+
```
123+
End comment", @"
124+
/// Title
125+
/// `````md
126+
/// # title
127+
/// ```
128+
/// code
129+
/// ```
130+
/// Outside of code
131+
/// `````
132+
/// ```dafny
133+
/// dafnycode
134+
/// ```
135+
/// End comment");
136+
TestOneDocstring(@"
137+
Title
138+
Indented code
139+
More indented code
140+
Back to normal
141+
Normal as well
142+
Also normal
143+
But this one indented", @"
144+
/// Title
145+
/// | Indented code
146+
/// | More indented code
147+
/// Back to normal
148+
/// Normal as well
149+
/// Also normal
150+
/// | But this one indented");
151+
}
152+
153+
const ExprSimp := ExpressionOptimization.ExprSimplifier()
154+
35155
method TestNoOptimize(e: Expr)
36-
//requires e.Optimize() == e // Too expensive
37156
{
157+
expect ExprSimp.ReplaceExpr(e) == e;
38158
}
39159

40160
function ConversionNum(t: Type, x: Expr): Expr {

Diff for: ‎Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-proofs.dfy

+22-1
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,29 @@
11
include "../Dafny/AST.dfy"
22

3-
/*This module does not contain any compiled code because it
3+
/*These modules do not contain any compiled code because they
44
only proves properties about DCOMP. In a sense, it's a test file. */
55
@Compile(false)
6+
module {:extern "RASTProofs"} RASTProofs {
7+
import opened RAST
8+
lemma AboutGatherSimpleQuotes(docstring: string, acc: string)
9+
ensures
10+
var r := GatherSimpleQuotes(docstring, acc);
11+
&& |acc| <= |r|
12+
&& |r[|acc|..]| <= |docstring|
13+
&& r == acc + docstring[..|r[|acc|..]|]
14+
&& (forall i | |acc| <= i < |r| :: r[i] == '`')
15+
&& (|docstring| > |r[|acc|..]| ==>
16+
docstring[|r[|acc|..]|] != '`')
17+
{
18+
var r := GatherSimpleQuotes(docstring, acc);
19+
if |docstring| == 0 || docstring[0] != '`' {
20+
21+
} else {
22+
23+
}
24+
}
25+
}
26+
@Compile(false)
627
module {:extern "DafnyToRustCompilerProofs"} DafnyToRustCompilerProofs {
728
import opened DafnyToRustCompiler
829
import opened DafnyToRustCompilerDefinitions

Diff for: ‎Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-rast.dfy

+55-1
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,8 @@ module RAST
1515
// Default Rust-like indentation
1616
const IND := " "
1717

18+
const DocStringPrefix: string := "/// "
19+
1820
datatype RASTTopDownVisitor<!T(!new)> =
1921
RASTTopDownVisitor(
2022
nameonly VisitTypeSingle: (T, Type) -> T,
@@ -351,9 +353,61 @@ module RAST
351353
else FoldLeft(f, f(init, xs[0]), xs[1..])
352354
}
353355

356+
function GatherSimpleQuotes(docstring: string, acc: string := ""): (r: string)
357+
ensures |r| <= |acc| + |docstring|
358+
{
359+
if |docstring| == 0 || docstring[0] != '`' then acc else
360+
GatherSimpleQuotes(docstring[1..], acc + "`")
361+
}
362+
363+
// Converts Dafny docstring into Rust docstring that won't normally cause issue with `cargo doc`
364+
// - Escape blocks ```...``` to ```dafny ...``` but keep ```rs...``` intact
365+
// - Every line starting with 4 or more spaces gets its first space replaced by a `|`
366+
function ConvertDocstring(dafnyDocstring: string, ind: string, newlineStarted: bool := true, codeMarker: Option<string> := None): string {
367+
if |dafnyDocstring| == 0 then dafnyDocstring
368+
else if dafnyDocstring[0] == '\n' then
369+
"\n" + ind + DocStringPrefix + ConvertDocstring(dafnyDocstring[1..], ind, true, codeMarker)
370+
else if dafnyDocstring[0] == ' ' then
371+
if codeMarker.None? && newlineStarted && |dafnyDocstring| > 4 && dafnyDocstring[..4] == " " then
372+
"| " + ConvertDocstring(dafnyDocstring[4..], ind, false, codeMarker)
373+
else
374+
" " + ConvertDocstring(dafnyDocstring[1..], ind, newlineStarted, codeMarker)
375+
else if newlineStarted then
376+
if && codeMarker.Some?
377+
&& |dafnyDocstring| >= |codeMarker.value| + 1
378+
&& dafnyDocstring[..|codeMarker.value| + 1] == codeMarker.value + "\n" then
379+
// End of code delimiter
380+
codeMarker.value + ConvertDocstring(dafnyDocstring[|codeMarker.value|..], ind, false, None)
381+
else if codeMarker.None? && |dafnyDocstring| >= 3 then
382+
var prefix := dafnyDocstring[..3];
383+
if prefix == "```" then
384+
var prefix := GatherSimpleQuotes(dafnyDocstring);
385+
var remaining := dafnyDocstring[|prefix|..];
386+
if |remaining| == 0 || remaining[0] == ' ' || remaining[0] == '\n' then
387+
// ``` becomes ```dafny
388+
// It's Dafny docstring, we want to ensure we add the Dafny identifier there
389+
prefix + "dafny" + ConvertDocstring(dafnyDocstring[|prefix|..], ind, false, Some(prefix))
390+
else if && |remaining| >= 3
391+
&& remaining[..2] == "rs"
392+
&& (remaining[2] == ' ' || remaining[2] == '\n') then
393+
// ```rs becomes ```
394+
prefix + ConvertDocstring(dafnyDocstring[|prefix|+2..], ind, false, Some(prefix))
395+
else
396+
prefix + ConvertDocstring(dafnyDocstring[|prefix|..], ind, false, Some(prefix))
397+
else
398+
dafnyDocstring[..1] + ConvertDocstring(dafnyDocstring[1..], ind, false, codeMarker)
399+
else if && codeMarker.Some?
400+
&& |codeMarker.value| <= |dafnyDocstring|
401+
&& dafnyDocstring[..|codeMarker.value|] == codeMarker.value then
402+
codeMarker.value + ConvertDocstring(dafnyDocstring[|codeMarker.value|..], ind, false, None)
403+
else
404+
dafnyDocstring[..1] + ConvertDocstring(dafnyDocstring[1..], ind, false, codeMarker)
405+
else
406+
dafnyDocstring[..1] + ConvertDocstring(dafnyDocstring[1..], ind, false, codeMarker)
407+
}
354408
function ToDocstringPrefix(docString: string, ind: string): string {
355409
if docString == "" then "" else
356-
"/// " + AddIndent(docString, ind + "/// ") + "\n" + ind
410+
DocStringPrefix + ConvertDocstring(docString, ind) + "\n" + ind
357411
}
358412

359413
datatype Mod =

0 commit comments

Comments
 (0)