Add simple purity analysis

Reviewed By: mbouaziz, ngorogiannis

Differential Revision: D10027627

fbshipit-source-id: a5ec6b11d

Makefile

@@ -92,7 +92,7 @@ BUILD_SYSTEMS_TESTS += \
 
 DIRECT_TESTS += \
   java_checkers java_eradicate java_infer java_lab java_tracing java_quandary \
-  java_racerd java_stability java_crashcontext java_hoisting java_starvation java_performance
+  java_racerd java_stability java_crashcontext java_hoisting java_starvation java_performance java_purity
 ifneq ($(ANT),no)
 BUILD_SYSTEMS_TESTS += ant
 endif

infer/man/man1/infer-analyze.txt

@@ -219,6 +219,14 @@ OPTIONS
        --project-root,-C dir
            Specify the root directory of the project (default: .)
 
+       --purity
+           Activates: [EXPERIMENTAL] Purity analysis (Conversely:
+           --no-purity)
+
+       --purity-only
+           Activates: Enable --purity and disable all other checkers
+           (Conversely: --no-purity-only)
+
        --quandary
            Activates: the quandary taint analysis (Conversely: --no-quandary)
 

infer/man/man1/infer-full.txt

@@ -645,6 +645,14 @@ OPTIONS
     See also infer-analyze(1), infer-capture(1), infer-report(1), and
            infer-run(1).
 
+       --purity
+           Activates: [EXPERIMENTAL] Purity analysis (Conversely:
+           --no-purity)           See also infer-analyze(1).
+
+       --purity-only
+           Activates: Enable --purity and disable all other checkers
+           (Conversely: --no-purity-only)           See also infer-analyze(1).
+
        --quandary
            Activates: the quandary taint analysis (Conversely: --no-quandary)       
     See also infer-analyze(1).

infer/man/man1/infer.txt

@@ -645,6 +645,14 @@ OPTIONS
     See also infer-analyze(1), infer-capture(1), infer-report(1), and
            infer-run(1).
 
+       --purity
+           Activates: [EXPERIMENTAL] Purity analysis (Conversely:
+           --no-purity)           See also infer-analyze(1).
+
+       --purity-only
+           Activates: Enable --purity and disable all other checkers
+           (Conversely: --no-purity-only)           See also infer-analyze(1).
+
        --quandary
            Activates: the quandary taint analysis (Conversely: --no-quandary)       
     See also infer-analyze(1).

infer/src/backend/Payloads.ml

@@ -21,7 +21,8 @@ type t =
   ; typestate: TypeState.t option
   ; uninit: UninitDomain.summary option
   ; cost: CostDomain.summary option
-  ; starvation: StarvationDomain.summary option }
+  ; starvation: StarvationDomain.summary option
+  ; purity: PurityDomain.summary option }
 
 let pp pe fmt
     { biabduction
@@ -35,14 +36,15 @@ let pp pe fmt
     ; annot_map
     ; uninit
     ; cost
-    ; starvation } =
+    ; starvation
+    ; purity } =
   let pp_opt prefix pp fmt = function
     | Some x ->
         F.fprintf fmt "%s: %a@\n" prefix pp x
     | None ->
         ()
   in
-  F.fprintf fmt "%a%a%a%a%a%a%a%a%a%a%a%a@\n"
+  F.fprintf fmt "%a%a%a%a%a%a%a%a%a%a%a%a%a@\n"
     (pp_opt "Biabduction" (BiabductionSummary.pp pe))
     biabduction (pp_opt "TypeState" TypeState.pp) typestate
     (pp_opt "CrashContext" Crashcontext.pp_stacktree)
@@ -63,6 +65,8 @@ let pp pe fmt
     cost
     (pp_opt "Starvation" StarvationDomain.pp_summary)
     starvation
+    (pp_opt "Purity" PurityDomain.pp_summary)
+    purity
 
 
 let empty =
@@ -78,4 +82,5 @@ let empty =
   ; buffer_overrun= None
   ; uninit= None
   ; cost= None
-  ; starvation= None }
+  ; starvation= None
+  ; purity= None }

infer/src/backend/Payloads.mli

@@ -21,7 +21,8 @@ type t =
   ; typestate: TypeState.t option
   ; uninit: UninitDomain.summary option
   ; cost: CostDomain.summary option
-  ; starvation: StarvationDomain.summary option }
+  ; starvation: StarvationDomain.summary option
+  ; purity: PurityDomain.summary option }
 
 val pp : Pp.env -> Format.formatter -> t -> unit
 

infer/src/base/Config.ml

