mikhail.ramalho updated this revision to Diff 239186.
mikhail.ramalho added a comment.
Herald added subscribers: llvm-commits, hiraditya.
Herald added a project: LLVM.
Two changes:
- Moved the BoolAssignmentChecker changes to separate revision (D73062
<https://reviews.llvm.org/D73062>).
- Rebased on top of master.
There are a few cases failing, some because clang is trying to match some
strings printed by the ranged constraint manager and there is at least 1
segfault.
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D28955/new/
https://reviews.llvm.org/D28955
Files:
clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h
clang/lib/StaticAnalyzer/Core/ProgramState.cpp
clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
clang/lib/StaticAnalyzer/Core/Store.cpp
llvm/include/llvm/Support/SMTAPI.h
llvm/lib/Support/Z3Solver.cpp
Index: llvm/lib/Support/Z3Solver.cpp
===================================================================
--- llvm/lib/Support/Z3Solver.cpp
+++ llvm/lib/Support/Z3Solver.cpp
@@ -872,6 +872,8 @@
bool isFPSupported() override { return true; }
+ bool isExtTruncSupported() override { return true; }
+
/// Reset the solver and remove all constraints.
void reset() override { Z3_solver_reset(Context.Context, Solver); }
Index: llvm/include/llvm/Support/SMTAPI.h
===================================================================
--- llvm/include/llvm/Support/SMTAPI.h
+++ llvm/include/llvm/Support/SMTAPI.h
@@ -433,6 +433,9 @@
/// Checks if the solver supports floating-points.
virtual bool isFPSupported() = 0;
+ /// Checks if the solver supports extension/truncation.
+ virtual bool isExtTruncSupported() = 0;
+
virtual void print(raw_ostream &OS) const = 0;
};
Index: clang/lib/StaticAnalyzer/Core/Store.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/Store.cpp
+++ clang/lib/StaticAnalyzer/Core/Store.cpp
@@ -532,7 +532,9 @@
elementType, Offset, cast<SubRegion>(ElemR->getSuperRegion()), Ctx));
}
- const llvm::APSInt& OffI = Offset.castAs<nonloc::ConcreteInt>().getValue();
+ // FIXME: This isn't quite correct, but avoids casting the Offset symbol
+ llvm::APSInt OffI = APSIntType(BaseIdxI).convert(
+ Offset.castAs<nonloc::ConcreteInt>().getValue());
assert(BaseIdxI.isSigned());
// Compute the new index.
Index: clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
+++ clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
@@ -72,6 +72,8 @@
}
SVal SimpleSValBuilder::evalCastFromNonLoc(NonLoc val, QualType castTy) {
+ ConstraintManager &CM = getStateManager().getConstraintManager();
+
bool isLocType = Loc::isLocType(castTy);
if (val.getAs<nonloc::PointerToMember>())
return val;
@@ -79,28 +81,37 @@
if (Optional<nonloc::LocAsInteger> LI = val.getAs<nonloc::LocAsInteger>()) {
if (isLocType)
return LI->getLoc();
+
// FIXME: Correctly support promotions/truncations.
- unsigned castSize = Context.getIntWidth(castTy);
- if (castSize == LI->getNumBits())
+ unsigned castSize = Context.getTypeSize(castTy);
+ if (!CM.canReasonAboutSymbolicExtTrunc() && castSize == LI->getNumBits())
return val;
+
return makeLocAsInteger(LI->getLoc(), castSize);
}
if (const SymExpr *se = val.getAsSymbolicExpression()) {
QualType T = Context.getCanonicalType(se->getType());
- // If types are the same or both are integers, ignore the cast.
+ // If types are the same, ignore the cast.
+ if (haveSameType(T, castTy))
+ return val;
+
+ // If types are both integers, ignore the cast.
// FIXME: Remove this hack when we support symbolic truncation/extension.
// HACK: If both castTy and T are integers, ignore the cast. This is
// not a permanent solution. Eventually we want to precisely handle
// extension/truncation of symbolic integers. This prevents us from losing
// precision when we assign 'x = y' and 'y' is symbolic and x and y are
// different integer types.
- if (haveSameType(T, castTy))
+ if (!CM.canReasonAboutSymbolicExtTrunc() &&
+ (T->isIntegralOrEnumerationType() &&
+ castTy->isIntegralOrEnumerationType()))
return val;
- if (!isLocType)
- return makeNonLoc(se, T, castTy);
- return UnknownVal();
+ if (isLocType)
+ return UnknownVal();
+
+ return makeNonLoc(se, T, castTy);
}
// If value is a non-integer constant, produce unknown.
Index: clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
@@ -120,7 +120,8 @@
case nonloc::ConcreteIntKind: {
const llvm::APSInt &IntVal = Value.castAs<nonloc::ConcreteInt>().getValue();
- bool IsInRange = IntVal >= From && IntVal <= To;
+ bool IsInRange = llvm::APSInt::compareValues(IntVal, From) != -1 &&
+ llvm::APSInt::compareValues(IntVal, To) != 1;
bool isFeasible = (IsInRange == InRange);
return isFeasible ? State : nullptr;
}
Index: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -254,6 +254,8 @@
bool canReasonAbout(SVal X) const override;
+ bool canReasonAboutSymbolicExtTrunc() const override;
+
ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override;
const llvm::APSInt *getSymVal(ProgramStateRef State,
@@ -379,6 +381,10 @@
return true;
}
+bool RangeConstraintManager::canReasonAboutSymbolicExtTrunc() const {
+ return false;
+}
+
ConditionTruthVal RangeConstraintManager::checkNull(ProgramStateRef State,
SymbolRef Sym) {
const RangeSet *Ranges = State->get<ConstraintRange>(Sym);
Index: clang/lib/StaticAnalyzer/Core/ProgramState.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/ProgramState.cpp
+++ clang/lib/StaticAnalyzer/Core/ProgramState.cpp
@@ -267,12 +267,12 @@
// to the type of T, which is not always the case (e.g. for void).
if (!T.isNull() && (T->isIntegralOrEnumerationType() || Loc::isLocType(T))) {
if (SymbolRef sym = V.getAsSymbol()) {
- if (const llvm::APSInt *Int = getStateManager()
- .getConstraintManager()
- .getSymVal(this, sym)) {
+ ConstraintManager &CM = getStateManager().getConstraintManager();
+
+ if (const llvm::APSInt *Int = CM.getSymVal(this, sym)) {
// FIXME: Because we don't correctly model (yet) sign-extension
// and truncation of symbolic values, we need to convert
- // the integer value to the correct signedness and bitwidth.
+ // the integer value to the correct signedness and
//
// This shows up in the following:
//
@@ -284,12 +284,13 @@
// The symbolic value stored to 'x' is actually the conjured
// symbol for the call to foo(); the type of that symbol is 'char',
// not unsigned.
- const llvm::APSInt &NewV = getBasicVals().Convert(T, *Int);
+ if (!CM.canReasonAboutSymbolicExtTrunc())
+ Int = &getBasicVals().Convert(T, *Int);
if (V.getAs<Loc>())
- return loc::ConcreteInt(NewV);
+ return loc::ConcreteInt(*Int);
else
- return nonloc::ConcreteInt(NewV);
+ return nonloc::ConcreteInt(*Int);
}
}
}
Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h
===================================================================
--- clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h
+++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h
@@ -90,16 +90,8 @@
virtual ~SValBuilder() = default;
- bool haveSameType(const SymExpr *Sym1, const SymExpr *Sym2) {
- return haveSameType(Sym1->getType(), Sym2->getType());
- }
-
bool haveSameType(QualType Ty1, QualType Ty2) {
- // FIXME: Remove the second disjunct when we support symbolic
- // truncation/extension.
- return (Context.getCanonicalType(Ty1) == Context.getCanonicalType(Ty2) ||
- (Ty1->isIntegralOrEnumerationType() &&
- Ty2->isIntegralOrEnumerationType()));
+ return (Context.getCanonicalType(Ty1) == Context.getCanonicalType(Ty2));
}
SVal evalCast(SVal val, QualType castTy, QualType originalType);
Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
===================================================================
--- clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
+++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
@@ -288,6 +288,10 @@
llvm_unreachable("Unsupported expression to reason about!");
}
+ bool canReasonAboutSymbolicExtTrunc() const override {
+ return Solver->isExtTruncSupported();
+ }
+
/// Dumps SMT formula
LLVM_DUMP_METHOD void dump() const { Solver->dump(); }
Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
===================================================================
--- clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
+++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
@@ -174,6 +174,11 @@
return checkNull(State, Sym);
}
+ /// canReasonAboutSymbolicExtTrunc - Not all ConstraintManagers can reason
+ /// symbolic extension and truncation. Used this to ask directly when
+ /// building SVals.
+ virtual bool canReasonAboutSymbolicExtTrunc() const = 0;
+
protected:
/// A flag to indicate that clients should be notified of assumptions.
/// By default this is the case, but sometimes this needs to be restricted
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
