(* *************************************************************)
(*                                                             *)
(*             The Compcert verified compiler                  *)
(*                                                             *)
(*           Sylvain Boulmé     Grenoble-INP, VERIMAG          *)
(*           Xavier Leroy       INRIA Paris-Rocquencourt       *)
(*           David Monniaux     CNRS, VERIMAG                  *)
(*           Cyril Six          Kalray                         *)
(*                                                             *)
(*  Copyright Kalray. Copyright VERIMAG. 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 Compopts.
Require Import AST Integers Floats.
Require Import Op CminorSel.
Require Import OpHelpers.
Require Import SelectOp SplitLong.
Require Import ExtValues.
Require Import DecBoolOps.
Require FPExtra.

Local Open Scope cminorsel_scope.
Local Open Scope string_scope.

Section SELECT.

Context {hf: helper_functions}.

Definition longconst (n: int64) : expr :=
  if Archi.splitlong then SplitLong.longconst n else Eop (Olongconst n) Enil.

Definition is_longconst (e: expr) :=
  if Archi.splitlong then SplitLong.is_longconst e else
  match e with
  | Eop (Olongconst n) Enil => Some n
  | _ => None
  end.

Definition intoflong (e: expr) :=
  if Archi.splitlong then SplitLong.intoflong e else
  match is_longconst e with
  | Some n => Eop (Ointconst (Int.repr (Int64.unsigned n))) Enil
  | None =>  Eop Olowlong (e ::: Enil)
  end.

Definition longofint (e: expr) :=
  if Archi.splitlong then SplitLong.longofint e else
  match is_intconst e with
  | Some n => longconst (Int64.repr (Int.signed n))
  | None =>  Eop Ocast32signed (e ::: Enil)
  end.

Definition longofintu (e: expr) :=
  if Archi.splitlong then SplitLong.longofintu e else
  match is_intconst e with
  | Some n => longconst (Int64.repr (Int.unsigned n))
  | None =>  Eop Ocast32unsigned (e ::: Enil)
  end.

(** ** Integer addition and pointer addition *)

Definition addlimm_shllimm sh k2 e1 :=
  if Compopts.optim_addx tt
  then
    match shift1_4_of_z (Int.unsigned sh) with
    | Some s14 => Eop (Oaddxlimm s14 k2) (e1:::Enil)
    | None => Eop (Oaddlimm k2) ((Eop (Oshllimm sh) (e1:::Enil)):::Enil)
    end
  else Eop (Oaddlimm k2) ((Eop (Oshllimm sh) (e1:::Enil)):::Enil).

Nondetfunction addlimm (n: int64) (e: expr) :=
  if Int64.eq n Int64.zero then e else
  match e with
  | Eop (Olongconst m) Enil => longconst (Int64.add n m)
  | Eop (Oaddrsymbol s m) Enil   =>
    (if Compopts.optim_globaladdroffset tt
     then Eop (Oaddrsymbol s (Ptrofs.add (Ptrofs.of_int64 n) m)) Enil
     else Eop (Oaddlimm n) (e ::: Enil))
  | Eop (Oaddrstack m) Enil      => Eop (Oaddrstack (Ptrofs.add (Ptrofs.of_int64 n) m)) Enil
  | Eop (Oaddlimm m) (t ::: Enil) => Eop (Oaddlimm(Int64.add n m)) (t ::: Enil)
  | Eop (Oaddxlimm sh m) (t ::: Enil) => Eop (Oaddxlimm sh (Int64.add n m)) (t ::: Enil)
  | Eop (Oshllimm sh) (t1:::Enil) => addlimm_shllimm sh n t1
  | _ => Eop (Oaddlimm n) (e ::: Enil)
  end.

Definition addl_shllimm n e1 e2 :=
  if Compopts.optim_addx tt
  then
    match shift1_4_of_z (Int.unsigned n) with
    | Some s14 => Eop (Oaddxl s14) (e1:::e2:::Enil)
    | None => Eop Oaddl (e2:::(Eop (Oshllimm n) (e1:::Enil)):::Enil)
    end
  else Eop Oaddl (e2:::(Eop (Oshllimm n) (e1:::Enil)):::Enil).

Nondetfunction addl (e1: expr) (e2: expr) :=
  if Archi.splitlong then SplitLong.addl e1 e2 else
  match e1, e2 with
  | Eop (Olongconst n1) Enil, t2 => addlimm n1 t2
  | t1, Eop (Olongconst n2) Enil => addlimm n2 t1
  | Eop (Oaddlimm n1) (t1:::Enil), Eop (Oaddlimm n2) (t2:::Enil) =>
      addlimm (Int64.add n1 n2) (Eop Oaddl (t1:::t2:::Enil))
  | Eop (Oaddlimm n1) (t1:::Enil), Eop (Oaddrstack n2) Enil =>
      Eop Oaddl (Eop (Oaddrstack (Ptrofs.add (Ptrofs.of_int64 n1) n2)) Enil ::: t1 ::: Enil)
  | Eop (Oaddrstack n1) Enil, Eop (Oaddlimm n2) (t2:::Enil) =>
      Eop Oaddl (Eop (Oaddrstack (Ptrofs.add n1 (Ptrofs.of_int64 n2))) Enil ::: t2 ::: Enil)
  | Eop (Oaddlimm n1) (t1:::Enil), t2 =>
      addlimm n1 (Eop Oaddl (t1:::t2:::Enil))
  | t1, Eop (Oaddlimm n2) (t2:::Enil) =>
      addlimm n2 (Eop Oaddl (t1:::t2:::Enil))
  | t1, (Eop Omull (t2:::t3:::Enil)) =>
      Eop Omaddl (t1:::t2:::t3:::Enil)
  | (Eop Omull (t2:::t3:::Enil)), t1 =>
      Eop Omaddl (t1:::t2:::t3:::Enil)
  | t1, (Eop (Omullimm n) (t2:::Enil)) =>
      Eop (Omaddlimm n) (t1:::t2:::Enil)
  | (Eop (Omullimm n) (t2:::Enil)), t1 =>
      Eop (Omaddlimm n) (t1:::t2:::Enil)
  | (Eop (Oshllimm n) (t1:::Enil)), t2 =>
    addl_shllimm n t1 t2
  | t2, (Eop (Oshllimm n) (t1:::Enil)) =>
    addl_shllimm n t1 t2
  | _, _ => Eop Oaddl (e1:::e2:::Enil)
  end.

(** ** Integer and pointer subtraction *)

Nondetfunction subl (e1: expr) (e2: expr) :=
  if Archi.splitlong then SplitLong.subl e1 e2 else
  match e1, e2 with
  | t1, Eop (Olongconst n2) Enil =>
      addlimm (Int64.neg n2) t1
  | Eop (Oaddlimm n1) (t1:::Enil), Eop (Oaddlimm n2) (t2:::Enil) =>
      addlimm (Int64.sub n1 n2) (Eop Osubl (t1:::t2:::Enil))
  | Eop (Oaddlimm n1) (t1:::Enil), t2 =>
      addlimm n1 (Eop Osubl (t1:::t2:::Enil))
  | t1, Eop (Oaddlimm n2) (t2:::Enil) =>
      addlimm (Int64.neg n2) (Eop Osubl (t1:::t2:::Enil))
  | t1, (Eop Omull (t2:::t3:::Enil)) =>
      Eop Omsubl (t1:::t2:::t3:::Enil)
  | t1, (Eop (Omullimm n) (t2:::Enil)) =>
      Eop (Omaddlimm (Int64.neg n)) (t1:::t2:::Enil)
  | _, _ => Eop Osubl (e1:::e2:::Enil)
  end.

Definition negl (e: expr) :=
  if Archi.splitlong then SplitLong.negl e else
  match is_longconst e with
  | Some n => longconst (Int64.neg n)
  | None =>  Eop Onegl (e ::: Enil)
  end.

(** ** Immediate shifts *)

Nondetfunction shllimm (e1: expr) (n: int) :=
  if Archi.splitlong then SplitLong.shllimm e1 n else
  if Int.eq n Int.zero then
    e1
  else if negb (Int.ltu n Int64.iwordsize') then
    Eop Oshll (e1 ::: Eop (Ointconst n) Enil ::: Enil)
  else match e1 with
    | Eop (Olongconst n1) Enil =>
        longconst (Int64.shl' n1 n)
    | Eop (Oshllimm n1) (t1:::Enil) =>
        if Int.ltu (Int.add n n1) Int64.iwordsize'
        then Eop (Oshllimm (Int.add n n1)) (t1:::Enil)
        else Eop (Oshllimm n) (e1:::Enil)
    | _ =>
        Eop (Oshllimm n) (e1:::Enil)
  end.

Nondetfunction shrluimm (e1: expr) (n: int) :=
  if Archi.splitlong then SplitLong.shrluimm e1 n else
  if Int.eq n Int.zero then e1 else
  if negb (Int.ltu n Int64.iwordsize') then
    Eop Oshrlu (e1:::Eop (Ointconst n) Enil:::Enil)
  else
    match e1 with
    | Eop (Olongconst n1) Enil =>
        longconst (Int64.shru' n1 n)
    | Eop (Oshrluimm n1) (t1:::Enil) =>
        if Int.ltu (Int.add n n1) Int64.iwordsize'
        then Eop (Oshrluimm (Int.add n n1)) (t1:::Enil)
        else Eop (Oshrluimm n) (e1:::Enil)
    | Eop (Oshllimm n1) (t1:::Enil) =>
        let stop := Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one) in
	let start := Z.sub (Z.add (Z.add (Int.unsigned n) stop) Z.one) Int64.zwordsize in
	if is_bitfieldl stop start
        then Eop (Oextfzl stop start) (t1:::Enil)
	else Eop (Oshrluimm n) (e1:::Enil)
    | _ =>
        Eop (Oshrluimm n) (e1:::Enil)
    end.

Nondetfunction shrlimm (e1: expr) (n: int) :=
  if Archi.splitlong then SplitLong.shrlimm e1 n else
  if Int.eq n Int.zero then e1 else
  if negb (Int.ltu n Int64.iwordsize') then
    Eop Oshrl (e1:::Eop (Ointconst n) Enil:::Enil)
  else
  match e1 with
  | Eop (Olongconst n1) Enil =>
      longconst (Int64.shr' n1 n)
  | Eop (Oshrlimm n1) (t1:::Enil) =>
      if Int.ltu (Int.add n n1) Int64.iwordsize'
      then Eop (Oshrlimm (Int.add n n1)) (t1:::Enil)
      else Eop (Oshrlimm n) (e1:::Enil)
  | Eop (Oshllimm n1) (t1:::Enil) =>
        let stop := Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one) in
	let start := Z.sub (Z.add (Z.add (Int.unsigned n) stop) Z.one) Int64.zwordsize in
	if is_bitfieldl stop start
        then Eop (Oextfsl stop start) (t1:::Enil)
	else Eop (Oshrlimm n) (e1:::Enil)
  | _ =>
      Eop (Oshrlimm n) (e1:::Enil)
  end.

(** ** General shifts *)

Definition shll (e1: expr) (e2: expr) :=
  if Archi.splitlong then SplitLong.shll e1 e2 else
  match is_intconst e2 with
  | Some n2 => shllimm e1 n2
  | None => Eop Oshll (e1:::e2:::Enil)
  end.

Definition shrl (e1: expr) (e2: expr) :=
  if Archi.splitlong then SplitLong.shrl e1 e2 else
  match is_intconst e2 with
  | Some n2 => shrlimm e1 n2
  | None => Eop Oshrl (e1:::e2:::Enil)
  end.

Definition shrlu (e1: expr) (e2: expr) :=
  if Archi.splitlong then SplitLong.shrlu e1 e2 else
  match is_intconst e2 with
  | Some n2 => shrluimm e1 n2
  | _ => Eop Oshrlu (e1:::e2:::Enil)
  end.

(** ** Integer multiply *)

Definition mullimm_base (n1: int64) (e2: expr) :=
  match Int64.one_bits' n1 with
  | i :: nil =>
      shllimm e2 i
  | i :: j :: nil =>
      Elet e2 (addl (shllimm (Eletvar 0) i) (shllimm (Eletvar 0) j))
  | _ =>
      Eop (Omullimm n1) (e2 ::: Enil)
  end.

Nondetfunction mullimm (n1: int64) (e2: expr) :=
  if Archi.splitlong then SplitLong.mullimm n1 e2
  else if Int64.eq n1 Int64.zero then longconst Int64.zero
  else if Int64.eq n1 Int64.one then e2
  else match e2 with
  | Eop (Olongconst n2) Enil => longconst (Int64.mul n1 n2)
  | Eop (Oaddlimm n2) (t2:::Enil) => addlimm (Int64.mul n1 n2) (mullimm_base n1 t2)
  | _ => mullimm_base n1 e2
  end.

Nondetfunction mull (e1: expr) (e2: expr) :=
  if Archi.splitlong then SplitLong.mull e1 e2 else
  match e1, e2 with
  | Eop (Olongconst n1) Enil, t2 => mullimm n1 t2
  | t1, Eop (Olongconst n2) Enil => mullimm n2 t1
  | _, _ => Eop Omull (e1:::e2:::Enil)
  end.

Definition mullhu (e1: expr) (n2: int64) :=
  if Archi.splitlong then SplitLong.mullhu e1 n2 else
  Eop Omullhu (e1 ::: longconst n2 ::: Enil).

Definition mullhs (e1: expr) (n2: int64) :=
  if Archi.splitlong then SplitLong.mullhs e1 n2 else
  Eop Omullhs (e1 ::: longconst n2 ::: Enil).

(** ** Bitwise and, or, xor *)

Nondetfunction andlimm (n1: int64) (e2: expr) := 
  if Int64.eq n1 Int64.zero then longconst Int64.zero else
  if Int64.eq n1 Int64.mone then e2 else
  match e2 with
  | Eop (Olongconst n2) Enil =>
      longconst (Int64.and n1 n2)
  | Eop (Oandlimm n2) (t2:::Enil) =>
      Eop (Oandlimm (Int64.and n1 n2)) (t2:::Enil)
  | Eop Onotl (t2:::Enil) => Eop (Oandnlimm n1) (t2:::Enil)
  | _ =>
      Eop (Oandlimm n1) (e2:::Enil)
  end.

Nondetfunction andl (e1: expr) (e2: expr) :=
  if Archi.splitlong then SplitLong.andl e1 e2 else
  match e1, e2 with
  | Eop (Olongconst n1) Enil, t2 => andlimm n1 t2
  | t1, Eop (Olongconst n2) Enil => andlimm n2 t1
  | (Eop Onotl (t1:::Enil)), t2 => Eop Oandnl (t1:::t2:::Enil) 
  | t1, (Eop Onotl (t2:::Enil)) => Eop Oandnl (t2:::t1:::Enil)
  | _, _ => Eop Oandl (e1:::e2:::Enil)
  end.

Nondetfunction orlimm (n1: int64) (e2: expr) :=
  if Int64.eq n1 Int64.zero then e2 else
  if Int64.eq n1 Int64.mone then longconst Int64.mone else
  match e2 with
  | Eop (Olongconst n2) Enil => longconst (Int64.or n1 n2)
  | Eop (Oorlimm n2) (t2:::Enil) => Eop (Oorlimm (Int64.or n1 n2)) (t2:::Enil)
  | Eop Onotl (t2:::Enil) => Eop (Oornlimm n1) (t2:::Enil)
  | _ => Eop (Oorlimm n1) (e2:::Enil)
  end.

Nondetfunction orl (e1: expr) (e2: expr) :=
  if Archi.splitlong then SplitLong.orl e1 e2 else
  match e1, e2 with
  | Eop (Olongconst n1) Enil, t2 => orlimm n1 t2
  | t1, Eop (Olongconst n2) Enil => orlimm n2 t1
  | (Eop Onotl (t1:::Enil)), t2 => Eop Oornl (t1:::t2:::Enil) 
  | t1, (Eop Onotl (t2:::Enil))  => Eop Oornl (t2:::t1:::Enil)
  | (Eop (Oandlimm nmask) (prev:::Enil)),
    (Eop (Oandlimm mask)
      ((Eop (Oshllimm start) (fld:::Enil)):::Enil)) =>
      let zstart := Int.unsigned start in
      let zstop := int64_highest_bit mask in
      if is_bitfieldl zstop zstart
      then
        let mask' := Int64.repr (zbitfield_mask zstop zstart) in
          if and_dec (Int64.eq_dec mask mask')
                     (Int64.eq_dec nmask (Int64.not mask'))
          then Eop (Oinsfl zstop zstart) (prev:::fld:::Enil)
          else Eop Oorl (e1:::e2:::Enil)
      else Eop Oorl (e1:::e2:::Enil)
  | (Eop (Oandlimm nmask) (prev:::Enil)),
    (Eop (Oandlimm mask) (fld:::Enil)) =>
      let zstart := 0 in
      let zstop := int64_highest_bit mask in
      if is_bitfieldl zstop zstart
      then
        let mask' := Int64.repr (zbitfield_mask zstop zstart) in
          if and_dec (Int64.eq_dec mask mask')
                     (Int64.eq_dec nmask (Int64.not mask'))
          then Eop (Oinsfl zstop zstart) (prev:::fld:::Enil)
          else Eop Oorl (e1:::e2:::Enil)
      else Eop Oorl (e1:::e2:::Enil)
  | _, _ => Eop Oorl (e1:::e2:::Enil)
  end.

Nondetfunction xorlimm (n1: int64) (e2: expr) :=
  if Int64.eq n1 Int64.zero then e2 else
  if Int64.eq n1 Int64.mone
  then Eop Onotl (e2:::Enil)
  else
  match e2 with
  | Eop (Olongconst n2) Enil => longconst (Int64.xor n1 n2)
  | Eop (Oxorlimm n2) (t2:::Enil) =>
      let n := Int64.xor n1 n2 in
      if Int64.eq n Int64.zero then t2 else Eop (Oxorlimm n) (t2:::Enil)
  | _ => Eop (Oxorlimm n1) (e2:::Enil)
  end.

Nondetfunction xorl (e1: expr) (e2: expr) :=
  if Archi.splitlong then SplitLong.xorl e1 e2 else
  match e1, e2 with
  | Eop (Olongconst n1) Enil, t2 => xorlimm n1 t2
  | t1, Eop (Olongconst n2) Enil => xorlimm n2 t1
  | _, _ => Eop Oxorl (e1:::e2:::Enil)
  end.

(** ** Integer logical negation *)

Nondetfunction notl (e: expr) :=
  match e with
  | Eop Oandl (e1:::e2:::Enil) => Eop Onandl (e1:::e2:::Enil)
  | Eop (Oandlimm n) (e1:::Enil) => Eop (Onandlimm n) (e1:::Enil)
  | Eop Oorl (e1:::e2:::Enil) => Eop Onorl (e1:::e2:::Enil)
  | Eop (Oorlimm n) (e1:::Enil) => Eop (Onorlimm n) (e1:::Enil)
  | Eop Oxorl (e1:::e2:::Enil) => Eop Onxorl (e1:::e2:::Enil)
  | Eop (Oxorlimm n) (e1:::Enil) => Eop (Onxorlimm n) (e1:::Enil)
  | Eop Onandl (e1:::e2:::Enil) => Eop Oandl (e1:::e2:::Enil)
  | Eop (Onandlimm n) (e1:::Enil) => Eop (Oandlimm n) (e1:::Enil)
  | Eop Onorl (e1:::e2:::Enil) => Eop Oorl (e1:::e2:::Enil)
  | Eop (Onorlimm n) (e1:::Enil) => Eop (Oorlimm n) (e1:::Enil)
  | Eop Onxorl (e1:::e2:::Enil) => Eop Oxorl (e1:::e2:::Enil)
  | Eop (Onxorlimm n) (e1:::Enil) => Eop (Oxorlimm n) (e1:::Enil)
  | Eop Oandnl (e1:::e2:::Enil) => Eop Oornl (e2:::e1:::Enil)
  | Eop (Oandnlimm n) (e1:::Enil) => Eop (Oorlimm (Int64.not n)) (e1:::Enil)
  | Eop Oornl (e1:::e2:::Enil) => Eop Oandnl (e2:::e1:::Enil)
  | Eop (Oornlimm n) (e1:::Enil) => Eop (Oandlimm (Int64.not n)) (e1:::Enil)
  | Eop Onotl (e1:::Enil) => e1
  | Eop (Olongconst k) Enil => Eop (Olongconst (Int64.not k)) Enil
  | _ => Eop Onotl (e:::Enil) 
  end.
(* old:  if Archi.splitlong then SplitLong.notl e else xorlimm Int64.mone e. *)

(** ** Integer division and modulus *)

Definition divlu_base (e1: expr) (e2: expr) := SplitLong.divlu_base e1 e2.
Definition modlu_base (e1: expr) (e2: expr) := SplitLong.modlu_base e1 e2.
Definition divls_base (e1: expr) (e2: expr) := SplitLong.divls_base e1 e2.
Definition modls_base (e1: expr) (e2: expr) := SplitLong.modls_base e1 e2.

Definition shrxlimm (e: expr) (n: int) :=
  if Archi.splitlong then SplitLong.shrxlimm e n else
  if Int.eq n Int.zero then e else Eop (Oshrxlimm n) (e ::: Enil).

(** ** Comparisons *)

Definition cmplu (c: comparison) (e1 e2: expr) :=
  if Archi.splitlong then SplitLong.cmplu c e1 e2 else
  match is_longconst e1, is_longconst e2 with
  | Some n1, Some n2 =>
      Eop (Ointconst (if Int64.cmpu c n1 n2 then Int.one else Int.zero)) Enil
  | Some n1, None => Eop (Ocmp (Ccompluimm (swap_comparison c) n1)) (e2:::Enil)
  | None, Some n2 => Eop (Ocmp (Ccompluimm c n2)) (e1:::Enil)
  | None, None => Eop (Ocmp (Ccomplu c)) (e1:::e2:::Enil)
  end.

Definition cmpl (c: comparison) (e1 e2: expr) :=
  if Archi.splitlong then SplitLong.cmpl c e1 e2 else
  match is_longconst e1, is_longconst e2 with
  | Some n1, Some n2 =>
      Eop (Ointconst (if Int64.cmp c n1 n2 then Int.one else Int.zero)) Enil
  | Some n1, None => Eop (Ocmp (Ccomplimm (swap_comparison c) n1)) (e2:::Enil)
  | None, Some n2 => Eop (Ocmp (Ccomplimm c n2)) (e1:::Enil)
  | None, None => Eop (Ocmp (Ccompl c)) (e1:::e2:::Enil)
  end.

(** ** Floating-point conversions *)

Definition longoffloat (e: expr) :=
  Eop Olongoffloat (e:::Enil).

Definition longuoffloat (e: expr) :=
  Eop Olonguoffloat (e:::Enil).

Definition floatoflong (e: expr) := 
  Eop Ofloatoflong (e:::Enil).

Definition floatoflongu (e: expr) := 
  Eop Ofloatoflongu (e:::Enil).

Definition longofsingle (e: expr) := longoffloat (floatofsingle e).

Definition longuofsingle (e: expr) := longuoffloat (floatofsingle e).

Definition use_inlined_fp_conversions := true.
Opaque use_inlined_fp_conversions.

Definition singleoflong (e: expr) :=
  if use_inlined_fp_conversions
  then FPExtra.e_single_of_long e
  else SplitLong.singleoflong e.

Definition singleoflongu (e: expr) :=
  if use_inlined_fp_conversions
  then FPExtra.e_single_of_longu e
  else SplitLong.singleoflongu e.

End SELECT.

(* Local Variables: *)
(* mode: coq *)
(* End: *)