(** [simplify p] removes unnecessary casts in the Clight program [p].

    Example: [(char) ((int)x + (int)y)] where [x] and [y] are of type [char]
    will be transformed into [x + y]. Primitive operations are thus supposed to
    be polymorphic, but working only on homogene types. *)


let error_prefix = "Clight casts simplification"
let error = Error.global_error error_prefix
let error_float () = error "float not supported."


(* Int sizes *)

let int_of_intsize = function
  | Clight.I8 -> 8
  | Clight.I16 -> 16
  | Clight.I32 -> 32

let intsize_of_int = function
  | i when i <= 8 -> Clight.I8
  | i when i <= 16 -> Clight.I16
  | _ -> Clight.I32

let op_intsize_no_cast op size1 size2 =
  op (int_of_intsize size1) (int_of_intsize size2)

let cmp_intsize cmp size1 size2 = op_intsize_no_cast cmp size1 size2

let op_intsize op size1 size2 =
  intsize_of_int (op_intsize_no_cast op size1 size2)

let max_intsize size1 size2 = op_intsize max size1 size2

let intsize_union size1 size2 = op_intsize (+) size1 size2

let pow2 = MiscPottier.pow 2

let belongs_to_int_type size sign i = match size, sign with
  | Clight.I8, AST.Unsigned -> 0 <= i && i <= (pow2 8) - 1
  | Clight.I8, AST.Signed -> -(pow2 7) <= i && i <= (pow2 7) - 1
  | Clight.I16, AST.Unsigned -> 0 <= i && i <= (pow2 16) - 1
  | Clight.I16, AST.Signed -> -(pow2 15) <= i && i <= (pow2 15) - 1
  | Clight.I32, AST.Unsigned -> 0 <= i
  | Clight.I32, AST.Signed ->
    let pow2_30 = pow2 30 in
    (-(pow2_30 + pow2_30)) <= i &&
    i <= ((pow2_30 - 1) + pow2_30) (* = 2^31 - 1 *)

let smallest_int_type i =
  let (size, sign) = match i with
  | _ when belongs_to_int_type Clight.I8 AST.Signed i ->
    (Clight.I8, AST.Signed)
  | _ when belongs_to_int_type Clight.I8 AST.Unsigned i ->
    (Clight.I8, AST.Unsigned)
  | _ when belongs_to_int_type Clight.I16 AST.Signed i ->
    (Clight.I16, AST.Signed)
  | _ when belongs_to_int_type Clight.I16 AST.Unsigned i ->
    (Clight.I16, AST.Unsigned)
  | _ when belongs_to_int_type Clight.I32 AST.Unsigned i ->
    (Clight.I32, AST.Unsigned)
  | _ ->
    (Clight.I32, AST.Signed) in
  Clight.Tint (size, sign)

let le_int_type size1 sign1 size2 sign2 = match sign1, sign2 with
  | AST.Unsigned, AST.Signed -> cmp_intsize (<) size1 size2
  | AST.Signed, AST.Unsigned -> false
  | _ -> cmp_intsize (<=) size1 size2

let int_type_union size1 sign1 size2 sign2 =
  if sign1 = sign2 then (max_intsize size1 size2, sign1)
  else (intsize_union size1 size2, AST.Signed)


(* C types *)

let type_of_expr (Clight.Expr (_, t)) = t

