diff options
| -rw-r--r-- | backend/CSE3analysisproof.v | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 7c276625..ea4d37ca 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -842,8 +842,6 @@ Section SOUNDNESS. sem_rhs sop args rs m v -> sem_rel (oper (ctx := ctx) no dst sop args rel) (rs # dst <- v) m. Proof. - Admitted. - (* intros until v. intros REL RHS. unfold oper. @@ -856,11 +854,7 @@ Section SOUNDNESS. subst. rewrite <- (forward_move_sound rel rs m r) by auto. apply move_sound; auto. - - destruct (is_trivial_sym_op sop). - { - apply kill_reg_sound; auto. - } - destruct rhs_find as [src |] eqn:RHS_FIND. + - destruct rhs_find as [src |] eqn:RHS_FIND. + destruct (Compopts.optim_CSE3_glb tt). * apply sem_rel_glb; split. ** pose proof (rhs_find_sound no sop (forward_move_l (ctx:=ctx) rel args) rel src rs m REL RHS_FIND) as SOUND. @@ -868,13 +862,19 @@ Section SOUNDNESS. 2: eassumption. rewrite <- (sem_rhs_det SOUND RHS). apply move_sound; auto. + ** apply sem_rel_glb; split. + *** apply oper1_sound; auto. + apply forward_move_rhs_sound; auto. + *** apply oper1_sound; auto. + * apply sem_rel_glb; split. ** apply oper1_sound; auto. apply forward_move_rhs_sound; auto. - * ** apply oper1_sound; auto. - apply forward_move_rhs_sound; auto. - + apply oper1_sound; auto. - apply forward_move_rhs_sound; auto. - Qed. *) + ** apply oper1_sound; auto. + + apply sem_rel_glb; split. + * apply oper1_sound; auto. + apply forward_move_rhs_sound; auto. + * apply oper1_sound; auto. + Qed. Hint Resolve oper_sound : cse3. |