[inferbo] Prevent deduplication of issues when different conditions

Summary:
This diff prevents deduplications of issues when they have different
conditions to reach.

Reviewed By: mbouaziz

Differential Revision: D13596220

fbshipit-source-id: 95f802edb

infer/src/bufferoverrun/arrayBlk.ml

@@ -127,6 +127,17 @@ module ArrInfo = struct
         F.pp_print_string f SpecialChars.down_tack
 
 
+  let is_symbolic : t -> bool =
+   fun arr ->
+    match arr with
+    | C {offset; size; stride} ->
+        Itv.is_symbolic offset || Itv.is_symbolic size || Itv.is_symbolic stride
+    | Java {length} ->
+        Itv.is_symbolic length
+    | Top ->
+        false
+
+
   let get_symbols : t -> Itv.SymbolSet.t =
    fun arr ->
     match arr with
@@ -235,6 +246,8 @@ end
 
 include AbstractDomain.Map (Allocsite) (ArrInfo)
 
+let compare = compare ArrInfo.compare
+
 let bot : t = empty
 
 let unknown : t = add Allocsite.unknown ArrInfo.top bot
@@ -296,6 +309,8 @@ let subst : t -> Bound.eval_sym -> PowLoc.eval_locpath -> t =
   fold subst1 a empty
 
 
+let is_symbolic : t -> bool = fun a -> exists (fun _ ai -> ArrInfo.is_symbolic ai) a
+
 let get_symbols : t -> Itv.SymbolSet.t =
  fun a ->
   fold (fun _ ai acc -> Itv.SymbolSet.union acc (ArrInfo.get_symbols ai)) a Itv.SymbolSet.empty

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -706,21 +706,6 @@ end
 module PrunePairs = struct
   include AbstractDomain.InvertedMap (Loc) (Val)
 
-  (* [subst] returns [None] if a pruned value is bottom, i.g., unreachable. *)
-  let subst x eval_sym_trace location =
-    let exception Unreachable in
-    let is_empty_val v =
-      Itv.is_empty (Val.get_itv v)
-      && PowLoc.is_empty (Val.get_pow_loc v)
-      && ArrayBlk.is_empty (Val.get_array_blk v)
-    in
-    let subst1 x =
-      let v = Val.subst x eval_sym_trace location in
-      if is_empty_val v then raise Unreachable else v
-    in
-    match map subst1 x with x -> Some x | exception Unreachable -> None
-
-
   let forget locs x = filter (fun l _ -> not (PowLoc.mem l locs)) x
 end
 
@@ -820,22 +805,6 @@ module LatestPrune = struct
 
   let top = Top
 
-  let subst x eval_sym_trace location =
-    match x with
-    | Latest p ->
-        Option.map (PrunePairs.subst p eval_sym_trace location) ~f:(fun p -> Latest p)
-    | TrueBranch (x, p) ->
-        Option.map (PrunePairs.subst p eval_sym_trace location) ~f:(fun p -> TrueBranch (x, p))
-    | FalseBranch (x, p) ->
-        Option.map (PrunePairs.subst p eval_sym_trace location) ~f:(fun p -> FalseBranch (x, p))
-    | V (x, ptrue, pfalse) ->
-        Option.map2 (PrunePairs.subst ptrue eval_sym_trace location)
-          (PrunePairs.subst pfalse eval_sym_trace location) ~f:(fun ptrue pfalse ->
-            V (x, ptrue, pfalse) )
-    | Top ->
-        Some x
-
-
   let forget locs =
     let is_mem_locs x = PowLoc.mem (Loc.of_pvar x) locs in
     function
@@ -852,6 +821,52 @@ module LatestPrune = struct
         Top
 end
 
