From aad66bc6f691a9e3f2fdfc2ef4541b64fd29b0a7 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Sun, 18 Jun 2017 13:07:53 -0700 Subject: [PATCH] [inferbo] More tests Reviewed By: skcho Differential Revision: D5265505 fbshipit-source-id: 5fc05f9 --- .../codetoanalyze/c/bufferoverrun/arith.c | 57 +++++++ .../codetoanalyze/c/bufferoverrun/cast.c | 25 +++ .../codetoanalyze/c/bufferoverrun/issues.exp | 8 + .../codetoanalyze/c/bufferoverrun/sizeof.c | 5 + .../c/bufferoverrun/unreachable.c | 11 ++ .../cpp/bufferoverrun/issues.exp | 7 + .../cpp/bufferoverrun/repro1.cpp | 144 ++++++++++++++++++ .../cpp/bufferoverrun/vector.cpp | 30 ++++ 8 files changed, 287 insertions(+) create mode 100644 infer/tests/codetoanalyze/c/bufferoverrun/arith.c create mode 100644 infer/tests/codetoanalyze/c/bufferoverrun/cast.c create mode 100644 infer/tests/codetoanalyze/cpp/bufferoverrun/repro1.cpp diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c new file mode 100644 index 000000000..426dc9f50 --- /dev/null +++ b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c @@ -0,0 +1,57 @@ +/* + * Copyright (c) 2017 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ + +void modulo_signed_Bad(int i) { + char arr[5]; + arr[i % 5] = 123; +} + +void modulo_signed_Good_FP(int i) { + char arr[5]; + if (i >= 0) { + arr[i % 5] = 123; + } +} + +void modulo_signed_Good2_FP(int i) { + char arr[5]; + int j = i % 5; + if (j >= 0) { + arr[j] = 123; + } +} + +void modulo_unsigned_Good_FP(unsigned int i) { + char arr[5]; + arr[i % 5] = 123; +} + +void modulo_signed_var_Bad_FN(unsigned int len, int i) { + char arr[len]; + arr[i % len] = 123; +} + +void modulo_unsigned_var_Good(unsigned int len, unsigned int i) { + char arr[len]; + arr[i % len] = 123; +} + +unsigned int modulo_unsigned(unsigned int a, unsigned int b) { return a % b; } + +void modulo_call_Good(unsigned int len, unsigned int i) { + char arr[len]; + arr[modulo_unsigned(i, len)] = 123; +} + +int modulo_signed(int a, int b) { return a % b; } + +void modulo_call_Bad_FN(unsigned int len, int i) { + char arr[len]; + arr[modulo_signed(i, len)] = 123; +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/cast.c b/infer/tests/codetoanalyze/c/bufferoverrun/cast.c new file mode 100644 index 000000000..3fe0f54dc --- /dev/null +++ b/infer/tests/codetoanalyze/c/bufferoverrun/cast.c @@ -0,0 +1,25 @@ +/* + * Copyright (c) 2017 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ + +#include + +void cast_Good() { + char arr[5]; + *(int32_t*)(arr + 1) = 123; +} + +void cast_Bad_FN() { + char arr[1]; + *(int32_t*)arr = 123; +} + +void cast2_Good_FP() { + int32_t arr[4]; + *(((char*)arr) + 4) = 123; +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 2faf6535e..b6b798214 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -1,7 +1,12 @@ +codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_Bad, 2, BUFFER_OVERRUN, [Offset: [-5, 5] Size: [5, 5]] +codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_Good2_FP, 4, BUFFER_OVERRUN, [Offset: [0, 5] Size: [5, 5]] +codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_Good_FP, 3, BUFFER_OVERRUN, [Offset: [-5, 5] Size: [5, 5]] +codetoanalyze/c/bufferoverrun/arith.c, modulo_unsigned_Good_FP, 2, BUFFER_OVERRUN, [Offset: [-5, 5] Size: [5, 5]] codetoanalyze/c/bufferoverrun/array_dynlength.c, init_variable_array, 3, BUFFER_OVERRUN, [Offset: [3xs$0 + 1, 3xs$1 + 1] Size: [3xs$0 + 1, 3xs$1 + 1]] codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 4, CONDITION_ALWAYS_TRUE, [] codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 13, CONDITION_ALWAYS_TRUE, [] codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 16, BUFFER_OVERRUN, [Offset: [0, 10] Size: [10, 10]] +codetoanalyze/c/bufferoverrun/cast.c, cast2_Good_FP, 2, BUFFER_OVERRUN, [Offset: [4, 4] Size: [4, 4]] codetoanalyze/c/bufferoverrun/do_while.c, do_while, 2, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/do_while.c:18:5 by call `do_while_sub()` ] codetoanalyze/c/bufferoverrun/do_while.c, do_while, 3, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/do_while.c:18:5 by call `do_while_sub()` ] codetoanalyze/c/bufferoverrun/for_loop.c, for_loop, 10, BUFFER_OVERRUN, [Offset: [0, 9] Size: [5, 10]] @@ -43,8 +48,11 @@ codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_true_Ok, 3, CONDI codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_value_Ok, 3, CONDITION_ALWAYS_FALSE, [] codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 1, CONDITION_ALWAYS_TRUE, [] codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 4, BUFFER_OVERRUN, [Offset: [1, 1] Size: [0, 0]] +codetoanalyze/c/bufferoverrun/sizeof.c, sizeof_char_good_FP, 2, BUFFER_OVERRUN, [Offset: [79, 79] Size: [10, 10]] codetoanalyze/c/bufferoverrun/sizeof.c, static_stride_bad, 7, BUFFER_OVERRUN, [Offset: [1, 1] Size: [0, 0]] codetoanalyze/c/bufferoverrun/trivial.c, trivial, 2, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10]] +codetoanalyze/c/bufferoverrun/unreachable.c, FP_exit_at_end_of_proc_good, 2, UNREACHABLE_CODE, [] +codetoanalyze/c/bufferoverrun/unreachable.c, FP_loop_once_intentional_good, 3, CONDITION_ALWAYS_FALSE, [] codetoanalyze/c/bufferoverrun/unreachable.c, FP_loop_with_break_good, 1, CONDITION_ALWAYS_TRUE, [] codetoanalyze/c/bufferoverrun/unreachable.c, FP_loop_with_exit_good, 1, CONDITION_ALWAYS_TRUE, [] codetoanalyze/c/bufferoverrun/unreachable.c, FP_loop_with_return_good, 1, CONDITION_ALWAYS_TRUE, [] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/sizeof.c b/infer/tests/codetoanalyze/c/bufferoverrun/sizeof.c index d62ff479b..4c982c6d7 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/sizeof.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/sizeof.c @@ -32,3 +32,8 @@ void static_stride_bad() { a[1]; // report } } + +void sizeof_char_good_FP(int i) { + char b[10]; + b[sizeof(b) - 1] = 123; +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/unreachable.c b/infer/tests/codetoanalyze/c/bufferoverrun/unreachable.c index b451444e6..71c51fc17 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/unreachable.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/unreachable.c @@ -41,6 +41,11 @@ void exit_at_end_of_if_good() { } } +void FP_exit_at_end_of_proc_good() { + nop(); + exit(5); +} + void FN_useless_else_bad() { if (__infer_nondet_int()) { exit(0); @@ -93,6 +98,12 @@ void FP_loop_with_unreachable_good() { } } +void FP_loop_once_intentional_good() { + do { + nop(); + } while (0); +} + void FN_loop_once_break_bad() { while (__infer_nondet_int()) { break; diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index e8d6aee1a..2769c99f8 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -1,7 +1,14 @@ codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_by_ref_bad, 4, BUFFER_OVERRUN, [Offset: [-1, -1] Size: [10, 10]] +codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_lI, 2, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector*,std::allocator*>>_operator[]()` ] +codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good_FP, 5, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `ral()` ] codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, instantiate_my_vector_oob_Ok, 3, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call `my_vector_oob_Bad()` ] codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN, [Offset: [s$6, s$7] Size: [s$6, s$7] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call `int_vector_access_at()` ] codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10]] +codetoanalyze/cpp/bufferoverrun/vector.cpp, constructor_Good_FP, 2, BUFFER_OVERRUN, [Offset: [0, 0] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector>_operator[]()` ] codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 11, BUFFER_OVERRUN, [Offset: [0, 0] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector>_operator[]()` ] codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 18, BUFFER_OVERRUN, [Offset: [1, 1] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector>_at()` ] codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN, [Offset: [s$14, s$15] Size: [s$14, s$15] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector>_operator[]()` ] +codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN, [Offset: [1, 1] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector>_operator[]()` ] +codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Good_FP, 3, BUFFER_OVERRUN, [Offset: [0, 0] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector>_operator[]()` ] +codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, BUFFER_OVERRUN, [Offset: [0, 0] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector>_operator[]()` ] +codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Good_FP, 4, BUFFER_OVERRUN, [Offset: [0, 0] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector>_operator[]()` ] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/repro1.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/repro1.cpp new file mode 100644 index 000000000..3de848b06 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/repro1.cpp @@ -0,0 +1,144 @@ +/* + * Copyright (c) 2017 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ +#include +#include +#include +#include + +int __infer_nondet_int(); + +#define ASSERT(x) assert(x) +#define xh(h) \ + ({ \ + const uint64_t* u1 = (const uint64_t*)(h); \ + const uint64_t* u2 = (const uint64_t*)((h) + 8); \ + *u1 ^ *u2; \ + }) +#define alo(a) aloi2(a, 0) +#define aloi2(a, i2) ((lo){i1tl(a.i), (i2)}) +#define i1tl(i1) (__infer_nondet_int() ? xh((i1).h) : (i1).i) +#define HL (sizeof(char) * 16) + +enum class TLOR { S, F }; + +uint32_t MH2(const void* k) { return (int64_t)k ^ __infer_nondet_int(); } + +uint32_t th(const void* k) { return MH2(k); } + +typedef int BI; +constexpr BI kBN = 0; + +typedef uint64_t ft; + +struct it { + ft i{0}; + char h[HL]; + it() : i(0) { ::memset(h, '\0', sizeof(h)); } + explicit it(ft f) : i(f) { ::memset(h, '\0', sizeof(h)); } +}; + +struct ai { + it i; + ai() {} + ai(it i_) : i(i_) {} +}; + +struct lo { + uint64_t i1; + uint64_t i2; +}; + +struct lt { + BI bI; +}; + +template +struct LMB { + TLOR lO(const lo& o) { + auto r = TLOR::S; + if (__infer_nondet_int()) { + r = TLOR::F; + } + return r; + } + void u(const lo& o) {} +}; + +template +struct LM { + typedef LMB B; + void l(lt& t, const lo& o) { lI(t, o); } + void tL(lt& t, const lo& o) { lI(t, o); } + void u(lt& t, const lo& o) { + ASSERT(fB(o) == t.bI); + if (t.bI == kBN) { + return; + } + uI(t.bI, o); + t.bI = kBN; + } + + private: + BI fB(const lo& o) { return (BI)th((const void*)&o) % b.size() + 1; } + void lI(lt& t, const lo& o) { + auto bi = fB(o); + auto r = b[bi - 1]->lO(o); + if (r != TLOR::S) { + t.bI = kBN; + return; + } + t.bI = bi; + } + void uI(BI bi, const lo& o) { b[bi - 1]->u(o); } + std::vector> b; +}; + +class TFM {}; + +typedef TFM LMDM; + +static LM* al; + +static inline void ral(lt* t, ai a) { + ASSERT(t); + lo o = alo(a); + al->u(*t, o); +} + +static inline void gal(lt* t, ai a) { + ASSERT(t); + lo o = alo(a); + if (__infer_nondet_int()) { + al->tL(*t, o); + } else { + al->l(*t, o); + } +} + +inline ai aft(ft i) { return ai(it(i)); } + +struct im { + private: + char e[]; + + public: + const char* gKPC() const noexcept { return e; } +}; + +struct arh { + ft i1; +}; + +static void am_Good_FP(im* it) { + const arh* ch = (const arh*)it->gKPC(); + const ai a = aft(ch->i1); + lt at; + gal(&at, a); + ral(&at, a); +} diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp index 364fc6ef1..62645c9e7 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp @@ -14,6 +14,36 @@ void out_of_bound_Bad(std::vector v) { v[n] = 1; } +void constructor_Good_FP() { + std::vector v(1); + v[0] = 2; +} + +void push_back_Good_FP() { + std::vector v; + v.push_back(1); + v[0] = 2; +} + +void push_back_Bad() { + std::vector v; + v.push_back(1); + v[1] = 2; +} + +void reserve_Good_FP() { + std::vector v; + v.reserve(42); + v.push_back(1); + v[0] = 2; +} + +void reserve_Bad() { + std::vector v; + v.reserve(42); + v[0] = 2; +} + struct Int_no_copy { Int_no_copy(Int_no_copy&) = delete; Int_no_copy(const Int_no_copy&) = delete;