diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-11-03 19:56:00 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-11-03 19:56:00 +0100 |
commit | 025a185487c579f768fb747dd6e91a931a2ae66b (patch) | |
tree | 1b35e5e7b5a50f8e96740a6ad51eef7a73481021 /backend | |
parent | 535a8f8706de231f1bd8a7f0243025d84906b03c (diff) | |
download | compcert-kvx-025a185487c579f768fb747dd6e91a931a2ae66b.tar.gz compcert-kvx-025a185487c579f768fb747dd6e91a931a2ae66b.zip |
refixcse3
Diffstat (limited to 'backend')
-rw-r--r-- | backend/CSE3analysis.v | 45 | ||||
-rw-r--r-- | backend/CSE3analysisproof.v | 42 |
2 files changed, 53 insertions, 34 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 5eb92a82..5ed04bc4 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -326,18 +326,21 @@ Section OPERATIONS. | _ => kill_reg dst rel end else - if is_trivial_sym_op op - then kill_reg dst rel - else - let args' := forward_move_l rel args in - match rhs_find op args' rel with - | Some r => - if Compopts.optim_CSE3_glb tt - then RELATION.glb (move r dst rel) - (oper1 dst op args' rel) - else oper1 dst op args' rel - | None => oper1 dst op args' rel - end. + let args' := forward_move_l rel args in + match rhs_find op args rel with + | Some r => + if Compopts.optim_CSE3_glb tt + then RELATION.glb (move r dst rel) + (RELATION.glb + (oper1 dst op args rel) + (oper1 dst op args' rel)) + else RELATION.glb + (oper1 dst op args rel) + (oper1 dst op args' rel) + | None => RELATION.glb + (oper1 dst op args rel) + (oper1 dst op args' rel) + end. Definition clever_kill_store (chunk : memory_chunk) (addr: addressing) (args : list reg) @@ -380,11 +383,21 @@ Section OPERATIONS. end else rel'. - Definition store + Definition store (tenv : typing_env) (chunk : memory_chunk) (addr: addressing) (args : list reg) - (src : reg) (ty: typ) + (src : reg) (rel : RELATION.t) : RELATION.t := - store1 chunk addr (forward_move_l rel args) (forward_move rel src) ty rel. + let args' := forward_move_l rel args in + let src' := forward_move rel src in + let tsrc := tenv src in + let tsrc' := tenv src' in + RELATION.glb + (RELATION.glb + (store1 chunk addr args src tsrc rel) + (store1 chunk addr args' src tsrc rel)) + (RELATION.glb + (store1 chunk addr args src' tsrc' rel) + (store1 chunk addr args' src' tsrc' rel)). Definition kill_builtin_res res rel := match res with @@ -427,7 +440,7 @@ Section OPERATIONS. | Icond _ _ _ _ _ | Ijumptable _ _ => Some rel | Istore chunk addr args src _ => - Some (store chunk addr args src (tenv (forward_move rel src)) rel) + Some (store tenv chunk addr args src rel) | Iop op args dst _ => Some (oper dst (SOp op) args rel) | Iload trap chunk addr args dst _ => Some (oper dst (SLoad chunk addr) args rel) | Icall _ _ _ dst _ => Some (kill_reg dst (kill_mem rel)) diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 07a58f23..1e5b88c3 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -853,24 +853,24 @@ 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. - eapply forward_move_rhs_sound in RHS. - 2: eassumption. + ** pose proof (rhs_find_sound no sop args rel src rs m REL RHS_FIND) as SOUND. rewrite <- (sem_rhs_det SOUND RHS). apply move_sound; auto. + ** apply sem_rel_glb; split. + *** apply oper1_sound; auto. + *** apply oper1_sound; auto. + apply forward_move_rhs_sound; auto. + * apply sem_rel_glb; split. + ** apply oper1_sound; auto. ** 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. + + apply sem_rel_glb; split. + * apply oper1_sound; auto. + * apply oper1_sound; auto. + apply forward_move_rhs_sound; auto. Qed. Hint Resolve oper_sound : cse3. @@ -959,22 +959,28 @@ Section SOUNDNESS. Hint Resolve store1_sound : cse3. + Theorem store_sound: forall no chunk addr args a src rel tenv rs m m', sem_rel rel rs m -> wt_regset tenv rs -> eval_addressing genv sp addr (rs ## args) = Some a -> Mem.storev chunk m a (rs#src) = Some m' -> - sem_rel (store (ctx:=ctx) no chunk addr args src (tenv (forward_move (ctx:=ctx) rel src)) rel) rs m'. + sem_rel (store (ctx:=ctx) no tenv chunk addr args src rel) rs m'. Proof. unfold store. intros until m'. intros REL WT ADDR STORE. - rewrite <- forward_move_l_sound with (rel:=rel) (m:=m) in ADDR by trivial. - rewrite <- forward_move_sound with (rel:=rel) (m:=m) in STORE by trivial. - apply store1_sound with (a := a) (m := m); trivial. - (* rewrite forward_move_sound with (rel:=rel) (m:=m) in STORE by trivial. - assumption. *) + apply sem_rel_glb; split. + - apply sem_rel_glb; split. + * apply store1_sound with (a := a) (m := m); trivial. + * rewrite <- forward_move_l_sound with (rel:=rel) (m:=m) in ADDR by trivial. + apply store1_sound with (a := a) (m := m); trivial. + - rewrite <- forward_move_sound with (rel:=rel) (m:=m) in STORE by trivial. + apply sem_rel_glb; split. + * apply store1_sound with (a := a) (m := m); trivial. + * rewrite <- forward_move_l_sound with (rel:=rel) (m:=m) in ADDR by trivial. + apply store1_sound with (a := a) (m := m); trivial. Qed. Hint Resolve store_sound : cse3. |