runtimeverification / runtimeverification/llvm-backend

Abort when trying to execute a hook that is not implemented

Open
#1,211 0 comments 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

code generation wontfix
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

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. 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

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.