Artiweb > Pull Request #3117

Critical changes to the KeY parser/grammer for more performance #3117

Github

Description

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.

Screenshot from 2023-04-15 03-36-14

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.

Screenshot from 2023-04-15 04-03-41

Screenshot from 2023-04-15 04-01-50

For discussing the changes, please refer to the comments on the source code below.

/cc @jwiesler @mattulbrich @unp1

Artifacts