Skip to content

Commit 0f38e2e

Browse files
ivgivg
authored
uses Allen's Interval Algebra in the KB.Value merge implementation (#1441)
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.
1 parent 167a5e1 commit 0f38e2e

File tree

1 file changed

+143
-78
lines changed

1 file changed

+143
-78
lines changed

‎lib/knowledge/bap_knowledge.ml

Lines changed: 143 additions & 78 deletions
Original file line numberDiff line numberDiff line change
@@ -1232,26 +1232,93 @@ module Dict = struct
12321232
let (<>) x y = uid x <> uid y [@@inline]
12331233

12341234

1235-
(* the order between intervals
1236-
The first interval is denoted with a series of [-],
1237-
the second interval is denoted with a series of [|],
1238-
their intersection is [+] and non-intersection is [.]
1235+
(** Allen's Interval Algebra
1236+
1237+
The Allen's Interval Algebra [1,2] describes 13 possible
1238+
relations between two intervals. See also [3] for the nice
1239+
visualizations and an available description.
1240+
1241+
[1]: https://doi.org/10.1145/182.358434
1242+
[2]: https://doi.org/10.1111/j.1467-8640.1989.tb00329.x
1243+
[3]: https://www.thomasalspaugh.org/pub/fnd/allen.html
12391244
*)
1240-
type interval_order =
1241-
| ILT (* ---.||| *)
1242-
| IGT (* |||.--- *)
1243-
| ILE (* --+|| *)
1244-
| IGE (* ||+-- *)
1245-
| INC (* anything else *)
1246-
1247-
let compare_interval l1 u1 l2 u2 =
1248-
match compare u1 l2, compare u2 l1 with
1249-
| 0,_ -> ILE
1250-
| _,0 -> IGE
1251-
| -1,_ -> ILT
1252-
| _,-1 -> IGT
1253-
| _ -> INC
1245+
module Interval = struct
1246+
type order =
1247+
| Before
1248+
| Meets
1249+
| Overlaps
1250+
| Finished
1251+
| Contains
1252+
| Starts
1253+
| Equals
1254+
| Started
1255+
| During
1256+
| Finishes
1257+
| Overlapped
1258+
| Met
1259+
| After
1260+
1261+
let invert f a b c d = f c d a b [@@inline]
1262+
1263+
let meets _ b c _ = b = c [@@inline]
1264+
let met a b c d = invert meets a b c d [@@inline] [@@specialize]
1265+
let before _ b c _ = b < c [@@inline]
1266+
let after a b c d = invert before a b c d [@@inline] [@@specialize]
1267+
let overlaps a b c d = a < c && b < d && b > c [@@inline]
1268+
let overlapped a b c d = invert overlaps a b c d [@@inline] [@@specialize]
1269+
let starts a b c d = a = c && b < d [@@inline]
1270+
let started a b c d = invert starts a b c d [@@inline] [@@specialize]
1271+
let finishes a b c d = a > c && b = d [@@inline]
1272+
let finished a b c d = invert finishes a b c d [@@inline] [@@specialize]
1273+
let during a b c d = a > c && b < d [@@inline]
1274+
let contains a b c d = invert during a b c d [@@inline] [@@specialize]
1275+
let equals a b c d = a = c && b = d [@@inline]
1276+
1277+
let relate a b c d = match () with
1278+
| () when meets a b c d -> Meets
1279+
| () when met a b c d -> Met
1280+
| () when before a b c d -> Before
1281+
| () when after a b c d -> After
1282+
| () when overlaps a b c d -> Overlaps
1283+
| () when overlapped a b c d -> Overlapped
1284+
| () when starts a b c d -> Starts
1285+
| () when started a b c d -> Started
1286+
| () when finishes a b c d -> Finishes
1287+
| () when finished a b c d -> Finished
1288+
| () when during a b c d -> During
1289+
| () when contains a b c d -> Contains
1290+
| () when equals a b c d -> Equals
1291+
| () -> assert false
1292+
[@@inline]
1293+
end
1294+
1295+
(** Extension of the Allen's Algebra over points.
12541296
1297+
A point can have only five relations to an interval.
1298+
1299+
*)
1300+
module Point = struct
1301+
type order =
1302+
| Before (* preceeds the interval *)
1303+
| Starts (* equal to the start *)
1304+
| During (* inside of the interval *)
1305+
| Finishes (* equal to the end *)
1306+
| After (* follows the interval *)
1307+
1308+
let before p a _ = p < a [@@inline]
1309+
let starts p a _ = p = a [@@inline]
1310+
let during p a b = p > a && p < b [@@inline]
1311+
let finishes p _ b = p = b [@@inline]
1312+
let after p _ b = p > b [@@inline]
1313+
let relate p a b = match () with
1314+
| () when before p a b -> Before
1315+
| () when starts p a b -> Starts
1316+
| () when during p a b -> During
1317+
| () when finishes p a b -> Finishes
1318+
| () when after p a b -> After
1319+
| () -> assert false
1320+
[@@inline]
1321+
end
12551322
end
12561323
type 'a key = 'a Key.t
12571324

@@ -1820,70 +1887,68 @@ module Dict = struct
18201887
~update:(fun k -> k m)
18211888
}
18221889

