[pulse] resolve function pointers when known

Summary:
There's already all the ingredients to treat function pointers pretty
well, even when stored inside (const) globals.

In OpenSSL they use something like the added tests but the globals are
not const... This may need tweaking via an option, eg to inline all
global initializers, or filtered by global names/file names. Or just
use the existing --pulse-model-{alloc,release}-pattern options.

Reviewed By: skcho

Differential Revision: D28221651

fbshipit-source-id: 5399f1141

infer/src/pulse/Pulse.ml

@@ -23,14 +23,6 @@ let report_topl_errors proc_desc err_log summary =
   List.iter ~f summary
 
 
-let proc_name_of_call call_exp =
-  match (call_exp : Exp.t) with
-  | Const (Cfun proc_name) | Closure {name= proc_name} ->
-      Some proc_name
-  | _ ->
-      None
-
-
 module PulseTransferFunctions = struct
   module CFG = ProcCfg.Normal
   module Domain = ExecutionDomain
@@ -146,14 +138,14 @@ module PulseTransferFunctions = struct
             :: rev_func_args ) )
     in
     let func_args = List.rev rev_func_args in
-    let callee_pname = proc_name_of_call call_exp in
+    let<*> astate, callee_pname = PulseOperations.eval_proc_name call_loc call_exp astate in
     let model =
       match callee_pname with
       | Some callee_pname ->
           PulseModels.dispatch tenv callee_pname func_args
           |> Option.map ~f:(fun model -> (model, callee_pname))
       | None ->
-          (* function pointer, etc.: skip for now *)
+          (* unresolved function pointer, etc.: skip *)
           None
     in
     (* do interprocedural call then destroy objects going out of scope *)
@@ -300,13 +292,15 @@ module PulseTransferFunctions = struct
           in
           let set_global_astates =
             match rhs_exp with
-            | Lvar pvar when Pvar.is_global pvar && Pvar.is_compile_constant pvar -> (
+            | Lvar pvar when Pvar.(is_global pvar && (is_const pvar || is_compile_constant pvar))
+              -> (
               (* Inline initializers of global constants when they are being used.
                  This addresses nullptr false positives by pruning infeasable paths global_var != global_constant_value,
                  where global_constant_value is the value of global_var *)
               (* TODO: Initial global constants only once *)
               match Pvar.get_initializer_pname pvar with
               | Some proc_name ->
+                  L.d_printfln_escaped "Found initializer for %a" (Pvar.pp Pp.text) pvar ;
                   let call_flags = CallFlags.default in
                   let ret_id_void = (Ident.create_fresh Ident.knormal, StdTyp.void) in
                   let no_error_states =

infer/src/pulse/PulseOperations.ml

@@ -214,6 +214,9 @@ let eval mode location exp0 astate =
               (astate, (captured_as, addr_trace, mode) :: rev_captured) )
         in
         Closures.record location name (List.rev rev_captured) astate
+    | Const (Cfun proc_name) ->
+        (* function pointers are represented as closures with no captured variables *)
+        Ok (Closures.record location proc_name [] astate)
     | Cast (_, exp') ->
         eval mode exp' astate
     | Const (Cint i) ->
@@ -277,6 +280,15 @@ let eval_deref location exp astate =
   Memory.eval_edge addr_hist Dereference astate
 
 
+let eval_proc_name location call_exp astate =
+  match (call_exp : Exp.t) with
+  | Const (Cfun proc_name) | Closure {name= proc_name} ->
+      Ok (astate, Some proc_name)
+  | _ ->
+      let+ astate, (f, _) = eval Read location call_exp astate in
+      (astate, AddressAttributes.get_closure_proc_name f astate)
+
+
 let eval_structure_isl mode loc exp astate =
   match (exp : Exp.t) with
   | Lfield (exp', field, _) ->

infer/src/pulse/PulseOperations.mli

@@ -117,6 +117,8 @@ val eval_access :
 (** Like [eval] but starts from an address instead of an expression, checks that it is valid, and if
     so dereferences it according to the access. *)
 
+val eval_proc_name : Location.t -> Exp.t -> t -> (t * Procname.t option) AccessResult.t
+
 val havoc_id : Ident.t -> ValueHistory.t -> t -> t
 
 val havoc_field :

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

@@ -13,6 +13,9 @@ codetoanalyze/c/pulse/memory_leak.c, malloc_formal_leak_bad, 0, MEMORY_LEAK, no_
 codetoanalyze/c/pulse/memory_leak.c, malloc_interproc_no_free_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `create_p` here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here]
 codetoanalyze/c/pulse/memory_leak.c, malloc_interproc_no_free_bad2, 5, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here]
 codetoanalyze/c/pulse/memory_leak.c, malloc_no_free_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here]
+codetoanalyze/c/pulse/memory_leak.c, malloc_ptr_leak_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `malloc_via_ptr` here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here]
+codetoanalyze/c/pulse/memory_leak.c, malloc_ptr_no_check_leak_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,when calling `malloc_via_ptr` here,assigned,is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `malloc_via_ptr`,return from call to `malloc_via_ptr`,assigned,invalid access occurs here]
+codetoanalyze/c/pulse/memory_leak.c, malloc_ptr_no_check_leak_bad, 3, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `malloc_via_ptr` here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here]
 codetoanalyze/c/pulse/nullptr.c, bug_after_abduction_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
 codetoanalyze/c/pulse/nullptr.c, bug_after_malloc_result_test_bad, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
 codetoanalyze/c/pulse/nullptr.c, bug_with_allocation_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]

infer/tests/codetoanalyze/c/pulse/memory_leak.c

@@ -36,3 +36,36 @@ void malloc_interproc_no_free_bad2() {
 }
 
 void malloc_formal_leak_bad(int* x) { x = (int*)malloc(sizeof(int*)); }
+
+static void* (*const malloc_func)(size_t) = malloc;
+static void (*const free_func)(void*) = free;
+
+void* malloc_via_ptr(size_t size) {
+  void* ret = NULL;
+
+  if (size <= 0) {
+    return NULL;
+  }
+
+  ret = malloc_func(size);
+  return ret;
+}
+
+void free_via_ptr(void* x) { free_func(x); }
+
+void malloc_ptr_leak_bad() { int* p = (int*)malloc_via_ptr(sizeof(int)); }
+
+void malloc_ptr_no_check_leak_bad() {
+  int* p = (int*)malloc_via_ptr(sizeof(int));
+  *p = 42;
+}
+
+void malloc_ptr_free_ok() {
+  int* p = (int*)malloc_via_ptr(sizeof(int));
+  free(p);
+}
+
+void malloc_ptr_free_ptr_ok() {
+  int* p = (int*)malloc_via_ptr(sizeof(int));
+  free_via_ptr(p);
+}