diff --git a/infer/src/IR/Typ.ml b/infer/src/IR/Typ.ml index 2161589ef..48877cc23 100644 --- a/infer/src/IR/Typ.ml +++ b/infer/src/IR/Typ.ml @@ -207,6 +207,8 @@ module T = struct let equal_desc = [%compare.equal: desc] + let equal_name = [%compare.equal: name] + let equal_quals = [%compare.equal: type_quals] let equal = [%compare.equal: t] @@ -1027,9 +1029,11 @@ module Procname = struct is_c_function name - let is_java_access_method pname = - match pname with Java java_pname -> Java.is_access_method java_pname | _ -> false + let is_java_lift f = function Java java_pname -> f java_pname | _ -> false + + let is_java_access_method = is_java_lift Java.is_access_method + let is_java_class_initializer = is_java_lift Java.is_class_initializer let is_objc_method procname = match procname with ObjC_Cpp name -> ObjC_Cpp.is_objc_method name | _ -> false diff --git a/infer/src/IR/Typ.mli b/infer/src/IR/Typ.mli index 9322f2b4a..6b0a08766 100644 --- a/infer/src/IR/Typ.mli +++ b/infer/src/IR/Typ.mli @@ -265,6 +265,8 @@ val equal : t -> t -> bool val equal_desc : desc -> desc -> bool +val equal_name : name -> name -> bool + val equal_quals : type_quals -> type_quals -> bool val equal_ignore_quals : t -> t -> bool @@ -534,6 +536,8 @@ being the name of the struct, [None] means the parameter is of some other type. val is_java_access_method : t -> bool + val is_java_class_initializer : t -> bool + val is_objc_method : t -> bool (** Hash tables with proc names as keys. *) diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml index 41cec6718..4887b5b6a 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml +++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml @@ -197,6 +197,29 @@ module TransferFunctions = struct false + let is_java_enum_values ~caller_pname ~callee_pname = + match + (Typ.Procname.get_class_type_name caller_pname, Typ.Procname.get_class_type_name callee_pname) + with + | Some caller_class_name, Some callee_class_name + when Typ.equal_name caller_class_name callee_class_name -> + Typ.Procname.is_java_class_initializer caller_pname + && String.equal (Typ.Procname.get_method callee_pname) "values" + | _, _ -> + false + + + let assign_java_enum_values id callee_pname mem = + match Typ.Procname.get_class_type_name callee_pname with + | Some (JavaClass class_name) -> + let class_var = Loc.of_var (Var.of_pvar (Pvar.mk_global class_name)) in + let fn = Typ.Fieldname.Java.from_string (Mangled.to_string class_name ^ ".$VALUES") in + let v = Dom.Mem.find (Loc.append_field class_var ~fn) mem in + Dom.Mem.add_stack (Loc.of_id id) v mem + | _ -> + assert false + + let exec_instr : Dom.Mem.t -> extras ProcData.t -> CFG.Node.t -> Sil.instr -> Dom.Mem.t = fun mem {summary; tenv; extras= {get_proc_summary_and_formals; oenv= {integer_type_widths}}} node instr -> @@ -284,31 +307,34 @@ module TransferFunctions = struct Sem.Prune.prune integer_type_widths exp mem | Call (((id, _) as ret), Const (Cfun callee_pname), params, location, _) -> ( let mem = Dom.Mem.add_stack_loc (Loc.of_id id) mem in - match Models.Call.dispatch tenv callee_pname params with - | Some {Models.exec} -> - let model_env = - let node_hash = CFG.Node.hash node in - BoUtils.ModelEnv.mk_model_env callee_pname ~node_hash location tenv - integer_type_widths - in - exec model_env ~ret mem - | None -> ( - match get_proc_summary_and_formals callee_pname with - | Some (callee_exit_mem, callee_formals) -> - instantiate_mem tenv integer_type_widths ret callee_formals callee_pname params mem - callee_exit_mem location - | None -> - (* This may happen for procedures with a biabduction model too. *) - L.d_printfln_escaped "/!\\ Unknown call to %a" Typ.Procname.pp callee_pname ; - if is_external callee_pname then ( - L.(debug BufferOverrun Verbose) - "/!\\ External call to unknown %a \n\n" Typ.Procname.pp callee_pname ; - assign_symbolic_pname_value callee_pname ret location mem ) - else if is_non_static callee_pname then ( - L.(debug BufferOverrun Verbose) - "/!\\ Non-static call to unknown %a \n\n" Typ.Procname.pp callee_pname ; - assign_symbolic_pname_value callee_pname ret location mem ) - else Dom.Mem.add_unknown_from id ~callee_pname ~location mem ) ) + if is_java_enum_values ~caller_pname:(Summary.get_proc_name summary) ~callee_pname then + assign_java_enum_values id callee_pname mem + else + match Models.Call.dispatch tenv callee_pname params with + | Some {Models.exec} -> + let model_env = + let node_hash = CFG.Node.hash node in + BoUtils.ModelEnv.mk_model_env callee_pname ~node_hash location tenv + integer_type_widths + in + exec model_env ~ret mem + | None -> ( + match get_proc_summary_and_formals callee_pname with + | Some (callee_exit_mem, callee_formals) -> + instantiate_mem tenv integer_type_widths ret callee_formals callee_pname params mem + callee_exit_mem location + | None -> + (* This may happen for procedures with a biabduction model too. *) + L.d_printfln_escaped "/!\\ Unknown call to %a" Typ.Procname.pp callee_pname ; + if is_external callee_pname then ( + L.(debug BufferOverrun Verbose) + "/!\\ External call to unknown %a \n\n" Typ.Procname.pp callee_pname ; + assign_symbolic_pname_value callee_pname ret location mem ) + else if is_non_static callee_pname then ( + L.(debug BufferOverrun Verbose) + "/!\\ Non-static call to unknown %a \n\n" Typ.Procname.pp callee_pname ; + assign_symbolic_pname_value callee_pname ret location mem ) + else Dom.Mem.add_unknown_from id ~callee_pname ~location mem ) ) | Call ((id, _), fun_exp, _, location, _) -> let mem = Dom.Mem.add_stack_loc (Loc.of_id id) mem in L.d_printfln_escaped "/!\\ Call to non-const function %a" Exp.pp fun_exp ; diff --git a/infer/tests/codetoanalyze/java/performance/IteratorTest.java b/infer/tests/codetoanalyze/java/performance/IteratorTest.java index df7e2da25..13a86a0e3 100644 --- a/infer/tests/codetoanalyze/java/performance/IteratorTest.java +++ b/infer/tests/codetoanalyze/java/performance/IteratorTest.java @@ -17,4 +17,15 @@ public class IteratorTest { public void linearIterable(Iterable elements) { appendTo(elements.iterator()); } + + enum Color { + RED, + GREEN, + BLUE; + + // The cost of class initializer should be constant. + static { + for (Color c : Color.values()) {} + } + } } diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index 86ca25ab1..1a4759d42 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -122,6 +122,7 @@ codetoanalyze/java/performance/Invariant.java, Invariant.formal_not_invariant_FP codetoanalyze/java/performance/Invariant.java, Invariant.list_size_invariant(java.util.List):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ items.length + 3 ⋅ (items.length + 1), O(items.length), degree = 1,{items.length + 1},Loop at line 66,{items.length},Loop at line 66] codetoanalyze/java/performance/Invariant.java, Invariant.local_not_invariant_FP(int):void, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 3 + 12 ⋅ (size + 5) + 7 ⋅ (size + 5) × (5+min(1, size)) + 4 ⋅ (5+min(0, size)), O(size²), degree = 2,{5+min(0, size)},Loop at line 46,{5+min(1, size)},Loop at line 46,{size + 5},Loop at line 46] codetoanalyze/java/performance/Invariant.java, Invariant.x_is_invariant_ok(int):void, 7, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 8 + 6 ⋅ (size + 20), O(size), degree = 1,{size + 20},Loop at line 19] +codetoanalyze/java/performance/IteratorTest.java, IteratorTest$Color.():void, -1, EXPENSIVE_ALLOCATION, no_bucket, ERROR, [with estimated cost 4, O(1), degree = 0] codetoanalyze/java/performance/IteratorTest.java, IteratorTest.appendTo(java.util.Iterator):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 1 + 10 ⋅ parts.length + 3 ⋅ (parts.length + 1), O(parts.length), degree = 1,{parts.length + 1},Loop at line 12,{parts.length},Loop at line 12] codetoanalyze/java/performance/IteratorTest.java, IteratorTest.linearIterable(java.lang.Iterable):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 9 + 10 ⋅ elements.length + 3 ⋅ (elements.length + 1), O(elements.length), degree = 1,{elements.length + 1},call to void IteratorTest.appendTo(Iterator),Loop at line 12,{elements.length},call to void IteratorTest.appendTo(Iterator),Loop at line 12] codetoanalyze/java/performance/JsonArray.java, libraries.marauder.analytics.utils.json.JsonArray.addStringEntry(java.lang.String):void, 4, EXPENSIVE_ALLOCATION, no_bucket, ERROR, [with estimated cost String.toCharArray().length.ub, O(String.toCharArray().length.ub), degree = 1,{String.toCharArray().length.ub},call to void JsonUtils.serialize(StringBuilder,String),call to void JsonUtils.escape(StringBuilder,String),Loop at line 13]