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 /backend/CSEproof.v | |
| parent | e16b34d9fc1aa7854759787fd52ad59c964c2d4b (diff) | |
| download | compcert-kvx-10aa130361a5a673a14a7b38ed9c077103f9155f.tar.gz compcert-kvx-10aa130361a5a673a14a7b38ed9c077103f9155f.zip | |
Improve CSE for known built-in functions
Known built-in functions are guaranteed not to change memory.
Diffstat (limited to 'backend/CSEproof.v')
| -rw-r--r-- | backend/CSEproof.v | 6 |
1 files changed, 4 insertions, 2 deletions
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. |