Skip to content

Commit 3a20c67

Browse files
tjhancetjhance
committed
handle numeric fields in struct syntax
1 parent bf38eb9 commit 3a20c67

File tree

8 files changed

+138
-22
lines changed

8 files changed

+138
-22
lines changed

‎source/rust_verify/src/lifetime_ast.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ pub(crate) enum IdKind {
1111
Fun,
1212
Local,
1313
Builtin,
14+
Field,
1415
}
1516

1617
#[derive(Debug, Clone, PartialEq, Eq, Hash)]

‎source/rust_verify/src/lifetime_emit.rs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,8 @@ pub(crate) fn encode_id(kind: IdKind, rename_count: usize, raw_id: &String) -> S
1212
IdKind::Fun => format!("f{}_{}", rename_count, raw_id),
1313
IdKind::Local => format!("x{}_{}", rename_count, vir::def::user_local_name(raw_id)),
1414
IdKind::Builtin => raw_id.clone(),
15+
IdKind::Field if raw_id.bytes().nth(0).unwrap().is_ascii_digit() => raw_id.clone(),
16+
IdKind::Field => format!("y{}_{}", rename_count, vir::def::user_local_name(raw_id)),
1517
}
1618
}
1719

‎source/rust_verify/src/lifetime_generate.rs

