[inferbo] Ondemand value generation of vector as function parameter

Summary:
It generates vector value ondemand when it is given as a parameter.

Depends on D16645589

Reviewed By: ezgicicek

Differential Revision: D16645624

fbshipit-source-id: 7498c8ab2

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -424,6 +424,12 @@ module Val = struct
       let trace = if Loc.is_global l then Trace.Global l else Trace.Parameter l in
       TraceSet.singleton location trace
     in
+    let ptr_to_c_array_alloc deref_path size =
+      let allocsite = Allocsite.make_symbol deref_path in
+      let offset = Itv.zero in
+      let traces = traces_of_loc (Loc.of_path deref_path) in
+      of_c_array_alloc allocsite ~stride:None ~offset ~size ~traces
+    in
     let is_java = Language.curr_language_is Java in
     L.d_printfln_escaped "Val.of_path %a : %a%s%s" SPath.pp_partial path (Typ.pp Pp.text) typ
       (if may_last_field then ", may_last_field" else "")
@@ -457,7 +463,10 @@ module Val = struct
               | _ ->
                   Itv.nat
             in
-            let offset = Itv.of_offset_path ~is_void:(Typ.is_pointer_to_void typ) path in
+            let offset =
+              if SPath.is_cpp_vector_elem path then Itv.zero
+              else Itv.of_offset_path ~is_void:(Typ.is_pointer_to_void typ) path
+            in
             let size = Itv.of_length_path ~is_void:(Typ.is_pointer_to_void typ) path in
             ArrayBlk.make_c allocsite ~stride ~offset ~size
           in
@@ -466,12 +475,14 @@ module Val = struct
       match BufferOverrunTypModels.dispatch tenv typename with
       | Some (CArray {deref_kind; length}) ->
           let deref_path = SPath.deref ~deref_kind path in
-          let l = Loc.of_path deref_path in
-          let traces = traces_of_loc l in
-          let allocsite = Allocsite.make_symbol deref_path in
-          let offset = Itv.zero in
           let size = Itv.of_int_lit length in
-          of_c_array_alloc allocsite ~stride:None ~offset ~size ~traces
+          ptr_to_c_array_alloc deref_path size
+      | Some (CppStdVector {element_typ}) ->
+          let deref_path =
+            SPath.field path (BufferOverrunField.cpp_vector_elem ~classname:typename element_typ)
+          in
+          let size = Itv.of_length_path ~is_void:false path in
+          ptr_to_c_array_alloc deref_path size
       | Some JavaCollection ->
           let deref_path = SPath.deref ~deref_kind:Deref_ArrayIndex path in
           let l = Loc.of_path deref_path in

infer/src/bufferoverrun/bufferOverrunField.ml

@@ -30,9 +30,15 @@ let pp ~pp_lhs ~pp_lhs_alone ~sep f lhs fn =
 let mk, get_type =
   let classname = "__infer__" in
   let types = ref Typ.Fieldname.Map.empty in
-  let mk name typ =
+  let mk ?cpp_classname name typ =
-    let fullname = Format.sprintf "%s.%s" classname name in
+    let fieldname =
-    let fieldname = Typ.Fieldname.Java.from_string fullname in
+      match cpp_classname with
+      | None ->
+          let fullname = Format.sprintf "%s.%s" classname name in
+          Typ.Fieldname.Java.from_string fullname
+      | Some classname ->
+          Typ.Fieldname.Clang.from_class_name classname name
+    in
     types := Typ.Fieldname.Map.add fieldname typ !types ;
     fieldname
   in
