From f86f971497d75a24f3fbad6ab566d461ad318457 Mon Sep 17 00:00:00 2001
From: Sungkeun Cho <scho@fb.com>
Date: Fri, 29 Mar 2019 06:01:35 -0700
Subject: [PATCH] [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  | 17 ++++++++++++++---
 .../src/bufferoverrun/bufferOverrunSemantics.ml |  2 +-
 2 files changed, 15 insertions(+), 4 deletions(-)

diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml
index 0846594ea..b10f8965e 100644
--- a/infer/src/bufferoverrun/bufferOverrunDomain.ml
+++ b/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
diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml
index 90ae73ff6..7fe10334f 100644
--- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml
+++ b/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 :