diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 7dc772f69..319b4f642 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -555,6 +555,9 @@ module Report = struct fun trace issue_desc -> let f elem (trace, depth) = match elem with + | Trace.Alloc location -> + let desc = "Alloc: " ^ issue_desc in + (Errlog.make_trace_element depth location desc [] :: trace, depth) | Trace.ArrAccess location -> let desc = "ArrayAccess: " ^ issue_desc in (Errlog.make_trace_element depth location desc [] :: trace, depth) diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 546d56336..b15b29dd0 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -73,7 +73,10 @@ let check_alloc_size size_exp {pname; location} mem cond_set = | Bottom -> cond_set | NonBottom length -> - let traces = Dom.Val.get_traces v_length in + let alloc_trace_elem = BufferOverrunTrace.Alloc location in + let traces = + Dom.Val.get_traces v_length |> BufferOverrunTrace.Set.add_elem alloc_trace_elem + in PO.ConditionSet.add_alloc_size pname location ~length traces cond_set @@ -303,7 +306,7 @@ module StdArray = struct {declare_local; declare_symbolic} end -(* Java's Collections are represented by their size. We don't care about the elements. +(* Java's Collections are represented by their size. We don't care about the elements. - when they are constructed, we set the size to 0 - each time we add an element, we increase the length of the array - each time we delete an element, we decrease the length of the array *) diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index 1dd24264c..98c181272 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml @@ -24,7 +24,7 @@ module AllocSizeCondition = struct let pp fmt length = F.fprintf fmt "alloc(%a)" ItvPure.pp length - let pp_description fmt length = F.fprintf fmt "Alloc: %a" ItvPure.pp length + let pp_description fmt length = F.fprintf fmt "Length: %a" ItvPure.pp length let make ~length = if ItvPure.is_invalid length then None else Some length diff --git a/infer/src/bufferoverrun/bufferOverrunTrace.ml b/infer/src/bufferoverrun/bufferOverrunTrace.ml index 8bc7181db..d9c260396 100644 --- a/infer/src/bufferoverrun/bufferOverrunTrace.ml +++ b/infer/src/bufferoverrun/bufferOverrunTrace.ml @@ -11,6 +11,7 @@ module F = Format module BoTrace = struct type elem = + | Alloc of Location.t | ArrAccess of Location.t | ArrDecl of Location.t | Assign of Location.t @@ -33,6 +34,8 @@ module BoTrace = struct let pp_elem : F.formatter -> elem -> unit = fun fmt elem -> match elem with + | Alloc location -> + F.fprintf fmt "Alloc (%a)" Location.pp_file_pos location | ArrAccess location -> F.fprintf fmt "ArrAccess (%a)" Location.pp_file_pos location | ArrDecl location -> diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 77d67bd30..221cdf902 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -27,13 +27,13 @@ codetoanalyze/c/bufferoverrun/global.c, compare_global_variable_bad, 3, BUFFER_O codetoanalyze/c/bufferoverrun/goto_loop.c, goto_loop, 11, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [10, +oo] Size: 10] codetoanalyze/c/bufferoverrun/inf_loop.c, inf_loop, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/issue_kinds.c, False_Issue_Type_l3_unknown_function_Bad, 5, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Call,Assignment,Assignment,Return,ArrayDeclaration,Assignment,Unknown value from: unknown_function,Assignment,ArrayAccess: Offset: 10 Size: [5, +oo]] -codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_is_big_Bad, 0, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Alloc: 2000000000] -codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_is_negative_Bad, 0, INFERBO_ALLOC_IS_NEGATIVE, no_bucket, ERROR, [Alloc: -2] -codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_is_zero_Bad, 0, INFERBO_ALLOC_IS_ZERO, no_bucket, ERROR, [Alloc: 0] -codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_big_Bad, 0, INFERBO_ALLOC_MAY_BE_BIG, no_bucket, ERROR, [Call,Assignment,Return] -codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_big_Good_FP, 1, INFERBO_ALLOC_MAY_BE_BIG, no_bucket, ERROR, [Call,Assignment,Return] -codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_negative_Bad, 0, INFERBO_ALLOC_MAY_BE_NEGATIVE, no_bucket, ERROR, [Call,Assignment,Return] -codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_negative_Good_FP, 0, INFERBO_ALLOC_MAY_BE_NEGATIVE, no_bucket, ERROR, [Call,Assignment,Return] +codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_is_big_Bad, 0, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Alloc: Length: 2000000000] +codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_is_negative_Bad, 0, INFERBO_ALLOC_IS_NEGATIVE, no_bucket, ERROR, [Alloc: Length: -2] +codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_is_zero_Bad, 0, INFERBO_ALLOC_IS_ZERO, no_bucket, ERROR, [Alloc: Length: 0] +codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_big_Bad, 0, INFERBO_ALLOC_MAY_BE_BIG, no_bucket, ERROR, [Call,Assignment,Return,Alloc: Length: [1, 1000000001]] +codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_big_Good_FP, 1, INFERBO_ALLOC_MAY_BE_BIG, no_bucket, ERROR, [Call,Assignment,Return,Alloc: Length: [1, 1000000001]] +codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_negative_Bad, 0, INFERBO_ALLOC_MAY_BE_NEGATIVE, no_bucket, ERROR, [Call,Assignment,Return,Alloc: Length: [-5, 5]] +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, l1_concrete_overrun_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10] codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_concrete_underrun_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: -1 Size: 10] codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_overrun_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Parameter: i,ArrayAccess: Offset: [max(10, i.lb), i.ub] Size: 10] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 23a35b548..ff44b75ce 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -50,5 +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, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: init,Assignment,Call,Assignment,Call,Call,Assignment,Return,ArrayAccess: Offset: [-1, 0] Size: 10 by call to `access_minus_one` ] codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Assignment,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 1 Size: 1] codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 0 Size: 0] -codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, INFERBO_ALLOC_IS_ZERO, no_bucket, ERROR, [Call,Call,Assignment,Call,Call,Call] +codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, INFERBO_ALLOC_IS_ZERO, no_bucket, ERROR, [Call,Call,Assignment,Call,Call,Call,Alloc: Length: 0] codetoanalyze/cpp/bufferoverrun/vector.cpp, safe_access3_Good, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []