From 4311371d812d5e26fda284f3d425daf87b046fab Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Tue, 18 Feb 2020 02:33:02 -0800 Subject: [PATCH] [inferbo] Revise split model semantics Reviewed By: ezgicicek Differential Revision: D19942999 fbshipit-source-id: c1d945160 --- .../src/bufferoverrun/bufferOverrunModels.ml | 24 ++++++++++--------- .../cpp/bufferoverrun/folly_split.cpp | 4 ++-- .../cpp/bufferoverrun/issues.exp | 4 +--- 3 files changed, 16 insertions(+), 16 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 1984fded3..97eea8c95 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -674,20 +674,22 @@ module StdVector = struct end module Split = struct - let std_vector ~adds_at_least_one {exp= vector_exp; typ= vector_typ} location mem = - let increment = if adds_at_least_one then Dom.Val.Itv.pos else Dom.Val.Itv.nat in - let vector_type_name = Option.value_exn (vector_typ |> Typ.strip_ptr |> Typ.name) in - let size_field = Fieldname.make vector_type_name "infer_size" in - let vector_size_locs = Sem.eval_locs vector_exp mem |> PowLoc.append_field ~fn:size_field in - let f_trace _ traces = Trace.(Set.add_elem location (through ~risky_fun:None)) traces in - Dom.Mem.transform_mem ~f:(Dom.Val.plus_a ~f_trace increment) vector_size_locs mem + let std_vector model_env ~adds_at_least_one ({typ= vector_typ} as vec_arg) mem = + match vector_typ with + | Typ.{desc= Tptr ({desc= Tstruct (CppClass (_, Template {args= TType elt_typ :: _}))}, _)} -> + let arr_locs = StdVector.deref_of model_env elt_typ vec_arg mem in + let size = if adds_at_least_one then Dom.Val.Itv.pos else Dom.Val.Itv.nat in + StdVector.set_size model_env arr_locs size mem + | _ -> + Logging.d_printfln_escaped "Could not find element type of vector" ; + mem end module Boost = struct module Split = struct let std_vector vector_arg = - let exec {location} ~ret:_ mem = - Split.std_vector ~adds_at_least_one:true vector_arg location mem + let exec model_env ~ret:_ mem = + Split.std_vector model_env ~adds_at_least_one:true vector_arg mem in {exec; check= no_check} end @@ -696,7 +698,7 @@ end module Folly = struct module Split = struct let std_vector vector_arg ignore_empty_opt = - let exec {location; integer_type_widths} ~ret:_ mem = + let exec ({integer_type_widths} as model_env) ~ret:_ mem = let adds_at_least_one = match ignore_empty_opt with | Some ignore_empty_exp -> @@ -705,7 +707,7 @@ module Folly = struct (* default: ignore_empty is false *) true in - Split.std_vector ~adds_at_least_one vector_arg location mem + Split.std_vector model_env ~adds_at_least_one vector_arg mem in {exec; check= no_check} end diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/folly_split.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/folly_split.cpp index a25292ecb..b6c1908d9 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/folly_split.cpp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/folly_split.cpp @@ -42,13 +42,13 @@ void splitTo(const Delim& delimiter, } // namespace folly namespace folly_split { -std::string FP_do_not_ignore_empty_Good(const std::string& s) { +std::string do_not_ignore_empty_Good(const std::string& s) { std::vector v; folly::split("delimiter", s, v); return v[0]; } -std::string FP_do_not_ignore_empty2_Good(const std::string& s) { +std::string do_not_ignore_empty2_Good(const std::string& s) { std::vector v; folly::split("delimiter", s, v, false); return v[0]; diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 4f375676f..2d19240cc 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -46,9 +46,7 @@ codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_throw_exc codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, throw_exception, 3, UNREACHABLE_CODE, no_bucket, ERROR, [Here] 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_split.cpp, folly_split::FP_do_not_ignore_empty2_Good, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset: 0 Size: 0] -codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::FP_do_not_ignore_empty_Good, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset: 0 Size: 0] -codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset: 0 Size: 0] +codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, BUFFER_OVERRUN_L4, no_bucket, ERROR, [,Array declaration,Array access: Offset: 0 Size: [0, +oo]] 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/global.cpp, access_constant_global_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: 5 Size: 5]