fixes the arithmetic modulus in Primus Lisp primitives #1463
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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.
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
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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.