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

[Ridwan Shariffdeen]

The current format supported is in smt2, so use --write-smt2s which will
produce a smt2 file


On Tue, Mar 23, 2021 at 6:46 PM Bharat Garhewal <b.garhewal at cs.ru.nl> wrote:

> I used:
>
> klee -write-kqueries --libc=uclibc --posix-runtime --external-calls=all
> --seed-out=file.bout example.bc
> On 23/03/2021 11:43, Ridwan Shariffdeen wrote:
>
> Hi
> What's the Klee command you used
>
> On Tue, Mar 23, 2021, 6:40 PM Bharat Garhewal <b.garhewal at cs.ru.nl> wrote:
>
>> 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 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 <b.garhewal at cs.ru.nl>
>> 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),
>>> 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
>>> klee-dev at imperial.ac.uk
>>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>>>
>>
-------------- next part --------------
HTML attachment scrubbed and removed