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

[Bharat Garhewal]

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