adds semantics for [v]{and[n],or,xor}p{d,s} instructions

ivg · ivg · commit 9338ae7ac9f1 · 2025-04-17T21:00:06.000Z
These instructions apply bitwise operations on the packed data, in
total 16 instructions. Suprisingly, out of this family we already
handled the packed xor variant, but the semantics was very ineffcient
as it wasn't using the fact that all bitwise operations are
distributive over concatenation.
diff --git a/README.md b/README.md
@@ -80,6 +80,12 @@ opam switch create . --deps-only
 dune build && dune install
 ```
 
+Note, if you don't have the `llvm-config` executable in the path, then run
+```
+ocaml tools/configure.ml --with-llvm-config=<path-to-you-llvm-config>
+```
+where `<path-to-your-llvm-config>` is usually `llvm-config-<ver>`, e.g., `llvm-config-11`.
+
 ## Using
 
 BAP, like Docker or Git, is driven by a single command-line utility called [bap][man-bap]. Just type `bap` in your shell and it will print a message which shows BAP capabilities. The `disassemble` command will take a binary program, disassemble it, lift it into the intermediate architecture agnostic representation, build a control flow graph, and finally apply staged user-defined analysis in a form of disassembling passes. Finally, the `--dump` option (`-d` in short) will output the resulting program in the specified format. This is the default command, so you don't even need to specify it, e.g., the following will disassembled and dump the `/bin/echo` binary on your machine:
diff --git a/plugins/primus_lisp/lisp/init.lisp b/plugins/primus_lisp/lisp/init.lisp
@@ -162,6 +162,10 @@
 
 (defmacro dolist (f x xs) (prog (f x) (dolist f xs)))
 
+(defun ident (x)
+  "(ident X) is X"
+  x)
+
 (defmacro min (x)
   "(min X Y ...) returns the lower bound of the (X,Y,...) set"
       x)
diff --git a/plugins/x86/semantics/test.t b/plugins/x86/semantics/test.t
@@ -1317,3 +1317,231 @@ and the same for a memory operand
   {
     mem := mem with [RDI + 0x10, el]:u256 <- YMM0
   }
+
+[v]andp{d,s}:
+  $ mc 0x0f,0x54,0xca
+  andps %xmm2, %xmm1
+  {
+    YMM1 := high:128[YMM1].127:0[YMM1] & 127:0[YMM2]
+  }
+  $ mc 0x66,0x0f,0x54,0xca
+  andpd %xmm2, %xmm1
+  {
+    YMM1 := high:128[YMM1].127:0[YMM1] & 127:0[YMM2]
+  }
+  $ mc 0xc5,0xf0,0x54,0xc2
+  vandps %xmm2, %xmm1, %xmm0
+  {
+    YMM0 := 0.127:0[YMM1] & 127:0[YMM2]
+  }
+  $ mc 0xc5,0xf1,0x54,0xc2
+  vandpd %xmm2, %xmm1, %xmm0
+  {
+    YMM0 := 0.127:0[YMM1] & 127:0[YMM2]
+  }
+  $ mc 0x0f,0x54,0x4e,0x2a
+  andps 0x2a(%rsi), %xmm1
+  {
+    YMM1 := high:128[YMM1].127:0[YMM1] & mem[RSI + 0x2A, el]:u128
+  }
+  $ mc 0x0f,0x54,0x4e,0x2a
+  andps 0x2a(%rsi), %xmm1
+  {
+    YMM1 := high:128[YMM1].127:0[YMM1] & mem[RSI + 0x2A, el]:u128
+  }
+  $ mc 0x66,0x0f,0x54,0x4e,0x2a
+  andpd 0x2a(%rsi), %xmm1
+  {
+    YMM1 := high:128[YMM1].127:0[YMM1] & mem[RSI + 0x2A, el]:u128
+  }
+  $ mc 0xc5,0xf0,0x54,0x46,0x2a
+  vandps 0x2a(%rsi), %xmm1, %xmm0
+  {
+    YMM0 := 0.127:0[YMM1] & mem[RSI + 0x2A, el]:u128
+  }
+  $ mc 0xc5,0xf1,0x54,0x46,0x2a
+  vandpd 0x2a(%rsi), %xmm1, %xmm0
+  {
+    YMM0 := 0.127:0[YMM1] & mem[RSI + 0x2A, el]:u128
+  }
+  $ mc 0xc5,0xf4,0x54,0x46,0x2a
+  vandps 0x2a(%rsi), %ymm1, %ymm0
+  {
+    YMM0 := YMM1 & mem[RSI + 0x2A, el]:u256
+  }
+  $ mc 0xc5,0xf5,0x54,0x46,0x2a
+  vandpd 0x2a(%rsi), %ymm1, %ymm0
+  {
+    YMM0 := YMM1 & mem[RSI + 0x2A, el]:u256
+  }
+
+[v]orp{d,s}:
+  $ mc 0x0f,0x56,0xca
+  orps %xmm2, %xmm1
+  {
+    YMM1 := high:128[YMM1].127:0[YMM1] | 127:0[YMM2]
+  }
+  $ mc 0x66,0x0f,0x56,0xca
+  orpd %xmm2, %xmm1
+  {
+    YMM1 := high:128[YMM1].127:0[YMM1] | 127:0[YMM2]
+  }
+  $ mc 0xc5,0xf0,0x56,0xc2
+  vorps %xmm2, %xmm1, %xmm0
+  {
+    YMM0 := 0.127:0[YMM1] | 127:0[YMM2]
+  }
+  $ mc 0xc5,0xf1,0x56,0xc2
+  vorpd %xmm2, %xmm1, %xmm0
+  {
+    YMM0 := 0.127:0[YMM1] | 127:0[YMM2]
+  }
+  $ mc 0x0f,0x56,0x4e,0x2a
+  orps 0x2a(%rsi), %xmm1
+  {
+    YMM1 := high:128[YMM1].127:0[YMM1] | mem[RSI + 0x2A, el]:u128
+  }
+  $ mc 0x0f,0x56,0x4e,0x2a
+  orps 0x2a(%rsi), %xmm1
+  {
+    YMM1 := high:128[YMM1].127:0[YMM1] | mem[RSI + 0x2A, el]:u128
+  }
+  $ mc 0x66,0x0f,0x56,0x4e,0x2a
+  orpd 0x2a(%rsi), %xmm1
+  {
+    YMM1 := high:128[YMM1].127:0[YMM1] | mem[RSI + 0x2A, el]:u128
+  }
+  $ mc 0xc5,0xf0,0x56,0x46,0x2a
+  vorps 0x2a(%rsi), %xmm1, %xmm0
+  {
+    YMM0 := 0.127:0[YMM1] | mem[RSI + 0x2A, el]:u128
+  }
+  $ mc 0xc5,0xf1,0x56,0x46,0x2a
+  vorpd 0x2a(%rsi), %xmm1, %xmm0
+  {
+    YMM0 := 0.127:0[YMM1] | mem[RSI + 0x2A, el]:u128
+  }
+  $ mc 0xc5,0xf4,0x56,0x46,0x2a
+  vorps 0x2a(%rsi), %ymm1, %ymm0
+  {
+    YMM0 := YMM1 | mem[RSI + 0x2A, el]:u256
+  }
+  $ mc 0xc5,0xf5,0x56,0x46,0x2a
+  vorpd 0x2a(%rsi), %ymm1, %ymm0
+  {
+    YMM0 := YMM1 | mem[RSI + 0x2A, el]:u256
+  }
+
+[v]xorp{d,s}:
+  $ mc 0x0f,0x57,0xca
+  xorps %xmm2, %xmm1
+  {
+    YMM1 := high:128[YMM1].127:0[YMM1] ^ 127:0[YMM2]
+  }
+  $ mc 0x66,0x0f,0x57,0xca
+  xorpd %xmm2, %xmm1
+  {
+    YMM1 := high:128[YMM1].127:0[YMM1] ^ 127:0[YMM2]
+  }
+  $ mc 0xc5,0xf0,0x57,0xc2
+  vxorps %xmm2, %xmm1, %xmm0
+  {
+    YMM0 := 0.127:0[YMM1] ^ 127:0[YMM2]
+  }
+  $ mc 0xc5,0xf1,0x57,0xc2
+  vxorpd %xmm2, %xmm1, %xmm0
+  {
+    YMM0 := 0.127:0[YMM1] ^ 127:0[YMM2]
+  }
+  $ mc 0x0f,0x57,0x4e,0x2a
+  xorps 0x2a(%rsi), %xmm1
+  {
+    YMM1 := high:128[YMM1].127:0[YMM1] ^ mem[RSI + 0x2A, el]:u128
+  }
+  $ mc 0x0f,0x57,0x4e,0x2a
+  xorps 0x2a(%rsi), %xmm1
+  {
+    YMM1 := high:128[YMM1].127:0[YMM1] ^ mem[RSI + 0x2A, el]:u128
+  }
+  $ mc 0x66,0x0f,0x57,0x4e,0x2a
+  xorpd 0x2a(%rsi), %xmm1
+  {
+    YMM1 := high:128[YMM1].127:0[YMM1] ^ mem[RSI + 0x2A, el]:u128
+  }
+  $ mc 0xc5,0xf0,0x57,0x46,0x2a
+  vxorps 0x2a(%rsi), %xmm1, %xmm0
+  {
+    YMM0 := 0.127:0[YMM1] ^ mem[RSI + 0x2A, el]:u128
+  }
+  $ mc 0xc5,0xf1,0x57,0x46,0x2a
+  vxorpd 0x2a(%rsi), %xmm1, %xmm0
+  {
+    YMM0 := 0.127:0[YMM1] ^ mem[RSI + 0x2A, el]:u128
+  }
+  $ mc 0xc5,0xf4,0x57,0x46,0x2a
+  vxorps 0x2a(%rsi), %ymm1, %ymm0
+  {
+    YMM0 := YMM1 ^ mem[RSI + 0x2A, el]:u256
+  }
+  $ mc 0xc5,0xf5,0x57,0x46,0x2a
+  vxorpd 0x2a(%rsi), %ymm1, %ymm0
+  {
+    YMM0 := YMM1 ^ mem[RSI + 0x2A, el]:u256
+  }
+
+[v]andnp{d,s}:
+  $ mc 0x0f,0x55,0xca
+  andnps %xmm2, %xmm1
+  {
+    YMM1 := high:128[YMM1].~(127:0[YMM1] & 127:0[YMM2])
+  }
+  $ mc 0x66,0x0f,0x55,0xca
+  andnpd %xmm2, %xmm1
+  {
+    YMM1 := high:128[YMM1].~(127:0[YMM1] & 127:0[YMM2])
+  }
+  $ mc 0xc5,0xf0,0x55,0xc2
+  vandnps %xmm2, %xmm1, %xmm0
+  {
+    YMM0 := 0.~(127:0[YMM1] & 127:0[YMM2])
+  }
+  $ mc 0xc5,0xf1,0x55,0xc2
+  vandnpd %xmm2, %xmm1, %xmm0
+  {
+    YMM0 := 0.~(127:0[YMM1] & 127:0[YMM2])
+  }
+  $ mc 0x0f,0x55,0x4e,0x2a
+  andnps 0x2a(%rsi), %xmm1
+  {
+    YMM1 := high:128[YMM1].~(127:0[YMM1] & mem[RSI + 0x2A, el]:u128)
+  }
+  $ mc 0x0f,0x55,0x4e,0x2a
+  andnps 0x2a(%rsi), %xmm1
+  {
+    YMM1 := high:128[YMM1].~(127:0[YMM1] & mem[RSI + 0x2A, el]:u128)
+  }
+  $ mc 0x66,0x0f,0x55,0x4e,0x2a
+  andnpd 0x2a(%rsi), %xmm1
+  {
+    YMM1 := high:128[YMM1].~(127:0[YMM1] & mem[RSI + 0x2A, el]:u128)
+  }
+  $ mc 0xc5,0xf0,0x55,0x46,0x2a
+  vandnps 0x2a(%rsi), %xmm1, %xmm0
+  {
+    YMM0 := 0.~(127:0[YMM1] & mem[RSI + 0x2A, el]:u128)
+  }
+  $ mc 0xc5,0xf1,0x55,0x46,0x2a
+  vandnpd 0x2a(%rsi), %xmm1, %xmm0
+  {
+    YMM0 := 0.~(127:0[YMM1] & mem[RSI + 0x2A, el]:u128)
+  }
+  $ mc 0xc5,0xf4,0x55,0x46,0x2a
+  vandnps 0x2a(%rsi), %ymm1, %ymm0
+  {
+    YMM0 := ~(YMM1 & mem[RSI + 0x2A, el]:u256)
+  }
+  $ mc 0xc5,0xf5,0x55,0x46,0x2a
+  vandnpd 0x2a(%rsi), %ymm1, %ymm0
+  {
+    YMM0 := ~(YMM1 & mem[RSI + 0x2A, el]:u256)
+  }
diff --git a/plugins/x86/semantics/x86-64-sse-intrinsics.lisp b/plugins/x86/semantics/x86-64-sse-intrinsics.lisp
@@ -175,12 +175,6 @@
 (defun MFENCE ()
   (intrinsic 'mfence))
 
-(defun ANDPDrr (rd rn rm)
-  (set-sse rd (logand rn rm)))
-
-(defun ANDPDrm (rd rn ptr _ _ off _)
-  (set-sse rd (logand rn (load-mem ptr off))))
-
 (defun sse-truncate (name rt rs rn)
   (intrinsic
    (symbol-concat name 'rtz *sse-format* :sep '_)
diff --git a/plugins/x86/semantics/x86-64.lisp b/plugins/x86/semantics/x86-64.lisp
diff --git a/plugins/x86/x86_disasm.ml b/plugins/x86/x86_disasm.ml
