From 9e4036cf2f33b1aff7b976488c61a0dad5da1fc3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Tue, 1 Dec 2020 01:33:34 -0800 Subject: [PATCH] [impurity] Change Var to Pvar Summary: We always add Pvars to impurity domain. So let's simplify the domain to make it explicit. Reviewed By: ngorogiannis Differential Revision: D25220214 fbshipit-source-id: 4dc9bce4c --- infer/src/checkers/impurity.ml | 24 ++++++++++++++---------- infer/src/checkers/impurityDomain.ml | 12 +++++++----- infer/src/checkers/impurityDomain.mli | 2 +- 3 files changed, 22 insertions(+), 16 deletions(-) diff --git a/infer/src/checkers/impurity.ml b/infer/src/checkers/impurity.ml index ed2c4fe2b..0eba1972f 100644 --- a/infer/src/checkers/impurity.ml +++ b/infer/src/checkers/impurity.ml @@ -42,7 +42,8 @@ let ignore_array_index (access : BaseMemory.Access.t) : unit HilExp.Access.t = TakeAddress -let add_invalid_and_modified ~var ~access ~check_empty attrs acc : ImpurityDomain.ModifiedVarSet.t = +let add_invalid_and_modified ~pvar ~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]) @@ -59,11 +60,11 @@ let add_invalid_and_modified ~var ~access ~check_empty attrs acc : ImpurityDomai else List.fold_left ~init:acc ~f:(fun acc trace -> - ImpurityDomain.ModifiedVarSet.add {var; access= ignore_array_index access; trace} acc ) + ImpurityDomain.ModifiedVarSet.add {pvar; access= ignore_array_index access; trace} acc ) invalid_and_modified -let add_to_modified ~var ~access ~addr pre_heap post modified_vars = +let add_to_modified ~pvar ~access ~addr pre_heap post modified_vars = let rec aux modified_vars ~addr_to_explore ~visited : ImpurityDomain.ModifiedVarSet.t = match addr_to_explore with | [] -> @@ -82,18 +83,19 @@ let add_to_modified ~var ~access ~addr pre_heap post modified_vars = "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 ~var ~access ~check_empty:false attrs_post modified_vars) + (add_invalid_and_modified ~pvar ~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 ~var ~access attrs_post ~check_empty:false + (add_invalid_and_modified ~pvar ~access attrs_post ~check_empty:false modified_vars) ~addr_to_explore:(addr_list @ addr_to_explore) ~visited | None -> aux - (add_invalid_and_modified ~var ~access ~check_empty:true attrs_post modified_vars) + (add_invalid_and_modified ~pvar ~access ~check_empty:true attrs_post + modified_vars) ~addr_to_explore ~visited ) ) in aux modified_vars ~addr_to_explore:[(access, addr)] ~visited:AbstractValue.Set.empty @@ -101,13 +103,13 @@ let add_to_modified ~var ~access ~addr pre_heap post modified_vars = let get_modified_params pname post_stack pre_heap post formals = List.fold_left formals ~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 + let pvar = Pvar.mk name pname in + match BaseStack.find_opt (Var.of_pvar pvar) post_stack with | Some (addr, _) when Typ.is_pointer typ -> ( match BaseMemory.find_opt addr pre_heap with | Some edges_pre -> BaseMemory.Edges.fold edges_pre ~init:acc ~f:(fun acc (access, (addr, _)) -> - add_to_modified ~var ~access ~addr pre_heap post acc ) + add_to_modified ~pvar ~access ~addr pre_heap post acc ) | None -> debug "The address is not materialized in in pre-heap." ; acc ) @@ -122,7 +124,9 @@ let get_modified_globals pre_heap post post_stack = (* 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 + add_to_modified + ~pvar:(Option.value_exn (Var.get_pvar var)) + ~access:HilExp.Access.Dereference ~addr pre_heap post modified_globals else modified_globals ) post_stack ImpurityDomain.ModifiedVarSet.empty diff --git a/infer/src/checkers/impurityDomain.ml b/infer/src/checkers/impurityDomain.ml index 91c2cf950..35ccd81ca 100644 --- a/infer/src/checkers/impurityDomain.ml +++ b/infer/src/checkers/impurityDomain.ml @@ -12,11 +12,13 @@ module SkippedCalls = PulseSkippedCalls type trace = WrittenTo of PulseTrace.t | Invalid of (PulseInvalidation.t * PulseTrace.t) [@@deriving compare] +let pp_pvar fmt pv = F.pp_print_string fmt (Pvar.get_simplified_name pv) + module ModifiedVar = struct - type t = {var: Var.t; access: unit HilExp.Access.t; trace: trace [@compare.ignore]} + type t = {pvar: Pvar.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 + let pp fmt {pvar} = F.fprintf fmt "@\n %a @\n" pp_pvar pvar end module ModifiedVarSet = AbstractDomain.FiniteSet (ModifiedVar) @@ -65,16 +67,16 @@ let pp_param_source fmt = function F.pp_print_string fmt "global variable" -let add_to_errlog ~nesting param_source ModifiedVar.{var; trace} errlog = +let add_to_errlog ~nesting param_source ModifiedVar.{pvar; 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 ) + F.fprintf fmt "%a `%a` modified here" pp_param_source param_source pp_pvar pvar ) 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 + F.fprintf fmt "%a `%a` %a here" pp_param_source param_source pp_pvar pvar PulseInvalidation.describe invalidation ) invalidation_trace errlog diff --git a/infer/src/checkers/impurityDomain.mli b/infer/src/checkers/impurityDomain.mli index b5e91ecd3..2fa2a01e0 100644 --- a/infer/src/checkers/impurityDomain.mli +++ b/infer/src/checkers/impurityDomain.mli @@ -10,7 +10,7 @@ type trace = WrittenTo of PulseTrace.t | Invalid of (PulseInvalidation.t * Pulse module ModifiedVar : sig type t = - { var: Var.t + { pvar: Pvar.t ; access: unit HilExp.Access.t (** accesses that are oblivious to modified array indices *) ; trace: trace } end