Skip to content

Commit 66f3d32

Browse files
utaalutaal
authored
Merge pull request rust-lang#20 from Chris-Hawblitzel/unit-enum-variant
add support for "unit" adt variants (enum variants with no fields)
2 parents 6791f18 + 26fa2ba commit 66f3d32

File tree

3 files changed

+87
-59
lines changed

3 files changed

+87
-59
lines changed

‎verify/rust_verify/src/rust_to_vir_adts.rs

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
use crate::rust_to_vir_base::{
22
check_generics, def_id_to_vir_path, get_mode, hack_get_def_name, ty_to_vir,
33
};
4+
use crate::unsupported_unless;
45
use crate::util::spanned_new;
5-
use crate::{unsupported, unsupported_unless};
66
use rustc_hir::{Crate, EnumDef, Generics, ItemId, VariantData};
77
use rustc_middle::ty::TyCtxt;
88
use rustc_span::Span;
@@ -52,9 +52,7 @@ fn check_variant_data<'tcx>(
5252
})
5353
.collect::<Vec<_>>(),
5454
),
55-
VariantData::Unit(_) => {
56-
unsupported!("unit_adt", variant_data);
57-
}
55+
VariantData::Unit(_vairant_id) => Rc::new(vec![]),
5856
}),
5957
)
6058
}

‎verify/rust_verify/src/rust_to_vir_expr.rs

Lines changed: 70 additions & 55 deletions
Original file line numberDiff line numberDiff line change
@@ -356,6 +356,62 @@ fn fn_call_to_vir<'tcx>(
356356
}
357357
}
358358

