[inferbo] Fix performance of issue deduplication

Reviewed By: mbouaziz

Differential Revision: D13151692

fbshipit-source-id: 62bb0a932

infer/src/IR/Typ.ml

@@ -15,6 +15,7 @@ module F = Format
 
 module IntegerWidths = struct
   type t = {char_width: int; short_width: int; int_width: int; long_width: int; longlong_width: int}
+  [@@deriving compare]
 
   let java = {char_width= 16; short_width= 16; int_width= 32; long_width= 64; longlong_width= 64}
 

infer/src/IR/Typ.mli

@@ -13,6 +13,7 @@ module F = Format
 
 module IntegerWidths : sig
   type t = {char_width: int; short_width: int; int_width: int; long_width: int; longlong_width: int}
+  [@@deriving compare]
 
   val java : t
 

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -481,8 +481,8 @@ module Report = struct
       -> e2:Exp.t
       -> Location.t
       -> Dom.Mem.t
-      -> PO.ConditionSet.t
-      -> PO.ConditionSet.t =
+      -> PO.ConditionSet.checked_t
+      -> PO.ConditionSet.checked_t =
    fun integer_type_widths ~is_plus ~e1 ~e2 location mem cond_set ->
     let arr = Sem.eval integer_type_widths e1 mem in
     let idx = Sem.eval integer_type_widths e2 mem in
@@ -501,8 +501,8 @@ module Report = struct
       -> e2:Exp.t
       -> Location.t
       -> Dom.Mem.t
-      -> PO.ConditionSet.t
-      -> PO.ConditionSet.t =
+      -> PO.ConditionSet.checked_t
+      -> PO.ConditionSet.checked_t =
    fun integer_type_widths ~bop ~e1 ~e2 location mem cond_set ->
     match bop with
     | Binop.PlusPI ->
@@ -518,8 +518,8 @@ module Report = struct
       -> Exp.t
       -> Location.t
       -> Dom.Mem.t
-      -> PO.ConditionSet.t
-      -> PO.ConditionSet.t =
+      -> PO.ConditionSet.checked_t
+      -> PO.ConditionSet.checked_t =
    fun integer_type_widths exp location mem cond_set ->
     let rec check_sub_expr exp cond_set =
       match exp with
@@ -596,7 +596,7 @@ module Report = struct
       -> Dom.Mem.t
       -> Payload.t
       -> Location.t
-      -> PO.ConditionSet.t =
+      -> PO.ConditionSet.checked_t =
    fun tenv integer_type_widths callee_pdesc params caller_mem summary location ->
     let callee_exit_mem = BufferOverrunSummary.get_output summary in
     let callee_cond = BufferOverrunSummary.get_cond_set summary in
@@ -619,8 +619,8 @@ module Report = struct
       -> CFG.Node.t
       -> Sil.instr
       -> Dom.Mem.t
-      -> PO.ConditionSet.t
-      -> PO.ConditionSet.t =
+      -> PO.ConditionSet.checked_t
+      -> PO.ConditionSet.checked_t =
    fun pdesc tenv integer_type_widths symbol_table node instr mem cond_set ->
     match instr with
     | Sil.Load (_, exp, _, location) ->
@@ -663,7 +663,7 @@ module Report = struct
         cond_set
 
 
-  let print_debug_info : Sil.instr -> Dom.Mem.t -> PO.ConditionSet.t -> unit =
+  let print_debug_info : Sil.instr -> Dom.Mem.t -> PO.ConditionSet.checked_t -> unit =
    fun instr pre cond_set ->
     L.(debug BufferOverrun Verbose) "@\n@\n================================@\n" ;
     L.(debug BufferOverrun Verbose) "@[<v 2>Pre-state : @,%a" Dom.Mem.pp pre ;
@@ -683,8 +683,8 @@ module Report = struct
       -> CFG.Node.t
       -> Instrs.not_reversed_t
       -> Dom.Mem.t AbstractInterpreter.State.t
-      -> PO.ConditionSet.t
-      -> PO.ConditionSet.t =
+      -> PO.ConditionSet.checked_t
+      -> PO.ConditionSet.checked_t =
    fun summary pdesc tenv integer_type_widths symbol_table cfg node instrs state cond_set ->
     match state with
     | _ when Instrs.is_empty instrs ->
@@ -717,9 +717,9 @@ module Report = struct
       -> Itv.SymbolTable.t
       -> CFG.t
       -> Analyzer.invariant_map
-      -> PO.ConditionSet.t
+      -> PO.ConditionSet.checked_t
       -> CFG.Node.t
-      -> PO.ConditionSet.t =
+      -> PO.ConditionSet.checked_t =
    fun summary pdesc tenv integer_type_widths symbol_table cfg inv_map cond_set node ->
     match Analyzer.extract_state (CFG.Node.id node) inv_map with
     | Some state ->
