From cff63f896852dcb3f83a2c0b205c8855036e6414 Mon Sep 17 00:00:00 2001
From: ivg <ivg@ieee.org>
Date: Thu, 24 Sep 2020 13:37:26 -0400
Subject: [PATCH] overhauls the target/architecture abstraction (1/n)

Introduces Theory.Target.t that superseeds Bap.Std.Arch.t. The old
representation suffered from a few problems that we inherited from
LLVM. The main issue is that Arch.t is not extensible and in order
to add a new architecture the Bap.Std code shall be changed in a
backward-compatibility-breaking manner. Arch.t is als unable to
represent the whole variety of computing devices, which is especially
relevant to micro-controllers (AVR, PIC) and IoT devices on which we
are currently focusing. Finally, Arch.t is not precise enough to
capture information that is necessary for code generation, the new
venue that we are currently exploring.

As the first attempt that didn't really work we introduced arch, sub,
and other properties to the `core-theory:unit` class in #1119. The problem
with that approach was the stringly typed interface as `arch` was
represented as a simple string. In addition, the proposed properties
werent' able to describe uncommon architectures. Finally, it was very
awkward to use, all fields were optional with no good
defaults.

This is the second attempt and it will be split into several pull
requests. The first PR, this one, introduce the Theory.Target.t but
still keeps Arch.t alive, i.e., it is used by all internal and
external components of BAP. This is to ensure that switching to
Target.t doesn't break any existing code. The consequent pull requests
will gradually deprecated functions that use Arch.t and switch
Target.t everywhere. The most important switch will affect the
disassembler/decoder framework, which is currently still stuck on
Arch.t. Just to be clear, after this work is finished and until BAP
3.0 and maybe even thereafter Arch.t will still work as it used to
work and no code will break or require updates. However, newly added
architectures, such as AVR or PIC, i.e., those that could not be
represented with Arch.t will not be available for the code that still
relies on it.

In addition to Theory.Target.t we add a few more abstractions and
convenience functions, e.g., `Project.empty` and a completely new
interface for Project.Input.t generation, which makes it easier to
create projects from strings or other custom data, e.g.,
`Project.Input.from_string` .

We also add Source, Language, and Compiler abstractions to the
knowledge base Core Theory. These abstractions, together with Target,
describe the full cycle of the program transformation using the
compiler from source code in the given language to the program for the
specified target (and the other way around). The Target abstraction
itself comes with a few more data types that describe various aspects
of the target system, including file formats, ABI, floating-point
ABI (FABI), endianness, which is no longer limited to the binary
choice of little and big endianness, and an extensible data type for
storing target-specific options.

Finally, all targets are formed into hierarchies and families, which
helps in controlling the vast zoo of computer architectures and
devices.

The Target.t is an abstract data type and is self-describing and
includes enough information that describes all the details of the
architecture. We also provide four library modules, for arm, mips,
powerpc, and x86 that exposes the currenlty declared targets.

Our LLVM backend is not yet precise enough to recongize many of the
supported targets and we don't have analyses right now that will infer
the target from the binary, but we will add the `--target` option in
the next PRs (when we will switch to Target.t) everywhere.

As usual, comments, questions, reviews are very welcome.
---
 lib/arm/arm_target.ml                         | 336 ++++++++++++
 lib/arm/arm_target.mli                        | 106 ++++
 lib/bap/bap.mli                               | 185 ++++++-
 lib/bap/bap_project.ml                        | 233 ++++----
 lib/bap/bap_project.mli                       |  19 +
 lib/bap_core_theory/bap_core_theory.ml        |   4 +-
 lib/bap_core_theory/bap_core_theory.mli       | 500 ++++++++++++++++--
 .../bap_core_theory_program.ml                | 151 ++++--
 .../bap_core_theory_program.mli               |  63 ++-
 lib/bap_core_theory/bap_core_theory_target.ml | 260 +++++++++
 .../bap_core_theory_target.mli                | 115 ++++
 lib/bap_disasm/bap_disasm_rec.ml              |  10 +-
 lib/bap_disasm/bap_disasm_symtab.ml           |   5 +-
 lib/bap_mips/bap_mips_target.ml               | 117 ++++
 lib/bap_mips/bap_mips_target.mli              |  34 ++
 lib/bap_powerpc/bap_powerpc_target.ml         | 112 ++++
 lib/bap_powerpc/bap_powerpc_target.mli        |  34 ++
 lib/bap_powerpc/bap_powerpc_targets.ml        | 120 +++++
 lib/bap_types/bap_arch.ml                     |  28 +-
 lib/bap_types/bap_arch.mli                    |   2 +
 lib/bap_types/bap_bitvector.ml                |   7 +
 lib/bap_types/bap_bitvector.mli               |   6 +
 lib/x86_cpu/x86_target.ml                     | 231 ++++++++
 lib/x86_cpu/x86_target.mli                    |  28 +
 oasis/arm                                     |   5 +-
 oasis/core-theory                             |   1 +
 oasis/mips                                    |  11 +-
 oasis/powerpc                                 |  11 +-
 oasis/x86                                     |   6 +-
 opam/opam                                     |   2 +-
 plugins/analyze/analyze_core_commands.ml      |  24 +-
 plugins/arm/.merlin                           |   5 +
 plugins/arm/arm_main.ml                       |   1 +
 plugins/mips/mips_main.ml                     |   1 +
 plugins/objdump/objdump_main.ml               |   5 +-
 plugins/powerpc/powerpc_main.ml               |   1 +
 plugins/radare2/.merlin                       |   2 +-
 plugins/radare2/radare2_main.ml               |   3 +-
 plugins/relocatable/rel_symbolizer.ml         |   6 +-
 plugins/stub_resolver/.merlin                 |   8 +-
 plugins/stub_resolver/stub_resolver_main.ml   |  96 +---
 plugins/x86/.merlin                           |   5 +
 plugins/x86/x86_main.ml                       |   3 +-
 plugins/x86/{x86_target.ml => x86_targets.ml} |   4 +-
 .../x86/{x86_target.mli => x86_targets.mli}   |   0
 45 files changed, 2528 insertions(+), 378 deletions(-)
 create mode 100644 lib/arm/arm_target.ml
 create mode 100644 lib/arm/arm_target.mli
 create mode 100644 lib/bap_core_theory/bap_core_theory_target.ml
 create mode 100644 lib/bap_core_theory/bap_core_theory_target.mli
 create mode 100644 lib/bap_mips/bap_mips_target.ml
 create mode 100644 lib/bap_mips/bap_mips_target.mli
 create mode 100644 lib/bap_powerpc/bap_powerpc_target.ml
 create mode 100644 lib/bap_powerpc/bap_powerpc_target.mli
 create mode 100644 lib/bap_powerpc/bap_powerpc_targets.ml
 create mode 100644 lib/x86_cpu/x86_target.ml
 create mode 100644 lib/x86_cpu/x86_target.mli
 rename plugins/x86/{x86_target.ml => x86_targets.ml} (92%)
 rename plugins/x86/{x86_target.mli => x86_targets.mli} (100%)

