search

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

C++ I/O intercept function support #8

Closed wuruoyu closed 4 years ago

wuruoyu commented 4 years ago

Hi,

I am wondering do you have any plan to support the interception of C++ file I/O function (e.g. std::getline). Thank you in advance!

Ruoyu

sebastianpoeplau commented 4 years ago

Hi @wuruoyu,

In principle, C++ I/O is already supported: we hook the libc functions that libc++ uses to implement C++ I/O. So if you have an instrumented C++ runtime, things should already work as expected. For example, std::fstream and friends are implemented with fopen. Similarly, we support std::cin for reading from standard input.

Have you found a use case where symbolic C++ I/O doesn't work as it should? If so, would you mind sharing the program so that we can investigate?

Cheers, Sebastian

wuruoyu commented 4 years ago

Oh it's my bad. It seems that I set up the SYMCC_INPUT_FILE incorrectly. Now it works as expected, thank you!

sebastianpoeplau commented 4 years ago

The mechanism is a bit fragile at the moment because we expect the contents of SYMCC_INPUT_FILE as a substring in the file name that the program passes to open or fopen (possibly via the C++ standard library). I guess it would be better to transform both names to some canonical form and then check for an exact match...

sebastianpoeplau commented 4 years ago

Anyway, glad it works for you now!