diff --git a/infer/documentation/issues/MODIFIES_IMMUTABLE.md b/infer/documentation/issues/MODIFIES_IMMUTABLE.md new file mode 100644 index 000000000..c3b3779cd --- /dev/null +++ b/infer/documentation/issues/MODIFIES_IMMUTABLE.md @@ -0,0 +1,13 @@ +This issue type indicates modifications to fields marked as @Immutable. For instance, below function `mutateArray` would be marked as modifying immutable field `testArray`: +```java + @Immutable int[] testArray = new int[]{0, 1, 2, 4}; + + int[] getTestArray() { + return testArray; + } + + void mutateArray() { + int[] array = getTestArray(); + array[2] = 7; + } +``` diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 4b1945f11..eb3eaef1f 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -490,6 +490,7 @@ OPTIONS MEMORY_LEAK (enabled by default), MISSING_REQUIRED_PROP (enabled by default), MIXED_SELF_WEAKSELF (enabled by default), + MODIFIES_IMMUTABLE (enabled by default), MULTIPLE_WEAKSELF (enabled by default), MUTABLE_LOCAL_VARIABLE_IN_COMPONENT_FILE (enabled by default), Missing_fld (enabled by default), @@ -1036,6 +1037,10 @@ OPTIONS --report-formatter { none | phabricator } Which formatter to use when emitting the report See also infer-report(1). + --report-immutable-modifications + Activates: Report modifications to immutable fields (Conversely: + --no-report-immutable-modifications) See also infer-report(1) and infer-run(1). + --report-previous path Report of the base revision to use for comparison See also infer-reportdiff(1). diff --git a/infer/man/man1/infer-report.txt b/infer/man/man1/infer-report.txt index 06665928a..8aeb46757 100644 --- a/infer/man/man1/infer-report.txt +++ b/infer/man/man1/infer-report.txt @@ -198,6 +198,7 @@ OPTIONS MEMORY_LEAK (enabled by default), MISSING_REQUIRED_PROP (enabled by default), MIXED_SELF_WEAKSELF (enabled by default), + MODIFIES_IMMUTABLE (enabled by default), MULTIPLE_WEAKSELF (enabled by default), MUTABLE_LOCAL_VARIABLE_IN_COMPONENT_FILE (enabled by default), Missing_fld (enabled by default), @@ -314,6 +315,10 @@ OPTIONS --report-formatter { none | phabricator } Which formatter to use when emitting the report + --report-immutable-modifications + Activates: Report modifications to immutable fields (Conversely: + --no-report-immutable-modifications) + --report-suppress-errors +error_name do not report a type of errors diff --git a/infer/man/man1/infer-run.txt b/infer/man/man1/infer-run.txt index 68d8f4ce3..8a8c46e02 100644 --- a/infer/man/man1/infer-run.txt +++ b/infer/man/man1/infer-run.txt @@ -118,6 +118,10 @@ OPTIONS Activates: Force converting an absolute path to a relative path to the root directory (Conversely: --no-report-force-relative-path) + --report-immutable-modifications + Activates: Report modifications to immutable fields (Conversely: + --no-report-immutable-modifications) + --report-suppress-errors +error_name do not report a type of errors diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index c778b685e..1478c3ac7 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -490,6 +490,7 @@ OPTIONS MEMORY_LEAK (enabled by default), MISSING_REQUIRED_PROP (enabled by default), MIXED_SELF_WEAKSELF (enabled by default), + MODIFIES_IMMUTABLE (enabled by default), MULTIPLE_WEAKSELF (enabled by default), MUTABLE_LOCAL_VARIABLE_IN_COMPONENT_FILE (enabled by default), Missing_fld (enabled by default), @@ -1036,6 +1037,10 @@ OPTIONS --report-formatter { none | phabricator } Which formatter to use when emitting the report See also infer-report(1). + --report-immutable-modifications + Activates: Report modifications to immutable fields (Conversely: + --no-report-immutable-modifications) See also infer-report(1) and infer-run(1). + --report-previous path Report of the base revision to use for comparison See also infer-reportdiff(1). diff --git a/infer/src/absint/AbstractDomain.ml b/infer/src/absint/AbstractDomain.ml index 8527dcdb4..1af8ed3c5 100644 --- a/infer/src/absint/AbstractDomain.ml +++ b/infer/src/absint/AbstractDomain.ml @@ -738,6 +738,14 @@ struct M.fold (fun key values acc -> S.fold (fun v acc -> f key v acc) values acc) m acc + let filter f m = + M.filter_map + (fun key values -> + let res = S.filter (fun elt -> f key elt) values in + if S.is_empty res then None else Some res ) + m + + let remove k v m = M.update k (function diff --git a/infer/src/absint/AbstractDomain.mli b/infer/src/absint/AbstractDomain.mli index 261ff5bba..29a0f0fcb 100644 --- a/infer/src/absint/AbstractDomain.mli +++ b/infer/src/absint/AbstractDomain.mli @@ -252,6 +252,8 @@ include sig val remove : Key.t -> Value.t -> t -> t [@@warning "-32"] val fold : (Key.t -> Value.t -> 'a -> 'a) -> t -> 'a -> 'a + + val filter : (Key.t -> Value.t -> bool) -> t -> t end end diff --git a/infer/src/absint/annotations.ml b/infer/src/absint/annotations.ml index c773f3f8b..782aae722 100644 --- a/infer/src/absint/annotations.ml +++ b/infer/src/absint/annotations.ml @@ -43,6 +43,8 @@ let guarded_by = "GuardedBy" let ignore_allocations = "IgnoreAllocations" +let immutable = "Immutable" + let initializer_ = "Initializer" let inject = "Inject" diff --git a/infer/src/absint/annotations.mli b/infer/src/absint/annotations.mli index ad618126a..60b56016a 100644 --- a/infer/src/absint/annotations.mli +++ b/infer/src/absint/annotations.mli @@ -17,6 +17,8 @@ val expensive : string val inject_prop : string +val immutable : string + val lockless : string val no_allocation : string diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index bd5f5c8f4..0824c49c0 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -2061,6 +2061,12 @@ and report_formatter = ~eq:PolyVariantEqual.( = ) "Which formatter to use when emitting the report" +and report_immutable_modifications = + CLOpt.mk_bool ~long:"report-immutable-modifications" ~default:false + ~in_help:InferCommand.[(Report, manual_generic); (Run, manual_generic)] + "Report modifications to immutable fields" + + and report_previous = CLOpt.mk_path_opt ~long:"report-previous" ~in_help:InferCommand.[(ReportDiff, manual_generic)] @@ -3157,6 +3163,8 @@ and report_force_relative_path = !report_force_relative_path and report_formatter = !report_formatter +and report_immutable_modifications = !report_immutable_modifications + and report_path_regex_blacklist = !report_path_regex_blacklist and report_path_regex_whitelist = !report_path_regex_whitelist diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index b61397769..ede700b08 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -118,6 +118,8 @@ val report_custom_error : bool val report_force_relative_path : bool +val report_immutable_modifications : bool + val report_nullable_inconsistency : bool val save_compact_summaries : bool diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index f3cd7f9d4..20878f76f 100644 --- a/infer/src/base/IssueType.ml +++ b/infer/src/base/IssueType.ml @@ -746,6 +746,11 @@ let mixed_self_weakself = ~user_documentation:[%blob "../../documentation/issues/MIXED_SELF_WEAKSELF.md"] +let modifies_immutable = + register ~id:"MODIFIES_IMMUTABLE" Error Impurity + ~user_documentation:[%blob "../../documentation/issues/MODIFIES_IMMUTABLE.md"] + + let multiple_weakself = register ~id:"MULTIPLE_WEAKSELF" ~hum:"Multiple WeakSelf Use" Error SelfInBlock ~user_documentation:[%blob "../../documentation/issues/MULTIPLE_WEAKSELF.md"] diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli index 7fb0cd57b..2eefdcb35 100644 --- a/infer/src/base/IssueType.mli +++ b/infer/src/base/IssueType.mli @@ -260,6 +260,8 @@ val missing_required_prop : t val mixed_self_weakself : t +val modifies_immutable : t + val multiple_weakself : t val mutable_local_variable_in_component_file : t diff --git a/infer/src/checkers/impurity.ml b/infer/src/checkers/impurity.ml index 15126b836..cc0276c79 100644 --- a/infer/src/checkers/impurity.ml +++ b/infer/src/checkers/impurity.ml @@ -178,6 +178,10 @@ let extract_impurity tenv pname formals (exec_state : ExecutionDomain.t) : Impur {modified_globals; modified_params; skipped_calls; exited} +let add_modified_ltr param_source set acc = + ImpurityDomain.ModifiedVarMap.fold (ImpurityDomain.add_to_errlog ~nesting:1 param_source) set acc + + let checker {IntraproceduralAnalysis.proc_desc; tenv; err_log} (pulse_summary_opt : PulseSummary.t option) = let proc_name = Procdesc.get_proc_name proc_desc in @@ -207,27 +211,39 @@ let checker {IntraproceduralAnalysis.proc_desc; tenv; err_log} in ImpurityDomain.join acc modified ) in - if PurityChecker.should_report proc_name && not (ImpurityDomain.is_pure impurity_astate) then - let modified_ltr param_source set acc = - ImpurityDomain.ModifiedVarMap.fold - (ImpurityDomain.add_to_errlog ~nesting:1 param_source) - set acc - in - let skipped_functions = - SkippedCalls.fold - (fun proc_name trace acc -> - Trace.add_to_errlog ~nesting:1 ~include_value_history:false - ~pp_immediate:(fun fmt -> - F.fprintf fmt "call to skipped function %a occurs here" Procname.pp proc_name ) - trace acc ) - skipped_calls [] - in - let impure_fun_desc = F.asprintf "Impure function %a" Procname.pp proc_name in - let impure_fun_ltr = Errlog.make_trace_element 0 pname_loc impure_fun_desc [] in - let ltr = - impure_fun_ltr - :: modified_ltr Formal modified_params - (modified_ltr Global modified_globals skipped_functions) - in - Reporting.log_issue proc_desc err_log ~loc:pname_loc ~ltr Impurity IssueType.impure_function - impure_fun_desc + if PurityChecker.should_report proc_name then ( + if Config.report_immutable_modifications then + ImpurityDomain.get_modified_immutables_opt tenv impurity_astate + |> Option.iter ~f:(fun (modified_params, modified_globals) -> + let immutable_fun_desc = + F.asprintf "Function %a modifies immutable fields" Procname.pp proc_name + in + let immutable_fun_ltr = + Errlog.make_trace_element 0 pname_loc immutable_fun_desc [] + in + let ltr = + immutable_fun_ltr + :: add_modified_ltr Formal modified_params + (add_modified_ltr Global modified_globals []) + in + Reporting.log_issue proc_desc err_log ~loc:pname_loc ~ltr Impurity + IssueType.modifies_immutable immutable_fun_desc ) ; + if not (ImpurityDomain.is_pure impurity_astate) then + let skipped_functions = + SkippedCalls.fold + (fun proc_name trace acc -> + Trace.add_to_errlog ~nesting:1 ~include_value_history:false + ~pp_immediate:(fun fmt -> + F.fprintf fmt "call to skipped function %a occurs here" Procname.pp proc_name ) + trace acc ) + skipped_calls [] + in + let impure_fun_desc = F.asprintf "Impure function %a" Procname.pp proc_name in + let impure_fun_ltr = Errlog.make_trace_element 0 pname_loc impure_fun_desc [] in + let ltr = + impure_fun_ltr + :: add_modified_ltr Formal modified_params + (add_modified_ltr Global modified_globals skipped_functions) + in + Reporting.log_issue proc_desc err_log ~loc:pname_loc ~ltr Impurity + IssueType.impure_function impure_fun_desc ) diff --git a/infer/src/checkers/impurityDomain.ml b/infer/src/checkers/impurityDomain.ml index f83f9df04..a8a865360 100644 --- a/infer/src/checkers/impurityDomain.ml +++ b/infer/src/checkers/impurityDomain.ml @@ -50,6 +50,41 @@ let pure = ; exited= Exited.bottom } +let filter_modifies_immutable tenv ~f = + ModifiedVarMap.filter (fun _pvar ModifiedAccess.{ordered_access_list} -> + List.exists ordered_access_list ~f:(fun access -> + match access with + | HilExp.Access.FieldAccess fname -> ( + let class_name = Fieldname.get_class_name fname in + match Tenv.lookup tenv class_name with + | Some mstruct -> + f mstruct + |> List.exists ~f:(fun (fieldname, _typ, annot) -> + String.equal + (Fieldname.get_field_name fieldname) + (Fieldname.get_field_name fname) + && Annotations.ia_has_annotation_with annot (fun annot -> + Annotations.annot_ends_with annot Annotations.immutable ) ) + | None -> + false ) + | _ -> + false ) ) + + +let get_modified_immutables_opt tenv {modified_params; modified_globals} = + let modified_immutable_params = + filter_modifies_immutable tenv modified_params ~f:(fun s -> s.fields) + in + let modified_immutable_globals = + filter_modifies_immutable tenv modified_globals ~f:(fun s -> s.statics) + in + if + ModifiedVarMap.is_bottom modified_immutable_params + && ModifiedVarMap.is_bottom modified_immutable_globals + then None + else Some (modified_immutable_params, modified_immutable_globals) + + let join astate1 astate2 = if phys_equal astate1 astate2 then astate1 else diff --git a/infer/src/checkers/impurityDomain.mli b/infer/src/checkers/impurityDomain.mli index 56971f853..5fd74e555 100644 --- a/infer/src/checkers/impurityDomain.mli +++ b/infer/src/checkers/impurityDomain.mli @@ -48,3 +48,5 @@ val add_to_errlog : -> Errlog.loc_trace_elem list val join : t -> t -> t + +val get_modified_immutables_opt : Tenv.t -> t -> (ModifiedVarMap.t * ModifiedVarMap.t) option diff --git a/infer/tests/codetoanalyze/java/immutability/ArrayTest.java b/infer/tests/codetoanalyze/java/immutability/ArrayTest.java new file mode 100644 index 000000000..5f42a87a9 --- /dev/null +++ b/infer/tests/codetoanalyze/java/immutability/ArrayTest.java @@ -0,0 +1,57 @@ +/* + * 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. + */ +package codetoanalyze.java.immutability; + +import com.moblica.common.xmob.utils.Immutable; + +class ArrayTest { + @Immutable final int[] testArray = new int[] {0, 1, 2, 4}; + @Immutable static String[] suitArray = {"spades", "hearts", "diamonds", "clubs"}; + int[] mutableArray = new int[] {0}; + + void array_mod_bad() { + testArray[3] = 3; // modifications to an immutable array are not ok + } + + int[] get_testArray() { + return testArray; + } + + void mutate_array_via_getter_bad() { + int[] array = get_testArray(); + array[2] = 7; // ERROR! + } + + void mutate_array_via_aliasing_bad() { + int[] array = get_testArray(); + int[] otherArray = array; + otherArray[2] = 7; // ERROR! + } + + void mutate_array_via_callee_bad() { + int[] array = get_testArray(); + int[] otherArray = array; + mutate_param_ok(array); // ERROR! + } + + void mutate_param_ok(int[] array) { + array[2] = 7; + } + + void mutate_static_array_bad() { + suitArray[0] = "pades"; // ERROR! + } + + void mutable_array_mod_ok() { + mutableArray[0] = 3; // modifications to mutable arrays are ok + } + + void mixed_mod_bad() { + mutableArray[0] = 3; // modifications to mutable arrays are ok + mutate_array_via_callee_bad(); // // modifications to immutables are not + } +} diff --git a/infer/tests/codetoanalyze/java/immutability/Immutable.java b/infer/tests/codetoanalyze/java/immutability/Immutable.java new file mode 100644 index 000000000..d33479c25 --- /dev/null +++ b/infer/tests/codetoanalyze/java/immutability/Immutable.java @@ -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. + */ +package com.moblica.common.xmob.utils; + +import java.lang.annotation.ElementType; +import java.lang.annotation.Target; + +/* + * add this annotation to a field to tell the static analyser that it should not be mutated, making + * tighter restrictions than normal. e.g. an @Immutable array can't have elements reassigned or to a + * method to tell that the return value shouldn't be mutated past that point + */ +@Target({ElementType.FIELD, ElementType.METHOD}) +public @interface Immutable {} diff --git a/infer/tests/codetoanalyze/java/immutability/Makefile b/infer/tests/codetoanalyze/java/immutability/Makefile new file mode 100644 index 000000000..89f5077ad --- /dev/null +++ b/infer/tests/codetoanalyze/java/immutability/Makefile @@ -0,0 +1,13 @@ +# 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. + +TESTS_DIR = ../../.. + +ANALYZER = checkers +INFER_OPTIONS = --impurity-only --report-immutable-modifications --disable-issue-type IMPURE_FUNCTION +INFERPRINT_OPTIONS = --issues-tests +SOURCES = $(wildcard *.java) + +include $(TESTS_DIR)/javac.make diff --git a/infer/tests/codetoanalyze/java/immutability/OuterTest.java b/infer/tests/codetoanalyze/java/immutability/OuterTest.java new file mode 100644 index 000000000..c2b419059 --- /dev/null +++ b/infer/tests/codetoanalyze/java/immutability/OuterTest.java @@ -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. + */ +package codetoanalyze.java.immutability; + +class OuterTest { + + ArrayTest[] arrays; + + void mutate_via_field_bad() { + ArrayTest atest = arrays[0]; + int[] array = atest.get_testArray(); + atest.mutate_param_ok(array); // ERROR! + } +} diff --git a/infer/tests/codetoanalyze/java/immutability/issues.exp b/infer/tests/codetoanalyze/java/immutability/issues.exp new file mode 100644 index 000000000..a2e44f290 --- /dev/null +++ b/infer/tests/codetoanalyze/java/immutability/issues.exp @@ -0,0 +1,7 @@ +codetoanalyze/java/immutability/ArrayTest.java, codetoanalyze.java.immutability.ArrayTest.array_mod_bad():void, 0, MODIFIES_IMMUTABLE, no_bucket, ERROR, [Function void ArrayTest.array_mod_bad() modifies immutable fields,parameter `this.*testArray*[]` modified here] +codetoanalyze/java/immutability/ArrayTest.java, codetoanalyze.java.immutability.ArrayTest.mixed_mod_bad():void, 0, MODIFIES_IMMUTABLE, no_bucket, ERROR, [Function void ArrayTest.mixed_mod_bad() modifies immutable fields,when calling `void ArrayTest.mutate_array_via_callee_bad()` here,when calling `void ArrayTest.mutate_param_ok(int[])` here,parameter `this.*testArray*[]` modified here] +codetoanalyze/java/immutability/ArrayTest.java, codetoanalyze.java.immutability.ArrayTest.mutate_array_via_aliasing_bad():void, 0, MODIFIES_IMMUTABLE, no_bucket, ERROR, [Function void ArrayTest.mutate_array_via_aliasing_bad() modifies immutable fields,parameter `this.*testArray*[]` modified here] +codetoanalyze/java/immutability/ArrayTest.java, codetoanalyze.java.immutability.ArrayTest.mutate_array_via_callee_bad():void, 0, MODIFIES_IMMUTABLE, no_bucket, ERROR, [Function void ArrayTest.mutate_array_via_callee_bad() modifies immutable fields,when calling `void ArrayTest.mutate_param_ok(int[])` here,parameter `this.*testArray*[]` modified here] +codetoanalyze/java/immutability/ArrayTest.java, codetoanalyze.java.immutability.ArrayTest.mutate_array_via_getter_bad():void, 0, MODIFIES_IMMUTABLE, no_bucket, ERROR, [Function void ArrayTest.mutate_array_via_getter_bad() modifies immutable fields,parameter `this.*testArray*[]` modified here] +codetoanalyze/java/immutability/ArrayTest.java, codetoanalyze.java.immutability.ArrayTest.mutate_static_array_bad():void, 0, MODIFIES_IMMUTABLE, no_bucket, ERROR, [Function void ArrayTest.mutate_static_array_bad() modifies immutable fields,global variable `immutability.ArrayTest.*suitArray*[]` modified here] +codetoanalyze/java/immutability/OuterTest.java, codetoanalyze.java.immutability.OuterTest.mutate_via_field_bad():void, 0, MODIFIES_IMMUTABLE, no_bucket, ERROR, [Function void OuterTest.mutate_via_field_bad() modifies immutable fields,when calling `void ArrayTest.mutate_param_ok(int[])` here,parameter `this.*arrays*[]*testArray*[]` modified here]