diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-07-03 19:08:18 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-07-17 09:17:28 +0200 |
| commit | 10aa130361a5a673a14a7b38ed9c077103f9155f (patch) | |
| tree | 88b1da80d7f16285f3b4fe19420b6be4c49f618d | |
| parent | e16b34d9fc1aa7854759787fd52ad59c964c2d4b (diff) | |
| download | compcert-10aa130361a5a673a14a7b38ed9c077103f9155f.tar.gz compcert-10aa130361a5a673a14a7b38ed9c077103f9155f.zip | |
Improve CSE for known built-in functions
Known built-in functions are guaranteed not to change memory.
| -rw-r--r-- | backend/CSE.v | 15 | ||||
| -rw-r--r-- | backend/CSEproof.v | 6 |
2 files changed, 14 insertions, 7 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 => diff --git a/backend/CSEproof.v b/backend/CSEproof.v index a60c316b..03c7ecfc 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -14,7 +14,7 @@ Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. Require Import AST Linking. -Require Import Values Memory Events Globalenvs Smallstep. +Require Import Values Memory Builtins Events Globalenvs Smallstep. Require Import Op Registers RTL. Require Import ValueDomain ValueAOp ValueAnalysis. Require Import CSEdomain CombineOp CombineOpproof CSE. @@ -1129,7 +1129,9 @@ Proof. { exists valu. apply set_res_unknown_holds. eapply kill_all_loads_hold; eauto. } destruct ef. + apply CASE1. - + apply CASE3. + + destruct (lookup_builtin_function name sg) as [bf|] eqn:LK. + ++ apply CASE2. simpl in H1; red in H1; rewrite LK in H1; inv H1. auto. + ++ apply CASE3. + apply CASE1. + apply CASE2; inv H1; auto. + apply CASE3. |