-
Notifications
You must be signed in to change notification settings - Fork 23
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.