diff options
| author | Alasdair Armstrong | 2019-03-07 20:22:03 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-03-08 17:21:30 +0000 |
| commit | 703e996e44d0c1773fb23cd554b896318fae081b (patch) | |
| tree | 15a4a4d207838a1f214c7c541b5397e2bdf6269d | |
| parent | 87ffe603e44e9be6f4109f6a9dd475df6dcfc489 (diff) | |
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.
| -rw-r--r-- | language/jib.ott (renamed from language/bytecode.ott) | 135 | ||||
| -rw-r--r-- | src/Makefile | 24 | ||||
| -rw-r--r-- | src/_tags | 1 | ||||
| -rw-r--r-- | src/isail.ml | 49 | ||||
| -rw-r--r-- | src/jib/anf.ml (renamed from src/anf.ml) | 4 | ||||
| -rw-r--r-- | src/jib/anf.mli (renamed from src/anf.mli) | 2 | ||||
| -rw-r--r-- | src/jib/c_backend.ml (renamed from src/c_backend.ml) | 1505 | ||||
| -rw-r--r-- | src/jib/c_backend.mli (renamed from src/c_backend.mli) | 35 | ||||
| -rw-r--r-- | src/jib/jib_compile.ml | 1367 | ||||
| -rw-r--r-- | src/jib/jib_compile.mli (renamed from src/bytecode_interpreter.ml) | 137 | ||||
| -rw-r--r-- | src/jib/jib_util.ml (renamed from src/bytecode_util.ml) | 208 | ||||
| -rw-r--r-- | src/sail.ml | 16 |
12 files changed, 1814 insertions, 1669 deletions
diff --git a/language/bytecode.ott b/language/jib.ott index cc329e02..7b5d0162 100644 --- a/language/bytecode.ott +++ b/language/jib.ott @@ -49,6 +49,7 @@ grammar % Fragments are small pure snippets of (abstract) C code, mostly % expressions, used by the aval and cval types. + fragment :: 'F_' ::= | id :: :: id | '&' id :: :: ref @@ -62,45 +63,67 @@ fragment :: 'F_' ::= | string :: :: raw | poly fragment :: :: poly -% init / clear -> create / kill +% Note that init / clear are sometimes refered to as create / kill + +%%% IR types ctyp :: 'CT_' ::= {{ com C type }} - | mpz_t :: :: lint -% Arbitrary precision GMP integer, mpz_t in C. - | bv_t ( bool ) :: :: lbits -% Variable length bitvector - flag represents direction, true - dec or false - inc - | sbv_t ( bool ) :: :: sbits -% Small variable length bitvector - less than 64 bits - | 'uint64_t' ( nat , bool ) :: :: fbits -% Fixed length bitvector that fits within a 64-bit word. - int -% represents length, and flag is the same as CT_bv. - | 'int64_t' nat :: :: fint -% Used for (signed) integers that fit within 64-bits. - | unit_t :: :: unit -% unit is a value in sail, so we represent it as a one element type -% here too for clarity but we actually compile it to an int which is -% always 0. +% Integer types +% +% lint is a large (l) arbitrary precision integer, mpz_t in C. +% fint(n) is a fixed precision signed integer that is representable in exactly n bits + | lint :: :: lint + | fint nat :: :: fint + +% Bitvector types - flag represents bit indexing direction, true - dec or false - inc +% +% lbits is a large (l) arbitrary precision bitvector +% sbits is a small (s) bitvector, such that sbits(n, _) is guaranteed to have a length of at most n. +% fbits is a fixed (f) bitvector, such that fbits(n, _) has a length of exactly n bits + | lbits ( bool ) :: :: lbits + | sbits ( nat , bool ) :: :: sbits + | fbits ( nat , bool ) :: :: fbits + +% Other Sail types + | unit :: :: unit | bool_t :: :: bool - | real_t :: :: real - | bit_t :: :: bit -% The real type in sail. Abstract here, but implemented using either -% GMP rationals or high-precision floating point. - | ( ctyp0 , ... , ctypn ) :: :: tup + | bit :: :: bit | string_t :: :: string - | enum id ( id0 , ... , idn ) :: :: enum - | struct id ( id0 * ctyp0 , ... , idn * ctypn ) :: :: struct - | variant id ( id0 * ctyp0 , ... , idn * ctypn ) :: :: variant + +% The real type in sail. Abstract here, so the code generator can +% choose to implement it using either GMP rationals or high-precision +% floating point. + | real :: :: real + + | ( ctyp0 , ... , ctypn ) :: :: tup + % Abstractly represent how all the Sail user defined types get mapped % into C. We don't fully worry about precise implementation details at % this point, as C doesn't have variants or tuples natively, but these % need to be encoded. + | enum id ( id0 , ... , idn ) :: :: enum + | struct id ( id0 * ctyp0 , ... , idn * ctypn ) :: :: struct + | variant id ( id0 * ctyp0 , ... , idn * ctypn ) :: :: variant + +% A vector type for non-bit vectors, and a (linked) list type. | vector ( bool , ctyp ) :: :: vector | list ( ctyp ) :: :: list -% A vector type for non-bit vectors, and a list type. + | ref ( ctyp ) :: :: ref + +% We can still have a very limited amount of polymorphism in this IR +% representation, as variants can have polymorphic constructors. The +% reason is we can put more precise types into constructors and then +% consume them as more general types meaning the underlying +% representation (rather than the high-level sail types) are what we +% need to specialise constructors, e.g. Some(0xFF) would be a Some +% constructor containing a fbits(8, true), but this could be pattern +% matched as Some(x) where the matching context expects x to have type +% lbits, and this must work without compiling to type incorrect C. | poly :: :: poly + cval :: 'CV_' ::= {{ ocaml fragment * ctyp }} {{ lem fragment * ctyp }} @@ -112,6 +135,7 @@ clexp :: 'CL_' ::= | clexp . nat :: :: tuple | current_exception : ctyp :: :: current_exception | have_exception :: :: have_exception + | return : ctyp :: :: return ctype_def :: 'CTD_' ::= {{ com C type definition }} @@ -125,45 +149,72 @@ iannot :: 'IA_' ::= instr :: 'I_' ::= {{ aux _ iannot }} +% The following are the minimal set of instructions output by +% Jib_compile.ml. | ctyp id :: :: decl | ctyp id = cval :: :: init - | if ( cval ) { instr0 ; ... ; instrn } - else { instr0 ; ... ; instrm } : ctyp :: :: if | jump ( cval ) string :: :: jump + | goto string :: :: goto + | string : :: :: label | clexp = bool id ( cval0 , ... , cvaln ) :: :: funcall | clexp = cval :: :: copy - | alias clexp = cval :: :: alias | clear ctyp id :: :: clear - | return cval :: :: return + | undefined ctyp :: :: undefined + | match_failure :: :: match_failure + | end :: :: end + +% All instructions containing nested instructions can be flattened +% away. try and throw only exist for internal use within +% Jib_compile.ml, as exceptional control flow is handled by a separate +% Jib->Jib pass. + | if ( cval ) { instr0 ; ... ; instrn } + else { instr0 ; ... ; instrm } : ctyp :: :: if | { instr0 ; ... ; instrn } :: :: block | try { instr0 ; ... ; instrn } :: :: try_block | throw cval :: :: throw + +% We can embed either comments or pass raw-strings through to the +% code-generator. The first is useful for annotating generated source, +% the second for inserting instrumention. I_raw should be side-effect +% free. | '//' string :: :: comment - | C string :: :: raw % only used for GCC attributes - | string : :: :: label - | goto string :: :: goto - | undefined ctyp :: :: undefined - | match_failure :: :: match_failure + | C string :: :: raw + +% Jib_compile.ml will represent all returns as assigments to the clexp +% CL_return, followed by end to signify the end of the +% function. + | return cval :: :: return -% For optimising away allocations. - | reset ctyp id :: :: reset - | ctyp id = cval :: :: reinit +% For optimising away allocations and copying. + | reset ctyp id :: :: reset + | ctyp id = cval :: :: reinit + | alias clexp = cval :: :: alias cdef :: 'CDEF_' ::= | register id : ctyp = { instr0 ; ... ; instrn } :: :: reg_dec - | ctype_def :: :: type + | ctype_def :: :: type + +% The first list of instructions sets up the global letbinding, while +% the second clears it. | let nat ( id0 : ctyp0 , ... , idn : ctypn ) = { instr0 ; ... ; instrm } :: :: let -% The first list of instructions creates up the global letbinding, the -% second kills it. - | val id ( ctyp0 , ... , ctypn ) -> ctyp - :: :: spec + + | val id ( ctyp0 , ... , ctypn ) -> ctyp :: :: spec + +% If mid = Some id this indicates that the caller should allocate the +% return type and passes a pointer to it as an extra argument id for +% the function to fill in. This is only done via Jib->Jib rewrites +% used when compiling to C. | function id mid ( id0 , ... , idn ) { instr0 ; ... ; instrm } :: :: fundef + +% Each function can have custom global state. In CDEF_startup and +% CDEF_finish all I_decl and I_init nodes are treated as global and no +% nested-instructions (if/block) are allowed. | startup id { instr0 ; ... ; instrn } :: :: startup 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: @@ -11,6 +11,7 @@ true: -traverse, debug, use_menhir <**/*.m{l,li}>: package(lem) <gen_lib>: include +<jib>: include <pprint> or <pprint/src>: include # disable partial match and unused variable warnings diff --git a/src/isail.ml b/src/isail.ml index 4c7cf8d6..e47973b4 100644 --- a/src/isail.ml +++ b/src/isail.ml @@ -57,7 +57,6 @@ open Pretty_print_sail type mode = | Evaluation of frame - | Bytecode of Value2.vl Bytecode_interpreter.gstate * Value2.vl Bytecode_interpreter.stack | Normal | Emacs @@ -67,7 +66,6 @@ let prompt () = match !current_mode with | Normal -> "sail> " | Evaluation _ -> "eval> " - | Bytecode _ -> "ir> " | Emacs -> "" let eval_clear = ref true @@ -76,7 +74,6 @@ let mode_clear () = match !current_mode with | Normal -> () | Evaluation _ -> if !eval_clear then LNoise.clear_screen () else () - | Bytecode _ -> () (* if !eval_clear then LNoise.clear_screen () else () *) | Emacs -> () let rec user_input callback = @@ -126,22 +123,6 @@ let print_program () = | Evaluation (Done (_, v)) -> print_endline (Value.string_of_value v |> Util.green |> Util.clear) | Evaluation _ -> () - | Bytecode (_, stack) -> - let open Bytecode_interpreter in - let open Bytecode_util in - let pc = stack.top.pc in - let instrs = stack.top.instrs in - for i = 0 to stack.top.pc - 1 do - print_endline (" " ^ Pretty_print_sail.to_string (pp_instr instrs.(i))) - done; - print_endline (">> " ^ Pretty_print_sail.to_string (pp_instr instrs.(stack.top.pc))); - for i = stack.top.pc + 1 to Array.length instrs - 1 do - print_endline (" " ^ Pretty_print_sail.to_string (pp_instr instrs.(i))) - done; - print_endline sep; - print_endline (Util.string_of_list ", " - (fun (id, vl) -> Printf.sprintf "%s = %s" (string_of_id id) (string_of_value vl)) - (Bindings.bindings stack.top.locals)) let rec run () = match !current_mode with @@ -165,7 +146,6 @@ let rec run () = print_endline "Breakpoint"; current_mode := Evaluation frame end - | Bytecode _ -> () let rec run_steps n = print_endline ("step " ^ string_of_int n); @@ -191,7 +171,6 @@ let rec run_steps n = print_endline "Breakpoint"; current_mode := Evaluation frame end - | Bytecode _ -> () let help = function | ":t" | ":type" -> @@ -372,16 +351,19 @@ let handle_input' input = | ":pretty" -> print_endline (Pretty_print_sail.to_string (Latex.defs !Interactive.ast)) | ":compile" -> + (* let open PPrint in let open C_backend in let ast = Process_file.rewrite_ast_c !Interactive.env !Interactive.ast in let ast, env = Specialize.(specialize typ_ord_specialization ast !Interactive.env) in let ctx = initial_ctx env in interactive_bytecode := bytecode_ast ctx (List.map flatten_cdef) ast + *) + () | ":ir" -> print_endline arg; - let open Bytecode in - let open Bytecode_util in + let open Jib in + let open Jib_util in let open PPrint in let is_cdef = function | CDEF_fundef (id, _, _, _) when Id.compare id (mk_id arg) = 0 -> true @@ -426,16 +408,6 @@ let handle_input' input = (* See initial_check.mli for an explanation of why we need this. *) Initial_check.have_undefined_builtins := false; Process_file.clear_symbols () - | ":exec" -> - let open Bytecode_interpreter in - let exp = Type_check.infer_exp !Interactive.env (Initial_check.exp_of_string arg) in - let anf = Anf.anf exp in - let ctx = C_backend.initial_ctx !Interactive.env in - let ctyp = C_backend.ctyp_of_typ ctx (Type_check.typ_of exp) in - let setup, call, cleanup = C_backend.compile_aexp ctx anf in - let instrs = C_backend.flatten_instrs (setup @ [call (CL_id (mk_id "interactive#", ctyp))] @ cleanup) in - current_mode := Bytecode (new_gstate !interactive_bytecode, new_stack instrs); - print_program () | _ -> unrecognised_command cmd end | Expression str -> @@ -538,17 +510,6 @@ let handle_input' input = current_mode := Evaluation frame end end - | Bytecode (gstate, stack) -> - begin match input with - | Command (cmd, arg) -> - () - | Expression str -> - print_endline "Evaluating IR, cannot evaluate expression" - | Empty -> - let gstate, stack = Bytecode_interpreter.step (gstate, stack) in - current_mode := Bytecode (gstate, stack); - print_program () - end let handle_input input = try handle_input' input with diff --git a/src/anf.ml b/src/jib/anf.ml index 5db836e9..16fb6756 100644 --- a/src/anf.ml +++ b/src/jib/anf.ml @@ -50,8 +50,8 @@ open Ast open Ast_util -open Bytecode -open Bytecode_util +open Jib +open Jib_util open Type_check open PPrint diff --git a/src/anf.mli b/src/jib/anf.mli index 6b9c9b51..e8d58fe4 100644 --- a/src/anf.mli +++ b/src/jib/anf.mli @@ -50,7 +50,7 @@ open Ast open Ast_util -open Bytecode +open Jib open Type_check (* The A-normal form (ANF) grammar *) diff --git a/src/c_backend.ml b/src/jib/c_backend.ml index 14930d47..a08261fc 100644 --- a/src/c_backend.ml +++ b/src/jib/c_backend.ml @@ -50,8 +50,9 @@ open Ast open Ast_util -open Bytecode -open Bytecode_util +open Jib +open Jib_compile +open Jib_util open Type_check open PPrint open Value2 @@ -63,9 +64,6 @@ module Big_int = Nat_big_num let c_verbosity = ref 0 let opt_debug_flow_graphs = ref false -let opt_debug_function = ref "" -let opt_trace = ref false -let opt_smt_trace = ref false let opt_static = ref false let opt_no_main = ref false let opt_memo_cache = ref false @@ -108,52 +106,6 @@ let zencode_id = function let max_int n = Big_int.pred (Big_int.pow_int_positive 2 (n - 1)) let min_int n = Big_int.negate (Big_int.pow_int_positive 2 (n - 1)) -(** The context type contains two type-checking - environments. ctx.local_env contains the closest typechecking - environment, usually from the expression we are compiling, whereas - ctx.tc_env is the global type checking environment from - type-checking the entire AST. We also keep track of local variables - in ctx.locals, so we know when their type changes due to flow - typing. *) -type ctx = - { records : (ctyp Bindings.t) Bindings.t; - enums : IdSet.t Bindings.t; - variants : (ctyp Bindings.t) Bindings.t; - tc_env : Env.t; - local_env : Env.t; - locals : (mut * ctyp) Bindings.t; - letbinds : int list; - recursive_functions : IdSet.t; - no_raw : bool; - optimize_smt : bool; - iterate_size : bool; - } - -let initial_ctx env = - { records = Bindings.empty; - enums = Bindings.empty; - variants = Bindings.empty; - tc_env = env; - local_env = env; - locals = Bindings.empty; - letbinds = []; - recursive_functions = IdSet.empty; - no_raw = false; - optimize_smt = true; - iterate_size = false; - } - -let initial_ctx_iterate env = - { (initial_ctx env) with iterate_size = true } - -let rec iterate_size ctx size n m = - if size > 64 then - CT_lint - else if prove __POS__ ctx.local_env (nc_and (nc_lteq (nconstant (min_int size)) n) (nc_lteq m (nconstant (max_int size)))) then - CT_fint size - else - iterate_size ctx (size + 1) n m - (** Convert a sail type into a C-type. This function can be quite slow, because it uses ctx.local_env and SMT to analyse the Sail types and attempts to fit them into the smallest possible C @@ -181,18 +133,12 @@ let rec ctyp_of_typ ctx typ = match nexp_simp n, nexp_simp m with | Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_constant m, _) when Big_int.less_equal (min_int 64) n && Big_int.less_equal m (max_int 64) -> - if ctx.iterate_size then - iterate_size ctx 2 (nconstant n) (nconstant m) - else - CT_fint 64 - | n, m when ctx.optimize_smt -> - if ctx.iterate_size then - iterate_size ctx 2 n m - else if prove __POS__ ctx.local_env (nc_lteq (nconstant (min_int 64)) n) && prove __POS__ ctx.local_env (nc_lteq m (nconstant (max_int 64))) then + CT_fint 64 + | n, m -> + if prove __POS__ ctx.local_env (nc_lteq (nconstant (min_int 64)) n) && prove __POS__ ctx.local_env (nc_lteq m (nconstant (max_int 64))) then CT_fint 64 else CT_lint - | _ -> CT_lint end | Typ_app (id, [A_aux (A_typ typ, _)]) when string_of_id id = "list" -> @@ -209,7 +155,7 @@ let rec ctyp_of_typ ctx typ = let direction = match ord with Ord_aux (Ord_dec, _) -> true | Ord_aux (Ord_inc, _) -> false | _ -> assert false in begin match nexp_simp n with | Nexp_aux (Nexp_constant n, _) when Big_int.less_equal n (Big_int.of_int 64) -> CT_fbits (Big_int.to_int n, direction) - | n when ctx.optimize_smt && prove __POS__ ctx.local_env (nc_lteq n (nint 64)) -> CT_sbits direction + | n when prove __POS__ ctx.local_env (nc_lteq n (nint 64)) -> CT_sbits (64, direction) | _ -> CT_lbits direction end @@ -229,7 +175,7 @@ let rec ctyp_of_typ ctx typ = | Typ_tup typs -> CT_tup (List.map (ctyp_of_typ ctx) typs) - | Typ_exist _ when ctx.optimize_smt -> + | Typ_exist _ -> (* Use Type_check.destruct_exist when optimising with SMT, to ensure that we don't cause any type variable clashes in local_env, and that we can optimize the existential based upon @@ -241,8 +187,6 @@ let rec ctyp_of_typ ctx typ = | None -> raise (Reporting.err_unreachable l __POS__ "Existential cannot be destructured!") end - | Typ_exist (_, _, typ) -> ctyp_of_typ ctx typ - | Typ_var kid -> CT_poly | _ -> c_error ~loc:l ("No C type for type " ^ string_of_typ typ) @@ -586,15 +530,15 @@ let analyze_primop' ctx id args typ = when ord1 = ord2 && n1 + n2 <= 64 -> AE_val (AV_C_fragment (F_op (F_op (vec1, "<<", v_int n2), "|", vec2), typ, CT_fbits (n1 + n2, ord1))) - | "append", [AV_C_fragment (vec1, _, CT_sbits ord1); AV_C_fragment (vec2, _, CT_fbits (n2, ord2))] + | "append", [AV_C_fragment (vec1, _, CT_sbits (64, ord1)); AV_C_fragment (vec2, _, CT_fbits (n2, ord2))] when ord1 = ord2 && is_sbits_typ ctx typ -> AE_val (AV_C_fragment (F_call ("append_sf", [vec1; vec2; v_int n2]), typ, ctyp_of_typ ctx typ)) - | "append", [AV_C_fragment (vec1, _, CT_fbits (n1, ord1)); AV_C_fragment (vec2, _, CT_sbits ord2)] + | "append", [AV_C_fragment (vec1, _, CT_fbits (n1, ord1)); AV_C_fragment (vec2, _, CT_sbits (64, ord2))] when ord1 = ord2 && is_sbits_typ ctx typ -> AE_val (AV_C_fragment (F_call ("append_fs", [vec1; v_int n1; vec2]), typ, ctyp_of_typ ctx typ)) - | "append", [AV_C_fragment (vec1, _, CT_sbits ord1); AV_C_fragment (vec2, _, CT_sbits ord2)] + | "append", [AV_C_fragment (vec1, _, CT_sbits (64, ord1)); AV_C_fragment (vec2, _, CT_sbits (64, ord2))] when ord1 = ord2 && is_sbits_typ ctx typ -> AE_val (AV_C_fragment (F_call ("append_ss", [vec1; vec2]), typ, ctyp_of_typ ctx typ)) @@ -669,867 +613,11 @@ let analyze_primop ctx id args typ = else no_change -(**************************************************************************) -(* 4. Conversion to low-level AST *) -(**************************************************************************) - -(** We now use a low-level AST (see language/bytecode.ott) that is - only slightly abstracted away from C. To be succint in comments we - usually refer to this as Sail IR or IR rather than low-level AST - repeatedly. - - The general idea is ANF expressions are converted into lists of - instructions (type instr) where allocations and deallocations are - now made explicit. ANF values (aval) are mapped to the cval type, - which is even simpler still. Some things are still more abstract - than in C, so the type definitions follow the sail type definition - structure, just with typ (from ast.ml) replaced with - ctyp. Top-level declarations that have no meaning for the backend - are not included at this level. - - The convention used here is that functions of the form compile_X - compile the type X into types in this AST, so compile_aval maps - avals into cvals. Note that the return types for these functions - are often quite complex, and they usually return some tuple - containing setup instructions (to allocate memory for the - expression), cleanup instructions (to deallocate that memory) and - possibly typing information about what has been translated. **) - -let ctype_def_ctyps = function - | CTD_enum _ -> [] - | CTD_struct (_, fields) -> List.map snd fields - | CTD_variant (_, ctors) -> List.map snd ctors - -let cval_ctyp = function (_, ctyp) -> ctyp - -let rec clexp_ctyp = function - | CL_id (_, ctyp) -> ctyp - | CL_field (clexp, field) -> - begin match clexp_ctyp clexp with - | CT_struct (id, ctors) -> - begin - try snd (List.find (fun (id, ctyp) -> string_of_id id = field) ctors) with - | Not_found -> c_error ("Struct type " ^ string_of_id id ^ " does not have a constructor " ^ field) - end - | ctyp -> c_error ("Bad ctyp for CL_field " ^ string_of_ctyp ctyp) - end - | CL_addr clexp -> - begin match clexp_ctyp clexp with - | CT_ref ctyp -> ctyp - | ctyp -> c_error ("Bad ctyp for CL_addr " ^ string_of_ctyp ctyp) - end - | CL_tuple (clexp, n) -> - begin match clexp_ctyp clexp with - | CT_tup typs -> - begin - try List.nth typs n with - | _ -> c_error "Tuple assignment index out of bounds" - end - | ctyp -> c_error ("Bad ctyp for CL_addr " ^ string_of_ctyp ctyp) - end - | CL_have_exception -> CT_bool - | CL_current_exception ctyp -> ctyp - -let cval_rename from_id to_id (frag, ctyp) = (frag_rename from_id to_id frag, ctyp) - -let rec instr_ctyps (I_aux (instr, aux)) = - match instr with - | I_decl (ctyp, _) | I_reset (ctyp, _) | I_clear (ctyp, _) | I_undefined ctyp -> [ctyp] - | I_init (ctyp, _, cval) | I_reinit (ctyp, _, cval) -> [ctyp; cval_ctyp cval] - | I_if (cval, instrs1, instrs2, ctyp) -> - ctyp :: cval_ctyp cval :: List.concat (List.map instr_ctyps instrs1 @ List.map instr_ctyps instrs2) - | I_funcall (clexp, _, _, cvals) -> - clexp_ctyp clexp :: List.map cval_ctyp cvals - | I_copy (clexp, cval) | I_alias (clexp, cval) -> [clexp_ctyp clexp; cval_ctyp cval] - | I_block instrs | I_try_block instrs -> List.concat (List.map instr_ctyps instrs) - | I_throw cval | I_jump (cval, _) | I_return cval -> [cval_ctyp cval] - | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_match_failure -> [] - -let rec c_ast_registers = function - | CDEF_reg_dec (id, ctyp, instrs) :: ast -> (id, ctyp, instrs) :: c_ast_registers ast - | _ :: ast -> c_ast_registers ast - | [] -> [] - -let cdef_ctyps ctx = function - | CDEF_reg_dec (_, ctyp, instrs) -> ctyp :: List.concat (List.map instr_ctyps instrs) - | CDEF_spec (_, ctyps, ctyp) -> ctyp :: ctyps - | CDEF_fundef (id, _, _, instrs) -> - let quant, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_env in - let arg_typs, ret_typ = match fn_typ with - | Typ_fn (arg_typs, ret_typ, _) -> arg_typs, ret_typ - | _ -> assert false - in - let arg_ctyps, ret_ctyp = - List.map (ctyp_of_typ ctx) arg_typs, - ctyp_of_typ { ctx with local_env = add_typquant (id_loc id) quant ctx.local_env } ret_typ - in - ret_ctyp :: arg_ctyps @ List.concat (List.map instr_ctyps instrs) - - | CDEF_startup (id, instrs) | CDEF_finish (id, instrs) -> List.concat (List.map instr_ctyps instrs) - | CDEF_type tdef -> ctype_def_ctyps tdef - | CDEF_let (_, bindings, instrs) -> - List.map snd bindings - @ List.concat (List.map instr_ctyps instrs) - -let is_ct_enum = function - | CT_enum _ -> true - | _ -> false - -let is_ct_variant = function - | CT_variant _ -> true - | _ -> false - -let is_ct_tup = function - | CT_tup _ -> true - | _ -> false - -let is_ct_list = function - | CT_list _ -> true - | _ -> false - -let is_ct_vector = function - | CT_vector _ -> true - | _ -> false - -let is_ct_struct = function - | CT_struct _ -> true - | _ -> false - -let is_ct_ref = function - | CT_ref _ -> true - | _ -> false - -let rec chunkify n xs = - match Util.take n xs, Util.drop n xs with - | xs, [] -> [xs] - | xs, ys -> xs :: chunkify n ys - -let rec compile_aval l ctx = function - | AV_C_fragment (frag, typ, ctyp) -> - let ctyp' = ctyp_of_typ ctx typ in - if not (ctyp_equal ctyp ctyp' || ctx.iterate_size) then - raise (Reporting.err_unreachable l __POS__ (string_of_ctyp ctyp ^ " != " ^ string_of_ctyp ctyp')); - [], (frag, ctyp_of_typ ctx typ), [] - - | AV_id (id, typ) -> - begin - try - let _, ctyp = Bindings.find id ctx.locals in - [], (F_id id, ctyp), [] - with - | Not_found -> - [], (F_id id, ctyp_of_typ ctx (lvar_typ typ)), [] - end - - | AV_ref (id, typ) -> - [], (F_ref id, CT_ref (ctyp_of_typ ctx (lvar_typ typ))), [] - - | AV_lit (L_aux (L_string str, _), typ) -> - [], (F_lit (V_string (String.escaped str)), ctyp_of_typ ctx typ), [] - - | AV_lit (L_aux (L_num n, _), typ) when Big_int.less_equal (min_int 64) n && Big_int.less_equal n (max_int 64) -> - let gs = gensym () in - [iinit CT_lint gs (F_lit (V_int n), CT_fint 64)], - (F_id gs, CT_lint), - [iclear CT_lint gs] - - | AV_lit (L_aux (L_num n, _), typ) -> - let gs = gensym () in - [iinit CT_lint gs (F_lit (V_string (Big_int.to_string n)), CT_string)], - (F_id gs, CT_lint), - [iclear CT_lint gs] - - | AV_lit (L_aux (L_zero, _), _) -> [], (F_lit (V_bit Sail2_values.B0), CT_bit), [] - | AV_lit (L_aux (L_one, _), _) -> [], (F_lit (V_bit Sail2_values.B1), CT_bit), [] - - | AV_lit (L_aux (L_true, _), _) -> [], (F_lit (V_bool true), CT_bool), [] - | AV_lit (L_aux (L_false, _), _) -> [], (F_lit (V_bool false), CT_bool), [] - - | AV_lit (L_aux (L_real str, _), _) -> - let gs = gensym () in - [iinit CT_real gs (F_lit (V_string str), CT_string)], - (F_id gs, CT_real), - [iclear CT_real gs] - - | AV_lit (L_aux (L_unit, _), _) -> [], (F_lit V_unit, CT_unit), [] - - | AV_lit (L_aux (_, l) as lit, _) -> - c_error ~loc:l ("Encountered unexpected literal " ^ string_of_lit lit) - - | AV_tuple avals -> - let elements = List.map (compile_aval l ctx) avals in - let cvals = List.map (fun (_, cval, _) -> cval) elements in - let setup = List.concat (List.map (fun (setup, _, _) -> setup) elements) in - let cleanup = List.concat (List.rev (List.map (fun (_, _, cleanup) -> cleanup) elements)) in - let tup_ctyp = CT_tup (List.map cval_ctyp cvals) in - let gs = gensym () in - setup - @ [idecl tup_ctyp gs] - @ List.mapi (fun n cval -> icopy l (CL_tuple (CL_id (gs, tup_ctyp), n)) cval) cvals, - (F_id gs, CT_tup (List.map cval_ctyp cvals)), - [iclear tup_ctyp gs] - @ cleanup - - | AV_record (fields, typ) -> - let ctyp = ctyp_of_typ ctx typ in - let gs = gensym () in - let compile_fields (id, aval) = - let field_setup, cval, field_cleanup = compile_aval l ctx aval in - field_setup - @ [icopy l (CL_field (CL_id (gs, ctyp), string_of_id id)) cval] - @ field_cleanup - in - [idecl ctyp gs] - @ List.concat (List.map compile_fields (Bindings.bindings fields)), - (F_id gs, ctyp), - [iclear ctyp gs] - - | AV_vector ([], _) -> - c_error "Encountered empty vector literal" - - (* Convert a small bitvector to a uint64_t literal. *) - | AV_vector (avals, typ) when is_bitvector avals && List.length avals <= 64 -> - begin - let bitstring = F_lit (V_bits (List.map value_of_aval_bit avals)) in - let len = List.length avals in - match destruct_vector ctx.tc_env typ with - | Some (_, Ord_aux (Ord_inc, _), _) -> - [], (bitstring, CT_fbits (len, false)), [] - | Some (_, Ord_aux (Ord_dec, _), _) -> - [], (bitstring, CT_fbits (len, true)), [] - | Some _ -> - c_error "Encountered order polymorphic bitvector literal" - | None -> - c_error "Encountered vector literal without vector type" - end - - (* Convert a bitvector literal that is larger than 64-bits to a - variable size bitvector, converting it in 64-bit chunks. *) - | AV_vector (avals, typ) when is_bitvector avals -> - let len = List.length avals in - let bitstring avals = F_lit (V_bits (List.map value_of_aval_bit avals)) in - let first_chunk = bitstring (Util.take (len mod 64) avals) in - let chunks = Util.drop (len mod 64) avals |> chunkify 64 |> List.map bitstring in - let gs = gensym () in - [iinit (CT_lbits true) gs (first_chunk, CT_fbits (len mod 64, true))] - @ List.map (fun chunk -> ifuncall (CL_id (gs, CT_lbits true)) - (mk_id "append_64") - [(F_id gs, CT_lbits true); (chunk, CT_fbits (64, true))]) chunks, - (F_id gs, CT_lbits true), - [iclear (CT_lbits true) gs] - - (* If we have a bitvector value, that isn't a literal then we need to set bits individually. *) - | AV_vector (avals, Typ_aux (Typ_app (id, [_; A_aux (A_order ord, _); A_aux (A_typ (Typ_aux (Typ_id bit_id, _)), _)]), _)) - when string_of_id bit_id = "bit" && string_of_id id = "vector" && List.length avals <= 64 -> - let len = List.length avals in - let direction = match ord with - | Ord_aux (Ord_inc, _) -> false - | Ord_aux (Ord_dec, _) -> true - | Ord_aux (Ord_var _, _) -> c_error "Polymorphic vector direction found" - in - let gs = gensym () in - let ctyp = CT_fbits (len, direction) in - let mask i = V_bits (Util.list_init (63 - i) (fun _ -> Sail2_values.B0) @ [Sail2_values.B1] @ Util.list_init i (fun _ -> Sail2_values.B0)) in - let aval_mask i aval = - let setup, cval, cleanup = compile_aval l ctx aval in - match cval with - | (F_lit (V_bit Sail2_values.B0), _) -> [] - | (F_lit (V_bit Sail2_values.B1), _) -> - [icopy l (CL_id (gs, ctyp)) (F_op (F_id gs, "|", F_lit (mask i)), ctyp)] - | _ -> - setup @ [iif cval [icopy l (CL_id (gs, ctyp)) (F_op (F_id gs, "|", F_lit (mask i)), ctyp)] [] CT_unit] @ cleanup - in - [idecl ctyp gs; - icopy l (CL_id (gs, ctyp)) (F_lit (V_bits (Util.list_init 64 (fun _ -> Sail2_values.B0))), ctyp)] - @ List.concat (List.mapi aval_mask (List.rev avals)), - (F_id gs, ctyp), - [] - - (* Compiling a vector literal that isn't a bitvector *) - | AV_vector (avals, Typ_aux (Typ_app (id, [_; A_aux (A_order ord, _); A_aux (A_typ typ, _)]), _)) - when string_of_id id = "vector" -> - let len = List.length avals in - let direction = match ord with - | Ord_aux (Ord_inc, _) -> false - | Ord_aux (Ord_dec, _) -> true - | Ord_aux (Ord_var _, _) -> c_error "Polymorphic vector direction found" - in - let vector_ctyp = CT_vector (direction, ctyp_of_typ ctx typ) in - let gs = gensym () in - let aval_set i aval = - let setup, cval, cleanup = compile_aval l ctx aval in - setup - @ [iextern (CL_id (gs, vector_ctyp)) - (mk_id "internal_vector_update") - [(F_id gs, vector_ctyp); (F_lit (V_int (Big_int.of_int i)), CT_fint 64); cval]] - @ cleanup - in - [idecl vector_ctyp gs; - iextern (CL_id (gs, vector_ctyp)) (mk_id "internal_vector_init") [(F_lit (V_int (Big_int.of_int len)), CT_fint 64)]] - @ List.concat (List.mapi aval_set (if direction then List.rev avals else avals)), - (F_id gs, vector_ctyp), - [iclear vector_ctyp gs] - - | AV_vector _ as aval -> - c_error ("Have AV_vector: " ^ Pretty_print_sail.to_string (pp_aval aval) ^ " which is not a vector type") - - | AV_list (avals, Typ_aux (typ, _)) -> - let ctyp = match typ with - | Typ_app (id, [A_aux (A_typ typ, _)]) when string_of_id id = "list" -> ctyp_of_typ ctx typ - | _ -> c_error "Invalid list type" - in - let gs = gensym () in - let mk_cons aval = - let setup, cval, cleanup = compile_aval l ctx aval in - setup @ [ifuncall (CL_id (gs, CT_list ctyp)) (mk_id ("cons#" ^ string_of_ctyp ctyp)) [cval; (F_id gs, CT_list ctyp)]] @ cleanup - in - [idecl (CT_list ctyp) gs] - @ List.concat (List.map mk_cons (List.rev avals)), - (F_id gs, CT_list ctyp), - [iclear (CT_list ctyp) gs] - -let compile_funcall l ctx id args typ = - let setup = ref [] in - let cleanup = ref [] in - - let quant, Typ_aux (fn_typ, _) = - try Env.get_val_spec id ctx.local_env - with Type_error _ -> - c_debug (lazy ("Falling back to global env for " ^ string_of_id id)); Env.get_val_spec id ctx.tc_env - in - let arg_typs, ret_typ = match fn_typ with - | Typ_fn (arg_typs, ret_typ, _) -> arg_typs, ret_typ - | _ -> assert false - in - let ctx' = { ctx with local_env = add_typquant (id_loc id) quant ctx.tc_env } in - let arg_ctyps, ret_ctyp = List.map (ctyp_of_typ ctx') arg_typs, ctyp_of_typ ctx' ret_typ in - let final_ctyp = ctyp_of_typ ctx typ in - - let setup_arg ctyp aval = - let arg_setup, cval, arg_cleanup = compile_aval l ctx aval in - setup := List.rev arg_setup @ !setup; - cleanup := arg_cleanup @ !cleanup; - let have_ctyp = cval_ctyp cval in - if is_polymorphic ctyp then - (F_poly (fst cval), have_ctyp) - else if ctyp_equal ctyp have_ctyp then - cval - else - let gs = gensym () in - setup := iinit ctyp gs cval :: !setup; - cleanup := iclear ctyp gs :: !cleanup; - (F_id gs, ctyp) - in - - assert (List.length arg_ctyps = List.length args); - - let setup_args = List.map2 setup_arg arg_ctyps args in - - List.rev !setup, - begin fun clexp -> - if ctyp_equal (clexp_ctyp clexp) ret_ctyp then - ifuncall clexp id setup_args - else - let gs = gensym () in - iblock [idecl ret_ctyp gs; - ifuncall (CL_id (gs, ret_ctyp)) id setup_args; - icopy l clexp (F_id gs, ret_ctyp); - iclear ret_ctyp gs] - end, - !cleanup - -let rec apat_ctyp ctx (AP_aux (apat, _, _)) = - match apat with - | AP_tup apats -> CT_tup (List.map (apat_ctyp ctx) apats) - | AP_global (_, typ) -> ctyp_of_typ ctx typ - | AP_cons (apat, _) -> CT_list (apat_ctyp ctx apat) - | AP_wild typ | AP_nil typ | AP_id (_, typ) -> ctyp_of_typ ctx typ - | AP_app (_, _, typ) -> ctyp_of_typ ctx typ - -let rec compile_match ctx (AP_aux (apat_aux, env, l)) cval case_label = - let ctx = { ctx with local_env = env } in - match apat_aux, cval with - | AP_id (pid, _), (frag, ctyp) when Env.is_union_constructor pid ctx.tc_env -> - [ijump (F_op (F_field (frag, "kind"), "!=", F_lit (V_ctor_kind (string_of_id pid))), CT_bool) case_label], - [], - ctx - - | AP_global (pid, typ), (frag, ctyp) -> - let global_ctyp = ctyp_of_typ ctx typ in - [icopy l (CL_id (pid, global_ctyp)) cval], [], ctx - - | AP_id (pid, _), (frag, ctyp) when is_ct_enum ctyp -> - begin match Env.lookup_id pid ctx.tc_env with - | Unbound -> [idecl ctyp pid; icopy l (CL_id (pid, ctyp)) (frag, ctyp)], [], ctx - | _ -> [ijump (F_op (F_id pid, "!=", frag), CT_bool) case_label], [], ctx - end - - | AP_id (pid, typ), _ -> - let ctyp = cval_ctyp cval in - let id_ctyp = ctyp_of_typ ctx typ in - c_debug (lazy ("Adding local " ^ string_of_id pid ^ " : " ^ string_of_ctyp id_ctyp)); - let ctx = { ctx with locals = Bindings.add pid (Immutable, id_ctyp) ctx.locals } in - [idecl id_ctyp pid; icopy l (CL_id (pid, id_ctyp)) cval], [iclear id_ctyp pid], ctx - - | AP_tup apats, (frag, ctyp) -> - begin - let get_tup n ctyp = (F_field (frag, "ztup" ^ string_of_int n), ctyp) in - let fold (instrs, cleanup, n, ctx) apat ctyp = - let instrs', cleanup', ctx = compile_match ctx apat (get_tup n ctyp) case_label in - instrs @ instrs', cleanup' @ cleanup, n + 1, ctx - in - match ctyp with - | CT_tup ctyps -> - let instrs, cleanup, _, ctx = List.fold_left2 fold ([], [], 0, ctx) apats ctyps in - instrs, cleanup, ctx - | _ -> failwith ("AP_tup with ctyp " ^ string_of_ctyp ctyp) - end - - | AP_app (ctor, apat, variant_typ), (frag, ctyp) -> - begin match ctyp with - | CT_variant (_, ctors) -> - let ctor_c_id = string_of_id ctor in - let ctor_ctyp = Bindings.find ctor (ctor_bindings ctors) in - (* These should really be the same, something has gone wrong if they are not. *) - if ctyp_equal ctor_ctyp (ctyp_of_typ ctx variant_typ) then - c_error ~loc:l (Printf.sprintf "%s is not the same type as %s" (string_of_ctyp ctor_ctyp) (string_of_ctyp (ctyp_of_typ ctx variant_typ))) - else (); - let ctor_c_id, ctor_ctyp = - if is_polymorphic ctor_ctyp then - let unification = List.map ctyp_suprema (ctyp_unify ctor_ctyp (apat_ctyp ctx apat)) in - (if List.length unification > 0 then - ctor_c_id ^ "_" ^ Util.string_of_list "_" (fun ctyp -> Util.zencode_string (string_of_ctyp ctyp)) unification - else - ctor_c_id), - ctyp_suprema (apat_ctyp ctx apat) - else - ctor_c_id, ctor_ctyp - in - let instrs, cleanup, ctx = compile_match ctx apat ((F_field (frag, Util.zencode_string ctor_c_id), ctor_ctyp)) case_label in - [ijump (F_op (F_field (frag, "kind"), "!=", F_lit (V_ctor_kind ctor_c_id)), CT_bool) case_label] - @ instrs, - cleanup, - ctx - | ctyp -> - c_error ~loc:l (Printf.sprintf "Variant constructor %s : %s matching against non-variant type %s : %s" - (string_of_id ctor) - (string_of_typ variant_typ) - (string_of_fragment ~zencode:false frag) - (string_of_ctyp ctyp)) - end - - | AP_wild _, _ -> [], [], ctx - - | AP_cons (hd_apat, tl_apat), (frag, CT_list ctyp) -> - let hd_setup, hd_cleanup, ctx = compile_match ctx hd_apat (F_field (F_unary ("*", frag), "hd"), ctyp) case_label in - let tl_setup, tl_cleanup, ctx = compile_match ctx tl_apat (F_field (F_unary ("*", frag), "tl"), CT_list ctyp) case_label in - [ijump (F_op (frag, "==", F_lit V_null), CT_bool) case_label] @ hd_setup @ tl_setup, tl_cleanup @ hd_cleanup, ctx - - | AP_cons _, (_, _) -> c_error "Tried to pattern match cons on non list type" - - | AP_nil _, (frag, _) -> [ijump (F_op (frag, "!=", F_lit V_null), CT_bool) case_label], [], ctx - -let unit_fragment = (F_lit V_unit, CT_unit) - -(** GLOBAL: label_counter is used to make sure all labels have unique - names. Like gensym_counter it should be safe to reset between - top-level definitions. **) -let label_counter = ref 0 - -let label str = - let str = str ^ string_of_int !label_counter in - incr label_counter; - str - -let pointer_assign ctyp1 ctyp2 = - match ctyp1 with - | CT_ref ctyp1 -> true - | _ -> false - -let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = - let ctx = { ctx with local_env = env } in - match aexp_aux with - | AE_let (mut, id, binding_typ, binding, (AE_aux (_, body_env, _) as body), body_typ) -> - let binding_ctyp = ctyp_of_typ { ctx with local_env = body_env } binding_typ in - let setup, call, cleanup = compile_aexp ctx binding in - let letb_setup, letb_cleanup = - [idecl binding_ctyp id; iblock (setup @ [call (CL_id (id, binding_ctyp))] @ cleanup)], [iclear binding_ctyp id] - in - let ctx = { ctx with locals = Bindings.add id (mut, binding_ctyp) ctx.locals } in - let setup, call, cleanup = compile_aexp ctx body in - letb_setup @ setup, call, cleanup @ letb_cleanup - - | AE_app (id, vs, typ) -> - compile_funcall l ctx id vs typ - - | AE_val aval -> - let setup, cval, cleanup = compile_aval l ctx aval in - setup, (fun clexp -> icopy l clexp cval), cleanup - - (* Compile case statements *) - | AE_case (aval, cases, typ) -> - let ctyp = ctyp_of_typ ctx typ in - let aval_setup, cval, aval_cleanup = compile_aval l ctx aval in - let case_return_id = gensym () in - let finish_match_label = label "finish_match_" in - let compile_case (apat, guard, body) = - let trivial_guard = match guard with - | AE_aux (AE_val (AV_lit (L_aux (L_true, _), _)), _, _) - | AE_aux (AE_val (AV_C_fragment (F_lit (V_bool true), _, _)), _, _) -> true - | _ -> false - in - let case_label = label "case_" in - c_debug (lazy ("Compiling match")); - let destructure, destructure_cleanup, ctx = compile_match ctx apat cval case_label in - c_debug (lazy ("Compiled match")); - let guard_setup, guard_call, guard_cleanup = compile_aexp ctx guard in - let body_setup, body_call, body_cleanup = compile_aexp ctx body in - let gs = gensym () in - let case_instrs = - destructure @ [icomment "end destructuring"] - @ (if not trivial_guard then - guard_setup @ [idecl CT_bool gs; guard_call (CL_id (gs, CT_bool))] @ guard_cleanup - @ [iif (F_unary ("!", F_id gs), CT_bool) (destructure_cleanup @ [igoto case_label]) [] CT_unit] - @ [icomment "end guard"] - else []) - @ body_setup @ [body_call (CL_id (case_return_id, ctyp))] @ body_cleanup @ destructure_cleanup - @ [igoto finish_match_label] - in - if is_dead_aexp body then - [ilabel case_label] - else - [iblock case_instrs; ilabel case_label] - in - [icomment "begin match"] - @ aval_setup @ [idecl ctyp case_return_id] - @ List.concat (List.map compile_case cases) - @ [imatch_failure ()] - @ [ilabel finish_match_label], - (fun clexp -> icopy l clexp (F_id case_return_id, ctyp)), - [iclear ctyp case_return_id] - @ aval_cleanup - @ [icomment "end match"] - - (* Compile try statement *) - | AE_try (aexp, cases, typ) -> - let ctyp = ctyp_of_typ ctx typ in - let aexp_setup, aexp_call, aexp_cleanup = compile_aexp ctx aexp in - let try_return_id = gensym () in - let handled_exception_label = label "handled_exception_" in - let fallthrough_label = label "fallthrough_exception_" in - let compile_case (apat, guard, body) = - let trivial_guard = match guard with - | AE_aux (AE_val (AV_lit (L_aux (L_true, _), _)), _, _) - | AE_aux (AE_val (AV_C_fragment (F_lit (V_bool true), _, _)), _, _) -> true - | _ -> false - in - let try_label = label "try_" in - let exn_cval = (F_current_exception, ctyp_of_typ ctx (mk_typ (Typ_id (mk_id "exception")))) in - let destructure, destructure_cleanup, ctx = compile_match ctx apat exn_cval try_label in - let guard_setup, guard_call, guard_cleanup = compile_aexp ctx guard in - let body_setup, body_call, body_cleanup = compile_aexp ctx body in - let gs = gensym () in - let case_instrs = - destructure @ [icomment "end destructuring"] - @ (if not trivial_guard then - guard_setup @ [idecl CT_bool gs; guard_call (CL_id (gs, CT_bool))] @ guard_cleanup - @ [ijump (F_unary ("!", F_id gs), CT_bool) try_label] - @ [icomment "end guard"] - else []) - @ body_setup @ [body_call (CL_id (try_return_id, ctyp))] @ body_cleanup @ destructure_cleanup - @ [igoto handled_exception_label] - in - [iblock case_instrs; ilabel try_label] - in - assert (ctyp_equal ctyp (ctyp_of_typ ctx typ)); - [idecl ctyp try_return_id; - itry_block (aexp_setup @ [aexp_call (CL_id (try_return_id, ctyp))] @ aexp_cleanup); - ijump (F_unary ("!", F_have_exception), CT_bool) handled_exception_label] - @ List.concat (List.map compile_case cases) - @ [igoto fallthrough_label; - ilabel handled_exception_label; - icopy l CL_have_exception (F_lit (V_bool false), CT_bool); - ilabel fallthrough_label], - (fun clexp -> icopy l clexp (F_id try_return_id, ctyp)), - [] - - | AE_if (aval, then_aexp, else_aexp, if_typ) -> - if is_dead_aexp then_aexp then - compile_aexp ctx else_aexp - else if is_dead_aexp else_aexp then - compile_aexp ctx then_aexp - else - let if_ctyp = ctyp_of_typ ctx if_typ in - let compile_branch aexp = - let setup, call, cleanup = compile_aexp ctx aexp in - fun clexp -> setup @ [call clexp] @ cleanup - in - let setup, cval, cleanup = compile_aval l ctx aval in - setup, - (fun clexp -> iif cval - (compile_branch then_aexp clexp) - (compile_branch else_aexp clexp) - if_ctyp), - cleanup - - (* FIXME: AE_record_update could be AV_record_update - would reduce some copying. *) - | AE_record_update (aval, fields, typ) -> - let ctyp = ctyp_of_typ ctx typ in - let ctors = match ctyp with - | CT_struct (_, ctors) -> List.fold_left (fun m (k, v) -> Bindings.add k v m) Bindings.empty ctors - | _ -> c_error "Cannot perform record update for non-record type" - in - let gs = gensym () in - let compile_fields (id, aval) = - let field_setup, cval, field_cleanup = compile_aval l ctx aval in - field_setup - @ [icopy l (CL_field (CL_id (gs, ctyp), string_of_id id)) cval] - @ field_cleanup - in - let setup, cval, cleanup = compile_aval l ctx aval in - [idecl ctyp gs] - @ setup - @ [icopy l (CL_id (gs, ctyp)) cval] - @ cleanup - @ List.concat (List.map compile_fields (Bindings.bindings fields)), - (fun clexp -> icopy l clexp (F_id gs, ctyp)), - [iclear ctyp gs] - - | AE_short_circuit (SC_and, aval, aexp) -> - let left_setup, cval, left_cleanup = compile_aval l ctx aval in - let right_setup, call, right_cleanup = compile_aexp ctx aexp in - let gs = gensym () in - left_setup - @ [ idecl CT_bool gs; - iif cval - (right_setup @ [call (CL_id (gs, CT_bool))] @ right_cleanup) - [icopy l (CL_id (gs, CT_bool)) (F_lit (V_bool false), CT_bool)] - CT_bool ] - @ left_cleanup, - (fun clexp -> icopy l clexp (F_id gs, CT_bool)), - [] - | AE_short_circuit (SC_or, aval, aexp) -> - let left_setup, cval, left_cleanup = compile_aval l ctx aval in - let right_setup, call, right_cleanup = compile_aexp ctx aexp in - let gs = gensym () in - left_setup - @ [ idecl CT_bool gs; - iif cval - [icopy l (CL_id (gs, CT_bool)) (F_lit (V_bool true), CT_bool)] - (right_setup @ [call (CL_id (gs, CT_bool))] @ right_cleanup) - CT_bool ] - @ left_cleanup, - (fun clexp -> icopy l clexp (F_id gs, CT_bool)), - [] - - (* This is a faster assignment rule for updating fields of a - struct. Turned on by !optimize_struct_updates. *) - | AE_assign (id, assign_typ, AE_aux (AE_record_update (AV_id (rid, _), fields, typ), _, _)) - when Id.compare id rid = 0 && !optimize_struct_updates -> - c_debug (lazy ("Optimizing struct update")); - let compile_fields (field_id, aval) = - let field_setup, cval, field_cleanup = compile_aval l ctx aval in - field_setup - @ [icopy l (CL_field (CL_id (id, ctyp_of_typ ctx typ), string_of_id field_id)) cval] - @ field_cleanup - in - List.concat (List.map compile_fields (Bindings.bindings fields)), - (fun clexp -> icopy l clexp unit_fragment), - [] - - | AE_assign (id, assign_typ, aexp) -> - let assign_ctyp = - match Bindings.find_opt id ctx.locals with - | Some (_, ctyp) -> ctyp - | None -> ctyp_of_typ ctx assign_typ - in - let setup, call, cleanup = compile_aexp ctx aexp in - setup @ [call (CL_id (id, assign_ctyp))], (fun clexp -> icopy l clexp unit_fragment), cleanup - - | AE_block (aexps, aexp, _) -> - let block = compile_block ctx aexps in - let setup, call, cleanup = compile_aexp ctx aexp in - block @ setup, call, cleanup - - | AE_loop (While, cond, body) -> - let loop_start_label = label "while_" in - let loop_end_label = label "wend_" in - let cond_setup, cond_call, cond_cleanup = compile_aexp ctx cond in - let body_setup, body_call, body_cleanup = compile_aexp ctx body in - let gs = gensym () in - let unit_gs = gensym () in - let loop_test = (F_unary ("!", F_id gs), CT_bool) in - [idecl CT_bool gs; idecl CT_unit unit_gs] - @ [ilabel loop_start_label] - @ [iblock (cond_setup - @ [cond_call (CL_id (gs, CT_bool))] - @ cond_cleanup - @ [ijump loop_test loop_end_label] - @ body_setup - @ [body_call (CL_id (unit_gs, CT_unit))] - @ body_cleanup - @ [igoto loop_start_label])] - @ [ilabel loop_end_label], - (fun clexp -> icopy l clexp unit_fragment), - [] - - | AE_loop (Until, cond, body) -> - let loop_start_label = label "repeat_" in - let loop_end_label = label "until_" in - let cond_setup, cond_call, cond_cleanup = compile_aexp ctx cond in - let body_setup, body_call, body_cleanup = compile_aexp ctx body in - let gs = gensym () in - let unit_gs = gensym () in - let loop_test = (F_id gs, CT_bool) in - [idecl CT_bool gs; idecl CT_unit unit_gs] - @ [ilabel loop_start_label] - @ [iblock (body_setup - @ [body_call (CL_id (unit_gs, CT_unit))] - @ body_cleanup - @ cond_setup - @ [cond_call (CL_id (gs, CT_bool))] - @ cond_cleanup - @ [ijump loop_test loop_end_label] - @ [igoto loop_start_label])] - @ [ilabel loop_end_label], - (fun clexp -> icopy l clexp unit_fragment), - [] - - | AE_cast (aexp, typ) -> compile_aexp ctx aexp - - | AE_return (aval, typ) -> - let fn_return_ctyp = match Env.get_ret_typ env with - | Some typ -> ctyp_of_typ ctx typ - | None -> c_error ~loc:l "No function return type found when compiling return statement" - in - (* Cleanup info will be re-added by fix_early_return *) - let return_setup, cval, _ = compile_aval l ctx aval in - let creturn = - if ctyp_equal fn_return_ctyp (cval_ctyp cval) then - [ireturn cval] - else - let gs = gensym () in - [idecl fn_return_ctyp gs; - icopy l (CL_id (gs, fn_return_ctyp)) cval; - ireturn (F_id gs, fn_return_ctyp)] - in - return_setup @ creturn, - (fun clexp -> icomment "unreachable after return"), - [] - - | AE_throw (aval, typ) -> - (* Cleanup info will be handled by fix_exceptions *) - let throw_setup, cval, _ = compile_aval l ctx aval in - throw_setup @ [ithrow cval], - (fun clexp -> icomment "unreachable after throw"), - [] - - | AE_field (aval, id, typ) -> - let ctyp = ctyp_of_typ ctx typ in - let setup, cval, cleanup = compile_aval l ctx aval in - setup, - (fun clexp -> icopy l clexp (F_field (fst cval, Util.zencode_string (string_of_id id)), ctyp)), - cleanup - - | AE_for (loop_var, loop_from, loop_to, loop_step, Ord_aux (ord, _), body) -> - (* We assume that all loop indices are safe to put in a CT_fint. *) - let ctx = { ctx with locals = Bindings.add loop_var (Immutable, CT_fint 64) ctx.locals } in - - let is_inc = match ord with - | Ord_inc -> true - | Ord_dec -> false - | Ord_var _ -> c_error "Polymorphic loop direction in C backend" - in - - (* Loop variables *) - let from_setup, from_call, from_cleanup = compile_aexp ctx loop_from in - let from_gs = gensym () in - let to_setup, to_call, to_cleanup = compile_aexp ctx loop_to in - let to_gs = gensym () in - let step_setup, step_call, step_cleanup = compile_aexp ctx loop_step in - let step_gs = gensym () in - let variable_init gs setup call cleanup = - [idecl (CT_fint 64) gs; - iblock (setup @ [call (CL_id (gs, CT_fint 64))] @ cleanup)] - in - - let loop_start_label = label "for_start_" in - let loop_end_label = label "for_end_" in - let body_setup, body_call, body_cleanup = compile_aexp ctx body in - let body_gs = gensym () in - - variable_init from_gs from_setup from_call from_cleanup - @ variable_init to_gs to_setup to_call to_cleanup - @ variable_init step_gs step_setup step_call step_cleanup - @ [iblock ([idecl (CT_fint 64) loop_var; - icopy l (CL_id (loop_var, (CT_fint 64))) (F_id from_gs, (CT_fint 64)); - idecl CT_unit body_gs; - iblock ([ilabel loop_start_label] - @ [ijump (F_op (F_id loop_var, (if is_inc then ">" else "<"), F_id to_gs), CT_bool) loop_end_label] - @ body_setup - @ [body_call (CL_id (body_gs, CT_unit))] - @ body_cleanup - @ [icopy l (CL_id (loop_var, (CT_fint 64))) - (F_op (F_id loop_var, (if is_inc then "+" else "-"), F_id step_gs), (CT_fint 64))] - @ [igoto loop_start_label]); - ilabel loop_end_label])], - (fun clexp -> icopy l clexp unit_fragment), - [] - -and compile_block ctx = function - | [] -> [] - | exp :: exps -> - let setup, call, cleanup = compile_aexp ctx exp in - let rest = compile_block ctx exps in - let gs = gensym () in - iblock (setup @ [idecl CT_unit gs; call (CL_id (gs, CT_unit))] @ cleanup) :: rest - -(** Compile a sail type definition into a IR one. Most of the - actual work of translating the typedefs into C is done by the code - generator, as it's easy to keep track of structs, tuples and unions - in their sail form at this level, and leave the fiddly details of - how they get mapped to C in the next stage. This function also adds - details of the types it compiles to the context, ctx, which is why - it returns a ctypdef * ctx pair. **) -let compile_type_def ctx (TD_aux (type_def, _)) = - match type_def with - | TD_enum (id, ids, _) -> - CTD_enum (id, ids), - { ctx with enums = Bindings.add id (IdSet.of_list ids) ctx.enums } - - | TD_record (id, _, ctors, _) -> - let ctors = List.fold_left (fun ctors (typ, id) -> Bindings.add id (ctyp_of_typ ctx typ) ctors) Bindings.empty ctors in - CTD_struct (id, Bindings.bindings ctors), - { ctx with records = Bindings.add id ctors ctx.records } - - | TD_variant (id, typq, tus, _) -> - let compile_tu = function - | Tu_aux (Tu_ty_id (typ, id), _) -> - let ctx = { ctx with local_env = add_typquant (id_loc id) typq ctx.local_env } in - ctyp_of_typ ctx typ, id - in - let ctus = List.fold_left (fun ctus (ctyp, id) -> Bindings.add id ctyp ctus) Bindings.empty (List.map compile_tu tus) in - CTD_variant (id, Bindings.bindings ctus), - { ctx with variants = Bindings.add id ctus ctx.variants } - - (* Will be re-written before here, see bitfield.ml *) - | TD_bitfield _ -> failwith "Cannot compile TD_bitfield" - (* All type abbreviations are filtered out in compile_def *) - | TD_abbrev _ -> assert false - -let instr_split_at f = - let rec instr_split_at' f before = function - | [] -> (List.rev before, []) - | instr :: instrs when f instr -> (List.rev before, instr :: instrs) - | instr :: instrs -> instr_split_at' f (instr :: before) instrs - in - instr_split_at' f [] - let generate_cleanup instrs = let generate_cleanup' (I_aux (instr, _)) = match instr with - | I_init (ctyp, id, cval) when not (is_stack_ctyp ctyp) -> [(id, iclear ctyp id)] - | I_decl (ctyp, id) when not (is_stack_ctyp ctyp) -> [(id, iclear ctyp id)] + | I_init (ctyp, id, cval) -> [(id, iclear ctyp id)] + | I_decl (ctyp, id) -> [(id, iclear ctyp id)] | instr -> [] in let is_clear ids = function @@ -1552,365 +640,103 @@ let generate_cleanup instrs = flow to cleanup heap-allocated variables correctly when a function terminates early. See the generate_cleanup function for how this is done. *) -let fix_early_return ret ctx instrs = +let fix_early_heap_return ret ret_ctyp instrs = let end_function_label = label "end_function_" in let is_return_recur (I_aux (instr, _)) = match instr with - | I_return _ | I_if _ | I_block _ -> true + | I_if _ | I_block _ | I_end | I_funcall _ | I_copy _ | I_undefined _ -> true | _ -> false in - let rec rewrite_return historic instrs = + let rec rewrite_return instrs = match instr_split_at is_return_recur instrs with | instrs, [] -> instrs | before, I_aux (I_block instrs, _) :: after -> before - @ [iblock (rewrite_return (historic @ before) instrs)] - @ rewrite_return (historic @ before) after + @ [iblock (rewrite_return instrs)] + @ rewrite_return after | before, I_aux (I_if (cval, then_instrs, else_instrs, ctyp), _) :: after -> - let historic = historic @ before in before - @ [iif cval (rewrite_return historic then_instrs) (rewrite_return historic else_instrs) ctyp] - @ rewrite_return historic after - | before, I_aux (I_return cval, (_, l)) :: after -> - let cleanup_label = label "cleanup_" in - let end_cleanup_label = label "end_cleanup_" in + @ [iif cval (rewrite_return then_instrs) (rewrite_return else_instrs) ctyp] + @ rewrite_return after + | before, I_aux (I_funcall (CL_return ctyp, extern, fid, args), aux) :: after -> + before + @ [I_aux (I_funcall (CL_addr (CL_id (ret, CT_ref ctyp)), extern, fid, args), aux)] + @ rewrite_return after + | before, I_aux (I_copy (CL_return ctyp, cval), aux) :: after -> + before + @ [I_aux (I_copy (CL_addr (CL_id (ret, CT_ref ctyp)), cval), aux)] + @ rewrite_return after + | before, I_aux ((I_end | I_undefined _), _) :: after -> before - @ [icopy l ret cval; - igoto cleanup_label] - (* This is probably dead code until cleanup_label, but how can we be sure there are no jumps into it? *) - @ rewrite_return (historic @ before) after - @ [igoto end_cleanup_label] - @ [ilabel cleanup_label] - @ generate_cleanup (historic @ before) @ [igoto end_function_label] - @ [ilabel end_cleanup_label] + @ rewrite_return after + | before, (I_aux ((I_copy _ | I_funcall _), _) as instr) :: after -> + before @ instr :: rewrite_return after | _, _ -> assert false in - rewrite_return [] instrs + rewrite_return instrs @ [ilabel end_function_label] (* This is like fix_early_return, but for stack allocated returns. *) -let fix_early_stack_return ctx instrs = +let fix_early_stack_return ret ret_ctyp instrs = let is_return_recur (I_aux (instr, _)) = match instr with - | I_return _ | I_if _ | I_block _ -> true + | I_if _ | I_block _ | I_end | I_funcall _ | I_copy _ -> true | _ -> false in - let rec rewrite_return historic instrs = + let rec rewrite_return instrs = match instr_split_at is_return_recur instrs with | instrs, [] -> instrs | before, I_aux (I_block instrs, _) :: after -> before - @ [iblock (rewrite_return (historic @ before) instrs)] - @ rewrite_return (historic @ before) after + @ [iblock (rewrite_return instrs)] + @ rewrite_return after | before, I_aux (I_if (cval, then_instrs, else_instrs, ctyp), _) :: after -> - let historic = historic @ before in before - @ [iif cval (rewrite_return historic then_instrs) (rewrite_return historic else_instrs) ctyp] - @ rewrite_return historic after - | before, (I_aux (I_return cval, _) as ret) :: after -> + @ [iif cval (rewrite_return then_instrs) (rewrite_return else_instrs) ctyp] + @ rewrite_return after + | before, I_aux (I_funcall (CL_return ctyp, extern, fid, args), aux) :: after -> before - @ [icomment "early return cleanup"] - @ generate_cleanup (historic @ before) - @ [ret] - (* There could be jumps into here *) - @ rewrite_return (historic @ before) after - | _, _ -> assert false - in - rewrite_return [] instrs - -let fix_exception_block ?return:(return=None) ctx instrs = - let end_block_label = label "end_block_exception_" in - let is_exception_stop (I_aux (instr, _)) = - match instr with - | I_throw _ | I_if _ | I_block _ | I_funcall _ -> true - | _ -> false - in - (* In this function 'after' is instructions after the one we've - matched on, 'before is instructions before the instruction we've - matched with, but after the previous match, and 'historic' are - all the befores from previous matches. *) - let rec rewrite_exception historic instrs = - match instr_split_at is_exception_stop instrs with - | instrs, [] -> instrs - | before, I_aux (I_block instrs, _) :: after -> + @ [I_aux (I_funcall (CL_id (ret, ctyp), extern, fid, args), aux)] + @ rewrite_return after + | before, I_aux (I_copy (CL_return ctyp, cval), aux) :: after -> before - @ [iblock (rewrite_exception (historic @ before) instrs)] - @ rewrite_exception (historic @ before) after - | before, I_aux (I_if (cval, then_instrs, else_instrs, ctyp), _) :: after -> - let historic = historic @ before in - before - @ [iif cval (rewrite_exception historic then_instrs) (rewrite_exception historic else_instrs) ctyp] - @ rewrite_exception historic after - | before, I_aux (I_throw cval, (_, l)) :: after -> + @ [I_aux (I_copy (CL_id (ret, ctyp), cval), aux)] + @ rewrite_return after + | before, I_aux (I_end, _) :: after -> before - @ [icopy l (CL_current_exception (cval_ctyp cval)) cval; - icopy l CL_have_exception (F_lit (V_bool true), CT_bool)] - @ generate_cleanup (historic @ before) - @ [igoto end_block_label] - @ rewrite_exception (historic @ before) after - | before, (I_aux (I_funcall (x, _, f, args), _) as funcall) :: after -> - let effects = match Env.get_val_spec f ctx.tc_env with - | _, Typ_aux (Typ_fn (_, _, effects), _) -> effects - | exception (Type_error _) -> no_effect (* nullary union constructor, so no val spec *) - | _ -> assert false (* valspec must have function type *) - in - if has_effect effects BE_escape then - before - @ [funcall; - iif (F_have_exception, CT_bool) (generate_cleanup (historic @ before) @ [igoto end_block_label]) [] CT_unit] - @ rewrite_exception (historic @ before) after - else - before @ funcall :: rewrite_exception (historic @ before) after - | _, _ -> assert false (* unreachable *) - in - match return with - | None -> - rewrite_exception [] instrs @ [ilabel end_block_label] - | Some ctyp -> - rewrite_exception [] instrs @ [ilabel end_block_label; iundefined ctyp] - -let rec map_try_block f (I_aux (instr, aux)) = - let instr = match instr with - | I_decl _ | I_reset _ | I_init _ | I_reinit _ -> instr - | I_if (cval, instrs1, instrs2, ctyp) -> - I_if (cval, List.map (map_try_block f) instrs1, List.map (map_try_block f) instrs2, ctyp) - | I_funcall _ | I_copy _ | I_alias _ | I_clear _ | I_throw _ | I_return _ -> instr - | I_block instrs -> I_block (List.map (map_try_block f) instrs) - | I_try_block instrs -> I_try_block (f (List.map (map_try_block f) instrs)) - | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_jump _ | I_match_failure | I_undefined _ -> instr + @ [ireturn (F_id ret, ret_ctyp)] + @ rewrite_return after + | before, (I_aux ((I_copy _ | I_funcall _), _) as instr) :: after -> + before @ instr :: rewrite_return after + | _, _ -> assert false in - I_aux (instr, aux) - -let fix_exception ?return:(return=None) ctx instrs = - let instrs = List.map (map_try_block (fix_exception_block ctx)) instrs in - fix_exception_block ~return:return ctx instrs - -let rec compile_arg_pat ctx label (P_aux (p_aux, (l, _)) as pat) ctyp = - match p_aux with - | P_id id -> (id, ([], [])) - | P_wild -> let gs = gensym () in (gs, ([], [])) - | P_tup [] | P_lit (L_aux (L_unit, _)) -> let gs = gensym () in (gs, ([], [])) - | P_var (pat, _) -> compile_arg_pat ctx label pat ctyp - | P_typ (_, pat) -> compile_arg_pat ctx label pat ctyp - | _ -> - let apat = anf_pat pat in - let gs = gensym () in - let destructure, cleanup, _ = compile_match ctx apat (F_id gs, ctyp) label in - (gs, (destructure, cleanup)) + rewrite_return instrs -let rec compile_arg_pats ctx label (P_aux (p_aux, (l, _)) as pat) ctyps = - match p_aux with - | P_typ (_, pat) -> compile_arg_pats ctx label pat ctyps - | P_tup pats when List.length pats = List.length ctyps -> - [], List.map2 (fun pat ctyp -> compile_arg_pat ctx label pat ctyp) pats ctyps, [] - | _ when List.length ctyps = 1 -> - [], [compile_arg_pat ctx label pat (List.nth ctyps 0)], [] +let rec insert_heap_returns ret_ctyps = function + | (CDEF_spec (id, _, ret_ctyp) as cdef) :: cdefs -> + cdef :: insert_heap_returns (Bindings.add id ret_ctyp ret_ctyps) cdefs - | _ -> - let arg_id, (destructure, cleanup) = compile_arg_pat ctx label pat (CT_tup ctyps) in - let new_ids = List.map (fun ctyp -> gensym (), ctyp) ctyps in - destructure - @ [idecl (CT_tup ctyps) arg_id] - @ List.mapi (fun i (id, ctyp) -> icopy l (CL_tuple (CL_id (arg_id, CT_tup ctyps), i)) (F_id id, ctyp)) new_ids, - List.map (fun (id, _) -> id, ([], [])) new_ids, - [iclear (CT_tup ctyps) arg_id] - @ cleanup - -let combine_destructure_cleanup xs = List.concat (List.map fst xs), List.concat (List.rev (List.map snd xs)) - -let fix_destructure fail_label = function - | ([], cleanup) -> ([], cleanup) - | destructure, cleanup -> - let body_label = label "fundef_body_" in - (destructure @ [igoto body_label; ilabel fail_label; imatch_failure (); ilabel body_label], cleanup) - -let letdef_count = ref 0 - -(** Compile a Sail toplevel definition into an IR definition **) -let rec compile_def n total ctx def = - match def with - | DEF_fundef (FD_aux (FD_function (_, _, _, [FCL_aux (FCL_Funcl (id, _), _)]), _)) - when !opt_memo_cache -> - let digest = - def |> Pretty_print_sail.doc_def |> Pretty_print_sail.to_string |> Digest.string - in - let cachefile = Filename.concat "_sbuild" ("ccache" ^ Digest.to_hex digest) in - let cached = - if Sys.file_exists cachefile then - let in_chan = open_in cachefile in - try - let compiled = Marshal.from_channel in_chan in - close_in in_chan; - Some (compiled, ctx) - with - | _ -> close_in in_chan; None - else - None - in - begin match cached with - | Some (compiled, ctx) -> - Util.progress "Compiling " (string_of_id id) n total; - compiled, ctx + | CDEF_fundef (id, None, args, body) :: cdefs -> + let gs = gensym () in + begin match Bindings.find_opt id ret_ctyps with | None -> - let compiled, ctx = compile_def' n total ctx def in - let out_chan = open_out cachefile in - Marshal.to_channel out_chan compiled [Marshal.Closures]; - close_out out_chan; - compiled, ctx + raise (Reporting.err_general (id_loc id) ("Cannot find return type for function " ^ string_of_id id)) + | Some ret_ctyp when not (is_stack_ctyp ret_ctyp) -> + CDEF_fundef (id, Some gs, args, fix_early_heap_return gs ret_ctyp body) + :: insert_heap_returns ret_ctyps cdefs + | Some ret_ctyp -> + CDEF_fundef (id, None, args, fix_early_stack_return gs ret_ctyp (idecl ret_ctyp gs :: body)) + :: insert_heap_returns ret_ctyps cdefs end - | _ -> compile_def' n total ctx def - -and compile_def' n total ctx = function - | DEF_reg_dec (DEC_aux (DEC_reg (_, _, typ, id), _)) -> - [CDEF_reg_dec (id, ctyp_of_typ ctx typ, [])], ctx - | DEF_reg_dec (DEC_aux (DEC_config (id, typ, exp), _)) -> - let aexp = analyze_functions ctx analyze_primop (c_literals ctx (no_shadow IdSet.empty (anf exp))) in - let setup, call, cleanup = compile_aexp ctx aexp in - let instrs = setup @ [call (CL_id (id, ctyp_of_typ ctx typ))] @ cleanup in - [CDEF_reg_dec (id, ctyp_of_typ ctx typ, instrs)], ctx - - | DEF_spec (VS_aux (VS_val_spec (_, id, _, _), _)) -> - c_debug (lazy "Compiling VS"); - let quant, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_env in - let arg_typs, ret_typ = match fn_typ with - | Typ_fn (arg_typs, ret_typ, _) -> arg_typs, ret_typ - | _ -> assert false - in - let ctx' = { ctx with local_env = add_typquant (id_loc id) quant ctx.local_env } in - let arg_ctyps, ret_ctyp = List.map (ctyp_of_typ ctx') arg_typs, ctyp_of_typ ctx' ret_typ in - [CDEF_spec (id, arg_ctyps, ret_ctyp)], ctx - - | DEF_fundef (FD_aux (FD_function (_, _, _, [FCL_aux (FCL_Funcl (id, Pat_aux (Pat_exp (pat, exp), _)), _)]), _)) -> - c_debug (lazy ("Compiling function " ^ string_of_id id)); - Util.progress "Compiling " (string_of_id id) n total; - - (* Find the function's type. *) - let quant, Typ_aux (fn_typ, _) = - try Env.get_val_spec id ctx.local_env - with Type_error _ -> - c_debug (lazy ("Falling back to global env for " ^ string_of_id id)); Env.get_val_spec id ctx.tc_env - in - let arg_typs, ret_typ = match fn_typ with - | Typ_fn (arg_typs, ret_typ, _) -> arg_typs, ret_typ - | _ -> assert false - in - - (* Handle the argument pattern. *) - let fundef_label = label "fundef_fail_" in - let orig_ctx = ctx in - (* The context must be updated before we call ctyp_of_typ on the argument types. *) - let ctx = { ctx with local_env = add_typquant (id_loc id) quant ctx.tc_env } in - - let arg_ctyps = List.map (ctyp_of_typ ctx) arg_typs in - let ret_ctyp = ctyp_of_typ ctx ret_typ in - - (* Optimize and compile the expression to ANF. *) - let aexp = no_shadow (pat_ids pat) (anf exp) in - c_debug (lazy (Pretty_print_sail.to_string (pp_aexp aexp))); - let aexp = analyze_functions ctx analyze_primop (c_literals ctx aexp) in + | CDEF_fundef (id, gs, _, _) :: _ -> + raise (Reporting.err_unreachable (id_loc id) __POS__ "Found function with return already re-written in insert_heap_returns") - if Id.compare (mk_id !opt_debug_function) id = 0 then - let header = - Printf.sprintf "Sail ANF for %s %s %s. (%s) -> %s" Util.("function" |> red |> clear) (string_of_id id) - (string_of_typquant quant) - Util.(string_of_list ", " (fun typ -> string_of_typ typ |> yellow |> clear) arg_typs) - Util.(string_of_typ ret_typ |> yellow |> clear) - - in - prerr_endline (Util.header header (List.length arg_typs + 2)); - prerr_endline (Pretty_print_sail.to_string (pp_aexp aexp)) - else (); - - (* Compile the function arguments as patterns. *) - let arg_setup, compiled_args, arg_cleanup = compile_arg_pats ctx fundef_label pat arg_ctyps in - let ctx = - (* We need the primop analyzer to be aware of the function argument types, so put them in ctx *) - List.fold_left2 (fun ctx (id, _) ctyp -> { ctx with locals = Bindings.add id (Immutable, ctyp) ctx.locals }) ctx compiled_args arg_ctyps - in - - (* Optimize and compile the expression from ANF to C. *) - let aexp = no_shadow (pat_ids pat) (anf exp) in - c_debug (lazy (Pretty_print_sail.to_string (pp_aexp aexp))); - let aexp = analyze_functions ctx analyze_primop (c_literals ctx aexp) in - c_debug (lazy (Pretty_print_sail.to_string (pp_aexp aexp))); - let setup, call, cleanup = compile_aexp ctx aexp in - c_debug (lazy "Compiled aexp"); - let gs = gensym () in - let destructure, destructure_cleanup = - compiled_args |> List.map snd |> combine_destructure_cleanup |> fix_destructure fundef_label - in - - if is_stack_ctyp ret_ctyp then - let instrs = arg_setup @ destructure @ [idecl ret_ctyp gs] @ setup @ [call (CL_id (gs, ret_ctyp))] @ cleanup @ destructure_cleanup @ arg_cleanup @ [ireturn (F_id gs, ret_ctyp)] in - let instrs = fix_early_stack_return ctx instrs in - let instrs = fix_exception ~return:(Some ret_ctyp) ctx instrs in - [CDEF_fundef (id, None, List.map fst compiled_args, instrs)], orig_ctx - else - let instrs = arg_setup @ destructure @ setup @ [call (CL_addr (CL_id (gs, CT_ref ret_ctyp)))] @ cleanup @ destructure_cleanup @ arg_cleanup in - let instrs = fix_early_return (CL_addr (CL_id (gs, CT_ref ret_ctyp))) ctx instrs in - let instrs = fix_exception ctx instrs in - [CDEF_fundef (id, Some gs, List.map fst compiled_args, instrs)], orig_ctx - - | DEF_fundef (FD_aux (FD_function (_, _, _, []), (l, _))) -> - c_error ~loc:l "Encountered function with no clauses" - | DEF_fundef (FD_aux (FD_function (_, _, _, funcls), (l, _))) -> - c_error ~loc:l "Encountered function with multiple clauses" - - (* All abbreviations should expanded by the typechecker, so we don't - need to translate type abbreviations into C typedefs. *) - | DEF_type (TD_aux (TD_abbrev _, _)) -> [], ctx - - | DEF_type type_def -> - let tdef, ctx = compile_type_def ctx type_def in - [CDEF_type tdef], ctx - - | DEF_val (LB_aux (LB_val (pat, exp), _)) -> - c_debug (lazy ("Compiling letbind " ^ string_of_pat pat)); - let ctyp = ctyp_of_typ ctx (typ_of_pat pat) in - let aexp = analyze_functions ctx analyze_primop (c_literals ctx (no_shadow IdSet.empty (anf exp))) in - let setup, call, cleanup = compile_aexp ctx aexp in - let apat = anf_pat ~global:true pat in - let gs = gensym () in - let end_label = label "let_end_" in - let destructure, destructure_cleanup, _ = compile_match ctx apat (F_id gs, ctyp) end_label in - let gs_setup, gs_cleanup = - [idecl ctyp gs], [iclear ctyp gs] - in - let bindings = List.map (fun (id, typ) -> id, ctyp_of_typ ctx typ) (apat_globals apat) in - let n = !letdef_count in - incr letdef_count; - let instrs = - gs_setup @ setup - @ [call (CL_id (gs, ctyp))] - @ cleanup - @ destructure - @ destructure_cleanup @ gs_cleanup - @ [ilabel end_label] - in - [CDEF_let (n, bindings, instrs)], - { ctx with letbinds = n :: ctx.letbinds } - - (* Only DEF_default that matters is default Order, but all order - polymorphism is specialised by this point. *) - | DEF_default _ -> [], ctx - - (* Overloading resolved by type checker *) - | DEF_overload _ -> [], ctx - - (* Only the parser and sail pretty printer care about this. *) - | DEF_fixity _ -> [], ctx - - (* We just ignore any pragmas we don't want to deal with. *) - | DEF_pragma _ -> [], ctx - - | DEF_internal_mutrec fundefs -> - let defs = List.map (fun fdef -> DEF_fundef fdef) fundefs in - List.fold_left (fun (cdefs, ctx) def -> let cdefs', ctx = compile_def n total ctx def in (cdefs @ cdefs', ctx)) ([], ctx) defs + | cdef :: cdefs -> + cdef :: insert_heap_returns ret_ctyps cdefs - | def -> - c_error ("Could not compile:\n" ^ Pretty_print_sail.to_string (Pretty_print_sail.doc_def def)) + | [] -> [] (** To keep things neat we use GCC's local labels extension to limit the scope of labels. We do this by iterating over all the blocks @@ -1941,16 +767,6 @@ let add_local_labels instrs = (* 5. Optimizations *) (**************************************************************************) -let rec clexp_rename from_id to_id = - let rename id = if Id.compare id from_id = 0 then to_id else id in - function - | CL_id (id, ctyp) -> CL_id (rename id, ctyp) - | CL_field (clexp, field) -> CL_field (clexp_rename from_id to_id clexp, field) - | CL_tuple (clexp, n) -> CL_tuple (clexp_rename from_id to_id clexp, n) - | CL_addr clexp -> CL_addr (clexp_rename from_id to_id clexp) - | CL_current_exception ctyp -> CL_current_exception ctyp - | CL_have_exception -> CL_have_exception - let rec instrs_rename from_id to_id = let rename id = if Id.compare id from_id = 0 then to_id else id in let crename = cval_rename from_id to_id in @@ -1974,7 +790,7 @@ let rec instrs_rename from_id to_id = | I_aux (I_block block, aux) :: instrs -> I_aux (I_block (irename block), aux) :: irename instrs | I_aux (I_try_block block, aux) :: instrs -> I_aux (I_try_block (irename block), aux) :: irename instrs | I_aux (I_throw cval, aux) :: instrs -> I_aux (I_throw (crename cval), aux) :: irename instrs - | (I_aux ((I_comment _ | I_raw _ | I_label _ | I_goto _ | I_match_failure | I_undefined _), _) as instr) :: instrs -> instr :: irename instrs + | (I_aux ((I_comment _ | I_raw _ | I_end | I_label _ | I_goto _ | I_match_failure | I_undefined _), _) as instr) :: instrs -> instr :: irename instrs | [] -> [] let hoist_ctyp = function @@ -1987,8 +803,8 @@ let hoist_id () = incr hoist_counter; id -let hoist_allocations ctx = function - | CDEF_fundef (function_id, _, _, _) as cdef when IdSet.mem function_id ctx.recursive_functions -> +let hoist_allocations recursive_functions = function + | CDEF_fundef (function_id, _, _, _) as cdef when IdSet.mem function_id recursive_functions -> c_debug (lazy (Printf.sprintf "skipping recursive function %s" (string_of_id function_id))); [cdef] @@ -2075,7 +891,6 @@ let flatten_cdef = | cdef -> cdef - let rec specialize_variants ctx prior = let unifications = ref (Bindings.empty) in @@ -2219,7 +1034,7 @@ let is_not_removed = function kill x; If found, we can remove the variable x, and directly modify y instead. *) -let remove_alias ctx = +let remove_alias = let pattern ctyp id = let alias = ref None in let rec scan ctyp id n instrs = @@ -2288,7 +1103,6 @@ let remove_alias ctx = [CDEF_fundef (function_id, heap_return, args, opt body)] | cdef -> [cdef] - (** This pass ensures that all variables created by I_decl have unique names *) let unique_names = let unique_counter = ref 0 in @@ -2348,7 +1162,7 @@ let unique_names = kill y; If found we can replace y by x *) -let combine_variables ctx = +let combine_variables = let pattern ctyp id = let combine = ref None in let rec scan id n instrs = @@ -2440,7 +1254,7 @@ let combine_variables ctx = to be 100% correct - so it's behind the -Oexperimental flag for now. Some benchmarking shows that this kind of optimization is very valuable however! *) -let hoist_alias ctx = +let hoist_alias = (* Must return true for a subset of the types hoist_ctyp would return true for. *) let is_struct = function | CT_struct _ -> true @@ -2488,15 +1302,15 @@ let hoist_alias ctx = let concatMap f xs = List.concat (List.map f xs) -let optimize ctx cdefs = +let optimize recursive_functions cdefs = let nothing cdefs = cdefs in cdefs |> (if !optimize_alias then concatMap unique_names else nothing) - |> (if !optimize_alias then concatMap (remove_alias ctx) else nothing) - |> (if !optimize_alias then concatMap (combine_variables ctx) else nothing) + |> (if !optimize_alias then concatMap remove_alias else nothing) + |> (if !optimize_alias then concatMap combine_variables else nothing) (* We need the runtime to initialize hoisted allocations *) - |> (if !optimize_hoist_allocations && not !opt_no_rts then concatMap (hoist_allocations ctx) else nothing) - |> (if !optimize_hoist_allocations && !optimize_experimental then concatMap (hoist_alias ctx) else nothing) + |> (if !optimize_hoist_allocations && not !opt_no_rts then concatMap (hoist_allocations recursive_functions) else nothing) + |> (if !optimize_hoist_allocations && !optimize_experimental then concatMap hoist_alias else nothing) (**************************************************************************) (* 6. Code generation *) @@ -2555,7 +1369,7 @@ let sgen_cval_param (frag, ctyp) = match ctyp with | CT_lbits direction -> string_of_fragment frag ^ ", " ^ string_of_bool direction - | CT_sbits direction -> + | CT_sbits (_, direction) -> string_of_fragment frag ^ ", " ^ string_of_bool direction | CT_fbits (len, direction) -> string_of_fragment frag ^ ", UINT64_C(" ^ string_of_int len ^ ") , " ^ string_of_bool direction @@ -2571,6 +1385,7 @@ let rec sgen_clexp = function | CL_addr clexp -> "(*(" ^ sgen_clexp clexp ^ "))" | CL_have_exception -> "have_exception" | CL_current_exception _ -> "current_exception" + | CL_return _ -> assert false let rec sgen_clexp_pure = function | CL_id (id, _) -> sgen_id id @@ -2579,6 +1394,7 @@ let rec sgen_clexp_pure = function | CL_addr clexp -> "(*(" ^ sgen_clexp_pure clexp ^ "))" | CL_have_exception -> "have_exception" | CL_current_exception _ -> "current_exception" + | CL_return _ -> assert false (** Generate instructions to copy from a cval to a clexp. This will insert any needed type conversions from big integers to small @@ -2800,6 +1616,8 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) = | I_raw str -> string (" " ^ str) + | I_end -> assert false + | I_match_failure -> string (" sail_match_failure(\"" ^ String.escaped (string_of_id fid) ^ "\");") @@ -3280,18 +2098,6 @@ let codegen_def' ctx = function ^ Util.string_of_list ", " string_of_ctyp arg_ctyps) else (); - (* If this function is set as opt_debug_function, then output its IR *) - if Id.compare (mk_id !opt_debug_function) id = 0 then - let header = - Printf.sprintf "Sail IR for %s %s(%s) : (%s) -> %s" Util.("function" |> red |> clear) (string_of_id id) - (Util.string_of_list ", " string_of_id args) - (Util.string_of_list ", " (fun ctyp -> Util.(string_of_ctyp ctyp |> yellow |> clear)) arg_ctyps) - Util.(string_of_ctyp ret_ctyp |> yellow |> clear) - in - prerr_endline (Util.header header (List.length arg_ctyps + 2)); - prerr_endline (Pretty_print_sail.to_string (separate_map hardline pp_instr instrs)) - else (); - let instrs = add_local_labels instrs in let args = Util.string_of_list ", " (fun x -> x) (List.map2 (fun ctyp arg -> sgen_ctyp ctyp ^ " " ^ sgen_id arg) arg_ctyps args) in let function_header = @@ -3383,7 +2189,7 @@ let codegen_ctg ctx = function (** When we generate code for a definition, we need to first generate any auxillary type definitions that are required. *) let codegen_def ctx def = - let ctyps = cdef_ctyps ctx def in + let ctyps = cdef_ctyps def |> CTSet.elements in (* We should have erased any polymorphism introduced by variants at this point! *) if List.exists is_polymorphic ctyps then let polymorphic_ctyps = List.filter is_polymorphic ctyps in @@ -3469,19 +2275,6 @@ let instrument_tracing ctx = CDEF_fundef (function_id, heap_return, args, instrument body) | cdef -> cdef -let bytecode_ast ctx rewrites (Defs defs) = - let assert_vs = Initial_check.extern_of_string (mk_id "sail_assert") "(bool, string) -> unit effect {escape}" in - let exit_vs = Initial_check.extern_of_string (mk_id "sail_exit") "unit -> unit effect {escape}" in - - let ctx = { ctx with tc_env = snd (Type_error.check ctx.tc_env (Defs [assert_vs; exit_vs])) } in - let total = List.length defs in - let _, chunks, ctx = - List.fold_left (fun (n, chunks, ctx) def -> let defs, ctx = compile_def n total ctx def in n + 1, defs :: chunks, ctx) (1, [], ctx) defs - in - let cdefs = List.concat (List.rev chunks) in - let cdefs, ctx = specialize_variants ctx [] cdefs in - rewrites cdefs - let rec get_recursive_functions (Defs defs) = match defs with | DEF_internal_mutrec fundefs :: defs -> @@ -3509,114 +2302,25 @@ let rec get_recursive_functions (Defs defs) = | _ :: defs -> get_recursive_functions (Defs defs) | [] -> IdSet.empty -let trace_cval = function (frag, ctyp) -> string_of_fragment frag ^ " : " ^ string_of_ctyp ctyp - -let rec trace_clexp = function - | CL_id (id, ctyp) -> sgen_id id ^ " : " ^ string_of_ctyp ctyp - | CL_field (clexp, field) -> "(" ^ trace_clexp clexp ^ ")->" ^ field ^ ")" - | CL_tuple (clexp, n) -> "(" ^ trace_clexp clexp ^ ")." ^ string_of_int n - | CL_addr clexp -> "*(" ^ trace_clexp clexp ^ ")" - | CL_have_exception -> "have_exception" - | CL_current_exception _ -> "current_exception" - -let rec smt_trace_instrs ctx function_id = function - | I_aux (I_jump (cval, label), aux) :: instrs -> - iraw ("printf(\"!branch %s %s\\n\"," ^ sgen_cval cval ^ " ?\"true\":\"false\", \"" ^ trace_cval cval ^ "\");") - :: I_aux (I_jump (cval, label), aux) - :: smt_trace_instrs ctx function_id instrs - - | (I_aux ((I_init (ctyp, id, cval) | I_reinit (ctyp, id, cval)), _) as instr) :: instrs -> - iraw ("printf(\"!create " ^ Util.zencode_string (string_of_id id) ^ " : " ^ string_of_ctyp ctyp ^ " = " ^ trace_cval cval ^ "\\n\");") - :: instr - :: smt_trace_instrs ctx function_id instrs - - | (I_aux ((I_decl (ctyp, id) | I_reset (ctyp, id)), _) as instr) :: instrs -> - iraw ("printf(\"!create " ^ Util.zencode_string (string_of_id id) ^ " : " ^ string_of_ctyp ctyp ^ "\\n\");") - :: instr - :: smt_trace_instrs ctx function_id instrs - - | I_aux (I_funcall (x, extern, f, args), aux) :: instrs -> - let extern_name = - if Env.is_extern f ctx.tc_env "c" then - Some (Env.get_extern f ctx.tc_env "c") - else if extern then - Some (string_of_id f) - else None - in - begin match extern_name with - | Some name -> - iraw ("printf(\"!" - ^ trace_clexp x - ^ " = " - ^ string_of_id f ^ "(" ^ Util.string_of_list ", " (fun cval -> String.escaped (trace_cval cval)) args ^ ")\\n\");") - :: I_aux (I_funcall (x, extern, f, args), aux) - :: smt_trace_instrs ctx function_id instrs - | None -> - iraw ("printf(\"!call " ^ string_of_id f ^ "(" ^ Util.string_of_list ", " (fun cval -> String.escaped (trace_cval cval)) args ^ ")\\n\");") - :: I_aux (I_funcall (x, extern, f, args), aux) - :: iraw ("printf(\"!" ^ trace_clexp x ^ " = endcall " ^ string_of_id f ^ "\\n\");") - :: smt_trace_instrs ctx function_id instrs - end - - | I_aux (I_return cval, aux) :: instrs -> - iraw ("printf(\"!return " ^ trace_cval cval ^ "\\n\");") - :: I_aux (I_return cval, aux) - :: smt_trace_instrs ctx function_id instrs - - | instr :: instrs -> instr :: smt_trace_instrs ctx function_id instrs - - | [] -> [] - -let smt_trace ctx = - function - | CDEF_fundef (function_id, heap_return, args, body) -> - let string_of_heap_return = function - | Some id -> Util.zencode_string (string_of_id id) - | None -> "return" - in - let body = - iraw ("printf(\"!link " ^ string_of_heap_return heap_return ^ "(" ^ Util.string_of_list ", " (fun id -> Util.zencode_string (string_of_id id)) args ^ ")\\n\");") - :: smt_trace_instrs ctx function_id body - in - CDEF_fundef (function_id, heap_return, args, body) - - | cdef -> cdef +let jib_of_ast env ast = + let ctx = + initial_ctx + ~convert_typ:ctyp_of_typ + ~optimize_anf:(fun ctx aexp -> analyze_functions ctx analyze_primop (c_literals ctx aexp)) + env + in + Jib_compile.compile_ast ctx ast -let compile_ast ctx output_chan c_includes (Defs defs) = +let compile_ast env output_chan c_includes ast = try c_debug (lazy (Util.log_line __MODULE__ __LINE__ "Identifying recursive functions")); - let recursive_functions = Spec_analysis.top_sort_defs (Defs defs) |> get_recursive_functions in - let ctx = { ctx with recursive_functions = recursive_functions } in - c_debug (lazy (Util.string_of_list ", " string_of_id (IdSet.elements recursive_functions))); - - let assert_vs = Initial_check.extern_of_string (mk_id "sail_assert") "(bool, string) -> unit effect {escape}" in - let exit_vs = Initial_check.extern_of_string (mk_id "sail_exit") "unit -> unit effect {escape}" in - let ctx = { ctx with tc_env = snd (Type_error.check ctx.tc_env (Defs [assert_vs; exit_vs])) } in - - if !opt_memo_cache then - (try - if Sys.is_directory "_sbuild" then - () - else - raise (Reporting.err_general Parse_ast.Unknown "_sbuild exists, but is a file not a directory!") - with - | Sys_error _ -> Unix.mkdir "_sbuild" 0o775) - else (); - - let total = List.length defs in - let _, chunks, ctx = - List.fold_left (fun (n, chunks, ctx) def -> let defs, ctx = compile_def n total ctx def in n + 1, defs :: chunks, ctx) (1, [], ctx) defs - in - let cdefs = List.concat (List.rev chunks) in - - let cdefs, ctx = specialize_variants ctx [] cdefs in - let cdefs = sort_ctype_defs cdefs in - let cdefs = optimize ctx cdefs in - let cdefs = if !opt_trace then List.map (instrument_tracing ctx) cdefs else cdefs in + let recursive_functions = Spec_analysis.top_sort_defs ast |> get_recursive_functions in - let cdefs = if !opt_smt_trace then List.map (fun cdef -> smt_trace ctx (flatten_cdef cdef)) cdefs else cdefs in + let cdefs, ctx = jib_of_ast env ast in + let cdefs = insert_heap_returns Bindings.empty cdefs in + let cdefs = optimize recursive_functions cdefs in - let docs = List.map (codegen_def ctx) cdefs in + let docs = separate_map (hardline ^^ hardline) (codegen_def ctx) cdefs in let preamble = separate hardline ([ string "#include \"sail.h\"" ] @@ -3702,7 +2406,7 @@ let compile_ast ctx output_chan c_includes (Defs defs) = let hlhl = hardline ^^ hardline in - Pretty_print_sail.to_string (preamble ^^ hlhl ^^ separate hlhl docs ^^ hlhl + Pretty_print_sail.to_string (preamble ^^ hlhl ^^ docs ^^ hlhl ^^ (if not !opt_no_rts then model_init ^^ hlhl ^^ model_fini ^^ hlhl @@ -3712,4 +2416,5 @@ let compile_ast ctx output_chan c_includes (Defs defs) = ^^ model_main ^^ hardline) |> output_string output_chan with - Type_error (_, l, err) -> c_error ("Unexpected type error when compiling to C:\n" ^ Type_error.string_of_type_error err) + | Type_error (_, l, err) -> + c_error ~loc:l ("Unexpected type error when compiling to C:\n" ^ Type_error.string_of_type_error err) diff --git a/src/c_backend.mli b/src/jib/c_backend.mli index 4017130a..2fc5be94 100644 --- a/src/c_backend.mli +++ b/src/jib/c_backend.mli @@ -48,7 +48,7 @@ (* SUCH DAMAGE. *) (**************************************************************************) -open Bytecode +open Jib open Type_check (** Global compilation options *) @@ -57,15 +57,6 @@ open Type_check (dot) format. *) val opt_debug_flow_graphs : bool ref -(** Print the ANF and IR representations of a specific function. *) -val opt_debug_function : string ref - -(** Instrument generated code to output a trace. opt_smt_trace is WIP - but intended to enable generating traces suitable for concolic - execution with SMT. *) -val opt_trace : bool ref -val opt_smt_trace : bool ref - (** Define generated functions as static *) val opt_static : bool ref @@ -102,7 +93,7 @@ val opt_extra_arguments : string option ref definitions in file _sbuild/ccacheDIGEST where DIGEST is the md5sum of the original function to be compiled. Enabled using the -memo flag. Uses Marshal so it's quite picky about the exact version of - the Sail version. This cache can obviously become stale if the C +b the Sail version. This cache can obviously become stale if the C backend changes - it'll load an old version compiled without said changes. *) val opt_memo_cache : bool ref @@ -115,27 +106,13 @@ val optimize_struct_updates : bool ref val optimize_alias : bool ref val optimize_experimental : bool ref -(** The compilation context. *) -type ctx - -(** Create a context from a typechecking environment. This environment - should be the environment returned by typechecking the full AST. *) -val initial_ctx : Env.t -> ctx - -(** Same as initial ctx, but iterate to find more precise bounds on - integers. *) -val initial_ctx_iterate : Env.t -> ctx - (** Convert a typ to a IR ctyp *) -val ctyp_of_typ : ctx -> Ast.typ -> ctyp - -val compile_aexp : ctx -> Ast.typ Anf.aexp -> instr list * (clexp -> instr) * instr list - -val compile_ast : ctx -> out_channel -> string list -> tannot Ast.defs -> unit - -val bytecode_ast : ctx -> (cdef list -> cdef list) -> tannot Ast.defs -> cdef list +val ctyp_of_typ : Jib_compile.ctx -> Ast.typ -> ctyp (** Rewriting steps for compiled ASTs *) val flatten_instrs : instr list -> instr list val flatten_cdef : cdef -> cdef + +val jib_of_ast : Env.t -> tannot Ast.defs -> cdef list * Jib_compile.ctx +val compile_ast : Env.t -> out_channel -> string list -> tannot Ast.defs -> unit diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml new file mode 100644 index 00000000..8411f464 --- /dev/null +++ b/src/jib/jib_compile.ml @@ -0,0 +1,1367 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* Alasdair Armstrong *) +(* Brian Campbell *) +(* Thomas Bauereiss *) +(* Anthony Fox *) +(* Jon French *) +(* Dominic Mulligan *) +(* Stephen Kell *) +(* Mark Wassell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + +open Ast +open Ast_util +open Jib +open Jib_util +open Type_check +open Value2 + +open Anf + +let opt_memo_cache = ref false + +(**************************************************************************) +(* 4. Conversion to low-level AST *) +(**************************************************************************) + +(** We now use a low-level AST called Jib (see language/bytecode.ott) + that is only slightly abstracted away from C. To be succint in + comments we usually refer to this as Sail IR or IR rather than + low-level AST repeatedly. + + The general idea is ANF expressions are converted into lists of + instructions (type instr) where allocations and deallocations are + now made explicit. ANF values (aval) are mapped to the cval type, + which is even simpler still. Some things are still more abstract + than in C, so the type definitions follow the sail type definition + structure, just with typ (from ast.ml) replaced with + ctyp. Top-level declarations that have no meaning for the backend + are not included at this level. + + The convention used here is that functions of the form compile_X + compile the type X into types in this AST, so compile_aval maps + avals into cvals. Note that the return types for these functions + are often quite complex, and they usually return some tuple + containing setup instructions (to allocate memory for the + expression), cleanup instructions (to deallocate that memory) and + possibly typing information about what has been translated. **) + +(* FIXME: This stage shouldn't care about this *) +let max_int n = Big_int.pred (Big_int.pow_int_positive 2 (n - 1)) +let min_int n = Big_int.negate (Big_int.pow_int_positive 2 (n - 1)) + +let rec is_bitvector = function + | [] -> true + | AV_lit (L_aux (L_zero, _), _) :: avals -> is_bitvector avals + | AV_lit (L_aux (L_one, _), _) :: avals -> is_bitvector avals + | _ :: _ -> false + +let rec value_of_aval_bit = function + | AV_lit (L_aux (L_zero, _), _) -> Sail2_values.B0 + | AV_lit (L_aux (L_one, _), _) -> Sail2_values.B1 + | _ -> assert false + +let is_ct_enum = function + | CT_enum _ -> true + | _ -> false + +let is_ct_variant = function + | CT_variant _ -> true + | _ -> false + +let is_ct_tup = function + | CT_tup _ -> true + | _ -> false + +let is_ct_list = function + | CT_list _ -> true + | _ -> false + +let is_ct_vector = function + | CT_vector _ -> true + | _ -> false + +let is_ct_struct = function + | CT_struct _ -> true + | _ -> false + +let is_ct_ref = function + | CT_ref _ -> true + | _ -> false + +let ctor_bindings = List.fold_left (fun map (id, ctyp) -> Bindings.add id ctyp map) Bindings.empty + +(** The context type contains two type-checking + environments. ctx.local_env contains the closest typechecking + environment, usually from the expression we are compiling, whereas + ctx.tc_env is the global type checking environment from + type-checking the entire AST. We also keep track of local variables + in ctx.locals, so we know when their type changes due to flow + typing. *) +type ctx = + { records : (ctyp Bindings.t) Bindings.t; + enums : IdSet.t Bindings.t; + variants : (ctyp Bindings.t) Bindings.t; + tc_env : Env.t; + local_env : Env.t; + locals : (mut * ctyp) Bindings.t; + letbinds : int list; + no_raw : bool; + convert_typ : ctx -> typ -> ctyp; + optimize_anf : ctx -> typ aexp -> typ aexp + } + +let initial_ctx ~convert_typ:convert_typ ~optimize_anf:optimize_anf env = + { records = Bindings.empty; + enums = Bindings.empty; + variants = Bindings.empty; + tc_env = env; + local_env = env; + locals = Bindings.empty; + letbinds = []; + no_raw = false; + convert_typ = convert_typ; + optimize_anf = optimize_anf + } + +let ctyp_of_typ ctx typ = ctx.convert_typ ctx typ + +let rec chunkify n xs = + match Util.take n xs, Util.drop n xs with + | xs, [] -> [xs] + | xs, ys -> xs :: chunkify n ys + +let rec compile_aval l ctx = function + | AV_C_fragment (frag, typ, ctyp) -> + let ctyp' = ctyp_of_typ ctx typ in + if not (ctyp_equal ctyp ctyp') then + raise (Reporting.err_unreachable l __POS__ (string_of_ctyp ctyp ^ " != " ^ string_of_ctyp ctyp')); + [], (frag, ctyp_of_typ ctx typ), [] + + | AV_id (id, typ) -> + begin + try + let _, ctyp = Bindings.find id ctx.locals in + [], (F_id id, ctyp), [] + with + | Not_found -> + [], (F_id id, ctyp_of_typ ctx (lvar_typ typ)), [] + end + + | AV_ref (id, typ) -> + [], (F_ref id, CT_ref (ctyp_of_typ ctx (lvar_typ typ))), [] + + | AV_lit (L_aux (L_string str, _), typ) -> + [], (F_lit (V_string (String.escaped str)), ctyp_of_typ ctx typ), [] + + | AV_lit (L_aux (L_num n, _), typ) when Big_int.less_equal (min_int 64) n && Big_int.less_equal n (max_int 64) -> + let gs = gensym () in + [iinit CT_lint gs (F_lit (V_int n), CT_fint 64)], + (F_id gs, CT_lint), + [iclear CT_lint gs] + + | AV_lit (L_aux (L_num n, _), typ) -> + let gs = gensym () in + [iinit CT_lint gs (F_lit (V_string (Big_int.to_string n)), CT_string)], + (F_id gs, CT_lint), + [iclear CT_lint gs] + + | AV_lit (L_aux (L_zero, _), _) -> [], (F_lit (V_bit Sail2_values.B0), CT_bit), [] + | AV_lit (L_aux (L_one, _), _) -> [], (F_lit (V_bit Sail2_values.B1), CT_bit), [] + + | AV_lit (L_aux (L_true, _), _) -> [], (F_lit (V_bool true), CT_bool), [] + | AV_lit (L_aux (L_false, _), _) -> [], (F_lit (V_bool false), CT_bool), [] + + | AV_lit (L_aux (L_real str, _), _) -> + let gs = gensym () in + [iinit CT_real gs (F_lit (V_string str), CT_string)], + (F_id gs, CT_real), + [iclear CT_real gs] + + | AV_lit (L_aux (L_unit, _), _) -> [], (F_lit V_unit, CT_unit), [] + + | AV_lit (L_aux (_, l) as lit, _) -> + raise (Reporting.err_general l ("Encountered unexpected literal " ^ string_of_lit lit ^ " when converting ANF represention into IR")) + + | AV_tuple avals -> + let elements = List.map (compile_aval l ctx) avals in + let cvals = List.map (fun (_, cval, _) -> cval) elements in + let setup = List.concat (List.map (fun (setup, _, _) -> setup) elements) in + let cleanup = List.concat (List.rev (List.map (fun (_, _, cleanup) -> cleanup) elements)) in + let tup_ctyp = CT_tup (List.map cval_ctyp cvals) in + let gs = gensym () in + setup + @ [idecl tup_ctyp gs] + @ List.mapi (fun n cval -> icopy l (CL_tuple (CL_id (gs, tup_ctyp), n)) cval) cvals, + (F_id gs, CT_tup (List.map cval_ctyp cvals)), + [iclear tup_ctyp gs] + @ cleanup + + | AV_record (fields, typ) -> + let ctyp = ctyp_of_typ ctx typ in + let gs = gensym () in + let compile_fields (id, aval) = + let field_setup, cval, field_cleanup = compile_aval l ctx aval in + field_setup + @ [icopy l (CL_field (CL_id (gs, ctyp), string_of_id id)) cval] + @ field_cleanup + in + [idecl ctyp gs] + @ List.concat (List.map compile_fields (Bindings.bindings fields)), + (F_id gs, ctyp), + [iclear ctyp gs] + + | AV_vector ([], _) -> + raise (Reporting.err_general l "Encountered empty vector literal") + + (* Convert a small bitvector to a uint64_t literal. *) + | AV_vector (avals, typ) when is_bitvector avals && List.length avals <= 64 -> + begin + let bitstring = F_lit (V_bits (List.map value_of_aval_bit avals)) in + let len = List.length avals in + match destruct_vector ctx.tc_env typ with + | Some (_, Ord_aux (Ord_inc, _), _) -> + [], (bitstring, CT_fbits (len, false)), [] + | Some (_, Ord_aux (Ord_dec, _), _) -> + [], (bitstring, CT_fbits (len, true)), [] + | Some _ -> + raise (Reporting.err_general l "Encountered order polymorphic bitvector literal") + | None -> + raise (Reporting.err_general l "Encountered vector literal without vector type") + end + + (* Convert a bitvector literal that is larger than 64-bits to a + variable size bitvector, converting it in 64-bit chunks. *) + | AV_vector (avals, typ) when is_bitvector avals -> + let len = List.length avals in + let bitstring avals = F_lit (V_bits (List.map value_of_aval_bit avals)) in + let first_chunk = bitstring (Util.take (len mod 64) avals) in + let chunks = Util.drop (len mod 64) avals |> chunkify 64 |> List.map bitstring in + let gs = gensym () in + [iinit (CT_lbits true) gs (first_chunk, CT_fbits (len mod 64, true))] + @ List.map (fun chunk -> ifuncall (CL_id (gs, CT_lbits true)) + (mk_id "append_64") + [(F_id gs, CT_lbits true); (chunk, CT_fbits (64, true))]) chunks, + (F_id gs, CT_lbits true), + [iclear (CT_lbits true) gs] + + (* If we have a bitvector value, that isn't a literal then we need to set bits individually. *) + | AV_vector (avals, Typ_aux (Typ_app (id, [_; A_aux (A_order ord, _); A_aux (A_typ (Typ_aux (Typ_id bit_id, _)), _)]), _)) + when string_of_id bit_id = "bit" && string_of_id id = "vector" && List.length avals <= 64 -> + let len = List.length avals in + let direction = match ord with + | Ord_aux (Ord_inc, _) -> false + | Ord_aux (Ord_dec, _) -> true + | Ord_aux (Ord_var _, _) -> raise (Reporting.err_general l "Polymorphic vector direction found") + in + let gs = gensym () in + let ctyp = CT_fbits (len, direction) in + let mask i = V_bits (Util.list_init (63 - i) (fun _ -> Sail2_values.B0) @ [Sail2_values.B1] @ Util.list_init i (fun _ -> Sail2_values.B0)) in + let aval_mask i aval = + let setup, cval, cleanup = compile_aval l ctx aval in + match cval with + | (F_lit (V_bit Sail2_values.B0), _) -> [] + | (F_lit (V_bit Sail2_values.B1), _) -> + [icopy l (CL_id (gs, ctyp)) (F_op (F_id gs, "|", F_lit (mask i)), ctyp)] + | _ -> + setup @ [iif cval [icopy l (CL_id (gs, ctyp)) (F_op (F_id gs, "|", F_lit (mask i)), ctyp)] [] CT_unit] @ cleanup + in + [idecl ctyp gs; + icopy l (CL_id (gs, ctyp)) (F_lit (V_bits (Util.list_init 64 (fun _ -> Sail2_values.B0))), ctyp)] + @ List.concat (List.mapi aval_mask (List.rev avals)), + (F_id gs, ctyp), + [] + + (* Compiling a vector literal that isn't a bitvector *) + | AV_vector (avals, Typ_aux (Typ_app (id, [_; A_aux (A_order ord, _); A_aux (A_typ typ, _)]), _)) + when string_of_id id = "vector" -> + let len = List.length avals in + let direction = match ord with + | Ord_aux (Ord_inc, _) -> false + | Ord_aux (Ord_dec, _) -> true + | Ord_aux (Ord_var _, _) -> raise (Reporting.err_general l "Polymorphic vector direction found") + in + let vector_ctyp = CT_vector (direction, ctyp_of_typ ctx typ) in + let gs = gensym () in + let aval_set i aval = + let setup, cval, cleanup = compile_aval l ctx aval in + setup + @ [iextern (CL_id (gs, vector_ctyp)) + (mk_id "internal_vector_update") + [(F_id gs, vector_ctyp); (F_lit (V_int (Big_int.of_int i)), CT_fint 64); cval]] + @ cleanup + in + [idecl vector_ctyp gs; + iextern (CL_id (gs, vector_ctyp)) (mk_id "internal_vector_init") [(F_lit (V_int (Big_int.of_int len)), CT_fint 64)]] + @ List.concat (List.mapi aval_set (if direction then List.rev avals else avals)), + (F_id gs, vector_ctyp), + [iclear vector_ctyp gs] + + | AV_vector _ as aval -> + raise (Reporting.err_general l ("Have AV_vector: " ^ Pretty_print_sail.to_string (pp_aval aval) ^ " which is not a vector type")) + + | AV_list (avals, Typ_aux (typ, _)) -> + let ctyp = match typ with + | Typ_app (id, [A_aux (A_typ typ, _)]) when string_of_id id = "list" -> ctyp_of_typ ctx typ + | _ -> raise (Reporting.err_general l "Invalid list type") + in + let gs = gensym () in + let mk_cons aval = + let setup, cval, cleanup = compile_aval l ctx aval in + setup @ [ifuncall (CL_id (gs, CT_list ctyp)) (mk_id ("cons#" ^ string_of_ctyp ctyp)) [cval; (F_id gs, CT_list ctyp)]] @ cleanup + in + [idecl (CT_list ctyp) gs] + @ List.concat (List.map mk_cons (List.rev avals)), + (F_id gs, CT_list ctyp), + [iclear (CT_list ctyp) gs] + +let compile_funcall l ctx id args typ = + let setup = ref [] in + let cleanup = ref [] in + + let quant, Typ_aux (fn_typ, _) = + (* If we can't find a function in local_env, fall back to the + global env - this happens when representing assertions, exit, + etc as functions in the IR. *) + try Env.get_val_spec id ctx.local_env with Type_error _ -> Env.get_val_spec id ctx.tc_env + in + let arg_typs, ret_typ = match fn_typ with + | Typ_fn (arg_typs, ret_typ, _) -> arg_typs, ret_typ + | _ -> assert false + in + let ctx' = { ctx with local_env = add_typquant (id_loc id) quant ctx.tc_env } in + let arg_ctyps, ret_ctyp = List.map (ctyp_of_typ ctx') arg_typs, ctyp_of_typ ctx' ret_typ in + let final_ctyp = ctyp_of_typ ctx typ in + + let setup_arg ctyp aval = + let arg_setup, cval, arg_cleanup = compile_aval l ctx aval in + setup := List.rev arg_setup @ !setup; + cleanup := arg_cleanup @ !cleanup; + let have_ctyp = cval_ctyp cval in + if is_polymorphic ctyp then + (F_poly (fst cval), have_ctyp) + else if ctyp_equal ctyp have_ctyp then + cval + else + let gs = gensym () in + setup := iinit ctyp gs cval :: !setup; + cleanup := iclear ctyp gs :: !cleanup; + (F_id gs, ctyp) + in + + assert (List.length arg_ctyps = List.length args); + + let setup_args = List.map2 setup_arg arg_ctyps args in + + List.rev !setup, + begin fun clexp -> + if ctyp_equal (clexp_ctyp clexp) ret_ctyp then + ifuncall clexp id setup_args + else + let gs = gensym () in + iblock [idecl ret_ctyp gs; + ifuncall (CL_id (gs, ret_ctyp)) id setup_args; + icopy l clexp (F_id gs, ret_ctyp); + iclear ret_ctyp gs] + end, + !cleanup + +let rec apat_ctyp ctx (AP_aux (apat, _, _)) = + match apat with + | AP_tup apats -> CT_tup (List.map (apat_ctyp ctx) apats) + | AP_global (_, typ) -> ctyp_of_typ ctx typ + | AP_cons (apat, _) -> CT_list (apat_ctyp ctx apat) + | AP_wild typ | AP_nil typ | AP_id (_, typ) -> ctyp_of_typ ctx typ + | AP_app (_, _, typ) -> ctyp_of_typ ctx typ + +let rec compile_match ctx (AP_aux (apat_aux, env, l)) cval case_label = + let ctx = { ctx with local_env = env } in + match apat_aux, cval with + | AP_id (pid, _), (frag, ctyp) when Env.is_union_constructor pid ctx.tc_env -> + [ijump (F_op (F_field (frag, "kind"), "!=", F_lit (V_ctor_kind (string_of_id pid))), CT_bool) case_label], + [], + ctx + + | AP_global (pid, typ), (frag, ctyp) -> + let global_ctyp = ctyp_of_typ ctx typ in + [icopy l (CL_id (pid, global_ctyp)) cval], [], ctx + + | AP_id (pid, _), (frag, ctyp) when is_ct_enum ctyp -> + begin match Env.lookup_id pid ctx.tc_env with + | Unbound -> [idecl ctyp pid; icopy l (CL_id (pid, ctyp)) (frag, ctyp)], [], ctx + | _ -> [ijump (F_op (F_id pid, "!=", frag), CT_bool) case_label], [], ctx + end + + | AP_id (pid, typ), _ -> + let ctyp = cval_ctyp cval in + let id_ctyp = ctyp_of_typ ctx typ in + let ctx = { ctx with locals = Bindings.add pid (Immutable, id_ctyp) ctx.locals } in + [idecl id_ctyp pid; icopy l (CL_id (pid, id_ctyp)) cval], [iclear id_ctyp pid], ctx + + | AP_tup apats, (frag, ctyp) -> + begin + let get_tup n ctyp = (F_field (frag, "ztup" ^ string_of_int n), ctyp) in + let fold (instrs, cleanup, n, ctx) apat ctyp = + let instrs', cleanup', ctx = compile_match ctx apat (get_tup n ctyp) case_label in + instrs @ instrs', cleanup' @ cleanup, n + 1, ctx + in + match ctyp with + | CT_tup ctyps -> + let instrs, cleanup, _, ctx = List.fold_left2 fold ([], [], 0, ctx) apats ctyps in + instrs, cleanup, ctx + | _ -> failwith ("AP_tup with ctyp " ^ string_of_ctyp ctyp) + end + + | AP_app (ctor, apat, variant_typ), (frag, ctyp) -> + begin match ctyp with + | CT_variant (_, ctors) -> + let ctor_c_id = string_of_id ctor in + let ctor_ctyp = Bindings.find ctor (ctor_bindings ctors) in + (* These should really be the same, something has gone wrong if they are not. *) + if ctyp_equal ctor_ctyp (ctyp_of_typ ctx variant_typ) then + raise (Reporting.err_general l (Printf.sprintf "%s is not the same type as %s" (string_of_ctyp ctor_ctyp) (string_of_ctyp (ctyp_of_typ ctx variant_typ)))) + else (); + let ctor_c_id, ctor_ctyp = + if is_polymorphic ctor_ctyp then + let unification = List.map ctyp_suprema (ctyp_unify ctor_ctyp (apat_ctyp ctx apat)) in + (if List.length unification > 0 then + ctor_c_id ^ "_" ^ Util.string_of_list "_" (fun ctyp -> Util.zencode_string (string_of_ctyp ctyp)) unification + else + ctor_c_id), + ctyp_suprema (apat_ctyp ctx apat) + else + ctor_c_id, ctor_ctyp + in + let instrs, cleanup, ctx = compile_match ctx apat ((F_field (frag, Util.zencode_string ctor_c_id), ctor_ctyp)) case_label in + [ijump (F_op (F_field (frag, "kind"), "!=", F_lit (V_ctor_kind ctor_c_id)), CT_bool) case_label] + @ instrs, + cleanup, + ctx + | ctyp -> + raise (Reporting.err_general l (Printf.sprintf "Variant constructor %s : %s matching against non-variant type %s : %s" + (string_of_id ctor) + (string_of_typ variant_typ) + (string_of_fragment ~zencode:false frag) + (string_of_ctyp ctyp))) + end + + | AP_wild _, _ -> [], [], ctx + + | AP_cons (hd_apat, tl_apat), (frag, CT_list ctyp) -> + let hd_setup, hd_cleanup, ctx = compile_match ctx hd_apat (F_field (F_unary ("*", frag), "hd"), ctyp) case_label in + let tl_setup, tl_cleanup, ctx = compile_match ctx tl_apat (F_field (F_unary ("*", frag), "tl"), CT_list ctyp) case_label in + [ijump (F_op (frag, "==", F_lit V_null), CT_bool) case_label] @ hd_setup @ tl_setup, tl_cleanup @ hd_cleanup, ctx + + | AP_cons _, (_, _) -> + raise (Reporting.err_general l "Tried to pattern match cons on non list type") + + | AP_nil _, (frag, _) -> [ijump (F_op (frag, "!=", F_lit V_null), CT_bool) case_label], [], ctx + +let unit_fragment = (F_lit V_unit, CT_unit) + +let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = + let ctx = { ctx with local_env = env } in + match aexp_aux with + | AE_let (mut, id, binding_typ, binding, (AE_aux (_, body_env, _) as body), body_typ) -> + let binding_ctyp = ctyp_of_typ { ctx with local_env = body_env } binding_typ in + let setup, call, cleanup = compile_aexp ctx binding in + let letb_setup, letb_cleanup = + [idecl binding_ctyp id; iblock (setup @ [call (CL_id (id, binding_ctyp))] @ cleanup)], [iclear binding_ctyp id] + in + let ctx = { ctx with locals = Bindings.add id (mut, binding_ctyp) ctx.locals } in + let setup, call, cleanup = compile_aexp ctx body in + letb_setup @ setup, call, cleanup @ letb_cleanup + + | AE_app (id, vs, typ) -> + compile_funcall l ctx id vs typ + + | AE_val aval -> + let setup, cval, cleanup = compile_aval l ctx aval in + setup, (fun clexp -> icopy l clexp cval), cleanup + + (* Compile case statements *) + | AE_case (aval, cases, typ) -> + let ctyp = ctyp_of_typ ctx typ in + let aval_setup, cval, aval_cleanup = compile_aval l ctx aval in + let case_return_id = gensym () in + let finish_match_label = label "finish_match_" in + let compile_case (apat, guard, body) = + let trivial_guard = match guard with + | AE_aux (AE_val (AV_lit (L_aux (L_true, _), _)), _, _) + | AE_aux (AE_val (AV_C_fragment (F_lit (V_bool true), _, _)), _, _) -> true + | _ -> false + in + let case_label = label "case_" in + let destructure, destructure_cleanup, ctx = compile_match ctx apat cval case_label in + let guard_setup, guard_call, guard_cleanup = compile_aexp ctx guard in + let body_setup, body_call, body_cleanup = compile_aexp ctx body in + let gs = gensym () in + let case_instrs = + destructure @ [icomment "end destructuring"] + @ (if not trivial_guard then + guard_setup @ [idecl CT_bool gs; guard_call (CL_id (gs, CT_bool))] @ guard_cleanup + @ [iif (F_unary ("!", F_id gs), CT_bool) (destructure_cleanup @ [igoto case_label]) [] CT_unit] + @ [icomment "end guard"] + else []) + @ body_setup @ [body_call (CL_id (case_return_id, ctyp))] @ body_cleanup @ destructure_cleanup + @ [igoto finish_match_label] + in + if is_dead_aexp body then + [ilabel case_label] + else + [iblock case_instrs; ilabel case_label] + in + [icomment "begin match"] + @ aval_setup @ [idecl ctyp case_return_id] + @ List.concat (List.map compile_case cases) + @ [imatch_failure ()] + @ [ilabel finish_match_label], + (fun clexp -> icopy l clexp (F_id case_return_id, ctyp)), + [iclear ctyp case_return_id] + @ aval_cleanup + @ [icomment "end match"] + + (* Compile try statement *) + | AE_try (aexp, cases, typ) -> + let ctyp = ctyp_of_typ ctx typ in + let aexp_setup, aexp_call, aexp_cleanup = compile_aexp ctx aexp in + let try_return_id = gensym () in + let handled_exception_label = label "handled_exception_" in + let fallthrough_label = label "fallthrough_exception_" in + let compile_case (apat, guard, body) = + let trivial_guard = match guard with + | AE_aux (AE_val (AV_lit (L_aux (L_true, _), _)), _, _) + | AE_aux (AE_val (AV_C_fragment (F_lit (V_bool true), _, _)), _, _) -> true + | _ -> false + in + let try_label = label "try_" in + let exn_cval = (F_current_exception, ctyp_of_typ ctx (mk_typ (Typ_id (mk_id "exception")))) in + let destructure, destructure_cleanup, ctx = compile_match ctx apat exn_cval try_label in + let guard_setup, guard_call, guard_cleanup = compile_aexp ctx guard in + let body_setup, body_call, body_cleanup = compile_aexp ctx body in + let gs = gensym () in + let case_instrs = + destructure @ [icomment "end destructuring"] + @ (if not trivial_guard then + guard_setup @ [idecl CT_bool gs; guard_call (CL_id (gs, CT_bool))] @ guard_cleanup + @ [ijump (F_unary ("!", F_id gs), CT_bool) try_label] + @ [icomment "end guard"] + else []) + @ body_setup @ [body_call (CL_id (try_return_id, ctyp))] @ body_cleanup @ destructure_cleanup + @ [igoto handled_exception_label] + in + [iblock case_instrs; ilabel try_label] + in + assert (ctyp_equal ctyp (ctyp_of_typ ctx typ)); + [idecl ctyp try_return_id; + itry_block (aexp_setup @ [aexp_call (CL_id (try_return_id, ctyp))] @ aexp_cleanup); + ijump (F_unary ("!", F_have_exception), CT_bool) handled_exception_label] + @ List.concat (List.map compile_case cases) + @ [igoto fallthrough_label; + ilabel handled_exception_label; + icopy l CL_have_exception (F_lit (V_bool false), CT_bool); + ilabel fallthrough_label], + (fun clexp -> icopy l clexp (F_id try_return_id, ctyp)), + [] + + | AE_if (aval, then_aexp, else_aexp, if_typ) -> + if is_dead_aexp then_aexp then + compile_aexp ctx else_aexp + else if is_dead_aexp else_aexp then + compile_aexp ctx then_aexp + else + let if_ctyp = ctyp_of_typ ctx if_typ in + let compile_branch aexp = + let setup, call, cleanup = compile_aexp ctx aexp in + fun clexp -> setup @ [call clexp] @ cleanup + in + let setup, cval, cleanup = compile_aval l ctx aval in + setup, + (fun clexp -> iif cval + (compile_branch then_aexp clexp) + (compile_branch else_aexp clexp) + if_ctyp), + cleanup + + (* FIXME: AE_record_update could be AV_record_update - would reduce some copying. *) + | AE_record_update (aval, fields, typ) -> + let ctyp = ctyp_of_typ ctx typ in + let ctors = match ctyp with + | CT_struct (_, ctors) -> List.fold_left (fun m (k, v) -> Bindings.add k v m) Bindings.empty ctors + | _ -> raise (Reporting.err_general l "Cannot perform record update for non-record type") + in + let gs = gensym () in + let compile_fields (id, aval) = + let field_setup, cval, field_cleanup = compile_aval l ctx aval in + field_setup + @ [icopy l (CL_field (CL_id (gs, ctyp), string_of_id id)) cval] + @ field_cleanup + in + let setup, cval, cleanup = compile_aval l ctx aval in + [idecl ctyp gs] + @ setup + @ [icopy l (CL_id (gs, ctyp)) cval] + @ cleanup + @ List.concat (List.map compile_fields (Bindings.bindings fields)), + (fun clexp -> icopy l clexp (F_id gs, ctyp)), + [iclear ctyp gs] + + | AE_short_circuit (SC_and, aval, aexp) -> + let left_setup, cval, left_cleanup = compile_aval l ctx aval in + let right_setup, call, right_cleanup = compile_aexp ctx aexp in + let gs = gensym () in + left_setup + @ [ idecl CT_bool gs; + iif cval + (right_setup @ [call (CL_id (gs, CT_bool))] @ right_cleanup) + [icopy l (CL_id (gs, CT_bool)) (F_lit (V_bool false), CT_bool)] + CT_bool ] + @ left_cleanup, + (fun clexp -> icopy l clexp (F_id gs, CT_bool)), + [] + | AE_short_circuit (SC_or, aval, aexp) -> + let left_setup, cval, left_cleanup = compile_aval l ctx aval in + let right_setup, call, right_cleanup = compile_aexp ctx aexp in + let gs = gensym () in + left_setup + @ [ idecl CT_bool gs; + iif cval + [icopy l (CL_id (gs, CT_bool)) (F_lit (V_bool true), CT_bool)] + (right_setup @ [call (CL_id (gs, CT_bool))] @ right_cleanup) + CT_bool ] + @ left_cleanup, + (fun clexp -> icopy l clexp (F_id gs, CT_bool)), + [] + + (* This is a faster assignment rule for updating fields of a + struct. *) + | AE_assign (id, assign_typ, AE_aux (AE_record_update (AV_id (rid, _), fields, typ), _, _)) + when Id.compare id rid = 0 -> + let compile_fields (field_id, aval) = + let field_setup, cval, field_cleanup = compile_aval l ctx aval in + field_setup + @ [icopy l (CL_field (CL_id (id, ctyp_of_typ ctx typ), string_of_id field_id)) cval] + @ field_cleanup + in + List.concat (List.map compile_fields (Bindings.bindings fields)), + (fun clexp -> icopy l clexp unit_fragment), + [] + + | AE_assign (id, assign_typ, aexp) -> + let assign_ctyp = + match Bindings.find_opt id ctx.locals with + | Some (_, ctyp) -> ctyp + | None -> ctyp_of_typ ctx assign_typ + in + let setup, call, cleanup = compile_aexp ctx aexp in + setup @ [call (CL_id (id, assign_ctyp))], (fun clexp -> icopy l clexp unit_fragment), cleanup + + | AE_block (aexps, aexp, _) -> + let block = compile_block ctx aexps in + let setup, call, cleanup = compile_aexp ctx aexp in + block @ setup, call, cleanup + + | AE_loop (While, cond, body) -> + let loop_start_label = label "while_" in + let loop_end_label = label "wend_" in + let cond_setup, cond_call, cond_cleanup = compile_aexp ctx cond in + let body_setup, body_call, body_cleanup = compile_aexp ctx body in + let gs = gensym () in + let unit_gs = gensym () in + let loop_test = (F_unary ("!", F_id gs), CT_bool) in + [idecl CT_bool gs; idecl CT_unit unit_gs] + @ [ilabel loop_start_label] + @ [iblock (cond_setup + @ [cond_call (CL_id (gs, CT_bool))] + @ cond_cleanup + @ [ijump loop_test loop_end_label] + @ body_setup + @ [body_call (CL_id (unit_gs, CT_unit))] + @ body_cleanup + @ [igoto loop_start_label])] + @ [ilabel loop_end_label], + (fun clexp -> icopy l clexp unit_fragment), + [] + + | AE_loop (Until, cond, body) -> + let loop_start_label = label "repeat_" in + let loop_end_label = label "until_" in + let cond_setup, cond_call, cond_cleanup = compile_aexp ctx cond in + let body_setup, body_call, body_cleanup = compile_aexp ctx body in + let gs = gensym () in + let unit_gs = gensym () in + let loop_test = (F_id gs, CT_bool) in + [idecl CT_bool gs; idecl CT_unit unit_gs] + @ [ilabel loop_start_label] + @ [iblock (body_setup + @ [body_call (CL_id (unit_gs, CT_unit))] + @ body_cleanup + @ cond_setup + @ [cond_call (CL_id (gs, CT_bool))] + @ cond_cleanup + @ [ijump loop_test loop_end_label] + @ [igoto loop_start_label])] + @ [ilabel loop_end_label], + (fun clexp -> icopy l clexp unit_fragment), + [] + + | AE_cast (aexp, typ) -> compile_aexp ctx aexp + + | AE_return (aval, typ) -> + let fn_return_ctyp = match Env.get_ret_typ env with + | Some typ -> ctyp_of_typ ctx typ + | None -> raise (Reporting.err_general l "No function return type found when compiling return statement") + in + (* Cleanup info will be re-added by fix_early_(heap/stack)_return *) + let return_setup, cval, _ = compile_aval l ctx aval in + let creturn = + if ctyp_equal fn_return_ctyp (cval_ctyp cval) then + [ireturn cval] + else + let gs = gensym () in + [idecl fn_return_ctyp gs; + icopy l (CL_id (gs, fn_return_ctyp)) cval; + ireturn (F_id gs, fn_return_ctyp)] + in + return_setup @ creturn, + (fun clexp -> icomment "unreachable after return"), + [] + + | AE_throw (aval, typ) -> + (* Cleanup info will be handled by fix_exceptions *) + let throw_setup, cval, _ = compile_aval l ctx aval in + throw_setup @ [ithrow cval], + (fun clexp -> icomment "unreachable after throw"), + [] + + | AE_field (aval, id, typ) -> + let ctyp = ctyp_of_typ ctx typ in + let setup, cval, cleanup = compile_aval l ctx aval in + setup, + (fun clexp -> icopy l clexp (F_field (fst cval, Util.zencode_string (string_of_id id)), ctyp)), + cleanup + + | AE_for (loop_var, loop_from, loop_to, loop_step, Ord_aux (ord, _), body) -> + (* We assume that all loop indices are safe to put in a CT_fint. *) + let ctx = { ctx with locals = Bindings.add loop_var (Immutable, CT_fint 64) ctx.locals } in + + let is_inc = match ord with + | Ord_inc -> true + | Ord_dec -> false + | Ord_var _ -> raise (Reporting.err_general l "Polymorphic loop direction in C backend") + in + + (* Loop variables *) + let from_setup, from_call, from_cleanup = compile_aexp ctx loop_from in + let from_gs = gensym () in + let to_setup, to_call, to_cleanup = compile_aexp ctx loop_to in + let to_gs = gensym () in + let step_setup, step_call, step_cleanup = compile_aexp ctx loop_step in + let step_gs = gensym () in + let variable_init gs setup call cleanup = + [idecl (CT_fint 64) gs; + iblock (setup @ [call (CL_id (gs, CT_fint 64))] @ cleanup)] + in + + let loop_start_label = label "for_start_" in + let loop_end_label = label "for_end_" in + let body_setup, body_call, body_cleanup = compile_aexp ctx body in + let body_gs = gensym () in + + variable_init from_gs from_setup from_call from_cleanup + @ variable_init to_gs to_setup to_call to_cleanup + @ variable_init step_gs step_setup step_call step_cleanup + @ [iblock ([idecl (CT_fint 64) loop_var; + icopy l (CL_id (loop_var, (CT_fint 64))) (F_id from_gs, (CT_fint 64)); + idecl CT_unit body_gs; + iblock ([ilabel loop_start_label] + @ [ijump (F_op (F_id loop_var, (if is_inc then ">" else "<"), F_id to_gs), CT_bool) loop_end_label] + @ body_setup + @ [body_call (CL_id (body_gs, CT_unit))] + @ body_cleanup + @ [icopy l (CL_id (loop_var, (CT_fint 64))) + (F_op (F_id loop_var, (if is_inc then "+" else "-"), F_id step_gs), (CT_fint 64))] + @ [igoto loop_start_label]); + ilabel loop_end_label])], + (fun clexp -> icopy l clexp unit_fragment), + [] + +and compile_block ctx = function + | [] -> [] + | exp :: exps -> + let setup, call, cleanup = compile_aexp ctx exp in + let rest = compile_block ctx exps in + let gs = gensym () in + iblock (setup @ [idecl CT_unit gs; call (CL_id (gs, CT_unit))] @ cleanup) :: rest + +(** Compile a sail type definition into a IR one. Most of the + actual work of translating the typedefs into C is done by the code + generator, as it's easy to keep track of structs, tuples and unions + in their sail form at this level, and leave the fiddly details of + how they get mapped to C in the next stage. This function also adds + details of the types it compiles to the context, ctx, which is why + it returns a ctypdef * ctx pair. **) +let compile_type_def ctx (TD_aux (type_def, (l, _))) = + match type_def with + | TD_enum (id, ids, _) -> + CTD_enum (id, ids), + { ctx with enums = Bindings.add id (IdSet.of_list ids) ctx.enums } + + | TD_record (id, _, ctors, _) -> + let ctors = List.fold_left (fun ctors (typ, id) -> Bindings.add id (ctyp_of_typ ctx typ) ctors) Bindings.empty ctors in + CTD_struct (id, Bindings.bindings ctors), + { ctx with records = Bindings.add id ctors ctx.records } + + | TD_variant (id, typq, tus, _) -> + let compile_tu = function + | Tu_aux (Tu_ty_id (typ, id), _) -> + let ctx = { ctx with local_env = add_typquant (id_loc id) typq ctx.local_env } in + ctyp_of_typ ctx typ, id + in + let ctus = List.fold_left (fun ctus (ctyp, id) -> Bindings.add id ctyp ctus) Bindings.empty (List.map compile_tu tus) in + CTD_variant (id, Bindings.bindings ctus), + { ctx with variants = Bindings.add id ctus ctx.variants } + + (* Will be re-written before here, see bitfield.ml *) + | TD_bitfield _ -> + Reporting.unreachable l __POS__ "Cannot compile TD_bitfield" + + (* All type abbreviations are filtered out in compile_def *) + | TD_abbrev _ -> + Reporting.unreachable l __POS__ "Found TD_abbrev in compile_type_def" + +let generate_cleanup instrs = + let generate_cleanup' (I_aux (instr, _)) = + match instr with + | I_init (ctyp, id, cval) -> [(id, iclear ctyp id)] + | I_decl (ctyp, id) -> [(id, iclear ctyp id)] + | instr -> [] + in + let is_clear ids = function + | I_aux (I_clear (_, id), _) -> IdSet.add id ids + | _ -> ids + in + let cleaned = List.fold_left is_clear IdSet.empty instrs in + instrs + |> List.map generate_cleanup' + |> List.concat + |> List.filter (fun (id, _) -> not (IdSet.mem id cleaned)) + |> List.map snd + +let fix_exception_block ?return:(return=None) ctx instrs = + let end_block_label = label "end_block_exception_" in + let is_exception_stop (I_aux (instr, _)) = + match instr with + | I_throw _ | I_if _ | I_block _ | I_funcall _ -> true + | _ -> false + in + (* In this function 'after' is instructions after the one we've + matched on, 'before is instructions before the instruction we've + matched with, but after the previous match, and 'historic' are + all the befores from previous matches. *) + let rec rewrite_exception historic instrs = + match instr_split_at is_exception_stop instrs with + | instrs, [] -> instrs + | before, I_aux (I_block instrs, _) :: after -> + before + @ [iblock (rewrite_exception (historic @ before) instrs)] + @ rewrite_exception (historic @ before) after + | before, I_aux (I_if (cval, then_instrs, else_instrs, ctyp), _) :: after -> + let historic = historic @ before in + before + @ [iif cval (rewrite_exception historic then_instrs) (rewrite_exception historic else_instrs) ctyp] + @ rewrite_exception historic after + | before, I_aux (I_throw cval, (_, l)) :: after -> + before + @ [icopy l (CL_current_exception (cval_ctyp cval)) cval; + icopy l CL_have_exception (F_lit (V_bool true), CT_bool)] + @ generate_cleanup (historic @ before) + @ [igoto end_block_label] + @ rewrite_exception (historic @ before) after + | before, (I_aux (I_funcall (x, _, f, args), _) as funcall) :: after -> + let effects = match Env.get_val_spec f ctx.tc_env with + | _, Typ_aux (Typ_fn (_, _, effects), _) -> effects + | exception (Type_error _) -> no_effect (* nullary union constructor, so no val spec *) + | _ -> assert false (* valspec must have function type *) + in + if has_effect effects BE_escape then + before + @ [funcall; + iif (F_have_exception, CT_bool) (generate_cleanup (historic @ before) @ [igoto end_block_label]) [] CT_unit] + @ rewrite_exception (historic @ before) after + else + before @ funcall :: rewrite_exception (historic @ before) after + | _, _ -> assert false (* unreachable *) + in + match return with + | None -> + rewrite_exception [] instrs @ [ilabel end_block_label] + | Some ctyp -> + rewrite_exception [] instrs @ [ilabel end_block_label; iundefined ctyp] + +let rec map_try_block f (I_aux (instr, aux)) = + let instr = match instr with + | I_decl _ | I_reset _ | I_init _ | I_reinit _ -> instr + | I_if (cval, instrs1, instrs2, ctyp) -> + I_if (cval, List.map (map_try_block f) instrs1, List.map (map_try_block f) instrs2, ctyp) + | I_funcall _ | I_copy _ | I_alias _ | I_clear _ | I_throw _ | I_return _ -> instr + | I_block instrs -> I_block (List.map (map_try_block f) instrs) + | I_try_block instrs -> I_try_block (f (List.map (map_try_block f) instrs)) + | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_jump _ | I_match_failure | I_undefined _ | I_end -> instr + in + I_aux (instr, aux) + +let fix_exception ?return:(return=None) ctx instrs = + let instrs = List.map (map_try_block (fix_exception_block ctx)) instrs in + fix_exception_block ~return:return ctx instrs + +let rec compile_arg_pat ctx label (P_aux (p_aux, (l, _)) as pat) ctyp = + match p_aux with + | P_id id -> (id, ([], [])) + | P_wild -> let gs = gensym () in (gs, ([], [])) + | P_tup [] | P_lit (L_aux (L_unit, _)) -> let gs = gensym () in (gs, ([], [])) + | P_var (pat, _) -> compile_arg_pat ctx label pat ctyp + | P_typ (_, pat) -> compile_arg_pat ctx label pat ctyp + | _ -> + let apat = anf_pat pat in + let gs = gensym () in + let destructure, cleanup, _ = compile_match ctx apat (F_id gs, ctyp) label in + (gs, (destructure, cleanup)) + +let rec compile_arg_pats ctx label (P_aux (p_aux, (l, _)) as pat) ctyps = + match p_aux with + | P_typ (_, pat) -> compile_arg_pats ctx label pat ctyps + | P_tup pats when List.length pats = List.length ctyps -> + [], List.map2 (fun pat ctyp -> compile_arg_pat ctx label pat ctyp) pats ctyps, [] + | _ when List.length ctyps = 1 -> + [], [compile_arg_pat ctx label pat (List.nth ctyps 0)], [] + + | _ -> + let arg_id, (destructure, cleanup) = compile_arg_pat ctx label pat (CT_tup ctyps) in + let new_ids = List.map (fun ctyp -> gensym (), ctyp) ctyps in + destructure + @ [idecl (CT_tup ctyps) arg_id] + @ List.mapi (fun i (id, ctyp) -> icopy l (CL_tuple (CL_id (arg_id, CT_tup ctyps), i)) (F_id id, ctyp)) new_ids, + List.map (fun (id, _) -> id, ([], [])) new_ids, + [iclear (CT_tup ctyps) arg_id] + @ cleanup + +let combine_destructure_cleanup xs = List.concat (List.map fst xs), List.concat (List.rev (List.map snd xs)) + +let fix_destructure fail_label = function + | ([], cleanup) -> ([], cleanup) + | destructure, cleanup -> + let body_label = label "fundef_body_" in + (destructure @ [igoto body_label; ilabel fail_label; imatch_failure (); ilabel body_label], cleanup) + +(** Functions that have heap-allocated return types are implemented by + passing a pointer a location where the return value should be + stored. The ANF -> Sail IR pass for expressions simply outputs an + I_return instruction for any return value, so this function walks + over the IR ast for expressions and modifies the return statements + into code that sets that pointer, as well as adds extra control + flow to cleanup heap-allocated variables correctly when a function + terminates early. See the generate_cleanup function for how this is + done. *) +let fix_early_return ret instrs = + let end_function_label = label "end_function_" in + let is_return_recur (I_aux (instr, _)) = + match instr with + | I_return _ | I_undefined _ | I_if _ | I_block _ -> true + | _ -> false + in + let rec rewrite_return historic instrs = + match instr_split_at is_return_recur instrs with + | instrs, [] -> instrs + | before, I_aux (I_block instrs, _) :: after -> + before + @ [iblock (rewrite_return (historic @ before) instrs)] + @ rewrite_return (historic @ before) after + | before, I_aux (I_if (cval, then_instrs, else_instrs, ctyp), _) :: after -> + let historic = historic @ before in + before + @ [iif cval (rewrite_return historic then_instrs) (rewrite_return historic else_instrs) ctyp] + @ rewrite_return historic after + | before, I_aux (I_return cval, (_, l)) :: after -> + let cleanup_label = label "cleanup_" in + let end_cleanup_label = label "end_cleanup_" in + before + @ [icopy l ret cval; + igoto cleanup_label] + (* This is probably dead code until cleanup_label, but we cannot be sure there are no jumps into it. *) + @ rewrite_return (historic @ before) after + @ [igoto end_cleanup_label; + ilabel cleanup_label] + @ generate_cleanup (historic @ before) + @ [igoto end_function_label; + ilabel end_cleanup_label] + | before, I_aux (I_undefined _, (_, l)) :: after -> + let cleanup_label = label "cleanup_" in + let end_cleanup_label = label "end_cleanup_" in + before + @ [igoto cleanup_label] + @ rewrite_return (historic @ before) after + @ [igoto end_cleanup_label; + ilabel cleanup_label] + @ generate_cleanup (historic @ before) + @ [igoto end_function_label; + ilabel end_cleanup_label] + | _, _ -> assert false + in + rewrite_return [] instrs + @ [ilabel end_function_label; iend ()] + +let letdef_count = ref 0 + +(** Compile a Sail toplevel definition into an IR definition **) +let rec compile_def n total ctx def = + match def with + | DEF_fundef (FD_aux (FD_function (_, _, _, [FCL_aux (FCL_Funcl (id, _), _)]), _)) + when !opt_memo_cache -> + let digest = + def |> Pretty_print_sail.doc_def |> Pretty_print_sail.to_string |> Digest.string + in + let cachefile = Filename.concat "_sbuild" ("ccache" ^ Digest.to_hex digest) in + let cached = + if Sys.file_exists cachefile then + let in_chan = open_in cachefile in + try + let compiled = Marshal.from_channel in_chan in + close_in in_chan; + Some (compiled, ctx) + with + | _ -> close_in in_chan; None + else + None + in + begin match cached with + | Some (compiled, ctx) -> + Util.progress "Compiling " (string_of_id id) n total; + compiled, ctx + | None -> + let compiled, ctx = compile_def' n total ctx def in + let out_chan = open_out cachefile in + Marshal.to_channel out_chan compiled [Marshal.Closures]; + close_out out_chan; + compiled, ctx + end + + | _ -> compile_def' n total ctx def + +and compile_def' n total ctx = function + | DEF_reg_dec (DEC_aux (DEC_reg (_, _, typ, id), _)) -> + [CDEF_reg_dec (id, ctyp_of_typ ctx typ, [])], ctx + | DEF_reg_dec (DEC_aux (DEC_config (id, typ, exp), _)) -> + let aexp = ctx.optimize_anf ctx (no_shadow IdSet.empty (anf exp)) in + let setup, call, cleanup = compile_aexp ctx aexp in + let instrs = setup @ [call (CL_id (id, ctyp_of_typ ctx typ))] @ cleanup in + [CDEF_reg_dec (id, ctyp_of_typ ctx typ, instrs)], ctx + + | DEF_reg_dec (DEC_aux (_, (l, _))) -> + raise (Reporting.err_general l "Cannot compile alias register declaration") + + | DEF_spec (VS_aux (VS_val_spec (_, id, _, _), _)) -> + let quant, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_env in + let arg_typs, ret_typ = match fn_typ with + | Typ_fn (arg_typs, ret_typ, _) -> arg_typs, ret_typ + | _ -> assert false + in + let ctx' = { ctx with local_env = add_typquant (id_loc id) quant ctx.local_env } in + let arg_ctyps, ret_ctyp = List.map (ctyp_of_typ ctx') arg_typs, ctyp_of_typ ctx' ret_typ in + [CDEF_spec (id, arg_ctyps, ret_ctyp)], ctx + + | DEF_fundef (FD_aux (FD_function (_, _, _, [FCL_aux (FCL_Funcl (id, Pat_aux (Pat_exp (pat, exp), _)), _)]), _)) -> + Util.progress "Compiling " (string_of_id id) n total; + + (* Find the function's type. *) + let quant, Typ_aux (fn_typ, _) = + try Env.get_val_spec id ctx.local_env with Type_error _ -> Env.get_val_spec id ctx.tc_env + in + let arg_typs, ret_typ = match fn_typ with + | Typ_fn (arg_typs, ret_typ, _) -> arg_typs, ret_typ + | _ -> assert false + in + + (* Handle the argument pattern. *) + let fundef_label = label "fundef_fail_" in + let orig_ctx = ctx in + (* The context must be updated before we call ctyp_of_typ on the argument types. *) + let ctx = { ctx with local_env = add_typquant (id_loc id) quant ctx.tc_env } in + + let arg_ctyps = List.map (ctyp_of_typ ctx) arg_typs in + let ret_ctyp = ctyp_of_typ ctx ret_typ in + + (* Compile the function arguments as patterns. *) + let arg_setup, compiled_args, arg_cleanup = compile_arg_pats ctx fundef_label pat arg_ctyps in + let ctx = + (* We need the primop analyzer to be aware of the function argument types, so put them in ctx *) + List.fold_left2 (fun ctx (id, _) ctyp -> { ctx with locals = Bindings.add id (Immutable, ctyp) ctx.locals }) ctx compiled_args arg_ctyps + in + + (* Optimize and compile the expression to ANF. *) + let aexp = no_shadow (pat_ids pat) (anf exp) in + let aexp = ctx.optimize_anf ctx aexp in + + let setup, call, cleanup = compile_aexp ctx aexp in + let destructure, destructure_cleanup = + compiled_args |> List.map snd |> combine_destructure_cleanup |> fix_destructure fundef_label + in + + let instrs = arg_setup @ destructure @ setup @ [call (CL_return ret_ctyp)] @ cleanup @ destructure_cleanup @ arg_cleanup in + let instrs = fix_early_return (CL_return ret_ctyp) instrs in + let instrs = fix_exception ~return:(Some ret_ctyp) ctx instrs in + [CDEF_fundef (id, None, List.map fst compiled_args, instrs)], orig_ctx + + | DEF_fundef (FD_aux (FD_function (_, _, _, []), (l, _))) -> + raise (Reporting.err_general l "Encountered function with no clauses") + + | DEF_fundef (FD_aux (FD_function (_, _, _, funcls), (l, _))) -> + raise (Reporting.err_general l "Encountered function with multiple clauses") + + (* All abbreviations should expanded by the typechecker, so we don't + need to translate type abbreviations into C typedefs. *) + | DEF_type (TD_aux (TD_abbrev _, _)) -> [], ctx + + | DEF_type type_def -> + let tdef, ctx = compile_type_def ctx type_def in + [CDEF_type tdef], ctx + + | DEF_val (LB_aux (LB_val (pat, exp), _)) -> + let ctyp = ctyp_of_typ ctx (typ_of_pat pat) in + let aexp = ctx.optimize_anf ctx (no_shadow IdSet.empty (anf exp)) in + let setup, call, cleanup = compile_aexp ctx aexp in + let apat = anf_pat ~global:true pat in + let gs = gensym () in + let end_label = label "let_end_" in + let destructure, destructure_cleanup, _ = compile_match ctx apat (F_id gs, ctyp) end_label in + let gs_setup, gs_cleanup = + [idecl ctyp gs], [iclear ctyp gs] + in + let bindings = List.map (fun (id, typ) -> id, ctyp_of_typ ctx typ) (apat_globals apat) in + let n = !letdef_count in + incr letdef_count; + let instrs = + gs_setup @ setup + @ [call (CL_id (gs, ctyp))] + @ cleanup + @ destructure + @ destructure_cleanup @ gs_cleanup + @ [ilabel end_label] + in + [CDEF_let (n, bindings, instrs)], + { ctx with letbinds = n :: ctx.letbinds } + + (* Only DEF_default that matters is default Order, but all order + polymorphism is specialised by this point. *) + | DEF_default _ -> [], ctx + + (* Overloading resolved by type checker *) + | DEF_overload _ -> [], ctx + + (* Only the parser and sail pretty printer care about this. *) + | DEF_fixity _ -> [], ctx + + (* We just ignore any pragmas we don't want to deal with. *) + | DEF_pragma _ -> [], ctx + + (* Termination measures only needed for Coq, and other theorem prover output *) + | DEF_measure _ -> [], ctx + + | DEF_internal_mutrec fundefs -> + let defs = List.map (fun fdef -> DEF_fundef fdef) fundefs in + List.fold_left (fun (cdefs, ctx) def -> let cdefs', ctx = compile_def n total ctx def in (cdefs @ cdefs', ctx)) ([], ctx) defs + + (* Scattereds and mapdefs should be removed by this point *) + | (DEF_scattered _ | DEF_mapdef _) as def -> + raise (Reporting.err_general Parse_ast.Unknown ("Could not compile:\n" ^ Pretty_print_sail.to_string (Pretty_print_sail.doc_def def))) + +let rec specialize_variants ctx prior = + let unifications = ref (Bindings.empty) in + + let fix_variant_ctyp var_id new_ctors = function + | CT_variant (id, ctors) when Id.compare id var_id = 0 -> CT_variant (id, new_ctors) + | ctyp -> ctyp + in + + let specialize_constructor ctx ctor_id ctyp = + function + | I_aux (I_funcall (clexp, extern, id, [cval]), ((_, l) as aux)) as instr when Id.compare id ctor_id = 0 -> + (* Work out how each call to a constructor in instantiated and add that to unifications *) + let unification = List.map ctyp_suprema (ctyp_unify ctyp (cval_ctyp cval)) in + let mono_id = append_id ctor_id ("_" ^ Util.string_of_list "_" (fun ctyp -> Util.zencode_string (string_of_ctyp ctyp)) unification) in + unifications := Bindings.add mono_id (ctyp_suprema (cval_ctyp cval)) !unifications; + + (* We need to cast each cval to it's ctyp_suprema in order to put it in the most general constructor *) + let casts = + let cast_to_suprema (frag, ctyp) = + let suprema = ctyp_suprema ctyp in + if ctyp_equal ctyp suprema then + [], (unpoly frag, ctyp), [] + else + let gs = gensym () in + [idecl suprema gs; + icopy l (CL_id (gs, suprema)) (unpoly frag, ctyp)], + (F_id gs, suprema), + [iclear suprema gs] + in + List.map cast_to_suprema [cval] + in + let setup = List.concat (List.map (fun (setup, _, _) -> setup) casts) in + let cvals = List.map (fun (_, cval, _) -> cval) casts in + let cleanup = List.concat (List.map (fun (_, _, cleanup) -> cleanup) casts) in + + let mk_funcall instr = + if List.length setup = 0 then + instr + else + iblock (setup @ [instr] @ cleanup) + in + + mk_funcall (I_aux (I_funcall (clexp, extern, mono_id, cvals), aux)) + + | I_aux (I_funcall (clexp, extern, id, cvals), ((_, l) as aux)) as instr when Id.compare id ctor_id = 0 -> + Reporting.unreachable l __POS__ "Multiple argument constructor found" + + | instr -> instr + in + + function + | (CDEF_type (CTD_variant (var_id, ctors)) as cdef) :: cdefs -> + let polymorphic_ctors = List.filter (fun (_, ctyp) -> is_polymorphic ctyp) ctors in + + let cdefs = + List.fold_left (fun cdefs (ctor_id, ctyp) -> List.map (cdef_map_instr (specialize_constructor ctx ctor_id ctyp)) cdefs) + cdefs + polymorphic_ctors + in + + let monomorphic_ctors = List.filter (fun (_, ctyp) -> not (is_polymorphic ctyp)) ctors in + let specialized_ctors = Bindings.bindings !unifications in + let new_ctors = monomorphic_ctors @ specialized_ctors in + + let ctx = { + ctx with variants = Bindings.add var_id + (List.fold_left (fun m (id, ctyp) -> Bindings.add id ctyp m) !unifications monomorphic_ctors) + ctx.variants + } in + + let cdefs = List.map (cdef_map_ctyp (map_ctyp (fix_variant_ctyp var_id new_ctors))) cdefs in + let prior = List.map (cdef_map_ctyp (map_ctyp (fix_variant_ctyp var_id new_ctors))) prior in + specialize_variants ctx (CDEF_type (CTD_variant (var_id, new_ctors)) :: prior) cdefs + + | cdef :: cdefs -> + let remove_poly (I_aux (instr, aux)) = + match instr with + | I_copy (clexp, (frag, ctyp)) when is_polymorphic ctyp -> + I_aux (I_copy (clexp, (frag, ctyp_suprema (clexp_ctyp clexp))), aux) + | instr -> I_aux (instr, aux) + in + let cdef = cdef_map_instr remove_poly cdef in + specialize_variants ctx (cdef :: prior) cdefs + + | [] -> List.rev prior, ctx + +(** Once we specialize variants, there may be additional type + dependencies which could be in the wrong order. As such we need to + sort the type definitions in the list of cdefs. *) +let sort_ctype_defs cdefs = + (* Split the cdefs into type definitions and non type definitions *) + let is_ctype_def = function CDEF_type _ -> true | _ -> false in + let unwrap = function CDEF_type ctdef -> ctdef | _ -> assert false in + let ctype_defs = List.map unwrap (List.filter is_ctype_def cdefs) in + let cdefs = List.filter (fun cdef -> not (is_ctype_def cdef)) cdefs in + + let ctdef_id = function + | CTD_enum (id, _) | CTD_struct (id, _) | CTD_variant (id, _) -> id + in + + let ctdef_ids = function + | CTD_enum _ -> IdSet.empty + | CTD_struct (_, ctors) | CTD_variant (_, ctors) -> + List.fold_left (fun ids (_, ctyp) -> IdSet.union (ctyp_ids ctyp) ids) IdSet.empty ctors + in + + (* Create a reverse (i.e. from types to the types that are dependent + upon them) id graph of dependencies between types *) + let module IdGraph = Graph.Make(Id) in + + let graph = + List.fold_left (fun g ctdef -> + List.fold_left (fun g id -> IdGraph.add_edge id (ctdef_id ctdef) g) + (IdGraph.add_edges (ctdef_id ctdef) [] g) (* Make sure even types with no dependencies are in graph *) + (IdSet.elements (ctdef_ids ctdef))) + IdGraph.empty + ctype_defs + in + + (* Then select the ctypes in the correct order as given by the topsort *) + let ids = IdGraph.topsort graph in + let ctype_defs = + List.map (fun id -> CDEF_type (List.find (fun ctdef -> Id.compare (ctdef_id ctdef) id = 0) ctype_defs)) ids + in + + ctype_defs @ cdefs + +let compile_ast ctx (Defs defs) = + let assert_vs = Initial_check.extern_of_string (mk_id "sail_assert") "(bool, string) -> unit effect {escape}" in + let exit_vs = Initial_check.extern_of_string (mk_id "sail_exit") "unit -> unit effect {escape}" in + + let ctx = { ctx with tc_env = snd (Type_error.check ctx.tc_env (Defs [assert_vs; exit_vs])) } in + + if !opt_memo_cache then + (try + if Sys.is_directory "_sbuild" then + () + else + raise (Reporting.err_general Parse_ast.Unknown "_sbuild exists, but is a file not a directory!") + with + | Sys_error _ -> Unix.mkdir "_sbuild" 0o775) + else (); + + let total = List.length defs in + let _, chunks, ctx = + List.fold_left (fun (n, chunks, ctx) def -> let defs, ctx = compile_def n total ctx def in n + 1, defs :: chunks, ctx) (1, [], ctx) defs + in + let cdefs = List.concat (List.rev chunks) in + let cdefs, ctx = specialize_variants ctx [] cdefs in + let cdefs = sort_ctype_defs cdefs in + cdefs, ctx diff --git a/src/bytecode_interpreter.ml b/src/jib/jib_compile.mli index 398e0c9d..50054149 100644 --- a/src/bytecode_interpreter.ml +++ b/src/jib/jib_compile.mli @@ -48,115 +48,40 @@ (* SUCH DAMAGE. *) (**************************************************************************) +open Anf open Ast open Ast_util -open Bytecode -open Bytecode_util - -module StringMap = Map.Make(String) - -type 'a frame = { - jump_table : int StringMap.t; - locals : 'a Bindings.t; - pc : int; - instrs : instr array - } - -type 'a gstate = { - globals : 'a Bindings.t; - cdefs : cdef list - } - -type 'a stack = { - top : 'a frame; - ret : ('a -> 'a frame) list - } - -let make_jump_table instrs = - let rec aux n = function - | I_aux (I_label label, _) :: instrs -> StringMap.add label n (aux (n + 1) instrs) - | _ :: instrs -> aux (n + 1) instrs - | [] -> StringMap.empty - in - aux 0 instrs - -let new_gstate cdefs = { - globals = Bindings.empty; - cdefs = cdefs +open Jib +open Type_check + +(** Context for compiling Sail to Jib. We need to pass a (global) + typechecking environment given by checking the full AST. We have to + provide a conversion function from Sail types into Jib types, as + well as a function that optimizes ANF expressions (which can just + be the identity function) *) +type ctx = + { records : (ctyp Bindings.t) Bindings.t; + enums : IdSet.t Bindings.t; + variants : (ctyp Bindings.t) Bindings.t; + tc_env : Env.t; + local_env : Env.t; + locals : (mut * ctyp) Bindings.t; + letbinds : int list; + no_raw : bool; + convert_typ : ctx -> typ -> ctyp; + optimize_anf : ctx -> typ aexp -> typ aexp } -let new_stack instrs = { - top = { - jump_table = make_jump_table instrs; - locals = Bindings.empty; - pc = 0; - instrs = Array.of_list instrs - }; - ret = [] - } - -let with_top stack f = - { stack with top = f (stack.top) } - -let eval_fragment gstate locals = function - | F_id id -> - begin match Bindings.find_opt id locals with - | Some vl -> vl - | None -> - begin match Bindings.find_opt id gstate.globals with - | Some vl -> vl - | None -> failwith "Identifier not found" - end - end - | F_lit vl -> vl - | _ -> failwith "Cannot eval fragment" - -let is_function id = function - | CDEF_fundef (id', _, _, _) when Id.compare id id' = 0 -> true - | _ -> false - -let step (gstate, stack) = - let I_aux (instr_aux, (_, l)) = stack.top.instrs.(stack.top.pc) in - match instr_aux with - | I_decl _ -> - gstate, with_top stack (fun frame -> { frame with pc = frame.pc + 1 }) - - | I_init (_, id, (fragment, _)) -> - let vl = eval_fragment gstate stack.top.locals fragment in - gstate, - with_top stack (fun frame -> { frame with pc = frame.pc + 1; locals = Bindings.add id vl frame.locals }) - - | I_jump ((fragment, _), label) -> - let vl = eval_fragment gstate stack.top.locals fragment in - gstate, - begin match vl with - | V_bool true -> - with_top stack (fun frame -> { frame with pc = StringMap.find label frame.jump_table }) - | V_bool false -> - with_top stack (fun frame -> { frame with pc = frame.pc + 1 }) - | _ -> - failwith "Type error" - end - - | I_funcall (clexp, _, id, cvals) -> - let args = List.map (fun (fragment, _) -> eval_fragment gstate stack.top.locals fragment) cvals in - let params, instrs = - match List.find_opt (is_function id) gstate.cdefs with - | Some (CDEF_fundef (_, _, params, instrs)) -> params, instrs - | _ -> failwith "Function not found" - in - gstate, - { - top = { - jump_table = make_jump_table instrs; - locals = List.fold_left2 (fun locals param arg -> Bindings.add param arg locals) Bindings.empty params args; - pc = 0; - instrs = Array.of_list instrs; - }; - ret = (fun vl -> { stack.top with pc = stack.top.pc + 1 }) :: stack.ret - } +val initial_ctx : + convert_typ:(ctx -> typ -> ctyp) -> + optimize_anf:(ctx -> typ aexp -> typ aexp) -> + Env.t -> + ctx - | I_goto label -> - gstate, with_top stack (fun frame -> { frame with pc = StringMap.find label frame.jump_table }) +(** Compile a Sail definition into a Jib definition. The first two + arguments are is the current definition number and the total number + of definitions, and can be used to drive a progress bar (see + Util.progress). *) +val compile_def : int -> int -> ctx -> tannot def -> cdef list * ctx - | _ -> raise (Reporting.err_unreachable l __POS__ "Unhandled instruction") +val compile_ast : ctx -> tannot defs -> cdef list * ctx diff --git a/src/bytecode_util.ml b/src/jib/jib_util.ml index 630d2a48..d9c6a541 100644 --- a/src/bytecode_util.ml +++ b/src/jib/jib_util.ml @@ -50,7 +50,7 @@ open Ast open Ast_util -open Bytecode +open Jib open Value2 open PPrint @@ -94,6 +94,9 @@ let iclear ?loc:(l=Parse_ast.Unknown) ctyp id = let ireturn ?loc:(l=Parse_ast.Unknown) cval = I_aux (I_return cval, (instr_number (), l)) +let iend ?loc:(l=Parse_ast.Unknown) () = + I_aux (I_end, (instr_number (), l)) + let iblock ?loc:(l=Parse_ast.Unknown) instrs = I_aux (I_block instrs, (instr_number (), l)) @@ -150,6 +153,7 @@ let rec clexp_rename from_id to_id = function CL_tuple (clexp_rename from_id to_id clexp, n) | CL_current_exception ctyp -> CL_current_exception ctyp | CL_have_exception -> CL_have_exception + | CL_return ctyp -> CL_return ctyp let rec instr_rename from_id to_id (I_aux (instr, aux)) = let instr = match instr with @@ -198,6 +202,8 @@ let rec instr_rename from_id to_id (I_aux (instr, aux)) = | I_match_failure -> I_match_failure + | I_end -> I_end + | I_reset (ctyp, id) when Id.compare id from_id = 0 -> I_reset (ctyp, to_id) | I_reset (ctyp, id) -> I_reset (ctyp, id) @@ -257,8 +263,8 @@ and string_of_ctyp = function | CT_lbits false -> "lbits(inc)" | CT_fbits (n, true) -> "fbits(" ^ string_of_int n ^ ", dec)" | CT_fbits (n, false) -> "fbits(" ^ string_of_int n ^ ", int)" - | CT_sbits true -> "sbits(dec)" - | CT_sbits false -> "sbits(inc)" + | CT_sbits (n, true) -> "sbits(" ^ string_of_int n ^ ", dec)" + | CT_sbits (n, false) -> "sbits(" ^ string_of_int n ^ ", inc)" | CT_fint n -> "int(" ^ string_of_int n ^ ")" | CT_bit -> "bit" | CT_unit -> "unit" @@ -276,31 +282,17 @@ and string_of_ctyp = function (** This function is like string_of_ctyp, but recursively prints all constructors in variants and structs. Used for debug output. *) and full_string_of_ctyp = function - | CT_lint -> "int" - | CT_lbits true -> "lbits(dec)" - | CT_lbits false -> "lbits(inc)" - | CT_fbits (n, true) -> "fbits(" ^ string_of_int n ^ ", dec)" - | CT_fbits (n, false) -> "fbits(" ^ string_of_int n ^ ", int)" - | CT_sbits true -> "sbits(dec)" - | CT_sbits false -> "sbits(inc)" - | CT_fint n -> "int(" ^ string_of_int n ^ ")" - | CT_bit -> "bit" - | CT_unit -> "unit" - | CT_bool -> "bool" - | CT_real -> "real" | CT_tup ctyps -> "(" ^ Util.string_of_list ", " full_string_of_ctyp ctyps ^ ")" - | CT_enum (id, _) -> string_of_id id | CT_struct (id, ctors) | CT_variant (id, ctors) -> "struct " ^ string_of_id id ^ "{ " ^ Util.string_of_list ", " (fun (id, ctyp) -> string_of_id id ^ " : " ^ full_string_of_ctyp ctyp) ctors ^ "}" - | CT_string -> "string" | CT_vector (true, ctyp) -> "vector(dec, " ^ full_string_of_ctyp ctyp ^ ")" | CT_vector (false, ctyp) -> "vector(inc, " ^ full_string_of_ctyp ctyp ^ ")" | CT_list ctyp -> "list(" ^ full_string_of_ctyp ctyp ^ ")" | CT_ref ctyp -> "ref(" ^ full_string_of_ctyp ctyp ^ ")" - | CT_poly -> "*" + | ctyp -> string_of_ctyp ctyp let rec map_ctyp f = function | (CT_lint | CT_fint _ | CT_lbits _ | CT_fbits _ | CT_sbits _ @@ -316,7 +308,7 @@ let rec ctyp_equal ctyp1 ctyp2 = match ctyp1, ctyp2 with | CT_lint, CT_lint -> true | CT_lbits d1, CT_lbits d2 -> d1 = d2 - | CT_sbits d1, CT_sbits d2 -> d1 = d2 + | CT_sbits (m1, d1), CT_sbits (m2, d2) -> m1 = m2 && d1 = d2 | CT_fbits (m1, d1), CT_fbits (m2, d2) -> m1 = m2 && d1 = d2 | CT_bit, CT_bit -> true | CT_fint n, CT_fint m -> n = m @@ -335,6 +327,75 @@ let rec ctyp_equal ctyp1 ctyp2 = | CT_poly, CT_poly -> true | _, _ -> false +let rec ctyp_compare ctyp1 ctyp2 = + let lex_ord c1 c2 = if c1 = 0 then c2 else c1 in + match ctyp1, ctyp2 with + | CT_lint, CT_lint -> 0 + | CT_lint, _ -> 1 + | _, CT_lint -> -1 + + | CT_fint n, CT_fint m -> compare n m + | CT_fint _, _ -> 1 + | _, CT_fint _ -> -1 + + | CT_fbits (n, ord1), CT_fbits (m, ord2) -> lex_ord (compare n m) (compare ord1 ord2) + | CT_fbits _, _ -> 1 + | _, CT_fbits _ -> -1 + + | CT_sbits (n, ord1), CT_sbits (m, ord2) -> lex_ord (compare n m) (compare ord1 ord2) + | CT_sbits _, _ -> 1 + | _, CT_sbits _ -> -1 + + | CT_lbits ord1 , CT_lbits ord2 -> compare ord1 ord2 + | CT_lbits _, _ -> 1 + | _, CT_lbits _ -> -1 + + | CT_bit, CT_bit -> 0 + | CT_bit, _ -> 1 + | _, CT_bit -> -1 + + | CT_unit, CT_unit -> 0 + | CT_unit, _ -> 1 + | _, CT_unit -> -1 + + | CT_real, CT_real -> 0 + | CT_real, _ -> 1 + | _, CT_real -> -1 + + | CT_poly, CT_poly -> 0 + | CT_poly, _ -> 1 + | _, CT_poly -> -1 + + | CT_bool, CT_bool -> 0 + | CT_bool, _ -> 1 + | _, CT_bool -> -1 + + | CT_string, CT_string -> 0 + | CT_string, _ -> 1 + | _, CT_string -> -1 + + | CT_ref ctyp1, CT_ref ctyp2 -> ctyp_compare ctyp1 ctyp2 + | CT_ref _, _ -> 1 + | _, CT_ref _ -> -1 + + | CT_list ctyp1, CT_list ctyp2 -> ctyp_compare ctyp1 ctyp2 + | CT_list _, _ -> 1 + | _, CT_list _ -> -1 + + | CT_vector (d1, ctyp1), CT_vector (d2, ctyp2) -> + lex_ord (ctyp_compare ctyp1 ctyp2) (compare d1 d2) + | CT_vector _, _ -> 1 + | _, CT_vector _ -> -1 + + | ctyp1, ctyp2 -> String.compare (full_string_of_ctyp ctyp1) (full_string_of_ctyp ctyp2) + +module CT = struct + type t = ctyp + let compare ctyp1 ctyp2 = ctyp_compare ctyp1 ctyp2 +end + +module CTSet = Set.Make(CT) + let rec ctyp_unify ctyp1 ctyp2 = match ctyp1, ctyp2 with | CT_tup ctyps1, CT_tup ctyps2 when List.length ctyps1 = List.length ctyps2 -> @@ -356,7 +417,7 @@ let rec ctyp_suprema = function | CT_lint -> CT_lint | CT_lbits d -> CT_lbits d | CT_fbits (_, d) -> CT_lbits d - | CT_sbits d -> CT_lbits d + | CT_sbits (_, d) -> CT_lbits d | CT_fint _ -> CT_lint | CT_unit -> CT_unit | CT_bool -> CT_bool @@ -420,6 +481,7 @@ let rec pp_clexp = function | CL_addr clexp -> string "*" ^^ pp_clexp clexp | CL_current_exception ctyp -> string "current_exception : " ^^ pp_ctyp ctyp | CL_have_exception -> string "have_exception" + | CL_return ctyp -> string "return : " ^^ pp_ctyp ctyp let rec pp_instr ?short:(short=false) (I_aux (instr, aux)) = match instr with @@ -470,6 +532,8 @@ let rec pp_instr ?short:(short=false) (I_aux (instr, aux)) = pp_keyword "goto" ^^ string (str |> Util.blue |> Util.clear) | I_match_failure -> pp_keyword "match_failure" + | I_end -> + pp_keyword "end" | I_undefined ctyp -> pp_keyword "undefined" ^^ pp_ctyp ctyp | I_raw str -> @@ -570,6 +634,7 @@ let rec clexp_deps = function | CL_addr clexp -> clexp_deps clexp | CL_have_exception -> IdSet.empty | CL_current_exception _ -> IdSet.empty + | CL_return _ -> IdSet.empty (* Return the direct, read/write dependencies of a single instruction *) let instr_deps = function @@ -589,6 +654,7 @@ let instr_deps = function | I_goto label -> IdSet.empty, IdSet.empty | I_undefined _ -> IdSet.empty, IdSet.empty | I_match_failure -> IdSet.empty, IdSet.empty + | I_end -> IdSet.empty, IdSet.empty (* instrs_graph returns the control-flow graph for a list of instructions. *) @@ -671,6 +737,7 @@ let rec map_clexp_ctyp f = function | CL_addr clexp -> CL_addr (map_clexp_ctyp f clexp) | CL_current_exception ctyp -> CL_current_exception (f ctyp) | CL_have_exception -> CL_have_exception + | CL_return ctyp -> CL_return (f ctyp) let rec map_instr_ctyp f (I_aux (instr, aux)) = let instr = match instr with @@ -691,6 +758,7 @@ let rec map_instr_ctyp f (I_aux (instr, aux)) = | I_undefined ctyp -> I_undefined (f ctyp) | I_reset (ctyp, id) -> I_reset (f ctyp, id) | I_reinit (ctyp1, id, (frag, ctyp2)) -> I_reinit (f ctyp1, id, (frag, f ctyp2)) + | I_end -> I_end | (I_comment _ | I_raw _ | I_label _ | I_goto _ | I_match_failure) as instr -> instr in I_aux (instr, aux) @@ -700,7 +768,7 @@ let rec map_instr f (I_aux (instr, aux)) = let instr = match instr with | I_decl _ | I_init _ | I_reset _ | I_reinit _ | I_funcall _ | I_copy _ | I_alias _ | I_clear _ | I_jump _ | I_throw _ | I_return _ - | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_match_failure | I_undefined _ -> instr + | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_match_failure | I_undefined _ | I_end -> instr | I_if (cval, instrs1, instrs2, ctyp) -> I_if (cval, List.map (map_instr f) instrs1, List.map (map_instr f) instrs2, ctyp) | I_block instrs -> @@ -744,7 +812,7 @@ let rec map_instrs f (I_aux (instr, aux)) = | I_funcall _ | I_copy _ | I_alias _ | I_clear _ | I_jump _ | I_throw _ | I_return _ -> instr | I_block instrs -> I_block (f (List.map (map_instrs f) instrs)) | I_try_block instrs -> I_try_block (f (List.map (map_instrs f) instrs)) - | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_match_failure | I_undefined _ -> instr + | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_match_failure | I_undefined _ | I_end -> instr in I_aux (instr, aux) @@ -769,3 +837,99 @@ let rec filter_instrs f instrs = | instr -> instr in List.filter f (List.map filter_instrs' instrs) + +(** GLOBAL: label_counter is used to make sure all labels have unique + names. Like gensym_counter it should be safe to reset between + top-level definitions. **) +let label_counter = ref 0 + +let label str = + let str = str ^ string_of_int !label_counter in + incr label_counter; + str + +let cval_ctyp = function (_, ctyp) -> ctyp + +let rec clexp_ctyp = function + | CL_id (_, ctyp) -> ctyp + | CL_return ctyp -> ctyp + | CL_field (clexp, field) -> + begin match clexp_ctyp clexp with + | CT_struct (id, ctors) -> + begin + try snd (List.find (fun (id, ctyp) -> string_of_id id = field) ctors) with + | Not_found -> failwith ("Struct type " ^ string_of_id id ^ " does not have a constructor " ^ field) + end + | ctyp -> failwith ("Bad ctyp for CL_field " ^ string_of_ctyp ctyp) + end + | CL_addr clexp -> + begin match clexp_ctyp clexp with + | CT_ref ctyp -> ctyp + | ctyp -> failwith ("Bad ctyp for CL_addr " ^ string_of_ctyp ctyp) + end + | CL_tuple (clexp, n) -> + begin match clexp_ctyp clexp with + | CT_tup typs -> + begin + try List.nth typs n with + | _ -> failwith "Tuple assignment index out of bounds" + end + | ctyp -> failwith ("Bad ctyp for CL_addr " ^ string_of_ctyp ctyp) + end + | CL_have_exception -> CT_bool + | CL_current_exception ctyp -> ctyp + +let rec instr_ctyps (I_aux (instr, aux)) = + match instr with + | I_decl (ctyp, _) | I_reset (ctyp, _) | I_clear (ctyp, _) | I_undefined ctyp -> + CTSet.singleton ctyp + | I_init (ctyp, _, cval) | I_reinit (ctyp, _, cval) -> + CTSet.add ctyp (CTSet.singleton (cval_ctyp cval)) + | I_if (cval, instrs1, instrs2, ctyp) -> + CTSet.union (instrs_ctyps instrs1) (instrs_ctyps instrs2) + |> CTSet.add (cval_ctyp cval) + |> CTSet.add ctyp + | I_funcall (clexp, _, _, cvals) -> + List.fold_left (fun m ctyp -> CTSet.add ctyp m) CTSet.empty (List.map cval_ctyp cvals) + |> CTSet.add (clexp_ctyp clexp) + | I_copy (clexp, cval) | I_alias (clexp, cval) -> + CTSet.add (clexp_ctyp clexp) (CTSet.singleton (cval_ctyp cval)) + | I_block instrs | I_try_block instrs -> + instrs_ctyps instrs + | I_throw cval | I_jump (cval, _) | I_return cval -> + CTSet.singleton (cval_ctyp cval) + | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_match_failure | I_end -> + CTSet.empty + +and instrs_ctyps instrs = List.fold_left CTSet.union CTSet.empty (List.map instr_ctyps instrs) + +let ctype_def_ctyps = function + | CTD_enum _ -> [] + | CTD_struct (_, fields) -> List.map snd fields + | CTD_variant (_, ctors) -> List.map snd ctors + +let cdef_ctyps = function + | CDEF_reg_dec (_, ctyp, instrs) -> + CTSet.add ctyp (instrs_ctyps instrs) + | CDEF_spec (_, ctyps, ctyp) -> + CTSet.add ctyp (List.fold_left (fun m ctyp -> CTSet.add ctyp m) CTSet.empty ctyps) + | CDEF_fundef (_, _, _, instrs) | CDEF_startup (_, instrs) | CDEF_finish (_, instrs) -> + instrs_ctyps instrs + | CDEF_type tdef -> + List.fold_right CTSet.add (ctype_def_ctyps tdef) CTSet.empty + | CDEF_let (_, bindings, instrs) -> + List.fold_left (fun m ctyp -> CTSet.add ctyp m) CTSet.empty (List.map snd bindings) + |> CTSet.union (instrs_ctyps instrs) + +let rec c_ast_registers = function + | CDEF_reg_dec (id, ctyp, instrs) :: ast -> (id, ctyp, instrs) :: c_ast_registers ast + | _ :: ast -> c_ast_registers ast + | [] -> [] + +let instr_split_at f = + let rec instr_split_at' f before = function + | [] -> (List.rev before, []) + | instr :: instrs when f instr -> (List.rev before, instr :: instrs) + | instr :: instrs -> instr_split_at' f (instr :: before) instrs + in + instr_split_at' f [] diff --git a/src/sail.ml b/src/sail.ml index 77f0e32d..813d8ec1 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -183,11 +183,8 @@ let options = Arg.align ([ Arg.Set C_backend.opt_static, " make generated C functions static"); ( "-trace", - Arg.Tuple [Arg.Set C_backend.opt_trace; Arg.Set Ocaml_backend.opt_trace_ocaml], + Arg.Tuple [Arg.Set Ocaml_backend.opt_trace_ocaml], " instrument output with tracing"); - ( "-smt_trace", - Arg.Tuple [Arg.Set C_backend.opt_smt_trace], - " instrument output with tracing for SMT"); ( "-cgen", Arg.Set opt_print_cgen, " generate CGEN source"); @@ -310,9 +307,6 @@ let options = Arg.align ([ ( "-dmagic_hash", Arg.Set Initial_check.opt_magic_hash, " (debug) allow special character # in identifiers"); - ( "-dfunction", - Arg.String (fun f -> C_backend.opt_debug_function := f), - " (debug) print debugging output for a single function"); ( "-dprofile", Arg.Set Profile.opt_profile, " (debug) provide basic profiling information for rewriting passes within Sail"); @@ -441,22 +435,22 @@ let main() = in let output_chan = match !opt_file_out with Some f -> open_out (f ^ ".c") | None -> stdout in Util.opt_warnings := true; - C_backend.compile_ast (C_backend.initial_ctx type_envs) output_chan (!opt_includes_c) ast_c; + C_backend.compile_ast type_envs output_chan (!opt_includes_c) ast_c; close_out output_chan else ()); (if !(opt_print_ir) then let ast_c = rewrite_ast_c type_envs ast in let ast_c, type_envs = Specialize.(specialize typ_ord_specialization ast_c type_envs) in - let ast_c, type_envs = Specialize.(specialize' 2 int_specialization_with_externs ast_c type_envs) in + let ast_c, type_envs = Specialize.(specialize' 2 int_specialization ast_c type_envs) in let output_chan = match !opt_file_out with | Some f -> Util.opt_colors := false; open_out (f ^ ".ir.sail") | None -> stdout in Util.opt_warnings := true; - let cdefs = C_backend.(bytecode_ast (initial_ctx_iterate type_envs) (List.map flatten_cdef) ast_c) in - let str = Pretty_print_sail.to_string PPrint.(separate_map hardline Bytecode_util.pp_cdef cdefs) in + let cdefs, _ = C_backend.jib_of_ast type_envs ast_c in + let str = Pretty_print_sail.to_string PPrint.(separate_map hardline Jib_util.pp_cdef cdefs) in output_string output_chan (str ^ "\n"); close_out output_chan else ()); |