From 75a52175806c238d0b18ff0878be652f95c5ac77 Mon Sep 17 00:00:00 2001 From: james Date: Sat, 3 Oct 2026 12:00:00 +0100 Subject: [PATCH] feat(frontend): parameterise checked compiler resource limits --- cli/driver.ML | 11 +++++---- src/Export.thy | 2 +- src/Frontend.thy | 62 ++++++++++++++++++++++++++++++++++++------------ tests/cli.py | 7 ++++++ 4 files changed, 62 insertions(+), 20 deletions(-) diff --git a/cli/driver.ML b/cli/driver.ML index 60a3424dca13fada197c5ba36a0a9cf903112b72..2feec6f67ac9e87132aa6fd2e71375a744d79eb2 100644 --- a/cli/driver.ML +++ b/cli/driver.ML @@ -26,15 +26,18 @@ fun output (ok, message) = (TextIO.output (if ok then TextIO.stdOut else TextIO.stdErr, text message); if ok then () else OS.Process.exit OS.Process.failure); +fun emit destination ((ok, bytes), report) = + if ok then (write destination bytes; output (true,report)) else output (false,report); + fun main () = (case CommandLine.arguments () of ["vectors", source, destination] => (case Remy.vectors (read source) of (true, bytes) => write destination bytes | result => output result) | ["eval", source, x, y, t] => output (Remy.reference (read source) (chars x) (chars y) (chars t)) - | [source, destination] => - let val ((ok, bytes), report) = Remy.artifact (read source) - in if ok then (write destination bytes; output (true,report)) else output (false,report) end - | _ => raise Fail "usage: remy source binary | remy vectors source data | remy eval source x y t") + | ["limits", depth, nodes, stack, source, destination] => + emit destination (Remy.configured (chars depth) (chars nodes) (chars stack) (read source)) + | [source, destination] => emit destination (Remy.artifact (read source)) + | _ => raise Fail "usage: remy limits depth nodes stack source binary | remy source binary | remy vectors source data | remy eval source x y t") handle exn => (TextIO.output (TextIO.stdErr, "remy: " ^ General.exnMessage exn ^ "\n"); OS.Process.exit OS.Process.failure); diff --git a/src/Export.thy b/src/Export.thy index 266c5362900307161a8ec4fcb7fff5b99374dcce..de0c450a510d0296cebdeb27219befd19638238c 100644 --- a/src/Export.thy +++ b/src/Export.thy @@ -6,6 +6,6 @@ definition ascii :: "integer \ char" where "ascii = char_of" definition ordinal :: "char \ integer" where "ordinal = of_char" -export_code artifact vectors reference ascii ordinal in SML module_name Remy file_prefix remy +export_code configured artifact vectors reference ascii ordinal in SML module_name Remy file_prefix remy end diff --git a/src/Frontend.thy b/src/Frontend.thy index e52ba10c2dfe874f76e57e2d1157edb05f6df405..35411f8346141939a6e22aff7a31ccc83ad9cbfb 100644 --- a/src/Frontend.thy +++ b/src/Frontend.thy @@ -104,24 +104,45 @@ next drule close_expression; auto dest: Suc.IH) qed -definition prepare :: "string \ expression option" where - "prepare s = (if \ list_all (\c. nat_of_char c < 128) s then None else - Option.bind (parse 128 [] (lex s [] [])) (\(e,rest). - if rest = [] \ nodes e \ 4096 then +record limits = + depth_budget :: nat + node_budget :: nat + stack_budget :: nat + +definition defaults :: limits where + "defaults = \depth_budget = 128, node_budget = 4096, stack_budget = 512\" + +definition valid_limits :: "limits \ bool" where + "valid_limits lim = (depth_budget lim \ 128 \ node_budget lim \ 4096 \ stack_budget lim \ 512)" + +definition prepare_with :: "limits \ string \ expression option" where + "prepare_with lim s = (if \ valid_limits lim \ \ list_all (\c. nat_of_char c < 128) s then None else + Option.bind (parse (depth_budget lim) [] (lex s [] [])) (\(e,rest). + if rest = [] \ nodes e \ node_budget lim then let code = compile (optimise e) [] in - if check code 0 = Some 1 \ demand (optimise e) \ 512 \ list_all encodable (native code) + if check code 0 = Some 1 \ demand (optimise e) \ stack_budget lim \ list_all encodable (native code) then Some e else None else None))" +definition prepare :: "string \ expression option" where + "prepare = prepare_with defaults" + +lemma prepare_with_scoped: "prepare_with lim s = Some e \ scoped 0 e" + by (auto simp: prepare_with_def Let_def dest: parse_scoped split: if_splits bind_splits prod.splits) + +lemma prepare_with_bounded: + "prepare_with lim s = Some e \ bounded (stack_budget lim) (compile (optimise e) []) 0" + by (auto simp: prepare_with_def Let_def closed_demand optimise_scoped dest: parse_scoped split: if_splits bind_splits prod.splits) + lemma prepare_scoped: "prepare s = Some e \ scoped 0 e" - by (auto simp: prepare_def Let_def dest: parse_scoped split: if_splits bind_splits prod.splits) + unfolding prepare_def using prepare_with_scoped by blast lemma prepare_bounded: "prepare s = Some e \ bounded 512 (compile (optimise e) []) 0" - by (auto simp: prepare_def Let_def closed_demand optimise_scoped dest: parse_scoped split: if_splits bind_splits prod.splits) + using prepare_with_bounded[where lim=defaults] by (simp add: prepare_def defaults_def) lemma prepare_encodable: "prepare s = Some e \ list_all encodable (native (compile (optimise e) []))" - by (auto simp: prepare_def Let_def split: if_splits bind_splits prod.splits) + by (auto simp: prepare_def prepare_with_def Let_def split: if_splits bind_splits prod.splits) theorem prepared_correct: "prepare source = Some e \ @@ -195,22 +216,33 @@ termination by (relation "measure (\(fuel,names,tokens,pos). fuel)") aut declare diagnose.simps [simp del] -definition source_error :: "string \ string" where - "source_error s = (if \ list_all (\c. nat_of_char c < 128) s then ''source must contain ASCII'' @ newline else - case diagnose 128 [] (lex s [] []) 0 of +definition source_error_with :: "limits \ string \ string" where + "source_error_with lim s = (if \ valid_limits lim then ''limits exceed compiler bounds'' @ newline else if \ list_all (\c. nat_of_char c < 128) s then ''source must contain ASCII'' @ newline else + case diagnose (depth_budget lim) [] (lex s [] []) 0 of Failed (Unexpected pos) \ ''syntax error at token '' @ decimal pos @ newline | Failed (Exhausted pos) \ ''parse depth limit exceeded at token '' @ decimal pos @ newline | Parsed (e,rest,pos) \ if rest \ [] then ''syntax error at token '' @ decimal pos @ newline - else if nodes e > 4096 then ''program exceeds 4096 nodes'' @ newline - else if demand (optimise e) > 512 then ''evaluation stack exceeds 512 words'' @ newline + else if nodes e > node_budget lim then ''program exceeds '' @ decimal (node_budget lim) @ '' nodes'' @ newline + else if demand (optimise e) > stack_budget lim then ''evaluation stack exceeds '' @ decimal (stack_budget lim) @ '' words'' @ newline else ''native validation failed'' @ newline)" -definition artifact :: "string \ (bool \ string) \ string" where - "artifact s = (case prepare s of None \ ((False,[]), source_error s) +definition artifact_with :: "limits \ string \ (bool \ string) \ string" where + "artifact_with lim s = (case prepare_with lim s of None \ ((False,[]), source_error_with lim s) | Some e \ let opt = optimise e; bytes = executable e in ((True, map char_of_nat bytes), decimal (nodes e) @ '' nodes -> '' @ decimal (nodes opt) @ '' nodes, '' @ decimal (length bytes) @ '' bytes, '' @ decimal (demand opt) @ '' stack words'' @ newline))" +definition source_error :: "string \ string" where + "source_error = source_error_with defaults" + +definition artifact :: "string \ (bool \ string) \ string" where + "artifact = artifact_with defaults" + +definition configured :: "string \ string \ string \ string \ (bool \ string) \ string" where + "configured depth count stacktext source = (case (number depth, number count, number stacktext) of + (Some d,Some n,Some k) \ artifact_with \depth_budget=d, node_budget=n, stack_budget=k\ source + | _ \ ((False,[]),''invalid resource limits'' @ newline))" + definition boundary :: "nat list" where "boundary = [0,1,63,64,65,127,255,256,2 ^ 31,2 ^ 32,2 ^ 63,2 ^ 64 - 1]" diff --git a/tests/cli.py b/tests/cli.py index 74398b2ec5f9b72d54f40632395be51129a6c7af..27979cd0cc7d5c555fd3fb018345e449067e2f55 100644 --- a/tests/cli.py +++ b/tests/cli.py @@ -39,6 +39,13 @@ def main(): large = f'(+ {large} {large})' source.write_text(large) assert '4096 nodes' in invoke(source,binary,ok=False) + source.write_text('(+ x y)') + invoke('limits',4,3,2,source,binary) + for depth, nodes, stack, message in [(4,2,2,'2 nodes'),(4,3,1,'1 words'), + (0,3,2,'parse depth'),(129,3,2,'compiler bounds'),('bad',3,2,'invalid resource')]: + binary.write_bytes(b'preserve') + assert message in invoke('limits',depth,nodes,stack,source,binary,ok=False) + assert binary.read_bytes() == b'preserve' source.write_text('é') assert 'ASCII' in invoke(source,binary,ok=False) for text in ['0x','0x10000000000000000','0xfg','0xffextra','-0x1']: