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 <[email protected]> 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 >> [email protected] >> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev >> >> > _______________________________________________ > klee-dev mailing list > [email protected] > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
