Skip to content

Commit 037f292

Browse files
claudeclaude
committed
Construction support: array literal aggregates produce CHC array type
Handle AggregateKind::Array in rvalue_type(): fold store operations over a base existential to build a CHC array term with each element constrained to its concrete value. Elements are not boxed — they go directly into the array. For empty arrays, element type 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
1 parent 9d80a9b commit 037f292

3 files changed

Lines changed: 109 additions & 51 deletions

File tree

‎src/analyze/basic_block.rs‎

Lines changed: 91 additions & 51 deletions
Original file line numberDiff line numberDiff line change
@@ -482,7 +482,14 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
482482
if op == mir::UnOp::PtrMetadata {
483483
if let rty::Type::Pointer(ref ptr) = operand_ty.ty {
484484
if matches!(ptr.kind, rty::PointerKind::Ref(rty::RefKind::Immut))
485-
&& operand_ty.ty.as_pointer().unwrap().elem.ty.as_tuple().is_some()
485+
&& operand_ty
486+
.ty
487+
.as_pointer()
488+
.unwrap()
489+
.elem
490+
.ty
491+
.as_tuple()
492+
.is_some()
486493
{
487494
return operand_ty.deref().tuple_proj(1).deref();
488495
}
@@ -549,63 +556,93 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
549556
builder.build(rty::PointerType::immut_to(ty).into(), chc::Term::box_(term))
550557
}
551558
Rvalue::Aggregate(kind, fields) => {
552-
// elaboration: all fields are boxed
553-
let field_tys: Vec<_> = fields
554-
.into_iter()
555-
.map(|operand| self.operand_type(operand).boxed())
556-
.collect();
557559
match *kind {
558-
mir::AggregateKind::Adt(did, variant_idx, args, _, _)
559-
if self.tcx.def_kind(did) == DefKind::Enum =>
560-
{
561-
let enum_def = self.ctx.get_or_register_enum_def(did);
562-
let variant_def = &enum_def.variants[variant_idx];
563-
let variant_rtys = variant_def
564-
.field_tys
565-
.clone()
560+
mir::AggregateKind::Array(mir_elem_ty) => {
561+
// Elements go directly into the array — do not box them.
562+
let elem_ptys: Vec<_> = fields
566563
.into_iter()
567-
.map(|ty| rty::RefinedType::unrefined(ty.vacuous()));
568-
569-
let rty_args: IndexVec<_, _> = args
570-
.types()
571-
.map(|ty| {
572-
self.type_builder
573-
.for_template(&mut self.ctx)
574-
.with_scope(&self.env)
575-
.build_refined(ty)
576-
})
564+
.map(|operand| self.operand_type(operand))
577565
.collect();
578-
for (field_pty, mut variant_rty) in
579-
field_tys.clone().into_iter().zip(variant_rtys)
580-
{
581-
variant_rty.instantiate_ty_params(rty_args.clone());
582-
let cs = self
583-
.env
584-
.relate_sub_refined_type(&field_pty.into(), &variant_rty.boxed());
585-
self.ctx.extend_clauses(cs);
586-
}
587-
588-
let sort_args: Vec<_> =
589-
rty_args.iter().map(|rty| rty.ty.to_sort()).collect();
590-
let ty = rty::EnumType::new(enum_def.name.clone(), rty_args).into();
591-
592566
let mut builder = PlaceTypeBuilder::default();
593-
let mut field_terms = Vec::new();
594-
for field_ty in field_tys {
595-
let (_, field_term) = builder.subsume(field_ty);
596-
field_terms.push(field_term);
567+
let elem_ty = elem_ptys.first().map_or_else(
568+
|| self.type_builder.build(mir_elem_ty).vacuous(),
569+
|p| p.ty.clone(),
570+
);
571+
let base_idx = builder.push_existential(chc::Sort::array(
572+
chc::Sort::int(),
573+
elem_ty.to_sort(),
574+
));
575+
let mut arr_term: chc::Term<PlaceTypeVar> = chc::Term::var(base_idx.into());
576+
for (i, pty) in elem_ptys.into_iter().enumerate() {
577+
let (_, elem_term) = builder.subsume(pty);
578+
arr_term = arr_term.store(chc::Term::int(i as i64), elem_term);
597579
}
598580
builder.build(
599-
ty,
600-
chc::Term::datatype_ctor(
601-
enum_def.name,
602-
sort_args,
603-
variant_def.name.clone(),
604-
field_terms,
605-
),
581+
rty::ArrayType::new(rty::Type::int(), elem_ty).into(),
582+
arr_term,
606583
)
607584
}
608-
_ => PlaceType::tuple(field_tys),
585+
other => {
586+
// elaboration: all fields are boxed
587+
let field_tys: Vec<_> = fields
588+
.into_iter()
589+
.map(|operand| self.operand_type(operand).boxed())
590+
.collect();
591+
match other {
592+
mir::AggregateKind::Adt(did, variant_idx, args, _, _)
593+
if self.tcx.def_kind(did) == DefKind::Enum =>
594+
{
595+
let enum_def = self.ctx.get_or_register_enum_def(did);
596+
let variant_def = &enum_def.variants[variant_idx];
597+
let variant_rtys = variant_def
598+
.field_tys
599+
.clone()
600+
.into_iter()
601+
.map(|ty| rty::RefinedType::unrefined(ty.vacuous()));
602+
603+
let rty_args: IndexVec<_, _> = args
604+
.types()
605+
.map(|ty| {
606+
self.type_builder
607+
.for_template(&mut self.ctx)
608+
.with_scope(&self.env)
609+
.build_refined(ty)
610+
})
611+
.collect();
612+
for (field_pty, mut variant_rty) in
613+
field_tys.clone().into_iter().zip(variant_rtys)
614+
{
615+
variant_rty.instantiate_ty_params(rty_args.clone());
616+
let cs = self.env.relate_sub_refined_type(
617+
&field_pty.into(),
618+
&variant_rty.boxed(),
619+
);
620+
self.ctx.extend_clauses(cs);
621+
}
622+
623+
let sort_args: Vec<_> =
624+
rty_args.iter().map(|rty| rty.ty.to_sort()).collect();
625+
let ty = rty::EnumType::new(enum_def.name.clone(), rty_args).into();
626+
627+
let mut builder = PlaceTypeBuilder::default();
628+
let mut field_terms = Vec::new();
629+
for field_ty in field_tys {
630+
let (_, field_term) = builder.subsume(field_ty);
631+
field_terms.push(field_term);
632+
}
633+
builder.build(
634+
ty,
635+
chc::Term::datatype_ctor(
636+
enum_def.name,
637+
sort_args,
638+
variant_def.name.clone(),
639+
field_terms,
640+
),
641+
)
642+
}
643+
_ => PlaceType::tuple(field_tys),
644+
}
645+
}
609646
}
610647
}
611648
Rvalue::Cast(
@@ -649,7 +686,10 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
649686
// Static array [T; N]: length is the const N from the MIR type
650687
let mir_ty = place.ty(&self.local_decls, self.tcx).ty;
651688
let mir_ty::TyKind::Array(_, len_const) = mir_ty.kind() else {
652-
unimplemented!("Rvalue::Len: Array model type but MIR type is {:?}", mir_ty)
689+
unimplemented!(
690+
"Rvalue::Len: Array model type but MIR type is {:?}",
691+
mir_ty
692+
)
653693
};
654694
let n = len_const
655695
.try_to_target_usize(self.tcx)

‎tests/ui/fail/array_literal_1.rs‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
//@error-in-other-file: Unsat
2+
//@compile-flags: -C debug-assertions=off
3+
4+
fn main() {
5+
let arr = [1i32, 2, 3];
6+
let s: &[i32] = &arr;
7+
let v = s[0];
8+
assert!(v == 99);
9+
}

‎tests/ui/pass/array_literal_1.rs‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
//@check-pass
2+
//@compile-flags: -C debug-assertions=off
3+
4+
fn main() {
5+
let arr = [1i32, 2, 3];
6+
let s: &[i32] = &arr;
7+
let v = s[0];
8+
assert!(v == 1);
9+
}

0 commit comments

Comments
 (0)