danielmarjamaki updated this revision to Diff 121726.
danielmarjamaki added a comment.
Herald added a subscriber: szepet.
I have updated the patch so it uses evalBinOpNN. This seems to work properly.
I have a number of TODOs in the test cases that should be fixed. Truncations
are not handled properly.
Here is a short example code:
void f(unsigned char X) {
if (X >= 10 && X <= 50) {
unsigned char Y = X + 0x100; // truncation
clang_analyzer_eval(Y >= 10 && Y <= 50); // expected-warning{{FALSE}}
}
}
The expected-warning should be TRUE but currently FALSE is written.
When the "Y >= 10" condition is evaluated the ProgramState is:
Store (direct and default bindings), 0x222ab0fe5f8 :
(Y,0,direct) : (unsigned char) ((reg_$0<unsigned char X>) + 256)
Expressions:
(0x222a96d6050,0x222ab0eb930) X + 256 : (unsigned char) ((reg_$0<unsigned
char X>) + 256)
(0x222a96d6050,0x222ab0eb960) clang_analyzer_eval :
&code{clang_analyzer_eval}
(0x222a96d6050,0x222ab0eb988) Y : &Y
(0x222a96d6050,0x222ab0eb9d8) Y : (unsigned char) ((reg_$0<unsigned char X>)
+ 256)
(0x222a96d6050,0x222ab0eb9f0) Y : (unsigned char) ((reg_$0<unsigned char X>)
+ 256)
(0x222a96d6050,0x222ab0eba08) Y >= 10 : ((unsigned char) ((reg_$0<unsigned
char X>) + 256)) >= 10
(0x222a96d6050,0x222ab0ebb28) clang_analyzer_eval :
&code{clang_analyzer_eval}
Ranges of symbol values:
reg_$0<unsigned char X> : { [10, 50] }
(reg_$0<unsigned char X>) + 256 : { [10, 50] }
It seems to me that the symbol initialization does not handle the range
properly. Imho there is nothing wrong with the calculation. What you think
about adding a range like below?
(unsigned char) ((reg_$0<unsigned char X>) + 256) : { [10, 50] }
Repository:
rL LLVM
https://reviews.llvm.org/D36471
Files:
include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h
lib/StaticAnalyzer/Core/ExprEngineC.cpp
lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
test/Analysis/range_calc.c
Index: test/Analysis/range_calc.c
===================================================================
--- test/Analysis/range_calc.c
+++ test/Analysis/range_calc.c
@@ -0,0 +1,143 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -verify %s
+
+void clang_analyzer_eval(int);
+
+#define INT_MAX ((signed int)((~0U)>>1))
+#define INT_MIN ((signed int)(~((~0U)>>1)))
+
+void addInts(int X)
+{
+ if (X >= 10 && X <= 50) {
+ int Y = X + 2;
+ clang_analyzer_eval(Y >= 12 && Y <= 52); // expected-warning{{TRUE}}
+ }
+
+ if (X < 5) {
+ int Y = X + 1;
+ clang_analyzer_eval(Y < 6); // expected-warning{{TRUE}}
+ }
+
+ if (X >= 1000) {
+ int Y = X + 1; // might overflow
+ clang_analyzer_eval(Y >= 1001); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(Y == INT_MIN); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(Y == INT_MIN || Y >= 1001); // expected-warning{{TRUE}}
+ }
+}
+
+void addU8(unsigned char X)
+{
+ if (X >= 10 && X <= 50) {
+ unsigned char Y = X + 2;
+ clang_analyzer_eval(Y >= 12 && Y <= 52); // expected-warning{{TRUE}}
+ }
+
+ if (X < 5) {
+ unsigned char Y = X + 1;
+ clang_analyzer_eval(Y < 6); // expected-warning{{TRUE}}
+ }
+
+ // TODO
+ if (X >= 10 && X <= 50) {
+ unsigned char Y = X + (-256); // truncation
+ clang_analyzer_eval(Y >= 10 && Y <= 50); // expected-warning{{FALSE}}
+ }
+
+ // TODO
+ if (X >= 10 && X <= 50) {
+ unsigned char Y = X + 256; // truncation
+ clang_analyzer_eval(Y >= 10 && Y <= 50); // expected-warning{{FALSE}} expected-warning{{UNKNOWN}}
+ }
+
+ // TODO
+ if (X >= 100) {
+ unsigned char Y = X + 1; // truncation
+ clang_analyzer_eval(Y == 0); // expected-warning{{FALSE}}}}
+ clang_analyzer_eval(Y >= 101); // expected-warning{{TRUE}}
+ clang_analyzer_eval(Y == 0 || Y >= 101); // expected-warning{{TRUE}}
+ }
+
+ if (X >= 100) {
+ unsigned short Y = X + 1;
+ clang_analyzer_eval(Y >= 101 && Y <= 256); // expected-warning{{TRUE}}
+ }
+}
+
+void sub1(int X)
+{
+ if (X >= 10 && X <= 50) {
+ int Y = X - 2;
+ clang_analyzer_eval(Y >= 8 && Y <= 48); // expected-warning{{TRUE}}
+ }
+
+ if (X >= 10 && X <= 50) {
+ unsigned char Y = (unsigned int)X - 20; // truncation
+ clang_analyzer_eval(Y <= 30 || Y >= 246); // expected-warning{{TRUE}}
+ }
+
+ // TODO
+ if (X >= 10 && X <= 50) {
+ unsigned char Y = (unsigned int)X - 256; // truncation
+ clang_analyzer_eval(Y >= 10 && Y <= 50); // expected-warning{{FALSE}} expected-warning{{UNKNOWN}}
+ }
+
+ if (X < 5) {
+ int Y = X - 1; // might overflow
+ clang_analyzer_eval(Y < 4); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(Y == INT_MAX); // expected-warning{{UNKNOWN}}
+ clang_analyzer_eval(Y == INT_MAX || Y < 4); // expected-warning{{TRUE}}
+ }
+
+ if (X >= 1000) {
+ int Y = X - 1;
+ clang_analyzer_eval(Y >= 999); // expected-warning{{TRUE}}
+ }
+}
+
+void subU8(unsigned char X)
+{
+ if (X >= 10 && X <= 50) {
+ unsigned char Y = X - 2;
+ clang_analyzer_eval(Y >= 8 && Y <= 48); // expected-warning{{TRUE}}
+ }
+
+ if (X >= 100) {
+ unsigned char Y = X - 1;
+ clang_analyzer_eval(Y >= 99 && Y <= 254); // expected-warning{{TRUE}}
+ }
+
+ if (X < 5) {
+ unsigned char Y = X - 1; // overflow
+ clang_analyzer_eval(Y < 4 || Y == 255); // expected-warning{{TRUE}}
+ }
+
+ // TODO
+ if (X >= 10 && X <= 50) {
+ unsigned char Y = X - (-256); // truncation
+ clang_analyzer_eval(Y >= 10 && Y <= 50); // expected-warning{{FALSE}} expected-warning{{UNKNOWN}}
+ }
+
+ // TODO
+ if (X >= 10 && X <= 50) {
+ unsigned char Y = X - 256; // truncation
+ clang_analyzer_eval(Y >= 10 && Y <= 50); // expected-warning{{FALSE}}
+ }
+
+ if (X >= 100) {
+ unsigned short Y = X + 1;
+ clang_analyzer_eval(Y >= 101 && Y <= 256); // expected-warning{{TRUE}}
+ }
+}
+
+void div(int X)
+{
+ if (X >= 10 && X <= 50) {
+ int Y = X / 2;
+ clang_analyzer_eval(Y >= 5); // expected-warning{{TRUE}}
+ clang_analyzer_eval(Y <= 25); // expected-warning{{TRUE}}
+ }
+
+ // No overflows
+}
+
+
Index: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===================================================================
--- lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -304,6 +304,8 @@
void print(ProgramStateRef State, raw_ostream &Out, const char *nl,
const char *sep) override;
+ ProgramStateRef evalRangeOp(ProgramStateRef state, SVal V) override;
+
//===------------------------------------------------------------------===//
// Implementation for interface from RangedConstraintManager.
//===------------------------------------------------------------------===//
@@ -741,3 +743,55 @@
}
Out << nl;
}
+
+ProgramStateRef RangeConstraintManager::evalRangeOp(ProgramStateRef St,
+ SVal V) {
+ const SymExpr *SE = V.getAsSymExpr();
+ if (!SE)
+ return nullptr;
+
+ const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SE);
+ if (!SIE)
+ return nullptr;
+
+ const clang::BinaryOperatorKind Opc = SIE->getOpcode();
+
+ if (Opc != BO_Add && Opc != BO_Sub && Opc != BO_Div)
+ return nullptr;
+
+ const SymExpr *LHS = SIE->getLHS();
+ const llvm::APSInt &RHS = SIE->getRHS();
+
+ ConstraintRangeTy Ranges = St->get<ConstraintRange>();
+ for (ConstraintRangeTy::iterator I = Ranges.begin(), E = Ranges.end(); I != E;
+ ++I) {
+ if (LHS != I.getKey())
+ continue;
+ const auto D = I.getData();
+ for (auto I = D.begin(); I != D.end(); ++I) {
+ NonLoc FromN = SVB.makeIntVal(I->From()).castAs<NonLoc>();
+ NonLoc ToN = SVB.makeIntVal(I->To()).castAs<NonLoc>();
+ NonLoc RHSN = SVB.makeIntVal(RHS).castAs<NonLoc>();
+
+ // Calculate Lower value.
+ SVal Tmp = SVB.evalBinOpNN(St, Opc, FromN, RHSN, LHS->getType());
+ const llvm::APSInt &Lower = Tmp.castAs<nonloc::ConcreteInt>().getValue();
+
+ // Calculate Upper value.
+ Tmp = SVB.evalBinOpNN(St, Opc, ToN, RHSN, LHS->getType());
+ const llvm::APSInt &Upper = Tmp.castAs<nonloc::ConcreteInt>().getValue();
+
+ // TODO: Handle truncations better
+ if (Lower > Upper)
+ continue;
+
+ // Set Range for symbol.
+ SymbolRef Sym = V.getAsSymbol();
+ RangeSet RS =
+ getRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
+ // TODO: This only evaluates the first range. Evaluate all ranges.
+ return RS.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, RS);
+ }
+ }
+ return nullptr;
+}
Index: lib/StaticAnalyzer/Core/ExprEngineC.cpp
===================================================================
--- lib/StaticAnalyzer/Core/ExprEngineC.cpp
+++ lib/StaticAnalyzer/Core/ExprEngineC.cpp
@@ -94,9 +94,13 @@
SVal Result = evalBinOp(state, Op, LeftV, RightV, B->getType());
if (!Result.isUnknown()) {
state = state->BindExpr(B, LCtx, Result);
+ ProgramStateRef state2 =
+ getConstraintManager().evalRangeOp(state, Result);
+ Bldr.generateNode(B, *it, state2 ? state2 : state);
+ } else {
+ Bldr.generateNode(B, *it, state);
}
- Bldr.generateNode(B, *it, state);
continue;
}
Index: include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h
===================================================================
--- include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h
+++ include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h
@@ -23,6 +23,8 @@
class SimpleConstraintManager : public ConstraintManager {
SubEngine *SU;
+
+protected:
SValBuilder &SVB;
public:
Index: include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
===================================================================
--- include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
+++ include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
@@ -142,13 +142,15 @@
/// Scan all symbols referenced by the constraints. If the symbol is not
/// alive, remove it.
virtual ProgramStateRef removeDeadBindings(ProgramStateRef state,
- SymbolReaper& SymReaper) = 0;
+ SymbolReaper &SymReaper) = 0;
- virtual void print(ProgramStateRef state,
- raw_ostream &Out,
- const char* nl,
+ virtual void print(ProgramStateRef state, raw_ostream &Out, const char *nl,
const char *sep) = 0;
+ virtual ProgramStateRef evalRangeOp(ProgramStateRef state, SVal V) {
+ return nullptr;
+ }
+
virtual void EndPath(ProgramStateRef state) {}
/// Convenience method to query the state to see if a symbol is null or
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
