diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 4321868a4..7964de54b 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -621,7 +621,7 @@ module Report = struct | Some callee_payload -> let callee_pdesc = Summary.get_proc_desc callee_summary in instantiate_cond tenv callee_pdesc params mem callee_payload location - |> PO.ConditionSet.join cond_set + |> PO.ConditionSet.merge cond_set | None -> (* no inferbo payload *) cond_set ) | None -> diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index 77b27eb04..485b908dc 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml @@ -708,7 +708,7 @@ 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 -> @@ -728,14 +728,11 @@ module ConditionWithTrace = struct {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) = + Option.value_map checked.report_issue_type ~default ~f:(fun 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} @@ -755,48 +752,54 @@ module ConditionSet = struct 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 + match (existing_checked.report_issue_type, new_checked.report_issue_type) with + | _, None -> + `AddAndStop + | Some existing_issue_type, Some new_issue_type + when IssueType.equal existing_issue_type new_issue_type + && ConditionWithTrace.have_similar_bounds existing_cwt new_cwt -> ( + match ConditionWithTrace.xcompare ~lhs:existing_cwt ~rhs:new_cwt with | `LeftSubsumesRight -> `DoNotAddAndStop | `RightSubsumesLeft -> `RemoveExistingAndContinue | `NotComparable -> - `KeepExistingAndContinue - else `KeepExistingAndContinue + `KeepExistingAndContinue ) + | _, _ -> + `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 + | `AddAndStop -> + new_ :: (if same then condset else List.rev_append acc existings) | `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_left ~f:join_one condset1 ~init:condset2 + let merge condset1 condset2 = List.rev_append condset1 condset2 let add_opt location val_traces condset = function | None -> @@ -804,7 +807,7 @@ module ConditionSet = struct | Some cond -> let trace = ConditionTrace.make location val_traces in let cwt = ConditionWithTrace.make cond trace in - join [cwt] condset + cwt :: condset let add_array_access location ~offset ~idx ~size ~is_collection_add ~idx_sym_exp ~size_sym_exp @@ -834,12 +837,24 @@ module ConditionSet = struct | None -> condset | Some cwt -> - join_one condset cwt + cwt :: condset 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 = + let condset = List.map condset ~f:(fun cwt -> (cwt, ConditionWithTrace.check cwt)) in + let conds_to_report, rest = + List.partition_tf condset ~f:(fun (_, {report_issue_type}) -> + Option.is_some report_issue_type ) + in + let conds_reported = + List.fold conds_to_report ~init:[] ~f:join_one + |> List.map ~f:(ConditionWithTrace.report ~report) + in + List.rev_append conds_reported rest + |> List.filter_map ~f:(fun (cwt, {propagate}) -> Option.some_if propagate cwt) + let pp_summary : F.formatter -> _ t0 -> unit = fun fmt condset -> diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli b/infer/src/bufferoverrun/bufferOverrunProofObligations.mli index 0e4d02151..bccc99529 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.mli @@ -59,7 +59,7 @@ module ConditionSet : sig -> t -> t - val join : t -> t -> t + val merge : t -> t -> t val subst : summary_t diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c index bacb0222d..6079abe00 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c @@ -306,3 +306,32 @@ void minmax_div_const_Bad(int n) { int x = a[n / 8]; } } + +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 +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c b/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c index a7a35131a..6d8d40f26 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c @@ -241,3 +241,24 @@ 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); } diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 3a6b12075..ea4fa0fed 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -1,3 +1,4 @@ +codetoanalyze/c/bufferoverrun/arith.c, call_two_safety_conditions2_Bad, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter: s,Binop: ([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,Binop: (0 - 1):unsigned32 by call to `unsigned_prune_ge1_Good` ] codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_zero1_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: x,Binop: (0 - 1):unsigned32 by call to `unsigned_prune_zero1_Good` ] codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_zero2_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: y,Assignment,Binop: ([-oo, 0] - 1):unsigned32 by call to `unsigned_prune_zero2_Good` ] @@ -19,6 +20,7 @@ codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min2_Good_FP, 2, BUFFER_OVERR codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min3_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 25] Size: 20] codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: 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,Binop: ([-oo, 9223372036854775807] + 1):signed64] +codetoanalyze/c/bufferoverrun/arith.c, two_safety_conditions2_Bad, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + [0, 80]):unsigned32] codetoanalyze/c/bufferoverrun/arith.c, use_int64_max_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 15 Size: 10] codetoanalyze/c/bufferoverrun/arith.c, use_uint64_max_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 15 Size: 10] codetoanalyze/c/bufferoverrun/array_content.c, array_min_index_from_one_FP, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] @@ -84,6 +86,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,Return,Alloc: 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,Alloc: 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,Binop: (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,ArrayDeclaration,Parameter: n,ArrayAccess: 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,ArrayDeclaration,Parameter: n,ArrayAccess: Offset: [9, 11] Size: 10 by call to `two_safety_conditions` ] codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_call_to_s2_symbolic_widened_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [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,Binop: ([1, +oo] + 1):signed32 by call to `s2_symbolic_widened_Bad` ] codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_concrete_overrun_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10] @@ -176,7 +180,8 @@ codetoanalyze/c/bufferoverrun/relation.c, FP_call_array_access_Ok, 0, BUFFER_OVE codetoanalyze/c/bufferoverrun/sizeof.c, FN_static_stride_bad, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 1 Size: 0] -codetoanalyze/c/bufferoverrun/trivial.c, trivial, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10] +codetoanalyze/c/bufferoverrun/trivial.c, malloc_zero_Bad, 2, INFERBO_ALLOC_IS_ZERO, no_bucket, ERROR, [Alloc: Length: 0] +codetoanalyze/c/bufferoverrun/trivial.c, trivial_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10] codetoanalyze/c/bufferoverrun/unreachable.c, FP_loop_once_intentional_good, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/unreachable.c, FP_loop_with_break_good, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/unreachable.c, FP_loop_with_exit_good, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] 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 174ca3722..54d85acf3 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -35,6 +35,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,ArrayDeclaration,Parameter: x,ArrayAccess: 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,Call,Assignment,Return,Assignment,ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: 5 Size: [0, 6]] codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call_loop_with_type_casting_Ok, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,Call,Parameter: data,Assignment,ArrayAccess: 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, [ArrayDeclaration,Assignment,Call,Parameter: data,Assignment,ArrayAccess: 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,ArrayDeclaration,Assignment,ArrayAccess: Offset: [2, +oo] (= [0, +oo] + 2) Size: 12] codetoanalyze/cpp/bufferoverrun/relation.cpp, call2_loop_Bad, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: arr,ArrayAccess: 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,ArrayDeclaration,Parameter: x,ArrayAccess: Offset: 11 Size: 5 by call to `plus_params2` ]