wraps proposals into with_empty and adds more guards (#1442)

The proposals (promises with options) now can use the choice monad
interface as well as other promises. Also adds a few guards to the
existing code to make it more readable and improve performance.

Author: ivg

lib/knowledge/bap_knowledge.ml

@@ -2949,14 +2949,22 @@ module Knowledge = struct
     current slot obj >>= fun opinions ->
     provide slot obj (Opinions.add agent x opinions)
 
+  let wrap_opinion get obj =
+    with_empty ~missing:None @@ fun () ->
+    get obj >>| Option.some
+
   let propose agent s get =
     ignore @@
     register_promise s @@ fun obj ->
-    get obj >>= suggest agent s obj
+    wrap_opinion get obj >>= function
+    | None -> Knowledge.return ()
+    | Some opinions -> suggest agent s obj opinions
 
   let proposing agent s ~propose:get scoped =
     let pid = register_promise s @@ fun obj ->
-      get obj >>= suggest agent s obj in
+      wrap_opinion get obj >>= function
+      | None -> Knowledge.return ()
+      | Some opinions -> suggest agent s obj opinions in
     scoped () >>= fun r ->
     remove_promise s pid;
     Knowledge.return r

plugins/bil/bil_lifter.ml

@@ -15,15 +15,16 @@ let package = "bap"
 module Optimizer = Theory.Parser.Make(Theory.Pass.Desugar(Bil_semantics.Core))
 [@@inlined]
 
-
 let provide_bir () =
   KB.Rule.(declare ~package "reify-ir" |>
            require Theory.Semantics.slot |>
            require Bil_ir.slot |>
            provide Theory.Semantics.slot |>
            comment "reifies IR");
   KB.promise Theory.Semantics.slot @@ fun obj ->
-  KB.collect Theory.Semantics.slot obj >>| fun sema ->
+  KB.collect Theory.Semantics.slot obj >>= fun sema ->
+  KB.proceed ~unless:(KB.Value.has Term.slot sema) >>= fun () ->
+  KB.return @@
   match Bil_ir.reify @@ KB.Value.get Bil_ir.slot sema with
   | [] -> Insn.empty
   | bir -> KB.Value.put Term.slot sema bir

plugins/mips/mips.ml

@@ -90,22 +90,18 @@ module Std = struct
   include Model
 end
 
-let () =
-  let provide_delay obj =
-    let open KB.Syntax in
-    Theory.Label.target obj >>= fun target ->
-    if Theory.Target.belongs Bap_mips_target.parent target
-    then
-      KB.collect Theory.Semantics.slot obj >>| fun insn ->
-      let name = KB.Value.get Insn.Slot.name insn in
-      Hashtbl.find_and_call Std.delayed_opcodes name
-        ~if_found:(fun delay ->
-            KB.Value.put Insn.Slot.delay insn (Some delay))
-        ~if_not_found:(fun _ -> Insn.empty)
-    else !!Insn.empty in
-  Bap_main.Extension.declare @@ fun _ctxt ->
+let promise_delay_slots () =
   KB.Rule.(declare ~package:"mips" "delay-slot" |>
            require Insn.Slot.name |>
            provide Insn.Slot.delay |>
            comment "provides the delay slot length for branches");
-  Ok (KB.promise Theory.Semantics.slot provide_delay)
+  KB.promise Theory.Semantics.slot @@ fun obj ->
+  let open KB.Syntax in
+  Theory.Label.target obj >>= fun target ->
+  KB.guard (Theory.Target.belongs Bap_mips_target.parent target) >>= fun () ->
+  KB.collect Theory.Semantics.slot obj >>| fun insn ->
+  let name = KB.Value.get Insn.Slot.name insn in
+  Hashtbl.find_and_call Std.delayed_opcodes name
+    ~if_found:(fun delay ->
+        KB.Value.put Insn.Slot.delay insn (Some delay))
+    ~if_not_found:(fun _ -> Insn.empty)

plugins/mips/mips_main.ml

@@ -47,4 +47,5 @@ let () =
       register_target `mipsel (module MIPS32_le);
       register_target `mips64 (module MIPS64);
       register_target `mips64el (module MIPS64_le);
+      Mips.promise_delay_slots ();
       Mips_abi.setup ());

plugins/relocatable/rel_symbolizer.ml

@@ -200,32 +200,31 @@ let resolve_stubs () =
   KB.collect References.slot unit >>= fun refs ->
   KB.collect Theory.Label.addr label >>=? fun addr ->
   KB.collect (Value.Tag.slot Sub.stub) label >>= fun is_stub ->
-  if not (Option.is_some is_stub) then KB.return None
-  else match References.lookup refs addr with
-    | Some (Name s) -> KB.return (Some s)
-    | _ ->
-      plt_size label >>=? fun size ->
-      collect_insns size addr >>| fun bil ->
-      find_references bil |>
-      List.find_map ~f:(function
-          | Name s -> Some s
-          | Addr dst -> match References.lookup refs dst with
-            | Some (Name s) -> Some s
-            | _ -> None)
+  KB.guard (Option.is_some is_stub) >>= fun () ->
+  match References.lookup refs addr with
+  | Some (Name s) -> KB.return (Some s)
+  | _ ->
+    plt_size label >>=? fun size ->
+    collect_insns size addr >>| fun bil ->
+    find_references bil |>
+    List.find_map ~f:(function
+        | Name s -> Some s
+        | Addr dst -> match References.lookup refs dst with
+          | Some (Name s) -> Some s
+          | _ -> None)
 
 let label_for_ref = function
   | Name s -> Theory.Label.for_name s
   | Addr x -> Theory.Label.for_addr x
 
 let mark_mips_stubs_as_functions () : unit =
   KB.promise Theory.Label.is_subroutine @@ fun label ->
-  KB.collect Theory.Label.addr label >>=? fun addr ->
-  KB.collect Theory.Label.unit label >>=? fun unit ->
-  KB.collect References.slot unit >>= fun refs ->
-  KB.collect Theory.Unit.target unit >>| fun target ->
-  let is_entry = (Theory.Target.matches target "mips") &&
-                 Option.is_some (References.lookup refs addr) in
-  Option.some_if is_entry true
+  let* unit = label-->?Theory.Label.unit in
+  let* target = unit-->Theory.Unit.target in
+  KB.guard (Theory.Target.matches target "mips") >>= fun () ->
+  let* addr = label-->?Theory.Label.addr in
+  KB.collect References.slot unit >>| fun refs ->
+  Option.(some_if (is_some (References.lookup refs addr))) true
 
 let () = Extension.declare ~doc @@ fun _ctxt ->
   References.prepare ();

plugins/thumb/thumb_main.ml

@@ -222,25 +222,24 @@ module Main = struct
   let load () =
     KB.promise Theory.Semantics.slot @@ fun label ->
     KB.collect Theory.Label.encoding label >>= fun encoding ->
-    if Theory.Language.equal Target.llvm_t32 encoding then
-      KB.collect MC.Insn.slot label >>=? fun insn ->
-      KB.collect Memory.slot label >>=? fun mem ->
-      Theory.instance () >>= Theory.require >>= fun (module Core) ->
-      let module Thumb = Thumb(Core) in
-      let addr = Word.to_bitvec@@Memory.min_addr mem in
-      match decode_opcode (MC.Insn.name insn) with
-      | None -> !!Insn.empty
-      | Some opcode ->
-        try
-          Thumb.lift_insn addr opcode insn >>| fun sema ->
-          Insn.with_basic sema insn
-        with uncaught ->
-          warning "failed to decode a thumb instruction: \
-                   uncaught exception %s\nBacktrace:\n %s\n"
-            (Exn.to_string uncaught)
-            (Caml.Printexc.get_backtrace ());
-          KB.return Insn.empty
-    else KB.return Insn.empty
+    KB.guard (Theory.Language.equal Target.llvm_t32 encoding) >>= fun () ->
+    KB.collect MC.Insn.slot label >>=? fun insn ->
+    KB.collect Memory.slot label >>=? fun mem ->
+    Theory.instance () >>= Theory.require >>= fun (module Core) ->
+    let module Thumb = Thumb(Core) in
+    let addr = Word.to_bitvec@@Memory.min_addr mem in
+    match decode_opcode (MC.Insn.name insn) with
+    | None -> !!Insn.empty
+    | Some opcode ->
+      try
+        Thumb.lift_insn addr opcode insn >>| fun sema ->
+        Insn.with_basic sema insn
+      with uncaught ->
+        warning "failed to decode a thumb instruction: \
+                 uncaught exception %s\nBacktrace:\n %s\n"
+          (Exn.to_string uncaught)
+          (Caml.Printexc.get_backtrace ());
+        KB.return Insn.empty
 end
 
 let () = Bap_main.Extension.declare @@ fun _ctxt ->