Skip to content

Commit

Permalink
Merge pull request #651 from hacspec/fix-500
Browse files Browse the repository at this point in the history
feat(engine): allow cast of closures as fn pointers
  • Loading branch information
W95Psp authored May 6, 2024
2 parents 9246d95 + 248b70b commit 5bb39d3
Show file tree
Hide file tree
Showing 4 changed files with 16 additions and 1 deletion.
2 changes: 1 addition & 1 deletion engine/lib/import_thir.ml
Original file line number Diff line number Diff line change
Expand Up @@ -865,7 +865,7 @@ end) : EXPR = struct

and c_pointer e typ span cast source =
match cast with
| ReifyFnPointer ->
| ClosureFnPointer Normal | ReifyFnPointer ->
(* we have arrow types, we do not distinguish between top-level functions and closures *)
(c_expr source).e
| Unsize ->
Expand Down
5 changes: 5 additions & 0 deletions test-harness/src/snapshots/toolchain__literals into-coq.snap
Original file line number Diff line number Diff line change
Expand Up @@ -53,6 +53,11 @@ Definition casts (x8 : int8) (x16 : int16) (x32 : int32) (x64 : int64) (xs : uin
let (_ : int8) := ((((cast x8).+(cast x16)).+(cast x32)).+(cast x64)).+(cast xs) : int8 in
tt.

Definition fn_pointer_cast (_ : unit) : unit :=
let (f : int32 -> int32) := fun x =>
x : int32 -> int32 in
tt.

Definition numeric (_ : unit) : unit :=
let (_ : uint_size) := (@repr WORDSIZE32 123) : uint_size in
let (_ : uint_size) := (@repr WORDSIZE32 42) : uint_size in
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -104,6 +104,11 @@ let casts (x8: u8) (x16: u16) (x32: u32) (x64: u64) (xs: usize) : Prims.unit =
in
()

/// https://github.com/hacspec/hax/issues/500
let fn_pointer_cast (_: Prims.unit) : Prims.unit =
let (f: (u32 -> u32)): u32 -> u32 = fun x -> x in
()

let numeric (_: Prims.unit) : Prims.unit =
let (_: usize):usize = sz 123 in
let (_: isize):isize = isz (-42) in
Expand Down
5 changes: 5 additions & 0 deletions tests/literals/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -76,3 +76,8 @@ fn casts(x8: u8, x16: u16, x32: u32, x64: u64, xs: usize) {
pub fn empty_array() {
let _: &[u8] = &[];
}

/// https://github.com/hacspec/hax/issues/500
fn fn_pointer_cast() {
let f: fn(&u32) -> &u32 = |x| x;
}

0 comments on commit 5bb39d3

Please sign in to comment.