From a4c3925d9a8a2b8dca1e31ac5914467b481c046d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Wed, 11 Mar 2020 08:50:45 -0700 Subject: [PATCH] [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 | 92 ++++++++++++------- infer/src/checkers/impurityDomain.ml | 35 +++---- infer/src/checkers/impurityDomain.mli | 7 +- .../codetoanalyze/cpp/impurity/issues.exp | 4 +- .../codetoanalyze/java/impurity/issues.exp | 6 +- 5 files changed, 81 insertions(+), 63 deletions(-) diff --git a/infer/src/checkers/impurity.ml b/infer/src/checkers/impurity.ml index 999ad399f..e148405af 100644 --- a/infer/src/checkers/impurity.ml +++ b/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} diff --git a/infer/src/checkers/impurityDomain.ml b/infer/src/checkers/impurityDomain.ml index fd6aa5367..4811f8c87 100644 --- a/infer/src/checkers/impurityDomain.ml +++ b/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 diff --git a/infer/src/checkers/impurityDomain.mli b/infer/src/checkers/impurityDomain.mli index d5c58e725..65884a58e 100644 --- a/infer/src/checkers/impurityDomain.mli +++ b/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 diff --git a/infer/tests/codetoanalyze/cpp/impurity/issues.exp b/infer/tests/codetoanalyze/cpp/impurity/issues.exp index 3f6f0571b..b1646de4f 100644 --- a/infer/tests/codetoanalyze/cpp/impurity/issues.exp +++ b/infer/tests/codetoanalyze/cpp/impurity/issues.exp @@ -3,13 +3,13 @@ ../../facebook-clang-plugins/clang/install/include/c++/v1/iterator, std::operator!=, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function std::operator!=,when calling `std::operator==` here,parameter `__x` modified here,when calling `std::operator==` here,parameter `__y` modified here] ../../facebook-clang-plugins/clang/install/include/c++/v1/iterator, std::operator!=, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function std::operator!=,when calling `std::operator==` here,parameter `__x` modified here,when calling `std::operator==` 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] diff --git a/infer/tests/codetoanalyze/java/impurity/issues.exp b/infer/tests/codetoanalyze/java/impurity/issues.exp index 0709a2cb2..8ffcf5b2d 100644 --- a/infer/tests/codetoanalyze/java/impurity/issues.exp +++ b/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]