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

[Ridwan Shariffdeen]

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