Changeset 5152
 Timestamp:
 Sep 8, 2016, 5:11:14 PM (3 years ago)
 Location:
 icGREP/icgrepdevel/icgrep/pablo/optimizers
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

icGREP/icgrepdevel/icgrep/pablo/optimizers/booleanreassociationpass.cpp
r4919 r5152 4 4 #include <boost/circular_buffer.hpp> 5 5 #include <boost/graph/adjacency_list.hpp> 6 #include <boost/graph/filtered_graph.hpp>7 6 #include <boost/graph/topological_sort.hpp> 7 #include <boost/graph/strong_components.hpp> 8 8 #include <pablo/optimizers/pablo_simplifier.hpp> 9 9 #include <pablo/analysis/pabloverifier.hpp> 10 10 #include <algorithm> 11 11 #include <numeric> // std::iota 12 #ifndef NDEBUG13 #include <queue>14 #endif15 12 #include <pablo/printer_pablos.h> 16 13 #include <iostream> 14 #include <llvm/Support/CommandLine.h> 15 #include "maxsat.hpp" 17 16 18 17 using namespace boost; 19 18 using namespace boost::container; 20 19 20 21 static cl::OptionCategory ReassociationOptions("Reassociation Optimization Options", "These options control the Pablo Reassociation optimization pass."); 22 23 static cl::opt<unsigned> LoadEarly("ReassociationLoadEarly", cl::init(false), 24 cl::desc("When recomputing an Associative operation, load values from preceeding blocks at the beginning of the " 25 "Scope Block rather than at the point of first use."), 26 cl::cat(ReassociationOptions)); 27 21 28 namespace pablo { 22 29 23 30 using TypeId = PabloAST::ClassTypeId; 24 using DependencyGraph = BooleanReassociationPass::Graph;25 using Vertex = DependencyGraph::vertex_descriptor;31 using Graph = BooleanReassociationPass::Graph; 32 using Vertex = Graph::vertex_descriptor; 26 33 using VertexData = BooleanReassociationPass::VertexData; 27 using SinkMap = BooleanReassociationPass::Map; 28 using DistributionGraph = adjacency_list<hash_setS, vecS, bidirectionalS, Vertex>; 29 using DistributionMap = flat_map<DependencyGraph::vertex_descriptor, DistributionGraph::vertex_descriptor>; 34 using DistributionGraph = BooleanReassociationPass::DistributionGraph; 35 using DistributionMap = flat_map<Graph::vertex_descriptor, DistributionGraph::vertex_descriptor>; 30 36 using VertexSet = std::vector<Vertex>; 31 37 using VertexSets = std::vector<VertexSet>; … … 39 45 **  */ 40 46 template<typename Iterator> 41 inline DependencyGraph::edge_descriptor first(const std::pair<Iterator, Iterator> & range) {47 inline Graph::edge_descriptor first(const std::pair<Iterator, Iterator> & range) { 42 48 assert (range.first != range.second); 43 49 return *range.first; 44 50 } 45 51 46 #ifndef NDEBUG47 static bool no_path(const Vertex u, const Vertex v, const DependencyGraph & G) {48 if (u == v) return false;49 flat_set<Vertex> V;50 std::queue<Vertex> Q;51 Q.push(u);52 for (;;) {53 Vertex w = Q.front();54 if (w == v) {55 return false;56 }57 Q.pop();58 for (auto e : make_iterator_range(out_edges(w, G))) {59 Vertex x = target(e, G);60 if (V.count(x)) continue;61 Q.push(x);62 V.insert(x);63 }64 if (Q.empty()) {65 break;66 }67 }68 return true;69 }70 #endif71 72 inline void add_edge(PabloAST * expr, const Vertex u, const Vertex v, DependencyGraph & G) {73 assert (no_path(v, u, G));74 // Make sure each edge is unique75 for (auto e : make_iterator_range(out_edges(u, G))) {76 if (LLVM_UNLIKELY(target(e, G) == v && (G[e] == nullptr  G[e] == expr))) {77 G[e] = expr;78 return;79 }80 }81 G[std::get<0>(add_edge(u, v, G))] = expr;82 }83 84 52 static inline bool inCurrentBlock(const Statement * stmt, const PabloBlock * const block) { 85 53 return stmt>getParent() == block; … … 98 66 } 99 67 68 inline Z3_ast & getDefinition(VertexData & data) { 69 return std::get<2>(data); 70 } 71 72 inline PabloAST * getValue(const VertexData & data) { 73 return std::get<1>(data); 74 } 75 100 76 inline PabloAST *& getValue(VertexData & data) { 101 return std::get<1>(data);102 }103 104 inline PabloAST * getValue(const VertexData & data) {105 77 return std::get<1>(data); 106 78 } … … 127 99 } 128 100 129 inline bool isMutable(const VertexData & data) { 130 return getType(data) != TypeId::Var; 131 } 132 133 inline bool isNonEscaping(const VertexData & data) { 134 // If these are redundant, the Simplifier pass will eliminate them. Trust that they're necessary. 135 switch (getType(data)) { 136 case TypeId::Assign: 137 case TypeId::Next: 138 case TypeId::If: 139 case TypeId::While: 140 return false; 141 default: 142 return true; 143 } 144 } 145 146 inline bool isSameType(const VertexData & data1, const VertexData & data2) { 147 return getType(data1) == getType(data2); 101 void add_edge(PabloAST * expr, const Vertex u, const Vertex v, Graph & G) { 102 // Make sure each edge is unique 103 assert (u < num_vertices(G) && v < num_vertices(G)); 104 assert (u != v); 105 106 // Just because we've supplied an expr doesn't mean it's useful. Check it. 107 if (expr) { 108 if (isAssociative(G[v])) { 109 expr = nullptr; 110 } else { 111 bool clear = true; 112 if (const Statement * dest = dyn_cast_or_null<Statement>(getValue(G[v]))) { 113 for (unsigned i = 0; i < dest>getNumOperands(); ++i) { 114 if (dest>getOperand(i) == expr) { 115 clear = false; 116 break; 117 } 118 } 119 } 120 if (LLVM_LIKELY(clear)) { 121 expr = nullptr; 122 } 123 } 124 } 125 126 for (auto e : make_iterator_range(out_edges(u, G))) { 127 if (LLVM_UNLIKELY(target(e, G) == v)) { 128 if (expr) { 129 if (G[e] == nullptr) { 130 G[e] = expr; 131 } else if (G[e] != expr) { 132 continue; 133 } 134 } 135 return; 136 } 137 } 138 G[boost::add_edge(u, v, G).first] = expr; 148 139 } 149 140 … … 167 158 } 168 159 160 161 /**  * 162 * @brief printGraph 163 **  */ 164 static void printGraph(const Graph & G, const std::string name) { 165 raw_os_ostream out(std::cerr); 166 167 std::vector<unsigned> c(num_vertices(G)); 168 strong_components(G, make_iterator_property_map(c.begin(), get(vertex_index, G), c[0])); 169 170 out << "digraph " << name << " {\n"; 171 for (auto u : make_iterator_range(vertices(G))) { 172 if (in_degree(u, G) == 0 && out_degree(u, G) == 0) { 173 continue; 174 } 175 out << "v" << u << " [label=\"" << u << ": "; 176 TypeId typeId; 177 PabloAST * expr; 178 Z3_ast node; 179 std::tie(typeId, expr, node) = G[u]; 180 bool temporary = false; 181 bool error = false; 182 if (expr == nullptr  (typeId != expr>getClassTypeId() && typeId != TypeId::Var)) { 183 temporary = true; 184 switch (typeId) { 185 case TypeId::And: 186 out << "And"; 187 break; 188 case TypeId::Or: 189 out << "Or"; 190 break; 191 case TypeId::Xor: 192 out << "Xor"; 193 break; 194 case TypeId::Not: 195 out << "Not"; 196 break; 197 default: 198 out << "???"; 199 error = true; 200 break; 201 } 202 if (expr) { 203 out << " ("; PabloPrinter::print(expr, out); out << ")"; 204 } 205 } else { 206 PabloPrinter::print(expr, out); 207 } 208 if (node == nullptr) { 209 out << " (*)"; 210 error = true; 211 } 212 out << "\""; 213 if (typeId == TypeId::Var) { 214 out << " style=dashed"; 215 } 216 if (error) { 217 out << " color=red"; 218 } else if (temporary) { 219 out << " color=blue"; 220 } 221 out << "];\n"; 222 } 223 for (auto e : make_iterator_range(edges(G))) { 224 const auto s = source(e, G); 225 const auto t = target(e, G); 226 out << "v" << s << " > v" << t; 227 bool cyclic = (c[s] == c[t]); 228 if (G[e]  cyclic) { 229 out << " ["; 230 if (G[e]) { 231 out << "label=\""; 232 PabloPrinter::print(G[e], out); 233 out << "\" "; 234 } 235 if (cyclic) { 236 out << "color=red "; 237 } 238 out << "]"; 239 } 240 out << ";\n"; 241 } 242 243 if (num_vertices(G) > 0) { 244 245 out << "{ rank=same;"; 246 for (auto u : make_iterator_range(vertices(G))) { 247 if (in_degree(u, G) == 0 && out_degree(u, G) != 0) { 248 out << " v" << u; 249 } 250 } 251 out << "}\n"; 252 253 out << "{ rank=same;"; 254 for (auto u : make_iterator_range(vertices(G))) { 255 if (out_degree(u, G) == 0 && in_degree(u, G) != 0) { 256 out << " v" << u; 257 } 258 } 259 out << "}\n"; 260 261 } 262 263 out << "}\n\n"; 264 out.flush(); 265 } 266 169 267 /**  * 170 268 * @brief optimize 171 269 **  */ 172 bool BooleanReassociationPass::optimize(PabloFunction & function) { 173 BooleanReassociationPass brp; 270 bool BooleanReassociationPass::optimize(PabloFunction & function) { 271 272 Z3_config cfg = Z3_mk_config(); 273 Z3_context ctx = Z3_mk_context(cfg); 274 Z3_del_config(cfg); 275 Z3_solver solver = Z3_mk_solver(ctx); 276 Z3_solver_inc_ref(ctx, solver); 277 278 BooleanReassociationPass brp(ctx, solver, function); 174 279 brp.processScopes(function); 175 #ifndef NDEBUG 176 PabloVerifier::verify(function, "postreassociation"); 177 #endif 280 281 Z3_solver_dec_ref(ctx, solver); 282 Z3_del_context(ctx); 283 178 284 Simplifier::optimize(function); 285 179 286 return true; 180 287 } … … 183 290 * @brief processScopes 184 291 **  */ 185 inline void BooleanReassociationPass::processScopes(PabloFunction & function) { 186 function.setEntryBlock(processScopes(function, function.getEntryBlock())); 292 inline bool BooleanReassociationPass::processScopes(PabloFunction & function) { 293 PabloBlock * const entry = function.getEntryBlock(); 294 CharacterizationMap map; 295 // Map the constants and input variables 296 map.add(entry>createZeroes(), Z3_mk_false(mContext)); 297 map.add(entry>createOnes(), Z3_mk_true(mContext)); 298 for (unsigned i = 0; i < mFunction.getNumOfParameters(); ++i) { 299 map.add(mFunction.getParameter(i), makeVar()); 300 } 301 mInFile = makeVar(); 302 processScopes(entry, map); 303 return mModified; 187 304 } 188 305 … … 190 307 * @brief processScopes 191 308 **  */ 192 PabloBlock * BooleanReassociationPass::processScopes(PabloFunction & f, PabloBlock * const block) { 193 for (Statement * stmt : *block) { 194 if (If * ifNode = dyn_cast<If>(stmt)) { 195 PabloBlock * rewrittenBlock = processScopes(f, ifNode>getBody()); 196 mResolvedScopes.emplace(rewrittenBlock, stmt); 197 ifNode>setBody(rewrittenBlock); 198 } else if (While * whileNode = dyn_cast<While>(stmt)) { 199 PabloBlock * rewrittenBlock = processScopes(f, whileNode>getBody()); 200 mResolvedScopes.emplace(rewrittenBlock, stmt); 201 whileNode>setBody(rewrittenBlock); 202 } 203 } 204 return processScope(f, block); 205 } 206 207 /**  * 208 * @brief getVertex 209 **  */ 210 template<typename ValueType, typename GraphType, typename MapType> 211 static inline Vertex getVertex(const ValueType value, GraphType & G, MapType & M) { 212 const auto f = M.find(value); 213 if (f != M.end()) { 214 return f>second; 215 } 216 const auto u = add_vertex(value, G); 217 M.insert(std::make_pair(value, u)); 218 return u; 219 } 220 221 /**  * 222 * @brief writeTree 223 **  */ 224 inline PabloAST * writeTree(PabloBlock * block, const TypeId typeId, circular_buffer<PabloAST *> & Q) { 225 while (Q.size() > 1) { 226 PabloAST * e1 = Q.front(); Q.pop_front(); 227 PabloAST * e2 = Q.front(); Q.pop_front(); 228 PabloAST * expr = nullptr; 229 switch (typeId) { 230 case TypeId::And: 231 expr = block>createAnd(e1, e2); break; 232 case TypeId::Or: 233 expr = block>createOr(e1, e2); break; 234 case TypeId::Xor: 235 expr = block>createXor(e1, e2); break; 236 default: break; 237 } 238 Q.push_back(expr); 239 } 240 return Q.front(); 241 } 242 243 /**  * 244 * @brief isReachableAtEntryPoint 245 **  */ 246 bool isReachableAtEntryPoint(const PabloAST * const expr, const PabloBlock * const block) { 247 // if expr is not a statement, it's always reachable 248 if (isa<Statement>(expr)) { 249 const PabloBlock * parent = cast<Statement>(expr)>getParent(); 250 // if expr is in the current block, it's not reachable at the entry point of this block 251 if (parent == block) { 252 return false; 253 } 254 const PabloBlock * current = block>getParent(); 255 // If expr is an Assign or Next node, it must escape its block (presuming the Simplifier has eliminated any 256 // unnecessary Assign or Next nodes.) We'll want to test whether the parent of its block is an ancestor of 257 // the current block. 258 if (isa<Assign>(expr)  isa<Next>(expr)) { 259 parent = parent>getParent(); 260 } 261 // If we can find expr in a preceeding block, it's reachable 262 for (;;) { 263 if (parent == current) { 264 return true; 265 } 266 if (current == nullptr) { 267 break; 268 } 269 current = current>getParent(); 270 } 271 // otherwise it must be in a nested block and therefore unreachable 272 return false; 273 } 274 return true; 275 } 276 277 /**  * 278 * @brief createTree 279 **  */ 280 PabloAST * BooleanReassociationPass::createTree(const PabloBlock * const block, PabloBlock * const newScope, const Vertex u, Graph & G) { 281 282 flat_set<PabloAST *> internalVars; 283 284 flat_set<PabloAST *> externalVars; 285 286 assert (in_degree(u, G) > 0); 287 288 for (const auto e : make_iterator_range(in_edges(u, G))) { 289 PabloAST * const expr = getValue(G[source(e, G)]); 290 assert ("G contains a null input variable!" && (expr != nullptr)); 291 if (isReachableAtEntryPoint(expr, block)) { 292 externalVars.insert(expr); 309 void BooleanReassociationPass::processScopes(PabloBlock * const block, CharacterizationMap & map) { 310 Z3_solver_push(mContext, mSolver); 311 for (Statement * stmt = block>front(); stmt; ) { 312 if (LLVM_UNLIKELY(isa<If>(stmt))) { 313 if (LLVM_UNLIKELY(isa<Zeroes>(cast<If>(stmt)>getCondition()))) { 314 stmt = stmt>eraseFromParent(true); 315 } else { 316 CharacterizationMap nested(map); 317 processScopes(cast<If>(stmt)>getBody(), nested); 318 for (Assign * def : cast<If>(stmt)>getDefined()) { 319 map.add(def, makeVar()); 320 } 321 stmt = stmt>getNextNode(); 322 } 323 } else if (LLVM_UNLIKELY(isa<While>(stmt))) { 324 if (LLVM_UNLIKELY(isa<Zeroes>(cast<While>(stmt)>getCondition()))) { 325 stmt = stmt>eraseFromParent(true); 326 } else { 327 CharacterizationMap nested(map); 328 processScopes(cast<While>(stmt)>getBody(), nested); 329 for (Next * var : cast<While>(stmt)>getVariants()) { 330 map.add(var, makeVar()); 331 } 332 stmt = stmt>getNextNode(); 333 } 334 } else { // characterize this statement then check whether it is equivalent to any existing one. 335 stmt = characterize(stmt, map); 336 } 337 } 338 distributeScope(block, map); 339 Z3_solver_pop(mContext, mSolver, 1); 340 } 341 342 /**  * 343 * @brief characterize 344 **  */ 345 inline Statement * BooleanReassociationPass::characterize(Statement * const stmt, CharacterizationMap & map) { 346 Z3_ast node = nullptr; 347 const size_t n = stmt>getNumOperands(); assert (n > 0); 348 if (isa<Variadic>(stmt)) { 349 Z3_ast operands[n]; 350 for (size_t i = 0; i < n; ++i) { 351 operands[i] = map.get(stmt>getOperand(i)); assert (operands[i]); 352 } 353 if (isa<And>(stmt)) { 354 node = Z3_mk_and(mContext, n, operands); 355 } else if (isa<Or>(stmt)) { 356 node = Z3_mk_or(mContext, n, operands); 357 } else if (isa<Xor>(stmt)) { 358 node = Z3_mk_xor(mContext, operands[0], operands[1]); 359 for (unsigned i = 2; LLVM_UNLIKELY(i < n); ++i) { 360 node = Z3_mk_xor(mContext, node, operands[i]); 361 } 362 } 363 } else if (isa<Not>(stmt)) { 364 Z3_ast op = map.get(stmt>getOperand(0)); assert (op); 365 node = Z3_mk_not(mContext, op); 366 } else if (isa<Sel>(stmt)) { 367 Z3_ast operands[3]; 368 for (size_t i = 0; i < 3; ++i) { 369 operands[i] = map.get(stmt>getOperand(i)); assert (operands[i]); 370 } 371 node = Z3_mk_ite(mContext, operands[0], operands[1], operands[2]); 372 } else if (LLVM_UNLIKELY(isa<InFile>(stmt)  isa<AtEOF>(stmt))) { 373 assert (stmt>getNumOperands() == 1); 374 Z3_ast check[2]; 375 check[0] = map.get(stmt>getOperand(0)); assert (check[0]); 376 check[1] = isa<InFile>(stmt) ? mInFile : Z3_mk_not(mContext, mInFile); assert (check[1]); 377 node = Z3_mk_and(mContext, 2, check); 378 } else { 379 if (LLVM_UNLIKELY(isa<Assign>(stmt)  isa<Next>(stmt))) { 380 Z3_ast op = map.get(stmt>getOperand(0)); assert (op); 381 map.add(stmt, op, true); 293 382 } else { 294 internalVars.insert(expr); 295 } 296 } 297 298 circular_buffer<PabloAST *> Q(in_degree(u, G)); 299 for (auto expr : externalVars) { 300 Q.push_back(expr); 301 } 302 303 const TypeId typeId = getType(G[u]); 304 Statement * stmt = newScope>front(); 305 if (Q.size() > 1) { 306 newScope>setInsertPoint(nullptr); 307 writeTree(newScope, typeId, Q); 308 assert (Q.size() == 1); 309 } 310 311 for (unsigned distance = 0; stmt; ++distance, stmt = stmt>getNextNode()) { 312 313 if (distance > 3 && Q.size() > 1) { // write out the current Q 314 writeTree(newScope, typeId, Q); 315 assert (Q.size() == 1); 316 } 317 318 bool found = false; 319 if (isa<If>(stmt)) { 320 for (Assign * def : cast<If>(stmt)>getDefined()) { 321 if (internalVars.erase(def) != 0) { 322 assert (!Q.full()); 323 Q.push_back(def); 324 found = true; 325 } 326 } 327 } else if (isa<While>(stmt)) { 328 for (Next * var : cast<While>(stmt)>getVariants()) { 329 if (internalVars.erase(var) != 0) { 330 assert (!Q.full()); 331 Q.push_back(var); 332 found = true; 333 } 334 } 335 } else if (internalVars.erase(stmt) != 0) { 336 Q.push_back(stmt); 337 found = true; 338 } 339 340 if (found) { 341 newScope>setInsertPoint(stmt); 342 distance = 0; 343 } 344 } 345 346 assert (internalVars.empty()); 347 348 newScope>setInsertPoint(newScope>back()); 349 350 writeTree(newScope, typeId, Q); 351 assert (Q.size() == 1); 352 PabloAST * const result = Q.front(); 353 assert (result); 354 getValue(G[u]) = result; 355 356 return result; 383 map.add(stmt, makeVar()); 384 } 385 return stmt>getNextNode(); 386 } 387 node = Z3_simplify(mContext, node); assert (node); 388 PabloAST * const replacement = map.findKey(node); 389 if (LLVM_LIKELY(replacement == nullptr)) { 390 map.add(stmt, node); 391 return stmt>getNextNode(); 392 } else { 393 return stmt>replaceWith(replacement); 394 } 395 357 396 } 358 397 … … 360 399 * @brief processScope 361 400 **  */ 362 inline PabloBlock * BooleanReassociationPass::processScope(PabloFunction & f, PabloBlock * const block) {401 inline void BooleanReassociationPass::distributeScope(PabloBlock * const block, CharacterizationMap & map) { 363 402 Graph G; 364 summarizeAST(block, G); 365 redistributeAST(G); 366 return rewriteAST(f, block, G); 367 } 368 369 /**  * 370 * @brief rewriteAST 371 **  */ 372 PabloBlock * BooleanReassociationPass::rewriteAST(PabloFunction & f, PabloBlock * const originalScope, Graph & G) { 373 374 using ReadyPair = std::pair<unsigned, Vertex>; 375 using ReadySet = std::vector<ReadyPair>; 376 377 // Determine the bottomup ordering of G 378 std::vector<unsigned> ordering(num_vertices(G)); 379 circular_buffer<Vertex> Q(num_vertices(G)); 380 for (const Vertex u : make_iterator_range(vertices(G))) { 381 if (out_degree(u, G) == 0 && in_degree(u, G) != 0) { 382 ordering[u] = 1; 383 Q.push_back(u); 384 } 385 } 386 387 while (!Q.empty()) { 388 const Vertex u = Q.front(); 389 Q.pop_front(); 390 assert (ordering[u] > 0); 391 for (const auto ei : make_iterator_range(in_edges(u, G))) { 392 const Vertex v = source(ei, G); 393 if (ordering[v] == 0) { 394 unsigned weight = 0; 395 bool ready = true; 396 for (const auto ej : make_iterator_range(out_edges(v, G))) { 397 const Vertex w = target(ej, G); 398 const unsigned t = ordering[w]; 399 if (t == 0) { 400 ready = false; 401 break; 402 } 403 weight = std::max(weight, t); 404 } 405 if (ready) { 406 assert (weight < std::numeric_limits<unsigned>::max()); 407 assert (weight > 0); 408 ordering[v] = (weight + 1); 409 Q.push_back(v); 410 } 411 } 412 } 413 } 414 415 // Compute the initial ready set 416 ReadySet readySet; 417 for (const Vertex u : make_iterator_range(vertices(G))) { 418 if (in_degree(u, G) == 0 && out_degree(u, G) != 0) { 419 readySet.emplace_back(ordering[u], u); 420 } 421 } 422 423 struct { 424 bool operator()(const ReadyPair a, const ReadyPair b) { 425 return std::get<0>(a) > std::get<0>(b); 426 } 427 } readyComparator; 428 429 std::sort(readySet.begin(), readySet.end(), readyComparator); 430 431 flat_set<Vertex> tested; 432 433 PabloBlock * const newScope = PabloBlock::Create(f); 434 435 // This should hold back Assign and Next nodes then write them in after any reassociated statements 436 // are rewritten at the earliest use. 437 438 // Rewrite the AST using the bottomup ordering 439 while (!readySet.empty()) { 440 441 // Scan through the ready set to determine which one 'kills' the greatest number of inputs 442 // NOTE: the readySet is kept in sorted "distance to sink" order; thus those closest to a 443 // sink will be evaluated first. 444 double best = 0; 445 auto chosen = readySet.begin(); 446 for (auto ri = readySet.begin(); ri != readySet.end(); ++ri) { 447 const Vertex u = std::get<1>(*ri); 448 const PabloAST * const expr = getValue(G[u]); 449 if (expr && (isa<Assign>(expr)  isa<Next>(expr))) { 450 chosen = ri; 451 break; 452 } 453 double progress = 0; 454 for (auto ei : make_iterator_range(in_edges(u, G))) { 455 const auto v = source(ei, G); 456 const auto totalUsesOfIthOperand = out_degree(v, G); 457 if (LLVM_UNLIKELY(totalUsesOfIthOperand == 0)) { 458 progress += 1.0; 459 } else { 460 unsigned unscheduledUsesOfIthOperand = 0; 461 for (auto ej : make_iterator_range(out_edges(v, G))) { 462 if (ordering[target(ej, G)]) { // if this edge leads to an unscheduled statement 463 ++unscheduledUsesOfIthOperand; 464 } 465 } 466 progress += std::pow((double)(totalUsesOfIthOperand  unscheduledUsesOfIthOperand + 1) / (double)(totalUsesOfIthOperand), 2); 467 } 468 } 469 if (progress > best) { 470 chosen = ri; 471 best = progress; 472 } 473 } 474 475 Vertex u; unsigned weight; 476 std::tie(weight, u) = *chosen; 477 readySet.erase(chosen); 478 479 assert (weight > 0); 480 481 if (LLVM_LIKELY(isMutable(G[u]))) { 482 PabloAST * expr = nullptr; 483 if (isAssociative(G[u])) { 484 expr = createTree(originalScope, newScope, u, G); 485 } else { 486 expr = getValue(G[u]); 487 } 488 assert (expr); 489 for (auto e : make_iterator_range(out_edges(u, G))) { 490 if (G[e] && G[e] != expr) { 491 if (PabloAST * user = getValue(G[target(e, G)])) { 492 cast<Statement>(user)>replaceUsesOfWith(G[e], expr); 493 } 494 } 495 } 496 // Make sure that optimization doesn't reduce this to an already written statement 497 if (LLVM_LIKELY(isa<Statement>(expr) && cast<Statement>(expr)>getParent() == originalScope)) { 498 newScope>insert(cast<Statement>(expr)); 499 } 500 } 501 502 // mark this instruction as written 503 ordering[u] = 0; 504 // Now check whether any new instructions are ready 505 for (auto ei : make_iterator_range(out_edges(u, G))) { 506 bool ready = true; 507 const auto v = target(ei, G); 508 // since G may be a multigraph, we need to check whether we've already tested v 509 if (tested.insert(v).second) { 510 for (auto ej : make_iterator_range(in_edges(v, G))) { 511 if (ordering[source(ej, G)]) { 512 ready = false; 513 break; 514 } 515 } 516 if (ready) { 517 auto entry = std::make_pair(ordering[v], v); 518 auto position = std::lower_bound(readySet.begin(), readySet.end(), entry, readyComparator); 519 readySet.insert(position, entry); 520 assert (std::is_sorted(readySet.cbegin(), readySet.cend(), readyComparator)); 521 } 522 } 523 } 524 tested.clear(); 525 } 526 originalScope>eraseFromParent(); 527 return newScope; 403 try { 404 transformAST(block, map, G); 405 } catch (std::runtime_error err) { 406 printGraph(G, "G"); 407 throw err; 408 } 528 409 } 529 410 … … 534 415 * are "flattened" (i.e., allowed to have any number of inputs.) 535 416 **  */ 536 void BooleanReassociationPass:: summarizeAST(PabloBlock * const block, Graph & G) const{537 Map M;417 void BooleanReassociationPass::transformAST(PabloBlock * const block, CharacterizationMap & C, Graph & G) { 418 StatementMap S; 538 419 // Compute the base defuse graph ... 539 420 for (Statement * stmt : *block) { 540 const Vertex u = getSummaryVertex(stmt, G, M, block); 541 for (unsigned i = 0; i != stmt>getNumOperands(); ++i) { 421 422 const Vertex u = makeVertex(stmt>getClassTypeId(), stmt, S, G, C.get(stmt)); 423 424 for (unsigned i = 0; i < stmt>getNumOperands(); ++i) { 542 425 PabloAST * const op = stmt>getOperand(i); 543 if (LLVM_UNLIKELY(isa<Integer>(op)  isa<String>(op))) { 544 continue; 545 } 546 const Vertex v = getSummaryVertex(op, G, M, block); 547 add_edge(op, v, u, G); 548 // If this operand is a Not operation that is not in this PabloBlock, 549 // pull its input operand in. It may lead to future optimizations. 550 if (LLVM_UNLIKELY(isa<Not>(op) && !inCurrentBlock(cast<Not>(op), block))) { 551 PabloAST * const negatedValue = cast<Not>(op)>getExpr(); 552 add_edge(negatedValue, getSummaryVertex(negatedValue, G, M, block), v, G); 553 } 554 } 555 if (isa<If>(stmt)) { 426 if (LLVM_LIKELY(isa<Statement>(op)  isa<Var>(op))) { 427 add_edge(op, makeVertex(TypeId::Var, op, C, S, G), u, G); 428 } 429 } 430 431 if (LLVM_UNLIKELY(isa<If>(stmt))) { 556 432 for (Assign * def : cast<const If>(stmt)>getDefined()) { 557 const Vertex v = getSummaryVertex(def, G, M, block);433 const Vertex v = makeVertex(TypeId::Var, def, C, S, G); 558 434 add_edge(def, u, v, G); 559 resolveNestedUsages( v, def, block, G, M, stmt);560 } 561 } else if ( isa<While>(stmt)) {435 resolveNestedUsages(block, def, v, C, S, G, stmt); 436 } 437 } else if (LLVM_UNLIKELY(isa<While>(stmt))) { 562 438 // To keep G a DAG, we need to do a bit of surgery on loop variants because 563 439 // the next variables it produces can be used within the condition. Instead, … … 565 441 // the Next node dependent on the loop. 566 442 for (Next * var : cast<const While>(stmt)>getVariants()) { 567 const Vertex v = getSummaryVertex(var, G, M, block);443 const Vertex v = makeVertex(TypeId::Var, var, C, S, G); 568 444 assert (in_degree(v, G) == 1); 569 add_edge(nullptr, source(first(in_edges(v, G)), G), u, G); 445 auto e = first(in_edges(v, G)); 446 add_edge(G[e], source(e, G), u, G); 570 447 remove_edge(v, u, G); 571 448 add_edge(var, u, v, G); 572 resolveNestedUsages(v, var, block, G, M, stmt); 573 } 574 } else { 575 resolveNestedUsages(u, stmt, block, G, M); 576 } 577 } 578 std::vector<Vertex> mapping(num_vertices(G)); 579 summarizeGraph(G, mapping); 449 resolveNestedUsages(block, var, v, C, S, G, stmt); 450 } 451 } else { 452 resolveNestedUsages(block, stmt, u, C, S, G, stmt); 453 } 454 } 455 456 if (redistributeGraph(C, S, G)) { 457 factorGraph(G); 458 rewriteAST(block, G); 459 mModified = true; 460 } 461 580 462 } 581 463 … … 583 465 * @brief resolveNestedUsages 584 466 **  */ 585 void BooleanReassociationPass::resolveNestedUsages(const Vertex u, PabloAST * expr, PabloBlock * const block, Graph & G, Map & M, const Statement * const ignoreIfThis) const { 586 for (PabloAST * user : expr>users()) { 587 assert (user); 467 void BooleanReassociationPass::resolveNestedUsages(PabloBlock * const block, PabloAST * const expr, const Vertex u, 468 CharacterizationMap & C, StatementMap & S, Graph & G, 469 const Statement * const ignoreIfThis) const { 470 assert ("Cannot resolve nested usages of a null expression!" && expr); 471 for (PabloAST * user : expr>users()) { assert (user); 588 472 if (LLVM_LIKELY(user != expr && isa<Statement>(user))) { 589 PabloBlock * parent = cast<Statement>(user)>getParent(); 590 assert (parent); 473 PabloBlock * parent = cast<Statement>(user)>getParent(); assert (parent); 591 474 if (LLVM_UNLIKELY(parent != block)) { 592 475 for (;;) { 476 if (parent>getParent() == block) { 477 Statement * const branch = parent>getBranch(); 478 if (LLVM_UNLIKELY(branch != ignoreIfThis)) { 479 // Add in a Var denoting the user of this expression so that it can be updated if expr changes. 480 const Vertex v = makeVertex(TypeId::Var, user, C, S, G); 481 add_edge(expr, u, v, G); 482 const Vertex w = makeVertex(branch>getClassTypeId(), branch, S, G); 483 add_edge(user, v, w, G); 484 } 485 break; 486 } 487 parent = parent>getParent(); 593 488 if (LLVM_UNLIKELY(parent == nullptr)) { 594 489 assert (isa<Assign>(expr)  isa<Next>(expr)); 595 490 break; 596 } else if (parent>getParent() == block) { 597 const auto f = mResolvedScopes.find(parent); 598 if (LLVM_UNLIKELY(f == mResolvedScopes.end())) { 599 throw std::runtime_error("Failed to resolve scope block!"); 600 } 601 Statement * const branch = f>second; 602 if (LLVM_UNLIKELY(branch == ignoreIfThis)) { 603 break; 604 } 605 // Add in a Var denoting the user of this expression so that it can be updated if expr changes. 606 const Vertex v = getSummaryVertex(user, G, M, block); 607 add_edge(expr, u, v, G); 608 609 const Vertex w = getSummaryVertex(branch, G, M, block); 610 add_edge(nullptr, v, w, G); 611 break; 612 } 613 parent = parent>getParent(); 614 } 615 } 616 } 617 } 618 } 619 620 /**  * 621 * @brief summarizeGraph 622 **  */ 623 inline void BooleanReassociationPass::summarizeGraph(Graph & G, std::vector<Vertex> & mapping) { 624 std::vector<Vertex> reverse_topological_ordering; 625 reverse_topological_ordering.reserve(num_vertices(G)); 626 627 topological_sort(G, std::back_inserter(reverse_topological_ordering)); 628 assert(mapping.size() >= num_vertices(G)); 629 for (const Vertex u : reverse_topological_ordering) { 630 if (in_degree(u, G) == 0 && out_degree(u, G) == 0) { 631 continue; 632 } else if (LLVM_LIKELY(out_degree(u, G) > 0)) { 633 if (isAssociative(G[u])) { 634 if (LLVM_UNLIKELY(in_degree(u, G) == 1)) { 635 // We have a redundant node here that'll simply end up being a duplicate 636 // of the input value. Remove it and add any of its outgoing edges to its 637 // input node. 638 const auto ei = first(in_edges(u, G)); 639 const Vertex v = source(ei, G); 640 for (auto ej : make_iterator_range(out_edges(u, G))) { 641 const Vertex w = target(ej, G); 642 add_edge(G[ei], v, w, G); 643 if (mapping[w] == mapping[u]) { 644 mapping[w] = v; 645 } 646 } 647 mapping[u] = v; 648 clear_vertex(u, G); 649 getType(G[u]) = TypeId::Var; 650 getValue(G[u]) = nullptr; 651 continue; 652 } else if (LLVM_UNLIKELY(out_degree(u, G) == 1)) { 653 // Otherwise if we have a single user, we have a similar case as above but 654 // we can only merge this vertex into the outgoing instruction if they are 655 // of the same type. 656 const auto ei = first(out_edges(u, G)); 657 const Vertex v = target(ei, G); 658 if (LLVM_UNLIKELY(isSameType(G[v], G[u]))) { 659 for (auto ej : make_iterator_range(in_edges(u, G))) { 660 add_edge(G[ei], source(ej, G), v, G); 661 } 662 mapping[u] = v; 663 clear_vertex(u, G); 664 getType(G[u]) = TypeId::Var; 665 getValue(G[u]) = nullptr; 666 continue; 667 } 668 } 669 } 670 } else if (isNonEscaping(G[u])) { 671 clear_in_edges(u, G); 672 getType(G[u]) = TypeId::Var; 673 getValue(G[u]) = nullptr; 674 continue; 675 } 676 } 677 } 491 } 492 } 493 } 494 } 495 } 496 } 497 498 678 499 679 500 /**  * … … 691 512 for (auto u : A) { 692 513 if (in_degree(u, G) > 0) { 693 VertexSet incomingAdjacencies;694 incomingAdjacencies.reserve(in_degree(u, G));514 VertexSet adjacencies; 515 adjacencies.reserve(in_degree(u, G)); 695 516 for (auto e : make_iterator_range(in_edges(u, G))) { 696 incomingAdjacencies.push_back(source(e, G)); 697 } 698 std::sort(incomingAdjacencies.begin(), incomingAdjacencies.end()); 699 B1.insert(std::move(incomingAdjacencies)); 517 adjacencies.push_back(source(e, G)); 518 } 519 std::sort(adjacencies.begin(), adjacencies.end()); 520 assert(std::unique(adjacencies.begin(), adjacencies.end()) == adjacencies.end()); 521 B1.insert(std::move(adjacencies)); 700 522 } 701 523 } … … 749 571 } 750 572 std::sort(Aj.begin(), Aj.end()); 573 assert(std::unique(Aj.begin(), Aj.end()) == Aj.end()); 751 574 VertexSet Ak; 752 575 Ak.reserve(std::min(Ai.size(), Aj.size())); … … 821 644 * there are not enough vertices in the biclique to make distribution profitable, eliminate the clique. 822 645 **  */ 823 static BicliqueSet && removeUnhelpfulBicliques(BicliqueSet && cliques, const DependencyGraph & G, DistributionGraph & H) {646 static BicliqueSet && removeUnhelpfulBicliques(BicliqueSet && cliques, const Graph & G, DistributionGraph & H) { 824 647 for (auto ci = cliques.begin(); ci != cliques.end(); ) { 825 648 const auto cardinalityA = std::get<0>(*ci).size(); … … 844 667 * @brief safeDistributionSets 845 668 **  */ 846 static DistributionSets safeDistributionSets(const DependencyGraph & G, DistributionGraph & H) {669 static DistributionSets safeDistributionSets(const Graph & G, DistributionGraph & H) { 847 670 848 671 VertexSet sinks; … … 866 689 867 690 /**  * 691 * @brief getVertex 692 **  */ 693 template<typename ValueType, typename GraphType, typename MapType> 694 static inline Vertex getVertex(const ValueType value, GraphType & G, MapType & M) { 695 const auto f = M.find(value); 696 if (f != M.end()) { 697 return f>second; 698 } 699 const auto u = add_vertex(value, G); 700 M.insert(std::make_pair(value, u)); 701 return u; 702 } 703 704 /**  * 868 705 * @brief generateDistributionGraph 869 706 **  */ 870 void generateDistributionGraph(const DependencyGraph & G, DistributionGraph & H) {707 void generateDistributionGraph(const Graph & G, DistributionGraph & H) { 871 708 DistributionMap M; 872 709 for (const Vertex u : make_iterator_range(vertices(G))) { … … 893 730 } 894 731 if (LLVM_LIKELY(distributable.size() > 1)) { 895 // We're only interested in computing a subgraph of G in which every source has an outdegree 896 // greater than 1. Otherwise we'd only end up permuting the AND/OR sequence with no logical 897 // benefit. (Note: this does not consider register pressure / liveness.) 898 flat_map<Vertex, bool> observedMoreThanOnce; 899 bool anyOpportunities = false; 732 flat_set<Vertex> observed; 900 733 for (const Vertex v : distributable) { 901 734 for (auto e : make_iterator_range(in_edges(v, G))) { 902 const Vertex w = source(e, G); 903 auto ob = observedMoreThanOnce.find(w); 904 if (ob == observedMoreThanOnce.end()) { 905 observedMoreThanOnce.emplace(w, false); 906 } else { 907 ob>second = true; 908 anyOpportunities = true; 909 } 910 } 911 } 912 if (anyOpportunities) { 913 for (const auto ob : observedMoreThanOnce) { 914 if (std::get<1>(ob)) { 915 const Vertex w = std::get<0>(ob); 916 for (auto e : make_iterator_range(out_edges(w, G))) { 917 const Vertex v = target(e, G); 918 if (distributable.count(v)) { 919 const Vertex y = getVertex(v, H, M); 920 add_edge(y, getVertex(u, H, M), H); 921 add_edge(getVertex(w, H, M), y, H); 922 } 923 } 735 const auto v = source(e, G); 736 observed.insert(v); 737 } 738 } 739 for (const Vertex w : observed) { 740 for (auto e : make_iterator_range(out_edges(w, G))) { 741 const Vertex v = target(e, G); 742 if (distributable.count(v)) { 743 const Vertex y = getVertex(v, H, M); 744 boost::add_edge(y, getVertex(u, H, M), H); 745 boost::add_edge(getVertex(w, H, M), y, H); 924 746 } 925 747 } … … 935 757 * Apply the distribution law to reduce computations whenever possible. 936 758 **  */ 937 void BooleanReassociationPass::redistributeAST(Graph & G) const { 938 939 std::vector<Vertex> mapping(num_vertices(G) + 16); 940 std::iota(mapping.begin(), mapping.end(), 0); // 0,1,.....n 759 bool BooleanReassociationPass::redistributeGraph(CharacterizationMap & C, StatementMap & M, Graph & G) const { 760 761 bool modified = false; 762 763 DistributionGraph H; 764 765 contractGraph(M, G); 941 766 942 767 for (;;) { 943 768 944 DistributionGraph H; 945 946 generateDistributionGraph(G, H); 947 948 // If we found no potential opportunities then we cannot apply the distribution law to any part of G. 949 if (num_vertices(H) == 0) { 769 for (;;) { 770 771 generateDistributionGraph(G, H); 772 773 // If we found no potential opportunities then we cannot apply the distribution law to any part of G. 774 if (num_vertices(H) == 0) { 775 break; 776 } 777 778 const DistributionSets distributionSets = safeDistributionSets(G, H); 779 780 if (LLVM_UNLIKELY(distributionSets.empty())) { 781 break; 782 } 783 784 modified = true; 785 786 for (const DistributionSet & set : distributionSets) { 787 788 // Each distribution tuple consists of the sources, intermediary, and sink nodes. 789 const VertexSet & sources = std::get<0>(set); 790 const VertexSet & intermediary = std::get<1>(set); 791 const VertexSet & sinks = std::get<2>(set); 792 793 const TypeId outerTypeId = getType(G[H[sinks.front()]]); 794 assert (outerTypeId == TypeId::And  outerTypeId == TypeId::Or); 795 const TypeId innerTypeId = (outerTypeId == TypeId::Or) ? TypeId::And : TypeId::Or; 796 797 const Vertex x = makeVertex(outerTypeId, nullptr, G); 798 const Vertex y = makeVertex(innerTypeId, nullptr, G); 799 800 // Update G to reflect the distributed operations (including removing the subgraph of 801 // the tobe distributed edges.) 802 803 add_edge(nullptr, x, y, G); 804 805 for (const Vertex i : sources) { 806 const auto u = H[i]; 807 for (const Vertex j : intermediary) { 808 const auto v = H[j]; 809 const auto e = edge(u, v, G); assert (e.second); 810 remove_edge(e.first, G); 811 } 812 add_edge(nullptr, u, y, G); 813 } 814 815 for (const Vertex i : intermediary) { 816 const auto u = H[i]; 817 for (const Vertex j : sinks) { 818 const auto v = H[j]; 819 const auto e = edge(u, v, G); assert (e.second); 820 add_edge(G[e.first], y, v, G); 821 remove_edge(e.first, G); 822 } 823 add_edge(nullptr, u, x, G); 824 getDefinition(G[u]) = nullptr; 825 } 826 827 } 828 829 H.clear(); 830 831 contractGraph(M, G); 832 } 833 834 // Although exceptionally unlikely, it's possible that if we can reduce the graph, we could 835 // further simplify it. Restart the process if and only if we succeed. 836 if (LLVM_UNLIKELY(reduceGraph(C, M, G))) { 837 if (LLVM_UNLIKELY(contractGraph(M, G))) { 838 H.clear(); 839 continue; 840 } 841 } 842 843 break; 844 } 845 846 return modified; 847 } 848 849 /**  * 850 * @brief isNonEscaping 851 **  */ 852 inline bool isNonEscaping(const VertexData & data) { 853 // If these are redundant, the Simplifier pass will eliminate them. Trust that they're necessary. 854 switch (getType(data)) { 855 case TypeId::Assign: 856 case TypeId::Next: 857 case TypeId::If: 858 case TypeId::While: 859 case TypeId::Count: 860 return false; 861 default: 862 return true; 863 } 864 } 865 866 /**  * 867 * @brief contractGraph 868 **  */ 869 bool BooleanReassociationPass::contractGraph(StatementMap & M, Graph & G) const { 870 871 bool contracted = false; 872 873 circular_buffer<Vertex> ordering(num_vertices(G)); 874 875 topological_sort(G, std::back_inserter(ordering)); // reverse topological ordering 876 877 // first contract the graph 878 for (const Vertex u : ordering) { 879 if (in_degree(u, G) == 0 && out_degree(u, G) == 0) { 880 continue; 881 } else if (LLVM_LIKELY(out_degree(u, G) > 0)) { 882 if (isAssociative(G[u])) { 883 if (LLVM_UNLIKELY(in_degree(u, G) == 1)) { 884 // We have a redundant node here that'll simply end up being a duplicate 885 // of the input value. Remove it and add any of its outgoing edges to its 886 // input node. 887 const auto ei = first(in_edges(u, G)); 888 const Vertex v = source(ei, G); 889 for (auto ej : make_iterator_range(out_edges(u, G))) { 890 const Vertex w = target(ej, G); 891 add_edge(G[ei], v, w, G); 892 } 893 removeVertex(u, M, G); 894 contracted = true; 895 } else if (LLVM_UNLIKELY(out_degree(u, G) == 1)) { 896 // Otherwise if we have a single user, we have a similar case as above but 897 // we can only merge this vertex into the outgoing instruction if they are 898 // of the same type. 899 const auto ei = first(out_edges(u, G)); 900 const Vertex v = target(ei, G); 901 if (LLVM_UNLIKELY(getType(G[v]) == getType(G[u]))) { 902 for (auto ej : make_iterator_range(in_edges(u, G))) { 903 add_edge(G[ei], source(ej, G), v, G); 904 } 905 removeVertex(u, M, G); 906 contracted = true; 907 } 908 } 909 } 910 } else if (LLVM_UNLIKELY(isNonEscaping(G[u]))) { 911 removeVertex(u, M, G); 912 contracted = true; 913 } 914 } 915 return contracted; 916 } 917 918 /**  * 919 * @brief isReducible 920 **  */ 921 inline bool isReducible(const VertexData & data) { 922 switch (getType(data)) { 923 case TypeId::Var: 924 case TypeId::If: 925 case TypeId::While: 926 return false; 927 default: 928 return true; 929 } 930 } 931 932 /**  * 933 * @brief reduceGraph 934 **  */ 935 bool BooleanReassociationPass::reduceGraph(CharacterizationMap & C, StatementMap & S, Graph & G) const { 936 937 bool reduced = false; 938 939 VertexMap M; 940 circular_buffer<Vertex> ordering(num_vertices(G)); 941 942 topological_sort(G, std::front_inserter(ordering)); // topological ordering 943 944 // first contract the graph 945 for (const Vertex u : ordering) { 946 if (isReducible(G[u])) { 947 Z3_ast & node = getDefinition(G[u]); 948 if (isAssociative(G[u])) { 949 const TypeId typeId = getType(G[u]); 950 if (node == nullptr) { 951 const auto n = in_degree(u, G); assert (n > 1); 952 Z3_ast operands[n]; 953 unsigned i = 0; 954 for (auto e : make_iterator_range(in_edges(u, G))) { 955 const Vertex v = source(e, G); 956 assert (getDefinition(G[v])); 957 operands[i++] = getDefinition(G[v]); 958 } 959 switch (typeId) { 960 case TypeId::And: 961 node = Z3_mk_and(mContext, n, operands); 962 break; 963 case TypeId::Or: 964 node = Z3_mk_or(mContext, n, operands); 965 break; 966 case TypeId::Xor: 967 node = Z3_mk_xor(mContext, operands[0], operands[1]); 968 for (unsigned i = 2; LLVM_UNLIKELY(i < n); ++i) { 969 node = Z3_mk_xor(mContext, node, operands[i]); 970 } 971 break; 972 default: llvm_unreachable("unexpected type id"); 973 } 974 975 assert (node); 976 node = Z3_simplify(mContext, node); 977 } 978 graph_traits<Graph>::in_edge_iterator begin, end; 979 restart: if (in_degree(u, G) > 1) { 980 std::tie(begin, end) = in_edges(u, G); 981 for (auto i = begin; ++i != end; ) { 982 const auto v = source(*i, G); 983 for (auto j = begin; j != i; ++j) { 984 const auto w = source(*j, G); 985 Z3_ast operands[2] = { getDefinition(G[v]), getDefinition(G[w]) }; 986 assert (operands[0]); 987 assert (operands[1]); 988 Z3_ast test = nullptr; 989 switch (typeId) { 990 case TypeId::And: 991 test = Z3_mk_and(mContext, 2, operands); break; 992 case TypeId::Or: 993 test = Z3_mk_or(mContext, 2, operands); break; 994 case TypeId::Xor: 995 test = Z3_mk_xor(mContext, operands[0], operands[1]); break; 996 default: 997 llvm_unreachable("impossible type id"); 998 } 999 assert (test); 1000 test = Z3_simplify(mContext, test); 1001 PabloAST * const factor = C.findKey(test); 1002 if (LLVM_UNLIKELY(factor != nullptr)) { 1003 const Vertex a = makeVertex(TypeId::Var, factor, S, G, test); 1004 // note: unless both edges carry an Pablo AST replacement value, they will converge into a single edge. 1005 PabloAST * const r1 = G[*i]; 1006 PabloAST * const r2 = G[*j]; 1007 1008 remove_edge(*i, G); 1009 remove_edge(*j, G); 1010 1011 if (LLVM_UNLIKELY(r1 && r2)) { 1012 add_edge(r1, a, u, G); 1013 add_edge(r2, a, u, G); 1014 } else { 1015 add_edge(r1 ? r1 : r2, a, u, G); 1016 } 1017 1018 // errs() << "  subsituting (" << a << ',' << u << ")=" << Z3_ast_to_string(mContext, test) 1019 // << " for (" << v << ',' << u << ")=" << Z3_ast_to_string(mContext, getDefinition(G[v])); 1020 1021 // switch (typeId) { 1022 // case TypeId::And: 1023 // errs() << " â§ "; break; 1024 // case TypeId::Or: 1025 // errs() << " âš "; break; 1026 // case TypeId::Xor: 1027 // errs() << " â "; break; 1028 // default: 1029 // llvm_unreachable("impossible type id"); 1030 // } 1031 1032 // errs() << "(" << w << ',' << u << ")=" << Z3_ast_to_string(mContext, getDefinition(G[w])) 1033 // << "\n"; 1034 1035 reduced = true; 1036 goto restart; 1037 } 1038 } 1039 } 1040 } 1041 } 1042 1043 if (LLVM_UNLIKELY(node == nullptr)) { 1044 throw std::runtime_error("No Z3 characterization for vertex " + std::to_string(u)); 1045 } 1046 1047 auto f = M.find(node); 1048 if (LLVM_LIKELY(f == M.end())) { 1049 M.emplace(node, u); 1050 } else if (isAssociative(G[u])) { 1051 const Vertex v = f>second; 1052 1053 // errs() << "  subsituting " << u << ":=\n" << Z3_ast_to_string(mContext, getDefinition(G[u])) 1054 // << "\n for " << v << ":=\n" << Z3_ast_to_string(mContext, getDefinition(G[v])) << "\n"; 1055 1056 for (auto e : make_iterator_range(out_edges(u, G))) { 1057 add_edge(G[e], v, target(e, G), G); 1058 } 1059 removeVertex(u, S, G); 1060 reduced = true; 1061 } 1062 } 1063 } 1064 return reduced; 1065 } 1066 1067 /**  * 1068 * @brief factorGraph 1069 **  */ 1070 bool BooleanReassociationPass::factorGraph(const TypeId typeId, Graph & G, std::vector<Vertex> & factors) const { 1071 1072 if (LLVM_UNLIKELY(factors.empty())) { 1073 return false; 1074 } 1075 1076 std::vector<Vertex> I, J, K; 1077 1078 bool modified = false; 1079 1080 for (auto i = factors.begin(); ++i != factors.end(); ) { 1081 assert (getType(G[*i]) == typeId); 1082 for (auto ei : make_iterator_range(in_edges(*i, G))) { 1083 I.push_back(source(ei, G)); 1084 } 1085 std::sort(I.begin(), I.end()); 1086 for (auto j = factors.begin(); j != i; ++j) { 1087 for (auto ej : make_iterator_range(in_edges(*j, G))) { 1088 J.push_back(source(ej, G)); 1089 } 1090 std::sort(J.begin(), J.end()); 1091 // get the pairwise intersection of each set of inputs (i.e., their common subexpression) 1092 std::set_intersection(I.begin(), I.end(), J.begin(), J.end(), std::back_inserter(K)); 1093 assert (std::is_sorted(K.begin(), K.end())); 1094 // if the intersection contains at least two elements 1095 const auto n = K.size(); 1096 if (n > 1) { 1097 Vertex a = *i; 1098 Vertex b = *j; 1099 if (LLVM_UNLIKELY(in_degree(a, G) == n  in_degree(b, G) == n)) { 1100 if (in_degree(a, G) != n) { 1101 assert (in_degree(b, G) == n); 1102 std::swap(a, b); 1103 } 1104 assert (in_degree(a, G) == n); 1105 if (in_degree(b, G) == n) { 1106 for (auto e : make_iterator_range(out_edges(b, G))) { 1107 add_edge(G[e], a, target(e, G), G); 1108 } 1109 removeVertex(b, G); 1110 } else { 1111 for (auto u : K) { 1112 remove_edge(u, b, G); 1113 } 1114 add_edge(nullptr, a, b, G); 1115 } 1116 } else { 1117 Vertex v = makeVertex(typeId, nullptr, G); 1118 for (auto u : K) { 1119 remove_edge(u, a, G); 1120 remove_edge(u, b, G); 1121 add_edge(nullptr, u, v, G); 1122 } 1123 add_edge(nullptr, v, a, G); 1124 add_edge(nullptr, v, b, G); 1125 factors.push_back(v); 1126 } 1127 modified = true; 1128 } 1129 K.clear(); 1130 J.clear(); 1131 } 1132 I.clear(); 1133 } 1134 return modified; 1135 } 1136 1137 /**  * 1138 * @brief factorGraph 1139 **  */ 1140 bool BooleanReassociationPass::factorGraph(Graph & G) const { 1141 // factor the associative vertices. 1142 std::vector<Vertex> factors; 1143 bool factored = false; 1144 for (unsigned i = 0; i < 3; ++i) { 1145 TypeId typeId[3] = { TypeId::And, TypeId::Or, TypeId::Xor}; 1146 for (auto j : make_iterator_range(vertices(G))) { 1147 if (getType(G[j]) == typeId[i]) { 1148 factors.push_back(j); 1149 } 1150 } 1151 if (factorGraph(typeId[i], G, factors)) { 1152 factored = true; 1153 } 1154 factors.clear(); 1155 } 1156 return factored; 1157 } 1158 1159 1160 inline bool isMutable(const Vertex u, const Graph & G) { 1161 return getType(G[u]) != TypeId::Var; 1162 } 1163 1164 /**  * 1165 * @brief rewriteAST 1166 **  */ 1167 void BooleanReassociationPass::rewriteAST(PabloBlock * const block, Graph & G) { 1168 1169 using line_t = long long int; 1170 1171 enum : line_t { MAX_INT = std::numeric_limits<line_t>::max() }; 1172 1173 Z3_config cfg = Z3_mk_config(); 1174 Z3_set_param_value(cfg, "MODEL", "true"); 1175 Z3_context ctx = Z3_mk_context(cfg); 1176 Z3_del_config(cfg); 1177 Z3_solver solver = Z3_mk_solver(ctx); 1178 Z3_solver_inc_ref(ctx, solver); 1179 1180 std::vector<Z3_ast> mapping(num_vertices(G), nullptr); 1181 1182 flat_map<PabloAST *, Z3_ast> M; 1183 1184 // Generate the variables 1185 const auto ty = Z3_mk_int_sort(ctx); 1186 Z3_ast ZERO = Z3_mk_int(ctx, 0, ty); 1187 1188 for (const Vertex u : make_iterator_range(vertices(G))) { 1189 const auto var = Z3_mk_fresh_const(ctx, nullptr, ty); 1190 Z3_ast constraint = nullptr; 1191 if (in_degree(u, G) == 0) { 1192 constraint = Z3_mk_eq(ctx, var, ZERO); 1193 } else { 1194 constraint = Z3_mk_gt(ctx, var, ZERO); 1195 } 1196 Z3_solver_assert(ctx, solver, constraint); 1197 1198 PabloAST * const expr = getValue(G[u]); 1199 if (expr) { 1200 const bool added = M.emplace(expr, var).second; 1201 assert ("G contains duplicate vertices for the same statement!" && added); 1202 } 1203 mapping[u] = var; 1204 } 1205 1206 // Add in the dependency constraints 1207 for (const Vertex u : make_iterator_range(vertices(G))) { 1208 Z3_ast const t = mapping[u]; 1209 for (auto e : make_iterator_range(in_edges(u, G))) { 1210 Z3_ast const s = mapping[source(e, G)]; 1211 Z3_solver_assert(ctx, solver, Z3_mk_lt(ctx, s, t)); 1212 } 1213 } 1214 1215 // Compute the soft ordering constraints 1216 std::vector<Z3_ast> ordering(0); 1217 ordering.reserve(2 * M.size()  1); 1218 1219 Z3_ast prior = nullptr; 1220 unsigned gap = 1; 1221 for (Statement * stmt : *block) { 1222 auto f = M.find(stmt); 1223 if (f != M.end()) { 1224 Z3_ast const node = f>second; 1225 if (prior) { 1226 ordering.push_back(Z3_mk_lt(ctx, prior, node)); 1227 Z3_ast ops[2] = { node, prior }; 1228 ordering.push_back(Z3_mk_le(ctx, Z3_mk_sub(ctx, 2, ops), Z3_mk_int(ctx, gap, ty))); 1229 } else { 1230 ordering.push_back(Z3_mk_eq(ctx, node, Z3_mk_int(ctx, gap, ty))); 1231 1232 } 1233 prior = node; 1234 gap = 0; 1235 } 1236 ++gap; 1237 } 1238 1239 if (LLVM_UNLIKELY(maxsat(ctx, solver, ordering) < 0)) { 1240 throw std::runtime_error("Unable to construct a topological ordering during reassociation!"); 1241 } 1242 1243 Z3_model model = Z3_solver_get_model(ctx, solver); 1244 Z3_model_inc_ref(ctx, model); 1245 1246 std::vector<Vertex> S(0); 1247 S.reserve(num_vertices(G)); 1248 1249 std::vector<line_t> L(num_vertices(G)); 1250 1251 1252 1253 for (const Vertex u : make_iterator_range(vertices(G))) { 1254 line_t line = LoadEarly ? 0 : MAX_INT; 1255 if (isMutable(u, G)) { 1256 Z3_ast value; 1257 if (LLVM_UNLIKELY(Z3_model_eval(ctx, model, mapping[u], Z3_L_TRUE, &value) != Z3_L_TRUE)) { 1258 throw std::runtime_error("Unexpected Z3 error when attempting to obtain value from model!"); 1259 } 1260 if (LLVM_UNLIKELY(Z3_get_numeral_int64(ctx, value, &line) != Z3_L_TRUE)) { 1261 throw std::runtime_error("Unexpected Z3 error when attempting to convert model value to integer!"); 1262 } 1263 S.push_back(u); 1264 } 1265 L[u] = line; 1266 } 1267 1268 Z3_model_dec_ref(ctx, model); 1269 1270 std::sort(S.begin(), S.end(), [&L](const Vertex u, const Vertex v){ return L[u] < L[v]; }); 1271 1272 block>setInsertPoint(nullptr); 1273 1274 std::vector<Vertex> T; 1275 1276 line_t count = 1; 1277 1278 for (auto u : S) { 1279 PabloAST *& stmt = getValue(G[u]); 1280 1281 assert (isMutable(u, G)); 1282 assert (L[u] > 0 && L[u] < MAX_INT); 1283 1284 if (isAssociative(G[u])) { 1285 1286 if (in_degree(u, G) == 0  out_degree(u, G) == 0) { 1287 throw std::runtime_error("Vertex " + std::to_string(u) + " is either a source or sink node but marked as associative!"); 1288 } 1289 1290 Statement * ip = block>getInsertPoint(); 1291 ip = ip ? ip>getNextNode() : block>front(); 1292 1293 const auto typeId = getType(G[u]); 1294 1295 T.reserve(in_degree(u, G)); 1296 for (const auto e : make_iterator_range(in_edges(u, G))) { 1297 T.push_back(source(e, G)); 1298 } 1299 1300 // Then sort them by their line position (noting any incoming value will either be 0 or MAX_INT) 1301 std::sort(T.begin(), T.end(), [&L](const Vertex u, const Vertex v){ return L[u] < L[v]; }); 1302 if (LoadEarly) { 1303 block>setInsertPoint(nullptr); 1304 } 1305 1306 circular_buffer<PabloAST *> Q(2); // in_degree(u, G)); 1307 for (auto u : T) { 1308 PabloAST * expr = getValue(G[u]); 1309 if (LLVM_UNLIKELY(expr == nullptr)) { 1310 throw std::runtime_error("Vertex " + std::to_string(u) + " does not have an expression!"); 1311 } 1312 Q.push_back(expr); 1313 if (Q.size() > 1) { 1314 1315 PabloAST * e1 = Q.front(); Q.pop_front(); 1316 PabloAST * e2 = Q.front(); Q.pop_front(); 1317 1318 if (in_degree(u, G) > 0) { 1319 if (LLVM_UNLIKELY(!dominates(e1, e2))) { 1320 std::string tmp; 1321 raw_string_ostream out(tmp); 1322 out << "e1: "; 1323 PabloPrinter::print(e1, out); 1324 out << " does not dominate e2: "; 1325 PabloPrinter::print(e2, out); 1326 throw std::runtime_error(out.str()); 1327 } 1328 assert (dominates(e1, e2)); 1329 assert (dominates(e2, ip)); 1330 Statement * dom = cast<Statement>(expr); 1331 for (;;) { 1332 PabloBlock * const parent = dom>getParent(); 1333 if (parent == block) { 1334 block>setInsertPoint(dom); 1335 break; 1336 } 1337 dom = parent>getBranch(); assert(dom); 1338 } 1339 assert (dominates(dom, ip)); 1340 } 1341 1342 switch (typeId) { 1343 case TypeId::And: 1344 expr = block>createAnd(e1, e2); break; 1345 case TypeId::Or: 1346 expr = block>createOr(e1, e2); break; 1347 case TypeId::Xor: 1348 expr = block>createXor(e1, e2); break; 1349 default: break; 1350 } 1351 Q.push_front(expr); 1352 } 1353 } 1354 1355 assert (Q.size() == 1); 1356 1357 T.clear(); 1358 1359 block>setInsertPoint(ip>getPrevNode()); 1360 1361 PabloAST * const replacement = Q.front(); assert (replacement); 1362 for (auto e : make_iterator_range(out_edges(u, G))) { 1363 if (G[e]) { 1364 if (PabloAST * user = getValue(G[target(e, G)])) { 1365 cast<Statement>(user)>replaceUsesOfWith(G[e], replacement); 1366 } 1367 } 1368 } 1369 1370 stmt = replacement; 1371 } 1372 1373 assert (stmt); 1374 assert (inCurrentBlock(stmt, block)); 1375 1376 if (LLVM_UNLIKELY(isa<If>(stmt)  isa<While>(stmt))) { 1377 for (auto e : make_iterator_range(out_edges(u, G))) { 1378 const auto v = target(e, G); 1379 assert (L[v] == std::numeric_limits<line_t>::max()); 1380 L[v] = count; 1381 } 1382 } 1383 1384 block>insert(cast<Statement>(stmt)); 1385 L[u] = count++; // update the line count with the actual one. 1386 } 1387 1388 Z3_solver_dec_ref(ctx, solver); 1389 Z3_del_context(ctx); 1390 1391 Statement * const end = block>getInsertPoint(); assert (end); 1392 for (;;) { 1393 Statement * const next = end>getNextNode(); 1394 if (next == nullptr) { 950 1395 break; 951 1396 } 952 953 const DistributionSets distributionSets = safeDistributionSets(G, H); 954 955 if (LLVM_UNLIKELY(distributionSets.empty())) { 956 break; 957 } 958 959 for (const DistributionSet & set : distributionSets) { 960 961 // Each distribution tuple consists of the sources, intermediary, and sink nodes. 962 const VertexSet & sources = std::get<0>(set); 963 const VertexSet & intermediary = std::get<1>(set); 964 const VertexSet & sinks = std::get<2>(set); 965 966 const TypeId outerTypeId = getType(G[mapping[H[sinks.front()]]]); 967 assert (outerTypeId == TypeId::And  outerTypeId == TypeId::Or); 968 const TypeId innerTypeId = (outerTypeId == TypeId::Or) ? TypeId::And : TypeId::Or; 969 970 // Update G to match the desired change 971 const Vertex x = addSummaryVertex(outerTypeId, G); 972 const Vertex y = addSummaryVertex(innerTypeId, G); 973 mapping.resize(num_vertices(G)); 974 mapping[x] = x; 975 mapping[y] = y; 976 977 for (const Vertex i : intermediary) { 978 const auto u = mapping[H[i]]; 979 assert (getType(G[u]) == innerTypeId); 980 for (const Vertex t : sinks) { 981 assert (getType(G[mapping[H[t]]]) == outerTypeId); 982 remove_edge(u, mapping[H[t]], G); 983 } 984 add_edge(nullptr, u, x, G); 985 } 986 987 for (const Vertex s : sources) { 988 const auto u = mapping[H[s]]; 989 for (const Vertex i : intermediary) { 990 remove_edge(u, mapping[H[i]], G); 991 } 992 add_edge(nullptr, u, y, G); 993 } 994 add_edge(nullptr, x, y, G); 995 996 for (const Vertex t : sinks) { 997 const auto v = mapping[H[t]]; 998 add_edge(getValue(G[v]), y, v, G); 999 } 1000 1001 summarizeGraph(G, mapping); 1002 } 1003 } 1397 next>eraseFromParent(true); 1398 } 1399 1400 #ifndef NDEBUG 1401 PabloVerifier::verify(mFunction, "postreassociation"); 1402 #endif 1403 1004 1404 } 1005 1405 … … 1007 1407 * @brief addSummaryVertex 1008 1408 **  */ 1009 inline Vertex BooleanReassociationPass::addSummaryVertex(const TypeId typeId, Graph & G) { 1010 return add_vertex(std::make_pair(typeId, nullptr), G); 1011 } 1012 1013 /**  * 1014 * @brief getVertex 1015 **  */ 1016 Vertex BooleanReassociationPass::getSummaryVertex(PabloAST * expr, Graph & G, Map & M, const PabloBlock * const block) { 1409 Vertex BooleanReassociationPass::makeVertex(const TypeId typeId, PabloAST * const expr, Graph & G, Z3_ast node) { 1410 // for (Vertex u : make_iterator_range(vertices(G))) { 1411 // if (LLVM_UNLIKELY(in_degree(u, G) == 0 && out_degree(u, G) == 0)) { 1412 // std::get<0>(G[u]) = typeId; 1413 // std::get<1>(G[u]) = expr; 1414 // return u; 1415 // } 1416 // } 1417 return add_vertex(std::make_tuple(typeId, expr, node), G); 1418 } 1419 1420 /**  * 1421 * @brief addSummaryVertex 1422 **  */ 1423 Vertex BooleanReassociationPass::makeVertex(const TypeId typeId, PabloAST * const expr, StatementMap & M, Graph & G, Z3_ast node) { 1424 assert (expr); 1017 1425 const auto f = M.find(expr); 1018 1426 if (f != M.end()) { 1427 assert (getValue(G[f>second]) == expr); 1019 1428 return f>second; 1020 1429 } 1021 // To simplify future analysis, every statement not in the current block will be recorded as a Var. 1022 const TypeId typeId = inCurrentBlock(expr, block) ? expr>getClassTypeId() : TypeId::Var; 1023 const auto u = add_vertex(std::make_pair(typeId, expr), G); 1024 M.insert(std::make_pair(expr, u)); 1430 const Vertex u = makeVertex(typeId, expr, G, node); 1431 M.emplace(expr, u); 1025 1432 return u; 1026 1433 } 1027 1434 1028 } 1435 /**  * 1436 * @brief addSummaryVertex 1437 **  */ 1438 Vertex BooleanReassociationPass::makeVertex(const TypeId typeId, PabloAST * const expr, CharacterizationMap & C, StatementMap & M, Graph & G) { 1439 assert (expr); 1440 const auto f = M.find(expr); 1441 if (f != M.end()) { 1442 assert (getValue(G[f>second]) == expr); 1443 return f>second; 1444 } 1445 const Vertex u = makeVertex(typeId, expr, G, C.get(expr)); 1446 M.emplace(expr, u); 1447 return u; 1448 } 1449 1450 /**  * 1451 * @brief removeSummaryVertex 1452 **  */ 1453 inline void BooleanReassociationPass::removeVertex(const Vertex u, StatementMap & M, Graph & G) const { 1454 VertexData & ref = G[u]; 1455 if (std::get<1>(ref)) { 1456 auto f = M.find(std::get<1>(ref)); 1457 assert (f != M.end()); 1458 M.erase(f); 1459 } 1460 removeVertex(u, G); 1461 } 1462 1463 /**  * 1464 * @brief removeSummaryVertex 1465 **  */ 1466 inline void BooleanReassociationPass::removeVertex(const Vertex u, Graph & G) const { 1467 VertexData & ref = G[u]; 1468 clear_vertex(u, G); 1469 std::get<0>(ref) = TypeId::Var; 1470 std::get<1>(ref) = nullptr; 1471 std::get<2>(ref) = nullptr; 1472 } 1473 1474 /**  * 1475 * @brief make 1476 **  */ 1477 inline Z3_ast BooleanReassociationPass::makeVar() const { 1478 Z3_ast node = Z3_mk_fresh_const(mContext, nullptr, Z3_mk_bool_sort(mContext)); 1479 // Z3_inc_ref(mContext, node); 1480 return node; 1481 } 1482 1483 /**  * 1484 * @brief add 1485 **  */ 1486 inline Z3_ast BooleanReassociationPass::CharacterizationMap::add(PabloAST * const expr, Z3_ast node, const bool forwardOnly) { 1487 assert (expr && node); 1488 mForward.emplace(expr, node); 1489 if (!forwardOnly) { 1490 mBackward.emplace(node, expr); 1491 } 1492 return node; 1493 } 1494 1495 /**  * 1496 * @brief get 1497 **  */ 1498 inline Z3_ast BooleanReassociationPass::CharacterizationMap::get(PabloAST * const expr) const { 1499 assert (expr); 1500 auto f = mForward.find(expr); 1501 if (LLVM_UNLIKELY(f == mForward.end())) { 1502 if (mPredecessor == nullptr) { 1503 return nullptr; 1504 } 1505 return mPredecessor>get(expr); 1506 } 1507 return f>second; 1508 } 1509 1510 /**  * 1511 * @brief get 1512 **  */ 1513 inline PabloAST * BooleanReassociationPass::CharacterizationMap::findKey(Z3_ast const node) const { 1514 assert (node); 1515 auto f = mBackward.find(node); 1516 if (LLVM_UNLIKELY(f == mBackward.end())) { 1517 if (mPredecessor == nullptr) { 1518 return nullptr; 1519 } 1520 return mPredecessor>findKey(node); 1521 } 1522 return f>second; 1523 } 1524 1525 /**  * 1526 * @brief constructor 1527 **  */ 1528 inline BooleanReassociationPass::BooleanReassociationPass(Z3_context ctx, Z3_solver solver, PabloFunction & f) 1529 : mContext(ctx) 1530 , mSolver(solver) 1531 , mFunction(f) 1532 , mModified(false) { 1533 1534 } 1535 1536 } 
icGREP/icgrepdevel/icgrep/pablo/optimizers/booleanreassociationpass.h
r4871 r5152 3 3 4 4 #include <pablo/codegenstate.h> 5 #include <boost/graph/adjacency_list.hpp> 5 6 #include <boost/container/flat_map.hpp> 6 #include < boost/graph/adjacency_list.hpp>7 #include <z3.h> 7 8 8 9 namespace pablo { … … 10 11 class BooleanReassociationPass { 11 12 public: 12 using VertexData = std:: pair<PabloAST::ClassTypeId, PabloAST *>;13 using VertexData = std::tuple<PabloAST::ClassTypeId, PabloAST *, Z3_ast>; 13 14 using Graph = boost::adjacency_list<boost::vecS, boost::vecS, boost::bidirectionalS, VertexData, PabloAST *>; 14 15 using Vertex = Graph::vertex_descriptor; 15 using Map = std::unordered_map<const PabloAST *, Vertex>; 16 using ScopeMap = boost::container::flat_map<const PabloBlock *, Statement *>; 16 using VertexMap = std::unordered_map<Z3_ast, Vertex>; 17 using StatementMap = boost::container::flat_map<PabloAST *, Vertex>; 18 using DistributionGraph = boost::adjacency_list<boost::hash_setS, boost::vecS, boost::bidirectionalS, Vertex>; 19 17 20 static bool optimize(PabloFunction & function); 21 18 22 protected: 19 inline BooleanReassociationPass() {} 20 void processScopes(PabloFunction & function); 21 PabloBlock * processScopes(PabloFunction & f, PabloBlock * const block); 22 PabloBlock * processScope(PabloFunction & f, PabloBlock * const block); 23 void summarizeAST(PabloBlock * const block, Graph & G) const; 24 static void summarizeGraph(Graph & G, std::vector<Vertex> & mapping); 25 void resolveNestedUsages(const Vertex u, PabloAST * expr, PabloBlock * const block, Graph & G, Map & M, const Statement * const ignoreIfThis = nullptr) const; 26 void redistributeAST(Graph & G) const; 27 PabloBlock * rewriteAST(PabloFunction & f, PabloBlock * const block, Graph & G); 28 static PabloAST * createTree(const PabloBlock * const block, PabloBlock * const newScope, const Vertex u, Graph & G); 29 static Vertex getSummaryVertex(PabloAST * expr, Graph & G, Map & M, const PabloBlock * const block); 30 static Vertex addSummaryVertex(const PabloAST::ClassTypeId typeId, Graph & G); 23 24 struct CharacterizationMap { 25 using ForwardMap = boost::container::flat_map<PabloAST *, Z3_ast>; 26 using BackwardMap = boost::container::flat_map<Z3_ast, PabloAST *>; 27 using iterator = ForwardMap::const_iterator; 28 Z3_ast add(PabloAST * const expr, Z3_ast node, const bool forwardOnly = false); 29 Z3_ast get(PabloAST * const expr) const; 30 PabloAST * findKey(Z3_ast const node) const; 31 iterator begin() const { return mForward.cbegin(); } 32 iterator end() const { return mForward.cend(); } 33 inline CharacterizationMap() : mPredecessor(nullptr) {} 34 inline CharacterizationMap(CharacterizationMap & predecessor) : mPredecessor(&predecessor) {} 35 private: 36 CharacterizationMap * const mPredecessor; 37 ForwardMap mForward; 38 BackwardMap mBackward; 39 }; 40 41 protected: 42 43 BooleanReassociationPass(Z3_context ctx, Z3_solver solver, PabloFunction & f); 44 bool processScopes(PabloFunction & function); 45 void processScopes(PabloBlock * const block, CharacterizationMap & map); 46 void distributeScope(PabloBlock * const block, CharacterizationMap & map); 47 48 void transformAST(PabloBlock * const block, CharacterizationMap & C, Graph & G); 49 void resolveNestedUsages(PabloBlock * const block, PabloAST * const expr, const Vertex u, CharacterizationMap &C, StatementMap & S, Graph & G, const Statement * const ignoreIfThis = nullptr) const; 50 51 bool contractGraph(StatementMap & M, Graph & G) const; 52 53 bool reduceGraph(CharacterizationMap & C, StatementMap & S, Graph & G) const; 54 55 bool factorGraph(const PabloAST::ClassTypeId typeId, Graph & G, std::vector<Vertex> & factors) const; 56 bool factorGraph(Graph & G) const; 57 58 static Vertex makeVertex(const PabloAST::ClassTypeId typeId, PabloAST * const expr, Graph & G, Z3_ast node = nullptr); 59 static Vertex makeVertex(const PabloAST::ClassTypeId typeId, PabloAST * const expr, StatementMap & M, Graph & G, Z3_ast node = nullptr); 60 static Vertex makeVertex(const PabloAST::ClassTypeId typeId, PabloAST * const expr, CharacterizationMap & C, StatementMap & M, Graph & G); 61 void removeVertex(const Vertex u, StatementMap & M, Graph & G) const; 62 void removeVertex(const Vertex u, Graph & G) const; 63 64 bool redistributeGraph(CharacterizationMap & C, StatementMap & M, Graph & G) const; 65 66 void rewriteAST(PabloBlock * const block, Graph & G); 67 68 Statement * characterize(Statement * const stmt, CharacterizationMap & map); 69 70 Z3_ast makeVar() const; 71 31 72 private: 32 ScopeMap mResolvedScopes; 73 Z3_context const mContext; 74 Z3_solver const mSolver; 75 Z3_ast mInFile; 76 PabloFunction & mFunction; 77 bool mModified; 33 78 }; 34 79
Note: See TracChangeset
for help on using the changeset viewer.