Reorganize more

examples/arm_cm0/balrob/balrob_endsScript.sml

@@ -7,9 +7,9 @@ val _ = new_theory "balrob_ends";
 (* __clzsi2 *)
 val reqs = (0,21);
 val init_addr = ``0x100013b4w : word32``;
-val end_addrs = [``0x100013dcw : word32``];
+val end_addr = ``0x100013dcw : word32``;
 
-val symb_exec_thm = birs_summary_execute birs_prog_config reqs (init_addr, end_addrs);
+val symb_exec_thm = birs_summary birs_prog_config reqs (init_addr, end_addr);
 
 Theorem balrob_clzsi2_symb_exec_thm = symb_exec_thm
 

examples/arm_cm0/balrob/balrob_insttestScript.sml

@@ -13,33 +13,19 @@ val _ = new_theory "balrob_insttest";
 (* instantiation test *)
 val reqs = (0,63);
 val init_addr = ``0x100012d6w : word32``;
-val end_addrs = [``0x100013b4w : word32``];
+val end_addr = ``0x100013b4w : word32``;
 
-val symb_exec_thm = birs_summary_execute birs_prog_config reqs (init_addr, end_addrs);
+val symb_exec_thm = birs_summary birs_prog_config reqs (init_addr, end_addr);
 
 Theorem balrob_insttest_symb_exec_thm = symb_exec_thm
 
 
-(* now try to instantiate *)
-val _ = print "prepare generic SEQ thm\n";
-val bprog_tm = (fst o dest_eq o concl) balrobLib.bir_balrob_prog_def;
-val birs_rule_SEQ_thm = birs_rule_SEQ_prog_fun bprog_tm;
-
+(* now instantiate *)
 val A_thm = balrob_insttest_symb_exec_thm;
 val B_thm = balrob_clzsi2_symb_exec_thm;
-(*
-val _ = print_thm A_thm;
-val _ = print_thm B_thm;
-*)
-
-val _ = print "start instantiation\n";
-val cont_thm = birs_sound_inst_SEQ_RULE birs_rule_SEQ_thm bir_symbLib.pcond_gen_symb A_thm B_thm;
-val cont_thm2 = birs_intervalLib.birs_intervals_Pi_RULE "countw" cont_thm;
-
-Theorem balrob_insttest_symb_inst_thm = cont_thm2
+val inst_thm = birs_basic_instantiate birs_prog_config A_thm B_thm;
 
-Theorem balrob_insttest_symb_more_thm = 
-  birs_execute_Pi_first_further birs_prog_config [``0x100012e8w : word32``, ``0x100012f6w : word32``] cont_thm2
+Theorem balrob_insttest_symb_inst_thm = inst_thm
 
 val _ = export_theory ();
 

examples/arm_cm0/balrob/balrob_intervaltestScript.sml

@@ -0,0 +1,21 @@
+open HolKernel Parse boolLib bossLib;
+
+open birs_intervalLib;
+
+open balrob_endsTheory;
+
+val _ = new_theory "balrob_intervaltest";
+
+(* ------------------- *)
+(* introduce interval  *)
+(* ------------------- *)
+(*
+val interval_thm = birs_intervals_Pi_unify_RULE "countw" balrob_clzsi2_symb_exec_thm;
+*)
+(*
+val interval_thm = birs_intervals_Pi_RULE "countw" balrob_clzsi2_symb_exec_thm;
+
+Theorem balrob_clzsi2_symb_interval_thm = interval_thm
+*)
+
+val _ = export_theory ();

examples/arm_cm0/balrob/balrob_supportLib.sml

@@ -8,8 +8,6 @@ local
   open birsSyntax;
 
   open birs_utilsLib;
-  open birs_mergeLib;
-  open birs_intervalLib;
 
   (* error handling *)
   val libname = "balrob_supportLib"
