[pulse] Refactor Optional models

Summary: Refactor `folly::Optional` models to make them easier to reuse for `std::optional`

Reviewed By: jvillard

Differential Revision: D24760053

fbshipit-source-id: f665e84c8

infer/src/pulse/PulseInvalidation.ml

@@ -91,7 +91,7 @@ let describe f cause =
       in
       F.fprintf f "%a whose lifetime has ended" pp_var pvar
   | OptionalEmpty ->
-      F.pp_print_string f "is folly::None"
+      F.pp_print_string f "is optional empty"
   | StdVector std_vector_f ->
       F.fprintf f "was potentially invalidated by `%a()`" pp_std_vector_function std_vector_f
   | JavaIterator java_iterator_f ->

infer/src/pulse/PulseModels.ml

@@ -182,7 +182,7 @@ module ObjC = struct
     |> PulseOperations.ok_continue
 end
 
-module FollyOptional = struct
+module Optional = struct
   let internal_value = Fieldname.make (Typ.CStruct cpp_model_namespace) "backing_value"
 
   let internal_value_access = HilExp.Access.FieldAccess internal_value
@@ -231,17 +231,15 @@ module FollyOptional = struct
     [ExecutionDomain.ContinueProgram astate]
 
 
-  let emplace optional : model =
+  let emplace optional ~desc : model =
    fun _ ~callee_procname:_ location ~ret:_ astate ->
-    let+ astate, _ =
-      assign_value_fresh location optional ~desc:"folly::Optional::emplace()" astate
-    in
+    let+ astate, _ = assign_value_fresh location optional ~desc astate in
     [ExecutionDomain.ContinueProgram astate]
 
 
-  let value optional : model =
+  let value optional ~desc : model =
    fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
-    let event = ValueHistory.Call {f= Model "folly::Optional::value()"; location; in_call= []} in
+    let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
     let* astate, ((value_addr, value_hist) as value) =
       to_internal_value_deref location optional astate
     in
@@ -251,12 +249,10 @@ module FollyOptional = struct
     |> PulseOperations.ok_continue
 
 
-  let has_value optional : model =
+  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 "folly::Optional::has_value()"; location}])
-    in
+    let ret_value = (ret_addr, [ValueHistory.Allocation {f= Model desc; location}]) 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
@@ -266,9 +262,9 @@ module FollyOptional = struct
     [ExecutionDomain.ContinueProgram astate_false; ExecutionDomain.ContinueProgram astate_true]
 
 
-  let value_or optional default : model =
+  let value_or optional default ~desc : model =
    fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
-    let event = ValueHistory.Call {f= Model "folly::Optional::value_or()"; location; in_call= []} in
+    let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
     let* astate, value_addr = to_internal_value_deref location optional astate in
     let astate_non_empty = PulseArithmetic.and_positive (fst value_addr) astate in
     let* astate_non_empty, value =
@@ -943,33 +939,36 @@ module ProcNameDispatcher = struct
           &++> Misc.skip "folly::SocketAddress's destructor is modelled as skip"
         ; -"folly" &:: "Optional" &:: "Optional" <>$ capt_arg_payload
           $+ any_arg_of_typ (-"folly" &:: "None")
-          $--> FollyOptional.assign_none ~desc:"folly::Optional::Optional(=None)"
+          $--> Optional.assign_none ~desc:"folly::Optional::Optional(=None)"
         ; -"folly" &:: "Optional" &:: "Optional" <>$ capt_arg_payload
-          $--> FollyOptional.assign_none ~desc:"folly::Optional::Optional()"
+          $--> Optional.assign_none ~desc:"folly::Optional::Optional()"
         ; -"folly" &:: "Optional" &:: "Optional" <>$ capt_arg_payload
           $+ capt_arg_payload_of_typ (-"folly" &:: "Optional")
-          $--> FollyOptional.assign_optional_value
+          $--> Optional.assign_optional_value
                  ~desc:"folly::Optional::Optional(folly::Optional<Value> arg)"
         ; -"folly" &:: "Optional" &:: "Optional" <>$ capt_arg_payload $+ capt_arg_payload
-          $+...$--> FollyOptional.assign_value ~desc:"folly::Optional::Optional(Value arg)"
+          $+...$--> Optional.assign_value ~desc:"folly::Optional::Optional(Value arg)"
         ; -"folly" &:: "Optional" &:: "assign" <>$ capt_arg_payload
           $+ any_arg_of_typ (-"folly" &:: "None")
-          $--> FollyOptional.assign_none ~desc:"folly::Optional::assign(=None)"
+          $--> Optional.assign_none ~desc:"folly::Optional::assign(=None)"
         ; -"folly" &:: "Optional" &:: "assign" <>$ capt_arg_payload
           $+ capt_arg_payload_of_typ (-"folly" &:: "Optional")
