Skip to content

Commit

Permalink
Upstream BV32 (#965)
Browse files Browse the repository at this point in the history
  • Loading branch information
nilehmann authored Jan 6, 2025
1 parent 50e349d commit 24003ac
Show file tree
Hide file tree
Showing 3 changed files with 186 additions and 1 deletion.
162 changes: 162 additions & 0 deletions lib/flux-rs/src/bitvec.rs
Original file line number Diff line number Diff line change
@@ -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<Ordering> {
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<u32> for BV32 {
#[trusted]
#[sig(fn(u32[@val]) -> BV32[bv_int_to_bv32(val)])]
fn from(value: u32) -> BV32 {
BV32(value)
}
}

impl Into<u32> 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 {}
2 changes: 2 additions & 0 deletions lib/flux-rs/src/lib.rs
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
pub mod bitvec;

pub use flux_attrs::*;

#[sig(fn(bool[true]) )]
Expand Down
23 changes: 22 additions & 1 deletion xtask/src/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ use std::{
env,
ffi::OsStr,
path::{Path, PathBuf},
process::ExitStatus,
};

use anyhow::anyhow;
Expand Down Expand Up @@ -275,11 +276,31 @@ fn run_cargo<S: AsRef<OsStr>>(
}
}

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 {
Expand Down

0 comments on commit 24003ac

Please sign in to comment.