C: Refactor C backend

Main change is splitting apart the Sail->IR compilation stage and the
C code generation and optimization phase. Rather than variously
calling the intermediate language either bytecode (when it's not
really) or simply IR, we give it a name: Jib (a type of Sail). Most of
the types are still prefixed by c/C, and I don't think it's worth
changing this.

The various parts of the C backend are now in the src/jib/ subdirectory

src/jib/anf.ml         - Sail->ANF translation
src/jib/jib_util.ml    - various Jib AST processing and helper functions (formerly bytecode_util)
src/jib/jib_compile.ml - Sail->Jib translation (using Sail->ANF)
src/jib/c_backend.ml   - Jib->C code generator and optimizations

Further, bytecode.ott is now jib.ott and generates jib.ml (which still
lives in src/ for now)

The optimizations in c_backend.ml should eventually be moved in a
separate jib_optimization file.

The Sail->Jib compilation can be parameterised by two functions - one
is a custom ANF->ANF optimization pass that can be specified on a per
Jib backend basis, and the other is the rule for translating Sail
types in Jib types. This can be more or less precise depending on how
precise we want to be about bit-widths etc, i.e. we only care about <64
and >64 for C, but for SMT generation we would want to be as precise
as possible.

Additional improvements:

The Jib IR is now agnostic about whether arguments are allocated on
the heap vs the stack and this is handled by the C code generator.

jib.ott now has some more comments explaining various parts of the Jib
AST.

A Set module and comparison function for ctyps is defined, and some
functions now return ctyp sets rather than lists to avoid repeated
work.

1 files changed, 12 insertions, 12 deletions

diff --git a/src/Makefile b/src/Makefile
index beba66df..d71c9fb8 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -74,16 +74,16 @@ full: sail lib doc
 ast.lem: ../language/sail.ott
 	ott -sort false -generate_aux_rules true -o ast.lem -picky_multiple_parses true ../language/sail.ott
 
-bytecode.lem: ../language/bytecode.ott ast.lem
-	ott -sort false -generate_aux_rules true -o bytecode.lem -picky_multiple_parses true ../language/bytecode.ott
+jib.lem: ../language/jib.ott ast.lem
+	ott -sort false -generate_aux_rules true -o jib.lem -picky_multiple_parses true ../language/jib.ott
 
 ast.ml: ast.lem
 	lem -ocaml ast.lem
 	sed -i.bak -f ast.sed ast.ml
 
-bytecode.ml: bytecode.lem
-	lem -ocaml bytecode.lem -lib . -lib gen_lib/
-	sed -i.bak -f ast.sed bytecode.ml
+jib.ml: jib.lem
+	lem -ocaml jib.lem -lib . -lib gen_lib/
+	sed -i.bak -f ast.sed jib.ml
 
 manifest.ml:
 	echo "(* Generated file -- do not edit. *)" > manifest.ml
@@ -99,18 +99,18 @@ else
 	echo let version=\"$(shell grep '^version:' ../opam | grep -o -E '"[^"]+"')\" >> manifest.ml
 endif
 
-sail: ast.ml bytecode.ml manifest.ml
+sail: ast.ml jib.ml manifest.ml
 	ocamlbuild -use-ocamlfind sail.native sail_lib.cma sail_lib.cmxa
 
-isail: ast.ml bytecode.ml manifest.ml
+isail: ast.ml jib.ml manifest.ml
 	ocamlbuild -use-ocamlfind isail.native
 
-coverage: ast.ml bytecode.ml manifest.ml
+coverage: ast.ml jib.ml manifest.ml
 	BISECT_COVERAGE=YES ocamlbuild -use-ocamlfind -plugin-tag 'package(bisect_ppx-ocamlbuild)' isail.native
 
 sail.native: sail
 
-sail.byte: ast.ml bytecode.ml manifest.ml
+sail.byte: ast.ml jib.ml manifest.ml
 	ocamlbuild -use-ocamlfind -cflag -g sail.byte
 
 interpreter: lem_interp/interp_ast.lem
@@ -132,9 +132,9 @@ clean:
 	-rm -f ast.ml
 	-rm -f ast.lem
 	-rm -f ast.ml.bak
-	-rm -f bytecode.ml
-	-rm -f bytecode.lem
-	-rm -f bytecode.ml.bak
+	-rm -f jib.ml
+	-rm -f jib.lem
+	-rm -f jib.ml.bak
 	-rm -f manifest.ml
 
 doc: