diff --git a/Makefile b/Makefile index 837f1381d..c8205e325 100644 --- a/Makefile +++ b/Makefile @@ -52,6 +52,7 @@ DIRECT_TESTS += \ c_errors \ c_frontend \ c_performance \ + c_purity \ c_uninit \ cpp_bufferoverrun \ cpp_conflicts \ diff --git a/infer/src/checkers/invariantModels.ml b/infer/src/checkers/invariantModels.ml index 46fbd3a83..24f854965 100644 --- a/infer/src/checkers/invariantModels.ml +++ b/infer/src/checkers/invariantModels.ml @@ -39,6 +39,7 @@ module ProcName = struct let open ProcnameDispatcher.ProcName in make_dispatcher [ +invariant_builtins <>--> VariantForHoisting + ; -"__variable_initialization" <>--> Invariant ; +(fun _ name -> BuiltinDecl.is_declared (Typ.Procname.from_string_c_fun name)) <>--> Variant ; +PatternMatch.implements_android "text.TextUtils" &:: "isEmpty" <>--> VariantForHoisting diff --git a/infer/src/checkers/purity.ml b/infer/src/checkers/purity.ml index 59046cfc2..c59fbb412 100644 --- a/infer/src/checkers/purity.ml +++ b/infer/src/checkers/purity.ml @@ -36,7 +36,7 @@ module TransferFunctions = struct let get_alias_set inferbo_mem var = let default = ModifiedVarSet.empty in let alias_v = BufferOverrunDomain.Mem.find (AbsLoc.Loc.of_var var) inferbo_mem in - let pow_locs = BufferOverrunDomain.Val.get_pow_loc alias_v in + let pow_locs = BufferOverrunDomain.Val.get_all_locs alias_v in AbsLoc.PowLoc.fold (fun loc modified_acc -> AbsLoc.Loc.get_path loc @@ -145,6 +145,8 @@ module TransferFunctions = struct else find_params_matching_modified_args inferbo_mem formals args callee_modified_params) + let modified_global ae = HilExp.AccessExpression.get_base ae |> fst |> Var.is_global + let exec_instr (astate : Domain.t) {tenv; ProcData.extras= {inferbo_invariant_map; formals; get_callee_summary}} (node : CFG.Node.t) (instr : HilInstr.t) = @@ -155,7 +157,8 @@ module TransferFunctions = struct Option.value_exn (BufferOverrunAnalysis.extract_post node_id inferbo_invariant_map) in match instr with - | Assign (ae, _, _) when is_heap_access ae -> + | Assign (ae, _, _) + when is_heap_access ae || (Language.curr_language_is Clang && modified_global ae) -> track_modified_params inferbo_mem formals ae |> Domain.join astate | Call (_, Direct called_pname, args, _, _) -> Domain.join astate @@ -187,13 +190,16 @@ end module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions) let should_report pdesc = - match Procdesc.get_proc_name pdesc with - | Typ.Procname.Java java_pname as proc_name -> - (not (Typ.Procname.is_constructor proc_name)) - && (not (Typ.Procname.Java.is_class_initializer java_pname)) - && not (Typ.Procname.Java.is_access_method java_pname) + let proc_name = Procdesc.get_proc_name pdesc in + (not (Typ.Procname.is_constructor proc_name)) + && + match proc_name with + | Typ.Procname.Java java_pname -> + not + ( Typ.Procname.Java.is_class_initializer java_pname + || Typ.Procname.Java.is_access_method java_pname ) | _ -> - L.(die InternalError "Not supposed to run on non-Java code.") + true let report_errors pdesc astate summary = diff --git a/infer/src/checkers/registerCheckers.ml b/infer/src/checkers/registerCheckers.ml index 24f98b246..0c2d79d5c 100644 --- a/infer/src/checkers/registerCheckers.ml +++ b/infer/src/checkers/registerCheckers.ml @@ -123,7 +123,8 @@ let all_checkers = ; (Cluster Starvation.reporting, Language.Clang) ] } ; { name= "purity" ; active= Config.purity || Config.loop_hoisting - ; callbacks= [(Procedure Purity.checker, Language.Java)] } + ; callbacks= + [(Procedure Purity.checker, Language.Java); (Procedure Purity.checker, Language.Clang)] } ; { name= "Class loading analysis" ; active= Config.class_loads ; callbacks= [(Procedure ClassLoads.analyze_procedure, Language.Java)] } ] diff --git a/infer/tests/codetoanalyze/c/purity/Makefile b/infer/tests/codetoanalyze/c/purity/Makefile new file mode 100644 index 000000000..84d7bd68c --- /dev/null +++ b/infer/tests/codetoanalyze/c/purity/Makefile @@ -0,0 +1,13 @@ +# Copyright (c) 2019-present, Facebook, Inc. +# +# This source code is licensed under the MIT license found in the +# LICENSE file in the root directory of this source tree. +TESTS_DIR = ../../.. + +CLANG_OPTIONS = -c +INFER_OPTIONS = -F --project-root $(TESTS_DIR) --purity-only --function-pointer-specialization +INFERPRINT_OPTIONS = --issues-tests + +SOURCES = $(wildcard *.c) + +include $(TESTS_DIR)/clang.make diff --git a/infer/tests/codetoanalyze/c/purity/array.c b/infer/tests/codetoanalyze/c/purity/array.c new file mode 100644 index 000000000..2d493b19f --- /dev/null +++ b/infer/tests/codetoanalyze/c/purity/array.c @@ -0,0 +1,39 @@ +/* + * Copyright (c) 2019-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ +#include +#include + +void swap_bad(int* array, int i, int j) { + int tmp = array[i]; + array[i] = array[j]; + array[j] = tmp; +} + +void alias_mod_bad(int array[], int i, int j) { + int* a = array; + a[j] = i; +} + +void fresh_arr_ok(int size) { + int arr[size]; + for (int i = 0; i < size - 1; i++) { + arr[i] = 0; + } +} + +void call_impure_with_local_ok(int size) { + int arr[size]; + alias_mod_bad(arr, 0, 9); +} + +void time_bad() { + time_t rawtime; + struct tm* timeinfo; + + time(&rawtime); + timeinfo = localtime(&rawtime); +} diff --git a/infer/tests/codetoanalyze/c/purity/global_test.c b/infer/tests/codetoanalyze/c/purity/global_test.c new file mode 100644 index 000000000..c70499b1d --- /dev/null +++ b/infer/tests/codetoanalyze/c/purity/global_test.c @@ -0,0 +1,29 @@ +/* + * Copyright (c) 2019-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ + +int global; + +static int s; + +void static_incr_bad() { s += 1; } + +void global_write_bad(int x, int y) { global += x + y; } + +void call_impure_bad(int size) { + for (int i = 0; i < size; i++) { + global_write_bad(i, size); + } +} + +int local_write_ok(int x, int y) { + int k = x + y; + k++; + return k; +} + +// calls foo which modifies global var +void call_set_bad() { static_incr_bad(); } diff --git a/infer/tests/codetoanalyze/c/purity/issues.exp b/infer/tests/codetoanalyze/c/purity/issues.exp new file mode 100644 index 000000000..02e24d36e --- /dev/null +++ b/infer/tests/codetoanalyze/c/purity/issues.exp @@ -0,0 +1,6 @@ +codetoanalyze/c/purity/array.c, call_impure_with_local_ok, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function call_impure_with_local_ok] +codetoanalyze/c/purity/array.c, fresh_arr_ok, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function fresh_arr_ok] +codetoanalyze/c/purity/global_test.c, local_write_ok, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function local_write_ok] +codetoanalyze/c/purity/struct.c, set_fresh_ok, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function set_fresh_ok] +codetoanalyze/c/purity/struct.c, set_fresh_primitive_ok, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function set_fresh_primitive_ok] +codetoanalyze/c/purity/struct.c, variable_init_ok, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function variable_init_ok] diff --git a/infer/tests/codetoanalyze/c/purity/struct.c b/infer/tests/codetoanalyze/c/purity/struct.c new file mode 100644 index 000000000..954f4369d --- /dev/null +++ b/infer/tests/codetoanalyze/c/purity/struct.c @@ -0,0 +1,35 @@ +/* + * Copyright (c) 2019-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ +typedef struct { + int i; +} Foo; + +static int variable_init_ok(const int* x) { + const Foo* foo = (const Foo*)x; + return foo->i; +} + +Foo* variable_init_bad(const int* x) { + Foo* foo = (const Foo*)x; // aliasing to x + foo->i = 0; + return foo; +} + +void set_fresh_ok() { + Foo* foo = {0}; + foo->i = 0; +} + +void set_fresh_primitive_ok(int x) { + Foo* foo = {x}; + foo->i = 0; +} + +void set_alias_primitive_bad(int* x) { + Foo* foo = {x}; + foo->i = 0; +}