src/clight/clightCasts.ml

   1
   2 (** [simplify p] removes unnecessary casts in the Clight program [p].
   3
   4     Example: [(char) ((int)x + (int)y)] where [x] and [y] are of type [char]
   5     will be transformed into [x + y]. Primitive operations are thus supposed to
   6     be polymorphic, but working only on homogene types. *)
   7
   8
   9 let error_prefix = "Clight casts simplification"
  10 let error = Error.global_error error_prefix
  11 let error_float () = error "float not supported."
  12
  13
  14 (* Int sizes *)
  15
  16 let int_of_intsize = function
  17   | Clight.I8 -> 8
  18   | Clight.I16 -> 16
  19   | Clight.I32 -> 32
  20
  21 let intsize_of_int = function
  22   | i when i <= 8 -> Clight.I8
  23   | i when i <= 16 -> Clight.I16
  24   | _ -> Clight.I32
  25
  26 let op_intsize_no_cast op size1 size2 =
  27   op (int_of_intsize size1) (int_of_intsize size2)
  28
  29 let cmp_intsize cmp size1 size2 = op_intsize_no_cast cmp size1 size2
  30
  31 let op_intsize op size1 size2 =
  32   intsize_of_int (op_intsize_no_cast op size1 size2)
  33
  34 let max_intsize size1 size2 = op_intsize max size1 size2
  35
  36 let intsize_union size1 size2 = op_intsize (+) size1 size2
  37
  38 let pow2 = MiscPottier.pow 2
  39
  40 let belongs_to_int_type size sign i = match size, sign with
  41   | Clight.I8, AST.Unsigned -> 0 <= i && i <= (pow2 8) - 1
  42   | Clight.I8, AST.Signed -> -(pow2 7) <= i && i <= (pow2 7) - 1
  43   | Clight.I16, AST.Unsigned -> 0 <= i && i <= (pow2 16) - 1
  44   | Clight.I16, AST.Signed -> -(pow2 15) <= i && i <= (pow2 15) - 1
  45   | Clight.I32, AST.Unsigned -> 0 <= i
  46   | Clight.I32, AST.Signed ->
  47     let pow2_30 = pow2 30 in
  48     (-(pow2_30 + pow2_30)) <= i &&
  49     i <= ((pow2_30 - 1) + pow2_30) (* = 2^31 - 1 *)
  50
  51 let smallest_int_type i =
  52   let (size, sign) = match i with
  53   | _ when belongs_to_int_type Clight.I8 AST.Signed i ->
  54     (Clight.I8, AST.Signed)
  55   | _ when belongs_to_int_type Clight.I8 AST.Unsigned i ->
  56     (Clight.I8, AST.Unsigned)
  57   | _ when belongs_to_int_type Clight.I16 AST.Signed i ->
  58     (Clight.I16, AST.Signed)
  59   | _ when belongs_to_int_type Clight.I16 AST.Unsigned i ->
  60     (Clight.I16, AST.Unsigned)
  61   | _ when belongs_to_int_type Clight.I32 AST.Unsigned i ->
  62     (Clight.I32, AST.Unsigned)
  63   | _ ->
  64     (Clight.I32, AST.Signed) in
  65   Clight.Tint (size, sign)
  66
  67 let le_int_type size1 sign1 size2 sign2 = match sign1, sign2 with
  68   | AST.Unsigned, AST.Signed -> cmp_intsize (<) size1 size2
  69   | AST.Signed, AST.Unsigned -> false
  70   | _ -> cmp_intsize (<=) size1 size2
  71
  72 let int_type_union size1 sign1 size2 sign2 =
  73   if sign1 = sign2 then (max_intsize size1 size2, sign1)
  74   else (intsize_union size1 size2, AST.Signed)
  75
  76
  77 (* C types *)
  78
  79 let type_of_expr (Clight.Expr (_, t)) = t
  80
  81 let cast_if_needed t (Clight.Expr (ed, t') as e) = match t, ed with
  82   | _ when t = t' -> e
  83   | Clight.Tint (size, sign), Clight.Econst_int i
  84     when belongs_to_int_type size sign i ->
  85     Clight.Expr (Clight.Econst_int i, t)
  86   | _ -> Clight.Expr (Clight.Ecast (t, e), t)
  87
  88 let cast_if_needed_opt opt_t e = match opt_t with
  89   | None -> e
  90   | Some t -> cast_if_needed t e
  91
  92 let is_int_type = function
  93   | Clight.Tint _ -> true
  94   | _ -> false
  95
  96 let le_ctype t1 t2 = match t1, t2 with
  97   | Clight.Tint (size1, sign1), Clight.Tint (size2, sign2) ->
  98     le_int_type size1 sign1 size2 sign2
  99   | _ -> t1 = t2
 100
 101 let ctype_union t1 t2 = match t1, t2 with
 102   | Clight.Tint (size1, sign1), Clight.Tint (size2, sign2) ->
 103     let (size, sign) = int_type_union size1 sign1 size2 sign2 in
 104     Clight.Tint (size, sign)
 105   | _ -> assert false (* only use on int types *)
 106
 107 let belongs_to_ctype t i = match t with
 108   | Clight.Tint (size, sign) -> belongs_to_int_type size sign i
 109   | _ -> false
 110
 111
 112 (* Simplification *)
 113
 114 let rec is_const_int (Clight.Expr (ed, _)) = match ed with
 115   | Clight.Econst_int _ -> true
 116   | Clight.Ecast (_, e) | Clight.Ecost (_, e) -> is_const_int e
 117   | _ -> false
 118
 119 let rec simplify_bool_op f_bool target_t e1 e2 =
 120   let (e1', e2', t') = simplify_and_same_type target_t e1 e2 in
 121   Clight.Expr (f_bool e1' e2', t')
 122
 123 and simplify_and_same_type target_t e1 e2 = match target_t with
 124
 125   | None when is_const_int e1 && is_const_int e2 ->
 126     let e1' = simplify_expr target_t e1 in
 127     let t1 = type_of_expr e1' in
 128     let e2' = simplify_expr target_t e2 in
 129     let t2 = type_of_expr e2' in
 130     if is_int_type t1 && is_int_type t2 then
 131       let t = ctype_union t1 t2 in
 132       let e1' = cast_if_needed t e1' in
 133       let e2' = cast_if_needed t e2' in
 134       (e1', e2', t)
 135     else (e1, e2, type_of_expr e1)
 136
 137   | None when is_const_int e1 ->
 138     let e2 = simplify_expr target_t e2 in
 139     let t2 = type_of_expr e2 in
 140     let e1 = simplify_expr (Some t2) e1 in
 141     (e1, e2, t2)
 142
 143   | None when is_const_int e2 ->
 144     let e1 = simplify_expr target_t e1 in
 145     let t1 = type_of_expr e1 in
 146     let e2 = simplify_expr (Some t1) e2 in
 147     (e1, e2, t1)
 148
 149   | _ ->
 150     let e1' = simplify_expr target_t e1 in
 151     let t1 = type_of_expr e1' in
 152     let e2' = simplify_expr target_t e2 in
 153     let t2 = type_of_expr e2' in
 154     if t1 = t2 then (e1', e2', t1)
 155     else (e1, e2, type_of_expr e1)
 156
 157 and simplify_expr target_t (Clight.Expr (ed, t) as e) = match target_t, ed with
 158
 159   | None, Clight.Econst_int i ->
 160     let t' = smallest_int_type i in
 161     Clight.Expr (ed, t')
 162
 163   | Some t', Clight.Econst_int i when belongs_to_ctype t' i ->
 164     Clight.Expr (ed, t')
 165
 166   | Some t', Clight.Econst_int _ -> cast_if_needed t' e
 167
 168   | _, Clight.Evar _ -> cast_if_needed_opt target_t e
 169
 170   | _, Clight.Esizeof _ ->
 171     let i = Driver.TargetArch.int_size * 8 in
 172     let t = smallest_int_type i in
 173     cast_if_needed_opt target_t (Clight.Expr (ed, t))
 174
 175   | _, Clight.Econst_float _ -> error_float ()
 176
 177   | _, Clight.Ederef e ->
 178     let e' = simplify_expr (Some (Clight.Tpointer t)) e in
 179     cast_if_needed_opt target_t (Clight.Expr (Clight.Ederef e', t))
 180
 181   | _, Clight.Eaddrof e ->
 182     let e' = simplify_expr None e in
 183     let e' =
 184       Clight.Expr (Clight.Eaddrof e', Clight.Tpointer (type_of_expr e')) in
 185     cast_if_needed_opt target_t e'
 186
 187   | _, Clight.Eunop (unop, e) ->
 188     let e' = simplify_expr target_t e in
 189     Clight.Expr (Clight.Eunop (unop, e'), type_of_expr e')
 190
 191   (* Particular case: shifts. The first argument will always be casted to int by
 192      CIL (except for unsigned int, treated in another pattern). *)
 193   (* TODO: is above really true?! *)
 194   (* [(_) e1 >> e2], when [e1] and [e2] simplified have the same type, is
 195      simplified to [e1 >> e2] (and respectively with [<<]). *)
 196   | _, Clight.Ebinop ((Clight.Oshl | Clight.Oshr) as binop,
 197                       Clight.Expr (Clight.Ecast (_, e1), _), e2) ->
 198     let e1 = simplify_expr target_t e1 in
 199     let t1 = type_of_expr e1 in
 200     let e2 = simplify_expr target_t e2 in
 201     let t2 = type_of_expr e2 in
 202     if t1 = t2 then Clight.Expr (Clight.Ebinop (binop, e1, e2), t1)
 203     else cast_if_needed_opt target_t e
 204
 205   | _, Clight.Ebinop (binop, e1, e2)
 206     when is_int_type (type_of_expr e1) && is_int_type (type_of_expr e2) ->
 207     let (e1, e2, t) = simplify_and_same_type target_t e1 e2 in
 208     cast_if_needed_opt target_t (Clight.Expr (Clight.Ebinop (binop, e1, e2), t))
 209
 210   | _, Clight.Ebinop (binop, e1, e2) ->
 211     let e1' = cast_if_needed (type_of_expr e1) (simplify_expr None e1) in
 212     let e2' = cast_if_needed (type_of_expr e2) (simplify_expr None e2) in
 213     Clight.Expr (Clight.Ebinop (binop, e1', e2'), t)
 214
 215   | _, Clight.Ecast (_, e) -> simplify_expr target_t e
 216
 217   | _, Clight.Econdition (e1, e2, e3) ->
 218     let e1' = simplify_expr None e1 in
 219     let (e2', e3', t') = simplify_and_same_type target_t e2 e3 in
 220     Clight.Expr (Clight.Econdition (e1', e2', e3'), t')
 221
 222   | _, Clight.Eandbool (e1, e2) ->
 223     simplify_bool_op (fun e1' e2' -> Clight.Eandbool (e1', e2')) target_t e1 e2
 224
 225   | _, Clight.Eorbool (e1, e2) ->
 226     simplify_bool_op (fun e1' e2' -> Clight.Eorbool (e1', e2')) target_t e1 e2
 227
 228   | _, Clight.Efield (e, field) ->
 229     let e' = simplify_expr (Some (type_of_expr e)) e in
 230     cast_if_needed_opt target_t (Clight.Expr (Clight.Efield (e', field), t))
 231
 232   | _, Clight.Ecost (lbl, e) ->
 233     let e' = simplify_expr target_t e in
 234     Clight.Expr (Clight.Ecost (lbl, e'), type_of_expr e')
 235
 236   | _, Clight.Ecall _ ->
 237     assert false (* should be impossible *)
 238
 239
 240 let f_ctype ctype _ = ctype
 241
 242 let f_expr e _ _ = e
 243
 244 let f_expr_descr e _ _ =  e
 245
 246 let f_statement stmt _ sub_stmts_res =
 247   let f_expr b e =
 248     simplify_expr (if b then Some (type_of_expr e) else None) e in
 249   let f_exprs b = List.map (f_expr b) in
 250   let f_sub_exprs = match stmt with
 251     | Clight.Sassign _ | Clight.Scall _ | Clight.Sreturn _ -> f_exprs true
 252     | _ -> f_exprs false in
 253   let sub_exprs = f_sub_exprs (ClightFold.statement_sub_exprs stmt) in
 254   ClightFold.statement_fill_subs stmt sub_exprs sub_stmts_res
 255
 256 let simplify_stmt = ClightFold.statement f_ctype f_expr f_expr_descr f_statement
 257
 258 let simplify_funct (id, fundef) =
 259   let fundef' = match fundef with
 260     | Clight.Internal cfun ->
 261       Clight.Internal
 262         { cfun with Clight.fn_body = simplify_stmt cfun.Clight.fn_body }
 263     | _ -> fundef in
 264   (id, fundef')
 265
 266 let simplify p =
 267   { p with Clight.prog_funct = List.map simplify_funct p.Clight.prog_funct }
 268
 269 (* TODO: restore above, but buggy with
 270    (unsigned int) (-x) -> - ((unsigned int) x) *)
 271
 272 (*
 273 let simplify p = p
 274 *)