selection of builtin.. progress...

1 files changed, 14 insertions, 13 deletions

diff --git a/backend/Selection.v b/backend/Selection.v
index e63cbce3..a87578ba 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -267,20 +267,21 @@ 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"
-       then Sbuiltin (sel_builtin_res optid) ef
-               (sel_builtin_args args
-                                 (Machregs.builtin_constraints ef))
-       else Sbuiltin (sel_builtin_res optid) ef
-               (sel_builtin_args args
-                                 (Machregs.builtin_constraints ef)))
-    | _ =>
-      Sbuiltin (sel_builtin_res optid) ef
-               (sel_builtin_args args
-                                 (Machregs.builtin_constraints ef))
+       then (match optid with
+               | None => OK Sskip
+               | Some id => Error (msg "Selection: ternary uint")
+             end)
+       else sel_builtin_default optid ef args)
+    | _ => sel_builtin_default optid ef args
   end.
 
 (** Conversion from Cminor statements to Cminorsel statements. *)
@@ -291,9 +292,9 @@ 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 =>
-      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)
+      (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
       end)
   | Cminor.Sbuiltin optid ef args =>