[pulse] model some of std::basic_string

Summary:
A common gotcha is the new test. Model the minimum amount of
`std::basic_string` to catch it.

Reviewed By: mbouaziz, ngorogiannis

Differential Revision: D16121090

fbshipit-source-id: 66f06cb43

infer/src/pulse/PulseModels.ml

@@ -77,6 +77,59 @@ module Cplusplus = struct
         Ok [PulseOperations.havoc_id ret_id [event] astate]
 end
 
+module StdBasicString = struct
+  let internal_string =
+    Typ.Fieldname.Clang.from_class_name
+      (Typ.CStruct (QualifiedCppName.of_list ["std"; "basic_string"]))
+      "__infer_model_backing_string"
+
+
+  let internal_string_access = HilExp.Access.FieldAccess internal_string
+
+  let to_internal_string location bstring astate =
+    PulseOperations.eval_access location bstring internal_string_access astate
+
+
+  let data : model =
+   fun ~caller_summary:_ location ~ret:(ret_id, _) ~actuals astate ->
+    let event = PulseDomain.ValueHistory.Call {f= Model "std::basic_string::data()"; location} in
+    match actuals with
+    | [(this_hist, _)] ->
+        to_internal_string location this_hist astate
+        >>= fun (astate, string_addr_hist) ->
+        PulseOperations.eval_access location string_addr_hist Dereference astate
+        >>| fun (astate, (string, hist)) ->
+        [PulseOperations.write_id ret_id (string, event :: hist) astate]
+    | _ ->
+        Ok [PulseOperations.havoc_id ret_id [event] astate]
+
+
+  let destructor : model =
+   fun ~caller_summary:_ location ~ret:(ret_id, _) ~actuals astate ->
+    let model = PulseDomain.Model "std::basic_string::~basic_string()" in
+    let call_event = PulseDomain.ValueHistory.Call {f= model; location} in
+    match actuals with
+    | [(this_hist, _)] ->
+        to_internal_string location this_hist astate
+        >>= fun (astate, string_addr_hist) ->
+        let invalidation =
+          PulseDomain.InterprocAction.ViaCall
+            { location
+            ; f= model
+            ; action=
+                ViaCall
+                  { location
+                  ; f= Model "deleting the underlying string"
+                  ; action= Immediate {imm= PulseDomain.Invalidation.CppDelete; location} } }
+        in
+        PulseOperations.invalidate_deref location invalidation string_addr_hist astate
+        >>= fun astate ->
+        PulseOperations.invalidate location invalidation string_addr_hist astate
+        >>| fun astate -> [astate]
+    | _ ->
+        Ok [PulseOperations.havoc_id ret_id [call_event] astate]
+end
+
 module StdFunction = struct
   let operator_call : model =
    fun ~caller_summary location ~ret ~actuals astate ->
@@ -105,11 +158,13 @@ module StdVector = struct
   let internal_array =
     Typ.Fieldname.Clang.from_class_name
       (Typ.CStruct (QualifiedCppName.of_list ["std"; "vector"]))
-      "__internal_array"
+      "__infer_model_backing_array"
+
 
+  let internal_array_access = HilExp.Access.FieldAccess internal_array
 
   let to_internal_array location vector astate =
-    PulseOperations.eval_access location vector (FieldAccess internal_array) astate
+    PulseOperations.eval_access location vector internal_array_access astate
 
 
   let element_of_internal_array location vector index astate =
@@ -175,7 +230,9 @@ module StdVector = struct
    fun ~caller_summary:_ location ~ret:_ ~actuals astate ->
     match actuals with
     | [(vector, _); _value] ->
-        let crumb = PulseDomain.ValueHistory.Call {f= Model "std::vector::push_back()"; location} in
+        let crumb =
+          PulseDomain.ValueHistory.Call {f= Model "std::vector::push_back()"; location}
+        in
         if PulseAbductiveDomain.Memory.is_std_vector_reserved (fst vector) astate then
           (* assume that any call to [push_back] is ok after one called [reserve] on the same vector
              (a perfect analysis would also make sure we don't exceed the reserved size) *)
@@ -194,6 +251,8 @@ module ProcNameDispatcher = struct
       [ -"folly" &:: "DelayedDestruction" &:: "destroy" &--> Misc.skip
       ; -"folly" &:: "Optional" &:: "reset" &--> Misc.skip
       ; -"folly" &:: "SocketAddress" &:: "~SocketAddress" &--> Misc.skip
+      ; -"std" &:: "basic_string" &:: "data" &--> StdBasicString.data
+      ; -"std" &:: "basic_string" &:: "~basic_string" &--> StdBasicString.destructor
       ; -"std" &:: "function" &:: "operator()" &--> StdFunction.operator_call
       ; -"std" &:: "function" &:: "operator=" &--> Misc.shallow_copy "std::function::operator="
       ; -"std" &:: "vector" &:: "assign" &--> StdVector.invalidate_references Assign

infer/tests/codetoanalyze/cpp/pulse/basic_string.cpp

@@ -0,0 +1,27 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+#include <string>
+
+// inspired by folly::Range
+struct Range {
+  const char *b_, *e_;
+
+  Range(const std::string& str) : b_(str.data()), e_(b_ + str.size()) {}
+
+  char operator[](size_t i) { return b_[i]; }
+};
+
+const Range setLanguage(const std::string& s) {
+  return s[0] == 'k' ? s.substr(0, 1) // cast to Range returns pointers
+                                      // into stack-allocated temporary string
+                     : "en";
+}
+
+bool use_range_of_invalidated_temporary_string_bad(const std::string& str) {
+  auto s = setLanguage(str);
+  return s[0] == 'k';
+}

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

@@ -1,3 +1,4 @@
+codetoanalyze/cpp/pulse/basic_string.cpp, use_range_of_invalidated_temporary_string_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `setLanguage()` here,when calling `std::basic_string::~basic_string()` (modelled) here,when calling `deleting the underlying string` (modelled) here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,variable declared,when calling `Range::operator[]()` here,invalid access occurs here]
 codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,invalid access occurs here]
 codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,invalid access occurs here]
 codetoanalyze/cpp/pulse/closures.cpp, call_lambda_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,when calling `call_lambda_bad::lambda_closures.cpp:163:12::operator()()` here,invalid access occurs here]