Explicit Unsized Metadata & Unified DST Handling

.charon_version

@@ -1 +1 @@
-0.1.123
+0.1.132

.gitignore

@@ -8,3 +8,4 @@ out/*/a.out
 *.llbc
 eurydice
 /.vscode
+.charon_version

Makefile

@@ -119,15 +119,11 @@ FORMAT_FILE=include/eurydice_glue.h
 
 .PHONY: format-check
 format-check:
-	@if ! dune build @fmt >/dev/null 2>&1; then \echo "\033[0;31m⚠️⚠️⚠️ SUGGESTED: $(MAKE) format-apply\033[0;m"; fi
-	@F=$$(mktemp); clang-format $(FORMAT_FILE) > $$F; \
-	  if ! diff -q $(FORMAT_FILE) $$F >/dev/null; then \echo "\033[0;31m⚠️⚠️⚠️ SUGGESTED: $(MAKE) format-apply\033[0;m"; fi; \
-	  rm -rf $$F
+	FORMAT_FILE=$(FORMAT_FILE) ./scripts/format.sh check
 
-.PHONY: format-check
+.PHONY: format-apply
 format-apply:
-	dune fmt >/dev/null || true
-	clang-format -i $(FORMAT_FILE)
+	FORMAT_FILE=$(FORMAT_FILE) ./scripts/format.sh apply
 
 .PHONY: clean-llbc
 clean-llbc:

bin/main.ml

@@ -111,7 +111,6 @@ Supported options:|}
         [ "Eurydice" ], "slice_len";
         [ "Eurydice" ], "slice_copy";
         [ "Eurydice" ], "array_eq";
-        [ "Eurydice" ], "slice_to_array2";
       ]);
 
   (* Some logic for more precisely tracking readonly functions, so as to remove
@@ -258,7 +257,6 @@ Supported options:|}
   Eurydice.Logging.log "Phase2.25" "%a" pfiles files;
   let files = Eurydice.Cleanup2.remove_array_repeats#visit_files false files in
   Eurydice.Logging.log "Phase2.26" "%a" pfiles files;
-  let files = Eurydice.Cleanup2.rewrite_slice_to_array#visit_files () files in
   let ((map, _, _) as map3), files = Krml.DataTypes.everything files in
   Eurydice.Cleanup2.fixup_monomorphization_map map;
   let files = Eurydice.Cleanup2.remove_discriminant_reads map3 files in
@@ -313,7 +311,7 @@ Supported options:|}
   Eurydice.Cleanup3.(also_skip_prefix_for_external_types scope_env)#visit_files () files;
   let files = Eurydice.Cleanup3.decay_cg_externals#visit_files (scope_env, false) files in
   let files = Eurydice.Cleanup3.add_extra_type_to_slice_index#visit_files () files in
-  let files = Eurydice.Cleanup3.remove_builtin_decls files in  
+  let files = Eurydice.Cleanup3.remove_builtin_decls files in
   Eurydice.Logging.log "Phase3.1" "%a" pfiles files;
   let c_name_map = Krml.GlobalNames.mapping (fst scope_env) in
 
@@ -392,7 +390,6 @@ Supported options:|}
   (*   print_endline (CStar.show_program p ); *)
   (*   print_endline "" *)
   (* ) files; *)
-
   let headers = CStarToC11.mk_headers c_name_map files in
   let deps = CStarToC11.drop_empty_headers deps headers in
   let internal_headers =

cremepat/ParseTree.ml

@@ -3,13 +3,7 @@ type pre_expr =
   (* Binding most loosely *)
   | Let of string * expr * expr
   | Sequence of expr list
-  | App of {
-    head: expr;
-    cgs: expr list;
-    methods: expr list;
-    ts: typ list;
-    args: expr list;
-  }
+  | App of { head : expr; cgs : expr list; methods : expr list; ts : typ list; args : expr list }
   | Addr of expr
   | Index of expr * expr
   (* Atomic -- we terminate matches and loops using braces, we are not barbarians. *)

flake.nix

@@ -104,7 +104,27 @@
         };
         inherit charon karamel;
       };
-      checks.default = packages.default.tests;
+      checks = {
+        default = packages.default.tests;
+        format = pkgs.runCommand "format-check"
+          {
+            src = ./.;
+            nativeBuildInputs = [
+              pkgs.bash
+              pkgs.gnumake
+              pkgs.clang-tools_18 # For clang-format
+              pkgs.ocamlPackages.ocaml
+              pkgs.ocamlPackages.ocamlformat_0_27_0
+              pkgs.ocamlPackages.dune_3
+            ];
+          } ''
+          cp -r $src src
+          chmod u+w src
+          cd src
+          bash ./scripts/format.sh check
+          touch $out
+        '';
+      };
       devShells.ci = pkgs.mkShell { packages = [ pkgs.jq ]; };
       devShells.default = (pkgs.mkShell.override { stdenv = pkgs.clangStdenv; }) {
         OCAMLRUNPARAM = "b"; # Get backtrace on exception
@@ -116,6 +136,7 @@
           # ocaml-lsp's version must match the ocaml version used. Pinning
           # this here to save me a headache.
           pkgs.ocamlPackages.ocaml-lsp
+          pkgs.rustup
         ];
         buildInputs = [ charon.buildInputs ];
         nativeBuildInputs = [ charon.nativeBuildInputs fstar pkgs.clang ];