Generate Bison parsers with `kbuild`

[geo2a]

The kbuild tool should be able to generate Bison parsers.

See this PR to mir-semantics for motivation: https://github.com/runtimeverification/mir-semantics/pull/66

Interface

The target should look something like this:

[parser.mir]
syntax-module = "MIR-SYNTAX"
sort = "Mir"
parser-type = "glr"

That should generate the parser_Mir_MIR-SYNTAX binary.

Implementation

To fulfill the target, kbuild should encapsulate the following call to kast (I currently implement it a pytest fixture):

@pytest.fixture(scope='session')
def mir_parser(llvm_dir: Path) -> Path:
    path_to_mir_parser = llvm_dir / 'parser_Mir_MIR-SYNTAX'
    try:
        kast_command = ['kast']
        kast_command += ['--definition', str(llvm_dir)]
        kast_command += ['--module', 'MIR-SYNTAX']
        kast_command += ['--sort', 'Mir']
        kast_command += ['--gen-glr-parser']
        kast_command += [str(path_to_mir_parser)]
        run_process(kast_command)
        return path_to_mir_parser
    except CalledProcessError as err:
        raise ValueError("Couldn't generate Bison parser") from err

[nishantjr]

It would be nice to have a fallback additional-args parameter taking parameters not yet supported by kbuild, for example, I'd also like LLVM's --enable-search to be passed to kompile.

[tothtamas28]

It would be nice to have a fallback additional-args parameter taking parameters not yet supported by kbuild

It's a deliberate choice such a parameter is not exposed (not only on kbuild, but also on functions in pyk.ktool). We used to have that option e.g. on kompile, and it turned out to be such a convenient workaround that people just used that instead of opening an issue, preventing tooling to evolve in the right direction.

[ehildenb]

@tothtamas28 I guess we'll need to build the bison parsers to try inner parsing anyway?

[tothtamas28]

I guess we'll need to build the bison parsers to try inner parsing anyway?

I think so.

Right now a kbuild target is a kompiled definition specifically, but it's a good idea to extend that notion to other resources (native bindings, parsers, etc.)