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

[Bharat Garhewal]

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 
> <mailto: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
>>     <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 <mailto: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
>>         <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 <mailto:klee-dev at imperial.ac.uk>
>>         https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>>         <https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
>>
-------------- next part --------------
HTML attachment scrubbed and removed