[pulse] Model `StdVector` allocator

Summary:
We ignored allocator models for vectors, and were not able to initialize vectors properly. This diff fixes this issue.

It also adds a test which was a FN before.

Reviewed By: skcho, jvillard

Differential Revision: D21089492

fbshipit-source-id: 6906cd1d1

infer/src/IR/ProcnameDispatcher.ml

@@ -729,6 +729,10 @@ module Call = struct
 
   let capt_arg_of_typ m = {one_arg_matcher= match_typ (m <...>! ()); capture= capture_arg}
 
+  let capt_arg_payload_of_typ m =
+    {one_arg_matcher= match_typ (m <...>! ()); capture= capture_arg_val}
+
+
   let capt_exp_of_typ m = {one_arg_matcher= match_typ (m <...>! ()); capture= capture_arg_exp}
 
   let one_arg_matcher_of_prim_typ typ =

infer/src/IR/ProcnameDispatcher.mli

@@ -199,6 +199,11 @@ module Call : sig
        one_arg
   (** Captures one arg of the given type *)
 
+  val capt_arg_payload_of_typ :
+       ('context, unit, _, 'arg_payload) name_matcher
+    -> ('context, 'arg_payload, 'wrapped_arg, 'wrapped_arg -> 'f, 'f, 'arg_payload) one_arg
+  (** Captures the payload of one arg of the given type *)
+
   val capt_exp_of_typ :
        ('context, unit, _, 'arg_payload) name_matcher
     -> ('context, Exp.t, 'wrapped_arg, 'wrapped_arg -> 'f, 'f, 'arg_payload) one_arg

infer/src/pulse/PulseModels.ml

@@ -435,6 +435,18 @@ module StdVector = struct
     >>= PulseOperations.havoc_field location vector GenericArrayBackedCollection.field trace
 
 
+  let init_list_constructor this init_list ~caller_summary:_ ~callee_procname:_ location ~ret:_
+      astate =
+    let event = ValueHistory.Call {f= Model "std::vector::vector()"; location; in_call= []} in
+    let* astate, init_copy = PulseOperations.shallow_copy location init_list astate in
+    let+ astate =
+      PulseOperations.write_field location ~ref:this GenericArrayBackedCollection.field
+        ~obj:(fst init_copy, event :: snd init_copy)
+        astate
+    in
+    [ExecutionDomain.ContinueProgram astate]
+
+
   let invalidate_references vector_f vector : model =
    fun ~caller_summary:_ ~callee_procname:_ location ~ret:_ astate ->
     let crumb =
@@ -534,6 +546,8 @@ module ProcNameDispatcher = struct
       ; +match_builtin BuiltinDecl.__cast <>$ capt_arg_payload $+...$--> Misc.id_first_arg
       ; +match_builtin BuiltinDecl.abort <>--> Misc.early_exit
       ; +match_builtin BuiltinDecl.exit <>--> Misc.early_exit
+      ; +match_builtin BuiltinDecl.__infer_initializer_list
+        <>$ capt_arg_payload $+...$--> Misc.id_first_arg
       ; +PatternMatch.implements_lang "System" &:: "exit" <>--> Misc.early_exit
       ; +match_builtin BuiltinDecl.__get_array_length <>--> Misc.return_unknown_size
       ; (* consider that all fbstrings are small strings to avoid false positives due to manual
@@ -578,6 +592,9 @@ module ProcNameDispatcher = struct
       ; -"std" &:: "integral_constant" < any_typ &+ capt_int
         >::+ (fun _ name -> String.is_prefix ~prefix:"operator_" name)
         <>--> Misc.return_int
+      ; -"std" &:: "vector" &:: "vector" <>$ capt_arg_payload
+        $+ capt_arg_payload_of_typ (-"std" &:: "initializer_list")
+        $+...$--> StdVector.init_list_constructor
       ; -"std" &:: "__wrap_iter" &:: "__wrap_iter" <>$ capt_arg_payload $+ capt_arg_payload
         $+...$--> GenericArrayBackedCollectionIterator.constructor ~desc:"iterator constructor"
       ; -"std" &:: "__wrap_iter" &:: "operator*" <>$ capt_arg_payload

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

@@ -77,7 +77,8 @@ codetoanalyze/cpp/pulse/values.cpp, free_if_deref_bad, 2, USE_AFTER_FREE, no_buc
 codetoanalyze/cpp/pulse/vector.cpp, FP_init_fill_then_push_back_loop_ok, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,variable `vec` declared here,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,variable `vec` declared here,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/vector.cpp, assign_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of assign_bad,was potentially invalidated by `std::vector::assign()`,use-after-lifetime part of the trace starts here,parameter `vec` of assign_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/vector.cpp, clear_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of clear_bad,was potentially invalidated by `std::vector::clear()`,use-after-lifetime part of the trace starts here,parameter `vec` of clear_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
-codetoanalyze/cpp/pulse/vector.cpp, deref_local_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,variable `vec` declared here,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,variable `vec` declared here,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/vector.cpp, deref_local_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,variable `C++ temporary` declared here,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,variable `C++ temporary` declared here,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/vector.cpp, deref_null_local_vector_element_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/vector.cpp, deref_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of deref_vector_element_after_push_back_bad,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,parameter `vec` of deref_vector_element_after_push_back_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/vector.cpp, deref_vector_pointer_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of deref_vector_pointer_element_after_push_back_bad,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,parameter `vec` of deref_vector_pointer_element_after_push_back_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/vector.cpp, emplace_back_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of emplace_back_bad,was potentially invalidated by `std::vector::emplace_back()`,use-after-lifetime part of the trace starts here,parameter `vec` of emplace_back_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]

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

@@ -29,6 +29,11 @@ void deref_local_vector_element_after_push_back_bad() {
   std::cout << *elt << "\n";
 }
 
+void deref_null_local_vector_element_bad() {
+  std::vector<int*> vec = {nullptr};
+  std::cout << *vec[0] << "\n";
+}
+
 void two_push_back_ok(std::vector<int>& vec) {
   vec.push_back(32);
   vec.push_back(52);