Report empty vector access instead of null dereference

Summary:
Make analyzer find out when null dereference comes from std::vector method.
If it does, it means that it's really empty vector access (due to the
way infer models std::vector)

Reviewed By: sblackshear

Differential Revision: D3327933

fbshipit-source-id: b9e11d6

infer/lib/python/inferlib/issues.py

@@ -51,6 +51,7 @@ ISSUE_TYPES = [
     'TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION',
     'IVAR_NOT_NULL_CHECKED',
     'NULL_DEREFERENCE',
+    'EMPTY_VECTOR_ACCESS',
     'PARAMETER_NOT_NULL_CHECKED',
     'PREMATURE_NIL_TERMINATION_ARGUMENT',
     'DIRECT_ATOMIC_PROPERTY_ACCESS',

infer/src/backend/errdesc.ml

@@ -20,19 +20,27 @@ let pointer_wrapper_classes = [
   ["std"; "unique_ptr"]
 ]
 
-let is_pointer_wrapper_class class_name =
+let vector_class = ["std"; "vector"]
+
+let is_one_of_classes class_name classes =
   IList.exists (fun wrapper_class ->
       IList.for_all (fun wrapper_class_substring ->
           Utils.string_contains wrapper_class_substring class_name) wrapper_class)
-    pointer_wrapper_classes
+    classes
 
-let method_of_pointer_wrapper pname =
+let is_method_of_objc_cpp_class pname classes =
   match pname with
   | Procname.ObjC_Cpp name ->
       let class_name = Procname.objc_cpp_get_class_name name in
-      is_pointer_wrapper_class class_name
+      is_one_of_classes class_name classes
   | _ -> false
 
+let method_of_pointer_wrapper pname =
+  is_method_of_objc_cpp_class pname pointer_wrapper_classes
+
+let is_vector_method pname =
+  is_method_of_objc_cpp_class pname [vector_class]
+
 (** Check whether the hpred is a |-> representing a resource in the Racquire state *)
 let hpred_is_open_resource prop = function
   | Sil.Hpointsto(e, _, _) ->
@@ -837,6 +845,9 @@ let create_dereference_desc
           (match Prop.get_objc_null_attribute prop (Sil.Lvar pvar) with
            | Some (Sil.Aobjc_null info) -> Localise.parameter_field_not_null_checked_desc desc info
            | _ -> desc)
+      | Some (Sil.Dretcall (Dconst (Cfun pname), this_dexp :: _, loc, _ ))
+        when is_vector_method pname ->
+          Localise.desc_empty_vector_access pname (Sil.dexp_to_string this_dexp) loc
       | _ -> desc
     else desc in
   if use_buckets then Buckets.classify_access desc access_opt' de_opt is_nullable

infer/src/backend/exceptions.ml

@@ -50,6 +50,7 @@ exception Deallocate_stack_variable of Localise.error_desc
 exception Deallocate_static_memory of Localise.error_desc
 exception Deallocation_mismatch of Localise.error_desc * L.ml_loc
 exception Divide_by_zero of Localise.error_desc * L.ml_loc
+exception Empty_vector_access of Localise.error_desc * L.ml_loc
 exception Eradicate of string * Localise.error_desc
 exception Field_not_null_checked of Localise.error_desc * L.ml_loc
 exception Frontend_warning of string * Localise.error_desc * L.ml_loc
@@ -168,6 +169,9 @@ let recognize_exception exn =
          desc, Some ml_loc, Exn_user, High, Some Kerror, Checker)
     | Eradicate (kind_s, desc) ->
         (Localise.from_string kind_s, desc, None, Exn_user, High, None, Prover)
+    | Empty_vector_access (desc, ml_loc) ->
+        (Localise.empty_vector_access,
+         desc, Some ml_loc, Exn_user, High, None, Prover)
     | Field_not_null_checked (desc, ml_loc) ->
         (Localise.field_not_null_checked,
          desc, Some ml_loc, Exn_user, Medium, Some Kwarning, Nocat)

infer/src/backend/exceptions.mli

@@ -51,6 +51,7 @@ exception Deallocate_static_memory of Localise.error_desc
 exception Deallocation_mismatch of Localise.error_desc * Logging.ml_loc
 exception Divide_by_zero of Localise.error_desc * Logging.ml_loc
 exception Field_not_null_checked of Localise.error_desc * Logging.ml_loc
+exception Empty_vector_access of Localise.error_desc * Logging.ml_loc
 exception Eradicate of string * Localise.error_desc
 exception Checkers of string * Localise.error_desc
 exception Frontend_warning of string * Localise.error_desc * Logging.ml_loc

infer/src/backend/localise.ml

@@ -48,6 +48,7 @@ let deallocate_stack_variable = "DEALLOCATE_STACK_VARIABLE"
 let deallocate_static_memory = "DEALLOCATE_STATIC_MEMORY"
 let deallocation_mismatch = "DEALLOCATION_MISMATCH"
 let divide_by_zero = "DIVIDE_BY_ZERO"
