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