Ignore:
Timestamp:
Sep 15, 2016, 4:29:27 PM (3 years ago)
Author:
nmedfort
Message:

Bug fix for reassociation pass.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • icGREP/icgrep-devel/icgrep/pablo/optimizers/booleanreassociationpass.cpp

    r5156 r5157  
    273273
    274274    Z3_config cfg = Z3_mk_config();
    275     Z3_context ctx = Z3_mk_context(cfg);
     275    Z3_context ctx = Z3_mk_context_rc(cfg);
    276276    Z3_del_config(cfg);
    277277
     
    302302 ** ------------------------------------------------------------------------------------------------------------- */
    303303inline bool BooleanReassociationPass::processScopes(PabloFunction & function) {
     304    mRefs.clear();
     305    CharacterizationMap C;
    304306    PabloBlock * const entry = function.getEntryBlock();
    305     CharacterizationMap map;
    306307    // 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));
    309310    for (unsigned i = 0; i < mFunction.getNumOfParameters(); ++i) {
    310         map.add(mFunction.getParameter(i), makeVar());
     311        C.add(mFunction.getParameter(i), makeVar());
    311312    }
    312313    mInFile = makeVar();
    313     processScopes(entry, map);
     314    processScopes(entry, C);
    314315    return mModified;
    315316}
     
    318319 * @brief processScopes
    319320 ** ------------------------------------------------------------------------------------------------------------- */
    320 void BooleanReassociationPass::processScopes(PabloBlock * const block, CharacterizationMap & map) {
     321void BooleanReassociationPass::processScopes(PabloBlock * const block, CharacterizationMap & C) {
     322    const auto offset = mRefs.size();
    321323    for (Statement * stmt = block->front(); stmt; ) {
    322324        if (LLVM_UNLIKELY(isa<If>(stmt))) {
     
    324326                stmt = stmt->eraseFromParent(true);
    325327            } else {
    326                 CharacterizationMap nested(map);
     328                CharacterizationMap nested(C);
    327329                processScopes(cast<If>(stmt)->getBody(), nested);
    328330                for (Assign * def : cast<If>(stmt)->getDefined()) {
    329                     map.add(def, makeVar());
     331                    C.add(def, makeVar());
    330332                }
    331333                stmt = stmt->getNextNode();
     
    335337                stmt = stmt->eraseFromParent(true);
    336338            } else {
    337                 CharacterizationMap nested(map);
     339                CharacterizationMap nested(C);
    338340                processScopes(cast<While>(stmt)->getBody(), nested);
    339341                for (Next * var : cast<While>(stmt)->getVariants()) {
    340                     map.add(var, makeVar());
     342                    C.add(var, makeVar());
    341343                }
    342344                stmt = stmt->getNextNode();
    343345            }
    344346        } else { // characterize this statement then check whether it is equivalent to any existing one.
    345             stmt = characterize(stmt, map);
     347            stmt = characterize(stmt, C);
    346348        }
    347349    }   
    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());
    349355}
    350356
     
    352358 * @brief characterize
    353359 ** ------------------------------------------------------------------------------------------------------------- */
    354 inline Statement * BooleanReassociationPass::characterize(Statement * const stmt, CharacterizationMap & map) {
     360inline Statement * BooleanReassociationPass::characterize(Statement * const stmt, CharacterizationMap & C) {
    355361    Z3_ast node = nullptr;
    356362    const size_t n = stmt->getNumOperands(); assert (n > 0);
     
    358364        Z3_ast operands[n];
    359365        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]);
    361367        }
    362368        if (isa<And>(stmt)) {
     
    367373            node = Z3_mk_xor(mContext, operands[0], operands[1]);
    368374            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;
    370380            }
    371381        }
    372382    } 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);
    374384        node = Z3_mk_not(mContext, op);
    375385    } else if (isa<Sel>(stmt)) {
    376386        Z3_ast operands[3];
    377387        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]);
    379389        }
    380390        node = Z3_mk_ite(mContext, operands[0], operands[1], operands[2]);
     
    382392        assert (stmt->getNumOperands() == 1);
    383393        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]);
    385395        check[1] = isa<InFile>(stmt) ? mInFile : Z3_mk_not(mContext, mInFile); assert (check[1]);
    386396        node = Z3_mk_and(mContext, 2, check);
    387397    } else {
    388398        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);
    391401        } else {
    392             map.add(stmt, makeVar());
     402            C.add(stmt, makeVar());
    393403        }
    394404        return stmt->getNextNode();
    395405    }
    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);
    398409    if (LLVM_LIKELY(replacement == nullptr)) {
    399         map.add(stmt, node);
     410        C.add(stmt, node);
     411        mRefs.push_back(node);
    400412        return stmt->getNextNode();
    401413    } else {
     414        Z3_dec_ref(mContext, node);
    402415        return stmt->replaceWith(replacement);
    403416    }
    404 
    405417}
    406418
     
    434446    // Compute the base def-use graph ...
    435447    for (Statement * stmt : *mBlock) {
    436 
    437448        const Vertex u = makeVertex(stmt->getClassTypeId(), stmt, S, G, C.get(stmt));
    438 
    439449        for (unsigned i = 0; i < stmt->getNumOperands(); ++i) {
    440450            PabloAST * const op = stmt->getOperand(i);
     
    443453            }
    444454        }
    445 
    446455        if (LLVM_UNLIKELY(isa<If>(stmt))) {
    447456            for (Assign * def : cast<const If>(stmt)->getDefined()) {
     
    778787 * Apply the distribution law to reduce computations whenever possible.
    779788 ** ------------------------------------------------------------------------------------------------------------- */
    780 bool BooleanReassociationPass::redistributeGraph(CharacterizationMap & C, VertexMap & M, Graph & G) const {
     789bool BooleanReassociationPass::redistributeGraph(CharacterizationMap & C, VertexMap & M, Graph & G) {
    781790
    782791    bool modified = false;
     
    948957                        add_edge(G[ej], v, target(ej, G), G);
    949958                    }
    950 //                    if (LLVM_UNLIKELY(getValue(G[v]) == nullptr && getValue(G[u]) != nullptr)) {
    951 //                        getValue(G[v]) = getValue(G[u]);
    952 //                    }
    953959                    removeVertex(u, G);
    954960                    contracted = true;
     
    963969                            add_edge(G[ej], source(ej, G), v, G);
    964970                        }
    965                         if (LLVM_UNLIKELY(getValue(G[v]) == nullptr && getValue(G[u]) != nullptr)) {
    966                             getValue(G[v]) = getValue(G[u]);
    967                         }
    968971                        removeVertex(u, G);
    969972                        contracted = true;
     
    996999 * @brief reduceGraph
    9971000 ** ------------------------------------------------------------------------------------------------------------- */
    998 bool BooleanReassociationPass::reduceVertex(const Vertex u, CharacterizationMap & C, VertexMap & M, Graph & G, const bool use_expensive_simplification) const {
    999 
    1000     bool reduced = false;
     1001BooleanReassociationPass::Reduction BooleanReassociationPass::reduceVertex(const Vertex u, CharacterizationMap & C, VertexMap & M, Graph & G, const bool use_expensive_simplification) {
     1002
     1003    Reduction reduction = Reduction::NoChange;
    10011004
    10021005    assert (isReducible(G[u]));
     
    10301033            }
    10311034            assert (node);
     1035            Z3_inc_ref(mContext, node);
     1036            mRefs.push_back(node);
    10321037            getDefinition(G[u]) = node;
    10331038        }
     
    10531058                    }
    10541059                    assert (test);
     1060                    Z3_inc_ref(mContext, test);
    10551061                    test = simplify(test, use_expensive_simplification);
    1056 
    10571062                    bool replacement = false;
    10581063                    Vertex x = 0;
     
    10611066                        x = f->second;
    10621067                        assert (getDefinition(G[x]) == test);
     1068                        Z3_dec_ref(mContext, test);
    10631069                        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)) {
    10671073                            x = makeVertex(TypeId::Var, factor, G, test);
    10681074                            M.emplace(test, x);
    10691075                            replacement = true;
     1076                            mRefs.push_back(test);
    10701077                        }
    10711078                    }
     
    10871094                        }
    10881095
    1089                         reduced = true;
     1096                        reduction = Reduction::Simplified;
     1097
    10901098                        goto restart;
    10911099                    }
     1100
     1101                    Z3_dec_ref(mContext, test);
    10921102                }
    10931103            }
     
    11081118        }
    11091119        removeVertex(u, G);
    1110         reduced = true;
    1111     }
    1112 
    1113     return reduced;
     1120        reduction = Reduction::Removed;
     1121    }
     1122
     1123    return reduction;
    11141124}
    11151125
     
    11171127 * @brief reduceGraph
    11181128 ** ------------------------------------------------------------------------------------------------------------- */
    1119 bool BooleanReassociationPass::reduceGraph(CharacterizationMap & C, VertexMap & M, Graph & G) const {
     1129bool BooleanReassociationPass::reduceGraph(CharacterizationMap & C, VertexMap & M, Graph & G) {
    11201130
    11211131    bool reduced = false;
     
    11301140    for (const Vertex u : ordering) {
    11311141        if (isReducible(G[u])) {
    1132             if (reduceVertex(u, C, M, G, false)) {
     1142            if (reduceVertex(u, C, M, G, false) != Reduction::NoChange) {
    11331143                reduced = true;
    11341144            }
     
    13441354    line_t count = 1;
    13451355
     1356//    errs() << "--------------------------------------------------\n";
     1357
     1358//    printGraph(G, "G");
     1359
    13461360    for (auto u : S) {
    13471361        PabloAST *& stmt = getValue(G[u]);
     
    13611375            const auto typeId = getType(G[u]);
    13621376
     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
    13631392            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) {
    14271410                                break;
    14281411                            }
    1429                             throw std::runtime_error("Unable to reduce vertex " + std::to_string(u));
     1412                            dom = parent->getBranch(); assert(dom);
    14301413                        }
    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();
    14441452
    14451453            mBlock->setInsertPoint(ip->getPrevNode());
     
    14481456                if (G[e]) {
    14491457                    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            }
    14561483        }
    14571484
     
    14661493        }
    14671494
     1495//        PabloPrinter::print(cast<Statement>(stmt), errs()); errs() << "\n";
     1496
    14681497        mBlock->insert(cast<Statement>(stmt));
    14691498        L[u] = count++; // update the line count with the actual one.
     1499//        next_statement: continue;
    14701500    }
    14711501
     
    15741604 * @brief make
    15751605 ** ------------------------------------------------------------------------------------------------------------- */
    1576 inline Z3_ast BooleanReassociationPass::makeVar() const {
     1606inline Z3_ast BooleanReassociationPass::makeVar() {
    15771607    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);
    15791610    return node;
    15801611}
     
    15831614 * @brief simplify
    15841615 ** ------------------------------------------------------------------------------------------------------------- */
    1585 Z3_ast BooleanReassociationPass::simplify(Z3_ast node, bool use_expensive_minimization) const {
    1586 
     1616Z3_ast BooleanReassociationPass::simplify(Z3_ast const node, bool use_expensive_minimization) const {
    15871617    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);
    15911620    if (use_expensive_minimization) {
    1592 
    15931621        Z3_goal g = Z3_mk_goal(mContext, true, false, false);
    15941622        Z3_goal_inc_ref(mContext, g);
    1595 
    1596         Z3_goal_assert(mContext, g, node);
     1623        Z3_goal_assert(mContext, g, result);
    15971624
    15981625        Z3_apply_result r = Z3_tactic_apply(mContext, mTactic, g);
    15991626        Z3_apply_result_inc_ref(mContext, r);
    1600 
    16011627        assert (Z3_apply_result_get_num_subgoals(mContext, r) == 1);
    16021628
    16031629        Z3_goal h = Z3_apply_result_get_subgoal(mContext, r, 0);
    16041630        Z3_goal_inc_ref(mContext, h);
     1631        Z3_goal_dec_ref(mContext, g);
    16051632
    16061633        const unsigned n = Z3_goal_size(mContext, h);
    16071634
     1635        Z3_ast optimized = nullptr;
    16081636        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
    16101640        } else if (n > 1) {
    16111641            Z3_ast operands[n];
    16121642            for (unsigned i = 0; i < n; ++i) {
    16131643                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            }
    16161651        }
    16171652        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;
    16201659}
    16211660
Note: See TracChangeset for help on using the changeset viewer.