Custom hooked Map externalisation
#363
Conversation
This is a first iteration of the profiling scripts based on the script from #355. Simply run via `scripts/performance-tests-kevm.sh` or `scripts/performance-tests-kontrol.sh` --------- Co-authored-by: Georgy Lukyanov <mail@geo2a.info>
I've noticed we don't kill the servers after running the tests over the feature branch. They will then stay as zombies when we run over `master`. I've already made the same change in the `kontrol`-script.
Term simplifications are cached in a `Map Term Term` while simplifying, and supplied from cache when already present. --------- Co-authored-by: Georgy Lukyanov <georgiylukjanov@gmail.com>
This fixes #319 and hopefully also #298 by newly allowing unification of: * Two maps with multiple fully concrete keys and no "rest" map variable (previously we could only match multiple keys if there was also a "rest of the map" variable) * Map with only concrete keys + "rest" variable with a map of mixed concrete/symbolic keys without a "rest" variable
When an execute request ends with an `Aborted`, `Stuck`, or `Branching` reason, it is usually re-executed with legacy `kore-rpc`. As part of that, the simplifier will run on the input. However, we are _also_ explicitly simplifying the end state of the execute request (and return `Vacuous` if it simplifies to `\bottom`). This additional work is unnecessary as we will anyway get the `\bottom` result back from `kore-rpc` (alas, in a slightly different shape). This saves one round of fall-back to `kore-rpc` and should speed up long-running proofs that have to fall back often due to side condition checking.
Simplification log should show the effect of an LLVM simplification, as well as a cache hit (both only if it changed the term)
geo2a
force-pushed
the
georgy/better-map-internalisation
branch
from
7ab269b to
b50af99
Compare
| , Symbol | ||
| { name = "Lbl'Unds'Int2Int'Pipe'-'-GT-Unds'" | ||
| , sortVars = [] | ||
| , argSorts = [SortApp "SortWrappedInt" [], SortApp "SortInt" []] |
There was a problem hiding this comment.
@geo2a I don't follow why the second argument has sort Int here; in the corresponding definition the second argument has sort WrappedInt? I might be missing something though.
There was a problem hiding this comment.
You're right, and it indeed makes the test I constructed to pass. We have been able to pin-point the problem to the MAP.update hook in the LLVM backend. I'll update the integration tests and also open an issue in the LLVm backend with the somewhat minimized definition and input.
There was a problem hiding this comment.
Remarkable timing; I had also just managed to build and get the same test to pass with the value sort as WrappedInt! Let's take a look at your new minimized example in our meeting this afternoon.
| [ function, total, hook(MAP.unit), | ||
| klabel(.MapInt2Int), symbol, latex(\dotCt{MapInt2Int}) | ||
| ] | ||
| syntax MapInt2Int ::= WrappedInt "Int2Int|->" WrappedInt |
There was a problem hiding this comment.
Here's the production I believe corresponds to the above comment @geo2a
|
Blocked on runtimeverification/llvm-backend#886 |
|
closing in favour of #378 |
Work on #321
Just adding integration tests for now.
I'm struggling to reproduce #321 as the provided bug report unfortunately contains a pre-multy-or LLVM definition. I've requested access to the relevant code bases in order to produce obtain the up-to-date definition.This turns out to be an issue in the LLVM backend; hence, blocked on runtimeverification/llvm-backend#886