From 2091a529b16705cfd57e7a5938b1d84cb0b8950c Mon Sep 17 00:00:00 2001
From: Sungkeun Cho <scho@fb.com>
Date: Mon, 17 Jul 2017 03:02:25 -0700
Subject: [PATCH] [inferbo] Avoid precision loss on pruning

Summary:
This commit avoids precision loss on pruning.

  // x -> [s$1, s$2]
  if(x) { ... }
  // x -> ?

before: x -> [min(0, s$1), max(0, s$2)]
because two x values, [0, 0] (true case) and [s$1, s$2] (false case), were joined after the if branch.

after: x -> [s$1, s$2]

Reviewed By: mbouaziz

Differential Revision: D5431009

fbshipit-source-id: 14a9efe
---
 infer/src/bufferoverrun/bufferOverrunSemantics.ml      | 2 +-
 infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp | 1 -
 infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp | 2 +-
 3 files changed, 2 insertions(+), 3 deletions(-)

diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml
index eb767e0e0..0efc7a649 100644
--- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml
+++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml
@@ -325,7 +325,7 @@ module Make (CFG : ProcCfg.S) = struct
         match Mem.find_alias x mem with
         | Some lv
          -> let v = Mem.find_heap lv mem in
-            let itv_v = if Itv.is_bot (Val.get_itv v) then Itv.bot else Itv.false_sem in
+            let itv_v = Itv.prune_ne (Val.get_itv v) Itv.false_sem in
             let v' = Val.modify_itv itv_v v in
             Mem.update_mem (PowLoc.singleton lv) v' mem
         | None
diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp
index cefb94eaa..d67d76428 100644
--- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp
+++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp
@@ -13,7 +13,6 @@ codetoanalyze/cpp/bufferoverrun/repro1.cpp, it_it, 0, BUFFER_OVERRUN, [ArrayAcce
 codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, instantiate_my_vector_oob_Ok, 3, BUFFER_OVERRUN, [Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [42, 42] Size: [42, 42] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call `my_vector_oob_Bad()` ]
 codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN, [Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [max(0, s$4), s$5] Size: [max(0, s$4), s$5] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call `int_vector_access_at()` ]
 codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [10, 10]]
-codetoanalyze/cpp/bufferoverrun/vector.cpp, call_safe_access2_Good_FP, 2, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [0, 0] @ codetoanalyze/cpp/bufferoverrun/vector.cpp:65:5 by call `safe_access2()` ]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 11, BUFFER_OVERRUN, [Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 0] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN, [Call,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 17, BUFFER_OVERRUN, [Call,Call,Call,Assignment,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 0] Size: [0, +oo]]
diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp
index de8bdbd32..a93309667 100644
--- a/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp
+++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp
@@ -66,7 +66,7 @@ void safe_access2(std::vector<int> v) {
   }
 }
 
-void call_safe_access2_Good_FP() {
+void call_safe_access2_Good() {
   std::vector<int> v;
   safe_access2(v);
 }