mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-11-24 00:42:28 +03:00
06f64078df
Update to API changes in macaw-base in macaw-ppc and macaw-arm The "block label" abstraction (used during arch-specific disassembly) was removed some time ago in the base macaw library. This change updates macaw-ppc and macaw-arm to remove uses of block labels. The major change is that the disassembly function only returns a single block at a time instead of a sequence of blocks. To facilitate this, the handling of the PowerPC conditional trap instruction (trap doubleword) is now an architecture-specific terminator instruction instead of encoding the logic of conditional trapping. We will now have to encode the conditional trapping logic in macaw-ppc-symbolic. Note that we have not done so yet. This commit also updates the expected results of the PowerPC tests; the number of discovered blocks is different, but not significantly so. It is hard to tell if this is a regression or an improvement. |
||
|---|---|---|
| .. | ||
| src/Data/Macaw/SemMC | ||
| ChangeLog.md | ||
| LICENSE | ||
| macaw-semmc.cabal | ||
| README.rst | ||
| Setup.hs | ||
Overview ======== This repository implements some shared code that can be re-used by multiple architecture-specific backends to bridge the semantics defined in the semmc repository [SemMC]_ to macaw [macaw]_. The semantics in SemMC are defined in terms of the ExprBuilder [EB]_ IR from Crucible/What4. The code in this library translates those ExprBuilder-based formulas into a Haskell function that generates macaw IR expressions (see the ``genExecInstruction`` function in ``Data.Macaw.SemMC.TH``). This repository contains code shared between all architectures; the intent is that each architecture will also define architecture-specific operations that are taken as an input to this library. Architecture-Specific Backends ============================== See macaw-ppc as an example for what is required in an architecture-specific backend. At a high level, the required steps are: 1. Define an architecture-specific register type 2. Define architecture-specific functions and statements 3. Define a transformation from architecture-specific locations into TH expressions 4. Define a function to translate ExprBuilder ``NonceApp``s into TH expressions 5. Define a function translate ExprBuilder ``App``s into TH expressions 6. Define a function to translate *instructions* into TH expressions Architecture-Specific Register Type ----------------------------------- Architecture-Specific Functions ------------------------------- Translating Architecture-Specific Locations ------------------------------------------- Translating ``NonceApp`` ------------------------ This translator is for translating architecture-specific uninterpreted functions, which are represented using ``NonceApp`` in ExprBuilder. These will be most often translated into architecture-specific functions, but may also require architecture-specific statements to represent side effects (including exceptions). This is also where all floating point operations are translated, as there are no floating point operations in macaw. Translating ``App`` ------------------- Very few ``App`` constructors in ExprBuilder require custom translation. This is primarily intended to translate division-type operations into architecture-specific functions, as there are no division operations defined in macaw. Translating Instructions ------------------------ The final specialized matcher is for doing direct translations of instructions into architecture-specific statements. This is meant for instructions for which we cannot express semantics in the ExprBuilder IR due to special side effects. Often, trap and system call-type instructions fall into this category. Note that this function is specified by TH ``Name`` instead of as a value-level function; this is required, as its type signature refers to an architecture-specific type, which we cannot mention in this shared library without incurring undesired dependencies. .. [SemMC] https://github.com/GaloisInc/semmc .. [macaw] https://github.com/GaloisInc/macaw .. [EB] https://github.com/GaloisInc/crucible/blob/master/what4/src/What4/Expr/Builder.hs