This is an archive of the discontinued LLVM Phabricator instance.

[analyzer] Add UnarySymExpr
ClosedPublic

Authored by martong on May 10 2022, 8:23 AM.

Details

Summary

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.

Diff Detail

Event Timeline

martong created this revision.May 10 2022, 8:23 AM
Herald added a project: Restricted Project. · View Herald Transcript
martong requested review of this revision.May 10 2022, 8:23 AM
Herald added a project: Restricted Project. · View Herald TranscriptMay 10 2022, 8:23 AM
Herald added a subscriber: cfe-commits. · View Herald Transcript
steakhal requested changes to this revision.May 10 2022, 9:04 AM

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
107

I think we should assert that we expect only UO_Minus (-), UO_Not (~).
The rest of the UO_* doesn't seem to be relevant anyway: PostInc, PostDec, PreInc, PreDec, AddrOf, Deref, Plus, LNot, Real, Imag, Extension, Coawait.

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.

This revision now requires changes to proceed.May 10 2022, 9:04 AM
NoQ added a comment.May 10 2022, 9:05 PM

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
107

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!

martong marked 9 inline comments as done.May 11 2022, 2:51 AM

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
107

Ok, I've added the assertion to the ctor.

clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
108–109

Ok, done.

martong updated this revision to Diff 428601.May 11 2022, 2:51 AM
martong marked 6 inline comments as done.
  • Handle UnarySymExpr in SValExplainer
  • Handle UnarySymExpr in SymbolExpressor
  • Handle UnarySymExpr in SimpleSvalBuilder's Simplifier
  • Better assertions
  • Handle UO_Not
steakhal added inline comments.May 11 2022, 5:39 AM
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.

martong marked an inline comment as done.May 12 2022, 11:48 PM
martong added inline comments.
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.

martong updated this revision to Diff 429152.May 13 2022, 12:04 AM
martong marked an inline comment as done.
  • Add type parameter to evalMinus and evalComplement
  • Correct dumpToStream in case of binary sub expressions
steakhal added inline comments.May 13 2022, 3:40 AM
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?

martong added inline comments.May 13 2022, 5:19 AM
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.

martong updated this revision to Diff 429207.May 13 2022, 5:20 AM
  • Revert "Add type parameter to evalMinus and evalComplement"
martong marked 2 inline comments as done.May 13 2022, 5:31 AM
martong added inline comments.
clang/test/Analysis/unary-sym-expr.c
36

No, that does not. And the reason of that is we cannot handle commutativity (yet).

steakhal accepted this revision.May 16 2022, 1:54 AM
steakhal added inline comments.
clang/test/Analysis/unary-sym-expr.c
36

We could still test it, and put there a FIXME.

This revision is now accepted and ready to land.May 16 2022, 1:54 AM
This revision was landed with ongoing or failed builds.May 26 2022, 5:17 AM
This revision was automatically updated to reflect the committed changes.
martong marked 2 inline comments as done.
martong added inline comments.May 26 2022, 5:18 AM
clang/test/Analysis/unary-sym-expr.c
36

Ok, added a fixme.