From 7754bcfe40be9a7879b1ff7a2848bb25b7ff1718 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 10 Jan 2025 14:54:48 +0100 Subject: [PATCH 1/3] Commit test output --- .gitignore | 2 +- Makefile | 5 + out/test-array/array.c | 112 ++++++++ out/test-array/array.h | 59 +++++ out/test-array2d/array2d.c | 54 ++++ out/test-array2d/array2d.h | 38 +++ out/test-const_generics/Eurydice.h | 36 +++ out/test-const_generics/const_generics.c | 216 +++++++++++++++ out/test-const_generics/const_generics.h | 125 +++++++++ .../inline_attributes.c | 31 +++ .../inline_attributes.h | 30 +++ out/test-int_switch/int_switch.c | 36 +++ out/test-int_switch/int_switch.h | 26 ++ out/test-issue_102/issue_102.c | 14 + out/test-issue_102/issue_102.h | 34 +++ out/test-issue_104/issue_104.c | 44 ++++ out/test-issue_104/issue_104.h | 42 +++ out/test-issue_106/issue_106.c | 31 +++ out/test-issue_106/issue_106.h | 32 +++ out/test-issue_107/issue_107.c | 22 ++ out/test-issue_107/issue_107.h | 29 +++ out/test-issue_123/issue_123.c | 59 +++++ out/test-issue_123/issue_123.h | 62 +++++ out/test-issue_96/issue_96.c | 36 +++ out/test-issue_96/issue_96.h | 37 +++ out/test-mismatch/mismatch.c | 14 + out/test-mismatch/mismatch.h | 24 ++ out/test-nested_arrays/Eurydice.h | 34 +++ out/test-nested_arrays/nested_arrays.c | 47 ++++ out/test-nested_arrays/nested_arrays.h | 163 ++++++++++++ out/test-nested_arrays2/nested_arrays2.c | 16 ++ out/test-nested_arrays2/nested_arrays2.h | 26 ++ out/test-partial_eq/partial_eq.c | 41 +++ out/test-partial_eq/partial_eq.h | 64 +++++ out/test-slice_array/slice_array.c | 62 +++++ out/test-slice_array/slice_array.h | 41 +++ out/test-symcrust/Eurydice.h | 34 +++ out/test-symcrust/internal/Eurydice.h | 25 ++ out/test-symcrust/symcrust.c | 71 +++++ out/test-symcrust/symcrust.h | 198 ++++++++++++++ out/test-traits/Eurydice.h | 34 +++ out/test-traits/traits.c | 47 ++++ out/test-traits/traits.h | 40 +++ .../where_clauses_closures.c | 73 ++++++ .../where_clauses_closures.h | 65 +++++ .../where_clauses_fncg.c | 55 ++++ .../where_clauses_fncg.h | 54 ++++ .../where_clauses_simple.c | 245 ++++++++++++++++++ .../where_clauses_simple.h | 170 ++++++++++++ 49 files changed, 2854 insertions(+), 1 deletion(-) create mode 100644 out/test-array/array.c create mode 100644 out/test-array/array.h create mode 100644 out/test-array2d/array2d.c create mode 100644 out/test-array2d/array2d.h create mode 100644 out/test-const_generics/Eurydice.h create mode 100644 out/test-const_generics/const_generics.c create mode 100644 out/test-const_generics/const_generics.h create mode 100644 out/test-inline_attributes/inline_attributes.c create mode 100644 out/test-inline_attributes/inline_attributes.h create mode 100644 out/test-int_switch/int_switch.c create mode 100644 out/test-int_switch/int_switch.h create mode 100644 out/test-issue_102/issue_102.c create mode 100644 out/test-issue_102/issue_102.h create mode 100644 out/test-issue_104/issue_104.c create mode 100644 out/test-issue_104/issue_104.h create mode 100644 out/test-issue_106/issue_106.c create mode 100644 out/test-issue_106/issue_106.h create mode 100644 out/test-issue_107/issue_107.c create mode 100644 out/test-issue_107/issue_107.h create mode 100644 out/test-issue_123/issue_123.c create mode 100644 out/test-issue_123/issue_123.h create mode 100644 out/test-issue_96/issue_96.c create mode 100644 out/test-issue_96/issue_96.h create mode 100644 out/test-mismatch/mismatch.c create mode 100644 out/test-mismatch/mismatch.h create mode 100644 out/test-nested_arrays/Eurydice.h create mode 100644 out/test-nested_arrays/nested_arrays.c create mode 100644 out/test-nested_arrays/nested_arrays.h create mode 100644 out/test-nested_arrays2/nested_arrays2.c create mode 100644 out/test-nested_arrays2/nested_arrays2.h create mode 100644 out/test-partial_eq/partial_eq.c create mode 100644 out/test-partial_eq/partial_eq.h create mode 100644 out/test-slice_array/slice_array.c create mode 100644 out/test-slice_array/slice_array.h create mode 100644 out/test-symcrust/Eurydice.h create mode 100644 out/test-symcrust/internal/Eurydice.h create mode 100644 out/test-symcrust/symcrust.c create mode 100644 out/test-symcrust/symcrust.h create mode 100644 out/test-traits/Eurydice.h create mode 100644 out/test-traits/traits.c create mode 100644 out/test-traits/traits.h create mode 100644 out/test-where_clauses_closures/where_clauses_closures.c create mode 100644 out/test-where_clauses_closures/where_clauses_closures.h create mode 100644 out/test-where_clauses_fncg/where_clauses_fncg.c create mode 100644 out/test-where_clauses_fncg/where_clauses_fncg.h create mode 100644 out/test-where_clauses_simple/where_clauses_simple.c create mode 100644 out/test-where_clauses_simple/where_clauses_simple.h diff --git a/.gitignore b/.gitignore index 12d4de8..65ce00c 100644 --- a/.gitignore +++ b/.gitignore @@ -1,8 +1,8 @@ _build lib/krml lib/charon -out test/*/target +out/*/a.out *.DS_Store *.orig *.llbc diff --git a/Makefile b/Makefile index b328895..9f01a5c 100644 --- a/Makefile +++ b/Makefile @@ -6,6 +6,9 @@ CHARON ?= $(CHARON_HOME)/bin/charon BROKEN_TESTS = step_by where_clauses chunks mutable_slice_range closure issue_49 issue_37 issue_105 TEST_DIRS = $(filter-out $(BROKEN_TESTS),$(subst test/,,$(shell find test -maxdepth 1 -mindepth 1 -type d))) +# Enable `foo/**` glob syntax +SHELL := bash -O globstar + .PHONY: all all: format-check @ocamlfind list | grep -q charon || test -L lib/charon || echo "⚠️⚠️⚠️ Charon not found; we suggest cd lib && ln -s path/to/charon charon" @@ -36,6 +39,8 @@ test-symcrust: CFLAGS += -Wno-unused-function test-%: test/%/out.llbc out/test-%/main.c | all $(EURYDICE) $(EXTRA) --output out/test-$* $< + sed -i 's/ KaRaMeL version: .*//' out/test-$*/**/*.{c,h} # This changes on every commit + sed -i 's/ KaRaMeL invocation: .*//' out/test-$*/**/*.{c,h} # This changes between local and CI cd out/test-$* && $(CC) $(CFLAGS) -I. -I../../include $(EXTRA_C) $*.c main.c && ./a.out custom-test-array: test-array diff --git a/out/test-array/array.c b/out/test-array/array.c new file mode 100644 index 0000000..60c02c0 --- /dev/null +++ b/out/test-array/array.c @@ -0,0 +1,112 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#include "array.h" + +array_Foo array_mk_foo(void) +{ + uint32_t x[2U] = { 0U }; + uint32_t y[2U] = { 1U, 1U }; + /* Passing arrays by value in Rust generates a copy in C */ + uint32_t copy_of_x[2U]; + memcpy(copy_of_x, x, (size_t)2U * sizeof (uint32_t)); + /* Passing arrays by value in Rust generates a copy in C */ + uint32_t copy_of_y[2U]; + memcpy(copy_of_y, y, (size_t)2U * sizeof (uint32_t)); + array_Foo lit; + memcpy(lit.x, copy_of_x, (size_t)2U * sizeof (uint32_t)); + memcpy(lit.y, copy_of_y, (size_t)2U * sizeof (uint32_t)); + return lit; +} + +array_Foo array_mk_foo2(void) +{ + return array_mk_foo(); +} + +void array_mut_array(uint32_t x[2U]) +{ + x[0U] = 1U; +} + +void array_mut_foo(array_Foo f) +{ + f.x[0U] = 1U; + uint32_t copy[2U]; + memcpy(copy, f.y, (size_t)2U * sizeof (uint32_t)); + copy[0U] = 0U; +} + +/** +A monomorphic instance of array.mk_incr.closure +with const generics +- K= 10 +*/ +uint32_t array_mk_incr_closure_95(size_t i) +{ + return (uint32_t)i; +} + +/** +A monomorphic instance of array.mk_incr +with const generics +- K= 10 +*/ +void array_mk_incr_95(uint32_t ret[10U]) +{ + KRML_MAYBE_FOR10(i, (size_t)0U, (size_t)10U, (size_t)1U, ret[i] = (uint32_t)i;); +} + +typedef struct _uint32_t__x2_s +{ + uint32_t *fst; + uint32_t *snd; +} +_uint32_t__x2; + +void array_main(void) +{ + /* XXX1 */ + array_Foo uu____0 = array_mk_foo2(); + uint32_t x[2U]; + memcpy(x, uu____0.x, (size_t)2U * sizeof (uint32_t)); + uint32_t y[2U]; + memcpy(y, uu____0.y, (size_t)2U * sizeof (uint32_t)); + uint32_t unsigned0 = 0U; + uint32_t uu____1[2U]; + memcpy(uu____1, x, (size_t)2U * sizeof (uint32_t)); + array_mut_array(uu____1); + /* Passing arrays by value in Rust generates a copy in C */ + uint32_t copy_of_x[2U]; + /* XXX2 */ + memcpy(copy_of_x, x, (size_t)2U * sizeof (uint32_t)); + /* Passing arrays by value in Rust generates a copy in C */ + uint32_t copy_of_y[2U]; + memcpy(copy_of_y, y, (size_t)2U * sizeof (uint32_t)); + array_Foo lit; + memcpy(lit.x, copy_of_x, (size_t)2U * sizeof (uint32_t)); + memcpy(lit.y, copy_of_y, (size_t)2U * sizeof (uint32_t)); + array_mut_foo(lit); + _uint32_t__x2 uu____4; + uu____4.fst = x; + uu____4.snd = &unsigned0; + /* XXX3 */ + uint32_t *left_val = uu____4.fst; + uint32_t *right_val0 = uu____4.snd; + EURYDICE_ASSERT(left_val[0U] == right_val0[0U], "panic!"); + uint32_t a[10U]; + array_mk_incr_95(a); + _uint32_t__x2 uu____5; + uu____5.fst = &a[9U]; + /* original Rust expression is not an lvalue in C */ + uint32_t lvalue = 9U; + uu____5.snd = &lvalue; + uint32_t *left_val0 = uu____5.fst; + uint32_t *right_val = uu____5.snd; + EURYDICE_ASSERT(left_val0[0U] == right_val[0U], "panic!"); +} + diff --git a/out/test-array/array.h b/out/test-array/array.h new file mode 100644 index 0000000..3e4a7ed --- /dev/null +++ b/out/test-array/array.h @@ -0,0 +1,59 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#ifndef __array_H +#define __array_H + +#if defined(__cplusplus) +extern "C" { +#endif + +#include "eurydice_glue.h" + +typedef struct array_Foo_s +{ + uint32_t x[2U]; + uint32_t y[2U]; +} +array_Foo; + +#define core_panicking_AssertKind_Eq 0 +#define core_panicking_AssertKind_Ne 1 +#define core_panicking_AssertKind_Match 2 + +typedef uint8_t core_panicking_AssertKind; + +array_Foo array_mk_foo(void); + +array_Foo array_mk_foo2(void); + +void array_mut_array(uint32_t x[2U]); + +void array_mut_foo(array_Foo f); + +/** +A monomorphic instance of array.mk_incr.closure +with const generics +- K= 10 +*/ +uint32_t array_mk_incr_closure_95(size_t i); + +/** +A monomorphic instance of array.mk_incr +with const generics +- K= 10 +*/ +void array_mk_incr_95(uint32_t ret[10U]); + +void array_main(void); + +#if defined(__cplusplus) +} +#endif + +#define __array_H_DEFINED +#endif diff --git a/out/test-array2d/array2d.c b/out/test-array2d/array2d.c new file mode 100644 index 0000000..2faa890 --- /dev/null +++ b/out/test-array2d/array2d.c @@ -0,0 +1,54 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#include "array2d.h" + +bool array2d_f(uint32_t x[4U][2U]) +{ + x[0U][0U] = 1U; + x[0U][1U] = 2U; + uint32_t y[4U][2U] = { { 1U, 2U }, { 3U, 4U }, { 1U, 2U }, { 3U, 4U } }; + return + core_array_equality___core__cmp__PartialEq__Array_U__N___for__Array_T__N____eq((size_t)4U, + x, + y, + uint32_t [2U], + uint32_t [2U], + bool); +} + +typedef struct _bool__x2_s +{ + bool *fst; + bool *snd; +} +_bool__x2; + +void array2d_main(void) +{ + uint32_t y[4U][2U]; + KRML_MAYBE_FOR4(i, + (size_t)0U, + (size_t)4U, + (size_t)1U, + y[i][0U] = 1U; + y[i][1U] = 2U;); + y[1U][0U] = 3U; + y[1U][1U] = 4U; + y[3U][0U] = 3U; + y[3U][1U] = 4U; + /* Passing arrays by value in Rust generates a copy in C */ + uint32_t copy_of_y[4U][2U]; + memcpy(copy_of_y, y, (size_t)4U * sizeof (uint32_t [2U])); + bool actual = array2d_f(copy_of_y); + bool expected = true; + _bool__x2 uu____1 = { .fst = &actual, .snd = &expected }; + bool *left_val = uu____1.fst; + bool *right_val = uu____1.snd; + EURYDICE_ASSERT(left_val[0U] == right_val[0U], "panic!"); +} + diff --git a/out/test-array2d/array2d.h b/out/test-array2d/array2d.h new file mode 100644 index 0000000..45677b2 --- /dev/null +++ b/out/test-array2d/array2d.h @@ -0,0 +1,38 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#ifndef __array2d_H +#define __array2d_H + +#if defined(__cplusplus) +extern "C" { +#endif + +#include "eurydice_glue.h" + +bool array2d_f(uint32_t x[4U][2U]); + +#define core_panicking_AssertKind_Eq 0 +#define core_panicking_AssertKind_Ne 1 +#define core_panicking_AssertKind_Match 2 + +typedef uint8_t core_panicking_AssertKind; + +void array2d_main(void); + +extern bool +core_cmp_impls___core__cmp__PartialEq_u32__for_u32__24__eq(uint32_t *x0, uint32_t *x1); + +extern bool +core_cmp_impls___core__cmp__PartialEq_u32__for_u32__24__ne(uint32_t *x0, uint32_t *x1); + +#if defined(__cplusplus) +} +#endif + +#define __array2d_H_DEFINED +#endif diff --git a/out/test-const_generics/Eurydice.h b/out/test-const_generics/Eurydice.h new file mode 100644 index 0000000..9eae3ff --- /dev/null +++ b/out/test-const_generics/Eurydice.h @@ -0,0 +1,36 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#ifndef __Eurydice_H +#define __Eurydice_H + +#if defined(__cplusplus) +extern "C" { +#endif + +#include "eurydice_glue.h" + +/** +A monomorphic instance of core.ops.range.RangeTo +with types size_t + +*/ +typedef size_t core_ops_range_RangeTo_08; + +/** +A monomorphic instance of core.ops.range.RangeFrom +with types size_t + +*/ +typedef size_t core_ops_range_RangeFrom_08; + +#if defined(__cplusplus) +} +#endif + +#define __Eurydice_H_DEFINED +#endif diff --git a/out/test-const_generics/const_generics.c b/out/test-const_generics/const_generics.c new file mode 100644 index 0000000..d3470cc --- /dev/null +++ b/out/test-const_generics/const_generics.c @@ -0,0 +1,216 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#include "const_generics.h" + +/** +A monomorphic instance of const_generics.serialize +with const generics +- OUT_LEN= 8 +*/ +void const_generics_serialize_3b(Eurydice_slice re, uint8_t ret[8U]) +{ + uint8_t out[8U] = { 0U }; + Eurydice_slice + uu____0 = Eurydice_array_to_subslice_to((size_t)8U, out, (size_t)4U, uint8_t, size_t); + uint8_t ret0[4U]; + core_num__u32_8__to_be_bytes(Eurydice_slice_index(re, (size_t)0U, uint32_t, uint32_t *), ret0); + Eurydice_slice_copy(uu____0, Eurydice_array_to_slice((size_t)4U, ret0, uint8_t), uint8_t); + Eurydice_slice + uu____1 = Eurydice_array_to_subslice_from((size_t)8U, out, (size_t)4U, uint8_t, size_t); + uint8_t ret1[4U]; + core_num__u32_8__to_be_bytes(Eurydice_slice_index(re, (size_t)1U, uint32_t, uint32_t *), ret1); + Eurydice_slice_copy(uu____1, Eurydice_array_to_slice((size_t)4U, ret1, uint8_t), uint8_t); + memcpy(ret, out, (size_t)8U * sizeof (uint8_t)); +} + +void const_generics_main(void) +{ + uint8_t s[8U]; + uint32_t buf[2U] = { 1U, 2U }; + const_generics_serialize_3b(Eurydice_array_to_slice((size_t)2U, buf, uint32_t), s); + EURYDICE_ASSERT(s[3U] == 1U, "panic!"); + EURYDICE_ASSERT(s[7U] == 2U, "panic!"); +} + +/** +A monomorphic instance of const_generics.mk_pairs +with types uint32_t, uint64_t +with const generics +- N= 2 +- M= 4 +*/ +const_generics_Pair_4e const_generics_mk_pairs_e0(uint32_t x, uint64_t y) +{ + uint32_t a1[2U]; + KRML_MAYBE_FOR2(i, (size_t)0U, (size_t)2U, (size_t)1U, a1[i] = x;); + uint64_t a2[4U]; + KRML_MAYBE_FOR4(i, (size_t)0U, (size_t)4U, (size_t)1U, a2[i] = y;); + /* Passing arrays by value in Rust generates a copy in C */ + uint32_t copy_of_a10[2U]; + memcpy(copy_of_a10, a1, (size_t)2U * sizeof (uint32_t)); + /* Passing arrays by value in Rust generates a copy in C */ + uint64_t copy_of_a20[4U]; + memcpy(copy_of_a20, a2, (size_t)4U * sizeof (uint64_t)); + const_generics_Pair_a5 p1; + memcpy(p1.left, copy_of_a10, (size_t)2U * sizeof (uint32_t)); + memcpy(p1.right, copy_of_a20, (size_t)4U * sizeof (uint64_t)); + /* Passing arrays by value in Rust generates a copy in C */ + uint64_t copy_of_a2[4U]; + memcpy(copy_of_a2, a2, (size_t)4U * sizeof (uint64_t)); + /* Passing arrays by value in Rust generates a copy in C */ + uint32_t copy_of_a1[2U]; + memcpy(copy_of_a1, a1, (size_t)2U * sizeof (uint32_t)); + const_generics_Pair_87 p2; + memcpy(p2.left, copy_of_a2, (size_t)4U * sizeof (uint64_t)); + memcpy(p2.right, copy_of_a1, (size_t)2U * sizeof (uint32_t)); + uint32_t uu____4[2U]; + memcpy(uu____4, p1.left, (size_t)2U * sizeof (uint32_t)); + uint32_t uu____5[2U]; + memcpy(uu____5, p2.right, (size_t)2U * sizeof (uint32_t)); + const_generics_Pair_4e lit; + memcpy(lit.left, uu____4, (size_t)2U * sizeof (uint32_t)); + memcpy(lit.right, uu____5, (size_t)2U * sizeof (uint32_t)); + return lit; +} + +typedef struct _uint32_t__x2_s +{ + uint32_t *fst; + uint32_t *snd; +} +_uint32_t__x2; + +void const_generics_main1(void) +{ + const_generics_Pair_4e uu____0 = const_generics_mk_pairs_e0(0U, 0ULL); + uint32_t left[2U]; + memcpy(left, uu____0.left, (size_t)2U * sizeof (uint32_t)); + uint32_t right[2U]; + memcpy(right, uu____0.right, (size_t)2U * sizeof (uint32_t)); + uint32_t expected = 0U; + _uint32_t__x2 uu____1; + uu____1.fst = left; + uu____1.snd = &expected; + uint32_t *left_val0 = uu____1.fst; + uint32_t *right_val0 = uu____1.snd; + EURYDICE_ASSERT(left_val0[0U] == right_val0[0U], "panic!"); + _uint32_t__x2 uu____2; + uu____2.fst = &left[1U]; + uu____2.snd = &expected; + uint32_t *left_val1 = uu____2.fst; + uint32_t *right_val1 = uu____2.snd; + EURYDICE_ASSERT(left_val1[0U] == right_val1[0U], "panic!"); + _uint32_t__x2 uu____3; + uu____3.fst = right; + uu____3.snd = &expected; + uint32_t *left_val2 = uu____3.fst; + uint32_t *right_val2 = uu____3.snd; + EURYDICE_ASSERT(left_val2[0U] == right_val2[0U], "panic!"); + _uint32_t__x2 uu____4; + uu____4.fst = &right[1U]; + uu____4.snd = &expected; + uint32_t *left_val = uu____4.fst; + uint32_t *right_val = uu____4.snd; + EURYDICE_ASSERT(left_val[0U] == right_val[0U], "panic!"); +} + +/** +A monomorphic instance of const_generics.f +with const generics +- FOO= 1 +- BAR= 2 +*/ +bool const_generics_f_e5(uint32_t x, size_t y) +{ + uint32_t arr1[1U]; + { + arr1[0U] = x; + } + size_t arr2[1U]; + { + arr2[0U] = y; + } + bool uu____0; + if (arr1[0U] == 2U) + { + uu____0 = arr2[0U] == (size_t)1U; + } + else + { + uu____0 = false; + } + return uu____0; +} + +/** +A monomorphic instance of const_generics.f +with const generics +- FOO= 3 +- BAR= 4 +*/ +bool const_generics_f_70(uint32_t x, size_t y) +{ + uint32_t arr1[3U]; + KRML_MAYBE_FOR3(i, (size_t)0U, (size_t)3U, (size_t)1U, arr1[i] = x;); + size_t arr2[3U]; + KRML_MAYBE_FOR3(i, (size_t)0U, (size_t)3U, (size_t)1U, arr2[i] = y;); + bool uu____0; + if (arr1[0U] == 4U) + { + uu____0 = arr2[0U] == (size_t)3U; + } + else + { + uu____0 = false; + } + return uu____0; +} + +/** +A monomorphic instance of const_generics.g +with const generics +- BAR= 3 +- FOO= 4 +*/ +bool const_generics_g_70(uint32_t x, size_t y) +{ + if (const_generics_f_70(x, y)) + { + if (x == 4U) + { + return y == (size_t)3U; + } + } + return false; +} + +typedef struct _bool__x2_s +{ + bool *fst; + bool *snd; +} +_bool__x2; + +void const_generics_main3(void) +{ + bool x; + if (const_generics_f_e5(0U, (size_t)0U)) + { + x = const_generics_g_70(0U, (size_t)0U); + } + else + { + x = false; + } + bool expected = false; + _bool__x2 uu____0 = { .fst = &x, .snd = &expected }; + bool *left_val = uu____0.fst; + bool *right_val = uu____0.snd; + EURYDICE_ASSERT(left_val[0U] == right_val[0U], "panic!"); +} + diff --git a/out/test-const_generics/const_generics.h b/out/test-const_generics/const_generics.h new file mode 100644 index 0000000..47356f9 --- /dev/null +++ b/out/test-const_generics/const_generics.h @@ -0,0 +1,125 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#ifndef __const_generics_H +#define __const_generics_H + +#if defined(__cplusplus) +extern "C" { +#endif + +#include "Eurydice.h" +#include "eurydice_glue.h" + +static inline void core_num__u32_8__to_be_bytes(uint32_t x0, uint8_t x1[4U]); + +/** +A monomorphic instance of const_generics.serialize +with const generics +- OUT_LEN= 8 +*/ +void const_generics_serialize_3b(Eurydice_slice re, uint8_t ret[8U]); + +void const_generics_main(void); + +#define core_panicking_AssertKind_Eq 0 +#define core_panicking_AssertKind_Ne 1 +#define core_panicking_AssertKind_Match 2 + +typedef uint8_t core_panicking_AssertKind; + +/** +A monomorphic instance of const_generics.Pair +with types uint32_t, uint32_t +with const generics +- $2size_t +- $2size_t +*/ +typedef struct const_generics_Pair_4e_s +{ + uint32_t left[2U]; + uint32_t right[2U]; +} +const_generics_Pair_4e; + +/** +A monomorphic instance of const_generics.Pair +with types uint32_t, uint64_t +with const generics +- $2size_t +- $4size_t +*/ +typedef struct const_generics_Pair_a5_s +{ + uint32_t left[2U]; + uint64_t right[4U]; +} +const_generics_Pair_a5; + +/** +A monomorphic instance of const_generics.Pair +with types uint64_t, uint32_t +with const generics +- $4size_t +- $2size_t +*/ +typedef struct const_generics_Pair_87_s +{ + uint64_t left[4U]; + uint32_t right[2U]; +} +const_generics_Pair_87; + +/** +A monomorphic instance of const_generics.mk_pairs +with types uint32_t, uint64_t +with const generics +- N= 2 +- M= 4 +*/ +const_generics_Pair_4e const_generics_mk_pairs_e0(uint32_t x, uint64_t y); + +void const_generics_main1(void); + +/** +A monomorphic instance of const_generics.f +with const generics +- FOO= 1 +- BAR= 2 +*/ +bool const_generics_f_e5(uint32_t x, size_t y); + +/** +A monomorphic instance of const_generics.f +with const generics +- FOO= 3 +- BAR= 4 +*/ +bool const_generics_f_70(uint32_t x, size_t y); + +/** +A monomorphic instance of const_generics.g +with const generics +- BAR= 3 +- FOO= 4 +*/ +bool const_generics_g_70(uint32_t x, size_t y); + +void const_generics_main3(void); + +extern uint32_t core_clone_impls___core__clone__Clone_for_u32__8__clone(uint32_t *x0); + +extern uint64_t core_clone_impls___core__clone__Clone_for_u64__9__clone(uint64_t *x0); + +extern uint8_t core_clone_impls___core__clone__Clone_for_u8__6__clone(uint8_t *x0); + +#if defined(__cplusplus) +} +#endif + +#define __const_generics_H_DEFINED +#endif diff --git a/out/test-inline_attributes/inline_attributes.c b/out/test-inline_attributes/inline_attributes.c new file mode 100644 index 0000000..57c9ab9 --- /dev/null +++ b/out/test-inline_attributes/inline_attributes.c @@ -0,0 +1,31 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#include "inline_attributes.h" + +inline uint32_t inline_attributes_f(void) +{ + return 1U; +} + +KRML_NOINLINE uint32_t inline_attributes_g(void) +{ + return 2U; +} + +KRML_MUSTINLINE uint32_t inline_attributes_h(void) +{ + return 3U; +} + +void inline_attributes_main(void) +{ + LowStar_Ignore_ignore(inline_attributes_f(), uint32_t, void *); + LowStar_Ignore_ignore(inline_attributes_g(), uint32_t, void *); + LowStar_Ignore_ignore(inline_attributes_h(), uint32_t, void *); +} + diff --git a/out/test-inline_attributes/inline_attributes.h b/out/test-inline_attributes/inline_attributes.h new file mode 100644 index 0000000..aaa1ef7 --- /dev/null +++ b/out/test-inline_attributes/inline_attributes.h @@ -0,0 +1,30 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#ifndef __inline_attributes_H +#define __inline_attributes_H + +#if defined(__cplusplus) +extern "C" { +#endif + +#include "eurydice_glue.h" + +uint32_t inline_attributes_f(void); + +uint32_t inline_attributes_g(void); + +uint32_t inline_attributes_h(void); + +void inline_attributes_main(void); + +#if defined(__cplusplus) +} +#endif + +#define __inline_attributes_H_DEFINED +#endif diff --git a/out/test-int_switch/int_switch.c b/out/test-int_switch/int_switch.c new file mode 100644 index 0000000..8b290b9 --- /dev/null +++ b/out/test-int_switch/int_switch.c @@ -0,0 +1,36 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#include "int_switch.h" + +uint32_t int_switch_f(void) +{ + return 0U; +} + +void int_switch_main(void) +{ + switch (int_switch_f()) + { + case 0U: + { + break; + } + case 1U: + { + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); + KRML_HOST_EXIT(255U); + break; + } + default: + { + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); + KRML_HOST_EXIT(255U); + } + } +} + diff --git a/out/test-int_switch/int_switch.h b/out/test-int_switch/int_switch.h new file mode 100644 index 0000000..d91cfcb --- /dev/null +++ b/out/test-int_switch/int_switch.h @@ -0,0 +1,26 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#ifndef __int_switch_H +#define __int_switch_H + +#if defined(__cplusplus) +extern "C" { +#endif + +#include "eurydice_glue.h" + +uint32_t int_switch_f(void); + +void int_switch_main(void); + +#if defined(__cplusplus) +} +#endif + +#define __int_switch_H_DEFINED +#endif diff --git a/out/test-issue_102/issue_102.c b/out/test-issue_102/issue_102.c new file mode 100644 index 0000000..6289b17 --- /dev/null +++ b/out/test-issue_102/issue_102.c @@ -0,0 +1,14 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#include "issue_102.h" + +void issue_102_main(void) +{ + +} + diff --git a/out/test-issue_102/issue_102.h b/out/test-issue_102/issue_102.h new file mode 100644 index 0000000..dcd9578 --- /dev/null +++ b/out/test-issue_102/issue_102.h @@ -0,0 +1,34 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#ifndef __issue_102_H +#define __issue_102_H + +#if defined(__cplusplus) +extern "C" { +#endif + +#include "eurydice_glue.h" + +#define issue_102_Error1_Reason1 1 +#define issue_102_Error1_Reason2 2 + +typedef uint8_t issue_102_Error1; + +#define issue_102_Error2_Reason1 3 +#define issue_102_Error2_Reason2 4 + +typedef uint8_t issue_102_Error2; + +void issue_102_main(void); + +#if defined(__cplusplus) +} +#endif + +#define __issue_102_H_DEFINED +#endif diff --git a/out/test-issue_104/issue_104.c b/out/test-issue_104/issue_104.c new file mode 100644 index 0000000..b44f8b6 --- /dev/null +++ b/out/test-issue_104/issue_104.c @@ -0,0 +1,44 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#include "issue_104.h" + +/** +A monomorphic instance of issue_104.sth +with types issue_104_S +with const generics + +*/ +uint8_t issue_104_sth_50(void) +{ + return ISSUE_104___ISSUE_104__FUN_FOR_ISSUE_104__S___VAL; +} + +uint8_t issue_104_call(void) +{ + return issue_104_sth_50(); +} + +typedef struct _uint8_t__x2_s +{ + uint8_t *fst; + uint8_t *snd; +} +_uint8_t__x2; + +void issue_104_main(void) +{ + /* original Rust expression is not an lvalue in C */ + uint8_t lvalue0 = issue_104_call(); + /* original Rust expression is not an lvalue in C */ + uint8_t lvalue = 5U; + _uint8_t__x2 uu____0 = { .fst = &lvalue0, .snd = &lvalue }; + uint8_t *left_val = uu____0.fst; + uint8_t *right_val = uu____0.snd; + EURYDICE_ASSERT(left_val[0U] == right_val[0U], "panic!"); +} + diff --git a/out/test-issue_104/issue_104.h b/out/test-issue_104/issue_104.h new file mode 100644 index 0000000..e8311d9 --- /dev/null +++ b/out/test-issue_104/issue_104.h @@ -0,0 +1,42 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#ifndef __issue_104_H +#define __issue_104_H + +#if defined(__cplusplus) +extern "C" { +#endif + +#include "eurydice_glue.h" + +#define core_panicking_AssertKind_Eq 0 +#define core_panicking_AssertKind_Ne 1 +#define core_panicking_AssertKind_Match 2 + +typedef uint8_t core_panicking_AssertKind; + +#define ISSUE_104___ISSUE_104__FUN_FOR_ISSUE_104__S___VAL (5U) + +/** +A monomorphic instance of issue_104.sth +with types issue_104_S +with const generics + +*/ +uint8_t issue_104_sth_50(void); + +uint8_t issue_104_call(void); + +void issue_104_main(void); + +#if defined(__cplusplus) +} +#endif + +#define __issue_104_H_DEFINED +#endif diff --git a/out/test-issue_106/issue_106.c b/out/test-issue_106/issue_106.c new file mode 100644 index 0000000..67d4a95 --- /dev/null +++ b/out/test-issue_106/issue_106.c @@ -0,0 +1,31 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#include "issue_106.h" + +uint8_t issue_106_generate(void) +{ + return 5U; +} + +void issue_106_main(void) +{ + +} + +uint8_t issue_106_use_it(uint8_t *x) +{ + return x[0U]; +} + +uint8_t issue_106_use_ref(void) +{ + /* original Rust expression is not an lvalue in C */ + uint8_t lvalue = issue_106_generate(); + return issue_106_use_it(&lvalue); +} + diff --git a/out/test-issue_106/issue_106.h b/out/test-issue_106/issue_106.h new file mode 100644 index 0000000..c878195 --- /dev/null +++ b/out/test-issue_106/issue_106.h @@ -0,0 +1,32 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#ifndef __issue_106_H +#define __issue_106_H + +#if defined(__cplusplus) +extern "C" { +#endif + +#include "eurydice_glue.h" + +typedef uint8_t issue_106_MyStruct; + +uint8_t issue_106_generate(void); + +void issue_106_main(void); + +uint8_t issue_106_use_it(uint8_t *x); + +uint8_t issue_106_use_ref(void); + +#if defined(__cplusplus) +} +#endif + +#define __issue_106_H_DEFINED +#endif diff --git a/out/test-issue_107/issue_107.c b/out/test-issue_107/issue_107.c new file mode 100644 index 0000000..513e9f2 --- /dev/null +++ b/out/test-issue_107/issue_107.c @@ -0,0 +1,22 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#include "issue_107.h" + +void issue_107_main(void) +{ + +} + +/** +This function found in impl {(issue_107::Fun for issue_107::MyStruct)} +*/ +uint8_t issue_107_f_18(void) +{ + return 5U; +} + diff --git a/out/test-issue_107/issue_107.h b/out/test-issue_107/issue_107.h new file mode 100644 index 0000000..0dad7ad --- /dev/null +++ b/out/test-issue_107/issue_107.h @@ -0,0 +1,29 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#ifndef __issue_107_H +#define __issue_107_H + +#if defined(__cplusplus) +extern "C" { +#endif + +#include "eurydice_glue.h" + +void issue_107_main(void); + +/** +This function found in impl {(issue_107::Fun for issue_107::MyStruct)} +*/ +uint8_t issue_107_f_18(void); + +#if defined(__cplusplus) +} +#endif + +#define __issue_107_H_DEFINED +#endif diff --git a/out/test-issue_123/issue_123.c b/out/test-issue_123/issue_123.c new file mode 100644 index 0000000..651e7bb --- /dev/null +++ b/out/test-issue_123/issue_123.c @@ -0,0 +1,59 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#include "issue_123.h" + +int32_t issue_123_fun(issue_123_E e) +{ + ptrdiff_t uu____0; + if (e == issue_123_E_One) + { + uu____0 = (ptrdiff_t)1; + } + else + { + uu____0 = (ptrdiff_t)5; + } + uint8_t uu____1 = (uint8_t)uu____0; + EURYDICE_ASSERT(!!(uu____1 >= 1U && uu____1 <= 5U), "assert failure"); + return (int32_t)uu____0; +} + +typedef struct _ptrdiff_t__x2_s +{ + ptrdiff_t *fst; + ptrdiff_t *snd; +} +_ptrdiff_t__x2; + +typedef struct _int32_t__x2_s +{ + int32_t *fst; + int32_t *snd; +} +_int32_t__x2; + +void issue_123_main(void) +{ + /* original Rust expression is not an lvalue in C */ + ptrdiff_t lvalue0 = (ptrdiff_t)((ptrdiff_t)255 + (ptrdiff_t)0); + /* original Rust expression is not an lvalue in C */ + ptrdiff_t lvalue1 = (ptrdiff_t)-1; + _ptrdiff_t__x2 uu____0 = { .fst = &lvalue0, .snd = &lvalue1 }; + ptrdiff_t *left_val0 = uu____0.fst; + ptrdiff_t *right_val0 = uu____0.snd; + EURYDICE_ASSERT(left_val0[0U] == right_val0[0U], "panic!"); + /* original Rust expression is not an lvalue in C */ + int32_t lvalue2 = issue_123_fun(issue_123_E_One); + /* original Rust expression is not an lvalue in C */ + int32_t lvalue = (int32_t)1; + _int32_t__x2 uu____1 = { .fst = &lvalue2, .snd = &lvalue }; + int32_t *left_val = uu____1.fst; + int32_t *right_val = uu____1.snd; + EURYDICE_ASSERT(left_val[0U] == right_val[0U], "panic!"); +} + diff --git a/out/test-issue_123/issue_123.h b/out/test-issue_123/issue_123.h new file mode 100644 index 0000000..0bf0003 --- /dev/null +++ b/out/test-issue_123/issue_123.h @@ -0,0 +1,62 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#ifndef __issue_123_H +#define __issue_123_H + +#if defined(__cplusplus) +extern "C" { +#endif + +#include "eurydice_glue.h" + +#define core_panicking_AssertKind_Eq 0 +#define core_panicking_AssertKind_Ne 1 +#define core_panicking_AssertKind_Match 2 + +typedef uint8_t core_panicking_AssertKind; + +#define issue_123_E_One 1 +#define issue_123_E_Five 5 + +typedef uint8_t issue_123_E; + +#define issue_123_E1_C1 4294967295 +#define issue_123_E1_C2 -4294967295 +#define issue_123_E1_C3 268435455 + +typedef int64_t issue_123_E1; + +#define issue_123_E2_C1 255 +#define issue_123_E2_C2 -1 + +typedef int16_t issue_123_E2; + +#define issue_123_E3_C1 255 + +typedef uint8_t issue_123_E3; + +#define issue_123_E4_C1 127 +#define issue_123_E4_C2 -126 + +typedef int8_t issue_123_E4; + +#define issue_123_Gamma2_V95_232 95232 +#define issue_123_Gamma2_V261_888 261888 + +typedef uint32_t issue_123_Gamma2; + +int32_t issue_123_fun(issue_123_E e); + +void issue_123_main(void); + +#if defined(__cplusplus) +} +#endif + +#define __issue_123_H_DEFINED +#endif diff --git a/out/test-issue_96/issue_96.c b/out/test-issue_96/issue_96.c new file mode 100644 index 0000000..93d32f9 --- /dev/null +++ b/out/test-issue_96/issue_96.c @@ -0,0 +1,36 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#include "issue_96.h" + +void issue_96_use_it(issue_96_MyStruct *x) +{ + +} + +void issue_96_use_it2(issue_96_MyStruct2 *x) +{ + +} + +void issue_96_main(void) +{ + issue_96_MyStruct x; + x.fst[0U] = 0U; + x.fst[1U] = 0U; + x.fst[2U] = 0U; + x.fst[3U] = 0U; + x.fst[4U] = 0U; + issue_96_MyStruct2 x0; + x0.fst[0U] = 0U; + x0.fst[1U] = 0U; + x0.fst[2U] = 0U; + x0.fst[3U] = 0U; + x0.fst[4U] = 0U; + x0.snd = 2U; +} + diff --git a/out/test-issue_96/issue_96.h b/out/test-issue_96/issue_96.h new file mode 100644 index 0000000..2e19424 --- /dev/null +++ b/out/test-issue_96/issue_96.h @@ -0,0 +1,37 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#ifndef __issue_96_H +#define __issue_96_H + +#if defined(__cplusplus) +extern "C" { +#endif + +#include "eurydice_glue.h" + +typedef struct issue_96_MyStruct_s { uint8_t fst[5U]; } issue_96_MyStruct; + +typedef struct issue_96_MyStruct2_s +{ + uint8_t fst[5U]; + uint32_t snd; +} +issue_96_MyStruct2; + +void issue_96_use_it(issue_96_MyStruct *x); + +void issue_96_use_it2(issue_96_MyStruct2 *x); + +void issue_96_main(void); + +#if defined(__cplusplus) +} +#endif + +#define __issue_96_H_DEFINED +#endif diff --git a/out/test-mismatch/mismatch.c b/out/test-mismatch/mismatch.c new file mode 100644 index 0000000..baa80f2 --- /dev/null +++ b/out/test-mismatch/mismatch.c @@ -0,0 +1,14 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#include "mismatch.h" + +void mismatch_main(void) +{ + +} + diff --git a/out/test-mismatch/mismatch.h b/out/test-mismatch/mismatch.h new file mode 100644 index 0000000..595b428 --- /dev/null +++ b/out/test-mismatch/mismatch.h @@ -0,0 +1,24 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#ifndef __mismatch_H +#define __mismatch_H + +#if defined(__cplusplus) +extern "C" { +#endif + +#include "eurydice_glue.h" + +void mismatch_main(void); + +#if defined(__cplusplus) +} +#endif + +#define __mismatch_H_DEFINED +#endif diff --git a/out/test-nested_arrays/Eurydice.h b/out/test-nested_arrays/Eurydice.h new file mode 100644 index 0000000..f53ea17 --- /dev/null +++ b/out/test-nested_arrays/Eurydice.h @@ -0,0 +1,34 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#ifndef __Eurydice_H +#define __Eurydice_H + +#if defined(__cplusplus) +extern "C" { +#endif + +#include "eurydice_glue.h" + +/** +A monomorphic instance of core.ops.range.Range +with types size_t + +*/ +typedef struct core_ops_range_Range_08_s +{ + size_t start; + size_t end; +} +core_ops_range_Range_08; + +#if defined(__cplusplus) +} +#endif + +#define __Eurydice_H_DEFINED +#endif diff --git a/out/test-nested_arrays/nested_arrays.c b/out/test-nested_arrays/nested_arrays.c new file mode 100644 index 0000000..fc9d820 --- /dev/null +++ b/out/test-nested_arrays/nested_arrays.c @@ -0,0 +1,47 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#include "nested_arrays.h" + +const uint32_t nested_arrays_ZERO[8U] = { 0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U }; + +typedef struct _uint32_t__x2_s +{ + uint32_t *fst; + uint32_t *snd; +} +_uint32_t__x2; + +void nested_arrays_main(void) +{ + uint32_t keys[3U][3U][8U]; + for (size_t i = (size_t)0U; i < (size_t)3U; i++) + { + memcpy(keys[i][0U], nested_arrays_ZERO, (size_t)8U * sizeof (uint32_t)); + memcpy(keys[i][1U], nested_arrays_ZERO, (size_t)8U * sizeof (uint32_t)); + memcpy(keys[i][2U], nested_arrays_ZERO, (size_t)8U * sizeof (uint32_t)); + } + for (size_t i0 = (size_t)0U; i0 < (size_t)3U; i0++) + { + size_t i1 = i0; + for (size_t i2 = (size_t)0U; i2 < (size_t)3U; i2++) + { + size_t j = i2; + for (size_t i = (size_t)0U; i < (size_t)8U; i++) + { + size_t k = i; + uint32_t actual = keys[i1][j][k]; + uint32_t expected = (uint32_t)k; + _uint32_t__x2 uu____0 = { .fst = &actual, .snd = &expected }; + uint32_t *left_val = uu____0.fst; + uint32_t *right_val = uu____0.snd; + EURYDICE_ASSERT(left_val[0U] == right_val[0U], "panic!"); + } + } + } +} + diff --git a/out/test-nested_arrays/nested_arrays.h b/out/test-nested_arrays/nested_arrays.h new file mode 100644 index 0000000..029f0ed --- /dev/null +++ b/out/test-nested_arrays/nested_arrays.h @@ -0,0 +1,163 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#ifndef __nested_arrays_H +#define __nested_arrays_H + +#if defined(__cplusplus) +extern "C" { +#endif + +#include "eurydice_glue.h" + +extern size_t core_clone_impls___core__clone__Clone_for_usize__5__clone(size_t *x0); + +#define core_cmp_Ordering_Less -1 +#define core_cmp_Ordering_Equal 0 +#define core_cmp_Ordering_Greater 1 + +typedef int8_t core_cmp_Ordering; + +extern bool +core_cmp_impls___core__cmp__PartialEq_usize__for_usize__21__eq(size_t *x0, size_t *x1); + +extern bool +core_cmp_impls___core__cmp__PartialEq_usize__for_usize__21__ne(size_t *x0, size_t *x1); + +extern bool +core_cmp_impls___core__cmp__PartialOrd_usize__for_usize__58__ge(size_t *x0, size_t *x1); + +extern bool +core_cmp_impls___core__cmp__PartialOrd_usize__for_usize__58__gt(size_t *x0, size_t *x1); + +extern bool +core_cmp_impls___core__cmp__PartialOrd_usize__for_usize__58__le(size_t *x0, size_t *x1); + +extern bool +core_cmp_impls___core__cmp__PartialOrd_usize__for_usize__58__lt(size_t *x0, size_t *x1); + +#define core_option_None 0 +#define core_option_Some 1 + +typedef uint8_t core_option_Option_77_tags; + +/** +A monomorphic instance of core.option.Option +with types core_cmp_Ordering + +*/ +typedef struct core_option_Option_77_s +{ + core_option_Option_77_tags tag; + core_cmp_Ordering f0; +} +core_option_Option_77; + +extern core_option_Option_77 +core_cmp_impls___core__cmp__PartialOrd_usize__for_usize__58__partial_cmp( + size_t *x0, + size_t *x1 +); + +extern size_t +core_iter_range___core__iter__range__Step_for_usize__43__backward(size_t x0, size_t x1); + +/** +A monomorphic instance of core.option.Option +with types size_t + +*/ +typedef struct core_option_Option_08_s +{ + core_option_Option_77_tags tag; + size_t f0; +} +core_option_Option_08; + +extern core_option_Option_08 +core_iter_range___core__iter__range__Step_for_usize__43__backward_checked(size_t x0, size_t x1); + +extern size_t +core_iter_range___core__iter__range__Step_for_usize__43__backward_unchecked( + size_t x0, + size_t x1 +); + +extern size_t +core_iter_range___core__iter__range__Step_for_usize__43__forward(size_t x0, size_t x1); + +extern core_option_Option_08 +core_iter_range___core__iter__range__Step_for_usize__43__forward_checked(size_t x0, size_t x1); + +extern size_t +core_iter_range___core__iter__range__Step_for_usize__43__forward_unchecked( + size_t x0, + size_t x1 +); + +extern core_option_Option_08 +core_iter_range___core__iter__range__Step_for_usize__43__steps_between(size_t *x0, size_t *x1); + +/** +A monomorphic instance of core.num.nonzero.NonZero +with types size_t + +*/ +typedef size_t core_num_nonzero_NonZero_08; + +#define core_result_Ok 0 +#define core_result_Err 1 + +typedef uint8_t core_result_Result_eb_tags; + +/** +A monomorphic instance of core.result.Result +with types (), core_num_nonzero_NonZero size_t + +*/ +typedef struct core_result_Result_eb_s +{ + core_result_Result_eb_tags tag; + core_num_nonzero_NonZero_08 f0; +} +core_result_Result_eb; + +/** +A monomorphic instance of K. +with types size_t, core_option_Option size_t + +*/ +typedef struct tuple_04_s +{ + size_t fst; + core_option_Option_08 snd; +} +tuple_04; + +static inline core_num_nonzero_private_NonZeroUsizeInner +core_num_nonzero_private___core__clone__Clone_for_core__num__nonzero__private__NonZeroUsizeInner__26__clone( + core_num_nonzero_private_NonZeroUsizeInner *x0 +); + +#define core_panicking_AssertKind_Eq 0 +#define core_panicking_AssertKind_Ne 1 +#define core_panicking_AssertKind_Match 2 + +typedef uint8_t core_panicking_AssertKind; + +typedef uint32_t nested_arrays_Key[8U]; + +extern const uint32_t nested_arrays_ZERO[8U]; + +void nested_arrays_main(void); + +#if defined(__cplusplus) +} +#endif + +#define __nested_arrays_H_DEFINED +#endif diff --git a/out/test-nested_arrays2/nested_arrays2.c b/out/test-nested_arrays2/nested_arrays2.c new file mode 100644 index 0000000..1ed4f50 --- /dev/null +++ b/out/test-nested_arrays2/nested_arrays2.c @@ -0,0 +1,16 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#include "nested_arrays2.h" + +const uint8_t nested_arrays2_TABLE[1U][1U] = { { 1U } }; + +void nested_arrays2_main(void) +{ + +} + diff --git a/out/test-nested_arrays2/nested_arrays2.h b/out/test-nested_arrays2/nested_arrays2.h new file mode 100644 index 0000000..2530ace --- /dev/null +++ b/out/test-nested_arrays2/nested_arrays2.h @@ -0,0 +1,26 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#ifndef __nested_arrays2_H +#define __nested_arrays2_H + +#if defined(__cplusplus) +extern "C" { +#endif + +#include "eurydice_glue.h" + +extern const uint8_t nested_arrays2_TABLE[1U][1U]; + +void nested_arrays2_main(void); + +#if defined(__cplusplus) +} +#endif + +#define __nested_arrays2_H_DEFINED +#endif diff --git a/out/test-partial_eq/partial_eq.c b/out/test-partial_eq/partial_eq.c new file mode 100644 index 0000000..e1d631d --- /dev/null +++ b/out/test-partial_eq/partial_eq.c @@ -0,0 +1,41 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#include "partial_eq.h" + +/** +This function found in impl {(core::cmp::PartialEq for partial_eq::Enum)#1} +*/ +inline bool partial_eq_eq_dd(partial_eq_Enum *self, partial_eq_Enum *other) +{ + return true; +} + +typedef struct _partial_eq_Enum__x2_s +{ + partial_eq_Enum *fst; + partial_eq_Enum *snd; +} +_partial_eq_Enum__x2; + +void partial_eq_main(void) +{ + partial_eq_Enum expected = partial_eq_Enum_A; + _partial_eq_Enum__x2 uu____0 = { .fst = &expected, .snd = &expected }; + partial_eq_Enum *left_val = uu____0.fst; + partial_eq_Enum *right_val = uu____0.snd; + EURYDICE_ASSERT(partial_eq_eq_dd(left_val, right_val), "panic!"); +} + +/** +This function found in impl {(core::fmt::Debug for partial_eq::Enum)#2} +*/ +inline core_result_Result_a9 partial_eq_fmt_19(partial_eq_Enum *self, core_fmt_Formatter *f) +{ + return core_fmt__core__fmt__Formatter__a__9__write_str(f, "A"); +} + diff --git a/out/test-partial_eq/partial_eq.h b/out/test-partial_eq/partial_eq.h new file mode 100644 index 0000000..418df65 --- /dev/null +++ b/out/test-partial_eq/partial_eq.h @@ -0,0 +1,64 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#ifndef __partial_eq_H +#define __partial_eq_H + +#if defined(__cplusplus) +extern "C" { +#endif + +#include "eurydice_glue.h" + +#define core_result_Ok 0 +#define core_result_Err 1 + +typedef uint8_t core_result_Result_a9_tags; + +/** +A monomorphic instance of core.result.Result +with types (), core_fmt_Error + +*/ +typedef struct core_result_Result_a9_s +{ + core_result_Result_a9_tags tag; + void *f0; +} +core_result_Result_a9; + +extern core_result_Result_a9 +core_fmt__core__fmt__Formatter__a__9__write_str(core_fmt_Formatter *x0, Prims_string x1); + +#define core_panicking_AssertKind_Eq 0 +#define core_panicking_AssertKind_Ne 1 +#define core_panicking_AssertKind_Match 2 + +typedef uint8_t core_panicking_AssertKind; + +#define partial_eq_Enum_A 0 + +typedef uint8_t partial_eq_Enum; + +/** +This function found in impl {(core::cmp::PartialEq for partial_eq::Enum)#1} +*/ +bool partial_eq_eq_dd(partial_eq_Enum *self, partial_eq_Enum *other); + +void partial_eq_main(void); + +/** +This function found in impl {(core::fmt::Debug for partial_eq::Enum)#2} +*/ +core_result_Result_a9 partial_eq_fmt_19(partial_eq_Enum *self, core_fmt_Formatter *f); + +#if defined(__cplusplus) +} +#endif + +#define __partial_eq_H_DEFINED +#endif diff --git a/out/test-slice_array/slice_array.c b/out/test-slice_array/slice_array.c new file mode 100644 index 0000000..8d4156e --- /dev/null +++ b/out/test-slice_array/slice_array.c @@ -0,0 +1,62 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#include "slice_array.h" + +typedef struct _uint8_t__x2_s +{ + uint8_t *fst; + uint8_t *snd; +} +_uint8_t__x2; + +void slice_array_f1(void) +{ + uint8_t x[4U][4U] = { { 0U } }; + Eurydice_slice + y0 = + Eurydice_slice_split_at_mut(Eurydice_array_to_slice((size_t)4U, x, uint8_t [4U]), + (size_t)2U, + uint8_t [4U], + Eurydice_slice_uint8_t_4size_t__x2).fst; + Eurydice_slice_index(y0, (size_t)0U, uint8_t [4U], uint8_t (*)[4U])[0U] = 1U; + uint8_t actual = x[0U][0U]; + uint8_t expected = 1U; + _uint8_t__x2 uu____0 = { .fst = &actual, .snd = &expected }; + uint8_t *left_val = uu____0.fst; + uint8_t *right_val = uu____0.snd; + EURYDICE_ASSERT(left_val[0U] == right_val[0U], "panic!"); +} + +void slice_array_f2(void) +{ + uint8_t x[4U][4U] = { { 0U } }; + Eurydice_slice + y0 = + Eurydice_slice_split_at_mut(Eurydice_array_to_slice((size_t)4U, x, uint8_t [4U]), + (size_t)2U, + uint8_t [4U], + Eurydice_slice_uint8_t_4size_t__x2).fst; + uint8_t z[4U]; + memcpy(z, + Eurydice_slice_index(y0, (size_t)0U, uint8_t [4U], uint8_t (*)[4U]), + (size_t)4U * sizeof (uint8_t)); + z[0U] = 1U; + uint8_t actual = x[0U][0U]; + uint8_t expected = 0U; + _uint8_t__x2 uu____0 = { .fst = &actual, .snd = &expected }; + uint8_t *left_val = uu____0.fst; + uint8_t *right_val = uu____0.snd; + EURYDICE_ASSERT(left_val[0U] == right_val[0U], "panic!"); +} + +void slice_array_main(void) +{ + slice_array_f1(); + slice_array_f2(); +} + diff --git a/out/test-slice_array/slice_array.h b/out/test-slice_array/slice_array.h new file mode 100644 index 0000000..47be82d --- /dev/null +++ b/out/test-slice_array/slice_array.h @@ -0,0 +1,41 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#ifndef __slice_array_H +#define __slice_array_H + +#if defined(__cplusplus) +extern "C" { +#endif + +#include "eurydice_glue.h" + +#define core_panicking_AssertKind_Eq 0 +#define core_panicking_AssertKind_Ne 1 +#define core_panicking_AssertKind_Match 2 + +typedef uint8_t core_panicking_AssertKind; + +typedef struct Eurydice_slice_uint8_t_4size_t__x2_s +{ + Eurydice_slice fst; + Eurydice_slice snd; +} +Eurydice_slice_uint8_t_4size_t__x2; + +void slice_array_f1(void); + +void slice_array_f2(void); + +void slice_array_main(void); + +#if defined(__cplusplus) +} +#endif + +#define __slice_array_H_DEFINED +#endif diff --git a/out/test-symcrust/Eurydice.h b/out/test-symcrust/Eurydice.h new file mode 100644 index 0000000..f53ea17 --- /dev/null +++ b/out/test-symcrust/Eurydice.h @@ -0,0 +1,34 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#ifndef __Eurydice_H +#define __Eurydice_H + +#if defined(__cplusplus) +extern "C" { +#endif + +#include "eurydice_glue.h" + +/** +A monomorphic instance of core.ops.range.Range +with types size_t + +*/ +typedef struct core_ops_range_Range_08_s +{ + size_t start; + size_t end; +} +core_ops_range_Range_08; + +#if defined(__cplusplus) +} +#endif + +#define __Eurydice_H_DEFINED +#endif diff --git a/out/test-symcrust/internal/Eurydice.h b/out/test-symcrust/internal/Eurydice.h new file mode 100644 index 0000000..2d95884 --- /dev/null +++ b/out/test-symcrust/internal/Eurydice.h @@ -0,0 +1,25 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#ifndef __internal_Eurydice_H +#define __internal_Eurydice_H + +#if defined(__cplusplus) +extern "C" { +#endif + +#include "../Eurydice.h" +#include "eurydice_glue.h" + +extern uint32_t Eurydice_min_u32(uint32_t x, uint32_t y); + +#if defined(__cplusplus) +} +#endif + +#define __internal_Eurydice_H_DEFINED +#endif diff --git a/out/test-symcrust/symcrust.c b/out/test-symcrust/symcrust.c new file mode 100644 index 0000000..3c8938a --- /dev/null +++ b/out/test-symcrust/symcrust.c @@ -0,0 +1,71 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#include "symcrust.h" + +#include "internal/Eurydice.h" + +void +symcrust_SymCrustMlKemPolyElementCompressAndEncode( + uint16_t *coeffs, + uint32_t nBitsPerCoefficient, + Eurydice_slice dst +) +{ + uint64_t SYMCRYPT_MLKEM_COMPRESS_MULCONSTANT = 10321339ULL; + uint32_t SYMCRYPT_MLKEM_COMPRESS_SHIFTCONSTANT = 35U; + size_t cbDstWritten = (size_t)0U; + uint32_t accumulator = 0U; + uint32_t nBitsInAccumulator = 0U; + EURYDICE_ASSERT(nBitsPerCoefficient > 0U, "panic!"); + EURYDICE_ASSERT(nBitsPerCoefficient <= 12U, "panic!"); + EURYDICE_ASSERT((uint64_t)Eurydice_slice_len(dst, uint8_t) + == 256ULL * (uint64_t)nBitsPerCoefficient / 8ULL, + "panic!"); + for (size_t i = (size_t)0U; i < (size_t)256U; i++) + { + size_t i0 = i; + uint32_t nBitsInCoefficient = nBitsPerCoefficient; + uint32_t coefficient = (uint32_t)coeffs[i0]; + if (nBitsPerCoefficient < 12U) + { + uint64_t multiplication = (uint64_t)coefficient * SYMCRYPT_MLKEM_COMPRESS_MULCONSTANT; + coefficient = + (uint32_t)(multiplication + >> (uint32_t)(SYMCRYPT_MLKEM_COMPRESS_SHIFTCONSTANT - (nBitsPerCoefficient + 1U))); + coefficient++; + coefficient = coefficient >> 1U; + coefficient = coefficient & ((1U << (uint32_t)nBitsPerCoefficient) - 1U); + } + while (nBitsInCoefficient > 0U) + { + uint32_t nBitsToEncode = Eurydice_min_u32(nBitsInCoefficient, 32U - nBitsInAccumulator); + uint32_t bitsToEncode = coefficient & ((1U << (uint32_t)nBitsToEncode) - 1U); + coefficient = coefficient >> (uint32_t)nBitsToEncode; + nBitsInCoefficient = nBitsInCoefficient - nBitsToEncode; + accumulator = accumulator | bitsToEncode << (uint32_t)nBitsInAccumulator; + nBitsInAccumulator = nBitsInAccumulator + nBitsToEncode; + if (nBitsInAccumulator == 32U) + { + Eurydice_slice + uu____0 = Eurydice_slice_subslice2(dst, cbDstWritten, cbDstWritten + (size_t)4U, uint8_t); + uint8_t ret[4U]; + core_num__u32_8__to_le_bytes(accumulator, ret); + Eurydice_slice_copy(uu____0, Eurydice_array_to_slice((size_t)4U, ret, uint8_t), uint8_t); + cbDstWritten = cbDstWritten + (size_t)4U; + accumulator = 0U; + nBitsInAccumulator = 0U; + } + } + } +} + +void symcrust_main(void) +{ + +} + diff --git a/out/test-symcrust/symcrust.h b/out/test-symcrust/symcrust.h new file mode 100644 index 0000000..46b5600 --- /dev/null +++ b/out/test-symcrust/symcrust.h @@ -0,0 +1,198 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#ifndef __symcrust_H +#define __symcrust_H + +#if defined(__cplusplus) +extern "C" { +#endif + +#include "Eurydice.h" +#include "eurydice_glue.h" + +extern uint8_t core_clone_impls___core__clone__Clone_for_u8__6__clone(uint8_t *x0); + +extern size_t core_clone_impls___core__clone__Clone_for_usize__5__clone(size_t *x0); + +#define core_cmp_Ordering_Less -1 +#define core_cmp_Ordering_Equal 0 +#define core_cmp_Ordering_Greater 1 + +typedef int8_t core_cmp_Ordering; + +extern core_cmp_Ordering +core_cmp_impls___core__cmp__Ord_for_u32__65__cmp(uint32_t *x0, uint32_t *x1); + +extern bool +core_cmp_impls___core__cmp__PartialEq_u32__for_u32__24__eq(uint32_t *x0, uint32_t *x1); + +extern bool +core_cmp_impls___core__cmp__PartialEq_u32__for_u32__24__ne(uint32_t *x0, uint32_t *x1); + +extern bool +core_cmp_impls___core__cmp__PartialEq_usize__for_usize__21__eq(size_t *x0, size_t *x1); + +extern bool +core_cmp_impls___core__cmp__PartialEq_usize__for_usize__21__ne(size_t *x0, size_t *x1); + +extern bool +core_cmp_impls___core__cmp__PartialOrd_u32__for_u32__64__ge(uint32_t *x0, uint32_t *x1); + +extern bool +core_cmp_impls___core__cmp__PartialOrd_u32__for_u32__64__gt(uint32_t *x0, uint32_t *x1); + +extern bool +core_cmp_impls___core__cmp__PartialOrd_u32__for_u32__64__le(uint32_t *x0, uint32_t *x1); + +extern bool +core_cmp_impls___core__cmp__PartialOrd_u32__for_u32__64__lt(uint32_t *x0, uint32_t *x1); + +#define core_option_None 0 +#define core_option_Some 1 + +typedef uint8_t core_option_Option_77_tags; + +/** +A monomorphic instance of core.option.Option +with types core_cmp_Ordering + +*/ +typedef struct core_option_Option_77_s +{ + core_option_Option_77_tags tag; + core_cmp_Ordering f0; +} +core_option_Option_77; + +extern core_option_Option_77 +core_cmp_impls___core__cmp__PartialOrd_u32__for_u32__64__partial_cmp( + uint32_t *x0, + uint32_t *x1 +); + +extern bool +core_cmp_impls___core__cmp__PartialOrd_usize__for_usize__58__ge(size_t *x0, size_t *x1); + +extern bool +core_cmp_impls___core__cmp__PartialOrd_usize__for_usize__58__gt(size_t *x0, size_t *x1); + +extern bool +core_cmp_impls___core__cmp__PartialOrd_usize__for_usize__58__le(size_t *x0, size_t *x1); + +extern bool +core_cmp_impls___core__cmp__PartialOrd_usize__for_usize__58__lt(size_t *x0, size_t *x1); + +extern core_option_Option_77 +core_cmp_impls___core__cmp__PartialOrd_usize__for_usize__58__partial_cmp( + size_t *x0, + size_t *x1 +); + +static inline uint32_t +core_convert_num___core__convert__From_u16__for_u32__69__from(uint16_t x0); + +static inline uint64_t +core_convert_num___core__convert__From_u32__for_u64__72__from(uint32_t x0); + +extern size_t +core_iter_range___core__iter__range__Step_for_usize__43__backward(size_t x0, size_t x1); + +/** +A monomorphic instance of core.option.Option +with types size_t + +*/ +typedef struct core_option_Option_08_s +{ + core_option_Option_77_tags tag; + size_t f0; +} +core_option_Option_08; + +extern core_option_Option_08 +core_iter_range___core__iter__range__Step_for_usize__43__backward_checked(size_t x0, size_t x1); + +extern size_t +core_iter_range___core__iter__range__Step_for_usize__43__backward_unchecked( + size_t x0, + size_t x1 +); + +extern size_t +core_iter_range___core__iter__range__Step_for_usize__43__forward(size_t x0, size_t x1); + +extern core_option_Option_08 +core_iter_range___core__iter__range__Step_for_usize__43__forward_checked(size_t x0, size_t x1); + +extern size_t +core_iter_range___core__iter__range__Step_for_usize__43__forward_unchecked( + size_t x0, + size_t x1 +); + +extern core_option_Option_08 +core_iter_range___core__iter__range__Step_for_usize__43__steps_between(size_t *x0, size_t *x1); + +/** +A monomorphic instance of core.num.nonzero.NonZero +with types size_t + +*/ +typedef size_t core_num_nonzero_NonZero_08; + +#define core_result_Ok 0 +#define core_result_Err 1 + +typedef uint8_t core_result_Result_eb_tags; + +/** +A monomorphic instance of core.result.Result +with types (), core_num_nonzero_NonZero size_t + +*/ +typedef struct core_result_Result_eb_s +{ + core_result_Result_eb_tags tag; + core_num_nonzero_NonZero_08 f0; +} +core_result_Result_eb; + +/** +A monomorphic instance of K. +with types size_t, core_option_Option size_t + +*/ +typedef struct tuple_04_s +{ + size_t fst; + core_option_Option_08 snd; +} +tuple_04; + +static inline core_num_nonzero_private_NonZeroUsizeInner +core_num_nonzero_private___core__clone__Clone_for_core__num__nonzero__private__NonZeroUsizeInner__26__clone( + core_num_nonzero_private_NonZeroUsizeInner *x0 +); + +static inline void core_num__u32_8__to_le_bytes(uint32_t x0, uint8_t x1[4U]); + +void +symcrust_SymCrustMlKemPolyElementCompressAndEncode( + uint16_t *coeffs, + uint32_t nBitsPerCoefficient, + Eurydice_slice dst +); + +void symcrust_main(void); + +#if defined(__cplusplus) +} +#endif + +#define __symcrust_H_DEFINED +#endif diff --git a/out/test-traits/Eurydice.h b/out/test-traits/Eurydice.h new file mode 100644 index 0000000..f53ea17 --- /dev/null +++ b/out/test-traits/Eurydice.h @@ -0,0 +1,34 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#ifndef __Eurydice_H +#define __Eurydice_H + +#if defined(__cplusplus) +extern "C" { +#endif + +#include "eurydice_glue.h" + +/** +A monomorphic instance of core.ops.range.Range +with types size_t + +*/ +typedef struct core_ops_range_Range_08_s +{ + size_t start; + size_t end; +} +core_ops_range_Range_08; + +#if defined(__cplusplus) +} +#endif + +#define __Eurydice_H_DEFINED +#endif diff --git a/out/test-traits/traits.c b/out/test-traits/traits.c new file mode 100644 index 0000000..8972ac9 --- /dev/null +++ b/out/test-traits/traits.c @@ -0,0 +1,47 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#include "traits.h" + +/** +This function found in impl {(traits::ToInt for traits::Foo)} +*/ +uint32_t traits_to_int_7d(traits_Foo *self) +{ + if (!(self[0U] == traits_Foo_Foo1)) + { + return 2U; + } + return 1U; +} + +/** +This function found in impl {(traits::ToInt for &0 (@Slice))#1} +*/ +uint32_t traits_to_int_dd(Eurydice_slice *self) +{ + uint32_t + uu____0 = + traits_to_int_7d(&Eurydice_slice_index(self[0U], (size_t)0U, traits_Foo, traits_Foo *)); + return + uu____0 + * traits_to_int_7d(&Eurydice_slice_index(self[0U], (size_t)1U, traits_Foo, traits_Foo *)); +} + +void traits_main(void) +{ + traits_Foo foos[2U] = { traits_Foo_Foo1, traits_Foo_Foo2 }; + /* original Rust expression is not an lvalue in C */ + Eurydice_slice lvalue = Eurydice_array_to_subslice2(foos, (size_t)0U, (size_t)2U, traits_Foo); + if (!(traits_to_int_dd(&lvalue) != 2U)) + { + return; + } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); + KRML_HOST_EXIT(255U); +} + diff --git a/out/test-traits/traits.h b/out/test-traits/traits.h new file mode 100644 index 0000000..edd4f6f --- /dev/null +++ b/out/test-traits/traits.h @@ -0,0 +1,40 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#ifndef __traits_H +#define __traits_H + +#if defined(__cplusplus) +extern "C" { +#endif + +#include "Eurydice.h" +#include "eurydice_glue.h" + +#define traits_Foo_Foo1 0 +#define traits_Foo_Foo2 1 + +typedef uint8_t traits_Foo; + +/** +This function found in impl {(traits::ToInt for traits::Foo)} +*/ +uint32_t traits_to_int_7d(traits_Foo *self); + +/** +This function found in impl {(traits::ToInt for &0 (@Slice))#1} +*/ +uint32_t traits_to_int_dd(Eurydice_slice *self); + +void traits_main(void); + +#if defined(__cplusplus) +} +#endif + +#define __traits_H_DEFINED +#endif diff --git a/out/test-where_clauses_closures/where_clauses_closures.c b/out/test-where_clauses_closures/where_clauses_closures.c new file mode 100644 index 0000000..0818499 --- /dev/null +++ b/out/test-where_clauses_closures/where_clauses_closures.c @@ -0,0 +1,73 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#include "where_clauses_closures.h" + +/** +This function found in impl {(where_clauses_closures::Ops<1: usize> for usize)} +*/ +size_t where_clauses_closures_zero_d6(void) +{ + return (size_t)0U; +} + +/** +This function found in impl {(where_clauses_closures::Ops<1: usize> for usize)} +*/ +size_t where_clauses_closures_of_usize_d6(size_t x) +{ + return x; +} + +/** +A monomorphic instance of where_clauses_closures.test.closure +with types size_t +with const generics +- K= 1 +*/ +size_t where_clauses_closures_test_closure_e3(size_t i) +{ + return where_clauses_closures_of_usize_d6(i); +} + +/** +A monomorphic instance of where_clauses_closures.test +with types size_t +with const generics +- K= 1 +*/ +size_t_x2 where_clauses_closures_test_e3(void) +{ + size_t x[1U]; + { + x[0U] = where_clauses_closures_of_usize_d6((size_t)0U); + } + size_t y = where_clauses_closures_zero_d6(); + size_t_x2 lit; + lit.fst = x[0U]; + lit.snd = y; + return lit; +} + +typedef struct _size_t__x2_s +{ + size_t *fst; + size_t *snd; +} +_size_t__x2; + +void where_clauses_closures_main(void) +{ + size_t_x2 uu____0 = where_clauses_closures_test_e3(); + size_t x = uu____0.fst; + size_t y = uu____0.snd; + _size_t__x2 uu____1 = { .fst = &x, .snd = &y }; + size_t *left_val = uu____1.fst; + size_t *right_val = uu____1.snd; + EURYDICE_ASSERT(left_val[0U] == right_val[0U], "panic!"); +} + diff --git a/out/test-where_clauses_closures/where_clauses_closures.h b/out/test-where_clauses_closures/where_clauses_closures.h new file mode 100644 index 0000000..93210eb --- /dev/null +++ b/out/test-where_clauses_closures/where_clauses_closures.h @@ -0,0 +1,65 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#ifndef __where_clauses_closures_H +#define __where_clauses_closures_H + +#if defined(__cplusplus) +extern "C" { +#endif + +#include "eurydice_glue.h" + +extern size_t core_clone_impls___core__clone__Clone_for_usize__5__clone(size_t *x0); + +#define core_panicking_AssertKind_Eq 0 +#define core_panicking_AssertKind_Ne 1 +#define core_panicking_AssertKind_Match 2 + +typedef uint8_t core_panicking_AssertKind; + +/** +This function found in impl {(where_clauses_closures::Ops<1: usize> for usize)} +*/ +size_t where_clauses_closures_zero_d6(void); + +/** +This function found in impl {(where_clauses_closures::Ops<1: usize> for usize)} +*/ +size_t where_clauses_closures_of_usize_d6(size_t x); + +/** +A monomorphic instance of where_clauses_closures.test.closure +with types size_t +with const generics +- K= 1 +*/ +size_t where_clauses_closures_test_closure_e3(size_t i); + +typedef struct size_t_x2_s +{ + size_t fst; + size_t snd; +} +size_t_x2; + +/** +A monomorphic instance of where_clauses_closures.test +with types size_t +with const generics +- K= 1 +*/ +size_t_x2 where_clauses_closures_test_e3(void); + +void where_clauses_closures_main(void); + +#if defined(__cplusplus) +} +#endif + +#define __where_clauses_closures_H_DEFINED +#endif diff --git a/out/test-where_clauses_fncg/where_clauses_fncg.c b/out/test-where_clauses_fncg/where_clauses_fncg.c new file mode 100644 index 0000000..86d4102 --- /dev/null +++ b/out/test-where_clauses_fncg/where_clauses_fncg.c @@ -0,0 +1,55 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#include "where_clauses_fncg.h" + +/** +This function found in impl {(where_clauses_fncg::Foo for u64)} +*/ +/** +A monomorphic instance of where_clauses_fncg.bar_ea +with const generics +- K= 8 +- L= 4 +*/ +uint64_t where_clauses_fncg_bar_ea_7b(uint8_t x[8U][4U], uint8_t _[4U][8U]) +{ + return (uint64_t)x[0U][0U]; +} + +/** +A monomorphic instance of where_clauses_fncg.f +with types uint64_t +with const generics +- K= 6 +- L= 8 +- M= 10 +*/ +uint64_t where_clauses_fncg_f_43(void) +{ + uint8_t buf0[8U][4U] = { { 0U } }; + uint8_t buf[4U][8U] = { { 0U } }; + return where_clauses_fncg_bar_ea_7b(buf0, buf); +} + +typedef struct _uint64_t__x2_s +{ + uint64_t *fst; + uint64_t *snd; +} +_uint64_t__x2; + +void where_clauses_fncg_main(void) +{ + uint64_t r = where_clauses_fncg_f_43(); + uint64_t expected = 0ULL; + _uint64_t__x2 uu____0 = { .fst = &r, .snd = &expected }; + uint64_t *left_val = uu____0.fst; + uint64_t *right_val = uu____0.snd; + EURYDICE_ASSERT(left_val[0U] == right_val[0U], "panic!"); +} + diff --git a/out/test-where_clauses_fncg/where_clauses_fncg.h b/out/test-where_clauses_fncg/where_clauses_fncg.h new file mode 100644 index 0000000..85b01ad --- /dev/null +++ b/out/test-where_clauses_fncg/where_clauses_fncg.h @@ -0,0 +1,54 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#ifndef __where_clauses_fncg_H +#define __where_clauses_fncg_H + +#if defined(__cplusplus) +extern "C" { +#endif + +#include "eurydice_glue.h" + +static inline uint64_t +core_convert_num___core__convert__From_u8__for_u64__66__from(uint8_t x0); + +#define core_panicking_AssertKind_Eq 0 +#define core_panicking_AssertKind_Ne 1 +#define core_panicking_AssertKind_Match 2 + +typedef uint8_t core_panicking_AssertKind; + +/** +This function found in impl {(where_clauses_fncg::Foo for u64)} +*/ +/** +A monomorphic instance of where_clauses_fncg.bar_ea +with const generics +- K= 8 +- L= 4 +*/ +uint64_t where_clauses_fncg_bar_ea_7b(uint8_t x[8U][4U], uint8_t _[4U][8U]); + +/** +A monomorphic instance of where_clauses_fncg.f +with types uint64_t +with const generics +- K= 6 +- L= 8 +- M= 10 +*/ +uint64_t where_clauses_fncg_f_43(void); + +void where_clauses_fncg_main(void); + +#if defined(__cplusplus) +} +#endif + +#define __where_clauses_fncg_H_DEFINED +#endif diff --git a/out/test-where_clauses_simple/where_clauses_simple.c b/out/test-where_clauses_simple/where_clauses_simple.c new file mode 100644 index 0000000..ad4ab29 --- /dev/null +++ b/out/test-where_clauses_simple/where_clauses_simple.c @@ -0,0 +1,245 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#include "where_clauses_simple.h" + +/** +This function found in impl {(where_clauses_simple::Ops for usize)#1} +*/ +/** +A monomorphic instance of where_clauses_simple.of_u16_56 +with const generics +- K= 3 +*/ +size_t where_clauses_simple_of_u16_56_e0(uint16_t x) +{ + return (size_t)x; +} + +/** +This function found in impl {(where_clauses_simple::Ops for usize)#1} +*/ +/** +A monomorphic instance of where_clauses_simple.add_56 +with const generics +- K= 3 +*/ +size_t where_clauses_simple_add_56_e0(uint16_t x[3U], size_t y) +{ + return (size_t)x[0U] + y + (size_t)3U; +} + +/** +A monomorphic instance of where_clauses_simple.fn_k +with types size_t +with const generics +- K= 3 +*/ +size_t where_clauses_simple_fn_k_71(void) +{ + size_t x = where_clauses_simple_of_u16_56_e0(0U); + uint16_t buf[3U] = { 0U }; + return where_clauses_simple_add_56_e0(buf, x); +} + +typedef struct _size_t__x2_s +{ + size_t *fst; + size_t *snd; +} +_size_t__x2; + +void where_clauses_simple_k_calls_k(void) +{ + size_t r = where_clauses_simple_fn_k_71(); + size_t r_expected = (size_t)3U; + _size_t__x2 uu____0 = { .fst = &r, .snd = &r_expected }; + size_t *left_val = uu____0.fst; + size_t *right_val = uu____0.snd; + EURYDICE_ASSERT(left_val[0U] == right_val[0U], "panic!"); +} + +/** +This function found in impl {(where_clauses_simple::Ops<1: usize> for u64)} +*/ +uint64_t where_clauses_simple_add_d9(uint16_t x[1U], uint64_t y) +{ + return (uint64_t)x[0U] + y; +} + +/** +This function found in impl {(where_clauses_simple::Ops<1: usize> for u64)} +*/ +uint64_t where_clauses_simple_of_u16_d9(uint16_t x) +{ + return (uint64_t)x; +} + +/** +A monomorphic instance of where_clauses_simple.fn_k +with types uint64_t +with const generics +- K= 1 +*/ +uint64_t where_clauses_simple_fn_k_3a(void) +{ + uint64_t x = where_clauses_simple_of_u16_d9(0U); + uint16_t buf[1U] = { 0U }; + return where_clauses_simple_add_d9(buf, x); +} + +typedef struct _uint64_t__x2_s +{ + uint64_t *fst; + uint64_t *snd; +} +_uint64_t__x2; + +void where_clauses_simple_k_calls_one(void) +{ + uint64_t r = where_clauses_simple_fn_k_3a(); + uint64_t r_expected = 0ULL; + _uint64_t__x2 uu____0 = { .fst = &r, .snd = &r_expected }; + uint64_t *left_val = uu____0.fst; + uint64_t *right_val = uu____0.snd; + EURYDICE_ASSERT(left_val[0U] == right_val[0U], "panic!"); +} + +/** +This function found in impl {(where_clauses_simple::Ops for usize)#1} +*/ +/** +A monomorphic instance of where_clauses_simple.of_u16_56 +with const generics +- K= 1 +*/ +size_t where_clauses_simple_of_u16_56_74(uint16_t x) +{ + return (size_t)x; +} + +/** +This function found in impl {(where_clauses_simple::Ops for usize)#1} +*/ +/** +A monomorphic instance of where_clauses_simple.add_56 +with const generics +- K= 1 +*/ +size_t where_clauses_simple_add_56_74(uint16_t x[1U], size_t y) +{ + return (size_t)x[0U] + y + (size_t)1U; +} + +/** +A monomorphic instance of where_clauses_simple.fn_1 +with types size_t +with const generics + +*/ +size_t where_clauses_simple_fn_1_e6(void) +{ + size_t x = where_clauses_simple_of_u16_56_74(0U); + uint16_t buf[1U] = { 0U }; + return where_clauses_simple_add_56_74(buf, x); +} + +void where_clauses_simple_one_calls_k(void) +{ + size_t r = where_clauses_simple_fn_1_e6(); + size_t r_expected = (size_t)1U; + _size_t__x2 uu____0 = { .fst = &r, .snd = &r_expected }; + size_t *left_val = uu____0.fst; + size_t *right_val = uu____0.snd; + EURYDICE_ASSERT(left_val[0U] == right_val[0U], "panic!"); +} + +/** +A monomorphic instance of where_clauses_simple.fn_1 +with types uint64_t +with const generics + +*/ +uint64_t where_clauses_simple_fn_1_6f(void) +{ + uint64_t x = where_clauses_simple_of_u16_d9(0U); + uint16_t buf[1U] = { 0U }; + return where_clauses_simple_add_d9(buf, x); +} + +void where_clauses_simple_one_calls_one(void) +{ + uint64_t r = where_clauses_simple_fn_1_6f(); + uint64_t r_expected = 0ULL; + _uint64_t__x2 uu____0 = { .fst = &r, .snd = &r_expected }; + uint64_t *left_val = uu____0.fst; + uint64_t *right_val = uu____0.snd; + EURYDICE_ASSERT(left_val[0U] == right_val[0U], "panic!"); +} + +/** +A monomorphic instance of where_clauses_simple.double +with types uint64_t, size_t +with const generics + +*/ +tuple_65 where_clauses_simple_double_47(uint64_t x, size_t y) +{ + tuple_65 lit; + uint16_t buf[1U] = { 0U }; + lit.fst = where_clauses_simple_add_d9(buf, x); + uint16_t buf0[1U] = { 0U }; + lit.snd = where_clauses_simple_add_56_74(buf0, y); + return lit; +} + +/** +A monomorphic instance of where_clauses_simple.double_k +with types size_t, uint64_t +with const generics +- K= 3 +*/ +tuple_b6 where_clauses_simple_double_k_7b(size_t x, uint64_t y) +{ + tuple_b6 lit; + uint16_t buf[3U] = { 0U }; + lit.fst = where_clauses_simple_add_56_e0(buf, x); + uint16_t buf0[1U] = { 0U }; + lit.snd = where_clauses_simple_add_d9(buf0, y); + return lit; +} + +void where_clauses_simple_main(void) +{ + where_clauses_simple_k_calls_k(); + where_clauses_simple_k_calls_one(); + where_clauses_simple_one_calls_k(); + where_clauses_simple_one_calls_one(); + tuple_65 x = where_clauses_simple_double_47(1ULL, (size_t)1U); + tuple_b6 y = where_clauses_simple_double_k_7b((size_t)1U, 1ULL); + uint64_t x_0 = 1ULL; + size_t x_1 = (size_t)2U; + _uint64_t__x2 uu____0 = { .fst = &x.fst, .snd = &x_0 }; + uint64_t *left_val0 = uu____0.fst; + uint64_t *right_val0 = uu____0.snd; + EURYDICE_ASSERT(left_val0[0U] == right_val0[0U], "panic!"); + _size_t__x2 uu____1 = { .fst = &x.snd, .snd = &x_1 }; + size_t *left_val1 = uu____1.fst; + size_t *right_val1 = uu____1.snd; + EURYDICE_ASSERT(left_val1[0U] == right_val1[0U], "panic!"); + size_t y_0 = (size_t)4U; + uint64_t y_1 = 1ULL; + _size_t__x2 uu____2 = { .fst = &y.fst, .snd = &y_0 }; + size_t *left_val2 = uu____2.fst; + size_t *right_val2 = uu____2.snd; + EURYDICE_ASSERT(left_val2[0U] == right_val2[0U], "panic!"); + _uint64_t__x2 uu____3 = { .fst = &y.snd, .snd = &y_1 }; + uint64_t *left_val = uu____3.fst; + uint64_t *right_val = uu____3.snd; + EURYDICE_ASSERT(left_val[0U] == right_val[0U], "panic!"); +} + diff --git a/out/test-where_clauses_simple/where_clauses_simple.h b/out/test-where_clauses_simple/where_clauses_simple.h new file mode 100644 index 0000000..0cd2297 --- /dev/null +++ b/out/test-where_clauses_simple/where_clauses_simple.h @@ -0,0 +1,170 @@ +/* + This file was generated by KaRaMeL + + F* version: + + */ + +#ifndef __where_clauses_simple_H +#define __where_clauses_simple_H + +#if defined(__cplusplus) +extern "C" { +#endif + +#include "eurydice_glue.h" + +extern uint64_t core_clone_impls___core__clone__Clone_for_u64__9__clone(uint64_t *x0); + +extern size_t core_clone_impls___core__clone__Clone_for_usize__5__clone(size_t *x0); + +static inline uint64_t +core_convert_num___core__convert__From_u16__for_u64__70__from(uint16_t x0); + +static inline size_t +core_convert_num___core__convert__From_u16__for_usize__96__from(uint16_t x0); + +#define core_panicking_AssertKind_Eq 0 +#define core_panicking_AssertKind_Ne 1 +#define core_panicking_AssertKind_Match 2 + +typedef uint8_t core_panicking_AssertKind; + +/** +This function found in impl {(where_clauses_simple::Ops for usize)#1} +*/ +/** +A monomorphic instance of where_clauses_simple.of_u16_56 +with const generics +- K= 3 +*/ +size_t where_clauses_simple_of_u16_56_e0(uint16_t x); + +/** +This function found in impl {(where_clauses_simple::Ops for usize)#1} +*/ +/** +A monomorphic instance of where_clauses_simple.add_56 +with const generics +- K= 3 +*/ +size_t where_clauses_simple_add_56_e0(uint16_t x[3U], size_t y); + +/** +A monomorphic instance of where_clauses_simple.fn_k +with types size_t +with const generics +- K= 3 +*/ +size_t where_clauses_simple_fn_k_71(void); + +void where_clauses_simple_k_calls_k(void); + +/** +This function found in impl {(where_clauses_simple::Ops<1: usize> for u64)} +*/ +uint64_t where_clauses_simple_add_d9(uint16_t x[1U], uint64_t y); + +/** +This function found in impl {(where_clauses_simple::Ops<1: usize> for u64)} +*/ +uint64_t where_clauses_simple_of_u16_d9(uint16_t x); + +/** +A monomorphic instance of where_clauses_simple.fn_k +with types uint64_t +with const generics +- K= 1 +*/ +uint64_t where_clauses_simple_fn_k_3a(void); + +void where_clauses_simple_k_calls_one(void); + +/** +This function found in impl {(where_clauses_simple::Ops for usize)#1} +*/ +/** +A monomorphic instance of where_clauses_simple.of_u16_56 +with const generics +- K= 1 +*/ +size_t where_clauses_simple_of_u16_56_74(uint16_t x); + +/** +This function found in impl {(where_clauses_simple::Ops for usize)#1} +*/ +/** +A monomorphic instance of where_clauses_simple.add_56 +with const generics +- K= 1 +*/ +size_t where_clauses_simple_add_56_74(uint16_t x[1U], size_t y); + +/** +A monomorphic instance of where_clauses_simple.fn_1 +with types size_t +with const generics + +*/ +size_t where_clauses_simple_fn_1_e6(void); + +void where_clauses_simple_one_calls_k(void); + +/** +A monomorphic instance of where_clauses_simple.fn_1 +with types uint64_t +with const generics + +*/ +uint64_t where_clauses_simple_fn_1_6f(void); + +void where_clauses_simple_one_calls_one(void); + +/** +A monomorphic instance of K. +with types uint64_t, size_t + +*/ +typedef struct tuple_65_s +{ + uint64_t fst; + size_t snd; +} +tuple_65; + +/** +A monomorphic instance of where_clauses_simple.double +with types uint64_t, size_t +with const generics + +*/ +tuple_65 where_clauses_simple_double_47(uint64_t x, size_t y); + +/** +A monomorphic instance of K. +with types size_t, uint64_t + +*/ +typedef struct tuple_b6_s +{ + size_t fst; + uint64_t snd; +} +tuple_b6; + +/** +A monomorphic instance of where_clauses_simple.double_k +with types size_t, uint64_t +with const generics +- K= 3 +*/ +tuple_b6 where_clauses_simple_double_k_7b(size_t x, uint64_t y); + +void where_clauses_simple_main(void); + +#if defined(__cplusplus) +} +#endif + +#define __where_clauses_simple_H_DEFINED +#endif From 295a4b656fb891f572ef3589488e8744473ab733 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 10 Jan 2025 14:58:09 +0100 Subject: [PATCH 2/3] Check test outputs in CI --- flake.nix | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/flake.nix b/flake.nix index d9c3b70..7de8e4b 100644 --- a/flake.nix +++ b/flake.nix @@ -73,7 +73,24 @@ cp --no-preserve=mode,ownership -rf ${inputs.charon.sourceInfo.outPath} ./charon export CHARON_HOME=./charon + # Move the committed test outputs out of the way + mv out out-comitted + + # Run the tests make -o all test + + # Clean generated files that we don't want to compare. + rm out/**/a.out + + # Check that there are no differences between the generated + # outputs and the committed outputs. + if diff -rq out-comitted out; then + echo "Ok: the regenerated files are the same as the checked out files" + else + echo "Error: the regenerated files differ from the checked out files" + diff -ru out-comitted out + exit 1 + fi ''; installPhase = ''touch $out''; }; From 0225fbd1ca5edfc1f0b253ac821a3f8ecb77156d Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 13 Jan 2025 14:06:43 +0100 Subject: [PATCH 3/3] Address review --- Makefile | 5 +++-- flake.nix | 1 + 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/Makefile b/Makefile index 9f01a5c..308b968 100644 --- a/Makefile +++ b/Makefile @@ -8,6 +8,7 @@ TEST_DIRS = $(filter-out $(BROKEN_TESTS),$(subst test/,,$(shell find test -maxd # Enable `foo/**` glob syntax SHELL := bash -O globstar +SED=$(shell which gsed &>/dev/null && echo gsed || echo sed) .PHONY: all all: format-check @@ -39,8 +40,8 @@ test-symcrust: CFLAGS += -Wno-unused-function test-%: test/%/out.llbc out/test-%/main.c | all $(EURYDICE) $(EXTRA) --output out/test-$* $< - sed -i 's/ KaRaMeL version: .*//' out/test-$*/**/*.{c,h} # This changes on every commit - sed -i 's/ KaRaMeL invocation: .*//' out/test-$*/**/*.{c,h} # This changes between local and CI + $(SED) -i 's/ KaRaMeL version: .*//' out/test-$*/**/*.{c,h} # This changes on every commit + $(SED) -i 's/ KaRaMeL invocation: .*//' out/test-$*/**/*.{c,h} # This changes between local and CI cd out/test-$* && $(CC) $(CFLAGS) -I. -I../../include $(EXTRA_C) $*.c main.c && ./a.out custom-test-array: test-array diff --git a/flake.nix b/flake.nix index 7de8e4b..d27b74c 100644 --- a/flake.nix +++ b/flake.nix @@ -67,6 +67,7 @@ buildInputs = [ charon.buildInputs eurydice ]; nativeBuildInputs = [ charon.nativeBuildInputs clang ]; buildPhase = '' + shopt -s globstar export CHARON="${charon}/bin/charon" # setup CHARON_HOME: it is expected to be writtable, hence the `cp --no-preserve`