[PATCH] D126481: [analyzer] Handle SymbolCast in SValBuilder

martong added a comment. I don't see this case different to the unary expressions. Consider the unary minus for example. Let's say, the symbol `a` is constrained to `[1, 1]` and then `-a` is constrained to `[-2, -2]`. This is clearly an infeasible state and the analyzer will terminate the

[PATCH] D126481: [analyzer] Handle SymbolCast in SValBuilder

ASDenysPetrov added a comment. @martong > So, the intersection should be empty in the above mentioned ambiguous case, > shouldn't' it? No. My current implementation doesn't contain this check in ConstraintAssignor in favor of the solution simplification. It'll be added in the next patches.

[PATCH] D126481: [analyzer] Handle SymbolCast in SValBuilder

martong added a comment. Actually, you already have a logic for checking if there is a contradiction in your D103096 patch, in ConstraintAssignor::updateExistingConstraints: // Update constraints in the map which bitwidth is equal or lower then //

[PATCH] D126481: [analyzer] Handle SymbolCast in SValBuilder

martong added a comment. > Suppose we have found the way to handle it. But what if we find a > contradiction while simplifying, like (short)(int x) = 0 and (int x) = 1. So > that we would already know that it is impossible. What SVal should we return > in such case? Undef? Unknown? Original

[PATCH] D126481: [analyzer] Handle SymbolCast in SValBuilder

ASDenysPetrov added a comment. @martong > Then we can iterate onto the solution. What we could do is to collect the > constants and types on the way of the cast visitation and then apply the same > logic that you have in D103096 . Suppose we have found the

[PATCH] D126481: [analyzer] Handle SymbolCast in SValBuilder

ASDenysPetrov added a comment. In D126481#3818769 , @martong wrote: > Yeah okay. I get it now. Thank you for your patience and your time on > elaborating the issue. > > First, I think we'd need to fabricate a test case that shows us the bug even >

[PATCH] D126481: [analyzer] Handle SymbolCast in SValBuilder

martong added a comment. Yeah okay. I get it now. Thank you for your patience and your time on elaborating the issue. First, I think we'd need to fabricate a test case that shows us the bug even without applying your patch (D103096 ). Then we can iterate

[PATCH] D126481: [analyzer] Handle SymbolCast in SValBuilder

ASDenysPetrov added a comment. @martong wrote: I think you did get it. I'm not talking about range but about concrete int. And I see that the current behavior needs an improvement or rework. Consider next code, which I used in my example: 1. void test(int x) { 2. assert((short)x == 0);

[PATCH] D126481: [analyzer] Handle SymbolCast in SValBuilder

martong added a comment. > Assume we have `(int)(short)(int x)`. `VisitSymbolCast` will try to get the > constant recursively in the next order: > > - `(short)(int x)` > - `(int x)` > > And here is my concern. Whether it is correct to get the range for `int x` > and consider it as a correct

[PATCH] D126481: [analyzer] Handle SymbolCast in SValBuilder

ASDenysPetrov reopened this revision. ASDenysPetrov added a comment. This revision is now accepted and ready to land. I've just investigated this patch deeply. I think we have wrong logic here. Assume we have `(int)(short)(int x)`. `VisitSymbolCast` will try to get the constant recursively in

[PATCH] D126481: [analyzer] Handle SymbolCast in SValBuilder

This revision was landed with ongoing or failed builds. This revision was automatically updated to reflect the committed changes. martong marked an inline comment as done. Closed by commit rG160798ab9be8: [analyzer] Handle SymbolCast in SValBuilder (authored by martong). Repository: rG LLVM

[PATCH] D126481: [analyzer] Handle SymbolCast in SValBuilder

ASDenysPetrov accepted this revision. ASDenysPetrov added a comment. This revision is now accepted and ready to land. In D126481#3545350 , @martong wrote: > This part of the SValBuilder is responsible for **constant folding**. We need > this constant

[PATCH] D126481: [analyzer] Handle SymbolCast in SValBuilder

martong marked an inline comment as done. martong added a comment. In D126481#3542919 , @ASDenysPetrov wrote: > @martong As you said, my solution D103096 > suppose to pass these and more other tests cases. So how it

[PATCH] D126481: [analyzer] Handle SymbolCast in SValBuilder

ASDenysPetrov added a comment. @martong As you said, my solution D103096 suppose to pass these and more other tests cases. So how it will help in combination with my solution D103096 ? Although, your patch is really simple

[PATCH] D126481: [analyzer] Handle SymbolCast in SValBuilder

martong updated this revision to Diff 432588. martong marked 7 inline comments as done. martong added a comment. - Hoist S->getOperand, rework the test file Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D126481/new/ https://reviews.llvm.org/D126481

[PATCH] D126481: [analyzer] Handle SymbolCast in SValBuilder

martong added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:1359 + return cache(S, + SVB.evalCast(Op, S->getType(), S->getOperand()->getType())); +} steakhal wrote: > Hoist this common subexpression.

[PATCH] D126481: [analyzer] Handle SymbolCast in SValBuilder

steakhal added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:1359 + return cache(S, + SVB.evalCast(Op, S->getType(), S->getOperand()->getType())); +} Hoist this common subexpression.

[PATCH] D126481: [analyzer] Handle SymbolCast in SValBuilder

martong created this revision. martong added reviewers: ASDenysPetrov, steakhal, NoQ. Herald added subscribers: manas, gamesh411, dkrupp, donat.nagy, Szelethus, mikhail.ramalho, a.sidorin, rnkovacs, szepet, baloghadamsoftware, xazax.hun. Herald added a reviewer: Szelethus. Herald added a project: