now runs through within one hour

kth-step · Jan 12, 2025 · 71b8d7f · 71b8d7f
1 parent 27e82e6
commit 71b8d7f
Show file tree

Hide file tree

Showing 6 changed files with 16 additions and 16 deletions.
diff --git a/examples/arm_cm0/balrob/balrob_faddScript.sml b/examples/arm_cm0/balrob/balrob_faddScript.sml
@@ -49,7 +49,7 @@ val balrob_summary___aeabi_fadd_c3_thm = save_thm("balrob_summary_" ^ entry_name
 
 (* ------------------------------------ *)
 
-(*
+
 val entry_name = "__aeabi_fadd";
 val reqs = get_fun_usage entry_name;
 val locs =
@@ -64,7 +64,7 @@ val symb_exec_thm = birs_summary birs_prog_config
   reqs
   locs;
 val _ = save_thm("balrob_summary_" ^ entry_name ^ "_thm", symb_exec_thm);
-*)
+
 
 (* ------------------------------------ *)
 

diff --git a/examples/arm_cm0/balrob/balrob_fdivScript.sml b/examples/arm_cm0/balrob/balrob_fdivScript.sml
@@ -106,7 +106,7 @@ val balrob_summary___aeabi_fdiv_c7_thm = save_thm("balrob_summary_" ^ entry_name
 
 (* ------------------------------------ *)
 
-(*
+
 (* TODO: uses two jump table encoded in manually extracted cfg! *)
 (* TODO: loads constants from memory! *)
 val entry_name = "__aeabi_fdiv";
@@ -132,7 +132,7 @@ val symb_exec_thm = birs_summary_gen
   reqs
   locs;
 val _ = save_thm("balrob_summary_" ^ entry_name ^ "_thm", symb_exec_thm);
-*)
+
 
 (* ------------------------------------ *)
 

diff --git a/examples/arm_cm0/balrob/balrob_fmulScript.sml b/examples/arm_cm0/balrob/balrob_fmulScript.sml
@@ -94,7 +94,7 @@ val balrob_summary___aeabi_fmul_c8_thm = save_thm("balrob_summary_" ^ entry_name
 
 (* ------------------------------------ *)
 
-(*
+
 (* TODO: uses one jump table encoded in manually extracted cfg! used to take 3 times as much time as sub or div *)
 (* TODO: loads constants from memory! is the constant loading part of the lifting? better add some code to check this *)
 val entry_name = "__aeabi_fmul";
@@ -118,7 +118,7 @@ val symb_exec_thm = birs_summary_gen
   reqs
   locs;
 val _ = save_thm("balrob_summary_" ^ entry_name ^ "_thm", symb_exec_thm);
-*)
+
 
 (* ------------------------------------ *)
 

diff --git a/examples/arm_cm0/balrob/balrob_fsubScript.sml b/examples/arm_cm0/balrob/balrob_fsubScript.sml
@@ -104,7 +104,7 @@ val balrob_summary___aeabi_fsub_c8_thm = save_thm("balrob_summary_" ^ entry_name
 
 (* ------------------------------------ *)
 
-(*
+
 val entry_name = "__aeabi_fsub";
 val reqs = get_fun_usage entry_name;
 val locs =
@@ -124,7 +124,7 @@ val symb_exec_thm = birs_summary birs_prog_config
   reqs
   locs;
 val _ = save_thm("balrob_summary_" ^ entry_name ^ "_thm", symb_exec_thm);
-*)
+
 
 (* ------------------------------------ *)
 

diff --git a/examples/arm_cm0/balrob/balrob_ftopScript.sml b/examples/arm_cm0/balrob/balrob_ftopScript.sml
@@ -4,16 +4,16 @@ open balrob_supportLib;
 
 open balrob_endsTheory;
 open balrob_miscTheory;
+(*
 open balrob_fadd_fakeTheory;
 open balrob_fsub_fakeTheory;
 open balrob_fmul_fakeTheory;
 open balrob_fdiv_fakeTheory;
-(*
+*)
 open balrob_faddTheory;
 open balrob_fsubTheory;
 open balrob_fmulTheory;
 open balrob_fdivTheory;
-*)
 
 val _ = new_theory "balrob_ftop";
 

diff --git a/examples/arm_cm0/balrob/balrob_topScript.sml b/examples/arm_cm0/balrob/balrob_topScript.sml
@@ -4,10 +4,16 @@ open balrob_supportLib;
 
 open balrob_endsTheory;
 open balrob_miscTheory;
+(*
 open balrob_fadd_fakeTheory;
 open balrob_fsub_fakeTheory;
 open balrob_fmul_fakeTheory;
 open balrob_fdiv_fakeTheory;
+*)
+open balrob_faddTheory;
+open balrob_fsubTheory;
+open balrob_fmulTheory;
+open balrob_fdivTheory;
 open balrob_ftopTheory;
 
 val _ = new_theory "balrob_top";
@@ -24,12 +30,6 @@ val locs =
   ( 0x10001504,
    [0x100016e0]);
 
-(*
-val locs =
-  ( 0x10001504,
-   [0x1000151a]);
-*)
-
 val symb_exec_thm = birs_summary_gen
   (fn x => ((*print "\n\n"; print_term x; print "\n\n";*) birs_simpLib.birs_simp_ID_fun x))
   (const_load_32_32_cheat_thms_fromprog_range (0x100016e4, 0x10001a88))