[inferbo] Substitute symbolic value of unknown function call to top

Summary: This diff substitutes symbolic values for unknown functions in proof obligations to top.  The goal of the diff is to avoid generating too many number of proof obligations that cannot be concretized.

Reviewed By: ezgicicek

Differential Revision: D14537542

fbshipit-source-id: 7f8f3bb4b

infer/src/bufferoverrun/bufferOverrunAnalysis.ml

@@ -131,7 +131,8 @@ module TransferFunctions = struct
       Sem.get_subst_map tenv integer_type_widths callee_formals params caller_mem callee_exit_mem
     in
     let eval_sym_trace =
-      Sem.mk_eval_sym_trace integer_type_widths callee_formals params caller_mem ~strict:false
+      Sem.mk_eval_sym_trace integer_type_widths callee_formals params caller_mem
+        ~mode:Sem.EvalNormal
     in
     let caller_mem =
       instantiate_mem_reachable ret callee_formals callee_pname ~callee_exit_mem eval_sym_trace

infer/src/bufferoverrun/bufferOverrunProofObligations.ml

@@ -14,6 +14,7 @@ module Dom = BufferOverrunDomain
 module ItvPure = Itv.ItvPure
 module MF = MarkupFormatter
 module Relation = BufferOverrunDomainRelation
+module Sem = BufferOverrunSemantics
 module ValTrace = BufferOverrunTrace
 
 module ConditionTrace = struct
@@ -753,9 +754,13 @@ module ConditionWithTrace = struct
         "Trying to substitute a non-symbolic condition %a from %a at %a. Why was it propagated in \
          the first place?"
         pp_summary cwt Typ.Procname.pp callee_pname Location.pp call_site ;
-    match Dom.Reachability.subst cwt.reachability (eval_sym_trace ~strict:true) call_site with
+    match
+      Dom.Reachability.subst cwt.reachability
+        (eval_sym_trace ~mode:Sem.EvalPOReachability)
+        call_site
+    with
     | `Reachable reachability -> (
-        let {Dom.eval_sym; trace_of_sym} = eval_sym_trace ~strict:false in
+        let {Dom.eval_sym; trace_of_sym} = eval_sym_trace ~mode:Sem.EvalPOCond in
         match Condition.subst eval_sym rel_map caller_relation cwt.cond with
         | None ->
             None

infer/src/bufferoverrun/bufferOverrunProofObligations.mli

@@ -73,7 +73,7 @@ module ConditionSet : sig
 
   val subst :
        summary_t
-    -> (strict:bool -> BufferOverrunDomain.eval_sym_trace)
+    -> (mode:BufferOverrunSemantics.eval_mode -> BufferOverrunDomain.eval_sym_trace)
     -> Relation.SubstMap.t
     -> Relation.t
     -> Typ.Procname.t

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -363,81 +363,97 @@ module ParamBindings = struct
     add_binding formals actuals empty
 end
 
-let rec eval_sympath_partial ~strict params p mem =
+(* There are three modes of ondemand evaluations.
+
+   EvalNormal: Given a symbolic value of an unknown function [Symb.SymbolPath.Callsite], it returns
+   a symbolic interval value.
+
+   EvalPOCond: Given a symbolic value of an unknown function, it returns the top interval value.
+   This is used when substituting condition expressions of proof obligations.
+
+   EvalPOReachability: This is similar to [EvalPOCond], but it returns the bottom location, instead
+   of the unknown location, when a location to substitute is not found.  This is used when
+   substituting reachabilities of proof obligations. *)
+type eval_mode = EvalNormal | EvalPOCond | EvalPOReachability
+
+let rec eval_sympath_partial ~mode params p mem =
   match p with
   | Symb.SymbolPath.Pvar x -> (
     try ParamBindings.find x params with Caml.Not_found ->
       L.d_printfln_escaped "Symbol %a is not found in parameters." (Pvar.pp Pp.text) x ;
       Val.Itv.top )
-  | Symb.SymbolPath.Callsite {cs} ->
+  | Symb.SymbolPath.Callsite {cs} -> (
-      L.d_printfln_escaped "Symbol for %a is not expected to be in parameters." Typ.Procname.pp
+    match mode with
-        (CallSite.pname cs) ;
+    | EvalNormal ->
-      Mem.find (Loc.of_allocsite (Allocsite.make_symbol p)) mem
+        L.d_printfln_escaped "Symbol for %a is not expected to be in parameters." Typ.Procname.pp
+          (CallSite.pname cs) ;
+        Mem.find (Loc.of_allocsite (Allocsite.make_symbol p)) mem
+    | EvalPOCond | EvalPOReachability ->
+        Val.Itv.top )
   | Symb.SymbolPath.Deref _ | Symb.SymbolPath.Field _ ->
-      let locs = eval_locpath ~strict params p mem in
+      let locs = eval_locpath ~mode params p mem in
       Mem.find_set locs mem
 
 
-and eval_locpath ~strict params p mem =
+and eval_locpath ~mode params p mem =
   let res =
     match p with
     | Symb.SymbolPath.Pvar _ | Symb.SymbolPath.Callsite _ ->
-        let v = eval_sympath_partial ~strict params p mem in
+        let v = eval_sympath_partial ~mode params p mem in
         Val.get_all_locs v
     | Symb.SymbolPath.Deref (_, p) ->
-        let v = eval_sympath_partial ~strict params p mem in
+        let v = eval_sympath_partial ~mode params p mem in
         Val.get_all_locs v
     | Symb.SymbolPath.Field (fn, p) ->
-        let locs = eval_locpath ~strict params p mem in
+        let locs = eval_locpath ~mode params p mem in
         PowLoc.append_field ~fn locs
   in
-  if PowLoc.is_empty res && not strict then (
+  if PowLoc.is_empty res then (
-    L.d_printfln_escaped "Location value for %a is not found." Symb.SymbolPath.pp_partial p ;
+    match mode with
-    PowLoc.unknown )
+    | EvalPOReachability ->
+        res
+    | EvalNormal | EvalPOCond ->
+        L.d_printfln_escaped "Location value for %a is not found." Symb.SymbolPath.pp_partial p ;
+        PowLoc.unknown )
   else res
 
 
-let eval_sympath ~strict params sympath mem =
+let eval_sympath ~mode params sympath mem =
   match sympath with
   | Symb.SymbolPath.Normal p ->
-      let v = eval_sympath_partial ~strict params p mem in
+      let v = eval_sympath_partial ~mode params p mem in
       (Val.get_itv v, Val.get_traces v)
   | Symb.SymbolPath.Offset p ->
-      let v = eval_sympath_partial ~strict params p mem in
+      let v = eval_sympath_partial ~mode params p mem in
       (ArrayBlk.offsetof (Val.get_array_blk v), Val.get_traces v)
   | Symb.SymbolPath.Length p ->
-      let v = eval_sympath_partial ~strict params p mem in
+      let v = eval_sympath_partial ~mode params p mem in
       (ArrayBlk.sizeof (Val.get_array_blk v), Val.get_traces v)
 
 
-(* We have two modes (strict and non-strict) on evaluating location paths. When a location to
-   substitute is not found:
-   - non-strict mode (which is used by default): it returns the unknown location.
-   - strict mode (which is used only in the substitution of condition of proof obligation): it
-     returns the bottom location. *)
 let mk_eval_sym_trace integer_type_widths callee_formals actual_exps caller_mem =
   let params =
     let actuals = List.map ~f:(fun (a, _) -> eval integer_type_widths a caller_mem) actual_exps in
     ParamBindings.make callee_formals actuals
   in
-  let eval_sym s bound_end =
+  let eval_sym ~mode s bound_end =
     let sympath = Symb.Symbol.path s in
-    let itv, _ = eval_sympath ~strict:false params sympath caller_mem in
+    let itv, _ = eval_sympath ~mode params sympath caller_mem in
     Symb.Symbol.assert_bound_end s bound_end ;
     Itv.get_bound itv bound_end
   in
   let trace_of_sym s =
     let sympath = Symb.Symbol.path s in
-    let itv, traces = eval_sympath ~strict:false params sympath caller_mem in
+    let itv, traces = eval_sympath ~mode:EvalNormal params sympath caller_mem in
     if Itv.eq itv Itv.bot then TraceSet.bottom else traces
   in
-  let eval_locpath ~strict partial = eval_locpath ~strict params partial caller_mem in
+  let eval_locpath ~mode partial = eval_locpath ~mode params partial caller_mem in
-  fun ~strict -> {eval_sym; trace_of_sym; eval_locpath= eval_locpath ~strict}
+  fun ~mode -> {eval_sym= eval_sym ~mode; trace_of_sym; eval_locpath= eval_locpath ~mode}
 
 
 let mk_eval_sym integer_type_widths callee_pdesc actual_exps caller_mem =
   let eval_sym_trace =
-    mk_eval_sym_trace integer_type_widths callee_pdesc actual_exps caller_mem ~strict:false
+    mk_eval_sym_trace integer_type_widths callee_pdesc actual_exps caller_mem ~mode:EvalNormal
   in
   eval_sym_trace.eval_sym
 

infer/tests/codetoanalyze/java/bufferoverrun/.inferconfig

@@ -0,0 +1,3 @@
+{
+   "external-java-packages": ["external."]
+}

infer/tests/codetoanalyze/java/bufferoverrun/External.java

@@ -0,0 +1,20 @@
+/*
+ * Copyright (c) 2019-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+import external.library.SomeExternalClass;
+
+public class External {
+  /* This function should raise deduplicated issues because the symbolic value of external method
+   * should be instantiated to top. */
+  void external_function_Bad(SomeExternalClass v) {
+    int i = (int) (v.externalMethod1()) + 1 + (int) (v.externalMethod1()) + 1;
+  }
+
+  /* This function should have no proof obilgation. */
+  void call_external_function_Good(SomeExternalClass v) {
+    external_function_Bad(v);
+  }
+}

infer/tests/codetoanalyze/java/bufferoverrun/Makefile

@@ -10,6 +10,6 @@ INFER_OPTIONS = --bufferoverrun-only --no-filtering --debug-exceptions \
 
 INFERPRINT_OPTIONS = --issues-tests
 
-SOURCES = $(wildcard *.java)
+SOURCES = $(wildcard *.java) $(wildcard $(TESTS_DIR)/external/library/*.java)
 
 include $(TESTS_DIR)/javac.make

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

@@ -7,3 +7,5 @@ codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Ar
 codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning2_Good_FP():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Assignment,Array access: Offset: 10 Size: 5]
 codetoanalyze/java/bufferoverrun/ArrayMember.java, codetoanalyze.java.bufferoverrun.ArrayMember.load_array_member_Bad():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `this.buf[*]`,Assignment,<Length trace>,Array declaration,Assignment,Array access: Offset: [max(10, this.buf[*].lb), min(10, this.buf[*].ub)] Size: 10]
 codetoanalyze/java/bufferoverrun/CompressedData.java, codetoanalyze.java.bufferoverrun.CompressedData.decompressData(codetoanalyze.java.bufferoverrun.CompressedData$D):int, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Parameter `this.yy`,<RHS trace>,Parameter `d.cci[*].s`,Assignment,Binary operation: ([0, this.yy - 1] × d.cci[*].s):signed32]
+codetoanalyze/java/bufferoverrun/External.java, External.external_function_Bad(external.library.SomeExternalClass):void, 1, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Length trace>,Unknown value from: __cast,Array access: Offset: [-oo, +oo] Size: [0, +oo]]
+codetoanalyze/java/bufferoverrun/External.java, External.external_function_Bad(external.library.SomeExternalClass):void, 1, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Unknown value from: int Integer.intValue(),Assignment,<RHS trace>,Unknown value from: int Integer.intValue(),Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32]