About KLEE, how to extract path conditions

[Andrea Aquino]

To the attention of the KLEE staff,

first of all we would like to introduce ourselves.
My name is Andrea Aquino while my colleague’s name is Meixian Chen, we are Ph.D. students at Università della Svizzera Italiana (Switzerland, Ticino).

We are currently looking for a way to extract path conditions produced by KLEE. Actually we will need to save on disk the symbolic constraints produced by KLEE during its execution in a human readable format.

For example if analysing a program KLEE calculates 3 path conditions:
1. x > 0
2. y > 0 && y < 5
3. x + y < 10

we would like to store them in a file in order to perform a posteriori checks on them.
We don’t care about redundancy (the same constraint stored two or more times).

Is there an easy way to achieve this goal?
How can we proceed?

Best regards,
Andrea Aquino, Meixian Chen

[Cristian Cadar]

You simply need to pass the --write-pcs, write-cvcs or write-smt2s
flags, see http://klee.github.io/klee/klee-files.html for more details.

Best,
Cristian

Post by Andrea Aquino
To the attention of the KLEE staff,
first of all we would like to introduce ourselves.
My name is Andrea Aquino while my colleague’s name is Meixian Chen, we are Ph.D. students at Università della Svizzera Italiana (Switzerland, Ticino).
We are currently looking for a way to extract path conditions produced by KLEE. Actually we will need to save on disk the symbolic constraints produced by KLEE during its execution in a human readable format.
1. x > 0
2. y > 0 && y < 5
3. x + y < 10
we would like to store them in a file in order to perform a posteriori checks on them.
We don’t care about redundancy (the same constraint stored two or more times).
Is there an easy way to achieve this goal?
How can we proceed?
Best regards,
Andrea Aquino, Meixian Chen
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

[Meixian Chen]

To the attention of the KLEE staff,

Thanks for your reply. We are trying to analysis the constraint queries
reusing opportunities in a single program and across different programs. We
try to collect constraint by KLEE after optimisation like simplification
and independence, but not cache. How could we achieve that?

Best regards,
Meixian Chen, Andrea Aquino

Post by Andrea Aquino
To the attention of the KLEE staff,
first of all we would like to introduce ourselves.
My name is Andrea Aquino while my colleague's name is Meixian Chen, we are
Ph.D. students at Università della Svizzera Italiana (Switzerland, Ticino).
We are currently looking for a way to extract path conditions produced by
KLEE. Actually we will need to save on disk the symbolic constraints
produced by KLEE during its execution in a human readable format.
1. x > 0
2. y > 0 && y < 5
3. x + y < 10
we would like to store them in a file in order to perform a posteriori checks on them.
We don't care about redundancy (the same constraint stored two or more
times).
Is there an easy way to achieve this goal?
How can we proceed?
Best regards,
Andrea Aquino, Meixian Chen