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

[Daniel Liew]

On 7 October 2014 23:47, Willem Pinckaers

Post by Willem Pinckaers
Hi List,
- 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.

Post by Willem Pinckaers
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.

Post by Willem Pinckaers
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.

[Cristian Cadar]

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

Post by Daniel Liew
On 7 October 2014 23:47, Willem Pinckaers

Post by Willem Pinckaers
Hi List,
- 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.

Post by Willem Pinckaers
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.

Post by Willem Pinckaers
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
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

[Willem Pinckaers]

Indeed, I don't think we need to optimize the memory consumption of the test suite, it is not excessive.

It seems I didn’t explain myself very well.

I would like to be able to run Klee on bit code with a different data layout, in particular a different pointer size. To test if my changes break anything I would like to run the test suite, however the test suite depends on calling external functions. And when external functions are needed/used it means that the data layout has to match with Klee.

By adding support for an internal printf I was hoping to be able to run the test suite to see if my changes break other parts of Klee, besides external function calls. (Which they do: test/Feature/FunctionPointer.c breaks and can be fixed with minor changes to legalFunctions)

(As a side effect it seems that memory is allocated twice for use with external functions, which could be disabled when external functions are not needed, but this is a minor issue to me at the moment).




I will do more work on testing if Klee can be made to support running bit code with a different data layout and if I am successful revisit this topic. It seems that there is no general benefit to having an internal printf at this point.

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.

Would adding a klee_internal_printf to the intrinsic functions which get aliased to printf when running with external functions disabled be acceptable?



Regards,
Willem

Best,
Cristian

Post by Daniel Liew
On 7 October 2014 23:47, Willem Pinckaers

Post by Willem Pinckaers
Hi List,
- 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.

Post by Willem Pinckaers
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.

Post by Willem Pinckaers
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
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

[Cristian Cadar]

Hi Willem,

Post by Willem Pinckaers
I would like to be able to run Klee on bit code with a different data
layout, in particular a different pointer size.

Yes, that would be a useful scenario to support.

Post by Willem Pinckaers
Would adding a klee_internal_printf to the intrinsic functions which
get aliased to printf when running with external functions disabled
be acceptable?

Yes, I think this would be ok.

Cristian