From 196a602c25dcd0e82eb50b2861ae132e15cdaf76 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Wed, 2 Jan 2019 21:19:38 -0800 Subject: [PATCH] [inferbo] Add model of basic_string Reviewed By: mbouaziz, jvillard Differential Revision: D13527054 fbshipit-source-id: 97915e462 --- infer/src/IR/ProcnameDispatcher.ml | 14 ++++++ infer/src/IR/ProcnameDispatcher.mli | 4 ++ .../src/bufferoverrun/bufferOverrunModels.ml | 50 +++++++++++++++++-- .../cpp/bufferoverrun/issues.exp | 2 + .../cpp/bufferoverrun/std_string.cpp | 4 +- 5 files changed, 67 insertions(+), 7 deletions(-) diff --git a/infer/src/IR/ProcnameDispatcher.ml b/infer/src/IR/ProcnameDispatcher.ml index 15c8906a9..123f3b6a3 100644 --- a/infer/src/IR/ProcnameDispatcher.ml +++ b/infer/src/IR/ProcnameDispatcher.ml @@ -107,6 +107,8 @@ type ('context, 'f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out, 'empt ; path_extra: ('context, 'f_in, 'f_out, 'captured_types, 'emptyness) path_extra ; get_markers: 'markers_in -> 'markers_out } +type typ_matcher = typ -> bool + (* Combinators *) let empty : ('context, 'f, 'f, unit, 'markers, 'markers, empty) path_matcher = @@ -772,6 +774,13 @@ module Call = struct {match_arg; marker_static_checker= no_marker_checker} + (** Matches the type matched by the given typ_matcher *) + let match_prim_typ : typ_matcher -> _ one_arg_matcher = + fun on_typ -> + let match_arg _context _capt arg = on_typ (FuncArg.typ arg) in + {match_arg; marker_static_checker= no_marker_checker} + + (* Function argument capture *) (** Do not capture this argument *) @@ -855,6 +864,11 @@ module Call = struct let capt_exp_of_typ m = {one_arg_matcher= match_typ (m <...>! ()); capture= capture_arg_exp} + let capt_exp_of_prim_typ typ = + let on_typ typ' = Typ.equal typ typ' in + {one_arg_matcher= match_prim_typ on_typ; capture= capture_arg_exp} + + let typ1 : 'marker -> ('context, unit, _, 'f, 'f, _, _) one_arg = fun m -> {one_arg_matcher= match_typ1 m; capture= no_capture} diff --git a/infer/src/IR/ProcnameDispatcher.mli b/infer/src/IR/ProcnameDispatcher.mli index 7b7dfe26b..1251ec8c3 100644 --- a/infer/src/IR/ProcnameDispatcher.mli +++ b/infer/src/IR/ProcnameDispatcher.mli @@ -245,6 +245,10 @@ module Call : sig -> ('context, Exp.t, 'wrapped_arg, 'wrapped_arg -> 'f, 'f, _, _) one_arg (** Captures one arg expression of the given type *) + val capt_exp_of_prim_typ : + Typ.t -> ('context, Exp.t, 'wrapped_arg, 'wrapped_arg -> 'f, 'f, _, _) one_arg + (** Captures one arg expression of the given primitive type *) + val capt_var_exn : ('context, Ident.t, 'wrapped_arg, 'wrapped_arg -> 'f, 'f, _, _) one_arg (** Captures one arg Var. Fails with an internal error if the expression is not a Var *) diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 3047fcf2d..ee670f196 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -37,6 +37,14 @@ let no_exec _model_env ~ret:_ mem = mem let no_check _model_env _mem cond_set = cond_set +let no_model = + let exec {pname} ~ret:_ mem = + L.d_printfln_escaped "No model for %a" Typ.Procname.pp pname ; + mem + in + {exec; check= no_check} + + (* It returns a tuple of: - type of array element - stride of the type @@ -312,12 +320,36 @@ module StdArray = struct location cond_set in {exec; check} +end + +module StdBasicString = struct + (* The (4) constructor in https://en.cppreference.com/w/cpp/string/basic_string/basic_string *) + let constructor_from_char_ptr tgt src len = + let {exec= malloc_exec; check= malloc_check} = malloc len in + let exec model_env ~ret:((ret_id, _) as ret) mem = + let mem = malloc_exec model_env ~ret mem in + let v = Dom.Mem.find (Loc.of_id ret_id) mem in + let mem = Dom.Mem.update_mem (Sem.eval_locs tgt mem) v mem in + let contents = + let src_locs = Sem.eval_locs src mem in + Dom.Mem.find_set src_locs mem + in + Dom.Mem.update_mem (Dom.Val.get_all_locs v) contents mem + in + let check ({location; integer_type_widths} as model_env) mem cond_set = + let cond_set = malloc_check model_env mem cond_set in + BoUtils.Check.lindex integer_type_widths ~array_exp:src ~index_exp:len ~last_included:true + mem location cond_set + in + {exec; check} - let no_model = - let exec {pname} ~ret:_ mem = - L.d_printfln_escaped "No model for %a" Typ.Procname.pp pname ; - mem + (* The (7) constructor in https://en.cppreference.com/w/cpp/string/basic_string/basic_string *) + let copy_constructor tgt src = + let exec _ ~ret:_ mem = + let tgt_locs = Sem.eval_locs tgt mem in + let v = Dom.Mem.find_set (Sem.eval_locs src mem) mem in + Dom.Mem.update_mem tgt_locs v mem in {exec; check= no_check} end @@ -492,7 +524,15 @@ module Call = struct ; std_array0 >:: "array" &--> StdArray.constructor ; std_array2 >:: "at" $ capt_arg $+ capt_arg $!--> StdArray.at ; std_array2 >:: "operator[]" $ capt_arg $+ capt_arg $!--> StdArray.at - ; -"std" &:: "array" &::.*--> StdArray.no_model + ; -"std" &:: "array" &::.*--> no_model + ; -"std" &:: "basic_string" &:: "basic_string" $ capt_exp + $+ capt_exp_of_typ (-"std" &:: "basic_string") + $--> StdBasicString.copy_constructor + ; -"std" &:: "basic_string" &:: "basic_string" $ capt_exp + $+ capt_exp_of_prim_typ (Typ.mk (Typ.Tptr (Typ.mk (Typ.Tint Typ.IChar), Pk_pointer))) + $+ capt_exp_of_prim_typ (Typ.mk (Typ.Tint Typ.size_t)) + $--> StdBasicString.constructor_from_char_ptr + ; -"std" &:: "basic_string" &::.*--> no_model ; +PatternMatch.implements_collection &:: "get" <>$ capt_var_exn $+ capt_exp $--> Collection.get_or_set_at_index ; +PatternMatch.implements_collection diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index fa3453e0b..f16aec742 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -79,6 +79,8 @@ codetoanalyze/cpp/bufferoverrun/std_string.cpp, last_char1_Bad, 3, BUFFER_OVERRU codetoanalyze/cpp/bufferoverrun/std_string.cpp, last_char1_Bad, 3, INTEGER_OVERFLOW_R2, no_bucket, ERROR, [,Risky value from: snprintf,Assignment,Binary operation: ([-oo, +oo] - 1):signed32] codetoanalyze/cpp/bufferoverrun/std_string.cpp, last_char2_Bad, 6, BUFFER_OVERRUN_R2, no_bucket, ERROR, [,Risky value from: vsnprintf,Assignment,,Array declaration,Array access: Offset: [-oo, +oo] Size: 1024] codetoanalyze/cpp/bufferoverrun/std_string.cpp, last_char2_Bad, 6, INTEGER_OVERFLOW_R2, no_bucket, ERROR, [,Risky value from: vsnprintf,Assignment,Binary operation: ([-oo, +oo] - 1):signed32] +codetoanalyze/cpp/bufferoverrun/std_string.cpp, to_string1_Bad, 3, BUFFER_OVERRUN_R2, no_bucket, ERROR, [,Risky value from: snprintf,Assignment,,Array declaration,Array access: Offset added: [-oo, +oo] Size: 1024] +codetoanalyze/cpp/bufferoverrun/std_string.cpp, to_string2_Bad, 6, BUFFER_OVERRUN_R2, no_bucket, ERROR, [,Risky value from: vsnprintf,Assignment,,Array declaration,Array access: Offset added: [-oo, +oo] Size: 1024] codetoanalyze/cpp/bufferoverrun/symb_arr.cpp, symb_arr_alloc_symb_arr_access_bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Parameter `this->h[*]`,Array access: Offset: 10 Size: 10] codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 10] codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,,Parameter `this->infer_size`,Binary operation: ([0, +oo] + 1):unsigned64] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/std_string.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/std_string.cpp index 5301cdc7d..82f712f7e 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/std_string.cpp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/std_string.cpp @@ -31,7 +31,7 @@ char last_char2_Bad(const char* fmt, ...) { return buf[n - 1]; } -std::string to_string1_Bad_FN(char* s, int i) { +std::string to_string1_Bad(char* s, int i) { char buf[1024]; int n = snprintf(buf, sizeof(buf), "%s%d", s, i); return std::string(buf, n); @@ -48,7 +48,7 @@ std::string to_string1_Good(char* s, int i) { return std::string(buf, n); } -std::string to_string2_Bad_FN(const char* fmt, ...) { +std::string to_string2_Bad(const char* fmt, ...) { char buf[1024]; va_list args; va_start(args, fmt);