diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-21 09:35:30 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-21 09:35:30 +0200 |
| commit | d10bc429a5c08a25471e3f65e328f5cee12e4542 (patch) | |
| tree | 90d1344259731c9e4ca2552a14092f963b59c95e /backend/CSE3analysis.v | |
| parent | c3c275ebe29d06399ecae84c975d1d21f0d4ed44 (diff) | |
| download | compcert-kvx-d10bc429a5c08a25471e3f65e328f5cee12e4542.tar.gz compcert-kvx-d10bc429a5c08a25471e3f65e328f5cee12e4542.zip | |
forward moves through CSE3 store
Diffstat (limited to 'backend/CSE3analysis.v')
| -rw-r--r-- | backend/CSE3analysis.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index bc5d3244..d3d1c043 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -323,7 +323,7 @@ Section OPERATIONS. (chunk : memory_chunk) (addr: addressing) (args : list reg) (src : reg) (ty: typ) (rel : RELATION.t) : RELATION.t := - store1 chunk addr (forward_move_l rel args) src ty rel. + store1 chunk addr (forward_move_l rel args) (forward_move rel src) ty rel. Definition kill_builtin_res res rel := match res with @@ -354,7 +354,7 @@ Section OPERATIONS. | Icond _ _ _ _ _ | Ijumptable _ _ => Some rel | Istore chunk addr args src _ => - Some (store chunk addr args src (tenv src) rel) + Some (store chunk addr args src (tenv (forward_move rel src)) rel) | Iop op args dst _ => Some (oper dst (SOp op) args rel) | Iload trap chunk addr args dst _ => Some (oper dst (SLoad chunk addr) args rel) | Icall _ _ _ dst _ => Some (kill_reg dst (kill_mem rel)) |