clangsa makes contradictory assumptions about variable

[llvmbot]

Bugzilla Link	48474
Version	11.0
OS	Linux
Attachments	screenshot from CodeChecker
Reporter	LLVM Bugzilla Contributor
CC	@steakhal,@devincoughlin,@martong,@haoNoQ

Extended Description

I attach a screenshot from CodeChecker. You can also find the static HTML report at: https://testresults.qt.io/codechecker/daily_analyses/qtbase/dev/qtbase-dev-20201210-238f466d49/qdatetime.cpp_clangsa_fbaaa3c8986c74ae8f6ae431391de560.plist.html#reportHash=62a0d374a5d8f3a09605154ad72cab0d

In this report we see the following assumptions the analyzer makes:

6. Assuming 'spec' is not equal to TimeZone [...]
7. Assuming 'spec' is equal to Timezone (since it follows that branch of the switch statement)

This issue stands out the most, because of the closeness of the contradictory assumptions.

But this report is invalid for other reasons too, for example clangsa fails to track into the Data constructor in line 3048, which would make it evident it can't happen.

[steakhal]

I think we have all the resources to track this down except time. For now, I have other tasks to do. Let's hope others will pick this issue up and fix this in the next release.

[llvmbot]

As mentioned, I can't get the exact assumptions reproduced when running clangsa in the console, for the main issue.

But I managed to get it for the issue in qrhivulkan.cpp described in Comment #​2. For this I can even attach a preprocessed source code file so that everybody can reproduce it.

Would that be of any help? What other data would you need from me?

[haoNoQ]

From this, in turn, it looks like while contradictory assumptions are bad, they don't seem to be why the warning shows up in the first place.

Separately, there's missing information in the bug path: why does the static analyzer believe that the deleted pointer is null? This checker needs to track the pointer in order to explain this (and it'll likely cause this particular warning to go away as the analyzer realizes something and second-guesses itself while tracking the pointer).

[haoNoQ]

Screenshot with line 904.

Trimmed, raw exploded graph from the clang.

It doesn't seem to reproduce the issue. In the dump it is easy to see that on all bug paths control flow goes through the default: branch of the switch (jumping from line 899 to line 904 - see the screenshot).

[llvmbot]

I was only able to reproduce what Balazs also got. I could not get in the Console exactly what I got on CodeChecker in the bug description, despite using the original file and the original compilation command. (I altered the --analyze command according to Balazs' guidelines, so that might contribute).

I will try qrhivulkan.cpp next. If I reproduce it precisely, should I open a new report for that?

[steakhal]

Trimmed, raw exploded graph from the clang. I'm not really used to such huge exploded graphs, so I would call for some help.

Artem, could you have a look at this, please?

[llvmbot]

qdatetime.cpp plist

[llvmbot]

I see 4 relevant files (qdatetime.cpp clangsa files) in my results directory. I guess some are related to the CTU failing, so I'm attaching only the one with extension plist. Here is the full list if you need more:

./failed/qdatetime.cpp_clangsa_fbaaa3c8986c74ae8f6ae431391de560.plist_CTU_unknown.zip ./qdatetime.cpp_clangsa_fbaaa3c8986c74ae8f6ae431391de560.d ./success/qdatetime.cpp_clangsa_fbaaa3c8986c74ae8f6ae431391de560.plist.stderr.txt ./qdatetime.cpp_clangsa_fbaaa3c8986c74ae8f6ae431391de560.plist

[steakhal]

You are right, that's still suspicious :D I'm gonna record an exploded graph.

[steakhal]

The html export of the report shows the correct bug path. Could you please send us the plist file for that report?

Locally, I exported the bug report to html and it seems correct to me.

[llvmbot]

Thanks Balazs! You were much faster than me trying to understand and minimize the specific case.

You are right that the specific issue seems like a CodeChecker visualization issue. But I see another contradiction:

In the output you attached, I see:

/home/elnbbea/git/qtbase/src/corelib/time/qdatetime.cpp:892:25: note: Assuming 'spec' is not equal to OffsetFromUTC [ ... ] /home/elnbbea/git/qtbase/src/corelib/time/qdatetime.cpp:899:9: note: Control jumps to 'case OffsetFromUTC:' at line 900

Any idea about this one?

Finally what do you think about the contradiction I posted earlier on qrhivulkan.cpp that I posted on comment #​2?

[steakhal]

the clang call and the text output of the analysis

[steakhal]

the generated plist file

[steakhal]

I was able to reproduce the issue. I must conclude that this is a visual/parse bug on the CodeChecker's side.

The text diagnostic output states that the switch statement inside the lambda takes the OffsetFromUTC case at line 900, not the one at line 902 as shown in the CodeChecker report. In fact, line 902 is not even mentioned in the plist, produced by clang.

I attach the reproduced plist, and stdout for the text output.

[steakhal]

You could use the tu_collector to pack all the files needed. Even the internal standard library header dependencies.

This command should create a zip file:

codechecker/tools/tu_collector/tu_collector/tu_collector.py --logfile /path/to/compile_commands.json --filter qdatetime.cpp -zip ZIP

The script is at https://github.com/Ericsson/codechecker/blob/master/tools/tu_collector/tu_collector/tu_collector.py

Yes, a button for such a thing would be awesome on the GUI.

[haoNoQ]

I didn't debug but i'm 90% sure it's a bug in the lambda support, not the solver. Constraints here are too simple to be worried about.

Also, creduce is a bad idea for false positives. It reduces them to true positives way too often to be trusted. In any case, a preprocessed file would make a perfectly sufficient reproducer, we'll be able to reduce it ourselves later. I can't diagnose from CodeChecker though because it doesn't provide all the source code (includes aren't included).

@​Gabor, isn't there in CodeChecker a natural opportunity to automatically generate reproducers (even for CTU)? If it still has access to the source code and to the run-lines it could provide reproducer links that we could download in one click, unpack and reproduce the issue. That could be huge for fixing bugs.

[martong]

Our default SMT solver in the analyzer is dumb but fast, so I assume that could be the cause for these issues. The second case with qrhivulkan.cpp should be filtered out by the clever Z3 SMT solver when it tries to refute the bug report. Still, I'd not expect this kind of unfeasible state with the default solver, so this is worth a deeper investigation (thanks again for reporting it).

How can I analyze a single file? With CodeChecker, you can use a skipfile (--skip). Generally, you can manually edit the compilation database json file to contain only one entry.

Do you think Z3 refutation is safe to turn on for everything? It should be. If you experience a crash when Z3 refutation is enabled then please report another bug here.

[llvmbot]

But I have seen this more times. Another example:

https://testresults.qt.io/codechecker/daily_analyses/qtbase/dev/qtbase-dev-20201211-b283ce1e83/qrhivulkan.cpp_clangsa_2cd8d11b8d6cfbf488b273c65ba784a1.plist.html#reportHash=e00e9c596a346d71081478dad340f1ef

See steps (3) vs (8): (3): Assuming field 'active' is true (8): Assuming field 'active' is false

Haven't tried Z3 refutation yet. How can I analyze a single file? Do you think Z3 refutation is safe to turn on for everything?

[martong]

Thanks for the report!

I see that we indeed take that case in the switch statement that results in an infeasible state.

Do you think you could reduce the issue to a minimal example (10-30 lines)? That would be a great help to fix the issue. We usually use creduce to reduce the source code automatically. Besides, I wonder if the bugreport is still there if you enable Z3 refutation, could you take a look?

[llvmbot]

assigned to @martong