feat(test/lean): support self-tests from the C backend

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

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

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

test/c/.gitignore

@@ -0,0 +1 @@
+out/

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

test/lean/.gitignore

@@ -0,0 +1 @@
+out/

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 = 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()):
         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:
+                os.chdir(f'../{subdir}')
                 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:
+                    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')
+
+                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 = '<testsuites>\n'
 
-xml += test_lean()
+xml += test_lean('lean')
+xml += test_lean('c', allowed_list=include_selftests, runnable=True)
 
 xml += '</testsuites>\n'