diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml index a22f7c34e..bb68e8711 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml +++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml @@ -35,7 +35,7 @@ module Init = struct let node_hash = CFG.Node.hash start_node in let location = CFG.Node.loc start_node in let integer_type_widths = oenv.OndemandEnv.integer_type_widths in - BoUtils.ModelEnv.mk_model_env pname ~node_hash location tenv integer_type_widths + BoUtils.ModelEnv.mk_model_env pname ~node_hash location tenv integer_type_widths get_summary in fun (mem, inst_num) {ProcAttributes.name; typ} -> let loc = Loc.of_pvar (Pvar.mk name pname) in @@ -305,6 +305,7 @@ module TransferFunctions = struct let pname = Procdesc.get_proc_name proc_desc in let node_hash = CFG.Node.hash node in BoUtils.ModelEnv.mk_model_env pname ~node_hash location tenv integer_type_widths + get_summary in match modeled_load_of_empty_collection_opt exp model_env (id, typ) mem with | Some mem' -> @@ -326,6 +327,7 @@ module TransferFunctions = struct let node_hash = CFG.Node.hash node in let model_env = BoUtils.ModelEnv.mk_model_env pname ~node_hash location tenv integer_type_widths + get_summary in let tgt_locs = Sem.eval_locs tgt_exp mem in let tgt_deref = @@ -343,6 +345,7 @@ module TransferFunctions = struct let pname = Procdesc.get_proc_name proc_desc in let node_hash = CFG.Node.hash node in BoUtils.ModelEnv.mk_model_env pname ~node_hash location tenv integer_type_widths + get_summary in let do_alloc = not (Sem.is_stack_exp exp1 mem) in BoUtils.Exec.decl_string model_env ~do_alloc locs s mem @@ -385,7 +388,7 @@ module TransferFunctions = struct 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 + integer_type_widths get_summary in exec model_env ~ret mem | None -> ( @@ -412,6 +415,7 @@ module TransferFunctions = struct let pname = Procdesc.get_proc_name proc_desc in let node_hash = CFG.Node.hash node in BoUtils.ModelEnv.mk_model_env pname ~node_hash location tenv integer_type_widths + get_summary in let mem, _ = BoUtils.Exec.decl_local model_env (mem, 1) (Loc.of_pvar pvar, typ) in mem @@ -442,9 +446,10 @@ let compute_invariant_map : let cfg = CFG.from_pdesc proc_desc in let analysis_data = let proc_name = Procdesc.get_proc_name proc_desc in - let get_summary proc_name = analyze_dependency proc_name |> Option.map ~f:snd in + let open IOption.Let_syntax in + let get_summary proc_name = analyze_dependency proc_name >>| snd in let get_formals callee_pname = - AnalysisCallbacks.get_proc_desc callee_pname |> Option.map ~f:Procdesc.get_pvar_formals + AnalysisCallbacks.get_proc_desc callee_pname >>| Procdesc.get_pvar_formals in let integer_type_widths = Exe_env.get_integer_type_widths exe_env proc_name in let oenv = OndemandEnv.mk proc_desc tenv integer_type_widths in diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 13448af76..8ade46342 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -9,6 +9,7 @@ open! IStd open! AbstractDomain.Types +module BoSummary = BufferOverrunAnalysisSummary module BoUtils = BufferOverrunUtils module CFG = BufferOverrunAnalysis.CFG module Dom = BufferOverrunDomain @@ -256,6 +257,7 @@ type get_checks_summary = Procname.t -> checks_summary option let check_instr : get_checks_summary + -> BoSummary.get_summary -> BoUtils.get_formals -> Procname.t -> Tenv.t @@ -265,7 +267,8 @@ let check_instr : -> Dom.Mem.t -> PO.ConditionSet.checked_t -> PO.ConditionSet.checked_t = - fun get_checks_summary get_formals pname tenv integer_type_widths node instr mem cond_set -> + fun get_checks_summary get_summary get_formals pname tenv integer_type_widths node instr mem + cond_set -> match instr with | Sil.Load {e= exp; loc= location} -> cond_set @@ -291,6 +294,7 @@ let check_instr : let model_env = let node_hash = CFG.Node.hash node in BoUtils.ModelEnv.mk_model_env pname ~node_hash location tenv integer_type_widths + get_summary in check model_env mem cond_set | None -> ( @@ -322,6 +326,7 @@ let print_debug_info : Sil.instr -> Dom.Mem.t -> PO.ConditionSet.checked_t -> un let check_instrs : get_checks_summary + -> BoSummary.get_summary -> BoUtils.get_formals -> Procname.t -> Tenv.t @@ -332,7 +337,8 @@ let check_instrs : -> Dom.Mem.t AbstractInterpreter.State.t -> Checks.t -> Checks.t = - fun get_checks_summary get_formals pname tenv integer_type_widths cfg node instrs state checks -> + fun get_checks_summary get_summary get_formals pname tenv integer_type_widths cfg node instrs state + checks -> match state with | _ when Instrs.is_empty instrs -> checks @@ -349,8 +355,8 @@ let check_instrs : checks in let cond_set = - check_instr get_checks_summary get_formals pname tenv integer_type_widths node instr pre - checks.cond_set + check_instr get_checks_summary get_summary get_formals pname tenv integer_type_widths node + instr pre checks.cond_set in print_debug_info instr pre cond_set ; {checks with cond_set} @@ -358,6 +364,7 @@ let check_instrs : let check_node : get_checks_summary + -> BoSummary.get_summary -> BoUtils.get_formals -> Procname.t -> Tenv.t @@ -367,12 +374,13 @@ let check_node : -> Checks.t -> CFG.Node.t -> Checks.t = - fun get_checks_summary get_formals pname tenv integer_type_widths cfg inv_map checks node -> + fun get_checks_summary get_summary get_formals pname tenv integer_type_widths cfg inv_map checks + node -> match BufferOverrunAnalysis.extract_state (CFG.Node.id node) inv_map with | Some state -> let instrs = CFG.instrs node in - check_instrs get_checks_summary get_formals pname tenv integer_type_widths cfg node instrs - state checks + check_instrs get_checks_summary get_summary get_formals pname tenv integer_type_widths cfg + node instrs state checks | _ -> checks @@ -381,6 +389,7 @@ type checks = Checks.t let compute_checks : get_checks_summary + -> BoSummary.get_summary -> BoUtils.get_formals -> Procname.t -> Tenv.t @@ -388,9 +397,11 @@ let compute_checks : -> CFG.t -> BufferOverrunAnalysis.invariant_map -> checks = - fun get_checks_summary get_formals pname tenv integer_type_widths cfg inv_map -> + fun get_checks_summary get_summary get_formals pname tenv integer_type_widths cfg inv_map -> CFG.fold_nodes cfg - ~f:(check_node get_checks_summary get_formals pname tenv integer_type_widths cfg inv_map) + ~f: + (check_node get_checks_summary get_summary get_formals pname tenv integer_type_widths cfg + inv_map) ~init:Checks.empty @@ -433,14 +444,24 @@ let checker ({InterproceduralAnalysis.proc_desc; tenv; exe_env; analyze_dependen AnalysisCallbacks.html_debug_new_node_session ~pp_name underlying_exit_node ~f:(fun () -> let cfg = CFG.from_pdesc proc_desc in let checks = + let open IOption.Let_syntax in + let get_summary_common callee_pname = + let+ _, summaries = analyze_dependency callee_pname in + summaries + in let get_checks_summary callee_pname = - analyze_dependency callee_pname - |> Option.bind ~f:(fun (_, (checker_summary, _analysis_summary)) -> checker_summary) + let* checker_summary, _analysis_summary = get_summary_common callee_pname in + checker_summary + in + let get_summary callee_pname = + let* _checker_summary, analysis_summary = get_summary_common callee_pname in + analysis_summary in let get_formals callee_pname = - AnalysisCallbacks.get_proc_desc callee_pname |> Option.map ~f:Procdesc.get_pvar_formals + AnalysisCallbacks.get_proc_desc callee_pname >>| Procdesc.get_pvar_formals in - compute_checks get_checks_summary get_formals proc_name tenv integer_type_widths cfg inv_map + compute_checks get_checks_summary get_summary get_formals proc_name tenv integer_type_widths + cfg inv_map in report_errors analysis_data checks ; Some (get_checks_summary checks) ) diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 7b80e5029..5d5772a64 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -1056,28 +1056,31 @@ module Collection = struct end module JavaClass = struct + let decl_array {pname; node_hash; location} ~ret:(ret_id, _) length mem = + let loc = + Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 ~path:None + ~represents_multiple_values:true + |> Loc.of_allocsite + in + let arr_v = + let allocsite = + Allocsite.make pname ~node_hash ~inst_num:1 ~dimension:1 ~path:None + ~represents_multiple_values:true + in + let traces = Trace.(Set.singleton location ArrayDeclaration) in + Dom.Val.of_java_array_alloc allocsite ~length ~traces + in + Dom.Mem.add_heap loc arr_v mem |> model_by_value (Dom.Val.of_loc loc) ret_id + + let get_fields class_name_exp = - let exec {pname; node_hash; location; tenv} ~ret:(ret_id, _) mem = + let exec ({tenv} as model_env) ~ret mem = match class_name_exp with | Exp.Const (Const.Cclass name) -> ( let typ_name = Typ.Name.Java.from_string (Ident.name_to_string name) in match Tenv.lookup tenv typ_name with | Some {fields} -> - let loc = - Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 ~path:None - ~represents_multiple_values:true - |> Loc.of_allocsite - in - let arr_v = - let allocsite = - Allocsite.make pname ~node_hash ~inst_num:1 ~dimension:1 ~path:None - ~represents_multiple_values:true - in - let length = List.length fields |> Itv.of_int in - let traces = Trace.(Set.singleton location ArrayDeclaration) in - Dom.Val.of_java_array_alloc allocsite ~length ~traces - in - Dom.Mem.add_heap loc arr_v mem |> model_by_value (Dom.Val.of_loc loc) ret_id + decl_array model_env ~ret (List.length fields |> Itv.of_int) mem | None -> Logging.d_printfln_escaped "Could not find class from tenv" ; mem ) @@ -1086,6 +1089,36 @@ module JavaClass = struct mem in {exec; check= no_check} + + + let get_enum_constants class_name_exp = + let exec ({get_summary} as model_env) ~ret mem = + match class_name_exp with + | Exp.Const (Const.Cclass name) -> ( + let enum_values_pname = + let class_name_str = Ident.name_to_string name in + Procname.make_java + ~class_name:(Typ.Name.Java.from_string class_name_str) + ~return_type:(Some (JavaSplitName.make (class_name_str ^ "[]"))) + ~method_name:"values" ~parameters:[] ~kind:Procname.Java.Static () + in + match get_summary enum_values_pname with + | Some enum_values_mem -> + let length = + let ret_loc = Loc.of_pvar (Pvar.get_ret_pvar enum_values_pname) in + let ret_v = Dom.Mem.find ret_loc enum_values_mem in + Dom.Mem.find_set (Dom.Val.get_all_locs ret_v) enum_values_mem + |> Dom.Val.array_sizeof + in + decl_array model_env ~ret length mem + | None -> + Logging.d_printfln_escaped "Summary of Enum.values not found" ; + mem ) + | _ -> + Logging.d_printfln_escaped "Parameter is not a class name constant" ; + mem + in + {exec; check= no_check} end module JavaString = struct @@ -1563,6 +1596,8 @@ module Call = struct &:: "substring" <>$ any_arg $+ capt_exp $+ capt_exp $--> JavaString.substring ; +PatternMatch.implements_lang "Class" &:: "getCanonicalName" &::.*--> JavaString.inferbo_constant_string + ; +PatternMatch.implements_lang "Class" + &:: "getEnumConstants" <>$ capt_exp $--> JavaClass.get_enum_constants ; +PatternMatch.implements_lang "Class" &:: "getFields" <>$ capt_exp $--> JavaClass.get_fields ; +PatternMatch.implements_lang "Enum" &:: "name" &::.*--> JavaString.inferbo_constant_string ; +PatternMatch.implements_lang "Integer" diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index ad59e4346..11ec65d6b 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -8,6 +8,7 @@ open! IStd open AbsLoc open! AbstractDomain.Types +module BoSummary = BufferOverrunAnalysisSummary module L = Logging module Dom = BufferOverrunDomain module PO = BufferOverrunProofObligations @@ -22,10 +23,11 @@ module ModelEnv = struct ; node_hash: int ; location: Location.t ; tenv: Tenv.t - ; integer_type_widths: Typ.IntegerWidths.t } + ; integer_type_widths: Typ.IntegerWidths.t + ; get_summary: BoSummary.get_summary } - let mk_model_env pname ~node_hash location tenv integer_type_widths = - {pname; node_hash; location; tenv; integer_type_widths} + let mk_model_env pname ~node_hash location tenv integer_type_widths get_summary = + {pname; node_hash; location; tenv; integer_type_widths; get_summary} end module Exec = struct diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.mli b/infer/src/bufferoverrun/bufferOverrunUtils.mli index b90c36c88..db98ad9e8 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.mli +++ b/infer/src/bufferoverrun/bufferOverrunUtils.mli @@ -16,10 +16,17 @@ module ModelEnv : sig ; node_hash: int ; location: Location.t ; tenv: Tenv.t - ; integer_type_widths: Typ.IntegerWidths.t } + ; integer_type_widths: Typ.IntegerWidths.t + ; get_summary: BufferOverrunAnalysisSummary.get_summary } val mk_model_env : - Procname.t -> node_hash:int -> Location.t -> Tenv.t -> Typ.IntegerWidths.t -> model_env + Procname.t + -> node_hash:int + -> Location.t + -> Tenv.t + -> Typ.IntegerWidths.t + -> BufferOverrunAnalysisSummary.get_summary + -> model_env end module Exec : sig diff --git a/infer/src/cost/cost.ml b/infer/src/cost/cost.ml index 8158d248f..46b57c2e7 100644 --- a/infer/src/cost/cost.ml +++ b/infer/src/cost/cost.ml @@ -18,6 +18,7 @@ module Node = ProcCfg.DefaultNode type extras_WorstCaseCost = { inferbo_invariant_map: BufferOverrunAnalysis.invariant_map ; integer_type_widths: Typ.IntegerWidths.t + ; inferbo_get_summary: BufferOverrunAnalysisSummary.get_summary ; get_node_nb_exec: Node.id -> BasicCost.t ; get_summary: Procname.t -> CostDomain.summary option ; get_formals: Procname.t -> (Pvar.t * Typ.t) list option } @@ -53,7 +54,13 @@ module InstrBasicCost = struct match instr with | Sil.Call (ret, Exp.Const (Const.Cfun callee_pname), params, _, _) when Config.inclusive_cost -> - let {inferbo_invariant_map; integer_type_widths; get_summary; get_formals} = extras in + let { inferbo_invariant_map + ; integer_type_widths + ; inferbo_get_summary + ; get_summary + ; get_formals } = + extras + in let operation_cost = match BufferOverrunAnalysis.extract_pre (InstrCFG.Node.id instr_node) inferbo_invariant_map @@ -71,7 +78,7 @@ module InstrBasicCost = struct let node_hash = InstrCFG.Node.hash instr_node in let model_env = BufferOverrunUtils.ModelEnv.mk_model_env callee_pname ~node_hash loc tenv - integer_type_widths + integer_type_widths inferbo_get_summary in CostDomain.of_operation_cost (model model_env ~ret inferbo_mem) | None -> ( @@ -326,9 +333,14 @@ let compute_get_node_nb_exec node_cfg bound_map : get_node_nb_exec = let compute_worst_case_cost tenv integer_type_widths get_summary get_formals instr_cfg_wto - inferbo_invariant_map get_node_nb_exec = + inferbo_invariant_map inferbo_get_summary get_node_nb_exec = let extras = - {inferbo_invariant_map; integer_type_widths; get_node_nb_exec; get_summary; get_formals} + { inferbo_invariant_map + ; integer_type_widths + ; inferbo_get_summary + ; get_node_nb_exec + ; get_summary + ; get_formals } in WorstCaseCost.compute tenv extras instr_cfg_wto @@ -367,20 +379,26 @@ let checker ({InterproceduralAnalysis.proc_desc; exe_env; analyze_dependency} as let is_on_ui_thread = ConcurrencyModels.runs_on_ui_thread tenv proc_name in let get_node_nb_exec = compute_get_node_nb_exec node_cfg bound_map in let astate = + let open IOption.Let_syntax in + let get_summary_common callee_pname = + let+ _, summaries = analyze_dependency callee_pname in + summaries + in let get_summary callee_pname = - match analyze_dependency callee_pname with - | Some (_, (payload, _, _)) -> - payload - | None -> - None + let* cost_summary, _inferbo_summary, _ = get_summary_common callee_pname in + cost_summary + in + let inferbo_get_summary callee_pname = + let* _cost_summary, inferbo_summary, _ = get_summary_common callee_pname in + inferbo_summary in let get_formals callee_pname = - AnalysisCallbacks.get_proc_desc callee_pname |> Option.map ~f:Procdesc.get_pvar_formals + AnalysisCallbacks.get_proc_desc callee_pname >>| Procdesc.get_pvar_formals in let instr_cfg = InstrCFG.from_pdesc proc_desc in let instr_cfg_wto = InstrCFG.wto instr_cfg in compute_worst_case_cost tenv integer_type_widths get_summary get_formals instr_cfg_wto - inferbo_invariant_map get_node_nb_exec + inferbo_invariant_map inferbo_get_summary get_node_nb_exec in let () = let exit_cost_record = astate.WorstCaseCost.costs in diff --git a/infer/src/cost/hoisting.ml b/infer/src/cost/hoisting.ml index ee0c2ac1e..e1babed92 100644 --- a/infer/src/cost/hoisting.ml +++ b/infer/src/cost/hoisting.ml @@ -100,7 +100,7 @@ let do_report extract_cost_if_expensive proc_desc err_log (Call.{pname; loc} as let get_cost_if_expensive tenv integer_type_widths get_callee_cost_summary_and_formals - inferbo_invariant_map Call.{pname; node; ret; params} = + inferbo_invariant_map inferbo_get_summary Call.{pname; node; ret; params} = let last_node = InstrCFG.last_of_underlying_node node in let inferbo_mem = let instr_node_id = InstrCFG.Node.id last_node in @@ -126,7 +126,7 @@ let get_cost_if_expensive tenv integer_type_widths get_callee_cost_summary_and_f let model_env = let node_hash = InstrCFG.Node.hash last_node in BufferOverrunUtils.ModelEnv.mk_model_env pname ~node_hash loc tenv - integer_type_widths + integer_type_widths inferbo_get_summary in model model_env ~ret inferbo_mem ) in @@ -169,16 +169,22 @@ let checker BufferOverrunAnalysis.cached_compute_invariant_map (InterproceduralAnalysis.bind_payload ~f:fst3 analysis_data) in + let open IOption.Let_syntax in let get_callee_cost_summary_and_formals callee_pname = - analyze_dependency callee_pname - |> Option.bind ~f:(function - | callee_pdesc, (_inferbo, _purity, Some callee_costs_summary) -> - Some (callee_costs_summary, Procdesc.get_pvar_formals callee_pdesc) - | _, (_, _, None) -> - None ) + let* callee_pdesc, (_inferbo, _purity, callee_costs_summary) = + analyze_dependency callee_pname + in + let+ callee_costs_summary = callee_costs_summary in + (callee_costs_summary, Procdesc.get_pvar_formals callee_pdesc) + in + let inferbo_get_summary callee_pname = + let* _callee_pdesc, (inferbo, _purity, _callee_costs_summary) = + analyze_dependency callee_pname + in + inferbo in get_cost_if_expensive tenv integer_type_widths get_callee_cost_summary_and_formals - inferbo_invariant_map + inferbo_invariant_map inferbo_get_summary else fun _ -> None in let get_callee_purity callee_pname = diff --git a/infer/tests/codetoanalyze/java/performance/EnumTest.java b/infer/tests/codetoanalyze/java/performance/EnumTest.java index 2b6be9aa6..4e43642c5 100644 --- a/infer/tests/codetoanalyze/java/performance/EnumTest.java +++ b/infer/tests/codetoanalyze/java/performance/EnumTest.java @@ -14,4 +14,8 @@ class EnumTest { void enum_name_constant(MyEnum e) { for (int i = 0; i < e.name().length(); i++) {} } + + void iterate_enum_constants() { + for (Object obj : MyEnum.class.getEnumConstants()) {} + } } diff --git a/infer/tests/codetoanalyze/java/performance/cost-issues.exp b/infer/tests/codetoanalyze/java/performance/cost-issues.exp index b714aa8bc..644630a9b 100644 --- a/infer/tests/codetoanalyze/java/performance/cost-issues.exp +++ b/infer/tests/codetoanalyze/java/performance/cost-issues.exp @@ -162,6 +162,7 @@ codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performan codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.two_loops():int, 549, OnUIThread:false codetoanalyze/java/performance/EnumTest.java, EnumTest.(), 3, OnUIThread:false codetoanalyze/java/performance/EnumTest.java, EnumTest.enum_name_constant(MyEnum):void, 198, OnUIThread:false +codetoanalyze/java/performance/EnumTest.java, EnumTest.iterate_enum_constants():void, 31, OnUIThread:false codetoanalyze/java/performance/EnumTest.java, MyEnum.():void, 29, OnUIThread:false codetoanalyze/java/performance/EnumTest.java, MyEnum.(java.lang.String,int), 5, OnUIThread:false codetoanalyze/java/performance/EnumTest.java, MyEnum.valueOf(java.lang.String):MyEnum, 7, OnUIThread:false