aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h2
-rw-r--r--include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h14
-rw-r--r--lib/StaticAnalyzer/Core/ExprEngineC.cpp3
-rw-r--r--lib/StaticAnalyzer/Core/SVals.cpp2
-rw-r--r--lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp40
-rw-r--r--lib/StaticAnalyzer/Core/SimpleConstraintManager.h12
6 files changed, 47 insertions, 26 deletions
diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h b/include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h
index be1b9cecca..bbf0469e06 100644
--- a/include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h
+++ b/include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h
@@ -281,7 +281,7 @@ public:
SymbolVal(SymbolRef sym) : NonLoc(SymbolValKind, sym) {}
SymbolRef getSymbol() const {
- return (const SymbolData*) Data;
+ return (const SymExpr*) Data;
}
static inline bool classof(const SVal* V) {
diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h b/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h
index 0d6e18eb3c..e4bbf6766d 100644
--- a/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h
+++ b/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h
@@ -40,6 +40,8 @@ namespace ento {
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 @@ public:
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 @@ public:
}
};
-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 @@ public:
}
};
-/// 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;
diff --git a/lib/StaticAnalyzer/Core/ExprEngineC.cpp b/lib/StaticAnalyzer/Core/ExprEngineC.cpp
index d74c48d962..0f49acca93 100644
--- a/lib/StaticAnalyzer/Core/ExprEngineC.cpp
+++ b/lib/StaticAnalyzer/Core/ExprEngineC.cpp
@@ -43,8 +43,7 @@ void ExprEngine::VisitBinaryOperator(const BinaryOperator* B,
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);
}
diff --git a/lib/StaticAnalyzer/Core/SVals.cpp b/lib/StaticAnalyzer/Core/SVals.cpp
index 52e52d6d59..6b71f184aa 100644
--- a/lib/StaticAnalyzer/Core/SVals.cpp
+++ b/lib/StaticAnalyzer/Core/SVals.cpp
@@ -99,7 +99,7 @@ SymbolRef SVal::getAsSymbol() const {
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();
diff --git a/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp b/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
index 79d8b8bf9d..4ae1f17eea 100644
--- a/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
+++ b/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
@@ -135,16 +135,29 @@ static BinaryOperator::Opcode NegateComparison(BinaryOperator::Opcode op) {
}
}
+
+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 @@ const ProgramState *SimpleConstraintManager::assumeAux(const ProgramState *state
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.
diff --git a/lib/StaticAnalyzer/Core/SimpleConstraintManager.h b/lib/StaticAnalyzer/Core/SimpleConstraintManager.h
index d4295d42d9..000af439fd 100644
--- a/lib/StaticAnalyzer/Core/SimpleConstraintManager.h
+++ b/lib/StaticAnalyzer/Core/SimpleConstraintManager.h
@@ -81,9 +81,17 @@ protected:
// 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
generated by cgit v1.2.3-18-g5258 (git 2.32.0) at 2025-08-04 16:31:10 +0000