2 (** [simplify p] removes unnecessary casts in the Clight program [p].
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. *)
9 let error_prefix = "Clight casts simplification"
10 let error = Error.global_error error_prefix
11 let error_float () = error "float not supported."
16 let int_of_intsize = function
21 let intsize_of_int = function
22 | i when i <= 8 -> Clight.I8
23 | i when i <= 16 -> Clight.I16
26 let op_intsize_no_cast op size1 size2 =
27 op (int_of_intsize size1) (int_of_intsize size2)
29 let cmp_intsize cmp size1 size2 = op_intsize_no_cast cmp size1 size2
31 let op_intsize op size1 size2 =
32 intsize_of_int (op_intsize_no_cast op size1 size2)
34 let max_intsize size1 size2 = op_intsize max size1 size2
36 let intsize_union size1 size2 = op_intsize (+) size1 size2
38 let pow2 = MiscPottier.pow 2
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 *)
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)
64 (Clight.I32, AST.Signed) in
65 Clight.Tint (size, sign)
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
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)
79 let type_of_expr (Clight.Expr (_, t)) = t
81 let cast_if_needed t (Clight.Expr (ed, t') as e) = match t, ed with
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)
88 let cast_if_needed_opt opt_t e = match opt_t with
90 | Some t -> cast_if_needed t e
92 let is_int_type = function
93 | Clight.Tint _ -> true
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
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 *)
107 let belongs_to_ctype t i = match t with
108 | Clight.Tint (size, sign) -> belongs_to_int_type size sign i
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
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')
123 and simplify_and_same_type target_t e1 e2 = match target_t with
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
135 else (e1, e2, type_of_expr e1)
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
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
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)
157 and simplify_expr target_t (Clight.Expr (ed, t) as e) = match target_t, ed with
159 | None, Clight.Econst_int i ->
160 let t' = smallest_int_type i in
163 | Some t', Clight.Econst_int i when belongs_to_ctype t' i ->
166 | Some t', Clight.Econst_int _ -> cast_if_needed t' e
168 | _, Clight.Evar _ -> cast_if_needed_opt target_t e
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))
175 | _, Clight.Econst_float _ -> error_float ()
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))
181 | _, Clight.Eaddrof e ->
182 let e' = simplify_expr None e in
184 Clight.Expr (Clight.Eaddrof e', Clight.Tpointer (type_of_expr e')) in
185 cast_if_needed_opt target_t e'
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')
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
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))
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)
215 | _, Clight.Ecast (_, e) -> simplify_expr target_t e
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')
222 | _, Clight.Eandbool (e1, e2) ->
223 simplify_bool_op (fun e1' e2' -> Clight.Eandbool (e1', e2')) target_t e1 e2
225 | _, Clight.Eorbool (e1, e2) ->
226 simplify_bool_op (fun e1' e2' -> Clight.Eorbool (e1', e2')) target_t e1 e2
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))
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')
236 | _, Clight.Ecall _ ->
237 assert false (* should be impossible *)
240 let f_ctype ctype _ = ctype
244 let f_expr_descr e _ _ = e
246 let f_statement stmt _ sub_stmts_res =
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
256 let simplify_stmt = ClightFold.statement f_ctype f_expr f_expr_descr f_statement
258 let simplify_funct (id, fundef) =
259 let fundef' = match fundef with
260 | Clight.Internal cfun ->
262 { cfun with Clight.fn_body = simplify_stmt cfun.Clight.fn_body }
267 { p with Clight.prog_funct = List.map simplify_funct p.Clight.prog_funct }
269 (* TODO: restore above, but buggy with
270 (unsigned int) (-x) -> - ((unsigned int) x) *)