Skip to content

fix(parser): Parse more than utf8#1072

Open
sishtiaq wants to merge 2 commits into
mainfrom
sishtiaq/954_parse_more_than_UTF8
Open

fix(parser): Parse more than utf8#1072
sishtiaq wants to merge 2 commits into
mainfrom
sishtiaq/954_parse_more_than_UTF8

Conversation

@sishtiaq

@sishtiaq sishtiaq commented Jul 13, 2026

Copy link
Copy Markdown
Collaborator

fix(parse): Extend parser to parse more than UTF-8 (#954).

sqlite3.c has a char table that needs to be parsed. This PR allows non-UTF-8 to be parsed too. The three chars {\n,\t,"} are still printed as human-readable, even if their corresponding hex codes are parsed.

The main change is that Parser.parseStringLiteral now returns a ByteArray, rather than a String. Some of the previous uses (AttrParser, MlirParser) converted to Byte anyway; these calculations have now gone.
On the other hand, UnitTest/Parser has a wrapper to convert to String for comparison.

TODO:

  • rm currently-commented-out escapeStringLiteral. (Replaced by escapeStringLiteralStr.)

\{\t,\n,"\} and their corresponding hex codes \{\09,\0A,\22\} are both printed as human-readable \{\t,\n,"\}.

ToDo:
escapeStringLiteral is not used anymore. rm it.
@sishtiaq sishtiaq force-pushed the sishtiaq/954_parse_more_than_UTF8 branch from d079d69 to bc31ba6 Compare July 13, 2026 14:39
@sishtiaq sishtiaq requested a review from GZGavinZhao July 13, 2026 14:40
@sishtiaq sishtiaq self-assigned this Jul 13, 2026
@sishtiaq sishtiaq requested a review from math-fehr July 13, 2026 14:42
@sishtiaq sishtiaq marked this pull request as ready for review July 13, 2026 14:44

@github-actions github-actions Bot left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

VeIR Benchmarks

Details
Benchmark suite Current: bc31ba6 Previous: f7ca4b1 Ratio
add-fold-worklist/create 2421500 ns (± 134555) 2270000 ns (± 109893) 1.07
add-fold-worklist/rewrite 3926000 ns (± 76158) 3959000 ns (± 79694) 0.99
add-fold-worklist-local/create 2304000 ns (± 69327) 2335000 ns (± 109468) 0.99
add-fold-worklist-local/rewrite 3626000 ns (± 35147) 3615000 ns (± 35784) 1.00
add-zero-worklist/create 2368000 ns (± 117713) 2322000 ns (± 115582) 1.02
add-zero-worklist/rewrite 2557000 ns (± 93871) 2504500 ns (± 66314) 1.02
add-zero-reuse-worklist/create 2109500 ns (± 143530) 1937500 ns (± 149410) 1.09
add-zero-reuse-worklist/rewrite 2117500 ns (± 105821) 2097000 ns (± 86689) 1.01
mul-two-worklist/create 2408000 ns (± 121148) 2286500 ns (± 188840) 1.05
mul-two-worklist/rewrite 5579000 ns (± 226646) 5517000 ns (± 174801) 1.01
add-fold-forwards/create 2481000 ns (± 121842) 2189000 ns (± 65580) 1.13
add-fold-forwards/rewrite 2976000 ns (± 46896) 2932000 ns (± 32708) 1.02
add-zero-forwards/create 2429000 ns (± 92534) 2326500 ns (± 269790) 1.04
add-zero-forwards/rewrite 1877000 ns (± 39518) 1894500 ns (± 47715) 0.99
add-zero-reuse-forwards/create 2064000 ns (± 76038) 1935500 ns (± 164132) 1.07
add-zero-reuse-forwards/rewrite 1481000 ns (± 38403) 1510000 ns (± 42610) 0.98
mul-two-forwards/create 2293000 ns (± 65458) 2244000 ns (± 80837) 1.02
mul-two-forwards/rewrite 3668000 ns (± 67229) 3622000 ns (± 38591) 1.01
add-zero-reuse-first/create 2076000 ns (± 119293) 2046500 ns (± 201731) 1.01
add-zero-reuse-first/rewrite 8000 ns (± 1617) 9000 ns (± 1893) 0.89
add-zero-lots-of-reuse-first/create 2054000 ns (± 102414) 1975500 ns (± 208057) 1.04
add-zero-lots-of-reuse-first/rewrite 767500 ns (± 25500) 775000 ns (± 26787) 0.99

This comment was automatically generated by workflow using github-action-benchmark.

Comment thread Veir/IR/Attribute.lean
toString attr := s!"{attr.value} : !riscv.reg"

def escapeStringLiteral (s : String) : String := Id.run do
-- def escapeStringLiteral (s : String) : String := Id.run do

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Stray code?

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nevermind, didn't read the PR description.

@math-fehr math-fehr left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks a lot! I added a few comments, but otherwise all good.

Comment thread UnitTest/Parser.lean
-/
#guard_msgs in
#eval testParser "\"\\t\\n\\\"hello world\\09\\0A\\22\"" parseOptionalStringLiteralStr

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I guess you should add a test here where we return none from parseOptionalStringLiteralStr?

Comment thread Veir/IR/Attribute.lean
Comment on lines +757 to +765
-- def escapeStringLiteral (s : String) : String := Id.run do
-- let mut result := ""
-- for c in s.toList do
-- if c == '\\' then result := result ++ "\\\\"
-- else if c == '"' then result := result ++ "\\\""
-- else if c == '\n' then result := result ++ "\\n"
-- else if c == '\t' then result := result ++ "\\t"
-- else result := result.push c
-- return result

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
-- def escapeStringLiteral (s : String) : String := Id.run do
-- let mut result := ""
-- for c in s.toList do
-- if c == '\\' then result := result ++ "\\\\"
-- else if c == '"' then result := result ++ "\\\""
-- else if c == '\n' then result := result ++ "\\n"
-- else if c == '\t' then result := result ++ "\\t"
-- else result := result.push c
-- return result

Comment thread Veir/IR/Attribute.lean
if n < 10 then Char.ofNat (n.toNat + '0'.toNat)
else Char.ofNat (n.toNat - 10 + 'A'.toNat)

def escapeStringLiteralBytes (b : ByteArray) : String := Id.run do

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
def escapeStringLiteralBytes (b : ByteArray) : String := Id.run do
def escapeStringLiteral (b : ByteArray) : String := Id.run do

I think Bytes is not needed since we have it as argument already?

let results ← parseOpResults
let opNameStart ← getPos
let some opName ← parseOptionalStringLiteral | return none
let opNameStr := String.fromUTF8! opName

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Here this will fail if we give non-utf8 operation name.
This was before failing with an "internal error" message.
Can you use fromUTF8? here and fail with an error message as well?

Comment thread Veir/Parser/Parser.lean
Comment on lines 301 to 302
Parse a string literal.
Raise an error if the next token is not a string literal.

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You should also update this documentation AFAIK

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants