diff --git a/infer/man/man1/infer-analyze.txt b/infer/man/man1/infer-analyze.txt index 41afce65e..a325b01c3 100644 --- a/infer/man/man1/infer-analyze.txt +++ b/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 diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index dca99428a..b1e42df89 100644 --- a/infer/man/man1/infer-full.txt +++ b/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. diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index a7957277a..1d6173c95 100644 --- a/infer/man/man1/infer.txt +++ b/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). diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index ababf8183..ac2771409 100644 --- a/infer/src/base/Config.ml +++ b/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 diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index b2446b3ce..e85bf5a82 100644 --- a/infer/src/base/Config.mli +++ b/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 diff --git a/infer/src/biabduction/SymExec.ml b/infer/src/biabduction/SymExec.ml index 204325f3b..4e40cfb3b 100644 --- a/infer/src/biabduction/SymExec.ml +++ b/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 - match (attrs.ProcAttributes.objc_accessor, model_as_malloc) with - | Some objc_accessor, _ -> + 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 with + | 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} = diff --git a/infer/tests/codetoanalyze/objc/errors/Makefile b/infer/tests/codetoanalyze/objc/errors/Makefile index ccce45f1f..f175293ab 100644 --- a/infer/tests/codetoanalyze/objc/errors/Makefile +++ b/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 \ diff --git a/infer/tests/codetoanalyze/objc/errors/issues.exp b/infer/tests/codetoanalyze/objc/errors/issues.exp index 975f84986..843f58ea3 100644 --- a/infer/tests/codetoanalyze/objc/errors/issues.exp +++ b/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] diff --git a/infer/tests/codetoanalyze/objc/errors/memory_leaks_benchmark/BAPatLeak.m b/infer/tests/codetoanalyze/objc/errors/memory_leaks_benchmark/BAPatLeak.m new file mode 100644 index 000000000..3287e3854 --- /dev/null +++ b/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 +#include + +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