[pulse] Model for folly::Optional::get_pointer

Summary: Model `folly::Optional::get_pointer` which returns an address to a value if exists or `nullptr` if empty.

Reviewed By: jvillard

Differential Revision: D24935677

fbshipit-source-id: 9d990fe07

infer/src/pulse/PulseModels.ml

@@ -252,7 +252,7 @@ module Optional = struct
   let has_value optional ~desc : model =
    fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
     let ret_addr = AbstractValue.mk_fresh () in
-    let ret_value = (ret_addr, [ValueHistory.Allocation {f= Model desc; location}]) in
+    let ret_value = (ret_addr, [ValueHistory.Call {f= Model desc; location; in_call= []}]) in
     let+ astate, (value_addr, _) = to_internal_value_deref location optional astate in
     let astate = PulseOperations.write_id ret_id ret_value astate in
     let astate_non_empty = PulseArithmetic.and_positive value_addr astate in
@@ -262,6 +262,25 @@ module Optional = struct
     [ExecutionDomain.ContinueProgram astate_false; ExecutionDomain.ContinueProgram astate_true]
 
 
+  let get_pointer optional ~desc : model =
+   fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
+    let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
+    let* astate, value_addr = to_internal_value_deref location optional astate in
+    let value_update_hist = (fst value_addr, event :: snd value_addr) in
+    let astate_value_addr =
+      PulseOperations.write_id ret_id value_update_hist astate
+      |> PulseArithmetic.and_positive (fst value_addr)
+    in
+    let nullptr = (AbstractValue.mk_fresh (), [event]) in
+    let+ astate_null =
+      PulseOperations.write_id ret_id nullptr astate
+      |> PulseArithmetic.and_eq_int (fst value_addr) IntLit.zero
+      |> PulseArithmetic.and_eq_int (fst nullptr) IntLit.zero
+      |> PulseOperations.invalidate location (ConstantDereference IntLit.zero) nullptr
+    in
+    [ExecutionDomain.ContinueProgram astate_value_addr; ExecutionDomain.ContinueProgram astate_null]
+
+
   let value_or optional default ~desc : model =
    fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
     let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
@@ -969,6 +988,8 @@ module ProcNameDispatcher = struct
           $+...$--> Optional.assign_none ~desc:"folly::Optional::reset()"
         ; -"folly" &:: "Optional" &:: "value" <>$ capt_arg_payload
           $+...$--> Optional.value ~desc:"folly::Optional::value()"
+        ; -"folly" &:: "Optional" &:: "get_pointer" $ capt_arg_payload
+          $+...$--> Optional.get_pointer ~desc:"folly::Optional::get_pointer()"
         ; -"folly" &:: "Optional" &:: "value_or" $ capt_arg_payload $+ capt_arg_payload
           $+...$--> Optional.value_or ~desc:"folly::Optional::value_or()"
           (* std::optional *)

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

@@ -50,6 +50,7 @@ codetoanalyze/cpp/pulse/nullptr.cpp, std_false_type_deref_bad, 3, NULLPTR_DEREFE
 codetoanalyze/cpp/pulse/nullptr.cpp, std_true_type_deref_bad, 3, 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/optional.cpp, assign2_bad, 4, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `folly::Optional<int>::operator=` here,passed as argument to `folly::Optional::reset()` (modelled),return from call to `folly::Optional::reset()` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `folly::Optional<int>::operator=`,passed as argument to `folly::Optional::reset()` (modelled),return from call to `folly::Optional::reset()` (modelled),return from call to `folly::Optional<int>::operator=`,invalid access occurs here]
 codetoanalyze/cpp/pulse/optional.cpp, assign_bad, 5, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),passed as argument to `folly::Optional<int>::operator=`,parameter `other` of folly::Optional<int>::operator=,passed as argument to `folly::Optional::assign(folly::Optional<Value> arg)` (modelled),return from call to `folly::Optional::assign(folly::Optional<Value> arg)` (modelled),return from call to `folly::Optional<int>::operator=`,invalid access occurs here]
+codetoanalyze/cpp/pulse/optional.cpp, get_pointer_no_check_none_check_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `folly::Optional::get_pointer()` (modelled),return from call to `folly::Optional::get_pointer()` (modelled),is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `folly::Optional::get_pointer()` (modelled),return from call to `folly::Optional::get_pointer()` (modelled),assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/optional.cpp, none_copy_bad, 3, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),passed as argument to `folly::Optional::Optional(folly::Optional<Value> arg)` (modelled),return from call to `folly::Optional::Optional(folly::Optional<Value> arg)` (modelled),invalid access occurs here]
 codetoanalyze/cpp/pulse/optional.cpp, none_no_check_bad, 2, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),invalid access occurs here]
 codetoanalyze/cpp/pulse/optional.cpp, not_none_check_value_ok_FP, 5, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),invalid access occurs here]

infer/tests/codetoanalyze/cpp/pulse/optional.cpp

@@ -63,6 +63,8 @@ class Optional {
 
   constexpr Value* operator->() { return &value(); }
 
+  Value* get_pointer();
+
   template <class U>
   constexpr Value value_or(U&& dflt) const&;
 };
@@ -147,6 +149,32 @@ void emplace(folly::Optional<State> state) {
 
 void operator_arrow_bad() { emplace(folly::none); }
 
+void get_pointer_check_none_check_ok() {
+  folly::Optional<int> foo{folly::none};
+  if (int* v = foo.get_pointer()) {
+    *v = 42;
+  }
+}
+
+void get_pointer_check_value_check_ok() {
+  folly::Optional<int> foo{5};
+  if (int* ptr = foo.get_pointer()) {
+    *ptr = 42;
+  }
+}
+
+void get_pointer_no_check_none_check_bad() {
+  folly::Optional<int> foo{folly::none};
+  int* ptr = foo.get_pointer();
+  *ptr = 42;
+}
+
+void get_pointer_no_check_value_check_ok() {
+  folly::Optional<int> foo{5};
+  int* ptr = foo.get_pointer();
+  *ptr = 42;
+}
+
 int value_or_check_empty_ok() {
   folly::Optional<int> foo{folly::none};
   if (foo.value_or(0) > 0) {