source: Deliverables/D2.2/8051/src/clight/clightCasts.ml @ 1664

Last change on this file since 1664 was 1099, checked in by ayache, 8 years ago

Bug fix in Deliverables/D2.2/8051: cast simplification.

File size: 6.7 KB
Line 
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
9let error_prefix = "Clight casts simplification"
10let error = Error.global_error error_prefix
11let error_float () = error "float not supported."
12
13
14(* Int sizes *)
15
16let int_of_intsize = function
17  | Clight.I8 -> 8
18  | Clight.I16 -> 16
19  | Clight.I32 -> 32
20
21let intsize_of_int = function
22  | i when i <= 8 -> Clight.I8
23  | i when i <= 16 -> Clight.I16
24  | _ -> Clight.I32
25
26let op_intsize_no_cast op size1 size2 =
27  op (int_of_intsize size1) (int_of_intsize size2)
28
29let cmp_intsize cmp size1 size2 = op_intsize_no_cast cmp size1 size2
30
31let op_intsize op size1 size2 =
32  intsize_of_int (op_intsize_no_cast op size1 size2)
33
34let max_intsize size1 size2 = op_intsize max size1 size2
35
36let intsize_union size1 size2 = op_intsize (+) size1 size2
37
38let pow2 = MiscPottier.pow 2
39
40let 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
51let 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
67let 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
72let int_type_union t1 t2 =
73  let (size, sign) = match t1, t2 with
74    | Clight.Tint (size1, sign1), Clight.Tint (size2, sign2)
75      when sign1 = sign2 -> (max_intsize size1 size2, sign1)
76    | Clight.Tint (size1, sign1), Clight.Tint (size2, sign2) ->
77      (intsize_union size1 size2, AST.Signed)
78    | _ -> assert false (* only use on int types *)
79  in
80  Clight.Tint (size, sign)
81
82
83(* C types *)
84
85let type_of_expr (Clight.Expr (_, t)) = t
86
87let cast_if_needed t (Clight.Expr (ed, t') as e) = match t, ed with
88  | _ when t = t' -> e
89  | Clight.Tint (size, sign), Clight.Econst_int i
90    when belongs_to_int_type size sign i ->
91    Clight.Expr (Clight.Econst_int i, t)
92  | _ -> Clight.Expr (Clight.Ecast (t, e), t)
93
94let le_ctype t1 t2 = match t1, t2 with
95  | Clight.Tint (size1, sign1), Clight.Tint (size2, sign2) ->
96    le_int_type size1 sign1 size2 sign2
97  | _ -> t1 = t2
98
99
100(* Simplification *)
101
102let rec simplify_bool_op f_bool t e1 e2 =
103  let (e1', e2', t') = simplify_and_same_type t e1 e2 in
104  Clight.Expr (f_bool e1' e2', t')
105
106and simplify_and_same_type t e1 e2 =
107  let e1' = simplify_expr e1 in
108  let e2' = simplify_expr e2 in
109  if type_of_expr e1' = type_of_expr e2' then (e1', e2', type_of_expr e1')
110  else (cast_if_needed t e1', cast_if_needed t e2', t)
111
112and simplify_expr (Clight.Expr (ed, t) as e) = match ed with
113
114  | Clight.Econst_int i ->
115    let t' = smallest_int_type i in
116    Clight.Expr (ed, t')
117
118  | Clight.Evar _ -> e
119
120  | Clight.Esizeof _ ->
121    let intsize = intsize_of_int (Driver.TargetArch.int_size * 8) in
122    Clight.Expr (ed, Clight.Tint (intsize, AST.Unsigned))
123
124  | Clight.Econst_float _ -> error_float ()
125
126  | Clight.Ederef e ->
127    let e' = simplify_expr e in
128    Clight.Expr (Clight.Ederef e', t)
129
130  | Clight.Eaddrof e ->
131    let e' = simplify_expr e in
132    Clight.Expr (Clight.Eaddrof e', t)
133
134  | Clight.Eunop _ -> e
135
136  | Clight.Ebinop _ -> e
137
138  (* [(t1) unop ((t2) e)], when [e] simplified has type [t1] and [t1] <= [t2],
139     is simplified to [unop e] *)
140  | Clight.Ecast
141      (t1,
142       Clight.Expr
143         (Clight.Eunop (unop, Clight.Expr (Clight.Ecast (_, e'), _)), t2))
144      when le_ctype t1 t2 ->
145    let e' = simplify_expr e' in
146    let t' = type_of_expr e' in
147    if t' = t1 then Clight.Expr (Clight.Eunop (unop, e'), t') else e
148
149  (* [(t) ((t') e1 binop (t') e2)], when [e1] and [e2] simplified have type [t]
150     and [t] <= [t'], is simplified to [e] *)
151  | Clight.Ecast
152      (t,
153       Clight.Expr
154         (Clight.Ebinop
155            (binop,
156             Clight.Expr (Clight.Ecast (_, e1), _),
157             Clight.Expr (Clight.Ecast (_, e2), _)),
158          t'))
159      when le_ctype t t' ->
160    let e1 = simplify_expr e1 in
161    let t1 = type_of_expr e1 in
162    let e2 = simplify_expr e2 in
163    let t2 = type_of_expr e2 in
164    if t1 = t && t2 = t then Clight.Expr (Clight.Ebinop (binop, e1, e2), t)
165    else e
166
167  | Clight.Ecast (t', e) ->
168    Clight.Expr (Clight.Ecast (t', simplify_expr e), t')
169
170  | Clight.Econdition (e1, e2, e3) ->
171    let e1' = simplify_expr e1 in
172    let (e2', e3', t') = simplify_and_same_type t e2 e3 in
173    Clight.Expr (Clight.Econdition (e1', e2', e3'), t')
174
175  | Clight.Eandbool (e1, e2) ->
176    simplify_bool_op (fun e1' e2' -> Clight.Eandbool (e1', e2')) t e1 e2
177
178  | Clight.Eorbool (e1, e2) ->
179    simplify_bool_op (fun e1' e2' -> Clight.Eorbool (e1', e2')) t e1 e2
180
181  | Clight.Efield (e, field) ->
182    Clight.Expr (Clight.Efield (simplify_expr e, field), t)
183
184  | Clight.Ecost (lbl, e) ->
185    Clight.Expr (Clight.Ecost (lbl, simplify_expr e), t)
186
187  | Clight.Ecall (id, e1, e2) ->
188    assert false (* should be impossible *)
189
190
191let f_ctype ctype _ = ctype
192
193let f_expr e _ _ = e
194
195let f_expr_descr e _ _ =  e
196
197let f_statement stmt _ sub_stmts_res =
198  let f_expr b e =
199    let e' = simplify_expr e in
200    if b then cast_if_needed (type_of_expr e) e'
201    else e' in
202  let f_exprs b = List.map (f_expr b) in
203  let f_sub_exprs = match stmt with
204    | Clight.Sassign _ | Clight.Scall _ | Clight.Sreturn _ -> f_exprs true
205    | _ -> f_exprs false in
206  let sub_exprs = f_sub_exprs (ClightFold.statement_sub_exprs stmt) in
207  ClightFold.statement_fill_subs stmt sub_exprs sub_stmts_res
208
209let simplify_stmt = ClightFold.statement f_ctype f_expr f_expr_descr f_statement
210
211let simplify_funct (id, fundef) =
212  let fundef' = match fundef with
213    | Clight.Internal cfun ->
214      Clight.Internal
215        { cfun with Clight.fn_body = simplify_stmt cfun.Clight.fn_body }
216    | _ -> fundef in
217  (id, fundef')
218
219let simplify p =
220  { p with Clight.prog_funct = List.map simplify_funct p.Clight.prog_funct }
Note: See TracBrowser for help on using the repository browser.