~james/remy

fix(frontend): distinguish syntax failures from resource limits

commit
33c6eac26df0f52eff4cf919f587a3b60628ab12 browse tree
parent
9a908c16a977ca9df2dada000c4243ea210d427b
author
james <j@cpl0.zip>
signature
Verified ~james signed with a key registered by ~james
date
2026-09-30 11:00 UTC

3 files changed, +19 −3

src/Examples.thy modified

@@ -121,4 +121,8 @@ lemma trailing_token_offset:
121121 "source_error ''(+ x y) 1'' = ''syntax error at token 5'' @ newline"
122122 by eval
123123
124+lemma exhausted_parser:
125+ "diagnose 0 [] [''1''] 7 = Failed (Exhausted 7)"
126+ by (subst diagnose.simps) simp
127+
124128 end

src/Frontend.thy modified

@@ -196,11 +196,14 @@ termination by (relation "measure (\<lambda>(fuel,names,tokens,pos). fuel)") aut
196196 declare diagnose.simps [simp del]
197197
198198 definition source_error :: "string \<Rightarrow> string" where
199- "source_error s = (case diagnose 128 [] (lex s [] []) 0 of
199+ "source_error s = (if \<not> list_all (\<lambda>c. nat_of_char c < 128) s then ''source must contain ASCII'' @ newline else
200+ case diagnose 128 [] (lex s [] []) 0 of
200201 Failed (Unexpected pos) \<Rightarrow> ''syntax error at token '' @ decimal pos @ newline
201- | Failed (Exhausted pos) \<Rightarrow> ''invalid source or resource limit'' @ newline
202+ | Failed (Exhausted pos) \<Rightarrow> ''parse depth limit exceeded at token '' @ decimal pos @ newline
202203 | Parsed (e,rest,pos) \<Rightarrow> if rest \<noteq> [] then ''syntax error at token '' @ decimal pos @ newline
203- else ''invalid source or resource limit'' @ newline)"
204+ else if nodes e > 4096 then ''program exceeds 4096 nodes'' @ newline
205+ else if demand (optimise e) > 512 then ''evaluation stack exceeds 512 words'' @ newline
206+ else ''native validation failed'' @ newline)"
204207
205208 definition artifact :: "string \<Rightarrow> (bool \<times> string) \<times> string" where
206209 "artifact s = (case prepare s of None \<Rightarrow> ((False,[]), source_error s)

tests/cli.py modified

@@ -32,6 +32,15 @@ def main():
3232 for text, position in [('(+ x)',3),('(div x y)',1),('(let a 3 b)',4),('(+ x y',4),('(+ x y) 1',5)]:
3333 source.write_text(text)
3434 assert f'token {position}\n' in invoke(source,binary,ok=False), text
35+ source.write_text('(+ 1 ' * 129 + '0' + ')' * 129)
36+ assert 'parse depth limit' in invoke(source,binary,ok=False)
37+ large = '0'
38+ for _ in range(12):
39+ large = f'(+ {large} {large})'
40+ source.write_text(large)
41+ assert '4096 nodes' in invoke(source,binary,ok=False)
42+ source.write_text('é')
43+ assert 'ASCII' in invoke(source,binary,ok=False)
3544 for text in ['0x','0x10000000000000000','0xfg','0xffextra','-0x1']:
3645 source.write_text(text)
3746 binary.write_bytes(b'preserve')