source: Deliverables/D2.3/8051-memoryspaces-branch/cparser/Bitfields.ml @ 460

Last change on this file since 460 was 460, checked in by campbell, 9 years ago

Port memory spaces changes to latest prototype compiler.

File size: 13.8 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, []); espace = Code} (* XXX are consts always Code? *)
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; espace = Any} in
144  let ty = TInt((if bf.bf_signed then IInt else IUInt), []) in
145  let e2 =
146    {edesc = ECast(ty, e1); etyp = ty; espace = Any} in
147  {edesc = EBinop(Oshr, e2, right_shift_count bf, e2.etyp);
148   etyp = e2.etyp; espace = Any}
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; espace = Any} 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,[]);
169     espace = Any} in
170  let newval_masked =
171    {edesc = EBinop(Oand, newval_shifted, msk, TInt(IUInt,[]));
172     etyp = TInt(IUInt,[]);
173     espace = Any}
174  and oldval_masked =
175    {edesc = EBinop(Oand, carrier, notmsk, TInt(IUInt,[]));
176     etyp = TInt(IUInt,[]); espace = Any} in
177  {edesc = EBinop(Oor,  oldval_masked, newval_masked,  TInt(IUInt,[]));
178   etyp =  TInt(IUInt,[]); espace = Any}
179
180(* Expressions *)
181
182let transf_expr env e =
183
184  let is_bitfield_access ty fieldname =
185    match unroll env ty with
186    | TStruct(id, _) ->
187        (try Some(Hashtbl.find bitfield_table (id, fieldname))
188         with Not_found -> None)
189    | _ -> None in
190
191  let is_bitfield_access_ptr ty fieldname =
192    match unroll env ty with
193    | TPtr(_, ty', _) -> is_bitfield_access ty' fieldname
194    | _ -> None in 
195
196  let rec texp e =
197    match e.edesc with
198    | EConst _ -> e
199    | ESizeof _ -> e
200    | EVar _ -> e
201
202    | EUnop(Odot fieldname, e1) ->
203        let e1' = texp e1 in
204        begin match is_bitfield_access e1.etyp fieldname with
205        | None ->
206            {edesc = EUnop(Odot fieldname, e1'); etyp = e.etyp; espace = e1'.espace}
207        | Some bf ->
208            bitfield_extract bf
209              {edesc = EUnop(Odot bf.bf_carrier, e1');
210               etyp = bf.bf_carrier_typ;
211               espace = e1'.espace}
212        end
213
214    | EUnop(Oarrow fieldname, e1) ->
215        let e1' = texp e1 in
216        begin match is_bitfield_access_ptr e1.etyp fieldname with
217        | None ->
218            {edesc = EUnop(Oarrow fieldname, e1'); etyp = e.etyp; espace = Any}
219        | Some bf ->
220            bitfield_extract bf
221              {edesc = EUnop(Oarrow bf.bf_carrier, e1');
222               etyp = bf.bf_carrier_typ; espace = Any}
223        end
224
225    | EUnop(op, e1) ->
226        (* Note: simplified expr, so no ++/-- *)
227        {edesc = EUnop(op, texp e1); etyp = e.etyp; espace = e.espace}
228
229    | EBinop(Oassign, e1, e2, ty) ->
230        begin match e1.edesc with
231        | EUnop(Odot fieldname, e11) ->
232            let lhs = texp e11 in let rhs = texp e2 in
233            begin match is_bitfield_access e11.etyp fieldname with
234            | None ->
235                {edesc = EBinop(Oassign,
236                                {edesc = EUnop(Odot fieldname, lhs);
237                                 etyp = e1.etyp; espace = lhs.espace},
238                                rhs, ty);
239                 etyp = e.etyp;
240                 espace = e.espace}
241            | Some bf ->
242                let carrier =
243                  {edesc = EUnop(Odot bf.bf_carrier, lhs);
244                   etyp = bf.bf_carrier_typ;
245                   espace = lhs.espace} in
246                {edesc = EBinop(Oassign, carrier,
247                                bitfield_assign bf carrier rhs,
248                                carrier.etyp);
249                 etyp = carrier.etyp;
250                 espace = lhs.espace}
251            end
252        | EUnop(Oarrow fieldname, e11) ->
253            let lhs = texp e11 in let rhs = texp e2 in
254            begin match is_bitfield_access_ptr e11.etyp fieldname with
255            | None ->
256                {edesc = EBinop(Oassign,
257                                {edesc = EUnop(Oarrow fieldname, lhs);
258                                 etyp = e1.etyp;
259                                 espace = e1.espace},
260                                rhs, ty);
261                 etyp = e.etyp;
262                 espace = e.espace}
263            | Some bf ->
264                let carrier =
265                  {edesc = EUnop(Oarrow bf.bf_carrier, lhs);
266                   etyp = bf.bf_carrier_typ;
267                   espace = Any} in
268                {edesc = EBinop(Oassign, carrier,
269                                bitfield_assign bf carrier rhs,
270                                carrier.etyp);
271                 etyp = carrier.etyp;
272                 espace = Any}
273            end
274        | _ ->
275            {edesc = EBinop(Oassign, texp e1, texp e2, e1.etyp); etyp = e1.etyp; espace = e1.espace}
276        end
277
278    | EBinop(op, e1, e2, ty) ->
279        (* Note: simplified expr assumed, so no assign-op *)
280        {edesc = EBinop(op, texp e1, texp e2, ty); etyp = e.etyp; espace = e.espace}
281    | EConditional(e1, e2, e3) ->
282        {edesc = EConditional(texp e1, texp e2, texp e3); etyp = e.etyp; espace = e.espace}
283    | ECast(ty, e1) ->
284        {edesc = ECast(ty, texp e1); etyp = e.etyp; espace = e.espace}
285    | ECall(e1, el) ->
286        {edesc = ECall(texp e1, List.map texp el); etyp = e.etyp; espace = e.espace}
287
288  in texp e
289
290(* Statements *)
291
292let rec transf_stmt env s =
293  match s.sdesc with
294  | Sskip -> s
295  | Sdo e ->
296      {sdesc = Sdo(transf_expr env e); sloc = s.sloc}
297  | Sseq(s1, s2) -> 
298      {sdesc = Sseq(transf_stmt env s1, transf_stmt env s2); sloc = s.sloc }
299  | Sif(e, s1, s2) ->
300      {sdesc = Sif(transf_expr env e, transf_stmt env s1, transf_stmt env s2);
301       sloc = s.sloc}
302  | Swhile(e, s1) ->
303      {sdesc = Swhile(transf_expr env e, transf_stmt env s1);
304       sloc = s.sloc}
305  | Sdowhile(s1, e) ->
306      {sdesc = Sdowhile(transf_stmt env s1, transf_expr env e);
307       sloc = s.sloc}
308  | Sfor(s1, e, s2, s3) ->
309      {sdesc = Sfor(transf_stmt env s1, transf_expr env e, transf_stmt env s2,
310                    transf_stmt env s3);
311       sloc = s.sloc}
312  | Sbreak -> s
313  | Scontinue -> s
314  | Sswitch(e, s1) ->
315      {sdesc = Sswitch(transf_expr env e, transf_stmt env s1); sloc = s.sloc}
316  | Slabeled(lbl, s) ->
317      {sdesc = Slabeled(lbl, transf_stmt env s); sloc = s.sloc}
318  | Sgoto lbl -> s
319  | Sreturn None -> s
320  | Sreturn (Some e) ->
321      {sdesc = Sreturn(Some(transf_expr env e)); sloc = s.sloc}
322  | Sblock _ | Sdecl _ ->
323      assert false     (* should not occur in unblocked code *)
324
325(* Functions *)
326
327let transf_fundef env f =
328  { f with fd_body = transf_stmt env f.fd_body }
329
330(* Initializers *)
331
332let bitfield_initializer bf i =
333  match i with
334  | Init_single e ->
335      let m = Int64.pred (Int64.shift_left 1L bf.bf_size) in
336      let e_mask =
337        {edesc = EConst(CInt(m, IUInt, sprintf "0x%LXU" m));
338         etyp = TInt(IUInt, []);
339         espace = Any} in
340      let e_and =
341        {edesc = EBinop(Oand, e, e_mask, TInt(IUInt,[]));
342         etyp = TInt(IUInt,[]);
343         espace = Any} in
344      {edesc = EBinop(Oshl, e_and, intconst (Int64.of_int bf.bf_pos) IInt,
345                      TInt(IUInt, []));
346       etyp = TInt(IUInt, []);
347       espace = Any}
348  | _ -> assert false
349
350let rec pack_bitfield_init id carrier fld_init_list =
351  match fld_init_list with
352  | [] -> ([], [])
353  | (fld, i) :: rem ->
354      try
355        let bf = Hashtbl.find bitfield_table (id, fld.fld_name) in
356        if bf.bf_carrier <> carrier then
357          ([], fld_init_list)
358        else begin
359          let (el, rem') = pack_bitfield_init id carrier rem in
360          (bitfield_initializer bf i :: el, rem')
361        end
362      with Not_found ->
363        ([], fld_init_list)
364
365let rec or_expr_list = function
366  | [] -> assert false
367  | [e] -> e
368  | e1 :: el ->
369      {edesc = EBinop(Oor, e1, or_expr_list el, TInt(IUInt,[]));
370       etyp = TInt(IUInt,[]);
371       espace = Any}
372
373let rec transf_struct_init id fld_init_list =
374  match fld_init_list with
375  | [] -> []
376  | (fld, i) :: rem ->
377      try
378        let bf = Hashtbl.find bitfield_table (id, fld.fld_name) in
379        let (el, rem') =
380          pack_bitfield_init id bf.bf_carrier fld_init_list in
381        ({fld_name = bf.bf_carrier; fld_typ = bf.bf_carrier_typ;
382          fld_bitfield = None},
383         Init_single {edesc = ECast(bf.bf_carrier_typ, or_expr_list el);
384                      etyp = bf.bf_carrier_typ;
385                      espace = Any})
386        :: transf_struct_init id rem'
387      with Not_found ->
388        (fld, i) :: transf_struct_init id rem
389
390let rec transf_init env i =
391  match i with
392  | Init_single e -> Init_single (transf_expr env e)
393  | Init_array il -> Init_array (List.map (transf_init env) il)
394  | Init_struct(id, fld_init_list) ->
395      let fld_init_list' =
396        List.map (fun (f, i) -> (f, transf_init env i)) fld_init_list in
397        Init_struct(id, transf_struct_init id fld_init_list')
398  | Init_union(id, fld, i) -> Init_union(id, fld, transf_init env i)
399
400let transf_decl env (sto, id, ty, init_opt) =
401  (sto, id, ty,
402   match init_opt with None -> None | Some i -> Some(transf_init env i))
403
404(* Programs *)
405
406let program p =
407  Transform.program
408    ~composite:transf_composite
409    ~decl: transf_decl
410    ~fundef:transf_fundef
411    p
Note: See TracBrowser for help on using the repository browser.