Dear Ridwan,
Thank you for the link! I'm trying to use your KLEE fork (from GitHub,
not the DockerHub), but I'm unable to capture the information that I want.
For instance, I've consider the following code:
#include <stdio.h>
#include <stdlib.h>
#include </klee/source/include/klee/klee.h>
int main(){
int k;
klee_make_symbolic(&k, sizeof(k), "k");
if (k == 20)
printf("Statement Five\n");
else
printf("Statement Six\n");
printf("\nk=%d\n", k);
return 0;
}
I generate the seed file with: gen-bout --second-var model_version 4 01
--second-var k 4 20
However, the kquery file I get is:
array k[4] : w32 -> w8 = symbolic
array model_version[4] : w32 -> w8 = symbolic
(query [(Eq 1
(ReadLSB w32 0 ))
(Eq 20 <---------- I would expect 'k' here
(ReadLSB w32 0 ))]
false)
Is this the expected behaviour, or perhaps I am doing something wrong?
Regards,
Bharat
On 13/03/2021 12:33, Ridwan Shariffdeen wrote:
Hi,
What you are looking for is for a concolic execution. I have a
modified version of KLEE to get what you want.
You can refer to the repo
https://github.com/rshariffdeen/klee/tree/concolic
<https://github.com/rshariffdeen/klee/tree/concolic> and build KLEE.
There is also a docker image hosted at
dockerhub rshariffdeen/klee:concolic which is already built.
Then using seed-file, you can feed the concrete input and it willl be
executed concretely but capturing the symbolic constraints you need.
If you are not familiar with see-file setting, I can let you know how
to use for one example.
Let me know, if you have any questions or if this works for you
Regards
On Fri, Mar 12, 2021 at 9:42 PM Bharat Garhewal <[email protected]
<mailto:[email protected]>> wrote:
Dear all,
I'm working on (white-box/grey-box) Active Automata Learning for
programs with data parameters
(i.e., our automata contain data parameters in guards and in i/o).
We require that for each concrete query, we can extract data
(i.e., path) constraints for that query.
For instance, consider that we have a one-element FIFO buffer with
two actions: PUSH(p) and POP(p):
Given a query of the form ``PUSH(p1=5) POP(p2=3)'' (where p1 and
p2 are the "markers"/"names" given
to 5 and 3), we want to retrieve the constraint "p1 =/= p2" from
the path followed by the program
(assuming that the comparison between 5 and 3 actually happens in
the program). We're trying
to obtain these PC using KLEE.
I've been trying to get concrete inputs working with KLEE (latest
docker build) and Zesti (docker, from
https://github.com/rshariffdeen/zesti
<https://github.com/rshariffdeen/zesti>), but I guess I'm doing
something wrong.
For instance, consider the "Tutorial One" example, get_sign, with
no changes to the source code.
If I run it with klee-zesti, as "klee-zesti -posix-runtime
-libc=uclibc get_sign.bc 22", It would expect to explore only one
branch, but I somehow end up exploring 10?
With Zesti (if anyone has any idea), I still end up exploring all
3 branches of the function.
Does anyone have any clues on how to get this working? (Either
KLEE or Zesti would be fine :))
Thank you,
Regards,
Bharat Garhewal,
ICIS - SWS,
Radboud University
_______________________________________________
klee-dev mailing list
[email protected] <mailto:[email protected]>
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
