diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-08 20:31:41 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-08 20:31:41 +0100 |
| commit | 2e8e84aea389d41332ebd5a569b474d3c1de23d6 (patch) | |
| tree | 525776da56e9034b450aabc2caaa9a85203b803d /backend/ForwardMoves.v | |
| parent | bc29d9b7abd397e30bd4a9cc5b1f43b9cec409bc (diff) | |
| download | compcert-kvx-2e8e84aea389d41332ebd5a569b474d3c1de23d6.tar.gz compcert-kvx-2e8e84aea389d41332ebd5a569b474d3c1de23d6.zip | |
correct semantics for bottom
Diffstat (limited to 'backend/ForwardMoves.v')
| -rw-r--r-- | backend/ForwardMoves.v | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/backend/ForwardMoves.v b/backend/ForwardMoves.v index 47fd2457..96a19ecd 100644 --- a/backend/ForwardMoves.v +++ b/backend/ForwardMoves.v @@ -272,14 +272,16 @@ Definition forward_map (f : RTL.function) := DS.fixpoint (RTL.fn_code f) RTL.successors_instr (apply_instr' (RTL.fn_code f)) (RTL.fn_entrypoint f) (Some RELATION.top). +Definition get_r (rel : RELATION.t) (x : reg) := + match PTree.get x rel with + | None => x + | Some src => src + end. + Definition get_rb (rb : RB.t) (x : reg) := match rb with | None => x - | Some rel => - match PTree.get x rel with - | None => x - | Some src => src - end + | Some rel => get_r rel x end. Definition subst_arg (fmap : option (PMap.t RB.t)) (pc : node) (x : reg) : reg := |