15044057891

Committed 15 May 2025 11:42AM UTC coverage: 59.37% (+1.8%) from 57.525%

Build # 15044057891

Build Type

push

github

Committed by

web-flow

Commit Message

Merge pull request #14 from daisytuner/sanitizers

enables sanitizer on unit tests

Run Details

63 of 67 new or added lines in 47 files covered. (94.03%)

570 existing lines in 62 files now uncovered.

7356 of 12390 relevant lines covered (59.37%)

505.93 hits per line

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

74.02

/src/symbolic/analysis.cpp

#include "sdfg/symbolic/analysis.h"

#include "sdfg/symbolic/symbolic.h"
#include "symengine/infinity.h"
#include "symengine/polys/basic_conversions.h"
#include "symengine/visitor.h"

namespace sdfg {
namespace symbolic {

Polynomial polynomial(const Expression& expr, const Symbol& symbol) {
    try {
        return SymEngine::from_basic<SymEngine::UExprPoly>(expr, symbol, true);
    } catch (SymEngine::SymEngineException& e) {
        return SymEngine::null;
    }
};

Affine affine(const Expression& expr, const Symbol& symbol) {
    auto poly = symbolic::polynomial(expr, symbol);
    if (poly == SymEngine::null || poly->get_degree() > 1) {
        return {SymEngine::null, SymEngine::null};
    }
    if (poly->get_degree() == 0) {
        return {symbolic::integer(0), poly->get_coeff(0)};
    }
    return {poly->get_coeff(1), poly->get_coeff(0)};
};

Sign strict_monotonicity_affine(const Expression& func, const Symbol& symbol) {
    return strict_monotonicity_affine(func, symbol, {});
};

Sign strict_monotonicity_affine(const Expression& func, const symbolic::Assumptions& assumptions) {
    Sign sign = Sign::NONE;
    bool initialized = false;

    for (auto atom : atoms(func)) {
        auto sym = SymEngine::rcp_static_cast<const SymEngine::Symbol>(atom);
        if (!initialized) {
            sign = strict_monotonicity_affine(func, sym, assumptions);
            if (sign == Sign::NONE) {
                return Sign::NONE;
            }
            initialized = true;
            continue;
        }
        if (sign != strict_monotonicity_affine(func, sym, assumptions)) {
            return Sign::NONE;
        }
    }
    return sign;
};

Sign strict_monotonicity_affine(const Expression& func, const Symbol& symbol,
                                const symbolic::Assumptions& assumptions) {
    auto aff = symbolic::affine(func, symbol);
    if (aff.first == SymEngine::null) {
        return Sign::NONE;
    }

    if (SymEngine::is_a<SymEngine::Integer>(*aff.first)) {
        auto coeff = SymEngine::rcp_static_cast<const SymEngine::Integer>(aff.first);
        if (coeff->as_int() > 0) {
            return Sign::POSITIVE;
        } else if (coeff->as_int() < 0) {
            return Sign::NEGATIVE;
        } else {
            return Sign::NONE;
        }
    } else if (SymEngine::is_a<SymEngine::Symbol>(*aff.first)) {
        auto sym = SymEngine::rcp_static_cast<const SymEngine::Symbol>(aff.first);
        if (assumptions.find(sym) != assumptions.end()) {
            auto& a = assumptions.at(sym);
            if (a.is_positive()) {
                return Sign::POSITIVE;
            } else if (a.is_negative()) {
                return Sign::NEGATIVE;
            } else {
                return Sign::NONE;
            }
        }
    }

    return Sign::NONE;
};

Sign strict_monotonicity(const Expression& func, const Symbol& symbol) {
    return strict_monotonicity(func, symbol, {});
};

Sign strict_monotonicity(const Expression& func, const symbolic::Assumptions& assumptions) {
    if (symbolic::strict_monotonicity_affine(func, assumptions) != Sign::NONE) {
        return symbolic::strict_monotonicity_affine(func, assumptions);
    }
    return Sign::NONE;
};

Sign strict_monotonicity(const Expression& func, const Symbol& symbol,
                         const symbolic::Assumptions& assumptions) {
    if (symbolic::strict_monotonicity_affine(func, symbol, assumptions) != Sign::NONE) {
        return symbolic::strict_monotonicity_affine(func, symbol, assumptions);
    }

    return Sign::NONE;
};

Sign strict_monotonicity(const Expression& func) {
    for (auto& sym : symbolic::atoms(func)) {
        auto sym_ = SymEngine::rcp_static_cast<const SymEngine::Symbol>(sym);
        if (symbolic::strict_monotonicity(func, sym_) != Sign::POSITIVE) {
            return Sign::NONE;
        }
    }
    return Sign::POSITIVE;
};

bool contiguity_affine(const Expression& func, const Symbol& symbol) {
    return contiguity_affine(func, symbol, {});
};

bool contiguity_affine(const Expression& func, const Symbol& symbol,
                       const symbolic::Assumptions& assumptions) {
    auto aff = symbolic::affine(func, symbol);
    if (aff.first == SymEngine::null) {
        return false;
    }

    if (SymEngine::is_a<SymEngine::Integer>(*aff.first)) {
        auto coeff = SymEngine::rcp_static_cast<const SymEngine::Integer>(aff.first);
        if (coeff->as_int() == 1) {
            return true;
        }
    } else if (SymEngine::is_a<SymEngine::Symbol>(*aff.first)) {
        auto sym = SymEngine::rcp_static_cast<const SymEngine::Symbol>(aff.first);
        if (assumptions.find(sym) != assumptions.end()) {
            auto& a = assumptions.at(sym);
            if (symbolic::eq(a.lower_bound(), symbolic::integer(1)) &&
                symbolic::eq(a.upper_bound(), symbolic::integer(1))) {
                return true;
            }
        }
    }

    return false;
};

bool contiguity(const Expression& func, const Symbol& symbol) {
    return contiguity(func, symbol, {});
}

bool contiguity(const Expression& func, const Symbol& symbol,
                const symbolic::Assumptions& assumptions) {
    if (symbolic::contiguity_affine(func, symbol, assumptions)) {
        return true;
    }

    return false;
};

Expression inverse(const Symbol& lhs, const Expression& rhs) {
    if (!symbolic::uses(rhs, lhs)) {
        return SymEngine::null;
    }

    if (SymEngine::is_a<SymEngine::Add>(*rhs)) {
        auto add = SymEngine::rcp_static_cast<const SymEngine::Add>(rhs);
        auto arg_0 = add->get_args()[0];
        auto arg_1 = add->get_args()[1];
        if (!symbolic::eq(arg_0, lhs)) {
            std::swap(arg_0, arg_1);
        }
        if (!symbolic::eq(arg_0, lhs)) {
            return SymEngine::null;
        }
        if (!SymEngine::is_a<SymEngine::Integer>(*arg_1)) {
            return SymEngine::null;
        }
        return symbolic::sub(lhs, arg_1);
    } else if (SymEngine::is_a<SymEngine::Mul>(*rhs)) {
        auto mul = SymEngine::rcp_static_cast<const SymEngine::Mul>(rhs);
        auto arg_0 = mul->get_args()[0];
        auto arg_1 = mul->get_args()[1];
        if (!symbolic::eq(arg_0, lhs)) {
            std::swap(arg_0, arg_1);
        }
        if (!symbolic::eq(arg_0, lhs)) {
            return SymEngine::null;
        }
        if (!SymEngine::is_a<SymEngine::Integer>(*arg_1)) {
            return SymEngine::null;
        }
        return symbolic::div(lhs, arg_1);
    }

    return SymEngine::null;
};

bool contains_infinity(const Expression& expr) {
    if (SymEngine::atoms<const SymEngine::Infty>(*expr).empty()) {
        return false;
    }
    return true;
};

Expression lower_bound_analysis(const symbolic::Expression& expr,
                                symbolic::Assumptions& assumptions) {
    if (SymEngine::is_a<SymEngine::Integer>(*expr)) {
        return SymEngine::rcp_static_cast<const SymEngine::Integer>(expr);
    }
    if (SymEngine::is_a<SymEngine::Symbol>(*expr)) {
        auto symbol = SymEngine::rcp_static_cast<const SymEngine::Symbol>(expr);
        if (assumptions.find(symbol) != assumptions.end()) {
            return assumptions[symbol].lower_bound();
        }
        return symbolic::infty(-1);
    }

    // Attempt analysis via monotonicity
    auto sign = symbolic::strict_monotonicity(expr, assumptions);
    if (sign == symbolic::Sign::NONE) {
        return symbolic::infty(-1);
    }

    // Subsitute all symbols accordingly
    symbolic::Expression lower_bound = expr;
    for (auto atom : symbolic::atoms(expr)) {
        auto symbol = SymEngine::rcp_static_cast<const SymEngine::Symbol>(atom);
        if (sign == symbolic::Sign::NEGATIVE) {
            auto ub = assumptions[symbol].upper_bound();
            lower_bound = symbolic::subs(lower_bound, symbol, ub);
        } else {  // if (sign == symbolic::Sign::POSITIVE)
            auto lb = assumptions[symbol].lower_bound();
            lower_bound = symbolic::subs(lower_bound, symbol, lb);
        }
    }

    // End of recursion
    if (contains_infinity(lower_bound)) {
        return symbolic::infty(-1);
    } else {
        if (symbolic::atoms(lower_bound).empty()) {
            return lower_bound;
        } else {
            auto new_lb = lower_bound_analysis(lower_bound, assumptions);
            return new_lb;
        }
    }
};

Expression upper_bound_analysis(const symbolic::Expression& expr,
                                symbolic::Assumptions& assumptions) {
    if (SymEngine::is_a<SymEngine::Integer>(*expr)) {
        return SymEngine::rcp_static_cast<const SymEngine::Integer>(expr);
    }
    if (SymEngine::is_a<SymEngine::Symbol>(*expr)) {
        auto symbol = SymEngine::rcp_static_cast<const SymEngine::Symbol>(expr);
        if (assumptions.find(symbol) != assumptions.end()) {
            return assumptions[symbol].upper_bound();
        }
        return symbolic::infty(1);
    }

    // Attempt analysis via monotonicity
    auto sign = symbolic::strict_monotonicity(expr, assumptions);
    if (sign == symbolic::Sign::NONE) {
        return symbolic::infty(1);
    }

    // Subsitute all symbols accordingly
    symbolic::Expression upper_bound = expr;
    for (auto atom : symbolic::atoms(expr)) {
        auto symbol = SymEngine::rcp_static_cast<const SymEngine::Symbol>(atom);
        if (sign == symbolic::Sign::NEGATIVE) {
            auto lb = assumptions[symbol].lower_bound();
            upper_bound = symbolic::subs(upper_bound, symbol, lb);
        } else {  // if (sign == symbolic::Sign::POSITIVE)
            auto ub = assumptions[symbol].upper_bound();
            upper_bound = symbolic::subs(upper_bound, symbol, ub);
        }
    }

    // End of recursion
    if (contains_infinity(upper_bound)) {
        return symbolic::infty(1);
    } else {
        if (symbolic::atoms(upper_bound).empty()) {
            return upper_bound;
        } else {
            auto new_ub = upper_bound_analysis(upper_bound, assumptions);
            return new_ub;
        }
    }
};
}  // namespace symbolic
}  // namespace sdfg

1	#include "sdfg/symbolic/analysis.h"
2
3	#include "sdfg/symbolic/symbolic.h"
4	#include "symengine/infinity.h"
5	#include "symengine/polys/basic_conversions.h"
6	#include "symengine/visitor.h"
7
8	namespace sdfg {
9	namespace symbolic {
10
11	Polynomial polynomial(const Expression& expr, const Symbol& symbol) {	1,903✔
12	try {
13	return SymEngine::from_basic<SymEngine::UExprPoly>(expr, symbol, true);	1,903✔
14	} catch (SymEngine::SymEngineException& e) {	3✔
15	return SymEngine::null;	3✔
16	}	3✔
17	};	1,906✔
18
19	Affine affine(const Expression& expr, const Symbol& symbol) {	1,898✔
20	auto poly = symbolic::polynomial(expr, symbol);	1,898✔
21	if (poly == SymEngine::null \|\| poly->get_degree() > 1) {	1,898✔
22	return {SymEngine::null, SymEngine::null};	3✔
23	}
24	if (poly->get_degree() == 0) {	1,895✔
25	return {symbolic::integer(0), poly->get_coeff(0)};	2✔
26	}
27	return {poly->get_coeff(1), poly->get_coeff(0)};	1,893✔
28	};	1,898✔
29
30	Sign strict_monotonicity_affine(const Expression& func, const Symbol& symbol) {	4✔
31	return strict_monotonicity_affine(func, symbol, {});	4✔
UNCOV 32	};	×
33
34	Sign strict_monotonicity_affine(const Expression& func, const symbolic::Assumptions& assumptions) {	17✔
35	Sign sign = Sign::NONE;	17✔
36	bool initialized = false;	17✔
37
38	for (auto atom : atoms(func)) {	58✔
39	auto sym = SymEngine::rcp_static_cast<const SymEngine::Symbol>(atom);	41✔
40	if (!initialized) {	41✔
41	sign = strict_monotonicity_affine(func, sym, assumptions);	17✔
42	if (sign == Sign::NONE) {	17✔
43	return Sign::NONE;	×
44	}
45	initialized = true;	17✔
46	continue;	17✔
47	}
48	if (sign != strict_monotonicity_affine(func, sym, assumptions)) {	24✔
49	return Sign::NONE;	11✔
50	}
51	}	41✔
52	return sign;	6✔
53	};	17✔
54
55	Sign strict_monotonicity_affine(const Expression& func, const Symbol& symbol,	1,871✔
56	const symbolic::Assumptions& assumptions) {
57	auto aff = symbolic::affine(func, symbol);	1,871✔
58	if (aff.first == SymEngine::null) {	1,871✔
59	return Sign::NONE;	1✔
60	}
61
62	if (SymEngine::is_a<SymEngine::Integer>(*aff.first)) {	1,870✔
63	auto coeff = SymEngine::rcp_static_cast<const SymEngine::Integer>(aff.first);	1,841✔
64	if (coeff->as_int() > 0) {	1,841✔
65	return Sign::POSITIVE;	1,839✔
66	} else if (coeff->as_int() < 0) {	2✔
67	return Sign::NEGATIVE;	1✔
68	} else {
69	return Sign::NONE;	1✔
70	}
71	} else if (SymEngine::is_a<SymEngine::Symbol>(*aff.first)) {	1,870✔
72	auto sym = SymEngine::rcp_static_cast<const SymEngine::Symbol>(aff.first);	29✔
73	if (assumptions.find(sym) != assumptions.end()) {	29✔
74	auto& a = assumptions.at(sym);	22✔
75	if (a.is_positive()) {	22✔
76	return Sign::POSITIVE;	15✔
77	} else if (a.is_negative()) {	7✔
78	return Sign::NEGATIVE;	2✔
79	} else {
80	return Sign::NONE;	5✔
81	}
82	}
83	}	29✔
84
85	return Sign::NONE;	7✔
86	};	1,871✔
87
88	Sign strict_monotonicity(const Expression& func, const Symbol& symbol) {	911✔
89	return strict_monotonicity(func, symbol, {});	911✔
UNCOV 90	};	×
91
92	Sign strict_monotonicity(const Expression& func, const symbolic::Assumptions& assumptions) {	6✔
93	if (symbolic::strict_monotonicity_affine(func, assumptions) != Sign::NONE) {	6✔
94	return symbolic::strict_monotonicity_affine(func, assumptions);	2✔
95	}
96	return Sign::NONE;	4✔
97	};	6✔
98
99	Sign strict_monotonicity(const Expression& func, const Symbol& symbol,	911✔
100	const symbolic::Assumptions& assumptions) {
101	if (symbolic::strict_monotonicity_affine(func, symbol, assumptions) != Sign::NONE) {	911✔
102	return symbolic::strict_monotonicity_affine(func, symbol, assumptions);	910✔
103	}
104
105	return Sign::NONE;	1✔
106	};	911✔
107
108	Sign strict_monotonicity(const Expression& func) {	×
109	for (auto& sym : symbolic::atoms(func)) {	×
110	auto sym_ = SymEngine::rcp_static_cast<const SymEngine::Symbol>(sym);	×
111	if (symbolic::strict_monotonicity(func, sym_) != Sign::POSITIVE) {	×
112	return Sign::NONE;	×
113	}
114	}	×
115	return Sign::POSITIVE;	×
UNCOV 116	};	×
117
118	bool contiguity_affine(const Expression& func, const Symbol& symbol) {	2✔
119	return contiguity_affine(func, symbol, {});	2✔
UNCOV 120	};	×
121
122	bool contiguity_affine(const Expression& func, const Symbol& symbol,	16✔
123	const symbolic::Assumptions& assumptions) {
124	auto aff = symbolic::affine(func, symbol);	16✔
125	if (aff.first == SymEngine::null) {	16✔
126	return false;	1✔
127	}
128
129	if (SymEngine::is_a<SymEngine::Integer>(*aff.first)) {	15✔
130	auto coeff = SymEngine::rcp_static_cast<const SymEngine::Integer>(aff.first);	13✔
131	if (coeff->as_int() == 1) {	13✔
132	return true;	12✔
133	}
134	} else if (SymEngine::is_a<SymEngine::Symbol>(*aff.first)) {	15✔
135	auto sym = SymEngine::rcp_static_cast<const SymEngine::Symbol>(aff.first);	2✔
136	if (assumptions.find(sym) != assumptions.end()) {	2✔
137	auto& a = assumptions.at(sym);	2✔
138	if (symbolic::eq(a.lower_bound(), symbolic::integer(1)) &&	3✔
139	symbolic::eq(a.upper_bound(), symbolic::integer(1))) {	1✔
140	return true;	1✔
141	}
142	}	1✔
143	}	2✔
144
145	return false;	2✔
146	};	16✔
147
148	bool contiguity(const Expression& func, const Symbol& symbol) {	12✔
149	return contiguity(func, symbol, {});	12✔
UNCOV 150	}	×
151
152	bool contiguity(const Expression& func, const Symbol& symbol,	12✔
153	const symbolic::Assumptions& assumptions) {
154	if (symbolic::contiguity_affine(func, symbol, assumptions)) {	12✔
155	return true;	11✔
156	}
157
158	return false;	1✔
159	};	12✔
160
161	Expression inverse(const Symbol& lhs, const Expression& rhs) {	1✔
162	if (!symbolic::uses(rhs, lhs)) {	1✔
163	return SymEngine::null;	1✔
164	}
165
166	if (SymEngine::is_a<SymEngine::Add>(*rhs)) {	×
167	auto add = SymEngine::rcp_static_cast<const SymEngine::Add>(rhs);	×
168	auto arg_0 = add->get_args()[0];	×
169	auto arg_1 = add->get_args()[1];	×
170	if (!symbolic::eq(arg_0, lhs)) {	×
171	std::swap(arg_0, arg_1);	×
UNCOV 172	}	×
173	if (!symbolic::eq(arg_0, lhs)) {	×
174	return SymEngine::null;	×
175	}
176	if (!SymEngine::is_a<SymEngine::Integer>(*arg_1)) {	×
177	return SymEngine::null;	×
178	}
179	return symbolic::sub(lhs, arg_1);	×
180	} else if (SymEngine::is_a<SymEngine::Mul>(*rhs)) {	×
181	auto mul = SymEngine::rcp_static_cast<const SymEngine::Mul>(rhs);	×
182	auto arg_0 = mul->get_args()[0];	×
183	auto arg_1 = mul->get_args()[1];	×
184	if (!symbolic::eq(arg_0, lhs)) {	×
185	std::swap(arg_0, arg_1);	×
UNCOV 186	}	×
187	if (!symbolic::eq(arg_0, lhs)) {	×
188	return SymEngine::null;	×
189	}
190	if (!SymEngine::is_a<SymEngine::Integer>(*arg_1)) {	×
191	return SymEngine::null;	×
192	}
193	return symbolic::div(lhs, arg_1);	×
194	}	×
195
196	return SymEngine::null;	×
197	};	1✔
198
199	bool contains_infinity(const Expression& expr) {	24✔
200	if (SymEngine::atoms<const SymEngine::Infty>(*expr).empty()) {	24✔
201	return false;	4✔
202	}
203	return true;	20✔
204	};	24✔
205
206	Expression lower_bound_analysis(const symbolic::Expression& expr,	53✔
207	symbolic::Assumptions& assumptions) {
208	if (SymEngine::is_a<SymEngine::Integer>(*expr)) {	53✔
209	return SymEngine::rcp_static_cast<const SymEngine::Integer>(expr);	25✔
210	}
211	if (SymEngine::is_a<SymEngine::Symbol>(*expr)) {	28✔
212	auto symbol = SymEngine::rcp_static_cast<const SymEngine::Symbol>(expr);	25✔
213	if (assumptions.find(symbol) != assumptions.end()) {	25✔
214	return assumptions[symbol].lower_bound();	1✔
215	}
216	return symbolic::infty(-1);	24✔
217	}	25✔
218
219	// Attempt analysis via monotonicity
220	auto sign = symbolic::strict_monotonicity(expr, assumptions);	3✔
221	if (sign == symbolic::Sign::NONE) {	3✔
222	return symbolic::infty(-1);	2✔
223	}
224
225	// Subsitute all symbols accordingly
226	symbolic::Expression lower_bound = expr;	1✔
227	for (auto atom : symbolic::atoms(expr)) {	4✔
228	auto symbol = SymEngine::rcp_static_cast<const SymEngine::Symbol>(atom);	3✔
229	if (sign == symbolic::Sign::NEGATIVE) {	3✔
230	auto ub = assumptions[symbol].upper_bound();	×
231	lower_bound = symbolic::subs(lower_bound, symbol, ub);	×
232	} else { // if (sign == symbolic::Sign::POSITIVE)	×
233	auto lb = assumptions[symbol].lower_bound();	3✔
234	lower_bound = symbolic::subs(lower_bound, symbol, lb);	3✔
235	}	3✔
236	}	3✔
237
238	// End of recursion
239	if (contains_infinity(lower_bound)) {	1✔
240	return symbolic::infty(-1);	×
241	} else {
242	if (symbolic::atoms(lower_bound).empty()) {	1✔
243	return lower_bound;	1✔
244	} else {
245	auto new_lb = lower_bound_analysis(lower_bound, assumptions);	×
246	return new_lb;	×
247	}	×
248	}
249	};	53✔
250
251	Expression upper_bound_analysis(const symbolic::Expression& expr,	53✔
252	symbolic::Assumptions& assumptions) {
253	if (SymEngine::is_a<SymEngine::Integer>(*expr)) {	53✔
254	return SymEngine::rcp_static_cast<const SymEngine::Integer>(expr);	25✔
255	}
256	if (SymEngine::is_a<SymEngine::Symbol>(*expr)) {	28✔
257	auto symbol = SymEngine::rcp_static_cast<const SymEngine::Symbol>(expr);	25✔
258	if (assumptions.find(symbol) != assumptions.end()) {	25✔
259	return assumptions[symbol].upper_bound();	1✔
260	}
261	return symbolic::infty(1);	24✔
262	}	25✔
263
264	// Attempt analysis via monotonicity
265	auto sign = symbolic::strict_monotonicity(expr, assumptions);	3✔
266	if (sign == symbolic::Sign::NONE) {	3✔
267	return symbolic::infty(1);	2✔
268	}
269
270	// Subsitute all symbols accordingly
271	symbolic::Expression upper_bound = expr;	1✔
272	for (auto atom : symbolic::atoms(expr)) {	4✔
273	auto symbol = SymEngine::rcp_static_cast<const SymEngine::Symbol>(atom);	3✔
274	if (sign == symbolic::Sign::NEGATIVE) {	3✔
275	auto lb = assumptions[symbol].lower_bound();	×
276	upper_bound = symbolic::subs(upper_bound, symbol, lb);	×
277	} else { // if (sign == symbolic::Sign::POSITIVE)	×
278	auto ub = assumptions[symbol].upper_bound();	3✔
279	upper_bound = symbolic::subs(upper_bound, symbol, ub);	3✔
280	}	3✔
281	}	3✔
282
283	// End of recursion
284	if (contains_infinity(upper_bound)) {	1✔
285	return symbolic::infty(1);	×
286	} else {
287	if (symbolic::atoms(upper_bound).empty()) {	1✔
288	return upper_bound;	1✔
289	} else {
290	auto new_ub = upper_bound_analysis(upper_bound, assumptions);	×
291	return new_ub;	×
292	}	×
293	}
294	};	53✔
295	} // namespace symbolic
296	} // namespace sdfg

daisytuner / sdfglib / 15044057891

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