Branching on the result of strcmp

[Unknown]

Hi,

When I run the following simple program with KLEE:
------------------------------------------------------------------------
#include <stdlib.h>
#include <stdio.h>
#include <string.h>

int main(int argc, char** argv)
{
const size_t LEN = 10;
char *s = malloc(LEN);
klee_make_symbolic(s, LEN, "s");

if (strcmp(s, "world") != 0)
puts("different");
else
puts("same");

return 0;
}
------------------------------------------------------------------------

I expect to see that both branches are covered and to see at least
one occurrence of "different" and at least one occurrence of "same".
However, the lastest version of KLEE outputs:
------------------------------------------------------------------------
KLEE: output directory = "klee-out-0"
KLEE: WARNING: undefined reference to function: puts
KLEE: WARNING: undefined reference to function: strcmp
KLEE: WARNING: calling external: strcmp(146291400, 146271112)
KLEE: WARNING: calling external: puts(146271424)
different

KLEE: done: total instructions = 38
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1
------------------------------------------------------------------------

Is this the expected behaviour, or a bug in KLEE, or a configuration
problem on my side?

Thanks,

[Unknown]

What command line arguments are you running it with?

Suhabe

Post by Unknown
Hi,
------------------------------------------------------------------------
#include <stdlib.h>
#include <stdio.h>
#include <string.h>
int main(int argc, char** argv)
{
? ? const size_t LEN = 10;
? ? char *s = malloc(LEN);
? ? klee_make_symbolic(s, LEN, "s");
? ? if (strcmp(s, "world") != 0)
? ? ? ? puts("different");
? ? else
? ? ? ? puts("same");
? ? return 0;
}
------------------------------------------------------------------------
I expect to see that both branches are covered and to see at least
one occurrence of "different" and at least one occurrence of "same".
------------------------------------------------------------------------
KLEE: output directory = "klee-out-0"
KLEE: WARNING: undefined reference to function: puts
KLEE: WARNING: undefined reference to function: strcmp
KLEE: WARNING: calling external: strcmp(146291400, 146271112)
KLEE: WARNING: calling external: puts(146271424)
different
KLEE: done: total instructions = 38
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1
------------------------------------------------------------------------
Is this the expected behaviour, or a bug in KLEE, or a configuration
problem on my side?
Thanks,
--
Seungbeom Kim
_______________________________________________
klee-dev mailing list
klee-dev at keeda.stanford.edu
http://keeda.Stanford.EDU/mailman/listinfo/klee-dev

[Unknown]

Very simple:

$ klee-gcc -c -g strcmp.c
$ klee strcmp.o

Oops, it seems that uclibc is not linked by default, contrary to
the older version (before open sourcing) which links it by default.
(I was confused and mistaken when I thought --posix-runtime would
enable it; it is --init-env that is enabled by --posix-runtime. ;))

$ klee --libc=uclibc strcmp.o

solves the problem.

Thanks!

Post by Unknown
What command line arguments are you running it with?
Suhabe

Post by Unknown
Hi,
------------------------------------------------------------------------
#include<stdlib.h>
#include<stdio.h>
#include<string.h>
int main(int argc, char** argv)
{
const size_t LEN = 10;
char *s = malloc(LEN);
klee_make_symbolic(s, LEN, "s");
if (strcmp(s, "world") != 0)
puts("different");
else
puts("same");
return 0;
}
------------------------------------------------------------------------
I expect to see that both branches are covered and to see at least
one occurrence of "different" and at least one occurrence of "same".
------------------------------------------------------------------------
KLEE: output directory = "klee-out-0"
KLEE: WARNING: undefined reference to function: puts
KLEE: WARNING: undefined reference to function: strcmp
KLEE: WARNING: calling external: strcmp(146291400, 146271112)
KLEE: WARNING: calling external: puts(146271424)
different
KLEE: done: total instructions = 38
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1
------------------------------------------------------------------------
Is this the expected behaviour, or a bug in KLEE, or a configuration
problem on my side?
Thanks,
--
Seungbeom Kim

[Unknown]

My apologies; I meant to reply on the mailing list, but I replied directly.

Sorry,
Brady J. Garvin


Seungbeom Kim,

I'm no expert on KLEE, but I would say from the trace that strcmp is being
evaluated by a call to native assembly. In other words, strcmp is not
compiled to LLVM bitcode, so KLEE is approximating the functions behavior
by executing it directly. It's no surprise then that the string it picks
as a concrete argument is not equal to "world".

Presumably you would like to cover both branches. In this case I believe
that you can use uclibc and --posix-runtime as documented in the
tutorials. Or, if necessary, you could also provide a C implementation of
strcmp in your sourcefile.

Like I said, I have only had short experience with KLEE. Others may
correct or improve my response.

Thanks,
Brady J. Garvin

Post by Unknown
Hi,
------------------------------------------------------------------------

#include <stdlib.h>

Post by Unknown
#include <stdio.h>
#include <string.h>
int main(int argc, char** argv)
{
const size_t LEN = 10;
char *s = malloc(LEN);
klee_make_symbolic(s, LEN, "s");
if (strcmp(s, "world") != 0)
puts("different");
else
puts("same");
return 0;
}
------------------------------------------------------------------------
I expect to see that both branches are covered and to see at least one

occurrence of "different" and at least one occurrence of "same".

Post by Unknown
------------------------------------------------------------------------

KLEE: output directory = "klee-out-0"

Post by Unknown
KLEE: WARNING: undefined reference to function: puts
KLEE: WARNING: undefined reference to function: strcmp
KLEE: WARNING: calling external: strcmp(146291400, 146271112)
KLEE: WARNING: calling external: puts(146271424)
different
KLEE: done: total instructions = 38
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1
------------------------------------------------------------------------
Is this the expected behaviour, or a bug in KLEE, or a configuration

problem on my side?

Post by Unknown
Thanks,
--
Seungbeom Kim
_______________________________________________
klee-dev mailing list
klee-dev at keeda.stanford.edu
http://keeda.Stanford.EDU/mailman/listinfo/klee-dev