From 2d889791e2acf516fa231eda157565ebd9e47d7e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Wed, 25 Jul 2018 09:04:54 -0700 Subject: [PATCH] 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 | 2 ++ infer/src/IR/Typ.mli | 2 ++ .../src/bufferoverrun/bufferOverrunChecker.ml | 8 +++--- .../src/bufferoverrun/bufferOverrunModels.ml | 7 +++--- infer/src/bufferoverrun/bufferOverrunUtils.ml | 25 +++++++++++++------ .../src/bufferoverrun/bufferOverrunUtils.mli | 10 +++++--- .../codetoanalyze/java/performance/issues.exp | 5 ++-- 7 files changed, 38 insertions(+), 21 deletions(-) diff --git a/infer/src/IR/Typ.ml b/infer/src/IR/Typ.ml index 3284e3c03..a022e526c 100644 --- a/infer/src/IR/Typ.ml +++ b/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 diff --git a/infer/src/IR/Typ.mli b/infer/src/IR/Typ.mli index aa1d8d274..f3a65fb08 100644 --- a/infer/src/IR/Typ.mli +++ b/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 diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 8daced715..79da3f0fd 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/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 diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index e2a610a4f..1fe3ffdc8 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/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} diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index 2718bb2a4..f4425c53e 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/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 = diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.mli b/infer/src/bufferoverrun/bufferOverrunUtils.mli index 2a593e9ed..97b7f2a6e 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.mli +++ b/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 diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index aebb841a3..28983932b 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/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.(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, []