20305765315

Committed 17 Dec 2025 02:13PM UTC coverage: 39.998% (-0.09%) from 40.09%

Build # 20305765315

Build Type

Pull #393

github

Committed by

web-flow

Commit Message

Merge b2467688c into cb779d466

Pull Request Pull Request #393: refactors assumptions analysis for better performance

Run Details

13423 of 43549 branches covered (30.82%)

Branch coverage included in aggregate %.

181 of 193 new or added lines in 2 files covered. (93.78%)

23 existing lines in 8 files now uncovered.

11580 of 18962 relevant lines covered (61.07%)

86.87 hits per line

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

61.49

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

daisytuner / sdfglib / 20305765315

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