feat(frontend): parse bounded hexadecimal word literals
4 files changed, +61 −3
- Makefile modified +1 −0
- src/Examples.thy modified +9 −0
- src/Frontend.thy modified +17 −3
- tests/cli.py added +34 −0
Makefile modified
| @@ -13,6 +13,7 @@ all: .build/ready | ||
| 13 | 13 | |
| 14 | 14 | check: all |
| 15 | 15 | python3 tests/native.py |
| 16 | + python3 tests/cli.py | |
| 16 | 17 | |
| 17 | 18 | payload: all |
| 18 | 19 | @mkdir -p .build/payload |
src/Examples.thy modified
| @@ -90,6 +90,15 @@ lemma trailing_rejected: "prepare ''(+ x y) 1'' = None" | ||
| 90 | 90 | lemma literal_overflow_rejected: "prepare ''18446744073709551616'' = None" |
| 91 | 91 | by eval |
| 92 | 92 | |
| 93 | +lemma hexadecimal_boundaries: | |
| 94 | + "number ''0xffffffffffffffff'' = Some (2 ^ 64 - 1) \<and> | |
| 95 | + number ''0x10000000000000000'' = None" | |
| 96 | + by eval | |
| 97 | + | |
| 98 | +lemma hexadecimal_execution: | |
| 99 | + "reference ''(+ x 0XfF)'' ''0x1'' ''0'' ''0'' = (True,''256'' @ newline)" | |
| 100 | + by eval | |
| 101 | + | |
| 93 | 102 | lemma incomplete_rejected: "prepare ''(if x y)'' = None" |
| 94 | 103 | by eval |
| 95 | 104 | |
src/Frontend.thy modified
| @@ -13,11 +13,25 @@ fun lex :: "string \<Rightarrow> string \<Rightarrow> string list \<Rightarrow> | ||
| 13 | 13 | else if c = CHR ''('' \<or> c = CHR '')'' then lex cs [] ([c] # finish word out) |
| 14 | 14 | else lex cs (c # word) out)" |
| 15 | 15 | |
| 16 | -definition number :: "string \<Rightarrow> nat option" where | |
| 17 | - "number s = (if s = [] \<or> \<not> list_all (\<lambda>c. 48 \<le> nat_of_char c \<and> nat_of_char c < 58) s | |
| 18 | - then None else let n = foldl (\<lambda>n c. min (2 ^ 64) (10 * n + nat_of_char c - 48)) 0 s in | |
| 16 | +fun digit :: "char \<Rightarrow> nat" where | |
| 17 | + "digit c = (let n = nat_of_char c in | |
| 18 | + if 48 \<le> n \<and> n < 58 then n - 48 else | |
| 19 | + if 65 \<le> n \<and> n < 71 then n - 55 else | |
| 20 | + if 97 \<le> n \<and> n < 103 then n - 87 else 16)" | |
| 21 | + | |
| 22 | +definition parse_digits :: "nat \<Rightarrow> string \<Rightarrow> nat option" where | |
| 23 | + "parse_digits base s = (if s = [] \<or> \<not> list_all (\<lambda>c. digit c < base) s | |
| 24 | + then None else let n = foldl (\<lambda>n c. min (2 ^ 64) (base * n + digit c)) 0 s in | |
| 19 | 25 | if n < 2 ^ 64 then Some n else None)" |
| 20 | 26 | |
| 27 | +definition number :: "string \<Rightarrow> nat option" where | |
| 28 | + "number s = (case s of a # b # rest \<Rightarrow> | |
| 29 | + if a = CHR ''0'' \<and> (b = CHR ''x'' \<or> b = CHR ''X'') then parse_digits 16 rest | |
| 30 | + else parse_digits 10 s | _ \<Rightarrow> parse_digits 10 s)" | |
| 31 | + | |
| 32 | +theorem number_bound: "number s = Some n \<Longrightarrow> n < 2 ^ 64" | |
| 33 | + by (auto simp: number_def parse_digits_def Let_def split: list.splits if_splits) | |
| 34 | + | |
| 21 | 35 | definition valid_name :: "string \<Rightarrow> bool" where |
| 22 | 36 | "valid_name s = (s \<noteq> [] \<and> list_all (\<lambda>c. (97 \<le> nat_of_char c \<and> nat_of_char c \<le> 122)) s |
| 23 | 37 | \<and> s \<noteq> ''let'' \<and> s \<noteq> ''if'')" |
tests/cli.py added
| @@ -0,0 +1,34 @@ | ||
| 1 | +from pathlib import Path | |
| 2 | +import subprocess | |
| 3 | +import tempfile | |
| 4 | + | |
| 5 | + | |
| 6 | +ROOT = Path(__file__).resolve().parents[1] | |
| 7 | + | |
| 8 | + | |
| 9 | +def invoke(*args, ok=True, data=None, preexec_fn=None): | |
| 10 | + result = subprocess.run([str(ROOT / '.build/remy'), *map(str, args)], input=data, | |
| 11 | + capture_output=True, text=True, timeout=30, preexec_fn=preexec_fn) | |
| 12 | + assert (result.returncode == 0) == ok, (args, result.stdout, result.stderr) | |
| 13 | + return result.stdout if ok else result.stderr | |
| 14 | + | |
| 15 | + | |
| 16 | +def main(): | |
| 17 | + with tempfile.TemporaryDirectory() as directory: | |
| 18 | + source, binary = Path(directory) / 'source', Path(directory) / 'binary' | |
| 19 | + for text, expected in [('0x0',0),('0xff',255),('0X7F',127),('0xffffffffffffffff',(1 << 64)-1), | |
| 20 | + ('(+ 0xffffffffffffffff 1)',0),('(< 0x8000000000000000 0xffffffffffffffff)',1)]: | |
| 21 | + source.write_text(text) | |
| 22 | + assert int(invoke('eval',source,'0','0','0')) == expected, text | |
| 23 | + source.write_text('(+ x y)') | |
| 24 | + assert int(invoke('eval',source,'0xFF','0x1','0x0')) == 256 | |
| 25 | + for text in ['0x','0x10000000000000000','0xfg','0xffextra','-0x1']: | |
| 26 | + source.write_text(text) | |
| 27 | + binary.write_bytes(b'preserve') | |
| 28 | + invoke(source,binary,ok=False) | |
| 29 | + assert binary.read_bytes() == b'preserve', text | |
| 30 | + print('CLI literal and rejection checks passed') | |
| 31 | + | |
| 32 | + | |
| 33 | +if __name__ == '__main__': | |
| 34 | + main() | |