diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-28 15:24:11 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-28 15:24:11 +0100 |
| commit | 3e15c72f5a5e34ac2e96e77022b2129125abcdd0 (patch) | |
| tree | 7394fda2104b24e5da78b5202189ad5937dd2418 /backend/CSE2proof.v | |
| parent | a7df9f6f48aa9282cb66b02bb63ca047b01f09b4 (diff) | |
| download | compcert-kvx-3e15c72f5a5e34ac2e96e77022b2129125abcdd0.tar.gz compcert-kvx-3e15c72f5a5e34ac2e96e77022b2129125abcdd0.zip | |
much better - seems to eliminate CSE not containing loads
Diffstat (limited to 'backend/CSE2proof.v')
| -rw-r--r-- | backend/CSE2proof.v | 18 |
1 files changed, 17 insertions, 1 deletions
diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index 47b60902..049423b0 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -372,6 +372,21 @@ Proof. apply REC; auto. Qed. +Lemma forward_move_map: + forall rel args rs, + sem_rel rel rs -> + rs ## (map (forward_move rel) args) = rs ## args. +Proof. + induction args; simpl; trivial. + intros rs REL. + f_equal. + 2: (apply IHargs; assumption). + unfold forward_move, sem_rel, sem_reg, sem_sym_val in *. + pose proof (REL a) as RELa. + destruct (rel ! a); trivial. + destruct s; congruence. +Qed. + Lemma oper_sound : forall rel : RELATION.t, forall op : operation, @@ -388,10 +403,11 @@ Proof. unfold oper. destruct find_op eqn:FIND. { - assert (eval_operation genv sp op rs ## args m = Some rs # r). + assert (eval_operation genv sp op rs ## (map (forward_move rel) args) m = Some rs # r) as FIND_OP. { apply (find_op_sound rel); trivial. } + rewrite forward_move_map in FIND_OP by assumption. replace v with (rs # r) by congruence. apply move_sound; auto. } |