onnx_runtime_shape_inference/dim_expr.rs
1//! Symbolic dimension arithmetic: [`DimExpr`].
2//!
3//! `onnx-runtime-ir`'s [`Dim`](onnx_runtime_ir::Dim) can only represent a
4//! concrete extent ([`Dim::Static`](onnx_runtime_ir::Dim::Static)) or an opaque
5//! symbol ([`Dim::Symbolic`](onnx_runtime_ir::Dim::Symbolic)). Shape inference
6//! for reshape / conv / pool / flatten needs *derived* dimensions such as
7//! `d0 * d1`, `d0 + k`, or `d0 / k`. We do **not** modify the frozen IR
8//! contract; instead this crate reasons over dimensions using a small canonical
9//! integer polynomial and only *lowers* back to an IR [`Dim`] when writing an
10//! inferred shape into the graph (see [`crate::context::SymbolInterner`]).
11//!
12//! # Representation
13//!
14//! A [`DimExpr`] is a multivariate polynomial with integer coefficients over
15//! the graph's [`SymbolId`]s: a sum of *monomials*, where each monomial is a
16//! sorted product of symbols paired with an `i64` coefficient. Canonicalisation
17//! (constant folding, term merging, sorted monomials) means two structurally
18//! equal expressions compare equal — so identical derived dimensions (e.g. two
19//! `batch * seq` products) intern to the *same* fresh symbol and stay unified.
20//!
21//! This is deliberately **not** a general CAS: it captures exactly the affine
22//! and product forms the Phase-1 op set produces. Operations it cannot
23//! represent exactly (floor division by a symbol, non-exact division) surface
24//! as `None`, and the caller falls back to a fresh opaque symbol — the same
25//! permissive degrade the reference implementation uses.
26//!
27//! # Overflow contract
28//!
29//! Coefficients are `i64`. A pathological (but not necessarily malicious) graph
30//! can drive a concrete total past `i64::MAX` — e.g. a `Size`/`Reshape` product
31//! over four `2^20` dims is `2^80`. Every coefficient combiner
32//! ([`add`](DimExpr::add), [`sub`](DimExpr::sub), [`mul`](DimExpr::mul)) is
33//! therefore **checked**: on overflow it does **not** panic (as unchecked debug
34//! arithmetic would) and does **not** wrap to a bogus — possibly zero or
35//! negative — static dim (as unchecked release arithmetic would). Instead the
36//! result **degrades to an opaque unknown** ([`DimExpr::overflow`]): an
37//! expression that reports as neither a constant nor a bare symbol, poisons any
38//! further arithmetic it participates in, and lowers to a *fresh* symbol (see
39//! [`crate::context::SymbolInterner::lower`]). This matches the crate's
40//! permissive philosophy: a single pathological dim degrades to "unknown"
41//! rather than aborting whole-graph inference. [`checked_div`](DimExpr::checked_div)
42//! likewise returns `None` on overflow (including the `i64::MIN / -1` edge) so
43//! the caller degrades to a fresh symbol.
44
45use std::collections::BTreeMap;
46
47use onnx_runtime_ir::SymbolId;
48
49/// A monomial: a sorted product of symbol ids. The empty vector is the constant
50/// monomial (`1`). Stored as raw `u32`s so it is `Ord` for canonical keying.
51type Monomial = Vec<u32>;
52
53/// A canonical integer polynomial over symbolic dimensions.
54///
55/// Invariant: `terms` never contains a zero coefficient, and every key
56/// ([`Monomial`]) is sorted ascending. The empty map is the integer `0`.
57///
58/// The `overflow` flag marks an expression whose exact value could not be
59/// represented because a coefficient combiner exceeded `i64` range. Such an
60/// expression is an opaque unknown (see the module-level overflow contract):
61/// it is never a constant or bare symbol, and it lowers to a fresh symbol.
62#[derive(Clone, PartialEq, Eq, Hash, Debug, Default)]
63pub struct DimExpr {
64 terms: BTreeMap<Monomial, i64>,
65 overflow: bool,
66}
67
68impl DimExpr {
69 /// The constant `n`.
70 pub fn constant(n: i64) -> Self {
71 let mut terms = BTreeMap::new();
72 if n != 0 {
73 terms.insert(Vec::new(), n);
74 }
75 Self {
76 terms,
77 overflow: false,
78 }
79 }
80
81 /// A single symbolic dimension.
82 pub fn symbol(s: SymbolId) -> Self {
83 let mut terms = BTreeMap::new();
84 terms.insert(vec![s.0], 1);
85 Self {
86 terms,
87 overflow: false,
88 }
89 }
90
91 /// An opaque unknown produced by an arithmetic overflow. See the
92 /// module-level overflow contract. It reports as neither a constant nor a
93 /// bare symbol, poisons any arithmetic it participates in, and lowers to a
94 /// fresh symbol.
95 pub fn overflow() -> Self {
96 Self {
97 terms: BTreeMap::new(),
98 overflow: true,
99 }
100 }
101
102 /// Whether this expression is the overflow/unknown sentinel.
103 pub fn is_overflow(&self) -> bool {
104 self.overflow
105 }
106
107 /// The integer value, if this expression is a pure constant (includes `0`).
108 pub fn as_const(&self) -> Option<i64> {
109 if self.overflow {
110 return None;
111 }
112 match self.terms.len() {
113 0 => Some(0),
114 1 => self.terms.get(&Vec::new()).copied(),
115 _ => None,
116 }
117 }
118
119 /// The single symbol, if this expression is exactly one symbol with
120 /// coefficient `1` (e.g. a bare `Dim::Symbolic` round-trips through this).
121 pub fn as_symbol(&self) -> Option<SymbolId> {
122 if self.overflow || self.terms.len() != 1 {
123 return None;
124 }
125 let (mono, &coeff) = self.terms.iter().next()?;
126 if coeff == 1 && mono.len() == 1 {
127 Some(SymbolId(mono[0]))
128 } else {
129 None
130 }
131 }
132
133 /// Whether this is a pure constant.
134 pub fn is_const(&self) -> bool {
135 self.as_const().is_some()
136 }
137
138 /// Drop any term whose coefficient collapsed to zero.
139 fn prune(mut self) -> Self {
140 self.terms.retain(|_, c| *c != 0);
141 self
142 }
143
144 /// `self + other`.
145 ///
146 /// Overflow-safe: an out-of-range coefficient sum degrades the result to
147 /// [`DimExpr::overflow`] (never panics, never wraps). See the module-level
148 /// overflow contract.
149 pub fn add(&self, other: &DimExpr) -> DimExpr {
150 if self.overflow || other.overflow {
151 return DimExpr::overflow();
152 }
153 let mut terms = self.terms.clone();
154 for (mono, &coeff) in &other.terms {
155 let slot = terms.entry(mono.clone()).or_insert(0);
156 match slot.checked_add(coeff) {
157 Some(v) => *slot = v,
158 None => return DimExpr::overflow(),
159 }
160 }
161 DimExpr {
162 terms,
163 overflow: false,
164 }
165 .prune()
166 }
167
168 /// `self - other`.
169 ///
170 /// Overflow-safe: see [`add`](DimExpr::add).
171 pub fn sub(&self, other: &DimExpr) -> DimExpr {
172 if self.overflow || other.overflow {
173 return DimExpr::overflow();
174 }
175 let mut terms = self.terms.clone();
176 for (mono, &coeff) in &other.terms {
177 let slot = terms.entry(mono.clone()).or_insert(0);
178 match slot.checked_sub(coeff) {
179 Some(v) => *slot = v,
180 None => return DimExpr::overflow(),
181 }
182 }
183 DimExpr {
184 terms,
185 overflow: false,
186 }
187 .prune()
188 }
189
190 /// `self * other`.
191 ///
192 /// Overflow-safe: an out-of-range coefficient product or accumulation
193 /// degrades the result to [`DimExpr::overflow`]. See [`add`](DimExpr::add).
194 pub fn mul(&self, other: &DimExpr) -> DimExpr {
195 if self.overflow || other.overflow {
196 return DimExpr::overflow();
197 }
198 let mut terms: BTreeMap<Monomial, i64> = BTreeMap::new();
199 for (a_mono, &a_c) in &self.terms {
200 for (b_mono, &b_c) in &other.terms {
201 let Some(prod) = a_c.checked_mul(b_c) else {
202 return DimExpr::overflow();
203 };
204 let mut mono = a_mono.clone();
205 mono.extend_from_slice(b_mono);
206 mono.sort_unstable();
207 let slot = terms.entry(mono).or_insert(0);
208 match slot.checked_add(prod) {
209 Some(v) => *slot = v,
210 None => return DimExpr::overflow(),
211 }
212 }
213 }
214 DimExpr {
215 terms,
216 overflow: false,
217 }
218 .prune()
219 }
220
221 /// `self / other`, only when the division is *exact*.
222 ///
223 /// Handles the cases the op set actually produces: division by a non-zero
224 /// constant (every coefficient must divide evenly) and division by a single
225 /// monomial (symbol cancellation, as in `Reshape` `-1` inference where
226 /// `total = b*s*768` is divided by `b*s*12` to yield `64`). Anything else —
227 /// dividing by a multi-term polynomial, or a non-exact quotient — returns
228 /// `None` so the caller can degrade to a fresh symbol.
229 pub fn checked_div(&self, other: &DimExpr) -> Option<DimExpr> {
230 // A poisoned operand has no representable value: degrade (caller mints a
231 // fresh symbol on `None`).
232 if self.overflow || other.overflow {
233 return None;
234 }
235 if self.terms.is_empty() {
236 return Some(DimExpr::constant(0));
237 }
238 // Divisor must be a single monomial with a non-zero coefficient.
239 if other.terms.len() != 1 {
240 return None;
241 }
242 let (div_mono, &div_coeff) = other.terms.iter().next()?;
243 if div_coeff == 0 {
244 return None;
245 }
246 let mut out: BTreeMap<Monomial, i64> = BTreeMap::new();
247 for (mono, &coeff) in &self.terms {
248 // `checked_rem`/`checked_div` guard the `i64::MIN / -1` overflow
249 // (divisor coefficients can be negative via `sub`): `None` degrades
250 // to a fresh symbol rather than panicking.
251 if coeff.checked_rem(div_coeff)? != 0 {
252 return None;
253 }
254 // Subtract the divisor's symbol multiset from this monomial.
255 let mut remaining = mono.clone();
256 for sym in div_mono {
257 let pos = remaining.iter().position(|s| s == sym)?;
258 remaining.remove(pos);
259 }
260 out.insert(remaining, coeff.checked_div(div_coeff)?);
261 }
262 Some(
263 DimExpr {
264 terms: out,
265 overflow: false,
266 }
267 .prune(),
268 )
269 }
270
271 /// The product of a slice of expressions (`1` for an empty slice).
272 pub fn product(exprs: &[DimExpr]) -> DimExpr {
273 let mut acc = DimExpr::constant(1);
274 for e in exprs {
275 acc = acc.mul(e);
276 }
277 acc
278 }
279}
280
281impl From<onnx_runtime_ir::Dim> for DimExpr {
282 fn from(d: onnx_runtime_ir::Dim) -> Self {
283 match d {
284 onnx_runtime_ir::Dim::Static(n) => DimExpr::constant(n as i64),
285 onnx_runtime_ir::Dim::Symbolic(s) => DimExpr::symbol(s),
286 }
287 }
288}
289
290#[cfg(test)]
291mod tests {
292 use super::*;
293
294 fn sym(n: u32) -> DimExpr {
295 DimExpr::symbol(SymbolId(n))
296 }
297
298 #[test]
299 fn constant_folding() {
300 let e = DimExpr::constant(3).add(&DimExpr::constant(4));
301 assert_eq!(e.as_const(), Some(7));
302 assert!(e.is_const());
303 }
304
305 #[test]
306 fn zero_is_canonical() {
307 assert_eq!(DimExpr::constant(0).as_const(), Some(0));
308 assert_eq!(
309 DimExpr::constant(5).sub(&DimExpr::constant(5)).as_const(),
310 Some(0)
311 );
312 }
313
314 #[test]
315 fn symbol_roundtrip() {
316 let e = sym(2);
317 assert_eq!(e.as_symbol(), Some(SymbolId(2)));
318 // 2*d is not a bare symbol.
319 assert_eq!(e.add(&sym(2)).as_symbol(), None);
320 }
321
322 #[test]
323 fn affine_expression() {
324 // d0 + 5
325 let e = sym(0).add(&DimExpr::constant(5));
326 assert_eq!(e.as_const(), None);
327 assert_eq!(e.as_symbol(), None);
328 // (d0 + 5) - 5 == d0
329 assert_eq!(e.sub(&DimExpr::constant(5)).as_symbol(), Some(SymbolId(0)));
330 }
331
332 #[test]
333 fn product_of_symbols() {
334 // d0 * d1
335 let e = sym(0).mul(&sym(1));
336 // commutative canonical form: d1 * d0 equals d0 * d1
337 assert_eq!(e, sym(1).mul(&sym(0)));
338 }
339
340 #[test]
341 fn exact_constant_division() {
342 let e = DimExpr::constant(48);
343 assert_eq!(
344 e.checked_div(&DimExpr::constant(6)).unwrap().as_const(),
345 Some(8)
346 );
347 // non-exact
348 assert!(
349 DimExpr::constant(7)
350 .checked_div(&DimExpr::constant(2))
351 .is_none()
352 );
353 }
354
355 #[test]
356 fn reshape_minus_one_cancellation() {
357 // total = b * s * 768, known = b * s * 12 -> 64
358 let b = sym(0);
359 let s = sym(1);
360 let total = DimExpr::product(&[b.clone(), s.clone(), DimExpr::constant(768)]);
361 let known = DimExpr::product(&[b, s, DimExpr::constant(12)]);
362 let missing = total.checked_div(&known).unwrap();
363 assert_eq!(missing.as_const(), Some(64));
364 }
365
366 #[test]
367 fn division_by_multiterm_is_none() {
368 let total = sym(0).mul(&sym(1));
369 let divisor = sym(0).add(&DimExpr::constant(1));
370 assert!(total.checked_div(&divisor).is_none());
371 }
372
373 #[test]
374 fn symbolic_product_division_keeps_symbol() {
375 // (b * 768) / 768 == b
376 let e = sym(0).mul(&DimExpr::constant(768));
377 let q = e.checked_div(&DimExpr::constant(768)).unwrap();
378 assert_eq!(q.as_symbol(), Some(SymbolId(0)));
379 }
380
381 #[test]
382 fn from_ir_dim() {
383 use onnx_runtime_ir::Dim;
384 assert_eq!(DimExpr::from(Dim::Static(4)).as_const(), Some(4));
385 assert_eq!(
386 DimExpr::from(Dim::Symbolic(SymbolId(9))).as_symbol(),
387 Some(SymbolId(9))
388 );
389 }
390
391 #[test]
392 fn mul_overflow_degrades_to_unknown() {
393 // A 2^80-scale product (four 2^20 dims) exceeds i64: no panic (as debug
394 // unchecked arithmetic would) and no wrap-to-zero (as release would).
395 let big = DimExpr::constant(1 << 20);
396 let total = DimExpr::product(&[big.clone(), big.clone(), big.clone(), big]);
397 assert!(total.is_overflow());
398 assert_eq!(total.as_const(), None); // never a bogus concrete dim
399 assert_eq!(total.as_symbol(), None);
400 }
401
402 #[test]
403 fn add_and_sub_overflow_degrade() {
404 let max = DimExpr::constant(i64::MAX);
405 assert!(max.add(&DimExpr::constant(1)).is_overflow());
406 let min = DimExpr::constant(i64::MIN);
407 assert!(min.sub(&DimExpr::constant(1)).is_overflow());
408 }
409
410 #[test]
411 fn overflow_poisons_further_arithmetic() {
412 let poisoned = DimExpr::overflow();
413 assert!(poisoned.add(&DimExpr::constant(1)).is_overflow());
414 assert!(poisoned.mul(&DimExpr::constant(2)).is_overflow());
415 assert!(poisoned.sub(&DimExpr::constant(3)).is_overflow());
416 assert!(poisoned.checked_div(&DimExpr::constant(4)).is_none());
417 // An overflowed divisor also degrades.
418 assert!(DimExpr::constant(8).checked_div(&poisoned).is_none());
419 }
420
421 #[test]
422 fn checked_div_guards_i64_min_over_neg_one() {
423 // i64::MIN / -1 overflows; the guard degrades to None rather than panic.
424 let num = DimExpr::constant(i64::MIN);
425 let div = DimExpr::constant(-1);
426 assert!(num.checked_div(&div).is_none());
427 }
428}