@@ -738,14 +738,14 @@ module Report = struct
       -> Itv.SymbolTable.t
       -> CFG.t
       -> Analyzer.invariant_map
-      -> PO.ConditionSet.t =
+      -> PO.ConditionSet.checked_t =
    fun summary pdesc tenv integer_type_widths symbol_table cfg inv_map ->
     CFG.fold_nodes cfg
       ~f:(check_node summary pdesc tenv integer_type_widths symbol_table cfg inv_map)
       ~init:PO.ConditionSet.empty
 
 
-  let report_errors : Summary.t -> PO.ConditionSet.t -> PO.ConditionSet.t =
+  let report_errors : Summary.t -> PO.ConditionSet.checked_t -> PO.ConditionSet.t =
    fun summary cond_set ->
     let report cond trace issue_type =
       let location = PO.ConditionTrace.get_report_location trace in

infer/src/bufferoverrun/bufferOverrunChecker.mli

@@ -9,8 +9,6 @@ open! IStd
 
 val checker : Callbacks.proc_callback_t
 
-module Payload : SummaryPayload.S with type t = BufferOverrunSummary.t
-
 module CFG = ProcCfg.NormalOneInstrPerNode
 
 type invariant_map

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -30,7 +30,7 @@ let mk_model_env pname node_hash location tenv integer_type_widths symbol_table
 
 type exec_fun = model_env -> ret:Ident.t * Typ.t -> Dom.Mem.t -> Dom.Mem.t
 
-type check_fun = model_env -> Dom.Mem.t -> PO.ConditionSet.t -> PO.ConditionSet.t
+type check_fun = model_env -> Dom.Mem.t -> PO.ConditionSet.checked_t -> PO.ConditionSet.checked_t
 
 type model = {exec: exec_fun; check: check_fun}
 

infer/src/bufferoverrun/bufferOverrunProofObligations.ml

@@ -15,10 +15,12 @@ module MF = MarkupFormatter
 module Relation = BufferOverrunDomainRelation
 module ValTrace = BufferOverrunTrace
 
-type checked_condition = {report_issue_type: IssueType.t option; propagate: bool}
+type report_issue_type = NotIssue | Issue of IssueType.t | SymbolicIssue
+
+type checked_condition = {report_issue_type: report_issue_type; propagate: bool}
 
 module AllocSizeCondition = struct
-  type t = ItvPure.t
+  type t = ItvPure.t [@@deriving compare]
 
   let get_symbols = ItvPure.get_symbols
 
@@ -66,23 +68,23 @@ module AllocSizeCondition = struct
   let check length =
     match ItvPure.xcompare ~lhs:length ~rhs:ItvPure.zero with
     | `Equal | `RightSubsumesLeft ->
-        {report_issue_type= Some IssueType.inferbo_alloc_is_zero; propagate= false}
+        {report_issue_type= Issue IssueType.inferbo_alloc_is_zero; propagate= false}
     | `LeftSmallerThanRight ->
-        {report_issue_type= Some IssueType.inferbo_alloc_is_negative; propagate= false}
+        {report_issue_type= Issue IssueType.inferbo_alloc_is_negative; propagate= false}
     | _ -> (
         let is_symbolic = ItvPure.is_symbolic length in
         match ItvPure.xcompare ~lhs:length ~rhs:ItvPure.mone with
         | `Equal | `LeftSmallerThanRight | `RightSubsumesLeft ->
-            {report_issue_type= Some IssueType.inferbo_alloc_is_negative; propagate= false}
+            {report_issue_type= Issue IssueType.inferbo_alloc_is_negative; propagate= false}
         | `LeftSubsumesRight when Bound.is_not_infty (ItvPure.lb length) ->
-            { report_issue_type= Some IssueType.inferbo_alloc_may_be_negative
+            { report_issue_type= Issue IssueType.inferbo_alloc_may_be_negative
             ; propagate= is_symbolic }
         | cmp_mone -> (
           match ItvPure.xcompare ~lhs:length ~rhs:itv_big with
           | `Equal | `RightSmallerThanLeft | `RightSubsumesLeft ->
