diff options
Diffstat (limited to 'backend/Selection.v')
| -rw-r--r-- | backend/Selection.v | 82 |
1 files changed, 77 insertions, 5 deletions
diff --git a/backend/Selection.v b/backend/Selection.v index 4154659c..37a78853 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -26,7 +26,7 @@ Require String. Require Import Coqlib Maps. Require Import AST Errors Integers Globalenvs Switch. Require Cminor. -Require Import Op CminorSel Cminortyping. +Require Import Op CminorSel OpHelpers Cminortyping. Require Import SelectOp SplitLong SelectLong SelectDiv. Require Machregs. @@ -277,6 +277,67 @@ Definition sel_switch_long := (fun arg ofs => subl arg (longconst (Int64.repr ofs))) lowlong. +Definition sel_builtin_default optid ef args := + OK (Sbuiltin (sel_builtin_res optid) ef + (sel_builtin_args args + (Machregs.builtin_constraints ef))). + +Definition sel_builtin optid ef args := + match ef with + | EF_builtin name sign => + (if String.string_dec name "__builtin_ternary_uint" + || String.string_dec name "__builtin_ternary_int" + then + match optid with + | None => OK Sskip + | Some id => + match args with + | a1::a2::a3::nil => + OK (Sassign id (select (sel_expr a3) (sel_expr a2) (sel_expr a1))) + | _ => Error (msg "__builtin_ternary_(u)int: arguments") + end + end + else + if String.string_dec name "__builtin_ternary_ulong" + || String.string_dec name "__builtin_ternary_long" + then + match optid with + | None => OK Sskip + | Some id => + match args with + | a1::a2::a3::nil => + OK (Sassign id (selectl (sel_expr a3) (sel_expr a2) (sel_expr a1))) + | _ => Error (msg "__builtin_ternary_(u)long: arguments") + end + end + else + if String.string_dec name "__builtin_ternary_double" + then + match optid with + | None => OK Sskip + | Some id => + match args with + | a1::a2::a3::nil => + OK (Sassign id (selectf (sel_expr a3) (sel_expr a2) (sel_expr a1))) + | _ => Error (msg "__builtin_ternary_double: arguments") + end + end + else + if String.string_dec name "__builtin_ternary_float" + then + match optid with + | None => OK Sskip + | Some id => + match args with + | a1::a2::a3::nil => + OK (Sassign id (selectfs (sel_expr a3) (sel_expr a2) (sel_expr a1))) + | _ => Error (msg "__builtin_ternary_float: arguments") + end + end + else + sel_builtin_default optid ef args) + | _ => sel_builtin_default optid ef args + (** "If conversion": conversion of certain if-then-else statements into branchless conditional move instructions. *) @@ -342,9 +403,12 @@ Fixpoint sel_stmt (ki: known_idents) (env: typenv) (s: Cminor.stmt) : res stmt : OK (match classify_call fn with | Call_default => Scall optid sg (inl _ (sel_expr fn)) (sel_exprlist args) | Call_imm id => Scall optid sg (inr _ id) (sel_exprlist args) - | Call_builtin ef => Sbuiltin (sel_builtin_res optid) ef - (sel_builtin_args args - (Machregs.builtin_constraints ef)) + | Call_builtin ef => (Sbuiltin (sel_builtin_res optid) ef + (sel_builtin_args args + (Machregs.builtin_constraints ef))) + (* sel_builtin_default optid ef args *) + (* THIS IS WHERE TO ACTIVATE OUR OWN BUILTINS + change sel_builtin_default to sel_builtin *) end) | Cminor.Sbuiltin optid ef args => OK (Sbuiltin (sel_builtin_res optid) ef @@ -466,11 +530,19 @@ Definition get_helpers (defmap: PTree.t globdef) : res helper_functions := do i64_sar <- lookup_helper globs "__compcert_i64_sar" sig_li_l ; do i64_umulh <- lookup_helper globs "__compcert_i64_umulh" sig_ll_l ; do i64_smulh <- lookup_helper globs "__compcert_i64_smulh" sig_ll_l ; + do i32_sdiv <- lookup_helper globs "__compcert_i32_sdiv" sig_ii_i ; + do i32_udiv <- lookup_helper globs "__compcert_i32_udiv" sig_ii_i ; + do i32_smod <- lookup_helper globs "__compcert_i32_smod" sig_ii_i ; + do i32_umod <- lookup_helper globs "__compcert_i32_umod" sig_ii_i ; + do f64_div <- lookup_helper globs "__compcert_f64_div" sig_ff_f ; + do f32_div <- lookup_helper globs "__compcert_f32_div" sig_ss_s ; OK (mk_helper_functions i64_dtos i64_dtou i64_stod i64_utod i64_stof i64_utof i64_sdiv i64_udiv i64_smod i64_umod i64_shl i64_shr i64_sar - i64_umulh i64_smulh). + i64_umulh i64_smulh + i32_sdiv i32_udiv i32_smod i32_umod + f64_div f32_div). (** Conversion of programs. *) |