Verifying programs with output

[tomsik68]

When verifying programs that use output like printf,puts,fprintf, Symbiotic is unable to tell the difference between output from klee and output from the verified program.

To reproduce the problem, verify memcleanup of the following program with --no-slice:

extern int printf(const char *, ...);

int main()
{
    printf("KLEE: ERROR: malicious.c:5: memory error: memory not cleaned up");
    return 0;
}

Fortunately, error replay prevents us from producing incorrect answer, but this prevents Symbiotic from answering correctly. I suggest we somehow ignore calls of these functions in klee.

[mchalupa]

I see, I know about this problem, but ignoring the calls can introduce other problems. The printf function may not only print output but also set variables ("%n" format), so we cannot entirely ignore it. The best solution would probably be to provide our implementations of such functions (which would also work generally for other verifiers than KLEE).

We can replace the pritnf call with some __symbiotic_printf that would perform the print into a string and returned the same values (and performed the side-effects) as would the print do..

[mchalupa]

For KLEE, we can redirect the stdout/stderr during executing the external calls to new file descriptors (opened over /dev/stdnull for instance), so that they do not get mixed with the output of KLEE.

[tomsik68]

I didn't think of %n, now I agree we can't just get rid of the calls. But I like the solution which redirects output to /dev/null.