[klee-dev] Replacing external printf with an internal version for the Klee tests.

[Willem Pinckaers]

Hi List,

Currently most tests for Klee depend on an externally provided printf function. Support for external functions has some side effects, among them:

- Memory usage is doubled for all non symbolic allocations. 
- The bitcode being tested has to have the same data layout as the compiled version of Klee. 

Without support for external functions Klee memory usage for non symbolic allocations can be reduced by about 50% and Klee could be made to analyze bit code that uses a different data layout.

The main barrier to being able to build and run Klee without external function support is that almost all the current test cases use external functions, in particular printf.


My goal is to convert the test cases to use an internal printf so that future patches can provide the option of not providing external functions. Currently disabling external functions breaks almost all tests.


I see two options for implementing an internal printf:

- Provide a printf written in c that is part of the test suite. This is what I have currently implemented.
 
  This currently hits a bug in llvm 3.4 and 3.5 where lli with force-interpreter=true does not properly execute va_start. But (after adopting the tests to link in the new printf) most test cases pass using force-interpreter=false.

  The main downside I see currently is that an internal printf can be executed symbolically by Klee.
  This is mitigated since the printf is only used for the test cases. And only one test case indicates the use of symbolic arguments to printf by using the —allow-external-symcalls command line argument to Kee. This test case is test/Feature/LowerSwitch.c, and that test is easily rewritten to use klee_get_value on the symbolic argument to printf.


- Alternatively provide a SpecialFunction that implements printf, using the Klee provided functionality to get concrete values and work with the data layout of the bit code being tested.
  
  I have not implemented this. It would mean less changes to the test cases, however implementation is a lot more work.




I would like to submit a pull request for this patch, and follow up patches that change the test cases to use the internal printf, but I wanted to check with the list to see if there were any (potential) issues that I should consider.


Regards,
   Willem