more lifetime refactoring

rr_frontend/radium/src/code.rs

@@ -283,6 +283,7 @@ pub enum Expr {
     /// an annotated expression
     Annot {
         a: Annotation,
+        why: Option<String>,
         e: Box<Expr>,
     },
     StructInitE {
@@ -312,13 +313,12 @@ pub enum Expr {
 }
 
 impl Expr {
-    pub fn with_optional_annotation(e: Expr, a: Option<Annotation>) -> Expr {
+    pub fn with_optional_annotation(e: Expr, a: Option<Annotation>, why: Option<String>) -> Expr {
         match a {
-            Some(a) => {
-                Expr::Annot {
-                    a,
-                    e: Box::new(e),
-                }
+            Some(a) => Expr::Annot {
+                a,
+                e: Box::new(e),
+                why,
             },
             None => e,
         }
@@ -371,8 +371,9 @@ impl Display for Expr {
                 //let formatted_ly = ly.caesium_fmt();
                 write!(f, "({}) at{{ {} }} \"{}\"", e, sls, name)
             },
-            Self::Annot { a, e } => {
-                write!(f, "AnnotExpr {} ({}) ({})", a.needs_laters(), a, e)
+            Self::Annot { a, e, why } => {
+                let why_fmt = if let Some(why) = why { format!(" (* {why} *) ") } else { format!(" ") };
+                write!(f, "AnnotExpr{}{} ({}) ({})", why_fmt, a.needs_laters(), a, e)
             },
             Self::BoxE(ly) => {
                 write!(f, "box{{{}}}", ly)
@@ -572,6 +573,7 @@ pub enum Stmt {
     Annot {
         a: Annotation,
         s: Box<Stmt>,
+        why: Option<String>,
     },
     Stuck,
 }
@@ -596,9 +598,10 @@ impl Stmt {
                 let formatted_s = s.caesium_fmt(indent);
                 format!("{ind}expr: {};\n{}", e, formatted_s.as_str())
             },
-            Stmt::Annot { a, s } => {
+            Stmt::Annot { a, s, why } => {
                 let formatted_s = s.caesium_fmt(indent);
-                format!("{ind}annot: {};\n{}", a, formatted_s.as_str())
+                let why_fmt = if let Some(why) = why { format!(" (* {why} *)") } else { format!("") };
+                format!("{ind}annot: {};{why_fmt}\n{}", a, formatted_s.as_str())
             },
             Stmt::If { ot, e, s1, s2 } => {
                 let formatted_s1 = s1.caesium_fmt(indent + 1);
@@ -653,11 +656,12 @@ impl Stmt {
     }
 
     /// Annotate a statement with a list of annotations
-    pub fn with_annotations(mut s: Stmt, a: Vec<Annotation>) -> Stmt {
+    pub fn with_annotations(mut s: Stmt, a: Vec<Annotation>, why: Option<String>) -> Stmt {
         for annot in a.into_iter() {
             s = Stmt::Annot {
                 a: annot,
                 s: Box::new(s),
+                why: why.clone(),
             };
         }
         s
@@ -952,17 +956,6 @@ impl FunctionCodeBuilder {
     pub fn add_basic_block(&mut self, index: usize, bb: Stmt) {
         self.basic_blocks.insert(index, bb);
     }
-
-    /// Initialize a local lifetime at the start of the function
-    /// (i.e., prepend the initialization statementto the first block of the function)
-    pub fn initialize_local_lifetime(&mut self, lft: Lft, outliving: Vec<Lft>) {
-        let bb0 = self.basic_blocks.remove(&FunctionCode::INITIAL_BB).unwrap();
-        let cont_stmt = Stmt::Annot {
-            a: Annotation::StartLft(format!("{}", lft), outliving),
-            s: Box::new(bb0),
-        };
-        self.basic_blocks.insert(FunctionCode::INITIAL_BB, cont_stmt);
-    }
 }
 
 #[derive(Debug, Clone)]

rr_frontend/translation/src/environment/polonius_info.rs

@@ -54,6 +54,34 @@ pub enum AtomicRegion {
 }
 
 impl AtomicRegion {
+    pub fn is_loan(&self) -> bool {
+        match *self {
+            Self::Loan(_, _) => true,
+            _ => false,
+        }
+    }
+
+    pub fn is_universal(&self) -> bool {
+        match *self {
+            Self::Universal(_, _) => true,
+            _ => false,
+        }
+    }
+
+    pub fn is_place(&self) -> bool {
+        match *self {
+            Self::PlaceRegion(_) => true,
+            _ => false,
+        }
+    }
+
+    pub fn is_value(&self) -> bool {
+        match *self {
+            Self::Unknown(_) => true,
+            _ => false,
+        }
+    }
+
     pub fn get_region(&self) -> facts::Region {
         match self {
             Self::Loan(_, r) => *r,

rr_frontend/translation/src/type_translator.rs

@@ -17,7 +17,7 @@ use rustc_middle::ty::{IntTy, Ty, TyKind, UintTy};
 use typed_arena::Arena;
 
 pub use crate::base::*;
-use crate::environment::Environment;
+use crate::environment::{polonius_info as info, Environment};
 //use rustc_middle::mir::Field;
 use crate::rustc_middle::ty::TypeFoldable;
 use crate::spec_parsers::enum_spec_parser::{EnumSpecParser, VerboseEnumSpecParser};
@@ -289,6 +289,25 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
         self.universal_lifetimes.borrow().get(&lft).map(|s| s.to_string())
     }
 
+    /// Format the Coq representation of an atomic region.
+    pub fn format_atomic_region(&self, r: &info::AtomicRegion) -> String {
+        match r {
+            info::AtomicRegion::Loan(_, r) => {
+                format!("llft{}", r.index())
+            },
+            info::AtomicRegion::Universal(_, r) => match self.lookup_universal_region(*r) {
+                Some(s) => s,
+                None => format!("ulft{}", r.index()),
+            },
+            info::AtomicRegion::PlaceRegion(r) => {
+                format!("plft{}", r.index())
+            },
+            info::AtomicRegion::Unknown(r) => {
+                format!("vlft{}", r.index())
+            },
+        }
+    }
+
     /// Try to translate a region to a Caesium lifetime.
     /// Note: This relies on all the regions being ReVar inference variables.
     // TODO: This currently uses the current function's specific scope.
@@ -969,7 +988,14 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
             builder.add_field(&f_name, field_spec.ty);
 
             if expect_refinement {
-                field_refinements.push(field_spec.rfn.unwrap());
+                if let Some(rfn) = field_spec.rfn {
+                    field_refinements.push(rfn);
+                } else {
+                    return Err(TranslationError::UnknownError(format!(
+                        "No refinement annotated for field {:?}",
+                        f_name
+                    )));
+                }
             }
         }
 
@@ -1515,8 +1541,23 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
             //"RefinedRust does currently not support associated types".to_string()}),
             //TyKind::Opaque(..) => Err(TranslationError::UnsupportedType {description:
             //"RefinedRust does currently not support returning impls".to_string()}),
-            _ => Err(TranslationError::UnsupportedType {
-                description: format!("Unknown unsupported type {}", ty),
+            TyKind::GeneratorWitnessMIR(_, _) => Err(TranslationError::UnsupportedType {
+                description: "RefinedRust does currently not support generators".to_string(),
+            }),
+            TyKind::Alias(kind, ty) => Err(TranslationError::UnsupportedType {
+                description: "RefinedRust does not support Alias types".to_string(),
+            }),
+            TyKind::Bound(_, _) => Err(TranslationError::UnsupportedType {
+                description: "RefinedRust does not support higher-ranked types".to_string(),
+            }),
+            TyKind::Placeholder(_) => Err(TranslationError::UnsupportedType {
+                description: "RefinedRust does not support higher-ranked types".to_string(),
+            }),
+            TyKind::Infer(_) => Err(TranslationError::UnsupportedType {
+                description: "RefinedRust does not support infer types".to_string(),
+            }),
+            TyKind::Error(_) => Err(TranslationError::UnsupportedType {
+                description: "RefinedRust does not support higher-ranked types".to_string(),
             }),
         }
     }