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
773 stars 135 forks source link

symcc: No output for openjpeg example #28

Closed break2make closed 3 years ago

break2make commented 3 years ago

After built of openjpeg, I have followed the following steps to start symbolic execution:

ubuntu@a7235eb2816d:~$ export SYMCC_INPUT_FILE='/tmp/file1.jp2'
ubuntu@a7235eb2816d:~$ unset SYMCC_NO_SYMBOLIC_INPUT 
ubuntu@a7235eb2816d:~$ echo $SYMCC_INPUT_FILE                 
/tmp/file1.jp2
ubuntu@a7235eb2816d:~$ sudo /tmp/openjpeg/build/bin/opj_decompress -i @@ -o /tmp/output/image.pgm

This is SymCC running with the QSYM backend
Reading program input until EOF (use Ctrl+D in a terminal)...

If I run the program without sudo:

ubuntu@a7235eb2816d:~$ /tmp/openjpeg/build/bin/opj_decompress -i @@ -o /tmp/output/image.pgm
This is SymCC running with the QSYM backend
Making data read from /tmp/file1.jp2 as symbolic
!! infile cannot be read: @@ !!

Query: Is it working? Program is waiting here for long time. Is the program waiting for input from stdin? Any suggestion.

sebastianpoeplau commented 3 years ago

Hi @break2make,

Using @@ as a placeholder for the input file is only supported via the fuzzing helper. When you want to run SymCC on a single input, just replace @@ with the actual name of the file:

$ /tmp/openjpeg/build/bin/opj_decompress -i /tmp/file1.jp2 -o /tmp/output/image.pgm

Hope this helps!

break2make commented 3 years ago

Yes, it works. Thank you.