This is an archive of the discontinued LLVM Phabricator instance.

[Analyzer][solver] Simplification: reorganize equalities with adjustment
ClosedPublic

Authored by martong on Oct 12 2021, 6:29 AM.

Details

Summary

Initiate the reorganization of the equality information during symbol
simplification. E.g., if we bump into c + 1 == 0 during simplification
then we'd like to express that c == -1. It makes sense to do this only
with SymIntExprs.

Diff Detail

Event Timeline

martong created this revision.Oct 12 2021, 6:29 AM
martong requested review of this revision.Oct 12 2021, 6:29 AM
Herald added a project: Restricted Project. · View Herald TranscriptOct 12 2021, 6:29 AM
Herald added a subscriber: cfe-commits. · View Herald Transcript

The coverage report of the test shows that L2124 is uncovered. Please add a test demonstrating that path as well.
I'm gonna come back to this tomorrow.

clang/test/Analysis/solver-sym-simplification-adjustment.c
37

Please express that C: [-2,-1] is then intersected with the already associated range which is [-1,1], thus we get c: [-1,-1].

56

Can we infer within this true branch that b must be 0 to make this path feasible?
If we already can infer this, can we put there the appropriate assertion?
If not, an assertion would be justified with a FIXME.

steakhal added inline comments.Oct 14 2021, 6:23 AM
clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
2126–2130

Can the simplification of a SymSymExpr result in IntSymExpr? If it can happen, then we could see such instances and we should do the right thing with them as well.
WDYT?

martong updated this revision to Diff 381520.Oct 22 2021, 5:45 AM
martong marked 3 inline comments as done.
  • Add comment about intersection in the test file
  • Add check in the feasible case in the test file
martong updated this revision to Diff 381536.Oct 22 2021, 7:15 AM
  • Add a test to cover if (OldState == State)

The coverage report of the test shows that L2124 is uncovered. Please add a test demonstrating that path as well.

I've added such a test, thanks for the notice!

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
2126–2130

Can the simplification of a SymSymExpr result in IntSymExpr?

Yes it can. However, in order to handle them we should extend computeAdjustment properly, which is absolutely not trivial - considering the test cases in additive-folding.cpp - So, I'd rather address that in another patch.

clang/test/Analysis/solver-sym-simplification-adjustment.c
37

Ok, I've added that comment.

56

Can we infer within this true branch that b must be 0 to make this path feasible?

Yes, we can.

If we already can infer this, can we put there the appropriate assertion?

Ok, I've added the appropriate clang_analyzer_eval to check this.

steakhal accepted this revision.Oct 25 2021, 2:06 AM

Awesome!
So clean, and I also like the tests.
Good job.

clang/test/Analysis/solver-sym-simplification-adjustment.c
59

Please assert clang_analyzer_eval(c == 0) as well.

This revision is now accepted and ready to land.Oct 25 2021, 2:06 AM
This revision was landed with ongoing or failed builds.Oct 27 2021, 7:49 AM
This revision was automatically updated to reflect the committed changes.
martong marked an inline comment as done.Oct 27 2021, 7:49 AM

Thanks for the assiduous review guys!