diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-10 09:11:12 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-10 09:11:12 +0100 |
| commit | 9cf4ca7760982b40e5721b2d6510eae0ced248a8 (patch) | |
| tree | 78bb00e9705d690f4b567268330c8f47f0a2751d /backend | |
| parent | 33c7fc589ebbbd0ebda9739c479bbd9ee7e526db (diff) | |
| download | compcert-kvx-9cf4ca7760982b40e5721b2d6510eae0ced248a8.tar.gz compcert-kvx-9cf4ca7760982b40e5721b2d6510eae0ced248a8.zip | |
forward_move_l
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/CSE3analysis.v | 12 | ||||
| -rw-r--r-- | backend/CSE3analysisproof.v | 20 |
2 files changed, 29 insertions, 3 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index bbe76f75..c88f06fa 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -128,14 +128,18 @@ Definition get_moves (eqs : PTree.t equation) : Record eq_context := mkeqcontext { eq_catalog : node -> option equation; - eq_kills : reg -> PSet.t; + eq_kill_reg : reg -> PSet.t; + eq_kill_mem : PSet.t; eq_moves : reg -> PSet.t }. Section OPERATIONS. Context {ctx : eq_context}. Definition kill_reg (r : reg) (rel : RELATION.t) : RELATION.t := - PSet.subtract rel (eq_kills ctx r). + PSet.subtract rel (eq_kill_reg ctx r). + + Definition kill_mem (rel : RELATION.t) : RELATION.t := + PSet.subtract rel (eq_kill_mem ctx). Definition pick_source (l : list reg) := (* todo: take min? *) match l with @@ -159,7 +163,9 @@ Section OPERATIONS. | _ => x end end. - + + Definition forward_move_l (rel : RELATION.t) : list reg -> list reg := + List.map (forward_move rel). End OPERATIONS. Definition totoro := RELATION.lub. diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index b14f3964..027a874a 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -277,6 +277,8 @@ Section SOUNDNESS. assumption. Qed. + Hint Resolve kill_reg_sound : cse3. + Lemma pick_source_sound : forall (l : list reg), match pick_source l with @@ -289,6 +291,8 @@ Section SOUNDNESS. left; trivial. Qed. + Hint Resolve pick_source_sound : cse3. + Theorem forward_move_sound : forall rel rs m x, (sem_rel rel rs m) -> @@ -323,6 +327,20 @@ Section SOUNDNESS. intuition congruence. Qed. + Hint Resolve forward_move_sound : cse3. + + Theorem forward_move_l_sound : + forall rel rs m l, + (sem_rel rel rs m) -> + rs ## (forward_move_l (ctx := ctx) rel l) = rs ## l. + Proof. + induction l; simpl; intros; trivial. + erewrite forward_move_sound by eassumption. + intuition congruence. + Qed. + + Hint Resolve forward_move_l_sound : cse3. + Theorem kill_mem_sound : forall rel rs m m', (sem_rel rel rs m) -> @@ -353,4 +371,6 @@ Section SOUNDNESS. intuition. congruence. Qed. + + Hint Resolve kill_mem_sound : cse3. End SOUNDNESS. |