Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

implements pcode floating-point and special operators #1452

Merged
merged 1 commit into from
Mar 24, 2022

Conversation

ivg
Copy link
Member

@ivg ivg commented Mar 23, 2022

Adds an intrinsic and symbol-concat primitives to Primus Lisp and uses them to implement all floating-point operators in pcode and cpuid routines for pcode-x86.

Also rewrites the subinstruction contraction procedure, which was broken. The new version is more aggressive and contracts all contractable subinstructions.

Another minor fix: fixes the pretty-printing for the attributes parsing error.

Below is the demonstration how intrinsic are reified into BIR code with the ucomisd instruction as an example,

$ bap mc --show-insn=asm --show-bir --x86-backend=ghidra -- 66 0f 2e 05 e6 02 00 00 
UCOMISD XMM0, qword ptr [0x2ee]
0000007d:
0000006c: intrinsic:x0 := extract:63:0[YMM0]
0000006e: call @intrinsic:is_fnan_ieee754_binary with return %00000070
00000070:
00000071: u98944 := intrinsic:y0
0000005e: intrinsic:x0 := mem[0x2EE, el]:u64
00000061: call @intrinsic:is_fnan_ieee754_binary with return %00000063
00000063:
00000064: u99072 := intrinsic:y0
00000057: PF := extract:7:0[u98944] | extract:7:0[u99072]
00000047: intrinsic:x0 := extract:63:0[YMM0]
0000004a: intrinsic:x1 := mem[0x2EE, el]:u64
0000004c: call @intrinsic:forder_ieee754_binary with return %0000004e
0000004e:
0000004f: u99328 := intrinsic:y0 = 0
0000003f: ZF := extract:7:0[PF] | extract:7:0[u99328]
0000002e: intrinsic:x0 := extract:63:0[YMM0]
00000031: intrinsic:x1 := mem[0x2EE, el]:u64
00000034: call @intrinsic:forder_ieee754_binary with return %00000036
00000036:
00000037: u99584 := high:1[intrinsic:y0]
00000026: CF := extract:7:0[PF] | extract:7:0[u99584]
00000020: OF := 0
0000001c: AF := 0
00000018: SF := 0

Adds an `intrinsic` and `symbol-concat` primitives to Primus Lisp and
uses them to implement all floating-point operators in pcode and cpuid
routines for pcode-x86.
| Result
| Writes
| Stores
| Aborts
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

note that :aborts is not yet implemented and thus not documented.

