Merge pull request #63 from AeneasVerif/protz_assertions

Prettify assertions
AeneasVerif · Aug 30, 2024 · fcdd185 · fcdd185
2 parents 7efec16 + 84d69ef
commit fcdd185
Show file tree

Hide file tree

Showing 8 changed files with 218 additions and 135 deletions.
diff --git a/Makefile b/Makefile
@@ -3,7 +3,7 @@ KRML_HOME 	?= $(dir $(abspath $(lastword $(MAKEFILE_LIST))))/../karamel
 EURYDICE	?= ./eurydice $(EURYDICE_FLAGS)
 CHARON		?= $(CHARON_HOME)/bin/charon
 
-BROKEN_TESTS		= step_by where_clauses chunks mutable_slice_range closure issue_49 symcrust
+BROKEN_TESTS		= step_by where_clauses chunks mutable_slice_range closure issue_49
 TEST_DIRS		= $(filter-out $(BROKEN_TESTS),$(subst test/,,$(shell find test -maxdepth 1 -mindepth 1 -type d)))
 
 .PHONY: all

diff --git a/bin/main.ml b/bin/main.ml
@@ -198,6 +198,7 @@ Supported options:|}
     fail __FILE__ __LINE__;
   Eurydice.Logging.log "Phase2.1" "%a" pfiles files;
   let files = Eurydice.Cleanup2.improve_names files in
+  let files = Eurydice.Cleanup2.recognize_asserts#visit_files () files in
   let files = Krml.Monomorphization.functions files in
   let files = Krml.Monomorphization.datatypes files in
   let files =
@@ -329,6 +330,9 @@ Supported options:|}
   in
 
   Eurydice.Logging.log "Phase3.3" "%a" pfiles files;
+  let files = List.map (fun (f, ds) -> f, List.filter (fun d ->
+    not (Krml.Idents.LidSet.mem (Krml.Ast.lid_of_decl d) Eurydice.Builtin.skip))
+  ds) files in
   let files = AstToCStar.mk_files files c_name_map Idents.LidSet.empty macros in
 
   let headers = CStarToC11.mk_headers c_name_map files in

diff --git a/include/eurydice_glue.h b/include/eurydice_glue.h
@@ -18,6 +18,13 @@ extern "C" {
 #include "krml/lowstar_endianness.h"
 
 #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__); \
+  } \
+} while (0)
 
 // SLICES, ARRAYS, ETC.
 
@@ -130,13 +137,18 @@ 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__u32_8__to_le_bytes(uint32_t src, uint8_t dst[4]) {
+  store32_le(dst, src);
+}
+
 static inline uint32_t core_num__u32_8__from_le_bytes(uint8_t buf[4]) {
   return load32_le(buf);
 }
 
 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);
 }
@@ -188,6 +200,9 @@ static inline uint8_t Eurydice_bitand_pv_u8(uint8_t *p, uint8_t 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;
+}
 
 #define core_num_nonzero_private_NonZeroUsizeInner size_t
 static inline core_num_nonzero_private_NonZeroUsizeInner