Merge pull request #284 from Nadrieril/charon-lib

charon/Cargo.toml

@@ -39,7 +39,8 @@ petgraph = "0.6.2"
 pretty = "0.12"
 regex = "1.7.1"
 rustc_version = "0.4"
-serde_json = "1.0.91"
+serde_json = { version = "1.0.91", features = ["unbounded_depth"] }
+serde_stacker = "0.1.11"
 serde = { version = "1.0.152", features = ["derive"] }
 stacker = "0.1"
 take_mut = "0.2.2"

charon/Charon.toml

@@ -6,5 +6,4 @@ opaque_modules = [
     "ids",
     "logger",
     "pretty",
-    "translate",
 ]

charon/src/ast/assumed.rs

@@ -54,7 +54,7 @@ pub static PTR_NON_NULL_NAME: [&str; 3] = ["core", "ptr", "NonNull"];
 /// - some of the ids here are actually traits, that we disambiguate later
 /// TODO: merge with the other enum?
 #[derive(Copy, Clone, EnumIsA)]
-pub(crate) enum BuiltinFun {
+pub enum BuiltinFun {
     Panic,
     BoxNew,
     BoxFree,
@@ -69,7 +69,7 @@ pub struct FunInfo {
 impl BuiltinFun {
     /// Converts to the ullbc equivalent. Panics if `self` is `Panic` as this should be handled
     /// separately.
-    pub(crate) fn to_ullbc_builtin_fun(self) -> ullbc_ast::AssumedFunId {
+    pub fn to_ullbc_builtin_fun(self) -> ullbc_ast::AssumedFunId {
         match self {
             BuiltinFun::BoxNew => ullbc_ast::AssumedFunId::BoxNew,
             BuiltinFun::BoxFree => ullbc_ast::AssumedFunId::BoxFree,
@@ -78,7 +78,7 @@ impl BuiltinFun {
     }
 
     /// Parse a name to recognize built-in functions.
-    pub(crate) fn parse_name(name: &Name) -> Option<Self> {
+    pub fn parse_name(name: &Name) -> Option<Self> {
         if PANIC_NAMES.iter().any(|panic| name.equals_ref_name(panic)) {
             Some(BuiltinFun::Panic)
         } else if name.equals_ref_name(&["alloc", "alloc", "box_free"]) {
@@ -125,7 +125,7 @@ impl BuiltinFun {
     }
 
     /// See the comments for [type_to_used_params]
-    pub(crate) fn to_fun_info(self) -> Option<FunInfo> {
+    pub fn to_fun_info(self) -> Option<FunInfo> {
         match self {
             BuiltinFun::Panic => None,
             BuiltinFun::BoxNew => None,

charon/src/ast/expressions.rs

@@ -2,7 +2,6 @@
 
 use crate::gast::{FunDeclId, TraitItemName};
 use crate::types::*;
-pub use crate::values::VarId;
 use crate::values::*;
 use derive_visitor::{Drive, DriveMut};
 use macros::{EnumAsGetters, EnumIsA, EnumToGetters, VariantIndexArity, VariantName};

charon/src/ast/expressions_utils.rs

@@ -1,5 +1,6 @@
 //! This file groups everything which is linked to implementations about [crate::expressions]
 use crate::expressions::*;
+use crate::values::*;
 use std::vec::Vec;
 
 impl Place {

charon/src/ast/gast.rs

@@ -1,29 +1,25 @@
 //! Definitions common to [crate::ullbc_ast] and [crate::llbc_ast]
-pub use crate::expressions::*;
-pub use crate::gast_utils::*;
+pub use super::gast_utils::*;
+use crate::expressions::*;
 use crate::generate_index_type;
 use crate::ids::Vector;
 use crate::llbc_ast;
 use crate::meta::{ItemMeta, Span};
 use crate::names::Name;
-pub use crate::types::GlobalDeclId;
-pub use crate::types::TraitClauseId;
 use crate::types::*;
-pub use crate::types::{
-    GenericArgs, GenericParams, TraitDeclId, TraitImplId, TraitInstanceId, TraitRef,
-};
 use crate::ullbc_ast;
+use crate::values::*;
 use derive_visitor::{Drive, DriveMut, Event, Visitor, VisitorMut};
 use macros::EnumIsA;
 use macros::EnumToGetters;
+use rustc_span::def_id::{CrateNum, DefId, DefIndex};
 use serde::{Deserialize, Serialize};
 
 generate_index_type!(FunDeclId, "Fun");
 generate_index_type!(BodyId, "Body");
 
 /// For use when deserializing.
-fn dummy_def_id() -> rustc_hir::def_id::DefId {
-    use rustc_hir::def_id::*;
+fn dummy_def_id() -> DefId {
     DefId {
         krate: CrateNum::MAX,
         index: DefIndex::MAX,
@@ -149,7 +145,7 @@ pub struct FunDecl {
     #[serde(skip)]
     #[drive(skip)]
     #[serde(default = "dummy_def_id")]
-    pub rust_id: rustc_hir::def_id::DefId,
+    pub rust_id: DefId,
     /// The meta data associated with the declaration.
     pub item_meta: ItemMeta,
     /// The signature contains the inputs/output types *with* non-erased regions.
@@ -171,7 +167,7 @@ pub struct GlobalDecl {
     #[serde(skip)]
     #[drive(skip)]
     #[serde(default = "dummy_def_id")]
-    pub rust_id: rustc_hir::def_id::DefId,
+    pub rust_id: DefId,
     /// The meta data associated with the declaration.
     pub item_meta: ItemMeta,
     pub generics: GenericParams,

charon/src/ast/gast_utils.rs

@@ -1,9 +1,8 @@
 //! Implementations for [crate::gast]
 
-use crate::gast::*;
+use crate::ast::*;
 use crate::ids::Vector;
 use crate::llbc_ast;
-use crate::types::*;
 use crate::ullbc_ast;
 
 /// Makes a lambda that generates a new variable id, pushes a new variable in
@@ -19,7 +18,7 @@ pub fn make_locals_generator(locals: &mut Vector<VarId, Var>) -> impl FnMut(Ty)
 }
 
 impl FunIdOrTraitMethodRef {
-    pub(crate) fn mk_assumed(aid: AssumedFunId) -> Self {
+    pub fn mk_assumed(aid: AssumedFunId) -> Self {
         Self::Fun(FunId::Assumed(aid))
     }
 }

charon/src/ast/krate.rs

@@ -0,0 +1,172 @@
+use crate::formatter::{FmtCtx, Formatter, IntoFormatter};
+use crate::gast::*;
+use crate::ids::{Generator, Vector};
+use crate::meta::{FileId, FileName, LocalFileId, VirtualFileId};
+use crate::reorder_decls::DeclarationsGroups;
+use crate::types::*;
+use derive_visitor::{Drive, DriveMut};
+use linked_hash_set::LinkedHashSet;
+use macros::{EnumAsGetters, EnumIsA, VariantIndexArity, VariantName};
+use rustc_span::def_id::DefId;
+use serde::{Deserialize, Serialize};
+use std::cmp::{Ord, PartialOrd};
+use std::collections::HashMap;
+use std::fmt;
+
+/// The id of a translated item.
+#[derive(
+    Copy,
+    Clone,
+    Debug,
+    PartialOrd,
+    Ord,
+    PartialEq,
+    Eq,
+    Hash,
+    EnumIsA,
+    EnumAsGetters,
+    VariantName,
+    VariantIndexArity,
+    Serialize,
+    Deserialize,
+    Drive,
+    DriveMut,
+)]
+#[charon::rename("AnyDeclId")]
+#[charon::variants_prefix("Id")]
+pub enum AnyTransId {
+    Type(TypeDeclId),
+    Fun(FunDeclId),
+    Global(GlobalDeclId),
+    TraitDecl(TraitDeclId),
+    TraitImpl(TraitImplId),
+}
+
+/// Implement `TryFrom`  and `From` to convert between an enum and its variants.
+macro_rules! wrap_unwrap_enum {
+    ($enum:ident::$variant:ident($variant_ty:ident)) => {
+        impl TryFrom<$enum> for $variant_ty {
+            type Error = ();
+            fn try_from(x: $enum) -> Result<Self, Self::Error> {
+                match x {
+                    $enum::$variant(x) => Ok(x),
+                    _ => Err(()),
+                }
+            }
+        }
+
+        impl From<$variant_ty> for $enum {
+            fn from(x: $variant_ty) -> Self {
+                $enum::$variant(x)
+            }
+        }
+    };
+}
+
+wrap_unwrap_enum!(AnyTransId::Fun(FunDeclId));
+wrap_unwrap_enum!(AnyTransId::Global(GlobalDeclId));
+wrap_unwrap_enum!(AnyTransId::Type(TypeDeclId));
+wrap_unwrap_enum!(AnyTransId::TraitDecl(TraitDeclId));
+wrap_unwrap_enum!(AnyTransId::TraitImpl(TraitImplId));
+
+/// A translated item.
+#[derive(Debug, Clone, Copy, EnumIsA, EnumAsGetters, VariantName, VariantIndexArity)]
+pub enum AnyTransItem<'ctx> {
+    Type(&'ctx TypeDecl),
+    Fun(&'ctx FunDecl),
+    Global(&'ctx GlobalDecl),
+    TraitDecl(&'ctx TraitDecl),
+    TraitImpl(&'ctx TraitImpl),
+}
+
+/// The data of a translated crate.
+#[derive(Default)]
+pub struct TranslatedCrate {
+    /// The name of the crate.
+    pub crate_name: String,
+
+    /// File names to ids and vice-versa
+    pub file_to_id: HashMap<FileName, FileId>,
+    pub id_to_file: HashMap<FileId, FileName>,
+    pub real_file_counter: Generator<LocalFileId>,
+    pub virtual_file_counter: Generator<VirtualFileId>,
+
+    /// All the ids, in the order in which we encountered them
+    pub all_ids: LinkedHashSet<AnyTransId>,
+    /// The map from rustc id to translated id.
+    pub id_map: HashMap<DefId, AnyTransId>,
+    /// The reverse map of ids.
+    pub reverse_id_map: HashMap<AnyTransId, DefId>,
+
+    /// The translated type definitions
+    pub type_decls: Vector<TypeDeclId, TypeDecl>,
+    /// The translated function definitions
+    pub fun_decls: Vector<FunDeclId, FunDecl>,
+    /// The translated global definitions
+    pub global_decls: Vector<GlobalDeclId, GlobalDecl>,
+    /// The bodies of functions and constants
+    pub bodies: Vector<BodyId, Body>,
+    /// The translated trait declarations
+    pub trait_decls: Vector<TraitDeclId, TraitDecl>,
+    /// The translated trait declarations
+    pub trait_impls: Vector<TraitImplId, TraitImpl>,
+    /// The re-ordered groups of declarations, initialized as empty.
+    pub ordered_decls: Option<DeclarationsGroups>,
+}
+
+impl TranslatedCrate {
+    pub fn get_item(&self, trans_id: AnyTransId) -> Option<AnyTransItem<'_>> {
+        match trans_id {
+            AnyTransId::Type(id) => self.type_decls.get(id).map(AnyTransItem::Type),
+            AnyTransId::Fun(id) => self.fun_decls.get(id).map(AnyTransItem::Fun),
+            AnyTransId::Global(id) => self.global_decls.get(id).map(AnyTransItem::Global),
+            AnyTransId::TraitDecl(id) => self.trait_decls.get(id).map(AnyTransItem::TraitDecl),
+            AnyTransId::TraitImpl(id) => self.trait_impls.get(id).map(AnyTransItem::TraitImpl),
+        }
+    }
+}
+
+impl fmt::Display for TranslatedCrate {
+    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
+        let fmt: FmtCtx = self.into_fmt();
+        match &self.ordered_decls {
+            None => {
+                // We do simple: types, globals, traits, functions
+                for d in &self.type_decls {
+                    writeln!(f, "{}\n", fmt.format_object(d))?
+                }
+                for d in &self.global_decls {
+                    writeln!(f, "{}\n", fmt.format_object(d))?
+                }
+                for d in &self.trait_decls {
+                    writeln!(f, "{}\n", fmt.format_object(d))?
+                }
+                for d in &self.trait_impls {
+                    writeln!(f, "{}\n", fmt.format_object(d))?
+                }
+                for d in &self.fun_decls {
+                    writeln!(f, "{}\n", fmt.format_object(d))?
+                }
+            }
+            Some(ordered_decls) => {
+                for gr in ordered_decls {
+                    for id in gr.get_ids() {
+                        writeln!(f, "{}\n", fmt.format_decl_id(id))?
+                    }
+                }
+            }
+        }
+        fmt::Result::Ok(())
+    }
+}
+
+impl<'tcx, 'ctx, 'a> IntoFormatter for &'a TranslatedCrate {
+    type C = FmtCtx<'a>;
+
+    fn into_fmt(self) -> Self::C {
+        FmtCtx {
+            translated: Some(self),
+            ..Default::default()
+        }
+    }
+}

charon/src/ast/llbc_ast.rs

@@ -6,12 +6,8 @@
 //! Also note that we completely break the definitions Statement and Terminator
 //! from MIR to use Statement only.
 
-pub use crate::gast::*;
-pub use crate::llbc_ast_utils::*;
-use crate::meta::Span;
-use crate::types::*;
-pub use crate::ullbc_ast::{Call, FunDeclId, GlobalDeclId, Var};
-use crate::values::*;
+pub use super::llbc_ast_utils::*;
+pub use crate::ast::*;
 use derive_visitor::{Drive, DriveMut};
 use macros::{EnumAsGetters, EnumIsA, EnumToGetters, VariantIndexArity, VariantName};
 use serde::{Deserialize, Serialize};

charon/src/ast/meta.rs

@@ -1,11 +1,11 @@
 //! Meta-information about programs (spans, etc.).
 
-pub use crate::meta_utils::*;
+pub use super::meta_utils::*;
 use crate::names::Name;
 use derive_visitor::{Drive, DriveMut};
-use hax_frontend_exporter::PathBuf;
 use macros::{EnumAsGetters, EnumIsA, EnumToGetters};
 use serde::{Deserialize, Serialize};
+use std::path::PathBuf;
 
 generate_index_type!(LocalFileId);
 generate_index_type!(VirtualFileId);