[pulse][join] join attributes present on only one side

Summary:
When a value has a certain attribute only on one side of a join, for
join to be a sound over-approximation we sometimes need to keep that
attribute, sometimes discard it, and sometimes weaken it (though that
last step is still TODO).

Reviewed By: skcho

Differential Revision:
D66774189

Privacy Context Container: L1208441

fbshipit-source-id: b6c5b4c7601ef9ba4a8476267d52a4bc601b4b63

infer/src/pulse/PulseJoin.ml

@@ -200,7 +200,59 @@ let join_stacks astate_lhs astate_rhs =
   (join_state, (stack_pre_join, heap_pre_join), (stack_post_join, heap_post_join))
 
 
-let join_one_sided_attribute _attr = (* TODO: weaken the given attribute in most cases *) None
+let join_one_sided_attribute (attr : Attribute.t) =
+  let weaken attr =
+    (* TODO: add weaker versions of some of the attributes so that we can distinguish when we have
+       lost precision on attributes or not (eg the pointer is null in all branches vs null in some
+       branches only. For now let's just pretend we always have the strong version. *)
+    attr
+  in
+  match attr with
+  | AlwaysReachable
+  (* maybe we want to be more forgiving, at least we get a closure to call even if it comes from
+     just one branch? *)
+  | Closure _
+  | CSharpResourceReleased
+  | DictContainConstKeys
+  | HackConstinitCalled
+  | Initialized
+  | JavaResourceReleased
+  (* could move these two to the "keep if one sided" case if this creates too many FPs *)
+  | ReturnedFromUnknown _
+  | UnknownEffect _
+  (* could be more forgiving about one-sided [StaticType] too *)
+  | StaticType _
+  | StdVectorReserve
+  (* harsh, but biased towards reporting more taint errors *)
+  | TaintSanitized _
+  | UnreachableAt _ ->
+      None
+  | Allocated _
+  | AwaitedAwaitable
+  | CopiedInto _
+  | CopiedReturn _
+  | InReportedRetainCycle
+  | LastLookup _
+  | SourceOriginOfCopy _
+  | StdMoved
+  | UsedAsBranchCond _
+  | WrittenTo _ ->
+      Some attr
+  | AddressOfCppTemporary _
+  | AddressOfStackVariable _
+  | ConfigUsage _
+  | DictReadConstKeys _
+  | EndOfCollection
+  | HackBuilder _
+  | Invalid _
+  | MustBeInitialized _
+  | MustBeValid _
+  | MustNotBeTainted _
+  | PropagateTaintFrom _
+  | Tainted _
+  | Uninitialized _ ->
+      Some (weaken attr)
+
 
 let join_two_sided_attribute join_state (attr1 : Attribute.t) (attr2 : Attribute.t) :
     Attribute.t option =

infer/tests/codetoanalyze/c/pulse-join/attributes.c

@@ -0,0 +1,64 @@
+/*
+ * 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.
+ */
+
+// best run with --pulse-max-disjuncts 0 --pulse-over-approximate-reasoning
+
+#include <stdlib.h>
+
+int init_one_branch_only_bad() {
+  int x;
+  if (random()) {
+    x = 42;
+  }
+  return x;
+}
+
+void FN_free_one_branch_only_bad() {
+  int* p = (int*)malloc(sizeof(int));
+  if (random()) {
+    // FN because Invalid is used to represent freed locations and are kept by
+    // joining
+    free(p);
+  }
+}
+
+// FN-ish: suppressed for now because we don't join histories properly
+void FNsuppressed_invalid_one_branch_only_bad() {
+  int* p = NULL;
+  int x = 42;
+  if (random()) {
+    p = &x;
+  }
+  *p = 11;
+}
+
+int* get_maybe_invalid_pointer(int a) {
+  if (a > 0) {
+    int* p = (int*)malloc(sizeof(int));
+    while (!p) {
+    }
+    return p;
+  }
+  return NULL;
+}
+
+void maybe_deref_pointer(int a, int* p) {
+  if (a > 0) {
+    *p = 42;
+  }
+}
+
+// no interproc yet
+void FN_interproc_joined_invalid_deref_bad() {
+  int* p = get_maybe_invalid_pointer(random());
+  maybe_deref_pointer(random(), p);
+}
+
+void interproc_path_sensitive_valid_deref_ok() {
+  int* p = get_maybe_invalid_pointer(10);
+  maybe_deref_pointer(10, p);
+}

infer/tests/codetoanalyze/c/pulse-join/issues.exp

@@ -1,3 +1,5 @@
+codetoanalyze/c/pulse-join/attributes.c, init_one_branch_only_bad, 5, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [variable `x` declared here,read to uninitialized value occurs here]
+codetoanalyze/c/pulse-join/attributes.c, FNsuppressed_invalid_one_branch_only_bad, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** SUPPRESSED ***,source of the null value part of the trace starts here,assigned,is assigned to the null pointer,null pointer dereference part of the trace starts here,invalid access occurs here]
 codetoanalyze/c/pulse-join/formula.c, FP_same_facts_different_branches_ok, 19, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here]
 codetoanalyze/c/pulse-join/formula.c, FP_same_facts_different_branches_ok, 23, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here]
 codetoanalyze/c/pulse-join/join.c, join_valid_invalid_pointers, 1, NULLPTR_DEREFERENCE_LATENT, no_bucket, ERROR, [*** SUPPRESSED ***,source of the null value part of the trace starts here,is assigned to the null pointer,null pointer dereference part of the trace starts here,parameter `p` of join_valid_invalid_pointers,invalid access occurs here]