From 8f060939d62e71f296e006408258b0fbdbc9ec3f Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Wed, 19 Dec 2018 06:29:13 -0800 Subject: [PATCH] [inferbo] Java pointers, arrays and collections Reviewed By: ezgicicek Differential Revision: D13128600 fbshipit-source-id: 0dd876692 --- .../src/bufferoverrun/bufferOverrunDomain.ml | 30 ++++++-------- infer/src/bufferoverrun/bufferOverrunField.ml | 18 +++++++++ .../src/bufferoverrun/bufferOverrunModels.ml | 40 +++++++++++-------- .../bufferoverrun/bufferOverrunOndemandEnv.ml | 10 +++-- .../bufferoverrun/bufferOverrunSemantics.ml | 5 +-- infer/src/bufferoverrun/bufferOverrunUtils.ml | 22 ++++++---- .../src/bufferoverrun/bufferOverrunUtils.mli | 2 +- infer/src/bufferoverrun/symb.ml | 9 +++-- infer/src/bufferoverrun/symb.mli | 2 +- .../java/bufferoverrun/issues.exp | 2 +- .../codetoanalyze/java/performance/issues.exp | 3 +- 11 files changed, 87 insertions(+), 56 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 774955a1d..e23b2fd44 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -360,9 +360,11 @@ module Val = struct of_itv ~traces (Itv.of_normal_path ~unsigned path) | Tptr (elt, _) -> if is_java then - let l = Loc.of_path path in + let deref_kind = SPath.Deref_JavaPointer in + let deref_path = SPath.deref ~deref_kind path in + let l = Loc.of_path deref_path in let traces = TraceSet.singleton location (Trace.Parameter l) in - {bot with itv= Itv.of_length_path path; powloc= PowLoc.singleton l; traces} + {bot with powloc= PowLoc.singleton l; traces} else let deref_kind = SPath.Deref_CPointer in let deref_path = SPath.deref ~deref_kind path in @@ -384,21 +386,15 @@ module Val = struct {bot with arrayblk; traces} | Tstruct typename -> ( match BufferOverrunTypModels.dispatch tenv typename with - | Some typ_model -> ( - match typ_model with - | CArray {deref_kind; length} -> - let deref_path = SPath.deref ~deref_kind 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 offset = Itv.zero in - let size = Itv.of_int_lit length in - of_c_array_alloc allocsite ~stride:None ~offset ~size ~traces - | JavaCollection -> - let l = Loc.of_path path in - let traces = TraceSet.singleton location (Trace.Parameter l) in - of_itv ~traces (Itv.of_normal_path ~unsigned:true path) ) - | None -> + | Some (CArray {deref_kind; length}) -> + let deref_path = SPath.deref ~deref_kind 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 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 -> let l = Loc.of_path path in let traces = TraceSet.singleton location (Trace.Parameter l) in of_loc ~traces l ) diff --git a/infer/src/bufferoverrun/bufferOverrunField.ml b/infer/src/bufferoverrun/bufferOverrunField.ml index eb981afcc..53f18405c 100644 --- a/infer/src/bufferoverrun/bufferOverrunField.ml +++ b/infer/src/bufferoverrun/bufferOverrunField.ml @@ -15,3 +15,21 @@ 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 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 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 + let get_type fn = Typ.Fieldname.Map.find_opt fn !types in + (mk, get_type) + + +let java_collection_length = + mk "java.collection.length" Typ.(Tint IUInt (* wrong: we need IInt but with unsigned symbol *)) diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index bce5fe2e4..efea89123 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -205,20 +205,24 @@ let infer_print e = {exec; check= no_check} +(* Java only *) let get_array_length array_exp = - let exec {integer_type_widths} ~ret mem = - let arr = Sem.eval integer_type_widths array_exp mem in - let traces = Dom.Val.get_traces arr in - let length = - if Language.curr_language_is Java then arr |> Dom.Val.get_itv - else arr |> Dom.Val.get_array_blk |> ArrayBlk.sizeof + 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 = Dom.Val.of_itv ~traces length in model_by_value result ret mem in {exec; check= no_check} +(* Clang only *) let set_array_length array length_exp = let exec {pname; node_hash; location; integer_type_widths} ~ret:_ mem = match array with @@ -310,7 +314,7 @@ end - 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_list _ = + 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 @@ -319,18 +323,22 @@ module Collection = struct ~represents_multiple_values:true in let alloc_loc = Loc.of_allocsite allocsite in - let init_size = Dom.Val.of_int 0 in + let init_length = Dom.Val.of_int 0 in let traces = Trace.(Set.singleton location ArrayDeclaration) in let v = Dom.Val.of_pow_loc (PowLoc.singleton alloc_loc) ~traces in - mem |> Dom.Mem.add_stack loc v |> Dom.Mem.add_heap alloc_loc init_size + 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 in {exec; check= no_check} - let change_size_by ~size_f alist_id _ ~ret:_ mem = - let alist_v = Dom.Mem.find (Loc.of_id alist_id) mem in - let locs = Dom.Val.get_pow_loc alist_v in - Dom.Mem.transform_mem ~f:size_f locs mem + 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 incr_size = Dom.Val.plus_a Dom.Val.Itv.one @@ -340,7 +348,7 @@ module Collection = struct 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_alist_size (Sem.eval integer_type_widths alist mem) mem + BoUtils.Exec.get_java_collection_length (Sem.eval integer_type_widths alist mem) mem let size array_exp = @@ -438,7 +446,7 @@ module Call = struct ; -"calloc" <>$ capt_exp $+ capt_exp $!--> calloc ; -"__new" <>$ capt_exp_of_typ (+PatternMatch.implements_collection) - $+...$--> Collection.new_list + $+...$--> Collection.new_collection ; -"__new" <>$ capt_exp $+...$--> malloc ; -"__new_array" <>$ capt_exp $+...$--> malloc ; -"__placement_new" <>$ capt_exp $+ capt_arg $+? capt_arg $!--> placement_new diff --git a/infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml b/infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml index 989c601db..514270f83 100644 --- a/infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml +++ b/infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml @@ -46,9 +46,13 @@ let mk pdesc = L.(die InternalError) "Deref of unmodeled type `%a`" Typ.Name.pp typename ) | _ -> L.(die InternalError) "Untyped expression is given." ) - | SPath.Field (fn, x) -> - let lookup = Tenv.lookup tenv in - Option.map (typ_of_param_path x) ~f:(Typ.Struct.fld_typ ~lookup ~default:Typ.void fn) + | SPath.Field (fn, x) -> ( + match BufferOverrunField.get_type fn with + | None -> + let lookup = Tenv.lookup tenv in + Option.map (typ_of_param_path x) ~f:(Typ.Struct.fld_typ ~lookup ~default:Typ.void fn) + | some_typ -> + some_typ ) | SPath.Callsite {ret_typ} -> Some ret_typ in diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 959d5f90b..9adb45c89 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -383,10 +383,7 @@ let eval_sympath params sympath mem = (ArrayBlk.offsetof (Val.get_array_blk v), Val.get_traces v) | Symb.SymbolPath.Length p -> let v = eval_sympath_partial params p mem in - let traces = Val.get_traces v in - let itv = ArrayBlk.sizeof (Val.get_array_blk v) in - let itv = if Language.curr_language_is Java then Itv.join itv (Val.get_itv v) else itv in - (itv, traces) + (ArrayBlk.sizeof (Val.get_array_blk v), Val.get_traces v) let mk_eval_sym_trace integer_type_widths callee_pdesc actual_exps caller_mem = diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index 6210a2241..56cd8739b 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -17,9 +17,12 @@ module Trace = BufferOverrunTrace module TraceSet = Trace.Set module Exec = struct - let get_alist_size alist mem = - let size_powloc = Dom.Val.get_pow_loc alist in - Dom.Mem.find_set size_powloc mem + 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 = @@ -110,14 +113,17 @@ module Exec = struct let alloc_loc = Loc.of_allocsite allocsite in let traces = Trace.(Set.singleton location ArrayDeclaration) in let mem = - let alist = + 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 alist mem + if Int.equal dimension 1 then Dom.Mem.add_stack loc collection mem else - let size = Dom.Val.of_itv ~traces Itv.zero in - Dom.Mem.add_heap loc alist mem |> Dom.Mem.add_heap alloc_loc size + 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) @@ -260,7 +266,7 @@ module Check = struct 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_alist_size arr mem |> Dom.Val.get_itv 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 diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.mli b/infer/src/bufferoverrun/bufferOverrunUtils.mli index 0036b0465..44c831fd1 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.mli +++ b/infer/src/bufferoverrun/bufferOverrunUtils.mli @@ -12,7 +12,7 @@ module Relation = BufferOverrunDomainRelation module PO = BufferOverrunProofObligations module Exec : sig - val get_alist_size : Dom.Val.t -> Dom.Mem.t -> Dom.Val.t + 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 diff --git a/infer/src/bufferoverrun/symb.ml b/infer/src/bufferoverrun/symb.ml index f8179cfd8..aa211fa78 100644 --- a/infer/src/bufferoverrun/symb.ml +++ b/infer/src/bufferoverrun/symb.ml @@ -16,7 +16,7 @@ module BoundEnd = struct end module SymbolPath = struct - type deref_kind = Deref_ArrayIndex | Deref_CPointer [@@deriving compare] + type deref_kind = Deref_ArrayIndex | Deref_CPointer | Deref_JavaPointer [@@deriving compare] type partial = | Pvar of Pvar.t @@ -57,9 +57,11 @@ module SymbolPath = struct let rec pp_partial_paren ~paren fmt = function | Pvar pvar -> Pvar.pp_value fmt pvar + | Deref (Deref_JavaPointer, p) when Config.bo_debug < 3 -> + pp_partial_paren ~paren fmt p | Deref (Deref_ArrayIndex, p) -> F.fprintf fmt "%a[*]" (pp_partial_paren ~paren:true) p - | Deref (Deref_CPointer, p) -> + | Deref ((Deref_CPointer | Deref_JavaPointer), p) -> pp_pointer ~paren fmt p | Field (fn, Deref (Deref_CPointer, p)) -> BufferOverrunField.pp ~pp_lhs:(pp_partial_paren ~paren:true) @@ -95,7 +97,8 @@ module SymbolPath = struct | Deref (Deref_ArrayIndex, _) -> true | Deref (Deref_CPointer, p) - (* unsound but avoids many FPs for non-array pointers *) + (* Deref_CPointer is unsound here but avoids many FPs for non-array pointers *) + | Deref (Deref_JavaPointer, p) | Field (_, p) -> represents_multiple_values p diff --git a/infer/src/bufferoverrun/symb.mli b/infer/src/bufferoverrun/symb.mli index e5a2deaf5..63f4819dd 100644 --- a/infer/src/bufferoverrun/symb.mli +++ b/infer/src/bufferoverrun/symb.mli @@ -15,7 +15,7 @@ module BoundEnd : sig end module SymbolPath : sig - type deref_kind = Deref_ArrayIndex | Deref_CPointer [@@deriving compare] + type deref_kind = Deref_ArrayIndex | Deref_CPointer | Deref_JavaPointer [@@deriving compare] type partial = private | Pvar of Pvar.t diff --git a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp index d9c62fe1c..cc0c9972d 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/CompressedData.java, codetoanalyze.java.bufferoverrun.CompressedData.decompressData(codetoanalyze.java.bufferoverrun.CompressedData$D):int, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,,Assignment,Binary operation: ([0, this.yy.ub - 1] × [-oo, +oo]):signed32] +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/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index ae6d7bfe2..6506f3473 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -54,7 +54,7 @@ codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_ 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_U5, no_bucket, ERROR, [Unknown value from: __cast,Assignment,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_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_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] @@ -165,7 +165,6 @@ codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops. codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2] -codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Parameter `a`,,Parameter `b`,Binary operation: (a.length × b.length):signed64] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 9, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2]