24046746427

Committed 06 Apr 2026 07:15PM UTC coverage: 64.771% (-0.2%) from 64.968%

Build # 24046746427

Build Type

Pull #649

github

Committed by

web-flow

Commit Message

Merge 300f78442 into e031e338e

Pull Request Pull Request #649: removes polly scheduler

Coverage Stats

28641 of 44219 relevant lines covered (64.77%)

625.62 hits per line

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

93.31

/sdfg/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/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::run(analysis::AnalysisManager& analysis_manager) {
    this->assumptions_.clear();
    this->assumptions_with_trivial_.clear();
    this->ref_assumptions_.clear();
    this->ref_assumptions_with_trivial_.clear();

    this->parameters_.clear();
    this->users_analysis_ = &analysis_manager.get<Users>();

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

    // Initialize root assumptions with SDFG-level assumptions
    this->assumptions_.insert({&sdfg_.root(), this->additional_assumptions_});
    auto& initial = this->assumptions_[&sdfg_.root()];

    this->assumptions_with_trivial_.insert({&sdfg_.root(), initial});
    auto& initial_with_trivial = this->assumptions_with_trivial_[&sdfg_.root()];
    for (auto& entry : sdfg_.assumptions()) {
        if (initial_with_trivial.find(entry.first) == initial_with_trivial.end()) {
            initial_with_trivial.insert({entry.first, entry.second});
        } else {
            for (auto& lb : entry.second.lower_bounds()) {
                initial_with_trivial.at(entry.first).add_lower_bound(lb);
            }
            for (auto& ub : entry.second.upper_bounds()) {
                initial_with_trivial.at(entry.first).add_upper_bound(ub);
            }
        }
    }

    // Traverse and propagate
    this->traverse(sdfg_.root(), initial, initial_with_trivial);
};

void AssumptionsAnalysis::traverse(
    structured_control_flow::ControlFlowNode& current,
    const symbolic::Assumptions& outer_assumptions,
    const symbolic::Assumptions& outer_assumptions_with_trivial
) {
    this->propagate_ref(current, outer_assumptions, outer_assumptions_with_trivial);

    if (auto sequence_stmt = dynamic_cast<structured_control_flow::Sequence*>(&current)) {
        for (size_t i = 0; i < sequence_stmt->size(); i++) {
            this->traverse(sequence_stmt->at(i).first, outer_assumptions, outer_assumptions_with_trivial);
        }
    } else if (auto if_else_stmt = dynamic_cast<structured_control_flow::IfElse*>(&current)) {
        for (size_t i = 0; i < if_else_stmt->size(); i++) {
            this->traverse(if_else_stmt->at(i).first, outer_assumptions, outer_assumptions_with_trivial);
        }
    } else if (auto while_stmt = dynamic_cast<structured_control_flow::While*>(&current)) {
        this->traverse(while_stmt->root(), outer_assumptions, outer_assumptions_with_trivial);
    } else if (auto loop_stmt = dynamic_cast<structured_control_flow::StructuredLoop*>(&current)) {
        this->traverse_structured_loop(loop_stmt, outer_assumptions, outer_assumptions_with_trivial);
    } else {
        // Other control flow nodes (e.g., Block) do not introduce assumptions or comprise scopes
    }
};

void AssumptionsAnalysis::traverse_structured_loop(
    structured_control_flow::StructuredLoop* loop,
    const symbolic::Assumptions& outer_assumptions,
    const symbolic::Assumptions& outer_assumptions_with_trivial
) {
    // A structured loop induces assumption for the loop body
    auto& body = loop->root();
    symbolic::Assumptions body_assumptions;

    // Define all constant symbols
    auto indvar = loop->indvar();
    auto update = loop->update();
    auto init = loop->init();

    // By definition, all symbols in the loop condition are constant within the loop body
    symbolic::SymbolSet loop_syms = symbolic::atoms(loop->condition());
    for (auto& sym : loop_syms) {
        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);
    body_assumptions[indvar].constant(true);

    // 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
    if (!loop->is_monotonic()) {
        this->propagate(body, body_assumptions, outer_assumptions, outer_assumptions_with_trivial);
        this->traverse(body, this->assumptions_[&body], this->assumptions_with_trivial_[&body]);
        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) {
        this->propagate(body, body_assumptions, outer_assumptions, outer_assumptions_with_trivial);
        this->traverse(body, this->assumptions_[&body], this->assumptions_with_trivial_[&body]);
        return;
    }
    auto ub = cnf_to_upper_bound(cnf, indvar);
    if (ub.is_null()) {
        this->propagate(body, body_assumptions, outer_assumptions, outer_assumptions_with_trivial);
        this->traverse(body, this->assumptions_[&body], this->assumptions_with_trivial_[&body]);
        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 (loop->is_contiguous()) {
        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()));
    }

    this->propagate(body, body_assumptions, outer_assumptions, outer_assumptions_with_trivial);
    this->traverse(body, this->assumptions_[&body], this->assumptions_with_trivial_[&body]);
}

void AssumptionsAnalysis::propagate(
    structured_control_flow::ControlFlowNode& node,
    const symbolic::Assumptions& node_assumptions,
    const symbolic::Assumptions& outer_assumptions,
    const symbolic::Assumptions& outer_assumptions_with_trivial
) {
    // Propagate assumptions
    this->assumptions_.insert({&node, node_assumptions});
    auto& propagated_assumptions = this->assumptions_[&node];
    for (auto& entry : outer_assumptions) {
        if (propagated_assumptions.find(entry.first) == propagated_assumptions.end()) {
            // New assumption
            propagated_assumptions.insert({entry.first, entry.second});
            continue;
        }

        // Merge assumptions from lower scopes
        auto& lower_assum = propagated_assumptions[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());
        }
    }

    this->assumptions_with_trivial_.insert({&node, node_assumptions});
    auto& assumptions_with_trivial = this->assumptions_with_trivial_[&node];
    for (auto& entry : outer_assumptions_with_trivial) {
        if (assumptions_with_trivial.find(entry.first) == assumptions_with_trivial.end()) {
            // New assumption
            assumptions_with_trivial.insert({entry.first, entry.second});
            continue;
        }
        // Merge assumptions from lower scopes
        auto& lower_assum = assumptions_with_trivial[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());
        }
    }
}

void AssumptionsAnalysis::propagate_ref(
    structured_control_flow::ControlFlowNode& node,
    const symbolic::Assumptions& outer_assumptions,
    const symbolic::Assumptions& outer_assumptions_with_trivial
) {
    this->ref_assumptions_.insert({&node, &outer_assumptions});
    this->ref_assumptions_with_trivial_.insert({&node, &outer_assumptions_with_trivial});
}

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:
            case types::TypeID::Tensor:
                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));
        }
    }
}

