[clang] [analyzer] Indicate UnarySymExpr is not supported by Z3 (PR #108900)

[Balazs Benics via cfe-commits]

steakhal wrote:

> > I'm okay with the PR, but this leaves me wonder how did you end up with this crash? How did you manage to avoid all the zillion other ways to crash the Z3 solver? Have you experienced such issues?
> 
> Thanks Balazs, TBH I'm not sure we've found all the ways to crash the Z3 solver since we stopped random testing with Z3 when we came across this issue. But we're getting that restarted to see what else we find (with this workaround in place). We have seen Z3 crashes specific to our internal proprietary target and have merged upstream and downstream only changes for those cases. As I think you may recall, we have our own specialized fuzzing tool for our downstream changes, so occasionally we find things not found anywhere else. 
> 
> Do you know if there's any other random testing done for csa without and with Z3? Maybe this is not being done now, or there's some gap if this issue had slipped through.

I'm not aware of anyone fuzzing CSA, neither with or without Z3 constraint solver. Without the right tooling, fuzzing is really inefficient. And even with the right tooling, it's not practical to cover new language features.
That said, it would be nice to see traction in the area.

At Sonar, we use a big corpus of projects for testing.

One way to find crashes is to run the Analysis LIT tests after removing the "REQUIRES: z3" lines (or patch the lit config to pass the z3 requirement). It's going to flood you.

https://github.com/llvm/llvm-project/pull/108900