Skip to content

Commit

Permalink
Remove the Cannot fetch THIR body error message (#1309)
Browse files Browse the repository at this point in the history
  • Loading branch information
@arnaudgolfouse
arnaudgolfouse authored Dec 24, 2024
2 parents 4ec5565 + f554cd0 commit c373377
Show file tree
Hide file tree
Showing 25 changed files with 357 additions and 285 deletions.
15 changes: 7 additions & 8 deletions creusot/src/backend.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ use rustc_span::{RealFileName, Span};
use crate::{
contracts_items::{is_resolve_function, is_spec, is_trusted},
ctx::{ItemType, TranslatedItem, TranslationCtx},
error::CannotFetchThir,
naming::ModulePath,
options::SpanMode,
run_why3::SpanMap,
Expand Down Expand Up @@ -52,7 +53,7 @@ impl<'tcx> Why3Generator<'tcx> {
Why3Generator { ctx, functions: Default::default(), span_map: Default::default() }
}

pub(crate) fn translate(&mut self, def_id: DefId) {
pub(crate) fn translate(&mut self, def_id: DefId) -> Result<(), CannotFetchThir> {
debug!("translating {:?}", def_id);

// eprintln!("{:?}", self.param_env(def_id));
Expand All @@ -66,7 +67,7 @@ impl<'tcx> Why3Generator<'tcx> {
self.functions.push(TranslatedItem::Logic { proof_modl: None });
}
ItemType::Logic { .. } | ItemType::Predicate { .. } => {
let proof_modl = logic::translate_logic_or_predicate(self, def_id);
let proof_modl = logic::translate_logic_or_predicate(self, def_id)?;
self.functions.push(TranslatedItem::Logic { proof_modl });
}
ItemType::Program => {
Expand All @@ -80,9 +81,10 @@ impl<'tcx> Why3Generator<'tcx> {
),
_ => (),
}
Ok(())
}

pub(crate) fn modules<'a>(&'a mut self) -> impl Iterator<Item = TranslatedItem> + 'a {
pub(crate) fn modules(&mut self) -> impl Iterator<Item = TranslatedItem> + '_ {
self.functions.drain(..)
}

Expand Down Expand Up @@ -148,11 +150,8 @@ impl<'tcx> Why3Generator<'tcx> {
None => return None, // The last segment is CrateRoot. Skip it.
Some(parent_id) => parent_id,
};
match key.disambiguated_data.data {
rustc_hir::definitions::DefPathData::Impl => {
return Some(display_impl_subject(&tcx.impl_subject(id).skip_binder()))
}
_ => {}
if key.disambiguated_data.data == rustc_hir::definitions::DefPathData::Impl {
return Some(display_impl_subject(&tcx.impl_subject(id).skip_binder()));
}
id.index = parent_id;
}
Expand Down
25 changes: 8 additions & 17 deletions creusot/src/backend/clone_map/elaborator.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -130,7 +130,7 @@ impl DepElab for ProgElab {
};

let coma = program::to_why(ctx, &mut names, name, bid);
return vec![Decl::Coma(coma)];
vec![Decl::Coma(coma)]
}
}

Expand Down Expand Up @@ -289,23 +289,18 @@ impl<'a, 'tcx> Expander<'a, 'tcx> {
param_env: ParamEnv<'tcx>,
initial: impl Iterator<Item = Dependency<'tcx>>,
) -> Self {
let exp = Self {
Self {
graph: Default::default(),
namer,
self_key,
param_env,
expansion_queue: initial.map(|b| (self_key, Strength::Strong, b)).collect(),
dep_bodies: Default::default(),
};
exp
}
}

fn namer(&mut self, source: Dependency<'tcx>) -> ExpansionProxy<'_, 'tcx> {
ExpansionProxy {
namer: &mut self.namer,
expansion_queue: &mut self.expansion_queue,
source,
}
ExpansionProxy { namer: self.namer, expansion_queue: &mut self.expansion_queue, source }
}

/// Expand the graph with new entries
Expand Down Expand Up @@ -421,11 +416,7 @@ fn expand_laws<'tcx>(
}
}

