[inferbo] Add vector model: push_back

Summary:
It adds a model of vector::push_back

Depends on D16687225

Reviewed By: ezgicicek

Differential Revision: D16687269

fbshipit-source-id: 9d2a73fca

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -728,6 +728,25 @@ module StdVector = struct
 
   let get_size vec_exp mem = eval_array_locs_length (deref_of vec_exp mem) mem
 
+  let set_size {location} vec_exp new_size mem =
+    let locs = deref_of vec_exp mem in
+    Dom.Mem.transform_mem locs mem ~f:(fun v ->
+        Dom.Val.set_array_length location ~length:new_size v )
+
+
+  let push_back vec_exp elt_exp =
+    let exec model_env ~ret:_ mem =
+      let mem =
+        let new_size = Dom.Val.plus_a (get_size vec_exp mem) (Dom.Val.of_int 1) in
+        set_size model_env vec_exp new_size mem
+      in
+      let elt_locs = Dom.Val.get_all_locs (Dom.Mem.find_set (deref_of vec_exp mem) mem) in
+      let elt_v = Dom.Mem.find_set (Sem.eval_locs elt_exp mem) mem in
+      Dom.Mem.update_mem elt_locs elt_v mem
+    in
+    {exec; check= no_check}
+
+
   let size vec_exp =
     let exec _ ~ret:(id, _) mem =
       let mem = Dom.Mem.add_stack (Loc.of_id id) (get_size vec_exp mem) mem in
@@ -1101,6 +1120,9 @@ module Call = struct
         $+? any_arg $--> StdVector.constructor_copy
       ; -"std" &:: "vector" < any_typ &+ any_typ >:: "operator[]" $ capt_exp $+ capt_exp
         $--> StdVector.at
+      ; -"std" &:: "vector" < any_typ &+ any_typ >:: "push_back" $ capt_exp $+ capt_exp
+        $--> StdVector.push_back
+      ; -"std" &:: "vector" < any_typ &+ any_typ >:: "reserve" $ any_arg $+ any_arg $--> no_model
       ; -"std" &:: "vector" < any_typ &+ any_typ >:: "size" $ capt_exp $--> StdVector.size
       ; +PatternMatch.implements_collection
         &:: "<init>" <>$ capt_var_exn $+ capt_exp $--> Collection.init

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

@@ -111,16 +111,15 @@ codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_call_safe_access2_Good, 2, INFERB
 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_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_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_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_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_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 6 Size: 5]
 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_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Array access: Offset: 1 Size: 0]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]
 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

@@ -33,7 +33,7 @@ void constructor_Bad() {
   v[3] = 2;
 }
 
-void FP_push_back_Good() {
+void push_back_Good() {
   std::vector<int> v;
   v.push_back(1);
   v[0] = 2;
@@ -45,7 +45,7 @@ void push_back_Bad() {
   v[1] = 2;
 }
 
-void FP_reserve_Good() {
+void reserve_Good() {
   std::vector<int> v;
   v.reserve(42);
   v.push_back(1);
@@ -156,7 +156,7 @@ void assert_Good_2(int x) {
   v[4] = 1;
 }
 
-void FN_assert_Bad() {
+void assert_Bad() {
   std::vector<int> v;
   for (int i = 0; i < 5; i++) {
     v.push_back(1);