fixes and improves aarch64 lifter (#1351)

1) adds proper aarch64 language ids for the ghidra backend
2) adds about 20 more instructions
3) dealiases R31 and ZR, WZR, and XZR
4) adds the full set of tests (that use symbolic executor)
5) fixes instructions with 32-bit operands, the new `setw` macro
   now correctly zeros the uppert 32 bits.

Also some number of quality of life changes:

1) `--primus-lisp-semantics` now fails with a clear message when the
passed argument doesn't name a folder (previously it was silently
ignoring it).

2) moves arm-wide operations to `arm-bits`

3) allows to repeat of the `--primus-lisp-load` parameter, to make it
easier to use it in scripts and recipes.

Author: ivg

Makefile

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

lib/arm/arm_target.ml

@@ -105,7 +105,7 @@ let (.$()) = List.nth_exn
 
 let aliases =
   xs @< ws @< qs @< ds @< ss @< hs @< bs
-  @<[fp64; lr64; sp64; zr; zr64]
+  @<[fp64; lr64; sp64; zr64]
   @<[sp32; zr32]
 
 let varsv8 = rs @< flagsv8 @< [datav8]
@@ -137,7 +137,6 @@ let aliasing = Theory.Alias.[
       def lr64 [reg xs.$(30)];
       def sp64 [reg xs.$(31)];
       def sp64 [unk; reg sp32];
-      def zr [reg xs.$(31)];
       def zr [reg zr64];
       def zr [unk; reg zr32];
     ];
@@ -153,10 +152,6 @@ let aliasing = Theory.Alias.[
 
 let parent = CT.Target.declare ~package "arm"
 
-module type v4 = sig
-end
-
-
 module type ARM = sig
   val endianness : CT.endianness
   val parent : CT.Target.t
@@ -511,9 +506,8 @@ let is_little t = Theory.Target.endianness t = Theory.Endianness.le
 let register_pcode () =
   Dis.register pcode @@ fun t ->
   let triple = match is_64bit t,is_little t,is_big t with
-    | true,true,_ -> "ARM:LE:32:v8"
-    | true,_,true -> "ARM:BE:32:v8"
-    | true,_,_    -> "ARM:LEBE:32:v8LEInstruction"
+    | true,true,_ -> "AARCH64:LE:64:v8A"
+    | true,_,_ -> "AARCH64:BE:64:v8A"
     | false,true,_ -> "ARM:LE:32:v7"
     | false,_,true -> "ARM:BE:32:v7"
     | false,_,_    -> "ARM:LEBE:32:v7LEInstruction" in

plugins/arm/semantics/aarch64.lisp

@@ -1,7 +1,8 @@
+(declare (context (target arm armv8-a+le)))
+
 (require bits)
 (require arm-bits)
 
-(declare (context (target armv8-a+le)))
 (defpackage aarch64 (:use core target arm))
 (defpackage llvm-aarch64 (:use aarch64))
 
@@ -13,7 +14,17 @@
   (set$ dst (lshift imm pos)))
 
 (defun MOVZWi (dst imm pos)
-  (set$ dst (lshift imm pos)))
+  (setw dst (lshift imm pos)))
+
+(defun MOVNWi (dst imm off)
+  (setw dst (lnot (lshift imm off))))
+
+(defmacro MOVK*i (dst reg imm off)
+  (let ((mask (lnot (lshift (- (lshift 1 16) 1) off))))
+    (set$ dst (logor (logand reg mask) (lshift imm off)))))
+
+(defun MOVKWi (dst reg imm off) (MOVK*i dst reg imm off))
+(defun MOVKXi (dst reg imm off) (MOVK*i dst reg imm off))
 
 (defun ADDXri (dst src imm off)
   (set$ dst (+ src (lshift imm off))))
