From 485b9c7bf5548c821067ff5e87f2dedef0651a22 Mon Sep 17 00:00:00 2001 From: Daiva Naudziuniene Date: Thu, 29 Nov 2018 07:40:09 -0800 Subject: [PATCH] [pulse] Abstract Location Set Summary: Instead of variable having the value of a single location on stack, we now allow variables to have multiple locations. Consequently, we also allow a memory location to point to a set of locations in the heap. We enforce a limit on a maximum number of locations in a set (currently 5). Reviewed By: jvillard Differential Revision: D13190876 fbshipit-source-id: 5cb5ba9a6 --- infer/src/checkers/PulseDomain.ml | 169 ++++++++++++------ infer/src/checkers/PulseDomain.mli | 10 +- .../tests/codetoanalyze/cpp/pulse/issues.exp | 1 - .../cpp/pulse/use_after_destructor.cpp | 6 +- 4 files changed, 120 insertions(+), 66 deletions(-) diff --git a/infer/src/checkers/PulseDomain.ml b/infer/src/checkers/PulseDomain.ml index c2fa49a16..4932d107a 100644 --- a/infer/src/checkers/PulseDomain.ml +++ b/infer/src/checkers/PulseDomain.ml @@ -15,8 +15,6 @@ module Invalidation = PulseInvalidation module AbstractAddress : sig type t = private int [@@deriving compare] - val equal : t -> t -> bool - val mk_fresh : unit -> t val pp : F.formatter -> t -> unit @@ -25,8 +23,6 @@ module AbstractAddress : sig end = struct type t = int [@@deriving compare] - let equal = [%compare.equal: t] - let next_fresh = ref 1 let mk_fresh () = @@ -39,6 +35,17 @@ end = struct let init () = next_fresh := 1 end +(** Set of abstract addresses in memory. *) +module AbstractAddressSet : sig + include module type of AbstractDomain.FiniteSet (AbstractAddress) + + val mk_fresh : unit -> t +end = struct + include AbstractDomain.FiniteSet (AbstractAddress) + + let mk_fresh () = singleton (AbstractAddress.mk_fresh ()) +end + (* {3 Heap domain } *) module Attribute = struct @@ -59,7 +66,7 @@ module Attributes = AbstractDomain.FiniteSet (Attribute) module Memory : sig module Edges : module type of PrettyPrintable.MakePPMap (AccessExpression.Access) - type edges = AbstractAddress.t Edges.t + type edges = AbstractAddressSet.t Edges.t type cell = edges * Attributes.t @@ -75,13 +82,13 @@ module Memory : sig val pp : F.formatter -> t -> unit - val add_edge : AbstractAddress.t -> AccessExpression.Access.t -> AbstractAddress.t -> t -> t + val add_edge : AbstractAddress.t -> AccessExpression.Access.t -> AbstractAddressSet.t -> t -> t val add_edge_and_back_edge : - AbstractAddress.t -> AccessExpression.Access.t -> AbstractAddress.t -> t -> t + AbstractAddress.t -> AccessExpression.Access.t -> AbstractAddressSet.t -> t -> t val find_edge_opt : - AbstractAddress.t -> AccessExpression.Access.t -> t -> AbstractAddress.t option + AbstractAddress.t -> AccessExpression.Access.t -> t -> AbstractAddressSet.t option val add_attributes : AbstractAddress.t -> Attributes.t -> t -> t @@ -90,13 +97,13 @@ module Memory : sig val get_invalidation : AbstractAddress.t -> t -> Invalidation.t option (** None denotes a valid location *) - val std_vector_reserve : AbstractAddress.t -> t -> t + val std_vector_reserve : AbstractAddressSet.t -> t -> t - val is_std_vector_reserved : AbstractAddress.t -> t -> bool + val is_std_vector_reserved : AbstractAddressSet.t -> t -> bool end = struct module Edges = PrettyPrintable.MakePPMap (AccessExpression.Access) - type edges = AbstractAddress.t Edges.t + type edges = AbstractAddressSet.t Edges.t type cell = edges * Attributes.t @@ -105,7 +112,7 @@ end = struct type t = cell Graph.t let pp = - Graph.pp ~pp_value:(Pp.pair ~fst:(Edges.pp ~pp_value:AbstractAddress.pp) ~snd:Attributes.pp) + Graph.pp ~pp_value:(Pp.pair ~fst:(Edges.pp ~pp_value:AbstractAddressSet.pp) ~snd:Attributes.pp) (* {3 Helper functions to traverse the two maps at once } *) @@ -123,15 +130,19 @@ end = struct (** [Dereference] edges induce a [TakeAddress] back edge and vice-versa, because [*(&x) = &( *x ) = x]. *) - let add_edge_and_back_edge addr_src (access : AccessExpression.Access.t) addr_end memory = - let memory = add_edge addr_src access addr_end memory in + let add_edge_and_back_edge addr_src (access : AccessExpression.Access.t) addrs_end memory = + let memory = add_edge addr_src access addrs_end memory in match access with | ArrayAccess _ | FieldAccess _ -> memory | TakeAddress -> - add_edge addr_end Dereference addr_src memory + AbstractAddressSet.fold + (fun addr_end -> add_edge addr_end Dereference (AbstractAddressSet.singleton addr_src)) + addrs_end memory | Dereference -> - add_edge addr_end TakeAddress addr_src memory + AbstractAddressSet.fold + (fun addr_end -> add_edge addr_end TakeAddress (AbstractAddressSet.singleton addr_src)) + addrs_end memory let find_edge_opt addr access memory = @@ -174,12 +185,19 @@ end = struct |> Option.bind ~f:(function Attribute.Invalid invalidation -> Some invalidation | _ -> None) - let std_vector_reserve address memory = add_attribute address Attribute.StdVectorReserve memory + let std_vector_reserve addresses memory = + AbstractAddressSet.fold + (fun address -> add_attribute address Attribute.StdVectorReserve) + addresses memory - let is_std_vector_reserved address memory = - Graph.find_opt address memory |> Option.map ~f:snd - |> Option.value_map ~default:false ~f:(fun attributes -> - Attributes.mem Attribute.StdVectorReserve attributes ) + + let is_std_vector_reserved addresses memory = + AbstractAddressSet.exists + (fun address -> + Graph.find_opt address memory |> Option.map ~f:snd + |> Option.value_map ~default:false ~f:(fun attributes -> + Attributes.mem Attribute.StdVectorReserve attributes ) ) + addresses (* {3 Monomorphic {!PPMap} interface as needed } *) @@ -199,20 +217,7 @@ end own. It so happens that the join on abstract states uses the join of stacks provided by this functor followed by normalization wrt the unification found between abstract locations so it's convenient to define stacks as elements of this domain. *) -module Stack = - AbstractDomain.Map - (Var) - (struct - type t = AbstractAddress.t - - let ( <= ) ~lhs ~rhs = AbstractAddress.equal lhs rhs - - let join l1 l2 = min l1 l2 - - let widen ~prev ~next ~num_iters:_ = join prev next - - let pp = AbstractAddress.pp - end) +module Stack = AbstractDomain.Map (Var) (AbstractAddressSet) (** the domain *) type astate = {heap: Memory.t; stack: Stack.t} @@ -237,10 +242,11 @@ module Domain : AbstractDomain.S with type t = astate = struct (Option.map ~f:fst cell, Option.value_map ~default:Attributes.empty ~f:snd cell) in Memory.Edges.for_all - (fun access_lhs addr_dst -> + (fun access_lhs lhs_addr_dst -> Option.bind edges_rhs_opt ~f:(fun edges_rhs -> Memory.Edges.find_opt access_lhs edges_rhs ) - |> Option.map ~f:(AbstractAddress.equal addr_dst) + |> Option.map ~f:(fun rhs_addr_dst -> + AbstractAddressSet.( <= ) ~lhs:lhs_addr_dst ~rhs:rhs_addr_dst ) |> Option.value ~default:false ) edges_lhs && Attributes.( <= ) ~lhs:attrs_lhs ~rhs:attrs_rhs ) @@ -269,29 +275,43 @@ module Domain : AbstractDomain.S with type t = astate = struct (** just to get the correct type coercion *) let to_canonical_address subst addr = (AddressUF.find subst addr :> AbstractAddress.t) + let to_canonical_address_set subst addrs = + AbstractAddressSet.map (to_canonical_address subst) addrs + + type nonrec t = {subst: AddressUF.t; astate: t} + let max_size_of_abstract_address_set = 5 + (** adds [(src_addr, access, dst_addr)] to [union_heap] and record potential new equality that results from it in [subst] *) let union_one_edge subst src_addr access dst_addr union_heap = let src_addr = to_canonical_address subst src_addr in - let dst_addr = to_canonical_address subst dst_addr in + let dst_addr = to_canonical_address_set subst dst_addr in match (Memory.find_edge_opt src_addr access union_heap, (access : AccessExpression.Access.t)) with - | Some dst_addr', _ when AbstractAddress.equal dst_addr dst_addr' -> + | Some dst_addr', _ when phys_equal dst_addr dst_addr' -> (* same edge *) (union_heap, `No_new_equality) | _, ArrayAccess _ -> (* do not trust array accesses for now, replace the destination of the edge by a fresh location *) - ( Memory.add_edge src_addr access (AbstractAddress.mk_fresh ()) union_heap + ( Memory.add_edge src_addr access (AbstractAddressSet.mk_fresh ()) union_heap , `No_new_equality ) | None, _ -> (Memory.add_edge src_addr access dst_addr union_heap, `No_new_equality) | Some dst_addr', _ -> - (* new equality [dst_addr = dst_addr'] found *) - ignore (AddressUF.union subst dst_addr dst_addr') ; - (union_heap, `New_equality) + let addr_join = AbstractAddressSet.join dst_addr dst_addr' in + if AbstractAddressSet.cardinal addr_join > max_size_of_abstract_address_set then ( + let min_addr = AbstractAddressSet.min_elt addr_join in + AbstractAddressSet.iter + (fun addr -> ignore (AddressUF.union subst min_addr addr)) + addr_join ; + ( Memory.add_edge src_addr access + (AbstractAddressSet.singleton (to_canonical_address subst min_addr)) + union_heap + , `New_equality ) ) + else (Memory.add_edge src_addr access addr_join union_heap, `No_new_equality) module Addresses = Caml.Set.Make (AbstractAddress) @@ -303,7 +323,7 @@ module Domain : AbstractDomain.S with type t = astate = struct let visit_edge access addr_dst (visited, union_heap) = union_one_edge subst addr access addr_dst union_heap |> fst - |> visit_address subst visited heap addr_dst + |> visit_address_set subst visited heap addr_dst in Memory.find_opt addr heap |> Option.fold ~init:(visited, union_heap) ~f:(fun (visited, union_heap) (edges, attrs) -> @@ -311,12 +331,19 @@ module Domain : AbstractDomain.S with type t = astate = struct Memory.Edges.fold visit_edge edges (visited, union_heap) ) + and visit_address_set subst visited heap addrs union_heap = + AbstractAddressSet.fold + (fun addr (visited, union_heap) -> visit_address subst visited heap addr union_heap) + addrs (visited, union_heap) + + let visit_stack subst heap stack union_heap = (* start graph exploration *) let visited = Addresses.empty in let _, union_heap = Stack.fold - (fun _var addr (visited, union_heap) -> visit_address subst visited heap addr union_heap) + (fun _var addr (visited, union_heap) -> + visit_address_set subst visited heap addr union_heap ) stack (visited, union_heap) in union_heap @@ -330,9 +357,14 @@ module Domain : AbstractDomain.S with type t = astate = struct (fun _var addr1_opt addr2_opt -> Option.both addr1_opt addr2_opt |> Option.iter ~f:(fun (addr1, addr2) -> - (* stack1 says [_var = addr1] and stack2 says [_var = addr2]: unify the - addresses since they are equal to the same variable *) - ignore (AddressUF.union subst addr1 addr2) ) ; + let addr_join = AbstractAddressSet.join addr1 addr2 in + if AbstractAddressSet.cardinal addr_join > max_size_of_abstract_address_set + then + let min_addr = AbstractAddressSet.min_elt addr_join in + AbstractAddressSet.iter + (fun addr -> ignore (AddressUF.union subst min_addr addr)) + addr_join + else () ) ; (* empty result map *) None ) stack1 stack2) @@ -375,7 +407,7 @@ module Domain : AbstractDomain.S with type t = astate = struct AddressUnionSet.pp set ) in L.d_printfln "Join unified addresses:@\n@[ %a@]" pp_union_find_classes state.subst ; - let stack = Stack.map (to_canonical_address state.subst) state.astate.stack in + let stack = Stack.map (to_canonical_address_set state.subst) state.astate.stack in {heap; stack} ) else normalize {state with astate= {state.astate with heap}} end @@ -493,6 +525,12 @@ module Operations = struct Ok astate + let check_addr_access_set actor addresses astate = + AbstractAddressSet.fold + (fun addr result -> result >>= check_addr_access actor addr) + addresses (Ok astate) + + (** Walk the heap starting from [addr] and following [path]. Stop either at the element before last and return [new_addr] if [overwrite_last] is [Some new_addr], or go until the end of the path if it is [None]. Create more addresses into the heap as needed to follow the [path]. Check that each @@ -500,7 +538,7 @@ module Operations = struct let rec walk actor ~on_last addr path astate = match (path, on_last) with | [], `Access -> - Ok (astate, addr) + Ok (astate, AbstractAddressSet.singleton addr) | [], `Overwrite _ -> L.die InternalError "Cannot overwrite last address in empty path" | [a], `Overwrite new_addr -> @@ -513,12 +551,23 @@ module Operations = struct >>= fun astate -> match Memory.find_edge_opt addr a astate.heap with | None -> - let addr' = AbstractAddress.mk_fresh () in + let addr' = AbstractAddressSet.mk_fresh () in let heap = Memory.add_edge_and_back_edge addr a addr' astate.heap in let astate = {astate with heap} in - walk actor ~on_last addr' path astate + walk_set actor ~on_last addr' path astate | Some addr' -> - walk actor ~on_last addr' path astate ) + walk_set actor ~on_last addr' path astate ) + + + and walk_set actor ~on_last addrs path astate = + AbstractAddressSet.fold + (fun addr result -> + result + >>= fun (astate, addr1) -> + walk actor ~on_last addr path astate + >>= fun (astate, addr2) -> Ok (astate, AbstractAddressSet.join addr1 addr2) ) + addrs + (Ok (astate, AbstractAddressSet.empty)) let write_var var addr astate = @@ -542,12 +591,12 @@ module Operations = struct | Some addr -> (astate, addr) | None -> - let addr = AbstractAddress.mk_fresh () in + let addr = AbstractAddressSet.mk_fresh () in let stack = Stack.add access_var addr astate.stack in ({astate with stack}, addr) in let actor = {access_expr; location} in - walk actor ~on_last base_addr access_list astate + walk_set actor ~on_last base_addr access_list astate (** Use the stack and heap to walk the access path represented by the given expression down to an @@ -571,8 +620,10 @@ module Operations = struct {astate with heap= Memory.invalidate address actor astate.heap} + let mark_invalid_set actor = AbstractAddressSet.fold (mark_invalid actor) + let havoc_var var astate = - {astate with stack= Stack.add var (AbstractAddress.mk_fresh ()) astate.stack} + {astate with stack= Stack.add var (AbstractAddressSet.mk_fresh ()) astate.stack} let havoc location (access_expr : AccessExpression.t) astate = @@ -581,7 +632,7 @@ module Operations = struct havoc_var access_var astate |> Result.return | _ -> walk_access_expr - ~on_last:(`Overwrite (AbstractAddress.mk_fresh ())) + ~on_last:(`Overwrite (AbstractAddressSet.mk_fresh ())) astate access_expr location >>| fst @@ -590,7 +641,7 @@ module Operations = struct materialize_address astate access_expr location >>= fun (astate, addr) -> let actor = {access_expr; location} in - check_addr_access actor addr astate >>| fun astate -> (astate, addr) + check_addr_access_set actor addr astate >>| fun astate -> (astate, addr) let read_all location access_exprs astate = @@ -605,7 +656,7 @@ module Operations = struct let invalidate cause location access_expr astate = materialize_address astate access_expr location >>= fun (astate, addr) -> - check_addr_access {access_expr; location} addr astate >>| mark_invalid cause addr + check_addr_access_set {access_expr; location} addr astate >>| mark_invalid_set cause addr let remove_vars vars astate = diff --git a/infer/src/checkers/PulseDomain.mli b/infer/src/checkers/PulseDomain.mli index 707302962..21fe4c37a 100644 --- a/infer/src/checkers/PulseDomain.mli +++ b/infer/src/checkers/PulseDomain.mli @@ -15,6 +15,10 @@ end include AbstractDomain.S +module AbstractAddressSet : sig + type t +end + val initial : t module Diagnostic : sig @@ -37,7 +41,7 @@ module StdVector : sig val mark_reserved : Location.t -> AccessExpression.t -> t -> t access_result end -val read : Location.t -> AccessExpression.t -> t -> (t * AbstractAddress.t) access_result +val read : Location.t -> AccessExpression.t -> t -> (t * AbstractAddressSet.t) access_result val read_all : Location.t -> AccessExpression.t list -> t -> t access_result @@ -45,9 +49,9 @@ val havoc_var : Var.t -> t -> t val havoc : Location.t -> AccessExpression.t -> t -> t access_result -val write_var : Var.t -> AbstractAddress.t -> t -> t +val write_var : Var.t -> AbstractAddressSet.t -> t -> t -val write : Location.t -> AccessExpression.t -> AbstractAddress.t -> t -> t access_result +val write : Location.t -> AccessExpression.t -> AbstractAddressSet.t -> t -> t access_result val invalidate : PulseInvalidation.t -> Location.t -> AccessExpression.t -> t -> t access_result diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index a10fe79fc..65d65c005 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -10,7 +10,6 @@ codetoanalyze/cpp/pulse/use_after_delete.cpp, reassign_field_of_deleted_bad, 3, codetoanalyze/cpp/pulse/use_after_delete.cpp, return_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 24, column 3 here,accessed `s` here] codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_branch_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 73, column 3 here,accessed `s` here] codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_loop_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 102, column 3 here,accessed `s->f` here] -codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::FP_allocate_in_branch_ok, 10, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [invalidated by destructor call `std::unique_ptr>_~unique_ptr(a2)` at line 245, column 10 here,accessed `a1` here] codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::double_destructor_bad, 5, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [invalidated by destructor call `use_after_destructor::S_~S(s)` at line 64, column 3 here,accessed `s` here] codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing1_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete alias` at line 142, column 3 here,accessed `s` here] codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 150, column 3 here,accessed `alias` here] diff --git a/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp b/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp index 4f13ee2a4..35b6ca1fa 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp @@ -232,7 +232,7 @@ void FP_destructor_order_empty_destructor_ok() { a.f = &b; } -std::unique_ptr* FP_allocate_in_branch_ok(bool b) { +std::unique_ptr* allocate_in_branch_ok(bool b) { std::unique_ptr a1; std::unique_ptr a2; std::unique_ptr* a3 = &a1; @@ -240,9 +240,9 @@ std::unique_ptr* FP_allocate_in_branch_ok(bool b) { if (b) { a2 = std::make_unique(*a1); a3 = &a2; - } // current join makes a1 and a2 equal + } return a3; -} // we get `use after destructor` for a1, after destructor call for a2 +} } // namespace use_after_destructor