From 042dd7d9cb9fe45718197a030b9383bcf4073e8a Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Tue, 31 Oct 2017 06:47:26 -0700 Subject: [PATCH] [inferbo] revise semantics of vector::data Summary: vector::data returns a pointer to the first value of the vector. - The size of the (array) pointer should be the same with the vector. - The pointer should point to the same abstract value with the vector. Reviewed By: mbouaziz Differential Revision: D6196592 fbshipit-source-id: cc17096 --- .../include/infer_model/vector_bufferoverrun.h | 14 ++++++++++++-- infer/src/bufferoverrun/arrayBlk.ml | 4 ++++ infer/src/bufferoverrun/bufferOverrunChecker.ml | 15 +++++++++++++++ infer/src/bufferoverrun/bufferOverrunDomain.ml | 4 ++++ .../codetoanalyze/cpp/bufferoverrun/issues.exp | 1 + .../codetoanalyze/cpp/bufferoverrun/vector.cpp | 13 +++++++++++++ 6 files changed, 49 insertions(+), 2 deletions(-) diff --git a/infer/models/cpp/include/infer_model/vector_bufferoverrun.h b/infer/models/cpp/include/infer_model/vector_bufferoverrun.h index 7e4cdcdb0..6f9a50374 100644 --- a/infer/models/cpp/include/infer_model/vector_bufferoverrun.h +++ b/infer/models/cpp/include/infer_model/vector_bufferoverrun.h @@ -29,6 +29,8 @@ extern "C" { int __inferbo_min(int, int); + +void __inferbo_set_size(void* p, int size); } bool __inferbo_empty(int* size) { return 1 - __inferbo_min(*size, 1); } @@ -233,9 +235,17 @@ class vector { reference back() { return (reference)*get(); } const_reference back() const { return (const_reference)*get(); } - value_type* data() noexcept { return get(); } + value_type* data() noexcept { + value_type* p = get(); + __inferbo_set_size((void*)&p, infer_size); + return p; + } - const value_type* data() const noexcept { return get(); } + const value_type* data() const noexcept { + value_type* p = get(); + __inferbo_set_size((void*)&p, infer_size); + return p; + } void push_back(const_reference __x); void push_back(value_type&& __x); diff --git a/infer/src/bufferoverrun/arrayBlk.ml b/infer/src/bufferoverrun/arrayBlk.ml index 029b55876..b18d58d9a 100644 --- a/infer/src/bufferoverrun/arrayBlk.ml +++ b/infer/src/bufferoverrun/arrayBlk.ml @@ -105,6 +105,8 @@ module ArrInfo = struct let prune_ne : t -> t -> t = fun arr1 arr2 -> {arr1 with offset= Itv.prune_ne arr1.offset arr2.offset} + + let set_size : Itv.t -> t -> t = fun size arr -> {arr with size} end include AbstractDomain.Map (Allocsite) (ArrInfo) @@ -182,3 +184,5 @@ let prune_comp : Binop.t -> astate -> astate -> astate = let prune_eq : astate -> astate -> astate = fun a1 a2 -> do_prune ArrInfo.prune_eq a1 a2 let prune_ne : astate -> astate -> astate = fun a1 a2 -> do_prune ArrInfo.prune_ne a1 a2 + +let set_size : Itv.t -> astate -> astate = fun size a -> map (ArrInfo.set_size size) a diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 37fbc7647..660d53b4f 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -101,6 +101,19 @@ module TransferFunctions (CFG : ProcCfg.S) = struct mem + let model_set_size : (Exp.t * Typ.t) list -> Location.t -> Dom.Mem.astate -> Dom.Mem.astate = + fun params location mem -> + match params with + | [(e1, _); (e2, _)] -> + let locs = Sem.eval_locs e1 mem location |> Dom.Val.get_pow_loc in + let size = Sem.eval e2 mem location |> Dom.Val.get_itv in + let arr = Dom.Mem.find_heap_set locs mem in + let arr = Dom.Val.set_array_size size arr in + Dom.Mem.strong_update_heap locs arr mem + | _ -> + mem + + let model_by_value value ret mem = match ret with | Some (id, _) -> @@ -144,6 +157,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct match Typ.Procname.get_method callee_pname with | "__inferbo_min" -> model_min ret params loc mem + | "__inferbo_set_size" -> + model_set_size params loc mem | "__exit" | "exit" -> Bottom | "fgetc" -> diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 2e09b54eb..ba4ac88b4 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -245,6 +245,10 @@ module Val = struct fun fmt x -> F.fprintf fmt "(%a, %a)" Itv.pp x.itv ArrayBlk.pp x.arrayblk + let set_array_size : Itv.t -> t -> t = + fun size v -> {v with arrayblk= ArrayBlk.set_size size v.arrayblk} + + module Itv = struct let nat = of_itv Itv.nat diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index ebf08edc3..e375315a7 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -13,6 +13,7 @@ codetoanalyze/cpp/bufferoverrun/repro1.cpp, ral_FP, 3, BUFFER_OVERRUN_S2, [Call, codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, instantiate_my_vector_oob_Ok, 3, BUFFER_OVERRUN_L1, [Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [42, 42] Size: [42, 42] @ 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_L2, [Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [u$4, u$5] Size: [u$4, u$5] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call `int_vector_access_at()` ] codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [10, 10]] +codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_L1, [Call,Call,Assignment,Call,Call,ArrayDeclaration,Assignment,Assignment,Return,Assignment,Assignment,Return,Assignment,Assignment,ArrayAccess: Offset: [10, 10] Size: [5, 5]] codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN_L5, [Call,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 18, BUFFER_OVERRUN_L3, [Call,Call,Call,Assignment,Call,Call,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [1, 1] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN_L2, [Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [u$12, u$13] Size: [u$12, u$13]] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp index 8817c5fa1..b77a43d0c 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp @@ -143,3 +143,16 @@ void call_safe_access6_Good() { std::vector v; safe_access6(v); } + +void data_Good() { + std::vector v(5); + int* p = v.data(); + p[4] = 1; +} + +void data_Bad() { + std::vector v(5); + int* p = v.data(); + p[4] = 10; + p[v[4]] = 1; +}