Split headers into logical units

.gitignore

@@ -8,7 +8,7 @@ out/*/a.out
 *.DS_Store
 *.orig
 *.llbc
-eurydice
+./eurydice
 /.vscode
 .charon_version
 

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:

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;

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

cremepat/Parse.mly

@@ -3,7 +3,7 @@
 %}
 
 %token<int>     INT
-%token<string>  UIDENT LIDENT UVAR UVARLIST
+%token<string>  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

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"

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 <stdbool.h>
+// Eurydice may emit the KRML_FOR_* series of macros
+#include <krml/internal/target.h>
+
+#include <stdio.h>
+
+// 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

include/eurydice/core.h

@@ -0,0 +1,215 @@
+#pragma once
+
+#include <inttypes.h>
+#include <stdlib.h>
+#include <string.h>
+
+#include "krml/lowstar_endianness.h"
+
+#ifdef _MSC_VER
+// For __popcnt
+#include <intrin.h>
+#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<T> 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
+

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 <utility>
+
+#ifndef __cpp_lib_type_identity
+template <class T> struct type_identity {
+  using type = T;
+};
+
+template <class T> using type_identity_t = typename type_identity<T>::type;
+#else
+using std::type_identity_t;
+#endif
+
+#define KRML_UNION_CONSTRUCTOR(T)                                              \
+  template <typename V>                                                        \
+  constexpr T(int t, V U::*m, type_identity_t<V> v) : tag(t) {                 \
+    val.*m = std::move(v);                                                     \
+  }                                                                            \
+  T() = default;
+
+#endif