19406662809

Committed 16 Nov 2025 01:54PM UTC coverage: 62.092% (-0.4%) from 62.447%

Build # 19406662809

Build Type

push

github

Committed by

web-flow

Commit Message

Merge pull request #347 from daisytuner/symbolic-range-analysis

extends symbol promotion with checks for effective range of scalars

Run Details

174 of 355 new or added lines in 10 files covered. (49.01%)

13 existing lines in 4 files now uncovered.

11048 of 17793 relevant lines covered (62.09%)

112.56 hits per line

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

90.07

/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::sub(symbolic::subs(inverse, indvar, num_elements), symbolic::one()));
                }
            }
        }
    }
    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].add_lower_bound(init);
    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);
        }
    }

    symbolic::CNF cnf;
    try {
        cnf = symbolic::conjunctive_normal_form(loop->condition());
    } catch (const symbolic::CNFException& e) {
        return;
    }
    auto ub = cnf_to_upper_bound(cnf, indvar);
    if (ub.is_null()) {
        return;
    }
    // Assumption: upper bound ub is tight for indvar if
    body_assumptions[indvar].add_upper_bound(ub);
    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()));
    }
}

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()) {
            scope = scope_analysis_->parent_scope(scope);
            continue;
        }
        for (auto& entry : this->assumptions_[scope]) {
            if (assums.find(entry.first) == assums.end()) {
                // New assumption
                assums.insert({entry.first, entry.second});
                continue;
            }

            // Merge assumptions from lower scopes
            auto& lower_assum = assums[entry.first];

            // Deprecated: combine with min
            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);

            // Add to set of bounds
            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);
            }

            // Set tight bounds
            if (lower_assum.tight_upper_bound().is_null()) {
                lower_assum.tight_upper_bound(entry.second.tight_upper_bound());
            }
            if (lower_assum.tight_lower_bound().is_null()) {
                lower_assum.tight_lower_bound(entry.second.tight_lower_bound());
            }

            // Set map
            if (lower_assum.map().is_null()) {
                lower_assum.map(entry.second.map());
            }

            // Set constant
            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});
            } else {
                for (auto& lb : entry.second.lower_bounds()) {
                    assums.at(entry.first).add_lower_bound(lb);
                }
                for (auto& ub : entry.second.upper_bounds()) {
                    assums.at(entry.first).add_upper_bound(ub);
                }
            }
        }
    }

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

daisytuner / sdfglib / 19406662809

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