Fix Java's handling of pointer parameters in Inferbo

Reviewed By: mbouaziz, skcho

Differential Revision: D8950535

fbshipit-source-id: 5691eb898

infer/src/IR/Typ.ml

@@ -172,6 +172,8 @@ let is_restrict {is_restrict} = is_restrict
 
 let is_volatile {is_volatile} = is_volatile
 
+let is_array {desc} = match desc with Tarray _ -> true | _ -> false
+
 let mk ?default ?quals desc : t =
   let default_ = {desc; quals= mk_type_quals ()} in
   let mk_aux ?(default= default_) ?(quals= default.quals) desc = {desc; quals} in

infer/src/IR/Typ.mli

@@ -265,6 +265,8 @@ val is_pointer_to_cpp_class : t -> bool
 
 val is_pointer : t -> bool
 
+val is_array : t -> bool
+
 val is_reference : t -> bool
 
 val has_block_prefix : string -> bool

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -57,10 +57,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
               |> Dom.Val.add_trace_elem (Trace.SymAssign (loc, location))
             in
             Dom.Mem.add_heap loc v mem
-        (* Temporary fix for ArrayLists in Java, need a better way to handle parameters, see T31498711 *)
-        | Typ.Tptr (typ, _)
-          when Language.curr_language_is Java ->
-            decl_sym_val pname path tenv ~node_hash location ~depth ~may_last_field loc typ mem
+        | Typ.Tptr (typ, _) when Language.curr_language_is Java && not (Typ.is_array typ) ->
+            BoUtils.Exec.decl_sym_java_ptr
+              ~decl_sym_val:(decl_sym_val ~may_last_field:false)
+              pname path tenv ~node_hash location ~depth loc typ ~inst_num ~new_alloc_num mem
         | Typ.Tptr (typ, _) ->
             BoUtils.Exec.decl_sym_arr ~decl_sym_val:(decl_sym_val ~may_last_field) pname path tenv
               ~node_hash location ~depth loc typ ~inst_num ~new_sym_num ~new_alloc_num mem

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -299,10 +299,9 @@ module ArrayList = struct
     let declare_local ~decl_local:_ {pname; node_hash; location} loc ~inst_num ~dimension mem =
       BoUtils.Exec.decl_local_arraylist pname ~node_hash location loc ~inst_num ~dimension mem
     in
-    let declare_symbolic ~decl_sym_val:_ path {pname; node_hash; location} ~depth:_ loc ~inst_num
-        ~new_sym_num ~new_alloc_num mem =
-      BoUtils.Exec.decl_sym_arraylist pname path ~node_hash location loc ~inst_num ~new_sym_num
-        ~new_alloc_num mem
+    let declare_symbolic ~decl_sym_val:_ path {pname; location} ~depth:_ loc ~inst_num:_
+        ~new_sym_num ~new_alloc_num:_ mem =
+      BoUtils.Exec.decl_sym_arraylist pname path location loc ~new_sym_num mem
     in
     {declare_local; declare_symbolic}
 

infer/src/bufferoverrun/bufferOverrunUtils.ml

@@ -105,20 +105,31 @@ module Exec = struct
     decl_sym_val pname path tenv ~node_hash location ~depth deref_loc typ mem
 
 
-  let decl_sym_arraylist
-      : Typ.Procname.t -> Itv.SymbolPath.partial -> node_hash:int -> Location.t -> Loc.t
-        -> inst_num:int -> new_sym_num:Itv.Counter.t -> new_alloc_num:Itv.Counter.t
-        -> Dom.Mem.astate -> Dom.Mem.astate =
-   fun pname path ~node_hash location loc ~inst_num ~new_sym_num ~new_alloc_num mem ->
+  let decl_sym_java_ptr
+      : decl_sym_val:decl_sym_val -> Typ.Procname.t -> Itv.SymbolPath.partial -> Tenv.t
+        -> node_hash:int -> Location.t -> depth:int -> Loc.t -> Typ.t -> inst_num:int
+        -> new_alloc_num:Itv.Counter.t -> Dom.Mem.astate -> Dom.Mem.astate =
+   fun ~decl_sym_val pname path tenv ~node_hash location ~depth loc typ ~inst_num ~new_alloc_num
+       mem ->
     let alloc_num = Itv.Counter.next new_alloc_num in
+    let elem = Trace.SymAssign (loc, location) in
     let allocsite = Sem.get_allocsite pname ~node_hash ~inst_num ~dimension:alloc_num in
     let alloc_loc = Loc.of_allocsite allocsite in
