Support for trait clause bounds

Makefile

@@ -1,10 +1,10 @@
 CHARON_HOME 	?= $(dir $(abspath $(lastword $(MAKEFILE_LIST))))/../charon
-KRML_HOME 		?= $(dir $(abspath $(lastword $(MAKEFILE_LIST))))/../karamel
+KRML_HOME 	?= $(dir $(abspath $(lastword $(MAKEFILE_LIST))))/../karamel
 EURYDICE	?= ./eurydice $(EURYDICE_FLAGS)
 CHARON		?= $(CHARON_HOME)/bin/charon
 
-CHARON_TEST_FILES	= arrays
-TEST_DIRS		= array const_generics traits array2d int_switch nested_arrays # step_by
+BROKEN_TESTS		= step_by where_clauses chunks mutable_slice_range
+TEST_DIRS		= $(filter-out $(BROKEN_TESTS),$(subst test/,,$(shell find test -maxdepth 1 -mindepth 1 -type d)))
 
 .PHONY: all
 all:
@@ -14,21 +14,8 @@ all:
 
 CFLAGS		:= -Wall -Werror -Wno-unused-variable $(CFLAGS) -I$(KRML_HOME)/include
 
-test: $(addprefix charon-test-,$(CHARON_TEST_FILES)) $(addprefix test-,$(TEST_DIRS))
+test: $(addprefix test-,$(TEST_DIRS))
 
-# Tests relying on Charon's test infrastructure
-
-$(CHARON_HOME)/tests/llbc/%.llbc: $(CHARON_HOME)/tests/src/%.rs
-	RUST_BACKTRACE=1 $(MAKE) -C $(CHARON_HOME)/tests test-$*
-
-.PRECIOUS: $(CHARON_HOME)/tests/llbc/%.llbc
-charon-test-%: $(CHARON_HOME)/tests/llbc/%.llbc | out/test-% all
-	mkdir -p out/charon-test-$*
-	$(EURYDICE) --output out/charon-test-$* $<
-	# These tests do not have a main
-	cd out/charon-test-$* && $(CC) $(CFLAGS) -I. -I../../include $*.c -c
-
-# Tests checked into the current repository
 .PHONY: phony
 .PRECIOUS: test/%/out.llbc
 test/%/out.llbc: phony
@@ -38,9 +25,12 @@ out/test-%/main.c: test/main.c
 	mkdir -p out/test-$*
 	sed 's/__NAME__/$*/g' $< > $@
 
+test-partial_eq: EXTRA_C = ../../test/partial_eq/stubs.c
+test-nested_arrays: EXTRA = -funroll-loops 0
+
 test-%: test/%/out.llbc out/test-%/main.c | all
-	$(EURYDICE) --output out/test-$* $<
-	cd out/test-$* && $(CC) $(CFLAGS) -I. -I../../include $*.c main.c && ./a.out
+	$(EURYDICE) $(EXTRA) --output out/test-$* $<
+	cd out/test-$* && $(CC) $(CFLAGS) -I. -I../../include $(EXTRA_C) $*.c main.c && ./a.out
 
 .PRECIOUS: out/%
 out/%:

bin/main.ml

@@ -12,11 +12,13 @@ Supported options:|}
   in
   let module O = Eurydice.Options in
   let debug s = Krml.Options.debug_modules := Krml.KString.split_on_char ',' s @ !Krml.Options.debug_modules in
+  let funroll_loops = ref 16 in
   let spec = [
     "--log", Arg.Set_string O.log_level, " log level, use * for everything";
     "--debug", Arg.String debug, " debug options, to be passed to krml";
     "--output", Arg.Set_string Krml.Options.tmpdir, " output directory in which to write files";
     "--config", Arg.Set_string O.config, " YAML configuration file";
+    "-funroll-loops", Arg.Set_int funroll_loops, " unrool loops up to N";
   ] in
   let spec = Arg.align spec in
   let files = ref [] in
@@ -38,10 +40,14 @@ Supported options:|}
   if !files = [] then
     fatal_error "%s" (Arg.usage_string spec usage);
 
-  let terminal_width = (* Terminal.Size.(match get_dimensions () with Some d -> d.columns | None -> 80) *) 100 in
+  let terminal_width = Terminal.Size.(match get_dimensions () with Some d -> d.columns | None -> 80) in
   let pfiles b files =
     PPrint.(ToBuffer.pretty 0.95 terminal_width b (Krml.PrintAst.print_files files ^^ hardline))
   in