@@ -27,49 +38,75 @@
              (load-hword (+ base (lshift off 2))))))
 
 (defun LDRWui (dst reg off)
-  (set$ dst
+  (setw dst
         (cast-unsigned (word) (load-hword (+ reg (lshift off 2))))))
 
 (defun LDRBBui (dst reg off)
+  (setw dst
+        (cast-unsigned (word) (load-byte (+ reg off)))))
+
+(defun LDRBBroX (dst reg off _ _)
   (set$ dst
         (cast-unsigned (word) (load-byte (+ reg off)))))
 
-(defmacro make-BFM (cast xd xr ir is)
+(defmacro make-BFM (set cast xd xr ir is)
   (let ((rs (word)))
     (if (< is ir)
         (if (and (/= is (- rs 1)) (= (+ is 1) ir))
-            (set$ xd (lshift xr (- rs ir)))
-            (set$ xd (lshift
+            (set xd (lshift xr (- rs ir)))
+            (set xd (lshift
                       (cast rs (extract is 0 xr))
                       (- rs ir))))
         (if (= is (- rs 1))
-            (set$ xd (rshift xr ir))
-            (set$ xd (cast rs (extract is ir xr)))))))
+            (set xd (rshift xr ir))
+            (set xd (cast rs (extract is ir xr)))))))
 
 (defun UBFMXri (xd xr ir is)
-  (make-BFM cast-unsigned xd xr ir is))
+  (make-BFM set$ cast-unsigned xd xr ir is))
+
+(defun UBFMWri (xd xr ir is)
+  (make-BFM setw cast-unsigned xd xr ir is))
 
 (defun SBFMXri (xd xr ir is)
-  (make-BFM cast-signed xd xr ir is))
+  (make-BFM set$ cast-signed xd xr ir is))
+
+(defun SBFMWri (xd xr ir is)
+  (make-BFM setw cast-signed xd xr ir is))
 
-(defun ORRXrs (rd rn rm is)
-  (set$ rd (logor rn (shifted rm is))))
+(defmacro ORN*rs (set rd rn rm is)
+  (set rd (logor rn (lnot (lshift rm is)))))
+
+(defun ORNWrs (rd rn rm is) (ORN*rs setw rd rn rm is))
+(defun ORNXrs (rd rn rm is) (ORN*rs set$ rd rn rm is))
+
+(defmacro log*?rs (set op rd rn rm is)
+  (set rd (op rn (shifted rm is))))
+
+(defun ORRWrs (rd rn rm is) (log*?rs setw logor  rd rn rm is))
+(defun EORWrs (rd rn rm is) (log*?rs setw logxor rd rn rm is))
+(defun ANDWrs (rd rn rm is) (log*?rs setw logand rd rn rm is))
+(defun ORRXrs (rd rn rm is) (log*?rs set$ logor  rd rn rm is))
+(defun EORXrs (rd rn rm is) (log*?rs set$ logxor rd rn rm is))
+(defun ANDXrs (rd rn rm is) (log*?rs set$ logand rd rn rm is))
+
+
+(defun ANDWri (dst rn imm)
+  (setw dst (logand rn imm)))
 
-(defun ORRWrs (rd rn rm is)
-  (set$ rd
-        (logor rn
-               (shifted rm is))))
 
 (defun ADRP (dst imm)
   (set$ dst (+
              (logand (get-program-counter) (lshift -1 12))
              (cast-signed (word) (lshift imm 12)))))
 
 (defun ADDWrs (dst r1 v s)
-  (set$ dst (+ r1 (lshift v s))))
+  (setw dst (+ r1 (lshift v s))))
+
+(defun SUBWrs (dst r1 v s)
+  (setw dst (- r1 (lshift v s))))
 
 (defun ADDWri (dst r1 imm s)
-  (set$ dst (+ r1 (lshift imm s))))
+  (setw dst (+ r1 (lshift imm s))))
 
 
 (defun SUBXrx64 (rd rn rm off)
@@ -79,12 +116,12 @@
   (add-with-carry rd rn (lnot (shifted rm off)) 1))
 
 (defun SUBSWrs (rd rn rm off)
-  (add-with-carry
+  (add-with-carry/clear-base
    rd
    rn (lnot (shifted rm off)) 1))
 
 (defun SUBSWri (rd rn imm off)
-  (add-with-carry rd rn (lnot (lshift imm off)) 1))
+  (add-with-carry/clear-base rd rn (lnot (lshift imm off)) 1))
 
 
 (defun SUBSXri (rd rn imm off)
@@ -97,7 +134,7 @@
   (set$ rd (- rn (lshift imm off))))
 
 (defun SUBWri (rd rn imm off)
-  (set$ rd (- rn (lshift imm off))))
+  (setw rd (- rn (lshift imm off))))
 
 (defun ADDXrs (rd rn rm off)
   (set$ rd (+ rn (shifted rm off))))
