include "Clight/Csyntax.ma".
include "Clight/TypeComparison.ma".

(* Attempt to remove unnecessary integer casts in Clight programs.

   This differs from the OCaml prototype by attempting to recursively determine
   whether subexpressions can be changed rather than using a fixed size pattern.
   As a result more complex expressions such as (char)((int)x + (int)y + (int)z)
   where x,y and z are chars can be simplified.
   
   A possible improvement that doesn't quite fit into this scheme would be to
   spot that casts can be removed in expressions like (int)x == (int)y where
   x and y have some smaller integer type.
 *)

(* Attempt to squeeze integer constant into a given type.

   This might be too conservative --- if we're going to cast it anyway, can't
   I just ignore the fact that the integer doesn't fit?
 *)

let rec reduce_bits (n,m:nat) (exp:bool) (v:BitVector (plus n (S m))) on n : option (BitVector (S m)) ≝
match n return λn. BitVector (n+S m) → option (BitVector (S m)) with
[ O ⇒ λv. Some ? v
| S n' ⇒ λv. if eq_b (head' ?? v) exp then reduce_bits ?? exp (tail ?? v) else None ?
] v.

definition pred_bitsize_of_intsize : intsize → nat ≝
λsz. match sz with [ I8 ⇒ 7 | I16 ⇒ 15 | I32 ⇒ 31 ].

definition signed : signedness → bool ≝
λsg. match sg with [ Unsigned ⇒ false | Signed ⇒ true ].