+module Reachability = struct
+  module PrunedVal = struct
+    type t = Val.t
+
+    let compare x y =
+      let r = Itv.compare (Val.get_itv x) (Val.get_itv y) in
+      if r <> 0 then r else ArrayBlk.compare (Val.get_array_blk x) (Val.get_array_blk y)
+
+
+    let pp = Val.pp
+
+    let is_symbolic : t -> bool = fun x -> Itv.is_symbolic x.itv || ArrayBlk.is_symbolic x.arrayblk
+
+    let is_empty v = Itv.is_empty (Val.get_itv v) && ArrayBlk.is_empty (Val.get_array_blk v)
+  end
+
+  module M = PrettyPrintable.MakePPSet (PrunedVal)
+
+  type t = M.t
+
+  let equal = M.equal
+
+  (* It keeps only symbolic pruned values, because non-symbolic ones are useless to see the
+     reachability. *)
+  let add v x = if PrunedVal.is_symbolic v then M.add v x else x
+
+  let make =
+    let of_prune_pairs p = PrunePairs.fold (fun _ v acc -> add v acc) p M.empty in
+    function
+    | LatestPrune.Latest p | LatestPrune.TrueBranch (_, p) | LatestPrune.FalseBranch (_, p) ->
+        of_prune_pairs p
+    | LatestPrune.V (_, ptrue, pfalse) ->
+        M.inter (of_prune_pairs ptrue) (of_prune_pairs pfalse)
+    | LatestPrune.Top ->
+        M.empty
+
+
+  let subst x eval_sym_trace location =
+    let exception Unreachable in
+    let subst1 x acc =
+      let v = Val.subst x eval_sym_trace location in
+      if PrunedVal.is_empty v then raise Unreachable else add v acc
+    in
+    match M.fold subst1 x M.empty with x -> `Reachable x | exception Unreachable -> `Unreachable
+end
+
 module MemReach = struct
   type t =
     { stack_locs: StackLocs.t

infer/src/bufferoverrun/bufferOverrunProofObligations.ml

@@ -702,9 +702,11 @@ module ConditionWithTrace = struct
     { cond: Condition.t
     ; trace: 'cond_trace ConditionTrace.t0
     ; reported: Reported.t option
-    ; latest_prune: Dom.LatestPrune.t }
+    ; reachability: Dom.Reachability.t }
+
+  let make cond trace latest_prune =
+    {cond; trace; reported= None; reachability= Dom.Reachability.make latest_prune}
 
-  let make cond trace latest_prune = {cond; trace; reported= None; latest_prune}
 
   let pp fmt {cond; trace} = F.fprintf fmt "%a %a" Condition.pp cond ConditionTrace.pp trace
 
@@ -717,12 +719,14 @@ module ConditionWithTrace = struct
   let have_similar_bounds {cond= cond1} {cond= cond2} = Condition.have_similar_bounds cond1 cond2
 
   let xcompare ~lhs ~rhs =
+    if Dom.Reachability.equal lhs.reachability rhs.reachability then
       match Condition.xcompare ~lhs:lhs.cond ~rhs:rhs.cond with
       | `Equal ->
           if ConditionTrace.compare lhs.trace rhs.trace <= 0 then `LeftSubsumesRight
           else `RightSubsumesLeft
       | (`LeftSubsumesRight | `RightSubsumesLeft | `NotComparable) as cmp ->
           cmp
