Re: [klee-dev] KLEE SMT query overhead

[William Leeson]

>
> Are we talking about "orders of magnitude" in the milli/micro-second
> range or about really expensive queries?

Expensive. If it helps, I ran klee for 5 hours on the most recent version
of find with the following settings:

klee --simplify-sym-indices --write-cvcs --write-cov --output-module
--max-memory=2000 --disable-inlining --optimize --use-forked-solver
--use-cex-cache --libc=uclibc --posix-runtime --external-calls=all
--only-output-states-covering-new --use-query-log=solver:smt2
--env-file=test.env --run-in-dir=/tmp/sandbox --write-smt2s
--max-sym-array-size=4096 --max-time=300min --watchdog
--max-memory-inhibit=false --max-static-fork-pct=1 --max-static-solve-pct=1
--max-static-cpfork-pct=1 --switch-type=internal --search=random-path
--search=nurs:covnew --use-batching-search --batch-instructions=1
findutils-4.9.0/obj-llvm/find/find.bc -sym-args 0 3 20 -sym-files 1 40
-sym-stdin 40

There are 10 queries listed as taking over 100s in the solver-queries.smt2
file, but when I ask STP to solve them, it takes somewhere between 0.6 and
1.7 seconds to solve.

Are you using the solvers in the container directly or via kleaver?
>
The results described above, directly in the container. However, I have
replicated it on a full install of klee with Z3. Should I be using kleaver?

Sorry for the duplicate message. I just realized I didn't reply all.

Thank you,
Will

On Wed, Mar 9, 2022 at 10:57 AM Frank Busse  wrote:

> Hi,
>
>
> On Tue, 8 Mar 2022 13:58:57 -0500
> William Leeson  wrote:
>
> > I'm finding that the Elapsed time reported by KLEE in solver-queries.smt2
> > for a single query is  different from the time reported by the solver
> klee
> > is built on (stp_simple in the docker /tmp folder). Orders of magnitude
> > different. I confirmed this on a local install of KLEE with Z3-4.8.4 as
> the
> > backend solver.
>
> Are we talking about "orders of magnitude" in the milli/micro-second
> range or about really expensive queries?
>
> > I was wondering if this is to be expected. Is there some overhead KLEE
> > incurs when calling the solvers? Is the solver being fed more than Query
> #X
> > from solver-queries.smt2 (For example, is it an incremental solve with
> > previous queries taken into account?)
>
> There is no incremental solving in upstream KLEE. The time is measured
> by another pseudo-solver in the solving chain (QueryLoggingSolver) in
> front of the core solvers (STP, Z3, MetaSMT). Hence, there is overhead
> involved, e.g. the conversion of KLEE's native expressions into
> solver-specific queries or for STP even a call of fork() depending on
> the configuration.
>
> Are you using the solvers in the container directly or via kleaver?
>
>
> Kind regards,
>
> Frank
>
> ___
> 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 SMT query overhead

[Frank Busse]

Hi,


On Tue, 8 Mar 2022 13:58:57 -0500
William Leeson  wrote:

> I'm finding that the Elapsed time reported by KLEE in solver-queries.smt2
> for a single query is  different from the time reported by the solver klee
> is built on (stp_simple in the docker /tmp folder). Orders of magnitude
> different. I confirmed this on a local install of KLEE with Z3-4.8.4 as the
> backend solver.

Are we talking about "orders of magnitude" in the milli/micro-second
range or about really expensive queries?

> I was wondering if this is to be expected. Is there some overhead KLEE
> incurs when calling the solvers? Is the solver being fed more than Query #X
> from solver-queries.smt2 (For example, is it an incremental solve with
> previous queries taken into account?)

There is no incremental solving in upstream KLEE. The time is measured
by another pseudo-solver in the solving chain (QueryLoggingSolver) in
front of the core solvers (STP, Z3, MetaSMT). Hence, there is overhead
involved, e.g. the conversion of KLEE's native expressions into
solver-specific queries or for STP even a call of fork() depending on
the configuration.

Are you using the solvers in the container directly or via kleaver?


Kind regards,

Frank

___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Re: [klee-dev] Collect path constraints with seed mode

[Cristian Cadar]

Hi,

On 21/09/2021 09:00, zy j wrote:

Hi,

I want to collect the path constraints of a specific PoC generated by 
fuzzing, I have found similar question in 
https://www.mail-archive.com/klee-dev@imperial.ac.uk/msg02743.html 
, 
which helps a lot, I added --use-query-log=all:smt2,solver:smt2 
--write-cvcs --write-smt2s to dump the constraints into files, and I got 
the test01.cvc and test01.smt2 successfully.


