diff --git a/infer/man/man1/infer-analyze.txt b/infer/man/man1/infer-analyze.txt index e41abc0ae..57fe2c08e 100644 --- a/infer/man/man1/infer-analyze.txt +++ b/infer/man/man1/infer-analyze.txt @@ -287,10 +287,22 @@ OPTIONS Regex of methods that should be modelled as allocs in Pulse --pulse-model-free-pattern string - Regex of methods that should be modelled as free in Pulse + Regex of methods that should be modelled as wrappers to free(3) in + Pulse. The pointer to be freed should be the first argument of the + function. This should only be needed if the code of the wrapper is + not visible to infer or if Pulse somehow doesn't understand it + (e.g. the call is dispatched to global function pointers). --pulse-model-malloc-pattern string - Regex of methods that should be modelled as mallocs in Pulse + Regex of methods that should be modelled as wrappers to malloc(3) + in Pulse. The size to allocate should be the first argument of the + function. See --pulse-model-free-pattern for more information. + + --pulse-model-realloc-pattern string + Regex of methods that should be modelled as wrappers to realloc(3) + in Pulse. The pointer to be reallocated should be the first + argument of the function and the new size the second argument. See + --pulse-model-free-pattern for more information. --pulse-model-release-pattern string Regex of methods that should be modelled as release in Pulse diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 6e48c3cc0..1991d24c6 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -1007,13 +1007,25 @@ OPTIONS See also infer-analyze(1). --pulse-model-free-pattern string - Regex of methods that should be modelled as free in Pulse + Regex of methods that should be modelled as wrappers to free(3) in + Pulse. The pointer to be freed should be the first argument of the + function. This should only be needed if the code of the wrapper is + not visible to infer or if Pulse somehow doesn't understand it + (e.g. the call is dispatched to global function pointers). See also infer-analyze(1). --pulse-model-malloc-pattern string - Regex of methods that should be modelled as mallocs in Pulse + Regex of methods that should be modelled as wrappers to malloc(3) + in Pulse. The size to allocate should be the first argument of the + function. See --pulse-model-free-pattern for more information. See also infer-analyze(1). + --pulse-model-realloc-pattern string + Regex of methods that should be modelled as wrappers to realloc(3) + in Pulse. The pointer to be reallocated should be the first + argument of the function and the new size the second argument. See + --pulse-model-free-pattern for more information. See also infer-analyze(1). + --pulse-model-release-pattern string Regex of methods that should be modelled as release in Pulse See also infer-analyze(1). @@ -1952,6 +1964,9 @@ INTERNAL OPTIONS --pulse-model-malloc-pattern-reset Cancel the effect of --pulse-model-malloc-pattern. + --pulse-model-realloc-pattern-reset + Cancel the effect of --pulse-model-realloc-pattern. + --pulse-model-release-pattern-reset Cancel the effect of --pulse-model-release-pattern. diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index 33949c53f..f34624f94 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -1007,13 +1007,25 @@ OPTIONS See also infer-analyze(1). --pulse-model-free-pattern string - Regex of methods that should be modelled as free in Pulse + Regex of methods that should be modelled as wrappers to free(3) in + Pulse. The pointer to be freed should be the first argument of the + function. This should only be needed if the code of the wrapper is + not visible to infer or if Pulse somehow doesn't understand it + (e.g. the call is dispatched to global function pointers). See also infer-analyze(1). --pulse-model-malloc-pattern string - Regex of methods that should be modelled as mallocs in Pulse + Regex of methods that should be modelled as wrappers to malloc(3) + in Pulse. The size to allocate should be the first argument of the + function. See --pulse-model-free-pattern for more information. See also infer-analyze(1). + --pulse-model-realloc-pattern string + Regex of methods that should be modelled as wrappers to realloc(3) + in Pulse. The pointer to be reallocated should be the first + argument of the function and the new size the second argument. See + --pulse-model-free-pattern for more information. See also infer-analyze(1). + --pulse-model-release-pattern string Regex of methods that should be modelled as release in Pulse See also infer-analyze(1). diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index c6e220cd4..382d21323 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -2012,22 +2012,35 @@ and pulse_model_abort = "Methods that should be modelled as abort in Pulse" -and pulse_model_malloc_pattern = - CLOpt.mk_string_opt ~long:"pulse-model-malloc-pattern" +and pulse_model_alloc_pattern = + CLOpt.mk_string_opt ~long:"pulse-model-alloc-pattern" ~in_help:InferCommand.[(Analyze, manual_generic)] - "Regex of methods that should be modelled as mallocs in Pulse" + "Regex of methods that should be modelled as allocs in Pulse" and pulse_model_free_pattern = CLOpt.mk_string_opt ~long:"pulse-model-free-pattern" ~in_help:InferCommand.[(Analyze, manual_generic)] - "Regex of methods that should be modelled as free in Pulse" + "Regex of methods that should be modelled as wrappers to $(i,free)(3) in Pulse. The pointer to \ + be freed should be the first argument of the function. This should only be needed if the code \ + of the wrapper is not visible to infer or if Pulse somehow doesn't understand it (e.g. the \ + call is dispatched to global function pointers)." -and pulse_model_alloc_pattern = - CLOpt.mk_string_opt ~long:"pulse-model-alloc-pattern" +and pulse_model_malloc_pattern = + CLOpt.mk_string_opt ~long:"pulse-model-malloc-pattern" ~in_help:InferCommand.[(Analyze, manual_generic)] - "Regex of methods that should be modelled as allocs in Pulse" + "Regex of methods that should be modelled as wrappers to $(i,malloc)(3) in Pulse. The size to \ + allocate should be the first argument of the function. See $(b,--pulse-model-free-pattern) \ + for more information." + + +and pulse_model_realloc_pattern = + CLOpt.mk_string_opt ~long:"pulse-model-realloc-pattern" + ~in_help:InferCommand.[(Analyze, manual_generic)] + "Regex of methods that should be modelled as wrappers to $(i,realloc)(3) in Pulse. The pointer \ + to be reallocated should be the first argument of the function and the new size the second \ + argument. See $(b,--pulse-model-free-pattern) for more information." and pulse_model_release_pattern = @@ -3287,11 +3300,13 @@ and pulse_max_disjuncts = !pulse_max_disjuncts and pulse_model_abort = RevList.to_list !pulse_model_abort +and pulse_model_alloc_pattern = Option.map ~f:Str.regexp !pulse_model_alloc_pattern + and pulse_model_free_pattern = Option.map ~f:Str.regexp !pulse_model_free_pattern and pulse_model_malloc_pattern = Option.map ~f:Str.regexp !pulse_model_malloc_pattern -and pulse_model_alloc_pattern = Option.map ~f:Str.regexp !pulse_model_alloc_pattern +and pulse_model_realloc_pattern = Option.map ~f:Str.regexp !pulse_model_realloc_pattern and pulse_model_release_pattern = Option.map ~f:Str.regexp !pulse_model_release_pattern diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 4828c7360..3e9f9858e 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -502,6 +502,8 @@ val pulse_model_free_pattern : Str.regexp option val pulse_model_malloc_pattern : Str.regexp option +val pulse_model_realloc_pattern : Str.regexp option + val pulse_model_release_pattern : Str.regexp option val pulse_model_return_first_arg : Str.regexp option diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 095574303..0c4ce3556 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -1412,8 +1412,12 @@ module ProcNameDispatcher = struct make_dispatcher ( transfer_ownership_matchers @ abort_matchers @ [ +BuiltinDecl.(match_builtin free) <>$ capt_arg_payload $--> C.free + ; +match_regexp_opt Config.pulse_model_free_pattern <>$ capt_arg_payload $+...$--> C.free ; +BuiltinDecl.(match_builtin malloc) <>$ capt_exp $--> C.malloc + ; +match_regexp_opt Config.pulse_model_malloc_pattern <>$ capt_exp $+...$--> C.malloc ; -"realloc" <>$ capt_arg_payload $+ capt_exp $--> C.realloc + ; +match_regexp_opt Config.pulse_model_realloc_pattern + <>$ capt_arg_payload $+ capt_exp $+...$--> C.realloc ; +BuiltinDecl.(match_builtin __delete) <>$ capt_arg_payload $--> Cplusplus.delete ; +BuiltinDecl.(match_builtin __new) <>$ capt_exp @@ -1814,8 +1818,6 @@ module ProcNameDispatcher = struct <>$ capt_arg_payload $+...$--> Misc.id_first_arg ~desc:"modelled as returning the first argument due to configuration option" - ; +match_regexp_opt Config.pulse_model_malloc_pattern <>$ capt_exp $+...$--> C.malloc - ; +match_regexp_opt Config.pulse_model_free_pattern <>$ capt_arg_payload $--> C.free ; +match_regexp_opt Config.pulse_model_skip_pattern &::.*++> Misc.skip "modelled as skip due to configuration option" ] ) end diff --git a/infer/tests/codetoanalyze/c/pulse/.inferconfig b/infer/tests/codetoanalyze/c/pulse/.inferconfig new file mode 100644 index 000000000..35ca4a4fa --- /dev/null +++ b/infer/tests/codetoanalyze/c/pulse/.inferconfig @@ -0,0 +1,5 @@ +{ + "pulse-model-free-pattern": "^my_free$", + "pulse-model-malloc-pattern": "\\(my\\|a\\)_malloc", + "pulse-model-realloc-pattern": "my_realloc" +} diff --git a/infer/tests/codetoanalyze/c/pulse/Makefile b/infer/tests/codetoanalyze/c/pulse/Makefile index ef57d9d94..cd7f985b0 100644 --- a/infer/tests/codetoanalyze/c/pulse/Makefile +++ b/infer/tests/codetoanalyze/c/pulse/Makefile @@ -7,10 +7,12 @@ TESTS_DIR = ../../.. CLANG_OPTIONS = -c INFER_OPTIONS = --pulse-only --debug-exceptions --project-root $(TESTS_DIR) \ - --pulse-report-latent-issues --pulse-model-malloc-pattern a_malloc + --pulse-report-latent-issues INFERPRINT_OPTIONS = --issues-tests SOURCES = $(wildcard *.c) include $(TESTS_DIR)/clang.make + +infer-out$(TEST_SUFFIX)/report.json: .inferconfig diff --git a/infer/tests/codetoanalyze/c/pulse/issues.exp b/infer/tests/codetoanalyze/c/pulse/issues.exp index 41b882a96..60e5faaa0 100644 --- a/infer/tests/codetoanalyze/c/pulse/issues.exp +++ b/infer/tests/codetoanalyze/c/pulse/issues.exp @@ -25,6 +25,8 @@ codetoanalyze/c/pulse/memory_leak.c, malloc_ptr_no_check_leak_bad, 2, NULLPTR_DE codetoanalyze/c/pulse/memory_leak.c, realloc_no_check_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `malloc` (modelled),is the null pointer,assigned,in call to `realloc_wrapper`,in call to `realloc` (modelled),is the null pointer,returned,return from call to `realloc_wrapper`,assigned,invalid access occurs here] codetoanalyze/c/pulse/memory_leak.c, realloc_no_free_bad, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `realloc_wrapper` here,allocated by `realloc` here,memory becomes unreachable here] codetoanalyze/c/pulse/memory_leak.c, report_leak_in_correct_line_bad, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `malloc` here,memory becomes unreachable here] +codetoanalyze/c/pulse/memory_leak.c, test_config_options_no_free_bad, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `my_realloc` here,memory becomes unreachable here] +codetoanalyze/c/pulse/memory_leak.c, user_malloc_leak_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `a_malloc` 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, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `malloc` here,memory becomes unreachable here] codetoanalyze/c/pulse/nullptr.c, bug_with_allocation_bad, 1, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `malloc` here,memory becomes unreachable here] @@ -35,7 +37,6 @@ codetoanalyze/c/pulse/nullptr.c, malloc_then_call_create_null_path_then_deref_un codetoanalyze/c/pulse/nullptr.c, null_alias_bad, 3, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `malloc` here,memory becomes unreachable here] codetoanalyze/c/pulse/nullptr.c, null_alias_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `malloc` (modelled),is the null pointer,assigned,invalid access occurs here] codetoanalyze/c/pulse/nullptr.c, nullptr_deref_young_bad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] -codetoanalyze/c/pulse/nullptr.c, user_malloc_leak_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `a_malloc` here,memory becomes unreachable here] codetoanalyze/c/pulse/traces.c, access_null_deref_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/c/pulse/traces.c, access_use_after_free_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `l` of access_use_after_free_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `l` of access_use_after_free_bad,invalid access occurs here] codetoanalyze/c/pulse/traces.c, call_makes_null_deref_manifest_bad, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [calling context starts here,in call to `something_about_strings_latent`,null pointer dereference part of the trace starts here,in call to `malloc` (modelled),is the null pointer,assigned,invalid access occurs here] diff --git a/infer/tests/codetoanalyze/c/pulse/issues.exp-isl b/infer/tests/codetoanalyze/c/pulse/issues.exp-isl index 9d5a3ef3b..1f2facd07 100644 --- a/infer/tests/codetoanalyze/c/pulse/issues.exp-isl +++ b/infer/tests/codetoanalyze/c/pulse/issues.exp-isl @@ -25,6 +25,8 @@ codetoanalyze/c/pulse/memory_leak.c, malloc_ptr_no_check_leak_bad, 2, NULLPTR_DE codetoanalyze/c/pulse/memory_leak.c, realloc_no_check_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `malloc` (modelled),is the null pointer,assigned,in call to `realloc_wrapper`,in call to `realloc` (modelled),is the null pointer,returned,return from call to `realloc_wrapper`,assigned,invalid access occurs here] codetoanalyze/c/pulse/memory_leak.c, realloc_no_free_bad, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `realloc_wrapper` here,allocated by `realloc` here,memory becomes unreachable here] codetoanalyze/c/pulse/memory_leak.c, report_leak_in_correct_line_bad, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `malloc` here,memory becomes unreachable here] +codetoanalyze/c/pulse/memory_leak.c, test_config_options_no_free_bad, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `my_realloc` here,memory becomes unreachable here] +codetoanalyze/c/pulse/memory_leak.c, user_malloc_leak_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `a_malloc` 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, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `malloc` here,memory becomes unreachable here] codetoanalyze/c/pulse/nullptr.c, bug_with_allocation_bad, 1, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `malloc` here,memory becomes unreachable here] @@ -35,7 +37,6 @@ codetoanalyze/c/pulse/nullptr.c, malloc_then_call_create_null_path_then_deref_un codetoanalyze/c/pulse/nullptr.c, null_alias_bad, 3, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `malloc` here,memory becomes unreachable here] codetoanalyze/c/pulse/nullptr.c, null_alias_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `malloc` (modelled),is the null pointer,assigned,invalid access occurs here] codetoanalyze/c/pulse/nullptr.c, nullptr_deref_young_bad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] -codetoanalyze/c/pulse/nullptr.c, user_malloc_leak_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `a_malloc` here,memory becomes unreachable here] codetoanalyze/c/pulse/traces.c, access_null_deref_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/c/pulse/traces.c, access_use_after_free_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,invalid access occurs here] codetoanalyze/c/pulse/traces.c, call_makes_null_deref_manifest_bad, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [calling context starts here,in call to `something_about_strings_latent`,null pointer dereference part of the trace starts here,in call to `malloc` (modelled),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 24698e6f5..400096870 100644 --- a/infer/tests/codetoanalyze/c/pulse/memory_leak.c +++ b/infer/tests/codetoanalyze/c/pulse/memory_leak.c @@ -121,3 +121,27 @@ void realloc_no_check_bad() { *q = 42; free(q); } + +void* my_malloc(size_t size); +void* a_malloc(size_t size); +void my_free(void* p); +void* my_realloc(void* p, size_t size); + +void user_malloc_leak_bad() { int* x = (int*)a_malloc(sizeof(int)); } + +void test_config_options_1_ok() { + int* p = (int*)malloc(sizeof(int)); + int* q = my_realloc(p, sizeof(int)); + my_free(q); +} + +void test_config_options_2_ok() { + int* p = (int*)my_malloc(sizeof(int)); + int* q = realloc(p, sizeof(int)); + my_free(q); +} + +void test_config_options_no_free_bad() { + int* p = (int*)my_malloc(sizeof(int)); + int* q = my_realloc(p, sizeof(int)); +} diff --git a/infer/tests/codetoanalyze/c/pulse/nullptr.c b/infer/tests/codetoanalyze/c/pulse/nullptr.c index 31fa749cd..ab4cd7b0d 100644 --- a/infer/tests/codetoanalyze/c/pulse/nullptr.c +++ b/infer/tests/codetoanalyze/c/pulse/nullptr.c @@ -89,8 +89,6 @@ void wrap_malloc(int** x) { } } -void user_malloc_leak_bad() { int* x = (int*)a_malloc(sizeof(int)); } - void call_no_return_good() { int* x = NULL; wrap_malloc(&x);