[unnecessary copy] Join non-disj astate when dropping disjuncts

Summary:
HACK: When it drops disjuncts due to the disjunct limit, it also loses some information on the
non-disjunctive abstract state, i.e. [pre_non_disj], which resulted in false positives. To mitigate
the problem, it joins [pre_non_disj] when needed, while it is incorrect to join without running
[exec_instr] precisely speaking.

Reviewed By: jvillard

Differential Revision: D50638427

fbshipit-source-id: ace6c1982984af92b270de1b88492b741da6a8e1

infer/src/absint/AbstractInterpreter.ml

@@ -426,15 +426,19 @@ struct
       | Some {State.post= post_disjuncts, post_non_disjunct; _} ->
           ((post_disjuncts, post_non_disjunct), List.length post_disjuncts)
     in
-    let (disjuncts, non_disj_astates), _ =
-      List.foldi (List.rev pre) ~init:current_post_n
-        ~f:(fun i (((post, non_disj_astate) as post_astate), n_disjuncts) pre_disjunct ->
+    let ((disjuncts, non_disj_astates), _), need_join_non_disj =
+      List.foldi (List.rev pre) ~init:(current_post_n, false)
+        ~f:(fun
+             i
+             ((((post, non_disj_astate) as post_astate), n_disjuncts), need_join_non_disj)
+             pre_disjunct
+           ->
           let limit = disjunct_limit - n_disjuncts in
           AnalysisState.set_remaining_disjuncts limit ;
           if limit <= 0 then (
             L.d_printfln "@[Reached disjunct limit: already got %d disjuncts@]@;" n_disjuncts ;
             DisjunctiveMetadata.add_dropped_disjuncts 1 ;
-            (post_astate, n_disjuncts) )
+            (((post, non_disj_astate), n_disjuncts), true) )
           else if is_new_pre pre_disjunct then (
             L.d_printfln "@[<v2>Executing node from disjunct #%d, setting limit to %d@;" i limit ;
             let disjuncts', non_disj' =
@@ -443,18 +447,34 @@ struct
             L.d_printfln "@]@\n" ;
             let disj', n, dropped = Domain.join_up_to ~limit:disjunct_limit ~into:post disjuncts' in
             DisjunctiveMetadata.add_dropped_disjuncts dropped ;
-            ((disj', T.NonDisjDomain.join non_disj_astate non_disj'), n) )
+            (((disj', T.NonDisjDomain.join non_disj_astate non_disj'), n), need_join_non_disj) )
           else (
             L.d_printfln "@[Skipping already-visited disjunct #%d@]@;" i ;
-            (post_astate, n_disjuncts) ) )
+            (* HACK: [pre_non_disj] may have a new information, e.g. when the predecessor node
+               reached the disjunct limit, so join [pre_non_disj]. *)
+            ((post_astate, n_disjuncts), true) ) )
     in
     let non_disjunct =
       if
         Config.pulse_prevent_non_disj_top
         || List.exists disjuncts ~f:T.DisjDomain.is_executable
         || List.is_empty disjuncts
-      then non_disj_astates
-      else T.NonDisjDomain.top
+      then
+        if need_join_non_disj then
+          (* HACK: When we drop disjuncts due to the disjunct limit, we may lose some information on
+             the non-disjunctive abstract state, i.e. [pre_non_disj], which can result in false
+             positives.  To mitigate the issue, join [pre_non_disj] when dropping disjuncts even
+             though joining without running [exec_instr] is, strictly speaking,
+             incorrect/unsound. *)
+          T.NonDisjDomain.join non_disj_astates pre_non_disj
+        else non_disj_astates
+      else
+        (* When there is no executable disjunct, we did not actually execute the instructions.
+           Instead, we passed the non-executable disjuncts to the next node unchanged.  While this
+           is fine for disjunctive abstract states, it is not for non-disjunctive abstract state,
+           e.g. the unnecessary copy checker since it may miss some modifications of copied values.
+           To mitigate the issue, return top when all disjuncts are non-executable. *)
+        T.NonDisjDomain.top
     in
     (disjuncts, non_disjunct)
 

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

