[inferbo] Add model: vector constructor

Summary: It adds vector model of constructor.

Reviewed By: ezgicicek

Differential Revision: D16645564

fbshipit-source-id: 92241a068

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -643,6 +643,53 @@ module StdBasicString = struct
     {exec; check= no_check}
 end
 
+module StdVector = struct
+  (* The (3) constructor in https://en.cppreference.com/w/cpp/container/vector/vector *)
+  let constructor vec_exp 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 deref_of_vec =
+        Allocsite.make pname ~node_hash ~inst_num:1 ~dimension:1 ~path:None
+          ~represents_multiple_values:false
+        |> Loc.of_allocsite
+      in
+      let array_v =
+        Sem.eval integer_type_widths (Exp.Var id) mem
+        |> Dom.Val.add_assign_trace_elem location vec_locs
+      in
+      mem
+      |> Dom.Mem.update_mem vec_locs (Dom.Val.of_loc deref_of_vec)
+      |> Dom.Mem.add_heap deref_of_vec array_v
+    in
+    {exec; 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
+      let array_v =
+        let locs = Dom.Val.get_all_locs deref_of_vec in
+        if PowLoc.is_bot locs then Dom.Val.unknown_from ~callee_pname:(Some pname) ~location
+        else Dom.Mem.find_set locs mem
+      in
+      Dom.Mem.add_stack (Loc.of_id id) array_v mem
+    and check {location; integer_type_widths} mem cond_set =
+      let idx = Sem.eval integer_type_widths index_exp mem in
+      let arr =
+        let deref_of_vec = Dom.Mem.find_set (Sem.eval_locs vec_exp mem) mem in
+        Dom.Mem.find_set (Dom.Val.get_all_locs deref_of_vec) mem
+      in
+      let relation = Dom.Mem.get_relation mem in
+      let latest_prune = Dom.Mem.get_latest_prune mem in
+      BoUtils.Check.array_access ~arr ~idx ~idx_sym_exp:None ~relation ~is_plus:true
+        ~last_included:false ~latest_prune location cond_set
+    in
+    {exec; check}
+end
+
 (* Java's Collections are represented like arrays. But 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
@@ -956,6 +1003,10 @@ 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
+        $--> StdVector.constructor
+      ; -"std" &:: "vector" < any_typ &+ any_typ >:: "operator[]" $ capt_exp $+ capt_exp
+        $--> StdVector.at
       ; +PatternMatch.implements_collection
         &:: "<init>" <>$ capt_var_exn $+ capt_exp $--> Collection.init
         (* model sets as lists *)

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

@@ -107,19 +107,16 @@ codetoanalyze/cpp/bufferoverrun/this.cpp, CThis::access_Bad, 2, BUFFER_OVERRUN_L
 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_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_constructor_Good, 2, 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_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_access, 2, 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, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Unknown value from: std::vector<int,std::allocator<int>>::size,Binary operation: ([0, +oo] + 1):unsigned32]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_safe_access2, 7, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Offset trace>,Unknown value from: std::vector<int,std::allocator<int>>::size,<Length trace>,Unknown value from: std::vector<int,std::allocator<int>>::size,Array declaration,Array access: Offset: [0, +oo] Size: [0, +oo]]
 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_access4, 2, 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_access5, 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, data_Bad, 4, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Offset trace>,Unknown value from: std::vector<int,std::allocator<int>>::operator[],<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_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, 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/vector.cpp

@@ -8,16 +8,21 @@
 #include <list>
 #include <assert.h>
 
-void out_of_bound_Bad(std::vector<int> v) {
+void FN_out_of_bound_Bad(std::vector<int> v) {
   unsigned int n = v.size();
   v[n] = 1;
 }
 
-void FP_constructor_Good() {
+void constructor_Good() {
   std::vector<int> v(1);
   v[0] = 2;
 }
 
+void constructor_Bad() {
+  std::vector<int> v(1);
+  v[3] = 2;
+}
+
 void FP_push_back_Good() {
   std::vector<int> v;
   v.push_back(1);
@@ -43,7 +48,7 @@ void reserve_Bad() {
   v[0] = 2;
 }
 
-void FP_safe_access(std::vector<int> v) {
+void safe_access(std::vector<int> v) {
   if (v.size() >= 10) {
     v[9] = 1;
   }
@@ -51,7 +56,7 @@ void FP_safe_access(std::vector<int> v) {
 
 void call_safe_access_Good() {
   std::vector<int> v(5, 0);
-  FP_safe_access(v);
+  safe_access(v);
 }
 
 void FP_safe_access2(std::vector<int> v) {
@@ -77,7 +82,7 @@ void FP_safe_access3_Good() {
   }
 }
 
-void FP_safe_access4(std::vector<int> v) {
+void safe_access4(std::vector<int> v) {
   if (!v.empty()) {
     v[0] = 1;
   }
@@ -85,10 +90,10 @@ void FP_safe_access4(std::vector<int> v) {
 
 void call_safe_access4_Good() {
   std::vector<int> v;
-  FP_safe_access4(v);
+  safe_access4(v);
 }
 
-void FP_safe_access5(std::vector<int> v) {
+void safe_access5(std::vector<int> v) {
   if (v.empty()) {
   } else {
     v[0] = 1;
@@ -97,17 +102,17 @@ void FP_safe_access5(std::vector<int> v) {
 
 void call_safe_access5_Good() {
   std::vector<int> v;
-  FP_safe_access5(v);
+  safe_access5(v);
 }
 
-void safe_access6(std::vector<int> v) {
+void FP_safe_access6(std::vector<int> v) {
   std::vector<int> v2(2);
   v2[v.empty()];
 }
 
 void call_safe_access6_Good() {
   std::vector<int> v;
-  safe_access6(v);
+  FP_safe_access6(v);
 }
 
 void FP_data_Good() {