Lines changed: 15 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ use crate::erase::{ErasureHints, ResolvedCall};
33
use crate::rust_to_vir_base::{
44
def_id_to_vir_path, local_to_var, mid_ty_const_to_vir, mid_ty_to_vir_datatype,
55
};
6-
use crate::rust_to_vir_expr::get_adt_res;
6+
use crate::rust_to_vir_expr::{field_name_to_vir_ident, get_adt_res};
77
use crate::verus_items::{PervasiveItem, RustItem, VerusItem, VerusItems};
88
use crate::{lifetime_ast::*, verus_items};
99
use air::ast_util::str_ident;
@@ -77,6 +77,7 @@ pub(crate) struct State {
7777
datatype_worklist: Vec<DefId>,
7878
imported_fun_worklist: Vec<DefId>,
7979
id_to_name: HashMap<String, Id>,
80+
field_to_name: HashMap<String, Id>,
8081
typ_param_to_name: HashMap<(String, Option<u32>), Id>,
8182
lifetime_to_name: HashMap<(String, Option<u32>), Id>,
8283
fun_to_name: HashMap<Fun, Id>,
@@ -99,6 +100,7 @@ impl State {
99100
datatype_worklist: Vec::new(),
100101
imported_fun_worklist: Vec::new(),
101102
id_to_name: HashMap::new(),
103+
field_to_name: HashMap::new(),
102104
typ_param_to_name: HashMap::new(),
103105
lifetime_to_name: HashMap::new(),
104106
fun_to_name: HashMap::new(),
@@ -137,6 +139,12 @@ impl State {
137139
Self::id(&mut self.rename_count, &mut self.id_to_name, IdKind::Local, &raw_id, f)
138140
}
139141

142+
fn field<S: Into<String>>(&mut self, raw_id: S) -> Id {
143+
let raw_id = raw_id.into();
144+
let f = || raw_id.clone();
145+
Self::id(&mut self.rename_count, &mut self.field_to_name, IdKind::Field, &raw_id, f)
146+
}
147+
140148
fn typ_param<S: Into<String>>(&mut self, raw_id: S, maybe_impl_index: Option<u32>) -> Id {
141149
let raw_id = raw_id.into();
142150
let (is_impl, impl_index) = match (raw_id.starts_with("impl "), maybe_impl_index) {
@@ -495,7 +503,7 @@ fn erase_pat<'tcx>(ctxt: &Context<'tcx>, state: &mut State, pat: &Pat) -> Patter
495503
let name = state.datatype_name(&vir_path);
496504
let mut binders: Vec<(Id, Pattern)> = Vec::new();
497505
for pat in pats.iter() {
498-
let field = state.local(pat.ident.to_string());
506+
let field = state.field(pat.ident.to_string());
499507
let pattern = erase_pat(ctxt, state, &pat.pat);
500508
binders.push((field, pattern));
501509
}
@@ -1114,9 +1122,9 @@ fn erase_expr<'tcx>(
11141122
let variant = datatype.x.get_variant(&variant_name);
11151123
let mut fs: Vec<(Id, Exp)> = Vec::new();
11161124
for f in fields.iter() {
1117-
let field_name = Arc::new(f.ident.as_str().to_string());
1118-
let (_, field_mode, _) = get_field(&variant.a, &field_name).a;
1119-
let name = state.local(f.ident.to_string());
1125+
let vir_field_name = field_name_to_vir_ident(f.ident.as_str());
1126+
let (_, field_mode, _) = get_field(&variant.a, &vir_field_name).a;
1127+
let name = state.field(f.ident.to_string());
11201128
let e = if field_mode == Mode::Spec {
11211129
phantom_data_expr(ctxt, state, &f.expr)
11221130
} else {
@@ -1204,12 +1212,7 @@ fn erase_expr<'tcx>(
12041212
if expect_spec {
12051213
erase_spec_exps(ctxt, state, expr, vec![exp1])
12061214
} else {
1207-
let field_name = field.to_string();
1208-
let field_id = if field_name.chars().all(char::is_numeric) {
1209-
Id::new(IdKind::Builtin, 0, field_name)
1210-
} else {
1211-
state.local(field.to_string())
1212-
};
1215+
let field_id = state.field(field.to_string());
12131216
mk_exp(ExpX::Field(exp1.expect("expr"), field_id))
12141217
}
12151218
}
@@ -2067,7 +2070,7 @@ fn erase_variant_data<'tcx>(
20672070
None => {
20682071
let mut fields: Vec<Field> = Vec::new();
20692072
for field in &variant.fields {
2070-
let name = state.local(field.ident(ctxt.tcx).to_string());
2073+
let name = state.field(field.ident(ctxt.tcx).to_string());
20712074
let typ = erase_ty(ctxt, state, &ctxt.tcx.type_of(field.did).skip_binder());
20722075
fields.push(Field { name, typ: revise_typ(field.did, typ) });
20732076
}

‎source/rust_verify/src/rust_to_vir_expr.rs

Lines changed: 13 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -40,7 +40,7 @@ use vir::ast::{
4040
Typ, TypX, UnaryOp, UnaryOpr, VirErr,
4141
};
4242
use vir::ast_util::{ident_binder, typ_to_diagnostic_str, types_equal, undecorate_typ};
43-
use vir::def::positional_field_ident;
43+
use vir::def::{positional_field_ident, positional_field_ident_for_str};
4444

4545
pub(crate) fn pat_to_mut_var<'tcx>(pat: &Pat) -> Result<(bool, String), VirErr> {
4646
let Pat { hir_id: _, kind, span, default_binding_modes } = pat;
@@ -481,7 +481,8 @@ pub(crate) fn pattern_to_vir_inner<'tcx>(
481481
let mut binders: Vec<Binder<vir::ast::Pattern>> = Vec::new();
482482
for fpat in pats.iter() {
483483
let pattern = pattern_to_vir(bctx, &fpat.pat)?;
484-
let binder = ident_binder(&str_ident(&fpat.ident.as_str()), &pattern);
484+
let ident = field_name_to_vir_ident(fpat.ident.as_str());
485+
let binder = ident_binder(&ident, &pattern);
485486
binders.push(binder);
486487
}
487488
PatternX::Constructor(vir_path, variant_name, Arc::new(binders))
@@ -1650,7 +1651,8 @@ pub(crate) fn expr_to_vir_innermost<'tcx>(
16501651
.iter()
16511652
.map(|f| -> Result<_, VirErr> {
16521653
let vir = expr_to_vir(bctx, f.expr, modifier)?;
1653-
Ok(ident_binder(&str_ident(&f.ident.as_str()), &vir))
1654+
let ident = field_name_to_vir_ident(f.ident.as_str());
1655+
Ok(ident_binder(&ident, &vir))
16541656
})
16551657
.collect::<Result<Vec<_>, _>>()?,
16561658
);
@@ -2201,3 +2203,11 @@ pub(crate) fn closure_to_vir<'tcx>(
22012203
panic!("closure_to_vir expects ExprKind::Closure");
22022204
}
22032205
}
2206+
2207+
pub(crate) fn field_name_to_vir_ident(name: &str) -> vir::ast::Ident {
2208+
if name.bytes().nth(0).unwrap().is_ascii_digit() {
2209+
positional_field_ident_for_str(name)
2210+
} else {
2211+
str_ident(name)
2212+
}
2213+
}

‎source/rust_verify_test/tests/adts.rs

Lines changed: 79 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1088,3 +1088,82 @@ test_verify_one_file! {
10881088
}
10891089
} => Ok(())
10901090
}
1091+
1092+
test_verify_one_file! {
1093+
#[test] struct_syntax_with_numeric_field_names verus_code! {
1094+
#[is_variant]
1095+
enum Foo {
1096+
Bar(u32, u32),
1097+
Qux,
1098+
}
1099+
1100+
fn test() {
1101+
let b = Foo::Bar { 1: 30, 0: 20 };
1102+
assert(b.get_Bar_0() == 20);
1103+
assert(b.get_Bar_1() == 30);
1104+
}
1105+
1106+
fn test2() {
1107+
let b = Foo::Bar { 1: 30, 0: 20 };
1108+
assert(b.get_Bar_1() == 20); // FAILS
1109+
}
1110+
1111+
1112+
fn test_pat(foo: Foo) {
1113+
let foo = Foo::Bar(20, 40);
1114+
match foo {
1115+
Foo::Bar { 1: a, 0: b } => {
1116+
assert(b == 20);
1117+
assert(a == 40);
1118+
}
1119+
Foo::Qux => { assert(false); }
1120+
}
1121+
}
1122+
1123+
fn test_pat2(foo: Foo) {
1124+
let foo = Foo::Bar(20, 40);
1125+
match foo {
1126+
Foo::Bar { 1: a, 0: b } => {
1127+
assert(b == 40); // FAILS
1128+
}
1129+
Foo::Qux => { }
1130+
}
1131+
}
1132+
1133+
fn test_pat_not_all_fields(foo: Foo) {
1134+
let foo = Foo::Bar(20, 40);
1135+
match foo {
1136+
Foo::Bar { 1: a, .. } => {
1137+
assert(a == 40);
1138+
}
1139+
Foo::Qux => { assert(false); }
1140+
}
1141+
}
1142+
1143+
fn test_pat_not_all_fields2(foo: Foo) {
1144+
let foo = Foo::Bar(20, 40);
1145+
match foo {
1146+
Foo::Bar { 1: a, .. } => {
1147+
assert(a == 20); // FAILS
1148+
}
1149+
Foo::Qux => { }
1150+
}
1151+
}
1152+
1153+
spec fn sfn(foo: Foo) -> (u32, u32) {
1154+
match foo {
1155+
Foo::Bar { 1: a, 0: b } => (b, a),
1156+
Foo::Qux => (0, 0),
1157+
}
1158+
}
1159+
1160+
proof fn test_sfn(foo: Foo) {
1161+
assert(sfn(Foo::Bar(20, 30)) == (20u32, 30u32));
1162+
assert(sfn(Foo::Qux) == (0u32, 0u32));
1163+
}
1164+
1165+
proof fn test_sfn2(foo: Foo) {
1166+
assert(sfn(Foo::Bar(20, 30)).0 == 30); // FAILS
1167+
}
1168+
} => Err(err) => assert_fails(err, 4)
1169+
}

