Merge pull request rust-lang#24 from Chris-Hawblitzel/basic-visibilit…

…y-for-datatypes

Only define datatypes when they are visible

verify/rust_verify/src/rust_to_vir.rs

@@ -29,13 +29,14 @@ fn check_item<'tcx>(
     id: &ItemId,
     item: &'tcx Item<'tcx>,
 ) -> Result<(), VirErr> {
+    let visibility = mk_visibility(&Some(module_path.clone()), &item.vis);
     match &item.kind {
         ItemKind::Fn(sig, generics, body_id) => {
             check_item_fn(
                 ctxt,
                 vir,
                 item.ident,
-                mk_visibility(&Some(module_path.clone()), &item.vis),
+                visibility,
                 ctxt.tcx.hir().attrs(item.hir_id()),
                 sig,
                 generics,
@@ -50,11 +51,11 @@ fn check_item<'tcx>(
             // TODO use rustc_middle info here? if sufficient, it may allow for a single code path
             // for definitions of the local crate and imported crates
             // let adt_def = tcx.adt_def(item.def_id);
-            check_item_struct(ctxt, vir, item.span, id, variant_data, generics)?;
+            check_item_struct(ctxt, vir, item.span, id, visibility, variant_data, generics)?;
         }
         ItemKind::Enum(enum_def, generics) => {
             // TODO use rustc_middle? see `Struct` case
-            check_item_enum(ctxt, vir, item.span, id, enum_def, generics)?;
+            check_item_enum(ctxt, vir, item.span, id, visibility, enum_def, generics)?;
         }
         ItemKind::Impl(impll) => {
             if let Some(TraitRef { path, hir_ref_id: _ }) = impll.of_trait {

verify/rust_verify/src/rust_to_vir_adts.rs

@@ -63,6 +63,7 @@ pub fn check_item_struct<'tcx>(
     vir: &mut KrateX,
     span: Span,
     id: &ItemId,
+    visibility: vir::ast::Visibility,
     variant_data: &'tcx VariantData<'tcx>,
     generics: &'tcx Generics<'tcx>,
 ) -> Result<(), VirErr> {
@@ -71,7 +72,7 @@ pub fn check_item_struct<'tcx>(
     let path = def_id_to_vir_path(ctxt.tcx, id.def_id.to_def_id());
     let variant_name = variant_ident(&name, &name);
     let variants = Arc::new(vec![check_variant_data(ctxt, &variant_name, variant_data)]);
-    vir.datatypes.push(spanned_new(span, DatatypeX { path, variants }));
+    vir.datatypes.push(spanned_new(span, DatatypeX { path, visibility, variants }));
     Ok(())
 }
 
@@ -80,6 +81,7 @@ pub fn check_item_enum<'tcx>(
     vir: &mut KrateX,
     span: Span,
     id: &ItemId,
+    visibility: vir::ast::Visibility,
     enum_def: &'tcx EnumDef<'tcx>,
     generics: &'tcx Generics<'tcx>,
 ) -> Result<(), VirErr> {
@@ -100,6 +102,6 @@ pub fn check_item_enum<'tcx>(
             })
             .collect::<Vec<_>>(),
     );
-    vir.datatypes.push(spanned_new(span, DatatypeX { path, variants }));
+    vir.datatypes.push(spanned_new(span, DatatypeX { path, visibility, variants }));
     Ok(())
 }

verify/rust_verify/src/rust_to_vir_expr.rs