@@ -191,58 +189,67 @@ val configs          = [("balrob",
 
 val birs_prog_config = ((fst o dest_eq o concl) balrobLib.bir_balrob_prog_def, balrobLib.balrob_birenvtyl_def);
 
-(* TODO: add previous summaries and indirectjump theorems as argument here (probably good as function), and the proper handling in the buildtree function *)
-fun birs_summary_execute (bprog_tm, prog_birenvtyl_def) reqs (init_addr, end_addrs) =
-  let
-    open bir_symbLib;
+local
     open bir_immSyntax;
-
-    val precond = bslSyntax.bandl (pred_conjs reqs);
-
     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;
+in
+ fun birs_basic_init_state (bprog_tm, prog_birenvtyl_def) reqs init_addr =
+  let
     val init_lbl = bir_lbl_from_addr init_addr;
-    val end_lbls = List.map bir_lbl_from_addr end_addrs;
-
+    val precond = bslSyntax.bandl (pred_conjs reqs);
     (* TODO: remove birs_env_thm and bsysprecond_thm make it separate things (only needed for transfer) *)
       (* they shouldn't come out of the symbolic exec function, it is only needed for the transfer, and it shouldn't be a problem to compute it repeatedly, see the function gen_senv_GEN_thm below *)
-    val (birs_state_init, _, _) =
-      bir_symb_analysis_init_gen (SOME pcond_gen_symb) init_lbl precond prog_birenvtyl_def;
-    val symb_exec_thm =
-      bir_symb_analysis bprog_tm end_lbls birs_state_init;
-
-    (* TODO: should merge Pi states here, also handle intervals correctly, in symbolic execution driver (together with the indirectjump handling and previous summaries) and also before merging *)
-    val interval_thm = birs_intervals_Pi_RULE "countw" symb_exec_thm;
-    val merged_thm = birs_Pi_merge_RULE interval_thm;
+    val (init_state, _, _) =
+      bir_symbLib.bir_symb_analysis_init_gen (SOME bir_symbLib.pcond_gen_symb) init_lbl precond prog_birenvtyl_def;
   in
-    merged_thm
+    init_state
   end;
 
-
-
-fun birs_execute_Pi_first_further (bprog_tm, _) end_addrs thm =
+ fun birs_basic_execute (bprog_tm, prog_birenvtyl_def) end_addrs init_state =
   let
-    open bir_immSyntax;
     open birs_intervalLib;
-    open birs_composeLib;
-
-    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 end_lbls = List.map bir_lbl_from_addr end_addrs;
+    val symb_exec_thm =
+      bir_symbLib.bir_symb_analysis bprog_tm end_lbls init_state;
+    val interval_thm = birs_intervals_Pi_unify_RULE "countw" symb_exec_thm;
+  in
+    interval_thm
+  end;
+end
 
-    val birs_state_tm = (get_birs_Pi_first o concl) thm;
+val birs_basic_merge =
+  let
+    open birs_mergeLib;
+    open birs_intervalLib;
+  in
+    (birs_Pi_merge_RULE o birs_intervals_Pi_bounds_RULE "countw")
+  end;
 
-    (* execute further *)
+fun birs_basic_instantiate (bprog_tm, prog_birenvtyl_def) =
+  let
+    open birs_composeLib;
+    open birs_instantiationLib;
+    open birs_intervalLib;
     val birs_rule_SEQ_thm = birs_rule_SEQ_prog_fun bprog_tm;
-    val symb_more_thm =
-      bir_symbLib.bir_symb_analysis bprog_tm end_lbls (birs_state_tm);
-    (* cleanup *)
-    val symb_more_interval_thm = birs_intervals_Pi_RULE "countw" symb_more_thm;
-    (* SEQ *)
-    val symb_more_compose_thm = birs_rule_SEQ_fun birs_rule_SEQ_thm thm symb_more_interval_thm;
+    val inst_SEQ_fun = birs_sound_inst_SEQ_RULE birs_rule_SEQ_thm bir_symbLib.pcond_gen_symb;
   in
-    symb_more_compose_thm
+    fn A_thm => (birs_intervals_Pi_unify_RULE "countw" o inst_SEQ_fun A_thm)
+  end;
+
+(* ========================================================================================== *)
+
+  (* TODO: add previous summaries and indirectjump theorems as argument here, and the proper handling in the buildtree function (probably good as function argument) *)
+     (* handle intervals correctly: in symbolic execution driver (together with the indirectjump handling and previous summaries) and also before merging *)
+  fun birs_summary (bprog_tm, prog_birenvtyl_def) reqs (init_addr, end_addr) =
+    let
+      val init_state = birs_basic_init_state (bprog_tm, prog_birenvtyl_def) reqs init_addr;
+      val symb_exec_thm = birs_basic_execute (bprog_tm, prog_birenvtyl_def) [end_addr] init_state;
+
+      val merged_thm = birs_basic_merge symb_exec_thm;
+    in
+      merged_thm
   end;
 
   fun gen_senv_GEN_thm prog_birenvtyl_def =