@@ -596,6 +596,7 @@ and ( annotation_reachability
     , loop_hoisting
     , ownership
     , printf_args
+    , purity
     , quandary
     , quandaryBO
     , racerd
@@ -651,6 +652,7 @@ and ( annotation_reachability
        For, example, this checker will warn about the type error in `printf(\"Hello %d\", \
        \"world\")`"
   and quandary = mk_checker ~long:"quandary" ~default:false "the quandary taint analysis"
+  and purity = mk_checker ~long:"purity" ~default:false "[EXPERIMENTAL] Purity analysis"
   and quandaryBO =
     mk_checker ~long:"quandaryBO" ~default:false
       "[EXPERIMENTAL] The quandaryBO tainted buffer access analysis"
@@ -717,6 +719,7 @@ and ( annotation_reachability
   , loop_hoisting
   , ownership
   , printf_args
+  , purity
   , quandary
   , quandaryBO
   , racerd
@@ -2767,6 +2770,8 @@ and procs_csv = !procs_csv
 
 and project_root = !project_root
 
+and purity = !purity
+
 and quandary = !quandary
 
 and quandaryBO = !quandaryBO

infer/src/base/Config.mli

@@ -527,6 +527,8 @@ val project_root : string
 
 val progress_bar : [`MultiLine | `Plain | `Quiet]
 
+val purity : bool
+
 val quandary : bool
 
 val quandaryBO : bool

infer/src/base/IssueType.ml

@@ -321,6 +321,8 @@ let precondition_not_met = from_string "PRECONDITION_NOT_MET"
 
 let premature_nil_termination = from_string "PREMATURE_NIL_TERMINATION_ARGUMENT"
 
+let pure_function = from_string "PURE_FUNCTION"
+
 let quandary_taint_error = from_string "QUANDARY_TAINT_ERROR"
 
 let registered_observer_being_deallocated = from_string "REGISTERED_OBSERVER_BEING_DEALLOCATED"

infer/src/base/IssueType.mli

@@ -227,6 +227,8 @@ val precondition_not_met : t
 
 val premature_nil_termination : t
 
+val pure_function : t
+
 val quandary_taint_error : t
 
 val registered_observer_being_deallocated : t

infer/src/checkers/purity.ml

@@ -0,0 +1,93 @@
+(*
+ * Copyright (c) 2018-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.
+ *)
+open! IStd
+module F = Format
+module L = Logging
+
+let debug fmt = L.(debug Analysis Verbose fmt)
+
+(* A simple purity checker *)
+
+module Payload = SummaryPayload.Make (struct
+  type t = PurityDomain.summary
+
+  let update_payloads post (payloads : Payloads.t) = {payloads with purity= Some post}
+
+  let of_payloads (payloads : Payloads.t) = payloads.purity
+end)
+
+module TransferFunctions (CFG : ProcCfg.S) = struct
+  module CFG = CFG
+  module Domain = PurityDomain.Pure
+
+  type extras = ProcData.no_extras
+
+  let rec is_heap_access ae =
+    match ae with
+    | AccessExpression.FieldOffset _ | AccessExpression.ArrayOffset _ ->
+        true
+    | AccessExpression.Dereference ae | AccessExpression.AddressOf ae ->
+        is_heap_access ae
+    | AccessExpression.Base _ ->
+        false
+
+
+  let exec_instr (astate : Domain.astate) {ProcData.pdesc; tenv} _ (instr : HilInstr.t) =
+    if astate then
+      match instr with
+      | Assign (ae, _, _) ->
+          not (is_heap_access ae)
+      | Call (_, Direct called_pname, _, _, _) -> (
+        match InvariantModels.Call.dispatch tenv called_pname [] with
+        | Some inv ->
+            InvariantModels.is_invariant inv
+        | None ->
+            Payload.read pdesc called_pname
+            |> Option.value_map ~default:false ~f:(fun summary ->
+                   debug "Reading from %a \n" Typ.Procname.pp called_pname ;
+                   summary ) )
+      | Call (_, Indirect _, _, _, _) ->
+          (* This should never happen in Java. Fail if it does. *)
+          L.(die InternalError) "Unexpected indirect call %a" HilInstr.pp instr
+      | _ ->
+          astate
+    else astate
+
+
+  let pp_session_name _node fmt = F.pp_print_string fmt "purity checker"
+end
+
+module Analyzer = LowerHil.MakeAbstractInterpreter (ProcCfg.Exceptional) (TransferFunctions)
+
+let should_report pure pdesc =
+  match Procdesc.get_proc_name pdesc with
+  | Typ.Procname.Java java_pname as proc_name ->
+      pure
+      && (not (Typ.Procname.is_constructor proc_name))
+      && not (Typ.Procname.Java.is_class_initializer java_pname)
+  | _ ->
+      L.(die InternalError "Not supposed to run on non-Java code.")
+
+
+let checker {Callbacks.tenv; summary; proc_desc} : Summary.t =
+  let initial = true in
+  let proc_name = Procdesc.get_proc_name proc_desc in
+  let proc_data = ProcData.make_default proc_desc tenv in
+  let report_pure () =
+    let loc = Procdesc.get_loc proc_desc in
+    let exp_desc = F.asprintf "Side-effect free function %a" Typ.Procname.pp proc_name in
+    let ltr = [Errlog.make_trace_element 0 loc exp_desc []] in
+    Reporting.log_error summary ~loc ~ltr IssueType.pure_function exp_desc
+  in
+  match Analyzer.compute_post proc_data ~initial with
+  | Some pure ->
+      if should_report pure proc_desc then report_pure () ;
+      Payload.update_summary pure summary
+  | None ->
+      L.internal_error "Analyzer failed to compute purity information for %a@." Typ.Procname.pp
+        proc_name ;
+      summary

infer/src/checkers/purityDomain.ml

@@ -0,0 +1,13 @@
+(*
+ * Copyright (c) 2018-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.
+ *)
+open! IStd
+module F = Format
+module Pure = AbstractDomain.BooleanAnd
+
+type summary = Pure.astate
+
+let pp_summary fmt summary = F.fprintf fmt "@\n Purity summary: %a @\n" Pure.pp summary

infer/src/checkers/registerCheckers.ml

@@ -115,7 +115,12 @@ let all_checkers =
     ; active= Config.starvation
     ; callbacks=
         [ (Procedure Starvation.analyze_procedure, Language.Java)
-        ; (Cluster Starvation.reporting, Language.Java) ] } ]
+        ; (Cluster Starvation.reporting, Language.Java) ] }
+  ; { name= "purity"
+    ; active= Config.purity
+    ; callbacks=
+        [(Procedure Purity.checker, Language.Clang); (Procedure Purity.checker, Language.Java)] }
+  ]
 
 
 let get_active_checkers () =

infer/tests/codetoanalyze/java/purity/Makefile

@@ -0,0 +1,13 @@
+# Copyright (c) 2018-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 = ../../..
+
+ANALYZER = checkers
+INFER_OPTIONS = --purity-only --debug-exceptions
+INFERPRINT_OPTIONS = --issues-tests
+SOURCES = $(wildcard *.java)
+
+include $(TESTS_DIR)/javac.make

infer/tests/codetoanalyze/java/purity/Test.java

@@ -0,0 +1,78 @@
+/*
+ * Copyright (c) 2018-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.
+ */
+import java.util.ArrayList;
+
+class Test {
+
+  private int a = 0;
+  static Integer[] global_arr;
+
+  void Test(int size) {
+    global_arr = new Integer[size];
+  }
+
+  void set_bad(int x, int y) {
+    a = x + y;
+  }
+
+  void global_array_set_bad(int x, int y) {
+    global_arr[0] = x + y;
+  }
+
+  int local_write_ok(int x, int y) {
+    int k = x + y;
+    k++;
+    return k;
+  }
+
+  void call_pure_ok(int size) {
+    for (int i = 0; i < size; i++) {
+      local_write_ok(i, size);
+    }
+  }
+
+  void call_impure_bad(int size) {
+    int d = 0;
+    for (int i = 0; i < size; i++) {
+      set_bad(i, size);
+    }
+  }
+
+  // as soon as we allocate with new, function is marked impure.
+  int local_alloc_bad_FP(int x, int y) {
+    ArrayList<Integer> list = new ArrayList<Integer>(x + y);
+    for (Integer el : list) {
+      call_pure_ok(el);
+    }
+    return list.size();
+  }
+
+
+  void parameter_field_write_bad(Test test, boolean b) {
+    int c = b ? 0 : 1;
+    test.a = c;
+  }
+
+
+  int parameter_field_access_ok(Test test) {
+    return test.a;
+  }
+
+  // expected to be impure since y points to x
+  void local_field_write_bad(Test x) {
+    Test y = x;
+    y.a = 0;
+  }
+
+  void swap_bad(int[] array, int i, int j) {
+    int tmp = array[i];
+    array[i] = array[j];
+    array[j] = tmp;
+   }
+
+
+}

infer/tests/codetoanalyze/java/purity/issues.exp

@@ -0,0 +1,3 @@
+codetoanalyze/java/purity/Test.java, Test.call_pure_ok(int):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void Test.call_pure_ok(int)]
+codetoanalyze/java/purity/Test.java, Test.local_write_ok(int,int):int, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function int Test.local_write_ok(int,int)]
+codetoanalyze/java/purity/Test.java, Test.parameter_field_access_ok(Test):int, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function int Test.parameter_field_access_ok(Test)]