Skip to content

Commit

Permalink
Partial support for Generator type (model-checking#486)
Browse files Browse the repository at this point in the history
Partial support for Generator type
  • Loading branch information
avanhatt authored and tedinski committed Apr 25, 2022
1 parent 391392b commit 778382e
Show file tree
Hide file tree
Showing 12 changed files with 125 additions and 57 deletions.
19 changes: 12 additions & 7 deletions compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/expr.rs
Original file line number Diff line number Diff line change
Expand Up @@ -351,7 +351,7 @@ macro_rules! expr {
impl Expr {
/// `&self`
pub fn address_of(self) -> Self {
assert!(self.can_take_address_of());
assert!(self.can_take_address_of(), "Can't take address of {:?}", self);
expr!(AddressOf(self), self.typ.clone().to_pointer())
}

Expand Down Expand Up @@ -566,9 +566,11 @@ impl Expr {
self,
field,
);

let typ = symbol_table.lookup_field_type_in_type(self.typ(), field).unwrap().clone();
expr!(Member { lhs: self, field: field.to_string() }, typ)
if let Some(ty) = symbol_table.lookup_field_type_in_type(self.typ(), field) {
expr!(Member { lhs: self, field: field.to_string() }, ty.clone())
} else {
unreachable!("unable to find field {:?} for type {:?}", field, self.typ())
}
}

/// `__nondet_typ()`
Expand Down Expand Up @@ -603,8 +605,9 @@ impl Expr {
// Check that each formal field has an value
assert!(
fields.iter().zip(values.iter()).all(|(f, v)| f.typ() == *v.typ()),
"Error in struct_expr; value type does not match field type.\n\t{:?}\n\t{:?}",
"Error in struct_expr; value type does not match field type.\n\t{:?}\n\t{:?}\n\t{:?}",
typ,
fields,
values
);
expr!(Struct { values }, typ)
Expand Down Expand Up @@ -709,8 +712,9 @@ impl Expr {
.iter()
.zip(non_padding_values.iter())
.all(|(f, v)| f.field_typ().unwrap() == v.typ()),
"Error in struct_expr; value type does not match field type.\n\t{:?}\n\t{:?}",
"Error in struct_expr; value type does not match field type.\n\t{:?}\n\t{:?}\n\t{:?}",
typ,
non_padding_fields,
non_padding_values
);

Expand Down Expand Up @@ -748,8 +752,9 @@ impl Expr {
);
assert!(
fields.iter().zip(values.iter()).all(|(f, v)| &f.typ() == v.typ()),
"Error in struct_expr; value type does not match field type.\n\t{:?}\n\t{:?}",
"Error in struct_expr; value type does not match field type.\n\t{:?}\n\t{:?}\n\t{:?}",
typ,
fields,
values
);

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -209,7 +209,7 @@ impl Symbol {
/// Setters
impl Symbol {
pub fn update_fn_declaration_with_definition(&mut self, body: Stmt) {
assert!(self.is_function_declaration());
assert!(self.is_function_declaration(), "Expected function declaration, got {:?}", self);
self.value = SymbolValues::Stmt(body);
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,10 @@ impl<'tcx> GotocCtx<'tcx> {
name if name.starts_with("bridge::client") => true,
// https://github.com/model-checking/rmc/issues/282
"bridge::closure::Closure::<'a, A, R>::call" => true,
// Generators
name if name.starts_with("<std::future::from_generator::GenFuture<T>") => true,
name if name.contains("reusable_box::ReusableBoxFuture") => true,
"tokio::sync::Semaphore::acquire_owned::{closure#0}" => true,
_ => false,
}
}
Expand Down Expand Up @@ -64,7 +68,6 @@ impl<'tcx> GotocCtx<'tcx> {
self.set_current_fn(instance);
let name = self.current_fn().name();
let old_sym = self.symbol_table.lookup(&name).unwrap();
assert!(old_sym.is_function());
if old_sym.is_function_definition() {
warn!("Double codegen of {:?}", old_sym);
} else if self.should_skip_current_fn() {
Expand All @@ -79,6 +82,7 @@ impl<'tcx> GotocCtx<'tcx> {
);
self.symbol_table.update_fn_declaration_with_definition(&name, body);
} else {
assert!(old_sym.is_function());
let mir = self.current_fn().mir();
self.print_instance(instance, mir);
let labels = self
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,9 @@ impl<'tcx> GotocCtx<'tcx> {
let dst = fargs.remove(0).cast_to(Type::void_pointer());
let count = fargs.remove(0);
let sz = {
match self.fn_sig_of_instance(instance).skip_binder().inputs()[0].kind() {
match self.fn_sig_of_instance(instance).unwrap().skip_binder().inputs()[0]
.kind()
{
ty::RawPtr(t) => {
let layout = self.layout_of(t.ty);
Expr::int_constant(layout.size.bytes(), Type::size_t())
Expand Down Expand Up @@ -259,17 +261,9 @@ impl<'tcx> GotocCtx<'tcx> {
"atomic_and_acqrel" => codegen_atomic_binop!(bitand),
"atomic_and_rel" => codegen_atomic_binop!(bitand),
"atomic_and_relaxed" => codegen_atomic_binop!(bitand),
"atomic_cxchg" => self.codegen_atomic_cxchg(intrinsic, fargs, p, loc),
"atomic_cxchg_acq" => self.codegen_atomic_cxchg(intrinsic, fargs, p, loc),
"atomic_cxchg_acq_failrelaxed" => self.codegen_atomic_cxchg(intrinsic, fargs, p, loc),
"atomic_cxchg_acqrel" => self.codegen_atomic_cxchg(intrinsic, fargs, p, loc),
"atomic_cxchg_acqrel_failrelaxed" => {
name if name.starts_with("atomic_cxchg") => {
self.codegen_atomic_cxchg(intrinsic, fargs, p, loc)
}
"atomic_cxchg_failacq" => self.codegen_atomic_cxchg(intrinsic, fargs, p, loc),
"atomic_cxchg_failrelaxed" => self.codegen_atomic_cxchg(intrinsic, fargs, p, loc),
"atomic_cxchg_rel" => self.codegen_atomic_cxchg(intrinsic, fargs, p, loc),
"atomic_cxchg_relaxed" => self.codegen_atomic_cxchg(intrinsic, fargs, p, loc),
"atomic_fence" => self.codegen_atomic_noop(intrinsic, loc),
"atomic_fence_acq" => self.codegen_atomic_noop(intrinsic, loc),
"atomic_fence_acqrel" => self.codegen_atomic_noop(intrinsic, loc),
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -573,7 +573,7 @@ impl<'tcx> GotocCtx<'tcx> {

pub fn codegen_func_expr(&mut self, instance: Instance<'tcx>, span: Option<&Span>) -> Expr {
let func = self.symbol_name(instance);
let funct = self.codegen_function_sig(self.fn_sig_of_instance(instance));
let funct = self.codegen_function_sig(self.fn_sig_of_instance(instance).unwrap());
// make sure the functions imported from other modules are in the symbol table
self.ensure(&func, |ctx, _| {
Symbol::function(
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -207,6 +207,12 @@ impl<'tcx> GotocCtx<'tcx> {
res.member(&field.ident.name.to_string(), &self.symbol_table)
}
ty::Closure(..) => res.member(&f.index().to_string(), &self.symbol_table),
ty::Generator(..) => self.codegen_unimplemented(
"ty::Generator",
Type::code(vec![], Type::empty()),
res.location().clone(),
"https://github.com/model-checking/rmc/issues/416",
),
_ => unimplemented!(),
}
}
Expand Down Expand Up @@ -235,7 +241,9 @@ impl<'tcx> GotocCtx<'tcx> {
// A local that is itself a FnDef, like Fn::call_once
ty::FnDef(defid, substs) => Some(self.codegen_fndef(*defid, substs, None)),
// A local can be pointer to a FnDef, like Fn::call and Fn::call_mut
ty::RawPtr(inner) => self.codegen_local_fndef(inner.ty).map(|f| f.address_of()),
ty::RawPtr(inner) => self
.codegen_local_fndef(inner.ty)
.map(|f| if f.can_take_address_of() { f.address_of() } else { f }),
// A local can be a boxed function pointer
ty::Adt(def, _) if def.is_box() => {
let boxed_ty = self.codegen_ty(ty);
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@ impl<'tcx> GotocCtx<'tcx> {
TerminatorKind::Resume => Stmt::assert_false("resume instruction", loc),
TerminatorKind::Abort => Stmt::assert_false("abort instruction", loc),
TerminatorKind::Return => {
let rty = self.current_fn().sig().skip_binder().output();
let rty = self.current_fn().sig().unwrap().skip_binder().output();
if rty.is_unit() {
self.codegen_ret_unit()
} else {
Expand Down Expand Up @@ -358,8 +358,12 @@ impl<'tcx> GotocCtx<'tcx> {
// should be a fat pointer for the trait
let trait_fat_ptr = fargs[0].to_owned();

// Check the Gotoc-level fat pointer type
assert!(trait_fat_ptr.typ().is_rust_trait_fat_ptr(&self.symbol_table));
//Check the Gotoc-level fat pointer type
assert!(
trait_fat_ptr.typ().is_rust_trait_fat_ptr(&self.symbol_table),
"Expected fat pointer, got:\n{:?}",
trait_fat_ptr,
);

self.codegen_virtual_funcall(
trait_fat_ptr,
Expand Down Expand Up @@ -537,6 +541,16 @@ impl<'tcx> GotocCtx<'tcx> {
let pt = self.place_ty(place);
let (def, _) = match pt.kind() {
ty::Adt(def, substs) => (def, substs),
ty::Generator(..) => {
return self
.codegen_unimplemented(
"ty::Generator",
Type::code(vec![], Type::empty()),
Location::none(),
"https://github.com/model-checking/rmc/issues/416",
)
.as_stmt(Location::none());
}
_ => unreachable!(),
};
let layout = self.layout_of(pt);
Expand Down
33 changes: 18 additions & 15 deletions compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/typ.rs
Original file line number Diff line number Diff line change
Expand Up @@ -148,20 +148,21 @@ impl<'tcx> GotocCtx<'tcx> {
self.sig_with_closure_untupled(sig)
}

pub fn fn_sig_of_instance(&self, instance: Instance<'tcx>) -> ty::PolyFnSig<'tcx> {
pub fn fn_sig_of_instance(&self, instance: Instance<'tcx>) -> Option<ty::PolyFnSig<'tcx>> {
let fntyp = instance.ty(self.tcx, ty::ParamEnv::reveal_all());
self.monomorphize(match fntyp.kind() {
ty::Closure(def_id, subst) => self.closure_sig(*def_id, subst),
ty::Closure(def_id, subst) => Some(self.closure_sig(*def_id, subst)),
ty::FnPtr(..) | ty::FnDef(..) => {
let sig = fntyp.fn_sig(self.tcx);
// Some virtual calls through a vtable may actually be closures
// or shims that also need the arguments untupled, even though
// the kind of the trait type is not a ty::Closure.
if self.ty_needs_closure_untupled(fntyp) {
return self.sig_with_closure_untupled(sig);
return Some(self.sig_with_closure_untupled(sig));
}
sig
Some(sig)
}
ty::Generator(_def_id, _substs, _movability) => None,
_ => unreachable!("Can't get function signature of type: {:?}", fntyp),
})
}
Expand Down Expand Up @@ -243,7 +244,7 @@ impl<'tcx> GotocCtx<'tcx> {
idx: usize,
) -> DatatypeComponent {
// Gives a binder with function signature
let sig = self.fn_sig_of_instance(instance);
let sig = self.fn_sig_of_instance(instance).unwrap();

// Gives an Irep Pointer object for the signature
let fn_ty = self.codegen_dynamic_function_sig(sig);
Expand Down Expand Up @@ -367,14 +368,6 @@ impl<'tcx> GotocCtx<'tcx> {
// StructTag("tag-std::boxed::Box<dyn std::error::Error + std::marker::Send + std::marker::Sync>") }
let t = self.monomorphize(t);
with_no_trimmed_paths(|| printer.print_type(t).unwrap());
// TODO: The following line is a temporary measure to remove the static lifetime
// appearing as \'static in mangled type names. This should be done using regular
// expressions to handle more or less whitespace around the lifetime, but this
// requires adding the regex module to the dependencies in Cargo.toml. This should
// probably be done modifying the rustc pretty printer, but that is deep in the rustc
// code. See the implementation of pretty_print_region on line 1720 in
// compiler/rustc_middle/src/ty/print/pretty.rs.
let name = name.replace(" + \'static", "").replace("\'static ", "");

// Crate resolution: mangled names need to be distinct across different versions
// of the same crate that could be pulled in by dependencies. However, RMC's
Expand Down Expand Up @@ -493,7 +486,7 @@ impl<'tcx> GotocCtx<'tcx> {
}
ty::FnPtr(sig) => self.codegen_function_sig(*sig).to_pointer(),
ty::Closure(_, subst) => self.codegen_ty_closure(ty, subst),
ty::Generator(_, _, _) => unimplemented!(),
ty::Generator(_, subst, _) => self.codegen_ty_generator(subst),
ty::Never =>
// unfortunately, there is no bottom in C. We must pick a type
{
Expand Down Expand Up @@ -681,6 +674,15 @@ impl<'tcx> GotocCtx<'tcx> {
})
}

/// Preliminary support for the Generator type kind. The core functionality remains
/// unimplemented, but this way we fail at verification time only if paths that
/// rely on Generator types are used.
fn codegen_ty_generator(&mut self, substs: ty::subst::SubstsRef<'tcx>) -> Type {
let tys = substs.as_generator().upvar_tys().map(|t| self.codegen_ty(t)).collect();
let output = self.codegen_ty(substs.as_generator().return_ty());
Type::code_with_unnamed_parameters(tys, output)
}

pub fn codegen_fat_ptr(&mut self, mir_type: Ty<'tcx>) -> Type {
assert!(
!self.use_thin_pointer(mir_type),
Expand Down Expand Up @@ -1125,7 +1127,8 @@ impl<'tcx> GotocCtx<'tcx> {
/// the function type of the current instance
pub fn fn_typ(&mut self) -> Type {
let sig = self.current_fn().sig();
let sig = self.tcx.normalize_erasing_late_bound_regions(ty::ParamEnv::reveal_all(), sig);
let sig =
self.tcx.normalize_erasing_late_bound_regions(ty::ParamEnv::reveal_all(), sig.unwrap());
// we don't call [codegen_function_sig] because we want to get a bit more metainformation.
let mut params: Vec<Parameter> = sig
.inputs()
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ pub struct CurrentFnCtx<'tcx> {
/// A human readable pretty name for the current function
readable_name: String,
/// The signature of the current function
sig: PolyFnSig<'tcx>,
sig: Option<PolyFnSig<'tcx>>,
/// A counter to enable creating temporary variables
temp_var_counter: u64,
}
Expand Down Expand Up @@ -111,7 +111,7 @@ impl CurrentFnCtx<'tcx> {
}

/// The signature of the function we are currently compiling
pub fn sig(&self) -> PolyFnSig<'tcx> {
pub fn sig(&self) -> Option<PolyFnSig<'tcx>> {
self.sig
}
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -10,15 +10,13 @@
use super::stubs::{HashMapStub, VecStub};
use crate::gotoc::cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Symbol, Type};
use crate::gotoc::mir_to_goto::utils::{
instance_name_is, instance_name_starts_with, sig_of_instance,
};
use crate::gotoc::mir_to_goto::utils::{instance_name_is, instance_name_starts_with};
use crate::gotoc::mir_to_goto::GotocCtx;
use rustc_hir::definitions::DefPathDataName;
use rustc_middle::mir::{BasicBlock, Place};
use rustc_middle::ty::layout::LayoutOf;
use rustc_middle::ty::print::with_no_trimmed_paths;
use rustc_middle::ty::{Instance, InstanceDef, Ty, TyCtxt};
use rustc_middle::ty::{self, Instance, InstanceDef, Ty, TyCtxt};
use rustc_span::Span;
use std::rc::Rc;

Expand All @@ -42,6 +40,31 @@ pub trait GotocHook<'tcx> {
) -> Stmt;
}

fn output_of_instance_is_never<'tcx>(tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool {
let ty = instance.ty(tcx, ty::ParamEnv::reveal_all());
match ty.kind() {
ty::Closure(_, substs) => tcx
.normalize_erasing_late_bound_regions(
ty::ParamEnv::reveal_all(),
substs.as_closure().sig(),
)
.output()
.is_never(),
ty::FnDef(..) | ty::FnPtr(..) => tcx
.normalize_erasing_late_bound_regions(ty::ParamEnv::reveal_all(), ty.fn_sig(tcx))
.output()
.is_never(),
ty::Generator(_, substs, _) => substs.as_generator().return_ty().is_never(),
_ => {
unreachable!(
"Can't take get ouput type of instance:\n{:?}\nType kind:\n{:?}",
ty,
ty.kind()
)
}
}
}

struct ExpectFail;
impl<'tcx> GotocHook<'tcx> for ExpectFail {
fn hook_applies(&self, tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool {
Expand Down Expand Up @@ -166,7 +189,7 @@ struct Panic;

impl<'tcx> GotocHook<'tcx> for Panic {
fn hook_applies(&self, tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool {
sig_of_instance(tcx, instance).output().is_never()
output_of_instance_is_never(tcx, instance)
&& (instance_name_is(tcx, instance, "begin_panic")
|| instance_name_is(tcx, instance, "panic"))
}
Expand All @@ -188,8 +211,7 @@ struct Nevers;

impl<'tcx> GotocHook<'tcx> for Nevers {
fn hook_applies(&self, tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool {
let sig = sig_of_instance(tcx, instance);
sig.output().is_never()
output_of_instance_is_never(tcx, instance)
}

fn handle(
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ use rustc_hir::definitions::DefPathDataName;
use rustc_middle::mir::mono::CodegenUnitNameBuilder;
use rustc_middle::mir::Local;
use rustc_middle::ty::print::with_no_trimmed_paths;
use rustc_middle::ty::{self, Instance, TyCtxt};
use rustc_middle::ty::{Instance, TyCtxt};
use tracing::debug;

impl<'tcx> GotocCtx<'tcx> {
Expand Down Expand Up @@ -126,14 +126,6 @@ pub fn full_crate_name(tcx: TyCtxt<'tcx>) -> String {
}

//TODO: These were moved from hooks.rs, where they didn't have a goto context. Normalize them.
pub fn sig_of_instance<'tcx>(tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> ty::FnSig<'tcx> {
let ty = instance.ty(tcx, ty::ParamEnv::reveal_all());
let sig = match ty.kind() {
ty::Closure(_, substs) => substs.as_closure().sig(),
_ => ty.fn_sig(tcx),
};
tcx.normalize_erasing_late_bound_regions(ty::ParamEnv::reveal_all(), sig)
}

/// Helper function to determine if the function name starts with `expected`
// TODO: rationalize how we match the hooks https://github.com/model-checking/rmc/issues/130
Expand Down
Loading

0 comments on commit 778382e

Please sign in to comment.