# Iekke V1.0

## Introduction
Iekke is SAT-based concurrent program verification tool. It is built on top of Deagle (front-end) and MiniSAT-2.2.1 (back-end). The basic idea of Iekke is to simulate sequentialization using partial order constraints, establishing a number of rounds.
The source code of Iekke is available on https://github.com/pac-lab00/Iekke.

## Installation
### Dependencies
- g++
- flex
- bison (Version 3.5.2 is recommended)
- gcc-multilib

### Building from source
Simply run
```
cd src && make
```
This generates executable binary **iekke_exe** in directory src/cbmc.

Note: Higher versions of Bison may generate *.tab.h/*.tab.cpp that triggers warnings. On such occasions, please try removing -Werror from CXXFLAGS in src/config.inc.

## Usage

```
iekke_exe <input file> <unwind options> <specifications> --rounds <num> --minisat
```

``<specifications>`` includes:
- **--unwinding-assertions**: generate an assertion for whether each loop is fully unwinded. This specification is strongly preferred in academic usage: if the user-defined assertion is TRUE but an unwinding assertion is violated, this TRUE result of used-defined assertion is not conclusive, indicating that one needs to enlarge the unwind limit and try again. This option is directly inherited from CBMC.
- **--no-assertions** : disable user-defined assertion (default enabled). This option is directly inherited from CBMC.
- **--datarace** : enable data race detection (default disabled).
- **--pointer-check** : enable null pointer dereference detection (default disabled). This option is directly inherited from CBMC.
- **--alloc-check** : enable malloc/calloc/... validity detection (default disabled). 
- **--memory-leak-check** : enable memory leak detection (default disabled). 
- **--signed-overflow-check** and **--unsigned-overflow-check** : enable signed/unsigned overflow detection (default both disabled). These options are directly inherited from CBMC.
- **--allow-pointer-unsoundness**: enable the experimental concurrency pointer analysis which might be unsound for some cases (default disabled, but enabled by SV-COMP script).