[inferbo] Return unknown value on non-const function calls

Summary:
It returns unknown values on non-const function calls like on unknown
function calls.

Reviewed By: mbouaziz

Differential Revision: D9478862

fbshipit-source-id: 4b795ec55

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -197,12 +197,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                 "/!\\ Unknown call to %a at %a@\n" Typ.Procname.pp callee_pname Location.pp
                 location ;
               Dom.Mem.add_unknown_from id ~callee_pname ~location mem )
-      | Call (_, fun_exp, _, location, _) ->
+      | Call ((id, _), fun_exp, _, location, _) ->
           let () =
             L.(debug BufferOverrun Verbose)
               "/!\\ Call to non-const function %a at %a" Exp.pp fun_exp Location.pp location
           in
-          mem
+          Dom.Mem.add_unknown_from_funcptr id ~location mem
       | Remove_temps (temps, _) ->
           Dom.Mem.remove_temps temps mem
       | Abstract _ | Nullify _ ->
@@ -571,8 +571,8 @@ module Report = struct
           else
             let desc = Format.asprintf "Parameter: %a" Loc.pp loc in
             (Errlog.make_trace_element depth location desc [] :: trace, depth)
-      | Trace.UnknownFrom (pname, location) ->
+      | Trace.UnknownFrom (pname_opt, location) ->
-          let desc = Format.asprintf "Unknown value from: %a" Typ.Procname.pp pname in
+          let desc = Format.asprintf "Unknown value from: %a" Trace.pp_pname_opt pname_opt in
           (Errlog.make_trace_element depth location desc [] :: trace, depth)
     in
     List.fold_right ~f ~init:([], 0) trace.trace |> fst |> List.rev

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -741,7 +741,8 @@ module MemReach = struct
 
   let add_heap : Loc.t -> Val.t -> t -> t = fun k v m -> {m with heap= Heap.add k v m.heap}
 
-  let add_unknown_from : Ident.t -> callee_pname:Typ.Procname.t -> location:Location.t -> t -> t =
+  let add_unknown_from
+      : Ident.t -> callee_pname:Typ.Procname.t option -> location:Location.t -> t -> t =
    fun id ~callee_pname ~location m ->
     let val_unknown = Val.unknown_from ~callee_pname ~location in
     add_stack (Loc.of_id id) val_unknown m |> add_heap Loc.unknown val_unknown
@@ -938,7 +939,12 @@ module Mem = struct
   let add_heap : Loc.t -> Val.t -> t -> t = fun k v -> f_lift (MemReach.add_heap k v)
 
   let add_unknown_from : Ident.t -> callee_pname:Typ.Procname.t -> location:Location.t -> t -> t =
-   fun id ~callee_pname ~location -> f_lift (MemReach.add_unknown_from id ~callee_pname ~location)
+   fun id ~callee_pname ~location ->
+    f_lift (MemReach.add_unknown_from id ~callee_pname:(Some callee_pname) ~location)
+
+
+  let add_unknown_from_funcptr : Ident.t -> location:Location.t -> t -> t =
+   fun id ~location -> f_lift (MemReach.add_unknown_from id ~callee_pname:None ~location)
 
 
   let strong_update_heap : PowLoc.t -> Val.t -> t -> t =

infer/src/bufferoverrun/bufferOverrunTrace.ml

@@ -18,7 +18,7 @@ module BoTrace = struct
     | Call of Location.t
     | Return of Location.t
     | SymAssign of Loc.t * Location.t
-    | UnknownFrom of Typ.Procname.t * Location.t
+    | UnknownFrom of Typ.Procname.t option * Location.t
   [@@deriving compare]
 
   type t = {length: int; trace: elem list} [@@deriving compare]
@@ -31,6 +31,13 @@ module BoTrace = struct
 
   let append x y = {length= x.length + y.length; trace= x.trace @ y.trace}
 
+  let pp_pname_opt fmt = function
+    | None ->
+        F.fprintf fmt "non-const function"
+    | Some pname ->
+        Typ.Procname.pp fmt pname
+
+
   let pp_elem : F.formatter -> elem -> unit =
    fun fmt elem ->
     match elem with
@@ -48,8 +55,8 @@ module BoTrace = struct
         F.fprintf fmt "Return (%a)" Location.pp_file_pos location
     | SymAssign (loc, location) ->
         F.fprintf fmt "SymAssign (%a, %a)" Loc.pp loc Location.pp_file_pos location
-    | UnknownFrom (pname, location) ->
+    | UnknownFrom (pname_opt, location) ->
-        F.fprintf fmt "UnknownFrom (%a, %a)" Typ.Procname.pp pname Location.pp_file_pos location
+        F.fprintf fmt "UnknownFrom (%a, %a)" pp_pname_opt pname_opt Location.pp_file_pos location
 
 
   let pp : F.formatter -> t -> unit =

infer/tests/codetoanalyze/c/bufferoverrun/function_call.c

@@ -72,3 +72,21 @@ void call_by_struct_ptr_bad() {
   struct_ptr_set_to_zero(sp);
   arr[sp->field - 1] = 123;
 }
+
+int ret_zero() { return 0; }
+
+void call_function_ptr_good_FP() {
+  int (*func_ptr)(void) = &ret_zero;
+  int arr[10];
+  if ((*func_ptr)() != 0) {
+    arr[10] = 1;
+  }
+}
+
+void call_function_ptr_bad() {
+  int (*func_ptr)(void) = &ret_zero;
+  int arr[10];
+  if ((*func_ptr)() == 0) {
+    arr[10] = 1;
+  }
+}

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

@@ -22,6 +22,8 @@ codetoanalyze/c/bufferoverrun/for_loop.c, for_loop, 10, BUFFER_OVERRUN_L3, no_bu
 codetoanalyze/c/bufferoverrun/function_call.c, call_by_arr_bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: -1 Size: 10]
 codetoanalyze/c/bufferoverrun/function_call.c, call_by_ptr_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: -1 Size: 10]
 codetoanalyze/c/bufferoverrun/function_call.c, call_by_struct_ptr_bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: -1 Size: 10]
+codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10]
+codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_good_FP, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10]
 codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: arr,Assignment,ArrayAccess: Offset: 100 Size: 10 by call to `arr_access` ]
 codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_bad_FN, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
 codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_bad_FN, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []