diff options
| -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 ()); |