On Oct 8, 2014, at 2:44 AM, Cristian Cadar <[email protected]> wrote:
> 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
>
> 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
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
