• Home
  • Features
  • Pricing
  • Docs
  • Announcements
  • Sign In

daisytuner / sdfglib / 20306853140

17 Dec 2025 02:49PM UTC coverage: 40.001% (-0.09%) from 40.09%
20306853140

push

github

web-flow
Merge pull request #393 from daisytuner/assumptions-analysis-refactor

refactors assumptions analysis for better performance

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%)

21 existing lines in 7 files now uncovered.

11582 of 18962 relevant lines covered (61.08%)

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
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)) {
451✔
424
            if (user->use() == not_allowed) {
244!
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
STATUS · Troubleshooting · Open an Issue · Sales · Support · CAREERS · ENTERPRISE · START FREE · SCHEDULE DEMO
ANNOUNCEMENTS · TWITTER · TOS & SLA · Supported CI Services · What's a CI service? · Automated Testing

© 2026 Coveralls, Inc