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@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
