extends the knowledge monad interface (#1360)

This is a quality of life PR (an extract from another PR that I am currently working on) that adds a few useful primitives to the knowledge base monad interface.

The most important addition is the new operator `require` that works like `collect` but raises the empty value conflict if the returned value is empty. This function is inteded to be used in the context of promises and proposals that now catch this exception and evaluate the whole scoped expression to the empty value of the computed domain. This vastly simplify the implementation logic of promises for domains that do not use `None` as the empty value.

To make things work even more smoothly we extend the KB.Syntax module with a few new operators. First of all, we include the `Monad.Let` directly into the `KB.Syntax` so that you don't need to open `KB.Let` anymore. Next, we introduce `let*?` and `let+?`, which let-binding couterparts of the already existing `>>=?` and `>>|?` infix operators. Next, we add `-->?` to complement `-->`, it collects an optional domain value and fails if it is `None`.

Finally, we add indexing operators for accessing fields of KB values. The also come with the empty-checking variants.

The PR also applies the new operators to the existing code for the demonstration purposes (and to show that it works). I also believe that the rewritten code is more reable, even despite that I still prefer the infix syntax to the let-binding operators.

Author: ivg

lib/bap_primus/bap_primus_lisp_semantics.ml

@@ -685,17 +685,14 @@ let provide_semantics ?(stdout=Format.std_formatter) () =
       provide Theory.Semantics.slot |>
       comment "reifies Primus Lisp definitions"
     end);
-  let (>>=?) x f = x >>= function
-    | None -> !!Insn.empty
-    | Some x -> f x in
   let require p k = if p then k () else !!Insn.empty in
   KB.promise Theory.Semantics.slot @@ fun obj ->
-  KB.collect Theory.Label.unit obj >>=? fun unit ->
-  KB.collect Property.name obj >>=? fun name ->
-  obtain_typed_program unit >>= fun prog ->
+  let* unit = obj-->?Theory.Label.unit in
+  let* name = obj-->?Property.name in
+  let* prog = obtain_typed_program unit in
   require (Set.mem prog.names name) @@ fun () ->
-  KB.collect Property.args obj >>= fun args ->
-  KB.collect Theory.Unit.target unit >>= fun target ->
+  let* args = obj-->Property.args in
+  let* target = KB.collect Theory.Unit.target unit in
   let bits = Theory.Target.bits target in
   KB.Context.set State.var State.{
       binds = Map.empty (module Theory.Var.Top);
@@ -706,7 +703,7 @@ let provide_semantics ?(stdout=Format.std_formatter) () =
     } >>= fun () ->
   let* (module Core) = Theory.current in
   let open Prelude(Core) in
-  reify stdout prog obj target name args >>= fun res ->
+  let* res = reify stdout prog obj target name args in
   KB.collect Disasm_expert.Basic.Insn.slot obj >>| function
   | Some basic when Insn.(res <> empty) ->
     Insn.with_basic res basic

lib/knowledge/bap_knowledge.ml

@@ -2442,7 +2442,14 @@ module Knowledge = struct
 
   let pids = ref Pid.zero
 
-  let register_promise (s : _ slot) run =
+  type conflict += Empty : ('a,'b) slot -> conflict
+
+  let with_empty ~missing scope =
+    Knowledge.catch (scope ())
+      (function Empty _ -> Knowledge.return missing
+              | other -> Knowledge.fail other)
+
+  let register_promise (type a b)(s : (a,b) slot) run =
     Pid.incr pids;
     let pid = !pids in
     Hashtbl.add_exn s.promises pid {run; pid};
@@ -2451,9 +2458,14 @@ module Knowledge = struct
   let remove_promise (s : _ slot) pid =
     Hashtbl.remove s.promises pid
 
+  let wrap (s : _ slot) get obj =
+    let missing = Domain.empty s.dom in
+    with_empty ~missing @@ fun () ->
+    get obj
+
   let promising s ~promise:get scoped =
     let pid = register_promise s @@ fun obj ->
-      get obj >>= fun x ->
+      wrap s get obj >>= fun x ->
       if Domain.is_empty s.dom x
       then Knowledge.return ()
       else provide s obj x in
@@ -2464,7 +2476,7 @@ module Knowledge = struct
   let promise s get =
     ignore @@
     register_promise s @@ fun obj ->
-    get obj >>= fun x ->
+    wrap s get obj >>= fun x ->
     if Domain.is_empty s.dom x
     then Knowledge.return ()
     else provide s obj x
@@ -2576,6 +2588,7 @@ module Knowledge = struct
       | GT | NC -> collect_inner slot obj promises
 
 
+
   let collect : type a p. (a,p) slot -> a obj -> p Knowledge.t =
     fun slot id ->
     if Object.is_null id
@@ -2592,6 +2605,13 @@ module Knowledge = struct
         leave_slot slot id >>= fun () ->
         current slot id
 
+
+  let require (slot : _ slot) obj =
+    collect slot obj >>= fun x ->
+    if (Domain.is_empty slot.dom x)
+    then Knowledge.fail (Empty slot)
+    else !!x
+
   let resolve slot obj =
     collect slot obj >>| Opinions.choice
 
