Skip to content

Commit

Permalink
Bump llvm-pretty{-bc-parser} submodules, adapt to ValPoison (#936)
Browse files Browse the repository at this point in the history
This bumps the `llvm-pretty` submodule to bring in the following PRs:

* GaloisInc/llvm-pretty#86 (support LLVM 11 `IsDefault` fields in metadata)
* GaloisInc/llvm-pretty#87 (Relax the Symbol requirement to `ConstBlockAddr`)
* GaloisInc/llvm-pretty#88 (add LLVM12 poison value)
* GaloisInc/llvm-pretty#90 (Support structs with bitfields in `Text.LLVM.DebugUtils`)

This also bumps the `llvm-pretty-bc-parser` submodule to bring in the
following PRs:

* GaloisInc/llvm-pretty-bc-parser#171 (don't consume fast math flag entry)
* GaloisInc/llvm-pretty-bc-parser#169 (make `getBitString` assumptions explicit)
* GaloisInc/llvm-pretty-bc-parser#168 (support for LLVM 11 `IsDefault` fields in metadata)
* GaloisInc/llvm-pretty-bc-parser#170 (remove `Aligned` from `SubWord`)
* GaloisInc/llvm-pretty-bc-parser#172 (fix BLOCKADDRESS parsing)
* GaloisInc/llvm-pretty-bc-parser#173 (parse LLVM12 poison value)
* GaloisInc/llvm-pretty-bc-parser#178 (use Seq over list in PartialModule)

Of these, the only PR that requires code changes in Crucible is
GaloisInc/llvm-pretty#88 (add LLVM12 poison value), as this adds a new
`ValPoison` constructor to `Value'`. Properly handling LLVM poison is a large
task that I do not wish to tackle here (see #366 for discussion of how one
might do this). For now, this PR does the bare minimum:

* In `Lang.Crucible.LLVM.Translation.BlockInfo.useVal`, treat `ValPoison`
  as not referencing any identifiers.
* The other two potential sites where `ValPoison` could be matched on are in
  `Lang.Crucible.LLVM.Translation.Constant.transConstant'` and
  `Lang.Crucible.LLVM.Translation.Expr.transValue`. Since we are not handling
  `ValPoison` for now, both of these functions will simply error if they
  encounter `ValPoison`.
* I have added a section to `crucible-llvm`'s `limitations.md` document which
  describes the above limitations of poison handling.
  • Loading branch information
RyanGlScott authored Dec 6, 2021
1 parent c811db8 commit acd37d5
Show file tree
Hide file tree
Showing 4 changed files with 20 additions and 2 deletions.
17 changes: 17 additions & 0 deletions crucible-llvm/doc/limitations.md
Original file line number Diff line number Diff line change
Expand Up @@ -101,3 +101,20 @@ memory yield arbitrary values. Since LLVM often passes loaded values
from uninitialized memory to `freeze` to ensure that the result is not
`undef`, this will ensure that a sizable number of use cases for
`freeze` will be handled as expected.

LLVM poison limitations
=======================
`crucible-llvm` has limited support for tracking
[poison values](https://releases.llvm.org/13.0.0/docs/LangRef.html#poisonvalues).
Certain LLVM instructions and intrinsics can return poison values under
certain circumstances, and `crucible-llvm` makes an effort to generate failing
assertions whenever such poison values are returned. For instance, LLVM's
`add` instruction can return poison if the result overflows, which
`crucible-llvm` is able to detect and simulate by throwing an appropriate
assertion failure.

There are other ways to create and propagate poison that `crucible-llvm` is
unable to track, however. There is no support for LLVM's `poison` constant
values, and `crucible-llvm` will throw an error if it encounters such a
`poison` constant. LLVM also permits values where only certain bits of the
value are poison, but `crucible-llvm` is unable to reason about this.
Original file line number Diff line number Diff line change
Expand Up @@ -284,6 +284,7 @@ useVal v = Set.unions $ case v of
L.ValLabel _ -> []
L.ValZeroInit -> []
L.ValAsm{} -> [] -- TODO! inline asm ...
L.ValPoison{} -> []

-- NB! metadata values are not considered as part of our use analysis
L.ValMd _md -> []
Expand Down
2 changes: 1 addition & 1 deletion dependencies/llvm-pretty

0 comments on commit acd37d5

Please sign in to comment.