From f8ee0a14aa8006c1ea6a93a86f5d765148e8bcc5 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Mon, 3 Feb 2020 04:46:19 -0800 Subject: [PATCH] [inferbo] Give semantics of std::make_shared as simple constructor Summary: This diff gives semantics of `std::make_shared` as simple constructor, i.e., it changes function call of `std::make_chared(i)` to the constructor `C(i)`. Reviewed By: ngorogiannis Differential Revision: D19432338 fbshipit-source-id: 0d838e555 --- infer/src/IR/Procname.ml | 8 +++ infer/src/IR/Procname.mli | 2 + infer/src/IR/Typ.ml | 2 + infer/src/IR/Typ.mli | 3 + .../bufferoverrun/bufferOverrunAnalysis.ml | 44 +++++++------ .../src/bufferoverrun/bufferOverrunChecker.ml | 27 +++++--- .../bufferoverrun/bufferOverrunSemantics.ml | 19 +++++- .../bufferoverrun/bufferOverrunSemantics.mli | 3 +- infer/src/bufferoverrun/bufferOverrunUtils.ml | 63 +++++++++++++++++++ .../src/bufferoverrun/bufferOverrunUtils.mli | 17 +++++ infer/src/istd/IList.ml | 12 ++++ infer/src/istd/IList.mli | 2 + .../cpp/bufferoverrun/issues.exp | 2 + .../cpp/bufferoverrun/smart_ptr.cpp | 46 ++++++++++++++ 14 files changed, 216 insertions(+), 34 deletions(-) create mode 100644 infer/tests/codetoanalyze/cpp/bufferoverrun/smart_ptr.cpp diff --git a/infer/src/IR/Procname.ml b/infer/src/IR/Procname.ml index 2e8fe024c..28edea86a 100644 --- a/infer/src/IR/Procname.ml +++ b/infer/src/IR/Procname.ml @@ -371,6 +371,14 @@ module C = struct let get_parameters c = c.parameters let replace_parameters new_parameters c = {c with parameters= new_parameters} + + (** NOTE: [std::make_shared] is parsed as [C] proc name in Sil, rather than [ObjC_Cpp]. *) + let is_make_shared {name} = + match QualifiedCppName.to_rev_list name with + | [make_shared; "std"] when String.is_prefix make_shared ~prefix:"make_shared" -> + true + | _ -> + false end module Block = struct diff --git a/infer/src/IR/Procname.mli b/infer/src/IR/Procname.mli index 2abcaa611..9998abdb7 100644 --- a/infer/src/IR/Procname.mli +++ b/infer/src/IR/Procname.mli @@ -173,6 +173,8 @@ module C : sig val c : QualifiedCppName.t -> string -> Parameter.clang_parameter list -> Typ.template_spec_info -> t (** Create a C procedure name from plain and mangled name. *) + + val is_make_shared : t -> bool end module Block : sig diff --git a/infer/src/IR/Typ.ml b/infer/src/IR/Typ.ml index 4eb149b87..120aa99f7 100644 --- a/infer/src/IR/Typ.ml +++ b/infer/src/IR/Typ.ml @@ -582,6 +582,8 @@ let unsome s = function (** turn a *T into a T. fails if [typ] is not a pointer type *) let strip_ptr typ = match typ.desc with Tptr (t, _) -> t | _ -> assert false +let is_ptr_to t ~ptr = match ptr.desc with Tptr (t', _) -> equal t t' | _ -> false + (** If an array type, return the type of the element. If not, return the default type if given, otherwise raise an exception *) let array_elem default_opt typ = diff --git a/infer/src/IR/Typ.mli b/infer/src/IR/Typ.mli index 66d39e2a1..71dd65d63 100644 --- a/infer/src/IR/Typ.mli +++ b/infer/src/IR/Typ.mli @@ -322,6 +322,9 @@ val name : t -> Name.t option val strip_ptr : t -> t (** turn a *T into a T. fails if [t] is not a pointer type *) +val is_ptr_to : t -> ptr:t -> bool +(** check if [ptr] is a pointer type to [t] *) + val array_elem : t option -> t -> t (** If an array type, return the type of the element. If not, return the default type if given, otherwise raise an exception *) diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml index 8dda6c879..c866ce204 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml +++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml @@ -158,7 +158,8 @@ module TransferFunctions = struct let instantiate_mem : - Typ.IntegerWidths.t + is_params_ref:bool + -> Typ.IntegerWidths.t -> Ident.t * Typ.t -> (Pvar.t * Typ.t) list -> Procname.t @@ -167,10 +168,10 @@ module TransferFunctions = struct -> BufferOverrunAnalysisSummary.t -> Location.t -> Dom.Mem.t = - fun integer_type_widths ret callee_formals callee_pname params caller_mem callee_exit_mem - location -> + fun ~is_params_ref integer_type_widths ret callee_formals callee_pname params caller_mem + callee_exit_mem location -> let eval_sym_trace = - Sem.mk_eval_sym_trace integer_type_widths callee_formals params caller_mem + Sem.mk_eval_sym_trace ~is_params_ref integer_type_widths callee_formals params caller_mem ~mode:Sem.EvalNormal in let mem = @@ -393,22 +394,25 @@ module TransferFunctions = struct in exec model_env ~ret mem | None -> ( - match (get_summary callee_pname, get_formals callee_pname) with - | Some callee_exit_mem, Some callee_formals -> - instantiate_mem integer_type_widths ret callee_formals callee_pname params mem - callee_exit_mem location - | _, _ -> - (* This may happen for procedures with a biabduction model too. *) - L.d_printfln_escaped "/!\\ Unknown call to %a" Procname.pp callee_pname ; - if is_external callee_pname then ( - L.(debug BufferOverrun Verbose) - "/!\\ External call to unknown %a \n\n" Procname.pp callee_pname ; - assign_symbolic_pname_value callee_pname params ret location mem ) - else if is_non_static callee_pname then ( - L.(debug BufferOverrun Verbose) - "/!\\ Non-static call to unknown %a \n\n" Procname.pp callee_pname ; - assign_symbolic_pname_value callee_pname params ret location mem ) - else Dom.Mem.add_unknown_from ret ~callee_pname ~location mem ) ) + let {BoUtils.ReplaceCallee.pname= callee_pname; params; is_params_ref} = + BoUtils.ReplaceCallee.replace_make_shared tenv get_formals callee_pname params + in + match (get_summary callee_pname, get_formals callee_pname) with + | Some callee_exit_mem, Some callee_formals -> + instantiate_mem ~is_params_ref integer_type_widths ret callee_formals callee_pname + params mem callee_exit_mem location + | _, _ -> + (* This may happen for procedures with a biabduction model too. *) + L.d_printfln_escaped "/!\\ Unknown call to %a" Procname.pp callee_pname ; + if is_external callee_pname then ( + L.(debug BufferOverrun Verbose) + "/!\\ External call to unknown %a \n\n" Procname.pp callee_pname ; + assign_symbolic_pname_value callee_pname params ret location mem ) + else if is_non_static callee_pname then ( + L.(debug BufferOverrun Verbose) + "/!\\ Non-static call to unknown %a \n\n" Procname.pp callee_pname ; + assign_symbolic_pname_value callee_pname params ret location mem ) + else Dom.Mem.add_unknown_from ret ~callee_pname ~location mem ) ) | Call (((id, _) as ret), fun_exp, _, location, _) -> let mem = Dom.Mem.add_stack_loc (Loc.of_id id) mem in L.d_printfln_escaped "/!\\ Call to non-const function %a" Exp.pp fun_exp ; diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 8917de708..114972566 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -234,7 +234,8 @@ let rec check_expr_for_integer_overflow integer_type_widths exp location mem con let instantiate_cond : - Typ.IntegerWidths.t + is_params_ref:bool + -> Typ.IntegerWidths.t -> Procname.t -> (Pvar.t * Typ.t) list -> (Exp.t * Typ.t) list @@ -242,8 +243,11 @@ let instantiate_cond : -> BufferOverrunCheckerSummary.t -> Location.t -> PO.ConditionSet.checked_t = - fun integer_type_widths callee_pname callee_formals params caller_mem callee_cond location -> - let eval_sym_trace = Sem.mk_eval_sym_trace integer_type_widths callee_formals params caller_mem in + fun ~is_params_ref integer_type_widths callee_pname callee_formals params caller_mem callee_cond + location -> + let eval_sym_trace = + Sem.mk_eval_sym_trace ~is_params_ref integer_type_widths callee_formals params caller_mem + in let latest_prune = Dom.Mem.get_latest_prune caller_mem in PO.ConditionSet.subst callee_cond eval_sym_trace callee_pname location latest_prune @@ -292,13 +296,16 @@ let check_instr : in check model_env mem cond_set | None -> ( - match (get_checks_summary callee_pname, get_formals callee_pname) with - | Some callee_condset, Some callee_formals -> - instantiate_cond integer_type_widths callee_pname callee_formals params mem - callee_condset location - |> PO.ConditionSet.join cond_set - | _, _ -> - (* unknown call / no inferbo payload *) cond_set ) ) + let {BoUtils.ReplaceCallee.pname= callee_pname; params; is_params_ref} = + BoUtils.ReplaceCallee.replace_make_shared tenv get_formals callee_pname params + in + match (get_checks_summary callee_pname, get_formals callee_pname) with + | Some callee_condset, Some callee_formals -> + instantiate_cond ~is_params_ref integer_type_widths callee_pname callee_formals params + mem callee_condset location + |> PO.ConditionSet.join cond_set + | _, _ -> + (* unknown call / no inferbo payload *) cond_set ) ) | Sil.Prune (exp, location, _, _) -> check_expr_for_integer_overflow integer_type_widths exp location mem cond_set | _ -> diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 3792de331..ed6c99186 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -453,10 +453,23 @@ let eval_sympath ~mode params sympath mem = (ArrayBlk.get_size ~cost_mode:(is_cost_mode mode) (Val.get_array_blk v), Val.get_traces v) -let mk_eval_sym_trace integer_type_widths (callee_formals : (Pvar.t * Typ.t) list) - (actual_exps : (Exp.t * Typ.t) list) caller_mem = +let mk_eval_sym_trace ?(is_params_ref = false) integer_type_widths + (callee_formals : (Pvar.t * Typ.t) list) (actual_exps : (Exp.t * Typ.t) list) caller_mem = let params = - let actuals = List.map ~f:(fun (a, _) -> eval integer_type_widths a caller_mem) actual_exps in + let actuals = + if is_params_ref then + match actual_exps with + | [] -> + [] + | (this, _) :: actual_exps -> + let this_actual = eval integer_type_widths this caller_mem in + let actuals = + List.map actual_exps ~f:(fun (a, _) -> + Mem.find_set (eval_locs a caller_mem) caller_mem ) + in + this_actual :: actuals + else List.map ~f:(fun (a, _) -> eval integer_type_widths a caller_mem) actual_exps + in ParamBindings.make callee_formals actuals in let eval_sym ~mode s bound_end = diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.mli b/infer/src/bufferoverrun/bufferOverrunSemantics.mli index 2cee69132..945759e95 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.mli +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.mli @@ -62,7 +62,8 @@ type eval_mode = the cost values only care about the upperbounds. *) val mk_eval_sym_trace : - Typ.IntegerWidths.t + ?is_params_ref:bool + -> Typ.IntegerWidths.t -> (Pvar.t * Typ.t) list -> (Exp.t * Typ.t) list -> BufferOverrunDomain.Mem.t diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index 3afda4bac..95b1146b1 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -330,3 +330,66 @@ module Check = struct end type get_formals = Procname.t -> (Pvar.t * Typ.t) list option + +module ReplaceCallee = struct + type replaced = {pname: Procname.t; params: (Exp.t * Typ.t) list; is_params_ref: bool} + + let is_cpp_constructor_with_types get_formals class_typ param_ref_typs pname = + let num_params = List.length param_ref_typs in + match pname with + | Procname.ObjC_Cpp {kind= CPPConstructor _; parameters} + when Int.equal (List.length parameters) num_params -> ( + match get_formals pname |> Option.map ~f:(List.map ~f:snd) with + | Some (this_typ :: formal_typs) -> ( + Typ.is_ptr_to class_typ ~ptr:this_typ + && + match + List.for_all2 param_ref_typs formal_typs ~f:(fun param_ref_typ formal_typ -> + Typ.is_ptr_to formal_typ ~ptr:param_ref_typ ) + with + | List.Or_unequal_lengths.Ok b -> + b + | List.Or_unequal_lengths.Unequal_lengths -> + false ) + | _ -> + false ) + | _ -> + false + + + let get_cpp_constructor_of_make_shared tenv get_formals = + let rec strip_ttype = function + | [] -> + Some [] + | Typ.TType x :: tl -> + Option.map (strip_ttype tl) ~f:(fun tl -> x :: tl) + | _ -> + None + in + function + | Procname.C ({template_args= Typ.Template {args}} as name) when Procname.C.is_make_shared name + -> ( + match strip_ttype args with + | Some (class_typ_templ :: param_typs_templ) -> + let open Option.Let_syntax in + let%bind class_name = Typ.name class_typ_templ in + let%bind {Struct.methods} = Tenv.lookup tenv class_name in + List.find methods + ~f:(is_cpp_constructor_with_types get_formals class_typ_templ param_typs_templ) + | _ -> + None ) + | _ -> + None + + + let replace_make_shared tenv get_formals pname params = + match get_cpp_constructor_of_make_shared tenv get_formals pname with + | Some constr -> + (* NOTE: This replaces the pointer to the target object. In the parameters of + [std::make_shared], the pointer is on the last place. On the other hand, it is on the + first place in the constructor's parameters. *) + let params = IList.move_last_to_first params in + {pname= constr; params; is_params_ref= true} + | None -> + {pname; params; is_params_ref= false} +end diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.mli b/infer/src/bufferoverrun/bufferOverrunUtils.mli index 18737a9a2..c4f9ef1c6 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.mli +++ b/infer/src/bufferoverrun/bufferOverrunUtils.mli @@ -94,3 +94,20 @@ module Check : sig end type get_formals = Procname.t -> (Pvar.t * Typ.t) list option + +module ReplaceCallee : sig + (** Replaced proc name with its modified parameters. + + [is_params_ref] represents that the parameters are given as references to variables, e.g., + when [int i = 5;], the function of [std::make_shared(i);] in C++ is translated to + [std::make_shared(&i, tgt)] in Sil where [tgt] is the variable for the target object, + rather than [std::make_shared(i, tgt)] (note that the type of [&i] is [int&]). + + The [is_params_ref] value is used to evaluate parameters correctly after replacing the callee. + For example, when we replace [std::make_shared(&i, tgt)] to the constructor call of [C], + i.e. [C(tgt, i)], the parameters' order and types are slightly different, so which should be + handled correctly later in the instantiation phase. *) + type replaced = {pname: Procname.t; params: (Exp.t * Typ.t) list; is_params_ref: bool} + + val replace_make_shared : Tenv.t -> get_formals -> Procname.t -> (Exp.t * Typ.t) list -> replaced +end diff --git a/infer/src/istd/IList.ml b/infer/src/istd/IList.ml index e588a352c..7c532147a 100644 --- a/infer/src/istd/IList.ml +++ b/infer/src/istd/IList.ml @@ -204,3 +204,15 @@ let fold2_result ~init ~f l1 l2 = let eval_until_first_some thunks = List.find_map thunks ~f:(fun f -> f ()) + +let move_last_to_first = + let rec move_last_to_first_helper l rev_acc = + match l with + | [] -> + [] + | [a] -> + a :: List.rev rev_acc + | hd :: tl -> + move_last_to_first_helper tl (hd :: rev_acc) + in + fun l -> move_last_to_first_helper l [] diff --git a/infer/src/istd/IList.mli b/infer/src/istd/IList.mli index 10b306b37..7c86da60c 100644 --- a/infer/src/istd/IList.mli +++ b/infer/src/istd/IList.mli @@ -67,3 +67,5 @@ val fold2_result : -> 'a list -> 'b list -> ('acc, 'err) result Base.List.Or_unequal_lengths.t + +val move_last_to_first : 'a list -> 'a list diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 24bd7e734..332ec2740 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -71,6 +71,8 @@ codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM::lI_FP, 2, INTEGER_OVERFLOW_ codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM::uI, 0, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: std::unique_ptr,std::default_delete>>::operator->,Array access: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good_FP, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Call,Assignment,Assignment,Call,Parameter `t->bI`,Call,Assignment,Call,,Parameter `bi`,Binary operation: ([-oo, +oo] - 1):signed32 by call to `ral_good` ] 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/smart_ptr.cpp, smart_ptr::use_shared_ptr1_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Assignment,Call,,Parameter `i`,,Array declaration,Array access: Offset: 8 Size: 5 by call to `smart_ptr::my_class::my_class` ] +codetoanalyze/cpp/bufferoverrun/smart_ptr.cpp, smart_ptr::use_shared_ptr2_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Assignment,Call,,Parameter `j`,,Array declaration,Array access: Offset: 16 Size: 10 by call to `smart_ptr::my_class::my_class` ] 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, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 5] codetoanalyze/cpp/bufferoverrun/std_array.cpp, array_iter3_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 5] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/smart_ptr.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/smart_ptr.cpp new file mode 100644 index 000000000..a90159a1b --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/smart_ptr.cpp @@ -0,0 +1,46 @@ +/* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ + +#include + +class smart_ptr { + public: + class my_class { + public: + my_class(int i) { + int a[5]; + a[i] = 0; + } + + my_class(int i, int j) { + int a[10]; + a[i + j] = 0; + } + }; + + void use_shared_ptr1_Good() { + int i = 3; + std::shared_ptr p = std::make_shared(i); + } + + void use_shared_ptr1_Bad() { + int i = 8; + std::shared_ptr p = std::make_shared(i); + } + + void use_shared_ptr2_Good() { + int i = 3; + int j = 5; + std::shared_ptr p = std::make_shared(i, j); + } + + void use_shared_ptr2_Bad() { + int i = 8; + int j = 8; + std::shared_ptr p = std::make_shared(i, j); + } +};