[inferbo] Add vector model: data

Summary:
It adds a vector model of `data` method.

Depends on D16687280

Reviewed By: ezgicicek

Differential Revision: D16689400

fbshipit-source-id: 156016b3c

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -752,6 +752,14 @@ module StdVector = struct
     {exec; check= no_check}
 
 
+  let data vec_exp =
+    let exec _ ~ret:(id, _) mem =
+      let arr = Dom.Mem.find_set (deref_of vec_exp mem) mem in
+      model_by_value arr id mem
+    in
+    {exec; check= no_check}
+
+
   let push_back vec_exp elt_exp =
     let exec model_env ~ret:_ mem =
       let mem =
@@ -1139,6 +1147,7 @@ module Call = struct
       ; -"std" &:: "vector" < any_typ &+ any_typ >:: "operator[]" $ capt_exp $+ capt_exp
         $--> StdVector.at
       ; -"std" &:: "vector" < any_typ &+ any_typ >:: "empty" $ capt_exp $--> StdVector.empty
+      ; -"std" &:: "vector" < any_typ &+ any_typ >:: "data" $ capt_exp $--> StdVector.data
       ; -"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

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

@@ -107,10 +107,9 @@ 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_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, 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, data_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Assignment,Assignment,Array access: Offset: 10 Size: 5]
 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` ]

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

@@ -125,7 +125,7 @@ void call_safe_access6_Good() {
   safe_access6(v);
 }
 
-void FP_data_Good() {
+void data_Good() {
   std::vector<int> v(5);
   int* p = v.data();
   p[4] = 1;