[inferbo] Add model of String::length

Reviewed By: mbouaziz

Differential Revision: D13547914

fbshipit-source-id: 7d496d11a

infer/src/IR/ProcnameDispatcher.ml

@@ -132,18 +132,21 @@ let name_cons :
     -> ('context, 'f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out) name_matcher =
  fun m name ->
   let {on_templated_name; get_markers} = m in
+  let match_fuzzy_name =
     let fuzzy_name_regexp =
-    name |> Str.quote |> Printf.sprintf "^%s\\(<[a-z0-9]+>\\)?$" |> Str.regexp
+      name |> Str.quote |> Printf.sprintf "^%s\\(<[a-z0-9_]+>\\)?$" |> Str.regexp
+    in
+    fun s -> Str.string_match fuzzy_name_regexp s 0
   in
   let on_qual_name context f qual_name =
     match QualifiedCppName.extract_last qual_name with
-    | Some (last, rest) when Str.string_match fuzzy_name_regexp last 0 ->
+    | Some (last, rest) when match_fuzzy_name last ->
         on_templated_name context f (rest, [])
     | _ ->
         None
   in
   let on_objc_cpp context f (objc_cpp : Typ.Procname.ObjC_Cpp.t) =
-    if String.equal name objc_cpp.method_name then
+    if match_fuzzy_name objc_cpp.method_name then
       on_templated_name context f (templated_name_of_class_name objc_cpp.class_name)
     else None
   in
@@ -865,7 +868,7 @@ module Call = struct
   let capt_exp_of_typ m = {one_arg_matcher= match_typ (m <...>! ()); capture= capture_arg_exp}
 
   let capt_exp_of_prim_typ typ =
-    let on_typ typ' = Typ.equal typ typ' in
+    let on_typ typ' = Typ.equal_ignore_quals typ typ' in
     {one_arg_matcher= match_prim_typ on_typ; capture= capture_arg_exp}
 
 

infer/src/IR/Typ.ml

@@ -135,6 +135,8 @@ type fkind =
   | FLongDouble  (** [long double] *)
 [@@deriving compare]
 
+let equal_fkind = [%compare.equal: fkind]
+
 let fkind_to_string = function
   | FFloat ->
       "float"
@@ -208,6 +210,23 @@ module T = struct
   let equal_quals = [%compare.equal: type_quals]
 
   let equal = [%compare.equal: t]
+
+  let rec equal_ignore_quals t1 t2 = equal_desc_ignore_quals t1.desc t2.desc
+
+  and equal_desc_ignore_quals d1 d2 =
+    match (d1, d2) with
+    | Tint ikind1, Tint ikind2 ->
+        equal_ikind ikind1 ikind2
+    | Tfloat fkind1, Tfloat fkind2 ->
+        equal_fkind fkind1 fkind2
+    | Tvoid, Tvoid ->
+        true
+    | Tptr (t1, ptr_kind1), Tptr (t2, ptr_kind2) ->
+        equal_ptr_kind ptr_kind1 ptr_kind2 && equal_ignore_quals t1 t2
+    | Tarray {elt= t1}, Tarray {elt= t2} ->
+        equal_ignore_quals t1 t2
+    | _, _ ->
+        false
 end
 
 include T

infer/src/IR/Typ.mli

@@ -250,6 +250,9 @@ val equal_desc : desc -> desc -> bool
 
 val equal_quals : type_quals -> type_quals -> bool
 
+val equal_ignore_quals : t -> t -> bool
+(** Equality for types, but ignoring quals in it. *)
+
 val pp_full : Pp.env -> F.formatter -> t -> unit
 (** Pretty print a type with all the details. *)
 

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -344,6 +344,21 @@ module StdBasicString = struct
     {exec; check}
 
 
+  (* The (5) constructor in https://en.cppreference.com/w/cpp/string/basic_string/basic_string *)
+  let constructor_from_char_ptr_without_len tgt src =
+    let exec {pname; node_hash; location; integer_type_widths} ~ret:_ mem =
+      match src with
+      | Exp.Const (Const.Cstr s) ->
+          let locs = Sem.eval_locs tgt mem in
+          BoUtils.Exec.decl_string pname ~node_hash integer_type_widths location locs s mem
+      | _ ->
+          let tgt_locs = Sem.eval_locs tgt mem in
+          let v = Sem.eval integer_type_widths src mem in
+          Dom.Mem.update_mem tgt_locs v mem
+    in
+    {exec; check= no_check}
+
+
   (* The (7) constructor in https://en.cppreference.com/w/cpp/string/basic_string/basic_string *)
   let copy_constructor tgt src =
     let exec _ ~ret:_ mem =
@@ -369,6 +384,15 @@ module StdBasicString = struct
           mem
     in
     {exec; check= no_check}
+
+
+  let length e =
+    let exec {integer_type_widths} ~ret:(ret_id, _) mem =
+      let v = Sem.eval_arr integer_type_widths e mem in
+      let length = Dom.Val.of_itv (ArrayBlk.sizeof (Dom.Val.get_array_blk v)) in
+      Dom.Mem.add_stack (Loc.of_id ret_id) length mem
+    in
+    {exec; check= no_check}
 end
 
 (* Java's Collections are represented like arrays. But we don't care about the elements.
@@ -545,11 +569,16 @@ module Call = struct
       ; -"std" &:: "basic_string" &:: "basic_string" $ capt_exp
         $+ capt_exp_of_typ (-"std" &:: "basic_string")
         $--> StdBasicString.copy_constructor
+      ; -"std" &:: "basic_string" &:: "basic_string" $ capt_exp
+        $+ capt_exp_of_prim_typ (Typ.mk (Typ.Tptr (Typ.mk (Typ.Tint Typ.IChar), Pk_pointer)))
+        $--> StdBasicString.constructor_from_char_ptr_without_len
       ; -"std" &:: "basic_string" &:: "basic_string" $ capt_exp
         $+ capt_exp_of_prim_typ (Typ.mk (Typ.Tptr (Typ.mk (Typ.Tint Typ.IChar), Pk_pointer)))
         $+ capt_exp_of_prim_typ (Typ.mk (Typ.Tint Typ.size_t))
         $--> StdBasicString.constructor_from_char_ptr
       ; -"std" &:: "basic_string" &:: "empty" $ capt_exp $--> StdBasicString.empty
+      ; -"std" &:: "basic_string" &:: "length" $ capt_exp $--> StdBasicString.length
+      ; -"std" &:: "basic_string" &:: "size" $ capt_exp $--> StdBasicString.length
       ; -"std" &:: "basic_string" &::.*--> no_model
       ; +PatternMatch.implements_collection
         &:: "get" <>$ capt_var_exn $+ capt_exp $--> Collection.get_or_set_at_index

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

@@ -75,12 +75,17 @@ codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int3_Bad, 3, INFERBO_ALLOC_IS
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int3_Bad, 3, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [<RHS trace>,Assignment,Binary operation: (4 × 18446744073709551615):unsigned64]
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, normal_array_bo, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 42 Size: 42]
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, std_array_bo_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 42 Size: 42]
+codetoanalyze/cpp/bufferoverrun/std_string.cpp, call_length4_1_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Length trace>,Array declaration,Array access: Offset: 11 Size: 10 by call to `length4` ]
 codetoanalyze/cpp/bufferoverrun/std_string.cpp, empty_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
 codetoanalyze/cpp/bufferoverrun/std_string.cpp, empty_Good, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/cpp/bufferoverrun/std_string.cpp, last_char1_Bad, 3, BUFFER_OVERRUN_R2, no_bucket, ERROR, [<Offset trace>,Risky value from: snprintf,Assignment,<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 1024]
 codetoanalyze/cpp/bufferoverrun/std_string.cpp, last_char1_Bad, 3, INTEGER_OVERFLOW_R2, no_bucket, ERROR, [<LHS trace>,Risky value from: snprintf,Assignment,Binary operation: ([-oo, +oo] - 1):signed32]
 codetoanalyze/cpp/bufferoverrun/std_string.cpp, last_char2_Bad, 6, BUFFER_OVERRUN_R2, no_bucket, ERROR, [<Offset trace>,Risky value from: vsnprintf,Assignment,<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 1024]
 codetoanalyze/cpp/bufferoverrun/std_string.cpp, last_char2_Bad, 6, INTEGER_OVERFLOW_R2, no_bucket, ERROR, [<LHS trace>,Risky value from: vsnprintf,Assignment,Binary operation: ([-oo, +oo] - 1):signed32]
+codetoanalyze/cpp/bufferoverrun/std_string.cpp, length2_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 11 Size: 10]
+codetoanalyze/cpp/bufferoverrun/std_string.cpp, length3_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 11 Size: 10]
+codetoanalyze/cpp/bufferoverrun/std_string.cpp, length_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 11 Size: 10]
+codetoanalyze/cpp/bufferoverrun/std_string.cpp, size_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 11 Size: 10]
 codetoanalyze/cpp/bufferoverrun/std_string.cpp, to_string1_Bad, 3, BUFFER_OVERRUN_R2, no_bucket, ERROR, [<Offset trace>,Risky value from: snprintf,Assignment,<Length trace>,Array declaration,Array access: Offset added: [-oo, +oo] Size: 1024]
 codetoanalyze/cpp/bufferoverrun/std_string.cpp, to_string2_Bad, 6, BUFFER_OVERRUN_R2, no_bucket, ERROR, [<Offset trace>,Risky value from: vsnprintf,Assignment,<Length trace>,Array declaration,Array access: Offset added: [-oo, +oo] Size: 1024]
 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]

infer/tests/codetoanalyze/cpp/bufferoverrun/std_string.cpp

@@ -86,3 +86,75 @@ void empty_Bad(std::string s) {
     a[10] = 0;
   }
 }
+
+void length_Good() {
+  std::string s("hello");
+  int a[10];
+  a[s.length()] = 0;
+}
+
+void length_Bad() {
+  std::string s("hellohello");
+  int a[10];
+  a[s.length()] = 0;
+}
+
+void length2_Good() {
+  const char* c = "hello";
+  std::string s(c);
+  int a[10];
+  a[s.length()] = 0;
+}
+
+void length2_Bad() {
+  const char* c = "hellohello";
+  std::string s(c);
+  int a[10];
+  a[s.length()] = 0;
+}
+
+void length3_Good() {
+  char* c = "hello";
+  std::string s(c);
+  int a[10];
+  a[s.length()] = 0;
+}
+
+void length3_Bad() {
+  char* c = "hellohello";
+  std::string s(c);
+  int a[10];
+  a[s.length()] = 0;
+}
+
+void length4(char* c) {
+  std::string s(c);
+  int a[10];
+  a[s.length()] = 0;
+}
+
+void call_length4_1_Good() {
+  char* c = "hello";
+  length4(c);
+}
+
+void call_length4_1_Bad() {
+  char* c = "hellohello";
+  length4(c);
+}
+
+void call_length4_2_Good() { length4("hello"); }
+
+void call_length4_2_Bad_FN() { length4("hellohello"); }
+
+void size_Good() {
+  std::string s("hello");
+  int a[10];
+  a[s.size()] = 0;
+}
+
+void size_Bad() {
+  std::string s("hellohello");
+  int a[10];
+  a[s.size()] = 0;
+}

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

@@ -25,11 +25,13 @@ codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_afte
 codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidated by call to `free(x)` at line 15 here,accessed `x` here]
 codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidated by call to `free(x)` at line 10 here,accessed `*(x)` here]
 codetoanalyze/cpp/pulse/vector.cpp, FP_init_fill_then_push_back_loop_ok, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(&(vec),(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::push_back(&(vec), ..)` at line 65 here,accessed `*(elt)` here]
-codetoanalyze/cpp/pulse/vector.cpp, VectorA_FP_push_back_value_field_ok, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 127 here,accessed `&(this->x)` here]
+codetoanalyze/cpp/pulse/vector.cpp, VectorA_FP_push_back_value_field_ok, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 125 here,accessed `&(this->x)` here]
 codetoanalyze/cpp/pulse/vector.cpp, assign_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::assign(vec, ..)` at line 84 here,accessed `*(elt)` here]
 codetoanalyze/cpp/pulse/vector.cpp, clear_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::clear(vec, ..)` at line 78 here,accessed `*(elt)` here]
 codetoanalyze/cpp/pulse/vector.cpp, deref_local_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(&(vec),(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::push_back(&(vec), ..)` at line 20 here,accessed `*(elt)` here]
 codetoanalyze/cpp/pulse/vector.cpp, deref_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,assigned to `y`,potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 13 here,accessed `*(y)` here]
+codetoanalyze/cpp/pulse/vector.cpp, emplace_back_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::emplace_back(vec, ..)` at line 108 here,accessed `*(elt)` here]
+codetoanalyze/cpp/pulse/vector.cpp, emplace_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::emplace(vec, ..)` at line 102 here,accessed `*(elt)` here]
 codetoanalyze/cpp/pulse/vector.cpp, insert_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::insert(vec, ..)` at line 96 here,accessed `*(elt)` here]
 codetoanalyze/cpp/pulse/vector.cpp, reserve_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::reserve(vec, ..)` at line 72 here,accessed `*(elt)` here]
 codetoanalyze/cpp/pulse/vector.cpp, shrink_to_fit_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::shrink_to_fit(vec, ..)` at line 90 here,accessed `*(elt)` here]

infer/tests/codetoanalyze/cpp/pulse/vector.cpp

@@ -97,17 +97,15 @@ void insert_bad(std::vector<int>& vec) {
   std::cout << *elt << "\n";
 }
 
-void FN_emplace_bad(std::vector<int>& vec) {
+void emplace_bad(std::vector<int>& vec) {
   int* elt = &vec[1];
-  vec.emplace(vec.begin(),
-              7); // procname matcher does not match emplace (T37883260)
+  vec.emplace(vec.begin(), 7);
   std::cout << *elt << "\n";
 }
 
-void FN_emplace_back_bad(std::vector<int>& vec) {
+void emplace_back_bad(std::vector<int>& vec) {
   int* elt = &vec[1];
-  vec.emplace_back(7); // procname matcher does not match emplace_back
-                       // (T37883260)
+  vec.emplace_back(7);
   std::cout << *elt << "\n";
 }