[klee-dev] Direct Search Towards Assertion

[Paul Marinescu]

Hi
The best you can do is not use -search=dfs. The current default search 
strategy is generally better than dfs and uses a combination of 
randomness and the minimum distance to an uncovered instruction 
(nurs:covnew).

See klee --help for available search strategies (nurs:md2u is another 
candidate).

You should keep in mind however that these search strategies will try 
the shortest static path to an uncovered instruction. If that path 
proves to be infeasible, they're gonna try the next shortest path and so 
on. While your example is fairly straightforward, generating that single 
path may not be.

You may want to search for 'directed symbolic execution'. There are 
several tools (including one based on KLEE on which I worked 
http://srg.doc.ic.ac.uk/projects/katch/) but the general problem is 
undecidable.

Paul

On 10/04/14 09:25, Kirill Bogdanov wrote:
> Hello everyone.
>
> I have a simple example, with the list of symbolic integers, and I am
> searching for the smallest one. At the end of the code I am checking if
> element at position [3] was the smallest one, and assert.
> code:
>
> #define n 10
> int main() {
>
> int a[n];
> klee_make_symbolic(&a, sizeof(a), "a");
>
> int index = 0;
> for (int i = 1; i<n;i++){
> if (a[i] < a[index])
> index = i;
>
> }
> printf("index: %i\n", index);
>
> if (index == 3){
> klee_assert(false);
> }
>
> return 0;
> }
>
> I am running with "-search=dfs" argument. In this example KLEE generates
> 2^(n-1) code paths in the for loop by trying all different combinations
> of input data.
>
> Question: I do not really care to cover all possible code paths in the
> for loop, I only care that the smallest element is not at position=3. I
> expect this assertion to produce constrain something like: a[3] < a[0]
> && a[3] < a[1] etc. Which should be easy to resolve.
> How can I "ask" KLEE to try to trigger this assertion as quick as
> possible at the beginning of the search?
>
> Thank you.
> Kirill
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>