reifies intrinsics into BIR functions (#1479)

lib/bap_disasm/bap_disasm_driver.ml

@@ -31,7 +31,8 @@ type jump = {
   barrier : bool;
   indirect : bool;
   resolved : Addr.Set.t;
-} [@@deriving bin_io, equal]
+  unresolved : Set.M(Theory.Label).t;
+} [@@deriving bin_io, equal, fields]
 
 let pp_encoding ppf {coding} =
   Format.fprintf ppf "%a" Theory.Language.pp 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"
@@ -533,6 +543,7 @@ type state = {
   data : Addr.Set.t;
   mems : mem list;
   debt : Machine.task list;
+  exts : Set.M(Theory.Label).t;
 } [@@deriving bin_io]
 
 let init = {
@@ -542,6 +553,7 @@ let init = {
   data = Set.empty (module Addr);
   mems = [];
   debt = [];
+  exts = Set.empty (module Theory.Label);
 }
 
 let forget_debt s = {s with debt=[]}
@@ -552,6 +564,7 @@ let equal x y =
   Map.equal equal_jump x.jmps y.jmps
 
 let subroutines x = x.funs
+let externals x = x.exts
 let blocks x = x.begs
 let jump {jmps} = Map.find jmps
 
@@ -565,18 +578,31 @@ let is_call dsts = dsts.call
 let is_barrier dsts = dsts.barrier
 
 
-let commit_calls jmps =
+let fold_calls field ~f ~init jmps  =
   Map.to_sequence jmps |>
-  KB.Seq.fold ~init:Addr.Set.empty ~f:(fun calls (_,dsts) ->
+  KB.Seq.fold ~init ~f:(fun init (_,dsts) ->
       if dsts.call then
-        Set.to_sequence dsts.resolved |>
-        KB.Seq.fold ~init:calls ~f:(fun calls addr ->
-            Theory.Label.for_addr (Word.to_bitvec addr) >>= fun dst ->
-            KB.provide Theory.Label.is_valid dst (Some true) >>= fun () ->
-            KB.provide Theory.Label.is_subroutine dst (Some true) >>| fun () ->
-            Set.add calls addr)
-      else KB.return calls)
-
+        Set.to_sequence (field dsts) |>
+        KB.Seq.fold ~init ~f:(fun calls addr ->
+            f calls addr)
+      else KB.return init)
+
+
+let commit_calls = fold_calls resolved
+    ~init:Addr.Set.empty
+    ~f:(fun calls addr ->
+        Theory.Label.for_addr (Word.to_bitvec addr) >>= fun dst ->
+        KB.provide Theory.Label.is_valid dst (Some true) >>= fun () ->
+        KB.provide Theory.Label.is_subroutine dst (Some true) >>| fun () ->
+        Set.add calls addr)
+
+let commit_externals = fold_calls unresolved
+    ~init:(Set.empty (module Theory.Label))
+    ~f:(fun exts dst ->
+        KB.return @@
+        if KB.Object.is_null dst
+        then exts
+        else Set.add exts dst)
 
 let owns mem s =
   List.exists s.debt ~f:(function
@@ -591,6 +617,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,10 +633,12 @@ 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_externals jmps >>= fun exts ->
+  let s = {funs; begs; data; jmps; mems = s.mems; debt; exts} in
   commit_calls s.jmps >>| fun funs ->
   {s with funs = Set.union s.funs funs - dels}
 
@@ -634,6 +663,7 @@ let scan mem s =
 
 let merge t1 t2 = {
   funs = Set.union t1.funs t2.funs;
+  exts = Set.union t1.exts t2.exts;
   begs = Set.union t1.begs t2.begs;
   data = Set.union t1.data t2.data;
   mems = List.rev_append t2.mems t1.mems;

lib/bap_disasm/bap_disasm_driver.mli

@@ -4,6 +4,8 @@ open Bap_image_std
 open Bap_knowledge
 open Bap_core_theory
 
+module Insn = Bap_disasm_insn
+
 type state [@@deriving bin_io]
 type insns
 type jump
@@ -14,6 +16,7 @@ val scan : mem -> state -> state knowledge
 val merge : state -> state -> state
 
 val subroutines : state -> Set.M(Addr).t
+val externals : state -> Set.M(Theory.Label).t
 val blocks : state -> Set.M(Addr).t
 val jump : state -> addr -> jump option
 

lib/bap_disasm/bap_disasm_symtab.ml

@@ -39,6 +39,7 @@ type t = {
   memory : fn Memmap.t;
   ecalls : string Addr.Map.t;
   icalls : string Addr.Map.t;
+  extern : Insn.t Map.M(Theory.Label).t;
 } [@@deriving sexp_of]
 
 
@@ -57,6 +58,7 @@ let empty = {
   memory = Memmap.empty;
   ecalls = Map.empty (module Addr);
   icalls = Map.empty (module Addr);
+  extern = Map.empty (module Theory.Label);
 }
 
 let merge m1 m2 =
@@ -75,6 +77,7 @@ let filter_calls name cfg calls =
 
 let remove t (name,entry,cfg) : t =
   if Map.mem t.addrs (Block.addr entry) then {
+    t with
     names = Map.remove t.names name;
     addrs = Map.remove t.addrs (Block.addr entry);
     memory = filter_mem t.memory name entry;
@@ -103,6 +106,7 @@ let dominators t mem = Memmap.dominators t.memory mem |> fns_of_seq
 let intersecting t mem = Memmap.intersections t.memory mem |> fns_of_seq
 let to_sequence t =
   Map.to_sequence t.addrs |> fns_of_seq |> Seq.of_list
+let externals t = Map.to_sequence t.extern
 let name_of_fn = fst
 let entry_of_fn = snd
 let span fn = span fn |> Memmap.map ~f:(fun _ -> ())
@@ -169,8 +173,17 @@ let collect_graphs disasm calls =
           then {tab with icalls = Map.set tab.icalls from name},graphs
           else {tab with ecalls = Map.set tab.ecalls from name},graphs)
 
+let collect_externals disasm =
+  Disasm.externals disasm |>
+  Set.to_sequence |>
+  KB.Seq.fold ~init:(Map.empty (module Theory.Label)) ~f:(fun extern label ->
+      let+ insn = label-->Theory.Semantics.slot in
+      Map.set extern label insn)
+
 let create disasm calls =
   let* (init,graphs) = collect_graphs disasm calls in
+  let* extern = collect_externals disasm in
+  let init = {init with extern} in
   Map.to_sequence graphs |>
   KB.Seq.fold ~init ~f:(fun tab (addr,(entry,cfg)) ->
       let+ name = Symbolizer.get_name addr in

lib/bap_disasm/bap_disasm_symtab.mli

@@ -6,6 +6,7 @@ open Image_internal_std
 
 module Disasm = Bap_disasm_driver
 module Callgraph = Bap_disasm_calls
+module Insn = Bap_disasm_insn
 
 type block = Bap_disasm_block.t
 type edge =  Bap_disasm_block.edge
@@ -31,6 +32,7 @@ val owners : t -> addr -> fn list
 val dominators : t -> mem -> fn list
 val intersecting : t -> mem -> fn list
 val to_sequence : t -> fn seq
+val externals : t -> (Theory.Label.t * Insn.t) seq
 val span : fn -> unit memmap
 
 

lib/bap_sema/bap_sema_lift.ml

@@ -336,15 +336,18 @@ let is_intrinsic sub =
   | "intrinsic" -> true
   | _ -> false
 
-let create_synthetic tid =
-  let sub = Ir_sub.create ~tid () in
+let create_synthetic ?blks ?name tid =
+  let sub = Ir_sub.create ?blks ?name ~tid () in
   let tags = List.filter_opt [
       Some Term.synthetic;
       Option.some_if (is_intrinsic sub) Ir_sub.intrinsic;
     ] in
   List.fold tags ~init:sub ~f:(fun sub tag ->
       Term.set_attr sub tag ())
 
+let has_sub prog tid =
+  Option.is_some (Term.find sub_t prog tid)
+
 let insert_synthetic prog =
   Term.enum sub_t prog |>
   Seq.fold ~init:prog ~f:(fun prog sub ->
@@ -357,12 +360,26 @@ let insert_synthetic prog =
               | Some dst -> match Ir_jmp.resolve dst with
                 | Second _ -> prog
                 | First dst ->
-                  if Option.is_some (Term.find sub_t prog dst)
+                  if has_sub prog dst
                   then prog
                   else
                     Term.append sub_t prog @@
                     create_synthetic dst)))
 
+let lift_insn ?addr insn =
+  let tid = Option.map addr ~f:Tid.for_addr in
+  List.rev @@ IrBuilder.lift_insn ?addr insn [Ir_blk.create ?tid ()]
+
+let reify_externals symtab prog =
+  Symtab.externals symtab |>
+  Seq.fold ~init:prog ~f:(fun prog (tid,insn) ->
+      if has_sub prog tid then prog
+      else
+        let blks = if KB.Value.is_empty insn
+          then None
+          else Some (lift_insn insn) in
+        let sub = create_synthetic ?blks tid in
+        Term.append sub_t prog sub)
 
 let program symtab =
   let b = Ir_program.Builder.create () in
@@ -393,12 +410,11 @@ let program symtab =
               jmp |>
               alternate_nonlocal sub |>
               link_call symtab addr sub_of_blk))) |>
+  reify_externals symtab |>
   insert_synthetic
 
 let sub blk cfg = lift_sub blk cfg
 
-let insn ?addr insn =
-  let tid = Option.map addr ~f:Tid.for_addr in
-  List.rev @@ IrBuilder.lift_insn ?addr insn [Ir_blk.create ?tid ()]
 
+let insn = lift_insn
 let insns = IrBuilder.insns

plugins/primus_lisp/primus_lisp_semantic_primitives.ml

@@ -722,8 +722,11 @@ module Primitives(CT : Theory.Core)(T : Target) = struct
           CT.set (ivar i s) !!x)
 
     let invoke_symbol name =
-      let name = KB.Name.(unqualified@@read name) in
-      let* dst = Theory.Label.for_name (sprintf "intrinsic:%s" name) in
+      let name = KB.Name.create
+          ~package:"intrinsic"
+          KB.Name.(unqualified@@read name) in
+      let* dst = Theory.Label.for_name (KB.Name.show name) in
+      KB.provide Primus.Lisp.Semantics.name dst (Some name) >>= fun () ->
       KB.provide Theory.Label.is_subroutine dst (Some true) >>= fun () ->
       CT.goto dst