Critical changes to the KeY parser/grammer for more performance #3117
This PR brings restructuring of the KeY's grammar KeYParser.g4
for more performance.
Some of the changes are critical as they change the grammar, and need to be discuss.
The current situation is as follows. All given benchmarks given on our biggest Key-file javaRules.key
. Parse time should be treated carefully, as JIT and caching effects have critical.
You see a lots of ambiguities and sometimes high maximal lookahead (max. 105).
The problem lies more in the primitives and some stupid rules.
The following is possible, depending on the severity on changes.
For discussing the changes, please refer to the comments on the source code below.
/cc @jwiesler @mattulbrich @unp1
Artifacts
- 27. May 2023 18:23 (7992.92 kB large)
- 27. May 2023 18:09 (15117.03 kB large)
- 18. Apr 2023 03:02 (10786.22 kB large)
- 15. Apr 2023 02:15 (170.12 kB large)