[impurity] Track unique accesses

Summary:
Impurity domain was tracking all changes to variables (with a list of traces that containing all write/invalid accesses). This results in having long traces with multiple access events for the same variable. For instance,

```
 void swap_impure(int[] array, int i, int j) {
    int tmp = array[i];
    array[i] = array[j]; \\ included in the trace
    array[j] = tmp;      \\ included in the trace
  }
```
here we recorded both array accesses.

This diff changes the domain to include accesses so that we only keep track of a single trace per access. Array accesses are only recorded once.

Note that we want to record all unique accesses, not just the first one, because impurity will be used for hoisting/cost where we will invalidate impure arguments and consider all the rest as not changing.

Reviewed By: jvillard

Differential Revision: D20385745

fbshipit-source-id: d3647dad3

infer/src/checkers/impurity.ml

@@ -12,12 +12,13 @@ open PulseDomainInterface
 
 let debug fmt = L.(debug Analysis Verbose fmt)
 
-let get_matching_dest_addr_opt ~edges_pre ~edges_post : AbstractValue.t list option =
+let get_matching_dest_addr_opt ~edges_pre ~edges_post :
+    (BaseMemory.Access.t * AbstractValue.t) list option =
   match
     List.fold2 ~init:(Some [])
-      ~f:(fun acc (_, (addr_dest_pre, _)) (_, (addr_dest_post, _)) ->
+      ~f:(fun acc (access, (addr_dest_pre, _)) (_, (addr_dest_post, _)) ->
         if AbstractValue.equal addr_dest_pre addr_dest_post then
-          Option.map acc ~f:(fun acc -> addr_dest_pre :: acc)
+          Option.map acc ~f:(fun acc -> (access, addr_dest_pre) :: acc)
         else None )
       (BaseMemory.Edges.bindings edges_pre)
       (BaseMemory.Edges.bindings edges_post)
@@ -29,7 +30,19 @@ let get_matching_dest_addr_opt ~edges_pre ~edges_post : AbstractValue.t list opt
       x
 
 
-let add_invalid_and_modified ~check_empty attrs acc =
+let ignore_array_index (access : BaseMemory.Access.t) : unit HilExp.Access.t =
+  match access with
+  | ArrayAccess (typ, _) ->
+      ArrayAccess (typ, ())
+  | FieldAccess fname ->
+      FieldAccess fname
+  | Dereference ->
+      Dereference
+  | TakeAddress ->
+      TakeAddress
+
+
+let add_invalid_and_modified ~var ~access ~check_empty attrs acc : ImpurityDomain.ModifiedVarSet.t =
   let modified =
     Attributes.get_written_to attrs
     |> Option.value_map ~default:[] ~f:(fun modified -> [ImpurityDomain.WrittenTo modified])
@@ -43,46 +56,47 @@ let add_invalid_and_modified ~check_empty attrs acc =
   in
   if check_empty && List.is_empty invalid_and_modified then
     L.(die InternalError) "Address is modified without being written to or invalidated."
-  else invalid_and_modified @ acc
+  else
+    List.fold_left ~init:acc
+      ~f:(fun acc trace ->
+        ImpurityDomain.ModifiedVarSet.add {var; access= ignore_array_index access; trace} acc )
+      invalid_and_modified
 
 
-let add_to_modified var addr pre_heap post acc =
-  let rec aux acc ~addr_to_explore ~visited : ImpurityDomain.trace list =
+let add_to_modified ~var ~access ~addr pre_heap post modified_vars =
+  let rec aux modified_vars ~addr_to_explore ~visited : ImpurityDomain.ModifiedVarSet.t =
     match addr_to_explore with
     | [] ->
-        acc
-    | addr :: addr_to_explore -> (
-        if AbstractValue.Set.mem addr visited then aux acc ~addr_to_explore ~visited
+        modified_vars
+    | (access, addr) :: addr_to_explore -> (
+        if AbstractValue.Set.mem addr visited then aux modified_vars ~addr_to_explore ~visited
         else
           let edges_pre_opt = BaseMemory.find_opt addr pre_heap in
           let cell_post_opt = BaseDomain.find_cell_opt addr post in
           let visited = AbstractValue.Set.add addr visited in
           match (edges_pre_opt, cell_post_opt) with
           | None, None ->
-              aux acc ~addr_to_explore ~visited
+              aux modified_vars ~addr_to_explore ~visited
           | Some _, None ->
               L.(die InternalError)
                 "It is unexpected to have an address which has a binding in pre but not in post!"
           | None, Some (_, attrs_post) ->
               aux
-                (add_invalid_and_modified ~check_empty:false attrs_post acc)
+                (add_invalid_and_modified ~var ~access ~check_empty:false attrs_post modified_vars)
                 ~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)
+                  (add_invalid_and_modified ~var ~access attrs_post ~check_empty:false
+                     modified_vars)
                   ~addr_to_explore:(addr_list @ addr_to_explore) ~visited
             | None ->
                 aux
-                  (add_invalid_and_modified ~check_empty:true attrs_post acc)
+                  (add_invalid_and_modified ~var ~access ~check_empty:true attrs_post modified_vars)
                   ~addr_to_explore ~visited ) )
   in
