From af9bb78e4c5df8d5fb5b34b42959a60ebd73c6e6 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Wed, 10 Jul 2024 05:39:51 +0200 Subject: [PATCH] fix(frontend): crashes on fn ptr This commit fixes the issue #757: the frontend was assuming functions expressions to be of a very specific shape. This commit fixes that. --- frontend/exporter/src/types/copied.rs | 100 ++++++++---------- .../toolchain__functions into-coq.snap | 46 ++++++++ .../toolchain__functions into-fstar.snap | 42 ++++++++ tests/Cargo.lock | 7 ++ tests/Cargo.toml | 1 + tests/functions/Cargo.toml | 10 ++ tests/functions/src/lib.rs | 6 ++ 7 files changed, 154 insertions(+), 58 deletions(-) create mode 100644 test-harness/src/snapshots/toolchain__functions into-coq.snap create mode 100644 test-harness/src/snapshots/toolchain__functions into-fstar.snap create mode 100644 tests/functions/Cargo.toml create mode 100644 tests/functions/src/lib.rs diff --git a/frontend/exporter/src/types/copied.rs b/frontend/exporter/src/types/copied.rs index 527507362..8fd350c83 100644 --- a/frontend/exporter/src/types/copied.rs +++ b/frontend/exporter/src/types/copied.rs @@ -2412,66 +2412,50 @@ pub enum ExprKind { #[map({ let e = gstate.thir().exprs[*fun].unroll_scope(gstate); let (generic_args, r#trait, bounds_impls); - let fun = match &e.kind { - /* TODO: see whether [user_ty] below is relevant or not */ - rustc_middle::thir::ExprKind::ZstLiteral {user_ty: _ } => { - match ty.kind() { - rustc_middle::ty::TyKind::FnDef(def_id, generics) => { - let (hir_id, attributes) = e.hir_id_and_attributes(gstate); - let hir_id = hir_id.map(|hir_id| hir_id.index()); - let contents = Box::new(ExprKind::GlobalName { - id: def_id.sinto(gstate) - }); - let mut translated_generics = generics.sinto(gstate); - let tcx = gstate.base().tcx; - r#trait = (|| { - let assoc_item = tcx.opt_associated_item(*def_id)?; - let assoc_trait = tcx.trait_of_item(assoc_item.def_id)?; - let trait_ref = ty::TraitRef::new(tcx, assoc_trait, generics.iter()); - let impl_expr = { - // TODO: we should not wrap into a dummy binder - let poly_trait_ref = ty::Binder::dummy(trait_ref); - poly_trait_ref.impl_expr(gstate, gstate.param_env()) - }; - let assoc_generics = tcx.generics_of(assoc_item.def_id); - let assoc_generics = translated_generics.drain(0..assoc_generics.parent_count); - Some((impl_expr, assoc_generics.collect())) - })(); - generic_args = translated_generics; - bounds_impls = solve_item_traits(gstate, gstate.param_env(), *def_id, generics, None); - Expr { - contents, - span: e.span.sinto(gstate), - ty: e.ty.sinto(gstate), - hir_id, - attributes, - } - }, - ty_kind => supposely_unreachable_fatal!( - gstate[e.span], - "CallNotTyFnDef"; - {e, ty_kind} - ) + // A function is any expression whose type is something callable + let fun = match ty.kind() { + rustc_middle::ty::TyKind::FnDef(def_id, generics) => { + let (hir_id, attributes) = e.hir_id_and_attributes(gstate); + let hir_id = hir_id.map(|hir_id| hir_id.index()); + let contents = Box::new(ExprKind::GlobalName { + id: def_id.sinto(gstate) + }); + let mut translated_generics = generics.sinto(gstate); + let tcx = gstate.base().tcx; + r#trait = (|| { + let assoc_item = tcx.opt_associated_item(*def_id)?; + let assoc_trait = tcx.trait_of_item(assoc_item.def_id)?; + let trait_ref = ty::TraitRef::new(tcx, assoc_trait, generics.iter()); + let impl_expr = { + // TODO: we should not wrap into a dummy binder + let poly_trait_ref = ty::Binder::dummy(trait_ref); + poly_trait_ref.impl_expr(gstate, gstate.param_env()) + }; + let assoc_generics = tcx.generics_of(assoc_item.def_id); + let assoc_generics = translated_generics.drain(0..assoc_generics.parent_count); + Some((impl_expr, assoc_generics.collect())) + })(); + generic_args = translated_generics; + bounds_impls = solve_item_traits(gstate, gstate.param_env(), *def_id, generics, None); + Expr { + contents, + span: e.span.sinto(gstate), + ty: e.ty.sinto(gstate), + hir_id, + attributes, } }, - kind => { - match ty.kind() { - rustc_middle::ty::TyKind::FnPtr(..) => { - generic_args = vec![]; // A function pointer has no generics - bounds_impls = vec![]; // A function pointer has no bounds - r#trait = None; // A function pointer is not a method - e.sinto(gstate) - }, - ty_kind => { - supposely_unreachable!( - gstate[e.span], - "CallNotTyFnDef"; - {e, kind, ty_kind} - ); - fatal!(gstate, "RefCallNotTyFnPtr") - } - } - } + rustc_middle::ty::TyKind::FnPtr(..) => { + generic_args = vec![]; // A function pointer has no generics + bounds_impls = vec![]; // A function pointer has no bounds + r#trait = None; // A function pointer is not a method + e.sinto(gstate) + }, + ty_kind => supposely_unreachable_fatal!( + gstate[e.span], + "CallNotTyFnDef"; + {e, ty_kind} + ) }; TO_TYPE::Call { ty: ty.sinto(gstate), diff --git a/test-harness/src/snapshots/toolchain__functions into-coq.snap b/test-harness/src/snapshots/toolchain__functions into-coq.snap new file mode 100644 index 000000000..56ca87c28 --- /dev/null +++ b/test-harness/src/snapshots/toolchain__functions into-coq.snap @@ -0,0 +1,46 @@ +--- +source: test-harness/src/harness.rs +expression: snapshot +info: + kind: + Translate: + backend: coq + info: + name: functions + manifest: functions/Cargo.toml + description: ~ + spec: + optional: false + broken: false + issue_id: ~ + positive: true + snapshot: + stderr: false + stdout: true + include_flag: ~ + backend_options: ~ +--- +exit = 0 + +[stdout] +diagnostics = [] + +[stdout.files] +"Functions.v" = ''' +(* File automatically generated by Hacspec *) +From Hacspec Require Import Hacspec_Lib MachineIntegers. +From Coq Require Import ZArith. +Import List.ListNotations. +Open Scope Z_scope. +Open Scope bool_scope. + +(*Not implemented yet? todo(item)*) + +Definition calling_function_pointer__f (_ : unit) : unit := + tt. + +Definition calling_function_pointer (_ : unit) : unit := + let f_ptr := calling_function_pointer__f : unit -> unit in + let _ := calling_function_pointer__f tt : unit in + tt. +''' diff --git a/test-harness/src/snapshots/toolchain__functions into-fstar.snap b/test-harness/src/snapshots/toolchain__functions into-fstar.snap new file mode 100644 index 000000000..21a6f688a --- /dev/null +++ b/test-harness/src/snapshots/toolchain__functions into-fstar.snap @@ -0,0 +1,42 @@ +--- +source: test-harness/src/harness.rs +expression: snapshot +info: + kind: + Translate: + backend: fstar + info: + name: functions + manifest: functions/Cargo.toml + description: ~ + spec: + optional: false + broken: false + issue_id: ~ + positive: true + snapshot: + stderr: false + stdout: true + include_flag: ~ + backend_options: ~ +--- +exit = 0 + +[stdout] +diagnostics = [] + +[stdout.files] +"Functions.fst" = ''' +module Functions +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +let calling_function_pointer__f (#v_T: Type0) (_: Prims.unit) : Prims.unit = () + +/// Issue #757 +let calling_function_pointer (_: Prims.unit) : Prims.unit = + let ff_ptr: Prims.unit -> Prims.unit = calling_function_pointer__f in + let _:Prims.unit = calling_function_pointer__f #i32 () in + () +''' diff --git a/tests/Cargo.lock b/tests/Cargo.lock index 9d18936a6..fe5e3ca74 100644 --- a/tests/Cargo.lock +++ b/tests/Cargo.lock @@ -235,6 +235,13 @@ version = "0.0.1" name = "fn-to-letfun" version = "0.1.0" +[[package]] +name = "functions" +version = "0.1.0" +dependencies = [ + "hax-lib", +] + [[package]] name = "generics" version = "0.1.0" diff --git a/tests/Cargo.toml b/tests/Cargo.toml index 68ec5ef04..8142bf4a4 100644 --- a/tests/Cargo.toml +++ b/tests/Cargo.toml @@ -28,5 +28,6 @@ members = [ "cli/include-flag", "cli/interface-only", "recursion", + "functions", ] resolver = "2" diff --git a/tests/functions/Cargo.toml b/tests/functions/Cargo.toml new file mode 100644 index 000000000..215bd726c --- /dev/null +++ b/tests/functions/Cargo.toml @@ -0,0 +1,10 @@ +[package] +name = "functions" +version = "0.1.0" +edition = "2021" + +[dependencies] +hax-lib = { path = "../../hax-lib" } + +[package.metadata.hax-tests] +into."fstar+coq" = { snapshot = "stdout" } diff --git a/tests/functions/src/lib.rs b/tests/functions/src/lib.rs new file mode 100644 index 000000000..f3c4b4801 --- /dev/null +++ b/tests/functions/src/lib.rs @@ -0,0 +1,6 @@ +/// Issue #757 +fn calling_function_pointer() { + fn f() {} + let f_ptr = f::; + f_ptr(); +}