diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 2529398939..7ec726f26f 100644 --- a/src/analyses/base.ml +++ b/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)) @@ -2286,8 +2286,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 *) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index 462383bec8..6831d89dbe 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/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 diff --git a/src/cdomain/value/cdomains/offset.ml b/src/cdomain/value/cdomains/offset.ml index e8cba0afc5..2d51f60996 100644 --- a/src/cdomain/value/cdomains/offset.ml +++ b/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 diff --git a/src/cdomain/value/cdomains/valueDomain.ml b/src/cdomain/value/cdomains/valueDomain.ml index cf2e5012d4..9f879f3b63 100644 --- a/src/cdomain/value/cdomains/valueDomain.ml +++ b/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 diff --git a/src/cdomains/lockDomain.ml b/src/cdomains/lockDomain.ml index b71573d6f6..e7295f0b56 100644 --- a/src/cdomains/lockDomain.ml +++ b/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 diff --git a/src/common/util/cilfacade.ml b/src/common/util/cilfacade.ml index 6e86701858..68c1410f2a 100644 --- a/src/common/util/cilfacade.ml +++ b/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 =