From f409450d8b8afd5887a1863731ffc4fa099c3e41 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Tue, 11 Dec 2018 05:09:26 -0800 Subject: [PATCH] [inferbo] Add tests for conditional proof obligations Reviewed By: mbouaziz Differential Revision: D13414441 fbshipit-source-id: bc46414bc --- .../conditional_proof_obligation.cpp | 123 ++++++++++++++++++ .../cpp/bufferoverrun/issues.exp | 10 ++ 2 files changed, 133 insertions(+) create mode 100644 infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp new file mode 100644 index 000000000..05edd582f --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp @@ -0,0 +1,123 @@ +/* + * Copyright (c) 2018-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ +#include + +void conditional_buffer_access(int* ptr, unsigned int size) { + int i; + if (size < 1) { + } else if (size < 2) { + i = *(ptr++); + } else if (size < 3) { + i = *(ptr++); + i = *(ptr++); + } else if (size < 4) { + i = *(ptr++); + i = *(ptr++); + i = *(ptr++); + } else if (size < 5) { + i = *(ptr++); + i = *(ptr++); + i = *(ptr++); + i = *(ptr++); + } +} + +void call_conditional_buffer_access_Good_FP() { + int a[1]; + conditional_buffer_access(a, 1); +} + +void call_conditional_buffer_access_Bad() { + int a[1]; + conditional_buffer_access(a, 3); +} + +void conditional_buffer_access2(unsigned int n) { + int a[n]; + conditional_buffer_access(a, n); +} + +void call_conditional_buffer_access2_1_Good_FP() { + conditional_buffer_access2(1); +} + +void call_conditional_buffer_access2_2_Good_FP() { + conditional_buffer_access2(3); +} + +void conditional_minus(int* ptr, unsigned int size) { + int i = 0; + if (ptr != NULL && (i < size - 1)) { + } +} + +void call_conditional_minus_1_Good_FP() { conditional_minus(NULL, 0); } + +void call_conditional_minus_2_Good() { + int a[3]; + conditional_minus(a, 3); +} + +void call_conditional_minus_2_Bad() { + int a[3]; + conditional_minus(a, 0); +} + +unsigned int conditional_minus2(int* ptr, unsigned int size) { + if (ptr != NULL) { + return (size - 1); + } +} + +void call_conditional_minus2_1_Good_FP() { conditional_minus2(NULL, 0); } + +void call_conditional_minus2_2_Good() { + int a[3]; + conditional_minus2(a, 3); +} + +void call_conditional_minus2_2_Bad() { + int a[3]; + conditional_minus2(a, 0); +} + +enum E { + E_SIZEONE = 0, + E_SIZETWO = 1, +}; + +void conditional_buffer_access3(int* ptr, int size) { + int i; + switch (ptr[0]) { + case E_SIZETWO: + i = ptr[size - 2]; + i = ptr[size - 1]; + break; + + case E_SIZEONE: + i = ptr[size - 1]; + break; + } +} + +void call_conditional_buffer_access3_1_Good() { + int a[2]; + a[0] = E_SIZETWO; + conditional_buffer_access3(a, 2); +} + +void call_conditional_buffer_access3_2_Good_FP() { + int a[1]; + a[0] = E_SIZEONE; + conditional_buffer_access3(a, 1); +} + +void call_conditional_buffer_access3_Bad() { + int a[1]; + a[0] = E_SIZETWO; + conditional_buffer_access3(a, 1); +} diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 0da5151af..1932c6aef 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -28,6 +28,16 @@ codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_overload1_Bad, 3, BUFFE codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_overload2_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 5] codetoanalyze/cpp/bufferoverrun/class.cpp, return_class_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Call,Array access: Offset: 5 Size: 5] codetoanalyze/cpp/bufferoverrun/class.cpp, use_global_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: 32 Size: 30] +codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access2_1_Good_FP, 1, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Parameter `n`,Array declaration,Call,,Parameter `*ptr`,Assignment,Assignment,Assignment,Array access: Offset: 3 Size: 1 by call to `conditional_buffer_access2` ] +codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access2_2_Good_FP, 1, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Parameter `n`,Array declaration,Call,,Parameter `*ptr`,Assignment,Assignment,Assignment,Array access: Offset: 3 Size: 3 by call to `conditional_buffer_access2` ] +codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access3_2_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,,Parameter `size`,,Parameter `*ptr`,Array access: Offset: -1 Size: 1 by call to `conditional_buffer_access3` ] +codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access3_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,,Parameter `size`,,Parameter `*ptr`,Array access: Offset: -1 Size: 1 by call to `conditional_buffer_access3` ] +codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,,Parameter `*ptr`,Assignment,Assignment,Assignment,Array access: Offset: 3 Size: 1 by call to `conditional_buffer_access` ] +codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access_Good_FP, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,,Parameter `*ptr`,Assignment,Assignment,Assignment,Array access: Offset: 3 Size: 1 by call to `conditional_buffer_access` ] +codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_minus2_1_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,,Parameter `size`,Binary operation: (0 - 1):unsigned32 by call to `conditional_minus2` ] +codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_minus2_2_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,,Parameter `size`,Binary operation: (0 - 1):unsigned32 by call to `conditional_minus2` ] +codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_minus_1_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,,Parameter `size`,Binary operation: (0 - 1):unsigned32 by call to `conditional_minus` ] +codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_minus_2_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,,Parameter `size`,Binary operation: (0 - 1):unsigned32 by call to `conditional_minus` ] codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp, CppIsTricky::vector_size_Bad, 1, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: __infer_skip_function,Call,,Parameter `*__il`,Array access: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp, CppIsTricky::vector_size_Bad, 3, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [,Assignment,,Call,Call,Unknown value from: std::distance,Call,Parameter `__n`,Assignment,Call,Parameter `__x->infer_size`,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `__n`,Assignment,Call,Parameter `this->infer_size`,Assignment,Binary operation: (1 - [0, +oo]):unsigned64] codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 5, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: lib,Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]]