@@ -2792,10 +2812,17 @@ module Knowledge = struct
 
   module Syntax = struct
     include Knowledge.Syntax
+    include Knowledge.Let
+
     let (-->) x p = collect p x
     let (<--) p f = promise p f
     let (//) c s = Object.read c s
 
+    let (-->?) x p =
+      collect p x >>= function
+      | None -> Knowledge.fail (Empty p)
+      | Some x -> !!x
+
     let (>>=?) x f =
       x >>= function
       | None -> Knowledge.return None
@@ -2805,6 +2832,23 @@ module Knowledge = struct
       x >>| function
       | None -> None
       | Some x -> f x
+
+    let (let*?) = (>>=?)
+    let (let+?) = (>>|?)
+
+
+    let (.$[]) v s = Value.get s v
+    let (.$[]<-) v s x = Value.put s v x
+
+    let (.?[]) v s = match v.$[s] with
+      | Some v -> !!v
+      | None -> Knowledge.fail (Empty s)
+
+    let (.![]) v s =
+      let r = v.$[s] in
+      if Domain.is_empty (Slot.domain s) r
+      then Knowledge.fail (Empty s)
+      else !!r
   end
 
   module type S = sig

lib/knowledge/bap_knowledge.mli

@@ -164,6 +164,16 @@ module Knowledge : sig
       value of the property domain is returned as the result.  *)
   val collect : ('a,'p) slot -> 'a obj -> 'p t
 
+  (** [require p x] collects the property [p] and fails if it is empty.
+
+      When [require p x] fails in the scope of a {!promise},
+      {!proposal}, or in the scope of [with_empty], then the scoped
+      computation immediately returns the empty value.
+
+      @since 2.4.0
+  *)
+  val require : ('a,'p) slot -> 'a obj -> 'p t
+
 
   (** [resolve p x] resolves the multi-opinion property [p]
 
@@ -186,6 +196,7 @@ module Knowledge : sig
       then [provide p x v] diverges into a conflict.
   *)
   val provide : ('a,'p) slot -> 'a obj -> 'p -> unit t
+
   (** [suggest a p x v] suggests [v] as the value for the property [p].
 
       The same as [provide] except the provided value is predicated by
@@ -195,26 +206,35 @@ module Knowledge : sig
 
   (** [promise p f] promises to compute the property [p].
 
-      If no knowledge exists about the property [p] of
-      an object [x], then [f x] is invoked to provide an
-      initial value.
+      If the property [p] of [x] is not provided, then [f x] is
+      invoked to provide the initial value, when [p] is collected.
 
       If there are more than one promises, then they all must
       provide a consistent answer. The function [f] may refer
       to the property [p] directly or indirectly. In that case
       the least fixed point solution of all functions [g] involved
       in the property computation is computed.
+
+      @since 2.4.0 if [require] is called in the scope of the promise
+      and fails, the the whole promise immediately returns the empty
+      value of the property domain, i.e., [f] is wrapped into
+      [with_missing].
   *)
   val promise : ('a,'p) slot -> ('a obj -> 'p t) -> unit
 
-
   (** [promising p ~promise f] evaluates [f ()] under [promise] and
       retracts it after [f] is evaluated.
 
       The information provided by [promise] is only available during
       evaluation of [f ()].
 
       @since 2.2.0
+
+
+      @since 2.4.0 if [require] is called in the scope of the promise
+      and fails, the the whole promise immediately returns the empty
+      value of the property domain, i.e., [promise] (not [f]) wrapped
+      into [with_missing].
   *)
   val promising : ('a,'p) slot -> promise:('a obj -> 'p t) ->
     (unit -> 's t) -> 's t
@@ -223,6 +243,12 @@ module Knowledge : sig
 
       The same as [promise] except that it promises a value for
       an opinion-based property.
+
+      @since 2.4.0 if [require] is called in the scope of the promise
+      and fails, the the whole promise immediately returns the empty
+      value of the property domain, i.e., [f] is wrapped into
+      [with_missing].
+
   *)
   val propose : agent -> ('a, 'p opinions) slot -> ('a obj -> 'p t) -> unit
 
@@ -233,10 +259,25 @@ module Knowledge : sig
       value for an opinion-based property.
 
       @since 2.2.0
+
+      @since 2.4.0 if [require] are called in the scope of the proposal
+      and fails, the the whole proposal immediately returns the empty
+      value of the property domain, i.e., [propose] (not [f]) wrapped
+      into [with_missing].
+
   *)
   val proposing : agent -> ('a, 'p opinions) slot ->
     propose:('a obj -> 'p t) -> (unit -> 's t) -> 's t
 
+
+  (** [with_empty ~missing f x] evaluates [f ()] and if it fails on an empty
+      immediately evaluates to [return missing].
+
+      @since 2.4.0
+  *)
+  val with_empty : missing:'r -> (unit -> 'r knowledge) -> 'r knowledge
+
+
   (** state with no knowledge  *)
   val empty : state
 
@@ -333,10 +374,62 @@ module Knowledge : sig
     include Monad.Syntax.S with type 'a t := 'a t
 
 
