Fixed example of merging, instantiating and transfer to BIR contract

examples/arm_cm0/balrob/balrob_endsScript.sml

@@ -4,6 +4,8 @@ open bir_programSyntax bir_program_labelsTheory;
 open bir_immTheory bir_valuesTheory bir_expTheory bir_exp_immTheory;
 open bir_tsTheory bir_bool_expTheory bir_programTheory;
 
+open bir_immSyntax;
+
 open bir_predLib;
 
 open bir_symbLib;
@@ -14,85 +16,50 @@ val _ = new_theory "balrob_ends";
 
 (* __clzsi2 *)
 
+(* commonBalrobScriptLib.sml *)
+val countw_space_req = 21;
+
 (* ------------------ *)
 (* Program boundaries *)
 (* ------------------ *)
-
-Definition balrob_clzsi2_init_addr_def:
- balrob_clzsi2_init_addr : word32 = 0x100013b4w
-End
-
-Definition balrob_clzsi2_end_addr_def:
- balrob_clzsi2_end_addr : word32 = 0x100013dcw
-End
+val clzsi2_init_addr = ``0x100013b4w : word32``;
+val clzsi2_end_addrs = [``0x100013dcw : word32``];
 
 (* -------------- *)
-(* BSPEC contract *)
+(* precondition   *)
 (* -------------- *)
-val bir_countw_hvar_tm = ``BExp_Const (Imm64 pre_countw)``;
 val bir_countw_bvar_tm = ``BExp_Den (BVar "countw" (BType_Imm Bit64))``;
 fun mk_countw_const v = ``BExp_Const (Imm64 ^(wordsSyntax.mk_wordii(v, 64)))``;
 fun mk_countw_plus tm v = bslSyntax.bplus (tm, mk_countw_const v);
 
-(* commonBalrobScriptLib.sml *)
-val countw_space_req = 21;
-val symbexec_init_tm = (* TODO: need SP here too *)
+val clzsi2_pre = (* TODO: need SP here too *)
   ``BExp_BinPred BIExp_LessOrEqual
        ^(bir_countw_bvar_tm)
        ^(mk_countw_const (0x10000000 - countw_space_req))``;
 
-Definition bspec_balrob_clzsi2_init_def:
-  bspec_balrob_clzsi2_init : bir_exp_t =
-   ^symbexec_init_tm
-End
-
-val bspec_balrob_clzsi2_pre_tm = bslSyntax.bandl [
-  bslSyntax.beq (bir_countw_bvar_tm, bir_countw_hvar_tm),
-  symbexec_init_tm
-];
-
-Definition bspec_balrob_clzsi2_pre_def:
-  bspec_balrob_clzsi2_pre (pre_countw:word64) : bir_exp_t =
-   ^bspec_balrob_clzsi2_pre_tm
-End
-
-(* TODO: move this after the symbolic execution and infer the minimum and the maximum *)
-(* TODO: make this an interval statement *)
-val (countw_min, countw_max) = (21, 21);
-val bspec_balrob_clzsi2_post_tm = bslSyntax.bandl [
- ``BExp_BinPred BIExp_LessOrEqual
-       ^(mk_countw_plus bir_countw_hvar_tm countw_min)
-       ^(bir_countw_bvar_tm)``,
- ``BExp_BinPred BIExp_LessOrEqual
-       ^(bir_countw_bvar_tm)
-       ^(mk_countw_plus bir_countw_hvar_tm countw_max)``
-];
-
-Definition bspec_balrob_clzsi2_post_def:
- bspec_balrob_clzsi2_post (pre_countw:word64) : bir_exp_t =
-  ^bspec_balrob_clzsi2_post_tm
-End
 
 (* --------------------------- *)
-(* Symbolic analysis execution *)
+(* Symbolic execution          *)
 (* --------------------------- *)
+val bprog_tm = (fst o dest_eq o concl) bir_balrob_prog_def;
+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 init_lbl = bir_lbl_from_addr clzsi2_init_addr;
+val end_lbls = List.map bir_lbl_from_addr clzsi2_end_addrs;
 
-val pcond_symb_o = SOME ``BVar "syp_gen" (BType_Imm Bit1)``;
-val (bsysprecond_thm, symb_analysis_thm) =
- bir_symb_analysis_thm_gen
-  pcond_symb_o
-  bir_balrob_prog_def
-  balrob_clzsi2_init_addr_def [balrob_clzsi2_end_addr_def]
-  bspec_balrob_clzsi2_init_def balrob_birenvtyl_def;
+val (birs_state_init, birs_env_thm, bsysprecond_thm) =
+  bir_symb_analysis_init_gen (SOME pcond_gen_symb) init_lbl clzsi2_pre balrob_birenvtyl_def;
+val symb_exec_thm =
+  bir_symb_analysis bprog_tm end_lbls birs_state_init;
 
