[pulse] don't always mistake equality for aliasing

Summary:
When applying function summaries, we are careful not to violate the
summary's assumptions about non-aliasing. For example, the summary we
generate for `foo(x,y) { *x = *y; }` will have `x` and `y` be allocated
to two different `AbstractValue.t` in the heap, representing
disjointness.

However, the current logic is too coarse and also rejects passing the
same pure value to functions that made no assumption about them being
equal or different, eg `goo(int x,int y) { int z = x + y; }`. This is
because the corresponding `AbstractValue.t` are different in the
callee's summary, but are represented by only one same value in callers
such as `goo(i,i)`.

This diff restricts the "don't violate aliasing" condition to only
consider heap-allocated values. This is consistent with separation logic
by the way: we use the implication `x|->- * y|->- |- x≠y`, which is
valid only when both `x` and `y` are both allocated in the heap as in
the left-hand-side of `|-`.

Reviewed By: skcho

Differential Revision: D22574297

fbshipit-source-id: 206a18499

infer/src/pulse/PulseInterproc.ml

@@ -92,11 +92,18 @@ let fold_globals_of_stack call_loc stack call_state ~f =
           Ok call_state )
 
 
-let visit call_state ~addr_callee ~addr_hist_caller =
+let visit call_state ~pre ~addr_callee ~addr_hist_caller =
   let addr_caller = fst addr_hist_caller in
   ( match AddressMap.find_opt addr_caller call_state.rev_subst with
   | Some addr_callee' when not (AbstractValue.equal addr_callee addr_callee') ->
