[inferbo] Conditional proof obligation

Summary:
In order to avoid FPs due to lack of relational info, we apply a heuristic: proof obligations has a latest pruned values,
then it is instantiated at Call statements. If there is a bottom value in the instantiated pruned values, we can say the
program point where the proof obligation is introduced is unreachable with the given parameters of the function.

Depends on D13414441

Reviewed By: mbouaziz

Differential Revision: D13414483

fbshipit-source-id: 61bd34ebb

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -359,8 +359,9 @@ module Report = struct
       Relation.SymExp.of_exp ~get_sym_f:(Sem.get_sym_f integer_type_widths mem) e2
     in
     let relation = Dom.Mem.get_relation mem in
+    let latest_prune = Dom.Mem.get_latest_prune mem in
     BoUtils.Check.array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus ~last_included:false
-      location cond_set
+      ~latest_prune location cond_set
 
 
   let check_binop :
@@ -414,8 +415,9 @@ module Report = struct
         let arr = Sem.eval integer_type_widths exp mem in
         let idx, idx_sym_exp = (Dom.Val.Itv.zero, Some Relation.SymExp.zero) in
         let relation = Dom.Mem.get_relation mem in
+        let latest_prune = Dom.Mem.get_latest_prune mem in
         BoUtils.Check.array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus:true
-          ~last_included:false location cond_set
+          ~last_included:false ~latest_prune location cond_set
     | Exp.BinOp (bop, e1, e2) ->
         check_binop integer_type_widths ~bop ~e1 ~e2 location mem cond_set
     | _ ->
@@ -427,8 +429,9 @@ module Report = struct
     | Binop.PlusA (Some _) | Binop.MinusA (Some _) | Binop.Mult (Some _) ->
         let lhs_v = Sem.eval integer_type_widths lhs mem in
         let rhs_v = Sem.eval integer_type_widths rhs mem in
-        BoUtils.Check.binary_operation integer_type_widths bop ~lhs:lhs_v ~rhs:rhs_v location
-          cond_set
+        let latest_prune = Dom.Mem.get_latest_prune mem in
+        BoUtils.Check.binary_operation integer_type_widths bop ~lhs:lhs_v ~rhs:rhs_v ~latest_prune
+          location cond_set
     | _ ->
         cond_set
 

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -647,7 +647,23 @@ end
 (* [PrunePairs] is a map from abstract locations to abstract values that represents pruned results
    in the latest pruning.  It uses [InvertedMap] because more pruning means smaller abstract
    states. *)
