diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-02-04 16:59:18 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-02-04 16:59:18 +0100 |
| commit | e88c7fa00a5174ecf897b3cb59b7adee818a1788 (patch) | |
| tree | ed92cc7bcc01e0f69afcc80f7fae4c6d23f91c3a /backend/CSE2.v | |
| parent | 0c07f0f560547ae83f3398adcd53be31e7707a62 (diff) | |
| download | compcert-kvx-e88c7fa00a5174ecf897b3cb59b7adee818a1788.tar.gz compcert-kvx-e88c7fa00a5174ecf897b3cb59b7adee818a1788.zip | |
wellformedness for memory
Diffstat (limited to 'backend/CSE2.v')
| -rw-r--r-- | backend/CSE2.v | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/backend/CSE2.v b/backend/CSE2.v index 358fade4..2fc0c323 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -305,8 +305,9 @@ Definition forward_move (rel : RELATION.t) (x : reg) : reg := end. Definition move (src dst : reg) (rel : RELATION.t) := - mkrel (PTree.set dst (SMove (forward_move rel src)) (var_to_sym (kill_reg dst rel))) - (mem_used rel). + let rel0 := kill_reg dst rel in + mkrel (PTree.set dst (SMove (forward_move rel src)) (var_to_sym rel0)) + (mem_used rel0). Definition find_op_fold op args (already : option reg) x sv := match already with @@ -346,7 +347,8 @@ Definition oper2 (op: operation) (dst : reg) (args : list reg) (rel : RELATION.t) : RELATION.t := let rel' := kill_reg dst rel in mkrel (PTree.set dst (SOp op (List.map (forward_move rel') args)) (var_to_sym rel')) - (mem_used rel). + (if op_depends_on_memory op then (pset_add dst (mem_used rel')) + else mem_used rel'). Definition oper1 (op: operation) (dst : reg) (args : list reg) (rel : RELATION.t) : RELATION.t := @@ -372,7 +374,7 @@ Definition load2 (chunk: memory_chunk) (addr : addressing) (dst : reg) (args : list reg) (rel : RELATION.t) : RELATION.t := let rel' := kill_reg dst rel in mkrel (PTree.set dst (SLoad chunk addr (List.map (forward_move rel') args)) (var_to_sym rel')) - (pset_add dst (mem_used rel)). + (pset_add dst (mem_used rel')). Definition load1 (chunk: memory_chunk) (addr : addressing) (dst : reg) (args : list reg) (rel : RELATION.t) := |