+  let fail file line =
+    Printf.printf "%s:%d exiting" file line;
+    exit 1
+  in
 
   (* This is where the action happens *)
   Eurydice.Logging.enable_logging !O.log_level;
@@ -56,6 +62,7 @@ Supported options:|}
     parentheses := true;
     no_shadow := true;
     extern_c := true;
+    unroll_loops := !funroll_loops;
     static_header := [
       Bundle.Prefix [ "core"; "convert" ];
       Bundle.Prefix [ "core"; "num" ];
@@ -76,10 +83,10 @@ Supported options:|}
             false
     );
 
-  let files = Eurydice.Builtin.files @ List.map (fun filename ->
+  let files = Eurydice.Builtin.files @ [ Eurydice.PreCleanup.merge (List.map (fun filename ->
     let llbc = Eurydice.LoadLlbc.load_file filename in
     Eurydice.Builtin.adjust (Eurydice.AstOfLlbc.file_of_crate llbc)
-  ) !files in
+  ) !files) ] in
   Eurydice.Builtin.check ();
 
   Printf.printf "1️⃣ LLBC ➡️  AST\n";
@@ -88,74 +95,98 @@ Supported options:|}
   Eurydice.Logging.log "Phase1" "%a" pfiles files;
   let errors, files = Krml.Checker.check_everything ~warn:true files in
   if errors then
-    exit 1;
+    fail __FILE__ __LINE__;
 
   Printf.printf "2️⃣ Cleanup\n";
-  let files =
+  let config =
     if !O.config = "" then
-      files
+      None
     else
-      let config = Eurydice.Bundles.load_config !O.config in
-      let config = Eurydice.Bundles.parse_config config in
-      let files = Eurydice.Bundles.bundle files config in
-      let files = Krml.Bundles.topological_sort files in
-      Krml.KPrint.bprintf "File order after topological sort: %s\n"
-        (String.concat ", " (List.map fst files));
-      files
+      Some (Eurydice.Bundles.parse_config (Eurydice.Bundles.load_config !O.config))
+  in
+  let files =
+    match config with
+    | None -> files
+    | Some config ->
+        let config = config in
+        let files = Eurydice.Bundles.bundle files config in
+        let files = Eurydice.Bundles.libraries files in
+        let files = Krml.Bundles.topological_sort files in
+        Krml.KPrint.bprintf "File order after topological sort: %s\n"
+          (String.concat ", " (List.map fst files));
+        files
   in
   let files = Eurydice.Cleanup1.cleanup files in
 
   Eurydice.Logging.log "Phase2" "%a" pfiles files;
   let errors, files = Krml.Checker.check_everything ~warn:true files in
   if errors then
-    exit 1;
+    fail __FILE__ __LINE__;
 
   Printf.printf "3️⃣ Monomorphization, datatypes\n";
   let files = Eurydice.Cleanup2.resugar_loops#visit_files () files in
   (* Sanity check for the big rewriting above. *)
   let errors, files = Krml.Checker.check_everything ~warn:true files in
   if errors then
-    exit 1;
+    fail __FILE__ __LINE__;
   Eurydice.Logging.log "Phase2.1" "%a" pfiles files;
   let files = Krml.Monomorphization.functions files in
   let files = Krml.Monomorphization.datatypes files in
+  let files =
+    match config with
+    | None -> files
+    | Some config ->
+        let files = Eurydice.Bundles.reassign_monomorphizations files config in
+        Eurydice.Logging.log "Phase2.15" "%a" pfiles files;
+        let files = Krml.Bundles.topological_sort files in
+        files
+  in
   Eurydice.Logging.log "Phase2.2" "%a" pfiles files;
+  (* Sanity check for the big rewriting above. *)
+  let errors, files = Krml.Checker.check_everything ~warn:true files in
+  if errors then
+    fail __FILE__ __LINE__;
   let files = Krml.Inlining.drop_unused files in
-  Eurydice.Logging.log "Phase2.3" "%a" pfiles files;
   let files = Eurydice.Cleanup2.remove_array_temporaries#visit_files () files in
   let files = Eurydice.Cleanup2.remove_array_repeats#visit_files () files in
   let files = Eurydice.Cleanup2.rewrite_slice_to_array#visit_files () files in
   let files = Krml.DataTypes.simplify files in
   let files = Krml.DataTypes.optimize files in
   let _, files = Krml.DataTypes.everything files in
