[biabd] ondemand analysis for `pthread_create` builtin

Summary:
When we see `pthread_create(..., ..., foo, ...)`, we want to call the function
`foo` to check that its precondition is met.  The initial goal was to get rid
of the uncouth call to `Summary.get` when what we really want is to analyse
`foo` instead of just betting on the fact that it has been analysed already.

Besides switching to `Ondemand.analyze_proc_name`, this also changes the
matching of the function pointer in the arguments of `pthread_create()` to
detect the common case of a constant function name. I also added tests.

Reviewed By: jeremydubreil

Differential Revision: D9195159

fbshipit-source-id: dfec79f14

infer/src/biabduction/BuiltinDefn.ml

@@ -635,30 +635,39 @@ let execute___cxx_typeid ({Builtin.pdesc; tenv; prop_; args; loc; exe_env} as r)
       raise (Exceptions.Wrong_argument_number __POS__)
 
 
-let execute_pthread_create ({Builtin.tenv; prop_; path; args; exe_env} as builtin_args)
+let execute_pthread_create ({Builtin.tenv; pdesc; prop_; path; args; exe_env} as builtin_args)
     : Builtin.ret_typ =
   match args with
   | [_; _; start_routine; arg]
     -> (
       let routine_name = Prop.exp_normalize_prop tenv prop_ (fst start_routine) in
       let routine_arg = Prop.exp_normalize_prop tenv prop_ (fst arg) in
-      match (routine_name, snd start_routine) with
+      let pname =
-      | Exp.Lvar pvar, _
+        match (routine_name, snd start_routine) with
-        -> (
+        | Exp.Lvar pvar, _ ->
-          let fun_name = Pvar.get_name pvar in
+            let fun_name = Pvar.get_name pvar in
-          let fun_string = Mangled.to_string fun_name in
+            let fun_string = Mangled.to_string fun_name in
-          L.d_strln ("pthread_create: calling function " ^ fun_string) ;
+            Some (Typ.Procname.from_string_c_fun fun_string)
-          match Summary.get (Typ.Procname.from_string_c_fun fun_string) with
+        | Exp.Const (Cfun pname), _ ->
+            Some pname
+        | _ ->
+            None
+      in
+      match pname with
+      | None ->
+          L.d_str "pthread_create: unknown function " ;
+          Sil.d_exp routine_name ;
+          L.d_strln ", skipping call." ;
+          [(prop_, path)]
+      | Some pname ->
+          L.d_strln ("pthread_create: calling function " ^ Typ.Procname.to_string pname) ;
+          match Ondemand.analyze_proc_name ~caller_pdesc:pdesc pname with
           | None ->
-              assert false
+              (* no precondition to check, skip *)
+              [(prop_, path)]
           | Some callee_summary ->
               SymExec.proc_call exe_env callee_summary
                 {builtin_args with args= [(routine_arg, snd arg)]} )
-      | _ ->
-          L.d_str "pthread_create: unknown function " ;
-          Sil.d_exp routine_name ;
-          L.d_strln ", skipping call." ;
-          [(prop_, path)] )
   | _ ->
       raise (Exceptions.Wrong_argument_number __POS__)
 

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

@@ -36,6 +36,7 @@ codetoanalyze/c/errors/memory_leaks/test.c, malloc_sizeof_value_leak_bad, 7, MEM
 codetoanalyze/c/errors/memory_leaks/test.c, malloc_sizeof_value_leak_bad, 8, ARRAY_OUT_OF_BOUNDS_L3, no_bucket
 codetoanalyze/c/errors/memory_leaks/test.c, simple_leak, 2, MEMORY_LEAK, no_bucket
 codetoanalyze/c/errors/memory_leaks/test.c, uses_allocator, 3, MEMORY_LEAK, no_bucket
+codetoanalyze/c/errors/mutex/pthread_create.c, pthread_create_deref_bad, 2, NULL_DEREFERENCE, B5
 codetoanalyze/c/errors/mutex/pthread_mutex.c, double_init_bad, 2, PRECONDITION_NOT_MET, no_bucket
 codetoanalyze/c/errors/mutex/pthread_mutex.c, double_lock_bad2, 4, LOCKING_ALREADY_LOCKED_MUTEX, no_bucket
 codetoanalyze/c/errors/mutex/pthread_mutex.c, double_lock_bad2, 4, LOCKING_UNINITIALIZED_MUTEX, no_bucket

infer/tests/codetoanalyze/c/errors/mutex/pthread_create.c

@@ -0,0 +1,34 @@
+/*
+ * Copyright (c) 2017-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.
+ */
+#include <pthread.h>
+
+void dummy() {}
+
+void deref_pointer(int* x) { int y = *x; }
+
+int pthread_create_dummy_ok() {
+  pthread_t thread;
+  return pthread_create(&thread, NULL, dummy, NULL);
+}
+
+int pthread_create_deref_bad() {
+  pthread_t thread;
+  return pthread_create(&thread, NULL, deref_pointer, NULL);
+}
+
+int pthread_create_deref_ok() {
+  pthread_t thread;
+  int x;
+  return pthread_create(&thread, NULL, deref_pointer, &x);
+}
+
+extern void some_unknown_function(void);
+
+int pthread_unknown_ok() {
+  pthread_t thread;
+  return pthread_create(&thread, NULL, some_unknown_function, NULL);
+}