From 10aa130361a5a673a14a7b38ed9c077103f9155f Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 3 Jul 2019 19:08:18 +0200 Subject: Improve CSE for known built-in functions Known built-in functions are guaranteed not to change memory. --- backend/CSE.v | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) (limited to 'backend/CSE.v') 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 => -- cgit