[inferbo] Evaluate cpp vector parameter symbolically

Summary:
This diff evaluates a cpp vector given as a parameter symbolically. Especially, it addresses it as an array, so the cost checker can use its symbolic length correctly.

**About handling `cpp.vector_elem` field:**

The field is a virtual field of vector object that points to the array of vector elements. It was introduced in Inferbo to model semantics of vector operations.
Since many semantics of Inferbo depends on type information, it had collected type information of vector elements, whenever `cpp.vector_elem` field was introduced, as a *side-effect*. A problem is that it has *side-effect*, which means it may introduce non-deterministic analysis results depending on the type information of the virtual field.

This diff changes it not to collect the type information on `cpp.vector_elem` as a side-effect. Instead, it tries to write the information to the abstract states (abstract location) when possible.

Reviewed By: ezgicicek

Differential Revision: D27674935

fbshipit-source-id: f3d52cae7

infer/src/bufferoverrun/absLoc.ml

@@ -568,7 +568,7 @@ module PowLoc = struct
         mk_known (LocSet.fold (fun l -> LocSet.add (Loc.get_parent_field l)) ploc LocSet.empty)
 
 
-  let append_field ploc ~fn =
+  let append_field ?typ ploc ~fn =
     match ploc with
     | Bottom ->
         (* Return the unknown location to avoid unintended unreachable nodes *)
@@ -576,7 +576,7 @@ module PowLoc = struct
     | Unknown ->
         Unknown
     | Known ploc ->
-        mk_known (LocSet.fold (fun l -> LocSet.add (Loc.append_field l fn)) ploc LocSet.empty)
+        mk_known (LocSet.fold (fun l -> LocSet.add (Loc.append_field ?typ l fn)) ploc LocSet.empty)
 
 
   let append_star_field ploc ~fn =

infer/src/bufferoverrun/absLoc.mli

@@ -111,7 +111,7 @@ module PowLoc : sig
 
   val get_parent_field : t -> t
 
-  val append_field : t -> fn:Fieldname.t -> t
+  val append_field : ?typ:Typ.t -> t -> fn:Fieldname.t -> t
 
   val append_star_field : t -> fn:Fieldname.t -> t
 

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -549,10 +549,37 @@ module Val = struct
       let traces = traces_of_loc (Loc.of_path deref_path) in
       of_c_array_alloc allocsite ~stride:None ~offset ~size ~traces
     in
+    let ptr_to_normal_c_array elt =
+      let deref_kind = SPath.Deref_CPointer in
+      let deref_path = SPath.deref ~deref_kind path in
+      let l = Loc.of_path deref_path in
+      let traces = traces_of_loc l in
+      let arrayblk =
+        let allocsite = Allocsite.make_symbol deref_path in
+        let stride =
+          match elt with
+          | Some {Typ.desc= Tint ikind} ->
+              Itv.of_int (Typ.width_of_ikind integer_type_widths ikind)
+          | _ ->
+              Itv.nat
+        in
+        let is_void = Typ.is_pointer_to_void typ in
+        let offset =
+          if SPath.is_cpp_vector_elem path then Itv.zero else Itv.of_offset_path ~is_void path
+        in
+        let size = Itv.of_length_path ~is_void path in
+        ArrayBlk.make_c allocsite ~stride ~offset ~size
+      in
+      {bot with arrayblk; traces}
+    in
     let is_java = Language.curr_language_is Java in
     L.d_printfln_escaped "Val.of_path %a : %a%s%s" SPath.pp_partial path (Typ.pp Pp.text) typ
       (if may_last_field then ", may_last_field" else "")
       (if is_java then ", is_java" else "") ;
