Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
module gunbc.recurring_failure_mode.lexer_literal_lexeme_straddles_its_sequence_partner

import std.types { NonEmptyStr }
import std.decl_ref { DeclarationRef, WholeDeclaration }
import gunbc.recurring_failure_mode { RecurringFailureMode }

data lexer_literal_lexeme_straddles_its_sequence_partner: RecurringFailureMode = RecurringFailureMode {
identity: "lexer_literal_lexeme_straddles_its_sequence_partner" as NonEmptyStr,

receipts: [
"**every token after a line comment carried a ByteRange past its true offset, on pure-ASCII sources, because the comment's lexeme was fabricated text** (INVALID STATE: the `.dag` line comment `// ab` lexed to the lexeme `//[32, 97, 98]`, and a bare `//` lexed to `//Empty`. `v2.compiler.tokenize` `lex_walk_step` advances `pos` by the lexeme's length, so every later token start and end was shifted by the difference: +39 after a 13-character comment, and past the end of the file in `extdeps.bazel.build_event_stream`. The captured annotation text was the rendering too.) Every locus consumer after a comment read the wrong bytes: refusal carets, the XL-2 reference-conservation census, and XL-5's exact loci.",
"MECHANISM, re-derived (DESIGN section 6b). `lex_match_prefix` answered the pattern LITERAL as its lexeme, while every other matcher answers the codepoints it consumed from the source. On the seed those are different carriers: a native String, and a codepoint `Value::List`. The sequence arm of `lex_rule_thunk` joins its two lexemes with `list_append`, which is `concat`. The line-comment rule is `Sequence(Literal \"//\", Repeat(LineCommentTextChar))`, so that join met a native String receiver and a codepoint list. The seed's `concat` on a String renders any other argument: that is its modelled behaviour (`(a, b) -> String`), and programs rely on it for Int, as in `dag/gunbc/instruments/generated_artifact_gate.dag`. The list therefore rendered as its display text. The seed cannot tell a codepoint list from a data `List<Int>` at the Value level; that is the named open thread of `v1_compiler.v1_interpreter` `string_realization_straddle_detail`. So the earliest link that could be justified away is the one that CREATED the straddle, the literal matcher, not the concat that met it. A first attempt refused non-string arguments in the seed's concat. It was withdrawn after it broke that legitimate Int stringification in the required floor on gunbc#12313.",
"REPAIR. `lex_match_prefix` consumes its prefix from the source (`lex_consume_prefix`), so every lexeme the lexer builds is one carrier and a sequence's join is a list append. The lexeme's value is unchanged. `lex_strip_prefix`, now unused, is deleted. DISTINGUISHING FACTS: not gunbc#12285, where the lexer counts scalars into a field named bytes. That shifts extents by the octet excess of non-ASCII scalars. This row's shift is in the length of the wrong TEXT and occurs on ASCII; the two compose. Why no claim saw it: `v2.test.tokenize.annotation_channel` checks annotation counts and token identities, never offsets or annotation text.",
"RUNG after the repair: mechanically preventable. The claims below execute the production rule set and red on the old matcher; nothing in the lexer's types stops a future matcher from answering a pattern literal again. CEILING: structurally impossible, once a String and a codepoint sequence are one carrier in the realization, so that no join of two lexemes can straddle. NEXT-RUNG TRIGGER, NAMING THE CAPABILITY: the Char/String realization grounding named by `string_realization_straddle_detail`'s open thread.",
],

evidence: [
DeclarationRef { module_path: "v2.test.tokenize.line_comment_extent", decl_name: "a_token_after_a_line_comment_starts_at_its_offset", field: WholeDeclaration },
DeclarationRef { module_path: "v2.test.tokenize.line_comment_extent", decl_name: "a_token_after_a_bare_line_comment_starts_at_its_offset", field: WholeDeclaration },
DeclarationRef { module_path: "v2.test.tokenize.line_comment_extent", decl_name: "a_line_comment_captures_its_own_text_and_extent", field: WholeDeclaration },
DeclarationRef { module_path: "v2.test.tokenize.line_comment_extent", decl_name: "tokens_without_a_comment_start_at_their_offsets", field: WholeDeclaration },
],
}
33 changes: 24 additions & 9 deletions src/v2/compiler/01_tokenize.dag
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ import v2.std.optional { Absent, Present }
import v2.std.diagnostic { Accepted, ByteRange, Diagnostic, ExternalContractUnknown, Locus, None, Outcome, Rejected, Textual, Unavailable, UserInputBoundary, WholeFile, diagnostics_singleton }
import v2.std.node { Symbol }
import std.algebra { Cons, Empty, list_append, list_snoc_item }
import v2.std.algebra { ListTailResult, TailAbsent, TailFound, fold_list, is_empty, is_prefix_of, length, list_tail }
import v2.std.algebra { TailAbsent, TailFound, fold_list, is_empty, is_prefix_of, length }
import v2.std.text { Char, CharAbsent, CharFound, SourceFold, String, fold_source, string_head, string_is_empty, string_tail }
import v2.std.logic { Bool }
import std.unicode.types { unicode_char_code_point, unicode_scalar_utf8_octet_count }
Expand Down Expand Up @@ -99,25 +99,40 @@ fn char_in_class(c: Char, class: LexCharClass) -> Bool {
}
}

