diff --git a/infer/src/IR/Typ.ml b/infer/src/IR/Typ.ml index 2127954c3..7f3045a78 100644 --- a/infer/src/IR/Typ.ml +++ b/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} diff --git a/infer/src/IR/Typ.mli b/infer/src/IR/Typ.mli index 3f71485a5..e15189269 100644 --- a/infer/src/IR/Typ.mli +++ b/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 diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index bb4722af1..1effdbb68 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/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) "@[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 diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.mli b/infer/src/bufferoverrun/bufferOverrunChecker.mli index a7383a191..380f8ca15 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.mli +++ b/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 diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index a112a456a..33029a00e 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/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} diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index 74a769948..6eca2cc5f 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/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:@;@[{ %a }@]" - (IList.pp_print_list ~max:30 ~pp_sep ConditionWithTrace.pp) + (IList.pp_print_list ~max:30 ~pp_sep pp_elem) condset diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli b/infer/src/bufferoverrun/bufferOverrunProofObligations.mli index 0167fb418..cd2589096 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli +++ b/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 diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.mli b/infer/src/bufferoverrun/bufferOverrunUtils.mli index bfd98483d..e300dde79 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.mli +++ b/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 diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c index 18e5a7d03..c473b31ba 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c +++ b/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 diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c b/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c index c9d4c606f..d7a410489 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c +++ b/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() { diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index ec2d6794f..cc95473bd 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/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, [,Assignment,,Array declaration,Array access: Offset: 1 Size: 1] codetoanalyze/c/bufferoverrun/arith.c, band_negative_Bad, 8, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Unknown value from: unknown_function,Assignment,Assignment,Assignment,,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, [,Assignment,,Array declaration,Array access: Offset: 1 Size: 1] -codetoanalyze/c/bufferoverrun/arith.c, band_positive_Bad, 6, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: unknown_nat,Assignment,Assignment,,Array declaration,Array access: Offset: [-oo, +oo] Size: 5] -codetoanalyze/c/bufferoverrun/arith.c, band_positive_Good, 6, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: unknown_nat,Assignment,Assignment,,Array declaration,Array access: Offset: [-oo, +oo] Size: 9] +codetoanalyze/c/bufferoverrun/arith.c, band_positive_Bad, 6, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Call,Assignment,Assignment,Assignment,,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, [,Assignment,,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,,Call,Assignment,Assignment,,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,,Parameter `x`,,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, [,Parameter `n`,Assignment,,Array declaration,Array access: Offset: [-oo, +oo] Size: 1] codetoanalyze/c/bufferoverrun/arith.c, div_const_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,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, [,Call,Assignment,,Array declaration,Array access: Offset: [0, 19] Size: 19] codetoanalyze/c/bufferoverrun/arith.c, plus_one_Bad, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [,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, [,Call,Assignment,Assignment,,Assignment,Binary operation: ([0, +oo] + [0, 80]):unsigned32] codetoanalyze/c/bufferoverrun/arith.c, use_int64_max_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: 15 Size: 10] codetoanalyze/c/bufferoverrun/arith.c, use_uint64_max_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,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,,Parameter `n`,,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,,Parameter `n`,,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,,Parameter `n`,,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, [,Unknown value from: unknown_function,Assignment,,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,,Parameter `n`,Assignment,,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,,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, [,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, [,Array declaration,Array access: Offset: 1 Size: 0] -codetoanalyze/c/bufferoverrun/trivial.c, trivial, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,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, [,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] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/trivial.c b/infer/tests/codetoanalyze/c/bufferoverrun/trivial.c index cb368f5b7..3d7ac6c75 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/trivial.c +++ b/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); +} diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 3a57cbb75..d9500ff22 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/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,,Parameter `x`,,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, [,Assignment,,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,,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,,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, [,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,,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,,Parameter `x`,,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, [,Call,Call,,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,,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,,Parameter `this[*].infer_size`,,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,,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,,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,Call,Parameter `__n`,Assignment,Call,Parameter `this[*].infer_size`,Call,,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,Call,Parameter `__n`,Assignment,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `this[*].infer_size`,Call,Parameter `__n`,Call,,Parameter `index`,,Parameter `this[*].infer_size`,Array declaration,Assignment,Array access: Offset: 1 Size: [0, +oo]]