Skip to content

Commit 9661d61

Browse files
ivgivg
committed
adds semantics for [v]{and[n],or,xor}p{d,s} instructions
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.
1 parent 3a7d339 commit 9661d61

File tree

6 files changed

+388
-10
lines changed

6 files changed

+388
-10
lines changed

‎README.md

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -80,6 +80,12 @@ opam switch create . --deps-only
8080
dune build && dune install
8181
```
8282
83+
Note, if you don't have the `llvm-config` executable in the path, then run
84+
```
85+
ocaml tools/configure.ml --with-llvm-config=<path-to-you-llvm-config>
86+
```
87+
where `<path-to-your-llvm-config>` is usually `llvm-config-<ver>`, e.g., `llvm-config-11`.
88+
8389
## Using
8490

8591
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:

‎plugins/primus_lisp/lisp/init.lisp

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -162,6 +162,10 @@
162162

163163
(defmacro dolist (f x xs) (prog (f x) (dolist f xs)))
164164

165+
(defun ident (x)
166+
"(ident X) is X"
167+
x)
168+
165169
(defmacro min (x)
166170
"(min X Y ...) returns the lower bound of the (X,Y,...) set"
167171
x)

‎plugins/x86/semantics/test.t

Lines changed: 228 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1317,3 +1317,231 @@ and the same for a memory operand
13171317
{
13181318
mem := mem with [RDI + 0x10, el]:u256 <- YMM0
13191319
}
1320+
1321+
[v]andp{d,s}:
1322+
$ mc 0x0f,0x54,0xca
1323+
andps %xmm2, %xmm1
1324+
{
1325+
YMM1 := high:128[YMM1].127:0[YMM1] & 127:0[YMM2]
1326+
}
1327+
$ mc 0x66,0x0f,0x54,0xca
1328+
andpd %xmm2, %xmm1
1329+
{
1330+
YMM1 := high:128[YMM1].127:0[YMM1] & 127:0[YMM2]
1331+
}
1332+
$ mc 0xc5,0xf0,0x54,0xc2
1333+
vandps %xmm2, %xmm1, %xmm0
1334+
{
1335+
YMM0 := 0.127:0[YMM1] & 127:0[YMM2]
1336+
}
1337+
$ mc 0xc5,0xf1,0x54,0xc2
1338+
vandpd %xmm2, %xmm1, %xmm0
1339+
{
1340+
YMM0 := 0.127:0[YMM1] & 127:0[YMM2]
1341+
}
1342+
$ mc 0x0f,0x54,0x4e,0x2a
1343+
andps 0x2a(%rsi), %xmm1
1344+
{
1345+
YMM1 := high:128[YMM1].127:0[YMM1] & mem[RSI + 0x2A, el]:u128
1346+
}
1347+
$ mc 0x0f,0x54,0x4e,0x2a
1348+
andps 0x2a(%rsi), %xmm1
1349+
{
1350+
YMM1 := high:128[YMM1].127:0[YMM1] & mem[RSI + 0x2A, el]:u128
1351+
}
1352+
$ mc 0x66,0x0f,0x54,0x4e,0x2a
1353+
andpd 0x2a(%rsi), %xmm1
1354+
{
1355+
YMM1 := high:128[YMM1].127:0[YMM1] & mem[RSI + 0x2A, el]:u128
1356+
}
1357+
$ mc 0xc5,0xf0,0x54,0x46,0x2a
1358+
vandps 0x2a(%rsi), %xmm1, %xmm0
1359+
{
1360+
YMM0 := 0.127:0[YMM1] & mem[RSI + 0x2A, el]:u128
1361+
}
1362+
$ mc 0xc5,0xf1,0x54,0x46,0x2a
1363+
vandpd 0x2a(%rsi), %xmm1, %xmm0
1364+
{
1365+
YMM0 := 0.127:0[YMM1] & mem[RSI + 0x2A, el]:u128
1366+
}
1367+
$ mc 0xc5,0xf4,0x54,0x46,0x2a
1368+
vandps 0x2a(%rsi), %ymm1, %ymm0
1369+
{
1370+
YMM0 := YMM1 & mem[RSI + 0x2A, el]:u256
1371+
}
1372+
$ mc 0xc5,0xf5,0x54,0x46,0x2a
1373+
vandpd 0x2a(%rsi), %ymm1, %ymm0
1374+
{
1375+
YMM0 := YMM1 & mem[RSI + 0x2A, el]:u256
1376+
}
1377+
1378+
[v]orp{d,s}:
1379+
$ mc 0x0f,0x56,0xca
1380+
orps %xmm2, %xmm1
1381+
{
1382+
YMM1 := high:128[YMM1].127:0[YMM1] | 127:0[YMM2]
1383+
}
1384+
$ mc 0x66,0x0f,0x56,0xca
1385+
orpd %xmm2, %xmm1
1386+
{
1387+
YMM1 := high:128[YMM1].127:0[YMM1] | 127:0[YMM2]
1388+
}
1389+
$ mc 0xc5,0xf0,0x56,0xc2
1390+
vorps %xmm2, %xmm1, %xmm0
1391+
{
1392+
YMM0 := 0.127:0[YMM1] | 127:0[YMM2]
1393+
}
1394+
$ mc 0xc5,0xf1,0x56,0xc2
1395+
vorpd %xmm2, %xmm1, %xmm0
1396+
{
1397+
YMM0 := 0.127:0[YMM1] | 127:0[YMM2]
1398+
}
1399+
$ mc 0x0f,0x56,0x4e,0x2a
1400+
orps 0x2a(%rsi), %xmm1
1401+
{
1402+
YMM1 := high:128[YMM1].127:0[YMM1] | mem[RSI + 0x2A, el]:u128
1403+
}
1404+
$ mc 0x0f,0x56,0x4e,0x2a
1405+
orps 0x2a(%rsi), %xmm1
1406+
{
1407+
YMM1 := high:128[YMM1].127:0[YMM1] | mem[RSI + 0x2A, el]:u128
1408+
}
1409+
$ mc 0x66,0x0f,0x56,0x4e,0x2a
1410+
orpd 0x2a(%rsi), %xmm1
1411+
{
1412+
YMM1 := high:128[YMM1].127:0[YMM1] | mem[RSI + 0x2A, el]:u128
1413+
}
1414+
$ mc 0xc5,0xf0,0x56,0x46,0x2a
1415+
vorps 0x2a(%rsi), %xmm1, %xmm0
1416+
{
1417+
YMM0 := 0.127:0[YMM1] | mem[RSI + 0x2A, el]:u128
1418+
}
1419+
$ mc 0xc5,0xf1,0x56,0x46,0x2a
1420+
vorpd 0x2a(%rsi), %xmm1, %xmm0
1421+
{
1422+
YMM0 := 0.127:0[YMM1] | mem[RSI + 0x2A, el]:u128
1423+
}
1424+
$ mc 0xc5,0xf4,0x56,0x46,0x2a
1425+
vorps 0x2a(%rsi), %ymm1, %ymm0
1426+
{
1427+
YMM0 := YMM1 | mem[RSI + 0x2A, el]:u256
1428+
}
1429+
$ mc 0xc5,0xf5,0x56,0x46,0x2a
1430+
vorpd 0x2a(%rsi), %ymm1, %ymm0
1431+
{
1432+
YMM0 := YMM1 | mem[RSI + 0x2A, el]:u256
1433+
}
1434+
1435+
[v]xorp{d,s}:
1436+
$ mc 0x0f,0x57,0xca
1437+
xorps %xmm2, %xmm1
1438+
{
1439+
YMM1 := high:128[YMM1].127:0[YMM1] ^ 127:0[YMM2]
1440+
}
1441+
$ mc 0x66,0x0f,0x57,0xca
1442+
xorpd %xmm2, %xmm1
1443+
{
1444+
YMM1 := high:128[YMM1].127:0[YMM1] ^ 127:0[YMM2]
1445+
}
1446+
$ mc 0xc5,0xf0,0x57,0xc2
1447+
vxorps %xmm2, %xmm1, %xmm0
1448+
{
1449+
YMM0 := 0.127:0[YMM1] ^ 127:0[YMM2]
1450+
}
1451+
$ mc 0xc5,0xf1,0x57,0xc2
1452+
vxorpd %xmm2, %xmm1, %xmm0
1453+
{
1454+
YMM0 := 0.127:0[YMM1] ^ 127:0[YMM2]
1455+
}
1456+
$ mc 0x0f,0x57,0x4e,0x2a
1457+
xorps 0x2a(%rsi), %xmm1
1458+
{
1459+
YMM1 := high:128[YMM1].127:0[YMM1] ^ mem[RSI + 0x2A, el]:u128
1460+
}
1461+
$ mc 0x0f,0x57,0x4e,0x2a
1462+
xorps 0x2a(%rsi), %xmm1
1463+
{
1464+
YMM1 := high:128[YMM1].127:0[YMM1] ^ mem[RSI + 0x2A, el]:u128
1465+
}
1466+
$ mc 0x66,0x0f,0x57,0x4e,0x2a
1467+
xorpd 0x2a(%rsi), %xmm1
1468+
{
1469+
YMM1 := high:128[YMM1].127:0[YMM1] ^ mem[RSI + 0x2A, el]:u128
1470+
}
1471+
$ mc 0xc5,0xf0,0x57,0x46,0x2a
1472+
vxorps 0x2a(%rsi), %xmm1, %xmm0
1473+
{
1474+
YMM0 := 0.127:0[YMM1] ^ mem[RSI + 0x2A, el]:u128
1475+
}
1476+
$ mc 0xc5,0xf1,0x57,0x46,0x2a
1477+
vxorpd 0x2a(%rsi), %xmm1, %xmm0
1478+
{
1479+
YMM0 := 0.127:0[YMM1] ^ mem[RSI + 0x2A, el]:u128
1480+
}
1481+
$ mc 0xc5,0xf4,0x57,0x46,0x2a
1482+
vxorps 0x2a(%rsi), %ymm1, %ymm0
1483+
{
1484+
YMM0 := YMM1 ^ mem[RSI + 0x2A, el]:u256
1485+
}
1486+
$ mc 0xc5,0xf5,0x57,0x46,0x2a
1487+
vxorpd 0x2a(%rsi), %ymm1, %ymm0
1488+
{
1489+
YMM0 := YMM1 ^ mem[RSI + 0x2A, el]:u256
1490+
}
1491+
1492+
[v]andnp{d,s}:
1493+
$ mc 0x0f,0x55,0xca
1494+
andnps %xmm2, %xmm1
1495+
{
1496+
YMM1 := high:128[YMM1].~(127:0[YMM1] & 127:0[YMM2])
1497+
}
1498+
$ mc 0x66,0x0f,0x55,0xca
1499+
andnpd %xmm2, %xmm1
1500+
{
1501+
YMM1 := high:128[YMM1].~(127:0[YMM1] & 127:0[YMM2])
1502+
}
1503+
$ mc 0xc5,0xf0,0x55,0xc2
1504+
vandnps %xmm2, %xmm1, %xmm0
1505+
{
1506+
YMM0 := 0.~(127:0[YMM1] & 127:0[YMM2])
1507+
}
1508+
$ mc 0xc5,0xf1,0x55,0xc2
1509+
vandnpd %xmm2, %xmm1, %xmm0
1510+
{
1511+
YMM0 := 0.~(127:0[YMM1] & 127:0[YMM2])
1512+
}
1513+
$ mc 0x0f,0x55,0x4e,0x2a
1514+
andnps 0x2a(%rsi), %xmm1
1515+
{
1516+
YMM1 := high:128[YMM1].~(127:0[YMM1] & mem[RSI + 0x2A, el]:u128)
1517+
}
1518+
$ mc 0x0f,0x55,0x4e,0x2a
1519+
andnps 0x2a(%rsi), %xmm1
1520+
{
1521+
YMM1 := high:128[YMM1].~(127:0[YMM1] & mem[RSI + 0x2A, el]:u128)
1522+
}
1523+
$ mc 0x66,0x0f,0x55,0x4e,0x2a
1524+
andnpd 0x2a(%rsi), %xmm1
1525+
{
1526+
YMM1 := high:128[YMM1].~(127:0[YMM1] & mem[RSI + 0x2A, el]:u128)
1527+
}
1528+
$ mc 0xc5,0xf0,0x55,0x46,0x2a
1529+
vandnps 0x2a(%rsi), %xmm1, %xmm0
1530+
{
1531+
YMM0 := 0.~(127:0[YMM1] & mem[RSI + 0x2A, el]:u128)
1532+
}
1533+
$ mc 0xc5,0xf1,0x55,0x46,0x2a
1534+
vandnpd 0x2a(%rsi), %xmm1, %xmm0
1535+
{
1536+
YMM0 := 0.~(127:0[YMM1] & mem[RSI + 0x2A, el]:u128)
1537+
}
1538+
$ mc 0xc5,0xf4,0x55,0x46,0x2a
1539+
vandnps 0x2a(%rsi), %ymm1, %ymm0
1540+
{
1541+
YMM0 := ~(YMM1 & mem[RSI + 0x2A, el]:u256)
1542+
}
1543+
$ mc 0xc5,0xf5,0x55,0x46,0x2a
1544+
vandnpd 0x2a(%rsi), %ymm1, %ymm0
1545+
{
1546+
YMM0 := ~(YMM1 & mem[RSI + 0x2A, el]:u256)
1547+
}

‎plugins/x86/semantics/x86-64-sse-intrinsics.lisp

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -175,12 +175,6 @@
175175
(defun MFENCE ()
176176
(intrinsic 'mfence))
177177

178-
(defun ANDPDrr (rd rn rm)
179-
(set-sse rd (logand rn rm)))
180-
181-
(defun ANDPDrm (rd rn ptr _ _ off _)
182-
(set-sse rd (logand rn (load-mem ptr off))))
183-
184178
(defun sse-truncate (name rt rs rn)
185179
(intrinsic
186180
(symbol-concat name 'rtz *sse-format* :sep '_)

0 commit comments

Comments
 (0)