diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-03-17 09:00:42 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-03-17 09:00:42 +0000 |
commit | 7d4128f2e6d73b8f105472f12157488d38898eff (patch) | |
tree | c76f90730ded3a2581f74977abe394b39d6cfc2d /backend/CSE.v | |
parent | 707b6a1ae9660b13cf6f68c7c0ce74017f5981c5 (diff) | |
download | compcert-kvx-7d4128f2e6d73b8f105472f12157488d38898eff.tar.gz compcert-kvx-7d4128f2e6d73b8f105472f12157488d38898eff.zip |
More aggressive CSE across Ibuiltin.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2152 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/CSE.v')
-rw-r--r-- | backend/CSE.v | 24 |
1 files changed, 21 insertions, 3 deletions
diff --git a/backend/CSE.v b/backend/CSE.v index 45a804e8..d381cc82 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -420,8 +420,18 @@ Module Solver := BBlock_solver(Numbering). common subexpressions across a function call (there is a risk of increasing too much the register pressure across the call), so we just forget all equations and start afresh with an empty numbering. - Finally, the remaining instructions modify neither registers nor - the memory, so we keep the numbering unchanged. *) + Finally, for instructions that modify neither registers nor + the memory, we keep the numbering unchanged. + + For builtin invocations [Ibuiltin], we have three strategies: +- Forget all equations. This is appropriate for builtins that can be + turned into function calls ([EF_external], [EF_malloc], [EF_free]). +- Forget equations involving loads but keep equations over registers. + This is appropriate for builtins that modify memory, e.g. [EF_memcpy]. +- Keep all equations, taking advantage of the fact that neither memory + nor registers are modified. This is appropriate for annotations, + for inlined builtin functions, and for volatile loads. +*) Definition transfer (f: function) (pc: node) (before: numbering) := match f.(fn_code)!pc with @@ -441,7 +451,15 @@ Definition transfer (f: function) (pc: node) (before: numbering) := | Itailcall sig ros args => empty_numbering | Ibuiltin ef args res s => - add_unknown (kill_loads before) res + match ef with + | EF_external _ _ | EF_malloc | EF_free | EF_inline_asm _ => + empty_numbering + | EF_vstore _ | EF_vstore_global _ _ _ | EF_memcpy _ _ => + add_unknown (kill_loads before) res + | EF_builtin _ _ | EF_vload _ | EF_vload_global _ _ _ + | EF_annot _ _ | EF_annot_val _ _ => + add_unknown before res + end | Icond cond args ifso ifnot => before | Ijumptable arg tbl => |