From c9eeaae22a0077829f78d61110998992a59156b8 Mon Sep 17 00:00:00 2001 From: Raito Bezarius Date: Tue, 11 Feb 2025 15:21:20 +0100 Subject: [PATCH 1/5] feat(test/lean): support self-tests from the C backend "self-tests" refers to self contained Sail programs that prints or do simple self contained computations. They are used in the C backend for testing and are ran. We "steal" from the C backend examples and try to run the Lean programs extracted in a similar fashion and expect to obtain similar results. Not all self tests are supported because of missing translation stubs. Note that we reuse the `coq-print.splice` translation stub as well. Signed-off-by: Raito Bezarius --- test/lean/run_tests.py | 50 ++++++++++++++++++++++++++++++++++-------- 1 file changed, 41 insertions(+), 9 deletions(-) diff --git a/test/lean/run_tests.py b/test/lean/run_tests.py index 24fc9de9a..1ebfc7e34 100755 --- a/test/lean/run_tests.py +++ b/test/lean/run_tests.py @@ -17,30 +17,61 @@ sail_dir = get_sail_dir() sail = get_sail() +# Self-tests refers to self contained Sail programs in test/c/ which are Sail programs +# that you can run to exercise the language and the extracted output. +# Not all self-tests are supported. +# TODO: once we support many of those, we should make this a `skip_selftests` +include_selftests = { + 'hello_world.sail', +} + print("Sail is {}".format(sail)) print("Sail dir is {}".format(sail_dir)) -def test_lean(): - banner('Testing lean target') - results = Results('lean') - for filenames in chunks(os.listdir('.'), parallel()): +def test_lean(subdir: str, allowed_list: set[str] | None = None, runnable: bool = False): + """ + Run all Sail files available in the `subdir`. + If `runnable` is set to `True`, it will do `lake run` + instead of `lake build`. + """ + banner(f'Testing lean target (sub-directory: {subdir})') + results = Results(subdir) + for filenames in chunks(os.listdir(f'../{subdir}'), parallel()): + os.chdir(f'../{subdir}') tests = {} for filename in filenames: + if allowed_list is not None and filename not in allowed_list: + continue + basename = os.path.splitext(os.path.basename(filename))[0] tests[filename] = os.fork() if tests[filename] == 0: step('rm -r {} || true'.format(basename)) step('mkdir -p {}'.format(basename)) - step('\'{}\' {} --lean --lean-output-dir {}'.format(sail, filename, basename)) - # NOTE: lake --dir does not behave the same as cd $dir && lake build... - step('lake build', cwd=f'{basename}/out') - status = step_with_status('diff {}/out/Out.lean {}.expected.lean'.format(basename, basename)) + # TODO: should probably be dependent on whether print should be pure or effectful. + extra_flags = ' '.join([ + '--splice', + 'coq-print.splice' + ] if runnable else [ ]) + step('\'{}\' {} {} --lean --lean-output-dir {}'.format(sail, extra_flags, filename, basename)) + if runnable: + # NOTE: lake --dir does not behave the same as cd $dir && lake build... + step('lake build', cwd=f'{basename}/out') + else: + step(f'lake run > expect 2> err_status', cwd=f'{basename}/out') + + status = step_with_status(f'diff {basename}/out/Out.lean {basename}.expected.lean') if status != 0: if update_expected: print(f'Overriding file {basename}.expected.lean') step(f'cp {basename}/out/Out.lean {basename}.expected.lean') else: sys.exit(1) + + if runnable: + status = step_with_status(f'diff {basename}/out/expected {basename}.expect') + if status != 0: + sys.exit(1) step('rm -r {}'.format(basename)) print_ok(filename) sys.exit(0) @@ -49,7 +80,8 @@ def test_lean(): xml = '\n' -xml += test_lean() +xml += test_lean('lean') +xml += test_lean('c', allowed_list=include_selftests, runnable=True) xml += '\n' From 328d2e026d27d9650915445a839b98926fed20e6 Mon Sep 17 00:00:00 2001 From: Raito Bezarius Date: Tue, 11 Feb 2025 15:21:42 +0100 Subject: [PATCH 2/5] chore(test): ignore output directories Running the tests may produce extraction output directories, we ignore them to avoid committing them by mistake. Signed-off-by: Raito Bezarius --- test/c/.gitignore | 1 + test/lean/.gitignore | 1 + 2 files changed, 2 insertions(+) create mode 100644 test/c/.gitignore create mode 100644 test/lean/.gitignore diff --git a/test/c/.gitignore b/test/c/.gitignore new file mode 100644 index 000000000..89f9ac04a --- /dev/null +++ b/test/c/.gitignore @@ -0,0 +1 @@ +out/ diff --git a/test/lean/.gitignore b/test/lean/.gitignore new file mode 100644 index 000000000..89f9ac04a --- /dev/null +++ b/test/lean/.gitignore @@ -0,0 +1 @@ +out/ From e2de9b67f1e6c67041fc3abb26b71b301b6b3836 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9o=20Stefanesco?= Date: Tue, 11 Feb 2025 16:06:57 +0000 Subject: [PATCH 3/5] Add stub for main functions --- src/sail_lean_backend/Sail/Sail.lean | 24 ++++++++++ src/sail_lean_backend/pretty_print_lean.ml | 21 +++++++- src/sail_lean_backend/sail_plugin_lean.ml | 56 ++++++++++++++-------- test/c/hello_world.expected.lean | 15 ++++++ test/lean/hello_world.expected.lean | 0 test/lean/run_tests.py | 4 +- 6 files changed, 96 insertions(+), 24 deletions(-) create mode 100644 test/c/hello_world.expected.lean create mode 100644 test/lean/hello_world.expected.lean diff --git a/src/sail_lean_backend/Sail/Sail.lean b/src/sail_lean_backend/Sail/Sail.lean index 6c3bc3623..932e6e600 100644 --- a/src/sail_lean_backend/Sail/Sail.lean +++ b/src/sail_lean_backend/Sail/Sail.lean @@ -48,11 +48,17 @@ inductive Error where | Assertion (s : String) open Error +def Error.print : Error → String +| Exit => "Exit" +| Unreachable => "Unreachable" +| Assertion s => s!"Assertion failed: {s}" + structure SequentialState (RegisterType : Register → Type) (c : ChoiceSource) where regs : Std.DHashMap Register RegisterType choiceState : c.α mem : Unit tags : Unit + sail_output : Array String -- TODO: be able to use the IO monad to run inductive RegisterRef (RegisterType : Register → Type) : Type → Type where | Reg (r : Register) : RegisterRef _ (RegisterType r) @@ -111,6 +117,23 @@ def vectorAccess [Inhabited α] (v : Vector α m) (n : Nat) := v[n]! def assert (p : Bool) (s : String) : PreSailM RegisterType c Unit := if p then pure () else throw (Assertion s) +/- def print_effect (s : String) : IO Unit := IO.print s -/ + +def print_effect (str : String) : PreSailM RegisterType c Unit := + modify fun s ↦ { s with sail_output := s.sail_output.push str } + +def print_endline_effect (str : String) : PreSailM RegisterType c Unit := + print_effect s!"{str}\n" + +def main_of_sail_main (initialState : SequentialState RegisterType c) (main : Unit → PreSailM RegisterType c Unit) : IO Unit := do + let res := main () |>.run initialState + match res with + | .ok _ s => do + for m in s.sail_output do + IO.print m + | .error e _ => do + IO.println s!"Error while running the sail program!: {e.print}" + end Regs namespace BitVec @@ -153,4 +176,5 @@ namespace Int def intAbs (x : Int) : Int := Int.ofNat (Int.natAbs x) end Int + end Sail diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index 62662e3cc..98213559a 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -11,6 +11,8 @@ open Pretty_print_common type global_context = { effect_info : Effects.side_effect_info } +let the_main_function_has_been_seen = ref false + type context = { global : global_context; env : Type_check.env; @@ -41,6 +43,9 @@ let rec fix_id name = match name with (* Lean keywords to avoid, to expand as needed *) | "rec" -> name ^ "'" + | "main" -> + the_main_function_has_been_seen := true; + "sail_main" | _ -> if String.contains name '#' then fix_id (String.concat "_" (Util.split_on_char '#' name)) else name let doc_id_ctor (Id_aux (i, _)) = @@ -734,6 +739,17 @@ let doc_monad_abbrev (has_registers : bool) = in separate space [string "abbrev"; string "SailM"; coloneq; pp_register_type] ^^ hardline ^^ hardline +let main_function_stub = + nest 2 + (separate hardline + [ + string "def main (_ : List String) : IO UInt32 := do"; + string "main_of_sail_main ⟨default, (), default, default, default⟩ sail_main"; + string "return 0"; + empty; + ] + ) + let pp_ast_lean (env : Type_check.env) effect_info ({ defs; _ } as ast : Libsail.Type_check.typed_ast) o = let defs = remove_imports defs 0 in let regs = State.find_registers defs in @@ -742,5 +758,6 @@ let pp_ast_lean (env : Type_check.env) effect_info ({ defs; _ } as ast : Libsail let register_refs = if has_registers then doc_reg_info env global regs else empty in let monad = doc_monad_abbrev has_registers in let types, fundefs = doc_defs (initial_context env global) defs in - print o (types ^^ register_refs ^^ monad ^^ fundefs); - () + let main_function = if !the_main_function_has_been_seen then main_function_stub else empty in + print o (types ^^ register_refs ^^ monad ^^ fundefs ^^ main_function); + !the_main_function_has_been_seen diff --git a/src/sail_lean_backend/sail_plugin_lean.ml b/src/sail_lean_backend/sail_plugin_lean.ml index 52118389b..7b813fc72 100644 --- a/src/sail_lean_backend/sail_plugin_lean.ml +++ b/src/sail_lean_backend/sail_plugin_lean.ml @@ -153,8 +153,15 @@ let lean_rewrites = ("attach_effects", []); ] -let create_lake_project (out_name : string) default_sail_dir = - (* Change the base directory if the option '--lean-output-dir' is set *) +type lean_context = { + out_name : string; + out_name_camel : string; + sail_dir : string; + main_file : out_channel; + lakefile : out_channel; +} + +let start_lean_output (out_name : string) default_sail_dir = let base_dir = match !opt_lean_output_dir with Some dir -> dir | None -> "." in let project_dir = Filename.concat base_dir out_name in if !opt_lean_force_output && Sys.file_exists project_dir && Sys.is_directory project_dir then ( @@ -167,35 +174,44 @@ let create_lake_project (out_name : string) default_sail_dir = output_string gitignore "/.lake"; close_out gitignore; let lean_toolchain = open_out (Filename.concat project_dir "lean-toolchain") in - (* Set the Lean version *) output_string lean_toolchain ("leanprover/" ^ lean_version); close_out lean_toolchain; - (* Camel-case the output name *) + let sail_dir = Reporting.get_sail_dir default_sail_dir in let out_name_camel = Libsail.Util.to_upper_camel_case out_name in - let lakefile = open_out (Filename.concat project_dir "lakefile.toml") in - output_string lakefile - ("name = \"" ^ out_name ^ "\"\ndefaultTargets = [\"" ^ out_name_camel ^ "\"]\n\n[[lean_lib]]\nname = \"" - ^ out_name_camel ^ "\"" - ); - close_out lakefile; let lean_src_dir = Filename.concat project_dir out_name_camel in if not (Sys.file_exists lean_src_dir) then Unix.mkdir lean_src_dir 0o775; - let sail_dir = Reporting.get_sail_dir default_sail_dir in let _ = Unix.system ("cp -r " ^ Filename.quote (sail_dir ^ "/src/sail_lean_backend/Sail") ^ " " ^ Filename.quote lean_src_dir) in - let project_main = open_out (Filename.concat project_dir (out_name_camel ^ ".lean")) in - output_string project_main ("import " ^ out_name_camel ^ ".Sail.Sail\n\n"); - output_string project_main "open Sail\n\n"; - project_main + let main_file = open_out (Filename.concat project_dir (out_name_camel ^ ".lean")) in + output_string main_file ("import " ^ out_name_camel ^ ".Sail.Sail\n\n"); + output_string main_file "open Sail\n\n"; + let lakefile = open_out (Filename.concat project_dir "lakefile.toml") in + { out_name; out_name_camel; sail_dir; main_file; lakefile } + +let close_context ctx = + close_out ctx.main_file; + close_out ctx.lakefile + +let create_lake_project (ctx : lean_context) executable = + (* Change the base directory if the option '--lean-output-dir' is set *) + output_string ctx.lakefile + ("name = \"" ^ ctx.out_name ^ "\"\ndefaultTargets = [\"" ^ ctx.out_name_camel ^ "\"]\n\n[[lean_lib]]\nname = \"" + ^ ctx.out_name_camel ^ "\"" + ); + if executable then ( + output_string ctx.lakefile "\n\n[[lean_exe]]\n"; + output_string ctx.lakefile "name = \"run\"\n"; + output_string ctx.lakefile ("root = \"" ^ ctx.out_name_camel ^ "\"\n") + ) let output (out_name : string) env effect_info ast default_sail_dir = - let project_main = create_lake_project out_name default_sail_dir in - (* Uncomment for debug output of the Sail code after the rewrite passes *) - (* Pretty_print_sail.output_ast stdout (Type_check.strip_ast ast); *) - Pretty_print_lean.pp_ast_lean env effect_info ast project_main; - close_out project_main + let ctx = start_lean_output out_name default_sail_dir in + let executable = Pretty_print_lean.pp_ast_lean env effect_info ast ctx.main_file in + create_lake_project ctx executable +(* Uncomment for debug output of the Sail code after the rewrite passes *) +(* Pretty_print_sail.output_ast stdout (Type_check.strip_ast ast) *) let lean_target out_name { default_sail_dir; ctx; ast; effect_info; env; _ } = let out_name = match out_name with Some f -> f | None -> "out" in diff --git a/test/c/hello_world.expected.lean b/test/c/hello_world.expected.lean new file mode 100644 index 000000000..7e0fff096 --- /dev/null +++ b/test/c/hello_world.expected.lean @@ -0,0 +1,15 @@ +import Out.Sail.Sail + +open Sail + +abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource + +def sail_main (_ : Unit) : SailM Unit := do + (print_endline_effect "Hello, World!") + +def initialize_registers (_ : Unit) : Unit := + () + +def main (_ : List String) : IO UInt32 := do + main_of_sail_main ⟨default, (), default, default, default⟩ sail_main + return 0 diff --git a/test/lean/hello_world.expected.lean b/test/lean/hello_world.expected.lean new file mode 100644 index 000000000..e69de29bb diff --git a/test/lean/run_tests.py b/test/lean/run_tests.py index 1ebfc7e34..c1254cc71 100755 --- a/test/lean/run_tests.py +++ b/test/lean/run_tests.py @@ -55,10 +55,10 @@ def test_lean(subdir: str, allowed_list: set[str] | None = None, runnable: bool ] if runnable else [ ]) step('\'{}\' {} {} --lean --lean-output-dir {}'.format(sail, extra_flags, filename, basename)) if runnable: + step(f'lake exe run > expected 2> err_status', cwd=f'{basename}/out') + else: # NOTE: lake --dir does not behave the same as cd $dir && lake build... step('lake build', cwd=f'{basename}/out') - else: - step(f'lake run > expect 2> err_status', cwd=f'{basename}/out') status = step_with_status(f'diff {basename}/out/Out.lean {basename}.expected.lean') if status != 0: From 979ef50caa01341a68f9592191f8c61f199cdaf0 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Wed, 12 Feb 2025 12:25:20 +0000 Subject: [PATCH 4/5] Lean: Don't chdir until after os.fork --- test/c/hello_world.expected.lean | 15 --------------- test/lean/run_tests.py | 2 +- 2 files changed, 1 insertion(+), 16 deletions(-) delete mode 100644 test/c/hello_world.expected.lean diff --git a/test/c/hello_world.expected.lean b/test/c/hello_world.expected.lean deleted file mode 100644 index 7e0fff096..000000000 --- a/test/c/hello_world.expected.lean +++ /dev/null @@ -1,15 +0,0 @@ -import Out.Sail.Sail - -open Sail - -abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource - -def sail_main (_ : Unit) : SailM Unit := do - (print_endline_effect "Hello, World!") - -def initialize_registers (_ : Unit) : Unit := - () - -def main (_ : List String) : IO UInt32 := do - main_of_sail_main ⟨default, (), default, default, default⟩ sail_main - return 0 diff --git a/test/lean/run_tests.py b/test/lean/run_tests.py index c1254cc71..ee239a3e4 100755 --- a/test/lean/run_tests.py +++ b/test/lean/run_tests.py @@ -37,7 +37,6 @@ def test_lean(subdir: str, allowed_list: set[str] | None = None, runnable: bool banner(f'Testing lean target (sub-directory: {subdir})') results = Results(subdir) for filenames in chunks(os.listdir(f'../{subdir}'), parallel()): - os.chdir(f'../{subdir}') tests = {} for filename in filenames: if allowed_list is not None and filename not in allowed_list: @@ -46,6 +45,7 @@ def test_lean(subdir: str, allowed_list: set[str] | None = None, runnable: bool basename = os.path.splitext(os.path.basename(filename))[0] tests[filename] = os.fork() if tests[filename] == 0: + os.chdir(f'../{subdir}') step('rm -r {} || true'.format(basename)) step('mkdir -p {}'.format(basename)) # TODO: should probably be dependent on whether print should be pure or effectful. From ff7e2cf7e47799fe18db467ba532ca22acb93adb Mon Sep 17 00:00:00 2001 From: Alasdair Date: Wed, 12 Feb 2025 13:10:39 +0000 Subject: [PATCH 5/5] Lean: Replace hello_world expected output --- test/c/hello_world.expected.lean | 15 +++++++++++++++ test/lean/hello_world.expected.lean | 0 test/lean/run_tests.py | 2 +- 3 files changed, 16 insertions(+), 1 deletion(-) create mode 100644 test/c/hello_world.expected.lean delete mode 100644 test/lean/hello_world.expected.lean diff --git a/test/c/hello_world.expected.lean b/test/c/hello_world.expected.lean new file mode 100644 index 000000000..7e0fff096 --- /dev/null +++ b/test/c/hello_world.expected.lean @@ -0,0 +1,15 @@ +import Out.Sail.Sail + +open Sail + +abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource + +def sail_main (_ : Unit) : SailM Unit := do + (print_endline_effect "Hello, World!") + +def initialize_registers (_ : Unit) : Unit := + () + +def main (_ : List String) : IO UInt32 := do + main_of_sail_main ⟨default, (), default, default, default⟩ sail_main + return 0 diff --git a/test/lean/hello_world.expected.lean b/test/lean/hello_world.expected.lean deleted file mode 100644 index e69de29bb..000000000 diff --git a/test/lean/run_tests.py b/test/lean/run_tests.py index ee239a3e4..65287d583 100755 --- a/test/lean/run_tests.py +++ b/test/lean/run_tests.py @@ -28,7 +28,7 @@ print("Sail is {}".format(sail)) print("Sail dir is {}".format(sail_dir)) -def test_lean(subdir: str, allowed_list: set[str] | None = None, runnable: bool = False): +def test_lean(subdir: str, allowed_list = None, runnable: bool = False): """ Run all Sail files available in the `subdir`. If `runnable` is set to `True`, it will do `lake run`