From 703e996e44d0c1773fb23cd554b896318fae081b Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Thu, 7 Mar 2019 20:22:03 +0000 Subject: 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. --- src/Makefile | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) (limited to 'src/Makefile') 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: -- cgit v1.2.3