From d657bb89789f1898e8a3c5dbb6ed53c11171d6f2 Mon Sep 17 00:00:00 2001 From: ivg Date: Tue, 8 Mar 2022 15:35:19 -0500 Subject: [PATCH] uses Allen's Interval Algebra in the KB.Value merge implementation The Allen's Interval Algebra gives an exhaustive set of 13 distinct relationships between two intervals that makes writing the merge operation much easier and less error prone. We also extend the algebra to the relation between a point and an interval to handle singleton ranges. --- lib/knowledge/bap_knowledge.ml | 221 +++++++++++++++++++++------------ 1 file changed, 143 insertions(+), 78 deletions(-) diff --git a/lib/knowledge/bap_knowledge.ml b/lib/knowledge/bap_knowledge.ml index 23baf662d..402015804 100644 --- a/lib/knowledge/bap_knowledge.ml +++ b/lib/knowledge/bap_knowledge.ml @@ -1232,26 +1232,93 @@ module Dict = struct let (<>) x y = uid x <> uid y [@@inline] - (* the order between intervals - The first interval is denoted with a series of [-], - the second interval is denoted with a series of [|], - their intersection is [+] and non-intersection is [.] + (** Allen's Interval Algebra + + The Allen's Interval Algebra [1,2] describes 13 possible + relations between two intervals. See also [3] for the nice + visualizations and an available description. + + [1]: https://doi.org/10.1145/182.358434 + [2]: https://doi.org/10.1111/j.1467-8640.1989.tb00329.x + [3]: https://www.thomasalspaugh.org/pub/fnd/allen.html *) - type interval_order = - | ILT (* ---.||| *) - | IGT (* |||.--- *) - | ILE (* --+|| *) - | IGE (* ||+-- *) - | INC (* anything else *) - - let compare_interval l1 u1 l2 u2 = - match compare u1 l2, compare u2 l1 with - | 0,_ -> ILE - | _,0 -> IGE - | -1,_ -> ILT - | _,-1 -> IGT - | _ -> INC + module Interval = struct + type order = + | Before + | Meets + | Overlaps + | Finished + | Contains + | Starts + | Equals + | Started + | During + | Finishes + | Overlapped + | Met + | After + + let invert f a b c d = f c d a b [@@inline] + + let meets _ b c _ = b = c [@@inline] + let met a b c d = invert meets a b c d [@@inline] [@@specialize] + let before _ b c _ = b < c [@@inline] + let after a b c d = invert before a b c d [@@inline] [@@specialize] + let overlaps a b c d = a < c && b < d && b > c [@@inline] + let overlapped a b c d = invert overlaps a b c d [@@inline] [@@specialize] + let starts a b c d = a = c && b < d [@@inline] + let started a b c d = invert starts a b c d [@@inline] [@@specialize] + let finishes a b c d = a > c && b = d [@@inline] + let finished a b c d = invert finishes a b c d [@@inline] [@@specialize] + let during a b c d = a > c && b < d [@@inline] + let contains a b c d = invert during a b c d [@@inline] [@@specialize] + let equals a b c d = a = c && b = d [@@inline] + + let relate a b c d = match () with + | () when meets a b c d -> Meets + | () when met a b c d -> Met + | () when before a b c d -> Before + | () when after a b c d -> After + | () when overlaps a b c d -> Overlaps + | () when overlapped a b c d -> Overlapped + | () when starts a b c d -> Starts + | () when started a b c d -> Started + | () when finishes a b c d -> Finishes + | () when finished a b c d -> Finished + | () when during a b c d -> During + | () when contains a b c d -> Contains + | () when equals a b c d -> Equals + | () -> assert false + [@@inline] + end + + (** Extension of the Allen's Algebra over points. + A point can have only five relations to an interval. + + *) + module Point = struct + type order = + | Before (* preceeds the interval *) + | Starts (* equal to the start *) + | During (* inside of the interval *) + | Finishes (* equal to the end *) + | After (* follows the interval *) + + let before p a _ = p < a [@@inline] + let starts p a _ = p = a [@@inline] + let during p a b = p > a && p < b [@@inline] + let finishes p _ b = p = b [@@inline] + let after p _ b = p > b [@@inline] + let relate p a b = match () with + | () when before p a b -> Before + | () when starts p a b -> Starts + | () when during p a b -> During + | () when finishes p a b -> Finishes + | () when after p a b -> After + | () -> assert false + [@@inline] + end end type 'a key = 'a Key.t @@ -1820,70 +1887,68 @@ module Dict = struct ~update:(fun k -> k m) } + let merge_11 m ka a kb b = match Key.compare ka kb with + | 0 -> make1 ka (app m ka kb b a) + | 1 -> make2 kb b ka a + | _ -> make2 ka a kb b + [@@inline] + + let merge_12 m ka a kb b kc c = + match Key.Point.relate ka kb kc with + | Before -> make3 ka a kb b kc c + | Starts -> make2 ka (app m ka kb b a) kc c + | During -> make3 kb b ka a kc c + | Finishes -> make2 kb b ka (app m ka kc c a) + | After -> make3 kb b kc c ka a + [@@inline] + + let merge_13 m ka a kb b kc c kd d = + match Key.Point.relate ka kb kd with + | Before -> make4 ka a kb b kc c kd d + | Starts -> make3 ka (app m ka kb b a) kc c kd d + | Finishes -> make3 kb b kc c kd (app m kd ka a d) + | After -> make4 kb b kc c kd d ka a + | During -> match Key.compare ka kc with + | 0 -> make3 kb b kc (app m kc ka a c) kd d + | 1 -> make4 kb b kc c ka a kd d + | _ -> make4 kb b ka a kc c kd d + [@@inline] + + let merge_22 m ka a kb b kc c kd d = + match Key.Interval.relate ka kb kc kd with + | Meets -> make3 ka a kb (app m kb kc c b) kd d + | Met -> make3 kc c kd (app m kd ka a d) kb b + | Before -> make4 ka a kb b kc c kd d + | After -> make4 kc c kd d ka a kb b + | Overlaps -> make4 ka a kc c kb b kd d + | Overlapped -> make4 kc c ka a kd d kb b + | Starts -> make3 ka (app m ka kc c a) kb b kd d + | Started -> make3 ka (app m ka kc c a) kd d kb b + | Finishes -> make3 kc c ka a kb (app m kb kd d b) + | Finished -> make3 ka a kc c kb (app m kb kd d b) + | During -> make4 kc c ka a kb b kd d + | Contains -> make4 ka a kc c kd d kb b + | Equals -> make2 ka (app m ka kc c a) kb (app m kb kd d b) + [@@inline] + let merge m x y = - if phys_equal x y then Ok x + if phys_equal x y then x else match x,y with - | T0,x | x, T0 -> Ok x + | T0,x | x, T0 -> x | T1 (ka, a), T1 (kb, b) -> - begin match Key.compare ka kb with - | 0 -> Ok (make1 ka (app m ka kb b a)) - | 1 -> Ok (make2 kb b ka a) - | _ -> Ok (make2 ka a kb b) - end + merge_11 m ka a kb b | T1 (ka, a), T2 (kb, b, kc, c) -> - begin match Key.compare_interval ka ka kb kc with - | ILT -> Ok (make3 ka a kb b kc c) - | IGT -> Ok (make3 kb b kc c ka a) - | ILE -> Ok (make2 ka (app m ka kb b a) kc c) - | IGE -> Ok (make2 kb b ka (app m ka kc c a)) - | INC -> Ok (make3 kb b ka a kc c) - end - | T2 (ka, a, kb, b), T1 (kc, c) -> - begin match Key.compare_interval ka kb kc kc with - | ILT -> Ok (make3 ka a kb b kc c) - | IGT -> Ok (make3 kc c ka a kb b) - | ILE -> Ok (make2 ka a kb (app m kb kc c b)) - | IGE -> Ok (make2 ka (app m ka kc c a) kb b) - | INC -> Ok (make3 ka a kc c kb b) - end + merge_12 m ka a kb b kc c + | T2 (kb, b, kc, c), T1 (ka, a) -> + merge_12 m ka a kb b kc c | T1 (ka, a), T3 (kb, b, kc, c, kd, d) -> - begin match Key.compare_interval ka ka kc kd with - | ILT -> Ok (make4 ka a kb b kc c kd d) - | IGT -> Ok (make4 kb b kc c kd d ka a) - | ILE -> Ok (make3 ka (app m ka kb b a) kc c kd d) - | IGE -> Ok (make3 kb b kc c ka (app m ka kd d a)) - | INC -> match Key.compare ka kc with - | 0 -> Ok (make3 kb b kc (app m kc ka a c) kd d) - | 1 -> Ok (make4 kb b kc c ka a kd d) - | _ -> Ok (make4 kb b ka a kc c kd d) - end + merge_13 m ka a kb b kc c kd d + | T3 (kb, b, kc, c, kd, d), T1 (ka, a) -> + merge_13 m ka a kb b kc c kd d | T2 (ka, a, kb, b), T2 (kc, c, kd, d) -> - begin match Key.compare_interval ka kb kc kd with - | ILT -> Ok (make4 ka a kb b kc c kd d) - | IGT -> Ok (make4 kc c kd d ka a kb b) - | ILE -> Ok (make3 ka a kb (app m kb kc c b) kd d) - | IGE -> Ok (make3 kc c kd (app m kd ka a d) kb b) - | INC -> match Key.compare ka kc, Key.compare kb kd with - | 0,1 -> Ok (make3 ka (app m ka kc c a) kd d kb b) - | 0,_ -> Ok (make3 ka (app m ka kc c a) kb b kd d) - | 1,0 -> Ok (make3 kc c ka a kb (app m kb kd d b)) - | _,0 -> Ok (make3 ka a kc c kb (app m kb kd d b)) - | 1,_ -> Ok (make4 kc c ka a kb b kd d) - | _,_ -> Ok (make4 ka a kc c kd d kb b) - end - | T3 (ka, a, kb, b, kc, c), T1 (kd,d) -> - begin match Key.compare_interval ka kc kd kd with - | ILT -> Ok (make4 ka a kb b kc c kd d) - | IGT -> Ok (make4 kd d ka a kb b kc c) - | ILE -> Ok (make3 ka a kb b kc (app m kc kd d c)) - | IGE -> Ok (make3 kd (app m kd ka a d) kb b kc c) - | INC -> match Key.compare kd kb with - | 0 -> Ok (make3 ka a kb (app m kb kd d b) kc c) - | 1 -> Ok (make4 ka a kb b kd d kc c) - | _ -> Ok (make4 ka a kd d kb b kc c) - end - | _ -> Ok (fold_merge m x y) - + merge_22 m ka a kb b kc c kd d + | _ -> fold_merge m x y + [@@inline] let sexp_of_t dict = Sexp.List (foreach ~init:[] dict { visit = fun k x xs -> @@ -2005,11 +2070,11 @@ module Record = struct let join x y = - try Dict.merge domain_merge x y + try Ok (Dict.merge domain_merge x y) with Merge_conflict err -> Error err let try_merge ~on_conflict x y = - try Dict.merge (resolving_merge on_conflict) x y + try Ok (Dict.merge (resolving_merge on_conflict) x y) with Merge_conflict err -> Error err let eq = Dict.Key.same