[Analyzer] Fix Z3ConstraintManager crash (PR37646)

[vlad.tsyrklevich]

Summary

Fix another Z3ConstraintManager crash, use fixAPSInt() to extend a
boolean APSInt.

[george.karpenkov]

LGTM with a nit on a test name.

test/Analysis/pr37646.c

1 ↗

(On Diff #149396)

The tests are already quite messy, but adding a new file per each bug seems excessive. Could we take your test and test/Analysis/apsint.c and combine them into e.g. z3_apsint_encoding.c ? (also adding a link to bugzilla)

[george.karpenkov]

Thanks!

[NoQ]

We might as well make a directory for z3-specific tests. Eg., z3/bool-bit-width.c.

Also does this test need to be z3-specific? We would also not like to crash here without z3.

[ddcc]

In D47617#1119257, @george.karpenkov wrote:

LGTM with a nit on a test name.

Same.

In D47617#1119268, @NoQ wrote:

Also does this test need to be z3-specific? We would also not like to crash here without z3.

I had the same though originally about the REQUIRES line. Since this code path is very specific to Z3ConstraintManager, it didn't seem useful to run the test on normal buildbots. But I have no preference either way.

[vlad.tsyrklevich]

In D47617#1119268, @NoQ wrote:

Also does this test need to be z3-specific? We would also not like to crash here without z3.

I originally did that so I could specify enabling and testing the z3 backend; however, looking at the testing infra more I realize that z3 is supposed to be run on the analyzer tests but it seems like z3 tests have been broken since October when r315627 landed. I submitted a fix in https://reviews.llvm.org/D47722

[vlad.tsyrklevich]

• Merge test with apsint.c and move to z3/apsint.c

[george.karpenkov]

Thanks!

lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
       RHS = LHS ? getSymVal(State, SSM->getRHS()) : nullptr;
     } else {
       llvm_unreachable("Unsupported binary expression to get symbol value!");
     }
 
     if (!LHS || !RHS)
       return nullptr;
 
-    llvm::APSInt ConvertedLHS = *LHS, ConvertedRHS = *RHS;
-    QualType LTy = getAPSIntType(*LHS), RTy = getAPSIntType(*RHS);
+    llvm::APSInt ConvertedLHS, ConvertedRHS;
+    QualType LTy, RTy;
+    std::tie(ConvertedLHS, LTy) = fixAPSInt(*LHS);
+    std::tie(ConvertedRHS, RTy) = fixAPSInt(*RHS);
     doIntTypeConversion<llvm::APSInt, Z3ConstraintManager::castAPSInt>(
         ConvertedLHS, LTy, ConvertedRHS, RTy);
     return BVF.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
   }
 
   llvm_unreachable("Unsupported expression to get symbol value!");
 }
 

test/Analysis/apsint.c

-// REQUIRES: z3
-// RUN: %clang_analyze_cc1 -triple x86_64-unknown-linux-gnu -analyzer-checker=core -verify %s
-// expected-no-diagnostics
-
-_Bool a() {
-  return !({ a(); });
-}

test/Analysis/z3/apsint.c

+// RUN: %clang_analyze_cc1 -triple x86_64-unknown-linux-gnu -analyzer-checker=core -verify %s
+// expected-no-diagnostics
+
+// https://bugs.llvm.org/show_bug.cgi?id=37622
+_Bool a() {
+  return !({ a(); });
+}
+
+// https://bugs.llvm.org/show_bug.cgi?id=37646
+_Bool b;
+void c() {
+  _Bool a = b | 0;
+  for (;;)
+    if (a)
+      ;
+}