[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

infer/src/bufferoverrun/bufferOverrunAnalysis.ml

@@ -69,20 +69,8 @@ module TransferFunctions = struct
         mem
 
 
-  let symbolic_pname_value pname params typ location mem =
+  let instantiate_mem_reachable ret_id callee_formals callee_pname ~callee_exit_mem
-    let obj_path =
+      ({Dom.eval_locpath} as eval_sym_trace) mem location =
-      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 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
+          Dom.Mem.find (Loc.of_pvar (Pvar.get_ret_pvar callee_pname)) callee_exit_mem
-            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
     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
+      instantiate_mem_reachable ret_id callee_formals callee_pname ~callee_exit_mem eval_sym_trace
-        eval_sym_trace caller_mem location
+        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. *)

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

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. *)
 

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
+  void call_throw_exception_unknown() {
-  // prevent poisoning the callees with Tops.
-  void call_throw_exception_linear() {
     for (int i = 0; i < throw_exception(); i++) {}
   }
 

infer/tests/codetoanalyze/java/performance/cost-issues.exp

@@ -351,7 +351,7 @@ codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.<init>(),
 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]

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, [<Length trace>,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, [<LHS trace>,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, [<LHS trace>,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, [<Offset trace>,Assignment,<Length trace>,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, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]