[pulse] Model for std::function copy constructor

Summary: Added a model for copy constructor for `std::function`. In most cases, the SIL instruction `std::function::function(&dest, &src)` gives us pointers to `dest` and `src`, hence, we model the copy constructor as a shallow copy. However, in some cases, e.g.  `std::function f = lambda_literal`, SIL instruction contains the closure itself `std::function::function(&dest, (operator(), captured_vars)`, hence, we need to make sure we copy the right value.

Reviewed By: ezgicicek

Differential Revision: D23396568

fbshipit-source-id: 0acb8f6bc

infer/src/pulse/PulseModels.ml

@@ -23,9 +23,8 @@ type model =
 let cpp_model_namespace = QualifiedCppName.of_list ["__infer_pulse_model"]
 
 module Misc = struct
-  let shallow_copy location event ret_id dest_pointer_hist src_pointer_hist astate =
-    let* astate, obj = PulseOperations.eval_access location src_pointer_hist Dereference astate in
-    let* astate, obj_copy = PulseOperations.shallow_copy location obj astate in
+  let shallow_copy_value location event ret_id dest_pointer_hist src_value_hist astate =
+    let* astate, obj_copy = PulseOperations.shallow_copy location src_value_hist astate in
     let+ astate =
       PulseOperations.write_deref location ~ref:dest_pointer_hist
         ~obj:(fst obj_copy, event :: snd obj_copy)
@@ -34,6 +33,11 @@ module Misc = struct
     PulseOperations.havoc_id ret_id [event] astate
 
 
+  let shallow_copy location event ret_id dest_pointer_hist src_pointer_hist astate =
+    let* astate, obj = PulseOperations.eval_access location src_pointer_hist Dereference astate in
+    shallow_copy_value location event ret_id dest_pointer_hist obj astate
+
+
   let shallow_copy_model model_desc dest_pointer_hist src_pointer_hist : model =
    fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
     let event = ValueHistory.Call {f= Model model_desc; location; in_call= []} in
@@ -455,9 +459,9 @@ module StdFunction = struct
           location callee_proc_name ~ret ~actuals ~formals_opt:None astate
 
 
-  let operator_equal dest src : model =
+  let assign dest ProcnameDispatcher.Call.FuncArg.{arg_payload= src; typ= src_typ} ~desc : model =
    fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
-    let event = ValueHistory.Call {f= Model "std::function::operator="; location; in_call= []} in
+    let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
     let+ astate =
       if PulseArithmetic.is_known_zero astate (fst src) then
         let empty_target = AbstractValue.mk_fresh () in
@@ -465,7 +469,12 @@ module StdFunction = struct
           PulseOperations.write_deref location ~ref:dest ~obj:(empty_target, [event]) astate
         in
         PulseOperations.havoc_id ret_id [event] astate
-      else Misc.shallow_copy location event ret_id dest src astate
+      else
+        match src_typ.Typ.desc with
+        | Tptr (_, Pk_reference) ->
+            Misc.shallow_copy location event ret_id dest src astate
+        | _ ->
+            Misc.shallow_copy_value location event ret_id dest src astate
     in
     [ExecutionDomain.ContinueProgram astate]
 end
@@ -892,9 +901,11 @@ module ProcNameDispatcher = struct
         ; -"std" &:: "basic_string" &:: "data" <>$ capt_arg_payload $--> StdBasicString.data
         ; -"std" &:: "basic_string" &:: "~basic_string" <>$ capt_arg_payload
           $--> StdBasicString.destructor
+        ; -"std" &:: "function" &:: "function" $ capt_arg_payload $+ capt_arg
+          $--> StdFunction.assign ~desc:"std::function::function"
         ; -"std" &:: "function" &:: "operator()" $ capt_arg $++$--> StdFunction.operator_call
-        ; -"std" &:: "function" &:: "operator=" $ capt_arg_payload $+ capt_arg_payload
-          $--> StdFunction.operator_equal
+        ; -"std" &:: "function" &:: "operator=" $ capt_arg_payload $+ capt_arg
+          $--> StdFunction.assign ~desc:"std::function::operator="
         ; +PatternMatch.Java.implements_lang "Object"
           &:: "clone" $ capt_arg_payload $--> JavaObject.clone
         ; ( +PatternMatch.Java.implements_lang "System"

infer/tests/codetoanalyze/cpp/pulse/closures.cpp

@@ -174,6 +174,16 @@ void call_lambda_std_fun_bad() {
   f(s);
 }
 
+void call_std_fun_constructor_bad() {
+  std::function<void(S*)> f1 = [](S* s) { int x = s->f; };
+  std::function<void(S*)> f2 = f1;
+  S* s = new S();
+  delete s;
+  f2(s);
+}
+
+void function_constructor_null_ok() { std::function<int()> f = nullptr; }
+
 void function_assign_null_ok() {
   std::function<int()> f = [] { return 1; };
   f = nullptr;

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

@@ -8,6 +8,7 @@ codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 5, USE_AFTE
 codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 8, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_bad,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,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,when calling `call_lambda_bad::lambda_closures.cpp:163:12::operator()` here,parameter `s` of call_lambda_bad::lambda_closures.cpp:163:12::operator(),invalid access occurs here]
 codetoanalyze/cpp/pulse/closures.cpp, call_lambda_std_fun_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,when calling `call_lambda_std_fun_bad::lambda_closures.cpp:171:7::operator()` here,parameter `s` of call_lambda_std_fun_bad::lambda_closures.cpp:171:7::operator(),invalid access occurs here]
+codetoanalyze/cpp/pulse/closures.cpp, call_std_fun_constructor_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,when calling `call_std_fun_constructor_bad::lambda_closures.cpp:178:32::operator()` here,parameter `s` of call_std_fun_constructor_bad::lambda_closures.cpp:178:32::operator(),invalid access occurs here]
 codetoanalyze/cpp/pulse/closures.cpp, capture_by_ref_bad, 7, 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/closures.cpp, capture_by_value_bad, 7, 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/closures.cpp, implicit_ref_capture_destroy_invoke_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s` declared here,is the address of a stack variable `s` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `s` declared here,value captured by by ref as `s`,invalid access occurs here]