klee_make_symbolic function definition

[Hongxu Chen]

Hi,

I hope to get to know what value is made symbolic during klee execution;
I add a printf log at the beginning of the function klee_make_symbolic
inside runtime/Runtest/intrinsics.c(
https://github.com/ccadar/klee/blob/master/runtime/Runtest/intrinsics.c#L34
):

fprintf(stderr, "klee_make_symbolic for %s with %lu bytes\n", name, nbytes);

However when running there is no output about it when klee meets
klee_make_symbolic function call in LLVM IR. So am I missing something?

Best Regards,
Hongxu Chen
**

[Kuchta, Tomasz]

Hello,

You could try to do the following to print the name of the symbolic variable:

In lib/Core/SpecialFunctionHanlder.cpp there is a handler named
handleMakeSymbolic.

At the beginning of the handler, there is an if-else block and in the ‘else’ part
‘name’ string is set.
You could try to add
klee_message(“symbolic variable name: %s”, name.c_str());
to print the name string.

Hope that helps,
Best regards,
Tomek


On 31 Oct 2013, at 08:17, Hongxu Chen <leftcopy.chx-***@public.gmane.org<mailto:leftcopy.chx-***@public.gmane.org>> wrote:

Hi,

I hope to get to know what value is made symbolic during klee execution; I add a printf log at the beginning of the function klee_make_symbolic inside runtime/Runtest/intrinsics.c(https://github.com/ccadar/klee/blob/master/runtime/Runtest/intrinsics.c#L34):

fprintf(stderr, "klee_make_symbolic for %s with %lu bytes\n", name, nbytes);

However when running there is no output about it when klee meets klee_make_symbolic function call in LLVM IR. So am I missing something?

Best Regards,
Hongxu Chen

[Daniel Liew]

KLEE will not let you call printf on symbolic data (I am not sure
about fprintf). To check if something is symbolic you should use the
klee_is_symbolic() (
https://github.com/ccadar/klee/blob/master/include/klee/klee.h ).

Also the implementation of klee_make_symbolic you link to is not what
is used during symbolic execution. What you link to is the version of
klee_make_symbolic used for replay. The version of klee_make_symbolic
used during symbolic execution is in SpecialFunctionHandler.cpp ( see
https://github.com/ccadar/klee/blob/master/lib/Core/SpecialFunctionHandler.cpp#L648
)

You can also use klee_print_expr("The value is:", your_expr); where
your_expr can be pretty much anything.

Hope that helps.

Post by Hongxu Chen
Hi,
I hope to get to know what value is made symbolic during klee execution;
I add a printf log at the beginning of the function klee_make_symbolic
inside
fprintf(stderr, "klee_make_symbolic for %s with %lu bytes\n", name, nbytes);
However when running there is no output about it when klee meets
klee_make_symbolic function call in LLVM IR. So am I missing something?
Best Regards,
Hongxu Chen

[Hongxu Chen]

Thanks so much Daniel and Kuchta. Now I know what I was wrong about and
following Kuchta's advice I got the symbolic value name.

Best Regards,
Hongxu Chen

Post by Daniel Liew
KLEE will not let you call printf on symbolic data (I am not sure
about fprintf). To check if something is symbolic you should use the
klee_is_symbolic() (
https://github.com/ccadar/klee/blob/master/include/klee/klee.h ).
Also the implementation of klee_make_symbolic you link to is not what
is used during symbolic execution. What you link to is the version of
klee_make_symbolic used for replay. The version of klee_make_symbolic
used during symbolic execution is in SpecialFunctionHandler.cpp ( see
https://github.com/ccadar/klee/blob/master/lib/Core/SpecialFunctionHandler.cpp#L648
)
You can also use klee_print_expr("The value is:", your_expr); where
your_expr can be pretty much anything.
Hope that helps.

Post by Hongxu Chen
Hi,
I hope to get to know what value is made symbolic during klee

execution;

Post by Hongxu Chen
I add a printf log at the beginning of the function klee_make_symbolic
inside
runtime/Runtest/intrinsics.c(

https://github.com/ccadar/klee/blob/master/runtime/Runtest/intrinsics.c#L34

Post by Hongxu Chen
fprintf(stderr, "klee_make_symbolic for %s with %lu bytes\n", name,

nbytes);

Post by Hongxu Chen
However when running there is no output about it when klee meets
klee_make_symbolic function call in LLVM IR. So am I missing something?
Best Regards,
Hongxu Chen