diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-21 18:04:43 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-21 18:04:43 +0200 |
| commit | 14388a6be6cf7aac50f2af4ff29fe9726ad83435 (patch) | |
| tree | 4d6c2816957e1bdbe262a59ed60cfb72dd1aa3c6 | |
| parent | d10bc429a5c08a25471e3f65e328f5cee12e4542 (diff) | |
| download | compcert-kvx-14388a6be6cf7aac50f2af4ff29fe9726ad83435.tar.gz compcert-kvx-14388a6be6cf7aac50f2af4ff29fe9726ad83435.zip | |
improvement in precision
| -rw-r--r-- | backend/CSE3analysis.v | 4 | ||||
| -rw-r--r-- | backend/CSE3analysisproof.v | 36 |
2 files changed, 34 insertions, 6 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index d3d1c043..b495371d 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -64,6 +64,7 @@ Module RELATION <: SEMILATTICE_WITHOUT_BOTTOM. Qed. Definition lub := PSet.inter. + Definition glb := PSet.union. Lemma ge_lub_left: forall x y, ge (lub x y) x. Proof. @@ -274,7 +275,8 @@ Section OPERATIONS. Definition oper (dst : reg) (op: sym_op) (args : list reg) (rel : RELATION.t) : RELATION.t := match rhs_find op (forward_move_l rel args) rel with - | Some r => move r dst rel + | Some r => RELATION.glb (move r dst rel) + (oper1 dst op args rel) | None => oper1 dst op args rel end. diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index e1e9f6cc..3ea5e078 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -361,6 +361,30 @@ Section SOUNDNESS. eq_catalog ctx i = Some eq -> sem_eq eq rs m. + Lemma sem_rel_glb: + forall rel1 rel2 rs m, + (sem_rel (RELATION.glb rel1 rel2) rs m) <-> + ((sem_rel rel1 rs m) /\ + (sem_rel rel2 rs m)). + Proof. + intros. + unfold sem_rel, RELATION.glb. + split. + - intro IMPLIES. + split; + intros i eq CONTAINS; + specialize IMPLIES with (i:=i) (eq0:=eq); + rewrite PSet.gunion in IMPLIES; + rewrite orb_true_iff in IMPLIES; + intuition. + - intros (IMPLIES1 & IMPLIES2) i eq. + rewrite PSet.gunion. + rewrite orb_true_iff. + specialize IMPLIES1 with (i:=i) (eq0:=eq). + specialize IMPLIES2 with (i:=i) (eq0:=eq). + intuition. + Qed. + Hypothesis ctx_kill_reg_has_lhs : forall lhs sop args j, eq_catalog ctx j = Some {| eq_lhs := lhs; @@ -755,11 +779,13 @@ Section SOUNDNESS. intros REL RHS. unfold oper. destruct rhs_find as [src |] eqn:RHS_FIND. - - 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. - rewrite <- (sem_rhs_det SOUND RHS). - apply move_sound; auto. + - 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. + rewrite <- (sem_rhs_det SOUND RHS). + apply move_sound; auto. + + apply oper1_sound; auto. - apply oper1_sound; auto. Qed. |