diff --git a/source/domains/abstractProductDomain.ml b/source/domains/abstractProductDomain.ml index 60760bc1c95..b7bffd985e4 100644 --- a/source/domains/abstractProductDomain.ml +++ b/source/domains/abstractProductDomain.ml @@ -29,11 +29,8 @@ module Make (Config : PRODUCT_CONFIG) = struct type product = element array - module IntMap = Map.Make (struct - type t = int - - let compare = compare - end) + module IntMap = Map.Make (Int) + module IntSet = Set.Make (Int) type abstract_slot = Slot : 'a Config.slot -> abstract_slot [@@unbox] @@ -56,8 +53,17 @@ module Make (Config : PRODUCT_CONFIG) = struct (* The route map indicates for each part under a product element which slot the element is in *) let route_map : int IntMap.t = let map = ref IntMap.empty in + let duplicates = ref IntSet.empty in let gather (route : int) (type a) (part : a part) = - map := IntMap.add (part_id part) route !map + let part_id = part_id part in + (* Ignore parts that are present in multiple slots. *) + if not (IntSet.mem part_id !duplicates) then + if not (IntMap.mem part_id !map) then + map := IntMap.add part_id route !map + else begin + map := IntMap.remove part_id !map; + duplicates := IntSet.add part_id !duplicates + end in Array.iteri (fun route (Slot slot) -> diff --git a/source/domains/test/abstractDomainTest.ml b/source/domains/test/abstractDomainTest.ml index fb755879348..65691d13a2f 100644 --- a/source/domains/test/abstractDomainTest.ml +++ b/source/domains/test/abstractDomainTest.ml @@ -2684,6 +2684,61 @@ end module TestFlatString = TestAbstractDomain (FlatString) +module TestProductAmbiguousPart = struct + module StringSet = AbstractSetDomain.Make (String) + + module Slots = struct + type 'a slot = + | Left : StringSet.t slot + | Right : StringSet.t slot + + let slots = 2 + + let slot_name (type a) (slot : a slot) = + match slot with + | Left -> "left" + | Right -> "right" + + + let slot_domain (type a) (slot : a slot) = + match slot with + | Left -> (module StringSet : AbstractDomain.S with type t = a) + | Right -> (module StringSet : AbstractDomain.S with type t = a) + + + let strict (type a) (_slot : a slot) = false + end + + include AbstractProductDomain.Make (Slots) + + let suite () = + let assert_raises_any f = + try + let _ = f () in + assert_failure "Expected an exception to be raised" + with + | _ -> () + in + let test_create _ = + assert_raises_any (fun () -> create [Part (StringSet.Self, StringSet.bottom)]) + in + let test_transform _ = + assert_raises_any (fun () -> transform StringSet.Self Map ~f:(StringSet.add "x") bottom) + in + let test_update_get _ = + let x = StringSet.singleton "x" in + assert_equal (bottom |> update Slots.Left x |> get Slots.Left) x; + assert_equal (bottom |> update Slots.Right x |> get Slots.Right) x; + assert_equal (bottom |> update Slots.Left x |> get Slots.Right) StringSet.bottom; + assert_equal (bottom |> update Slots.Right x |> get Slots.Left) StringSet.bottom + in + [ + "test_create" >:: test_create; + "test_transform" >:: test_transform; + "test_update_get" >:: test_update_get; + ] +end + let () = "abstractDomainTest" >::: [ @@ -2701,5 +2756,6 @@ let () = "tree" >::: TestTreeDomain.suite (); "string_biset" >::: TestOverUnderStringSet.suite (); "flat_string" >::: TestFlatString.suite (); + "product_ambiguous_part" >::: TestProductAmbiguousPart.suite (); ] |> run_test_tt_main