From 7b7e6990e4a8b742449356327b2007f0ba6a0cac Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Tue, 29 Jan 2019 18:44:13 -0800 Subject: [PATCH] [inferbo] Add models for basic array iterator Reviewed By: mbouaziz Differential Revision: D13858898 fbshipit-source-id: 4518dad05 --- infer/src/bufferoverrun/arrayBlk.ml | 13 +++ .../src/bufferoverrun/bufferOverrunDomain.ml | 7 ++ .../src/bufferoverrun/bufferOverrunModels.ml | 39 +++++++++ .../cpp/bufferoverrun/issues.exp | 9 ++ .../cpp/bufferoverrun/std_array.cpp | 87 +++++++++++++++++++ 5 files changed, 155 insertions(+) diff --git a/infer/src/bufferoverrun/arrayBlk.ml b/infer/src/bufferoverrun/arrayBlk.ml index 7c7c4e0ea..849e0f384 100644 --- a/infer/src/bufferoverrun/arrayBlk.ml +++ b/infer/src/bufferoverrun/arrayBlk.ml @@ -219,6 +219,17 @@ module ArrInfo = struct Top + let set_offset : Itv.t -> t -> t = + fun offset arr -> + match arr with + | C {size; stride} -> + C {offset; size; stride} + | Java _ -> + L.(die InternalError) "Unexpected offset setting on Java array" + | Top -> + Top + + let offsetof = function C {offset} -> offset | Java _ -> Itv.zero | Top -> Itv.top let sizeof = function C {size} -> size | Java {length} -> length | Top -> Itv.top @@ -337,6 +348,8 @@ let set_length : Itv.t -> t -> t = fun length a -> map (ArrInfo.set_length lengt let set_stride : Z.t -> t -> t = fun stride a -> map (ArrInfo.set_stride stride) a +let set_offset : Itv.t -> t -> t = fun offset a -> map (ArrInfo.set_offset offset) a + let lift_cmp_itv cmp_itv cmp_loc arr1 arr2 = match (is_singleton_or_more arr1, is_singleton_or_more arr2) with | IContainer.Singleton (as1, ai1), IContainer.Singleton (as2, ai2) -> diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 2bc9ee8ad..344432e3c 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -390,6 +390,13 @@ module Val = struct ; traces= Trace.(Set.add_elem location (through ~risky_fun:None)) v.traces } + let set_array_offset : Location.t -> Itv.t -> t -> t = + fun location offset v -> + { v with + arrayblk= ArrayBlk.set_offset offset v.arrayblk + ; traces= Trace.(Set.add_elem location (through ~risky_fun:None)) v.traces } + + let set_array_stride : Z.t -> t -> t = fun new_stride v -> PhysEqual.optim1 v ~res:{v with arrayblk= ArrayBlk.set_stride new_stride v.arrayblk} diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 5e941fb82..6fe643a9d 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -420,6 +420,38 @@ module StdArray = struct location cond_set in {exec; check} + + + let begin_ _size (array_exp, _) = + let exec {location; integer_type_widths} ~ret:(id, _) mem = + let v = + Sem.eval integer_type_widths array_exp mem |> Dom.Val.set_array_offset location Itv.zero + in + Dom.Mem.add_stack (Loc.of_id id) v mem + in + {exec; check= no_check} + + + let end_ size (array_exp, _) = + let exec {location; integer_type_widths} ~ret:(id, _) mem = + let v = + let offset = Itv.of_int_lit (IntLit.of_int64 size) in + Sem.eval integer_type_widths array_exp mem |> Dom.Val.set_array_offset location offset + in + Dom.Mem.add_stack (Loc.of_id id) v mem + in + {exec; check= no_check} + + + let back size (array_exp, _) = + let exec {location; integer_type_widths} ~ret:(id, _) mem = + let v = + let offset = Itv.of_int_lit (IntLit.of_int64 Int64.(size - one)) in + Sem.eval integer_type_widths array_exp mem |> Dom.Val.set_array_offset location offset + in + Dom.Mem.add_stack (Loc.of_id id) v mem + in + {exec; check= no_check} end module StdBasicString = struct @@ -629,6 +661,7 @@ module Call = struct let open ProcnameDispatcher.Call in let mk_std_array () = -"std" &:: "array" < any_typ &+ capt_int in let std_array0 = mk_std_array () in + let std_array1 = mk_std_array () in let std_array2 = mk_std_array () in let char_ptr = Typ.mk (Typ.Tptr (Typ.mk (Typ.Tint Typ.IChar), Pk_pointer)) in make_dispatcher @@ -667,6 +700,12 @@ module Call = struct $+ capt_arg_of_typ (-"std" &:: "vector") $+? capt_exp $--> Folly.Split.std_vector ; std_array0 >:: "array" &--> StdArray.constructor + ; std_array1 >:: "begin" $ capt_arg $!--> StdArray.begin_ + ; std_array1 >:: "cbegin" $ capt_arg $!--> StdArray.begin_ + ; std_array1 >:: "end" $ capt_arg $!--> StdArray.end_ + ; std_array1 >:: "cend" $ capt_arg $!--> StdArray.end_ + ; std_array1 >:: "front" $ capt_arg $!--> StdArray.begin_ + ; std_array1 >:: "back" $ capt_arg $!--> StdArray.back ; std_array2 >:: "at" $ capt_arg $+ capt_arg $!--> StdArray.at ; std_array2 >:: "operator[]" $ capt_arg $+ capt_arg $!--> StdArray.at ; -"std" &:: "array" &::.*--> no_model diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 595136ca6..432b81e50 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -77,6 +77,15 @@ codetoanalyze/cpp/bufferoverrun/repro1.cpp, gal_FP, 4, INTEGER_OVERFLOW_L5, no_b codetoanalyze/cpp/bufferoverrun/repro1.cpp, ral_FP, 3, BUFFER_OVERRUN_S2, no_bucket, ERROR, [Parameter `t->bI`,Call,Parameter `this->b.infer_size`,Call,Parameter `this->b.infer_size`,Call,Parameter `this->infer_size`,Call,,Parameter `index`,,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: [-1+max(1, t->bI.lb), -1+max(1, t->bI.ub)] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/repro1.cpp, ral_FP, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this->b.infer_size`,Call,Parameter `this->b.infer_size`,Call,Parameter `this->infer_size`,Call,,Parameter `this->infer_size`,Binary operation: (4 × [0, +oo]):unsigned64] 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, 3, BUFFER_OVERRUN_L4, no_bucket, ERROR, [,Array declaration,Through,Array access: Offset: [0, +oo] 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] +codetoanalyze/cpp/bufferoverrun/std_array.cpp, array_iter2_Good_FP, 3, BUFFER_OVERRUN_L4, no_bucket, ERROR, [,Array declaration,Through,Array access: Offset: [0, +oo] Size: 11] +codetoanalyze/cpp/bufferoverrun/std_array.cpp, array_iter3_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 5] +codetoanalyze/cpp/bufferoverrun/std_array.cpp, array_iter_back_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 5] +codetoanalyze/cpp/bufferoverrun/std_array.cpp, array_iter_front_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 5] +codetoanalyze/cpp/bufferoverrun/std_array.cpp, array_rev_iter_Bad, 5, BUFFER_OVERRUN_L5, no_bucket, ERROR, [,Array declaration,Array access: Offset: [-oo, +oo] Size: 5] +codetoanalyze/cpp/bufferoverrun/std_array.cpp, array_rev_iter_Good_FP, 5, BUFFER_OVERRUN_L5, no_bucket, ERROR, [,Array declaration,Array access: Offset: [-oo, +oo] Size: 11] codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int1_Bad, 3, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Assignment,Allocation: Length: 4611686018427387903] codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int2_Bad, 3, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Assignment,Allocation: Length: 9223372036854775807] codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int2_Bad, 3, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [,Assignment,Binary operation: (4 × 9223372036854775807):unsigned64] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/std_array.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/std_array.cpp index 14b045643..fec534896 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/std_array.cpp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/std_array.cpp @@ -51,3 +51,90 @@ void std_array_contents_Bad() { a[0] = 10; a[a[0]] = 0; } + +void array_iter1_Good() { + std::array a; + for (auto it = a.begin(); it < a.end(); ++it) { + *it = 10; + } + a[a[0]] = 0; +} + +void array_iter1_Bad() { + std::array a; + for (auto it = a.begin(); it < a.end(); ++it) { + *it = 10; + } + a[a[0]] = 0; +} + +// TODO: Inferbo should give a preciser widening threshold. +void array_iter2_Good_FP() { + std::array a; + for (auto it = a.begin(); it != a.end(); ++it) { + *it = 10; + } + a[a[0]] = 0; +} + +void array_iter2_Bad() { + std::array a; + for (auto it = a.begin(); it != a.end(); ++it) { + *it = 10; + } + a[a[0]] = 0; +} + +void array_iter3_Good() { + std::array a = {10}; + for (auto it = a.cbegin(); it < a.cend(); ++it) { + a[*it] = 10; + } +} + +void array_iter3_Bad() { + std::array a = {10}; + for (auto it = a.cbegin(); it < a.cend(); ++it) { + a[*it] = 10; + } +} + +void array_iter_front_Good() { + std::array a; + a.front() = 10; + a[a[0]] = 0; +} + +void array_iter_front_Bad() { + std::array a; + a.front() = 10; + a[a[0]] = 0; +} + +void array_iter_back_Good() { + std::array a; + a.back() = 10; + a[a[0]] = 0; +} + +void array_iter_back_Bad() { + std::array a; + a.back() = 10; + a[a[0]] = 0; +} + +void array_rev_iter_Good_FP() { + std::array a; + for (auto it = a.rbegin(); it < a.rend(); ++it) { + *it = 10; + } + a[a[0]] = 0; +} + +void array_rev_iter_Bad() { + std::array a; + for (auto it = a.rbegin(); it < a.rend(); ++it) { + *it = 10; + } + a[a[0]] = 0; +}