[klee-dev] code style for easy, efficient symbolic execution

[Nemeth, Laszlo]

Hi,

I'm using klee to check various properties of models. When generating the C representation I have two options:

  1.  A bunch of global declarations. This is the current approach, and pretty easy to generate.
  2.  A more object-oriented way: state is local to components and components communicate via messages (function calls with parameters).

The models are large, my generated files are 10-15k lines. And running them takes about four weeks on the hardware available to me, which isn't really acceptable. I've already run test to determine if the number of symbolic variables or the size of those domains are the problem. When the domains are constrained (klee_range(0, 2) instead of klee_range(0, 65535)), there is a speedup but negligible. I have models with a few hundred symbolic variables.

Question to someone knowledgeable about klee's internals: which representation would be easier (resulting in faster execution) for klee to process?

Or in more general terms, does klee have some sort of a cost semantics? Should I generate loops or recursion? As far as I can tell, aggressive compiler optimizations are switched off in the Makefile for clang, is it worth trying to generate inlineable code, ie a trade-off between function calls and code size?

Insights, pointers to papers are much appreciated.
Thanks,
  Laszlo

-------------- next part --------------
HTML attachment scrubbed and removed