From f935cfe277fbf839ba149b45b6d27418a8e16a8c Mon Sep 17 00:00:00 2001 From: Ted Kremenek Date: Wed, 3 Dec 2008 18:56:12 +0000 Subject: BasicConstraintManager: - Fix nonsensical logic in AssumeSymLE. When comparing 'sym <= constant' and the constant is the minimum integer value, add the constraint that 'sym == constant' when the path is deemed feasible. All other cases are feasible. - Improve AssumeSymLT to address . When comparing 'sym < constant' and constant is the minimum integer value we know the path is infeasible. - Add test case for . llvm-svn: 60489 --- clang/lib/Analysis/BasicConstraintManager.cpp | 30 +++++++++++++++++++++------ 1 file changed, 24 insertions(+), 6 deletions(-) (limited to 'clang/lib/Analysis/BasicConstraintManager.cpp') diff --git a/clang/lib/Analysis/BasicConstraintManager.cpp b/clang/lib/Analysis/BasicConstraintManager.cpp index 5ce95a1e565..c8065d18690 100644 --- a/clang/lib/Analysis/BasicConstraintManager.cpp +++ b/clang/lib/Analysis/BasicConstraintManager.cpp @@ -312,6 +312,13 @@ BasicConstraintManager::AssumeSymEQ(const GRState* St, SymbolID sym, const GRState* BasicConstraintManager::AssumeSymLT(const GRState* St, SymbolID sym, const llvm::APSInt& V, bool& isFeasible) { + + // Is 'V' the smallest possible value? + if (V == llvm::APSInt::getMinValue(V.getBitWidth(), V.isSigned())) { + // sym cannot be any value less than 'V'. This path is infeasible. + isFeasible = false; + return St; + } // FIXME: For now have assuming x < y be the same as assuming sym != V; return AssumeSymNE(St, sym, V, isFeasible); @@ -345,17 +352,28 @@ const GRState* BasicConstraintManager::AssumeSymLE(const GRState* St, SymbolID sym, const llvm::APSInt& V, bool& isFeasible) { - // FIXME: Primitive logic for now. Only reject a path if the value of - // sym is a constant X and !(X <= V). - + // Reject a path if the value of sym is a constant X and !(X <= V). if (const llvm::APSInt* X = getSymVal(St, sym)) { isFeasible = *X <= V; return St; } - isFeasible = !isNotEqual(St, sym, V) || - (V != llvm::APSInt::getMinValue(V.getBitWidth(), V.isSigned())); - + // Sym is not a constant, but it is worth looking to see if V is the + // minimum integer value. + if (V == llvm::APSInt::getMinValue(V.getBitWidth(), V.isSigned())) { + // If we know that sym != V, then this condition is infeasible since + // there is no other value less than V. + isFeasible = !isNotEqual(St, sym, V); + + // If the path is still feasible then as a consequence we know that + // 'sym == V' because we cannot have 'sym < V' (no smaller values). + // Add this constraint. + if (isFeasible) + return AddEQ(St, sym, V); + } + else + isFeasible = true; + return St; } -- cgit v1.2.3