diff --git a/crates/flux-desugar/src/desugar.rs b/crates/flux-desugar/src/desugar.rs index ccabed6419..d849b493a5 100644 --- a/crates/flux-desugar/src/desugar.rs +++ b/crates/flux-desugar/src/desugar.rs @@ -999,6 +999,10 @@ trait DesugarCtxt<'genv, 'tcx: 'genv> { Ok((self.genv().alloc_slice(&fhir_args), self.genv().alloc_slice(&constraints))) } + /// This is the mega desugaring function [`surface::Ty`] -> [`fhir::Ty`]. + /// These are both similar representations. The most important difference is that + /// [`fhir::Ty`] has explicit refinement parameters and [`surface::Ty`] does not. + /// Refinements are implicitly scoped in surface. fn desugar_ty(&mut self, ty: &surface::Ty) -> Result<fhir::Ty<'genv>> { let node_id = ty.node_id; let span = ty.span; @@ -1358,6 +1362,7 @@ trait DesugarCtxt<'genv, 'tcx: 'genv> { } } + /// Desugar surface literal fn desugar_lit(&self, span: Span, lit: surface::Lit) -> Result<fhir::Lit> { match lit.kind { surface::LitKind::Integer => { @@ -1373,6 +1378,9 @@ trait DesugarCtxt<'genv, 'tcx: 'genv> { } surface::LitKind::Bool => Ok(fhir::Lit::Bool(lit.symbol == kw::True)), surface::LitKind::Str => Ok(fhir::Lit::Str(lit.symbol)), + surface::LitKind::Char => { + Ok(fhir::Lit::Char(lit.symbol.as_str().parse::<char>().unwrap())) + } _ => Err(self.emit_err(errors::UnexpectedLiteral { span })), } } diff --git a/crates/flux-fhir-analysis/src/conv/mod.rs b/crates/flux-fhir-analysis/src/conv/mod.rs index 53f432a65c..45a6ec86a8 100644 --- a/crates/flux-fhir-analysis/src/conv/mod.rs +++ b/crates/flux-fhir-analysis/src/conv/mod.rs @@ -2084,6 +2084,7 @@ fn conv_lit(lit: fhir::Lit) -> rty::Constant { fhir::Lit::Real(r) => rty::Constant::Real(rty::Real(r)), fhir::Lit::Bool(b) => rty::Constant::from(b), fhir::Lit::Str(s) => rty::Constant::from(s), + fhir::Lit::Char(c) => rty::Constant::from(c), } } fn conv_un_op(op: fhir::UnOp) -> rty::UnOp { diff --git a/crates/flux-fhir-analysis/src/wf/sortck.rs b/crates/flux-fhir-analysis/src/wf/sortck.rs index d1cb360085..a169cd8ba0 100644 --- a/crates/flux-fhir-analysis/src/wf/sortck.rs +++ b/crates/flux-fhir-analysis/src/wf/sortck.rs @@ -712,6 +712,7 @@ fn synth_lit(lit: fhir::Lit) -> rty::Sort { fhir::Lit::Bool(_) => rty::Sort::Bool, fhir::Lit::Real(_) => rty::Sort::Real, fhir::Lit::Str(_) => rty::Sort::Str, + fhir::Lit::Char(_) => rty::Sort::Char, } } diff --git a/crates/flux-infer/src/fixpoint_encoding.rs b/crates/flux-infer/src/fixpoint_encoding.rs index 97abd0cbcc..b6243efe65 100644 --- a/crates/flux-infer/src/fixpoint_encoding.rs +++ b/crates/flux-infer/src/fixpoint_encoding.rs @@ -177,6 +177,7 @@ impl SortEncodingCtxt { rty::Sort::Real => fixpoint::Sort::Real, rty::Sort::Bool => fixpoint::Sort::Bool, rty::Sort::Str => fixpoint::Sort::Str, + rty::Sort::Char => fixpoint::Sort::Int, rty::Sort::BitVec(size) => fixpoint::Sort::BitVec(Box::new(bv_size_to_fixpoint(*size))), // There's no way to declare opaque sorts in the fixpoint horn syntax so we encode user // declared opaque sorts, type parameter sorts, and (unormalizable) type alias sorts as @@ -597,6 +598,7 @@ fn const_to_fixpoint(cst: rty::Constant) -> fixpoint::Constant { rty::Constant::Int(i) => fixpoint::Constant::Numeral(i), rty::Constant::Real(r) => fixpoint::Constant::Decimal(r), rty::Constant::Bool(b) => fixpoint::Constant::Boolean(b), + rty::Constant::Char(c) => fixpoint::Constant::Numeral(BigInt::from(u32::from(c))), rty::Constant::Str(s) => fixpoint::Constant::String(fixpoint::SymStr(s)), } } @@ -1120,7 +1122,7 @@ impl<'genv, 'tcx> ExprEncodingCtxt<'genv, 'tcx> { scx: &mut SortEncodingCtxt, ) -> QueryResult<fixpoint::Expr> { let e = match sort { - rty::Sort::Int | rty::Sort::Real => { + rty::Sort::Int | rty::Sort::Real | rty::Sort::Char => { fixpoint::Expr::Atom( rel, Box::new([self.expr_to_fixpoint(e1, scx)?, self.expr_to_fixpoint(e2, scx)?]), diff --git a/crates/flux-middle/src/big_int.rs b/crates/flux-middle/src/big_int.rs index 6389019f0f..c7f57895a9 100644 --- a/crates/flux-middle/src/big_int.rs +++ b/crates/flux-middle/src/big_int.rs @@ -76,6 +76,12 @@ impl From<i32> for BigInt { } } +impl From<u32> for BigInt { + fn from(val: u32) -> Self { + BigInt { sign: Sign::NonNegative, val: val as u128 } + } +} + impl liquid_fixpoint::FixpointFmt for BigInt { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self.sign { diff --git a/crates/flux-middle/src/fhir.rs b/crates/flux-middle/src/fhir.rs index 4767ce972e..dd48e32ca9 100644 --- a/crates/flux-middle/src/fhir.rs +++ b/crates/flux-middle/src/fhir.rs @@ -937,7 +937,8 @@ pub enum Lit { Int(i128), Real(i128), Bool(bool), - Str(Symbol), + Str(Symbol), // `rustc_span::Symbol` interns a value with the type + Char(char), // all Rust chars are u32s } #[derive(Clone, Copy, Debug)] @@ -1427,6 +1428,7 @@ impl fmt::Debug for Lit { Lit::Real(r) => write!(f, "{r}real"), Lit::Bool(b) => write!(f, "{b}"), Lit::Str(s) => write!(f, "\"{s:?}\""), + Lit::Char(c) => write!(f, "\'{c}\'"), } } } diff --git a/crates/flux-middle/src/rty/expr.rs b/crates/flux-middle/src/rty/expr.rs index 72da28cf44..1f12037a8d 100644 --- a/crates/flux-middle/src/rty/expr.rs +++ b/crates/flux-middle/src/rty/expr.rs @@ -479,6 +479,10 @@ impl Expr { } BaseTy::Uint(_) => ExprKind::Constant(Constant::from(bits)).intern(), BaseTy::Bool => ExprKind::Constant(Constant::Bool(bits != 0)).intern(), + BaseTy::Char => { + let c = char::from_u32(bits.try_into().unwrap()).unwrap(); + ExprKind::Constant(Constant::Char(c)).intern() + } _ => bug!(), } } @@ -905,6 +909,7 @@ pub enum Constant { Real(Real), Bool(bool), Str(Symbol), + Char(char), } impl Constant { @@ -983,7 +988,11 @@ impl Constant { let b = scalar_to_bits(tcx, scalar, ty)?; Some(Constant::Bool(b != 0)) } - _ => None, + TyKind::Char => { + let b = scalar_to_bits(tcx, scalar, ty)?; + Some(Constant::Char(char::from_u32(b as u32)?)) + } + _ => bug!(), } } @@ -1039,6 +1048,12 @@ impl From<Symbol> for Constant { } } +impl From<char> for Constant { + fn from(c: char) -> Self { + Constant::Char(c) + } +} + impl_internable!(ExprKind); impl_slice_internable!(Expr, KVar); @@ -1195,7 +1210,8 @@ mod pretty { Constant::Int(i) => w!("{i}"), Constant::Real(r) => w!("{}.0", ^r.0), Constant::Bool(b) => w!("{b}"), - Constant::Str(sym) => w!("{sym}"), + Constant::Str(sym) => w!("\"{sym}\""), + Constant::Char(c) => write!(f, "\'{c}\'"), } } } diff --git a/crates/flux-middle/src/rty/fold.rs b/crates/flux-middle/src/rty/fold.rs index 4956bc9f5a..df3a92df50 100644 --- a/crates/flux-middle/src/rty/fold.rs +++ b/crates/flux-middle/src/rty/fold.rs @@ -448,6 +448,7 @@ impl TypeSuperVisitable for Sort { | Sort::Bool | Sort::Real | Sort::Str + | Sort::Char | Sort::BitVec(_) | Sort::Loc | Sort::Param(_) @@ -476,6 +477,7 @@ impl TypeSuperFoldable for Sort { | Sort::Real | Sort::Loc | Sort::Str + | Sort::Char | Sort::BitVec(_) | Sort::Param(_) | Sort::Var(_) diff --git a/crates/flux-middle/src/rty/mod.rs b/crates/flux-middle/src/rty/mod.rs index 134fb8b4fa..f7e59ff9eb 100644 --- a/crates/flux-middle/src/rty/mod.rs +++ b/crates/flux-middle/src/rty/mod.rs @@ -749,6 +749,7 @@ pub enum Sort { Real, BitVec(BvSize), Str, + Char, Loc, Param(ParamTy), Tuple(List<Sort>), @@ -1271,6 +1272,13 @@ impl Ty { .unwrap_or_default() } + /// Whether the type is a `char` + pub fn is_char(&self) -> bool { + self.as_bty_skipping_existentials() + .map(BaseTy::is_char) + .unwrap_or_default() + } + pub fn is_uninit(&self) -> bool { matches!(self.kind(), TyKind::Uninit) } @@ -1544,6 +1552,14 @@ impl BaseTy { matches!(self, BaseTy::Adt(adt_def, _) if adt_def.is_box()) } + pub fn is_char(&self) -> bool { + matches!(self, BaseTy::Char) + } + + pub fn is_str(&self) -> bool { + matches!(self, BaseTy::Str) + } + pub fn unpack_box(&self) -> Option<(&Ty, &Ty)> { if let BaseTy::Adt(adt_def, args) = self && adt_def.is_box() diff --git a/crates/flux-middle/src/rty/pretty.rs b/crates/flux-middle/src/rty/pretty.rs index b721b519a3..90da338581 100644 --- a/crates/flux-middle/src/rty/pretty.rs +++ b/crates/flux-middle/src/rty/pretty.rs @@ -96,6 +96,7 @@ impl Pretty for Sort { Sort::Int => w!("int"), Sort::Real => w!("real"), Sort::Str => w!("str"), + Sort::Char => w!("char"), Sort::BitVec(size) => w!("bitvec({:?})", size), Sort::Loc => w!("loc"), Sort::Var(n) => w!("@{}", ^n.index()), diff --git a/crates/flux-middle/src/sort_of.rs b/crates/flux-middle/src/sort_of.rs index 581061fecb..cd51d12746 100644 --- a/crates/flux-middle/src/sort_of.rs +++ b/crates/flux-middle/src/sort_of.rs @@ -37,6 +37,7 @@ impl<'sess, 'tcx> GlobalEnv<'sess, 'tcx> { let sort = match ty.kind() { ty::TyKind::Bool => Some(rty::Sort::Bool), ty::TyKind::Slice(_) | ty::TyKind::Int(_) | ty::TyKind::Uint(_) => Some(rty::Sort::Int), + ty::TyKind::Char => Some(rty::Sort::Char), ty::TyKind::Str => Some(rty::Sort::Str), ty::TyKind::Adt(adt_def, args) => { let mut sort_args = vec![]; @@ -58,7 +59,6 @@ impl<'sess, 'tcx> GlobalEnv<'sess, 'tcx> { self.sort_of_generic_param(generic_param_def.def_id)? } ty::TyKind::Float(_) - | ty::TyKind::Char | ty::TyKind::RawPtr(..) | ty::TyKind::Ref(..) | ty::TyKind::Tuple(_) @@ -95,6 +95,7 @@ impl rty::BaseTy { match self { rty::BaseTy::Int(_) | rty::BaseTy::Uint(_) | rty::BaseTy::Slice(_) => rty::Sort::Int, rty::BaseTy::Bool => rty::Sort::Bool, + rty::BaseTy::Char => rty::Sort::Char, rty::BaseTy::Adt(adt_def, args) => adt_def.sort(args), rty::BaseTy::Param(param_ty) => rty::Sort::Param(*param_ty), rty::BaseTy::Str => rty::Sort::Str, @@ -108,7 +109,6 @@ impl rty::BaseTy { rty::Sort::Alias(*kind, alias_ty) } rty::BaseTy::Float(_) - | rty::BaseTy::Char | rty::BaseTy::RawPtr(..) | rty::BaseTy::Ref(..) | rty::BaseTy::FnPtr(..) diff --git a/crates/flux-refineck/src/checker.rs b/crates/flux-refineck/src/checker.rs index 31ec23e2df..2bb78c2cfc 100644 --- a/crates/flux-refineck/src/checker.rs +++ b/crates/flux-refineck/src/checker.rs @@ -633,7 +633,7 @@ impl<'ck, 'genv, 'tcx, M: Mode> Checker<'ck, 'genv, 'tcx, M> { } TerminatorKind::SwitchInt { discr, targets } => { let discr_ty = self.check_operand(infcx, env, terminator_span, discr)?; - if discr_ty.is_integral() || discr_ty.is_bool() { + if discr_ty.is_integral() || discr_ty.is_bool() || discr_ty.is_char() { Ok(Self::check_if(&discr_ty, targets)) } else { Ok(Self::check_match(&discr_ty, targets)) @@ -943,6 +943,8 @@ impl<'ck, 'genv, 'tcx, M: Mode> Checker<'ck, 'genv, 'tcx, M> { Ok(Guard::Pred(pred)) } + /// Checks conditional branching as in a `match` statement. [`SwitchTargets`] (https://doc.rust-lang.org/nightly/nightly-rustc/stable_mir/mir/struct.SwitchTargets.html) contains a list of branches - the exact bit value which is being compared and the block to jump to. Using the conditionals, each branch can be checked using the new control flow information. + /// See https://github.com/flux-rs/flux/pull/840#discussion_r1786543174 fn check_if(discr_ty: &Ty, targets: &SwitchTargets) -> Vec<(BasicBlock, Guard)> { let mk = |bits| { match discr_ty.kind() { @@ -953,7 +955,7 @@ impl<'ck, 'genv, 'tcx, M: Mode> Checker<'ck, 'genv, 'tcx, M> { idx.clone() } } - TyKind::Indexed(bty @ (BaseTy::Int(_) | BaseTy::Uint(_)), idx) => { + TyKind::Indexed(bty @ (BaseTy::Int(_) | BaseTy::Uint(_) | BaseTy::Char), idx) => { Expr::eq(idx.clone(), Expr::from_bits(bty, bits)) } _ => tracked_span_bug!("unexpected discr_ty {:?}", discr_ty), @@ -1486,7 +1488,10 @@ impl<'ck, 'genv, 'tcx, M: Mode> Checker<'ck, 'genv, 'tcx, M> { let idx = Expr::constant(rty::Constant::from(*s)); Ok(Ty::mk_ref(ReStatic, Ty::indexed(BaseTy::Str, idx), Mutability::Not)) } - Constant::Char => Ok(Ty::char()), + Constant::Char(c) => { + let idx = Expr::constant(rty::Constant::from(*c)); + Ok(Ty::indexed(BaseTy::Char, idx)) + } Constant::Param(param_const, ty) => { let idx = Expr::const_generic(*param_const); let ctor = self diff --git a/crates/flux-refineck/src/primops.rs b/crates/flux-refineck/src/primops.rs index 5e3712a281..7d58441871 100644 --- a/crates/flux-refineck/src/primops.rs +++ b/crates/flux-refineck/src/primops.rs @@ -1,3 +1,28 @@ +/// This file defines the refinement rules for primitive operations. +/// Flux needs to define how to reason about primitive operations on different +/// [`BaseTy`]s. This is done by defining a set of rules for each operation. +/// +/// For example, equality checks depend on whether the `BaseTy` is treated as +/// refineable or opaque. +/// +/// ``` +/// // Make the rules for `a == b`. +/// fn mk_eq_rules() -> RuleMatcher<2> { +/// primop_rules! { +/// // if the `BaseTy` is refineable, then we can reason about equality. +/// // The specified types in the `if` are refineable and Flux will use +/// // the refined postcondition (`bool[E::eq(a, b)]`) to reason about +/// // the invariants of `==`. +/// fn(a: T, b: T) -> bool[E::eq(a, b)] +/// if T.is_integral() || T.is_bool() || T.is_char() || T.is_str() +/// +/// // Otherwise, if the `BaseTy` is opaque, then we can't reason +/// // about equality. Flux only knows that the return type is a boolean, +/// // but the return value is unrefined. +/// fn(a: T, b: T) -> bool +/// } +/// } +/// ``` use std::{hash::Hash, sync::LazyLock}; use flux_common::tracked_span_bug; @@ -280,7 +305,7 @@ fn mk_bit_xor_rules() -> RuleMatcher<2> { fn mk_eq_rules() -> RuleMatcher<2> { primop_rules! { fn(a: T, b: T) -> bool[E::eq(a, b)] - if T.is_integral() || T.is_bool() + if T.is_integral() || T.is_bool() || T.is_char() || T.is_str() fn(a: T, b: T) -> bool } diff --git a/crates/flux-rustc-bridge/src/lowering.rs b/crates/flux-rustc-bridge/src/lowering.rs index 1a10af24e5..214fd2e232 100644 --- a/crates/flux-rustc-bridge/src/lowering.rs +++ b/crates/flux-rustc-bridge/src/lowering.rs @@ -646,6 +646,8 @@ impl<'sess, 'tcx> MirLoweringCtxt<'_, 'sess, 'tcx> { .ok_or_else(|| UnsupportedReason::new(format!("unsupported constant `{constant:?}`"))) } + /// A `ScalarInt` is just a set of bits that can represent any scalar value. + /// This can represent all the primitive types with a fixed size. fn scalar_int_to_constant( &self, scalar: rustc_ty::ScalarInt, @@ -663,7 +665,7 @@ impl<'sess, 'tcx> MirLoweringCtxt<'_, 'sess, 'tcx> { TyKind::Float(float_ty) => { Some(Constant::Float(scalar_to_bits(self.tcx, scalar, ty).unwrap(), *float_ty)) } - TyKind::Char => Some(Constant::Char), + TyKind::Char => Some(Constant::Char(scalar.try_into().unwrap())), TyKind::Bool => Some(Constant::Bool(scalar.try_to_bool().unwrap())), TyKind::Tuple(tys) if tys.is_empty() => Some(Constant::Unit), _ => { diff --git a/crates/flux-rustc-bridge/src/mir.rs b/crates/flux-rustc-bridge/src/mir.rs index b214ff8c92..0c77aac217 100644 --- a/crates/flux-rustc-bridge/src/mir.rs +++ b/crates/flux-rustc-bridge/src/mir.rs @@ -198,6 +198,7 @@ pub enum StatementKind { Nop, } +/// Corresponds to <https://doc.rust-lang.org/beta/nightly-rustc/rustc_middle/mir/enum.Rvalue.html> pub enum Rvalue { Use(Operand), Repeat(Operand, Const), @@ -341,8 +342,7 @@ pub enum Constant { Float(u128, FloatTy), Bool(bool), Str(Symbol), - /// We only support opaque chars, so no data stored here for now - Char, + Char(char), Unit, Param(ParamConst, Ty), /// General catch-all for constants of a given Ty @@ -750,7 +750,7 @@ impl fmt::Debug for Constant { Constant::Bool(b) => write!(f, "{b}"), Constant::Unit => write!(f, "()"), Constant::Str(s) => write!(f, "\"{s:?}\""), - Constant::Char => write!(f, "\"<opaque char>\""), + Constant::Char(c) => write!(f, "\'{c}\'"), Constant::Opaque(ty) => write!(f, "<opaque {:?}>", ty), Constant::Param(p, _) => write!(f, "{:?}", p), } diff --git a/tests/tests/pos/structs/enum-match-04.rs b/tests/tests/pos/structs/enum-match-04.rs new file mode 100644 index 0000000000..74a6a543f0 --- /dev/null +++ b/tests/tests/pos/structs/enum-match-04.rs @@ -0,0 +1,14 @@ +// match with different types +fn test00(flag: char) { + match flag { + 'l' => {}, + _ => {}, + } +} + +fn test01(flag: f32) { + match flag { + 0.0 => {}, + _ => {}, + } +} \ No newline at end of file diff --git a/tests/tests/pos/surface/char02.rs b/tests/tests/pos/surface/char02.rs new file mode 100644 index 0000000000..d74fb8a48c --- /dev/null +++ b/tests/tests/pos/surface/char02.rs @@ -0,0 +1,9 @@ +#[flux::sig(fn() -> char['a'])] +pub fn char00() -> char { + 'a' +} + +#[flux::sig(fn(c: char{v: 'a' <= v && v <= 'z'}) -> bool[true])] +pub fn lowercase(c: char) -> bool { + 'c' == 'c' +} diff --git a/tests/tests/pos/surface/str01.rs b/tests/tests/pos/surface/str01.rs index 2ef0fd7ffd..f87089d13e 100644 --- a/tests/tests/pos/surface/str01.rs +++ b/tests/tests/pos/surface/str01.rs @@ -1,8 +1,47 @@ +#![allow(dead_code)] + +use flux_rs::extern_spec; + pub fn str01() -> usize { let x = "str"; x.len() } -pub fn panic() { - panic!("a panic") +#[flux::sig(fn (&str["cat"]))] +fn require_cat(_x: &str) {} + +pub fn test_cat() { + require_cat("cat"); + // require_cat("dog"); //~ ERROR refinement type +} + +#[flux::sig(fn (&str[@a], &{str[@b] | a == b}))] +fn require_eq(_x: &str, _y: &str) {} + +pub fn test_eq() { + require_eq("a", "a"); + // require_eq("a", "b"); //~ ERROR refinement type +} + +/// PITFALL: The following function will fail to verify due to Flux implementation +/// details. Constant strings in the compiled binary will get parsed by `lower_constant` +/// in `lowering.rs`. The `Ty`pe of the constant string will be `&&str`. This is +/// due to constant promotion (https://github.com/rust-lang/const-eval/blob/master/promotion.md). +/// This is not a fundamental limitation in Flux, but is a current limitation in the +/// implementation. +pub fn identity() -> bool { + // "cat" == "cat" //~ FAILURE to verify + true +} + +#[extern_spec] +impl str { + #[flux::sig(fn(&str[@s]) -> usize[str_len(s)])] + fn len(s: &str) -> usize; } + +#[flux::sig(fn() -> usize[3])] +pub fn str_len_good() -> usize { + let x = "hog"; + x.len() +} \ No newline at end of file