From 684045e9e843ed9b8be30728482ce3d69d63b527 Mon Sep 17 00:00:00 2001 From: "Zancanaro; Carlo" Date: Thu, 4 Oct 2012 17:11:33 +1000 Subject: 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. --- clang/lib/Analysis/.#Interval.cpp | 1 - clang/lib/Analysis/.#Interval_flymake.cpp | 1 - clang/lib/Analysis/Interval.cpp | 535 +++++++++++++++++---- .../Core/IntervalConstraintManager.cpp | 442 +++++++++++++++++ 4 files changed, 877 insertions(+), 102 deletions(-) delete mode 120000 clang/lib/Analysis/.#Interval.cpp delete mode 120000 clang/lib/Analysis/.#Interval_flymake.cpp create mode 100644 clang/lib/StaticAnalyzer/Core/IntervalConstraintManager.cpp (limited to 'clang/lib') 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 #include #include +#include using namespace clang; -typedef EquationSystem > EqnSys; -typedef Expression > EqnExpr; - #include template std::string toString(const T& obj) { @@ -31,6 +29,28 @@ std::string toString(const T& obj) { return stream.str(); } +#include +template +std::ostream& operator<<(std::ostream& cout, const std::pair& v) { + cout << "(" << v.first << ", " << v.second << ")"; + return cout; +} + +template +std::ostream& operator<<(std::ostream& cout, const std::map& v) { + cout << "{"; + for (typename std::map::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 ZBar; -typedef std::map Vector; +//typedef std::map Vector; + +struct Vector : public std::map { + Vector(const ZBar& val=infinity()) + : _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 p = this->insert(std::pair(key, _val)); + return p.first->second; + } + ZBar _val; +}; + typedef std::pair Result; // a "slice" of an equation +//typedef std::map LinearEquation; // one `Result` per variable +struct LinearEquation : public std::map { + 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 p = this->insert(std::pair(key, r)); + return p.first->second; + } +}; + +typedef Vector Condition; + +typedef EquationSystem EqnSys; +typedef Expression EqnExpr; +typedef Variable EqnVar; + + +struct LinearOperator : public Operator { + LinearOperator(const LinearEquation& result) + : _values(result) {} + + Vector eval(const std::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 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, l, r); +} +template +T max(const T& l, const T& r) { + return (l < r ? l : r); +} template T negate(const T& v) { return -v; @@ -98,25 +206,90 @@ template T addValues(const T& l, const T& r) { return l + r; } -template -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, left, right); +} + +Vector operator-(const Vector& left, const Vector& right) { + return merge_maps_with(addValues, 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() { + return Vector(infinity()); +} + +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 >* add = new Addition >(); -Subtraction >* sub = new Subtraction >(); -Multiplication >* mul = new Multiplication >(); - -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, 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(*it); - Variable > var = system.variable(decl->getNameAsString()); - std::vector args; - args.push_back(&system.constant(-infinity >())); - 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(*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 >* var = static_cast >*>(left); - - std::vector args; - args.push_back(&system.constant(-infinity >())); - 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(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(stmt), system); + return fromInteger(static_cast(stmt)); case Stmt::DeclRefExprClass: - return fromDeclExpr(static_cast(stmt), system); + return fromDeclExpr(static_cast(stmt)); case Stmt::UnaryOperatorClass: - return fromUnary(static_cast(stmt), system); + return fromUnary(static_cast(stmt)); case Stmt::DeclStmtClass: - return fromDeclStmt(static_cast(stmt), system); + return fromDeclStmt(static_cast(stmt)); case Stmt::BinaryOperatorClass: - { - const BinaryOperator* binop = static_cast(stmt); - if (binop->isAssignmentOp()) - return fromAssignment(binop, system); - else - return fromBinary(binop, system); - } + return fromBinary(static_cast(stmt)); + } + const Expr* expr = dyn_cast(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(left)->getNameInfo().getAsString(); + value = *static_cast(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(right)->getNameInfo().getAsString(); + value = *static_cast(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 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(); - 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(stmt); + if (binop->isAssignmentOp()) { + const Expr* left = binop->getLHS()->IgnoreParenCasts(); + const Expr* right = binop->getRHS()->IgnoreParenCasts(); + if (left->getStmtClass() == Stmt::DeclRefExprClass) { + name = static_cast(left)->getNameInfo().getAsString(); + expr = fromStmt(right); + } + } + } else if (stmt->getStmtClass() == Stmt::DeclStmtClass) { + stmt->dump(); + const DeclStmt* decl_stmt = static_cast(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(*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 args; + args.push_back(lastVar); + EqnExpr* expr = &system.expression(new LinearOperator(eqn), args); + + // the max expression + std::vector maxArgs; + maxArgs.push_back(&system.constant(-infinity())); + 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(terminator.getStmt()); - llvm::errs() << "If: \n"; - if_stmt->dump(); + EqnVar* lastVar = var; + var = &system.variable(id + "-" + toString(++counter)); + + // the linear expression + std::vector args; + args.push_back(lastVar); + EqnExpr* expr = &system.expression(new LinearOperator(eqn), args); + + // the max expression + std::vector maxArgs; + maxArgs.push_back(&system.constant(-infinity())); + 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 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((*it)->getTerminatorCondition()); + std::vector args; + args.push_back(&system.constant(fromComparison(binop))); + args.push_back(runOnBlock(*it, system)); + preArgs.push_back(&system.expression(new Minimum(), 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())); + 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 > strategy(system); - DynamicVariableAssignment > rho(system, strategy); + DynamicMaxStrategy strategy(system); + DynamicVariableAssignment rho(system, strategy); strategy.setRho(rho); for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) { - Variable >& var = system.variable(i); + Variable& 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 { +public: + Range(const llvm::APSInt &from, const llvm::APSInt &to) + : std::pair(&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 { +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 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 ConstraintRangeTy; + +namespace clang { +namespace ento { +template<> +struct ProgramStateTrait + : public ProgramStatePartialTrait { + 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(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(); + ConstraintRangeTy::Factory& CRFactory = state->get_context(); + + 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(CR); +} + +RangeSet +IntervalConstraintManager::GetRange(ProgramStateRef state, SymbolRef sym) { + if (ConstraintRangeTy::data_type* V = state->get(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(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(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(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(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(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(sym, New); +} + +//===------------------------------------------------------------------------=== +// Pretty-printing. +//===------------------------------------------------------------------------===/ + +void IntervalConstraintManager::print(ProgramStateRef St, raw_ostream &Out, + const char* nl, const char *sep) { + + ConstraintRangeTy Ranges = St->get(); + + 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; +} -- cgit v1.2.3