const symbolic::Assumptions& AssumptionsAnalysis::
    get(structured_control_flow::ControlFlowNode& node, bool include_trivial_bounds) {
    if (include_trivial_bounds) {
        return *this->ref_assumptions_with_trivial_[&node];
    } else {
        return *this->ref_assumptions_[&node];
    }
}

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

} // 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/symbolic.h"
14	#include "sdfg/types/type.h"
15
16	namespace sdfg {
17	namespace analysis {
18
19	symbolic::Expression AssumptionsAnalysis::cnf_to_upper_bound(const symbolic::CNF& cnf, const symbolic::Symbol indvar) {	891✔
20	std::vector<symbolic::Expression> candidates;	891✔
21
22	for (const auto& clause : cnf) {	984✔
23	for (const auto& literal : clause) {	984✔
24	// Comparison: indvar < expr
25	if (SymEngine::is_a<SymEngine::StrictLessThan>(*literal)) {	984✔
26	auto lt = SymEngine::rcp_static_cast<const SymEngine::StrictLessThan>(literal);	958✔
27	if (symbolic::eq(lt->get_arg1(), indvar) && !symbolic::uses(lt->get_arg2(), indvar)) {	958✔
28	auto ub = symbolic::sub(lt->get_arg2(), symbolic::one());	944✔
29	candidates.push_back(ub);	944✔
30	}	944✔
31	}	958✔
32	// Comparison: indvar <= expr
33	else if (SymEngine::is_a<SymEngine::LessThan>(*literal)) {	26✔
34	auto le = SymEngine::rcp_static_cast<const SymEngine::LessThan>(literal);	25✔
35	if (symbolic::eq(le->get_arg1(), indvar) && !symbolic::uses(le->get_arg2(), indvar)) {	25✔
36	candidates.push_back(le->get_arg2());	24✔
37	}	24✔
38	}	25✔
39	// Comparison: indvar == expr
40	else if (SymEngine::is_a<SymEngine::Equality>(*literal)) {	1✔
41	auto eq = SymEngine::rcp_static_cast<const SymEngine::Equality>(literal);	×
42	if (symbolic::eq(eq->get_arg1(), indvar) && !symbolic::uses(eq->get_arg2(), indvar)) {	×
43	candidates.push_back(eq->get_arg2());	×
44	}	×
45	}	×
46	}	984✔
47	}	984✔
48
49	if (candidates.empty()) {	891✔
50	return SymEngine::null;	12✔
51	}	12✔
52
53	// Return the smallest upper bound across all candidate constraints
54	symbolic::Expression result = candidates[0];	879✔
55	for (size_t i = 1; i < candidates.size(); ++i) {	968✔
56	result = symbolic::min(result, candidates[i]);	89✔
57	}	89✔
58
59	return result;	879✔
60	}	891✔
61
62	AssumptionsAnalysis::AssumptionsAnalysis(StructuredSDFG& sdfg)
63	: Analysis(sdfg) {	297✔
64
65	};	297✔
66
67	void AssumptionsAnalysis::run(analysis::AnalysisManager& analysis_manager) {	297✔
68	this->assumptions_.clear();	297✔
69	this->assumptions_with_trivial_.clear();	297✔
70	this->ref_assumptions_.clear();	297✔
71	this->ref_assumptions_with_trivial_.clear();	297✔
72
73	this->parameters_.clear();	297✔
74	this->users_analysis_ = &analysis_manager.get<Users>();	297✔
75
76	// Determine parameters
77	this->determine_parameters(analysis_manager);	297✔
78
79	// Initialize root assumptions with SDFG-level assumptions
80	this->assumptions_.insert({&sdfg_.root(), this->additional_assumptions_});	297✔
81	auto& initial = this->assumptions_[&sdfg_.root()];	297✔
82
83	this->assumptions_with_trivial_.insert({&sdfg_.root(), initial});	297✔
84	auto& initial_with_trivial = this->assumptions_with_trivial_[&sdfg_.root()];	297✔
85	for (auto& entry : sdfg_.assumptions()) {	1,822✔
86	if (initial_with_trivial.find(entry.first) == initial_with_trivial.end()) {	1,822✔
87	initial_with_trivial.insert({entry.first, entry.second});	1,822✔
88	} else {	1,822✔
89	for (auto& lb : entry.second.lower_bounds()) {	×
90	initial_with_trivial.at(entry.first).add_lower_bound(lb);	×
91	}	×
92	for (auto& ub : entry.second.upper_bounds()) {	×
93	initial_with_trivial.at(entry.first).add_upper_bound(ub);	×
94	}	×
95	}	×
96	}	1,822✔
97
98	// Traverse and propagate
99	this->traverse(sdfg_.root(), initial, initial_with_trivial);	297✔
100	};	297✔
101
102	void AssumptionsAnalysis::traverse(
103	structured_control_flow::ControlFlowNode& current,
104	const symbolic::Assumptions& outer_assumptions,
105	const symbolic::Assumptions& outer_assumptions_with_trivial
106	) {	2,927✔
107	this->propagate_ref(current, outer_assumptions, outer_assumptions_with_trivial);	2,927✔
108
109	if (auto sequence_stmt = dynamic_cast<structured_control_flow::Sequence*>(&current)) {	2,927✔
110	for (size_t i = 0; i < sequence_stmt->size(); i++) {	2,928✔
111	this->traverse(sequence_stmt->at(i).first, outer_assumptions, outer_assumptions_with_trivial);	1,704✔
112	}	1,704✔
113	} else if (auto if_else_stmt = dynamic_cast<structured_control_flow::IfElse*>(&current)) {	1,703✔
114	for (size_t i = 0; i < if_else_stmt->size(); i++) {	19✔
115	this->traverse(if_else_stmt->at(i).first, outer_assumptions, outer_assumptions_with_trivial);	12✔
116	}	12✔
117	} else if (auto while_stmt = dynamic_cast<structured_control_flow::While*>(&current)) {	1,696✔
118	this->traverse(while_stmt->root(), outer_assumptions, outer_assumptions_with_trivial);	22✔
119	} else if (auto loop_stmt = dynamic_cast<structured_control_flow::StructuredLoop*>(&current)) {	1,674✔
120	this->traverse_structured_loop(loop_stmt, outer_assumptions, outer_assumptions_with_trivial);	892✔
121	} else {	892✔
122	// Other control flow nodes (e.g., Block) do not introduce assumptions or comprise scopes
123	}	782✔
124	};	2,927✔
125
126	void AssumptionsAnalysis::traverse_structured_loop(
127	structured_control_flow::StructuredLoop* loop,
128	const symbolic::Assumptions& outer_assumptions,
129	const symbolic::Assumptions& outer_assumptions_with_trivial
130	) {	892✔
131	// A structured loop induces assumption for the loop body
132	auto& body = loop->root();	892✔
133	symbolic::Assumptions body_assumptions;	892✔
134
135	// Define all constant symbols
136	auto indvar = loop->indvar();	892✔
137	auto update = loop->update();	892✔
138	auto init = loop->init();	892✔
139
140	// By definition, all symbols in the loop condition are constant within the loop body
141	symbolic::SymbolSet loop_syms = symbolic::atoms(loop->condition());	892✔
142	for (auto& sym : loop_syms) {	1,894✔
143	body_assumptions.insert({sym, symbolic::Assumption(sym)});	1,894✔
144	body_assumptions[sym].constant(true);	1,894✔
145	}	1,894✔
146
147	// Collect other constant symbols based on uses
148	UsersView users_view(*this->users_analysis_, body);	892✔
149	std::unordered_set<std::string> visited;	892✔
150	for (auto& read : users_view.reads()) {	12,561✔
151	if (!sdfg_.exists(read->container())) {	12,561✔
152	continue;	×
153	}	×
154	if (visited.find(read->container()) != visited.end()) {	12,561✔
155	continue;	7,248✔
156	}	7,248✔
157	visited.insert(read->container());	5,313✔
158
159	auto& type = this->sdfg_.type(read->container());	5,313✔
160	if (!type.is_symbol() \|\| type.type_id() != types::TypeID::Scalar) {	5,313✔
161	continue;	2,335✔
162	}	2,335✔
163
164	if (users_view.reads(read->container()) != users_view.uses(read->container())) {	2,978✔
165	continue;	925✔
166	}	925✔
167
168	if (body_assumptions.find(symbolic::symbol(read->container())) == body_assumptions.end()) {	2,053✔
169	symbolic::Symbol sym = symbolic::symbol(read->container());	940✔
170	body_assumptions.insert({sym, symbolic::Assumption(sym)});	940✔
171	body_assumptions[sym].constant(true);	940✔
172	}	940✔
173	}	2,053✔
174
175	// Define map of indvar
176	body_assumptions[indvar].map(update);	892✔
177	body_assumptions[indvar].constant(true);	892✔
178
179	// Determine non-tight lower and upper bounds from inverse index access
180	std::vector<symbolic::Expression> lbs, ubs;	892✔
181	for (auto user : this->users_analysis_->reads(indvar->get_name())) {	4,447✔
182	if (auto* memlet = dynamic_cast<data_flow::Memlet*>(user->element())) {	4,447✔
183	const types::IType* memlet_type = &memlet->base_type();	2,289✔
184	for (long long i = memlet->subset().size() - 1; i >= 0; i--) {	6,257✔
185	symbolic::Expression num_elements = SymEngine::null;	3,980✔
186	if (auto* pointer_type = dynamic_cast<const types::Pointer*>(memlet_type)) {	3,980✔
187	memlet_type = &pointer_type->pointee_type();	1,729✔
188	} else if (auto* array_type = dynamic_cast<const types::Array*>(memlet_type)) {	2,251✔
189	memlet_type = &array_type->element_type();	2,239✔
190	num_elements = array_type->num_elements();	2,239✔
191	} else {	2,239✔
192	break;	12✔
193	}	12✔
194	if (!symbolic::uses(memlet->subset().at(i), indvar)) {	3,968✔
195	continue;	1,658✔
196	}	1,658✔
197	symbolic::Expression inverse = symbolic::inverse(memlet->subset().at(i), indvar);	2,310✔
198	if (inverse.is_null()) {	2,310✔
199	continue;	9✔
200	}	9✔
201	lbs.push_back(symbolic::subs(inverse, indvar, symbolic::zero()));	2,301✔
202	if (num_elements.is_null()) {	2,301✔
203	std::string container;	953✔
204	if (memlet->src_conn() == "void") {	953✔
205	container = dynamic_cast<data_flow::AccessNode&>(memlet->src()).data();	618✔
206	} else {	618✔
207	container = dynamic_cast<data_flow::AccessNode&>(memlet->dst()).data();	335✔
208	}	335✔
209	if (this->is_parameter(container)) {	953✔
210	ubs.push_back(symbolic::sub(	899✔
211	symbolic::subs(inverse, indvar, symbolic::dynamic_sizeof(symbolic::symbol(container))),	899✔
212	symbolic::one()	899✔
213	));	899✔
214	}	899✔
215	} else {	1,348✔
216	ubs.push_back(symbolic::sub(symbolic::subs(inverse, indvar, num_elements), symbolic::one()));	1,348✔
217	}	1,348✔
218	}	2,301✔
219	}	2,289✔
220	}	4,447✔
221	for (auto lb : lbs) {	2,301✔
222	body_assumptions[indvar].add_lower_bound(lb);	2,301✔
223	}	2,301✔
224	for (auto ub : ubs) {	2,247✔
225	body_assumptions[indvar].add_upper_bound(ub);	2,247✔
226	}	2,247✔
227
228	// Prove that update is monotonic -> assume bounds
229	if (!loop->is_monotonic()) {	892✔
230	this->propagate(body, body_assumptions, outer_assumptions, outer_assumptions_with_trivial);	1✔
231	this->traverse(body, this->assumptions_[&body], this->assumptions_with_trivial_[&body]);	1✔
232	return;	1✔
233	}	1✔
234
235	// Assumption: init is tight lower bound for indvar
236	body_assumptions[indvar].add_lower_bound(init);	891✔
237	body_assumptions[indvar].tight_lower_bound(init);	891✔
238	body_assumptions[indvar].lower_bound_deprecated(init);	891✔
239
240	// Assumption: inverse index access lower bounds are lower bound for init
241	if (SymEngine::is_a<SymEngine::Symbol>(*init) && !lbs.empty()) {	891✔
242	auto sym = SymEngine::rcp_static_cast<const SymEngine::Symbol>(init);	79✔
243	if (!body_assumptions.contains(sym)) {	79✔
244	body_assumptions.insert({sym, symbolic::Assumption(sym)});	1✔
245	}	1✔
246	for (auto lb : lbs) {	257✔
247	body_assumptions[sym].add_lower_bound(lb);	257✔
248	}	257✔
249	}	79✔
250
251	symbolic::CNF cnf;	891✔
252	try {	891✔
253	cnf = symbolic::conjunctive_normal_form(loop->condition());	891✔
254	} catch (const symbolic::CNFException& e) {	891✔
255	this->propagate(body, body_assumptions, outer_assumptions, outer_assumptions_with_trivial);	×
256	this->traverse(body, this->assumptions_[&body], this->assumptions_with_trivial_[&body]);	×
257	return;	×
258	}	×
259	auto ub = cnf_to_upper_bound(cnf, indvar);	891✔
260	if (ub.is_null()) {	891✔
261	this->propagate(body, body_assumptions, outer_assumptions, outer_assumptions_with_trivial);	12✔
262	this->traverse(body, this->assumptions_[&body], this->assumptions_with_trivial_[&body]);	12✔
263	return;	12✔
264	}	12✔
265	// Assumption: upper bound ub is tight for indvar if
266	body_assumptions[indvar].add_upper_bound(ub);	879✔
267	body_assumptions[indvar].upper_bound_deprecated(ub);	879✔
268	// TODO: handle non-contiguous tight upper bounds with modulo
269	// Example: for (i = 0; i < n; i += 3) -> tight_upper_bound = (n - 1) - ((n - 1) % 3)
270	if (loop->is_contiguous()) {	879✔
271	body_assumptions[indvar].tight_upper_bound(ub);	800✔
272	}	800✔
273
274	// Assumption: inverse index access upper bounds are upper bound for ub
275	if (SymEngine::is_a<SymEngine::Symbol>(*ub) && !ubs.empty()) {	879✔
276	auto sym = SymEngine::rcp_static_cast<const SymEngine::Symbol>(ub);	20✔
277	if (!body_assumptions.contains(sym)) {	20✔
278	body_assumptions.insert({sym, symbolic::Assumption(sym)});	×
279	}	×
280	for (auto ub : ubs) {	56✔
281	body_assumptions[sym].add_upper_bound(ub);	56✔
282	}	56✔
283	}	20✔
284
285	// Assumption: any ub symbol is at least init
286	for (auto& sym : symbolic::atoms(ub)) {	977✔
287	body_assumptions[sym].add_lower_bound(symbolic::add(init, symbolic::one()));	977✔
288	body_assumptions[sym].lower_bound_deprecated(symbolic::add(init, symbolic::one()));	977✔
289	}	977✔
290
291	this->propagate(body, body_assumptions, outer_assumptions, outer_assumptions_with_trivial);	879✔
292	this->traverse(body, this->assumptions_[&body], this->assumptions_with_trivial_[&body]);	879✔
293	}	879✔
294
295	void AssumptionsAnalysis::propagate(
296	structured_control_flow::ControlFlowNode& node,
297	const symbolic::Assumptions& node_assumptions,
298	const symbolic::Assumptions& outer_assumptions,
299	const symbolic::Assumptions& outer_assumptions_with_trivial
300	) {	892✔
301	// Propagate assumptions
302	this->assumptions_.insert({&node, node_assumptions});	892✔
303	auto& propagated_assumptions = this->assumptions_[&node];	892✔
304	for (auto& entry : outer_assumptions) {	2,146✔
305	if (propagated_assumptions.find(entry.first) == propagated_assumptions.end()) {	2,146✔
306	// New assumption
307	propagated_assumptions.insert({entry.first, entry.second});	757✔
308	continue;	757✔
309	}	757✔
310
311	// Merge assumptions from lower scopes
312	auto& lower_assum = propagated_assumptions[entry.first];	1,389✔
313
314	// Deprecated: combine with min
315	auto lower_ub_deprecated = lower_assum.upper_bound_deprecated();	1,389✔
316	auto lower_lb_deprecated = lower_assum.lower_bound_deprecated();	1,389✔
317	auto new_ub_deprecated = symbolic::min(entry.second.upper_bound_deprecated(), lower_ub_deprecated);	1,389✔
318	auto new_lb_deprecated = symbolic::max(entry.second.lower_bound_deprecated(), lower_lb_deprecated);	1,389✔
319	lower_assum.upper_bound_deprecated(new_ub_deprecated);	1,389✔
320	lower_assum.lower_bound_deprecated(new_lb_deprecated);	1,389✔
321
322	// Add to set of bounds
323	for (auto ub : entry.second.upper_bounds()) {	1,430✔
324	lower_assum.add_upper_bound(ub);	1,430✔
325	}	1,430✔
326	for (auto lb : entry.second.lower_bounds()) {	1,389✔
327	lower_assum.add_lower_bound(lb);	1,302✔
328	}	1,302✔
329
330	// Set tight bounds
331	if (lower_assum.tight_upper_bound().is_null()) {	1,389✔
332	lower_assum.tight_upper_bound(entry.second.tight_upper_bound());	1,379✔
333	}	1,379✔
334	if (lower_assum.tight_lower_bound().is_null()) {	1,389✔
335	lower_assum.tight_lower_bound(entry.second.tight_lower_bound());	1,379✔
336	}	1,379✔
337
338	// Set map
339	if (lower_assum.map().is_null()) {	1,389✔
340	lower_assum.map(entry.second.map());	1,379✔
341	}	1,379✔
342
343	// Set constant
344	if (!lower_assum.constant()) {	1,389✔
345	lower_assum.constant(entry.second.constant());	×
346	}	×
347	}	1,389✔
348
349	this->assumptions_with_trivial_.insert({&node, node_assumptions});	892✔
350	auto& assumptions_with_trivial = this->assumptions_with_trivial_[&node];	892✔
351	for (auto& entry : outer_assumptions_with_trivial) {	7,577✔
352	if (assumptions_with_trivial.find(entry.first) == assumptions_with_trivial.end()) {	7,577✔
353	// New assumption
354	assumptions_with_trivial.insert({entry.first, entry.second});	4,742✔
355	continue;	4,742✔
356	}	4,742✔
357	// Merge assumptions from lower scopes
358	auto& lower_assum = assumptions_with_trivial[entry.first];	2,835✔
359
360	// Deprecated: combine with min
361	auto lower_ub_deprecated = lower_assum.upper_bound_deprecated();	2,835✔
362	auto lower_lb_deprecated = lower_assum.lower_bound_deprecated();	2,835✔
363	auto new_ub_deprecated = symbolic::min(entry.second.upper_bound_deprecated(), lower_ub_deprecated);	2,835✔
364	auto new_lb_deprecated = symbolic::max(entry.second.lower_bound_deprecated(), lower_lb_deprecated);	2,835✔
365	lower_assum.upper_bound_deprecated(new_ub_deprecated);	2,835✔
366	lower_assum.lower_bound_deprecated(new_lb_deprecated);	2,835✔
367
368	// Add to set of bounds
369	for (auto ub : entry.second.upper_bounds()) {	4,265✔
370	lower_assum.add_upper_bound(ub);	4,265✔
371	}	4,265✔
372	for (auto lb : entry.second.lower_bounds()) {	3,494✔
373	lower_assum.add_lower_bound(lb);	3,494✔
374	}	3,494✔
375
376	// Set tight bounds
377	if (lower_assum.tight_upper_bound().is_null()) {	2,835✔
378	lower_assum.tight_upper_bound(entry.second.tight_upper_bound());	2,035✔
379	}	2,035✔
380	if (lower_assum.tight_lower_bound().is_null()) {	2,835✔
381	lower_assum.tight_lower_bound(entry.second.tight_lower_bound());	1,944✔
382	}	1,944✔
383
384	// Set map
385	if (lower_assum.map().is_null()) {	2,835✔
386	lower_assum.map(entry.second.map());	1,943✔
387	}	1,943✔
388
389	// Set constant
390	if (!lower_assum.constant()) {	2,835✔
391	lower_assum.constant(entry.second.constant());	1✔
392	}	1✔
393	}	2,835✔
394	}	892✔
395
396	void AssumptionsAnalysis::propagate_ref(
397	structured_control_flow::ControlFlowNode& node,
398	const symbolic::Assumptions& outer_assumptions,
399	const symbolic::Assumptions& outer_assumptions_with_trivial
400	) {	2,927✔
401	this->ref_assumptions_.insert({&node, &outer_assumptions});	2,927✔
402	this->ref_assumptions_with_trivial_.insert({&node, &outer_assumptions_with_trivial});	2,927✔
403	}	2,927✔
404
405	void AssumptionsAnalysis::determine_parameters(analysis::AnalysisManager& analysis_manager) {	297✔
406	for (auto& container : this->sdfg_.arguments()) {	1,112✔
407	bool readonly = true;	1,112✔
408	Use not_allowed;	1,112✔
409	switch (this->sdfg_.type(container).type_id()) {	1,112✔
410	case types::TypeID::Scalar:	522✔
411	not_allowed = Use::WRITE;	522✔
412	break;	522✔
413	case types::TypeID::Pointer:	364✔
414	not_allowed = Use::MOVE;	364✔
415	break;	364✔
416	case types::TypeID::Array:	225✔
417	case types::TypeID::Structure:	225✔
418	case types::TypeID::Reference:	226✔
419	case types::TypeID::Function:	226✔
420	case types::TypeID::Tensor:	226✔
421	continue;	226✔
422	}	1,112✔
423	for (auto user : this->users_analysis_->uses(container)) {	1,754✔
424	if (user->use() == not_allowed) {	1,754✔
425	readonly = false;	3✔
426	break;	3✔
427	}	3✔
428	}	1,754✔
429	if (readonly) {	886✔
430	this->parameters_.insert(symbolic::symbol(container));	883✔
431	}	883✔
432	}	886✔
433	}	297✔
434
435	const symbolic::Assumptions& AssumptionsAnalysis::
436	get(structured_control_flow::ControlFlowNode& node, bool include_trivial_bounds) {	7,190✔
437	if (include_trivial_bounds) {	7,190✔
438	return *this->ref_assumptions_with_trivial_[&node];	6,709✔
439	} else {	6,709✔
440	return *this->ref_assumptions_[&node];	481✔
441	}	481✔
442	}	7,190✔
443
444	const symbolic::SymbolSet& AssumptionsAnalysis::parameters() { return this->parameters_; }	9✔
445
446	bool AssumptionsAnalysis::is_parameter(const symbolic::Symbol& container) {	975✔
447	return this->parameters_.contains(container);	975✔
448	}	975✔
449
450	bool AssumptionsAnalysis::is_parameter(const std::string& container) {	975✔
451	return this->is_parameter(symbolic::symbol(container));	975✔
452	}	975✔
453
454	} // namespace analysis
455	} // namespace sdfg

daisytuner / docc / 24046746427

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