-  match aux [] ~addr_to_explore:[addr] ~visited:AbstractValue.Set.empty with
-  | [] ->
-      acc
-  | hd :: tl ->
-      ImpurityDomain.ModifiedVarSet.add {var; trace_list= (hd, tl)} acc
+  aux modified_vars ~addr_to_explore:[(access, addr)] ~visited:AbstractValue.Set.empty
 
 
 let get_modified_params pname post_stack pre_heap post formals =
@@ -93,15 +107,35 @@ let get_modified_params pname post_stack pre_heap post formals =
         match BaseMemory.find_opt addr pre_heap with
         | Some edges_pre ->
             BaseMemory.Edges.fold
-              (fun _ (addr, _) acc -> add_to_modified var addr pre_heap post acc)
+              (fun access (addr, _) acc -> add_to_modified ~var ~access ~addr pre_heap post acc)
               edges_pre acc
         | None ->
-            debug "The address is not materialized in pre-heap." ;
+            debug "The address is not materialized in in pre-heap." ;
             acc )
       | _ ->
           acc )
 
 
+let get_modified_globals pre_heap post post_stack =
+  BaseStack.fold
+    (fun var (addr, _) modified_globals ->
+      if Var.is_global var then
+        (* since global vars are rooted in the stack, we don't have
+           access here but we still want to pick up changes to
+           globals. *)
+        add_to_modified ~var ~access:HilExp.Access.Dereference ~addr pre_heap post modified_globals
+      else modified_globals )
+    post_stack ImpurityDomain.ModifiedVarSet.empty
+
+
+let is_modeled_pure tenv pname =
+  match PurityModels.ProcName.dispatch tenv pname with
+  | Some callee_summary ->
+      PurityDomain.is_pure callee_summary
+  | None ->
+      false
+
+
 (** Given Pulse summary, extract impurity info, i.e. parameters and global variables that are
     modified by the function and skipped functions. *)
 let extract_impurity tenv pdesc pre_post : ImpurityDomain.t =
@@ -112,23 +146,11 @@ let extract_impurity tenv pdesc pre_post : ImpurityDomain.t =
   let modified_params =
     Procdesc.get_formals pdesc |> get_modified_params pname post_stack pre_heap post
   in
-  let modified_globals =
-    BaseStack.fold
-      (fun var (addr, _) acc ->
-        if Var.is_global var then add_to_modified var addr pre_heap post acc else acc )
-      post_stack ImpurityDomain.ModifiedVarSet.empty
-  in
-  let is_modeled_pure pname =
-    match PurityModels.ProcName.dispatch tenv pname with
-    | Some callee_summary ->
-        PurityDomain.is_pure callee_summary
-    | None ->
-        false
-  in
+  let modified_globals = get_modified_globals pre_heap post post_stack in
   let skipped_calls =
     AbductiveDomain.extract_skipped_calls pre_post
     |> PulseAbductiveDomain.SkippedCalls.filter (fun proc_name _ ->
-           Purity.should_report proc_name && not (is_modeled_pure proc_name) )
+           Purity.should_report proc_name && not (is_modeled_pure tenv proc_name) )
   in
   {modified_globals; modified_params; skipped_calls}
 

infer/src/checkers/impurityDomain.ml

