15827874660

Committed 23 Jun 2025 03:03PM UTC coverage: 64.193% (+0.4%) from 63.824%

Build # 15827874660

Build Type

push

github

Committed by

web-flow

Commit Message

Merge pull request #100 from daisytuner/transformations

new definition of map and adapts transformations

Run Details

148 of 194 new or added lines in 13 files covered. (76.29%)

45 existing lines in 4 files now uncovered.

8193 of 12763 relevant lines covered (64.19%)

136.04 hits per line

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

87.5

/src/analysis/assumptions_analysis.cpp

#include "sdfg/analysis/assumptions_analysis.h"

#include <utility>
#include <vector>

#include "sdfg/analysis/scope_analysis.h"
#include "sdfg/analysis/users.h"
#include "sdfg/symbolic/assumptions.h"
#include "sdfg/symbolic/extreme_values.h"
#include "sdfg/symbolic/polynomials.h"
#include "sdfg/symbolic/series.h"

namespace sdfg {
namespace analysis {

symbolic::Expression AssumptionsAnalysis::cnf_to_upper_bound(const symbolic::CNF& cnf,
                                                             const symbolic::Symbol& indvar) {
    std::vector<symbolic::Expression> candidates;

    for (const auto& clause : cnf) {
        for (const auto& literal : clause) {
            // Comparison: indvar < expr
            if (SymEngine::is_a<SymEngine::StrictLessThan>(*literal)) {
                auto lt = SymEngine::rcp_static_cast<const SymEngine::StrictLessThan>(literal);
                if (symbolic::eq(lt->get_arg1(), indvar) &&
                    !symbolic::uses(lt->get_arg2(), indvar)) {
                    auto ub = symbolic::sub(lt->get_arg2(), symbolic::one());
                    candidates.push_back(ub);
                }
            }
            // Comparison: indvar <= expr
            else if (SymEngine::is_a<SymEngine::LessThan>(*literal)) {
                auto le = SymEngine::rcp_static_cast<const SymEngine::LessThan>(literal);
                if (symbolic::eq(le->get_arg1(), indvar) &&
                    !symbolic::uses(le->get_arg2(), indvar)) {
                    candidates.push_back(le->get_arg2());
                }
            }
            // Comparison: indvar == expr
            else if (SymEngine::is_a<SymEngine::Equality>(*literal)) {
                auto eq = SymEngine::rcp_static_cast<const SymEngine::Equality>(literal);
                if (symbolic::eq(eq->get_arg1(), indvar) &&
                    !symbolic::uses(eq->get_arg2(), indvar)) {
                    candidates.push_back(eq->get_arg2());
                }
            }
        }
    }

    if (candidates.empty()) {
        return SymEngine::null;
    }

    // Return the smallest upper bound across all candidate constraints
    symbolic::Expression result = candidates[0];
    for (size_t i = 1; i < candidates.size(); ++i) {
        result = symbolic::min(result, candidates[i]);
    }

    return result;
}

AssumptionsAnalysis::AssumptionsAnalysis(StructuredSDFG& sdfg)
    : Analysis(sdfg) {

      };

void AssumptionsAnalysis::visit_block(structured_control_flow::Block* block,
                                      analysis::AnalysisManager& analysis_manager) {
    return;
};

void AssumptionsAnalysis::visit_sequence(structured_control_flow::Sequence* sequence,
                                         analysis::AnalysisManager& analysis_manager) {
    return;
};

void AssumptionsAnalysis::visit_if_else(structured_control_flow::IfElse* if_else,
                                        analysis::AnalysisManager& analysis_manager) {
    auto& users = analysis_manager.get<analysis::Users>();
    for (size_t i = 0; i < if_else->size(); i++) {
        auto& scope = if_else->at(i).first;
        auto condition = if_else->at(i).second;
        auto symbols = symbolic::atoms(condition);

        // Assumption: symbols are read-only in scope
        bool read_only = true;
        analysis::UsersView scope_users(users, scope);
        for (auto& sym : symbols) {
            if (scope_users.writes(sym->get_name()).size() > 0) {
                read_only = false;
                break;
            }
        }
        if (!read_only) {
            continue;
        }

        try {
            auto cnf = symbolic::conjunctive_normal_form(condition);

            // Assumption: no or conditions
            bool has_complex_clauses = false;
            for (auto& clause : cnf) {
                if (clause.size() > 1) {
                    has_complex_clauses = true;
                    break;
                }
            }
            if (has_complex_clauses) {
                continue;
            }

            for (auto& sym : symbols) {
                symbolic::Expression ub = symbolic::infty(1);
                symbolic::Expression lb = symbolic::infty(-1);
                for (auto& clause : cnf) {
                    auto& literal = clause[0];
                    // Literal does not use symbol
                    if (!symbolic::uses(literal, sym)) {
                        continue;
                    }

                    if (SymEngine::is_a<SymEngine::Equality>(*literal)) {
                        auto eq = SymEngine::rcp_dynamic_cast<const SymEngine::Equality>(literal);
                        auto lhs = eq->get_args()[0];
                        auto rhs = eq->get_args()[1];
                        if (SymEngine::eq(*lhs, *sym) && !symbolic::uses(rhs, sym)) {
                            ub = rhs;
                            lb = rhs;
                            break;
                        } else if (SymEngine::eq(*rhs, *sym) && !symbolic::uses(lhs, sym)) {
                            ub = lhs;
                            lb = lhs;
                            break;
                        }
                    } else if (SymEngine::is_a<SymEngine::StrictLessThan>(*literal)) {
                        auto lt =
                            SymEngine::rcp_dynamic_cast<const SymEngine::StrictLessThan>(literal);
                        auto lhs = lt->get_args()[0];
                        auto rhs = lt->get_args()[1];
                        if (SymEngine::eq(*lhs, *sym) && !symbolic::uses(rhs, sym)) {
                            if (symbolic::eq(ub, symbolic::infty(1))) {
                                ub = rhs;
                            } else {
                                ub = symbolic::min(ub, rhs);
                            }
                        } else if (SymEngine::eq(*rhs, *sym) && !symbolic::uses(lhs, sym)) {
                            if (symbolic::eq(lb, symbolic::infty(-1))) {
                                lb = lhs;
                            } else {
                                lb = symbolic::max(lb, lhs);
                            }
                        }
                    } else if (SymEngine::is_a<SymEngine::LessThan>(*literal)) {
                        auto lt = SymEngine::rcp_dynamic_cast<const SymEngine::LessThan>(literal);
                        auto lhs = lt->get_args()[0];
                        auto rhs = lt->get_args()[1];
                        if (SymEngine::eq(*lhs, *sym) && !symbolic::uses(rhs, sym)) {
                            if (symbolic::eq(ub, symbolic::infty(1))) {
                                ub = rhs;
                            } else {
                                ub = symbolic::min(ub, rhs);
                            }
                        } else if (SymEngine::eq(*rhs, *sym) && !symbolic::uses(lhs, sym)) {
                            if (symbolic::eq(lb, symbolic::infty(-1))) {
                                lb = lhs;
                            } else {
                                lb = symbolic::max(lb, lhs);
                            }
                        }
                    }
                }

                // Failed to infer anything
                if (symbolic::eq(ub, symbolic::infty(1)) && symbolic::eq(lb, symbolic::infty(-1))) {
                    continue;
                }

                if (this->assumptions_.find(&scope) == this->assumptions_.end()) {
                    this->assumptions_.insert({&scope, symbolic::Assumptions()});
                }
                auto& scope_assumptions = this->assumptions_[&scope];
                if (scope_assumptions.find(sym) == scope_assumptions.end()) {
                    scope_assumptions.insert({sym, symbolic::Assumption(sym)});
                }

                scope_assumptions[sym].constant(true);
                if (!symbolic::eq(ub, symbolic::infty(1))) {
                    scope_assumptions[sym].upper_bound(ub);
                }
                if (!symbolic::eq(lb, symbolic::infty(-1))) {
                    scope_assumptions[sym].lower_bound(lb);
                }
            }
        } catch (const symbolic::CNFException& e) {
            continue;
        }
    }
};

void AssumptionsAnalysis::visit_while(structured_control_flow::While* while_loop,
                                      analysis::AnalysisManager& analysis_manager) {
    return;
};

void AssumptionsAnalysis::visit_for(structured_control_flow::For* for_loop,
                                    analysis::AnalysisManager& analysis_manager) {
    auto indvar = for_loop->indvar();
    auto update = for_loop->update();

    // Add new assumptions
    auto& body = for_loop->root();
    if (this->assumptions_.find(&body) == this->assumptions_.end()) {
        this->assumptions_.insert({&body, symbolic::Assumptions()});
    }
    auto& body_assumptions = this->assumptions_[&body];

    // By definition: indvar and condition symbols are constant
    symbolic::SymbolSet syms = {indvar};
    for (auto& sym : symbolic::atoms(for_loop->condition())) {
        syms.insert(sym);
    }
    for (auto& sym : syms) {
        if (body_assumptions.find(sym) == body_assumptions.end()) {
            body_assumptions.insert({sym, symbolic::Assumption(sym)});
        }
        body_assumptions[sym].constant(true);
    }

    // Bounds of indvar

    // Prove that update is monotonic -> assume bounds
    auto& assums = this->get(*for_loop);
    if (!symbolic::series::is_monotonic(update, indvar, assums)) {
        return;
    }

    // Assumption 2: init is lower bound
    body_assumptions[indvar].lower_bound(for_loop->init());
    try {
        auto cnf = symbolic::conjunctive_normal_form(for_loop->condition());
        auto ub = cnf_to_upper_bound(cnf, indvar);
        if (ub == SymEngine::null) {
            return;
        }
        // Assumption 3: ub is upper bound
        body_assumptions[indvar].upper_bound(ub);

        // Assumption 4: any ub symbol is at least init
        for (auto& sym : symbolic::atoms(ub)) {
            body_assumptions[sym].lower_bound(symbolic::add(for_loop->init(), symbolic::one()));
        }
    } catch (const symbolic::CNFException& e) {
        return;
    }
}

void AssumptionsAnalysis::visit_map(structured_control_flow::Map* map,
                                    analysis::AnalysisManager& analysis_manager) {
    auto indvar = map->indvar();
    auto update = map->update();

    // Add new assumptions
    auto& body = map->root();
    if (this->assumptions_.find(&body) == this->assumptions_.end()) {
        this->assumptions_.insert({&body, symbolic::Assumptions()});
    }
    auto& body_assumptions = this->assumptions_[&body];

    // By definition: indvar and condition symbols are constant
    symbolic::SymbolSet syms = {indvar};
    for (auto& sym : symbolic::atoms(map->condition())) {
        syms.insert(sym);
    }
    for (auto& sym : syms) {
        if (body_assumptions.find(sym) == body_assumptions.end()) {
            body_assumptions.insert({sym, symbolic::Assumption(sym)});
        }
        body_assumptions[sym].constant(true);
    }

    // Bounds of indvar

    // Prove that update is monotonic -> assume bounds
    auto& assums = this->get(*map);
    if (!symbolic::series::is_monotonic(update, indvar, assums)) {
        return;
    }

    // Assumption 2: init is lower bound
    body_assumptions[indvar].lower_bound(map->init());
    try {
        auto cnf = symbolic::conjunctive_normal_form(map->condition());
        auto ub = cnf_to_upper_bound(cnf, indvar);
        if (ub == SymEngine::null) {
            return;
        }
        // Assumption 3: ub is upper bound
        body_assumptions[indvar].upper_bound(ub);

        // Assumption 4: any ub symbol is at least init
        for (auto& sym : symbolic::atoms(ub)) {
            body_assumptions[sym].lower_bound(symbolic::add(map->init(), symbolic::one()));
        }
    } catch (const symbolic::CNFException& e) {
        return;
    }
};

void AssumptionsAnalysis::traverse(structured_control_flow::Sequence& root,
                                   analysis::AnalysisManager& analysis_manager) {
    std::list<structured_control_flow::ControlFlowNode*> queue = {&root};
    while (!queue.empty()) {
        auto current = queue.front();
        queue.pop_front();

        if (auto block_stmt = dynamic_cast<structured_control_flow::Block*>(current)) {
            this->visit_block(block_stmt, analysis_manager);
        } else if (auto sequence_stmt = dynamic_cast<structured_control_flow::Sequence*>(current)) {
            this->visit_sequence(sequence_stmt, analysis_manager);
            for (size_t i = 0; i < sequence_stmt->size(); i++) {
                queue.push_back(&sequence_stmt->at(i).first);
            }
        } else if (auto if_else_stmt = dynamic_cast<structured_control_flow::IfElse*>(current)) {
            this->visit_if_else(if_else_stmt, analysis_manager);
            for (size_t i = 0; i < if_else_stmt->size(); i++) {
                queue.push_back(&if_else_stmt->at(i).first);
            }
        } else if (auto while_stmt = dynamic_cast<structured_control_flow::While*>(current)) {
            this->visit_while(while_stmt, analysis_manager);
            queue.push_back(&while_stmt->root());
        } else if (auto for_stmt = dynamic_cast<structured_control_flow::For*>(current)) {
            this->visit_for(for_stmt, analysis_manager);
            queue.push_back(&for_stmt->root());
        } else if (auto map_stmt = dynamic_cast<structured_control_flow::Map*>(current)) {
            this->visit_map(map_stmt, analysis_manager);
            queue.push_back(&map_stmt->root());
        }
    }
};

void AssumptionsAnalysis::run(analysis::AnalysisManager& analysis_manager) {
    this->assumptions_.clear();

    // Add sdfg assumptions
    this->assumptions_.insert({&sdfg_.root(), symbolic::Assumptions()});

    // Add additional assumptions
    for (auto& entry : this->additional_assumptions_) {
        this->assumptions_[&sdfg_.root()][entry.first] = entry.second;
    }

    // Forward propagate for each node
    this->traverse(sdfg_.root(), analysis_manager);
};

const symbolic::Assumptions AssumptionsAnalysis::get(structured_control_flow::ControlFlowNode& node,
                                                     bool include_trivial_bounds) {
    // Compute assumptions on the fly

    // Node-level assumptions
    symbolic::Assumptions assums;
    if (this->assumptions_.find(&node) != this->assumptions_.end()) {
        for (auto& entry : this->assumptions_[&node]) {
            assums.insert({entry.first, entry.second});
        }
    }

    AnalysisManager manager(this->sdfg_);
    auto& scope_analysis = manager.get<ScopeAnalysis>();

    auto scope = scope_analysis.parent_scope(&node);
    while (scope != nullptr) {
        // Don't overwrite lower scopes' assumptions
        if (this->assumptions_.find(scope) != this->assumptions_.end()) {
            for (auto& entry : this->assumptions_[scope]) {
                if (assums.find(entry.first) == assums.end()) {
                    assums.insert({entry.first, entry.second});
                }
            }
        }
        scope = scope_analysis.parent_scope(scope);
    }

    if (include_trivial_bounds) {
        for (auto& entry : sdfg_.assumptions()) {
            if (assums.find(entry.first) == assums.end()) {
                assums.insert({entry.first, entry.second});
            }
        }
    }

    return assums;
};

const symbolic::Assumptions AssumptionsAnalysis::get(structured_control_flow::ControlFlowNode& from,
                                                     structured_control_flow::ControlFlowNode& to,
                                                     bool include_trivial_bounds) {
    auto assums_from = this->get(from, include_trivial_bounds);
    auto assums_to = this->get(to, include_trivial_bounds);

    // Add lower scope assumptions to outer
    // ignore constants assumption
    for (auto& entry : assums_from) {
        if (assums_to.find(entry.first) == assums_to.end()) {
            auto assums_safe = assums_to;
            assums_safe.at(entry.first).constant(false);
            assums_to.insert({entry.first, assums_safe.at(entry.first)});
        } else {
            auto assums_safe = assums_to;
            assums_safe.at(entry.first).constant(entry.second.constant());
            assums_to[entry.first] = assums_safe.at(entry.first);
        }
    }

    return assums_to;
}

void AssumptionsAnalysis::add(symbolic::Assumptions& assums,
                              structured_control_flow::ControlFlowNode& node) {
    if (this->assumptions_.find(&node) == this->assumptions_.end()) {
        return;
    }

    for (auto& entry : this->assumptions_[&node]) {
        if (assums.find(entry.first) == assums.end()) {
            assums.insert({entry.first, entry.second});
        } else {
            assums[entry.first] = entry.second;
        }
    }
}

}  // namespace analysis
}  // namespace sdfg

