[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<C>(i)` to the constructor `C(i)`.

Reviewed By: ngorogiannis

Differential Revision: D19432338

fbshipit-source-id: 0d838e555

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

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

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 =

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 *)

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
+   fun ~is_params_ref integer_type_widths ret callee_formals callee_pname params caller_mem
-       location ->
+       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
+              let {BoUtils.ReplaceCallee.pname= callee_pname; params; is_params_ref} =
-            | Some callee_exit_mem, Some callee_formals ->
+                BoUtils.ReplaceCallee.replace_make_shared tenv get_formals callee_pname params
-                instantiate_mem integer_type_widths ret callee_formals callee_pname params mem
+              in
-                  callee_exit_mem location
+              match (get_summary callee_pname, get_formals callee_pname) with
-            | _, _ ->
+              | Some callee_exit_mem, Some callee_formals ->
-                (* This may happen for procedures with a biabduction model too. *)
+                  instantiate_mem ~is_params_ref integer_type_widths ret callee_formals callee_pname
-                L.d_printfln_escaped "/!\\ Unknown call to %a" Procname.pp callee_pname ;
+                    params mem callee_exit_mem location
-                if is_external callee_pname then (
+              | _, _ ->
-                  L.(debug BufferOverrun Verbose)
+                  (* This may happen for procedures with a biabduction model too. *)
-                    "/!\\ External call to unknown %a \n\n" Procname.pp callee_pname ;
+                  L.d_printfln_escaped "/!\\ Unknown call to %a" Procname.pp callee_pname ;
-                  assign_symbolic_pname_value callee_pname params ret location mem )
+                  if is_external callee_pname then (
-                else if is_non_static callee_pname then (
+                    L.(debug BufferOverrun Verbose)
-                  L.(debug BufferOverrun Verbose)
+                      "/!\\ External call to unknown %a \n\n" Procname.pp callee_pname ;
-                    "/!\\ Non-static call to unknown %a \n\n" Procname.pp callee_pname ;
+                    assign_symbolic_pname_value callee_pname params ret location mem )
-                  assign_symbolic_pname_value callee_pname params ret location mem )
+                  else if is_non_static callee_pname then (
-                else Dom.Mem.add_unknown_from ret ~callee_pname ~location mem ) )
+                    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 ;

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 ->
+ fun ~is_params_ref integer_type_widths callee_pname callee_formals params caller_mem callee_cond
-  let eval_sym_trace = Sem.mk_eval_sym_trace integer_type_widths callee_formals params caller_mem in
+     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
+          let {BoUtils.ReplaceCallee.pname= callee_pname; params; is_params_ref} =
-        | Some callee_condset, Some callee_formals ->
+            BoUtils.ReplaceCallee.replace_make_shared tenv get_formals callee_pname params
-            instantiate_cond integer_type_widths callee_pname callee_formals params mem
+          in
-              callee_condset location
+          match (get_checks_summary callee_pname, get_formals callee_pname) with
-            |> PO.ConditionSet.join cond_set
+          | Some callee_condset, Some callee_formals ->
-        | _, _ ->
+              instantiate_cond ~is_params_ref integer_type_widths callee_pname callee_formals params
-            (* unknown call / no inferbo payload *) cond_set ) )
+                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
   | _ ->

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)
+let mk_eval_sym_trace ?(is_params_ref = false) integer_type_widths
-    (actual_exps : (Exp.t * Typ.t) list) caller_mem =
+    (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 =

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

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

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<C>(i);] in C++ is translated to
+      [std::make_shared<C>(&i, tgt)] in Sil where [tgt] is the variable for the target object,
+      rather than [std::make_shared<C>(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<C>(&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

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 []

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

infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp

@@ -71,6 +71,8 @@ codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>::lI_FP, 2, INTEGER_OVERFLOW_
 codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>::uI, 0, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Length trace>,Unknown value from: std::unique_ptr<LMB<TFM>,std::default_delete<LMB<TFM>>>::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,<LHS trace>,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,<Offset trace>,Parameter `i`,<Length trace>,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,<Offset trace>,Parameter `i`,<Length trace>,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,<Offset trace>,Parameter `j`,<Length trace>,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, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, array_iter2_Bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, array_iter3_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]

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 <memory>
+
+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<my_class> p = std::make_shared<my_class>(i);
+  }
+
+  void use_shared_ptr1_Bad() {
+    int i = 8;
+    std::shared_ptr<my_class> p = std::make_shared<my_class>(i);
+  }
+
+  void use_shared_ptr2_Good() {
+    int i = 3;
+    int j = 5;
+    std::shared_ptr<my_class> p = std::make_shared<my_class>(i, j);
+  }
+
+  void use_shared_ptr2_Bad() {
+    int i = 8;
+    int j = 8;
+    std::shared_ptr<my_class> p = std::make_shared<my_class>(i, j);
+  }
+};