diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-03 11:53:59 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-03 11:53:59 +0200 |
| commit | 38e8be31f6445b42526ad577bc388f821649b062 (patch) | |
| tree | 533656e6c1da78581f433239d705d44f446dc93c /backend/CSE.v | |
| parent | b70d80e7259873ac941830e02b022ca8e92541a6 (diff) | |
| parent | 7ae2140a2763f1e646630ceca27c2088aa31cf00 (diff) | |
| download | compcert-kvx-38e8be31f6445b42526ad577bc388f821649b062.tar.gz compcert-kvx-38e8be31f6445b42526ad577bc388f821649b062.zip | |
Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-load
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 aaaf492c..9da30f50 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 => |