+  Eurydice.Logging.log "Phase2.3" "%a" pfiles files;
   let files = Eurydice.Cleanup2.remove_trivial_ite#visit_files () files in
+  Eurydice.Logging.log "Phase2.4" "%a" pfiles files;
   let files = Eurydice.Cleanup2.remove_trivial_into#visit_files () files in
   let files = Krml.Structs.pass_by_ref files in
+  Eurydice.Logging.log "Phase2.5" "%a" pfiles files;
+  let files = Eurydice.Cleanup2.detect_array_returning_builtins#visit_files () files in
   let files = Eurydice.Cleanup2.remove_literals#visit_files () files in
   let files = Krml.Simplify.optimize_lets files in
   (* let files = Eurydice.Cleanup2.break_down_nested_arrays#visit_files () files in *)
+  Eurydice.Logging.log "Phase2.6" "%a" pfiles files;
+  let files = Eurydice.Cleanup2.remove_array_from_fn files in
   let files = Eurydice.Cleanup2.remove_implicit_array_copies#visit_files () files in
   let files = Krml.Simplify.sequence_to_let#visit_files () files in
   let files = Krml.Simplify.hoist#visit_files [] files in
   let files = Krml.Simplify.fixup_hoist#visit_files () files in
   let files = Krml.Simplify.misc_cosmetic#visit_files () files in
-  Eurydice.Logging.log "Phase2.4" "%a" pfiles files;
   let files = Krml.Simplify.let_to_sequence#visit_files () files in
-  Eurydice.Logging.log "Phase2.5" "%a" pfiles files;
   let files = Krml.Inlining.cross_call_analysis files in
-  Eurydice.Logging.log "Phase2.6" "%a" pfiles files;
   let files = Krml.Simplify.remove_unused files in
-  let files = Eurydice.Cleanup2.remove_array_from_fn#visit_files () files in
+  Eurydice.Logging.log "Phase2.7" "%a" pfiles files;
+  Eurydice.Logging.log "Phase2.8" "%a" pfiles files;
   (* Macros stemming from globals *)
   let files, macros = Eurydice.Cleanup2.build_macros files in
 
   Eurydice.Logging.log "Phase3" "%a" pfiles files;
   let errors, files = Krml.Checker.check_everything ~warn:true files in
   if errors then
-    exit 1;
+    fail __FILE__ __LINE__;
 
   let scope_env = Krml.Simplify.allocate_c_env files in
   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
+  Eurydice.Logging.log "Phase3.1" "%a" pfiles files;
   let macros =
     let cg_macros = Eurydice.Cleanup3.build_cg_macros#visit_files () files in
     Krml.Idents.LidSet.(union (union macros cg_macros) Eurydice.Builtin.macros)
@@ -186,6 +217,7 @@ Supported options:|}
           Some d
     ) ds
   ) files in
+  Eurydice.Logging.log "Phase3.2" "%a" pfiles files;
   let files = AstToCStar.mk_files files c_name_map Idents.LidSet.empty macros in
 
   let headers = CStarToC11.mk_headers c_name_map files in

dune-project

@@ -18,6 +18,12 @@
  (synopsis "A Rust to C translator")
  (description "Eurydice builds upon Charon to take existing Rust code and
               translate it to C")
- (depends ocaml dune terminal yaml))
+ (depends
+  ocaml
+  dune
+  yaml
+  (terminal (>= 0.4.0))
+ )
+)
 
 (using menhir 2.1)

eurydice.opam

