20342982902

Committed 18 Dec 2025 03:58PM UTC coverage: 39.454% (-0.4%) from 39.849%

Build # 20342982902

Build Type

push

github

Committed by

web-flow

Commit Message

Merge pull request #398 from daisytuner/trunc

adds trunc_i32 symbolic function and type minimization pass

Run Details

13402 of 44093 branches covered (30.39%)

Branch coverage included in aggregate %.

10 of 134 new or added lines in 9 files covered. (7.46%)

30 existing lines in 7 files now uncovered.

11549 of 19147 relevant lines covered (60.32%)

84.38 hits per line

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

52.98

/src/symbolic/maps.cpp

#include "sdfg/symbolic/maps.h"

#include <isl/ctx.h>
#include <isl/options.h>
#include <isl/set.h>
#include <isl/space.h>

#include "sdfg/symbolic/extreme_values.h"
#include "sdfg/symbolic/polynomials.h"
#include "sdfg/symbolic/utils.h"

namespace sdfg {
namespace symbolic {
namespace maps {

bool is_monotonic_affine(const Expression expr, const Symbol sym, const Assumptions& assums) {
    SymbolVec symbols = {sym};
    auto poly = polynomial(expr, symbols);
    if (poly == SymEngine::null) {
        return false;
    }
    auto coeffs = affine_coefficients(poly, symbols);
    if (coeffs.empty()) {
        return false;
    }
    auto mul = minimum(coeffs[sym], {}, assums);
    if (mul == SymEngine::null) {
        return false;
    }
    if (!SymEngine::is_a<SymEngine::Integer>(*mul)) {
        return false;
    }
    auto mul_int = SymEngine::rcp_dynamic_cast<const SymEngine::Integer>(mul);
    try {
        long long val = mul_int->as_int();
        if (val <= 0) {
            return false;
        }
    } catch (const SymEngine::SymEngineException&) {
        return false;
    }

    return true;
}

bool is_monotonic_pow(const Expression expr, const Symbol sym, const Assumptions& assums) {
    if (SymEngine::is_a<SymEngine::Pow>(*expr)) {
        auto pow = SymEngine::rcp_dynamic_cast<const SymEngine::Pow>(expr);
        auto base = pow->get_base();
        auto exp = pow->get_exp();
        if (SymEngine::is_a<SymEngine::Integer>(*exp) && SymEngine::is_a<SymEngine::Symbol>(*base)) {
            auto exp_int = SymEngine::rcp_dynamic_cast<const SymEngine::Integer>(exp);
            try {
                long long val = exp_int->as_int();
                if (val <= 0) {
                    return false;
                }
            } catch (const SymEngine::SymEngineException&) {
                return false;
            }
            auto base_sym = SymEngine::rcp_static_cast<const SymEngine::Symbol>(base);
            auto ub_sym = minimum(base_sym, {}, assums);
            if (ub_sym == SymEngine::null) {
                return false;
            }
            auto positive = symbolic::Ge(ub_sym, symbolic::integer(0));
            return symbolic::is_true(positive);
        }
    }

    return false;
}

bool is_monotonic(const Expression expr, const Symbol sym, const Assumptions& assums) {
    if (is_monotonic_affine(expr, sym, assums)) {
        return true;
    }
    return is_monotonic_pow(expr, sym, assums);
}

bool is_disjoint_isl(
    const MultiExpression& expr1,
    const MultiExpression& expr2,
    const Symbol indvar,
    const Assumptions& assums1,
    const Assumptions& assums2
) {
    if (expr1.size() != expr2.size()) {
        return false;
    }
    if (expr1.empty()) {
        return false;
    }

    // Transform both expressions into two maps with separate dimensions
    auto expr1_delinearized = delinearize(expr1, assums1);
    auto expr2_delinearized = delinearize(expr2, assums2);
    if (expr1_delinearized.size() != expr2_delinearized.size()) {
        return false;
    }

    // Cheap per-dimension check
    for (size_t i = 0; i < expr1_delinearized.size(); i++) {
        auto& dim1 = expr1_delinearized[i];
        auto& dim2 = expr2_delinearized[i];
        auto maps = expressions_to_intersection_map_str({dim1}, {dim2}, indvar, assums1, assums2);

        isl_ctx* ctx = isl_ctx_alloc();
        isl_options_set_on_error(ctx, ISL_ON_ERROR_CONTINUE);

        isl_map* map_1 = isl_map_read_from_str(ctx, std::get<0>(maps).c_str());
        isl_map* map_2 = isl_map_read_from_str(ctx, std::get<1>(maps).c_str());
        isl_map* map_3 = isl_map_read_from_str(ctx, std::get<2>(maps).c_str());
        if (!map_1 || !map_2 || !map_3) {
            if (map_1) {
                isl_map_free(map_1);
            }
            if (map_2) {
                isl_map_free(map_2);
            }
            if (map_3) {
                isl_map_free(map_3);
            }
            isl_ctx_free(ctx);
            continue;
        }

        // Find aliasing pairs under the constraint that dimensions are different

        isl_map* composed = isl_map_apply_domain(map_2, map_3);
        if (!composed) {
            isl_map_free(map_1);
            if (map_2) {
                isl_map_free(map_2);
            }
            if (map_3) {
                isl_map_free(map_3);
            }
            isl_ctx_free(ctx);
            continue;
        }
        isl_map* alias_pairs = isl_map_intersect(composed, map_1);
        if (!alias_pairs) {
            if (composed) {
                isl_map_free(composed);
            }
            if (map_1) {
                isl_map_free(map_1);
            }
            isl_ctx_free(ctx);
            continue;
        }

        bool disjoint = isl_map_is_empty(alias_pairs);
        isl_map_free(alias_pairs);
        isl_ctx_free(ctx);
        if (disjoint) {
            return true;
        }
    }
    if (expr1_delinearized.size() == 1) {
        return false;
    }

    // Now check on all dimensions together
    auto maps = expressions_to_intersection_map_str(expr1_delinearized, expr2_delinearized, indvar, assums1, assums2);

    isl_ctx* ctx = isl_ctx_alloc();
    isl_options_set_on_error(ctx, ISL_ON_ERROR_CONTINUE);

    isl_map* map_1 = isl_map_read_from_str(ctx, std::get<0>(maps).c_str());
    isl_map* map_2 = isl_map_read_from_str(ctx, std::get<1>(maps).c_str());
    isl_map* map_3 = isl_map_read_from_str(ctx, std::get<2>(maps).c_str());
    if (!map_1 || !map_2 || !map_3) {
        if (map_1) {
            isl_map_free(map_1);
        }
        if (map_2) {
            isl_map_free(map_2);
        }
        if (map_3) {
            isl_map_free(map_3);
        }
        isl_ctx_free(ctx);
        return false;
    }

    // Find aliasing pairs under the constraint that dimensions are different

    isl_map* composed = isl_map_apply_domain(map_2, map_3);
    if (!composed) {
        isl_map_free(map_1);
        if (map_2) {
            isl_map_free(map_2);
        }
        if (map_3) {
            isl_map_free(map_3);
        }
        isl_ctx_free(ctx);
        return false;
    }
    isl_map* alias_pairs = isl_map_intersect(composed, map_1);
    if (!alias_pairs) {
        if (composed) {
            isl_map_free(composed);
        }
        if (map_1) {
            isl_map_free(map_1);
        }
        isl_ctx_free(ctx);
        return false;
    }

    bool disjoint = isl_map_is_empty(alias_pairs);
    isl_map_free(alias_pairs);
    isl_ctx_free(ctx);

    return disjoint;
}

bool is_disjoint_monotonic(
    const MultiExpression& expr1,
    const MultiExpression& expr2,
    const Symbol indvar,
    const Assumptions& assums1,
    const Assumptions& assums2
) {
    // TODO: Handle assumptions1 and assumptions2

    for (size_t i = 0; i < expr1.size(); i++) {
        auto& dim1 = expr1[i];
        if (expr2.size() <= i) {
            continue;
        }
        auto& dim2 = expr2[i];
        if (!symbolic::eq(dim1, dim2)) {
            continue;
        }

        // Collect all symbols
        symbolic::SymbolSet syms;
        for (auto& sym : symbolic::atoms(dim1)) {
            syms.insert(sym);
        }

        // Collect all non-constant symbols
        bool can_analyze = true;
        for (auto& sym : syms) {
            if (!assums1.at(sym).constant()) {
                if (sym->get_name() != indvar->get_name()) {
                    can_analyze = false;
                    break;
                }
            }
        }
        if (!can_analyze) {
            continue;
        }

        // Check if both dimensions are monotonic in non-constant symbols
        if (is_monotonic(dim1, indvar, assums1)) {
            return true;
        }
    }

    return false;
}

bool intersects(
    const MultiExpression& expr1,
    const MultiExpression& expr2,
    const Symbol indvar,
    const Assumptions& assums1,
    const Assumptions& assums2
) {
    if (is_disjoint_monotonic(expr1, expr2, indvar, assums1, assums2)) {
        return false;
    }
    if (is_disjoint_isl(expr1, expr2, indvar, assums1, assums2)) {
        return false;
    }
    return true;
}

} // namespace maps
} // namespace symbolic
} // namespace sdfg

