overhauls the target/architecture abstraction (3/n)

lib/arm/arm_target.ml

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

lib/bap_core_theory/bap_core_theory.mli

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

lib/bap_core_theory/bap_core_theory_target.ml

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

lib/bap_core_theory/bap_core_theory_target.mli

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

lib/bap_image/bap_memory.ml

@@ -461,3 +461,16 @@ let slot = KB.Class.property ~package:"bap"
     Theory.Program.cls "mem" domain
     ~public:true
     ~desc:"a memory region occupied by the program"
+
+let () =
+  let open KB.Syntax in
+  KB.promise Theory.Label.addr @@ fun label ->
+  KB.collect slot label >>|? fun mem ->
+  Some (Addr.to_bitvec (min_addr mem))
+
+let () =
+  let open KB.Rule in
+  declare ~package:"bap" "addr-of-mem" |>
+  require slot |>
+  provide Theory.Label.addr |>
+  comment "addr of the first byte"

lib/bap_systemz/bap_systemz_target.ml

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

lib/bap_systemz/bap_systemz_target.mli

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

lib/bap_types/bap_arch.ml

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

lib/bap_types/bap_ir.ml

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

lib/bap_types/bap_ir.mli

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

lib/bap_types/bap_stmt.ml

@@ -110,6 +110,6 @@ let persistent = Knowledge.Persistent.of_binable (module struct
   end)
 
 let slot = Knowledge.Class.property ~package:"bap"
-    ~persistent Theory.Program.Semantics.cls "bil" domain
+    ~persistent Theory.Semantics.cls "bil" domain
     ~public:true
     ~desc:"semantics of statements in BIL"

lib/bap_types/bap_stmt.mli

@@ -26,6 +26,6 @@ end
 module Stmts_pp : Printable.S with type t = stmt list
 module Stmts_data : Data.S with type t = stmt list
 
-val slot : (Theory.Program.Semantics.cls, stmt list) Knowledge.slot
+val slot : (Theory.Semantics.cls, stmt list) Knowledge.slot
 val domain : stmt list Knowledge.domain
 val persistent : stmt list Knowledge.persistent

lib/x86_cpu/x86_target.ml

@@ -186,7 +186,7 @@ let i686 = Theory.Target.declare ~package "i686"
 let amd64 = Theory.Target.declare ~package "amd64"
     ~parent:i686
     ~nicknames:["x64"; "x86_64"; "x86-64"; ]
-    ~bits:32
+    ~bits:64
     ~data:M64.data
     ~code:M64.data
     ~vars:M64.vars

oasis/mc

@@ -9,7 +9,8 @@ Library mc_plugin
   CompiledObject:  best
   Modules:         Mc_main
   BuildDepends:    core_kernel, bap-main, bap, regular, bap-plugins,
-                   bap-core-theory, bap-knowledge, ppx_jane, bitvec
+                   bap-core-theory, bap-knowledge, ppx_jane, bitvec,
+                   ogre
   XMETAExtraLines: tags="command, disassemble"
 
 

oasis/systemz

@@ -0,0 +1,22 @@
+Flag systemz
+ Description: Build Systemz lifter
+ Default: false
+
+Library "bap-systemz"
+ Build$:           flag(everything) || flag(systemz)
+ XMETADescription: common definitions for Systemz targets
+ Path: lib/bap_systemz
+ BuildDepends: core_kernel, bap-knowledge, bap-core-theory
+ FindlibName: bap-systemz
+ Modules: Bap_systemz_target
+
+Library systemz_plugin
+  XMETADescription: provide Systemz lifter
+  Path:             plugins/systemz
+  Build$:           flag(everything) || flag(systemz)
+  BuildDepends:     core_kernel, ppx_jane, ogre,
+                    bap-core-theory, bap-knowledge, bap-main,
+                    bap, bap-systemz
+  FindlibName:      bap-plugin-systemz
+  InternalModules:  Systemz_main, Systemz_lifter
+  XMETAExtraLines:  tags="systemz, lifter, z9"

plugins/bil/bil_lifter.ml

@@ -479,7 +479,8 @@ let provide_lifter ~enable_intrinsics ~with_fp () =
     Knowledge.collect Memory.slot obj >>? fun mem ->
     Knowledge.collect Disasm_expert.Basic.Insn.slot obj >>? fun insn ->
     match lift ~enable_intrinsics arch mem insn with
-    | Error _ ->
+    | Error err ->
+      info "BIL: the BIL lifter failed with %a" Error.pp err;
       Knowledge.return (Insn.of_basic insn)
     | Ok bil ->
       Bil_semantics.context >>= fun ctxt ->