diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index bd2b1cbec..41ba726b7 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -536,7 +536,7 @@ module Report = struct List.fold_right ~f ~init:([], 0) trace.trace |> fst |> List.rev - let report_errors : Specs.summary -> Procdesc.t -> PO.ConditionSet.t -> unit = + let report_errors : Specs.summary -> Procdesc.t -> PO.ConditionSet.t -> PO.ConditionSet.t = fun summary pdesc cond_set -> let pname = Procdesc.get_proc_name pdesc in let report cond trace issue_type = @@ -575,8 +575,7 @@ let compute_post let inv_map = Analyzer.exec_pdesc ~initial:Dom.Mem.init pdata in let entry_mem = extract_post inv_map (CFG.start_node cfg) in let exit_mem = extract_post inv_map (CFG.exit_node cfg) in - let cond_set = Report.check_proc summary pdata inv_map in - Report.report_errors summary pdesc cond_set ; + let cond_set = Report.check_proc summary pdata inv_map |> Report.report_errors summary pdesc in match (entry_mem, exit_mem) with | Some entry_mem, Some exit_mem -> Some (entry_mem, exit_mem, cond_set) diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index 538d66e60..d94519821 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml @@ -15,6 +15,8 @@ module ItvPure = Itv.ItvPure module MF = MarkupFormatter module ValTraceSet = BufferOverrunTrace.Set +type checked_condition = {report_issue_type: IssueType.t option; propagate: bool} + module AllocSizeCondition = struct type t = ItvPure.astate @@ -62,23 +64,30 @@ module AllocSizeCondition = struct let check length = match ItvPure.xcompare ~lhs:length ~rhs:ItvPure.zero with | `Equal | `RightSubsumesLeft -> - Some IssueType.inferbo_alloc_is_zero + {report_issue_type= Some IssueType.inferbo_alloc_is_zero; propagate= false} | `LeftSmallerThanRight -> - Some IssueType.inferbo_alloc_is_negative + {report_issue_type= Some IssueType.inferbo_alloc_is_negative; propagate= false} | _ -> match ItvPure.xcompare ~lhs:length ~rhs:ItvPure.mone with | `Equal | `LeftSmallerThanRight | `RightSubsumesLeft -> - Some IssueType.inferbo_alloc_is_negative + {report_issue_type= Some IssueType.inferbo_alloc_is_negative; propagate= false} | `LeftSubsumesRight when Itv.Bound.is_not_infty (ItvPure.lb length) -> - Some IssueType.inferbo_alloc_may_be_negative - | _ -> + {report_issue_type= Some IssueType.inferbo_alloc_may_be_negative; propagate= true} + | cmp_mone -> match ItvPure.xcompare ~lhs:length ~rhs:itv_big with | `Equal | `RightSmallerThanLeft | `RightSubsumesLeft -> - Some IssueType.inferbo_alloc_is_big + {report_issue_type= Some IssueType.inferbo_alloc_is_big; propagate= false} | `LeftSubsumesRight when Itv.Bound.is_not_infty (ItvPure.ub length) -> - Some IssueType.inferbo_alloc_may_be_big - | _ -> - None + {report_issue_type= Some IssueType.inferbo_alloc_may_be_big; propagate= true} + | cmp_big -> + let propagate = + match (cmp_mone, cmp_big) with + | `NotComparable, _ | _, `NotComparable -> + true + | _ -> + false + in + {report_issue_type= None; propagate} let subst bound_map length = @@ -194,7 +203,7 @@ module ArrayAccessCondition = struct (* check buffer overrun and return its confidence *) - let check : t -> IssueType.t option = + let check : t -> checked_condition = fun c -> (* idx = [il, iu], size = [sl, su], we want to check that 0 <= idx < size *) let c' = set_size_pos c in @@ -202,21 +211,28 @@ module ArrayAccessCondition = struct let not_overrun = ItvPure.lt_sem c'.idx c'.size in let not_underrun = ItvPure.le_sem ItvPure.zero c'.idx in (* il >= 0 and iu < sl, definitely not an error *) - if ItvPure.is_one not_overrun && ItvPure.is_one not_underrun then None - (* iu < 0 or il >= su, definitely an error *) + if ItvPure.is_one not_overrun && ItvPure.is_one not_underrun then + {report_issue_type= None; propagate= false} (* iu < 0 or il >= su, definitely an error *) else if ItvPure.is_zero not_overrun || ItvPure.is_zero not_underrun then - Some IssueType.buffer_overrun_l1 (* su <= iu < +oo, most probably an error *) + {report_issue_type= Some IssueType.buffer_overrun_l1; propagate= false} + (* su <= iu < +oo, most probably an error *) else if Itv.Bound.is_not_infty (ItvPure.ub c.idx) && Itv.Bound.le (ItvPure.ub c.size) (ItvPure.ub c.idx) - then Some IssueType.buffer_overrun_l2 (* symbolic il >= sl, probably an error *) + then {report_issue_type= Some IssueType.buffer_overrun_l2; propagate= false} + (* symbolic il >= sl, probably an error *) else if Itv.Bound.is_symbolic (ItvPure.lb c.idx) && Itv.Bound.le (ItvPure.lb c'.size) (ItvPure.lb c.idx) - then Some IssueType.buffer_overrun_s2 (* other symbolic bounds are probably too noisy *) - else if Config.bo_debug <= 3 && (ItvPure.is_symbolic c.idx || ItvPure.is_symbolic c.size) then - None - else if filter1 c then Some IssueType.buffer_overrun_l5 - else if filter2 c then Some IssueType.buffer_overrun_l4 - else Some IssueType.buffer_overrun_l3 + then {report_issue_type= Some IssueType.buffer_overrun_s2; propagate= true} + else + (* other symbolic bounds are probably too noisy *) + let is_symbolic = ItvPure.is_symbolic c.idx || ItvPure.is_symbolic c.size in + let report_issue_type = + if Config.bo_debug <= 3 && is_symbolic then None + else if filter1 c then Some IssueType.buffer_overrun_l5 + else if filter2 c then Some IssueType.buffer_overrun_l4 + else Some IssueType.buffer_overrun_l3 + in + {report_issue_type; propagate= is_symbolic} let subst : Itv.Bound.t bottom_lifted Itv.SubstMap.t -> t -> t option = @@ -461,13 +477,11 @@ module ConditionSet = struct let check_all ~report condset = - List.iter condset ~f:(fun cwt -> - match Condition.check cwt.cond with - | None -> - () - | Some issue_type -> - let issue_type = set_buffer_overrun_u5 cwt issue_type in - report cwt.cond cwt.trace issue_type ) + List.filter condset ~f:(fun cwt -> + let {report_issue_type; propagate} = Condition.check cwt.cond in + report_issue_type |> Option.map ~f:(set_buffer_overrun_u5 cwt) + |> Option.iter ~f:(report cwt.cond cwt.trace) ; + propagate ) let pp_cwt fmt cwt = F.fprintf fmt "%a %a" Condition.pp cwt.cond ConditionTrace.pp cwt.trace diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index d8a6e692f..62a59bb2f 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -34,8 +34,8 @@ codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_goo, 1, CONDITION_ALWAYS_TRU codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_lI, 2, BUFFER_OVERRUN_L5, ERROR, [Call,Call,Assignment,Return,Assignment,Return,Assignment,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [0, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_uI_FP, 0, BUFFER_OVERRUN_S2, ERROR, [Parameter: bi,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [-1+max(1, s$4), -1+max(1, s$5)] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_u_FP, 5, BUFFER_OVERRUN_S2, ERROR, [Call,Parameter: bi,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [-1+max(1, s$8), -1+max(1, s$9)] Size: [0, +oo]] +codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good, 5, BUFFER_OVERRUN_L5, ERROR, [Call,Call,Call,Assignment,Call,Call,Call,Parameter: bi,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [0, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/repro1.cpp, ral_FP, 3, BUFFER_OVERRUN_S2, ERROR, [Call,Call,Parameter: bi,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [-1+max(1, s$4), -1+max(1, s$5)] Size: [0, +oo]] -codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, instantiate_my_vector_oob_Ok, 3, BUFFER_OVERRUN_L1, ERROR, [Call,Parameter: newsize,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,Parameter: i,ArrayAccess: Offset: [42, 42] Size: [42, 42] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call to `my_vector_oob_Bad()` ] codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN_L2, ERROR, [Call,Call,ArrayDeclaration,Assignment,Parameter: i,ArrayAccess: Offset: [u$4, u$5] Size: [u$4, u$5] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call to `int_vector_access_at()` ] codetoanalyze/cpp/bufferoverrun/std_array.cpp, normal_array_bo, 2, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [42, 42] Size: [42, 42]] codetoanalyze/cpp/bufferoverrun/std_array.cpp, std_array_bo_Bad, 2, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [42, 42] Size: [42, 42]] @@ -50,4 +50,5 @@ codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Bad, 3, BUFFER_OVERRUN codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Good_FP, 3, BUFFER_OVERRUN_L3, ERROR, [ArrayDeclaration,Call,Parameter: init,Assignment,Call,Assignment,Call,Call,Assignment,Return,ArrayAccess: Offset: [-1, 0] Size: [10, 10] @ codetoanalyze/cpp/bufferoverrun/vector.cpp:206:3 by call to `access_minus_one()` ] codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN_L1, ERROR, [Call,Call,Assignment,Call,Assignment,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [1, 1] Size: [1, 1]] codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, BUFFER_OVERRUN_L1, ERROR, [Call,Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [0, 0] Size: [0, 0]] +codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, INFERBO_ALLOC_IS_ZERO, ERROR, [Call,Call,Assignment,Call,Call,Call] codetoanalyze/cpp/bufferoverrun/vector.cpp, safe_access3_Good, 2, CONDITION_ALWAYS_FALSE, WARNING, []