diff --git a/infer/src/absint/AbstractDomain.mli b/infer/src/absint/AbstractDomain.mli index 24fbaf2f1..7e19e653c 100644 --- a/infer/src/absint/AbstractDomain.mli +++ b/infer/src/absint/AbstractDomain.mli @@ -74,10 +74,6 @@ module BottomLifted (Domain : S) : sig val map : f:(Domain.t -> Domain.t) -> t -> t end -module BottomLiftedUtils : sig - val pp : pp:(Format.formatter -> 'a -> unit) -> Format.formatter -> 'a bottom_lifted -> unit -end - (** Create a domain with Top element from a pre-domain *) module TopLifted (Domain : S) : WithTop with type t = Domain.t top_lifted diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml index 61f7ed3ab..163985b4d 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml +++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml @@ -70,12 +70,17 @@ module TransferFunctions = struct if Dom.LatestPrune.is_top latest_prune' then mem else Dom.Mem.set_latest_prune latest_prune' mem | Error `SubstBottom -> - Dom.Mem.bottom + Dom.Mem.bot | Error `SubstFail -> mem - let instantiate_mem_reachable (ret_id, _) callee_formals callee_pname ~callee_exit_mem + let symbolic_pname_value pname typ location mem = + let path = CallSite.make pname location |> Symb.SymbolPath.of_callsite ~ret_typ:typ in + Dom.Mem.find (Loc.of_allocsite (Allocsite.make_symbol path)) mem + + + let instantiate_mem_reachable (ret_id, ret_typ) callee_formals callee_pname ~callee_exit_mem ({Dom.eval_locpath} as eval_sym_trace) mem location = let formal_locs = List.fold callee_formals ~init:PowLoc.bot ~f:(fun acc (formal, _) -> @@ -115,7 +120,9 @@ module TransferFunctions = struct | Some callee_pdesc when Procdesc.has_added_return_param callee_pdesc -> Dom.Val.of_loc (Loc.of_pvar (Pvar.get_ret_param_pvar callee_pname)) | _ -> - Dom.Mem.find (Loc.of_pvar (Pvar.get_ret_pvar callee_pname)) callee_exit_mem + if Language.curr_language_is Java && Dom.Mem.is_exc_raised callee_exit_mem then + symbolic_pname_value callee_pname ret_typ location mem + else Dom.Mem.find (Loc.of_pvar (Pvar.get_ret_pvar callee_pname)) callee_exit_mem in Dom.Mem.add_stack ret_var (Dom.Val.subst ret_val eval_sym_trace location) mem |> instantiate_ret_alias @@ -201,6 +208,8 @@ module TransferFunctions = struct | Load {id; e= exp; typ} -> let represents_multiple_values = is_array_access_exp exp in BoUtils.Exec.load_locs ~represents_multiple_values id typ (Sem.eval_locs exp mem) mem + | Store {e2= Exn _} when Language.curr_language_is Java -> + Dom.Mem.exc_raised | Store {e1= tgt_exp; e2= Const (Const.Cstr _) as src; loc= location} when Language.curr_language_is Java -> let pname = Summary.get_proc_name summary in @@ -280,10 +289,7 @@ module TransferFunctions = struct if is_external callee_pname then ( L.(debug BufferOverrun Verbose) "/!\\ External call to unknown %a \n\n" Typ.Procname.pp callee_pname ; - let callsite = CallSite.make callee_pname location in - let path = Symb.SymbolPath.of_callsite ~ret_typ callsite in - let loc = Loc.of_allocsite (Allocsite.make_symbol path) in - let v = Dom.Mem.find loc mem in + let v = symbolic_pname_value callee_pname ret_typ location mem in Dom.Mem.add_stack (Loc.of_id id) v mem ) else Dom.Mem.add_unknown_from id ~callee_pname ~location mem ) ) | Call ((id, _), fun_exp, _, location, _) -> diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 440f520d7..c9c1ff180 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -345,7 +345,7 @@ let check_instrs : match state with | _ when Instrs.is_empty instrs -> checks - | {AbstractInterpreter.State.pre= Bottom} -> + | {AbstractInterpreter.State.pre= Bottom | ExcRaised} -> checks | {AbstractInterpreter.State.pre= NonBottom _ as pre; post} -> if Instrs.nth_exists instrs 1 then @@ -353,7 +353,7 @@ let check_instrs : let instr = Instrs.nth_exn instrs 0 in let checks = match post with - | Bottom -> + | Bottom | ExcRaised -> add_unreachable_code cfg node instr Instrs.empty checks | NonBottom _ -> checks diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 5adadc5ba..9bc2a0037 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -1939,18 +1939,71 @@ module MemReach = struct end module Mem = struct - include AbstractDomain.BottomLifted (MemReach) - - type 'has_oenv t0 = 'has_oenv MemReach.t0 AbstractDomain.Types.bottom_lifted + type 'has_oenv t0 = Bottom | ExcRaised | NonBottom of 'has_oenv MemReach.t0 type no_oenv_t = GOption.none t0 + type t = GOption.some t0 + let bot : t = Bottom + let exc_raised : t = ExcRaised + + let is_exc_raised = function ExcRaised -> true | _ -> false + + let ( <= ) ~lhs ~rhs = + if phys_equal lhs rhs then true + else + match (lhs, rhs) with + | Bottom, _ -> + true + | _, Bottom -> + false + | ExcRaised, _ -> + true + | _, ExcRaised -> + false + | NonBottom lhs, NonBottom rhs -> + MemReach.( <= ) ~lhs ~rhs + + + let join x y = + if phys_equal x y then x + else + match (x, y) with + | Bottom, m | m, Bottom -> + m + | ExcRaised, m | m, ExcRaised -> + m + | NonBottom m1, NonBottom m2 -> + PhysEqual.optim2 ~res:(NonBottom (MemReach.join m1 m2)) x y + + + let widen ~prev:prev0 ~next:next0 ~num_iters = + if phys_equal prev0 next0 then prev0 + else + match (prev0, next0) with + | Bottom, m | m, Bottom -> + m + | ExcRaised, m | m, ExcRaised -> + m + | NonBottom prev, NonBottom next -> + PhysEqual.optim2 ~res:(NonBottom (MemReach.widen ~prev ~next ~num_iters)) prev0 next0 + + + let map ~f x = + match x with + | Bottom | ExcRaised -> + x + | NonBottom m -> + let m' = f m in + if phys_equal m' m then x else NonBottom m' + + let init : OndemandEnv.t -> t = fun oenv -> NonBottom (MemReach.init oenv) let f_lift_default : default:'a -> ('h MemReach.t0 -> 'a) -> 'h t0 -> 'a = - fun ~default f m -> match m with Bottom -> default | NonBottom m' -> f m' + fun ~default f m -> match m with Bottom | ExcRaised -> default | NonBottom m' -> f m' let is_stack_loc : Loc.t -> _ t0 -> bool = @@ -2065,8 +2118,8 @@ module Mem = struct let apply_latest_prune : Exp.t -> t -> t * PrunePairs.t = fun e -> function - | Bottom -> - (Bottom, PrunePairs.empty) + | (Bottom | ExcRaised) as x -> + (x, PrunePairs.empty) | NonBottom m -> let m, prune_pairs = MemReach.apply_latest_prune e m in (NonBottom m, prune_pairs) @@ -2128,13 +2181,18 @@ module Mem = struct let instantiate_relation : Relation.SubstMap.t -> caller:t -> callee:no_oenv_t -> t = fun subst_map ~caller ~callee -> match callee with - | Bottom -> + | Bottom | ExcRaised -> caller | NonBottom callee -> map ~f:(fun caller -> MemReach.instantiate_relation subst_map ~caller ~callee) caller - let unset_oenv = function Bottom -> Bottom | NonBottom m -> NonBottom (MemReach.unset_oenv m) + let unset_oenv = function + | (Bottom | ExcRaised) as x -> + x + | NonBottom m -> + NonBottom (MemReach.unset_oenv m) + let set_first_idx_of_null loc idx = map ~f:(MemReach.set_first_idx_of_null loc idx) @@ -2147,5 +2205,12 @@ module Mem = struct PowLoc.fold get_c_strlen' locs Val.bot - let pp f m = AbstractDomain.BottomLiftedUtils.pp ~pp:MemReach.pp f m + let pp f m = + match m with + | Bottom -> + F.pp_print_string f SpecialChars.up_tack + | ExcRaised -> + F.pp_print_string f (SpecialChars.up_tack ^ " by exception") + | NonBottom m -> + MemReach.pp f m end diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 0bc0f3822..a4850d591 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -364,7 +364,7 @@ let by_risky_value_from lib_fun = let bottom = - let exec _model_env ~ret:_ _mem = Bottom in + let exec _model_env ~ret:_ _mem = Dom.Mem.bot in {exec; check= no_check} diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index a778aa6e8..d0f192d56 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -81,6 +81,8 @@ module BoundMap = struct [COST ANALYSIS INTERNAL WARNING:] No 'env' found. This location is \ unreachable returning cost 0 \n" ; BasicCost.zero + | ExcRaised -> + BasicCost.one | NonBottom mem -> BufferOverrunDomain.MemReach.range ~filter_loc:(filter_loc control_map) ~node_id mem diff --git a/infer/tests/codetoanalyze/java/performance/UnknownCallsTest.java b/infer/tests/codetoanalyze/java/performance/UnknownCallsTest.java index 523d57ba4..a8c161fb3 100644 --- a/infer/tests/codetoanalyze/java/performance/UnknownCallsTest.java +++ b/infer/tests/codetoanalyze/java/performance/UnknownCallsTest.java @@ -63,4 +63,26 @@ class UnknownCallsTest { list.get(i).hashCode(); } } + + int throw_exception() { + throw new IllegalStateException(); + } + + void call_throw_exception_linear() { + for (int i = 0; i < throw_exception(); i++) {} + } + + boolean unknown_bool; + + int may_throw_exception() { + if (unknown_bool) { + throw new IllegalStateException(); + } else { + return 10; + } + } + + void call_may_throw_exception_constant() { + for (int i = 0; i < may_throw_exception(); i++) {} + } } diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index c260b85a0..d857e480e 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -183,8 +183,14 @@ codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switc codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.test_switch():int, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 798, O(1), degree = 0] codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.vanilla_switch(int):void, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_loop_over_charArray(java.lang.StringBuilder,java.lang.String):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 14 + 12 ⋅ String.toCharArray().length.ub, O(String.toCharArray().length.ub), degree = 1,{String.toCharArray().length.ub},call to void UnknownCallsTest.loop_over_charArray(StringBuilder,String),Loop at line 52] +codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_may_throw_exception_constant():void, 1, EXPENSIVE_ALLOCATION, no_bucket, ERROR, [with estimated cost 11, O(1), degree = 0] +codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_may_throw_exception_constant():void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 217, O(1), degree = 0] +codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_throw_exception_linear():void, 1, EXPENSIVE_ALLOCATION, no_bucket, ERROR, [with estimated cost (1+max(0, UnknownCallsTest.throw_exception().ub)), O(UnknownCallsTest.throw_exception().ub), degree = 1,{1+max(0, UnknownCallsTest.throw_exception().ub)},Loop at line 72] +codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_throw_exception_linear():void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ UnknownCallsTest.throw_exception().ub + 8 ⋅ (1+max(0, UnknownCallsTest.throw_exception().ub)), O(UnknownCallsTest.throw_exception().ub), degree = 1,{1+max(0, UnknownCallsTest.throw_exception().ub)},Loop at line 72,{UnknownCallsTest.throw_exception().ub},Loop at line 72] codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.jsonArray_linear(org.json.JSONArray):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 5 + 5 ⋅ jsonArray.length, O(jsonArray.length), degree = 1,{jsonArray.length},Loop at line 18] codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.loop_over_charArray(java.lang.StringBuilder,java.lang.String):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 8 + 12 ⋅ String.toCharArray().length.ub, O(String.toCharArray().length.ub), degree = 1,{String.toCharArray().length.ub},Loop at line 52] +codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.may_throw_exception():int, 2, UNREACHABLE_CODE, no_bucket, ERROR, [Here] codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_max_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 9, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 21 + 5 ⋅ (Math.min(...).ub + 1), O(Math.min(...).ub), degree = 1,{Math.min(...).ub + 1},Loop at line 47] codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_sum_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 6, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 15 + 6 ⋅ 2⋅Math.min(...).ub, O(2⋅Math.min(...).ub), degree = 1,{2⋅Math.min(...).ub},Loop at line 33] +codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.throw_exception():int, 1, UNREACHABLE_CODE, no_bucket, ERROR, [Here] codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.unmodeled_impure_linear(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 13 ⋅ list.length + 3 ⋅ (list.length + 1), O(list.length), degree = 1,{list.length + 1},Loop at line 62,{list.length},Loop at line 62]