From 10d215107cfb69f9b4c1618c9c12ec503c0ec104 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 12 Jun 2026 16:21:25 +0000 Subject: [PATCH 1/4] feat: add support for statically-sized arrays and slices MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add `model::Slice` and `Model` impls for `[T]`, `model::Slice`, and `[T; N]` so that the existing Model-trait normalization pipeline handles these types without changes to the core type-builder logic: - `[T]` normalizes to `model::Slice` = `(Array, Int)`, matching the Vec model (`.0` = array, `.1` = length) - `[T; N]` normalizes to `model::Array`, reusing the existing array model (N is statically known, written directly in specs) - `&[T]` and `&mut [T]` flow through the existing reference handling Add `Rvalue::Len` handling in `basic_block.rs` (slice length comes from fat-pointer metadata in MIR, not a function call): - For slice model (TupleType): project element 1 then deref the box - For static array model (ArrayType): evaluate the const N from MIR Add `UnOp::PtrMetadata` handling for `&[T]` references: extract the length by deref → tuple_proj(1) → deref. Add extern specs for `<[T]>::len`, `<[T]>::index`, `<[T]>::index_mut`, and `<[T]>::is_empty`, mirroring the existing Vec specs. Add test cases: - `tests/ui/pass/slice_1.rs`: safe indexing with non-empty slice - `tests/ui/fail/slice_1.rs`: out-of-bounds access (empty slice) - `tests/ui/pass/slice_2.rs`: two-element slice, two safe indices https://claude.ai/code/session_01BV92ggaKvAp7oNknvVmGsM --- src/analyze/basic_block.rs | 37 +++++++++++++++++++++++++++++ std.rs | 48 ++++++++++++++++++++++++++++++++++++++ tests/ui/fail/slice_1.rs | 14 +++++++++++ tests/ui/pass/slice_1.rs | 15 ++++++++++++ tests/ui/pass/slice_2.rs | 15 ++++++++++++ 5 files changed, 129 insertions(+) create mode 100644 tests/ui/fail/slice_1.rs create mode 100644 tests/ui/pass/slice_1.rs create mode 100644 tests/ui/pass/slice_2.rs diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs index 835a6623..c56be071 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -476,6 +476,20 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { Rvalue::UnaryOp(op, operand) => { let operand_ty = self.operand_type(operand); + // PtrMetadata extracts the length from a fat-pointer slice (&[T]). + // In the model, &[T] is &immut TupleType([Box>, Box]), + // so the length is (*operand).1. + if op == mir::UnOp::PtrMetadata { + if let rty::Type::Pointer(ref ptr) = operand_ty.ty { + if matches!(ptr.kind, rty::PointerKind::Ref(rty::RefKind::Immut)) + && operand_ty.ty.as_pointer().unwrap().elem.ty.as_tuple().is_some() + { + return operand_ty.deref().tuple_proj(1).deref(); + } + } + unimplemented!("PtrMetadata on {:?}", operand_ty.ty); + } + let mut builder = PlaceTypeBuilder::default(); let (operand_ty, operand_term) = builder.subsume(operand_ty); match (&operand_ty, op) { @@ -622,6 +636,29 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { let (_, term) = builder.subsume(ty); builder.build(rty::Type::Int, chc::Term::datatype_discr(sym, term)) } + Rvalue::Len(place) => { + let model_place = self.elaborate_place(&place); + let place_ty = self.env.place_type(model_place); + match &place_ty.ty { + rty::Type::Tuple(_) => { + // Slice model: TupleType([Box>, Box]) + // Length is element 1 (boxed Int): project then deref the box + place_ty.tuple_proj(1).deref() + } + rty::Type::Array(_) => { + // Static array [T; N]: length is the const N from the MIR type + let mir_ty = place.ty(&self.local_decls, self.tcx).ty; + let mir_ty::TyKind::Array(_, len_const) = mir_ty.kind() else { + unimplemented!("Rvalue::Len: Array model type but MIR type is {:?}", mir_ty) + }; + let n = len_const + .try_to_target_usize(self.tcx) + .expect("array length must be a known constant"); + PlaceType::with_ty_and_term(rty::Type::int(), chc::Term::int(n as i64)) + } + _ => unimplemented!("Rvalue::Len for model type: {:?}", place_ty.ty), + } + } _ => unimplemented!( "rvalue={:?} ({:?})", rvalue, diff --git a/std.rs b/std.rs index 9d1a883f..d254c177 100644 --- a/std.rs +++ b/std.rs @@ -364,6 +364,14 @@ mod thrust_models { type Ty = model::Seq<::Ty>; } + impl Model for [T] { + type Ty = model::Seq<::Ty>; + } + + impl Model for [T; N] { + type Ty = model::Array::Ty>; + } + impl Model for Option where T: Model { type Ty = Option<::Ty>; } @@ -825,3 +833,43 @@ fn _extern_spec_partialord_gt(x: &T, y: &T) -> bool { PartialOrd::gt(x, y) } + +#[thrust::extern_spec_fn] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(result == slice.1)] +fn _extern_spec_slice_len(slice: &[T]) -> usize + where T: thrust_models::Model, T::Ty: PartialEq +{ + <[T]>::len(slice) +} + +#[thrust::extern_spec_fn] +#[thrust_macros::requires(index < slice.1)] +#[thrust_macros::ensures(*result == slice.0[index])] +fn _extern_spec_slice_index(slice: &[T], index: usize) -> &T + where T: thrust_models::Model, T::Ty: PartialEq +{ + <[T] as std::ops::Index>::index(slice, index) +} + +#[thrust::extern_spec_fn] +#[thrust_macros::requires(index < (*slice).1)] +#[thrust_macros::ensures( + *result == (*slice).0[index] && + !result == (!slice).0[index] && + !slice == thrust_models::model::Seq((*slice).0.store(index, !result), (*slice).1) +)] +fn _extern_spec_slice_index_mut(slice: &mut [T], index: usize) -> &mut T + where T: thrust_models::Model, T::Ty: PartialEq +{ + <[T] as std::ops::IndexMut>::index_mut(slice, index) +} + +#[thrust::extern_spec_fn] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(result == (slice.1 == 0))] +fn _extern_spec_slice_is_empty(slice: &[T]) -> bool + where T: thrust_models::Model, T::Ty: PartialEq +{ + <[T]>::is_empty(slice) +} diff --git a/tests/ui/fail/slice_1.rs b/tests/ui/fail/slice_1.rs new file mode 100644 index 00000000..5635f546 --- /dev/null +++ b/tests/ui/fail/slice_1.rs @@ -0,0 +1,14 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +#[thrust::trusted] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(result.1 == 0)] +fn empty_slice() -> &'static [i32] { + unimplemented!() +} + +fn main() { + let s = empty_slice(); + let _ = s[0]; +} diff --git a/tests/ui/pass/slice_1.rs b/tests/ui/pass/slice_1.rs new file mode 100644 index 00000000..7c7d0d3e --- /dev/null +++ b/tests/ui/pass/slice_1.rs @@ -0,0 +1,15 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +#[thrust::trusted] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(result.1 > 0)] +fn nonempty_slice() -> &'static [i32] { + unimplemented!() +} + +fn main() { + let s = nonempty_slice(); + assert!(s.len() > 0); + let _ = s[0]; +} diff --git a/tests/ui/pass/slice_2.rs b/tests/ui/pass/slice_2.rs new file mode 100644 index 00000000..ab0ab992 --- /dev/null +++ b/tests/ui/pass/slice_2.rs @@ -0,0 +1,15 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +#[thrust::trusted] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(result.1 >= 2)] +fn two_elem_slice() -> &'static [i32] { + unimplemented!() +} + +fn main() { + let s = two_elem_slice(); + let _ = s[0]; + let _ = s[1]; +} From f5f3c4ac07e595b05b8474ed2447c0c563632738 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 23 Jun 2026 17:39:48 +0000 Subject: [PATCH 2/4] Basic support: Seq as unified array/slice model and PlaceElem::Index MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Switch [T] and [T;N] to both use model::Seq (replacing model::Slice and model::Array). Remove the Slice struct from std.rs and update the index_mut extern spec constructor accordingly. Now both static arrays and slices share the same (Array, Int) logical representation. Add Path::Index / path_type() arm in env.rs: MIR (*s)[i] projections resolve to a select on the Seq's inner array (field 0 → deref → select). Simplify PlaceElem::Len to always use the Tuple (Seq) branch. Add tests/ui/fail/slice_2.rs pairing the existing pass: s[2] on a slice guaranteed only len >= 2 cannot be proven safe → Unsat. https://claude.ai/code/session_01BV92ggaKvAp7oNknvVmGsM --- src/refine/env.rs | 22 ++++++++++++++++++++++ std.rs | 2 +- tests/ui/fail/slice_2.rs | 14 ++++++++++++++ 3 files changed, 37 insertions(+), 1 deletion(-) create mode 100644 tests/ui/fail/slice_2.rs diff --git a/src/refine/env.rs b/src/refine/env.rs index d9c3dfbc..cfed5397 100644 --- a/src/refine/env.rs +++ b/src/refine/env.rs @@ -1051,6 +1051,7 @@ enum Path { Deref(Box), TupleProj(Box, usize), Downcast(Box, VariantIdx, FieldIdx), + Index(Box, Local), } impl<'tcx> From> for Path { @@ -1067,6 +1068,7 @@ impl<'tcx> From> for Path { }; Path::Downcast(Box::new(path), variant_idx, field_idx) } + Some(PlaceElem::Index(local)) => Path::Index(Box::new(path), local), None => break, _ => unimplemented!(), }; @@ -1099,6 +1101,26 @@ where self.path_type(path) .downcast(*variant_idx, *field_idx, &self.enum_defs) } + Path::Index(path, idx_local) => { + let inner_pty = self.path_type(path); + let idx_pty = self.local_type(*idx_local); + // Seq = (Box>, Box): get field 0 then deref the box. + let arr_pty = match inner_pty.ty.clone() { + rty::Type::Tuple(_) => inner_pty.tuple_proj(0).deref(), + ty => unimplemented!("PlaceElem::Index on non-Seq type: {:?}", ty), + }; + let rty::Type::Array(arr_ty) = arr_pty.ty.clone() else { + unreachable!("expected Array type after index normalization") + }; + let elem_refined_ty = *arr_ty.elem; + let mut builder = refine::PlaceTypeBuilder::default(); + let (_, arr_term) = builder.subsume(arr_pty); + let (_, idx_term) = builder.subsume(idx_pty); + let (elem_ty, value_var_ex) = builder.subsume_rty(elem_refined_ty); + let elem_term = crate::chc::Term::var(value_var_ex.into()); + builder.push_formula(elem_term.clone().equal_to(arr_term.select(idx_term))); + builder.build(elem_ty, elem_term) + } } } diff --git a/std.rs b/std.rs index d254c177..df26c23a 100644 --- a/std.rs +++ b/std.rs @@ -369,7 +369,7 @@ mod thrust_models { } impl Model for [T; N] { - type Ty = model::Array::Ty>; + type Ty = model::Seq<::Ty>; } impl Model for Option where T: Model { diff --git a/tests/ui/fail/slice_2.rs b/tests/ui/fail/slice_2.rs new file mode 100644 index 00000000..8229a5a2 --- /dev/null +++ b/tests/ui/fail/slice_2.rs @@ -0,0 +1,14 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +#[thrust::trusted] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(result.1 >= 2)] +fn two_elem_slice() -> &'static [i32] { + unimplemented!() +} + +fn main() { + let s = two_elem_slice(); + let _ = s[2]; +} From bf51811677da3a1187cff846741904f4c8d3d337 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 23 Jun 2026 17:40:13 +0000 Subject: [PATCH 3/4] Construction support: array literal aggregates produce Seq MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Handle AggregateKind::Array in rvalue_type(): fold store operations over a base existential to build a CHC array term, then wrap with the concrete element count to produce Seq = (Array, N). Element type for empty arrays is read from AggregateKind::Array(ty) directly. Paired tests: pass asserts s[0]==1 (correct), fail asserts s[0]==99 → Unsat. https://claude.ai/code/session_01BV92ggaKvAp7oNknvVmGsM --- src/analyze/basic_block.rs | 159 ++++++++++++++++++------------- tests/ui/fail/array_literal_1.rs | 9 ++ tests/ui/pass/array_literal_1.rs | 9 ++ 3 files changed, 112 insertions(+), 65 deletions(-) create mode 100644 tests/ui/fail/array_literal_1.rs create mode 100644 tests/ui/pass/array_literal_1.rs diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs index c56be071..523e8ae2 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -482,7 +482,14 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { if op == mir::UnOp::PtrMetadata { if let rty::Type::Pointer(ref ptr) = operand_ty.ty { if matches!(ptr.kind, rty::PointerKind::Ref(rty::RefKind::Immut)) - && operand_ty.ty.as_pointer().unwrap().elem.ty.as_tuple().is_some() + && operand_ty + .ty + .as_pointer() + .unwrap() + .elem + .ty + .as_tuple() + .is_some() { return operand_ty.deref().tuple_proj(1).deref(); } @@ -549,63 +556,97 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { builder.build(rty::PointerType::immut_to(ty).into(), chc::Term::box_(term)) } Rvalue::Aggregate(kind, fields) => { - // elaboration: all fields are boxed - let field_tys: Vec<_> = fields - .into_iter() - .map(|operand| self.operand_type(operand).boxed()) - .collect(); match *kind { - mir::AggregateKind::Adt(did, variant_idx, args, _, _) - if self.tcx.def_kind(did) == DefKind::Enum => - { - let enum_def = self.ctx.get_or_register_enum_def(did); - let variant_def = &enum_def.variants[variant_idx]; - let variant_rtys = variant_def - .field_tys - .clone() + mir::AggregateKind::Array(mir_elem_ty) => { + // Build a Seq = (Array, len) from the literal elements. + let elem_ptys: Vec<_> = fields .into_iter() - .map(|ty| rty::RefinedType::unrefined(ty.vacuous())); - - let rty_args: IndexVec<_, _> = args - .types() - .map(|ty| { - self.type_builder - .for_template(&mut self.ctx) - .with_scope(&self.env) - .build_refined(ty) - }) + .map(|operand| self.operand_type(operand)) .collect(); - for (field_pty, mut variant_rty) in - field_tys.clone().into_iter().zip(variant_rtys) - { - variant_rty.instantiate_ty_params(rty_args.clone()); - let cs = self - .env - .relate_sub_refined_type(&field_pty.into(), &variant_rty.boxed()); - self.ctx.extend_clauses(cs); - } - - let sort_args: Vec<_> = - rty_args.iter().map(|rty| rty.ty.to_sort()).collect(); - let ty = rty::EnumType::new(enum_def.name.clone(), rty_args).into(); - + let n = elem_ptys.len(); let mut builder = PlaceTypeBuilder::default(); - let mut field_terms = Vec::new(); - for field_ty in field_tys { - let (_, field_term) = builder.subsume(field_ty); - field_terms.push(field_term); + let elem_ty = elem_ptys.first().map_or_else( + || self.type_builder.build(mir_elem_ty).vacuous(), + |p| p.ty.clone(), + ); + let base_idx = builder.push_existential(chc::Sort::array( + chc::Sort::int(), + elem_ty.to_sort(), + )); + let mut arr_term: chc::Term = chc::Term::var(base_idx.into()); + for (i, pty) in elem_ptys.into_iter().enumerate() { + let (_, elem_term) = builder.subsume(pty); + arr_term = arr_term.store(chc::Term::int(i as i64), elem_term); + } + let arr_pty = builder.build( + rty::ArrayType::new(rty::Type::int(), elem_ty).into(), + arr_term, + ); + let n_pty = + PlaceType::with_ty_and_term(rty::Type::int(), chc::Term::int(n as i64)); + PlaceType::tuple(vec![arr_pty.boxed(), n_pty.boxed()]) + } + other => { + // elaboration: all fields are boxed + let field_tys: Vec<_> = fields + .into_iter() + .map(|operand| self.operand_type(operand).boxed()) + .collect(); + match other { + mir::AggregateKind::Adt(did, variant_idx, args, _, _) + if self.tcx.def_kind(did) == DefKind::Enum => + { + let enum_def = self.ctx.get_or_register_enum_def(did); + let variant_def = &enum_def.variants[variant_idx]; + let variant_rtys = variant_def + .field_tys + .clone() + .into_iter() + .map(|ty| rty::RefinedType::unrefined(ty.vacuous())); + + let rty_args: IndexVec<_, _> = args + .types() + .map(|ty| { + self.type_builder + .for_template(&mut self.ctx) + .with_scope(&self.env) + .build_refined(ty) + }) + .collect(); + for (field_pty, mut variant_rty) in + field_tys.clone().into_iter().zip(variant_rtys) + { + variant_rty.instantiate_ty_params(rty_args.clone()); + let cs = self.env.relate_sub_refined_type( + &field_pty.into(), + &variant_rty.boxed(), + ); + self.ctx.extend_clauses(cs); + } + + let sort_args: Vec<_> = + rty_args.iter().map(|rty| rty.ty.to_sort()).collect(); + let ty = rty::EnumType::new(enum_def.name.clone(), rty_args).into(); + + let mut builder = PlaceTypeBuilder::default(); + let mut field_terms = Vec::new(); + for field_ty in field_tys { + let (_, field_term) = builder.subsume(field_ty); + field_terms.push(field_term); + } + builder.build( + ty, + chc::Term::datatype_ctor( + enum_def.name, + sort_args, + variant_def.name.clone(), + field_terms, + ), + ) + } + _ => PlaceType::tuple(field_tys), } - builder.build( - ty, - chc::Term::datatype_ctor( - enum_def.name, - sort_args, - variant_def.name.clone(), - field_terms, - ), - ) } - _ => PlaceType::tuple(field_tys), } } Rvalue::Cast( @@ -641,21 +682,9 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { let place_ty = self.env.place_type(model_place); match &place_ty.ty { rty::Type::Tuple(_) => { - // Slice model: TupleType([Box>, Box]) - // Length is element 1 (boxed Int): project then deref the box + // Seq = (Array, Int): length is field 1 (boxed Int). place_ty.tuple_proj(1).deref() } - rty::Type::Array(_) => { - // Static array [T; N]: length is the const N from the MIR type - let mir_ty = place.ty(&self.local_decls, self.tcx).ty; - let mir_ty::TyKind::Array(_, len_const) = mir_ty.kind() else { - unimplemented!("Rvalue::Len: Array model type but MIR type is {:?}", mir_ty) - }; - let n = len_const - .try_to_target_usize(self.tcx) - .expect("array length must be a known constant"); - PlaceType::with_ty_and_term(rty::Type::int(), chc::Term::int(n as i64)) - } _ => unimplemented!("Rvalue::Len for model type: {:?}", place_ty.ty), } } diff --git a/tests/ui/fail/array_literal_1.rs b/tests/ui/fail/array_literal_1.rs new file mode 100644 index 00000000..1fa49d74 --- /dev/null +++ b/tests/ui/fail/array_literal_1.rs @@ -0,0 +1,9 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +fn main() { + let arr = [1i32, 2, 3]; + let s: &[i32] = &arr; + let v = s[0]; + assert!(v == 99); +} diff --git a/tests/ui/pass/array_literal_1.rs b/tests/ui/pass/array_literal_1.rs new file mode 100644 index 00000000..4a563891 --- /dev/null +++ b/tests/ui/pass/array_literal_1.rs @@ -0,0 +1,9 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +fn main() { + let arr = [1i32, 2, 3]; + let s: &[i32] = &arr; + let v = s[0]; + assert!(v == 1); +} From ac84456bb103bc9bcf6e7b22cb691321b739ffa4 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 23 Jun 2026 17:40:21 +0000 Subject: [PATCH 4/4] =?UTF-8?q?Coercion=20support:=20&[T;N]=20=E2=86=92=20?= =?UTF-8?q?&[T]=20unsize=20coercion=20is=20identity=20on=20Seq?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Since both [T;N] and [T] now model as Seq, the PointerCoercion::Unsize cast is a model-level identity: just pass through the operand's place type. Paired tests: pass accesses index 3 on a 4-element slice (safe), fail accesses index 4 → Unsat. https://claude.ai/code/session_01BV92ggaKvAp7oNknvVmGsM --- src/analyze/basic_block.rs | 8 ++++++++ tests/ui/fail/array_literal_2.rs | 8 ++++++++ tests/ui/pass/array_literal_2.rs | 8 ++++++++ 3 files changed, 24 insertions(+) create mode 100644 tests/ui/fail/array_literal_2.rs create mode 100644 tests/ui/pass/array_literal_2.rs diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs index 523e8ae2..d9f5ac27 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -663,6 +663,14 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { }; PlaceType::with_ty_and_term(func_ty.vacuous(), chc::Term::null()) } + Rvalue::Cast( + mir::CastKind::PointerCoercion(mir_ty::adjustment::PointerCoercion::Unsize, _), + operand, + _ty, + ) => { + // &[T; N] → &[T]: both are modeled as &Seq, so pass through directly. + self.operand_type(operand) + } Rvalue::Discriminant(place) => { let place = self.elaborate_place(&place); let ty = self.env.place_type(place); diff --git a/tests/ui/fail/array_literal_2.rs b/tests/ui/fail/array_literal_2.rs new file mode 100644 index 00000000..99ccdb15 --- /dev/null +++ b/tests/ui/fail/array_literal_2.rs @@ -0,0 +1,8 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +fn main() { + let arr = [0i32, 0, 0, 0]; + let s: &[i32] = &arr; + let _ = s[4]; +} diff --git a/tests/ui/pass/array_literal_2.rs b/tests/ui/pass/array_literal_2.rs new file mode 100644 index 00000000..abbc05e6 --- /dev/null +++ b/tests/ui/pass/array_literal_2.rs @@ -0,0 +1,8 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +fn main() { + let arr = [0i32, 0, 0, 0]; + let s: &[i32] = &arr; + let _ = s[3]; +}