diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 67e6276239..e3be4674d7 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -251,14 +251,9 @@ struct let bool_top ik = ID.(join (of_int ik Z.zero) (of_int ik Z.one)) in (* An auxiliary function for ptr arithmetic on array values. *) let addToAddr n (addr:Addr.t) = - let typeOffsetOpt o t = - try - Some (Cilfacade.typeOffset t o) - with Cilfacade.TypeOfError _ -> - None - in + let exception UnknownPtr in (* adds n to the last offset *) - let rec addToOffset n (t:typ option) = function + let rec addToOffset n (t : typ) ((v, off) : Addr.Mval.t) = function | `Index (i, `NoOffset) -> (* If we have arrived at the last Offset and it is an Index, we add our integer to it *) `Index(IdxDom.add i (iDtoIdx n), `NoOffset) @@ -267,31 +262,32 @@ struct * then check if we're subtracting exactly its offsetof. * If so, n cancels out f exactly. * This is to better handle container_of hacks. *) - 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 - begin match IdxDom.(to_bool (eq f_offset (neg n_offset))) with - | Some true -> `NoOffset - | _ -> `Field (f, `Index (n_offset, `NoOffset)) - end - | None -> `Field (f, `Index (n_offset, `NoOffset)) + 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 + begin match IdxDom.(to_bool (eq f_offset (neg (iDtoIdx n)))) with + | Some true -> `NoOffset + | _ when isArrayType f.ftype -> `Field (f, `Index (n, `NoOffset)) + | _ when GobOption.exists (Z.equal Z.zero) (ID.to_int n) -> `NoOffset (* adding (or subtracting) 0 to any type of pointer is ok *) + | _ -> raise UnknownPtr (* adding (or subtracting) anything else than 0 to a pointer that is non-indexable will yield an unknown pointer *) end | `Index (i, o) -> - let t' = BatOption.bind t (typeOffsetOpt (Index (integer 0, NoOffset))) in (* actual index value doesn't matter for typeOffset *) - `Index(i, addToOffset n t' o) - | `Field (f, o) -> - let t' = BatOption.bind t (typeOffsetOpt (Field (f, NoOffset))) in - `Field(f, addToOffset n t' o) - | `NoOffset -> `Index(iDtoIdx n, `NoOffset) + let t' = Cilfacade.typeOffset t NoOffset in (* actual index value doesn't matter for typeOffset *) + `Index(i, addToOffset n t' (Addr.Mval.add_offset (v, off) o) o) + | `Field (f, o) -> `Field(f, addToOffset n f.ftype (Addr.Mval.add_offset (v, off) o) o) + (* The following cases are only reached via the first call, but not recursively (as the previous cases catch those) *) + | `NoOffset when isArrayType (v.vtype) || is_alloc_var (Analyses.ask_of_ctx ctx) v -> `Index (iDtoIdx n, `NoOffset) + | `NoOffset when GobOption.exists (Z.equal Z.zero) (ID.to_int n) -> `NoOffset (* adding (or subtracting) 0 to any type of pointer is ok *) + | `NoOffset -> raise UnknownPtr (* adding (or subtracting) anything else than 0 to a pointer that is non-indexable will yield an unknown pointer *) in let default = function | Addr.NullPtr when GobOption.exists (Z.equal Z.zero) (ID.to_int n) -> Addr.NullPtr | _ -> Addr.UnknownPtr in match Addr.to_mval addr with - | Some (x, o) -> Addr.of_mval (x, addToOffset n (Some x.vtype) o) + | Some (x, o) -> ( + try Addr.of_mval (x, addToOffset n x.vtype (x,o) o) + with UnknownPtr -> default addr + ) | None -> default addr in let addToAddrOp p (n:ID.t):value = @@ -1172,9 +1168,6 @@ struct (* interpreter end *) - let is_not_alloc_var ctx v = - not (ctx.ask (Queries.IsAllocVar v)) - let is_not_heap_alloc_var ctx v = let is_alloc = ctx.ask (Queries.IsAllocVar v) in not is_alloc || (is_alloc && not (ctx.ask (Queries.IsHeapVar v))) @@ -1437,7 +1430,7 @@ struct (* If there's a non-heap var or an offset in the lval set, we answer with bottom *) (* If we're asking for the BlobSize from the base address, then don't check for offsets => we want to avoid getting bot *) if AD.exists (function - | Addr (v,o) -> is_not_alloc_var ctx v || (if not from_base_addr then o <> `NoOffset else false) + | Addr (v,o) -> is_not_alloc_var (Analyses.ask_of_ctx ctx) v || (if not from_base_addr then o <> `NoOffset else false) | _ -> false) a then Queries.Result.bot q else ( diff --git a/src/analyses/baseUtil.ml b/src/analyses/baseUtil.ml index dd77392404..c9dce4a496 100644 --- a/src/analyses/baseUtil.ml +++ b/src/analyses/baseUtil.ml @@ -12,3 +12,6 @@ let is_always_unknown variable = variable.vstorage = Extern || Ciltools.is_volat let is_excluded_from_earlyglobs v = List.mem v.vname (get_string_list "exp.exclude_from_earlyglobs") let is_excluded_from_invalidation v = List.mem v.vname (get_string_list "exp.exclude_from_invalidation") + +let is_alloc_var (a: Q.ask) (v: varinfo): bool = a.f (Queries.IsAllocVar v) +let is_not_alloc_var (a: Q.ask) (v: varinfo): bool = not (a.f (Queries.IsAllocVar v)) \ No newline at end of file diff --git a/src/analyses/baseUtil.mli b/src/analyses/baseUtil.mli index 7054cd57fc..cce25ca8f2 100644 --- a/src/analyses/baseUtil.mli +++ b/src/analyses/baseUtil.mli @@ -8,3 +8,5 @@ val is_volatile: varinfo -> bool val is_always_unknown: varinfo -> bool val is_excluded_from_earlyglobs: varinfo -> bool val is_excluded_from_invalidation: varinfo -> bool +val is_alloc_var: Queries.ask -> varinfo -> bool +val is_not_alloc_var: Queries.ask -> varinfo -> bool diff --git a/tests/regression/02-base/13-add-zero-to-struct-ptr.c b/tests/regression/02-base/13-add-zero-to-struct-ptr.c new file mode 100644 index 0000000000..1ccd2d6957 --- /dev/null +++ b/tests/regression/02-base/13-add-zero-to-struct-ptr.c @@ -0,0 +1,17 @@ +#include + +struct a { + pthread_mutex_t b; +}; +struct c { + struct a *conn; +} d(); + +int main() { + struct a str = {0}; + struct c axel = {0}; + axel.conn = &str; + pthread_mutex_t* ptr = &((axel.conn + 0)->b); + pthread_mutex_lock(ptr); + pthread_mutex_unlock(ptr); +} \ No newline at end of file diff --git a/tests/regression/02-base/14-add-nondet-to-int-ptr.c b/tests/regression/02-base/14-add-nondet-to-int-ptr.c new file mode 100644 index 0000000000..5acf00c604 --- /dev/null +++ b/tests/regression/02-base/14-add-nondet-to-int-ptr.c @@ -0,0 +1,14 @@ +// PARAM: --set ana.activated[+] memOutOfBounds +#include + +struct c { + int *conn; +} d(); + +int main() { + int str = {0}; + struct c axel = {0}; + axel.conn = &str; + int *ptr = (axel.conn + rand ()); + int x = *ptr + 1; // WARN +} \ No newline at end of file diff --git a/tests/regression/02-base/15-add-nondet-to-struct-ptr-with-offset.c b/tests/regression/02-base/15-add-nondet-to-struct-ptr-with-offset.c new file mode 100644 index 0000000000..3c846f8755 --- /dev/null +++ b/tests/regression/02-base/15-add-nondet-to-struct-ptr-with-offset.c @@ -0,0 +1,26 @@ +#include + +struct a { + pthread_mutex_t b; +}; +struct c { + struct a *conn; +} d(); + +int main() { + struct a str = {0}; + struct c axel = {0}; + axel.conn = &str.b; + pthread_mutex_t* ptr = axel.conn + rand(); + pthread_mutex_lock(ptr); + pthread_mutex_unlock(ptr); // WARN + pthread_mutex_t* ptr = axel.conn - rand(); + pthread_mutex_lock(ptr); + pthread_mutex_unlock(ptr); // WARN + pthread_mutex_t* ptr = axel.conn + 0; + pthread_mutex_lock(ptr); + pthread_mutex_unlock(ptr); // NOWARN + pthread_mutex_t* ptr = axel.conn - 0; + pthread_mutex_lock(ptr); + pthread_mutex_unlock(ptr); // NOWARN +} \ No newline at end of file