This is a project to generate C code using an LLM and check its equivalence with symbolic execution.
Note: Floating point operations are not supported by KLEE, and so we kind of have to avoid them. Not ideal...
Start the klee container
docker run --rm -it -v $(pwd):/home/klee/workspace klee/klee
Install the python dependencies TODO: Add to dockerfile
pip install openai python-dotenv
Run the python script to generate the C code and check equivalence with symbolic execution
python3 kleeGeneration.py
Compile the C code to a bytecode file
clang -emit-llvm -c -g kleeTest.c -o kleeTest.bc
Run the symbolic execution
klee --write-smt2s kleeTest.bc