diff --git a/lib/arm/arm_target.ml b/lib/arm/arm_target.ml
new file mode 100644
index 0000000000..a066c35da0
--- /dev/null
+++ b/lib/arm/arm_target.ml
@@ -0,0 +1,336 @@
+open Core_kernel
+open Bap_core_theory
+open Bap.Std
+
+let package = "bap"
+
+type r128 and r80 and r64 and r32 and r16 and r8
+
+type 'a bitv = 'a Theory.Bitv.t Theory.Value.sort
+
+let r128 : r128 bitv = Theory.Bitv.define 128
+let r80 : r80 bitv = Theory.Bitv.define 80
+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 untyped = List.map ~f:Theory.Var.forget
+let (@<) xs ys = untyped xs @ untyped ys
+
+let array ?(index=string_of_int) t pref size =
+  List.init size ~f:(fun i -> reg t (pref ^ index i))
+
+let mems = Theory.Mem.define r32 r8
+let data = Theory.Var.define mems (Var.name Arm_env.mem)
+
+let of_bil v =
+  Theory.Var.define (Var.sort v) (Var.name v)
+
+let vars32 = List.map ~f:of_bil Arm_env.[
+    r0; r1; r2; r3; r4; r5; r6; r7; r8; r9;
+    r10; r11; r12; sp; lr; mem;
+    nf; zf; cf; vf; qf;
+  ]
+
+let vars32_fp = vars32 @ untyped @@ array r64 "D" 16
+
+
+let gp64 = array r64 "X" 30
+let fp64 = array r128 "Q" 32
+let sp64 = [reg r64 "SP"]
+let lr64 = [reg r64 "LR"]
+let mems64 = Theory.Mem.define r64 r8
+let data64 = Theory.Var.define mems64 "mem"
+let flags64 = [
+  reg bool "NF";
+  reg bool "ZF";
+  reg bool "CF";
+  reg bool "VF";
+]
+
+let vars64 = gp64 @< fp64 @< sp64 @< lr64 @< flags64 @< [data64]
+
+let parent = Theory.Target.declare "arm"
+
+module type v4 = sig
+end
+
+
+module type ARM = sig
+  val endianness : Theory.Target.endianness
+  val parent : Theory.Target.t
+  val v4 : Theory.Target.t
+  val v4t : Theory.Target.t
+  val v5 : Theory.Target.t
+  val v5t : Theory.Target.t
+  val v5te : Theory.Target.t
+  val v5tej : Theory.Target.t
+  val v6 : Theory.Target.t
+  val v6t2 : Theory.Target.t
+  val v6z : Theory.Target.t
+  val v6k : Theory.Target.t
+  val v6m : Theory.Target.t
+  val v7 : Theory.Target.t
+  val v7fp : Theory.Target.t
+  val v7a : Theory.Target.t
+  val v7afp : Theory.Target.t
+  val v8a : Theory.Target.t
+  val v81a : Theory.Target.t
+  val v82a : Theory.Target.t
+  val v83a : Theory.Target.t
+  val v84a : Theory.Target.t
+  val v85a : Theory.Target.t
+  val v86a : Theory.Target.t
+end
+
+module type Endianness =  sig val endianness : Theory.Target.endianness end
+module Family (Order : Endianness) = struct
+  include Order
+
+  let ordered name =
+    let order = Theory.Target.Endianness.name endianness in
+    name ^ "+" ^ KB.Name.unqualified order
+
+  let (<:) parent name =
+    if Theory.Target.is_unknown parent
+    then Theory.Target.unknown
+    else Theory.Target.declare ~package (ordered name) ~parent
+        ~nicknames:[name]
+
+  let is_bi_endian = Theory.Target.Endianness.(equal bi) endianness
+
+  let v4 =
+    if is_bi_endian
+    then Theory.Target.unknown
+    else Theory.Target.declare ~package (ordered "armv4")
+        ~parent
+        ~nicknames:["armv4"]
+        ~bits:32
+        ~byte:8
+        ~endianness
+        ~code:data
+        ~data:data
+        ~vars:vars32
+
+  let v4t   = v4 <: "armv4t"
+  let v5    = v4 <: "armv5"
+  let v5t   = v5 <: "armv5t"
+  let v5te  = v5t <: "armv5te"
+  let v5tej = v5te <: "armv5tej"
+  let v6    = v5tej <: "armv6"
+  let v6t2  = v6 <: "armv6t2"
+  let v6z   = v6 <: "armv6z"
+  let v6k   = v6z <: "armv6k"
+  let v6m   = v6 <: "armv6-m"
+
+  let v7    = if not is_bi_endian then v6t2 <: "armv7"
+    else Theory.Target.declare ~package (ordered "armv4")
+        ~parent
+        ~nicknames:["armv4"]
+        ~bits:32
+        ~byte:8
+        ~endianness
+        ~code:data
+        ~data:data
+        ~vars:vars32
+
+  let v7fp  = Theory.Target.declare ~package (ordered "armv7+fp") ~parent:v7
+      ~nicknames:["armv7+fp"]
+      ~vars:vars32_fp
+
+  let v7a    = v7 <: "armv7-a"
+  let v7afp  = Theory.Target.declare ~package (ordered "armv7-a+fp")
+      ~nicknames:["armv7-a+fp"]
+      ~parent:v7a
+      ~vars:vars32_fp
+
+  let v8a =
+    Theory.Target.declare ~package (ordered "armv8-a") ~parent:v7
+      ~nicknames:["armv8-a"]
+      ~bits:64
+      ~code:data64
+      ~data:data64
+      ~vars:vars64
+
+  let v81a = v8a  <: "armv8.1-a"
+  let v82a = v81a <: "armv8.2-a"
+  let v83a = v82a <: "armv8.3-a"
+  let v84a = v83a <: "armv8.4-a"
+  let v85a = v84a <: "armv8.5-a"
+  let v86a = v85a <: "armv8.6-a"
+
+  let parent = if is_bi_endian then v7 else v4
+end
+
+module LE = Family(struct
+    let endianness = Theory.Target.Endianness.le
+  end)
+
+
+module Bi = Family(struct
+    let endianness = Theory.Target.Endianness.bi
+  end)
+
+
+module EB = Family(struct
+    let endianness = Theory.Target.Endianness.eb
+  end)
+
+let family_of_endian is_little : (module ARM) = match is_little with
+  | None -> (module Bi)
+  | Some true -> (module LE)
+  | Some false -> (module EB)
+
+
+let prefixes = ["arm"; "thumb"; "aarch64";]
+let suffixes = ["eb"; "_be"]
+
+let in_family = function
+  | None -> false
+  | Some x -> List.exists prefixes ~f:(fun prefix ->
+      String.is_prefix ~prefix x)
+
+let drop_end s =
+  Option.value ~default:s @@
+  List.find_map suffixes ~f:(fun suffix ->
+      String.chop_suffix ~suffix s)
+
+let split s = List.find_map_exn prefixes ~f:(fun prefix ->
+    match String.chop_prefix ~prefix s with
+    | None -> None
+    | Some r -> Some (prefix,drop_end r))
+
+let normalize arch sub =
+  match arch,sub with
+  | None,_ -> assert false
+  | Some arch,None -> split arch
+  | Some arch, Some sub -> arch,sub
+
+let enable_loader () =
+  let open Bap.Std in
+  KB.Rule.(declare ~package "arm-target" |>
+           require Project.specification_slot |>
+           provide Theory.Unit.target |>
+           comment "computes target from the OGRE specification");
+  let open KB.Syntax in
+  let request_info doc =
+    let open Ogre.Syntax in
+    let request =
+      Ogre.request Image.Scheme.arch >>= fun arch ->
+      Ogre.request Image.Scheme.subarch >>= fun sub ->
+      Ogre.request Image.Scheme.is_little_endian >>= fun little ->
+      Ogre.return (arch,sub, little) in
+    match Ogre.eval request doc with
+    | Error _ -> None,None,None
+    | Ok info -> info in
+  KB.promise Theory.Unit.target @@ fun unit ->
+  KB.collect Project.specification_slot unit >>|
+  request_info >>| fun (arch,sub,is_little) ->
+  if not (in_family arch) then Theory.Target.unknown
+  else
+    let module Family = (val family_of_endian is_little) in
+    match normalize arch sub with
+    | "arm","v4"  -> Family.v4
+    | "arm","v4t" -> Family.v4t
+    | "arm","v5" -> Family.v5
+    | "arm","v5t" -> Family.v5t
+    | "arm","v5te" -> Family.v5te
+    | "arm","v5tej" -> Family.v5tej
+    | "arm","v6" -> Family.v6
+    | "arm","v6z" -> Family.v6z
+    | "arm","v6k" -> Family.v6k
+    | "arm","v6m" -> Family.v6m
+    | "arm","v6t2" -> Family.v6t2
+    | "arm","v7" -> Family.v7
+    | "arm","v7fp" -> Family.v7
+    | "arm","v7a" -> Family.v7a
+    | "arm","v7afp" -> Family.v7afp
+    | "arm","v8" -> Family.v8a
+    | "arm","v8a" -> Family.v8a
+    | "arm","v81a" -> Family.v81a
+    | "arm","v82a" -> Family.v82a
+    | "arm","v83a" -> Family.v83a
+    | "arm","v84a" -> Family.v84a
+    | "arm","v85a" -> Family.v85a
+    | "arm","v86a" -> Family.v86a
+    | "thumb", "v4" -> Family.v4t
+    | "thumb", "v5" -> Family.v5t
+    | "aarch64",_   -> Family.v86a
+    | _ -> Family.v7
+
+
+type arms = [
+  | Arch.arm
+  | Arch.armeb
+  | Arch.thumb
+  | Arch.thumbeb
+  | Arch.aarch64
+]
+
+let arms : arms Map.M(Theory.Target).t =
+  Map.of_alist_exn (module Theory.Target) [
+    LE.v4, `armv4;
+    LE.v4t, `thumbv4;
+    LE.v5, `armv5;
+    LE.v5t, `thumbv5;
+    LE.v5te, `thumbv5;
+    LE.v5tej, `thumbv5;
+    LE.v6, `armv6;
+    LE.v6z, `armv6;
+    LE.v6k, `armv6;
+    LE.v6m, `armv6;
+    LE.v6t2, `armv6;
+    LE.v7, `armv7;
+    LE.v7a, `armv7;
+    LE.v7afp, `armv7;
+    LE.v8a, `aarch64;
+    LE.v81a, `aarch64;
+    LE.v82a, `aarch64;
+    LE.v83a, `aarch64;
+    LE.v84a, `aarch64;
+    LE.v85a, `aarch64;
+    LE.v86a, `aarch64;
+    EB.v4, `armv4eb;
+    EB.v4t, `thumbv4eb;
+    EB.v5, `armv5eb;
+    EB.v5t, `thumbv5eb;
+    EB.v5te, `thumbv5eb;
+    EB.v5tej, `thumbv5eb;
+    EB.v6,  `armv6eb;
+    EB.v6z, `armv6eb;
+    EB.v6k, `armv6eb;
+    EB.v6m, `armv6eb;
+    EB.v6t2,`armv6eb;
+    EB.v7, `armv7eb;
+    EB.v7a, `armv7eb;
+    EB.v7afp, `armv7eb;
+    EB.v8a,  `aarch64_be;
+    EB.v81a, `aarch64_be;
+    EB.v82a, `aarch64_be;
+    EB.v83a, `aarch64_be;
+    EB.v84a, `aarch64_be;
+    EB.v85a, `aarch64_be;
+    EB.v86a, `aarch64_be;
+  ]
+
+
+let enable_arch () =
+  let open KB.Syntax in
+  KB.Rule.(declare ~package "arm-arch" |>
+           require Theory.Unit.target |>
+           provide Arch.unit_slot |>
+           comment "computes Arch.t from the unit's target");
+  KB.promise Arch.unit_slot @@ fun unit ->
+  KB.collect Theory.Unit.target unit >>| fun t ->
+  match Map.find arms t with
+  | Some arch -> (arch :> Arch.t)
+  | None -> `unknown
+
+
+let load () =
+  enable_loader ();
+  enable_arch ()
diff --git a/lib/arm/arm_target.mli b/lib/arm/arm_target.mli
new file mode 100644
index 0000000000..060d5a0063
--- /dev/null
+++ b/lib/arm/arm_target.mli
@@ -0,0 +1,106 @@
+(** Declarations of various ARM targets.*)
+
+open Bap_core_theory
+
+
+(** The parent of all ARM targets.
+
+    When a new target is declared it is advised to use this target as
+    parent so that the newly declared target will be included into the
+    ARM Targets family.
+    The [parent] target is pure abstract and doesn't have any
+    propreties set.
+*)
+val parent : Theory.Target.t
+
+
+(** The family of little endian targets.
+
+    Each version is the parent to the following version, with [parent]
+    being the the earliest version.*)
+module LE : sig
+  val parent : Theory.Target.t (** currently the same as [v4]  *)
+  val v4 : Theory.Target.t
+  val v4t : Theory.Target.t
+  val v5 : Theory.Target.t
+  val v5t : Theory.Target.t
+  val v5te : Theory.Target.t
+  val v5tej : Theory.Target.t
+  val v6 : Theory.Target.t
+  val v6t2 : Theory.Target.t
+  val v6z : Theory.Target.t
+  val v6k : Theory.Target.t
+  val v6m : Theory.Target.t
+  val v7 : Theory.Target.t
+  val v7fp : Theory.Target.t
+  val v7a : Theory.Target.t
+  val v7afp : Theory.Target.t
+  val v8a : Theory.Target.t
+  val v81a : Theory.Target.t
+  val v82a : Theory.Target.t
+  val v83a : Theory.Target.t
+  val v84a : Theory.Target.t
+  val v85a : Theory.Target.t
+  val v86a : Theory.Target.t
+end
+
+
+(** The family of big endian targets.
+
+    Each version is the parent to the following version, with [parent]
+    being the the earliest version.*)
+module EB : sig
+  val parent : Theory.Target.t (** currently the same as [v4]  *)
+  val v4 : Theory.Target.t
+  val v4t : Theory.Target.t
+  val v5 : Theory.Target.t
+  val v5t : Theory.Target.t
+  val v5te : Theory.Target.t
+  val v5tej : Theory.Target.t
+  val v6 : Theory.Target.t
+  val v6t2 : Theory.Target.t
+  val v6z : Theory.Target.t
+  val v6k : Theory.Target.t
+  val v6m : Theory.Target.t
+  val v7 : Theory.Target.t
+  val v7fp : Theory.Target.t
+  val v7a : Theory.Target.t
+  val v7afp : Theory.Target.t
+  val v8a : Theory.Target.t
+  val v81a : Theory.Target.t
+  val v82a : Theory.Target.t
+  val v83a : Theory.Target.t
+  val v84a : Theory.Target.t
+  val v85a : Theory.Target.t
+  val v86a : Theory.Target.t
+end
+
+
+(** The family of targets with switchable endiannes.
+
+    The switchable (context-dependent) endianness was introduced
+    in [v7] therefore there are no targets of earlier version.
+*)
+module Bi : sig
+  val parent : Theory.Target.t (** the same as [v7]  *)
+  val v7 : Theory.Target.t
+  val v7fp : Theory.Target.t
+  val v7a : Theory.Target.t
+  val v7afp : Theory.Target.t
+  val v8a : Theory.Target.t
+  val v81a : Theory.Target.t
+  val v82a : Theory.Target.t
+  val v83a : Theory.Target.t
+  val v84a : Theory.Target.t
+  val v85a : Theory.Target.t
+  val v86a : Theory.Target.t
+end
+
+
+
+(** [load ()] loads the knowledge base rules for the ARM targets.
+
+    This includes parsing the loader output and enabling backward
+    compatibility with the old [Arch.t] representation.
+*)
+val load : unit -> unit
diff --git a/lib/bap/bap.mli b/lib/bap/bap.mli
index c2a24fd66b..1206b75e62 100644
--- a/lib/bap/bap.mli
+++ b/lib/bap/bap.mli
@@ -1250,6 +1250,33 @@ module Std : sig
     (** [create v w] creates a word from bitvector [v] of width [w].*)
     val create : Bitvec.t -> int -> t
 
+
+    (** [code_addr t x] uses target's address size to create a word.
+
+        Same as [create x (Theory.Target.code_addr_size t)].
+
+        @since 2.2.0
+    *)
+    val code_addr : Theory.Target.t -> Bitvec.t -> t
+
+
+    (** [data_addr t x] uses target's code address size to create a word.
+
+        Same as [create x (Theory.Target.data_addr_size t)].
+
+        @since 2.2.0
+    *)
+    val data_addr : Theory.Target.t -> Bitvec.t -> t
+
+    (** [data_word t x] uses target's word size to create a word.
+
+        Same as [create x (Theory.Target.bits t)].
+
+        @since 2.2.0
+    *)
+    val data_word : Theory.Target.t -> Bitvec.t -> t
+
+
     (** [of_string s] parses a bitvector from a string representation
         defined in section {!bv_string}.    *)
     val of_string : string -> t
@@ -4013,6 +4040,24 @@ module Std : sig
     (** the architecture (ISA) of a program.  *)
     val slot : (Theory.program, t) Knowledge.slot
 
+    (** [unit_slot] the arch property of the unit.
+
+        Use this slot to enable backward compatibility of the [Arch.t]
+        type with the [Theory.Target.t] by registering a promise that
+        translates [Theory.Target.t] to [Arch.t].
+
+        Example,
+
+        {[
+          let target = Theory.Target.declare ~package:"foo" "r600"
+          let () = KB.promise Arch.unit_slot @@ fun unit ->
+            KB.collect Theory.Unit.target >>| fun t ->
+            if Theory.Target.equal t target then `r600
+            else `unknown
+        ]}
+    *)
+    val unit_slot : (Theory.Unit.cls, t) Knowledge.slot
+
     (** [arch] type implements [Regular]  interface  *)
     include Regular.S with type t := t
   end
@@ -9367,15 +9412,32 @@ module Std : sig
       ?reconstructor:reconstructor source ->
       input -> t Or_error.t
 
-    (** [arch project] reveals the architecture of a loaded file  *)
+
+    (** [empty target] creates a for the given [target]. *)
+    val empty : Theory.Target.t -> t
+
+    (** [arch project] reveals the architecture of a loaded file
+
+        @deprecated use [target project] instead.
+    *)
     val arch : t -> arch
 
 
+    (** [target project] returns the target system of the project.
+
+        @since 2.2.0
+    *)
+    val target : t -> Theory.Target.t
+
+
     (** [specification p] returns the specification of the binary.
 
-        @since 2.2.0*)
+        @since 2.2.0 *)
     val specification : t -> Ogre.doc
 
+    (** the slot to access the specification of a unit.
+        @since 2.2.0 *)
+    val specification_slot : (Theory.Unit.cls, Ogre.Doc.t) KB.slot
 
     (** [state project] returns the core state of the [project].
 
@@ -9547,22 +9609,113 @@ module Std : sig
 
     (** Input information.
 
-        This module abstracts input type.
-    *)
+        This module abstracts the input data necessary to create a
+        project. *)
     module Input : sig
       type t = input
 
-      (** [file ?loader ~filename] input data from a file, using the
+
+      (** [load filename] loads the file from the specified path.
+          The file must be regular (i.e., not a pipe) and is expected
+          to have the necessary meta information, i.e., not the raw
+          code (use [raw_file] to load files that are raw code).
+
+          If [loader] is not specified then all image loaders are used
+          and the information from the is merged, otherwise only the
+          selected loaded is used. See {!Image.available_backend}.
+
+          The [target] could be used to specialize the target
+          information retrieved from the file. If it is less specific,
+          then it will be ignored, if it contradicts the information
+          in the file then the project creation will fail.
+
+          @since 2.2.0 *)
+      val load : ?target:Theory.Target.t -> ?loader:string -> string -> t
+
+      (** [raw_file ?base target ~filename] creates an input from a binary
+          file that is raw code for the given [target], i.e.,
+          without any headers or meta information.
+
+          @param base is an virtual address of the first byte
+          (defaults to 0).
+
+          @since 2.2.0 *)
+      val raw_file : ?base:addr -> Theory.Target.t -> string -> t
+
+
+      (** [create ?base target code] creates input from the binary
+          [code] for the given [target].
+
+          @since 2.2.0 *)
+      val from_string : ?base:addr -> Theory.Target.t -> string -> t
+
+      (** [create ?base target code] creates input from the binary
+          [code] for the given [target].
+
+          @since 2.2.0 *)
+      val from_bigstring : ?base:addr -> Theory.Target.t -> Bigstring.t -> t
+
+
+      (** [custom target] creates a custom input.
+
+          The [target] parameter denotes the target system of the
+          input program. The [code] and [data] parameters are stored
+          in the [Project.memory] and [code] is disassembled and
+          lifted if the specified [target] has a disassembler and lifter.
+
+          The [filename] is used to communicate with external tools
+          and will be broadcasted via [Info.file] stream and stored in
+          the filename property of the project, otherwise it is not
+          used when the project is created.
+
+          The [finish project] is the post-constructor that takes the
+          nearly finished project (with code and data and potentially
+          disassembled and lifted code) and constructs the final
+          project.
+      *)
+      val custom :
+        ?finish:(project -> project) ->
+        ?filename:string ->
+        ?code:value memmap ->
+        ?data:value memmap ->
+        Theory.Target.t -> t
+
+
+      (** [register_loader name load] register a loader under provided
+          [name]. The [load] function will be called the filename, and it
+          must return the [input] value. *)
+      val register_loader : string -> (string -> t) -> unit
+
+      (** [available_loaders ()] returns a list of names of currently known loaders.  *)
+      val available_loaders : unit -> string list
+
+      (** {3 Deprecated Interface}
+
+          The following functions are deprecated and better
+          alternatives are provided.
+          They might be removed in BAP 3.0.*)
+
+      (** [binary ?base arch ~filename] create an input from a binary
+          file that is a pure code without any headers or meta
+          information.
+
+          @param base is an virtual address of the first byte
+          (defaults to 0).
+
+          @deprecated use [Input.raw_file] instead.
+      *)
+      val binary : ?base:addr -> arch -> filename:string -> t
+
+      (** [file ?target ?loader ~filename] input data from a file, using the
           specified loader. If [loader] is not specified, then some existing
           loader will be used. If it is specified, then it is first looked
           up in the [available_loaders] and if it is not found, then it will
-          be looked up in the {!Image.available_backends}.  *)
-      val file : ?loader:string -> filename:string -> t
+          be looked up in the {!Image.available_backends}.
 
-      (** [binary ?base arch ~filename] create an input from a binary
-          file, that is a pure code.
-          @param base is an virtual address of the first byte (defaults to 0).*)
-      val binary : ?base:addr -> arch -> filename:string -> t
+          @deprecated use [Input.load filename]
+
+      *)
+      val file : ?loader:string -> filename:string -> t
 
       (** [create arch filename ~code ~data] creates an input from a
           file, using two memory maps. The [code] memmap spans the code in
@@ -9570,18 +9723,12 @@ module Std : sig
           function can be used to propagate to the project any
           additional information that is available to the loader. It
           defaults to [ident].
+          @deprecated use either [Input.custom] or [Input.from_string]
+          and [Input.from_bigstring].
       *)
       val create :
         ?finish:(project -> project) ->
         arch -> string -> code:value memmap -> data: value memmap -> t
-
-      (** [register_loader name load] register a loader under provided
-          [name]. The [load] function will be called the filename, and it
-          must return the [input] value. *)
-      val register_loader : string -> (string -> t) -> unit
-
-      (** [available_loaders ()] returns a list of names of currently known loaders.  *)
-      val available_loaders : unit -> string list
     end
 
     (** {3 Registering passes}
diff --git a/lib/bap/bap_project.ml b/lib/bap/bap_project.ml
index bd34b2267d..e282440f79 100644
--- a/lib/bap/bap_project.ml
+++ b/lib/bap/bap_project.ml
@@ -24,53 +24,40 @@ let query doc attr =
       (Error.to_string_hum err) ()
   | Ok bias -> bias
 
+let rec guess_arch t =
+  if Theory.Target.is_unknown t then `unknown
+  else
+    Theory.Target.name t |>
+    KB.Name.unqualified  |>
+    Arch.of_string |> function
+    | Some arch -> arch
+    | None -> guess_arch (Theory.Target.parent t)
+
 module Spec = struct
   module Fact = Ogre.Make(KB)
   open Fact.Syntax
 
-  let provide slot obj value =
-    Fact.lift @@ KB.provide slot obj value
-
-  let str field slot unit =
-    Fact.request field >>= function
-    | None | Some "" | Some "unknown" ->
-      Fact.return ()
-    | value -> provide slot unit value
-
-  let bool field slot unit =
-    Fact.request field >>= provide slot unit
-
-  let int field slot unit =
-    Fact.request field >>= function
-    | Some x ->
-      provide slot unit (Some (Int64.to_int_exn x))
-    | None -> Fact.return ()
-
-  let facts fields unit =
-    Fact.List.iter fields ~f:(fun provide -> provide unit)
-
-  let init_unit =
-    let open Theory.Unit in
-    let open Image.Scheme in
-    facts [
-      str arch Target.arch;
-      str subarch Target.subarch;
-      str vendor Target.vendor;
-      str system Target.system;
-      str abi Target.abi;
-      int bits Target.bits;
-      bool is_little_endian Target.is_little_endian;
-    ]
-
-  let provide spec unit =
-    let open KB.Syntax in
-    Fact.exec (init_unit unit) spec >>= function
-    | Error err ->
-      invalid_argf "Failed to provide the image specification \
-                    to the knowledge base: %s"
-        (Error.to_string_hum err) ()
-    | Ok _doc -> KB.return ()
-
+  type KB.Conflict.t += Spec_inconsistency of Error.t
+
+  let domain = KB.Domain.flat "spec"
+      ~empty:Ogre.Doc.empty
+      ~inspect:Ogre.Doc.sexp_of_t
+      ~join:(fun d1 d2 -> match Ogre.Doc.merge d1 d2 with
+          | Ok d -> Ok d
+          | Error err ->
+            Error (Spec_inconsistency err))
+      ~equal:(fun d1 d2 -> Ogre.Doc.compare d1 d2 = 0)
+
+  let slot = KB.Class.property Theory.Unit.cls "unit-spec" domain
+      ~package
+      ~persistent:(KB.Persistent.of_binable (module struct
+                     type t = Ogre.Doc.t [@@deriving bin_io]
+                   end))
+
+  let () = KB.Conflict.register_printer @@ function
+    | Spec_inconsistency err ->
+      Some (Error.to_string_hum err)
+    | _ -> None
 
   let init arch =
     let module Field = Image.Scheme in
@@ -92,31 +79,27 @@ module Spec = struct
     | Ok doc -> doc
 end
 
-let with_arch arch mems =
+let target_of_spec spec =
   let open KB.Syntax in
-  let width = Size.in_bits (Arch.addr_size arch) in
-  KB.promising Arch.slot ~promise:(fun label ->
-      KB.collect Theory.Label.addr label >>| function
-      | None -> `unknown
-      | Some p ->
-        let p = Word.create p width in
-        if Memmap.contains mems p
-        then arch
-        else `unknown)
-
-let with_filename spec arch data code path =
+  KB.Object.scoped Theory.Unit.cls @@ fun unit ->
+  KB.provide Spec.slot unit spec >>= fun () ->
+  KB.collect Theory.Unit.target unit
+
+let with_filename spec target data code path =
   let open KB.Syntax in
