symbolic aggregate data structures?

[Mark R. Tuttle]

What is the "right" way to assign symbolic values to aggregate data
structures like arrays?

If I run klee on

main() {
int a[2];
klee_make_symbolic(&a,sizeof(a),"a");
return 0;
}

then "ktest-tool --write-ints" displays the array in a rather
user-unfriendly way:

num objects: 1
object 0: name: 'a'
object 0: size: 8
object 0: data: '\x00\x00\x00\x00\x00\x00\x00\x00'

If I run klee on

main(){
int a[2];
klee_make_symbolic(&a[0],sizeof(a[0]),"a0");
klee_make_symbolic(&a[1],sizeof(a[1]),"a1");
return 0;
}

then klee seems to complain that I'm calling klee_make_symbolic with a
pointer into an array and a size that is not the size of the array:

KLEE: ERROR: /nfs/site/home/mrtuttle/shr/uefi/ddt/q1/demo2.c:3: wrong size
given to klee_make_symbolic[_name]

If I run klee on

main(){
int a[2];
a[0] = klee_int("a0");
a[1] = klee_int("a1");
return 0;
}

then "ktest-tool --write-ints" displays the array fairly nicely,

num objects: 2
object 0: name: 'a0'
object 0: size: 4
object 0: data: 0
object 1: name: 'a1'
object 1: size: 4
object 1: data: 0

This seems the best solution. But is there a way to extend this to
integers of size other than four bytes, to characters, character strings
(so that strings print as strings), etc?

Thanks,
Mark

[Cristian Cadar]

This is a presentation issue, so the best solution would be to extend
the ktest-tool (a small program written in Python) to output data in the
desired format. I would be happy to consider such a patch.

Best,
Cristian

Post by Mark R. Tuttle
What is the "right" way to assign symbolic values to aggregate data
structures like arrays?
If I run klee on
main() {
int a[2];
klee_make_symbolic(&a,sizeof(a),"a");
return 0;
}
then "ktest-tool --write-ints" displays the array in a rather
num objects: 1
object 0: name: 'a'
object 0: size: 8
object 0: data: '\x00\x00\x00\x00\x00\x00\x00\x00'
If I run klee on
main(){
int a[2];
klee_make_symbolic(&a[0],sizeof(a[0]),"a0");
klee_make_symbolic(&a[1],sizeof(a[1]),"a1");
return 0;
}
then klee seems to complain that I'm calling klee_make_symbolic with a
KLEE: ERROR: /nfs/site/home/mrtuttle/shr/uefi/ddt/q1/demo2.c:3: wrong
size given to klee_make_symbolic[_name]
If I run klee on
main(){
int a[2];
a[0] = klee_int("a0");
a[1] = klee_int("a1");
return 0;
}
then "ktest-tool --write-ints" displays the array fairly nicely,
num objects: 2
object 0: name: 'a0'
object 0: size: 4
object 0: data: 0
object 1: name: 'a1'
object 1: size: 4
object 1: data: 0
This seems the best solution. But is there a way to extend this to
integers of size other than four bytes, to characters, character strings
(so that strings print as strings), etc?
Thanks,
Mark
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

[Mark R. Tuttle]

Thanks, that's great. I'm also seeking assurance, I guess, that I'm not
missing semantic or performance distinctions of significance among

int a[2];
klee_make_symbolic(&a,sizeof(a),"a");

and

int a[2];
a[0] = klee_int("a0");
a[1] = klee_int("a1");

and

int a[2];
for (int i=0; i<2; i++) { a[i] = klee_int("a"); }

Thanks,
Mark

This is a presentation issue, so the best solution would be to extend the
ktest-tool (a small program written in Python) to output data in the
desired format. I would be happy to consider such a patch.
Best,
Cristian

Post by Mark R. Tuttle
What is the "right" way to assign symbolic values to aggregate data
structures like arrays?
If I run klee on
main() {
int a[2];
klee_make_symbolic(&a,sizeof(a),"a");
return 0;
}
then "ktest-tool --write-ints" displays the array in a rather
num objects: 1
object 0: name: 'a'
object 0: size: 8
object 0: data: '\x00\x00\x00\x00\x00\x00\x00\x00'
If I run klee on
main(){
int a[2];
klee_make_symbolic(&a[0],sizeof(a[0]),"a0");
klee_make_symbolic(&a[1],sizeof(a[1]),"a1");
return 0;
}
then klee seems to complain that I'm calling klee_make_symbolic with a
KLEE: ERROR: /nfs/site/home/mrtuttle/shr/uefi/ddt/q1/demo2.c:3: wrong
size given to klee_make_symbolic[_name]
If I run klee on
main(){
int a[2];
a[0] = klee_int("a0");
a[1] = klee_int("a1");
return 0;
}
then "ktest-tool --write-ints" displays the array fairly nicely,
num objects: 2
object 0: name: 'a0'
object 0: size: 4
object 0: data: 0
object 1: name: 'a1'
object 1: size: 4
object 1: data: 0
This seems the best solution. But is there a way to extend this to
integers of size other than four bytes, to characters, character strings
(so that strings print as strings), etc?
Thanks,
Mark
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

[Cristian Cadar]

Hi Mark, the three approaches should be roughly equivalent (although
there are some small differences), but in the unlikely event that you
notice any significant performance differences, please let us know.

Cristian

Post by Mark R. Tuttle
Thanks, that's great. I'm also seeking assurance, I guess, that I'm not
missing semantic or performance distinctions of significance among
int a[2];
klee_make_symbolic(&a,sizeof(a),"a");
and
int a[2];
a[0] = klee_int("a0");
a[1] = klee_int("a1");
and
int a[2];
for (int i=0; i<2; i++) { a[i] = klee_int("a"); }
Thanks,
Mark
This is a presentation issue, so the best solution would be to
extend the ktest-tool (a small program written in Python) to output
data in the desired format. I would be happy to consider such a patch.
Best,
Cristian
What is the "right" way to assign symbolic values to aggregate data
structures like arrays?
If I run klee on
main() {
int a[2];
klee_make_symbolic(&a,sizeof(__a),"a");
return 0;
}
then "ktest-tool --write-ints" displays the array in a rather
num objects: 1
object 0: name: 'a'
object 0: size: 8
object 0: data: '\x00\x00\x00\x00\x00\x00\x00\__x00'
If I run klee on
main(){
int a[2];
klee_make_symbolic(&a[0],__sizeof(a[0]),"a0");
klee_make_symbolic(&a[1],__sizeof(a[1]),"a1");
return 0;
}
then klee seems to complain that I'm calling klee_make_symbolic with a
/nfs/site/home/mrtuttle/shr/__uefi/ddt/q1/demo2.c:3: wrong
size given to klee_make_symbolic[_name]
If I run klee on
main(){
int a[2];
a[0] = klee_int("a0");
a[1] = klee_int("a1");
return 0;
}
then "ktest-tool --write-ints" displays the array fairly nicely,
num objects: 2
object 0: name: 'a0'
object 0: size: 4
object 0: data: 0
object 1: name: 'a1'
object 1: size: 4
object 1: data: 0
This seems the best solution. But is there a way to extend this to
integers of size other than four bytes, to characters, character strings
(so that strings print as strings), etc?
Thanks,
Mark
_________________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/__mailman/listinfo/klee-dev
<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
_________________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/__mailman/listinfo/klee-dev
<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev