Merge pull request #544 from Nadrieril/check-bound-vars

charon/src/ast/krate.rs

@@ -3,6 +3,7 @@ use crate::formatter::{FmtCtx, Formatter, IntoFormatter};
 use crate::ids::Vector;
 use crate::reorder_decls::DeclarationsGroups;
 use derive_generic_visitor::{ControlFlow, Drive, DriveMut};
+use index_vec::Idx;
 use indexmap::IndexSet;
 use macros::{EnumAsGetters, EnumIsA, VariantIndexArity, VariantName};
 use serde::{Deserialize, Serialize};
@@ -317,6 +318,11 @@ impl<'tcx, 'ctx, 'a> IntoFormatter for &'a TranslatedCrate {
     }
 }
 
+pub trait HasVectorOf<Id: Idx>: std::ops::Index<Id, Output: Sized> {
+    fn get_vector(&self) -> &Vector<Id, Self::Output>;
+    fn get_vector_mut(&mut self) -> &mut Vector<Id, Self::Output>;
+}
+
 /// Delegate `Index` implementations to subfields.
 macro_rules! mk_index_impls {
     ($ty:ident.$field:ident[$idx:ty]: $output:ty) => {
@@ -331,6 +337,14 @@ macro_rules! mk_index_impls {
                 &mut self.$field[index]
             }
         }
+        impl HasVectorOf<$idx> for $ty {
+            fn get_vector(&self) -> &Vector<$idx, Self::Output> {
+                &self.$field
+            }
+            fn get_vector_mut(&mut self) -> &mut Vector<$idx, Self::Output> {
+                &mut self.$field
+            }
+        }
     };
 }
 pub(crate) use mk_index_impls;

charon/src/ast/types/vars.rs

@@ -1,8 +1,12 @@
 //! Type-level variables. There are 4 kinds of variables at the type-level: regions, types, const
 //! generics and trait clauses. The relevant definitions are in this module.
-use std::ops::{Index, IndexMut};
+use std::{
+    borrow::Borrow,
+    ops::{Index, IndexMut},
+};
 
 use derive_generic_visitor::{Drive, DriveMut};
+use index_vec::Idx;
 use serde::{Deserialize, Serialize};
 
 use crate::ast::*;
@@ -284,21 +288,37 @@ impl<T> BindingStack<T> {
     pub fn depth(&self) -> DeBruijnId {
         DeBruijnId::new(self.stack.len() - 1)
     }
+    /// Map a bound variable to ids binding depth.
+    pub fn as_bound_var<Id>(&self, var: DeBruijnVar<Id>) -> (DeBruijnId, Id) {
+        match var {
+            DeBruijnVar::Bound(dbid, varid) => (dbid, varid),
+            DeBruijnVar::Free(varid) => (self.depth(), varid),
+        }
+    }
     pub fn push(&mut self, x: T) {
         self.stack.push(x);
     }
     pub fn pop(&mut self) -> Option<T> {
         self.stack.pop()
     }
     /// Helper that computes the real index into `self.stack`.
-    fn real_index(&self, id: DeBruijnId) -> usize {
-        self.stack.len() - 1 - id.index
+    fn real_index(&self, id: DeBruijnId) -> Option<usize> {
+        self.stack.len().checked_sub(id.index + 1)
     }
     pub fn get(&self, id: DeBruijnId) -> Option<&T> {
-        self.stack.get(self.real_index(id))
+        self.stack.get(self.real_index(id)?)
+    }
+    pub fn get_var<'a, Id: Idx, Inner>(&'a self, var: DeBruijnVar<Id>) -> Option<&'a Inner::Output>
+    where
+        T: Borrow<Inner>,
+        Inner: HasVectorOf<Id> + 'a,
+    {
+        let (dbid, varid) = self.as_bound_var(var);
+        self.get(dbid)
+            .and_then(|x| x.borrow().get_vector().get(varid))
     }
     pub fn get_mut(&mut self, id: DeBruijnId) -> Option<&mut T> {
-        let index = self.real_index(id);
+        let index = self.real_index(id)?;
         self.stack.get_mut(index)
     }
     /// Iterate over the binding levels, from the innermost (0) out.
@@ -313,6 +333,11 @@ impl<T> BindingStack<T> {
             .enumerate()
             .map(|(i, x)| (DeBruijnId::new(i), x))
     }
+    pub fn map_ref<'a, U>(&'a self, f: impl FnMut(&'a T) -> U) -> BindingStack<U> {
+        BindingStack {
+            stack: self.stack.iter().map(f).collect(),
+        }
+    }
 
     pub fn innermost(&self) -> &T {
         self.stack.last().unwrap()

charon/src/ast/types_utils.rs

@@ -91,7 +91,7 @@ impl GenericParams {
                 .map_ref_indexed(|id, _| ConstGeneric::Var(DeBruijnVar::bound(depth, id))),
             trait_refs: self.trait_clauses.map_ref_indexed(|id, clause| TraitRef {
                 kind: TraitRefKind::Clause(DeBruijnVar::bound(depth, id)),
-                trait_decl_ref: clause.trait_.clone(),
+                trait_decl_ref: clause.trait_.clone().move_under_binders(depth),
             }),
             target,
         }
@@ -141,13 +141,11 @@ impl<T> RegionBinder<T> {
     where
         T: AstVisitable,
     {
-        let mut val = self.skip_binder;
         let args = GenericArgs {
             regions: self.regions.map_ref_indexed(|_, _| Region::Erased),
             ..GenericArgs::empty(GenericsSource::Builtin)
         };
-        val.drive_mut(&mut SubstVisitor::new(&args));
-        val
+        self.skip_binder.substitute(&args)
     }
 }
 
@@ -654,11 +652,11 @@ impl VisitAstMut for SubstVisitor<'_> {
         }
     }
 
-    fn exit_trait_ref(&mut self, tr: &mut TraitRef) {
-        match &mut tr.kind {
+    fn exit_trait_ref_kind(&mut self, kind: &mut TraitRefKind) {
+        match kind {
             TraitRefKind::Clause(var) => {
                 if let Some(new_tr) = self.process_var(var) {
-                    *tr = new_tr;
+                    *kind = new_tr.kind;
                 }
             }
             _ => (),
@@ -680,10 +678,12 @@ pub trait TyVisitable: Sized + AstVisitable {
 
     /// Move under `depth` binders.
     fn move_under_binders(mut self, depth: DeBruijnId) -> Self {
-        let Continue(()) = self.visit_db_id::<Infallible>(|id| {
-            *id = id.plus(depth);
-            Continue(())
-        });
+        if !depth.is_zero() {
+            let Continue(()) = self.visit_db_id::<Infallible>(|id| {
+                *id = id.plus(depth);
+                Continue(())
+            });
+        }
         self
     }
 

charon/src/bin/charon-driver/translate/translate_ctx.rs

@@ -1370,11 +1370,7 @@ impl<'tcx, 'ctx, 'a> IntoFormatter for &'a BodyTransCtx<'tcx, 'ctx> {
     fn into_fmt(self) -> Self::C {
         FmtCtx {
             translated: Some(&self.t_ctx.translated),
-            generics: self
-                .binding_levels
-                .iter()
-                .map(|bl| Cow::Borrowed(&bl.params))
-                .collect(),
+            generics: self.binding_levels.map_ref(|bl| Cow::Borrowed(&bl.params)),
             locals: Some(&self.locals),
         }
     }

charon/src/bin/charon/main.rs

@@ -187,6 +187,10 @@ pub fn main() -> anyhow::Result<()> {
         // Run just the driver.
         let mut cmd = driver_cmd()?;
 
+        for arg in std::mem::take(&mut options.rustc_args) {
+            cmd.arg(arg);
+        }
+
         cmd.env(CHARON_ARGS, serde_json::to_string(&options).unwrap());
 
         // Make sure the build target is explicitly set. This is needed to detect which crates are

charon/src/pretty/formatter.rs

@@ -1,5 +1,7 @@
 use std::borrow::Cow;
-use std::collections::VecDeque;
+use std::fmt::Display;
+
+use index_vec::Idx;
 
 use crate::ast::*;
 use crate::common::TAB_INCR;
@@ -80,7 +82,7 @@ impl<'a, 'b> SetGenerics<'a> for FmtCtx<'b> {
     fn set_generics(&'a self, generics: &'a GenericParams) -> Self::C {
         FmtCtx {
             translated: self.translated.as_deref(),
-            generics: [Cow::Borrowed(generics)].into(),
+            generics: BindingStack::new(Cow::Borrowed(generics)),
             locals: self.locals.as_deref(),
         }
     }
@@ -125,7 +127,7 @@ impl<'a, 'b> PushBinder<'a> for FmtCtx<'b> {
 
     fn push_binder(&'a self, new_params: Cow<'a, GenericParams>) -> Self::C {
         let mut generics = self.generics.clone();
-        generics.push_front(new_params);
+        generics.push(new_params);
         FmtCtx {
             translated: self.translated.as_deref(),
             generics,
@@ -170,7 +172,7 @@ pub struct FmtCtx<'a> {
     pub translated: Option<&'a TranslatedCrate>,
     /// Generics form a stack, where each binder introduces a new level. For DeBruijn indices to
     /// work, we keep the innermost parameters at the start of the vector.
-    pub generics: VecDeque<Cow<'a, GenericParams>>,
+    pub generics: BindingStack<Cow<'a, GenericParams>>,
     pub locals: Option<&'a Locals>,
 }
 
@@ -254,30 +256,42 @@ impl<'a> Formatter<AnyTransId> for FmtCtx<'a> {
     }
 }
 
-impl<'a> Formatter<RegionDbVar> for FmtCtx<'a> {
-    fn format_object(&self, var: RegionDbVar) -> String {
+impl<'a> FmtCtx<'a> {
+    fn format_bound_var<Id: Idx + Display, T>(
+        &self,
+        var: DeBruijnVar<Id>,
+        var_prefix: &str,
+        f: impl Fn(&T) -> Option<String>,
+    ) -> String
+    where
+        GenericParams: HasVectorOf<Id, Output = T>,
+    {
         if self.generics.is_empty() {
-            return format!("'_{var}");
+            return format!("{var_prefix}{var}");
         }
-        let (dbid, varid) = match var {
-            DeBruijnVar::Bound(dbid, varid) => (dbid.index, varid),
-            DeBruijnVar::Free(varid) => (self.generics.len() - 1, varid),
-        };
-        match self
-            .generics
-            .get(dbid)
-            .and_then(|generics| generics.regions.get(varid))
-        {
-            None => format!("wrong_region('_{var})"),
-            Some(v) => match &v.name {
-                Some(name) => name.to_string(),
-                None if dbid == self.generics.len() - 1 => format!("'_{varid}"),
-                None => format!("'_{var}"),
+        match self.generics.get_var::<_, GenericParams>(var) {
+            None => format!("missing({var_prefix}{var})"),
+            Some(v) => match f(v) {
+                Some(name) => name,
+                None => {
+                    let (dbid, varid) = self.generics.as_bound_var(var);
+                    if dbid == self.generics.depth() {
+                        format!("{var_prefix}{varid}")
+                    } else {
+                        format!("{var_prefix}{var}")
+                    }
+                }
             },
         }
     }
 }
 
+impl<'a> Formatter<RegionDbVar> for FmtCtx<'a> {
+    fn format_object(&self, var: RegionDbVar) -> String {
+        self.format_bound_var(var, "'_", |v| v.name.as_ref().map(|name| name.to_string()))
+    }
+}
+
 impl<'a> Formatter<&RegionVar> for FmtCtx<'a> {
     fn format_object(&self, var: &RegionVar) -> String {
         match &var.name {
@@ -289,62 +303,19 @@ impl<'a> Formatter<&RegionVar> for FmtCtx<'a> {
 
 impl<'a> Formatter<TypeDbVar> for FmtCtx<'a> {
     fn format_object(&self, var: TypeDbVar) -> String {
-        if self.generics.is_empty() {
-            return format!("@Type{var}");
-        }
-        let (dbid, varid) = match var {
-            DeBruijnVar::Bound(dbid, varid) => (dbid.index, varid),
-            DeBruijnVar::Free(varid) => (self.generics.len() - 1, varid),
-        };
-        match self
-            .generics
-            .get(dbid)
-            .and_then(|generics| generics.types.get(varid))
-        {
-            None => format!("missing_type_var({var})"),
-            Some(v) => v.to_string(),
-        }
+        self.format_bound_var(var, "@Type", |v| Some(v.to_string()))
     }
 }
 
 impl<'a> Formatter<ConstGenericDbVar> for FmtCtx<'a> {
     fn format_object(&self, var: ConstGenericDbVar) -> String {
-        if self.generics.is_empty() {
-            return format!("@ConstGeneric{var}");
-        }
-        let (dbid, varid) = match var {
-            DeBruijnVar::Bound(dbid, varid) => (dbid.index, varid),
-            DeBruijnVar::Free(varid) => (self.generics.len() - 1, varid),
-        };
-        match self
-            .generics
-            .get(dbid)
-            .and_then(|generics| generics.const_generics.get(varid))
-        {
-            None => format!("missing_cg_var({var})"),
-            Some(v) => v.fmt_with_ctx(self),
-        }
+        self.format_bound_var(var, "@ConstGeneric", |v| Some(v.fmt_with_ctx(self)))
     }
 }
 
 impl<'a> Formatter<ClauseDbVar> for FmtCtx<'a> {
     fn format_object(&self, var: ClauseDbVar) -> String {
-        if self.generics.is_empty() {
-            return format!("@TraitClause{var}");
-        }
-        let (dbid, varid) = match var {
-            DeBruijnVar::Bound(dbid, varid) => (dbid.index, varid),
-            DeBruijnVar::Free(varid) => (self.generics.len() - 1, varid),
-        };
-        match self
-            .generics
-            .get(dbid)
-            .and_then(|generics| generics.trait_clauses.get(varid))
-        {
-            None => format!("missing_clause_var({var})"),
-            Some(_) if dbid == self.generics.len() - 1 => format!("@TraitClause{varid}"),
-            Some(_) => format!("@TraitClause{var}"),
-        }
+        self.format_bound_var(var, "@TraitClause", |_| None)
     }
 }