From 33aa07357fc8ae7c6ba6ccca6f6e78704aecb4c1 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Thu, 20 Dec 2018 11:01:52 -0800 Subject: [PATCH] [inferbo] Model Java collections using arrays Reviewed By: ezgicicek, skcho Differential Revision: D13190960 fbshipit-source-id: fba435f34 --- infer/src/bufferoverrun/arrayBlk.ml | 15 ++ .../src/bufferoverrun/bufferOverrunChecker.ml | 13 +- .../src/bufferoverrun/bufferOverrunDomain.ml | 18 +- infer/src/bufferoverrun/bufferOverrunField.ml | 18 +- .../src/bufferoverrun/bufferOverrunModels.ml | 165 ++++++++++-------- infer/src/bufferoverrun/bufferOverrunUtils.ml | 54 ------ .../src/bufferoverrun/bufferOverrunUtils.mli | 23 --- infer/src/bufferoverrun/itv.ml | 4 + infer/src/bufferoverrun/itv.mli | 4 + .../java/bufferoverrun/Array.java | 7 +- .../java/bufferoverrun/issues.exp | 2 +- .../java/performance/CollectionTest.java | 4 +- .../codetoanalyze/java/performance/issues.exp | 26 +-- 13 files changed, 160 insertions(+), 193 deletions(-) diff --git a/infer/src/bufferoverrun/arrayBlk.ml b/infer/src/bufferoverrun/arrayBlk.ml index 828d502ca..acf7d8f54 100644 --- a/infer/src/bufferoverrun/arrayBlk.ml +++ b/infer/src/bufferoverrun/arrayBlk.ml @@ -180,6 +180,17 @@ module ArrInfo = struct Top + let transform_length : f:(Itv.t -> Itv.t) -> t -> t = + fun ~f arr -> + match arr with + | C {offset; size; stride} -> + C {offset; size= f size; stride} + | Java {length} -> + Java {length= f length} + | Top -> + Top + + (* Set new stride only when the previous stride is a constant interval. *) let set_stride : Z.t -> t -> t = fun new_stride arr -> @@ -320,3 +331,7 @@ let lift_cmp_itv cmp_itv cmp_loc arr1 arr2 = (Allocsite.eq as1 as2)) | _ -> Boolean.Top + + +let transform_length : f:(Itv.t -> Itv.t) -> t -> t = + fun ~f a -> map (ArrInfo.transform_length ~f) a diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index afd48dd0d..983a100e2 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -45,15 +45,10 @@ module Init = struct ?stride ~inst_num ~represents_multiple_values ~dimension mem | Typ.Tstruct typname -> ( match TypModels.dispatch tenv typname with - | Some typ_model -> ( - match typ_model with - | CArray {element_typ; length} -> - BoUtils.Exec.decl_local_array ~decl_local pname ~node_hash location loc element_typ - ~length:(Some length) ~inst_num ~represents_multiple_values ~dimension mem - | JavaCollection -> - BoUtils.Exec.decl_local_collection pname ~node_hash location loc ~inst_num - ~represents_multiple_values ~dimension mem ) - | None -> + | Some (CArray {element_typ; length}) -> + BoUtils.Exec.decl_local_array ~decl_local pname ~node_hash location loc element_typ + ~length:(Some length) ~inst_num ~represents_multiple_values ~dimension mem + | Some JavaCollection | None -> (mem, inst_num) ) | _ -> (mem, inst_num) diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 4e7b88209..9d91d9431 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -352,6 +352,13 @@ module Val = struct ; traces= Trace.(Set.add_elem location ArrayDeclaration) length.traces } + let transform_array_length : Location.t -> f:(Itv.t -> Itv.t) -> t -> t = + fun location ~f v -> + { v with + arrayblk= ArrayBlk.transform_length ~f v.arrayblk + ; traces= Trace.(Set.add_elem location Through) v.traces } + + let set_array_stride : Z.t -> t -> t = fun new_stride v -> PhysEqual.optim1 v ~res:{v with arrayblk= ArrayBlk.set_stride new_stride v.arrayblk} @@ -408,7 +415,14 @@ module Val = struct let offset = Itv.zero in let size = Itv.of_int_lit length in of_c_array_alloc allocsite ~stride:None ~offset ~size ~traces - | Some JavaCollection | None -> + | Some JavaCollection -> + let deref_path = SPath.deref ~deref_kind:Deref_ArrayIndex path in + let l = Loc.of_path deref_path in + let traces = TraceSet.singleton location (Trace.Parameter l) in + let allocsite = Allocsite.make_symbol deref_path in + let length = Itv.of_length_path path in + of_java_array_alloc allocsite ~length ~traces + | None -> let l = Loc.of_path path in let traces = TraceSet.singleton location (Trace.Parameter l) in of_loc ~traces l ) @@ -458,8 +472,6 @@ module Val = struct let nat = of_itv Itv.nat - let one = of_itv Itv.one - let pos = of_itv Itv.pos let top = of_itv Itv.top diff --git a/infer/src/bufferoverrun/bufferOverrunField.ml b/infer/src/bufferoverrun/bufferOverrunField.ml index 53f18405c..e132e8b97 100644 --- a/infer/src/bufferoverrun/bufferOverrunField.ml +++ b/infer/src/bufferoverrun/bufferOverrunField.ml @@ -10,20 +10,29 @@ module F = Format (** If fn is empty, prints [pp_lhs_alone lhs] Otherwise prints [pp_lhs lhs ^ sep ^ fn] + + Create invisible phantom fields by giving them a name ending in '.' + The name preceeding the '.' will be used in debug mode. *) let pp ~pp_lhs ~pp_lhs_alone ~sep f lhs fn = let fieldname = Typ.Fieldname.to_flat_string fn in - if String.is_empty fieldname then pp_lhs_alone f lhs + if String.is_empty fieldname then + if Config.bo_debug > 0 then + let fieldname = + Option.value ~default:"" + (Typ.Fieldname.to_simplified_string fn |> String.chop_suffix ~suffix:".") + in + F.fprintf f "%a%s%s" pp_lhs lhs sep fieldname + else pp_lhs_alone f lhs else F.fprintf f "%a%s%s" pp_lhs lhs sep fieldname let mk, get_type = let classname = "__infer__" in let types = ref Typ.Fieldname.Map.empty in - let mk name typ_desc = + let mk name typ = let fullname = Format.sprintf "%s.%s" classname name in let fieldname = Typ.Fieldname.Java.from_string fullname in - let typ = Typ.mk typ_desc in types := Typ.Fieldname.Map.add fieldname typ !types ; fieldname in @@ -31,5 +40,4 @@ let mk, get_type = (mk, get_type) -let java_collection_length = - mk "java.collection.length" Typ.(Tint IUInt (* wrong: we need IInt but with unsigned symbol *)) +let java_collection_internal_array = mk "java.collection.$elements." Typ.(mk_array void) diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index efea89123..9af616361 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -205,18 +205,19 @@ let infer_print e = {exec; check= no_check} +let eval_array_locs_length arr_locs mem = + if PowLoc.is_empty arr_locs then Dom.Val.Itv.top + else + let arr = Dom.Mem.find_set arr_locs mem in + let traces = Dom.Val.get_traces arr in + let length = arr |> Dom.Val.get_array_blk |> ArrayBlk.sizeof in + Dom.Val.of_itv ~traces length + + (* Java only *) let get_array_length array_exp = let exec _ ~ret mem = - let arr_locs = Sem.eval_locs array_exp mem in - let result = - if PowLoc.is_empty arr_locs then Dom.Val.Itv.top - else - let arr = Dom.Mem.find_set arr_locs mem in - let traces = Dom.Val.get_traces arr in - let length = arr |> Dom.Val.get_array_blk |> ArrayBlk.sizeof in - Dom.Val.of_itv ~traces length - in + let result = eval_array_locs_length (Sem.eval_locs array_exp mem) mem in model_by_value result ret mem in {exec; check= no_check} @@ -309,123 +310,133 @@ module StdArray = struct {exec; check= no_check} end -(* Java's Collections are represented by their size. We don't care about the elements. +(* Java's Collections are represented like arrays. But 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 *) module Collection = struct let new_collection _ = let exec {pname; node_hash; location} ~ret:(id, _) mem = - let loc = Loc.of_id id in - let path = Option.bind (Dom.Mem.find_simple_alias id mem) ~f:Loc.get_path in - let allocsite = - Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 ~path - ~represents_multiple_values:true - in - let alloc_loc = Loc.of_allocsite allocsite in - let init_length = Dom.Val.of_int 0 in + let represents_multiple_values = true in let traces = Trace.(Set.singleton location ArrayDeclaration) in - let v = Dom.Val.of_pow_loc (PowLoc.singleton alloc_loc) ~traces in - let length_loc = Loc.append_field alloc_loc ~fn:BufferOverrunField.java_collection_length in - mem |> Dom.Mem.add_stack loc v |> Dom.Mem.add_heap length_loc init_length + let coll_allocsite = + Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 ~path:None + ~represents_multiple_values + in + let internal_array = + let allocsite = + Allocsite.make pname ~node_hash ~inst_num:1 ~dimension:1 ~path:None + ~represents_multiple_values + in + Dom.Val.of_java_array_alloc allocsite ~length:Itv.zero ~traces + in + let coll_loc = Loc.of_allocsite coll_allocsite in + let internal_array_loc = + Loc.append_field coll_loc ~fn:BufferOverrunField.java_collection_internal_array + in + mem + |> Dom.Mem.add_heap internal_array_loc internal_array + |> Dom.Mem.add_stack (Loc.of_id id) + (coll_loc |> PowLoc.singleton |> Dom.Val.of_pow_loc ~traces) in {exec; check= no_check} - let change_size_by ~size_f collection_id _ ~ret:_ mem = - let collection_v = Dom.Mem.find (Loc.of_id collection_id) mem in - let collection_locs = Dom.Val.get_pow_loc collection_v in - let length_locs = - PowLoc.append_field collection_locs ~fn:BufferOverrunField.java_collection_length - in - Dom.Mem.transform_mem ~f:size_f length_locs mem + let eval_collection_internal_array_locs coll_exp mem = + Sem.eval_locs coll_exp mem + |> PowLoc.append_field ~fn:BufferOverrunField.java_collection_internal_array + + let get_collection_internal_array_locs coll_id mem = + let coll = Dom.Mem.find (Loc.of_id coll_id) mem in + Dom.Val.get_pow_loc coll + |> PowLoc.append_field ~fn:BufferOverrunField.java_collection_internal_array - let incr_size = Dom.Val.plus_a Dom.Val.Itv.one - let decr_size size = Dom.Val.minus_a size Dom.Val.Itv.one + let eval_collection_length coll_exp mem = + let arr_locs = eval_collection_internal_array_locs coll_exp mem in + eval_array_locs_length arr_locs mem - let add alist_id = {exec= change_size_by ~size_f:incr_size alist_id; check= no_check} - let get_size integer_type_widths alist mem = - BoUtils.Exec.get_java_collection_length (Sem.eval integer_type_widths alist mem) mem + let change_size_by ~size_f coll_id {location} ~ret:_ mem = + Dom.Mem.transform_mem + ~f:(Dom.Val.transform_array_length location ~f:size_f) + (get_collection_internal_array_locs coll_id mem) + mem - let size array_exp = - let exec {integer_type_widths} ~ret mem = - let size = get_size integer_type_widths array_exp mem in - model_by_value size ret mem + let add coll_id = {exec= change_size_by ~size_f:Itv.incr coll_id; check= no_check} + + let size coll_exp = + let exec _ ~ret mem = + let result = eval_collection_length coll_exp mem in + model_by_value result ret mem in {exec; check= no_check} - let iterator alist = + let iterator coll_exp = let exec {integer_type_widths} ~ret mem = - let itr = Sem.eval integer_type_widths alist mem in + let itr = Sem.eval integer_type_widths coll_exp mem in model_by_value itr ret mem in {exec; check= no_check} let hasNext iterator = - let exec {integer_type_widths} ~ret mem = + let exec _ ~ret mem = (* Set the size of the iterator to be [0, size-1], so that range will be size of the collection. *) - let collection_size = - get_size integer_type_widths iterator mem |> Dom.Val.get_iterator_itv - in + let collection_size = eval_collection_length iterator mem |> Dom.Val.get_iterator_itv in model_by_value collection_size ret mem in {exec; check= no_check} - let addAll alist_id alist_to_add = - let exec ({integer_type_widths} as model_env) ~ret mem = - let to_add_length = get_size integer_type_widths alist_to_add mem in - change_size_by ~size_f:(Dom.Val.plus_a to_add_length) alist_id model_env ~ret mem + let addAll coll_id coll_to_add = + let exec model_env ~ret mem = + let to_add_length = eval_collection_length coll_to_add mem |> Dom.Val.get_itv in + change_size_by ~size_f:(Itv.plus to_add_length) coll_id model_env ~ret mem in {exec; check= no_check} - let add_at_index (alist_id : Ident.t) index_exp = - let check {location; integer_type_widths} mem cond_set = - let array_exp = Exp.Var alist_id in - BoUtils.Check.collection_access integer_type_widths ~array_exp ~index_exp ~last_included:true - mem location cond_set + let check_index ~last_included coll_id index_exp {location; integer_type_widths} mem cond_set = + let arr = + let arr_locs = get_collection_internal_array_locs coll_id mem in + Dom.Mem.find_set arr_locs mem + in + let idx = Sem.eval integer_type_widths index_exp mem in + let idx_sym_exp = + Relation.SymExp.of_exp ~get_sym_f:(Sem.get_sym_f integer_type_widths mem) index_exp in - {exec= change_size_by ~size_f:incr_size alist_id; check} + let relation = Dom.Mem.get_relation mem in + let latest_prune = Dom.Mem.get_latest_prune mem in + BoUtils.Check.array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus:true ~last_included + ~latest_prune location cond_set - let remove_at_index alist_id index_exp = - let check {location; integer_type_widths} mem cond_set = - let array_exp = Exp.Var alist_id in - BoUtils.Check.collection_access integer_type_widths ~array_exp ~index_exp - ~last_included:false mem location cond_set - in - {exec= change_size_by ~size_f:decr_size alist_id; check} + let add_at_index (coll_id : Ident.t) index_exp = + { exec= change_size_by ~size_f:Itv.incr coll_id + ; check= check_index ~last_included:true coll_id index_exp } - let addAll_at_index alist_id index_exp alist_to_add = - let exec ({integer_type_widths} as model_env) ~ret mem = - let to_add_length = get_size integer_type_widths alist_to_add mem in - change_size_by ~size_f:(Dom.Val.plus_a to_add_length) alist_id model_env ~ret mem - in - let check {location; integer_type_widths} mem cond_set = - let array_exp = Exp.Var alist_id in - BoUtils.Check.collection_access integer_type_widths ~index_exp ~array_exp ~last_included:true - mem location cond_set + let remove_at_index coll_id index_exp = + { exec= change_size_by ~size_f:Itv.decr coll_id + ; check= check_index ~last_included:false coll_id index_exp } + + + let addAll_at_index coll_id index_exp coll_to_add = + let exec model_env ~ret mem = + let to_add_length = eval_collection_length coll_to_add mem |> Dom.Val.get_itv in + change_size_by ~size_f:(Itv.plus to_add_length) coll_id model_env ~ret mem in - {exec; check} + {exec; check= check_index ~last_included:true coll_id index_exp} - let get_or_set_at_index alist_id index_exp = + let get_or_set_at_index coll_id index_exp = let exec _model_env ~ret:_ mem = mem in - let check {location; integer_type_widths} mem cond_set = - let array_exp = Exp.Var alist_id in - BoUtils.Check.collection_access integer_type_widths ~index_exp ~array_exp - ~last_included:false mem location cond_set - in - {exec; check} + {exec; check= check_index ~last_included:false coll_id index_exp} end module Call = struct diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index 56cd8739b..fddc20f62 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -17,14 +17,6 @@ module Trace = BufferOverrunTrace module TraceSet = Trace.Set module Exec = struct - let get_java_collection_length alist mem = - let collection_locs = Dom.Val.get_pow_loc alist in - let length_locs = - PowLoc.append_field collection_locs ~fn:BufferOverrunField.java_collection_length - in - Dom.Mem.find_set length_locs mem - - let load_locs id locs mem = let v = Dom.Mem.find_set locs mem in let mem = Dom.Mem.add_stack (Loc.of_id id) v mem in @@ -95,39 +87,6 @@ module Exec = struct (mem, inst_num + 1) - let decl_local_collection : - Typ.Procname.t - -> node_hash:int - -> Location.t - -> Loc.t - -> inst_num:int - -> represents_multiple_values:bool - -> dimension:int - -> Dom.Mem.t - -> Dom.Mem.t * int = - fun pname ~node_hash location loc ~inst_num ~represents_multiple_values ~dimension mem -> - let path = Loc.get_path loc in - let allocsite = - Allocsite.make pname ~node_hash ~inst_num ~dimension ~path ~represents_multiple_values:true - in - let alloc_loc = Loc.of_allocsite allocsite in - let traces = Trace.(Set.singleton location ArrayDeclaration) in - let mem = - let collection = - Dom.Val.of_pow_loc (PowLoc.singleton alloc_loc) ~traces - |> Dom.Val.sets_represents_multiple_values ~represents_multiple_values - in - if Int.equal dimension 1 then Dom.Mem.add_stack loc collection mem - else - let length = Dom.Val.of_itv ~traces Itv.zero in - let length_loc = - Loc.append_field alloc_loc ~fn:BufferOverrunField.java_collection_length - in - Dom.Mem.add_heap loc collection mem |> Dom.Mem.add_heap length_loc length - in - (mem, inst_num + 1) - - let init_c_array_fields tenv integer_type_widths pname path ~node_hash typ locs ?dyn_length mem = let rec init_field path locs dimension ?dyn_length (mem, inst_num) (field_name, field_typ, _) = let field_path = Option.map path ~f:(fun path -> Symb.SymbolPath.field path field_name) in @@ -261,19 +220,6 @@ module Check = struct ~latest_prune location cond_set - let collection_access integer_type_widths ~array_exp ~index_exp ~last_included mem location - cond_set = - let idx = Sem.eval integer_type_widths index_exp mem in - let arr = Sem.eval integer_type_widths array_exp mem in - let idx_traces = Dom.Val.get_traces idx in - let size = Exec.get_java_collection_length arr mem |> Dom.Val.get_itv in - let idx = Dom.Val.get_itv idx in - let relation = Dom.Mem.get_relation mem in - let latest_prune = Dom.Mem.get_latest_prune mem in - check_access ~size ~idx ~size_sym_exp:None ~idx_sym_exp:None ~relation ~arr ~idx_traces - ~last_included ~latest_prune location cond_set - - let lindex integer_type_widths ~array_exp ~index_exp ~last_included mem location cond_set = let idx = Sem.eval integer_type_widths index_exp mem in let arr = Sem.eval_arr integer_type_widths array_exp mem in diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.mli b/infer/src/bufferoverrun/bufferOverrunUtils.mli index 44c831fd1..96e92744b 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.mli +++ b/infer/src/bufferoverrun/bufferOverrunUtils.mli @@ -12,8 +12,6 @@ module Relation = BufferOverrunDomainRelation module PO = BufferOverrunProofObligations module Exec : sig - val get_java_collection_length : Dom.Val.t -> Dom.Mem.t -> Dom.Val.t - val load_locs : Ident.t -> PowLoc.t -> Dom.Mem.t -> Dom.Mem.t val load_val : Ident.t -> Dom.Val.t -> Dom.Mem.t -> Dom.Mem.t @@ -45,17 +43,6 @@ module Exec : sig -> Dom.Mem.t -> Dom.Mem.t * int - val decl_local_collection : - Typ.Procname.t - -> node_hash:int - -> Location.t - -> Loc.t - -> inst_num:int - -> represents_multiple_values:bool - -> dimension:int - -> Dom.Mem.t - -> Dom.Mem.t * int - val init_c_array_fields : Tenv.t -> Typ.IntegerWidths.t @@ -114,16 +101,6 @@ module Check : sig -> PO.ConditionSet.checked_t -> PO.ConditionSet.checked_t - val collection_access : - Typ.IntegerWidths.t - -> array_exp:Exp.t - -> index_exp:Exp.t - -> last_included:bool - -> Dom.Mem.t - -> Location.t - -> PO.ConditionSet.checked_t - -> PO.ConditionSet.checked_t - val binary_operation : Typ.IntegerWidths.t -> Binop.t diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index ed1af90db..afbcb11b2 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -553,6 +553,10 @@ let plus : t -> t -> t = lift2 ItvPure.plus let minus : t -> t -> t = lift2 ItvPure.minus +let incr = plus one + +let decr x = minus x one + let get_iterator_itv : t -> t = lift1 ItvPure.get_iterator_itv let is_const : t -> Z.t option = bind1zo ItvPure.is_const diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index 516285351..64a17daa2 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/infer/src/bufferoverrun/itv.mli @@ -147,6 +147,10 @@ val get_bound : t -> Symb.BoundEnd.t -> Bound.t bottom_lifted val is_false : t -> bool +val decr : t -> t + +val incr : t -> t + val neg : t -> t val normalize : t -> t diff --git a/infer/tests/codetoanalyze/java/bufferoverrun/Array.java b/infer/tests/codetoanalyze/java/bufferoverrun/Array.java index 4a839eac1..019bbecaf 100644 --- a/infer/tests/codetoanalyze/java/bufferoverrun/Array.java +++ b/infer/tests/codetoanalyze/java/bufferoverrun/Array.java @@ -15,14 +15,9 @@ class Array { a.add(0, 100); } - ArrayList collection_add_zero_Bad() { + ArrayList collection_remove_from_empty_Bad() { ArrayList b = new ArrayList<>(); b.remove(0); return b; } - - void collection_add_zero2_Good() { - ArrayList b = collection_add_zero_Bad(); - b.add(0, 100); - } } diff --git a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp index cc0c9972d..1af2b5475 100644 --- a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp @@ -1,2 +1,2 @@ -codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.collection_add_zero_Bad():java.util.ArrayList, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset: 0 Size: 0] +codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.collection_remove_from_empty_Bad():java.util.ArrayList, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 0 Size: 0] codetoanalyze/java/bufferoverrun/CompressedData.java, codetoanalyze.java.bufferoverrun.CompressedData.decompressData(codetoanalyze.java.bufferoverrun.CompressedData$D):int, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,,Parameter `d.cci[*].s`,Assignment,Binary operation: ([0, this.yy.ub - 1] × d.cci[*].s):signed32] diff --git a/infer/tests/codetoanalyze/java/performance/CollectionTest.java b/infer/tests/codetoanalyze/java/performance/CollectionTest.java index b0d4f283a..648862b26 100644 --- a/infer/tests/codetoanalyze/java/performance/CollectionTest.java +++ b/infer/tests/codetoanalyze/java/performance/CollectionTest.java @@ -21,9 +21,9 @@ public class CollectionTest { for (MyCollection list : mSubscribers) {} } - // Expected |mSubscribers| * |list| but we get T + // Expected |mSubscribers| * |list| but we get |mSubscribers| // because we are not tracking elements of collections - void iterate_over_mycollection_quad_FP( + void iterate_over_mycollection_quad_FN( ConcurrentLinkedQueue> mSubscribers) { for (MyCollection list : mSubscribers) { iterate_over_mycollection(list); diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index 6506f3473..3a780484f 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -8,23 +8,23 @@ codetoanalyze/java/performance/ArrayCost.java, ArrayCost.isPowOfTwo_FP(int):bool codetoanalyze/java/performance/ArrayCost.java, ArrayCost.isPowOfTwo_FP(int):boolean, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 884, degree = 0] codetoanalyze/java/performance/ArrayCost.java, ArrayCost.isPowOfTwo_FP(int):boolean, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 883, degree = 0] codetoanalyze/java/performance/ArrayCost.java, ArrayCost.isPowOfTwo_FP(int):boolean, 12, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 890, degree = 0] -codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_add3_overrun_bad():void, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset added: 4 Size: 3] -codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_addAll_bad():void, 10, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset added: 5 Size: 4] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_add3_overrun_bad():void, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Through,Through,Through,Array access: Offset added: 4 Size: 3] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_addAll_bad():void, 10, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Through,Through,Through,Array access: Offset added: 5 Size: 4] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_add_in_loop_FP():void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_add_in_loop_FP():void, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_add_in_loop_ok():void, 19, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 202, degree = 0] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_add_in_loop_ok():void, 19, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 201, degree = 0] -codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_empty_overrun_bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset added: 1 Size: 0] -codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_empty_underrun_bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset added: -1 Size: 0] -codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_get_overrun_bad():void, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset: 2 Size: 1] -codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_get_underrun_bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset: 0 Size: 0] -codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remove_bad():void, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset: 1 Size: 1] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_empty_overrun_bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset added: 1 Size: 0] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_empty_underrun_bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset added: -1 Size: 0] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_get_overrun_bad():void, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Through,Array access: Offset: 2 Size: 1] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_get_underrun_bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 0 Size: 0] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remove_bad():void, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Through,Through,Through,Array access: Offset: 1 Size: 1] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remove_in_loop_Good_FP():void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remove_in_loop_Good_FP():void, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] -codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remove_in_loop_Good_FP():void, 6, BUFFER_OVERRUN_L5, no_bucket, ERROR, [,Assignment,,Array declaration,Assignment,Array access: Offset: [0, +oo] Size: [0, +oo]] -codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remove_overrun_bad():void, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset: 1 Size: 1] -codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_set_overrun_bad():void, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset: 1 Size: 1] -codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_set_underrun_bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset: 0 Size: 0] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remove_in_loop_Good_FP():void, 6, BUFFER_OVERRUN_L5, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: [0, +oo] Size: [0, +oo]] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remove_overrun_bad():void, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Through,Array access: Offset: 1 Size: 1] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_set_overrun_bad():void, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Through,Array access: Offset: 1 Size: 1] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_set_underrun_bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 0 Size: 0] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 5 ⋅ list.length.ub, degree = 1] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ list.length.ub, degree = 1] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_shortcut_FP(java.util.ArrayList):boolean, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 13 ⋅ (list.length.ub - 1) + 2 ⋅ (list.length.ub - 1) × (-Integer.intValue().lb + 11) + 4 ⋅ list.length.ub × (-Integer.intValue().lb + 11), degree = 2] @@ -53,8 +53,8 @@ codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_ codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_call_quad(int,CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 21 ⋅ (list.length.ub - 1) + 5 ⋅ (list.length.ub - 1) × list.length.ub + 4 ⋅ list.length.ub, degree = 2] codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_mycollection(CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ list.length.ub, degree = 1] codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_mycollection(CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 5 ⋅ list.length.ub, degree = 1] -codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_mycollection_quad_FP(java.util.concurrent.ConcurrentLinkedQueue):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] -codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_mycollection_quad_FP(java.util.concurrent.ConcurrentLinkedQueue):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,,Assignment,Binary operation: ([0, +oo] + 1):signed32 by call to `void CollectionTest.iterate_over_mycollection(CollectionTest$MyCollection)` ] +codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_mycollection_quad_FN(java.util.concurrent.ConcurrentLinkedQueue):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 21 ⋅ (mSubscribers.length.ub - 1) + 4 ⋅ mSubscribers.length.ub, degree = 1] +codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_mycollection_quad_FN(java.util.concurrent.ConcurrentLinkedQueue):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 21 ⋅ (mSubscribers.length.ub - 1) + 4 ⋅ mSubscribers.length.ub, degree = 1] codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_some_java_collection(java.util.concurrent.ConcurrentLinkedQueue):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 9 ⋅ (mSubscribers.length.ub - 1) + 4 ⋅ mSubscribers.length.ub, degree = 1] codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_some_java_collection(java.util.concurrent.ConcurrentLinkedQueue):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 9 ⋅ (mSubscribers.length.ub - 1) + 4 ⋅ mSubscribers.length.ub, degree = 1] codetoanalyze/java/performance/CollectionTest.java, CollectionTest.loop_over_call(int,CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 17 ⋅ size.ub + 5 ⋅ size.ub × list.length.ub, degree = 2]