+    match path with
+    | BoField.Field {fn; typ} when BufferOverrunField.is_cpp_vector_elem fn ->
+        ptr_to_normal_c_array typ
+    | _ -> (
       match typ.Typ.desc with
       | Tint (IBool | IChar | ISChar | IUChar | IUShort) ->
           let v = itv_val ~non_int:is_java in
@@ -581,28 +608,7 @@ module Val = struct
             let l = Loc.of_path deref_path in
             let traces = traces_of_loc l in
             {bot with powloc= PowLoc.singleton l; traces}
-        else
-          let deref_kind = SPath.Deref_CPointer in
-          let deref_path = SPath.deref ~deref_kind path in
-          let l = Loc.of_path deref_path in
-          let traces = traces_of_loc l in
-          let arrayblk =
-            let allocsite = Allocsite.make_symbol deref_path in
-            let stride =
-              match elt.Typ.desc with
-              | Typ.Tint ikind ->
-                  Itv.of_int (Typ.width_of_ikind integer_type_widths ikind)
-              | _ ->
-                  Itv.nat
-            in
-            let offset =
-              if SPath.is_cpp_vector_elem path then Itv.zero
-              else Itv.of_offset_path ~is_void:(Typ.is_pointer_to_void typ) path
-            in
-            let size = Itv.of_length_path ~is_void:(Typ.is_pointer_to_void typ) path in
-            ArrayBlk.make_c allocsite ~stride ~offset ~size
-          in
-          {bot with arrayblk; traces}
+          else ptr_to_normal_c_array (Some elt)
       | Tstruct typename -> (
         match BufferOverrunTypModels.dispatch tenv typename with
         | Some (CArray {deref_kind; length}) ->
@@ -646,7 +652,7 @@ module Val = struct
           else
             let stride = Option.map stride ~f:(fun n -> IntLit.to_int_exn n) in
             let offset = Itv.zero in
-          of_c_array_alloc allocsite ~stride ~offset ~size ~traces
+            of_c_array_alloc allocsite ~stride ~offset ~size ~traces )
 
 
   let on_demand : default:t -> ?typ:Typ.t -> OndemandEnv.t -> Loc.t -> t =

infer/src/bufferoverrun/bufferOverrunField.ml

@@ -13,14 +13,10 @@ let pp ~pp_lhs ~sep f lhs fn = F.fprintf f "%a%s%s" pp_lhs lhs sep (Fieldname.ge
 let mk, get_type =
   let class_name = "__infer__" in
   let types = ref Fieldname.Map.empty in
-  let mk ?cpp_classname name typ =
+  let mk name typ =
     let fieldname =
-      match cpp_classname with
-      | None ->
       let class_name, field_name = String.rsplit2_exn ~on:'.' (class_name ^ "." ^ name) in
       Fieldname.make (Typ.Name.Java.from_string class_name) field_name
-      | Some classname ->
-          Fieldname.make classname name
     in
     types := Fieldname.Map.add fieldname typ !types ;
     fieldname
@@ -51,7 +47,7 @@ let c_strlen () =
 
 let cpp_vector_elem_str = "cpp.vector_elem"
 
-let cpp_vector_elem ~vec_typ ~elt_typ =
+let cpp_vector_elem ~vec_typ =
   let classname =
     match vec_typ.Typ.desc with
     | Typ.Tptr (vec_typ, _) -> (
@@ -63,8 +59,8 @@ let cpp_vector_elem ~vec_typ ~elt_typ =
     | _ ->
         L.(die InternalError) "First parameter of constructor should be a pointer."
   in
-  let desc = Typ.Tptr (elt_typ, Typ.Pk_pointer) in
-  mk ~cpp_classname:classname cpp_vector_elem_str {Typ.desc; quals= Typ.mk_type_quals ()}
+  (* Note: Avoid calling [mk] that has side-effects introducing non-deterministic results *)
+  Fieldname.make classname cpp_vector_elem_str
 
 
 let is_cpp_vector_elem fn = String.equal (Fieldname.to_simplified_string fn) cpp_vector_elem_str

infer/src/bufferoverrun/bufferOverrunField.mli

@@ -23,7 +23,7 @@ val get_type : Fieldname.t -> Typ.t option
 val c_strlen : unit -> Fieldname.t
 (** Field for C string's length *)
 
-val cpp_vector_elem : vec_typ:Typ.t -> elt_typ:Typ.t -> Fieldname.t
+val cpp_vector_elem : vec_typ:Typ.t -> Fieldname.t
 (** Field for C++ vector's elements *)
 
 val java_collection_internal_array : Fieldname.t

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -479,29 +479,30 @@ module StdArray = struct
 end
 
 module ArrObjCommon = struct
-  let deref_of {integer_type_widths} exp ~fn mem =
-    Dom.Val.get_all_locs (Sem.eval_arr integer_type_widths exp mem) |> PowLoc.append_field ~fn
+  let deref_of {integer_type_widths} exp ~fn ?fn_typ mem =
+    let typ = Option.map fn_typ ~f:Typ.mk_ptr in
+    Dom.Val.get_all_locs (Sem.eval_arr integer_type_widths exp mem) |> PowLoc.append_field ?typ ~fn
 
 
   let eval_size model_env exp ~fn mem =
     Sem.eval_array_locs_length (deref_of model_env exp ~fn mem) mem
 
 
-  let size_exec exp ~fn ({integer_type_widths} as model_env) ~ret:(id, _) mem =
+  let size_exec exp ~fn ?fn_typ ({integer_type_widths} as model_env) ~ret:(id, _) mem =
     let locs = Sem.eval integer_type_widths exp mem |> Dom.Val.get_all_locs in
     match PowLoc.is_singleton_or_more locs with
     | Singleton (BoField.Prim (Loc.Allocsite (Allocsite.LiteralString s))) ->
         model_by_value (Dom.Val.of_int (String.length s)) id mem
     | _ ->
-        let arr_locs = deref_of model_env exp ~fn mem in
+        let arr_locs = deref_of model_env exp ~fn ?fn_typ mem in
         let mem = Dom.Mem.add_stack (Loc.of_id id) (Sem.eval_array_locs_length arr_locs mem) mem in
         load_size_alias id arr_locs mem
 
 
-  let at arr_exp ~fn index_exp =
+  let at arr_exp ~fn ?fn_typ index_exp =
     let exec ({pname; location} as model_env) ~ret:(id, typ) mem =
       let array_v =
-        let locs = deref_of model_env arr_exp ~fn mem in
+        let locs = deref_of model_env arr_exp ~fn ?fn_typ mem in
         if PowLoc.is_bot locs then Dom.Val.unknown_from typ ~callee_pname:(Some pname) ~location
         else Dom.Mem.find_set locs mem
       in
@@ -516,13 +517,14 @@ module ArrObjCommon = struct
     {exec; check}
 
 
-  let copy_constructor model_env deref_of_tgt ~fn src_exp mem =
-    let deref_of_src = deref_of model_env src_exp ~fn mem in
+  let copy_constructor model_env deref_of_tgt ~fn ?fn_typ src_exp mem =
+    let deref_of_src = deref_of model_env src_exp ~fn ?fn_typ mem in
     Dom.Mem.update_mem deref_of_tgt (Dom.Mem.find_set deref_of_src mem) mem
 
 
-  let constructor_from_char_ptr ({integer_type_widths} as model_env) tgt_deref ~fn src mem =
-    let elem_locs = PowLoc.append_field tgt_deref ~fn in
+  let constructor_from_char_ptr ({integer_type_widths} as model_env) tgt_deref ~fn ?char_typ src mem
+      =
+    let elem_locs = PowLoc.append_field ?typ:(Option.map char_typ ~f:Typ.mk_ptr) tgt_deref ~fn in
     match src with
     | Exp.Const (Const.Cstr s) ->
         BoUtils.Exec.decl_string model_env ~do_alloc:true elem_locs s mem
@@ -545,16 +547,17 @@ end
 
 module StdVector = struct
   let append_field loc ~vec_typ ~elt_typ =
-    Loc.append_field loc (BufferOverrunField.cpp_vector_elem ~vec_typ ~elt_typ)
+    Loc.append_field ~typ:(Typ.mk_ptr elt_typ) loc (BufferOverrunField.cpp_vector_elem ~vec_typ)
 
 
   let append_fields locs ~vec_typ ~elt_typ =
-    PowLoc.append_field locs ~fn:(BufferOverrunField.cpp_vector_elem ~vec_typ ~elt_typ)
+    PowLoc.append_field ~typ:(Typ.mk_ptr elt_typ) locs
+      ~fn:(BufferOverrunField.cpp_vector_elem ~vec_typ)
 
 
   let deref_of model_env elt_typ {exp= vec_exp; typ= vec_typ} mem =
-    let fn = BufferOverrunField.cpp_vector_elem ~vec_typ ~elt_typ in
-    ArrObjCommon.deref_of model_env vec_exp ~fn mem
+    let fn = BufferOverrunField.cpp_vector_elem ~vec_typ in
+    ArrObjCommon.deref_of model_env vec_exp ~fn ~fn_typ:(Typ.mk_ptr elt_typ) mem
 
 
   (* The (3) constructor in https://en.cppreference.com/w/cpp/container/vector/vector *)
@@ -591,16 +594,19 @@ module StdVector = struct
         (Dom.Val.get_all_locs v, Dom.Val.get_traces v)
       in
       let deref_of_vec = append_fields vec_locs ~vec_typ ~elt_typ in
-      let fn = BufferOverrunField.cpp_vector_elem ~vec_typ ~elt_typ in
+      let fn = BufferOverrunField.cpp_vector_elem ~vec_typ in
       mem
       |> Dom.Mem.update_mem vec_locs (Dom.Val.of_pow_loc ~traces deref_of_vec)
-      |> ArrObjCommon.copy_constructor model_env deref_of_vec ~fn src_exp
+      |> ArrObjCommon.copy_constructor model_env deref_of_vec ~fn ~fn_typ:(Typ.mk_ptr elt_typ)
+           src_exp
     in
     {exec; check= no_check}
 
 
   let at elt_typ {exp= vec_exp; typ= vec_typ} index_exp =
-    ArrObjCommon.at vec_exp ~fn:(BufferOverrunField.cpp_vector_elem ~vec_typ ~elt_typ) index_exp
+    ArrObjCommon.at vec_exp
+      ~fn:(BufferOverrunField.cpp_vector_elem ~vec_typ)
+      ~fn_typ:(Typ.mk_ptr elt_typ) index_exp
 
 
   let set_size {location} locs new_size mem =
@@ -651,7 +657,9 @@ module StdVector = struct
 
   let size elt_typ {exp= vec_exp; typ= vec_typ} =
     let exec =
-      ArrObjCommon.size_exec vec_exp ~fn:(BufferOverrunField.cpp_vector_elem ~vec_typ ~elt_typ)
+      ArrObjCommon.size_exec vec_exp
+        ~fn:(BufferOverrunField.cpp_vector_elem ~vec_typ)
+        ~fn_typ:(Typ.mk_ptr elt_typ)
     in
     {exec; check= no_check}
 
@@ -728,8 +736,8 @@ module StdBasicString = struct
       let mem =
         Dom.Mem.update_mem tgt_locs (Dom.Val.of_pow_loc ~traces:Trace.Set.bottom tgt_deref) mem
       in
-      let fn = BufferOverrunField.cpp_vector_elem ~vec_typ:tgt_typ ~elt_typ:char_typ in
-      ArrObjCommon.constructor_from_char_ptr model_env tgt_deref src ~fn mem
+      let fn = BufferOverrunField.cpp_vector_elem ~vec_typ:tgt_typ in
+      ArrObjCommon.constructor_from_char_ptr model_env tgt_deref src ~fn ~char_typ mem
     in
     let check ({location; integer_type_widths} as model_env) mem cond_set =
       Option.value_map len_opt ~default:cond_set ~f:(fun len ->
@@ -1324,7 +1332,7 @@ module JavaString = struct
     {exec; check= no_check}
 
 
-  let length exp = {exec= ArrObjCommon.size_exec exp ~fn; check= no_check}
+  let length exp = {exec= ArrObjCommon.size_exec exp ~fn ?fn_typ:None; check= no_check}
 
   (** Given a string of length n, return itv [-1, n_u-1]. *)
   let range_itv_mone model_env exp mem =

infer/tests/codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp

@@ -7,7 +7,7 @@
 #include <vector>
 
 namespace CppIsTricky {
-void FN_vector_size_Bad() {
+void vector_size_Bad() {
   const auto vec = std::vector<int>{1, 2, 3};
   const int numExpectedElements = 1;
   const auto delta = numExpectedElements - vec.size();

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

@@ -44,6 +44,7 @@ codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_condition
 codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_minus_2_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,<LHS trace>,Parameter `size`,Binary operation: (0 - 1):unsigned32 by call to `conditional_minus` ]
 codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_throw_exception_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `i`,<Length trace>,Array declaration,Array access: Offset: -5 Size: 10 by call to `throw_exception` ]
 codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, throw_exception, 3, UNREACHABLE_CODE, no_bucket, ERROR, [Here]
+codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp, CppIsTricky::vector_size_Bad, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: (1 - [0, +oo]):unsigned64]
 codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 5, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Length trace>,Unknown value from: lib,Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 10, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 30 Size: 10]
 codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, BUFFER_OVERRUN_L4, no_bucket, ERROR, [<Length trace>,Set array size,Array access: Offset: 0 Size: [0, +oo]]

infer/tests/codetoanalyze/cpp/performance/cost-issues.exp

@@ -1,2 +1,5 @@
+../../facebook-clang-plugins/clang/install/include/c++/v1/string, std::operator!=<b7ca98c5140c72c>, 37 + 12 ⋅ __lhs->cpp.vector_elem.length.ub(u) + (__lhs->cpp.vector_elem.length.ub(u) + 1),  OnUIThread:false, [{__lhs->cpp.vector_elem.length.ub(u) + 1},Call to std::operator==<std::allocator<char>_>,Loop,{__lhs->cpp.vector_elem.length.ub(u)},Call to std::operator==<std::allocator<char>_>,Loop]
+../../facebook-clang-plugins/clang/install/include/c++/v1/string, std::operator==<std::allocator<char>_>, 31 + 12 ⋅ __lhs->cpp.vector_elem.length.ub(u) + (__lhs->cpp.vector_elem.length.ub(u) + 1),  OnUIThread:false, [{__lhs->cpp.vector_elem.length.ub(u) + 1},Loop,{__lhs->cpp.vector_elem.length.ub(u)},Loop]
 codetoanalyze/cpp/performance/string_test.cpp, call_google_strlen_linear, 2 + str->strlen.ub(u),  OnUIThread:false, [{str->strlen.ub(u)},Modeled call to google::StrLen]
 codetoanalyze/cpp/performance/string_test.cpp, call_google_strlen_with_loop_linear, 4 + 3 ⋅ str->strlen.ub(u) + str->strlen.ub(u) + 2 ⋅ (str->strlen.ub(u) + 1),  OnUIThread:false, [{str->strlen.ub(u) + 1},Loop,{str->strlen.ub(u)},Modeled call to google::StrLen,{str->strlen.ub(u)},Loop]
+codetoanalyze/cpp/performance/string_test.cpp, string_compare_linear, 45 + 12 ⋅ a->cpp.vector_elem.length.ub(u) + (a->cpp.vector_elem.length.ub(u) + 1),  OnUIThread:false, [{a->cpp.vector_elem.length.ub(u) + 1},Call to std::operator!=<b7ca98c5140c72c>,Call to std::operator==<std::allocator<char>_>,Loop,{a->cpp.vector_elem.length.ub(u)},Call to std::operator!=<b7ca98c5140c72c>,Call to std::operator==<std::allocator<char>_>,Loop]

infer/tests/codetoanalyze/cpp/performance/string_test.cpp

@@ -5,6 +5,8 @@
  * LICENSE file in the root directory of this source tree.
  */
 
+#include <string>
+
 namespace google {
 int StrLen(char*);
 }
@@ -16,3 +18,10 @@ void call_google_strlen_with_loop_linear(char* str) {
   for (int i = 0; i < len; i++) {
   }
 }
+
+void string_compare_linear(const std::string& a, const std::string& b) {
+  if (a != b) {
+    return 0;
+  }
+  return 1;
+}