Commit 0d74359a authored by Valentin Perrelle's avatar Valentin Perrelle

[Cil] Extract Cil.fieldBitsOffset from Cil.bitsOffset

parent 18624738
...@@ -1151,7 +1151,7 @@ and equalModuloPackedAlign attrs1 attrs2 = ...@@ -1151,7 +1151,7 @@ and equalModuloPackedAlign attrs1 attrs2 =
Raises [Failure] if the fields are not equivalent. Raises [Failure] if the fields are not equivalent.
If [mustCheckOffsets] is true, then there is already a difference in the If [mustCheckOffsets] is true, then there is already a difference in the
composite type, so each field must be checked. *) composite type, so each field must be checked. *)
and checkFieldsEqualModuloPackedAlign ~mustCheckOffsets typ_ci1 typ_ci2 f1 f2 = and checkFieldsEqualModuloPackedAlign ~mustCheckOffsets f1 f2 =
if f1.fbitfield <> f2.fbitfield then if f1.fbitfield <> f2.fbitfield then
raise (Failure "different bitfield info"); raise (Failure "different bitfield info");
if mustCheckOffsets || not (equal_attributes_for_merge f1.fattr f2.fattr) then if mustCheckOffsets || not (equal_attributes_for_merge f1.fattr f2.fattr) then
...@@ -1160,11 +1160,8 @@ and checkFieldsEqualModuloPackedAlign ~mustCheckOffsets typ_ci1 typ_ci2 f1 f2 = ...@@ -1160,11 +1160,8 @@ and checkFieldsEqualModuloPackedAlign ~mustCheckOffsets typ_ci1 typ_ci2 f1 f2 =
in which case the difference may be safely ignored *) in which case the difference may be safely ignored *)
begin begin
try try
let offs1, width1 = let offs1, width1 = Cil.fieldBitsOffset f1
Cil.bitsOffset typ_ci1 (Field (f1, NoOffset)) and offs2, width2 = Cil.fieldBitsOffset f2
in
let offs2, width2 =
Cil.bitsOffset typ_ci2 (Field (f2, NoOffset))
in in
if not (equalModuloPackedAlign f1.fattr f2.fattr) if not (equalModuloPackedAlign f1.fattr f2.fattr)
|| offs1 <> offs2 || width1 <> width2 then || offs1 <> offs2 || width1 <> width2 then
...@@ -1252,12 +1249,9 @@ and matchCompInfo (oldfidx: int) (oldci: compinfo) ...@@ -1252,12 +1249,9 @@ and matchCompInfo (oldfidx: int) (oldci: compinfo)
[%a] vs [%a]" [%a] vs [%a]"
pp_attrs attrs pp_attrs oldattrs)) pp_attrs attrs pp_attrs oldattrs))
in in
let typ_ci = TComp(ci, {scache = Not_Computed}, []) in
let typ_oldci = TComp(oldci, {scache = Not_Computed}, []) in
List.iter2 List.iter2
(fun oldf f -> (fun oldf f ->
checkFieldsEqualModuloPackedAlign ~mustCheckOffsets checkFieldsEqualModuloPackedAlign ~mustCheckOffsets f oldf;
typ_ci typ_oldci f oldf;
(* Make sure the types are compatible *) (* Make sure the types are compatible *)
(* Note: 6.2.7 §1 states that the names of the fields should be the (* Note: 6.2.7 §1 states that the names of the fields should be the
same. We do not force this for now, but could do it. *) same. We do not force this for now, but could do it. *)
......
...@@ -248,8 +248,7 @@ let rec pretty_bits_internal env bfinfo typ ~align ~start ~stop = ...@@ -248,8 +248,7 @@ let rec pretty_bits_internal env bfinfo typ ~align ~start ~stop =
try try
let full_fields_to_print = List.fold_left let full_fields_to_print = List.fold_left
(fun acc field -> (fun acc field ->
let current_offset = Field (field,NoOffset) in let start_o,width_o = fieldBitsOffset field in
let start_o,width_o = bitsOffset typ current_offset in
let start_o,width_o = let start_o,width_o =
Integer.of_int start_o, Integer.of_int width_o Integer.of_int start_o, Integer.of_int width_o
in in
......
...@@ -433,13 +433,13 @@ and fieldinfo = { ...@@ -433,13 +433,13 @@ and fieldinfo = {
expression. *) expression. *)
mutable fsize_in_bits: int option; mutable fsize_in_bits: int option;
(** (Deprecated. Use {!Cil.bitsOffset} instead.) Similar to [fbitfield] for (** (Deprecated. Use {!Cil.fieldBitsOffset} or {!Cil.bitsOffset} instead.)
all types of fields. Similar to [fbitfield] for all types of fields.
@deprecated only Jessie uses this *) @deprecated only Jessie uses this *)
mutable foffset_in_bits: int option; mutable foffset_in_bits: int option;
(** Offset at which the field starts in the structure. Do not read directly, (** Offset at which the field starts in the structure. Do not read directly,
but use {!Cil.bitsOffset} instead. *) but use {!Cil.fieldBitsOffset} or {!Cil.bitsOffset} instead. *)
mutable fpadding_in_bits: int option; mutable fpadding_in_bits: int option;
(** (Deprecated.) Store the size of the padding that follows the field, if any. (** (Deprecated.) Store the size of the padding that follows the field, if any.
......
...@@ -1833,10 +1833,11 @@ class cil_printer () = object (self) ...@@ -1833,10 +1833,11 @@ class cil_printer () = object (self)
self#attributes fi.fattr; self#attributes fi.fattr;
if Kernel.(is_debug_key_enabled dkey_print_field_offsets) then if Kernel.(is_debug_key_enabled dkey_print_field_offsets) then
try try
let (offset, size) = Cil.bitsOffset fi.ftype (Field (fi, NoOffset)) in let (offset, size) = Cil.fieldBitsOffset fi in
let first = offset in let first = offset in
let last = offset + size - 1 in let last = if size > 0 then Some (offset + size - 1) else None in
fprintf fmt " /* bits %d .. %d */" first last let pp_opt fmt = Pretty_utils.pp_opt ~none:"" Format.pp_print_int fmt in
fprintf fmt " /* bits %d .. %a */" first pp_opt last
with Cil.SizeOfError _ -> () with Cil.SizeOfError _ -> ()
method private opt_funspec fmt funspec = method private opt_funspec fmt funspec =
......
...@@ -4419,6 +4419,29 @@ and sizeOf ~loc t = ...@@ -4419,6 +4419,29 @@ and sizeOf ~loc t =
integer ~loc ((bitsSizeOf t) lsr 3) integer ~loc ((bitsSizeOf t) lsr 3)
with SizeOfError _ -> new_exp ~loc (SizeOf(t)) with SizeOfError _ -> new_exp ~loc (SizeOf(t))
and fieldBitsOffset (f : fieldinfo) : int * int =
if not f.fcomp.cstruct (* union *) then
0, bitsSizeOf f.ftype
else begin
if f.foffset_in_bits = None then begin
let aux ~last acc fi =
let acc' = offsetOfFieldAcc ~last ~fi ~sofar:acc in
fi.fsize_in_bits <- Some acc'.oaLastFieldWidth;
fi.foffset_in_bits <- Some acc'.oaLastFieldStart;
acc'
in
ignore (
fold_struct_fields aux
{ oaFirstFree = 0;
oaLastFieldStart = 0;
oaLastFieldWidth = 0;
oaPrevBitPack = None }
f.fcomp.cfields
);
end;
Extlib.the f.foffset_in_bits, Extlib.the f.fsize_in_bits
end
and bitsOffset (baset: typ) (off: offset) : int * int = and bitsOffset (baset: typ) (off: offset) : int * int =
let rec loopOff (baset: typ) (width: int) (start: int) = function let rec loopOff (baset: typ) (width: int) (start: int) = function
NoOffset -> start, width NoOffset -> start, width
...@@ -4432,38 +4455,13 @@ and bitsOffset (baset: typ) (off: offset) : int * int = ...@@ -4432,38 +4455,13 @@ and bitsOffset (baset: typ) (off: offset) : int * int =
let bitsbt = bitsSizeOf bt in let bitsbt = bitsSizeOf bt in
loopOff bt bitsbt (start + ei * bitsbt) off loopOff bt bitsbt (start + ei * bitsbt) off
end end
| Field(f, off) when not f.fcomp.cstruct (* union *) -> | Field(f, off) ->
if check_invariants then if check_invariants then
assert (match unrollType baset with (match unrollType baset with
| TComp (ci, _, _) -> ci == f.fcomp | TComp (ci, _, _) -> assert (ci == f.fcomp)
| _ -> false); | _ -> assert false);
let offsbits, size = fieldBitsOffset f in
(* All union fields start at offset 0 *) (* All union fields start at offset 0 *)
loopOff f.ftype (bitsSizeOf f.ftype) start off
| Field(f, off) (* struct *) ->
if check_invariants then
assert (match unrollType baset with
| TComp (ci, _, _) -> ci == f.fcomp
| _ -> false);
if f.foffset_in_bits = None then begin
let aux ~last acc fi =
let acc' = offsetOfFieldAcc ~last ~fi ~sofar:acc in
fi.fsize_in_bits <- Some acc'.oaLastFieldWidth;
fi.foffset_in_bits <- Some acc'.oaLastFieldStart;
acc'
in
ignore (
fold_struct_fields aux
{ oaFirstFree = 0;
oaLastFieldStart = 0;
oaLastFieldWidth = 0;
oaPrevBitPack = None }
f.fcomp.cfields
);
end;
let offsbits, size =
Extlib.the f.foffset_in_bits, Extlib.the f.fsize_in_bits
in
loopOff f.ftype size (start + offsbits) off loopOff f.ftype size (start + offsbits) off
in in
loopOff baset (bitsSizeOf baset) 0 off loopOff baset (bitsSizeOf baset) 0 off
......
...@@ -2185,6 +2185,13 @@ val intOfAttrparam: attrparam -> int option ...@@ -2185,6 +2185,13 @@ val intOfAttrparam: attrparam -> int option
* this after you call {!Cil.initCIL}. *) * this after you call {!Cil.initCIL}. *)
val bitsOffset: typ -> offset -> int * int val bitsOffset: typ -> offset -> int * int
(** Give a field, returns the number of bits from the structure or union
* containing the field and the width (also expressed in bits) for the subobject
* denoted by the field. Raises {!Cil.SizeOfError} when it cannot compute
* the size. This function is architecture dependent, so you should only call
* this after you call {!Cil.initCIL}. *)
val fieldBitsOffset: fieldinfo -> int * int
(** Like map but try not to make a copy of the list *) (** Like map but try not to make a copy of the list *)
val mapNoCopy: ('a -> 'a) -> 'a list -> 'a list val mapNoCopy: ('a -> 'a) -> 'a list -> 'a list
......
...@@ -470,10 +470,9 @@ let memset_typ_offsm_int full_typ i = ...@@ -470,10 +470,9 @@ let memset_typ_offsm_int full_typ i =
(* Do not produce NaN or infinites here (unless they are accepted (* Do not produce NaN or infinites here (unless they are accepted
by the engine). *) by the engine). *)
if Fval.is_finite f = True then update size v' else update size v if Fval.is_finite f = True then update size v' else update size v
| TComp ({ cstruct = true ; cfields = l}, _, _) as tcomp -> (* struct *) | TComp ({ cstruct = true ; cfields = l}, _, _) -> (* struct *)
let aux_field offsm fi = let aux_field offsm fi =
let field = Field (fi, NoOffset) in let offset_fi = Int.of_int (fst (Cil.fieldBitsOffset fi)) in
let offset_fi = Int.of_int (fst (Cil.bitsOffset tcomp field)) in
aux fi.ftype (Int.add offset offset_fi) offsm aux fi.ftype (Int.add offset offset_fi) offsm
in in
List.fold_left aux_field offsm l List.fold_left aux_field offsm l
......
...@@ -1250,7 +1250,7 @@ and eval_toffset ~alarm_mode env typ toffset = ...@@ -1250,7 +1250,7 @@ and eval_toffset ~alarm_mode env typ toffset =
| TField (fi, remaining) -> | TField (fi, remaining) ->
let size_current default = let size_current default =
try Ival.of_int (fst (Cil.bitsOffset typ (Field(fi, NoOffset)))) try Ival.of_int (fst (Cil.fieldBitsOffset fi))
with Cil.SizeOfError _ -> default with Cil.SizeOfError _ -> default
in in
let attrs = Cil.filter_qualifier_attributes (Cil.typeAttrs typ) in let attrs = Cil.filter_qualifier_attributes (Cil.typeAttrs typ) in
......
...@@ -20,8 +20,6 @@ ...@@ -20,8 +20,6 @@
(* *) (* *)
(**************************************************************************) (**************************************************************************)
open Cil_types
module PLoc = struct module PLoc = struct
type value = Cvalue.V.t type value = Cvalue.V.t
...@@ -70,10 +68,10 @@ module PLoc = struct ...@@ -70,10 +68,10 @@ module PLoc = struct
let no_offset = Precise Precise_locs.offset_zero let no_offset = Precise Precise_locs.offset_zero
let forward_field typ field = function let forward_field _typ field = function
| Precise offset -> | Precise offset ->
begin try begin try
let field = fst (Cil.bitsOffset typ (Field (field, NoOffset))) in let field = fst (Cil.fieldBitsOffset field) in
let field_i = Integer.of_int field in let field_i = Integer.of_int field in
Precise (Precise_locs.shift_offset_by_singleton field_i offset) Precise (Precise_locs.shift_offset_by_singleton field_i offset)
with Cil.SizeOfError _ -> Precise (Precise_locs.offset_top) with Cil.SizeOfError _ -> Precise (Precise_locs.offset_top)
...@@ -189,12 +187,12 @@ module PLoc = struct ...@@ -189,12 +187,12 @@ module PLoc = struct
then `Bottom then `Bottom
else `Value (new_mem, Precise new_off) else `Value (new_mem, Precise new_off)
let backward_field typ field = function let backward_field _typ field = function
| Imprecise _ as x -> `Value x | Imprecise _ as x -> `Value x
| Precise offset -> | Precise offset ->
begin try begin try
let offset_ival = Precise_locs.imprecise_offset offset in let offset_ival = Precise_locs.imprecise_offset offset in
let field = fst (Cil.bitsOffset typ (Field (field, NoOffset))) in let field = fst (Cil.fieldBitsOffset field) in
let field_i = Integer.of_int (- field) in let field_i = Integer.of_int (- field) in
let ival = Ival.add_singleton_int field_i offset_ival in let ival = Ival.add_singleton_int field_i offset_ival in
if Ival.is_bottom ival if Ival.is_bottom ival
......
...@@ -99,15 +99,12 @@ struct ...@@ -99,15 +99,12 @@ struct
let typ = TComp(comp,Cil.empty_size_cache (),[]) in let typ = TComp(comp,Cil.empty_size_cache (),[]) in
H.add cache comp typ ; typ H.add cache comp typ ; typ
let field_offset cache fd = let field_offset _cache fd =
let typ = typ_of_comp cache fd.fcomp in Cil.fieldBitsOffset fd
let offset = Cil_types.(Field(fd,NoOffset)) in
Cil.bitsOffset typ offset
let range_field cache fd = let range_field cache fd =
let typ = typ_of_comp cache fd.fcomp in let typ = typ_of_comp cache fd.fcomp in
let offset = Cil_types.(Field(fd,NoOffset)) in Cil.fieldBitsOffset fd, Cil.bitsSizeOf typ
Cil.bitsOffset typ offset , Cil.bitsSizeOf typ
let range_index typ n = let range_index typ n =
let len = Cil.bitsSizeOf typ * n in (0 , len) , len let len = Cil.bitsSizeOf typ * n in (0 , len) , len
......
...@@ -489,12 +489,7 @@ let bits_sizeof_object = function ...@@ -489,12 +489,7 @@ let bits_sizeof_object = function
| C_array ainfo -> bits_sizeof_array ainfo | C_array ainfo -> bits_sizeof_array ainfo
let field_offset fd = let field_offset fd =
if fd.fcomp.cstruct then (* C struct *) fst (Cil.fieldBitsOffset fd) / 8
let ctype = TComp(fd.fcomp,Cil.empty_size_cache(),[]) in
let offset = Field(fd,NoOffset) in
fst (Cil.bitsOffset ctype offset) / 8
else (* CIL invariant: all C union fields start at offset 0 *)
0
(* Conforms to C-ISO 6.3.1.8 *) (* Conforms to C-ISO 6.3.1.8 *)
(* If same sign => greater rank. *) (* If same sign => greater rank. *)
......
...@@ -13,7 +13,7 @@ struct st { ...@@ -13,7 +13,7 @@ struct st {
struct fam { struct fam {
int a; int a;
char b; char b;
int fam[]; // check that a SizeOfError exception does not crash the printer int fam[]; // check that the printer handles flexible arrays members
}; };
int main() { int main() {
......
...@@ -9,7 +9,7 @@ struct st { ...@@ -9,7 +9,7 @@ struct st {
struct fam { struct fam {
int a ; /* bits 0 .. 31 */ int a ; /* bits 0 .. 31 */
char b ; /* bits 32 .. 39 */ char b ; /* bits 32 .. 39 */
int fam[] ; int fam[] ; /* bits 64 .. */
}; };
int main(void) int main(void)
{ {
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment