Skip to content

Commit

Permalink
[analyzer][solver] Track symbol equivalence
Browse files Browse the repository at this point in the history
Summary:
For the most cases, we try to reason about symbol either based on the
information we know about that symbol in particular or about its
composite parts.  This is faster and eliminates costly brute force
searches through existing constraints.

However, we do want to support some cases that are widespread enough
and involve reasoning about different existing constraints at once.
These include:
  * resoning about 'a - b' based on what we know about 'b - a'
  * reasoning about 'a <= b' based on what we know about 'a > b' or 'a < b'

This commit expands on that part by tracking symbols known to be equal
while still avoiding brute force searches.  It changes the way we track
constraints for individual symbols.  If we know for a fact that 'a == b'
then there is no need in tracking constraints for both 'a' and 'b' especially
if these constraints are different.  This additional relationship makes
dead/live logic for constraints harder as we want to maintain as much
information on the equivalence class as possible, but we still won't
carry the information that we don't need anymore.

Differential Revision: https://reviews.llvm.org/D82445
  • Loading branch information
SavchenkoValeriy committed Jul 22, 2020
1 parent f531c1c commit b13d987
Show file tree
Hide file tree
Showing 6 changed files with 797 additions and 66 deletions.
Expand Up @@ -373,7 +373,7 @@ class SuppressInlineDefensiveChecksVisitor final : public BugReporterVisitor {
class FalsePositiveRefutationBRVisitor final : public BugReporterVisitor {
private:
/// Holds the constraints in a given path
ConstraintRangeTy Constraints;
ConstraintMap Constraints;

public:
FalsePositiveRefutationBRVisitor();
Expand All @@ -390,7 +390,6 @@ class FalsePositiveRefutationBRVisitor final : public BugReporterVisitor {
bool OverwriteConstraintsOnExistingSyms);
};


/// The visitor detects NoteTags and displays the event notes they contain.
class TagVisitor : public BugReporterVisitor {
public:
Expand Down
Expand Up @@ -136,14 +136,8 @@ class RangeSet {
}
};

class ConstraintRange {};
using ConstraintRangeTy = llvm::ImmutableMap<SymbolRef, RangeSet>;

template <>
struct ProgramStateTrait<ConstraintRange>
: public ProgramStatePartialTrait<ConstraintRangeTy> {
static void *GDMIndex();
};
using ConstraintMap = llvm::ImmutableMap<SymbolRef, RangeSet>;
ConstraintMap getConstraintMap(ProgramStateRef State);

class RangedConstraintManager : public SimpleConstraintManager {
public:
Expand Down Expand Up @@ -222,4 +216,6 @@ class RangedConstraintManager : public SimpleConstraintManager {
} // namespace ento
} // namespace clang

REGISTER_FACTORY_WITH_PROGRAMSTATE(ConstraintMap)

#endif
7 changes: 3 additions & 4 deletions clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
Expand Up @@ -2813,7 +2813,7 @@ UndefOrNullArgVisitor::VisitNode(const ExplodedNode *N, BugReporterContext &BRC,
//===----------------------------------------------------------------------===//

FalsePositiveRefutationBRVisitor::FalsePositiveRefutationBRVisitor()
: Constraints(ConstraintRangeTy::Factory().getEmptyMap()) {}
: Constraints(ConstraintMap::Factory().getEmptyMap()) {}

void FalsePositiveRefutationBRVisitor::finalizeVisitor(
BugReporterContext &BRC, const ExplodedNode *EndPathNode,
Expand Down Expand Up @@ -2855,9 +2855,8 @@ void FalsePositiveRefutationBRVisitor::finalizeVisitor(
void FalsePositiveRefutationBRVisitor::addConstraints(
const ExplodedNode *N, bool OverwriteConstraintsOnExistingSyms) {
// Collect new constraints
const ConstraintRangeTy &NewCs = N->getState()->get<ConstraintRange>();
ConstraintRangeTy::Factory &CF =
N->getState()->get_context<ConstraintRange>();
ConstraintMap NewCs = getConstraintMap(N->getState());
ConstraintMap::Factory &CF = N->getState()->get_context<ConstraintMap>();

// Add constraints if we don't have them yet
for (auto const &C : NewCs) {
Expand Down

0 comments on commit b13d987

Please sign in to comment.