let cast_if_needed t (Clight.Expr (ed, t') as e) = match t, ed with
  | _ when t = t' -> e
  | Clight.Tint (size, sign), Clight.Econst_int i
    when belongs_to_int_type size sign i ->
    Clight.Expr (Clight.Econst_int i, t)
  | _ -> Clight.Expr (Clight.Ecast (t, e), t)

let cast_if_needed_opt opt_t e = match opt_t with
  | None -> e
  | Some t -> cast_if_needed t e

let is_int_type = function
  | Clight.Tint _ -> true
  | _ -> false

let le_ctype t1 t2 = match t1, t2 with
  | Clight.Tint (size1, sign1), Clight.Tint (size2, sign2) ->
    le_int_type size1 sign1 size2 sign2
  | _ -> t1 = t2

let ctype_union t1 t2 = match t1, t2 with
  | Clight.Tint (size1, sign1), Clight.Tint (size2, sign2) ->
    let (size, sign) = int_type_union size1 sign1 size2 sign2 in
    Clight.Tint (size, sign)
  | _ -> assert false (* only use on int types *)

let belongs_to_ctype t i = match t with
  | Clight.Tint (size, sign) -> belongs_to_int_type size sign i
  | _ -> false


(* Simplification *)

let rec is_const_int (Clight.Expr (ed, _)) = match ed with
  | Clight.Econst_int _ -> true
  | Clight.Ecast (_, e) | Clight.Ecost (_, e) -> is_const_int e
  | _ -> false

let rec simplify_bool_op f_bool target_t e1 e2 =
  let (e1', e2', t') = simplify_and_same_type target_t e1 e2 in
  Clight.Expr (f_bool e1' e2', t')

and simplify_and_same_type target_t e1 e2 = match target_t with

  | None when is_const_int e1 && is_const_int e2 ->
    let e1' = simplify_expr target_t e1 in
    let t1 = type_of_expr e1' in
    let e2' = simplify_expr target_t e2 in
    let t2 = type_of_expr e2' in
    if is_int_type t1 && is_int_type t2 then
      let t = ctype_union t1 t2 in
      let e1' = cast_if_needed t e1' in
      let e2' = cast_if_needed t e2' in
      (e1', e2', t)
    else (e1, e2, type_of_expr e1)

  | None when is_const_int e1 ->
    let e2 = simplify_expr target_t e2 in
    let t2 = type_of_expr e2 in
    let e1 = simplify_expr (Some t2) e1 in
    (e1, e2, t2)

  | None when is_const_int e2 ->
    let e1 = simplify_expr target_t e1 in
    let t1 = type_of_expr e1 in
    let e2 = simplify_expr (Some t1) e2 in
    (e1, e2, t1)

  | _ ->
    let e1' = simplify_expr target_t e1 in
    let t1 = type_of_expr e1' in
    let e2' = simplify_expr target_t e2 in
    let t2 = type_of_expr e2' in
    if t1 = t2 then (e1', e2', t1)
    else (e1, e2, type_of_expr e1)

and simplify_expr target_t (Clight.Expr (ed, t) as e) = match target_t, ed with

  | None, Clight.Econst_int i ->
    let t' = smallest_int_type i in
    Clight.Expr (ed, t')

  | Some t', Clight.Econst_int i when belongs_to_ctype t' i ->
    Clight.Expr (ed, t')

  | Some t', Clight.Econst_int _ -> cast_if_needed t' e

  | _, Clight.Evar _ -> cast_if_needed_opt target_t e

  | _, Clight.Esizeof _ ->
    let i = Driver.TargetArch.int_size * 8 in
    let t = smallest_int_type i in
    cast_if_needed_opt target_t (Clight.Expr (ed, t))

  | _, Clight.Econst_float _ -> error_float ()

  | _, Clight.Ederef e ->
    let e' = simplify_expr (Some (Clight.Tpointer t)) e in
    cast_if_needed_opt target_t (Clight.Expr (Clight.Ederef e', t))

  | _, Clight.Eaddrof e ->
    let e' = simplify_expr None e in
    let e' =
      Clight.Expr (Clight.Eaddrof e', Clight.Tpointer (type_of_expr e')) in
    cast_if_needed_opt target_t e'

  | _, Clight.Eunop (unop, e) ->
    let e' = simplify_expr target_t e in
    Clight.Expr (Clight.Eunop (unop, e'), type_of_expr e')

  (* Particular case: shifts. The first argument will always be casted to int by
     CIL (except for unsigned int, treated in another pattern). *)
  (* TODO: is above really true?! *)
  (* [(_) e1 >> e2], when [e1] and [e2] simplified have the same type, is
     simplified to [e1 >> e2] (and respectively with [<<]). *)
  | _, Clight.Ebinop ((Clight.Oshl | Clight.Oshr) as binop,
		      Clight.Expr (Clight.Ecast (_, e1), _), e2) ->
    let e1 = simplify_expr target_t e1 in
    let t1 = type_of_expr e1 in
    let e2 = simplify_expr target_t e2 in
    let t2 = type_of_expr e2 in
    if t1 = t2 then Clight.Expr (Clight.Ebinop (binop, e1, e2), t1)
    else cast_if_needed_opt target_t e

  | _, Clight.Ebinop (binop, e1, e2)
    when is_int_type (type_of_expr e1) && is_int_type (type_of_expr e2) ->
    let (e1, e2, t) = simplify_and_same_type target_t e1 e2 in
    cast_if_needed_opt target_t (Clight.Expr (Clight.Ebinop (binop, e1, e2), t))

  | _, Clight.Ebinop (binop, e1, e2) ->
    let e1' = cast_if_needed (type_of_expr e1) (simplify_expr None e1) in
    let e2' = cast_if_needed (type_of_expr e2) (simplify_expr None e2) in
    Clight.Expr (Clight.Ebinop (binop, e1', e2'), t)

  | _, Clight.Ecast (_, e) -> simplify_expr target_t e

  | _, Clight.Econdition (e1, e2, e3) ->
    let e1' = simplify_expr None e1 in
    let (e2', e3', t') = simplify_and_same_type target_t e2 e3 in
    Clight.Expr (Clight.Econdition (e1', e2', e3'), t')

  | _, Clight.Eandbool (e1, e2) ->
    simplify_bool_op (fun e1' e2' -> Clight.Eandbool (e1', e2')) target_t e1 e2

  | _, Clight.Eorbool (e1, e2) ->
    simplify_bool_op (fun e1' e2' -> Clight.Eorbool (e1', e2')) target_t e1 e2

  | _, Clight.Efield (e, field) ->
    let e' = simplify_expr (Some (type_of_expr e)) e in
    cast_if_needed_opt target_t (Clight.Expr (Clight.Efield (e', field), t))

  | _, Clight.Ecost (lbl, e) ->
    let e' = simplify_expr target_t e in
    Clight.Expr (Clight.Ecost (lbl, e'), type_of_expr e')

  | _, Clight.Ecall _ ->
    assert false (* should be impossible *)


let f_ctype ctype _ = ctype

let f_expr e _ _ = e

let f_expr_descr e _ _ =  e

let f_statement stmt _ sub_stmts_res =
  let f_expr b e =
    simplify_expr (if b then Some (type_of_expr e) else None) e in
  let f_exprs b = List.map (f_expr b) in
  let f_sub_exprs = match stmt with
    | Clight.Sassign _ | Clight.Scall _ | Clight.Sreturn _ -> f_exprs true
    | _ -> f_exprs false in
  let sub_exprs = f_sub_exprs (ClightFold.statement_sub_exprs stmt) in
  ClightFold.statement_fill_subs stmt sub_exprs sub_stmts_res

let simplify_stmt = ClightFold.statement f_ctype f_expr f_expr_descr f_statement

let simplify_funct (id, fundef) =
  let fundef' = match fundef with
    | Clight.Internal cfun ->
      Clight.Internal
	{ cfun with Clight.fn_body = simplify_stmt cfun.Clight.fn_body }
    | _ -> fundef in
  (id, fundef')

let simplify p =
  { p with Clight.prog_funct = List.map simplify_funct p.Clight.prog_funct }

(* TODO: restore above, but buggy with
   (unsigned int) (-x) -> - ((unsigned int) x) *)

(*
let simplify p = p
*)