Functorise and refactor C code generator

Currently uses the -c2 option

Now generates a sail_state struct which is passed as a pointer to all
generated functions. This contains all registers, letbindings, and the
exception state. (Letbindings must be included as they can contain
pointers to registers). This should make it possible to use sail models
in a multi-threaded program by creating multiple sail_states, provided a
suitable set of thread-safe memory builtins are provided. Currently the
sail_state cannot be passed to the memory builtins.

For foo.sail, now generate a foo.c, foo.h, and (optionally) a foo_emu.c.
foo_emu.c wraps the generated library into an emulator that behaves the
same as the one we previously generated.

The sail_assert and sail_match_failure builtins are now in a separate
file, as they must exist even when the RTS is not used.

Name mangling can be controlled via the exports and exports_mangled
fields of the configuration struct (currently not exposed outside of
OCaml). exports allows specifying a name in C for any Sail identifier
(before name mangling) and exports_mangled allows specifiying a name for
a mangled Sail identifier - this is primarily useful for generic
functions and data structures which have been specialised.

5 files changed, 57 insertions, 43 deletions

diff --git a/lib/rts.c b/lib/rts.c
index edae3965..f0ae149c 100644
--- a/lib/rts.c
+++ b/lib/rts.c
@@ -1,28 +1,15 @@
-#include<string.h>
-#include<getopt.h>
-#include<inttypes.h>
+#include <string.h>
+#include <getopt.h>
+#include <inttypes.h>
 
-#include"sail.h"
-#include"rts.h"
-#include"elf.h"
+#include "sail.h"
+#include "rts.h"
+#include "elf.h"
 
 static uint64_t g_elf_entry;
 uint64_t g_cycle_count = 0;
 static uint64_t g_cycle_limit;
 
-void sail_match_failure(sail_string msg)
-{
-  fprintf(stderr, "Pattern match failure in %s\n", msg);
-  exit(EXIT_FAILURE);
-}
-
-unit sail_assert(bool b, sail_string msg)
-{
-  if (b) return UNIT;
-  fprintf(stderr, "Assertion failed: %s\n", msg);
-  exit(EXIT_FAILURE);
-}
-
 unit sail_exit(unit u)
 {
   fprintf(stderr, "[Sail] Exiting after %" PRIu64 " cycles\n", g_cycle_count);
diff --git a/lib/rts.h b/lib/rts.h
index 68d01cb5..1ba48d59 100644
--- a/lib/rts.h
+++ b/lib/rts.h
@@ -1,22 +1,12 @@
-#pragma once
+#ifndef SAIL_RTS_H
+#define SAIL_RTS_H
 
-#include<inttypes.h>
-#include<stdlib.h>
-#include<stdio.h>
+#include <inttypes.h>
+#include <stdlib.h>
+#include <stdio.h>
 
-#include"sail.h"
-
-/*
- * This function should be called whenever a pattern match failure
- * occurs. Pattern match failures are always fatal.
- */
-void sail_match_failure(sail_string msg);
-
-/*
- * sail_assert implements the assert construct in Sail. If any
- * assertion fails we immediately exit the model.
- */
-unit sail_assert(bool b, sail_string msg);
+#include "sail.h"
+#include "sail_failure.h"
 
 unit sail_exit(unit);
 
@@ -169,3 +159,5 @@ void cleanup_rts(void);
 
 unit z__SetConfig(sail_string, sail_int);
 unit z__ListConfig(const unit u);
+
+#endif
diff --git a/lib/sail.h b/lib/sail.h
index fbbce541..98ca3adb 100644
--- a/lib/sail.h
+++ b/lib/sail.h
@@ -1,12 +1,13 @@
-#pragma once
+#ifndef SAIL_H
+#define SAIL_H
 
-#include<inttypes.h>
-#include<stdlib.h>
-#include<stdio.h>
-#include<stdbool.h>
-#include<gmp.h>
+#include <inttypes.h>
+#include <stdlib.h>
+#include <stdio.h>
+#include <stdbool.h>
+#include <gmp.h>
 
-#include<time.h>
+#include <time.h>
 
 static inline void *sail_malloc(size_t size)
 {
@@ -440,3 +441,5 @@ void get_time_ns(sail_int*, const unit);
 /* ***** ARM optimisations ***** */
 
 void arm_align(lbits *, const lbits, const sail_int);
+
+#endif
diff --git a/lib/sail_failure.c b/lib/sail_failure.c
new file mode 100644
index 00000000..b725d42c
--- /dev/null
+++ b/lib/sail_failure.c
@@ -0,0 +1,14 @@
+#include "sail_failure.h"
+
+void sail_match_failure(sail_string msg)
+{
+  fprintf(stderr, "Pattern match failure in %s\n", msg);
+  exit(EXIT_FAILURE);
+}
+
+unit sail_assert(bool b, sail_string msg)
+{
+  if (b) return UNIT;
+  fprintf(stderr, "Assertion failed: %s\n", msg);
+  exit(EXIT_FAILURE);
+}
diff --git a/lib/sail_failure.h b/lib/sail_failure.h
new file mode 100644
index 00000000..d43baf4d
--- /dev/null
+++ b/lib/sail_failure.h
@@ -0,0 +1,18 @@
+#ifndef SAIL_FAILURE_H
+#define SAIL_FAILURE_H
+
+#include "sail.h"
+
+/*
+ * This function should be called whenever a pattern match failure
+ * occurs. Pattern match failures are always fatal.
+ */
+void sail_match_failure(sail_string msg);
+
+/*
+ * sail_assert implements the assert construct in Sail. If any
+ * assertion fails we immediately exit the model.
+ */
+unit sail_assert(bool b, sail_string msg);
+
+#endif