diff options
| -rw-r--r-- | backend/ForwardMoves.v | 71 | ||||
| -rw-r--r-- | backend/ForwardMovesproof.v | 126 |
2 files changed, 150 insertions, 47 deletions
diff --git a/backend/ForwardMoves.v b/backend/ForwardMoves.v index b812b22d..47fd2457 100644 --- a/backend/ForwardMoves.v +++ b/backend/ForwardMoves.v @@ -272,48 +272,51 @@ Definition forward_map (f : RTL.function) := DS.fixpoint (RTL.fn_code f) RTL.successors_instr (apply_instr' (RTL.fn_code f)) (RTL.fn_entrypoint f) (Some RELATION.top). -Definition subst_arg (rel : RELATION.t) (x : reg) : reg := - match PTree.get x rel with +Definition get_rb (rb : RB.t) (x : reg) := + match rb with | None => x - | Some src => src + | Some rel => + match PTree.get x rel with + | None => x + | Some src => src + end + end. + +Definition subst_arg (fmap : option (PMap.t RB.t)) (pc : node) (x : reg) : reg := + match fmap with + | None => x + | Some inv => get_rb (PMap.get pc inv) x end. -Definition subst_args rel := List.map (subst_arg rel). +Definition subst_args fmap pc := List.map (subst_arg fmap pc). (* Transform *) -Definition transf_instr (fmap : PMap.t RB.t) (pc: node) (instr: instruction) := - match fmap !! pc with - | None => instr - | Some rel => - match instr with - | Iop op args dst s => - Iop op (subst_args rel args) dst s - | Iload trap chunk addr args dst s => - Iload trap chunk addr (subst_args rel args) dst s - | Icall sig ros args dst s => - Icall sig ros (subst_args rel args) dst s - | Itailcall sig ros args => - Itailcall sig ros (subst_args rel args) - | Icond cond args s1 s2 => - Icond cond (subst_args rel args) s1 s2 - | Ijumptable arg tbl => - Ijumptable (subst_arg rel arg) tbl - | Ireturn (Some arg) => - Ireturn (Some (subst_arg rel arg)) - | _ => instr - end +Definition transf_instr (fmap : option (PMap.t RB.t)) + (pc: node) (instr: instruction) := + match instr with + | Iop op args dst s => + Iop op (subst_args fmap pc args) dst s + | Iload trap chunk addr args dst s => + Iload trap chunk addr (subst_args fmap pc args) dst s + | Icall sig ros args dst s => + Icall sig ros (subst_args fmap pc args) dst s + | Itailcall sig ros args => + Itailcall sig ros (subst_args fmap pc args) + | Icond cond args s1 s2 => + Icond cond (subst_args fmap pc args) s1 s2 + | Ijumptable arg tbl => + Ijumptable (subst_arg fmap pc arg) tbl + | Ireturn (Some arg) => + Ireturn (Some (subst_arg fmap pc arg)) + | _ => instr end. Definition transf_function (f: function) : function := - match forward_map f with - | None => f (* can't analyze due to errors ?! *) - | Some fmap => - {| fn_sig := f.(fn_sig); - fn_params := f.(fn_params); - fn_stacksize := f.(fn_stacksize); - fn_code := PTree.map (transf_instr fmap) f.(fn_code); - fn_entrypoint := f.(fn_entrypoint) |} - end. + {| fn_sig := f.(fn_sig); + fn_params := f.(fn_params); + fn_stacksize := f.(fn_stacksize); + fn_code := PTree.map (transf_instr (forward_map f)) f.(fn_code); + fn_entrypoint := f.(fn_entrypoint) |}. Definition transf_fundef (fd: fundef) : fundef := diff --git a/backend/ForwardMovesproof.v b/backend/ForwardMovesproof.v index 936e9e56..c56ba042 100644 --- a/backend/ForwardMovesproof.v +++ b/backend/ForwardMovesproof.v @@ -47,9 +47,6 @@ Lemma sig_preserved: forall f, funsig (transf_fundef f) = funsig f. Proof. destruct f; trivial. - simpl. - unfold transf_function. - destruct (forward_map _); reflexivity. Qed. Lemma find_function_translated: @@ -63,35 +60,58 @@ Proof. eapply function_ptr_translated; eauto. Qed. -(* Lemma transf_function_at: forall f pc i, f.(fn_code)!pc = Some i -> - (transf_function f).(fn_code)!pc = Some(transf_instr pc i). + (transf_function f).(fn_code)!pc = + Some(transf_instr (forward_map f) pc i). Proof. - intros until i. intro Hcode. + intros until i. intro CODE. unfold transf_function; simpl. rewrite PTree.gmap. unfold option_map. - rewrite Hcode. + rewrite CODE. + reflexivity. +Qed. + +Definition fmap_sem (fmap : option (PMap.t RB.t)) (pc : node) (rs : regset) := + forall x : reg, + (rs # (subst_arg fmap pc x)) = (rs # x). + +Lemma apply_instr'_bot : + forall code, + forall pc, + RB.eq (apply_instr' code pc RB.bot) RB.bot. +Proof. reflexivity. Qed. +(*Lemma fmap_sem_step : + forall f : function, + forall pc pc' : node, + forall instr, + (f.fn_code ! pc) = Some instr -> + In pc' (successors_instr instr) -> + (fmap_sem (forward_map f) pc rs) -> + (fmap_sem (forward_map f) pc' rs'). + *) + Ltac TR_AT := match goal with | [ A: (fn_code _)!_ = Some _ |- _ ] => generalize (transf_function_at _ _ _ A); intros end. -*) Inductive match_frames: RTL.stackframe -> RTL.stackframe -> Prop := - | match_frames_intro: forall res f sp pc rs, - match_frames (Stackframe res f sp pc rs) - (Stackframe res (transf_function f) sp pc rs). +| match_frames_intro: forall res f sp pc rs, + (fmap_sem (forward_map f) pc rs) -> + match_frames (Stackframe res f sp pc rs) + (Stackframe res (transf_function f) sp pc rs). Inductive match_states: RTL.state -> RTL.state -> Prop := | match_regular_states: forall stk f sp pc rs m stk' - (STACKS: list_forall2 match_frames stk stk'), + (STACKS: list_forall2 match_frames stk stk'), + (fmap_sem (forward_map f) pc rs) -> match_states (State stk f sp pc rs m) (State stk' (transf_function f) sp pc rs m) | match_callstates: forall stk f args m stk' @@ -106,8 +126,88 @@ Inductive match_states: RTL.state -> RTL.state -> Prop := Lemma step_simulation: forall S1 t S2, RTL.step ge S1 t S2 -> forall S1', match_states S1 S1' -> - exists S2', RTL.step tge S1' t S2' /\ match_states S2 S2'. + exists S2', RTL.step tge S1' t S2' /\ match_states S2 S2'. Admitted. +(* + induction 1; intros S1' MS; inv MS; try TR_AT. +- (* nop *) + econstructor; split. eapply exec_Inop; eauto. + constructor; auto. +- (* op *) + econstructor; split. + eapply exec_Iop with (v := v); eauto. + rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved. + constructor; auto. +(* load *) +- econstructor; split. + assert (eval_addressing tge sp addr rs ## args = Some a). + rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. + eapply exec_Iload; eauto. + constructor; auto. +- (* load notrap1 *) + econstructor; split. + assert (eval_addressing tge sp addr rs ## args = None). + rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. + eapply exec_Iload_notrap1; eauto. + constructor; auto. +- (* load notrap2 *) + econstructor; split. + assert (eval_addressing tge sp addr rs ## args = Some a). + rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. + eapply exec_Iload_notrap2; eauto. + constructor; auto. +- (* store *) + econstructor; split. + assert (eval_addressing tge sp addr rs ## args = Some a). + rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. + eapply exec_Istore; eauto. + constructor; auto. +(* call *) +- econstructor; split. + eapply exec_Icall with (fd := transf_fundef fd); eauto. + eapply find_function_translated; eauto. + apply sig_preserved. + constructor. constructor; auto. constructor. +(* tailcall *) +- econstructor; split. + eapply exec_Itailcall with (fd := transf_fundef fd); eauto. + eapply find_function_translated; eauto. + apply sig_preserved. + constructor. auto. +(* builtin *) +- econstructor; split. + eapply exec_Ibuiltin; eauto. + eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. + constructor; auto. +(* cond *) +- econstructor; split. + eapply exec_Icond; eauto. + constructor; auto. +(* jumptbl *) +- econstructor; split. + eapply exec_Ijumptable; eauto. + constructor; auto. +(* return *) +- econstructor; split. + eapply exec_Ireturn; eauto. + constructor; auto. +(* internal function *) +- simpl. econstructor; split. + eapply exec_function_internal; eauto. + constructor; auto. +(* external function *) +- econstructor; split. + eapply exec_function_external; eauto. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. + constructor; auto. +(* return *) +- inv STACKS. inv H1. + econstructor; split. + eapply exec_return; eauto. + constructor; auto. +Qed. + *) Lemma transf_initial_states: forall S1, RTL.initial_state prog S1 -> |