18715914051

Committed 22 Oct 2025 12:19PM UTC coverage: 62.358% (+0.7%) from 61.619%

Build # 18715914051

Build Type

push

github

Committed by

web-flow

Commit Message

Merge pull request #292 from daisytuner/flop-analysis-extension

Extension for the FlopAnalysis

Run Details

357 of 423 new or added lines in 10 files covered. (84.4%)

9 existing lines in 3 files now uncovered.

9711 of 15573 relevant lines covered (62.36%)

104.01 hits per line

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

87.92

/src/analysis/assumptions_analysis.cpp

#include "sdfg/analysis/assumptions_analysis.h"

#include <utility>
#include <vector>

#include "sdfg/analysis/analysis.h"
#include "sdfg/analysis/scope_analysis.h"
#include "sdfg/analysis/users.h"
#include "sdfg/data_flow/access_node.h"
#include "sdfg/data_flow/memlet.h"
#include "sdfg/structured_control_flow/structured_loop.h"
#include "sdfg/symbolic/assumptions.h"
#include "sdfg/symbolic/series.h"
#include "sdfg/symbolic/symbolic.h"
#include "sdfg/types/type.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) {
    return;
};

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

void AssumptionsAnalysis::
    visit_structured_loop(structured_control_flow::StructuredLoop* loop, analysis::AnalysisManager& analysis_manager) {
    auto indvar = loop->indvar();
    auto update = loop->update();
    auto init = loop->init();

    // Add new assumptions
    auto& body = 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(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);

    // Determine non-tight lower and upper bounds from inverse index access
    std::vector<symbolic::Expression> lbs, ubs;
    for (auto user : this->users_analysis_->reads(indvar->get_name())) {
        if (auto* memlet = dynamic_cast<data_flow::Memlet*>(user->element())) {
            const types::IType* memlet_type = &memlet->base_type();
            for (long long i = memlet->subset().size() - 1; i >= 0; i--) {
                symbolic::Expression num_elements = SymEngine::null;
                if (auto* pointer_type = dynamic_cast<const types::Pointer*>(memlet_type)) {
                    memlet_type = &pointer_type->pointee_type();
                } else if (auto* array_type = dynamic_cast<const types::Array*>(memlet_type)) {
                    memlet_type = &array_type->element_type();
                    num_elements = array_type->num_elements();
                } else {
                    break;
                }
                if (!symbolic::uses(memlet->subset().at(i), indvar)) {
                    continue;
                }
                symbolic::Expression inverse = symbolic::inverse(memlet->subset().at(i), indvar);
                if (inverse.is_null()) {
                    continue;
                }
                lbs.push_back(symbolic::subs(inverse, indvar, symbolic::zero()));
                if (num_elements.is_null()) {
                    std::string container;
                    if (memlet->src_conn() == "void") {
                        container = dynamic_cast<data_flow::AccessNode&>(memlet->src()).data();
                    } else {
                        container = dynamic_cast<data_flow::AccessNode&>(memlet->dst()).data();
                    }
                    if (this->is_parameter(container)) {
                        ubs.push_back(symbolic::sub(
                            symbolic::subs(inverse, indvar, symbolic::dynamic_sizeof(symbolic::symbol(container))),
                            symbolic::one()
                        ));
                    }
                } else {
                    ubs.push_back(symbolic::subs(inverse, indvar, num_elements));
                }
            }
        }
    }
    for (auto lb : lbs) {
        body_assumptions[indvar].add_lower_bound(lb);
    }
    for (auto ub : ubs) {
        body_assumptions[indvar].add_upper_bound(ub);
    }

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

    // Assumption: init is tight lower bound for indvar
    body_assumptions[indvar].tight_lower_bound(init);
    body_assumptions[indvar].lower_bound_deprecated(init);

    // Assumption: inverse index access lower bounds are lower bound for init
    if (SymEngine::is_a<SymEngine::Symbol>(*init) && !lbs.empty()) {
        auto sym = SymEngine::rcp_static_cast<const SymEngine::Symbol>(init);
        if (!body_assumptions.contains(sym)) {
            body_assumptions.insert({sym, symbolic::Assumption(sym)});
        }
        for (auto lb : lbs) {
            body_assumptions[sym].add_lower_bound(lb);
        }
    }

    try {
        auto cnf = symbolic::conjunctive_normal_form(loop->condition());
        auto ub = cnf_to_upper_bound(cnf, indvar);
        if (ub == SymEngine::null) {
            return;
        }
        // Assumption: upper bound ub is tight for indvar if
        body_assumptions[indvar].upper_bound_deprecated(ub);
        // TODO: handle non-contiguous tight upper bounds with modulo
        // Example: for (i = 0; i < n; i += 3) -> tight_upper_bound = (n - 1) - ((n - 1) % 3)
        if (symbolic::series::is_contiguous(update, indvar, assums)) {
            body_assumptions[indvar].tight_upper_bound(ub);
        }

        // Assumption: inverse index access upper bounds are upper bound for ub
        if (SymEngine::is_a<SymEngine::Symbol>(*ub) && !ubs.empty()) {
            auto sym = SymEngine::rcp_static_cast<const SymEngine::Symbol>(ub);
            if (!body_assumptions.contains(sym)) {
                body_assumptions.insert({sym, symbolic::Assumption(sym)});
            }
            for (auto ub : ubs) {
                body_assumptions[sym].add_upper_bound(ub);
            }
        }

        // Assumption: any ub symbol is at least init
        for (auto& sym : symbolic::atoms(ub)) {
            body_assumptions[sym].add_lower_bound(symbolic::add(init, symbolic::one()));
            body_assumptions[sym].lower_bound_deprecated(symbolic::add(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 loop_stmt = dynamic_cast<structured_control_flow::StructuredLoop*>(current)) {
            this->visit_structured_loop(loop_stmt, analysis_manager);
            queue.push_back(&loop_stmt->root());
        }
    }
};

void AssumptionsAnalysis::determine_parameters(analysis::AnalysisManager& analysis_manager) {
    for (auto& container : this->sdfg_.arguments()) {
        bool readonly = true;
        Use not_allowed;
        switch (this->sdfg_.type(container).type_id()) {
            case types::TypeID::Scalar:
                not_allowed = Use::WRITE;
                break;
            case types::TypeID::Pointer:
                not_allowed = Use::MOVE;
                break;
            case types::TypeID::Array:
            case types::TypeID::Structure:
            case types::TypeID::Reference:
            case types::TypeID::Function:
                continue;
        }
        for (auto user : this->users_analysis_->uses(container)) {
            if (user->use() == not_allowed) {
                readonly = false;
                break;
            }
        }
        if (readonly) {
            this->parameters_.insert(symbolic::symbol(container));
        }
    }
}

void AssumptionsAnalysis::run(analysis::AnalysisManager& analysis_manager) {
    this->assumptions_.clear();
    this->parameters_.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;
    }

    this->scope_analysis_ = &analysis_manager.get<ScopeAnalysis>();
    this->users_analysis_ = &analysis_manager.get<Users>();

    // Determine parameters
    this->determine_parameters(analysis_manager);

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

    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_deprecated = lower_assum.upper_bound_deprecated();
                    auto lower_lb_deprecated = lower_assum.lower_bound_deprecated();
                    auto new_ub_deprecated = symbolic::min(entry.second.upper_bound_deprecated(), lower_ub_deprecated);
                    auto new_lb_deprecated = symbolic::max(entry.second.lower_bound_deprecated(), lower_lb_deprecated);
                    lower_assum.upper_bound_deprecated(new_ub_deprecated);
                    lower_assum.lower_bound_deprecated(new_lb_deprecated);

                    for (auto ub : entry.second.upper_bounds()) {
                        lower_assum.add_upper_bound(ub);
                    }
                    for (auto lb : entry.second.lower_bounds()) {
                        lower_assum.add_lower_bound(lb);
                    }

                    auto lower_tight_ub = lower_assum.tight_upper_bound();
                    if (!entry.second.tight_upper_bound().is_null() && !lower_tight_ub.is_null()) {
                        auto new_tight_ub = symbolic::min(entry.second.tight_upper_bound(), lower_tight_ub);
                        lower_assum.tight_upper_bound(new_tight_ub);
                    }
                    auto lower_tight_lb = lower_assum.tight_lower_bound();
                    if (!entry.second.tight_lower_bound().is_null() && !lower_tight_lb.is_null()) {
                        auto new_tight_lb = symbolic::max(entry.second.tight_lower_bound(), lower_tight_lb);
                        lower_assum.tight_lower_bound(new_tight_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_deprecated = lower_assum.upper_bound_deprecated();
            auto lower_lb_deprecated = lower_assum.lower_bound_deprecated();
            auto new_ub_deprecated = symbolic::min(entry.second.upper_bound_deprecated(), lower_ub_deprecated);
            auto new_lb_deprecated = symbolic::max(entry.second.lower_bound_deprecated(), lower_lb_deprecated);
            lower_assum.upper_bound_deprecated(new_ub_deprecated);
            lower_assum.lower_bound_deprecated(new_lb_deprecated);

            for (auto ub : entry.second.upper_bounds()) {
                lower_assum.add_upper_bound(ub);
            }
            for (auto lb : entry.second.lower_bounds()) {
                lower_assum.add_lower_bound(lb);
            }

            auto lower_tight_ub = lower_assum.tight_upper_bound();
            if (!entry.second.tight_upper_bound().is_null() && !lower_tight_ub.is_null()) {
                auto new_tight_ub = symbolic::min(entry.second.tight_upper_bound(), lower_tight_ub);
                lower_assum.tight_upper_bound(new_tight_ub);
            }
            auto lower_tight_lb = lower_assum.tight_lower_bound();
            if (!entry.second.tight_lower_bound().is_null() && !lower_tight_lb.is_null()) {
                auto new_tight_lb = symbolic::max(entry.second.tight_lower_bound(), lower_tight_lb);
                lower_assum.tight_lower_bound(new_tight_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;
}

const symbolic::SymbolSet& AssumptionsAnalysis::parameters() { return this->parameters_; }

bool AssumptionsAnalysis::is_parameter(const symbolic::Symbol& container) {
    return this->parameters_.contains(container);
}

bool AssumptionsAnalysis::is_parameter(const std::string& container) {
    return this->is_parameter(symbolic::symbol(container));
}

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/analysis.h"
7	#include "sdfg/analysis/scope_analysis.h"
8	#include "sdfg/analysis/users.h"
9	#include "sdfg/data_flow/access_node.h"
10	#include "sdfg/data_flow/memlet.h"
11	#include "sdfg/structured_control_flow/structured_loop.h"
12	#include "sdfg/symbolic/assumptions.h"
13	#include "sdfg/symbolic/series.h"
14	#include "sdfg/symbolic/symbolic.h"
15	#include "sdfg/types/type.h"
16
17	namespace sdfg {
18	namespace analysis {
19
20	symbolic::Expression AssumptionsAnalysis::cnf_to_upper_bound(const symbolic::CNF& cnf, const symbolic::Symbol indvar) {	123✔
21	std::vector<symbolic::Expression> candidates;	123✔
22
23	for (const auto& clause : cnf) {	258✔
24	for (const auto& literal : clause) {	271✔
25	// Comparison: indvar < expr
26	if (SymEngine::is_a<SymEngine::StrictLessThan>(*literal)) {	136✔
27	auto lt = SymEngine::rcp_static_cast<const SymEngine::StrictLessThan>(literal);	122✔
28	if (symbolic::eq(lt->get_arg1(), indvar) && !symbolic::uses(lt->get_arg2(), indvar)) {	122✔
29	auto ub = symbolic::sub(lt->get_arg2(), symbolic::one());	122✔
30	candidates.push_back(ub);	122✔
31	}	122✔
32	}	122✔
33	// Comparison: indvar <= expr
34	else if (SymEngine::is_a<SymEngine::LessThan>(*literal)) {	14✔
35	auto le = SymEngine::rcp_static_cast<const SymEngine::LessThan>(literal);	7✔
36	if (symbolic::eq(le->get_arg1(), indvar) && !symbolic::uses(le->get_arg2(), indvar)) {	7✔
37	candidates.push_back(le->get_arg2());	6✔
38	}	6✔
39	}	7✔
40	// Comparison: indvar == expr
41	else if (SymEngine::is_a<SymEngine::Equality>(*literal)) {	7✔
42	auto eq = SymEngine::rcp_static_cast<const SymEngine::Equality>(literal);	×
43	if (symbolic::eq(eq->get_arg1(), indvar) && !symbolic::uses(eq->get_arg2(), indvar)) {	×
44	candidates.push_back(eq->get_arg2());	×
45	}	×
46	}	×
47	}
48	}
49
50	if (candidates.empty()) {	123✔
51	return SymEngine::null;	6✔
52	}
53
54	// Return the smallest upper bound across all candidate constraints
55	symbolic::Expression result = candidates[0];	117✔
56	for (size_t i = 1; i < candidates.size(); ++i) {	128✔
57	result = symbolic::min(result, candidates[i]);	11✔
58	}	11✔
59
60	return result;	117✔
61	}	240✔
62
63	AssumptionsAnalysis::AssumptionsAnalysis(StructuredSDFG& sdfg)	386✔
64	: Analysis(sdfg) {	193✔
65
66	};	193✔
67
68	void AssumptionsAnalysis::visit_block(structured_control_flow::Block* block, analysis::AnalysisManager& analysis_manager) {	201✔
69	return;	201✔
70	};
71
72	void AssumptionsAnalysis::
73	visit_sequence(structured_control_flow::Sequence* sequence, analysis::AnalysisManager& analysis_manager) {	376✔
74	return;	376✔
75	};
76
77	void AssumptionsAnalysis::
78	visit_if_else(structured_control_flow::IfElse* if_else, analysis::AnalysisManager& analysis_manager) {	24✔
79	return;	24✔
80	};
81
82	void AssumptionsAnalysis::
83	visit_while(structured_control_flow::While* while_loop, analysis::AnalysisManager& analysis_manager) {	14✔
84	return;	14✔
85	};
86
87	void AssumptionsAnalysis::
88	visit_structured_loop(structured_control_flow::StructuredLoop* loop, analysis::AnalysisManager& analysis_manager) {	126✔
89	auto indvar = loop->indvar();	126✔
90	auto update = loop->update();	126✔
91	auto init = loop->init();	126✔
92
93	// Add new assumptions
94	auto& body = loop->root();	126✔
95	if (this->assumptions_.find(&body) == this->assumptions_.end()) {	126✔
96	this->assumptions_.insert({&body, symbolic::Assumptions()});	126✔
97	}	126✔
98	auto& body_assumptions = this->assumptions_[&body];	126✔
99
100	// By definition: indvar and condition symbols are constant
101	symbolic::SymbolSet syms = {indvar};	126✔
102	for (auto& sym : symbolic::atoms(loop->condition())) {	361✔
103	syms.insert(sym);	235✔
104	}
105	for (auto& sym : syms) {	361✔
106	if (body_assumptions.find(sym) == body_assumptions.end()) {	235✔
107	body_assumptions.insert({sym, symbolic::Assumption(sym)});	235✔
108	}	235✔
109	body_assumptions[sym].constant(true);	235✔
110	}
111
112	// Map of indvar
113	body_assumptions[indvar].map(update);	126✔
114
115	// Determine non-tight lower and upper bounds from inverse index access
116	std::vector<symbolic::Expression> lbs, ubs;	126✔
117	for (auto user : this->users_analysis_->reads(indvar->get_name())) {	583✔
118	if (auto* memlet = dynamic_cast<data_flow::Memlet*>(user->element())) {	457✔
119	const types::IType* memlet_type = &memlet->base_type();	179✔
120	for (long long i = memlet->subset().size() - 1; i >= 0; i--) {	422✔
121	symbolic::Expression num_elements = SymEngine::null;	243✔
122	if (auto* pointer_type = dynamic_cast<const types::Pointer*>(memlet_type)) {	243✔
123	memlet_type = &pointer_type->pointee_type();	171✔
124	} else if (auto* array_type = dynamic_cast<const types::Array*>(memlet_type)) {	243✔
125	memlet_type = &array_type->element_type();	72✔
126	num_elements = array_type->num_elements();	72✔
127	} else {	72✔
NEW 128	break;	×
129	}
130	if (!symbolic::uses(memlet->subset().at(i), indvar)) {	243✔
131	continue;	64✔
132	}
133	symbolic::Expression inverse = symbolic::inverse(memlet->subset().at(i), indvar);	179✔
134	if (inverse.is_null()) {	179✔
135	continue;	1✔
136	}
137	lbs.push_back(symbolic::subs(inverse, indvar, symbolic::zero()));	178✔
138	if (num_elements.is_null()) {	178✔
139	std::string container;	138✔
140	if (memlet->src_conn() == "void") {	138✔
141	container = dynamic_cast<data_flow::AccessNode&>(memlet->src()).data();	80✔
142	} else {	80✔
143	container = dynamic_cast<data_flow::AccessNode&>(memlet->dst()).data();	58✔
144	}
145	if (this->is_parameter(container)) {	138✔
146	ubs.push_back(symbolic::sub(	136✔
147	symbolic::subs(inverse, indvar, symbolic::dynamic_sizeof(symbolic::symbol(container))),	136✔
148	symbolic::one()	136✔
149	));
150	}	136✔
151	} else {	138✔
152	ubs.push_back(symbolic::subs(inverse, indvar, num_elements));	40✔
153	}
154	}	243✔
155	}	179✔
156	}
157	for (auto lb : lbs) {	304✔
158	body_assumptions[indvar].add_lower_bound(lb);	178✔
159	}	178✔
160	for (auto ub : ubs) {	302✔
161	body_assumptions[indvar].add_upper_bound(ub);	176✔
162	}	176✔
163
164	// Prove that update is monotonic -> assume bounds
165	auto& assums = this->get(*loop);	126✔
166	if (!symbolic::series::is_monotonic(update, indvar, assums)) {	126✔
167	return;	3✔
168	}
169
170	// Assumption: init is tight lower bound for indvar
171	body_assumptions[indvar].tight_lower_bound(init);	123✔
172	body_assumptions[indvar].lower_bound_deprecated(init);	123✔
173
174	// Assumption: inverse index access lower bounds are lower bound for init
175	if (SymEngine::is_a<SymEngine::Symbol>(*init) && !lbs.empty()) {	123✔
176	auto sym = SymEngine::rcp_static_cast<const SymEngine::Symbol>(init);	10✔
177	if (!body_assumptions.contains(sym)) {	10✔
178	body_assumptions.insert({sym, symbolic::Assumption(sym)});	4✔
179	}	4✔
180	for (auto lb : lbs) {	30✔
181	body_assumptions[sym].add_lower_bound(lb);	20✔
182	}	20✔
183	}	10✔
184
185	try {
186	auto cnf = symbolic::conjunctive_normal_form(loop->condition());	123✔
187	auto ub = cnf_to_upper_bound(cnf, indvar);	123✔
188	if (ub == SymEngine::null) {	123✔
189	return;	6✔
190	}
191	// Assumption: upper bound ub is tight for indvar if
192	body_assumptions[indvar].upper_bound_deprecated(ub);	117✔
193	// TODO: handle non-contiguous tight upper bounds with modulo
194	// Example: for (i = 0; i < n; i += 3) -> tight_upper_bound = (n - 1) - ((n - 1) % 3)
195	if (symbolic::series::is_contiguous(update, indvar, assums)) {	117✔
196	body_assumptions[indvar].tight_upper_bound(ub);	105✔
197	}	105✔
198
199	// Assumption: inverse index access upper bounds are upper bound for ub
200	if (SymEngine::is_a<SymEngine::Symbol>(*ub) && !ubs.empty()) {	117✔
NEW 201	auto sym = SymEngine::rcp_static_cast<const SymEngine::Symbol>(ub);	×
NEW 202	if (!body_assumptions.contains(sym)) {	×
NEW 203	body_assumptions.insert({sym, symbolic::Assumption(sym)});	×
NEW 204	}	×
NEW 205	for (auto ub : ubs) {	×
NEW 206	body_assumptions[sym].add_upper_bound(ub);	×
NEW 207	}	×
NEW 208	}	×
209
210	// Assumption: any ub symbol is at least init
211	for (auto& sym : symbolic::atoms(ub)) {	218✔
212	body_assumptions[sym].add_lower_bound(symbolic::add(init, symbolic::one()));	101✔
213	body_assumptions[sym].lower_bound_deprecated(symbolic::add(init, symbolic::one()));	101✔
214	}
215	} catch (const symbolic::CNFException& e) {	123✔
216	return;
217	}	×
218	}	126✔
219
220	void AssumptionsAnalysis::traverse(structured_control_flow::Sequence& root, analysis::AnalysisManager& analysis_manager) {	193✔
221	std::list<structured_control_flow::ControlFlowNode*> queue = {&root};	193✔
222	while (!queue.empty()) {	949✔
223	auto current = queue.front();	756✔
224	queue.pop_front();	756✔
225
226	if (auto block_stmt = dynamic_cast<structured_control_flow::Block*>(current)) {	756✔
227	this->visit_block(block_stmt, analysis_manager);	201✔
228	} else if (auto sequence_stmt = dynamic_cast<structured_control_flow::Sequence*>(current)) {	756✔
229	this->visit_sequence(sequence_stmt, analysis_manager);	376✔
230	for (size_t i = 0; i < sequence_stmt->size(); i++) {	758✔
231	queue.push_back(&sequence_stmt->at(i).first);	382✔
232	}	382✔
233	} else if (auto if_else_stmt = dynamic_cast<structured_control_flow::IfElse*>(current)) {	555✔
234	this->visit_if_else(if_else_stmt, analysis_manager);	24✔
235	for (size_t i = 0; i < if_else_stmt->size(); i++) {	65✔
236	queue.push_back(&if_else_stmt->at(i).first);	41✔
237	}	41✔
238	} else if (auto while_stmt = dynamic_cast<structured_control_flow::While*>(current)) {	179✔
239	this->visit_while(while_stmt, analysis_manager);	14✔
240	queue.push_back(&while_stmt->root());	14✔
241	} else if (auto loop_stmt = dynamic_cast<structured_control_flow::StructuredLoop*>(current)) {	155✔
242	this->visit_structured_loop(loop_stmt, analysis_manager);	126✔
243	queue.push_back(&loop_stmt->root());	126✔
244	}	126✔
245	}
246	};	193✔
247
248	void AssumptionsAnalysis::determine_parameters(analysis::AnalysisManager& analysis_manager) {	193✔
249	for (auto& container : this->sdfg_.arguments()) {	403✔
250	bool readonly = true;	210✔
251	Use not_allowed;
252	switch (this->sdfg_.type(container).type_id()) {	210✔
253	case types::TypeID::Scalar:
254	not_allowed = Use::WRITE;	120✔
255	break;	120✔
256	case types::TypeID::Pointer:
257	not_allowed = Use::MOVE;	88✔
258	break;	88✔
259	case types::TypeID::Array:
260	case types::TypeID::Structure:
261	case types::TypeID::Reference:
262	case types::TypeID::Function:
263	continue;	2✔
264	}
265	for (auto user : this->users_analysis_->uses(container)) {	465✔
266	if (user->use() == not_allowed) {	257✔
267	readonly = false;	14✔
268	break;	14✔
269	}
270	}
271	if (readonly) {	208✔
272	this->parameters_.insert(symbolic::symbol(container));	194✔
273	}	194✔
274	}
275	}	193✔
276
277	void AssumptionsAnalysis::run(analysis::AnalysisManager& analysis_manager) {	193✔
278	this->assumptions_.clear();	193✔
279	this->parameters_.clear();	193✔
280
281	// Add sdfg assumptions
282	this->assumptions_.insert({&sdfg_.root(), symbolic::Assumptions()});	193✔
283
284	// Add additional assumptions
285	for (auto& entry : this->additional_assumptions_) {	193✔
286	this->assumptions_[&sdfg_.root()][entry.first] = entry.second;	×
287	}
288
289	this->scope_analysis_ = &analysis_manager.get<ScopeAnalysis>();	193✔
290	this->users_analysis_ = &analysis_manager.get<Users>();	193✔
291
292	// Determine parameters
293	this->determine_parameters(analysis_manager);	193✔
294
295	// Forward propagate for each node
296	this->traverse(sdfg_.root(), analysis_manager);	193✔
297	};	193✔
298
299	const symbolic::Assumptions AssumptionsAnalysis::
300	get(structured_control_flow::ControlFlowNode& node, bool include_trivial_bounds) {	781✔
301	// Compute assumptions on the fly
302
303	// Node-level assumptions
304	symbolic::Assumptions assums;	781✔
305	if (this->assumptions_.find(&node) != this->assumptions_.end()) {	781✔
306	for (auto& entry : this->assumptions_[&node]) {	714✔
307	assums.insert({entry.first, entry.second});	461✔
308	}
309	}	253✔
310
311	auto scope = scope_analysis_->parent_scope(&node);	781✔
312	while (scope != nullptr) {	3,493✔
313	if (this->assumptions_.find(scope) != this->assumptions_.end()) {	2,712✔
314	for (auto& entry : this->assumptions_[scope]) {	3,095✔
315	if (assums.find(entry.first) == assums.end()) {	1,486✔
316	// New assumption
317	assums.insert({entry.first, entry.second});	1,183✔
318	} else {	1,183✔
319	// Merge assumptions from lower scopes
320	auto& lower_assum = assums[entry.first];	303✔
321	auto lower_ub_deprecated = lower_assum.upper_bound_deprecated();	303✔
322	auto lower_lb_deprecated = lower_assum.lower_bound_deprecated();	303✔
323	auto new_ub_deprecated = symbolic::min(entry.second.upper_bound_deprecated(), lower_ub_deprecated);	303✔
324	auto new_lb_deprecated = symbolic::max(entry.second.lower_bound_deprecated(), lower_lb_deprecated);	303✔
325	lower_assum.upper_bound_deprecated(new_ub_deprecated);	303✔
326	lower_assum.lower_bound_deprecated(new_lb_deprecated);	303✔
327
328	for (auto ub : entry.second.upper_bounds()) {	802✔
329	lower_assum.add_upper_bound(ub);	499✔
330	}	499✔
331	for (auto lb : entry.second.lower_bounds()) {	987✔
332	lower_assum.add_lower_bound(lb);	684✔
333	}	684✔
334
335	auto lower_tight_ub = lower_assum.tight_upper_bound();	303✔
336	if (!entry.second.tight_upper_bound().is_null() && !lower_tight_ub.is_null()) {	303✔
NEW 337	auto new_tight_ub = symbolic::min(entry.second.tight_upper_bound(), lower_tight_ub);	×
NEW 338	lower_assum.tight_upper_bound(new_tight_ub);	×
NEW 339	}	×
340	auto lower_tight_lb = lower_assum.tight_lower_bound();	303✔
341	if (!entry.second.tight_lower_bound().is_null() && !lower_tight_lb.is_null()) {	303✔
NEW 342	auto new_tight_lb = symbolic::max(entry.second.tight_lower_bound(), lower_tight_lb);	×
NEW 343	lower_assum.tight_lower_bound(new_tight_lb);	×
NEW 344	}	×
345
346	if (lower_assum.map() == SymEngine::null) {	303✔
347	lower_assum.map(entry.second.map());	303✔
348	}	303✔
349	if (!lower_assum.constant()) {	303✔
350	lower_assum.constant(entry.second.constant());	22✔
351	}	22✔
352	}	303✔
353	}
354	}	1,609✔
355	scope = scope_analysis_->parent_scope(scope);	2,712✔
356	}
357
358	if (include_trivial_bounds) {	781✔
359	for (auto& entry : sdfg_.assumptions()) {	2,968✔
360	if (assums.find(entry.first) == assums.end()) {	2,366✔
361	assums.insert({entry.first, entry.second});	887✔
362	}	887✔
363	}
364	}	602✔
365
366	return assums;	781✔
367	};	781✔
368
369	const symbolic::Assumptions AssumptionsAnalysis::
370	get(structured_control_flow::ControlFlowNode& from,	228✔
371	structured_control_flow::ControlFlowNode& to,
372	bool include_trivial_bounds) {
373	auto assums_from = this->get(from, include_trivial_bounds);	228✔
374	auto assums_to = this->get(to, include_trivial_bounds);	228✔
375
376	// Add lower scope assumptions to outer
377	// ignore constants assumption
378	for (auto& entry : assums_from) {	1,212✔
379	if (assums_to.find(entry.first) == assums_to.end()) {	984✔
380	auto assums_safe = assums_to;	×
381	assums_safe.at(entry.first).constant(false);	×
382	assums_to.insert({entry.first, assums_safe.at(entry.first)});	×
383	} else {	×
384	auto lower_assum = assums_to[entry.first];	984✔
385	auto lower_ub_deprecated = lower_assum.upper_bound_deprecated();	984✔
386	auto lower_lb_deprecated = lower_assum.lower_bound_deprecated();	984✔
387	auto new_ub_deprecated = symbolic::min(entry.second.upper_bound_deprecated(), lower_ub_deprecated);	984✔
388	auto new_lb_deprecated = symbolic::max(entry.second.lower_bound_deprecated(), lower_lb_deprecated);	984✔
389	lower_assum.upper_bound_deprecated(new_ub_deprecated);	984✔
390	lower_assum.lower_bound_deprecated(new_lb_deprecated);	984✔
391
392	for (auto ub : entry.second.upper_bounds()) {	2,564✔
393	lower_assum.add_upper_bound(ub);	1,580✔
394	}	1,580✔
395	for (auto lb : entry.second.lower_bounds()) {	2,808✔
396	lower_assum.add_lower_bound(lb);	1,824✔
397	}	1,824✔
398
399	auto lower_tight_ub = lower_assum.tight_upper_bound();	984✔
400	if (!entry.second.tight_upper_bound().is_null() && !lower_tight_ub.is_null()) {	984✔
401	auto new_tight_ub = symbolic::min(entry.second.tight_upper_bound(), lower_tight_ub);	187✔
402	lower_assum.tight_upper_bound(new_tight_ub);	187✔
403	}	187✔
404	auto lower_tight_lb = lower_assum.tight_lower_bound();	984✔
405	if (!entry.second.tight_lower_bound().is_null() && !lower_tight_lb.is_null()) {	984✔
406	auto new_tight_lb = symbolic::max(entry.second.tight_lower_bound(), lower_tight_lb);	283✔
407	lower_assum.tight_lower_bound(new_tight_lb);	283✔
408	}	283✔
409
410	if (lower_assum.map() == SymEngine::null) {	984✔
411	lower_assum.map(entry.second.map());	456✔
412	}	456✔
413	lower_assum.constant(entry.second.constant());	984✔
414	assums_to[entry.first] = lower_assum;	984✔
415	}	984✔
416	}
417
418	return assums_to;	228✔
419	}	228✔
420
421	const symbolic::SymbolSet& AssumptionsAnalysis::parameters() { return this->parameters_; }	67✔
422
423	bool AssumptionsAnalysis::is_parameter(const symbolic::Symbol& container) {	160✔
424	return this->parameters_.contains(container);	160✔
425	}
426
427	bool AssumptionsAnalysis::is_parameter(const std::string& container) {	160✔
428	return this->is_parameter(symbolic::symbol(container));	160✔
NEW 429	}	×
430
431	void AssumptionsAnalysis::add(symbolic::Assumptions& assums, structured_control_flow::ControlFlowNode& node) {	×
432	if (this->assumptions_.find(&node) == this->assumptions_.end()) {	×
433	return;	×
434	}
435
436	for (auto& entry : this->assumptions_[&node]) {	×
437	if (assums.find(entry.first) == assums.end()) {	×
438	assums.insert({entry.first, entry.second});	×
439	} else {	×
440	assums[entry.first] = entry.second;	×
441	}
442	}
443	}	×
444
445	} // namespace analysis
446	} // namespace sdfg

daisytuner / sdfglib / 18715914051

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