1890+
let merge_11 m ka a kb b = match Key.compare ka kb with
1891+
| 0 -> make1 ka (app m ka kb b a)
1892+
| 1 -> make2 kb b ka a
1893+
| _ -> make2 ka a kb b
1894+
[@@inline]
1895+
1896+
let merge_12 m ka a kb b kc c =
1897+
match Key.Point.relate ka kb kc with
1898+
| Before -> make3 ka a kb b kc c
1899+
| Starts -> make2 ka (app m ka kb b a) kc c
1900+
| During -> make3 kb b ka a kc c
1901+
| Finishes -> make2 kb b ka (app m ka kc c a)
1902+
| After -> make3 kb b kc c ka a
1903+
[@@inline]
1904+
1905+
let merge_13 m ka a kb b kc c kd d =
1906+
match Key.Point.relate ka kb kd with
1907+
| Before -> make4 ka a kb b kc c kd d
1908+
| Starts -> make3 ka (app m ka kb b a) kc c kd d
1909+
| Finishes -> make3 kb b kc c kd (app m kd ka a d)
1910+
| After -> make4 kb b kc c kd d ka a
1911+
| During -> match Key.compare ka kc with
1912+
| 0 -> make3 kb b kc (app m kc ka a c) kd d
1913+
| 1 -> make4 kb b kc c ka a kd d
1914+
| _ -> make4 kb b ka a kc c kd d
1915+
[@@inline]
1916+
1917+
let merge_22 m ka a kb b kc c kd d =
1918+
match Key.Interval.relate ka kb kc kd with
1919+
| Meets -> make3 ka a kb (app m kb kc c b) kd d
1920+
| Met -> make3 kc c kd (app m kd ka a d) kb b
1921+
| Before -> make4 ka a kb b kc c kd d
1922+
| After -> make4 kc c kd d ka a kb b
1923+
| Overlaps -> make4 ka a kc c kb b kd d
1924+
| Overlapped -> make4 kc c ka a kd d kb b
1925+
| Starts -> make3 ka (app m ka kc c a) kb b kd d
1926+
| Started -> make3 ka (app m ka kc c a) kd d kb b
1927+
| Finishes -> make3 kc c ka a kb (app m kb kd d b)
1928+
| Finished -> make3 ka a kc c kb (app m kb kd d b)
1929+
| During -> make4 kc c ka a kb b kd d
1930+
| Contains -> make4 ka a kc c kd d kb b
1931+
| Equals -> make2 ka (app m ka kc c a) kb (app m kb kd d b)
1932+
[@@inline]
1933+
18231934
let merge m x y =
1824-
if phys_equal x y then Ok x
1935+
if phys_equal x y then x
18251936
else match x,y with
1826-
| T0,x | x, T0 -> Ok x
1937+
| T0,x | x, T0 -> x
18271938
| T1 (ka, a), T1 (kb, b) ->
1828-
begin match Key.compare ka kb with
1829-
| 0 -> Ok (make1 ka (app m ka kb b a))
1830-
| 1 -> Ok (make2 kb b ka a)
1831-
| _ -> Ok (make2 ka a kb b)
1832-
end
1939+
merge_11 m ka a kb b
18331940
| T1 (ka, a), T2 (kb, b, kc, c) ->
1834-
begin match Key.compare_interval ka ka kb kc with
1835-
| ILT -> Ok (make3 ka a kb b kc c)
1836-
| IGT -> Ok (make3 kb b kc c ka a)
1837-
| ILE -> Ok (make2 ka (app m ka kb b a) kc c)
1838-
| IGE -> Ok (make2 kb b ka (app m ka kc c a))
1839-
| INC -> Ok (make3 kb b ka a kc c)
1840-
end
1841-
| T2 (ka, a, kb, b), T1 (kc, c) ->
1842-
begin match Key.compare_interval ka kb kc kc with
1843-
| ILT -> Ok (make3 ka a kb b kc c)
1844-
| IGT -> Ok (make3 kc c ka a kb b)
1845-
| ILE -> Ok (make2 ka a kb (app m kb kc c b))
1846-
| IGE -> Ok (make2 ka (app m ka kc c a) kb b)
1847-
| INC -> Ok (make3 ka a kc c kb b)
1848-
end
1941+
merge_12 m ka a kb b kc c
1942+
| T2 (kb, b, kc, c), T1 (ka, a) ->
1943+
merge_12 m ka a kb b kc c
18491944
| T1 (ka, a), T3 (kb, b, kc, c, kd, d) ->
1850-
begin match Key.compare_interval ka ka kc kd with
1851-
| ILT -> Ok (make4 ka a kb b kc c kd d)
1852-
| IGT -> Ok (make4 kb b kc c kd d ka a)
1853-
| ILE -> Ok (make3 ka (app m ka kb b a) kc c kd d)
1854-
| IGE -> Ok (make3 kb b kc c ka (app m ka kd d a))
1855-
| INC -> match Key.compare ka kc with
1856-
| 0 -> Ok (make3 kb b kc (app m kc ka a c) kd d)
1857-
| 1 -> Ok (make4 kb b kc c ka a kd d)
1858-
| _ -> Ok (make4 kb b ka a kc c kd d)
1859-
end
1945+
merge_13 m ka a kb b kc c kd d
1946+
| T3 (kb, b, kc, c, kd, d), T1 (ka, a) ->
1947+
merge_13 m ka a kb b kc c kd d
18601948
| T2 (ka, a, kb, b), T2 (kc, c, kd, d) ->
1861-
begin match Key.compare_interval ka kb kc kd with
1862-
| ILT -> Ok (make4 ka a kb b kc c kd d)
1863-
| IGT -> Ok (make4 kc c kd d ka a kb b)
1864-
| ILE -> Ok (make3 ka a kb (app m kb kc c b) kd d)
1865-
| IGE -> Ok (make3 kc c kd (app m kd ka a d) kb b)
1866-
| INC -> match Key.compare ka kc, Key.compare kb kd with
1867-
| 0,1 -> Ok (make3 ka (app m ka kc c a) kd d kb b)
1868-
| 0,_ -> Ok (make3 ka (app m ka kc c a) kb b kd d)
1869-
| 1,0 -> Ok (make3 kc c ka a kb (app m kb kd d b))
1870-
| _,0 -> Ok (make3 ka a kc c kb (app m kb kd d b))
1871-
| 1,_ -> Ok (make4 kc c ka a kb b kd d)
1872-
| _,_ -> Ok (make4 ka a kc c kd d kb b)
1873-
end
1874-
| T3 (ka, a, kb, b, kc, c), T1 (kd,d) ->
1875-
begin match Key.compare_interval ka kc kd kd with
1876-
| ILT -> Ok (make4 ka a kb b kc c kd d)
1877-
| IGT -> Ok (make4 kd d ka a kb b kc c)
1878-
| ILE -> Ok (make3 ka a kb b kc (app m kc kd d c))
1879-
| IGE -> Ok (make3 kd (app m kd ka a d) kb b kc c)
1880-
| INC -> match Key.compare kd kb with
1881-
| 0 -> Ok (make3 ka a kb (app m kb kd d b) kc c)
1882-
| 1 -> Ok (make4 ka a kb b kd d kc c)
1883-
| _ -> Ok (make4 ka a kd d kb b kc c)
1884-
end
1885-
| _ -> Ok (fold_merge m x y)
1886-
1949+
merge_22 m ka a kb b kc c kd d
1950+
| _ -> fold_merge m x y
1951+
[@@inline]
18871952

18881953
let sexp_of_t dict = Sexp.List (foreach ~init:[] dict {
18891954
visit = fun k x xs ->
@@ -2005,11 +2070,11 @@ module Record = struct
20052070

20062071

20072072
let join x y =
2008-
try Dict.merge domain_merge x y
2073+
try Ok (Dict.merge domain_merge x y)
20092074
with Merge_conflict err -> Error err
20102075

20112076
let try_merge ~on_conflict x y =
2012-
try Dict.merge (resolving_merge on_conflict) x y
2077+
try Ok (Dict.merge (resolving_merge on_conflict) x y)
20132078
with Merge_conflict err -> Error err
20142079

20152080
let eq = Dict.Key.same

0 commit comments

Comments
 (0)