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

[Cristian Cadar]

Hi Laszlo,

There is no optimal code style for symbolic execution, although 
sometimes the style can significantly influence performance.  There is 
some research on these topics (e.g., estimating constraint solving 
performance, understanding the impact of program transformations in 
symbolic execution), but it is still far away from the kind of cost 
model you are looking for.

Best,
Cristian

On 02/07/2020 18:27, Nemeth, Laszlo wrote:
> 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
> 
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>