Hey there, great fan of the project. I'm currently looking further into it with the goal of implementing a different cost model for the instructions under synthesis, but I can't wrap my head around the right usage of souper.
Through other issues, reading the source code and the README, I deduced that the tool is embedded in the sclang/sclang++ derivatives of the normal LLVM compiler. The tool was built successfully and seems to run with the following command:
env SOUPER_DEBUG=1 SOUPER_USE_CEGIS=1 time ../build/sclang -O3 sqlite3.c shell.c -lpthread -ldl -lm -o sqlite_souper
The source code to sqlite, I'm trying to compile can be found here: https://sqlite.org/download.html
Notice the additional flags for debug output and CEGIS usage.
The output shows that the CEGIS inference runs and sometimes also finds SAT equations; however, the resulting binary always has the same size as the binary compiled by the clang compiler present in the third-party packages. I additionally increased the instructions to be synthesized from only "const" to "and,or,xor,const,ne,ule", without any result. I have a redis instance running on the same machine, and it seems to be used, as subsequent compilations run faster by a large margin.
Has anyone with experience in using souper, any idea what I'm doing wrong? Is the tool still applicable in 2025 and with LLVM 18? Am I using the wrong examples?
Hey there, great fan of the project. I'm currently looking further into it with the goal of implementing a different cost model for the instructions under synthesis, but I can't wrap my head around the right usage of souper.
Through other issues, reading the source code and the README, I deduced that the tool is embedded in the sclang/sclang++ derivatives of the normal LLVM compiler. The tool was built successfully and seems to run with the following command:
The source code to sqlite, I'm trying to compile can be found here: https://sqlite.org/download.html
Notice the additional flags for debug output and CEGIS usage.
The output shows that the CEGIS inference runs and sometimes also finds SAT equations; however, the resulting binary always has the same size as the binary compiled by the clang compiler present in the third-party packages. I additionally increased the instructions to be synthesized from only "const" to "and,or,xor,const,ne,ule", without any result. I have a redis instance running on the same machine, and it seems to be used, as subsequent compilations run faster by a large margin.
Has anyone with experience in using souper, any idea what I'm doing wrong? Is the tool still applicable in 2025 and with LLVM 18? Am I using the wrong examples?