mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-11-27 03:13:43 +03:00
89fc5a73f7
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> |
||
|---|---|---|
| .. | ||
| 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