From 5303177a2d127ae6ca8038f8c69859e9f3362ef7 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Wed, 2 Oct 2019 15:26:08 -0700 Subject: [PATCH] [inferbo] Symbolic value on functions returning only exception Summary: This diff generates a symbolic value when a function returns only exceptions. Previously, the exception expression is evaluated to top, thus it was propagated to other functions, which made those costs as top. For preventing that situation, this diff changed: * exception expressions are evaluated to bottom, and * if callee's return value is bottom, it generates a symbolic value for it. Reviewed By: ezgicicek Differential Revision: D17500386 fbshipit-source-id: 0fdcc710d --- infer/src/absint/AbstractDomain.mli | 4 - .../bufferoverrun/bufferOverrunAnalysis.ml | 20 +++-- .../src/bufferoverrun/bufferOverrunChecker.ml | 4 +- .../src/bufferoverrun/bufferOverrunDomain.ml | 83 +++++++++++++++++-- .../src/bufferoverrun/bufferOverrunModels.ml | 2 +- infer/src/checkers/cost.ml | 2 + .../java/performance/UnknownCallsTest.java | 22 +++++ .../codetoanalyze/java/performance/issues.exp | 6 ++ 8 files changed, 120 insertions(+), 23 deletions(-) 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]