+    let v = Dom.Val.of_pow_loc (PowLoc.singleton alloc_loc) |> Dom.Val.add_trace_elem elem in
+    L.(debug BufferOverrun Verbose) "alloc_num:%d, depth:%d \n" alloc_num depth ;
+    let mem = Dom.Mem.add_heap loc v mem in
+    decl_sym_val pname path tenv ~node_hash location ~depth alloc_loc typ mem
+
+
+  let decl_sym_arraylist
+      : Typ.Procname.t -> Itv.SymbolPath.partial -> Location.t -> Loc.t
+        -> new_sym_num:Itv.Counter.t -> Dom.Mem.astate -> Dom.Mem.astate =
+   fun pname path location loc ~new_sym_num mem ->
     let size =
       Itv.make_sym ~unsigned:true pname (Itv.SymbolPath.length path) new_sym_num |> Dom.Val.of_itv
       |> Dom.Val.add_trace_elem (Trace.SymAssign (loc, location))
     in
-    let alist = Dom.Val.of_pow_loc (PowLoc.singleton alloc_loc) in
-    mem |> Dom.Mem.add_heap loc alist |> Dom.Mem.add_heap alloc_loc size
+    Dom.Mem.add_heap loc size mem
 
 
   let init_array_fields tenv pname ~node_hash typ locs ?dyn_length mem =

infer/src/bufferoverrun/bufferOverrunUtils.mli

@@ -38,10 +38,14 @@ module Exec : sig
     -> inst_num:int -> new_sym_num:Itv.Counter.t -> new_alloc_num:Itv.Counter.t -> Dom.Mem.astate
     -> Dom.Mem.astate
 
+  val decl_sym_java_ptr :
+    decl_sym_val:decl_sym_val -> Typ.Procname.t -> Itv.SymbolPath.partial -> Tenv.t
+    -> node_hash:int -> Location.t -> depth:int -> Loc.t -> Typ.t -> inst_num:int
+    -> new_alloc_num:Itv.Counter.t -> Dom.Mem.astate -> Dom.Mem.astate
+
   val decl_sym_arraylist :
-    Typ.Procname.t -> Itv.SymbolPath.partial -> node_hash:int -> Location.t -> Loc.t
-    -> inst_num:int -> new_sym_num:Itv.Counter.t -> new_alloc_num:Itv.Counter.t -> Dom.Mem.astate
-    -> Dom.Mem.astate
+    Typ.Procname.t -> Itv.SymbolPath.partial -> Location.t -> Loc.t -> new_sym_num:Itv.Counter.t
+    -> Dom.Mem.astate -> Dom.Mem.astate
 
   val init_array_fields :
     Tenv.t -> Typ.Procname.t -> node_hash:int -> Typ.t -> PowLoc.t -> ?dyn_length:Exp.t

infer/tests/codetoanalyze/java/performance/issues.exp

@@ -64,9 +64,9 @@ codetoanalyze/java/performance/Cost_test_deps.java, int Cost_test_deps.two_loops
 codetoanalyze/java/performance/Cost_test_deps.java, void Cost_test_deps.if_bad(int), 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 608]
 codetoanalyze/java/performance/Cost_test_deps.java, void Cost_test_deps.if_bad(int), 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 607]
 codetoanalyze/java/performance/EvilCfg.java, void EvilCfg.foo(int,int,boolean), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
-codetoanalyze/java/performance/FieldAccess.java, void FieldAccess.iterate_upto_field_size(FieldAccess$Test), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
+codetoanalyze/java/performance/FieldAccess.java, void FieldAccess.iterate_upto_field_size(FieldAccess$Test), 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 6 * test.a.ub]
+codetoanalyze/java/performance/FieldAccess.java, void FieldAccess.iterate_upto_field_size(FieldAccess$Test), 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1 + 6 * test.a.ub]
 codetoanalyze/java/performance/JsonArray.java, void JsonArray.addStringEntry(String), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
-codetoanalyze/java/performance/JsonArray.java, void JsonArray.addStringEntry(String), 2, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: int StringBuilder.length(),ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/java/performance/JsonMap.java, void JsonMap.addEntry(String,JsonType), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
 codetoanalyze/java/performance/JsonMap.java, void JsonMap.addEntry(String,JsonType), 6, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Call,Unknown value from: StringBuilder StringBuilder.append(String),Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/java/performance/JsonMap.java, void JsonMap.addEntry(String,Object), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
@@ -75,7 +75,6 @@ codetoanalyze/java/performance/JsonMap.java, void JsonMap.addEntry(String,boolea
 codetoanalyze/java/performance/JsonMap.java, void JsonMap.addEntry(String,double), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
 codetoanalyze/java/performance/JsonMap.java, void JsonMap.addEntry(String,long), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
 codetoanalyze/java/performance/JsonMap.java, void JsonMap.addKeyToMap(String), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
-codetoanalyze/java/performance/JsonMap.java, void JsonMap.addKeyToMap(String), 2, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: int StringBuilder.length(),ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/java/performance/JsonString.java, JsonString.<init>(String), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
 codetoanalyze/java/performance/JsonUtils.java, StringBuilder JsonUtils.serialize(String), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
 codetoanalyze/java/performance/JsonUtils.java, void JsonUtils.escape(StringBuilder,String), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []