static void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment);
};
+/// Try to simplify a given symbolic expression's associated value based on the
+/// constraints in State. This is needed because the Environment bindings are
+/// not getting updated when a new constraint is added to the State.
+SymbolRef simplify(ProgramStateRef State, SymbolRef Sym);
+
} // namespace ento
} // namespace clang
// Constraint manager implementation details
//===----------------------------------------------------------------------===//
-static SymbolRef simplify(ProgramStateRef State, SymbolRef Sym) {
- SValBuilder &SVB = State->getStateManager().getSValBuilder();
- SVal SimplifiedVal = SVB.simplifySVal(State, SVB.makeSymbolVal(Sym));
- return SimplifiedVal.getAsSymbol();
-}
-
class RangeConstraintManager : public RangedConstraintManager {
public:
RangeConstraintManager(ExprEngine *EE, SValBuilder &SVB)
// This is an infeasible assumption.
return nullptr;
- if (SymbolRef SimplifiedSym = simplify(State, Sym))
- Sym = SimplifiedSym;
-
if (ProgramStateRef NewState = setConstraint(State, Sym, NewConstraint)) {
if (auto Equality = EqualityInfo::extract(Sym, Int, Adjustment)) {
// If the original assumption is not Sym + Adjustment !=/</> Int,
SValBuilder &SVB, RangeSet::Factory &F, ProgramStateRef State) {
SymbolSet ClassMembers = getClassMembers(State);
for (const SymbolRef &MemberSym : ClassMembers) {
- SymbolRef SimplifiedMemberSym = ::simplify(State, MemberSym);
+ SymbolRef SimplifiedMemberSym = ento::simplify(State, MemberSym);
if (SimplifiedMemberSym && MemberSym != SimplifiedMemberSym) {
EquivalenceClass ClassOfSimplifiedSym =
EquivalenceClass::find(State, SimplifiedMemberSym);
return St;
llvm::APSInt Point = AdjustmentType.convert(Int) - Adjustment;
-
RangeSet New = getRange(St, Sym);
New = F.deletePoint(New, Point);
ProgramStateRef RangedConstraintManager::assumeSym(ProgramStateRef State,
SymbolRef Sym,
bool Assumption) {
+ Sym = simplify(State, Sym);
+
// Handle SymbolData.
- if (isa<SymbolData>(Sym)) {
+ if (isa<SymbolData>(Sym))
return assumeSymUnsupported(State, Sym, Assumption);
- // Handle symbolic expression.
- } else if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(Sym)) {
+ // Handle symbolic expression.
+ if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(Sym)) {
// We can only simplify expressions whose RHS is an integer.
BinaryOperator::Opcode op = SIE->getOpcode();
ProgramStateRef RangedConstraintManager::assumeSymInclusiveRange(
ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
const llvm::APSInt &To, bool InRange) {
+
+ Sym = simplify(State, Sym);
+
// Get the type used for calculating wraparound.
BasicValueFactory &BVF = getBasicVals();
APSIntType WraparoundType = BVF.getAPSIntType(Sym->getType());
ProgramStateRef
RangedConstraintManager::assumeSymUnsupported(ProgramStateRef State,
SymbolRef Sym, bool Assumption) {
+ Sym = simplify(State, Sym);
+
BasicValueFactory &BVF = getBasicVals();
QualType T = Sym->getType();
}
}
+SymbolRef simplify(ProgramStateRef State, SymbolRef Sym) {
+ SValBuilder &SVB = State->getStateManager().getSValBuilder();
+ SVal SimplifiedVal = SVB.simplifySVal(State, SVB.makeSymbolVal(Sym));
+ if (SymbolRef SimplifiedSym = SimplifiedVal.getAsSymbol())
+ return SimplifiedSym;
+ return Sym;
+}
+
} // end of namespace ento
} // end of namespace clang
--- /dev/null
+// RUN: %clang_analyze_cc1 %s \
+// RUN: -analyzer-checker=core \
+// RUN: -analyzer-checker=debug.ExprInspection \
+// RUN: -verify
+
+// Here, we test that symbol simplification in the solver does not produce any
+// crashes.
+
+// expected-no-diagnostics
+
+static int a, b;
+static long c;
+
+static void f(int i, int j)
+{
+ (void)(j <= 0 && i ? i : j);
+}
+
+static void g(void)
+{
+ int d = a - b | (c < 0);
+ for (;;)
+ {
+ f(d ^ c, c);
+ }
+}
--- /dev/null
+// RUN: %clang_analyze_cc1 %s \
+// RUN: -analyzer-checker=core \
+// RUN: -analyzer-checker=debug.ExprInspection \
+// RUN: -verify
+
+// Here we test that the range based solver equivalency tracking mechanism
+// assigns a properly typed range to the simplified symbol.
+
+void clang_analyzer_printState();
+void clang_analyzer_eval(int);
+
+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 this point b1 is considered 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.
+
+ clang_analyzer_eval(a0 - b0 != 0); // expected-warning{{TRUE}}
+ }
+}