[klee-dev] Limiting/Guiding KLEE exploration

[Breno Miranda]

Dear Cristian,

Thank you very much for clarifying. I appreciate your help on this.

If I may, I have a follow up question regarding mixing concrete and
symbolic arguments, and using *klee_assume* at the same time.

Sticking with the *grep* example, the argument *-B num* defines how many
lines should be printed before each match. Let's say that I want to
constrain the values of *num* to be between 1 and 5. It is possible to do
that using the following code (In the code, when proceeded by -B, num maps
to the variable *out_before*):

klee_make_symbolic(&out_before, sizeof(out_before), "out_before");
> klee_assume(out_before > 0 & out_before < 6);


Now, if I run KLEE mixing concrete and symbolic arguments (e.g.: *klee
./grep.bc text list.txt --sym-args 0 2 2*) it may generate test cases like
this one:


ktest file : './klee-last/test000032.ktest'
> args       : ['./grep.bc', 'text', 'list.txt', '-sym-args', '0', '2', '2']
> num objects: 4
> object    0: name: 'n_args'
> object    0: size: 4
> object    0: data: 1
> object    1: name: 'arg0'
> object    1: size: 3
> object    1: data: '-v\x00'
> object    2: name: 'model_version'
> object    2: size: 4
> object    2: data: 1
>
>
> *object    3: name: 'out_before'object    3: size: 4object    3: data: 2*


Is it possible to replay this test case in the "original" (not
instrumented) code in a way that it considers the value of the variable
"out_before"? In other words, I would like this test case to be equivalent
to *./grep.exe text list.txt -v -B 2*, but instead, it is equivalent
to *./grep.exe
text list.txt -v* when replayed as it does not consider the value of
"out_before".

What is the proper way of using *klee_assume* such that the generated test
cases can be properly replayed in the original code?

Thank you in advance for your attention.

I look forward to hearing from you.

--
Yours sincerely,
Breno Miranda

On Wed, Nov 26, 2014 at 11:34 AM, Cristian Cadar <c.cadar at imperial.ac.uk>
wrote:

> Hi Breno,
>
> You can mix concrete and symbolic arguments (e.g., klee prog.bc -E
> --sym-args 0 1 4), so part of what you want to achieve is easy.  You can
> constrain individual bytes with klee_assume() or similar constructs, but
> there is no command-line functionality for this.
>
> Best,
> Cristian
>
> On 25/11/14 23:18, Breno Miranda wrote:
>
>> Dear All,
>>
>> I'm performing some tests on *grep* using KLEE and I have one question
>> regarding test case generation.
>>
>> I'm aware of the arguments *grep* accepts (for example, let's assume
>> that this string contains all the command-line arguments accepted on a
>> given version of grep: *A:B:CEFGHVX:bce:f:hiLlnqsvwxyUu*) and If I run
>> KLEE via command line (for example: klee --libc=uclibc --posix-runtime
>> --only-output-states-covering-new ./grep.bc -sym-args 0 2 2) it will
>> generate test cases to the majority of(if not to all) the accepted
>> parameters (this is expected because KLEE will do the best to achieve
>> "full" path coverage).
>>
>> However, let's assume that I'm interested in a *specific use case* of
>> grep. I want, for example, to explore extended regular expressions
>> (*-E*) and some tweaks on the output are allowed, which means that
>> I'm interested only in a subset of the accepted parameters (e.g.:
>> *EHce:f:hiLlnqsvwx*).
>>
>> *Is there a way I can direct/guide KLEE exploration, and consequently,
>> test case generation to focus on the parameters I'm interested in via
>> command-line?* I believe that the answer is *no* but, because KLEE has
>> so many options available, I would like to hear from the experts in this
>> list.
>>
>> I'm aware that *klee_assume* can be used to "limit"/guide KLEE and it
>> could be applied in the scenario above, but I am curious about what my
>> options would be using command-line.
>>
>>
>> I look forward to hearing from you.
>>
>> --
>> Yours sincerely,
>> Breno Miranda
>>
>>
>> _______________________________________________
>> klee-dev mailing list
>> klee-dev at imperial.ac.uk
>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>>
>>
> _______________________________________________
> 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