1	#include "sdfg/symbolic/maps.h"
2
3	#include <isl/ctx.h>
4	#include <isl/options.h>
5	#include <isl/set.h>
6	#include <isl/space.h>
7
8	#include "sdfg/symbolic/extreme_values.h"
9	#include "sdfg/symbolic/polynomials.h"
10	#include "sdfg/symbolic/utils.h"
11
12	namespace sdfg {
13	namespace symbolic {
14	namespace maps {
15
16	bool is_monotonic_affine(const Expression expr, const Symbol sym, const Assumptions& assums) {	58✔
17	SymbolVec symbols = {sym};	58!
18	auto poly = polynomial(expr, symbols);	58!
19	if (poly == SymEngine::null) {	58!
20	return false;	×
21	}
22	auto coeffs = affine_coefficients(poly, symbols);	58!
23	if (coeffs.empty()) {	58✔
24	return false;	1✔
25	}
26	auto mul = minimum(coeffs[sym], {}, assums);	57!
27	if (mul == SymEngine::null) {	57!
28	return false;	×
29	}
30	if (!SymEngine::is_a<SymEngine::Integer>(*mul)) {	57!
31	return false;	×
32	}
33	auto mul_int = SymEngine::rcp_dynamic_cast<const SymEngine::Integer>(mul);	57!
34	try {
35	long long val = mul_int->as_int();	57!
36	if (val <= 0) {	57✔
37	return false;	10✔
38	}
39	} catch (const SymEngine::SymEngineException&) {	47!
40	return false;	×
41	}	×
42
43	return true;	47✔
44	}	58✔
45
46	bool is_monotonic_pow(const Expression expr, const Symbol sym, const Assumptions& assums) {	11✔
47	if (SymEngine::is_a<SymEngine::Pow>(*expr)) {	11✔
48	auto pow = SymEngine::rcp_dynamic_cast<const SymEngine::Pow>(expr);	1✔
49	auto base = pow->get_base();	1!
50	auto exp = pow->get_exp();	1!
51	if (SymEngine::is_a<SymEngine::Integer>(exp) && SymEngine::is_a<SymEngine::Symbol>(base)) {	1!
52	auto exp_int = SymEngine::rcp_dynamic_cast<const SymEngine::Integer>(exp);	1!
53	try {
54	long long val = exp_int->as_int();	1!
55	if (val <= 0) {	1!
56	return false;	×
57	}
58	} catch (const SymEngine::SymEngineException&) {	1!
59	return false;	×
60	}	×
61	auto base_sym = SymEngine::rcp_static_cast<const SymEngine::Symbol>(base);	1!
62	auto ub_sym = minimum(base_sym, {}, assums);	1!
63	if (ub_sym == SymEngine::null) {	1!
64	return false;	×
65	}
66	auto positive = symbolic::Ge(ub_sym, symbolic::integer(0));	1!
67	return symbolic::is_true(positive);	1!
68	}	1✔
69	}	1!
70
71	return false;	10✔
72	}	11✔
73
74	bool is_monotonic(const Expression expr, const Symbol sym, const Assumptions& assums) {	58✔
75	if (is_monotonic_affine(expr, sym, assums)) {	58!
76	return true;	47✔
77	}
78	return is_monotonic_pow(expr, sym, assums);	11!
79	}	58✔
80
81	bool is_disjoint_isl(	36✔
82	const MultiExpression& expr1,
83	const MultiExpression& expr2,
84	const Symbol indvar,
85	const Assumptions& assums1,
86	const Assumptions& assums2
87	) {
88	if (expr1.size() != expr2.size()) {	36!
89	return false;	×
90	}
91	if (expr1.empty()) {	36!
92	return false;	×
93	}
94
95	// Transform both expressions into two maps with separate dimensions
96	auto expr1_delinearized = delinearize(expr1, assums1);	36✔
97	auto expr2_delinearized = delinearize(expr2, assums2);	36!
98	if (expr1_delinearized.size() != expr2_delinearized.size()) {	36!
99	return false;	×
100	}
101
102	// Cheap per-dimension check
103	for (size_t i = 0; i < expr1_delinearized.size(); i++) {	72✔
104	auto& dim1 = expr1_delinearized[i];	50✔
105	auto& dim2 = expr2_delinearized[i];	50✔
106	auto maps = expressions_to_intersection_map_str({dim1}, {dim2}, indvar, assums1, assums2);	50!
107
108	isl_ctx* ctx = isl_ctx_alloc();	50!
109	isl_options_set_on_error(ctx, ISL_ON_ERROR_CONTINUE);	50!
110
111	isl_map* map_1 = isl_map_read_from_str(ctx, std::get<0>(maps).c_str());	50!
112	isl_map* map_2 = isl_map_read_from_str(ctx, std::get<1>(maps).c_str());	50!
113	isl_map* map_3 = isl_map_read_from_str(ctx, std::get<2>(maps).c_str());	50!
114	if (!map_1 \|\| !map_2 \|\| !map_3) {	50!
115	if (map_1) {	1!
116	isl_map_free(map_1);	×
117	}	×
118	if (map_2) {	1!
119	isl_map_free(map_2);	×
120	}	×
121	if (map_3) {	1!
122	isl_map_free(map_3);	1!
123	}	1✔
124	isl_ctx_free(ctx);	1!
125	continue;	1✔
126	}
127
128	// Find aliasing pairs under the constraint that dimensions are different
129
130	isl_map* composed = isl_map_apply_domain(map_2, map_3);	49!
131	if (!composed) {	49!
132	isl_map_free(map_1);	×
133	if (map_2) {	×
134	isl_map_free(map_2);	×
135	}	×
136	if (map_3) {	×
137	isl_map_free(map_3);	×
138	}	×
139	isl_ctx_free(ctx);	×
NEW 140	continue;	×
141	}
142	isl_map* alias_pairs = isl_map_intersect(composed, map_1);	49!
143	if (!alias_pairs) {	49!
144	if (composed) {	×
145	isl_map_free(composed);	×
146	}	×
147	if (map_1) {	×
148	isl_map_free(map_1);	×
149	}	×
150	isl_ctx_free(ctx);	×
NEW 151	continue;	×
152	}
153
154	bool disjoint = isl_map_is_empty(alias_pairs);	49!
155	isl_map_free(alias_pairs);	49!
156	isl_ctx_free(ctx);	49!
157	if (disjoint) {	49✔
158	return true;	14✔
159	}
160	}	50✔
161	if (expr1_delinearized.size() == 1) {	22✔
162	return false;	14✔
163	}
164
165	// Now check on all dimensions together
166	auto maps = expressions_to_intersection_map_str(expr1_delinearized, expr2_delinearized, indvar, assums1, assums2);	8!
167
168	isl_ctx* ctx = isl_ctx_alloc();	8!
169	isl_options_set_on_error(ctx, ISL_ON_ERROR_CONTINUE);	8!
170
171	isl_map* map_1 = isl_map_read_from_str(ctx, std::get<0>(maps).c_str());	8!
172	isl_map* map_2 = isl_map_read_from_str(ctx, std::get<1>(maps).c_str());	8!
173	isl_map* map_3 = isl_map_read_from_str(ctx, std::get<2>(maps).c_str());	8!
174	if (!map_1 \|\| !map_2 \|\| !map_3) {	8!
175	if (map_1) {	×
176	isl_map_free(map_1);	×
177	}	×
178	if (map_2) {	×
179	isl_map_free(map_2);	×
180	}	×
181	if (map_3) {	×
182	isl_map_free(map_3);	×
183	}	×
184	isl_ctx_free(ctx);	×
185	return false;	×
186	}
187
188	// Find aliasing pairs under the constraint that dimensions are different
189
190	isl_map* composed = isl_map_apply_domain(map_2, map_3);	8!
191	if (!composed) {	8!
192	isl_map_free(map_1);	×
193	if (map_2) {	×
194	isl_map_free(map_2);	×
195	}	×
196	if (map_3) {	×
197	isl_map_free(map_3);	×
198	}	×
199	isl_ctx_free(ctx);	×
200	return false;	×
201	}
202	isl_map* alias_pairs = isl_map_intersect(composed, map_1);	8!
203	if (!alias_pairs) {	8!
204	if (composed) {	×
205	isl_map_free(composed);	×
206	}	×
207	if (map_1) {	×
208	isl_map_free(map_1);	×
209	}	×
210	isl_ctx_free(ctx);	×
211	return false;	×
212	}
213
214	bool disjoint = isl_map_is_empty(alias_pairs);	8!
215	isl_map_free(alias_pairs);	8!
216	isl_ctx_free(ctx);	8!
217
218	return disjoint;	8✔
219	}	36✔
220
221	bool is_disjoint_monotonic(	84✔
222	const MultiExpression& expr1,
223	const MultiExpression& expr2,
224	const Symbol indvar,
225	const Assumptions& assums1,
226	const Assumptions& assums2
227	) {
228	// TODO: Handle assumptions1 and assumptions2
229
230	for (size_t i = 0; i < expr1.size(); i++) {	131✔
231	auto& dim1 = expr1[i];	95✔
232	if (expr2.size() <= i) {	95!
233	continue;	×
234	}
235	auto& dim2 = expr2[i];	95✔
236	if (!symbolic::eq(dim1, dim2)) {	95!
237	continue;	28✔
238	}
239
240	// Collect all symbols
241	symbolic::SymbolSet syms;	67✔
242	for (auto& sym : symbolic::atoms(dim1)) {	131!
243	syms.insert(sym);	64!
244	}
245
246	// Collect all non-constant symbols
247	bool can_analyze = true;	67✔
248	for (auto& sym : syms) {	122✔
249	if (!assums1.at(sym).constant()) {	64!
250	if (sym->get_name() != indvar->get_name()) {	58!
251	can_analyze = false;	9✔
252	break;	9✔
253	}
254	}	49✔
255	}
256	if (!can_analyze) {	67✔
257	continue;	9✔
258	}
259
260	// Check if both dimensions are monotonic in non-constant symbols
261	if (is_monotonic(dim1, indvar, assums1)) {	58!
262	return true;	48✔
263	}
264	}	67!
265
266	return false;	36✔
267	}	84✔
268
269	bool intersects(	84✔
270	const MultiExpression& expr1,
271	const MultiExpression& expr2,
272	const Symbol indvar,
273	const Assumptions& assums1,
274	const Assumptions& assums2
275	) {
276	if (is_disjoint_monotonic(expr1, expr2, indvar, assums1, assums2)) {	84!
277	return false;	48✔
278	}
279	if (is_disjoint_isl(expr1, expr2, indvar, assums1, assums2)) {	36!
280	return false;	18✔
281	}
282	return true;	18✔
283	}	84✔
284
285	} // namespace maps
286	} // namespace symbolic
287	} // namespace sdfg

daisytuner / sdfglib / 20342982902

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