summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorZancanaro; Carlo <czan8762@plang3.cs.usyd.edu.au>2012-10-04 17:11:33 +1000
committerZancanaro; Carlo <czan8762@plang3.cs.usyd.edu.au>2012-10-04 17:11:33 +1000
commit684045e9e843ed9b8be30728482ce3d69d63b527 (patch)
tree0707aa71b902384766a7c0eb4d901fac9a5cbb63
parentf168645671e31b5d2e7fb134b9d9f8750aebb872 (diff)
Lets keep trying with this here equation system.
Still not there, but more non-functional code is there. Splitting blocks into sub-blocks now works, as does some of the guard stuff and the general "shape" of the resulting equation system.
l---------clang/include/clang/Analysis/Analyses/IntervalSolver/.#EquationSystem.hpp1
l---------clang/include/clang/Analysis/Analyses/IntervalSolver/.#EquationSystem_flymake.hpp1
l---------clang/include/clang/Analysis/Analyses/IntervalSolver/.#Expression.hpp1
l---------clang/include/clang/Analysis/Analyses/IntervalSolver/.#Expression_flymake.hpp1
l---------clang/include/clang/Analysis/Analyses/IntervalSolver/.#Operator_flymake.hpp1
-rw-r--r--clang/include/clang/Analysis/Analyses/IntervalSolver/EquationSystem.hpp21
-rw-r--r--clang/include/clang/Analysis/Analyses/IntervalSolver/Expression.hpp5
-rw-r--r--clang/include/clang/Analysis/Analyses/IntervalSolver/IdMap.hpp2
-rw-r--r--clang/include/clang/Analysis/Analyses/IntervalSolver/Operator.hpp7
-rw-r--r--clang/include/clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp2
-rw-r--r--clang/include/clang/Frontend/Analyses.def1
-rw-r--r--clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h2
l---------clang/lib/Analysis/.#Interval.cpp1
l---------clang/lib/Analysis/.#Interval_flymake.cpp1
-rw-r--r--clang/lib/Analysis/Interval.cpp535
-rw-r--r--clang/lib/StaticAnalyzer/Core/IntervalConstraintManager.cpp442
16 files changed, 902 insertions, 122 deletions
diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/.#EquationSystem.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/.#EquationSystem.hpp
deleted file mode 120000
index 56b9060..0000000
--- a/clang/include/clang/Analysis/Analyses/IntervalSolver/.#EquationSystem.hpp
+++ /dev/null
@@ -1 +0,0 @@
-carlo@pc-4w14-0.cs.usyd.edu.au.4300:1348200365 \ No newline at end of file
diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/.#EquationSystem_flymake.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/.#EquationSystem_flymake.hpp
deleted file mode 120000
index 4dc56be..0000000
--- a/clang/include/clang/Analysis/Analyses/IntervalSolver/.#EquationSystem_flymake.hpp
+++ /dev/null
@@ -1 +0,0 @@
-carlo@pc-4w14-0.cs.usyd.edu.au.9390:1348126501 \ No newline at end of file
diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/.#Expression.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/.#Expression.hpp
deleted file mode 120000
index 4dc56be..0000000
--- a/clang/include/clang/Analysis/Analyses/IntervalSolver/.#Expression.hpp
+++ /dev/null
@@ -1 +0,0 @@
-carlo@pc-4w14-0.cs.usyd.edu.au.9390:1348126501 \ No newline at end of file
diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/.#Expression_flymake.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/.#Expression_flymake.hpp
deleted file mode 120000
index 4dc56be..0000000
--- a/clang/include/clang/Analysis/Analyses/IntervalSolver/.#Expression_flymake.hpp
+++ /dev/null
@@ -1 +0,0 @@
-carlo@pc-4w14-0.cs.usyd.edu.au.9390:1348126501 \ No newline at end of file
diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/.#Operator_flymake.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/.#Operator_flymake.hpp
deleted file mode 120000
index 4dc56be..0000000
--- a/clang/include/clang/Analysis/Analyses/IntervalSolver/.#Operator_flymake.hpp
+++ /dev/null
@@ -1 +0,0 @@
-carlo@pc-4w14-0.cs.usyd.edu.au.9390:1348126501 \ No newline at end of file
diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/EquationSystem.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/EquationSystem.hpp
index 701da7c..d95366d 100644
--- a/clang/include/clang/Analysis/Analyses/IntervalSolver/EquationSystem.hpp
+++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/EquationSystem.hpp
@@ -91,22 +91,18 @@ struct EquationSystem {
void indexMaxExpressions() {
_expr_to_var = new IdMap<MaxExpression<Domain>,Variable<Domain>*>(maxExpressionCount(), NULL);
for (unsigned int i = 0, length = _right_sides.size(); i < length; ++i) {
- _right_sides[i]->mapTo(*_variables[i], *_expr_to_var);
+ if (_right_sides[i])
+ _right_sides[i]->mapTo(*_variables[i], *_expr_to_var);
}
}
Variable<Domain>* varFromExpr(const Expression<Domain>& expr) const {
- if (_expr_to_var) { // we've indexed:
- const MaxExpression<Domain>* maxExpr = expr.toMaxExpression();//dynamic_cast<const MaxExpression<Domain>*>(&expr);
- if (maxExpr) {
- return (*_expr_to_var)[*maxExpr];
- } else {
- return NULL;
- }
+ assert(_expr_to_var != NULL); // ensure we've indexed
+ const MaxExpression<Domain>* maxExpr = expr.toMaxExpression();//dynamic_cast<const MaxExpression<Domain>*>(&expr);
+ if (maxExpr) {
+ return (*_expr_to_var)[*maxExpr];
} else {
- std::cout << "throw exception" << *(char*)NULL;
return NULL;
- //throw "Must index max expressions before attempting lookup";
}
}
@@ -125,7 +121,10 @@ struct EquationSystem {
for (unsigned int i = 0, length = _variables.size();
i < length;
++i) {
- cout << *_variables[i] << " = " << *_right_sides[i] << std::endl;
+ if (_right_sides[i])
+ cout << *_variables[i] << " = " << *_right_sides[i] << std::endl;
+ else
+ cout << *_variables[i] << " = NULL" << std::endl;
}
}
diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/Expression.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/Expression.hpp
index 7b0f2cf..c4ee4c0 100644
--- a/clang/include/clang/Analysis/Analyses/IntervalSolver/Expression.hpp
+++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/Expression.hpp
@@ -84,7 +84,9 @@ struct Variable : public Expression<Domain> {
template<typename Domain>
struct OperatorExpression : public Expression<Domain> {
OperatorExpression(const Operator<Domain>& op, const std::vector<Expression<Domain>*>& arguments)
- : _operator(op), _arguments(arguments) { }
+ : _operator(op), _arguments(arguments) {
+ assert(!arguments.empty());
+ }
virtual Domain eval(const VariableAssignment<Domain>& rho) const {
std::vector<Domain> argumentValues;
@@ -145,7 +147,6 @@ struct MaxExpression : public OperatorExpression<Domain> {
MaxExpression(const unsigned int& id, const Maximum<Domain>& op, const std::vector<Expression<Domain>*>& arguments)
: OperatorExpression<Domain>(op, arguments), _id(id) { }
-
const MaxExpression* toMaxExpression() const {
return this;
}
diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/IdMap.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/IdMap.hpp
index 27c0806..5e3aa3b 100644
--- a/clang/include/clang/Analysis/Analyses/IntervalSolver/IdMap.hpp
+++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/IdMap.hpp
@@ -7,7 +7,7 @@ template<typename T, typename V>
struct IdMap {
IdMap(unsigned int length, V initial)
: _length(length), _assignment(new V[length]) {
- for (unsigned int i = 0; i < _length; ++i) {
+ for (unsigned int i = 0; i < length; ++i) {
_assignment[i] = initial;
}
}
diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/Operator.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/Operator.hpp
index b67591f..08c66ff 100644
--- a/clang/include/clang/Analysis/Analyses/IntervalSolver/Operator.hpp
+++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/Operator.hpp
@@ -28,6 +28,11 @@ struct Maximum : public Operator<Domain> {
}
};
+
+template<class T>
+T minimum(const T& l, const T& r) {
+ return (l < r ? l : r);
+}
template<typename Domain>
struct Minimum : public Operator<Domain> {
virtual Domain eval(const std::vector<Domain>& arguments) const {
@@ -35,7 +40,7 @@ struct Minimum : public Operator<Domain> {
for (typename std::vector<Domain>::const_iterator it = arguments.begin();
it != arguments.end();
++it) {
- result = (*it < result ? *it : result);
+ result = minimum(*it, result); //*it < result ? *it : result);
}
return result;
}
diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp
index d2adff5..0bbebfc 100644
--- a/clang/include/clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp
+++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp
@@ -47,6 +47,8 @@ private:
solver_log::fixpoint << indent() << "Stabilise " << x << std::endl;
stack_depth++;
+ if (!_system[x])
+ return;
Domain val = _system[x]->eval(DependencyAssignment(*this, x),
_strategy);
stack_depth--;
diff --git a/clang/include/clang/Frontend/Analyses.def b/clang/include/clang/Frontend/Analyses.def
index b5b9394..902575f 100644
--- a/clang/include/clang/Frontend/Analyses.def
+++ b/clang/include/clang/Frontend/Analyses.def
@@ -23,6 +23,7 @@ ANALYSIS_STORE(RegionStore, "region", "Use region-based analyzer store", CreateR
ANALYSIS_CONSTRAINTS(BasicConstraints, "basic", "Use basic constraint tracking", CreateBasicConstraintManager)
ANALYSIS_CONSTRAINTS(RangeConstraints, "range", "Use constraint tracking of concrete value ranges", CreateRangeConstraintManager)
+ANALYSIS_CONSTRAINTS(IntervalConstraints, "interval", "Use constraint tracking of intervals", CreateIntervalConstraintManager)
#ifndef ANALYSIS_DIAGNOSTICS
#define ANALYSIS_DIAGNOSTICS(NAME, CMDFLAG, DESC, CREATEFN, AUTOCREATE)
diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
index 631858d..4051cfc 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
@@ -73,6 +73,8 @@ ConstraintManager* CreateBasicConstraintManager(ProgramStateManager& statemgr,
SubEngine &subengine);
ConstraintManager* CreateRangeConstraintManager(ProgramStateManager& statemgr,
SubEngine &subengine);
+ConstraintManager* CreateIntervalConstraintManager(ProgramStateManager& statemgr,
+ SubEngine &subengine);
} // end GR namespace
diff --git a/clang/lib/Analysis/.#Interval.cpp b/clang/lib/Analysis/.#Interval.cpp
deleted file mode 120000
index 235903b..0000000
--- a/clang/lib/Analysis/.#Interval.cpp
+++ /dev/null
@@ -1 +0,0 @@
-carlo@pc-4w14-0.cs.usyd.edu.au.1585:1347012043 \ No newline at end of file
diff --git a/clang/lib/Analysis/.#Interval_flymake.cpp b/clang/lib/Analysis/.#Interval_flymake.cpp
deleted file mode 120000
index 235903b..0000000
--- a/clang/lib/Analysis/.#Interval_flymake.cpp
+++ /dev/null
@@ -1 +0,0 @@
-carlo@pc-4w14-0.cs.usyd.edu.au.1585:1347012043 \ No newline at end of file
diff --git a/clang/lib/Analysis/Interval.cpp b/clang/lib/Analysis/Interval.cpp
index 726c6de..96dd841 100644
--- a/clang/lib/Analysis/Interval.cpp
+++ b/clang/lib/Analysis/Interval.cpp
@@ -17,12 +17,10 @@
#include <algorithm>
#include <vector>
#include <map>
+#include <set>
using namespace clang;
-typedef EquationSystem<Complete<int> > EqnSys;
-typedef Expression<Complete<int> > EqnExpr;
-
#include <sstream>
template<typename T>
std::string toString(const T& obj) {
@@ -31,6 +29,28 @@ std::string toString(const T& obj) {
return stream.str();
}
+#include <ostream>
+template<typename K,typename V>
+std::ostream& operator<<(std::ostream& cout, const std::pair<K,V>& v) {
+ cout << "(" << v.first << ", " << v.second << ")";
+ return cout;
+}
+
+template<typename K,typename V>
+std::ostream& operator<<(std::ostream& cout, const std::map<K,V>& v) {
+ cout << "{";
+ for (typename std::map<K,V>::const_iterator it = v.begin(), ei = v.end();
+ it != ei;
+ ++it) {
+ if (it != v.begin())
+ cout << ", ";
+ cout << it->first << ": " << it->second;
+ }
+ cout << "}";
+ return cout;
+}
+
+
IntervalAnalysis :: IntervalAnalysis(AnalysisDeclContext &context)
: context(&context) {
}
@@ -48,9 +68,89 @@ IntervalAnalysis :: ~IntervalAnalysis() {
// Hooray!
typedef Complete<int64_t> ZBar;
-typedef std::map<std::string, ZBar> Vector;
+//typedef std::map<std::string, ZBar> Vector;
+
+struct Vector : public std::map<std::string, ZBar> {
+ Vector(const ZBar& val=infinity<ZBar>())
+ : _val(val) { }
+ ZBar operator[](const std::string& key) const {
+ if (this->find(key) != this->end())
+ return this->find(key)->second;
+ return _val;
+ }
+ ZBar& operator[](const std::string& key) {
+ if (this->find(key) != this->end())
+ return this->find(key)->second;
+ std::pair<iterator,bool> p = this->insert(std::pair<const std::string, ZBar>(key, _val));
+ return p.first->second;
+ }
+ ZBar _val;
+};
+
typedef std::pair<Vector, ZBar> Result; // a "slice" of an equation
+//typedef std::map<std::string, Result> LinearEquation; // one `Result` per variable
+struct LinearEquation : public std::map<std::string, Result> {
+ Result operator[](const std::string& key) const {
+ if (this->find(key) != this->end())
+ return this->find(key)->second;
+ Result r;
+ r.first[key] = 1;
+ r.second = 0;
+ return r;
+ }
+ Result& operator[](const std::string& key) {
+ if (this->find(key) != this->end())
+ return this->find(key)->second;
+ Result r;
+ r.first[key] = 1;
+ r.second = 0;
+ std::pair<iterator,bool> p = this->insert(std::pair<const std::string, Result>(key, r));
+ return p.first->second;
+ }
+};
+
+typedef Vector Condition;
+
+typedef EquationSystem<Vector> EqnSys;
+typedef Expression<Vector> EqnExpr;
+typedef Variable<Vector> EqnVar;
+
+
+struct LinearOperator : public Operator<Vector> {
+ LinearOperator(const LinearEquation& result)
+ : _values(result) {}
+
+ Vector eval(const std::vector<Vector>& vector) const {
+ assert(vector.size() == 1);
+ const Vector& v = vector[0];
+ Vector result = v;
+ for (LinearEquation::const_iterator it = _values.begin(),
+ ei = _values.end();
+ it != ei;
+ ++it) {
+ ZBar subresult = 0;
+ for (Vector::const_iterator jt = it->second.first.begin(),
+ ej = it->second.first.end();
+ jt != ej;
+ ++jt) {
+ subresult += jt->second * v[jt->first];
+ }
+ subresult += it->second.second;
+ result[it->first] = subresult;
+ }
+ return result;
+ }
+
+ void print(std::ostream& cout) const {
+ cout << "linear[" << _values << "]";
+ }
+
+ LinearEquation _values;
+};
+
+
+
template<class F, class M>
void transform_values(const F& f, M& map) {
for (typename M::iterator it = map.begin(),
@@ -90,6 +190,14 @@ M merge_maps_with(const F& f, const M& left, const M& right) {
return result;
}
+template<>
+Vector minimum(const Vector& l, const Vector& r) {
+ return merge_maps_with(minimum<ZBar>, l, r);
+}
+template<class T>
+T max(const T& l, const T& r) {
+ return (l < r ? l : r);
+}
template<class T>
T negate(const T& v) {
return -v;
@@ -98,25 +206,90 @@ template<class T>
T addValues(const T& l, const T& r) {
return l + r;
}
-template<class T>
-T subValues(const T& l, const T& r) {
- return l - r;
+
+Vector operator-(const Vector& vector) {
+ Vector result(-vector._val);
+ for (Vector::const_iterator it = vector.begin(),
+ ei = vector.end();
+ it != ei;
+ ++it) {
+ result[it->first] = -it->second;
+ }
+ return result;
+}
+
+Vector operator+(const Vector& left, const Vector& right) {
+ return merge_maps_with(addValues<ZBar>, left, right);
+}
+
+Vector operator-(const Vector& left, const Vector& right) {
+ return merge_maps_with(addValues<ZBar>, left, -right);
+}
+
+Vector operator*(const Vector& left, const ZBar& right) {
+ Vector result;
+ for (Vector::const_iterator it = left.begin(),
+ ei = left.end();
+ it != ei;
+ ++it) {
+ result[it->first] = (it->second * right);
+ }
+ return result;
+}
+Vector operator*(const ZBar& left, const Vector& right) {
+ return right * left;
+}
+bool operator<(const Vector& left, const Vector& right) {
+ for (Vector::const_iterator it = left.begin(),
+ ei = left.end();
+ it != ei;
+ ++it) {
+ if (it->second < right[it->first]) {
+ return true;
+ }
+ }
+ for (Vector::const_iterator it = right.begin(),
+ ei = right.end();
+ it != ei;
+ ++it) {
+ if (left[it->first] < it->second) {
+ return true;
+ }
+ }
+ return false;
+}
+
+template<>
+Vector infinity<Vector>() {
+ return Vector(infinity<ZBar>());
+}
+
+std::ostream& operator<<(std::ostream& cout, const Vector& v) {
+ cout << "{";
+ for (Vector::const_iterator it = v.begin(), ei = v.end();
+ it != ei;
+ ++it) {
+ cout << it->first << ": " << it->second << ", ";
+ }
+ cout << "_: " << v._val;
+ cout << "}";
+ return cout;
}
-Result fromStmt(const Stmt*, EqnSys&);
+Result fromStmt(const Stmt*);
-Result fromInteger(const IntegerLiteral* expr, EqnSys& system) {
+Result fromInteger(const IntegerLiteral* expr) {
return Result(Vector(), *expr->getValue().getRawData());
}
-Result fromDeclExpr(const DeclRefExpr* expr, EqnSys& system) {
+Result fromDeclExpr(const DeclRefExpr* expr) {
Vector val;
val[expr->getNameInfo().getAsString()] = 1;
return Result(val, 0);
}
-Result fromUnary(const UnaryOperator* op, EqnSys& system) {
+Result fromUnary(const UnaryOperator* op) {
switch (op->getOpcode()) {
case UO_PreInc:
break;
@@ -126,18 +299,16 @@ Result fromUnary(const UnaryOperator* op, EqnSys& system) {
return Result(Vector(), 0);
}
-
-Addition<Complete<int> >* add = new Addition<Complete<int> >();
-Subtraction<Complete<int> >* sub = new Subtraction<Complete<int> >();
-Multiplication<Complete<int> >* mul = new Multiplication<Complete<int> >();
-
-Result fromBinary(const BinaryOperator* op, EqnSys& system) {
- Result left = fromStmt(op->getLHS()->IgnoreParenCasts(), system);
- Result right = fromStmt(op->getRHS()->IgnoreParenCasts(), system);
+Result fromBinary(const BinaryOperator* op) {
+ Result left = fromStmt(op->getLHS()->IgnoreParenCasts());
+ Result right = fromStmt(op->getRHS()->IgnoreParenCasts());
switch (op->getOpcode()) {
+ case BO_Assign:
+ return right;
case BO_Sub:
transform_values(negate<ZBar>, right.first);
+ right.second *= -1;
case BO_Add:
{
Result result;
@@ -160,11 +331,27 @@ Result fromBinary(const BinaryOperator* op, EqnSys& system) {
scalar = right.second;
value = left;
}
- for (Vector::iterator it = value.first.begin(),
- ei = value.first.end();
- it != ei;
- ++it) {
- it->second *= scalar;
+ if (scalar > 0) {
+ for (Vector::iterator it = value.first.begin(),
+ ei = value.first.end();
+ it != ei;
+ ++it) {
+ it->second *= scalar;
+ }
+ } else {
+ Vector newValue;
+ for (Vector::iterator it = value.first.begin(),
+ ei = value.first.end();
+ it != ei;
+ ++it) {
+ std::string name;
+ if (it->first[0] == '-') {
+ name = it->first.substr(1);
+ } else {
+ name = '-' + it->first;
+ }
+ newValue[name] = (-scalar) * it->second;
+ }
}
right.second *= scalar;
return value;
@@ -178,21 +365,7 @@ Result fromBinary(const BinaryOperator* op, EqnSys& system) {
return Result();
}
-Result fromDeclStmt(const DeclStmt* stmt, EqnSys& system) {
- /*for (DeclStmt::const_decl_iterator it = stmt->decl_begin(),
- ei = stmt->decl_end();
- it != ei;
- ++it) {
- if ((*it)->getKind() == Decl::Var) {
- const VarDecl* decl = static_cast<const VarDecl*>(*it);
- Variable<Complete<int> > var = system.variable(decl->getNameAsString());
- std::vector<EqnExpr*> args;
- args.push_back(&system.constant(-infinity<Complete<int> >()));
- args.push_back(fromStmt(decl->getInit(), system));
- system[var] = &system.maxExpression(args);
- }
- }*/
-
+Result fromDeclStmt(const DeclStmt* stmt) {
for (DeclStmt::const_decl_iterator it = stmt->decl_begin(),
ei = stmt->decl_end();
it != ei;
@@ -201,110 +374,272 @@ Result fromDeclStmt(const DeclStmt* stmt, EqnSys& system) {
const VarDecl* decl = static_cast<const VarDecl*>(*it);
llvm::errs() << decl->getNameAsString() << " = ";
- Result expr = fromStmt(decl->getInit(), system);
- llvm::errs() << "<{ ";
+ Result expr = fromStmt(decl->getInit());
for (Vector::iterator it = expr.first.begin(),
ei = expr.first.end();
it != ei;
++it) {
if (it != expr.first.begin())
- llvm::errs() << ", ";
- llvm::errs() << toString(it->first) << " = " << toString(it->second);
+ llvm::errs() << " + ";
+ llvm::errs() << toString(it->second) << "*" << toString(it->first);
}
- llvm::errs() << " }, " << toString(expr.second) << ">\n";
+ llvm::errs() << " + " << toString(expr.second) << "\n";
+
+
+ llvm::errs() << "-" << decl->getNameAsString() << " = ";
+ for (Vector::iterator it = expr.first.begin(),
+ ei = expr.first.end();
+ it != ei;
+ ++it) {
+ if (it != expr.first.begin())
+ llvm::errs() << " + ";
+ llvm::errs() << toString(it->second) << "*" << toString(it->first);
+ }
+ llvm::errs() << " - " << toString(expr.second) << "\n";
}
}
return Result();
}
-Result fromAssignment(const BinaryOperator* op, EqnSys& system) {
- /*EqnExpr* left = fromStmt(op->getLHS()->IgnoreParenCasts(), system);
- EqnExpr* right = fromStmt(op->getRHS()->IgnoreParenCasts(), system);
- Variable<Complete<int> >* var = static_cast<Variable<Complete<int> >*>(left);
-
- std::vector<EqnExpr*> args;
- args.push_back(&system.constant(-infinity<Complete<int> >()));
- args.push_back(right);
- if (system[*var] != NULL)
- args.push_back(system[*var]);
- system[*var] = &system.maxExpression(args);*/
-
+Result fromAssignment(const BinaryOperator* op) {
const Expr* left = op->getLHS()->IgnoreParenCasts();
if (left->getStmtClass() == Stmt::DeclRefExprClass) {
std::string name = static_cast<const DeclRefExpr*>(left)->getNameInfo().getAsString();
- Result expr = fromStmt(op->getRHS()->IgnoreParenCasts(), system);
- llvm::errs() << name << " = <{ ";
+ Result expr = fromStmt(op->getRHS()->IgnoreParenCasts());
+ llvm::errs() << name << " = ";
for (Vector::iterator it = expr.first.begin(),
ei = expr.first.end();
it != ei;
++it) {
if (it != expr.first.begin())
- llvm::errs() << ", ";
- llvm::errs() << toString(it->first) << " = " << toString(it->second);
+ llvm::errs() << " + ";
+ llvm::errs() << toString(it->second) << "*" << toString(it->first);
}
- llvm::errs() << " }, " << toString(expr.second) << ">\n";
+ llvm::errs() << " + " << toString(expr.second) << "\n";
return expr;
}
return Result();
}
-Result fromStmt(const Stmt* stmt, EqnSys& system) {
+Result fromStmt(const Stmt* stmt) {
if (!stmt)
return Result();
+ //stmt->dump();
switch (stmt->getStmtClass()) {
case Stmt::IntegerLiteralClass:
- return fromInteger(static_cast<const IntegerLiteral*>(stmt), system);
+ return fromInteger(static_cast<const IntegerLiteral*>(stmt));
case Stmt::DeclRefExprClass:
- return fromDeclExpr(static_cast<const DeclRefExpr*>(stmt), system);
+ return fromDeclExpr(static_cast<const DeclRefExpr*>(stmt));
case Stmt::UnaryOperatorClass:
- return fromUnary(static_cast<const UnaryOperator*>(stmt), system);
+ return fromUnary(static_cast<const UnaryOperator*>(stmt));
case Stmt::DeclStmtClass:
- return fromDeclStmt(static_cast<const DeclStmt*>(stmt), system);
+ return fromDeclStmt(static_cast<const DeclStmt*>(stmt));
case Stmt::BinaryOperatorClass:
- {
- const BinaryOperator* binop = static_cast<const BinaryOperator*>(stmt);
- if (binop->isAssignmentOp())
- return fromAssignment(binop, system);
- else
- return fromBinary(binop, system);
- }
+ return fromBinary(static_cast<const BinaryOperator*>(stmt));
+ }
+ const Expr* expr = dyn_cast<const Expr>(stmt);
+ if (expr) {
+ const Expr* expr2 = expr->IgnoreParenCasts();
+ if (expr != expr2)
+ return fromStmt(expr2);
}
+ llvm::errs() << "we shouldn't get here...\n";
return Result();
}
-void runOnBlock(std::string id, const CFGBlock* block, EqnSys& system) {
+Condition fromComparison(const BinaryOperator* op) {
+ if (op->isRelationalOp()) {
+ const Expr* left = op->getLHS()->IgnoreParenCasts();
+ const Expr* right = op->getRHS()->IgnoreParenCasts();
+
+ Condition cond;
+ std::string name;
+ int64_t value;
+ if (left->getStmtClass() == Stmt::DeclRefExprClass) {
+ if (right->getStmtClass() == Stmt::IntegerLiteralClass) {
+ name = static_cast<const DeclRefExpr*>(left)->getNameInfo().getAsString();
+ value = *static_cast<const IntegerLiteral*>(right)->getValue().getRawData();
+ switch (op->getOpcode()) {
+ case BO_LT:
+ cond[name] = value - 1;
+ break;
+ case BO_LE:
+ cond[name] = value;
+ break;
+ case BO_GE:
+ cond['-' + name] = -value;
+ break;
+ case BO_GT:
+ cond['-' + name] = -(value + 1);
+ break;
+ }
+ return cond;
+ } else {
+ return Condition();
+ }
+ } else if (right->getStmtClass() == Stmt::DeclRefExprClass) {
+ if (left->getStmtClass() == Stmt::IntegerLiteralClass) {
+ name = static_cast<const DeclRefExpr*>(right)->getNameInfo().getAsString();
+ value = *static_cast<const IntegerLiteral*>(left)->getValue().getRawData();
+ switch (op->getOpcode()) {
+ case BO_LT:
+ cond['-' + name] = -(value + 1);
+ break;
+ case BO_LE:
+ cond['-' + name] = -value;
+ break;
+ case BO_GE:
+ cond[name] = value;
+ break;
+ case BO_GT:
+ cond[name] = value - 1;
+ break;
+ }
+ return cond;
+ } else {
+ return Condition();
+ }
+ }
+ return Condition();
+ }
+ return Condition();
+}
+
+std::map<const CFGBlock*, EqnVar*> seen_blocks;
+EqnVar* runOnBlock(const CFGBlock* block, EqnSys& system) {
+ if (seen_blocks.find(block) != seen_blocks.end())
+ return seen_blocks.find(block)->second;
+
+ std::string id = toString(block->getBlockID());
+ unsigned int counter = 0;
+
+ // detemine equations for this block
+ LinearEquation eqn;
+ EqnVar* var;
+ Result current;
+
+ var = &system.variable(id);
for (CFGBlock::const_iterator it = block->begin(),
ei = block->end();
it != ei;
++it) {
const CFGStmt* cfg_stmt = it->getAs<CFGStmt>();
- Result expr = fromStmt(cfg_stmt->getStmt(), system);
- /*llvm::errs() << "<{ ";
- for (Vector::iterator it = expr.first.begin(),
- ei = expr.first.end();
- it != ei;
- ++it) {
- if (it != expr.first.begin())
- llvm::errs() << ", ";
- llvm::errs() << toString(it->first) << " = " << toString(it->second);
+ const Stmt* stmt = cfg_stmt->getStmt();
+
+ std::string name = "";
+ Result expr;
+ if (stmt->getStmtClass() == Stmt::BinaryOperatorClass) {
+ const BinaryOperator* binop = static_cast<const BinaryOperator*>(stmt);
+ if (binop->isAssignmentOp()) {
+ const Expr* left = binop->getLHS()->IgnoreParenCasts();
+ const Expr* right = binop->getRHS()->IgnoreParenCasts();
+ if (left->getStmtClass() == Stmt::DeclRefExprClass) {
+ name = static_cast<const DeclRefExpr*>(left)->getNameInfo().getAsString();
+ expr = fromStmt(right);
+ }
+ }
+ } else if (stmt->getStmtClass() == Stmt::DeclStmtClass) {
+ stmt->dump();
+ const DeclStmt* decl_stmt = static_cast<const DeclStmt*>(stmt);
+ for (DeclStmt::const_decl_iterator jt = decl_stmt->decl_begin(),
+ ej = decl_stmt->decl_end();
+ jt != ej;
+ ++jt) {
+ if ((*jt)->getKind() == Decl::Var) {
+ const VarDecl* decl = static_cast<const VarDecl*>(*jt);
+ name = decl->getNameAsString();
+ expr = fromStmt(decl->getInit());
+ if (jt+1 != ej) {
+ llvm::errs() << "Only the first declaration in a multi-declaration statement is used.\n";
+ }
+ llvm::errs() << "Name: " << name << "\n";
+ llvm::errs() << toString(expr) << "\n";
+ break; // only take the first one, for now
+ } else {
+ llvm::errs() << (*jt)->getDeclKindName() << "\n";
+ }
+ }
}
- llvm::errs() << "}, " << toString(expr.second) << ">\n";*/
+ if (name == "")
+ continue;
+
+ // by here we expect `name` and `expr` to be set correctly
+
+ bool newBlock = false;
+ for (Vector::const_iterator jt = expr.first.begin(),
+ ej = expr.first.end();
+ jt != ej;
+ ++jt) {
+ // new block if we read from any variable we've already written to
+ newBlock |= (eqn.find(jt->first) != eqn.end());
+ }
+
+ if (newBlock) {
+ EqnVar* lastVar = var;
+ var = &system.variable(id + "-" + toString(++counter));
+
+ // the linear expression
+ std::vector<EqnExpr*> args;
+ args.push_back(lastVar);
+ EqnExpr* expr = &system.expression(new LinearOperator(eqn), args);
+
+ // the max expression
+ std::vector<EqnExpr*> maxArgs;
+ maxArgs.push_back(&system.constant(-infinity<Vector>()));
+ maxArgs.push_back(expr);
+ system[*var] = &system.maxExpression(args);
+ eqn = LinearEquation();
+ }
+
+ eqn[name] = expr;
+ expr.first = expr.first;
+ expr.second = -expr.second;
+ eqn["-"+name] = expr;
}
- fromStmt(block->getTerminatorCondition(), system);
- /*if (terminator.getStmt() != NULL) {
- if (terminator.getStmt()->getStmtClass() == Stmt::IfStmtClass) {
- const IfStmt* if_stmt = static_cast<const IfStmt*>(terminator.getStmt());
- llvm::errs() << "If: \n";
- if_stmt->dump();
+ EqnVar* lastVar = var;
+ var = &system.variable(id + "-" + toString(++counter));
+
+ // the linear expression
+ std::vector<EqnExpr*> args;
+ args.push_back(lastVar);
+ EqnExpr* expr = &system.expression(new LinearOperator(eqn), args);
+
+ // the max expression
+ std::vector<EqnExpr*> maxArgs;
+ maxArgs.push_back(&system.constant(-infinity<Vector>()));
+ maxArgs.push_back(expr);
+ system[*var] = &system.maxExpression(maxArgs);
+
+ // save the last variable we used (the final values from this block)
+ seen_blocks[block] = var;
+
+ // determine predecessor variables/conditions
+ // we have to do this last to prevent an infinite loop situation
+ std::vector<EqnExpr*> preArgs;
+ for (CFGBlock::const_pred_iterator it = block->pred_begin(),
+ ei = block->pred_end();
+ it != ei;
+ ++it) {
+ if ((*it)->getTerminatorCondition()) {
+ const BinaryOperator* binop = static_cast<const BinaryOperator*>((*it)->getTerminatorCondition());
+ std::vector<EqnExpr*> args;
+ args.push_back(&system.constant(fromComparison(binop)));
+ args.push_back(runOnBlock(*it, system));
+ preArgs.push_back(&system.expression(new Minimum<Vector>(), args));
} else {
- llvm::errs() << "\n";
- terminator.getStmt()->dump();
+ preArgs.push_back(runOnBlock(*it, system));
}
- }*/
- return; // TODO: return a generated expression
+ }
+ EqnVar* preVar = &system.variable(id);
+ if (preArgs.empty())
+ preArgs.push_back(&system.constant(infinity<Vector>()));
+ system[*preVar] = &system.maxExpression(preArgs);
+
+ // return the final value we used
+ return var;
}
void IntervalAnalysis::runOnAllBlocks() {
@@ -324,16 +659,16 @@ void IntervalAnalysis::runOnAllBlocks() {
todo.pop_front();
continue;
}
- llvm::errs() << (void*)block << "\n";
+ llvm::errs() << block->getBlockID() << "\n";
seen.insert(block);
todo.pop_front();
- runOnBlock(toString(block), block, system);
+ runOnBlock(block, system);
llvm::errs() << "-> ";
for (CFGBlock::const_succ_iterator it = block->succ_begin(),
ei = block->succ_end();
it != ei;
it++ ) {
- llvm::errs() << (void*) *it << ", ";
+ llvm::errs() << (*it)->getBlockID() << ", ";
todo.push_back(*it);
}
llvm::errs() << "\n\n";
@@ -344,12 +679,12 @@ void IntervalAnalysis::runOnAllBlocks() {
llvm::errs() << toString(system) << "\n";
system.indexMaxExpressions();
- DynamicMaxStrategy<Complete<int> > strategy(system);
- DynamicVariableAssignment<Complete<int> > rho(system, strategy);
+ DynamicMaxStrategy<Vector> strategy(system);
+ DynamicVariableAssignment<Vector> rho(system, strategy);
strategy.setRho(rho);
for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) {
- Variable<Complete<int> >& var = system.variable(i);
+ Variable<Vector>& var = system.variable(i);
llvm::errs() << toString(var.name()) << " = " << toString(rho[var]) << "\n";
}
diff --git a/clang/lib/StaticAnalyzer/Core/IntervalConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/IntervalConstraintManager.cpp
new file mode 100644
index 0000000..9d04720
--- /dev/null
+++ b/clang/lib/StaticAnalyzer/Core/IntervalConstraintManager.cpp
@@ -0,0 +1,442 @@
+//== IntervalConstraintManager.cpp - Manage range constraints.------*- C++ -*--==//
+//
+// The LLVM Compiler Infrastructure
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+//
+// This file defines IntervalConstraintManager, a class that tracks simple
+// equality and inequality constraints on symbolic values of ProgramState.
+//
+//===----------------------------------------------------------------------===//
+
+#include "SimpleConstraintManager.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h"
+#include "llvm/Support/Debug.h"
+#include "llvm/ADT/FoldingSet.h"
+#include "llvm/ADT/ImmutableSet.h"
+#include "llvm/Support/raw_ostream.h"
+
+using namespace clang;
+using namespace ento;
+
+namespace { class ConstraintRange {}; }
+static int ConstraintRangeIndex = 0;
+
+/// A Range represents the closed range [from, to]. The caller must
+/// guarantee that from <= to. Note that Range is immutable, so as not
+/// to subvert RangeSet's immutability.
+namespace {
+class Range : public std::pair<const llvm::APSInt*,
+ const llvm::APSInt*> {
+public:
+ Range(const llvm::APSInt &from, const llvm::APSInt &to)
+ : std::pair<const llvm::APSInt*, const llvm::APSInt*>(&from, &to) {
+ assert(from <= to);
+ }
+ bool Includes(const llvm::APSInt &v) const {
+ return *first <= v && v <= *second;
+ }
+ const llvm::APSInt &From() const {
+ return *first;
+ }
+ const llvm::APSInt &To() const {
+ return *second;
+ }
+ const llvm::APSInt *getConcreteValue() const {
+ return &From() == &To() ? &From() : NULL;
+ }
+
+ void Profile(llvm::FoldingSetNodeID &ID) const {
+ ID.AddPointer(&From());
+ ID.AddPointer(&To());
+ }
+};
+
+
+class RangeTrait : public llvm::ImutContainerInfo<Range> {
+public:
+ // When comparing if one Range is less than another, we should compare
+ // the actual APSInt values instead of their pointers. This keeps the order
+ // consistent (instead of comparing by pointer values) and can potentially
+ // be used to speed up some of the operations in RangeSet.
+ static inline bool isLess(key_type_ref lhs, key_type_ref rhs) {
+ return *lhs.first < *rhs.first || (!(*rhs.first < *lhs.first) &&
+ *lhs.second < *rhs.second);
+ }
+};
+
+/// RangeSet contains a set of ranges. If the set is empty, then
+/// there the value of a symbol is overly constrained and there are no
+/// possible values for that symbol.
+class RangeSet {
+ typedef llvm::ImmutableSet<Range, RangeTrait> PrimRangeSet;
+ PrimRangeSet ranges; // no need to make const, since it is an
+ // ImmutableSet - this allows default operator=
+ // to work.
+public:
+ typedef PrimRangeSet::Factory Factory;
+ typedef PrimRangeSet::iterator iterator;
+
+ RangeSet(PrimRangeSet RS) : ranges(RS) {}
+
+ iterator begin() const { return ranges.begin(); }
+ iterator end() const { return ranges.end(); }
+
+ bool isEmpty() const { return ranges.isEmpty(); }
+
+ /// Construct a new RangeSet representing '{ [from, to] }'.
+ RangeSet(Factory &F, const llvm::APSInt &from, const llvm::APSInt &to)
+ : ranges(F.add(F.getEmptySet(), Range(from, to))) {}
+
+ /// Profile - Generates a hash profile of this RangeSet for use
+ /// by FoldingSet.
+ void Profile(llvm::FoldingSetNodeID &ID) const { ranges.Profile(ID); }
+
+ /// getConcreteValue - If a symbol is contrained to equal a specific integer
+ /// constant then this method returns that value. Otherwise, it returns
+ /// NULL.
+ const llvm::APSInt* getConcreteValue() const {
+ return ranges.isSingleton() ? ranges.begin()->getConcreteValue() : 0;
+ }
+
+private:
+ void IntersectInRange(BasicValueFactory &BV, Factory &F,
+ const llvm::APSInt &Lower,
+ const llvm::APSInt &Upper,
+ PrimRangeSet &newRanges,
+ PrimRangeSet::iterator &i,
+ PrimRangeSet::iterator &e) const {
+ // There are six cases for each range R in the set:
+ // 1. R is entirely before the intersection range.
+ // 2. R is entirely after the intersection range.
+ // 3. R contains the entire intersection range.
+ // 4. R starts before the intersection range and ends in the middle.
+ // 5. R starts in the middle of the intersection range and ends after it.
+ // 6. R is entirely contained in the intersection range.
+ // These correspond to each of the conditions below.
+ for (/* i = begin(), e = end() */; i != e; ++i) {
+ if (i->To() < Lower) {
+ continue;
+ }
+ if (i->From() > Upper) {
+ break;
+ }
+
+ if (i->Includes(Lower)) {
+ if (i->Includes(Upper)) {
+ newRanges = F.add(newRanges, Range(BV.getValue(Lower),
+ BV.getValue(Upper)));
+ break;
+ } else
+ newRanges = F.add(newRanges, Range(BV.getValue(Lower), i->To()));
+ } else {
+ if (i->Includes(Upper)) {
+ newRanges = F.add(newRanges, Range(i->From(), BV.getValue(Upper)));
+ break;
+ } else
+ newRanges = F.add(newRanges, *i);
+ }
+ }
+ }
+
+public:
+ // Returns a set containing the values in the receiving set, intersected with
+ // the closed range [Lower, Upper]. Unlike the Range type, this range uses
+ // modular arithmetic, corresponding to the common treatment of C integer
+ // overflow. Thus, if the Lower bound is greater than the Upper bound, the
+ // range is taken to wrap around. This is equivalent to taking the
+ // intersection with the two ranges [Min, Upper] and [Lower, Max],
+ // or, alternatively, /removing/ all integers between Upper and Lower.
+ RangeSet Intersect(BasicValueFactory &BV, Factory &F,
+ const llvm::APSInt &Lower,
+ const llvm::APSInt &Upper) const {
+ PrimRangeSet newRanges = F.getEmptySet();
+
+ PrimRangeSet::iterator i = begin(), e = end();
+ if (Lower <= Upper)
+ IntersectInRange(BV, F, Lower, Upper, newRanges, i, e);
+ else {
+ // The order of the next two statements is important!
+ // IntersectInRange() does not reset the iteration state for i and e.
+ // Therefore, the lower range most be handled first.
+ IntersectInRange(BV, F, BV.getMinValue(Upper), Upper, newRanges, i, e);
+ IntersectInRange(BV, F, Lower, BV.getMaxValue(Lower), newRanges, i, e);
+ }
+ return newRanges;
+ }
+
+ void print(raw_ostream &os) const {
+ bool isFirst = true;
+ os << "{ ";
+ for (iterator i = begin(), e = end(); i != e; ++i) {
+ if (isFirst)
+ isFirst = false;
+ else
+ os << ", ";
+
+ os << '[' << i->From().toString(10) << ", " << i->To().toString(10)
+ << ']';
+ }
+ os << " }";
+ }
+
+ bool operator==(const RangeSet &other) const {
+ return ranges == other.ranges;
+ }
+};
+} // end anonymous namespace
+
+typedef llvm::ImmutableMap<SymbolRef,RangeSet> ConstraintRangeTy;
+
+namespace clang {
+namespace ento {
+template<>
+struct ProgramStateTrait<ConstraintRange>
+ : public ProgramStatePartialTrait<ConstraintRangeTy> {
+ static inline void *GDMIndex() { return &ConstraintRangeIndex; }
+};
+}
+}
+
+namespace {
+class IntervalConstraintManager : public SimpleConstraintManager{
+ RangeSet GetRange(ProgramStateRef state, SymbolRef sym);
+public:
+ IntervalConstraintManager(SubEngine &subengine)
+ : SimpleConstraintManager(subengine) {}
+
+ ProgramStateRef assumeSymNE(ProgramStateRef state, SymbolRef sym,
+ const llvm::APSInt& Int,
+ const llvm::APSInt& Adjustment);
+
+ ProgramStateRef assumeSymEQ(ProgramStateRef state, SymbolRef sym,
+ const llvm::APSInt& Int,
+ const llvm::APSInt& Adjustment);
+
+ ProgramStateRef assumeSymLT(ProgramStateRef state, SymbolRef sym,
+ const llvm::APSInt& Int,
+ const llvm::APSInt& Adjustment);
+
+ ProgramStateRef assumeSymGT(ProgramStateRef state, SymbolRef sym,
+ const llvm::APSInt& Int,
+ const llvm::APSInt& Adjustment);
+
+ ProgramStateRef assumeSymGE(ProgramStateRef state, SymbolRef sym,
+ const llvm::APSInt& Int,
+ const llvm::APSInt& Adjustment);
+
+ ProgramStateRef assumeSymLE(ProgramStateRef state, SymbolRef sym,
+ const llvm::APSInt& Int,
+ const llvm::APSInt& Adjustment);
+
+ const llvm::APSInt* getSymVal(ProgramStateRef St, SymbolRef sym) const;
+
+ // FIXME: Refactor into SimpleConstraintManager?
+ bool isEqual(ProgramStateRef St, SymbolRef sym, const llvm::APSInt& V) const {
+ const llvm::APSInt *i = getSymVal(St, sym);
+ return i ? *i == V : false;
+ }
+
+ ProgramStateRef removeDeadBindings(ProgramStateRef St, SymbolReaper& SymReaper);
+
+ void print(ProgramStateRef St, raw_ostream &Out,
+ const char* nl, const char *sep);
+
+private:
+ RangeSet::Factory F;
+};
+
+} // end anonymous namespace
+
+ConstraintManager* ento::CreateIntervalConstraintManager(ProgramStateManager&,
+ SubEngine &subeng) {
+ return new IntervalConstraintManager(subeng);
+}
+
+const llvm::APSInt* IntervalConstraintManager::getSymVal(ProgramStateRef St,
+ SymbolRef sym) const {
+ const ConstraintRangeTy::data_type *T = St->get<ConstraintRange>(sym);
+ return T ? T->getConcreteValue() : NULL;
+}
+
+/// Scan all symbols referenced by the constraints. If the symbol is not alive
+/// as marked in LSymbols, mark it as dead in DSymbols.
+ProgramStateRef
+IntervalConstraintManager::removeDeadBindings(ProgramStateRef state,
+ SymbolReaper& SymReaper) {
+
+ ConstraintRangeTy CR = state->get<ConstraintRange>();
+ ConstraintRangeTy::Factory& CRFactory = state->get_context<ConstraintRange>();
+
+ for (ConstraintRangeTy::iterator I = CR.begin(), E = CR.end(); I != E; ++I) {
+ SymbolRef sym = I.getKey();
+ if (SymReaper.maybeDead(sym))
+ CR = CRFactory.remove(CR, sym);
+ }
+
+ return state->set<ConstraintRange>(CR);
+}
+
+RangeSet
+IntervalConstraintManager::GetRange(ProgramStateRef state, SymbolRef sym) {
+ if (ConstraintRangeTy::data_type* V = state->get<ConstraintRange>(sym))
+ return *V;
+
+ // Lazily generate a new RangeSet representing all possible values for the
+ // given symbol type.
+ QualType T = state->getSymbolManager().getType(sym);
+ BasicValueFactory& BV = state->getBasicVals();
+ return RangeSet(F, BV.getMinValue(T), BV.getMaxValue(T));
+}
+
+//===------------------------------------------------------------------------===
+// assumeSymX methods: public interface for IntervalConstraintManager.
+//===------------------------------------------------------------------------===/
+
+// The syntax for ranges below is mathematical, using [x, y] for closed ranges
+// and (x, y) for open ranges. These ranges are modular, corresponding with
+// a common treatment of C integer overflow. This means that these methods
+// do not have to worry about overflow; RangeSet::Intersect can handle such a
+// "wraparound" range.
+// As an example, the range [UINT_MAX-1, 3) contains five values: UINT_MAX-1,
+// UINT_MAX, 0, 1, and 2.
+
+ProgramStateRef
+IntervalConstraintManager::assumeSymNE(ProgramStateRef state, SymbolRef sym,
+ const llvm::APSInt& Int,
+ const llvm::APSInt& Adjustment) {
+ BasicValueFactory &BV = state->getBasicVals();
+
+ llvm::APSInt Lower = Int-Adjustment;
+ llvm::APSInt Upper = Lower;
+ --Lower;
+ ++Upper;
+
+ // [Int-Adjustment+1, Int-Adjustment-1]
+ // Notice that the lower bound is greater than the upper bound.
+ RangeSet New = GetRange(state, sym).Intersect(BV, F, Upper, Lower);
+ return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
+}
+
+ProgramStateRef
+IntervalConstraintManager::assumeSymEQ(ProgramStateRef state, SymbolRef sym,
+ const llvm::APSInt& Int,
+ const llvm::APSInt& Adjustment) {
+ // [Int-Adjustment, Int-Adjustment]
+ BasicValueFactory &BV = state->getBasicVals();
+ llvm::APSInt AdjInt = Int-Adjustment;
+ RangeSet New = GetRange(state, sym).Intersect(BV, F, AdjInt, AdjInt);
+ return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
+}
+
+ProgramStateRef
+IntervalConstraintManager::assumeSymLT(ProgramStateRef state, SymbolRef sym,
+ const llvm::APSInt& Int,
+ const llvm::APSInt& Adjustment) {
+ BasicValueFactory &BV = state->getBasicVals();
+
+ QualType T = state->getSymbolManager().getType(sym);
+ const llvm::APSInt &Min = BV.getMinValue(T);
+
+ // Special case for Int == Min. This is always false.
+ if (Int == Min)
+ return NULL;
+
+ llvm::APSInt Lower = Min-Adjustment;
+ llvm::APSInt Upper = Int-Adjustment;
+ --Upper;
+
+ RangeSet New = GetRange(state, sym).Intersect(BV, F, Lower, Upper);
+ return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
+}
+
+ProgramStateRef
+IntervalConstraintManager::assumeSymGT(ProgramStateRef state, SymbolRef sym,
+ const llvm::APSInt& Int,
+ const llvm::APSInt& Adjustment) {
+ BasicValueFactory &BV = state->getBasicVals();
+
+ QualType T = state->getSymbolManager().getType(sym);
+ const llvm::APSInt &Max = BV.getMaxValue(T);
+
+ // Special case for Int == Max. This is always false.
+ if (Int == Max)
+ return NULL;
+
+ llvm::APSInt Lower = Int-Adjustment;
+ llvm::APSInt Upper = Max-Adjustment;
+ ++Lower;
+
+ RangeSet New = GetRange(state, sym).Intersect(BV, F, Lower, Upper);
+ return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
+}
+
+ProgramStateRef
+IntervalConstraintManager::assumeSymGE(ProgramStateRef state, SymbolRef sym,
+ const llvm::APSInt& Int,
+ const llvm::APSInt& Adjustment) {
+ BasicValueFactory &BV = state->getBasicVals();
+
+ QualType T = state->getSymbolManager().getType(sym);
+ const llvm::APSInt &Min = BV.getMinValue(T);
+
+ // Special case for Int == Min. This is always feasible.
+ if (Int == Min)
+ return state;
+
+ const llvm::APSInt &Max = BV.getMaxValue(T);
+
+ llvm::APSInt Lower = Int-Adjustment;
+ llvm::APSInt Upper = Max-Adjustment;
+
+ RangeSet New = GetRange(state, sym).Intersect(BV, F, Lower, Upper);
+ return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
+}
+
+ProgramStateRef
+IntervalConstraintManager::assumeSymLE(ProgramStateRef state, SymbolRef sym,
+ const llvm::APSInt& Int,
+ const llvm::APSInt& Adjustment) {
+ BasicValueFactory &BV = state->getBasicVals();
+
+ QualType T = state->getSymbolManager().getType(sym);
+ const llvm::APSInt &Max = BV.getMaxValue(T);
+
+ // Special case for Int == Max. This is always feasible.
+ if (Int == Max)
+ return state;
+
+ const llvm::APSInt &Min = BV.getMinValue(T);
+
+ llvm::APSInt Lower = Min-Adjustment;
+ llvm::APSInt Upper = Int-Adjustment;
+
+ RangeSet New = GetRange(state, sym).Intersect(BV, F, Lower, Upper);
+ return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
+}
+
+//===------------------------------------------------------------------------===
+// Pretty-printing.
+//===------------------------------------------------------------------------===/
+
+void IntervalConstraintManager::print(ProgramStateRef St, raw_ostream &Out,
+ const char* nl, const char *sep) {
+
+ ConstraintRangeTy Ranges = St->get<ConstraintRange>();
+
+ if (Ranges.isEmpty()) {
+ Out << nl << sep << "Ranges are empty." << nl;
+ return;
+ }
+
+ Out << nl << sep << "Ranges of symbol values:";
+ for (ConstraintRangeTy::iterator I=Ranges.begin(), E=Ranges.end(); I!=E; ++I){
+ Out << nl << ' ' << I.getKey() << " : ";
+ I.getData().print(Out);
+ }
+ Out << nl;
+}