-          $--> FollyOptional.assign_optional_value
+          $--> Optional.assign_optional_value
                  ~desc:"folly::Optional::assign(folly::Optional<Value> arg)"
         ; -"folly" &:: "Optional" &:: "assign" <>$ capt_arg_payload $+ capt_arg_payload
-          $+...$--> FollyOptional.assign_value ~desc:"folly::Optional::assign(Value arg)"
-        ; -"folly" &:: "Optional" &:: "emplace<>" $ capt_arg_payload $+...$--> FollyOptional.emplace
-        ; -"folly" &:: "Optional" &:: "emplace" $ capt_arg_payload $+...$--> FollyOptional.emplace
+          $+...$--> Optional.assign_value ~desc:"folly::Optional::assign(Value arg)"
+        ; -"folly" &:: "Optional" &:: "emplace<>" $ capt_arg_payload
+          $+...$--> Optional.emplace ~desc:"folly::Optional::emplace()"
+        ; -"folly" &:: "Optional" &:: "emplace" $ capt_arg_payload
+          $+...$--> Optional.emplace ~desc:"folly::Optional::emplace()"
         ; -"folly" &:: "Optional" &:: "has_value" <>$ capt_arg_payload
-          $+...$--> FollyOptional.has_value
+          $+...$--> Optional.has_value ~desc:"folly::Optional::has_value()"
         ; -"folly" &:: "Optional" &:: "reset" <>$ capt_arg_payload
-          $+...$--> FollyOptional.assign_none ~desc:"folly::Optional::reset()"
-        ; -"folly" &:: "Optional" &:: "value" <>$ capt_arg_payload $+...$--> FollyOptional.value
+          $+...$--> Optional.assign_none ~desc:"folly::Optional::reset()"
+        ; -"folly" &:: "Optional" &:: "value" <>$ capt_arg_payload
+          $+...$--> Optional.value ~desc:"folly::Optional::value()"
         ; -"folly" &:: "Optional" &:: "value_or" $ capt_arg_payload $+ capt_arg_payload
-          $+...$--> FollyOptional.value_or
+          $+...$--> Optional.value_or ~desc:"folly::Optional::value_or()"
         ; -"std" &:: "basic_string" &:: "data" <>$ capt_arg_payload $--> StdBasicString.data
         ; -"std" &:: "basic_string" &:: "~basic_string" <>$ capt_arg_payload
           $--> StdBasicString.destructor

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

@@ -46,12 +46,12 @@ codetoanalyze/cpp/pulse/nullptr.cpp, deref_nullptr_bad, 2, NULLPTR_DEREFERENCE,
 codetoanalyze/cpp/pulse/nullptr.cpp, no_check_return_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `may_return_nullptr` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `may_return_nullptr`,return from call to `may_return_nullptr`,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/nullptr.cpp, std_false_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/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 folly::None,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 folly::None,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, 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 folly::None,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 folly::None,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, operator_arrow_bad, 0, 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 folly::None,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),when calling `emplace` here,parameter `state` of emplace,passed as argument to `folly::Optional<State>::operator->`,return from call to `folly::Optional<State>::operator->`,invalid access occurs here]
-codetoanalyze/cpp/pulse/optional.cpp, test_trace_ref, 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 folly::None,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, 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, 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, operator_arrow_bad, 0, 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),when calling `emplace` here,parameter `state` of emplace,passed as argument to `folly::Optional<State>::operator->`,return from call to `folly::Optional<State>::operator->`,invalid access occurs here]
+codetoanalyze/cpp/pulse/optional.cpp, test_trace_ref, 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/path.cpp, faulty_call_bad, 0, NULLPTR_DEREFERENCE, no_bucket, ERROR, [calling context starts here,in call to `only_bad_on_42_latent`,invalidation part of the trace starts here,when calling `may_return_null` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `may_return_null`,return from call to `may_return_null`,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/path.cpp, only_bad_on_42_latent, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,when calling `may_return_null` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `may_return_null`,return from call to `may_return_null`,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/reference_wrapper.cpp, reference_wrapper_heap_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `getwrapperHeap` here,passed as argument to `WrapsB::WrapsB`,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,return from call to `WrapsB::WrapsB`,when calling `WrapsB::~WrapsB` here,parameter `this` of WrapsB::~WrapsB,when calling `WrapsB::__infer_inner_destructor_~WrapsB` here,parameter `this` of WrapsB::__infer_inner_destructor_~WrapsB,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `getwrapperHeap`,passed as argument to `WrapsB::WrapsB`,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,return from call to `WrapsB::WrapsB`,passed as argument to `ReferenceWrapperHeap::ReferenceWrapperHeap`,parameter `a` of ReferenceWrapperHeap::ReferenceWrapperHeap,passed as argument to `WrapsB::getb`,return from call to `WrapsB::getb`,assigned,return from call to `ReferenceWrapperHeap::ReferenceWrapperHeap`,return from call to `getwrapperHeap`,invalid access occurs here]