From f1bd2e48c5324d3f7cda4090c87f8a5b6f463ce2 Mon Sep 17 00:00:00 2001 From: "Zancanaro; Carlo" Date: Mon, 15 Oct 2012 17:08:15 +1100 Subject: Fix up the Equation System generation. Now there's a bug in the solver. The solver seems to work fine when run as a tool by itself, but not in the clang stuff. Very annoying. --- TODO.org | 55 -- .../Analysis/Analyses/IntervalSolver/Complete.hpp | 5 +- .../Analyses/IntervalSolver/Expression.hpp | 20 +- .../Analyses/IntervalSolver/MaxStrategy.hpp | 7 +- .../Analyses/IntervalSolver/VariableAssignment.hpp | 12 +- clang/lib/Analysis/CMakeLists.txt | 5 +- clang/lib/Analysis/Interval.cpp | 568 +++++++++++---------- .../Checkers/.#ArrayBoundCheckerV2_flymake.cpp | 1 - clang/lib/StaticAnalyzer/Checkers/.#Checkers.td | 1 - clang/lib/StaticAnalyzer/Checkers/Checkers.td | 2 +- .../Core/IntervalConstraintManager.cpp | 27 +- 11 files changed, 364 insertions(+), 339 deletions(-) delete mode 100644 TODO.org delete mode 120000 clang/lib/StaticAnalyzer/Checkers/.#ArrayBoundCheckerV2_flymake.cpp delete mode 120000 clang/lib/StaticAnalyzer/Checkers/.#Checkers.td diff --git a/TODO.org b/TODO.org deleted file mode 100644 index f59cf4b..0000000 --- a/TODO.org +++ /dev/null @@ -1,55 +0,0 @@ -* TODO Refactoring [1/4] -- [X] Fix up logging -- [ ] Separate classes into files -- [ ] Put outer-loop in a class (out of main) -- [ ] Give EquationSystem methods for creating assignments/strategies -* TODO Verbosity [2/3] -- [X] Wrap output streams [5/5] - - [X] strategies - - [X] fixpoint - - [X] debug - - [X] trace - - [X] info -- [X] Command-line arguments [5/5] - - [X] strategies - - [X] fixpoint - - [X] debug - - [X] trace - - [X] info -- [-] Provide output [0/5] - - [-] strategies [1/2] - - [ ] print the system and assignment, then the next strategy - - [X] print each strategy like this: - max(0, x, sub(y,2)) --[2]-> sub(y,2) - - [ ] fixpoint - print the system we're working with, then print the resultant assignment - - [ ] debug - print the initial system we're working with - print more general info in the main loop (number of loops, each assignment/strategy) - - [ ] trace - maybe we don't need this - would be something like "entering/exiting" everything mildly important - - [ ] info - print the initial system we're working with -* TODO make test [2/3] -- [-] write test cases [1/4] - - [X] examples from paper - - [ ] best cases - - [ ] worst cases - - [ ] average cases -- [X] write a script to run over each test case and return pass/fail -- [X] consolidate into makefile as `make test` -* TODO Min-cost flow problem [1/3] -- [X] Research min-cost flow libraries - Potentially just use LEMON? It looks pretty decent. - LEMON it is! -- [ ] Implement the min-cost flow operator MCF - It takes four construction-time arguments and one run-time argument. - Construction time: - - T (the template constraint matrix) - - A (the multiplicative modification factor) - - b (the additive modification factor) - - c (the bound in the guard) - Run-time: - - d (the abstract value to be operated on) -- [ ] Update test cases to include MCF diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/Complete.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/Complete.hpp index 5219c9e..9acb9d0 100644 --- a/clang/include/clang/Analysis/Analyses/IntervalSolver/Complete.hpp +++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/Complete.hpp @@ -15,10 +15,7 @@ struct Complete { : _value(value), _infinity(false) { } Complete(const T& value, const bool& infinity) : _value(value), _infinity(infinity) { - if (value == 0 && infinity == true) { - std::cout << "throw exception" << *(char*)NULL; - //throw "Zero infinity? Die die die!"; - } + assert(value != 0 || infinity == false); } Complete(const Complete& other) : _value(other._value), _infinity(other._infinity) { } diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/Expression.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/Expression.hpp index c4ee4c0..ac9b052 100644 --- a/clang/include/clang/Analysis/Analyses/IntervalSolver/Expression.hpp +++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/Expression.hpp @@ -28,7 +28,7 @@ struct Expression { } virtual Domain eval(const VariableAssignment&) const = 0; - virtual Domain eval(const VariableAssignment& rho, + virtual Domain evalWithStrat(const VariableAssignment& rho, const MaxStrategy&) const { return eval(rho); } @@ -98,16 +98,20 @@ struct OperatorExpression : public Expression { return _operator.eval(argumentValues); } - virtual Domain eval(const VariableAssignment& rho, const MaxStrategy& strat) const { + virtual Domain evalWithStrat(const VariableAssignment& rho, const MaxStrategy& strat) const { std::vector argumentValues; for (typename std::vector*>::const_iterator it = _arguments.begin(); it != _arguments.end(); ++it) { - argumentValues.push_back((*it)->eval(rho, strat)); + argumentValues.push_back((*it)->evalWithStrat(rho, strat)); } return _operator.eval(argumentValues); } + std::vector*>& arguments() { + return _arguments; + } + const std::vector*>& arguments() const { return _arguments; } @@ -139,7 +143,7 @@ struct OperatorExpression : public Expression { private: const Operator& _operator; protected: - const std::vector*> _arguments; + std::vector*> _arguments; }; template @@ -151,18 +155,18 @@ struct MaxExpression : public OperatorExpression { return this; } - virtual Domain eval(const VariableAssignment& rho, const MaxStrategy& strat) const { - return this->_arguments[strat.get(*this)]->eval(rho, strat); + virtual Domain evalWithStrat(const VariableAssignment& rho, const MaxStrategy& strat) const { + return this->_arguments[strat.get(*this)]->evalWithStrat(rho, strat); } unsigned int bestStrategy(const VariableAssignment& rho, const MaxStrategy& strat) const { - Domain bestValue = this->eval(rho, strat); + Domain bestValue = this->evalWithStrat(rho, strat); unsigned int bestIndex = strat.get(*this); for (unsigned int i = 0, length = this->_arguments.size(); i < length; ++i) { - const Domain value = this->_arguments[i]->eval(rho, strat); + const Domain value = this->_arguments[i]->evalWithStrat(rho, strat); if (bestValue < value) { bestValue = value; bestIndex = i; diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/MaxStrategy.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/MaxStrategy.hpp index f5cb0d8..57dcdeb 100644 --- a/clang/include/clang/Analysis/Analyses/IntervalSolver/MaxStrategy.hpp +++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/MaxStrategy.hpp @@ -54,9 +54,12 @@ struct DynamicMaxStrategy : public MaxStrategy { solver_log::strategy << indent() << "Invalidating " << v << " - " << *_system[v] << std::endl; _stable.filter(_var_influence[v]); + IdSet > infl = _var_influence[v]; + _var_influence[v].clear(); + for (typename IdSet >::iterator - it = _var_influence[v].begin(), - end = _var_influence[v].end(); + it = infl.begin(), + end = infl.end(); it != end; ++it) { solve(_system.maxExpression(*it)); diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp index 0bbebfc..ba5f650 100644 --- a/clang/include/clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp +++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp @@ -35,8 +35,12 @@ struct DynamicVariableAssignment : public VariableAssignment { void invalidate(const Variable& x) const { solver_log::fixpoint << indent() << "Invalidating " << x << std::endl; - _stable.remove(x); - _values[x] = infinity(); + if (_stable.contains(x)) { + _stable.remove(x); + _values[x] = infinity(); + + solve(x); + } } private: @@ -49,8 +53,8 @@ private: stack_depth++; if (!_system[x]) return; - Domain val = _system[x]->eval(DependencyAssignment(*this, x), - _strategy); + Domain val = _system[x]->evalWithStrat(DependencyAssignment(*this, x), + _strategy); stack_depth--; if (val != _values[x]) { diff --git a/clang/lib/Analysis/CMakeLists.txt b/clang/lib/Analysis/CMakeLists.txt index bede002..3d2251e 100644 --- a/clang/lib/Analysis/CMakeLists.txt +++ b/clang/lib/Analysis/CMakeLists.txt @@ -21,5 +21,8 @@ add_clang_library(clangAnalysis UninitializedValues.cpp ) +add_library(lib_lemon IMPORTED emon) + add_dependencies(clangAnalysis ClangAttrClasses ClangAttrList - ClangDiagnosticAnalysis ClangDeclNodes ClangStmtNodes) + ClangDiagnosticAnalysis ClangDeclNodes ClangStmtNodes + lib_lemon) diff --git a/clang/lib/Analysis/Interval.cpp b/clang/lib/Analysis/Interval.cpp index 96dd841..ac96107 100644 --- a/clang/lib/Analysis/Interval.cpp +++ b/clang/lib/Analysis/Interval.cpp @@ -21,6 +21,12 @@ using namespace clang; +std::string negate_string(const std::string& str) { + if (str[0] == '-') + return str.substr(1); + return '-' + str; +} + #include template std::string toString(const T& obj) { @@ -36,6 +42,20 @@ std::ostream& operator<<(std::ostream& cout, const std::pair& v) { return cout; } +template +std::ostream& operator<<(std::ostream& cout, const std::vector& v) { + cout << "["; + for(typename std::vector::const_iterator it = v.begin(), ei = v.end(); + it != ei; + ++it) { + if (it != v.begin()) + cout << ", "; + cout << *it; + } + cout << "]"; + return cout; +} + template std::ostream& operator<<(std::ostream& cout, const std::map& v) { cout << "{"; @@ -50,14 +70,6 @@ std::ostream& operator<<(std::ostream& cout, const std::map& v) { return cout; } - -IntervalAnalysis :: IntervalAnalysis(AnalysisDeclContext &context) - : context(&context) { -} - -IntervalAnalysis :: ~IntervalAnalysis() { -} - // Two pieces of state: // -> condition protecting a node // -> node's expression itself @@ -68,10 +80,14 @@ IntervalAnalysis :: ~IntervalAnalysis() { // Hooray! typedef Complete ZBar; +template<> +ZBar infinity() { + return ZBar(1, true); +} //typedef std::map Vector; struct Vector : public std::map { - Vector(const ZBar& val=infinity()) + Vector(const ZBar& val=0) : _val(val) { } ZBar operator[](const std::string& key) const { if (this->find(key) != this->end()) @@ -87,8 +103,23 @@ struct Vector : public std::map { ZBar _val; }; +Vector negate_vector(const Vector& v) { + Vector result; + for (Vector::const_iterator it = v.begin(), + ei = v.end(); + it != ei; + ++it) { + result[negate_string(it->first)] = it->second; + } + return result; +} + typedef std::pair Result; // a "slice" of an equation +Result negate_result(const Result& r) { + return Result(negate_vector(r.first), -r.second); +} + //typedef std::map LinearEquation; // one `Result` per variable struct LinearEquation : public std::map { Result operator[](const std::string& key) const { @@ -112,21 +143,21 @@ struct LinearEquation : public std::map { typedef Vector Condition; -typedef EquationSystem EqnSys; -typedef Expression EqnExpr; -typedef Variable EqnVar; +typedef EquationSystem EqnSys; +typedef Expression EqnExpr; +typedef Variable EqnVar; struct LinearOperator : public Operator { - LinearOperator(const LinearEquation& result) + 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(); + for (LinearEquation::const_iterator it = _values->begin(), + ei = _values->end(); it != ei; ++it) { ZBar subresult = 0; @@ -143,10 +174,10 @@ struct LinearOperator : public Operator { } void print(std::ostream& cout) const { - cout << "linear[" << _values << "]"; + cout << "linear[" << *_values << "]"; } - LinearEquation _values; + const LinearEquation* _values; }; @@ -192,6 +223,7 @@ M merge_maps_with(const F& f, const M& left, const M& right) { template<> Vector minimum(const Vector& l, const Vector& r) { + return (l < r ? l : r); return merge_maps_with(minimum, l, r); } template @@ -240,12 +272,15 @@ Vector operator*(const ZBar& left, const Vector& right) { return right * left; } bool operator<(const Vector& left, const Vector& right) { + bool equal = true; for (Vector::const_iterator it = left.begin(), ei = left.end(); it != ei; ++it) { if (it->second < right[it->first]) { - return true; + equal = false; + } else if (it->second > right[it->first]) { + return false; } } for (Vector::const_iterator it = right.begin(), @@ -253,10 +288,12 @@ bool operator<(const Vector& left, const Vector& right) { it != ei; ++it) { if (left[it->first] < it->second) { - return true; + equal = false; + } else if (left[it->first] > it->second) { + return false; } } - return false; + return equal ? left._val < right._val : true; } template<> @@ -277,10 +314,16 @@ std::ostream& operator<<(std::ostream& cout, const Vector& v) { } -Result fromStmt(const Stmt*); + + + + +/* Expression functions */ + +Result fromExpr(const Expr*); Result fromInteger(const IntegerLiteral* expr) { - return Result(Vector(), *expr->getValue().getRawData()); + return Result(Vector(0), *expr->getValue().getRawData()); } Result fromDeclExpr(const DeclRefExpr* expr) { @@ -296,19 +339,24 @@ Result fromUnary(const UnaryOperator* op) { case UO_PostInc: break; } - return Result(Vector(), 0); + return Result(Vector(0), 0); +} + +Result operator*(const ZBar& l, const Result& r) { + return Result(l * r.first, l * r.second); } Result fromBinary(const BinaryOperator* op) { - Result left = fromStmt(op->getLHS()->IgnoreParenCasts()); - Result right = fromStmt(op->getRHS()->IgnoreParenCasts()); + Result left = fromExpr(op->getLHS()->IgnoreParenCasts()); + Result right = fromExpr(op->getRHS()->IgnoreParenCasts()); switch (op->getOpcode()) { case BO_Assign: return right; case BO_Sub: - transform_values(negate, right.first); - right.second *= -1; + right = negate_result(right); + //transform_values(negate, right.first); + //right.second *= -1; case BO_Add: { Result result; @@ -320,7 +368,7 @@ Result fromBinary(const BinaryOperator* op) { case BO_Mul: { if (!left.first.empty() && !right.first.empty()) { - return Result(Vector(), 0); + return Result(Vector(0), 0); } ZBar scalar = 0; Result value; @@ -331,30 +379,11 @@ Result fromBinary(const BinaryOperator* op) { scalar = right.second; value = left; } - if (scalar > 0) { - for (Vector::iterator it = value.first.begin(), - ei = value.first.end(); - it != ei; - ++it) { - it->second *= scalar; - } + if (scalar >= 0) { + return scalar * value; } 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; - } + return -scalar * negate_result(value); } - right.second *= scalar; - return value; } case BO_LT: case BO_LE: @@ -365,65 +394,7 @@ Result fromBinary(const BinaryOperator* op) { return Result(); } -Result fromDeclStmt(const DeclStmt* stmt) { - 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); - llvm::errs() << decl->getNameAsString() << " = "; - - 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->second) << "*" << toString(it->first); - } - 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) { - 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()); - 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->second) << "*" << toString(it->first); - } - llvm::errs() << " + " << toString(expr.second) << "\n"; - return expr; - } - return Result(); -} - -Result fromStmt(const Stmt* stmt) { +Result fromExpr(const Expr* stmt) { if (!stmt) return Result(); //stmt->dump(); @@ -434,93 +405,109 @@ Result fromStmt(const Stmt* stmt) { return fromDeclExpr(static_cast(stmt)); case Stmt::UnaryOperatorClass: return fromUnary(static_cast(stmt)); - case Stmt::DeclStmtClass: - return fromDeclStmt(static_cast(stmt)); case Stmt::BinaryOperatorClass: return fromBinary(static_cast(stmt)); } - const Expr* expr = dyn_cast(stmt); - if (expr) { - const Expr* expr2 = expr->IgnoreParenCasts(); - if (expr != expr2) - return fromStmt(expr2); - } + const Expr* expr = stmt->IgnoreParenCasts(); + if (stmt != expr) + return fromExpr(expr); llvm::errs() << "we shouldn't get here...\n"; return Result(); } -Condition fromComparison(const BinaryOperator* op) { + +/* Comparison stuff */ + +Condition fromComparison(const BinaryOperator* op, bool negate) { + Condition cond(infinity()); + if (!op) { + if (negate) + return -cond; + else + return cond; + } if (op->isRelationalOp()) { const Expr* left = op->getLHS()->IgnoreParenCasts(); const Expr* right = op->getRHS()->IgnoreParenCasts(); - Condition cond; + bool flip = false; 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(); - } + name = static_cast(left)->getNameInfo().getAsString(); } 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(); + name = static_cast(right)->getNameInfo().getAsString(); + flip = true; + } else { + return cond; + } + + if (right->getStmtClass() == Stmt::IntegerLiteralClass) { + value = *static_cast(right)->getValue().getRawData(); + } else if (left->getStmtClass() == Stmt::IntegerLiteralClass) { + value = *static_cast(left)->getValue().getRawData(); + } else { + return cond; + } + + BinaryOperator::Opcode operation = op->getOpcode(); + if (flip) { + switch (operation) { + case BO_LT: operation = BO_GT; break; + case BO_GT: operation = BO_LT; break; + case BO_LE: operation = BO_GE; break; + case BO_GE: operation = BO_LE; break; } } - return Condition(); + + switch (operation) { + case BO_LT: + if (negate) + cond[negate_string(name)] = -value; + else + cond[name] = value - 1; + break; + case BO_LE: + if (negate) + cond[negate_string(name)] = -(value + 1); + else + cond[name] = value; + break; + case BO_GE: + if (negate) + cond[name] = value - 1; + else + cond[negate_string(name)] = -value; + break; + case BO_GT: + if (negate) + cond[name] = value; + else + cond['-' + name] = -(value + 1); + break; + } } - return Condition(); + return cond; } -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; +/* Blocks */ - std::string id = toString(block->getBlockID()); - unsigned int counter = 0; - - // detemine equations for this block - LinearEquation eqn; - EqnVar* var; - Result current; +typedef std::map Counters; +typedef std::map VarMap; +typedef std::map > BlockVars; - var = &system.variable(id); +void runOnBlock(const CFGBlock* block, EqnSys& system, BlockVars& block_vars) { + Counters counters; + std::string block_id = toString(block->getBlockID()); + VarMap vars; + + for (std::set::iterator it = block_vars[block].begin(), + ei = block_vars[block].end(); + it != ei; + ++it) { + vars[*it] = &system.variable(*it + '-' + block_id + "-pre"); + } + for (CFGBlock::const_iterator it = block->begin(), ei = block->end(); it != ei; @@ -529,7 +516,7 @@ EqnVar* runOnBlock(const CFGBlock* block, EqnSys& system) { const Stmt* stmt = cfg_stmt->getStmt(); std::string name = ""; - Result expr; + Result result; if (stmt->getStmtClass() == Stmt::BinaryOperatorClass) { const BinaryOperator* binop = static_cast(stmt); if (binop->isAssignmentOp()) { @@ -537,11 +524,10 @@ EqnVar* runOnBlock(const CFGBlock* block, EqnSys& system) { const Expr* right = binop->getRHS()->IgnoreParenCasts(); if (left->getStmtClass() == Stmt::DeclRefExprClass) { name = static_cast(left)->getNameInfo().getAsString(); - expr = fromStmt(right); + result = fromExpr(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(); @@ -550,104 +536,150 @@ EqnVar* runOnBlock(const CFGBlock* block, EqnSys& system) { if ((*jt)->getKind() == Decl::Var) { const VarDecl* decl = static_cast(*jt); name = decl->getNameAsString(); - expr = fromStmt(decl->getInit()); - if (jt+1 != ej) { + result = fromExpr(decl->getInit()); + jt++; + if (jt != 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"; } } } 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()); + std::string count = toString(counters[name]); + EqnVar* var = &system.variable(name + '-' + block_id + '[' + count + ']'); + EqnVar* negative_var = &system.variable(negate_string(name) + '-' + block_id + '[' + count + ']'); + counters[name]++; + for (int negative = 0; negative < 2; ++negative) { // one loop for positive, the other for negative + if (negative) { + result = negate_result(result); + } + EqnExpr* expression = &system.constant(result.second); + for (Vector::iterator it = result.first.begin(), + ei = result.first.end(); + it != ei; + ++it) { + if (!vars[it->first]) + vars[it->first] = &system.variable(it->first + '-' + block_id + "-pre"); + std::vector additionArgs; + additionArgs.push_back(expression); + + if (it->second == 1) { + additionArgs.push_back(vars[it->first]); + } else { + std::vector multiplicationArgs; + multiplicationArgs.push_back(vars[it->first]); + multiplicationArgs.push_back(&system.constant(it->second)); + additionArgs.push_back(&system.expression(new Multiplication(), multiplicationArgs)); + } + + expression = &system.expression(new Addition(), additionArgs); + } + + std::vector maxArgs; + maxArgs.push_back(&system.constant(-infinity())); + maxArgs.push_back(expression); + if (negative) + system[*negative_var] = &system.maxExpression(maxArgs); + else + system[*var] = &system.maxExpression(maxArgs); } + vars[name] = var; + vars[negate_string(name)] = negative_var; + block_vars[block].insert(name); + block_vars[block].insert(negate_string(name)); + } - 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); + // add to our successor entry values + for (CFGBlock::const_succ_iterator + it = block->succ_begin(), + ei = block->succ_end(); + it != ei; + ++it) { + bool negate_terminator = it != block->succ_begin(); // not the first means `false` branch + Condition cond = fromComparison(static_cast(block->getTerminatorCondition()), negate_terminator); + for (VarMap::iterator jt = vars.begin(), + ej = vars.end(); + jt != ej; + ++jt) { + block_vars[*it].insert(jt->first); + + ZBar val = cond[jt->first]; + EqnVar* var = &system.variable(jt->first + '-' + toString((*it)->getBlockID()) + "-pre"); + if (system[*var] == NULL) { + std::vector maxArgs; + maxArgs.push_back(&system.constant(-infinity())); + system[*var] = &system.maxExpression(maxArgs); + } + + EqnExpr* expr = NULL; + if (val == -infinity()) { + // don't do anything here: min(-inf, x) = -inf (for all x) + } else if (val == infinity()) { + // no need to have a min here: min(inf, x) = x (for all x) + expr = jt->second; + } else { + // need a min here + std::vector minArgs; + minArgs.push_back(&system.constant(val)); + minArgs.push_back(jt->second); + expr = &system.expression(new Minimum(), minArgs); + } - // the max expression - std::vector maxArgs; - maxArgs.push_back(&system.constant(-infinity())); - maxArgs.push_back(expr); - system[*var] = &system.maxExpression(args); - eqn = LinearEquation(); + if (expr) { + std::set ignore; + for (VarMap::iterator + variables = vars.begin(), + variables_end = vars.end(); + variables != variables_end; + ++variables) { + if (ignore.find(variables->first) != ignore.end()) + continue; + ignore.insert(negate_string(variables->first)); + + std::vector plusArgs; + for (int negate = 0; negate < 2; ++negate) { + std::string var_name = negate ? negate_string(variables->first) : variables->first; + std::vector minArgs; + minArgs.push_back(vars[var_name]); + minArgs.push_back(&system.constant(cond[var_name])); + plusArgs.push_back(&system.expression(new Minimum(), minArgs)); + } + + std::vector guard_args; + guard_args.push_back(&system.expression(new Addition(), plusArgs)); // value + guard_args.push_back(&system.constant(0)); // lower-bound (so value must be >= this) + guard_args.push_back(expr); // result + expr = &system.expression(new Guard(), guard_args); + } + system[*var]->arguments().push_back(expr); + } } - - eqn[name] = expr; - expr.first = expr.first; - expr.second = -expr.second; - eqn["-"+name] = expr; } +} - 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 { - preArgs.push_back(runOnBlock(*it, system)); - } - } - 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; +IntervalAnalysis :: IntervalAnalysis(AnalysisDeclContext &context) + : context(&context) { } -void IntervalAnalysis::runOnAllBlocks() { - llvm::errs() << "Enter run on all blocks\n"; +IntervalAnalysis :: ~IntervalAnalysis() { +} +void IntervalAnalysis::runOnAllBlocks() { const CFG *cfg = this->context->getCFG(); + cfg->dump(context->getASTContext().getLangOpts(), + llvm::sys::Process::StandardErrHasColors()); + EqnSys system; + BlockVars block_vars; std::set seen; std::deque todo; @@ -659,37 +691,51 @@ void IntervalAnalysis::runOnAllBlocks() { todo.pop_front(); continue; } - llvm::errs() << block->getBlockID() << "\n"; seen.insert(block); todo.pop_front(); - runOnBlock(block, system); - llvm::errs() << "-> "; + runOnBlock(block, system, block_vars); for (CFGBlock::const_succ_iterator it = block->succ_begin(), ei = block->succ_end(); it != ei; it++ ) { - llvm::errs() << (*it)->getBlockID() << ", "; todo.push_back(*it); } - llvm::errs() << "\n\n"; } - llvm::errs() << "Exit run on all blocks\n"; + std::vector a; + + a.push_back(&system.constant(-infinity())); + a.push_back(&system.constant(0)); + system[system.variable("x")] = &system.maxExpression(a); + a.clear(); + + system.variable("y"); + + a.push_back(&system.variable("x")); + a.push_back(&system.variable("z")); + EqnExpr* minExpr = &system.expression(new Maximum(), a); + a.clear(); + + a.push_back(&system.constant(-infinity())); + a.push_back(minExpr); + system[system.variable("y")] = &system.maxExpression(a); + a.clear(); + + a.push_back(&system.constant(-infinity())); + a.push_back(&system.variable("y")); + system[system.variable("z")] = &system.maxExpression(a); 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); + EqnVar& var = system.variable(size - i - 1); llvm::errs() << toString(var.name()) << " = " << toString(rho[var]) << "\n"; } - - // cfg->dump(context->getASTContext().getLangOpts(), - // llvm::sys::Process::StandardErrHasColors()); } diff --git a/clang/lib/StaticAnalyzer/Checkers/.#ArrayBoundCheckerV2_flymake.cpp b/clang/lib/StaticAnalyzer/Checkers/.#ArrayBoundCheckerV2_flymake.cpp deleted file mode 120000 index 235903b..0000000 --- a/clang/lib/StaticAnalyzer/Checkers/.#ArrayBoundCheckerV2_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/StaticAnalyzer/Checkers/.#Checkers.td b/clang/lib/StaticAnalyzer/Checkers/.#Checkers.td deleted file mode 120000 index 235903b..0000000 --- a/clang/lib/StaticAnalyzer/Checkers/.#Checkers.td +++ /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/StaticAnalyzer/Checkers/Checkers.td b/clang/lib/StaticAnalyzer/Checkers/Checkers.td index f577a89..3c211a3 100644 --- a/clang/lib/StaticAnalyzer/Checkers/Checkers.td +++ b/clang/lib/StaticAnalyzer/Checkers/Checkers.td @@ -28,7 +28,7 @@ def DeadCodeExperimental : Package<"deadcode">, InPackage, Hidden; def Security : Package <"security">; def InsecureAPI : Package<"insecureAPI">, InPackage; -def SecurityExperimental : Package<"security">, InPackage, Hidden; +def SecurityExperimental : Package<"security">, InPackage; //, Hidden; def Taint : Package<"taint">, InPackage, Hidden; def Unix : Package<"unix">; diff --git a/clang/lib/StaticAnalyzer/Core/IntervalConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/IntervalConstraintManager.cpp index 9d04720..dc2f0d9 100644 --- a/clang/lib/StaticAnalyzer/Core/IntervalConstraintManager.cpp +++ b/clang/lib/StaticAnalyzer/Core/IntervalConstraintManager.cpp @@ -254,6 +254,7 @@ private: ConstraintManager* ento::CreateIntervalConstraintManager(ProgramStateManager&, SubEngine &subeng) { + llvm::errs() << "Creating interval constraint manager\n"; return new IntervalConstraintManager(subeng); } @@ -294,7 +295,7 @@ IntervalConstraintManager::GetRange(ProgramStateRef state, SymbolRef sym) { } //===------------------------------------------------------------------------=== -// assumeSymX methods: public interface for IntervalConstraintManager. +// eSymX methods: public interface for IntervalConstraintManager. //===------------------------------------------------------------------------===/ // The syntax for ranges below is mathematical, using [x, y] for closed ranges @@ -309,6 +310,10 @@ ProgramStateRef IntervalConstraintManager::assumeSymNE(ProgramStateRef state, SymbolRef sym, const llvm::APSInt& Int, const llvm::APSInt& Adjustment) { + llvm::errs() << "AssumeNE\n"; + state->dump(); + sym->dump(); + BasicValueFactory &BV = state->getBasicVals(); llvm::APSInt Lower = Int-Adjustment; @@ -326,6 +331,10 @@ ProgramStateRef IntervalConstraintManager::assumeSymEQ(ProgramStateRef state, SymbolRef sym, const llvm::APSInt& Int, const llvm::APSInt& Adjustment) { + llvm::errs() << "AssumeEQ\n"; + state->dump(); + sym->dump(); + // [Int-Adjustment, Int-Adjustment] BasicValueFactory &BV = state->getBasicVals(); llvm::APSInt AdjInt = Int-Adjustment; @@ -337,6 +346,10 @@ ProgramStateRef IntervalConstraintManager::assumeSymLT(ProgramStateRef state, SymbolRef sym, const llvm::APSInt& Int, const llvm::APSInt& Adjustment) { + llvm::errs() << "AssumeLT\n"; + state->dump(); + sym->dump(); + BasicValueFactory &BV = state->getBasicVals(); QualType T = state->getSymbolManager().getType(sym); @@ -358,6 +371,10 @@ ProgramStateRef IntervalConstraintManager::assumeSymGT(ProgramStateRef state, SymbolRef sym, const llvm::APSInt& Int, const llvm::APSInt& Adjustment) { + llvm::errs() << "AssumeGT\n"; + state->dump(); + sym->dump(); + BasicValueFactory &BV = state->getBasicVals(); QualType T = state->getSymbolManager().getType(sym); @@ -379,6 +396,10 @@ ProgramStateRef IntervalConstraintManager::assumeSymGE(ProgramStateRef state, SymbolRef sym, const llvm::APSInt& Int, const llvm::APSInt& Adjustment) { + llvm::errs() << "AssumeGE\n"; + state->dump(); + sym->dump(); + BasicValueFactory &BV = state->getBasicVals(); QualType T = state->getSymbolManager().getType(sym); @@ -401,6 +422,10 @@ ProgramStateRef IntervalConstraintManager::assumeSymLE(ProgramStateRef state, SymbolRef sym, const llvm::APSInt& Int, const llvm::APSInt& Adjustment) { + llvm::errs() << "AssumeLE\n"; + state->dump(); + sym->dump(); + BasicValueFactory &BV = state->getBasicVals(); QualType T = state->getSymbolManager().getType(sym); -- cgit v1.2.3