Crucible specs should be required to call `{llvm,jvm,mir}_execute_func`

[sauclovian-g]

Currently, at least for LLVM specs, it's possible to write a spec that doesn't actually call llvm_execute_func to run the function it's specified. In most cases this will result in complaints and failure (e.g. unless the function takes no arguments, it's an error to not provide them), but for sufficiently simple functions the verification will succeed.

It isn't clear whether it's possible to concoct an example that produces an incorrect verification success. It's plausible, but it's not worth chasing after: it's overwhelmingly likely that any spec we see that doesn't actually call the function is a mistake, and it should just be prohibited.

I haven't checked if this is actually the same for JVM and MIR specs, but it would be surprising if it weren't.

[sauclovian-g]

See also #946, which is essentially a different manifestation of the same missing check.

[brianhuffman]

PR #2743 adds the necessary checks for jvm_execute_func. We still need to add similar checks for llvm_execute_func and mir_execute_func.

[sauclovian-g]

#947 should also be crossreferenced here.