No results when running symbolized OpenJpeg

[thetheodor]

Hello again, I am trying to reproduce the OpenJpeg example.

I followed the instructions on http://www.s3.eurecom.fr/tools/symbolic_execution/symcc.html:

• I built SymCC in release mode (I tried both with and without QSYM).
• I configured OpenJpeg (1f1e9682) with cmake -G Ninja .. -DBUILD_THIRDPARTY=ON and CC/CXX/SYMCC_NO_SYMBOLIC_INPUT appropriately set.
• Built OpenJpeg: I can see several warnings emitted by SymCC however I didn't see any symbolized XXX (I saw this when building the test.c example).
• Unset SYMCC_NO_SYMBOLIC_INPUT, exported SYMCC_OUTPUT_DIR and run bin/opj_decompress -i file1.jp2 -o /tmp/image.pgm, however I didn't see any output produced by SymCC's runtime.

Did I miss some step?

Thanks

[sebastianpoeplau]

Hey @ttheodor,

Have you set SYMCC_INPUT_FILE to file1.jp2? Otherwise the program will expect symbolic input on stdin.

Also, to reproduce the experiments we did for the paper you'll want to run SymCC together with AFL. There's documentation here - the gist is that we run AFL in distributed mode and make it exchange test cases with SymCC. There is a helper that repeatedly pulls interesting inputs from AFL and runs SymCC on them, feeding new test cases back to the fuzzer.

Let me know if you run into problems!

Cheers, Seb

[sebastianpoeplau]

I'm closing the issue, hoping that the docs have solved your problem. Feel free to reopen it if necessary!