-              {report_issue_type= Some IssueType.inferbo_alloc_is_big; propagate= false}
+              {report_issue_type= Issue IssueType.inferbo_alloc_is_big; propagate= false}
           | `LeftSubsumesRight when Bound.is_not_infty (ItvPure.ub length) ->
-              {report_issue_type= Some IssueType.inferbo_alloc_may_be_big; propagate= is_symbolic}
+              {report_issue_type= Issue IssueType.inferbo_alloc_may_be_big; propagate= is_symbolic}
           | cmp_big ->
               let propagate =
                 match (cmp_mone, cmp_big) with
@@ -92,7 +94,8 @@ module AllocSizeCondition = struct
                 | _ ->
                     false
               in
-              {report_issue_type= None; propagate} ) )
+              if propagate then {report_issue_type= SymbolicIssue; propagate}
+              else {report_issue_type= NotIssue; propagate} ) )
 
 
   let subst eval_sym length =
@@ -277,27 +280,27 @@ module ArrayAccessCondition = struct
     in
     (* il >= 0 and iu < sl, definitely not an error *)
     if Boolean.is_true not_overrun && Boolean.is_true not_underrun then
-      {report_issue_type= None; propagate= false} (* iu < 0 or il >= su, definitely an error *)
+      {report_issue_type= NotIssue; propagate= false} (* iu < 0 or il >= su, definitely an error *)
     else if Boolean.is_false not_overrun || Boolean.is_false not_underrun then
-      {report_issue_type= Some IssueType.buffer_overrun_l1; propagate= false}
+      {report_issue_type= Issue IssueType.buffer_overrun_l1; propagate= false}
       (* su <= iu < +oo, most probably an error *)
     else if
       Bound.is_not_infty (ItvPure.ub real_idx) && Bound.le (ItvPure.ub size) (ItvPure.ub real_idx)
-    then {report_issue_type= Some IssueType.buffer_overrun_l2; propagate= false}
+    then {report_issue_type= Issue IssueType.buffer_overrun_l2; propagate= false}
       (* symbolic il >= sl, probably an error *)
     else if
       Bound.is_symbolic (ItvPure.lb real_idx) && Bound.le (ItvPure.lb size) (ItvPure.lb real_idx)
-    then {report_issue_type= Some IssueType.buffer_overrun_s2; propagate= true}
+    then {report_issue_type= Issue IssueType.buffer_overrun_s2; propagate= true}
     else
       (* other symbolic bounds are probably too noisy *)
       let is_symbolic =
         ItvPure.is_symbolic c.offset || ItvPure.is_symbolic c.idx || ItvPure.is_symbolic size
       in
       let report_issue_type =
-        if Config.bo_debug <= 3 && is_symbolic then None
-        else if filter1 ~real_idx c then Some IssueType.buffer_overrun_l5
-        else if filter2 ~real_idx c then Some IssueType.buffer_overrun_l4
-        else Some IssueType.buffer_overrun_l3
+        if Config.bo_debug <= 3 && is_symbolic then SymbolicIssue
+        else if filter1 ~real_idx c then Issue IssueType.buffer_overrun_l5
+        else if filter2 ~real_idx c then Issue IssueType.buffer_overrun_l4
+        else Issue IssueType.buffer_overrun_l3
       in
       {report_issue_type; propagate= is_symbolic}
 
@@ -340,6 +343,7 @@ module BinaryOperationCondition = struct
     ; integer_widths: Typ.IntegerWidths.t
     ; lhs: ItvPure.t
     ; rhs: ItvPure.t }
+  [@@deriving compare]
 
   let get_symbols c = Symb.SymbolSet.union (ItvPure.get_symbols c.lhs) (ItvPure.get_symbols c.rhs)
 
@@ -431,7 +435,7 @@ module BinaryOperationCondition = struct
 
 
   let check ({binop; typ; integer_widths; lhs; rhs} as c) =
-    if is_mult_one binop lhs rhs then {report_issue_type= None; propagate= false}
+    if is_mult_one binop lhs rhs then {report_issue_type= NotIssue; propagate= false}
     else
       let v =
         match binop with
@@ -452,20 +456,21 @@ module BinaryOperationCondition = struct
         (* typ_lb <= v_lb and v_ub <= typ_ub, not an error *)
         ((not check_underflow) || Bound.le typ_lb v_lb)
         && ((not check_overflow) || Bound.le v_ub typ_ub)
-      then {report_issue_type= None; propagate= false}
+      then {report_issue_type= NotIssue; propagate= false}
       else if
         (* v_ub < typ_lb or typ_ub < v_lb, definitely an error *)
         (check_underflow && Bound.lt v_ub typ_lb) || (check_overflow && Bound.lt typ_ub v_lb)
-      then {report_issue_type= Some IssueType.integer_overflow_l1; propagate= false}
+      then {report_issue_type= Issue IssueType.integer_overflow_l1; propagate= false}
       else if
         (* -oo != v_lb < typ_lb or typ_ub < v_ub != +oo, probably an error *)
         (check_underflow && Bound.lt v_lb typ_lb && Bound.is_not_infty v_lb)
         || (check_overflow && Bound.lt typ_ub v_ub && Bound.is_not_infty v_ub)
-      then {report_issue_type= Some IssueType.integer_overflow_l2; propagate= false}
+      then {report_issue_type= Issue IssueType.integer_overflow_l2; propagate= false}
       else
         let is_symbolic = ItvPure.is_symbolic v in
         let report_issue_type =
-          if Config.bo_debug <= 3 && is_symbolic then None else Some IssueType.integer_overflow_l5
+          if Config.bo_debug <= 3 && is_symbolic then SymbolicIssue
+          else Issue IssueType.integer_overflow_l5
         in
         {report_issue_type; propagate= is_symbolic}
 
@@ -493,6 +498,9 @@ module Condition = struct
     | AllocSize of AllocSizeCondition.t
     | ArrayAccess of ArrayAccessCondition.t
     | BinaryOperation of BinaryOperationCondition.t
+  [@@deriving compare]
+
+  let equal = [%compare.equal: t]
 
   let make_alloc_size = Option.map ~f:(fun c -> AllocSize c)
 
@@ -673,6 +681,8 @@ module ConditionWithTrace = struct
     F.fprintf fmt "%a %a" Condition.pp cond ConditionTrace.pp_summary trace
 
 
+  let have_same_bounds {cond= cond1} {cond= cond2} = Condition.equal cond1 cond2
+
   let have_similar_bounds {cond= cond1} {cond= cond2} = Condition.have_similar_bounds cond1 cond2
 
   let xcompare ~lhs ~rhs =
@@ -718,34 +728,34 @@ module ConditionWithTrace = struct
     else issue_type
 
 
-  let check_aux cwt =
+  let check cwt =
     let ({report_issue_type; propagate} as checked) = Condition.check cwt.cond in
     match report_issue_type with
-    | None ->
+    | NotIssue | SymbolicIssue ->
         checked
-    | Some issue_type ->
+    | Issue issue_type ->
         let issue_type = set_u5 cwt issue_type in
         (* Only report if the precision has improved.
         This is approximated by: only report if the issue_type has changed. *)
         let report_issue_type =
           match cwt.reported with
           | Some reported when Reported.equal reported issue_type ->
-              (* already reported and the precision hasn't improved *) None
+              (* already reported and the precision hasn't improved *) SymbolicIssue
           | _ ->
               (* either never reported or already reported but the precision has improved *)
-              Some issue_type
+              Issue issue_type
         in
         {report_issue_type; propagate}
 
 
-  let check ~report cwt =
-    let {report_issue_type; propagate} = check_aux cwt in
-    match report_issue_type with
-    | Some issue_type ->
+  let report ~report ((cwt, checked) as default) =
+    match checked.report_issue_type with
+    | NotIssue | SymbolicIssue ->
+        default
+    | Issue issue_type ->
         report cwt.cond cwt.trace issue_type ;
-        if propagate then Some {cwt with reported= Some (Reported.make issue_type)} else None
-    | None ->
-        Option.some_if propagate cwt
+        if checked.propagate then ({cwt with reported= Some (Reported.make issue_type)}, checked)
+        else default
 
 
   let forget_locs locs cwt = {cwt with cond= Condition.forget_locs locs cwt.cond}
@@ -759,54 +769,67 @@ module ConditionSet = struct
 
   type t = ConditionTrace.intra_cond_trace t0
 
+  type checked_t = (ConditionTrace.intra_cond_trace ConditionWithTrace.t0 * checked_condition) list
+
   type summary_t = unit t0
 
   (* invariant: join_one of one of the elements should return the original list *)
 
   let empty = []
 
-  let try_merge ~existing ~new_ =
+  let try_merge ~existing:(existing_cwt, existing_checked) ~new_:(new_cwt, new_checked) =
     (* we don't want to remove issues that would end up in a higher bucket,
      e.g. [a, b] < [c, d] is subsumed by [a, +oo] < [c, d] but the latter is less precise *)
-    if ConditionWithTrace.have_similar_bounds existing new_ then
-      match ConditionWithTrace.xcompare ~lhs:existing ~rhs:new_ with
+    let try_deduplicate () =
+      match ConditionWithTrace.xcompare ~lhs:existing_cwt ~rhs:new_cwt with
       | `LeftSubsumesRight ->
           `DoNotAddAndStop
       | `RightSubsumesLeft ->
           `RemoveExistingAndContinue
       | `NotComparable ->
           `KeepExistingAndContinue
-    else `KeepExistingAndContinue
+    in
+    match (existing_checked.report_issue_type, new_checked.report_issue_type) with
+    | _, NotIssue ->
+        `DoNotAddAndStop
+    | SymbolicIssue, SymbolicIssue when ConditionWithTrace.have_same_bounds existing_cwt new_cwt ->
+        try_deduplicate ()
+    | Issue existing_issue_type, Issue new_issue_type
+      when IssueType.equal existing_issue_type new_issue_type
+           && ConditionWithTrace.have_similar_bounds existing_cwt new_cwt ->
+        try_deduplicate ()
+    | _, _ ->
+        `KeepExistingAndContinue
 
 
   let join_one condset new_ =
