Compilation of Unreduced Semantics Sometimes Fails

[sskeirik]

When using the fuzzer using the run-fuzzer.py script, as part of the preparation process, the fuzzer constructs a K definition from the linked SMIR JSON blob and then passes that to the K llvm-backend to be compiled into a native binary.

During the llvm-kompile process, it invokes the Clang linker, lld. This process can balloon to using up to 4GB memory and to using 15-30 minutes. When this happens, the linking process can crash. The exact error that lld prints can vary. We have observed several error messages:

1. a duplicate symbol
2. an undefined symbol
3. an internal table grew too large

I hypothesize that either:

1. there is an issue with lld on very large link jobs or;
2. the unreduced semantics is somehow not processed properly by our toolchain and generates an invalid input to the LLVM backend which causes it to crash.

It's not clear which one is the issue, but --- there appears to be a work-around for this issue.

The prover toolchain also invokes llvm-kompile like above but it first prunes the LLVM kompile input by deleting functions from the SMIR info that appear to be unreachable from the test start symbol.

A simple test where the fuzzer was modified to also perform this reduce step appears to make LLVM kompile work --- this is unsurprising because I believe, in both cases, the same definition.kore is generated.

I will run the modified fuzzer on all tests to check if it completely solves the problem for now and update this issue later with my test results.