diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-03 22:26:06 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-03 22:26:06 +0200 |
| commit | 487fc42595bb43450f2b0b5a49b4edbc22892b9f (patch) | |
| tree | eb671c210dd1e09651003c4f0add4cca118519a2 /backend/Selection.v | |
| parent | 677771949bd62f7f5bbcf99bba6b6f816f07a6c2 (diff) | |
| download | compcert-kvx-487fc42595bb43450f2b0b5a49b4edbc22892b9f.tar.gz compcert-kvx-487fc42595bb43450f2b0b5a49b4edbc22892b9f.zip | |
rm old select/selectl/selectf/selectfs
Diffstat (limited to 'backend/Selection.v')
| -rw-r--r-- | backend/Selection.v | 61 |
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. *) |