From ddd09b83fd41d81a92ce77420249cbde891d762e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Mon, 9 Mar 2020 08:57:57 -0700 Subject: [PATCH] [impurity] Refactor and ignore invalidations to constant dereferences Summary: - ignore `ConstantDereference` invalidations since they just represent assignments to constants. - add `impurity.mli` - split `extract_impurity` into several sub functions. Reviewed By: jvillard Differential Revision: D20335674 fbshipit-source-id: f0fd6b5f4 --- infer/src/checkers/impurity.ml | 130 ++++++++++++++++---------------- infer/src/checkers/impurity.mli | 11 +++ 2 files changed, 78 insertions(+), 63 deletions(-) create mode 100644 infer/src/checkers/impurity.mli diff --git a/infer/src/checkers/impurity.ml b/infer/src/checkers/impurity.ml index a753db5d6..8f10f6b25 100644 --- a/infer/src/checkers/impurity.ml +++ b/infer/src/checkers/impurity.ml @@ -12,9 +12,6 @@ open PulseDomainInterface let debug fmt = L.(debug Analysis Verbose fmt) -(* An impurity analysis that relies on pulse to determine how the state - changes *) - let get_matching_dest_addr_opt ~edges_pre ~edges_post : AbstractValue.t list option = match List.fold2 ~init:(Some []) @@ -37,14 +34,72 @@ let add_invalid_and_modified ~check_empty attrs acc = 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 ) + let invalid_and_modified = + match Attributes.get_invalid attrs with + | None | Some (PulseInvalidation.ConstantDereference _, _) -> + modified + | Some invalid -> + ImpurityDomain.Invalid invalid :: modified in - if check_empty && List.is_empty res then + if check_empty && List.is_empty invalid_and_modified then L.(die InternalError) "Address is modified without being written to or invalidated." - else res @ acc + else invalid_and_modified @ acc + + +let add_to_modified var addr pre_heap post acc = + let rec aux acc ~addr_to_explore ~visited : ImpurityDomain.trace list = + match addr_to_explore with + | [] -> + acc + | addr :: addr_to_explore -> ( + if AbstractValue.Set.mem addr visited then aux acc ~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 + | 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) + ~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:AbstractValue.Set.empty with + | [] -> + acc + | hd :: tl -> + ImpurityDomain.ModifiedVarSet.add {var; trace_list= (hd, tl)} acc + + +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 + | Some (addr, _) when Typ.is_pointer typ -> ( + 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) + edges_pre acc + | None -> + debug "The address is not materialized in pre-heap." ; + acc ) + | _ -> + acc ) (** Given Pulse summary, extract impurity info, i.e. parameters and global variables that are @@ -53,65 +108,14 @@ let extract_impurity tenv pdesc pre_post : ImpurityDomain.t = let pre_heap = (AbductiveDomain.extract_pre pre_post).BaseDomain.heap in let post = AbductiveDomain.extract_post pre_post in let post_stack = post.BaseDomain.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 AbstractValue.Set.mem addr visited then aux acc ~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 - | 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) - ~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:AbstractValue.Set.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 -> ( - match BaseMemory.find_opt addr pre_heap with - | Some edges_pre -> - BaseMemory.Edges.fold - (fun _ (addr, _) acc -> add_to_modified var addr acc) - edges_pre acc - | None -> - debug "The address is not materialized in pre-heap." ; - acc ) - | _ -> - acc ) + 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 acc else acc) + (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 = diff --git a/infer/src/checkers/impurity.mli b/infer/src/checkers/impurity.mli new file mode 100644 index 000000000..c7cb1de60 --- /dev/null +++ b/infer/src/checkers/impurity.mli @@ -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. + *) + +open! IStd + +val checker : Callbacks.proc_callback_t +(** An impurity analysis that relies on pulse summaries to determine how the state changes *)