[inferbo] Ignore the top of latest prune of callees

Summary:
This diff prevents that the latest prune value is overwritten as top
from callees.

Reviewed By: jvillard

Differential Revision: D16540391

fbshipit-source-id: bdd5b42ed

infer/src/bufferoverrun/bufferOverrunAnalysis.ml

@@ -64,7 +64,11 @@ module TransferFunctions = struct
       |> Dom.LatestPrune.subst ~ret_id eval_sym_trace location
     with
     | Ok latest_prune' ->
-        Dom.Mem.set_latest_prune latest_prune' mem
+        (* Note that we are losing some precisions here, e.g., the best results should be "and" of
+           caller's and callee's pruned conditions.  For now, we defer the implementation of the
+           "and" since we haven't seen a case where "and" would help yet. *)
+        if Dom.LatestPrune.is_top latest_prune' then mem
+        else Dom.Mem.set_latest_prune latest_prune' mem
     | Error `SubstBottom ->
         Dom.Mem.bottom
     | Error `SubstFail ->

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -1121,6 +1121,8 @@ module LatestPrune = struct
 
   let top = Top
 
+  let is_top = function Top -> true | _ -> false
+
   let forget locs =
     let is_mem_locs x = PowLoc.mem (Loc.of_pvar x) locs in
     function

infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp

@@ -202,3 +202,27 @@ void call_conditional_inequality_depth1_2_Good() {
 void call_conditional_inequality_depth1_3_Bad() {
   conditional_inequality_depth1(6);
 }
+
+class MyString {
+  char* _data = "";
+  size_t _size = 0;
+
+ public:
+  size_t size() { return _size; }
+
+  char* data() { return _data; }
+};
+
+void set_fourth_idx(char* p) { p[3] = '0'; }
+
+void set_fourth_idx_safe(MyString* input) {
+  if (input->size() < 4) {
+    return;
+  }
+  set_fourth_idx(input->data());
+}
+
+void call_set_fourth_idx_safe_Good() {
+  MyString* s = new MyString();
+  set_fourth_idx_safe(s);
+}