diff --git a/Makefile b/Makefile index 1643e8da7..146da1c18 100644 --- a/Makefile +++ b/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 diff --git a/infer/man/man1/infer-analyze.txt b/infer/man/man1/infer-analyze.txt index 02a2997be..4c815c729 100644 --- a/infer/man/man1/infer-analyze.txt +++ b/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) diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index de2794962..54ad978e3 100644 --- a/infer/man/man1/infer-full.txt +++ b/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). diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index eb48df94f..5e047e3f1 100644 --- a/infer/man/man1/infer.txt +++ b/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). diff --git a/infer/src/backend/Payloads.ml b/infer/src/backend/Payloads.ml index 8cf484e8a..89baac116 100644 --- a/infer/src/backend/Payloads.ml +++ b/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 } diff --git a/infer/src/backend/Payloads.mli b/infer/src/backend/Payloads.mli index 34a737bed..4ea301e94 100644 --- a/infer/src/backend/Payloads.mli +++ b/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 diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index faca48c50..db5cb4183 100644 --- a/infer/src/base/Config.ml +++ b/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 diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 9665ca5e9..1d7ecc20e 100644 --- a/infer/src/base/Config.mli +++ b/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 diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index 6ce4cc31c..18b1423bb 100644 --- a/infer/src/base/IssueType.ml +++ b/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" diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli index 4cd5e66fb..57c7081a9 100644 --- a/infer/src/base/IssueType.mli +++ b/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 diff --git a/infer/src/checkers/purity.ml b/infer/src/checkers/purity.ml new file mode 100644 index 000000000..88760789c --- /dev/null +++ b/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 diff --git a/infer/src/checkers/purityDomain.ml b/infer/src/checkers/purityDomain.ml new file mode 100644 index 000000000..55b402b1f --- /dev/null +++ b/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 diff --git a/infer/src/checkers/registerCheckers.ml b/infer/src/checkers/registerCheckers.ml index 1e46f6a18..6adda581f 100644 --- a/infer/src/checkers/registerCheckers.ml +++ b/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 () = diff --git a/infer/tests/codetoanalyze/java/purity/Makefile b/infer/tests/codetoanalyze/java/purity/Makefile new file mode 100644 index 000000000..22d3c761d --- /dev/null +++ b/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 diff --git a/infer/tests/codetoanalyze/java/purity/Test.java b/infer/tests/codetoanalyze/java/purity/Test.java new file mode 100644 index 000000000..34133935b --- /dev/null +++ b/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 list = new ArrayList(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; + } + + +} diff --git a/infer/tests/codetoanalyze/java/purity/issues.exp b/infer/tests/codetoanalyze/java/purity/issues.exp new file mode 100644 index 000000000..e1c12e946 --- /dev/null +++ b/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)]