Add is mut ref function.

epfl-lara · Jun 1, 2021 · 574e8d8 · 574e8d8
1 parent 5f48baf
commit 574e8d8
Show file tree

Hide file tree

Showing 4 changed files with 12 additions and 10 deletions.
diff --git a/stainless_extraction/src/bindings.rs b/stainless_extraction/src/bindings.rs
@@ -209,7 +209,7 @@ impl<'bxtor, 'a, 'l, 'tcx> BindingsCollector<'bxtor, 'a, 'l, 'tcx> {
   }
 }
 
-impl<'bxtor, 'a, 'l, 'tcx> Visitor<'tcx> for BindingsCollector<'bxtor, 'a, 'l, 'tcx> {
+impl<'tcx> Visitor<'tcx> for BindingsCollector<'_, '_, '_, 'tcx> {
   type Map = rustc_middle::hir::map::Map<'tcx>;
 
   fn nested_visit_map(&mut self) -> NestedVisitorMap<Self::Map> {

diff --git a/stainless_extraction/src/expr/mod.rs b/stainless_extraction/src/expr/mod.rs
@@ -1,7 +1,6 @@
 use std::convert::TryFrom;
 
 use literal::Literal;
-use rustc_middle::mir::Mutability;
 use rustc_middle::ty::{subst::SubstsRef, Ty, TyKind};
 use rustc_mir_build::thir::{BlockSafety, Expr, ExprKind, FruInfo, Stmt, StmtKind};
 
@@ -362,7 +361,7 @@ impl<'a, 'l, 'tcx> BodyExtractor<'a, 'l, 'tcx> {
     let e = self.extract_expr(expr);
 
     // If this is a mutable reference, we DON'T freshCopy
-    if let Some(Mutability::Mut) = expr.ty.ref_mutability() {
+    if is_mut_ref(expr.ty) {
       e
     } else {
       let tpe = self.base.extract_ty(expr.ty, &self.txtcx, expr.span);

diff --git a/stainless_extraction/src/lib.rs b/stainless_extraction/src/lib.rs
@@ -34,7 +34,7 @@ use bindings::DefContext;
 use fns::TypeClassKey;
 use stainless_data::ast::Type;
 use std_items::{CrateItem, StdItem, StdItems};
-use ty::{Generics, TyExtractionCtxt};
+use ty::{is_mut_ref, Generics, TyExtractionCtxt};
 use utils::UniqueCounter;
 
 mod bindings;
@@ -432,12 +432,11 @@ impl<'a, 'l, 'tcx> BodyExtractor<'a, 'l, 'tcx> {
   /// Checks whether the function has any parameters passed by mutable
   /// reference.
   fn has_mut_ref(&self) -> bool {
-    self.body.params.iter().any(|p| {
-      matches!(
-        self.tables.node_type(p.hir_id).ref_mutability(),
-        Some(Mutability::Mut)
-      )
-    })
+    self
+      .body
+      .params
+      .iter()
+      .any(|p| is_mut_ref(self.tables.node_type(p.hir_id)))
   }
 
   fn extract_body_expr(&mut self, ldi: LocalDefId) -> st::Expr<'l> {

diff --git a/stainless_extraction/src/ty.rs b/stainless_extraction/src/ty.rs
@@ -67,6 +67,10 @@ pub fn uint_bit_width(int_ty: &UintTy, tcx: TyCtxt<'_>) -> u64 {
   int_ty.bit_width().unwrap_or_else(|| pointer_bit_width(tcx))
 }
 
+pub fn is_mut_ref<'tcx>(ty: Ty<'tcx>) -> bool {
+  matches!(ty.ref_mutability(), Some(Mutability::Mut))
+}
+
 impl<'l, 'tcx> BaseExtractor<'l, 'tcx> {
   pub(super) fn extract_ty(
     &mut self,