diff --git a/src/cdomain/value/cdomains/threadIdDomain.ml b/src/cdomain/value/cdomains/threadIdDomain.ml index e7b915df3d..882717f01a 100644 --- a/src/cdomain/value/cdomains/threadIdDomain.ml +++ b/src/cdomain/value/cdomains/threadIdDomain.ml @@ -147,40 +147,36 @@ struct (* We do not consider a thread its own parent *) false else - let cdef_ancestor = P.common_suffix p p' in - P.equal p cdef_ancestor + match GobList.remove_common_prefix Base.equal (List.rev p) (List.rev p') with + | [], _ -> true + | _ :: _, _ -> false let may_create ((p, s) as t) ((p', s') as t') = if is_unique t' then is_must_parent t t' (* unique must be created by something unique (that's a prefix) *) else if is_unique t then ( (* t' is already non-unique *) - let cdef_ancestor = P.common_suffix p p' in - if P.equal cdef_ancestor p then ( (* p is prefix of p' *) - (* let dp = elements added to prefix *) + match GobList.remove_common_prefix Base.equal (List.rev p) (List.rev p') with + | [], dp -> (* p is prefix of p' *) + (* dp = elements added to prefix *) (* S.disjoint (S.of_list p) (S.union (S.of_list dp) s') (* added elements must not appear in p, otherwise compose would become shorter and non-unique *) *) (* no need to check disjointness, because if t' is well-formed, then dp and s' won't have anything from cdef_ancestor anyway *) true - ) - else if P.equal cdef_ancestor p' then ( (* p is not prefix of p', but p' is prefix of p *) - (* TODO: avoid length calculations? *) - let dp' = BatList.take (List.length p - List.length cdef_ancestor) p in (* elements removed from prefix *) + | dp', [] -> (* p is not prefix of p', but p' is prefix of p *) + (* dp' = elements removed from prefix *) S.subset (S.of_list dp') s' (* removed elements become part of set, must be contained, because compose can only add them *) (* no need to check disjointness, because if t' is well-formed, then s' won't have anything from cdef_ancestor anyway *) - ) - else - false (* prefixes must not be incompatible (one is prefix of another or vice versa), because compose cannot fix incompatibility there *) + | _ :: _, _ :: _ -> (* prefixes must not be incompatible (one is prefix of another or vice versa), because compose cannot fix incompatibility there *) + false ) else ( (* both are non-unique *) - let cdef_ancestor = P.common_suffix p p' in - if P.equal cdef_ancestor p' then ( (* p' is prefix of p *) - (* TODO: avoid length calculations? *) - let dp' = BatList.take (List.length p - List.length cdef_ancestor) p in (* elements removed from prefix *) + match GobList.remove_common_prefix Base.equal (List.rev p) (List.rev p') with + | dp', [] -> (* p' is prefix of p *) + (* dp' = elements removed from prefix *) S.subset (S.union (S.of_list dp') s) s' (* elements must be contained, because compose can only add them *) (* can just subset s' thanks to well-formedness conditions *) (* no need to check disjointness, because if t' is well-formed, then s' won't have anything from cdef_ancestor anyway *) - ) - else - false (* p' must be prefix of p, because non-unique compose can only shorten prefix *) + | _, _ :: _ -> (* p' must be prefix of p, because non-unique compose can only shorten prefix *) + false ) let compose ((p, s) as current) ni = diff --git a/src/common/domains/printable.ml b/src/common/domains/printable.ml index 93d3f99edc..9ef9e7e79a 100644 --- a/src/common/domains/printable.ml +++ b/src/common/domains/printable.ml @@ -631,16 +631,6 @@ struct BatPrintf.fprintf f "\n\n"; loop 0 xs; BatPrintf.fprintf f "\n\n" - - let common_prefix x y = - let rec helper acc x y = - match x,y with - | x::xs, y::ys when Base.equal x y-> helper (x::acc) xs ys - | _ -> acc - in - List.rev (helper [] x y) - - let common_suffix x y = List.rev (common_prefix (List.rev x) (List.rev y)) end module type ChainParams = sig diff --git a/src/util/std/gobList.ml b/src/util/std/gobList.ml index 3743b0127e..f0b3b99932 100644 --- a/src/util/std/gobList.ml +++ b/src/util/std/gobList.ml @@ -30,6 +30,11 @@ let rec fold_while_some (f : 'a -> 'b -> 'a option) (acc: 'a) (xs: 'b list): 'a let equal = List.eq +let rec remove_common_prefix eq l1 l2 = + match l1, l2 with + | x1 :: l1', x2 :: l2' when eq x1 x2 -> remove_common_prefix eq l1' l2' + | _, _ -> (l1, l2) + (** Given a predicate and a list, returns two lists [(l1, l2)]. [l1] contains the prefix of the list until the last element that satisfies the predicate, [l2] contains all subsequent elements. The order of elements is preserved. *) let until_last_with (pred: 'a -> bool) (xs: 'a list) =