diff --git a/experimental/include/experimental/Support/BooleanLogic/BDD.h b/experimental/include/experimental/Support/BooleanLogic/BDD.h deleted file mode 100644 index 52c7fffc88..0000000000 --- a/experimental/include/experimental/Support/BooleanLogic/BDD.h +++ /dev/null @@ -1,54 +0,0 @@ -//===- BDD.h - BDD Decomposition for Bool Expressions --*-- C++ -*-===// -// -// Dynamatic is under the Apache License v2.0 with LLVM Exceptions. -// See https://llvm.org/LICENSE.txt for license information. -// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception -// -//===----------------------------------------------------------------------===// -// -// This file defines the functions for performing a BDD decomposition on -// boolean logic expression, following a specific order of variables. -// -//===----------------------------------------------------------------------===// - -#ifndef DYNAMATIC_SUPPORT_BDD_H -#define DYNAMATIC_SUPPORT_BDD_H - -#include "experimental/Support/BooleanLogic/BoolExpression.h" -#include - -namespace dynamatic { -namespace experimental { -namespace boolean { - -/// A BDD is a tree which represents a boolean expression by considering all the -/// outcomes of the expression as a decision tree, with two edges (positive and -/// negative) for each non terminal node. Each node is charaterized by a boolean -/// variable and possibly 2 subsequent nodes, stored into `successors` -struct BDD { - // First element is the `negative` branch; second is the `positive` branch - std::optional> successors; - BoolExpression *boolVariable; - - /// Build a BDD node with two descendents - BDD(BDD *ni, BDD *pi, BoolExpression *bv) - : successors({ni, pi}), boolVariable(bv) {} - - /// Build a leaf - BDD(BoolExpression *bv) : boolVariable(bv) {} -}; - -/// Replaces a boolean variable in a boolean expression with the specified truth -/// value -void restrict(BoolExpression *exp, const std::string &var, - bool expressionValue); - -/// Build a BDD out of an expression, by relying on the order of variables -/// provided -BDD *buildBDD(BoolExpression *exp, std::vector variableList); - -} // namespace boolean -} // namespace experimental -} // namespace dynamatic - -#endif // DYNAMATIC_SUPPORT_BDD_H diff --git a/experimental/include/experimental/Support/BooleanLogic/ROBDD.h b/experimental/include/experimental/Support/BooleanLogic/ROBDD.h new file mode 100644 index 0000000000..197c46386d --- /dev/null +++ b/experimental/include/experimental/Support/BooleanLogic/ROBDD.h @@ -0,0 +1,127 @@ +//===- ROBDD.h - ROBDD construction and analysis ----------------*- C++ -*-===// +// +// Dynamatic is under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception +// +//===----------------------------------------------------------------------===// +// +// This file provides a Reduced Ordered Binary Decision Diagram (ROBDD) builder +// and basic analysis utilities. A user-specified variable order is respected. +// +// Provided functionality: +// * ROBDD Construction from a minimized BoolExpression and a variable order. +// * Traversal of an ROBDD subgraph with a designated root and two designated +// sinks. +// * Enumeration of every vertex pair that covers all paths from the root to +// either sink inside that subgraph. +// +//===----------------------------------------------------------------------===// + +#ifndef DYNAMATIC_SUPPORT_ROBDD_H +#define DYNAMATIC_SUPPORT_ROBDD_H + +#include +#include +#include + +#include "experimental/Support/BooleanLogic/BoolExpression.h" +#include "mlir/Support/LogicalResult.h" + +namespace dynamatic { +namespace experimental { +namespace boolean { + +/// Replaces a boolean variable in a boolean expression with a truth value. +void restrict(BoolExpression *exp, const std::string &var, + bool expressionValue); + +/// One node of a reduced ordered BDD (ROBDD). +/// var : variable name (empty for terminals) +/// falseSucc : successor index when var evaluates to false +/// trueSucc : successor index when var evaluates to true +/// preds : indices of all predecessor nodes that point to this node +struct ROBDDNode { + std::string var; + unsigned falseSucc; + unsigned trueSucc; + std::vector preds; +}; + +/// Container for a reduced ordered BDD (ROBDD) built from a BoolExpression. +/// Each internal node is indexed by its position in the user-defined variable +/// order. Two additional nodes at the end are the 0 and 1 terminals. +class ROBDD { +public: + /// Create an empty ROBDD. + ROBDD(); + + /// Build a lightweight ROBDD for CFG reachability analysis. + /// + /// Unlike a general ROBDD which may have multiple nodes for the same variable + /// (representing different sub-functions), this specialized implementation + /// enforces a **one-node-per-variable** constraint. + /// + /// This design exploits the specific structure of CFG path conditions, + /// allowing for a simplified, linear-sized construction without the need for + /// a global unique-table for node deduplication. + mlir::LogicalResult + buildROBDDFromExpression(BoolExpression *expr, + const std::vector &varOrder); + + /// Traverse the subgraph reachable from `root` until either `tTrue` or + /// `tFalse` (treated as local sinks). Aborts if any path reaches the global + /// 0/1 terminals prematurely. Returns the list of node indices in the + /// subgraph (sorted in ascending order, always including `root`, `tTrue`, + /// `tFalse`). + std::vector collectSubgraph(unsigned root, unsigned tTrue, + unsigned tFalse) const; + + /// Enumerates all non-trivial pairs of vertices that cover all paths within + /// the subgraph defined by (root, tTrue, tFalse). Trivial covers (e.g., those + /// containing the root node or both terminals) are explicitly excluded from + /// the results. + /// + /// Returns pairs sorted lexicographically (first ascending, then second + /// ascending). + std::vector> + findPairsCoveringAllPaths(unsigned root, unsigned tTrue, + unsigned tFalse) const; + + /// Accessors. + const std::vector &getnodes() const { return nodes; } + const std::vector &getpreds(unsigned idx) const { + return nodes[idx].preds; + } + unsigned root() const { return rootIndex; } + unsigned one() const { return oneIndex; } + unsigned zero() const { return zeroIndex; } + +private: + /// Storage: internal nodes first, then terminals zeroIndex and oneIndex. + std::vector nodes; + + /// Variable order used to build the diagram (minimized & filtered). + std::vector order; + + /// Index of the ROBDD root node. + unsigned rootIndex = 0; + /// Index of the constant 0 terminal. + unsigned zeroIndex = 0; + /// Index of the constant 1 terminal. + unsigned oneIndex = 0; + + /// Build an OBDD via Shannon expansion per the filtered order. + void expandFrom(unsigned idx, BoolExpression *residual, + std::vector &expanded); + + /// Helper: test whether nodes `a` and `b` cover all paths. + bool doesPairCoverAllPaths(unsigned root, unsigned tTrue, unsigned tFalse, + unsigned a, unsigned b) const; +}; + +} // namespace boolean +} // namespace experimental +} // namespace dynamatic + +#endif // DYNAMATIC_SUPPORT_ROBDD_H diff --git a/experimental/lib/Analysis/GSAAnalysis.cpp b/experimental/lib/Analysis/GSAAnalysis.cpp index 1afdc9a5eb..c89d657e59 100644 --- a/experimental/lib/Analysis/GSAAnalysis.cpp +++ b/experimental/lib/Analysis/GSAAnalysis.cpp @@ -13,7 +13,7 @@ //===----------------------------------------------------------------------===// #include "experimental/Analysis/GSAAnalysis.h" -#include "experimental/Support/BooleanLogic/BDD.h" +#include "experimental/Support/BooleanLogic/ROBDD.h" #include "experimental/Support/FtdSupport.h" #include "mlir/Analysis/CFGLoopInfo.h" #include "mlir/Dialect/Func/IR/FuncOps.h" diff --git a/experimental/lib/Support/BooleanLogic/BDD.cpp b/experimental/lib/Support/BooleanLogic/BDD.cpp deleted file mode 100644 index 6135b0b311..0000000000 --- a/experimental/lib/Support/BooleanLogic/BDD.cpp +++ /dev/null @@ -1,84 +0,0 @@ -//===- BDD.cpp - BDD Decomposition for Bool Expressions -----*----- C++ -*-===// -// -// Dynamatic is under the Apache License v2.0 with LLVM Exceptions. -// See https://llvm.org/LICENSE.txt for license information. -// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception -// -//===----------------------------------------------------------------------===// -// -// This file implements the functions for performing a BDD decomposition on -// boolean logic expression, following a specific order of variables. -// -//===----------------------------------------------------------------------===// - -#include "experimental/Support/BooleanLogic/BDD.h" -#include "experimental/Support/BooleanLogic/BoolExpression.h" - -#include -#include -#include - -using namespace dynamatic::experimental::boolean; -using namespace llvm; - -void dynamatic::experimental::boolean::restrict(BoolExpression *exp, - const std::string &var, - bool expressionValue) { - - // If the input is a variable only, then possibly substitute the value with - // the provided one. If the expression is a binary one, recursively call - // `restrict` over the two inputs - if (exp->type == ExpressionType::Variable) { - SingleCond *singleCond = static_cast(exp); - if (singleCond->id == var) { - // Invert the value if complemented - if (singleCond->isNegated) - exp->type = - (expressionValue) ? ExpressionType::Zero : ExpressionType::One; - else - exp->type = - (expressionValue) ? ExpressionType::One : ExpressionType::Zero; - } - - } else if (exp->type == ExpressionType::And || - exp->type == ExpressionType::Or) { - Operator *op = static_cast(exp); - - if (op->left) - restrict(op->left, var, expressionValue); - - if (op->right) - restrict(op->right, var, expressionValue); - } -} - -BDD *dynamatic::experimental::boolean::buildBDD( - BoolExpression *exp, std::vector variableList) { - if (exp->type == ExpressionType::Variable || - exp->type == ExpressionType::Zero || exp->type == ExpressionType::One) - return new BDD(exp); - - // Get the next variable to expand - const std::string &var = variableList[0]; - - // Get a boolean expression in which `var` is substituted with false - BoolExpression *restrictedNegative = exp->deepCopy(); - restrict(restrictedNegative, var, false); - restrictedNegative = restrictedNegative->boolMinimize(); - - // Get a boolean expression in which `var` is substituted with true - BoolExpression *restrictedPositive = exp->deepCopy(); - restrict(restrictedPositive, var, true); - restrictedPositive = restrictedPositive->boolMinimize(); - - // Get a list of the next variables to expand - std::vector subList(std::next(variableList.begin()), - variableList.end()); - - // Recursively build the left and right sub-trees - BDD *negativeInput = buildBDD(restrictedNegative, subList); - BDD *positiveInput = buildBDD(restrictedPositive, subList); - auto *condition = new SingleCond(ExpressionType::Variable, var); - - return new BDD(negativeInput, positiveInput, condition); -} diff --git a/experimental/lib/Support/BooleanLogic/CMakeLists.txt b/experimental/lib/Support/BooleanLogic/CMakeLists.txt index c59e616dc0..cb1b839196 100644 --- a/experimental/lib/Support/BooleanLogic/CMakeLists.txt +++ b/experimental/lib/Support/BooleanLogic/CMakeLists.txt @@ -2,7 +2,7 @@ add_dynamatic_library(DynamaticExperimentalSupportBooleanLogic BoolExpression.cpp Lexer.cpp Parser.cpp - BDD.cpp + ROBDD.cpp LINK_LIBS PRIVATE DynamaticSupportEspresso diff --git a/experimental/lib/Support/BooleanLogic/ROBDD.cpp b/experimental/lib/Support/BooleanLogic/ROBDD.cpp new file mode 100644 index 0000000000..ee92fa38e2 --- /dev/null +++ b/experimental/lib/Support/BooleanLogic/ROBDD.cpp @@ -0,0 +1,324 @@ +//===- ROBDD.cpp - ROBDD construction and analysis --------------*- C++ -*-===// +// +// Dynamatic is under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception +// +//===----------------------------------------------------------------------===// +// +// This file implements construction of a Reduced Ordered Binary Decision +// Diagram (ROBDD) from a BoolExpression and basic analysis utilities. +// +//===----------------------------------------------------------------------===// + +#include "experimental/Support/BooleanLogic/ROBDD.h" +#include "experimental/Support/BooleanLogic/BoolExpression.h" + +#include +#include +#include +#include +#include +#include +#include + +#include "mlir/Support/LogicalResult.h" +#include "llvm/Support/raw_ostream.h" + +using namespace dynamatic::experimental::boolean; +using namespace llvm; +using namespace mlir; + +void dynamatic::experimental::boolean::restrict(BoolExpression *exp, + const std::string &var, + bool expressionValue) { + + // If the input is a variable only, then possibly substitute the value with + // the provided one. If the expression is a binary one, recursively call + // `restrict` over the two inputs + if (exp->type == ExpressionType::Variable) { + SingleCond *singleCond = static_cast(exp); + if (singleCond->id == var) { + // Invert the value if complemented + if (singleCond->isNegated) + exp->type = + (expressionValue) ? ExpressionType::Zero : ExpressionType::One; + else + exp->type = + (expressionValue) ? ExpressionType::One : ExpressionType::Zero; + } + + } else if (exp->type == ExpressionType::And || + exp->type == ExpressionType::Or) { + Operator *op = static_cast(exp); + + if (op->left) + restrict(op->left, var, expressionValue); + + if (op->right) + restrict(op->right, var, expressionValue); + } +} + +ROBDD::ROBDD() { + nodes.clear(); + order.clear(); + rootIndex = zeroIndex = oneIndex = 0; +} + +LogicalResult +ROBDD::buildROBDDFromExpression(BoolExpression *expr, + const std::vector &varOrder) { + nodes.clear(); + order.clear(); + rootIndex = zeroIndex = oneIndex = 0; + + if (!expr) { + llvm::errs() << "ROBDD: null expression\n"; + return failure(); + } + + // Minimize the whole expression once before starting. + BoolExpression *rootExpr = expr->boolMinimize(); + + // If the expression itself is constant, build only two terminals. + if (rootExpr->type == ExpressionType::Zero || + rootExpr->type == ExpressionType::One) { + nodes.resize(2); + zeroIndex = 0; + oneIndex = 1; + + // Terminals have no variables and no successors (indicated by specific + // sentinel values like UINT_MAX). Note: We create BOTH terminals to + // maintain valid zeroIndex/oneIndex invariants for the class, even if one + // of them is unreachable in this specific trivial graph. + nodes[zeroIndex] = {"", UINT_MAX, UINT_MAX, {}}; + nodes[oneIndex] = {"", UINT_MAX, UINT_MAX, {}}; + rootIndex = (rootExpr->type == ExpressionType::One) ? oneIndex : zeroIndex; + return success(); + } + + // Keep only variables that still appear after minimization and respect + // the order provided by the user. + std::set present = rootExpr->getVariables(); + for (const auto &v : varOrder) + if (present.find(v) != present.end()) + order.push_back(v); + + // Pre-allocate all internal nodes. + // Note: We initialize successors to UINT_MAX to indicate they are currently + // unconnected/dummies. These fields will be overwritten with actual indices + // during the expansion phase. + const unsigned n = (unsigned)order.size(); + nodes.resize(n + 2); + zeroIndex = n; + oneIndex = n + 1; + + for (unsigned i = 0; i < n; ++i) + nodes[i] = ROBDDNode{order[i], UINT_MAX, UINT_MAX, {}}; + + nodes[zeroIndex] = {"", UINT_MAX, UINT_MAX, {}}; + nodes[oneIndex] = {"", UINT_MAX, UINT_MAX, {}}; + + // Root is always the first internal node (smallest variable index). + rootIndex = 0; + + // Recursively expand edges from the root; mark each expanded node to + // avoid rebuilding the same subgraph. + std::vector expanded(nodes.size(), 0); + expandFrom(rootIndex, rootExpr, expanded); + + // After the BDD is fully built, clean up each node's predecessor list: + // sort in ascending order and remove any duplicates. + for (auto &nd : nodes) { + auto &ps = nd.preds; + std::sort(ps.begin(), ps.end()); + ps.erase(std::unique(ps.begin(), ps.end()), ps.end()); + } + + return success(); +} + +void ROBDD::expandFrom(unsigned idx, BoolExpression *residual, + std::vector &expanded) { + if (idx >= order.size() || expanded[idx]) + return; + + const std::string &var = order[idx]; + + // Perform Shannon expansion for the current variable. + BoolExpression *f0 = residual->deepCopy(); + restrict(f0, var, false); + f0 = f0->boolMinimize(); + BoolExpression *f1 = residual->deepCopy(); + restrict(f1, var, true); + f1 = f1->boolMinimize(); + + // Decide the next node index for each branch. + auto decideNext = [&](BoolExpression *f, unsigned &succ) { + if (!f) { + succ = zeroIndex; + return; + } + if (f->type == ExpressionType::Zero) { + succ = zeroIndex; + return; + } + if (f->type == ExpressionType::One) { + succ = oneIndex; + return; + } + + // Find the earliest variable in the current order that appears in f. + auto vars = f->getVariables(); + size_t vpos = order.size(); + for (size_t i = 0; i < order.size(); ++i) + if (vars.find(order[i]) != vars.end()) { + vpos = i; + break; + } + + succ = static_cast(vpos); + }; + + unsigned fSucc = zeroIndex, tSucc = oneIndex; + decideNext(f0, fSucc); + decideNext(f1, tSucc); + + // Connect edges for the current node. + nodes[idx].falseSucc = fSucc; + nodes[idx].trueSucc = tSucc; + + // While expanding the BDD, record the current node `idx` + // as a predecessor of each of its false/true successors. + nodes[fSucc].preds.push_back(idx); + nodes[tSucc].preds.push_back(idx); + + expanded[idx] = 1; + + // Recurse only on unexplored internal successors. + if (fSucc < zeroIndex && !expanded[fSucc]) + expandFrom(fSucc, f0, expanded); + if (tSucc < zeroIndex && !expanded[tSucc]) + expandFrom(tSucc, f1, expanded); +} + +std::vector ROBDD::collectSubgraph(unsigned rootNode, + unsigned trueTerminal, + unsigned falseTerminal) const { + std::vector visited(nodes.size(), 0); + std::vector workStack{rootNode}; + std::vector subgraph; + + while (!workStack.empty()) { + unsigned u = workStack.back(); + workStack.pop_back(); + + // Bounds check and visited check + if (u >= nodes.size() || visited[u]) + continue; + + visited[u] = 1; + subgraph.push_back(u); + + // Stop expansion at the designated local sinks. + if (u == trueTerminal || u == falseTerminal) + continue; + + // Abort if we accidentally reach the global terminals. + if (u == zeroIndex || u == oneIndex) { + llvm::errs() << "Illegal subgraph: reached global terminal\n"; + std::abort(); + } + + const auto &nd = nodes[u]; + workStack.push_back(nd.falseSucc); + workStack.push_back(nd.trueSucc); + } + + // Ensure both designated sinks appear in the final list (if they weren't + // reached). + if (std::find(subgraph.begin(), subgraph.end(), trueTerminal) == + subgraph.end()) + subgraph.push_back(trueTerminal); + if (std::find(subgraph.begin(), subgraph.end(), falseTerminal) == + subgraph.end()) + subgraph.push_back(falseTerminal); + + std::sort(subgraph.begin(), subgraph.end()); + return subgraph; +} + +bool ROBDD::doesPairCoverAllPaths(unsigned rootNode, unsigned trueTerminal, + unsigned falseTerminal, unsigned coverNodeA, + unsigned coverNodeB) const { + // Use a visited array to avoid cycles and redundant processing. + std::vector visited(nodes.size(), 0); + std::vector workStack{rootNode}; + + // Helper to push valid successors to the stack. + auto pushToStack = [&](unsigned v) { + // If we hit either of the covering nodes, the path is "blocked" or + // "covered" by them, so we stop traversing this path (effectively treating + // them as sinks). + if (v == coverNodeA || v == coverNodeB) + return; + + if (v < nodes.size() && !visited[v]) + workStack.push_back(v); + }; + + while (!workStack.empty()) { + unsigned u = workStack.back(); + workStack.pop_back(); + + // Standard DFS checks: bounds, visited, or hitting the cover nodes (double + // check). + if (u >= nodes.size() || visited[u] || u == coverNodeA || u == coverNodeB) + continue; + visited[u] = 1; + + // If we managed to reach either terminal without hitting coverNodeA or + // coverNodeB, then the pair does NOT cover all paths. + if (u == trueTerminal || u == falseTerminal) + return false; + + const auto &nd = nodes[u]; + pushToStack(nd.falseSucc); + pushToStack(nd.trueSucc); + } + + // If the stack is empty and we never reached a terminal, + // all paths were covered by the pair. + return true; +} + +std::vector> +ROBDD::findPairsCoveringAllPaths(unsigned rootNode, unsigned trueTerminal, + unsigned falseTerminal) const { + // Collect and validate the subgraph (sorted, includes root, trueTerminal, + // falseTerminal). + std::vector candidates = + collectSubgraph(rootNode, trueTerminal, falseTerminal); + std::vector> coveringPairs; + + // Scan all pairs in ascending order. + for (size_t i = 1; i < candidates.size() - 2; ++i) { + for (size_t j = i + 1; j < candidates.size(); ++j) { + if (doesPairCoverAllPaths(rootNode, trueTerminal, falseTerminal, + candidates[i], candidates[j])) { + coveringPairs.emplace_back(candidates[i], candidates[j]); + } + } + } + + // Sort lexicographically by (first, second). + std::sort(coveringPairs.begin(), coveringPairs.end(), + [](const auto &lhs, const auto &rhs) { + if (lhs.first != rhs.first) + return lhs.first < rhs.first; + return lhs.second < rhs.second; + }); + + return coveringPairs; +} \ No newline at end of file diff --git a/experimental/lib/Support/FtdImplementation.cpp b/experimental/lib/Support/FtdImplementation.cpp index c7ca948a71..0a42f5a84f 100644 --- a/experimental/lib/Support/FtdImplementation.cpp +++ b/experimental/lib/Support/FtdImplementation.cpp @@ -15,8 +15,8 @@ #include "experimental/Support/FtdImplementation.h" #include "dynamatic/Analysis/ControlDependenceAnalysis.h" #include "dynamatic/Support/Backedge.h" -#include "experimental/Support/BooleanLogic/BDD.h" #include "experimental/Support/BooleanLogic/BoolExpression.h" +#include "experimental/Support/BooleanLogic/ROBDD.h" #include "experimental/Support/FtdSupport.h" #include "mlir/Analysis/CFGLoopInfo.h" #include "mlir/Dialect/ControlFlow/IR/ControlFlowOps.h" @@ -291,7 +291,7 @@ static BoolExpression *getBlockLoopExitCondition(Block *loopExit, CFGLoop *loop, /// Run the Cytron algorithm to determine, give a set of values, in which blocks /// should we add a merge in order for those values to be merged static DenseSet -runCrytonAlgorithm(Region &funcRegion, DenseMap &inputBlocks) { +runCytronAlgorithm(Region &funcRegion, DenseMap &inputBlocks) { // Get dominance frontier auto dominanceFrontier = getDominanceFrontier(funcRegion); @@ -340,7 +340,7 @@ runCrytonAlgorithm(Region &funcRegion, DenseMap &inputBlocks) { LogicalResult experimental::ftd::createPhiNetwork( Region &funcRegion, PatternRewriter &rewriter, SmallVector &vals, - SmallVector &toSubstitue) { + SmallVector &toSubstitute) { if (vals.empty()) { llvm::errs() << "Input of \"createPhiNetwork\" is empty"; @@ -394,7 +394,7 @@ LogicalResult experimental::ftd::createPhiNetwork( // In which block a new phi is necessary DenseSet blocksToAddPhi = - runCrytonAlgorithm(funcRegion, inputBlocks); + runCytronAlgorithm(funcRegion, inputBlocks); // A backedge is created for each block in `blocksToAddPhi`, and it will // contain the value used as placeholder for the phi @@ -478,7 +478,7 @@ LogicalResult experimental::ftd::createPhiNetwork( inputPerBlock[&bb] = foundValue; } - for (auto &op : toSubstitue) + for (auto &op : toSubstitute) op->set(inputPerBlock[op->getOwner()->getBlock()]); return success(); @@ -692,62 +692,6 @@ static Value boolVariableToCircuit(PatternRewriter &rewriter, return condition; } -/// Get a circuit out a boolean expression, depending on the different kinds -/// of expressions you might have. -static Value boolExpressionToCircuit(PatternRewriter &rewriter, - BoolExpression *expr, Block *block, - const ftd::BlockIndexing &bi) { - - // Variable case - if (expr->type == ExpressionType::Variable) - return boolVariableToCircuit(rewriter, expr, block, bi); - - // Constant case (either 0 or 1) - rewriter.setInsertionPointToStart(block); - auto sourceOp = rewriter.create( - block->getOperations().front().getLoc()); - Value cnstTrigger = sourceOp.getResult(); - - auto intType = rewriter.getIntegerType(1); - auto cstAttr = rewriter.getIntegerAttr( - intType, (expr->type == ExpressionType::One ? 1 : 0)); - - auto constOp = rewriter.create( - block->getOperations().front().getLoc(), cstAttr, cnstTrigger); - - constOp->setAttr(FTD_OP_TO_SKIP, rewriter.getUnitAttr()); - - return constOp.getResult(); -} - -/// Convert a `BDD` object as obtained from the bdd expansion to a -/// circuit -static Value bddToCircuit(PatternRewriter &rewriter, BDD *bdd, Block *block, - const ftd::BlockIndexing &bi) { - if (!bdd->successors.has_value()) - return boolExpressionToCircuit(rewriter, bdd->boolVariable, block, bi); - - rewriter.setInsertionPointToStart(block); - - // Get the two operands by recursively calling `bddToCircuit` (it possibly - // creates other muxes in a hierarchical way) - SmallVector muxOperands; - muxOperands.push_back( - bddToCircuit(rewriter, bdd->successors.value().first, block, bi)); - muxOperands.push_back( - bddToCircuit(rewriter, bdd->successors.value().second, block, bi)); - Value muxCond = - boolExpressionToCircuit(rewriter, bdd->boolVariable, block, bi); - - // Create the multiplxer and add it to the rest of the circuit - auto muxOp = rewriter.create( - block->getOperations().front().getLoc(), muxOperands[0].getType(), - muxCond, muxOperands); - muxOp->setAttr(FTD_OP_TO_SKIP, rewriter.getUnitAttr()); - - return muxOp.getResult(); -} - // Returns true if loop is a while loop, detected by the loop header being // also a loop exit and not a loop latch static bool isWhileLoop(CFGLoop *loop) { @@ -766,6 +710,288 @@ static bool isWhileLoop(CFGLoop *loop) { !llvm::is_contained(latchBlocks, headerBlock); } +/// Build a MUX tree for an ROBDD subgraph delimited by +/// startIdx -> {trueSinkIdx, falseSinkIdx}. +/// Strategy: +/// 1) Enumerate all start–{true,false} all-paths-covering pairs (u,v) in +/// ascending order, each pair instantiates one MUX stage. 2) Input placement +/// per pair (u,v): +/// • Choose the largest common predecessor P of {u,v}. +/// Whichever endpoint equals P.trueSucc goes to the TRUE input; +/// the other goes to FALSE. +/// • If u and v are adjacent, the successive one's input is a terminal +/// constant (true-edge -> 1, false-edge -> 0). +/// 3) Chain the MUXes: select(mux[0]) is the start condition; for i>0, +/// select(mux[i]) = out(mux[i-1]). +/// 4) For non-constant inputs, recurse on the corresponding sub-region; +/// the recursion’s sinks are the next all-paths-covering pair or the +/// subgraph's sinks. +static Value buildMuxTree(PatternRewriter &rewriter, Block *block, + const ftd::BlockIndexing &bi, const ROBDD &robdd, + unsigned startIdx, unsigned trueSinkIdx, + unsigned falseSinkIdx) { + + const auto &nodes = robdd.getnodes(); + + // Look up the boolean signal for a given condition variable name and + // return it as the select input of a mux (converted to a handshake channel). + auto getSel = [&](const std::string &varName) -> Value { + auto condBlkOpt = bi.getBlockFromCondition(varName); + if (!condBlkOpt.has_value()) { + llvm::errs() << "convertRobddToCircuit: cannot map condition '" << varName + << "'.\n"; + return nullptr; + } + Value s = condBlkOpt.value()->getTerminator()->getOperand(0); + s.setType(ftd::channelifyType(s.getType())); + return s; + }; + + // Create a handshake boolean constant (0 or 1) as a channel signal. + // The returned Value can be connected directly to a mux input. + auto makeConst = [&](bool v) -> Value { + rewriter.setInsertionPointToStart(block); + auto src = rewriter.create( + block->getOperations().front().getLoc()); + auto i1 = rewriter.getIntegerType(1); + auto cst = rewriter.create( + block->getOperations().front().getLoc(), + rewriter.getIntegerAttr(i1, v ? 1 : 0), src.getResult()); + cst->setAttr(FTD_OP_TO_SKIP, rewriter.getUnitAttr()); + return cst.getResult(); + }; + + // Optional inversion for a selection. + auto maybeNot = [&](Value sel, bool invert) -> Value { + if (!invert) + return sel; + rewriter.setInsertionPointToStart(block); + auto notOp = rewriter.create( + block->getOperations().front().getLoc(), + ftd::channelifyType(sel.getType()), sel); + notOp->setAttr(FTD_OP_TO_SKIP, rewriter.getUnitAttr()); + return notOp.getResult(); + }; + + // Describes one mux data input: + // - isConst : true if this input is a boolean constant + // - constVal : value of the constant if isConst == true + // - nodeIdx : ROBDD node index if this input is driven by a variable + struct InputSpec { + bool isConst = false, constVal = false; + unsigned nodeIdx = 0; + }; + + // Decide how to connect the two vertices (u, v) of a pair to the false/true + // inputs of a mux. + auto decideInputsForPair = + [&](unsigned u, unsigned v) -> std::pair { + // Convert a ROBDD node index to an InputSpec. + auto nodeToSpec = [&](unsigned idx) -> InputSpec { + return {false, false, idx}; + }; + + // Check whether there is a direct edge from node a to node b: + // +1 if a.trueSucc == b (true edge) + // 0 if a.falseSucc == b (false edge) + // -1 if no direct edge from a to b + auto edge = [&](unsigned a, unsigned b) -> int { + if (nodes[a].trueSucc == b) + return +1; + if (nodes[a].falseSucc == b) + return 0; + return -1; + }; + + // Wrap the two vertices in the pair into InputSpec objects. + InputSpec specU = nodeToSpec(u); + InputSpec specV = nodeToSpec(v); + + // If there's a direct edge connecting u and v -> successor becomes + // constant. + int uv = edge(u, v), vu = edge(v, u); + if (uv != -1 && vu == -1) { + specV.isConst = true; + specV.constVal = (uv == +1); + } else if (vu != -1 && uv == -1) { + specU.isConst = true; + specU.constVal = (vu == +1); + } + + // The largest common predecessor decides who goes to true. + // nodes[].preds are already sorted in ascending order. + unsigned chosenP = 0; + const auto &predU = nodes[u].preds; + const auto &predV = nodes[v].preds; + size_t iu = 0, iv = 0; + while (iu < predU.size() && iv < predV.size()) { + if (predU[iu] == predV[iv]) { + if (predU[iu] > chosenP) + chosenP = predU[iu]; + ++iu; + ++iv; + } else if (predU[iu] < predV[iv]) { + ++iu; + } else { + ++iv; + } + } + + return (nodes[chosenP].trueSucc == specV.nodeIdx) ? std::pair{specU, specV} + : std::pair{specV, specU}; + }; + + // List all-paths-covering pairs (sorted). + auto pairs = + robdd.findPairsCoveringAllPaths(startIdx, trueSinkIdx, falseSinkIdx); + + // No pair -> no mux; return `start` condition with a possible Boolean + // negation. + if (pairs.empty()) { + // Root is a terminal: return constant value 1/0. + if (startIdx == trueSinkIdx) + return makeConst(true); + if (startIdx == falseSinkIdx) + return makeConst(false); + + bool dir = (nodes[startIdx].trueSucc == trueSinkIdx && + nodes[startIdx].falseSucc == falseSinkIdx); + bool inv = (nodes[startIdx].trueSucc == falseSinkIdx && + nodes[startIdx].falseSucc == trueSinkIdx); + + if (!dir && !inv) { + llvm::errs() + << "convertRobddToCircuit: start node doesn't map to sinks.\n"; + llvm::errs() << " Summary\n"; + llvm::errs() << " nodes.size = " << nodes.size() << "\n"; + llvm::errs() << " startIdx = " << startIdx << "\n"; + llvm::errs() << " trueSinkIdx = " << trueSinkIdx << "\n"; + llvm::errs() << " falseSinkIdx = " << falseSinkIdx << "\n"; + llvm::errs() << " trueSucc = " << nodes[startIdx].trueSucc << "\n"; + llvm::errs() << " falseSucc = " << nodes[startIdx].falseSucc << "\n"; + return nullptr; + } + + Value sel = getSel(nodes[startIdx].var); + if (!sel) + return nullptr; + return maybeNot(sel, inv); + } + + // Create handshake constants for Boolean false and true + Value c0 = makeConst(false); + Value c1 = makeConst(true); + + // Specification of one Mux stage + struct MuxSpec { + InputSpec inF, inT; + Value select, out; + Operation *op = nullptr; + }; + + // Build the list of mux stages from the given all-paths-covering pairs + // + // NOTE: The vector contains a sequence of path-covering vertex pairs + // sorted topologically from the root towards the sinks. Each pair represents + // a sequential stage in the decomposition. We construct a chain of Muxes + // where the i-th Mux corresponds to the i-th pair, and its selection is + // driven by the output of the (i-1)-th Mux (or the root variable for i=0). + std::vector muxChain; + muxChain.reserve(pairs.size()); + + for (auto [u, v] : pairs) { + auto [inF, inT] = decideInputsForPair(u, v); + muxChain.push_back(MuxSpec{inF, inT, nullptr, nullptr, nullptr}); + } + + // The first mux select signal comes from the starting variable + // Later muxes will use the previous mux output as select + muxChain[0].select = getSel(nodes[startIdx].var); + if (!muxChain[0].select) + return nullptr; + + // Create each mux with partial inputs; real variable inputs will be filled + // later + for (size_t i = 0; i < muxChain.size(); ++i) { + if (i > 0) + muxChain[i].select = muxChain[i - 1].out; + + Value inF = muxChain[i].inF.isConst ? (muxChain[i].inF.constVal ? c1 : c0) + : c0; // placeholder + Value inT = muxChain[i].inT.isConst ? (muxChain[i].inT.constVal ? c1 : c0) + : c0; // placeholder + + // Override constants for the last mux if an input is exactly a terminal + // node. This ignores inF/inT.constVal and uses the terminal identity + // instead. + if (i + 1 == muxChain.size()) { + if (muxChain[i].inF.nodeIdx == robdd.one()) + inF = c1; + else if (muxChain[i].inF.nodeIdx == robdd.zero()) + inF = c0; + if (muxChain[i].inT.nodeIdx == robdd.one()) + inT = c1; + else if (muxChain[i].inT.nodeIdx == robdd.zero()) + inT = c0; + } + + rewriter.setInsertionPointToStart(block); + auto mux = rewriter.create( + block->getOperations().front().getLoc(), c0.getType(), + muxChain[i].select, ValueRange{inF, inT}); + mux->setAttr(FTD_OP_TO_SKIP, rewriter.getUnitAttr()); + + muxChain[i].op = mux.getOperation(); + muxChain[i].out = mux.getResult(); + } + + // Helper lambda to set an operand of an operation at the given position + auto setOpnd = [&](Operation *op, int pos, Value v) { + op->setOperand(pos, v); + }; + + // Fill real inputs for each mux by recursion + // False/true sinks default to global sinks; if there is a next mux, use its + // inputs + for (size_t i = 0; i < muxChain.size(); ++i) { + unsigned subF = falseSinkIdx, subT = trueSinkIdx; + if (i + 1 < muxChain.size()) { + subF = muxChain[i + 1].inF.nodeIdx; + subT = muxChain[i + 1].inT.nodeIdx; + } + + if (!muxChain[i].inF.isConst) { + unsigned s = muxChain[i].inF.nodeIdx; + Value sub = buildMuxTree(rewriter, block, bi, robdd, s, subT, subF); + if (!sub) + return nullptr; + // operand index 1 = false + setOpnd(muxChain[i].op, 1, sub); + } + if (!muxChain[i].inT.isConst) { + unsigned s = muxChain[i].inT.nodeIdx; + Value sub = buildMuxTree(rewriter, block, bi, robdd, s, subT, subF); + if (!sub) + return nullptr; + // operand index 2 = true + setOpnd(muxChain[i].op, 2, sub); + } + } + + // Return the output of the last mux in the chain + return muxChain.back().out; +} + +/// Convert the entire ROBDD into a circuit by invoking buildMuxTree on the +/// ROBDD root with terminal nodes {one, zero}. The result is a MUX tree in +/// which each variable appears exactly once. +static Value convertRobddToCircuit(PatternRewriter &rewriter, Block *block, + const ftd::BlockIndexing &bi, + const ROBDD &robdd) { + return buildMuxTree(rewriter, block, bi, robdd, robdd.root(), robdd.one(), + robdd.zero()); +} + using PairOperandConsumer = std::pair; /// Insert a branch to the correct position, taking into account whether it @@ -826,12 +1052,14 @@ static Value addSuppressionInLoop(PatternRewriter &rewriter, CFGLoop *loop, // Sort the cofactors alphabetically std::sort(cofactorList.begin(), cofactorList.end()); - // Apply a BDD expansion to the loop exit expression and the list of - // cofactors - BDD *bdd = buildBDD(fLoopExit, cofactorList); - - // Convert the boolean expression obtained through BDD to a circuit - Value branchCond = bddToCircuit(rewriter, bdd, loopExit, bi); + // Build ROBDD on the loop-exit condition and lower to mux chain + ROBDD robdd; + if (failed(robdd.buildROBDDFromExpression(fLoopExit, cofactorList))) { + llvm::errs() << "ROBDD: buildROBDDFromExpression failed in " + "addSuppressionInLoop.\n"; + std::abort(); + } + Value branchCond = convertRobddToCircuit(rewriter, loopExit, bi, robdd); Operation *loopTerminator = loopExit->getTerminator(); assert(isa(loopTerminator) && @@ -936,8 +1164,16 @@ static void insertDirectSuppression( std::set blocks = fSup->getVariables(); std::vector cofactorList(blocks.begin(), blocks.end()); - BDD *bdd = buildBDD(fSup, cofactorList); - Value branchCond = bddToCircuit(rewriter, bdd, consumer->getBlock(), bi); + + // Build ROBDD and lower to mux tree + ROBDD robdd; + if (failed(robdd.buildROBDDFromExpression(fSup, cofactorList))) { + llvm::errs() << "ROBDD: buildROBDDFromExpression failed in " + "insertDirectSuppression.\n"; + std::abort(); + } + Value branchCond = + convertRobddToCircuit(rewriter, consumer->getBlock(), bi, robdd); rewriter.setInsertionPointToStart(consumer->getBlock()); auto branchOp = rewriter.create( @@ -969,7 +1205,7 @@ void ftd::addSuppOperandConsumer(PatternRewriter &rewriter, auto cda = ControlDependenceAnalysis(region).getAllBlockDeps(); // Skip the prod-cons if the producer is part of the operations related to - // the BDD expansion or INIT merges + // the ROBDD expansion or INIT merges if (consumerOp->hasAttr(FTD_OP_TO_SKIP) || consumerOp->hasAttr(FTD_INIT_MERGE)) return; @@ -1003,7 +1239,7 @@ void ftd::addSuppOperandConsumer(PatternRewriter &rewriter, return; // Skip the prod-cons if the consumer is part of the operations - // related to the BDD expansion or INIT merges + // related to the ROBDD expansion or INIT merges if (producerOp->hasAttr(FTD_OP_TO_SKIP) || producerOp->hasAttr(FTD_INIT_MERGE)) return;