[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

@@ -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
 

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, _) ->

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

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

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}
 
 

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

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++) {}
+  }
 }

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]