diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index c1f3b58d3..ec3268efe 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -240,14 +240,14 @@ let mk_initial proc_desc = let discard_unreachable ({pre; post} as astate) = - let pre_addresses = PulseDomain.visit (pre :> PulseDomain.t) in + let pre_addresses = PulseDomain.reachable_addresses (pre :> PulseDomain.t) in let pre_old_heap = (pre :> PulseDomain.t).heap in let pre_new_heap = PulseDomain.Memory.filter (fun address -> PulseDomain.AbstractAddressSet.mem address pre_addresses) pre_old_heap in - let post_addresses = PulseDomain.visit (post :> PulseDomain.t) in + let post_addresses = PulseDomain.reachable_addresses (post :> PulseDomain.t) in let all_addresses = PulseDomain.AbstractAddressSet.union pre_addresses post_addresses in let post_old_heap = (post :> PulseDomain.t).heap in let post_new_heap = diff --git a/infer/src/pulse/PulseDomain.ml b/infer/src/pulse/PulseDomain.ml index e70636441..d54bc5b81 100644 --- a/infer/src/pulse/PulseDomain.ml +++ b/infer/src/pulse/PulseDomain.ml @@ -491,11 +491,26 @@ let pp fmt {heap; stack} = F.fprintf fmt "{@[ heap=@[%a@];@;stack=@[%a@];@]}" Memory.pp heap Stack.pp stack -module GraphGC : sig - val visit : t -> AbstractAddressSet.t - (** compute the set of abstract addresses that are "used" in the abstract state, i.e. reachable - from the stack variables *) +module GraphVisit : sig + val fold : + var_filter:(Var.t -> bool) + -> t + -> init:'accum + -> f:( 'accum + -> AbstractAddress.t + -> Var.t + -> Memory.Access.t list + -> ('accum, 'final) Base.Continue_or_stop.t) + -> finish:('accum -> 'final) + -> AbstractAddressSet.t * 'final + (** Generic graph traversal of the memory starting from each variable in the stack that pass + [var_filter], in order. Returns the result of folding over every address in the graph and the + set of addresses that have been visited before [f] returned [Stop] or all reachable addresses + were seen. [f] is passed each address together with the variable from which the address was + reached and the access path from that variable to the address. *) end = struct + open Base.Continue_or_stop + let visit address visited = if AbstractAddressSet.mem address visited then `AlreadyVisited else @@ -503,29 +518,50 @@ end = struct `NotAlreadyVisited visited - let rec visit_address astate address visited = + let rec visit_address orig_var ~f rev_accesses astate address ((visited, accum) as visited_accum) + = match visit address visited with | `AlreadyVisited -> - visited + Continue visited_accum | `NotAlreadyVisited visited -> ( - match Memory.find_opt address astate.heap with - | None -> - visited - | Some (edges, _) -> - visit_edges astate ~edges visited ) - - - and visit_edges ~edges astate visited = - Memory.Edges.fold - (fun _access (address, _trace) visited -> visit_address astate address visited) - edges visited - - - let visit astate = - Stack.fold - (fun _var (address, _loc) visited -> visit_address astate address visited) - astate.stack AbstractAddressSet.empty + match f accum address orig_var rev_accesses with + | Continue accum -> ( + match Memory.find_opt address astate.heap with + | None -> + Continue (visited, accum) + | Some (edges, _) -> + visit_edges orig_var ~f rev_accesses astate ~edges (visited, accum) ) + | Stop fin -> + Stop (visited, fin) ) + + + and visit_edges orig_var ~f rev_accesses ~edges astate visited_accum = + let finish visited_accum = Continue visited_accum in + Container.fold_until edges + ~fold:(IContainer.fold_of_pervasives_map_fold ~fold:Memory.Edges.fold) + ~finish ~init:visited_accum ~f:(fun visited_accum (access, (address, _trace)) -> + match visit_address orig_var ~f (access :: rev_accesses) astate address visited_accum with + | Continue _ as cont -> + cont + | Stop fin -> + Stop (Stop fin) ) + + + let fold ~var_filter astate ~init ~f ~finish = + let finish (visited, accum) = (visited, finish accum) in + let init = (AbstractAddressSet.empty, init) in + Container.fold_until astate.stack + ~fold:(IContainer.fold_of_pervasives_map_fold ~fold:Stack.fold) ~init ~finish + ~f:(fun visited_accum (var, (address, _loc)) -> + if var_filter var then visit_address var ~f [] astate address visited_accum + else Continue visited_accum ) end include GraphComparison -include GraphGC + +let reachable_addresses astate = + GraphVisit.fold astate + ~var_filter:(fun _ -> true) + ~init:() ~finish:Fn.id + ~f:(fun () _ _ _ -> Continue ()) + |> fst diff --git a/infer/src/pulse/PulseDomain.mli b/infer/src/pulse/PulseDomain.mli index c53969efc..a84a73d5b 100644 --- a/infer/src/pulse/PulseDomain.mli +++ b/infer/src/pulse/PulseDomain.mli @@ -109,9 +109,9 @@ val empty : t include AbstractDomain.NoJoin with type t := t -val visit : t -> AbstractAddressSet.t +val reachable_addresses : t -> AbstractAddressSet.t (** compute the set of abstract addresses that are "used" in the abstract state, i.e. reachable - from the stack variables *) + from the stack variables *) type mapping