Skip to content

Commit 20826d5

Browse files
utaalutaal
authored
Merge pull request rust-lang#24 from Chris-Hawblitzel/basic-visibility-for-datatypes
Only define datatypes when they are visible
2 parents 8dda2f6 + 097cc84 commit 20826d5

File tree

14 files changed

+96
-38
lines changed

14 files changed

+96
-38
lines changed

‎verify/rust_verify/src/rust_to_vir.rs

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -29,13 +29,14 @@ fn check_item<'tcx>(
2929
id: &ItemId,
3030
item: &'tcx Item<'tcx>,
3131
) -> Result<(), VirErr> {
32+
let visibility = mk_visibility(&Some(module_path.clone()), &item.vis);
3233
match &item.kind {
3334
ItemKind::Fn(sig, generics, body_id) => {
3435
check_item_fn(
3536
ctxt,
3637
vir,
3738
item.ident,
38-
mk_visibility(&Some(module_path.clone()), &item.vis),
39+
visibility,
3940
ctxt.tcx.hir().attrs(item.hir_id()),
4041
sig,
4142
generics,
@@ -50,11 +51,11 @@ fn check_item<'tcx>(
5051
// TODO use rustc_middle info here? if sufficient, it may allow for a single code path
5152
// for definitions of the local crate and imported crates
5253
// let adt_def = tcx.adt_def(item.def_id);
53-
check_item_struct(ctxt, vir, item.span, id, variant_data, generics)?;
54+
check_item_struct(ctxt, vir, item.span, id, visibility, variant_data, generics)?;
5455
}
5556
ItemKind::Enum(enum_def, generics) => {
5657
// TODO use rustc_middle? see `Struct` case
57-
check_item_enum(ctxt, vir, item.span, id, enum_def, generics)?;
58+
check_item_enum(ctxt, vir, item.span, id, visibility, enum_def, generics)?;
5859
}
5960
ItemKind::Impl(impll) => {
6061
if let Some(TraitRef { path, hir_ref_id: _ }) = impll.of_trait {

‎verify/rust_verify/src/rust_to_vir_adts.rs

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -63,6 +63,7 @@ pub fn check_item_struct<'tcx>(
6363
vir: &mut KrateX,
6464
span: Span,
6565
id: &ItemId,
66+
visibility: vir::ast::Visibility,
6667
variant_data: &'tcx VariantData<'tcx>,
6768
generics: &'tcx Generics<'tcx>,
6869
) -> Result<(), VirErr> {
@@ -71,7 +72,7 @@ pub fn check_item_struct<'tcx>(
7172
let path = def_id_to_vir_path(ctxt.tcx, id.def_id.to_def_id());
7273
let variant_name = variant_ident(&name, &name);
7374
let variants = Arc::new(vec![check_variant_data(ctxt, &variant_name, variant_data)]);
74-
vir.datatypes.push(spanned_new(span, DatatypeX { path, variants }));
75+
vir.datatypes.push(spanned_new(span, DatatypeX { path, visibility, variants }));
7576
Ok(())
7677
}
7778

@@ -80,6 +81,7 @@ pub fn check_item_enum<'tcx>(
8081
vir: &mut KrateX,
8182
span: Span,
8283
id: &ItemId,
84+
visibility: vir::ast::Visibility,
8385
enum_def: &'tcx EnumDef<'tcx>,
8486
generics: &'tcx Generics<'tcx>,
8587
) -> Result<(), VirErr> {
@@ -100,6 +102,6 @@ pub fn check_item_enum<'tcx>(
100102
})
101103
.collect::<Vec<_>>(),
102104
);
103-
vir.datatypes.push(spanned_new(span, DatatypeX { path, variants }));
105+
vir.datatypes.push(spanned_new(span, DatatypeX { path, visibility, variants }));
104106
Ok(())
105107
}