-      raise (Contradiction (Aliasing {addr_caller; addr_callee; addr_callee'; call_state}))
+      (* [addr_caller] corresponds to several values in the callee, see if that's a problem for
+         applying the pre-condition, i.e. if both values are addresses in the callee's heap, which
+         means they must be disjoint. If so, raise a contradiction, but if not then continue as it
+         just means that the callee doesn't care about the value of these variables. *)
+      if
+        BaseMemory.mem addr_callee pre.BaseDomain.heap
+        && BaseMemory.mem addr_callee' pre.BaseDomain.heap
+      then raise (Contradiction (Aliasing {addr_caller; addr_callee; addr_callee'; call_state}))
   | _ ->
       () ) ;
   if AddressSet.mem addr_callee call_state.visited then (`AlreadyVisited, call_state)
@@ -126,7 +133,7 @@ let add_call_to_trace proc_name call_location caller_history in_call =
     addresses are traversed in the process. *)
 let rec materialize_pre_from_address callee_proc_name call_location ~pre ~addr_pre ~addr_hist_caller
     call_state =
-  match visit call_state ~addr_callee:addr_pre ~addr_hist_caller with
+  match visit call_state ~pre ~addr_callee:addr_pre ~addr_hist_caller with
   | `AlreadyVisited, call_state ->
       Ok call_state
   | `NotAlreadyVisited, call_state -> (
@@ -318,7 +325,7 @@ let record_post_cell callee_proc_name call_loc ~addr_callee ~edges_pre_opt
 let rec record_post_for_address callee_proc_name call_loc ({AbductiveDomain.pre; _} as pre_post)
     ~addr_callee ~addr_hist_caller call_state =
   L.d_printfln "%a<->%a" AbstractValue.pp addr_callee AbstractValue.pp (fst addr_hist_caller) ;
-  match visit call_state ~addr_callee ~addr_hist_caller with
+  match visit call_state ~pre:(pre :> BaseDomain.t) ~addr_callee ~addr_hist_caller with
   | `AlreadyVisited, call_state ->
       call_state
   | `NotAlreadyVisited, call_state -> (

infer/tests/codetoanalyze/cpp/pulse/aliasing.cpp

@@ -0,0 +1,52 @@
+/*
+ * 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.
+ */
+
+void ifthenderef(bool b, int* x) {
+  if (b) {
+    *x = 42;
+  }
+}
+
+void ifnotthenderef(bool b, int* x) {
+  if (!b) {
+    *x = 42;
+  }
+}
+
+void call_ifthenderef_false_null_ok() { ifthenderef(false, nullptr); }
+
+void call_ifthenderef_true_null_bad() { ifthenderef(true, nullptr); }
+
+void call_ifnotthenderef_true_null_ok() { ifnotthenderef(true, nullptr); }
+
+void call_ifnotthenderef_false_null_bad() { ifnotthenderef(false, nullptr); }
+
+// should be FN given the current "all allocated addresses are assumed
+// disjoint unless specified otherwise" but we detect the bug because
+// we don't propagate pure equalities that we discover to the heap part
+void alias_null_deref_bad(int* x, int* y) {
+  *x = 32;
+  *y = 52;
+  if (x == y) {
+    // here we have x|-> * x |-> which should be a contradiction
+    int* p = nullptr;
+    *p = 42;
+  }
+}
+
+void diverge_if_alias_ok(int* x, int* y) {
+  if (x == y) {
+    for (;;)
+      ;
+  }
+}
+
+void FP_diverge_before_null_deref_ok(int* x) {
+  diverge_if_alias_ok(x, x);
+  int* p = nullptr;
+  *p = 42;
+}

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

@@ -1,3 +1,7 @@
+codetoanalyze/cpp/pulse/aliasing.cpp, FP_diverge_before_null_deref_ok, 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/aliasing.cpp, alias_null_deref_bad, 6, 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/aliasing.cpp, call_ifnotthenderef_false_null_bad, 0, 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,when calling `ifnotthenderef` here,parameter `x` of ifnotthenderef,invalid access occurs here]
+codetoanalyze/cpp/pulse/aliasing.cpp, call_ifthenderef_true_null_bad, 0, 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,when calling `ifthenderef` here,parameter `x` of ifthenderef,invalid access occurs here]
 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,variable `C++ temporary` declared here,passed as argument to `Range::Range`,parameter `str` of Range::Range,return from call to `Range::Range`,passed as argument to `std::basic_string::~basic_string()` (modelled),return from call to `std::basic_string::~basic_string()` (modelled),was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `setLanguage`,variable `C++ temporary` declared here,passed as argument to `Range::Range`,parameter `str` of Range::Range,passed as argument to `std::basic_string::data()` (modelled),return from call to `std::basic_string::data()` (modelled),assigned,return from call to `Range::Range`,return from call to `setLanguage`,when calling `Range::operator[]` here,parameter `this` of Range::operator[],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,parameter `ptr` of multiple_invalidations_branch_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_bad,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,parameter `ptr` of multiple_invalidations_branch_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_bad,invalid access occurs here]
@@ -77,6 +81,7 @@ codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_global_bad, 2, USE_AFTER
 codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of double_free_simple_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of double_free_simple_bad,invalid access occurs here]
 codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of use_after_free_simple_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of use_after_free_simple_bad,invalid access occurs here]
 codetoanalyze/cpp/pulse/use_after_scope.cpp, access_out_of_scope_stack_ref_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `p` declared here,when calling `invalidate_local_ok` here,variable `t` declared here,is the address of a stack variable `t` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `p` declared here,passed as argument to `invalidate_local_ok`,variable `t` declared here,assigned,return from call to `invalidate_local_ok`,invalid access occurs here]
+codetoanalyze/cpp/pulse/values.cpp, FP_function_empty_range_interproc_ok, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `StringRange::StringRange` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `StringRange::StringRange`,assigned,return from call to `StringRange::StringRange`,when calling `find_first_non_space` here,parameter `x` of find_first_non_space,passed as argument to `StringRange::data`,return from call to `StringRange::data`,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/values.cpp, error_under_true_conditionals_bad, 5, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of error_under_true_conditionals_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of error_under_true_conditionals_bad,invalid access occurs here]
 codetoanalyze/cpp/pulse/values.cpp, free_if_deref_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of free_if_deref_bad,when calling `free_if` here,parameter `x` of free_if,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of free_if_deref_bad,invalid access occurs here]
 codetoanalyze/cpp/pulse/vector.cpp, FP_init_fill_then_push_back_loop_ok, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,variable `vec` declared here,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,variable `vec` declared here,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]

infer/tests/codetoanalyze/cpp/pulse/values.cpp

@@ -111,7 +111,7 @@ void find_first_non_space(StringRange& x) {
   }
 }
 
-void function_empty_range_interproc_ok() {
+void FP_function_empty_range_interproc_ok() {
   StringRange x{};
   find_first_non_space(x);
 }