forked from OSchip/llvm-project
[analyzer] Refactor and simplify SimpleConstraintManager
Summary: SimpleConstraintManager is difficult to use, and makes assumptions about capabilities of the constraint manager. This patch refactors out those portions into a new RangedConstraintManager, and also fixes some issues with camel case, formatting, and confusing naming. Reviewers: zaks.anna, dcoughlin Subscribers: mgorny, xazax.hun, NoQ, rgov, cfe-commits Differential Revision: https://reviews.llvm.org/D26061 llvm-svn: 296242
This commit is contained in:
parent
9488560bb8
commit
9bc02cee8d
|
@ -139,6 +139,8 @@ public:
|
|||
return nullptr;
|
||||
}
|
||||
|
||||
/// Scan all symbols referenced by the constraints. If the symbol is not
|
||||
/// alive, remove it.
|
||||
virtual ProgramStateRef removeDeadBindings(ProgramStateRef state,
|
||||
SymbolReaper& SymReaper) = 0;
|
||||
|
||||
|
|
|
@ -0,0 +1,92 @@
|
|||
//== SimpleConstraintManager.h ----------------------------------*- C++ -*--==//
|
||||
//
|
||||
// The LLVM Compiler Infrastructure
|
||||
//
|
||||
// This file is distributed under the University of Illinois Open Source
|
||||
// License. See LICENSE.TXT for details.
|
||||
//
|
||||
//===----------------------------------------------------------------------===//
|
||||
//
|
||||
// Simplified constraint manager backend.
|
||||
//
|
||||
//===----------------------------------------------------------------------===//
|
||||
|
||||
#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SIMPLECONSTRAINTMANAGER_H
|
||||
#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SIMPLECONSTRAINTMANAGER_H
|
||||
|
||||
#include "clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h"
|
||||
#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
|
||||
|
||||
namespace clang {
|
||||
|
||||
namespace ento {
|
||||
|
||||
class SimpleConstraintManager : public ConstraintManager {
|
||||
SubEngine *SU;
|
||||
SValBuilder &SVB;
|
||||
|
||||
public:
|
||||
SimpleConstraintManager(SubEngine *subengine, SValBuilder &SB)
|
||||
: SU(subengine), SVB(SB) {}
|
||||
|
||||
~SimpleConstraintManager() override;
|
||||
|
||||
//===------------------------------------------------------------------===//
|
||||
// Implementation for interface from ConstraintManager.
|
||||
//===------------------------------------------------------------------===//
|
||||
|
||||
/// Ensures that the DefinedSVal conditional is expressed as a NonLoc by
|
||||
/// creating boolean casts to handle Loc's.
|
||||
ProgramStateRef assume(ProgramStateRef State, DefinedSVal Cond,
|
||||
bool Assumption) override;
|
||||
|
||||
ProgramStateRef assumeInclusiveRange(ProgramStateRef State, NonLoc Value,
|
||||
const llvm::APSInt &From,
|
||||
const llvm::APSInt &To,
|
||||
bool InRange) override;
|
||||
|
||||
protected:
|
||||
//===------------------------------------------------------------------===//
|
||||
// Interface that subclasses must implement.
|
||||
//===------------------------------------------------------------------===//
|
||||
|
||||
/// Given a symbolic expression that can be reasoned about, assume that it is
|
||||
/// true/false and generate the new program state.
|
||||
virtual ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym,
|
||||
bool Assumption) = 0;
|
||||
|
||||
/// Given a symbolic expression within the range [From, To], assume that it is
|
||||
/// true/false and generate the new program state.
|
||||
/// This function is used to handle case ranges produced by a language
|
||||
/// extension for switch case statements.
|
||||
virtual ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State,
|
||||
SymbolRef Sym,
|
||||
const llvm::APSInt &From,
|
||||
const llvm::APSInt &To,
|
||||
bool InRange) = 0;
|
||||
|
||||
/// Given a symbolic expression that cannot be reasoned about, assume that
|
||||
/// it is zero/nonzero and add it directly to the solver state.
|
||||
virtual ProgramStateRef assumeSymUnsupported(ProgramStateRef State,
|
||||
SymbolRef Sym,
|
||||
bool Assumption) = 0;
|
||||
|
||||
//===------------------------------------------------------------------===//
|
||||
// Internal implementation.
|
||||
//===------------------------------------------------------------------===//
|
||||
|
||||
BasicValueFactory &getBasicVals() const { return SVB.getBasicValueFactory(); }
|
||||
SymbolManager &getSymbolManager() const { return SVB.getSymbolManager(); }
|
||||
|
||||
private:
|
||||
ProgramStateRef assume(ProgramStateRef State, NonLoc Cond, bool Assumption);
|
||||
|
||||
ProgramStateRef assumeAux(ProgramStateRef State, NonLoc Cond,
|
||||
bool Assumption);
|
||||
};
|
||||
|
||||
} // end GR namespace
|
||||
|
||||
} // end clang namespace
|
||||
|
||||
#endif
|
|
@ -34,6 +34,7 @@ add_clang_library(clangStaticAnalyzerCore
|
|||
PlistDiagnostics.cpp
|
||||
ProgramState.cpp
|
||||
RangeConstraintManager.cpp
|
||||
RangedConstraintManager.cpp
|
||||
RegionStore.cpp
|
||||
SValBuilder.cpp
|
||||
SVals.cpp
|
||||
|
|
|
@ -20,8 +20,8 @@ ConstraintManager::~ConstraintManager() {}
|
|||
|
||||
static DefinedSVal getLocFromSymbol(const ProgramStateRef &State,
|
||||
SymbolRef Sym) {
|
||||
const MemRegion *R = State->getStateManager().getRegionManager()
|
||||
.getSymbolicRegion(Sym);
|
||||
const MemRegion *R =
|
||||
State->getStateManager().getRegionManager().getSymbolicRegion(Sym);
|
||||
return loc::MemRegionVal(R);
|
||||
}
|
||||
|
||||
|
|
|
@ -12,7 +12,7 @@
|
|||
//
|
||||
//===----------------------------------------------------------------------===//
|
||||
|
||||
#include "SimpleConstraintManager.h"
|
||||
#include "RangedConstraintManager.h"
|
||||
#include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
|
||||
#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
|
||||
#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h"
|
||||
|
@ -282,12 +282,31 @@ REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintRange,
|
|||
RangeSet))
|
||||
|
||||
namespace {
|
||||
class RangeConstraintManager : public SimpleConstraintManager {
|
||||
RangeSet getRange(ProgramStateRef State, SymbolRef Sym);
|
||||
|
||||
class RangeConstraintManager : public RangedConstraintManager {
|
||||
public:
|
||||
RangeConstraintManager(SubEngine *SE, SValBuilder &SVB)
|
||||
: SimpleConstraintManager(SE, SVB) {}
|
||||
: RangedConstraintManager(SE, SVB) {}
|
||||
|
||||
//===------------------------------------------------------------------===//
|
||||
// Implementation for interface from ConstraintManager.
|
||||
//===------------------------------------------------------------------===//
|
||||
|
||||
bool canReasonAbout(SVal X) const override;
|
||||
|
||||
ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override;
|
||||
|
||||
const llvm::APSInt *getSymVal(ProgramStateRef State,
|
||||
SymbolRef Sym) const override;
|
||||
|
||||
ProgramStateRef removeDeadBindings(ProgramStateRef State,
|
||||
SymbolReaper &SymReaper) override;
|
||||
|
||||
void print(ProgramStateRef State, raw_ostream &Out, const char *nl,
|
||||
const char *sep) override;
|
||||
|
||||
//===------------------------------------------------------------------===//
|
||||
// Implementation for interface from RangedConstraintManager.
|
||||
//===------------------------------------------------------------------===//
|
||||
|
||||
ProgramStateRef assumeSymNE(ProgramStateRef State, SymbolRef Sym,
|
||||
const llvm::APSInt &V,
|
||||
|
@ -313,26 +332,19 @@ public:
|
|||
const llvm::APSInt &V,
|
||||
const llvm::APSInt &Adjustment) override;
|
||||
|
||||
ProgramStateRef assumeSymbolWithinInclusiveRange(
|
||||
ProgramStateRef assumeSymWithinInclusiveRange(
|
||||
ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
|
||||
const llvm::APSInt &To, const llvm::APSInt &Adjustment) override;
|
||||
|
||||
ProgramStateRef assumeSymbolOutOfInclusiveRange(
|
||||
ProgramStateRef assumeSymOutsideInclusiveRange(
|
||||
ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
|
||||
const llvm::APSInt &To, const llvm::APSInt &Adjustment) override;
|
||||
|
||||
const llvm::APSInt *getSymVal(ProgramStateRef St,
|
||||
SymbolRef Sym) const override;
|
||||
ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override;
|
||||
|
||||
ProgramStateRef removeDeadBindings(ProgramStateRef St,
|
||||
SymbolReaper &SymReaper) override;
|
||||
|
||||
void print(ProgramStateRef St, raw_ostream &Out, const char *nl,
|
||||
const char *sep) override;
|
||||
|
||||
private:
|
||||
RangeSet::Factory F;
|
||||
|
||||
RangeSet getRange(ProgramStateRef State, SymbolRef Sym);
|
||||
|
||||
RangeSet getSymLTRange(ProgramStateRef St, SymbolRef Sym,
|
||||
const llvm::APSInt &Int,
|
||||
const llvm::APSInt &Adjustment);
|
||||
|
@ -356,10 +368,46 @@ ento::CreateRangeConstraintManager(ProgramStateManager &StMgr, SubEngine *Eng) {
|
|||
return llvm::make_unique<RangeConstraintManager>(Eng, StMgr.getSValBuilder());
|
||||
}
|
||||
|
||||
const llvm::APSInt *RangeConstraintManager::getSymVal(ProgramStateRef St,
|
||||
SymbolRef Sym) const {
|
||||
const ConstraintRangeTy::data_type *T = St->get<ConstraintRange>(Sym);
|
||||
return T ? T->getConcreteValue() : nullptr;
|
||||
bool RangeConstraintManager::canReasonAbout(SVal X) const {
|
||||
Optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>();
|
||||
if (SymVal && SymVal->isExpression()) {
|
||||
const SymExpr *SE = SymVal->getSymbol();
|
||||
|
||||
if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SE)) {
|
||||
switch (SIE->getOpcode()) {
|
||||
// We don't reason yet about bitwise-constraints on symbolic values.
|
||||
case BO_And:
|
||||
case BO_Or:
|
||||
case BO_Xor:
|
||||
return false;
|
||||
// We don't reason yet about these arithmetic constraints on
|
||||
// symbolic values.
|
||||
case BO_Mul:
|
||||
case BO_Div:
|
||||
case BO_Rem:
|
||||
case BO_Shl:
|
||||
case BO_Shr:
|
||||
return false;
|
||||
// All other cases.
|
||||
default:
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
||||
if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(SE)) {
|
||||
if (BinaryOperator::isComparisonOp(SSE->getOpcode())) {
|
||||
// We handle Loc <> Loc comparisons, but not (yet) NonLoc <> NonLoc.
|
||||
if (Loc::isLocType(SSE->getLHS()->getType())) {
|
||||
assert(Loc::isLocType(SSE->getRHS()->getType()));
|
||||
return true;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
return false;
|
||||
}
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
ConditionTruthVal RangeConstraintManager::checkNull(ProgramStateRef State,
|
||||
|
@ -386,6 +434,12 @@ ConditionTruthVal RangeConstraintManager::checkNull(ProgramStateRef State,
|
|||
return ConditionTruthVal();
|
||||
}
|
||||
|
||||
const llvm::APSInt *RangeConstraintManager::getSymVal(ProgramStateRef St,
|
||||
SymbolRef Sym) const {
|
||||
const ConstraintRangeTy::data_type *T = St->get<ConstraintRange>(Sym);
|
||||
return T ? T->getConcreteValue() : nullptr;
|
||||
}
|
||||
|
||||
/// Scan all symbols referenced by the constraints. If the symbol is not alive
|
||||
/// as marked in LSymbols, mark it as dead in DSymbols.
|
||||
ProgramStateRef
|
||||
|
@ -429,7 +483,7 @@ RangeSet RangeConstraintManager::getRange(ProgramStateRef State,
|
|||
}
|
||||
|
||||
//===------------------------------------------------------------------------===
|
||||
// assumeSymX methods: public interface for RangeConstraintManager.
|
||||
// assumeSymX methods: protected interface for RangeConstraintManager.
|
||||
//===------------------------------------------------------------------------===/
|
||||
|
||||
// The syntax for ranges below is mathematical, using [x, y] for closed ranges
|
||||
|
@ -646,7 +700,7 @@ RangeConstraintManager::assumeSymLE(ProgramStateRef St, SymbolRef Sym,
|
|||
return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
|
||||
}
|
||||
|
||||
ProgramStateRef RangeConstraintManager::assumeSymbolWithinInclusiveRange(
|
||||
ProgramStateRef RangeConstraintManager::assumeSymWithinInclusiveRange(
|
||||
ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
|
||||
const llvm::APSInt &To, const llvm::APSInt &Adjustment) {
|
||||
RangeSet New = getSymGERange(State, Sym, From, Adjustment);
|
||||
|
@ -656,7 +710,7 @@ ProgramStateRef RangeConstraintManager::assumeSymbolWithinInclusiveRange(
|
|||
return New.isEmpty() ? nullptr : State->set<ConstraintRange>(Sym, New);
|
||||
}
|
||||
|
||||
ProgramStateRef RangeConstraintManager::assumeSymbolOutOfInclusiveRange(
|
||||
ProgramStateRef RangeConstraintManager::assumeSymOutsideInclusiveRange(
|
||||
ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
|
||||
const llvm::APSInt &To, const llvm::APSInt &Adjustment) {
|
||||
RangeSet RangeLT = getSymLTRange(State, Sym, From, Adjustment);
|
||||
|
|
|
@ -0,0 +1,204 @@
|
|||
//== RangedConstraintManager.cpp --------------------------------*- C++ -*--==//
|
||||
//
|
||||
// The LLVM Compiler Infrastructure
|
||||
//
|
||||
// This file is distributed under the University of Illinois Open Source
|
||||
// License. See LICENSE.TXT for details.
|
||||
//
|
||||
//===----------------------------------------------------------------------===//
|
||||
//
|
||||
// This file defines RangedConstraintManager, a class that provides a
|
||||
// range-based constraint manager interface.
|
||||
//
|
||||
//===----------------------------------------------------------------------===//
|
||||
|
||||
#include "RangedConstraintManager.h"
|
||||
#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
|
||||
|
||||
namespace clang {
|
||||
|
||||
namespace ento {
|
||||
|
||||
RangedConstraintManager::~RangedConstraintManager() {}
|
||||
|
||||
ProgramStateRef RangedConstraintManager::assumeSym(ProgramStateRef State,
|
||||
SymbolRef Sym,
|
||||
bool Assumption) {
|
||||
// Handle SymbolData.
|
||||
if (isa<SymbolData>(Sym)) {
|
||||
return assumeSymUnsupported(State, Sym, Assumption);
|
||||
|
||||
// Handle symbolic expression.
|
||||
} else if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(Sym)) {
|
||||
// We can only simplify expressions whose RHS is an integer.
|
||||
|
||||
BinaryOperator::Opcode op = SIE->getOpcode();
|
||||
if (BinaryOperator::isComparisonOp(op)) {
|
||||
if (!Assumption)
|
||||
op = BinaryOperator::negateComparisonOp(op);
|
||||
|
||||
return assumeSymRel(State, SIE->getLHS(), op, SIE->getRHS());
|
||||
}
|
||||
|
||||
} else if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(Sym)) {
|
||||
// Translate "a != b" to "(b - a) != 0".
|
||||
// We invert the order of the operands as a heuristic for how loop
|
||||
// conditions are usually written ("begin != end") as compared to length
|
||||
// calculations ("end - begin"). The more correct thing to do would be to
|
||||
// canonicalize "a - b" and "b - a", which would allow us to treat
|
||||
// "a != b" and "b != a" the same.
|
||||
SymbolManager &SymMgr = getSymbolManager();
|
||||
BinaryOperator::Opcode Op = SSE->getOpcode();
|
||||
assert(BinaryOperator::isComparisonOp(Op));
|
||||
|
||||
// For now, we only support comparing pointers.
|
||||
assert(Loc::isLocType(SSE->getLHS()->getType()));
|
||||
assert(Loc::isLocType(SSE->getRHS()->getType()));
|
||||
QualType DiffTy = SymMgr.getContext().getPointerDiffType();
|
||||
SymbolRef Subtraction =
|
||||
SymMgr.getSymSymExpr(SSE->getRHS(), BO_Sub, SSE->getLHS(), DiffTy);
|
||||
|
||||
const llvm::APSInt &Zero = getBasicVals().getValue(0, DiffTy);
|
||||
Op = BinaryOperator::reverseComparisonOp(Op);
|
||||
if (!Assumption)
|
||||
Op = BinaryOperator::negateComparisonOp(Op);
|
||||
return assumeSymRel(State, Subtraction, Op, Zero);
|
||||
}
|
||||
|
||||
// If we get here, there's nothing else we can do but treat the symbol as
|
||||
// opaque.
|
||||
return assumeSymUnsupported(State, Sym, Assumption);
|
||||
}
|
||||
|
||||
ProgramStateRef RangedConstraintManager::assumeSymInclusiveRange(
|
||||
ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
|
||||
const llvm::APSInt &To, bool InRange) {
|
||||
// Get the type used for calculating wraparound.
|
||||
BasicValueFactory &BVF = getBasicVals();
|
||||
APSIntType WraparoundType = BVF.getAPSIntType(Sym->getType());
|
||||
|
||||
llvm::APSInt Adjustment = WraparoundType.getZeroValue();
|
||||
SymbolRef AdjustedSym = Sym;
|
||||
computeAdjustment(AdjustedSym, Adjustment);
|
||||
|
||||
// Convert the right-hand side integer as necessary.
|
||||
APSIntType ComparisonType = std::max(WraparoundType, APSIntType(From));
|
||||
llvm::APSInt ConvertedFrom = ComparisonType.convert(From);
|
||||
llvm::APSInt ConvertedTo = ComparisonType.convert(To);
|
||||
|
||||
// Prefer unsigned comparisons.
|
||||
if (ComparisonType.getBitWidth() == WraparoundType.getBitWidth() &&
|
||||
ComparisonType.isUnsigned() && !WraparoundType.isUnsigned())
|
||||
Adjustment.setIsSigned(false);
|
||||
|
||||
if (InRange)
|
||||
return assumeSymWithinInclusiveRange(State, AdjustedSym, ConvertedFrom,
|
||||
ConvertedTo, Adjustment);
|
||||
return assumeSymOutsideInclusiveRange(State, AdjustedSym, ConvertedFrom,
|
||||
ConvertedTo, Adjustment);
|
||||
}
|
||||
|
||||
ProgramStateRef
|
||||
RangedConstraintManager::assumeSymUnsupported(ProgramStateRef State,
|
||||
SymbolRef Sym, bool Assumption) {
|
||||
BasicValueFactory &BVF = getBasicVals();
|
||||
QualType T = Sym->getType();
|
||||
|
||||
// Non-integer types are not supported.
|
||||
if (!T->isIntegralOrEnumerationType())
|
||||
return State;
|
||||
|
||||
// Reverse the operation and add directly to state.
|
||||
const llvm::APSInt &Zero = BVF.getValue(0, T);
|
||||
if (Assumption)
|
||||
return assumeSymNE(State, Sym, Zero, Zero);
|
||||
else
|
||||
return assumeSymEQ(State, Sym, Zero, Zero);
|
||||
}
|
||||
|
||||
ProgramStateRef RangedConstraintManager::assumeSymRel(ProgramStateRef State,
|
||||
SymbolRef Sym,
|
||||
BinaryOperator::Opcode Op,
|
||||
const llvm::APSInt &Int) {
|
||||
assert(BinaryOperator::isComparisonOp(Op) &&
|
||||
"Non-comparison ops should be rewritten as comparisons to zero.");
|
||||
|
||||
// Simplification: translate an assume of a constraint of the form
|
||||
// "(exp comparison_op expr) != 0" to true into an assume of
|
||||
// "exp comparison_op expr" to true. (And similarly, an assume of the form
|
||||
// "(exp comparison_op expr) == 0" to true into an assume of
|
||||
// "exp comparison_op expr" to false.)
|
||||
if (Int == 0 && (Op == BO_EQ || Op == BO_NE)) {
|
||||
if (const BinarySymExpr *SE = dyn_cast<BinarySymExpr>(Sym))
|
||||
if (BinaryOperator::isComparisonOp(SE->getOpcode()))
|
||||
return assumeSym(State, Sym, (Op == BO_NE ? true : false));
|
||||
}
|
||||
|
||||
// Get the type used for calculating wraparound.
|
||||
BasicValueFactory &BVF = getBasicVals();
|
||||
APSIntType WraparoundType = BVF.getAPSIntType(Sym->getType());
|
||||
|
||||
// We only handle simple comparisons of the form "$sym == constant"
|
||||
// or "($sym+constant1) == constant2".
|
||||
// The adjustment is "constant1" in the above expression. It's used to
|
||||
// "slide" the solution range around for modular arithmetic. For example,
|
||||
// x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which
|
||||
// in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to
|
||||
// the subclasses of SimpleConstraintManager to handle the adjustment.
|
||||
llvm::APSInt Adjustment = WraparoundType.getZeroValue();
|
||||
computeAdjustment(Sym, Adjustment);
|
||||
|
||||
// Convert the right-hand side integer as necessary.
|
||||
APSIntType ComparisonType = std::max(WraparoundType, APSIntType(Int));
|
||||
llvm::APSInt ConvertedInt = ComparisonType.convert(Int);
|
||||
|
||||
// Prefer unsigned comparisons.
|
||||
if (ComparisonType.getBitWidth() == WraparoundType.getBitWidth() &&
|
||||
ComparisonType.isUnsigned() && !WraparoundType.isUnsigned())
|
||||
Adjustment.setIsSigned(false);
|
||||
|
||||
switch (Op) {
|
||||
default:
|
||||
llvm_unreachable("invalid operation not caught by assertion above");
|
||||
|
||||
case BO_EQ:
|
||||
return assumeSymEQ(State, Sym, ConvertedInt, Adjustment);
|
||||
|
||||
case BO_NE:
|
||||
return assumeSymNE(State, Sym, ConvertedInt, Adjustment);
|
||||
|
||||
case BO_GT:
|
||||
return assumeSymGT(State, Sym, ConvertedInt, Adjustment);
|
||||
|
||||
case BO_GE:
|
||||
return assumeSymGE(State, Sym, ConvertedInt, Adjustment);
|
||||
|
||||
case BO_LT:
|
||||
return assumeSymLT(State, Sym, ConvertedInt, Adjustment);
|
||||
|
||||
case BO_LE:
|
||||
return assumeSymLE(State, Sym, ConvertedInt, Adjustment);
|
||||
} // end switch
|
||||
}
|
||||
|
||||
void RangedConstraintManager::computeAdjustment(SymbolRef &Sym,
|
||||
llvm::APSInt &Adjustment) {
|
||||
// Is it a "($sym+constant1)" expression?
|
||||
if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(Sym)) {
|
||||
BinaryOperator::Opcode Op = SE->getOpcode();
|
||||
if (Op == BO_Add || Op == BO_Sub) {
|
||||
Sym = SE->getLHS();
|
||||
Adjustment = APSIntType(Adjustment).convert(SE->getRHS());
|
||||
|
||||
// Don't forget to negate the adjustment if it's being subtracted.
|
||||
// This should happen /after/ promotion, in case the value being
|
||||
// subtracted is, say, CHAR_MIN, and the promoted type is 'int'.
|
||||
if (Op == BO_Sub)
|
||||
Adjustment = -Adjustment;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
} // end of namespace ento
|
||||
|
||||
} // end of namespace clang
|
|
@ -1,4 +1,4 @@
|
|||
//== SimpleConstraintManager.h ----------------------------------*- C++ -*--==//
|
||||
//== RangedConstraintManager.h ----------------------------------*- C++ -*--==//
|
||||
//
|
||||
// The LLVM Compiler Infrastructure
|
||||
//
|
||||
|
@ -7,59 +7,55 @@
|
|||
//
|
||||
//===----------------------------------------------------------------------===//
|
||||
//
|
||||
// Code shared between BasicConstraintManager and RangeConstraintManager.
|
||||
// Ranged constraint manager, built on SimpleConstraintManager.
|
||||
//
|
||||
//===----------------------------------------------------------------------===//
|
||||
|
||||
#ifndef LLVM_CLANG_LIB_STATICANALYZER_CORE_SIMPLECONSTRAINTMANAGER_H
|
||||
#define LLVM_CLANG_LIB_STATICANALYZER_CORE_SIMPLECONSTRAINTMANAGER_H
|
||||
#ifndef LLVM_CLANG_LIB_STATICANALYZER_CORE_RANGEDCONSTRAINTMANAGER_H
|
||||
#define LLVM_CLANG_LIB_STATICANALYZER_CORE_RANGEDCONSTRAINTMANAGER_H
|
||||
|
||||
#include "clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h"
|
||||
#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
|
||||
#include "clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h"
|
||||
|
||||
namespace clang {
|
||||
|
||||
namespace ento {
|
||||
|
||||
class SimpleConstraintManager : public ConstraintManager {
|
||||
SubEngine *SU;
|
||||
SValBuilder &SVB;
|
||||
|
||||
class RangedConstraintManager : public SimpleConstraintManager {
|
||||
public:
|
||||
SimpleConstraintManager(SubEngine *SE, SValBuilder &SB) : SU(SE), SVB(SB) {}
|
||||
~SimpleConstraintManager() override;
|
||||
RangedConstraintManager(SubEngine *SE, SValBuilder &SB)
|
||||
: SimpleConstraintManager(SE, SB) {}
|
||||
|
||||
~RangedConstraintManager() override;
|
||||
|
||||
//===------------------------------------------------------------------===//
|
||||
// Common implementation for the interface provided by ConstraintManager.
|
||||
// Implementation for interface from SimpleConstraintManager.
|
||||
//===------------------------------------------------------------------===//
|
||||
|
||||
ProgramStateRef assume(ProgramStateRef State, DefinedSVal Cond,
|
||||
bool Assumption) override;
|
||||
ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym,
|
||||
bool Assumption) override;
|
||||
|
||||
ProgramStateRef assume(ProgramStateRef State, NonLoc Cond, bool Assumption);
|
||||
ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym,
|
||||
const llvm::APSInt &From,
|
||||
const llvm::APSInt &To,
|
||||
bool InRange) override;
|
||||
|
||||
ProgramStateRef assumeInclusiveRange(ProgramStateRef State, NonLoc Value,
|
||||
const llvm::APSInt &From,
|
||||
const llvm::APSInt &To,
|
||||
bool InRange) override;
|
||||
|
||||
ProgramStateRef assumeSymRel(ProgramStateRef State, const SymExpr *LHS,
|
||||
BinaryOperator::Opcode Op,
|
||||
const llvm::APSInt &Int);
|
||||
|
||||
ProgramStateRef assumeSymWithinInclusiveRange(ProgramStateRef State,
|
||||
SymbolRef Sym,
|
||||
const llvm::APSInt &From,
|
||||
const llvm::APSInt &To,
|
||||
bool InRange);
|
||||
ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
|
||||
bool Assumption) override;
|
||||
|
||||
protected:
|
||||
/// Assume a constraint between a symbolic expression and a concrete integer.
|
||||
virtual ProgramStateRef assumeSymRel(ProgramStateRef State, SymbolRef Sym,
|
||||
BinaryOperator::Opcode op,
|
||||
const llvm::APSInt &Int);
|
||||
|
||||
//===------------------------------------------------------------------===//
|
||||
// Interface that subclasses must implement.
|
||||
//===------------------------------------------------------------------===//
|
||||
|
||||
// Each of these is of the form "$Sym+Adj <> V", where "<>" is the comparison
|
||||
// operation for the method being invoked.
|
||||
|
||||
virtual ProgramStateRef assumeSymNE(ProgramStateRef State, SymbolRef Sym,
|
||||
const llvm::APSInt &V,
|
||||
const llvm::APSInt &Adjustment) = 0;
|
||||
|
@ -84,28 +80,19 @@ protected:
|
|||
const llvm::APSInt &V,
|
||||
const llvm::APSInt &Adjustment) = 0;
|
||||
|
||||
virtual ProgramStateRef assumeSymbolWithinInclusiveRange(
|
||||
virtual ProgramStateRef assumeSymWithinInclusiveRange(
|
||||
ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
|
||||
const llvm::APSInt &To, const llvm::APSInt &Adjustment) = 0;
|
||||
|
||||
virtual ProgramStateRef assumeSymbolOutOfInclusiveRange(
|
||||
virtual ProgramStateRef assumeSymOutsideInclusiveRange(
|
||||
ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
|
||||
const llvm::APSInt &To, const llvm::APSInt &Adjustment) = 0;
|
||||
|
||||
//===------------------------------------------------------------------===//
|
||||
// Internal implementation.
|
||||
//===------------------------------------------------------------------===//
|
||||
|
||||
BasicValueFactory &getBasicVals() const { return SVB.getBasicValueFactory(); }
|
||||
SymbolManager &getSymbolManager() const { return SVB.getSymbolManager(); }
|
||||
|
||||
bool canReasonAbout(SVal X) const override;
|
||||
|
||||
ProgramStateRef assumeAux(ProgramStateRef State, NonLoc Cond,
|
||||
bool Assumption);
|
||||
|
||||
ProgramStateRef assumeAuxForSymbol(ProgramStateRef State, SymbolRef Sym,
|
||||
bool Assumption);
|
||||
private:
|
||||
static void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment);
|
||||
};
|
||||
|
||||
} // end GR namespace
|
|
@ -7,12 +7,12 @@
|
|||
//
|
||||
//===----------------------------------------------------------------------===//
|
||||
//
|
||||
// This file defines SimpleConstraintManager, a class that holds code shared
|
||||
// between BasicConstraintManager and RangeConstraintManager.
|
||||
// This file defines SimpleConstraintManager, a class that provides a
|
||||
// simplified constraint manager interface, compared to ConstraintManager.
|
||||
//
|
||||
//===----------------------------------------------------------------------===//
|
||||
|
||||
#include "SimpleConstraintManager.h"
|
||||
#include "clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h"
|
||||
#include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
|
||||
#include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
|
||||
#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
|
||||
|
@ -23,48 +23,6 @@ namespace ento {
|
|||
|
||||
SimpleConstraintManager::~SimpleConstraintManager() {}
|
||||
|
||||
bool SimpleConstraintManager::canReasonAbout(SVal X) const {
|
||||
Optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>();
|
||||
if (SymVal && SymVal->isExpression()) {
|
||||
const SymExpr *SE = SymVal->getSymbol();
|
||||
|
||||
if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SE)) {
|
||||
switch (SIE->getOpcode()) {
|
||||
// We don't reason yet about bitwise-constraints on symbolic values.
|
||||
case BO_And:
|
||||
case BO_Or:
|
||||
case BO_Xor:
|
||||
return false;
|
||||
// We don't reason yet about these arithmetic constraints on
|
||||
// symbolic values.
|
||||
case BO_Mul:
|
||||
case BO_Div:
|
||||
case BO_Rem:
|
||||
case BO_Shl:
|
||||
case BO_Shr:
|
||||
return false;
|
||||
// All other cases.
|
||||
default:
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
||||
if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(SE)) {
|
||||
if (BinaryOperator::isComparisonOp(SSE->getOpcode())) {
|
||||
// We handle Loc <> Loc comparisons, but not (yet) NonLoc <> NonLoc.
|
||||
if (Loc::isLocType(SSE->getLHS()->getType())) {
|
||||
assert(Loc::isLocType(SSE->getRHS()->getType()));
|
||||
return true;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
return false;
|
||||
}
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef State,
|
||||
DefinedSVal Cond,
|
||||
bool Assumption) {
|
||||
|
@ -92,23 +50,6 @@ ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef State,
|
|||
return State;
|
||||
}
|
||||
|
||||
ProgramStateRef
|
||||
SimpleConstraintManager::assumeAuxForSymbol(ProgramStateRef State,
|
||||
SymbolRef Sym, bool Assumption) {
|
||||
BasicValueFactory &BVF = getBasicVals();
|
||||
QualType T = Sym->getType();
|
||||
|
||||
// None of the constraint solvers currently support non-integer types.
|
||||
if (!T->isIntegralOrEnumerationType())
|
||||
return State;
|
||||
|
||||
const llvm::APSInt &zero = BVF.getValue(0, T);
|
||||
if (Assumption)
|
||||
return assumeSymNE(State, Sym, zero, zero);
|
||||
else
|
||||
return assumeSymEQ(State, Sym, zero, zero);
|
||||
}
|
||||
|
||||
ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef State,
|
||||
NonLoc Cond,
|
||||
bool Assumption) {
|
||||
|
@ -118,7 +59,8 @@ ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef State,
|
|||
if (!canReasonAbout(Cond)) {
|
||||
// Just add the constraint to the expression without trying to simplify.
|
||||
SymbolRef Sym = Cond.getAsSymExpr();
|
||||
return assumeAuxForSymbol(State, Sym, Assumption);
|
||||
assert(Sym);
|
||||
return assumeSymUnsupported(State, Sym, Assumption);
|
||||
}
|
||||
|
||||
switch (Cond.getSubKind()) {
|
||||
|
@ -129,51 +71,7 @@ ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef State,
|
|||
nonloc::SymbolVal SV = Cond.castAs<nonloc::SymbolVal>();
|
||||
SymbolRef Sym = SV.getSymbol();
|
||||
assert(Sym);
|
||||
|
||||
// Handle SymbolData.
|
||||
if (!SV.isExpression()) {
|
||||
return assumeAuxForSymbol(State, Sym, Assumption);
|
||||
|
||||
// Handle symbolic expression.
|
||||
} else if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(Sym)) {
|
||||
// We can only simplify expressions whose RHS is an integer.
|
||||
|
||||
BinaryOperator::Opcode Op = SE->getOpcode();
|
||||
if (BinaryOperator::isComparisonOp(Op)) {
|
||||
if (!Assumption)
|
||||
Op = BinaryOperator::negateComparisonOp(Op);
|
||||
|
||||
return assumeSymRel(State, SE->getLHS(), Op, SE->getRHS());
|
||||
}
|
||||
|
||||
} else if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(Sym)) {
|
||||
// Translate "a != b" to "(b - a) != 0".
|
||||
// We invert the order of the operands as a heuristic for how loop
|
||||
// conditions are usually written ("begin != end") as compared to length
|
||||
// calculations ("end - begin"). The more correct thing to do would be to
|
||||
// canonicalize "a - b" and "b - a", which would allow us to treat
|
||||
// "a != b" and "b != a" the same.
|
||||
SymbolManager &SymMgr = getSymbolManager();
|
||||
BinaryOperator::Opcode Op = SSE->getOpcode();
|
||||
assert(BinaryOperator::isComparisonOp(Op));
|
||||
|
||||
// For now, we only support comparing pointers.
|
||||
assert(Loc::isLocType(SSE->getLHS()->getType()));
|
||||
assert(Loc::isLocType(SSE->getRHS()->getType()));
|
||||
QualType DiffTy = SymMgr.getContext().getPointerDiffType();
|
||||
SymbolRef Subtraction =
|
||||
SymMgr.getSymSymExpr(SSE->getRHS(), BO_Sub, SSE->getLHS(), DiffTy);
|
||||
|
||||
const llvm::APSInt &Zero = getBasicVals().getValue(0, DiffTy);
|
||||
Op = BinaryOperator::reverseComparisonOp(Op);
|
||||
if (!Assumption)
|
||||
Op = BinaryOperator::negateComparisonOp(Op);
|
||||
return assumeSymRel(State, Subtraction, Op, Zero);
|
||||
}
|
||||
|
||||
// If we get here, there's nothing else we can do but treat the symbol as
|
||||
// opaque.
|
||||
return assumeAuxForSymbol(State, Sym, Assumption);
|
||||
return assumeSym(State, Sym, Assumption);
|
||||
}
|
||||
|
||||
case nonloc::ConcreteIntKind: {
|
||||
|
@ -206,7 +104,7 @@ ProgramStateRef SimpleConstraintManager::assumeInclusiveRange(
|
|||
// Just add the constraint to the expression without trying to simplify.
|
||||
SymbolRef Sym = Value.getAsSymExpr();
|
||||
assert(Sym);
|
||||
return assumeSymWithinInclusiveRange(State, Sym, From, To, InRange);
|
||||
return assumeSymInclusiveRange(State, Sym, From, To, InRange);
|
||||
}
|
||||
|
||||
switch (Value.getSubKind()) {
|
||||
|
@ -217,7 +115,7 @@ ProgramStateRef SimpleConstraintManager::assumeInclusiveRange(
|
|||
case nonloc::LocAsIntegerKind:
|
||||
case nonloc::SymbolValKind: {
|
||||
if (SymbolRef Sym = Value.getAsSymbol())
|
||||
return assumeSymWithinInclusiveRange(State, Sym, From, To, InRange);
|
||||
return assumeSymInclusiveRange(State, Sym, From, To, InRange);
|
||||
return State;
|
||||
} // end switch
|
||||
|
||||
|
@ -230,118 +128,6 @@ ProgramStateRef SimpleConstraintManager::assumeInclusiveRange(
|
|||
} // end switch
|
||||
}
|
||||
|
||||
static void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment) {
|
||||
// Is it a "($sym+constant1)" expression?
|
||||
if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(Sym)) {
|
||||
BinaryOperator::Opcode Op = SE->getOpcode();
|
||||
if (Op == BO_Add || Op == BO_Sub) {
|
||||
Sym = SE->getLHS();
|
||||
Adjustment = APSIntType(Adjustment).convert(SE->getRHS());
|
||||
|
||||
// Don't forget to negate the adjustment if it's being subtracted.
|
||||
// This should happen /after/ promotion, in case the value being
|
||||
// subtracted is, say, CHAR_MIN, and the promoted type is 'int'.
|
||||
if (Op == BO_Sub)
|
||||
Adjustment = -Adjustment;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
ProgramStateRef SimpleConstraintManager::assumeSymRel(ProgramStateRef State,
|
||||
const SymExpr *LHS,
|
||||
BinaryOperator::Opcode Op,
|
||||
const llvm::APSInt &Int) {
|
||||
assert(BinaryOperator::isComparisonOp(Op) &&
|
||||
"Non-comparison ops should be rewritten as comparisons to zero.");
|
||||
|
||||
SymbolRef Sym = LHS;
|
||||
|
||||
// Simplification: translate an assume of a constraint of the form
|
||||
// "(exp comparison_op expr) != 0" to true into an assume of
|
||||
// "exp comparison_op expr" to true. (And similarly, an assume of the form
|
||||
// "(exp comparison_op expr) == 0" to true into an assume of
|
||||
// "exp comparison_op expr" to false.)
|
||||
if (Int == 0 && (Op == BO_EQ || Op == BO_NE)) {
|
||||
if (const BinarySymExpr *SE = dyn_cast<BinarySymExpr>(Sym))
|
||||
if (BinaryOperator::isComparisonOp(SE->getOpcode()))
|
||||
return assume(State, nonloc::SymbolVal(Sym), (Op == BO_NE ? true : false));
|
||||
}
|
||||
|
||||
// Get the type used for calculating wraparound.
|
||||
BasicValueFactory &BVF = getBasicVals();
|
||||
APSIntType WraparoundType = BVF.getAPSIntType(LHS->getType());
|
||||
|
||||
// We only handle simple comparisons of the form "$sym == constant"
|
||||
// or "($sym+constant1) == constant2".
|
||||
// The adjustment is "constant1" in the above expression. It's used to
|
||||
// "slide" the solution range around for modular arithmetic. For example,
|
||||
// x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which
|
||||
// in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to
|
||||
// the subclasses of SimpleConstraintManager to handle the adjustment.
|
||||
llvm::APSInt Adjustment = WraparoundType.getZeroValue();
|
||||
computeAdjustment(Sym, Adjustment);
|
||||
|
||||
// Convert the right-hand side integer as necessary.
|
||||
APSIntType ComparisonType = std::max(WraparoundType, APSIntType(Int));
|
||||
llvm::APSInt ConvertedInt = ComparisonType.convert(Int);
|
||||
|
||||
// Prefer unsigned comparisons.
|
||||
if (ComparisonType.getBitWidth() == WraparoundType.getBitWidth() &&
|
||||
ComparisonType.isUnsigned() && !WraparoundType.isUnsigned())
|
||||
Adjustment.setIsSigned(false);
|
||||
|
||||
switch (Op) {
|
||||
default:
|
||||
llvm_unreachable("invalid operation not caught by assertion above");
|
||||
|
||||
case BO_EQ:
|
||||
return assumeSymEQ(State, Sym, ConvertedInt, Adjustment);
|
||||
|
||||
case BO_NE:
|
||||
return assumeSymNE(State, Sym, ConvertedInt, Adjustment);
|
||||
|
||||
case BO_GT:
|
||||
return assumeSymGT(State, Sym, ConvertedInt, Adjustment);
|
||||
|
||||
case BO_GE:
|
||||
return assumeSymGE(State, Sym, ConvertedInt, Adjustment);
|
||||
|
||||
case BO_LT:
|
||||
return assumeSymLT(State, Sym, ConvertedInt, Adjustment);
|
||||
|
||||
case BO_LE:
|
||||
return assumeSymLE(State, Sym, ConvertedInt, Adjustment);
|
||||
} // end switch
|
||||
}
|
||||
|
||||
ProgramStateRef SimpleConstraintManager::assumeSymWithinInclusiveRange(
|
||||
ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
|
||||
const llvm::APSInt &To, bool InRange) {
|
||||
// Get the type used for calculating wraparound.
|
||||
BasicValueFactory &BVF = getBasicVals();
|
||||
APSIntType WraparoundType = BVF.getAPSIntType(Sym->getType());
|
||||
|
||||
llvm::APSInt Adjustment = WraparoundType.getZeroValue();
|
||||
SymbolRef AdjustedSym = Sym;
|
||||
computeAdjustment(AdjustedSym, Adjustment);
|
||||
|
||||
// Convert the right-hand side integer as necessary.
|
||||
APSIntType ComparisonType = std::max(WraparoundType, APSIntType(From));
|
||||
llvm::APSInt ConvertedFrom = ComparisonType.convert(From);
|
||||
llvm::APSInt ConvertedTo = ComparisonType.convert(To);
|
||||
|
||||
// Prefer unsigned comparisons.
|
||||
if (ComparisonType.getBitWidth() == WraparoundType.getBitWidth() &&
|
||||
ComparisonType.isUnsigned() && !WraparoundType.isUnsigned())
|
||||
Adjustment.setIsSigned(false);
|
||||
|
||||
if (InRange)
|
||||
return assumeSymbolWithinInclusiveRange(State, AdjustedSym, ConvertedFrom,
|
||||
ConvertedTo, Adjustment);
|
||||
return assumeSymbolOutOfInclusiveRange(State, AdjustedSym, ConvertedFrom,
|
||||
ConvertedTo, Adjustment);
|
||||
}
|
||||
|
||||
} // end of namespace ento
|
||||
|
||||
} // end of namespace clang
|
||||
|
|
Loading…
Reference in New Issue