From 0aeff47ea220a16fec90bcad05e4b79b838a69c9 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Thu, 29 Oct 2020 18:16:59 +0100
Subject: Added semantics for the PowerPC sel and mulh built-ins

The semantics of the various selection functions are defined analogously
to the ones from the type generic sel function. The semantics for the
various high word multiplication functions is defined using the Integer
functions.
Bug 30035
---
 powerpc/Builtins1.v | 48 ++++++++++++++++++++++++++++++++++++++++++++----
 1 file changed, 44 insertions(+), 4 deletions(-)

(limited to 'powerpc')

diff --git a/powerpc/Builtins1.v b/powerpc/Builtins1.v
index 53c83d7e..9d7aadd9 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.
-- 
cgit