Simplify

kth-step · Oct 14, 2024 · e8b4e92 · e8b4e92
1 parent a3dec14
commit e8b4e92
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 9 deletions.
diff --git a/examples/arm_cm0/balrob/balrob_endsScript.sml b/examples/arm_cm0/balrob/balrob_endsScript.sml
@@ -4,12 +4,13 @@ open balrob_supportLib;
 
 val _ = new_theory "balrob_ends";
 
-(* __clzsi2 *)
-val reqs = (0,21);
-val init_addr = ``0x100013b4w : word32``;
-val end_addr = ``0x100013dcw : word32``;
+val entry_name = "__clzsi2";
+val reqs = get_fun_usage entry_name;
+val locs =
+  (0x100013b4,
+   0x100013dc);
 
-val symb_exec_thm = birs_summary birs_prog_config reqs (init_addr, end_addr);
+val symb_exec_thm = birs_summary birs_prog_config reqs locs;
 
 Theorem balrob_clzsi2_symb_exec_thm = symb_exec_thm
 

diff --git a/examples/arm_cm0/balrob/balrob_insttestScript.sml b/examples/arm_cm0/balrob/balrob_insttestScript.sml
@@ -12,10 +12,11 @@ val _ = new_theory "balrob_insttest";
 
 (* instantiation test *)
 val reqs = (0,63);
-val init_addr = ``0x100012d6w : word32``;
-val end_addr = ``0x100013b4w : word32``;
+val locs =
+  (0x100012d6,
+   0x100013b4);
 
-val symb_exec_thm = birs_summary birs_prog_config reqs (init_addr, end_addr);
+val symb_exec_thm = birs_summary birs_prog_config reqs locs;
 
 Theorem balrob_insttest_symb_exec_thm = symb_exec_thm
 

diff --git a/examples/arm_cm0/balrob/balrob_supportLib.sml b/examples/arm_cm0/balrob/balrob_supportLib.sml
@@ -191,8 +191,9 @@ val birs_prog_config = ((fst o dest_eq o concl) balrobLib.bir_balrob_prog_def, b
 
 local
     open bir_immSyntax;
+    fun mk_word_addr v = wordsSyntax.mk_wordii(v, 32);
     fun mk_bir_lbl x = ``bir_block_pc (BL_Address ^(gen_mk_Imm x))``;
-    val bir_lbl_from_addr = snd o dest_eq o concl o EVAL o mk_bir_lbl;
+    val bir_lbl_from_addr = snd o dest_eq o concl o EVAL o mk_bir_lbl o mk_word_addr;
 in
  fun birs_basic_init_state (bprog_tm, prog_birenvtyl_def) reqs init_addr =
   let