Testing Structures with klee

[Saikat Dutta]

Hi,
Normally big application have structures and linked lists or arrays of such
structures as inputs to functions. Is there an easy way to symbolically
declare them using klee? Or does one have to declare each of their
component primitive variables?
Thanks.
-Saikat

[Daniel Liew]

KLEE models memory at the bytes level so you can things like this...

include <stdio.h>

int main(int argc, char** argv)
{
typedef struct
{
int a;
int b;
} A;

A instance;

klee_make_symbolic(&instance, sizeof(A));

if ( instance.a > 0 )
printf("instance.a >0\n");
else
printf("instance.a <=0\n");

}

As for "Normally big application have..." that totally depends on what
sort of programs you are talking about. KLEE has built-in support for
declaring symbolic command line arguments and symbolic files as
command line arguments for convenience. You can get info on the is by
running

$ klee --posix-runtime <program>.bc --help

usage: (klee_init_env) [options] [program arguments]
-sym-arg <N> - Replace by a symbolic argument with length N
-sym-args <MIN> <MAX> <N> - Replace by at least MIN arguments and at most
MAX arguments, each with maximum length N
-sym-files <NUM> <N> - Make stdin and up to NUM symbolic files, each
with maximum size N.
-sym-stdout - Make stdout symbolic.
-max-fail <N> - Allow up to <N> injected failures
-fd-fail - Shortcut for '-max-fail 1'

See the Coreutils webpage
(http://ccadar.github.io/klee/TestingCoreutils.html) for an example of
how to use these

Post by Saikat Dutta
Hi,
Normally big application have structures and linked lists or arrays of such
structures as inputs to functions. Is there an easy way to symbolically
declare them using klee? Or does one have to declare each of their component
primitive variables?
Thanks.
-Saikat

[Saikat Dutta]

Thanks.
But what about linked lists? If there exists a next pointer in a structure,
will it be taken care of by klee?Or do i need to fix the length of linked
list and declare every instance of that structure symbolically?I m a bit
confused.

Post by Daniel Liew
KLEE models memory at the bytes level so you can things like this...
include <stdio.h>
int main(int argc, char** argv)
{
typedef struct
{
int a;
int b;
} A;
A instance;
klee_make_symbolic(&instance, sizeof(A));
if ( instance.a > 0 )
printf("instance.a >0\n");
else
printf("instance.a <=0\n");
}
As for "Normally big application have..." that totally depends on what
sort of programs you are talking about. KLEE has built-in support for
declaring symbolic command line arguments and symbolic files as
command line arguments for convenience. You can get info on the is by
running
$ klee --posix-runtime <program>.bc --help
usage: (klee_init_env) [options] [program arguments]
-sym-arg <N> - Replace by a symbolic argument with length N
-sym-args <MIN> <MAX> <N> - Replace by at least MIN arguments and at most
MAX arguments, each with maximum length N
-sym-files <NUM> <N> - Make stdin and up to NUM symbolic files, each
with maximum size N.
-sym-stdout - Make stdout symbolic.
-max-fail <N> - Allow up to <N> injected failures
-fd-fail - Shortcut for '-max-fail 1'
See the Coreutils webpage
(http://ccadar.github.io/klee/TestingCoreutils.html) for an example of
how to use these

Post by Saikat Dutta
Hi,
Normally big application have structures and linked lists or arrays of

such

Post by Saikat Dutta
structures as inputs to functions. Is there an easy way to symbolically
declare them using klee? Or does one have to declare each of their

component

Post by Saikat Dutta
primitive variables?
Thanks.
-Saikat

[Daniel Liew]

KLEE isn't great with completely symbolic link lists. The pointer
could point to **anything** so in order to be complete KLEE must
consider every object allocated in memory. This does not scale very
well.

Post by Saikat Dutta
Thanks.
But what about linked lists? If there exists a next pointer in a structure,
will it be taken care of by klee?Or do i need to fix the length of linked
list and declare every instance of that structure symbolically?I m a bit
confused.

Post by Daniel Liew
KLEE models memory at the bytes level so you can things like this...
include <stdio.h>
int main(int argc, char** argv)
{
typedef struct
{
int a;
int b;
} A;
A instance;
klee_make_symbolic(&instance, sizeof(A));
if ( instance.a > 0 )
printf("instance.a >0\n");
else
printf("instance.a <=0\n");
}
As for "Normally big application have..." that totally depends on what
sort of programs you are talking about. KLEE has built-in support for
declaring symbolic command line arguments and symbolic files as
command line arguments for convenience. You can get info on the is by
running
$ klee --posix-runtime <program>.bc --help
usage: (klee_init_env) [options] [program arguments]
-sym-arg <N> - Replace by a symbolic argument with length N
-sym-args <MIN> <MAX> <N> - Replace by at least MIN arguments and at most
MAX arguments, each with maximum length N
-sym-files <NUM> <N> - Make stdin and up to NUM symbolic files, each
with maximum size N.
-sym-stdout - Make stdout symbolic.
-max-fail <N> - Allow up to <N> injected failures
-fd-fail - Shortcut for '-max-fail 1'
See the Coreutils webpage
(http://ccadar.github.io/klee/TestingCoreutils.html) for an example of
how to use these

Post by Saikat Dutta
Hi,
Normally big application have structures and linked lists or arrays of such
structures as inputs to functions. Is there an easy way to symbolically
declare them using klee? Or does one have to declare each of their component
primitive variables?
Thanks.
-Saikat