Implement Enums

mir-ssa-analysis/src/lib.rs

@@ -1,9 +1,6 @@
 #![feature(rustc_private)]
 
-use prusti_rustc_interface::{
-    index::IndexVec,
-    middle::mir,
-};
+use prusti_rustc_interface::{index::IndexVec, middle::mir};
 use std::collections::HashMap;
 
 pub type SsaVersion = usize;
@@ -34,9 +31,15 @@ impl SsaAnalysis {
         let local_count = body.local_decls.len();
         let block_count = body.basic_blocks.reverse_postorder().len();
 
-        let block_started = std::iter::repeat(false).take(block_count).collect::<Vec<_>>();
-        let initial_version_in_block = std::iter::repeat(None).take(block_count).collect::<Vec<_>>();
-        let final_version_in_block = std::iter::repeat(None).take(block_count).collect::<Vec<_>>();
+        let block_started = std::iter::repeat(false)
+            .take(block_count)
+            .collect::<Vec<_>>();
+        let initial_version_in_block = std::iter::repeat(None)
+            .take(block_count)
+            .collect::<Vec<_>>();
+        let final_version_in_block = std::iter::repeat(None)
+            .take(block_count)
+            .collect::<Vec<_>>();
 
         let mut ssa_visitor = SsaVisitor {
             version_counter: IndexVec::from_raw(vec![0; local_count]),
@@ -69,11 +72,7 @@ struct SsaVisitor {
 }
 
 impl<'tcx> SsaVisitor {
-    fn walk_block<'a>(
-        &mut self,
-        body: &'a mir::Body<'tcx>,
-        block: mir::BasicBlock,
-    ) {
+    fn walk_block<'a>(&mut self, body: &'a mir::Body<'tcx>, block: mir::BasicBlock) {
         if self.final_version_in_block[block.as_usize()].is_some() {
             return;
         }
@@ -95,7 +94,9 @@ impl<'tcx> SsaVisitor {
                 // TODO: cfg cycles
                 prev_versions.push((
                     *pred,
-                    self.final_version_in_block[pred.as_usize()].as_ref().unwrap()[local.into()],
+                    self.final_version_in_block[pred.as_usize()]
+                        .as_ref()
+                        .unwrap()[local.into()],
                 ));
             }
             if prev_versions.is_empty() {
@@ -117,7 +118,9 @@ impl<'tcx> SsaVisitor {
             assert!(self.analysis.phi.insert(block, phis).is_none());
         }
 
-        assert!(self.initial_version_in_block[block.as_usize()].replace(initial_versions.clone()).is_none());
+        assert!(self.initial_version_in_block[block.as_usize()]
+            .replace(initial_versions.clone())
+            .is_none());
 
         use mir::visit::Visitor;
         self.last_version = initial_versions;
@@ -127,12 +130,14 @@ impl<'tcx> SsaVisitor {
             .map(|local| self.last_version[local.into()])
             .collect::<IndexVec<_, _>>();
         for local in 0..self.local_count {
-            self.analysis.version.insert((
-                body.terminator_loc(block),
-                local.into(),
-            ), final_versions[local.into()]);
+            self.analysis.version.insert(
+                (body.terminator_loc(block), local.into()),
+                final_versions[local.into()],
+            );
         }
-        assert!(self.final_version_in_block[block.as_usize()].replace(final_versions).is_none());
+        assert!(self.final_version_in_block[block.as_usize()]
+            .replace(final_versions)
+            .is_none());
 
         use prusti_rustc_interface::data_structures::graph::WithSuccessors;
         for succ in body.basic_blocks.successors(block) {
@@ -152,7 +157,9 @@ impl<'tcx> mir::visit::Visitor<'tcx> for SsaVisitor {
     ) {
         let local = place.local;
 
-        assert!(self.analysis.version
+        assert!(self
+            .analysis
+            .version
             .insert((location, local), self.last_version[local])
             .is_none());
 
@@ -161,12 +168,17 @@ impl<'tcx> mir::visit::Visitor<'tcx> for SsaVisitor {
             let new_version = self.version_counter[local] + 1;
             self.version_counter[local] = new_version;
             self.last_version[local] = new_version;
-            assert!(self.analysis.updates
-                .insert(location, SsaUpdate {
-                    local,
-                    old_version,
-                    new_version,
-                })
+            assert!(self
+                .analysis
+                .updates
+                .insert(
+                    location,
+                    SsaUpdate {
+                        local,
+                        old_version,
+                        new_version,
+                    }
+                )
                 .is_none());
         }
     }

mir-state-analysis/src/free_pcs/impl/local.rs

@@ -42,7 +42,9 @@ impl Default for CapabilityLocal<'_> {
 
 impl<'tcx> CapabilityLocal<'tcx> {
     pub fn get_allocated_mut(&mut self) -> &mut CapabilityProjections<'tcx> {
-        let Self::Allocated(cps) = self else { panic!("Expected allocated local") };
+        let Self::Allocated(cps) = self else {
+            panic!("Expected allocated local")
+        };
         cps
     }
     pub fn new(local: Local, perm: CapabilityKind) -> Self {
@@ -198,8 +200,7 @@ impl<'tcx> CapabilityProjections<'tcx> {
         }
         let mut ops = Vec::new();
         for (to, from, _) in collapsed {
-            let removed_perms: Vec<_> =
-                old_caps.extract_if(|old, _| to.is_prefix(*old)).collect();
+            let removed_perms: Vec<_> = old_caps.extract_if(|old, _| to.is_prefix(*old)).collect();
             let perm = removed_perms
                 .iter()
                 .fold(CapabilityKind::Exclusive, |acc, (_, p)| {

mir-state-analysis/src/free_pcs/impl/triple.rs

@@ -58,7 +58,8 @@ impl<'tcx> Visitor<'tcx> for Fpcs<'_, 'tcx> {
                 self.ensures_unalloc(local);
             }
             &Retag(_, box place) => self.requires_exclusive(place),
-            AscribeUserType(..) | PlaceMention(..) | Coverage(..) | Intrinsic(..) | ConstEvalCounter | Nop => (),
+            AscribeUserType(..) | PlaceMention(..) | Coverage(..) | Intrinsic(..)
+            | ConstEvalCounter | Nop => (),
         };
     }
 
@@ -88,11 +89,19 @@ impl<'tcx> Visitor<'tcx> for Fpcs<'_, 'tcx> {
                     }
                 }
             }
-            &Drop { place, replace: false, .. } => {
+            &Drop {
+                place,
+                replace: false,
+                ..
+            } => {
                 self.requires_write(place);
                 self.ensures_write(place);
             }
-            &Drop { place, replace: true, .. } => {
+            &Drop {
+                place,
+                replace: true,
+                ..
+            } => {
                 self.requires_write(place);
                 self.ensures_exclusive(place);
             }

mir-state-analysis/src/utils/repacker.rs

@@ -11,8 +11,7 @@ use prusti_rustc_interface::{
     index::bit_set::BitSet,
     middle::{
         mir::{
-            tcx::PlaceTy, Body, HasLocalDecls, Local, Mutability, Place as MirPlace,
-            ProjectionElem,
+            tcx::PlaceTy, Body, HasLocalDecls, Local, Mutability, Place as MirPlace, ProjectionElem,
         },
         ty::{TyCtxt, TyKind},
     },

prusti-contracts/prusti-contracts/src/lib.rs

@@ -342,7 +342,7 @@ pub fn old<T>(arg: T) -> T {
 /// Universal quantifier.
 ///
 /// This is a Prusti-internal representation of the `forall` syntax.
-#[prusti::builtin="forall"]
+#[prusti::builtin = "forall"]
 pub fn forall<T, F>(_trigger_set: T, _closure: F) -> bool {
     true
 }

prusti-contracts/prusti-specs/src/lib.rs

@@ -77,7 +77,9 @@ fn extract_prusti_attributes(
                         // tokens identical to the ones passed by the native procedural
                         // macro call.
                         let mut iter = attr.tokens.into_iter();
-                        let TokenTree::Group(group) = iter.next().unwrap() else { unreachable!() };
+                        let TokenTree::Group(group) = iter.next().unwrap() else {
+                            unreachable!()
+                        };
                         assert!(iter.next().is_none(), "Unexpected shape of an attribute.");
                         group.stream()
                     }
@@ -596,10 +598,14 @@ pub fn refine_trait_spec(_attr: TokenStream, tokens: TokenStream) -> TokenStream
                 let parsed_predicate =
                     handle_result!(predicate::parse_predicate_in_impl(makro.mac.tokens.clone()));
 
-                let ParsedPredicate::Impl(predicate) = parsed_predicate else { unreachable!() };
+                let ParsedPredicate::Impl(predicate) = parsed_predicate else {
+                    unreachable!()
+                };
 
                 // Patch spec function: Rewrite self with _self: <SpecStruct>
-                let syn::Item::Fn(spec_function) = predicate.spec_function else { unreachable!() };
+                let syn::Item::Fn(spec_function) = predicate.spec_function else {
+                    unreachable!()
+                };
                 generated_spec_items.push(spec_function);
 
                 // Add patched predicate function to new items
@@ -872,7 +878,9 @@ fn extract_prusti_attributes_for_types(
                         // tokens identical to the ones passed by the native procedural
                         // macro call.
                         let mut iter = attr.tokens.into_iter();
-                        let TokenTree::Group(group) = iter.next().unwrap() else { unreachable!() };
+                        let TokenTree::Group(group) = iter.next().unwrap() else {
+                            unreachable!()
+                        };
                         group.stream()
                     }
                 };

prusti-encoder/src/encoders/generic.rs

@@ -1,7 +1,4 @@
-use task_encoder::{
-    TaskEncoder,
-    TaskEncoderDependencies,
-};
+use task_encoder::{TaskEncoder, TaskEncoderDependencies};
 
 pub struct GenericEncoder;
 
@@ -39,7 +36,8 @@ impl TaskEncoder for GenericEncoder {
     type EncodingError = GenericEncoderError;
 
     fn with_cache<'vir, F, R>(f: F) -> R
-        where F: FnOnce(&'vir task_encoder::CacheRef<'vir, GenericEncoder>) -> R,
+    where
+        F: FnOnce(&'vir task_encoder::CacheRef<'vir, GenericEncoder>) -> R,
     {
         CACHE.with(|cache| {
             // SAFETY: the 'vir and 'tcx given to this function will always be
@@ -57,38 +55,49 @@ impl TaskEncoder for GenericEncoder {
     fn do_encode_full<'vir>(
         task_key: &Self::TaskKey<'vir>,
         deps: &mut TaskEncoderDependencies<'vir>,
-    ) -> Result<(
-        Self::OutputFullLocal<'vir>,
-        Self::OutputFullDependency<'vir>,
-    ), (
-        Self::EncodingError,
-        Option<Self::OutputFullDependency<'vir>>,
-    )> {
-        deps.emit_output_ref::<Self>(*task_key, GenericEncoderOutputRef {
-            snapshot_param_name: "s_Param",
-            predicate_param_name: "p_Param",
-            domain_type_name: "s_Type",
-        });
-        vir::with_vcx(|vcx| Ok((GenericEncoderOutput {
-            snapshot_param: vir::vir_domain! { vcx; domain s_Param {} },
-            predicate_param: vir::vir_predicate! { vcx; predicate p_Param(self_p: Ref/*, self_s: s_Param*/) },
-            domain_type: vir::vir_domain! { vcx; domain s_Type {
-                // TODO: only emit these when the types are actually used?
-                //       emit instead from type encoder, to be consistent with the ADT case?
-                unique function s_Type_Bool(): s_Type;
-                unique function s_Type_Int_isize(): s_Type;
-                unique function s_Type_Int_i8(): s_Type;
-                unique function s_Type_Int_i16(): s_Type;
-                unique function s_Type_Int_i32(): s_Type;
-                unique function s_Type_Int_i64(): s_Type;
-                unique function s_Type_Int_i128(): s_Type;
-                unique function s_Type_Uint_usize(): s_Type;
-                unique function s_Type_Uint_u8(): s_Type;
-                unique function s_Type_Uint_u16(): s_Type;
-                unique function s_Type_Uint_u32(): s_Type;
-                unique function s_Type_Uint_u64(): s_Type;
-                unique function s_Type_Uint_u128(): s_Type;
-            } },
-        }, ())))
+    ) -> Result<
+        (
+            Self::OutputFullLocal<'vir>,
+            Self::OutputFullDependency<'vir>,
+        ),
+        (
+            Self::EncodingError,
+            Option<Self::OutputFullDependency<'vir>>,
+        ),
+    > {
+        deps.emit_output_ref::<Self>(
+            *task_key,
+            GenericEncoderOutputRef {
+                snapshot_param_name: "s_Param",
+                predicate_param_name: "p_Param",
+                domain_type_name: "s_Type",
+            },
+        );
+        vir::with_vcx(|vcx| {
+            Ok((
+                GenericEncoderOutput {
+                    snapshot_param: vir::vir_domain! { vcx; domain s_Param {} },
+                    predicate_param: vir::vir_predicate! { vcx; predicate p_Param(self_p: Ref/*, self_s: s_Param*/) },
+                    domain_type: vir::vir_domain! { vcx; domain s_Type {
+                        // TODO: only emit these when the types are actually used?
+                        //       emit instead from type encoder, to be consistent with the ADT case?
+                        unique function s_Type_Bool(): s_Type;
+                        unique function s_Type_Int_isize(): s_Type;
+                        unique function s_Type_Int_i8(): s_Type;
+                        unique function s_Type_Int_i16(): s_Type;
+                        unique function s_Type_Int_i32(): s_Type;
+                        unique function s_Type_Int_i64(): s_Type;
+                        unique function s_Type_Int_i128(): s_Type;
+                        unique function s_Type_Uint_usize(): s_Type;
+                        unique function s_Type_Uint_u8(): s_Type;
+                        unique function s_Type_Uint_u16(): s_Type;
+                        unique function s_Type_Uint_u32(): s_Type;
+                        unique function s_Type_Uint_u64(): s_Type;
+                        unique function s_Type_Uint_u128(): s_Type;
+                    } },
+                },
+                (),
+            ))
+        })
     }
 }