diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-10-30 20:59:54 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-10-30 20:59:54 +0100 |
| commit | 7158ee7375fc78ea73248354febdbedfd4abf1fc (patch) | |
| tree | bfb4b50fd226341bd6e45e232f18e049fa0440ad /backend/CSE3proof.v | |
| parent | 82ecfc692b0f84b52162e5f0972fbcc6a9f7f51e (diff) | |
| download | compcert-kvx-7158ee7375fc78ea73248354febdbedfd4abf1fc.tar.gz compcert-kvx-7158ee7375fc78ea73248354febdbedfd4abf1fc.zip | |
reinstated old version
Diffstat (limited to 'backend/CSE3proof.v')
| -rw-r--r-- | backend/CSE3proof.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index a0361746..3fbc9912 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -63,7 +63,7 @@ Proof. destruct rel as [rel | ]; simpl; intros. 2: contradiction. eapply forward_move_sound; eauto. -Qed. + Qed. Lemma forward_move_l_b_sound : forall rel rs m x, @@ -447,6 +447,7 @@ 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'. +Proof. induction 1; intros S1' MS; inv MS. - (* Inop *) exists (State ts tf sp pc' rs m). split. @@ -462,12 +463,12 @@ Lemma step_simulation: destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC. pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SOp op) (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND. - * destruct (if (negb (Compopts.optim_CSE3_trivial_ops tt) && is_trivial_op op) + * destruct (if is_trivial_op op then None else rhs_find pc (SOp op) (subst_args (fst (preanalysis tenv f)) pc args) t) eqn:FIND. - ** destruct (negb (Compopts.optim_CSE3_trivial_ops tt) && is_trivial_op op). discriminate. + ** destruct (is_trivial_op op). discriminate. apply exec_Iop with (op := Omove) (args := r :: nil). TR_AT. subst instr'. |