[inferbo] Revise join of LatestPrune

Reviewed By: mbouaziz

Differential Revision: D13449197

fbshipit-source-id: a2913c494

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -727,6 +727,14 @@ module LatestPrune = struct
     | TrueBranch (x', ptrue), FalseBranch (y', pfalse)
       when Pvar.equal x' y' ->
         V (x', ptrue, pfalse)
+    | TrueBranch (x1, ptrue1), V (x2, ptrue2, pfalse)
+    | V (x2, ptrue2, pfalse), TrueBranch (x1, ptrue1)
+      when Pvar.equal x1 x2 ->
+        V (x1, PrunePairs.join ptrue1 ptrue2, pfalse)
+    | FalseBranch (x1, pfalse1), V (x2, ptrue, pfalse2)
+    | V (x2, ptrue, pfalse2), FalseBranch (x1, pfalse1)
+      when Pvar.equal x1 x2 ->
+        V (x1, ptrue, PrunePairs.join pfalse1 pfalse2)
     | V (x1, ptrue1, pfalse1), V (x2, ptrue2, pfalse2) when Pvar.equal x1 x2 ->
         V (x1, PrunePairs.join ptrue1 ptrue2, PrunePairs.join pfalse1 pfalse2)
     | _, _ ->

infer/tests/codetoanalyze/c/bufferoverrun/issues.exp

@@ -197,6 +197,7 @@ codetoanalyze/c/bufferoverrun/pointer_arith.c, pointer_arith_bad, 4, BUFFER_OVER
 codetoanalyze/c/bufferoverrun/prune_alias.c, FP_prune_alias_exp_Ok, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]
 codetoanalyze/c/bufferoverrun/prune_alias.c, bad_if_alias, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]
 codetoanalyze/c/bufferoverrun/prune_alias.c, bad_if_not_alias, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]
+codetoanalyze/c/bufferoverrun/prune_alias.c, call_latest_prune_join_3_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Offset trace>,Parameter `n`,<Length trace>,Parameter `*a`,Array access: Offset: 3 Size: 2 by call to `latest_prune_join` ]
 codetoanalyze/c/bufferoverrun/prune_alias.c, call_prune_arrblk_ne_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,<Length trace>,Parameter `*x`,Array access: Offset: 5 Size: 5 by call to `prune_arrblk_ne` ]
 codetoanalyze/c/bufferoverrun/prune_alias.c, loop_prune2_Good_FP, 8, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Parameter `length`,<Length trace>,Parameter `length`,Array declaration,Array access: Offset: [length - length + 1, length] Size: length]
 codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_and_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]

infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c

@@ -227,3 +227,40 @@ void call_bad_if_not_alias_Bad_AlreadyReported() {
   int x, y;
   bad_if_not_alias(x, y);
 }
+
+int unknown_function();
+
+void latest_prune_join(int* a, int n) {
+  int x;
+  if (unknown_function()) {
+    if (n < 4) {
+      x = 1;
+    } else {
+      x = 0;
+    }
+  } else {
+    if (n < 5) {
+      x = 1;
+    } else {
+      return;
+    }
+  }
+  if (x) {
+    a[n] = 0;
+  }
+}
+
+void call_latest_prune_join_1_Good() {
+  int a[5];
+  latest_prune_join(a, 3);
+}
+
+void call_latest_prune_join_2_Good() {
+  int a[5];
+  latest_prune_join(a, 10);
+}
+
+void call_latest_prune_join_3_Bad() {
+  int a[2];
+  latest_prune_join(a, 3);
+}