fn val<'tcx>(
ctx: &mut Why3Generator<'tcx>,
mut sig: Signature,
kind: Option<DeclKind>,
) -> Vec<Decl> {
fn val(ctx: &mut Why3Generator, mut sig: Signature, kind: Option<DeclKind>) -> Vec<Decl> {
sig.contract.variant = Vec::new();
if let Some(k) = kind {
let ax = if !sig.contract.is_empty() { Some(spec_axiom(&sig)) } else { None };
Expand Down Expand Up @@ -473,7 +464,7 @@ fn resolve_term<'tcx>(
}
traits::TraitResolved::UnknownFound | traits::TraitResolved::UnknownNotFound => {
// We don't know the instance => body is opaque
return None;
None
}
traits::TraitResolved::NoInstance => {
// We know there is no instance => body is true
Expand Down Expand Up @@ -603,7 +594,7 @@ fn term<'tcx>(
let ty = ctx.type_of(def_id).instantiate(ctx.tcx, subst);
let ty = ctx.tcx.normalize_erasing_regions(param_env, ty);
let span = ctx.def_span(def_id);
let res = from_ty_const(&mut ctx.ctx, constant, ty, param_env, span);
let res = from_ty_const(&ctx.ctx, constant, ty, param_env, span);
Some(res)
} else if is_resolve_function(ctx.tcx, def_id) {
resolve_term(ctx, param_env, def_id, subst)
Expand All @@ -623,7 +614,7 @@ fn term<'tcx>(
let TyKind::Closure(did, _) = subst.type_at(1).kind() else { return None };
Some(ctx.closure_contract(*did).unnest.clone().unwrap())
} else {
let term = ctx.term(def_id).unwrap().clone();
let term = ctx.term_fail_fast(def_id).unwrap().clone();
let term = normalize(
ctx.tcx,
param_env,
Expand Down
33 changes: 16 additions & 17 deletions creusot/src/backend/logic.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,12 +12,11 @@ mod vcgen;

use self::vcgen::vc;

use super::{is_trusted_function, signature::signature_of, term::lower_pure, Why3Generator};
use super::{
is_trusted_function, signature::signature_of, term::lower_pure, CannotFetchThir, Why3Generator,
};

pub(crate) fn binders_to_args(
ctx: &mut Why3Generator,
binders: Vec<Binder>,
) -> (Vec<Ident>, Vec<Binder>) {
pub(crate) fn binders_to_args(binders: Vec<Binder>) -> (Vec<Ident>, Vec<Binder>) {
let mut args = Vec::new();
let mut out_binders = Vec::new();
let mut fresh = 0;
Expand All @@ -30,11 +29,11 @@ pub(crate) fn binders_to_args(
}
Binder::UnNamed(_) => unreachable!("unnamed parameter in logical function signature"),
Binder::Named(ref nm) => {
args.push(nm.clone().into());
args.push(nm.clone());
out_binders.push(b);
}
Binder::Typed(ghost, binders, ty) => {
let (inner_args, inner_binders) = binders_to_args(ctx, binders);
let (inner_args, inner_binders) = binders_to_args(binders);
args.extend(inner_args);
out_binders.push(Binder::Typed(ghost, inner_binders, ty));
}
Expand All @@ -43,16 +42,16 @@ pub(crate) fn binders_to_args(
(args, out_binders)
}

pub(crate) fn translate_logic_or_predicate<'tcx>(
ctx: &mut Why3Generator<'tcx>,
pub(crate) fn translate_logic_or_predicate(
ctx: &mut Why3Generator,
def_id: DefId,
) -> Option<FileModule> {
) -> Result<Option<FileModule>, CannotFetchThir> {
let mut names = Dependencies::new(ctx, def_id);

// Check that we don't have both `builtins` and a contract at the same time (which are contradictory)
if get_builtin(ctx.tcx, def_id).is_some() {
if signature_of(ctx, &mut names, "".into(), def_id).contract.is_empty() {
return None;
return Ok(None);
}

ctx.crash_and_error(
Expand All @@ -69,14 +68,14 @@ pub(crate) fn translate_logic_or_predicate<'tcx>(
|| is_trusted_function(ctx.tcx, def_id)
|| !ctx.has_body(def_id)
{
return None;
return Ok(None);
}

let term = ctx.ctx.term(def_id).unwrap().clone();
let term = ctx.ctx.term(def_id)?.unwrap().clone();

let mut body_decls = Vec::new();

let (arg_names, new_binders) = binders_to_args(ctx, sig.args);
let (arg_names, new_binders) = binders_to_args(sig.args);

let param_decls = arg_names.iter().zip(new_binders.iter()).map(|(nm, binder)| {
Decl::LogicDecl(LogicDecl {
Expand Down Expand Up @@ -129,7 +128,7 @@ pub(crate) fn translate_logic_or_predicate<'tcx>(
let meta = ctx.display_impl_of(def_id);
let path = ctx.module_path(def_id);
let name = path.why3_ident();
Some(FileModule { path, modl: Module { name, decls, attrs, meta } })
Ok(Some(FileModule { path, modl: Module { name, decls, attrs, meta } }))
}

pub(crate) fn lower_logical_defn<'tcx, N: Namer<'tcx>>(
Expand Down Expand Up @@ -234,8 +233,8 @@ fn limited_function_encode(
let lim_call = function_call(&lim_sig);
lim_sig.trigger = Some(Trigger::single(lim_call.clone()));
decls.push(Decl::LogicDecl(LogicDecl { kind, sig: lim_sig }));
decls.push(Decl::Axiom(definition_axiom(&sig, body, "def")));
decls.push(Decl::Axiom(definition_axiom(&sig, lim_call, "def_lim")));
decls.push(Decl::Axiom(definition_axiom(sig, body, "def")));
decls.push(Decl::Axiom(definition_axiom(sig, lim_call, "def_lim")));
}

pub(crate) fn spec_axiom(sig: &Signature) -> Axiom {
Expand Down
36 changes: 18 additions & 18 deletions creusot/src/backend/logic/vcgen.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -144,20 +144,20 @@ fn is_structurally_recursive(ctx: &mut Why3Generator<'_>, self_id: DefId, t: &Te
let mut binds = Default::default();
pattern.binds(&mut binds);
let old_smaller = self.smaller_than.clone();
self.smaller_than.retain(|nm, _| !binds.contains(&nm));
self.smaller_than.retain(|nm, _| !binds.contains(nm));
binds.into_iter().for_each(|b| self.smaller_than(b, arg));
self.visit_term(body);
self.smaller_than = old_smaller;
}

TermKind::Match { arms, scrutinee } => {
self.visit_term(&scrutinee);
self.visit_term(scrutinee);

for (pat, exp) in arms {
let mut binds = Default::default();
pat.binds(&mut binds);
let old_smaller = self.smaller_than.clone();
self.smaller_than.retain(|nm, _| !binds.contains(&nm));
self.smaller_than.retain(|nm, _| !binds.contains(nm));
binds.into_iter().for_each(|b| self.smaller_than(b, scrutinee));
self.visit_term(exp);
self.smaller_than = old_smaller;
Expand All @@ -176,7 +176,7 @@ fn is_structurally_recursive(ctx: &mut Why3Generator<'_>, self_id: DefId, t: &Te
orig_args,
};

s.visit_term(&t);
s.visit_term(t);

s.valid()
}
Expand Down Expand Up @@ -299,10 +299,10 @@ impl<'a, 'tcx> VCGen<'a, 'tcx> {
// BinOp::Or => self.build_vc(lhs, &|lhs| {
// Ok(Exp::if_(lhs, k(Exp::mk_true())?, self.build_vc(rhs, k)?,))
// }),
BinOp::Div => self.build_vc(&lhs, &|lhs| {
BinOp::Div => self.build_vc(lhs, &|lhs| {
self.build_vc(rhs, &|rhs| k(Exp::var("div").app(vec![lhs.clone(), rhs])))
}),
_ => self.build_vc(&lhs, &|lhs| {
_ => self.build_vc(lhs, &|lhs| {
self.build_vc(rhs, &|rhs| {
k(Exp::BinaryOp(binop_to_binop(*op), Box::new(lhs.clone()), Box::new(rhs)))
})
Expand Down Expand Up @@ -359,9 +359,9 @@ impl<'a, 'tcx> VCGen<'a, 'tcx> {
})
}
// VC( * T, Q) = VC(T, |t| Q(*t))
TermKind::Cur { term } => self.build_vc(&term, &|term| k(term.field("current"))),
TermKind::Cur { term } => self.build_vc(term, &|term| k(term.field("current"))),
// VC( ^ T, Q) = VC(T, |t| Q(^t))
TermKind::Fin { term } => self.build_vc(&term, &|term| k(term.field("final"))),
TermKind::Fin { term } => self.build_vc(term, &|term| k(term.field("final"))),
// VC(A -> B, Q) = VC(A, VC(B, Q(A -> B)))
TermKind::Impl { lhs, rhs } => self.build_vc(lhs, &|lhs| {
Ok(Exp::if_(lhs, self.build_vc(rhs, k)?, k(Exp::mk_true())?))
Expand All @@ -372,7 +372,7 @@ impl<'a, 'tcx> VCGen<'a, 'tcx> {
&& arms.len() == 2
&& arms.iter().all(|a| a.0.get_bool().is_some()) =>
{
self.build_vc(&scrutinee, &|scrut| {
self.build_vc(scrutinee, &|scrut| {
let mut arms: Vec<_> = arms
.iter()
.map(&|arm: &(Pattern<'tcx>, Term<'tcx>)| {
Expand Down Expand Up @@ -461,11 +461,11 @@ impl<'a, 'tcx> VCGen<'a, 'tcx> {
match pat {
Pattern::Constructor { variant, fields, substs } => {
let fields =
fields.into_iter().map(|pat| self.build_pattern_inner(bounds, pat)).collect();
fields.iter().map(|pat| self.build_pattern_inner(bounds, pat)).collect();
let substs = self.ctx.borrow().normalize_erasing_regions(self.param_env, *substs);
if self.ctx.borrow().def_kind(variant) == DefKind::Variant {
Pat::ConsP(self.names.borrow_mut().constructor(*variant, substs), fields)
} else if fields.len() == 0 {
} else if fields.is_empty() {
Pat::TupleP(vec![])
} else {
Pat::RecP(
Expand Down Expand Up @@ -500,9 +500,9 @@ impl<'a, 'tcx> VCGen<'a, 'tcx> {
Pat::mk_false()
}
}
Pattern::Tuple(pats) => Pat::TupleP(
pats.into_iter().map(|pat| self.build_pattern_inner(bounds, pat)).collect(),
),
Pattern::Tuple(pats) => {
Pat::TupleP(pats.iter().map(|pat| self.build_pattern_inner(bounds, pat)).collect())
}
Pattern::Deref { pointee, kind } => match kind {
PointerKind::Box | PointerKind::Shr => self.build_pattern_inner(bounds, pointee),
PointerKind::Mut => {
Expand All @@ -516,7 +516,7 @@ impl<'a, 'tcx> VCGen<'a, 'tcx> {
let occ = self.subst.borrow().occ(id);

if occ == 0 {
return id.clone();
id.clone()
} else {
Ident::from_string(format!("{}_{occ}", &**id))
}
Expand Down Expand Up @@ -574,7 +574,7 @@ impl<'a, 'tcx> VCGen<'a, 'tcx> {
let top_level_args = self.top_level_args();

let mut subst: Environment =
top_level_args.into_iter().zip(call_args.into_iter().cloned()).collect();
top_level_args.into_iter().zip(call_args.iter().cloned()).collect();
let orig_variant = self.self_sig().contract.variant.remove(0);
let mut rec_var_exp = orig_variant.clone();
rec_var_exp.subst(&mut subst);
Expand All @@ -588,7 +588,7 @@ impl<'a, 'tcx> VCGen<'a, 'tcx> {
/// Produces the top-level call expression for the function being verified
fn top_level_args(&self) -> Vec<Ident> {
let sig = self.self_sig();
let (arg_names, _) = binders_to_args(*self.ctx.borrow_mut(), sig.args);
let (arg_names, _) = binders_to_args(sig.args);
arg_names
}

Expand All @@ -613,7 +613,7 @@ pub(crate) fn get_func_name<'tcx>(
// Add dependency
names.value(id, subst);

QName::from_string(&a.as_str()).without_search_path()
QName::from_string(a.as_str()).without_search_path()
})
.unwrap_or_else(|| names.value(id, subst))
}
Loading

0 comments on commit c373377

Please sign in to comment.