From e1783942e16c04ba32216028b6a7c9c59eda00d4 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 29 Jun 2026 05:30:28 +0000 Subject: [PATCH 1/3] Add array literal construction Handle `Rvalue::Aggregate(Array, ...)` by building a Seq model (Box>, Box) whose array component is the store-fold of all literal elements and whose length is the static count N. Also handle `mir::Const::Ty` (type-level constants, e.g. array length N) by extracting the scalar integer and delegating to `const_value_ty`. Map `[T; N]` to `model::Seq` in `std.rs`, matching `[T]` and `Vec`. Co-Authored-By: Claude Sonnet 4.6 Claude-Session: https://claude.ai/code/session_013oVufAKCMzsLRnQ8F58PdP --- src/analyze/basic_block.rs | 145 ++++++++++++++++++++++++------------- std.rs | 4 + 2 files changed, 97 insertions(+), 52 deletions(-) diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs index d497a4a5..f02385f7 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -454,7 +454,13 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { .unwrap(); self.const_value_ty(&val, ty) } - _ => unimplemented!("const: {:?}", const_), + mir::Const::Ty(ty, _) => { + let scalar_int = const_ + .try_to_scalar_int() + .expect("type-level const must be a primitive scalar"); + let val = mir::ConstValue::Scalar(mir::interpret::Scalar::Int(scalar_int)); + self.const_value_ty(&val, ty) + } } } @@ -535,63 +541,98 @@ 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 Seq = (Box>, Box) from array literal elements, + // pinning each element at its index via store folds. + 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( diff --git a/std.rs b/std.rs index 32525a2b..8d7337b0 100644 --- a/std.rs +++ b/std.rs @@ -368,6 +368,10 @@ mod thrust_models { type Ty = model::Seq<::Ty>; } + impl Model for [T; N] { + type Ty = model::Seq<::Ty>; + } + impl Model for Option where T: Model { type Ty = Option<::Ty>; } From 33660111cb5d884f299a009f2cdb864c421fae93 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 29 Jun 2026 05:44:27 +0000 Subject: [PATCH 2/3] Add array-to-slice coercion and slice indexing Support the MIR operations needed to turn `[T; N]` into `&[T]` and index it: - `Rvalue::CopyForDeref`: pass-through to the place type (coerce-for-deref). - `Rvalue::Cast(PointerCoercion::Unsize)`: identity coercion since `[T; N]` and `[T]` share the same `Seq` model. Fix a bug in `remove_bounds_check_setup` where the slice receiver local was incorrectly NOP'd when `PtrMetadata` was applied directly to it. The receiver must remain live for the reconstructed `Index::index` call. Co-Authored-By: Claude Sonnet 4.6 Claude-Session: https://claude.ai/code/session_013oVufAKCMzsLRnQ8F58PdP --- src/analyze/basic_block.rs | 10 ++++++++++ src/analyze/reconstruct_slice_indexing.rs | 16 +++++++++++++--- tests/ui/fail/array_literal_1.rs | 9 +++++++++ tests/ui/fail/array_literal_2.rs | 8 ++++++++ tests/ui/fail/array_literal_3.rs | 9 +++++++++ tests/ui/pass/array_literal_1.rs | 9 +++++++++ tests/ui/pass/array_literal_2.rs | 8 ++++++++ tests/ui/pass/array_literal_3.rs | 10 ++++++++++ 8 files changed, 76 insertions(+), 3 deletions(-) create mode 100644 tests/ui/fail/array_literal_1.rs create mode 100644 tests/ui/fail/array_literal_2.rs create mode 100644 tests/ui/fail/array_literal_3.rs create mode 100644 tests/ui/pass/array_literal_1.rs create mode 100644 tests/ui/pass/array_literal_2.rs create mode 100644 tests/ui/pass/array_literal_3.rs diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs index f02385f7..4a3ecca2 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -479,6 +479,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { fn rvalue_type(&mut self, rvalue: Rvalue<'tcx>) -> PlaceType { match rvalue { Rvalue::Use(operand) => self.operand_type(operand), + Rvalue::CopyForDeref(place) => self.env.place_type(self.elaborate_place(&place)), Rvalue::UnaryOp(op, operand) => { let operand_ty = self.operand_type(operand); @@ -649,6 +650,15 @@ 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] and similar unsizings: both sides share the same Seq model, + // so the coercion is identity. + self.operand_type(operand) + } Rvalue::Discriminant(place) => { let place = self.elaborate_place(&place); let ty = self.env.place_type(place); diff --git a/src/analyze/reconstruct_slice_indexing.rs b/src/analyze/reconstruct_slice_indexing.rs index b600cd2a..0e92c911 100644 --- a/src/analyze/reconstruct_slice_indexing.rs +++ b/src/analyze/reconstruct_slice_indexing.rs @@ -269,7 +269,7 @@ fn reconstruct_access<'tcx>( result_local, ); let receiver = receiver_operand(tcx, body, &bounds_check, &access, region); - remove_bounds_check_setup(body, &bounds_check); + remove_bounds_check_setup(body, &bounds_check, access.receiver.local); let (lang_item, method_name) = if access.mutable { (LangItem::IndexMut, sym::index_mut) @@ -358,7 +358,11 @@ fn receiver_operand<'tcx>( } /// Removes the MIR temporaries that only supported the now-replaced bounds check. -fn remove_bounds_check_setup<'tcx>(body: &mut Body<'tcx>, bounds_check: &BoundsCheck<'tcx>) { +fn remove_bounds_check_setup<'tcx>( + body: &mut Body<'tcx>, + bounds_check: &BoundsCheck<'tcx>, + receiver_local: Local, +) { let mut lowered_locals: Vec<_> = bounds_check.condition_local.into_iter().collect(); if let Some(len_place) = bounds_check .len @@ -373,7 +377,13 @@ fn remove_bounds_check_setup<'tcx>(body: &mut Body<'tcx>, bounds_check: &BoundsC continue; }; if lhs.local == len_place.local { - if let Some(raw_place) = operand.place().filter(|place| place.projection.is_empty()) + // Only include the PtrMetadata operand if it is a distinct temporary — i.e. + // not the receiver that the reconstructed Index::index call will use. + // When PtrMetadata is applied directly to the slice reference (the receiver), + // that local must not be NOP'd: its assignment may be in this same block. + if let Some(raw_place) = operand + .place() + .filter(|place| place.projection.is_empty() && place.local != receiver_local) { lowered_locals.push(raw_place.local); } 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/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/fail/array_literal_3.rs b/tests/ui/fail/array_literal_3.rs new file mode 100644 index 00000000..dc085982 --- /dev/null +++ b/tests/ui/fail/array_literal_3.rs @@ -0,0 +1,9 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +fn main() { + let mut arr = [1i32, 2, 3]; + let s: &mut [i32] = &mut arr; + s[0] = 42; + assert!(s[0] == 1); // old value → Unsat +} 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); +} 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]; +} diff --git a/tests/ui/pass/array_literal_3.rs b/tests/ui/pass/array_literal_3.rs new file mode 100644 index 00000000..10f29014 --- /dev/null +++ b/tests/ui/pass/array_literal_3.rs @@ -0,0 +1,10 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +fn main() { + let mut arr = [1i32, 2, 3]; + let s: &mut [i32] = &mut arr; + s[0] = 42; + assert!(s[0] == 42); + assert!(s[1] == 2); +} From 86e1be87a4d1c160fa1ce09eb631f0798fad8967 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 29 Jun 2026 05:44:49 +0000 Subject: [PATCH 3/3] Add Vec-to-slice coercion extern specs Specify the postcondition `*result == *vec` for the three ways a `Vec` can be coerced to `&[T]`: `as_slice`, `Deref::deref`, and `AsRef::as_ref`. This lets the refinement checker treat all three as preserving the Seq model. Co-Authored-By: Claude Sonnet 4.6 Claude-Session: https://claude.ai/code/session_013oVufAKCMzsLRnQ8F58PdP --- std.rs | 27 +++++++++++++++++++++++++++ tests/ui/fail/vec_as_ref.rs | 10 ++++++++++ tests/ui/fail/vec_as_slice.rs | 10 ++++++++++ tests/ui/fail/vec_deref.rs | 10 ++++++++++ tests/ui/pass/vec_as_ref.rs | 12 ++++++++++++ tests/ui/pass/vec_as_slice.rs | 12 ++++++++++++ tests/ui/pass/vec_deref.rs | 12 ++++++++++++ 7 files changed, 93 insertions(+) create mode 100644 tests/ui/fail/vec_as_ref.rs create mode 100644 tests/ui/fail/vec_as_slice.rs create mode 100644 tests/ui/fail/vec_deref.rs create mode 100644 tests/ui/pass/vec_as_ref.rs create mode 100644 tests/ui/pass/vec_as_slice.rs create mode 100644 tests/ui/pass/vec_deref.rs diff --git a/std.rs b/std.rs index 8d7337b0..20a41c4f 100644 --- a/std.rs +++ b/std.rs @@ -804,6 +804,33 @@ fn _extern_spec_vec_truncate(vec: &mut Vec, len: usize) where T: thrust_mo Vec::truncate(vec, len) } +#[thrust::extern_spec_fn] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(*result == *vec)] +fn _extern_spec_vec_as_slice(vec: &Vec) -> &[T] + where T: thrust_models::Model, T::Ty: PartialEq +{ + Vec::as_slice(vec) +} + +#[thrust::extern_spec_fn] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(*result == *vec)] +fn _extern_spec_vec_deref(vec: &Vec) -> &[T] + where T: thrust_models::Model, T::Ty: PartialEq +{ + as std::ops::Deref>::deref(vec) +} + +#[thrust::extern_spec_fn] +#[thrust_macros::requires(true)] +#[thrust_macros::ensures(*result == *vec)] +fn _extern_spec_vec_as_ref(vec: &Vec) -> &[T] + where T: thrust_models::Model, T::Ty: PartialEq +{ + as AsRef<[T]>>::as_ref(vec) +} + #[thrust::extern_spec_fn] #[thrust_macros::requires(true)] #[thrust_macros::ensures(result == slice.1)] diff --git a/tests/ui/fail/vec_as_ref.rs b/tests/ui/fail/vec_as_ref.rs new file mode 100644 index 00000000..9e87c0fb --- /dev/null +++ b/tests/ui/fail/vec_as_ref.rs @@ -0,0 +1,10 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +fn main() { + let mut v: Vec = Vec::new(); + Vec::push(&mut v, 10); + Vec::push(&mut v, 20); + let s: &[i32] = v.as_ref(); + assert!(s[0] == 99); // wrong value → Unsat +} diff --git a/tests/ui/fail/vec_as_slice.rs b/tests/ui/fail/vec_as_slice.rs new file mode 100644 index 00000000..6726e985 --- /dev/null +++ b/tests/ui/fail/vec_as_slice.rs @@ -0,0 +1,10 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +fn main() { + let mut v: Vec = Vec::new(); + Vec::push(&mut v, 10); + Vec::push(&mut v, 20); + let s = Vec::as_slice(&v); + assert!(s[0] == 99); // wrong value → Unsat +} diff --git a/tests/ui/fail/vec_deref.rs b/tests/ui/fail/vec_deref.rs new file mode 100644 index 00000000..57852710 --- /dev/null +++ b/tests/ui/fail/vec_deref.rs @@ -0,0 +1,10 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +fn main() { + let mut v: Vec = Vec::new(); + Vec::push(&mut v, 10); + Vec::push(&mut v, 20); + let s: &[i32] = &v; + assert!(s[0] == 99); // wrong value → Unsat +} diff --git a/tests/ui/pass/vec_as_ref.rs b/tests/ui/pass/vec_as_ref.rs new file mode 100644 index 00000000..81b37c67 --- /dev/null +++ b/tests/ui/pass/vec_as_ref.rs @@ -0,0 +1,12 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +fn main() { + let mut v: Vec = Vec::new(); + Vec::push(&mut v, 10); + Vec::push(&mut v, 20); + let s: &[i32] = v.as_ref(); + assert!(s.len() == 2); + assert!(s[0] == 10); + assert!(s[1] == 20); +} diff --git a/tests/ui/pass/vec_as_slice.rs b/tests/ui/pass/vec_as_slice.rs new file mode 100644 index 00000000..4ac4b05a --- /dev/null +++ b/tests/ui/pass/vec_as_slice.rs @@ -0,0 +1,12 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +fn main() { + let mut v: Vec = Vec::new(); + Vec::push(&mut v, 10); + Vec::push(&mut v, 20); + let s = Vec::as_slice(&v); + assert!(s.len() == 2); + assert!(s[0] == 10); + assert!(s[1] == 20); +} diff --git a/tests/ui/pass/vec_deref.rs b/tests/ui/pass/vec_deref.rs new file mode 100644 index 00000000..54b3e760 --- /dev/null +++ b/tests/ui/pass/vec_deref.rs @@ -0,0 +1,12 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +fn main() { + let mut v: Vec = Vec::new(); + Vec::push(&mut v, 10); + Vec::push(&mut v, 20); + let s: &[i32] = &v; + assert!(s.len() == 2); + assert!(s[0] == 10); + assert!(s[1] == 20); +}