adds armv8 (aarch64) lifter

Makefile

@@ -55,7 +55,7 @@ testsuite:
 	git clone https://github.com/BinaryAnalysisPlatform/bap-testsuite.git testsuite
 
 check: testsuite
-	make REVISION=eaa6b5e -C testsuite
+	make REVISION=3720beda -C testsuite
 
 .PHONY: indent check-style status-clean
 

lib/arm/arm_target.ml

@@ -76,10 +76,13 @@ let vfp3regs = Theory.Role.Register.[
 
 let vars32_fp = vars32 @ untyped @@ array r64 "D" 16
 
-let gp64 = array r64 "X" 30
+let gp64 = array r64 "X" 29
 let fp64 = array r128 "Q" 32
-let sp64 = [reg r64 "SP"]
-let lr64 = [reg r64 "LR"]
+let fp64 = reg r64 "FP"       (* X29 *)
+let lr64 = reg r64 "LR"       (* X30 *)
+let sp64 = reg r64 "SP"       (* X31 *)
+let zr64 = reg r64 "XZR"
+let zr32 = reg r32 "WZR"
 let mems64 = CT.Mem.define r64 r8
 let data64 = CT.Var.define mems64 "mem"
 let flags64 = [
@@ -89,13 +92,18 @@ let flags64 = [
   reg bool "VF";
 ]
 
-let vars64 = gp64 @< fp64 @< sp64 @< lr64 @< flags64 @< [data64]
+let vars64 = gp64 @< [fp64; sp64; lr64] @< flags64 @< [data64]
 
 let regs64 = Theory.Role.Register.[
-    [general; integer], gp64 @< sp64 @< lr64;
-    [general; floating], untyped fp64;
-    [stack_pointer], untyped sp64;
-    [link], untyped lr64;
+    [general; integer], gp64 @< [fp64; lr64; sp64];
+    [general; floating], untyped [fp64];
+    [stack_pointer], untyped [sp64];
+    [frame_pointer], untyped [fp64];
+    [function_argument], array r64 "X" 8 @< array r64 "Q" 8;
+    [function_return], [reg r64 "X0"] @< [reg r128 "Q0"];
+    [constant; zero; pseudo], [zr64] @< [zr32];
+    [pseudo], array r32 "W" 31 @< [reg r32 "WSP"];
+    [link], untyped [lr64];
   ] @ status_regs
 
 
@@ -375,7 +383,7 @@ let enable_arch () =
 
 let llvm_a32 = CT.Language.declare ~package "llvm-A32"
 let llvm_t32 = CT.Language.declare ~package "llvm-T32"
-let llvm_a64 = CT.Language.declare ~package "llvm-A64"
+let llvm_a64 = CT.Language.declare ~package "llvm-aarch64"
 
 module Dis = Disasm_expert.Basic
 

lib/bap/bap_project.ml

@@ -44,21 +44,17 @@ let with_filename spec target code memory path =
   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 code addr then
-        Theory.Unit.for_file path >>= fun unit ->
-        KB.sequence [
-          KB.provide Image.Spec.slot unit spec;
-          KB.provide Theory.Unit.bias unit bias;
-          KB.provide Theory.Unit.target unit target;
-          KB.provide Image.Spec.slot unit spec;
-          KB.provide Theory.Unit.path unit (Some path);
-          KB.provide memory_slot unit memory;
-        ] >>| fun () ->
-        Some unit
-      else KB.return None)
+  KB.promising Theory.Label.unit ~promise:(fun _ ->
+      Theory.Unit.for_file path >>= fun unit ->
+      KB.sequence [
+        KB.provide Image.Spec.slot unit spec;
+        KB.provide Theory.Unit.bias unit bias;
+        KB.provide Theory.Unit.target unit target;
+        KB.provide Image.Spec.slot unit spec;
+        KB.provide Theory.Unit.path unit (Some path);
+        KB.provide memory_slot unit memory;
+      ] >>| fun () ->
+      Some unit)
 
 
 module State = struct

lib/bap_c/bap_c_abi.ml

@@ -311,6 +311,8 @@ module Arg = struct
 
     let bits self = self.bits
 
+    let deplet self = {self with args = Map.empty (module Int)}
+
     let pop self = match Map.min_elt self.args with
       | None -> None
       | Some (k,x) ->
@@ -434,7 +436,7 @@ module Arg = struct
         Arg.return res
     let pop s n = update s n File.pop
     let popn ~n s a = update s a (File.popn n)
-
+    let deplet s n = update s n @@ fun s -> Some (File.deplet s,())
   end
 
   let size s t = match s.ruler#bits t with
@@ -492,6 +494,10 @@ module Arg = struct
     let* s = Arg.get () in
     Arena.popn ~n:2 s file >>| ignore
 
+  let deplet file =
+    let* s = Arg.get () in
+    Arena.deplet s file
+
   let switch where = Arg.update @@ fun s -> {s with where}
   let where = Arg.gets @@ fun s -> s.where
 

lib/bap_c/bap_c_abi.mli

@@ -286,6 +286,12 @@ module Arg : sig
   *)
   val align_even : arena -> unit t
 
+  (** [deplet arena] unconditionally consumes all registers in arena.
+
+      The computation is never rejected.
+  *)
+  val deplet : arena -> unit t
+
   (** [reference arena t] passes the argument of type [t] as a pointer
       to [t] via the first available register in [arena].
 

lib/bap_core_theory/bap_core_theory.mli

@@ -1574,6 +1574,12 @@ module Theory : sig
     *)
     val var : t -> string -> unit Var.t option
 
+
+    (** [has_roles t roles v] is true if [v] has all the [roles] in [t].
+
+        @since 2.3.0 *)
+    val has_roles : t -> role list -> 'a Var.t -> bool
+
     (** [endianness target] describes the byte order.
 
         Describes how multibyte words are stored in the main memory. *)

lib/bap_core_theory/bap_core_theory_target.ml

@@ -252,6 +252,10 @@ let is_included roles info = match roles with
   | Some included ->
     fun var -> List.for_all included ~f:(has_role info.regs var)
 
+let has_roles t roles var =
+  let {regs} = info t and var = Var.forget var in
+  List.for_all roles ~f:(has_role regs var)
+
 let regs ?exclude ?roles t =
   let info = info t in
   let pred = match exclude,roles with

lib/bap_core_theory/bap_core_theory_target.mli

@@ -64,6 +64,7 @@ val regs :
   ?roles:role list ->
   t -> Set.M(Var.Top).t
 val reg : ?exclude:role list -> ?unique:bool -> t -> role -> unit Var.t option
+val has_roles : t -> role list -> _ Var.t -> bool
 val endianness : t -> endianness
 val system : t -> system
 val abi : t -> abi

lib/bap_mips/bap_mips_target.ml

@@ -64,6 +64,7 @@ let define ?(parent=parent) bits endianness =
     ~regs:Theory.Role.Register.[
         [general; integer], regs gpr_names;
         [general; floating], untyped fprs;
+        [constant; zero; pseudo], regs ["ZERO"];
         [stack_pointer], regs ["SP"];
         [frame_pointer], regs ["FP"];
         [link], regs ["RA"];