[inferbo] More reachability checks on pruning

Summary:
It does more reachability checks on prunings. Before the diff, it checked the reachability only by the condition expression of prune commands, but now also uses PrunePairs.

Depends on D14321575

Reviewed By: mbouaziz

Differential Revision: D14321605

fbshipit-source-id: f630de842

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -829,17 +829,26 @@ module CoreVal = struct
 
   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)
+    if r <> 0 then r
+    else
+      let r = PowLoc.compare (Val.get_pow_loc x) (Val.get_pow_loc y) in
+      if r <> 0 then r else ArrayBlk.compare (Val.get_array_blk x) (Val.get_array_blk y)
+
 
+  let pp fmt x =
+    F.fprintf fmt "(%a, %a, %a)" Itv.pp (Val.get_itv x) PowLoc.pp (Val.get_pow_loc x) ArrayBlk.pp
+      (Val.get_array_blk x)
 
-  let pp fmt x = F.fprintf fmt "(%a, %a)" Itv.pp (Val.get_itv x) ArrayBlk.pp (Val.get_array_blk x)
 
   let is_symbolic v =
     let itv = Val.get_itv v in
     if Itv.is_bottom itv then ArrayBlk.is_symbolic (Val.get_array_blk v) else Itv.is_symbolic itv
 
 
-  let is_empty v = Itv.is_bottom (Val.get_itv v) && ArrayBlk.is_empty (Val.get_array_blk v)
+  let is_empty v =
+    Itv.is_bottom (Val.get_itv v)
+    && PowLoc.is_empty (Val.get_pow_loc v)
+    && ArrayBlk.is_empty (Val.get_array_blk v)
 end
 
 module PruningExp = struct
@@ -968,6 +977,8 @@ module PrunePairs = struct
   include AbstractDomain.InvertedMap (Loc) (PrunedVal)
 
   let forget locs x = filter (fun l _ -> not (PowLoc.mem l locs)) x
+
+  let is_reachable x = not (exists (fun _ v -> PrunedVal.is_empty v) x)
 end
 
 module LatestPrune = struct

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -664,7 +664,7 @@ module Prune = struct
       Mem.meet_constraints constrs mem
     in
     let {mem; prune_pairs} = prune_helper integer_type_widths e {mem; prune_pairs} in
-    Mem.set_prune_pairs prune_pairs mem
+    if PrunePairs.is_reachable prune_pairs then Mem.set_prune_pairs prune_pairs mem else Mem.bot
 end
 
 let get_matching_pairs :