@@ -125,9 +125,9 @@ codetoanalyze/cpp/pulse/leaks.cpp, leaks::new_array_delete_bad, 2, MEMORY_LEAK_C
 codetoanalyze/cpp/pulse/leaks.cpp, leaks::unique_ptr_pointer_bad, 1, MEMORY_LEAK_CPP, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `new` here,memory becomes unreachable here]
 codetoanalyze/cpp/pulse/leaks.cpp, leaks::FP_call_static_local_alloc_twice_ok, 3, MEMORY_LEAK_CPP, no_bucket, ERROR, [allocation part of the trace starts here,when calling `leaks::static_local_alloc_ok` here,allocated by `new` here,memory becomes unreachable here]
 codetoanalyze/cpp/pulse/leaks.cpp, leaks::unknown_wrapper_alloc_then_leak_bad, 3, MEMORY_LEAK_CPP, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `new` here,memory becomes unreachable here]
-codetoanalyze/cpp/pulse/max_disjuncts.cpp, call_join_full_disjs1_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here]
-codetoanalyze/cpp/pulse/max_disjuncts.cpp, call_join_full_disjs2_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here]
-codetoanalyze/cpp/pulse/max_disjuncts.cpp, call_join_full_disjs3_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/max_disjuncts.cpp, max_disjuncts::call_join_full_disjs1_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/max_disjuncts.cpp, max_disjuncts::call_join_full_disjs2_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/max_disjuncts.cpp, max_disjuncts::call_join_full_disjs3_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/nullptr.cpp, A::this_notnull_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [parameter `this` of A::this_notnull_bad,taking "then" branch,is assigned to the null pointer,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/nullptr.cpp, A::call_null_arg_bad, 0, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,when calling `A::expect_notnull_ok` here,parameter `a` of A::expect_notnull_ok,invalid access occurs here]
 codetoanalyze/cpp/pulse/nullptr.cpp, deref_nullptr_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here]

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

@@ -136,9 +136,9 @@ codetoanalyze/cpp/pulse/leaks.cpp, leaks::FP_call_static_local_alloc_twice_ok, 3
 codetoanalyze/cpp/pulse/leaks.cpp, leaks::unknown_wrapper_alloc_then_leak_bad, 3, MEMORY_LEAK_CPP, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `new` here,memory becomes unreachable here]
 codetoanalyze/cpp/pulse/leaks.cpp, leaks::capture_alloc_unknown_ok, 2, MEMORY_LEAK_CPP, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `new` here,memory becomes unreachable here]
 codetoanalyze/cpp/pulse/leaks.cpp, leaks::capture_alloc_return_ok, 2, MEMORY_LEAK_CPP, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `new` here,memory becomes unreachable here]
-codetoanalyze/cpp/pulse/max_disjuncts.cpp, call_join_full_disjs1_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here]
-codetoanalyze/cpp/pulse/max_disjuncts.cpp, call_join_full_disjs2_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here]
-codetoanalyze/cpp/pulse/max_disjuncts.cpp, call_join_full_disjs3_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/max_disjuncts.cpp, max_disjuncts::call_join_full_disjs1_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/max_disjuncts.cpp, max_disjuncts::call_join_full_disjs2_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/max_disjuncts.cpp, max_disjuncts::call_join_full_disjs3_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/nullptr.cpp, A::this_notnull_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [parameter `this` of A::this_notnull_bad,taking "then" branch,is assigned to the null pointer,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/nullptr.cpp, A::call_null_arg_bad, 0, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,when calling `A::expect_notnull_ok` here,parameter `a` of A::expect_notnull_ok,invalid access occurs here]
 codetoanalyze/cpp/pulse/nullptr.cpp, deref_nullptr_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here]

infer/tests/codetoanalyze/cpp/pulse/max_disjuncts.cpp

@@ -5,6 +5,10 @@
  * LICENSE file in the root directory of this source tree.
  */
 
+#include <vector>
+
+namespace max_disjuncts {
+
 int rand_int();
 
 // This returns the state with current maximum disjuncts (20).
@@ -102,3 +106,19 @@ void call_join_full_disjs3_bad() {
   int* p = nullptr;
   *p = 42;
 }
+
+struct Arr {
+  int arr[2];
+  std::vector<int> vec;
+};
+
+void copy_and_modify_ok(const std::vector<int>& v, const Arr& arg) {
+  int x = get_full_disjs(); // make max disjuncts
+  auto copied_arg = arg; // copy arg
+  for (const int& e : v) {
+    copied_arg.arr[0] = 42; // modify copied_arg
+    int y = arg.arr[0];
+  }
+}
+
+} // namespace max_disjuncts