[Analyzer][Z3] Test fixes for Z3 constraint manager

[vlad.tsyrklevich]

Summary

Since Z3 tests have been not been running [1] some tests needed to be
updated. I also added a regression test for [1].

[1] https://reviews.llvm.org/D47722

[george.karpenkov]

Impressive, really. So almost all tests still pass.
However, a few questions should be resolved before we can merge:

• Do all tests for Z3 run when LLVM is configured to use Z3? I'm not sure if that's the right thing: do all tests start to take 10x time to run once Z3 is enabled?

Should we create a separate ninja target for those?

• Is anyone interested in running a buildbot running those?

[george.karpenkov]

Seems to be good to merge regardless.

[ddcc]

In D47726#1121395, @george.karpenkov wrote:

• Do all tests for Z3 run when LLVM is configured to use Z3? I'm not sure if that's the right thing: do all tests start to take 10x time to run once Z3 is enabled?

The test approach is what @dcoughlin suggested in D28952, where the tests are run using each constraint manager that is available. At that time, he measured an increase in test time from 25s to 90s (see https://reviews.llvm.org/D28952#686284).

• Is anyone interested in running a buildbot running those?

@dcoughlin mentioned that he (Apple?) would set up a buildbot for this, but I don't know if that happened.

[george.karpenkov]

@ddcc To be completely honest, I see a few design issues with the current implementation of Z3 backend,
the main one being that it checks satisfiability after every single exploded node.
To the best of my knowledge, reasonable scalability would not be achieved with such an approach,
and I'm not sure how feasible would it be to change it without rewriting most of the checkers.

Thus we currently do not plan to set up a Z3 bot, but if you wish to maintain we certainly can provide pointers on how this can be done.

The test approach is what @dcoughlin suggested in D28952, where the tests are run using each constraint manager that is available

Apologies for conflicting instruction. Now that @mikhail.ramalho is working on refutation with Z3 it might not make sense to force the user to run all tests with Z3 at all times.
What do you think if we introduce ninja check-clang-analyzer to run the analyzer tests, and ninja check-clang-analyzer-z3 to run all the analyzer tests with Z3?
[there might be another ninja target for running all analyzer tests, I just don't remember which one. But at the end of the day there should be away to run analyzer tests without Z3 even when Z3 is linked in]

[ddcc]

@ddcc To be completely honest, I see a few design issues with the current implementation of Z3 backend,
the main one being that it checks satisfiability after every single exploded node.
To the best of my knowledge, reasonable scalability would not be achieved with such an approach,
and I'm not sure how feasible would it be to change it without rewriting most of the checkers.

I agree, though a number of these are limitations in CSA, and not specifically the backend.

Thus we currently do not plan to set up a Z3 bot, but if you wish to maintain we certainly can provide pointers on how this can be done.

I don't plan to set one up either. Just compiling clang/llvm is already very resource intensive.

What do you think if we introduce ninja check-clang-analyzer to run the analyzer tests, and ninja check-clang-analyzer-z3 to run all the analyzer tests with Z3?
[there might be another ninja target for running all analyzer tests, I just don't remember which one. But at the end of the day there should be away to run analyzer tests without Z3 even when Z3 is linked in]

Sounds good.

[george.karpenkov]

I agree, though a number of these are limitations in CSA, and not specifically the backend.

Yeah, so for instance we always assume that for a given state we know whether it's feasible or not,
and IMO for efficient SMT solver support we would need to operate over "lazy" states which may or may not be feasible.

cfe/trunk/test/Analysis/PR24184.cpp

+// UNSUPPORTED: z3
 // RUN: %clang_analyze_cc1 -w -analyzer-eagerly-assume -fcxx-exceptions -analyzer-checker=core -analyzer-checker=alpha.core.PointerArithm,alpha.core.CastToStruct -analyzer-max-loop 64 -verify %s
 // RUN: %clang_analyze_cc1 -w -analyzer-checker=core -analyzer-checker=cplusplus -fcxx-exceptions -analyzer-checker alpha.core.PointerArithm,alpha.core.CastToStruct -analyzer-max-loop 63 -verify %s
 
 // These tests used to hit an assertion in the bug report. Test case from http://llvm.org/PR24184.
 typedef struct {
   int cbData;
   unsigned pbData;
 } CRYPT_DATA_BLOB;

cfe/trunk/test/Analysis/constant-folding.c

void testBitwiseRules(unsigned int a, int b) {
   // Rules don't apply to signed typed, as the values might be negative.
   clang_analyzer_eval((b | 1) > 0); // expected-warning{{UNKNOWN}}
 
   // Even for signed values, bitwise OR with a non-zero is always non-zero.
   clang_analyzer_eval((b | 1) == 0); // expected-warning{{FALSE}}
   clang_analyzer_eval((b | -2) == 0); // expected-warning{{FALSE}}
   clang_analyzer_eval((b | 10) == 0); // expected-warning{{FALSE}}
   clang_analyzer_eval((b | 0) == 0); // expected-warning{{UNKNOWN}}
+#ifdef ANALYZER_CM_Z3
+  clang_analyzer_eval((b | -2) >= 0); // expected-warning{{FALSE}}
+#else
   clang_analyzer_eval((b | -2) >= 0); // expected-warning{{UNKNOWN}}
+#endif
 
   // Check that dynamically computed constants also work.
   int constant = 1 << 3;
   unsigned int d = a | constant;
   clang_analyzer_eval(constant > 0); // expected-warning{{TRUE}}
 }

cfe/trunk/test/Analysis/loop-unrolling.cpp

int nested_inlined_unroll1() {
   }
   int a = 22 / k; // expected-warning {{Division by zero}}
   return 0;
 }
 
 int nested_inlined_no_unroll1() {
   int k;
   for (int i = 0; i < 9; i++) {
+#ifdef ANALYZER_CM_Z3
+    clang_analyzer_numTimesReached(); // expected-warning {{13}}
+#else
     clang_analyzer_numTimesReached(); // expected-warning {{15}}
+#endif
     k = simple_unknown_bound_loop();  // reevaluation without inlining, splits the state as well
   }
   int a = 22 / k; // no-warning
   return 0;
 }
 
 int recursion_unroll1(bool b) {
   int k = 2;

cfe/trunk/test/Analysis/z3/enabled.c

+// REQUIRES: z3
+// RUN: echo %clang_analyze_cc1 | FileCheck %s
+// CHECK: -analyzer-constraints=z3