Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Partial support for Generator type #486

Merged
merged 4 commits into from
Sep 17, 2021
Merged
Show file tree
Hide file tree
Changes from 2 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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