-module PrunePairs = AbstractDomain.InvertedMap (Loc) (Val)
+module PrunePairs = struct
+  include AbstractDomain.InvertedMap (Loc) (Val)
+
+  (* [subst] returns [None] if a pruned value is bottom, i.g., unreachable. *)
+  let subst x eval_sym_trace location =
+    let exception Unreachable in
+    let is_empty_val v =
+      Itv.is_empty (Val.get_itv v)
+      && PowLoc.is_empty (Val.get_pow_loc v)
+      && ArrayBlk.is_empty (Val.get_array_blk v)
+    in
+    let subst1 x =
+      let v = Val.subst x eval_sym_trace location in
+      if is_empty_val v then raise Unreachable else v
+    in
+    match map subst1 x with x -> Some x | exception Unreachable -> None
+end
 
 module LatestPrune = struct
   (* Latest p: The pruned pairs 'p' has pruning information (which
@@ -744,6 +760,21 @@ module LatestPrune = struct
   let widen ~prev ~next ~num_iters:_ = join prev next
 
   let top = Top
+
+  let subst x eval_sym_trace location =
+    match x with
+    | Latest p ->
+        Option.map (PrunePairs.subst p eval_sym_trace location) ~f:(fun p -> Latest p)
+    | TrueBranch (x, p) ->
+        Option.map (PrunePairs.subst p eval_sym_trace location) ~f:(fun p -> TrueBranch (x, p))
+    | FalseBranch (x, p) ->
+        Option.map (PrunePairs.subst p eval_sym_trace location) ~f:(fun p -> FalseBranch (x, p))
+    | V (x, ptrue, pfalse) ->
+        Option.map2 (PrunePairs.subst ptrue eval_sym_trace location)
+          (PrunePairs.subst pfalse eval_sym_trace location) ~f:(fun ptrue pfalse ->
+            V (x, ptrue, pfalse) )
+    | Top ->
+        Some x
 end
 
 module MemReach = struct
@@ -968,6 +999,8 @@ module MemReach = struct
         {m with latest_prune= LatestPrune.Top}
 
 
+  let get_latest_prune : t -> LatestPrune.t = fun {latest_prune} -> latest_prune
+
   let get_reachable_locs_from : (Pvar.t * Typ.t) list -> PowLoc.t -> t -> PowLoc.t =
     let add_reachable1 ~root loc v acc =
       if Loc.equal root loc then PowLoc.union acc (Val.get_all_locs v)
@@ -1132,6 +1165,10 @@ module Mem = struct
    fun e1 e2 -> map ~f:(MemReach.update_latest_prune e1 e2)
 
 
+  let get_latest_prune : t -> LatestPrune.t =
+    f_lift_default ~default:LatestPrune.Top MemReach.get_latest_prune
+
+
   let get_relation : t -> Relation.t =
    fun m -> f_lift_default ~default:Relation.bot MemReach.get_relation m
 

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -64,7 +64,8 @@ let check_alloc_size size_exp {location; integer_type_widths} mem cond_set =
       cond_set
   | NonBottom length ->
       let traces = Dom.Val.get_traces v_length in
-      PO.ConditionSet.add_alloc_size location ~length traces cond_set
+      let latest_prune = Dom.Mem.get_latest_prune mem in
+      PO.ConditionSet.add_alloc_size location ~length traces latest_prune cond_set
 
 
 let malloc size_exp =

infer/src/bufferoverrun/bufferOverrunProofObligations.ml

@@ -672,9 +672,12 @@ end
 
 module ConditionWithTrace = struct
   type 'cond_trace t0 =
-    {cond: Condition.t; trace: 'cond_trace ConditionTrace.t0; reported: Reported.t option}
+    { cond: Condition.t
+    ; trace: 'cond_trace ConditionTrace.t0
+    ; reported: Reported.t option
+    ; latest_prune: Dom.LatestPrune.t }
 
-  let make cond trace = {cond; trace; reported= None}
+  let make cond trace latest_prune = {cond; trace; reported= None; latest_prune}
 
   let pp fmt {cond; trace} = F.fprintf fmt "%a %a" Condition.pp cond ConditionTrace.pp trace
 
@@ -695,26 +698,29 @@ module ConditionWithTrace = struct
         cmp
 
 
-  let subst {Dom.eval_sym; trace_of_sym} rel_map caller_relation callee_pname call_site cwt =
+  let subst ({Dom.eval_sym; trace_of_sym} as eval_sym_trace) rel_map caller_relation callee_pname
+      call_site cwt =
     let symbols = Condition.get_symbols cwt.cond in
     if Symb.SymbolSet.is_empty symbols then
       L.(die InternalError)
         "Trying to substitute a non-symbolic condition %a from %a at %a. Why was it propagated in \
          the first place?"
         pp_summary cwt Typ.Procname.pp callee_pname Location.pp call_site ;
-    match Condition.subst eval_sym rel_map caller_relation cwt.cond with
-    | None ->
-        None
-    | Some cond ->
-        let traces_caller =
-          Symb.SymbolSet.fold
-            (fun symbol val_traces -> ValTrace.Set.join (trace_of_sym symbol) val_traces)
-            symbols ValTrace.Set.empty
-        in
-        let trace =
-          ConditionTrace.make_call_and_subst ~traces_caller ~callee_pname call_site cwt.trace
-        in
-        Some {cond; trace; reported= cwt.reported}
+    Option.find_map (Dom.LatestPrune.subst cwt.latest_prune eval_sym_trace call_site)
+      ~f:(fun latest_prune ->
+        match Condition.subst eval_sym rel_map caller_relation cwt.cond with
+        | None ->
+            None
+        | Some cond ->
+            let traces_caller =
+              Symb.SymbolSet.fold
+                (fun symbol val_traces -> ValTrace.Set.join (trace_of_sym symbol) val_traces)
+                symbols ValTrace.Set.empty
+            in
+            let trace =
+              ConditionTrace.make_call_and_subst ~traces_caller ~callee_pname call_site cwt.trace
+            in
+            Some {cond; trace; reported= cwt.reported; latest_prune} )
 
 
   let set_u5 {cond; trace} issue_type =
@@ -761,8 +767,7 @@ module ConditionWithTrace = struct
 
   let forget_locs locs cwt = {cwt with cond= Condition.forget_locs locs cwt.cond}
 
-  let for_summary {cond; trace; reported} =
-    {cond; trace= ConditionTrace.for_summary trace; reported}
+  let for_summary cwt = {cwt with trace= ConditionTrace.for_summary cwt.trace}
 end
 
 module ConditionSet = struct
@@ -832,35 +837,37 @@ module ConditionSet = struct
 
   let check_one cwt = (cwt, ConditionWithTrace.check cwt)
 
-  let add_opt location val_traces condset = function
+  let add_opt location val_traces latest_prune condset = function
     | None ->
         condset
     | Some cond ->
         let trace = ConditionTrace.make location val_traces in
-        let cwt = ConditionWithTrace.make cond trace in
+        let cwt = ConditionWithTrace.make cond trace latest_prune in
         join_one condset (check_one cwt)
 
 
   let add_array_access location ~offset ~idx ~size ~last_included ~idx_sym_exp ~size_sym_exp
-      ~relation ~idx_traces ~arr_traces condset =
+      ~relation ~idx_traces ~arr_traces ~latest_prune condset =
     ArrayAccessCondition.make ~offset ~idx ~size ~last_included ~idx_sym_exp ~size_sym_exp
       ~relation
     |> Condition.make_array_access
     |> add_opt location
          (ValTrace.Issue.(binary location ArrayAccess) idx_traces arr_traces)
-         condset
+         latest_prune condset
 
 
-  let add_alloc_size location ~length val_traces condset =
+  let add_alloc_size location ~length val_traces latest_prune condset =
     AllocSizeCondition.make ~length |> Condition.make_alloc_size
-    |> add_opt location (ValTrace.Issue.alloc location val_traces) condset
+    |> add_opt location (ValTrace.Issue.alloc location val_traces) latest_prune condset
 
 
   let add_binary_operation integer_type_widths location bop ~lhs ~rhs ~lhs_traces ~rhs_traces
-      condset =
+      ~latest_prune condset =
     BinaryOperationCondition.make integer_type_widths bop ~lhs ~rhs
     |> Condition.make_binary_operation
-    |> add_opt location (ValTrace.Issue.(binary location Binop) lhs_traces rhs_traces) condset
+    |> add_opt location
+         (ValTrace.Issue.(binary location Binop) lhs_traces rhs_traces)
+         latest_prune condset
 
 
   let subst condset eval_sym_trace rel_subst_map caller_relation callee_pname call_site =

infer/src/bufferoverrun/bufferOverrunProofObligations.mli

@@ -46,11 +46,17 @@ module ConditionSet : sig
     -> relation:Relation.t
     -> idx_traces:BufferOverrunTrace.Set.t
     -> arr_traces:BufferOverrunTrace.Set.t
+    -> latest_prune:BufferOverrunDomain.LatestPrune.t
     -> checked_t
     -> checked_t
 
   val add_alloc_size :
-    Location.t -> length:ItvPure.t -> BufferOverrunTrace.Set.t -> checked_t -> checked_t
+       Location.t
+    -> length:ItvPure.t
+    -> BufferOverrunTrace.Set.t
+    -> BufferOverrunDomain.LatestPrune.t
+    -> checked_t
+    -> checked_t
 
   val add_binary_operation :
        Typ.IntegerWidths.t
@@ -60,6 +66,7 @@ module ConditionSet : sig
     -> rhs:ItvPure.t
     -> lhs_traces:BufferOverrunTrace.Set.t
     -> rhs_traces:BufferOverrunTrace.Set.t
+    -> latest_prune:BufferOverrunDomain.LatestPrune.t
     -> checked_t
     -> checked_t
 

infer/src/bufferoverrun/bufferOverrunUtils.ml

@@ -216,7 +216,7 @@ end
 
 module Check = struct
   let check_access ~size ~idx ~size_sym_exp ~idx_sym_exp ~relation ~arr ~idx_traces ~last_included
-      location cond_set =
+      ~latest_prune location cond_set =
     match (size, idx) with
     | NonBottom length, NonBottom idx ->
         let offset =
@@ -229,12 +229,13 @@ module Check = struct
         in
         let arr_traces = Dom.Val.get_traces arr in
         PO.ConditionSet.add_array_access location ~size:length ~offset ~idx ~size_sym_exp
-          ~idx_sym_exp ~relation ~last_included ~idx_traces ~arr_traces cond_set
+          ~idx_sym_exp ~relation ~last_included ~idx_traces ~arr_traces ~latest_prune cond_set
     | _ ->
         cond_set
 
 
-  let array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus ~last_included location cond_set =
+  let array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus ~last_included ~latest_prune location
+      cond_set =
     let arr_blk = Dom.Val.get_array_blk arr in
     let size = ArrayBlk.sizeof arr_blk in
     let size_sym_exp = Relation.SymExp.of_sym (Dom.Val.get_size_sym arr) in
@@ -251,7 +252,7 @@ module Check = struct
       "@[<v 2>Add condition :@,array: %a@,  idx: %a + %a@,@]@." ArrayBlk.pp arr_blk Itv.pp
       (ArrayBlk.offsetof arr_blk) Itv.pp idx ;
     check_access ~size ~idx ~size_sym_exp ~idx_sym_exp ~relation ~arr ~idx_traces ~last_included
-      location cond_set
+      ~latest_prune location cond_set
 
 
   let collection_access integer_type_widths ~array_exp ~index_exp ~last_included mem location
@@ -262,8 +263,9 @@ module Check = struct
     let size = Exec.get_alist_size arr mem |> Dom.Val.get_itv in
     let idx = Dom.Val.get_itv idx in
     let relation = Dom.Mem.get_relation mem in
+    let latest_prune = Dom.Mem.get_latest_prune mem in
     check_access ~size ~idx ~size_sym_exp:None ~idx_sym_exp:None ~relation ~arr ~idx_traces
-      ~last_included location cond_set
+      ~last_included ~latest_prune location cond_set
 
 
   let lindex integer_type_widths ~array_exp ~index_exp ~last_included mem location cond_set =
@@ -273,7 +275,9 @@ module Check = struct
       Relation.SymExp.of_exp ~get_sym_f:(Sem.get_sym_f integer_type_widths mem) index_exp
     in
     let relation = Dom.Mem.get_relation mem in
-    array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus:true ~last_included location cond_set
+    let latest_prune = Dom.Mem.get_latest_prune mem in
+    array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus:true ~last_included ~latest_prune
+      location cond_set
 
 
   let array_access_byte ~arr ~idx ~relation ~is_plus ~last_included location cond_set =
@@ -294,10 +298,12 @@ module Check = struct
     let idx = Sem.eval integer_type_widths byte_index_exp mem in
     let arr = Sem.eval_arr integer_type_widths array_exp mem in
     let relation = Dom.Mem.get_relation mem in
-    array_access_byte ~arr ~idx ~relation ~is_plus:true ~last_included location cond_set
+    let latest_prune = Dom.Mem.get_latest_prune mem in
+    array_access_byte ~arr ~idx ~relation ~is_plus:true ~last_included ~latest_prune location
+      cond_set
 
 
-  let binary_operation integer_type_widths bop ~lhs ~rhs location cond_set =
+  let binary_operation integer_type_widths bop ~lhs ~rhs ~latest_prune location cond_set =
     let lhs_itv = Dom.Val.get_itv lhs in
     let rhs_itv = Dom.Val.get_itv rhs in
     match (lhs_itv, rhs_itv) with
@@ -307,7 +313,7 @@ module Check = struct
           Itv.ItvPure.pp lhs_itv Itv.ItvPure.pp rhs_itv ;
         PO.ConditionSet.add_binary_operation integer_type_widths location bop ~lhs:lhs_itv
           ~rhs:rhs_itv ~lhs_traces:(Dom.Val.get_traces lhs) ~rhs_traces:(Dom.Val.get_traces rhs)
-          cond_set
+          ~latest_prune cond_set
     | _, _ ->
         cond_set
 end

infer/src/bufferoverrun/bufferOverrunUtils.mli

@@ -89,6 +89,7 @@ module Check : sig
     -> relation:Relation.t
     -> is_plus:bool
     -> last_included:bool
+    -> latest_prune:Dom.LatestPrune.t
     -> Location.t
     -> PO.ConditionSet.checked_t
     -> PO.ConditionSet.checked_t
@@ -128,6 +129,7 @@ module Check : sig
     -> Binop.t
     -> lhs:Dom.Val.t
     -> rhs:Dom.Val.t
+    -> latest_prune:Dom.LatestPrune.t
     -> Location.t
     -> PO.ConditionSet.checked_t
     -> PO.ConditionSet.checked_t

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

@@ -110,7 +110,7 @@ void call_conditional_buffer_access3_1_Good() {
   conditional_buffer_access3(a, 2);
 }
 
-void call_conditional_buffer_access3_2_Good_FP() {
+void call_conditional_buffer_access3_2_Good() {
   int a[1];
   a[0] = E_SIZEONE;
   conditional_buffer_access3(a, 1);

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

@@ -30,7 +30,6 @@ codetoanalyze/cpp/bufferoverrun/class.cpp, return_class_Bad, 2, BUFFER_OVERRUN_L
 codetoanalyze/cpp/bufferoverrun/class.cpp, use_global_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 32 Size: 30]
 codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access2_1_Good_FP, 1, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Parameter `n`,Array declaration,Call,<Length trace>,Parameter `*ptr`,Assignment,Assignment,Assignment,Array access: Offset: 3 Size: 1 by call to `conditional_buffer_access2` ]
 codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access2_2_Good_FP, 1, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Parameter `n`,Array declaration,Call,<Length trace>,Parameter `*ptr`,Assignment,Assignment,Assignment,Array access: Offset: 3 Size: 3 by call to `conditional_buffer_access2` ]
-codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access3_2_Good_FP, 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_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,Assignment,Array access: Offset: 3 Size: 1 by call to `conditional_buffer_access` ]
 codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access_Good_FP, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Length trace>,Parameter `*ptr`,Assignment,Assignment,Assignment,Array access: Offset: 3 Size: 1 by call to `conditional_buffer_access` ]