[inferbo] Add models of vector constructors

Summary:
It adds models of vector constructors.

Depends on D16645624

Reviewed By: ezgicicek

Differential Revision: D16687167

fbshipit-source-id: eac49df6d

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -644,25 +644,26 @@ module StdBasicString = struct
 end
 
 module StdVector = struct
-  (* The (3) constructor in https://en.cppreference.com/w/cpp/container/vector/vector *)
+  let get_classname vec_typ =
-  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)
+          L.(die InternalError) "Unknown class name of vector `%a`" (Typ.pp_full Pp.text) vec_typ
-                "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
+
+
+  (* The (3) constructor in https://en.cppreference.com/w/cpp/container/vector/vector *)
+  let constructor_size 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 = get_classname vec_typ in
       let deref_of_vec =
         Allocsite.make pname ~node_hash ~inst_num:1 ~dimension:1 ~path:None
           ~represents_multiple_values:false
@@ -680,6 +681,30 @@ module StdVector = struct
     {exec; check}
 
 
+  (* The (1) constructor in https://en.cppreference.com/w/cpp/container/vector/vector *)
+  let constructor_empty elt_typ vec = constructor_size elt_typ vec Exp.zero
+
+  (* The (5) constructor in https://en.cppreference.com/w/cpp/container/vector/vector *)
+  let constructor_copy elt_typ (vec_exp, vec_typ) src_exp =
+    let exec {integer_type_widths} ~ret:_ mem =
+      let vec_locs, traces =
+        let v = Sem.eval integer_type_widths vec_exp mem in
+        (Dom.Val.get_all_locs v, Dom.Val.get_traces v)
+      in
+      let deref_of_vec =
+        let classname = get_classname vec_typ in
+        PowLoc.append_field vec_locs ~fn:(BufferOverrunField.cpp_vector_elem ~classname elt_typ)
+      in
+      let deref_of_src =
+        Dom.Mem.find_set (Sem.eval_locs src_exp mem) mem |> Dom.Val.get_all_locs
+      in
+      mem
+      |> Dom.Mem.update_mem vec_locs (Dom.Val.of_pow_loc ~traces deref_of_vec)
+      |> Dom.Mem.update_mem deref_of_vec (Dom.Mem.find_set deref_of_src mem)
+    in
+    {exec; check= no_check}
+
+
   let at vec_exp index_exp =
     let exec {pname; location} ~ret:(id, _) mem =
       let deref_of_vec = Dom.Mem.find_set (Sem.eval_locs vec_exp mem) mem in
@@ -1058,7 +1083,19 @@ module Call = struct
         < capt_typ `T
         &+ any_typ >:: "vector"
         $ capt_arg_of_typ (-"std" &:: "vector")
-        $+ capt_exp $--> StdVector.constructor
+        $--> StdVector.constructor_empty
+      ; -"std" &:: "vector"
+        < capt_typ `T
+        &+ any_typ >:: "vector"
+        $ capt_arg_of_typ (-"std" &:: "vector")
+        $+ capt_exp_of_prim_typ (Typ.mk (Typ.Tint Typ.size_t))
+        $+? any_arg $--> StdVector.constructor_size
+      ; -"std" &:: "vector"
+        < capt_typ `T
+        &+ any_typ >:: "vector"
+        $ capt_arg_of_typ (-"std" &:: "vector")
+        $+ capt_exp_of_typ (-"std" &:: "vector")
+        $+? any_arg $--> StdVector.constructor_copy
       ; -"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/tests/codetoanalyze/cpp/bufferoverrun/folly_split.cpp

@@ -42,19 +42,19 @@ void splitTo(const Delim& delimiter,
 } // namespace folly
 
 namespace folly_split {
-std::string do_not_ignore_empty_Good(const std::string& s) {
+std::string FP_do_not_ignore_empty_Good(const std::string& s) {
   std::vector<std::string> v;
   folly::split("delimiter", s, v);
   return v[0];
 }
 
-std::string do_not_ignore_empty2_Good(const std::string& s) {
+std::string FP_do_not_ignore_empty2_Good(const std::string& s) {
   std::vector<std::string> v;
   folly::split("delimiter", s, v, false);
   return v[0];
 }
 
-std::string FN_do_not_ignore_empty_Bad(const std::string& s) {
+std::string do_not_ignore_empty_Bad(const std::string& s) {
   std::vector<std::string> v;
   folly::split("delimiter", s, v, true);
   return v[0];

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

@@ -44,6 +44,9 @@ 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_split.cpp, folly_split::FP_do_not_ignore_empty2_Good, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,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, [<Length trace>,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, [<Length trace>,Array declaration,Assignment,Array access: Offset: 0 Size: 0]
 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]
@@ -104,20 +107,21 @@ codetoanalyze/cpp/bufferoverrun/std_string.cpp, to_string2_Good, 6, CONDITION_AL
 codetoanalyze/cpp/bufferoverrun/symb_arr.cpp, symb_arr_alloc::symb_arr_access_bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Parameter `this->h[*]`,Array access: Offset: 10 Size: 10]
 codetoanalyze/cpp/bufferoverrun/this.cpp, CThis::access_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `this->n`,<Length trace>,Parameter `this->n`,Array declaration,Array access: Offset: this->n + 1 Size: this->n + 1]
 codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
-codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_assert_Good, 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, FP_call_safe_access2_Good, 2, INFERBO_ALLOC_IS_ZERO, no_bucket, ERROR, [Array declaration,Assignment,Call,Parameter `*v->vector_elem`,Allocation: Length: 0 by call to `safe_access2` ]
-codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_assert_Good_2, 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, FP_call_safe_access4_Good, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,<Length trace>,Parameter `*v->vector_elem`,Array access: Offset: 0 Size: 0 by call to `safe_access4` ]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_call_safe_access5_Good, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,<Length trace>,Parameter `*v->vector_elem`,Array access: Offset: 0 Size: 0 by call to `safe_access5` ]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_call_safe_access_Good, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,<Length trace>,Parameter `*v->vector_elem`,Array access: Offset: 9 Size: 5 by call to `safe_access` ]
 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_push_back_Good, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Array access: Offset: 0 Size: 0]
-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_reserve_Good, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Array access: Offset: 0 Size: 0]
-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_access3_Good, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Array access: Offset: 0 Size: 0]
 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]]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Array access: Offset: 1 Size: 0]
-codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_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]]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Array access: Offset: 0 Size: 0]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, simple_size_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Array declaration,Assignment,<Length trace>,Array declaration,Assignment,Array access: Offset: 3 Size: 3]
 codetoanalyze/cpp/bufferoverrun/void_ptr.cpp, FP_call_casting_void_ptr_Ok, 2, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Array declaration,Call,<Length trace>,Parameter `*p`,Assignment,Array access: Offset: 14 Size: 2 by call to `casting_void_ptr` ]

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

@@ -64,7 +64,7 @@ void safe_access(std::vector<int> v) {
   }
 }
 
-void call_safe_access_Good() {
+void FP_call_safe_access_Good() {
   std::vector<int> v(5, 0);
   safe_access(v);
 }
@@ -80,7 +80,7 @@ void safe_access2(std::vector<int> v) {
   }
 }
 
-void call_safe_access2_Good() {
+void FP_call_safe_access2_Good() {
   std::vector<int> v;
   safe_access2(v);
 }
@@ -98,7 +98,7 @@ void safe_access4(std::vector<int> v) {
   }
 }
 
-void call_safe_access4_Good() {
+void FP_call_safe_access4_Good() {
   std::vector<int> v;
   safe_access4(v);
 }
@@ -110,7 +110,7 @@ void safe_access5(std::vector<int> v) {
   }
 }
 
-void call_safe_access5_Good() {
+void FP_call_safe_access5_Good() {
   std::vector<int> v;
   safe_access5(v);
 }
@@ -138,7 +138,7 @@ void data_Bad() {
   p[v[4]] = 1;
 }
 
-void FP_assert_Good() {
+void assert_Good() {
   std::vector<int> v;
   for (int i = 0; i < 5; i++) {
     v.push_back(1);
@@ -147,7 +147,7 @@ void FP_assert_Good() {
   v[4] = 1;
 }
 
-void FP_assert_Good_2(int x) {
+void assert_Good_2(int x) {
   std::vector<int> v;
   for (int i = 0; i < 5; i++) {
     v.push_back(1);
@@ -156,7 +156,7 @@ void FP_assert_Good_2(int x) {
   v[4] = 1;
 }
 
-void assert_Bad() {
+void FN_assert_Bad() {
   std::vector<int> v;
   for (int i = 0; i < 5; i++) {
     v.push_back(1);