search

runtimeverification / k

K Framework Tools 7.0
BSD 3-Clause "New" or "Revised" License
450 stars 149 forks source link

Generate binary KORE directly from bison #2519

Closed Baltoli closed 2 years ago

Baltoli commented 2 years ago

The binary KORE pipeline still has one step where textual KORE is required - parsing a program from surface syntax into a KORE term requires the use of --gen-glr-bison-parser and the corresponding parser_SORT executable.

Currently, this isn't a big bottleneck (as the motivating example from the C semantics comes from the concatenation of several individual terms into a single translation unit). However, if a semantics were to generate a particularly huge individual program term, parsing the textual KORE into binary after the initial parsing step would be a problem.

ehildenb commented 2 years ago

@dwightguth and @Baltoli is this still an issue? If not, please close.

Baltoli commented 2 years ago

We don't have any real need to do this; it's unlikely to become a bottleneck. Happy to close.