16069945621

Committed 04 Jul 2025 08:56AM UTC coverage: 64.375% (-0.2%) from 64.606%

Build # 16069945621

Build Type

push

github

Committed by

web-flow

Commit Message

Merge pull request #137 from daisytuner/clang-format

runs clang-format on codebase

Run Details

609 of 827 new or added lines in 63 files covered. (73.64%)

46 existing lines in 30 files now uncovered.

8578 of 13325 relevant lines covered (64.38%)

177.24 hits per line

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

88.08

/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);
    }

    // Map of indvar
    body_assumptions[indvar].map(update);

    // 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);
    }

    // Map of indvar
    body_assumptions[indvar].map(update);

    // 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) {
        if (this->assumptions_.find(scope) != this->assumptions_.end()) {
            for (auto& entry : this->assumptions_[scope]) {
                if (assums.find(entry.first) == assums.end()) {
                    // New assumption
                    assums.insert({entry.first, entry.second});
                } else {
                    // Merge assumptions from lower scopes
                    auto& lower_assum = assums[entry.first];
                    auto lower_ub = lower_assum.upper_bound();
                    auto lower_lb = lower_assum.lower_bound();
                    auto new_ub = symbolic::min(entry.second.upper_bound(), lower_ub);
                    auto new_lb = symbolic::max(entry.second.lower_bound(), lower_lb);
                    lower_assum.upper_bound(new_ub);
                    lower_assum.lower_bound(new_lb);

                    if (lower_assum.map() == SymEngine::null) {
                        lower_assum.map(entry.second.map());
                    }
                    if (!lower_assum.constant()) {
                        lower_assum.constant(entry.second.constant());
                    }
                }
            }
        }
        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 lower_assum = assums_to[entry.first];
            auto lower_ub = lower_assum.upper_bound();
            auto lower_lb = lower_assum.lower_bound();
            auto new_ub = symbolic::min(entry.second.upper_bound(), lower_ub);
            auto new_lb = symbolic::max(entry.second.lower_bound(), lower_lb);
            lower_assum.upper_bound(new_ub);
            lower_assum.lower_bound(new_lb);

            if (lower_assum.map() == SymEngine::null) {
                lower_assum.map(entry.second.map());
            }
            lower_assum.constant(entry.second.constant());
            assums_to[entry.first] = lower_assum;
        }
    }

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

daisytuner / sdfglib / 16069945621

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