Development
Build
To build and install from source, you'll need to install:
- GHC 9.4, 9.6, or 9.8
cabal-install
3.6 or later
Follow the instructions on the Haskell installation page.
Then, clone GREASE and its submodules:
git clone https://github.com/GaloisInc/grease
cd grease
git submodule update --init
Then, build with cabal
:
cabal build exe:grease
See Test suite for how to run the tests.
Docker
GREASE also offers a nightly Docker image that gets built after each commit to
the main
branch. To run GREASE on an input using Docker, run the following
docker run ghcr.io/galoisinc/grease:nightly <input>
GREASE's test suite can also be run through Docker, although it requires
changing the entrypoint to use grease-tests
instead:
docker run --entrypoint grease-tests ghcr.io/galoisinc/grease:nightly
The Docker image is available for both amd64
and arm64
architectures.
Documentation
Documentation is built with mdBook. Install with cargo
(or with a package
manager):
cargo install mdbook
Then build the book with:
cd doc
mdbook build
As always, see --help
for more options.
Linting
Generic scripts
We have a few Python scripts in scripts/lint/
that perform one-off
checks. They generally take some number of paths as arguments, check
.github/workflows/lint.yml
to see how they are invoked in CI.
hlint
We treat a small number of hlint warnings as errors in CI. To run hlint locally, try:
hlint grease{,-aarch32,-ppc,-x86}/src grease-cli/{main,src,tests}
ruff
We lint and format the Python linting scripts and Ghidra plug-in with ruff.
ruff format scripts/lint ghidra_scripts
ruff check scripts/lint ghidra_scripts
typos
We run typos on doc/
to spell-check the documentation. To run it locally,
try:
typos doc/
Source code
The grease
source code is split up into a number of smaller libraries, each
residing in its own top-level directory:
grease
: This comprises the core ofgrease
as a library.grease-aarch32
: This extends thegrease
library with the ability to reason about AArch32 binaries.grease-ppc
: This extends thegrease
library with the ability to reason about 32-bit and 64-bit PowerPC binaries.grease-x86
: This extends thegrease
library with the ability to reason about x86-64 binaries.grease-cli
: This defines a command-line application on top of the library code ingrease
.
Periodic tasks
The following is a list of things that should be done occasionally by GREASE developers.
- Check for out-of-date documentation
- Fix warnings from
cabal haddock
- Review and triage old issues
- Update versions of dependencies and tools
- Bump bounds on Hackage dependencies (
cabal outdated
can help) - Bump submodules
- Update versions of tools used in CI:
- Cabal
- GHC (see below)
- Linters
- OS images
what4-solvers
- Update versions of tools used in the Dockerfile:
ghcup
- Bump bounds on Hackage dependencies (
GHC versions
We support the three most recent versions of GHC. We try to support new versions as soon as they are supported by the libraries that we depend on.
Adding a new version
GREASE has several Galois-developed dependencies that are pinned as Git submodules, in deps/
.
These dependencies need to support new GHC versions before GREASE itself can.
First, create GitHub issues on each of these dependencies requesting support for the new GHC version.
Then, create an issue on the GREASE repo that includes:
- A link to the GHC release notes for the new version
- Links to the issues on the dependencies
- A link to this section of this document
Then, wait for the issues on the dependencies to be resolved. When adding support for the new GHC version to GREASE itself, complete the following steps:
- For each package:
-
Allow the new version of
base
in the Cabalbuild-depends
-
Run
cabal {build,test,haddock}
, bumping dependency bounds and submodules as needed -
Fix any new warnings from
-Wdefault
-
Allow the new version of
- Add the new GHC version to the matrix in the GitHub Actions workflows
- Bump the GHC version in the Dockerfile to the latest supported version
- Follow the below steps to remove the oldest GHC version
Removing an old version
- Remove the old version from the matrix in the GitHub Actions configuration
-
Remove outdated CPP
ifdef
s that refer to the dropped version -
Remove outdated
if
stanzas in the Cabal files