‎verify/rust_verify/src/rust_to_vir_expr.rs

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -590,20 +590,21 @@ pub(crate) fn expr_to_vir_inner<'tcx>(
590590
ExprKind::Field(lhs, name) => {
591591
let vir_lhs = expr_to_vir(bctx, lhs)?;
592592
let lhs_ty = tc.node_type(lhs.hir_id);
593-
let (datatype_name, field_name, unbox) = if let Some(adt_def) = lhs_ty.ty_adt_def() {
593+
let (datatype, field_name, unbox) = if let Some(adt_def) = lhs_ty.ty_adt_def() {
594594
unsupported_err_unless!(
595595
adt_def.variants.len() == 1,
596596
expr.span,
597597
"field_of_adt_with_multiple_variants",
598598
expr
599599
);
600-
let datatype_name = hack_get_def_name(tcx, adt_def.did);
600+
let datatype_path = def_id_to_vir_path(tcx, adt_def.did);
601+
let datatype_name = datatype_path.last().unwrap();
601602
let variant = adt_def.variants.iter().next().unwrap();
602603
let variant_name = variant_ident(datatype_name.as_str(), &variant.ident.as_str());
603604
// TODO: deduplicate with Ctor?
604605
// TODO: is there a compiler function to do this instead?
605606
let fielddef = variant.fields.iter().find(|x| &x.ident == name).expect(
606-
format!("cannot find field {:?} in struct {:?}", name, datatype_name).as_str(),
607+
format!("cannot find field {:?} in struct {:?}", name, datatype_path).as_str(),
607608
);
608609
let field_typ = mid_ty_to_vir(tcx, tcx.type_of(fielddef.did));
609610
let target_typ = typ_of_node(bctx, &expr.hir_id);
@@ -612,12 +613,12 @@ pub(crate) fn expr_to_vir_inner<'tcx>(
612613
(_, TypX::TypParam(_)) => Some(target_typ),
613614
_ => None,
614615
};
615-
(Arc::new(datatype_name), variant_field_ident(&variant_name, &name.as_str()), unbox)
616+
(datatype_path, variant_field_ident(&variant_name, &name.as_str()), unbox)
616617
} else {
617618
unsupported_err!(expr.span, "field_of_non_adt", expr)
618619
};
619620
let mut vir =
620-
spanned_new(expr.span, ExprX::Field { lhs: vir_lhs, datatype_name, field_name });
621+
spanned_new(expr.span, ExprX::Field { lhs: vir_lhs, datatype, field_name });
621622
if let Some(target_typ) = unbox {
622623
vir = Spanned::new(
623624
vir.span.clone(),

‎verify/rust_verify/src/verifier.rs

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -226,7 +226,14 @@ impl Verifier {
226226
Self::check_internal_result(air_context.command(&command));
227227
}
228228

229-
let datatype_commands = vir::datatype_to_air::datatypes_to_air(&krate.datatypes);
229+
let datatype_commands = vir::datatype_to_air::datatypes_to_air(
230+
&krate
231+
.datatypes
232+
.iter()
233+
.cloned()
234+
.filter(|d| Verifier::is_visible_to(&d.x.visibility, module))
235+
.collect(),
236+
);
230237
Self::run_commands(air_context, &datatype_commands, &("Datatypes".to_string()));
231238

232239
// Declare the function symbols

‎verify/rust_verify/tests/modules.rs

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
#![feature(rustc_private)]
2+
#[macro_use]
3+
mod common;
4+
use common::*;
5+
6+
test_verify_with_pervasive! {
7+
#[test] test_mod_adt_0 code! {
8+
mod M1 {
9+
#[derive(PartialEq, Eq)]
10+
pub struct Car {
11+
pub four_doors: bool,
12+
}
13+
}
14+
15+
mod M2 {
16+
use crate::M1::Car;
17+
use builtin::*;
18+
use crate::pervasive::*;
19+
20+
fn mod_adt_0() {
21+
assert(!Car { four_doors: false }.four_doors);
22+
}
23+
}
24+
} => Ok(())
25+
}

‎verify/vir/src/ast.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -184,8 +184,7 @@ pub enum ExprX {
184184
/// Construct datatype value of type Path and variant Ident, with field initializers Binders<Expr>
185185
Ctor(Path, Ident, Binders<Expr>),
186186
/// Read field from datatype
187-
/// TODO: datatype_name should be Path, not Ident
188-
Field { lhs: Expr, datatype_name: Ident, field_name: Ident },
187+
Field { lhs: Expr, datatype: Path, field_name: Ident },
189188
/// Primitive unary operation
190189
Unary(UnaryOp, Expr),
191190
/// Special unary operator
@@ -278,6 +277,7 @@ pub type Variants = Binders<Fields>;
278277
#[derive(Debug)]
279278
pub struct DatatypeX {
280279
pub path: Path,
280+
pub visibility: Visibility,
281281
pub variants: Variants,
282282
}
283283
pub type Datatype = Arc<Spanned<DatatypeX>>;

‎verify/vir/src/ast_to_sst.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -107,11 +107,11 @@ pub(crate) fn expr_to_exp(ctx: &Ctx, expr: &Expr) -> Result<Exp, VirErr> {
107107
}
108108
Ok(exp)
109109
}
110-
ExprX::Field { lhs, datatype_name, field_name } => Ok(Spanned::new(
110+
ExprX::Field { lhs, datatype, field_name } => Ok(Spanned::new(
111111
expr.span.clone(),
112112
ExpX::Field {
113113
lhs: expr_to_exp(ctx, lhs)?,
114-
datatype_name: datatype_name.clone(),
114+
datatype: datatype.clone(),
115115
field_name: field_name.clone(),
116116
},
117117
)),

‎verify/vir/src/ast_visitor.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -32,13 +32,13 @@ where
3232
);
3333
f(&expr)
3434
}
35-
ExprX::Field { lhs, datatype_name, field_name } => {
35+
ExprX::Field { lhs, datatype, field_name } => {
3636
let lhs1 = map_expr_visitor(lhs, f)?;
3737
let expr = Spanned::new(
3838
expr.span.clone(),
3939
ExprX::Field {
4040
lhs: lhs1,
41-
datatype_name: datatype_name.clone(),
41+
datatype: datatype.clone(),
4242
field_name: field_name.clone(),
4343
},
4444
);

‎verify/vir/src/modes.rs

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,5 @@
1-
use crate::ast::{Datatype, Expr, ExprX, Function, Ident, Krate, Mode, Stmt, StmtX, VirErr};
1+
use crate::ast::{Datatype, Expr, ExprX, Function, Ident, Krate, Mode, Path, Stmt, StmtX, VirErr};
22
use crate::ast_util::err_string;
3-
use crate::sst_to_air::path_to_air_ident;
43
use air::ast::Span;
54
use std::collections::HashMap;
65

@@ -35,7 +34,7 @@ pub struct ErasureModes {
3534

3635
struct Typing {
3736
pub(crate) funs: HashMap<Ident, Function>,
38-
pub(crate) datatypes: HashMap<Ident, Datatype>,
37+
pub(crate) datatypes: HashMap<Path, Datatype>,
3938
pub(crate) vars: HashMap<Ident, Mode>,
4039
pub(crate) erasure_modes: ErasureModes,
4140
}
@@ -90,9 +89,9 @@ fn check_expr(typing: &mut Typing, outer_mode: Mode, expr: &Expr) -> Result<Mode
9089
.collect::<Result<Vec<_>, _>>()?;
9190
Ok(binder_modes.into_iter().fold(outer_mode, mode_join))
9291
}
93-
ExprX::Field { lhs, datatype_name, field_name } => {
92+
ExprX::Field { lhs, datatype: datatype_path, field_name } => {
9493
let lhs_mode = check_expr(typing, outer_mode, lhs)?;
95-
let datatype = &typing.datatypes[datatype_name].clone();
94+
let datatype = &typing.datatypes[datatype_path].clone();
9695
let variants = &datatype.x.variants;
9796
assert_eq!(variants.len(), 1);
9897
let fields = &variants[0].a;
@@ -231,12 +230,12 @@ fn check_function(typing: &mut Typing, function: &Function) -> Result<(), VirErr
231230

232231
pub fn check_crate(krate: &Krate) -> Result<ErasureModes, VirErr> {
233232
let mut funs: HashMap<Ident, Function> = HashMap::new();
234-
let mut datatypes: HashMap<Ident, Datatype> = HashMap::new();
233+
let mut datatypes: HashMap<Path, Datatype> = HashMap::new();
235234
for function in krate.functions.iter() {
236235
funs.insert(function.x.name.clone(), function.clone());
237236
}
238237
for datatype in krate.datatypes.iter() {
239-
datatypes.insert(path_to_air_ident(&datatype.x.path.clone()), datatype.clone());
238+
datatypes.insert(datatype.x.path.clone(), datatype.clone());
240239
}
241240
let erasure_modes = ErasureModes { condition_modes: vec![], var_modes: vec![] };
242241
let mut typing = Typing { funs, datatypes, vars: HashMap::new(), erasure_modes };

‎verify/vir/src/sst.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,7 @@ pub enum ExpX {
3636
Old(Ident, Ident), // used only during sst_to_air to generate AIR Old
3737
Call(Ident, Typs, Exps), // call to spec function
3838
Ctor(Path, Ident, Binders<Exp>),
39-
Field { lhs: Exp, datatype_name: Ident, field_name: Ident },
39+
Field { lhs: Exp, datatype: Path, field_name: Ident },
4040
Unary(UnaryOp, Exp),
4141
UnaryOpr(UnaryOpr, Exp),
4242
Binary(BinaryOp, Exp, Exp),

‎verify/vir/src/sst_to_air.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -225,7 +225,7 @@ pub(crate) fn exp_to_expr(ctx: &Ctx, exp: &Exp) -> Expr {
225225
ExpX::If(e1, e2, e3) => {
226226
mk_ite(&exp_to_expr(ctx, e1), &exp_to_expr(ctx, e2), &exp_to_expr(ctx, e3))
227227
}
228-
ExpX::Field { lhs, datatype_name: _, field_name: name } => {
228+
ExpX::Field { lhs, datatype: _, field_name: name } => {
229229
// TODO: this should include datatype_name in the function name
230230
let lh = exp_to_expr(ctx, lhs);
231231
Arc::new(ExprX::Apply(name.clone(), Arc::new(vec![lh])))

‎verify/vir/src/sst_visitor.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -34,13 +34,13 @@ where
3434
);
3535
f(&exp)
3636
}
37-
ExpX::Field { lhs, datatype_name, field_name } => {
37+
ExpX::Field { lhs, datatype, field_name } => {
3838
let lhs1 = map_exp_visitor_bind(lhs, fb, f)?;
3939
let exp = Spanned::new(
4040
exp.span.clone(),
4141
ExpX::Field {
4242
lhs: lhs1,
43-
datatype_name: datatype_name.clone(),
43+
datatype: datatype.clone(),
4444
field_name: field_name.clone(),
4545
},
4646
);

‎verify/vir/src/triggers_auto.rs

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
use crate::ast::{BinaryOp, Ident, UnaryOp, UnaryOpr, VirErr};
1+
use crate::ast::{BinaryOp, Ident, Path, UnaryOp, UnaryOpr, VirErr};
22
use crate::ast_util::err_str;
33
use crate::context::Ctx;
44
use crate::sst::{Exp, ExpX, Trig, Trigs};
@@ -31,7 +31,7 @@ and programmers having to use manual triggers to eliminate the timeouts.
3131
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
3232
enum App {
3333
Const(Constant),
34-
Field(Ident, Ident),
34+
Field(Path, Ident),
3535
Call(Ident),
3636
Ctor(Ident, Ident), // datatype constructor: (Path, Variant)
3737
Other(u64), // u64 is an id, assigned via a simple counter
@@ -208,12 +208,12 @@ fn gather_terms(ctxt: &mut Ctxt, ctx: &Ctx, exp: &Exp, depth: u64) -> (bool, Ter
208208
Arc::new(TermX::App(App::Ctor(path_to_air_ident(path), variant), Arc::new(terms))),
209209
)
210210
}
211-
ExpX::Field { lhs, datatype_name, field_name } => {
211+
ExpX::Field { lhs, datatype, field_name } => {
212212
let (is_pure, arg) = gather_terms(ctxt, ctx, lhs, depth + 1);
213213
(
214214
is_pure,
215215
Arc::new(TermX::App(
216-
App::Field(datatype_name.clone(), field_name.clone()),
216+
App::Field(datatype.clone(), field_name.clone()),
217217
Arc::new(vec![arg]),
218218
)),
219219
)

‎verify/vir/src/well_formed.rs

Lines changed: 29 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,11 @@
1-
use crate::ast::{Expr, ExprX, Function, Ident, Krate, Mode, VirErr};
1+
use crate::ast::{Datatype, Expr, ExprX, Function, Ident, Krate, Mode, Path, VirErr};
22
use crate::ast_util::err_string;
33
use crate::ast_visitor::map_expr_visitor;
44
use std::collections::HashMap;
55

66
struct Ctxt {
77
pub(crate) funs: HashMap<Ident, Function>,
8+
pub(crate) dts: HashMap<Path, Datatype>,
89
}
910

1011
fn check_function(ctxt: &Ctxt, function: &Function) -> Result<(), VirErr> {
@@ -26,6 +27,22 @@ fn check_function(ctxt: &Ctxt, function: &Function) -> Result<(), VirErr> {
2627
);
2728
}
2829
}
30+
ExprX::Ctor(path, _, _) => {
31+
if !ctxt.dts.contains_key(path) {
32+
return err_string(
33+
&expr.span,
34+
format!("constructor of datatype not visible here"),
35+
);
36+
}
37+
}
38+
ExprX::Field { datatype: path, .. } => {
39+
if !ctxt.dts.contains_key(path) {
40+
return err_string(
41+
&expr.span,
42+
format!("field access of datatype not visible here"),
43+
);
44+
}
45+
}
2946
_ => {}
3047
}
3148
Ok(expr.clone())
@@ -35,11 +52,17 @@ fn check_function(ctxt: &Ctxt, function: &Function) -> Result<(), VirErr> {
3552
}
3653

3754
pub fn check_crate(krate: &Krate) -> Result<(), VirErr> {
38-
let mut funs: HashMap<Ident, Function> = HashMap::new();
39-
for function in krate.functions.iter() {
40-
funs.insert(function.x.name.clone(), function.clone());
41-
}
42-
let ctxt = Ctxt { funs };
55+
let funs = krate
56+
.functions
57+
.iter()
58+
.map(|function| (function.x.name.clone(), function.clone()))
59+
.collect();
60+
let dts = krate
61+
.datatypes
62+
.iter()
63+
.map(|datatype| (datatype.x.path.clone(), datatype.clone()))
64+
.collect();
65+
let ctxt = Ctxt { funs, dts };
4366
for function in krate.functions.iter() {
4467
check_function(&ctxt, function)?;
4568
}

0 commit comments

Comments
 (0)