From 8e58d17e8d23592ed4d0ac4bcde98668b1bcec2b Mon Sep 17 00:00:00 2001 From: Evan Johnson Date: Thu, 7 Dec 2023 15:13:04 -0800 Subject: [PATCH 1/2] add support for lnot on ints and uints --- crates/flux-refineck/src/sigs/default.rs | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) diff --git a/crates/flux-refineck/src/sigs/default.rs b/crates/flux-refineck/src/sigs/default.rs index aaac77c63f..ffa18995b1 100644 --- a/crates/flux-refineck/src/sigs/default.rs +++ b/crates/flux-refineck/src/sigs/default.rs @@ -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::{ @@ -30,6 +30,7 @@ pub(super) static UN_OPS: LazyLock> = LazyLock::new(|| { table.extend(mk_neg()); table.extend([mk_not()]); + table.extend(mk_lnot()); table }); @@ -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)> { + let int_lnots = INT_TYS.map(|int_ty| { + define_btys! { let Int = BaseTy::Int(int_ty); }; + (mir::UnOp::Not, s!(fn(a: Int) -> Int[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[E::tt()])) + }); + + chain!(int_lnots, uint_lnots) +} From 762c301f3bf995b19ea5131ba07b61383774117c Mon Sep 17 00:00:00 2001 From: Evan Johnson Date: Tue, 12 Dec 2023 10:51:05 -0800 Subject: [PATCH 2/2] make recommended changes for PR #574 --- crates/flux-refineck/src/sigs/default.rs | 4 ++-- crates/flux-refineck/src/sigs/overflow.rs | 1 + crates/flux-tests/tests/pos/surface/binop.rs | 24 ++++++++++++++++++++ 3 files changed, 27 insertions(+), 2 deletions(-) diff --git a/crates/flux-refineck/src/sigs/default.rs b/crates/flux-refineck/src/sigs/default.rs index ffa18995b1..6775417698 100644 --- a/crates/flux-refineck/src/sigs/default.rs +++ b/crates/flux-refineck/src/sigs/default.rs @@ -171,12 +171,12 @@ pub(crate) fn mk_not() -> (mir::UnOp, Sig<1>) { pub(crate) fn mk_lnot() -> impl IntoIterator)> { let int_lnots = INT_TYS.map(|int_ty| { define_btys! { let Int = BaseTy::Int(int_ty); }; - (mir::UnOp::Not, s!(fn(a: Int) -> Int[E::tt()])) + (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[E::tt()])) + (mir::UnOp::Not, s!(fn(a: Uint) -> Uint{v: E::tt()})) }); chain!(int_lnots, uint_lnots) diff --git a/crates/flux-refineck/src/sigs/overflow.rs b/crates/flux-refineck/src/sigs/overflow.rs index ca2a8e75ee..fe66057bb6 100644 --- a/crates/flux-refineck/src/sigs/overflow.rs +++ b/crates/flux-refineck/src/sigs/overflow.rs @@ -29,6 +29,7 @@ pub(super) static UN_OPS: LazyLock> = LazyLock::new(|| { table.extend(mk_neg()); table.extend([super::default::mk_not()]); + table.extend(super::default::mk_lnot()); table }); diff --git a/crates/flux-tests/tests/pos/surface/binop.rs b/crates/flux-tests/tests/pos/surface/binop.rs index f2aedb98b0..dec17fc35b 100644 --- a/crates/flux-tests/tests/pos/surface/binop.rs +++ b/crates/flux-tests/tests/pos/surface/binop.rs @@ -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 { @@ -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 +} +