From 3f71cf327bfeac38fafdeae0294ab3d70c34925a Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Fri, 26 Oct 2018 22:45:09 -0700 Subject: [PATCH] [inferbo] Separate offset and index in condition Summary: This diff preserves values of offset and index separately, rather than one value of their addition, because premature addition results in imprecise FPs by the limited expressiveness of the domain. Reviewed By: mbouaziz Differential Revision: D10851393 fbshipit-source-id: 1685ead36 --- .../bufferOverrunProofObligations.ml | 160 ++++++++++-------- .../bufferOverrunProofObligations.mli | 1 + infer/src/bufferoverrun/bufferOverrunUtils.ml | 35 ++-- infer/src/bufferoverrun/itv.mli | 4 + .../c/bufferoverrun/array_content.c | 2 +- .../codetoanalyze/c/bufferoverrun/do_while.c | 6 +- .../codetoanalyze/c/bufferoverrun/for_loop.c | 16 ++ .../codetoanalyze/c/bufferoverrun/issues.exp | 4 +- .../codetoanalyze/java/performance/issues.exp | 2 +- 9 files changed, 141 insertions(+), 89 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index eb53761a7..cd67ea4cb 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml @@ -99,91 +99,106 @@ end module ArrayAccessCondition = struct type t = - { idx: ItvPure.astate + { offset: ItvPure.astate + ; idx: ItvPure.astate ; size: ItvPure.astate ; idx_sym_exp: Relation.SymExp.t option ; size_sym_exp: Relation.SymExp.t option ; relation: Relation.astate } [@@deriving compare] - let get_symbols c = ItvPure.get_symbols c.idx @ ItvPure.get_symbols c.size - - let set_size_pos : t -> t = - fun c -> - let size' = ItvPure.make_positive c.size in - if phys_equal size' c.size then c else {c with size= size'} + let get_symbols c = + ItvPure.get_symbols c.offset @ ItvPure.get_symbols c.idx @ ItvPure.get_symbols c.size let pp : F.formatter -> t -> unit = fun fmt c -> - let c = set_size_pos c in - F.fprintf fmt "%a < %a" ItvPure.pp c.idx ItvPure.pp c.size ; + let pp_offset fmt = + if not (ItvPure.is_zero c.offset) then F.fprintf fmt "%a + " ItvPure.pp c.offset + in + F.fprintf fmt "%t%a < %a" pp_offset ItvPure.pp c.idx ItvPure.pp (ItvPure.make_positive c.size) ; if Option.is_some Config.bo_relational_domain then F.fprintf fmt "@,%a < %a when %a" Relation.SymExp.pp_opt c.idx_sym_exp Relation.SymExp.pp_opt c.size_sym_exp Relation.pp c.relation + (* TODO: change description to distinguish offset and index *) let pp_description : F.formatter -> t -> unit = fun fmt c -> - let c = set_size_pos c in - F.fprintf fmt "Offset: %a Size: %a" ItvPure.pp c.idx ItvPure.pp c.size + F.fprintf fmt "Offset: %a Size: %a" ItvPure.pp (ItvPure.plus c.offset c.idx) ItvPure.pp + (ItvPure.make_positive c.size) let make : - idx:ItvPure.t + offset:ItvPure.t + -> idx:ItvPure.t -> size:ItvPure.t -> idx_sym_exp:Relation.SymExp.t option -> size_sym_exp:Relation.SymExp.t option -> relation:Relation.astate -> t option = - fun ~idx ~size ~idx_sym_exp ~size_sym_exp ~relation -> - if ItvPure.is_invalid idx || ItvPure.is_invalid size then None - else Some {idx; size; idx_sym_exp; size_sym_exp; relation} + fun ~offset ~idx ~size ~idx_sym_exp ~size_sym_exp ~relation -> + if ItvPure.is_invalid offset || ItvPure.is_invalid idx || ItvPure.is_invalid size then None + else Some {offset; idx; size; idx_sym_exp; size_sym_exp; relation} + + let have_similar_bounds {offset= loff; idx= lidx; size= lsiz} + {offset= roff; idx= ridx; size= rsiz} = + ItvPure.have_similar_bounds loff roff + && ItvPure.have_similar_bounds lidx ridx + && ItvPure.have_similar_bounds lsiz rsiz - let have_similar_bounds {idx= lidx; size= lsiz} {idx= ridx; size= rsiz} = - ItvPure.have_similar_bounds lidx ridx && ItvPure.have_similar_bounds lsiz rsiz + let has_infty {offset; idx; size} = + ItvPure.has_infty offset || ItvPure.has_infty idx || ItvPure.has_infty size - 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 xcompare ~lhs:{offset= loff; idx= lidx; size= lsiz} ~rhs:{offset= roff; idx= ridx; size= rsiz} + = + let offcmp = ItvPure.xcompare ~lhs:loff ~rhs:roff in let idxcmp = ItvPure.xcompare ~lhs:lidx ~rhs:ridx in let sizcmp = ItvPure.xcompare ~lhs:lsiz ~rhs:rsiz in - match (idxcmp, sizcmp) with - | `Equal, `Equal -> + match (offcmp, idxcmp, sizcmp) with + | `Equal, `Equal, `Equal -> `Equal - | `NotComparable, _ -> + | `NotComparable, _, _ | _, `NotComparable, _ -> `NotComparable - | `Equal, (`LeftSmallerThanRight | `LeftSubsumesRight) -> + | `Equal, `Equal, (`LeftSmallerThanRight | `LeftSubsumesRight) -> `LeftSubsumesRight - | `Equal, (`RightSmallerThanLeft | `RightSubsumesLeft) -> + | `Equal, `Equal, (`RightSmallerThanLeft | `RightSubsumesLeft) -> `RightSubsumesLeft - | `LeftSubsumesRight, (`Equal | `LeftSubsumesRight) -> + | (`Equal | `LeftSubsumesRight), (`Equal | `LeftSubsumesRight), (`Equal | `LeftSubsumesRight) + -> `LeftSubsumesRight - | `RightSubsumesLeft, (`Equal | `RightSubsumesLeft) -> + | (`Equal | `RightSubsumesLeft), (`Equal | `RightSubsumesLeft), (`Equal | `RightSubsumesLeft) + -> `RightSubsumesLeft - | (`LeftSmallerThanRight | `RightSmallerThanLeft), _ -> - let lidxpos = ItvPure.le_sem ItvPure.zero lidx in - let ridxpos = ItvPure.le_sem ItvPure.zero ridx in + | (`Equal | `LeftSmallerThanRight), (`Equal | `LeftSmallerThanRight), _ + | (`Equal | `RightSmallerThanLeft), (`Equal | `RightSmallerThanLeft), _ -> + let lidxpos = ItvPure.le_sem (ItvPure.neg lidx) loff in + let ridxpos = ItvPure.le_sem (ItvPure.neg ridx) roff in if not (Itv.Boolean.equal lidxpos ridxpos) then `NotComparable else if Itv.Boolean.is_true lidxpos then (* both idx >= 0 *) - match (idxcmp, sizcmp) with - | `LeftSmallerThanRight, (`Equal | `RightSmallerThanLeft | `RightSubsumesLeft) -> + match (offcmp, idxcmp, sizcmp) with + | ( (`Equal | `LeftSmallerThanRight) + , (`Equal | `LeftSmallerThanRight) + , (`Equal | `RightSmallerThanLeft | `RightSubsumesLeft) ) -> `RightSubsumesLeft - | `RightSmallerThanLeft, (`Equal | `LeftSmallerThanRight | `LeftSubsumesRight) -> + | ( (`Equal | `RightSmallerThanLeft) + , (`Equal | `RightSmallerThanLeft) + , (`Equal | `LeftSmallerThanRight | `LeftSubsumesRight) ) -> `LeftSubsumesRight | _ -> `NotComparable else if Itv.Boolean.is_false lidxpos then (* both idx < 0, size doesn't matter *) - match idxcmp with - | `LeftSmallerThanRight -> + match (offcmp, idxcmp) with + | `Equal, `LeftSmallerThanRight | `LeftSmallerThanRight, `Equal -> `LeftSubsumesRight - | `RightSmallerThanLeft -> + | `Equal, `RightSmallerThanLeft | `RightSmallerThanLeft, `Equal -> `RightSubsumesLeft - | `Equal -> + | `Equal, `Equal -> `Equal | _ -> `NotComparable @@ -192,34 +207,34 @@ module ArrayAccessCondition = struct `NotComparable - let filter1 : t -> bool = - fun c -> - ItvPure.is_top c.idx || ItvPure.is_top c.size || ItvPure.is_lb_infty c.idx + let filter1 : real_idx:ItvPure.t -> t -> bool = + fun ~real_idx c -> + ItvPure.is_top real_idx || ItvPure.is_top c.size || ItvPure.is_lb_infty real_idx || ItvPure.is_lb_infty c.size - || (ItvPure.is_nat c.idx && ItvPure.is_nat c.size) + || (ItvPure.is_nat real_idx && ItvPure.is_nat c.size) - let filter2 : t -> bool = - fun c -> + let filter2 : real_idx:ItvPure.t -> t -> bool = + fun ~real_idx c -> (* basically, alarms involving infinity are filtered *) - ((not (ItvPure.is_finite c.idx)) || not (ItvPure.is_finite c.size)) + ((not (ItvPure.is_finite real_idx)) || not (ItvPure.is_finite c.size)) && (* except the following cases *) not - ( Bound.is_not_infty (ItvPure.lb c.idx) + ( Bound.is_not_infty (ItvPure.lb real_idx) && (* idx non-infty lb < 0 *) - Bound.lt (ItvPure.lb c.idx) Bound.zero - || Bound.is_not_infty (ItvPure.lb c.idx) + Bound.lt (ItvPure.lb real_idx) Bound.zero + || Bound.is_not_infty (ItvPure.lb real_idx) && (* idx non-infty lb > size lb *) - Bound.gt (ItvPure.lb c.idx) (ItvPure.lb c.size) - || Bound.is_not_infty (ItvPure.lb c.idx) + Bound.gt (ItvPure.lb real_idx) (ItvPure.lb c.size) + || Bound.is_not_infty (ItvPure.lb real_idx) && (* idx non-infty lb > size ub *) - Bound.gt (ItvPure.lb c.idx) (ItvPure.ub c.size) - || Bound.is_not_infty (ItvPure.ub c.idx) + Bound.gt (ItvPure.lb real_idx) (ItvPure.ub c.size) + || Bound.is_not_infty (ItvPure.ub real_idx) && (* idx non-infty ub > size lb *) - Bound.gt (ItvPure.ub c.idx) (ItvPure.lb c.size) - || Bound.is_not_infty (ItvPure.ub c.idx) + Bound.gt (ItvPure.ub real_idx) (ItvPure.lb c.size) + || Bound.is_not_infty (ItvPure.ub real_idx) && (* idx non-infty ub > size ub *) - Bound.gt (ItvPure.ub c.idx) (ItvPure.ub c.size) ) + Bound.gt (ItvPure.ub real_idx) (ItvPure.ub c.size) ) (* check buffer overrun and return its confidence *) @@ -228,17 +243,18 @@ module ArrayAccessCondition = struct (* idx = [il, iu], size = [sl, su], For arrays : we want to check that 0 <= idx < size For adding into arraylists: we want to check that 0 <= idx <= size *) - let c' = set_size_pos c in + let real_idx = ItvPure.plus c.offset c.idx in + let size = ItvPure.make_positive c.size in (* if sl < 0, use sl' = 0 *) let not_overrun = - if is_collection_add then ItvPure.le_sem c'.idx c'.size - else if Relation.lt_sat_opt c'.idx_sym_exp c'.size_sym_exp c'.relation then Itv.Boolean.true_ - else ItvPure.lt_sem c'.idx c'.size + if is_collection_add then ItvPure.le_sem real_idx size + else if Relation.lt_sat_opt c.idx_sym_exp c.size_sym_exp c.relation then Itv.Boolean.true_ + else ItvPure.lt_sem real_idx size in let not_underrun = - if Relation.le_sat_opt (Some Relation.SymExp.zero) c'.idx_sym_exp c'.relation then + if Relation.le_sat_opt (Some Relation.SymExp.zero) c.idx_sym_exp c.relation then Itv.Boolean.true_ - else ItvPure.le_sem ItvPure.zero c'.idx + else ItvPure.le_sem ItvPure.zero real_idx in (* il >= 0 and iu < sl, definitely not an error *) if Itv.Boolean.is_true not_overrun && Itv.Boolean.is_true not_underrun then @@ -247,19 +263,21 @@ module ArrayAccessCondition = struct {report_issue_type= Some IssueType.buffer_overrun_l1; propagate= false} (* su <= iu < +oo, most probably an error *) else if - Bound.is_not_infty (ItvPure.ub c.idx) && Bound.le (ItvPure.ub c.size) (ItvPure.ub c.idx) + 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} (* symbolic il >= sl, probably an error *) else if - Bound.is_symbolic (ItvPure.lb c.idx) && Bound.le (ItvPure.lb c'.size) (ItvPure.lb c.idx) + 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} else (* other symbolic bounds are probably too noisy *) - let is_symbolic = ItvPure.is_symbolic c.idx || ItvPure.is_symbolic c.size in + 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 c then Some IssueType.buffer_overrun_l5 - else if filter2 c then Some IssueType.buffer_overrun_l4 + 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 in {report_issue_type; propagate= is_symbolic} @@ -272,12 +290,14 @@ module ArrayAccessCondition = struct -> t -> t option = fun eval_sym rel_map caller_relation c -> - match (ItvPure.subst c.idx eval_sym, ItvPure.subst c.size eval_sym) with - | NonBottom idx, NonBottom size -> + match + (ItvPure.subst c.offset eval_sym, ItvPure.subst c.idx eval_sym, ItvPure.subst c.size eval_sym) + with + | NonBottom offset, NonBottom idx, NonBottom size -> let idx_sym_exp = Relation.SubstMap.symexp_subst_opt rel_map c.idx_sym_exp in let size_sym_exp = Relation.SubstMap.symexp_subst_opt rel_map c.size_sym_exp in let relation = Relation.instantiate rel_map ~caller:caller_relation ~callee:c.relation in - Some {idx; size; idx_sym_exp; size_sym_exp; relation} + Some {offset; idx; size; idx_sym_exp; size_sym_exp; relation} | _ -> None @@ -780,9 +800,9 @@ module ConditionSet = struct join [cwt] condset - let add_array_access location ~idx ~size ~is_collection_add ~idx_sym_exp ~size_sym_exp ~relation - val_traces condset = - ArrayAccessCondition.make ~idx ~size ~idx_sym_exp ~size_sym_exp ~relation + let add_array_access location ~offset ~idx ~size ~is_collection_add ~idx_sym_exp ~size_sym_exp + ~relation val_traces condset = + ArrayAccessCondition.make ~offset ~idx ~size ~idx_sym_exp ~size_sym_exp ~relation |> Condition.make_array_access ~is_collection_add |> add_opt location val_traces condset diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli b/infer/src/bufferoverrun/bufferOverrunProofObligations.mli index 1cc97f799..0e4d02151 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.mli @@ -36,6 +36,7 @@ module ConditionSet : sig val add_array_access : Location.t + -> offset:ItvPure.astate -> idx:ItvPure.astate -> size:ItvPure.astate -> is_collection_add:bool diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index 454273eab..ab28cee1d 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -297,12 +297,20 @@ end module Check = struct let check_access ~size ~idx ~size_sym_exp ~idx_sym_exp ~relation ~arr ~idx_traces ?(is_collection_add = false) location cond_set = - let arr_traces = Dom.Val.get_traces arr in match (size, idx) with | NonBottom length, NonBottom idx -> + let offset = + match ArrayBlk.offsetof (Dom.Val.get_array_blk arr) with + | Bottom -> + (* Java's collection has no offset. *) + Itv.ItvPure.zero + | NonBottom offset -> + offset + in + let arr_traces = Dom.Val.get_traces arr in let traces = TraceSet.merge ~arr_traces ~idx_traces location in - PO.ConditionSet.add_array_access location ~size:length ~idx ~size_sym_exp ~idx_sym_exp - ~relation ~is_collection_add traces cond_set + PO.ConditionSet.add_array_access location ~size:length ~offset ~idx ~size_sym_exp + ~idx_sym_exp ~relation ~is_collection_add traces cond_set | _ -> cond_set @@ -311,20 +319,19 @@ module Check = struct let arr_blk = Dom.Val.get_array_blk arr in let size = ArrayBlk.sizeof arr_blk in let size_sym_exp = Relation.SymExp.of_sym (Dom.Val.get_size_sym arr) in - let offset = ArrayBlk.offsetof arr_blk in - let offset_sym_exp = Relation.SymExp.of_sym (Dom.Val.get_offset_sym arr) in let idx_itv = Dom.Val.get_itv idx in let idx_traces = Dom.Val.get_traces idx in - let idx_in_blk = (if is_plus then Itv.plus else Itv.minus) offset idx_itv in + let idx = if is_plus then idx_itv else Itv.neg idx_itv in let idx_sym_exp = + let offset_sym_exp = Relation.SymExp.of_sym (Dom.Val.get_offset_sym arr) in Option.map2 offset_sym_exp idx_sym_exp ~f:(fun offset_sym_exp idx_sym_exp -> let op = if is_plus then Relation.SymExp.plus else Relation.SymExp.minus in op idx_sym_exp offset_sym_exp ) in L.(debug BufferOverrun Verbose) - "@[Add condition :@,array: %a@, idx: %a@,@]@." ArrayBlk.pp arr_blk Itv.pp idx_in_blk ; - check_access ~size ~idx:idx_in_blk ~size_sym_exp ~idx_sym_exp ~relation ~arr ~idx_traces - location cond_set + "@[Add condition :@,array: %a@, idx: %a + %a@,@]@." ArrayBlk.pp arr_blk Itv.pp + (ArrayBlk.offsetof arr_blk) Itv.pp idx ; + check_access ~size ~idx ~size_sym_exp ~idx_sym_exp ~relation ~arr ~idx_traces location cond_set let collection_access ~array_exp ~index_exp ?(is_collection_add = false) mem location cond_set = @@ -349,14 +356,14 @@ module Check = struct let array_access_byte ~arr ~idx ~relation ~is_plus location cond_set = let arr_blk = Dom.Val.get_array_blk arr in let size = ArrayBlk.sizeof_byte arr_blk in - let offset = ArrayBlk.offsetof arr_blk in let idx_itv = Dom.Val.get_itv idx in let idx_traces = Dom.Val.get_traces idx in - let idx_in_blk = (if is_plus then Itv.plus else Itv.minus) offset idx_itv in + let idx = if is_plus then idx_itv else Itv.neg idx_itv in L.(debug BufferOverrun Verbose) - "@[Add condition :@,array: %a@, idx: %a@,@]@." ArrayBlk.pp arr_blk Itv.pp idx_in_blk ; - check_access ~size ~idx:idx_in_blk ~size_sym_exp:None ~idx_sym_exp:None ~relation ~arr - ~idx_traces location cond_set ~is_collection_add:true + "@[Add condition :@,array: %a@, idx: %a + %a@,@]@." ArrayBlk.pp arr_blk Itv.pp + (ArrayBlk.offsetof arr_blk) Itv.pp idx ; + check_access ~size ~idx ~size_sym_exp:None ~idx_sym_exp:None ~relation ~arr ~idx_traces + location cond_set ~is_collection_add:true let lindex_byte ~array_exp ~byte_index_exp mem location cond_set = diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index b53599db6..ecb697e3e 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/infer/src/bufferoverrun/itv.mli @@ -98,6 +98,8 @@ module ItvPure : sig val is_top : t -> bool + val is_zero : t -> bool + val is_one : t -> bool val is_ge_zero : t -> bool @@ -136,6 +138,8 @@ module ItvPure : sig val subst : t -> (Symb.Symbol.t -> Bound.t bottom_lifted) -> t bottom_lifted + val neg : t -> t + val plus : t -> t -> t val minus : t -> t -> t diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/array_content.c b/infer/tests/codetoanalyze/c/bufferoverrun/array_content.c index ea96a5c77..03f6df90a 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/array_content.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/array_content.c @@ -48,7 +48,7 @@ int array_min_index_from_one_FP(int* a, int length) { We need a either a narrowing or a relational domain to prove that index_min < length */ -void call_array_min_index_from_one_good_FP() { +void call_array_min_index_from_one_good() { int a[2]; a[array_min_index_from_one_FP(a, 2) - 1] = 0; } diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/do_while.c b/infer/tests/codetoanalyze/c/bufferoverrun/do_while.c index 3ee10eaea..fe1b5e0e7 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/do_while.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/do_while.c @@ -17,8 +17,12 @@ void do_while_sub(char* a, int len) { } while (i < len); } -void do_while() { +void do_while_Good() { char* a = malloc(10); do_while_sub(a, 10); /* SAFE */ +} + +void do_while_Bad() { + char* a = malloc(10); do_while_sub(a, 11); /* BUG */ } diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/for_loop.c b/infer/tests/codetoanalyze/c/bufferoverrun/for_loop.c index c9b747755..02be909e5 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/for_loop.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/for_loop.c @@ -80,3 +80,19 @@ void malloc_sizeof_value_leak_good() { } /* missing free(x) */ } + +void initialize_arr(int* arr, int count) { + for (int i = 0; i < count; ++i) { + arr[i] = 0; + } +} + +void call_initialize_arr_Good() { + int arr[10]; + initialize_arr(arr, 5); +} + +void call_initialize_arr_Bad() { + int arr[10]; + initialize_arr(arr, 20); +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 61dddd5b5..4dfa06150 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -20,7 +20,6 @@ codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min_Bad, 2, BUFFER_OVERRUN_L2 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, use_int64_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, [] -codetoanalyze/c/bufferoverrun/array_content.c, call_array_min_index_from_one_good_FP, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: a,Assignment,ArrayAccess: Offset: [1, +oo] Size: 2 by call to `array_min_index_from_one_FP` ] codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_arr10_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_arr_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_ptr_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] @@ -40,13 +39,14 @@ codetoanalyze/c/bufferoverrun/cast.c, cast_signed_to_unsigned_Bad_FN, 4, CONDITI codetoanalyze/c/bufferoverrun/cast.c, cast_signed_to_unsigned_Good, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/cast.c, cast_unsigned_to_signed_Bad_FN, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/cast.c, cast_unsigned_to_signed_Good, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] -codetoanalyze/c/bufferoverrun/do_while.c, do_while, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [ArrayDeclaration,Assignment,Call,Parameter: a,Assignment,ArrayAccess: Offset: [0, +oo] Size: 10 by call to `do_while_sub` ] +codetoanalyze/c/bufferoverrun/do_while.c, do_while_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,Call,Parameter: a,Assignment,ArrayAccess: Offset: [0, 10] Size: 10 by call to `do_while_sub` ] codetoanalyze/c/bufferoverrun/duplicates.c, one_alarm_is_enough, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: arr,ArrayAccess: Offset: 1 Size: 1 by call to `two_accesses` ] codetoanalyze/c/bufferoverrun/duplicates.c, tsa_one_alarm_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: n,ArrayAccess: Offset: 3 Size: 1 by call to `two_symbolic_accesses` ] codetoanalyze/c/bufferoverrun/duplicates.c, tsa_two_alarms_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: n,ArrayAccess: Offset: -1 Size: 1 by call to `two_symbolic_accesses` ] codetoanalyze/c/bufferoverrun/duplicates.c, tsa_two_alarms_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: n,ArrayAccess: Offset: 1 Size: 1 by call to `two_symbolic_accesses` ] codetoanalyze/c/bufferoverrun/external.c, extern_bad, 5, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: lib,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/c/bufferoverrun/external.c, extern_bad, 10, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 30 Size: 10] +codetoanalyze/c/bufferoverrun/for_loop.c, call_initialize_arr_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: arr,Assignment,ArrayAccess: Offset: [0, 19] Size: 10 by call to `initialize_arr` ] codetoanalyze/c/bufferoverrun/for_loop.c, call_two_loops_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,Call,Parameter: m,Assignment,Return,ArrayAccess: Offset: 15 Size: 10] codetoanalyze/c/bufferoverrun/for_loop.c, for_loop, 10, BUFFER_OVERRUN_L3, no_bucket, 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, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: -1 Size: 10] diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index da829f660..ff55c48e9 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -126,7 +126,7 @@ codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils. codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addKeyToMap(java.lang.String):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/JsonString.java, libraries.marauder.analytics.utils.json.JsonString.(java.lang.String), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.escape(java.lang.StringBuilder,java.lang.String):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] -codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.escape(java.lang.StringBuilder,java.lang.String):void, 1, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: char[] String.toCharArray(),Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] +codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.escape(java.lang.StringBuilder,java.lang.String):void, 1, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: char[] String.toCharArray(),Assignment,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.escape(java.lang.StringBuilder,java.lang.String):void, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32] codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.serialize(java.lang.String):java.lang.StringBuilder, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.serialize(java.lang.StringBuilder,java.lang.String):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []