[inferbo] Introduce closure value

Summary:
This diff extends inferbo's domain to include closure values.  The goal of this extension is to
follow missing semantics where closures are handled as values, for example, a closure is assigned to
an object field, then it is got later to call.

Due to the bottom-up nature of the analyzer, sometimes we don't know which values are written in a
field, which is the same for the other non-closure values.

Reviewed By: ezgicicek

Differential Revision: D23932186

fbshipit-source-id: 4a575d0de

Makefile

@@ -99,6 +99,7 @@ BUILD_SYSTEMS_TESTS += \
 
 DIRECT_TESTS += \
   objc_autoreleasepool \
+  objc_bufferoverrun \
   objc_biabduction \
   objc_frontend \
   objc_linters \

infer/src/IR/Typ.ml

@@ -601,6 +601,8 @@ let is_void typ = match typ.desc with Tvoid -> true | _ -> false
 
 let is_pointer_to_int typ = match typ.desc with Tptr ({desc= Tint _}, _) -> true | _ -> false
 
+let is_pointer_to_function typ = match typ.desc with Tptr ({desc= Tfun}, _) -> true | _ -> false
+
 let is_int typ = match typ.desc with Tint _ -> true | _ -> false
 
 let is_unsigned_int typ = match typ.desc with Tint ikind -> ikind_is_unsigned ikind | _ -> false

infer/src/IR/Typ.mli

@@ -332,6 +332,8 @@ val is_void : t -> bool
 
 val is_pointer_to_int : t -> bool
 
+val is_pointer_to_function : t -> bool
+
 val is_pointer : t -> bool
 
 val is_reference : t -> bool

infer/src/bufferoverrun/FuncPtr.ml

@@ -0,0 +1,42 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! IStd
+module SPath = Symb.SymbolPath
+
+type t = Path of SPath.partial | Closure of Exp.closure [@@deriving compare]
+
+let pp f = function
+  | Path path ->
+      SPath.pp_partial f path
+  | Closure closure ->
+      Exp.pp_closure f closure
+
+
+module Set = struct
+  include AbstractDomain.FiniteSet (struct
+    type nonrec t = t [@@deriving compare]
+
+    let pp = pp
+  end)
+
+  type eval_func_ptrs = SPath.partial -> t
+
+  let of_path path = singleton (Path path)
+
+  let of_closure closure = singleton (Closure closure)
+
+  let subst x eval_func_ptr =
+    fold
+      (fun func_ptr acc ->
+        match func_ptr with
+        | Path path ->
+            join acc (eval_func_ptr path)
+        | Closure _ ->
+            add func_ptr acc )
+      x empty
+end

infer/src/bufferoverrun/FuncPtr.mli

@@ -0,0 +1,22 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! IStd
+
+type t = Path of Symb.SymbolPath.partial | Closure of Exp.closure
+
+module Set : sig
+  include AbstractDomain.FiniteSetS with type elt = t
+
+  type eval_func_ptrs = Symb.SymbolPath.partial -> t
+
+  val of_path : Symb.SymbolPath.partial -> t
+
+  val of_closure : Exp.closure -> t
+
+  val subst : t -> eval_func_ptrs -> t
+end

infer/src/bufferoverrun/bufferOverrunAnalysis.ml

@@ -278,8 +278,45 @@ module TransferFunctions = struct
         Dom.Mem.add_unknown ret ~location mem
 
 
+  let call {interproc= {tenv}; get_summary; get_formals; oenv= {integer_type_widths}} node location
+      ((id, _) as ret) callee_pname params mem =
+    let mem = Dom.Mem.add_stack_loc (Loc.of_id id) mem in
+    let fun_arg_list =
+      List.map params ~f:(fun (exp, typ) ->
+          ProcnameDispatcher.Call.FuncArg.{exp; typ; arg_payload= ()} )
+    in
+    match Models.Call.dispatch tenv callee_pname fun_arg_list with
+    | Some {Models.exec} ->
+        let model_env =
+          let node_hash = CFG.Node.hash node in
+          BoUtils.ModelEnv.mk_model_env callee_pname ~node_hash location tenv integer_type_widths
+            get_summary
+        in
+        exec model_env ~ret mem
+    | None -> (
+        let {BoUtils.ReplaceCallee.pname= callee_pname; params; is_params_ref} =
+          BoUtils.ReplaceCallee.replace_make_shared tenv get_formals callee_pname params
+        in
+        match (get_summary callee_pname, get_formals callee_pname) with
+        | Some callee_exit_mem, Some callee_formals ->
+            instantiate_mem ~is_params_ref integer_type_widths id callee_formals callee_pname params
+              mem callee_exit_mem location
+        | _, _ ->
+            (* This may happen for procedures with a biabduction model too. *)
+            L.d_printfln_escaped "/!\\ Unknown call to %a" Procname.pp callee_pname ;
+            ScubaLogging.cost_log_message ~label:"unmodeled_function_inferbo"
+              ~message:(F.asprintf "Unmodeled Function[Inferbo] : %a" Procname.pp callee_pname) ;
+            Dom.Mem.add_unknown_from ret ~callee_pname ~location mem )
+
+
+  let unknown_call location ((id, _) as ret) mem =
+    let mem = Dom.Mem.add_stack_loc (Loc.of_id id) mem in
+    Dom.Mem.add_unknown ret ~location mem
+
+
   let exec_instr : Dom.Mem.t -> analysis_data -> CFG.Node.t -> Sil.instr -> Dom.Mem.t =
-   fun mem {interproc= {proc_desc; tenv}; get_summary; get_formals; oenv= {integer_type_widths}}
+   fun mem
+       ({interproc= {proc_desc; tenv}; get_summary; oenv= {integer_type_widths}} as analysis_data)
        node instr ->
     match instr with
     | Load {id} when Ident.is_none id ->
@@ -372,38 +409,19 @@ module TransferFunctions = struct
         assign_java_enum_values get_summary id
           ~caller_pname:(Procdesc.get_proc_name proc_desc)
           ~callee_pname mem
-    | Call (((id, _) as ret), Const (Cfun callee_pname), params, location, _) -> (
+    | Call (ret, Const (Cfun callee_pname), params, location, _) ->
-        let mem = Dom.Mem.add_stack_loc (Loc.of_id id) mem in
+        call analysis_data node location ret callee_pname params mem
-        let fun_arg_list =
+    | Call (ret, fun_exp, params, location, _) -> (
-          List.map params ~f:(fun (exp, typ) ->
+        let func_ptrs = Sem.eval integer_type_widths fun_exp mem |> Dom.Val.get_func_ptrs in
-              ProcnameDispatcher.Call.FuncArg.{exp; typ; arg_payload= ()} )
+        match FuncPtr.Set.is_singleton_or_more func_ptrs with
-        in
+        | Singleton (Closure {name= callee_pname}) ->
-        match Models.Call.dispatch tenv callee_pname fun_arg_list with
+            call analysis_data node location ret callee_pname params mem
-        | Some {Models.exec} ->
+        | More ->
-            let model_env =
+            L.d_printfln_escaped "/!\\ Call to multiple functions %a" Exp.pp fun_exp ;
-              let node_hash = CFG.Node.hash node in
+            unknown_call location ret mem
-              BoUtils.ModelEnv.mk_model_env callee_pname ~node_hash location tenv
+        | Empty | Singleton (Path _) ->
-                integer_type_widths get_summary
+            L.d_printfln_escaped "/!\\ Call to non-const function %a" Exp.pp fun_exp ;
-            in
+            unknown_call location ret mem )
-            exec model_env ~ret mem
-        | None -> (
-            let {BoUtils.ReplaceCallee.pname= callee_pname; params; is_params_ref} =
-              BoUtils.ReplaceCallee.replace_make_shared tenv get_formals callee_pname params
-            in
-            match (get_summary callee_pname, get_formals callee_pname) with
-            | Some callee_exit_mem, Some callee_formals ->
-                instantiate_mem ~is_params_ref integer_type_widths id callee_formals callee_pname
-                  params mem callee_exit_mem location
-            | _, _ ->
-                (* This may happen for procedures with a biabduction model too. *)
-                L.d_printfln_escaped "/!\\ Unknown call to %a" Procname.pp callee_pname ;
-                ScubaLogging.cost_log_message ~label:"unmodeled_function_inferbo"
-                  ~message:(F.asprintf "Unmodeled Function[Inferbo] : %a" Procname.pp callee_pname) ;
-                Dom.Mem.add_unknown_from ret ~callee_pname ~location mem ) )
-    | Call (((id, _) as ret), fun_exp, _, location, _) ->
-        let mem = Dom.Mem.add_stack_loc (Loc.of_id id) mem in
-        L.d_printfln_escaped "/!\\ Call to non-const function %a" Exp.pp fun_exp ;
-        Dom.Mem.add_unknown ret ~location mem
     | Metadata (VariableLifetimeBegins (pvar, typ, location)) when Pvar.is_global pvar ->
         let model_env =
           let pname = Procdesc.get_proc_name proc_desc in

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -84,8 +84,9 @@ end
 
 type eval_sym_trace =
   { eval_sym: Bounds.Bound.eval_sym
-  ; trace_of_sym: Symb.Symbol.t -> Trace.Set.t
+  ; eval_locpath: PowLoc.eval_locpath
-  ; eval_locpath: PowLoc.eval_locpath }
+  ; eval_func_ptrs: FuncPtr.Set.eval_func_ptrs
+  ; trace_of_sym: Symb.Symbol.t -> Trace.Set.t }
 
 module Val = struct
   type t =
@@ -95,6 +96,7 @@ module Val = struct
     ; modeled_range: ModeledRange.t
     ; powloc: PowLoc.t
     ; arrayblk: ArrayBlk.t
+    ; func_ptrs: FuncPtr.Set.t
     ; traces: TraceSet.t }
 
   let bot : t =
@@ -104,6 +106,7 @@ module Val = struct
     ; modeled_range= ModeledRange.bottom
     ; powloc= PowLoc.bot
     ; arrayblk= ArrayBlk.bot
+    ; func_ptrs= FuncPtr.Set.bottom
     ; traces= TraceSet.bottom }
 
 
@@ -119,12 +122,16 @@ module Val = struct
       if not (ModeledRange.is_bottom range) then
         F.fprintf fmt " (modeled_range:%a)" ModeledRange.pp range
     in
+    let func_ptrs_pp fmt func_ptrs =
+      if not (FuncPtr.Set.is_bottom func_ptrs) then
+        F.fprintf fmt ", func_ptrs:%a" FuncPtr.Set.pp func_ptrs
+    in
     let trace_pp fmt traces =
       if Config.bo_debug >= 3 then F.fprintf fmt ", %a" TraceSet.pp traces
     in
-    F.fprintf fmt "(%a%a%a%a, %a, %a%a)" Itv.pp x.itv itv_thresholds_pp x.itv_thresholds
+    F.fprintf fmt "(%a%a%a%a, %a, %a%a%a)" Itv.pp x.itv itv_thresholds_pp x.itv_thresholds
       itv_updated_by_pp x.itv_updated_by modeled_range_pp x.modeled_range PowLoc.pp x.powloc
-      ArrayBlk.pp x.arrayblk trace_pp x.traces
+      ArrayBlk.pp x.arrayblk func_ptrs_pp x.func_ptrs trace_pp x.traces
 
 
   let unknown_from : Typ.t -> callee_pname:_ -> location:_ -> t =
@@ -137,6 +144,7 @@ module Val = struct
     ; modeled_range= ModeledRange.bottom
     ; powloc= (if is_int then PowLoc.bot else PowLoc.unknown)
     ; arrayblk= (if is_int then ArrayBlk.bottom else ArrayBlk.unknown)
+    ; func_ptrs= FuncPtr.Set.bottom
     ; traces }
 
 
@@ -149,6 +157,7 @@ module Val = struct
       && ModeledRange.leq ~lhs:lhs.modeled_range ~rhs:rhs.modeled_range
       && PowLoc.leq ~lhs:lhs.powloc ~rhs:rhs.powloc
       && ArrayBlk.leq ~lhs:lhs.arrayblk ~rhs:rhs.arrayblk
+      && FuncPtr.Set.leq ~lhs:lhs.func_ptrs ~rhs:rhs.func_ptrs
 
 
   let widen ~prev ~next ~num_iters =
@@ -166,6 +175,7 @@ module Val = struct
           ModeledRange.widen ~prev:prev.modeled_range ~next:next.modeled_range ~num_iters
       ; powloc= PowLoc.widen ~prev:prev.powloc ~next:next.powloc ~num_iters
       ; arrayblk= ArrayBlk.widen ~prev:prev.arrayblk ~next:next.arrayblk ~num_iters
+      ; func_ptrs= FuncPtr.Set.widen ~prev:prev.func_ptrs ~next:next.func_ptrs ~num_iters
       ; traces= TraceSet.join prev.traces next.traces }
 
 
@@ -179,6 +189,7 @@ module Val = struct
       ; modeled_range= ModeledRange.join x.modeled_range y.modeled_range
       ; powloc= PowLoc.join x.powloc y.powloc
       ; arrayblk= ArrayBlk.join x.arrayblk y.arrayblk
+      ; func_ptrs= FuncPtr.Set.join x.func_ptrs y.func_ptrs
       ; traces= TraceSet.join x.traces y.traces }
 
 
@@ -196,6 +207,8 @@ module Val = struct
 
   let get_all_locs : t -> PowLoc.t = fun x -> PowLoc.join x.powloc (get_array_locs x)
 
+  let get_func_ptrs : t -> FuncPtr.Set.t = fun x -> x.func_ptrs
+
   let get_traces : t -> TraceSet.t = fun x -> x.traces
 
   let of_itv ?(traces = TraceSet.bottom) itv = {bot with itv; traces}
@@ -230,6 +243,8 @@ module Val = struct
     of_c_array_alloc allocsite ~stride ~offset ~size ~traces:TraceSet.bottom
 
 
+  let of_func_ptrs func_ptrs = {bot with func_ptrs}
+
   let deref_of_literal_string s =
     let max_char = String.fold s ~init:0 ~f:(fun acc c -> max acc (Char.to_int c)) in
     of_itv (Itv.set_lb_zero (Itv.of_int max_char))
@@ -449,7 +464,7 @@ module Val = struct
 
 
   let subst : t -> eval_sym_trace -> Location.t -> t =
-   fun x {eval_sym; trace_of_sym; eval_locpath} location ->
+   fun x {eval_sym; eval_locpath; eval_func_ptrs; trace_of_sym} location ->
     let symbols = get_symbols x in
     let traces_caller =
       Itv.SymbolSet.fold
@@ -463,6 +478,7 @@ module Val = struct
       itv= Itv.subst x.itv eval_sym
     ; powloc= PowLoc.join powloc powloc_from_arrayblk
     ; arrayblk
+    ; func_ptrs= FuncPtr.Set.subst x.func_ptrs eval_func_ptrs
     ; traces }
     (* normalize bottom *)
     |> normalize
@@ -505,7 +521,10 @@ module Val = struct
 
   let unknown_locs = of_pow_loc PowLoc.unknown ~traces:TraceSet.bottom
 
-  let is_bot x = Itv.is_bottom x.itv && PowLoc.is_bot x.powloc && ArrayBlk.is_bot x.arrayblk
+  let is_bot x =
+    Itv.is_bottom x.itv && PowLoc.is_bot x.powloc && ArrayBlk.is_bot x.arrayblk
+    && FuncPtr.Set.is_bottom x.func_ptrs
+
 
   let is_mone x = Itv.is_mone (get_itv x)
 
@@ -544,6 +563,8 @@ module Val = struct
         itv_val ~non_int:true |> set_itv_updated_by_unknown
     | Tint _ | Tvoid ->
         itv_val ~non_int:false |> set_itv_updated_by_addition
+    | Tptr ({desc= Tfun}, _) ->
+        of_func_ptrs (FuncPtr.Set.of_path path)
     | Tptr (elt, _) ->
         if is_java || SPath.is_this path then
           let deref_kind =
@@ -652,6 +673,9 @@ module Val = struct
               | Some typ when Loc.is_global l ->
                   L.d_printfln_escaped "Val.on_demand for %a -> global" Loc.pp l ;
                   do_on_demand path typ
+              | Some typ when Typ.is_pointer_to_function typ ->
+                  L.d_printfln_escaped "Val.on_demand for %a -> function pointer" Loc.pp l ;
+                  do_on_demand path typ
               | _ ->
                   L.d_printfln_escaped "Val.on_demand for %a -> no type" Loc.pp l ;
                   default )

infer/src/bufferoverrun/bufferOverrunDomain.mli

@@ -36,8 +36,9 @@ end
 (** type for on-demand symbol evaluation in Inferbo *)
 type eval_sym_trace =
   { eval_sym: Bounds.Bound.eval_sym  (** evaluating symbol *)
-  ; trace_of_sym: Symb.Symbol.t -> BufferOverrunTrace.Set.t  (** getting traces of symbol *)
+  ; eval_locpath: AbsLoc.PowLoc.eval_locpath  (** evaluating path *)
-  ; eval_locpath: AbsLoc.PowLoc.eval_locpath  (** evaluating path *) }
+  ; eval_func_ptrs: FuncPtr.Set.eval_func_ptrs  (** evaluating function pointers *)
+  ; trace_of_sym: Symb.Symbol.t -> BufferOverrunTrace.Set.t  (** getting traces of symbol *) }
 
 module Val : sig
   type t =
@@ -47,6 +48,7 @@ module Val : sig
     ; modeled_range: ModeledRange.t
     ; powloc: AbsLoc.PowLoc.t  (** Simple pointers *)
     ; arrayblk: ArrayBlk.t  (** Array blocks *)
+    ; func_ptrs: FuncPtr.Set.t  (** Function pointers *)
     ; traces: BufferOverrunTrace.Set.t }
 
   include AbstractDomain.S with type t := t
@@ -81,6 +83,8 @@ module Val : sig
 
   val of_pow_loc : traces:BufferOverrunTrace.Set.t -> AbsLoc.PowLoc.t -> t
 
+  val of_func_ptrs : FuncPtr.Set.t -> t
+
   val unknown_locs : t
 
   val unknown_from : Typ.t -> callee_pname:Procname.t option -> location:Location.t -> t
@@ -113,6 +117,8 @@ module Val : sig
 
   val get_pow_loc : t -> AbsLoc.PowLoc.t
 
+  val get_func_ptrs : t -> FuncPtr.Set.t
+
   val get_traces : t -> BufferOverrunTrace.Set.t
 
   val set_array_length : Location.t -> length:t -> t -> t

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -470,7 +470,13 @@ let mk_eval_sym_trace ?(is_params_ref = false) integer_type_widths
                   Mem.find_set (eval_locs a caller_mem) caller_mem )
             in
             this_actual :: actuals
-      else List.map ~f:(fun (a, _) -> eval integer_type_widths a caller_mem) actual_exps
+      else
+        List.map actual_exps ~f:(fun (a, _) ->
+            match (a : Exp.t) with
+            | Closure closure ->
+                FuncPtr.Set.of_closure closure |> Val.of_func_ptrs
+            | _ ->
+                eval integer_type_widths a caller_mem )
     in
     ParamBindings.make callee_formals actuals
   in
@@ -480,13 +486,20 @@ let mk_eval_sym_trace ?(is_params_ref = false) integer_type_widths
     Symb.Symbol.check_bound_end s bound_end ;
     Itv.get_bound itv bound_end
   in
+  let eval_locpath ~mode partial = eval_locpath ~mode params partial caller_mem in
+  let eval_func_ptrs ~mode partial =
+    eval_sympath_partial ~mode params partial caller_mem |> Val.get_func_ptrs
+  in
   let trace_of_sym s =
     let sympath = Symb.Symbol.path s 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 ~mode partial = eval_locpath ~mode params partial caller_mem in
+  fun ~mode ->
-  fun ~mode -> {eval_sym= eval_sym ~mode; trace_of_sym; eval_locpath= eval_locpath ~mode}
+    { eval_sym= eval_sym ~mode
+    ; eval_locpath= eval_locpath ~mode
+    ; eval_func_ptrs= eval_func_ptrs ~mode
+    ; trace_of_sym }
 
 
 let mk_eval_sym_mode ~mode integer_type_widths callee_formals actual_exps caller_mem =

infer/tests/codetoanalyze/objc/bufferoverrun/Makefile

@@ -0,0 +1,18 @@
+# Copyright (c) Facebook, Inc. and its affiliates.
+#
+# This source code is licensed under the MIT license found in the
+# LICENSE file in the root directory of this source tree.
+
+TESTS_DIR = ../../..
+
+CLANG_OPTIONS = -c $(OBJC_CLANG_OPTIONS)
+INFER_OPTIONS = --bufferoverrun-only --debug-exceptions --project-root $(TESTS_DIR) \
+  --report-force-relative-path --xcode-isysroot-suffix $(XCODE_ISYSROOT_SUFFIX)
+INFERPRINT_OPTIONS = --issues-tests
+
+SOURCES = $(wildcard *.m)
+
+include $(TESTS_DIR)/clang.make
+include $(TESTS_DIR)/objc.make
+
+infer-out/report.json: $(MAKEFILE_LIST)

infer/tests/codetoanalyze/objc/bufferoverrun/block.m

@@ -0,0 +1,53 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+#import <Foundation/Foundation.h>
+
+typedef int (^GetNum)();
+
+@interface MyObject : NSObject
+@end
+
+@implementation MyObject {
+  GetNum _get_num;
+}
+
+- (void)set_get_num:(GetNum)get_num {
+  _get_num = get_num;
+}
+
+- (GetNum)get_get_num {
+  return _get_num;
+}
+
+@end
+
+@interface Block : NSObject
+@end
+
+@implementation Block
+
+- (void)block_in_field_Good {
+  int a[10];
+  MyObject* o = [MyObject new];
+  [o set_get_num:^int {
+    return 5;
+  }];
+  GetNum get_num = [o get_get_num];
+  a[get_num()] = 0;
+}
+
+- (void)block_in_field_Bad {
+  int a[10];
+  MyObject* o = [MyObject new];
+  [o set_get_num:^int {
+    return 15;
+  }];
+  GetNum get_num = [o get_get_num];
+  a[get_num()] = 0;
+}
+
+@end

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

@@ -0,0 +1 @@
+codetoanalyze/objc/bufferoverrun/block.m, Block.block_in_field_Bad, 7, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Call,Assignment,<Length trace>,Array declaration,Array access: Offset: 15 Size: 10]