diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index 8d5ea86299..4546fda32e 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -34,6 +34,24 @@ struct let size_of_type_in_bytes typ = intdom_of_int (Cilfacade.bytesSizeOf typ) + let offs_lt_zero offs = + try ID.lt offs (intdom_of_int 0) + with IntDomain.ArithmeticOnIntegerBot _ -> None + + let check_deref_offset_bounds ptr_size offs = + let ptr_size_le_offs = + try ID.le ptr_size offs + with IntDomain.ArithmeticOnIntegerBot _ -> None + in + offs_lt_zero offs, ptr_size_le_offs + + let check_ptr_offset_bounds ptr_size offs = + let ptr_size_lt_offs = + try ID.lt ptr_size offs + with IntDomain.ArithmeticOnIntegerBot _ -> None + in + offs_lt_zero offs, ptr_size_lt_offs + let rec exp_contains_a_ptr (exp:exp) = match exp with | Const _ @@ -290,23 +308,17 @@ struct | `Lifted es -> let casted_es = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) es in (* TODO: proper castkind *) let casted_offs = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) offs_intdom in (* TODO: proper castkind *) - let ptr_size_lt_offs = - let one = intdom_of_int 1 in - let casted_es = ID.sub casted_es one in - begin try ID.lt casted_es casted_offs - with IntDomain.ArithmeticOnIntegerBot _ -> None - end - in let behavior = Undefined MemoryOutOfBoundsAccess in let cwe_number = 823 in - begin match ptr_size_lt_offs with - | Some true -> + begin match check_deref_offset_bounds casted_es casted_offs with + | Some true, _ + | _, Some true -> (set_mem_safety_flag InvalidDeref; M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of lval dereference expression is %a (in bytes). It is offset by %a (in bytes). Memory out-of-bounds access must occur" ID.pretty casted_es ID.pretty casted_offs); Checks.warn Checks.Category.InvalidMemoryAccess "Size of lval dereference expression is %a (in bytes). It is offset by %a (in bytes). Memory out-of-bounds access must occur" ID.pretty casted_es ID.pretty casted_offs - | Some false -> + | Some false, Some false -> Checks.safe Checks.Category.InvalidMemoryAccess - | None -> + | _ -> (set_mem_safety_flag InvalidDeref; M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Could not compare size of lval dereference expression (%a) (in bytes) with offset by (%a) (in bytes). Memory out-of-bounds access might occur" ID.pretty casted_es ID.pretty casted_offs); Checks.warn Checks.Category.InvalidMemoryAccess "Could not compare size of lval dereference expression (%a) (in bytes) with offset by (%a) (in bytes). Memory out-of-bounds access might occur" ID.pretty casted_es ID.pretty casted_offs @@ -343,15 +355,15 @@ struct | `Lifted ps, ao -> let casted_ps = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) ps in (* TODO: proper castkind *) let casted_ao = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) ao in (* TODO: proper castkind *) - let ptr_size_lt_offs = ID.lt casted_ps casted_ao in - begin match ptr_size_lt_offs with - | Some true -> + begin match check_ptr_offset_bounds casted_ps casted_ao with + | Some true, _ + | _, Some true -> set_mem_safety_flag InvalidDeref; M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer is %a (in bytes). It is offset by %a (in bytes) due to pointer arithmetic. Memory out-of-bounds access must occur" ID.pretty casted_ps ID.pretty casted_ao; Checks.warn Checks.Category.InvalidMemoryAccess "Size of pointer is %a (in bytes). It is offset by %a (in bytes) due to pointer arithmetic. Memory out-of-bounds access must occur" ID.pretty casted_ps ID.pretty casted_ao - | Some false -> + | Some false, Some false -> Checks.safe Checks.Category.InvalidMemoryAccess - | None -> + | _ -> set_mem_safety_flag InvalidDeref; M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Could not compare size of pointer (%a) (in bytes) with offset by (%a) (in bytes). Memory out-of-bounds access might occur" ID.pretty casted_ps ID.pretty casted_ao; Checks.warn Checks.Category.InvalidMemoryAccess "Could not compare size of pointer (%a) (in bytes) with offset by (%a) (in bytes). Memory out-of-bounds access might occur" ID.pretty casted_ps ID.pretty casted_ao @@ -431,15 +443,15 @@ struct | `Lifted ps, `Lifted o -> let casted_ps = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) ps in (* TODO: proper castkind *) let casted_o = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) o in (* TODO: proper castkind *) - let ptr_size_lt_offs = ID.lt casted_ps casted_o in - begin match ptr_size_lt_offs with - | Some true -> + begin match check_ptr_offset_bounds casted_ps casted_o with + | Some true, _ + | _, Some true -> set_mem_safety_flag InvalidDeref; M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer in expression %a is %a (in bytes). It is offset by %a (in bytes). Memory out-of-bounds access must occur" d_exp binopexp ID.pretty casted_ps ID.pretty casted_o; Checks.warn Checks.Category.InvalidMemoryAccess "Size of pointer in expression %a is %a (in bytes). It is offset by %a (in bytes). Memory out-of-bounds access must occur" d_exp binopexp ID.pretty casted_ps ID.pretty casted_o - | Some false -> + | Some false, Some false -> Checks.safe Checks.Category.InvalidMemoryAccess - | None -> + | _ -> set_mem_safety_flag InvalidDeref; M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Could not compare pointer size (%a) with offset (%a). Memory out-of-bounds access may occur" ID.pretty casted_ps ID.pretty casted_o; Checks.warn Checks.Category.InvalidMemoryAccess "Could not compare pointer size (%a) with offset (%a). Memory out-of-bounds access may occur" ID.pretty casted_ps ID.pretty casted_o diff --git a/tests/regression/74-invalid_deref/34-negative-index-after-ptr-increment.c b/tests/regression/74-invalid_deref/34-negative-index-after-ptr-increment.c new file mode 100644 index 0000000000..12eb084dfc --- /dev/null +++ b/tests/regression/74-invalid_deref/34-negative-index-after-ptr-increment.c @@ -0,0 +1,14 @@ +// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval +#include + +int main() { + int *b = malloc(2 * sizeof(int)); + int x; + + *b++ = 0; //NOWARN + + x = *(b - 2); //WARN + + free(b - 1); + return x; +} diff --git a/tests/regression/74-invalid_deref/35-negative-index-after-ptr-increment-index-syntax.c b/tests/regression/74-invalid_deref/35-negative-index-after-ptr-increment-index-syntax.c new file mode 100644 index 0000000000..ad4dd65b03 --- /dev/null +++ b/tests/regression/74-invalid_deref/35-negative-index-after-ptr-increment-index-syntax.c @@ -0,0 +1,14 @@ +// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval +#include + +int main() { + int *b = malloc(2 * sizeof(int)); + + *b++ = 0; //NOWARN + + if (b[-2]) //WARN + return 1; + + free(b - 1); + return 0; +} diff --git a/tests/regression/74-invalid_deref/36-one-past-pointer.c b/tests/regression/74-invalid_deref/36-one-past-pointer.c new file mode 100644 index 0000000000..b4ceb506d7 --- /dev/null +++ b/tests/regression/74-invalid_deref/36-one-past-pointer.c @@ -0,0 +1,12 @@ +// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval +#include +#include + +int main(void) { + char *buf = malloc(4); + char *end; + end = buf + 4; //NOWARN + printf("%p", (void *) end); //NOWARN + free(buf); + return 0; +} diff --git a/tests/regression/74-invalid_deref/37-one-past-deref-offset.c b/tests/regression/74-invalid_deref/37-one-past-deref-offset.c new file mode 100644 index 0000000000..8c441d4793 --- /dev/null +++ b/tests/regression/74-invalid_deref/37-one-past-deref-offset.c @@ -0,0 +1,16 @@ +// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval +#include + +struct S { + unsigned char a; + unsigned char b:2; + unsigned char c:2; + unsigned char d; +} __attribute__((packed)); + +int main(void) { + struct S *p = malloc(2); + p->d = 1; //WARN + free(p); + return 0; +}