1	#include "sdfg/analysis/assumptions_analysis.h"
2
3	#include <utility>
4	#include <vector>
5
6	#include "sdfg/analysis/scope_analysis.h"
7	#include "sdfg/analysis/users.h"
8	#include "sdfg/symbolic/assumptions.h"
9	#include "sdfg/symbolic/extreme_values.h"
10	#include "sdfg/symbolic/polynomials.h"
11	#include "sdfg/symbolic/series.h"
12
13	namespace sdfg {
14	namespace analysis {
15
16	symbolic::Expression AssumptionsAnalysis::cnf_to_upper_bound(const symbolic::CNF& cnf,	118✔
17	const symbolic::Symbol& indvar) {
18	std::vector<symbolic::Expression> candidates;	118✔
19
20	for (const auto& clause : cnf) {	246✔
21	for (const auto& literal : clause) {	257✔
22	// Comparison: indvar < expr
23	if (SymEngine::is_a<SymEngine::StrictLessThan>(*literal)) {	129✔
24	auto lt = SymEngine::rcp_static_cast<const SymEngine::StrictLessThan>(literal);	118✔
25	if (symbolic::eq(lt->get_arg1(), indvar) &&	236✔
26	!symbolic::uses(lt->get_arg2(), indvar)) {	118✔
27	auto ub = symbolic::sub(lt->get_arg2(), symbolic::one());	118✔
28	candidates.push_back(ub);	118✔
29	}	118✔
30	}	118✔
31	// Comparison: indvar <= expr
32	else if (SymEngine::is_a<SymEngine::LessThan>(*literal)) {	11✔
33	auto le = SymEngine::rcp_static_cast<const SymEngine::LessThan>(literal);	6✔
34	if (symbolic::eq(le->get_arg1(), indvar) &&	11✔
35	!symbolic::uses(le->get_arg2(), indvar)) {	5✔
36	candidates.push_back(le->get_arg2());	5✔
37	}	5✔
38	}	6✔
39	// Comparison: indvar == expr
40	else if (SymEngine::is_a<SymEngine::Equality>(*literal)) {	5✔
41	auto eq = SymEngine::rcp_static_cast<const SymEngine::Equality>(literal);	×
42	if (symbolic::eq(eq->get_arg1(), indvar) &&	×
43	!symbolic::uses(eq->get_arg2(), indvar)) {	×
44	candidates.push_back(eq->get_arg2());	×
45	}	×
46	}	×
47	}
48	}
49
50	if (candidates.empty()) {	118✔
51	return SymEngine::null;	4✔
52	}
53
54	// Return the smallest upper bound across all candidate constraints
55	symbolic::Expression result = candidates[0];	114✔
56	for (size_t i = 1; i < candidates.size(); ++i) {	123✔
57	result = symbolic::min(result, candidates[i]);	9✔
58	}	9✔
59
60	return result;	114✔
61	}	232✔
62
63	AssumptionsAnalysis::AssumptionsAnalysis(StructuredSDFG& sdfg)	292✔
64	: Analysis(sdfg) {	146✔
65
66	};	146✔
67
68	void AssumptionsAnalysis::visit_block(structured_control_flow::Block* block,	206✔
69	analysis::AnalysisManager& analysis_manager) {
70	return;	206✔
71	};
72
73	void AssumptionsAnalysis::visit_sequence(structured_control_flow::Sequence* sequence,	318✔
74	analysis::AnalysisManager& analysis_manager) {
75	return;	318✔
76	};
77
78	void AssumptionsAnalysis::visit_if_else(structured_control_flow::IfElse* if_else,	27✔
79	analysis::AnalysisManager& analysis_manager) {
80	auto& users = analysis_manager.get<analysis::Users>();	27✔
81	for (size_t i = 0; i < if_else->size(); i++) {	73✔
82	auto& scope = if_else->at(i).first;	46✔
83	auto condition = if_else->at(i).second;	46✔
84	auto symbols = symbolic::atoms(condition);	46✔
85
86	// Assumption: symbols are read-only in scope
87	bool read_only = true;	46✔
88	analysis::UsersView scope_users(users, scope);	46✔
89	for (auto& sym : symbols) {	73✔
90	if (scope_users.writes(sym->get_name()).size() > 0) {	39✔
91	read_only = false;	12✔
92	break;	12✔
93	}
94	}
95	if (!read_only) {	46✔
96	continue;	12✔
97	}
98
99	try {
100	auto cnf = symbolic::conjunctive_normal_form(condition);	34✔
101
102	// Assumption: no or conditions
103	bool has_complex_clauses = false;	34✔
104	for (auto& clause : cnf) {	69✔
105	if (clause.size() > 1) {	35✔
106	has_complex_clauses = true;	×
107	break;	×
108	}
109	}
110	if (has_complex_clauses) {	34✔
111	continue;	×
112	}
113
114	for (auto& sym : symbols) {	57✔
115	symbolic::Expression ub = symbolic::infty(1);	23✔
116	symbolic::Expression lb = symbolic::infty(-1);	23✔
117	for (auto& clause : cnf) {	39✔
118	auto& literal = clause[0];	26✔
119	// Literal does not use symbol
120	if (!symbolic::uses(literal, sym)) {	26✔
121	continue;	2✔
122	}
123
124	if (SymEngine::is_a<SymEngine::Equality>(*literal)) {	24✔
125	auto eq = SymEngine::rcp_dynamic_cast<const SymEngine::Equality>(literal);	10✔
126	auto lhs = eq->get_args()[0];	10✔
127	auto rhs = eq->get_args()[1];	10✔
128	if (SymEngine::eq(lhs, sym) && !symbolic::uses(rhs, sym)) {	10✔
129	ub = rhs;	1✔
130	lb = rhs;	1✔
131	break;	1✔
132	} else if (SymEngine::eq(rhs, sym) && !symbolic::uses(lhs, sym)) {	9✔
133	ub = lhs;	9✔
134	lb = lhs;	9✔
135	break;	9✔
136	}
137	} else if (SymEngine::is_a<SymEngine::StrictLessThan>(*literal)) {	24✔
138	auto lt =
139	SymEngine::rcp_dynamic_cast<const SymEngine::StrictLessThan>(literal);	8✔
140	auto lhs = lt->get_args()[0];	8✔
141	auto rhs = lt->get_args()[1];	8✔
142	if (SymEngine::eq(lhs, sym) && !symbolic::uses(rhs, sym)) {	8✔
143	if (symbolic::eq(ub, symbolic::infty(1))) {	5✔
144	ub = rhs;	5✔
145	} else {	5✔
146	ub = symbolic::min(ub, rhs);	×
147	}
148	} else if (SymEngine::eq(rhs, sym) && !symbolic::uses(lhs, sym)) {	8✔
149	if (symbolic::eq(lb, symbolic::infty(-1))) {	3✔
150	lb = lhs;	3✔
151	} else {	3✔
152	lb = symbolic::max(lb, lhs);	×
153	}
154	}	3✔
155	} else if (SymEngine::is_a<SymEngine::LessThan>(*literal)) {	14✔
156	auto lt = SymEngine::rcp_dynamic_cast<const SymEngine::LessThan>(literal);	1✔
157	auto lhs = lt->get_args()[0];	1✔
158	auto rhs = lt->get_args()[1];	1✔
159	if (SymEngine::eq(lhs, sym) && !symbolic::uses(rhs, sym)) {	1✔
160	if (symbolic::eq(ub, symbolic::infty(1))) {	×
161	ub = rhs;	×
162	} else {	×
163	ub = symbolic::min(ub, rhs);	×
164	}
165	} else if (SymEngine::eq(rhs, sym) && !symbolic::uses(lhs, sym)) {	1✔
166	if (symbolic::eq(lb, symbolic::infty(-1))) {	1✔
167	lb = lhs;	1✔
168	} else {	1✔
169	lb = symbolic::max(lb, lhs);	×
170	}
171	}	1✔
172	}	1✔
173	}
174
175	// Failed to infer anything
176	if (symbolic::eq(ub, symbolic::infty(1)) && symbolic::eq(lb, symbolic::infty(-1))) {	31✔
177	continue;	5✔
178	}
179
180	if (this->assumptions_.find(&scope) == this->assumptions_.end()) {	18✔
181	this->assumptions_.insert({&scope, symbolic::Assumptions()});	14✔
182	}	14✔
183	auto& scope_assumptions = this->assumptions_[&scope];	18✔
184	if (scope_assumptions.find(sym) == scope_assumptions.end()) {	18✔
185	scope_assumptions.insert({sym, symbolic::Assumption(sym)});	18✔
186	}	18✔
187
188	scope_assumptions[sym].constant(true);	18✔
189	if (!symbolic::eq(ub, symbolic::infty(1))) {	18✔
190	scope_assumptions[sym].upper_bound(ub);	15✔
191	}	15✔
192	if (!symbolic::eq(lb, symbolic::infty(-1))) {	18✔
193	scope_assumptions[sym].lower_bound(lb);	14✔
194	}	14✔
195	}	23✔
196	} catch (const symbolic::CNFException& e) {	34✔
197	continue;
198	}	×
199	}	46✔
200	};	27✔
201
202	void AssumptionsAnalysis::visit_while(structured_control_flow::While* while_loop,	7✔
203	analysis::AnalysisManager& analysis_manager) {
204	return;	7✔
205	};
206
207	void AssumptionsAnalysis::visit_for(structured_control_flow::For* for_loop,	108✔
208	analysis::AnalysisManager& analysis_manager) {
209	auto indvar = for_loop->indvar();	108✔
210	auto update = for_loop->update();	108✔
211
212	// Add new assumptions
213	auto& body = for_loop->root();	108✔
214	if (this->assumptions_.find(&body) == this->assumptions_.end()) {	108✔
215	this->assumptions_.insert({&body, symbolic::Assumptions()});	108✔
216	}	108✔
217	auto& body_assumptions = this->assumptions_[&body];	108✔
218
219	// By definition: indvar and condition symbols are constant
220	symbolic::SymbolSet syms = {indvar};	108✔
221	for (auto& sym : symbolic::atoms(for_loop->condition())) {	321✔
222	syms.insert(sym);	213✔
223	}
224	for (auto& sym : syms) {	321✔
225	if (body_assumptions.find(sym) == body_assumptions.end()) {	213✔
226	body_assumptions.insert({sym, symbolic::Assumption(sym)});	213✔
227	}	213✔
228	body_assumptions[sym].constant(true);	213✔
229	}
230
231	// Bounds of indvar
232
233	// Prove that update is monotonic -> assume bounds
234	auto& assums = this->get(*for_loop);	108✔
235	if (!symbolic::series::is_monotonic(update, indvar, assums)) {	108✔
236	return;	1✔
237	}
238
239	// Assumption 2: init is lower bound
240	body_assumptions[indvar].lower_bound(for_loop->init());	107✔
241	try {
242	auto cnf = symbolic::conjunctive_normal_form(for_loop->condition());	107✔
243	auto ub = cnf_to_upper_bound(cnf, indvar);	107✔
244	if (ub == SymEngine::null) {	107✔
245	return;	4✔
246	}
247	// Assumption 3: ub is upper bound
248	body_assumptions[indvar].upper_bound(ub);	103✔
249
250	// Assumption 4: any ub symbol is at least init
251	for (auto& sym : symbolic::atoms(ub)) {	202✔
252	body_assumptions[sym].lower_bound(symbolic::add(for_loop->init(), symbolic::one()));	99✔
253	}
254	} catch (const symbolic::CNFException& e) {	107✔
255	return;
256	}	×
257	}	108✔
258
259	void AssumptionsAnalysis::visit_map(structured_control_flow::Map* map,	11✔
260	analysis::AnalysisManager& analysis_manager) {
261	auto indvar = map->indvar();	11✔
262	auto update = map->update();	11✔
263
264	// Add new assumptions
265	auto& body = map->root();	11✔
266	if (this->assumptions_.find(&body) == this->assumptions_.end()) {	11✔
267	this->assumptions_.insert({&body, symbolic::Assumptions()});	11✔
268	}	11✔
269	auto& body_assumptions = this->assumptions_[&body];	11✔
270
271	// By definition: indvar and condition symbols are constant
272	symbolic::SymbolSet syms = {indvar};	11✔
273	for (auto& sym : symbolic::atoms(map->condition())) {	35✔
274	syms.insert(sym);	24✔
275	}
276	for (auto& sym : syms) {	35✔
277	if (body_assumptions.find(sym) == body_assumptions.end()) {	24✔
278	body_assumptions.insert({sym, symbolic::Assumption(sym)});	24✔
279	}	24✔
280	body_assumptions[sym].constant(true);	24✔
281	}
282
283	// Bounds of indvar
284
285	// Prove that update is monotonic -> assume bounds
286	auto& assums = this->get(*map);	11✔
287	if (!symbolic::series::is_monotonic(update, indvar, assums)) {	11✔
NEW 288	return;	×
289	}
290
291	// Assumption 2: init is lower bound
292	body_assumptions[indvar].lower_bound(map->init());	11✔
293	try {
294	auto cnf = symbolic::conjunctive_normal_form(map->condition());	11✔
295	auto ub = cnf_to_upper_bound(cnf, indvar);	11✔
296	if (ub == SymEngine::null) {	11✔
NEW 297	return;	×
298	}
299	// Assumption 3: ub is upper bound
300	body_assumptions[indvar].upper_bound(ub);	11✔
301
302	// Assumption 4: any ub symbol is at least init
303	for (auto& sym : symbolic::atoms(ub)) {	24✔
304	body_assumptions[sym].lower_bound(symbolic::add(map->init(), symbolic::one()));	13✔
305	}
306	} catch (const symbolic::CNFException& e) {	11✔
307	return;
NEW 308	}	×
309	};	11✔
310
311	void AssumptionsAnalysis::traverse(structured_control_flow::Sequence& root,	146✔
312	analysis::AnalysisManager& analysis_manager) {
313	std::list<structured_control_flow::ControlFlowNode*> queue = {&root};	146✔
314	while (!queue.empty()) {	831✔
315	auto current = queue.front();	685✔
316	queue.pop_front();	685✔
317
318	if (auto block_stmt = dynamic_cast<structured_control_flow::Block*>(current)) {	685✔
319	this->visit_block(block_stmt, analysis_manager);	206✔
320	} else if (auto sequence_stmt = dynamic_cast<structured_control_flow::Sequence*>(current)) {	685✔
321	this->visit_sequence(sequence_stmt, analysis_manager);	318✔
322	for (size_t i = 0; i < sequence_stmt->size(); i++) {	685✔
323	queue.push_back(&sequence_stmt->at(i).first);	367✔
324	}	367✔
325	} else if (auto if_else_stmt = dynamic_cast<structured_control_flow::IfElse*>(current)) {	479✔
326	this->visit_if_else(if_else_stmt, analysis_manager);	27✔
327	for (size_t i = 0; i < if_else_stmt->size(); i++) {	73✔
328	queue.push_back(&if_else_stmt->at(i).first);	46✔
329	}	46✔
330	} else if (auto while_stmt = dynamic_cast<structured_control_flow::While*>(current)) {	161✔
331	this->visit_while(while_stmt, analysis_manager);	7✔
332	queue.push_back(&while_stmt->root());	7✔
333	} else if (auto for_stmt = dynamic_cast<structured_control_flow::For*>(current)) {	134✔
334	this->visit_for(for_stmt, analysis_manager);	108✔
335	queue.push_back(&for_stmt->root());	108✔
336	} else if (auto map_stmt = dynamic_cast<structured_control_flow::Map*>(current)) {	127✔
337	this->visit_map(map_stmt, analysis_manager);	11✔
338	queue.push_back(&map_stmt->root());	11✔
339	}	11✔
340	}
341	};	146✔
342
343	void AssumptionsAnalysis::run(analysis::AnalysisManager& analysis_manager) {	146✔
344	this->assumptions_.clear();	146✔
345
346	// Add sdfg assumptions
347	this->assumptions_.insert({&sdfg_.root(), symbolic::Assumptions()});	146✔
348
349	// Add additional assumptions
350	for (auto& entry : this->additional_assumptions_) {	146✔
351	this->assumptions_[&sdfg_.root()][entry.first] = entry.second;	×
352	}
353
354	// Forward propagate for each node
355	this->traverse(sdfg_.root(), analysis_manager);	146✔
356	};	146✔
357
358	const symbolic::Assumptions AssumptionsAnalysis::get(structured_control_flow::ControlFlowNode& node,	549✔
359	bool include_trivial_bounds) {
360	// Compute assumptions on the fly
361
362	// Node-level assumptions
363	symbolic::Assumptions assums;	549✔
364	if (this->assumptions_.find(&node) != this->assumptions_.end()) {	549✔
365	for (auto& entry : this->assumptions_[&node]) {	498✔
366	assums.insert({entry.first, entry.second});	330✔
367	}
368	}	168✔
369
370	AnalysisManager manager(this->sdfg_);	549✔
371	auto& scope_analysis = manager.get<ScopeAnalysis>();	549✔
372
373	auto scope = scope_analysis.parent_scope(&node);	549✔
374	while (scope != nullptr) {	1,848✔
375	// Don't overwrite lower scopes' assumptions
376	if (this->assumptions_.find(scope) != this->assumptions_.end()) {	1,299✔
377	for (auto& entry : this->assumptions_[scope]) {	1,416✔
378	if (assums.find(entry.first) == assums.end()) {	584✔
379	assums.insert({entry.first, entry.second});	454✔
380	}	454✔
381	}
382	}	832✔
383	scope = scope_analysis.parent_scope(scope);	1,299✔
384	}
385
386	if (include_trivial_bounds) {	549✔
387	for (auto& entry : sdfg_.assumptions()) {	1,616✔
388	if (assums.find(entry.first) == assums.end()) {	1,192✔
389	assums.insert({entry.first, entry.second});	475✔
390	}	475✔
391	}
392	}	424✔
393
394	return assums;	549✔
395	};	549✔
396
397	const symbolic::Assumptions AssumptionsAnalysis::get(structured_control_flow::ControlFlowNode& from,	122✔
398	structured_control_flow::ControlFlowNode& to,
399	bool include_trivial_bounds) {
400	auto assums_from = this->get(from, include_trivial_bounds);	122✔
401	auto assums_to = this->get(to, include_trivial_bounds);	122✔
402
403	// Add lower scope assumptions to outer
404	// ignore constants assumption
405	for (auto& entry : assums_from) {	464✔
406	if (assums_to.find(entry.first) == assums_to.end()) {	342✔
407	auto assums_safe = assums_to;	×
408	assums_safe.at(entry.first).constant(false);	×
409	assums_to.insert({entry.first, assums_safe.at(entry.first)});	×
410	} else {	×
411	auto assums_safe = assums_to;	342✔
412	assums_safe.at(entry.first).constant(entry.second.constant());	342✔
413	assums_to[entry.first] = assums_safe.at(entry.first);	342✔
414	}	342✔
415	}
416
417	return assums_to;	122✔
418	}	122✔
419
420	void AssumptionsAnalysis::add(symbolic::Assumptions& assums,	×
421	structured_control_flow::ControlFlowNode& node) {
422	if (this->assumptions_.find(&node) == this->assumptions_.end()) {	×
423	return;	×
424	}
425
426	for (auto& entry : this->assumptions_[&node]) {	×
427	if (assums.find(entry.first) == assums.end()) {	×
428	assums.insert({entry.first, entry.second});	×
429	} else {	×
430	assums[entry.first] = entry.second;	×
431	}
432	}
433	}	×
434
435	} // namespace analysis
436	} // namespace sdfg

daisytuner / sdfglib / 15827874660

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