Klee runs much faster on file without global variables

[ThanhVu (Vu) Nguyen]

Hi, I have a relative small file (<200 loc's) which has about 15 global
variables. Running klee on this file takes very long time, over 15 mins,
at which point I just manually kill the process. I then manually convert
all these global variables into local (by simply passing them to every
function call) then rerun Klee on the modified file. This time it takes
Klee just less than a min to finish running.

is such performance expected for using local vs global variables ? If it
is the case then I will try to convert global vars to local ones whenever
possible before running Klee.

I compile the object file with the flags --optimize -emit-llvm -c and run
klee on the resulting object file with the flags
"--allow-external-sym-calls -optimize". Are there other relevant flags I
should consider ? Also if interested I can send the file I use for this
experiment.



Vu,

[Martin Nowack]

Hi Vu,

Sounds interesting. Can you send the example or better even a stripped-down version of the original and the changed version?

What kind of data types are the globals?
How do you provide them as an argument - call by value, call-by-reference?

Thanks a lot,
Martin

Hi, I have a relative small file (<200 loc's) which has about 15 global variables. Running klee on this file takes very long time, over 15 mins, at which point I just manually kill the process. I then manually convert all these global variables into local (by simply passing them to every function call) then rerun Klee on the modified file. This time it takes Klee just less than a min to finish running.
is such performance expected for using local vs global variables ? If it is the case then I will try to convert global vars to local ones whenever possible before running Klee.
I compile the object file with the flags --optimize -emit-llvm -c and run klee on the resulting object file with the flags "--allow-external-sym-calls -optimize". Are there other relevant flags I should consider ? Also if interested I can send the file I use for this experiment.
Vu,
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

---------------------------------------------------
Martin Nowack
Research Assistant

Technische Universität Dresden
Computer Science
Institute of Systems Architecture
Systems Engineering
01062 Dresden

Phone: [phone]
Email: martin_nowack-***@public.gmane.org
----------------------------------------------------