From c5ca4db8d08f11304b940d86a5336755a2be3926 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Mon, 23 Sep 2019 09:53:17 -0700 Subject: [PATCH] [pulse][impurity] Use pulse for detecting impurity Summary: Introduce a new experimental checker (`--impurity`) that detects impurity information, tracking which parameters and global variables of a function are modified. The checker relies on Pulse to detect how the state changes: it traverses the pre and post pairs starting from the parameter/global variable and finds where the pre and post heaps diverge. At diversion points, we expect to see WrittenTo/Invalid attributes containing a trace of how the address was modified. We use these to construct the trace of impurity. This checker is a complement to the purity checker that exists mainly for Java (and used for cost and loop-hoisting analyses). The aim of this new experimental checker is to rely on Pulse's precise memory treatment and come up with a more precise im(purity) analysis. To distinguish the two checkers, we introduce a new issue type `IMPURE_FUNCTION` that reports when a function is impure, rather than when it is pure (as in the purity checker). TODO: - improve the analysis to rely on impurity information of external library calls. Currently, all library calls are assumed to be nops, hence pure. - de-entangle Pulse reporting from analysis. Reviewed By: skcho Differential Revision: D17051567 fbshipit-source-id: 5e10afb4f --- Makefile | 1 + infer/man/man1/infer-analyze.txt | 8 + infer/man/man1/infer-full.txt | 9 ++ infer/man/man1/infer-report.txt | 1 + infer/man/man1/infer.txt | 9 ++ infer/src/backend/Payloads.ml | 3 + infer/src/backend/Payloads.mli | 1 + infer/src/base/Config.ml | 6 + infer/src/base/Config.mli | 2 + infer/src/base/IssueType.ml | 2 + infer/src/base/IssueType.mli | 2 + infer/src/checkers/impurity.ml | 153 ++++++++++++++++++ infer/src/checkers/impurityDomain.ml | 84 ++++++++++ infer/src/checkers/impurityDomain.mli | 39 +++++ infer/src/checkers/purity.ml | 4 + infer/src/checkers/purity.mli | 2 + infer/src/checkers/registerCheckers.ml | 5 + infer/src/pulse/PulseAbductiveDomain.ml | 4 + infer/src/pulse/PulseAbductiveDomain.mli | 4 + infer/src/pulse/PulseDomain.mli | 2 + .../tests/codetoanalyze/cpp/impurity/Makefile | 17 ++ .../codetoanalyze/cpp/impurity/array_test.cpp | 62 +++++++ .../cpp/impurity/global_test.cpp | 34 ++++ .../cpp/impurity/invalid_test.cpp | 36 +++++ .../codetoanalyze/cpp/impurity/issues.exp | 26 +++ .../codetoanalyze/cpp/impurity/param_test.cpp | 28 ++++ .../codetoanalyze/cpp/impurity/unmodeled.cpp | 11 ++ .../codetoanalyze/cpp/impurity/vector.cpp | 41 +++++ 28 files changed, 596 insertions(+) create mode 100644 infer/src/checkers/impurity.ml create mode 100644 infer/src/checkers/impurityDomain.ml create mode 100644 infer/src/checkers/impurityDomain.mli create mode 100644 infer/tests/codetoanalyze/cpp/impurity/Makefile create mode 100644 infer/tests/codetoanalyze/cpp/impurity/array_test.cpp create mode 100644 infer/tests/codetoanalyze/cpp/impurity/global_test.cpp create mode 100644 infer/tests/codetoanalyze/cpp/impurity/invalid_test.cpp create mode 100644 infer/tests/codetoanalyze/cpp/impurity/issues.exp create mode 100644 infer/tests/codetoanalyze/cpp/impurity/param_test.cpp create mode 100644 infer/tests/codetoanalyze/cpp/impurity/unmodeled.cpp create mode 100644 infer/tests/codetoanalyze/cpp/impurity/vector.cpp diff --git a/Makefile b/Makefile index bee9cc319..5dc4913de 100644 --- a/Makefile +++ b/Makefile @@ -62,6 +62,7 @@ DIRECT_TESTS += \ cpp_conflicts \ cpp_errors \ cpp_frontend \ + cpp_impurity \ cpp_linters \ cpp_linters-for-test-only \ cpp_liveness \ diff --git a/infer/man/man1/infer-analyze.txt b/infer/man/man1/infer-analyze.txt index 74fbac872..d8c8507ec 100644 --- a/infer/man/man1/infer-analyze.txt +++ b/infer/man/man1/infer-analyze.txt @@ -141,6 +141,14 @@ OPTIONS Activates: Enable --immutable-cast and disable all other checkers (Conversely: --no-immutable-cast-only) + --impurity + Activates: [EXPERIMENTAL] Impurity analysis (Conversely: + --no-impurity) + + --impurity-only + Activates: Enable --impurity and disable all other checkers + (Conversely: --no-impurity-only) + --no-inefficient-keyset-iterator Deactivates: Check for inefficient uses of keySet iterator that access both the key and the value. (Conversely: diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 566cbaae4..324cd2802 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -401,6 +401,7 @@ OPTIONS (disabled by default), GRAPHQL_FIELD_ACCESS (enabled by default), GUARDEDBY_VIOLATION (enabled by default), + IMPURE_FUNCTION (enabled by default), INEFFICIENT_KEYSET_ITERATOR (enabled by default), INFERBO_ALLOC_IS_BIG (enabled by default), INFERBO_ALLOC_IS_NEGATIVE (enabled by default), @@ -606,6 +607,14 @@ OPTIONS Activates: Enable --immutable-cast and disable all other checkers (Conversely: --no-immutable-cast-only) See also infer-analyze(1). + --impurity + Activates: [EXPERIMENTAL] Impurity analysis (Conversely: + --no-impurity) See also infer-analyze(1). + + --impurity-only + Activates: Enable --impurity and disable all other checkers + (Conversely: --no-impurity-only) See also infer-analyze(1). + --no-inefficient-keyset-iterator Deactivates: Check for inefficient uses of keySet iterator that access both the key and the value. (Conversely: diff --git a/infer/man/man1/infer-report.txt b/infer/man/man1/infer-report.txt index df59be235..e4ae91463 100644 --- a/infer/man/man1/infer-report.txt +++ b/infer/man/man1/infer-report.txt @@ -150,6 +150,7 @@ OPTIONS (disabled by default), GRAPHQL_FIELD_ACCESS (enabled by default), GUARDEDBY_VIOLATION (enabled by default), + IMPURE_FUNCTION (enabled by default), INEFFICIENT_KEYSET_ITERATOR (enabled by default), INFERBO_ALLOC_IS_BIG (enabled by default), INFERBO_ALLOC_IS_NEGATIVE (enabled by default), diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index b47e25b45..5134b98e6 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -401,6 +401,7 @@ OPTIONS (disabled by default), GRAPHQL_FIELD_ACCESS (enabled by default), GUARDEDBY_VIOLATION (enabled by default), + IMPURE_FUNCTION (enabled by default), INEFFICIENT_KEYSET_ITERATOR (enabled by default), INFERBO_ALLOC_IS_BIG (enabled by default), INFERBO_ALLOC_IS_NEGATIVE (enabled by default), @@ -606,6 +607,14 @@ OPTIONS Activates: Enable --immutable-cast and disable all other checkers (Conversely: --no-immutable-cast-only) See also infer-analyze(1). + --impurity + Activates: [EXPERIMENTAL] Impurity analysis (Conversely: + --no-impurity) See also infer-analyze(1). + + --impurity-only + Activates: Enable --impurity and disable all other checkers + (Conversely: --no-impurity-only) See also infer-analyze(1). + --no-inefficient-keyset-iterator Deactivates: Check for inefficient uses of keySet iterator that access both the key and the value. (Conversely: diff --git a/infer/src/backend/Payloads.ml b/infer/src/backend/Payloads.ml index 3369341ef..b0096eac1 100644 --- a/infer/src/backend/Payloads.ml +++ b/infer/src/backend/Payloads.ml @@ -15,6 +15,7 @@ type t = ; buffer_overrun_checker: BufferOverrunCheckerSummary.t option ; class_loads: ClassLoadsDomain.summary option ; cost: CostDomain.summary option + ; impurity: ImpurityDomain.t option ; lab_resource_leaks: ResourceLeakDomain.summary option ; litho: LithoDomain.t option ; pulse: PulseSummary.t option @@ -43,6 +44,7 @@ let fields = ~buffer_overrun_checker:(fun f -> mk f "BufferOverrunChecker" BufferOverrunCheckerSummary.pp) ~class_loads:(fun f -> mk f "ClassLoads" ClassLoadsDomain.pp_summary) ~cost:(fun f -> mk f "Cost" CostDomain.pp_summary) + ~impurity:(fun f -> mk f "Impurity" ImpurityDomain.pp) ~litho:(fun f -> mk f "Litho" LithoDomain.pp) ~pulse:(fun f -> mk f "Pulse" PulseSummary.pp) ~purity:(fun f -> mk f "Purity" PurityDomain.pp_summary) @@ -68,6 +70,7 @@ let empty = ; buffer_overrun_checker= None ; class_loads= None ; cost= None + ; impurity= None ; lab_resource_leaks= None ; litho= None ; pulse= None diff --git a/infer/src/backend/Payloads.mli b/infer/src/backend/Payloads.mli index 48d2cf30a..764f4b5b1 100644 --- a/infer/src/backend/Payloads.mli +++ b/infer/src/backend/Payloads.mli @@ -20,6 +20,7 @@ include ; buffer_overrun_checker: BufferOverrunCheckerSummary.t option ; class_loads: ClassLoadsDomain.summary option ; cost: CostDomain.summary option + ; impurity: ImpurityDomain.t option ; lab_resource_leaks: ResourceLeakDomain.summary option ; litho: LithoDomain.t option ; pulse: PulseSummary.t option diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 2f0ad0618..6051093b3 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -27,6 +27,7 @@ type checkers = ; eradicate: bool ref ; fragment_retains_view: bool ref ; immutable_cast: bool ref + ; impurity: bool ref ; inefficient_keyset_iterator: bool ref ; linters: bool ref ; litho: bool ref @@ -667,6 +668,7 @@ and { annotation_reachability ; eradicate ; fragment_retains_view ; immutable_cast + ; impurity ; inefficient_keyset_iterator ; linters ; litho @@ -713,6 +715,7 @@ and { annotation_reachability mk_checker ~long:"immutable-cast" ~default:false "the detection of object cast from immutable type to mutable type. For instance, it will \ detect cast from ImmutableList to List, ImmutableMap to Map, and ImmutableSet to Set." + and impurity = mk_checker ~long:"impurity" ~default:false "[EXPERIMENTAL] Impurity analysis" and inefficient_keyset_iterator = mk_checker ~long:"inefficient-keyset-iterator" ~default:true "Check for inefficient uses of keySet iterator that access both the key and the value." @@ -789,6 +792,7 @@ and { annotation_reachability ; eradicate ; fragment_retains_view ; immutable_cast + ; impurity ; inefficient_keyset_iterator ; linters ; litho @@ -2905,6 +2909,8 @@ and icfg_dotty_outfile = !icfg_dotty_outfile and immutable_cast = !immutable_cast +and impurity = !impurity + and inefficient_keyset_iterator = !inefficient_keyset_iterator and iphoneos_target_sdk_version = !iphoneos_target_sdk_version diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 3b45b46bc..aa1bbebaa 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -396,6 +396,8 @@ val icfg_dotty_outfile : string option val immutable_cast : bool +val impurity : bool + val inefficient_keyset_iterator : bool val infer_is_clang : bool diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index 116e04c9d..1cfd39656 100644 --- a/infer/src/base/IssueType.ml +++ b/infer/src/base/IssueType.ml @@ -287,6 +287,8 @@ let guardedby_violation_racerd = register_from_string "GUARDEDBY_VIOLATION" ~hum:"GuardedBy Violation" +let impure_function = register_from_string "IMPURE_FUNCTION" + let inefficient_keyset_iterator = register_from_string "INEFFICIENT_KEYSET_ITERATOR" let inferbo_alloc_is_big = register_from_string "INFERBO_ALLOC_IS_BIG" diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli index 52920ad2f..55f0bbf2e 100644 --- a/infer/src/base/IssueType.mli +++ b/infer/src/base/IssueType.mli @@ -174,6 +174,8 @@ val graphql_field_access : t val guardedby_violation_racerd : t +val impure_function : t + val inefficient_keyset_iterator : t val inferbo_alloc_is_big : t diff --git a/infer/src/checkers/impurity.ml b/infer/src/checkers/impurity.ml new file mode 100644 index 000000000..e01f96611 --- /dev/null +++ b/infer/src/checkers/impurity.ml @@ -0,0 +1,153 @@ +(* + * 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. + *) +open! IStd +module F = Format +module L = Logging +module AbstractAddress = PulseDomain.AbstractAddress +module Attributes = PulseDomain.Attributes +module BaseStack = PulseDomain.Stack + +let debug fmt = L.(debug Analysis Verbose fmt) + +(* An impurity analysis that relies on pulse to determine how the state + changes *) + +module Payload = SummaryPayload.Make (struct + type t = ImpurityDomain.t + + let field = Payloads.Fields.impurity +end) + +let get_matching_dest_addr_opt ~edges_pre ~edges_post : AbstractAddress.t list option = + match + List.fold2 ~init:(Some []) + ~f:(fun acc (_, (addr_dest_pre, _)) (_, (addr_dest_post, _)) -> + if AbstractAddress.equal addr_dest_pre addr_dest_post then + Option.map acc ~f:(fun acc -> addr_dest_pre :: acc) + else None ) + (PulseDomain.Memory.Edges.bindings edges_pre) + (PulseDomain.Memory.Edges.bindings edges_post) + with + | Unequal_lengths -> + debug "Mismatch in pre and post.\n" ; + None + | Ok x -> + x + + +let add_invalid_and_modified ~check_empty attrs acc = + let modified = + Attributes.get_written_to attrs + |> Option.value_map ~default:[] ~f:(fun modified -> [ImpurityDomain.WrittenTo modified]) + in + let res = + Attributes.get_invalid attrs + |> Option.value_map ~default:modified ~f:(fun invalid -> + ImpurityDomain.Invalid invalid :: modified ) + in + if check_empty && List.is_empty res then + L.(die InternalError) "Address is modified without being written to or invalidated." + else res @ acc + + +(** Given Pulse summary, extract impurity info, i.e. parameters and + global variables that are modified by the function. + + TODO: keep track of impure library calls *) +let extract_impurity pdesc pre_post : ImpurityDomain.t = + let pre_heap = (PulseAbductiveDomain.extract_pre pre_post).PulseDomain.heap in + let post_heap = (PulseAbductiveDomain.extract_post pre_post).PulseDomain.heap in + let post_stack = (PulseAbductiveDomain.extract_post pre_post).PulseDomain.stack in + let add_to_modified var addr acc = + let rec aux acc ~addr_to_explore ~visited : ImpurityDomain.trace list = + match addr_to_explore with + | [] -> + acc + | addr :: addr_to_explore -> ( + if PulseDomain.AbstractAddressSet.mem addr visited then aux acc ~addr_to_explore ~visited + else + let cell_pre_opt = PulseDomain.Memory.find_opt addr pre_heap in + let cell_post_opt = PulseDomain.Memory.find_opt addr post_heap in + let visited = PulseDomain.AbstractAddressSet.add addr visited in + match (cell_pre_opt, cell_post_opt) with + | None, None -> + aux acc ~addr_to_explore ~visited + | Some (_, _pre_attrs), None -> + L.(die InternalError) + "It is unexpected to have an address which has a binding in pre but not in post!" + | None, Some (_edges_post, attrs_post) -> + aux + (add_invalid_and_modified ~check_empty:false attrs_post acc) + ~addr_to_explore ~visited + | Some (edges_pre, _), Some (edges_post, attrs_post) -> ( + match get_matching_dest_addr_opt ~edges_pre ~edges_post with + | Some addr_list -> + aux + (add_invalid_and_modified attrs_post ~check_empty:false acc) + ~addr_to_explore:(addr_list @ addr_to_explore) ~visited + | None -> + aux + (add_invalid_and_modified ~check_empty:true attrs_post acc) + ~addr_to_explore ~visited ) ) + in + match aux [] ~addr_to_explore:[addr] ~visited:PulseDomain.AbstractAddressSet.empty with + | [] -> + acc + | hd :: tl -> + ImpurityDomain.ModifiedVarSet.add {var; trace_list= (hd, tl)} acc + in + let pname = Procdesc.get_proc_name pdesc in + let modified_params = + Procdesc.get_formals pdesc + |> List.fold_left ~init:ImpurityDomain.ModifiedVarSet.empty ~f:(fun acc (name, typ) -> + let var = Var.of_pvar (Pvar.mk name pname) in + match BaseStack.find_opt var post_stack with + | Some (addr, _) when Typ.is_pointer typ -> + add_to_modified var addr acc + | _ -> + acc ) + in + let modified_globals = + BaseStack.fold + (fun var (addr, _) acc -> if Var.is_global var then add_to_modified var addr acc else acc) + post_stack ImpurityDomain.ModifiedVarSet.empty + in + {modified_globals; modified_params} + + +let report_errors summary (ImpurityDomain.{modified_globals; modified_params} as astate) = + let pdesc = Summary.get_proc_desc summary in + let proc_name = Procdesc.get_proc_name pdesc in + let pname_loc = Procdesc.get_loc pdesc in + if Purity.should_report pdesc && not (ImpurityDomain.is_pure astate) then + let impure_fun_desc = F.asprintf "Impure function %a" Typ.Procname.pp proc_name in + let impure_fun_ltr = Errlog.make_trace_element 0 pname_loc impure_fun_desc [] in + let modified_ltr ~str set acc = + ImpurityDomain.ModifiedVarSet.fold (ImpurityDomain.add_to_errlog ~nesting:1 ~str) set acc + in + let ltr = + impure_fun_ltr + :: modified_ltr ~str:"parameter" modified_params + (modified_ltr ~str:"global var" modified_globals []) + in + Reporting.log_error summary ~loc:pname_loc ~ltr IssueType.impure_function impure_fun_desc + + +let checker ({Callbacks.summary} as callback) : Summary.t = + let pulse_summary = Pulse.checker callback in + match pulse_summary.payloads.pulse with + | Some pre_posts -> + let modified = + List.fold pre_posts ~init:ImpurityDomain.pure ~f:(fun acc pre_post -> + let modified = extract_impurity (Summary.get_proc_desc summary) pre_post in + ImpurityDomain.join acc modified ) + in + report_errors summary modified ; + Payload.update_summary modified summary + | None -> + debug "@\n\n[WARNING] Couldn't find any Pulse summary to extract impurity information." ; + summary diff --git a/infer/src/checkers/impurityDomain.ml b/infer/src/checkers/impurityDomain.ml new file mode 100644 index 000000000..446ce103b --- /dev/null +++ b/infer/src/checkers/impurityDomain.ml @@ -0,0 +1,84 @@ +(* + * 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. + *) + +open! IStd +module F = Format + +type trace = + | WrittenTo of unit PulseDomain.InterprocAction.t + | Invalid of PulseDomain.Invalidation.t PulseDomain.Trace.t +[@@deriving compare] + +module ModifiedVar = struct + type nonempty_action_type = trace * trace list [@@deriving compare] + + type t = {var: Var.t; trace_list: nonempty_action_type} [@@deriving compare] + + let pp fmt {var} = F.fprintf fmt "@\n %a @\n" Var.pp var +end + +module ModifiedVarSet = AbstractDomain.FiniteSet (ModifiedVar) + +type t = {modified_params: ModifiedVarSet.t; modified_globals: ModifiedVarSet.t} + +let is_pure {modified_globals; modified_params} = + ModifiedVarSet.is_empty modified_globals && ModifiedVarSet.is_empty modified_params + + +let pp fmt ({modified_globals; modified_params} as astate) = + if is_pure astate then F.fprintf fmt "@\n pure @\n" + else if ModifiedVarSet.is_empty modified_params then + F.fprintf fmt "@\n impure, modified globals :%a @\n" ModifiedVarSet.pp modified_globals + else if ModifiedVarSet.is_empty modified_globals then + F.fprintf fmt "@\n impure, modified params :%a @\n" ModifiedVarSet.pp modified_params + else + F.fprintf fmt "@\n impure, modified params :%a, modified globals :%a @\n" ModifiedVarSet.pp + modified_params ModifiedVarSet.pp modified_globals + + +let pure = {modified_params= ModifiedVarSet.empty; modified_globals= ModifiedVarSet.empty} + +let join astate1 astate2 = + if phys_equal astate1 astate2 then astate1 + else + let {modified_globals= mg1; modified_params= mp1} = astate1 in + let {modified_globals= mg2; modified_params= mp2} = astate2 in + PhysEqual.optim2 + ~res: + { modified_globals= ModifiedVarSet.join mg1 mg2 + ; modified_params= ModifiedVarSet.join mp1 mp2 } + astate1 astate2 + + +let add_to_errlog ~nesting ~str ModifiedVar.{var; trace_list} errlog = + let rec aux ~nesting rev_errlog action = + match action with + | WrittenTo (PulseDomain.InterprocAction.Immediate {location}) -> + let rev_errlog = + Errlog.make_trace_element nesting location + (F.asprintf "%s '%a' is modified at %a" str Var.pp var Location.pp location) + [] + :: rev_errlog + in + List.rev_append rev_errlog errlog + | WrittenTo (PulseDomain.InterprocAction.ViaCall {action; f; location}) -> + aux ~nesting:(nesting + 1) + ( Errlog.make_trace_element nesting location + (F.asprintf "%s '%a' is modified when calling %a at %a" str Var.pp var + PulseDomain.describe_call_event f Location.pp location) + [] + :: rev_errlog ) + (WrittenTo action) + | Invalid trace -> + PulseDomain.Trace.add_to_errlog + ~header:(F.asprintf "%s '%a'" str Var.pp var) + (fun f invalidation -> + F.fprintf f "%a here" PulseDomain.Invalidation.describe invalidation ) + trace rev_errlog + in + let first_trace, rest = trace_list in + List.fold_left rest ~init:(aux ~nesting [] first_trace) ~f:(aux ~nesting) diff --git a/infer/src/checkers/impurityDomain.mli b/infer/src/checkers/impurityDomain.mli new file mode 100644 index 000000000..2dc89b743 --- /dev/null +++ b/infer/src/checkers/impurityDomain.mli @@ -0,0 +1,39 @@ +(* + * 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. + *) +open! IStd + +type trace = + | WrittenTo of unit PulseDomain.InterprocAction.t + | Invalid of PulseDomain.Invalidation.t PulseDomain.Trace.t +[@@deriving compare] + +module ModifiedVar : sig + type nonempty_action_type = trace * trace sexp_list + + type t = {var: Var.t; trace_list: nonempty_action_type} +end + +module ModifiedVarSet : sig + include AbstractDomain.FiniteSetS with type elt = ModifiedVar.t +end + +type t = {modified_params: ModifiedVarSet.t; modified_globals: ModifiedVarSet.t} + +val pure : t + +val is_pure : t -> bool + +val add_to_errlog : + nesting:int + -> str:string + -> ModifiedVar.t + -> Errlog.loc_trace_elem sexp_list + -> Errlog.loc_trace_elem sexp_list + +val pp : Format.formatter -> t -> unit + +val join : t -> t -> t diff --git a/infer/src/checkers/purity.ml b/infer/src/checkers/purity.ml index 5192ca496..32dd4c44b 100644 --- a/infer/src/checkers/purity.ml +++ b/infer/src/checkers/purity.ml @@ -193,6 +193,10 @@ let should_report pdesc = not ( Typ.Procname.Java.is_class_initializer java_pname || Typ.Procname.Java.is_access_method java_pname ) + | Typ.Procname.ObjC_Cpp name -> + not + ( Typ.Procname.ObjC_Cpp.is_destructor name + || Typ.Procname.ObjC_Cpp.is_objc_constructor name.method_name ) | _ -> true diff --git a/infer/src/checkers/purity.mli b/infer/src/checkers/purity.mli index 489676eb8..455a55f9f 100644 --- a/infer/src/checkers/purity.mli +++ b/infer/src/checkers/purity.mli @@ -8,3 +8,5 @@ open! IStd val checker : Callbacks.proc_callback_t + +val should_report : Procdesc.t -> bool diff --git a/infer/src/checkers/registerCheckers.ml b/infer/src/checkers/registerCheckers.ml index 865148ca4..31b69ad66 100644 --- a/infer/src/checkers/registerCheckers.ml +++ b/infer/src/checkers/registerCheckers.ml @@ -123,6 +123,11 @@ let all_checkers = ; (Cluster Starvation.reporting, Language.Java) ; (Procedure Starvation.analyze_procedure, Language.Clang) ; (Cluster Starvation.reporting, Language.Clang) ] } + ; { name= "impurity" + ; active= Config.impurity + ; callbacks= + [(Procedure Impurity.checker, Language.Clang); (Procedure Pulse.checker, Language.Clang)] + } ; { name= "purity" ; active= Config.purity || Config.loop_hoisting ; callbacks= diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index e1cd3b5f0..2892a31c4 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -836,3 +836,7 @@ module PrePost = struct (* apply the postcondition *) Ok (apply_post callee_proc_name call_location pre_post ~formals ~actuals call_state) end + +let extract_pre {pre} = (pre :> PulseDomain.t) + +let extract_post {post} = (post :> PulseDomain.t) diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index 4c25a6480..a6214b28b 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -102,3 +102,7 @@ end val discard_unreachable : t -> t (** garbage collect unreachable addresses in the state to make it smaller, just for convenience and keep its size down *) + +val extract_pre : PrePost.t -> PulseDomain.t + +val extract_post : PrePost.t -> PulseDomain.t diff --git a/infer/src/pulse/PulseDomain.mli b/infer/src/pulse/PulseDomain.mli index b45e25715..d6fe2c56b 100644 --- a/infer/src/pulse/PulseDomain.mli +++ b/infer/src/pulse/PulseDomain.mli @@ -96,6 +96,8 @@ module Attributes : sig val get_must_be_valid : t -> unit InterprocAction.t option + val get_invalid : t -> Invalidation.t Trace.t option + val get_written_to : t -> unit InterprocAction.t option val get_address_of_stack_variable : t -> (Var.t * ValueHistory.t * Location.t) option diff --git a/infer/tests/codetoanalyze/cpp/impurity/Makefile b/infer/tests/codetoanalyze/cpp/impurity/Makefile new file mode 100644 index 000000000..51f5b1d2c --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/impurity/Makefile @@ -0,0 +1,17 @@ +# 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 = ../../.. + +# see explanations in cpp/errors/Makefile for the custom isystem +CLANG_OPTIONS = -x c++ -std=c++17 -nostdinc++ -isystem$(CLANG_INCLUDES)/c++/v1/ -c +INFER_OPTIONS = --impurity-only --debug-exceptions --project-root $(TESTS_DIR) --report-force-relative-path +INFERPRINT_OPTIONS = --issues-tests + +SOURCES = $(wildcard *.cpp) + +include $(TESTS_DIR)/clang.make + +infer-out/report.json: $(MAKEFILE_LIST) diff --git a/infer/tests/codetoanalyze/cpp/impurity/array_test.cpp b/infer/tests/codetoanalyze/cpp/impurity/array_test.cpp new file mode 100644 index 000000000..798442fab --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/impurity/array_test.cpp @@ -0,0 +1,62 @@ +/* + * 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. + */ +// modifies a & b +void array_mod_impure(int a[10], int b[10], int c) { + a[0] = c; + b[0] = c; +} + +// modifies a twice +void array_mod_both_impure(int a[10], int b) { + a[0] = b; + a[1] = 0; +} + +// modifies a +void call_array_mod_impure(int a[10]) { + int b[10]; + array_mod_impure(a, b, 9); +} + +void call_array_mod_with_fresh_pure() { + int a[10]; + array_mod_impure(a, a, 0); +} + +// modifies array +void alias_mod_impure(int array[], int i, int j) { + int* a = array; + a[j] = i; +} + +struct Foo { + int x; +}; + +void modify_direct_impure(Foo array[10], int i, Foo foo) { array[i].x = foo.x; } + +void modify_ptr_impure(Foo array[10], Foo foo) { + Foo* tmp = array; + tmp->x = foo.x; +} + +void call_impure_with_fresh_pure() { + struct Foo f1 = {1}; + struct Foo f2 = {2}; + struct Foo f3 = {3}; + Foo array[2] = {f1, f2}; + modify_direct_impure(array, 0, f3); + modify_ptr_impure(array, f3); +} + +// Note: Unlike C++, in Java, this is gonna be impure because +// everything is passed by reference in Java +int modify_by_copy_pure(Foo array[1], int i, Foo foo) { + Foo tmp = array[i]; + tmp.x = foo.x; + return tmp.x; +} diff --git a/infer/tests/codetoanalyze/cpp/impurity/global_test.cpp b/infer/tests/codetoanalyze/cpp/impurity/global_test.cpp new file mode 100644 index 000000000..3f4128d5b --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/impurity/global_test.cpp @@ -0,0 +1,34 @@ +/* + * 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. + */ +static int x; +int a[3]; + +void modify_global_primitive_impure() { x = 10; } + +void modify_global_array_impure() { a[0] = 0; } + +void call_modify_global() { + modify_global_primitive_impure(); + modify_global_array_impure(); +} + +// modifies local static arr +int* local_static_var_impure() { + + // Lifetime of a static variable is throughout the program. + static int arr[100]; + + /* Some operations on arr[] */ + arr[0] = 10; + arr[1] = 20; + + return arr; +} + +void modify_global_inside_lamda_impure() { + auto lam = [&]() { x++; }; +} diff --git a/infer/tests/codetoanalyze/cpp/impurity/invalid_test.cpp b/infer/tests/codetoanalyze/cpp/impurity/invalid_test.cpp new file mode 100644 index 000000000..807c3c9e5 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/impurity/invalid_test.cpp @@ -0,0 +1,36 @@ +/* + * 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. + */ +#include + +int* global_pointer; + +void free_global_pointer_impure() { free(global_pointer); } +// If Pulse raises an error, it stops the world and has no summary. +void double_free_global_impure_FN() { + free_global_pointer_impure(); + free_global_pointer_impure(); +} + +int free_param_impure(int* x) { + free(x); + return 0; +} + +struct Simple { + int f; +}; +void delete_param_impure(Simple* s) { delete s; } + +void local_deleted_pure() { + auto* s = new Simple{1}; + delete s; +} + +Simple* reassign_impure(Simple* s) { + s = new Simple{2}; + return s; +} diff --git a/infer/tests/codetoanalyze/cpp/impurity/issues.exp b/infer/tests/codetoanalyze/cpp/impurity/issues.exp new file mode 100644 index 000000000..ac08013b8 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/impurity/issues.exp @@ -0,0 +1,26 @@ +../../facebook-clang-plugins/clang/install/include/c++/v1/iterator, std::__wrap_iter::operator++, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function std::__wrap_iter::operator++,parameter 'this' is modified at line 1390, column 9] +../../facebook-clang-plugins/clang/install/include/c++/v1/iterator, std::__wrap_iter::operator++, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function std::__wrap_iter::operator++,parameter 'this' is modified at line 1390, column 9] +codetoanalyze/cpp/impurity/array_test.cpp, alias_mod_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function alias_mod_impure,parameter 'array' is modified at line 33, column 3] +codetoanalyze/cpp/impurity/array_test.cpp, array_mod_both_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function array_mod_both_impure,parameter 'a' is modified at line 15, column 3,parameter 'a' is modified at line 16, column 3] +codetoanalyze/cpp/impurity/array_test.cpp, array_mod_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function array_mod_impure,parameter 'b' is modified at line 10, column 3,parameter 'a' is modified at line 9, column 3] +codetoanalyze/cpp/impurity/array_test.cpp, call_array_mod_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function call_array_mod_impure,parameter 'a' is modified when calling `array_mod_impure()()` at line 22, column 3,parameter 'a' is modified at line 9, column 3] +codetoanalyze/cpp/impurity/array_test.cpp, modify_direct_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_direct_impure,parameter 'array' is modified at line 40, column 60] +codetoanalyze/cpp/impurity/array_test.cpp, modify_ptr_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_ptr_impure,parameter 'array' is modified at line 44, column 3] +codetoanalyze/cpp/impurity/global_test.cpp, call_modify_global, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function call_modify_global,global var 'a' is modified when calling `modify_global_array_impure()()` at line 16, column 3,global var 'a' is modified at line 12, column 37,global var 'x' is modified when calling `modify_global_primitive_impure()()` at line 15, column 3,global var 'x' is modified at line 10, column 41] +codetoanalyze/cpp/impurity/global_test.cpp, local_static_var_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function local_static_var_impure,global var 'local_static_var_impure.arr' is modified at line 26, column 3,global var 'local_static_var_impure.arr' is modified at line 27, column 3] +codetoanalyze/cpp/impurity/global_test.cpp, modify_global_array_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_global_array_impure,global var 'a' is modified at line 12, column 37] +codetoanalyze/cpp/impurity/global_test.cpp, modify_global_inside_lamda_impure::lambda_global_test.cpp:33:14::operator(), 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_global_inside_lamda_impure::lambda_global_test.cpp:33:14::operator(),global var 'x' is modified at line 33, column 22] +codetoanalyze/cpp/impurity/global_test.cpp, modify_global_primitive_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_global_primitive_impure,global var 'x' is modified at line 10, column 41] +codetoanalyze/cpp/impurity/invalid_test.cpp, delete_param_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function delete_param_impure,parameter 's',was invalidated by `delete` here] +codetoanalyze/cpp/impurity/invalid_test.cpp, double_free_global_impure_FN, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `free_global_pointer_impure()` here,memory was invalidated by call to `free()` here,use-after-lifetime part of the trace starts here,when calling `free_global_pointer_impure()` here,invalid access occurs here] +codetoanalyze/cpp/impurity/invalid_test.cpp, free_global_pointer_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function free_global_pointer_impure,global var 'global_pointer',was invalidated by call to `free()` here] +codetoanalyze/cpp/impurity/invalid_test.cpp, free_param_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function free_param_impure,parameter 'x',was invalidated by call to `free()` here] +codetoanalyze/cpp/impurity/invalid_test.cpp, reassign_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function reassign_impure,parameter 's' is modified at line 34, column 3] +codetoanalyze/cpp/impurity/param_test.cpp, create_cycle_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function create_cycle_impure,parameter 'x' is modified at line 23, column 44] +codetoanalyze/cpp/impurity/param_test.cpp, invalidate_local_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function invalidate_local_impure,parameter 'pp' is modified at line 27, column 3] +codetoanalyze/cpp/impurity/param_test.cpp, modify_mut_ref_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_mut_ref_impure,parameter 'x' is modified at line 8, column 38] +codetoanalyze/cpp/impurity/vector.cpp, assign_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function assign_impure,parameter 'vec' is modified at line 29, column 45] +codetoanalyze/cpp/impurity/vector.cpp, clear_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function clear_impure,parameter 'vec' is modified at line 26, column 44] +codetoanalyze/cpp/impurity/vector.cpp, insert_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function insert_impure,parameter 'vec' is modified at line 8, column 45] +codetoanalyze/cpp/impurity/vector.cpp, push_back_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function push_back_impure,parameter 'vec' is modified at line 10, column 48] +codetoanalyze/cpp/impurity/vector.cpp, push_back_in_loop_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function push_back_in_loop_impure,parameter 'vec' is modified at line 21, column 5] diff --git a/infer/tests/codetoanalyze/cpp/impurity/param_test.cpp b/infer/tests/codetoanalyze/cpp/impurity/param_test.cpp new file mode 100644 index 000000000..3fceb5653 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/impurity/param_test.cpp @@ -0,0 +1,28 @@ +/* + * 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. + */ +// modifies x (a mutable reference argument) +void modify_mut_ref_impure(int* x) { ++*x; } + +int primitive_pure(int x) { x++; } + +int fact_pure(int n) { + int f = 1; + while (n > 0) + f *= n--; + return f; +} + +struct node { + struct node* next; + int data; +}; +void create_cycle_impure(struct node* x) { x->next = x; } + +void invalidate_local_impure(int** pp) { + int t = 0xdeadbeef; + *pp = &t; // <-- potential bug here since t goes out of scope +} diff --git a/infer/tests/codetoanalyze/cpp/impurity/unmodeled.cpp b/infer/tests/codetoanalyze/cpp/impurity/unmodeled.cpp new file mode 100644 index 000000000..3ab8dc7b6 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/impurity/unmodeled.cpp @@ -0,0 +1,11 @@ +/* + * 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. + */ +#include + +void output_stream_impure_FN() { std::cout << "Hello, world!" << std::endl; } + +int random_impure_FN() { std::rand(); } diff --git a/infer/tests/codetoanalyze/cpp/impurity/vector.cpp b/infer/tests/codetoanalyze/cpp/impurity/vector.cpp new file mode 100644 index 000000000..4903f259c --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/impurity/vector.cpp @@ -0,0 +1,41 @@ +/* + * 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. + */ +#include +void insert_impure(std::vector& vec) { vec.insert(vec.begin(), 2); } + +void push_back_impure(std::vector& vec) { vec.push_back(32); } + +void fresh_push_back_pure() { + std::vector vec = {0, 0}; + push_back_impure(vec); +} + +// modifies vec +void push_back_in_loop_impure(std::vector& vec, + std::vector& vec_other) { + for (const auto& i : vec_other) { + vec.push_back(i); + } +} + +// modifies vec +void clear_impure(std::vector& vec) { vec.clear(); } + +// modifies vec +void assign_impure(std::vector& vec) { vec.assign(11, 7); } + +struct A { + int i; +}; + +// iterators are not modeled in pulse yet +int set_zero_impure_FN(std::vector& numbers) { + for (auto& num : numbers) { + num.i = 0; + } + return 0; +}