diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-10 15:06:12 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-10 15:06:12 +0100 |
commit | 11dc19dc169d99a944abb4144ea67eb4fc03f883 (patch) | |
tree | e2302c850109839b7e4bcf890a327cd1f7538ea7 | |
parent | c2319ee007eba06f92837e1e370dfa5e58b06b82 (diff) | |
download | compcert-kvx-11dc19dc169d99a944abb4144ea67eb4fc03f883.tar.gz compcert-kvx-11dc19dc169d99a944abb4144ea67eb4fc03f883.zip |
moved no away
-rw-r--r-- | backend/CSE3analysis.v | 27 | ||||
-rw-r--r-- | backend/CSE3analysisproof.v | 8 |
2 files changed, 23 insertions, 12 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 456898cf..7357a811 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -193,7 +193,10 @@ Section OPERATIONS. Definition forward_move_l (rel : RELATION.t) : list reg -> list reg := List.map (forward_move rel). - Definition eq_find (no : node) (eq : equation) := + Section PER_NODE. + Variable no : node. + + Definition eq_find (eq : equation) := match eq_find_oracle ctx no eq with | Some id => match eq_catalog ctx id with @@ -204,7 +207,7 @@ Section OPERATIONS. end. - Definition rhs_find (no : node) (sop : sym_op) (args : list reg) (rel : RELATION.t) : option reg := + Definition rhs_find (sop : sym_op) (args : list reg) (rel : RELATION.t) : option reg := match pick_source (PSet.elements (PSet.inter (eq_rhs_oracle ctx no sop args) rel)) with | None => None | Some src => @@ -217,15 +220,23 @@ Section OPERATIONS. end end. - Definition oper2 (no : node) (dst : reg) (op: sym_op)(args : list reg) - (rel : RELATION.t) := + Definition oper2 (dst : reg) (op: sym_op)(args : list reg) + (rel : RELATION.t) : RELATION.t := let rel' := kill_reg dst rel in - match eq_find no {| eq_lhs := dst; - eq_op := op; - eq_args:= args |} with + match eq_find {| eq_lhs := dst; + eq_op := op; + eq_args:= args |} with | Some id => PSet.add id rel' | None => rel' end. - End OPERATIONS. + + Definition oper1 (dst : reg) (op: sym_op) (args : list reg) + (rel : RELATION.t) : RELATION.t := + if List.in_dec peq dst args + then kill_reg dst rel + else oper2 dst op args rel. + + End PER_NODE. +End OPERATIONS. Definition totoro := RELATION.lub. diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index e2ce6b5d..a1e57eb5 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -485,10 +485,10 @@ Section SOUNDNESS. sem_rel rel rs m -> sem_rhs sop args rs m v -> ~ In dst args -> - eq_find (ctx := ctx) - no {| eq_lhs := dst; - eq_op := sop; - eq_args:= args |} = Some eqno -> + eq_find (ctx := ctx) no + {| eq_lhs := dst; + eq_op := sop; + eq_args:= args |} = Some eqno -> sem_rel (PSet.add eqno (kill_reg (ctx := ctx) dst rel)) (rs # dst <- v) m. Proof. intros until v. |