source: Deliverables/D2.2/8051/cparser/Bitfields.ml @ 486

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

Deliverable D2.2

File size: 13.0 KB
Line 
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
21open Printf
22open Machine
23open C
24open Cutil
25open Transform
26
27(* Info associated to each bitfield *)
28
29type 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
44let bitfield_table =
45      (Hashtbl.create 57: (ident * string, bitfield_info) Hashtbl.t)
46
47(* Packing algorithm -- keep consistent with [Cutil.pack_bitfield]! *)
48
49let 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
57let 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
78let 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
98let 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
105let left_shift_count bf =
106  intconst
107    (Int64.of_int (8 * !config.sizeof_int - (bf.bf_pos + bf.bf_size)))
108    IInt
109
110let right_shift_count bf =
111  intconst
112    (Int64.of_int (8 * !config.sizeof_int - bf.bf_size))
113    IInt
114
115let 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
127unsigned int bitfield_unsigned_extract(unsigned int x, int ofs, int sz)
128{
129  return (x << (BITSIZE_UINT - (ofs + sz))) >> (BITSIZE_UINT - sz);
130}
131
132signed 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
140let 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
154unsigned 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
162let 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
180let 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
282let 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
317let transf_fundef env f =
318  { f with fd_body = transf_stmt env f.fd_body }
319
320(* Initializers *)
321
322let 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
337let 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
352let 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
359let 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
375let 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
385let 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
391let program p =
392  Transform.program
393    ~composite:transf_composite
394    ~decl: transf_decl
395    ~fundef:transf_fundef
396    p
Note: See TracBrowser for help on using the repository browser.