Skip to content

Commit 2292e09

Browse files
committed
fix(proof): escape backslashes in stub text instead of padding them (#952)
CI caught what my local run did not: appending a space after a trailing backslash produced '\ ' inside a non-raw docstring — an invalid escape sequence, which this repo's pytest config escalates from SyntaxWarning to an error. My fix for an escaping bug introduced a different escaping bug. Padding a dangerous character is not escaping it. _inline now escapes every backslash ('\\' renders identically when the docstring is read), which also covers Windows paths and regexes anywhere in the text, not just at the delimiter boundary. The trailing-quote case keeps its separating space, which is safe. The tests were too weak to catch it: ast.parse succeeds on source that merely warns. They now assert under warnings.simplefilter('error') and cover 'C:\\path', 're: \\d+' and '\\n' as well as the boundary tails. Also records the lesson, including: run the CI invocation locally, not a single-file subset — warning behaviour differs.
1 parent fb64b38 commit 2292e09

2 files changed

Lines changed: 31 additions & 14 deletions

File tree

codeframe/core/proof/stubs.py

Lines changed: 15 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -187,17 +187,22 @@ def _inline(text: str) -> str:
187187
whitespace runs to single spaces and neutralize the sequence that can close
188188
a docstring from inside one.
189189
190-
The trailing character matters separately. Six templates butt the text
191-
straight against their own closing delimiter — ``\"\"\"Proves: {description}\"\"\"``
192-
— so text ending in a single quote yields four in a row: Python closes the
193-
docstring on the first three and the fourth opens an unterminated literal.
194-
A trailing backslash escapes the delimiter's first quote for the same
195-
result. Neither is a ``\"\"\"`` run, so the replacement above does not see
196-
them (CI review on #952). One space is enough to separate them, and reads
197-
identically.
190+
Backslashes are escaped rather than left alone. Inside a non-raw docstring
191+
every ``\\x`` is an escape sequence, so a Windows path or a regex in the
192+
text emits ``SyntaxWarning: invalid escape sequence`` — an error under this
193+
repo's pytest config — and a *trailing* backslash escapes the template's
194+
own closing delimiter outright. Doubling renders identically when the
195+
docstring is read.
196+
197+
The trailing quote matters separately. Six templates butt the text straight
198+
against their closing delimiter — ``\"\"\"Proves: {description}\"\"\"`` — so text
199+
ending in one quote yields four in a row: Python closes the docstring on
200+
the first three and the fourth opens an unterminated literal. That is not a
201+
``\"\"\"`` run, so the replacement above does not see it. One space separates
202+
them and reads the same.
198203
"""
199-
collapsed = " ".join(str(text).split()).replace('"""', "'''")
200-
return collapsed + " " if collapsed.endswith(('"', "\\")) else collapsed
204+
collapsed = " ".join(str(text).split()).replace("\\", "\\\\").replace('"""', "'''")
205+
return collapsed + " " if collapsed.endswith('"') else collapsed
201206

202207

203208
def _js_string(text: str) -> str:

tests/core/test_proof9_evidence_integrity_952.py

Lines changed: 16 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -502,24 +502,36 @@ class TestTextEndingAtTheDocstringBoundary:
502502

503503
_PY_GATES = [Gate.UNIT, Gate.CONTRACT, Gate.VISUAL, Gate.A11Y, Gate.PERF, Gate.SEC]
504504

505-
@pytest.mark.parametrize("tail", ['"', '""', "\\", '\\"'])
505+
@pytest.mark.parametrize(
506+
"tail", ['"', '""', "\\", '\\"', "C:\\path", "re: \\d+", "\\n"]
507+
)
506508
@pytest.mark.parametrize("gate", _PY_GATES)
507509
def test_a_description_ending_at_the_delimiter_still_parses(self, gate, tail):
510+
"""Also asserts no SyntaxWarning: a stray backslash makes an invalid
511+
escape sequence inside a non-raw docstring, which this repo's pytest
512+
config escalates to an error — so a stub that merely *parses* is not
513+
enough."""
508514
import ast
515+
import warnings
509516

510517
from codeframe.core.proof.stubs import generate_stubs
511518

512519
req = _requirement("REQ-952-08", "t", f"ends with {tail}", [gate])
513-
ast.parse(generate_stubs(req)[gate])
520+
with warnings.catch_warnings():
521+
warnings.simplefilter("error")
522+
ast.parse(generate_stubs(req)[gate])
514523

515-
@pytest.mark.parametrize("tail", ['"', '""', "\\"])
524+
@pytest.mark.parametrize("tail", ['"', '""', "\\", "C:\\path"])
516525
def test_a_title_ending_at_a_delimiter_still_parses(self, tail):
517526
import ast
527+
import warnings
518528

519529
from codeframe.core.proof.stubs import generate_stubs
520530

521531
req = _requirement("REQ-952-09", f"ends with {tail}", "d", [Gate.UNIT])
522-
ast.parse(generate_stubs(req)[Gate.UNIT])
532+
with warnings.catch_warnings():
533+
warnings.simplefilter("error")
534+
ast.parse(generate_stubs(req)[Gate.UNIT])
523535

524536
def test_the_description_is_still_present_and_readable(self):
525537
from codeframe.core.proof.stubs import generate_stubs

0 commit comments

Comments
 (0)