From f066776b17dd88bd0376e95f84a2a3055fdcc8f3 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Mon, 5 Aug 2019 08:20:26 -0700 Subject: [PATCH] [inferbo] Add model: vector size Summary: It adds vector model of the size function Reviewed By: ezgicicek Differential Revision: D16645589 fbshipit-source-id: 6518fa228 --- infer/src/bufferoverrun/bufferOverrunModels.ml | 10 ++++++++++ .../codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp | 2 +- .../tests/codetoanalyze/cpp/bufferoverrun/issues.exp | 11 +++++------ .../tests/codetoanalyze/cpp/bufferoverrun/repro1.cpp | 8 ++++---- .../tests/codetoanalyze/cpp/bufferoverrun/vector.cpp | 10 ++++++++++ 5 files changed, 30 insertions(+), 11 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 89143cebb..a90e03679 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -688,6 +688,15 @@ module StdVector = struct ~last_included:false ~latest_prune location cond_set in {exec; check} + + + let size vec_exp = + let exec _ ~ret:(id, _) mem = + let deref_of_vec = Dom.Mem.find_set (Sem.eval_locs vec_exp mem) mem in + let size_v = eval_array_locs_length (Dom.Val.get_all_locs deref_of_vec) mem in + Dom.Mem.add_stack (Loc.of_id id) size_v mem + in + {exec; check= no_check} end (* Java's Collections are represented like arrays. But we don't care about the elements. @@ -1007,6 +1016,7 @@ module Call = struct $--> StdVector.constructor ; -"std" &:: "vector" < any_typ &+ any_typ >:: "operator[]" $ capt_exp $+ capt_exp $--> StdVector.at + ; -"std" &:: "vector" < any_typ &+ any_typ >:: "size" $ capt_exp $--> StdVector.size ; +PatternMatch.implements_collection &:: "" <>$ capt_var_exn $+ capt_exp $--> Collection.init (* model sets as lists *) diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp index 2b4a148a6..5809bbcde 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp @@ -7,7 +7,7 @@ #include namespace CppIsTricky { -void vector_size_Bad() { +void FN_vector_size_Bad() { const auto vec = std::vector{1, 2, 3}; const int numExpectedElements = 1; const auto delta = numExpectedElements - vec.size(); diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index bc219be71..3c4a7bd61 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -42,9 +42,10 @@ codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_condition codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_inequality_join2_2_Bad, 1, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `idx`,,Array declaration,Array access: Offset: 6 Size: 5 by call to `conditional_inequality_join2` ] 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_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, 3, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [,Assignment,,Unknown value from: std::vector>::size,Binary operation: (1 - [-oo, +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]] codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 10, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 30 Size: 10] +codetoanalyze/cpp/bufferoverrun/folly_memory_UninitializedMemoryHacks.cpp, folly::resizeWithoutInitialization, 1, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] +codetoanalyze/cpp/bufferoverrun/folly_memory_UninitializedMemoryHacks.cpp, folly::resizeWithoutInitialization, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_by_ref_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Call,Assignment,,Array declaration,Array access: Offset: -1 Size: 10] codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_loop_with_init_S_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Call,Parameter `length`,Assignment,,Array declaration,Array access: Offset: 10 Size: 10] codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Assignment,Array access: Offset: 5 Size: 5] @@ -61,11 +62,8 @@ codetoanalyze/cpp/bufferoverrun/relation.cpp, call2_plus_params_Bad, 0, BUFFER_O codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C::foo_Bad, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C::foo_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 5] codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C::goo, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] -codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM::fB_FP, 0, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [,Unknown value from: std::vector,std::default_delete>>,std::allocator,std::default_delete>>>>::size,Binary operation: ([-oo, +oo] + 1):unsigned64] codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM::lI_FP, 2, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: std::unique_ptr,std::default_delete>>::operator->,Array access: Offset: [-oo, +oo] Size: [0, +oo]] -codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM::lI_FP, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [,Call,Unknown value from: std::vector,std::default_delete>>,std::allocator,std::default_delete>>>>::size,Assignment,Assignment,Binary operation: ([-oo, +oo] - 1):signed32] codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM::uI, 0, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: std::unique_ptr,std::default_delete>>::operator->,Array access: Offset: [-oo, +oo] Size: [0, +oo]] -codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good_FP, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Call,Assignment,Assignment,Call,Parameter `t->bI`,Call,Assignment,Call,,Parameter `bi`,Binary operation: ([-oo, +oo] - 1):signed32 by call to `ral_good` ] codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Parameter `v->_size`,Call,,Parameter `i`,,Parameter `this->_size`,Array declaration,Assignment,Array access: Offset: v->_size Size: v->_size by call to `int_vector::access_at` ] codetoanalyze/cpp/bufferoverrun/std_array.cpp, array_iter1_Bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 5] codetoanalyze/cpp/bufferoverrun/std_array.cpp, array_iter2_Bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 5] @@ -110,8 +108,8 @@ codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_assert_Good_2, 6, BUFFER_OVERRUN_ codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_data_Good, 3, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: std::vector>::data,Assignment,Array access: Offset: [-oo, +oo] (⇐ [-oo, +oo] + 4) Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_push_back_Good, 3, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: std::vector>::operator[],Array access: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_reserve_Good, 4, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: std::vector>::operator[],Array access: Offset: [-oo, +oo] Size: [0, +oo]] -codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_safe_access2, 6, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [,Unknown value from: std::vector>::size,Binary operation: ([0, +oo] + 1):unsigned32] -codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_safe_access2, 7, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: std::vector>::size,,Unknown value from: std::vector>::size,Array declaration,Array access: Offset: [0, +oo] Size: [0, +oo]] +codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_safe_access2, 6, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] +codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_safe_access2, 6, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_safe_access3_Good, 3, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: std::vector>::operator[],Array access: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_safe_access6, 2, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: std::vector>::empty,,Array declaration,Assignment,Array access: Offset: [-oo, +oo] Size: 2] codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 6, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: std::vector>::operator[],Array access: Offset: [-oo, +oo] Size: [0, +oo]] @@ -121,4 +119,5 @@ codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Bad, 3, BUFFER_OVERRUN codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Array declaration,Call,Parameter `*init`,Assignment,Call,Parameter `*__param_0->a`,Assignment,Call,,Parameter `count`,Call,Parameter `idx`,Assignment,Array access: Offset: [-1, 0] Size: 10 by call to `access_minus_one` ] codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: std::vector>::operator[],Array access: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: std::vector>::operator[],Array access: Offset: [-oo, +oo] Size: [0, +oo]] +codetoanalyze/cpp/bufferoverrun/vector.cpp, simple_size_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,,Array declaration,Assignment,Array access: Offset: 3 Size: 3] codetoanalyze/cpp/bufferoverrun/void_ptr.cpp, FP_call_casting_void_ptr_Ok, 2, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Array declaration,Call,,Parameter `*p`,Assignment,Array access: Offset: 14 Size: 2 by call to `casting_void_ptr` ] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/repro1.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/repro1.cpp index 36c23dad2..bdc7b543e 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/repro1.cpp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/repro1.cpp @@ -74,7 +74,7 @@ struct LM { void l(lt& t, const lo& o) { lI_FP(t, o); } void tL(lt& t, const lo& o) { lI_FP(t, o); } void u(lt& t, const lo& o) { - ASSERT(fB_FP(o) == t.bI); + ASSERT(fB(o) == t.bI); if (t.bI == kBN) { return; } @@ -83,9 +83,9 @@ struct LM { } private: - BI fB_FP(const lo& o) { return (BI)th((const void*)&o) % b.size() + 1; } + BI fB(const lo& o) { return (BI)th((const void*)&o) % b.size() + 1; } void lI_FP(lt& t, const lo& o) { - auto bi = fB_FP(o); + auto bi = fB(o); auto r = b[bi - 1]->lO(o); if (r != TLOR::S) { t.bI = kBN; @@ -133,7 +133,7 @@ struct arh { ft i1; }; -static void am_Good_FP(im* it) { +static void am_Good(im* it) { const arh* ch = (const arh*)it->gKPC(); const ai a = aft(ch->i1); lt at; diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp index 97d9b4d68..030355a27 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp @@ -13,6 +13,16 @@ void FN_out_of_bound_Bad(std::vector v) { v[n] = 1; } +void simple_size_Good() { + std::vector v(3); + v[v.size() - 1] = 2; +} + +void simple_size_Bad() { + std::vector v(3); + v[v.size()] = 2; +} + void constructor_Good() { std::vector v(1); v[0] = 2;