Hello,
I am attempting to symbolically test a program that uses a hash table
and have encountered some performance issues that I do not understand.
I have created a small program that exhibits this behavior. In the
code below, I create a symbolic string, hash that string, and then
assign into a location in a table determined by the hash. I am
running klee from svn (rev: 116946) with llvm-gcc 2.7 as recommended
in the "getting started" guide.
What I have found is that increasing the size of the symbolic hash key
(STRING_SIZE below) results in a drastic increase in execution time.
(Interestingly, increases in the hash table size (TABLE_SIZE)
counterintuitively seem to improve performance in some cases). Memory
usage is fairly constant during execution and the CPU stays pegged
around 100%. While I would have guessed that this was due to an
explosion in set of paths being explored, output from the tool upon
completion indicates that it is not:
KLEE: done: total instructions = 108
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1
Below is the code for the example. I am curious to discover the
reason for this performance behavior and hope to find a workaround to
let me write tests with symbolic hash keys.
Thanks!
Chris Hayden
CODE:
/* Generic hash function (a popular one from Bernstein).
(copied from the redis key-value store) */
unsigned int dictGenHashFunction(const unsigned char *buf, int len) {
unsigned int hash = 5381;
while (len--)
hash = ((hash << 5) + hash) + (*buf++); /* hash * 33 + c */
return hash;
}
#define STRING_SIZE 4
#define TABLE_SIZE 100
int main(int argc, char *argv) {
char symb_str[STRING_SIZE];
klee_make_symbolic(symb_str, sizeof(symb_str), "str");
unsigned int hash = dictGenHashFunction(symb_str, sizeof(symb_str));
int hash_table[TABLE_SIZE];
hash_table[hash % TABLE_SIZE] = 1;
return 0;
}
--
hayden at cs.umd.edu / chayden at gmail.com
http://www.cs.umd.edu/~hayden
