diff options
Diffstat (limited to 'powerpc')
| -rw-r--r-- | powerpc/Builtins1.v | 48 |
1 files changed, 44 insertions, 4 deletions
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. |