-
Notifications
You must be signed in to change notification settings - Fork 273
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
fixes and improves label handling in the IR theory #1333
Merged
Merged
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
For the context, since the Ghidra PR the semantics of the [blk] operation in Core Theory was refined and corresponding theories were updated. Before BinaryAnalysisPlatform#1326 all theories were just ignoring the labels passed to the [blk] operator. The reason for that was that the [blk] operation serves two purposes. It enables concatenation of data and control flow effects. And it attaches a label to that sequence so that it could be referenced elsewhere. Before BinaryAnalysisPlatform#1326 it was only used for the first purpose, i.e., to merge data and control effects into the single effect. But for Ghidra we needed an ability to create labels (as ghidra is relying on Branch/Cbranch) instructions everywhere, even to express the intra-instruction logic, not real control flow. Now, the theories have to take into account the label passed to the blk operation, when they produce their denotations, unless the label is `Label.null`. If the label is `Label.null` then the operation is denotes just a sequence of data and control flow effects. Moreover, denotations are allowed to coalesce several blocks together. But if the label is non-null then the denotation has to preserve it. Before this PR the BIR theory wasn't fully respecting the passed labels and was sometimes optimizing them away, for example, when the label was attached to an empty denotation. This PR takes care of keeping the passed labels and at the same time preserving the minimal form of the generated IR. Of course assuming that lifters are using the `blk` operation correctly, i.e., that they are not passing non-null labels to blocks that they do not plan to invoke later. In other words, if you have a lifter that uses the `blk` operation you need to update it and pass `Theory.Label.null` there instead of the fresh label. This will have the same semantics as it had before. Passing non-null label now has a different semantics.
ivg
added a commit
to ivg/opam-repository
that referenced
this pull request
Dec 8, 2021
This release brings This release brings Ghidra as the new disassembler and lifting backend, significantly improves our Thumb lifter (especially with respect to interworking), adds forward-chainging rules and context variables to the knowledge base, support for LLVM 12, a pass that flattens IR, and a new framework for pattern matching on bytes that leverages the available patterns and actions from the Ghidra project. It also contains many bug fixes and improvements, most notable performance improvements that make bap from 30 to 50 per cent faster. See below for the full list of changes. Package-wise, we split bap into three parts: `bap-core`, `bap`, and `bap-extra`. The `bap-core` metapackage contains the minimal set of core packages that is necessary to disassemble the binary, the `bap` package extends this set with various analysis, finally, `bap-extra` includes rarely used or hard to install packages, such as the symbolic executor, which is very heavy on installation, and `bap-ghidra`, which is right now in a very experimental stage and is only installable on Ubuntu 18.04, since it requires the libghidra-dev package available from ppa, ``` sudo add-apt-repository ppa:ivg/ghidra -y sudo apt-get install libghidra-dev -y sudo apt-get install libghidra-data -y ``` Changelog ========= Features -------- - BinaryAnalysisPlatform/bap#1325 adds armeb abi - BinaryAnalysisPlatform/bap#1326 adds experimental Ghidra disassembler and lifting backend - BinaryAnalysisPlatform/bap#1332 adds the flatten pass - BinaryAnalysisPlatform/bap#1341 adds context variables to the knowledge base - BinaryAnalysisPlatform/bap#1343 adds register aliases to the Core Theory - BinaryAnalysisPlatform/bap#1358 adds LLVM 12 support - BinaryAnalysisPlatform/bap#1360 extends the knowledge monad interface - BinaryAnalysisPlatform/bap#1363 adds forward-chaining rules and Primus Lisp methods - BinaryAnalysisPlatform/bap#1364 adds a generic byte pattern matcher based on Ghidra - BinaryAnalysisPlatform/bap#1365 adds support for the Thumb IT blocks - BinaryAnalysisPlatform/bap#1369 adds some missing `t2LDR.-i12` instructions to the Thumb lifter Improvements ------------ - BinaryAnalysisPlatform/bap#1336 improves the `main` function discovery heuristics - BinaryAnalysisPlatform/bap#1337 adds more Primus Lisp stubs and fixes some existing - BinaryAnalysisPlatform/bap#1342 uses context variables to store the current theory - BinaryAnalysisPlatform/bap#1344 uses the context variables to store the Primus Lisp state - BinaryAnalysisPlatform/bap#1355 tweaks symbolization and function start identification facilities - BinaryAnalysisPlatform/bap#1353 improves arm-family support - BinaryAnalysisPlatform/bap#1356 stops proposing aliases as potential subroutine names - BinaryAnalysisPlatform/bap#1361 rewrites knowledge and primus monads - BinaryAnalysisPlatform/bap#1370 tweaks Primus Lisp' method resolution to keep super methods - BinaryAnalysisPlatform/bap#1375 error handling and performance tweaks - BinaryAnalysisPlatform/bap#1378 improves reification of calls in the IR theory (part I) - BinaryAnalysisPlatform/bap#1379 improves semantics of some ITT instructions - BinaryAnalysisPlatform/bap#1380 Fixes handling of fallthroughs in IR theory Bug Fixes --------- - BinaryAnalysisPlatform/bap#1328 fixes C.ABI.Args `popn` and `align_even` operators - BinaryAnalysisPlatform/bap#1329 fixes frame layout calculation in the Primus loader - BinaryAnalysisPlatform/bap#1330 fixes the address size computation in the llvm backend - BinaryAnalysisPlatform/bap#1333 fixes and improves label handling in the IR theor - BinaryAnalysisPlatform/bap#1338 fixes core:eff theory - BinaryAnalysisPlatform/bap#1340 fixes the Node.update for graphs with unlabeled nodes - BinaryAnalysisPlatform/bap#1347 fixes a knowledge base race condition in the run plugin - BinaryAnalysisPlatform/bap#1348 fixes endianness in the raw loader - BinaryAnalysisPlatform/bap#1349 short-circuits evaluation of terms in Bap_main.init - BinaryAnalysisPlatform/bap#1350 fixes variable rewriter and some Primus Lisp symbolic functions - BinaryAnalysisPlatform/bap#1351 fixes and improves aarch64 lifter - BinaryAnalysisPlatform/bap#1352 fixes several Primus Lisp stubs - BinaryAnalysisPlatform/bap#1357 fixes some T32 instructions that are accessing to PC - BinaryAnalysisPlatform/bap#1359 fixes handling of let-bound variables in flatten pass - BinaryAnalysisPlatform/bap#1366 fixes a bug in the `cmp` semantics - BinaryAnalysisPlatform/bap#1374 fixes handling modified immediate constants in ARM T32 encoding - BinaryAnalysisPlatform/bap#1376 fixes fresh variable generation - BinaryAnalysisPlatform/bap#1377 fixes the IR theory implementation Tooling ------- - BinaryAnalysisPlatform/bap#1319 fixes the shared folder in deb packages - BinaryAnalysisPlatform/bap#1320 removes sudo from postinst and postrm actions in the deb packages - BinaryAnalysisPlatform/bap#1321 enables push flag in the publish-docker-image action - BinaryAnalysisPlatform/bap#1323 fixes the ppx_bap version in the dev-repo opam file - BinaryAnalysisPlatform/bap#1331 fixes the docker publisher, also enables manual triggering - BinaryAnalysisPlatform/bap#1327 fixes a typo in the ubuntu dockerfiles - BinaryAnalysisPlatform/bap#1345 fixes bapdoc - BinaryAnalysisPlatform/bap#1346 nightly tests are failing due to a bug upstream
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.
For the context, since the Ghidra PR the semantics of the [blk]
operation in Core Theory was refined and corresponding theories were
updated. Before #1326 all theories were just ignoring the labels
passed to the [blk] operator. The reason for that was that the [blk]
operation serves two purposes. It enables concatenation of data and
control flow effects. And it attaches a label to that sequence so that
it could be referenced elsewhere. Before #1326 it was only used for
the first purpose, i.e., to merge data and control effects into the
single effect. But for Ghidra we needed an ability to create
labels (as ghidra is relying on Branch/Cbranch) instructions
everywhere, even to express the intra-instruction logic, not real
control flow.
Now, the theories have to take into account the label passed to the
blk operation, when they produce their denotations, unless the label is
Label.null
. If the label isLabel.null
then the operation isdenotes just a sequence of data and control flow effects. Moreover,
denotations are allowed to coalesce several blocks together. But if
the label is non-null then the denotation has to preserve it.
Before this PR the BIR theory wasn't fully respecting the passed
labels and was sometimes optimizing them away, for example, when the
label was attached to an empty denotation. This PR takes care of
keeping the passed labels and at the same time preserving the minimal
form of the generated IR. Of course assuming that lifters are using
the
blk
operation correctly, i.e., that they are not passingnon-null labels to blocks that they do not plan to invoke later.
In other words, if you have a lifter that uses the
blk
operation youneed to update it and pass
Theory.Label.null
there instead of thefresh label. This will have the same semantics as it had
before. Passing non-null label now has a different semantics.