Skip to content

Commit

Permalink
Merge pull request creusot-rs#801 from xldenis/tyinv-gen
Browse files Browse the repository at this point in the history 
Generate structural type invariants
  • Loading branch information
@voidc
voidc committed Jun 14, 2023
2 parents 88eff84 + f41ad35 commit ee50ea2
Show file tree
Hide file tree
Showing 72 changed files with 2,602 additions and 1,485 deletions.
23 changes: 23 additions & 0 deletions creusot-contracts/src/invariant.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,29 @@ pub trait Invariant {
}
}

#[predicate]
#[open(self)]
#[rustc_diagnostic_item = "creusot_invariant_internal"]
pub fn inv<T>(_x: T) -> bool {
true
}

pub trait UserInv {
#[predicate]
#[rustc_diagnostic_item = "creusot_invariant_user"]
fn user_inv(self) -> bool;
}

#[cfg(creusot)]
impl<T> UserInv for T {
#[predicate]
#[open]
#[rustc_diagnostic_item = "creusot_invariant_user_default"]
default fn user_inv(self) -> bool {
true
}
}

impl<'a, T: Invariant + ?Sized> Invariant for &'a T {
#[predicate]
#[open]
Expand Down
106 changes: 75 additions & 31 deletions creusot/src/backend.rs
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
use indexmap::{IndexMap, IndexSet};
use rustc_hir::{def::DefKind, def_id::DefId};
use rustc_span::DUMMY_SP;

use crate::{
ctx::{TranslatedItem, TranslationCtx},
Expand All @@ -9,6 +10,8 @@ use std::ops::{Deref, DerefMut};

pub(crate) use clone_map::*;

use self::{dependency::Dependency, ty_inv::TyInvKind};

pub(crate) mod clone_map;
pub(crate) mod constant;
pub(crate) mod dependency;
Expand All @@ -21,13 +24,26 @@ pub(crate) mod signature;
pub(crate) mod term;
pub(crate) mod traits;
pub(crate) mod ty;
pub(crate) mod ty_inv;

#[derive(Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord, Debug)]
pub(crate) enum TransId {
Item(DefId),
TyInv(TyInvKind),
}

impl From<DefId> for TransId {
fn from(def_id: DefId) -> Self {
TransId::Item(def_id)
}
}

pub struct Why3Generator<'tcx> {
ctx: TranslationCtx<'tcx>,
dependencies: IndexMap<DefId, CloneSummary<'tcx>>,
functions: IndexMap<DefId, TranslatedItem>,
translated_items: IndexSet<DefId>,
in_translation: Vec<IndexSet<DefId>>,
dependencies: IndexMap<TransId, CloneSummary<'tcx>>,
functions: IndexMap<TransId, TranslatedItem>,
translated_items: IndexSet<TransId>,
in_translation: Vec<IndexSet<TransId>>,
}

impl<'tcx> Deref for Why3Generator<'tcx> {
Expand Down Expand Up @@ -56,12 +72,13 @@ impl<'tcx> Why3Generator<'tcx> {
}

// Checks if we are allowed to recurse into
fn safe_cycle(&self, def_id: DefId) -> bool {
self.in_translation.last().map(|l| l.contains(&def_id)).unwrap_or_default()
fn safe_cycle(&self, trans_id: TransId) -> bool {
self.in_translation.last().map(|l| l.contains(&trans_id)).unwrap_or_default()
}

pub(crate) fn translate(&mut self, def_id: DefId) {
if self.translated_items.contains(&def_id) || self.safe_cycle(def_id) {
let tid = def_id.into();
if self.translated_items.contains(&tid) || self.safe_cycle(tid) {
return;
}
debug!("translating {:?}", def_id);
Expand All @@ -72,17 +89,17 @@ impl<'tcx> Why3Generator<'tcx> {
ItemType::Trait => {
self.start(def_id);
let tr = self.translate_trait(def_id);
self.dependencies.insert(def_id, CloneSummary::new());
self.functions.insert(def_id, tr);
self.dependencies.insert(tid, CloneSummary::new());
self.functions.insert(tid, tr);
self.finish(def_id);
}
ItemType::Impl => {
if self.tcx.impl_trait_ref(def_id).is_some() {
self.start(def_id);
let impl_ = traits::lower_impl(self, def_id);

self.dependencies.insert(def_id, CloneSummary::new());
self.functions.insert(def_id, TranslatedItem::Impl { modl: impl_ });
self.dependencies.insert(tid, CloneSummary::new());
self.functions.insert(tid, TranslatedItem::Impl { modl: impl_ });
self.finish(def_id);
}
}
Expand All @@ -95,15 +112,15 @@ impl<'tcx> Why3Generator<'tcx> {
self.start(def_id);
let (modl, dependencies) = self.translate_assoc_ty(def_id);
self.finish(def_id);
self.dependencies.insert(def_id, dependencies);
self.functions.insert(def_id, TranslatedItem::AssocTy { modl });
self.dependencies.insert(tid, dependencies);
self.functions.insert(tid, TranslatedItem::AssocTy { modl });
}
ItemType::Constant => {
self.start(def_id);
let (constant, dependencies) = self.translate_constant(def_id);
self.finish(def_id);
self.dependencies.insert(def_id, dependencies);
self.functions.insert(def_id, constant);
self.dependencies.insert(tid, dependencies);
self.functions.insert(tid, constant);
}
ItemType::Type => {
let bg = self.binding_group(def_id).clone();
Expand All @@ -116,7 +133,7 @@ impl<'tcx> Why3Generator<'tcx> {
self.finish(*d);
}

let repr = self.representative_type(def_id);
let repr = self.representative_type(def_id).into();
if let Some(modl) = modl {
self.functions
.insert(repr, TranslatedItem::Type { modl, accessors: Default::default() });
Expand Down Expand Up @@ -148,31 +165,31 @@ impl<'tcx> Why3Generator<'tcx> {
debug!("translating {:?} as logical", def_id);
let (stub, modl, proof_modl, has_axioms, deps) =
crate::backend::logic::translate_logic_or_predicate(self, def_id);
self.dependencies.insert(def_id, deps);
self.dependencies.insert(def_id.into(), deps);

TranslatedItem::Logic { stub, interface, modl, proof_modl, has_axioms }
}
ItemType::Closure => {
let (ty_modl, modl) = program::translate_closure(self, def_id);
self.dependencies.insert(def_id, deps);
self.dependencies.insert(def_id.into(), deps);

TranslatedItem::Closure { interface: vec![ty_modl, interface], modl }
}
ItemType::Program => {
debug!("translating {def_id:?} as program");

self.dependencies.insert(def_id, deps);
self.dependencies.insert(def_id.into(), deps);
let modl = program::translate_function(self, def_id);
TranslatedItem::Program { interface, modl }
}
_ => unreachable!(),
};

self.functions.insert(def_id, translated);
self.functions.insert(def_id.into(), translated);
}

pub(crate) fn translate_accessor(&mut self, field_id: DefId) {
if !self.translated_items.insert(field_id) {
if !self.translated_items.insert(field_id.into()) {
return;
}

Expand All @@ -187,30 +204,52 @@ impl<'tcx> Why3Generator<'tcx> {
self.translate(adt_did);

let accessor = ty::translate_accessor(self, adt_did, variant_did, field_id);
let repr_id = self.representative_type(adt_did);
let repr_id: TransId = self.representative_type(adt_did).into();
if let TranslatedItem::Type { ref mut accessors, .. } = &mut self.functions[&repr_id] {
accessors.entry(variant_did).or_default().insert(field_id, accessor);
};
// self.types[&repr_id].accessors;
}

pub(crate) fn translate_tyinv(&mut self, inv_kind: TyInvKind) {
let tid = TransId::TyInv(inv_kind);
if self.dependencies.contains_key(&tid) {
return;
}

if let TyInvKind::Adt(adt_did) = inv_kind {
self.translate(adt_did);
}

let (modl, deps) = ty_inv::build_inv_module(self, inv_kind);
self.dependencies.insert(tid, deps);
self.functions.insert(tid, TranslatedItem::TyInv { modl });
}

pub(crate) fn item(&self, def_id: DefId) -> Option<&TranslatedItem> {
let def_id = if matches!(util::item_type(***self, def_id), ItemType::Type) {
let tid: TransId = if matches!(util::item_type(***self, def_id), ItemType::Type) {
self.representative_type(def_id)
} else {
def_id
};
self.functions.get(&def_id)
}
.into();
self.functions.get(&tid)
}

pub(crate) fn modules(self) -> impl Iterator<Item = (DefId, TranslatedItem)> + 'tcx {
pub(crate) fn modules(self) -> impl Iterator<Item = (TransId, TranslatedItem)> + 'tcx {
self.functions.into_iter()
}

pub(crate) fn start_group(&mut self, ids: IndexSet<DefId>) {
assert!(!ids.is_empty());
let ids = ids.into_iter().map(Into::into).collect();
if self.in_translation.iter().rev().any(|s| !s.is_disjoint(&ids)) {
let span = self.def_span(ids.first().unwrap());
let span = if let TransId::Item(def_id) = ids.first().unwrap() {
self.def_span(def_id)
} else {
DUMMY_SP
};

self.in_translation.push(ids);

self.crash_and_error(
Expand All @@ -229,7 +268,8 @@ impl<'tcx> Why3Generator<'tcx> {

// Indicate we have finished translating a given id
pub(crate) fn finish(&mut self, def_id: DefId) {
if !self.in_translation.last_mut().unwrap().remove(&def_id) {
let tid = def_id.into();
if !self.in_translation.last_mut().unwrap().remove(&tid) {
self.crash_and_error(
self.def_span(def_id),
&format!("{:?} is not in translation", def_id),
Expand All @@ -240,10 +280,14 @@ impl<'tcx> Why3Generator<'tcx> {
self.in_translation.pop();
}

self.translated_items.insert(def_id);
self.translated_items.insert(tid);
}

pub(crate) fn dependencies(&self, def_id: DefId) -> Option<&CloneSummary<'tcx>> {
self.dependencies.get(&def_id)
pub(crate) fn dependencies(&self, key: Dependency<'tcx>) -> Option<&CloneSummary<'tcx>> {
let tid = match key {
Dependency::TyInv(ty) => TransId::TyInv(TyInvKind::from_ty(ty)),
_ => key.did().map(|(def_id, _)| TransId::Item(def_id))?,
};
self.dependencies.get(&tid)
}
}
Loading

0 comments on commit ee50ea2

Please sign in to comment.