diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2020-10-29 18:16:59 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-11-07 15:23:45 +0100 |
| commit | 0aeff47ea220a16fec90bcad05e4b79b838a69c9 (patch) | |
| tree | 45b121a50a93b08041e6ac09c20bd614eeddb4c0 /powerpc | |
| parent | 4011a085abee25df19c6e7659f2168ef17c7c344 (diff) | |
| download | compcert-kvx-0aeff47ea220a16fec90bcad05e4b79b838a69c9.tar.gz compcert-kvx-0aeff47ea220a16fec90bcad05e4b79b838a69c9.zip | |
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
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. |