@@ -12,8 +12,8 @@ bug-reports: "https://github.com/AeneasVerif/eurydice/issues"
 depends: [
   "ocaml"
   "dune" {>= "3.7"}
-  "terminal"
   "yaml"
+  "terminal" {>= "0.4.0"}
   "odoc" {with-doc}
 ]
 build: [

include/eurydice_glue.h

@@ -34,7 +34,12 @@ typedef struct {
 // remark above about how pointer arithmetic works in C), meaning either pointer or array type.
 #define EURYDICE_SLICE(x, start, end) ((Eurydice_slice){ .ptr = (void*)(x + start), .len = end - start })
 #define EURYDICE_SLICE_LEN(s, _) s.len
-#define Eurydice_slice_index(s, i, t, _ret_t) (((t*) s.ptr)[i])
+// This macro is a pain because in case the dereferenced element type is an
+// array, you cannot simply write `t x` as it would yield `int[4] x` instead,
+// which is NOT correct C syntax, so we add a dedicated phase in Eurydice that
+// adds an extra argument to this macro at the last minute so that we have the
+// correct type of *pointers* to elements.
+#define Eurydice_slice_index(s, i, t, t_ptr_t, _ret_t) (((t_ptr_t) s.ptr)[i])
 #define Eurydice_slice_subslice(s, r, t, _, _ret_t) EURYDICE_SLICE((t*)s.ptr, r.start, r.end)
 #define Eurydice_slice_subslice_to(s, subslice_end_pos, t, _, _ret_t) EURYDICE_SLICE((t*)s.ptr, 0, subslice_end_pos)
 #define Eurydice_slice_subslice_from(s, subslice_start_pos, t, _, _ret_t) EURYDICE_SLICE((t*)s.ptr, subslice_start_pos, s.len)
@@ -47,6 +52,8 @@ typedef struct {
 #define core_slice___Slice_T___copy_from_slice(dst, src, t, _ret_t) memcpy(dst.ptr, src.ptr, dst.len * sizeof(t))
 #define core_array___Array_T__N__23__as_slice(len_, ptr_, t, _ret_t) ((Eurydice_slice){ .ptr = ptr_, .len = len_ })
 
+#define core_array___core__clone__Clone_for__Array_T__N___20__clone(len, src, dst, elem_type, _ret_t) \
+  (memcpy(dst, src, len * sizeof(elem_type)))
 #define core_array_TryFromSliceError uint8_t
 
 #define Eurydice_array_eq(sz, a1, a2, t, _, _ret_t) (memcmp(a1, a2, sz * sizeof(t)) == 0)
@@ -56,6 +63,11 @@ typedef struct {
   ((ret_t){ \
     .fst = EURYDICE_SLICE((element_type*)slice.ptr, 0, mid), \
     .snd = EURYDICE_SLICE((element_type*)slice.ptr, mid, slice.len)})
+#define core_slice___Slice_T___split_at_mut(slice, mid, element_type, ret_t) \
+  ((ret_t){ \
+    .fst = { .ptr = slice.ptr, .len = mid }, \
+    .snd = { .ptr = (char*)slice.ptr + mid * sizeof(element_type), .len = slice.len - mid }})
+
 
 // Can't have a flexible array as a member of a union -- this violates strict aliasing rules.
 typedef struct
@@ -80,12 +92,20 @@ static inline void core_num__u32_8__to_be_bytes(uint32_t src, uint8_t dst[4]) {
   memcpy(dst, &x, 4);
 }
 
+static inline void core_num__u64_9__to_le_bytes(uint64_t v,uint8_t buf[8]) {
+  store64_le(buf,v);
+}
+static inline uint64_t core_num__u64_9__from_le_bytes(uint8_t buf[8]) {
+  return load64_le(buf);
+}
+
 static inline int64_t
-core_convert_num___core__convert__From_i32__for_i64__59__from(int32_t x)
-{
+core_convert_num___core__convert__From_i32__for_i64__59__from(int32_t x) {
   return x;
 }
 
+static inline uint32_t core_num__u8_6__count_ones(uint8_t x0) { return __builtin_popcount(x0); }
+
 // unsigned overflow wraparound semantics in C
 static inline uint16_t core_num__u16_7__wrapping_add(uint16_t x, uint16_t y) { return x + y; }
 static inline uint8_t core_num__u8_6__wrapping_sub(uint8_t x, uint8_t y) { return x - y; }
@@ -160,12 +180,18 @@ typedef struct {
        .tag = core_option_Some, \
        .f0 = ((iter)->index++, &((t*)((iter)->s.ptr))[(iter)->index-1]) }))
 
-// MISC
+// STRINGS
+
+typedef const char *Prims_string;
 
-#define core_fmt_Formatter void
+// MISC (UNTESTED)
 
+typedef void *core_fmt_Formatter;
+typedef void *core_fmt_Arguments;
+typedef void *core_fmt_rt_Argument;
+#define core_fmt_rt__core__fmt__rt__Argument__a__1__new_display(x1, x2, x3, x4) NULL
 
-// VECTORS
+// VECTORS (ANCIENT, POSSIBLY UNTESTED)
 
 /* For now these are passed by value -- three words. We could conceivably change
  * the representation to heap-allocate this struct and only pass around the