[immutability] Add a new experimental immutability analysis

Summary:
This diff adds a new issue type for reporting modifications to immutable fields (when `report-immutable-modifications` is enabled).

The underlying analysis depends on impurity analysis which itself is based on post-processing of pulse's summaries.

Reviewed By: skcho

Differential Revision: D25216637

fbshipit-source-id: 42e843793

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;
+  }
+```

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

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
 

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
 

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

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

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
 

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"

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

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

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

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"]

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

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,12 +211,24 @@ 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
+      if PurityChecker.should_report proc_name then (
-        let modified_ltr param_source set acc =
+        if Config.report_immutable_modifications then
-          ImpurityDomain.ModifiedVarMap.fold
+          ImpurityDomain.get_modified_immutables_opt tenv impurity_astate
-            (ImpurityDomain.add_to_errlog ~nesting:1 param_source)
+          |> Option.iter ~f:(fun (modified_params, modified_globals) ->
-            set acc
+                 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 ->
@@ -226,8 +242,8 @@ let checker {IntraproceduralAnalysis.proc_desc; tenv; err_log}
           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
+            :: add_modified_ltr Formal modified_params
-               (modified_ltr Global modified_globals skipped_functions)
+                 (add_modified_ltr Global modified_globals skipped_functions)
           in
-        Reporting.log_issue proc_desc err_log ~loc:pname_loc ~ltr Impurity IssueType.impure_function
+          Reporting.log_issue proc_desc err_log ~loc:pname_loc ~ltr Impurity
-          impure_fun_desc
+            IssueType.impure_function impure_fun_desc )

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

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

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
+  }
+}

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 {}

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

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!
+  }
+}

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]