diff --git a/powerpc/Builtins1.v b/powerpc/Builtins1.v
index 53c83d7e5e..9d7aadd9ed 100644
--- a/powerpc/Builtins1.v
+++ b/powerpc/Builtins1.v
@@ -19,15 +19,55 @@ Require Import String Coqlib.
 Require Import AST Integers Floats Values.
 Require Import Builtins0.
 
-Inductive platform_builtin : Type := .
+Inductive platform_builtin : Type :=
+  | BI_isel
+  | BI_uisel
+  | BI_isel64
+  | BI_uisel64
+  | BI_bsel
+  | BI_mulhw
+  | BI_mulhwu
+  | BI_mulhd
+  | BI_mulhdu.
 
 Local Open Scope string_scope.
 
 Definition platform_builtin_table : list (string * platform_builtin) :=
-  nil.
+     ("__builtin_isel", BI_isel)
+  :: ("__builtin_uisel", BI_uisel)
+  :: ("__builtin_isel64", BI_isel64)
+  :: ("__builtin_uisel64", BI_uisel64)
+  :: ("__builtin_bsel", BI_bsel)
+  :: ("__builtin_mulhw", BI_mulhw)
+  :: ("__builtin_mulhwu", BI_mulhwu)
+  :: ("__builtin_mulhd", BI_mulhd)
+  :: ("__builtin_mulhdu", BI_mulhdu)
+  :: nil.
 
 Definition platform_builtin_sig (b: platform_builtin) : signature :=
-  match b with end.
+  match b with
+  | BI_isel | BI_uisel | BI_bsel =>
+     mksignature (Tint :: Tint :: Tint :: nil) Tint cc_default
+  | BI_isel64 | BI_uisel64 =>
+     mksignature (Tint :: Tlong :: Tlong :: nil) Tlong cc_default
+  | BI_mulhw | BI_mulhwu =>
+     mksignature (Tint :: Tint :: nil) Tint cc_default
+  | BI_mulhd | BI_mulhdu =>
+     mksignature (Tlong :: Tlong :: nil) Tlong cc_default
+  end.
 
 Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) :=
-  match b with end.
+  match b with
+  | BI_isel | BI_uisel | BI_bsel =>
+    mkbuiltin_n3t Tint Tint Tint Tint (fun c n1 n2 => if Int.eq c Int.zero then n2 else n1)
+  | BI_isel64 | BI_uisel64 =>
+    mkbuiltin_n3t Tint Tlong Tlong Tlong (fun c n1 n2 => if Int.eq c Int.zero then n2 else n1)
+  | BI_mulhw =>
+    mkbuiltin_n2t Tint Tint Tint Int.mulhs
+  | BI_mulhwu =>
+    mkbuiltin_n2t Tint Tint Tint Int.mulhu
+  | BI_mulhd =>
+    mkbuiltin_n2t Tlong Tlong Tlong Int64.mulhs
+  | BI_mulhdu =>
+    mkbuiltin_n2t Tlong Tlong Tlong Int64.mulhu
+  end.