diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-31 16:25:41 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-31 16:25:41 +0200 |
| commit | e55776fd96f78518da49dfa9e856c3e070353fc9 (patch) | |
| tree | b873ee292a523d03a712fdd17a17c3bf7334e603 /backend/Injectproof.v | |
| parent | ba1c4372b984293ca75a524eb0e532d354377ade (diff) | |
| download | compcert-kvx-e55776fd96f78518da49dfa9e856c3e070353fc9.tar.gz compcert-kvx-e55776fd96f78518da49dfa9e856c3e070353fc9.zip | |
cond
Diffstat (limited to 'backend/Injectproof.v')
| -rw-r--r-- | backend/Injectproof.v | 56 |
1 files changed, 54 insertions, 2 deletions
diff --git a/backend/Injectproof.v b/backend/Injectproof.v index 306e855b..11472c0e 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -1508,8 +1508,60 @@ Section INJECTOR. ** eapply external_call_symbols_preserved; eauto. apply senv_preserved. * admit. - - admit. - - admit. + - (* cond *) + destruct ((gen_injections f) ! pc) eqn:INJECTION. + + destruct b eqn:B. + ++ 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). + destruct SKIP as [trs' [MATCH PLUS]]. + econstructor; split. + * eapply Smallstep.plus_left. + ** apply exec_Icond with (b := true) (cond := cond) (args := args) (ifso := pc_inj) (ifnot := ifnot). + exact ALTER. + replace args with (instr_uses (Icond cond args ifso ifnot)) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + simpl. reflexivity. + ** apply Smallstep.plus_star. + exact PLUS. + ** reflexivity. + * simpl. constructor; auto. + apply match_regs_trans with (rs2:=trs); auto. + + ++ 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). + destruct SKIP as [trs' [MATCH PLUS]]. + econstructor; split. + * eapply Smallstep.plus_one. + apply exec_Icond with (b := false) (cond := cond) (args := args) (ifso := pc_inj) (ifnot := ifnot). + exact ALTER. + replace args with (instr_uses (Icond cond args ifso ifnot)) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + simpl. reflexivity. + * simpl. constructor; auto. + + destruct b eqn:B. + * econstructor; split. + ** eapply Smallstep.plus_one. + apply exec_Icond with (b := true) (cond := cond) (args := args) (ifso := ifso) (ifnot := ifnot). + *** rewrite transf_function_preserves with (f:=f); eauto. + eapply max_pc_function_sound; eauto. + *** replace args with (instr_uses (Icond cond args ifso ifnot)) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + *** reflexivity. + ** constructor; auto. + * econstructor; split. + ** eapply Smallstep.plus_one. + apply exec_Icond with (b := false) (cond := cond) (args := args) (ifso := ifso) (ifnot := ifnot). + *** rewrite transf_function_preserves with (f:=f); eauto. + eapply max_pc_function_sound; eauto. + *** replace args with (instr_uses (Icond cond args ifso ifnot)) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + *** reflexivity. + ** constructor; auto. + - admit. - admit. - admit. |