pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[pulse] RIP join

Browse Source 
Summary:
It's dead.

dr_pig_dead

Reviewed By: mbouaziz

Differential Revision: D14258494

fbshipit-source-id: 136e92eb3
master
Jules Villard 6 years ago committed by Facebook Github Bot
parent c02edf85a9
commit e118fe2ea4
1 changed files with 3 additions and 188 deletions
Show Stats Download Patch File Download Diff File

191
infer/src/checkers/PulseDomain.ml
Unescape View File

@ -6,7 +6,6 @@
*)
open! IStd
module F = Format
module L = Logging
module Invalidation = PulseInvalidation
(* {2 Abstract domain description } *)
@ -93,8 +92,6 @@ module Memory : sig
val for_all : (AbstractAddress.t -> cell -> bool) -> t -> bool
val fold : (AbstractAddress.t -> cell -> 'accum -> 'accum) -> t -> 'accum -> 'accum
val pp : F.formatter -> t -> unit
val add_edge : AbstractAddress.t -> Access.t -> AddrTracePair.t -> t -> t
@ -215,8 +212,6 @@ end = struct
let find_opt = Graph.find_opt
let for_all = Graph.for_all
let fold = Graph.fold
end
(** Stacks: map addresses of variables to values and initialisation location.
@ -292,192 +287,12 @@ let piecewise_lessthan lhs rhs =
lhs.heap
module JoinState = struct
module AddressUnionSet = struct
module Set = PrettyPrintable.MakePPSet (AbstractAddress)
type elt = AbstractAddress.t [@@deriving compare]
type t = Set.t ref
let create x = ref (Set.singleton x)
let compare_size _ _ = 0
let merge ~from ~to_ = to_ := Set.union !from !to_
let pp f x = Set.pp f !x
end
module AddressUF = ImperativeUnionFind.Make (AddressUnionSet)
(** just to get the correct type coercion *)
let to_canonical_address subst addr = (AddressUF.find subst addr :> AbstractAddress.t)
type nonrec t = {subst: AddressUF.t; astate: t}
(** adds [(src_addr, access, value)] to [union_heap] and record potential new equality that
results from it in [subst] *)
let union_one_edge subst src_addr access value union_heap =
let dst_addr, _ = value in
let src_addr = to_canonical_address subst src_addr in
let dst_addr = to_canonical_address subst dst_addr in
match (Memory.find_edge_opt src_addr access union_heap, (access : Memory.Access.t)) with
| Some (dst_addr', _), _ when AbstractAddress.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
, `No_new_equality )
| None, _ ->
(Memory.add_edge src_addr access value 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)
module Addresses = Caml.Set.Make (AbstractAddress)
let rec visit_address subst visited heap addr union_heap =
if Addresses.mem addr visited then (visited, union_heap)
else
let visited = Addresses.add addr visited in
let visit_edge access value (visited, union_heap) =
union_one_edge subst addr access value union_heap
|> fst
|> visit_address subst visited heap (fst value)
in
Memory.find_opt addr heap
|> Option.fold ~init:(visited, union_heap) ~f:(fun (visited, union_heap) (edges, attrs) ->
let union_heap = Memory.add_attributes addr attrs union_heap in
Memory.Edges.fold visit_edge edges (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 )
stack (visited, union_heap)
in
union_heap
let populate_subst_from_stacks subst stack1 stack2 =
ignore
((* Use [Caml.Map.merge] to detect the variables present in both stacks. Build an empty
result map since we don't use the result. *)
Stack.merge
(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) ) ;
(* empty result map *)
None )
stack1 stack2)
let from_astate_union {heap= heap1; stack= stack1} {heap= heap2; stack= stack2} =
let subst = AddressUF.create () in
(* gather equalities from the stacks *)
populate_subst_from_stacks subst stack1 stack2 ;
(* union the heaps, take this opportunity to do garbage collection of unreachable values by
only copying the addresses reachable from the variables in the stacks *)
let heap = visit_stack subst heap1 stack1 Memory.empty |> visit_stack subst heap2 stack2 in
(* This keeps all the variables and picks one representative address for each variable in
common thanks to [AbstractAddressDomain_JoinIsMin] *)
let stack = Stack.join stack1 stack2 in
{subst; astate= {heap; stack}}
let rec normalize state =
let one_addr subst addr (edges, attrs) (heap, has_converged) =
let heap = Memory.add_attributes addr attrs heap in
Memory.Edges.fold
(fun access addr_dest (heap, has_converged) ->
match union_one_edge subst addr access addr_dest heap with
| heap, `No_new_equality ->
(heap, has_converged)
| heap, `New_equality ->
(heap, false) )
edges (heap, has_converged)
in
let heap, has_converged =
Memory.fold (one_addr state.subst) state.astate.heap (Memory.empty, true)
in
if has_converged then (
let pp_union_find_classes f subst =
Container.iter subst ~fold:AddressUF.fold_sets ~f:(fun ((repr : AddressUF.Repr.t), set) ->
F.fprintf f "%a=%a@;" AbstractAddress.pp
(repr :> AbstractAddress.t)
AddressUnionSet.pp set )
in
L.d_printfln "Join unified addresses:@\n@[<v2> %a@]" pp_union_find_classes state.subst ;
let stack =
Stack.map
(fun (addr, loc) -> (to_canonical_address state.subst addr, loc))
state.astate.stack
in
{heap; stack} )
else normalize {state with astate= {state.astate with heap}}
end
(** Given
- stacks S1, S2 : Var -> Address,
- graphs G1, G2 : Address -> Access -> Address,
- and invalid sets I1, I2 : 2^Address
(all finite), the join of 2 abstract states (S1, G1, I1) and (S2, G2, I2) is (S, G, A) where
there exists a substitution σ from addresses to addresses such that the following holds. Given
addresses l, l', access path a, and graph G, we write l –a–> l' ∈ G if there is a path labelled
by a from l to l' in G (in particular, if a is empty then l –a–> l' ∈ G for all l, l').
∀ i ∈ {1,2}, ∀ l, x, a, ∀ l' ∈ Ii, ((x, l) ∈ Si ∧ l –a–> l' ∈ Gi)
=> (x, σ(l)) ∈ S ∧ σ(l) –a–> σ(l') ∈ G ∧ σ(l') ∈ I
let join _ _ = (* not implemented: use disjunctive domain instead *) assert false
For now the implementation gives back a larger heap than necessary, where all the previously
reachable location are still reachable (up to the substitution) instead of only the locations
leading to invalid ones.
*)
let join astate1 astate2 =
if phys_equal astate1 astate2 then astate1
else
(* high-level idea: maintain some union-find data structure to identify locations in one heap
with locations in the other heap. Build the initial join state as follows:
- equate all locations that correspond to identical variables in both stacks, eg joining
stacks {x=1} and {x=2} adds "1=2" to the unification.
- add all addresses reachable from stack variables to the join state heap
This gives us an abstract state that is the union of both abstract states, but more states
can still be made equal. For instance, if 1 points to 3 in the first heap and 2 points to 4
in the second heap and we deduced "1 = 2" from the stacks already (as in the example just
above) then we can deduce "3 = 4". Proceed in this fashion until no more equalities are
discovered, and return the abstract state where a canonical representative has been chosen
consistently for each equivalence class (this is what the union-find data structure gives
us). *)
JoinState.from_astate_union astate1 astate2 |> JoinState.normalize
(* TODO: this could be [piecewise_lessthan lhs' (join lhs rhs)] where [lhs'] is [lhs] renamed
according to the unification discovered while joining [lhs] and [rhs]. *)
let ( <= ) ~lhs ~rhs = phys_equal lhs rhs || piecewise_lessthan lhs rhs
let max_widening = 5
let widen ~prev ~next ~num_iters =
(* widening is underapproximation for now... TODO *)
if num_iters > max_widening then prev else if phys_equal prev next then prev else join prev next
let widen ~prev:_ ~next:_ ~num_iters:_ =
(* not implemented: use disjunctive domain instead *) assert false
let pp fmt {heap; stack} =

Write Preview
Loading…
Cancel
Save