diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2019-09-03 10:52:23 +0200 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2019-09-03 10:52:23 +0200 |
commit | 0cb5a0b65b4fbeb5bc1c14f75951798f20500177 (patch) | |
tree | 767381d2490c86dcee95da2631ac5c94e14de8f5 /backend/CSE.v | |
parent | 1fbd5d18a9f4398d7ecb9b9ab148a96f575fd1e0 (diff) | |
parent | 2f7f68f69b6408e4de6210c827b108eff011af51 (diff) | |
download | compcert-kvx-0cb5a0b65b4fbeb5bc1c14f75951798f20500177.tar.gz compcert-kvx-0cb5a0b65b4fbeb5bc1c14f75951798f20500177.zip |
Merge remote-tracking branch 'origin/mppa-work-upstream-merge' into mppa-work
Conflicts:
configure
mppa_k1c/Archi.v
mppa_k1c/Asmexpand.ml
Diffstat (limited to 'backend/CSE.v')
-rw-r--r-- | backend/CSE.v | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/backend/CSE.v b/backend/CSE.v index 6d3f6f33..ecfa1f9e 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -14,7 +14,7 @@ proceeds by value numbering over extended basic blocks. *) Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. -Require Import AST Linking. +Require Import AST Linking Builtins. Require Import Values Memory. Require Import Op Registers RTL. Require Import ValueDomain ValueAnalysis CSEdomain CombineOp. @@ -444,10 +444,10 @@ Module Solver := BBlock_solver(Numbering). ([EF_external], [EF_runtime], [EF_malloc], [EF_free]). - Forget equations involving loads but keep equations over registers. This is appropriate for builtins that can modify memory, - e.g. volatile stores, or [EF_builtin] + e.g. volatile stores, or [EF_builtin] for unknown builtin functions. - Keep all equations, taking advantage of the fact that neither memory - nor registers are modified. This is appropriate for annotations - and for volatile loads. + nor registers are modified. This is appropriate for annotations, + volatile loads, and known builtin functions. *) Definition transfer (f: function) (approx: PMap.t VA.t) (pc: node) (before: numbering) := @@ -473,8 +473,13 @@ Definition transfer (f: function) (approx: PMap.t VA.t) (pc: node) (before: numb match ef with | EF_external _ _ | EF_runtime _ _ | EF_malloc | EF_free | EF_inline_asm _ _ _ => empty_numbering - | EF_builtin _ _ | EF_vstore _ => + | EF_vstore _ => set_res_unknown (kill_all_loads before) res + | EF_builtin name sg => + match lookup_builtin_function name sg with + | Some bf => set_res_unknown before res + | None => set_res_unknown (kill_all_loads before) res + end | EF_memcpy sz al => match args with | dst :: src :: nil => |