20261708173

Committed 16 Dec 2025 08:41AM UTC coverage: 40.086% (-0.2%) from 40.251%

Build # 20261708173

Build Type

Pull #392

github

Committed by

web-flow

Commit Message

Merge d12f829bf into e5e8aa90d

Pull Request Pull Request #392: refactors passes to improve performance

Run Details

13621 of 43972 branches covered (30.98%)

Branch coverage included in aggregate %.

129 of 178 new or added lines in 15 files covered. (72.47%)

55 existing lines in 8 files now uncovered.

11633 of 19027 relevant lines covered (61.14%)

90.79 hits per line

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

60.46

/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();
    this->cache_nodes_.clear();
    this->cache_nodes_bounds_.clear();
    this->cache_range_.clear();
    this->cache_range_bounds_.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) {
    if (include_trivial_bounds) {
        std::string key = std::to_string(node.element_id());
        if (this->cache_nodes_.find(key) != this->cache_nodes_.end()) {
            return this->cache_nodes_[key];
        }
    } else {
        std::string key = std::to_string(node.element_id());
        if (this->cache_nodes_bounds_.find(key) != this->cache_nodes_bounds_.end()) {
            return this->cache_nodes_bounds_[key];
        }
    }

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

    if (include_trivial_bounds) {
        std::string key = std::to_string(node.element_id());
        this->cache_nodes_.insert({key, assums});
        return this->cache_nodes_[key];
    } else {
        std::string key = std::to_string(node.element_id());
        this->cache_nodes_bounds_.insert({key, assums});
        return this->cache_nodes_bounds_[key];
    }
};

const symbolic::Assumptions& AssumptionsAnalysis::
    get(structured_control_flow::ControlFlowNode& from,
        structured_control_flow::ControlFlowNode& to,
        bool include_trivial_bounds) {
    if (include_trivial_bounds) {
        std::string key = std::to_string(from.element_id()) + "." + std::to_string(to.element_id());
        if (this->cache_range_.find(key) != this->cache_range_.end()) {
            return this->cache_range_[key];
        }
    } else {
        std::string key = std::to_string(from.element_id()) + "." + std::to_string(to.element_id());
        if (this->cache_range_bounds_.find(key) != this->cache_range_bounds_.end()) {
            return this->cache_range_bounds_[key];
        }
    }

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

    if (include_trivial_bounds) {
        std::string key = std::to_string(from.element_id()) + "." + std::to_string(to.element_id());
        this->cache_range_.insert({key, assums_to});
        return this->cache_range_[key];
    } else {
        std::string key = std::to_string(from.element_id()) + "." + std::to_string(to.element_id());
        this->cache_range_bounds_.insert({key, assums_to});
        return this->cache_range_bounds_[key];
    }
}

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

daisytuner / sdfglib / 20261708173

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