Skip to content

Commit

Permalink
Merge pull request #465 from Nadrieril/ctor-as-fn
Browse files Browse the repository at this point in the history
  • Loading branch information
Nadrieril authored Nov 26, 2024
2 parents 3a58b40 + bbcec05 commit e8427b8
Show file tree
Hide file tree
Showing 5 changed files with 247 additions and 50 deletions.
6 changes: 3 additions & 3 deletions charon/Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

102 changes: 84 additions & 18 deletions charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs
Original file line number Diff line number Diff line change
Expand Up @@ -121,11 +121,11 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
// ```
hax::AssocItemContainer::TraitImplContainer {
impl_id,
implemented_trait,
implemented_trait_ref,
overrides_default,
..
} => {
let trait_id = self.register_trait_decl_id(span, implemented_trait);
let trait_id = self.register_trait_decl_id(span, &implemented_trait_ref.def_id);
let impl_id = self.register_trait_impl_id(span, impl_id);
ItemKind::TraitImpl {
impl_id,
Expand All @@ -141,10 +141,10 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
// fn baz(...); // <- declaration of a trait method
// }
// ```
hax::AssocItemContainer::TraitContainer { trait_id } => {
hax::AssocItemContainer::TraitContainer { trait_ref, .. } => {
// The trait id should be Some(...): trait markers (that we may eliminate)
// don't have associated items.
let trait_id = self.register_trait_decl_id(span, trait_id);
let trait_id = self.register_trait_decl_id(span, &trait_ref.def_id);
let item_name = TraitItemName(assoc.name.clone());

ItemKind::TraitDecl {
Expand Down Expand Up @@ -1236,12 +1236,12 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
fn translate_body(
&mut self,
def: &hax::FullDef,
arg_count: usize,
sig: &FunSig,
item_meta: &ItemMeta,
) -> Result<Result<Body, Opaque>, Error> {
// Stopgap measure because there are still many panics in charon and hax.
let mut this = panic::AssertUnwindSafe(&mut *self);
let res = panic::catch_unwind(move || this.translate_body_aux(def, arg_count, item_meta));
let res = panic::catch_unwind(move || this.translate_body_aux(def, sig, item_meta));
match res {
Ok(Ok(body)) => Ok(body),
// Translation error
Expand All @@ -1259,14 +1259,74 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
fn translate_body_aux(
&mut self,
def: &hax::FullDef,
arg_count: usize,
sig: &FunSig,
item_meta: &ItemMeta,
) -> Result<Result<Body, Opaque>, Error> {
if item_meta.opacity.with_private_contents().is_opaque() {
// The bodies of foreign functions are opaque by default.
return Ok(Err(Opaque));
}

if let hax::FullDefKind::Ctor {
adt_def_id,
ctor_of,
variant_id,
fields,
output_ty,
..
} = def.kind()
{
let span = item_meta.span;
let adt_decl_id = self.register_type_decl_id(span, adt_def_id);
let output_ty = self.translate_ty(span, output_ty)?;
let mut locals = Locals {
arg_count: fields.len(),
vars: Vector::new(),
};
locals.new_var(None, output_ty); // return place
let args: Vec<_> = fields
.iter()
.map(|field| {
let ty = self.translate_ty(span, &field.ty)?;
let place = locals.new_var(None, ty);
Ok(Operand::Move(place))
})
.try_collect()?;
let variant = match ctor_of {
hax::CtorOf::Struct => None,
hax::CtorOf::Variant => Some(VariantId::from(*variant_id)),
};
let statement = Statement {
span,
content: RawStatement::Assign(
locals.return_place(),
Rvalue::Aggregate(
AggregateKind::Adt(
TypeId::Adt(adt_decl_id),
variant,
None,
sig.generics.identity_args(),
),
args,
),
),
};
let block = BlockData {
statements: vec![statement],
terminator: Terminator {
span,
content: RawTerminator::Return,
},
};
let body = Body::Unstructured(GExprBody {
span,
locals,
comments: Default::default(),
body: [block].into_iter().collect(),
});
return Ok(Ok(body));
}

// Retrieve the body
let rust_id = def.rust_def_id();
let Some(body) =
Expand All @@ -1275,7 +1335,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
return Ok(Err(Opaque));
};

self.locals.arg_count = arg_count;
self.locals.arg_count = sig.inputs.len();
// Here, we have to create a MIR state, which contains the body
// Yes, we have to clone, this is annoying: we end up cloning the body twice
let state = self
Expand Down Expand Up @@ -1332,12 +1392,20 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
hax::FullDefKind::Closure { args, .. } => &args.sig,
hax::FullDefKind::Fn { sig, .. } => sig,
hax::FullDefKind::AssocFn { sig, .. } => sig,
hax::FullDefKind::Ctor { .. } => {
error_or_panic!(
self,
span,
"Casting constructors to function pointers is not supported"
)
hax::FullDefKind::Ctor {
fields, output_ty, ..
} => {
let sig = hax::TyFnSig {
inputs: fields.iter().map(|field| field.ty.clone()).collect(),
output: output_ty.clone(),
c_variadic: false,
safety: hax::Safety::Safe,
abi: hax::Abi::Rust,
};
&hax::Binder {
value: sig,
bound_vars: Default::default(),
}
}
hax::FullDefKind::Const { ty, .. }
| hax::FullDefKind::AssocConst { ty, .. }
Expand All @@ -1347,9 +1415,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
output: ty.clone(),
c_variadic: false,
safety: hax::Safety::Safe,
abi: hax::Abi::Abi {
todo: String::new(),
},
abi: hax::Abi::Rust,
};
&hax::Binder {
value: sig,
Expand Down Expand Up @@ -1473,7 +1539,7 @@ impl BodyTransCtx<'_, '_> {
let body_id = if !is_trait_method_decl_without_default {
// Translate the body. This doesn't store anything if we can't/decide not to translate
// this body.
match self.translate_body(def, signature.inputs.len(), &item_meta) {
match self.translate_body(def, &signature, &item_meta) {
Ok(Ok(body)) => Ok(self.t_ctx.translated.bodies.push(body)),
// Opaque declaration
Ok(Err(Opaque)) => Err(Opaque),
Expand Down
13 changes: 8 additions & 5 deletions charon/src/bin/charon-driver/translate/translate_types.rs
Original file line number Diff line number Diff line change
Expand Up @@ -617,11 +617,14 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
// Add generics from the parent item, recursively (recursivity is useful for closures, as
// they could be nested).
match &def.kind {
FullDefKind::AssocTy { parent, .. }
| FullDefKind::AssocFn { parent, .. }
| FullDefKind::AssocConst { parent, .. }
| FullDefKind::Closure { parent, .. } => {
let parent_def = self.t_ctx.hax_def(parent)?;
FullDefKind::AssocTy { .. }
| FullDefKind::AssocFn { .. }
| FullDefKind::AssocConst { .. }
| FullDefKind::Closure { .. }
| FullDefKind::Ctor { .. }
| FullDefKind::Variant { .. } => {
let parent_def_id = def.parent.as_ref().unwrap();
let parent_def = self.t_ctx.hax_def(parent_def_id)?;
self.push_generics_for_def(span, &parent_def, true)?;
}
_ => {}
Expand Down
156 changes: 139 additions & 17 deletions charon/tests/ui/issue-378-ctor-as-fn.out
Original file line number Diff line number Diff line change
@@ -1,17 +1,139 @@
error: Casting constructors to function pointers is not supported
--> /rustc/library/core/src/option.rs:579:5

note: the error occurred when translating `core::option::Option::Some`, which is (transitively) used at the following location(s):
--> tests/ui/issue-378-ctor-as-fn.rs:3:34
|
3 | static F: fn(u8) -> Option<u8> = Some;
| ----
4 |
5 | fn main() {
6 | let f: fn(u8) -> _ = Some;
| ----
|
error: Item `core::option::Option::Some::{constructor#0}` caused errors; ignoring.
--> /rustc/library/core/src/option.rs:579:5

ERROR The extraction generated 2 errors
# Final LLBC before serialization:

trait core::marker::Sized<Self>

enum core::option::Option<T>
where
[@TraitClause0]: core::marker::Sized<T>,
=
| None()
| Some(T)


fn core::option::Option::Some<T>(@1: T) -> core::option::Option<T>[@TraitClause0]
where
[@TraitClause0]: core::marker::Sized<T>,

fn test_crate::F() -> fn(u8) -> core::option::Option<u8>[core::marker::Sized<u8>]
{
let @0: fn(u8) -> core::option::Option<u8>[core::marker::Sized<u8>]; // return

@0 := cast<fn(u8) -> core::option::Option<u8>[core::marker::Sized<u8>], fn(u8) -> core::option::Option<u8>[core::marker::Sized<u8>]>(const (core::option::Option::Some<u8>))
return
}

global test_crate::F: fn(u8) -> core::option::Option<u8>[core::marker::Sized<u8>] = test_crate::F()

opaque type alloc::string::String

struct test_crate::Foo =
{
u32,
alloc::string::String,
}

enum test_crate::Bar<'a, T>
where
[@TraitClause0]: core::marker::Sized<T>,
T : 'a,
=
| Variant(&'a (T))


fn test_crate::Foo(@1: u32, @2: alloc::string::String) -> test_crate::Foo
{
let @0: test_crate::Foo; // return
let @1: u32; // arg #1
let @2: alloc::string::String; // arg #2

@0 := test_crate::Foo { 0: move (@1), 1: move (@2) }
return
}

fn alloc::string::{alloc::string::String}::new() -> alloc::string::String

fn test_crate::Bar::Variant<'a, T>(@1: &'a (T)) -> test_crate::Bar<'a, T>[@TraitClause0]
where
[@TraitClause0]: core::marker::Sized<T>,
T : 'a,
{
let @0: test_crate::Bar<'a, T>[@TraitClause0]; // return
let @1: &'a (T); // arg #1

@0 := test_crate::Bar::Variant { 0: move (@1) }
return
}

fn test_crate::main()
{
let @0: (); // return
let f@1: fn(u8) -> core::option::Option<u8>[core::marker::Sized<u8>]; // local
let @2: core::option::Option<u8>[core::marker::Sized<u8>]; // anonymous local
let @3: fn(u8) -> core::option::Option<u8>[core::marker::Sized<u8>]; // anonymous local
let f@4: fn(u8) -> core::option::Option<u8>[core::marker::Sized<u8>]; // local
let @5: fn(u8) -> core::option::Option<u8>[core::marker::Sized<u8>]; // anonymous local
let @6: core::option::Option<u8>[core::marker::Sized<u8>]; // anonymous local
let @7: fn(u8) -> core::option::Option<u8>[core::marker::Sized<u8>]; // anonymous local
let f@8: fn(u32, alloc::string::String) -> test_crate::Foo; // local
let @9: test_crate::Foo; // anonymous local
let @10: fn(u32, alloc::string::String) -> test_crate::Foo; // anonymous local
let @11: alloc::string::String; // anonymous local
let f@12: fn(&'_ (i32)) -> test_crate::Bar<'_, i32>[core::marker::Sized<i32>]; // local
let @13: test_crate::Bar<'_, i32>[core::marker::Sized<i32>]; // anonymous local
let @14: fn(&'_ (i32)) -> test_crate::Bar<'_, i32>[core::marker::Sized<i32>]; // anonymous local
let @15: &'_ (i32); // anonymous local
let @16: &'_ (i32); // anonymous local
let @17: i32; // anonymous local
let @18: (); // anonymous local

f@1 := const (core::option::Option::Some<u8>)
@fake_read(f@1)
@3 := copy (f@1)
@2 := core::option::Option::Some<u8>(const (42 : u8))
drop @3
@fake_read(@2)
drop @2
@5 := copy (f@1)
f@4 := cast<fn(u8) -> core::option::Option<u8>[core::marker::Sized<u8>], fn(u8) -> core::option::Option<u8>[core::marker::Sized<u8>]>(move (@5))
drop @5
@fake_read(f@4)
@7 := copy (f@4)
@6 := (move @7)(const (42 : u8))
drop @7
@fake_read(@6)
drop @6
f@8 := const (test_crate::Foo)
@fake_read(f@8)
@10 := copy (f@8)
@11 := alloc::string::{alloc::string::String}::new()
@9 := test_crate::Foo(const (42 : u32), move (@11))
drop @11
drop @10
@fake_read(@9)
drop @9
drop @9
f@12 := const (test_crate::Bar::Variant<'_, i32>)
@fake_read(f@12)
@14 := copy (f@12)
@17 := const (42 : i32)
@16 := &@17
@15 := &*(@16)
@13 := test_crate::Bar::Variant<'_, i32>(move (@15))
drop @15
drop @14
@fake_read(@13)
drop @17
drop @16
drop @13
@18 := ()
@0 := move (@18)
drop f@12
drop f@8
drop f@4
drop f@1
@0 := ()
return
}



Loading

0 comments on commit e8427b8

Please sign in to comment.