choose prog_gen based on da_isa in bir_lifter_interfaceLib

kth-step · Feb 13, 2024 · 6f323c2 · 6f323c2
1 parent 9f7b460
commit 6f323c2
Show file tree

Hide file tree

Showing 4 changed files with 19 additions and 7 deletions.
diff --git a/examples/riscv/isqrt/isqrtScript.sml b/examples/riscv/isqrt/isqrtScript.sml
@@ -7,6 +7,6 @@ val _ = set_trace "bir_inst_lifting.DEBUG_LEVEL" 2;
 
 val _ = new_theory "isqrt";
 
-val _ = lift_da_and_store "isqrt" "isqrt.da" ((Arbnum.fromInt 0), (Arbnum.fromInt 0x1000000));
+val _ = lift_da_and_store "isqrt" "isqrt.da" da_riscv ((Arbnum.fromInt 0), (Arbnum.fromInt 0x1000000));
 
 val _ = export_theory ();
diff --git a/examples/riscv/swap/swapScript.sml b/examples/riscv/swap/swapScript.sml
@@ -7,6 +7,6 @@ val _ = set_trace "bir_inst_lifting.DEBUG_LEVEL" 2;
 
 val _ = new_theory "swap";
 
-val _ = lift_da_and_store "swap" "swap.da" ((Arbnum.fromInt 0), (Arbnum.fromInt 0x1000000));
+val _ = lift_da_and_store "swap" "swap.da" da_riscv ((Arbnum.fromInt 0), (Arbnum.fromInt 0x1000000));
 
 val _ = export_theory ();
diff --git a/examples/tutorial/2-lift/bir_prog_add_regScript.sml b/examples/tutorial/2-lift/bir_prog_add_regScript.sml
@@ -10,6 +10,7 @@ val _ = new_theory "bir_prog_add_reg";
 
 val _ = lift_da_and_store "add_reg"
                           "../1-code/src/add_reg.da"
+                          da_arm8
                           ((Arbnum.fromInt 0), (Arbnum.fromInt 0x1000000));
 
 val _ = export_theory();
diff --git a/src/tools/lifter/bir_lifter_interfaceLib.sml b/src/tools/lifter/bir_lifter_interfaceLib.sml
@@ -35,22 +35,33 @@ open gcc_supportLib;
 
 in
 
+fun prog_gen_of_isa isa =
+  case isa of
+    da_arm8 => bmil_arm8.bir_lift_prog_gen
+  | da_riscv => bmil_riscv.bir_lift_prog_gen
+
+fun string_of_isa isa =
+  case isa of
+    da_arm8 => "arm8"
+  | da_riscv  => "riscv"
+
 (* Debug values:
   val da_name = "../1-code/src/add_reg.da"
   val prog_name = "add_reg"
+  val isa = da_arm8
   val prog_interval = ((Arbnum.fromInt 0), (Arbnum.fromInt 0x1000000))
 *)
-fun lift_da_and_store prog_name da_name da_isa prog_interval =
+fun lift_da_and_store prog_name da_name isa prog_interval =
   let
     val _ = print_with_style_ [Bold, Underline] ("Lifting "^da_name^"\n");
 
     val (region_map, aes_sections) = read_disassembly_file_regions da_name
 
-    val (thm_riscv, errors) = bmil_riscv.bir_lift_prog_gen
+    val (thm_x, errors) = (prog_gen_of_isa isa)
 			       prog_interval
 			       aes_sections
 
-    val (lift_app_1_tm, bir_prog_tm) = (dest_comb o concl) thm_riscv;
+    val (lift_app_1_tm, bir_prog_tm) = (dest_comb o concl) thm_x;
     val (_, bir_progbin_tm) = dest_comb lift_app_1_tm;
 
     val _ = print "\n\n";
@@ -62,9 +73,9 @@ fun lift_da_and_store prog_name da_name da_isa prog_interval =
     val bir_x_progbin_def = Define `^bir_x_progbin_var = ^bir_progbin_tm`;
 
     (* now save the lifter theorem using the definitions *)
-    val bir_x_riscv_lift_THM = save_thm ("bir_"^prog_name^"_riscv_lift_THM",
+    val bir_x_lift_THM = save_thm ("bir_"^prog_name^"_"^(string_of_isa isa)^"_lift_THM",
 	   REWRITE_RULE [GSYM bir_x_prog_def,
-			 GSYM bir_x_progbin_def] thm_riscv);
+			 GSYM bir_x_progbin_def] thm_x);
   in
     ()
   end;