Skip to content

[clang analyzer] Z3 error: Argument #x00007fff at position 1 does not match declaration (declare-fun bvsle ((_ BitVec 16) (_ BitVec 16)) Bool) #43375

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Closed
LebedevRI opened this issue Nov 17, 2019 · 6 comments
Closed

[clang analyzer] Z3 error: Argument #x00007fff at position 1 does not match declaration (declare-fun bvsle ((_ BitVec 16) (_ BitVec 16)) Bool) #43375

LebedevRI opened this issue Nov 17, 2019 · 6 comments
Assignees
@haoNoQ
Labels
bugzilla Issues migrated from bugzilla clang:static analyzer

Comments

@LebedevRI
Copy link
Member

Bugzilla Link 44030
Version trunk
OS Linux
Attachments AbstractDngDecompressor-0382b2.sh, AbstractDngDecompressor-0382b2.cpp, VC5Decompressor-a956e9.cpp, VC5Decompressor-a956e9.sh
CC @steakhal,@devincoughlin,@zmodem,@mikhailramalho,@haoNoQ

Extended Description

Was playing around with clang trunk + Z3 4.8.6 + CodeChecker --z3 on
and got the following crash
@LebedevRI
Copy link
Member Author

assigned to @haoNoQ

@haoNoQ
Copy link
Collaborator

haoNoQ commented Jan 15, 2020

I don't think this should block the release because Z3 support in the Static Analyzer was never declared stable to begin with. I doubt Clang is actually ever shipped with Z3 support; even if it is, it shouldn't be. I wish we had this, but we're not there yet :(

I could try to take a look tho. bvand is a fairly basic operation, i wonder what could go wrong. Probably cast symbols messed up.

@LebedevRI
Copy link
Member Author

I don't think this should block the release because Z3 support in the Static
Analyzer was never declared stable to begin with.
That's fair.

I doubt Clang is actually ever shipped with Z3 support;
It is, in apt.llvm.org debian builds, i didn't build it myself.

even if it is, it shouldn't be. I wish we had
this, but we're not there yet :(
FWIW this was the only static analyzer-Z3 bug i've encountered,
that is why i've filled a bug.

I could try to take a look tho. bvand is a fairly basic operation, i
wonder what could go wrong. Probably cast symbols messed up.

Thanks!

@mikhailramalho
Copy link
Member

Yep, this is another issue related to the casts being dropped by the CSA :/

In particular, the haveSameType call in SimpleSValBuilder.cpp:98 returns that the two bit-vectors have the same width.

The range constraint manager is more lenient about these width mismatches, but the solver will refuse to encode the program :/

The correct fix is to implement the whole truncation/extension in the CSA.

Maybe we can have this task as part of GSOC this year? Maybe implement support for truncation/extension and floating-points :D

@zmodem
Copy link
Collaborator

zmodem commented Jan 23, 2020

As was mentioned above, I don't think we should block the release on this.

@steakhal
Copy link
Contributor

It was really thoughtful to read this.
Unfortunately this bug can materialize during Z3 refutation as well - which is beyond doubt that useful and should be supported.

I'm also expecting to bite back in the future if we can't deal with this issue.
FYI there is a patch touching this topic: https://reviews.llvm.org/D85528

PS thanks Lebedev for the CC.

@llvmbot llvmbot transferred this issue from llvm/llvm-bugzilla-archive Dec 10, 2021
steakhal pushed a commit that referenced this issue May 2, 2022
[analyzer] Fix cast evaluation on scoped enums in ExprEngine
fd7efe3 
We ignored the cast if the enum was scoped.
This is bad since there is no implicit conversion from the scoped enum to the corresponding underlying type.

The fix is basically: isIntegralOrEnumerationType() -> isIntegralOr**Unscoped**EnumerationType()

This materialized in crashes on analyzing the LLVM itself using the Z3 refutation.
Refutation synthesized the given Z3 Binary expression (`BO_And` of `unsigned char` aka. 8 bits
and an `int` 32 bits) with the wrong bitwidth in the end, which triggered an assert.

Now, we evaluate the cast according to the standard.

This bug could have been triggered using the Z3 CM according to
https://bugs.llvm.org/show_bug.cgi?id=44030

Fixes #47570 #43375

Reviewed By: martong

Differential Revision: https://reviews.llvm.org/D85528
@steakhal steakhal closed this as completed May 2, 2022
haoNoQ pushed a commit to swiftlang/llvm-project that referenced this issue Jul 19, 2022
@haoNoQ
[analyzer] Fix cast evaluation on scoped enums in ExprEngine
f2d1dc5 
We ignored the cast if the enum was scoped.
This is bad since there is no implicit conversion from the scoped enum to the corresponding underlying type.

The fix is basically: isIntegralOrEnumerationType() -> isIntegralOr**Unscoped**EnumerationType()

This materialized in crashes on analyzing the LLVM itself using the Z3 refutation.
Refutation synthesized the given Z3 Binary expression (`BO_And` of `unsigned char` aka. 8 bits
and an `int` 32 bits) with the wrong bitwidth in the end, which triggered an assert.

Now, we evaluate the cast according to the standard.

This bug could have been triggered using the Z3 CM according to
https://bugs.llvm.org/show_bug.cgi?id=44030

Fixes llvm#47570 llvm#43375

Reviewed By: martong

Differential Revision: https://reviews.llvm.org/D85528

(cherry picked from commit fd7efe3)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@haoNoQ haoNoQ

Labels
bugzilla Issues migrated from bugzilla clang:static analyzer
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
5 participants
@LebedevRI @zmodem @mikhailramalho @haoNoQ @steakhal