From d8d2f2b23d9001a5cc4c471ec26e9de4b6a69e4d Mon Sep 17 00:00:00 2001 From: Loc Le Date: Thu, 20 May 2021 09:08:27 -0700 Subject: [PATCH] [pulse] added user-defined models for malloc/free Reviewed By: jvillard Differential Revision: D28549360 fbshipit-source-id: c5e6466cf --- infer/man/man1/infer-analyze.txt | 6 ++++++ infer/man/man1/infer-full.txt | 14 ++++++++++++++ infer/man/man1/infer.txt | 8 ++++++++ infer/src/base/Config.ml | 16 ++++++++++++++++ infer/src/base/Config.mli | 4 ++++ infer/src/pulse/PulseModels.ml | 2 ++ infer/tests/codetoanalyze/c/pulse/Makefile | 2 +- infer/tests/codetoanalyze/c/pulse/issues.exp | 1 + infer/tests/codetoanalyze/c/pulse/issues.exp-isl | 1 + infer/tests/codetoanalyze/c/pulse/nullptr.c | 2 ++ 10 files changed, 55 insertions(+), 1 deletion(-) diff --git a/infer/man/man1/infer-analyze.txt b/infer/man/man1/infer-analyze.txt index ae94c8cd8..e41abc0ae 100644 --- a/infer/man/man1/infer-analyze.txt +++ b/infer/man/man1/infer-analyze.txt @@ -286,6 +286,12 @@ OPTIONS --pulse-model-alloc-pattern string 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 + + --pulse-model-malloc-pattern string + Regex of methods that should be modelled as mallocs in Pulse + --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 11935bd6c..26e7b9c63 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -1005,6 +1005,14 @@ OPTIONS Regex of methods that should be modelled as allocs in Pulse See also infer-analyze(1). + --pulse-model-free-pattern string + Regex of methods that should be modelled as free in Pulse + See also infer-analyze(1). + + --pulse-model-malloc-pattern string + Regex of methods that should be modelled as mallocs in Pulse + 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). @@ -1937,6 +1945,12 @@ INTERNAL OPTIONS --pulse-model-alloc-pattern-reset Cancel the effect of --pulse-model-alloc-pattern. + --pulse-model-free-pattern-reset + Cancel the effect of --pulse-model-free-pattern. + + --pulse-model-malloc-pattern-reset + Cancel the effect of --pulse-model-malloc-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 bca6fa8f3..c1768b12c 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -1005,6 +1005,14 @@ OPTIONS Regex of methods that should be modelled as allocs in Pulse See also infer-analyze(1). + --pulse-model-free-pattern string + Regex of methods that should be modelled as free in Pulse + See also infer-analyze(1). + + --pulse-model-malloc-pattern string + Regex of methods that should be modelled as mallocs in Pulse + 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 edb59e0d1..851f3e780 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -2012,6 +2012,18 @@ 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" + ~in_help:InferCommand.[(Analyze, manual_generic)] + "Regex of methods that should be modelled as mallocs 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" + + and pulse_model_alloc_pattern = CLOpt.mk_string_opt ~long:"pulse-model-alloc-pattern" ~in_help:InferCommand.[(Analyze, manual_generic)] @@ -3268,6 +3280,10 @@ and pulse_max_disjuncts = !pulse_max_disjuncts and pulse_model_abort = RevList.to_list !pulse_model_abort +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_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 846397e3e..a53fe398e 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -498,6 +498,10 @@ val pulse_model_abort : string list val pulse_model_alloc_pattern : Str.regexp option +val pulse_model_free_pattern : Str.regexp option + +val pulse_model_malloc_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 4311c998c..b7cb27f2d 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -1799,6 +1799,8 @@ 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/Makefile b/infer/tests/codetoanalyze/c/pulse/Makefile index 886bd5364..ef57d9d94 100644 --- a/infer/tests/codetoanalyze/c/pulse/Makefile +++ b/infer/tests/codetoanalyze/c/pulse/Makefile @@ -7,7 +7,7 @@ TESTS_DIR = ../../.. CLANG_OPTIONS = -c INFER_OPTIONS = --pulse-only --debug-exceptions --project-root $(TESTS_DIR) \ - --pulse-report-latent-issues + --pulse-report-latent-issues --pulse-model-malloc-pattern a_malloc INFERPRINT_OPTIONS = --issues-tests diff --git a/infer/tests/codetoanalyze/c/pulse/issues.exp b/infer/tests/codetoanalyze/c/pulse/issues.exp index c13dd4d45..ef4ac5f37 100644 --- a/infer/tests/codetoanalyze/c/pulse/issues.exp +++ b/infer/tests/codetoanalyze/c/pulse/issues.exp @@ -31,6 +31,7 @@ codetoanalyze/c/pulse/nullptr.c, malloc_then_call_create_null_path_then_deref_un 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, null_alias_bad, 4, 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, 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 d384f5ce3..1590d7843 100644 --- a/infer/tests/codetoanalyze/c/pulse/issues.exp-isl +++ b/infer/tests/codetoanalyze/c/pulse/issues.exp-isl @@ -30,6 +30,7 @@ codetoanalyze/c/pulse/nullptr.c, malloc_then_call_create_null_path_then_deref_un 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, null_alias_bad, 4, 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, 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/nullptr.c b/infer/tests/codetoanalyze/c/pulse/nullptr.c index ab4cd7b0d..31fa749cd 100644 --- a/infer/tests/codetoanalyze/c/pulse/nullptr.c +++ b/infer/tests/codetoanalyze/c/pulse/nullptr.c @@ -89,6 +89,8 @@ 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);