-  let width = Size.in_bits (Arch.addr_size arch) in
-  let bias = Option.map (query spec Image.Scheme.bias)
-      ~f:(fun x -> Bitvec.(int64 x mod modulus width)) in
+  let width = Theory.Target.code_addr_size target in
+  let bias = query spec Image.Scheme.bias |> Option.map
+               ~f:(fun x -> Bitvec.(int64 x mod modulus width)) in
   KB.promising Theory.Label.unit ~promise:(fun label ->
       KB.collect Theory.Label.addr label >>=? fun addr ->
       let addr = Word.create addr width in
       if Memmap.contains data addr || Memmap.contains code addr
       then
         Theory.Unit.for_file path >>= fun unit ->
-        Spec.provide spec unit >>= fun () ->
+        KB.provide Spec.slot unit spec >>= fun () ->
         KB.provide Theory.Unit.bias unit bias >>= fun () ->
+        KB.provide Theory.Unit.target unit target >>= fun () ->
+        KB.provide Spec.slot unit spec >>= fun () ->
         KB.provide Theory.Unit.path unit (Some path) >>| fun () ->
         Some unit
       else KB.return None)
@@ -182,11 +165,14 @@ module State = struct
     KB.Domain.flat ~empty ~equal "disassembly" ~inspect
 
   module Toplevel = struct
-    let run spec arch ~code ~data file k =
+    let run spec target ~code ~data file k =
       let result = Toplevel.var "disassembly-result" in
+      let compute_target = if Theory.Target.is_unknown target
+        then target_of_spec spec
+        else KB.return target in
       Toplevel.put result begin
-        with_arch arch code @@ fun () ->
-        with_filename spec arch code data file @@ fun () ->
+        compute_target >>= fun target ->
+        with_filename spec target code data file @@ fun () ->
         k
       end;
       Toplevel.get result
@@ -197,6 +183,7 @@ type state = State.t [@@deriving bin_io]
 
 type t = {
   arch    : arch;
+  target  : Theory.Target.t;
   spec    : Ogre.doc;
   state   : State.t;
   disasm  : disasm Lazy.t;
@@ -207,6 +194,7 @@ type t = {
   passes  : string list;
 } [@@deriving fields]
 
+
 module Info = struct
   let file,got_file = Stream.create ()
   let arch,got_arch = Stream.create ()
@@ -227,12 +215,29 @@ module Input = struct
     spec : Ogre.doc;
     file : string;
     finish : t -> t;
+    target : Theory.Target.t;
   }
 
   type t = unit -> result
 
-  let create ?(finish=ident) arch file ~code ~data () = {
-    arch; file; code; data; finish; spec=Spec.init arch;
+
+  let custom
+      ?(finish=ident)
+      ?(filename="")
+      ?(code=Memmap.empty)
+      ?(data=Memmap.empty) target () = {
+    arch=guess_arch target; file=filename; code; data; finish;
+    target;
+    spec = Ogre.Doc.empty
+  }
+
+  let create
+      ?(finish=ident) arch file ~code ~data () = {
+    arch; file; code; data; finish;
+    target = Theory.Target.unknown;
+    spec = match arch with
+      | #Arch.unknown -> Ogre.Doc.empty
+      | arch -> Spec.init arch;
   }
 
   let loaders = String.Table.create ()
@@ -244,13 +249,14 @@ module Input = struct
 
   let is_data v = not (is_code v)
 
-  let of_image finish file img = {
+  let result_of_image ?(target=Theory.Target.unknown) finish file img = {
     arch = Image.arch img;
     data = Memmap.filter ~f:is_data (Image.memory img);
     code = Memmap.filter ~f:is_code (Image.memory img);
     spec = Image.spec img;
     file;
     finish;
+    target;
   }
 
   let symtab_agent =
@@ -268,7 +274,7 @@ module Input = struct
     Symbolizer.provide symtab_agent image_symbols;
     Rooter.provide image_roots
 
-  let of_image ?loader filename =
+  let of_image ?target ?loader filename =
     Image.create ?backend:loader filename >>| fun (img,warns) ->
     List.iter warns ~f:(fun e -> warning "%a" Error.pp e);
     let spec = Image.spec img in
@@ -285,30 +291,51 @@ module Input = struct
                   Term.set_attr sub Sub.entry_point ()
                 | _ -> sub))
     } in
-    of_image finish filename img
+    result_of_image ?target finish filename img
 
-  let from_image ?loader filename () =
-    of_image ?loader filename |> ok_exn
+  let from_image ?target ?loader filename () =
+    of_image ?target ?loader filename |> ok_exn
 
-  let file ?loader ~filename = match loader with
-    | None -> from_image filename
+  let load ?target ?loader filename = match loader with
+    | None -> from_image ?target filename
     | Some name -> match Hashtbl.find loaders name with
-      | None -> from_image ?loader filename
+      | None -> from_image ?target ?loader filename
       | Some load -> load filename
 
+  let file ?loader ~filename = load ?loader filename
+
   let null arch : addr =
     Addr.of_int 0 ~width:(Arch.addr_size arch |> Size.in_bits)
 
-  let binary ?base arch ~filename () =
-    let big = Bap_fileutils.readfile filename in
+  let raw ?(target=Theory.Target.unknown) ?(filename="") ?base arch big () =
     if Bigstring.length big = 0 then invalid_arg "file is empty";
-    let base = Option.value base ~default:(null arch) in
-    let mem = Memory.create (Arch.endian arch) base big |> ok_exn in
+    let addr_size = if Theory.Target.is_unknown target
+      then Arch.addr_size arch |> Size.in_bits
+      else Theory.Target.code_addr_size target in
+    let endian = if Theory.Target.is_unknown target
+      then Arch.endian arch else
+      if Theory.Target.endianness target =
+         Theory.Target.Endianness.le
+      then LittleEndian else BigEndian in
+    let base = Option.value base ~default:(Addr.zero addr_size) in
+    let mem = Memory.create endian base big |> ok_exn in
     let section = Value.create Image.section "bap.user" in
     let code = Memmap.add Memmap.empty mem section in
     let data = Memmap.empty  in
     let spec = Spec.init arch in
-    {arch; data; code; file = filename; finish = ident; spec}
+    {arch; data; code; file = filename; finish = ident; spec; target}
+
+  let binary ?base arch ~filename =
+    raw ?base arch (Bap_fileutils.readfile filename)
+
+  let raw_file ?base target filename =
+    raw ~target ?base `unknown (Bap_fileutils.readfile filename)
+
+  let from_bigstring ?base target data =
+    raw ~target ?base `unknown data
+
+  let from_string ?base target data =
+    from_bigstring ?base target (Bigstring.of_string data)
 
   let available_loaders () =
     Hashtbl.keys loaders @ Image.available_backends ()
@@ -365,6 +392,19 @@ let unused_options =
                please consult the documentation for the proper \
                alternative" name))
 
+let empty target = {
+  arch = guess_arch target;
+  target;
+  spec = Ogre.Doc.empty;
+  state = State.empty;
+  memory = Memmap.empty;
+  storage = Dict.empty;
+  program = lazy (Program.create ());
+  symbols = lazy Symtab.empty;
+  disasm = lazy (Disasm.create Graphs.Cfg.empty);
+  passes = []
+}
+
 let (=?) name = Option.map ~f:(fun _ -> name)
 
 let create
@@ -384,14 +424,14 @@ let create
       "rooter" =? p4;
       "rooter" =? p5;
     ];
-    let {Input.arch; data; code; file; spec; finish} = read () in
+    let {Input.arch; data; code; file; spec; finish; target} = read () in
     Signal.send Info.got_file file;
     Signal.send Info.got_arch arch;
     Signal.send Info.got_data data;
     Signal.send Info.got_code code;
     Signal.send Info.got_spec spec;
     let run k =
-      State.Toplevel.run spec arch ~code ~data file k in
+      State.Toplevel.run spec target ~code ~data file k in
     let state = match state with
       | Some state -> state
       | None ->
@@ -420,7 +460,8 @@ let create
       symbols;
       arch; memory=union_memory code data;
       storage = Dict.set Dict.empty filename file;
-      passes=[]
+      passes=[];
+      target;
     }
   with
   | Toplevel.Conflict err ->