‎source/rust_verify_test/tests/modes.rs

Lines changed: 20 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -950,9 +950,8 @@ test_verify_one_file! {
950950
}
951951

952952
test_verify_one_file! {
953-
// TODO(utaal) issue with tracked rewrite, I believe
954-
#[ignore] #[test] test_struct_pattern_fields_out_of_order_fail_issue_348 verus_code! {
955-
struct Foo {
953+
#[test] test_struct_pattern_fields_out_of_order_fail_issue_348 verus_code! {
954+
tracked struct Foo {
956955
ghost a: u64,
957956
tracked b: u64,
958957
}
@@ -992,6 +991,24 @@ test_verify_one_file! {
992991
} => Ok(())
993992
}
994993

994+
test_verify_one_file! {
995+
#[test] test_struct_pattern_fields_numeric_out_of_order_fail verus_code! {
996+
tracked struct Foo(ghost u64, tracked u64);
997+
998+
proof fn some_call(tracked y: u64) { }
999+
1000+
proof fn t() {
1001+
let tracked foo = Foo(5, 6);
1002+
let tracked Foo { 1: b, 0: a } = foo;
1003+
1004+
// Variable 'a' has the mode of field '0' (that is, spec)
1005+
// some_call requires 'proof'
1006+
// So this should fail
1007+
some_call(a);
1008+
}
1009+
} => Err(err) => assert_vir_error_msg(err, "expression has mode spec, expected mode proof")
1010+
}
1011+
9951012
test_verify_one_file! {
9961013
#[test] test_use_exec_var_in_forall verus_code! {
9971014
spec fn some_fn(j: int) -> bool {

‎source/vir/src/ast.rs

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -480,8 +480,8 @@ pub enum PatternX {
480480
/// Note: ast_simplify replaces this with Constructor
481481
Tuple(Patterns),
482482
/// Match constructor of datatype Path, variant Ident
483-
/// For tuple-style variants, the patterns appear in order and are named "0", "1", etc.
484-
/// For struct-style variants, the patterns may appear in any order.
483+
/// For tuple-style variants, the fields are named "_0", "_1", etc.
484+
/// Fields can appear **in any order** even for tuple variants.
485485
Constructor(Path, Ident, Binders<Pattern>),
486486
Or(Pattern, Pattern),
487487
}
@@ -611,8 +611,8 @@ pub enum ExprX {
611611
Tuple(Exprs),
612612
/// Construct datatype value of type Path and variant Ident,
613613
/// with field initializers Binders<Expr> and an optional ".." update expression.
614-
/// For tuple-style variants, the field initializers appear in order and are named "_0", "_1", etc.
615-
/// For struct-style variants, the field initializers may appear in any order.
614+
/// For tuple-style variants, the fields are named "_0", "_1", etc.
615+
/// Fields can appear **in any order** even for tuple variants.
616616
Ctor(Path, Ident, Binders<Expr>, Option<Expr>),
617617
/// Primitive 0-argument operation
618618
NullaryOpr(NullaryOpr),

‎source/vir/src/def.rs

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -474,6 +474,10 @@ pub fn positional_field_ident(idx: usize) -> Ident {
474474
Arc::new(format!("_{}", idx))
475475
}
476476

477+
pub fn positional_field_ident_for_str(idx: &str) -> Ident {
478+
Arc::new(format!("_{}", idx))
479+
}
480+
477481
pub fn monotyp_apply(datatype: &Path, args: &Vec<Path>) -> Path {
478482
if args.len() == 0 {
479483
datatype.clone()

0 commit comments

Comments
 (0)