-    (** [x-->p] is [collect p x] *)
+    (** the monadic let-binding operators.
+
+        Brings [let*] for [bind] and [let+] for [map] to the scope
+        of the [Syntax] module.
+
+        @since 2.4.0 (before that an explicit [open Knowledge.Let] was
+        required.    *)
+    include Monad.Syntax.Let.S with type 'a t := 'a t
+
+
+    (** [let*? v = x in f] evaluates to [f y] if [v] is [Some r].
+
+        Otherwise evaluates to [return None].
+
+        This let-binding operator is synonumous to [>>=?]
+
+        @since 2.4.0
+    *)
+    val (let*?) : 'a option t -> ('a -> 'b option t) -> 'b option t
+
+    (** [let+? v = x in f] evaluates to [!!(f y)] if [v] is [Some r].
+
+        Otherwise evaluates to [return None].
+
+        This let-binding operator is synonumous to [>>|?]
+
+        @since 2.4.0
+    *)
+    val (let+?) : 'a option t -> ('a -> 'b option) -> 'b option t
+
+    (** [x-->p] is [collect p x].
+
+        Example,
+        {[
+          let* addr = label-->address in
+          ...
+        ]}
+    *)
     val (-->) : 'a obj -> ('a,'p) slot -> 'p t
 
 
+    (** [x-->?p] returns property [p] if it is not empty.
+
+        Otherwise, if [x-->p] evaluates to empty or to [None]
+        fails with the empty value conflict.
+
+        Example,
+        {[
+          let* addr = label-->?address in
+          ...
+        ]}
+
+        See also {!with_empty}. *)
+    val (-->?) : 'a obj -> ('a, 'p option) slot -> 'p t
+
+
     (** [p <-- f] is [promise p f]  *)
     val (<--) : ('a,'p) slot -> ('a obj -> 'p t) -> unit
 
@@ -351,6 +444,42 @@ module Knowledge : sig
 
     (** [x >>|? f] evaluates to [f y] if [x] evaluates to [Some y].  *)
     val (>>|?) : 'a option t -> ('a -> 'b option) -> 'b option t
+
+
+    (** [x.$[p]] is the propery [p] of [x].
+
+        @since 2.4.0
+    *)
+    val (.$[]) : ('a,_) cls value -> ('a,'p) slot -> 'p
+
+
+    (** [x.$[p] <- r] updates the property [p] of [x] to [r].
+
+        Returns the value [x] with the new property. The previous
+        value is ignored so there is no merging or monotonicity check
+        involved.
+
+        @since 2.4.0 *)
+    val (.$[]<-) : ('a,'b) cls value -> ('a,'p) slot -> 'p -> ('a,'b) cls value
+
+
+    (** [x.?[p]] returns the non-[None] property [p] or fails.
+
+        The result is [return r] when [x.$[p]] is [Some r] or a
+        knowledge base conflict otherwise.
+
+        @since 2.4.0
+    *)
+    val (.?[]) : ('a,_) cls value -> ('a,'p option) slot -> 'p knowledge
+
+    (** [x.![p]] returns the property [p] or fails if it is empty.
+
+        The result is [return r] if not [Domain.is_empty dom r],
+        where [dom] is [Slot.domain p].
+
+        @since 2.4.0
+    *)
+    val (.![]) : ('a,_) cls value -> ('a,'p) slot -> 'p knowledge
   end
 
 
@@ -1388,7 +1517,6 @@ module Knowledge : sig
   module Conflict : sig
     type t = conflict = ..
 
-
     (** [to_string err] is the textual representation of the conflict [err]
 
         @since 2.2.0  *)

plugins/bil/bil_lifter.ml

@@ -289,21 +289,17 @@ let provide_bil ~enable_intrinsics () =
            require Disasm_expert.Basic.Insn.slot |>
            provide Bil.code |>
            comment "uses legacy lifters to provide BIL code.");
-  let unknown = KB.Domain.empty Bil.domain in
-  let (>>?) x f = x >>= function
-    | None -> KB.return unknown
-    | Some x -> f x in
   let enable_intrinsics = split_specs enable_intrinsics in
   KB.promise Bil.code @@ fun obj ->
-  Knowledge.collect Arch.slot obj >>= fun arch ->
-  Theory.Label.target obj >>= fun target ->
-  Knowledge.collect Memory.slot obj >>? fun mem ->
-  Knowledge.collect Disasm_expert.Basic.Insn.slot obj >>? fun insn ->
+  let* arch = KB.require Arch.slot obj in
+  let* target = Theory.Label.target obj in
+  let* mem = obj-->?Memory.slot in
+  let* insn = obj-->?Disasm_expert.Basic.Insn.slot in
   match lift ~enable_intrinsics target arch mem insn with
   | Error err ->
     info "BIL: the BIL lifter failed with %a" Error.pp err;
-    !!unknown
-  | Ok [] -> !!unknown
+    KB.return []
+  | Ok [] -> KB.return []
   | Ok bil ->
     Optimizer.run Bil.Theory.parser bil >>= fun sema ->
     let bil = Insn.bil sema in