359+
pub(crate) fn expr_tuple_datatype_ctor_to_vir<'tcx>(
360+
ctxt: &Ctxt<'tcx>,
361+
expr: &Expr<'tcx>,
362+
res: &Res,
363+
args_slice: &[Expr<'tcx>],
364+
) -> Result<vir::ast::Expr, VirErr> {
365+
let variant = ctxt.tcx.expect_variant_res(*res);
366+
if let Res::Def(DefKind::Ctor(ctor_of, ctor_kind), _def_id) = res {
367+
unsupported_unless!(
368+
ctor_of == &rustc_hir::def::CtorOf::Variant,
369+
"non_variant_ctor_in_call_expr",
370+
expr
371+
);
372+
unsupported_unless!(
373+
ctor_kind == &rustc_hir::def::CtorKind::Fn
374+
|| ctor_kind == &rustc_hir::def::CtorKind::Const,
375+
"non_fn_ctor_in_call_expr",
376+
expr
377+
);
378+
}
379+
let vir_path = {
380+
// TODO is there a safer way to do this?
381+
let mut vir_path = def_id_to_vir_path(ctxt.tcx, res.def_id());
382+
Rc::get_mut(&mut vir_path).unwrap().pop(); // remove constructor
383+
Rc::get_mut(&mut vir_path).unwrap().pop(); // remove variant
384+
vir_path
385+
};
386+
let name = vir_path.last().expect("invalid path in datatype ctor");
387+
let variant_name = variant_ident(name.as_str(), &variant.ident.as_str());
388+
let vir_fields = Rc::new(
389+
args_slice
390+
.iter()
391+
.enumerate()
392+
.map(|(i, e)| -> Result<_, VirErr> {
393+
// TODO: deduplicate with Struct?
394+
let fielddef = &variant.fields[i];
395+
let field_typ = mid_ty_to_vir(ctxt.tcx, ctxt.tcx.type_of(fielddef.did));
396+
let expr_typ = typ_of_node(ctxt, &e.hir_id);
397+
let mut vir = expr_to_vir(ctxt, e)?;
398+
match (&*field_typ, &*expr_typ) {
399+
(TypX::TypParam(_), TypX::TypParam(_)) => {} // already boxed
400+
(TypX::TypParam(_), _) => {
401+
vir = Spanned::new(
402+
vir.span.clone(),
403+
ExprX::UnaryOpr(UnaryOpr::Box(expr_typ), vir),
404+
);
405+
}
406+
_ => {}
407+
}
408+
Ok(ident_binder(&variant_positional_field_ident(&variant_name, i), &vir))
409+
})
410+
.collect::<Result<Vec<_>, _>>()?,
411+
);
412+
Ok(spanned_new(expr.span, ExprX::Ctor(vir_path, variant_name, vir_fields)))
413+
}
414+
359415
pub(crate) fn expr_to_vir_inner<'tcx>(
360416
ctxt: &Ctxt<'tcx>,
361417
expr: &Expr<'tcx>,
@@ -379,58 +435,7 @@ pub(crate) fn expr_to_vir_inner<'tcx>(
379435
ExprKind::Path(QPath::Resolved(
380436
None,
381437
rustc_hir::Path { res: res @ Res::Def(DefKind::Ctor(_, _), _), .. },
382-
)) => {
383-
let variant = tcx.expect_variant_res(*res);
384-
if let Res::Def(DefKind::Ctor(ctor_of, ctor_kind), _def_id) = res {
385-
unsupported_unless!(
386-
ctor_of == &rustc_hir::def::CtorOf::Variant,
387-
"non_variant_ctor_in_call_expr",
388-
fun
389-
);
390-
unsupported_unless!(
391-
ctor_kind == &rustc_hir::def::CtorKind::Fn,
392-
"non_fn_ctor_in_call_expr",
393-
fun
394-
);
395-
}
396-
let vir_path = {
397-
// TODO is there a safer way to do this?
398-
let mut vir_path = def_id_to_vir_path(tcx, res.def_id());
399-
Rc::get_mut(&mut vir_path).unwrap().pop(); // remove constructor
400-
Rc::get_mut(&mut vir_path).unwrap().pop(); // remove variant
401-
vir_path
402-
};
403-
let name = vir_path.last().expect("invalid path in datatype ctor");
404-
let variant_name = variant_ident(name.as_str(), &variant.ident.as_str());
405-
let vir_fields = Rc::new(
406-
args_slice
407-
.iter()
408-
.enumerate()
409-
.map(|(i, e)| -> Result<_, VirErr> {
410-
// TODO: deduplicate with Struct?
411-
let fielddef = &variant.fields[i];
412-
let field_typ = mid_ty_to_vir(ctxt.tcx, tcx.type_of(fielddef.did));
413-
let expr_typ = typ_of_node(ctxt, &e.hir_id);
414-
let mut vir = expr_to_vir(ctxt, e)?;
415-
match (&*field_typ, &*expr_typ) {
416-
(TypX::TypParam(_), TypX::TypParam(_)) => {} // already boxed
417-
(TypX::TypParam(_), _) => {
418-
vir = Spanned::new(
419-
vir.span.clone(),
420-
ExprX::UnaryOpr(UnaryOpr::Box(expr_typ), vir),
421-
);
422-
}
423-
_ => {}
424-
}
425-
Ok(ident_binder(
426-
&variant_positional_field_ident(&variant_name, i),
427-
&vir,
428-
))
429-
})
430-
.collect::<Result<Vec<_>, _>>()?,
431-
);
432-
Ok(spanned_new(expr.span, ExprX::Ctor(vir_path, variant_name, vir_fields)))
433-
}
438+
)) => expr_tuple_datatype_ctor_to_vir(ctxt, expr, res, *args_slice),
434439
// a function
435440
ExprKind::Path(QPath::Resolved(
436441
None,
@@ -529,9 +534,19 @@ pub(crate) fn expr_to_vir_inner<'tcx>(
529534
}
530535
node => unsupported_err!(expr.span, format!("Path {:?}", node)),
531536
},
532-
Res::Def(_, id) => {
533-
let name = hack_get_def_name(tcx, id); // TODO: proper handling of paths
534-
Ok(spanned_new(expr.span, ExprX::Var(Rc::new(name))))
537+
Res::Def(def_kind, id) => {
538+
match def_kind {
539+
DefKind::Fn => {
540+
let name = hack_get_def_name(tcx, id); // TODO: proper handling of paths
541+
Ok(spanned_new(expr.span, ExprX::Var(Rc::new(name))))
542+
}
543+
DefKind::Ctor(_, _ctor_kind) => {
544+
expr_tuple_datatype_ctor_to_vir(ctxt, expr, &path.res, &[])
545+
}
546+
_ => {
547+
unsupported_err!(expr.span, format!("Path {:?} kind {:?}", id, def_kind))
548+
}
549+
}
535550
}
536551
res => unsupported_err!(expr.span, format!("Path {:?}", res)),
537552
},

‎verify/rust_verify/tests/adts.rs

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -78,3 +78,18 @@ test_verify_with_pervasive! {
7878
}
7979
} => Ok(())
8080
}
81+
82+
test_verify_with_pervasive! {
83+
#[test] test_enum_unit code! {
84+
#[derive(PartialEq, Eq, Structural)]
85+
enum AB {
86+
A,
87+
B(nat),
88+
}
89+
90+
#[spec]
91+
fn is_a(l: AB) -> bool {
92+
l == AB::A
93+
}
94+
} => Ok(())
95+
}

0 commit comments

Comments
 (0)