diff options
| author | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-04-12 09:14:52 +0200 |
|---|---|---|
| committer | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-04-12 09:14:52 +0200 |
| commit | 69220f5c7fa9b455899f48e2628e2ed190316f91 (patch) | |
| tree | a90ad954e845ab728f5c7ccb2883c3efb1cceaa4 | |
| parent | bba585d012eaf30609eac296c3fe78697fc7dda8 (diff) | |
| download | compcert-kvx-69220f5c7fa9b455899f48e2628e2ed190316f91.tar.gz compcert-kvx-69220f5c7fa9b455899f48e2628e2ed190316f91.zip | |
Add exec_MBjumptable to PseudoAsmblock.cfi_step
+ Proof of corresponding case in exit_step_simulation
| -rw-r--r-- | mppa_k1c/lib/PseudoAsmblock.v | 8 | ||||
| -rw-r--r-- | mppa_k1c/lib/PseudoAsmblockproof.v | 19 |
2 files changed, 26 insertions, 1 deletions
diff --git a/mppa_k1c/lib/PseudoAsmblock.v b/mppa_k1c/lib/PseudoAsmblock.v index 3686ac68..b7669529 100644 --- a/mppa_k1c/lib/PseudoAsmblock.v +++ b/mppa_k1c/lib/PseudoAsmblock.v @@ -181,7 +181,13 @@ Inductive cfi_step (f: function): control_flow_inst -> regset -> mem -> trace -> | exec_MBcond_false cond args lbl rs m rs': eval_condition cond (to_Machrs rs)##args m = Some false -> rs' = set_from_Machrs (undef_regs (destroyed_by_cond cond) rs) rs -> - cfi_step f (MBcond cond args lbl) rs m E0 rs' m. + cfi_step f (MBcond cond args lbl) rs m E0 rs' m + | exec_MBjumptable arg tbl rs m index lbl pc rs': + to_Machrs rs arg = Vint index -> + list_nth_z tbl (Int.unsigned index) = Some lbl -> + goto_label f lbl rs = Some pc -> + rs' = set_from_Machrs (undef_regs destroyed_by_jumptable rs) rs -> + cfi_step f (MBjumptable arg tbl) rs m E0 (rs'#PC <- pc) m. (* TODO à finir... diff --git a/mppa_k1c/lib/PseudoAsmblockproof.v b/mppa_k1c/lib/PseudoAsmblockproof.v index 093ef1a4..cdb46202 100644 --- a/mppa_k1c/lib/PseudoAsmblockproof.v +++ b/mppa_k1c/lib/PseudoAsmblockproof.v @@ -874,6 +874,25 @@ Proof. -- erewrite agree_mregs_list in H15; eauto. -- trivial. * repeat econstructor; eauto. erewrite agree_sp; eauto. + (* MBjumptable *) + + simplify_someHyps. intros. + assert ((rs # PC <- (Vptr fb ofs)) PC = Vptr fb ofs). { + rewrite Pregmap.gss. reflexivity. + } + eassert (exists pc, goto_label next tf lbl rs # PC <- (Vptr fb ofs) = Some pc + /\ transl_code_at_pc fb f tf c' pc) as (pc & GOTO_LABEL & _). { + eapply find_label_goto_label; eauto. + } + eexists. eexists. split. + * repeat econstructor; eauto. + rewrite <- H14. + symmetry. eapply agree_mregs. eapply agree_set_other; eauto. + * repeat econstructor; eauto. + (* copy paste from MBgoto *) + -- simplify_regmap. + exploit find_label_goto_label; eauto. intros (pc' & GOTO_LABEL' & TRANSL). + assert(pc' = pc). { congruence. } subst. eauto. + -- simplify_regmap. erewrite agree_sp; eauto. + (* MBreturn *) try_simplify_someHyps. eexists. eexists. split. |