forked from OSchip/llvm-project
[Analyzer] Mark `SymbolData` parts of iterator position as live in program state maps
Marking a symbolic expression as live is non-recursive. In our checkers we either use conjured symbols or conjured symbols plus/minus integers to represent abstract position of iterators, so in this latter case we also must mark the `SymbolData` part of these symbolic expressions as live to prevent them from getting reaped. Differential Revision: https://reviews.llvm.org/D48764 llvm-svn: 337151
This commit is contained in:
parent
0a75de4bfe
commit
0a7592b5e2
|
@ -488,14 +488,18 @@ void IteratorChecker::checkLiveSymbols(ProgramStateRef State,
|
|||
// alive
|
||||
auto RegionMap = State->get<IteratorRegionMap>();
|
||||
for (const auto Reg : RegionMap) {
|
||||
const auto Pos = Reg.second;
|
||||
SR.markLive(Pos.getOffset());
|
||||
const auto Offset = Reg.second.getOffset();
|
||||
for (auto i = Offset->symbol_begin(); i != Offset->symbol_end(); ++i)
|
||||
if (isa<SymbolData>(*i))
|
||||
SR.markLive(*i);
|
||||
}
|
||||
|
||||
auto SymbolMap = State->get<IteratorSymbolMap>();
|
||||
for (const auto Sym : SymbolMap) {
|
||||
const auto Pos = Sym.second;
|
||||
SR.markLive(Pos.getOffset());
|
||||
const auto Offset = Sym.second.getOffset();
|
||||
for (auto i = Offset->symbol_begin(); i != Offset->symbol_end(); ++i)
|
||||
if (isa<SymbolData>(*i))
|
||||
SR.markLive(*i);
|
||||
}
|
||||
|
||||
auto ContMap = State->get<ContainerMap>();
|
||||
|
@ -1157,21 +1161,31 @@ ProgramStateRef relateIteratorPositions(ProgramStateRef State,
|
|||
const IteratorPosition &Pos2,
|
||||
bool Equal) {
|
||||
auto &SVB = State->getStateManager().getSValBuilder();
|
||||
|
||||
// FIXME: This code should be reworked as follows:
|
||||
// 1. Subtract the operands using evalBinOp().
|
||||
// 2. Assume that the result doesn't overflow.
|
||||
// 3. Compare the result to 0.
|
||||
// 4. Assume the result of the comparison.
|
||||
const auto comparison =
|
||||
SVB.evalBinOp(State, BO_EQ, nonloc::SymbolVal(Pos1.getOffset()),
|
||||
nonloc::SymbolVal(Pos2.getOffset()), SVB.getConditionType())
|
||||
.getAs<DefinedSVal>();
|
||||
nonloc::SymbolVal(Pos2.getOffset()),
|
||||
SVB.getConditionType());
|
||||
|
||||
if (comparison) {
|
||||
auto NewState = State->assume(*comparison, Equal);
|
||||
if (const auto CompSym = comparison->getAsSymbol()) {
|
||||
return assumeNoOverflow(NewState, cast<SymIntExpr>(CompSym)->getLHS(), 2);
|
||||
}
|
||||
assert(comparison.getAs<DefinedSVal>() &&
|
||||
"Symbol comparison must be a `DefinedSVal`");
|
||||
|
||||
return NewState;
|
||||
auto NewState = State->assume(comparison.castAs<DefinedSVal>(), Equal);
|
||||
if (const auto CompSym = comparison.getAsSymbol()) {
|
||||
assert(isa<SymIntExpr>(CompSym) &&
|
||||
"Symbol comparison must be a `SymIntExpr`");
|
||||
assert(BinaryOperator::isComparisonOp(
|
||||
cast<SymIntExpr>(CompSym)->getOpcode()) &&
|
||||
"Symbol comparison must be a comparison");
|
||||
return assumeNoOverflow(NewState, cast<SymIntExpr>(CompSym)->getLHS(), 2);
|
||||
}
|
||||
|
||||
return State;
|
||||
return NewState;
|
||||
}
|
||||
|
||||
bool isZero(ProgramStateRef State, const NonLoc &Val) {
|
||||
|
@ -1225,14 +1239,12 @@ bool compare(ProgramStateRef State, NonLoc NL1, NonLoc NL2,
|
|||
auto &SVB = State->getStateManager().getSValBuilder();
|
||||
|
||||
const auto comparison =
|
||||
SVB.evalBinOp(State, Opc, NL1, NL2, SVB.getConditionType())
|
||||
.getAs<DefinedSVal>();
|
||||
SVB.evalBinOp(State, Opc, NL1, NL2, SVB.getConditionType());
|
||||
|
||||
if (comparison) {
|
||||
return !State->assume(*comparison, false);
|
||||
}
|
||||
assert(comparison.getAs<DefinedSVal>() &&
|
||||
"Symbol comparison must be a `DefinedSVal`");
|
||||
|
||||
return false;
|
||||
return !State->assume(comparison.castAs<DefinedSVal>(), false);
|
||||
}
|
||||
|
||||
} // namespace
|
||||
|
|
Loading…
Reference in New Issue