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