@@ -13,9 +13,8 @@ type trace = WrittenTo of PulseTrace.t | Invalid of (PulseInvalidation.t * Pulse
 [@@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]
+  type t = {var: Var.t; access: unit HilExp.Access.t; trace: trace [@compare.ignore]}
+  [@@deriving compare]
 
   let pp fmt {var} = F.fprintf fmt "@\n %a @\n" Var.pp var
 end
@@ -61,20 +60,16 @@ let pp_param_source fmt = function
       F.pp_print_string fmt "global variable"
 
 
-let add_to_errlog ~nesting param_source ModifiedVar.{var; trace_list} errlog =
-  let aux ~nesting errlog trace =
-    match trace with
-    | WrittenTo access_trace ->
-        PulseTrace.add_to_errlog ~include_value_history:false ~nesting
-          ~pp_immediate:(fun fmt ->
-            F.fprintf fmt "%a `%a` modified here" pp_param_source param_source Var.pp var )
-          access_trace errlog
-    | Invalid (invalidation, invalidation_trace) ->
-        PulseTrace.add_to_errlog ~include_value_history:false ~nesting
-          ~pp_immediate:(fun fmt ->
-            F.fprintf fmt "%a `%a` %a here" pp_param_source param_source Var.pp var
-              PulseInvalidation.describe invalidation )
-          invalidation_trace errlog
-  in
-  let first_trace, rest = trace_list in
-  List.fold_left rest ~init:(aux ~nesting errlog first_trace) ~f:(aux ~nesting)
+let add_to_errlog ~nesting param_source ModifiedVar.{var; trace} errlog =
+  match trace with
+  | WrittenTo access_trace ->
+      PulseTrace.add_to_errlog ~include_value_history:false ~nesting
+        ~pp_immediate:(fun fmt ->
+          F.fprintf fmt "%a `%a` modified here" pp_param_source param_source Var.pp var )
+        access_trace errlog
+  | Invalid (invalidation, invalidation_trace) ->
+      PulseTrace.add_to_errlog ~include_value_history:false ~nesting
+        ~pp_immediate:(fun fmt ->
+          F.fprintf fmt "%a `%a` %a here" pp_param_source param_source Var.pp var
+            PulseInvalidation.describe invalidation )
+        invalidation_trace errlog

infer/src/checkers/impurityDomain.mli

@@ -9,9 +9,10 @@ open! IStd
 type trace = WrittenTo of PulseTrace.t | Invalid of (PulseInvalidation.t * PulseTrace.t)
 
 module ModifiedVar : sig
-  type nonempty_action_type = trace * trace list
-
-  type t = {var: Var.t; trace_list: nonempty_action_type}
+  type t =
+    { var: Var.t
+    ; access: unit HilExp.Access.t  (** accesses that are oblivious to modified array indices *)
+    ; trace: trace }
 end
 
 module ModifiedVarSet : sig

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

@@ -3,13 +3,13 @@
 ../../facebook-clang-plugins/clang/install/include/c++/v1/iterator, std::operator!=<A_*>, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function std::operator!=<A_*>,when calling `std::operator==<A_*,_A_*>` here,parameter `__x` modified here,when calling `std::operator==<A_*,_A_*>` here,parameter `__y` modified here]
 ../../facebook-clang-plugins/clang/install/include/c++/v1/iterator, std::operator!=<int_*>, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function std::operator!=<int_*>,when calling `std::operator==<int_*,_int_*>` here,parameter `__x` modified here,when calling `std::operator==<int_*,_int_*>` here,parameter `__y` modified here]
 codetoanalyze/cpp/impurity/array_test.cpp, alias_mod_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function alias_mod_impure,parameter `array` modified here]
-codetoanalyze/cpp/impurity/array_test.cpp, array_mod_both_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function array_mod_both_impure,parameter `a` modified here,parameter `a` modified here]
+codetoanalyze/cpp/impurity/array_test.cpp, array_mod_both_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function array_mod_both_impure,parameter `a` modified here]
 codetoanalyze/cpp/impurity/array_test.cpp, array_mod_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function array_mod_impure,parameter `b` modified here,parameter `a` modified here]
 codetoanalyze/cpp/impurity/array_test.cpp, call_array_mod_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function call_array_mod_impure,when calling `array_mod_impure` here,parameter `a` modified here]
 codetoanalyze/cpp/impurity/array_test.cpp, modify_direct_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_direct_impure,parameter `array` modified here]
 codetoanalyze/cpp/impurity/array_test.cpp, modify_ptr_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_ptr_impure,parameter `array` modified here]
 codetoanalyze/cpp/impurity/global_test.cpp, call_modify_global, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function call_modify_global,when calling `modify_global_array_impure` here,global variable `a` modified here,when calling `modify_global_primitive_impure` here,global variable `x` modified here]
