moves knowledge base rules from the library to the plugin (#1403)

They all fit nicely into the disassemble plugin and it also opens an
opportunity to introduce command-line parameters for the rules. None
are added so far, but its good to have this option.

Author: ivg

lib/bap/bap.mli

@@ -6773,6 +6773,14 @@ module Std : sig
         (** [ops insn] gives an access to [insn]'s operands.   *)
         val ops  : ('a,'k) t -> op array
 
+        (** [subs insn] an array of subinstructions.
+
+            An instruction can contain subinstructions, which could be
+            accessed with this function. Returns an empty array if
+            there are no subinstructions.
+
+            @since 2.5.0 *)
+        val subs : ('a,'k) t -> ('a,'k) t array
       end
 
       (** Trie maps over instructions  *)
@@ -7029,6 +7037,12 @@ module Std : sig
 
       (** [slot] for accessing the sequence number of a subinstruction.  *)
       val slot : (Theory.program, t option) KB.slot
+
+
+      (** [fresh] evaluates to a freshly generated sequence number.
+
+          @since 2.5.0  *)
+      val fresh : tid knowledge
     end
 
 

lib/bap/bap_project.ml

@@ -39,163 +39,6 @@ let memory_slot = KB.Class.property Theory.Unit.cls "unit-memory"
     ~desc:"annotated memory regions of the unit"
     Memmap.domain
 
-module Symbols = struct
-  open KB.Let
-  open KB.Syntax
-
-  module Addr = struct
-    include Bitvec
-    include Bitvec_order
-    include Bitvec_binprot.Functions
-    include Bitvec_sexp.Functions
-  end
-
-  type table = {
-    roots : Set.M(Addr).t;
-    names : string Map.M(Addr).t;
-    aliases : Set.M(String).t Map.M(Addr).t;
-  } [@@deriving compare, equal, bin_io, sexp]
-
-  let empty = {
-    roots = Set.empty (module Addr);
-    names = Map.empty (module Addr);
-    aliases = Map.empty (module Addr);
-  }
-
-  let slot = KB.Class.property Theory.Unit.cls
-      ~package:"bap" "symbol-table"
-      ~persistent:(KB.Persistent.of_binable (module struct
-                     type t = table [@@deriving bin_io]
-                   end)) @@
-    KB.Domain.flat ~empty ~equal:equal_table "symbols"
-
-  let is_ident s =
-    String.length s > 0 &&
-    (Char.is_alpha s.[0] || Char.equal s.[0] '_') &&
-    String.for_all s ~f:(fun c -> Char.is_alphanum c ||
-                                  Char.equal c '_')
-
-  let from_spec t =
-    let collect fld = Ogre.collect Ogre.Query.(select @@ from fld) in
-    let open Ogre.Let in
-    let to_addr =
-      let m = Bitvec.modulus (Theory.Target.code_addr_size t) in
-      let n = Theory.Target.code_alignment t / Theory.Target.byte t in
-      let mask = Int64.(lnot (of_int n - 1L)) in
-      fun x ->
-        let x = Int64.(x land mask) in
-        Bitvec.(int64 x mod m) in
-    let add_alias tab addr alias = {
-      tab with aliases = Map.update tab.aliases addr ~f:(function
-        | None -> Set.singleton (module String) alias
-        | Some names -> Set.add names alias)
-    } in
-    let pp_comma ppf () = Format.pp_print_string ppf ", " in
-    let pp_addrs =
-      Format.pp_print_list ~pp_sep:pp_comma Bitvec.pp
-    and pp_names =
-      Format.pp_print_list ~pp_sep:pp_comma Format.pp_print_string in
-    let* roots =
-      let+ roots =
-        let* starts = collect Image.Scheme.code_start in
-        let* values = collect Image.Scheme.symbol_value in
-        let+ entry = Ogre.request Image.Scheme.entry_point in
-        let roots = Seq.append starts (Seq.map ~f:fst values) in
-        match entry with
-        | None -> roots
-        | Some entry -> Seq.cons entry roots in
-      Seq.fold roots ~init:(Set.empty (module Bitvec_order))
-        ~f:(fun xs x -> Set.add xs (to_addr x)) in
-    let+ named_symbols = collect Image.Scheme.named_symbol in
-    let init = {empty with roots},
-               Bap_relation.empty Bitvec.compare String.compare in
-    Seq.fold named_symbols ~init ~f:(fun (tab,rel) (data,name) ->
-        let addr = to_addr data in
-        if Set.mem roots addr && is_ident name
-        then tab,Bap_relation.add rel (to_addr data) name
-        else add_alias tab addr name, rel) |> fun (table,rel) ->
-    Bap_relation.matching rel table
-      ~saturated:(fun k v t -> {
-            t with names = Map.add_exn t.names k v
-          })
-      ~unmatched:(fun reason t -> match reason with
-          | Non_injective_fwd (addrs,name) ->
-            info "the symbol %s has ambiguous addresses: %a@\n"
-              name pp_addrs addrs;
-            t
-          | Non_injective_bwd (names,addr) ->
-            info "the symbol at %a has ambiguous names: %a@\n"
-              Bitvec.pp addr pp_names names;
-            t)
-
-  let build_table t spec = match Ogre.eval (from_spec t) spec with
-    | Ok x -> x
-    | Error err ->
-      invalid_argf "Malformed ogre specification: %s"
-        (Error.to_string_hum err) ()
-
-  let collect_inputs from obj f =
-    KB.collect Theory.Label.unit obj >>=? fun unit ->
-    KB.collect Theory.Label.addr obj >>=? fun addr ->
-    let+ data = KB.collect from unit in
-    f data addr
-
-  let promised_table : unit =
-    KB.promise slot @@ fun unit ->
-    let* t = KB.collect Theory.Unit.target unit in
-    let+ s = KB.collect Image.Spec.slot unit in
-    build_table t s
-
-  let promised_roots : unit =
-    KB.Rule.(begin
-        declare "provides roots" |>
-        require Image.Spec.slot |>
-        provide Theory.Label.is_subroutine |>
-        comment "computes roots from spec";
-      end);
-    KB.promise Theory.Label.is_subroutine @@ fun obj ->
-    collect_inputs slot obj @@ fun {roots} addr ->
-    Option.some_if (Set.mem roots addr) true
-
-
-  let names_agent = KB.Agent.register
-      ~package:"bap" "specification-provider"
-      ~desc:"provides names obtained from the image specification."
-
-  let promised_names : unit =
-    KB.Rule.(begin
-        declare "provides names" |>
-        require Image.Spec.slot |>
-        provide Theory.Label.possible_name |>
-        comment "computes symbol names from spec";
-      end);
-    KB.propose names_agent Theory.Label.possible_name @@ fun obj ->
-    collect_inputs slot obj @@ fun {names} addr ->
-    Map.find names addr
-
-
-  let promised_aliases : unit =
-    KB.Rule.(begin
-        declare "provides aliases" |>
-        require Image.Spec.slot |>
-        provide Theory.Label.possible_name |>
-        comment "computes symbol aliases (names) from spec";
-      end);
-    KB.promise Theory.Label.aliases @@ fun obj ->
-    let* unit = KB.collect Theory.Label.unit obj in
-    let* addr = KB.collect Theory.Label.addr obj in
-    match unit,addr with
-    | None,_|_,None -> KB.return (Set.empty (module String))
-    | Some unit, Some addr ->
-      let+ {aliases} = KB.collect slot unit in
-      match Map.find aliases addr with
-      | None -> Set.empty (module String)
-      | Some aliases -> aliases
-end
-
-
-
-
 let with_filename spec target _code memory path f =
   let open KB.Syntax in
   let width = Theory.Target.code_addr_size target in

lib/bap_disasm/bap_disasm_basic.ml

@@ -319,7 +319,7 @@ module Insn = struct
     encoding : string;
     code : int;
     name : string;
-    asm  : bytes;
+    asm  : string;
     kinds: kind list;
     opers: Op.t array;
     subs : ins_info array;
@@ -342,14 +342,18 @@ module Insn = struct
 
   let name {name = x} = x
   let code op = op.code
-  let asm  x = Bytes.to_string x.asm
+  let asm  x = x.asm
   let ops  x = x.opers
   let kinds x = x.kinds
   let subs x = x.subs
   let is op x =
     let equal x y = Kind.compare x y = 0 in
     List.mem ~equal op.kinds x
 
+  let normalize_asm asm =
+    String.substr_replace_all asm ~pattern:"\t"
+      ~with_:" " |> String.strip
+
   let rec create ?parent ~asm ~kinds dis ~insn =
     let subs = Hashtbl.create (module Int) in
     let opers =
@@ -379,8 +383,8 @@ module Insn = struct
       if asm then
         let data = Bytes.create (C.insn_asm_size !!dis ~insn) in
         C.insn_asm_copy !!dis ~insn data;
-        data
-      else Bytes.empty in
+        normalize_asm @@ Bytes.to_string data
+      else "" in
     let kinds =
       if kinds then
         List.fold Kind.all ~init:[] ~f:(fun ks k ->
@@ -416,7 +420,7 @@ let sexp_of_full_insn = sexp_of_insn
 let compare_full_insn i1 i2 =
   let open Insn in
   let r1 = Int.compare i1.code i2.code in
-  if r1 <> 0 then Bytes.compare i1.asm i2.asm
+  if r1 <> 0 then String.compare i1.asm i2.asm
   else r1
 
 

lib/bap_disasm/bap_disasm_insn.ml

@@ -82,11 +82,6 @@ end
 type t = Theory.Semantics.t
 type op = Op.t [@@deriving bin_io, compare, sexp]
 
-let normalize_asm asm =
-  String.substr_replace_all asm ~pattern:"\t"
-    ~with_:" " |> String.strip
-
-
 module Slot = struct
   type 'a t = (Theory.Effect.cls, 'a) KB.slot
   let empty = "#undefined"
@@ -111,19 +106,6 @@ module Slot = struct
       ~public:true
       ~desc:"an assembly string"
 
-  let provide_asm : unit =
-    KB.Rule.(begin
-        declare ~package:"bap" "asm-of-basic" |>
-        require Insn.slot |>
-        provide asm |>
-        comment "provides the assembly string";
-      end);
-    let open KB.Syntax in
-    KB.promise Theory.Semantics.slot @@ fun label ->
-    let+ insn = label-->?Insn.slot in
-    KB.Value.put asm Theory.Semantics.empty @@
-    normalize_asm @@ Insn.asm insn
-
   let sexp_of_op = function
     | Op.Reg r -> Sexp.Atom (Reg.name r)
     | Op.Imm w -> sexp_of_int64 (Imm.to_int64 w)
@@ -307,7 +289,7 @@ let write init ops =
 let set_basic effect insn : t =
   write effect Slot.[
       name <-- Insn.name insn;
-      asm <-- normalize_asm (Insn.asm insn);
+      asm <-- Insn.asm insn;
       ops <-- Some (Insn.ops insn);
     ]
 
@@ -337,7 +319,7 @@ let should = must
 let shouldn't = mustn't
 
 let name = KB.Value.get Slot.name
-let asm = KB.Value.get Slot.asm
+let asm  = KB.Value.get Slot.asm
 let bil insn = KB.Value.get Bil.slot insn
 let ops s = match KB.Value.get Slot.ops s with
   | None -> [||]
@@ -447,41 +429,6 @@ module Seqnum = struct
   let fresh = KB.Syntax.(freshnum >>= label)
 end
 
-
-
-let provide_sequence_semantics () =
-  let open KB.Syntax in
-  KB.promise Theory.Semantics.slot @@ fun obj ->
-  KB.collect Insn.slot obj >>= function
-  | None -> !!Theory.Semantics.empty
-  | Some insn when not (String.equal (Insn.name insn) "seq") ->
-    !!Theory.Semantics.empty
-  | Some insn -> match Insn.subs insn with
-    | [||] -> !!Theory.Semantics.empty
-    | subs ->
-      Theory.instance () >>= Theory.require >>= fun (module CT) ->
-      let subs = Array.to_list subs |>
-                 List.map ~f:(fun sub ->
-                     Seqnum.fresh >>| fun lbl ->
-                     lbl,sub) in
-      KB.all subs >>=
-      KB.List.map ~f:(fun (obj,sub) ->
-          KB.provide Insn.slot obj (Some sub) >>= fun () ->
-          KB.collect Theory.Semantics.slot obj >>= fun sema ->
-          let nil = Theory.Effect.empty Theory.Effect.Sort.bot in
-          CT.seq (CT.blk obj !!nil !!nil) !!sema) >>=
-      KB.List.reduce ~f:(fun s1 s2 -> CT.seq !!s1 !!s2) >>| function
-      | None -> empty
-      | Some sema -> with_basic sema insn
-
-let () =
-  let open KB.Rule in
-  declare "sequential-instruction" |>
-  require Insn.slot |>
-  provide Theory.Semantics.slot |>
-  comment "computes sequential instructions semantics";
-  provide_sequence_semantics ()
-
 let () =
   Data.Write.create ~pp:Adt.pp () |>
   add_writer ~desc:"Abstract Data Type pretty printing format"

lib/bap_disasm/bap_disasm_insn.mli

@@ -46,6 +46,7 @@ module Seqnum : sig
   type t = int
   val label : ?package:string -> t -> Theory.Label.t KB.t
   val slot : (Theory.program, t option) KB.slot
+  val fresh : tid KB.t
 end
 
 module Slot : sig

lib/bap_image/bap_memory.ml

@@ -446,7 +446,6 @@ include Printable.Make(struct
 
 let hexdump t = Format.asprintf "%a" pp_hex t
 
-
 let domain = KB.Domain.optional "mem"
     ~equal:(fun x y ->
         Addr.equal x.addr y.addr &&
@@ -457,30 +456,3 @@ let slot = KB.Class.property ~package:"bap"
     Theory.Program.cls "mem" domain
     ~public:true
     ~desc:"a memory region occupied by the program"
-
-let () =
-  let open KB.Syntax in
-  KB.promise Theory.Label.addr @@ fun label ->
-  KB.collect slot label >>|? fun mem ->
-  Some (Addr.to_bitvec (min_addr mem))
-
-let () =
-  KB.Rule.(begin
-      declare ~package:"bap" "code-of-mem" |>
-      require slot |>
-      provide Theory.Semantics.code |>
-      comment "extracts the memory contents"
-    end);
-  let open KB.Syntax in
-  KB.promise Theory.Semantics.slot @@ fun label ->
-  let+ {data; off; size} = label-->?slot in
-  let empty = KB.Value.empty Theory.Semantics.cls in
-  KB.Value.put Theory.Semantics.code empty @@
-  Some (Bigstring.to_string ~pos:off ~len:size data)
-
-let () =
-  let open KB.Rule in
-  declare ~package:"bap" "addr-of-mem" |>
-  require slot |>
-  provide Theory.Label.addr |>
-  comment "addr of the first byte"

lib/bap_types/bap_arch.ml

@@ -84,17 +84,6 @@ module T = struct
       Theory.Unit.cls "unit-arch" domain
       ~persistent
 
-  let _arch_of_unit_ : unit =
-    KB.Rule.(declare ~package:"bap" "arch-of-unit" |>
-             require Theory.Label.unit |>
-             require unit_slot |>
-             provide slot |>
-             comment "propagates arch from the unit");
-    let open KB.Syntax in
-    KB.promise slot @@ fun obj ->
-    KB.collect Theory.Label.unit obj >>= function
-    | None -> KB.return `unknown
-    | Some unit -> KB.collect unit_slot unit
 end
 
 include T