[analyzer] Correct Z3 test cases, fix exposed crashes (#146597)

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.

Co-authored-by: einvbri <[email protected]>

Author: vabridgers

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};

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}}

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) 

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;
   };