diff --git a/lib/flux-rs/src/bitvec.rs b/lib/flux-rs/src/bitvec.rs new file mode 100644 index 0000000000..df50c4794d --- /dev/null +++ b/lib/flux-rs/src/bitvec.rs @@ -0,0 +1,162 @@ +use core::{ + cmp::Ordering, + ops::{Add, BitAnd, BitOr, Not, Rem, Shl, Shr, Sub}, +}; + +use flux_attrs::*; + +#[derive(Debug, Clone, Copy, Hash)] +#[opaque] +#[refined_by(x: bitvec<32>)] +pub struct BV32(u32); + +#[trusted] +impl PartialOrd for BV32 { + fn partial_cmp(&self, other: &Self) -> Option { + self.0.partial_cmp(&other.0) + } + + #[sig(fn(&BV32[@x], &BV32[@y]) -> bool[bv_ule(x, y)])] + fn le(&self, other: &Self) -> bool { + self.0 <= other.0 + } + + #[sig(fn(&BV32[@x], &BV32[@y]) -> bool[bv_ult(x, y)])] + fn lt(&self, other: &Self) -> bool { + self.0 < other.0 + } + + #[sig(fn(&BV32[@x], &BV32[@y]) -> bool[bv_uge(x, y)])] + fn ge(&self, other: &Self) -> bool { + self.0 >= other.0 + } + + #[sig(fn(&BV32[@x], &BV32[@y]) -> bool[bv_ugt(x, y)])] + fn gt(&self, other: &Self) -> bool { + self.0 > other.0 + } +} + +#[trusted] +impl BV32 { + #[sig(fn(BV32[@x], BV32[@y]) -> BV32[bv_add(x, y)])] + pub fn wrapping_add(self, other: BV32) -> BV32 { + BV32(self.0.wrapping_add(other.0)) + } + + #[sig(fn (u32[@val]) -> BV32[bv_int_to_bv32(val)])] + pub const fn new(value: u32) -> BV32 { + BV32(value) + } +} + +impl From for BV32 { + #[trusted] + #[sig(fn(u32[@val]) -> BV32[bv_int_to_bv32(val)])] + fn from(value: u32) -> BV32 { + BV32(value) + } +} + +impl Into for BV32 { + #[trusted] + #[sig(fn(BV32[@val]) -> u32[bv_bv32_to_int(val)])] + fn into(self) -> u32 { + self.0 + } +} + +impl Not for BV32 { + type Output = BV32; + + #[trusted] + #[sig(fn(BV32[@x]) -> BV32[bv_not(x)])] + fn not(self) -> BV32 { + BV32(!self.0) + } +} + +impl BitAnd for BV32 { + type Output = BV32; + + #[trusted] + #[sig(fn(BV32[@x], BV32[@y]) -> BV32[bv_and(x, y)])] + fn bitand(self, rhs: Self) -> BV32 { + BV32(self.0 & rhs.0) + } +} + +impl BitOr for BV32 { + type Output = BV32; + + #[trusted] + #[sig(fn(BV32[@x], BV32[@y]) -> BV32[bv_or(x, y)])] + fn bitor(self, rhs: Self) -> BV32 { + BV32(self.0 | rhs.0) + } +} + +impl Shl for BV32 { + type Output = BV32; + + #[trusted] + #[sig(fn(BV32[@x], BV32[@y]) -> BV32[bv_shl(x, y)])] + fn shl(self, rhs: Self) -> BV32 { + BV32(self.0 << rhs.0) + } +} + +impl Shr for BV32 { + type Output = BV32; + + #[trusted] + #[sig(fn(BV32[@x], BV32[@y]) -> BV32[bv_lshr(x, y)])] + fn shr(self, rhs: Self) -> BV32 { + BV32(self.0 >> rhs.0) + } +} + +impl Add for BV32 { + type Output = BV32; + + #[trusted] + #[sig(fn(BV32[@val1], BV32[@val2]) -> BV32[bv_add(val1, val2)])] + fn add(self, rhs: Self) -> BV32 { + BV32(self.0 + rhs.0) + } +} + +impl Sub for BV32 { + type Output = BV32; + + #[trusted] + #[sig(fn(BV32[@val1], BV32[@val2]) -> BV32[bv_sub(val1, val2)])] + fn sub(self, rhs: Self) -> BV32 { + BV32(self.0.wrapping_add(!rhs.0)) + } +} + +impl Rem for BV32 { + type Output = BV32; + + #[trusted] + #[sig(fn(BV32[@val1], BV32[@val2]) -> BV32[bv_urem(val1, val2)])] + fn rem(self, rhs: Self) -> BV32 { + BV32(self.0 & rhs.0) + } +} + +#[trusted] +impl PartialEq for BV32 { + #[sig(fn(&BV32[@val1], &BV32[@val2]) -> bool[val1 == val2])] + fn eq(&self, other: &Self) -> bool { + self.0 == other.0 + } + + #[sig(fn(&BV32[@val1], &BV32[@val2]) -> bool[val1 != val2])] + fn ne(&self, other: &Self) -> bool { + self.0 != other.0 + } +} + +impl Eq for BV32 {} diff --git a/lib/flux-rs/src/lib.rs b/lib/flux-rs/src/lib.rs index a9b572e1e5..a157b2c3f2 100644 --- a/lib/flux-rs/src/lib.rs +++ b/lib/flux-rs/src/lib.rs @@ -1,3 +1,5 @@ +pub mod bitvec; + pub use flux_attrs::*; #[sig(fn(bool[true]) )] diff --git a/xtask/src/main.rs b/xtask/src/main.rs index e2d80ad220..705835fc7e 100644 --- a/xtask/src/main.rs +++ b/xtask/src/main.rs @@ -2,6 +2,7 @@ use std::{ env, ffi::OsStr, path::{Path, PathBuf}, + process::ExitStatus, }; use anyhow::anyhow; @@ -275,11 +276,31 @@ fn run_cargo>( } } - child.wait()?; + check_status(child.wait()?)?; Ok(artifacts) } +fn check_status(st: ExitStatus) -> anyhow::Result<()> { + if st.success() { + return Ok(()); + } + let err = match st.code() { + Some(code) => anyhow!("command exited with non-zero code: {code}"), + #[cfg(unix)] + None => { + use std::os::unix::process::ExitStatusExt; + match st.signal() { + Some(sig) => anyhow!("command was terminated by a signal: {sig}"), + None => anyhow!("command was terminated by a signal"), + } + } + #[cfg(not(unix))] + None => anyhow!("command was terminated by a signal"), + }; + Err(err) +} + fn display_command(cmd: &std::process::Command) { for var in cmd.get_envs() { if let Some(val) = var.1 {