Constant folding of Int, Float, String, and Bool

[dwightguth]

This PR adds a compilation phase (enabled only on the llvm and haskell backend for simplicity's sake) which will evaluate at compile time hooked expressions over integers, floats, strings, bools, and identifiers to their ultimate value if they contain no variables or side effects.

This is done by means of a simple set of hook implementations provided as part of ConstantFolding.java which desugar each string token to its underlying domain-specific implementation, then reflectively invoke the right hook based on the hook attribute, then reconstruct the resulting token. It does this recursively, evaluating arguments, and then evaluating the function itself if the arguments have evaluated to a token.

Formally speaking, it will evaluate an expression if all of the following statements are true:

1. The term is nested under the right side of a rewrite operator.
2. The term is a KApply whose KLabel is a hooked function that is not tagged with the impure attribute.
3. The hook namespace of the hook is one of STRING, BOOL, INT, or FLOAT.
4. All of the arguments to the function are KTokens or can be constant folded to a KToken.

If this is the case, the compiler will attempt to fold the expression and if it fails, either because no constant-folding hook implementation was provided, or because the function is not defined on those inputs, it will report an error.

This is not ready yet, but the final draft of the PR will contain Java unit tests for each of the hook implementations, as well as several integration tests testing the functionality end to end. Right now I'm just trying to get it to a point where it passes CI.

[ehildenb]

Please provide times at make -j1 for tests/regression-new, pl-tutorial make, evm, c, and either Algorand or elrond.

[radumereuta]

1. Can you also add some integration tests?
   One that passes, and has simple (ex: 1+2) and complex rules (1+2*5 + "abc").
   One definition that goes into checks and outputs some errors thrown by the new functions.
2. Is there an issue you should reference in this PR?

[dwightguth]

I addressed Radu's comments. I will get the performance numbers as soon as I can, but I wanted to take care of the requested code changes first.

[ttuegel]

The implementation of the hooks appears the same as the Haskell backend, where the backend implements the hook.

[radumereuta]

Not really happy about the look of the double location error message, but I agree this can be addressed in another PR.

[dwightguth]

This is a placeholder post where I will add statistics relating to the performance details Everett has asked for as I compute them. Don't assume that what you see here is everything I am collecting until I explicitly let you know that I've finished computing everything.

On master branch:
tests/regression-new, time to run make krun -k after having run make kompile -k. Measured using time, includes overhead: 18m44s.
pl-tutorial. time to run make krun after having run make kompile and removing all java-backend definitions. Measured using time, includes overhead: 6.1s.
evm, time to run make test-bchain, measured using perf, only includes time spent in backend: 18m
c, time to run make test-llvm, measured using perf, only includes time spent in backend: 39s.
algorand, time to run make test, measured using perf, only includes time spent in backend: 1.2s.

On folding branch, same methodology:
tests/regression-new: 18m2s
pl-tutorial: 6.6s
evm: 18m
c: 37s
algorand: 1.5s

[ehildenb]

Let's wait on #1921 so that this goes into #1697

[ehildenb]

Looks good to me, only concerns are:

• Should we add this code (which introduces complexity and possibly bugs) if there is no demonstration that it actually improves performance?
• Should it be an error for a hooked function in INT, BOOL, STRING, or FLOAT to not have a constant folding implementation? That will make adding hooks down the line harder, if we find there is something we have a hook for in the backends but don't want to implement the same hook in Java.

[radumereuta]

Someone had a good idea. If we add an option to enable/disable this step during kompile then we offer developers a way of avoiding possible bugs.

[dwightguth]

I think the main argument at this time in favor of merging this PR is that it will improve the readability of macros in our code. Instead of writing something like:

rule pow256 => 115792089237316195423570985008687907853269984665640564039457584007913129639936 [macro]

We can instead write:

rule pow256 => 2 ^Int 256 [macro]

And it will be functionally identical, because constant folding will expand the latter to the former automatically.

That being said, just because it doesn't substantially improve performance currently doesn't mean it's not still a good optimization to have. Consider for example EVM. Previously, we introduced macros like pow256 because they were quantities being used by rules in the semantics where 2 ^Int 256 was being used previously in the semantics to the detriment performance. If we had had this optimization then, we would have seen improvements in performance as a result of this. I think some part of the fact that we don't see significant improvements from this change must be attributed to the fact that our K developers have been deliberately working around the lack of just such an optimization by manually optimizing constant expressions themselves. Doing it automatically is more efficient and less error-prone.