Hi Cristi,
I understand. LLVM seems to compile functions with return
in similar way.
...
if (y > 0) {
a = klee_get_state_info();
} else {
b = klee_get_state_info();
}
...
LLVM lifts the function call here too and assigns for
a and b the same return value. For me this is not the
desired bahavior since the function returns different
values for each of the exeuction state, but this is
probably my design issue.
Raimondas
On 11.06.2009, at 02:16, Cristian Cadar wrote:
> Hi Raimondas, this is really a question of how LLVM compiles the code.
> In the first case, LLVM lifts the call to klee_warning before the
> second
> if statement, while in the second case it doesn't. You can take a
> look
> at klee-last/assembly.ll, which contains a disassembled version of the
> actual LLVM bitcode run by KLEE.
>
> Cristian
>
> On Thu, 2009-06-11 at 02:02 +0200, Raimondas Sasnauskas wrote:
>> Hi,
>>
>> I've noticed one strange effect when caling special functions
>> with empty parameter list from interpreted code in KLEE.
>>
>> Assume we add klee_warning2() which print a string to cerr.
>>
>> lib/Core/SpecialFunctionHandler.h:
>>
>> HANDLER(handleWarning2);
>>
>> lib/Core/SpecialFunctionHandler.cpp:
>>
>> add("klee_warning2", handleWarning2, false),
>>
>> [..]
>>
>> void SpecialFunctionHandler::handleWarning2(ExecutionState &state,
>> KInstruction *target,
>> std::vector<ref<Expr> >
>> &arguments) {
>> assert(arguments.size()==0 && "invalid number of arguments to
>> klee_warning2");
>> llvm::cerr << "klee warning 2\n";
>> }
>>
>> Now let's take this example:
>>
>> int main() {
>>
>> int x = klee_int("x");
>> int y = klee_int("y");
>>
>> if (x > 0) {
>> /* nop */
>> } else {
>> if (y > 0) {
>> klee_warning2();
>> } else {
>> klee_warning2();
>> }
>> }
>>
>> return 0;
>> }
>>
>> # klee test.o
>> KLEE: output directory = "klee-out-0"
>> KLEE: WARNING: undefined reference to function: klee_warning2
>> klee warning 2
>> KLEE: done: total instructions = 44
>> KLEE: done: completed paths = 2
>> KLEE: done: generated tests = 2
>>
>> The function klee_warning2 is executed only once.
>> Let's make a small modification:
>>
>> ...
>> if (y > 0) {
>> ++x;
>> klee_warning2();
>> } else {
>> ...
>>
>> # klee test.o
>> KLEE: output directory = "klee-out-2"
>> KLEE: WARNING: undefined reference to function: klee_warning2
>> klee warning 2
>> klee warning 2
>> KLEE: done: total instructions = 62
>> KLEE: done: completed paths = 3
>> KLEE: done: generated tests = 3
>>
>>
>> Any ideas where it comes from?
>> I have many special functions with empty parameter list
>> and this issue does not occur in the older KLEE version.
>>
>>
>> Thanks,
>> Raimondas
>>
>>
>> --
>> Raimondas Sasnauskas, PhD Student
>> Distributed Systems Group
>> RWTH Aachen University
>> http://ds.cs.rwth-aachen.de/members/sasnauskas
>>
>>
>>
>>
>>
>>
>> _______________________________________________
>> klee-dev mailing list
>> klee-dev at keeda.stanford.edu
>> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
>
--
Raimondas Sasnauskas, PhD Student
Distributed Systems Group
RWTH Aachen University
http://ds.cs.rwth-aachen.de/members/sasnauskas
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 2498 bytes
Desc: not available
Url :
http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20090611/d3a280d4/attachment.bin
