diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-03 11:53:59 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-03 11:53:59 +0200 |
commit | 38e8be31f6445b42526ad577bc388f821649b062 (patch) | |
tree | 533656e6c1da78581f433239d705d44f446dc93c /backend/Constprop.v | |
parent | b70d80e7259873ac941830e02b022ca8e92541a6 (diff) | |
parent | 7ae2140a2763f1e646630ceca27c2088aa31cf00 (diff) | |
download | compcert-kvx-38e8be31f6445b42526ad577bc388f821649b062.tar.gz compcert-kvx-38e8be31f6445b42526ad577bc388f821649b062.zip |
Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-load
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 b68f4cae..cf1a9171 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 |