Merge branch 'feature/cil/bitsOffset' into 'master'

[Cil] Extract Cil.fieldBitsOffset from Cil.bitsOffset

See merge request frama-c/frama-c!2920

src/kernel_internals/typing/mergecil.ml

@@ -1151,7 +1151,7 @@ and equalModuloPackedAlign attrs1 attrs2 =
    Raises [Failure] if the fields are not equivalent.
    If [mustCheckOffsets] is true, then there is already a difference in the
    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
     raise (Failure "different bitfield info");
   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 =
        in which case the difference may be safely ignored *)
     begin
       try
-        let offs1, width1 =
-          Cil.bitsOffset typ_ci1 (Field (f1, NoOffset))
-        in
-        let offs2, width2 =
-          Cil.bitsOffset typ_ci2 (Field (f2, NoOffset))
+        let offs1, width1 = Cil.fieldBitsOffset f1
+        and offs2, width2 = Cil.fieldBitsOffset f2
         in
         if not (equalModuloPackedAlign f1.fattr f2.fattr)
         || offs1 <> offs2 || width1 <> width2 then
@@ -1252,12 +1249,9 @@ and matchCompInfo (oldfidx: int) (oldci: compinfo)
                      [%a] vs [%a]"
                     pp_attrs attrs pp_attrs oldattrs))
         in
