diff --git a/infer/src/checkers/PulseDomain.ml b/infer/src/checkers/PulseDomain.ml index 0fb47d6eb..1ef108c01 100644 --- a/infer/src/checkers/PulseDomain.ml +++ b/infer/src/checkers/PulseDomain.ml @@ -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 join _ _ = (* not implemented: use disjunctive domain instead *) assert false - 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@[ %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 - - 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} =