@@ -138,6 +175,11 @@
     (store-word (+ dst off (sizeof word)) t2)
     (set$ dst (+ dst off))))
 
+(defun STPXi (t1 t2 base off)
+  (let ((off (lshift off 4)))
+    (store-word base (+ base off))
+    (store-word base (+ base off (sizeof word)))))
+
 (defun LDPXpost (dst r1 r2 base off)
   (let ((off (lshift off 3)))
     (set$ r1 (load-word base))
@@ -208,21 +250,3 @@
 (defun Bcc (cnd off)
   (when (condition-holds cnd)
     (relative-jump off)))
-
-(defun condition-holds (cnd)
-  (case cnd
-    0b0000 ZF
-    0b0001 (lnot ZF)
-    0b0010 CF
-    0b0010 (lnot CF)
-    0b0100 NF
-    0b0101 (lnot NF)
-    0b0110 VF
-    0b0111 (lnot VF)
-    0b1000 (logand CF (lnot ZF))
-    0b1001 (logor (lnot CF) ZF)
-    0b1010 (= NF VF)
-    0b1011 (/= NF VF)
-    0b1100 (logand (= NF VF) (= ZF 0))
-    0b1101 (logor (/= NF VF) (/= ZF 0))
-    true))

plugins/arm/semantics/arm-bits.lisp

@@ -11,6 +11,17 @@
     (set CF (carry r x y))
     (set$ rd r)))
 
+(defun add-with-carry/clear-base (rd x y c)
+  (let ((r (+ c y x)))
+    (set NF (msb r))
+    (set VF (overflow r x y))
+    (set ZF (is-zero r))
+    (set CF (carry r x y))
+    (clear-base rd)
+    (set$ rd r)))
+
+
+
 (defun logandnot (rd rn)
   (logand rd (lnot rn)))
 
@@ -20,3 +31,30 @@
     (set$ rd (shift r rm))
     (set ZF (is-zero rd))
     (set NF (msb rd))))
+
+(defun condition-holds (cnd)
+  (case cnd
+    0b0000 ZF
+    0b0001 (lnot ZF)
+    0b0010 CF
+    0b0010 (lnot CF)
+    0b0100 NF
+    0b0101 (lnot NF)
+    0b0110 VF
+    0b0111 (lnot VF)
+    0b1000 (logand CF (lnot ZF))
+    0b1001 (logor (lnot CF) ZF)
+    0b1010 (= NF VF)
+    0b1011 (/= NF VF)
+    0b1100 (logand (= NF VF) (lnot ZF))
+    0b1101 (logor (/= NF VF) ZF)
+    true))
+
+(defun clear-base (reg)
+  (set$ (alias-base-register reg) 0))
+
+(defmacro setw (reg val)
+  "(set Wx V) sets a Wx register clearing the upper 32 bits."
+  (let ((res val))
+    (clear-base reg)
+    (set$ reg res)))

plugins/primus_lisp/primus_lisp_main.ml

@@ -376,8 +376,8 @@ let () =
     Config.(param (list dir) ~doc:"paths to lisp libraries" "add") in
 
   let features =
-    Config.(param (list string) ~doc:"load specified module" "load"
-              ~default:["posix"]) in
+    Config.(param_all (list string) ~doc:"load specified module" "load"
+              ~default:[["posix"]]) in
 
   let semantics =
     let doc = sprintf "prepend the specified folders to the list of
@@ -413,7 +413,7 @@ let () =
       if !!enable_typecheck then
         Project.register_pass' ~deps:["api"] ~autorun:true typecheck;
       let paths = [Filename.current_dir_name] @ !!libs @ library_paths in
-      let features = "core" :: !!features in
+      let features = "core" :: List.concat !!features in
       Primus.Components.register_generic ~package:"bap" "lisp-type-checker"
         (module TypeErrorSummary)
         ~desc:"Typechecks program and outputs the summary in the standard output.";