[CN-exec] Only use _Bool in runtime library

lib/fulminate/cn_to_ail.ml

@@ -21,7 +21,9 @@ let setter_str filename sym =
   "cn_test_set_" ^ Utils.static_prefix filename ^ "_" ^ Sym.pp_string sym
 
 
-let true_const = A.AilEconst (ConstantPredefined PConstantTrue)
+let true_const = A.(AilEconst (ConstantInteger (IConstant (Z.of_int 1, Decimal, None))))
+
+let false_const = A.(AilEconst (ConstantInteger (IConstant (Z.of_int 0, Decimal, None))))
 
 let ownership_ctypes = ref []
 
@@ -646,9 +648,7 @@ let cn_to_ail_const const basetype =
       in
       wrap (A.AilEunary (Address, mk_expr ail_const'))
     | Alloc_id _ -> failwith (__LOC__ ^ ": TODO Alloc_id")
-    | Bool b ->
-      wrap
-        (A.AilEconst (ConstantPredefined (if b then PConstantTrue else PConstantFalse)))
+    | Bool b -> wrap (if b then true_const else false_const)
     | Unit -> wrap ail_null (* Gets overridden by dest_with_unit_check *)
     | Null -> wrap ail_null
     | CType_const _ -> failwith (__LOC__ ^ ": TODO CType_const")

runtime/libcn/check_compat.cpp

@@ -1,7 +1,6 @@
 #pragma clang diagnostic ignored "-Wc++11-narrowing"
 
 #include <bennet/prelude.h>
-#include <cn-executable/utils.h>
 #include <cn-testing/prelude.h>
 #include <cn-replicate/prelude.h>
 

runtime/libcn/include/bennet/dsl/arbitrary.h

@@ -2,7 +2,7 @@
 #define BENNET_ARBITRARY_H
 
 #include <bennet/internals/domain.h>
-#include <cn-executable/utils.h>
+#include <bennet/internals/fulm_types.h>
 
 uint8_t get_null_in_every(void);
 void set_null_in_every(uint8_t n);

runtime/libcn/include/bennet/dsl/assert.h

@@ -6,7 +6,6 @@
 #include <bennet/info/backtracks.h>
 #include <bennet/state/failure.h>
 #include <bennet/utils/optional.h>
-#include <cn-executable/utils.h>
 
 #ifdef __cplusplus
 extern "C" {

runtime/libcn/include/bennet/dsl/assign.h

@@ -4,7 +4,6 @@
 #include <stdbool.h>
 
 #include <bennet/state/alloc.h>
-#include <cn-executable/utils.h>
 
 #define bennet_assign(pointer_ty, id, base_ptr, addr, value, bytes, vars)                \
   (bennet_assign_##pointer_ty(id, base_ptr, addr, value, bytes, vars))

runtime/libcn/include/bennet/internals/fulm_types.h

@@ -0,0 +1,24 @@
+
+typedef struct cn_bits_u8 cn_bits_u8;
+typedef struct cn_bits_i8 cn_bits_i8;
+typedef struct cn_bits_u16 cn_bits_u16;
+typedef struct cn_bits_i16 cn_bits_i16;
+typedef struct cn_bits_u32 cn_bits_u32;
+typedef struct cn_bits_i32 cn_bits_i32;
+typedef struct cn_bits_u64 cn_bits_u64;
+typedef struct cn_bits_i64 cn_bits_i64;
+typedef struct cn_pointer cn_pointer;
+typedef struct cn_bool cn_bool;
+
+void* convert_from_cn_pointer(cn_pointer*);
+uint8_t convert_from_cn_bits_u8(cn_bits_u8*);
+uint16_t convert_from_cn_bits_u16(cn_bits_u16*);
+uint32_t convert_from_cn_bits_u32(cn_bits_u32*);
+uint64_t convert_from_cn_bits_u64(cn_bits_u64*);
+int8_t convert_from_cn_bits_i8(cn_bits_i8*);
+int16_t convert_from_cn_bits_i16(cn_bits_i16*);
+int32_t convert_from_cn_bits_i32(cn_bits_i32*);
+int64_t convert_from_cn_bits_i64(cn_bits_i64*);
+
+
+

runtime/libcn/include/bennet/state/alloc.h

@@ -5,7 +5,6 @@
 
 #include <bennet/internals/domain.h>
 #include <bennet/utils/optional.h>
-#include <cn-executable/utils.h>
 
 #ifdef __cplusplus
 extern "C" {

runtime/libcn/include/bennet/state/rand_alloc.h

@@ -5,6 +5,7 @@
 #include <stdint.h>
 
 #include <bennet/internals/domain.h>
+#include <cn-executable/error.h>
 
 // Opaque struct for the allocator
 struct rand_alloc;

runtime/libcn/include/bennet/utils/vector.h

@@ -6,8 +6,6 @@
 #include <stdlib.h>
 #include <string.h>
 
-#include <cn-executable/utils.h>
-
 #ifdef __cplusplus
 extern "C" {
 #endif

runtime/libcn/include/cn-executable/error.h

@@ -0,0 +1,61 @@
+#define cn_printf(level, ...)                                                            \
+  if (get_cn_logging_level() >= level) {                                                 \
+    printf(__VA_ARGS__);                                                                 \
+  }
+
+  /* Error handlers */
+
+
+enum cn_logging_level {
+  CN_LOGGING_NONE = 0,
+  CN_LOGGING_ERROR = 1,
+  CN_LOGGING_INFO = 2
+};
+
+enum cn_logging_level get_cn_logging_level(void);
+
+/** Sets the logging level, returning the previous one */
+enum cn_logging_level set_cn_logging_level(enum cn_logging_level new_level);
+
+enum cn_trace_granularity {
+  CN_TRACE_NONE = 0,
+  CN_TRACE_ENDS = 1,
+  CN_TRACE_ALL = 2,
+};
+
+enum cn_trace_granularity get_cn_trace_granularity(void);
+
+/** Sets the trace granularity, returning the previous one */
+enum cn_trace_granularity set_cn_trace_granularity(
+    enum cn_trace_granularity new_granularity);
+
+void cn_print_nr_owned_predicates(void);
+
+struct cn_error_message_info {
+  const char* function_name;
+  char* file_name;
+  int line_number;
+  char* cn_source_loc;
+  struct cn_error_message_info* parent;
+  struct cn_error_message_info* child;
+};
+
+void initialise_error_msg_info_(
+    const char* function_name, char* file_name, int line_number);
+
+#define initialise_error_msg_info()                                                      \
+  initialise_error_msg_info_(__func__, __FILE__, __LINE__)
+
+void reset_error_msg_info();
+void free_error_msg_info();
+
+void update_error_message_info_(
+    const char* function_name, char* file_name, int line_number, char* cn_source_loc);
+
+void cn_pop_msg_info();
+
+#define update_cn_error_message_info(x)                                                  \
+  update_error_message_info_(__func__, __FILE__, __LINE__ + 1, x)
+
+#define update_cn_error_message_info_access_check(x)                                     \
+  update_error_message_info_(__func__, __FILE__, __LINE__, x)

runtime/libcn/include/cn-executable/hash_table.h

@@ -72,7 +72,7 @@ typedef struct {
 
 hash_table_iterator ht_iterator(hash_table* table);
 
-bool ht_next(hash_table_iterator* it);
+_Bool ht_next(hash_table_iterator* it);
 
 #ifdef __cplusplus
 }

runtime/libcn/include/cn-executable/rts_deps.h

@@ -26,7 +26,6 @@
   #define int64_t   __cerbty_int64_t
   #define intptr_t  __cerbty_intptr_t
   #define alignof   _Alignof
-  #define bool      _Bool
 
 #else
   #include <stdalign.h>

runtime/libcn/include/cn-executable/utils.h

@@ -7,15 +7,8 @@
 #include "hash_table.h"
 #include "rts_deps.h"
 #include "stack.h"
+#include "error.h"
 
-#define cn_printf(level, ...)                                                            \
-  if (get_cn_logging_level() >= level) {                                                 \
-    printf(__VA_ARGS__);                                                                 \
-  }
-
-// XXX: things used by injected code
-#define true  1
-#define false 0
 
 #ifdef __cplusplus
 extern "C" {
@@ -30,63 +23,8 @@ enum spec_mode {
   NON_SPEC = 6
 };
 
-/* Error handlers */
 void reset_fulminate(void);
 
-enum cn_logging_level {
-  CN_LOGGING_NONE = 0,
-  CN_LOGGING_ERROR = 1,
-  CN_LOGGING_INFO = 2
-};
-
-enum cn_logging_level get_cn_logging_level(void);
-
-/** Sets the logging level, returning the previous one */
-enum cn_logging_level set_cn_logging_level(enum cn_logging_level new_level);
-
-enum cn_trace_granularity {
-  CN_TRACE_NONE = 0,
-  CN_TRACE_ENDS = 1,
-  CN_TRACE_ALL = 2,
-};
-
-enum cn_trace_granularity get_cn_trace_granularity(void);
-
-/** Sets the trace granularity, returning the previous one */
-enum cn_trace_granularity set_cn_trace_granularity(
-    enum cn_trace_granularity new_granularity);
-
-void cn_print_nr_owned_predicates(void);
-
-struct cn_error_message_info {
-  const char* function_name;
-  char* file_name;
-  int line_number;
-  char* cn_source_loc;
-  struct cn_error_message_info* parent;
-  struct cn_error_message_info* child;
-};
-
-void initialise_error_msg_info_(
-    const char* function_name, char* file_name, int line_number);
-
-#define initialise_error_msg_info()                                                      \
-  initialise_error_msg_info_(__func__, __FILE__, __LINE__)
-
-void reset_error_msg_info();
-void free_error_msg_info();
-
-void update_error_message_info_(
-    const char* function_name, char* file_name, int line_number, char* cn_source_loc);
-
-void cn_pop_msg_info();
-
-#define update_cn_error_message_info(x)                                                  \
-  update_error_message_info_(__func__, __FILE__, __LINE__ + 1, x)
-
-#define update_cn_error_message_info_access_check(x)                                     \
-  update_error_message_info_(__func__, __FILE__, __LINE__, x)
-
 /* Wrappers for C types */
 
 /* Signed bitvectors */
@@ -134,7 +72,7 @@ typedef struct cn_pointer {
 } cn_pointer;
 
 typedef struct cn_bool {
-  bool val;
+  _Bool val;
 } cn_bool;
 
 typedef struct cn_alloc_id {
@@ -146,8 +84,8 @@ typedef hash_table cn_map;
 void initialise_ownership_ghost_state(void);
 void free_ownership_ghost_state(void);
 void initialise_ghost_stack_depth(void);
-void initialise_exec_c_locs_mode(bool flag);
-void initialise_ownership_stack_mode(bool flag);
+void initialise_exec_c_locs_mode(_Bool flag);
+void initialise_ownership_stack_mode(_Bool flag);
 signed long get_cn_stack_depth(void);
 void ghost_stack_depth_incr(void);
 void ghost_stack_depth_decr(void);
@@ -169,7 +107,7 @@ void cn_free_sized(void*, size_t len);
 void cn_print_nr_u64(int i, unsigned long u);
 void cn_print_u64(const char* str, unsigned long u);
 void dump_ownership_ghost_state(int stack_depth);
-bool is_mapped(void* ptr);
+_Bool is_mapped(void* ptr);
 
 /* cn_failure callbacks */
 enum cn_failure_mode {
@@ -187,8 +125,8 @@ void cn_failure(enum cn_failure_mode failure_mode, enum spec_mode spec_mode);
 
 /* Conversion functions */
 
-cn_bool* convert_to_cn_bool(bool b);
-bool convert_from_cn_bool(cn_bool* b);
+cn_bool* convert_to_cn_bool(_Bool b);
+_Bool convert_from_cn_bool(cn_bool* b);
 void cn_assert(cn_bool* cn_b, enum spec_mode spec_mode);
 cn_bool* cn_bool_and(cn_bool* b1, cn_bool* b2);
 cn_bool* cn_bool_or(cn_bool* b1, cn_bool* b2);

runtime/libcn/include/cn-replicate/shape.h

@@ -3,8 +3,7 @@
 
 #include <stddef.h>
 #include <string.h>
-
-#include <cn-executable/utils.h>
+#include <bennet/internals/fulm_types.h>
 
 #ifdef __cplusplus
 extern "C" {

runtime/libcn/include/cn-testing/test.h

@@ -9,7 +9,6 @@
 #include <time.h>
 
 #include <bennet/prelude.h>
-#include <cn-executable/utils.h>
 #include <cn-testing/result.h>
 #include <cn-replicate/lines.h>
 #include <cn-replicate/shape.h>

runtime/libcn/include/dune

@@ -17,6 +17,7 @@
    runtime/include/cn-executable/fulminate_alloc.h)
   (cn-executable/hash_table.h as runtime/include/cn-executable/hash_table.h)
   (cn-executable/utils.h as runtime/include/cn-executable/utils.h)
+  (cn-executable/error.h as runtime/include/cn-executable/error.h)
   (cn-executable/rts_deps.h as runtime/include/cn-executable/rts_deps.h)
   (cn-executable/cerb_types.h as runtime/include/cn-executable/cerb_types.h)
   (cn-executable/stack.h as runtime/include/cn-executable/stack.h)
@@ -52,6 +53,7 @@
    as
    runtime/include/bennet/internals/domains/wint.h)
   (bennet/internals/domain.h as runtime/include/bennet/internals/domain.h)
+  (bennet/internals/fulm_types.h as runtime/include/bennet/internals/fulm_types.h)
   (bennet/internals/rand.h as runtime/include/bennet/internals/rand.h)
   (bennet/internals/size.h as runtime/include/bennet/internals/size.h)
   (bennet/internals/urn.h as runtime/include/bennet/internals/urn.h)