Module Builtins1


Platform-specific built-in functions

Require Import String Coqlib.
Require Import AST Integers Floats Values.
Require Import Builtins0.

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) :=
     ("__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
  | 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
  | 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.