diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-02-27 05:45:13 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-02-27 05:45:13 +0100 |
| commit | 222c9047d61961db9c6b19fed5ca49829223fd33 (patch) | |
| tree | 70350802e58091cf90560060f1775148124bc0d0 /backend/CSE2proof.v | |
| parent | a5e20ecb933a1dc12bae3e4eeb330e86f13832d8 (diff) | |
| download | compcert-kvx-222c9047d61961db9c6b19fed5ca49829223fd33.tar.gz compcert-kvx-222c9047d61961db9c6b19fed5ca49829223fd33.zip | |
CSE2 now uses is_trivial_op
Diffstat (limited to 'backend/CSE2proof.v')
| -rw-r--r-- | backend/CSE2proof.v | 23 |
1 files changed, 21 insertions, 2 deletions
diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index 0b92f5e5..eb4268f0 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -1401,6 +1401,24 @@ Proof. Qed. Hint Resolve wellformed_mem_mpc : wellformed. +Lemma match_same_option : + forall { A B : Type}, + forall x : option A, + forall y : B, + (match x with Some _ => y | None => y end) = y. +Proof. + destruct x; trivial. +Qed. + +Lemma match_same_bool : + forall { B : Type}, + forall x : bool, + forall y : B, + (if x then y else y) = y. +Proof. + destruct x; trivial. +Qed. + Lemma step_simulation: forall S1 t S2, RTL.step ge S1 t S2 -> forall S1', match_states S1 S1' -> @@ -1428,8 +1446,9 @@ Proof. reflexivity. - (* op *) unfold transf_instr in *. - destruct find_op_in_fmap eqn:FIND_OP. + destruct (if is_trivial_op op then None else find_op_in_fmap (forward_map f) pc op (subst_args (forward_map f) pc args)) eqn:FIND_OP. { + destruct is_trivial_op. discriminate. unfold find_op_in_fmap, fmap_sem', fmap_sem in *. destruct (forward_map f) as [map |] eqn:MAP. 2: discriminate. @@ -1846,4 +1865,4 @@ Proof. exact step_simulation. Qed. -End PRESERVATION.
\ No newline at end of file +End PRESERVATION. |