23958770921

Committed 03 Apr 2026 07:13PM UTC coverage: 64.782% (-0.03%) from 64.815%

Build # 23958770921

Build Type

Pull #643

github

Committed by

web-flow

Commit Message

Merge 05adaeb24 into 951590cfc

Pull Request Pull Request #643: Replaces LoopNormalization by LoopNormalForm pass

Run Details

110 of 184 new or added lines in 2 files covered. (59.78%)

5 existing lines in 2 files now uncovered.

29108 of 44932 relevant lines covered (64.78%)

561.63 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

60.34

/opt/src/transformations/loop_condition_normalize.cpp

#include "sdfg/transformations/loop_condition_normalize.h"

#include <stdexcept>

#include "sdfg/builder/structured_sdfg_builder.h"
#include "sdfg/structured_control_flow/map.h"
#include "sdfg/symbolic/conjunctive_normal_form.h"
#include "sdfg/symbolic/polynomials.h"
#include "sdfg/symbolic/symbolic.h"

/**
 * Loop Condition Normalize Transformation Implementation
 *
 * This transformation converts `!=` (Unequality) conditions to relational comparisons
 * (`<` or `>`) based on the loop's stride direction.
 *
 * Algorithm:
 * 1. Check that stride is ±1 (unit stride)
 * 2. Convert condition to CNF
 * 3. For each Unequality literal involving the indvar:
 *    a. Normalize to form: indvar != bound (solve for indvar if affine)
 *    b. Based on stride sign:
 *       - stride = +1: convert to indvar < bound
 *       - stride = -1: convert to indvar > bound
 * 4. Reconstruct the condition from the modified CNF
 *
 * The transformation assumes LLVM-style well-formed loops where the bound is
 * reachable from init. For a loop `for (i = 0; i != N; i++)`, we trust that
 * N >= 0 (loop will eventually reach N).
 */

