From fc8fa7a4819a46aeae576264ed03a1715ae1922b Mon Sep 17 00:00:00 2001 From: Andreas Lindner Date: Sat, 12 Oct 2024 17:47:36 +0200 Subject: [PATCH] Fixed example of merging, instantiating and transfer to BIR contract --- examples/arm_cm0/balrob/balrob_endsScript.sml | 83 ++++--------- .../balrob/balrob_ends_mergeScript.sml | 15 +-- .../arm_cm0/balrob/balrob_insttestScript.sml | 77 ++++++------ .../balrob/balrob_symb_transfScript.sml | 117 +++++++++++------- 4 files changed, 137 insertions(+), 155 deletions(-) diff --git a/examples/arm_cm0/balrob/balrob_endsScript.sml b/examples/arm_cm0/balrob/balrob_endsScript.sml index c9dea89bc..03792661a 100644 --- a/examples/arm_cm0/balrob/balrob_endsScript.sml +++ b/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 (); diff --git a/examples/arm_cm0/balrob/balrob_ends_mergeScript.sml b/examples/arm_cm0/balrob/balrob_ends_mergeScript.sml index be0d1a73b..34d3f154e 100644 --- a/examples/arm_cm0/balrob/balrob_ends_mergeScript.sml +++ b/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 (); diff --git a/examples/arm_cm0/balrob/balrob_insttestScript.sml b/examples/arm_cm0/balrob/balrob_insttestScript.sml index 8a67f9626..fb5ef4495 100644 --- a/examples/arm_cm0/balrob/balrob_insttestScript.sml +++ b/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 (); diff --git a/examples/arm_cm0/balrob/balrob_symb_transfScript.sml b/examples/arm_cm0/balrob/balrob_symb_transfScript.sml index 8946318b4..5881863a2 100644 --- a/examples/arm_cm0/balrob/balrob_symb_transfScript.sml +++ b/examples/arm_cm0/balrob/balrob_symb_transfScript.sml @@ -6,73 +6,104 @@ open bir_tsTheory bir_bool_expTheory bir_programTheory; open bir_immSyntax; open bir_symbLib; +open birs_instantiationLib; +open birs_utilsLib; open balrobLib; open balrob_endsTheory; val _ = new_theory "balrob_symb_transf"; -val balrob_prog_vars_thm = balrobTheory.balrob_prog_vars_thm; -val balrob_prog_vars_list_def = balrobTheory.balrob_prog_vars_list_def; + + +val balrob_exec_thm = balrob_clzsi2_symb_exec_thm; +(*val bsysprecond_thm = balrob_clzsi2_bsysprecond_thm;*) +val birs_env_thm = balrob_clzsi2_birs_env_thm; +(**) +val bprog_envtyl_tm = (fst o dest_eq o concl) balrob_birenvtyl_def; +(* TODO: the following can be extracted from the theorems above *) +val init_addr_tm = ``0x100013b4w : word32``; +val end_addr_tm = ``0x100013dcw : word32``; +val balrob_pre = ``BExp_BinPred BIExp_LessOrEqual + (BExp_Den (BVar "countw" (BType_Imm Bit64))) + (BExp_Const (Imm64 0xFFFFFEBw))``; + +(* TODO: move this after the symbolic execution, and infer the minimum and the maximum *) +val (countw_min, countw_max) = (21, 21); + +(* -------------- *) +(* BSPEC contract *) +(* -------------- *) +val bir_countw_bvar_tm = ``BExp_Den (BVar "countw" (BType_Imm Bit64))``; +val bir_countw_hvar_tm = ``BExp_Const (Imm64 pre_countw)``; +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); +val bir_hvar_cond = bslSyntax.beq (bir_countw_bvar_tm, bir_countw_hvar_tm); + +val bspec_balrob_pre_tm = + ``BExp_BinExp BIExp_And + ^balrob_pre + ^bir_hvar_cond``; + +Definition bspec_balrob_pre_def: + bspec_balrob_pre (pre_countw:word64) : bir_exp_t = + ^bspec_balrob_pre_tm +End + +(* TODO: make this an interval statement *) +val bspec_balrob_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_post_def: + bspec_balrob_post (pre_countw:word64) : bir_exp_t = + ^bspec_balrob_post_tm +End + (* --------------------- *) (* Auxiliary definitions *) (* --------------------- *) +val bspec_pre_tm = (lhs o snd o strip_forall o concl) bspec_balrob_pre_def; +val bspec_post_tm = (lhs o snd o strip_forall o concl) bspec_balrob_post_def; -val init_addr_tm = (snd o dest_eq o concl) balrob_clzsi2_init_addr_def; -val end_addr_tm = (snd o dest_eq o concl) balrob_clzsi2_end_addr_def; - -val bspec_pre_tm = (lhs o snd o strip_forall o concl) bspec_balrob_clzsi2_pre_def; -val bspec_post_tm = (lhs o snd o strip_forall o concl) bspec_balrob_clzsi2_post_def; - +(* ------------------------------- *) +(* make theorem for mk_bsysprecond fix *) +(* ------------------------------- *) +fun create_mk_bsysprecond_thm t = + (computeLib.RESTR_EVAL_CONV [``birs_eval_exp``] THENC birs_stepLib.birs_eval_exp_CONV) + (``mk_bsysprecond ^t ^bprog_envtyl_tm``); +val mk_bsysprecond_pcond_thm = create_mk_bsysprecond_thm bspec_pre_tm; +val birs_pcond_tm = (snd o dest_eq o concl) mk_bsysprecond_pcond_thm; +val bir_hvar_cond_symb = (snd o dest_eq o concl o create_mk_bsysprecond_thm) bir_hvar_cond; (* ------------------------------- *) (* prepare for BIR property transfer *) (* ------------------------------- *) -val bprog_envtyl_tm = (fst o dest_eq o concl) balrob_birenvtyl_def; -fun mk_bsysprecond_thm bspec_pre_tm bprog_envtyl_tm = - (computeLib.RESTR_EVAL_CONV [``birs_eval_exp``] THENC birs_stepLib.birs_eval_exp_CONV) - (``mk_bsysprecond ^bspec_pre_tm ^bprog_envtyl_tm``); - -(* TODO: need to instantiate "syp_gen" to true and remove that conjunct in the initial state before being able to transfer *) -(* TODO: need to bring hol variables for countw and SP into the initial pathcondition before this step *) -val pre_pcond_new_exp = (snd o dest_eq o snd o strip_forall o concl) bspec_balrob_clzsi2_pre_def; -val bsysprecond_thm = mk_bsysprecond_thm pre_pcond_new_exp bprog_envtyl_tm; -val bsysprecond_thm = REWRITE_RULE [GSYM bspec_balrob_clzsi2_pre_def] bsysprecond_thm; - -val pre_pcond_new = (snd o dest_eq o concl) bsysprecond_thm; -val holvar_eq_exp = List.nth(birs_utilsLib.dest_band pre_pcond_new, 1); -(* -val _ = print_term holvar_eq_exp; -val _ = print "\n"; -*) -val specd_symb_analysis_thm = birs_instantiationLib.birs_sound_symb_inst_RULE [(``BVar "syp_gen" (BType_Imm Bit1)``, holvar_eq_exp)] balrob_clzsi2_symb_analysis_thm; -val pcond_symb_analysis_thm = birs_utilsLib.birs_sys_pcond_RULE pre_pcond_new specd_symb_analysis_thm; -val fixed_symb_analysis_thm = REWRITE_RULE [GSYM bsysprecond_thm] pcond_symb_analysis_thm; - -(* -val _ = print_thm bsysprecond_thm; -val _ = print "\n"; -val _ = print "\n"; -val _ = print_thm fixed_symb_analysis_thm; -val _ = print "\n"; -val _ = print "\n"; -val _ = raise Fail ""; -*) +val specd_symb_analysis_thm = birs_sound_symb_inst_RULE [(``BVar "syp_gen" (BType_Imm Bit1)``, bir_hvar_cond_symb)] balrob_exec_thm; +val pcond_symb_analysis_thm = birs_sys_pcond_RULE birs_pcond_tm specd_symb_analysis_thm; +val fixed_symb_analysis_thm = CONV_RULE (birs_sys_CONV (REWRITE_CONV [GSYM mk_bsysprecond_pcond_thm, GSYM birs_env_thm])) pcond_symb_analysis_thm; (* ------------------------------- *) (* BIR property transfer *) (* ------------------------------- *) (*val _ = bir_smtLib.bir_smt_set_trace false 1;*) +val balrob_prog_vars_thm = balrobTheory.balrob_prog_vars_thm; +val balrob_prog_vars_list_def = balrobTheory.balrob_prog_vars_list_def; + (* val _ = HOL_Interactive.toggle_quietdec(); val bir_prog_def = bir_balrob_prog_def; val birenvtyl_def = balrob_birenvtyl_def; -val bspec_pre_def = bspec_balrob_clzsi2_pre_def; -val bspec_post_def = bspec_balrob_clzsi2_post_def; +val bspec_pre_def = bspec_balrob_pre_def; +val bspec_post_def = bspec_balrob_post_def; val prog_vars_list_def = balrob_prog_vars_list_def; val symb_analysis_thm = fixed_symb_analysis_thm; -(*val bsysprecond_thm = balrob_clzsi2_bsysprecond_thm;*) +val bsysprecond_thm = mk_bsysprecond_pcond_thm; val prog_vars_thm = balrob_prog_vars_thm; val _ = HOL_Interactive.toggle_quietdec(); *) @@ -80,8 +111,8 @@ val _ = HOL_Interactive.toggle_quietdec(); val bspec_cont_thm = bir_symb_transfer init_addr_tm end_addr_tm bspec_pre_tm bspec_post_tm bir_balrob_prog_def balrob_birenvtyl_def - bspec_balrob_clzsi2_pre_def bspec_balrob_clzsi2_post_def balrob_prog_vars_list_def - fixed_symb_analysis_thm bsysprecond_thm balrob_prog_vars_thm; + bspec_balrob_pre_def bspec_balrob_post_def balrob_prog_vars_list_def + fixed_symb_analysis_thm mk_bsysprecond_pcond_thm balrob_prog_vars_thm; Theorem bspec_cont_balrob: bir_cont bir_balrob_prog bir_exp_true