Page MenuHomePhabricator

[analyzer][solver][NFC] Introduce ConstraintAssignor
ClosedPublic

Authored by vsavchenko on Jul 9 2021, 4:50 AM.

Details

Summary

The new component is a symmetric response to SymbolicRangeInferrer.
While the latter is the unified component, which answers all the
questions what does the solver knows about a particular symbolic
expression, assignor associates new constraints (aka "assumes")
with symbolic expressions and can imply additional knowledge that
the solver can extract and use later on.

  • Why do we need it and why is SymbolicRangeInferrer not enough?

As it is noted before, the inferrer only helps us to get the most
precise range information based on the existing knowledge and on the
mathematical foundations of different operations that symbolic
expressions actually represent. It doesn't introduce new constraints.

The assignor, on the other hand, can impose constraints on other
symbols using the same domain knowledge.

  • But for some expressions, SymbolicRangeInferrer looks into constraints for similar expressions, why can't we do that for all the cases?

That's correct! But in order to do something like this, we should
have a finite number of possible "similar expressions".

Let's say we are asked about $a - $b and we know something about
$b - $a. The inferrer can invert this expression and check
constraints for $b - $a. This is simple!
But let's say we are asked about $a and we know that $a * $b != 0.
In this situation, we can imply that $a != 0, but the inferrer shouldn't
try every possible symbolic expression X to check if $a * X or
X * $a is constrained to non-zero.

With the assignor mechanism, we can catch this implication right at
the moment we associate $a * $b with non-zero range, and set similar
constraints for $a and $b as well.

Diff Detail

Event Timeline

vsavchenko created this revision.Jul 9 2021, 4:50 AM
vsavchenko requested review of this revision.Jul 9 2021, 4:50 AM
Herald added a project: Restricted Project. · View Herald TranscriptJul 9 2021, 4:50 AM
Herald added a subscriber: cfe-commits. · View Herald Transcript
martong accepted this revision.Jul 9 2021, 8:20 AM

Generally it looks okay to me. However, I have a question:
In SimpleSValBuilder::evalBinOpNN we do infer values to symbols. E.g. if we have an expression y / x and y is known to be 0 then we assign 0 to the division expression. On one hand, this logic is independent from whichever solver implementation we use. On the other hand, we do the value inferring based on the fact that y is a constrainted to be in [0, 0] so in this sense this infer logic should be in the solver.
What do you think, perhaps another round of refactoring should move that logic into the solver?

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
1388

New now, but it might be old after a while.

1394

typo, can.

This revision is now accepted and ready to land.Jul 9 2021, 8:20 AM
vsavchenko added inline comments.Jul 9 2021, 9:00 AM
clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
1388

Whoops, this is how I first named the class. It is not new handler, but new constraint. Because of this ambiguity I actually renamed it 😅

Uhh, what the hell happened with the Stack?

Fix comments

This revision was landed with ongoing or failed builds.Jul 13 2021, 11:01 AM
This revision was automatically updated to reflect the committed changes.

Hi,

When compiling with gcc I see the following new warnings with this patch:

[4/22] Building CXX object tools/clang/lib/StaticAnalyzer/Core/CMakeFiles/obj.clangStaticAnalyzerCore.dir/RangeConstraintManager.cpp.o
/repo/uabelho/master-github/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:2395:17: warning: 'clang::ento::ProgramStateRef {anonymous}::RangeConstraintManager::setRange(clang::ento::ProgramStateRef, {anonymous}::EquivalenceClass, clang::ento::RangeSet)' defined but not used [-Wunused-function]
 2395 | ProgramStateRef RangeConstraintManager::setRange(ProgramStateRef State,
      |                 ^~~~~~~~~~~~~~~~~~~~~~
/repo/uabelho/master-github/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:2384:10: warning: 'clang::ento::RangeSet {anonymous}::RangeConstraintManager::getRange(clang::ento::ProgramStateRef, {anonymous}::EquivalenceClass)' defined but not used [-Wunused-function]
 2384 | RangeSet RangeConstraintManager::getRange(ProgramStateRef State,
      |          ^~~~~~~~~~~~~~~~~~~~~~

Will those methods be used or can they be removed?

Hi,

When compiling with gcc I see the following new warnings with this patch:

[4/22] Building CXX object tools/clang/lib/StaticAnalyzer/Core/CMakeFiles/obj.clangStaticAnalyzerCore.dir/RangeConstraintManager.cpp.o
/repo/uabelho/master-github/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:2395:17: warning: 'clang::ento::ProgramStateRef {anonymous}::RangeConstraintManager::setRange(clang::ento::ProgramStateRef, {anonymous}::EquivalenceClass, clang::ento::RangeSet)' defined but not used [-Wunused-function]
 2395 | ProgramStateRef RangeConstraintManager::setRange(ProgramStateRef State,
      |                 ^~~~~~~~~~~~~~~~~~~~~~
/repo/uabelho/master-github/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:2384:10: warning: 'clang::ento::RangeSet {anonymous}::RangeConstraintManager::getRange(clang::ento::ProgramStateRef, {anonymous}::EquivalenceClass)' defined but not used [-Wunused-function]
 2384 | RangeSet RangeConstraintManager::getRange(ProgramStateRef State,
      |          ^~~~~~~~~~~~~~~~~~~~~~

Will those methods be used or can they be removed?

I think they can be removed, waiting for Valeriy's approval.
https://reviews.llvm.org/D106063

Hi,

When compiling with gcc I see the following new warnings with this patch:

[4/22] Building CXX object tools/clang/lib/StaticAnalyzer/Core/CMakeFiles/obj.clangStaticAnalyzerCore.dir/RangeConstraintManager.cpp.o
/repo/uabelho/master-github/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:2395:17: warning: 'clang::ento::ProgramStateRef {anonymous}::RangeConstraintManager::setRange(clang::ento::ProgramStateRef, {anonymous}::EquivalenceClass, clang::ento::RangeSet)' defined but not used [-Wunused-function]
 2395 | ProgramStateRef RangeConstraintManager::setRange(ProgramStateRef State,
      |                 ^~~~~~~~~~~~~~~~~~~~~~
/repo/uabelho/master-github/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:2384:10: warning: 'clang::ento::RangeSet {anonymous}::RangeConstraintManager::getRange(clang::ento::ProgramStateRef, {anonymous}::EquivalenceClass)' defined but not used [-Wunused-function]
 2384 | RangeSet RangeConstraintManager::getRange(ProgramStateRef State,
      |          ^~~~~~~~~~~~~~~~~~~~~~

Will those methods be used or can they be removed?

I think they can be removed, waiting for Valeriy's approval.
https://reviews.llvm.org/D106063

Thanks!