HOTFIXES not stuck on uneval.d functions, replacement from path condition

[jberthold]

Indeterminate result for function calls under injections

When the rewrite subject contains a function call under an injection, the function's return sort may be more general than the sort expected by a rewrite rule that is being tried. This shows up as a failing match between two injections in rule LHS and subject. Previous code was declaring this a match failure for the rule but didn't abort the rewrite. The correct behaviour is to abort the rewrite (or to unify, which booster doesn't).
Fixes a problem where booster would return Stuck which then falls back to legacy kore-rpc where progress can be made.

It is still possible for booster to return Stuck when trying to match a function call (because of rule indexing which limits the amount of rules that could possibly apply. An expression with an unevaluated function call will never be rewritten by booster, but a modification of the indexing mechanism and rule selection is left for future work.

Added replacement from path conditions into term evaluation

When the path condition contains equations of the form domain-value ==Int expression, this information should be used to replace any syntactic occurrences of expression by the obviously simpler domain-value (expression should obviously not be another, different, domain value so it must be a function call or a more complex expression).
This holds likewise for ==Bool and for other domain equality operations, ==Int and ==Bool replacements are implemented. The replacement happens after LLVM evaluation but before any other hook or (function or simplification) equation application.

[jberthold]

KEVM and kontrol performance tests were run and showed minimal speedup for the branch version over current master.

[ehildenb]

Some quick questions (for the record):

• My understanding was that we had a soundness issue in rule indexing, where we were not taking into account that a function symbol on an indexed cell should result in * index for that cell. That is not addressed in this PR right?
• When doing the replacement of the expression with the domain value, we don't lose the equality in the side-condition between the two do we? We retain the information that the expression was set equal to the domain value?

[jberthold]

Some quick questions (for the record):

• My understanding was that we had a soundness issue in rule indexing, where we were not taking into account that a function symbol on an indexed cell should result in * index for that cell. That is not addressed in this PR right?

Correct, this issue is not addressed, and will be part of a follow-up PR to index more things and use a better algebra. I had draft code to implement better indexing but there was a bug in it and it aborts too often so I wanted to merge the improvements first.
What currently happens is,

• If the cell with the function symbol is indexed, the index will contain a function symbol as TopSymbol and the request will get Stuck because only rules with * will be tried (the relevant ones will probably not be those). Booster falls back to kore and kore unifies function call and LHS (or is able to evaluate the function call)
• if the cell with the function symbol is not part of the index, the fix here applies, the rewrite is aborted (and booster falls back to kore which unifies or evaluates, same as above)

• When doing the replacement of the expression with the domain value, we don't lose the equality in the side-condition between the two do we? We retain the information that the expression was set equal to the domain value?

We retain all path conditions, we just use some of them to make the term simpler and more concrete.