[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

@@ -62,6 +62,7 @@ DIRECT_TESTS += \
   cpp_conflicts \
   cpp_errors \
   cpp_frontend \
+  cpp_impurity \
   cpp_linters \
   cpp_linters-for-test-only \
   cpp_liveness \

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:

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:

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

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:

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

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

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

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

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"

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

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

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)

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

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
 

infer/src/checkers/purity.mli

@@ -8,3 +8,5 @@
 open! IStd
 
 val checker : Callbacks.proc_callback_t
+
+val should_report : Procdesc.t -> bool

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=

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)

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

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

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)

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

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

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 <stdlib.h>
+
+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;
+}

infer/tests/codetoanalyze/cpp/impurity/issues.exp

@@ -0,0 +1,26 @@
+../../facebook-clang-plugins/clang/install/include/c++/v1/iterator, std::__wrap_iter<A*>::operator++, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function std::__wrap_iter<A*>::operator++,parameter 'this' is modified at line 1390, column 9]
+../../facebook-clang-plugins/clang/install/include/c++/v1/iterator, std::__wrap_iter<int*>::operator++, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function std::__wrap_iter<int*>::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]

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

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 <iostream>
+
+void output_stream_impure_FN() { std::cout << "Hello, world!" << std::endl; }
+
+int random_impure_FN() { std::rand(); }

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 <vector>
+void insert_impure(std::vector<int>& vec) { vec.insert(vec.begin(), 2); }
+
+void push_back_impure(std::vector<int>& vec) { vec.push_back(32); }
+
+void fresh_push_back_pure() {
+  std::vector<int> vec = {0, 0};
+  push_back_impure(vec);
+}
+
+// modifies vec
+void push_back_in_loop_impure(std::vector<int>& vec,
+                              std::vector<int>& vec_other) {
+  for (const auto& i : vec_other) {
+    vec.push_back(i);
+  }
+}
+
+// modifies vec
+void clear_impure(std::vector<int>& vec) { vec.clear(); }
+
+// modifies vec
+void assign_impure(std::vector<int>& vec) { vec.assign(11, 7); }
+
+struct A {
+  int i;
+};
+
+// iterators are not modeled in pulse yet
+int set_zero_impure_FN(std::vector<A>& numbers) {
+  for (auto& num : numbers) {
+    num.i = 0;
+  }
+  return 0;
+}