fn lex_strip_prefix(prefix: v2.std.text.String, source: v2.std.text.String) -> ListTailResult<Char> {
// THE LEXEME IS THE SOURCE'S OWN TEXT, NOT THE PATTERN'S. Every other matcher answers the codepoints
// it consumed from `source`; this one answered the pattern literal `prefix`. The two agree as
// values, but on the seed they are different carriers -- a pattern literal is a native String, the
// source is a codepoint list -- and the sequence arm of lex_rule_thunk joins its two lexemes with
// list_append. The line-comment rule is Sequence(Literal "//", Repeat(..)), so that join met a native
// String and a codepoint list, and the seed's concat rendered the list: `// ab` became the text
// `//[32, 97, 98]` and a bare `//` became `//Empty`. lex_walk_step advances every extent by the
// lexeme's length, so every token after any line comment was mislocated (gunbc.recurring_failure_mode
// lexer_literal_lexeme_straddles_its_sequence_partner). Consuming the prefix from the source makes
// every lexeme one carrier; the value is unchanged.
fn lex_consume_prefix(prefix: v2.std.text.String, source: v2.std.text.String) -> LexMatchResult {
fold_list(
xs: prefix,
empty: TailFound { tail: source },
empty: LexMatchAccepted { remaining: source, lexeme: std.algebra.Empty },
cons: fn(acc, _) {
match acc {
TailAbsent => TailAbsent
TailFound { tail: r } => list_tail(xs: r)
LexMatchRejected => LexMatchRejected
LexMatchAccepted { remaining: r, lexeme: consumed } =>
match string_head(s: r) {
CharAbsent => LexMatchRejected
CharFound { value: c } =>
match string_tail(s: r) {
TailFound { tail: rest } => LexMatchAccepted { remaining: rest, lexeme: list_snoc_item(xs: consumed, item: c) }
TailAbsent => LexMatchRejected
}
}
}
}
)
}

fn lex_match_prefix(prefix: v2.std.text.String, source: v2.std.text.String) -> LexMatchResult {
if is_prefix_of(prefix: prefix, xs: source, eq: fn(a, b) { a == b }) {
match lex_strip_prefix(prefix: prefix, source: source) {
TailFound { tail: rem } => LexMatchAccepted { remaining: rem, lexeme: prefix }
TailAbsent => LexMatchRejected
}
lex_consume_prefix(prefix: prefix, source: source)
} else {
LexMatchRejected
}
Expand Down
65 changes: 65 additions & 0 deletions src/v2/test/claim/tokenize/line_comment_extent_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,65 @@
module v2.test.tokenize.line_comment_extent

import v2.std.text { String }
import v2.std.logic { Bool }
import v2.std.algebra { fold_list }
import v2.std.compilers.lexing { lex_artifact_annotations, lex_artifact_semantic_tokens, token_stream_all }
import v2.compiler.tokenize { lex_walk_artifact }
import v2.extdeps.languages.dag { dag_lex_rules }
import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }

data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly

// A LINE COMMENT ADVANCES THE LEXER BY ITS OWN LENGTH, AND ITS CAPTURED TEXT IS ITSELF.
//
// The `.dag` line-comment rule is Sequence(Literal "//", Repeat(LineCommentTextChar)), and the
// sequence arm of v2.compiler.tokenize lex_rule_thunk joins the two lexemes with list_append. The
// literal matcher answered the pattern's own text -- a native String on the seed -- beside the
// repeat's codepoint list, and the seed's concat renders a list it cannot tell from data: `// ab`
// became the text `//[32, 97, 98]` and a bare `//` became `//Empty`. lex_walk_step advances every
// extent by the lexeme's length, so every token after any line comment carried a ByteRange past its
// true offset. The route here is the production one: the `.dag` language's own rule set through
// lex_walk_artifact. Rostered as gunbc.recurring_failure_mode
// lexer_literal_lexeme_straddles_its_sequence_partner.
//
// The sources are ASCII so byte and scalar offsets agree; the unit question is gunbc#12285's.
fn token_starts(source: String) -> String {
match lex_walk_artifact(source: chars(s: source), file: ^probe, rules: dag_lex_rules()) {
v2.std.diagnostic.Accepted { value: a, diagnostics: _ } =>
fold_list(
xs: token_stream_all(stream: lex_artifact_semantic_tokens(artifact: a)),
empty: "",
cons: fn(acc, t) { concat(acc, concat("|", concat(t.lexeme, concat("@", to_string(t.start))))) }
)
v2.std.diagnostic.Rejected { diagnostics: _ } => "REFUSED"
}
}

fn annotation_texts(source: String) -> String {
match lex_walk_artifact(source: chars(s: source), file: ^probe, rules: dag_lex_rules()) {
v2.std.diagnostic.Accepted { value: a, diagnostics: _ } =>
fold_list(
xs: lex_artifact_annotations(artifact: a),
empty: "",
cons: fn(acc, n) { concat(acc, concat("|", concat(n.lexeme, concat("@", concat(to_string(n.start), concat("-", to_string(n.end))))))) }
)
v2.std.diagnostic.Rejected { diagnostics: _ } => "REFUSED"
}
}

// The control: no comment, so no join, and the extents were always right.
test fn tokens_without_a_comment_start_at_their_offsets() -> Bool {
token_starts(source: "a\n\nb\n") == "|a@0|b@3"
}

test fn a_token_after_a_line_comment_starts_at_its_offset() -> Bool {
token_starts(source: "a\n// ab\nb\n") == "|a@0|b@8"
}

test fn a_token_after_a_bare_line_comment_starts_at_its_offset() -> Bool {
token_starts(source: "a\n//\nb\n") == "|a@0|b@5"
}

test fn a_line_comment_captures_its_own_text_and_extent() -> Bool {
annotation_texts(source: "a\n// ab\nb\n") == "|// ab@2-7"
}