From 51dd6b2b022ade7a1fc4ec8c404d9b81c7e961f5 Mon Sep 17 00:00:00 2001 From: "Zancanaro; Carlo" Date: Tue, 27 Nov 2012 14:56:56 +1100 Subject: Updated solver stuff. This really should have already been in here... --- clang/lib/Analysis/Interval.cpp | 350 +++++++++++++-------- clang/lib/StaticAnalyzer/Checkers/IntervalTest.cpp | 102 +++++- 2 files changed, 313 insertions(+), 139 deletions(-) (limited to 'clang/lib') diff --git a/clang/lib/Analysis/Interval.cpp b/clang/lib/Analysis/Interval.cpp index 4b274ed..ab79abb 100644 --- a/clang/lib/Analysis/Interval.cpp +++ b/clang/lib/Analysis/Interval.cpp @@ -5,7 +5,6 @@ #include "clang/AST/StmtVisitor.h" #include "clang/Analysis/Analyses/IntervalSolver/Log.hpp" -#include "clang/Analysis/Analyses/IntervalSolver/Complete.hpp" #include "clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp" #include "clang/Analysis/Analyses/IntervalSolver/EquationSystem.hpp" @@ -22,6 +21,7 @@ using namespace clang; using namespace std; + template T neg(const T& t) { return -t; @@ -90,14 +90,6 @@ ostream& operator<<(ostream& cout, const map& v) { // // Hooray! -typedef Complete ZBar; -template<> -ZBar infinity() { - return ZBar(1, true); -} - - - struct Vector : public map { @@ -160,7 +152,7 @@ Vector operator+(const Vector& left, const Vector& right) { return result; } -Vector operator*(const ZBar& left, const Vector& right) { +Vector scalar_mult(const ZBar& left, const Vector& right) { Vector result(left * right._val); for (Vector::const_iterator @@ -173,9 +165,6 @@ Vector operator*(const ZBar& left, const Vector& right) { return result; } -Vector operator*(const Vector& left, const ZBar& right) { - return right * left; -} ostream& operator<<(ostream& cout, const Vector& v) { cout << "{"; @@ -225,6 +214,7 @@ Result fromDeclExpr(const DeclRefExpr* expr) { } Result fromUnary(const UnaryOperator* op) { + assert(false); // unary operations aren't supported. Sorry! switch (op->getOpcode()) { case UO_PreInc: break; @@ -235,7 +225,7 @@ Result fromUnary(const UnaryOperator* op) { } Result operator*(const ZBar& l, const Result& r) { - return Result(l * r.first, l * r.second); + return Result(scalar_mult(l, r.first), l * r.second); } Result fromBinary(const BinaryOperator* op) { @@ -276,12 +266,8 @@ Result fromBinary(const BinaryOperator* op) { return scalar * -value; } } - case BO_LT: - case BO_LE: - case BO_GT: - case BO_GE: - break; - } + } + assert(false); // Unknown binary operation. Only assignment, addition, subtraction and multiplication are permitted return Result(); } @@ -384,24 +370,25 @@ Condition fromComparison(const BinaryOperator* op, bool negate) { /* Blocks */ -typedef map Counters; -typedef map VarMap; -typedef map > BlockVars; +struct Block : public map { + Result& operator[](const string& key) { + iterator it = this->find(key); + if (it != this->end()) + return it->second; + Vector vector; + vector[key] = 1; + pair p = this->insert(pair(key, Result(vector, 0))); + return p.first->second; + } +}; -void runOnBlock(const CFGBlock* block, EqnSys& system, BlockVars& block_vars) { - Counters counters; - string block_id = toString(block->getBlockID()); - VarMap vars; - for (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(); +vector splitBlock(const CFGBlock* block) { + vector subBlocks; + + for (CFGBlock::const_iterator + it = block->begin(), + ei = block->end(); it != ei; ++it) { const CFGStmt* cfg_stmt = it->getAs(); @@ -437,78 +424,161 @@ void runOnBlock(const CFGBlock* block, EqnSys& system, BlockVars& block_vars) { } } } - if (name == "") - continue; - string count = toString(counters[name]); - EqnVar* var = &system.variable(name + '-' + block_id + '[' + count + ']'); - EqnVar* negative_var = &system.variable(-name + '-' + block_id + '[' + count + ']'); - counters[name]++; - for (int negative = 0; negative < 2; ++negative) { // one loop for positive, the other for negative - if (negative) { - result = -result; - } - - EqnExpr* expression; + if (name != "") { + if (subBlocks.empty()) + subBlocks.push_back(Block()); + Block& subBlock = subBlocks.back(); - if (result.first.size() > 0) { - // make sure all our variables exist in vars + bool make_new = subBlock.find(name) != subBlock.end(); + if (!make_new) { 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"); + if (subBlock.find(it->first) != subBlock.end()) { + make_new = true; + break; + } } + } + if (make_new) { + Block newBlock; + newBlock[name] = result; + subBlocks.push_back(newBlock); + } else { + subBlock[name] = result; + } + } + } - // set up the min-cost-flow operator - vector supplies; - vector > arcs; - vector minCostArgs; - ZBar dummy_value = 0; - supplies.push_back(dummy_value); // dummy node to suck up flow - int index = 1; // the solver uses 1-indexing, for some reason - for (map::iterator - it = vars.begin(), - ei = vars.end(); - it != ei; - it++) { - index++; - supplies.push_back(result.first[it->first]); - dummy_value -= result.first[it->first]; - if (it->first[0] == '-') - arcs.push_back(pair(1,index)); - else - arcs.push_back(pair(index,1)); - minCostArgs.push_back(vars[it->first]); + return subBlocks; +} + +typedef map Counters; + +string var_name(const int& i, const string& block_id) { + return toString(i) + '-' + block_id; +} + +void runOnBlock(const ConstraintMatrix& T, const CFGBlock* block, EqnSys& system) { + + int size = T.size(); + string block_id = toString(block->getBlockID()); + vector counters(size); + vector vars(size); + + vector infArgs; + infArgs.push_back(&system.constant(-infinity())); + infArgs.push_back(&system.constant(infinity())); + for (int i = 0; i < size; ++i) { + vars[i] = &system.variable(var_name(i, block_id)+"-pre"); + if (system[*vars[i]] == NULL) { + system[*vars[i]] = &system.maxExpression(infArgs); + } + } + + vector subBlocks = splitBlock(block); + + map mcf_indices; // 1-indexed, for the mcf stuff + int mcf_vert_count = 1; + vector > mcf_edges; + { + for (int j = 0; j < size; ++j) { + string from = ""; + string to = ""; + for (map::const_iterator + jt = T[j].begin(), + ej = T[j].end(); + jt != ej; + ++jt) { + if (mcf_indices.find(jt->first) == mcf_indices.end()) { + mcf_indices[jt->first] = ++mcf_vert_count; + } + assert(jt->second == 1 || jt->second == -1); + assert(jt->second != 1 || from == ""); + assert(jt->second != -1 || to == ""); + if (jt->second == 1) + from = jt->first; + if (jt->second == -1) + to = jt->first; + } + int source = (from == "" ? 1 : mcf_indices[from]); + int dest = (to == "" ? 1 : mcf_indices[to]); + + mcf_edges.push_back(pair(source,dest)); + } + } + + + + for (int blockIndex = 0, blockSize = subBlocks.size(); blockIndex < blockSize; ++blockIndex) { + Block& subBlock = subBlocks[blockIndex]; + + vector nextVars(size); + for (int i = 0; i < size; ++i) { + const map& tk = T[i]; + + ZBar b = 0; + map indices; + for (map::const_iterator + tk_it = tk.begin(), + tk_end = tk.end(); + tk_it != tk_end; + tk_it++) { + b += ZBar(tk_it->second) * subBlock[tk_it->first].second; + } + + vector g(mcf_vert_count); + for (map::const_iterator + tk_it = tk.begin(), + tk_end = tk.end(); + tk_it != tk_end; + tk_it++) { // each column of Tk + const map& A = subBlock[tk_it->first].first; + for (map::const_iterator + A_it = A.begin(), + A_end = A.end(); + A_it != A_end; + A_it++) { // each row of A + ZBar value = A_it->second * ZBar(tk_it->second); + g[mcf_indices[A_it->first]-1] += value; + g[0] -= value; } - supplies[0] = dummy_value; + } + + vector args(size); + for (int j = 0; j < size; ++j) { + assert(vars[j] != NULL); + args[j] = vars[j]; + } + + EqnExpr* minCostExpr = &system.expression(new MinCostFlow(g, mcf_edges), args); - EqnExpr* minCostExpr = &system.expression(new MinCostFlow(supplies, arcs), minCostArgs); - + EqnExpr* expression; + if (b == 0) { + expression = minCostExpr; + } else { // add the constant factor to the min-cost bit vector additionArgs; - additionArgs.push_back(&system.constant(result.second)); + additionArgs.push_back(&system.constant(b)); additionArgs.push_back(minCostExpr); expression = &system.expression(new Addition(), additionArgs); - } else { - expression = &system.constant(result.second); } - // max(-inf, expr), so strategy iteration will work + string count = toString(counters[i]); + counters[i]++; + EqnVar* newVar = &system.variable(var_name(i, block_id)+'-'+count); + + // make it max(-inf, expr), so strategy iteration will work 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); + system[*newVar] = &system.maxExpression(maxArgs); + nextVars[i] = newVar; } - vars[name] = var; - vars[-name] = negative_var; - block_vars[block].insert(name); - block_vars[block].insert(-name); + vars = nextVars; // update our variable listings } // add to our successor entry values @@ -519,35 +589,43 @@ void runOnBlock(const CFGBlock* block, EqnSys& system, BlockVars& block_vars) { ++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"); + + for (int i = 0; i < size; ++i) { + EqnVar* var = &system.variable(var_name(i, toString((*it)->getBlockID()))+"-pre"); if (system[*var] == NULL) { 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) - expr = &system.constant(-infinity()); - } 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 - vector minArgs; - minArgs.push_back(&system.constant(val)); - minArgs.push_back(jt->second); - expr = &system.expression(new Minimum(), minArgs); + if (T[i].size() == 1) { // only one value in this row, so it's okay for a test + ZBar val = infinity(); + Vector::iterator cond_finder; + if (T[i].begin()->second < 0) + cond_finder = cond.find('-' + T[i].begin()->first); + else + cond_finder = cond.find(T[i].begin()->first); + if (cond_finder != cond.end()) { + val = cond_finder->second; + //val *= ; // potentially change it's sign + } + if (val == -infinity()) { + // don't do anything here: min(-inf, x) = -inf (for all x) + expr = &system.constant(-infinity()); + } else if (val == infinity()) { + // no need to have a min here: min(inf, x) = x (for all x) + expr = vars[i]; + } else { + // need a min here + vector minArgs; + minArgs.push_back(&system.constant(val)); + minArgs.push_back(vars[i]); + expr = &system.expression(new Minimum(), minArgs); + } + } else { // more than one value in this row, so leave it for now... + expr = vars[i]; } - system[*var]->arguments().push_back(expr); } } @@ -565,33 +643,13 @@ IntervalAnalysis :: IntervalAnalysis(AnalysisDeclContext &context) IntervalAnalysis :: ~IntervalAnalysis() { } -void IntervalAnalysis::runOnAllBlocks(const Decl& decl) { +map > IntervalAnalysis::runOnAllBlocks(const Decl& decl, const ConstraintMatrix& T) { const CFG *cfg = this->context->getCFG(); cfg->dump(context->getASTContext().getLangOpts(), llvm::sys::Process::StandardErrHasColors()); - EqnSys system; - BlockVars block_vars; - - vector infArg; - infArg.push_back(&system.constant(-infinity())); // left-most argument has to be -infinity - infArg.push_back(&system.constant(infinity())); - set& function_arguments = block_vars[&cfg->getEntry()]; - string block_id = toString(cfg->getEntry().getBlockID()); - if (const FunctionDecl* func = dyn_cast(&decl)) { - for (unsigned int i = func->getNumParams(); i > 0; i--) { - string name = func->getParamDecl(i-1)->getNameAsString(); - - // add the variables to the first block - function_arguments.insert(name); - function_arguments.insert(neg(name)); - - // set the vars to infinity (unconstrained) - system[system.variable(name + '-' + block_id + "-pre")] = &system.maxExpression(infArg); - system[system.variable(neg(name) + '-' + block_id + "-pre")] = &system.maxExpression(infArg); - } - } + EqnSys system; set seen; deque todo; @@ -605,25 +663,41 @@ void IntervalAnalysis::runOnAllBlocks(const Decl& decl) { } seen.insert(block); todo.pop_front(); - runOnBlock(block, system, block_vars); + runOnBlock(T, block, system); for (CFGBlock::const_succ_iterator it = block->succ_begin(), - ei = block->succ_end(); + ei = block->succ_end(); it != ei; it++ ) { todo.push_back(*it); } } - llvm::errs() << toString(system) << "\n"; - system.indexMaxExpressions(); Solver solver(system); - for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) { - EqnVar& var = system.variable(i); - llvm::errs() << toString(var.name()) << " = " << toString(solver.solve(var)) << "\n"; + map > resultMap; + + for (int i = 0; i < system.variableCount(); ++i) { + solver.solve(system.variable(i)); + } + + for (CFG::const_iterator + it = cfg->begin(), + ei = cfg->end(); + it != ei; + ++it) { + vector& vector = resultMap[*it]; + string block_id = toString((*it)->getBlockID()); + for (int i = 0, size = T.size(); i < size; ++i) { + EqnVar& var = system.variable(var_name(i, block_id) + "-pre"); + vector.push_back(solver.solve(var)); + } } + + llvm::errs() << toString(system) << "\n"; + + return resultMap; } diff --git a/clang/lib/StaticAnalyzer/Checkers/IntervalTest.cpp b/clang/lib/StaticAnalyzer/Checkers/IntervalTest.cpp index badb671..c1e0273 100644 --- a/clang/lib/StaticAnalyzer/Checkers/IntervalTest.cpp +++ b/clang/lib/StaticAnalyzer/Checkers/IntervalTest.cpp @@ -7,6 +7,15 @@ using namespace clang; using namespace ento; +using namespace std; + +#include +template +string toString(const T& obj) { + stringstream stream; + stream << obj; + return stream.str(); +} namespace { class IntervalTest: public Checker { @@ -14,7 +23,98 @@ public: void checkASTCodeBody(const Decl *D, AnalysisManager& mgr, BugReporter &BR) const { if (IntervalAnalysis *a = mgr.getAnalysis(D)) { - a->runOnAllBlocks(*D); + CFG* cfg = mgr.getCFG(D); + + set variables; + + if (const FunctionDecl* func = dyn_cast(D)) { + for (unsigned int i = func->getNumParams(); i > 0; i--) { + variables.insert(func->getParamDecl(i-1)->getNameAsString()); + } + } + for (CFG::iterator + it = cfg->begin(), + ei = cfg->end(); + it != ei; + ++it) { + for (CFGBlock::iterator + block_it = (*it)->begin(), + block_end = (*it)->end(); + block_it != block_end; + block_it++) { + const CFGStmt* cfg_stmt = block_it->getAs(); + const Stmt* stmt = cfg_stmt->getStmt(); + if (stmt->getStmtClass() == Stmt::BinaryOperatorClass) { + const BinaryOperator* binop = static_cast(stmt); + if (binop->isAssignmentOp()) { + const Expr* left = binop->getLHS()->IgnoreParenCasts(); + if (left->getStmtClass() == Stmt::DeclRefExprClass) { + variables.insert(static_cast(left)->getNameInfo().getAsString()); + } + } + } else if (stmt->getStmtClass() == Stmt::DeclStmtClass) { + 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); + variables.insert(decl->getNameAsString()); + jt++; + if (jt != ej) { + llvm::errs() << "Only the first declaration in a multi-declaration statement is used.\n"; + } + break; // only take the first one, for now + } + } + } + } + } + + + + vector labels; + ConstraintMatrix T; + set::iterator end = variables.end(); + for (set::iterator it = variables.begin(); + it != end; + ++it) { + map pos_row; + pos_row[*it] = 1; + T.push_back(pos_row); + labels.push_back(*it); + + map neg_row; + neg_row[*it] = -1; + T.push_back(neg_row); + labels.push_back("-" + *it); + + for (set::iterator jt = variables.begin(); + jt != end; + ++jt) { + if (it != jt) { + map diff_row; + diff_row[*it] = 1; + diff_row[*jt] = -1; + T.push_back(diff_row); + labels.push_back(*it + " - " + *jt); + } + } + } + + map > result = a->runOnAllBlocks(*D, T); + + for (map >::iterator + it = result.begin(), + ei = result.end(); + it != ei; + ++it) { + llvm::errs() << "Block " << toString(it->first->getBlockID()) << ": \n"; + for (unsigned int i = 0; i < T.size(); ++i) { + llvm::errs() << "\t" << labels[i] << " <= " << toString(it->second[i]) << "\n"; + } + } } } }; -- cgit v1.2.3