From 40143ab01cc52580dabb9d954be816e153ca34ae Mon Sep 17 00:00:00 2001 From: Dulma Churchill Date: Mon, 11 May 2020 02:50:37 -0700 Subject: [PATCH] [pulse] Model CFRelease as removing the Allocated attribute rather than as free Summary: Because in the real semantics CFRelease can be used more than once, and also the variables can be used after CFRelease in general, modelling this as `free` causes many `USE_AFTER_FREE` errors. Now we change the model to not add the `Invalid CFree` attribute, but to just remove the `Allocated` attribute. So we can model memory leaks in the simple case of `Create` and not `CFRelease` before going out of scope, but we avoid the `USE_AFTER_FREE`. Since the model for CFRelease now diverges from free, changed the command line option for modelling to `pulse-model-release-pattern`. Reviewed By: jvillard Differential Revision: D21324895 fbshipit-source-id: ab323d981 --- infer/man/man1/infer-analyze.txt | 4 ++-- infer/man/man1/infer-full.txt | 8 ++++---- infer/man/man1/infer.txt | 4 ++-- infer/src/absint/PatternMatch.ml | 4 ++-- infer/src/absint/PatternMatch.mli | 2 +- infer/src/base/Config.ml | 8 ++++---- infer/src/base/Config.mli | 2 +- infer/src/pulse/PulseModels.ml | 16 +++++++++------- .../objc/pulse/CFRetainReleaseExample.m | 18 ++++++++++++++++++ infer/tests/codetoanalyze/objc/pulse/Makefile | 2 +- .../codetoanalyze/objc/pulse/MemoryLeaks.m | 9 ++++++++- .../tests/codetoanalyze/objc/pulse/issues.exp | 3 ++- 12 files changed, 54 insertions(+), 26 deletions(-) create mode 100644 infer/tests/codetoanalyze/objc/pulse/CFRetainReleaseExample.m diff --git a/infer/man/man1/infer-analyze.txt b/infer/man/man1/infer-analyze.txt index 86e6b8036..459acc30e 100644 --- a/infer/man/man1/infer-analyze.txt +++ b/infer/man/man1/infer-analyze.txt @@ -240,8 +240,8 @@ 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-release-pattern string + Regex of methods that should be modelled as release in Pulse --pulse-only Activates: Enable --pulse and disable all other checkers diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index d06639173..41246abbc 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -866,8 +866,8 @@ 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 + --pulse-model-release-pattern string + Regex of methods that should be modelled as release in Pulse See also infer-analyze(1). --pulse-only @@ -1618,8 +1618,8 @@ 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-release-pattern-reset + Cancel the effect of --pulse-model-release-pattern. --pulse-recency-limit int Maximum number of array elements and structure fields to keep diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index 99f9bffa8..7b563052f 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -866,8 +866,8 @@ 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 + --pulse-model-release-pattern string + Regex of methods that should be modelled as release in Pulse See also infer-analyze(1). --pulse-only diff --git a/infer/src/absint/PatternMatch.ml b/infer/src/absint/PatternMatch.ml index 8eab6157d..0c7d794f1 100644 --- a/infer/src/absint/PatternMatch.ml +++ b/infer/src/absint/PatternMatch.ml @@ -483,8 +483,8 @@ module ObjectiveC = struct false - let is_modelled_as_free _ procname = - match Config.pulse_model_free_pattern with + let is_modelled_as_release _ procname = + match Config.pulse_model_release_pattern with | Some regex -> Str.string_match regex procname 0 | None -> diff --git a/infer/src/absint/PatternMatch.mli b/infer/src/absint/PatternMatch.mli index c52e45d2c..124149b70 100644 --- a/infer/src/absint/PatternMatch.mli +++ b/infer/src/absint/PatternMatch.mli @@ -170,5 +170,5 @@ module ObjectiveC : sig val is_modelled_as_alloc : Tenv.t -> string -> bool - val is_modelled_as_free : Tenv.t -> string -> bool + val is_modelled_as_release : Tenv.t -> string -> bool end diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 1d287445d..f6898032f 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -1789,10 +1789,10 @@ and pulse_model_alloc_pattern = "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" +and pulse_model_release_pattern = + CLOpt.mk_string_opt ~long:"pulse-model-release-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 release in Pulse" and pulse_widen_threshold = @@ -2875,7 +2875,7 @@ and pulse_max_disjuncts = !pulse_max_disjuncts 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_release_pattern = Option.map ~f:Str.regexp !pulse_model_release_pattern and pulse_widen_threshold = !pulse_widen_threshold diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index e8f09d945..7037ed003 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -455,7 +455,7 @@ val pulse_max_disjuncts : int val pulse_model_alloc_pattern : Str.regexp option -val pulse_model_free_pattern : Str.regexp option +val pulse_model_release_pattern : Str.regexp option val pulse_widen_threshold : int diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index b597c6888..87688a272 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -665,14 +665,16 @@ module ProcNameDispatcher = struct ) ; +PatternMatch.ObjectiveC.is_core_graphics_create_or_copy &++> C.malloc ; +PatternMatch.ObjectiveC.is_core_foundation_create_or_copy &++> C.malloc - ; +PatternMatch.ObjectiveC.is_core_graphics_release <>$ capt_arg_payload $--> C.free - ; -"CFRelease" <>$ capt_arg_payload $--> C.free - ; -"CFAutorelease" <>$ capt_arg_payload $--> C.free - ; -"CFBridgingRelease" <>$ capt_arg_payload $--> C.cf_bridging_release - ; +match_builtin BuiltinDecl.__free_cf <>$ capt_arg_payload $--> C.cf_bridging_release - ; +PatternMatch.ObjectiveC.is_modelled_as_alloc &++> C.malloc_not_null ; +match_builtin BuiltinDecl.malloc_no_fail <>$ capt_arg_payload $--> C.malloc_not_null - ; +PatternMatch.ObjectiveC.is_modelled_as_free <>$ capt_arg_payload $--> C.free ] + ; +PatternMatch.ObjectiveC.is_modelled_as_alloc &++> C.malloc_not_null + ; +PatternMatch.ObjectiveC.is_core_graphics_release + <>$ capt_arg_payload $--> C.cf_bridging_release + ; -"CFRelease" <>$ capt_arg_payload $--> C.cf_bridging_release + ; +PatternMatch.ObjectiveC.is_modelled_as_release + <>$ capt_arg_payload $--> C.cf_bridging_release + ; -"CFAutorelease" <>$ capt_arg_payload $--> C.cf_bridging_release + ; -"CFBridgingRelease" <>$ capt_arg_payload $--> C.cf_bridging_release + ; +match_builtin BuiltinDecl.__free_cf <>$ capt_arg_payload $--> C.cf_bridging_release ] end let dispatch tenv proc_name args = ProcNameDispatcher.dispatch tenv proc_name args diff --git a/infer/tests/codetoanalyze/objc/pulse/CFRetainReleaseExample.m b/infer/tests/codetoanalyze/objc/pulse/CFRetainReleaseExample.m new file mode 100644 index 000000000..e065c91e0 --- /dev/null +++ b/infer/tests/codetoanalyze/objc/pulse/CFRetainReleaseExample.m @@ -0,0 +1,18 @@ +/* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ +#import + +static CFStringRef use_after_cfrelease_ok(CFStringRef message) { + CFRetain(message); + CFStringRef lastMessage = message; + CFRelease(lastMessage); + lastMessage = message; + CFRelease(lastMessage); + lastMessage = message; + + return lastMessage; +} diff --git a/infer/tests/codetoanalyze/objc/pulse/Makefile b/infer/tests/codetoanalyze/objc/pulse/Makefile index f76937b71..61da3acb8 100644 --- a/infer/tests/codetoanalyze/objc/pulse/Makefile +++ b/infer/tests/codetoanalyze/objc/pulse/Makefile @@ -8,7 +8,7 @@ TESTS_DIR = ../../.. CLANG_OPTIONS = -c $(OBJC_CLANG_OPTIONS) -fobjc-arc INFER_OPTIONS = --pulse-only --debug-exceptions --project-root $(TESTS_DIR) \ --pulse-model-alloc-pattern "AB[IF].*Create.*" \ ---pulse-model-free-pattern ABFRelease +--pulse-model-release-pattern ABFRelease INFERPRINT_OPTIONS = --issues-tests SOURCES = $(wildcard *.m) diff --git a/infer/tests/codetoanalyze/objc/pulse/MemoryLeaks.m b/infer/tests/codetoanalyze/objc/pulse/MemoryLeaks.m index 563986192..cac233446 100644 --- a/infer/tests/codetoanalyze/objc/pulse/MemoryLeaks.m +++ b/infer/tests/codetoanalyze/objc/pulse/MemoryLeaks.m @@ -91,9 +91,16 @@ NSLocale* wrap_bridge(CFLocaleRef x) { CFBridgingRelease(x); } -NSLocale* call_bridge_interproc_leak_bad_FP() { +NSLocale* call_bridge_interproc_leak_ok_FP() { CFLocaleRef nameRef = CFLocaleCreate(NULL, NULL); NSLocale* locale = wrap_bridge(nameRef); } +void wrap_cfrelease(CFLocaleRef x) { CFRelease(x); } + +void call_cfrelease_interproc_leak_ok_FP() { + CFLocaleRef nameRef = CFLocaleCreate(NULL, NULL); + wrap_cfrelease(nameRef); +} + @end diff --git a/infer/tests/codetoanalyze/objc/pulse/issues.exp b/infer/tests/codetoanalyze/objc/pulse/issues.exp index d9023b48a..e7f29b7da 100644 --- a/infer/tests/codetoanalyze/objc/pulse/issues.exp +++ b/infer/tests/codetoanalyze/objc/pulse/issues.exp @@ -4,6 +4,7 @@ codetoanalyze/objc/pulse/MemoryLeaks.m, MemoryLeaks::call_no_bridge_leak_bad, 1, codetoanalyze/objc/pulse/MemoryLeaks.m, MemoryLeaks::cg_path_create_mutable_leak_bad:, 2, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `CGPathCreateMutable` (modelled),allocation part of the trace ends here,memory becomes unreachable here] codetoanalyze/objc/pulse/MemoryLeaks.m, MemoryLeaks::cg_path_create_with_rect_leak_bad, 3, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `CGPathCreateWithRect` (modelled),allocation part of the trace ends here,memory becomes unreachable here] codetoanalyze/objc/pulse/MemoryLeaks.m, MemoryLeaks::no_bridge_leak_bad, 1, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `CFLocaleCreate` (modelled),allocation part of the trace ends here,memory becomes unreachable here] -codetoanalyze/objc/pulse/MemoryLeaks.m, call_bridge_interproc_leak_bad_FP, 2, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `CFLocaleCreate` (modelled),allocation part of the trace ends here,memory becomes unreachable here] +codetoanalyze/objc/pulse/MemoryLeaks.m, call_bridge_interproc_leak_ok_FP, 2, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `CFLocaleCreate` (modelled),allocation part of the trace ends here,memory becomes unreachable here] +codetoanalyze/objc/pulse/MemoryLeaks.m, call_cfrelease_interproc_leak_ok_FP, 2, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `CFLocaleCreate` (modelled),allocation part of the trace ends here,memory becomes unreachable here] codetoanalyze/objc/pulse/use_after_free.m, PulseTest::use_after_free_simple_in_objc_method_bad:, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of PulseTest::use_after_free_simple_in_objc_method_bad:,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of PulseTest::use_after_free_simple_in_objc_method_bad:,invalid access occurs here] codetoanalyze/objc/pulse/use_after_free.m, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of use_after_free_simple_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of use_after_free_simple_bad,invalid access occurs here]