Hi Thurston,
I think what is taking so long is the object resolution phase. Unlike
our previous system EXE, KLEE is not doing any pointer tracking, and is
trying instead all possible base objects when you index myFunctions by
the unconstrained "instr" variable. You can find more details in our
EXE and KLEE papers.
If you constrain "instr" to be between 0 and 399 after making it
symbolic, KLEE should behave similarly to when you use the switch statement.
Best,
Cristian
On 08/28/2012 09:42 PM, Thurston Dang wrote:
> Hi,
>
> I've been running klee on an emulator, which has code similar to:
> myFunctions [0] = &function0;
> myFunctions [1] = &function1;
> ...
> myFunctions [399] = &function399;
> klee_make_symbolic(&instr, sizeof(instr), "instr");
>
> int (*myFunction)(void) = myFunctions [instr];
> int result = (*myFunction) ();
> and it takes surprisingly long to run (e.g., with an array of size
> 400, it takes almost 3 hours).
> From the queries, it appears that klee is trying possible values of
> 'myFunction', and then working backwards to find the corresponding
> symbolic array index.
>
> One workaround has been to use switch statements e.g.,
> switch (instr) {
> case 0:
> myFunction = function0;
> break;
> case 1:
> myFunction = function1;
> break;
> ...
>
> Is there a more elegant or efficient solution? One which minimizes
> changes to the emulator code would be particularly useful.
>
> The most related thread I've found in the archives is
> http://www.mail-archive.com/klee-dev@keeda.stanford.edu/msg00014.html,
> though I view my example as "reading a concrete object at a symbolic
> offset" (and hence shouldn't be slow).
>
> Thanks,
> Thurston
> _______________________________________________
> klee-dev mailing list
> klee-dev@keeda.stanford.edu
> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
>
_______________________________________________
klee-dev mailing list
klee-dev@keeda.stanford.edu
http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
