[inferbo] Java pointers, arrays and collections

Reviewed By: ezgicicek

Differential Revision: D13128600

fbshipit-source-id: 0dd876692

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,9 +386,7 @@ 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} ->
+      | 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
@@ -394,11 +394,7 @@ 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
-        | 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 JavaCollection | None ->
           let l = Loc.of_path path in
           let traces = TraceSet.singleton location (Trace.Parameter l) in
           of_loc ~traces l )

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 *))

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 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 =
-      if Language.curr_language_is Java then arr |> Dom.Val.get_itv
-      else arr |> Dom.Val.get_array_blk |> ArrayBlk.sizeof
+        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

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) ->
+      | 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

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 =

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

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
 

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
 

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

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, [<Length trace>,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, [<LHS trace>,Assignment,<RHS trace>,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, [<LHS trace>,Assignment,<RHS trace>,Parameter `d.cci[*].s`,Assignment,Binary operation: ([0, this.yy.ub - 1] × d.cci[*].s):signed32]

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,<LHS trace>,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,<LHS trace>,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, [<LHS trace>,Parameter `a`,<RHS trace>,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]