@ivg ivg merged commit d0764a5 into BinaryAnalysisPlatform:master Mar 24, 2022
@ivg ivg deleted the intrinsic-functions branch March 24, 2022 02:44
ivg added a commit that referenced this pull request Apr 21, 2022
…instructions (#1458)

* Add some bitvector functions and assert-msg macro

* Add immediate decoding and logical immediate insns

* Add barrier instructions via the special primitive

* add MADD, MSUB, SDIV, UDIV and conditional select

* Fix zeros and ones bitvector constructors

* organise instructions into categories

* move ADRP to integer arithmetic category

* remove private access from arm-bits functions

* Added stur instructions and fixed bug in `condition-holds` macro

* Bug fixes for STUR insns

* condense repeated definitions into macros

* implement TBZ and TBNZ

* separated into files

* rename aarch64 files and make aarch64-helper

* add some processor state instructions
LLVM can't seem to disassemble ARMv8.4 instructions like RMIF, SETF8
and SETF16. Also, CFINV gets turned into MSR (register) but LLVM
returns ill-formed asm...?
I've commented this in aarch64-pstate.lisp.

* fix typo in pstate instructions
i typed is_zero with underscore instead of primitive is-zero

* implement rotate-left

* add missing documentation and rename for clarity
documentation added for macros and helper functions.

* apply upstream changes from #1454

* implement CAS and friends for X registers
llvm mnemonics most likely incorrect, will investigate
why bap's llvm doesn't disassemble these insns

* correct CAS mnemonic and code
i've used ` bap mc --cpu=cortex-a55 --triple=aarch64`
to get the llvm mnemonic, but will need to talk to ivan
about lisp context and
specifying generic armv8.x instead of a specific cpu

* fix typos in CAS instruction code

* fix CFINV, RMIF, SETF8 and SETF16 using #1461

* use clz instead of loop for highest-set-bit

* miscellaneous changes to helper functions

* update barrier code to use symbol-concat (#1452)

* fix CAS and friends for X registers

* generalise CAS to W or X registers

* generalise CAS and friends to 8-bit and 16-bit

* rename CAS parameter names

* fixes the cast-signed Primus Lisp primitive

* fixes the arithmetic modulus in Primus Lisp primitives

The Primus Lisp semantic primitives were hardcoding 64-bit
arithmetic, which was obviously incorrect. In addition, the
shifting operations were coercing the operands to the same size,
like in arithmetic operations, which contradicts the established
semantics of shifts both in Core Theory and in BIL. Now, the shifting
operators will produce values of the same sort as the sort of the
first operand.

* adds arbitrary-precision loopless clz and popcount in Primus Lisp

* uses clz instead of clz64 and properly casts the operand

* use fixed cast-signed primitive from #1462

* fix bitmask decoding of W registers
the result in decode-bit-masks should only be
replicated to the width of the registers being assigned to.
so, we need to pass in the register width when decoding.

Co-authored-by: Tom Malcolm <ThomasMalcolm01@gmail.com>
Co-authored-by: Tom <52238845+Thomas-Malcolm@users.noreply.github.com>
Co-authored-by: ivg <ivg@ieee.org>
kit-ty-kate pushed a commit to ocaml/opam-repository that referenced this pull request Jul 14, 2022
2.5.0
=====

- BinaryAnalysisPlatform/bap#1390 adds the flattening pass to the library interface
- BinaryAnalysisPlatform/bap#1389 adds `insn-code` to the `Theory.Semantics` class
- BinaryAnalysisPlatform/bap#1394 adds the `Bitvec.modular` function
- BinaryAnalysisPlatform/bap#1395 adds LLVM 13/14 compatibility
- BinaryAnalysisPlatform/bap#1408 adds support for mips64el target
- BinaryAnalysisPlatform/bap#1409 adds the `--print-missing` option to print unlifed instructions
- BinaryAnalysisPlatform/bap#1410 adds several new Primus Lisp primitives and new instructions
- BinaryAnalysisPlatform/bap#1428 adds the monad choice interface to the knowledge base
- BinaryAnalysisPlatform/bap#1429 refines the `Theory.Target.matches` and adds the `matching` function
- BinaryAnalysisPlatform/bap#1434 adds arm unpredicated BL instruction
- BinaryAnalysisPlatform/bap#1444 adds the x86/amd64 plt corrector component to the Primus base system
- BinaryAnalysisPlatform/bap#1445 updates the `Sub.compute_liveness` function to handle SSA form
- BinaryAnalysisPlatform/bap#1446 provides the new liveness analysis
- BinaryAnalysisPlatform/bap#1452 implements pcode floating-point and special operators
- BinaryAnalysisPlatform/bap#1457 adds optional `join` for `Knowledge.Domain.mapping`
- BinaryAnalysisPlatform/bap#1461 enables v8.{1,2,3,4,5,6}a revisions for the aarch64 target
- BinaryAnalysisPlatform/bap#1464 adds arbitrary-precision loopless clz and popcount to Primus Lisp
- BinaryAnalysisPlatform/bap#1460 adds compatibility with Core_kernel >= 0.15
- BinaryAnalysisPlatform/bap#1466 adds semantics for the x86 SSE floating-point instructions
- BinaryAnalysisPlatform/bap#1469 adds the jump destination addresses/names to the assembly output
- BinaryAnalysisPlatform/bap#1458 adds more aarch64 instructions
- BinaryAnalysisPlatform/bap#1473 adds an `--arm-features` command-line option
- BinaryAnalysisPlatform/bap#1476 implements the naming scheme for interrupts
- BinaryAnalysisPlatform/bap#1479 reifies external subroutines and intrinsics into I
- BinaryAnalysisPlatform/bap#1482 enables BIR subroutines without an explicit return
- BinaryAnalysisPlatform/bap#1481 enables disabling the patterns plugin
- BinaryAnalysisPlatform/bap#1483 implements floating-point intrinsic subroutines
- BinaryAnalysisPlatform/bap#1488 adds compatibility with OCaml 4.14 and Core v0.15
- BinaryAnalysisPlatform/bap#1489 adds some missing functionality to Primus Lisp POSIX
- BinaryAnalysisPlatform/bap#1490 adds some missing C POSIX APIs
- BinaryAnalysisPlatform/bap#1492 makes bit-twiddling operations easier to read and analyze
- BinaryAnalysisPlatform/bap#1493 adds smart constructors and destructors to the C types library
- BinaryAnalysisPlatform/bap#1491 adds semantics for the x86-64 `popq` instruction
- BinaryAnalysisPlatform/bap#1497 extends the C.Abi library
- BinaryAnalysisPlatform/bap#1498 adds the extended lvalue assignment to Primus Interpreter
- BinaryAnalysisPlatform/bap#1499 makes BIL smart constructors smart
- BinaryAnalysisPlatform/bap#1500 makes argument passing well-typed
- BinaryAnalysisPlatform/bap#1503 reimplements C types printing functions
- BinaryAnalysisPlatform/bap#1504 extends the demanglers library to the new targets infrastructure
- BinaryAnalysisPlatform/bap#1505 rewrites x86 abi using the new infrastructure
- BinaryAnalysisPlatform/bap#1511 implements some missing Thumb instructions
- BinaryAnalysisPlatform/bap#1513 implements the x86_64 padd instructions
- BinaryAnalysisPlatform/bap#1515 allows target overriding
- BinaryAnalysisPlatform/bap#1516 adds armv8 BFM instructions
- BinaryAnalysisPlatform/bap#1517 publishes Theory.Target.nicknames and extends Primus Contexts
- BinaryAnalysisPlatform/bap#1519 extends Core Theory with target registration and lookup
- BinaryAnalysisPlatform/bap#1520 adds the high-level calling convention specification language
- BinaryAnalysisPlatform/bap#1521 reimplements x86 targets using the new infrastructure
- BinaryAnalysisPlatform/bap#1522 reimplements ARM ABI and target specification
- BinaryAnalysisPlatform/bap#1523 rewrites mips targets and abi
- BinaryAnalysisPlatform/bap#1524 adds C data type layout
- BinaryAnalysisPlatform/bap#1525 adds the pass by reference argument passing method
- BinaryAnalysisPlatform/bap#1526 restructures powerpc targets and reimplements ppc32 eabi
- BinaryAnalysisPlatform/bap#1529 makes the ABI processors usable programmatically

- BinaryAnalysisPlatform/bap#1391 fixes ARM/Thumb `movt` semantics
- BinaryAnalysisPlatform/bap#1396 fixes the path plugin loader path handling
- BinaryAnalysisPlatform/bap#1414 fixes the pc value in pc-relative thumb ldr
- BinaryAnalysisPlatform/bap#1420 fixes the low-level Disasm_expert.Basic.create function
- BinaryAnalysisPlatform/bap#1421 fixes the core-theory plugin semantics tags
- BinaryAnalysisPlatform/bap#1426 fixes arm predication
- BinaryAnalysisPlatform/bap#1438 reads correctly unqualified system names
- BinaryAnalysisPlatform/bap#1439 fixes a bug in the KB update function, adds new functions
- BinaryAnalysisPlatform/bap#1448 fixes an accidental dependency on the bap-traces internal module
- BinaryAnalysisPlatform/bap#1449 fixes unconditional pop with return in thumb
- BinaryAnalysisPlatform/bap#1455 fixes register assignments in p-code semantics
- BinaryAnalysisPlatform/bap#1462 fixes the `cast-signed` Primus Lisp primitive
- BinaryAnalysisPlatform/bap#1463 fixes the arithmetic modulus in Primus Lisp primitives
- BinaryAnalysisPlatform/bap#1465 fixes handling of `jmp term`s in the flatten pass
- BinaryAnalysisPlatform/bap#1467 fixes a sporadic internal error in the cache garbage collector
- BinaryAnalysisPlatform/bap#1468 fixes the relocation symbolizer incorrect handling of intrinsics
- BinaryAnalysisPlatform/bap#1458 fixes aarch64 bitmask immediate encoding
- BinaryAnalysisPlatform/bap#1486 fixes type unification on binary operation application
- BinaryAnalysisPlatform/bap#1485 fixes little-endian MIPS disassembling
- BinaryAnalysisPlatform/bap#1494 fixes the encoding of the comparison operators
- BinaryAnalysisPlatform/bap#1496 fixes registers allocation in the abi specification DSL
- BinaryAnalysisPlatform/bap#1502 fixes the bitvector order function
- BinaryAnalysisPlatform/bap#1528 fixes armv4t name that was missing the arm prefix

- BinaryAnalysisPlatform/bap#1393 improves the Primus Lisp documentation generator
- BinaryAnalysisPlatform/bap#1397 fixes the macOS CI build
- BinaryAnalysisPlatform/bap#1399 updates the url of the testing repo to use the encrypted version
- BinaryAnalysisPlatform/bap#1432 updates the docker image
- BinaryAnalysisPlatform/bap#1435 selects specific llvm components for linking
- BinaryAnalysisPlatform/bap#1447 updates to the git+https in the dockerfiles
- BinaryAnalysisPlatform/bap#1470 corrects linking of Unix library in configure
- BinaryAnalysisPlatform/bap#1478 fixes the opam/opam dev-repo protocol which broke the release action
- BinaryAnalysisPlatform/bap#1480 adds an automation to build a docker image for the latest release
- BinaryAnalysisPlatform/bap#1514 adds the mmap dependency

- BinaryAnalysisPlatform/bap#1386 adds missing ARM target ABI information
- BinaryAnalysisPlatform/bap#1388 adds aliasing information for x86
- BinaryAnalysisPlatform/bap#1392 adds an option to directly use ogre files as a loader
- BinaryAnalysisPlatform/bap#1398 provides the assembly string as a promise (removes #undefined)
- BinaryAnalysisPlatform/bap#1400 improves the computation of the instruction properties
- BinaryAnalysisPlatform/bap#1401 improves the KB.Value merge operation
- BinaryAnalysisPlatform/bap#1402 moves promises and theories into the core-theory plugin
- BinaryAnalysisPlatform/bap#1403 moves knowledge base rules from the library to the plugin
- BinaryAnalysisPlatform/bap#1404 improves the peformance of the byte patterns matcher (1/3)
- BinaryAnalysisPlatform/bap#1405 improves the performance of bitvectors (2/3)
- BinaryAnalysisPlatform/bap#1411 [optimization] do not store empty objects in the knowledge base
- BinaryAnalysisPlatform/bap#1412 updates the KB version number and adds a few more microoptimizations
- BinaryAnalysisPlatform/bap#1413 updates bap to latest OCaml, switches to newer bitstrings
- BinaryAnalysisPlatform/bap#1415 switches to patricia trees in the KB implementation
- BinaryAnalysisPlatform/bap#1416 Reimplements x86 bitscan and popcnt
- BinaryAnalysisPlatform/bap#1418 uses the builtin clz function from base, instead of the custom one
- BinaryAnalysisPlatform/bap#1417 relaxes the speculative disassembler constraints
- BinaryAnalysisPlatform/bap#1419 allows bapbuild to work when bap and other defaults are not present
- BinaryAnalysisPlatform/bap#1422 relaxes interpreters to allow ill-typed operations
- BinaryAnalysisPlatform/bap#1425 applies ARM modified immediate (MIC) decoding in more places
- BinaryAnalysisPlatform/bap#1423 reimplements clz using the branchless/loopless algorithm
- BinaryAnalysisPlatform/bap#1427 removes unnecessary units from the knowledge base
- BinaryAnalysisPlatform/bap#1430 refines and extends target definitions
- BinaryAnalysisPlatform/bap#1431 partially upgrades byteweight to work with the modern bap
- BinaryAnalysisPlatform/bap#1441 uses Allen's Interval Algebra in the KB.Value merge implementation
- BinaryAnalysisPlatform/bap#1442 wraps proposals into with_empty and adds more guards
- BinaryAnalysisPlatform/bap#1443 adds subinstruction contraction to improve the ghidra lifter output
- BinaryAnalysisPlatform/bap#1433 adds mode events to traces
- BinaryAnalysisPlatform/bap#1450 hushes bil lifters
- BinaryAnalysisPlatform/bap#1451 removes falls-through from unconditional branches in IR reification
- BinaryAnalysisPlatform/bap#1454 improves the setw function used
- BinaryAnalysisPlatform/bap#1456 removes Thumb2 branches from the legacy ARM lifter
- BinaryAnalysisPlatform/bap#1471 uses function starts as the entires when building the symtab
- BinaryAnalysisPlatform/bap#1472 improves disassembler performance
- BinaryAnalysisPlatform/bap#1475 unifies name generation for IR subroutines
- BinaryAnalysisPlatform/bap#1477 removes the special Primus Lisp primitive
- BinaryAnalysisPlatform/bap#1484 disables byteweight
- BinaryAnalysisPlatform/bap#1487 reduces memory footprint
- BinaryAnalysisPlatform/bap#1501 makes all C data type sizes a multitude of their alignment
- BinaryAnalysisPlatform/bap#1506 optimizes encoding computation for x86
- BinaryAnalysisPlatform/bap#1510 adds an example on how to create a monad transformer stack (#1354)
- BinaryAnalysisPlatform/bap#1518 uses signed casts for promoting arguments
- BinaryAnalysisPlatform/bap#1530 turns x86 endbr instructions into nops
- BinaryAnalysisPlatform/bap#1531 adds patterns to recognize certain x86 endbr as function starts
- BinaryAnalysisPlatform/bap#1532 improves the main subroutine discovery within glibc runtime
- BinaryAnalysisPlatform/bap#1535 prevents knowledge conflicts on mangled names
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant