From 7158ee7375fc78ea73248354febdbedfd4abf1fc Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 30 Oct 2020 20:59:54 +0100 Subject: reinstated old version --- backend/CSE3proof.v | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'backend/CSE3proof.v') 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'. -- cgit