Considering my purpose is to get the path constraints of given PoC, I 
should use test01.smt2 file, right? But the constraints in that file 
are very few, seems they are not in accumulate mode, but only record the 
constraints for the last branch. If I want to collect the whole path 
constraints for a given PoC (if there are 20 branches before crash, I 
want to collect all of the 20 branches' constraints), how can I do that?
I'm not sure what is the exact question here, but test*.smt2 should 
contain the path condition associated with that path.




Besides, I also noticed that there was a command line option named 
--write-pcs, which seems to be what I need: 
https://www.mail-archive.com/klee-dev@imperial.ac.uk/msg00636.html 
. 
However, there is no --write-pcs in the latest version, is it replaced 
by other option?

It is now --write-kqueries

Best,
Cristian



Best regards,

Jiang


___
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] Need help in making a structure pointer symbolic

[Cristian Cadar]

Hi,

You can make pointers symbolic in KLEE, but this might not accomplish 
what you hope.  Making a pointer symbolic means it can refer to any 
address in memory, including invalid ones.


Best,
Cristian

On 04/03/2022 08:37, Sandip Ghosal wrote:

Hello Everyone,

Can somebody help me to make a pointer to a structure symbolic?

For example, I have a linked list node, and I am trying to make the 
pointer to the structure symbolic as follows:


struct Node{
    int data;
    struct Node *next;
}

struct Node *node = NULL;

node = (struct Node*)malloc(sizeof(struct Node))

klee_make_symbolic(node, sizeof(struct Node *), "e1");


Now what I understand is that Klee is not able to make memory address 
symbolic probably because of infinite address space. Please let me know 
if this is the limitation of Klee or there is some other way for making 
a pointer variable symbolic.


Thanks in advance.

--
Thanks & Regards
Sandip Ghosal




___
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] fork() : creating child processes in KLEE's execution

[Cristian Cadar]

Hi,

KLEE does not use the system call fork() to fork states.  See 
Executor::fork() in the code.


Best,
Cristian

On 23/02/2022 18:40, Pansilu Pitigalaarachchi wrote:

Hi,

I would like to check the possible scenarios where KLEE creates a child 
process.


1.My current understanding is that a 'state fork' performed at a branch 
condition will not result in a real forking of the KLEE process & does 
not invoke fork() syscall to create a child process of klee. i.e. the 
'state forking' described in the original KLEE paper is a process where 
the objects in klee's memory are updated to create a new state.

Can I check if this understanding is correct ?

2.In code, I encountered some cases where the fork() syscall is invoked.
lib/Solver/MetaSMTSolver.cpp
tools/klee-replay/file-creator.c
tools/klee-replay/klee-replay.c etc
Can I check if there are any cases where fork() syscall is issued to 
fork the klee process as a result of 'state forks' in symbolic execution ?


I went through the mailing list history and some literature/papers on 
klee, but cout not find a definite answer. I would really appreciate it 
if someone can help clarify.

Thanks in advance.
--
Pansilu Pitigalaarachchi


___
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 should the function parameter be symbolised if the function parameter is a file type?

[Cristian Cadar]

Hi,

To use symbolic files, you should use KLEE's symbolic environment 
support.  See https://klee.github.io/docs/options/#symbolic-environment 
and the tutorials for information on how KLEE supports symbolic files.


Best wishes,
Cristian

On 18/01/2022 03:46, rongze xv wrote:

Hi,

I am confused about How should the function parameter be symbolised if 
the function parameter is a file type.


For example, I use KLEE to test a function ok_png ok_png_read(FILE 
*file, ok_png_decode_flags decode_flags), the test code written is as 
follows:

int main(int argc, char **argv){
      FILE *file = malloc(sizeof(FILE));
      klee_make_symbolic(file,sizeof(FILE),"file");
      ok_png_read(file,OK_PNG_COLOR_FORMAT_RGBA);
}
But always get something like this, “memcpy.c:29: memory error: out of 
bound pointer”, I think the function is not tested successfully, I don't 
know how to handle such a situation, please help.


If you can reply to me in your spare time, thank you very much!!

Sincerely，
Xu Rongze

___
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 SMT query overhead

[William Leeson]

Hello,

I'm working on a project dealing with SMT solvers. We are collecting
queries from KLEE using the latest klee docker image with the
"--use-query-log=solver:smt2" flag on. We are then dividing this file into
individual queries. We run several SMT solvers on these queries and collect
the execution time.

I'm finding that the Elapsed time reported by KLEE in solver-queries.smt2
for a single query is  different from the time reported by the solver klee
is built on (stp_simple in the docker /tmp folder). Orders of magnitude
different. I confirmed this on a local install of KLEE with Z3-4.8.4 as the
backend solver.

I was wondering if this is to be expected. Is there some overhead KLEE
incurs when calling the solvers? Is the solver being fed more than Query #X
from solver-queries.smt2 (For example, is it an incremental solve with
previous queries taken into account?)

Thank you,
Will
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev