20764569418

Committed 06 Jan 2026 10:50PM UTC coverage: 62.168% (+21.4%) from 40.764%

Build # 20764569418

Build Type

push

github

Committed by

web-flow

Commit Message

Merge pull request #433 from daisytuner/clang-coverage

updates clang coverage flags

Run Details

14988 of 24109 relevant lines covered (62.17%)

88.57 hits per line

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

90.85

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

daisytuner / sdfglib / 20764569418

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