--- /dev/null
+(* *********************************************************************)
+(* *)
+(* 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 *)
+ bf_signed: bool } (* signed or unsigned *)
+
+(* 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 *)
+ else if pos + n > 8 * !config.sizeof_int then
+ (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
+ pack ((m.fld_name, pos, n, signed) :: accu) (pos + n) ms
+ 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
+ let carrier = sprintf "__bf%d" count in
+ let carrier_typ = TInt(unsigned_ikind_for_carrier nbits, []) in
+ List.iter
+ (fun (name, pos, sz, signed) ->
+ Hashtbl.add bitfield_table
+ (id, name)
+ {bf_carrier = carrier; bf_carrier_typ = carrier_typ;
+ bf_pos = pos; bf_size = sz; bf_signed = signed})
+ bitfields;
+ { fld_name = carrier; fld_typ = carrier_typ; fld_bitfield = None}
+ :: transf_members env id (count + 1) ml'
+ 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
+ {edesc = EBinop(Oshr, e2, right_shift_count bf, e2.etyp);
+ etyp = e2.etyp}
+
+(* 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,[])}
+
+(* Expressions *)
+
+let transf_expr env e =
+
+ let is_bitfield_access ty fieldname =
+ match unroll env ty with
+ | TStruct(id, _) ->
+ (try Some(Hashtbl.find bitfield_table (id, fieldname))
+ with Not_found -> None)
+ | _ -> None in
+
+ let is_bitfield_access_ptr ty fieldname =
+ match unroll env ty with
+ | TPtr(ty', _) -> is_bitfield_access ty' fieldname
+ | _ -> None in
+
+ let rec texp e =
+ match e.edesc with
+ | EConst _ -> e
+ | ESizeof _ -> e
+ | EVar _ -> e
+
+ | EUnop(Odot fieldname, e1) ->
+ let e1' = texp e1 in
+ begin match is_bitfield_access e1.etyp fieldname with
+ | None ->
+ {edesc = EUnop(Odot fieldname, e1'); etyp = e.etyp}
+ | Some bf ->
+ bitfield_extract bf
+ {edesc = EUnop(Odot bf.bf_carrier, e1');
+ etyp = bf.bf_carrier_typ}
+ end
+
+ | EUnop(Oarrow fieldname, e1) ->
+ let e1' = texp e1 in
+ begin match is_bitfield_access_ptr e1.etyp fieldname with
+ | None ->
+ {edesc = EUnop(Oarrow fieldname, e1'); etyp = e.etyp}
+ | Some bf ->
+ bitfield_extract bf
+ {edesc = EUnop(Oarrow bf.bf_carrier, e1');
+ etyp = bf.bf_carrier_typ}
+ end
+
+ | EUnop(op, e1) ->
+ (* Note: simplified expr, so no ++/-- *)
+ {edesc = EUnop(op, texp e1); etyp = e.etyp}
+
+ | EBinop(Oassign, e1, e2, ty) ->
+ begin match e1.edesc with
+ | EUnop(Odot fieldname, e11) ->
+ let lhs = texp e11 in let rhs = texp e2 in
+ begin match is_bitfield_access e11.etyp fieldname with
+ | None ->
+ {edesc = EBinop(Oassign,
+ {edesc = EUnop(Odot fieldname, lhs);
+ etyp = e1.etyp},
+ rhs, ty);
+ etyp = e.etyp}
+ | Some bf ->
+ let carrier =
+ {edesc = EUnop(Odot bf.bf_carrier, lhs);
+ etyp = bf.bf_carrier_typ} in
+ {edesc = EBinop(Oassign, carrier,
+ bitfield_assign bf carrier rhs,
+ carrier.etyp);
+ etyp = carrier.etyp}
+ end
+ | EUnop(Oarrow fieldname, e11) ->
+ let lhs = texp e11 in let rhs = texp e2 in
+ begin match is_bitfield_access_ptr e11.etyp fieldname with
+ | None ->
+ {edesc = EBinop(Oassign,
+ {edesc = EUnop(Oarrow fieldname, lhs);
+ etyp = e1.etyp},
+ rhs, ty);
+ etyp = e.etyp}
+ | Some bf ->
+ let carrier =
+ {edesc = EUnop(Oarrow bf.bf_carrier, lhs);
+ etyp = bf.bf_carrier_typ} in
+ {edesc = EBinop(Oassign, carrier,
+ bitfield_assign bf carrier rhs,
+ carrier.etyp);
+ etyp = carrier.etyp}
+ end
+ | _ ->
+ {edesc = EBinop(Oassign, texp e1, texp e2, e1.etyp); etyp = e1.etyp}
+ end
+
+ | EBinop(op, e1, e2, ty) ->
+ (* Note: simplified expr assumed, so no assign-op *)
+ {edesc = EBinop(op, texp e1, texp e2, ty); etyp = e.etyp}
+ | EConditional(e1, e2, e3) ->
+ {edesc = EConditional(texp e1, texp e2, texp e3); etyp = e.etyp}
+ | ECast(ty, e1) ->
+ {edesc = ECast(ty, texp e1); etyp = e.etyp}
+ | ECall(e1, el) ->
+ {edesc = ECall(texp e1, List.map texp el); etyp = e.etyp}
+
+ in texp e
+
+(* Statements *)
+
+let rec transf_stmt env s =
+ match s.sdesc with
+ | Sskip -> s
+ | Sdo e ->
+ {sdesc = Sdo(transf_expr env e); sloc = s.sloc}
+ | Sseq(s1, s2) ->
+ {sdesc = Sseq(transf_stmt env s1, transf_stmt env s2); sloc = s.sloc }
+ | Sif(e, s1, s2) ->
+ {sdesc = Sif(transf_expr env e, transf_stmt env s1, transf_stmt env s2);
+ sloc = s.sloc}
+ | Swhile(e, s1) ->
+ {sdesc = Swhile(transf_expr env e, transf_stmt env s1);
+ sloc = s.sloc}
+ | Sdowhile(s1, e) ->
+ {sdesc = Sdowhile(transf_stmt env s1, transf_expr env e);
+ sloc = s.sloc}
+ | Sfor(s1, e, s2, s3) ->
+ {sdesc = Sfor(transf_stmt env s1, transf_expr env e, transf_stmt env s2,
+ transf_stmt env s3);
+ sloc = s.sloc}
+ | Sbreak -> s
+ | Scontinue -> s
+ | Sswitch(e, s1) ->
+ {sdesc = Sswitch(transf_expr env e, transf_stmt env s1); sloc = s.sloc}
+ | Slabeled(lbl, s) ->
+ {sdesc = Slabeled(lbl, transf_stmt env s); sloc = s.sloc}
+ | Sgoto lbl -> s
+ | Sreturn None -> s
+ | Sreturn (Some e) ->
+ {sdesc = Sreturn(Some(transf_expr env e)); sloc = s.sloc}
+ | Sblock _ | Sdecl _ ->
+ assert false (* should not occur in unblocked code *)
+
+(* Functions *)
+
+let transf_fundef env f =
+ { f with fd_body = transf_stmt env f.fd_body }
+
+(* 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
+ | Init_single e -> Init_single (transf_expr env e)
+ | 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))
+
+(* Programs *)
+
+let program p =
+ Transform.program
+ ~composite:transf_composite
+ ~decl: transf_decl
+ ~fundef:transf_fundef
+ p
projects / pkg-cerco / acc-trusted.git / blobdiff