@@ -432,6 +473,7 @@ let create
   | exn -> Or_error.of_exn ~backtrace:`Get exn
 
 let specification = spec
+let specification_slot = Spec.slot
 
 let symbols {symbols} = Lazy.force symbols
 let disasm {disasm} = Lazy.force disasm
@@ -940,21 +982,16 @@ let () =
   Data.set_module_name instance "Bap.Std.Project"
 
 let () =
-  KB.Rule.(declare ~package:"bap" "project-filename" |>
-           dynamic ["input"] |>
-           dynamic ["data"; "code"; "path"] |>
-           require Theory.Label.addr |>
-           provide Theory.Label.unit |>
-           comment {|
-On [Project.create input] provides [path] for the address [x]
-if [x] in [data] or [x] in [code].
-|});
-  KB.Rule.(declare ~package:"bap" "project-arch" |>
-           dynamic ["input"] |>
-           dynamic ["arch"; "code"] |>
-           require Theory.Label.addr |>
-           provide Arch.slot |>
-           comment {|
-On [Project.create input] provides [arch] for the address [x]
-if [x] in [code].
-|})
+  let open KB.Rule in
+  declare ~package:"bap" "project-filename" |>
+  dynamic ["input"] |>
+  dynamic ["data"; "code"; "path"] |>
+  dynamic ["loader"] |>
+  require Theory.Label.addr |>
+  provide Theory.Label.unit |>
+  comment {|
+  On [Project.create input] provides [unit] for the address [x]
+  if [x] in [data] or [x] in [code]. The [unit] is initialized
+  with the specification from the loader, filename, target name,
+  etc.
+|};
diff --git a/lib/bap/bap_project.mli b/lib/bap/bap_project.mli
index 1319351d8d..405e28e8ce 100644
--- a/lib/bap/bap_project.mli
+++ b/lib/bap/bap_project.mli
@@ -17,6 +17,8 @@ type second = float
 
 val state : t -> state
 
+val empty : Theory.Target.t -> t
+
 val create :
   ?package:string ->
   ?state:state ->
@@ -28,7 +30,10 @@ val create :
   input -> t Or_error.t
 
 val arch : t -> arch
+val target : t -> Theory.Target.t
 val specification : t -> Ogre.doc
+val specification_slot : (Theory.Unit.cls, Ogre.Doc.t) KB.slot
+
 val program : t -> program term
 val with_program : t -> program term -> t
 val symbols : t -> symtab
@@ -68,6 +73,19 @@ end
 
 module Input : sig
   type t = input
+
+  val load : ?target:Theory.Target.t -> ?loader:string -> string -> t
+  val custom :
+    ?finish:(project -> project) ->
+    ?filename:string ->
+    ?code:value memmap ->
+    ?data:value memmap ->
+    Theory.Target.t -> t
+
+  val raw_file : ?base:addr -> Theory.Target.t -> string -> t
+  val from_string : ?base:addr -> Theory.Target.t -> string -> t
+  val from_bigstring : ?base:addr -> Theory.Target.t -> Bigstring.t -> t
+
   val file : ?loader:string -> filename:string -> t
   val binary : ?base:addr -> arch -> filename:string -> t
 
@@ -77,6 +95,7 @@ module Input : sig
     string ->
     code:value memmap ->
     data:value memmap -> t
+
   val register_loader : string -> (string -> t) -> unit
   val available_loaders : unit -> string list
 end
diff --git a/lib/bap_core_theory/bap_core_theory.ml b/lib/bap_core_theory/bap_core_theory.ml
index 42f50ba0dd..8522f185d2 100644
--- a/lib/bap_core_theory/bap_core_theory.ml
+++ b/lib/bap_core_theory/bap_core_theory.ml
@@ -3,7 +3,7 @@ open Bap_knowledge
 module KB = Knowledge
 
 module Theory = struct
-  module Value   = Bap_core_theory_value
+  module Value = Bap_core_theory_value
   module Bool = Value.Bool
   module Bitv = Value.Bitv
   module Mem = Value.Mem
@@ -14,6 +14,8 @@ module Theory = struct
   module Program = Bap_core_theory_program
   module Label = Program.Label
   module Unit = Program.Unit
+  module Source = Program.Source
+  module Target = Bap_core_theory_target
   type program = Program.cls
 
 
diff --git a/lib/bap_core_theory/bap_core_theory.mli b/lib/bap_core_theory/bap_core_theory.mli
index 66c6023706..e2c59c48f1 100644
--- a/lib/bap_core_theory/bap_core_theory.mli
+++ b/lib/bap_core_theory/bap_core_theory.mli
@@ -646,7 +646,7 @@ module Theory : sig
       val pp : formatter -> 'a t -> unit
 
 
-      (** Sort without a type index.
+      (** Sorts with erased type indices.
 
           This module enables construction of complex data structures
           on sorts, like maps, sets, etc, e.g.,
@@ -1107,6 +1107,401 @@ module Theory : sig
   end
 
 
+  (** The source code artifact of a compilation unit.
+
+      Contains the information about the source code of a program
+      unit. Note, that it is not an attribute of a program that
+      denotes the semantics of that program, but an artifact
+      that is associated with the compile unit.
+
+      The information about the source code is represented as an
+      extesnsible {!KB.Value.t}. To add a new property of the Source
+      class use {!KB.Class.property},
+        to access existing properties use {!KB.Value.get}
+        and {!KB.Value.put}.
+
+
+      @since 2.2.0
+  *)
+  module Source : sig
+    type cls
+    include KB.Value.S with type t = (cls,unit) KB.cls KB.Value.t
+
+    (** the abstract name of a programming language  *)
+    type language
+
+
+    (** the class index for the core-theory:source class  *)
+    val cls : (cls,unit) KB.cls
+
+
+    (** the language of the source code  *)
+    val language : (cls,language) KB.slot
+
+    (** the source code text  *)
+    val code : (cls,string) KB.slot
+
+    (** the file name of the unit's source code  *)
+    val file : (cls,string option) KB.slot
+
+    (** The source code language. *)
+    module Language : sig
+      include Base.Comparable.S with type t = language
+      include Binable.S with type t := t
+      include Stringable.S with type t := t
+      include Pretty_printer.S with type t := t
+
+      (** [declare ?package name] declares a new source code language.  *)
+      val declare : ?package:string -> string -> language
+
+      (** the unique name of the language  *)
+      val name : language -> KB.Name.t
+    end
+  end
+
+
+  (** Description of the execution target.
+
+      An abstract description of the system on which a program is
+      intended to be run. The description precisely describes various
+      architectual and microarchitectual details of the target system,
+      and could be extended with further details either internally, by
+      adding more fields (and functions to this module) or storing
+      those options in [Options.t]; or externally, by maintaining
+      finite mappings from [Target.t] to corresponding properties.
+
+      The [Target.t] has a lightweight immediate representation, which
+      is portable across OCaml runtime and persistent across versions
+      of BAP and OCaml.
+
+      @since 2.2.0  *)
+  module Target : sig
+    (** the abstract type representing the target.
+
+        This type is a unique identifier of the target,
+        represented as [KB.Name.t] underneath the hood.
+    *)
+    type t
+    include Base.Comparable.S with type t := t
+    include Binable.S with type t := t
+    include Stringable.S with type t := t
+    include Pretty_printer.S with type t := t
+
+    (** The ordering of the bytes.  *)
+    type endianness
+
+    (** The operating system  *)
+    type system
+
+    (** The application binary interface  *)
+    type abi
+
+    (** The floating-point ABI  *)
+    type fabi
+
+    (** The file format  *)
+    type format
+
+    (** The set of target-specific options.  *)
+    type options = (options_cls,unit) KB.cls KB.Value.t and options_cls
+
+    (** [declare ?package name] declares a new execution target.
+
+        The packaged name of the target must be unique and the target
+        shall be declared during the module registration (commonly as
+        a toplevel definition of a module that implements the target
+        support package).
+
+        The newly declared target inherits all the parameters from the
+        [parent] target unless they are explicitly overriden.
+
+        For the description of parameters see the corresponding
+        accessor functions in this module.
+    *)
+    val declare :
+      ?parent:t ->               (** defaults to [unknown] *)
+      ?bits:int ->               (** defaults to [32] *)
+      ?byte:int ->               (** defaults to [8]  *)
+      ?data:_ Mem.t Var.t ->     (** defaults to [mem : Mem(bits,byte)] *)
+      ?code:_ Mem.t Var.t ->     (** defaults to [mem : Mem(bits,byte)] *)
+      ?vars:unit Var.t list ->   (** defaults to [[]] *)
+      ?endianness:endianness ->  (** defaults to [Endian.big] *)
+      ?system:system ->          (** defaults to [System.unknown]  *)
+      ?abi:abi ->                (** defaults to [Abi.unknown] *)
+      ?fabi:fabi ->              (** defaults to [Fabi.unknown] *)
+      ?format:format ->          (** defaults to [Format.unknown] *)
+      ?options:options ->        (** defaults to [Options.empty] *)
+      ?nicknames:string list ->  (** defaults to [[]] *)
+      ?package:string ->         (** defaults to ["user"] *)
+      string -> t
+
+    (** [lookup ?package name] lookups a target with the given [name].
+
+        If [name] is unqualified then it is qualified with the
+        [package] (which itself defaults to "user"), otherwise the
+        [package] parameter is ignored.
+
+        Returns [None] if the target with the given name wasn't declared.
+    *)
+    val lookup : ?package:string -> string -> t option
+
+    (** [get ?package name] returns the target with the given [name].
+
+        If the target with the given name wasn't declared raises an
+        exception.
+
+        See {!lookup} for the details on the [name] and [package] parameters.
+    *)
+    val get : ?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. *)
+    val declared : unit -> t list
+
+    (** [unknown] the unknown architecture.
+
+        The [core-theory:unknown] is the ancestor of all other
+        architectures with all fields set to defaults as described
+        in {!declare}. *)
+    val unknown : t
+
+    (** [is_unknown t] is [true] if [t] is equal to [unknown].  *)
+    val is_unknown : t -> bool
+
+    (** [name target] is the unique name of the target.  *)
+    val name : t -> KB.Name.t
+
+    (** [matches target name] is true if [name] matches either
+        the unqualified name of the target itsef or one of its
+        ancestors; or if the name matches one of the target
+        nicknames. E.g., [matches target "mips"].
+    *)
+    val matches : t -> string -> bool
+
+    (** [order t t'] the order of [t] and [t'] in the target hierarchy.
+
+        - [order t t'] is [NC] if [t] and [t'] are different and
+          neither [t] is an ancestor of [t'] nor [t'] is an ancestor of [t];
+        - [order t t'] is [LT] if [t] is an ancestor of [t'];
+        - [order t t'] is [GT] if [t'] is an ancestor of [t];
+        - [order t t'] is [EQ] if [t] and [t'] are equal.
+    *)
+    val order : t -> t -> KB.Order.partial
+
+    (** [belongs t t'] iff [order t t'] is [GT] or [EQ].
+
+        The [belongs t] predicate defines a {!family} of targets that
+        are derived from the target [t], e.g., [belongs arm] defines
+        a set of all ARM targets. *)
+    val belongs : t -> t -> bool
+
+    (** [parent t] is the closest ancestor of [t] or [unknown]
+        if [t] is unknown  *)
+    val parent : t -> t
+
+    (** [parents t] returns an ordered list of [t]'s ancestors.
+
+        The closest ancestor comes first in the list and the last
+        element of the list is [unknown].
+    *)
+    val parents : t -> t list
+
+    (** [family p] returns an ordered list of targets that {!belongs} [p].
+
+        The family members are ordered according to their hierarchy
+        with [p] comming first.
+    *)
+    val family : t -> t list
+
+    (** [partition targets] partitions targets into families.
+
+        The partition is a list where each element is a list of family
+        members with the family parent coming as the first member and
+        all other members ordered in the ascending order of their
+        hierarchy, i.e., for each [p::fs] in [families ()]
+        [family p] is [p:fs]. The families itself are partitioned by
+        the lexical order of the unqualified names of the family
+        parents.
+    *)
+    val partition : t list -> t list list
+
+    (** [families ()] partitions all declared targets into families,
+        i.e., it is [partition @@ declared ()].
+    *)
+    val families : unit -> t list list
+
+    (** [bits target] is the bitness of the target architecture.
+
+        It is commonly the number of bits of the machine word in the
+        given architecture and corresponds to the logical width of the
+        data bus.
+    *)
+    val bits : t -> int
+
+
+    (** [byte target] is the size of the target's byte. *)
+    val byte : t -> int
+
+    (** [data_addr_size target] is the number of bits in the data address.
+
+        The logical size of the data address, which is taken
+        from the sort of the keys of the [data] memory variable. *)
+    val data_addr_size : t -> int
+
+    (** [code_addr_size target] the size of the program counter.
+
+        The size of the instruction address, which is taken
+        from the sort of the keys of the [data] memory variable. *)
+    val code_addr_size : t -> int
+
+    (** [data target] the main memory variable. *)
+    val data : t -> (unit,unit) Mem.t Var.t
+
+    (** [code target] the code memory variable. *)
+    val code : t -> (unit,unit) Mem.t Var.t
+
+    (** [vars target] is the set of all registers and memories.
+
+        The set includes both general-purpose, floating-points, and
+        status registers, as well variables that denote memories and
+        other entities specific to the target.
+    *)
+    val vars : t -> Set.M(Var.Top).t
+
+    (** [endianness target] describes the byte order.
+
+        Describes how multibyte words are stored in the main memory. *)
+    val endianness : t -> endianness
+
+    (** [system target] the target operating system.  *)
+    val system : t -> system
+
+    (** [abi target] the target application binary interface.  *)
+    val abi : t -> abi
+
+    (** [fabi target] the target floating-point ABI.  *)
+    val fabi : t -> fabi
+
+    (** [format target] the target file format.  *)
+    val format : t -> format
+
+    (** [options target] the target-specific set of options.  *)
+    val options : t -> options
+
+
+    (** Defines how multibyte words are stored in the memory.
+
+        The number of variants are essentially infinite, given that
+        there is an infinite number of variants of the byte and word
+        sizes, but the two orderings are the most common: little and
+        big endian. More orderings could be declared when necessary.
+    *)
+    module Endianness : sig
+      include Base.Comparable.S with type t = endianness
+      include Binable.S with type t := t
+      include Stringable.S with type t := t
+      include Pretty_printer.S with type t := t
+
+      (** In the big endian ordering the most significant byte of the
+          word is stored at the smallest address.   *)
+      val eb : endianness
+
+      (** In the little endian ordering the least significant byte of
+          the word is stored at the largest address. *)
+      val le : endianness
+
+
+      (** In the bi-endian order the endianness is essentially
+          unspecified and depends on the execution context, e.g.,
+          on the status register or memory page descriptor.  *)
+      val bi : endianness
+
+      (** [declare ?package string] declares a new byte ordering.
+
+          The [package] [name] pair should be unique.
+      *)
+      val declare : ?package:string -> string -> endianness
+
+      (** the unique name  *)
+      val name : endianness -> KB.Name.t
+    end
+
+
+    (** The Operating System.*)
+    module System : sig
+      include Base.Comparable.S with type t = system
+      include Binable.S with type t := t
+      include Stringable.S with type t := t
+      include Pretty_printer.S with type t := t
+
+      (** [declare ?package string] declares a new operating system.
+
+          The [package] [name] pair should be unique.
+      *)
+      val declare : ?package:string -> string -> system
+
+      (** the unique name  *)
+      val name : system -> KB.Name.t
+    end
+
+    (** The Application Binary Interface name  *)
+    module Abi : sig
+      include Base.Comparable.S with type t = abi
+      include Binable.S with type t := t
+      include Stringable.S with type t := t
+      include Pretty_printer.S with type t := t
+
+
+      (** [declare ?package string] declares a new ABI.
+
+          The [package] [name] pair should be unique.*)
+      val declare : ?package:string -> string -> abi
+
+      (** the unique name of the ABI  *)
+      val name : abi -> KB.Name.t
+    end
+
+    (** The Application Floating-point Binary Interface name  *)
+    module Fabi : sig
+      include Base.Comparable.S with type t = fabi
+      include Binable.S with type t := t
+      include Stringable.S with type t := t
+      include Pretty_printer.S with type t := t
+
+      (** [declare ?package string] declares a new FABI.
+
+          The [package] [name] pair should be unique.*)
+      val declare : ?package:string -> string -> fabi
+
+      (** the unique name of the FABI  *)
+      val name : fabi -> KB.Name.t
+    end
+
+
+    (** An extensible set of the target options.
+
+        The set is represented with the {!KB.Value.t},
+        to add a new property, use {!KB.Class.property},
+        to access existing properties use {!KB.Value.get}
+        and {!KB.Value.put}.
+    *)
+    module Options : sig
+      type cls = options_cls
+      include KB.Value.S with type t = options
+      include Binable.S with type t := t
+      include Pretty_printer.S with type t := t
+
+      (** the class index of the target properties  *)
+      val cls : (cls, unit) KB.cls
+
+
+      (** the textual representation of the set of properties.  *)
+      val to_string : t -> string
+    end
+  end
+
+
   (** A unit of code.
 
       A unit of code is a generic piece of code, i.e., a set of
@@ -1124,6 +1519,8 @@ module Theory : sig
     (** the meta type of the unit object  *)
     type t = cls KB.Object.t
 
+    type compiler
+
 
     (** the base class for all units.
 
@@ -1159,10 +1556,6 @@ module Theory : sig
     (** [path] is the path of the file from which the unit originates.  *)
     val path : (cls, string option) KB.slot
 
-
-    (** [format] the file format of the unit, e.g., ["elf"].*)
-    val format : (cls, string option) KB.slot
-
     (** [is-executed] is true if the unit is an executable file ready
         to be executed by the operating system. *)
     val is_executable : (cls, bool option) KB.slot
@@ -1181,71 +1574,70 @@ module Theory : sig
     *)
     val bias : (cls, Bitvec.t option) KB.slot
 
-    (** Information about the target architecture.
-
-        Assuming that the code is produced from source the target
-        denotes the target for which this source is built and
-        tailored. This module provides information about the target
-        triplet and target features.
-    *)
-    module Target : sig
-
-      (** [arch] the target architecture, e.g., [arm].  *)
-      val arch : (cls, string option) KB.slot
-
-      (** [subarch] the target subarchitecture designator, e.g, [v7]  *)
-      val subarch : (cls, string option) KB.slot
+    (** [target] the target on which this unit should be executed.   *)
+    val target : (cls, Target.t) KB.slot
 
-      (** [vendor] the target vendor, e.g., [apple] *)
-      val vendor : (cls, string option) KB.slot
+    (** [source] the source of this unit. *)
+    val source : (cls, Source.t) KB.slot
 
-      (** [system] the target operating system, e.g., [darwin]  *)
-      val system : (cls, string option) KB.slot
+    (** [compiler] the program that translated the unit from the [source].  *)
+    val compiler : (cls, compiler option) KB.slot
 
-      (** [bits] the number of bits in the machine word, e.g., [32]  *)
-      val bits   : (cls, int option) KB.slot
+    (** Information about the compiler.
 
-      (** [abi] target's ABI, e.g., [gnueabi].  *)
-      val abi    : (cls, string option) KB.slot
+        A compiler is a translator that was used to translate
+        the code in this unit from the source to the target
+        representation.
+    *)
+    module Compiler : sig
+      include Base.Comparable.S with type t = compiler
+      include Binable.S with type t := t
+      include Pretty_printer.S with type t := t
 
-      (** [fabi] targets floating-point ABI, e.g., [hf]  *)
-      val fabi   : (cls, string option) KB.slot
+      (** [declare name] declares a compiler.
 
-      (** [cpu] the target CPU, e.g., [cortex] *)
-      val cpu    : (cls, string option) KB.slot
+          The compiler here represents more of a process that compiled
+          the unit rather than a specific program, thus it includes
+          the configuration parameters and command-line options.
+      *)
+      val create :
+        ?specs:(string * string) list ->
+        ?version:string list ->
+        ?options:string list ->
+        string -> compiler
 
-      (** [fpu] the target FPU.  *)
-      val fpu    : (cls, string option) KB.slot
+      (** [version] the compiler version.
 
+          The least specific (aka major) version comes first in the
+          list, with more detailed versions added after. The exact
+          meaning of the version consituents is specific to the compiler.
+      *)
+      val version : compiler -> string list
 
-      (** [is_little_endian] is true if the target's default
-          endianness is the little endian order.   *)
-      val is_little_endian : (cls, bool option) KB.slot
-    end
+      (** [options] the list of options that were used to compile the unit.
 
-    (** Information about the code source.  *)
-    module Source : sig
+          Options are specified as a list of command-line options with
+          possible repetitions. The meaning of the options is specific
+          to the compiler.
 
-      (** [language] the programming language in which the code of
-          this unit was written.  *)
-      val language : (cls, string option) KB.slot
-    end
+          Note, that [options] are the options passed to the compiler
+          when this compilation unit was compiled from the source, not
+          the options of the compiler itsef, for the latter see [specs].
+      *)
+      val options : compiler -> string list
 
-    (** Information about the compiler.
 
-        A compiler is a translator that was used to translate
-        the code in this unit from the source to the target
-        representation.
-    *)
-    module Compiler : sig
+      (** [specs] the configuration of the compiler.
 
-      (** [name] the compiler name  *)
-      val name : (cls, string option) KB.slot
+          A key-value storage of the configuration parameters of the
+          compiler itself. *)
+      val specs : compiler -> string Map.M(String).t
 
-      (** [version] the compiler version.  *)
-      val version : (cls, string option) KB.slot
+      (** is the textual representation of the compiler descriptor  *)
+      val to_string : compiler -> string
     end
 
+
     include Knowledge.Object.S with type t := t
   end
 
@@ -1298,6 +1690,8 @@ module Theory : sig
     (** a compilation unit (file/library/object) to which this label belongs  *)
     val unit : (program, Unit.t option) KB.slot
 
+    (** [target label] is the [Unit.target] of the label's [unit].   *)
+    val target : label -> Target.t knowledge
 
     (** a link is valid if it references a valid program.
 
diff --git a/lib/bap_core_theory/bap_core_theory_program.ml b/lib/bap_core_theory/bap_core_theory_program.ml
index d60df4d3fe..c0a62a1b77 100644
--- a/lib/bap_core_theory/bap_core_theory_program.ml
+++ b/lib/bap_core_theory/bap_core_theory_program.ml
@@ -4,6 +4,7 @@ open Bap_knowledge
 
 let package = "core-theory"
 module Effect = Bap_core_theory_effect
+module Target = Bap_core_theory_target
 
 type cls = Program
 type program = cls
@@ -46,6 +47,52 @@ let string_property ?(domain=name) ~desc cls name =
     ~public:true
     ~desc
 
+module Source = struct
+  type cls = Source
+  let cls : (cls,unit) Knowledge.cls =
+    Knowledge.Class.declare ~package "unit-source" ()
+
+  type language = Knowledge.Name.t
+
+  module Language = struct
+    type t = Knowledge.Name.t [@@deriving bin_io]
+    let declare ?package name = Knowledge.Name.create ?package name
+    let unknown = Knowledge.Name.read ":unknown"
+    let name x = x
+    include Base.Comparable.Make(Knowledge.Name)
+
+    let domain = Knowledge.Domain.flat
+        ~inspect:Knowledge.Name.sexp_of_t
+        ~empty:unknown
+        ~equal "language"
+
+    include (Knowledge.Name : Stringable.S with type t := t)
+    include (Knowledge.Name : Pretty_printer.S with type t := t)
+  end
+
+  let language = Knowledge.Class.property cls
+      ~package "source-language" Language.domain
+      ~persistent:Knowledge.Persistent.name
+      ~public:true
+      ~desc:"the language of the unit's source code"
+
+  let code = Knowledge.Class.property cls
+      ~package "source-code" Knowledge.Domain.string
+      ~persistent:Knowledge.Persistent.string
+      ~public:true
+      ~desc:"the units source code text"
+
+  let file = string_property ~domain:path cls "source-path"
+      ~desc:"a path to the source code file"
+
+  module Value = (val Knowledge.Value.derive cls)
+
+  let persistent = Knowledge.Persistent.of_binable (module Value)
+
+  include Value
+
+end
+
 module Unit = struct
   open Knowledge.Syntax
   type cls = Unit
@@ -96,63 +143,66 @@ module Unit = struct
     Knowledge.Symbol.intern ~package:"region" name cls
 
 
-  module Target = struct
-    let arch = string_property cls "target-arch"
-        ~desc:"target machine architecture"
-    let subarch = string_property cls "target-subarch"
-        ~desc:"target machine subarchitecture"
-    let vendor = string_property cls "target-vendor"
-        ~desc:"target machine vendor"
-    let system = string_property cls "target-system"
-        ~desc:"target machine operating system"
-    let abi = string_property cls "target-abi"
-        ~desc:"target machine application binary interface"
-    let fabi = string_property cls "target-fabi"
-        ~desc:"target machine floating-point binary interface"
-    let cpu = string_property cls "target-cpu"
-        ~desc:"target machine CPU model"
-    let fpu = string_property cls "target-fpu"
-        ~desc:"target machine FPU model"
-
-    let bits = Knowledge.Domain.optional "bits"
-        ~equal:Int.equal
-        ~inspect:sexp_of_int
-
-    let bits =
-      Knowledge.Class.property ~package cls "target-bits" bits
-        ~persistent:(Knowledge.Persistent.of_binable (module struct
-                       type t = int option [@@deriving bin_io]
-                     end))
-        ~public:true
-        ~desc:"the bitness of the architecture"
-
-    let is_little_endian =
-      Knowledge.Class.property ~package cls "target-is-little-endian"
-        Knowledge.Domain.bool
-        ~persistent:(Knowledge.Persistent.of_binable (module struct
-                       type t = bool option [@@deriving bin_io]
-                     end))
-        ~public:true
-        ~desc:"whether the target architecture is little endian"
-  end
+  let target =
+    Knowledge.Class.property ~package cls "unit-target" Target.domain
+      ~persistent:Target.persistent
+      ~public:true
+      ~desc:"the target system for the unit"
 
-  module Source = struct
-    let language = string_property cls "source-language"
-        ~desc:"the original source language"
-  end
 
-  module Compiler = struct
-    let name = string_property cls "compiler-name"
-        ~desc:"the name of the compiler used to build the unit"
+  let source =
+    Knowledge.Class.property ~package cls "unit-source" Source.domain
+      ~persistent:Source.persistent
+      ~public:true
+      ~desc:"the source of the unit"
 
-    let version = string_property cls "compiler-version"
-        ~desc:"the version of the compiler used to build the unit"
+
+  module Compiler = struct
+    type t = {
+      name : string;
+      version : string list;
+      options : string list;
+      specs : string String.Map.t;
+    } [@@deriving bin_io, compare, equal, fields, sexp]
+
+    let create ?(specs=[]) ?(version=[]) ?(options=[]) name = {
+      name; version; options;
+      specs = String.Map.of_alist_exn specs;
+    }
+
+    let pp ppf x = Sexp.pp_hum ppf (sexp_of_t x)
+
+    let to_string x = Format.asprintf "%a" pp x
+
+    let persistent = Knowledge.Persistent.of_binable (module struct
+        type nonrec t = t option [@@deriving bin_io]
+      end)
+
+    let domain = Knowledge.Domain.optional
+        ~inspect:sexp_of_t
+        ~equal
+        "compiler"
+
+    include Base.Comparable.Make(struct
+        type nonrec t = t [@@deriving bin_io, compare, sexp]
+      end)
   end
 
+  type compiler = Compiler.t
+
+  let compiler = Knowledge.Class.property ~package cls "unit-compiler"
+      Compiler.domain
+      ~persistent:Compiler.persistent
+      ~public:true
+      ~desc:"the compiler that compiles/compiled the unit"
+
+
   include (val Knowledge.Object.derive cls)
 
 end
 
+
+
 module Label = struct
 
   let int = Knowledge.Domain.optional "ivec"
@@ -240,6 +290,11 @@ module Label = struct
     Knowledge.Symbol.intern ?package s cls >>= fun obj ->
     Knowledge.provide ivec obj (Some x) >>| fun () -> obj
 
+  let target x =
+    Knowledge.collect unit x >>= function
+    | None -> Knowledge.return Target.unknown
+    | Some unit -> Knowledge.collect Unit.target unit
+
   let _decide_name_from_possible_name : unit =
     Knowledge.Rule.(declare ~package "name-of-possible-names" |>
                     require possible_name |>
diff --git a/lib/bap_core_theory/bap_core_theory_program.mli b/lib/bap_core_theory/bap_core_theory_program.mli
index aca4245328..9414419a9d 100644
--- a/lib/bap_core_theory/bap_core_theory_program.mli
+++ b/lib/bap_core_theory/bap_core_theory_program.mli
@@ -2,6 +2,7 @@ open Core_kernel
 open Bap_knowledge
 
 module Effect = Bap_core_theory_effect
+module Target = Bap_core_theory_target
 
 type cls
 type program = cls
@@ -17,12 +18,39 @@ end
 
 include Knowledge.Value.S with type t := t
 
+module Source : sig
+  open Knowledge
+  type cls
+  include Knowledge.Value.S with type t = (cls,unit) Class.t Value.t
+
+  type language
+
+  val cls : (cls,unit) Class.t
+
+  val language : (cls,language) slot
+
+  val code : (cls,string) slot
+
+  val file : (cls,string option) slot
+
+  module Language : sig
+    include Base.Comparable.S with type t = language
+    include Binable.S with type t := t
+    include Stringable.S with type t := t
+    include Pretty_printer.S with type t := t
+    val declare : ?package:string -> string -> language
+    val name : language -> Knowledge.Name.t
+  end
+end
+
 module Unit : sig
   open Knowledge
   type cls
 
   type t = cls obj
 
+  type compiler
+
   val cls : (cls,unit) Class.t
 
   val for_file : string -> t knowledge
@@ -34,26 +62,24 @@ module Unit : sig
   val is_executable : (cls, bool option) slot
   val bias : (cls, Bitvec.t option) slot
 
-  module Target : sig
-    val arch : (cls, string option) slot
-    val subarch : (cls, string option) slot
-    val vendor : (cls, string option) slot
-    val system : (cls, string option) slot
-    val bits   : (cls, int option) slot
-    val abi    : (cls, string option) slot
-    val fabi   : (cls, string option) slot
-    val cpu    : (cls, string option) slot
-    val fpu    : (cls, string option) slot
-    val is_little_endian : (cls, bool option) slot
-  end
-
-  module Source : sig
-    val language : (cls, string option) slot
-  end
+  val target : (cls, Target.t) slot
+  val source : (cls, Source.t) slot
+  val compiler : (cls, compiler option) slot
 
   module Compiler : sig
-    val name : (cls, string option) slot
-    val version : (cls, string option) slot
+    include Base.Comparable.S with type t = compiler
+    include Binable.S with type t := t
+    include Pretty_printer.S with type t := t
+
+    val create :
+      ?specs:(string * string) list ->
+      ?version:string list ->
+      ?options:string list ->
+      string -> compiler
+    val version : compiler -> string list
+    val options : compiler -> string list
+    val specs : compiler -> string Map.M(String).t
+    val to_string : compiler -> string
   end
 
   include Knowledge.Object.S with type t := t
@@ -74,6 +100,7 @@ module Label : sig
   val for_addr : ?package:string -> Bitvec.t -> t knowledge
   val for_name : ?package:string -> string -> t knowledge
   val for_ivec : ?package:string -> int -> t knowledge
+  val target : t -> Target.t knowledge
 
   include Knowledge.Object.S with type t := t
 end
diff --git a/lib/bap_core_theory/bap_core_theory_target.ml b/lib/bap_core_theory/bap_core_theory_target.ml
new file mode 100644
index 0000000000..0ae52e0712
--- /dev/null
+++ b/lib/bap_core_theory/bap_core_theory_target.ml
@@ -0,0 +1,260 @@
+open Core_kernel
+open Bap_knowledge
+
+module KB = Knowledge
+module Var = Bap_core_theory_var
+module Val = Bap_core_theory_value
+module Mem = Val.Mem
+module Bitv = Val.Bitv
+module Sort = Val.Sort
+module Name = KB.Name
+
+
+let package = "core-theory"
+
+type t = Name.t [@@deriving bin_io, compare, sexp]
+type target = t
+type endianness = Name.t
+type system = Name.t
+type abi = Name.t
+type format = Name.t
+type fabi = Name.t
+type name = Name.t
+
+module Enum = struct
+  type t = Name.t [@@deriving bin_io]
+  let declare ?package name = Name.create ?package name
+  let read ?package name = Name.read ?package name
+  let name x = x
+  include Base.Comparable.Make(Name)
+  include (Name : Stringable.S with type t := t)
+  include (Name : Pretty_printer.S with type t := t)
+
+end
+
+module Endianness = struct
+  include Enum
+  let le = declare ~package "le"
+  let eb = declare ~package "eb"
+  let bi = declare ~package "bi"
+end
+
+module System = Enum
+module Abi = Enum
+module Fabi = Enum
+
+module Options = struct
+  type cls = Options
+  let cls : (cls,unit) KB.cls = KB.Class.declare ~package "target-options" ()
+  let pp ppf x = KB.Value.pp ppf x
+  let to_string x = Format.asprintf "%a" pp x
+  include (val KB.Value.derive cls)
+end
+
+type options = Options.t and options_cls = Options.cls
+
+type mem = Var : ('a,'b) Mem.t Var.t -> mem
+
+type info = {
+  parent : target;
+  bits : int;
+  byte : int;
+  data : mem;
+  code : mem;
+  vars : Set.M(Var.Top).t;
+  endianness : Name.t;
+  system : Name.t;
+  abi : Name.t;
+  fabi : Name.t;
+  format : Name.t;
+  options : Options.t;
+  names : String.Caseless.Set.t
+}
+
+let unknown = Name.create ~package:KB.Symbol.keyword "unknown"
+let empty = unknown
+
+let mem name k v =
+  let k = Bitv.(define k)
+  and v = Bitv.(define v) in
+  Var.define (Mem.define k v) name
+
+let pack v = Var v
+
+let unpack (Var var) =
+  let s = Var.sort var in
+  let k = Bitv.size@@Mem.keys s
+  and v = Bitv.size@@Mem.vals s in
+  mem (Var.name var) k v
+
+
+let unknown = {
+  parent = unknown;
+  bits = 32;
+  byte = 8;
+  data = pack@@mem "mem" 32 8;
+  code = pack@@mem "mem" 32 8;
+  vars = Set.empty (module Var.Top);
+  endianness = Endianness.eb;
+  system = unknown;
+  abi = unknown;
+  fabi = unknown;
+  format = unknown;
+  options = Options.empty;
+  names = String.Caseless.Set.empty;
+}
+
+let targets = Hashtbl.of_alist_exn (module Name) [
+    unknown.parent, unknown
+  ]
+
+let extend parent
+    ?(bits=parent.bits)
+    ?(byte=parent.byte)
+    ?(data=unpack@@parent.data)
+    ?(code=unpack@@parent.code)
+    ?vars
+    ?(endianness=parent.endianness)
+    ?(system=parent.system)
+    ?(abi=parent.abi)
+    ?(fabi=parent.fabi)
+    ?(format=parent.format)
+    ?(options=parent.options)
+    ?nicknames name = {
+  parent=name; bits; byte; endianness;
+  system; abi; fabi; format;
+  options;
+  data = pack data;
+  code = pack code;
+  vars = Option.value_map vars
+      ~default:parent.vars
+      ~f:(Set.of_list (module Var.Top));
+  names = Option.value_map nicknames
+      ~default:parent.names
+      ~f:String.Caseless.Set.of_list;
+}
+
+let declare
+    ?(parent=unknown.parent)
+    ?bits ?byte ?data ?code ?vars ?endianness
+    ?system ?abi ?fabi ?format ?options
+    ?nicknames ?package name =
+  let name = Name.create ?package name in
+  if Hashtbl.mem targets name
+  then failwithf "A target with name %s already exists \
+                  in the package %s, please choose another \
+                  name or package"
+      (Name.unqualified name)
+      (Name.package name) ();
+  let p = Hashtbl.find_exn targets parent in
+  let info = extend ?bits ?byte ?data ?code ?vars ?endianness
+      ?system ?abi ?fabi ?format ?options ?nicknames p parent in
+  Hashtbl.add_exn targets name info;
+  name
+
+let lookup ?package name =
+  let name = Name.read ?package name in
+  if Hashtbl.mem targets name then Some name
+  else None
+
+let get ?package name =
+  let name = Name.read ?package name in
+  if not (Hashtbl.mem targets name)
+  then invalid_argf "Unknown target %s" (Name.to_string name) ();
+  name
+
+let info name = match Hashtbl.find targets name with
+  | None -> unknown
+  | Some t -> t
+
+let parent t = (info t).parent
+let name t = t
+let bits t = (info t).bits
+let byte t = (info t).byte
+let data t = unpack@@(info t).data
+let code t = unpack@@(info t).code
+let vars t = (info t).vars
+
+let data_addr_size,
+    code_addr_size =
+  let keys v = Bitv.size @@ Mem.keys @@ Var.sort v in
+  (fun t -> keys @@ data t),
+  (fun t -> keys @@ code t)
+
+let endianness t = (info t).endianness
+let system t = (info t).system
+let abi t = (info t).abi
+let fabi t = (info t).fabi
+let format t = (info t).format
+let options t = (info t).options
+
+let parents target =
+  let rec closure ps p =
+    if p = unknown.parent
+    then List.rev (p::ps)
+    else closure (p::ps) (parent p) in
+  closure [] (parent target)
+
+let is_unknown c = Name.equal c unknown.parent
+let is_known c = not@@is_unknown c
+
+let rec belongs p c =
+  Name.equal p c || is_known c && belongs p (parent c)
+
+let rec matches_name t name =
+  String.Caseless.equal (Name.unqualified t) name ||
+  is_known t && matches_name (parent t) name
+
+let rec matches t name =
+  let nicks = (info t).names in
+  Set.mem nicks name || matches_name t name
+
+let order t1 t2 : KB.Order.partial =
+  if Name.equal t1 t2 then EQ
+  else if belongs t1 t2 then LT
+  else if belongs t2 t1 then GT
+  else NC
+
+let declared () = Hashtbl.keys targets |>
+                  List.filter ~f:is_known
+
+let sort_family_by_order =
+  List.sort ~compare:(fun t1 t2 -> match order t1 t2 with
+      | KB.Order.NC | EQ -> 0
+      | LT -> -1
+      | GT -> 1)
+
+let sort_by_parent_name =
+  List.sort ~compare:(fun f1 f2 -> match f1,f2 with
+      | t1::_, t2::_ ->
+        String.compare (Name.unqualified t1) (Name.unqualified t2)
+      | _ -> 0)
+
+let family t =
+  declared () |>
+  List.filter ~f:(belongs t) |>
+  sort_family_by_order
+
+let partition xs =
+  let families = Map.empty (module Name) in
+  let universe = Set.of_list (module Name) xs in
+  let rec grandest t =
+    let p = parent t in
+    if is_known p && Set.mem universe p
+    then grandest p else t in
+  List.fold xs ~init:families ~f:(fun families t ->
+      Map.add_multi families (grandest t) t) |>
+  Map.data |>
+  List.map ~f:sort_family_by_order |>
+  sort_by_parent_name
+
+let families () = partition@@declared ()
+
+let unknown = empty
+let domain = KB.Domain.define ~empty ~order "target"
+    ~inspect:sexp_of_t
+let persistent = KB.Persistent.name
+
+include (Name : Base.Comparable.S with type t := t)
+include (Name : Stringable.S with type t := t)
+include (Name : Pretty_printer.S with type t := t)
diff --git a/lib/bap_core_theory/bap_core_theory_target.mli b/lib/bap_core_theory/bap_core_theory_target.mli
new file mode 100644
index 0000000000..d46e8e17b7
--- /dev/null
+++ b/lib/bap_core_theory/bap_core_theory_target.mli
@@ -0,0 +1,115 @@
+open Core_kernel
+open Bap_knowledge
+
+module KB = Knowledge
+module Var = Bap_core_theory_var
+module Mem = Bap_core_theory_value.Mem
+
+type t [@@deriving bin_io, compare, sexp]
+type endianness
+type system
+type abi
+type fabi
+type format
+type options = (options_cls,unit) KB.Class.t KB.Value.t and options_cls
+
+val declare :
+  ?parent:t ->
+  ?bits:int ->
+  ?byte:int ->
+  ?data:_ Mem.t Var.t ->
+  ?code:_ Mem.t Var.t ->
+  ?vars:unit Var.t list ->
+  ?endianness:endianness ->
+  ?system:system ->
+  ?abi:abi ->
+  ?fabi:fabi ->
+  ?format:format ->
+  ?options:options ->
+  ?nicknames:string list ->
+  ?package:string ->
+  string -> t
+
+val get : ?package:string -> string -> t
+val lookup : ?package:string -> string -> t option
+val unknown : t
+val is_unknown : t -> bool
+val name : t -> KB.Name.t
+val matches : t -> string -> bool
+val order : t -> t -> KB.Order.partial
+val belongs : t -> t -> bool
+val parent : t -> t
+val parents : t -> t list
+val declared : unit -> t list
+val family : t -> t list
+val partition : t list -> t list list
+val families : unit -> t list list
+val bits : t -> int
+val byte : t -> int
+val data_addr_size : t -> int
+val code_addr_size : t -> int
+val data : t -> (unit,unit) Mem.t Var.t
+val code : t -> (unit,unit) Mem.t Var.t
+val vars : t -> Set.M(Var.Top).t
+val endianness : t -> endianness
+val system : t -> system
+val abi : t -> abi
+val fabi : t -> fabi
+val format : t -> format
+val options : t -> options
+
+val domain : t KB.Domain.t
+val persistent : t KB.Persistent.t
+
+module Endianness : sig
+  include Base.Comparable.S with type t = endianness
+  include Binable.S with type t := t
+  include Stringable.S with type t := t
+  include Pretty_printer.S with type t := t
+  val le : endianness
+  val eb : endianness
+  val bi : endianness
+  val declare : ?package:string -> string -> endianness
+  val name : endianness -> KB.Name.t
+end
+
+module System : sig
+  include Base.Comparable.S with type t = system
+  include Binable.S with type t := t
+  include Stringable.S with type t := t
+  include Pretty_printer.S with type t := t
+  val declare : ?package:string -> string -> system
+  val name : system -> KB.Name.t
+end
+
+module Abi : sig
+  include Base.Comparable.S with type t = abi
+  include Binable.S with type t := t
+  include Stringable.S with type t := t
+  include Pretty_printer.S with type t := t
+  val declare : ?package:string -> string -> abi
+  val name : abi -> KB.Name.t
+end
+
+module Fabi : sig
+  include Base.Comparable.S with type t = fabi
+  include Binable.S with type t := t
+  include Stringable.S with type t := t
+  include Pretty_printer.S with type t := t
+  val declare : ?package:string -> string -> fabi
+  val name : fabi -> KB.Name.t
+end
+
+module Options : sig
+  type cls = options_cls
+  include KB.Value.S with type t = options
+  include Binable.S with type t := t
+  include Pretty_printer.S with type t := t
+  val cls : (cls, unit) KB.cls
+  val to_string : t -> string
+end
+
+include Base.Comparable.S with type t := t
+include Binable.S with type t := t
+include Stringable.S with type t := t
+include Pretty_printer.S with type t := t
diff --git a/lib/bap_disasm/bap_disasm_rec.ml b/lib/bap_disasm/bap_disasm_rec.ml
index 8dbf17dec3..9f92bcd6c3 100644
--- a/lib/bap_disasm/bap_disasm_rec.ml
+++ b/lib/bap_disasm/bap_disasm_rec.ml
@@ -113,20 +113,14 @@ let with_unit =
            comment "[Rec.{run,scan} arch mem] provides a unit for [mem]");
   fun arch mem ->
     let width = Size.in_bits (Arch.addr_size arch) in
-    let is_little = Arch.endian arch = LittleEndian in
     let lower = Word.to_bitvec @@ Memory.min_addr mem
     and upper = Word.to_bitvec @@ Memory.max_addr mem in
     KB.promising Theory.Label.unit ~promise:(fun label ->
         KB.collect Theory.Label.addr label >>= function
         | Some p when Memory.contains mem @@ Word.create p width ->
           Theory.Unit.for_region ~lower ~upper >>= fun unit ->
-          let (:=) slot value = KB.provide slot unit (Some value) in
-          KB.List.sequence Theory.Unit.[
-              Target.bits := width;
-              Target.arch := Arch.to_string arch;
-              Target.is_little_endian := is_little;
-            ] >>= fun () ->
-          KB.return (Some unit)
+          KB.provide Arch.unit_slot unit arch >>| fun () ->
+          Some unit
         | _ -> KB.return None)
 
 let scan arch mem state =
diff --git a/lib/bap_disasm/bap_disasm_symtab.ml b/lib/bap_disasm/bap_disasm_symtab.ml
index cfbf8a29be..bd9e6be927 100644
--- a/lib/bap_disasm/bap_disasm_symtab.ml
+++ b/lib/bap_disasm/bap_disasm_symtab.ml
@@ -155,10 +155,7 @@ let build_cfg disasm calls entry =
 
 let build_symbol disasm calls start =
   build_cfg disasm calls start >>= function
-  | None ->
-    Format.eprintf "Failed to obtain a CFG from %a@\n%!"
-      Addr.pp start;
-    assert false
+  | None -> failwith "Broken CFG, try bap --cache-clean"
   | Some (entry,graph) ->
     Symbolizer.get_name start >>| fun name ->
     name,entry,graph
diff --git a/lib/bap_mips/bap_mips_target.ml b/lib/bap_mips/bap_mips_target.ml
new file mode 100644
index 0000000000..35f4cd2666
--- /dev/null
+++ b/lib/bap_mips/bap_mips_target.ml
@@ -0,0 +1,117 @@
+open Core_kernel
+open Bap_core_theory
+open Bap.Std
+
+
+let package = "bap"
+
+type r128 and r80 and r64 and r32 and r16 and r8
+
+type 'a bitv = 'a Theory.Bitv.t Theory.Value.sort
+
+let r128 : r128 bitv = Theory.Bitv.define 128
+let r80 : r80 bitv = Theory.Bitv.define 80
+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 gpr_names = [
+  "AT";
+  "V0"; "V1";
+  "A0"; "A1"; "A2"; "A3";
+  "T0"; "T1"; "T2"; "T3"; "T4"; "T5"; "T6"; "T7";
+  "S0"; "S1"; "S2"; "S3"; "S4"; "S5"; "S6"; "S7";
+  "T8"; "T9";
+  "K0"; "K1";
+  "GP";
+  "SP";
+  "FP";
+  "RA"
+]
+
+let untyped = List.map ~f:Theory.Var.forget
+let (@<) xs ys = untyped xs @ untyped ys
+
+let name size order  =
+  let order = Theory.Target.Endianness.name order in
+  sprintf "mips%d+%s" size (KB.Name.unqualified order)
+
+let parent = Theory.Target.declare ~package "mips"
+
+let define ?(parent=parent) bits endianness =
+  let size = Theory.Bitv.size bits in
+  let gprs = List.map gpr_names ~f:(reg bits) in
+  let mems = Theory.Mem.define bits r8 in
+  let data = Theory.Var.define mems "mem" in
+  let vars = gprs @< [data] in
+  Theory.Target.declare ~package (name size endianness)
+    ~parent
+    ~bits:size
+    ~endianness
+    ~vars
+    ~code:data
+    ~data:data
+
+
+let mips32bi = define r32 Theory.Target.Endianness.bi
+let mips32eb = define r32 Theory.Target.Endianness.eb ~parent:mips32bi
+let mips32le = define r32 Theory.Target.Endianness.le ~parent:mips32bi
+
+let mips64bi = define r64 Theory.Target.Endianness.bi
+let mips64le = define r64 Theory.Target.Endianness.le ~parent:mips64bi
+let mips64eb = define r64 Theory.Target.Endianness.eb ~parent:mips64bi
+
+let enable_loader () =
+  KB.Rule.(declare ~package "mips-target" |>
+           require Project.specification_slot |>
+           provide Theory.Unit.target |>
+           comment "computes target from the OGRE specification");
+  let open KB.Syntax in
+  let request_info doc =
+    let open Ogre.Syntax in
+    let request =
+      Ogre.request Image.Scheme.arch >>= fun arch ->
+      Ogre.request Image.Scheme.is_little_endian >>= fun little ->
+      Ogre.return (arch,little) in
+    match Ogre.eval request doc with
+    | Error _ -> None,None
+    | Ok info -> info in
+  KB.promise Theory.Unit.target @@ fun unit ->
+  KB.collect Project.specification_slot unit >>|
+  request_info >>| function
+  | Some "mips", None -> mips32bi
+  | Some "mips64",None -> mips64bi
+  | Some "mips",Some true -> mips32le
+  | Some "mips64",Some true -> mips64le
+  | Some "mips",Some false -> mips32eb
+  | Some "mips64",Some false -> mips64eb
+  | _ -> Theory.Target.unknown
+
+
+let mapped_mips = Map.of_alist_exn (module Theory.Target) [
+    mips32eb, `mips;
+    mips32le, `mipsel;
+    mips64eb, `mips64;
+    mips64le, `mips64el;
+  ]
+
+let map_mips () =
+  KB.Rule.(declare ~package "mips-arch" |>
+           require Theory.Unit.target |>
+           provide Arch.unit_slot |>
+           comment "computes Arch.t from the unit's target");
+  let open KB.Syntax in
+  KB.promise Arch.unit_slot @@ fun unit ->
+  KB.collect Theory.Unit.target unit >>|
+  Map.find mapped_mips >>| function
+  | Some arch -> arch
+  | None -> `unknown
+
+
+let load () =
+  enable_loader ();
+  map_mips ()
diff --git a/lib/bap_mips/bap_mips_target.mli b/lib/bap_mips/bap_mips_target.mli
new file mode 100644
index 0000000000..bac8e5eebc
--- /dev/null
+++ b/lib/bap_mips/bap_mips_target.mli
@@ -0,0 +1,34 @@
+(** Declares some of the MIPS targets.
+
+    More targets could be added without modifying this module. It is
+    advised to inherit from one of the targets defined here to include
+    the newly defined target into the mips family, though it is not
+    strictly required.
+*)
+open Bap_core_theory
+
+
+(** [parent] it the parent of all MIPS.
+
+    No properties are set. *)
+val parent : Theory.Target.t
+
+(** {3 The MIPS 32 family}*)
+
+val mips32bi : Theory.Target.t (** The bi-endian MIPS32 (the parent)  *)
+val mips32eb : Theory.Target.t (** The big endian MIPS32  *)
+val mips32le : Theory.Target.t (** The little endian MIPS32  *)
+
+(** {3 The MIPS 64 family}*)
+
+val mips64bi : Theory.Target.t (** The bi-endian MIPS64 (the parent)  *)
+val mips64eb : Theory.Target.t (** The big endian MIPS64  *)
+val mips64le : Theory.Target.t (** The little endian MIPS64  *)
+
+
+(** [load ()] loads the knowledge base rules for the MIPS targets.
+
+    This includes parsing the loader output and enabling backward
+    compatibility with the old [Arch.t] representation.
+*)
+val load : unit -> unit
diff --git a/lib/bap_powerpc/bap_powerpc_target.ml b/lib/bap_powerpc/bap_powerpc_target.ml
new file mode 100644
index 0000000000..05f29d4fb5
--- /dev/null
+++ b/lib/bap_powerpc/bap_powerpc_target.ml
@@ -0,0 +1,112 @@
+open Core_kernel
+open Bap_core_theory
+open Bap.Std
+
+
+let package = "bap"
+
+type r128 and r80 and r64 and r32 and r16 and r8
+
+type 'a bitv = 'a Theory.Bitv.t Theory.Value.sort
+
+let r128 : r128 bitv = Theory.Bitv.define 128
+let r80 : r80 bitv = Theory.Bitv.define 80
+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 name size order  =
+  let order = Theory.Target.Endianness.name order in
+  sprintf "powerpc%d+%s" size (KB.Name.unqualified order)
+
+let parent = Theory.Target.declare ~package "powerpc"
+
+let crflags =
+  List.concat @@ List.init 8 ~f:(fun group ->
+      List.map ["UN"; "EQ"; "GT"; "LT"] ~f:(fun f ->
+          reg bool @@ sprintf "CR%d%s" group f))
+
+let flags = List.map ~f:(reg bool) [
+    "SO"; "CA"; "OV";
+    "CA32"; "OV32";
+    "C"; "FL"; "FE"; "FG"; "FU"
+  ] @ crflags
+
+let define ?(parent=parent) bits endianness =
+  let size = Theory.Bitv.size bits in
+  let mems = Theory.Mem.define bits r8 in
+  let data = Theory.Var.define mems "mem" in
+  let vars = array bits "R" 32 @<
+             array bits "F" 32 @<
+             array r128 "VR" 32 @<
+             flags @<
+             [reg bits "CTR"; reg bits "LR"; reg bits "TAR" ] @<
+             [data] in
+  Theory.Target.declare ~package (name size endianness)
+    ~parent
+    ~bits:size
+    ~endianness
+    ~vars
+    ~code:data
+    ~data:data
+
+
+let powerpc32bi = define r32 Theory.Target.Endianness.bi
+let powerpc32eb = define r32 Theory.Target.Endianness.eb ~parent:powerpc32bi
+let powerpc32le = define r32 Theory.Target.Endianness.le ~parent:powerpc32bi
+
+let powerpc64bi = define r64 Theory.Target.Endianness.bi
+let powerpc64le = define r64 Theory.Target.Endianness.le ~parent:powerpc64bi
+let powerpc64eb = define r64 Theory.Target.Endianness.eb ~parent:powerpc64bi
+
+let enable_loader () =
+  let open KB.Syntax in
+  let request_info doc =
+    let open Ogre.Syntax in
+    let request =
+      Ogre.request Image.Scheme.arch >>= fun arch ->
+      Ogre.request Image.Scheme.is_little_endian >>= fun little ->
+      Ogre.return (arch,little) in
+    match Ogre.eval request doc with
+    | Error _ -> None,None
+    | Ok info -> info in
+  KB.promise Theory.Unit.target @@ fun unit ->
+  KB.collect Project.specification_slot unit >>|
+  request_info >>| function
+  | Some "powerpc", None -> powerpc32bi
+  | Some "powerpc64",None -> powerpc64bi
+  | Some "powerpc",Some true -> powerpc32le
+  | Some "powerpc64",Some true -> powerpc64le
+  | Some "powerpc",Some false -> powerpc32eb
+  | Some "powerpc64",Some false -> powerpc64eb
+  | _ -> Theory.Target.unknown
+
+
+let mapped_powerpc = Map.of_alist_exn (module Theory.Target) [
+    powerpc32eb, `ppc;
+    powerpc64eb, `ppc64;
+    powerpc64le, `ppc64le;
+  ]
+
+let map_powerpc () =
+  let open KB.Syntax in
+  KB.promise Arch.unit_slot @@ fun unit ->
+  KB.collect Theory.Unit.target unit >>|
+  Map.find mapped_powerpc >>| function
+  | Some arch -> arch
+  | None -> `unknown
+
+
+let load () =
+  enable_loader ();
+  map_powerpc ()
diff --git a/lib/bap_powerpc/bap_powerpc_target.mli b/lib/bap_powerpc/bap_powerpc_target.mli
new file mode 100644
index 0000000000..a3c6edb7b6
--- /dev/null
+++ b/lib/bap_powerpc/bap_powerpc_target.mli
@@ -0,0 +1,34 @@
+(** Declares some of the PowerPC targets.
+
+    More targets could be added without modifying this module. It is
+    advised to inherit from one of the targets defined here to include
+    the newly defined target into the powerpc family, though it is not
+    strictly required.
+*)
+open Bap_core_theory
+
+
+(** [parent] it the parent of all PowerPC.
+
+    No properties are set. *)
+val parent : Theory.Target.t
+
+(** {3 The PowerPC 32 family}*)
+
+val powerpc32bi : Theory.Target.t (** The bi-endian PowerPC32 (the parent)  *)
+val powerpc32eb : Theory.Target.t (** The big endian PowerPC32  *)
+val powerpc32le : Theory.Target.t (** The little endian PowerPC32  *)
+
+(** {3 The PowerPC 64 family}*)
+
+val powerpc64bi : Theory.Target.t (** The bi-endian PowerPC64 (the parent)  *)
+val powerpc64eb : Theory.Target.t (** The big endian PowerPC64  *)
+val powerpc64le : Theory.Target.t (** The little endian PowerPC64  *)
+
+
+(** [load ()] loads the knowledge base rules for the PowerPC targets.
+
+    This includes parsing the loader output and enabling backward
+    compatibility with the old [Arch.t] representation.
+*)
+val load : unit -> unit
diff --git a/lib/bap_powerpc/bap_powerpc_targets.ml b/lib/bap_powerpc/bap_powerpc_targets.ml
new file mode 100644
index 0000000000..2d70465ae5
--- /dev/null
+++ b/lib/bap_powerpc/bap_powerpc_targets.ml
@@ -0,0 +1,120 @@
+open Core_kernel
+open Bap_core_theory
+open Bap.Std
+
+
+let package = "bap"
+
+type r128 and r80 and r64 and r32 and r16 and r8
+
+type 'a bitv = 'a Theory.Bitv.t Theory.Value.sort
+
+let r128 : r128 bitv = Theory.Bitv.define 128
+let r80 : r80 bitv = Theory.Bitv.define 80
+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 name size order  =
+  let order = Theory.Target.Endianness.name order in
+  sprintf "powerpc%d+%s" size (KB.Name.unqualified order)
+
+let parent = Theory.Target.declare ~package "powerpc"
+
+let crflags =
+  List.concat @@ List.init 8 ~f:(fun group ->
+      List.map ["UN"; "EQ"; "GT"; "LT"] ~f:(fun f ->
+          reg bool @@ sprintf "CR%d%s" group f))
+
+let flags = List.map ~f:(reg bool) [
+    "SO"; "CA"; "OV";
+    "CA32"; "OV32";
+    "C"; "FL"; "FE"; "FG"; "FU"
+  ] @ crflags
+
+let define ?(parent=parent) bits endianness =
+  let size = Theory.Bitv.size bits in
+  let mems = Theory.Mem.define bits r8 in
+  let data = Theory.Var.define mems "mem" in
+  let vars = array bits "R" 32 @<
+             array bits "F" 32 @<
+             array r128 "VR" 32 @<
+             flags @<
+             [reg bits "CTR"; reg bits "LR"; reg bits "TAR" ] @<
+             [data] in
+  Theory.Target.declare ~package (name size endianness)
+    ~parent
+    ~bits:size
+    ~endianness
+    ~vars
+    ~code:data
+    ~data:data
+
+
+let powerpc32bi = define r32 Theory.Target.Endianness.bi
+let powerpc32eb = define r32 Theory.Target.Endianness.eb ~parent:powerpc32bi
+let powerpc32le = define r32 Theory.Target.Endianness.le ~parent:powerpc32bi
+
+let powerpc64bi = define r64 Theory.Target.Endianness.bi
+let powerpc64le = define r64 Theory.Target.Endianness.le ~parent:powerpc64bi
+let powerpc64eb = define r64 Theory.Target.Endianness.eb ~parent:powerpc64bi
+
+let enable_loader () =
+  let open KB.Syntax in
+  KB.Rule.(declare ~package "powerpc-target" |>
+           require Project.specification_slot |>
+           provide Theory.Unit.target |>
+           comment "computes target from the OGRE specification");
+  let request_info doc =
+    let open Ogre.Syntax in
+    let request =
+      Ogre.request Image.Scheme.arch >>= fun arch ->
+      Ogre.request Image.Scheme.is_little_endian >>= fun little ->
+      Ogre.return (arch,little) in
+    match Ogre.eval request doc with
+    | Error _ -> None,None
+    | Ok info -> info in
+  KB.promise Theory.Unit.target @@ fun unit ->
+  KB.collect Project.specification_slot unit >>|
+  request_info >>| function
+  | Some "powerpc", None -> powerpc32bi
+  | Some "powerpc64",None -> powerpc64bi
+  | Some "powerpc",Some true -> powerpc32le
+  | Some "powerpc64",Some true -> powerpc64le
+  | Some "powerpc",Some false -> powerpc32eb
+  | Some "powerpc64",Some false -> powerpc64eb
+  | _ -> Theory.Target.unknown
+
+
+let mapped_powerpc = Map.of_alist_exn (module Theory.Target) [
+    powerpc32eb, `ppc;
+    powerpc64eb, `ppc64;
+    powerpc64le, `ppc64le;
+  ]
+
+let map_powerpc () =
+  let open KB.Syntax in
+  KB.Rule.(declare ~package "powerpc-arch" |>
+           require Theory.Unit.target |>
+           provide Arch.unit_slot |>
+           comment "computes Arch.t from the unit's target");
+  KB.promise Arch.unit_slot @@ fun unit ->
+  KB.collect Theory.Unit.target unit >>|
+  Map.find mapped_powerpc >>| function
+  | Some arch -> arch
+  | None -> `unknown
+
+
+let load () =
+  enable_loader ();
+  map_powerpc ()
diff --git a/lib/bap_types/bap_arch.ml b/lib/bap_types/bap_arch.ml
index 88aa206786..3ee98b8f5f 100644
--- a/lib/bap_types/bap_arch.ml
+++ b/lib/bap_types/bap_arch.ml
@@ -72,32 +72,28 @@ module T = struct
   let domain =
     KB.Domain.flat ~empty:`unknown ~equal ~inspect:sexp_of_t "arch"
 
+  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:(KB.Persistent.of_binable (module struct
-                     type t = arch [@@deriving bin_io]
-                   end))
-      ~public:true
-      ~desc:"an ISA of the program"
+      ~persistent
 
+  let unit_slot = KB.Class.property ~package:"bap"
+      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 Theory.Unit.Target.arch |>
+             require unit_slot |>
              provide slot |>
-             comment "compute arch from the unit target defintions");
+             comment "propagates arch from the unit");
     let open KB.Syntax in
-    let (>>=?) x f =
-      x >>= function
-      | None -> KB.return `unknown
-      | Some x -> f x in
     KB.promise slot @@ fun obj ->
-    KB.collect Theory.Label.unit obj >>=? fun unit ->
-    KB.collect Theory.Unit.Target.arch unit >>=? fun arch ->
-    KB.return (from_string arch)
-
-
+    KB.collect Theory.Label.unit obj >>= function
+    | None -> KB.return `unknown
+    | Some unit -> KB.collect unit_slot unit
 end
 
 include T
diff --git a/lib/bap_types/bap_arch.mli b/lib/bap_types/bap_arch.mli
index 46765cb49d..e3b749a60c 100644
--- a/lib/bap_types/bap_arch.mli
+++ b/lib/bap_types/bap_arch.mli
@@ -11,4 +11,6 @@ val endian : arch -> endian
 
 val slot : (Theory.program, arch) KB.slot
 
+val unit_slot : (Theory.Unit.cls, arch) KB.slot
+
 include Regular.S with type t := arch
diff --git a/lib/bap_types/bap_bitvector.ml b/lib/bap_types/bap_bitvector.ml
index 1bf1950eca..adc52ab07c 100644
--- a/lib/bap_types/bap_bitvector.ml
+++ b/lib/bap_types/bap_bitvector.ml
@@ -1,3 +1,4 @@
+open Bap_core_theory
 open Core_kernel
 open Regular.Std
 open Or_error
@@ -138,6 +139,11 @@ let lift3 = Packed.lift3
 type t = Packed.t [@@deriving bin_io]
 
 let create x w = Packed.create (Bitvec.to_bigint x) w [@@inline]
+let code_addr t x = create x (Theory.Target.code_addr_size t) [@@inline]
+let data_addr t x = create x (Theory.Target.data_addr_size t) [@@inline]
+let data_word t x = create x (Theory.Target.bits t) [@@inline]
+
+
 let to_bitvec x = Packed.payload x [@@inline]
 let unsigned x = x [@@inline]
 let signed x = Packed.signed x [@@inline]
@@ -563,6 +569,7 @@ module Mono = Comparable.Make(struct
         | _ -> failwith "Non monomorphic comparison"
   end)
 
+
 module Trie = struct
   module Common = struct
     type nonrec t = t
diff --git a/lib/bap_types/bap_bitvector.mli b/lib/bap_types/bap_bitvector.mli
index e9ffe7f709..70fa8ed3f8 100644
--- a/lib/bap_types/bap_bitvector.mli
+++ b/lib/bap_types/bap_bitvector.mli
@@ -1,3 +1,4 @@
+open Bap_core_theory
 open Core_kernel
 open Regular.Std
 open Format
@@ -14,6 +15,11 @@ include Bap_integer.S with type t := t
 module Mono : Comparable.S with type t := t
 
 val create : Bitvec.t -> int -> t
+
+val code_addr : Theory.Target.t -> Bitvec.t -> t
+val data_addr : Theory.Target.t -> Bitvec.t -> t
+val data_word : Theory.Target.t -> Bitvec.t -> t
+
 val to_bitvec : t -> Bitvec.t
 
 val of_string : string -> t
diff --git a/lib/x86_cpu/x86_target.ml b/lib/x86_cpu/x86_target.ml
new file mode 100644
index 0000000000..9d9b521ab8
--- /dev/null
+++ b/lib/x86_cpu/x86_target.ml
@@ -0,0 +1,231 @@
+open Bap_core_theory
+open Core_kernel
+
+let package = "bap"
+
+type r128 and r80 and r64 and r32 and r16 and r8
+
+type 'a bitv = 'a Theory.Bitv.t Theory.Value.sort
+
+let r128 : r128 bitv = Theory.Bitv.define 128
+let r80 : r80 bitv = Theory.Bitv.define 80
+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 untyped = List.map ~f:Theory.Var.forget
+
+let (@<) xs ys = untyped xs @ untyped ys
+
+let array ?(index=string_of_int) t pref size =
+  List.init size ~f:(fun i -> reg t (pref ^ index i))
+
+module M16 = struct
+  let main = [
+    reg r16 "AX";
+    reg r16 "BX";
+    reg r16 "CX";
+    reg r16 "DX";
+  ]
+
+  let index = [
+    reg r16 "SI";
+    reg r16 "DI";
+    reg r16 "BP";
+    reg r16 "SP";
+  ]
+
+  let segment = [
+    reg r16 "CS";
+    reg r16 "DS";
+    reg r16 "ES";
+    reg r16 "SS";
+  ]
+
+  let flags = [
+    reg bool "CF";
+    reg bool "PF";
+    reg bool "AF";
+    reg bool "ZF";
+    reg bool "SF";
+    reg bool "TF";
+    reg bool "IF";
+    reg bool "DF";
+    reg bool "OF";
+  ]
+
+  let mems = Theory.Mem.define r16 r8
+  let data = Theory.Var.define mems "mem"
+
+  let vars = main @< index @< segment @< flags @< [data]
+end
+
+module M32 = struct
+  let main = [
+    reg r32 "EAX";
+    reg r32 "EBX";
+    reg r32 "ECX";
+    reg r32 "EDX";
+  ]
+
+  let index = [
+    reg r32 "ESI";
+    reg r32 "EDI";
+    reg r32 "EBP";
+    reg r32 "ESP";
+  ]
+
+  let segment = [
+    reg r16 "CS";
+    reg r16 "DS";
+    reg r16 "ES";
+    reg r16 "SS";
+    reg r16 "FS";
+    reg r16 "GS";
+  ]
+
+  let flags = M16.flags
+
+  let stx = array r80 "ST" 8
+  let mmx = array r64 "MM" 8
+  let xmmx = array r128 "XMM" 8
+
+  let mems = Theory.Mem.define r32 r8
+  let data = Theory.Var.define mems "mem"
+
+  let i386 = main @< index @< segment @< flags @< [data]
+  let i486 = i386 @< stx
+  let i586 = i486 @< mmx
+  let i686 = i586 @< xmmx
+end
+
+module M64 = struct
+  let main = [
+    reg r64 "RAX";
+    reg r64 "RBX";
+    reg r64 "RCX";
+    reg r64 "RDX";
+  ]
+
+  let index = [
+    reg r64 "RSI";
+    reg r64 "RDI";
+    reg r64 "RBP";
+    reg r64 "RSP";
+  ]
+
+  let segment = [
+    reg r16 "CS";
+    reg r16 "DS";
+    reg r16 "ES";
+    reg r16 "SS";
+  ]
+
+  let rx = array r64 "R" 8
+      ~index:(fun i -> string_of_int (i+8))
+
+  let stx = M32.stx
+  let mmx = M32.mmx
+  let xmmx = array r128 "XMM" 16
+
+  let flags = M32.flags
+  let mems = Theory.Mem.define r64 r8
+  let data = Theory.Var.define mems "mem"
+
+  let vars = main @< index @< segment @< rx @< stx @< mmx @< xmmx @<
+             flags @< [data]
+end
+
+let parent = Theory.Target.declare ~package "x86"
+
+let i86 = Theory.Target.declare ~package "i86"
+    ~parent
+    ~nicknames:["8086"]
+    ~bits:16
+    ~byte:8
+    ~data:M16.data
+    ~code:M16.data
+    ~vars:M16.vars
+    ~endianness:Theory.Target.Endianness.le
+
+let i186 = Theory.Target.declare ~package "i186"
+    ~parent:i86
+    ~nicknames:["80186"; "186"]
+
+let i286 = Theory.Target.declare ~package "i286"
+    ~parent:i186
+    ~nicknames:["80286"; "286"]
+
+let i386 = Theory.Target.declare ~package "i386"
+    ~parent:i286
+    ~nicknames:["386"; "80386"]
+    ~bits:32
+    ~data:M32.data
+    ~code:M32.data
+    ~vars:M32.i386
+
+let i486 = Theory.Target.declare ~package "i486"
+    ~parent:i386
+    ~nicknames:["486"; "80486"]
+    ~vars:M32.i486
+
+let i586 = Theory.Target.declare ~package "i586"
+    ~parent:i486
+    ~nicknames:["586"; "80586"; "p5"]
+
+let i686 = Theory.Target.declare ~package "i686"
+    ~parent:i586
+    ~nicknames:["686"; "80686"; "p6"]
+
+let amd64 = Theory.Target.declare ~package "amd64"
+    ~parent:i686
+    ~nicknames:["x64"; "x86_64"; "x86-64"; ]
+    ~bits:32
+    ~data:M64.data
+    ~code:M64.data
+    ~vars:M64.vars
+
+
+let family = [amd64; i686; i586; i486; i386; i86]
+
+let enable_loader () =
+  let open Bap.Std in
+  let open KB.Syntax in
+  KB.Rule.(declare ~package "x86-target" |>
+           require Project.specification_slot |>
+           provide Theory.Unit.target |>
+           comment "computes target from the OGRE specification");
+  let request_arch doc =
+    match Ogre.eval (Ogre.request Image.Scheme.arch) doc with
+    | Error _ -> None
+    | Ok arch -> arch in
+  KB.promise Theory.Unit.target @@ fun unit ->
+  KB.collect Project.specification_slot unit >>|
+  request_arch >>| function
+  | Some ("amd64"|"x86-64"|"x86_64") -> amd64
+  | Some ("x86"|"i386"|"i486"|"i586"|"i686") -> i686
+  | _ -> Theory.Target.unknown
+
+let enable_arch () =
+  let open Bap.Std in
+  let open KB.Syntax in
+  KB.Rule.(declare ~package "x86-arch" |>
+           require Theory.Unit.target |>
+           provide Arch.unit_slot |>
+           comment "computes Arch.t from the unit's target");
+  KB.promise Arch.unit_slot @@ fun unit ->
+  KB.collect Theory.Unit.target unit >>| fun t ->
+  if Theory.Target.belongs amd64 t
+  then `x86_64
+  else if Theory.Target.belongs i386 t
+  then `x86
+  else `unknown
+
+let load () =
+  enable_loader ();
+  enable_arch ()
diff --git a/lib/x86_cpu/x86_target.mli b/lib/x86_cpu/x86_target.mli
new file mode 100644
index 0000000000..9d57f223a7
--- /dev/null
+++ b/lib/x86_cpu/x86_target.mli
@@ -0,0 +1,28 @@
+(** Declarations of some x86 targets.  *)
+
+open Bap_core_theory
+
+(** The parent of all x86 targets.
+
+    When a new target is declared it is advised to use this target as
+    parent so that the newly declared target will be included into the
+    x86 Targets family.
+    The [parent] target is pure abstract and doesn't have any
+    propreties set.
+*)
+val parent : Theory.Target.t
+val i86 : Theory.Target.t
+val i186 : Theory.Target.t
+val i286 : Theory.Target.t
+val i386 : Theory.Target.t
+val i486 : Theory.Target.t
+val i586 : Theory.Target.t
+val i686 : Theory.Target.t
+val amd64 : Theory.Target.t
+
+(** [load ()] loads the knowledge base rules for the x86 targets.
+
+    This includes parsing the loader output and enabling backward
+    compatibility with the old [Arch.t] representation.
+*)
+val load : unit -> unit
diff --git a/oasis/arm b/oasis/arm
index 48a5295169..dc05161e9b 100644
--- a/oasis/arm
+++ b/oasis/arm
@@ -6,8 +6,8 @@ Library "bap-arm"
  XMETADescription: arm lifting
  Path:             lib/arm
  Build$:           flag(everything) || flag(arm)
- BuildDepends:     bap
- BuildDepends:     bap, core_kernel, ppx_jane, regular
+ BuildDepends:     bap, core_kernel, ppx_jane, regular,
+                   bap-core-theory, bap-knowledge, ogre
  FindlibName:      bap-arm
  Modules:
                  ARM,
@@ -26,6 +26,7 @@ Library "bap-arm"
                  Arm_op,
                  Arm_reg,
                  Arm_shift,
+                 Arm_target,
                  Arm_types,
                  Arm_utils
 
diff --git a/oasis/core-theory b/oasis/core-theory
index 3812199c40..780517c0d2 100644
--- a/oasis/core-theory
+++ b/oasis/core-theory
@@ -20,5 +20,6 @@ Library bap_core_theory
         Bap_core_theory_program,
         Bap_core_theory_manager,
         Bap_core_theory_parser,
+        Bap_core_theory_target,
         Bap_core_theory_value,
         Bap_core_theory_var
diff --git a/oasis/mips b/oasis/mips
index f4a50ce3f4..f30244daf0 100644
--- a/oasis/mips
+++ b/oasis/mips
@@ -2,12 +2,21 @@ Flag mips
   Description: Build MIPS lifter
   Default: true
 
+Library "bap-mips"
+ Build$:           flag(everything) || flag(mips)
+ XMETADescription: common definitions for MIPS targets
+ Path: lib/bap_mips
+ BuildDepends: core_kernel, ppx_jane,
+               ogre, bap-knowledge, bap-core-theory, bap
+ FindlibName: bap-mips
+ Modules: Bap_mips_target
+
 Library mips_plugin
   XMETADescription:     provide MIPS lifter
   Path:                 plugins/mips
   FindlibName:          bap-plugin-mips
   Build$:               flag(everything) || flag (mips)
-  BuildDepends:         bap, bap-abi, bap-c, bap-core-theory, core_kernel,
+  BuildDepends:         bap, bap-mips, bap-abi, bap-c, bap-core-theory, core_kernel,
                         ppx_jane, regular, zarith, bap-knowledge, bap-main, bap-api
   InternalModules:
                         Mips,
diff --git a/oasis/powerpc b/oasis/powerpc
index 803627f726..d6f5058a10 100644
--- a/oasis/powerpc
+++ b/oasis/powerpc
@@ -2,12 +2,21 @@ Flag powerpc
  Description: Build PowerPC lifter
  Default: false
 
+Library "bap-powerpc"
+ Build$:           flag(everything) || flag(powerpc)
+ XMETADescription: common definitions for PowerPC targets
+ Path: lib/bap_powerpc
+ BuildDepends: core_kernel, ppx_jane,
+               ogre, bap-knowledge, bap-core-theory, bap
+ FindlibName: bap-powerpc
+ Modules: Bap_powerpc_target
+
 Library powerpc_plugin
   XMETADescription: provide PowerPC lifter
   Path:             plugins/powerpc
   Build$:           flag(everything) || flag(powerpc)
   BuildDepends:     bap, bap-abi, bap-c, zarith, monads, core_kernel,
-                    ppx_jane, regular, bap-api
+                    ppx_jane, regular, bap-api, bap-powerpc
   FindlibName:      bap-plugin-powerpc
   InternalModules:  Powerpc,
                     Powerpc_cpu,
diff --git a/oasis/x86 b/oasis/x86
index 88c3fb0654..f7b4604e2d 100644
--- a/oasis/x86
+++ b/oasis/x86
@@ -7,13 +7,15 @@ Library "bap-x86-cpu"
  XMETADescription: provide x86 lifter
  Path:             lib/x86_cpu
  FindlibName:      bap-x86-cpu
- BuildDepends:     bap, core_kernel, ppx_jane
+ BuildDepends:     bap, core_kernel, ppx_jane,
+                   bap-core-theory, ogre, bap-knowledge
  Modules:          X86_cpu,
                    X86_env,
                    X86_asm,
                    X86_asm_reg,
                    X86_asm_reg_types,
                    X86_llvm_env,
+                   X86_target,
                    X86_types
 
 Library x86_plugin
@@ -46,7 +48,7 @@ Library x86_plugin
                    X86_opcode_scas,
                    X86_opcode_stos,
                    X86_operands,
-                   X86_target,
+                   X86_targets,
                    X86_tools,
                    X86_tools_flags,
                    X86_tools_imm,
diff --git a/opam/opam b/opam/opam
index be0cbbb977..b746befacb 100644
--- a/opam/opam
+++ b/opam/opam
@@ -9,7 +9,7 @@ bug-reports: "https://github.com/BinaryAnalysisPlatform/bap/issues"
 depends: [
   "ocaml" {>= "4.07.0"}
   "base-unix"
-  "bitstring"
+  "bitstring" {>= "3.0.0" & < "4.0.0"}
   "camlzip"
   "linenoise" {>= "1.1" & < "2.0"}
   "cmdliner" {>= "1.0" & < "2.0"}
diff --git a/plugins/analyze/analyze_core_commands.ml b/plugins/analyze/analyze_core_commands.ml
index 462ba6ab43..38f96900bd 100644
--- a/plugins/analyze/analyze_core_commands.ml
+++ b/plugins/analyze/analyze_core_commands.ml
@@ -39,7 +39,8 @@ let belongs_to_subr subr insn =
     require Theory.Label.addr subr @@ fun subr ->
     require Theory.Label.unit insn @@ fun unit ->
     require Theory.Label.addr insn @@ fun insn ->
-    require Theory.Unit.Target.bits unit @@ fun bits ->
+    KB.collect Theory.Unit.target unit >>|
+    Theory.Target.code_addr_size >>= fun bits ->
     KB.collect Project.State.slot unit >>| fun state ->
     let subrs = Project.State.subroutines state in
     let insn = Word.create insn bits
@@ -67,25 +68,12 @@ let iter_subr entry subrs disasm ~f =
     ~node:(fun insns () -> KB.List.iter insns ~f)
     ~edge:(fun _ _ _ -> KB.return ())
 
-
-let make_triple unit =
-  KB.collect Theory.Unit.Target.arch   unit >>= fun arch ->
-  KB.collect Theory.Unit.Target.subarch unit >>= fun sub ->
-  KB.collect Theory.Unit.Target.vendor unit >>= fun vendor ->
-  KB.collect Theory.Unit.Target.system unit >>= fun system ->
-  KB.collect Theory.Unit.Target.abi unit >>| fun abi ->
-  let (=?) x default = Option.value x ~default in
-  sprintf "%s%s-%s-%s-%s"
-    (arch =? "unknown") (sub =? "") (vendor =? "none")
-    (system =? "unknown") (abi =? "unknown")
-
-
 let print_unit () =
   KB.objects Theory.Unit.cls >>=
   KB.Seq.iter ~f:(fun obj ->
       KB.Object.repr Theory.Unit.cls obj >>= fun str ->
-      make_triple obj >>| fun triple ->
-      Format.printf "%-40s %s@\n" str triple)
+      KB.collect Theory.Unit.target obj >>| fun triple ->
+      Format.printf "%-40s %a@\n" str Theory.Target.pp triple)
 
 let ensure x yes =
   x >>= function
@@ -113,10 +101,6 @@ let list_insns unit slots =
       ensure (belongs_to_unit unit obj) @@ fun () ->
       print_insn slots obj)
 
-let word_for_unit unit bitvec =
-  KB.collect Theory.Unit.Target.bits unit >>|? fun bits ->
-  Some (Word.create bitvec bits)
-
 let print_subr unit name_or_addr slots =
   KB.collect Project.State.slot unit >>= fun state ->
   KB.Symbol.package >>= fun current ->
diff --git a/plugins/arm/.merlin b/plugins/arm/.merlin
index 18f35eff9d..b8b7c0ecfa 100644
--- a/plugins/arm/.merlin
+++ b/plugins/arm/.merlin
@@ -6,6 +6,11 @@ B ../../_build/lib/arm
 B ../../_build/lib/bap_api
 B ../../_build/lib/bap_abi
 
+B ../../lib/bap_c
+B ../../lib/arm
+B ../../lib/bap_api
+B ../../lib/bap_abi
+
 S ../../lib/bap_c
 S ../../lib/arm
 S ../../lib/bap_api
diff --git a/plugins/arm/arm_main.ml b/plugins/arm/arm_main.ml
index 83f3e1b83e..942499d3d4 100644
--- a/plugins/arm/arm_main.ml
+++ b/plugins/arm/arm_main.ml
@@ -35,6 +35,7 @@ end
 
 let () =
   Config.when_ready (fun _ ->
+      Arm_target.load ();
       List.iter Arch.all_of_arm ~f:(fun arch ->
           register_target (arch :> arch) (module ARM);
           Arm_gnueabi.setup ()))
diff --git a/plugins/mips/mips_main.ml b/plugins/mips/mips_main.ml
index 54a2bebdfe..caac3d242c 100644
--- a/plugins/mips/mips_main.ml
+++ b/plugins/mips/mips_main.ml
@@ -39,6 +39,7 @@ module MIPS64_le = Make(M64LE)
 
 let () =
   Config.when_ready (fun _ ->
+      Bap_mips_target.load ();
       register_target `mips (module MIPS32);
       register_target `mipsel (module MIPS32_le);
       register_target `mips64 (module MIPS64);
diff --git a/plugins/objdump/objdump_main.ml b/plugins/objdump/objdump_main.ml
index 1c9961f8ec..1249832a85 100644
--- a/plugins/objdump/objdump_main.ml
+++ b/plugins/objdump/objdump_main.ml
@@ -187,9 +187,10 @@ let provide_function_starts_and_names ctxt : unit =
     KB.collect Theory.Label.unit label >>=? fun unit ->
     KB.collect Theory.Unit.path unit >>=? fun path ->
     KB.collect Theory.Unit.bias unit >>= fun bias ->
-    KB.collect Theory.Unit.Target.bits unit >>= fun size ->
+    KB.collect Theory.Unit.target unit >>|
+    Theory.Target.code_addr_size >>= fun size ->
     KB.collect key_slot label >>|? fun key ->
-    f (Repository.name repo ?size ?bias ~path key) in
+    f (Repository.name repo ~size ?bias ~path key) in
   let is_known = function
     | None -> None
     | Some _ -> Some true in
diff --git a/plugins/powerpc/powerpc_main.ml b/plugins/powerpc/powerpc_main.ml
index f26102d9bd..adfd06773a 100644
--- a/plugins/powerpc/powerpc_main.ml
+++ b/plugins/powerpc/powerpc_main.ml
@@ -40,6 +40,7 @@ module PowerPC64_le = Make(T64_le)
 let () =
   Config.when_ready (fun _ ->
       info "Providing PowerPC semantics in BIL";
+      Bap_powerpc_target.load ();
       Powerpc_add.init ();
       Powerpc_branch.init ();
       Powerpc_compare.init ();
diff --git a/plugins/radare2/.merlin b/plugins/radare2/.merlin
index 06df5fe6ac..e4e061bda0 100644
--- a/plugins/radare2/.merlin
+++ b/plugins/radare2/.merlin
@@ -1,5 +1,5 @@
-PKG bap
 PKG yojson
+PKG zarith
 B ../../_build/plugins/radare2
 B ../../lib/bap_relation
 REC
diff --git a/plugins/radare2/radare2_main.ml b/plugins/radare2/radare2_main.ml
index 713eb37cf7..2ff0e09aab 100644
--- a/plugins/radare2/radare2_main.ml
+++ b/plugins/radare2/radare2_main.ml
@@ -17,7 +17,8 @@ let provide_roots file funcs =
     KB.collect Theory.Label.addr label >>=? fun addr ->
     KB.collect Theory.Label.unit label >>=? fun unit ->
     KB.collect Theory.Unit.bias unit >>= fun bias ->
-    KB.collect Theory.Unit.Target.bits unit >>=? fun bits ->
+    KB.collect Theory.Unit.target unit >>|
+    Theory.Target.code_addr_size >>= fun bits ->
     KB.collect Theory.Unit.path unit >>|? fun path ->
     if String.equal path file then
       let bias = Option.value bias ~default:Bitvec.zero in
diff --git a/plugins/relocatable/rel_symbolizer.ml b/plugins/relocatable/rel_symbolizer.ml
index b330aa534a..38b5dd6874 100644
--- a/plugins/relocatable/rel_symbolizer.ml
+++ b/plugins/relocatable/rel_symbolizer.ml
@@ -186,9 +186,9 @@ let mark_mips_stubs_as_functions refs file : unit =
   KB.collect Theory.Label.addr label >>=? fun addr ->
   KB.collect Theory.Label.unit label >>=? fun unit ->
   KB.collect Theory.Unit.path unit >>=? fun path ->
-  KB.collect Theory.Unit.Target.arch unit >>|? fun arch ->
+  KB.collect Theory.Unit.target unit >>| fun target ->
   let is_entry = path = file &&
-                 (arch = "mips" || arch = "mips64") &&
+                 (Theory.Target.matches target "mips") &&
                  Option.is_some (References.lookup refs addr) in
   Option.some_if is_entry true
 
@@ -202,7 +202,7 @@ let () = Extension.declare ~doc @@ fun _ctxt ->
            require Theory.Label.addr |>
            require Theory.Label.unit |>
            require Theory.Unit.path |>
-           require Theory.Unit.Target.arch |>
+           require Theory.Unit.target |>
            dynamic ["specification"] |>
            dynamic ["filename"] |>
            provide Theory.Label.is_subroutine |>
diff --git a/plugins/stub_resolver/.merlin b/plugins/stub_resolver/.merlin
index 22f213b7c8..962ce741a2 100644
--- a/plugins/stub_resolver/.merlin
+++ b/plugins/stub_resolver/.merlin
@@ -1,7 +1,3 @@
-PKG core_kernel
-PKG oUnit
-PKG bap
-PKG bap-abi
-
 S .
-B ../../_build/plugins/stub_resolver
\ No newline at end of file
+B ../../_build/plugins/stub_resolver
+REC
\ No newline at end of file
diff --git a/plugins/stub_resolver/stub_resolver_main.ml b/plugins/stub_resolver/stub_resolver_main.ml
index 85f54f27aa..d02b133835 100644
--- a/plugins/stub_resolver/stub_resolver_main.ml
+++ b/plugins/stub_resolver/stub_resolver_main.ml
@@ -68,21 +68,19 @@ let signatures = Extension.Configuration.parameters
     Extension.Type.(list path) "signatures"
     ~doc:("A list of folders and files that contain signatures for \
            stubs identification. Each file shall have a name of the \
-           form $(b,<triple>.stubs) and contain a list of words each \
+           form $(b,<target>.stubs) and contain a list of words each \
            denoting a possible starting sequence of a bytes for a \
-           stub. The triple has the form \
-           $(b,<arch><subarch>-<system>-<abi>). Only $(b,<arch>) is \
-           required, all other fileds could be omitted (or filled in \
-           with $(b,unknown). E.g., $(b,arm.stubs), \
-           $(b,armv7-linux-gnueabi.stubs), etc. Each word denoting a \
-           signature must be encoded as an ASCII number and be binary \
-           (start with $(b,0b)), octal (start with $(b,0o), or \
-           hexadecimal (start with $(b,0x), e.g., $(b,0xDEADBEEF). If \
-           the prefix is omitted then the hexadecimal notation is \
-           assumed, e.g., $(b,DEADBEEF) is also acceptable. The \
-           signature length is automatically inferred from the word, \
-           i.e., the leading zeros are not discarded. By default we \
-           search in the current working folder and in " ^
+           stub. The <target> is the name of the target, e.g., \
+           $(b,arm.stubs), $(b,armv7-linux-gnueabi.stubs), etc. Each \
+           word denoting a signature must be encoded as an ASCII \
+           number and be binary (start with $(b,0b)), octal (start \
+           with $(b,0o), or hexadecimal (start with $(b,0x), e.g., \
+           $(b,0xDEADBEEF). If the prefix is omitted then the \
+           hexadecimal notation is assumed, e.g., $(b,DEADBEEF) is \
+           also acceptable. The signature length is automatically \
+           inferred from the word, i.e., the leading zeros are not \
+           discarded. By default we search in the current working \
+           folder and in " ^
           default_signatures_folder)
 
 module Stubs : sig
@@ -130,12 +128,8 @@ end
 
 module Signatures : sig
   type t
-  type triple
   val collect : ctxt -> t
-
-  val triple : ?arch:string -> ?subarch:string -> ?system:string ->
-    ?abi:string -> unit -> triple
-  val matching : triple -> t -> Word.Set.t
+  val matching : Theory.Target.t -> t -> Word.Set.t
 end = struct
   type parser_outcome =
     | Success of word
@@ -143,9 +137,7 @@ end = struct
     | Empty
     | Comment
 
-  type triple = string list list
-  type t = (string list * Word.Set.t) list
-
+  type t = (string * Word.Set.t) list
 
   let is_prefixed s =
     String.length s > 1 && match s.[0],s.[1] with
@@ -185,27 +177,12 @@ end = struct
             file (number+1) msg;
           words)
 
-  let parse_triple s = String.split s ~on:'-' |> List.map ~f:(function
-      | "" -> "unknown"
-      | s -> s)
-
   let parse_filename s =
     match String.split (Filename.basename s) ~on:'.' with
     | [""; "stubs"] -> None      (* for .stubs *)
-    | [triple; "stubs"] -> Some (parse_triple triple)
+    | [name; "stubs"] -> Some name
     | _ -> None
 
-  let matches xs ys =
-    let rec next xs ys = match xs,ys with
-      | x :: xs, y::ys -> matches x y xs ys
-      | _,[]|[],_ -> true
-    and matches x y xs ys = match x,y with
-      | _,"unknown" | "unknown",_
-      | _,"" | "",_ -> next xs ys
-      | x,y -> x = y && next xs ys in
-    next xs ys
-
-
   let collect ctxt : t =
     let signatures = Extension.Configuration.get ctxt signatures in
     let paths = Filename.current_dir_name ::
@@ -224,21 +201,12 @@ end = struct
         then add_files sigs path
         else add_file sigs path)
 
-  let triple
-      ?(arch="unknown")
-      ?(subarch="")
-      ?(system="unknown")
-      ?(abi="unknown") () = [
-    [arch; system; abi];
-    [arch^subarch; system; abi];
-  ]
-
-  let matching triple sigs =
-    let all t = Word.Set.union_list @@
-      List.filter_map sigs ~f:(fun (t' ,s) ->
-          Option.some_if (matches t t') s) in
-    Set.union_list (module Word) @@
-    List.map triple ~f:all
+
+  let matching target sigs =
+    Word.Set.union_list @@
+    List.filter_map sigs ~f:(fun (t' ,s) ->
+        Option.some_if (Theory.Target.matches target t') s)
+
 end
 
 let mark_plt_as_stub ctxt : unit =
@@ -269,25 +237,14 @@ let word_of_memory mem =
   Word.create (bitvec_of_memory mem) width
 
 
-let collect_triple unit =
-  KB.collect Theory.Unit.Target.arch unit >>= fun arch ->
-  KB.collect Theory.Unit.Target.subarch unit >>= fun subarch ->
-  KB.collect Theory.Unit.Target.system unit >>= fun system ->
-  KB.collect Theory.Unit.Target.abi unit >>| fun abi ->
-  Signatures.triple ?arch ?subarch ?system ?abi ()
 
 let with_path_and_unit label f =
   KB.collect Theory.Label.unit label >>=? fun unit ->
   KB.collect Theory.Unit.path unit >>=? fun path ->
   f path unit
 
-let with_context label f =
-  with_path_and_unit label @@ fun path unit ->
-  collect_triple unit >>= fun triple ->
-  f path triple
-
-let find_mem bits code addr =
-  let addr = Word.create addr bits in
+let find_mem target code addr =
+  let addr = Word.code_addr target addr in
   Memmap.lookup code addr |>
   Seq.find_map ~f:(fun (mem,_) ->
       match Memory.view ~from:addr mem with
@@ -316,10 +273,9 @@ let detect_stubs_by_signatures ctxt : unit =
   KB.promise (Value.Tag.slot Sub.stub) @@ fun label ->
   KB.collect Theory.Label.addr label >>=? fun addr ->
   with_path_and_unit label @@ fun path unit ->
-  collect_triple unit >>= fun triple ->
-  KB.collect Theory.Unit.Target.bits unit >>|? fun bits ->
-  Option.bind (find_mem bits code addr) ~f:(fun mem ->
-      let sigs = Signatures.matching triple sigs in
+  KB.collect Theory.Unit.target unit >>| fun target ->
+  Option.bind (find_mem target code addr) ~f:(fun mem ->
+      let sigs = Signatures.matching target sigs in
       Option.some_if (path = file && matches sigs mem) ())
 
 let update prog =
diff --git a/plugins/x86/.merlin b/plugins/x86/.merlin
index 41adeef62d..1ccb622706 100644
--- a/plugins/x86/.merlin
+++ b/plugins/x86/.merlin
@@ -3,4 +3,9 @@ B ../../_build/lib/bap_abi
 B ../../_build/lib/bap_api
 B ../../_build/lib/x86_cpu
 B ../../_build/lib/bap_c
+B ../../plugins/x86
+B ../../lib/bap_abi
+B ../../lib/bap_api
+B ../../lib/x86_cpu
+B ../../lib/bap_c
 REC
\ No newline at end of file
diff --git a/plugins/x86/x86_main.ml b/plugins/x86/x86_main.ml
index cfd4dc29e7..bb23098be9 100644
--- a/plugins/x86/x86_main.ml
+++ b/plugins/x86/x86_main.ml
@@ -1,11 +1,12 @@
 open Core_kernel
 open Bap.Std
-open X86_target
+open X86_targets
 include Self()
 
 type kind = Legacy | Modern | Merge [@@deriving equal]
 
 let main kind x32 x64 =
+  X86_target.load ();
   let ia32, amd64 = match kind with
     | Legacy -> (module IA32L : Target), (module AMD64L : Target)
     | Modern -> (module IA32 : Target), (module AMD64 : Target)
diff --git a/plugins/x86/x86_target.ml b/plugins/x86/x86_targets.ml
similarity index 92%
rename from plugins/x86/x86_target.ml
rename to plugins/x86/x86_targets.ml
index 578149e8f0..0565ee89e4 100644
--- a/plugins/x86/x86_target.ml
+++ b/plugins/x86/x86_targets.ml
@@ -8,13 +8,13 @@ module AMD64L = X86_lifter.AMD64
 
 module IA32D = struct
   module CPU = IA32L.CPU
-  let lift mem insn =
+  let lift _mem insn =
     Or_error.error "unimplemented" insn Insn.sexp_of_t
 end
 
 module AMD64D = struct
   module CPU = AMD64L.CPU
-  let lift mem insn =
+  let lift _mem insn =
     Or_error.error "unimplemented" insn Insn.sexp_of_t
 end
 
diff --git a/plugins/x86/x86_target.mli b/plugins/x86/x86_targets.mli
similarity index 100%
rename from plugins/x86/x86_target.mli
rename to plugins/x86/x86_targets.mli