diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml index 599706b1c..6b0fdd89a 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml +++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml @@ -69,20 +69,8 @@ module TransferFunctions = struct mem - let symbolic_pname_value pname params typ location mem = - let obj_path = - match params with - | (param, _) :: _ -> - PowLoc.min_elt_opt (Sem.eval_locs param mem) |> Option.bind ~f:Loc.get_path - | _ -> - None - in - let path = Symb.SymbolPath.of_callsite ?obj_path ~ret_typ:typ (CallSite.make pname location) in - Dom.Mem.find (Loc.of_allocsite (Allocsite.make_symbol path)) mem - - - let instantiate_mem_reachable (ret_id, ret_typ) callee_formals callee_pname params - ~callee_exit_mem ({Dom.eval_locpath} as eval_sym_trace) mem location = + let instantiate_mem_reachable ret_id callee_formals callee_pname ~callee_exit_mem + ({Dom.eval_locpath} as eval_sym_trace) mem location = let formal_locs = List.fold callee_formals ~init:LocSet.empty ~f:(fun acc (formal, _) -> LocSet.add (Loc.of_pvar formal) acc ) @@ -122,9 +110,7 @@ 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)) | _ -> - if Language.curr_language_is Java && Dom.Mem.is_exc_raised callee_exit_mem then - symbolic_pname_value callee_pname params ret_typ location mem - else Dom.Mem.find (Loc.of_pvar (Pvar.get_ret_pvar callee_pname)) callee_exit_mem + 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 @@ -136,7 +122,7 @@ module TransferFunctions = struct let instantiate_mem : is_params_ref:bool -> Typ.IntegerWidths.t - -> Ident.t * Typ.t + -> Ident.t -> (Pvar.t * Typ.t) list -> Procname.t -> (Exp.t * Typ.t) list @@ -144,15 +130,15 @@ module TransferFunctions = struct -> BufferOverrunAnalysisSummary.t -> Location.t -> Dom.Mem.t = - fun ~is_params_ref integer_type_widths ret callee_formals callee_pname params caller_mem + fun ~is_params_ref integer_type_widths ret_id callee_formals callee_pname params caller_mem callee_exit_mem location -> let eval_sym_trace = Sem.mk_eval_sym_trace ~is_params_ref integer_type_widths callee_formals params caller_mem ~mode:Sem.EvalNormal in let mem = - instantiate_mem_reachable ret callee_formals callee_pname params ~callee_exit_mem - eval_sym_trace caller_mem location + instantiate_mem_reachable ret_id callee_formals callee_pname ~callee_exit_mem eval_sym_trace + caller_mem location in if Language.curr_language_is Java then Dom.Mem.incr_iterator_simple_alias_on_call eval_sym_trace ~callee_exit_mem mem @@ -409,7 +395,7 @@ module TransferFunctions = struct with | callee_pname, `Found (callee_exit_mem, callee_formals) | _, `FoundFromSubclass (callee_pname, callee_exit_mem, callee_formals) -> - instantiate_mem ~is_params_ref integer_type_widths ret callee_formals callee_pname + instantiate_mem ~is_params_ref integer_type_widths id callee_formals callee_pname params mem callee_exit_mem location | _, `NotFound -> (* This may happen for procedures with a biabduction model too. *) diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index b7b6b14dd..20b18075c 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -2226,8 +2226,6 @@ module Mem = struct let exc_raised : t = ExcRaised - let is_exc_raised = function ExcRaised -> true | _ -> false - let leq ~lhs ~rhs = if phys_equal lhs rhs then true else diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.mli b/infer/src/bufferoverrun/bufferOverrunDomain.mli index d75534855..256e12ed8 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.mli +++ b/infer/src/bufferoverrun/bufferOverrunDomain.mli @@ -467,8 +467,6 @@ module Mem : sig val exc_raised : t - val is_exc_raised : _ t0 -> bool - val is_rep_multi_loc : AbsLoc.Loc.t -> _ t0 -> bool (** Check if an abstract location represents multiple concrete locations. *) diff --git a/infer/tests/codetoanalyze/java/performance/UnknownCallsTest.java b/infer/tests/codetoanalyze/java/performance/UnknownCallsTest.java index 5eb55289b..70c78b9a3 100644 --- a/infer/tests/codetoanalyze/java/performance/UnknownCallsTest.java +++ b/infer/tests/codetoanalyze/java/performance/UnknownCallsTest.java @@ -67,9 +67,7 @@ class UnknownCallsTest { throw new IllegalStateException(); } - // specifically for exceptions, we generate a symbolic value to - // prevent poisoning the callees with Tops. - void call_throw_exception_linear() { + void call_throw_exception_unknown() { for (int i = 0; i < throw_exception(); i++) {} } diff --git a/infer/tests/codetoanalyze/java/performance/cost-issues.exp b/infer/tests/codetoanalyze/java/performance/cost-issues.exp index 7ebc7c4ea..3d7271e47 100644 --- a/infer/tests/codetoanalyze/java/performance/cost-issues.exp +++ b/infer/tests/codetoanalyze/java/performance/cost-issues.exp @@ -351,7 +351,7 @@ codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.(), codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_concrete_func_linear_FP(UnknownCallsTest$AbstractC):void, ⊤, OnUIThread:false, [Unbounded loop,Loop] codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_loop_over_charArray_FP(java.lang.StringBuilder,java.lang.String):void, ⊤, OnUIThread:false, [Call to void UnknownCallsTest.loop_over_charArray_FP(StringBuilder,String),Unbounded loop,Loop] codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_may_throw_exception_constant():void, 220, OnUIThread:false, [] -codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_throw_exception_linear():void, 5 + 5 ⋅ UnknownCallsTest.throw_exception().ub + 8 ⋅ (1+max(0, UnknownCallsTest.throw_exception().ub)), OnUIThread:false, [{1+max(0, UnknownCallsTest.throw_exception().ub)},Loop,{UnknownCallsTest.throw_exception().ub},Loop] +codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_throw_exception_unknown():void, ⊤, OnUIThread:false, [Unbounded loop,Loop] codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.jsonArray_constant():void, 22, OnUIThread:false, [] codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.jsonArray_linear(org.json.JSONArray):void, 8 + 5 ⋅ jsonArray.length, OnUIThread:false, [{jsonArray.length},Loop] codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.loop_over_charArray_FP(java.lang.StringBuilder,java.lang.String):void, ⊤, OnUIThread:false, [Unbounded loop,Loop] diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index 886b11c45..60c713deb 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -79,6 +79,8 @@ codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_conc codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_concrete_func_linear_FP(UnknownCallsTest$AbstractC):void, 2, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: int[] UnknownCallsTest$AbstractC.abstract_func(),Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_concrete_func_linear_FP(UnknownCallsTest$AbstractC):void, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [,Unknown value from: int[] UnknownCallsTest$AbstractC.abstract_func(),Binary operation: ([0, +oo] + 1):signed32] codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_loop_over_charArray_FP(java.lang.StringBuilder,java.lang.String):void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Call to void UnknownCallsTest.loop_over_charArray_FP(StringBuilder,String),Unbounded loop,Loop] +codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_throw_exception_unknown():void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop] +codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_throw_exception_unknown():void, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.loop_over_charArray_FP(java.lang.StringBuilder,java.lang.String):void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop] codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.loop_over_charArray_FP(java.lang.StringBuilder,java.lang.String):void, 1, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Assignment,,Unknown value from: char[] String.toCharArray(),Array access: Offset: [-oo, +oo] (⇐ [-oo, +oo] + [0, +oo]) Size: [0, +oo]] codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.loop_over_charArray_FP(java.lang.StringBuilder,java.lang.String):void, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32]