Page MenuHomePhabricator

[analyzer] Rework Z3 requirements in the CSA testsuite
Needs ReviewPublic

Authored by steakhal on Jul 13 2020, 6:14 AM.

Details

Summary

Summary:

  • rename the USE_Z3_SOLVER llvm-lit parameter to RECHECK_WITH_Z3_SOLVER to reflect its behavior
  • document the RECHECK_WITH_Z3_SOLVER parameter in the checker_dev_manual.html
  • introduce the %clang_analyze_cc1_range and %clang_analyze_cc1_z3 substitutions to control the constraint manager used for the test
  • 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?")
  • FIX a bunch of tests, specifying the required constraint manager, and z3 requirement if needed
  • 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.

Diff Detail

Event Timeline

steakhal created this revision.Jul 13 2020, 6:14 AM
steakhal updated this revision to Diff 277409.Jul 13 2020, 6:29 AM
  • use the %clang_analyze_cc1_range in PR37855.c

I lack the confidence to accept this straight away, but the overall direction looks great. LGTM!

You're going to be very popular around here with these patches! :)

clang/test/Analysis/trustnonnullchecker_test.m
1–3

Why did you delete this? @NoQ, is D57062 related?

clang/www/analyzer/checker_dev_manual.html
6

This menu is still not working, right?

548–550

What is the difference in between clang_analyze_cc1 and clang_analyze_cc1_range then?

548–550

I meant to delete this inline, oops :)

steakhal marked an inline comment as done.Jul 13 2020, 9:13 AM

Thanks for the really fast feedback @Szelethus!

Should we prefer using %clang_analyze_cc1 over raw %clang_cc1 invocations with the -analyze flag? And fall back to the more specific %clang_analyze_cc1_range/%clang_analyze_cc1_z3, if the test turns out, requires a certain constraint manager?
If so, I started to update some tests according to this, and a few questions raised during that process.

  • Which should we use for example the analyzer-enabled-checkers.c, which only prints the enabled checkers?
  • There is also an interesting behavior about command-line parsing. [1]

[1]: AFAIK flags should not be position dependant.
But moving the -analyze flag around makes this test fail.

PASS:
./bin/clang -cc1 -internal-isystem ./lib/clang/11.0.0/include -nostdsysteminc -analyzer-constraints=range -setup-static-analyzer -fsyntax-only -analyze -analyzer-checker=core,debug.ExprInspection ../../clang/test/Analysis/handle_constructors_with_new_array.cpp -verify

After moving the -analyze after the -nostdsysteminc flag, it FAILs:
./bin/clang -cc1 -internal-isystem ./lib/clang/11.0.0/include -nostdsysteminc -analyze -analyzer-constraints=range -setup-static-analyzer -fsyntax-only -analyzer-checker=core,debug.ExprInspection ../../clang/test/Analysis/handle_constructors_with_new_array.cpp -verify

Could someone tell me the difference?

clang/www/analyzer/checker_dev_manual.html
6

IDK. But I don't really want to touch any css/js related things :D

@Szelethus Can you vaguely remember why did we keep the invalid-analyzer-config-value.c test if the invalid-a-na-ly-zer-con-fig-value.c has the very same content?
IMO we should only keep the former with a description why has the file such a weird name :D

NoQ added a comment.Jul 13 2020, 2:08 PM

Folks, please announce your overall plan for Z3 (unless i missed it). It looks like you are planning to actively support Z3 as a constraint manager, i.e. invoke it on every assume()? Did you consider my usual suggestion to only apply it to refuting non-buggy states in order to combat your false negatives similarly to how our current Z3 refutation refutes buggy states to combat false positives?

clang/www/analyzer/checker_dev_manual.html
534

Yeah, just delete this :)

llvm/utils/lit/lit/llvm/config.py
412–413

I'm for longer names, "range" is too vague, "z3" is already ambiguous (does it mean as constraint manager or for refutation?).

%clang_analyze_cc1_range_cm_only would probably make more sense. It also looks more like a FIXME and tells that something's wrong with the test.

steakhal marked 4 inline comments as done.Jul 14 2020, 1:45 AM
In D83677#2148435, @NoQ wrote:

[...] It looks like you are planning to actively support Z3 as a constraint manager. [...] Did you consider my usual suggestion to only apply it to refuting non-buggy states in order to combat your false negatives similarly to how our current Z3 refutation refutes buggy states to combat false positives?

I don't plan to invest time to support Z3-CM.

Although, I highly value the refutation infrastructure. TBH this patch focused fixing the test-infra to be able to have tests explicitly testing refutation related warnings.
Please note that previously you could not require z3 and only run the test using the range-CM. Using also the Z3-CM would not emit warning for that case, making the test fail.
Besides fixing this (which was my primary object), adds new ToolSubsts in a backward-compatible manner to let the test author specify explicitly the CM of their choice.

clang/www/analyzer/checker_dev_manual.html
534

Is the ninja check-clang-analysis the prefered way running the test?
I will reword the doc then.

llvm/utils/lit/lit/llvm/config.py
412–413

I'm for longer names, "range" is too vague, "z3" is already ambiguous (does it mean as constraint manager or for refutation?).

If we don't expect the clangSA dev to be able to differentiate, why should we expect them to know what 'cm' means there?
I'm not against longer names, but kinda hard to strike the balance for finding short but descriptive names.

A lengthy ToolSubst would consume most of the available space in the line, rendering most of the RUN commands to span across multiple lines.

[...] It also looks more like a FIXME and tells that something's wrong with the test.

I don't think that should be suspicious.
I wouldn't assume that test is wrong, simply that test works only with the range-CM.