-    let rec aux ~new_ acc ~same = function
+    let pp_cond fmt (cond, _) = ConditionWithTrace.pp fmt cond in
+    let rec aux acc ~same = function
       | [] ->
           if Config.bo_debug >= 3 then
-            L.(debug BufferOverrun Verbose)
-              "[InferboPO] Adding new condition %a@." ConditionWithTrace.pp new_ ;
+            L.d_printfln "[InferboPO] Adding new condition %a@." pp_cond new_ ;
           if same then new_ :: condset else new_ :: acc
       | existing :: rest as existings -> (
         match try_merge ~existing ~new_ with
         | `DoNotAddAndStop ->
             if Config.bo_debug >= 3 then
-              L.(debug BufferOverrun Verbose)
-                "[InferboPO] Not adding condition %a (because of existing %a)@."
-                ConditionWithTrace.pp new_ ConditionWithTrace.pp existing ;
+              L.d_printfln "[InferboPO] Not adding condition %a (because of existing %a)@." pp_cond
+                new_ pp_cond existing ;
             if same then condset else List.rev_append acc existings
         | `RemoveExistingAndContinue ->
             if Config.bo_debug >= 3 then
-              L.(debug BufferOverrun Verbose)
-                "[InferboPO] Removing condition %a (because of new %a)@." ConditionWithTrace.pp
-                existing ConditionWithTrace.pp new_ ;
-            aux ~new_ acc ~same:false rest
+              L.d_printfln "[InferboPO] Removing condition %a (because of new %a)@." pp_cond
+                existing pp_cond new_ ;
+            aux acc ~same:false rest
         | `KeepExistingAndContinue ->
-            aux ~new_ (existing :: acc) ~same rest )
+            aux (existing :: acc) ~same rest )
     in
-    aux ~new_ [] ~same:true condset
+    aux [] ~same:true condset
+
 
+  let join condset1 condset2 = List.fold condset2 ~init:condset1 ~f:join_one
 
-  let join condset1 condset2 = List.fold_left ~f:join_one condset1 ~init:condset2
+  let check_one cwt = (cwt, ConditionWithTrace.check cwt)
 
   let add_opt location val_traces condset = function
     | None ->
@@ -814,7 +837,7 @@ module ConditionSet = struct
     | Some cond ->
         let trace = ConditionTrace.make location val_traces in
         let cwt = ConditionWithTrace.make cond trace in
-        join [cwt] condset
+        join_one condset (check_one cwt)
 
 
   let add_array_access location ~offset ~idx ~size ~last_included ~idx_sym_exp ~size_sym_exp
@@ -848,12 +871,16 @@ module ConditionSet = struct
       | None ->
           condset
       | Some cwt ->
-          join_one condset cwt
+          join_one condset (check_one cwt)
     in
     List.fold condset ~f:subst_add_cwt ~init:[]
 
 
-  let check_all ~report condset = List.filter_map condset ~f:(ConditionWithTrace.check ~report)
+  let check_all ~report condset =
+    condset
+    |> List.map ~f:(ConditionWithTrace.report ~report)
+    |> List.filter_map ~f:(fun (cwt, {propagate}) -> Option.some_if propagate cwt)
+
 
   let pp_summary : F.formatter -> _ t0 -> unit =
    fun fmt condset ->
@@ -865,11 +892,12 @@ module ConditionSet = struct
     F.fprintf fmt "@]"
 
 
-  let pp : Format.formatter -> t -> unit =
+  let pp : Format.formatter -> checked_t -> unit =
    fun fmt condset ->
     let pp_sep fmt () = F.fprintf fmt ",@;" in
+    let pp_elem fmt (x, _) = ConditionWithTrace.pp fmt x in
     F.fprintf fmt "Safety conditions:@;@[<hov 2>{ %a }@]"
-      (IList.pp_print_list ~max:30 ~pp_sep ConditionWithTrace.pp)
+      (IList.pp_print_list ~max:30 ~pp_sep pp_elem)
       condset
 
 

infer/src/bufferoverrun/bufferOverrunProofObligations.mli

@@ -25,11 +25,13 @@ end
 module ConditionSet : sig
   type t
 
+  type checked_t
+
   type summary_t
 
-  val empty : t
+  val empty : checked_t
 
-  val pp : Format.formatter -> t -> unit
+  val pp : Format.formatter -> checked_t -> unit
 
   val pp_summary : Format.formatter -> summary_t -> unit
 
@@ -44,10 +46,11 @@ module ConditionSet : sig
     -> relation:Relation.t
     -> idx_traces:BufferOverrunTrace.Set.t
     -> arr_traces:BufferOverrunTrace.Set.t
-    -> t
-    -> t
+    -> checked_t
+    -> checked_t
 
-  val add_alloc_size : Location.t -> length:ItvPure.t -> BufferOverrunTrace.Set.t -> t -> t
+  val add_alloc_size :
+    Location.t -> length:ItvPure.t -> BufferOverrunTrace.Set.t -> checked_t -> checked_t
 
   val add_binary_operation :
        Typ.IntegerWidths.t
@@ -57,10 +60,10 @@ module ConditionSet : sig
     -> rhs:ItvPure.t
     -> lhs_traces:BufferOverrunTrace.Set.t
     -> rhs_traces:BufferOverrunTrace.Set.t
-    -> t
-    -> t
+    -> checked_t
+    -> checked_t
 
-  val join : t -> t -> t
+  val join : checked_t -> checked_t -> checked_t
 
   val subst :
        summary_t
@@ -69,9 +72,9 @@ module ConditionSet : sig
     -> Relation.t
     -> Typ.Procname.t
     -> Location.t
-    -> t
+    -> checked_t
 
-  val check_all : report:(Condition.t -> ConditionTrace.t -> IssueType.t -> unit) -> t -> t
+  val check_all : report:(Condition.t -> ConditionTrace.t -> IssueType.t -> unit) -> checked_t -> t
   (** Check the conditions, call [report] on those that trigger an issue, returns those that needs to be propagated to callers. *)
 
   val for_summary : t -> summary_t

infer/src/bufferoverrun/bufferOverrunUtils.mli

@@ -136,8 +136,8 @@ module Check : sig
     -> is_plus:bool
     -> last_included:bool
     -> Location.t
-    -> PO.ConditionSet.t
-    -> PO.ConditionSet.t
+    -> PO.ConditionSet.checked_t
+    -> PO.ConditionSet.checked_t
 
   val lindex :
        Typ.IntegerWidths.t
@@ -146,8 +146,8 @@ module Check : sig
     -> last_included:bool
     -> Dom.Mem.t
     -> Location.t
-    -> PO.ConditionSet.t
-    -> PO.ConditionSet.t
+    -> PO.ConditionSet.checked_t
+    -> PO.ConditionSet.checked_t
 
   val lindex_byte :
        Typ.IntegerWidths.t
@@ -156,8 +156,8 @@ module Check : sig
     -> last_included:bool
     -> Dom.Mem.t
     -> Location.t
-    -> PO.ConditionSet.t
-    -> PO.ConditionSet.t
+    -> PO.ConditionSet.checked_t
+    -> PO.ConditionSet.checked_t
 
   val collection_access :
        Typ.IntegerWidths.t
@@ -166,8 +166,8 @@ module Check : sig
     -> last_included:bool
     -> Dom.Mem.t
     -> Location.t
-    -> PO.ConditionSet.t
-    -> PO.ConditionSet.t
+    -> PO.ConditionSet.checked_t
+    -> PO.ConditionSet.checked_t
 
   val binary_operation :
        Typ.IntegerWidths.t
@@ -175,6 +175,6 @@ module Check : sig
     -> lhs:Dom.Val.t
     -> rhs:Dom.Val.t
     -> Location.t
-    -> PO.ConditionSet.t
-    -> PO.ConditionSet.t
+    -> PO.ConditionSet.checked_t
+    -> PO.ConditionSet.checked_t
 end

infer/tests/codetoanalyze/c/bufferoverrun/arith.c

@@ -335,6 +335,35 @@ void minmax_div_const2_Bad_FN() {
   div_const2(-2);
 }
 
+uint32_t unknown_nat() {
+  uint32_t x = unknown_function();
+  if (x >= 0) {
+    return x;
+  } else {
+    return 0;
+  }
+}
+
+void two_safety_conditions2_Bad(uint32_t s) {
+  uint32_t x = unknown_nat();
+  uint32_t y, z;
+
+  if (unknown_function()) {
+    y = 0;
+  } else {
+    y = 80;
+  }
+  z = x + y; // integer overflow L5: [0, +oo] + [0, 80]
+
+  if (s >= 10 && s <= 20) {
+    z = x + s; // [0, +oo] + [max(10, s.lb), min(20, s.ub)]
+  }
+}
+
+void call_two_safety_conditions2_Bad() {
+  two_safety_conditions2_Bad(15); // integer overflow L5: [0, +oo] + 15
+}
+
 void band_positive_constant_Good() {
   char a[3];
   int x = 6 & 2; // y is 2

infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c

@@ -242,6 +242,27 @@ void False_Issue_Type_l3_unknown_function_Bad() {
   }
 }
 
+int mone_to_one() {
+  int x = unknown_function();
+  if (x >= -1 && x <= 1) {
+    return x;
+  } else {
+    return 0;
+  }
+}
+
+void two_safety_conditions(int n) {
+  char a[10];
+  int y = mone_to_one();
+  if (unknown_function()) {
+    a[n] = 0; // should be L1 when n=10
+  } else {
+    a[n + y] = 0; // should be L2 when n=10
+  }
+}
+
+void call_two_safety_conditions_l1_and_l2_Bad() { two_safety_conditions(10); }
+
 /* issue1 and issue2 are deduplicated since the offset of issue2
    ([10,+oo]) subsumes that of issue1 ([10,10]). */
 void deduplicate_issues_Bad() {

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

@@ -1,9 +1,9 @@
 codetoanalyze/c/bufferoverrun/arith.c, band_constant_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]
 codetoanalyze/c/bufferoverrun/arith.c, band_negative_Bad, 8, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Unknown value from: unknown_function,Assignment,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 2] Size: 2]
 codetoanalyze/c/bufferoverrun/arith.c, band_negative_constant_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]
-codetoanalyze/c/bufferoverrun/arith.c, band_positive_Bad, 6, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Offset trace>,Unknown value from: unknown_nat,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 5]
-codetoanalyze/c/bufferoverrun/arith.c, band_positive_Good, 6, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Offset trace>,Unknown value from: unknown_nat,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 9]
+codetoanalyze/c/bufferoverrun/arith.c, band_positive_Bad, 6, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Call,Assignment,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 8] Size: 5]
 codetoanalyze/c/bufferoverrun/arith.c, band_positive_constant_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 2 Size: 2]
+codetoanalyze/c/bufferoverrun/arith.c, call_two_safety_conditions2_Bad, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,<LHS trace>,Call,Assignment,Assignment,<RHS trace>,Parameter `s`,Binary operation: ([0, +oo] + 15):unsigned32 by call to `two_safety_conditions2_Bad` ]
 codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_ge1_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,<LHS trace>,Parameter `x`,<RHS trace>,Parameter `y`,Binary operation: (0 - 1):unsigned32 by call to `unsigned_prune_ge1_Good` ]
 codetoanalyze/c/bufferoverrun/arith.c, div_const2_FP, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Offset trace>,Parameter `n`,Assignment,<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 1]
 codetoanalyze/c/bufferoverrun/arith.c, div_const_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 2 Size: 2]
@@ -26,6 +26,7 @@ codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min3_Good_FP, 2, BUFFER_OVERR
 codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Call,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 19] Size: 19]
 codetoanalyze/c/bufferoverrun/arith.c, plus_one_Bad, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [<LHS trace>,Unknown value from: unknown_int,Assignment,Binary operation: ([-oo, 9223372036854775807] + 1):signed64]
 codetoanalyze/c/bufferoverrun/arith.c, simple_overflow_Bad, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Binary operation: (85 × 4294967295):unsigned32]
+codetoanalyze/c/bufferoverrun/arith.c, two_safety_conditions2_Bad, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Call,Assignment,Assignment,<RHS trace>,Assignment,Binary operation: ([0, +oo] + [0, 80]):unsigned32]
 codetoanalyze/c/bufferoverrun/arith.c, use_int64_max_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 15 Size: 10]
 codetoanalyze/c/bufferoverrun/arith.c, use_uint64_max_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 15 Size: 10]
 codetoanalyze/c/bufferoverrun/array_content.c, array_min_index_from_one_FP, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
@@ -94,6 +95,8 @@ codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_negative_Bad, 0, INFER
 codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_negative_Good_FP, 0, INFERBO_ALLOC_MAY_BE_NEGATIVE, no_bucket, ERROR, [Call,Assignment,Allocation: Length: [-5, 5]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, call_to_alloc_may_be_big2_is_big_Bad, 1, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Call,Parameter `n`,Allocation: Length: [100000000, +oo] by call to `alloc_may_be_big2_Silenced` ]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, call_to_alloc_may_be_big2_is_big_Bad, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,<LHS trace>,Parameter `n`,<RHS trace>,Call,Assignment,Assignment,Binary operation: (100000000 + [0, +oo]):signed32 by call to `alloc_may_be_big2_Silenced` ]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, call_two_safety_conditions_l1_and_l2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `n`,<Length trace>,Array declaration,Array access: Offset: 10 Size: 10 by call to `two_safety_conditions` ]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, call_two_safety_conditions_l1_and_l2_Bad, 0, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Call,<Offset trace>,Parameter `n`,<Length trace>,Array declaration,Array access: Offset: [9, 11] Size: 10 by call to `two_safety_conditions` ]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, deduplicate_issues_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Unknown value from: unknown_function,Assignment,<Length trace>,Array declaration,Array access: Offset: [10, +oo] Size: 10]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_call_to_s2_symbolic_widened_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `n`,Assignment,<Length trace>,Parameter `n`,Array declaration,Array access: Offset: [1, +oo] Size: 1 by call to `s2_symbolic_widened_Bad` ]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_call_to_s2_symbolic_widened_Bad, 0, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,<LHS trace>,Parameter `n`,Assignment,Binary operation: ([1, +oo] + 1):signed32 by call to `s2_symbolic_widened_Bad` ]
@@ -193,7 +196,8 @@ codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 1, CONDITION_ALWAYS_TRU
 codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 1 Size: 0]
 codetoanalyze/c/bufferoverrun/sizeof.c, static_stride_bad, 5, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/sizeof.c, static_stride_bad, 7, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 1 Size: 0]
-codetoanalyze/c/bufferoverrun/trivial.c, trivial, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
+codetoanalyze/c/bufferoverrun/trivial.c, malloc_zero_Bad, 2, INFERBO_ALLOC_IS_ZERO, no_bucket, ERROR, [Allocation: Length: 0]
+codetoanalyze/c/bufferoverrun/trivial.c, trivial_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
 codetoanalyze/c/bufferoverrun/unreachable.c, FP_loop_once_intentional_good, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/unreachable.c, FP_loop_with_break_good, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/unreachable.c, FP_loop_with_exit_good, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]

infer/tests/codetoanalyze/c/bufferoverrun/trivial.c

@@ -7,7 +7,13 @@
  * LICENSE file in the root directory of this source tree.
  */
 
-void trivial() {
+void trivial_Bad() {
   int a[10];
   a[10] = 0; /* BUG */
 }
+
+void malloc_zero_Bad() {
+  char* x;
+  x = malloc(0);
+  x = malloc(1);
+}

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

@@ -44,6 +44,7 @@ codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call3_plus_params2_Ok, 0, BUFFE
 codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call3_plus_params_Ok, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `x`,<Length trace>,Array declaration,Array access: Offset: -1 Size: 5 by call to `plus_params` ]
 codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call_id_Ok, 4, BUFFER_OVERRUN_L3, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Assignment,Call,Assignment,Assignment,Array declaration,Assignment,Array access: Offset: 5 Size: [0, 6]]
 codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call_loop_with_type_casting_Ok, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,<Length trace>,Parameter `data`,Assignment,Array access: Offset: [2, +oo] (⇐ [0, +oo] + 2) Size: 1 by call to `loop_with_type_casting` ]
+codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call_loop_with_type_casting_Ok, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Array declaration,Assignment,Call,<Length trace>,Parameter `data`,Assignment,Array access: Offset: [0, +oo] Size: 1 by call to `loop_with_type_casting` ]
 codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_loop2_Ok, 9, BUFFER_OVERRUN_L4, no_bucket, ERROR, [<Length trace>,Assignment,Array declaration,Assignment,Array access: Offset: [2, +oo] (⇐ [0, +oo] + 2) Size: 12]
 codetoanalyze/cpp/bufferoverrun/relation.cpp, call2_loop_Bad, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Array declaration,Call,<Length trace>,Parameter `arr`,Array access: Offset: [0, +oo] Size: 5 by call to `loop` ]
 codetoanalyze/cpp/bufferoverrun/relation.cpp, call2_plus_params2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `x`,<Length trace>,Array declaration,Array access: Offset: 11 Size: 5 by call to `plus_params2` ]
@@ -78,6 +79,7 @@ codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, INTEGER_OVERFLOW_
 codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Offset trace>,Call,Call,<Length trace>,Call,Parameter `__n`,Call,Parameter `__n`,Assignment,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Array declaration,Assignment,Assignment,Array access: Offset: [-oo, +oo] Size: 5]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 7, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this[*].infer_size`,Assignment,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,<LHS trace>,Parameter `this[*].infer_size`,Binary operation: ([0, +oo] + 1):unsigned64]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 10, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this[*].infer_size`,Assignment,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Assignment,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Assignment,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Assignment,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,<LHS trace>,Parameter `this[*].infer_size`,<RHS trace>,Parameter `__n`,Binary operation: ([3, +oo] + 42):unsigned64]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 11, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this[*].infer_size`,Assignment,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Assignment,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Assignment,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Assignment,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Assignment,Call,Parameter `this[*].infer_size`,Call,<RHS trace>,Parameter `this[*].infer_size`,Binary operation: (4 × [45, +oo]):unsigned64]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: __infer_skip_function,Call,<Length trace>,Parameter `__il`,Array access: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 17, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Call,Call,Unknown value from: std::distance<const_int_*>,Call,Parameter `__n`,Assignment,Call,Parameter `this[*].infer_size`,Call,<RHS trace>,Parameter `this[*].infer_size`,Binary operation: (4 × [0, +oo]):unsigned64]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 18, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Call,Call,Unknown value from: std::distance<const_int_*>,Call,Parameter `__n`,Assignment,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `__n`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this[*].infer_size`,Array declaration,Assignment,Array access: Offset: 1 Size: [0, +oo]]