diff --git a/lib/bap_disasm/bap_disasm_driver.ml b/lib/bap_disasm/bap_disasm_driver.ml index 363e00d15..451e5dbb0 100644 --- a/lib/bap_disasm/bap_disasm_driver.ml +++ b/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; diff --git a/lib/bap_disasm/bap_disasm_driver.mli b/lib/bap_disasm/bap_disasm_driver.mli index 1e48a5083..7d2563eaf 100644 --- a/lib/bap_disasm/bap_disasm_driver.mli +++ b/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 diff --git a/lib/bap_disasm/bap_disasm_symtab.ml b/lib/bap_disasm/bap_disasm_symtab.ml index 6f11a3104..ae4583eae 100644 --- a/lib/bap_disasm/bap_disasm_symtab.ml +++ b/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 diff --git a/lib/bap_disasm/bap_disasm_symtab.mli b/lib/bap_disasm/bap_disasm_symtab.mli index 94ee836df..3ee70c72b 100644 --- a/lib/bap_disasm/bap_disasm_symtab.mli +++ b/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 diff --git a/lib/bap_sema/bap_sema_lift.ml b/lib/bap_sema/bap_sema_lift.ml index ffcf6e882..5c489734e 100644 --- a/lib/bap_sema/bap_sema_lift.ml +++ b/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; @@ -345,6 +345,9 @@ let create_synthetic tid = 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 diff --git a/plugins/primus_lisp/primus_lisp_semantic_primitives.ml b/plugins/primus_lisp/primus_lisp_semantic_primitives.ml index 317daec7a..cdeed6dcc 100644 --- a/plugins/primus_lisp/primus_lisp_semantic_primitives.ml +++ b/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