Lean: Use generated sail_model_init function

Brings the number of passing test cases up to 161
rems-project · Mar 3, 2025 · f24c9f3 · f24c9f3
1 parent 2d3900c
commit f24c9f3
Show file tree

Hide file tree

Showing 34 changed files with 95 additions and 8 deletions.
diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml
@@ -1206,7 +1206,7 @@ let doc_instantiations ctx env =
       ^^ hardline
 
 let main_function_stub has_registers =
-  let main_call = if has_registers then "(initialize_registers >=> sail_main)" else "sail_main" in
+  let main_call = if has_registers then "(sail_model_init >=> sail_main)" else "sail_main" in
   nest 2
     (separate hardline
        [

diff --git a/src/sail_lean_backend/sail_plugin_lean.ml b/src/sail_lean_backend/sail_plugin_lean.ml
@@ -144,6 +144,7 @@ let lean_rewrites =
     (* ("prover_regstate", [Bool_arg false]); *)
     (* ("remove_assert", rewrite_ast_remove_assert); *)
     ("top_sort_defs", []);
+    ("add_register_init_function", []);
     ("const_prop_mutrec", [String_arg "coq"]);
     ("exp_lift_assign", []);
     ("early_return", []);

diff --git a/test/lean/SailTinyArm.expected.lean b/test/lean/SailTinyArm.expected.lean
@@ -2233,6 +2233,9 @@ def initialize_registers (_ : Unit) : SailM Unit := do
   writeReg R1 (← (undefined_bitvector 64))
   writeReg R0 (← (undefined_bitvector 64))
 
+def sail_model_init (x_0 : Unit) : SailM Unit := do
+  (initialize_registers ())
+
 end Functions
 open Functions
 
diff --git a/test/lean/append.expected.lean b/test/lean/append.expected.lean
@@ -137,6 +137,9 @@ def unif_vector_subrange (i : Nat) (v : (BitVec (8 * i + 8))) : (BitVec 8) :=
 def initialize_registers (_ : Unit) : Unit :=
   ()
 
+def sail_model_init (x_0 : Unit) : Unit :=
+  (initialize_registers ())
+
 end Functions
 open Functions
 
diff --git a/test/lean/atom_bool.expected.lean b/test/lean/atom_bool.expected.lean
@@ -44,6 +44,9 @@ def foo (_ : Unit) : Bool :=
 def initialize_registers (_ : Unit) : Unit :=
   ()
 
+def sail_model_init (x_0 : Unit) : Unit :=
+  (initialize_registers ())
+
 end Functions
 open Functions
 
diff --git a/test/lean/bitfield.expected.lean b/test/lean/bitfield.expected.lean
@@ -200,6 +200,9 @@ def _set_cr_type_LT (r_ref : (RegisterRef (BitVec 8))) (v : (BitVec 1)) : SailM
 def initialize_registers (_ : Unit) : SailM Unit := do
   writeReg R (← (undefined_cr_type ()))
 
+def sail_model_init (x_0 : Unit) : SailM Unit := do
+  (initialize_registers ())
+
 end Functions
 open Functions
 
diff --git a/test/lean/bitvec_operation.expected.lean b/test/lean/bitvec_operation.expected.lean
@@ -187,6 +187,9 @@ def vector_literal (x : Int) (y : Int) : (Vector Int 2) :=
 def initialize_registers (_ : Unit) : Unit :=
   ()
 
+def sail_model_init (x_0 : Unit) : Unit :=
+  (initialize_registers ())
+
 end Functions
 open Functions
 
diff --git a/test/lean/early_return.expected.lean b/test/lean/early_return.expected.lean
@@ -494,6 +494,9 @@ def initialize_registers (_ : Unit) : SailM Unit := do
   writeReg r_C (← (undefined_E ()))
   writeReg r (← (undefined_nat ()))
 
+def sail_model_init (x_0 : Unit) : SailM Unit := do
+  (initialize_registers ())
+
 end Functions
 open Functions
 
diff --git a/test/lean/enum.expected.lean b/test/lean/enum.expected.lean
@@ -146,6 +146,9 @@ def num_of_E (arg_ : E) : Int :=
 def initialize_registers (_ : Unit) : Unit :=
   ()
 
+def sail_model_init (x_0 : Unit) : Unit :=
+  (initialize_registers ())
+
 end Functions
 open Functions
 
diff --git a/test/lean/errors.expected.lean b/test/lean/errors.expected.lean
@@ -143,6 +143,9 @@ def test_assert (b : Bool) : SailM (BitVec 1) := do
 def initialize_registers (_ : Unit) : SailM Unit := do
   writeReg dummy (← (undefined_bit ()))
 
+def sail_model_init (x_0 : Unit) : SailM Unit := do
+  (initialize_registers ())
+
 end Functions
 open Functions
 
diff --git a/test/lean/extern.expected.lean b/test/lean/extern.expected.lean
@@ -303,6 +303,9 @@ def extern_hex_str_upper (_ : Unit) : String :=
 def initialize_registers (_ : Unit) : Unit :=
   ()
 
+def sail_model_init (x_0 : Unit) : Unit :=
+  (initialize_registers ())
+
 end Functions
 open Functions
 
diff --git a/test/lean/extern_bitvec.expected.lean b/test/lean/extern_bitvec.expected.lean
@@ -139,6 +139,9 @@ def extern_vector_length (x : (Vector Int 3)) : Int :=
 def initialize_registers (_ : Unit) : Unit :=
   ()
 
+def sail_model_init (x_0 : Unit) : Unit :=
+  (initialize_registers ())
+
 end Functions
 open Functions
 
diff --git a/test/lean/implicit.expected.lean b/test/lean/implicit.expected.lean
@@ -139,6 +139,9 @@ def slice_mask2 {n : _} (i : (BitVec n)) (l : (BitVec n)) (b : Bool) : (BitVec n
 def initialize_registers (_ : Unit) : Unit :=
   ()
 
+def sail_model_init (x_0 : Unit) : Unit :=
+  (initialize_registers ())
+
 end Functions
 open Functions
 
diff --git a/test/lean/ite.expected.lean b/test/lean/ite.expected.lean
@@ -162,6 +162,9 @@ def initialize_registers (_ : Unit) : SailM Unit := do
   writeReg R (← (undefined_nat ()))
   writeReg B (← (undefined_bool ()))
 
+def sail_model_init (x_0 : Unit) : SailM Unit := do
+  (initialize_registers ())
+
 end Functions
 open Functions
 
diff --git a/test/lean/let.expected.lean b/test/lean/let.expected.lean
@@ -136,6 +136,9 @@ def baz (_ : Unit) : SailM (BitVec 16) := do
 def initialize_registers (_ : Unit) : Unit :=
   ()
 
+def sail_model_init (x_0 : Unit) : Unit :=
+  (initialize_registers ())
+
 end Functions
 open Functions
 
diff --git a/test/lean/loop.expected.lean b/test/lean/loop.expected.lean
@@ -245,6 +245,9 @@ def while_loopmultiplevar (m : Nat) (n : Nat) : Nat := Id.run do
 def initialize_registers (_ : Unit) : SailM Unit := do
   writeReg r (← (undefined_nat ()))
 
+def sail_model_init (x_0 : Unit) : SailM Unit := do
+  (initialize_registers ())
+
 end Functions
 open Functions
 
diff --git a/test/lean/mapping.expected.lean b/test/lean/mapping.expected.lean
@@ -271,6 +271,9 @@ def size_bits3_backwards_matches (arg_ : (BitVec 2)) : Bool :=
 def initialize_registers (_ : Unit) : Unit :=
   ()
 
+def sail_model_init (x_0 : Unit) : Unit :=
+  (initialize_registers ())
+
 end Functions
 open Functions
 
diff --git a/test/lean/match.expected.lean b/test/lean/match.expected.lean
@@ -207,6 +207,9 @@ def initialize_registers (_ : Unit) : SailM Unit := do
   writeReg r_B (← (undefined_E ()))
   writeReg r_C (← (undefined_E ()))
 
+def sail_model_init (x_0 : Unit) : SailM Unit := do
+  (initialize_registers ())
+
 end Functions
 open Functions
 
diff --git a/test/lean/match_bv.expected.lean b/test/lean/match_bv.expected.lean
@@ -176,6 +176,9 @@ def write_CSR2 (v__30 : (BitVec 12)) : SailM Bool := do
 def initialize_registers (_ : Unit) : Unit :=
   ()
 
+def sail_model_init (x_0 : Unit) : Unit :=
+  (initialize_registers ())
+
 end Functions
 open Functions
 
diff --git a/test/lean/option.expected.lean b/test/lean/option.expected.lean
@@ -134,6 +134,9 @@ def option_match (x : (Option Unit)) (y : (BitVec 1)) : (Option (BitVec 1)) :=
 def initialize_registers (_ : Unit) : Unit :=
   ()
 
+def sail_model_init (x_0 : Unit) : Unit :=
+  (initialize_registers ())
+
 end Functions
 open Functions
 
diff --git a/test/lean/range.expected.lean b/test/lean/range.expected.lean
@@ -144,6 +144,9 @@ def f_unkn (x : Int) : Int :=
 def initialize_registers (_ : Unit) : Unit :=
   ()
 
+def sail_model_init (x_0 : Unit) : Unit :=
+  (initialize_registers ())
+
 end Functions
 open Functions
 
diff --git a/test/lean/register_vector.expected.lean b/test/lean/register_vector.expected.lean
@@ -257,6 +257,9 @@ def initialize_registers (_ : Unit) : SailM Unit := do
   writeReg R1 (← (undefined_bitvector 64))
   writeReg R0 (← (undefined_bitvector 64))
 
+def sail_model_init (x_0 : Unit) : SailM Unit := do
+  (initialize_registers ())
+
 end Functions
 open Functions
 
diff --git a/test/lean/registers.expected.lean b/test/lean/registers.expected.lean
@@ -159,6 +159,9 @@ def initialize_registers (_ : Unit) : SailM Unit := do
   writeReg NAT (← (undefined_nat ()))
   writeReg BIT (← (undefined_bit ()))
 
+def sail_model_init (x_0 : Unit) : SailM Unit := do
+  (initialize_registers ())
+
 end Functions
 open Functions
 
diff --git a/test/lean/riscv_duopod.expected.lean b/test/lean/riscv_duopod.expected.lean
@@ -252,6 +252,9 @@ def initialize_registers (_ : Unit) : SailM Unit := do
   writeReg nextPC (← (undefined_bitvector 64))
   writeReg Xs (← (undefined_vector 32 (← (undefined_bitvector 64))))
 
+def sail_model_init (x_0 : Unit) : SailM Unit := do
+  (initialize_registers ())
+
 end Functions
 open Functions
 
diff --git a/test/lean/run_tests.py b/test/lean/run_tests.py
@@ -36,7 +36,6 @@
     'primop',
     'poly_pair',
     'assign_rename_bug',
-    'config',
     'cheri128_hsb',
     'union_variant_names',
     'lib_hex_bits',
@@ -53,7 +52,6 @@
     'spc_mappings',
     'concurrency_interface',
     'vector_example',
-    'reg_init_let',
     'for_shadow',
     'list_torture',
     'option_nest',
@@ -65,22 +63,17 @@
     'type_if_bits',
     'poly_union',
     'nexp_simp_euclidian',
-    'config_register_ones',
     'toplevel_tyvar',
     'ediv_from_tdiv',
     'concurrency_interface_write',
     'read_write_ram',
     'issue136',
     'fail_exception',
-    'natural_sort_reg',
     'option_option',
     'anf_as_pattern',
     'poly_mapping',
     'real_prop',
-    'vector_init',
-    'partial_mapping',
     'lib_dec_bits',
-    'list_list_eq',
     'constructor247',
     'config_vec_list',
     'deep_poly_nest',

diff --git a/test/lean/struct.expected.lean b/test/lean/struct.expected.lean
@@ -173,6 +173,9 @@ def match_struct (value : My_struct) : SailM Int := do
 def initialize_registers (_ : Unit) : Unit :=
   ()
 
+def sail_model_init (x_0 : Unit) : Unit :=
+  (initialize_registers ())
+
 end Functions
 open Functions
 
diff --git a/test/lean/struct_of_enum.expected.lean b/test/lean/struct_of_enum.expected.lean
@@ -150,6 +150,9 @@ def undefined_s_test (_ : Unit) : SailM s_test := do
 def initialize_registers (_ : Unit) : Unit :=
   ()
 
+def sail_model_init (x_0 : Unit) : Unit :=
+  (initialize_registers ())
+
 end Functions
 open Functions
 
diff --git a/test/lean/trivial.expected.lean b/test/lean/trivial.expected.lean
@@ -44,6 +44,9 @@ def foo (y : Unit) : Unit :=
 def initialize_registers (_ : Unit) : Unit :=
   ()
 
+def sail_model_init (x_0 : Unit) : Unit :=
+  (initialize_registers ())
+
 end Functions
 open Functions
 
diff --git a/test/lean/tuples.expected.lean b/test/lean/tuples.expected.lean
@@ -57,6 +57,9 @@ def tuple2 (_ : Unit) : SailM (Int × Int) := do
 def initialize_registers (_ : Unit) : Unit :=
   ()
 
+def sail_model_init (x_0 : Unit) : Unit :=
+  (initialize_registers ())
+
 end Functions
 open Functions
 
diff --git a/test/lean/type_kid.expected.lean b/test/lean/type_kid.expected.lean
@@ -45,6 +45,9 @@ def foo (x : k_a) : (k_a × k_a) :=
 def initialize_registers (_ : Unit) : Unit :=
   ()
 
+def sail_model_init (x_0 : Unit) : Unit :=
+  (initialize_registers ())
+
 end Functions
 open Functions
 
diff --git a/test/lean/typedef.expected.lean b/test/lean/typedef.expected.lean
@@ -145,6 +145,9 @@ def uses_xlen_term (_ : Unit) : Int :=
 def initialize_registers (_ : Unit) : Unit :=
   ()
 
+def sail_model_init (x_0 : Unit) : Unit :=
+  (initialize_registers ())
+
 end Functions
 open Functions
 
diff --git a/test/lean/typquant.expected.lean b/test/lean/typquant.expected.lean
@@ -201,6 +201,9 @@ def termination (n : Nat) : Int :=
 def initialize_registers (_ : Unit) : Unit :=
   ()
 
+def sail_model_init (x_0 : Unit) : Unit :=
+  (initialize_registers ())
+
 end Functions
 open Functions
 
diff --git a/test/lean/undefined.expected.lean b/test/lean/undefined.expected.lean
@@ -50,6 +50,9 @@ def bar (n : Int) : SailM (Vector Int 4) := do
 def initialize_registers (_ : Unit) : Unit :=
   ()
 
+def sail_model_init (x_0 : Unit) : Unit :=
+  (initialize_registers ())
+
 end Functions
 open Functions
 
diff --git a/test/lean/union.expected.lean b/test/lean/union.expected.lean
@@ -88,6 +88,9 @@ def use_is_none (opt : (my_option k_a)) : Bool :=
 def initialize_registers (_ : Unit) : Unit :=
   ()
 
+def sail_model_init (x_0 : Unit) : Unit :=
+  (initialize_registers ())
+
 end Functions
 open Functions