[klee-dev] [KLEE] write to a symbolic address & constraints for write

[Liu, Mingyi]

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, &c);
}

printf("c=%d\n", c);

It was executed successfully (because &c 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
-------------- next part --------------
HTML attachment scrubbed and removed