15909488298

Committed 26 Jun 2025 06:20PM UTC coverage: 65.099% (+0.008%) from 65.091%

Build # 15909488298

Build Type

push

github

Committed by

web-flow

Commit Message

Merge pull request #111 from daisytuner/map-intervall-analysis

Adds intervall analysis to prove disjoint maps

Run Details

28 of 47 new or added lines in 2 files covered. (59.57%)

1 existing line in 1 file now uncovered.

8541 of 13120 relevant lines covered (65.1%)

145.28 hits per line

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

72.85

/src/symbolic/maps.cpp

#include "sdfg/symbolic/maps.h"

#include <isl/ctx.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);
    if (mul_int->as_int() <= 0) {
        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);
            if (exp_int->as_int() <= 0) {
                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;
    }

    isl_ctx* ctx = isl_ctx_alloc();

    // Transform both expressions into two maps with separate dimensions
    auto expr1_delinearized = delinearize(expr1, assums1);
    auto expr2_delinearized = delinearize(expr2, assums2);
    auto maps = expressions_to_intersection_map_str(expr1_delinearized, expr2_delinearized, indvar,
                                                    assums1, assums2);
    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) {
    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 is_disjoint_interval(const MultiExpression& expr1, const MultiExpression& expr2,
                          const Symbol& indvar, const Assumptions& assums1,
                          const Assumptions& assums2) {
    for (size_t i = 0; i < expr1.size(); i++) {
        auto& dim1 = expr1[i];
        if (expr2.size() <= i) {
            continue;
        }
        auto& dim2 = expr2[i];

        auto lb1 = minimum(dim1, {}, assums1);
        if (lb1 == SymEngine::null) {
            continue;
        }
        auto ub1 = maximum(dim1, {}, assums1);
        if (ub1 == SymEngine::null) {
            continue;
        }
        auto lb2 = minimum(dim2, {}, assums2);
        if (lb2 == SymEngine::null) {
            continue;
        }
        auto ub2 = maximum(dim2, {}, assums2);
        if (ub2 == SymEngine::null) {
            continue;
        }

        auto dis1 = symbolic::Gt(lb1, ub2);
        auto dis2 = symbolic::Gt(lb2, ub1);
        if (symbolic::is_true(dis1) || symbolic::is_true(dis2)) {
            return true;
        }
    }

    return false;
}

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

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

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

daisytuner / sdfglib / 15909488298

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