Fix experiment

kth-step · Nov 10, 2024 · 4e93e04 · 4e93e04
1 parent 5c1ab42
commit 4e93e04
Show file tree

Hide file tree

Showing 5 changed files with 19 additions and 2 deletions.
diff --git a/examples/arm_cm0/balrob/balrob_endsScript.sml b/examples/arm_cm0/balrob/balrob_endsScript.sml
@@ -26,6 +26,11 @@ val locs =
 val symb_exec_thm = birs_summary birs_prog_config [] reqs locs;
 val _ = save_thm("balrob_summary_" ^ entry_name ^ "_thm", symb_exec_thm);
 
+
 (* ------------------------------------ *)
 
+val _ = print "\n";
+val _ = Profile.print_profile_results (Profile.results ());
+
+
 val _ = export_theory ();
diff --git a/examples/arm_cm0/balrob/balrob_faddScript.sml b/examples/arm_cm0/balrob/balrob_faddScript.sml
@@ -3,6 +3,7 @@ open HolKernel Parse boolLib bossLib;
 open balrob_supportLib;
 
 open balrob_endsTheory;
+open balrob_fmulTheory; (* TODO: remove this line later *)
 
 val _ = new_theory "balrob_fadd";
 

diff --git a/examples/arm_cm0/balrob/balrob_fdivScript.sml b/examples/arm_cm0/balrob/balrob_fdivScript.sml
@@ -111,7 +111,12 @@ val locs =
   ( 0x100005A4,
    [0x10000678]);
 
-val symb_exec_thm = birs_summary birs_prog_config
+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))
+  (gen_const_load_32_32_cheat_thms [
+    (0x100007bc, 0x100007c8),
+    (0x100007c4, 0x10000808)])
+  birs_prog_config
   [balrob_summary___clzsi2_thm,
    balrob_summary___aeabi_fdiv_loop_thm,
    balrob_summary___aeabi_fdiv_c1_thm,

diff --git a/examples/arm_cm0/balrob/balrob_fmulScript.sml b/examples/arm_cm0/balrob/balrob_fmulScript.sml
@@ -3,8 +3,10 @@ open HolKernel Parse boolLib bossLib;
 open balrob_supportLib;
 
 open balrob_endsTheory;
+(*
 open balrob_fsubTheory; (* TODO: remove this line later *)
 open balrob_faddTheory; (* TODO: remove this line later *)
+*)
 
 val _ = new_theory "balrob_fmul";
 
@@ -99,7 +101,10 @@ val locs =
   ( 0x10000B44,
    [0x10000C12]);
 
-val symb_exec_thm = birs_summary birs_prog_config
+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))
+  (gen_const_load_32_32_cheat_thms [(0x10000DA0, 0x10000DA8)])
+  birs_prog_config
   [balrob_summary___clzsi2_thm,
    balrob_summary___aeabi_fmul_c1_thm,
    balrob_summary___aeabi_fmul_c2_thm,

diff --git a/examples/arm_cm0/balrob/balrob_fsubScript.sml b/examples/arm_cm0/balrob/balrob_fsubScript.sml
@@ -3,6 +3,7 @@ open HolKernel Parse boolLib bossLib;
 open balrob_supportLib;
 
 open balrob_endsTheory;
+open balrob_fmulTheory; (* TODO: remove this line later *)
 
 val _ = new_theory "balrob_fsub";