Bitfields.ml 16.5 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
(*                                                                     *)
(*  Copyright Institut National de Recherche en Informatique et en     *)
(*  Automatique.  All rights reserved.  This file is distributed       *)
(*  under the terms of the GNU General Public License as published by  *)
(*  the Free Software Foundation, either version 2 of the License, or  *)
(*  (at your option) any later version.  This file is also distributed *)
(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
(*                                                                     *)
(* *********************************************************************)

(* Elimination of bit fields in structs *)

(* Assumes: unblocked, simplified code.
   Preserves: unblocked, simplified code. *)

open Printf
open Machine
open C
open Cutil
open Transform

(* Info associated to each bitfield *)

type bitfield_info =
  { bf_carrier: string; (* name of underlying regular field *)
    bf_carrier_typ: typ; (* type of underlying regular field *)
    bf_pos: int;        (* start bit *)
    bf_size: int;       (* size in bit *)
34
35
36
    bf_signed: bool;    (* is field signed or unsigned? *)
    bf_signed_res: bool (* is result of extracting field signed or unsigned? *)
  }
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68

(* invariants:
     0 <= pos < bitsizeof(int)
     0 < sz <= bitsizeof(int)
     0 < pos + sz <= bitsizeof(int)
*)

(* Mapping (struct identifier, bitfield name) -> bitfield info *)

let bitfield_table =
      (Hashtbl.create 57: (ident * string, bitfield_info) Hashtbl.t)

(* Packing algorithm -- keep consistent with [Cutil.pack_bitfield]! *)

let unsigned_ikind_for_carrier nbits =
  if nbits <= 8 then IUChar else
  if nbits <= 8 * !config.sizeof_short then IUShort else
  if nbits <= 8 * !config.sizeof_int then IUInt else
  if nbits <= 8 * !config.sizeof_long then IULong else
  if nbits <= 8 * !config.sizeof_longlong then IULongLong else
  assert false

let pack_bitfields env id ml =
  let rec pack accu pos = function
  | [] ->
      (pos, accu, [])
  | m :: ms as ml ->
      match m.fld_bitfield with
      | None -> (pos, accu, ml)
      | Some n ->
          if n = 0 then
            (pos, accu, ms) (* bit width 0 means end of pack *)
69
          else if pos + n > 8 * !config.sizeof_int then
70
71
72
73
74
75
            (pos, accu, ml) (* doesn't fit in current word *)
          else begin
            let signed =
              match unroll env m.fld_typ with
              | TInt(ik, _) -> is_signed_ikind ik
              | _ -> assert false (* should never happen, checked in Elab *) in
76
77
78
79
80
            let signed2 =
              match unroll env (type_of_member env m) with
              | TInt(ik, _) -> is_signed_ikind ik
              | _ -> assert false (* should never happen, checked in Elab *) in
            pack ((m.fld_name, pos, n, signed, signed2) :: accu) (pos + n) ms
81
82
83
84
85
86
87
88
89
90
          end
  in pack [] 0 ml

let rec transf_members env id count = function
  | [] -> []
  | m :: ms as ml ->
      if m.fld_bitfield = None then
        m :: transf_members env id count ms
      else begin
        let (nbits, bitfields, ml') = pack_bitfields env id ml in
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
        if nbits = 0 then
          (* Lone zero-size bitfield: just ignore *)
          transf_members env id count ml'
        else begin
          (* Create integer field of sufficient size for this bitfield group *)
          let carrier = sprintf "__bf%d" count in
          let carrier_typ = TInt(unsigned_ikind_for_carrier nbits, []) in
          List.iter
            (fun (name, pos, sz, signed, signed2) ->
              if name <> "" then
                Hashtbl.add bitfield_table
                  (id, name)
                  {bf_carrier = carrier; bf_carrier_typ = carrier_typ;
                   bf_pos = pos; bf_size = sz;
                   bf_signed = signed; bf_signed_res = signed2})
            bitfields;
          { fld_name = carrier; fld_typ = carrier_typ; fld_bitfield = None}
          :: transf_members env id (count + 1) ml'
        end
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
      end

let transf_composite env su id ml =
  match su with
  | Struct -> transf_members env id 1 ml
  | Union  -> ml

(* Bitfield manipulation expressions *)

let left_shift_count bf =
  intconst 
    (Int64.of_int (8 * !config.sizeof_int - (bf.bf_pos + bf.bf_size)))
    IInt

let right_shift_count bf =
  intconst 
    (Int64.of_int (8 * !config.sizeof_int - bf.bf_size))
    IInt

let insertion_mask bf =
  let m =
    Int64.shift_left
      (Int64.pred (Int64.shift_left 1L bf.bf_size))
      bf.bf_pos in
  (* Give the mask an hexadecimal string representation, nicer to read *)
  {edesc = EConst(CInt(m, IUInt, sprintf "0x%LXU" m)); etyp = TInt(IUInt, [])}

(* Extract the value of a bitfield *)

(* Reference C code:

unsigned int bitfield_unsigned_extract(unsigned int x, int ofs, int sz)
{
  return (x << (BITSIZE_UINT - (ofs + sz))) >> (BITSIZE_UINT - sz);
}

signed int bitfield_signed_extract(unsigned int x, int ofs, int sz)
{
  return ((signed int) (x << (BITSIZE_UINT - (ofs + sz))))
         >> (BITSIZE_UINT - sz);
}

*)

let bitfield_extract bf carrier =
  let e1 =
    {edesc = EBinop(Oshl, carrier, left_shift_count bf, TInt(IUInt, []));
     etyp = carrier.etyp} in
  let ty = TInt((if bf.bf_signed then IInt else IUInt), []) in
  let e2 =
    {edesc = ECast(ty, e1); etyp = ty} in
161
162
163
164
165
166
167
  let e3 =
    {edesc = EBinop(Oshr, e2, right_shift_count bf, e2.etyp);
     etyp = ty} in
  if bf.bf_signed_res = bf.bf_signed then e3 else begin
    let ty' = TInt((if bf.bf_signed_res then IInt else IUInt), []) in
    {edesc = ECast(ty', e3); etyp = ty'}
  end
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196

(* Assign a bitfield within a carrier *)

(* Reference C code:

unsigned int bitfield_insert(unsigned int x, int ofs, int sz, unsigned int y)
{
  unsigned int mask = ((1U << sz) - 1) << ofs;
  return (x & ~mask) | ((y << ofs) & mask);
}

*)

let bitfield_assign bf carrier newval =
  let msk = insertion_mask bf in
  let notmsk = {edesc = EUnop(Onot, msk); etyp = msk.etyp} in
  let newval_shifted =
    {edesc = EBinop(Oshl, newval, intconst (Int64.of_int bf.bf_pos) IUInt,
                    TInt(IUInt,[]));
     etyp = TInt(IUInt,[])} in
  let newval_masked =
    {edesc = EBinop(Oand, newval_shifted, msk, TInt(IUInt,[]));
     etyp = TInt(IUInt,[])}
  and oldval_masked =
    {edesc = EBinop(Oand, carrier, notmsk, TInt(IUInt,[]));
     etyp = TInt(IUInt,[])} in
  {edesc = EBinop(Oor,  oldval_masked, newval_masked,  TInt(IUInt,[]));
   etyp =  TInt(IUInt,[])}

xleroy's avatar
xleroy committed
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
(* Detect invariant l-values *)

let rec invariant_lvalue e =
  match e.edesc with
  | EVar _ -> true
  | EUnop(Oderef, {edesc = EVar _}) -> true   (* to check *)
  | EUnop(Odot _, e1) -> invariant_lvalue e1
  | _ -> false

(* Bind a l-value to a temporary variable if it is not invariant. *)

let bind_lvalue e fn =
  if invariant_lvalue e then
    fn e
  else begin
    let tmp = new_temp (TPtr(e.etyp, [])) in
    ecomma (eassign tmp (eaddrof e))
           (fn {edesc = EUnop(Oderef, tmp); etyp = e.etyp})
  end

(* Transformation of operators *)

let op_for_incr_decr = function
  | Opreincr -> Oadd
  | Opredecr -> Osub
  | Opostincr -> Oadd
  | Opostdecr -> Osub
  | _ -> assert false
225

xleroy's avatar
xleroy committed
226
227
228
229
230
231
232
233
234
235
236
237
let op_for_assignop = function
  | Oadd_assign -> Oadd
  | Osub_assign -> Osub
  | Omul_assign -> Omul
  | Odiv_assign -> Odiv
  | Omod_assign -> Omod
  | Oand_assign -> Oand
  | Oor_assign -> Oor 
  | Oxor_assign -> Oxor
  | Oshl_assign -> Oshl
  | Oshr_assign -> Oshr
  | _ -> assert false
238

xleroy's avatar
xleroy committed
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
(* Check whether a field access (e.f or e->f) is a bitfield access.
   If so, return carrier expression (e and *e, respectively)
   and bitfield_info *)

let rec is_bitfield_access env e =
  match e.edesc with
  | EUnop(Odot fieldname, e1) ->
      begin match unroll env e1.etyp with
      | TStruct(id, _) ->
          (try Some(e1, Hashtbl.find bitfield_table (id, fieldname))
           with Not_found -> None)
      | _ ->
          None
      end
  | EUnop(Oarrow fieldname, e1) ->
      begin match unroll env e1.etyp with
      | TPtr(ty, _) ->
          is_bitfield_access env
            {edesc = EUnop(Odot fieldname,
                           {edesc = EUnop(Oderef, e1); etyp = ty});
             etyp = e.etyp}
      | _ ->
          None
      end
  | _ -> None
264

xleroy's avatar
xleroy committed
265
(* Expressions *)
266

xleroy's avatar
xleroy committed
267
268
269
270
271
type context = Val | Effects

let transf_expr env ctx e =

  let rec texp ctx e =
272
273
274
275
276
    match e.edesc with
    | EConst _ -> e
    | ESizeof _ -> e
    | EVar _ -> e

xleroy's avatar
xleroy committed
277
278
    | EUnop(Odot s, e1) ->
        begin match is_bitfield_access env e with
279
        | None ->
xleroy's avatar
xleroy committed
280
281
282
            {edesc = EUnop(Odot s, texp Val e1); etyp = e.etyp}
        | Some(ex, bf) ->
            transf_read ex bf
283
        end
xleroy's avatar
xleroy committed
284
285
    | EUnop(Oarrow s, e1) ->
        begin match is_bitfield_access env e with
286
        | None ->
xleroy's avatar
xleroy committed
287
288
289
            {edesc = EUnop(Oarrow s, texp Val e1); etyp = e.etyp}
        | Some(ex, bf) ->
            transf_read ex bf
290
        end
xleroy's avatar
xleroy committed
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
    | EUnop((Opreincr|Opredecr) as op, e1) ->
        begin match is_bitfield_access env e1 with
        | None ->
            {edesc = EUnop(op, texp Val e1); etyp = e.etyp}
        | Some(ex, bf) ->
            transf_pre ctx (op_for_incr_decr op) ex bf e1.etyp
        end
    | EUnop((Opostincr|Opostdecr) as op, e1) ->
        begin match is_bitfield_access env e1 with
        | None ->
            {edesc = EUnop(op, texp Val e1); etyp = e.etyp}
        | Some(ex, bf) ->
            transf_post ctx (op_for_incr_decr op) ex bf e1.etyp
        end
    | EUnop(op, e1) -> 
        {edesc = EUnop(op, texp Val e1); etyp = e.etyp}
307
308

    | EBinop(Oassign, e1, e2, ty) ->
xleroy's avatar
xleroy committed
309
310
311
312
313
314
        begin match is_bitfield_access env e1 with
        | None ->
            {edesc = EBinop(Oassign, texp Val e1, texp Val e2, ty);
             etyp = e.etyp}
        | Some(ex, bf) ->
            transf_assign ctx ex bf e2
315
        end
xleroy's avatar
xleroy committed
316
317
318
319
320
321
322
323
324
325
326
327
328
    | EBinop((Oadd_assign|Osub_assign|Omul_assign|Odiv_assign
                         |Omod_assign|Oand_assign|Oor_assign|Oxor_assign
                         |Oshl_assign|Oshr_assign) as op,
             e1, e2, ty) ->
        begin match is_bitfield_access env e1 with
        | None ->
            {edesc = EBinop(op, texp Val e1, texp Val e2, ty); etyp = e.etyp}
        | Some(ex, bf) ->
            transf_assignop ctx (op_for_assignop op) ex bf e2 ty
        end
    | EBinop(Ocomma, e1, e2, ty) ->
        {edesc = EBinop(Ocomma, texp Effects e1, texp Val e2, ty);
         etyp = e.etyp}
329
    | EBinop(op, e1, e2, ty) ->
xleroy's avatar
xleroy committed
330
331
        {edesc = EBinop(op, texp Val e1, texp Val e2, ty); etyp = e.etyp}

332
    | EConditional(e1, e2, e3) ->
xleroy's avatar
xleroy committed
333
334
        {edesc = EConditional(texp Val e1, texp ctx e2, texp ctx e3);
         etyp = e.etyp}
335
    | ECast(ty, e1) ->
xleroy's avatar
xleroy committed
336
        {edesc = ECast(ty, texp Val e1); etyp = e.etyp}
337
    | ECall(e1, el) ->
xleroy's avatar
xleroy committed
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
        {edesc = ECall(texp Val e1, List.map (texp Val) el); etyp = e.etyp}

  and transf_read e bf =
    bitfield_extract bf
      {edesc = EUnop(Odot bf.bf_carrier, texp Val e); etyp = bf.bf_carrier_typ}

  and transf_assign ctx e1 bf e2 =
    bind_lvalue (texp Val e1) (fun base ->
      let carrier =
        {edesc = EUnop(Odot bf.bf_carrier, base); etyp = bf.bf_carrier_typ} in
      let asg =
        eassign carrier (bitfield_assign bf carrier (texp Val e2)) in
      if ctx = Val then ecomma asg (bitfield_extract bf carrier) else asg)

  and transf_assignop ctx op e1 bf e2 tyres =
    bind_lvalue (texp Val e1) (fun base ->
      let carrier =
        {edesc = EUnop(Odot bf.bf_carrier, base); etyp = bf.bf_carrier_typ} in
      let rhs =
        {edesc = EBinop(op, bitfield_extract bf carrier, texp Val e2, tyres);
         etyp = tyres} in
      let asg =
        eassign carrier (bitfield_assign bf carrier rhs) in
      if ctx = Val then ecomma asg (bitfield_extract bf carrier) else asg)

  and transf_pre ctx op e1 bf tyfield =
    transf_assignop ctx op e1 bf (intconst 1L IInt)
                                 (unary_conversion env tyfield)

  and transf_post ctx op e1 bf tyfield  =
    if ctx = Effects then
      transf_pre ctx op e1 bf tyfield
    else begin
      bind_lvalue (texp Val e1) (fun base ->
        let carrier =
          {edesc = EUnop(Odot bf.bf_carrier, base); etyp = bf.bf_carrier_typ} in
        let temp = new_temp tyfield in
        let tyres = unary_conversion env tyfield in
        let settemp = eassign temp (bitfield_extract bf carrier) in
        let rhs =
          {edesc = EBinop(op, temp, intconst 1L IInt, tyres); etyp = tyres} in
        let asg =
          eassign carrier (bitfield_assign bf carrier rhs) in
        ecomma (ecomma settemp asg) temp)
    end

  in texp ctx e
385
386
387
388
389
390
391

(* Statements *)

let rec transf_stmt env s =
  match s.sdesc with
  | Sskip -> s
  | Sdo e ->
xleroy's avatar
xleroy committed
392
      {sdesc = Sdo(transf_expr env Effects e); sloc = s.sloc}
393
394
395
  | Sseq(s1, s2) -> 
      {sdesc = Sseq(transf_stmt env s1, transf_stmt env s2); sloc = s.sloc }
  | Sif(e, s1, s2) ->
xleroy's avatar
xleroy committed
396
      {sdesc = Sif(transf_expr env Val e, transf_stmt env s1, transf_stmt env s2);
397
398
       sloc = s.sloc}
  | Swhile(e, s1) ->
xleroy's avatar
xleroy committed
399
      {sdesc = Swhile(transf_expr env Val e, transf_stmt env s1);
400
401
       sloc = s.sloc}
  | Sdowhile(s1, e) ->
xleroy's avatar
xleroy committed
402
      {sdesc = Sdowhile(transf_stmt env s1, transf_expr env Val e);
403
404
       sloc = s.sloc}
  | Sfor(s1, e, s2, s3) ->
xleroy's avatar
xleroy committed
405
406
      {sdesc = Sfor(transf_stmt env s1, transf_expr env Val e,
                    transf_stmt env s2, transf_stmt env s3);
407
408
409
410
       sloc = s.sloc}
  | Sbreak -> s
  | Scontinue -> s
  | Sswitch(e, s1) ->
xleroy's avatar
xleroy committed
411
412
      {sdesc = Sswitch(transf_expr env Val e, transf_stmt env s1);
       sloc = s.sloc}
413
414
415
416
417
  | Slabeled(lbl, s) ->
      {sdesc = Slabeled(lbl, transf_stmt env s); sloc = s.sloc}
  | Sgoto lbl -> s
  | Sreturn None -> s
  | Sreturn (Some e) ->
xleroy's avatar
xleroy committed
418
      {sdesc = Sreturn(Some(transf_expr env Val e)); sloc = s.sloc}
419
420
421
422
423
424
  | Sblock _ | Sdecl _ ->
      assert false     (* should not occur in unblocked code *)

(* Functions *)

let transf_fundef env f =
xleroy's avatar
xleroy committed
425
426
427
428
  reset_temps();
  let newbody = transf_stmt env f.fd_body in
  let temps = get_temps() in  
  { f with fd_locals = f.fd_locals @ temps; fd_body = newbody }
429

430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
(* Initializers *)

let bitfield_initializer bf i =
  match i with
  | Init_single e ->
      let m = Int64.pred (Int64.shift_left 1L bf.bf_size) in
      let e_mask =
        {edesc = EConst(CInt(m, IUInt, sprintf "0x%LXU" m));
         etyp = TInt(IUInt, [])} in
      let e_and =
        {edesc = EBinop(Oand, e, e_mask, TInt(IUInt,[]));
         etyp = TInt(IUInt,[])} in
      {edesc = EBinop(Oshl, e_and, intconst (Int64.of_int bf.bf_pos) IInt,
                      TInt(IUInt, []));
       etyp = TInt(IUInt, [])}
  | _ -> assert false

let rec pack_bitfield_init id carrier fld_init_list =
  match fld_init_list with
  | [] -> ([], [])
  | (fld, i) :: rem ->
      try
        let bf = Hashtbl.find bitfield_table (id, fld.fld_name) in
        if bf.bf_carrier <> carrier then
          ([], fld_init_list)
        else begin
          let (el, rem') = pack_bitfield_init id carrier rem in
          (bitfield_initializer bf i :: el, rem')
        end
      with Not_found ->
        ([], fld_init_list)

let rec or_expr_list = function
  | [] -> assert false
  | [e] -> e
  | e1 :: el ->
      {edesc = EBinop(Oor, e1, or_expr_list el, TInt(IUInt,[]));
       etyp = TInt(IUInt,[])}

let rec transf_struct_init id fld_init_list =
  match fld_init_list with
  | [] -> []
  | (fld, i) :: rem ->
      try
        let bf = Hashtbl.find bitfield_table (id, fld.fld_name) in
        let (el, rem') =
          pack_bitfield_init id bf.bf_carrier fld_init_list in
        ({fld_name = bf.bf_carrier; fld_typ = bf.bf_carrier_typ;
          fld_bitfield = None},
         Init_single {edesc = ECast(bf.bf_carrier_typ, or_expr_list el);
                      etyp = bf.bf_carrier_typ})
        :: transf_struct_init id rem'
      with Not_found ->
        (fld, i) :: transf_struct_init id rem

let rec transf_init env i =
  match i with
xleroy's avatar
xleroy committed
487
  | Init_single e -> Init_single (transf_expr env Val e)
488
489
490
491
492
493
494
495
496
497
498
  | Init_array il -> Init_array (List.map (transf_init env) il)
  | Init_struct(id, fld_init_list) ->
      let fld_init_list' =
        List.map (fun (f, i) -> (f, transf_init env i)) fld_init_list in
        Init_struct(id, transf_struct_init id fld_init_list')
  | Init_union(id, fld, i) -> Init_union(id, fld, transf_init env i)

let transf_decl env (sto, id, ty, init_opt) =
  (sto, id, ty,
   match init_opt with None -> None | Some i -> Some(transf_init env i))

499
500
501
(* Programs *)

let program p =
502
503
504
505
506
  Transform.program
    ~composite:transf_composite
    ~decl: transf_decl
    ~fundef:transf_fundef 
    p