Kalashnikov is a fully automatic program synthesiser and second-order SAT solver. As well as a program synthesiser, Kalashnikov is a decision procedure for an NEXPTIME-complete logic, which means you can use it for a very wide class of problems, including:
- Synthesising C programs from a specification (the specification is also given as a C program).
- Superoptimisation (producing optimal code that does the same thing as some other code).
- Finding bugs in C programs with no false alarms.
- Proving safety for C programs.
- Proving termination and non-termination of C programs.
- Automatic refactoring.
- Automatically finding complexity bounds.
Currently the only operating system we support is Linux.
- Make sure you have Python and the standard C toolchain installed, including
gcc. - Download and install CBMC. Make sure to add it to your
PATH. - Clone this repository.
- Set the
KALASHNIKOVDIRenvironment variable to point to the directory you just cloned into. - Add
$KALASHNIKOVDIR/srcto yourPATH. - Run some examples!
sudo apt-get install cbmc gcc python
git clone https://github.com/blexim/synth ~/kalashnikov
export KALASHNIKOVDIR=~/kalashnikov
export PATH=$PATH:$KALASHNIKOVDIR/src/kalashnikov
kalashnikov.py --help
- Second-Order Propositional Satisfiability: describes the synthesiser itself, how it works, the problem it solves and the underlying theory.
- Using Program Synthesis for Program Analysis: describes how Kalashnikov is optimised specifically for building program analyses.
- Unrestricted Termination and Non-Termination Arguments for Bit-Vector Programs: we used Kalashnikov to prove termination and non-termination for C programs. The tool we built for this paper is Juggernaut, which is slow but unstoppable.
- Propositional Reasoning about Safety and Termination of Heap-Manipulating Programs: this is a logic & associated decision procedure we made in order to use Kalashnikov for reasoning about programs with linked lists. The associated tool is Shakira, which checks that heaps don't lie.
- Danger Invariants: Kalashnikov can be used for finding very deep bugs in C programs without false positives by searching for Danger Invariants. The associated tool is Dangerzone.