Skip to content

Document building CBMC with IPASIR and Riss #6031

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Apr 14, 2021
Merged

Document building CBMC with IPASIR and Riss #6031

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
47 changes: 47 additions & 0 deletions COMPILING.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -373,3 +373,50 @@ compilation flag:
cmake -S . -Bbuild -DCMAKE_CXX_FLAGS="-DBDD_GUARDS"
```
and then `cmake --build build`

## Compiling with alternative SAT solvers

For the packaged builds of CBMC on our release page we currently build CBMC
with the MiniSat2 SAT solver statically linked at compile time. However it is
also possible to build CBMC using alternative SAT solvers.

### Compiling with Riss

The [Riss](https://github.com/conp-solutions/riss) solver supports the
[IPASIR](https://github.com/biotomas/ipasir) C interface to incremental SAT
solvers, which is also supported by CBMC. So the process for producing a CBMC
with Riss build is to build Riss as a static library then compile CBMC with the
IPASIR build options and link to the Riss static library. The following
instructions have been confirmed to work on Ubuntu 20 at the time of writing.
They can also be made to work on Ubuntu 18, by using a debug build of Riss. Riss
uses Linux specific functionality / API calls. Therefore it can't be compiled
successfully on Windows or macOS.

1. Download Riss:
```
git clone https://github.com/conp-solutions/riss riss
```
This will clone the Riss repository into a `riss` subdirectory.

2. Build Riss:
```
cd riss
cmake -H. -Brelease -DCMAKE_BUILD_TYPE=Release
cd release
make riss-coprocessor-lib-static
cd ../..
```
This will create a build directory called `release` inside the clone of the
Riss repository and build the static library in
`riss/release/lib/libriss-coprocessor.a`.

3. Build CBMC:
```
make -C src LIBS="$PWD/riss/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss/riss
```
This links the Riss library and the pthreads library. The pthreads library is
needed because the Riss library uses it for multithreading. Passing the
IPASIR parameter tells the build system to build for the IPASIR interface.
The argument for the IPASIR parameter gives the build system the location for
the IPASIR headers, which is needed for the cbmc includes of `ipasir.h`. The
compiled binary will be placed in `cbmc/src/cbmc/cbmc`.