Experiment to evaluate concrete terms in booster instead of llvm library

[jberthold]

Fully concrete terms are currently sent to the LLVM backend library, which may (or may not) represent a considerable fraction of execution time. Several ideas combined may get us some performance improvements:

1. Implement a broad selection of hooked functions for frequently-used data types
2. Decide in some way dynamically how and whether to call the LLVM library:

• Export hooks instead of term API (plus hooked-type API) from LLVM library.
  • Hopefully thread-safe by construction
  • will keep calling marshalling more often, but hopefully very efficient small functions
• be more semantics-independent: not recompiling a specific definition but rather have a generic llvm library
  • amounts to exporting the hooks when taken to the extreme
  • however, there may be cases of generic functions doing useful work on symbolic input
• hook analysis a) analyse function equations for which hooks they use (transitively, bottom-up) b) synthesize term attribute to get a list of hooks c) only call llvm if there are hooks not implemented in booster

[ehildenb]

I think the initial idea is just that we can avoid calling the LLVM backend in many cases, which means that the global lock on the LLVM backend shared library won't be as big of a blocker to concurrency.

In particular, many side-conditions on rules probably may be discharged to true/false with just a handful of equation applications. So we could do something like, 10 rounds of equation application on concrete terms before invoking the LLVM backend, so that for very long simplifications like computeValidJumpDests we still fallback, but for very short ones we just discharge them directly.

Of course, it's still OK to just use LLVM backend for all hooks, and see which ones are most prominent. My guess is that Int and Bool hooks will dominate the remaining requests we have to make, so we can implement just the concrete cases of those hooks (since that's all we'd be using the LLVM backend for anyway), and avoid those calls.

We really should strive for the simplest and easiest thing that makes us call less into LLVM (to avoid the global lock on the shared library). Doing more complicated analysis of hooks/etc... to produce a specialized binary seems pretty unnecessary right now.

[jberthold]

My first experiments with less LLVM and more internal hooks unfortunately shows significantly longer runtimes in KEVM tests.

[jberthold]

Conducted another experiment with a special simplifier for rewrite rule side conditions, which would only call LLVM when no equations are applicable, in combination with implemented hooks for Bool and Int operations. Code lives on branch 551-EXPERIMENT_simpler-side-condition-simplifier .

KEVM and kontrol tests on the branch perform on par with master - i.e., we do not seem to get any speedup from this change. We could further analyse the execution with this branch to find out whether the change reduces the amount of LLVM calls at all, and if not, add more hooks to be able to reduce them and re-measure.