let rec simplify_int (sz,sz':intsize) (sg,sg':signedness) (i:bvint sz) : option (bvint sz') ≝
  let bit ≝ signed sg ∧ head' … i in
  match nat_compare (pred_bitsize_of_intsize sz) (pred_bitsize_of_intsize sz')
      return λn,m,x.BitVector (S n) → option (BitVector (S m)) with
  [ nat_lt _ _ ⇒ λi. None ?   (* refuse to make constants larger *)
  | nat_eq _ ⇒ λi. Some ? i
  | nat_gt x y ⇒ λi.
      match reduce_bits ?? bit (i⌈BitVector (S (y+S x))↦BitVector ((S x) + (S y))⌉) with
      [ Some i' ⇒ if signed sg' then if eq_b bit (head' … i') then Some ? i' else None ? else Some ? i'
      | None ⇒ None ?
      ]
  ] i.
>(commutative_plus_faster (S x)) @refl
qed.

(* Compare integer types to decide if we can omit casts. *)

inductive inttype_cmp : Type[0] ≝
| itc_le : inttype_cmp
| itc_no : inttype_cmp.

definition inttype_compare ≝
λt1,t2.
match t1 with
[ Tint sz sg ⇒
  match t2 with
  [ Tint sz' sg' ⇒
      match sz with
      [ I8 ⇒ itc_le
      | I16 ⇒ match sz' with [ I8 ⇒ itc_no | _ ⇒ itc_le ]
      | I32 ⇒ match sz' with [ I32 ⇒ itc_le | _ ⇒ itc_no ]
      ]
  | _ ⇒ itc_no
  ]
| _ ⇒ itc_no
].

(* Operations where it is safe to use a smaller integer type on the assumption
   that we would cast it down afterwards anyway. *)

definition binop_simplifiable ≝
λop. match op with [ Oadd ⇒ true | Osub ⇒ true | _ ⇒ false ].

(* simplify_expr [e] [ty'] takes an expression e and a desired type ty', and
   returns a flag stating whether the desired type was achieved and a simplified
   version of e. *)

let rec simplify_expr (e:expr) (ty':type) : bool × expr ≝
match e with
[ Expr ed ty ⇒
  match ed with
  [ Econst_int sz i ⇒
    match ty with
    [ Tint _ sg ⇒
      match ty' with
      [ Tint sz' sg' ⇒
        match simplify_int sz sz' sg sg' i with
        [ Some i' ⇒ 〈true, Expr (Econst_int sz' i') ty'〉
        | None ⇒ 〈false, e〉
        ]
      | _ ⇒ 〈false, e〉 ]
    | _ ⇒ 〈false, e〉 ]
  | Ederef e1 ⇒
      let ty1 ≝ typeof e1 in
      〈type_eq ty ty',Expr (Ederef (\snd (simplify_expr e1 ty1))) ty〉
  | Eaddrof e1 ⇒
      let ty1 ≝ typeof e1 in
      〈type_eq ty ty',Expr (Eaddrof (\snd (simplify_expr e1 ty1))) ty〉
  | Eunop op e1 ⇒
      let ty1 ≝ typeof e1 in
      〈type_eq ty ty',Expr (Eunop op (\snd (simplify_expr e1 ty1))) ty〉
  | Ebinop op e1 e2 ⇒
      if binop_simplifiable op then
        let 〈desired_type1, e1'〉 ≝ simplify_expr e1 ty' in
        let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty' in
        if desired_type1 ∧ desired_type2 then
          〈true, Expr (Ebinop op e1' e2') ty'〉
        else
          let 〈desired_type1, e1'〉 ≝ simplify_expr e1 ty in
          let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty in
            〈false, Expr (Ebinop op e1' e2') ty〉
      else
        let 〈desired_type1, e1'〉 ≝ simplify_expr e1 ty in
        let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty in
          〈type_eq ty ty', Expr (Ebinop op e1' e2') ty〉
  | Ecast ty e1 ⇒
      match inttype_compare ty' ty with
      [ itc_le ⇒
        let 〈desired_type, e1'〉 ≝ simplify_expr e1 ty' in
        if desired_type then 〈true, e1'〉 else 
          let 〈desired_type, e1'〉 ≝ simplify_expr e1 ty in
          if desired_type then 〈false, e1'〉 else 〈false, Expr (Ecast ty e1') ty〉
      | itc_no ⇒
        let 〈desired_type, e1'〉 ≝ simplify_expr e1 ty in
        if desired_type then 〈false, e1'〉 else 〈false, Expr (Ecast ty e1') ty〉
      ]
  | Econdition e1 e2 e3 ⇒
      let 〈irrelevant, e1'〉 ≝ simplify_expr e1 (typeof e1) in (* TODO try to reduce size *)
      let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty' in
      let 〈desired_type3, e3'〉 ≝ simplify_expr e3 ty' in
      if desired_type2 ∧ desired_type3 then
        〈true, Expr (Econdition e1' e2' e3') ty'〉
      else
        let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty in
        let 〈desired_type3, e3'〉 ≝ simplify_expr e3 ty in
          〈false, Expr (Econdition e1' e2' e3') ty〉
    (* Could probably do better with these, too. *)
  | Eandbool e1 e2 ⇒
      let 〈desired_type1, e1'〉 ≝ simplify_expr e1 ty in
      let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty in
        〈type_eq ty ty', Expr (Eandbool e1' e2') ty〉
  | Eorbool e1 e2 ⇒
      let 〈desired_type1, e1'〉 ≝ simplify_expr e1 ty in
      let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty in
        〈type_eq ty ty', Expr (Eorbool e1' e2') ty〉
  (* Could also improve Esizeof *)
  | Efield e1 f ⇒
      let ty1 ≝ typeof e1 in
      〈type_eq ty ty',Expr (Efield (\snd (simplify_expr e1 ty1)) f) ty〉
  | Ecost l e1 ⇒
      let 〈desired_type, e1'〉 ≝ simplify_expr e1 ty' in
        〈desired_type, Expr (Ecost l e1') (typeof e1')〉
  | _ ⇒ 〈type_eq ty ty',e〉
  ]
].

definition simplify_e ≝ λe. \snd (simplify_expr e (typeof e)).

let rec simplify_statement (s:statement) : statement ≝
match s with
[ Sskip ⇒ Sskip
| Sassign e1 e2 ⇒ Sassign (simplify_e e1) (simplify_e e2)
| Scall eo e es ⇒ Scall (option_map ?? simplify_e eo) (simplify_e e) (map ?? simplify_e es)
| Ssequence s1 s2 ⇒ Ssequence (simplify_statement s1) (simplify_statement s2)
| Sifthenelse e s1 s2 ⇒ Sifthenelse (simplify_e e) (simplify_statement s1) (simplify_statement s2) (* TODO: try to reduce size of e *)
| Swhile e s1 ⇒ Swhile (simplify_e e) (simplify_statement s1) (* TODO: try to reduce size of e *)
| Sdowhile e s1 ⇒ Sdowhile (simplify_e e) (simplify_statement s1) (* TODO: try to reduce size of e *)
| Sfor s1 e s2 s3 ⇒ Sfor (simplify_statement s1) (simplify_e e) (simplify_statement s2) (simplify_statement s3) (* TODO: reduce size of e *)
| Sbreak ⇒ Sbreak
| Scontinue ⇒ Scontinue
| Sreturn eo ⇒ Sreturn (option_map ?? simplify_e eo)
| Sswitch e ls ⇒ Sswitch (simplify_e e) (simplify_ls ls)
| Slabel l s1 ⇒ Slabel l (simplify_statement s1)
| Sgoto l ⇒ Sgoto l
| Scost l s1 ⇒ Scost l (simplify_statement s1)
]
and simplify_ls ls ≝
match ls with
[ LSdefault s ⇒ LSdefault (simplify_statement s)
| LScase sz i s ls' ⇒ LScase sz i (simplify_statement s) (simplify_ls ls')
].

definition simplify_function : function → function ≝
λf. mk_function (fn_return f) (fn_params f) (fn_vars f) (simplify_statement (fn_body f)).

definition simplify_fundef : clight_fundef → clight_fundef ≝
λf. match f with
  [ CL_Internal f ⇒ CL_Internal (simplify_function f)
  | _ ⇒ f
  ].

definition simplify_program : clight_program → clight_program ≝
λp. transform_program … p simplify_fundef.