diff --git a/infer/man/man1/infer-analyze.txt b/infer/man/man1/infer-analyze.txt index 3353e4cd6..994b88ac7 100644 --- a/infer/man/man1/infer-analyze.txt +++ b/infer/man/man1/infer-analyze.txt @@ -232,6 +232,12 @@ OPTIONS Activates: [EXPERIMENTAL] C++ lifetime analysis (Conversely: --no-pulse) + --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-only Activates: Enable --pulse and disable all other checkers (Conversely: --no-pulse-only) diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 82121a873..aeb9c22b5 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -862,6 +862,14 @@ OPTIONS Activates: [EXPERIMENTAL] C++ lifetime analysis (Conversely: --no-pulse) See also infer-analyze(1). + --pulse-model-alloc-pattern string + 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-only Activates: Enable --pulse and disable all other checkers (Conversely: --no-pulse-only) See also infer-analyze(1). @@ -1606,6 +1614,12 @@ INTERNAL OPTIONS --pulse-max-disjuncts int Under-approximate after int disjunctions in the domain + --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-widen-threshold int Under-approximate after int loop iterations diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index 5c258956c..a328dd401 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -862,6 +862,14 @@ OPTIONS Activates: [EXPERIMENTAL] C++ lifetime analysis (Conversely: --no-pulse) See also infer-analyze(1). + --pulse-model-alloc-pattern string + 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-only Activates: Enable --pulse and disable all other checkers (Conversely: --no-pulse-only) See also infer-analyze(1). diff --git a/infer/src/absint/PatternMatch.ml b/infer/src/absint/PatternMatch.ml index 266f86569..4b6045108 100644 --- a/infer/src/absint/PatternMatch.ml +++ b/infer/src/absint/PatternMatch.ml @@ -483,4 +483,20 @@ module ObjectiveC = struct let is_core_graphics_release _ procname = String.is_prefix ~prefix:"CG" procname && String.is_suffix ~suffix:"Release" procname + + + let is_modelled_as_alloc _ procname = + match Config.pulse_model_alloc_pattern with + | Some regex -> + Str.string_match regex procname 0 + | None -> + false + + + let is_modelled_as_free _ procname = + match Config.pulse_model_free_pattern with + | Some regex -> + Str.string_match regex procname 0 + | None -> + false end diff --git a/infer/src/absint/PatternMatch.mli b/infer/src/absint/PatternMatch.mli index 08018cc07..b33c604df 100644 --- a/infer/src/absint/PatternMatch.mli +++ b/infer/src/absint/PatternMatch.mli @@ -165,4 +165,8 @@ module ObjectiveC : sig val is_core_graphics_create_or_copy : Tenv.t -> string -> bool val is_core_graphics_release : Tenv.t -> string -> bool + + val is_modelled_as_alloc : Tenv.t -> string -> bool + + val is_modelled_as_free : Tenv.t -> string -> bool end diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 743e19e16..396bc7393 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -1778,6 +1778,18 @@ and pulse_max_disjuncts = "Under-approximate after $(i,int) disjunctions in the domain" +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 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" + + and pulse_widen_threshold = CLOpt.mk_int ~long:"pulse-widen-threshold" ~default:3 "Under-approximate after $(i,int) loop iterations" @@ -2850,6 +2862,10 @@ and pulse_intraprocedural_only = !pulse_intraprocedural_only 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_widen_threshold = !pulse_widen_threshold and pure_by_default = !pure_by_default diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index d2bf24c46..56a1db59d 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -451,6 +451,10 @@ val pulse_intraprocedural_only : bool val pulse_max_disjuncts : int +val pulse_model_alloc_pattern : Str.regexp option + +val pulse_model_free_pattern : Str.regexp option + val pulse_widen_threshold : int val pure_by_default : bool diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 3aa8a3d6d..ecb0db750 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -106,6 +106,20 @@ module C = struct ret_value in [astate_alloc; ExecutionDomain.ContinueProgram astate_null] + + + let malloc_not_null _ : model = + fun ~caller_summary:_ ~callee_procname location ~ret:(ret_id, _) astate -> + let ret_addr = AbstractValue.mk_fresh () in + let hist = + [ValueHistory.Allocation {f= Model (Procname.to_string callee_procname); location}] + in + let ret_value = (ret_addr, hist) in + let immediate_hist = Trace.Immediate {location; history= hist} in + let astate = PulseOperations.write_id ret_id ret_value astate in + PulseOperations.allocate callee_procname location ret_value astate + |> PulseArithmetic.and_positive immediate_hist ret_addr + |> PulseOperations.ok_continue end module Cplusplus = struct @@ -544,7 +558,9 @@ module ProcNameDispatcher = struct ; +PatternMatch.ObjectiveC.is_core_graphics_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 ] + ; -"CFAutorelease" <>$ capt_arg_payload $--> C.free + ; +PatternMatch.ObjectiveC.is_modelled_as_alloc &++> C.malloc_not_null + ; +PatternMatch.ObjectiveC.is_modelled_as_free <>$ capt_arg_payload $--> C.free ] end let dispatch tenv proc_name args = ProcNameDispatcher.dispatch tenv proc_name args diff --git a/infer/tests/codetoanalyze/objc/pulse/AllocPatternMemLeak.m b/infer/tests/codetoanalyze/objc/pulse/AllocPatternMemLeak.m new file mode 100644 index 000000000..65dadf16f --- /dev/null +++ b/infer/tests/codetoanalyze/objc/pulse/AllocPatternMemLeak.m @@ -0,0 +1,30 @@ +/* + * 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. + */ +#include +#include + +typedef struct ABFDataRef { +} ABFDataRef; + +ABFDataRef* ABFDataCreate(size_t size); +void ABFRelease(ABFDataRef*); + +@interface A : NSObject +@end + +@implementation A + +- (void)create_no_release_leak_bad { + ABFDataRef* someData = ABFDataCreate(4); +} + +- (void)create_then_release_ok { + ABFDataRef* someData = ABFDataCreate(4); + ABFRelease(someData); +} + +@end diff --git a/infer/tests/codetoanalyze/objc/pulse/Makefile b/infer/tests/codetoanalyze/objc/pulse/Makefile index ccb5174a1..ebe0588bf 100644 --- a/infer/tests/codetoanalyze/objc/pulse/Makefile +++ b/infer/tests/codetoanalyze/objc/pulse/Makefile @@ -6,7 +6,7 @@ TESTS_DIR = ../../.. CLANG_OPTIONS = -c $(OBJC_CLANG_OPTIONS) -INFER_OPTIONS = --pulse-only --debug-exceptions --project-root $(TESTS_DIR) +INFER_OPTIONS = --pulse-only --debug-exceptions --project-root $(TESTS_DIR) --pulse-model-alloc-pattern AB[IF].*Create.* --pulse-model-free-pattern ABFRelease INFERPRINT_OPTIONS = --issues-tests SOURCES = $(wildcard *.m) diff --git a/infer/tests/codetoanalyze/objc/pulse/issues.exp b/infer/tests/codetoanalyze/objc/pulse/issues.exp index fad4bd751..51e84d8db 100644 --- a/infer/tests/codetoanalyze/objc/pulse/issues.exp +++ b/infer/tests/codetoanalyze/objc/pulse/issues.exp @@ -1,3 +1,4 @@ +codetoanalyze/objc/pulse/AllocPatternMemLeak.m, A::create_no_release_leak_bad, 1, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `ABFDataCreate` (modelled),allocation part of the trace ends here,memory becomes unreachable here] 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/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]