[klee-dev] KLEE compiler optimization?

Paul Rubel prubel at bbn.com
Thu Jan 31 15:29:27 GMT 2013


Jonathan Neuschäfer writes:

<snip>

 > > The developer of Cloud9 told me this might be due to KLEE compiler
 > > optimization or some other reason. Is anybody can tell me why?
 > > 
 > > Is there any way I can stop this optimization?
 > 
 > Is klee called with "-optimize" on the command line at some point?


Regarding optimizations I've been down that path lately. Even if the
code is compile without optimization compile flags and you pass in the
-disable-opt argument to the c9-worker there are still some
optimizations made via lib/Module/KModule.cpp, about line 405, as the
bitcode is internalized: InstructionCombining, CFGSimplification,
AggressiveDCE, and globalDCE. I'm sure these speed up the execution
quite a bit but it can make tracing back to source and trying simple
examples more complicated.

I've successfully commented out those 4 optimizations and run
examples. If the other fixes don't work it's an option. 

          Paul





More information about the klee-dev mailing list