-val _ = show_tags := true;
+(* TODO: should merge Pi states here *)
+val symb_exec_merged_thm = symb_exec_thm;
 
-val _ = Portable.pprint Tag.pp_tag (tag bsysprecond_thm);
+Theorem balrob_clzsi2_symb_exec_thm = symb_exec_merged_thm
 
+(* only need the following two theorems for property transfer,
+    then also need to instantiate pcond_gen_symb with the hol free variable constant conditions *)
 Theorem balrob_clzsi2_bsysprecond_thm = bsysprecond_thm
-
-val _ = Portable.pprint Tag.pp_tag (tag symb_analysis_thm);
-
-Theorem balrob_clzsi2_symb_analysis_thm = symb_analysis_thm
+Theorem balrob_clzsi2_birs_env_thm = birs_env_thm
 
 val _ = export_theory ();

examples/arm_cm0/balrob/balrob_ends_mergeScript.sml

@@ -7,17 +7,15 @@ open balrob_endsTheory;
 
 val _ = new_theory "balrob_ends_merge";
 
-val _ = show_tags := true;
-val _ = Portable.pprint Tag.pp_tag (tag balrob_clzsi2_symb_analysis_thm);
-val _ = print_thm balrob_clzsi2_symb_analysis_thm;
+val _ = print_thm balrob_clzsi2_symb_exec_thm;
 val _ = print "\n\n";
 
 (* --------------------------- *)
 (* merging     *)
 (* --------------------------- *)
 val _ = print "starting merging\n\n\n";
-
-val merged_thm = birs_Pi_merge_RULE balrob_clzsi2_symb_analysis_thm;
+(* move this to balrob_endsScript when interval handling is in place (for countw and SP) *)
+val merged_thm = birs_Pi_merge_RULE balrob_clzsi2_symb_exec_thm;
 
 (* get conjuncts as list *)
 (* TODO: this will not be true later when we include countw and stack pointer intervals in the path condition, need to "forward" them into the new path condition and merge them as part of the instantiation *)
@@ -28,12 +26,5 @@ val _ = if list_eq_contents term_id_eq pcond_sysl pcond_Pifl then () else
 
 Theorem balrob_clzsi2_symb_merged_thm = merged_thm
 
-val prepared_thm = merged_thm;
-
-val _ = Portable.pprint Tag.pp_tag (tag prepared_thm);
-val _ = print_thm prepared_thm;
-
-Theorem balrob_clzsi2_symb_prepared_thm = prepared_thm
-
 
 val _ = export_theory ();

examples/arm_cm0/balrob/balrob_insttestScript.sml

@@ -4,6 +4,8 @@ open bir_programSyntax bir_program_labelsTheory;
 open bir_immTheory bir_valuesTheory bir_expTheory bir_exp_immTheory;
 open bir_tsTheory bir_bool_expTheory bir_programTheory;
 
+open bir_immSyntax;
+
 open bir_predLib;
 
 open bir_symbLib;
@@ -18,79 +20,70 @@ open balrob_ends_mergeTheory;
 val _ = new_theory "balrob_insttest";
 
 (* instantiation test *)
+(* commonBalrobScriptLib.sml *)
+val countw_space_req = 63;
 
 (* ------------------ *)
 (* Program boundaries *)
 (* ------------------ *)
-
-Definition balrob_insttest_init_addr_def:
- balrob_insttest_init_addr : word32 = 0x100012d6w
-End
-
-Definition balrob_insttest_end_addr_def:
- balrob_insttest_end_addr : word32 = 0x100013b4w
-End
+val insttest_init_addr = ``0x100012d6w : word32``;
+val insttest_end_addrs = [``0x100013b4w : word32``];
 
 (* -------------- *)
-(* BSPEC contract *)
+(* precondition   *)
 (* -------------- *)
 val bir_countw_bvar_tm = ``BExp_Den (BVar "countw" (BType_Imm Bit64))``;
 fun mk_countw_const v = ``BExp_Const (Imm64 ^(wordsSyntax.mk_wordii(v, 64)))``;
 fun mk_countw_plus tm v = bslSyntax.bplus (tm, mk_countw_const v);
 
