Apply formatter

model-checking · Aug 23, 2024 · 69fd136 · 69fd136
1 parent a742547
commit 69fd136
Show file tree

Hide file tree

Showing 5 changed files with 180 additions and 120 deletions.
diff --git a/kani-compiler/src/kani_middle/transform/check_aliasing/actions.rs b/kani-compiler/src/kani_middle/transform/check_aliasing/actions.rs
@@ -6,8 +6,8 @@
 //! statements of the code.
 
 use stable_mir::mir::{
-    BorrowKind, Local, LocalDecl, Mutability, Operand, ProjectionElem, Rvalue,
-    Statement, StatementKind, Place,
+    BorrowKind, Local, LocalDecl, Mutability, Operand, Place, ProjectionElem, Rvalue, Statement,
+    StatementKind,
 };
 use stable_mir::ty::{RigidTy, Ty, TyKind};
 
@@ -47,11 +47,7 @@ impl<'locals> CollectActions<'locals> {
         match self.locals[rvalue].ty.kind() {
             TyKind::RigidTy(RigidTy::Ref(_, ty, _)) | TyKind::RigidTy(RigidTy::RawPtr(ty, _)) => {
                 // reborrow
-                self.actions.push(Action::NewMutRefFromRaw {
-                    lvalue,
-                    rvalue,
-                    ty,
-                });
+                self.actions.push(Action::NewMutRefFromRaw { lvalue, rvalue, ty });
             }
             _ => {}
         }
@@ -67,7 +63,7 @@ impl<'locals> CollectActions<'locals> {
                 let lvalue = to;
                 let rvalue = from.local.clone();
                 self.actions.push(Action::NewStackReference { lvalue, rvalue });
-            },
+            }
             [ProjectionElem::Deref] => {
                 // Reborrow
                 // x : &mut T = &*(y : *mut T OR &mut T)
@@ -93,14 +89,13 @@ impl<'locals> CollectActions<'locals> {
                 let lvalue = to;
                 match self.locals[rvalue].ty.kind() {
                     TyKind::RigidTy(RigidTy::Ref(_, ty, _)) => {
-                        self.actions.push(Action::NewMutRawFromRef {
-                            lvalue,
-                            rvalue,
-                            ty,
-                        });
+                        self.actions.push(Action::NewMutRawFromRef { lvalue, rvalue, ty });
                     }
                     _ => {
-                        panic!("Dereference of rvalue case not yet handled for raw pointers {:?}", from);
+                        panic!(
+                            "Dereference of rvalue case not yet handled for raw pointers {:?}",
+                            from
+                        );
                     }
                 }
             }
@@ -116,10 +111,10 @@ impl<'locals> CollectActions<'locals> {
             [] => {
                 // Direct usage -- no update needed
                 return;
-            },
+            }
             [ProjectionElem::Deref] => {
                 // Dereference -- instrument stack check
-            },
+            }
             _ => {
                 // Field access -- not yet handled.
                 return;
@@ -129,12 +124,12 @@ impl<'locals> CollectActions<'locals> {
             TyKind::RigidTy(RigidTy::Ref(_, ty, _)) => {
                 self.actions.push(Action::StackUpdateReference { place: place.local, ty });
                 self.actions.push(Action::StackCheck);
-            },
+            }
             TyKind::RigidTy(RigidTy::RawPtr(ty, _)) => {
                 self.actions.push(Action::StackUpdatePointer { place: place.local, ty });
                 self.actions.push(Action::StackCheck);
-            },
-            _ => {},
+            }
+            _ => {}
         }
     }
 
