aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Selection.v
diff options
context:
space:
mode:
Diffstat (limited to 'backend/Selection.v')
-rw-r--r--backend/Selection.v61
1 files changed, 0 insertions, 61 deletions
diff --git a/backend/Selection.v b/backend/Selection.v
index 37a78853..2d407094 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -277,67 +277,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
-
(** "If conversion": conversion of certain if-then-else statements
into branchless conditional move instructions. *)