diff options
Diffstat (limited to 'backend/Constprop.v')
| -rw-r--r-- | backend/Constprop.v | 44 |
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 |