@@ -590,20 +590,21 @@ pub(crate) fn expr_to_vir_inner<'tcx>(
         ExprKind::Field(lhs, name) => {
             let vir_lhs = expr_to_vir(bctx, lhs)?;
             let lhs_ty = tc.node_type(lhs.hir_id);
-            let (datatype_name, field_name, unbox) = if let Some(adt_def) = lhs_ty.ty_adt_def() {
+            let (datatype, field_name, unbox) = if let Some(adt_def) = lhs_ty.ty_adt_def() {
                 unsupported_err_unless!(
                     adt_def.variants.len() == 1,
                     expr.span,
                     "field_of_adt_with_multiple_variants",
                     expr
                 );
-                let datatype_name = hack_get_def_name(tcx, adt_def.did);
+                let datatype_path = def_id_to_vir_path(tcx, adt_def.did);
+                let datatype_name = datatype_path.last().unwrap();
                 let variant = adt_def.variants.iter().next().unwrap();
                 let variant_name = variant_ident(datatype_name.as_str(), &variant.ident.as_str());
                 // TODO: deduplicate with Ctor?
                 // TODO: is there a compiler function to do this instead?
                 let fielddef = variant.fields.iter().find(|x| &x.ident == name).expect(
-                    format!("cannot find field {:?} in struct {:?}", name, datatype_name).as_str(),
+                    format!("cannot find field {:?} in struct {:?}", name, datatype_path).as_str(),
                 );
                 let field_typ = mid_ty_to_vir(tcx, tcx.type_of(fielddef.did));
                 let target_typ = typ_of_node(bctx, &expr.hir_id);
@@ -612,12 +613,12 @@ pub(crate) fn expr_to_vir_inner<'tcx>(
                     (_, TypX::TypParam(_)) => Some(target_typ),
                     _ => None,
                 };
-                (Arc::new(datatype_name), variant_field_ident(&variant_name, &name.as_str()), unbox)
+                (datatype_path, variant_field_ident(&variant_name, &name.as_str()), unbox)
             } else {
                 unsupported_err!(expr.span, "field_of_non_adt", expr)
             };
             let mut vir =
-                spanned_new(expr.span, ExprX::Field { lhs: vir_lhs, datatype_name, field_name });
+                spanned_new(expr.span, ExprX::Field { lhs: vir_lhs, datatype, field_name });
             if let Some(target_typ) = unbox {
                 vir = Spanned::new(
                     vir.span.clone(),

verify/rust_verify/src/verifier.rs

@@ -226,7 +226,14 @@ impl Verifier {
             Self::check_internal_result(air_context.command(&command));
         }
 
-        let datatype_commands = vir::datatype_to_air::datatypes_to_air(&krate.datatypes);
+        let datatype_commands = vir::datatype_to_air::datatypes_to_air(
+            &krate
+                .datatypes
+                .iter()
+                .cloned()
+                .filter(|d| Verifier::is_visible_to(&d.x.visibility, module))
+                .collect(),
+        );
         Self::run_commands(air_context, &datatype_commands, &("Datatypes".to_string()));
 
         // Declare the function symbols

verify/rust_verify/tests/modules.rs

@@ -0,0 +1,25 @@
+#![feature(rustc_private)]
+#[macro_use]
+mod common;
+use common::*;
+
+test_verify_with_pervasive! {
+    #[test] test_mod_adt_0 code! {
+        mod M1 {
+            #[derive(PartialEq, Eq)]
+            pub struct Car {
+                pub four_doors: bool,
+            }
+        }
+
+        mod M2 {
+            use crate::M1::Car;
+            use builtin::*;
+            use crate::pervasive::*;
+
+            fn mod_adt_0() {
+                assert(!Car { four_doors: false }.four_doors);
+            }
+        }
+    } => Ok(())
+}

verify/vir/src/ast.rs

@@ -184,8 +184,7 @@ pub enum ExprX {
     /// Construct datatype value of type Path and variant Ident, with field initializers Binders<Expr>
     Ctor(Path, Ident, Binders<Expr>),
     /// Read field from datatype
-    /// TODO: datatype_name should be Path, not Ident
-    Field { lhs: Expr, datatype_name: Ident, field_name: Ident },
+    Field { lhs: Expr, datatype: Path, field_name: Ident },
     /// Primitive unary operation
     Unary(UnaryOp, Expr),
     /// Special unary operator
@@ -278,6 +277,7 @@ pub type Variants = Binders<Fields>;
 #[derive(Debug)]
 pub struct DatatypeX {
     pub path: Path,
+    pub visibility: Visibility,
     pub variants: Variants,
 }
 pub type Datatype = Arc<Spanned<DatatypeX>>;

verify/vir/src/ast_to_sst.rs

@@ -107,11 +107,11 @@ pub(crate) fn expr_to_exp(ctx: &Ctx, expr: &Expr) -> Result<Exp, VirErr> {
             }
             Ok(exp)
         }
-        ExprX::Field { lhs, datatype_name, field_name } => Ok(Spanned::new(
+        ExprX::Field { lhs, datatype, field_name } => Ok(Spanned::new(
             expr.span.clone(),
             ExpX::Field {
                 lhs: expr_to_exp(ctx, lhs)?,
-                datatype_name: datatype_name.clone(),
+                datatype: datatype.clone(),
                 field_name: field_name.clone(),
             },
         )),

verify/vir/src/ast_visitor.rs

@@ -32,13 +32,13 @@ where
             );
             f(&expr)
         }
-        ExprX::Field { lhs, datatype_name, field_name } => {
+        ExprX::Field { lhs, datatype, field_name } => {
             let lhs1 = map_expr_visitor(lhs, f)?;
             let expr = Spanned::new(
                 expr.span.clone(),
                 ExprX::Field {
                     lhs: lhs1,
-                    datatype_name: datatype_name.clone(),
+                    datatype: datatype.clone(),
                     field_name: field_name.clone(),
                 },
             );

verify/vir/src/modes.rs

@@ -1,6 +1,5 @@
-use crate::ast::{Datatype, Expr, ExprX, Function, Ident, Krate, Mode, Stmt, StmtX, VirErr};
+use crate::ast::{Datatype, Expr, ExprX, Function, Ident, Krate, Mode, Path, Stmt, StmtX, VirErr};
 use crate::ast_util::err_string;
-use crate::sst_to_air::path_to_air_ident;
 use air::ast::Span;
 use std::collections::HashMap;
 
@@ -35,7 +34,7 @@ pub struct ErasureModes {
 
 struct Typing {
     pub(crate) funs: HashMap<Ident, Function>,
-    pub(crate) datatypes: HashMap<Ident, Datatype>,
+    pub(crate) datatypes: HashMap<Path, Datatype>,
     pub(crate) vars: HashMap<Ident, Mode>,
     pub(crate) erasure_modes: ErasureModes,
 }
@@ -90,9 +89,9 @@ fn check_expr(typing: &mut Typing, outer_mode: Mode, expr: &Expr) -> Result<Mode
                 .collect::<Result<Vec<_>, _>>()?;
             Ok(binder_modes.into_iter().fold(outer_mode, mode_join))
         }
-        ExprX::Field { lhs, datatype_name, field_name } => {
+        ExprX::Field { lhs, datatype: datatype_path, field_name } => {
             let lhs_mode = check_expr(typing, outer_mode, lhs)?;
-            let datatype = &typing.datatypes[datatype_name].clone();
+            let datatype = &typing.datatypes[datatype_path].clone();
             let variants = &datatype.x.variants;
             assert_eq!(variants.len(), 1);
             let fields = &variants[0].a;
@@ -231,12 +230,12 @@ fn check_function(typing: &mut Typing, function: &Function) -> Result<(), VirErr
 
 pub fn check_crate(krate: &Krate) -> Result<ErasureModes, VirErr> {
     let mut funs: HashMap<Ident, Function> = HashMap::new();
-    let mut datatypes: HashMap<Ident, Datatype> = HashMap::new();
+    let mut datatypes: HashMap<Path, Datatype> = HashMap::new();
     for function in krate.functions.iter() {
         funs.insert(function.x.name.clone(), function.clone());
     }
     for datatype in krate.datatypes.iter() {
-        datatypes.insert(path_to_air_ident(&datatype.x.path.clone()), datatype.clone());
+        datatypes.insert(datatype.x.path.clone(), datatype.clone());
     }
     let erasure_modes = ErasureModes { condition_modes: vec![], var_modes: vec![] };
     let mut typing = Typing { funs, datatypes, vars: HashMap::new(), erasure_modes };

verify/vir/src/sst.rs

@@ -36,7 +36,7 @@ pub enum ExpX {
     Old(Ident, Ident),       // used only during sst_to_air to generate AIR Old
     Call(Ident, Typs, Exps), // call to spec function
     Ctor(Path, Ident, Binders<Exp>),
-    Field { lhs: Exp, datatype_name: Ident, field_name: Ident },
+    Field { lhs: Exp, datatype: Path, field_name: Ident },
     Unary(UnaryOp, Exp),
     UnaryOpr(UnaryOpr, Exp),
     Binary(BinaryOp, Exp, Exp),

verify/vir/src/sst_to_air.rs

@@ -225,7 +225,7 @@ pub(crate) fn exp_to_expr(ctx: &Ctx, exp: &Exp) -> Expr {
         ExpX::If(e1, e2, e3) => {
             mk_ite(&exp_to_expr(ctx, e1), &exp_to_expr(ctx, e2), &exp_to_expr(ctx, e3))
         }
-        ExpX::Field { lhs, datatype_name: _, field_name: name } => {
+        ExpX::Field { lhs, datatype: _, field_name: name } => {
             // TODO: this should include datatype_name in the function name
             let lh = exp_to_expr(ctx, lhs);
             Arc::new(ExprX::Apply(name.clone(), Arc::new(vec![lh])))

verify/vir/src/sst_visitor.rs

@@ -34,13 +34,13 @@ where
             );
             f(&exp)
         }
-        ExpX::Field { lhs, datatype_name, field_name } => {
+        ExpX::Field { lhs, datatype, field_name } => {
             let lhs1 = map_exp_visitor_bind(lhs, fb, f)?;
             let exp = Spanned::new(
                 exp.span.clone(),
                 ExpX::Field {
                     lhs: lhs1,
-                    datatype_name: datatype_name.clone(),
+                    datatype: datatype.clone(),
                     field_name: field_name.clone(),
                 },
             );

verify/vir/src/triggers_auto.rs

@@ -1,4 +1,4 @@
-use crate::ast::{BinaryOp, Ident, UnaryOp, UnaryOpr, VirErr};
+use crate::ast::{BinaryOp, Ident, Path, UnaryOp, UnaryOpr, VirErr};
 use crate::ast_util::err_str;
 use crate::context::Ctx;
 use crate::sst::{Exp, ExpX, Trig, Trigs};
@@ -31,7 +31,7 @@ and programmers having to use manual triggers to eliminate the timeouts.
 #[derive(Clone, Debug, PartialEq, Eq, Hash)]
 enum App {
     Const(Constant),
-    Field(Ident, Ident),
+    Field(Path, Ident),
     Call(Ident),
     Ctor(Ident, Ident), // datatype constructor: (Path, Variant)
     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
                 Arc::new(TermX::App(App::Ctor(path_to_air_ident(path), variant), Arc::new(terms))),
             )
         }
-        ExpX::Field { lhs, datatype_name, field_name } => {
+        ExpX::Field { lhs, datatype, field_name } => {
             let (is_pure, arg) = gather_terms(ctxt, ctx, lhs, depth + 1);
             (
                 is_pure,
                 Arc::new(TermX::App(
-                    App::Field(datatype_name.clone(), field_name.clone()),
+                    App::Field(datatype.clone(), field_name.clone()),
                     Arc::new(vec![arg]),
                 )),
             )

verify/vir/src/well_formed.rs

@@ -1,10 +1,11 @@
-use crate::ast::{Expr, ExprX, Function, Ident, Krate, Mode, VirErr};
+use crate::ast::{Datatype, Expr, ExprX, Function, Ident, Krate, Mode, Path, VirErr};
 use crate::ast_util::err_string;
 use crate::ast_visitor::map_expr_visitor;
 use std::collections::HashMap;
 
 struct Ctxt {
     pub(crate) funs: HashMap<Ident, Function>,
+    pub(crate) dts: HashMap<Path, Datatype>,
 }
 
 fn check_function(ctxt: &Ctxt, function: &Function) -> Result<(), VirErr> {
@@ -26,6 +27,22 @@ fn check_function(ctxt: &Ctxt, function: &Function) -> Result<(), VirErr> {
                         );
                     }
                 }
+                ExprX::Ctor(path, _, _) => {
+                    if !ctxt.dts.contains_key(path) {
+                        return err_string(
+                            &expr.span,
+                            format!("constructor of datatype not visible here"),
+                        );
+                    }
+                }
+                ExprX::Field { datatype: path, .. } => {
+                    if !ctxt.dts.contains_key(path) {
+                        return err_string(
+                            &expr.span,
+                            format!("field access of datatype not visible here"),
+                        );
+                    }
+                }
                 _ => {}
             }
             Ok(expr.clone())
@@ -35,11 +52,17 @@ fn check_function(ctxt: &Ctxt, function: &Function) -> Result<(), VirErr> {
 }
 
 pub fn check_crate(krate: &Krate) -> Result<(), VirErr> {
-    let mut funs: HashMap<Ident, Function> = HashMap::new();
-    for function in krate.functions.iter() {
-        funs.insert(function.x.name.clone(), function.clone());
-    }
-    let ctxt = Ctxt { funs };
+    let funs = krate
+        .functions
+        .iter()
+        .map(|function| (function.x.name.clone(), function.clone()))
+        .collect();
+    let dts = krate
+        .datatypes
+        .iter()
+        .map(|datatype| (datatype.x.path.clone(), datatype.clone()))
+        .collect();
+    let ctxt = Ctxt { funs, dts };
     for function in krate.functions.iter() {
         check_function(&ctxt, function)?;
     }