[inferbo] Avoid top value on unknown non-static function call

Summary:
This diff avoids making top values on unknown non-static function,
such as abstract function, calls.  This is necessary because the
generated top values ruin the precision of the cost checker.

Reviewed By: ezgicicek

Differential Revision: D17418611

fbshipit-source-id: aeb759bdd

infer/src/bufferoverrun/bufferOverrunAnalysis.ml

@@ -80,6 +80,11 @@ module TransferFunctions = struct
     Dom.Mem.find (Loc.of_allocsite (Allocsite.make_symbol path)) mem
 
 
+  let assign_symbolic_pname_value pname (id, typ) location mem =
+    let v = symbolic_pname_value pname typ location mem in
+    Dom.Mem.add_stack (Loc.of_id id) v 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 =
@@ -144,6 +149,14 @@ module TransferFunctions = struct
         false
 
 
+  let is_non_static pname =
+    match pname with
+    | Typ.Procname.Java java_pname ->
+        not (Typ.Procname.Java.is_static java_pname)
+    | _ ->
+        false
+
+
   let instantiate_mem :
          Tenv.t
       -> Typ.IntegerWidths.t
@@ -268,7 +281,7 @@ module TransferFunctions = struct
         mem
     | Prune (exp, _, _, _) ->
         Sem.Prune.prune integer_type_widths exp mem
-    | Call (((id, ret_typ) as ret), Const (Cfun callee_pname), params, location, _) -> (
+    | Call (((id, _) as ret), Const (Cfun callee_pname), params, location, _) -> (
         let mem = Dom.Mem.add_stack_loc (Loc.of_id id) mem in
         match Models.Call.dispatch tenv callee_pname params with
         | Some {Models.exec} ->
@@ -289,8 +302,11 @@ 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 v = symbolic_pname_value callee_pname ret_typ location mem in
+                assign_symbolic_pname_value callee_pname ret location mem )
-                Dom.Mem.add_stack (Loc.of_id id) v mem )
+              else if is_non_static callee_pname then (
+                L.(debug BufferOverrun Verbose)
+                  "/!\\ Non-static call to unknown  %a \n\n" Typ.Procname.pp callee_pname ;
+                assign_symbolic_pname_value callee_pname ret location mem )
               else Dom.Mem.add_unknown_from id ~callee_pname ~location mem ) )
     | Call ((id, _), fun_exp, _, location, _) ->
         let mem = Dom.Mem.add_stack_loc (Loc.of_id id) mem in

infer/tests/codetoanalyze/java/performance/UnknownCallsTest.java

@@ -85,4 +85,13 @@ class UnknownCallsTest {
   void call_may_throw_exception_constant() {
     for (int i = 0; i < may_throw_exception(); i++) {}
   }
+
+  abstract class AbstractC {
+    abstract int[] abstract_func();
+  }
+
+  void call_concrete_func_linear(AbstractC x) {
+    int[] a = x.abstract_func();
+    for (int i = 0; i < a.length; i++) {}
+  }
 }

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

@@ -183,6 +183,7 @@ codetoanalyze/java/performance/StringTest.java, StringTest.indexof_quadratic(jav
 codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.test_switch():int, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 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_concrete_func_linear(UnknownCallsTest$AbstractC):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 5 + 6 ⋅ UnknownCallsTest$AbstractC.abstract_func().length.ub, O(UnknownCallsTest$AbstractC.abstract_func().length.ub), degree = 1,{UnknownCallsTest$AbstractC.abstract_func().length.ub},Loop at line 95]
 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]