From ec7e6a36203f7ed4661b220a7c63e17db16f70a2 Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Tue, 25 Nov 2025 13:44:00 -0800 Subject: [PATCH 1/4] Allow double quotes in cremepat to simplify pattern-match on trait impls --- cremepat/Lex.ml | 12 ++++++++++++ cremepat/Parse.mly | 4 +++- lib/Cleanup2.ml | 13 ++++++++----- 3 files changed, 23 insertions(+), 6 deletions(-) diff --git a/cremepat/Lex.ml b/cremepat/Lex.ml index 80285b31..537be322 100644 --- a/cremepat/Lex.ml +++ b/cremepat/Lex.ml @@ -65,6 +65,7 @@ let rec token lexbuf = (* | "_" -> locate lexbuf UNDERSCORE *) | "::" -> locate lexbuf COLONCOLON | ":" -> locate lexbuf COLON + | "\"" -> string (Buffer.create 16) lexbuf | "\n" -> incr lines; cur_line := fst (loc lexbuf); @@ -75,3 +76,14 @@ let rec token lexbuf = let l = Utf8.lexeme lexbuf in failwith (Printf.sprintf "unhandled token: %s, len=%d" l (String.length l)) | _ -> assert false + +and string b lexbuf = + match%sedlex lexbuf with + | "\\\"" -> + Buffer.add_string b "\""; + string b lexbuf + | "\"" -> locate lexbuf (STRING (Buffer.contents b)) + | any -> + Buffer.add_string b (Utf8.lexeme lexbuf); + string b lexbuf + | _ -> assert false diff --git a/cremepat/Parse.mly b/cremepat/Parse.mly index 3d7dcec5..9d6db1d3 100644 --- a/cremepat/Parse.mly +++ b/cremepat/Parse.mly @@ -3,7 +3,7 @@ %} %token INT -%token UIDENT LIDENT UVAR UVARLIST +%token UIDENT LIDENT UVAR UVARLIST STRING %token EOF COMMA EQUALS LBRACK RBRACK LBRACKHASH LANGLE RANGLE LCURLY RCURLY %token COLON COLONCOLON AMP LPAREN RPAREN LPARENHASH SEMI %token MATCH TRUE FALSE LET WHILE BREAK ARROW ABORT @@ -40,6 +40,8 @@ ident: path_item: | i = ident { Name i } +| s = STRING + { Name s } | p = UVAR { if p = "" then Wild else Var p } | _p = UVARLIST diff --git a/lib/Cleanup2.ml b/lib/Cleanup2.ml index 67aa03ca..89888927 100644 --- a/lib/Cleanup2.ml +++ b/lib/Cleanup2.ml @@ -1135,11 +1135,14 @@ let cosmetic = method! visit_expr _ e = match e with - | [%cremepat {| core::slice::?impl::len(Eurydice::array_to_slice_shared[#?n](?)) |}] - when impl = "{@Slice}" -> n - | [%cremepat {| core::slice::?impl::len(Eurydice::array_to_slice_mut[#?n](?)) |}] - when impl = "{@Slice}" -> n - | [%cremepat {| core::slice::?impl::len(?e) |}] when impl = "{@Slice}" -> + | [%cremepat + {| + core::slice::"{@Slice}"::len(Eurydice::array_to_slice_shared[#?n](?)) + |}] + -> n + | [%cremepat + {| core::slice::"{@Slice}"::len(Eurydice::array_to_slice_mut[#?n](?)) |}] -> n + | [%cremepat {| core::slice::"{@Slice}"::len(?e) |}] -> with_type (TInt SizeT) (EField (e, "meta")) | [%cremepat {| Eurydice::slice_index_mut(?s, ?i) |}] -> with_type e.typ From a2823b001227789d74f327e74b6cbf3631b75fd0 Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Tue, 25 Nov 2025 13:47:37 -0800 Subject: [PATCH 2/4] Remove unused stuff from the glue --- include/eurydice_glue.h | 5 ----- 1 file changed, 5 deletions(-) diff --git a/include/eurydice_glue.h b/include/eurydice_glue.h index 7655f6db..1883a06b 100644 --- a/include/eurydice_glue.h +++ b/include/eurydice_glue.h @@ -386,11 +386,6 @@ core_num_nonzero_private___core__clone__Clone_for_core__num__nonzero__private__N #define core_iter_range__core__iter__traits__iterator__Iterator_A__for_core__ops__range__Range_A__TraitClause_0___next \ Eurydice_range_iter_next -// See note in karamel/lib/Inlining.ml if you change this -#define Eurydice_into_iter(x, t, _ret_t, _) (x) -#define core_iter_traits_collect__core__iter__traits__collect__IntoIterator_Clause1_Item__I__for_I__into_iter \ - Eurydice_into_iter - // STRINGS typedef char Eurydice_c_char_t; From 97fc6ef03c6b6912135105af9cf1df41d7f6d3bf Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Tue, 25 Nov 2025 14:19:34 -0800 Subject: [PATCH 3/4] Split headers into logical units --- Makefile | 2 +- bin/main.ml | 5 +- include/eurydice_glue.h | 509 +----------------- out/test-array/array.h | 2 +- out/test-array2d/array2d.h | 2 +- out/test-castunsize/castunsize.h | 2 +- out/test-closure/closure.h | 2 +- out/test-closure_fn_cast/closure_fn_cast.h | 2 +- out/test-collision/collision.h | 2 +- out/test-const_generics/const_generics.h | 2 +- out/test-core_num/core_num.h | 2 +- out/test-dst/dst.h | 2 +- .../dyn_trait_struct_type.h | 2 +- out/test-floating_points/floating_points.h | 2 +- out/test-fn_cast/fn_cast.h | 2 +- out/test-fn_higher_order/fn_higher_order.h | 2 +- out/test-for/for.h | 2 +- out/test-global_ref/global_ref.h | 2 +- .../inline_attributes.h | 2 +- out/test-int_switch/int_switch.h | 2 +- out/test-issue_102/issue_102.h | 2 +- out/test-issue_104/issue_104.h | 2 +- out/test-issue_105/issue_105.h | 2 +- out/test-issue_106/issue_106.h | 2 +- out/test-issue_107/issue_107.h | 2 +- out/test-issue_123/issue_123.h | 2 +- out/test-issue_128/issue_128.h | 2 +- out/test-issue_212/issue_212.h | 2 +- out/test-issue_37/issue_37.h | 2 +- out/test-issue_49/issue_49.h | 2 +- out/test-issue_96/issue_96.h | 2 +- out/test-issue_k630/issue_k630.h | 2 +- .../internal/libcrux_core.h | 2 +- .../internal/libcrux_mlkem1024_avx2.h | 2 +- .../internal/libcrux_mlkem1024_portable.h | 2 +- .../internal/libcrux_mlkem512_avx2.h | 2 +- .../internal/libcrux_mlkem512_portable.h | 2 +- .../internal/libcrux_mlkem768_avx2.h | 2 +- .../internal/libcrux_mlkem768_portable.h | 2 +- .../internal/libcrux_mlkem_avx2.h | 2 +- .../internal/libcrux_mlkem_portable.h | 2 +- out/test-libcrux-no-const/libcrux_core.h | 2 +- out/test-libcrux-no-const/libcrux_mlkem1024.h | 2 +- .../libcrux_mlkem1024_avx2.h | 2 +- .../libcrux_mlkem1024_portable.h | 2 +- out/test-libcrux-no-const/libcrux_mlkem512.h | 2 +- .../libcrux_mlkem512_avx2.h | 2 +- .../libcrux_mlkem512_portable.h | 2 +- out/test-libcrux-no-const/libcrux_mlkem768.h | 2 +- .../libcrux_mlkem768_avx2.h | 2 +- .../libcrux_mlkem768_portable.h | 2 +- .../libcrux_mlkem_avx2.h | 2 +- .../libcrux_mlkem_portable.h | 2 +- out/test-libcrux-no-const/libcrux_sha3_avx2.h | 2 +- .../libcrux_sha3_portable.h | 2 +- out/test-libcrux/internal/libcrux_core.h | 2 +- .../internal/libcrux_mlkem1024_avx2.h | 2 +- .../internal/libcrux_mlkem1024_portable.h | 2 +- .../internal/libcrux_mlkem512_avx2.h | 2 +- .../internal/libcrux_mlkem512_portable.h | 2 +- .../internal/libcrux_mlkem768_avx2.h | 2 +- .../internal/libcrux_mlkem768_portable.h | 2 +- .../internal/libcrux_mlkem_avx2.h | 2 +- .../internal/libcrux_mlkem_portable.h | 2 +- out/test-libcrux/libcrux_core.h | 2 +- out/test-libcrux/libcrux_mlkem1024.h | 2 +- out/test-libcrux/libcrux_mlkem1024_avx2.h | 2 +- out/test-libcrux/libcrux_mlkem1024_portable.h | 2 +- out/test-libcrux/libcrux_mlkem512.h | 2 +- out/test-libcrux/libcrux_mlkem512_avx2.h | 2 +- out/test-libcrux/libcrux_mlkem512_portable.h | 2 +- out/test-libcrux/libcrux_mlkem768.h | 2 +- out/test-libcrux/libcrux_mlkem768_avx2.h | 2 +- out/test-libcrux/libcrux_mlkem768_portable.h | 2 +- out/test-libcrux/libcrux_mlkem_avx2.h | 2 +- out/test-libcrux/libcrux_mlkem_portable.h | 2 +- out/test-libcrux/libcrux_sha3_avx2.h | 2 +- out/test-libcrux/libcrux_sha3_portable.h | 2 +- out/test-lvalue/lvalue.h | 2 +- out/test-mismatch/mismatch.h | 2 +- out/test-more_dst/more_dst.h | 2 +- .../more_primitive_types.h | 2 +- out/test-more_str/more_str.h | 2 +- out/test-names/names.h | 2 +- out/test-nested_arrays/nested_arrays.h | 2 +- out/test-nested_arrays2/nested_arrays2.h | 2 +- out/test-option/option.h | 2 +- out/test-parentparent/parentparent.h | 2 +- out/test-partial_eq/partial_eq.h | 2 +- out/test-raw_pointers/raw_pointers.h | 2 +- out/test-reborrow/reborrow.h | 2 +- out/test-recursion/recursion.h | 2 +- out/test-repeat/repeat.h | 2 +- out/test-result/result.h | 2 +- out/test-slice_array/slice_array.h | 2 +- out/test-step_by/step_by.h | 2 +- out/test-substr/substr.h | 2 +- out/test-symcrust/internal/Eurydice.h | 2 +- out/test-symcrust/symcrust.h | 2 +- out/test-trait_generics/trait_generics.h | 2 +- out/test-traits/traits.h | 2 +- out/test-traits2/traits2.h | 2 +- out/test-traits3/traits3.h | 2 +- .../we_need_charon_monomorphization.h | 2 +- .../where_clauses_closures.h | 2 +- .../where_clauses_fncg.h | 2 +- .../where_clauses_simple.h | 2 +- out/testxx-result/result.h | 2 +- scripts/format.sh | 2 +- test/core_cmp_lib.c | 2 +- test/main.c | 2 +- 111 files changed, 115 insertions(+), 617 deletions(-) diff --git a/Makefile b/Makefile index 0b55923c..da7b4eb0 100644 --- a/Makefile +++ b/Makefile @@ -186,7 +186,7 @@ nix-magic: update-charon-pin: nix-shell -p jq --run ./scripts/update-charon-pin.sh -FORMAT_FILE=include/eurydice_glue.h +FORMAT_FILE=include/eurydice.h .PHONY: format-check format-check: diff --git a/bin/main.ml b/bin/main.ml index b5c76050..321839fb 100644 --- a/bin/main.ml +++ b/bin/main.ml @@ -18,6 +18,7 @@ Supported options:|} Krml.Options.backtrace := true in let funroll_loops = ref 16 in + let default_include = ref true in let spec = [ "--log", Arg.Set_string O.log_level, " log level, use * for everything"; @@ -36,6 +37,7 @@ Supported options:|} ( "-fc++17-compat", Arg.Set Krml.Options.cxx17_compat, " instead of generating C11/C++20 code (default), generate C++17-only code" ); + "--no-default-include", Arg.Clear default_include, " do not insert #include \"eurydice.h\""; ] in let spec = Arg.align spec in @@ -84,7 +86,8 @@ Supported options:|} allow_tapps := true; minimal := true; curly_braces := true; - add_very_early_include := [ All, "\"eurydice_glue.h\"" ]; + if !default_include then + add_very_early_include := [ All, "\"eurydice.h\"" ]; parentheses := true; no_shadow := true; extern_c := true; diff --git a/include/eurydice_glue.h b/include/eurydice_glue.h index 1883a06b..31dd3e87 100644 --- a/include/eurydice_glue.h +++ b/include/eurydice_glue.h @@ -1,510 +1,5 @@ #pragma once -#include -#include -#include -#include -#include +#warning "Please include eurydice.h from here on" -#ifdef _MSC_VER -// For __popcnt -#include -#endif - -#include "krml/internal/target.h" -#include "krml/lowstar_endianness.h" - -// C++ HELPERS - -#if defined(__cplusplus) - -#ifndef KRML_HOST_EPRINTF -#define KRML_HOST_EPRINTF(...) fprintf(stderr, __VA_ARGS__) -#endif - -#include - -#ifndef __cpp_lib_type_identity -template struct type_identity { - using type = T; -}; - -template using type_identity_t = typename type_identity::type; -#else -using std::type_identity_t; -#endif - -#define KRML_UNION_CONSTRUCTOR(T) \ - template \ - constexpr T(int t, V U::*m, type_identity_t v) : tag(t) { \ - val.*m = std::move(v); \ - } \ - T() = default; - -#endif - -// GENERAL-PURPOSE STUFF - -#define LowStar_Ignore_ignore(e, t, _ret_t) ((void)e) - -#define EURYDICE_ASSERT(test, msg) \ - do { \ - if (!(test)) { \ - fprintf(stderr, "assertion \"%s\" failed: file \"%s\", line %d\n", msg, \ - __FILE__, __LINE__); \ - exit(255); \ - } \ - } while (0) - -// SIZEOF, ALIGNOF - -#define Eurydice_sizeof(t) sizeof(t) - -#define Eurydice_alignof(t) alignof(t) - -// SLICES, ARRAYS, ETC. - -// For convenience, we give these common slice types, below, a distinguished -// status and rather than emit them in the client code, we skip their -// code-generation in Cleanup3.ml and write them by hand here. This makes it -// easy to write interop code that brings those definitions in scope. - -// &[u8] -typedef struct Eurydice_borrow_slice_u8_s { - const uint8_t *ptr; - size_t meta; -} Eurydice_borrow_slice_u8; - -// &[u16] -typedef struct Eurydice_borrow_slice_i16_s { - const int16_t *ptr; - size_t meta; -} Eurydice_borrow_slice_i16; - -// &mut [u8] -typedef struct Eurydice_mut_borrow_slice_u8_s { - uint8_t *ptr; - size_t meta; -} Eurydice_mut_borrow_slice_u8; - -// &mut [u16] -typedef struct Eurydice_mut_borrow_slice_i16_s { - int16_t *ptr; - size_t meta; -} Eurydice_mut_borrow_slice_i16; - -#if defined(__cplusplus) -#define KRML_CLITERAL(type) type -#else -#define KRML_CLITERAL(type) (type) -#endif - -#if defined(__cplusplus) && defined(__cpp_designated_initializers) || \ - !(defined(__cplusplus)) -#define EURYDICE_CFIELD(X) X -#else -#define EURYDICE_CFIELD(X) -#endif - -#define Eurydice_array_repeat(dst, len, init, t) \ - ERROR "should've been desugared" - -// Copy a slice with memcopy -#define Eurydice_slice_copy(dst, src, t) \ - memcpy(dst.ptr, src.ptr, dst.meta * sizeof(t)) - -#define core_array___Array_T__N___as_slice(len_, ptr_, t, ret_t) \ - (KRML_CLITERAL(ret_t){EURYDICE_CFIELD(.ptr =)(ptr_)->data, \ - EURYDICE_CFIELD(.meta =) len_}) - -#define core_array__core__clone__Clone_for__Array_T__N___clone( \ - len, src, elem_type, _ret_t) \ - (*(src)) -#define TryFromSliceError uint8_t -#define core_array_TryFromSliceError uint8_t - -// Distinguished support for some PartialEq trait implementations -// -// core::cmp::PartialEq<@Array> for @Array -#define Eurydice_array_eq(sz, a1, a2, t) \ - (memcmp((a1)->data, (a2)->data, sz * sizeof(t)) == 0) -// core::cmp::PartialEq<&0 (@Slice)> for @Array -#define Eurydice_array_eq_slice_shared(sz, a1, s2, t, _) \ - (memcmp((a1)->data, (s2)->ptr, sz * sizeof(t)) == 0) -#define Eurydice_array_eq_slice_mut(sz, a1, s2, t, _) \ - Eurydice_array_eq_slice_shared(sz, a1, s2, t, _) - -// DEPRECATED -- should no longer be generated -#define core_array_equality__core__cmp__PartialEq__Array_U__N___for__Array_T__N___eq( \ - sz, a1, a2, t, _, _ret_t) \ - Eurydice_array_eq(sz, a1, a2, t) -#define core_array_equality__core__cmp__PartialEq__0___Slice_U____for__Array_T__N___eq( \ - sz, a1, a2, t, _, _ret_t) \ - Eurydice_array_eq(sz, a1, ((a2)->ptr), t) -#define core_cmp_impls__core__cmp__PartialEq__0_mut__B___for__1_mut__A___eq( \ - _m0, _m1, src1, src2, _0, _1, T) \ - Eurydice_slice_eq(src1, src2, _, _, T, _) - -#define Eurydice_slice_split_at(slice, mid, element_type, ret_t) \ - KRML_CLITERAL(ret_t) { \ - EURYDICE_CFIELD(.fst =){EURYDICE_CFIELD(.ptr =)((slice).ptr), \ - EURYDICE_CFIELD(.meta =) mid}, \ - EURYDICE_CFIELD(.snd =) { \ - EURYDICE_CFIELD(.ptr =) \ - ((slice).ptr + mid), EURYDICE_CFIELD(.meta =)((slice).meta - mid) \ - } \ - } - -#define Eurydice_slice_split_at_mut(slice, mid, element_type, ret_t) \ - KRML_CLITERAL(ret_t) { \ - EURYDICE_CFIELD(.fst =){EURYDICE_CFIELD(.ptr =)((slice).ptr), \ - EURYDICE_CFIELD(.meta =) mid}, \ - EURYDICE_CFIELD(.snd =) { \ - EURYDICE_CFIELD(.ptr =) \ - ((slice).ptr + mid), EURYDICE_CFIELD(.meta =)((slice).meta - mid) \ - } \ - } - -// Conversion of slice to an array, rewritten (by Eurydice) to name the -// destination array, since arrays are not values in C. -// N.B.: see note in karamel/lib/Inlining.ml if you change this. - -#define Eurydice_slice_to_ref_array2(len_, src, arr_ptr, t_ptr, t_arr, t_err, \ - t_res) \ - (src.meta >= len_ \ - ? ((t_res){.tag = core_result_Ok, .val = {.case_Ok = arr_ptr}}) \ - : ((t_res){.tag = core_result_Err, .val = {.case_Err = 0}})) - -// CORE STUFF (conversions, endianness, ...) - -// We slap extern "C" on declarations that intend to implement a prototype -// generated by Eurydice, because Eurydice prototypes are always emitted within -// an extern "C" block, UNLESS you use -fcxx17-compat, in which case, you must -// pass -DKRML_CXX17_COMPAT="" to your C++ compiler. -#if defined(__cplusplus) && !defined(KRML_CXX17_COMPAT) -extern "C" { -#endif - -#define core_hint_black_box(X, _0, _1) (X) - -// [ u8; 2 ] -typedef struct Eurydice_array_u8x2_s { - uint8_t data[2]; -} Eurydice_array_u8x2; - -// [ u8; 4 ] -typedef struct Eurydice_array_u8x4_s { - uint8_t data[4]; -} Eurydice_array_u8x4; - -// [ u8; 8 ] -typedef struct Eurydice_array_u8x8_s { - uint8_t data[8]; -} Eurydice_array_u8x8; - -static inline uint16_t core_num__u16__from_le_bytes(Eurydice_array_u8x2 buf) { - return load16_le(buf.data); -} - -static inline Eurydice_array_u8x4 core_num__u32__to_be_bytes(uint32_t src) { - // TODO: why not store32_be? - Eurydice_array_u8x4 a; - uint32_t x = htobe32(src); - memcpy(a.data, &x, 4); - return a; -} - -static inline Eurydice_array_u8x4 core_num__u32__to_le_bytes(uint32_t src) { - Eurydice_array_u8x4 a; - store32_le(a.data, src); - return a; -} - -static inline uint32_t core_num__u32__from_le_bytes(Eurydice_array_u8x4 buf) { - return load32_le(buf.data); -} - -static inline Eurydice_array_u8x8 core_num__u64__to_le_bytes(uint64_t v) { - Eurydice_array_u8x8 a; - store64_le(a.data, v); - return a; -} - -static inline uint64_t core_num__u64__from_le_bytes(Eurydice_array_u8x8 buf) { - return load64_le(buf.data); -} - -static inline int64_t -core_convert_num__core__convert__From_i32__for_i64__from(int32_t x) { - return x; -} - -static inline uint64_t -core_convert_num__core__convert__From_u8__for_u64__from(uint8_t x) { - return x; -} - -static inline uint64_t -core_convert_num__core__convert__From_u16__for_u64__from(uint16_t x) { - return x; -} - -static inline size_t -core_convert_num__core__convert__From_u16__for_usize__from(uint16_t x) { - return x; -} - -static inline uint32_t core_num__u8__count_ones(uint8_t x0) { -#ifdef _MSC_VER - return __popcnt(x0); -#else - return __builtin_popcount(x0); -#endif -} - -static inline uint32_t core_num__u32__count_ones(uint32_t x0) { -#ifdef _MSC_VER - return __popcnt(x0); -#else - return __builtin_popcount(x0); -#endif -} - -static inline uint32_t core_num__i32__count_ones(int32_t x0) { -#ifdef _MSC_VER - return __popcnt(x0); -#else - return __builtin_popcount(x0); -#endif -} - -static inline size_t core_cmp_impls__core__cmp__Ord_for_usize__min(size_t a, - size_t b) { - if (a <= b) - return a; - else - return b; -} - -// unsigned overflow wraparound semantics in C -static inline uint8_t core_num__u8__wrapping_sub(uint8_t x, uint8_t y) { - return x - y; -} -static inline uint8_t core_num__u8__wrapping_add(uint8_t x, uint8_t y) { - return x + y; -} -static inline uint8_t core_num__u8__wrapping_mul(uint8_t x, uint8_t y) { - return x * y; -} -static inline uint16_t core_num__u16__wrapping_sub(uint16_t x, uint16_t y) { - return x - y; -} -static inline uint16_t core_num__u16__wrapping_add(uint16_t x, uint16_t y) { - return x + y; -} -static inline uint16_t core_num__u16__wrapping_mul(uint16_t x, uint16_t y) { - return x * y; -} -static inline uint32_t core_num__u32__wrapping_sub(uint32_t x, uint32_t y) { - return x - y; -} -static inline uint32_t core_num__u32__wrapping_add(uint32_t x, uint32_t y) { - return x + y; -} -static inline uint32_t core_num__u32__wrapping_mul(uint32_t x, uint32_t y) { - return x * y; -} -static inline uint64_t core_num__u64__wrapping_sub(uint64_t x, uint64_t y) { - return x - y; -} -static inline uint64_t core_num__u64__wrapping_add(uint64_t x, uint64_t y) { - return x + y; -} -static inline uint64_t core_num__u64__wrapping_mul(uint64_t x, uint64_t y) { - return x * y; -} -static inline size_t core_num__usize__wrapping_sub(size_t x, size_t y) { - return x - y; -} -static inline size_t core_num__usize__wrapping_add(size_t x, size_t y) { - return x + y; -} -static inline size_t core_num__usize__wrapping_mul(size_t x, size_t y) { - return x * y; -} - -static inline uint64_t core_num__u64__rotate_left(uint64_t x0, uint32_t x1) { - return (x0 << x1) | (x0 >> ((-x1) & 63)); -} - -static inline void core_ops_arith__i32__add_assign(int32_t *x0, int32_t *x1) { - *x0 = *x0 + *x1; -} - -static inline uint8_t Eurydice_bitand_pv_u8(uint8_t *p, uint8_t v) { - return (*p) & v; -} -static inline uint8_t Eurydice_shr_pv_u8(uint8_t *p, int32_t v) { - return (*p) >> v; -} -static inline uint32_t Eurydice_min_u32(uint32_t x, uint32_t y) { - return x < y ? x : y; -} - -static inline uint8_t -core_ops_bit__core__ops__bit__BitAnd_u8__u8__for___a__u8___bitand(uint8_t *x0, - uint8_t x1) { - return Eurydice_bitand_pv_u8(x0, x1); -} - -static inline uint8_t -core_ops_bit__core__ops__bit__Shr_i32__u8__for___a__u8___shr(uint8_t *x0, - int32_t x1) { - return Eurydice_shr_pv_u8(x0, x1); -} - -#define core_num_nonzero_private_NonZeroUsizeInner size_t -static inline core_num_nonzero_private_NonZeroUsizeInner -core_num_nonzero_private___core__clone__Clone_for_core__num__nonzero__private__NonZeroUsizeInner___clone( - core_num_nonzero_private_NonZeroUsizeInner *x0) { - return *x0; -} - -#if defined(__cplusplus) && !defined(KRML_CXX17_COMPAT) -} -#endif - -// ITERATORS - -#define Eurydice_range_iter_next(iter_ptr, t, ret_t) \ - (((iter_ptr)->start >= (iter_ptr)->end) \ - ? (KRML_CLITERAL(ret_t){EURYDICE_CFIELD(.tag =) 0, \ - EURYDICE_CFIELD(.f0 =) 0}) \ - : (KRML_CLITERAL(ret_t){EURYDICE_CFIELD(.tag =) 1, \ - EURYDICE_CFIELD(.f0 =)(iter_ptr)->start++})) - -#define core_iter_range__core__iter__traits__iterator__Iterator_A__for_core__ops__range__Range_A__TraitClause_0___next \ - Eurydice_range_iter_next - -// STRINGS - -typedef char Eurydice_c_char_t; -typedef const Eurydice_c_char_t *Prims_string; -typedef void Eurydice_c_void_t; - -// UNSAFE CODE - -#define core_slice___Slice_T___as_mut_ptr(x, t, _) (x.ptr) -#define core_mem_size_of(t, _) (sizeof(t)) -#define core_slice_raw_from_raw_parts_mut(ptr, len, _0, _1) \ - (KRML_CLITERAL(Eurydice_slice){(void *)(ptr), len}) -#define core_slice_raw_from_raw_parts(ptr, len, _0, _1) \ - (KRML_CLITERAL(Eurydice_slice){(void *)(ptr), len}) - -// FIXME: add dedicated extraction to extract NonNull as T* -#define core_ptr_non_null_NonNull void * - -// PRINTING -// -// This is temporary. Ultimately we want to be able to extract all of this. - -typedef void *core_fmt_Formatter; -#define core_fmt_rt__core__fmt__rt__Argument__a___new_display(x1, x2, x3, x4) \ - NULL - -// BOXES - -#ifndef EURYDICE_MALLOC -#define EURYDICE_MALLOC malloc -#endif - -#ifndef EURYDICE_REALLOC -#define EURYDICE_REALLOC realloc -#endif - -static inline char *malloc_and_init(size_t sz, char *init) { - char *ptr = (char *)EURYDICE_MALLOC(sz); - if (ptr != NULL) - memcpy(ptr, init, sz); - return ptr; -} - -#define Eurydice_box_new(init, t, t_dst) \ - ((t_dst)(malloc_and_init(sizeof(t), (char *)(&init)))) - -// Initializer for array of size zero -#define Eurydice_empty_array(dummy, t, t_dst) ((t_dst){.data = {}}) - -#define Eurydice_box_new_array(len, ptr, t, t_dst) \ - ((t_dst)(malloc_and_init(len * sizeof(t), (char *)(ptr)))) - -// FIXME this needs to handle allocation failure errors, but this seems hard to -// do without evaluating malloc_and_init twice... -#define alloc_boxed__alloc__boxed__Box_T___try_new(init, t, t_ret) \ - ((t_ret){.tag = core_result_Ok, \ - .f0 = (t *)malloc_and_init(sizeof(t), (char *)(&init))}) - -// VECTORS - -// We adapt the layout of https://doc.rust-lang.org/std/vec/struct.Vec.html, -// dispensing with the nested RawVec -- basically, we follow what the -// documentation says. Just like Eurydice_slice, we keep sizes in number of -// elements. This means we pass three words by value whenever we carry a vector -// around. Things that modify the vector take &mut's in Rust, or a Eurydice_vec* -// in C. -// -// Another design choice: just like Eurydice_slice, we treat Eurydice_vec as an -// opaque type, and rely on macros receiving their type arguments at call-site -// to perform necessary casts. A downside is that anything that looks into the -// definition of Eurydice_vec must be exposed (from the eurydice point of view) -// as an external -- see, for instance, Eurydice_vec_failed, below. -typedef struct { - char *ptr; - size_t len; /* current length, in elements */ - size_t capacity; /* the size of the allocation, in number of elements */ -} Eurydice_vec, alloc_vec_Vec; - -// This is a helper that Eurydice has special knowledge about. Essentially, -// allocation functions return a result type that has been monomorphized, say, -// Result_XY; this means we need to do something like: -// Eurydice_vec v = try_with_capacity(len, sz); -// Result_XY r = v.ptr == NULL ? (Result_XY) { .tag = core_result_Ok, .case_Ok -// = v } -// : (Result_XY) { .tag = core_result_Error, .case_Error = ... }; -// but with a macro (since we don't have templates). -// However, unless we allow statement-expressions (GCC extension), we cannot do -// the above with an expression, since we need to name the result of -// try_with_capacity to avoid evaluating it twice. -static inline Eurydice_vec Eurydice_vec_alloc2(size_t len, size_t element_sz) { - return ((Eurydice_vec){.ptr = (char *)EURYDICE_MALLOC(len * element_sz), - .len = len, - .capacity = len}); -} - -#define Eurydice_vec_alloc(len, t, _) (Eurydice_vec_alloc2((len), sizeof(t))) -#define Eurydice_vec_overflows(len, t, _) (!((len) <= SIZE_MAX / (sizeof(t)))) -#define Eurydice_vec_failed(v, _, _1) ((v).ptr == NULL) -#define Eurydice_layout(t, _) \ - ((core_alloc_layout_Layout){.size = sizeof(t), .align = _Alignof(t)}) - -#define alloc_vec__alloc__vec__Vec_T___resize( \ - /* Eurydice_vec * */ v, /* size_t */ new_len, /* T */ elt, T, _0, _1) \ - do { \ - if (new_len <= (v)->capacity) \ - (v)->len = new_len; \ - else { \ - (v)->ptr = EURYDICE_REALLOC((v)->ptr, new_len * sizeof(T)); \ - /* TODO: check success? Rust function is infallible */ \ - for (size_t i = (v)->len; i < new_len; i++) \ - ((T *)(v)->ptr)[i] = elt; \ - (v)->len = new_len; \ - (v)->capacity = new_len; \ - } \ - } while (0) - -#define alloc_vec__alloc__vec__Vec_T___into_boxed_slice(/* Eurydice_vec */ v, \ - T, _0, _1) \ - ((Eurydice_slice){.ptr = (v).ptr, .len = (v).len}) - -#define alloc_boxed__alloc__boxed__Box_T___from_raw(x, _0, _1) (x) -#define alloc_boxed__alloc__boxed__Box_T___into_raw(x, _0, _1) (x) +#include "eurydice.h" diff --git a/out/test-array/array.h b/out/test-array/array.h index fec31e13..764db602 100644 --- a/out/test-array/array.h +++ b/out/test-array/array.h @@ -8,7 +8,7 @@ #ifndef array_H #define array_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-array2d/array2d.h b/out/test-array2d/array2d.h index c928de2a..3f664aa6 100644 --- a/out/test-array2d/array2d.h +++ b/out/test-array2d/array2d.h @@ -8,7 +8,7 @@ #ifndef array2d_H #define array2d_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-castunsize/castunsize.h b/out/test-castunsize/castunsize.h index ac703eb0..6398e9e1 100644 --- a/out/test-castunsize/castunsize.h +++ b/out/test-castunsize/castunsize.h @@ -8,7 +8,7 @@ #ifndef castunsize_H #define castunsize_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-closure/closure.h b/out/test-closure/closure.h index 4759824c..906c959a 100644 --- a/out/test-closure/closure.h +++ b/out/test-closure/closure.h @@ -8,7 +8,7 @@ #ifndef closure_H #define closure_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-closure_fn_cast/closure_fn_cast.h b/out/test-closure_fn_cast/closure_fn_cast.h index 3c131a51..613c1312 100644 --- a/out/test-closure_fn_cast/closure_fn_cast.h +++ b/out/test-closure_fn_cast/closure_fn_cast.h @@ -8,7 +8,7 @@ #ifndef closure_fn_cast_H #define closure_fn_cast_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-collision/collision.h b/out/test-collision/collision.h index a08c5285..7689c653 100644 --- a/out/test-collision/collision.h +++ b/out/test-collision/collision.h @@ -8,7 +8,7 @@ #ifndef collision_H #define collision_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-const_generics/const_generics.h b/out/test-const_generics/const_generics.h index 945b234a..6a42eb5f 100644 --- a/out/test-const_generics/const_generics.h +++ b/out/test-const_generics/const_generics.h @@ -8,7 +8,7 @@ #ifndef const_generics_H #define const_generics_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-core_num/core_num.h b/out/test-core_num/core_num.h index d62b6a35..4f66b6dc 100644 --- a/out/test-core_num/core_num.h +++ b/out/test-core_num/core_num.h @@ -8,7 +8,7 @@ #ifndef core_num_H #define core_num_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-dst/dst.h b/out/test-dst/dst.h index bb5f31a5..5ec69635 100644 --- a/out/test-dst/dst.h +++ b/out/test-dst/dst.h @@ -8,7 +8,7 @@ #ifndef dst_H #define dst_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-dyn_trait_struct_type/dyn_trait_struct_type.h b/out/test-dyn_trait_struct_type/dyn_trait_struct_type.h index ced6a67b..9bb93ba6 100644 --- a/out/test-dyn_trait_struct_type/dyn_trait_struct_type.h +++ b/out/test-dyn_trait_struct_type/dyn_trait_struct_type.h @@ -8,7 +8,7 @@ #ifndef dyn_trait_struct_type_H #define dyn_trait_struct_type_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-floating_points/floating_points.h b/out/test-floating_points/floating_points.h index e4d37532..122b1167 100644 --- a/out/test-floating_points/floating_points.h +++ b/out/test-floating_points/floating_points.h @@ -8,7 +8,7 @@ #ifndef floating_points_H #define floating_points_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-fn_cast/fn_cast.h b/out/test-fn_cast/fn_cast.h index 06c20bde..69b75ddf 100644 --- a/out/test-fn_cast/fn_cast.h +++ b/out/test-fn_cast/fn_cast.h @@ -8,7 +8,7 @@ #ifndef fn_cast_H #define fn_cast_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-fn_higher_order/fn_higher_order.h b/out/test-fn_higher_order/fn_higher_order.h index d0235ef1..4e3c8d2d 100644 --- a/out/test-fn_higher_order/fn_higher_order.h +++ b/out/test-fn_higher_order/fn_higher_order.h @@ -8,7 +8,7 @@ #ifndef fn_higher_order_H #define fn_higher_order_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-for/for.h b/out/test-for/for.h index 69f27de1..6dfc55ad 100644 --- a/out/test-for/for.h +++ b/out/test-for/for.h @@ -8,7 +8,7 @@ #ifndef for_H #define for_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-global_ref/global_ref.h b/out/test-global_ref/global_ref.h index 99f390ed..e43ddd32 100644 --- a/out/test-global_ref/global_ref.h +++ b/out/test-global_ref/global_ref.h @@ -8,7 +8,7 @@ #ifndef global_ref_H #define global_ref_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-inline_attributes/inline_attributes.h b/out/test-inline_attributes/inline_attributes.h index c2a19750..a2aaef0e 100644 --- a/out/test-inline_attributes/inline_attributes.h +++ b/out/test-inline_attributes/inline_attributes.h @@ -8,7 +8,7 @@ #ifndef inline_attributes_H #define inline_attributes_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-int_switch/int_switch.h b/out/test-int_switch/int_switch.h index b902a899..be532c3e 100644 --- a/out/test-int_switch/int_switch.h +++ b/out/test-int_switch/int_switch.h @@ -8,7 +8,7 @@ #ifndef int_switch_H #define int_switch_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-issue_102/issue_102.h b/out/test-issue_102/issue_102.h index 7dbe6da1..7bbbe0bb 100644 --- a/out/test-issue_102/issue_102.h +++ b/out/test-issue_102/issue_102.h @@ -8,7 +8,7 @@ #ifndef issue_102_H #define issue_102_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-issue_104/issue_104.h b/out/test-issue_104/issue_104.h index f3f507c5..6213776a 100644 --- a/out/test-issue_104/issue_104.h +++ b/out/test-issue_104/issue_104.h @@ -8,7 +8,7 @@ #ifndef issue_104_H #define issue_104_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-issue_105/issue_105.h b/out/test-issue_105/issue_105.h index 3c1aceb1..3d49effc 100644 --- a/out/test-issue_105/issue_105.h +++ b/out/test-issue_105/issue_105.h @@ -8,7 +8,7 @@ #ifndef issue_105_H #define issue_105_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-issue_106/issue_106.h b/out/test-issue_106/issue_106.h index b3ffeff5..c45dee03 100644 --- a/out/test-issue_106/issue_106.h +++ b/out/test-issue_106/issue_106.h @@ -8,7 +8,7 @@ #ifndef issue_106_H #define issue_106_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-issue_107/issue_107.h b/out/test-issue_107/issue_107.h index 49930ae1..8f39bfbf 100644 --- a/out/test-issue_107/issue_107.h +++ b/out/test-issue_107/issue_107.h @@ -8,7 +8,7 @@ #ifndef issue_107_H #define issue_107_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-issue_123/issue_123.h b/out/test-issue_123/issue_123.h index 42bc72fa..a83b8fbd 100644 --- a/out/test-issue_123/issue_123.h +++ b/out/test-issue_123/issue_123.h @@ -8,7 +8,7 @@ #ifndef issue_123_H #define issue_123_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-issue_128/issue_128.h b/out/test-issue_128/issue_128.h index 7df31b78..1f02e350 100644 --- a/out/test-issue_128/issue_128.h +++ b/out/test-issue_128/issue_128.h @@ -8,7 +8,7 @@ #ifndef issue_128_H #define issue_128_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-issue_212/issue_212.h b/out/test-issue_212/issue_212.h index b0519295..15636f96 100644 --- a/out/test-issue_212/issue_212.h +++ b/out/test-issue_212/issue_212.h @@ -8,7 +8,7 @@ #ifndef issue_212_H #define issue_212_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-issue_37/issue_37.h b/out/test-issue_37/issue_37.h index bc188144..2abc17c4 100644 --- a/out/test-issue_37/issue_37.h +++ b/out/test-issue_37/issue_37.h @@ -8,7 +8,7 @@ #ifndef issue_37_H #define issue_37_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-issue_49/issue_49.h b/out/test-issue_49/issue_49.h index 1519190c..9e9295a0 100644 --- a/out/test-issue_49/issue_49.h +++ b/out/test-issue_49/issue_49.h @@ -8,7 +8,7 @@ #ifndef issue_49_H #define issue_49_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-issue_96/issue_96.h b/out/test-issue_96/issue_96.h index ff5c3436..3381855c 100644 --- a/out/test-issue_96/issue_96.h +++ b/out/test-issue_96/issue_96.h @@ -8,7 +8,7 @@ #ifndef issue_96_H #define issue_96_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-issue_k630/issue_k630.h b/out/test-issue_k630/issue_k630.h index 811e5592..586297f2 100644 --- a/out/test-issue_k630/issue_k630.h +++ b/out/test-issue_k630/issue_k630.h @@ -8,7 +8,7 @@ #ifndef issue_k630_H #define issue_k630_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux-no-const/internal/libcrux_core.h b/out/test-libcrux-no-const/internal/libcrux_core.h index 1d08f61a..1b86c08b 100644 --- a/out/test-libcrux-no-const/internal/libcrux_core.h +++ b/out/test-libcrux-no-const/internal/libcrux_core.h @@ -8,7 +8,7 @@ #ifndef internal_libcrux_core_H #define internal_libcrux_core_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux-no-const/internal/libcrux_mlkem1024_avx2.h b/out/test-libcrux-no-const/internal/libcrux_mlkem1024_avx2.h index f05c911a..558edd96 100644 --- a/out/test-libcrux-no-const/internal/libcrux_mlkem1024_avx2.h +++ b/out/test-libcrux-no-const/internal/libcrux_mlkem1024_avx2.h @@ -8,7 +8,7 @@ #ifndef internal_libcrux_mlkem1024_avx2_H #define internal_libcrux_mlkem1024_avx2_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux-no-const/internal/libcrux_mlkem1024_portable.h b/out/test-libcrux-no-const/internal/libcrux_mlkem1024_portable.h index fbe2eb4e..976af248 100644 --- a/out/test-libcrux-no-const/internal/libcrux_mlkem1024_portable.h +++ b/out/test-libcrux-no-const/internal/libcrux_mlkem1024_portable.h @@ -8,7 +8,7 @@ #ifndef internal_libcrux_mlkem1024_portable_H #define internal_libcrux_mlkem1024_portable_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux-no-const/internal/libcrux_mlkem512_avx2.h b/out/test-libcrux-no-const/internal/libcrux_mlkem512_avx2.h index fc84ca78..074c80f2 100644 --- a/out/test-libcrux-no-const/internal/libcrux_mlkem512_avx2.h +++ b/out/test-libcrux-no-const/internal/libcrux_mlkem512_avx2.h @@ -8,7 +8,7 @@ #ifndef internal_libcrux_mlkem512_avx2_H #define internal_libcrux_mlkem512_avx2_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux-no-const/internal/libcrux_mlkem512_portable.h b/out/test-libcrux-no-const/internal/libcrux_mlkem512_portable.h index 02e858f1..6630df30 100644 --- a/out/test-libcrux-no-const/internal/libcrux_mlkem512_portable.h +++ b/out/test-libcrux-no-const/internal/libcrux_mlkem512_portable.h @@ -8,7 +8,7 @@ #ifndef internal_libcrux_mlkem512_portable_H #define internal_libcrux_mlkem512_portable_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux-no-const/internal/libcrux_mlkem768_avx2.h b/out/test-libcrux-no-const/internal/libcrux_mlkem768_avx2.h index 9198afef..a0e95728 100644 --- a/out/test-libcrux-no-const/internal/libcrux_mlkem768_avx2.h +++ b/out/test-libcrux-no-const/internal/libcrux_mlkem768_avx2.h @@ -8,7 +8,7 @@ #ifndef internal_libcrux_mlkem768_avx2_H #define internal_libcrux_mlkem768_avx2_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux-no-const/internal/libcrux_mlkem768_portable.h b/out/test-libcrux-no-const/internal/libcrux_mlkem768_portable.h index 2fa167ea..0f2f1379 100644 --- a/out/test-libcrux-no-const/internal/libcrux_mlkem768_portable.h +++ b/out/test-libcrux-no-const/internal/libcrux_mlkem768_portable.h @@ -8,7 +8,7 @@ #ifndef internal_libcrux_mlkem768_portable_H #define internal_libcrux_mlkem768_portable_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux-no-const/internal/libcrux_mlkem_avx2.h b/out/test-libcrux-no-const/internal/libcrux_mlkem_avx2.h index 46d58112..b69cfd83 100644 --- a/out/test-libcrux-no-const/internal/libcrux_mlkem_avx2.h +++ b/out/test-libcrux-no-const/internal/libcrux_mlkem_avx2.h @@ -8,7 +8,7 @@ #ifndef internal_libcrux_mlkem_avx2_H #define internal_libcrux_mlkem_avx2_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux-no-const/internal/libcrux_mlkem_portable.h b/out/test-libcrux-no-const/internal/libcrux_mlkem_portable.h index 01d7afd8..ca71ad48 100644 --- a/out/test-libcrux-no-const/internal/libcrux_mlkem_portable.h +++ b/out/test-libcrux-no-const/internal/libcrux_mlkem_portable.h @@ -8,7 +8,7 @@ #ifndef internal_libcrux_mlkem_portable_H #define internal_libcrux_mlkem_portable_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux-no-const/libcrux_core.h b/out/test-libcrux-no-const/libcrux_core.h index 1c26bba2..2830afda 100644 --- a/out/test-libcrux-no-const/libcrux_core.h +++ b/out/test-libcrux-no-const/libcrux_core.h @@ -8,7 +8,7 @@ #ifndef libcrux_core_H #define libcrux_core_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux-no-const/libcrux_mlkem1024.h b/out/test-libcrux-no-const/libcrux_mlkem1024.h index 1725ecf6..03574413 100644 --- a/out/test-libcrux-no-const/libcrux_mlkem1024.h +++ b/out/test-libcrux-no-const/libcrux_mlkem1024.h @@ -8,7 +8,7 @@ #ifndef libcrux_mlkem1024_H #define libcrux_mlkem1024_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux-no-const/libcrux_mlkem1024_avx2.h b/out/test-libcrux-no-const/libcrux_mlkem1024_avx2.h index e865e597..ded0ae33 100644 --- a/out/test-libcrux-no-const/libcrux_mlkem1024_avx2.h +++ b/out/test-libcrux-no-const/libcrux_mlkem1024_avx2.h @@ -8,7 +8,7 @@ #ifndef libcrux_mlkem1024_avx2_H #define libcrux_mlkem1024_avx2_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux-no-const/libcrux_mlkem1024_portable.h b/out/test-libcrux-no-const/libcrux_mlkem1024_portable.h index b97be75a..02fa2ee4 100644 --- a/out/test-libcrux-no-const/libcrux_mlkem1024_portable.h +++ b/out/test-libcrux-no-const/libcrux_mlkem1024_portable.h @@ -8,7 +8,7 @@ #ifndef libcrux_mlkem1024_portable_H #define libcrux_mlkem1024_portable_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux-no-const/libcrux_mlkem512.h b/out/test-libcrux-no-const/libcrux_mlkem512.h index f92f40a4..467d1dc8 100644 --- a/out/test-libcrux-no-const/libcrux_mlkem512.h +++ b/out/test-libcrux-no-const/libcrux_mlkem512.h @@ -8,7 +8,7 @@ #ifndef libcrux_mlkem512_H #define libcrux_mlkem512_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux-no-const/libcrux_mlkem512_avx2.h b/out/test-libcrux-no-const/libcrux_mlkem512_avx2.h index ad2bbca8..43bb3a8c 100644 --- a/out/test-libcrux-no-const/libcrux_mlkem512_avx2.h +++ b/out/test-libcrux-no-const/libcrux_mlkem512_avx2.h @@ -8,7 +8,7 @@ #ifndef libcrux_mlkem512_avx2_H #define libcrux_mlkem512_avx2_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux-no-const/libcrux_mlkem512_portable.h b/out/test-libcrux-no-const/libcrux_mlkem512_portable.h index 21bde63a..82c0734d 100644 --- a/out/test-libcrux-no-const/libcrux_mlkem512_portable.h +++ b/out/test-libcrux-no-const/libcrux_mlkem512_portable.h @@ -8,7 +8,7 @@ #ifndef libcrux_mlkem512_portable_H #define libcrux_mlkem512_portable_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux-no-const/libcrux_mlkem768.h b/out/test-libcrux-no-const/libcrux_mlkem768.h index a6490afd..f5441d3e 100644 --- a/out/test-libcrux-no-const/libcrux_mlkem768.h +++ b/out/test-libcrux-no-const/libcrux_mlkem768.h @@ -8,7 +8,7 @@ #ifndef libcrux_mlkem768_H #define libcrux_mlkem768_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux-no-const/libcrux_mlkem768_avx2.h b/out/test-libcrux-no-const/libcrux_mlkem768_avx2.h index c5097c5f..7187b6ed 100644 --- a/out/test-libcrux-no-const/libcrux_mlkem768_avx2.h +++ b/out/test-libcrux-no-const/libcrux_mlkem768_avx2.h @@ -8,7 +8,7 @@ #ifndef libcrux_mlkem768_avx2_H #define libcrux_mlkem768_avx2_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux-no-const/libcrux_mlkem768_portable.h b/out/test-libcrux-no-const/libcrux_mlkem768_portable.h index 9fe38bb6..217d0014 100644 --- a/out/test-libcrux-no-const/libcrux_mlkem768_portable.h +++ b/out/test-libcrux-no-const/libcrux_mlkem768_portable.h @@ -8,7 +8,7 @@ #ifndef libcrux_mlkem768_portable_H #define libcrux_mlkem768_portable_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux-no-const/libcrux_mlkem_avx2.h b/out/test-libcrux-no-const/libcrux_mlkem_avx2.h index 6c44e4e7..67858c02 100644 --- a/out/test-libcrux-no-const/libcrux_mlkem_avx2.h +++ b/out/test-libcrux-no-const/libcrux_mlkem_avx2.h @@ -8,7 +8,7 @@ #ifndef libcrux_mlkem_avx2_H #define libcrux_mlkem_avx2_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux-no-const/libcrux_mlkem_portable.h b/out/test-libcrux-no-const/libcrux_mlkem_portable.h index f5eb1ed0..3a67d234 100644 --- a/out/test-libcrux-no-const/libcrux_mlkem_portable.h +++ b/out/test-libcrux-no-const/libcrux_mlkem_portable.h @@ -8,7 +8,7 @@ #ifndef libcrux_mlkem_portable_H #define libcrux_mlkem_portable_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux-no-const/libcrux_sha3_avx2.h b/out/test-libcrux-no-const/libcrux_sha3_avx2.h index 67223717..bae1bc2b 100644 --- a/out/test-libcrux-no-const/libcrux_sha3_avx2.h +++ b/out/test-libcrux-no-const/libcrux_sha3_avx2.h @@ -8,7 +8,7 @@ #ifndef libcrux_sha3_avx2_H #define libcrux_sha3_avx2_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux-no-const/libcrux_sha3_portable.h b/out/test-libcrux-no-const/libcrux_sha3_portable.h index c232de99..6ed7afa3 100644 --- a/out/test-libcrux-no-const/libcrux_sha3_portable.h +++ b/out/test-libcrux-no-const/libcrux_sha3_portable.h @@ -8,7 +8,7 @@ #ifndef libcrux_sha3_portable_H #define libcrux_sha3_portable_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux/internal/libcrux_core.h b/out/test-libcrux/internal/libcrux_core.h index d1136b8c..8b435749 100644 --- a/out/test-libcrux/internal/libcrux_core.h +++ b/out/test-libcrux/internal/libcrux_core.h @@ -8,7 +8,7 @@ #ifndef internal_libcrux_core_H #define internal_libcrux_core_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux/internal/libcrux_mlkem1024_avx2.h b/out/test-libcrux/internal/libcrux_mlkem1024_avx2.h index 29f04ea0..2a9b8986 100644 --- a/out/test-libcrux/internal/libcrux_mlkem1024_avx2.h +++ b/out/test-libcrux/internal/libcrux_mlkem1024_avx2.h @@ -8,7 +8,7 @@ #ifndef internal_libcrux_mlkem1024_avx2_H #define internal_libcrux_mlkem1024_avx2_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux/internal/libcrux_mlkem1024_portable.h b/out/test-libcrux/internal/libcrux_mlkem1024_portable.h index bb6a0d8b..8f8bd29d 100644 --- a/out/test-libcrux/internal/libcrux_mlkem1024_portable.h +++ b/out/test-libcrux/internal/libcrux_mlkem1024_portable.h @@ -8,7 +8,7 @@ #ifndef internal_libcrux_mlkem1024_portable_H #define internal_libcrux_mlkem1024_portable_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux/internal/libcrux_mlkem512_avx2.h b/out/test-libcrux/internal/libcrux_mlkem512_avx2.h index c09d12cf..d05d438b 100644 --- a/out/test-libcrux/internal/libcrux_mlkem512_avx2.h +++ b/out/test-libcrux/internal/libcrux_mlkem512_avx2.h @@ -8,7 +8,7 @@ #ifndef internal_libcrux_mlkem512_avx2_H #define internal_libcrux_mlkem512_avx2_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux/internal/libcrux_mlkem512_portable.h b/out/test-libcrux/internal/libcrux_mlkem512_portable.h index 2f001a69..4015021a 100644 --- a/out/test-libcrux/internal/libcrux_mlkem512_portable.h +++ b/out/test-libcrux/internal/libcrux_mlkem512_portable.h @@ -8,7 +8,7 @@ #ifndef internal_libcrux_mlkem512_portable_H #define internal_libcrux_mlkem512_portable_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux/internal/libcrux_mlkem768_avx2.h b/out/test-libcrux/internal/libcrux_mlkem768_avx2.h index 9be84f26..e02c3b3a 100644 --- a/out/test-libcrux/internal/libcrux_mlkem768_avx2.h +++ b/out/test-libcrux/internal/libcrux_mlkem768_avx2.h @@ -8,7 +8,7 @@ #ifndef internal_libcrux_mlkem768_avx2_H #define internal_libcrux_mlkem768_avx2_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux/internal/libcrux_mlkem768_portable.h b/out/test-libcrux/internal/libcrux_mlkem768_portable.h index 91e648ab..ad9781ef 100644 --- a/out/test-libcrux/internal/libcrux_mlkem768_portable.h +++ b/out/test-libcrux/internal/libcrux_mlkem768_portable.h @@ -8,7 +8,7 @@ #ifndef internal_libcrux_mlkem768_portable_H #define internal_libcrux_mlkem768_portable_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux/internal/libcrux_mlkem_avx2.h b/out/test-libcrux/internal/libcrux_mlkem_avx2.h index 692e06d6..13e96093 100644 --- a/out/test-libcrux/internal/libcrux_mlkem_avx2.h +++ b/out/test-libcrux/internal/libcrux_mlkem_avx2.h @@ -8,7 +8,7 @@ #ifndef internal_libcrux_mlkem_avx2_H #define internal_libcrux_mlkem_avx2_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux/internal/libcrux_mlkem_portable.h b/out/test-libcrux/internal/libcrux_mlkem_portable.h index a5c347ca..f4425268 100644 --- a/out/test-libcrux/internal/libcrux_mlkem_portable.h +++ b/out/test-libcrux/internal/libcrux_mlkem_portable.h @@ -8,7 +8,7 @@ #ifndef internal_libcrux_mlkem_portable_H #define internal_libcrux_mlkem_portable_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux/libcrux_core.h b/out/test-libcrux/libcrux_core.h index 1db5ba32..d06a3a54 100644 --- a/out/test-libcrux/libcrux_core.h +++ b/out/test-libcrux/libcrux_core.h @@ -8,7 +8,7 @@ #ifndef libcrux_core_H #define libcrux_core_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux/libcrux_mlkem1024.h b/out/test-libcrux/libcrux_mlkem1024.h index 1725ecf6..03574413 100644 --- a/out/test-libcrux/libcrux_mlkem1024.h +++ b/out/test-libcrux/libcrux_mlkem1024.h @@ -8,7 +8,7 @@ #ifndef libcrux_mlkem1024_H #define libcrux_mlkem1024_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux/libcrux_mlkem1024_avx2.h b/out/test-libcrux/libcrux_mlkem1024_avx2.h index 3979f258..0056873b 100644 --- a/out/test-libcrux/libcrux_mlkem1024_avx2.h +++ b/out/test-libcrux/libcrux_mlkem1024_avx2.h @@ -8,7 +8,7 @@ #ifndef libcrux_mlkem1024_avx2_H #define libcrux_mlkem1024_avx2_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux/libcrux_mlkem1024_portable.h b/out/test-libcrux/libcrux_mlkem1024_portable.h index f7a28b7e..d51ba272 100644 --- a/out/test-libcrux/libcrux_mlkem1024_portable.h +++ b/out/test-libcrux/libcrux_mlkem1024_portable.h @@ -8,7 +8,7 @@ #ifndef libcrux_mlkem1024_portable_H #define libcrux_mlkem1024_portable_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux/libcrux_mlkem512.h b/out/test-libcrux/libcrux_mlkem512.h index f92f40a4..467d1dc8 100644 --- a/out/test-libcrux/libcrux_mlkem512.h +++ b/out/test-libcrux/libcrux_mlkem512.h @@ -8,7 +8,7 @@ #ifndef libcrux_mlkem512_H #define libcrux_mlkem512_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux/libcrux_mlkem512_avx2.h b/out/test-libcrux/libcrux_mlkem512_avx2.h index 4e7ab7c4..cfa1cae8 100644 --- a/out/test-libcrux/libcrux_mlkem512_avx2.h +++ b/out/test-libcrux/libcrux_mlkem512_avx2.h @@ -8,7 +8,7 @@ #ifndef libcrux_mlkem512_avx2_H #define libcrux_mlkem512_avx2_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux/libcrux_mlkem512_portable.h b/out/test-libcrux/libcrux_mlkem512_portable.h index b96f9772..3f1955b8 100644 --- a/out/test-libcrux/libcrux_mlkem512_portable.h +++ b/out/test-libcrux/libcrux_mlkem512_portable.h @@ -8,7 +8,7 @@ #ifndef libcrux_mlkem512_portable_H #define libcrux_mlkem512_portable_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux/libcrux_mlkem768.h b/out/test-libcrux/libcrux_mlkem768.h index a6490afd..f5441d3e 100644 --- a/out/test-libcrux/libcrux_mlkem768.h +++ b/out/test-libcrux/libcrux_mlkem768.h @@ -8,7 +8,7 @@ #ifndef libcrux_mlkem768_H #define libcrux_mlkem768_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux/libcrux_mlkem768_avx2.h b/out/test-libcrux/libcrux_mlkem768_avx2.h index 7d9af467..eda0b4bf 100644 --- a/out/test-libcrux/libcrux_mlkem768_avx2.h +++ b/out/test-libcrux/libcrux_mlkem768_avx2.h @@ -8,7 +8,7 @@ #ifndef libcrux_mlkem768_avx2_H #define libcrux_mlkem768_avx2_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux/libcrux_mlkem768_portable.h b/out/test-libcrux/libcrux_mlkem768_portable.h index 0a44b7d2..58bd3dc6 100644 --- a/out/test-libcrux/libcrux_mlkem768_portable.h +++ b/out/test-libcrux/libcrux_mlkem768_portable.h @@ -8,7 +8,7 @@ #ifndef libcrux_mlkem768_portable_H #define libcrux_mlkem768_portable_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux/libcrux_mlkem_avx2.h b/out/test-libcrux/libcrux_mlkem_avx2.h index 21bb0e9e..5ca0fb3a 100644 --- a/out/test-libcrux/libcrux_mlkem_avx2.h +++ b/out/test-libcrux/libcrux_mlkem_avx2.h @@ -8,7 +8,7 @@ #ifndef libcrux_mlkem_avx2_H #define libcrux_mlkem_avx2_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux/libcrux_mlkem_portable.h b/out/test-libcrux/libcrux_mlkem_portable.h index a26297ee..e85e7212 100644 --- a/out/test-libcrux/libcrux_mlkem_portable.h +++ b/out/test-libcrux/libcrux_mlkem_portable.h @@ -8,7 +8,7 @@ #ifndef libcrux_mlkem_portable_H #define libcrux_mlkem_portable_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux/libcrux_sha3_avx2.h b/out/test-libcrux/libcrux_sha3_avx2.h index da662942..6a78282e 100644 --- a/out/test-libcrux/libcrux_sha3_avx2.h +++ b/out/test-libcrux/libcrux_sha3_avx2.h @@ -8,7 +8,7 @@ #ifndef libcrux_sha3_avx2_H #define libcrux_sha3_avx2_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-libcrux/libcrux_sha3_portable.h b/out/test-libcrux/libcrux_sha3_portable.h index 7db9e271..97cea664 100644 --- a/out/test-libcrux/libcrux_sha3_portable.h +++ b/out/test-libcrux/libcrux_sha3_portable.h @@ -8,7 +8,7 @@ #ifndef libcrux_sha3_portable_H #define libcrux_sha3_portable_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-lvalue/lvalue.h b/out/test-lvalue/lvalue.h index adc35b2a..ff32d4d3 100644 --- a/out/test-lvalue/lvalue.h +++ b/out/test-lvalue/lvalue.h @@ -8,7 +8,7 @@ #ifndef lvalue_H #define lvalue_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-mismatch/mismatch.h b/out/test-mismatch/mismatch.h index 02215194..2772f492 100644 --- a/out/test-mismatch/mismatch.h +++ b/out/test-mismatch/mismatch.h @@ -8,7 +8,7 @@ #ifndef mismatch_H #define mismatch_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-more_dst/more_dst.h b/out/test-more_dst/more_dst.h index 0025c309..15500dbb 100644 --- a/out/test-more_dst/more_dst.h +++ b/out/test-more_dst/more_dst.h @@ -8,7 +8,7 @@ #ifndef more_dst_H #define more_dst_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-more_primitive_types/more_primitive_types.h b/out/test-more_primitive_types/more_primitive_types.h index e8184073..0179b889 100644 --- a/out/test-more_primitive_types/more_primitive_types.h +++ b/out/test-more_primitive_types/more_primitive_types.h @@ -8,7 +8,7 @@ #ifndef more_primitive_types_H #define more_primitive_types_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-more_str/more_str.h b/out/test-more_str/more_str.h index 41c24507..0bf2e774 100644 --- a/out/test-more_str/more_str.h +++ b/out/test-more_str/more_str.h @@ -8,7 +8,7 @@ #ifndef more_str_H #define more_str_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-names/names.h b/out/test-names/names.h index be6871a2..fd257c78 100644 --- a/out/test-names/names.h +++ b/out/test-names/names.h @@ -8,7 +8,7 @@ #ifndef names_H #define names_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-nested_arrays/nested_arrays.h b/out/test-nested_arrays/nested_arrays.h index 5532aa4a..723af115 100644 --- a/out/test-nested_arrays/nested_arrays.h +++ b/out/test-nested_arrays/nested_arrays.h @@ -8,7 +8,7 @@ #ifndef nested_arrays_H #define nested_arrays_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-nested_arrays2/nested_arrays2.h b/out/test-nested_arrays2/nested_arrays2.h index 6b24f02b..c6ff17e9 100644 --- a/out/test-nested_arrays2/nested_arrays2.h +++ b/out/test-nested_arrays2/nested_arrays2.h @@ -8,7 +8,7 @@ #ifndef nested_arrays2_H #define nested_arrays2_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-option/option.h b/out/test-option/option.h index 3e0ac9d9..29e396db 100644 --- a/out/test-option/option.h +++ b/out/test-option/option.h @@ -8,7 +8,7 @@ #ifndef option_H #define option_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-parentparent/parentparent.h b/out/test-parentparent/parentparent.h index 7c3b10c0..e4ca5589 100644 --- a/out/test-parentparent/parentparent.h +++ b/out/test-parentparent/parentparent.h @@ -8,7 +8,7 @@ #ifndef parentparent_H #define parentparent_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-partial_eq/partial_eq.h b/out/test-partial_eq/partial_eq.h index f61a6f88..086a38d3 100644 --- a/out/test-partial_eq/partial_eq.h +++ b/out/test-partial_eq/partial_eq.h @@ -8,7 +8,7 @@ #ifndef partial_eq_H #define partial_eq_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-raw_pointers/raw_pointers.h b/out/test-raw_pointers/raw_pointers.h index c15e7ea3..eb20c492 100644 --- a/out/test-raw_pointers/raw_pointers.h +++ b/out/test-raw_pointers/raw_pointers.h @@ -8,7 +8,7 @@ #ifndef raw_pointers_H #define raw_pointers_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-reborrow/reborrow.h b/out/test-reborrow/reborrow.h index 60d6dd9c..e238ce99 100644 --- a/out/test-reborrow/reborrow.h +++ b/out/test-reborrow/reborrow.h @@ -8,7 +8,7 @@ #ifndef reborrow_H #define reborrow_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-recursion/recursion.h b/out/test-recursion/recursion.h index 4c25fa33..4aaabc3f 100644 --- a/out/test-recursion/recursion.h +++ b/out/test-recursion/recursion.h @@ -8,7 +8,7 @@ #ifndef recursion_H #define recursion_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-repeat/repeat.h b/out/test-repeat/repeat.h index b951b9b3..ddb1352e 100644 --- a/out/test-repeat/repeat.h +++ b/out/test-repeat/repeat.h @@ -8,7 +8,7 @@ #ifndef repeat_H #define repeat_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-result/result.h b/out/test-result/result.h index 476058ff..71cd043a 100644 --- a/out/test-result/result.h +++ b/out/test-result/result.h @@ -8,7 +8,7 @@ #ifndef result_H #define result_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-slice_array/slice_array.h b/out/test-slice_array/slice_array.h index b1dac341..b1d93a67 100644 --- a/out/test-slice_array/slice_array.h +++ b/out/test-slice_array/slice_array.h @@ -8,7 +8,7 @@ #ifndef slice_array_H #define slice_array_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-step_by/step_by.h b/out/test-step_by/step_by.h index c7276ee7..89149833 100644 --- a/out/test-step_by/step_by.h +++ b/out/test-step_by/step_by.h @@ -8,7 +8,7 @@ #ifndef step_by_H #define step_by_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-substr/substr.h b/out/test-substr/substr.h index 9ab5a7b6..0b3da1fe 100644 --- a/out/test-substr/substr.h +++ b/out/test-substr/substr.h @@ -8,7 +8,7 @@ #ifndef substr_H #define substr_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-symcrust/internal/Eurydice.h b/out/test-symcrust/internal/Eurydice.h index 35d046de..104317ed 100644 --- a/out/test-symcrust/internal/Eurydice.h +++ b/out/test-symcrust/internal/Eurydice.h @@ -8,7 +8,7 @@ #ifndef internal_Eurydice_H #define internal_Eurydice_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-symcrust/symcrust.h b/out/test-symcrust/symcrust.h index d262924d..fd50dea7 100644 --- a/out/test-symcrust/symcrust.h +++ b/out/test-symcrust/symcrust.h @@ -8,7 +8,7 @@ #ifndef symcrust_H #define symcrust_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-trait_generics/trait_generics.h b/out/test-trait_generics/trait_generics.h index ef4b5b53..be512f47 100644 --- a/out/test-trait_generics/trait_generics.h +++ b/out/test-trait_generics/trait_generics.h @@ -8,7 +8,7 @@ #ifndef trait_generics_H #define trait_generics_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-traits/traits.h b/out/test-traits/traits.h index a6ca2ab1..69a85a69 100644 --- a/out/test-traits/traits.h +++ b/out/test-traits/traits.h @@ -8,7 +8,7 @@ #ifndef traits_H #define traits_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-traits2/traits2.h b/out/test-traits2/traits2.h index 487cd10e..e805ebee 100644 --- a/out/test-traits2/traits2.h +++ b/out/test-traits2/traits2.h @@ -8,7 +8,7 @@ #ifndef traits2_H #define traits2_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-traits3/traits3.h b/out/test-traits3/traits3.h index 1ab47318..da6a4bd6 100644 --- a/out/test-traits3/traits3.h +++ b/out/test-traits3/traits3.h @@ -8,7 +8,7 @@ #ifndef traits3_H #define traits3_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-we_need_charon_monomorphization/we_need_charon_monomorphization.h b/out/test-we_need_charon_monomorphization/we_need_charon_monomorphization.h index 12e3a354..e70e5b2e 100644 --- a/out/test-we_need_charon_monomorphization/we_need_charon_monomorphization.h +++ b/out/test-we_need_charon_monomorphization/we_need_charon_monomorphization.h @@ -8,7 +8,7 @@ #ifndef we_need_charon_monomorphization_H #define we_need_charon_monomorphization_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-where_clauses_closures/where_clauses_closures.h b/out/test-where_clauses_closures/where_clauses_closures.h index 420cf98c..fb97a7c5 100644 --- a/out/test-where_clauses_closures/where_clauses_closures.h +++ b/out/test-where_clauses_closures/where_clauses_closures.h @@ -8,7 +8,7 @@ #ifndef where_clauses_closures_H #define where_clauses_closures_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-where_clauses_fncg/where_clauses_fncg.h b/out/test-where_clauses_fncg/where_clauses_fncg.h index 984f9ca8..aafe0866 100644 --- a/out/test-where_clauses_fncg/where_clauses_fncg.h +++ b/out/test-where_clauses_fncg/where_clauses_fncg.h @@ -8,7 +8,7 @@ #ifndef where_clauses_fncg_H #define where_clauses_fncg_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/test-where_clauses_simple/where_clauses_simple.h b/out/test-where_clauses_simple/where_clauses_simple.h index 715bd094..3a0b4826 100644 --- a/out/test-where_clauses_simple/where_clauses_simple.h +++ b/out/test-where_clauses_simple/where_clauses_simple.h @@ -8,7 +8,7 @@ #ifndef where_clauses_simple_H #define where_clauses_simple_H -#include "eurydice_glue.h" +#include "eurydice.h" #if defined(__cplusplus) diff --git a/out/testxx-result/result.h b/out/testxx-result/result.h index 9bada21c..6c9ae789 100644 --- a/out/testxx-result/result.h +++ b/out/testxx-result/result.h @@ -8,7 +8,7 @@ #ifndef result_H #define result_H -#include "eurydice_glue.h" +#include "eurydice.h" diff --git a/scripts/format.sh b/scripts/format.sh index 0158f4d1..57a3d96f 100755 --- a/scripts/format.sh +++ b/scripts/format.sh @@ -10,7 +10,7 @@ if [ $# -ne 1 ]; then usage fi -format_file="${FORMAT_FILE:-include/eurydice_glue.h}" +format_file="${FORMAT_FILE:-include/eurydice.h}" case "$1" in check) diff --git a/test/core_cmp_lib.c b/test/core_cmp_lib.c index 8c1e9ad2..a2678955 100644 --- a/test/core_cmp_lib.c +++ b/test/core_cmp_lib.c @@ -1,6 +1,6 @@ // this file provides the comparison implementations for various built-in types -#include "eurydice_glue.h" +#include "eurydice.h" // the implementation for `()` comparison -- the inputs are `&()` // as the function interface is `&self` diff --git a/test/main.c b/test/main.c index b0a7678f..4ae720f4 100644 --- a/test/main.c +++ b/test/main.c @@ -1,5 +1,5 @@ #include "__NAME__.h" -#include "eurydice_glue.h" +#include "eurydice.h" int main() { __NAME___main(); From 5ca42bdb4309a18e332321ca9ae66607824428eb Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Wed, 26 Nov 2025 08:00:31 -0800 Subject: [PATCH 4/4] Missing files were not caught because of bad gitignore --- .gitignore | 2 +- include/eurydice.h | 11 ++ include/eurydice/base.h | 45 +++++++ include/eurydice/core.h | 215 ++++++++++++++++++++++++++++++++++ include/eurydice/cpp_compat.h | 32 +++++ include/eurydice/fmt.h | 9 ++ include/eurydice/iterator.h | 16 +++ include/eurydice/slice.h | 102 ++++++++++++++++ include/eurydice/str.h | 7 ++ include/eurydice/unsafe.h | 10 ++ include/eurydice/vec_box.h | 101 ++++++++++++++++ 11 files changed, 549 insertions(+), 1 deletion(-) create mode 100644 include/eurydice.h create mode 100644 include/eurydice/base.h create mode 100644 include/eurydice/core.h create mode 100644 include/eurydice/cpp_compat.h create mode 100644 include/eurydice/fmt.h create mode 100644 include/eurydice/iterator.h create mode 100644 include/eurydice/slice.h create mode 100644 include/eurydice/str.h create mode 100644 include/eurydice/unsafe.h create mode 100644 include/eurydice/vec_box.h diff --git a/.gitignore b/.gitignore index cce59f33..feb99120 100644 --- a/.gitignore +++ b/.gitignore @@ -8,7 +8,7 @@ out/*/a.out *.DS_Store *.orig *.llbc -eurydice +./eurydice /.vscode .charon_version diff --git a/include/eurydice.h b/include/eurydice.h new file mode 100644 index 00000000..55b5c3d3 --- /dev/null +++ b/include/eurydice.h @@ -0,0 +1,11 @@ +#pragma once + +#include "eurydice/base.h" +#include "eurydice/core.h" +#include "eurydice/cpp_compat.h" +#include "eurydice/fmt.h" +#include "eurydice/iterator.h" +#include "eurydice/slice.h" +#include "eurydice/str.h" +#include "eurydice/unsafe.h" +#include "eurydice/vec_box.h" diff --git a/include/eurydice/base.h b/include/eurydice/base.h new file mode 100644 index 00000000..d0554268 --- /dev/null +++ b/include/eurydice/base.h @@ -0,0 +1,45 @@ +#pragma once + +// Base macros emitted by the code-gen -- this file should always be included, +// unless you want to reimplement some stuff by hand. + +// Eurydice emits type `bool` +#include +// Eurydice may emit the KRML_FOR_* series of macros +#include + +#include + +// GENERAL-PURPOSE STUFF + +#define LowStar_Ignore_ignore(e, t, _ret_t) ((void)e) + +#define EURYDICE_ASSERT(test, msg) \ + do { \ + if (!(test)) { \ + fprintf(stderr, "assertion \"%s\" failed: file \"%s\", line %d\n", msg, \ + __FILE__, __LINE__); \ + exit(255); \ + } \ + } while (0) + +// SIZEOF, ALIGNOF + +#define Eurydice_sizeof(t) sizeof(t) + +#define Eurydice_alignof(t) alignof(t) + +// MACROS EXPECTED BY CODE-GEN + +#if defined(__cplusplus) +#define KRML_CLITERAL(type) type +#else +#define KRML_CLITERAL(type) (type) +#endif + +#if defined(__cplusplus) && defined(__cpp_designated_initializers) || \ + !(defined(__cplusplus)) +#define EURYDICE_CFIELD(X) X +#else +#define EURYDICE_CFIELD(X) +#endif diff --git a/include/eurydice/core.h b/include/eurydice/core.h new file mode 100644 index 00000000..3e99bf8d --- /dev/null +++ b/include/eurydice/core.h @@ -0,0 +1,215 @@ +#pragma once + +#include +#include +#include + +#include "krml/lowstar_endianness.h" + +#ifdef _MSC_VER +// For __popcnt +#include +#endif + +// CORE STUFF (conversions, endianness, ...) + +// We slap extern "C" on declarations that intend to implement a prototype +// generated by Eurydice, because Eurydice prototypes are always emitted within +// an extern "C" block, UNLESS you use -fcxx17-compat, in which case, you must +// pass -DKRML_CXX17_COMPAT="" to your C++ compiler. +#if defined(__cplusplus) && !defined(KRML_CXX17_COMPAT) +extern "C" { +#endif + +#define core_hint_black_box(X, _0, _1) (X) + +// FIXME: add dedicated extraction to extract NonNull as T* +#define core_ptr_non_null_NonNull void * + +// [ u8; 2 ] +typedef struct Eurydice_array_u8x2_s { + uint8_t data[2]; +} Eurydice_array_u8x2; + +// [ u8; 4 ] +typedef struct Eurydice_array_u8x4_s { + uint8_t data[4]; +} Eurydice_array_u8x4; + +// [ u8; 8 ] +typedef struct Eurydice_array_u8x8_s { + uint8_t data[8]; +} Eurydice_array_u8x8; + +static inline uint16_t core_num__u16__from_le_bytes(Eurydice_array_u8x2 buf) { + return load16_le(buf.data); +} + +static inline Eurydice_array_u8x4 core_num__u32__to_be_bytes(uint32_t src) { + // TODO: why not store32_be? + Eurydice_array_u8x4 a; + uint32_t x = htobe32(src); + memcpy(a.data, &x, 4); + return a; +} + +static inline Eurydice_array_u8x4 core_num__u32__to_le_bytes(uint32_t src) { + Eurydice_array_u8x4 a; + store32_le(a.data, src); + return a; +} + +static inline uint32_t core_num__u32__from_le_bytes(Eurydice_array_u8x4 buf) { + return load32_le(buf.data); +} + +static inline Eurydice_array_u8x8 core_num__u64__to_le_bytes(uint64_t v) { + Eurydice_array_u8x8 a; + store64_le(a.data, v); + return a; +} + +static inline uint64_t core_num__u64__from_le_bytes(Eurydice_array_u8x8 buf) { + return load64_le(buf.data); +} + +static inline int64_t +core_convert_num__core__convert__From_i32__for_i64__from(int32_t x) { + return x; +} + +static inline uint64_t +core_convert_num__core__convert__From_u8__for_u64__from(uint8_t x) { + return x; +} + +static inline uint64_t +core_convert_num__core__convert__From_u16__for_u64__from(uint16_t x) { + return x; +} + +static inline size_t +core_convert_num__core__convert__From_u16__for_usize__from(uint16_t x) { + return x; +} + +static inline uint32_t core_num__u8__count_ones(uint8_t x0) { +#ifdef _MSC_VER + return __popcnt(x0); +#else + return __builtin_popcount(x0); +#endif +} + +static inline uint32_t core_num__u32__count_ones(uint32_t x0) { +#ifdef _MSC_VER + return __popcnt(x0); +#else + return __builtin_popcount(x0); +#endif +} + +static inline uint32_t core_num__i32__count_ones(int32_t x0) { +#ifdef _MSC_VER + return __popcnt(x0); +#else + return __builtin_popcount(x0); +#endif +} + +static inline size_t core_cmp_impls__core__cmp__Ord_for_usize__min(size_t a, + size_t b) { + if (a <= b) + return a; + else + return b; +} + +// unsigned overflow wraparound semantics in C +static inline uint8_t core_num__u8__wrapping_sub(uint8_t x, uint8_t y) { + return x - y; +} +static inline uint8_t core_num__u8__wrapping_add(uint8_t x, uint8_t y) { + return x + y; +} +static inline uint8_t core_num__u8__wrapping_mul(uint8_t x, uint8_t y) { + return x * y; +} +static inline uint16_t core_num__u16__wrapping_sub(uint16_t x, uint16_t y) { + return x - y; +} +static inline uint16_t core_num__u16__wrapping_add(uint16_t x, uint16_t y) { + return x + y; +} +static inline uint16_t core_num__u16__wrapping_mul(uint16_t x, uint16_t y) { + return x * y; +} +static inline uint32_t core_num__u32__wrapping_sub(uint32_t x, uint32_t y) { + return x - y; +} +static inline uint32_t core_num__u32__wrapping_add(uint32_t x, uint32_t y) { + return x + y; +} +static inline uint32_t core_num__u32__wrapping_mul(uint32_t x, uint32_t y) { + return x * y; +} +static inline uint64_t core_num__u64__wrapping_sub(uint64_t x, uint64_t y) { + return x - y; +} +static inline uint64_t core_num__u64__wrapping_add(uint64_t x, uint64_t y) { + return x + y; +} +static inline uint64_t core_num__u64__wrapping_mul(uint64_t x, uint64_t y) { + return x * y; +} +static inline size_t core_num__usize__wrapping_sub(size_t x, size_t y) { + return x - y; +} +static inline size_t core_num__usize__wrapping_add(size_t x, size_t y) { + return x + y; +} +static inline size_t core_num__usize__wrapping_mul(size_t x, size_t y) { + return x * y; +} + +static inline uint64_t core_num__u64__rotate_left(uint64_t x0, uint32_t x1) { + return (x0 << x1) | (x0 >> ((-x1) & 63)); +} + +static inline void core_ops_arith__i32__add_assign(int32_t *x0, int32_t *x1) { + *x0 = *x0 + *x1; +} + +static inline uint8_t Eurydice_bitand_pv_u8(uint8_t *p, uint8_t v) { + return (*p) & v; +} +static inline uint8_t Eurydice_shr_pv_u8(uint8_t *p, int32_t v) { + return (*p) >> v; +} +static inline uint32_t Eurydice_min_u32(uint32_t x, uint32_t y) { + return x < y ? x : y; +} + +static inline uint8_t +core_ops_bit__core__ops__bit__BitAnd_u8__u8__for___a__u8___bitand(uint8_t *x0, + uint8_t x1) { + return Eurydice_bitand_pv_u8(x0, x1); +} + +static inline uint8_t +core_ops_bit__core__ops__bit__Shr_i32__u8__for___a__u8___shr(uint8_t *x0, + int32_t x1) { + return Eurydice_shr_pv_u8(x0, x1); +} + +#define core_num_nonzero_private_NonZeroUsizeInner size_t +static inline core_num_nonzero_private_NonZeroUsizeInner +core_num_nonzero_private___core__clone__Clone_for_core__num__nonzero__private__NonZeroUsizeInner___clone( + core_num_nonzero_private_NonZeroUsizeInner *x0) { + return *x0; +} + +#if defined(__cplusplus) && !defined(KRML_CXX17_COMPAT) +} +#endif + diff --git a/include/eurydice/cpp_compat.h b/include/eurydice/cpp_compat.h new file mode 100644 index 00000000..b64438ba --- /dev/null +++ b/include/eurydice/cpp_compat.h @@ -0,0 +1,32 @@ +#pragma once + +// Compatibility helpers for C++. This header can be safely omitted if you don't +// intend on generating code that ought to work with C++17 via the +// -fcxx17-compat flag. + +#if defined(__cplusplus) + +#ifndef KRML_HOST_EPRINTF +#define KRML_HOST_EPRINTF(...) fprintf(stderr, __VA_ARGS__) +#endif + +#include + +#ifndef __cpp_lib_type_identity +template struct type_identity { + using type = T; +}; + +template using type_identity_t = typename type_identity::type; +#else +using std::type_identity_t; +#endif + +#define KRML_UNION_CONSTRUCTOR(T) \ + template \ + constexpr T(int t, V U::*m, type_identity_t v) : tag(t) { \ + val.*m = std::move(v); \ + } \ + T() = default; + +#endif diff --git a/include/eurydice/fmt.h b/include/eurydice/fmt.h new file mode 100644 index 00000000..745377bf --- /dev/null +++ b/include/eurydice/fmt.h @@ -0,0 +1,9 @@ +#pragma once + +// PRINTING +// +// FIXME: this is temporary. Ultimately we want to be able to extract all of this. + +typedef void *core_fmt_Formatter; +#define core_fmt_rt__core__fmt__rt__Argument__a___new_display(x1, x2, x3, x4) \ + NULL diff --git a/include/eurydice/iterator.h b/include/eurydice/iterator.h new file mode 100644 index 00000000..183a25ff --- /dev/null +++ b/include/eurydice/iterator.h @@ -0,0 +1,16 @@ +#pragma once + +// ITERATORS + +// FIXME: these definitions should eventually be extracted instead of being hand +// written + +#define Eurydice_range_iter_next(iter_ptr, t, ret_t) \ + (((iter_ptr)->start >= (iter_ptr)->end) \ + ? (KRML_CLITERAL(ret_t){EURYDICE_CFIELD(.tag =) 0, \ + EURYDICE_CFIELD(.f0 =) 0}) \ + : (KRML_CLITERAL(ret_t){EURYDICE_CFIELD(.tag =) 1, \ + EURYDICE_CFIELD(.f0 =)(iter_ptr)->start++})) + +#define core_iter_range__core__iter__traits__iterator__Iterator_A__for_core__ops__range__Range_A__TraitClause_0___next \ + Eurydice_range_iter_next diff --git a/include/eurydice/slice.h b/include/eurydice/slice.h new file mode 100644 index 00000000..fa4e139a --- /dev/null +++ b/include/eurydice/slice.h @@ -0,0 +1,102 @@ +#pragma once + +#include +#include + +// SLICES, ARRAYS, ETC. + +// For convenience, we give these common slice types, below, a distinguished +// status and rather than emit them in the client code, we skip their +// code-generation in Cleanup3.ml and write them by hand here. This makes it +// easy to write interop code that brings those definitions in scope. + +// &[u8] +typedef struct Eurydice_borrow_slice_u8_s { + const uint8_t *ptr; + size_t meta; +} Eurydice_borrow_slice_u8; + +// &[u16] +typedef struct Eurydice_borrow_slice_i16_s { + const int16_t *ptr; + size_t meta; +} Eurydice_borrow_slice_i16; + +// &mut [u8] +typedef struct Eurydice_mut_borrow_slice_u8_s { + uint8_t *ptr; + size_t meta; +} Eurydice_mut_borrow_slice_u8; + +// &mut [u16] +typedef struct Eurydice_mut_borrow_slice_i16_s { + int16_t *ptr; + size_t meta; +} Eurydice_mut_borrow_slice_i16; + +// Copy a slice with memcopy +#define Eurydice_slice_copy(dst, src, t) \ + memcpy(dst.ptr, src.ptr, dst.meta * sizeof(t)) + +#define core_array___Array_T__N___as_slice(len_, ptr_, t, ret_t) \ + (KRML_CLITERAL(ret_t){EURYDICE_CFIELD(.ptr =)(ptr_)->data, \ + EURYDICE_CFIELD(.meta =) len_}) + +#define core_array__core__clone__Clone_for__Array_T__N___clone( \ + len, src, elem_type, _ret_t) \ + (*(src)) +#define TryFromSliceError uint8_t +#define core_array_TryFromSliceError uint8_t + +// Distinguished support for some PartialEq trait implementations +// +// core::cmp::PartialEq<@Array> for @Array +#define Eurydice_array_eq(sz, a1, a2, t) \ + (memcmp((a1)->data, (a2)->data, sz * sizeof(t)) == 0) +// core::cmp::PartialEq<&0 (@Slice)> for @Array +#define Eurydice_array_eq_slice_shared(sz, a1, s2, t, _) \ + (memcmp((a1)->data, (s2)->ptr, sz * sizeof(t)) == 0) +#define Eurydice_array_eq_slice_mut(sz, a1, s2, t, _) \ + Eurydice_array_eq_slice_shared(sz, a1, s2, t, _) + +// DEPRECATED -- should no longer be generated +#define core_array_equality__core__cmp__PartialEq__Array_U__N___for__Array_T__N___eq( \ + sz, a1, a2, t, _, _ret_t) \ + Eurydice_array_eq(sz, a1, a2, t) +#define core_array_equality__core__cmp__PartialEq__0___Slice_U____for__Array_T__N___eq( \ + sz, a1, a2, t, _, _ret_t) \ + Eurydice_array_eq(sz, a1, ((a2)->ptr), t) +#define core_cmp_impls__core__cmp__PartialEq__0_mut__B___for__1_mut__A___eq( \ + _m0, _m1, src1, src2, _0, _1, T) \ + Eurydice_slice_eq(src1, src2, _, _, T, _) + +#define Eurydice_slice_split_at(slice, mid, element_type, ret_t) \ + KRML_CLITERAL(ret_t) { \ + EURYDICE_CFIELD(.fst =){EURYDICE_CFIELD(.ptr =)((slice).ptr), \ + EURYDICE_CFIELD(.meta =) mid}, \ + EURYDICE_CFIELD(.snd =) { \ + EURYDICE_CFIELD(.ptr =) \ + ((slice).ptr + mid), EURYDICE_CFIELD(.meta =)((slice).meta - mid) \ + } \ + } + +#define Eurydice_slice_split_at_mut(slice, mid, element_type, ret_t) \ + KRML_CLITERAL(ret_t) { \ + EURYDICE_CFIELD(.fst =){EURYDICE_CFIELD(.ptr =)((slice).ptr), \ + EURYDICE_CFIELD(.meta =) mid}, \ + EURYDICE_CFIELD(.snd =) { \ + EURYDICE_CFIELD(.ptr =) \ + ((slice).ptr + mid), EURYDICE_CFIELD(.meta =)((slice).meta - mid) \ + } \ + } + +// Conversion of slice to an array, rewritten (by Eurydice) to name the +// destination array, since arrays are not values in C. +// N.B.: see note in karamel/lib/Inlining.ml if you change this. + +#define Eurydice_slice_to_ref_array2(len_, src, arr_ptr, t_ptr, t_arr, t_err, \ + t_res) \ + (src.meta >= len_ \ + ? ((t_res){.tag = core_result_Ok, .val = {.case_Ok = arr_ptr}}) \ + : ((t_res){.tag = core_result_Err, .val = {.case_Err = 0}})) + diff --git a/include/eurydice/str.h b/include/eurydice/str.h new file mode 100644 index 00000000..fdcdccbc --- /dev/null +++ b/include/eurydice/str.h @@ -0,0 +1,7 @@ +#pragma once + +// STRINGS + +typedef char Eurydice_c_char_t; +typedef const Eurydice_c_char_t *Prims_string; +typedef void Eurydice_c_void_t; diff --git a/include/eurydice/unsafe.h b/include/eurydice/unsafe.h new file mode 100644 index 00000000..13dc7c4f --- /dev/null +++ b/include/eurydice/unsafe.h @@ -0,0 +1,10 @@ +#pragma once + +// UNSAFE CODE + +#define core_slice___Slice_T___as_mut_ptr(x, t, _) (x.ptr) +#define core_mem_size_of(t, _) (sizeof(t)) +#define core_slice_raw_from_raw_parts_mut(ptr, len, _0, _1) \ + (KRML_CLITERAL(Eurydice_slice){(void *)(ptr), len}) +#define core_slice_raw_from_raw_parts(ptr, len, _0, _1) \ + (KRML_CLITERAL(Eurydice_slice){(void *)(ptr), len}) diff --git a/include/eurydice/vec_box.h b/include/eurydice/vec_box.h new file mode 100644 index 00000000..a9e95e0a --- /dev/null +++ b/include/eurydice/vec_box.h @@ -0,0 +1,101 @@ +#pragma once + +#include +#include + +// BOXES + +#ifndef EURYDICE_MALLOC +#define EURYDICE_MALLOC malloc +#endif + +#ifndef EURYDICE_REALLOC +#define EURYDICE_REALLOC realloc +#endif + +static inline char *malloc_and_init(size_t sz, char *init) { + char *ptr = (char *)EURYDICE_MALLOC(sz); + if (ptr != NULL) + memcpy(ptr, init, sz); + return ptr; +} + +#define Eurydice_box_new(init, t, t_dst) \ + ((t_dst)(malloc_and_init(sizeof(t), (char *)(&init)))) + +// Initializer for array of size zero +#define Eurydice_empty_array(dummy, t, t_dst) ((t_dst){.data = {}}) + +#define Eurydice_box_new_array(len, ptr, t, t_dst) \ + ((t_dst)(malloc_and_init(len * sizeof(t), (char *)(ptr)))) + +// FIXME this needs to handle allocation failure errors, but this seems hard to +// do without evaluating malloc_and_init twice... +#define alloc_boxed__alloc__boxed__Box_T___try_new(init, t, t_ret) \ + ((t_ret){.tag = core_result_Ok, \ + .f0 = (t *)malloc_and_init(sizeof(t), (char *)(&init))}) + +// VECTORS + +// We adapt the layout of https://doc.rust-lang.org/std/vec/struct.Vec.html, +// dispensing with the nested RawVec -- basically, we follow what the +// documentation says. Just like Eurydice_slice, we keep sizes in number of +// elements. This means we pass three words by value whenever we carry a vector +// around. Things that modify the vector take &mut's in Rust, or a Eurydice_vec* +// in C. +// +// Another design choice: just like Eurydice_slice, we treat Eurydice_vec as an +// opaque type, and rely on macros receiving their type arguments at call-site +// to perform necessary casts. A downside is that anything that looks into the +// definition of Eurydice_vec must be exposed (from the eurydice point of view) +// as an external -- see, for instance, Eurydice_vec_failed, below. +typedef struct { + char *ptr; + size_t len; /* current length, in elements */ + size_t capacity; /* the size of the allocation, in number of elements */ +} Eurydice_vec, alloc_vec_Vec; + +// This is a helper that Eurydice has special knowledge about. Essentially, +// allocation functions return a result type that has been monomorphized, say, +// Result_XY; this means we need to do something like: +// Eurydice_vec v = try_with_capacity(len, sz); +// Result_XY r = v.ptr == NULL ? (Result_XY) { .tag = core_result_Ok, .case_Ok +// = v } +// : (Result_XY) { .tag = core_result_Error, .case_Error = ... }; +// but with a macro (since we don't have templates). +// However, unless we allow statement-expressions (GCC extension), we cannot do +// the above with an expression, since we need to name the result of +// try_with_capacity to avoid evaluating it twice. +static inline Eurydice_vec Eurydice_vec_alloc2(size_t len, size_t element_sz) { + return ((Eurydice_vec){.ptr = (char *)EURYDICE_MALLOC(len * element_sz), + .len = len, + .capacity = len}); +} + +#define Eurydice_vec_alloc(len, t, _) (Eurydice_vec_alloc2((len), sizeof(t))) +#define Eurydice_vec_overflows(len, t, _) (!((len) <= SIZE_MAX / (sizeof(t)))) +#define Eurydice_vec_failed(v, _, _1) ((v).ptr == NULL) +#define Eurydice_layout(t, _) \ + ((core_alloc_layout_Layout){.size = sizeof(t), .align = _Alignof(t)}) + +#define alloc_vec__alloc__vec__Vec_T___resize( \ + /* Eurydice_vec * */ v, /* size_t */ new_len, /* T */ elt, T, _0, _1) \ + do { \ + if (new_len <= (v)->capacity) \ + (v)->len = new_len; \ + else { \ + (v)->ptr = EURYDICE_REALLOC((v)->ptr, new_len * sizeof(T)); \ + /* TODO: check success? Rust function is infallible */ \ + for (size_t i = (v)->len; i < new_len; i++) \ + ((T *)(v)->ptr)[i] = elt; \ + (v)->len = new_len; \ + (v)->capacity = new_len; \ + } \ + } while (0) + +#define alloc_vec__alloc__vec__Vec_T___into_boxed_slice(/* Eurydice_vec */ v, \ + T, _0, _1) \ + ((Eurydice_slice){.ptr = (v).ptr, .len = (v).len}) + +#define alloc_boxed__alloc__boxed__Box_T___from_raw(x, _0, _1) (x) +#define alloc_boxed__alloc__boxed__Box_T___into_raw(x, _0, _1) (x)