(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
(*                                                                     *)
(*  Copyright Institut National de Recherche en Informatique et en     *)
(*  Automatique.  All rights reserved.  This file is distributed       *)
(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
(*                                                                     *)
(* *********************************************************************)

(** Instruction selection for 64-bit integer operations *)

Require Import Coqlib.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import CminorSel.
Require Import SelectOp.

Local Open Scope cminorsel_scope.
Local Open Scope string_scope.

(** Some operations on 64-bit integers are transformed into calls to
  runtime library functions or built-in functions.
  Here are the names and signatures of these functions. *)

Definition i64_dtos := ident_of_string "__i64_dtos".
Definition i64_dtou := ident_of_string "__i64_dtou".
Definition i64_stod := ident_of_string "__i64_stod".
Definition i64_utod := ident_of_string "__i64_utod".
Definition i64_stof := ident_of_string "__i64_stof".
Definition i64_utof := ident_of_string "__i64_utof".
Definition i64_neg := ident_of_string "__builtin_negl".
Definition i64_add := ident_of_string "__builtin_addl".
Definition i64_sub := ident_of_string "__builtin_subl".
Definition i64_mul := ident_of_string "__builtin_mull".
Definition i64_sdiv := ident_of_string "__i64_sdiv".
Definition i64_udiv := ident_of_string "__i64_udiv".
Definition i64_smod := ident_of_string "__i64_smod".
Definition i64_umod := ident_of_string "__i64_umod".
Definition i64_shl := ident_of_string "__i64_shl".
Definition i64_shr := ident_of_string "__i64_shr".
Definition i64_sar := ident_of_string "__i64_sar".

Definition sig_l_l := mksignature (Tlong :: nil) (Some Tlong) cc_default.
Definition sig_l_f := mksignature (Tlong :: nil) (Some Tfloat) cc_default.
Definition sig_l_s := mksignature (Tlong :: nil) (Some Tsingle) cc_default.
Definition sig_f_l := mksignature (Tfloat :: nil) (Some Tlong) cc_default.
Definition sig_ll_l := mksignature (Tlong :: Tlong :: nil) (Some Tlong) cc_default.
Definition sig_li_l := mksignature (Tlong :: Tint :: nil) (Some Tlong) cc_default.
Definition sig_ii_l := mksignature (Tint :: Tint :: nil) (Some Tlong) cc_default.

Section SELECT.

Definition makelong (h l: expr): expr :=
  Eop Omakelong (h ::: l ::: Enil).

Nondetfunction splitlong (e: expr) (f: expr -> expr -> expr) :=
  match e with
  | Eop Omakelong (h ::: l ::: Enil) => f h l
  | _ => Elet e (f (Eop Ohighlong (Eletvar O ::: Enil)) (Eop Olowlong (Eletvar O ::: Enil)))
  end.

Nondetfunction splitlong2 (e1 e2: expr) (f: expr -> expr -> expr -> expr -> expr) :=
  match e1, e2 with
  | Eop Omakelong (h1 ::: l1 ::: Enil), Eop Omakelong (h2 ::: l2 ::: Enil) =>
      f h1 l1 h2 l2
  | Eop Omakelong (h1 ::: l1 ::: Enil), t2 =>
      Elet t2 (f (lift h1) (lift l1)
                 (Eop Ohighlong (Eletvar O ::: Enil)) (Eop Olowlong (Eletvar O ::: Enil)))
  | t1, Eop Omakelong (h2 ::: l2 ::: Enil) =>
      Elet t1 (f (Eop Ohighlong (Eletvar O ::: Enil)) (Eop Olowlong (Eletvar O ::: Enil))
                 (lift h2) (lift l2))
  | _, _ =>
      Elet e1 (Elet (lift e2)
        (f (Eop Ohighlong (Eletvar 1 ::: Enil)) (Eop Olowlong (Eletvar 1 ::: Enil))
           (Eop Ohighlong (Eletvar O ::: Enil)) (Eop Olowlong (Eletvar O ::: Enil))))
  end.

Nondetfunction lowlong (e: expr) :=
  match e with
  | Eop Omakelong (e1 ::: e2 ::: Enil) => e2
  | _ => Eop Olowlong (e ::: Enil)
  end.

Nondetfunction highlong (e: expr) :=
  match e with
  | Eop Omakelong (e1 ::: e2 ::: Enil) => e1
  | _ => Eop Ohighlong (e ::: Enil)
  end.

Definition longconst (n: int64) : expr :=
  makelong (Eop (Ointconst (Int64.hiword n)) Enil)
           (Eop (Ointconst (Int64.loword n)) Enil).

Nondetfunction is_longconst (e: expr) :=
  match e with
  | Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) =>
      Some(Int64.ofwords h l)
  | _ =>
      None
  end.

Definition is_longconst_zero (e: expr) :=
  match is_longconst e with
  | Some n => Int64.eq n Int64.zero
  | None => false
  end.

Definition intoflong (e: expr) := lowlong e.

Definition longofint (e: expr) :=
  Elet e (makelong (shrimm (Eletvar O) (Int.repr 31)) (Eletvar O)).

Definition longofintu (e: expr) :=
  makelong (Eop (Ointconst Int.zero) Enil) e.

Definition negl (e: expr) :=
  match is_longconst e with
  | Some n => longconst (Int64.neg n)
  | None => Ebuiltin (EF_builtin i64_neg sig_l_l) (e ::: Enil)
  end.

Definition notl (e: expr) :=
  splitlong e (fun h l => makelong (notint h) (notint l)).

Definition longoffloat (arg: expr) := 
  Eexternal i64_dtos sig_f_l (arg ::: Enil).
Definition longuoffloat (arg: expr) :=
  Eexternal i64_dtou sig_f_l (arg ::: Enil).
Definition floatoflong (arg: expr) :=
  Eexternal i64_stod sig_l_f (arg ::: Enil).
Definition floatoflongu (arg: expr) :=
  Eexternal i64_utod sig_l_f (arg ::: Enil).
Definition longofsingle (arg: expr) := 
  longoffloat (floatofsingle arg).
Definition longuofsingle (arg: expr) :=
  longuoffloat (floatofsingle arg).
Definition singleoflong (arg: expr) :=
  Eexternal i64_stof sig_l_s (arg ::: Enil).
Definition singleoflongu (arg: expr) :=
  Eexternal i64_utof sig_l_s (arg ::: Enil).

Definition andl (e1 e2: expr) :=
  splitlong2 e1 e2 (fun h1 l1 h2 l2 => makelong (and h1 h2) (and l1 l2)).

Definition orl (e1 e2: expr) :=
  splitlong2 e1 e2 (fun h1 l1 h2 l2 => makelong (or h1 h2) (or l1 l2)).

Definition xorl (e1 e2: expr) :=
  splitlong2 e1 e2 (fun h1 l1 h2 l2 => makelong (xor h1 h2) (xor l1 l2)).

Definition shllimm (e1: expr) (n: int) :=
  if Int.eq n Int.zero then e1 else
  if Int.ltu n Int.iwordsize then
   splitlong e1 (fun h l =>
     makelong (or (shlimm h n) (shruimm l (Int.sub Int.iwordsize n)))
              (shlimm l n))
  else if Int.ltu n Int64.iwordsize' then
    makelong (shlimm (lowlong e1) (Int.sub n Int.iwordsize))
             (Eop (Ointconst Int.zero) Enil)
  else
    Eexternal i64_shl sig_li_l (e1 ::: Eop (Ointconst n) Enil ::: Enil).

Definition shrluimm (e1: expr) (n: int) :=
  if Int.eq n Int.zero then e1 else
  if Int.ltu n Int.iwordsize then
    splitlong e1 (fun h l =>
      makelong (shruimm h n)
               (or (shruimm l n) (shlimm h (Int.sub Int.iwordsize n))))
  else if Int.ltu n Int64.iwordsize' then
    makelong (Eop (Ointconst Int.zero) Enil)
             (shruimm (highlong e1) (Int.sub n Int.iwordsize))
  else
    Eexternal i64_shr sig_li_l (e1 ::: Eop (Ointconst n) Enil ::: Enil).

Definition shrlimm (e1: expr) (n: int) :=
  if Int.eq n Int.zero then e1 else
  if Int.ltu n Int.iwordsize then
    splitlong e1 (fun h l =>
      makelong (shrimm h n)
               (or (shruimm l n) (shlimm h (Int.sub Int.iwordsize n))))
  else if Int.ltu n Int64.iwordsize' then
    Elet (highlong e1)
      (makelong (shrimm (Eletvar 0) (Int.repr 31))
                (shrimm (Eletvar 0) (Int.sub n Int.iwordsize)))
  else
    Eexternal i64_sar sig_li_l (e1 ::: Eop (Ointconst n) Enil ::: Enil).

Definition is_intconst (e: expr) :=
  match e with
  | Eop (Ointconst n) Enil => Some n
  | _ => None
  end.

Definition shll (e1 e2: expr) :=
  match is_intconst e2 with
  | Some n => shllimm e1 n
  | None => Eexternal i64_shl sig_li_l (e1 ::: e2 ::: Enil)
  end.

Definition shrlu (e1 e2: expr) :=
  match is_intconst e2 with
  | Some n => shrluimm e1 n
  | None => Eexternal i64_shr sig_li_l (e1 ::: e2 ::: Enil)
  end.

Definition shrl (e1 e2: expr) :=
  match is_intconst e2 with
  | Some n => shrlimm e1 n
  | None => Eexternal i64_sar sig_li_l (e1 ::: e2 ::: Enil)
  end.

Definition addl (e1 e2: expr) :=
  let default := Ebuiltin (EF_builtin i64_add sig_ll_l) (e1 ::: e2 ::: Enil) in
  match is_longconst e1, is_longconst e2 with
  | Some n1, Some n2 => longconst (Int64.add n1 n2)
  | Some n1, _ => if Int64.eq n1 Int64.zero then e2 else default
  | _, Some n2 => if Int64.eq n2 Int64.zero then e1 else default
  | _, _ => default
  end.

Definition subl (e1 e2: expr) :=
  let default := Ebuiltin (EF_builtin i64_sub sig_ll_l) (e1 ::: e2 ::: Enil) in
  match is_longconst e1, is_longconst e2 with
  | Some n1, Some n2 => longconst (Int64.sub n1 n2)
  | Some n1, _ => if Int64.eq n1 Int64.zero then negl e2 else default
  | _, Some n2 => if Int64.eq n2 Int64.zero then e1 else default
  | _, _ => default
  end.

Definition mull_base (e1 e2: expr) :=
  splitlong2 e1 e2 (fun h1 l1 h2 l2 =>
    Elet (Ebuiltin (EF_builtin i64_mul sig_ii_l) (l1 ::: l2 ::: Enil))
      (makelong
        (add (add (Eop Ohighlong (Eletvar O ::: Enil))
                  (mul (lift l1) (lift h2)))
             (mul (lift h1) (lift l2)))
        (Eop Olowlong (Eletvar O ::: Enil)))).

Definition mullimm (e: expr) (n: int64) :=
  if Int64.eq n Int64.zero then longconst Int64.zero else
  if Int64.eq n Int64.one then e else
  match Int64.is_power2 n with
  | Some l => shllimm e (Int.repr (Int64.unsigned l))
  | None   => mull_base e (longconst n)
  end.

Definition mull (e1 e2: expr) :=
  match is_longconst e1, is_longconst e2 with
  | Some n1, Some n2 => longconst (Int64.mul n1 n2)
  | Some n1, _ => mullimm e2 n1
  | _, Some n2 => mullimm e1 n2
  | _, _ => mull_base e1 e2
  end.

Definition binop_long (id: ident) (sem: int64 -> int64 -> int64) (e1 e2: expr) :=
  match is_longconst e1, is_longconst e2 with
  | Some n1, Some n2 => longconst (sem n1 n2)
  | _, _ => Eexternal id sig_ll_l (e1 ::: e2 ::: Enil)
  end.

Definition divl := binop_long i64_sdiv Int64.divs.
Definition modl := binop_long i64_smod Int64.mods.

Definition divlu (e1 e2: expr) :=
  let default := Eexternal i64_udiv sig_ll_l (e1 ::: e2 ::: Enil) in
  match is_longconst e1, is_longconst e2 with
  | Some n1, Some n2 => longconst (Int64.divu n1 n2)
  | _, Some n2 =>
      match Int64.is_power2 n2 with
      | Some l => shrluimm e1 (Int.repr (Int64.unsigned l))
      | None   => default
      end
  | _, _ => default
  end.

Definition modlu (e1 e2: expr) :=
  let default := Eexternal i64_umod sig_ll_l (e1 ::: e2 ::: Enil) in
  match is_longconst e1, is_longconst e2 with
  | Some n1, Some n2 => longconst (Int64.modu n1 n2)
  | _, Some n2 =>
      match Int64.is_power2 n2 with
      | Some l => andl e1 (longconst (Int64.sub n2 Int64.one))
      | None   => default
      end
  | _, _ => default
  end.

Definition cmpl_eq_zero (e: expr) :=
  splitlong e (fun h l => comp Ceq (or h l) (Eop (Ointconst Int.zero) Enil)).

Definition cmpl_ne_zero (e: expr) :=
  splitlong e (fun h l => comp Cne (or h l) (Eop (Ointconst Int.zero) Enil)).

Definition cmplu_gen (ch cl: comparison) (e1 e2: expr) :=
  splitlong2 e1 e2 (fun h1 l1 h2 l2 =>
    Econdition (CEcond (Ccomp Ceq) (h1:::h2:::Enil))
               (Eop (Ocmp (Ccompu cl)) (l1:::l2:::Enil))
               (Eop (Ocmp (Ccompu ch)) (h1:::h2:::Enil))).

Definition cmplu (c: comparison) (e1 e2: expr) :=
  match c with
  | Ceq =>
      cmpl_eq_zero (xorl e1 e2)
(*
        (if is_longconst_zero e2 then e1
         else if is_longconst_zero e1 then e2
         else xorl e1 e2) *)
  | Cne =>
      cmpl_ne_zero (xorl e1 e2)
(*        (if is_longconst_zero e2 then e1
         else if is_longconst_zero e1 then e2
         else xorl e1 e2) *)
  | Clt =>
      cmplu_gen Clt Clt e1 e2
  | Cle =>
      cmplu_gen Clt Cle e1 e2
  | Cgt =>
      cmplu_gen Cgt Cgt e1 e2
  | Cge =>
      cmplu_gen Cgt Cge e1 e2
  end.

Definition cmpl_gen (ch cl: comparison) (e1 e2: expr) :=
  splitlong2 e1 e2 (fun h1 l1 h2 l2 =>
    Econdition (CEcond (Ccomp Ceq) (h1:::h2:::Enil))
               (Eop (Ocmp (Ccompu cl)) (l1:::l2:::Enil))
               (Eop (Ocmp (Ccomp ch)) (h1:::h2:::Enil))).

Definition cmpl (c: comparison) (e1 e2: expr) :=
  match c with
  | Ceq =>
      cmpl_eq_zero (xorl e1 e2)
(*
        (if is_longconst_zero e2 then e1
         else if is_longconst_zero e1 then e2
         else xorl e1 e2) *)
  | Cne =>
      cmpl_ne_zero (xorl e1 e2)
(*        (if is_longconst_zero e2 then e1
         else if is_longconst_zero e1 then e2
         else xorl e1 e2) *)
  | Clt =>
      if is_longconst_zero e2
      then comp Clt (highlong e1) (Eop (Ointconst Int.zero) Enil)
      else cmpl_gen Clt Clt e1 e2
  | Cle =>
      cmpl_gen Clt Cle e1 e2
  | Cgt =>
      cmpl_gen Cgt Cgt e1 e2
  | Cge =>
      if is_longconst_zero e2
      then comp Cge (highlong e1) (Eop (Ointconst Int.zero) Enil)
      else cmpl_gen Cgt Cge e1 e2
  end.

End SELECT.

(** Checking that the helper functions are available. *)

Require Import Errors.
Require Import Globalenvs.
Local Open Scope error_monad_scope.

Definition check_helper (ge: Cminor.genv) (name_sg: ident * signature) : res unit :=
  let (name, sg) := name_sg in
  match Genv.find_symbol ge name with
  | None => 
      Error (CTX name :: MSG ": not declared" :: nil)
  | Some b =>
      match Genv.find_funct_ptr ge b with
      | Some (External (EF_external name' sg')) =>
          if ident_eq name' name && signature_eq sg' sg
          then OK tt
          else Error (CTX name :: MSG ": wrong declaration" :: nil)
      | _ =>
          Error (CTX name :: MSG ": wrong declaration" :: nil)
      end
  end.

Definition i64_helpers :=
    (i64_dtos, sig_f_l) ::
    (i64_dtou, sig_f_l) ::
    (i64_stod, sig_l_f) ::
    (i64_utod, sig_l_f) ::
    (i64_stof, sig_l_s) ::
    (i64_utof, sig_l_s) ::
    (i64_sdiv, sig_ll_l) ::
    (i64_udiv, sig_ll_l) ::
    (i64_smod, sig_ll_l) ::
    (i64_umod, sig_ll_l) ::
    (i64_shl, sig_li_l) ::
    (i64_shr, sig_li_l) ::
    (i64_sar, sig_li_l) ::
    nil.

Definition check_helpers (ge: Cminor.genv): res unit :=
  do x <- mmap (check_helper ge) i64_helpers;
  OK tt.