Merge branch 'mppa-ternary' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-ternary

1 files changed, 46 insertions, 6 deletions

diff --git a/backend/Selection.v b/backend/Selection.v
index 05a06abf..5cfa3dcb 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -267,6 +267,48 @@ 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
+         match optid with
+           | None => OK Sskip
+           | Some id =>
+             match args with
+               | a1::a2::a3::nil =>
+                 OK (Sassign id (Eop Oselect
+                                     ((sel_expr a3):::
+                                      (sel_expr a2):::
+                                      (sel_expr a1):::Enil)))
+               | _ => Error (msg "__builtin_ternary_ulong: arguments")
+             end
+         end
+       else
+       if String.string_dec name "__builtin_ternary_ulong"
+       then
+         match optid with
+           | None => OK Sskip
+           | Some id =>
+             match args with
+               | a1::a2::a3::nil =>
+                 OK (Sassign id (Eop Oselectl
+                                     ((sel_expr a3):::
+                                                   (sel_expr a2):::
+                                                   (sel_expr a1):::Enil)))
+               | _ => Error (msg "__builtin_ternary_uint: 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 :=
@@ -275,12 +317,10 @@ 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)
-      | Call_builtin ef => Sbuiltin (sel_builtin_res optid) ef
-                                    (sel_builtin_args args
-                                       (Machregs.builtin_constraints ef))
+      (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 =>
       OK (Sbuiltin (sel_builtin_res optid) ef