source: icGREP/icgrep-devel/icgrep/pablo/optimizers/pablo_bddminimization.cpp @ 4725

Last change on this file since 4725 was 4725, checked in by nmedfort, 4 years ago

Temporary check-in.

File size: 21.7 KB
Line 
1#include "pablo_bddminimization.h"
2#include <pablo/codegenstate.h>
3#include <pablo/builder.hpp>
4#include <stack>
5#include <iostream>
6#include <pablo/printer_pablos.h>
7#include <cudd.h>
8#include <cuddInt.h>
9#include <util.h>
10#include <queue>
11#include <boost/circular_buffer.hpp>
12#include <pablo/optimizers/pablo_simplifier.hpp>
13#include <boost/container/flat_set.hpp>
14
15using namespace llvm;
16using namespace boost;
17using namespace boost::container;
18
19namespace pablo {
20
21bool BDDMinimizationPass::optimize(PabloFunction & function, const bool full) {
22    BDDMinimizationPass am;
23    am.eliminateLogicallyEquivalentStatements(function);
24    if (full) {
25        am.simplifyAST(function);
26    }
27    return Simplifier::optimize(function);
28}
29
30/** ------------------------------------------------------------------------------------------------------------- *
31 * @brief initialize
32 * @param vars the input vars for this program
33 * @param entry the entry block
34 *
35 * Scan through the program to identify any advances and calls then initialize the BDD engine with
36 * the proper variable ordering.
37 ** ------------------------------------------------------------------------------------------------------------- */
38void BDDMinimizationPass::eliminateLogicallyEquivalentStatements(PabloFunction & function) {
39
40    std::stack<Statement *> scope;
41    unsigned variableCount = 0; // number of statements that cannot always be categorized without generating a new variable
42
43    for (const Statement * stmt = function.getEntryBlock().front(); ; ) {
44        while ( stmt ) {
45            if (LLVM_UNLIKELY(isa<If>(stmt) || isa<While>(stmt))) {
46                // Set the next statement to be the first statement of the inner scope and push the
47                // next statement of the current statement into the scope stack.
48                const PabloBlock & nested = isa<If>(stmt) ? cast<If>(stmt)->getBody() : cast<While>(stmt)->getBody();
49                scope.push(stmt->getNextNode());
50                stmt = nested.front();
51                assert (stmt);
52                continue;
53            }
54            switch (stmt->getClassTypeId()) {
55                case PabloAST::ClassTypeId::Assign:
56                case PabloAST::ClassTypeId::Next:
57                case PabloAST::ClassTypeId::Advance:
58                case PabloAST::ClassTypeId::Call:
59                case PabloAST::ClassTypeId::MatchStar:
60                case PabloAST::ClassTypeId::ScanThru:
61                    variableCount++;
62                    break;                                   
63                default:
64                    break;
65            }
66            stmt = stmt->getNextNode();
67        }
68        if (scope.empty()) {
69            break;
70        }
71        stmt = scope.top();
72        scope.pop();
73    }
74
75    // Initialize the BDD engine ...
76    mManager = Cudd_Init(variableCount + function.getNumOfParameters() - function.getNumOfResults(), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0);
77    Cudd_MakeTreeNode(mManager, 0, function.getNumOfParameters(), MTR_DEFAULT);
78    // Map the predefined 0/1 entries
79    mCharacterizationMap[function.getEntryBlock().createZeroes()] = Zero();
80    mCharacterizationMap[function.getEntryBlock().createOnes()] = One();   
81    // Order the variables so the input Vars are pushed to the end; they ought to
82    // be the most complex to resolve.   
83    for (auto i = 0; i != function.getNumOfParameters(); ++i) {
84        mCharacterizationMap[function.getParameter(i)] = NewVar(function.getParameter(i));
85    }
86
87    SubsitutionMap baseMap;
88    baseMap.insert(Zero(), function.getEntryBlock().createZeroes());
89    baseMap.insert(One(), function.getEntryBlock().createOnes());
90
91    Cudd_AutodynEnable(mManager, CUDD_REORDER_LAZY_SIFT);
92
93    eliminateLogicallyEquivalentStatements(function.getEntryBlock(), baseMap);
94
95    Cudd_Quit(mManager);
96    mCharacterizationMap.clear();
97}
98
99/** ------------------------------------------------------------------------------------------------------------- *
100 * @brief characterize
101 * @param vars the input vars for this program
102 *
103 * Scan through the program and iteratively compute the BDDs for each statement.
104 ** ------------------------------------------------------------------------------------------------------------- */
105void BDDMinimizationPass::eliminateLogicallyEquivalentStatements(PabloBlock & block, SubsitutionMap & parent) {
106    SubsitutionMap subsitutionMap(&parent);
107    Statement * stmt = block.front();
108
109    while (stmt) {
110        if (LLVM_UNLIKELY(isa<If>(stmt))) {
111            eliminateLogicallyEquivalentStatements(cast<If>(stmt)->getBody(), subsitutionMap);
112        } else if (LLVM_UNLIKELY(isa<While>(stmt))) {
113            eliminateLogicallyEquivalentStatements(cast<While>(stmt)->getBody(), subsitutionMap);
114        } else { // attempt to characterize this statement and replace it if
115            DdNode * bdd = eliminateLogicallyEquivalentStatements(stmt);
116            if (LLVM_LIKELY(!isa<Assign>(stmt) && !isa<Next>(stmt))) {
117                PabloAST * replacement = subsitutionMap[bdd];
118                if (replacement) {
119                    Cudd_RecursiveDeref(mManager, bdd);
120                    stmt = stmt->replaceWith(replacement, false, true);
121                    continue;
122                }
123                subsitutionMap.insert(bdd, stmt);
124            }
125            mCharacterizationMap.insert(std::make_pair(stmt, bdd));
126        }
127        stmt = stmt->getNextNode();
128    }
129    Cudd_ReduceHeap(mManager, CUDD_REORDER_SIFT, 0);
130}
131
132/** ------------------------------------------------------------------------------------------------------------- *
133 * @brief characterize
134 ** ------------------------------------------------------------------------------------------------------------- */
135inline DdNode * BDDMinimizationPass::eliminateLogicallyEquivalentStatements(const Statement * const stmt) {
136
137    DdNode * bdd = nullptr;
138    // Map our operands to the computed BDDs
139    std::array<DdNode *, 3> input;
140    for (unsigned i = 0; i != stmt->getNumOperands(); ++i) {
141        PabloAST * const op = stmt->getOperand(i);
142        if (op == nullptr) {
143            throw std::runtime_error("Statement has Null operand!");
144        }
145        if (LLVM_UNLIKELY(isa<Integer>(op) || isa<String>(op))) {
146            continue;
147        }
148        auto f = mCharacterizationMap.find(op);
149        if (LLVM_UNLIKELY(f == mCharacterizationMap.end())) {
150            throw std::runtime_error("Error in AST: attempted to characterize statement with unknown operand!");
151        }
152        input[i] = f->second;
153    }
154
155    switch (stmt->getClassTypeId()) {
156        case PabloAST::ClassTypeId::Assign:
157        case PabloAST::ClassTypeId::Next:
158            return input[0];
159        case PabloAST::ClassTypeId::And:
160            bdd = And(input[0], input[1]);
161            break;       
162        case PabloAST::ClassTypeId::Or:
163            bdd = Or(input[0], input[1]);
164            break;
165        case PabloAST::ClassTypeId::Xor:
166            bdd = Xor(input[0], input[1]);
167            break;
168        case PabloAST::ClassTypeId::Not:
169            bdd = Not(input[0]);
170            break;
171        case PabloAST::ClassTypeId::Sel:
172            bdd = Ite(input[0], input[1], input[2]);
173            break;
174        case PabloAST::ClassTypeId::Call:
175            // TODO: we may have more than one output. Need to fix call class to allow for it.
176        case PabloAST::ClassTypeId::Advance:
177        case PabloAST::ClassTypeId::MatchStar:
178        case PabloAST::ClassTypeId::ScanThru:
179            return NewVar(stmt);
180        default:
181            throw std::runtime_error("Unexpected statement type " + stmt->getName()->to_string());
182    }
183
184    Cudd_Ref(bdd);
185
186    if (LLVM_UNLIKELY(noSatisfyingAssignment(bdd))) {
187        Cudd_RecursiveDeref(mManager, bdd);
188        bdd = Zero();
189    }
190
191    return bdd;
192}
193
194/** ------------------------------------------------------------------------------------------------------------- *
195 * @brief simplifyAST
196 ** ------------------------------------------------------------------------------------------------------------- */
197inline void BDDMinimizationPass::simplifyAST(PabloFunction & function) {
198    PabloBuilder builder(function.getEntryBlock());
199    std::vector<Statement *> terminals;
200    for (unsigned i = 0; i != function.getNumOfResults(); ++i) {
201        terminals.push_back(function.getResult(i));
202    }
203    simplifyAST(builder, terminals);
204}
205
206/** ------------------------------------------------------------------------------------------------------------- *
207 * @brief isSimplifiable
208 ** ------------------------------------------------------------------------------------------------------------- */
209inline bool isSimplifiable(const PabloAST * const expr, const PabloBlock * const pb) {
210    switch (expr->getClassTypeId()) {
211        case PabloAST::ClassTypeId::And:
212        case PabloAST::ClassTypeId::Or:
213        case PabloAST::ClassTypeId::Not:
214        case PabloAST::ClassTypeId::Sel:
215            return cast<Statement>(expr)->getParent() == pb;
216        default:
217            return false;
218    }
219}
220
221/** ------------------------------------------------------------------------------------------------------------- *
222 * @brief simplifyAST
223 ** ------------------------------------------------------------------------------------------------------------- */
224void BDDMinimizationPass::simplifyAST(PabloBuilder & block, std::vector<Statement *> & terminals) {
225
226    for (Statement * stmt : block) {
227        if (isa<While>(stmt)) {
228            PabloBuilder builder(cast<If>(stmt)->getBody(), block);
229            std::vector<Statement *> terminals;
230            for (Assign * var : cast<const If>(stmt)->getDefined()) {
231                terminals.push_back(var);
232            }
233            simplifyAST(builder, terminals);
234            for (Assign * var : cast<const If>(stmt)->getDefined()) {
235                block.record(var);
236            }
237            continue;
238        } else if (isa<While>(stmt)) {
239            PabloBuilder builder(cast<While>(stmt)->getBody(), block);
240            std::vector<Statement *> terminals;
241            for (Next * var : cast<const While>(stmt)->getVariants()) {
242                terminals.push_back(var);
243            }
244            simplifyAST(builder, terminals);
245            for (Next * var : cast<const While>(stmt)->getVariants()) {
246                block.record(var);
247            }
248            continue;
249        }
250        block.record(stmt);
251    }
252
253    std::queue<Statement *> Q;
254    std::vector<PabloAST *> variables;
255
256    while (!terminals.empty()) {
257
258        for (Statement * term : terminals) {
259            Q.push(term);
260        }
261
262        // find the variables for this set of terminals
263        for (;;) {
264            Statement * stmt = Q.front();
265            Q.pop();
266            mCharacterizationMap[stmt] = nullptr;
267            for (unsigned i = 0; i != stmt->getNumOperands(); ++i) {
268                if (isSimplifiable(stmt->getOperand(i), stmt->getParent())) {
269                    Q.push(cast<Statement>(stmt->getOperand(i)));
270                } else {
271                    variables.push_back(stmt->getOperand(i));
272                }
273            }
274            if (Q.empty()) {
275                break;
276            }
277        }
278
279        std::sort(variables.begin(), variables.end());
280        std::unique(variables.begin(), variables.end());
281
282
283        mManager = Cudd_Init(variables.size(), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0);
284        Cudd_AutodynEnable(mManager, CUDD_REORDER_LAZY_SIFT);
285
286        unsigned i = 0;
287        for (PabloAST * var : variables) {
288            mCharacterizationMap[var] = Cudd_bddIthVar(mManager, i++);
289        }
290
291        for (PabloAST * term : terminals) {
292            characterizeTerminalBddTree(term);
293        }
294        Cudd_ReduceHeap(mManager, CUDD_REORDER_SIFT, 0);
295
296        for (Statement * term : terminals) {
297            DdNode * const f = mCharacterizationMap[term];
298            Cudd_Ref(f);
299            PabloAST * replacement = simplifyAST(f, variables, block);
300            if (replacement) {
301                term->replaceWith(replacement, false, true);
302            }
303            Cudd_RecursiveDeref(mManager, f);
304        }
305
306        Cudd_Quit(mManager);
307
308        mCharacterizationMap.clear();
309
310        // Now clear our terminals and test whether we can process another layer within this block
311        terminals.clear();
312        for (PabloAST * var : variables) {
313            if (isa<Statement>(var) && cast<Statement>(var)->getParent() == block.getPabloBlock()) {
314                terminals.push_back(cast<Statement>(var));
315            }
316        }
317    }
318
319}
320
321///** ------------------------------------------------------------------------------------------------------------- *
322// * @brief simplifyAST
323// ** ------------------------------------------------------------------------------------------------------------- */
324DdNode * BDDMinimizationPass::characterizeTerminalBddTree(PabloAST * expr) {
325
326    const auto f = mCharacterizationMap.find(expr);
327    if (f == mCharacterizationMap.end()) {
328        return nullptr;
329    } else if (f->second) {
330        return f->second;
331    }
332
333    Statement * stmt = cast<Statement>(expr);
334    std::array<DdNode *, 3> input;
335
336    for (unsigned i = 0; i != stmt->getNumOperands(); ++i) {
337        input[i] = characterizeTerminalBddTree(stmt->getOperand(i));
338    }
339
340    DdNode * bdd = nullptr;
341    switch (expr->getClassTypeId()) {
342        case PabloAST::ClassTypeId::And:
343            bdd = And(input[0], input[1]);
344            break;
345        case PabloAST::ClassTypeId::Or:
346            bdd = Or(input[0], input[1]);
347            break;
348        case PabloAST::ClassTypeId::Not:
349            bdd = Not(input[0]);
350            break;
351        case PabloAST::ClassTypeId::Sel:
352            bdd = Ite(input[0], input[1], input[2]);
353            break;
354        default:
355            throw std::runtime_error("Unexpected operand given to BDDMinimizationPass::characterizeTerminalBddTree!");
356    }
357    Cudd_Ref(bdd);
358    return bdd;
359}
360
361/** ------------------------------------------------------------------------------------------------------------- *
362 * @brief simplifyAST
363 ** ------------------------------------------------------------------------------------------------------------- */
364PabloAST * BDDMinimizationPass::simplifyAST(DdNode * const f, const std::vector<PabloAST *> & variables, PabloBuilder & builder) {
365    assert (!noSatisfyingAssignment(f));
366    DdNode * g = Cudd_FindEssential(mManager, f);
367    if (g && Cudd_SupportSize(mManager, g) > 0) {
368        if (g == f) { // every variable is essential
369            return makeCoverAST(f, variables, builder);
370        }
371        Cudd_Ref(g);
372        PabloAST * c0 = makeCoverAST(g, variables, builder);
373        if (LLVM_UNLIKELY(c0 == nullptr)) {
374            Cudd_RecursiveDeref(mManager, g);
375            return nullptr;
376        }
377        DdNode * h = Cudd_Cofactor(mManager, f, g);
378        Cudd_Ref(h);
379        PabloAST * c1 = simplifyAST(h, variables, builder);
380        if (LLVM_UNLIKELY(c1 == nullptr)) {
381            Cudd_RecursiveDeref(mManager, g);
382            Cudd_RecursiveDeref(mManager, h);
383            cast<Statement>(c0)->eraseFromParent(true);
384            return nullptr;
385        }
386        assert (And(g, h) == f);
387        Cudd_RecursiveDeref(mManager, g);
388        Cudd_RecursiveDeref(mManager, h);
389        return builder.createAnd(c0, c1, "escf");
390    }
391
392    DdNode ** disjunct = nullptr;
393    int disjuncts = Cudd_bddIterDisjDecomp(mManager, f, &disjunct);
394    assert (disjuncts < 2 || Or(disjunct[0], disjunct[1]) == f);
395
396    DdNode ** conjunct = nullptr;
397    int conjuncts = Cudd_bddIterConjDecomp(mManager, f, &conjunct);
398    assert (conjuncts < 2 || And(conjunct[0], conjunct[1]) == f);
399
400    if (LLVM_LIKELY(disjuncts == 2 && conjuncts == 2)) {
401        if (Cudd_SharingSize(disjunct, 2) > Cudd_SharingSize(conjunct, 2)) {
402            disjuncts = 0;
403        }
404    }
405
406    DdNode * decomp[] = { nullptr, nullptr };
407    if (disjuncts == 2) {
408        memcpy(decomp, disjunct, sizeof(DdNode *) * 2);
409    } else if (conjuncts == 2) {
410        memcpy(decomp, conjunct, sizeof(DdNode *) * 2);
411    }
412
413    FREE(disjunct);
414    FREE(conjunct);
415
416    if ((decomp[0] != decomp[1]) && (decomp[0] != f) && (decomp[1] != f)) {
417        Cudd_Ref(decomp[0]);
418        Cudd_Ref(decomp[1]);
419        PabloAST * d0 = simplifyAST(decomp[0], variables, builder);
420        Cudd_RecursiveDeref(mManager, decomp[0]);
421        if (LLVM_UNLIKELY(d0 == nullptr)) {
422            Cudd_RecursiveDeref(mManager, decomp[1]);
423            return nullptr;
424        }
425
426        PabloAST * d1 = simplifyAST(decomp[1], variables, builder);
427        Cudd_RecursiveDeref(mManager, decomp[1]);
428        if (LLVM_UNLIKELY(d1 == nullptr)) {
429            cast<Statement>(d0)->eraseFromParent(true);
430            return nullptr;
431        }
432
433        if (disjuncts == 2) {
434            return builder.createOr(d0, d1, "disj");
435        } else {
436            return builder.createAnd(d0, d1, "conj");
437        }
438    }
439    return makeCoverAST(f, variables, builder);
440}
441
442/** ------------------------------------------------------------------------------------------------------------- *
443 * @brief makeCoverAST
444 ** ------------------------------------------------------------------------------------------------------------- */
445PabloAST * BDDMinimizationPass::makeCoverAST(DdNode * const f, const std::vector<PabloAST *> & variables, PabloBuilder & builder) {
446
447    std::queue<PabloAST *> SQ;
448    const unsigned n = variables.size();
449    circular_buffer<PabloAST *> CQ(n);
450    circular_buffer<PabloAST *> DQ(n);
451
452    assert (mManager->size == variables.size());
453
454    int cube[n];
455
456    DdNode * g = f;
457
458    Cudd_Ref(g);
459
460    while (g != Cudd_ReadLogicZero(mManager)) {
461        int length = 0;
462        DdNode * implicant = Cudd_LargestCube(mManager, g, &length);
463        if (LLVM_UNLIKELY(implicant == nullptr)) {
464            Cudd_RecursiveDeref(mManager, g);
465            return nullptr;
466        }
467        Cudd_Ref(implicant);
468        DdNode * prime = Cudd_bddMakePrime(mManager, implicant, f);
469        if (LLVM_UNLIKELY(prime == nullptr)) {
470            Cudd_RecursiveDeref(mManager, g);
471            Cudd_RecursiveDeref(mManager, implicant);
472            return nullptr;
473        }
474        Cudd_Ref(prime);
475        Cudd_RecursiveDeref(mManager, implicant);
476
477        DdNode * h = Cudd_bddAnd(mManager, g, Cudd_Not(prime));
478        if (LLVM_UNLIKELY(h == nullptr)) {
479            Cudd_RecursiveDeref(mManager, g);
480            Cudd_RecursiveDeref(mManager, prime);
481            return nullptr;
482        }
483        Cudd_Ref(h);
484        Cudd_RecursiveDeref(mManager, g);
485
486        g = h;
487        if (LLVM_UNLIKELY(Cudd_BddToCubeArray(mManager, prime, cube) == 0)) {
488            Cudd_RecursiveDeref(mManager, g);
489            Cudd_RecursiveDeref(mManager, prime);
490            return nullptr;
491        }
492        Cudd_RecursiveDeref(mManager, prime);
493
494        assert (DQ.empty() && CQ.empty());
495
496        for (auto i = 0; i != n; ++i) {
497            assert (cube[i] >= 0 && cube[i] <= 2);
498            if (cube[i] == 0) {
499                assert (!DQ.full());
500                DQ.push_back(variables[i]);
501            } else if (cube[i] == 1) {
502                assert (!CQ.full());
503                CQ.push_back(variables[i]);
504            }
505        }
506
507        if (LLVM_UNLIKELY(DQ.empty() && CQ.empty())) {
508            throw std::runtime_error("Error! statement contains no elements!");
509        }
510
511        if (DQ.size() > 0) {
512            while (DQ.size() > 1) {
513                PabloAST * v1 = DQ.front(); DQ.pop_front();
514                PabloAST * v2 = DQ.front(); DQ.pop_front();
515                DQ.push_back(builder.createOr(v1, v2));
516            }
517            CQ.push_back(builder.createNot(DQ.front()));
518            DQ.pop_front();
519        }
520
521        assert (!CQ.empty());
522        while (CQ.size() > 1) {
523            PabloAST * v1 = CQ.front(); CQ.pop_front();
524            PabloAST * v2 = CQ.front(); CQ.pop_front();
525            CQ.push_back(builder.createAnd(v1, v2));
526        }
527        SQ.push(CQ.front()); CQ.pop_front();
528    }
529    Cudd_RecursiveDeref(mManager, g);
530    if (LLVM_UNLIKELY(SQ.empty())) {
531        throw std::runtime_error("Error! statement queue empty!");
532    }
533    while (SQ.size() > 1) {
534        PabloAST * v1 = SQ.front(); SQ.pop();
535        PabloAST * v2 = SQ.front(); SQ.pop();
536        SQ.push(builder.createOr(v1, v2));
537    }
538    return SQ.front();
539}
540
541/** ------------------------------------------------------------------------------------------------------------- *
542 * @brief CUDD wrappers
543 ** ------------------------------------------------------------------------------------------------------------- */
544
545inline DdNode * BDDMinimizationPass::Zero() const {
546    return Cudd_ReadLogicZero(mManager);
547}
548
549inline DdNode * BDDMinimizationPass::One() const {
550    return Cudd_ReadOne(mManager);
551}
552
553inline DdNode * BDDMinimizationPass::NewVar(const PabloAST * expr) {
554    DdNode * var = Cudd_bddIthVar(mManager, mVariables.size());
555    mVariables.push_back(const_cast<PabloAST *>(expr));
556    return var;
557}
558
559inline bool BDDMinimizationPass::isZero(DdNode * const x) const {
560    return x == Zero();
561}
562
563inline DdNode * BDDMinimizationPass::And(DdNode * const x, DdNode * const y) {
564    DdNode * r = Cudd_bddAnd(mManager, x, y);
565    return r;
566}
567
568inline DdNode * BDDMinimizationPass::Intersect(DdNode * const x, DdNode * const y) {
569    DdNode * r = Cudd_bddIntersect(mManager, x, y); Cudd_Ref(r);
570    return r;
571}
572
573inline DdNode * BDDMinimizationPass::Or(DdNode * const x, DdNode * const y) {
574    DdNode * r = Cudd_bddOr(mManager, x, y);
575    return r;
576}
577
578inline DdNode * BDDMinimizationPass::Xor(DdNode * const x, DdNode * const y) {
579    DdNode * r = Cudd_bddXor(mManager, x, y);
580    return r;
581}
582
583inline DdNode * BDDMinimizationPass::Not(DdNode * const x) const {
584    return Cudd_Not(x);
585}
586
587inline DdNode * BDDMinimizationPass::Ite(DdNode * const x, DdNode * const y, DdNode * const z) {
588    DdNode * r = Cudd_bddIte(mManager, x, y, z);
589    return r;
590}
591
592inline bool BDDMinimizationPass::noSatisfyingAssignment(DdNode * const x) {
593    return Cudd_bddLeq(mManager, x, Zero());
594}
595
596inline void BDDMinimizationPass::shutdown() {
597    Cudd_Quit(mManager);
598}
599
600} // end of namespace pablo
601
Note: See TracBrowser for help on using the repository browser.