@@ -44,3 +50,14 @@ let java_collection_internal_array = mk "java.collection.$elements." Typ.(mk_arr
 
 let c_strlen () =
   if Language.curr_language_is Java then mk "length" Typ.uint else mk "c.strlen" Typ.uint
+
+
+let cpp_vector_elem_str = "cpp.vector_elem"
+
+let cpp_vector_elem ~classname elt_typ =
+  let desc = Typ.Tptr (elt_typ, Typ.Pk_pointer) in
+  mk ~cpp_classname:classname cpp_vector_elem_str {Typ.desc; quals= Typ.mk_type_quals ()}
+
+
+let is_cpp_vector_elem fn =
+  String.equal (Typ.Fieldname.to_simplified_string fn) cpp_vector_elem_str

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -645,16 +645,29 @@ end
 
 module StdVector = struct
   (* The (3) constructor in https://en.cppreference.com/w/cpp/container/vector/vector *)
-  let constructor vec_exp size_exp =
+  let constructor elt_typ (vec_exp, vec_typ) size_exp =
     let {exec= malloc_exec; check} = malloc ~can_be_zero:true size_exp in
     let exec ({pname; node_hash; integer_type_widths; location} as model_env) ~ret:((id, _) as ret)
         mem =
       let mem = malloc_exec model_env ~ret mem in
       let vec_locs = Sem.eval_locs vec_exp mem in
+      let classname =
+        match vec_typ.Typ.desc with
+        | Typ.Tptr (vec_typ, _) -> (
+          match Typ.name vec_typ with
+          | None ->
+              L.(die InternalError)
+                "Unknown class name of vector `%a`" (Typ.pp_full Pp.text) vec_typ
+          | Some t ->
+              t )
+        | _ ->
+            L.(die InternalError) "First parameter of constructor should be a pointer."
+      in
       let deref_of_vec =
         Allocsite.make pname ~node_hash ~inst_num:1 ~dimension:1 ~path:None
           ~represents_multiple_values:false
         |> Loc.of_allocsite
+        |> Loc.append_field ~fn:(BufferOverrunField.cpp_vector_elem ~classname elt_typ)
       in
       let array_v =
         Sem.eval integer_type_widths (Exp.Var id) mem
@@ -1012,8 +1025,11 @@ module Call = struct
         $+ any_arg_of_typ (-"std" &:: "basic_string")
         $--> by_value Dom.Val.Itv.unknown_bool
       ; -"std" &:: "basic_string" &::.*--> no_model
-      ; -"std" &:: "vector" < any_typ &+ any_typ >:: "vector" $ capt_exp $+ capt_exp
+      ; -"std" &:: "vector"
-        $--> StdVector.constructor
+        < capt_typ `T
+        &+ any_typ >:: "vector"
+        $ capt_arg_of_typ (-"std" &:: "vector")
+        $+ capt_exp $--> StdVector.constructor
       ; -"std" &:: "vector" < any_typ &+ any_typ >:: "operator[]" $ capt_exp $+ capt_exp
         $--> StdVector.at
       ; -"std" &:: "vector" < any_typ &+ any_typ >:: "size" $ capt_exp $--> StdVector.size

infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml

@@ -42,6 +42,8 @@ let mk pdesc =
             match BufferOverrunTypModels.dispatch tenv typename with
             | Some (CArray {element_typ}) ->
                 Some element_typ
+            | Some (CppStdVector {element_typ}) ->
+                Some (Typ.mk (Typ.Tptr (element_typ, Typ.Pk_pointer)))
             | Some _ ->
                 L.internal_error "Deref of non-array modeled type `%a`" Typ.Name.pp typename ;
                 None

infer/src/bufferoverrun/bufferOverrunTypModels.ml

@@ -9,12 +9,15 @@ open! IStd
 
 type typ_model =
   | CArray of {element_typ: Typ.t; deref_kind: Symb.SymbolPath.deref_kind; length: IntLit.t}
+  | CppStdVector of {element_typ: Typ.t}
   | JavaCollection
 
 let std_array element_typ length =
   CArray {element_typ; deref_kind= Symb.SymbolPath.Deref_ArrayIndex; length= IntLit.of_int64 length}
 
 
+let std_vector element_typ = CppStdVector {element_typ}
+
 (* Java's Collections are represented by their size. We don't care about the elements.
 - when they are constructed, we set the size to 0
 - each time we add an element, we increase the length of the array
@@ -26,6 +29,7 @@ let dispatch : (Tenv.t, typ_model) ProcnameDispatcher.TypName.dispatcher =
   let open ProcnameDispatcher.TypName in
   make_dispatcher
     [ -"std" &:: "array" < capt_typ `T &+ capt_int >--> std_array
+    ; -"std" &:: "vector" < capt_typ `T &+ any_typ >--> std_vector
     ; +PatternMatch.implements_collection &::.*--> collection
     ; +PatternMatch.implements_iterator &::.*--> collection
     ; +PatternMatch.implements_org_json "JSONArray" &::.*--> collection ]

infer/src/bufferoverrun/bufferOverrunUtils.ml

@@ -59,7 +59,7 @@ module Exec = struct
       | Some (CArray {element_typ; length}) ->
           decl_local_array model_env loc element_typ ~length:(Some length) ~inst_num
             ~represents_multiple_values ~dimension mem
-      | Some JavaCollection | None ->
+      | Some (CppStdVector _) | Some JavaCollection | None ->
           (mem, inst_num) )
     | _ ->
         (mem, inst_num)

infer/src/bufferoverrun/symb.ml

@@ -232,6 +232,13 @@ module SymbolPath = struct
         is_void
     | Normal _ | Modeled _ ->
         false
+
+
+  let is_cpp_vector_elem = function
+    | Field (fn, _) ->
+        BufferOverrunField.is_cpp_vector_elem fn
+    | _ ->
+        false
 end
 
 module Symbol = struct

infer/src/bufferoverrun/symb.mli

@@ -87,6 +87,8 @@ module SymbolPath : sig
   val exists_str_partial : f:(string -> bool) -> partial -> bool
 
   val is_void_ptr_path : t -> bool
+
+  val is_cpp_vector_elem : partial -> bool
 end
 
 module Symbol : sig

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

@@ -44,8 +44,6 @@ codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_condition
 codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_minus_2_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,<LHS trace>,Parameter `size`,Binary operation: (0 - 1):unsigned32 by call to `conditional_minus` ]
 codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 5, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Length trace>,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, [<Length trace>,Array declaration,Array access: Offset: 30 Size: 10]
-codetoanalyze/cpp/bufferoverrun/folly_memory_UninitializedMemoryHacks.cpp, folly::resizeWithoutInitialization<int,_void>, 1, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
-codetoanalyze/cpp/bufferoverrun/folly_memory_UninitializedMemoryHacks.cpp, folly::resizeWithoutInitialization<int,_void>, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_by_ref_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Call,Assignment,<Length trace>,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, [<Offset trace>,Call,Parameter `length`,Assignment,<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
 codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Assignment,Array access: Offset: 5 Size: 5]
@@ -62,8 +60,11 @@ codetoanalyze/cpp/bufferoverrun/relation.cpp, call2_plus_params_Bad, 0, BUFFER_O
 codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C::foo_Bad, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C::foo_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
 codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C::goo, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
+codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>::fB_FP, 0, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Parameter `*o`,Call,Parameter `*k`,Call,Parameter `*k`,Assignment,Assignment,Binary operation: ([-oo, +oo] + 1):unsigned64]
 codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>::lI_FP, 2, 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, LM<TFM>::lI_FP, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Call,Parameter `*o`,Call,Parameter `*k`,Call,Parameter `*k`,Assignment,Assignment,Assignment,Assignment,Binary operation: ([-oo, +oo] - 1):signed32]
 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/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]
@@ -108,13 +109,12 @@ codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_assert_Good_2, 6, BUFFER_OVERRUN_
 codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_data_Good, 3, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Length trace>,Unknown value from: std::vector<int,std::allocator<int>>::data,Assignment,Array access: Offset: [-oo, +oo] (⇐ [-oo, +oo] + 4) Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_push_back_Good, 3, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Length trace>,Unknown value from: std::vector<int,std::allocator<int>>::operator[],Array access: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_reserve_Good, 4, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Length trace>,Unknown value from: std::vector<int,std::allocator<int>>::operator[],Array access: Offset: [-oo, +oo] Size: [0, +oo]]
-codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_safe_access2, 6, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
-codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_safe_access2, 6, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_safe_access3_Good, 3, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Length trace>,Unknown value from: std::vector<int,std::allocator<int>>::operator[],Array access: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_safe_access6, 2, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Offset trace>,Unknown value from: std::vector<int,std::allocator<int>>::empty,<Length trace>,Array declaration,Assignment,Array access: Offset: [-oo, +oo] Size: 2]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 6, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Length trace>,Unknown value from: std::vector<int,std::allocator<int>>::operator[],Array access: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, constructor_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Array access: Offset: 3 Size: 1]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Length trace>,Unknown value from: std::vector<int,std::allocator<int>>::data,Assignment,Array access: Offset: [-oo, +oo] (⇐ [-oo, +oo] + [-oo, +oo]) Size: [0, +oo]]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Parameter `*v->vector_elem`,Assignment,<Length trace>,Parameter `*v->vector_elem`,Array access: Offset: v->vector_elem.length Size: v->vector_elem.length]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,Parameter `*init`,Assignment,Call,Parameter `*__param_0->a`,Assignment,Call,<Length trace>,Parameter `count`,Call,Parameter `idx`,Assignment,Array access: Offset: -1 Size: 10 by call to `access_minus_one` ]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Array declaration,Call,Parameter `*init`,Assignment,Call,Parameter `*__param_0->a`,Assignment,Call,<Length trace>,Parameter `count`,Call,Parameter `idx`,Assignment,Array access: Offset: [-1, 0] Size: 10 by call to `access_minus_one` ]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Length trace>,Unknown value from: std::vector<int,std::allocator<int>>::operator[],Array access: Offset: [-oo, +oo] Size: [0, +oo]]

infer/tests/codetoanalyze/cpp/bufferoverrun/repro1.cpp

@@ -74,7 +74,7 @@ struct LM {
   void l(lt& t, const lo& o) { lI_FP(t, o); }
   void tL(lt& t, const lo& o) { lI_FP(t, o); }
   void u(lt& t, const lo& o) {
-    ASSERT(fB(o) == t.bI);
+    ASSERT(fB_FP(o) == t.bI);
     if (t.bI == kBN) {
       return;
     }
@@ -83,9 +83,9 @@ struct LM {
   }
 
  private:
-  BI fB(const lo& o) { return (BI)th((const void*)&o) % b.size() + 1; }
+  BI fB_FP(const lo& o) { return (BI)th((const void*)&o) % b.size() + 1; }
   void lI_FP(lt& t, const lo& o) {
-    auto bi = fB(o);
+    auto bi = fB_FP(o);
     auto r = b[bi - 1]->lO(o);
     if (r != TLOR::S) {
       t.bI = kBN;
@@ -133,7 +133,7 @@ struct arh {
   ft i1;
 };
 
-static void am_Good(im* it) {
+static void am_Good_FP(im* it) {
   const arh* ch = (const arh*)it->gKPC();
   const ai a = aft(ch->i1);
   lt at;

infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp

@@ -8,7 +8,7 @@
 #include <list>
 #include <assert.h>
 
-void FN_out_of_bound_Bad(std::vector<int> v) {
+void out_of_bound_Bad(std::vector<int> v) {
   unsigned int n = v.size();
   v[n] = 1;
 }
@@ -69,7 +69,7 @@ void call_safe_access_Good() {
   safe_access(v);
 }
 
-void FP_safe_access2(std::vector<int> v) {
+void safe_access2(std::vector<int> v) {
   if (v.empty()) {
     return;
   }
@@ -82,7 +82,7 @@ void FP_safe_access2(std::vector<int> v) {
 
 void call_safe_access2_Good() {
   std::vector<int> v;
-  FP_safe_access2(v);
+  safe_access2(v);
 }
 
 void FP_safe_access3_Good() {