Commit test output

.gitignore

@@ -1,8 +1,8 @@
 _build
 lib/krml
 lib/charon
-out
 test/*/target
+out/*/a.out
 *.DS_Store
 *.orig
 *.llbc

Makefile

@@ -6,6 +6,10 @@ 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 
+SED=$(shell which gsed &>/dev/null && echo gsed || echo sed)
+
 .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 +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
 	cd out/test-$* && $(CC) $(CFLAGS) -I. -I../../include $(EXTRA_C) $*.c main.c && ./a.out
 
 custom-test-array: test-array

flake.nix

@@ -67,13 +67,31 @@
                 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`
                   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'';
               };

out/test-array/array.c

@@ -0,0 +1,112 @@
+/* 
+  This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
+
+  F* version: <unknown>
+
+ */
+
+#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!");
+}
+

out/test-array/array.h

@@ -0,0 +1,59 @@
+/* 
+  This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
+
+  F* version: <unknown>
+
+ */
+
+#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

out/test-array2d/array2d.c

@@ -0,0 +1,54 @@
+/* 
+  This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
+
+  F* version: <unknown>
+
+ */
+
+#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!");
+}
+

out/test-array2d/array2d.h

@@ -0,0 +1,38 @@
+/* 
+  This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
+
+  F* version: <unknown>
+
+ */
+
+#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

out/test-const_generics/Eurydice.h

@@ -0,0 +1,36 @@
+/* 
+  This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
+
+  F* version: <unknown>
+
+ */
+
+#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