@@ -143,24 +138,24 @@ impl<'locals> CollectActions<'locals> {
         match rvalue {
             Rvalue::AddressOf(_, place) => {
                 self.visit_place(place);
-            },
+            }
             Rvalue::Ref(_, _, place) => {
                 self.visit_place(place);
             }
             // The rest are not yet handled
-            Rvalue::Aggregate(_, _) => {},
-            Rvalue::BinaryOp(_, _, _) => {},
-            Rvalue::Cast(_, _, _) => {},
-            Rvalue::CheckedBinaryOp(_, _, _) => {},
-            Rvalue::CopyForDeref(_) => {},
-            Rvalue::Discriminant(_) => {},
-            Rvalue::Len(_) => {},
-            Rvalue::Repeat(_, _) => {},
-            Rvalue::ShallowInitBox(_, _) => {},
-            Rvalue::ThreadLocalRef(_) => {},
-            Rvalue::NullaryOp(_, _) => {},
-            Rvalue::UnaryOp(_, _) => {},
-            Rvalue::Use(_) => {},
+            Rvalue::Aggregate(_, _) => {}
+            Rvalue::BinaryOp(_, _, _) => {}
+            Rvalue::Cast(_, _, _) => {}
+            Rvalue::CheckedBinaryOp(_, _, _) => {}
+            Rvalue::CopyForDeref(_) => {}
+            Rvalue::Discriminant(_) => {}
+            Rvalue::Len(_) => {}
+            Rvalue::Repeat(_, _) => {}
+            Rvalue::ShallowInitBox(_, _) => {}
+            Rvalue::ThreadLocalRef(_) => {}
+            Rvalue::NullaryOp(_, _) => {}
+            Rvalue::UnaryOp(_, _) => {}
+            Rvalue::Use(_) => {}
         }
     }
 
@@ -171,18 +166,18 @@ impl<'locals> CollectActions<'locals> {
                 self.visit_rvalue_places(rvalue);
                 self.visit_place(place);
             }
-            StatementKind::FakeRead(_, _) => {},
-            StatementKind::SetDiscriminant { .. } => {},
-            StatementKind::Deinit(_) => {},
-            StatementKind::StorageLive(_) => {},
-            StatementKind::StorageDead(_) => {},
-            StatementKind::Retag(_, _) => {},
-            StatementKind::PlaceMention(_) => {},
-            StatementKind::AscribeUserType { .. } => {},
-            StatementKind::Coverage(_) => {},
-            StatementKind::Intrinsic(_) => {},
-            StatementKind::ConstEvalCounter => {},
-            StatementKind::Nop => {},
+            StatementKind::FakeRead(_, _) => {}
+            StatementKind::SetDiscriminant { .. } => {}
+            StatementKind::Deinit(_) => {}
+            StatementKind::StorageLive(_) => {}
+            StatementKind::StorageDead(_) => {}
+            StatementKind::Retag(_, _) => {}
+            StatementKind::PlaceMention(_) => {}
+            StatementKind::AscribeUserType { .. } => {}
+            StatementKind::Coverage(_) => {}
+            StatementKind::Intrinsic(_) => {}
+            StatementKind::ConstEvalCounter => {}
+            StatementKind::Nop => {}
         }
     }
 

diff --git a/kani-compiler/src/kani_middle/transform/check_aliasing/function_cache.rs b/kani-compiler/src/kani_middle/transform/check_aliasing/function_cache.rs
@@ -2,10 +2,10 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //! This module contains a cache of resolved generic functions
 
-use super::{MirInstance, MirError};
+use super::{MirError, MirInstance};
+use crate::kani_middle::find_fn_def;
 use rustc_middle::ty::TyCtxt;
 use stable_mir::ty::{GenericArgKind as GenericArg, GenericArgs};
-use crate::kani_middle::find_fn_def;
 
 /// FunctionSignature encapsulates the data
 /// for rust functions with generic arguments
@@ -56,8 +56,7 @@ pub struct Cache {
 impl Cache {
     /// Register the signature the to the cache
     /// in the given compilation context, ctx
-    pub fn register(&mut self, ctx: &TyCtxt, sig: Signature) ->
-        Result<&MirInstance, MirError> {
+    pub fn register(&mut self, ctx: &TyCtxt, sig: Signature) -> Result<&MirInstance, MirError> {
         let Cache { cache } = self;
         for i in 0..cache.len() {
             if sig == cache[i].signature {
@@ -72,8 +71,7 @@ impl Cache {
     }
 
     /// Register the kani assertion function
-    pub fn register_assert(&mut self, ctx: &TyCtxt) ->
-        Result<&MirInstance, MirError> {
+    pub fn register_assert(&mut self, ctx: &TyCtxt) -> Result<&MirInstance, MirError> {
         let diagnostic = "KaniAssert".to_string();
         let args = vec![];
         let sig = Signature { diagnostic, args };