Changeset 5157 for icGREP/icgrepdevel/icgrep/pablo/optimizers
 Timestamp:
 Sep 15, 2016, 4:29:27 PM (3 years ago)
 Location:
 icGREP/icgrepdevel/icgrep/pablo/optimizers
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

icGREP/icgrepdevel/icgrep/pablo/optimizers/booleanreassociationpass.cpp
r5156 r5157 273 273 274 274 Z3_config cfg = Z3_mk_config(); 275 Z3_context ctx = Z3_mk_context (cfg);275 Z3_context ctx = Z3_mk_context_rc(cfg); 276 276 Z3_del_config(cfg); 277 277 … … 302 302 **  */ 303 303 inline bool BooleanReassociationPass::processScopes(PabloFunction & function) { 304 mRefs.clear(); 305 CharacterizationMap C; 304 306 PabloBlock * const entry = function.getEntryBlock(); 305 CharacterizationMap map;306 307 // Map the constants and input variables 307 map.add(entry>createZeroes(), Z3_mk_false(mContext));308 map.add(entry>createOnes(), Z3_mk_true(mContext));308 C.add(entry>createZeroes(), Z3_mk_false(mContext)); 309 C.add(entry>createOnes(), Z3_mk_true(mContext)); 309 310 for (unsigned i = 0; i < mFunction.getNumOfParameters(); ++i) { 310 map.add(mFunction.getParameter(i), makeVar());311 C.add(mFunction.getParameter(i), makeVar()); 311 312 } 312 313 mInFile = makeVar(); 313 processScopes(entry, map);314 processScopes(entry, C); 314 315 return mModified; 315 316 } … … 318 319 * @brief processScopes 319 320 **  */ 320 void BooleanReassociationPass::processScopes(PabloBlock * const block, CharacterizationMap & map) { 321 void BooleanReassociationPass::processScopes(PabloBlock * const block, CharacterizationMap & C) { 322 const auto offset = mRefs.size(); 321 323 for (Statement * stmt = block>front(); stmt; ) { 322 324 if (LLVM_UNLIKELY(isa<If>(stmt))) { … … 324 326 stmt = stmt>eraseFromParent(true); 325 327 } else { 326 CharacterizationMap nested( map);328 CharacterizationMap nested(C); 327 329 processScopes(cast<If>(stmt)>getBody(), nested); 328 330 for (Assign * def : cast<If>(stmt)>getDefined()) { 329 map.add(def, makeVar());331 C.add(def, makeVar()); 330 332 } 331 333 stmt = stmt>getNextNode(); … … 335 337 stmt = stmt>eraseFromParent(true); 336 338 } else { 337 CharacterizationMap nested( map);339 CharacterizationMap nested(C); 338 340 processScopes(cast<While>(stmt)>getBody(), nested); 339 341 for (Next * var : cast<While>(stmt)>getVariants()) { 340 map.add(var, makeVar());342 C.add(var, makeVar()); 341 343 } 342 344 stmt = stmt>getNextNode(); 343 345 } 344 346 } else { // characterize this statement then check whether it is equivalent to any existing one. 345 stmt = characterize(stmt, map);347 stmt = characterize(stmt, C); 346 348 } 347 349 } 348 distributeScope(block, map); 350 distributeScope(block, C); 351 for (auto i = mRefs.begin() + offset; i != mRefs.end(); ++i) { 352 Z3_dec_ref(mContext, *i); 353 } 354 mRefs.erase(mRefs.begin() + offset, mRefs.end()); 349 355 } 350 356 … … 352 358 * @brief characterize 353 359 **  */ 354 inline Statement * BooleanReassociationPass::characterize(Statement * const stmt, CharacterizationMap & map) {360 inline Statement * BooleanReassociationPass::characterize(Statement * const stmt, CharacterizationMap & C) { 355 361 Z3_ast node = nullptr; 356 362 const size_t n = stmt>getNumOperands(); assert (n > 0); … … 358 364 Z3_ast operands[n]; 359 365 for (size_t i = 0; i < n; ++i) { 360 operands[i] = map.get(stmt>getOperand(i)); assert (operands[i]);366 operands[i] = C.get(stmt>getOperand(i)); assert (operands[i]); 361 367 } 362 368 if (isa<And>(stmt)) { … … 367 373 node = Z3_mk_xor(mContext, operands[0], operands[1]); 368 374 for (unsigned i = 2; LLVM_UNLIKELY(i < n); ++i) { 369 node = Z3_mk_xor(mContext, node, operands[i]); 375 Z3_inc_ref(mContext, node); 376 Z3_ast temp = Z3_mk_xor(mContext, node, operands[i]); 377 Z3_inc_ref(mContext, temp); 378 Z3_dec_ref(mContext, node); 379 node = temp; 370 380 } 371 381 } 372 382 } else if (isa<Not>(stmt)) { 373 Z3_ast op = map.get(stmt>getOperand(0)); assert (op);383 Z3_ast op = C.get(stmt>getOperand(0)); assert (op); 374 384 node = Z3_mk_not(mContext, op); 375 385 } else if (isa<Sel>(stmt)) { 376 386 Z3_ast operands[3]; 377 387 for (size_t i = 0; i < 3; ++i) { 378 operands[i] = map.get(stmt>getOperand(i)); assert (operands[i]);388 operands[i] = C.get(stmt>getOperand(i)); assert (operands[i]); 379 389 } 380 390 node = Z3_mk_ite(mContext, operands[0], operands[1], operands[2]); … … 382 392 assert (stmt>getNumOperands() == 1); 383 393 Z3_ast check[2]; 384 check[0] = map.get(stmt>getOperand(0)); assert (check[0]);394 check[0] = C.get(stmt>getOperand(0)); assert (check[0]); 385 395 check[1] = isa<InFile>(stmt) ? mInFile : Z3_mk_not(mContext, mInFile); assert (check[1]); 386 396 node = Z3_mk_and(mContext, 2, check); 387 397 } else { 388 398 if (LLVM_UNLIKELY(isa<Assign>(stmt)  isa<Next>(stmt))) { 389 Z3_ast op = map.get(stmt>getOperand(0)); assert (op);390 map.add(stmt, op, true);399 Z3_ast op = C.get(stmt>getOperand(0)); assert (op); 400 C.add(stmt, op, true); 391 401 } else { 392 map.add(stmt, makeVar());402 C.add(stmt, makeVar()); 393 403 } 394 404 return stmt>getNextNode(); 395 405 } 396 node = simplify(node); assert (node); 397 PabloAST * const replacement = map.findKey(node); 406 Z3_inc_ref(mContext, node); 407 node = simplify(node); 408 PabloAST * const replacement = C.findKey(node); 398 409 if (LLVM_LIKELY(replacement == nullptr)) { 399 map.add(stmt, node); 410 C.add(stmt, node); 411 mRefs.push_back(node); 400 412 return stmt>getNextNode(); 401 413 } else { 414 Z3_dec_ref(mContext, node); 402 415 return stmt>replaceWith(replacement); 403 416 } 404 405 417 } 406 418 … … 434 446 // Compute the base defuse graph ... 435 447 for (Statement * stmt : *mBlock) { 436 437 448 const Vertex u = makeVertex(stmt>getClassTypeId(), stmt, S, G, C.get(stmt)); 438 439 449 for (unsigned i = 0; i < stmt>getNumOperands(); ++i) { 440 450 PabloAST * const op = stmt>getOperand(i); … … 443 453 } 444 454 } 445 446 455 if (LLVM_UNLIKELY(isa<If>(stmt))) { 447 456 for (Assign * def : cast<const If>(stmt)>getDefined()) { … … 778 787 * Apply the distribution law to reduce computations whenever possible. 779 788 **  */ 780 bool BooleanReassociationPass::redistributeGraph(CharacterizationMap & C, VertexMap & M, Graph & G) const{789 bool BooleanReassociationPass::redistributeGraph(CharacterizationMap & C, VertexMap & M, Graph & G) { 781 790 782 791 bool modified = false; … … 948 957 add_edge(G[ej], v, target(ej, G), G); 949 958 } 950 // if (LLVM_UNLIKELY(getValue(G[v]) == nullptr && getValue(G[u]) != nullptr)) {951 // getValue(G[v]) = getValue(G[u]);952 // }953 959 removeVertex(u, G); 954 960 contracted = true; … … 963 969 add_edge(G[ej], source(ej, G), v, G); 964 970 } 965 if (LLVM_UNLIKELY(getValue(G[v]) == nullptr && getValue(G[u]) != nullptr)) {966 getValue(G[v]) = getValue(G[u]);967 }968 971 removeVertex(u, G); 969 972 contracted = true; … … 996 999 * @brief reduceGraph 997 1000 **  */ 998 bool BooleanReassociationPass::reduceVertex(const Vertex u, CharacterizationMap & C, VertexMap & M, Graph & G, const bool use_expensive_simplification) const{999 1000 bool reduced = false;1001 BooleanReassociationPass::Reduction BooleanReassociationPass::reduceVertex(const Vertex u, CharacterizationMap & C, VertexMap & M, Graph & G, const bool use_expensive_simplification) { 1002 1003 Reduction reduction = Reduction::NoChange; 1001 1004 1002 1005 assert (isReducible(G[u])); … … 1030 1033 } 1031 1034 assert (node); 1035 Z3_inc_ref(mContext, node); 1036 mRefs.push_back(node); 1032 1037 getDefinition(G[u]) = node; 1033 1038 } … … 1053 1058 } 1054 1059 assert (test); 1060 Z3_inc_ref(mContext, test); 1055 1061 test = simplify(test, use_expensive_simplification); 1056 1057 1062 bool replacement = false; 1058 1063 Vertex x = 0; … … 1061 1066 x = f>second; 1062 1067 assert (getDefinition(G[x]) == test); 1068 Z3_dec_ref(mContext, test); 1063 1069 replacement = true; 1064 } else {1065 PabloAST * const factor = C. findKey(test);1066 if (LLVM_UNLIKELY( !inCurrentBlock(factor, mBlock))) {1070 } else if (LLVM_LIKELY(C.predecessor() != nullptr)) { 1071 PabloAST * const factor = C.predecessor()>findKey(test); 1072 if (LLVM_UNLIKELY(factor != nullptr)) { 1067 1073 x = makeVertex(TypeId::Var, factor, G, test); 1068 1074 M.emplace(test, x); 1069 1075 replacement = true; 1076 mRefs.push_back(test); 1070 1077 } 1071 1078 } … … 1087 1094 } 1088 1095 1089 reduced = true; 1096 reduction = Reduction::Simplified; 1097 1090 1098 goto restart; 1091 1099 } 1100 1101 Z3_dec_ref(mContext, test); 1092 1102 } 1093 1103 } … … 1108 1118 } 1109 1119 removeVertex(u, G); 1110 reduc ed = true;1111 } 1112 1113 return reduc ed;1120 reduction = Reduction::Removed; 1121 } 1122 1123 return reduction; 1114 1124 } 1115 1125 … … 1117 1127 * @brief reduceGraph 1118 1128 **  */ 1119 bool BooleanReassociationPass::reduceGraph(CharacterizationMap & C, VertexMap & M, Graph & G) const{1129 bool BooleanReassociationPass::reduceGraph(CharacterizationMap & C, VertexMap & M, Graph & G) { 1120 1130 1121 1131 bool reduced = false; … … 1130 1140 for (const Vertex u : ordering) { 1131 1141 if (isReducible(G[u])) { 1132 if (reduceVertex(u, C, M, G, false) ) {1142 if (reduceVertex(u, C, M, G, false) != Reduction::NoChange) { 1133 1143 reduced = true; 1134 1144 } … … 1344 1354 line_t count = 1; 1345 1355 1356 // errs() << "\n"; 1357 1358 // printGraph(G, "G"); 1359 1346 1360 for (auto u : S) { 1347 1361 PabloAST *& stmt = getValue(G[u]); … … 1361 1375 const auto typeId = getType(G[u]); 1362 1376 1377 // retry: 1378 1379 T.clear(); 1380 T.reserve(in_degree(u, G)); 1381 for (const auto e : make_iterator_range(in_edges(u, G))) { 1382 T.push_back(source(e, G)); 1383 } 1384 1385 // Then sort them by their line position (noting any incoming value will either be 0 or MAX_INT) 1386 std::sort(T.begin(), T.end(), [&L](const Vertex u, const Vertex v){ return L[u] < L[v]; }); 1387 1388 if (LoadEarly) { 1389 mBlock>setInsertPoint(nullptr); 1390 } 1391 1363 1392 PabloAST * expr = nullptr; 1364 1365 for (;;) { 1366 1367 T.reserve(in_degree(u, G)); 1368 for (const auto e : make_iterator_range(in_edges(u, G))) { 1369 T.push_back(source(e, G)); 1370 } 1371 1372 // Then sort them by their line position (noting any incoming value will either be 0 or MAX_INT) 1373 std::sort(T.begin(), T.end(), [&L](const Vertex u, const Vertex v){ return L[u] < L[v]; }); 1374 1375 if (LoadEarly) { 1376 mBlock>setInsertPoint(nullptr); 1377 } 1378 1379 bool done = true; 1380 1381 PabloAST * join = nullptr; 1382 1383 for (auto v : T) { 1384 expr = getValue(G[v]); 1385 if (LLVM_UNLIKELY(expr == nullptr)) { 1386 throw std::runtime_error("Vertex " + std::to_string(v) + " does not have an expression!"); 1387 } 1388 if (join) { 1389 1390 if (in_degree(v, G) > 0) { 1391 1392 assert (L[v] > 0 && L[v] < MAX_INT); 1393 1394 Statement * dom = cast<Statement>(expr); 1395 for (;;) { 1396 PabloBlock * const parent = dom>getParent(); 1397 if (parent == mBlock) { 1398 break; 1399 } 1400 dom = parent>getBranch(); assert(dom); 1401 } 1402 mBlock>setInsertPoint(dom); 1403 1404 assert (dominates(join, expr)); 1405 assert (dominates(expr, ip)); 1406 assert (dominates(dom, ip)); 1407 } 1408 1409 Statement * const currIP = mBlock>getInsertPoint(); 1410 1411 switch (typeId) { 1412 case TypeId::And: 1413 expr = mBlock>createAnd(join, expr); break; 1414 case TypeId::Or: 1415 expr = mBlock>createOr(join, expr); break; 1416 case TypeId::Xor: 1417 expr = mBlock>createXor(join, expr); break; 1418 default: 1419 llvm_unreachable("Invalid TypeId!"); 1420 } 1421 1422 // If the insertion point hasn't "moved" then we didn't make a new statement 1423 // and thus must have unexpectidly reused a prior statement (or Var.) 1424 if (LLVM_UNLIKELY(currIP == mBlock>getInsertPoint())) { 1425 if (LLVM_LIKELY(reduceVertex(u, C, M, G, true))) { 1426 done = false; 1393 PabloAST * join = nullptr; 1394 1395 for (auto v : T) { 1396 expr = getValue(G[v]); 1397 if (LLVM_UNLIKELY(expr == nullptr)) { 1398 throw std::runtime_error("Vertex " + std::to_string(v) + " does not have an expression!"); 1399 } 1400 if (join) { 1401 1402 if (in_degree(v, G) > 0) { 1403 1404 assert (L[v] > 0 && L[v] < MAX_INT); 1405 1406 Statement * dom = cast<Statement>(expr); 1407 for (;;) { 1408 PabloBlock * const parent = dom>getParent(); 1409 if (parent == mBlock) { 1427 1410 break; 1428 1411 } 1429 throw std::runtime_error("Unable to reduce vertex " + std::to_string(u));1412 dom = parent>getBranch(); assert(dom); 1430 1413 } 1431 } 1432 join = expr; 1433 } 1434 1435 T.clear(); 1436 1437 if (done) { 1438 break; 1439 } 1440 } 1441 1442 1443 PabloAST * const replacement = expr; assert (replacement); 1414 mBlock>setInsertPoint(dom); 1415 1416 assert (dominates(join, expr)); 1417 assert (dominates(expr, ip)); 1418 assert (dominates(dom, ip)); 1419 } 1420 1421 switch (typeId) { 1422 case TypeId::And: 1423 expr = mBlock>createAnd(join, expr); break; 1424 case TypeId::Or: 1425 expr = mBlock>createOr(join, expr); break; 1426 case TypeId::Xor: 1427 expr = mBlock>createXor(join, expr); break; 1428 default: 1429 llvm_unreachable("Invalid TypeId!"); 1430 } 1431 1432 // // If the insertion point isn't the statement we just attempted to create 1433 // // we must have unexpectidly reused a prior statement (or Var.) 1434 // if (LLVM_UNLIKELY(expr != mBlock>getInsertPoint())) { 1435 // const auto reduction = reduceVertex(u, C, M, G, true); 1436 // if (LLVM_UNLIKELY(reduction == Reduction::NoChange)) { 1437 // throw std::runtime_error("Unable to reduce vertex " + std::to_string(u)); 1438 // } else if (LLVM_UNLIKELY(reduction == Reduction::Simplified)) { 1439 // goto retry; 1440 // } else { // if (reduction == Reduction::Removed) { 1441 // mBlock>setInsertPoint(ip>getPrevNode()); 1442 // goto next_statement; 1443 // } 1444 // } 1445 } 1446 join = expr; 1447 } 1448 1449 assert (expr); 1450 1451 Statement * const currIP = mBlock>getInsertPoint(); 1444 1452 1445 1453 mBlock>setInsertPoint(ip>getPrevNode()); … … 1448 1456 if (G[e]) { 1449 1457 if (PabloAST * user = getValue(G[target(e, G)])) { 1450 cast<Statement>(user)>replaceUsesOfWith(G[e], replacement); 1451 } 1452 } 1453 } 1454 1455 stmt = replacement; 1458 cast<Statement>(user)>replaceUsesOfWith(G[e], expr); 1459 } 1460 } 1461 } 1462 1463 stmt = expr; 1464 1465 // If the insertion point isn't the statement we just attempted to create, 1466 // we must have unexpectidly reused a prior statement (or var.) 1467 if (LLVM_UNLIKELY(expr != currIP)) { 1468 L[u] = 0; 1469 // If that statement happened to be in the current block, locate which 1470 // statement it "duplicated" (if any) and set the duplicate's line # to 1471 // the line of the original statement to maintain a consistent view of 1472 // the program. 1473 if (inCurrentBlock(expr, mBlock)) { 1474 for (auto v : make_iterator_range(vertices(G))) { 1475 if (LLVM_UNLIKELY(getValue(G[v]) == expr)) { 1476 L[u] = L[v]; 1477 break; 1478 } 1479 } 1480 } 1481 continue; 1482 } 1456 1483 } 1457 1484 … … 1466 1493 } 1467 1494 1495 // PabloPrinter::print(cast<Statement>(stmt), errs()); errs() << "\n"; 1496 1468 1497 mBlock>insert(cast<Statement>(stmt)); 1469 1498 L[u] = count++; // update the line count with the actual one. 1499 // next_statement: continue; 1470 1500 } 1471 1501 … … 1574 1604 * @brief make 1575 1605 **  */ 1576 inline Z3_ast BooleanReassociationPass::makeVar() const{1606 inline Z3_ast BooleanReassociationPass::makeVar() { 1577 1607 Z3_ast node = Z3_mk_fresh_const(mContext, nullptr, Z3_mk_bool_sort(mContext)); 1578 // Z3_inc_ref(mContext, node); 1608 Z3_inc_ref(mContext, node); 1609 mRefs.push_back(node); 1579 1610 return node; 1580 1611 } … … 1583 1614 * @brief simplify 1584 1615 **  */ 1585 Z3_ast BooleanReassociationPass::simplify(Z3_ast node, bool use_expensive_minimization) const { 1586 1616 Z3_ast BooleanReassociationPass::simplify(Z3_ast const node, bool use_expensive_minimization) const { 1587 1617 assert (node); 1588 1589 node = Z3_simplify_ex(mContext, node, mParams); 1590 1618 Z3_ast result = Z3_simplify_ex(mContext, node, mParams); 1619 Z3_inc_ref(mContext, result); 1591 1620 if (use_expensive_minimization) { 1592 1593 1621 Z3_goal g = Z3_mk_goal(mContext, true, false, false); 1594 1622 Z3_goal_inc_ref(mContext, g); 1595 1596 Z3_goal_assert(mContext, g, node); 1623 Z3_goal_assert(mContext, g, result); 1597 1624 1598 1625 Z3_apply_result r = Z3_tactic_apply(mContext, mTactic, g); 1599 1626 Z3_apply_result_inc_ref(mContext, r); 1600 1601 1627 assert (Z3_apply_result_get_num_subgoals(mContext, r) == 1); 1602 1628 1603 1629 Z3_goal h = Z3_apply_result_get_subgoal(mContext, r, 0); 1604 1630 Z3_goal_inc_ref(mContext, h); 1631 Z3_goal_dec_ref(mContext, g); 1605 1632 1606 1633 const unsigned n = Z3_goal_size(mContext, h); 1607 1634 1635 Z3_ast optimized = nullptr; 1608 1636 if (n == 1) { 1609 node = Z3_goal_formula(mContext, h, 0); 1637 optimized = Z3_goal_formula(mContext, h, 0); 1638 Z3_inc_ref(mContext, optimized); 1639 1610 1640 } else if (n > 1) { 1611 1641 Z3_ast operands[n]; 1612 1642 for (unsigned i = 0; i < n; ++i) { 1613 1643 operands[i] = Z3_goal_formula(mContext, h, i); 1614 } 1615 node = Z3_mk_and(mContext, n, operands); 1644 Z3_inc_ref(mContext, operands[i]); 1645 } 1646 optimized = Z3_mk_and(mContext, n, operands); 1647 Z3_inc_ref(mContext, optimized); 1648 for (unsigned i = 0; i < n; ++i) { 1649 Z3_dec_ref(mContext, operands[i]); 1650 } 1616 1651 } 1617 1652 Z3_goal_dec_ref(mContext, h); 1618 } 1619 return node; 1653 Z3_apply_result_dec_ref(mContext, r); 1654 Z3_dec_ref(mContext, result); 1655 result = optimized; 1656 } 1657 Z3_dec_ref(mContext, node); 1658 return result; 1620 1659 } 1621 1660 
icGREP/icgrepdevel/icgrep/pablo/optimizers/booleanreassociationpass.h
r5156 r5157 44 44 BooleanReassociationPass(Z3_context ctx, Z3_params params, Z3_tactic tactic, PabloFunction & f); 45 45 bool processScopes(PabloFunction & function); 46 void processScopes(PabloBlock * const block, CharacterizationMap & map);46 void processScopes(PabloBlock * const block, CharacterizationMap & C); 47 47 void distributeScope(PabloBlock * const block, CharacterizationMap & C); 48 48 … … 52 52 bool contractGraph(Graph & G) const; 53 53 54 bool reduceVertex(const Vertex u, CharacterizationMap & C, VertexMap & M, Graph & G, const bool use_expensive_simplification) const; 55 bool reduceGraph(CharacterizationMap & C, VertexMap & M, Graph & G) const; 54 bool reduceGraph(CharacterizationMap & C, VertexMap & M, Graph & G); 55 56 enum class Reduction { 57 NoChange 58 , Simplified 59 , Removed 60 }; 61 62 Reduction reduceVertex(const Vertex u, CharacterizationMap & C, VertexMap & M, Graph & G, const bool use_expensive_simplification); 56 63 57 64 bool factorGraph(const PabloAST::ClassTypeId typeId, Graph & G, std::vector<Vertex> & factors) const; … … 64 71 void removeVertex(const Vertex u, Graph & G) const; 65 72 66 bool redistributeGraph(CharacterizationMap & C, VertexMap & M, Graph & G) const;73 bool redistributeGraph(CharacterizationMap & C, VertexMap & M, Graph & G); 67 74 68 75 bool rewriteAST(CharacterizationMap & C, VertexMap &M, Graph & G); … … 72 79 Z3_ast simplify(Z3_ast node, bool use_expensive_minimization = false) const; 73 80 74 Z3_ast makeVar() const;81 Z3_ast makeVar(); 75 82 76 83 private: … … 80 87 Z3_tactic const mTactic; 81 88 Z3_ast mInFile; 89 std::vector<Z3_ast> mRefs; 82 90 PabloFunction & mFunction; 83 91 bool mModified;
Note: See TracChangeset
for help on using the changeset viewer.