From 5a71583c72f672f3d0c801623d1f64fd71dba313 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Wed, 29 Jul 2020 01:40:54 -0700 Subject: [PATCH] [inferbo] Remove symbols on functions returning only exception Summary: D17500386 had added the ability to give symbolic values on functions returning exceptions. However, this might cause FPs or cryptic complexity reports (especially with subclass heuristics). This diff aims to revert it back. Reviewed By: skcho Differential Revision: D22764266 fbshipit-source-id: 1615544d8 --- .../bufferoverrun/bufferOverrunAnalysis.ml | 30 +++++-------------- .../src/bufferoverrun/bufferOverrunDomain.ml | 2 -- .../src/bufferoverrun/bufferOverrunDomain.mli | 2 -- .../java/performance/UnknownCallsTest.java | 4 +-- .../java/performance/cost-issues.exp | 2 +- .../codetoanalyze/java/performance/issues.exp | 2 ++ 6 files changed, 12 insertions(+), 30 deletions(-) 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]