add flag for (undefined) functions that should be modelled as mallocs

Reviewed By: jvillard

Differential Revision: D16418471

fbshipit-source-id: f30061204

infer/man/man1/infer-analyze.txt

@@ -313,6 +313,14 @@ OPTIONS
        --uninit-only
            Activates: Enable --uninit and disable all other checkers
            (Conversely: --no-uninit-only)
+BIABDUCTION CHECKER OPTIONS
+       --biabduction-fallback-model-alloc-pattern string
+           Regex of methods that should be modelled as allocs if definition
+           is missing
+
+       --biabduction-fallback-model-free-pattern string
+           Regex of methods that should be modelled as free if definition is
+           missing
 BUCK FLAVORS OPTIONS
        --merge
            Activates: Merge the captured results directories specified in the

infer/man/man1/infer-full.txt

@@ -113,6 +113,14 @@ OPTIONS
            using the checkers framework (Conversely: --biabduction)       
     See also infer-analyze(1).
 
+       --biabduction-fallback-model-alloc-pattern string
+           Regex of methods that should be modelled as allocs if definition
+           is missing           See also infer-analyze(1).
+
+       --biabduction-fallback-model-free-pattern string
+           Regex of methods that should be modelled as free if definition is
+           missing           See also infer-analyze(1).
+
        --biabduction-only
            Activates: Enable --biabduction and disable all other checkers
            (Conversely: --no-biabduction-only)           See also infer-analyze(1).
@@ -1146,6 +1154,12 @@ INTERNAL OPTIONS
            /my/source/File.java with project root /my/root into
            ../source/File.java
 
+       --biabduction-fallback-model-alloc-pattern-reset
+           Cancel the effect of --biabduction-fallback-model-alloc-pattern.
+
+       --biabduction-fallback-model-free-pattern-reset
+           Cancel the effect of --biabduction-fallback-model-free-pattern.
+
        --bo-relational-domain-reset
            Cancel the effect of --bo-relational-domain.
 

infer/man/man1/infer.txt

@@ -113,6 +113,14 @@ OPTIONS
            using the checkers framework (Conversely: --biabduction)       
     See also infer-analyze(1).
 
+       --biabduction-fallback-model-alloc-pattern string
+           Regex of methods that should be modelled as allocs if definition
+           is missing           See also infer-analyze(1).
+
+       --biabduction-fallback-model-free-pattern string
+           Regex of methods that should be modelled as free if definition is
+           missing           See also infer-analyze(1).
+
        --biabduction-only
            Activates: Enable --biabduction and disable all other checkers
            (Conversely: --no-biabduction-only)           See also infer-analyze(1).

infer/src/base/Config.ml

@@ -189,6 +189,8 @@ let lint_dotty_dir_name = "lint_dotty"
 
 let lint_issues_dir_name = "lint_issues"
 
+let manual_biabduction = "BIABDUCTION CHECKER OPTIONS"
+
 let manual_buck_compilation_db = "BUCK COMPILATION DATABASE OPTIONS"
 
 let manual_buck_flavors = "BUCK FLAVORS OPTIONS"
@@ -838,6 +840,18 @@ and array_level =
 |}
 
 
+and biabduction_model_alloc_pattern =
+  CLOpt.mk_string_opt ~long:"biabduction-fallback-model-alloc-pattern"
+    ~in_help:InferCommand.[(Analyze, manual_biabduction)]
+    "Regex of methods that should be modelled as allocs if definition is missing"
+
+
+and biabduction_model_free_pattern =
+  CLOpt.mk_string_opt ~long:"biabduction-fallback-model-free-pattern"
+    ~in_help:InferCommand.[(Analyze, manual_biabduction)]
+    "Regex of methods that should be modelled as free if definition is missing"
+
+
 and bo_relational_domain =
   CLOpt.mk_symbol_opt ~long:"bo-relational-domain"
     ~in_help:InferCommand.[(Analyze, manual_buffer_overrun)]
@@ -2701,6 +2715,10 @@ and array_level = !array_level
 
 and biabduction = !biabduction
 
+and biabduction_model_alloc_pattern = Option.map ~f:Str.regexp !biabduction_model_alloc_pattern
+
+and biabduction_model_free_pattern = Option.map ~f:Str.regexp !biabduction_model_free_pattern
+
 and bootclasspath = !bootclasspath
 
 and bo_debug = !bo_debug

infer/src/base/Config.mli

@@ -53,6 +53,10 @@ val assign : string
 
 val backend_stats_dir_name : string
 
+val biabduction_model_alloc_pattern : Str.regexp option
+
+val biabduction_model_free_pattern : Str.regexp option
+
 val bin_dir : string
 
 val bound_error_allowed_in_procedure_call : bool

infer/src/biabduction/SymExec.ml

@@ -1426,20 +1426,37 @@ let rec sym_exec exe_env tenv current_summary instr_ (prop_ : Prop.normal Prop.t
                     | Some resolved_pdesc -> (
                         let attrs = Procdesc.get_attributes resolved_pdesc in
                         let ret_type = attrs.ProcAttributes.ret_type in
-                        let model_as_malloc =
+                        let model_as_malloc ret_type resolved_pname =
                           Objc_models.is_malloc_model ret_type resolved_pname
+                          ||
+                          match Config.biabduction_model_alloc_pattern with
+                          | Some pat ->
+                              Str.string_match pat (Typ.Procname.to_string resolved_pname) 0
+                          | None ->
+                              false
+                        in
+                        let model_as_free resolved_pname =
+                          match Config.biabduction_model_free_pattern with
+                          | Some pat ->
+                              Str.string_match pat (Typ.Procname.to_string resolved_pname) 0
+                          | None ->
+                              false
                         in
-                        match (attrs.ProcAttributes.objc_accessor, model_as_malloc) with
+                        match attrs.ProcAttributes.objc_accessor with
-                        | Some objc_accessor, _ ->
+                        | Some objc_accessor ->
                             (* If it's an ObjC getter or setter, call the builtin rather than skipping *)
                             handle_objc_instance_method_call n_actual_params n_actual_params prop
                               tenv (fst ret_id_typ) current_pdesc resolved_pname loc path
                               (sym_exec_objc_accessor resolved_pname objc_accessor ret_type)
-                        | None, true ->
+                        | None when model_as_malloc ret_type resolved_pname ->
                             (* If it's an alloc model, call alloc rather than skipping *)
                             sym_exec_alloc_model exe_env resolved_pname ret_type tenv ret_id_typ
                               current_summary loc prop path
-                        | None, false ->
+                        | None when model_as_free resolved_pname ->
+                            (* If it's an free model, call free rather than skipping *)
+                            sym_exec_free_model exe_env ret_id_typ n_actual_params tenv
+                              current_summary loc prop path
+                        | _ ->
                             let is_objc_instance_method =
                               ClangMethodKind.equal attrs.ProcAttributes.clang_method_kind
                                 ClangMethodKind.OBJC_INSTANCE
@@ -1847,6 +1864,13 @@ and sym_exec_alloc_model exe_env pname ret_typ tenv ret_id_typ summary loc prop
   instrs exe_env tenv summary (Instrs.singleton alloc_instr) [(prop, path)]
 
 
+and sym_exec_free_model exe_env ret_id_typ args tenv summary loc prop path : Builtin.ret_typ =
+  let free_fun = Exp.Const (Const.Cfun BuiltinDecl.free) in
+  let free_instr = Sil.Call (ret_id_typ, free_fun, args, loc, CallFlags.default) in
+  L.d_strln "No spec found, method is modelled as free, executing free... " ;
+  instrs exe_env tenv summary (Instrs.singleton free_instr) [(prop, path)]
+
+
 (** Perform symbolic execution for a function call *)
 and proc_call ?dynamic_dispatch exe_env callee_summary
     {Builtin.summary; tenv; prop_= pre; path; ret_id_typ; args= actual_pars; loc} =

infer/tests/codetoanalyze/objc/errors/Makefile

@@ -9,7 +9,8 @@ CLANG_OPTIONS = -c $(OBJC_CLANG_OPTIONS)
 
 CLEAN_EXTRA = infer-out-arc infer-out-all infer-out-all infer-out-arc \
               issues.exp.test.all issues.exp.test.arc issues.exp.test.default
-INFER_OPTIONS = --biabduction-only --dump-duplicate-symbols --debug-exceptions --project-root $(TESTS_DIR)
+INFER_OPTIONS = --biabduction-only --dump-duplicate-symbols --debug-exceptions --project-root $(TESTS_DIR) \
+		--biabduction-fallback-model-alloc-pattern AB[IF].*Create.* --biabduction-fallback-model-free-pattern ABFRelease
 INFERPRINT_OPTIONS = --issues-tests
 
 SOURCES_DEFAULT = \
@@ -21,6 +22,7 @@ SOURCES_DEFAULT = \
   memory_leaks_benchmark/CoreVideoExample.m \
   memory_leaks_benchmark/RetainCycleLength3.m \
   memory_leaks_benchmark/ReleasedInBlock.m \
+  memory_leaks_benchmark/BAPatLeak.m \
   npe/dynamic_dispatch.m \
   npe/Fraction.m \
   npe/NPD_core_foundation.m \

infer/tests/codetoanalyze/objc/errors/issues.exp

@@ -72,6 +72,7 @@ codetoanalyze/objc/errors/subtyping/KindOfClassExample.m, shouldThrowDivideByZer
 codetoanalyze/objc/errors/subtyping/KindOfClassExample.m, shouldThrowDivideByZero2, 2, DIVIDE_BY_ZERO, no_bucket, ERROR, [start of procedure shouldThrowDivideByZero2(),start of procedure init,return from a call to Base::init,start of procedure returnsZero2(),Taking false branch,return from a call to returnsZero2]
 codetoanalyze/objc/errors/subtyping/KindOfClassExample.m, shouldThrowDivideByZero3, 3, DIVIDE_BY_ZERO, no_bucket, ERROR, [start of procedure shouldThrowDivideByZero3(),start of procedure init,return from a call to Derived::init,Taking true branch]
 codetoanalyze/objc/errors/variadic_methods/premature_nil_termination.m, PrematureNilTermA::nilInArrayWithObjects, 5, PREMATURE_NIL_TERMINATION_ARGUMENT, B1, ERROR, [start of procedure nilInArrayWithObjects]
+codetoanalyze/objc/errors/memory_leaks_benchmark/BAPatLeak.m, A::someMethod_bad, 1, MEMORY_LEAK, no_bucket, ERROR, [start of procedure someMethod_bad]
 codetoanalyze/objc/errors/memory_leaks_benchmark/CoreVideoExample.m, CoreVideoExample::cvpixelbuffer_not_released_leak, 1, MEMORY_LEAK, no_bucket, ERROR, [start of procedure cvpixelbuffer_not_released_leak]
 codetoanalyze/objc/errors/memory_leaks_benchmark/NSData_models_tests.m, NSData_models_tests::macForIV:, 2, MEMORY_LEAK, no_bucket, ERROR, [start of procedure macForIV:]
 codetoanalyze/objc/errors/memory_leaks_benchmark/NSString_models_tests.m, StringInitA::hexStringValue, 11, MEMORY_LEAK, no_bucket, ERROR, [start of procedure hexStringValue,Skipping CFStringCreateWithBytesNoCopy(): method has no implementation,Taking false branch]

infer/tests/codetoanalyze/objc/errors/memory_leaks_benchmark/BAPatLeak.m

@@ -0,0 +1,33 @@
+/*
+ * 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;
+
+// if impl is there --biabduction-fallback-model-alloc-pattern wont catch it
+ABFDataRef* ABFDataCreate(size_t size);
+void ABRelease(ABFDataRef*);
+
+@interface A : NSObject
+@end
+
+@implementation A
+
+- (void)someMethod_bad {
+  ABFDataRef* someData = ABFDataCreate(4);
+  // this allocates a new ABFData structure
+}
+
+- (void)someMethod_ok {
+  ABFDataRef* someData = ABFDataCreate(4);
+  // this allocates a new ABFData structure
+  ABFRelease(someData);
+}
+
+@end