17701640355

Committed 13 Sep 2025 08:25PM UTC coverage: 60.51%. Remained the same

Build # 17701640355

Build Type

push

github

Committed by

web-flow

Commit Message

Merge pull request #226 from daisytuner/infty

uses infty constants and thread-safe rcp pointers

Run Details

16 of 20 new or added lines in 3 files covered. (80.0%)

1 existing line in 1 file now uncovered.

9445 of 15609 relevant lines covered (60.51%)

106.8 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 = SymEngine::Inf;
                symbolic::Expression lb = SymEngine::NegInf;
                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, SymEngine::Inf)) {
                                ub = rhs;
                            } else {
                                ub = symbolic::min(ub, rhs);
                            }
                        } else if (SymEngine::eq(*rhs, *sym) && !symbolic::uses(lhs, sym)) {
                            if (symbolic::eq(lb, SymEngine::NegInf)) {
                                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, SymEngine::Inf)) {
                                ub = rhs;
                            } else {
                                ub = symbolic::min(ub, rhs);
                            }
                        } else if (SymEngine::eq(*rhs, *sym) && !symbolic::uses(lhs, sym)) {
                            if (symbolic::eq(lb, SymEngine::NegInf)) {
                                lb = lhs;
                            } else {
                                lb = symbolic::max(lb, lhs);
                            }
                        }
                    }
                }

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

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