[Bug] [kompile] - Frontend loops forever on certain syntax when passing --gen-[glr-]bison-parser

runtimeverification / k

K Framework Tools 7.0

BSD 3-Clause "New" or "Revised" License

450 stars 149 forks source link

[Bug] [kompile] - Frontend loops forever on certain syntax when passing --gen-[glr-]bison-parser #1607

Closed hjorthjort closed 2 years ago

hjorthjort commented 4 years ago

K Version

RV-K version 1.0-SNAPSHOT
Git revision: 0aa62f7
Git branch: UNKNOWN
Build date: Tue Oct 13 12:24:05 UTC 2020

Description

Running kompile with --gen-[glr-]bison-parser seems to never result in a bison file being generated, and the frontend doesn't terminate.

Input Files

I haven't managed to get this in minimized form yet. But it is reproducible in https://github.com/kframework/wasm-semantics on the hjorthjort branch.

Reproduction Steps

Clone the KWasm semantics, then:

git submodule update --init --recursive
make deps
make KOMPILE_OPTS="--gen-bison-parser"

Expected Behavior

It's possible (likely) that the KWasm semantics are not suited for Bison parsing as it stands currently, so we expect Bison failures. However, we expect there to be a Bison file produced in the temp directory (.kompile-...) which we can expect, or to Bison to report errors.

Instead, it seems the call to generate the Bison file never terminates.

80955.jstack.txt

radumereuta commented 4 years ago

I managed to trace the problem to somewhere here https://github.com/kframework/k/blob/master/kernel/src/main/java/org/kframework/parser/inner/kernel/KSyntax2Bison.java#L190

for (Sort sort : iterable(module.allSorts())) -> 2152
  for (Production prod : Optional.ofNullable(prods.get(sort)).orElse(java.util.Collections.emptyList())) -> subsets from over 70.000 productions

That's a lot. So I think it does finish but it's just going to take a long time.

The Bison parser is meant to be used to parse programs, but in the list of productions I see everything from domains.md included. I think that's the first thing that needs to be sorted.

Let me know if you need help with that.

ehildenb commented 4 years ago

Suggestions:

Seems like we need to run a Java profiler on the code which generates the Bison parser, and see if any of the code there can be optimized.
In the Java kast parser, rassoc lists are really slow, but lassoc lists are 1 order of magnitude faster. So potentially could look at optimizing the bison parser in similar ways? Should we just make user-defined lists be left-associative for parsing then (then we lose cons-list style matching)? Could try writing grammar to be left-recursive, but then change tree-structure afterwards (what to do with ambiguities?).

ehildenb commented 4 years ago

@dwightguth should have a chance at some point to profile this.

ehildenb commented 4 years ago

Another possibility: maybe we can disable the slow code when doing just LR parsing (and only enable it when doing GLR parsing).

dwightguth commented 2 years ago

This is probably fixed. If you're still having issues feel free to reopen though.