crucible

Crucible
========

<img src="doc/crucible.svg" alt="Crucible logo" width="25%" />

Introduction
-------------

Crucible is a language-agnostic library for performing forward
symbolic execution of imperative programs.  It provides a collection
of data-structures and APIs for expressing programs as control-flow
graphs.  Programs expressed as CFGs in this way can be automatically
explored by the symbolic execution engine.  In addition, new data
types and operations can be added to the symbolic simulator by
implementing fresh primitives directly in Haskell.  Crucible relies on
an underlying library called [What4](https://github.com/GaloisInc/what4)
that provides formula representations, and connections to a variety of
SAT and SMT solvers that can be used to perform verification and find
counterexamples to logical conditions computed from program simulation.

Crucible has been designed as a set of Haskell packages organized so
that Crucible itself has a minimal number of external dependencies,
and functionality independent of crucible can be separated into sub-libraries.

Currently, the repository consists of the following Haskell packages:
 * **`crucible`** provides the core Crucible definitions, including the
   symbolic simulator and control-flow-graph program representations.
 * **`crucible-llvm`** provides translation and runtime support for
   executing LLVM assembly programs in the Crucible symbolic simulator.
 * **`crucible-jvm`** provides translation and runtime support for
   executing JVM bytecode programs in the Crucible symbolic simulator.
 * **`crux`** provides common support libraries for running the
   crucible simulator in a basic "all-at-once" use mode for simulation
   and verification.  This includes most of the setup steps required
   to actually set the simulator off and running, as well as
   functionality for collecting and discharging safety conditions and
   generated assertions via solvers.  Both the `crux-llvm` and `crucible-jvm`
   executables are thin wrappers around the functionality provided
   by `crux`.

In addition, there are the following library/executable packages:

 * **`crux-llvm`**, a standalone frontend for executing C and C++ programs
   in the crucible symbolic simulator.  The front-end invokes `clang`
   to produce LLVM bitcode, and runs the resulting programs using
   the `crucible-llvm` language frontend.

 * **`crux-llvm-svcomp`**, an alternative entrypoint to `crux-llvm`
   that uses the protocol established for the [SV-COMP][sv-comp] competition.
   See [here](crux-llvm/README.md) for more details.

[sv-comp]: https://sv-comp.sosy-lab.org

 * **`crucible-jvm`**, also contains an executable for directly
   running compiled JVM bytecode programs, in a similar vein
   to the `crux-llvm` package.

 * **`crux-mir`**, a tool for executing Rust programs in the crucible symbolic
   simulator.  This is the backend for the `cargo crux-test` command provided
   by `mir-json`.  See the [`crux-mir` README](crux-mir