From 199e10df8e776e4b27f9cfd2357db6babf674ed1 Mon Sep 17 00:00:00 2001
From: Alasdair
Date: Tue, 28 Apr 2020 17:24:04 +0100
Subject: 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.
---
 language/jib.ott | 1 +
 1 file changed, 1 insertion(+)

(limited to 'language')

diff --git a/language/jib.ott b/language/jib.ott
index 63c86126..9c739ec4 100644
--- a/language/jib.ott
+++ b/language/jib.ott
@@ -57,6 +57,7 @@ grammar
 
 name :: '' ::=
   | id nat                :: :: name
+  | global id nat         :: :: global
   | have_exception nat    :: :: have_exception
   | current_exception nat :: :: current_exception
   | throw_location nat    :: :: throw_location
-- 
cgit v1.2.3