diff options
Diffstat (limited to 'backend/Injectproof.v')
| -rw-r--r-- | backend/Injectproof.v | 254 |
1 files changed, 129 insertions, 125 deletions
diff --git a/backend/Injectproof.v b/backend/Injectproof.v index dd5e72f8..13154850 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -785,24 +785,29 @@ Section INJECTOR. rewrite map_length. assumption. - rewrite Pos.ltb_lt in VALID. - destruct (eval_addressing ge sp addr trs ## args) as [a | ] eqn:ADDR. + destruct (eval_addressing ge sp addr trs ## args) as [a | ] eqn:EVAL. + destruct (Mem.loadv chunk m a) as [v | ] eqn:LOAD. * exists (trs # res <- v). split. - ** apply exec_Iload with (trap := NOTRAP) (chunk := chunk) (addr := addr) (args := args) (dst := res) (a := a); trivial. + ** apply exec_Iload with (trap := NOTRAP) (chunk := chunk) (addr := addr) (args := args) (dst := res); trivial. + eapply has_loaded_normal; eauto. all: try rewrite eval_addressing_preserved with (ge1 := ge). all: auto using symbols_preserved. ** apply assign_above; auto. * exists (trs # res <- Vundef). split. - ** apply exec_Iload_notrap2 with (chunk := chunk) (addr := addr) (args := args) (dst := res) (a := a); trivial. + ** apply exec_Iload with (trap := NOTRAP) (chunk := chunk) (addr := addr) (args := args) (dst := res); trivial. + eapply has_loaded_default; eauto. all: rewrite eval_addressing_preserved with (ge1 := ge). + intros a0 EVAL'; rewrite EVAL in EVAL'; inv EVAL'. assumption. all: auto using symbols_preserved. ** apply assign_above; auto. + exists (trs # res <- Vundef). split. - * apply exec_Iload_notrap1 with (chunk := chunk) (addr := addr) (args := args) (dst := res); trivial. + * apply exec_Iload with (trap := NOTRAP) (chunk := chunk) (addr := addr) (args := args) (dst := res); trivial. + eapply has_loaded_default; eauto. all: rewrite eval_addressing_preserved with (ge1 := ge). + intros a0 EVAL'; rewrite EVAL in EVAL'; inv EVAL'. all: auto using symbols_preserved. * apply assign_above; auto. Qed. @@ -1351,128 +1356,127 @@ Section INJECTOR. assumption. - (* load *) - destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION. - + exploit transf_function_redirects; eauto. - { eapply max_pc_function_sound; eauto. } - intros [pc_inj [ALTER SKIP]]. - specialize SKIP with (ts := ts) (sp := sp) (m := m) - (trs := trs # dst <- v). - destruct SKIP as [trs' [MATCH PLUS]]. - econstructor; split. - * eapply Smallstep.plus_left. - ** apply exec_Iload with (trap := trap) (chunk := chunk) (addr := addr) (args := args) (a := a). - exact ALTER. - rewrite eval_addressing_preserved with (ge1 := ge). - { - replace args with (instr_uses (Iload trap chunk addr args dst pc')) by reflexivity. - rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. - } - exact symbols_preserved. - eassumption. - ** apply Smallstep.plus_star. - exact PLUS. - ** reflexivity. - * constructor; trivial. - apply match_regs_trans with (rs2 := trs # dst <- v); trivial. - apply match_regs_write. - assumption. - + econstructor; split. - * apply Smallstep.plus_one. - apply exec_Iload with (trap := trap) (chunk := chunk) (addr := addr) (args := args) (a := a). - ** rewrite transf_function_preserves with (f:=f); eauto. - eapply max_pc_function_sound; eauto. - ** rewrite eval_addressing_preserved with (ge1 := ge). - { - replace args with (instr_uses (Iload trap chunk addr args dst pc')) by reflexivity. - rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. - } - exact symbols_preserved. - ** eassumption. - * constructor; trivial. - apply match_regs_write. - assumption. - - - (* load notrap1 *) - destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION. - + exploit transf_function_redirects; eauto. + inv H0. + + destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION. + * exploit transf_function_redirects; eauto. { eapply max_pc_function_sound; eauto. } - intros [pc_inj [ALTER SKIP]]. - specialize SKIP with (ts := ts) (sp := sp) (m := m) - (trs := trs # dst <- Vundef). - destruct SKIP as [trs' [MATCH PLUS]]. - econstructor; split. - * eapply Smallstep.plus_left. - ** apply exec_Iload_notrap1 with (chunk := chunk) (addr := addr) (args := args). - exact ALTER. - rewrite eval_addressing_preserved with (ge1 := ge). - { - replace args with (instr_uses (Iload NOTRAP chunk addr args dst pc')) by reflexivity. - rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. - } - exact symbols_preserved. - ** apply Smallstep.plus_star. - exact PLUS. - ** reflexivity. - * constructor; trivial. - apply match_regs_trans with (rs2 := trs # dst <- Vundef); trivial. - apply match_regs_write. - assumption. - + econstructor; split. - * apply Smallstep.plus_one. - apply exec_Iload_notrap1 with (chunk := chunk) (addr := addr) (args := args). - ** rewrite transf_function_preserves with (f:=f); eauto. - eapply max_pc_function_sound; eauto. - ** rewrite eval_addressing_preserved with (ge1 := ge). - { - replace args with (instr_uses (Iload NOTRAP chunk addr args dst pc')) by reflexivity. - rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. - } - exact symbols_preserved. - * constructor; trivial. - apply match_regs_write. - assumption. - - - (* load notrap2 *) - destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION. - + exploit transf_function_redirects; eauto. - { eapply max_pc_function_sound; eauto. } - intros [pc_inj [ALTER SKIP]]. - specialize SKIP with (ts := ts) (sp := sp) (m := m) - (trs := trs # dst <- Vundef). - destruct SKIP as [trs' [MATCH PLUS]]. - econstructor; split. - * eapply Smallstep.plus_left. - ** apply exec_Iload_notrap2 with (chunk := chunk) (addr := addr) (args := args) (a := a). - exact ALTER. - rewrite eval_addressing_preserved with (ge1 := ge). - { - replace args with (instr_uses (Iload NOTRAP chunk addr args dst pc')) by reflexivity. - rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. - } - exact symbols_preserved. - eassumption. - ** apply Smallstep.plus_star. - exact PLUS. - ** reflexivity. - * constructor; trivial. - apply match_regs_trans with (rs2 := trs # dst <- Vundef); trivial. - apply match_regs_write. - assumption. - + econstructor; split. - * apply Smallstep.plus_one. - apply exec_Iload_notrap2 with (chunk := chunk) (addr := addr) (args := args) (a := a). - ** rewrite transf_function_preserves with (f:=f); eauto. - eapply max_pc_function_sound; eauto. - ** rewrite eval_addressing_preserved with (ge1 := ge). - { - replace args with (instr_uses (Iload NOTRAP chunk addr args dst pc')) by reflexivity. - rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. - } - exact symbols_preserved. - ** eassumption. - * constructor; trivial. - apply match_regs_write. - assumption. + intros [pc_inj [ALTER SKIP]]. + specialize SKIP with (ts := ts) (sp := sp) (m := m) + (trs := trs # dst <- v). + destruct SKIP as [trs' [MATCH PLUS]]. + econstructor; split. + -- eapply Smallstep.plus_left. + ** apply exec_Iload with (trap := trap) (chunk := chunk) (addr := addr) (args := args). + exact ALTER. + eapply has_loaded_normal; eauto. rewrite eval_addressing_preserved with (ge1 := ge). + { + replace args with (instr_uses (Iload trap chunk addr args dst pc')) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + } + exact symbols_preserved. + ** apply Smallstep.plus_star. + exact PLUS. + ** reflexivity. + -- constructor; trivial. + apply match_regs_trans with (rs2 := trs # dst <- v); trivial. + apply match_regs_write. + assumption. + * econstructor; split. + -- apply Smallstep.plus_one. + apply exec_Iload with (trap := trap) (chunk := chunk) (addr := addr) (args := args). + ** rewrite transf_function_preserves with (f:=f); eauto. + eapply max_pc_function_sound; eauto. + ** eapply has_loaded_normal; eauto. rewrite eval_addressing_preserved with (ge1 := ge). + { + replace args with (instr_uses (Iload trap chunk addr args dst pc')) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + } + exact symbols_preserved. + -- constructor; trivial. + apply match_regs_write. + assumption. + + destruct (eval_addressing) eqn:EVAL in LOAD. + * specialize (LOAD v). + destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION. + -- exploit transf_function_redirects; eauto. + { eapply max_pc_function_sound; eauto. } + intros [pc_inj [ALTER SKIP]]. + specialize SKIP with (ts := ts) (sp := sp) (m := m) + (trs := trs # dst <- Vundef). + destruct SKIP as [trs' [MATCH PLUS]]. + econstructor; split. + ++ eapply Smallstep.plus_left. + ** apply exec_Iload with (trap := NOTRAP) (chunk := chunk) (addr := addr) (args := args). + exact ALTER. + eapply has_loaded_default; eauto. rewrite eval_addressing_preserved with (ge1 := ge). + { + replace args with (instr_uses (Iload NOTRAP chunk addr args dst pc')) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + simpl. intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'. apply LOAD; auto. + } + exact symbols_preserved. + ** apply Smallstep.plus_star. + exact PLUS. + ** reflexivity. + ++ constructor; trivial. + apply match_regs_trans with (rs2 := trs # dst <- Vundef); trivial. + apply match_regs_write. + assumption. + -- econstructor; split. + ++ apply Smallstep.plus_one. + apply exec_Iload with (trap := NOTRAP) (chunk := chunk) (addr := addr) (args := args). + ** rewrite transf_function_preserves with (f:=f); eauto. + eapply max_pc_function_sound; eauto. + ** eapply has_loaded_default; eauto. rewrite eval_addressing_preserved with (ge1 := ge). + { + replace args with (instr_uses (Iload NOTRAP chunk addr args dst pc')) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + simpl. intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'. apply LOAD; auto. + } + exact symbols_preserved. + ++ constructor; trivial. + apply match_regs_write. + assumption. + * destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION. + -- exploit transf_function_redirects; eauto. + { eapply max_pc_function_sound; eauto. } + intros [pc_inj [ALTER SKIP]]. + specialize SKIP with (ts := ts) (sp := sp) (m := m) + (trs := trs # dst <- Vundef). + destruct SKIP as [trs' [MATCH PLUS]]. + econstructor; split. + ++ eapply Smallstep.plus_left. + ** apply exec_Iload with (trap := NOTRAP) (chunk := chunk) (addr := addr) (args := args). + exact ALTER. + eapply has_loaded_default; eauto. rewrite eval_addressing_preserved with (ge1 := ge). + { + replace args with (instr_uses (Iload NOTRAP chunk addr args dst pc')) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + simpl. intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'. + } + exact symbols_preserved. + ** apply Smallstep.plus_star. + exact PLUS. + ** reflexivity. + ++ constructor; trivial. + apply match_regs_trans with (rs2 := trs # dst <- Vundef); trivial. + apply match_regs_write. + assumption. + -- econstructor; split. + ++ apply Smallstep.plus_one. + apply exec_Iload with (trap := NOTRAP) (chunk := chunk) (addr := addr) (args := args). + ** rewrite transf_function_preserves with (f:=f); eauto. + eapply max_pc_function_sound; eauto. + ** eapply has_loaded_default; eauto. rewrite eval_addressing_preserved with (ge1 := ge). + { + replace args with (instr_uses (Iload NOTRAP chunk addr args dst pc')) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + simpl. intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'. + } + exact symbols_preserved. + ++ constructor; trivial. + apply match_regs_write. + assumption. - (* store *) destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION. |