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

[Ridwan Shariffdeen]

I'm not much familiar with the kquery format, but you can use smt2 or cvc
formats which will give you the constraints you are looking for. What is
the format your tool expects the constraints in?

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

> Ah, so if I want the constraints while referring to the variable and not
> just the value, we will have to parse the smt2 file?
>
> If so, that will pose a problem for our use-case, since we want to parse
> the constraints and then feed them to our tool.
>
> I suppose I should start digging around in the KLEE source then, any tips?
> :)
>
> Thank you,
>
> Bharat
> On 23/03/2021 11:51, Ridwan Shariffdeen wrote:
>
> 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