From c05062556fa1adb718983e36dd6273b94855210d Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Thu, 8 Aug 2019 07:52:31 -0700 Subject: [PATCH] [inferbo] Add vector model: push_back Summary: It adds a model of vector::push_back Depends on D16687225 Reviewed By: ezgicicek Differential Revision: D16687269 fbshipit-source-id: 9d2a73fca --- .../src/bufferoverrun/bufferOverrunModels.ml | 22 +++++++++++++++++++ .../cpp/bufferoverrun/issues.exp | 5 ++--- .../cpp/bufferoverrun/vector.cpp | 6 ++--- 3 files changed, 27 insertions(+), 6 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 987cc2ce7..22f5bd2b0 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -728,6 +728,25 @@ module StdVector = struct let get_size vec_exp mem = eval_array_locs_length (deref_of vec_exp mem) mem + let set_size {location} vec_exp new_size mem = + let locs = deref_of vec_exp mem in + Dom.Mem.transform_mem locs mem ~f:(fun v -> + Dom.Val.set_array_length location ~length:new_size v ) + + + let push_back vec_exp elt_exp = + let exec model_env ~ret:_ mem = + let mem = + let new_size = Dom.Val.plus_a (get_size vec_exp mem) (Dom.Val.of_int 1) in + set_size model_env vec_exp new_size mem + in + let elt_locs = Dom.Val.get_all_locs (Dom.Mem.find_set (deref_of vec_exp mem) mem) in + let elt_v = Dom.Mem.find_set (Sem.eval_locs elt_exp mem) mem in + Dom.Mem.update_mem elt_locs elt_v mem + in + {exec; check= no_check} + + let size vec_exp = let exec _ ~ret:(id, _) mem = let mem = Dom.Mem.add_stack (Loc.of_id id) (get_size vec_exp mem) mem in @@ -1101,6 +1120,9 @@ module Call = struct $+? any_arg $--> StdVector.constructor_copy ; -"std" &:: "vector" < any_typ &+ any_typ >:: "operator[]" $ capt_exp $+ capt_exp $--> StdVector.at + ; -"std" &:: "vector" < any_typ &+ any_typ >:: "push_back" $ capt_exp $+ capt_exp + $--> StdVector.push_back + ; -"std" &:: "vector" < any_typ &+ any_typ >:: "reserve" $ any_arg $+ any_arg $--> no_model ; -"std" &:: "vector" < any_typ &+ any_typ >:: "size" $ capt_exp $--> StdVector.size ; +PatternMatch.implements_collection &:: "" <>$ capt_var_exn $+ capt_exp $--> Collection.init diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 77752bf57..307ae4d4a 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -111,16 +111,15 @@ codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_call_safe_access2_Good, 2, INFERB codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_call_safe_access4_Good, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,,Parameter `*v->vector_elem`,Array access: Offset: 0 Size: 0 by call to `safe_access4` ] codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_call_safe_access5_Good, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,,Parameter `*v->vector_elem`,Array access: Offset: 0 Size: 0 by call to `safe_access5` ] 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_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset: 0 Size: 0] -codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_reserve_Good, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset: 0 Size: 0] codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_safe_access3_Good, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset: 0 Size: 0] 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_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 6 Size: 5] codetoanalyze/cpp/bufferoverrun/vector.cpp, constructor_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset: 3 Size: 1] codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: std::vector>::data,Assignment,Array access: Offset: [-oo, +oo] (⇐ [-oo, +oo] + [-oo, +oo]) Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Parameter `*v->vector_elem`,Assignment,,Parameter `*v->vector_elem`,Array access: Offset: v->vector_elem.length Size: v->vector_elem.length] codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Bad, 3, BUFFER_OVERRUN_L1, 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 Size: 10 by call to `access_minus_one` ] 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_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset: 1 Size: 0] +codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 1 Size: 1] codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset: 0 Size: 0] 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/vector.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp index ddc304ac4..5cc121694 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp @@ -33,7 +33,7 @@ void constructor_Bad() { v[3] = 2; } -void FP_push_back_Good() { +void push_back_Good() { std::vector v; v.push_back(1); v[0] = 2; @@ -45,7 +45,7 @@ void push_back_Bad() { v[1] = 2; } -void FP_reserve_Good() { +void reserve_Good() { std::vector v; v.reserve(42); v.push_back(1); @@ -156,7 +156,7 @@ void assert_Good_2(int x) { v[4] = 1; } -void FN_assert_Bad() { +void assert_Bad() { std::vector v; for (int i = 0; i < 5; i++) { v.push_back(1);