* riscv: added grift as submodule
* added macaw-riscv project
* make arch polykinded everywhere in macaw base
* stubbed out riscv_info
* update grift
* started on RISCVReg
* started on RISCVReg
* RegisterInfo instance for RISCVReg (a few unimplemented fields)
* filled out archRegSet
* filled out withArchConstraints, archAddrWidth, and archEndianness
* added Arch module
* RISCV initialBlockRegs
* preliminary work on disassembleFn
* wip: disassembleFn
* made things more lens-y
* wip: disassemble instruction
* finished disassembly of grift assignment statements
* separated out DisInstM into separate module
* disassembly wip
* finished disassembleBlock
* Finished riscvDisassembleFn
* bump grift submodule
* made macaw discovery poly-kinded
* added risc-v test suite
* added risc-v test suite
* fixed macaw semantics to hardware x0 to constant value 0
* added riscvPreserveReg based on assembler's manual
* riscvDemandContext
* successfully disassembled a block!
* enhanced tests to allow optional entry point spec
* stubbed out identifyCall
* stubbed out identifyReturn
* passing initial test
* added checkForReturnAddr stub
* fleshed out identifyCall and identifyReturn
* update grift submodule
* bug fix and exception handling
* added EXC register, which tracks whether or not we've attempted to
read from/write to any system registers.
* Replaced custom CSR type with GRIFT's (but we're not using it
currently)
* added better show instance for GPRs we should migrate this to a
GRIFT pretty printer at some point)
* Fixed a vicious bug in the semantics; unsigned and signed LT were
getting swapped in translation
* added pattern synonyms for GPRs
* improved docs and fixed RISCVReg bug (GP was 3 instead of 4)
* changed undefineds to errors
* changed RISCV class to RISCVConstraints
* wrapped GRIFT's "RV" parameter in a type to remove the need to make
macaw architecture parameter polykinded
* rolled back all changes to macaw base that made things poly-kinded
* reverted two more macaw core changes, updated license, removed old PPC test
* macaw: update to upstream changes in bv-sized and grift
* address code review comments
* macaw-riscv: expose fewer modules
* Update RISCVTermStmt definition
* Update riscv_info. macaw-riscv now builds against master
* Update bv-sized and cabal freeze files
* Update cabal freeze files with satisfying lens version
* Get tests building
* Fix printf runtime error
* Add simpler tests
* Change RISCV target version and update grift pointer
[skip ci]
* Compressed branch test passes
[skip ci]
* Add additional small tests
[skip ci]
* Introduce a syscall PrimFn
* Syscalls now correctly classified
* Fix return regs from syscall
* Extract syscall arguments
* Update expected riscv test results
* Add macaw-riscv build + test to CI
* Get building with GHC 9.0.2
* Revert "Update cabal freeze files with satisfying lens version"
This reverts commit 4aa95c19c3.
* Install softfloat in CI
* Update Grift
* Some initial cleanup
* More cleanup
* Resolve FIXME on getReg
* Detect and only accept rv64gc rvreprs
* Address Tristan's PR comments
* Update Grift pointer
* Add info on installing Softfloat to README for macaw-riscv
* Add missing submodule step to softfloat build instructions
Co-authored-by: Ben Selfridge <benselfridge@000279.local>
Co-authored-by: Valentin Robert <val@galois.com>
This contains a variety of fixes needed to make the packages in the `macaw`
repo compile with GHC 9.0:
* GHC 9.0 implements simplified subsumption (see
[here](https://gitlab.haskell.org/ghc/ghc/-/wikis/migration/9.0?version_id=5fcd0a50e0872efb3c38a32db140506da8310d87#simplified-subsumption)).
In most cases, adapting to this is a matter of manually eta expanding
definitions, such as in `base:Data.Macaw.Analysis.RegisterUse`. In the case
of `macaw-x86-symbolic:Data.Macaw.X86.Crucible`, the type signature of
`evalExt` had to be made more specific to adapt to the loss of contravariance
when typechecking `(->)`.
* GHC's constraint solver now solves constraints in each top-level group
sooner (see
[here](https://gitlab.haskell.org/ghc/ghc/-/wikis/migration/9.0?version_id=5fcd0a50e0872efb3c38a32db140506da8310d87#the-order-of-th-splices-is-more-important)).
This affects `macaw-aarch32` and `macaw-symbolic`, as they separate top-level
groups with `$(return [])` Template Haskell splices. The previous locations
of these splices made it so that the TH-generated instances in that package
were not available to any code before the splice, resulting in type errors
when compiled with GHC 9.0.
To overcome this, I rearranged the TH-generated instances so that they appear
before the top-level groups that make use of them.
* GHC 9.0 now enables `-Wstar-is-type` in `-Wall`, so this patch replaces some
uses of `*` with `Data.Kind.Type`. `Data.Kind` requires the use of GHC 8.0 or
later, so this patch also updates thes lower bounds on `base` to `>= 4.9` in
the appropriate `.cabal` files. (I'm fairly certain that this requirement was
already present implicity, but better to be explicit about it.)
* The `asl-translator`, `crucible`, and `semmc` submodules were updated to
allow them to build with GHC 9.0. The `llvm-pretty` and
`llvm-pretty-bc-parser` submodules were also bumped to accommodate unrelated
changes in `crucible` that were brought in.
* The upper version bounds on `doctest` in `macaw-symbolic`'s test suite were
raised to allow it to build with GHC 9.0.
This updates the `crucible` submodule to include GaloisInc/crucible#906
(`Control granularity of reading uninitialized memory`), as well as the
`semmc` submodule to bring in corresponding changes on its side
(GaloisInc/semmc#69). Some additional `?memOpts :: MemOptions` constraints
needed to be added to some functions in `macaw-symbolic` and
`macaw-refinement` as a result.
This updates the `llvm-pretty-bc-parser` to include these PRs:
* GaloisInc/llvm-pretty-bc-parser#159 (`Support parsing fneg instructions`)
* GaloisInc/llvm-pretty-bc-parser#166 (`Support parsing freeze instructions`)
* GaloisInc/llvm-pretty-bc-parser#164 (`Parse DebugInfoEnumerator properly on LLVM 12+`)
* GaloisInc/llvm-pretty-bc-parser#162 (`Support parsing dict{Associated,Allocated,Rank} fields introduced in LLVM 12`)
The `llvm-pretty` submodule had corresponding changes as well. These were
included as part of a previous commit to update the `llvm-pretty` submodule
(952fe5578d), but the `llvm-pretty-bc-parser`
submodule was not updated at the same time. This commit brings the two back
into harmony.
See `Note [Sign-extending immediate operands in push]` in
`Data.Macaw.X86.Semantics` for the full story. I have also added a test case
in `macaw-x86-symbolic` which ensures that the stack-pointer-decrementing
logic behaves as one would expect.
Bumps in the `flexdis86` submodule to bring in GaloisInc/flexdis86#37.
Fixes#235.
This bumps the `crucible` submodule to bring in:
* `crucible-symio` (GaloisInc/crucible#788). This requires adding a new
project dependency in `cabal.project.dist`.
* GaloisInc/crucible#808, which adds yet another `?memOpts :: MemOptions`
constraint, this time in `doPtrAddOffset`.
GaloisInc/crucible#794 increases the number of functions that use
implicit `MemOptions`, including a handful of key LLVM memory model–related
functions. As a result, many parts of `macaw` need to add implicit `?memOpts`
parameters to accommodate to this change.
None of the common default ppc32 ABIs use a Table of Contents (TOC), so default
our code to not assume it either. This has accompanying changes in
macaw-loader-ppc, which also made incorrect assumptions about ppc32.
Note that we may eventually need to support rarely-used ABIs that do use a
TOC (or similar dedicated registers, e.g., the Small Data Area mode). When we
do, we will probably want that to be a data-oriented decision rather than a
type-level one, as each architecture supports multiple ABIs. We may also need to
modify ppc64 to support ABIs without TOCs, but we'll do it when we need to.
The new test suites cover x86_64, PowerPC, and ARM. They test that the semantics are actually correct (rather than just seeing if symbolic execution produces any result). The `Data.Macaw.Symbolic.Testing` module in macaw-symbolic provides some common utilities for symbolic execution engine setup, while there are tailored test harnesses for each architecture.
The semantics of the test harnesses are documented in each architecture test suite, but they:
1. Discover all of the test binaries (which are generated from the included makefiles)
2. Treat each function whose name begins with `test_` as a test entry point
3. Symbolically executes each test case with fully symbolic register states
4. Extracts the return value after symbolic execution, which is treated as the predicate to an assertion that must be proved
- If the test case is in the `pass` subdirectory, it is proved and expected to hold
- If the test case is in the `fail` subdirectory, it is proved and expected to not hold.
Each test harness supports two options for debugging:
- Dumping generated SMT queries
- Dumping generated Macaw IR for inspection
This testing uncovered a bug in the (previously untested) macaw-aarch32-symbolic code. It required a number of submodule updates to:
- Adapt to some what4 changes
- Fix a bug in the LLVM memory model that lets these tests pass
- Adapt to changes to some crucible APIs
This change also modifies the CI configuration to install SMT solvers earlier (which are now needed for all of the symbolic package tests).
Nat is no longer a what4 base type, so we have to adapt various APIs to accommodate that. The template haskell in macaw-semmc is updated to remove Nat cases. Changes to the `SymFn` type required removing a type parameter.
This commit also adds macaw-refinement to CI (which requires installing SMT solvers); that code had to be updated due to the what4 changes.
Co-authored-by: Tristan Ravitch <tristan@galois.com>
The previous implementation used all of the registers defined in ASL translator.
It turns out that we don't actually use all of them in macaw; the significant
difference is that the `__memory` pseudo-location is used by asl-translator, but
not macaw (as macaw handles memory through implicit context). This change
modifies the register assignment to include everything except memory (which
requires an update to the asl-translator submodule).
Consolidate three different checks that control when to explore
a function into a single one defined in exploreFunPred.
Modify noreturn function calls to not treat the return address
as a potential function entry point.
Add basic checking of LSDA address to compare-dwarfdump.
Minor code refactoring and submodule updates.
aarch32: Support mixed ARM/Thumb1 binaries
This updates the aarch32 backend to decode Thumb instructions and generate the Thumb semantics. The major implementation change is to use the `ArchBlockPrecond` feature of macaw to track the Thumb state (`PSTATE_T`) across block boundaries.
The ARM code discovery decides whether or not a function entry point should be decoded as Thumb by examining the low bit of the function address. If the low bit is set, it is a Thumb entry point. This has the slightly odd effect of causing macaw to say that the function is at the address with the low bit set, which is not technically true. This is documented in the README, but not obvious on inspection. Most use cases should not care, and can in any case account for it. In the future, it should be possible to fix this (though it will require some changes to the core of macaw).
This change treats them as no-ops (which is what they do on all released
hardware). We could represent them with arch extensions. This has a supporting
change in flexdis86 (included as a submodule).
* update to bv-sized branch of what4 and other things
* removed parameterized-utils submodule completely
* Updates submodules
* Fixes macaw-symbolic w.r.t. crucible-llvm changes
Co-authored-by: Ben Selfridge <ben@000548-benselfridge.local>
Improve the TH codegen for macaw-semmc
This change lazily translates as much as possible. It also generates somewhat more compact code. This change also finishes implementing primitives for the aarch32 backend. Complementing the aarch32 changes, the macaw-semmc interface has been modified to allow macaw-aarch32 to avoid a redundant serialize-deserialize round.
Co-authored-by: Kevin Quick <kquick@galois.com>
