flux-rs / flux

Refinement Types for Rust
MIT License
658 stars 21 forks source link

Add flux attribute for checking overflows #861

Closed vrindisbacher closed 4 weeks ago

vrindisbacher commented 1 month ago

Adds a flux attribute to check overflows, similar to flux_rs::trusted. Fixes (#827).

vrindisbacher commented 1 month ago

@nilehmann, I assume I should add some tests? Is there a convention to follow when adding those?

Also, for now, since I figured we would want to keep the global configuration of check_overflow, I override check_overflow in the CheckerConfig. I followed a similar approach to trusted for applying the attr to modules.

I tested on my own file (see below) and got expected results.

#[flux::check_overflow]
mod my_mod {
    fn add(x: u32, y: u32) -> u32 {
        x + y
    }

    fn add2(x: u32) -> u32 {
        x + 2
    }
}

#[flux_rs::refined_by(inner: int)]
struct MyStruct {
    #[field(u32[inner])]
    inner: u32,
}

impl MyStruct {
    fn add1(&self) -> u32 {
        self.inner + 1
    }

    #[flux::check_overflow]
    fn add2(&self) -> u32 {
        self.inner + 2
    }
}

#[flux::check_overflow]
impl MyStruct {
    fn add3(&self) -> u32 {
        self.inner + 3
    }

    fn add4(&self) -> u32 {
        self.inner + 4
    }
}