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

[Cristian Cadar]

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, &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
> 
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>