Perform constant propagation for known built-in functions

When an external function is a known built-in function and it is
applied to compile-time integer or FP constants, we can use
the known semantics of the builtin to compute the result
at compile-time.

1 files changed, 42 insertions, 2 deletions

diff --git a/backend/Constprop.v b/backend/Constprop.v
index d8211ffe..4aab7677 100644
--- a/backend/Constprop.v
+++ b/backend/Constprop.v
@@ -15,7 +15,7 @@
   and the corresponding code rewriting. *)
 
 Require Import Coqlib Maps Integers Floats Lattice Kildall.
-Require Import AST Linking.
+Require Import AST Linking Builtins.
 Require Compopts Machregs.
 Require Import Op Registers RTL.
 Require Import Liveness ValueDomain ValueAOp ValueAnalysis.
@@ -139,6 +139,30 @@ Definition builtin_strength_reduction
   | _ => builtin_args_strength_reduction ae al (Machregs.builtin_constraints ef)
   end.
 
+(*
+Definition transf_builtin
+             (ae: AE.t) (am: amem) (rm: romem)
+             (ef: external_function)
+             (args: list (builtin_arg reg)) (res: builtin_res reg) (s: node) :=
+  let dfl := Ibuiltin ef (builtin_strength_reduction ae ef args) res s in
+  match ef, res with
+  | EF_builtin name sg, BR rd =>
+      match lookup_builtin_function name sg with
+      | Some bf => 
+          match eval_static_builtin_function ae am rm bf args with
+          | Some a =>
+              match const_for_result a with
+              | Some cop => Iop cop nil rd s
+              | None => dfl
+              end
+          | None => dfl
+          end
+      | None => dfl
+      end
+  | _, _ => dfl
+  end.
+*)
+
 Definition transf_instr (f: function) (an: PMap.t VA.t) (rm: romem)
                         (pc: node) (instr: instruction) :=
   match an!!pc with
@@ -176,7 +200,23 @@ Definition transf_instr (f: function) (an: PMap.t VA.t) (rm: romem)
       | Itailcall sig ros args =>
           Itailcall sig (transf_ros ae ros) args
       | Ibuiltin ef args res s =>
-          Ibuiltin ef (builtin_strength_reduction ae ef args) res s
+          let dfl := Ibuiltin ef (builtin_strength_reduction ae ef args) res s in
+          match ef, res with
+          | EF_builtin name sg, BR rd =>
+              match lookup_builtin_function name sg with
+              | Some bf => 
+                  match eval_static_builtin_function ae am rm bf args with
+                  | Some a =>
+                      match const_for_result a with
+                      | Some cop => Iop cop nil rd s
+                      | None => dfl
+                      end
+                 | None => dfl
+                 end
+             | None => dfl
+             end
+          | _, _ => dfl
+          end
       | Icond cond args s1 s2 =>
           let aargs := aregs ae args in
           match resolve_branch (eval_static_condition cond aargs) with