oxilean-kernel 0.1.5

OxiLean kernel - The trusted computing base for type checking
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49

//! `abstract_div` against a verbatim copy of its earlier body.

use super::*;

/// The division as the earlier body computed it.
fn earlier_abstract_div(a: &Interval, b: &Interval) -> Interval {
    if a.is_bottom() || b.is_bottom() {
        return Interval::bottom();
    }
    if b.contains(0) {
        return Interval::top();
    }
    let combos = [a.lo / b.lo, a.lo / b.hi, a.hi / b.lo, a.hi / b.hi];
    let lo = *combos
        .iter()
        .min()
        .expect("combos iterator must be non-empty");
    let hi = *combos
        .iter()
        .max()
        .expect("combos iterator must be non-empty");
    Interval::new(lo, hi)
}

#[test]
fn agrees_with_the_earlier_body_on_every_pair_of_bounds() {
    let bounds = [i64::MIN + 1, -9, -2, -1, 0, 1, 3, 7, i64::MAX];
    let mut dividends = vec![Interval::bottom()];
    for &lo in &bounds {
        for &hi in &bounds {
            if lo <= hi {
                dividends.push(Interval::new(lo, hi));
            }
        }
    }
    // `top` reaches `i64::MIN`, whose quotient by -1 overflows in either body,
    // so it is tried as a divisor only (it contains 0).
    let mut divisors = dividends.clone();
    divisors.push(Interval::top());
    for a in &dividends {
        for b in &divisors {
            assert_eq!(
                abstract_div(a, b),
                earlier_abstract_div(a, b),
                "{a:?} / {b:?}"
            );
        }
    }
}