solfuzzer terminates with a crash on inputs containing invalid UTF-8 (mild obstacle to fuzzing)

[agroce]

Given any .sol input from standard input that contains invalid UTF-8 (which will frequently be produced by byte-mutating fuzzers like AFL), solfuzzer fails like this:

Testing compiler with optimizer.
terminate called after throwing an instance of 'nlohmann::json_abi_v3_11_3::detail::type_error'
  what():  [json.exception.type_error.316] invalid UTF-8 byte at index 35: 0x80
Aborted

This looks like a crash to the fuzzer, so produces lots of spurious crashes and an annoying burden for triage. The solc executable does not crash on such inputs, as far as I can see. This isn't a major problem, fuzzing still works, but it definitely imposes a cost (of 9 million executions of solfuzzer in one fuzzing run, over 3 million have been crashes due to this UTF-8 issue, and with a larger starting corpus especially the crash set is composed of a huge number of ways to reach this uninteresting non-bug crash).

This is on the latest solc/solidity (0.8.24 github main branch)

Steps to Reproduce

Just run solfuzzer on an input like:

contract test {
    f\200^@ction g() pu\203lic { f(); }
}

build/test/tools/solfuzzer < crash.sol

[agroce]

(I made a weak local patch, but this would be nice to have to not patch before fuzz runs; I'm resuming something like the campaign from a few years ago that found quite a few bugs. I'm probably going to port my stuff from then to AFL++ and centipede, which might find some interesting things with those mutations + a better fuzz engine)

[agroce]

New campaign with patch is turning things up, but so far only "pragma experimental solidity" bugs, which I assume you folks don't want to hear about, since that's going away shortly and isn't guaranteed stable anyway

[clonker]

Yeah these will go away (presumably) with the 0.9 release and are generally deemed unstable, indeed. Thanks for making sure!

[agroce]

BTW, I'm adding "pragma experimental SMTChecker" to the start of corpus files to trigger that, since it's been a bug-rich part of solc for a long time, but I know that's being deprecated. Is there a way to get solfuzzer to try the various model-check modes now, or does it need the pragma or editing solfuzzer?