Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

add support for lnot on ints and uints #574

Merged
merged 2 commits into from
Dec 13, 2023
Merged

add support for lnot on ints and uints #574

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
8e58d17
add support for lnot on ints and uints
enjhnsn2 Dec 7, 2023
762c301
make recommended changes for PR #574
enjhnsn2 Dec 12, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
17 changes: 16 additions & 1 deletion crates/flux-refineck/src/sigs/default.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ use flux_middle::{
rty::{BaseTy, BinOp, Expr, INT_TYS, UINT_TYS},
rustc::mir,
};
use itertools::iproduct;
use itertools::{chain, iproduct};

use super::{Sig, SigTable};
use crate::{
Expand All @@ -30,6 +30,7 @@ pub(super) static UN_OPS: LazyLock<SigTable<mir::UnOp, 1>> = LazyLock::new(|| {

table.extend(mk_neg());
table.extend([mk_not()]);
table.extend(mk_lnot());

table
});
Expand Down Expand Up @@ -166,3 +167,17 @@ pub(crate) fn mk_not() -> (mir::UnOp, Sig<1>) {
define_btys! { let bool = BaseTy::Bool; }
(mir::UnOp::Not, s!(fn(a: bool) -> bool[a.not()]))
}

pub(crate) fn mk_lnot() -> impl IntoIterator<Item = (mir::UnOp, Sig<1>)> {
let int_lnots = INT_TYS.map(|int_ty| {
define_btys! { let Int = BaseTy::Int(int_ty); };
(mir::UnOp::Not, s!(fn(a: Int) -> Int{v: E::tt()}))
});

let uint_lnots = UINT_TYS.map(|uint_ty| {
define_btys! { let Uint = BaseTy::Uint(uint_ty); };
(mir::UnOp::Not, s!(fn(a: Uint) -> Uint{v: E::tt()}))
});

chain!(int_lnots, uint_lnots)
}
1 change: 1 addition & 0 deletions crates/flux-refineck/src/sigs/overflow.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,7 @@ pub(super) static UN_OPS: LazyLock<SigTable<mir::UnOp, 1>> = LazyLock::new(|| {

table.extend(mk_neg());
table.extend([super::default::mk_not()]);
table.extend(super::default::mk_lnot());

table
});
Expand Down
24 changes: 24 additions & 0 deletions crates/flux-tests/tests/pos/surface/binop.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -64,6 +64,18 @@ pub fn bitwise_shr_u32_u32(a: u32, b: u32) -> u32 {
a >> b
}

// Bitwise UnOps
#[flux::sig(fn(u32{v: v > 0}) -> u32)]
pub fn bitwise_not_u32(a: u32) -> u32 {
!a
}

#[flux::sig(fn(i32{v: v > 0}) -> i32)]
pub fn bitwise_not_i32(a: i32) -> i32 {
!a
}


// Logical BinOps
#[flux::sig(fn(a: bool, b: bool) -> bool{v: v == a || v == b})]
pub fn logical_or(a: bool, b: bool) -> bool {
Expand All @@ -79,3 +91,15 @@ pub fn logical_or_ft(a: bool, b: bool) -> bool {
pub fn logical_or_ff(a: bool, b: bool) -> bool {
a | b
}

// Logical UnOps
#[flux::sig(fn(bool[true]) -> bool[false])]
pub fn logical_not_t(a: bool) -> bool {
!a
}

#[flux::sig(fn(bool[false]) -> bool[true])]
pub fn logical_not_f(a: bool) -> bool {
!a
}

Loading