[analyzer] Indicate UnarySymExpr is not supported by Z3

[vabridgers]

Random testing found that the Z3 wrapper does not support UnarySymExpr, which was added recently and not included in the original Z3 wrapper. For now, just avoid submitting expressions to Z3 to avoid compiler crashes.

Some crash context ...

clang -cc1 -analyze -analyzer-checker=core z3-unarysymexpr.c -analyzer-constraints=z3

Unsupported expression to reason about!
UNREACHABLE executed at clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h:297!

Stack dump:
3. /clang/test/Analysis/z3-unarysymexpr.c:13:7: Error evaluating branch #0 llvm::sys::PrintStackTrace(llvm::raw_ostream&, int) #1 llvm::sys::RunSignalHandlers() #8 clang::ento::SimpleConstraintManager::assumeAux( llvm::IntrusiveRefCntPtr<clang::ento::ProgramState const>, clang::ento::NonLoc, bool) #9 clang::ento::SimpleConstraintManager::assume( llvm::IntrusiveRefCntPtr<clang::ento::ProgramState const>, clang::ento::NonLoc, bool)

[llvmbot]

@llvm/pr-subscribers-clang

@llvm/pr-subscribers-clang-static-analyzer-1

Author: None (vabridgers)

Changes

Random testing found that the Z3 wrapper does not support UnarySymExpr, which was added recently and not included in the original Z3 wrapper. For now, just avoid submitting expressions to Z3 to avoid compiler crashes.

Some crash context ...

clang -cc1 -analyze -analyzer-checker=core z3-unarysymexpr.c -analyzer-constraints=z3

Unsupported expression to reason about!
UNREACHABLE executed at clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h:297!

Stack dump:
3. <root>/clang/test/Analysis/z3-unarysymexpr.c:13:7: Error evaluating branch #0 <addr> llvm::sys::PrintStackTrace(llvm::raw_ostream&, int) #1 <addr> llvm::sys::RunSignalHandlers() #8 <addr> clang::ento::SimpleConstraintManager::assumeAux( llvm::IntrusiveRefCntPtr<clang::ento::ProgramState const>, clang::ento::NonLoc, bool) #9 <addr> clang::ento::SimpleConstraintManager::assume( llvm::IntrusiveRefCntPtr<clang::ento::ProgramState const>, clang::ento::NonLoc, bool)

---

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

2 Files Affected:

• (modified) clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h (+7)
• (added) clang/test/Analysis/z3-unarysymexpr.c (+16)

diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
index bf18c353b85083..16a6b3a2e18112 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
@@ -278,6 +278,13 @@ class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
     if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym))
       return canReasonAbout(SVB.makeSymbolVal(SC->getOperand()));
 
+    // If a UnarySymExpr is encountered, the Z3
+    // wrapper does not support those. So indicate Z3 does not
+    // support those and return.
+    if (const UnarySymExpr *USE = dyn_cast<UnarySymExpr>(Sym)) {
+      return false;
+    }
+
     if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
       if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE))
         return canReasonAbout(SVB.makeSymbolVal(SIE->getLHS()));
diff --git a/clang/test/Analysis/z3-unarysymexpr.c b/clang/test/Analysis/z3-unarysymexpr.c
new file mode 100644
index 00000000000000..80625eb61eb52e
--- /dev/null
+++ b/clang/test/Analysis/z3-unarysymexpr.c
@@ -0,0 +1,16 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -verify %s \
+// RUN:  -analyzer-constraints=z3 
+
+// REQUIRES: Z3
+//
+// This LIT covers a crash associated with this test.
+// The expectation is to not crash!
+//
+
+long a;
+void b() {
+  long c;
+  if (~(b && a)) // expected-warning {{address of function 'b' will always evaluate to 'true'}}
+  // expected-note@-1 {{prefix with the address-of operator to silence this warning}}
+    c ^= 0; // expected-warning {{The left expression of the compound assignment is an uninitialized value. The computed value will also be garbage}}
+}

[vabridgers]

Maybe this CR could be easily improved to handle this case correctly rather than avoiding the crash, just wanted to see if it's better to get this change in for now avoiding the crash or get some advice on how to fix this correctly.

[NagyDonat]

Do I understand it correctly that this deficiency affects the standalone Z3 analysis mode (as opposed to the "Z3 refutation" where the analysis is performed with the native range-based constraint manager, and then the results are validated with Z3 to discard the logically impossible paths)?

[vabridgers]

Hi @NagyDonat , yes this is only exposed when z3 is used as the constraint manager. This crash does not occur when using z3-refutation.

[steakhal]

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?

[vabridgers]

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.

Thanks

[steakhal]

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.

[vabridgers]

Hi @NagyDonat , I think all comments have been addressed. Please review at your convenience. Thank you!

[NagyDonat]

LGTM with some additional bikeshedding in a comment that could be shorter IMO.