Work less, work better. Experiments tend to show it is a good way to increase the productivity. So, no shiny new feature today, but we shipped some improvements that may speed up the symbolic exploration!
On the agenda:
- take advantage of the incremental solving mode (
-sse-engine multi-checks); - welcome the IR-level sub-expression elimination pass (
-sse-cse).
Overall, symbolic exploration spends most of its time in constraint solving.
Besides, BINSEC used to open a new solver session for each issued query.
But, let us now give a try to the incremental mode of SMT solvers. Within the multi-checks engine variant, BINSEC compares each new query with the previous one. If the latter is a parent of the former – which often happens with the depth first search strategy – BINSEC holds the session, both saving the setup time and thriving the prior solver knowledge.
Less usual, but when the emulation speed becomes the exploration bottleneck (e.g. France CyberSecurity Challenge licorne), you can now activate the common sub-expression elimination pass to optimize the BINSEC intermediate representation and, hence, reduce the number of processed micro-instructions.
Also, as a side announcement, we opened the Discussions section in the GitHub repository. Feel free to come and get help on how to use BINSEC.
Have a nice day :-)