Hi, All,
Looks like there is caching somewhere in Klee/SMT even without options
"--use-cache", "--use-cex-cache".
Consider an example when some SMT-time-consuming operation is run twice:
with the same symbolic data: it takes *time* to pass all the
paths
with two different symbolic data's: it takes 2* *time ..*
More details: example:
#include <stdio.h>
#include "klee/klee.h"
void doLongOperation(char c) {
char buf[512];
//any SMT consuming operation: here snprintf from uClibc is used
snprintf<http://www.opengroup.org/onlinepubs/009695399/functions/snprintf.html>
(buf,
sizeof<http://www.opengroup.org/onlinepubs/009695399/functions/sizeof.html>
buf, "%llu\n", (unsigned long long)c);
}
int main(int argc, char** argv) {
klee_debug(">> start 1..\n");
char symChar1;
klee_make_symbolic(&symChar1,
sizeof<http://www.opengroup.org/onlinepubs/009695399/functions/sizeof.html>
symChar1, "char1");
klee_assume(symChar1 < 0 && symChar1 > -3); //not to make you
crazy waiting for the end..
doLongOperation(symChar1);
klee_debug("<< end 1. start 2..\n");
char symChar2; //comment to
observe caching
klee_make_symbolic(&symChar2,
sizeof<http://www.opengroup.org/onlinepubs/009695399/functions/sizeof.html>
symChar2, "char2");//..
klee_assume(symChar2 < 0 && symChar2 > -3); //..
doLongOperation(symChar2); //..
// doLongOperation(symChar1); //uncomment to observe caching
klee_debug("<< end 2\n");
return 0;
}
Started with the command:
../Release/bin/klee \
--output-dir klee \
--posix-runtime --libc=uclibc --init-env \
--coverable-modules files.coverable \
--simplify-sym-indices \
--all-external-warnings \
--output-module \
--disable-inlining \
--optimize \
--allow-external-sym-calls \
--only-output-states-covering-new \
--max-instruction-time=3600. \
--max-memory-inhibit=false \
experiments.o
And here is the output:
the first experiment (with two different symbolic chars):
>> start 1...
{ long time }
<< end 1. start 2...
{ long time }
end 2
the second experiment (with the same symbolic char):
>> start 1...
{ long time }
<< end 1. start 2...
end 2 //*it takes no time to calc the second call*
*
*
*
*
*Could anybody comment such behaviour?*
*
*
*Thanks.*
*
*
*--*
*Kind regards, *
*Ayrat Khalimov,*
*Ulianovsk, Russia*
*
*
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20110112/79b9cab3/attachment.html
