diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-05 13:52:34 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-05 13:52:34 +0200 |
| commit | 799698875bd5b42b9ef5e57138f71128e68ed35e (patch) | |
| tree | 2c577959006a78fc7067560995899a96e44ec764 /backend/Selection.v | |
| parent | e4bc9aa604977ee168c2f580d3fc3c3521f6c25c (diff) | |
| download | compcert-kvx-799698875bd5b42b9ef5e57138f71128e68ed35e.tar.gz compcert-kvx-799698875bd5b42b9ef5e57138f71128e68ed35e.zip | |
removed the unproved hack to get builtins, will be reinstated later
Diffstat (limited to 'backend/Selection.v')
| -rw-r--r-- | backend/Selection.v | 72 |
1 files changed, 6 insertions, 66 deletions
diff --git a/backend/Selection.v b/backend/Selection.v index d2067dab..05a06abf 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -267,68 +267,6 @@ 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 - end. - (** Conversion from Cminor statements to Cminorsel statements. *) Fixpoint sel_stmt (s: Cminor.stmt) : res stmt := @@ -337,10 +275,12 @@ Fixpoint sel_stmt (s: Cminor.stmt) : res stmt := | Cminor.Sassign id e => OK (Sassign id (sel_expr e)) | Cminor.Sstore chunk addr rhs => OK (store chunk (sel_expr addr) (sel_expr rhs)) | Cminor.Scall optid sg fn args => - (match classify_call fn with - | Call_default => OK (Scall optid sg (inl _ (sel_expr fn)) (sel_exprlist args)) - | Call_imm id => OK (Scall optid sg (inr _ id) (sel_exprlist args)) - | Call_builtin ef => sel_builtin optid ef args + 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)) end) | Cminor.Sbuiltin optid ef args => OK (Sbuiltin (sel_builtin_res optid) ef |