-(* commonBalrobScriptLib.sml *)
-val countw_space_req = 63;
-val bspec_balrob_insttest_pre_tm = 
+val insttest_pre = (* TODO: need SP here too *)
   ``BExp_BinPred BIExp_LessOrEqual
        ^(bir_countw_bvar_tm)
        ^(mk_countw_const (0x10000000 - countw_space_req))``;
 
-Definition bspec_balrob_insttest_pre_def:
-  bspec_balrob_insttest_pre (pre_countw:word64) : bir_exp_t =
-   ^bspec_balrob_insttest_pre_tm
-End
-
-
 (* --------------------------- *)
-(* Symbolic analysis execution *)
+(* Symbolic execution          *)
 (* --------------------------- *)
+val init_addr = insttest_init_addr;
+val end_addrs = insttest_end_addrs;
+val precond = insttest_pre;
+val birenvtyl_def = balrob_birenvtyl_def;
 
-val (bsysprecond_thm, symb_analysis_thm) =
- bir_symb_analysis_thm_gen
-  NONE
-  bir_balrob_prog_def
-  balrob_insttest_init_addr_def [balrob_insttest_end_addr_def]
-  bspec_balrob_insttest_pre_def balrob_birenvtyl_def;
-
-val _ = show_tags := true;
-
-val _ = Portable.pprint Tag.pp_tag (tag bsysprecond_thm);
+val bprog_tm = (fst o dest_eq o concl) bir_balrob_prog_def;
+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 init_lbl = bir_lbl_from_addr init_addr;
+val end_lbls = List.map bir_lbl_from_addr end_addrs;
 
-Theorem balrob_insttest_bsysprecond_thm = bsysprecond_thm
+val (birs_state_init, birs_env_thm, bsysprecond_thm) =
+  bir_symb_analysis_init_gen (SOME pcond_gen_symb) init_lbl precond birenvtyl_def;
+val symb_exec_thm =
+  bir_symb_analysis bprog_tm end_lbls birs_state_init;
 
-val _ = Portable.pprint Tag.pp_tag (tag symb_analysis_thm);
+Theorem balrob_insttest_symb_exec_thm = symb_exec_thm
 
-Theorem balrob_insttest_symb_analysis_thm = symb_analysis_thm
+(* ------------------------------ *)
 
 (*
 val _ = print_thm balrob_clzsi2_symb_merged_thm;
 val _ = raise Fail "";
 *)
-val birenvtyl_def = balrob_birenvtyl_def;
-val bprog_envtyl_tm = (fst o dest_eq o concl) birenvtyl_def;
-val birs_env_thm = (REWRITE_CONV [birenvtyl_def] THENC EVAL THENC REWRITE_CONV [GSYM birs_auxTheory.birs_gen_env_thm, GSYM birs_auxTheory.birs_gen_env_NULL_thm]) ``bir_senv_GEN_list ^bprog_envtyl_tm``;
 
 (* now try to instantiate *)
 val _ = print "prepare generic SEQ thm\n";
-val birs_rule_SEQ_thm = birs_rule_SEQ_prog_fun ((fst o dest_eq o concl) bir_balrob_prog_def);
-val bv_syp_gen = ``BVar "syp_gen" (BType_Imm Bit1)``;
-val A_thm = CONV_RULE (RAND_CONV (LAND_CONV (REWRITE_CONV [birs_env_thm]))) symb_analysis_thm;
-val B_thm = CONV_RULE (RAND_CONV (LAND_CONV (REWRITE_CONV [birs_env_thm]))) balrob_clzsi2_symb_merged_thm;
+val birs_rule_SEQ_thm = birs_rule_SEQ_prog_fun bprog_tm;
+val A_thm = balrob_insttest_symb_exec_thm;
+val B_thm = balrob_clzsi2_symb_merged_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 bv_syp_gen A_thm B_thm;
-val cont_thm_fixed = CONV_RULE (RAND_CONV (LAND_CONV (REWRITE_CONV [GSYM birs_env_thm]))) cont_thm;
+val cont_thm = birs_sound_inst_SEQ_RULE birs_rule_SEQ_thm pcond_gen_symb A_thm B_thm;
+
+Theorem balrob_insttest_symb_inst_thm = cont_thm
 
-Theorem balrob_insttest_symb_inst_thm = cont_thm_fixed
+(* now continue execution after that *)
 
 val _ = export_theory ();