[analyzer] Correct Z3 test cases, fix exposed crashes

[vabridgers]

PR145731 corrected the analyzer test runner to consider use of z3 when used by testcases, which exposed problems in test cases PR37855.c and crashes in z3-crosscheck.c This change fixes those crashes and re-enables the test cases that were "XFAIL"'d out.

[llvmbot]

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

@llvm/pr-subscribers-llvm-support

Author: None (vabridgers)

Changes

PR145731 corrected the analyzer test runner to consider use of z3 when used by testcases, which exposed problems in test cases PR37855.c and crashes in z3-crosscheck.c This change fixes those crashes and re-enables the test cases that were "XFAIL"'d out.

---

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

4 Files Affected:

• (modified) clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h (+3)
• (modified) clang/test/Analysis/PR37855.c (+4-6)
• (modified) clang/test/Analysis/z3-crosscheck.c (-2)
• (modified) llvm/lib/Support/Z3Solver.cpp (+2-1)

diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
index 70a7953918ace..a6cb6c0f12a8c 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
@@ -598,6 +598,9 @@ class SMTConv {
     if (APSIntBitwidth == 1 && Ty.isNull())
       return {Int.extend(Ctx.getTypeSize(Ctx.BoolTy)),
               getAPSIntType(Ctx, NewInt)};
+    else if (APSIntBitwidth == 1 && !Ty.isNull())
+      return {Int.extend(Ctx.getTypeSize(getAPSIntType(Ctx, Int))),
+              getAPSIntType(Ctx, NewInt)};
     if (llvm::isPowerOf2_32(APSIntBitwidth) || Ty.isNull())
       return {Int, Ty};
     return {Int.extend(Ctx.getTypeSize(Ty)), Ty};
diff --git a/clang/test/Analysis/PR37855.c b/clang/test/Analysis/PR37855.c
index 434df576e8ece..92ed9ffe69a7d 100644
--- a/clang/test/Analysis/PR37855.c
+++ b/clang/test/Analysis/PR37855.c
@@ -2,23 +2,21 @@
 // RUN: %clang_analyze_cc1 -analyzer-checker=core -w -analyzer-config crosscheck-with-z3=true -verify %s
 // REQUIRES: z3
 
-// XFAIL: *
-
 typedef struct o p;
 struct o {
   struct {
   } s;
 };
 
-void q(*r, p2) { r < p2; }
+void q(int *r, int p2) { r < p2; }
 
-void k(l, node) {
+void k(int l, int node) {
   struct {
     p *node;
   } * n, *nodep, path[sizeof(void)];
-  path->node = l;
+  path->node = (p*) l;
   for (n = path; node != l;) {
-    q(node, n->node);
+    q((int *)&node, (int)n->node);
     nodep = n;
   }
   if (nodep) // expected-warning {{Branch condition evaluates to a garbage value}}
diff --git a/clang/test/Analysis/z3-crosscheck.c b/clang/test/Analysis/z3-crosscheck.c
index ca20cd6a879f1..8cbe7dd2975d0 100644
--- a/clang/test/Analysis/z3-crosscheck.c
+++ b/clang/test/Analysis/z3-crosscheck.c
@@ -2,8 +2,6 @@
 // RUN: %clang_analyze_cc1 -triple x86_64-pc-linux-gnu -analyzer-checker=core,unix.Malloc,debug.ExprInspection -analyzer-config crosscheck-with-z3=true -verify %s
 // REQUIRES: z3
 
-// XFAIL: *
-
 void clang_analyzer_dump(float);
 
 int foo(int x) 
diff --git a/llvm/lib/Support/Z3Solver.cpp b/llvm/lib/Support/Z3Solver.cpp
index 27027093a0c6f..056a17ad80123 100644
--- a/llvm/lib/Support/Z3Solver.cpp
+++ b/llvm/lib/Support/Z3Solver.cpp
@@ -932,7 +932,8 @@ class Z3Statistics final : public SMTSolverStatistics {
   };
   unsigned getUnsigned(StringRef Key) const override {
     auto It = UnsignedValues.find(Key.str());
-    assert(It != UnsignedValues.end());
+    if (It == UnsignedValues.end())
+      return 0;
     return It->second;
   };
 

[NagyDonat]

LGTM, thanks for fixing these testcases! I suggested one minor simplification in an inline comment, but overall I'm satisfied with the code.

[NagyDonat]

Suggested change

	if (APSIntBitwidth == 1 && Ty.isNull())
	return {Int.extend(Ctx.getTypeSize(Ctx.BoolTy)),
	getAPSIntType(Ctx, NewInt)};
	else if (APSIntBitwidth == 1 && !Ty.isNull())
	return {Int.extend(Ctx.getTypeSize(getAPSIntType(Ctx, Int))),
	getAPSIntType(Ctx, NewInt)};
	if (APSIntBitwidth == 1) {
	if (Ty.isNull())
	return {Int.extend(Ctx.getTypeSize(Ctx.BoolTy)),
	getAPSIntType(Ctx, NewInt)};
	return {Int.extend(Ctx.getTypeSize(getAPSIntType(Ctx, Int))),
	getAPSIntType(Ctx, NewInt)};
	}

[steakhal]

Remember to not have redundant "else" after having a "return".

[NagyDonat]

You're right, thanks, I edited my suggestion.

[steakhal]

Why did this assertion fail? I thought the "rlimit" must exist on the required Z3 versions.

[steakhal]

@vabridgers Could you investigate this question?