Hi Ayrat,
Some KLEE options are turned on by default. In particular, both
--use-cache and --use-cex-cache are on by default. If you disable them
(--use-cache=false --use-cex-cache=false), I think both operations will
take a long time.
It would be nice to have a way to display the default values on "klee
--help"
Best wishes,
Cristian
On 12/01/11 20:52, Ayrat Khalimov wrote:
> 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*
> *
> *
