Skip to content

Commit

Permalink
Simplify the way builtins/imports are handled. (#1350)
Browse files Browse the repository at this point in the history
  • Loading branch information
@jhjourdan
jhjourdan authored Feb 7, 2025
2 parents 4cb864f + bac6b27 commit 5169c1e
Show file tree
Hide file tree
Showing 52 changed files with 698 additions and 789 deletions.
68 changes: 32 additions & 36 deletions creusot/src/backend/clone_map.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -53,30 +53,31 @@ pub enum PreludeModule {
}

impl PreludeModule {
pub fn qname(&self) -> QName {
match self {
PreludeModule::Float32 => QName::from_string("prelude.prelude.Float32"),
PreludeModule::Float64 => QName::from_string("prelude.prelude.Float64"),
PreludeModule::Int => QName::from_string("prelude.prelude.Int"),
PreludeModule::Int8 => QName::from_string("prelude.prelude.Int8"),
PreludeModule::Int16 => QName::from_string("prelude.prelude.Int16"),
PreludeModule::Int32 => QName::from_string("prelude.prelude.Int32"),
PreludeModule::Int64 => QName::from_string("prelude.prelude.Int64"),
PreludeModule::Int128 => QName::from_string("prelude.prelude.Int128"),
PreludeModule::UInt8 => QName::from_string("prelude.prelude.UInt8"),
PreludeModule::UInt16 => QName::from_string("prelude.prelude.UInt16"),
PreludeModule::UInt32 => QName::from_string("prelude.prelude.UInt32"),
PreludeModule::UInt64 => QName::from_string("prelude.prelude.UInt64"),
PreludeModule::UInt128 => QName::from_string("prelude.prelude.UInt128"),
PreludeModule::Char => QName::from_string("prelude.prelude.Char"),
PreludeModule::Opaque => QName::from_string("prelude.prelude.Opaque"),
PreludeModule::Isize => QName::from_string("prelude.prelude.IntSize"),
PreludeModule::Usize => QName::from_string("prelude.prelude.UIntSize"),
PreludeModule::Bool => QName::from_string("prelude.prelude.Bool"),
PreludeModule::Borrow => QName::from_string("prelude.prelude.Borrow"),
PreludeModule::Slice => QName::from_string("prelude.prelude.Slice"),
PreludeModule::Intrinsic => QName::from_string("prelude.prelude.Intrinsic"),
}
pub fn qname(&self) -> Vec<Ident> {
let qname: QName = match self {
PreludeModule::Float32 => "prelude.prelude.Float32.".into(),
PreludeModule::Float64 => "prelude.prelude.Float64.".into(),
PreludeModule::Int => "prelude.prelude.Int.".into(),
PreludeModule::Int8 => "prelude.prelude.Int8.".into(),
PreludeModule::Int16 => "prelude.prelude.Int16.".into(),
PreludeModule::Int32 => "prelude.prelude.Int32.".into(),
PreludeModule::Int64 => "prelude.prelude.Int64.".into(),
PreludeModule::Int128 => "prelude.prelude.Int128.".into(),
PreludeModule::UInt8 => "prelude.prelude.UInt8.".into(),
PreludeModule::UInt16 => "prelude.prelude.UInt16.".into(),
PreludeModule::UInt32 => "prelude.prelude.UInt32.".into(),
PreludeModule::UInt64 => "prelude.prelude.UInt64.".into(),
PreludeModule::UInt128 => "prelude.prelude.UInt128.".into(),
PreludeModule::Char => "prelude.prelude.Char.".into(),
PreludeModule::Opaque => "prelude.prelude.Opaque.".into(),
PreludeModule::Isize => "prelude.prelude.IntSize.".into(),
PreludeModule::Usize => "prelude.prelude.UIntSize.".into(),
PreludeModule::Bool => "prelude.prelude.Bool.".into(),
PreludeModule::Borrow => "prelude.prelude.Borrow.".into(),
PreludeModule::Slice => "prelude.prelude.Slice.".into(),
PreludeModule::Intrinsic => "prelude.prelude.Intrinsic.".into(),
};
qname.module
}
}

Expand Down Expand Up @@ -274,12 +275,11 @@ impl<'tcx> CloneNames<'tcx> {
if let Some((did, _)) = key.did()
&& let Some(why3_modl) = get_builtin(self.tcx, did)
{
let qname = QName::from_string(why3_modl.as_str());
let name = qname.name.clone();
if let Some(modl) = qname.module_qname() {
return Kind::UsedBuiltin(modl, Symbol::intern(&*name));
let qname = QName::from(why3_modl.as_str());
if qname.module.is_empty() {
return Kind::Named(Symbol::intern(&qname.name));
} else {
return Kind::Named(Symbol::intern(&*name));
return Kind::UsedBuiltin(qname);
}
}
key.base_ident(self.tcx)
Expand Down Expand Up @@ -308,15 +308,15 @@ pub enum Kind {
/// This symbol is locally defined
Named(Symbol),
/// Used, UsedBuiltin: the symbols in the last argument must be acompanied by a `use` statement in Why3
UsedBuiltin(QName, Symbol),
UsedBuiltin(QName),
}

impl Kind {
fn ident(&self) -> Ident {
match self {
Kind::Unnamed => panic!("Unnamed item"),
Kind::Named(nm) => nm.as_str().into(),
Kind::UsedBuiltin(_, _) => {
Kind::UsedBuiltin(_) => {
panic!("cannot get ident of used module {self:?}")
}
}
Expand All @@ -326,11 +326,7 @@ impl Kind {
match self {
Kind::Unnamed => panic!("Unnamed item"),
Kind::Named(nm) => nm.as_str().into(),
Kind::UsedBuiltin(modl, id) => {
let mut module = modl.module.clone();
module.push(modl.name.clone());
QName { module, name: id.as_str().into() }
}
Kind::UsedBuiltin(qname) => qname.clone().without_search_path(),
}
}
}
Expand Down
37 changes: 18 additions & 19 deletions creusot/src/backend/clone_map/elaborator.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -35,10 +35,7 @@ use rustc_middle::ty::{
};
use rustc_span::{Span, Symbol, DUMMY_SP};
use rustc_type_ir::{ConstKind, EarlyBinder};
use why3::{
declaration::{Axiom, Decl, DeclKind, LogicDecl, Signature, TyDecl, Use},
QName,
};
use why3::declaration::{Axiom, Decl, DeclKind, LogicDecl, Signature, TyDecl, Use};

/// Weak dependencies are allowed to form cycles in the graph, but strong ones cannot,
/// weak dependencies are used to perform an initial stratification of the dependency graph.
Expand Down Expand Up @@ -180,9 +177,18 @@ impl DepElab for LogicElab {
_ => None,
};

if let Some(b) = get_builtin(ctx.tcx, def_id) {
let Some(name) = QName::from_string(b.as_str()).module_qname() else { return vec![] };
return vec![Decl::UseDecl(Use { name, as_: None, export: false })];
if get_builtin(ctx.tcx, def_id).is_some() {
match elab.namer.insert(dep) {
Kind::Named(_) => return vec![],
Kind::UsedBuiltin(qname) => {
return vec![Decl::UseDecl(Use {
name: qname.module.clone(),
as_: None,
export: false,
})]
}
Kind::Unnamed => unreachable!(),
}
}

let sig = ctx.sig(def_id).clone();
Expand Down Expand Up @@ -226,7 +232,7 @@ fn expand_ty_inv_axiom<'tcx>(
let rewrite = elab.rewrite;
let exp = lower_pure(ctx, &mut names, &term);
let axiom =
Axiom { name: names.insert(Dependency::TyInvAxiom(ty)).qname().name, rewrite, axiom: exp };
Axiom { name: names.insert(Dependency::TyInvAxiom(ty)).ident(), rewrite, axiom: exp };
vec![Decl::Axiom(axiom)]
}

Expand Down Expand Up @@ -259,19 +265,12 @@ impl DepElab for TyElab {
}
TyKind::Closure(did, subst) => translate_closure_ty(ctx, &mut names, *did, subst)
.map_or(vec![], |d| vec![Decl::TyDecl(d)]),
TyKind::Adt(adt_def, subst)
if let Some(why3_modl) = get_builtin(ctx.tcx, adt_def.did()) =>
{
assert!(matches!(names.insert(dep), Kind::UsedBuiltin(_, _)));

TyKind::Adt(adt_def, subst) if get_builtin(ctx.tcx, adt_def.did()).is_some() => {
for ty in subst.types() {
translate_ty(ctx, &mut elab.namer(dep), DUMMY_SP, ty);
translate_ty(ctx, &mut names, DUMMY_SP, ty);
}

let qname = QName::from_string(why3_modl.as_str());
let Some(name) = qname.module_qname() else { return vec![] };
let use_decl = Use { as_: None, name, export: false };
vec![Decl::UseDecl(use_decl)]
let Kind::UsedBuiltin(qname) = names.insert(dep) else { unreachable!() };
vec![Decl::UseDecl(Use { as_: None, name: qname.module.clone(), export: false })]
}
TyKind::Adt(_, _) => {
let (def_id, subst) = dep.did().unwrap();
Expand Down
27 changes: 4 additions & 23 deletions creusot/src/backend/logic/vcgen.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,13 +17,13 @@ use crate::{
pearlite::{super_visit_term, Literal, Pattern, PointerKind, Term, TermVisitor},
};
use rustc_hir::{def::DefKind, def_id::DefId};
use rustc_middle::ty::{EarlyBinder, GenericArgsRef, Ty, TyKind, TypingEnv};
use rustc_middle::ty::{EarlyBinder, Ty, TyKind, TypingEnv};
use rustc_span::{Span, Symbol};
use why3::{
declaration::Signature,
exp::{BinOp, Environment},
ty::Type,
Exp, Ident, QName,
Exp, Ident,
};

/// Verification conditions for lemma functions.
Expand Down Expand Up @@ -236,8 +236,7 @@ impl<'a, 'tcx> VCGen<'a, 'tcx> {
// Items are just global names so
// VC(i, Q) = Q(i)
TermKind::Item(id, sub) => {
let item_name =
get_func_name(*self.ctx.borrow_mut(), *self.names.borrow_mut(), *id, sub);
let item_name = self.names.borrow_mut().value(*id, sub);

if get_builtin(self.ctx.borrow().tcx, *id).is_some() {
// Builtins can leverage Why3 polymorphism and sometimes can cause typeck errors in why3 due to ambiguous type variables so lets fix the type now.
Expand Down Expand Up @@ -265,8 +264,7 @@ impl<'a, 'tcx> VCGen<'a, 'tcx> {
.zip(args.clone())
.map(|(nm, res)| (ident_of(nm.0), res))
.collect();
let fname =
get_func_name(*self.ctx.borrow_mut(), *self.names.borrow_mut(), *id, subst);
let fname = self.names.borrow_mut().value(*id, subst);
let mut sig = sig_to_why3(
*self.ctx.borrow_mut(),
*self.names.borrow_mut(),
Expand Down Expand Up @@ -608,20 +606,3 @@ impl<'a, 'tcx> VCGen<'a, 'tcx> {
self.subst.borrow_mut().pop_subst();
}
}

// Push into `CloneMap::value`?
pub(crate) fn get_func_name<'tcx>(
ctx: &Why3Generator<'tcx>,
names: &mut Dependencies<'tcx>,
id: DefId,
subst: GenericArgsRef<'tcx>,
) -> QName {
get_builtin(ctx.tcx, id)
.map(|a| {
// Add dependency
names.value(id, subst);

QName::from_string(a.as_str()).without_search_path()
})
.unwrap_or_else(|| names.value(id, subst))
}
4 changes: 2 additions & 2 deletions creusot/src/backend/place.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -218,7 +218,7 @@ pub(crate) fn projections_to_expr<'tcx, 'a, N: Namer<'tcx>>(
let foc = focus.call(is);
is.push(IntermediateStmt::Call(
vec![Param::Term(result.clone(), elt_ty1.clone())],
Expr::Symbol(QName::from_string("Slice.get")),
Expr::Symbol(QName::from("Slice.get")),
vec![Arg::Ty(elt_ty1), Arg::Term(foc), Arg::Term(ix_exp1)],
));

Expand All @@ -232,7 +232,7 @@ pub(crate) fn projections_to_expr<'tcx, 'a, N: Namer<'tcx>>(

is.push(IntermediateStmt::Call(
vec![Param::Term(out.clone(), ty)],
Expr::Symbol(QName::from_string("Slice.set")),
Expr::Symbol(QName::from("Slice.set")),
vec![Arg::Ty(elt_ty), Arg::Term(foc), Arg::Term(ix_exp), Arg::Term(rhs)],
));
constructor(is, Exp::qvar(out.into()))
Expand Down
Loading

0 comments on commit 5169c1e

Please sign in to comment.