From 987ef9ef67aa94191a0c5d3a26bb139a69909dee Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Tue, 7 Aug 2018 09:49:27 -0700 Subject: [PATCH] [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 | 37 ++++++++++++------- infer/tests/codetoanalyze/c/errors/issues.exp | 1 + .../c/errors/mutex/pthread_create.c | 34 +++++++++++++++++ 3 files changed, 58 insertions(+), 14 deletions(-) create mode 100644 infer/tests/codetoanalyze/c/errors/mutex/pthread_create.c diff --git a/infer/src/biabduction/BuiltinDefn.ml b/infer/src/biabduction/BuiltinDefn.ml index 43644fb1a..5a66b79c6 100644 --- a/infer/src/biabduction/BuiltinDefn.ml +++ b/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 - | Exp.Lvar pvar, _ - -> ( - let fun_name = Pvar.get_name pvar in - let fun_string = Mangled.to_string fun_name in - L.d_strln ("pthread_create: calling function " ^ fun_string) ; - match Summary.get (Typ.Procname.from_string_c_fun fun_string) with + let pname = + match (routine_name, snd start_routine) with + | Exp.Lvar pvar, _ -> + let fun_name = Pvar.get_name pvar in + let fun_string = Mangled.to_string fun_name in + Some (Typ.Procname.from_string_c_fun fun_string) + | 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__) diff --git a/infer/tests/codetoanalyze/c/errors/issues.exp b/infer/tests/codetoanalyze/c/errors/issues.exp index 181fb31bd..792cf68a9 100644 --- a/infer/tests/codetoanalyze/c/errors/issues.exp +++ b/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 diff --git a/infer/tests/codetoanalyze/c/errors/mutex/pthread_create.c b/infer/tests/codetoanalyze/c/errors/mutex/pthread_create.c new file mode 100644 index 000000000..ff61d5b1f --- /dev/null +++ b/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 + +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); +}