From bd040cf6965567ead88167f67bb2167441fec27c Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Thu, 15 Mar 2018 18:54:20 -0700 Subject: [PATCH] [inferbo] Add an issue type for alarms by unknown function call Summary: It adds an issue type, `BUFFER_OVERRUN_U5`, for alarms involving unknown values, i.e., when the trace set includes an unknown function call. Reviewed By: mbouaziz Differential Revision: D7178841 fbshipit-source-id: bfe857b --- infer/src/base/IssueType.ml | 2 ++ infer/src/base/IssueType.mli | 2 ++ .../bufferOverrunProofObligations.ml | 20 +++++++++++ infer/src/bufferoverrun/bufferOverrunTrace.ml | 8 +++++ infer/src/bufferoverrun/itv.ml | 2 ++ infer/src/bufferoverrun/itv.mli | 2 ++ .../c/bufferoverrun/issue_kinds.c | 34 +++++++++++++++++++ .../codetoanalyze/c/bufferoverrun/issues.exp | 8 +++-- .../cpp/bufferoverrun/issues.exp | 6 ++-- 9 files changed, 78 insertions(+), 6 deletions(-) diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index 467d589cb..01d3d76ff 100644 --- a/infer/src/base/IssueType.ml +++ b/infer/src/base/IssueType.ml @@ -104,6 +104,8 @@ let buffer_overrun_l5 = from_string ~enabled:false "BUFFER_OVERRUN_L5" let buffer_overrun_s2 = from_string "BUFFER_OVERRUN_S2" +let buffer_overrun_u5 = from_string ~enabled:false "BUFFER_OVERRUN_U5" + let cannot_star = from_string "Cannot_star" let checkers_allocates_memory = from_string "CHECKERS_ALLOCATES_MEMORY" diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli index 66594a279..3265887a8 100644 --- a/infer/src/base/IssueType.mli +++ b/infer/src/base/IssueType.mli @@ -55,6 +55,8 @@ val buffer_overrun_l5 : t val buffer_overrun_s2 : t +val buffer_overrun_u5 : t + val cannot_star : t val checkers_allocates_memory : t diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index 25991766e..538d66e60 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml @@ -117,6 +117,8 @@ module ArrayAccessCondition = struct ItvPure.have_similar_bounds lidx ridx && ItvPure.have_similar_bounds lsiz rsiz + let has_infty {idx; size} = ItvPure.has_infty idx || ItvPure.has_infty size + let xcompare ~lhs:{idx= lidx; size= lsiz} ~rhs:{idx= ridx; size= rsiz} = let idxcmp = ItvPure.xcompare ~lhs:lidx ~rhs:ridx in let sizcmp = ItvPure.xcompare ~lhs:lsiz ~rhs:rsiz in @@ -257,6 +259,8 @@ module Condition = struct false + let has_infty = function ArrayAccess c -> ArrayAccessCondition.has_infty c | _ -> false + let xcompare ~lhs ~rhs = match (lhs, rhs) with | AllocSize lhs, AllocSize rhs -> @@ -341,6 +345,12 @@ module ConditionTrace = struct ValTraceSet.instantiate ~traces_caller ~traces_callee:ct.val_traces location in {ct with cond_trace= Inter (caller_pname, callee_pname, location); val_traces} + + + let has_unknown ct = ValTraceSet.has_unknown ct.val_traces + + let check : t -> IssueType.t option = + fun ct -> if has_unknown ct then Some IssueType.buffer_overrun_u5 else None end module ConditionSet = struct @@ -441,12 +451,22 @@ module ConditionSet = struct List.fold condset ~f:subst_add_cwt ~init:[] + let set_buffer_overrun_u5 cwt issue_type = + if ( IssueType.equal issue_type IssueType.buffer_overrun_l3 + || IssueType.equal issue_type IssueType.buffer_overrun_l4 + || IssueType.equal issue_type IssueType.buffer_overrun_l5 ) + && Condition.has_infty cwt.cond + then Option.value (ConditionTrace.check cwt.trace) ~default:issue_type + else issue_type + + 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 ) diff --git a/infer/src/bufferoverrun/bufferOverrunTrace.ml b/infer/src/bufferoverrun/bufferOverrunTrace.ml index 6abb44b68..c5359ac2e 100644 --- a/infer/src/bufferoverrun/bufferOverrunTrace.ml +++ b/infer/src/bufferoverrun/bufferOverrunTrace.ml @@ -55,6 +55,11 @@ module BoTrace = struct fun fmt t -> let pp_sep fmt () = F.fprintf fmt " :: " in F.pp_print_list ~pp_sep pp_elem fmt t.trace + + + let is_unknown_elem = function UnknownFrom _ -> true | _ -> false + + let has_unknown x = List.exists x.trace ~f:is_unknown_elem end module Set = struct @@ -105,6 +110,9 @@ module Set = struct add new_trace traces ) arr_traces traces ) idx_traces empty + + + let has_unknown t = exists BoTrace.has_unknown t end include BoTrace diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 4fcaa1dac..4c6619396 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -840,6 +840,8 @@ module ItvPure = struct let have_similar_bounds (l1, u1) (l2, u2) = Bound.are_similar l1 l2 && Bound.are_similar u1 u2 + let has_infty = function Bound.MInf, _ | _, Bound.PInf -> true | _, _ -> false + let subst : t -> Bound.t bottom_lifted SubstMap.t -> t bottom_lifted = fun x map -> match (Bound.subst_lb (lb x) map, Bound.subst_ub (ub x) map) with diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index 43f4ef4a5..7c5e6fe07 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/infer/src/bufferoverrun/itv.mli @@ -82,6 +82,8 @@ module ItvPure : sig val have_similar_bounds : t -> t -> bool + val has_infty : t -> bool + val make_positive : t -> t val join : t -> t -> t diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c b/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c index 852c31953..08aa7ed95 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c @@ -158,3 +158,37 @@ void alloc_may_be_big_Bad() { malloc(zero_or_ten(1) * 100 * 1000 * 1000 + 1); } void alloc_may_be_big_Good_FP() { malloc(zero_or_ten(1) * 100 * 1000 * 1000 + 1); } + +void l1_unknown_function_Bad() { + int a[5]; + int idx = unknown_function() * 10; + if (10 <= idx) { + if (idx <= 10) { + a[idx] = 0; + } + } +} + +int zero_to_infty() { + int r = 0; + for (int i = 0; i < zero_or_ten(0); i++) { + r++; + } + return r; +} + +/* Inferbo raises U5 alarm because + - the pair of offset:[10,10] and size:[5,+oo] is belong to L3 + - the offset value is from an unknown function + - there is at least one infinity bound (in size). + However, it should ideally raise L3, because the infinity is not + from the unknown function. */ +void False_Issue_Type_l3_unknown_function_Bad() { + int* a = (int*)malloc((zero_to_infty() + 5) * sizeof(int)); + int idx = unknown_function() * 10; + if (10 <= idx) { + if (idx <= 10) { + a[idx] = 0; + } + } +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index d9699a108..d32f3ee05 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -15,7 +15,7 @@ codetoanalyze/c/bufferoverrun/duplicates.c, one_alarm_is_enough, 2, BUFFER_OVERR codetoanalyze/c/bufferoverrun/duplicates.c, tsa_one_alarm_Bad, 0, BUFFER_OVERRUN_L1, ERROR, [Call,ArrayDeclaration,Parameter: n,ArrayAccess: Offset: [3, 3] Size: [1, 1] @ codetoanalyze/c/bufferoverrun/duplicates.c:23:3 by call to `two_symbolic_accesses()` ] codetoanalyze/c/bufferoverrun/duplicates.c, tsa_two_alarms_Bad, 0, BUFFER_OVERRUN_L1, ERROR, [Call,ArrayDeclaration,Parameter: n,ArrayAccess: Offset: [-1, -1] Size: [1, 1] @ codetoanalyze/c/bufferoverrun/duplicates.c:24:3 by call to `two_symbolic_accesses()` ] codetoanalyze/c/bufferoverrun/duplicates.c, tsa_two_alarms_Bad, 0, BUFFER_OVERRUN_L1, ERROR, [Call,ArrayDeclaration,Parameter: n,ArrayAccess: Offset: [1, 1] Size: [1, 1] @ codetoanalyze/c/bufferoverrun/duplicates.c:23:3 by call to `two_symbolic_accesses()` ] -codetoanalyze/c/bufferoverrun/external.c, extern_bad, 5, BUFFER_OVERRUN_L5, ERROR, [Unknown value from: lib,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] +codetoanalyze/c/bufferoverrun/external.c, extern_bad, 5, BUFFER_OVERRUN_U5, ERROR, [Unknown value from: lib,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/c/bufferoverrun/external.c, extern_bad, 10, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [30, 30] Size: [10, 10]] codetoanalyze/c/bufferoverrun/for_loop.c, for_loop, 10, BUFFER_OVERRUN_L3, ERROR, [Call,ArrayDeclaration,Assignment,Assignment,Return,Assignment,Assignment,ArrayAccess: Offset: [0, 9] Size: [5, 10]] codetoanalyze/c/bufferoverrun/function_call.c, call_by_arr_bad, 3, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: [-1, -1] Size: [10, 10]] @@ -25,6 +25,7 @@ codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN_ codetoanalyze/c/bufferoverrun/global.c, compare_global_variable_bad, 3, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [10, 10]] codetoanalyze/c/bufferoverrun/goto_loop.c, goto_loop, 11, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [10, +oo] Size: [10, 10]] codetoanalyze/c/bufferoverrun/inf_loop.c, inf_loop, 4, CONDITION_ALWAYS_TRUE, WARNING, [] +codetoanalyze/c/bufferoverrun/issue_kinds.c, False_Issue_Type_l3_unknown_function_Bad, 5, BUFFER_OVERRUN_U5, ERROR, [Call,Assignment,Assignment,Return,ArrayDeclaration,Assignment,Unknown value from: unknown_function,Assignment,ArrayAccess: Offset: [10, 10] Size: [5, +oo]] codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_is_big_Bad, 0, INFERBO_ALLOC_IS_BIG, ERROR, [Alloc: [2000000000, 2000000000]] codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_is_negative_Bad, 0, INFERBO_ALLOC_IS_NEGATIVE, ERROR, [Alloc: [-2, -2]] codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_is_zero_Bad, 0, INFERBO_ALLOC_IS_ZERO, ERROR, [Alloc: [0, 0]] @@ -36,6 +37,7 @@ codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_concrete_overrun_Bad, 2, BUFFER_ codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_concrete_underrun_Bad, 2, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [-1, -1] Size: [10, 10]] codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_overrun_Bad, 3, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Parameter: i,ArrayAccess: Offset: [max(10, s$0), s$1] Size: [10, 10]] codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_underrun_Bad, 3, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Parameter: i,ArrayAccess: Offset: [s$0, min(-1, s$1)] Size: [10, 10]] +codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_unknown_function_Bad, 5, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Unknown value from: unknown_function,Assignment,ArrayAccess: Offset: [10, 10] Size: [5, 5]] codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_no_overrun_Good_FP, 2, BUFFER_OVERRUN_L2, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 10] Size: [10, 10]] codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_no_underrun_Good_FP, 2, BUFFER_OVERRUN_L2, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [-1, 9] Size: [9, 9]] codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_overrun_Bad, 2, BUFFER_OVERRUN_L2, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 10] Size: [10, 10]] @@ -47,8 +49,8 @@ codetoanalyze/c/bufferoverrun/issue_kinds.c, l3_concrete_overrun_Bad, 2, BUFFER_ codetoanalyze/c/bufferoverrun/issue_kinds.c, l3_concrete_underrun_Bad, 2, BUFFER_OVERRUN_L3, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [-1, 9] Size: [10, 10]] codetoanalyze/c/bufferoverrun/issue_kinds.c, l4_widened_no_overrun_Good_FP, 3, BUFFER_OVERRUN_L4, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: [10, 10]] codetoanalyze/c/bufferoverrun/issue_kinds.c, l4_widened_overrun_Bad, 3, BUFFER_OVERRUN_L4, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: [10, 10]] -codetoanalyze/c/bufferoverrun/issue_kinds.c, l5_external_Warn_Bad, 2, BUFFER_OVERRUN_L5, ERROR, [Unknown value from: unknown_function,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] -codetoanalyze/c/bufferoverrun/issue_kinds.c, l5_external_Warn_Bad, 2, BUFFER_OVERRUN_L5, ERROR, [ArrayDeclaration,Unknown value from: unknown_function,ArrayAccess: Offset: [-oo, +oo] Size: [10, 10]] +codetoanalyze/c/bufferoverrun/issue_kinds.c, l5_external_Warn_Bad, 2, BUFFER_OVERRUN_U5, ERROR, [ArrayDeclaration,Unknown value from: unknown_function,ArrayAccess: Offset: [-oo, +oo] Size: [10, 10]] +codetoanalyze/c/bufferoverrun/issue_kinds.c, l5_external_Warn_Bad, 2, BUFFER_OVERRUN_U5, ERROR, [Unknown value from: unknown_function,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/c/bufferoverrun/issue_kinds.c, s2_symbolic_widened_Bad, 3, BUFFER_OVERRUN_S2, ERROR, [Offset: [s$0, +oo] Size: [s$0, s$1]] codetoanalyze/c/bufferoverrun/issue_kinds.c, s2_symbolic_widened_Good_FP, 3, BUFFER_OVERRUN_S2, ERROR, [Offset: [s$0, +oo] Size: [s$0, s$1]] codetoanalyze/c/bufferoverrun/models.c, exit_bo_good_unreachable_bad, 2, UNREACHABLE_CODE, ERROR, [] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 1495e1d49..f63ca3409 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -9,7 +9,7 @@ codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access2_Bad, 2, BUFFER_OVERR codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access_Bad, 2, BUFFER_OVERRUN_L1, ERROR, [Call,Call,Parameter: n,Assignment,ArrayAccess: Offset: [10, 10] Size: [10, 10]] codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_Bad, 3, BUFFER_OVERRUN_L1, ERROR, [Offset: [10, 10] Size: [5, 5]] codetoanalyze/cpp/bufferoverrun/class.cpp, return_class_Bad, 2, BUFFER_OVERRUN_L1, ERROR, [Return,ArrayAccess: Offset: [5, 5] Size: [5, 5]] -codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 5, BUFFER_OVERRUN_L5, ERROR, [Unknown value from: lib,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] +codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 5, BUFFER_OVERRUN_U5, ERROR, [Unknown value from: lib,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 10, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [30, 30] Size: [10, 10]] codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, BUFFER_OVERRUN_L4, ERROR, [Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [0, 0] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_by_ref_bad, 4, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: [-1, -1] Size: [10, 10]] @@ -33,8 +33,8 @@ codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN_L1, ERRO codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 6, BUFFER_OVERRUN_L1, ERROR, [Call,Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [6, 6] Size: [5, 5]] codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, BUFFER_OVERRUN_L3, ERROR, [Call,Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [4, 4] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_L5, ERROR, [Call,Parameter: __n,Call,Parameter: __n,Assignment,Call,Call,ArrayDeclaration,Assignment,Assignment,Return,Assignment,Assignment,Return,Assignment,Call,Return,Return,ArrayAccess: Offset: [-oo, +oo] Size: [5, 5]] -codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN_L5, ERROR, [Unknown value from: __infer_skip_function,Call,Parameter: __il,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] -codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 18, BUFFER_OVERRUN_L3, ERROR, [Call,Call,Unknown value from: std::distance,Call,Parameter: __n,Assignment,Call,Call,Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [1, 1] Size: [0, +oo]] +codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN_U5, ERROR, [Unknown value from: __infer_skip_function,Call,Parameter: __il,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] +codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 18, BUFFER_OVERRUN_U5, ERROR, [Call,Call,Unknown value from: std::distance,Call,Parameter: __n,Assignment,Call,Call,Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [1, 1] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN_L2, ERROR, [Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [u$4, u$5] Size: [u$4, u$5]] codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Bad, 3, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Call,Parameter: init,Assignment,Call,Assignment,Call,Call,Assignment,Return,ArrayAccess: Offset: [-1, -1] Size: [10, 10] @ codetoanalyze/cpp/bufferoverrun/vector.cpp:206:3 by call to `access_minus_one()` ] 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()` ]