[inferbo] revise semantics of vector::data

Summary:
vector::data returns a pointer to the first value of the vector.

- The size of the (array) pointer should be the same with the vector.
- The pointer should point to the same abstract value with the vector.

Reviewed By: mbouaziz

Differential Revision: D6196592

fbshipit-source-id: cc17096

infer/models/cpp/include/infer_model/vector_bufferoverrun.h

@@ -29,6 +29,8 @@
 
 extern "C" {
 int __inferbo_min(int, int);
+
+void __inferbo_set_size(void* p, int size);
 }
 
 bool __inferbo_empty(int* size) { return 1 - __inferbo_min(*size, 1); }
@@ -233,9 +235,17 @@ class vector {
   reference back() { return (reference)*get(); }
   const_reference back() const { return (const_reference)*get(); }
 
-  value_type* data() noexcept { return get(); }
+  value_type* data() noexcept {
+    value_type* p = get();
+    __inferbo_set_size((void*)&p, infer_size);
+    return p;
+  }
 
-  const value_type* data() const noexcept { return get(); }
+  const value_type* data() const noexcept {
+    value_type* p = get();
+    __inferbo_set_size((void*)&p, infer_size);
+    return p;
+  }
 
   void push_back(const_reference __x);
   void push_back(value_type&& __x);

infer/src/bufferoverrun/arrayBlk.ml

@@ -105,6 +105,8 @@ module ArrInfo = struct
   let prune_ne : t -> t -> t =
     fun arr1 arr2 -> {arr1 with offset= Itv.prune_ne arr1.offset arr2.offset}
 
+
+  let set_size : Itv.t -> t -> t = fun size arr -> {arr with size}
 end
 
 include AbstractDomain.Map (Allocsite) (ArrInfo)
@@ -182,3 +184,5 @@ let prune_comp : Binop.t -> astate -> astate -> astate =
 let prune_eq : astate -> astate -> astate = fun a1 a2 -> do_prune ArrInfo.prune_eq a1 a2
 
 let prune_ne : astate -> astate -> astate = fun a1 a2 -> do_prune ArrInfo.prune_ne a1 a2
+
+let set_size : Itv.t -> astate -> astate = fun size a -> map (ArrInfo.set_size size) a

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -101,6 +101,19 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
           mem
 
 
+  let model_set_size : (Exp.t * Typ.t) list -> Location.t -> Dom.Mem.astate -> Dom.Mem.astate =
+    fun params location mem ->
+      match params with
+      | [(e1, _); (e2, _)] ->
+          let locs = Sem.eval_locs e1 mem location |> Dom.Val.get_pow_loc in
+          let size = Sem.eval e2 mem location |> Dom.Val.get_itv in
+          let arr = Dom.Mem.find_heap_set locs mem in
+          let arr = Dom.Val.set_array_size size arr in
+          Dom.Mem.strong_update_heap locs arr mem
+      | _ ->
+          mem
+
+
   let model_by_value value ret mem =
     match ret with
     | Some (id, _) ->
@@ -144,6 +157,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       match Typ.Procname.get_method callee_pname with
       | "__inferbo_min" ->
           model_min ret params loc mem
+      | "__inferbo_set_size" ->
+          model_set_size params loc mem
       | "__exit" | "exit" ->
           Bottom
       | "fgetc" ->

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -245,6 +245,10 @@ module Val = struct
     fun fmt x -> F.fprintf fmt "(%a, %a)" Itv.pp x.itv ArrayBlk.pp x.arrayblk
 
 
+  let set_array_size : Itv.t -> t -> t =
+    fun size v -> {v with arrayblk= ArrayBlk.set_size size v.arrayblk}
+
+
   module Itv = struct
     let nat = of_itv Itv.nat
 

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

@@ -13,6 +13,7 @@ codetoanalyze/cpp/bufferoverrun/repro1.cpp, ral_FP, 3, BUFFER_OVERRUN_S2, [Call,
 codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, instantiate_my_vector_oob_Ok, 3, BUFFER_OVERRUN_L1, [Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [42, 42] Size: [42, 42] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call `my_vector_oob_Bad()` ]
 codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN_L2, [Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [u$4, u$5] Size: [u$4, u$5] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call `int_vector_access_at()` ]
 codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [10, 10]]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_L1, [Call,Call,Assignment,Call,Call,ArrayDeclaration,Assignment,Assignment,Return,Assignment,Assignment,Return,Assignment,Assignment,ArrayAccess: Offset: [10, 10] Size: [5, 5]]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN_L5, [Call,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 18, BUFFER_OVERRUN_L3, [Call,Call,Call,Assignment,Call,Call,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [1, 1] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN_L2, [Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [u$12, u$13] Size: [u$12, u$13]]

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

@@ -143,3 +143,16 @@ void call_safe_access6_Good() {
   std::vector<int> v;
   safe_access6(v);
 }
+
+void data_Good() {
+  std::vector<int> v(5);
+  int* p = v.data();
+  p[4] = 1;
+}
+
+void data_Bad() {
+  std::vector<int> v(5);
+  int* p = v.data();
+  p[4] = 10;
+  p[v[4]] = 1;
+}