]> matita.cs.unibo.it Git - pkg-cerco/acc-trusted.git/blob - cparser/Bitfields.ml
Imported Upstream version 0.1
[pkg-cerco/acc-trusted.git] / cparser / Bitfields.ml
1 (* *********************************************************************)
2 (*                                                                     *)
3 (*              The Compcert verified compiler                         *)
4 (*                                                                     *)
5 (*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
6 (*                                                                     *)
7 (*  Copyright Institut National de Recherche en Informatique et en     *)
8 (*  Automatique.  All rights reserved.  This file is distributed       *)
9 (*  under the terms of the GNU General Public License as published by  *)
10 (*  the Free Software Foundation, either version 2 of the License, or  *)
11 (*  (at your option) any later version.  This file is also distributed *)
12 (*  under the terms of the INRIA Non-Commercial License Agreement.     *)
13 (*                                                                     *)
14 (* *********************************************************************)
15
16 (* Elimination of bit fields in structs *)
17
18 (* Assumes: unblocked, simplified code.
19    Preserves: unblocked, simplified code. *)
20
21 open Printf
22 open Machine
23 open C
24 open Cutil
25 open Transform
26
27 (* Info associated to each bitfield *)
28
29 type bitfield_info =
30   { bf_carrier: string; (* name of underlying regular field *)
31     bf_carrier_typ: typ; (* type of underlying regular field *)
32     bf_pos: int;        (* start bit *)
33     bf_size: int;       (* size in bit *)
34     bf_signed: bool }   (* signed or unsigned *)
35
36 (* invariants:
37      0 <= pos < bitsizeof(int)
38      0 < sz <= bitsizeof(int)
39      0 < pos + sz <= bitsizeof(int)
40 *)
41
42 (* Mapping (struct identifier, bitfield name) -> bitfield info *)
43
44 let bitfield_table =
45       (Hashtbl.create 57: (ident * string, bitfield_info) Hashtbl.t)
46
47 (* Packing algorithm -- keep consistent with [Cutil.pack_bitfield]! *)
48
49 let unsigned_ikind_for_carrier nbits =
50   if nbits <= 8 then IUChar else
51   if nbits <= 8 * !config.sizeof_short then IUShort else
52   if nbits <= 8 * !config.sizeof_int then IUInt else
53   if nbits <= 8 * !config.sizeof_long then IULong else
54   if nbits <= 8 * !config.sizeof_longlong then IULongLong else
55   assert false
56
57 let pack_bitfields env id ml =
58   let rec pack accu pos = function
59   | [] ->
60       (pos, accu, [])
61   | m :: ms as ml ->
62       match m.fld_bitfield with
63       | None -> (pos, accu, ml)
64       | Some n ->
65           if n = 0 then
66             (pos, accu, ms) (* bit width 0 means end of pack *)
67           else if pos + n > 8 * !config.sizeof_int then
68             (pos, accu, ml) (* doesn't fit in current word *)
69           else begin
70             let signed =
71               match unroll env m.fld_typ with
72               | TInt(ik, _) -> is_signed_ikind ik
73               | _ -> assert false (* should never happen, checked in Elab *) in
74             pack ((m.fld_name, pos, n, signed) :: accu) (pos + n) ms
75           end
76   in pack [] 0 ml
77
78 let rec transf_members env id count = function
79   | [] -> []
80   | m :: ms as ml ->
81       if m.fld_bitfield = None then
82         m :: transf_members env id count ms
83       else begin
84         let (nbits, bitfields, ml') = pack_bitfields env id ml in
85         let carrier = sprintf "__bf%d" count in
86         let carrier_typ = TInt(unsigned_ikind_for_carrier nbits, []) in
87         List.iter
88           (fun (name, pos, sz, signed) ->
89             Hashtbl.add bitfield_table
90               (id, name)
91               {bf_carrier = carrier; bf_carrier_typ = carrier_typ;
92                bf_pos = pos; bf_size = sz; bf_signed = signed})
93           bitfields;
94         { fld_name = carrier; fld_typ = carrier_typ; fld_bitfield = None}
95         :: transf_members env id (count + 1) ml'
96       end
97
98 let transf_composite env su id ml =
99   match su with
100   | Struct -> transf_members env id 1 ml
101   | Union  -> ml
102
103 (* Bitfield manipulation expressions *)
104
105 let left_shift_count bf =
106   intconst 
107     (Int64.of_int (8 * !config.sizeof_int - (bf.bf_pos + bf.bf_size)))
108     IInt
109
110 let right_shift_count bf =
111   intconst 
112     (Int64.of_int (8 * !config.sizeof_int - bf.bf_size))
113     IInt
114
115 let insertion_mask bf =
116   let m =
117     Int64.shift_left
118       (Int64.pred (Int64.shift_left 1L bf.bf_size))
119       bf.bf_pos in
120   (* Give the mask an hexadecimal string representation, nicer to read *)
121   {edesc = EConst(CInt(m, IUInt, sprintf "0x%LXU" m)); etyp = TInt(IUInt, [])}
122
123 (* Extract the value of a bitfield *)
124
125 (* Reference C code:
126
127 unsigned int bitfield_unsigned_extract(unsigned int x, int ofs, int sz)
128 {
129   return (x << (BITSIZE_UINT - (ofs + sz))) >> (BITSIZE_UINT - sz);
130 }
131
132 signed int bitfield_signed_extract(unsigned int x, int ofs, int sz)
133 {
134   return ((signed int) (x << (BITSIZE_UINT - (ofs + sz))))
135          >> (BITSIZE_UINT - sz);
136 }
137
138 *)
139
140 let bitfield_extract bf carrier =
141   let e1 =
142     {edesc = EBinop(Oshl, carrier, left_shift_count bf, TInt(IUInt, []));
143      etyp = carrier.etyp} in
144   let ty = TInt((if bf.bf_signed then IInt else IUInt), []) in
145   let e2 =
146     {edesc = ECast(ty, e1); etyp = ty} in
147   {edesc = EBinop(Oshr, e2, right_shift_count bf, e2.etyp);
148    etyp = e2.etyp}
149
150 (* Assign a bitfield within a carrier *)
151
152 (* Reference C code:
153
154 unsigned int bitfield_insert(unsigned int x, int ofs, int sz, unsigned int y)
155 {
156   unsigned int mask = ((1U << sz) - 1) << ofs;
157   return (x & ~mask) | ((y << ofs) & mask);
158 }
159
160 *)
161
162 let bitfield_assign bf carrier newval =
163   let msk = insertion_mask bf in
164   let notmsk = {edesc = EUnop(Onot, msk); etyp = msk.etyp} in
165   let newval_shifted =
166     {edesc = EBinop(Oshl, newval, intconst (Int64.of_int bf.bf_pos) IUInt,
167                     TInt(IUInt,[]));
168      etyp = TInt(IUInt,[])} in
169   let newval_masked =
170     {edesc = EBinop(Oand, newval_shifted, msk, TInt(IUInt,[]));
171      etyp = TInt(IUInt,[])}
172   and oldval_masked =
173     {edesc = EBinop(Oand, carrier, notmsk, TInt(IUInt,[]));
174      etyp = TInt(IUInt,[])} in
175   {edesc = EBinop(Oor,  oldval_masked, newval_masked,  TInt(IUInt,[]));
176    etyp =  TInt(IUInt,[])}
177
178 (* Expressions *)
179
180 let transf_expr env e =
181
182   let is_bitfield_access ty fieldname =
183     match unroll env ty with
184     | TStruct(id, _) ->
185         (try Some(Hashtbl.find bitfield_table (id, fieldname))
186          with Not_found -> None)
187     | _ -> None in
188
189   let is_bitfield_access_ptr ty fieldname =
190     match unroll env ty with
191     | TPtr(ty', _) -> is_bitfield_access ty' fieldname
192     | _ -> None in 
193
194   let rec texp e =
195     match e.edesc with
196     | EConst _ -> e
197     | ESizeof _ -> e
198     | EVar _ -> e
199
200     | EUnop(Odot fieldname, e1) ->
201         let e1' = texp e1 in
202         begin match is_bitfield_access e1.etyp fieldname with
203         | None ->
204             {edesc = EUnop(Odot fieldname, e1'); etyp = e.etyp}
205         | Some bf ->
206             bitfield_extract bf
207               {edesc = EUnop(Odot bf.bf_carrier, e1');
208                etyp = bf.bf_carrier_typ}
209         end
210
211     | EUnop(Oarrow fieldname, e1) ->
212         let e1' = texp e1 in
213         begin match is_bitfield_access_ptr e1.etyp fieldname with
214         | None ->
215             {edesc = EUnop(Oarrow fieldname, e1'); etyp = e.etyp}
216         | Some bf ->
217             bitfield_extract bf
218               {edesc = EUnop(Oarrow bf.bf_carrier, e1');
219                etyp = bf.bf_carrier_typ}
220         end
221
222     | EUnop(op, e1) ->
223         (* Note: simplified expr, so no ++/-- *)
224         {edesc = EUnop(op, texp e1); etyp = e.etyp}
225
226     | EBinop(Oassign, e1, e2, ty) ->
227         begin match e1.edesc with
228         | EUnop(Odot fieldname, e11) ->
229             let lhs = texp e11 in let rhs = texp e2 in
230             begin match is_bitfield_access e11.etyp fieldname with
231             | None ->
232                 {edesc = EBinop(Oassign,
233                                 {edesc = EUnop(Odot fieldname, lhs);
234                                  etyp = e1.etyp},
235                                 rhs, ty);
236                  etyp = e.etyp}
237             | Some bf ->
238                 let carrier =
239                   {edesc = EUnop(Odot bf.bf_carrier, lhs);
240                    etyp = bf.bf_carrier_typ} in
241                 {edesc = EBinop(Oassign, carrier,
242                                 bitfield_assign bf carrier rhs,
243                                 carrier.etyp);
244                  etyp = carrier.etyp}
245             end
246         | EUnop(Oarrow fieldname, e11) ->
247             let lhs = texp e11 in let rhs = texp e2 in
248             begin match is_bitfield_access_ptr e11.etyp fieldname with
249             | None ->
250                 {edesc = EBinop(Oassign,
251                                 {edesc = EUnop(Oarrow fieldname, lhs);
252                                  etyp = e1.etyp},
253                                 rhs, ty);
254                  etyp = e.etyp}
255             | Some bf ->
256                 let carrier =
257                   {edesc = EUnop(Oarrow bf.bf_carrier, lhs);
258                    etyp = bf.bf_carrier_typ} in
259                 {edesc = EBinop(Oassign, carrier,
260                                 bitfield_assign bf carrier rhs,
261                                 carrier.etyp);
262                  etyp = carrier.etyp}
263             end
264         | _ ->
265             {edesc = EBinop(Oassign, texp e1, texp e2, e1.etyp); etyp = e1.etyp}
266         end
267
268     | EBinop(op, e1, e2, ty) ->
269         (* Note: simplified expr assumed, so no assign-op *)
270         {edesc = EBinop(op, texp e1, texp e2, ty); etyp = e.etyp}
271     | EConditional(e1, e2, e3) ->
272         {edesc = EConditional(texp e1, texp e2, texp e3); etyp = e.etyp}
273     | ECast(ty, e1) ->
274         {edesc = ECast(ty, texp e1); etyp = e.etyp}
275     | ECall(e1, el) ->
276         {edesc = ECall(texp e1, List.map texp el); etyp = e.etyp}
277
278   in texp e
279
280 (* Statements *)
281
282 let rec transf_stmt env s =
283   match s.sdesc with
284   | Sskip -> s
285   | Sdo e ->
286       {sdesc = Sdo(transf_expr env e); sloc = s.sloc}
287   | Sseq(s1, s2) -> 
288       {sdesc = Sseq(transf_stmt env s1, transf_stmt env s2); sloc = s.sloc }
289   | Sif(e, s1, s2) ->
290       {sdesc = Sif(transf_expr env e, transf_stmt env s1, transf_stmt env s2);
291        sloc = s.sloc}
292   | Swhile(e, s1) ->
293       {sdesc = Swhile(transf_expr env e, transf_stmt env s1);
294        sloc = s.sloc}
295   | Sdowhile(s1, e) ->
296       {sdesc = Sdowhile(transf_stmt env s1, transf_expr env e);
297        sloc = s.sloc}
298   | Sfor(s1, e, s2, s3) ->
299       {sdesc = Sfor(transf_stmt env s1, transf_expr env e, transf_stmt env s2,
300                     transf_stmt env s3);
301        sloc = s.sloc}
302   | Sbreak -> s
303   | Scontinue -> s
304   | Sswitch(e, s1) ->
305       {sdesc = Sswitch(transf_expr env e, transf_stmt env s1); sloc = s.sloc}
306   | Slabeled(lbl, s) ->
307       {sdesc = Slabeled(lbl, transf_stmt env s); sloc = s.sloc}
308   | Sgoto lbl -> s
309   | Sreturn None -> s
310   | Sreturn (Some e) ->
311       {sdesc = Sreturn(Some(transf_expr env e)); sloc = s.sloc}
312   | Sblock _ | Sdecl _ ->
313       assert false     (* should not occur in unblocked code *)
314
315 (* Functions *)
316
317 let transf_fundef env f =
318   { f with fd_body = transf_stmt env f.fd_body }
319
320 (* Initializers *)
321
322 let bitfield_initializer bf i =
323   match i with
324   | Init_single e ->
325       let m = Int64.pred (Int64.shift_left 1L bf.bf_size) in
326       let e_mask =
327         {edesc = EConst(CInt(m, IUInt, sprintf "0x%LXU" m));
328          etyp = TInt(IUInt, [])} in
329       let e_and =
330         {edesc = EBinop(Oand, e, e_mask, TInt(IUInt,[]));
331          etyp = TInt(IUInt,[])} in
332       {edesc = EBinop(Oshl, e_and, intconst (Int64.of_int bf.bf_pos) IInt,
333                       TInt(IUInt, []));
334        etyp = TInt(IUInt, [])}
335   | _ -> assert false
336
337 let rec pack_bitfield_init id carrier fld_init_list =
338   match fld_init_list with
339   | [] -> ([], [])
340   | (fld, i) :: rem ->
341       try
342         let bf = Hashtbl.find bitfield_table (id, fld.fld_name) in
343         if bf.bf_carrier <> carrier then
344           ([], fld_init_list)
345         else begin
346           let (el, rem') = pack_bitfield_init id carrier rem in
347           (bitfield_initializer bf i :: el, rem')
348         end
349       with Not_found ->
350         ([], fld_init_list)
351
352 let rec or_expr_list = function
353   | [] -> assert false
354   | [e] -> e
355   | e1 :: el ->
356       {edesc = EBinop(Oor, e1, or_expr_list el, TInt(IUInt,[]));
357        etyp = TInt(IUInt,[])}
358
359 let rec transf_struct_init id fld_init_list =
360   match fld_init_list with
361   | [] -> []
362   | (fld, i) :: rem ->
363       try
364         let bf = Hashtbl.find bitfield_table (id, fld.fld_name) in
365         let (el, rem') =
366           pack_bitfield_init id bf.bf_carrier fld_init_list in
367         ({fld_name = bf.bf_carrier; fld_typ = bf.bf_carrier_typ;
368           fld_bitfield = None},
369          Init_single {edesc = ECast(bf.bf_carrier_typ, or_expr_list el);
370                       etyp = bf.bf_carrier_typ})
371         :: transf_struct_init id rem'
372       with Not_found ->
373         (fld, i) :: transf_struct_init id rem
374
375 let rec transf_init env i =
376   match i with
377   | Init_single e -> Init_single (transf_expr env e)
378   | Init_array il -> Init_array (List.map (transf_init env) il)
379   | Init_struct(id, fld_init_list) ->
380       let fld_init_list' =
381         List.map (fun (f, i) -> (f, transf_init env i)) fld_init_list in
382         Init_struct(id, transf_struct_init id fld_init_list')
383   | Init_union(id, fld, i) -> Init_union(id, fld, transf_init env i)
384
385 let transf_decl env (sto, id, ty, init_opt) =
386   (sto, id, ty,
387    match init_opt with None -> None | Some i -> Some(transf_init env i))
388
389 (* Programs *)
390
391 let program p =
392   Transform.program
393     ~composite:transf_composite
394     ~decl: transf_decl
395     ~fundef:transf_fundef 
396     p