-        let typ_ci = TComp(ci, {scache = Not_Computed}, []) in
-        let typ_oldci = TComp(oldci, {scache = Not_Computed}, []) in
         List.iter2
           (fun oldf f ->
-             checkFieldsEqualModuloPackedAlign ~mustCheckOffsets
-               typ_ci typ_oldci f oldf;
+             checkFieldsEqualModuloPackedAlign ~mustCheckOffsets f oldf;
              (* Make sure the types are compatible *)
              (* 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. *)

src/kernel_services/analysis/bit_utils.ml

@@ -248,8 +248,7 @@ let rec pretty_bits_internal env bfinfo typ ~align ~start ~stop =
         try
           let full_fields_to_print = List.fold_left
             (fun acc field ->
-               let current_offset = Field (field,NoOffset) in
-               let start_o,width_o = bitsOffset typ current_offset in
+               let start_o,width_o = fieldBitsOffset field in
                let start_o,width_o =
                  Integer.of_int start_o, Integer.of_int width_o
                in

src/kernel_services/ast_data/cil_types.mli

@@ -436,13 +436,14 @@ and fieldinfo = {
       expression. *)
 
   mutable fsize_in_bits: int option;
-  (** (Deprecated. Use {!Cil.bitsOffset} instead.) Similar to [fbitfield] for
-      all types of fields.
-      @deprecated only Jessie uses this *)
+  (** Similar to [fbitfield] for all types of fields.
+      Do not read this field directly. Use {!Cil.fieldBitsOffset} or
+      {!Cil.bitsOffset} instead. *)
 
   mutable foffset_in_bits: int option;
-  (** Offset at which the field starts in the structure. Do not read directly,
-      but use {!Cil.bitsOffset} instead. *)
+  (** Offset at which the field starts in the structure.
+      Do not read this field directly. Use {!Cil.fieldBitsOffset} or
+      {!Cil.bitsOffset} instead. *)
 
   mutable fpadding_in_bits: int option;
   (** (Deprecated.) Store the size of the padding that follows the field, if any.

src/kernel_services/ast_printing/cil_printer.ml

@@ -1833,10 +1833,11 @@ class cil_printer () = object (self)
       self#attributes fi.fattr;
     if Kernel.(is_debug_key_enabled dkey_print_field_offsets) then
       try
-        let (offset, size) = Cil.bitsOffset fi.ftype (Field (fi, NoOffset)) in
+        let (offset, size) = Cil.fieldBitsOffset fi in
         let first = offset in
-        let last = offset + size - 1 in
-        fprintf fmt " /* bits %d .. %d */" first last
+        let last = if size > 0 then Some (offset + size - 1) else None in
+        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 _ -> ()
 
   method private opt_funspec fmt funspec =

src/kernel_services/ast_queries/cil.ml

@@ -4419,6 +4419,30 @@ and sizeOf ~loc t =
     integer ~loc ((bitsSizeOf t) lsr 3)
   with SizeOfError _ -> new_exp ~loc (SizeOf(t))
 
+and fieldBitsOffset (f : fieldinfo) : int * int =
+  if  not f.fcomp.cstruct (* union *) then
+    (* All union fields start at offset 0 *)
+    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 =
   let rec loopOff (baset: typ) (width: int) (start: int) = function
       NoOffset -> start, width
@@ -4432,38 +4456,12 @@ and bitsOffset (baset: typ) (off: offset) : int * int =
         let bitsbt = bitsSizeOf bt in
         loopOff bt bitsbt (start + ei * bitsbt) off
       end
-    | Field(f, off) when not f.fcomp.cstruct (* union *) ->
+    | Field(f, off) ->
       if check_invariants then
-        assert (match unrollType baset with
-            | TComp (ci, _, _) -> ci == f.fcomp
-            | _ -> false);
-      (* 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
+        (match unrollType baset with
+         | TComp (ci, _, _) -> assert (ci == f.fcomp)
+         | _ -> assert false);
+      let offsbits, size = fieldBitsOffset f in
       loopOff f.ftype size (start + offsbits) off
   in
   loopOff baset (bitsSizeOf baset) 0 off

src/kernel_services/ast_queries/cil.mli

@@ -2185,6 +2185,13 @@ val intOfAttrparam: attrparam -> int option
  * this after you call {!Cil.initCIL}. *)
 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 *)
 val mapNoCopy: ('a -> 'a) -> 'a list -> 'a list
 

src/plugins/value/domains/cvalue/builtins_memory.ml

@@ -470,10 +470,9 @@ let memset_typ_offsm_int full_typ i =
           (* Do not produce NaN or infinites here (unless they are accepted
              by the engine). *)
           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 field = Field (fi, NoOffset) in
-            let offset_fi = Int.of_int (fst (Cil.bitsOffset tcomp field)) in
+            let offset_fi = Int.of_int (fst (Cil.fieldBitsOffset fi)) in
             aux fi.ftype (Int.add offset offset_fi) offsm
           in
           List.fold_left aux_field offsm l

src/plugins/value/legacy/eval_terms.ml

@@ -1250,7 +1250,7 @@ and eval_toffset ~alarm_mode env typ toffset =
 
   | TField (fi, remaining) ->
     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
     in
     let attrs = Cil.filter_qualifier_attributes (Cil.typeAttrs typ) in

src/plugins/value/values/main_locations.ml

@@ -20,8 +20,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-open Cil_types
-
 module PLoc = struct
 
   type value = Cvalue.V.t
@@ -70,10 +68,10 @@ module PLoc = struct
 
   let no_offset = Precise Precise_locs.offset_zero
 
-  let forward_field typ field = function
+  let forward_field _typ field = function
     | Precise offset ->
       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
           Precise (Precise_locs.shift_offset_by_singleton field_i offset)
         with Cil.SizeOfError _ -> Precise (Precise_locs.offset_top)
@@ -189,12 +187,12 @@ module PLoc = struct
       then `Bottom
       else `Value (new_mem, Precise new_off)
 
-  let backward_field typ field = function
+  let backward_field _typ field = function
     | Imprecise _ as x -> `Value x
     | Precise offset ->
       begin try
           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 ival = Ival.add_singleton_int field_i offset_ival in
           if Ival.is_bottom ival

src/plugins/wp/Layout.ml

@@ -99,15 +99,12 @@ struct
       let typ = TComp(comp,Cil.empty_size_cache (),[]) in
       H.add cache comp typ ; typ
 
-  let field_offset cache fd =
-    let typ = typ_of_comp cache fd.fcomp in
-    let offset = Cil_types.(Field(fd,NoOffset)) in
-    Cil.bitsOffset typ offset
+  let field_offset _cache fd =
+    Cil.fieldBitsOffset fd
 
   let range_field cache fd =
     let typ = typ_of_comp cache fd.fcomp in
-    let offset = Cil_types.(Field(fd,NoOffset)) in
-    Cil.bitsOffset typ offset , Cil.bitsSizeOf typ
+    Cil.fieldBitsOffset fd, Cil.bitsSizeOf typ
 
   let range_index typ n =
     let len = Cil.bitsSizeOf typ * n in (0 , len) , len

src/plugins/wp/ctypes.ml

@@ -489,12 +489,7 @@ let bits_sizeof_object = function
   | C_array ainfo -> bits_sizeof_array ainfo
 
 let field_offset fd =
-  if fd.fcomp.cstruct then (* C struct *)
-    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
+  fst (Cil.fieldBitsOffset fd) / 8
 
 (* Conforms to C-ISO 6.3.1.8        *)
 (* If same sign => greater rank.    *)

tests/syntax/field-offsets.c

@@ -13,7 +13,7 @@ struct st {
 struct fam {
   int a;
   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() {

tests/syntax/oracle/field-offsets.res.oracle

@@ -9,7 +9,7 @@ struct st {
 struct fam {
    int a ; /* bits 0 .. 31 */
    char b ; /* bits 32 .. 39 */
-   int fam[] ;
+   int fam[] ; /* bits 64 ..  */
 };
 int main(void)
 {