[klee-dev] Using KLEE to obtain Path Constraints from concrete input queries in an Active Learning setting

[Bharat Garhewal]

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), 
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
-------------- next part --------------
HTML attachment scrubbed and removed