[pulse] Add options for modelling alloc models and free models from user-defined regexes.

Reviewed By: jvillard

Differential Revision: D21039304

fbshipit-source-id: a43b17235

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)

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
 

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).

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

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

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

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

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

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 <Foundation/NSObject.h>
+#include <stdlib.h>
+
+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

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)

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]