From 487fc42595bb43450f2b0b5a49b4edbc22892b9f Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 3 Jun 2019 22:26:06 +0200
Subject: rm old select/selectl/selectf/selectfs

---
 backend/Selection.v     | 61 -------------------------------------------------
 backend/Selectionaux.ml |  6 ++---
 2 files changed, 3 insertions(+), 64 deletions(-)

(limited to 'backend')

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. *)
 
diff --git a/backend/Selectionaux.ml b/backend/Selectionaux.ml
index 52ddd799..b43b0e7f 100644
--- a/backend/Selectionaux.ml
+++ b/backend/Selectionaux.ml
@@ -75,9 +75,9 @@ let fast_cmove ty =
   | "powerpc", _ -> false
   | "riscV", _ -> false
   | "x86", _ -> 
-      (match ty with Tint -> true | Tlong -> Archi.ptr64 | _ -> false)
-  | _, _ ->
-      assert false
+     (match ty with Tint -> true | Tlong -> Archi.ptr64 | _ -> false)
+  | "mppa_k1c", _ -> false (* TODO DM *)
+  | a, m -> failwith (Printf.sprintf "fast_cmove: unknown arch %s %s" a m)
 
 (* The if-conversion heuristic depend on the
    -fif-conversion and -ffavor-branchless flags.
-- 
cgit