Re: [klee-dev] [KLEE] write to a symbolic address & constraints for write
Hi Mingyi, it's unclear to me what you are running exactly. In general,
it's good to include a complete program and the exact commands you ran.
Best wishes,
Cristian
On 20/11/2020 02:58, Liu, Mingyi wrote:
Hi klee-dev members,
I made args symbolic and provided a seed ktest file for the following
target (code snippets):
if(*(u64*)args >= 0x327b2000&& *(u64*)args <= 0x643c9000) {
printf("WRITE\n");
*(u64*)*(u64*)args = 4;
printf("val1 = %llx\n", *(u64*)args);
printf("point_to1 = %p\n", *(u64*)*(u64*)args);
}
when running the compiled target with that seed ktest file, I got the
following:
WRITE
val1 = 327b2000
point_to1 = 0x4
But, when running the target under KLEE with the seed option, I got the
following:
WRITE
val1 = 327b2000
Given that 0x327b2000 is a valid address, why was the last line failed?
Does that mean we cannot write to a symbolic address?
Another question is that, I made a, b and c symbolic for the following
target, and run it under KLEE with seed(a=2, b=3) option:
printf("a=%d\nb=%d\nc=%d\n", a, b, c);
if(a > 0&& a < 100&& b > 0&& b < 100) {
sprintf((char*)buf, "%*d%*d%n\n", a, 0, b, 0, );
}
printf("c=%d\n", c);
It was executed successfully (because is not symbolic?) and had the
following output:
a=0
b=0
c=0
c=5
Then I checked the kquery file, the constraints for a (=2) and b (=3)
could be identified easily by:
(Eq false (Sle N0 1))
(Eq false
(Ult 0
(Add w64 18446744073709551615
(SExt w64 (Add w32 4294967295 N0)
(Eq false (Sle N1 1))
(Ult 0
(Add w64 18446744073709551615
N2:(SExt w64 (Add w32 4294967295 N1
(Eq false
(Ult 0 (Add w64 18446744073709551614 N2)))]
But there are no constraints for "write" or "store" the value 5. It's
known that the KQuery language supports "read" expressions such as Read
and ReadLSB, I am wondering does it have "write" or "store" expressions?
If not, why "write" or "store" are not that necessary?
Thanks in advance, your help will be much appreciated!
Best,
Mingyi Liu
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
[klee-dev] [KLEE] write to a symbolic address & constraints for write
Hi klee-dev members,
I made args symbolic and provided a seed ktest file for the following target
(code snippets):
if (*(u64*)args >= 0x327b2000 && *(u64*)args <= 0x643c9000) {
printf("WRITE\n");
*(u64*)*(u64*)args = 4;
printf("val1 = %llx\n", *(u64*)args);
printf("point_to1 = %p\n", *(u64*)*(u64*)args);
}
when running the compiled target with that seed ktest file, I got the following:
WRITE
val1 = 327b2000
point_to1 = 0x4
But, when running the target under KLEE with the seed option, I got the
following:
WRITE
val1 = 327b2000
Given that 0x327b2000 is a valid address, why was the last line failed? Does
that mean we cannot write to a symbolic address?
Another question is that, I made a, b and c symbolic for the following target,
and run it under KLEE with seed(a=2, b=3) option:
printf("a=%d\nb=%d\nc=%d\n", a, b, c);
if (a > 0 && a < 100 && b > 0 && b < 100) {
sprintf((char*)buf, "%*d%*d%n\n", a, 0, b, 0, );
}
printf("c=%d\n", c);
It was executed successfully (because is not symbolic?) and had the
following output:
a=0
b=0
c=0
c=5
Then I checked the kquery file, the constraints for a (=2) and b (=3) could be
identified easily by:
(Eq false (Sle N0 1))
(Eq false
(Ult 0
(Add w64 18446744073709551615
(SExt w64 (Add w32 4294967295 N0)
(Eq false (Sle N1 1))
(Ult 0
(Add w64 18446744073709551615
N2:(SExt w64 (Add w32 4294967295 N1
(Eq false
(Ult 0 (Add w64 18446744073709551614 N2)))]
But there are no constraints for "write" or "store" the value 5. It's known
that the KQuery language supports "read" expressions such as Read and ReadLSB,
I am wondering does it have "write" or "store" expressions? If not, why "write"
or "store" are not that necessary?
Thanks in advance, your help will be much appreciated!
Best,
Mingyi Liu
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
