[inferbo] Update reachability conditions at function call

Summary:
This diff updates the reachability conditions of proof obligations at every function calls.

Depends on D13781124

Reviewed By: mbouaziz

Differential Revision: D13781147

fbshipit-source-id: 3c8768bd9

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -260,7 +260,9 @@ let instantiate_cond :
   let eval_sym_trace =
     Sem.mk_eval_sym_trace integer_type_widths callee_formals params caller_mem
   in
+  let latest_prune = Dom.Mem.get_latest_prune caller_mem in
   PO.ConditionSet.subst callee_cond eval_sym_trace rel_subst_map caller_rel callee_pname location
+    latest_prune
 
 
 let check_instr :

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -741,7 +741,10 @@ module CoreVal = struct
 
   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 = Itv.is_symbolic (Val.get_itv v) || ArrayBlk.is_symbolic (Val.get_array_blk v)
+  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)
 end
@@ -999,7 +1002,7 @@ module Reachability = struct
      reachability. *)
   let add v x = if PrunedVal.is_symbolic v then M.add v x else x
 
-  let make latest_prune =
+  let of_latest_prune latest_prune =
     let of_prune_pairs p = PrunePairs.fold (fun _ v acc -> add v acc) p M.empty in
     match latest_prune with
     | LatestPrune.Latest p | LatestPrune.TrueBranch (_, p) | LatestPrune.FalseBranch (_, p) ->
@@ -1010,6 +1013,10 @@ module Reachability = struct
         M.empty
 
 
+  let make latest_prune = of_latest_prune latest_prune
+
+  let add_latest_prune latest_prune x = M.union x (of_latest_prune latest_prune)
+
   let subst x eval_sym_trace location =
     let exception Unreachable in
     let subst1 x acc =

infer/src/bufferoverrun/bufferOverrunProofObligations.ml

@@ -762,6 +762,10 @@ module ConditionWithTrace = struct
         None
 
 
+  let update_reachability latest_prune ({reachability} as cwt) =
+    {cwt with reachability= Dom.Reachability.add_latest_prune latest_prune reachability}
+
+
   let set_u5 {cond; trace} issue_type =
     if
       ( IssueType.equal issue_type IssueType.buffer_overrun_l3
@@ -918,7 +922,8 @@ module ConditionSet = struct
          latest_prune condset
 
 
-  let subst condset eval_sym_trace rel_subst_map caller_relation callee_pname call_site =
+  let subst condset eval_sym_trace rel_subst_map caller_relation callee_pname call_site
+      latest_prune =
     let subst_add_cwt condset cwt =
       match
         ConditionWithTrace.subst eval_sym_trace rel_subst_map caller_relation callee_pname
@@ -927,6 +932,7 @@ module ConditionSet = struct
       | None ->
           condset
       | Some cwt ->
+          let cwt = ConditionWithTrace.update_reachability latest_prune cwt in
           join_one condset (check_one cwt)
     in
     List.fold condset ~f:subst_add_cwt ~init:[]

infer/src/bufferoverrun/bufferOverrunProofObligations.mli

@@ -77,6 +77,7 @@ module ConditionSet : sig
     -> Relation.t
     -> Typ.Procname.t
     -> Location.t
+    -> BufferOverrunDomain.LatestPrune.t
     -> checked_t
 
   val report_errors :

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

@@ -191,7 +191,7 @@ void conditional_inequality_depth1(int i) {
   }
 }
 
-void call_conditional_inequality_depth1_1_Good_FP() {
+void call_conditional_inequality_depth1_1_Good() {
   conditional_inequality_depth1(5);
 }
 

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

@@ -36,7 +36,6 @@ codetoanalyze/cpp/bufferoverrun/class.cpp, use_global_Bad, 2, BUFFER_OVERRUN_L1,
 codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access3_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Offset trace>,Parameter `size`,<Length trace>,Parameter `*ptr`,Array access: Offset: -1 Size: 1 by call to `conditional_buffer_access3` ]
 codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Length trace>,Parameter `*ptr`,Assignment,Assignment,Array access: Offset: 2 Size: 1 by call to `conditional_buffer_access` ]
 codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_inequality_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `idx`,<Length trace>,Array declaration,Array access: Offset: 6 Size: 5 by call to `conditional_inequality` ]
-codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_inequality_depth1_1_Good_FP, 1, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Parameter `i`,Call,<Offset trace>,Parameter `i`,<Length trace>,Array declaration,Array access: Offset: 5 Size: 5 by call to `conditional_inequality_depth1` ]
 codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_inequality_depth1_3_Bad, 1, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Parameter `i`,Call,<Offset trace>,Parameter `i`,<Length trace>,Array declaration,Array access: Offset: 6 Size: 5 by call to `conditional_inequality_depth1` ]
 codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_inequality_join1_Bad, 1, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `idx`,<Length trace>,Array declaration,Array access: Offset: 6 Size: 5 by call to `conditional_inequality_join1` ]
 codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_inequality_join1_Good_FP, 1, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `idx`,<Length trace>,Array declaration,Array access: Offset: 5 Size: 5 by call to `conditional_inequality_join1` ]