[PATCH] D83677: [analyzer] Rework Z3 requirements in the CSA testsuite

[Balázs Benics via Phabricator via llvm-commits]

steakhal created this revision.
steakhal added reviewers: NoQ, Szelethus, vsavchenko, martong, ddcc, gamesh411, xazax.hun.
Herald added subscribers: llvm-commits, ASDenysPetrov, Charusso, dkrupp, donat.nagy, mikhail.ramalho, a.sidorin, zzheng, delcypher, JDevlieghere, rnkovacs, szepet, baloghadamsoftware, whisperity, mgorny.
Herald added a project: LLVM.

1. Summary:
2. rename the `USE_Z3_SOLVER` llvm-lit parameter to `RECHECK_WITH_Z3_SOLVER` to reflect its behavior
3. document the `RECHECK_WITH_Z3_SOLVER` parameter in the `checker_dev_manual.html`
4. introduce the `%clang_analyze_cc1_range` and `%clang_analyze_cc1_z3` substitutions to control the constraint manager used for the test
5. FIX the `REQUIRES: z3` expressions in tests (before the patch it wanted to mean something like "only run this test if we use the Z3 constraint manager"; after the patch "is clang build with z3?")
6. FIX a bunch of tests, specifying the required constraint manager, and z3 requirement if needed
7. DELETE `z3/enabled.c` test, since that no longer serves any purpose - IMO

Before the patch:
=================

Using `./bin/llvm-lit -sv --param USE_Z3_SOLVER=0 ...../test/Analysis  --show-unsupported   --show-xfail`:

  Unsupported Tests (6):
    Clang :: Analysis/PR24184.cpp
    Clang :: Analysis/PR37855.c
    Clang :: Analysis/exploded-graph-rewriter/win_path_forbidden_chars.cpp
    Clang :: Analysis/trustnonnullchecker_test.m
    Clang :: Analysis/z3-crosscheck.c
    Clang :: Analysis/z3/enabled.c
  
  ********************
  Expectedly Failed Tests (5):
    Clang :: Analysis/container-modeling-no-aggressive-binary-operation-simplification-warn.cpp
    Clang :: Analysis/iterator-modeling-no-aggressive-binary-operation-simplification-no-crash.cpp
    Clang :: Analysis/outofbound-notwork.c
    Clang :: Analysis/redecl.c
    Clang :: Analysis/string-fail.c
  
  
  Testing Time: 80.68s
    Unsupported      :   6
    Passed           : 716
    Expectedly Failed:   5



---

Using `./bin/llvm-lit -sv --param USE_Z3_SOLVER=1 ...../test/Analysis  --show-unsupported   --show-xfail`:

  Unsupported Tests (3):
    Clang :: Analysis/PR24184.cpp
    Clang :: Analysis/exploded-graph-rewriter/win_path_forbidden_chars.cpp
    Clang :: Analysis/trustnonnullchecker_test.m
  
  ********************
  Expectedly Failed Tests (5):
    Clang :: Analysis/container-modeling-no-aggressive-binary-operation-simplification-warn.cpp
    Clang :: Analysis/iterator-modeling-no-aggressive-binary-operation-simplification-no-crash.cpp
    Clang :: Analysis/outofbound-notwork.c
    Clang :: Analysis/redecl.c
    Clang :: Analysis/string-fail.c
  
  ********************
  Failed Tests (7):
    Clang :: Analysis/constant-folding.c
    Clang :: Analysis/container-modeling.cpp
    Clang :: Analysis/dump_egraph.c
    Clang :: Analysis/expr-inspection.c
    Clang :: Analysis/iterator-modeling.cpp
    Clang :: Analysis/loop-unrolling.cpp
    Clang :: Analysis/plist-macros.cpp
  
  
  Testing Time: 236.37s
    Unsupported      :   3
    Passed           : 712
    Expectedly Failed:   5
    Failed           :   7



---

After the patch:
================

Using `./bin/llvm-lit -sv --param RECHECK_WITH_Z3_SOLVER=0 ...../test/Analysis  --show-unsupported   --show-xfail`:

  Unsupported Tests (1):
    Clang :: Analysis/exploded-graph-rewriter/win_path_forbidden_chars.cpp
  
  ********************
  Expectedly Failed Tests (5):
    Clang :: Analysis/container-modeling-no-aggressive-binary-operation-simplification-warn.cpp
    Clang :: Analysis/iterator-modeling-no-aggressive-binary-operation-simplification-no-crash.cpp
    Clang :: Analysis/outofbound-notwork.c
    Clang :: Analysis/redecl.c
    Clang :: Analysis/string-fail.c
  
  
  Testing Time: 99.74s
    Unsupported      :   1
    Passed           : 720
    Expectedly Failed:   5



---

Using `./bin/llvm-lit -sv --param RECHECK_WITH_Z3_SOLVER=1 ...../test/Analysis  --show-unsupported   --show-xfail`:

  Unsupported Tests (1):
    Clang :: Analysis/exploded-graph-rewriter/win_path_forbidden_chars.cpp
  
  ********************
  Expectedly Failed Tests (5):
    Clang :: Analysis/container-modeling-no-aggressive-binary-operation-simplification-warn.cpp
    Clang :: Analysis/iterator-modeling-no-aggressive-binary-operation-simplification-no-crash.cpp
    Clang :: Analysis/outofbound-notwork.c
    Clang :: Analysis/redecl.c
    Clang :: Analysis/string-fail.c
  
  ********************
  Failed Tests (2):
    Clang :: Analysis/container-modeling.cpp
    Clang :: Analysis/iterator-modeling.cpp
  
  
  Testing Time: 255.49s
    Unsupported      :   1
    Passed           : 718
    Expectedly Failed:   5
    Failed           :   2

Before and after the patch, the `container-modeling.cpp` and `iterator-modeling.cpp` were crashing using the Z3 constraint manager.
Worth to have a look at those in the future, if we think that the Z3 constraint manager worth the investment.


https://reviews.llvm.org/D83677

Files:
  clang/test/Analysis/PR24184.cpp
  clang/test/Analysis/analyzer_test.py
  clang/test/Analysis/constant-folding.c
  clang/test/Analysis/dump_egraph.c
  clang/test/Analysis/expr-inspection.c
  clang/test/Analysis/lit.local.cfg
  clang/test/Analysis/loop-unrolling.cpp
  clang/test/Analysis/plist-macros.cpp
  clang/test/Analysis/trustnonnullchecker_test.m
  clang/test/Analysis/z3/enabled.c
  clang/test/CMakeLists.txt
  clang/test/lit.site.cfg.py.in
  clang/www/analyzer/checker_dev_manual.html
  llvm/utils/gn/secondary/clang/test/BUILD.gn
  llvm/utils/lit/lit/llvm/config.py

-------------- next part --------------
A non-text attachment was scrubbed...
Name: D83677.277401.patch
Type: text/x-patch
Size: 13802 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/llvm-commits/attachments/20200713/968a8a39/attachment.bin>