Commit 0aeff47e authored by Bernhard Schommer's avatar Bernhard Schommer Committed by Xavier Leroy
Browse files

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
parent 4011a085
......@@ -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.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment