[circt-bmc] Correct signature of generated printf

[bryceberger]

lib/Tools/circt-bmc/LowerToBMC.cpp generates a printf stub with (previously) the signature (ptr, ...) -> void. lib/Conversion/SMTToZ3LLVM/LowerSMTToZ3LLVM.cpp looks up a function named printf, and expects the signature to be (ptr, ...) -> i32. Because these types are not the same, circt-bmc crashes (but only when invoked with --print-solver-output).

Because the (ptr, ...) -> i32 signature is correct, this changes the generated stub to have that type.

Fixes #8411

[bryceberger]

(first contribution, please let me know if this is the wrong way to go about the solution / opening prs / etc)

[TaoBi22]

As discussed in #8411, this doesn't work on my machine. However, @maerhart pointed out that in this PR LowerSMTToZ3LLVM still uses void as its printf return type. If I change the definition of printfType in LowerSMTToZ3LLVM to auto printfType = LLVM::LLVMFunctionType::get(rewriter.getI32Type(), {ptrTy}, true); then things work fine. Is this the case on your end too? If so then I guess that's the best solution (reverting #8327 and applying this)

[bryceberger]

Maybe I'm holding git submodules wrong... I haven't rebased the branch, but after a git submodule update and rebuilding this is now not working on my machine. Changing the type in LowerSMTToZ3LLVM does make it work again.

[TaoBi22]

Interesting - in that case could you double check that it's still failing if you undo the changes in this PR? This stuff was changed upstream recently so an out of date submodule could be to blame. If it still works after you undo them then great, and if not then we can revert 8327 and apply these changes.

[bryceberger]

It does work on 51a69bc. It also works on 87f7feb (current main). Guess this was a git submodule error on my part. Going to close this for now.

[TaoBi22]

Ah cool, thanks nonetheless for trying out circt-bmc and contributing back!!