runtimeverification / runtimeverification/llvm-backend
Abort when trying to execute a hook that is not implemented
Nobody has claimed this yet.
- Dominant language
- C++
- Stars
- 43
- Forks
- 22
- PR merge metrics
- No merged PRs in 30d
Description
Description
Due to a mismatch between the versions pulled by Nix on the K frontend CI, we discovered that the LLVM backend can throw an Abort trap if we create a K rule with a hook that has not been implemented yet. What happens under the hood is that we try to create a function call to a function name we don't recognize as part of the standard semantics. We can also experience a segmentation fault if we attempt to create a rule with a hook that isn't from a K built-in module and isn't defined. In that case, we'll create a function call without a definition, which causes this error when it's called.
Below is the trace for the first scenario. In this case, the error happened at kompile time:
k> make[1]: Entering directory '/private/tmp/nix-build-k-7.1.0-25fca84d2f03388b9662b6c5d7d554866bd47657-test.drv-0/source/tests/regression-new/mint-llvm-4'
k> /nix/store/d10nl5c6gkhsrg3g5x428ljvlnnn78jf-k-7.1.0-25fca84d2f03388b9662b6c5d7d554866bd47657/bin/kompile --syntax-module TEST --no-haskell-binary --no-exc-wrap --type-inference-mode checked --backend llvm test.k --output-definition ./test-kompiled
k> MINT.bytes2MInt
k> /nix/store/d10nl5c6gkhsrg3g5x428ljvlnnn78jf-k-7.1.0-25fca84d2f03388b9662b6c5d7d554866bd47657/lib/kframework/../../bin/../lib/kllvm/scripts/utils.sh: line 25: 17885 Abort trap: 6 "$@"
Error: or] Critical: llvm-kompile returned nonzero exit code: 134
k> Examine output to see errors.
k> make[1]: *** [../../../include/kframework/ktest.mak:53: test-kompiled/timestamp] Error 113
k> make[1]: Leaving directory '/private/tmp/nix-build-k-7.1.0-25fca84d2f03388b9662b6c5d7d554866bd47657-test.drv-0/source/tests/regression-new/mint-llvm-4'
k> make: *** [../../include/kframework/ktest-group.mak:21: mint-llvm-4] Error 2
For the second behavior, we would only see the segmentation fault at kruntime.
Contributor guide
No contributing guide indexed for this repository
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Research direction
Start with the regression scenario in tests/regression-new/mint-llvm-4 and reproduce it with kompile using the LLVM backend. Trace the failure from llvm-kompile for an unimplemented hook and from kruntime for an undefined hook. Done means both cases report a controlled error instead of aborting or segfaulting, with regression coverage for the reported scenarios.
Written by the indexing model from the issue text.
Assessment
- Tech stack
- cpp
- Domain
- compilers
- Issue type
- Bug
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Activity status
- Stale
- Clarity
- Needs clarification
- Newbie friendliness
- 35/100