This patch adds a new descendant to the SymExpr hierarchy. This way, now we
can assign constraints to symbolic unary expressions. This time, only
the unary minus is handled, later patches might extend with other unary
operators.
Details
- Reviewers
NoQ steakhal Szelethus - Commits
- rGb5b2aec1ff51: [analyzer] Add UnarySymExpr
Diff Detail
- Repository
- rG LLVM Github Monorepo
Event Timeline
Looks great. It'll be a nice addition.
It feels like SymbolCast is a UnarySymExpr, but I like to have a distinct entity for this.
Anyway. There are a lot more places where we visit and handle all SymExpr kinds.
Such as:
SValExplainer, SymbolExpressor, SymbolicRangeInferrer, SimpleSValBuilder::simplifySValOnce()::Simplifier, TypeRetrievingVisitor.
Out of these, I think SValExplainer, SymbolExpressor, and TypeRetrievingVisitor are the crucial ones to have consistent behavior.
On top of these, the rest of them e.g. the constraint manager and simplification just improve the reasoning about these, so they probably can be done incrementally.
clang/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h | ||
---|---|---|
321 | This is always true, right? | |
325 | I would prefer distinct assertions. This way if it triggers we can know which condition is violated. | |
352 | I see that all the rest of the classes have this comment, but I found them not too useful. | |
clang/lib/StaticAnalyzer/Core/SValBuilder.cpp | ||
104 | I think we should assert that we expect only UO_Minus (-), UO_Not (~). | |
clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp | ||
108–109 | Also handle it here. | |
clang/lib/StaticAnalyzer/Core/SymbolManager.cpp | ||
73–76 | Have a test for this. |
Looks great!
I suspect you'll catch a few crashes/assertion failures if you run this on real-world code, due to various parts of the static analyzer being startled by the new thing, so I really recommend doing this.
clang/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h | ||
---|---|---|
338 | LLVM_DUMP_METHOD? | |
clang/lib/StaticAnalyzer/Core/SValBuilder.cpp | ||
104 | Actually, let's put such assertion in the constructor. The earlier we catch the problem the better. | |
clang/lib/StaticAnalyzer/Core/SymbolManager.cpp | ||
498 | Excellent! |
Thanks for the review guys!
It feels like SymbolCast is a UnarySymExpr, but I like to have a distinct entity for this.
Yes, their implementation is similar, but there are subtle differences.
Anyway. There are a lot more places where we visit and handle all SymExpr kinds.
Such as:
SValExplainer, SymbolExpressor, SymbolicRangeInferrer, SimpleSValBuilder::simplifySValOnce()::Simplifier, TypeRetrievingVisitor.Out of these, I think SValExplainer, SymbolExpressor, and TypeRetrievingVisitor are the crucial ones to have consistent behavior.
On top of these, the rest of them e.g. the constraint manager and simplification just improve the reasoning about these, so they probably can be done incrementally.
Okay, I've extended the SValExplainer, SymbolExpressor and the Simplifier. TypeRetrievingVisitor uses the virtual getType() function of SymExpr and we override that in UnarySymExpr, so that is already handled. I'd like to handle the constraint manager related things (SymbolicRangeInferrer) in a separate patch.
I suspect you'll catch a few crashes/assertion failures if you run this on real-world code, due to various parts of the static analyzer being startled by the new thing, so I really recommend doing this.
Yeah, I am on it.
clang/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h | ||
---|---|---|
321 | Yes. Maybe that is not meaningful anymore (since classof is impelented in the class properly). So I've deleted it. | |
325 | Ok, I've split them up. | |
338 | SymbolManager.cpp does that for the base class' function: LLVM_DUMP_METHOD void SymExpr::dump() const { dumpToStream(llvm::errs()); } | |
352 | I'd like to keep it consistent with the other classes, besides the comment might be useful for newcomers. | |
clang/lib/StaticAnalyzer/Core/SValBuilder.cpp | ||
104 | Ok, I've added the assertion to the ctor. | |
clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp | ||
108–109 | Ok, done. |
- Handle UnarySymExpr in SValExplainer
- Handle UnarySymExpr in SymbolExpressor
- Handle UnarySymExpr in SimpleSvalBuilder's Simplifier
- Better assertions
- Handle UO_Not
clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp | ||
---|---|---|
107 | I'm not sure if we should rely on SVal::getType(). I think the calling context should pass the type along here. |
clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp | ||
---|---|---|
107 | Good point. One example where the type of the SVal is different than the type of the UnaryExpr is here: void test_x(int x, long y) { x = y; // $x has `long` type -x; // the UnaryExpr `-x` has `int` type } Note that if we use support-symbolic-integer-casts=true then there is no such type mismatch because there is in implicit cast modeled at x = y, thus $x type is correctly int. Anyway, I am going to update evalMinus and evalComplement to take an additional QualType parameter. | |
clang/lib/StaticAnalyzer/Core/SymbolManager.cpp | ||
73–76 | Would be better to add parenthesis around for compound expressions. So expressions like -x where x = a + b should look like -($a + $b) instead of the wrong format -$a + $b. I am going to update. |
- Add type parameter to evalMinus and evalComplement
- Correct dumpToStream in case of binary sub expressions
clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp | ||
---|---|---|
107 | Please add this test with both scenarios with support-symbolic-integer-casts. D125532 will help in demonstrating this. | |
clang/lib/StaticAnalyzer/Core/SymbolManager.cpp | ||
73–76 | Good point! | |
clang/test/Analysis/unary-sym-expr.c | ||
36 | Does it work if you swap x and y? |
clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp | ||
---|---|---|
107 | Ahh, unfortunately, if we use the type of the AST's UnaryExpr instead of the operand SVal then we will end up crashing the constraint solver, because of the missing SymbolCast below: void crash(int b, long c) { b = c; if (b > 0) // $b is long if(-b) // should not crash here // $-b is int ; // SymbolicRangeInferrer // takes the negated range of $-b (with type int) // getRangeForNegatedSub // and takes the range of $b (with type long) and tries to intersect them. // RangeSet VisitSymExpr(SymbolRef Sym) } This manifests in the child patch, because that's where we add the support of UnarySymExpr to the solver, so I add a test case there. |
clang/test/Analysis/unary-sym-expr.c | ||
---|---|---|
36 | No, that does not. And the reason of that is we cannot handle commutativity (yet). |
clang/test/Analysis/unary-sym-expr.c | ||
---|---|---|
36 | We could still test it, and put there a FIXME. |
clang/test/Analysis/unary-sym-expr.c | ||
---|---|---|
36 | Ok, added a fixme. |
This is always true, right?