Libc function support (strcmp family) to enhance solving

[tosanjay]

If we use a code (attached) that has strncmp() to check a user input for a particular string (4 char long only!), the tool is not able to generate input that go beyond the guarded branch with that check. TO reproduce:

1. compile the code with symcc (./symcc fuzzme.c -o fuzzme).
2. create a simple text file (input) with random string (say AAAAA).
3. run the tool as SYMCC_SOLVER_TIMEOUT=50000 SYMCC_INPUT_FILE=/tmp/input fuzzme /tmp/input
4. continue generating inputs (upto 3rd, i guess) and after that no input is generated. fuzzme.zip

I think support for such few functions will be highly useful for better performance.

[rojaster]

As a workaround you can try this:

with models

First build the models in /models/klee-libc by

cd /models/klee-libc
./build.sh

This will produce minilibc.a

Now you can compile c applications that use a set of functions compiled by symcc:

SYMCC_REGULAR_LIBCXX=1 sym++ strcmp-example.c ../models/klee-libc/minilibc.a -o strcmp-example
../util/min-concolic-exec.sh -i ./inp -o ./outs ./strcmp-example @@
...
...