From 155f59ed96498158028e6b102762dc03b1c5fcbd Mon Sep 17 00:00:00 2001 From: Andrea Lattuada Date: Wed, 2 Jun 2021 14:46:00 +0200 Subject: [PATCH 1/6] Design document for smt equality and immutable references --- verify/docs/air/opaque_datatype.air | 28 +++ ...ity-and-references-support-and-encoding.md | 208 ++++++++++++++++++ 2 files changed, 236 insertions(+) create mode 100644 verify/docs/air/opaque_datatype.air create mode 100644 verify/docs/equality-and-references-support-and-encoding.md diff --git a/verify/docs/air/opaque_datatype.air b/verify/docs/air/opaque_datatype.air new file mode 100644 index 0000000000000..bcb8252f46739 --- /dev/null +++ b/verify/docs/air/opaque_datatype.air @@ -0,0 +1,28 @@ +(declare-sort OPAQ&Car) + +(declare-fun passengers (OPAQ&Car) Int) + +(check-valid + (declare-const car@ OPAQ&Car) + (block + (assume + (= (passengers car@) 10) + ) + (block + (assert + "000" + (and + (= (passengers car@) 10) + (not (= (passengers car@) 11)) + ) + ) + ) + (block + ;; should fail + (assert + "001" + (= (passengers car@) 14) + ) + ) + ) +) diff --git a/verify/docs/equality-and-references-support-and-encoding.md b/verify/docs/equality-and-references-support-and-encoding.md new file mode 100644 index 0000000000000..ccd28c2cc4c7a --- /dev/null +++ b/verify/docs/equality-and-references-support-and-encoding.md @@ -0,0 +1,208 @@ +# Dust: equality and references support and encoding + +Andrea Lattuada, June 2nd 2021 + +In the document I will refer to both `struct`s and `enum`s as "algebraic data types", adts in short. For the sake of writing non-contrived examples, we are going to assume that we have chosen a design for "mathematical" sequences that's similar to dafny's sequences. + +## Design dimensions + +When designing the interface and encoding of equality and reference support for Dust, we need to consider both (a) the user facing language and diagnostics, and (b) the encoding to _z3_ (via _air_). + +### Language + +Rust uses the `PartialEq` and `Eq` trait to define the `==` (`.eq`) operator for types that implement them. An `==` implementation however does not necessarily conform to structural equality. `Eq` is implemented for `Cell`, but `Cell` has interior mutability (with an unsafe implmentation). + +If the programmer uses `#[derive(PartialEq, Eq)]` for an adt without interior mutability, and all the recursively enclosed types have the same property, they obtain an `==` implementation that is structural equality. The built-in `StructuralEq` trait marks those adts where the `==` was automatically derived to be structural equality, but this property is shallow, and does not say anything about whether the enclosed types don't have interior mutability and have structural `==`. + +The user needs to know, and sometimes affirm, when a type can be treated as immutable (lacking interior mutability) for the purpose of encoding; additionally, depending on the encoding, it may be important to distinguish between types that have structural equality and those that have an immutable api, but do not have structural equality, like `Vec` (with the exception of `Vec::capacity` and related functions). + +We also need to determine whether and how to support verifying the bodies functions for types that have an immutable api but do not have structural equality, e.g. `Vec`. We may decide to restrict this support to the safe interior mutability mechanisms provided by the standard library (`Cell`, `RefCell`, `Mutex`, ...). + +### Encoding + +#### Adts with structural equality + +Adts that only contain primitive types (possibly by means of other adts with the same property) can always have an equality implementation that conforms to smt equality (with structural equality). These can be encoded as _air_ datatypes, like in the following example: + +```rust +#[derive(PartialEq, Eq)] +struct Thing { a: int, b: bool } +... +let t = Thing { a: 12, b: true }; +``` + +``` +(declare-datatypes () ((Thing (Thing/Thing (Thing/Thing/a Int) (Thing/Thing/b Bool))))) +... +(declare-const t@ Thing) +(assume + (= t@ (Thing/Thing 12 true)) +) +``` + +For these types, if the `==` implementation is structural equality, we can encode `==` to smt equality: + +```rust +affirm(Thing { a: 12, b: true } != Thing { a: 14, b: true }); +``` + +``` +(assert + "" (req%affirm (not (= (Thing/Thing 12 true) (Thing/Thing 14 true))))) +``` + +This encoding is however unsound in general for any other adt, for example, for the following struct: + +```rust +#[derive(Eq)] +struct Custom { a: int } + +impl std::cmp::PartialEq for Custom { + fn eq(&self, other: &Self) -> bool { + self.a == other.a + 1 + } +} +``` + +This also extends to generic adts whenever the type parameters also have equality that conforms to smt equality (with structural equality). + +```rust +#[derive(PartialEq, Eq)] +struct Foo { a: A, b: bool } +``` + +In this example `==` of `Foo` would conform to smt equality, but `Foo` would not. + +#### Adts that have interior mutability (and/or raw pointers) but expose an "immutable" interface + +This set of types can also be defined those adts that do _not_ have well-defined structural equality (i.e. where at least one of the fields has interior mutability, is a raw pointer, or is another adt that recursively contains these) but "hide" the interior mutability in their public interface, and act like "immutable" types. + +`RefCell` is not one such type, as one can change its value while holding a shared reference. The following is such a (slightly contrived) type: + +```rust +struct List { + contents: RefCell>, +} + +impl List { + /// Makes an empty List + pub fn new() -> List { + List { contents: RefCell::new(Box::new()) } + } + + /// Push an item at the end of the list + pub fn push(&mut self, v: u64) { + let borrowed = self.contents.borrow_mut(); + // use borrowed to reallocate the boxed slice, and copy data over + } + + /// Get the item at position i, or None if it doesn't exist + pub fn get(&self, i: usize) -> Option { + self.contents.borrow().get(i) + } +} +``` + +Again, we treat generic adts as having this property if the type parameters have at least structural equality. The design needs to clarify whether there's a difference between "immutable" adts with generic arguments that have structural equality and those with generic arguments that are themselves "immutable" adts. + +Possibly with the exception of `Vec::capacity` and related methods, `Vec` is a type that satisfies this property, when `T` is either structural (`Vec`) or "immutable" (`Vec>`). + +## Using _traits_ to strengthen a function's or type's spec + +The rust standard library sometimes uses ("marker") traits to denote that a certain type has a specific property, potentially that a certain function has a stronger (more restrictive) specification. One example is `stc::cmp::Eq`: this trait does not define any new functions, but types implementing it promise that the `PartialEq::eq` (`==`) implementation is an equivalence relation: in addition to it being symmetric and transitive (as required by `PartialEq`), `Eq` asserts that `==` is also reflexive. Another example is `std::marker::Send` and `std::marker::Sync`, which asserts that a type is can be safely transferred across thread boundaries, and that it's one for which it's safe to share references across threads, respectively. + +As described in the following section(s), we plan on leaning on this to extend the specification for `==` to, e.g., structural equality, for the types that conform to it. + +## The `builtin::Structural` trait, and visibility + +Because the `std::marker::StructuralEq` reflects only shallow structural equality, we add a verifier-specific marker trait, `builtin::Structural`, which can only be implemented for an adt if its `==` implementation conforms to structural equality. Adts that implement this trait are encoded as `air` datatypes, and `==` for these types is encoded as smt equality, whenever all of their fields are visible in the current scope; if at least _one_ of the fields is not visible, the encoding will be opaque, as discussed later. + +The `trait builtint::Structural` can be implemented by the user, and the verifier checks that the type can indeed recursively conform to structural equality, and that the `==` implementation matches. If there are type parameters, these must also restricted to implement `builtin::Structural`. A `derive` macro is provided, so that the user can write: + +```rust +#[derive(PartialEq, Eq, Structural)] +struct Thing { + value: T, +} +``` + +The following derived `Structural` implementation would match the following: + +```rust +impl builtin::Structural for Thing { } +``` + +## `builtin::Structural` types with non-visible fields + +When referencing a `Structural` type from a separate module where some of the fields are not visible (not `pub`/ `pub(crate)`), we encode the entire type as an opaque z3 "sort". + +## `builtin::Immutable`, `builtin::ImmutableEq` for adts that (may) have interior mutability (and/or raw pointers) but expose an "immutable" interface + +When a type may have interior mutability, but exposes an "immutable" interface (through its entire API), the user can mark it `Immutable`. Additionally, the trait `builtin::ImmutableEq` asserts that `==` conforms to "mathematical" (smt) equality. `Immutable` is required for `ImmutableEq`. + + + +--- + + + +## The `builtin::View` trait, and `builtin::ViewEq` + +In general, specifications for public functions of a type should be written in terms of an abstract representation of the type's contents. A `Vec` should be represented just as a sequence (maybe, a slice) of integers; by default none of the facts necessary to prove the implementation should leak into the publicly visible specification of the interface. In our experience with _Veribetrfs_, inadvertently exposing internal invariants and properties is one of the common causes of long verification times and timeouts; this is because the solver has access to facts internal to the implementations that are irrelevant but can still be selected and cause qunatifier triggers to fire. + +With the exception of very simple ADTs that have all public fields and implement `Structural`, the abstract representation of a type must be specified by implementing the `View` trait: + +```rust +trait View { + type View : std::marker::StructEq; + + #[spec] + fn view(&self) -> Self::View { unimplemented!() } +} +``` + +So, for `Vec`, we'd implement `View` as something like: + +```rust +impl builtin::View for Vec { + type View = [T]; // (a sequence of T's) +} +``` + +The specification for `Vec::push` and `Vec::get` can then be along the lines of: + +```rust +pub fn push(&mut self, value: T) { + ensures(self.view() == old(self).view() + [value]); +``` + +```rust +pub fn get(&self, index: usize) -> Option { + ensures(result == self.view()[index]); +``` + +Note that we did not provide an implementation for the `view` function. Generally speaking, `.view()` is unaffected by functions on the type that take immutable references. We are still working out the details on when `.view()` should be havoc'd. + +The `builtin::ViewEq` trait indicates that the equality implemented by `==` matches view equality, which is always structural equality of the `View`. `builtin::ViewEq` is an `unsafe` trait, as the verifier generally cannot check whether `==` matches view equality. There are two ways of imlpementing `ViewEq`: + +1. The user can manually write `unsafe impl builtin::ViewEq for T`, and this becomes part of the TCB. The `unsafe` keyword allows easy inspection. +2. The user can use a derive macro to `#[derive(ViewEq)]` the implementation for a type that also implements `View`. In this case the verifier will check that `a == b` $ \Leftrightarrow $ `a.view() == b.view()`. + +Implementing `View` also requires that the view does **not** change except for when we have `mut` or `&mut T`: to start this is trivially enforced by having `View` require `Immutable` or `Structural`. + +## Immutable references, `&_ T` + + + +Control havoc-ing with the `builtin::Immutable` trait. `StructEq` implies `Immutable` and `View` requires `Immutable`? + + + +## TODO + +* [ ] When to havoc `.view()` +* [ ] What about `Vec` where `T` is "immutable" +* [ ] What about `Vec` where `T` has interior mutability -- punt on this? +* [ ] `Hash` +* [x] Auto-`opaque` + From fa18a525c49468e6fdd808d0124fdd9bef70b80b Mon Sep 17 00:00:00 2001 From: Andrea Lattuada Date: Wed, 1 Sep 2021 17:19:16 +0200 Subject: [PATCH 2/6] Use opaque sort for datatypes when members are non-visible --- verify/rust_verify/src/rust_to_vir_adts.rs | 110 +++++++++++---------- verify/rust_verify/src/rust_to_vir_base.rs | 21 ++-- verify/rust_verify/src/verifier.rs | 2 + verify/rust_verify/tests/adts_opaque.rs | 57 +++++++++++ verify/vir/src/ast.rs | 2 + verify/vir/src/datatype_to_air.rs | 91 +++++++++++------ verify/vir/src/def.rs | 5 + verify/vir/src/func_to_air.rs | 43 +++++--- verify/vir/src/sst_to_air.rs | 16 +-- verify/vir/src/well_formed.rs | 1 + 10 files changed, 238 insertions(+), 110 deletions(-) create mode 100644 verify/rust_verify/tests/adts_opaque.rs diff --git a/verify/rust_verify/src/rust_to_vir_adts.rs b/verify/rust_verify/src/rust_to_vir_adts.rs index d111e5dd96ca8..914b7372fb974 100644 --- a/verify/rust_verify/src/rust_to_vir_adts.rs +++ b/verify/rust_verify/src/rust_to_vir_adts.rs @@ -1,6 +1,7 @@ use crate::context::Context; use crate::rust_to_vir_base::{ - check_generics, def_id_to_vir_path, get_mode, hack_get_def_name, ty_to_vir, + check_generics, def_id_to_vir_path, get_mode, hack_get_def_name, is_visibility_private, + ty_to_vir, }; use crate::unsupported_unless; use crate::util::spanned_new; @@ -15,47 +16,51 @@ fn check_variant_data<'tcx>( ctxt: &Context<'tcx>, name: &Ident, variant_data: &'tcx VariantData<'tcx>, -) -> Variant { +) -> (Variant, bool) { // TODO handle field visibility; does rustc_middle::ty::Visibility have better visibility // information than hir? - ident_binder( - name, - &(match variant_data { - VariantData::Struct(fields, recovered) => { - unsupported_unless!(!recovered, "recovered_struct", variant_data); - Arc::new( - fields - .iter() - .map(|field| { - ident_binder( - &variant_field_ident(name, &field.ident.as_str()), - &( - ty_to_vir(ctxt.tcx, field.ty), - get_mode(Mode::Exec, ctxt.tcx.hir().attrs(field.hir_id)), - ), - ) - }) - .collect::>(), - ) - } - VariantData::Tuple(fields, _variant_id) => Arc::new( - fields - .iter() - .enumerate() - .map(|(i, field)| { + let (vir_fields, one_field_private) = match variant_data { + VariantData::Struct(fields, recovered) => { + unsupported_unless!(!recovered, "recovered_struct", variant_data); + let (vir_fields, field_private): (Vec<_>, Vec<_>) = fields + .iter() + .map(|field| { + ( + ident_binder( + &variant_field_ident(name, &field.ident.as_str()), + &( + ty_to_vir(ctxt.tcx, field.ty), + get_mode(Mode::Exec, ctxt.tcx.hir().attrs(field.hir_id)), + ), + ), + is_visibility_private(&field.vis.node), + ) + }) + .unzip(); + (Arc::new(vir_fields), field_private.into_iter().any(|x| x)) + } + VariantData::Tuple(fields, _variant_id) => { + let (vir_fields, field_private): (Vec<_>, Vec<_>) = fields + .iter() + .enumerate() + .map(|(i, field)| { + ( ident_binder( &variant_positional_field_ident(name, i), &( ty_to_vir(ctxt.tcx, field.ty), get_mode(Mode::Exec, ctxt.tcx.hir().attrs(field.hir_id)), ), - ) - }) - .collect::>(), - ), - VariantData::Unit(_vairant_id) => Arc::new(vec![]), - }), - ) + ), + is_visibility_private(&field.vis.node), + ) + }) + .unzip(); + (Arc::new(vir_fields), field_private.into_iter().any(|x| x)) + } + VariantData::Unit(_vairant_id) => (Arc::new(vec![]), false), + }; + (ident_binder(name, &vir_fields), one_field_private) } pub fn check_item_struct<'tcx>( @@ -71,8 +76,10 @@ pub fn check_item_struct<'tcx>( let name = hack_get_def_name(ctxt.tcx, id.def_id.to_def_id()); 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, visibility, variants })); + let (variant, one_field_private) = check_variant_data(ctxt, &variant_name, variant_data); + let variants = Arc::new(vec![variant]); + vir.datatypes + .push(spanned_new(span, DatatypeX { path, visibility, one_field_private, variants })); Ok(()) } @@ -88,20 +95,21 @@ pub fn check_item_enum<'tcx>( check_generics(generics)?; let name = Arc::new(hack_get_def_name(ctxt.tcx, id.def_id.to_def_id())); let path = def_id_to_vir_path(ctxt.tcx, id.def_id.to_def_id()); - let variants = Arc::new( - enum_def - .variants - .iter() - .map(|variant| { - let rust_variant_name = variant.ident.as_str(); - let variant_name = str_ident( - format!("{}{}{}", name, vir::def::VARIANT_SEPARATOR, rust_variant_name) - .as_str(), - ); - check_variant_data(ctxt, &variant_name, &variant.data) - }) - .collect::>(), - ); - vir.datatypes.push(spanned_new(span, DatatypeX { path, visibility, variants })); + let (variants, one_field_private): (Vec<_>, Vec<_>) = enum_def + .variants + .iter() + .map(|variant| { + let rust_variant_name = variant.ident.as_str(); + let variant_name = str_ident( + format!("{}{}{}", name, vir::def::VARIANT_SEPARATOR, rust_variant_name).as_str(), + ); + check_variant_data(ctxt, &variant_name, &variant.data) + }) + .unzip(); + let one_field_private = one_field_private.into_iter().any(|x| x); + vir.datatypes.push(spanned_new( + span, + DatatypeX { path, visibility, one_field_private, variants: Arc::new(variants) }, + )); Ok(()) } diff --git a/verify/rust_verify/src/rust_to_vir_base.rs b/verify/rust_verify/src/rust_to_vir_base.rs index c66e990731d69..508e326a93ffb 100644 --- a/verify/rust_verify/src/rust_to_vir_base.rs +++ b/verify/rust_verify/src/rust_to_vir_base.rs @@ -64,17 +64,23 @@ pub(crate) fn ident_to_var<'tcx>(ident: &Ident) -> String { ident.to_string() } -pub(crate) fn mk_visibility<'tcx>( - owning_module: &Option, - vis: &Visibility<'tcx>, -) -> vir::ast::Visibility { - let is_private = match vis.node { +pub(crate) fn is_visibility_private(vis_kind: &VisibilityKind) -> bool { + match vis_kind { VisibilityKind::Inherited => true, VisibilityKind::Public => false, VisibilityKind::Crate(_) => false, VisibilityKind::Restricted { .. } => unsupported!("restricted visibility"), - }; - vir::ast::Visibility { owning_module: owning_module.clone(), is_private } + } +} + +pub(crate) fn mk_visibility<'tcx>( + owning_module: &Option, + vis: &Visibility<'tcx>, +) -> vir::ast::Visibility { + vir::ast::Visibility { + owning_module: owning_module.clone(), + is_private: is_visibility_private(&vis.node), + } } #[derive(Debug)] @@ -318,6 +324,7 @@ pub(crate) fn mid_ty_to_vir<'tcx>(tcx: TyCtxt<'tcx>, ty: rustc_middle::ty::Ty) - TyKind::Tuple(_) if ty.tuple_fields().count() == 0 => TypX::Unit, TyKind::Bool => TypX::Bool, TyKind::Adt(AdtDef { did, .. }, _) => { + dbg!(ty); let s = ty.to_string(); // TODO use lang items instead of string comparisons if s == crate::typecheck::BUILTIN_INT { diff --git a/verify/rust_verify/src/verifier.rs b/verify/rust_verify/src/verifier.rs index e62bc7468b4d0..6dc6f000adc7a 100644 --- a/verify/rust_verify/src/verifier.rs +++ b/verify/rust_verify/src/verifier.rs @@ -227,6 +227,8 @@ impl Verifier { } let datatype_commands = vir::datatype_to_air::datatypes_to_air( + ctx, + module, &krate .datatypes .iter() diff --git a/verify/rust_verify/tests/adts_opaque.rs b/verify/rust_verify/tests/adts_opaque.rs new file mode 100644 index 0000000000000..e8086a36c9fa9 --- /dev/null +++ b/verify/rust_verify/tests/adts_opaque.rs @@ -0,0 +1,57 @@ +#![feature(rustc_private)] +#[macro_use] +mod common; +use common::*; + +const M1: &str = code_str! { + mod M1 { + use builtin::*; + + #[derive(PartialEq, Eq)] + pub struct Car { + passengers: nat, + pub four_doors: bool, + } + + #[spec] + #[verifier(pub_abstract)] + pub fn get_passengers(c: Car) -> nat { + c.passengers + } + + #[derive(PartialEq, Eq)] + pub struct Bike { + pub hard_tail: bool, + } + } +}; + +test_verify_with_pervasive! { + #[test] test_transparent_struct_1 M1.to_string() + code_str! { + mod M2 { + use crate::M1::{Car, Bike}; + use builtin::*; + use crate::pervasive::*; + + fn test_transparent_struct_1() { + assert((Bike { hard_tail: true }).hard_tail); + } + } + } => Ok(()) +} + +test_verify_with_pervasive! { + #[test] test_opaque_struct_1 M1.to_string() + code_str! { + mod M2 { + use crate::M1::{Car, get_passengers, Bike}; + use builtin::*; + use crate::pervasive::*; + + fn test_opaque_struct_1(c: Car) { + requires(get_passengers(c) == 12); + assert(get_passengers(c) == 12); + } + } + } => Ok(()) + // => Err(err) => assert_one_fails(err) +} diff --git a/verify/vir/src/ast.rs b/verify/vir/src/ast.rs index 625dbf0194bf5..3fa0120e79bb0 100644 --- a/verify/vir/src/ast.rs +++ b/verify/vir/src/ast.rs @@ -292,6 +292,8 @@ pub type Variants = Binders; pub struct DatatypeX { pub path: Path, pub visibility: Visibility, + /// Whether at least one of the datatype fields (in any variant) is private + pub one_field_private: bool, pub variants: Variants, } pub type Datatype = Arc>; diff --git a/verify/vir/src/datatype_to_air.rs b/verify/vir/src/datatype_to_air.rs index 48018ce4f6629..9a3bbfac37059 100644 --- a/verify/vir/src/datatype_to_air.rs +++ b/verify/vir/src/datatype_to_air.rs @@ -1,10 +1,12 @@ +use crate::ast::Path; +use crate::context::Ctx; use crate::def::{prefix_box, prefix_type_id, prefix_unbox}; use crate::sst_to_air::{path_to_air_ident, typ_to_air}; use air::ast::{Command, CommandX, Commands, DeclX}; use air::ast_util::str_typ; use std::sync::Arc; -fn datatype_to_air(datatype: &crate::ast::Datatype) -> air::ast::Datatype { +fn datatype_to_air<'a>(ctx: &'a Ctx, datatype: &crate::ast::Datatype) -> air::ast::Datatype { Arc::new(air::ast::BinderX { name: path_to_air_ident(&datatype.x.path), a: Arc::new( @@ -17,7 +19,7 @@ fn datatype_to_air(datatype: &crate::ast::Datatype) -> air::ast::Datatype { Arc::new( fields .iter() - .map(|field| Arc::new(field.map_a(|(typ, _)| typ_to_air(typ)))) + .map(|field| Arc::new(field.map_a(|(typ, _)| typ_to_air(ctx, typ)))) .collect::>(), ) })) @@ -27,37 +29,66 @@ fn datatype_to_air(datatype: &crate::ast::Datatype) -> air::ast::Datatype { }) } -pub fn datatypes_to_air(datatypes: &crate::ast::Datatypes) -> Commands { +pub fn datatypes_to_air<'a>( + ctx: &'a Ctx, + source_module: &Path, + datatypes: &crate::ast::Datatypes, +) -> Commands { let mut commands: Vec = Vec::new(); - let air_datatypes = - datatypes.iter().map(|datatype| datatype_to_air(datatype)).collect::>(); - commands.push(Arc::new(CommandX::Global(Arc::new(DeclX::Datatypes(Arc::new(air_datatypes)))))); - for datatype in datatypes.iter() { - let decl_type_id = Arc::new(DeclX::Const( - prefix_type_id(&path_to_air_ident(&datatype.x.path)), - str_typ(crate::def::TYPE), - )); - commands.push(Arc::new(CommandX::Global(decl_type_id))); + for dt in datatypes.iter() { + eprintln!( + "::DT {:?} owning={:?} priv_field={:?} ?={:?}", + dt.x.path, dt.x.visibility.owning_module, dt.x.one_field_private, source_module + ); } - for datatype in datatypes.iter() { - let decl_box = Arc::new(DeclX::Fun( - prefix_box(&path_to_air_ident(&datatype.x.path)), - Arc::new(vec![str_typ(&path_to_air_ident(&datatype.x.path))]), - str_typ(crate::def::POLY), - )); - let decl_unbox = Arc::new(DeclX::Fun( - prefix_unbox(&path_to_air_ident(&datatype.x.path)), - Arc::new(vec![str_typ(crate::def::POLY)]), - str_typ(&path_to_air_ident(&datatype.x.path)), - )); - commands.push(Arc::new(CommandX::Global(decl_box))); - commands.push(Arc::new(CommandX::Global(decl_unbox))); + let (transparent, opaque): (Vec<_>, Vec<_>) = + datatypes.iter().partition(|datatype| match &datatype.x.visibility.owning_module { + None => true, + Some(target) if target.len() > source_module.len() => !datatype.x.one_field_private, + // Child can access private item in parent, so check if target is parent: + Some(target) => { + target[..] == source_module[..target.len()] || !datatype.x.one_field_private + } + }); + // Encode transparent types as air datatypes + let transparent_air_datatypes: Vec<_> = + transparent.iter().map(|datatype| datatype_to_air(ctx, datatype)).collect(); + commands.push(Arc::new(CommandX::Global(Arc::new(DeclX::Datatypes(Arc::new( + transparent_air_datatypes, + )))))); + // Encode opaque types as air sorts + for datatype in opaque.iter() { + let decl_opaq_sort = Arc::new(air::ast::DeclX::Sort(path_to_air_ident(&datatype.x.path))); + commands.push(Arc::new(CommandX::Global(decl_opaq_sort))); } - for datatype in datatypes.iter() { - let nodes = crate::prelude::datatype_box_axioms(&path_to_air_ident(&datatype.x.path)); - let axioms = air::parser::nodes_to_commands(&nodes) - .expect("internal error: malformed datatype axioms"); - commands.extend(axioms.iter().cloned()); + for (_is_transparent, datatypes) in &[(true, transparent), (false, opaque)] { + for datatype in datatypes.iter() { + let decl_type_id = Arc::new(DeclX::Const( + prefix_type_id(&path_to_air_ident(&datatype.x.path)), + str_typ(crate::def::TYPE), + )); + commands.push(Arc::new(CommandX::Global(decl_type_id))); + } + for datatype in datatypes.iter() { + let decl_box = Arc::new(DeclX::Fun( + prefix_box(&path_to_air_ident(&datatype.x.path)), + Arc::new(vec![str_typ(&path_to_air_ident(&datatype.x.path))]), + str_typ(crate::def::POLY), + )); + let decl_unbox = Arc::new(DeclX::Fun( + prefix_unbox(&path_to_air_ident(&datatype.x.path)), + Arc::new(vec![str_typ(crate::def::POLY)]), + str_typ(&path_to_air_ident(&datatype.x.path)), + )); + commands.push(Arc::new(CommandX::Global(decl_box))); + commands.push(Arc::new(CommandX::Global(decl_unbox))); + } + for datatype in datatypes.iter() { + let nodes = crate::prelude::datatype_box_axioms(&path_to_air_ident(&datatype.x.path)); + let axioms = air::parser::nodes_to_commands(&nodes) + .expect("internal error: malformed datatype axioms"); + commands.extend(axioms.iter().cloned()); + } } Arc::new(commands) } diff --git a/verify/vir/src/def.rs b/verify/vir/src/def.rs index d1e457c1a05d4..7c914566182b5 100644 --- a/verify/vir/src/def.rs +++ b/verify/vir/src/def.rs @@ -81,6 +81,7 @@ pub const TYPE_ID_SINT: &str = "SINT"; pub const PREFIX_TYPE_ID: &str = "TYPE%"; pub const HAS_TYPE: &str = "has_type"; pub const VARIANT_FIELD_SEPARATOR: &str = "/"; +pub const SUFFIX_OPAQUE_DATATYPE: &str = "&OPAQ"; pub fn suffix_global_id(ident: &Ident) -> Ident { Arc::new(ident.to_string() + SUFFIX_GLOBAL) @@ -110,6 +111,10 @@ pub fn prefix_type_id(ident: &Ident) -> Ident { Arc::new(PREFIX_TYPE_ID.to_string() + ident) } +pub fn opaque_datatype(ident: &Ident) -> Ident { + Arc::new(ident.as_ref().to_owned() + SUFFIX_OPAQUE_DATATYPE) +} + pub fn prefix_box(ident: &Ident) -> Ident { Arc::new(PREFIX_BOX.to_string() + ident) } diff --git a/verify/vir/src/func_to_air.rs b/verify/vir/src/func_to_air.rs index a8f9b4a43ef24..3e46455651b4e 100644 --- a/verify/vir/src/func_to_air.rs +++ b/verify/vir/src/func_to_air.rs @@ -17,14 +17,22 @@ use air::ast_util::{ }; use std::sync::Arc; -fn func_bind(typ_params: &Idents, params: &Params, trig_expr: &Expr, add_fuel: bool) -> Bind { +fn func_bind<'a>( + ctx: &'a Ctx, + typ_params: &Idents, + params: &Params, + trig_expr: &Expr, + add_fuel: bool, +) -> Bind { let mut binders: Vec> = Vec::new(); for typ_param in typ_params.iter() { binders.push(ident_binder(&suffix_typ_param_id(&typ_param), &str_typ(crate::def::TYPE))); } for param in params.iter() { - binders - .push(ident_binder(&suffix_local_id(¶m.x.name.clone()), &typ_to_air(¶m.x.typ))); + binders.push(ident_binder( + &suffix_local_id(¶m.x.name.clone()), + &typ_to_air(ctx, ¶m.x.typ), + )); } if add_fuel { binders.push(ident_binder(&str_ident(FUEL_LOCAL), &str_typ(FUEL_TYPE))); @@ -46,7 +54,8 @@ fn func_def_args(typ_params: &Idents, params: &Params) -> Vec { } // (forall (...) (= (f ...) body)) -fn func_def_quant( +fn func_def_quant<'a>( + ctx: &'a Ctx, name: &Ident, typ_params: &Idents, params: &Params, @@ -55,7 +64,7 @@ fn func_def_quant( let f_args = func_def_args(typ_params, params); let f_app = string_apply(name, &Arc::new(f_args)); let f_eq = Arc::new(ExprX::Binary(BinaryOp::Eq, f_app.clone(), body)); - Ok(Arc::new(ExprX::Bind(func_bind(typ_params, params, &f_app, false), f_eq))) + Ok(Arc::new(ExprX::Bind(func_bind(ctx, typ_params, params, &f_app, false), f_eq))) } fn func_body_to_air( @@ -111,8 +120,10 @@ fn func_body_to_air( let rec_f_def = ident_apply(&rec_f, &args_def); let eq_zero = mk_eq(&rec_f_fuel, &rec_f_zero); let eq_body = mk_eq(&rec_f_succ, &body_expr); - let bind_zero = func_bind(&function.x.typ_params, &function.x.params, &rec_f_fuel, true); - let bind_body = func_bind(&function.x.typ_params, &function.x.params, &rec_f_succ, true); + let bind_zero = + func_bind(ctx, &function.x.typ_params, &function.x.params, &rec_f_fuel, true); + let bind_body = + func_bind(ctx, &function.x.typ_params, &function.x.params, &rec_f_succ, true); let forall_zero = Arc::new(ExprX::Bind(bind_zero, eq_zero)); let forall_body = Arc::new(ExprX::Bind(bind_body, eq_body)); let fuel_nat_decl = Arc::new(DeclX::Const(fuel_nat_f, str_typ(FUEL_TYPE))); @@ -124,6 +135,7 @@ fn func_body_to_air( rec_f_def }; let e_forall = func_def_quant( + ctx, &suffix_global_id(&function.x.name), &function.x.typ_params, &function.x.params, @@ -171,7 +183,7 @@ pub fn req_ens_to_air( exprs.push(loc_expr); } let body = Arc::new(ExprX::Multi(MultiOp::And, Arc::new(exprs))); - let e_forall = func_def_quant(&name, &typ_params, ¶ms, body)?; + let e_forall = func_def_quant(ctx, &name, &typ_params, ¶ms, body)?; let req_ens_axiom = Arc::new(DeclX::Axiom(e_forall)); commands.push(Arc::new(CommandX::Global(req_ens_axiom))); } @@ -182,14 +194,14 @@ pub fn req_ens_to_air( /// as well as any related functions symbols (e.g., recursive versions), /// if the function is a spec function. pub fn func_name_to_air(ctx: &Ctx, function: &Function) -> Result { - let mut all_typs = vec_map(&function.x.params, |param| typ_to_air(¶m.x.typ)); + let mut all_typs = vec_map(&function.x.params, |param| typ_to_air(ctx, ¶m.x.typ)); for _ in function.x.typ_params.iter() { all_typs.insert(0, str_typ(crate::def::TYPE)); } let mut commands: Vec = Vec::new(); if let (Mode::Spec, Some((_, ret, _))) = (function.x.mode, function.x.ret.as_ref()) { // Declare the function symbol itself - let typ = typ_to_air(&ret); + let typ = typ_to_air(ctx, &ret); let name = suffix_global_id(&function.x.name); let decl = Arc::new(DeclX::Fun(name, Arc::new(all_typs), typ)); commands.push(Arc::new(CommandX::Global(decl))); @@ -199,9 +211,10 @@ pub fn func_name_to_air(ctx: &Ctx, function: &Function) -> Result Result Result<(Commands, Commands), VirErr> { - let mut all_typs = vec_map(&function.x.params, |param| typ_to_air(¶m.x.typ)); + let mut all_typs = vec_map(&function.x.params, |param| typ_to_air(ctx, ¶m.x.typ)); let param_typs = Arc::new(all_typs.clone()); for _ in function.x.typ_params.iter() { all_typs.insert(0, str_typ(crate::def::TYPE)); @@ -239,7 +252,7 @@ pub fn func_decl_to_air(ctx: &Ctx, function: &Function) -> Result<(Commands, Com if let Some(expr) = typ_invariant(&ret, &f_app, true) { // (axiom (forall (...) expr)) let e_forall = Arc::new(ExprX::Bind( - func_bind(&function.x.typ_params, &function.x.params, &f_app, false), + func_bind(ctx, &function.x.typ_params, &function.x.params, &f_app, false), expr, )); let inv_axiom = Arc::new(DeclX::Axiom(e_forall)); @@ -269,7 +282,7 @@ pub fn func_decl_to_air(ctx: &Ctx, function: &Function) -> Result<(Commands, Com let mut ens_typing_invs: Vec = Vec::new(); if let Some((name, typ, mode)) = &function.x.ret { let param = ParamX { name: name.clone(), typ: typ.clone(), mode: *mode }; - ens_typs.push(typ_to_air(&typ)); + ens_typs.push(typ_to_air(ctx, &typ)); ens_params.push(Spanned::new(function.span.clone(), param)); if let Some(expr) = typ_invariant(&typ, &ident_var(&suffix_local_id(&name)), true) { ens_typing_invs.push(expr); diff --git a/verify/vir/src/sst_to_air.rs b/verify/vir/src/sst_to_air.rs index 8fbc39fde86fa..375bf5e067a80 100644 --- a/verify/vir/src/sst_to_air.rs +++ b/verify/vir/src/sst_to_air.rs @@ -41,7 +41,7 @@ pub(crate) fn apply_range_fun(name: &str, range: &IntRange, exprs: Vec) -> str_apply(name, &args) } -pub(crate) fn typ_to_air(typ: &Typ) -> air::ast::Typ { +pub(crate) fn typ_to_air<'a>(_ctx: &'a Ctx, typ: &Typ) -> air::ast::Typ { match &**typ { TypX::Unit => str_typ(UNIT), TypX::Int(_) => int_typ(), @@ -262,7 +262,7 @@ pub(crate) fn exp_to_expr(ctx: &Ctx, exp: &Exp) -> Expr { Quant::Exists => mk_and(&vec![inv, expr]), }; let binders = vec_map(&*binders, |b| { - Arc::new(BinderX { name: suffix_local_id(&b.name), a: typ_to_air(&b.a) }) + Arc::new(BinderX { name: suffix_local_id(&b.name), a: typ_to_air(ctx, &b.a) }) }); let triggers = vec_map(&*trigs, |trig| Arc::new(vec_map(trig, |x| exp_to_expr(ctx, x)))); @@ -380,9 +380,9 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Vec { } StmX::Decl { ident, typ, mutable, init: _ } => { state.local_shared.push(if *mutable { - Arc::new(DeclX::Var(suffix_local_id(&ident), typ_to_air(&typ))) + Arc::new(DeclX::Var(suffix_local_id(&ident), typ_to_air(ctx, &typ))) } else { - Arc::new(DeclX::Const(suffix_local_id(&ident), typ_to_air(&typ))) + Arc::new(DeclX::Const(suffix_local_id(&ident), typ_to_air(ctx, &typ))) }); if ctx.debug { state @@ -638,13 +638,15 @@ pub fn body_stm_to_air( .push(Arc::new(DeclX::Const(suffix_typ_param_id(&x), str_typ(crate::def::TYPE)))); } for param in params.iter() { - local_shared - .push(Arc::new(DeclX::Const(suffix_local_id(¶m.x.name), typ_to_air(¶m.x.typ)))); + local_shared.push(Arc::new(DeclX::Const( + suffix_local_id(¶m.x.name), + typ_to_air(ctx, ¶m.x.typ), + ))); } match ret { None => {} Some((x, typ, _)) => { - local_shared.push(Arc::new(DeclX::Const(suffix_local_id(&x), typ_to_air(&typ)))); + local_shared.push(Arc::new(DeclX::Const(suffix_local_id(&x), typ_to_air(ctx, &typ)))); } } diff --git a/verify/vir/src/well_formed.rs b/verify/vir/src/well_formed.rs index 6190aacd0bafb..893950dbfd2b2 100644 --- a/verify/vir/src/well_formed.rs +++ b/verify/vir/src/well_formed.rs @@ -35,6 +35,7 @@ fn check_function(ctxt: &Ctxt, function: &Function) -> Result<(), VirErr> { ); } } + // TODO: disallow private fields, unless function is marked #[verified(pub_abstract)] ExprX::Field { datatype: path, .. } => { if !ctxt.dts.contains_key(path) { return err_string( From ed405429b50d4427102fa4cd87b32789853d774d Mon Sep 17 00:00:00 2001 From: Andrea Lattuada Date: Thu, 16 Sep 2021 16:54:08 +0200 Subject: [PATCH 3/6] Add support for immutable references --- verify/rust_verify/src/rust_to_vir_base.rs | 70 ++++++++++++---------- verify/rust_verify/src/rust_to_vir_expr.rs | 26 ++++---- verify/rust_verify/tests/refs.rs | 14 +++++ 3 files changed, 69 insertions(+), 41 deletions(-) create mode 100644 verify/rust_verify/tests/refs.rs diff --git a/verify/rust_verify/src/rust_to_vir_base.rs b/verify/rust_verify/src/rust_to_vir_base.rs index 508e326a93ffb..0acbfbe235267 100644 --- a/verify/rust_verify/src/rust_to_vir_base.rs +++ b/verify/rust_verify/src/rust_to_vir_base.rs @@ -319,12 +319,11 @@ pub(crate) fn mk_range<'tcx>(ty: rustc_middle::ty::Ty<'tcx>) -> IntRange { } // TODO review and cosolidate type translation, e.g. with `ty_to_vir`, if possible -pub(crate) fn mid_ty_to_vir<'tcx>(tcx: TyCtxt<'tcx>, ty: rustc_middle::ty::Ty) -> Typ { - let typ_x = match ty.kind() { - TyKind::Tuple(_) if ty.tuple_fields().count() == 0 => TypX::Unit, - TyKind::Bool => TypX::Bool, - TyKind::Adt(AdtDef { did, .. }, _) => { - dbg!(ty); +pub(crate) fn mid_ty_to_vir<'tcx>(tcx: TyCtxt<'tcx>, ty: rustc_middle::ty::Ty<'tcx>) -> Typ { + match ty.kind() { + TyKind::Tuple(_) if ty.tuple_fields().count() == 0 => Arc::new(TypX::Unit), + TyKind::Bool => Arc::new(TypX::Bool), + TyKind::Adt(AdtDef { did, .. }, _) => Arc::new({ let s = ty.to_string(); // TODO use lang items instead of string comparisons if s == crate::typecheck::BUILTIN_INT { @@ -334,17 +333,20 @@ pub(crate) fn mid_ty_to_vir<'tcx>(tcx: TyCtxt<'tcx>, ty: rustc_middle::ty::Ty) - } else { def_id_to_ty_path(tcx, *did) } - } - TyKind::Uint(_) | TyKind::Int(_) => TypX::Int(mk_range(ty)), - TyKind::Param(param) => TypX::TypParam(Arc::new(param.name.to_string())), + }), + TyKind::Ref(_, tys, rustc_ast::Mutability::Not) => mid_ty_to_vir(tcx, tys), + TyKind::Uint(_) | TyKind::Int(_) => Arc::new(TypX::Int(mk_range(ty))), + TyKind::Param(param) => Arc::new(TypX::TypParam(Arc::new(param.name.to_string()))), _ => { unsupported!(format!("type {:?}", ty)) } - }; - Arc::new(typ_x) + } } -pub(crate) fn mid_ty_to_vir_opt<'tcx>(tcx: TyCtxt<'tcx>, ty: rustc_middle::ty::Ty) -> Option { +pub(crate) fn mid_ty_to_vir_opt<'tcx>( + tcx: TyCtxt<'tcx>, + ty: rustc_middle::ty::Ty<'tcx>, +) -> Option { match ty.kind() { TyKind::Never => None, TyKind::Tuple(_) if ty.tuple_fields().count() == 0 => None, @@ -368,8 +370,8 @@ pub(crate) fn _ty_resolved_path_to_debug_path(_tcx: TyCtxt<'_>, ty: &Ty) -> Stri pub(crate) fn ty_to_vir<'tcx>(tcx: TyCtxt<'tcx>, ty: &Ty) -> Typ { let Ty { hir_id: _, kind, span } = ty; - let typ_x = match kind { - rustc_hir::TyKind::Path(QPath::Resolved(None, path)) => match path.res { + match kind { + rustc_hir::TyKind::Path(QPath::Resolved(None, path)) => Arc::new(match path.res { Res::PrimTy(PrimTy::Bool) => TypX::Bool, Res::PrimTy(PrimTy::Uint(UintTy::U8)) => TypX::Int(IntRange::U(8)), Res::PrimTy(PrimTy::Uint(UintTy::U16)) => TypX::Int(IntRange::U(16)), @@ -401,12 +403,15 @@ pub(crate) fn ty_to_vir<'tcx>(tcx: TyCtxt<'tcx>, ty: &Ty) -> Typ { _ => { unsupported!(format!("type {:#?} {:?} {:?}", kind, path.res, span)) } - }, + }), + rustc_hir::TyKind::Rptr( + _, + rustc_hir::MutTy { ty: tys, mutbl: rustc_ast::Mutability::Not }, + ) => ty_to_vir(tcx, tys), _ => { unsupported!(format!("type {:#?} {:?}", kind, span)) } - }; - Arc::new(typ_x) + } } pub(crate) struct BodyCtxt<'tcx> { @@ -419,6 +424,23 @@ pub(crate) fn typ_of_node<'tcx>(bctx: &BodyCtxt<'tcx>, id: &HirId) -> Typ { mid_ty_to_vir(bctx.ctxt.tcx, bctx.types.node_type(*id)) } +pub(crate) fn implements_structural<'tcx>( + tcx: TyCtxt<'tcx>, + ty: &'tcx rustc_middle::ty::TyS<'tcx>, +) -> bool { + let structural_def_id = tcx + .get_diagnostic_item(rustc_span::Symbol::intern("builtin::Structural")) + .expect("structural trait is not defined"); + let substs_ref = tcx.mk_substs([].iter()); + let ty_impls_structural = tcx.type_implements_trait(( + structural_def_id, + ty, + substs_ref, + rustc_middle::ty::ParamEnv::empty(), + )); + ty_impls_structural +} + // Do equality operations on these operands translate into the SMT solver's == operation? pub(crate) fn is_smt_equality<'tcx>( bctx: &BodyCtxt<'tcx>, @@ -431,20 +453,8 @@ pub(crate) fn is_smt_equality<'tcx>( (TypX::Bool, TypX::Bool) => true, (TypX::Int(_), TypX::Int(_)) => true, (TypX::Path(_), TypX::Path(_)) if types_equal(&t1, &t2) => { - let structural_def_id = bctx - .ctxt - .tcx - .get_diagnostic_item(rustc_span::Symbol::intern("builtin::Structural")) - .expect("structural trait is not defined"); let ty = bctx.types.node_type(*id1); - let substs_ref = bctx.ctxt.tcx.mk_substs([].iter()); - let ty_impls_structural = bctx.ctxt.tcx.type_implements_trait(( - structural_def_id, - ty, - substs_ref, - rustc_middle::ty::ParamEnv::empty(), - )); - ty_impls_structural + implements_structural(bctx.ctxt.tcx, &ty) } _ => false, } diff --git a/verify/rust_verify/src/rust_to_vir_expr.rs b/verify/rust_verify/src/rust_to_vir_expr.rs index 2cb692f30ea14..d75c5c94a5fa7 100644 --- a/verify/rust_verify/src/rust_to_vir_expr.rs +++ b/verify/rust_verify/src/rust_to_vir_expr.rs @@ -10,7 +10,7 @@ use crate::util::{ }; use crate::{unsupported, unsupported_err, unsupported_err_unless, unsupported_unless}; use air::ast::{Binder, BinderX, Ident, Quant}; -use rustc_ast::{Attribute, LitKind}; +use rustc_ast::{Attribute, BorrowKind, LitKind, Mutability}; use rustc_hir::def::{DefKind, Res}; use rustc_hir::{ Arm, BinOpKind, BindingAnnotation, Block, Destination, Expr, ExprKind, Local, LoopSource, @@ -537,16 +537,20 @@ pub(crate) fn expr_to_vir_inner<'tcx>( } }, ExprKind::Cast(source, _) => Ok(mk_ty_clip(&expr_typ, &expr_to_vir(bctx, source)?)), - ExprKind::Unary(op, arg) => { - let varg = expr_to_vir(bctx, arg)?; - let vop = match op { - UnOp::Not => UnaryOp::Not, - _ => { - unsupported_err!(expr.span, "unary expression", expr) - } - }; - Ok(mk_expr(ExprX::Unary(vop, varg))) - } + ExprKind::AddrOf(BorrowKind::Ref, Mutability::Not, e) => expr_to_vir_inner(bctx, e), + ExprKind::Unary(op, arg) => match op { + UnOp::Not => { + let varg = expr_to_vir(bctx, arg)?; + Ok(mk_expr(ExprX::Unary(UnaryOp::Not, varg))) + } + UnOp::Deref => match bctx.types.node_type(arg.hir_id).kind() { + TyKind::Ref(_, _tys, rustc_ast::Mutability::Not) => expr_to_vir_inner(bctx, arg), + _ => unsupported_err!(expr.span, "dereferencing this type is unsupported", expr), + }, + _ => { + unsupported_err!(expr.span, "unary expression", expr) + } + }, ExprKind::Binary(op, lhs, rhs) => { let vlhs = expr_to_vir(bctx, lhs)?; let vrhs = expr_to_vir(bctx, rhs)?; diff --git a/verify/rust_verify/tests/refs.rs b/verify/rust_verify/tests/refs.rs new file mode 100644 index 0000000000000..df62b1c1b8f7b --- /dev/null +++ b/verify/rust_verify/tests/refs.rs @@ -0,0 +1,14 @@ +#![feature(rustc_private)] +#[macro_use] +mod common; +use common::*; + +test_verify_with_pervasive! { + #[test] test_ref_0 code! { + fn test_ref_0(p: int) { + requires(p == 12); + let b: &int = &p; + assert(*b == 12); + } + } => Ok(()) +} From 8d14697f68efee19ba13b06f98868ca745b5d3de Mon Sep 17 00:00:00 2001 From: Andrea Lattuada Date: Thu, 16 Sep 2021 17:31:26 +0200 Subject: [PATCH 4/6] Attribute #[verifier(no_verify)] for structs: forces encoding as a sort, instead of an air adt --- verify/rust_verify/src/rust_to_vir.rs | 22 +++++++- verify/rust_verify/src/rust_to_vir_adts.rs | 30 ++++++++--- verify/rust_verify/tests/modules.rs | 14 +++++ verify/vir/src/ast.rs | 10 +++- verify/vir/src/datatype_to_air.rs | 32 ++++++------ verify/vir/src/well_formed.rs | 61 ++++++++++++++-------- 6 files changed, 120 insertions(+), 49 deletions(-) diff --git a/verify/rust_verify/src/rust_to_vir.rs b/verify/rust_verify/src/rust_to_vir.rs index 3f900e6f79260..e672d6881c7e6 100644 --- a/verify/rust_verify/src/rust_to_vir.rs +++ b/verify/rust_verify/src/rust_to_vir.rs @@ -51,11 +51,29 @@ 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, visibility, variant_data, generics)?; + check_item_struct( + ctxt, + vir, + item.span, + id, + visibility, + ctxt.tcx.hir().attrs(item.hir_id()), + variant_data, + generics, + )?; } ItemKind::Enum(enum_def, generics) => { // TODO use rustc_middle? see `Struct` case - check_item_enum(ctxt, vir, item.span, id, visibility, enum_def, generics)?; + check_item_enum( + ctxt, + vir, + item.span, + id, + visibility, + ctxt.tcx.hir().attrs(item.hir_id()), + enum_def, + generics, + )?; } ItemKind::Impl(impll) => { if let Some(TraitRef { path, hir_ref_id: _ }) = impll.of_trait { diff --git a/verify/rust_verify/src/rust_to_vir_adts.rs b/verify/rust_verify/src/rust_to_vir_adts.rs index 914b7372fb974..092a8d8a026f5 100644 --- a/verify/rust_verify/src/rust_to_vir_adts.rs +++ b/verify/rust_verify/src/rust_to_vir_adts.rs @@ -1,14 +1,15 @@ use crate::context::Context; use crate::rust_to_vir_base::{ - check_generics, def_id_to_vir_path, get_mode, hack_get_def_name, is_visibility_private, - ty_to_vir, + check_generics, def_id_to_vir_path, get_mode, get_verifier_attrs, hack_get_def_name, + is_visibility_private, ty_to_vir, }; use crate::unsupported_unless; use crate::util::spanned_new; +use rustc_ast::Attribute; use rustc_hir::{EnumDef, Generics, ItemId, VariantData}; use rustc_span::Span; use std::sync::Arc; -use vir::ast::{DatatypeX, Ident, KrateX, Mode, Variant, VirErr}; +use vir::ast::{DatatypeTransparency, DatatypeX, Ident, KrateX, Mode, Variant, VirErr}; use vir::ast_util::{ident_binder, str_ident}; use vir::def::{variant_field_ident, variant_ident, variant_positional_field_ident}; @@ -69,6 +70,7 @@ pub fn check_item_struct<'tcx>( span: Span, id: &ItemId, visibility: vir::ast::Visibility, + attrs: &[Attribute], variant_data: &'tcx VariantData<'tcx>, generics: &'tcx Generics<'tcx>, ) -> Result<(), VirErr> { @@ -77,9 +79,16 @@ 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 (variant, one_field_private) = check_variant_data(ctxt, &variant_name, variant_data); + let vattrs = get_verifier_attrs(attrs)?; + let transparency = if !vattrs.do_verify { + DatatypeTransparency::Never + } else if one_field_private { + DatatypeTransparency::WithinModule + } else { + DatatypeTransparency::Always + }; let variants = Arc::new(vec![variant]); - vir.datatypes - .push(spanned_new(span, DatatypeX { path, visibility, one_field_private, variants })); + vir.datatypes.push(spanned_new(span, DatatypeX { path, visibility, transparency, variants })); Ok(()) } @@ -89,6 +98,7 @@ pub fn check_item_enum<'tcx>( span: Span, id: &ItemId, visibility: vir::ast::Visibility, + attrs: &[Attribute], enum_def: &'tcx EnumDef<'tcx>, generics: &'tcx Generics<'tcx>, ) -> Result<(), VirErr> { @@ -107,9 +117,17 @@ pub fn check_item_enum<'tcx>( }) .unzip(); let one_field_private = one_field_private.into_iter().any(|x| x); + let vattrs = get_verifier_attrs(attrs)?; + let transparency = if !vattrs.do_verify { + DatatypeTransparency::Never + } else if one_field_private { + DatatypeTransparency::WithinModule + } else { + DatatypeTransparency::Always + }; vir.datatypes.push(spanned_new( span, - DatatypeX { path, visibility, one_field_private, variants: Arc::new(variants) }, + DatatypeX { path, visibility, transparency, variants: Arc::new(variants) }, )); Ok(()) } diff --git a/verify/rust_verify/tests/modules.rs b/verify/rust_verify/tests/modules.rs index fce1f78053ec9..8230dca7b00ac 100644 --- a/verify/rust_verify/tests/modules.rs +++ b/verify/rust_verify/tests/modules.rs @@ -23,3 +23,17 @@ test_verify_with_pervasive! { } } => Ok(()) } + +test_verify_with_pervasive! { + #[test] test_mod_adt_no_verify code! { + #[verifier(no_verify)] + #[derive(PartialEq, Eq)] + pub struct Car { + pub four_doors: bool, + } + + fn mod_adt_no_verify() { + assert(!Car { four_doors: false }.four_doors); + } + } => Err(err) => assert_eq!(err.len(), 0) +} diff --git a/verify/vir/src/ast.rs b/verify/vir/src/ast.rs index 3fa0120e79bb0..2ea4133f11522 100644 --- a/verify/vir/src/ast.rs +++ b/verify/vir/src/ast.rs @@ -287,13 +287,19 @@ pub type Fields = Binders<(Typ, Mode)>; pub type Variant = Binder; pub type Variants = Binders; +#[derive(Debug)] +pub enum DatatypeTransparency { + Never, + WithinModule, + Always, +} + /// struct or enum #[derive(Debug)] pub struct DatatypeX { pub path: Path, pub visibility: Visibility, - /// Whether at least one of the datatype fields (in any variant) is private - pub one_field_private: bool, + pub transparency: DatatypeTransparency, pub variants: Variants, } pub type Datatype = Arc>; diff --git a/verify/vir/src/datatype_to_air.rs b/verify/vir/src/datatype_to_air.rs index 9a3bbfac37059..8cb70578e9764 100644 --- a/verify/vir/src/datatype_to_air.rs +++ b/verify/vir/src/datatype_to_air.rs @@ -1,4 +1,4 @@ -use crate::ast::Path; +use crate::ast::{DatatypeTransparency, Path}; use crate::context::Ctx; use crate::def::{prefix_box, prefix_type_id, prefix_unbox}; use crate::sst_to_air::{path_to_air_ident, typ_to_air}; @@ -29,27 +29,27 @@ fn datatype_to_air<'a>(ctx: &'a Ctx, datatype: &crate::ast::Datatype) -> air::as }) } +pub fn is_datatype_transparent(source_module: &Path, datatype: &crate::ast::Datatype) -> bool { + match datatype.x.transparency { + DatatypeTransparency::Never => false, + DatatypeTransparency::WithinModule => match &datatype.x.visibility.owning_module { + None => true, + Some(target) if target.len() > source_module.len() => false, + // Child can access private item in parent, so check if target is parent: + Some(target) => target[..] == source_module[..target.len()], + }, + DatatypeTransparency::Always => true, + } +} + pub fn datatypes_to_air<'a>( ctx: &'a Ctx, source_module: &Path, datatypes: &crate::ast::Datatypes, ) -> Commands { let mut commands: Vec = Vec::new(); - for dt in datatypes.iter() { - eprintln!( - "::DT {:?} owning={:?} priv_field={:?} ?={:?}", - dt.x.path, dt.x.visibility.owning_module, dt.x.one_field_private, source_module - ); - } let (transparent, opaque): (Vec<_>, Vec<_>) = - datatypes.iter().partition(|datatype| match &datatype.x.visibility.owning_module { - None => true, - Some(target) if target.len() > source_module.len() => !datatype.x.one_field_private, - // Child can access private item in parent, so check if target is parent: - Some(target) => { - target[..] == source_module[..target.len()] || !datatype.x.one_field_private - } - }); + datatypes.iter().partition(|datatype| is_datatype_transparent(source_module, *datatype)); // Encode transparent types as air datatypes let transparent_air_datatypes: Vec<_> = transparent.iter().map(|datatype| datatype_to_air(ctx, datatype)).collect(); @@ -61,7 +61,7 @@ pub fn datatypes_to_air<'a>( let decl_opaq_sort = Arc::new(air::ast::DeclX::Sort(path_to_air_ident(&datatype.x.path))); commands.push(Arc::new(CommandX::Global(decl_opaq_sort))); } - for (_is_transparent, datatypes) in &[(true, transparent), (false, opaque)] { + for datatypes in &[transparent, opaque] { for datatype in datatypes.iter() { let decl_type_id = Arc::new(DeclX::Const( prefix_type_id(&path_to_air_ident(&datatype.x.path)), diff --git a/verify/vir/src/well_formed.rs b/verify/vir/src/well_formed.rs index 893950dbfd2b2..d4c0ddd7cc3cc 100644 --- a/verify/vir/src/well_formed.rs +++ b/verify/vir/src/well_formed.rs @@ -1,6 +1,7 @@ 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 crate::datatype_to_air::is_datatype_transparent; use std::collections::HashMap; struct Ctxt { @@ -9,39 +10,53 @@ struct Ctxt { } fn check_function(ctxt: &Ctxt, function: &Function) -> Result<(), VirErr> { - // Check that public, non-abstract spec function bodies don't refer to private items - if function.x.is_abstract || function.x.visibility.is_private || function.x.mode != Mode::Spec { - return Ok(()); - } if let Some(body) = &function.x.body { map_expr_visitor(body, &mut |expr: &Expr| { match &expr.x { ExprX::Call(x, _, _) => { - let callee = &ctxt.funs[x]; - if callee.x.visibility.is_private { - return err_string( - &expr.span, - format!( - "public spec function cannot refer to private items, unless function is marked #[verifier(pub_abstract)]" - ), - ); + // Check that public, non-abstract spec function bodies don't refer to private items + if !function.x.is_abstract + && !function.x.visibility.is_private + && function.x.mode == Mode::Spec + { + let callee = &ctxt.funs[x]; + if callee.x.visibility.is_private { + return err_string( + &expr.span, + format!( + "public spec function cannot refer to private items, unless function is marked #[verifier(pub_abstract)]" + ), + ); + } } } - ExprX::Ctor(path, _, _) => { - if !ctxt.dts.contains_key(path) { - return err_string( - &expr.span, - format!("constructor of datatype not visible here"), - ); + ExprX::Ctor(path, _variant, _fields) => { + if let Some(dt) = ctxt.dts.get(path) { + if let Some(module) = &function.x.visibility.owning_module { + if !is_datatype_transparent(&module, dt) { + return err_string( + &expr.span, + format!("constructor of datatype with unencoded fields here"), + ); + } + } + } else { + panic!("constructor of undefined datatype"); } } // TODO: disallow private fields, unless function is marked #[verified(pub_abstract)] ExprX::Field { datatype: path, .. } => { - if !ctxt.dts.contains_key(path) { - return err_string( - &expr.span, - format!("field access of datatype not visible here"), - ); + if let Some(dt) = ctxt.dts.get(path) { + if let Some(module) = &function.x.visibility.owning_module { + if !is_datatype_transparent(&module, dt) { + return err_string( + &expr.span, + format!("field access of datatype with unencoded fields here"), + ); + } + } + } else { + panic!("field access of undefined datatype"); } } _ => {} From 18ccfba9b729cbcb81961f62a9cb92670c844d8f Mon Sep 17 00:00:00 2001 From: Andrea Lattuada Date: Fri, 17 Sep 2021 14:05:32 +0200 Subject: [PATCH 5/6] air example for encoding functions on types with interior mutability --- .../docs/air/nondeterministic_functions.air | 23 +++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100644 verify/docs/air/nondeterministic_functions.air diff --git a/verify/docs/air/nondeterministic_functions.air b/verify/docs/air/nondeterministic_functions.air new file mode 100644 index 0000000000000..6f7782c68bce7 --- /dev/null +++ b/verify/docs/air/nondeterministic_functions.air @@ -0,0 +1,23 @@ +(declare-sort Vec) + +(declare-fun capacity (Vec) Int) + +(check-valid + (declare-const v@ Vec) + (declare-const c1@ Int) + (declare-const c2@ Int) + (block + (assume + (= c1@ (capacity v@)) + ) + (assume + (= c2@ (capacity v@)) + ) + (block + (assert + "000" + (= c1@ c2@) + ) + ) + ) +) From 8b9ff404db2e01ae97ef827178bfc5de014df01c Mon Sep 17 00:00:00 2001 From: Andrea Lattuada Date: Fri, 17 Sep 2021 15:19:30 +0200 Subject: [PATCH 6/6] Clean up unused vir def, and switched to implicit lifetime for typ_to_air --- verify/vir/src/def.rs | 5 ----- verify/vir/src/sst_to_air.rs | 2 +- 2 files changed, 1 insertion(+), 6 deletions(-) diff --git a/verify/vir/src/def.rs b/verify/vir/src/def.rs index 7c914566182b5..d1e457c1a05d4 100644 --- a/verify/vir/src/def.rs +++ b/verify/vir/src/def.rs @@ -81,7 +81,6 @@ pub const TYPE_ID_SINT: &str = "SINT"; pub const PREFIX_TYPE_ID: &str = "TYPE%"; pub const HAS_TYPE: &str = "has_type"; pub const VARIANT_FIELD_SEPARATOR: &str = "/"; -pub const SUFFIX_OPAQUE_DATATYPE: &str = "&OPAQ"; pub fn suffix_global_id(ident: &Ident) -> Ident { Arc::new(ident.to_string() + SUFFIX_GLOBAL) @@ -111,10 +110,6 @@ pub fn prefix_type_id(ident: &Ident) -> Ident { Arc::new(PREFIX_TYPE_ID.to_string() + ident) } -pub fn opaque_datatype(ident: &Ident) -> Ident { - Arc::new(ident.as_ref().to_owned() + SUFFIX_OPAQUE_DATATYPE) -} - pub fn prefix_box(ident: &Ident) -> Ident { Arc::new(PREFIX_BOX.to_string() + ident) } diff --git a/verify/vir/src/sst_to_air.rs b/verify/vir/src/sst_to_air.rs index 375bf5e067a80..b2187156cfa1a 100644 --- a/verify/vir/src/sst_to_air.rs +++ b/verify/vir/src/sst_to_air.rs @@ -41,7 +41,7 @@ pub(crate) fn apply_range_fun(name: &str, range: &IntRange, exprs: Vec) -> str_apply(name, &args) } -pub(crate) fn typ_to_air<'a>(_ctx: &'a Ctx, typ: &Typ) -> air::ast::Typ { +pub(crate) fn typ_to_air(_ctx: &Ctx, typ: &Typ) -> air::ast::Typ { match &**typ { TypX::Unit => str_typ(UNIT), TypX::Int(_) => int_typ(),