Implement Tarjan-Havlak Loop Analysis Algorithm
MODIFY
CMakeLists.txt
CMakeLists.txt
@@ -119,6 +119,7 @@ set(UTIL_SRCS
util/sort.cpp
util/stopwatch.cpp
util/symexec.cpp
+ util/unionfind.cpp
)
add_library(util STATIC ${UTIL_SRCS})

MODIFY
ir/function.cpp
ir/function.cpp
#include "ir/function.h"
#include "ir/instr.h"
#include "util/errors.h"
+#include "util/unionfind.h"
+#include <fstream>
using namespace smt;
using namespace util;
@@ -253,6 +255,14 @@ bool Function::removeUnusedStuff(const multimap<Value*, Value*> &users,
return changed;
}
+void Function::unroll(unsigned k) {
+ if (k == 0)
+ return;
+ LoopAnalysis la(*this);
+ ofstream out("a.gv");
+ la.printDot(out);
+}
+
void Function::print(ostream &os, bool print_header) const {
{
const auto &gvars = getGlobalVars();
@@ -428,5 +438,121 @@ void DomTree::printDot(std::ostream &os) const {
os << "}\n";
}
+
+void LoopAnalysis::getDepthFirstSpanningTree() {
+ unsigned bb_count = f.getBBs().size();
+ node.resize(bb_count, nullptr);
+ last.resize(bb_count, -1u);
+
+ map<const BasicBlock*, vector<const BasicBlock*>> edges;
+ for (auto [src, dst, instr] : cfg) {
+ edges[&src].push_back(&dst);
+ }
+
+ unsigned current = 0;
+ vector<pair<const BasicBlock*,bool>> s;
+ s.emplace_back(&f.getFirstBB(), false);
+ while(!s.empty()) {
+ auto &[bb, flag] = s.back();
+ s.pop_back();
+
+ if (flag) {
+ last[number[bb]] = current - 1;
+ } else {
+ node[current] = bb;
+ number[bb] = current++;
+
+ s.emplace_back(bb, true);
+ for (auto tgt : edges[bb])
+ if (!number.count(tgt))
+ s.emplace_back(tgt, false);
+ }
+ }
+}
+
+// Implemention of Tarjan-Havlak algorithm.
+//
+// Irreducible loops are partially supported.
+//
+// Tarjan, R. (1974). Testing Flow Graph Reducibility.
+// Havlak, P. (1997). Nesting of reducible and irreducible loops.
+void LoopAnalysis::analysis() {
+ getDepthFirstSpanningTree();
+ unsigned bb_count = f.getBBs().size();
+
+ auto isAncestor = [this](unsigned w, unsigned v) -> bool {
+ return w <= v && v <= last[w];
+ };
+
+ vector<set<unsigned>> nonBackPreds(bb_count), backPreds(bb_count);
+ header.resize(bb_count, 0);
+ type.resize(bb_count, NodeType::nonheader);
+
+ for (auto [src, dst, instr] : cfg) {
+ unsigned v = number.at(&src), w = number.at(&dst);
+ if (isAncestor(w, v))
+ backPreds[w].insert(v);
+ else
+ nonBackPreds[w].insert(v);
+ }
+
+ UnionFind uf(bb_count);
+
+ for (unsigned w = bb_count - 1; w != -1u; --w) {
+ set<unsigned> P;
+ for (unsigned v : backPreds[w])
+ if (v != w)
+ P.insert(uf.find(v));
+ else
+ type[w] = NodeType::self;
+
+ if (!P.empty())
+ type[w] = NodeType::reducible;
+
+ set<unsigned> workList(P);
+ while (!workList.empty()) {
+ unsigned x = *workList.begin();
+ workList.erase(x);
+
+ for (unsigned y : nonBackPreds[x]) {
+ unsigned yy = uf.find(y);
+ if (!isAncestor(w, yy)) {
+ type[w] = NodeType::irreducible;
+ nonBackPreds[w].insert(yy);
+ } else if (yy != w && !P.count(yy)) {
+ P.insert(yy);
+ workList.insert(yy);
+ }
+ }
+ }
+
+ for (unsigned x : P) {
+ header[x] = w;
+ uf.merge(x, w);
+ }
+ }
+}
+
+void LoopAnalysis::printDot(ostream &os) const {
+ os << "digraph {\n";
+ for (unsigned i = 0, e = f.getBBs().size(); i != e; ++i) {
+ if (type[i] == NodeType::nonheader)
+ continue;
+ os << '"' << bb_dot_name(node[i]->getName())
+ << "\" [shape=circle]\n";
+ }
+ for (unsigned i = 0, e = f.getBBs().size(); i != e; ++i) {
+ // do not draw self loop for root
+ if (header[i] == i)
+ continue;
+ if (type[i] == NodeType::nonheader ||
+ type[header[i]] == NodeType::nonheader)
+ continue;
+ os << '"' << bb_dot_name(node[header[i]]->getName()) << "\" -> \""
+ << bb_dot_name(node[i]->getName()) << "\";\n";
+ }
+ os << "}\n";
+}
+
}

MODIFY
ir/function.h
ir/function.h
@@ -156,6 +156,8 @@ public:
bool removeUnusedStuff(const std::multimap<Value*, Value*> &users,
const std::vector<std::string_view> &src_glbs);
+ void unroll(unsigned k);
+
void print(std::ostream &os, bool print_header = true) const;
friend std::ostream &operator<<(std::ostream &os, const Function &f);
};
@@ -212,4 +214,22 @@ class DomTree final {
void printDot(std::ostream &os) const;
};
+class LoopAnalysis final {
+ Function &f;
+ CFG cfg;
+
+ std::map<const BasicBlock*, unsigned> number;
+ std::vector<const BasicBlock*> node;
+ std::vector<unsigned> last;
+ void getDepthFirstSpanningTree();
+
+ std::vector<unsigned> header;
+ enum NodeType { nonheader, self, reducible, irreducible };
+ std::vector<NodeType> type;
+ void analysis();
+public:
+ LoopAnalysis(Function &f) : f(f), cfg(f) { analysis(); }
+ void printDot(std::ostream &os) const;
+};
+
}

