From e46b3e49b2a34c27f5703327c884cf3bcd0c6a49 Mon Sep 17 00:00:00 2001 From: Pierre Goutagny Date: Thu, 10 Jun 2021 18:22:02 +0200 Subject: Complete `tunnel_step_correct` proof up to Ijumptable Excluding Icond --- backend/RTLTunnelingproof.v | 236 ++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 227 insertions(+), 9 deletions(-) (limited to 'backend') diff --git a/backend/RTLTunnelingproof.v b/backend/RTLTunnelingproof.v index c54667a4..53f8bbf7 100644 --- a/backend/RTLTunnelingproof.v +++ b/backend/RTLTunnelingproof.v @@ -344,6 +344,118 @@ Proof. apply H. apply IHargs. Qed. +Lemma instruction_type_preserved: + forall (f tf:function) (pc:node) (i ti:instruction) + (TF: tunnel_function f = OK tf) + (FATPC: (fn_code f) ! pc = Some i) + (NOTINOP: forall s, i <> Inop s) + (NOTICOND: forall cond args ifso ifnot info, i <> Icond cond args ifso ifnot info) + (TI: ti = tunnel_instr (branch_target f) i), + (fn_code tf) ! (branch_target f pc) = Some ti. +Proof. + intros. + assert ((fn_code tf) ! pc = Some (tunnel_instr (branch_target f) i)) as TFATPC. + rewrite (tunnel_function_unfold f tf pc); eauto. + rewrite FATPC; eauto. + exploit branch_target_bounds; eauto. + intro TB. inversion TB as [BT|s|cond args ifso ifnot info]; try (rewrite FATPC in H; congruence). +Qed. + +(* rq: utilisée pour `tunnel_step_correct` mais je ne comprends pas tout *) +(**) Lemma find_function_translated: + forall ros rs trs fd, + regs_lessdef rs trs -> + find_function ge ros rs = Some fd -> + exists tfd, tunnel_fundef fd = OK tfd /\ find_function tge ros trs = Some tfd. +Proof. + intros. destruct ros; simpl in *. + - (* reg *) + assert (E: trs # r = rs # r). + { exploit Genv.find_funct_inv. apply H0. intros (b & EQ). + generalize (H r) . rewrite EQ. intro LD. inv LD. auto. } + rewrite E. exploit functions_translated; eauto. + - (* ident *) + rewrite symbols_preserved. destruct (Genv.find_symbol ge i); inv H0. + exploit function_ptr_translated; eauto. + intros (tf & X1 & X2). exists tf; intuition. +Qed. + +Lemma list_forall2_lessdef_rs: + forall rs trs args, + regs_lessdef rs trs -> + list_forall2 Val.lessdef rs ## args trs ## args. +Proof. + intros rs trs args LD. + exploit (reglist_lessdef rs trs args). apply LD. + induction args; simpl; intros H; try constructor; inv H. + apply H3. apply IHargs. apply H5. +Qed. + +Lemma fn_stacksize_preserved: + forall f tf + (TF: tunnel_function f = OK tf), + fn_stacksize f = fn_stacksize tf. +Proof. + intros f tf. unfold tunnel_function. + destruct (check_included _ _); try congruence. + intro H. monadInv H. simpl. reflexivity. +Qed. + +Lemma regs_setres_lessdef: + forall res vres tvres rs trs, + regs_lessdef rs trs -> Val.lessdef vres tvres -> + regs_lessdef (regmap_setres res vres rs) (regmap_setres res tvres trs). +Proof. + induction res; intros; simpl; try auto using set_reg_lessdef. +Qed. + +Lemma regmap_optget_lessdef: + forall or rs trs, + regs_lessdef rs trs -> Val.lessdef (regmap_optget or Vundef rs) (regmap_optget or Vundef trs). +Proof. + intros or rs trs RS. + induction or; simpl; auto using set_reg_lessdef. +Qed. + +Lemma tunnel_fundef_Internal: + forall (f:function) (tf:fundef) + (TF: tunnel_fundef (Internal f) = OK tf), + exists (tf':function), tf = (Internal tf') /\ tunnel_function f = OK tf'. +Proof. + intros f tf. + unfold tunnel_fundef. simpl. intro H. monadInv H. exists x. + split. reflexivity. apply EQ. +Qed. + +Lemma fn_entrypoint_preserved: + forall f tf + (TF: tunnel_function f = OK tf), + fn_entrypoint tf = branch_target f (fn_entrypoint f). +Proof. + intros f tf. + unfold tunnel_function. destruct (check_included _ _); try congruence. + intro TF. monadInv TF. simpl. reflexivity. +Qed. + +Lemma init_regs_lessdef: + forall f tf args targs + (ARGS: list_forall2 Val.lessdef args targs) + (TF: tunnel_function f = OK tf), + regs_lessdef (init_regs args (fn_params f)) (init_regs targs (fn_params tf)). +Proof. + assert (regs_lessdef (Regmap.init Vundef) (Regmap.init Vundef)) as Hundef. + { unfold Regmap.init. unfold regs_lessdef. intro. unfold Regmap.get. rewrite PTree.gempty. apply Val.lessdef_undef. } + + intros f tf args targs ARGS. + + unfold tunnel_function. destruct (check_included _ _) eqn:EQinc; try congruence. + intro TF. monadInv TF. simpl. destruct (fn_params f) eqn:EQP; simpl. + - apply Hundef. + - induction ARGS. + + apply Hundef. + + apply set_reg_lessdef; try assumption. +Admitted. + (* `Lemma tunnel_step_correct` correspond au diagramme "option simulation" *) Lemma tunnel_step_correct: forall st1 t st2, step ge st1 t st2 -> @@ -368,18 +480,124 @@ Proof. intros (tv & EVAL & LD). left; eexists; split. + eapply exec_Iop with (v:=tv). - assert ((fn_code tf) ! pc = Some (Iop op args res (branch_target f pc'))). - rewrite (tunnel_function_unfold f tf pc); eauto. - rewrite H. simpl. reflexivity. - (* TODO: refaire ça joliment *) - assert (target_bounds (branch_target f) (bound (branch_target f)) pc (fn_code f)! pc). - apply (branch_target_bounds) with tf. apply TF. - inv H2. rewrite TB. apply H1. rewrite H in H4. congruence. - rewrite H in H4. congruence. + apply instruction_type_preserved with (Iop op args res pc'); (simpl; auto)||congruence. rewrite <- EVAL. apply eval_operation_preserved. apply symbols_preserved. + apply match_states_intro; eauto. apply set_reg_lessdef. apply LD. apply RS. - (* Iload *) - + exploit eval_addressing_lessdef; try eassumption. + apply reglist_lessdef. apply RS. + intros (ta & EVAL & LD). + exploit Mem.loadv_extends; try eassumption. + intros (tv & LOAD & LD'). + left. eexists. split. + + eapply exec_Iload. + * exploit instruction_type_preserved; (simpl; eauto)||congruence. + * rewrite <- EVAL. apply eval_addressing_preserved. apply symbols_preserved. + * apply LOAD. + + apply match_states_intro; try assumption. apply set_reg_lessdef. apply LD'. apply RS. + - (* Iload NOTRAP1 *) + exploit eval_addressing_lessdef_none; try eassumption. + apply reglist_lessdef; apply RS. + left. eexists. split. + + eapply exec_Iload_notrap1. + * exploit instruction_type_preserved; (simpl; eauto)||congruence. + * rewrite <- H1. apply eval_addressing_preserved. apply symbols_preserved. + + apply match_states_intro; try assumption. apply set_reg_lessdef. unfold default_notrap_load_value. apply Val.lessdef_undef. apply RS. + - (* Iload NOTRAP2 *) + exploit eval_addressing_lessdef; try eassumption. + apply reglist_lessdef; apply RS. + intros (ta & EVAL & LD). + (* TODO: on peut sans doute factoriser ça *) + destruct (Mem.loadv chunk tm ta) eqn:Htload. + + left; eexists; split. + eapply exec_Iload. + * exploit instruction_type_preserved; (simpl; eauto)||congruence. + * rewrite <- EVAL. apply eval_addressing_preserved. apply symbols_preserved. + * apply Htload. + * apply match_states_intro; try assumption. apply set_reg_lessdef; eauto. + + left; eexists; split. + eapply exec_Iload_notrap2. + * exploit instruction_type_preserved; (simpl; eauto)||congruence. + * rewrite <- EVAL. apply eval_addressing_preserved. apply symbols_preserved. + * apply Htload. + * apply match_states_intro; try assumption. apply set_reg_lessdef; eauto. + - (* Lstore *) + exploit eval_addressing_lessdef; try eassumption. + apply reglist_lessdef; apply RS. + intros (ta & EVAL & LD). + exploit Mem.storev_extends; try eassumption. apply RS. + intros (tm' & STORE & MEM'). + left. eexists. split. + + eapply exec_Istore. + * exploit instruction_type_preserved; (simpl; eauto)||congruence. + * rewrite <- EVAL. apply eval_addressing_preserved. apply symbols_preserved. + * rewrite STORE. reflexivity. + + apply match_states_intro; try eassumption. + - (* Icall *) + left. + exploit find_function_translated; try eassumption. + intros (tfd & TFD & FIND). + eexists. split. + + eapply exec_Icall. + * exploit instruction_type_preserved; (simpl; eauto)||congruence. + * apply FIND. + * apply sig_preserved. apply TFD. + + apply match_states_call; try assumption. + * apply list_forall2_cons; try assumption. apply match_stackframes_intro; try assumption. + * apply list_forall2_lessdef_rs. apply RS. + - (* Itailcall *) + exploit find_function_translated; try eassumption. + intros (tfd & TFD & FIND). + exploit Mem.free_parallel_extends; try eassumption. + intros (tm' & FREE & MEM'). + left. eexists. split. + + eapply exec_Itailcall. + * exploit instruction_type_preserved; (simpl; eauto)||congruence. + * apply FIND. + * apply sig_preserved. apply TFD. + * erewrite <- fn_stacksize_preserved; try eassumption. + + apply match_states_call; try assumption. + apply list_forall2_lessdef_rs. apply RS. + - (* Ibuiltin *) + exploit eval_builtin_args_lessdef; try eassumption. apply RS. + intros (vl2 & EVAL & LD). + exploit external_call_mem_extends; try eassumption. + intros (tvres & tm' & EXT & LDRES & MEM' & UNCHGD). + left. eexists. split. + + eapply exec_Ibuiltin. + * exploit instruction_type_preserved; (simpl; eauto)||congruence. + * eapply eval_builtin_args_preserved. eapply symbols_preserved. eapply EVAL. + * eapply external_call_symbols_preserved. eapply senv_preserved. eapply EXT. + + apply match_states_intro; try assumption. apply regs_setres_lessdef; try assumption. + - (* Icond *) + admit. + - (* Ijumptable *) + left. eexists. split. + + eapply exec_Ijumptable. + * exploit instruction_type_preserved; (simpl; eauto)||congruence. + * generalize (RS arg). rewrite H0. intro. inv H2. reflexivity. + * rewrite list_nth_z_map. rewrite H1. simpl. reflexivity. + + apply match_states_intro; try eassumption. + - (* Ireturn *) + exploit Mem.free_parallel_extends; try eassumption. + intros (tm' & FREE & MEM'). + left. eexists. split. + + eapply exec_Ireturn. + * exploit instruction_type_preserved; (simpl; eauto)||congruence. + * erewrite <- fn_stacksize_preserved. eapply FREE. eapply TF. + + apply match_states_return; try eassumption. + apply regmap_optget_lessdef. apply RS. + - (* internal function *) + exploit tunnel_fundef_Internal; try eassumption. + intros (tf' & EQ & TF'). subst. + exploit Mem.alloc_extends; try eassumption. reflexivity. reflexivity. + intros (m2' & ALLOC & EXT). + left. eexists. split. + + eapply exec_function_internal. + rewrite <- (fn_stacksize_preserved f tf'). eapply ALLOC. eapply TF'. + + rewrite (fn_entrypoint_preserved f tf'); try eassumption. apply match_states_intro; try eassumption. + apply init_regs_lessdef. + Qed. -- cgit