fixes a bug in the KB update function, adds new functions (#1439)

The bug was a typo in the merge function that was manifested with the
`Failure "types are not equal"` exception.

The new functions, are

- `proceed ~until` as a dual to `guard`;
- `Value.is_empty` that returns `true` if a value is empty
- `Value.has` that checks if the specific property of the value is empty

The change also ensures that empty properties are not stored in
values (which also makes the `Value.is_empty` implementation trivial).

Author: ivg

lib/knowledge/bap_knowledge.ml

@@ -1835,7 +1835,7 @@ module Dict = struct
           | 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 kb b a))
+          | 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) ->
@@ -1853,7 +1853,7 @@ module Dict = struct
           | 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 kd d c) kd d)
+            | 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
@@ -1934,6 +1934,7 @@ module Record = struct
     Hashtbl.create (module Uid)
 
   let empty = Dict.empty
+  let is_empty = Dict.is_empty
 
   let uid = Key.uid
   let domain k = Hashtbl.find_exn vtables (uid k)
@@ -2294,18 +2295,25 @@ module Knowledge = struct
     let empty cls =
       {cls; data=Record.empty; time = next_second ()}
 
+    let is_empty {data} = Record.is_empty data
+
     let order {data=x} {data=y} = Record.order x y
 
     let refine {data; cls; time} s=
       {data; time; cls = Class.refine cls s}
 
     let cls {cls} = cls
     let create cls data = {cls; data; time = next_second ()}
-    let put {Slot.key} v x = {
-      v with data = Record.put key v.data x;
-             time = next_second ()
-    }
+    let put {Slot.key; dom} v x =
+      if Domain.is_empty dom x then v
+      else {
+        v with data = Record.put key v.data x;
+               time = next_second ()
+      }
     let get {Slot.key; dom} {data} = Record.get key dom data
+    let has {Slot.key; dom} {data} =
+      not @@ Domain.is_empty dom @@ Record.get key dom data
+
     let strip
       : type a b. (a value, b value) Type_equal.t -> (a,b) Type_equal.t =
       fun T -> T
@@ -2669,6 +2677,7 @@ module Knowledge = struct
   let guard cnd = if not cnd
     then reject ()
     else Knowledge.return ()
+  let proceed ~unless:cnd = guard (not cnd)
   let on cnd yes = if cnd
     then yes
     else reject ()

lib/knowledge/bap_knowledge.mli

@@ -329,6 +329,16 @@ module Knowledge : sig
   val guard : bool -> unit t
 
 
+  (** [proceed ~unless:cnd] rejects the computation unless [cnd] holds.
+
+      Dual to {!guard}, this operator rejects a promise (or any other
+      computation in the scope of the {!with_empty} operator) unless
+      the [cnd] holds, i.e., it is the same as [guard (not cnd)].
+
+      @since 2.5.0 *)
+  val proceed : unless:bool -> unit t
+
+
   (** [on cnd x] evaluates to [x] if [cnd], otherwise rejects.
 
       When in the scope of the [with_empty] function, e.g., in a
@@ -886,6 +896,13 @@ module Knowledge : sig
     val empty : ('a,'b) cls -> ('a,'b) cls value
 
 
+    (** [is_empty x] iff all properties of [x] are empty.
+
+        @since 2.5.0
+    *)
+    val is_empty : _ value -> bool
+
+
     (** [order x y] orders [x] and [y] by their information content.  *)
     val order : 'a value -> 'a value -> Order.partial
 
@@ -941,6 +958,12 @@ module Knowledge : sig
     (** [put p v x] sets a value of the property [p].  *)
     val put : ('k,'p) slot -> ('k,'s) cls value -> 'p -> ('k,'s) cls value
 
+    (** [has p x] if property [p] of [x] is not empty.
+
+        @since 2.5.0
+    *)
+    val has : ('k,'p) slot -> ('k,'s) cls value -> bool
+
     (** [refine v s] refines the sort of [v] to [s].
 
         Since, this function doesn't change the information stored in