[klee-dev] Klee runs much faster on file without global variables

Martin Nowack martin_nowack at tu-dresden.de
Fri Feb 14 07:15:15 GMT 2014


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

On 14 Feb 2014, at 04:50, ThanhVu (Vu) Nguyen <tnguyen at cs.unm.edu> wrote:

> 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
> klee-dev at imperial.ac.uk
> 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: +49 351 463 39608
Email: martin_nowack at tu-dresden.de
----------------------------------------------------

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 496 bytes
Desc: Message signed with OpenPGP using GPGMail
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20140214/26a1e023/attachment.sig>


More information about the klee-dev mailing list