The high level goal is to write and/or generate architecture-specific backends
for /macaw/ based on the semantics discovered by /semmc/. In particular, we
are interested in making /macaw-ppc/ and /macaw-arm/. We will hand-write some
of the code, but we will generate as much as possible automatically. We will
read in the semantics files generated by /semmc/ and use Template
Haskell to generate a function that transforms machine
states according to the learned semantics.
We will implement a base package (/macaw-semmc/) that provides shared
infrastructure for all of our backends; this will include the Template Haskell
function to create a state transformer function from learned semantics files.
** Repository Layout
- ~macaw-semmc~ contains the architecture-independent components of the translation from semmc semantics into macaw IR.
- ~macaw-ppc~ implements the PowerPC-specific backend of the translation.
- ~macaw-ppc-symbolic~ implements a translation of macaw IR (with PowerPC architecture-specific functions) into Crucible IR, which is suitable for symbolic execution.
- ~macaw-arm~ implements the ARM-specific backend of the translation.
** Building
The dependencies of this project that are not available on Hackage are tracked via git submodules. To build with a reasonably modern version of ~cabal~ (i.e., one that supports ~new-build~):
