Indeed, I don't think we need to optimize the memory consumption of the
test suite, it is not excessive.
The ability to deal with external calls is one of the most important
strengths of dynamic symbolic execution. However, as Dan pointed out,
there is the option of disallowing such calls if needed. I could
understand the need to special case printf and I'd be happy to consider
such a patch, but this should be an option to KLEE, which should not
require any changes to the test suite.
Best,
Cristian
On 08/10/14 10:34, Daniel Liew wrote:
On 7 October 2014 23:47, Willem Pinckaers
<[email protected]> wrote:
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.
For the test suite I really don't think the memory usage matters. They
are mostly small programs and testing external function calls is
important because it is an important feature of KLEE because real
world code inevitably needs to call into a C library or make system
calls at some point.
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.
Outside of the test suite I could see these being potentially useful
but if you really need this wouldn't it be simpler if your program had
no external function calls? If your program has external calls and you
disable external call support in KLEE your program probably isn't
going to run.
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.
Could you report that to the LLVM developers?
Thanks,
Dan.
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
