overhauls the target/architecture abstraction (3/n) (#1227)

In this episode, we liberate `bap mc` and `bap objdump` from the bonds
of the `Arch.t` representation. We also add the systemz lifter for
demonstration purposes. Of course, the lifter is minimal and far from
being usable, but that serves well its didactic purposes.

The interface of the `bap mc` command is preserved but is extended
with a few more command-line options that provide a great deal of
flexibility. Not only it is now possible to specify the target and
encoding, but it is now possible to pass options directly to the
backend, which is useful for disassembling targets that are not yet
known to BAP. Below is an excerpt from the bap-mc man page
(see bap mc --help)

```
       SETTING ARCHITECHTURE

       The target architecture is controlled by several groups of options that
       can not be used together:

       - arch;
       - target and encoding;
       - triple, backend, cpu, bits, and order.

       The arch option provides the least control but is easiest to use. It
       relies on the dependency-injection mechanism and lets the target
       support packages (plugins that implement support for the given
       architecture) do their best to guess the target and encoding that
       matches the provided name. Use the common names for the architecture
       and it should work. You can use the bits and order options to give more
       hints to the target support packages. They default to 32 and little
       correspondingly.

       The target and encoding provides precise control over the selection of
       the target and the encoding that is used to represent machine
       instructions. The encoding field can be omitted and will be deduced
       from the target. Use  bap list targets and  bap list encodings to get
       the list of supported targets and encodings respectivly.

       Finally, the triple, backend, cpu,... group of options provides the
       full control over the disassembler backend and bypasses the
       dependency-injection mechanism to pass the specified options directly
       to the corresponding backends. This enables disassembling of targets
       and encodings that are not yet supported by BAP. The meanings of the
       options totally depend on the selected backend and they are passed as
       is to the corresponding arguments of the Disasm_expert.Basic.create
       function. The bits and order defaults to 32 and little corresondingly
       and are used to specify the number of bits in the target's addresses
       and the order of bytes in the word. This group of options is useful
       during the implementation and debugging of new targets and thus is
       reserved for experts. Note, when this group is used the semantics of
       the instructions will not be provided as it commonly requires the
       target specification.
```

Author: ivg

lib/arm/arm_target.ml

@@ -57,7 +57,7 @@ let flags64 = [
 
 let vars64 = gp64 @< fp64 @< sp64 @< lr64 @< flags64 @< [data64]
 
-let parent = CT.Target.declare "arm"
+let parent = CT.Target.declare ~package "arm"
 
 module type v4 = sig
 end
@@ -81,6 +81,7 @@ module type ARM = sig
   val v7fp : CT.Target.t
   val v7a : CT.Target.t
   val v7afp : CT.Target.t
+  val v7m : CT.Target.t
   val v8a : CT.Target.t
   val v81a : CT.Target.t
   val v82a : CT.Target.t
@@ -131,16 +132,18 @@ module Family (Order : Endianness) = struct
   let v6m   = v6 <: "armv6-m"
 
   let v7 = if not is_bi_endian then v6t2 <: "armv7"
-    else CT.Target.declare ~package (ordered "armv4")
+    else CT.Target.declare ~package (ordered "armv7")
         ~parent
-        ~nicknames:["armv4"]
+        ~nicknames:["armv7"]
         ~bits:32
         ~byte:8
         ~endianness
         ~code:data
         ~data:data
         ~vars:vars32
 
+  let v7m = v7 <: "armv7-m"
+
   let v7fp  = CT.Target.declare ~package (ordered "armv7+fp") ~parent:v7
       ~nicknames:["armv7+fp"]
       ~vars:vars32_fp
@@ -250,8 +253,7 @@ let enable_loader () =
     | "arm","v84a" -> Family.v84a
     | "arm","v85a" -> Family.v85a
     | "arm","v86a" -> Family.v86a
-    | "thumb", "v4" -> Family.v4t
-    | "thumb", "v5" -> Family.v5t
+    | "thumb",_     -> Family.v7m
     | "aarch64",_   -> Family.v86a
     | _ -> Family.v7
 
@@ -367,43 +369,39 @@ module Encodings = struct
     symbols_encoding
 end
 
-let (>>=?) x f = x >>= function
-  | None -> !!CT.Language.unknown
-  | Some x -> f x
 
 let compute_encoding_from_symbol_table default label =
+  let (>>=?) x f = x >>= function
+    | None -> !!default
+    | Some x -> f x in
   KB.collect CT.Label.unit label >>=? fun unit ->
   KB.collect CT.Label.addr label >>=? fun addr ->
   KB.collect Encodings.slot unit >>= fun encodings ->
   KB.return @@ match Map.find encodings addr with
   | Some x -> x
   | None -> default
 
-(* here less than means: was introduced before *)
-let (<) t p = not (CT.Target.belongs p t)
-let (<=) t p = CT.Target.equal t p || t < p
-let (>=) = CT.Target.belongs
-
+(* here t < p means that t was introduced before p *)
+let (>=) t p = CT.Target.belongs t p
+let (<) t p = t >= p && not (p >= t)
+let (<=) t p = t = p || t < p
 let is_arm = CT.Target.belongs parent
 
-let before_thumb2 t =
-  t < LE.v6t2 ||
-  t < EB.v6t2
-
-let is_64bit t =
-  t >= LE.v8a ||
-  t >= EB.v8a ||
-  t >= Bi.v8a
+let before_thumb2 t = t < LE.v6t2 || t < EB.v6t2
+let is_64bit t = LE.v8a <= t || EB.v8a <= t || Bi.v8a <= t
+let is_thumb_only t = LE.v7m <= t || EB.v7m <= t || Bi.v7m <= t
 
 let guess_encoding label target =
   if is_arm target then
     if before_thumb2 target
     then compute_encoding_from_symbol_table llvm_a32 label
     else KB.return @@
-      if is_64bit target then llvm_a64 else llvm_a32
+      if is_64bit target then llvm_a64 else
+      if is_thumb_only target
+      then llvm_t32
+      else llvm_a32
   else KB.return CT.Language.unknown
 
-
 let enable_decoder () =
   let open KB.Syntax in
   register llvm_a32 "armv7";
@@ -412,6 +410,7 @@ let enable_decoder () =
   KB.promise CT.Label.encoding @@ fun label ->
   CT.Label.target label >>= guess_encoding label
 
+
 let load () =
   enable_loader ();
   enable_arch ();

lib/bap_core_theory/bap_core_theory.mli

@@ -1255,6 +1255,12 @@ module Theory : sig
     *)
     val get : ?package:string -> string -> t
 
+    (** [read ?package name] is a synonym for [get ?package name].
+
+        Introduces for the consistency with the [Enum.S] interface.
+    *)
+    val read : ?package:string -> string -> t
+
     (** [declared ()] is the list of declared targets.
         The order is unspecified, see also {!families}. The list
         doesn't include the [unknown] target. *)
@@ -1694,6 +1700,9 @@ module Theory : sig
 
       (** the hash value of the enum  *)
       val hash : t -> int
+
+      (** [members ()] the list of all members of the enumeration type. *)
+      val members : unit -> t list
     end
 
     (** Creates a new enumerated type.  *)

lib/bap_core_theory/bap_core_theory_target.ml

@@ -35,6 +35,7 @@ module Enum = struct
     val domain : t KB.domain
     val persistent : t KB.persistent
     val hash : t -> int
+    val members : unit -> t list
   end
 
   module Make() = struct
@@ -61,6 +62,7 @@ module Enum = struct
     let unknown = Name.of_string ":unknown"
     let is_unknown = Name.equal unknown
     let hash = Name.hash
+    let members () = Hash_set.to_list elements
     include Base.Comparable.Make(Name)
     include (Name : Stringable.S with type t := t)
     include (Name : Pretty_printer.S with type t := t)
@@ -203,6 +205,8 @@ let get ?package name =
   then invalid_argf "Unknown target %s" (Name.to_string name) ();
   name
 
+let read = get
+
 let info name = match Hashtbl.find targets name with
   | None -> unknown
   | Some t -> t

lib/bap_core_theory/bap_core_theory_target.mli

@@ -31,6 +31,7 @@ val declare :
   string -> t
 
 val get : ?package:string -> string -> t
+val read : ?package:string -> string -> t
 val lookup : ?package:string -> string -> t option
 val unknown : t
 val is_unknown : t -> bool
@@ -76,6 +77,7 @@ module Enum : sig
     val domain : t KB.domain
     val persistent : t KB.persistent
     val hash : t -> int
+    val members : unit -> t list
   end
 
   module Make() : S

lib/bap_image/bap_memory.ml

@@ -461,3 +461,16 @@ 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 () =
+  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_systemz/bap_systemz_target.ml

@@ -0,0 +1,40 @@
+open Core_kernel
+open Bap_core_theory
+
+let package = "bap"
+
+type r64 and r32 and r16 and r8
+
+type 'a bitv = 'a Theory.Bitv.t Theory.Value.sort
+
+let r64 : r64 bitv = Theory.Bitv.define 64
+let r32 : r32 bitv = Theory.Bitv.define 32
+let r16 : r16 bitv = Theory.Bitv.define 16
+let r8  : r8  bitv = Theory.Bitv.define 8
+let bool = Theory.Bool.t
+
+let reg t n = Theory.Var.define t n
+
+let array ?(index=string_of_int) t pref size =
+  List.init size ~f:(fun i -> reg t (pref ^ index i))
+
+let untyped = List.map ~f:Theory.Var.forget
+let (@<) xs ys = untyped xs @ untyped ys
+
+let mems = Theory.Mem.define r64 r8
+
+let gpr = array r64 "R" 16
+let fpr = array r64 "F" 16
+let mem = reg mems "mem"
+
+let vars = gpr @< fpr @< [mem]
+
+let parent = Theory.Target.declare ~package "systemz"
+
+let z9 = Theory.Target.declare ~package "systemz9" ~parent
+    ~bits:64
+    ~code:mem
+    ~data:mem
+    ~vars
+
+let llvm_encoding = Theory.Language.declare ~package "llvm-systemz"

lib/bap_systemz/bap_systemz_target.mli

@@ -0,0 +1,21 @@
+open Bap_core_theory
+
+
+type r64 and r32 and r16 and r8
+
+type 'a bitv = 'a Theory.Bitv.t Theory.Value.sort
+
+val r64 : r64 bitv
+val r32 : r32 bitv
+val r16 : r16 bitv
+val r8  : r8 bitv
+
+val mem : (r64, r8) Theory.Mem.t Theory.var
+val gpr : r64 Theory.Bitv.t Theory.var list
+val fpr : r64 Theory.Bitv.t Theory.var list
+
+val parent : Theory.Target.t
+
+val z9 : Theory.Target.t
+
+val llvm_encoding : Theory.Language.t

lib/bap_types/bap_arch.ml

@@ -75,6 +75,7 @@ module T = struct
   let persistent = KB.Persistent.of_binable (module struct
       type t = arch [@@deriving bin_io]
     end)
+
   let slot = KB.Class.property ~package:"bap"
       Theory.Program.cls "arch" domain
       ~persistent

lib/bap_types/bap_ir.ml

@@ -115,7 +115,7 @@ module Tid = struct
     then intern str
     else match str.[0] with
       | '%' -> parse @@ sprintf "#<%s 0x%s>"
-          (KB.Name.show (KB.Class.name Theory.Program.Semantics.cls))
+          (KB.Name.show (KB.Class.name Theory.Semantics.cls))
           (String.subo ~pos:1 str)
       | '@' -> intern (String.subo ~pos:1 str)
       | _ -> intern str
@@ -1251,7 +1251,7 @@ module Term = struct
     end)
 
   let slot = Knowledge.Class.property
-      Theory.Program.Semantics.cls "bir" domain
+      Theory.Semantics.cls "bir" domain
       ~package ~persistent
       ~public:true
       ~desc:"BIL semantics in a graphical IR"

lib/bap_types/bap_ir.mli

@@ -69,7 +69,7 @@ end
 module Term : sig
   type 'a t = 'a term
 
-  val slot : (Theory.Program.Semantics.cls, blk term list) KB.slot
+  val slot : (Theory.Semantics.cls, blk term list) KB.slot
 
   val clone : 'a t -> 'a t
   val same : 'a t -> 'a t -> bool