Contracts guiding optimization

A compiler can perform optimizations based on data properties it knows:

let num = num * 2;

if num == 5 {
    doing_work()
}

This turns into a no-op for integer nums because there is never work to be done.

In practice, the point where the property is visible to the compiler is often far away from where it could be used. (And it may be more complex, though when working with indices in a const-sized aray, simple bounds could often make a difference). But we have immutability guarantees, so doing a lot of things manually, we could have:

struct Even8(u8);
impl Even8 {
    fn new(input: u8) -> Result<Self, ()> {
        if input & 1 == 1 {
            return Err(())
        }
        Ok(Even8(input))
    }

    fn get(&self) -> u8 {
        if self.0 & 1 == 1 {
            unsafe { std::hint::unreachable_unchecked() }
        }
        self.0
    }
}

pub fn check(num: u8) {
    let num = Even8::new(num).unwrap();

    if num.get() == 5 {
        doing_work()
    }
}

#[inline(never)]
fn doing_work() {
    doing_work()
}

where the unsafe is justified because all ways to get a legal Even8 make its inner value indeed even -- and godbolt shows that indeed while the unreachable_unchecked is in place, doing_work is never jumped to.

For this to be practically usabe, it'd need to be somewhat automated, and probably described in terms of contracts (for the struct itself, and thus any function that creates it) -- for example, the constructor could be guarded with an assert!. (The assert will be optimized away here as the compiler can show locally that it will never trigger because it branched on the same condition just before; but generally, it will ensure that no programmer error will send things down the UB path of unreachable_unchecked).

Before I go and hack around on this: Are there any crates around that maybe already do some of this? I've looked at contract based programming, but all I found was more focused on verification and less on optimization. (Plus I found a lot of crates on completely unrelated "smart contracts").

1 Like

I found at least one crate that goes part of the way: pre, as recently advertised on RustConf

I think the NonZero use of rustc_layout_scalar_valid_range_start(1) is sort of an example of what you're talking about (a very limited one though)?

I'm aware of tools that help you achieve this sort of pre-condition programming, MIRAI, and Prusti.

It was pointed out to me before that Rust used to have pre-conditions that could potentially help with these optimizations.

This topic was automatically closed 90 days after the last reply. We invite you to open a new topic if you have further questions or comments.