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]