Propagating invariants for optimization

1

this is more of a curiosity/challenge than a need but i have some code that i am trying to optimize by propagating some invariants such as the intersection of any set of bounding boxes always being fully contained by one of them when it exists.

seems to work very well with individual variables such as the code snippet below (all assert here are not present in the assembly output because the compiler can guarantee them to be always true)

pub fn f1(input:BoundingBox<i32, ScreenSpace>,cbb: [BoundingBox<i32,ScreenSpace>;4])->Option<BoundingBox<i32, ScreenSpace>>{
    let [cbb1,cbb2,cbb3,cbb4]=cbb;
    let mut smallest=input;
    smallest=smallest.intersection(&cbb1)?;
    smallest=smallest.intersection(&cbb2)?;
    smallest=smallest.intersection(&cbb3)?;
    smallest=smallest.intersection(&cbb4)?;
    assert!(smallest.pos.x>=input.pos.x);
    assert!(smallest.pos.y>=input.pos.y);
    assert!(smallest.pos.x+smallest.size.width<=input.pos.x+input.size.width);
    assert!(smallest.pos.y+smallest.size.height<=input.pos.y+input.size.height);
    Some(smallest)
}

however it does't propagate if it's done through a for loop or an iterator it seems (asserts are included in the binary and checked at runtime)

pub fn f2(input:BoundingBox<i32, ScreenSpace>,cbb:[BoundingBox<i32,ScreenSpace>;4])->Option<BoundingBox<i32, ScreenSpace>>{
    let smallest=cbb.iter().fold(Some(input),|acc,x|acc.and_then(|a|a.intersection(&x)))?;
    assert!(smallest.pos.x>=input.pos.x);
    assert!(smallest.pos.y>=input.pos.y);
    assert!(smallest.pos.x+smallest.size.width<=input.pos.x+input.size.width);
    assert!(smallest.pos.y+smallest.size.height<=input.pos.y+input.size.height);
    Some(smallest)
}

i am mostly just curious to know if anyone knows any tricks to propagate invariants through loops.
compiler used is nightly for aarch64-unknown-linux-gnu if it's relevant

2

Last time I've tried to propagate similar checks, I've found that non-trivial conditional code easily "forgets" them.

This seems to be a limitation of the LLVM optimizer, and it gets very tedious to work around it, where it's possible at all.

I recommend:

  1. Think super hard about numeric overflows. It's not true that a + b > a. That's not a bug, not even a limitation of the optimizer. First, you need to prove that your arithmetic can't overflow (or use checked arithmetic and handle overflows explicitly).

  2. Put the high-level checks/assertions you think are sufficient where they belong, regardless whether the optimizer currently can use them or not. It will eventually if/when it gets better.

  3. Use cargo-show-asm to find missed optimizations and tweak code to make it optimize if possible, or at least minimize bloat with code like if !checks { abort(); } that generates less code bloat than redundant panicking asserts. If you have earlier checks, the later ones are (probably) redundant so they don't need to be pretty, just as cheap as possible.

3 Likes
3

makes sense i immagine that tracking all kinds of invariants across all branches can get challenging for the compiler. would be cool if you could have points where you are allowed to explicitly remind it