[klee-dev] Counter Example Cache Slows Down KLEE

[YJKim]

Dear KLEE team,

I am Young Joo Kim, a graduate student in KAIST, South Korea.  I found that
the
counter example cache slowed down KLEE significantly in our experiments.
Would
you explain why the counter example cache can slow down KLEE significantly?

For example, in the attached bubble sort example, the counter example cache
slowed down the testing 7 times slower than when we disabled the counter
example cache by modifying the KLEE code.  We used DFS strategy, uclibc for
C standard library, and POSIX  runtime option for symbolic file model.
See the detailed info below:

<Not using counter example cache>
total execution time : 4834 sec
solve time : 4689 sec
# of total queries : 278948
# of generated tests : 40320
-----------------------------------------------------
<Using counter example cache>
total execution time : 35686 sec
solve time :  35483 sec
cex cache time : 35454 sec
# of total queries : 71607
# of generated tests : 40320

We found that counter example cache also slowed down other target programs
including
libexif (13585 LOC); detailed information on testing libexif is as below :
(with --max-time=1800 and we modified KLEE not to terminate before
completion of the test case generation).

<Not using counter example cache>
total execution time : 3795 sec
solve time : 3366 sec
# of total queries : 70707
# of generated tests : 2188
------------------------------------------------------
<Using counter example cache>
total execution time : 11359 sec
solve time : 11318 sec
cex cache time : 11315 sec
# of total queries : 10467
# of generated tests : 39

Thank you very much for your help

Sincerely
-Youngjoo Kim


-- 

--------------------------------------------------
Young Joo Kim, M.S. Candidate
    PSW Lab CS Dept. KAIST
373-1 Guseong-dong, Yuseong-gu
  Daejon, South Korea (305-701)
      http://pswlab.kaist.ac.kr
--------------------------------------------------

#include <klee/klee.h>

#define ARRAYSIZE 8
int main(){
    int arr[ARRAYSIZE] = {0,};
    klee_make_symbolic(&arr, sizeof(arr), "arr");

    int i, j;
    int tmp;
    int n = ARRAYSIZE;
    if (n <= 1) return;

    i = 1;
    do
    {
        for (j = n - 1; j >= i; --j)
        {
            if (arr[j-1] > arr[j])
            {
                tmp = arr[j-1];
                arr[j-1] = arr[j];
                arr[j] = tmp;
            }
        }
    } while (++i < n);
}
_______________________________________________
klee-dev mailing list
klee-dev@keeda.stanford.edu
http://keeda.Stanford.EDU/mailman/listinfo/klee-dev