From aae17242d754a154c6fa9f8206815e834586b466 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Fri, 8 Mar 2019 10:49:20 -0800 Subject: [PATCH] [pulse] no addresses in attributes Summary: This removes the "abstract addresses" that used to be stored in the `Closure` attribute of pulse abstract addresses. There used to be a list of values recorded for each closure, each one representing one captured value. Instead these values are now recorded as fake edges in the memory graph. Having addresses appear in attributes causes issues when trying to establish graph isomorphism between two memory states. Avoid it by rewriting the closures mechanism to encode captured addresses as fake edges in memory. This way captured addresses are automatically treated right by the graph algorithms (in the next diffs). Reviewed By: mbouaziz Differential Revision: D14323044 fbshipit-source-id: 413b4d989 --- infer/src/checkers/PulseDomain.ml | 72 ++++++++++++--------------- infer/src/checkers/PulseDomain.mli | 20 ++++---- infer/src/checkers/PulseOperations.ml | 52 +++++++++++++++---- 3 files changed, 86 insertions(+), 58 deletions(-) diff --git a/infer/src/checkers/PulseDomain.ml b/infer/src/checkers/PulseDomain.ml index d9c9ae9f0..875f0f7a1 100644 --- a/infer/src/checkers/PulseDomain.ml +++ b/infer/src/checkers/PulseDomain.ml @@ -10,6 +10,33 @@ module Invalidation = PulseInvalidation (* {2 Abstract domain description } *) +(** Purposefully declared before [AbstractAddress] to avoid attributes depending on + addresses. Otherwise they become a pain to handle when comparing memory states. *) +module Attribute = struct + (* OPTIM: [Invalid _] is first in the order to make queries about invalidation status more + efficient (only need to look at the first element in the set of attributes to know if an + address is invalid) *) + type t = + (* DO NOT MOVE, see toplevel comment *) + | Invalid of Invalidation.t + | AddressOfCppTemporary of Var.t * Location.t option + | Closure of Typ.Procname.t + | StdVectorReserve + [@@deriving compare] + + let pp f = function + | Invalid invalidation -> + Invalidation.pp f invalidation + | AddressOfCppTemporary (var, location_opt) -> + F.fprintf f "&%a (%a)" Var.pp var (Pp.option Location.pp) location_opt + | Closure pname -> + F.fprintf f "%a" Typ.Procname.pp pname + | StdVectorReserve -> + F.pp_print_string f "std::vector::reserve()" +end + +module Attributes = AbstractDomain.FiniteSet (Attribute) + (** An abstract address in memory. *) module AbstractAddress : sig type t = private int [@@deriving compare] @@ -49,31 +76,6 @@ module AddrTracePair = struct else AbstractAddress.pp f (fst addr_trace) end -module Attribute = struct - (* OPTIM: [Invalid _] is first in the order to make queries about invalidation status more - efficient (only need to look at the first element in the set of attributes to know if an - address is invalid) *) - type t = - (* DO NOT MOVE, see toplevel comment *) - | Invalid of Invalidation.t - | AddressOfCppTemporary of Var.t * Location.t option - | Closure of Typ.Procname.t * AddrTracePair.t list - | StdVectorReserve - [@@deriving compare] - - let pp f = function - | Invalid invalidation -> - Invalidation.pp f invalidation - | AddressOfCppTemporary (var, location_opt) -> - F.fprintf f "&%a (%a)" Var.pp var (Pp.option Location.pp) location_opt - | Closure (pname, captured) -> - F.fprintf f "%a[%a]" Typ.Procname.pp pname (Pp.seq ~sep:"," AddrTracePair.pp) captured - | StdVectorReserve -> - F.pp_print_string f "std::vector::reserve()" -end - -module Attributes = AbstractDomain.FiniteSet (Attribute) - module Memory : sig module Access : PrettyPrintable.PrintableOrderedType with type t = AbstractAddress.t HilExp.Access.t @@ -94,6 +96,8 @@ module Memory : sig val for_all : (AbstractAddress.t -> cell -> bool) -> t -> bool + val set_cell : AbstractAddress.t -> cell -> t -> t + val pp : F.formatter -> t -> unit val add_edge : AbstractAddress.t -> Access.t -> AddrTracePair.t -> t -> t @@ -215,6 +219,8 @@ end = struct let for_all = Graph.for_all + let set_cell = Graph.add + let filter = Graph.filter end @@ -325,8 +331,8 @@ end = struct match Memory.find_opt address astate.heap with | None -> visited - | Some (edges, attrs) -> - visit_edges astate ~edges visited |> visit_attributes astate attrs ) + | Some (edges, _) -> + visit_edges astate ~edges visited ) and visit_edges ~edges astate visited = @@ -335,18 +341,6 @@ end = struct edges visited - and visit_attributes astate attrs visited = - Attributes.fold - (fun attr visited -> - match attr with - | Attribute.Invalid _ | Attribute.AddressOfCppTemporary _ | Attribute.StdVectorReserve -> - visited - | Attribute.Closure (_, captured) -> - List.fold captured ~init:visited ~f:(fun visited (address, _) -> - visit_address astate address visited ) ) - attrs visited - - let visit_stack astate visited = Stack.fold (fun _var (address, _loc) visited -> visit_address astate address visited) diff --git a/infer/src/checkers/PulseDomain.mli b/infer/src/checkers/PulseDomain.mli index 07fa7b48c..44edefb80 100644 --- a/infer/src/checkers/PulseDomain.mli +++ b/infer/src/checkers/PulseDomain.mli @@ -8,6 +8,15 @@ open! IStd module F = Format +module Attribute : sig + type t = + | Invalid of PulseInvalidation.t + | AddressOfCppTemporary of Var.t * Location.t option + | Closure of Typ.Procname.t + | StdVectorReserve + [@@deriving compare] +end + module AbstractAddress : sig type t = private int [@@deriving compare] @@ -35,15 +44,6 @@ module AddrTracePair : sig type t = AbstractAddress.t * PulseTrace.t [@@deriving compare] end -module Attribute : sig - type t = - | Invalid of PulseInvalidation.t - | AddressOfCppTemporary of Var.t * Location.t option - | Closure of Typ.Procname.t * AddrTracePair.t list - | StdVectorReserve - [@@deriving compare] -end - module Attributes : PrettyPrintable.PPSet with type elt = Attribute.t module Memory : sig @@ -60,6 +60,8 @@ module Memory : sig val find_opt : AbstractAddress.t -> t -> cell option + val set_cell : AbstractAddress.t -> cell -> t -> t + val add_edge : AbstractAddress.t -> Access.t -> AddrTracePair.t -> t -> t val add_edge_and_back_edge : AbstractAddress.t -> Access.t -> AddrTracePair.t -> t -> t diff --git a/infer/src/checkers/PulseOperations.ml b/infer/src/checkers/PulseOperations.ml index d6e106a60..0191205fc 100644 --- a/infer/src/checkers/PulseOperations.ml +++ b/infer/src/checkers/PulseOperations.ml @@ -298,17 +298,47 @@ let record_var_decl_location location var astate = module Closures = struct open Result.Monad_infix + let fake_capture_field_prefix = "__capture_" + + let mk_fake_field ~id = + Typ.Fieldname.Clang.from_class_name + (Typ.CStruct (QualifiedCppName.of_list ["std"; "function"])) + (Printf.sprintf "%s%d" fake_capture_field_prefix id) + + + let is_captured_fake_access (access : _ HilExp.Access.t) = + match access with + | FieldAccess fieldname + when String.is_prefix ~prefix:fake_capture_field_prefix (Typ.Fieldname.to_string fieldname) + -> + true + | _ -> + false + + + let mk_capture_edges captured = + let fake_fields = + List.rev_mapi captured ~f:(fun id captured_addr_trace -> + (HilExp.Access.FieldAccess (mk_fake_field ~id), captured_addr_trace) ) + in + Memory.Edges.of_seq (Caml.List.to_seq fake_fields) + + let check_captured_addresses location lambda addr astate = match Memory.find_opt addr astate.heap with | None -> Ok astate - | Some (_, attributes) -> + | Some (edges, attributes) -> IContainer.iter_result ~fold:(IContainer.fold_of_pervasives_fold ~fold:Attributes.fold) attributes ~f:(function - | Attribute.Closure (_, captured) -> - IContainer.iter_result ~fold:List.fold captured ~f:(fun addr_trace -> - check_addr_access {access_expr= lambda; location} addr_trace astate - >>| fun _ -> () ) + | Attribute.Closure _ -> + IContainer.iter_result + ~fold:(IContainer.fold_of_pervasives_map_fold ~fold:Memory.Edges.fold) edges + ~f:(fun (access, addr_trace) -> + if is_captured_fake_access access then + check_addr_access {access_expr= lambda; location} addr_trace astate + >>| fun _ -> () + else Ok () ) | _ -> Ok () ) >>| fun () -> astate @@ -320,11 +350,13 @@ module Closures = struct (closure_addr, [PulseTrace.Assignment {lhs= access_expr; location}]) astate >>| fun astate -> - { astate with - heap= - Memory.add_attributes closure_addr - (Attributes.singleton (Closure (pname, captured))) - astate.heap } + let fake_capture_edges = mk_capture_edges captured in + let heap = + Memory.set_cell closure_addr + (fake_capture_edges, Attributes.singleton (Closure pname)) + astate.heap + in + {astate with heap} let record location access_expr pname captured astate =