calls Primus Lisp to reify intrinsics

lib/bap_disasm/bap_disasm_driver.ml

@@ -31,6 +31,7 @@ type jump = {
   barrier : bool;
   indirect : bool;
   resolved : Addr.Set.t;
+  unresolved : Set.M(Theory.Label).t;
 } [@@deriving bin_io, equal]
 
 let pp_encoding ppf {coding} =
@@ -387,7 +388,8 @@ let collect_dests source code =
     call = Insn.(is call insn);
     barrier = Insn.(is barrier insn);
     indirect = false;
-    resolved = Set.empty (module Addr)
+    resolved = Set.empty (module Addr);
+    unresolved = Set.empty (module Theory.Label);
   } in
   KB.Value.get Insn.Slot.dests insn |> function
   | None -> KB.return init
@@ -396,15 +398,23 @@ let collect_dests source code =
     KB.Seq.fold ~init ~f:(fun dest label ->
         get_encoding label >>=
         merge_encodings dest.encoding >>= fun encoding ->
+        KB.collect Theory.Label.is_subroutine label >>= fun is_call ->
         KB.collect Theory.Label.addr label >>| function
         | Some d -> {
             dest with
             encoding;
+            call = dest.call ||
+                   Option.value is_call ~default:false;
             resolved =
               Set.add dest.resolved @@
-              Word.code_addr encoding.target d
+              Word.code_addr encoding.target d;
           }
-        | None -> {dest with indirect=true; encoding})
+        | None -> {
+            dest with
+            indirect=true;
+            unresolved = Set.add dest.unresolved label;
+            encoding;
+          })
 
 let pp_addr_opt ppf = function
   | None -> Format.fprintf ppf "Unk"
@@ -577,6 +587,14 @@ let commit_calls jmps =
             Set.add calls addr)
       else KB.return calls)
 
+let reify_unresolved jmps =
+  Map.to_sequence jmps |>
+  KB.Seq.iter ~f:(fun (_,{unresolved}) ->
+      Set.to_sequence unresolved |>
+      KB.Seq.iter ~f:(fun label ->
+          KB.ignore_m @@
+          KB.collect Theory.Semantics.slot label))
+
 
 let owns mem s =
   List.exists s.debt ~f:(function
@@ -591,6 +609,7 @@ let merge_dests d1 d2 = {
   barrier = d1.barrier || d2.barrier;
   indirect = d1.indirect || d2.indirect;
   resolved = Set.union d1.resolved d2.resolved;
+  unresolved = Set.union d1.unresolved d2.unresolved;
 }
 
 let scan_step ?(code=empty) ?(data=empty) ?(funs=empty) s mem =
@@ -606,11 +625,13 @@ let scan_step ?(code=empty) ?(data=empty) ?(funs=empty) s mem =
   let begs = Set.union s.begs begs - dels in
   let jmps = Map.filter_map jmps ~f:(fun dsts ->
       let resolved = dsts.resolved - data in
-      if Set.is_empty resolved && not dsts.indirect
+      if Set.is_empty resolved &&
+         not dsts.indirect
       then None
       else Some {dsts with resolved}) in
   let s = {funs; begs; data; jmps; mems = s.mems; debt} in
-  commit_calls s.jmps >>| fun funs ->
+  commit_calls s.jmps >>= fun funs ->
+  reify_unresolved s.jmps >>| fun () ->
   {s with funs = Set.union s.funs funs - dels}
 
 let already_scanned mem s =

plugins/primus_lisp/primus_lisp_main.ml

@@ -310,6 +310,19 @@ module Semantics = struct
     KB.Name.create ~package:(Insn.encoding insn) (Insn.name insn) |>
     Option.some
 
+  let translate_intrinsic_to_name () =
+    KB.Rule.(begin
+        declare "translate-intrinsic-to-lisp-name" |>
+        require Theory.Label.name |>
+        provide Lisp.Semantics.name |>
+        comment "translate all intrinsic functions to Lisp calls"
+      end);
+    KB.promise Lisp.Semantics.name @@ fun this ->
+    let*? name = this-->Theory.Label.name in
+    let name = KB.Name.read name in
+    KB.guard (String.equal "intrinsic" (KB.Name.package name)) >>| fun () ->
+    Some name
+
   let strip_lisp_extension = String.chop_suffix ~suffix:".lisp"
 
   let collect_features folder =
@@ -344,6 +357,7 @@ module Semantics = struct
   let enable_lifter sites =
     translate_ops_to_args ();
     translate_opcode_to_name ();
+    translate_intrinsic_to_name ();
     load_lisp_sources sites;
 end