reifies intrinsics into BIR functions

lib/bap_disasm/bap_disasm_driver.ml

@@ -32,7 +32,7 @@ type jump = {
   indirect : bool;
   resolved : Addr.Set.t;
   unresolved : Set.M(Theory.Label).t;
-} [@@deriving bin_io, equal]
+} [@@deriving bin_io, equal, fields]
 
 let pp_encoding ppf {coding} =
   Format.fprintf ppf "%a" Theory.Language.pp coding
@@ -543,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 = {
@@ -552,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=[]}
@@ -562,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
 
@@ -575,26 +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)
-
-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))
-
+        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
@@ -629,9 +637,9 @@ let scan_step ?(code=empty) ?(data=empty) ?(funs=empty) s mem =
          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 ->
-  reify_unresolved s.jmps >>| fun () ->
+  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}
 
 let already_scanned mem s =
@@ -655,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,8 +336,8 @@ 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;
@@ -363,6 +363,18 @@ let insert_synthetic prog =
                     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) ->
+      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 +405,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