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

[Bharat Garhewal]

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 
> <mailto: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 <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