20026333216

Committed 08 Dec 2025 11:19AM UTC coverage: 61.756% (+0.05%) from 61.708%

Build # 20026333216

Build Type

push

github

Committed by

web-flow

Commit Message

Merge pull request #381 from daisytuner/assumptions-constants

Sets constant assumptions for read-only symbols in loop bodies

Run Details

18 of 19 new or added lines in 2 files covered. (94.74%)

12 existing lines in 3 files now uncovered.

11399 of 18458 relevant lines covered (61.76%)

103.95 hits per line

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

89.66

/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];

    // Define all constant symbols

    // By definition, all symbols in the loop condition are constant within the loop body
    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);
    }

    // Collect other constant symbols based on uses
    UsersView users_view(*this->users_analysis_, body);
    std::unordered_set<std::string> visited;
    for (auto& read : users_view.reads()) {
        if (!sdfg_.exists(read->container())) {
            continue;
        }

        if (visited.find(read->container()) != visited.end()) {
            continue;
        }
        visited.insert(read->container());

        auto& type = this->sdfg_.type(read->container());
        if (!type.is_symbol() || type.type_id() != types::TypeID::Scalar) {
            continue;
        }

        if (users_view.reads(read->container()) != users_view.uses(read->container())) {
            continue;
        }

        if (body_assumptions.find(symbolic::symbol(read->container())) == body_assumptions.end()) {
            symbolic::Symbol sym = symbolic::symbol(read->container());
            body_assumptions.insert({sym, symbolic::Assumption(sym)});
            body_assumptions[sym].constant(true);
        }
    }

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

daisytuner / sdfglib / 20026333216

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