Skip to content

Commit

Permalink
Merge pull request #992 from creusot-rs/clone-map-cleanup
Browse files Browse the repository at this point in the history 
Remove all naming from `elaborator`
  • Loading branch information
@xldenis
xldenis authored Apr 9, 2024
2 parents f8aa384 + 93d6e4e commit 6edb5c1
Show file tree
Hide file tree
Showing 101 changed files with 2,854 additions and 3,465 deletions.
36 changes: 26 additions & 10 deletions creusot/src/backend/clone_map.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -93,8 +93,6 @@ pub(crate) trait Namer<'tcx> {

fn ty(&mut self, def_id: DefId, subst: GenericArgsRef<'tcx>) -> QName;

fn real_ty(&mut self, ty: Ty<'tcx>) -> QName;

fn constructor(&mut self, def_id: DefId, subst: GenericArgsRef<'tcx>) -> QName;

fn ty_inv(&mut self, ty: Ty<'tcx>) -> QName;
Expand Down Expand Up @@ -144,11 +142,6 @@ impl<'tcx> Namer<'tcx> for Dependencies<'tcx> {
}
}

fn real_ty(&mut self, ty: Ty<'tcx>) -> QName {
let node = DepNode::Type(ty);
self.insert(node).qname()
}

fn constructor(&mut self, def_id: DefId, subst: GenericArgsRef<'tcx>) -> QName {
let type_id = match self.tcx.def_kind(def_id) {
DefKind::Closure | DefKind::Struct | DefKind::Enum | DefKind::Union => def_id,
Expand Down Expand Up @@ -284,8 +277,22 @@ impl<'tcx> CloneNames<'tcx> {
}
DepNode::Type(ty) if !matches!(ty.kind(), TyKind::Alias(_, _)) => {
let kind = if let Some((did, _)) = key.did() {
let modl = module_name(self.tcx, did);
let name = Symbol::intern(&*item_name(self.tcx, did, Namespace::TypeNS));
let (modl, name) = if let Some(why3_modl) = util::get_builtin(self.tcx, did) {
let qname = QName::from_string(why3_modl.as_str()).unwrap();
let name = qname.name.clone();
let modl = qname.module_ident().unwrap();
(Symbol::intern(&modl), Symbol::intern(&*name))
} else {
let modl: Symbol = if util::item_type(self.tcx, did) == ItemType::Closure {
Symbol::intern(&format!("{}_Type", module_name(self.tcx, did)))
} else {
module_name(self.tcx, did)
};

let name = Symbol::intern(&*item_name(self.tcx, did, Namespace::TypeNS));

(modl, name)
};

Kind::Used(modl, name)
} else {
Expand All @@ -295,6 +302,15 @@ impl<'tcx> CloneNames<'tcx> {
return kind;
}
_ => {
if let DepNode::Item(id, _) = key
&& let Some(why3_modl) = util::get_builtin(self.tcx, id)
{
let qname = QName::from_string(why3_modl.as_str()).unwrap();
let name = qname.name.clone();
let modl = qname.module_qname().name;
return Kind::Used(Symbol::intern(&*modl), Symbol::intern(&*name));
};

let base = key.base_ident(self.tcx);

Kind::Named(self.counts.freshen(base))
Expand Down Expand Up @@ -376,7 +392,7 @@ impl Kind {
fn ident(&self) -> Ident {
match self {
Kind::Named(nm) => nm.as_str().into(),
Kind::Used(_, _) => panic!("cannot get ident of used module"),
Kind::Used(_, _) => panic!("cannot get ident of used module {self:?}"),
}
}

Expand Down
76 changes: 42 additions & 34 deletions creusot/src/backend/clone_map/elaborator.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,12 +9,12 @@ use rustc_target::abi::FieldIdx;

use why3::{
declaration::{Axiom, Decl, LetDecl, LetKind, Signature, Use, ValDecl},
Ident, QName,
QName,
};

use crate::{
backend::{
dependency::ExtendedId,
dependency::{Dependency, ExtendedId},
logic::{lower_logical_defn, lower_pure_defn, sigs, spec_axiom},
signature::sig_to_why3,
term::lower_pure,
Expand All @@ -33,7 +33,7 @@ use super::{CloneNames, DepNode, Kind};

/// The symbol elaborator expands required definitions as symbols and definitions, effectively performing the clones itself.
pub(super) struct SymbolElaborator<'tcx> {
used_types: IndexSet<DefId>,
used_types: IndexSet<Symbol>,
_param_env: ParamEnv<'tcx>,
}

Expand Down Expand Up @@ -77,40 +77,57 @@ impl<'tcx> SymbolElaborator<'tcx> {
}
}

fn elaborate_ty<N: Namer<'tcx>>(
fn elaborate_ty(
&mut self,
ctx: &mut Why3Generator<'tcx>,
names: &mut N,
names: &mut SymNamer<'tcx>,
ty: Ty<'tcx>,
) -> Vec<Decl> {
let Some((def_id, subst)) = DepNode::Type(ty).did() else { return Vec::new() };

match ty.kind() {
TyKind::Alias(_, _) => vec![ctx.assoc_ty_decl(names, def_id, subst)],
_ => {
let use_decl = self.used_types.insert(def_id).then(|| {
if let Some(builtin) = get_builtin(ctx.tcx, def_id) {
let name = QName::from_string(&builtin.as_str()).unwrap().module_qname();
Use { name, as_: None, export: false }
} else {
let name = names.ty(def_id, subst);
let name = name.module_qname();
let mod_name: Ident =
if util::item_type(ctx.tcx, def_id) == ItemType::Closure {
format!("{}_Type", module_name(ctx.tcx, def_id)).into()
} else {
module_name(ctx.tcx, def_id).to_string().into()
};
Use { name: mod_name.into(), as_: Some(name), export: false }
}
});
use_decl.into_iter().map(Decl::UseDecl).collect()
if let Some(why3_modl) = util::get_builtin(ctx.tcx, def_id) {
let qname = QName::from_string(why3_modl.as_str()).unwrap();
let Kind::Used(modl, _) = names.insert(DepNode::Type(ty)) else {
return vec![];
};

self.used_types
.insert(*modl)
.then(|| {
let use_decl =
Use { as_: None, name: qname.module_qname(), export: false };

vec![Decl::UseDecl(use_decl)]
})
.unwrap_or_default()
} else {
self.emit_use(names, DepNode::Type(ty))
}
}
}
}

fn emit_use(&mut self, names: &mut SymNamer<'tcx>, dep: Dependency<'tcx>) -> Vec<Decl> {
if let k @ Kind::Used(modl, _) = names.insert(dep) {
self.used_types
.insert(*modl)
.then(|| {
let qname = k.qname();
let name = qname.module_qname();
let use_decl = Use { as_: Some(name.clone()), name, export: false };
vec![Decl::UseDecl(use_decl)]
})
.unwrap_or_default()
} else {
vec![]
}
}

fn elaborate_item(
&self,
&mut self,
ctx: &mut Why3Generator<'tcx>,
names: &mut SymNamer<'tcx>,
param_env: ParamEnv<'tcx>,
Expand All @@ -128,11 +145,7 @@ impl<'tcx> SymbolElaborator<'tcx> {
}

if let Kind::Used(_, _) = names.get(item) {
let qname = names.get(item).qname();
let name = qname.module_qname();
let use_decl = Use { as_: Some(name.clone()), name, export: false };

return vec![Decl::UseDecl(use_decl)];
return self.emit_use(names, item);
};

let mut pre_sig = EarlyBinder::bind(sig(ctx, item)).instantiate(ctx.tcx, subst);
Expand Down Expand Up @@ -287,7 +300,7 @@ impl<'tcx> SymNamer<'tcx> {
impl<'tcx> Namer<'tcx> for SymNamer<'tcx> {
fn value(&mut self, def_id: DefId, subst: GenericArgsRef<'tcx>) -> QName {
let node = DepNode::new(self.tcx, (def_id, subst));
self.get(node).ident().into()
self.get(node).qname()
}

fn ty(&mut self, def_id: DefId, subst: GenericArgsRef<'tcx>) -> QName {
Expand All @@ -303,11 +316,6 @@ impl<'tcx> Namer<'tcx> for SymNamer<'tcx> {
}
}

fn real_ty(&mut self, ty: Ty<'tcx>) -> QName {
let node = DepNode::Type(ty);
self.insert(node).ident().into()
}

fn constructor(&mut self, def_id: DefId, subst: GenericArgsRef<'tcx>) -> QName {
let type_id = match self.tcx.def_kind(def_id) {
DefKind::Closure | DefKind::Struct | DefKind::Enum | DefKind::Union => def_id,
Expand Down
8 changes: 4 additions & 4 deletions creusot/tests/should_fail/bug/01_resolve_unsoundness.mlcfg
View file
Original file line number Diff line number Diff line change
Expand Up @@ -103,17 +103,17 @@ module C01ResolveUnsoundness_MakeVecOfSize

axiom inv0 : forall x : Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global) . inv0 x = true
use seq.Seq
function shallow_model2 (self : borrowed (Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global))) : Seq.seq bool
function shallow_model1 (self : borrowed (Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global))) : Seq.seq bool

=
[#"../../../../../creusot-contracts/src/model.rs" 108 8 108 31] shallow_model0 ( * self)
val shallow_model2 (self : borrowed (Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global))) : Seq.seq bool
ensures { result = shallow_model2 self }
val shallow_model1 (self : borrowed (Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global))) : Seq.seq bool
ensures { result = shallow_model1 self }

val push0 (self : borrowed (Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global))) (value : bool) : ()
requires {inv1 self}
requires {inv2 value}
ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 78 26 78 51] shallow_model0 ( ^ self) = Seq.snoc (shallow_model2 self) value }
ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 78 26 78 51] shallow_model0 ( ^ self) = Seq.snoc (shallow_model1 self) value }

val new0 (_1 : ()) : Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global)
ensures { [#"../../../../../creusot-contracts/src/std/vec.rs" 68 26 68 44] Seq.length (shallow_model0 result) = 0 }
Expand Down
1 change: 0 additions & 1 deletion creusot/tests/should_fail/bug/222.mlcfg
View file
Original file line number Diff line number Diff line change
Expand Up @@ -77,7 +77,6 @@ module C222_UsesInvariant
ensures { [#"../../../../../creusot-contracts/src/std/option.rs" 29 0 126 1] result = * self /\ ^ self = Core_Option_Option_Type.C_None }
ensures { inv0 result }

use C222_Once_Type as C222_Once_Type
let rec cfg uses_invariant [#"../222.rs" 40 0 40 41] [@cfg:stackify] [@cfg:subregion_analysis] (x : borrowed (C222_Once_Type.t_once t)) : ()
requires {[#"../222.rs" 38 11 38 24] invariant0 ( * x)}
requires {[#"../222.rs" 40 25 40 26] inv1 x}
Expand Down
Loading

0 comments on commit 6edb5c1

Please sign in to comment.