namespace sdfg {
namespace transformations {

LoopConditionNormalize::LoopConditionNormalize(structured_control_flow::StructuredLoop& loop) : loop_(loop) {}

std::string LoopConditionNormalize::name() const { return "LoopConditionNormalize"; }

bool LoopConditionNormalize::
    can_be_applied(builder::StructuredSDFGBuilder& builder, analysis::AnalysisManager& analysis_manager) {
    // Check for unit stride (±1)
    auto stride = loop_.stride();
    if (stride.is_null()) {
        return false;
    }
    auto stride_int = stride->as_int();
    if (stride_int != 1 && stride_int != -1) {
        return false;
    }

    // Convert condition to CNF
    symbolic::CNF cnf;
    try {
        cnf = symbolic::conjunctive_normal_form(loop_.condition());
    } catch (...) {
        return false;
    }

    auto indvar = loop_.indvar();

    // Check if there's at least one Unequality or Equality involving indvar
    bool has_convertible = false;
    for (const auto& clause : cnf) {
        for (const auto& literal : clause) {
            if (SymEngine::is_a<SymEngine::Unequality>(*literal) || SymEngine::is_a<SymEngine::Equality>(*literal)) {
                SymEngine::RCP<const SymEngine::Basic> lhs, rhs;

                if (SymEngine::is_a<SymEngine::Unequality>(*literal)) {
                    auto ne = SymEngine::rcp_static_cast<const SymEngine::Unequality>(literal);
                    lhs = ne->get_arg1();
                    rhs = ne->get_arg2();
                } else {
                    auto eq = SymEngine::rcp_static_cast<const SymEngine::Equality>(literal);
                    lhs = eq->get_arg1();
                    rhs = eq->get_arg2();
                }

                // Check if indvar is involved
                bool lhs_has_indvar = symbolic::uses(lhs, indvar->get_name());
                bool rhs_has_indvar = symbolic::uses(rhs, indvar->get_name());

                if (!lhs_has_indvar && !rhs_has_indvar) {
                    // indvar not involved, skip
                    continue;
                }

                if (lhs_has_indvar && rhs_has_indvar) {
                    // indvar on both sides, can't normalize
                    continue;
                }

                // One side has indvar - check if affine
                auto expr_with_indvar = lhs_has_indvar ? lhs : rhs;
                symbolic::SymbolVec syms = {indvar};
                auto poly = symbolic::polynomial(expr_with_indvar, syms);
                if (poly.is_null()) {
                    continue;
                }

                auto coeffs = symbolic::affine_coefficients(poly, syms);
                if (coeffs.empty() || coeffs.find(indvar) == coeffs.end()) {
                    continue;
                }

                // Coefficient must be a non-zero integer
                auto coeff = coeffs.at(indvar);
                if (!SymEngine::is_a<SymEngine::Integer>(*coeff)) {
                    continue;
                }
                auto coeff_int = SymEngine::rcp_static_cast<const SymEngine::Integer>(coeff)->as_int();
                // Only allow coefficient = 1 (simple i != bound case)
                // Coefficient != 1 (e.g., 2*i + 1 != N) is unsafe because
                // we can't guarantee the bound will be hit (depends on divisibility)
                if (coeff_int != 1) {
                    continue;
                }

                has_convertible = true;
                break;
            }
        }
        if (has_convertible) {
            break;
        }
    }

    return has_convertible;
}

void LoopConditionNormalize::apply(builder::StructuredSDFGBuilder& builder, analysis::AnalysisManager& analysis_manager) {
    auto indvar = loop_.indvar();
    auto stride = loop_.stride();
    auto stride_int = stride->as_int();

    // Convert condition to CNF
    symbolic::CNF cnf = symbolic::conjunctive_normal_form(loop_.condition());

    // Build a new CNF with converted literals
    symbolic::CNF new_cnf;

    for (const auto& clause : cnf) {
        std::vector<symbolic::Condition> new_clause;

        for (const auto& literal : clause) {
            if (!SymEngine::is_a<SymEngine::Unequality>(*literal) && !SymEngine::is_a<SymEngine::Equality>(*literal)) {
                // Keep non-equality/inequality literals as-is
                new_clause.push_back(literal);
                continue;
            }

            bool is_unequality = SymEngine::is_a<SymEngine::Unequality>(*literal);
            SymEngine::RCP<const SymEngine::Basic> lhs, rhs;

            if (is_unequality) {
                auto ne = SymEngine::rcp_static_cast<const SymEngine::Unequality>(literal);
                lhs = ne->get_arg1();
                rhs = ne->get_arg2();
            } else {
                auto eq = SymEngine::rcp_static_cast<const SymEngine::Equality>(literal);
                lhs = eq->get_arg1();
                rhs = eq->get_arg2();
            }

            bool lhs_has_indvar = symbolic::uses(lhs, indvar->get_name());
            bool rhs_has_indvar = symbolic::uses(rhs, indvar->get_name());

            if (!lhs_has_indvar && !rhs_has_indvar) {
                // indvar not involved, keep as-is
                new_clause.push_back(literal);
                continue;
            }

            if (lhs_has_indvar && rhs_has_indvar) {
                // indvar on both sides, keep as-is
                new_clause.push_back(literal);
                continue;
            }

            // Ensure indvar is on LHS
            if (!lhs_has_indvar) {
                std::swap(lhs, rhs);
            }

            // LHS now has indvar, RHS does not
            // Normalize: coeff * indvar + offset != rhs  =>  indvar != (rhs - offset) / coeff
            symbolic::SymbolVec syms = {indvar};
            auto poly = symbolic::polynomial(lhs, syms);
            if (poly.is_null()) {
                new_clause.push_back(literal);
                continue;
            }

            auto coeffs = symbolic::affine_coefficients(poly, syms);
            if (coeffs.empty() || coeffs.find(indvar) == coeffs.end()) {
                new_clause.push_back(literal);
                continue;
            }

            auto coeff = coeffs.at(indvar);
            if (!SymEngine::is_a<SymEngine::Integer>(*coeff)) {
                new_clause.push_back(literal);
                continue;
            }
            auto coeff_int = SymEngine::rcp_static_cast<const SymEngine::Integer>(coeff)->as_int();
            // Only handle coefficient = 1 (safety check, should match can_be_applied)
            if (coeff_int != 1) {
                new_clause.push_back(literal);
                continue;
            }

            symbolic::Expression offset = symbolic::zero();
            if (coeffs.count(symbolic::symbol("__daisy_constant__"))) {
                offset = coeffs.at(symbolic::symbol("__daisy_constant__"));
            }

            // Since coeff = 1, we have: i + offset != rhs
            // Normalized form: i != (rhs - offset)
            auto normalized_bound = symbolic::expand(symbolic::sub(rhs, offset));

            // Now we have: indvar != normalized_bound
            // Convert based on stride sign

            if (is_unequality) {
                // i != bound
                // stride > 0 (positive): i < bound
                // stride < 0 (negative): i > bound
                symbolic::Condition new_literal;
                if (stride_int > 0) {
                    new_literal = symbolic::Lt(indvar, normalized_bound);
                } else {
                    new_literal = symbolic::Gt(indvar, normalized_bound);
                }
                new_clause.push_back(new_literal);
            } else {
                // Equality (i == bound) is rare in loop conditions
                // It means "run only when equal" which is a single-iteration loop
                // We keep it as-is since it's semantically different from a range
                new_clause.push_back(literal);
            }
        }

        new_cnf.push_back(new_clause);
    }

    // Reconstruct condition from CNF
    // CNF is AND of clauses, each clause is OR of literals
    symbolic::Condition new_condition = symbolic::__true__();

    for (const auto& clause : new_cnf) {
        if (clause.empty()) {
            continue;
        }

        symbolic::Condition clause_cond = clause[0];
        for (size_t i = 1; i < clause.size(); ++i) {
            clause_cond = symbolic::Or(clause_cond, clause[i]);
        }

        new_condition = symbolic::And(new_condition, clause_cond);
    }

    // Update the loop condition
    builder.update_loop(loop_, indvar, new_condition, loop_.init(), loop_.update());
}

void LoopConditionNormalize::to_json(nlohmann::json& j) const {
    std::string loop_type = "for";
    if (dynamic_cast<const structured_control_flow::Map*>(&loop_)) {
        loop_type = "map";
    }

    j["transformation_type"] = this->name();
    j["subgraph"] = {{"0", {{"element_id", loop_.element_id()}, {"type", loop_type}}}};
    j["parameters"] = nlohmann::json::object();
}

LoopConditionNormalize LoopConditionNormalize::
    from_json(builder::StructuredSDFGBuilder& builder, const nlohmann::json& desc) {
    auto loop_id = desc["subgraph"]["0"]["element_id"].get<size_t>();

    auto element = builder.find_element_by_id(loop_id);
    if (element == nullptr) {
        throw std::runtime_error("Element with ID " + std::to_string(loop_id) + " not found.");
    }

    auto loop = dynamic_cast<structured_control_flow::StructuredLoop*>(element);
    if (loop == nullptr) {
        throw std::runtime_error("Element with ID " + std::to_string(loop_id) + " is not a StructuredLoop.");
    }

    return LoopConditionNormalize(*loop);
}

} // namespace transformations
} // namespace sdfg

