krun throw an error instance of `std::out_of_range`

[yanliu18]

I attempted to implement the builtin operations using identifier tokens directly such that we can remove syntax ambiguities. The new way of implmentation is here: https://github.com/runtimeverification/mir-semantics/blob/c558fe6ce6cd72c351f714e991ab2726c1d99256/kmir/k-src/mir-rvalue.md?plain=1#L89-L105

kmir parse is successful in returning the right tokens, however kmir run return an error:

terminate called after throwing an instance of 'std::out_of_range'
  what():  map::at
/nix/store/3907sdalv6p3glw0azaq4xjh02s0a0qk-k-6.0.0-8dd443af390df69efb5acbeb58ca7eef39af7238-maven/bin/../lib/kframework/k-util.sh: line 114: 10335 Aborted                 (core dumped) "$@"
[Error] krun: kore-expand-macros 
/home/emma/.kbuild/mir-semantics/48ef824/target/v6.0.0/llvm 
/tmp/.krun-2023-06-29-13-36-58-qrMWkXUVb8/tmp.in.fPPynx5W5c

The original implemtation at master branch has no such error, I wander why.

Process to reproduce the error:

On branch 90-make-sure-that-all-tokens-in-the-semantics-are-whitelisted-as-identifiers, under director mir-semantics/kmir

poetry run kbuild kompile llvm
poetry shell
kmir run --definition-dir $(kbuild which llvm) src/tests/integration/test-data/handwritten-mir/execution/arithm-simple.mir --output pretty

Checking K version

krun --version

returns

cat: /nix/store/3907sdalv6p3glw0azaq4xjh02s0a0qk-k-6.0.0-8dd443af390df69efb5acbeb58ca7eef39af7238-maven/lib/kframework/git-describe.out: No such file or directory
K version:    v6.0.0
Build date:   Wed Jun 28 00:31:31 AEST 2023

[Baltoli]

The error is happening during macro expansion; I'm not immediately sure why that's the case but I'll take a look at reproducing the problem.

[Baltoli]

Steps to take for debugging this:

• Full clean build (i.e. from a fresh git checkout, or having wiped out all derived products)
• Isolate the invocation of kore-expand-macros that's causing the issue - need to look at how kmir handles options + verbosity to figure this out
• Run in a debugger to work out where the crash is
• LLVM-backend specific investigation (i.e. what part of the AST is breaking the macro expander)

[Baltoli]

The issue here is that the GLR parser for the MIR syntax has not been regenerated between builds. The branch relevant to this PR changes the production that Add(const 1_usize, const 1_usize) would parse to; previously, it would have been _(_, _)_Identifier_Operand_Operand, but it's now _(_, _)_BinaryOpName_Operand_Operand.

When the stale parser is invoked, it will generate the old label, and the macro expander then breaks because that label doesn't exist in the semantics. The error message could admittedly be friendlier in this case!

Running kbuild clean inside your Poetry shell should address this.

[Baltoli]

The problem happens because of this code: https://github.com/runtimeverification/mir-semantics/blob/e0d53af3b5d6a642a6d5d85317d88774767f55b7/kmir/src/kmir/kmir.py#L30-L32

It will fail to generate the GLR parser if that file already exists in the Pyk kbuild cache; I believe that kbuild now supports a TOML config option to handle the generation of the parser in the build system: https://github.com/runtimeverification/pyk/blob/49d861944bad260be137f68f4adc37b360e25771/src/pyk/kbuild/project.py#L132

[yanliu18]

@Baltoli Thanks, kbuild clean works. And your suggestion are accepted to put on our list. Thanks.