Re: [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, );
}

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

Re: [klee-dev] How to make assumption on symbolic stdin in klee

[Cristian Cadar]

Hi Pushi, to do this, you will need to modify the code in runtime/POSIX.

Best,
Cristian

On 16/11/2020 12:34, Pushi Zhang wrote:

Hi all,

       As in the documentation of klee, we can use command "-sym-stdin" 
to make inputs symbolic.


       Here my question is: how can we make assumptions to the symbolic 
stdin, like in klee_assume?


Best,
Pushi

___
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

Re: [klee-dev] KLEE floating-point support

[Cristian Cadar]

Hi Aleksei,

From what I understand, you managed to rebase the KLEE-Float extension 
on top of KLEE's mainline.  That's great!


As I mentioned on GitHub, my main concern is that KLEE-Float changes the 
expression representation, which has a significant impact on the core of 
KLEE.  The question is whether it is possible to integrate the changes 
in such a way that the core of KLEE is minimally affected.  This would 
require incremental changes and careful measurements.


I am also considering right now experimenting with supporting FP 
programs via fixed-point arithmetic, see the last project at 
https://klee.github.io/projects/.


My proposal would be to first submit your changes to the KLEE-Float 
project at https://github.com/srg-imperial/klee-float.  There is still 
interest in that extension, but it's starting to show its age, as you 
can see in the open issues.  In fact, even the Docker container is 
difficult to run these days, as Arch Linux changed its packaging format 
in the meantime.


Best,
Cristian

On 22/11/2020 21:08, Aleksei Pleshakov wrote:
I currently have the https://github.com/srg-imperial/klee-float 
patch along with some FP intrinsics 
supported here: https://github.com/qrort/klee 
. You have mentioned that you'd be happy 
to discuss the possibilities of this to be merged in mainline KLEE in 
this issue . I am 
willing to take the work that needs to be done. Can we discuss it? :)


___
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