Skip to content

Commit

Permalink
Cleanup
Browse files Browse the repository at this point in the history
  • Loading branch information
@voidc
voidc committed Oct 13, 2023
1 parent 90fda6e commit 8d2f2a2
Show file tree
Hide file tree
Showing 2 changed files with 39 additions and 37 deletions.
26 changes: 14 additions & 12 deletions creusot/src/translation/function/terminator.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -77,18 +77,7 @@ impl<'tcx> BodyTranslator<'_, 'tcx> {
let TyKind::Closure(def_id, _) = ty.kind() else { panic!() };
let mut assertion = self.assertions.remove(def_id).unwrap();
assertion.subst(&inv_subst(self.body, &self.locals, terminator.source_info));

if let Some(resolver) = &mut self.resolver {
let frozen = resolver.frozen_locals_before(location);
let free_vars = assertion.free_vars();
for f in frozen.iter() {
if free_vars.contains(&self.locals[&f]) {
let msg = format!("Use of borrowed variable {}", self.locals[&f]);
self.ctx.crash_and_error(assertion.span, &msg);
}
}
}

self.check_ghost_term(&assertion, location);
self.emit_ghost_assign(*destination, assertion);
self.emit_terminator(Terminator::Goto(target.unwrap()));
return;
Expand Down Expand Up @@ -191,6 +180,19 @@ impl<'tcx> BodyTranslator<'_, 'tcx> {
_ => unreachable!("Resume assertions"),
}
}

fn check_ghost_term(&mut self, term: &Term<'tcx>, location: Location) {
if let Some(resolver) = &mut self.resolver {
let frozen = resolver.frozen_locals_before(location);
let free_vars = term.free_vars();
for f in frozen.iter() {
if free_vars.contains(&self.locals[&f]) {
let msg = format!("Use of borrowed variable {}", self.locals[&f]);
self.ctx.crash_and_error(term.span, &msg);
}
}
}
}
}

pub(crate) fn resolve_function<'tcx>(
Expand Down
50 changes: 25 additions & 25 deletions creusot/src/translation/pearlite.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1358,11 +1358,11 @@ impl<'tcx> Term<'tcx> {

pub(crate) fn free_vars(&self) -> HashSet<Symbol> {
let mut free = HashSet::new();
self.free(&HashSet::new(), &mut free);
self.free_vars_inner(&HashSet::new(), &mut free);
free
}

fn free(&self, bound: &HashSet<Symbol>, free: &mut HashSet<Symbol>) {
fn free_vars_inner(&self, bound: &HashSet<Symbol>, free: &mut HashSet<Symbol>) {
match &self.kind {
TermKind::Var(v) => {
if !bound.contains(v) {
Expand All @@ -1372,70 +1372,70 @@ impl<'tcx> Term<'tcx> {
TermKind::Lit(_) => {}
TermKind::Item(_, _) => {}
TermKind::Binary { lhs, rhs, .. } => {
lhs.free(bound, free);
rhs.free(bound, free)
lhs.free_vars_inner(bound, free);
rhs.free_vars_inner(bound, free)
}
TermKind::Unary { arg, .. } => arg.free(bound, free),
TermKind::Unary { arg, .. } => arg.free_vars_inner(bound, free),
TermKind::Forall { binder, body } => {
let mut bound = bound.clone();
bound.insert(binder.0);

body.free(&bound, free);
body.free_vars_inner(&bound, free);
}
TermKind::Exists { binder, body } => {
let mut bound = bound.clone();
bound.insert(binder.0);

body.free(&bound, free);
body.free_vars_inner(&bound, free);
}
TermKind::Call { fun, args, .. } => {
fun.free(bound, free);
fun.free_vars_inner(bound, free);
for arg in args {
arg.free(bound, free);
arg.free_vars_inner(bound, free);
}
}
TermKind::Constructor { fields, .. } => {
for field in fields {
field.free(bound, free);
field.free_vars_inner(bound, free);
}
}
TermKind::Tuple { fields } => {
for field in fields {
field.free(bound, free);
field.free_vars_inner(bound, free);
}
}
TermKind::Cur { term } => term.free(bound, free),
TermKind::Fin { term } => term.free(bound, free),
TermKind::Cur { term } => term.free_vars_inner(bound, free),
TermKind::Fin { term } => term.free_vars_inner(bound, free),
TermKind::Impl { lhs, rhs } => {
lhs.free(bound, free);
rhs.free(bound, free)
lhs.free_vars_inner(bound, free);
rhs.free_vars_inner(bound, free)
}
TermKind::Match { scrutinee, arms } => {
scrutinee.free(bound, free);
scrutinee.free_vars_inner(bound, free);
let mut bound = bound.clone();

for (pat, arm) in arms {
pat.binds(&mut bound);
arm.free(&bound, free);
arm.free_vars_inner(&bound, free);
}
}
TermKind::Let { pattern, arg, body } => {
arg.free(bound, free);
arg.free_vars_inner(bound, free);
let mut bound = bound.clone();
pattern.binds(&mut bound);
body.free(&bound, free);
body.free_vars_inner(&bound, free);
}
TermKind::Projection { lhs, .. } => lhs.free(bound, free),
TermKind::Old { term } => term.free(bound, free),
TermKind::Projection { lhs, .. } => lhs.free_vars_inner(bound, free),
TermKind::Old { term } => term.free_vars_inner(bound, free),
TermKind::Closure { body } => {
body.free(&bound, free);
body.free_vars_inner(&bound, free);
}
TermKind::Absurd => {}
TermKind::Reborrow { cur, fin } => {
cur.free(bound, free);
fin.free(bound, free)
cur.free_vars_inner(bound, free);
fin.free_vars_inner(bound, free)
}
TermKind::Assert { cond } => cond.free(bound, free),
TermKind::Assert { cond } => cond.free_vars_inner(bound, free),
}
}
}

0 comments on commit 8d2f2a2

Please sign in to comment.