diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index f45089917..78df7ba06 100644 --- a/infer/src/pulse/Pulse.ml +++ b/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 = diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 3bf8a864f..0f54fe107 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/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, _) -> diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index 7804404a8..e8d6c3e5e 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/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 : diff --git a/infer/tests/codetoanalyze/c/pulse/issues.exp b/infer/tests/codetoanalyze/c/pulse/issues.exp index 2077e7c30..214abf5f1 100644 --- a/infer/tests/codetoanalyze/c/pulse/issues.exp +++ b/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] diff --git a/infer/tests/codetoanalyze/c/pulse/memory_leak.c b/infer/tests/codetoanalyze/c/pulse/memory_leak.c index 25d285a9f..3873a2619 100644 --- a/infer/tests/codetoanalyze/c/pulse/memory_leak.c +++ b/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); +}