MODIFY
tools/alive-tv.cpp
tools/alive-tv.cpp
@@ -94,6 +94,16 @@ static llvm::cl::opt<std::string> opt_tgt_fn(
"tgt-fn", llvm::cl::desc("Name of tgt function (without @)"),
llvm::cl::cat(opt_alive), llvm::cl::init("tgt"));
+static llvm::cl::opt<unsigned> opt_src_unrolling_factor(
+ "src-unroll",
+ llvm::cl::desc("Unrolling factor for src function (default=0)"),
+ llvm::cl::cat(opt_alive), llvm::cl::init(0));
+
+static llvm::cl::opt<unsigned> opt_tgt_unrolling_factor(
+ "tgt-unroll",
+ llvm::cl::desc("Unrolling factor for tgt function (default=0)"),
+ llvm::cl::cat(opt_alive), llvm::cl::init(0));
+
static llvm::cl::opt<bool> opt_tactic_verbose(
"tactic-verbose", llvm::cl::desc("SMT Tactic verbose mode"),
llvm::cl::cat(opt_alive), llvm::cl::init(false));
@@ -283,6 +293,7 @@ static void compareFunctions(llvm::Function &F1, llvm::Function &F2,
++errorCount;
return;
}
+ Func1->unroll(opt_src_unrolling_factor);
auto Func2 = llvm2alive(F2, llvm::TargetLibraryInfoWrapperPass(targetTriple)
.getTLI(F2), Func1->getGlobalVarNames());
@@ -292,6 +303,7 @@ static void compareFunctions(llvm::Function &F1, llvm::Function &F2,
++errorCount;
return;
}
+ Func2->unroll(opt_tgt_unrolling_factor);
smt_init->reset();
Transform t;

ADD
util/unionfind.cpp
+// Copyright (c) 2018-present The Alive2 Authors.
+// Distributed under the MIT license that can be found in the LICENSE file.
+
+#include "util/unionfind.h"
+#include <vector>
+
+using namespace std;
+
+namespace util {
+
+UnionFind::UnionFind(unsigned n) {
+ for (unsigned i = 0; i < n; ++i) {
+ id.push_back(i);
+ }
+}
+
+unsigned UnionFind::find(unsigned i) {
+ unsigned root = i;
+ while (root != id[root])
+ root = id[root];
+ id[i] = root;
+ return root;
+}
+
+void UnionFind::merge(unsigned p, unsigned q) {
+ unsigned i = find(p);
+ unsigned j = find(q);
+ id[i] = j;
+}
+
+}

ADD
util/unionfind.h
+#pragma once
+
+// Copyright (c) 2018-present The Alive2 Authors.
+// Distributed under the MIT license that can be found in the LICENSE file.
+
+#include <vector>
+
+namespace util {
+
+class UnionFind final {
+ std::vector<unsigned> id;
+public:
+ UnionFind(unsigned n);
+ unsigned find(unsigned i);
+ void merge(unsigned p, unsigned q);
+};
+
+}

Implement Tarjan-Havlak Loop Analysis Algorithm (#501)