diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-01 09:57:01 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-01 09:57:01 +0200 |
commit | 951963b380f1ff1e0b55f8303e4ae098cedb3cb5 (patch) | |
tree | 6cc793efe8fc8d2950d7b313bfde79b2ecf40d24 /backend/Constprop.v | |
parent | 7cfaf10b604372044f53cb65b03df33c23f8b26d (diff) | |
parent | 3324ece265091490d5380caf753d76aeee059d3f (diff) | |
download | compcert-951963b380f1ff1e0b55f8303e4ae098cedb3cb5.tar.gz compcert-951963b380f1ff1e0b55f8303e4ae098cedb3cb5.zip |
Merge branch 'new-builtins'
Diffstat (limited to 'backend/Constprop.v')
-rw-r--r-- | backend/Constprop.v | 73 |
1 files changed, 45 insertions, 28 deletions
diff --git a/backend/Constprop.v b/backend/Constprop.v index ce56ff62..cd844d30 100644 --- a/backend/Constprop.v +++ b/backend/Constprop.v @@ -20,6 +20,7 @@ Require Import AST. Require Import Integers. Require Import Floats. Require Import Op. +Require Machregs. Require Import Registers. Require Import RTL. Require Import Lattice. @@ -102,39 +103,58 @@ Definition num_iter := 10%nat. Definition successor (f: function) (ae: AE.t) (pc: node) : node := successor_rec num_iter f ae pc. -Fixpoint annot_strength_reduction (ae: AE.t) (a: annot_arg reg) := +Fixpoint builtin_arg_reduction (ae: AE.t) (a: builtin_arg reg) := match a with - | AA_base r => + | BA r => match areg ae r with - | I n => AA_int n - | L n => AA_long n - | F n => if Compopts.generate_float_constants tt then AA_float n else a - | FS n => if Compopts.generate_float_constants tt then AA_single n else a + | I n => BA_int n + | L n => BA_long n + | F n => if Compopts.generate_float_constants tt then BA_float n else a + | FS n => if Compopts.generate_float_constants tt then BA_single n else a | _ => a end - | AA_longofwords hi lo => - match annot_strength_reduction ae hi, annot_strength_reduction ae lo with - | AA_int nhi, AA_int nlo => AA_long (Int64.ofwords nhi nlo) - | hi', lo' => AA_longofwords hi' lo' + | BA_splitlong hi lo => + match builtin_arg_reduction ae hi, builtin_arg_reduction ae lo with + | BA_int nhi, BA_int nlo => BA_long (Int64.ofwords nhi nlo) + | hi', lo' => BA_splitlong hi' lo' end | _ => a end. -Function builtin_strength_reduction - (ae: AE.t) (ef: external_function) (args: list reg) := - match ef, args with - | EF_vload chunk, r1 :: nil => - match areg ae r1 with - | Ptr(Gl symb n1) => (EF_vload_global chunk symb n1, nil) - | _ => (ef, args) - end - | EF_vstore chunk, r1 :: r2 :: nil => - match areg ae r1 with - | Ptr(Gl symb n1) => (EF_vstore_global chunk symb n1, r2 :: nil) - | _ => (ef, args) +Definition builtin_arg_strength_reduction + (ae: AE.t) (a: builtin_arg reg) (c: builtin_arg_constraint) := + let a' := builtin_arg_reduction ae a in + if builtin_arg_ok a' c then a' else a. + +Fixpoint builtin_args_strength_reduction + (ae: AE.t) (al: list (builtin_arg reg)) (cl: list builtin_arg_constraint) := + match al with + | nil => nil + | a :: al => + builtin_arg_strength_reduction ae a (List.hd OK_default cl) + :: builtin_args_strength_reduction ae al (List.tl cl) + end. + +(** For debug annotations, add constant values to the original info + instead of replacing it. *) + +Fixpoint debug_strength_reduction (ae: AE.t) (al: list (builtin_arg reg)) := + match al with + | nil => nil + | a :: al => + let a' := builtin_arg_reduction ae a in + let al' := a :: debug_strength_reduction ae al in + match a' with + | BA_int _ | BA_long _ | BA_float _ | BA_single _ => a' :: al' + | _ => al' end - | _, _ => - (ef, args) + end. + +Definition builtin_strength_reduction + (ae: AE.t) (ef: external_function) (al: list (builtin_arg reg)) := + match ef with + | EF_debug _ _ _ => debug_strength_reduction ae al + | _ => builtin_args_strength_reduction ae al (Machregs.builtin_constraints ef) end. Definition transf_instr (f: function) (an: PMap.t VA.t) (rm: romem) @@ -174,10 +194,7 @@ 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 => - let (ef', args') := builtin_strength_reduction ae ef args in - Ibuiltin ef' args' res s - | Iannot ef args s => - Iannot ef (List.map (annot_strength_reduction ae) args) s + Ibuiltin ef (builtin_strength_reduction ae ef args) res s | Icond cond args s1 s2 => let aargs := aregs ae args in match resolve_branch (eval_static_condition cond aargs) with |