Changeset 5152 for icGREP


Ignore:
Timestamp:
Sep 8, 2016, 5:11:14 PM (3 years ago)
Author:
nmedfort
Message:

Work on a Z3 based reassociation pass.

Location:
icGREP/icgrep-devel/icgrep/pablo/optimizers
Files:
2 edited

Legend:

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

    r4919 r5152  
    44#include <boost/circular_buffer.hpp>
    55#include <boost/graph/adjacency_list.hpp>
    6 #include <boost/graph/filtered_graph.hpp>
    76#include <boost/graph/topological_sort.hpp>
     7#include <boost/graph/strong_components.hpp>
    88#include <pablo/optimizers/pablo_simplifier.hpp>
    99#include <pablo/analysis/pabloverifier.hpp>
    1010#include <algorithm>
    1111#include <numeric> // std::iota
    12 #ifndef NDEBUG
    13 #include <queue>
    14 #endif
    1512#include <pablo/printer_pablos.h>
    1613#include <iostream>
     14#include <llvm/Support/CommandLine.h>
     15#include "maxsat.hpp"
    1716
    1817using namespace boost;
    1918using namespace boost::container;
    2019
     20
     21static cl::OptionCategory ReassociationOptions("Reassociation Optimization Options", "These options control the Pablo Reassociation optimization pass.");
     22
     23static cl::opt<unsigned> LoadEarly("Reassociation-Load-Early", 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
    2128namespace pablo {
    2229
    2330using TypeId = PabloAST::ClassTypeId;
    24 using DependencyGraph = BooleanReassociationPass::Graph;
    25 using Vertex = DependencyGraph::vertex_descriptor;
     31using Graph = BooleanReassociationPass::Graph;
     32using Vertex = Graph::vertex_descriptor;
    2633using 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>;
     34using DistributionGraph = BooleanReassociationPass::DistributionGraph;
     35using DistributionMap = flat_map<Graph::vertex_descriptor, DistributionGraph::vertex_descriptor>;
    3036using VertexSet = std::vector<Vertex>;
    3137using VertexSets = std::vector<VertexSet>;
     
    3945 ** ------------------------------------------------------------------------------------------------------------- */
    4046template<typename Iterator>
    41 inline DependencyGraph::edge_descriptor first(const std::pair<Iterator, Iterator> & range) {
     47inline Graph::edge_descriptor first(const std::pair<Iterator, Iterator> & range) {
    4248    assert (range.first != range.second);
    4349    return *range.first;
    4450}
    4551
    46 #ifndef NDEBUG
    47 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 #endif
    71 
    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 unique
    75     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 
    8452static inline bool inCurrentBlock(const Statement * stmt, const PabloBlock * const block) {
    8553    return stmt->getParent() == block;
     
    9866}
    9967
     68inline Z3_ast & getDefinition(VertexData & data) {
     69    return std::get<2>(data);
     70}
     71
     72inline PabloAST * getValue(const VertexData & data) {
     73    return std::get<1>(data);
     74}
     75
    10076inline PabloAST *& getValue(VertexData & data) {
    101     return std::get<1>(data);
    102 }
    103 
    104 inline PabloAST * getValue(const VertexData & data) {
    10577    return std::get<1>(data);
    10678}
     
    12799}
    128100
    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);
     101void 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;
    148139}
    149140
     
    167158}
    168159
     160
     161/** ------------------------------------------------------------------------------------------------------------- *
     162 * @brief printGraph
     163 ** ------------------------------------------------------------------------------------------------------------- */
     164static 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
    169267/** ------------------------------------------------------------------------------------------------------------- *
    170268 * @brief optimize
    171269 ** ------------------------------------------------------------------------------------------------------------- */
    172 bool BooleanReassociationPass::optimize(PabloFunction & function) {   
    173     BooleanReassociationPass brp;
     270bool 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);
    174279    brp.processScopes(function);
    175     #ifndef NDEBUG
    176     PabloVerifier::verify(function, "post-reassociation");
    177     #endif
     280
     281    Z3_solver_dec_ref(ctx, solver);
     282    Z3_del_context(ctx);
     283
    178284    Simplifier::optimize(function);
     285
    179286    return true;
    180287}
     
    183290 * @brief processScopes
    184291 ** ------------------------------------------------------------------------------------------------------------- */
    185 inline void BooleanReassociationPass::processScopes(PabloFunction & function) {
    186     function.setEntryBlock(processScopes(function, function.getEntryBlock()));
     292inline 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;
    187304}
    188305
     
    190307 * @brief processScopes
    191308 ** ------------------------------------------------------------------------------------------------------------- */
    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);
     309void 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 ** ------------------------------------------------------------------------------------------------------------- */
     345inline 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);
    293382        } 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
    357396}
    358397
     
    360399 * @brief processScope
    361400 ** ------------------------------------------------------------------------------------------------------------- */
    362 inline PabloBlock * BooleanReassociationPass::processScope(PabloFunction & f, PabloBlock * const block) {
     401inline void BooleanReassociationPass::distributeScope(PabloBlock * const block, CharacterizationMap & map) {
    363402    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 bottom-up 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 bottom-up 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    }
    528409}
    529410
     
    534415 * are "flattened" (i.e., allowed to have any number of inputs.)
    535416 ** ------------------------------------------------------------------------------------------------------------- */
    536 void BooleanReassociationPass::summarizeAST(PabloBlock * const block, Graph & G) const {
    537     Map M;
     417void BooleanReassociationPass::transformAST(PabloBlock * const block, CharacterizationMap & C, Graph & G) {
     418    StatementMap S;
    538419    // Compute the base def-use graph ...
    539420    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) {
    542425            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))) {
    556432            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);
    558434                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))) {
    562438            // To keep G a DAG, we need to do a bit of surgery on loop variants because
    563439            // the next variables it produces can be used within the condition. Instead,
     
    565441            // the Next node dependent on the loop.
    566442            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);
    568444                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);
    570447                remove_edge(v, u, G);
    571448                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
    580462}
    581463
     
    583465 * @brief resolveNestedUsages
    584466 ** ------------------------------------------------------------------------------------------------------------- */
    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);
     467void 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);
    588472        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);
    591474            if (LLVM_UNLIKELY(parent != block)) {
    592475                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();
    593488                    if (LLVM_UNLIKELY(parent == nullptr)) {
    594489                        assert (isa<Assign>(expr) || isa<Next>(expr));
    595490                        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
    678499
    679500/** ------------------------------------------------------------------------------------------------------------- *
     
    691512    for (auto u : A) {
    692513        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));
    695516            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));
    700522        }
    701523    }
     
    749571            }
    750572            std::sort(Aj.begin(), Aj.end());
     573            assert(std::unique(Aj.begin(), Aj.end()) == Aj.end());
    751574            VertexSet Ak;
    752575            Ak.reserve(std::min(Ai.size(), Aj.size()));
     
    821644 * there are not enough vertices in the biclique to make distribution profitable, eliminate the clique.
    822645 ** ------------------------------------------------------------------------------------------------------------- */
    823 static BicliqueSet && removeUnhelpfulBicliques(BicliqueSet && cliques, const DependencyGraph & G, DistributionGraph & H) {
     646static BicliqueSet && removeUnhelpfulBicliques(BicliqueSet && cliques, const Graph & G, DistributionGraph & H) {
    824647    for (auto ci = cliques.begin(); ci != cliques.end(); ) {
    825648        const auto cardinalityA = std::get<0>(*ci).size();
     
    844667 * @brief safeDistributionSets
    845668 ** ------------------------------------------------------------------------------------------------------------- */
    846 static DistributionSets safeDistributionSets(const DependencyGraph & G, DistributionGraph & H) {
     669static DistributionSets safeDistributionSets(const Graph & G, DistributionGraph & H) {
    847670
    848671    VertexSet sinks;
     
    866689
    867690/** ------------------------------------------------------------------------------------------------------------- *
     691 * @brief getVertex
     692 ** ------------------------------------------------------------------------------------------------------------- */
     693template<typename ValueType, typename GraphType, typename MapType>
     694static 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/** ------------------------------------------------------------------------------------------------------------- *
    868705 * @brief generateDistributionGraph
    869706 ** ------------------------------------------------------------------------------------------------------------- */
    870 void generateDistributionGraph(const DependencyGraph & G, DistributionGraph & H) {
     707void generateDistributionGraph(const Graph & G, DistributionGraph & H) {
    871708    DistributionMap M;
    872709    for (const Vertex u : make_iterator_range(vertices(G))) {
     
    893730            }
    894731            if (LLVM_LIKELY(distributable.size() > 1)) {
    895                 // We're only interested in computing a subgraph of G in which every source has an out-degree
    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;
    900733                for (const Vertex v : distributable) {
    901734                    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);
    924746                        }
    925747                    }
     
    935757 * Apply the distribution law to reduce computations whenever possible.
    936758 ** ------------------------------------------------------------------------------------------------------------- */
    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
     759bool BooleanReassociationPass::redistributeGraph(CharacterizationMap & C, StatementMap & M, Graph & G) const {
     760
     761    bool modified = false;
     762
     763    DistributionGraph H;
     764
     765    contractGraph(M, G);
    941766
    942767    for (;;) {
    943768
    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 to-be 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 ** ------------------------------------------------------------------------------------------------------------- */
     852inline 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 ** ------------------------------------------------------------------------------------------------------------- */
     869bool 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 ** ------------------------------------------------------------------------------------------------------------- */
     921inline 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 ** ------------------------------------------------------------------------------------------------------------- */
     935bool 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;
     979restart:        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 ** ------------------------------------------------------------------------------------------------------------- */
     1070bool 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 ** ------------------------------------------------------------------------------------------------------------- */
     1140bool 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
     1160inline bool isMutable(const Vertex u, const Graph & G) {
     1161    return getType(G[u]) != TypeId::Var;
     1162}
     1163
     1164/** ------------------------------------------------------------------------------------------------------------- *
     1165 * @brief rewriteAST
     1166 ** ------------------------------------------------------------------------------------------------------------- */
     1167void 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) {
    9501395            break;
    9511396        }
    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, "post-reassociation");
     1402    #endif
     1403
    10041404}
    10051405
     
    10071407 * @brief addSummaryVertex
    10081408 ** ------------------------------------------------------------------------------------------------------------- */
    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) {
     1409Vertex 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 ** ------------------------------------------------------------------------------------------------------------- */
     1423Vertex BooleanReassociationPass::makeVertex(const TypeId typeId, PabloAST * const expr, StatementMap & M, Graph & G, Z3_ast node) {
     1424    assert (expr);
    10171425    const auto f = M.find(expr);
    10181426    if (f != M.end()) {
     1427        assert (getValue(G[f->second]) == expr);
    10191428        return f->second;
    10201429    }
    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);
    10251432    return u;
    10261433}
    10271434
    1028 }
     1435/** ------------------------------------------------------------------------------------------------------------- *
     1436 * @brief addSummaryVertex
     1437 ** ------------------------------------------------------------------------------------------------------------- */
     1438Vertex 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 ** ------------------------------------------------------------------------------------------------------------- */
     1453inline 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 ** ------------------------------------------------------------------------------------------------------------- */
     1466inline 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 ** ------------------------------------------------------------------------------------------------------------- */
     1477inline 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 ** ------------------------------------------------------------------------------------------------------------- */
     1486inline 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 ** ------------------------------------------------------------------------------------------------------------- */
     1498inline 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 ** ------------------------------------------------------------------------------------------------------------- */
     1513inline 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 ** ------------------------------------------------------------------------------------------------------------- */
     1528inline 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/icgrep-devel/icgrep/pablo/optimizers/booleanreassociationpass.h

    r4871 r5152  
    33
    44#include <pablo/codegenstate.h>
     5#include <boost/graph/adjacency_list.hpp>
    56#include <boost/container/flat_map.hpp>
    6 #include <boost/graph/adjacency_list.hpp>
     7#include <z3.h>
    78
    89namespace pablo {
     
    1011class BooleanReassociationPass {
    1112public:
    12     using VertexData = std::pair<PabloAST::ClassTypeId, PabloAST *>;
     13    using VertexData = std::tuple<PabloAST::ClassTypeId, PabloAST *, Z3_ast>;
    1314    using Graph = boost::adjacency_list<boost::vecS, boost::vecS, boost::bidirectionalS, VertexData, PabloAST *>;
    1415    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
    1720    static bool optimize(PabloFunction & function);
     21
    1822protected:
    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
     41protected:
     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
    3172private:
    32     ScopeMap mResolvedScopes;
     73    Z3_context const            mContext;
     74    Z3_solver const             mSolver;
     75    Z3_ast                      mInFile;
     76    PabloFunction &             mFunction;
     77    bool                        mModified;
    3378};
    3479
Note: See TracChangeset for help on using the changeset viewer.