[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

@@ -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
+       --pulse-model-release-pattern string
-           Regex of methods that should be modelled as free in Pulse
+           Regex of methods that should be modelled as release in Pulse
 
        --pulse-only
            Activates: Enable --pulse and disable all other checkers

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
+       --pulse-model-release-pattern string
-           Regex of methods that should be modelled as free in Pulse       
+           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
+       --pulse-model-release-pattern-reset
-           Cancel the effect of --pulse-model-free-pattern.
+           Cancel the effect of --pulse-model-release-pattern.
 
        --pulse-recency-limit int
            Maximum number of array elements and structure fields to keep

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
+       --pulse-model-release-pattern string
-           Regex of methods that should be modelled as free in Pulse       
+           Regex of methods that should be modelled as release in Pulse       
     See also infer-analyze(1).
 
        --pulse-only

infer/src/absint/PatternMatch.ml

@@ -483,8 +483,8 @@ module ObjectiveC = struct
         false
 
 
-  let is_modelled_as_free _ procname =
+  let is_modelled_as_release _ procname =
-    match Config.pulse_model_free_pattern with
+    match Config.pulse_model_release_pattern with
     | Some regex ->
         Str.string_match regex procname 0
     | None ->

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

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 =
+and pulse_model_release_pattern =
-  CLOpt.mk_string_opt ~long:"pulse-model-free-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
 

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
 

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

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 <UIKit/UIKit.h>
+
+static CFStringRef use_after_cfrelease_ok(CFStringRef message) {
+  CFRetain(message);
+  CFStringRef lastMessage = message;
+  CFRelease(lastMessage);
+  lastMessage = message;
+  CFRelease(lastMessage);
+  lastMessage = message;
+
+  return lastMessage;
+}

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)

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

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]