[pulse] Only propagate existing WrittenTo attributes at function calls

Summary:
Previously, at each function call, we added a `WrittenTo` attribute for applying the address of the actuals.  However, this results in mistakenly considering each function application that inspects its argument as impure. Instead, we should only propagate `WrittenTo` if the actuals have already `WrittenTo` attributes.

 For instance, for the following functions
```
 public static boolean is_null(Byte a) {
    return a == null;
  }

  public static boolean call_is_null(Byte a) {
    return is_null(a);
  }
```

We used to get the following pulse summary for `call_is_null` (showing only one of the disjuncts):
```
#0: PRE:
      { roots={ &a=v1 };
        mem  ={ v1 -> { * -> v2 } };
        attrs={ v1 -> { MustBeValid  },
                v2 -> { Arith =null, BoItv ([max(0, v2), min(0, v2)]) } };}
    POST:
      { roots={ &a=v1, &return=v8 };
        mem  ={ v1 -> { * -> v2 }, v8 -> { * -> v4 } };
        attrs={ v2 -> { Arith =null,
                        BoItv ([max(0, v2), min(0, v2)]),
                        WrittenTo-----------WRONG  },
                v4 -> { Arith =1,
                        BoItv (1),
                        Invalid ConstantDereference(is the constant 1),
                        WrittenTo-----------WRONG   },
                v8 -> { WrittenTo  } };}
    SKIPPED_CALLS: { }
```

where we mistakenly recorded a `WrittenTo` for `v2` (what `a` points to). As a result, we considered `call_is_null` as impure :( This diff fixes that since the callee `is_null` doesn't have any `WrittenTo` attributes for its parameter `a`. So, we don't propagate `WrittenTo` and get the following summary
```
#0: PRE:
      { roots={ &a=v1 };
        mem  ={ v1 -> { * -> v2 } };
        attrs={ v1 -> { MustBeValid  },
                v2 -> { Arith =null, BoItv ([max(0, v2), min(0, v2)]) } };}
    POST:
      { roots={ &a=v1, &return=v8 };
        mem  ={ v1 -> { * -> v2 }, v8 -> { * -> v4 } };
        attrs={ v2 -> { Arith =null, BoItv ([max(0, v2), min(0, v2)]) },
                v4 -> { Arith =1,
                        BoItv (1),
                        Invalid ConstantDereference(is the constant 1) },
                v8 -> { WrittenTo  } };}
    SKIPPED_CALLS: { }
```

Reviewed By: skcho

Differential Revision: D20490102

fbshipit-source-id: 253d8ef64

infer/src/pulse/PulseAbductiveDomain.ml

@@ -817,19 +817,16 @@ module PrePost = struct
       BaseMemory.add addr_caller edges_post_caller heap
     in
     let attrs =
-      let written_to =
       let written_to_callee_opt =
         let open IOption.Let_syntax in
         let* attrs = BaseAddressAttributes.find_opt addr_caller attrs in
         Attributes.get_written_to attrs
       in
-        let callee_trace =
       match written_to_callee_opt with
       | None ->
-              Trace.Immediate {location= call_loc; history= []}
+          attrs
-          | Some access_trace ->
+      | Some callee_trace ->
-              access_trace
+          let written_to =
-        in
             Attribute.WrittenTo
               (ViaCall
                  { in_call= callee_trace

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

@@ -1,7 +1,5 @@
 ../../facebook-clang-plugins/clang/install/include/c++/v1/iterator, std::__wrap_iter<A*>::operator++, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function std::__wrap_iter<A*>::operator++,parameter `this` modified here]
 ../../facebook-clang-plugins/clang/install/include/c++/v1/iterator, std::__wrap_iter<int*>::operator++, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function std::__wrap_iter<int*>::operator++,parameter `this` modified here]
-../../facebook-clang-plugins/clang/install/include/c++/v1/iterator, std::operator!=<A_*>, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function std::operator!=<A_*>,when calling `std::operator==<A_*,_A_*>` here,parameter `__x` modified here,when calling `std::operator==<A_*,_A_*>` here,parameter `__y` modified here]
-../../facebook-clang-plugins/clang/install/include/c++/v1/iterator, std::operator!=<int_*>, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function std::operator!=<int_*>,when calling `std::operator==<int_*,_int_*>` here,parameter `__x` modified here,when calling `std::operator==<int_*,_int_*>` here,parameter `__y` modified here]
 codetoanalyze/cpp/impurity/array_test.cpp, alias_mod_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function alias_mod_impure,parameter `array` modified here]
 codetoanalyze/cpp/impurity/array_test.cpp, array_mod_both_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function array_mod_both_impure,parameter `a` modified here]
 codetoanalyze/cpp/impurity/array_test.cpp, array_mod_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function array_mod_impure,parameter `b` modified here,parameter `a` modified here]

infer/tests/codetoanalyze/cpp/impurity/struct_test.cpp

@@ -0,0 +1,13 @@
+/*
+ * 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.
+ */
+struct Foo {
+  int x;
+
+  bool operator<(const Foo& rhs) const { return x < rhs.x; }
+};
+
+void call_lt_pure(Foo& lhs, Foo& rhs) { lhs < rhs; }

infer/tests/codetoanalyze/java/impurity/Localities.java

@@ -174,4 +174,12 @@ class Localities {
     Foo first = get_first_pure(list);
     first.inc_impure();
   }
+
+  public static boolean is_null_pure(Byte a) {
+    return a == null;
+  }
+
+  public static boolean call_is_null_pure(Byte a) {
+    return is_null_pure(a);
+  }
 }