1	#include "sdfg/transformations/loop_condition_normalize.h"
2
3	#include <stdexcept>
4
5	#include "sdfg/builder/structured_sdfg_builder.h"
6	#include "sdfg/structured_control_flow/map.h"
7	#include "sdfg/symbolic/conjunctive_normal_form.h"
8	#include "sdfg/symbolic/polynomials.h"
9	#include "sdfg/symbolic/symbolic.h"
10
11	/**
12	* Loop Condition Normalize Transformation Implementation
13	*
14	* This transformation converts `!=` (Unequality) conditions to relational comparisons
15	* (`<` or `>`) based on the loop's stride direction.
16	*
17	* Algorithm:
18	* 1. Check that stride is ±1 (unit stride)
19	* 2. Convert condition to CNF
20	* 3. For each Unequality literal involving the indvar:
21	* a. Normalize to form: indvar != bound (solve for indvar if affine)
22	* b. Based on stride sign:
23	* - stride = +1: convert to indvar < bound
24	* - stride = -1: convert to indvar > bound
25	* 4. Reconstruct the condition from the modified CNF
26	*
27	* The transformation assumes LLVM-style well-formed loops where the bound is
28	* reachable from init. For a loop `for (i = 0; i != N; i++)`, we trust that
29	* N >= 0 (loop will eventually reach N).
30	*/
31
32	namespace sdfg {
33	namespace transformations {
34
35	LoopConditionNormalize::LoopConditionNormalize(structured_control_flow::StructuredLoop& loop) : loop_(loop) {}	34✔
36
NEW 37	std::string LoopConditionNormalize::name() const { return "LoopConditionNormalize"; }	×
38
39	bool LoopConditionNormalize::
40	can_be_applied(builder::StructuredSDFGBuilder& builder, analysis::AnalysisManager& analysis_manager) {	34✔
41	// Check for unit stride (±1)
42	auto stride = loop_.stride();	34✔
43	if (stride.is_null()) {	34✔
NEW 44	return false;	×
NEW 45	}	×
46	auto stride_int = stride->as_int();	34✔
47	if (stride_int != 1 && stride_int != -1) {	34✔
48	return false;	1✔
49	}	1✔
50
51	// Convert condition to CNF
52	symbolic::CNF cnf;	33✔
53	try {	33✔
54	cnf = symbolic::conjunctive_normal_form(loop_.condition());	33✔
55	} catch (...) {	33✔
NEW 56	return false;	×
NEW 57	}	×
58
59	auto indvar = loop_.indvar();	33✔
60
61	// Check if there's at least one Unequality or Equality involving indvar
62	bool has_convertible = false;	33✔
63	for (const auto& clause : cnf) {	33✔
64	for (const auto& literal : clause) {	33✔
65	if (SymEngine::is_a<SymEngine::Unequality>(literal) \|\| SymEngine::is_a<SymEngine::Equality>(literal)) {	33✔
66	SymEngine::RCP<const SymEngine::Basic> lhs, rhs;	6✔
67
68	if (SymEngine::is_a<SymEngine::Unequality>(*literal)) {	6✔
69	auto ne = SymEngine::rcp_static_cast<const SymEngine::Unequality>(literal);	6✔
70	lhs = ne->get_arg1();	6✔
71	rhs = ne->get_arg2();	6✔
72	} else {	6✔
NEW 73	auto eq = SymEngine::rcp_static_cast<const SymEngine::Equality>(literal);	×
NEW 74	lhs = eq->get_arg1();	×
NEW 75	rhs = eq->get_arg2();	×
NEW 76	}	×
77
78	// Check if indvar is involved
79	bool lhs_has_indvar = symbolic::uses(lhs, indvar->get_name());	6✔
80	bool rhs_has_indvar = symbolic::uses(rhs, indvar->get_name());	6✔
81
82	if (!lhs_has_indvar && !rhs_has_indvar) {	6✔
83	// indvar not involved, skip
NEW 84	continue;	×
NEW 85	}	×
86
87	if (lhs_has_indvar && rhs_has_indvar) {	6✔
88	// indvar on both sides, can't normalize
NEW 89	continue;	×
NEW 90	}	×
91
92	// One side has indvar - check if affine
93	auto expr_with_indvar = lhs_has_indvar ? lhs : rhs;	6✔
94	symbolic::SymbolVec syms = {indvar};	6✔
95	auto poly = symbolic::polynomial(expr_with_indvar, syms);	6✔
96	if (poly.is_null()) {	6✔
NEW 97	continue;	×
NEW 98	}	×
99
100	auto coeffs = symbolic::affine_coefficients(poly, syms);	6✔
101	if (coeffs.empty() \|\| coeffs.find(indvar) == coeffs.end()) {	6✔
NEW 102	continue;	×
NEW 103	}	×
104
105	// Coefficient must be a non-zero integer
106	auto coeff = coeffs.at(indvar);	6✔
107	if (!SymEngine::is_a<SymEngine::Integer>(*coeff)) {	6✔
NEW 108	continue;	×
NEW 109	}	×
110	auto coeff_int = SymEngine::rcp_static_cast<const SymEngine::Integer>(coeff)->as_int();	6✔
111	// Only allow coefficient = 1 (simple i != bound case)
112	// Coefficient != 1 (e.g., 2*i + 1 != N) is unsafe because
113	// we can't guarantee the bound will be hit (depends on divisibility)
114	if (coeff_int != 1) {	6✔
115	continue;	1✔
116	}	1✔
117
118	has_convertible = true;	5✔
119	break;	5✔
120	}	6✔
121	}	33✔
122	if (has_convertible) {	33✔
123	break;	5✔
124	}	5✔
125	}	33✔
126
127	return has_convertible;	33✔
128	}	33✔
129
130	void LoopConditionNormalize::apply(builder::StructuredSDFGBuilder& builder, analysis::AnalysisManager& analysis_manager) {	5✔
131	auto indvar = loop_.indvar();	5✔
132	auto stride = loop_.stride();	5✔
133	auto stride_int = stride->as_int();	5✔
134
135	// Convert condition to CNF
136	symbolic::CNF cnf = symbolic::conjunctive_normal_form(loop_.condition());	5✔
137
138	// Build a new CNF with converted literals
139	symbolic::CNF new_cnf;	5✔
140
141	for (const auto& clause : cnf) {	5✔
142	std::vector<symbolic::Condition> new_clause;	5✔
143
144	for (const auto& literal : clause) {	5✔
145	if (!SymEngine::is_a<SymEngine::Unequality>(literal) && !SymEngine::is_a<SymEngine::Equality>(literal)) {	5✔
146	// Keep non-equality/inequality literals as-is
NEW 147	new_clause.push_back(literal);	×
NEW 148	continue;	×
NEW 149	}	×
150
151	bool is_unequality = SymEngine::is_a<SymEngine::Unequality>(*literal);	5✔
152	SymEngine::RCP<const SymEngine::Basic> lhs, rhs;	5✔
153
154	if (is_unequality) {	5✔
155	auto ne = SymEngine::rcp_static_cast<const SymEngine::Unequality>(literal);	5✔
156	lhs = ne->get_arg1();	5✔
157	rhs = ne->get_arg2();	5✔
158	} else {	5✔
NEW 159	auto eq = SymEngine::rcp_static_cast<const SymEngine::Equality>(literal);	×
NEW 160	lhs = eq->get_arg1();	×
NEW 161	rhs = eq->get_arg2();	×
NEW 162	}	×
163
164	bool lhs_has_indvar = symbolic::uses(lhs, indvar->get_name());	5✔
165	bool rhs_has_indvar = symbolic::uses(rhs, indvar->get_name());	5✔
166
167	if (!lhs_has_indvar && !rhs_has_indvar) {	5✔
168	// indvar not involved, keep as-is
NEW 169	new_clause.push_back(literal);	×
NEW 170	continue;	×
NEW 171	}	×
172
173	if (lhs_has_indvar && rhs_has_indvar) {	5✔
174	// indvar on both sides, keep as-is
NEW 175	new_clause.push_back(literal);	×
NEW 176	continue;	×
NEW 177	}	×
178
179	// Ensure indvar is on LHS
180	if (!lhs_has_indvar) {	5✔
181	std::swap(lhs, rhs);	4✔
182	}	4✔
183
184	// LHS now has indvar, RHS does not
185	// Normalize: coeff * indvar + offset != rhs => indvar != (rhs - offset) / coeff
186	symbolic::SymbolVec syms = {indvar};	5✔
187	auto poly = symbolic::polynomial(lhs, syms);	5✔
188	if (poly.is_null()) {	5✔
NEW 189	new_clause.push_back(literal);	×
NEW 190	continue;	×
NEW 191	}	×
192
193	auto coeffs = symbolic::affine_coefficients(poly, syms);	5✔
194	if (coeffs.empty() \|\| coeffs.find(indvar) == coeffs.end()) {	5✔
NEW 195	new_clause.push_back(literal);	×
NEW 196	continue;	×
NEW 197	}	×
198
199	auto coeff = coeffs.at(indvar);	5✔
200	if (!SymEngine::is_a<SymEngine::Integer>(*coeff)) {	5✔
NEW 201	new_clause.push_back(literal);	×
NEW 202	continue;	×
NEW 203	}	×
204	auto coeff_int = SymEngine::rcp_static_cast<const SymEngine::Integer>(coeff)->as_int();	5✔
205	// Only handle coefficient = 1 (safety check, should match can_be_applied)
206	if (coeff_int != 1) {	5✔
NEW 207	new_clause.push_back(literal);	×
NEW 208	continue;	×
NEW 209	}	×
210
211	symbolic::Expression offset = symbolic::zero();	5✔
212	if (coeffs.count(symbolic::symbol("__daisy_constant__"))) {	5✔
213	offset = coeffs.at(symbolic::symbol("__daisy_constant__"));	5✔
214	}	5✔
215
216	// Since coeff = 1, we have: i + offset != rhs
217	// Normalized form: i != (rhs - offset)
218	auto normalized_bound = symbolic::expand(symbolic::sub(rhs, offset));	5✔
219
220	// Now we have: indvar != normalized_bound
221	// Convert based on stride sign
222
223	if (is_unequality) {	5✔
224	// i != bound
225	// stride > 0 (positive): i < bound
226	// stride < 0 (negative): i > bound
227	symbolic::Condition new_literal;	5✔
228	if (stride_int > 0) {	5✔
229	new_literal = symbolic::Lt(indvar, normalized_bound);	4✔
230	} else {	4✔
231	new_literal = symbolic::Gt(indvar, normalized_bound);	1✔
232	}	1✔
233	new_clause.push_back(new_literal);	5✔
234	} else {	5✔
235	// Equality (i == bound) is rare in loop conditions
236	// It means "run only when equal" which is a single-iteration loop
237	// We keep it as-is since it's semantically different from a range
NEW 238	new_clause.push_back(literal);	×
NEW 239	}	×
240	}	5✔
241
242	new_cnf.push_back(new_clause);	5✔
243	}	5✔
244
245	// Reconstruct condition from CNF
246	// CNF is AND of clauses, each clause is OR of literals
247	symbolic::Condition new_condition = symbolic::__true__();	5✔
248
249	for (const auto& clause : new_cnf) {	5✔
250	if (clause.empty()) {	5✔
NEW 251	continue;	×
NEW 252	}	×
253
254	symbolic::Condition clause_cond = clause[0];	5✔
255	for (size_t i = 1; i < clause.size(); ++i) {	5✔
NEW 256	clause_cond = symbolic::Or(clause_cond, clause[i]);	×
NEW 257	}	×
258
259	new_condition = symbolic::And(new_condition, clause_cond);	5✔
260	}	5✔
261
262	// Update the loop condition
263	builder.update_loop(loop_, indvar, new_condition, loop_.init(), loop_.update());	5✔
264	}	5✔
265
NEW 266	void LoopConditionNormalize::to_json(nlohmann::json& j) const {	×
NEW 267	std::string loop_type = "for";	×
NEW 268	if (dynamic_cast<const structured_control_flow::Map*>(&loop_)) {	×
NEW 269	loop_type = "map";	×
NEW 270	}	×
271
NEW 272	j["transformation_type"] = this->name();	×
NEW 273	j["subgraph"] = {{"0", {{"element_id", loop_.element_id()}, {"type", loop_type}}}};	×
NEW 274	j["parameters"] = nlohmann::json::object();	×
NEW 275	}	×
276
277	LoopConditionNormalize LoopConditionNormalize::
NEW 278	from_json(builder::StructuredSDFGBuilder& builder, const nlohmann::json& desc) {	×
NEW 279	auto loop_id = desc["subgraph"]["0"]["element_id"].get<size_t>();	×
280
NEW 281	auto element = builder.find_element_by_id(loop_id);	×
NEW 282	if (element == nullptr) {	×
NEW 283	throw std::runtime_error("Element with ID " + std::to_string(loop_id) + " not found.");	×
NEW 284	}	×
285
NEW 286	auto loop = dynamic_cast<structured_control_flow::StructuredLoop*>(element);	×
NEW 287	if (loop == nullptr) {	×
NEW 288	throw std::runtime_error("Element with ID " + std::to_string(loop_id) + " is not a StructuredLoop.");	×
NEW 289	}	×
290
NEW 291	return LoopConditionNormalize(*loop);	×
NEW 292	}	×
293
294	} // namespace transformations
295	} // namespace sdfg

daisytuner / docc / 23958770921

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous