diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-11-26 15:11:15 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-11-26 15:11:15 +0100 |
commit | d09c509f8d1bd8335ebedbe260320bb43c5a2723 (patch) | |
tree | 6fb67cb401687e6bdb4d7b7796abc5f56f427329 /backend/CSE3analysis.v | |
parent | d30d56425a8cf73852f7acafe21458be6c787ebc (diff) | |
download | compcert-kvx-d09c509f8d1bd8335ebedbe260320bb43c5a2723.tar.gz compcert-kvx-d09c509f8d1bd8335ebedbe260320bb43c5a2723.zip |
ajouté Cond, tout passe
Diffstat (limited to 'backend/CSE3analysis.v')
-rw-r--r-- | backend/CSE3analysis.v | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 137282a4..4b616568 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -146,7 +146,8 @@ Proof. Defined. Inductive equation_or_condition := - | Equ : reg -> sym_op -> list reg -> equation_or_condition. +| Equ : reg -> sym_op -> list reg -> equation_or_condition +| Cond : condition -> list reg -> equation_or_condition. Definition eq_dec_equation : forall eq eq' : equation_or_condition, {eq = eq'} + {eq <> eq'}. @@ -154,6 +155,7 @@ Proof. generalize peq. generalize eq_dec_sym_op. generalize eq_dec_args. + generalize eq_condition. decide equality. Defined. @@ -172,6 +174,7 @@ Definition get_reg_kills (eqs : PTree.t equation_or_condition) : | Equ lhs sop args => add_i_j lhs eqno (add_ilist_j args eqno already) + | Cond cond args => add_ilist_j args eqno already end) eqs (PMap.init PSet.empty). @@ -182,15 +185,13 @@ Definition eq_cond_depends_on_mem eq_cond := | SLoad _ _ => true | SOp op => op_depends_on_memory op end + | Cond cond args => cond_depends_on_memory cond end. Definition eq_cond_depends_on_store eq_cond := match eq_cond with - | Equ lhs sop args => - match sop with - | SLoad _ _ => true - | SOp op => false - end + | Equ _ (SLoad _ _) _ => true + | _ => false end. Definition get_mem_kills (eqs : PTree.t equation_or_condition) : PSet.t := @@ -229,6 +230,7 @@ Definition get_moves (eqs : PTree.t equation_or_condition) : if is_smove sop then add_i_j lhs eqno already else already + | _ => already end) eqs (PMap.init PSet.empty). Record eq_context := mkeqcontext @@ -294,11 +296,11 @@ Section OPERATIONS. | None => None | Some src => match eq_catalog ctx src with - | None => None | Some (Equ eq_lhs eq_sop eq_args) => if eq_dec_sym_op sop eq_sop && eq_dec_args args eq_args then Some eq_lhs else None + | _ => None end end. |