removed the unproved hack to get builtins, will be reinstated later

4 files changed, 8 insertions, 74 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
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index d839f22a..50ff377a 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -854,8 +854,6 @@ Remark find_label_commut:
   | _, _ => False
   end.
 Proof.
-Admitted.
-(*
   induction s; intros until k'; simpl; intros MC SE; try (monadInv SE); simpl; auto.
 (* store *)
   unfold store. destruct (addressing m (sel_expr e)); simpl; auto.
@@ -888,7 +886,6 @@ Admitted.
 (* label *)
   destruct (ident_eq lbl l). auto. apply IHs; auto.
 Qed.
- *)
 
 Definition measure (s: Cminor.state) : nat :=
   match s with
@@ -903,8 +900,6 @@ Lemma sel_step_correct:
   (exists T2, step tge T1 t T2 /\ match_states S2 T2)
   \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 T1)%nat.
 Proof.
-Admitted.
-(*
   induction 1; intros T1 ME; inv ME; try (monadInv TS).
 - (* skip seq *)
   inv MC. left; econstructor; split. econstructor. econstructor; eauto.
@@ -1072,7 +1067,6 @@ Admitted.
   right; split. simpl; omega. split. auto. econstructor; eauto.
   apply sel_builtin_res_correct; auto.
 Qed.
- *)
 
 Lemma sel_initial_states:
   forall S, Cminor.initial_state prog S ->
diff --git a/test/monniaux/bitsliced-aes/bs.c b/test/monniaux/bitsliced-aes/bs.c
index 929fd24d..9848d6cb 100644
--- a/test/monniaux/bitsliced-aes/bs.c
+++ b/test/monniaux/bitsliced-aes/bs.c
@@ -2,7 +2,7 @@
 #include <string.h>
 #include "bs.h"
 
-#if defined(__K1C__) && defined(__COMPCERT__)
+#if 0 /* defined(__K1C__) && defined(__COMPCERT__) */
 #define TERNARY(x, v0, v1) __builtin_ternary_ulong((x)!=0, (v1), (v0))
 #else
 #define TERNARY(x, v0, v1) ((x) ? (v1) : (v0))
diff --git a/test/monniaux/bitsliced-tea/bstea.h b/test/monniaux/bitsliced-tea/bstea.h
index 793f29ff..0ebb2f17 100644
--- a/test/monniaux/bitsliced-tea/bstea.h
+++ b/test/monniaux/bitsliced-tea/bstea.h
@@ -6,7 +6,7 @@
 
 #include "bstea_wordsize.h"
 
-#if defined(__K1C__) && defined(__COMPCERT__)
+#if 0 /* defined(__K1C__) && defined(__COMPCERT__) */
 #define TERNARY(x, v1, v0) __builtin_ternary_ulong((x)!=0, (v1), (v0))
 #else
 #define TERNARY(x, v1, v0) ((x) ? (v1) : (v0))