-codetoanalyze/cpp/impurity/global_test.cpp, local_static_var_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function local_static_var_impure,global variable `local_static_var_impure.arr` modified here,global variable `local_static_var_impure.arr` modified here]
+codetoanalyze/cpp/impurity/global_test.cpp, local_static_var_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function local_static_var_impure,global variable `local_static_var_impure.arr` modified here]
 codetoanalyze/cpp/impurity/global_test.cpp, modify_global_array_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_global_array_impure,global variable `a` modified here]
 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 variable `x` modified here]
 codetoanalyze/cpp/impurity/global_test.cpp, modify_global_primitive_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_global_primitive_impure,global variable `x` modified here]

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

@@ -9,8 +9,8 @@ codetoanalyze/java/impurity/Localities.java, Localities.copy_ref_impure(int[],in
 codetoanalyze/java/impurity/Localities.java, Localities.get_array_impure(Localities$Foo[],int,Localities$Foo):Localities$Foo[], 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function Localities$Foo[] Localities.get_array_impure(Localities$Foo[],int,Localities$Foo),parameter `array` modified here]
 codetoanalyze/java/impurity/Localities.java, Localities.get_f_impure(Localities$Foo[],int,Localities$Foo):Localities$Foo, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function Localities$Foo Localities.get_f_impure(Localities$Foo[],int,Localities$Foo),parameter `array` modified here]
 codetoanalyze/java/impurity/Localities.java, Localities.get_foo_via_tmp_impure(Localities$Foo[],int,Localities$Foo,Localities$Foo):Localities$Bar, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function Localities$Bar Localities.get_foo_via_tmp_impure(Localities$Foo[],int,Localities$Foo,Localities$Foo),parameter `array` modified here]
-codetoanalyze/java/impurity/Localities.java, Localities.incrementAll_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities.incrementAll_impure(ArrayList),when calling `void Localities$Foo.inc_impure()` here,parameter `list` modified here,when calling `void Localities$Foo.inc_impure()` here,parameter `list` modified here,when calling `void Localities$Foo.inc_impure()` here,parameter `list` modified here]
-codetoanalyze/java/impurity/Localities.java, Localities.makeAllZero_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities.makeAllZero_impure(ArrayList),parameter `list` modified here,parameter `list` modified here,parameter `list` modified here]
+codetoanalyze/java/impurity/Localities.java, Localities.incrementAll_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities.incrementAll_impure(ArrayList),when calling `void Localities$Foo.inc_impure()` here,parameter `list` modified here]
+codetoanalyze/java/impurity/Localities.java, Localities.makeAllZero_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities.makeAllZero_impure(ArrayList),parameter `list` modified here]
 codetoanalyze/java/impurity/Localities.java, Localities.modify_first_el_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities.modify_first_el_impure(ArrayList),parameter `list` modified here]
 codetoanalyze/java/impurity/Localities.java, Localities.modify_via_call_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities.modify_via_call_impure(ArrayList),when calling `void Localities$Foo.inc_impure()` here,parameter `list` modified here]
 codetoanalyze/java/impurity/Localities.java, Localities.newHashCode_impure():int, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function int Localities.newHashCode_impure(),call to skipped function int Object.hashCode() occurs here]
@@ -31,5 +31,5 @@ codetoanalyze/java/impurity/Test.java, Test.global_array_set_impure(int,int):voi
 codetoanalyze/java/impurity/Test.java, Test.local_field_write_impure(Test):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.local_field_write_impure(Test),parameter `x` modified here]
 codetoanalyze/java/impurity/Test.java, Test.parameter_field_write_impure(Test,boolean):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.parameter_field_write_impure(Test,boolean),parameter `test` modified here]
 codetoanalyze/java/impurity/Test.java, Test.set_impure(int,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.set_impure(int,int),parameter `this` modified here]
-codetoanalyze/java/impurity/Test.java, Test.swap_impure(int[],int,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.swap_impure(int[],int,int),parameter `array` modified here,parameter `array` modified here]
+codetoanalyze/java/impurity/Test.java, Test.swap_impure(int[],int,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.swap_impure(int[],int,int),parameter `array` modified here]
 codetoanalyze/java/impurity/Test.java, Test.systemNanoTime_impure():long, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function long Test.systemNanoTime_impure(),call to skipped function long System.nanoTime() occurs here]