Module Builtins0

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


Definition val_opt_has_rettype (ov: option val) (t: rettype) : Prop :=
  match ov with Some v => Val.has_rettype v t | None => True end.

Definition val_opt_inject (j: meminj) (ov ov': option val) : Prop :=
  match ov, ov' with
  | None, _ => True
  | Some v, Some v' => Val.inject j v v'
  | _, None => False
  end.


Record builtin_sem (tret: rettype) : Type := mkbuiltin {
  bs_sem :> list val -> option val;
  bs_well_typed: forall vl,
    val_opt_has_rettype (bs_sem vl) tret;
  bs_inject: forall j vl vl',
    Val.inject_list j vl vl' -> val_opt_inject j (bs_sem vl) (bs_sem vl')
}.


Local Unset Program Cases.

Program Definition mkbuiltin_v1t
     (tret: rettype) (f: val -> val)
     (WT: forall v1, Val.has_rettype (f v1) tret)
     (INJ: forall j v1 v1', Val.inject j v1 v1' -> Val.inject j (f v1) (f v1')) :=
  mkbuiltin tret (fun vl => match vl with v1 :: nil => Some (f v1) | _ => None end) _ _.

Program Definition mkbuiltin_v2t
     (tret: rettype) (f: val -> val -> val)
     (WT: forall v1 v2, Val.has_rettype (f v1 v2) tret)
     (INJ: forall j v1 v1' v2 v2',
           Val.inject j v1 v1' -> Val.inject j v2 v2' ->
           Val.inject j (f v1 v2) (f v1' v2')) :=
  mkbuiltin tret (fun vl => match vl with v1 :: v2 :: nil => Some (f v1 v2) | _ => None end) _ _.

Program Definition mkbuiltin_v3t
     (tret: rettype) (f: val -> val -> val -> val)
     (WT: forall v1 v2 v3, Val.has_rettype (f v1 v2 v3) tret)
     (INJ: forall j v1 v1' v2 v2' v3 v3',
           Val.inject j v1 v1' -> Val.inject j v2 v2' -> Val.inject j v3 v3' ->
           Val.inject j (f v1 v2 v3) (f v1' v2' v3')) :=
  mkbuiltin tret (fun vl => match vl with v1 :: v2 :: v3 :: nil => Some (f v1 v2 v3) | _ => None end) _ _.

Program Definition mkbuiltin_v1p
     (tret: rettype) (f: val -> option val)
     (WT: forall v1, val_opt_has_rettype (f v1) tret)
     (INJ: forall j v1 v1',
        Val.inject j v1 v1' -> val_opt_inject j (f v1) (f v1')) :=
  mkbuiltin tret (fun vl => match vl with v1 :: nil => f v1 | _ => None end) _ _.

Program Definition mkbuiltin_v2p
     (tret: rettype) (f: val -> val -> option val)
     (WT: forall v1 v2, val_opt_has_rettype (f v1 v2) tret)
     (INJ: forall j v1 v1' v2 v2',
        Val.inject j v1 v1' -> Val.inject j v2 v2' ->
        val_opt_inject j (f v1 v2) (f v1' v2')) :=
  mkbuiltin tret (fun vl => match vl with v1 :: v2 :: nil => f v1 v2 | _ => None end) _ _.



Definition valty (t: typ) : Type :=
  match t with
  | Tint => int
  | Tlong => int64
  | Tfloat => float
  | Tsingle => float32
  | Tany32 | Tany64 => Empty_set (* no clear semantic meaning *)
  end.

Definition valretty (t: rettype) : Type :=
  match t with
  | Tret t => valty t
  | Tint8signed => { n: int | n = Int.sign_ext 8 n }
  | Tint8unsigned => { n: int | n = Int.zero_ext 8 n }
  | Tint16signed => { n: int | n = Int.sign_ext 16 n }
  | Tint16unsigned => { n: int | n = Int.zero_ext 16 n }
  | Tvoid => unit
  end.


Definition inj_num (t: rettype) : valretty t -> val :=
  match t with
  | Tret Tint => Vint
  | Tret Tlong => Vlong
  | Tret Tfloat => Vfloat
  | Tret Tsingle => Vsingle
  | Tret (Tany32 | Tany64) => fun _ => Vundef
  | Tint8signed => fun n => Vint (proj1_sig n)
  | Tint8unsigned => fun n => Vint (proj1_sig n)
  | Tint16signed => fun n => Vint (proj1_sig n)
  | Tint16unsigned => fun n => Vint (proj1_sig n)
  | Tvoid => fun _ => Vundef
  end.


Definition proj_num {A: Type} (t: typ) (k0: A) (v: val): (valty t -> A) -> A :=
  match t with
  | Tint => fun k1 => match v with Vint n => k1 n | _ => k0 end
  | Tlong => fun k1 => match v with Vlong n => k1 n | _ => k0 end
  | Tfloat => fun k1 => match v with Vfloat n => k1 n | _ => k0 end
  | Tsingle => fun k1 => match v with Vsingle n => k1 n | _ => k0 end
  | Tany32 | Tany64 => fun k1 => k0
  end.

Lemma inj_num_wt: forall t x, Val.has_rettype (inj_num t x) t.

Lemma inj_num_inject: forall j t x, Val.inject j (inj_num t x) (inj_num t x).

Lemma inj_num_opt_wt: forall t x, val_opt_has_rettype (option_map (inj_num t) x) t.

Lemma inj_num_opt_inject: forall j t x,
  val_opt_inject j (option_map (inj_num t) x) (option_map (inj_num t) x).

Lemma proj_num_wt:
  forall tres t k1 v,
  (forall x, Val.has_rettype (k1 x) tres) ->
  Val.has_rettype (proj_num t Vundef v k1) tres.

Lemma proj_num_inject:
  forall j t k1 v k1' v',
  (forall x, Val.inject j (k1 x) (k1' x)) ->
  Val.inject j v v' ->
  Val.inject j (proj_num t Vundef v k1) (proj_num t Vundef v' k1').

Lemma proj_num_opt_wt:
  forall tres t k0 k1 v,
  k0 = None \/ k0 = Some Vundef ->
  (forall x, val_opt_has_rettype (k1 x) tres) ->
  val_opt_has_rettype (proj_num t k0 v k1) tres.

Lemma proj_num_opt_inject:
  forall j k0 t k1 v k1' v',
  (forall ov, val_opt_inject j k0 ov) ->
  (forall x, val_opt_inject j (k1 x) (k1' x)) ->
  Val.inject j v v' ->
  val_opt_inject j (proj_num t k0 v k1) (proj_num t k0 v' k1').


Program Definition mkbuiltin_n1t
    (targ1: typ) (tres: rettype)
    (f: valty targ1 -> valretty tres) :=
  mkbuiltin_v1t tres
    (fun v1 => proj_num targ1 Vundef v1 (fun x => inj_num tres (f x)))
    _ _.

Program Definition mkbuiltin_n2t
    (targ1 targ2: typ) (tres: rettype)
    (f: valty targ1 -> valty targ2 -> valretty tres) :=
  mkbuiltin_v2t tres
    (fun v1 v2 =>
       proj_num targ1 Vundef v1 (fun x1 =>
       proj_num targ2 Vundef v2 (fun x2 => inj_num tres (f x1 x2))))
    _ _.

Program Definition mkbuiltin_n3t
    (targ1 targ2 targ3: typ) (tres: rettype)
    (f: valty targ1 -> valty targ2 -> valty targ3 -> valretty tres) :=
  mkbuiltin_v3t tres
    (fun v1 v2 v3 =>
       proj_num targ1 Vundef v1 (fun x1 =>
       proj_num targ2 Vundef v2 (fun x2 =>
       proj_num targ3 Vundef v3 (fun x3 => inj_num tres (f x1 x2 x3)))))
    _ _.

Program Definition mkbuiltin_n1p
    (targ1: typ) (tres: rettype)
    (f: valty targ1 -> option (valretty tres)) :=
  mkbuiltin_v1p tres
    (fun v1 => proj_num targ1 None v1 (fun x => option_map (inj_num tres) (f x)))
    _ _.

Program Definition mkbuiltin_n2p
    (targ1 targ2: typ) (tres: rettype)
    (f: valty targ1 -> valty targ2 -> option (valretty tres)) :=
  mkbuiltin_v2p tres
    (fun v1 v2 =>
      proj_num targ1 None v1 (fun x1 =>
      proj_num targ2 None v2 (fun x2 => option_map (inj_num tres) (f x1 x2))))
    _ _.


Section LOOKUP.

Context {A: Type} (sig_of: A -> signature).

Fixpoint lookup_builtin (name: string) (sg: signature) (l: list (string * A)) : option A :=
  match l with
  | nil => None
  | (n, b) :: l =>
      if string_dec name n && signature_eq sg (sig_of b)
      then Some b
      else lookup_builtin name sg l
  end.

Lemma lookup_builtin_sig: forall name sg b l,
  lookup_builtin name sg l = Some b -> sig_of b = sg.

End LOOKUP.


Inductive standard_builtin : Type :=
  | BI_select (t: typ)
  | BI_fabs
  | BI_fabsf
  | BI_fsqrt
  | BI_negl
  | BI_addl
  | BI_subl
  | BI_mull
  | BI_i16_bswap
  | BI_i32_bswap
  | BI_i64_bswap
  | BI_unreachable
  | BI_i64_umulh
  | BI_i64_smulh
  | BI_i64_sdiv
  | BI_i64_udiv
  | BI_i64_smod
  | BI_i64_umod
  | BI_i64_shl
  | BI_i64_shr
  | BI_i64_sar
  | BI_i64_dtos
  | BI_i64_dtou
  | BI_i64_stod
  | BI_i64_utod
  | BI_i64_stof
  | BI_i64_utof.

Local Open Scope string_scope.

Definition standard_builtin_table : list (string * standard_builtin) :=
    ("__builtin_sel", BI_select Tint)
 :: ("__builtin_sel", BI_select Tlong)
 :: ("__builtin_sel", BI_select Tfloat)
 :: ("__builtin_sel", BI_select Tsingle)
 :: ("__builtin_fabs", BI_fabs)
 :: ("__builtin_fabsf", BI_fabsf)
 :: ("__builtin_fsqrt", BI_fsqrt)
 :: ("__builtin_sqrt", BI_fsqrt)
 :: ("__builtin_negl", BI_negl)
 :: ("__builtin_addl", BI_addl)
 :: ("__builtin_subl", BI_subl)
 :: ("__builtin_mull", BI_mull)
 :: ("__builtin_bswap16", BI_i16_bswap)
 :: ("__builtin_bswap", BI_i32_bswap)
 :: ("__builtin_bswap32", BI_i32_bswap)
 :: ("__builtin_bswap64", BI_i64_bswap)
 :: ("__builtin_unreachable", BI_unreachable)
 :: ("__compcert_i64_umulh", BI_i64_umulh)
 :: ("__compcert_i64_smulh", BI_i64_smulh)
 :: ("__compcert_i64_sdiv", BI_i64_sdiv)
 :: ("__compcert_i64_udiv", BI_i64_udiv)
 :: ("__compcert_i64_smod", BI_i64_smod)
 :: ("__compcert_i64_umod", BI_i64_umod)
 :: ("__compcert_i64_shl", BI_i64_shl)
 :: ("__compcert_i64_shr", BI_i64_shr)
 :: ("__compcert_i64_sar", BI_i64_sar)
 :: ("__compcert_i64_dtos", BI_i64_dtos)
 :: ("__compcert_i64_dtou", BI_i64_dtou)
 :: ("__compcert_i64_stod", BI_i64_stod)
 :: ("__compcert_i64_utod", BI_i64_utod)
 :: ("__compcert_i64_stof", BI_i64_stof)
 :: ("__compcert_i64_utof", BI_i64_utof)
 :: nil.

Definition standard_builtin_sig (b: standard_builtin) : signature :=
  match b with
  | BI_select t =>
      mksignature (Tint :: t :: t :: nil) t cc_default
  | BI_fabs | BI_fsqrt =>
      mksignature (Tfloat :: nil) Tfloat cc_default
  | BI_fabsf =>
      mksignature (Tsingle :: nil) Tsingle cc_default
  | BI_negl =>
      mksignature (Tlong :: nil) Tlong cc_default
  | BI_addl | BI_subl | BI_i64_umulh| BI_i64_smulh
  | BI_i64_sdiv | BI_i64_udiv | BI_i64_smod | BI_i64_umod =>
      mksignature (Tlong :: Tlong :: nil) Tlong cc_default
  | BI_mull =>
      mksignature (Tint :: Tint :: nil) Tlong cc_default
  | BI_i32_bswap =>
      mksignature (Tint :: nil) Tint cc_default
  | BI_i64_bswap =>
      mksignature (Tlong :: nil) Tlong cc_default
  | BI_i16_bswap =>
      mksignature (Tint :: nil) Tint cc_default
  | BI_unreachable =>
      mksignature nil Tvoid cc_default
  | BI_i64_shl | BI_i64_shr | BI_i64_sar =>
      mksignature (Tlong :: Tint :: nil) Tlong cc_default
  | BI_i64_dtos | BI_i64_dtou =>
      mksignature (Tfloat :: nil) Tlong cc_default
  | BI_i64_stod | BI_i64_utod =>
      mksignature (Tlong :: nil) Tfloat cc_default
  | BI_i64_stof | BI_i64_utof =>
      mksignature (Tlong :: nil) Tsingle cc_default
  end.

Program Definition standard_builtin_sem (b: standard_builtin) : builtin_sem (sig_res (standard_builtin_sig b)) :=
  match b with
  | BI_select t =>
      mkbuiltin t
       (fun vargs => match vargs with
          | Vint n :: v1 :: v2 :: nil => Some (Val.normalize (if Int.eq n Int.zero then v2 else v1) t)
          | _ => None
        end) _ _
  | BI_fabs => mkbuiltin_n1t Tfloat Tfloat Float.abs
  | BI_fabsf => mkbuiltin_n1t Tsingle Tsingle Float32.abs
  | BI_fsqrt => mkbuiltin_n1t Tfloat Tfloat Float.sqrt
  | BI_negl => mkbuiltin_n1t Tlong Tlong Int64.neg
  | BI_addl => mkbuiltin_v2t Tlong Val.addl _ _
  | BI_subl => mkbuiltin_v2t Tlong Val.subl _ _
  | BI_mull => mkbuiltin_v2t Tlong Val.mull' _ _
  | BI_i16_bswap =>
    mkbuiltin_n1t Tint Tint
                  (fun n => Int.repr (decode_int (List.rev (encode_int 2%nat (Int.unsigned n)))))
  | BI_i32_bswap =>
    mkbuiltin_n1t Tint Tint
                  (fun n => Int.repr (decode_int (List.rev (encode_int 4%nat (Int.unsigned n)))))
  | BI_i64_bswap =>
    mkbuiltin_n1t Tlong Tlong
                  (fun n => Int64.repr (decode_int (List.rev (encode_int 8%nat (Int64.unsigned n)))))
  | BI_unreachable => mkbuiltin Tvoid (fun vargs => None) _ _
  | BI_i64_umulh => mkbuiltin_n2t Tlong Tlong Tlong Int64.mulhu
  | BI_i64_smulh => mkbuiltin_n2t Tlong Tlong Tlong Int64.mulhs
  | BI_i64_sdiv => mkbuiltin_v2p Tlong Val.divls _ _
  | BI_i64_udiv => mkbuiltin_v2p Tlong Val.divlu _ _
  | BI_i64_smod => mkbuiltin_v2p Tlong Val.modls _ _
  | BI_i64_umod => mkbuiltin_v2p Tlong Val.modlu _ _
  | BI_i64_shl => mkbuiltin_v2t Tlong Val.shll _ _
  | BI_i64_shr => mkbuiltin_v2t Tlong Val.shrlu _ _
  | BI_i64_sar => mkbuiltin_v2t Tlong Val.shrl _ _
  | BI_i64_dtos => mkbuiltin_n1p Tfloat Tlong Float.to_long
  | BI_i64_dtou => mkbuiltin_n1p Tfloat Tlong Float.to_longu
  | BI_i64_stod => mkbuiltin_n1t Tlong Tfloat Float.of_long
  | BI_i64_utod => mkbuiltin_n1t Tlong Tfloat Float.of_longu
  | BI_i64_stof => mkbuiltin_n1t Tlong Tsingle Float32.of_long
  | BI_i64_utof => mkbuiltin_n1t Tlong Tsingle Float32.of_longu
  end.