+    else `NotComparable
 
 
   let subst eval_sym_trace rel_map caller_relation callee_pname call_site cwt =
@@ -732,9 +736,8 @@ module ConditionWithTrace = struct
         "Trying to substitute a non-symbolic condition %a from %a at %a. Why was it propagated in \
          the first place?"
         pp_summary cwt Typ.Procname.pp callee_pname Location.pp call_site ;
-    Option.find_map
-      (Dom.LatestPrune.subst cwt.latest_prune (eval_sym_trace ~strict:true) call_site)
-      ~f:(fun latest_prune ->
+    match Dom.Reachability.subst cwt.reachability (eval_sym_trace ~strict:true) call_site with
+    | `Reachable reachability -> (
         let {Dom.eval_sym; trace_of_sym} = eval_sym_trace ~strict:false in
         match Condition.subst eval_sym rel_map caller_relation cwt.cond with
         | None ->
@@ -748,7 +751,9 @@ module ConditionWithTrace = struct
             let trace =
               ConditionTrace.make_call_and_subst ~traces_caller ~callee_pname call_site cwt.trace
             in
-            Some {cond; trace; reported= cwt.reported; latest_prune} )
+            Some {cond; trace; reported= cwt.reported; reachability} )
+    | `Unreachable ->
+        None
 
 
   let set_u5 {cond; trace} issue_type =

infer/src/bufferoverrun/itv.ml

@@ -612,6 +612,8 @@ let subst : t -> Bound.eval_sym -> t =
  fun x eval_sym -> match x with NonBottom x' -> ItvPure.subst x' eval_sym | _ -> x
 
 
+let is_symbolic = bind1bool ItvPure.is_symbolic
+
 let get_symbols : t -> SymbolSet.t = function
   | Bottom ->
       SymbolSet.empty

infer/src/bufferoverrun/itv.mli

@@ -156,6 +156,8 @@ val neg : t -> t
 
 val normalize : t -> t
 
+val is_symbolic : t -> bool
+
 val get_symbols : t -> SymbolSet.t
 
 val eq : t -> t -> bool

infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c

@@ -289,7 +289,7 @@ void call_two_safety_conditions_l1_and_l2_Bad() { two_safety_conditions(10); }
 
 /* issue1 and issue2 are deduplicated since the offset of issue2
    ([10,+oo]) subsumes that of issue1 ([10,10]). */
-void deduplicate_issues_Bad() {
+void deduplicate_issues_1_Bad() {
   int a[10];
   int x = 10;
   a[x] = 0; // issue1: [10,10] < [10,10]
@@ -298,3 +298,15 @@ void deduplicate_issues_Bad() {
     a[x] = 0; // issue2: [10,+oo] < [10,10]
   }
 }
+
+/* issue1 and issue2 are not deduplicated since they have different
+   conditions to reach. */
+void deduplicate_issues_2_Bad(int y) {
+  int a[10];
+  int x = 10;
+  a[x] = 0; // issue1: [10,10] < [10,10]
+  x = unknown_function();
+  if (x >= 10 && y >= 0) {
+    a[x] = 0; // issue2: [10,+oo] < [10,10]
+  }
+}

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

@@ -131,7 +131,9 @@ codetoanalyze/c/bufferoverrun/issue_kinds.c, call_to_alloc_may_be_big2_is_big_Ba
 codetoanalyze/c/bufferoverrun/issue_kinds.c, call_to_alloc_may_be_big2_is_big_Bad, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,<LHS trace>,Parameter `n`,<RHS trace>,Call,Assignment,Assignment,Binary operation: (100000000 + [0, +oo]):signed32 by call to `alloc_may_be_big2_Silenced` ]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, call_two_safety_conditions_l1_and_l2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `n`,<Length trace>,Array declaration,Array access: Offset: 10 Size: 10 by call to `two_safety_conditions` ]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, call_two_safety_conditions_l1_and_l2_Bad, 0, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Call,<Offset trace>,Parameter `n`,<Length trace>,Array declaration,Array access: Offset: [9, 11] Size: 10 by call to `two_safety_conditions` ]
-codetoanalyze/c/bufferoverrun/issue_kinds.c, deduplicate_issues_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Unknown value from: unknown_function,Assignment,<Length trace>,Array declaration,Array access: Offset: [10, +oo] Size: 10]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, deduplicate_issues_1_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Unknown value from: unknown_function,Assignment,<Length trace>,Array declaration,Array access: Offset: [10, +oo] Size: 10]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, deduplicate_issues_2_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, deduplicate_issues_2_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Unknown value from: unknown_function,Assignment,<Length trace>,Array declaration,Array access: Offset: [10, +oo] Size: 10]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_call_to_s2_symbolic_widened_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Assignment,Call,<Offset trace>,Parameter `*n`,Assignment,<Length trace>,Parameter `*n`,Array declaration,Array access: Offset: [1, +oo] Size: 1 by call to `s2_symbolic_widened_Bad` ]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_call_to_s2_symbolic_widened_Bad, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Call,<LHS trace>,Parameter `*n`,Assignment,Binary operation: ([1, +oo] + 1):signed32 by call to `s2_symbolic_widened_Bad` ]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_concrete_overrun_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]