This is an archive of the discontinued LLVM Phabricator instance.

[Analyzer][solver] Fix crashes during symbol simplification
ClosedPublic

Authored by martong on Jun 24 2021, 3:06 AM.

Details

Summary

Consider the code

void f(int a0, int b0, int c)
{
    int a1 = a0 - b0;
    int b1 = (unsigned)a1 + c;
    if (c == 0) {
        int d = 7L / b1;
    }
}

At the point of divisiion by b1 that is considered to be non-zero,
which results in a new constraint for $a0 - $b0 + $c. The type
of this sym is unsigned, however, the simplified sym is `$a0 -
$b0` and its type is signed. This is probably the result of the
inherent improper handling of casts. Anyway, Range assignment
for constraints use this type information. Therefore, we must
make sure that first we simplify the symbol and only then we
assign the range.

Diff Detail

Event Timeline

martong created this revision.Jun 24 2021, 3:06 AM
martong requested review of this revision.Jun 24 2021, 3:06 AM
Herald added a project: Restricted Project. · View Herald TranscriptJun 24 2021, 3:06 AM
Herald added a subscriber: cfe-commits. · View Herald Transcript
martong added a reviewer: NoQ.Jun 24 2021, 3:10 AM
vsavchenko added inline comments.Jun 24 2021, 4:04 AM
clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
2307–2308

I don't like the idea of duplicating it into every assume method. This way we drastically increase our chances to forget it (like you did with assumeSymGE and assumeSymLE).
I think the better place for it is in RangedConstraintManager::assumeSymRel and neighboring methods, though still not perfect.
I don't really get why we get not simplified symbol to begin with.

martong added inline comments.Jun 24 2021, 7:59 AM
clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
2307–2308

assumeSymRel is not enough, because e.g. assumeSymGE is called also e.g. from assumeSymUnsupported. Perhaps we could change the signature of assumeSymEQ/NE/GT/GE/LT/LE to take an auxiliary Simplifier wrapper object instead of SymbolRef?

ProgramStateRef assumeSymNE(ProgramStateRef State, Simplifier S,
                                    const llvm::APSInt &V,
                                    const llvm::APSInt &Adjustment);

And for the Simplifier something like:

struct Simplifier {
  SymbolRef SimplifiedSym = nullptr;
  Simplifier(SymbolRef Sym) : SimplifiedSym(simplify(Sym)) {}
  
};

I don't really get why we get not simplified symbol to begin with.

This is because of the Environment bindings. I.e. b1 is bound to $a0 - $b0 + $c when we evaluate int b1 = (unsigned)a1 + c;. This binding is not changed/updated, so when we evaluate the division then we query the DeclRefExpr for b1 from the Environment and that gives still $a0 - $b0 + $c. We either do the simplification in the ConstraintManager (as we do now with this and the parent patch) or perhaps we could try to simplify the Environment bindings as an alternative solution.

I don't really get why we get not simplified symbol to begin with.

This is because of the Environment bindings. I.e. b1 is bound to $a0 - $b0 + $c when we evaluate int b1 = (unsigned)a1 + c;. This binding is not changed/updated, so when we evaluate the division then we query the DeclRefExpr for b1 from the Environment and that gives still $a0 - $b0 + $c. We either do the simplification in the ConstraintManager (as we do now with this and the parent patch) or perhaps we could try to simplify the Environment bindings as an alternative solution.

Yeah, I remember now, thanks!

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
2307–2308

assumeSymRel is not enough, because e.g. assumeSymGE is called also e.g. from assumeSymUnsupported.

Yep, that's why I suggested assumeSymRel and its neighbors. I actually think that three top-level public methods from RangedConstraintManager will do: assumeSym, assumeSymInclusiveRange, and assumeSymUnsupported.

We can't really change the signatures of those methods because we'll be introducing this functionality into solvers that didn't sign up for this (and don't need it).

Also we can least put this if statement inside of simplify, so we can use it like this: Sym = simplify(St, Sym);.

martong updated this revision to Diff 354274.Jun 24 2021, 9:01 AM
  • Use simplify from RangedConstraintManager
martong marked 2 inline comments as done.Jun 24 2021, 9:01 AM
martong added inline comments.
clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
2307–2308

Okay, I've updated like so.

Awesome, thanks for swiftly addressing it!

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

Oof, and there is no way to avoid all these namespaces?

vsavchenko accepted this revision.Jun 24 2021, 9:05 AM
This revision is now accepted and ready to land.Jun 24 2021, 9:05 AM
martong marked 2 inline comments as done.Jun 25 2021, 2:48 AM

Valeriy, thanks for the assiduous and quick review!

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

Unfortunately, the candidate function would be the member simplify in that case. Though, we can get rid of the ::clang prefix.

This revision was automatically updated to reflect the committed changes.
martong marked an inline comment as done.
vsavchenko added inline comments.Jun 25 2021, 2:56 AM
clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
1981

OK, at least ento::!