Merge pull request #1679 from goblint/offset-to_index-bytes

Change `Offset.MakeLattice.to_index` to return bytes, not bits

Author: sim642

src/analyses/base.ml

@@ -271,8 +271,8 @@ struct
           let n_offset = iDtoIdx n in
           begin match t with
             | Some t ->
-              let (f_offset_bits, _) = bitsOffset t (Field (f, NoOffset)) in
-              let f_offset = IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int (f_offset_bits / 8)) in
+              let f_offset_bytes = Cilfacade.bytesOffsetOnly t (Field (f, NoOffset)) in
+              let f_offset = IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int f_offset_bytes) in
               begin match IdxDom.(to_bool (eq f_offset (neg n_offset))) with
                 | Some true -> `NoOffset
                 | _ -> `Field (f, `Index (n_offset, `NoOffset))
@@ -2289,8 +2289,7 @@ struct
       ID.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int x)
     in
     let size_of_type_in_bytes typ =
-      let typ_size_in_bytes = (bitsSizeOf typ) / 8 in
-      intdom_of_int typ_size_in_bytes
+      intdom_of_int (Cilfacade.bytesSizeOf typ)
     in
     if points_to_heap_only man ptr then
       (* Ask for BlobSize from the base address (the second component being set to true) in order to avoid BlobSize giving us bot *)

src/analyses/memOutOfBounds.ml

@@ -32,8 +32,7 @@ struct
     ID.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int x)
 
   let size_of_type_in_bytes typ =
-    let typ_size_in_bytes = (bitsSizeOf typ) / 8 in
-    intdom_of_int typ_size_in_bytes
+    intdom_of_int (Cilfacade.bytesSizeOf typ)
 
   let rec exp_contains_a_ptr (exp:exp) =
     match exp with
@@ -149,8 +148,8 @@ struct
     | `NoOffset -> intdom_of_int 0
     | `Field (field, o) ->
       let field_as_offset = Field (field, NoOffset) in
-      let bits_offset, _size = GoblintCil.bitsOffset (TComp (field.fcomp, [])) field_as_offset in
-      let bytes_offset = intdom_of_int (bits_offset / 8) in
+      let bytes_offset = Cilfacade.bytesOffsetOnly (TComp (field.fcomp, [])) field_as_offset in
+      let bytes_offset = intdom_of_int bytes_offset in
       let remaining_offset = offs_to_idx field.ftype o in
       begin
         try ID.add bytes_offset remaining_offset
@@ -279,7 +278,7 @@ struct
              M.warn "Size of lval dereference expression %a is bot. Out-of-bounds memory access may occur" d_exp e)
           | `Lifted es ->
             let casted_es = ID.cast_to (Cilfacade.ptrdiff_ikind ()) es in
-            let casted_offs = ID.div (ID.cast_to (Cilfacade.ptrdiff_ikind ()) offs_intdom) (ID.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int 8)) in
+            let casted_offs = ID.cast_to (Cilfacade.ptrdiff_ikind ()) offs_intdom in
             let ptr_size_lt_offs =
               let one = intdom_of_int 1 in
               let casted_es = ID.sub casted_es one in

src/cdomain/value/cdomains/offset.ml

@@ -202,6 +202,8 @@ struct
     | `Index (_,o) -> `Index (Idx.top (), of_exp o)
     | `Field (f,o) -> `Field (f, of_exp o)
 
+  let eight = Z.of_int 8
+
   let to_index ?typ (offs: t): Idx.t =
     let idx_of_int x =
       Idx.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int x)
@@ -211,22 +213,24 @@ struct
       | `Field (field, o) ->
         let field_as_offset = Field (field, NoOffset) in
         let bits_offset, _size = GoblintCil.bitsOffset (TComp (field.fcomp, [])) field_as_offset  in
-        let bits_offset = idx_of_int bits_offset in
+        let bits_offset = Z.of_int bits_offset in
+        (* Interval of floor and ceil division in case bitfield offset. *)
+        let bytes_offset = Idx.of_interval (Cilfacade.ptrdiff_ikind ()) Z.(fdiv bits_offset eight, cdiv bits_offset eight) in
         let remaining_offset = offset_to_index_offset ~typ:field.ftype o in
-        GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () -> Idx.add bits_offset remaining_offset
+        GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () -> Idx.add bytes_offset remaining_offset
       | `Index (x, o) ->
-        let (item_typ, item_size_in_bits) =
+        let (item_typ, item_size_in_bytes) =
           match Option.map unrollType typ with
           | Some TArray(item_typ, _, _) ->
-            let item_size_in_bits = bitsSizeOf item_typ in
-            (Some item_typ, idx_of_int item_size_in_bits)
+            let item_size_in_bytes = Cilfacade.bytesSizeOf item_typ in
+            (Some item_typ, idx_of_int item_size_in_bytes)
           | _ ->
             (None, Idx.top ())
         in
         (* Binary operations on offsets should not generate overflow warnings in SV-COMP *)
-        let bits_offset = GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () -> Idx.mul item_size_in_bits x in
+        let bytes_offset = GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () -> Idx.mul item_size_in_bytes x in
         let remaining_offset = offset_to_index_offset ?typ:item_typ o in
-        GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () -> Idx.add bits_offset remaining_offset
+        GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () -> Idx.add bytes_offset remaining_offset
     in
     offset_to_index_offset ?typ offs
 

src/cdomain/value/cdomains/valueDomain.ml

@@ -992,7 +992,7 @@ struct
                 not @@ ask.is_multiple var
                 && not @@ Cil.isVoidType t      (* Size of value is known *)
                 && GobOption.exists (fun blob_size -> (* Size of blob is known *)
-                    Z.equal blob_size (Z.of_int @@ Cil.bitsSizeOf (TComp (toptype, []))/8)
+                    Z.equal blob_size (Z.of_int @@ Cilfacade.bytesSizeOf (TComp (toptype, [])))
                   ) blob_size_opt
               | _ -> false
             in

src/cdomains/lockDomain.ml

@@ -14,8 +14,8 @@ struct
 
   let semantic_equal_mval ((v, o): t) ((v', o'): Mval.t): bool option =
     if CilType.Varinfo.equal v v' then (
-      let (index1, _) = GoblintCil.bitsOffset v.vtype (Offset.Z.to_cil o) in (* TODO: better way to compute this? as Z.t not int *)
-      let index2: IndexDomain.t = ValueDomain.Offs.to_index ~typ:v.vtype o' in (* TODO: is this bits or bytes? *)
+      let index1 = Cilfacade.bytesOffsetOnly v.vtype (Offset.Z.to_cil o) in (* TODO: better way to compute this? as Z.t not int *)
+      let index2: IndexDomain.t = ValueDomain.Offs.to_index ~typ:v.vtype o' in
       match IndexDomain.equal_to (Z.of_int index1) index2 with
       | `Eq -> Some true
       | `Neq -> Some false

src/common/util/cilfacade.ml

@@ -381,6 +381,17 @@ let typeSigBlendAttributes baseAttrs =
   typeSigAddAttrs contageous
 
 
+let bytesSizeOf t =
+  let bits = bitsSizeOf t in
+  assert (bits mod 8 = 0);
+  bits / 8
+
+let bytesOffsetOnly t o =
+  let bits_offset, _ = bitsOffset t o in
+  assert (bits_offset mod 8 = 0);
+  bits_offset / 8
+
+
 (** {!Cil.mkCast} using our {!typeOf}. *)
 let mkCast ~(e: exp) ~(newt: typ) =
   let oldt =