[cfe-commits] r145831 - in /cfe/trunk: include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h lib/StaticAnalyzer/Core/ExprEngineC.cpp lib/StaticAnalyzer/Core/SVals.cpp lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp lib/StaticAnalyzer/Core/SimpleConstraintManager.h
Anna Zaks
ganna at apple.com
Mon Dec 5 10:58:19 PST 2011
Author: zaks
Date: Mon Dec 5 12:58:19 2011
New Revision: 145831
URL: http://llvm.org/viewvc/llvm-project?rev=145831&view=rev
Log:
[analyzer] First step toward removing
ConstraintManager::canReasonAbout() from the ExprEngine.
ExprEngine should not care if the constraint solver can reason about
something or not. The solver should be able to handle all the SymExprs.
To do this, the solver should be able to keep track of not only the
SymbolData but of all SymExprs. This is why we change SymbolRef to be an
alias of SymExpr*. When encountering an expression it cannot simplify,
the solver should just add the constraints to it.
Modified:
cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h
cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h
cfe/trunk/lib/StaticAnalyzer/Core/ExprEngineC.cpp
cfe/trunk/lib/StaticAnalyzer/Core/SVals.cpp
cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.h
Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h?rev=145831&r1=145830&r2=145831&view=diff
==============================================================================
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h (original)
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h Mon Dec 5 12:58:19 2011
@@ -281,7 +281,7 @@
SymbolVal(SymbolRef sym) : NonLoc(SymbolValKind, sym) {}
SymbolRef getSymbol() const {
- return (const SymbolData*) Data;
+ return (const SymExpr*) Data;
}
static inline bool classof(const SVal* V) {
Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h?rev=145831&r1=145830&r2=145831&view=diff
==============================================================================
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h (original)
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h Mon Dec 5 12:58:19 2011
@@ -40,6 +40,8 @@
class TypedValueRegion;
class VarRegion;
+/// \brief Symbolic value. These values used to capture symbolic execution of
+/// the program.
class SymExpr : public llvm::FoldingSetNode {
public:
enum Kind { RegionValueKind, ConjuredKind, DerivedKind, ExtentKind,
@@ -69,8 +71,12 @@
static inline bool classof(const SymExpr*) { return true; }
};
-typedef unsigned SymbolID;
+typedef const SymExpr* SymbolRef;
+typedef llvm::SmallVector<SymbolRef, 2> SymbolRefSmallVectorTy;
+typedef unsigned SymbolID;
+/// \brief A symbol representing data which can be stored in a memory location
+/// (region).
class SymbolData : public SymExpr {
private:
const SymbolID Sym;
@@ -90,9 +96,6 @@
}
};
-typedef const SymbolData* SymbolRef;
-typedef llvm::SmallVector<SymbolRef, 2> SymbolRefSmallVectorTy;
-
/// A symbol representing the value of a MemRegion.
class SymbolRegionValue : public SymbolData {
const TypedValueRegion *R;
@@ -122,7 +125,8 @@
}
};
-/// A symbol representing the result of an expression.
+/// A symbol representing the result of an expression in the case when we do
+/// not know anything about what the expression is.
class SymbolConjured : public SymbolData {
const Stmt *S;
QualType T;
Modified: cfe/trunk/lib/StaticAnalyzer/Core/ExprEngineC.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/ExprEngineC.cpp?rev=145831&r1=145830&r2=145831&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/ExprEngineC.cpp (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/ExprEngineC.cpp Mon Dec 5 12:58:19 2011
@@ -43,8 +43,7 @@
if (Op == BO_Assign) {
// EXPERIMENTAL: "Conjured" symbols.
// FIXME: Handle structs.
- if (RightV.isUnknown() ||
- !getConstraintManager().canReasonAbout(RightV)) {
+ if (RightV.isUnknown()) {
unsigned Count = currentBuilderContext->getCurrentBlockCount();
RightV = svalBuilder.getConjuredSymbolVal(NULL, B->getRHS(), Count);
}
Modified: cfe/trunk/lib/StaticAnalyzer/Core/SVals.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/SVals.cpp?rev=145831&r1=145830&r2=145831&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/SVals.cpp (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/SVals.cpp Mon Dec 5 12:58:19 2011
@@ -99,7 +99,7 @@
return X->getSymbol();
if (const nonloc::SymExprVal *X = dyn_cast<nonloc::SymExprVal>(this))
- if (SymbolRef Y = dyn_cast<SymbolData>(X->getSymbolicExpression()))
+ if (SymbolRef Y = X->getSymbolicExpression())
return Y;
return getAsLocSymbol();
Modified: cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp?rev=145831&r1=145830&r2=145831&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp Mon Dec 5 12:58:19 2011
@@ -135,16 +135,29 @@
}
}
+
+const ProgramState *SimpleConstraintManager::assumeAuxForSymbol(
+ const ProgramState *State,
+ SymbolRef Sym,
+ bool Assumption) {
+ QualType T = State->getSymbolManager().getType(Sym);
+ const llvm::APSInt &zero = State->getBasicVals().getValue(0, T);
+ if (Assumption)
+ return assumeSymNE(State, Sym, zero, zero);
+ else
+ return assumeSymEQ(State, Sym, zero, zero);
+}
+
const ProgramState *SimpleConstraintManager::assumeAux(const ProgramState *state,
NonLoc Cond,
bool Assumption) {
- // We cannot reason about SymSymExprs,
- // and can only reason about some SymIntExprs.
+ // We cannot reason about SymSymExprs, and can only reason about some
+ // SymIntExprs.
if (!canReasonAbout(Cond)) {
- // Just return the current state indicating that the path is feasible.
- // This may be an over-approximation of what is possible.
- return state;
+ // Just add the constraint to the expression without trying to simplify.
+ SymbolRef sym = Cond.getAsSymExpr();
+ return assumeAuxForSymbol(state, sym, Assumption);
}
BasicValueFactory &BasicVals = state->getBasicVals();
@@ -157,22 +170,19 @@
case nonloc::SymbolValKind: {
nonloc::SymbolVal& SV = cast<nonloc::SymbolVal>(Cond);
SymbolRef sym = SV.getSymbol();
- QualType T = SymMgr.getType(sym);
- const llvm::APSInt &zero = BasicVals.getValue(0, T);
- if (Assumption)
- return assumeSymNE(state, sym, zero, zero);
- else
- return assumeSymEQ(state, sym, zero, zero);
+ return assumeAuxForSymbol(state, sym, Assumption);
}
case nonloc::SymExprValKind: {
nonloc::SymExprVal V = cast<nonloc::SymExprVal>(Cond);
- // For now, we only handle expressions whose RHS is an integer.
- // All other expressions are assumed to be feasible.
- const SymIntExpr *SE = dyn_cast<SymIntExpr>(V.getSymbolicExpression());
+ SymbolRef sym = V.getSymbolicExpression();
+ assert(sym);
+
+ // We can only simplify expressions whose RHS is an integer.
+ const SymIntExpr *SE = dyn_cast<SymIntExpr>(sym);
if (!SE)
- return state;
+ return assumeAuxForSymbol(state, sym, Assumption);
BinaryOperator::Opcode op = SE->getOpcode();
// Implicitly compare non-comparison expressions to 0.
Modified: cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.h?rev=145831&r1=145830&r2=145831&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.h (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.h Mon Dec 5 12:58:19 2011
@@ -81,9 +81,17 @@
// Internal implementation.
//===------------------------------------------------------------------===//
- const ProgramState *assumeAux(const ProgramState *state, Loc Cond,bool Assumption);
+ const ProgramState *assumeAux(const ProgramState *state,
+ Loc Cond,
+ bool Assumption);
- const ProgramState *assumeAux(const ProgramState *state, NonLoc Cond, bool Assumption);
+ const ProgramState *assumeAux(const ProgramState *state,
+ NonLoc Cond,
+ bool Assumption);
+
+ const ProgramState *assumeAuxForSymbol(const ProgramState *State,
+ SymbolRef Sym,
+ bool Assumption);
};
} // end GR namespace
More information about the cfe-commits
mailing list