eurecom-s3 / symcc

SymCC: efficient compiler-based symbolic execution
http://www.s3.eurecom.fr/tools/symbolic_execution/symcc.html
GNU General Public License v3.0
781 stars 137 forks source link

Manual build not generating symbolic output #74

Open PROgram52bc opened 3 years ago

PROgram52bc commented 3 years ago

When I followed the main Readme document and built symcc afresh, the compiled executable doesn't contain any symbolic execution logic. The docker image provided worked fine, however.

I thought the issue was with the missing libc++ and libc++abi library installation, since the compiled executables had different sizes. I tried apt install libc++ libc++abi, and set the corresponding environment variable (export SYMCC_LIBCXX_PATH=/usr/lib/llvm-10) Now the generated executable by sym++ sample.cpp has the same size as the one in the docker image

$ ls -l a.out
-rwxr-xr-x 1 root root 96896 Sep  1 09:14 a.out

But the issue still exists, that the executable doesn't seem to contain the symbolic execution logic

$ echo "hi" | ./a.out 
This is SymCC running with the QSYM backend
Reading program input until EOF (use Ctrl+D in a terminal)...
What's your name?
Hello, hi!

Did I miss some steps?

$ z3 --version
Z3 version 4.8.13 - 64 bit - build hashcode 148cb83b0d030fae6af99fb30f8da9a64004ba16

$ cat /etc/os-release
NAME="Ubuntu"
VERSION="20.04.2 LTS (Focal Fossa)"
ID=ubuntu
ID_LIKE=debian
PRETTY_NAME="Ubuntu 20.04.2 LTS"
VERSION_ID="20.04"
HOME_URL="https://www.ubuntu.com/"
SUPPORT_URL="https://help.ubuntu.com/"
BUG_REPORT_URL="https://bugs.launchpad.net/ubuntu/"
PRIVACY_POLICY_URL="https://www.ubuntu.com/legal/terms-and-policies/privacy-policy"
VERSION_CODENAME=focal
UBUNTU_CODENAME=focal