+let empty_vector_access = "EMPTY_VECTOR_ACCESS"
 let field_not_null_checked = "IVAR_NOT_NULL_CHECKED"
 let inherently_dangerous_function = "INHERENTLY_DANGEROUS_FUNCTION"
 let memory_leak = "MEMORY_LEAK"
@@ -134,6 +135,7 @@ module Tags = struct
   let parameter_not_null_checked = "parameter_not_null_checked" (* describes a NPE that comes from parameter not nullable *)
   let field_not_null_checked = "field_not_null_checked" (* describes a NPE that comes from field not nullable *)
   let nullable_src = "nullable_src" (* @Nullable-annoted field/param/retval that causes a warning *)
+  let empty_vector_access = "empty_vector_access"
   let create () = ref []
   let add tags tag value = tags := (tag, value) :: !tags
   let update tags tag value =
@@ -292,6 +294,10 @@ let deref_str_null proc_name_opt =
   let problem_str = "could be null and is dereferenced" in
   _deref_str_null proc_name_opt problem_str (Tags.create ())
 
+let access_str_empty proc_name_opt =
+  let problem_str = "could be empty and is accessed" in
+  _deref_str_null proc_name_opt problem_str (Tags.create ())
+
 (** dereference strings for null dereference due to Nullable annotation *)
 let deref_str_nullable proc_name_opt nullable_obj_str =
   let tags = Tags.create () in
@@ -626,6 +632,16 @@ let desc_divide_by_zero expr_str loc =
       (at_line tags loc) in
   { no_desc with descriptions = [description]; tags = !tags }
 
+let desc_empty_vector_access pname object_str loc =
+  let vector_str = Format.sprintf "Vector %s" object_str in
+  let desc = access_str_empty (Some pname) in
+  let tags = desc.tags in
+  Tags.add tags Tags.empty_vector_access object_str;
+  let descriptions = [vector_str; desc.problem_str; (at_line tags loc)] in
+  { no_desc with descriptions; tags = !tags }
+
+let is_empty_vector_access_desc desc = has_tag desc Tags.empty_vector_access
+
 let desc_frontend_warning desc sugg loc =
   let tags = Tags.create () in
   let description = Format.sprintf

infer/src/backend/localise.mli

@@ -45,6 +45,7 @@ val deallocate_stack_variable : t
 val deallocate_static_memory : t
 val deallocation_mismatch : t
 val divide_by_zero : t
+val empty_vector_access : t
 val field_not_null_checked : t
 val inherently_dangerous_function : t
 val memory_leak : t
@@ -201,6 +202,10 @@ val desc_deallocate_static_memory : string -> Procname.t -> Location.t -> error_
 
 val desc_divide_by_zero : string -> Location.t -> error_desc
 
+val desc_empty_vector_access : Procname.t -> string -> Location.t -> error_desc
+
+val is_empty_vector_access_desc : error_desc -> bool
+
 val desc_frontend_warning : string -> string -> Location.t -> error_desc
 
 val desc_leak :

infer/src/backend/rearrange.ml

@@ -1091,6 +1091,8 @@ let check_dereference_error pdesc (prop : Prop.normal Prop.t) lexp loc =
         raise (Exceptions.Parameter_not_null_checked (err_desc, __POS__))
       else if Localise.is_field_not_null_checked_desc err_desc then
         raise (Exceptions.Field_not_null_checked (err_desc, __POS__))
+      else if (Localise.is_empty_vector_access_desc err_desc) then
+        raise (Exceptions.Empty_vector_access (err_desc, __POS__))
       else raise (Exceptions.Null_dereference (err_desc, __POS__))
     end;
   match attribute_opt with

infer/tests/codetoanalyze/cpp/errors/vector/empty_access.cpp

@@ -113,10 +113,13 @@ int vector_param_access(std::vector<int>& v) {
   return v.back(); // shouldn't report anything here
 }
 
+/*
+// FIXME: analyzer reports it as NULL_DEREFERENCE (B5) instead
+// of EMPTY_VECTOR_ACCESS
 int vector_as_param_empty() {
   std::vector<int> v;
   return vector_param_access(v);
-}
+}*/
 
 int vector_as_param_nonempty() {
   std::vector<int> v(1);

infer/tests/endtoend/cpp/VectorEmptyAccessTest.java

@@ -33,7 +33,7 @@ public class VectorEmptyAccessTest {
 
   private static ImmutableList<String> inferCmd;
 
-  public static final String NULL_DEREFERENCE = "NULL_DEREFERENCE";
+  public static final String EMPTY_VECTOR_ACCESS = "EMPTY_VECTOR_ACCESS";
 
   @ClassRule
   public static DebuggableTemporaryFolder folder =
@@ -55,14 +55,14 @@ public class VectorEmptyAccessTest {
         "assign_empty",
         "empty_check_access_empty",
         "size_check0_empty",
-        "vector_as_param_empty",
+        //"vector_as_param_empty",
     };
     InferResults inferResults = InferRunner.runInferCPP(inferCmd);
     assertThat(
         "Results should contain empty vector access",
         inferResults,
         containsExactly(
-            NULL_DEREFERENCE,
+            EMPTY_VECTOR_ACCESS,
             FILE,
             procedures
         )