diff options
| -rw-r--r-- | language/bytecode.ott | 133 | ||||
| -rw-r--r-- | src/Makefile | 13 | ||||
| -rw-r--r-- | src/ast.sed | 1 | ||||
| -rw-r--r-- | src/c_backend.ml | 667 |
4 files changed, 450 insertions, 364 deletions
diff --git a/language/bytecode.ott b/language/bytecode.ott new file mode 100644 index 00000000..7342a1e9 --- /dev/null +++ b/language/bytecode.ott @@ -0,0 +1,133 @@ +indexvar n , m , i , j ::= + {{ phantom }} + {{ com Index variables for meta-lists }} + +metavar nat ::= + {{ phantom }} + {{ ocaml int }} + {{ lem nat }} + +metavar id ::= + {{ phantom }} + {{ ocaml id }} + {{ lem id }} + +metavar mid ::= + {{ phantom }} + {{ ocaml id option }} + {{ lem maybe id }} + +metavar string ::= + {{ phantom }} + {{ ocaml string }} + {{ lem string }} + +metavar op ::= + {{ phantom }} + {{ ocaml string }} + {{ lem string }} + +metavar bool ::= + {{ phantom }} + {{ ocaml bool }} + {{ lem bool }} + +embed +{{ lem + +open import Ast + +}} + +grammar + + +% Fragments are small pure snippets of (abstract) C code, mostly +% expressions, used by the aval and cval types. +fragment :: 'F_' ::= + | id :: :: id + | string :: :: lit + | have_exception :: :: have_exception + | current_exception :: :: current_exception + | fragment op fragment' :: :: op + | op fragment :: :: unary + | fragment . string :: :: field + +ctyp :: 'CT_' ::= + {{ com C type }} + | mpz_t :: :: mpz +% Arbitrary precision GMP integer, mpz_t in C. }} + | bv_t ( bool ) :: :: bv +% Variable length bitvector - flag represents direction, inc or dec }} + | uint64_t ( nat , bool ) :: :: uint64 +% Fixed length bitvector that fits within a 64-bit word. - int +% represents length, and flag is the same as CT_bv. }} + | int64_t :: :: int64 +% 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. + | 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 + | string_t :: :: string + | enum id ( id0 , ... , idn ) :: :: enum + | struct id ( id0 * ctyp0 , ... , idn * ctypn ) :: :: struct + | variant id ( id0 * ctyp0 , ... , idn * ctypn ) :: :: variant +% 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. + +cval :: 'CV_' ::= + {{ ocaml fragment * ctyp }} + {{ lem fragment * ctyp }} + +clexp :: 'CL_' ::= + | id :: :: id + | id . string :: :: field + | * id :: :: addr + | current_exception :: :: current_exception + | have_exception :: :: have_exception + +ctype_def :: 'CTD_' ::= + {{ com C type definition }} + | enum id = id0 '|' ... '|' idn :: :: enum + | struct id = { id0 : ctyp0 , ... , idn : ctypn } :: :: struct + | variant id = { id0 : ctyp0 , ... , idn : ctypn } :: :: variant + +iannot :: 'IA_' ::= + {{ lem nat * nat * nat }} + {{ ocaml int * int * int }} + +instr :: 'I_' ::= + {{ aux _ iannot }} + | ctyp id :: :: decl + | alloc ctyp id :: :: alloc + | ctyp id = cval :: :: init + | if ( cval ) { instr0 ; ... ; instrn } + else { instr0 ; ... ; instrm } : ctyp :: :: if + | clexp = id ( cval0 , ... , cvaln ) : ctyp :: :: funcall + | clexp = cval :: :: copy + | clexp = ( ctyp ) id : ctyp' :: :: convert + | clear ctyp id :: :: clear + | return cval :: :: return + | { instr0 ; ... ; instrn } :: :: block + | try { instr0 ; ... ; instrn } :: :: try_block + | throw cval :: :: throw + | '//' string :: :: comment + | C string :: :: raw % only used for GCC attributes + | string : :: :: label + | goto string :: :: goto + | match_failure :: :: match_failure + +cdef :: 'CDEF_' ::= + | register id : ctyp :: :: reg_dec + | ctype_def :: :: type + | function id mid ( id0 , ... , idn ) { + instr0 ; ... ; instrm + } :: :: fundef
\ No newline at end of file diff --git a/src/Makefile b/src/Makefile index 2a9fcc32..924cfb1c 100644 --- a/src/Makefile +++ b/src/Makefile @@ -60,17 +60,24 @@ full: sail lib power doc test ast.lem: ../language/l2.ott ott -sort false -generate_aux_rules true -o ast.lem -picky_multiple_parses true ../language/l2.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 + ast.ml: ast.lem lem -ocaml ast.lem sed -i -f ast.sed ast.ml +bytecode.ml: bytecode.lem + lem -ocaml bytecode.lem + sed -i -f ast.sed bytecode.ml + lem_interp/interp_ast.lem: ../language/l2.ott ott -sort false -generate_aux_rules true -o lem_interp/interp_ast.lem -picky_multiple_parses true ../language/l2.ott -sail: ast.ml +sail: ast.ml bytecode.ml ocamlbuild -use-ocamlfind sail.native -isail: ast.ml +isail: ast.ml bytecode.ml ocamlbuild -use-ocamlfind isail.native sail.native: sail @@ -265,6 +272,8 @@ clean: -rm -rf sail.docdir -rm -f ast.ml -rm -f ast.lem + -rm -f bytecode.ml + -rm -f bytecode.lem doc: ocamlbuild -use-ocamlfind sail.docdir/index.html diff --git a/src/ast.sed b/src/ast.sed index 39c58a50..3f53dc78 100644 --- a/src/ast.sed +++ b/src/ast.sed @@ -1,2 +1,3 @@ s/type l = | Unknown/type l = Parse_ast.l/ s/type value = | Val/open Value/ +s/type iannot = int \* int \* int/type iannot = int \* Parse_ast.l/
\ No newline at end of file diff --git a/src/c_backend.ml b/src/c_backend.ml index d39680b9..753922f2 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -50,6 +50,7 @@ open Ast open Ast_util +open Bytecode open Type_check open PPrint module Big_int = Nat_big_num @@ -74,15 +75,6 @@ let lvar_typ = function (* | Union (_, typ) -> typ *) | _ -> assert false -(** Fragments are small pure snippets of C code, mostly expressions, - used by the AV_C_fragment and CV_C_fragment constructors. *) -type fragment = - | F_id of id - | F_lit of string - | F_field of fragment * string - | F_op of fragment * string * fragment - | F_unary of string * fragment - let rec string_of_fragment = function | F_id id -> Util.zencode_string (string_of_id id) | F_lit str -> str @@ -92,6 +84,8 @@ let rec string_of_fragment = function Printf.sprintf "%s %s %s" (string_of_fragment' f1) op (string_of_fragment f2) | F_unary (op, f) -> op ^ string_of_fragment' f + | F_have_exception -> "have_exception" + | F_current_exception -> "(*current_exception)" and string_of_fragment' f = match f with | F_op _ -> "(" ^ string_of_fragment f ^ ")" @@ -537,35 +531,6 @@ let rec anf (E_aux (e_aux, exp_annot) as exp) = let max_int64 = Big_int.of_int64 Int64.max_int let min_int64 = Big_int.of_int64 Int64.min_int -type ctyp = - (* Arbitrary precision GMP integer, mpz_t in C. *) - | CT_mpz - (* The real type in sail. Abstract here, but implemented using - either GMP rationals or high-precision floating point. *) - | CT_real - (* Variable length bitvector - flag represents direction, inc or dec *) - | CT_bv of bool - (* Fixed length bitvector that fits within a 64-bit word. - int - represents length, and flag is the same as CT_bv. *) - | CT_uint64 of int * bool - | CT_int - (* Used for (signed) integers that fit within 64-bits. *) - | CT_int64 - (* 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. *) - | CT_unit - | CT_bool - (* 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. *) - | CT_tup of ctyp list - | CT_struct of id * ctyp Bindings.t - | CT_enum of id * IdSet.t - | CT_variant of id * ctyp Bindings.t - | CT_string - type ctx = { records : (ctyp Bindings.t) Bindings.t; enums : IdSet.t Bindings.t; @@ -585,7 +550,7 @@ let rec ctyp_equal ctyp1 ctyp2 = | CT_mpz, CT_mpz -> true | CT_bv d1, CT_bv d2 -> d1 = d2 | CT_uint64 (m1, d1), CT_uint64 (m2, d2) -> m1 = m2 && d1 = d2 - | CT_int, CT_int -> true + | CT_bit, CT_bit -> true | CT_int64, CT_int64 -> true | CT_unit, CT_unit -> true | CT_bool, CT_bool -> true @@ -606,7 +571,7 @@ let rec string_of_ctyp = function | CT_uint64 (n, true) -> "uint64_t<" ^ string_of_int n ^ ", dec>" | CT_uint64 (n, false) -> "uint64_t<" ^ string_of_int n ^ ", int>" | CT_int64 -> "int64_t" - | CT_int -> "int" + | CT_bit -> "bit" | CT_unit -> "unit" | CT_bool -> "bool" | CT_real -> "real" @@ -618,7 +583,7 @@ let rec string_of_ctyp = function let rec ctyp_of_typ ctx typ = let Typ_aux (typ_aux, l) as typ = Env.expand_synonyms ctx.tc_env typ in match typ_aux with - | Typ_id id when string_of_id id = "bit" -> CT_int + | Typ_id id when string_of_id id = "bit" -> CT_bit | Typ_id id when string_of_id id = "bool" -> CT_bool | Typ_id id when string_of_id id = "int" -> CT_mpz | Typ_app (id, _) when string_of_id id = "range" || string_of_id id = "atom" -> @@ -646,9 +611,9 @@ let rec ctyp_of_typ ctx typ = | Typ_id id when string_of_id id = "string" -> CT_string | Typ_id id when string_of_id id = "real" -> CT_real - | Typ_id id | Typ_app (id, _) when Bindings.mem id ctx.records -> CT_struct (id, Bindings.find id ctx.records) - | Typ_id id | Typ_app (id, _) when Bindings.mem id ctx.variants -> CT_variant (id, Bindings.find id ctx.variants) - | Typ_id id when Bindings.mem id ctx.enums -> CT_enum (id, Bindings.find id ctx.enums) + | Typ_id id | Typ_app (id, _) when Bindings.mem id ctx.records -> CT_struct (id, Bindings.find id ctx.records |> Bindings.bindings) + | Typ_id id | Typ_app (id, _) when Bindings.mem id ctx.variants -> CT_variant (id, Bindings.find id ctx.variants |> Bindings.bindings) + | Typ_id id when Bindings.mem id ctx.enums -> CT_enum (id, Bindings.find id ctx.enums |> IdSet.elements) | Typ_tup typs -> CT_tup (List.map (ctyp_of_typ ctx) typs) @@ -657,14 +622,16 @@ let rec ctyp_of_typ ctx typ = | _ -> c_error ~loc:l ("No C-type for type " ^ string_of_typ typ) let rec is_stack_ctyp ctyp = match ctyp with - | CT_uint64 _ | CT_int64 | CT_int | CT_unit | CT_bool | CT_enum _ -> true + | CT_uint64 _ | CT_int64 | CT_bit | CT_unit | CT_bool | CT_enum _ -> true | CT_bv _ | CT_mpz | CT_real | CT_string -> false - | CT_struct (_, fields) -> Bindings.for_all (fun _ ctyp -> is_stack_ctyp ctyp) fields - | CT_variant (_, ctors) -> Bindings.for_all (fun _ ctyp -> is_stack_ctyp ctyp) ctors + | CT_struct (_, fields) -> List.for_all (fun (_, ctyp) -> is_stack_ctyp ctyp) fields + | CT_variant (_, ctors) -> List.for_all (fun (_, ctyp) -> is_stack_ctyp ctyp) ctors | CT_tup ctyps -> List.for_all is_stack_ctyp ctyps let is_stack_typ ctx typ = is_stack_ctyp (ctyp_of_typ ctx typ) +let ctor_bindings = List.fold_left (fun map (id, ctyp) -> Bindings.add id ctyp map) Bindings.empty + (**************************************************************************) (* 3. Optimization of primitives and literals *) (**************************************************************************) @@ -807,9 +774,10 @@ let analyze_primop ctx id args typ = (* 4. Conversion to low-level AST *) (**************************************************************************) -(** We now define a low-level AST 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. +(** 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 @@ -828,65 +796,69 @@ let analyze_primop ctx id args typ = expression), cleanup instructions (to deallocate that memory) and possibly typing information about what has been translated. **) -type ctype_def = - | CTD_enum of id * IdSet.t - | CTD_record of id * ctyp Bindings.t - | CTD_variant of id * ctyp Bindings.t +let instr_counter = ref 0 + +let instr_number () = + let n = !instr_counter in + incr instr_counter; + n + +let idecl ?loc:(l=Parse_ast.Unknown) ctyp id = + I_aux (I_decl (ctyp, id), (instr_number (), l)) +let ialloc ?loc:(l=Parse_ast.Unknown) ctyp id = + I_aux (I_alloc (ctyp, id), (instr_number (), l)) +let iinit ?loc:(l=Parse_ast.Unknown) ctyp id cval = + I_aux (I_init (ctyp, id, cval), (instr_number (), l)) +let iif ?loc:(l=Parse_ast.Unknown) cval then_instrs else_instrs ctyp = + I_aux (I_if (cval, then_instrs, else_instrs, ctyp), (instr_number (), l)) +let ifuncall ?loc:(l=Parse_ast.Unknown) clexp id cvals ctyp = + I_aux (I_funcall (clexp, id, cvals, ctyp), (instr_number (), l)) +let icopy ?loc:(l=Parse_ast.Unknown) clexp cval = + I_aux (I_copy (clexp, cval), (instr_number (), l)) +let iconvert ?loc:(l=Parse_ast.Unknown) clexp ctyp1 id ctyp2 = + I_aux (I_convert (clexp, ctyp1, id, ctyp2), (instr_number (), l)) +let iclear ?loc:(l=Parse_ast.Unknown) ctyp id = + I_aux (I_clear (ctyp, id), (instr_number (), l)) +let ireturn ?loc:(l=Parse_ast.Unknown) cval = + I_aux (I_return cval, (instr_number (), l)) +let iblock ?loc:(l=Parse_ast.Unknown) instrs = + I_aux (I_block instrs, (instr_number (), l)) +let itry_block ?loc:(l=Parse_ast.Unknown) instrs = + I_aux (I_try_block instrs, (instr_number (), l)) +let ithrow ?loc:(l=Parse_ast.Unknown) cval = + I_aux (I_throw cval, (instr_number (), l)) +let icomment ?loc:(l=Parse_ast.Unknown) str = + I_aux (I_comment str, (instr_number (), l)) +let ilabel ?loc:(l=Parse_ast.Unknown) label = + I_aux (I_label label, (instr_number (), l)) +let igoto ?loc:(l=Parse_ast.Unknown) label = + I_aux (I_goto label, (instr_number (), l)) +let imatch_failure ?loc:(l=Parse_ast.Unknown) () = + I_aux (I_match_failure, (instr_number (), l)) +let iraw ?loc:(l=Parse_ast.Unknown) str = + I_aux (I_raw str, (instr_number (), l)) let ctype_def_ctyps = function | CTD_enum _ -> [] - | CTD_record (_, fields) -> List.map snd (Bindings.bindings fields) - | CTD_variant (_, ctors) -> List.map snd (Bindings.bindings ctors) - -type cval = - | CV_id of id * ctyp - | CV_C_fragment of fragment * ctyp - -let cval_ctyp = function - | CV_id (_, ctyp) -> ctyp - | CV_C_fragment (_, ctyp) -> ctyp - -type clexp = - | CL_id of id - | CL_field of id * id - | CL_addr of clexp - | CL_raw of string - -type instr = - | I_decl of ctyp * id - | I_alloc of ctyp * id - | I_init of ctyp * id * cval - | I_if of cval * instr list * instr list * ctyp - | I_funcall of clexp * id * cval list * ctyp - | I_convert of clexp * ctyp * id * ctyp - | I_assign of id * cval - | I_copy of clexp * cval - | I_clear of ctyp * id - | I_throw of cval - | I_return of cval - | I_block of instr list - | I_try_block of instr list - | I_comment of string - | I_label of string - | I_goto of string - | I_raw of string - -let rec map_instrs f instr = + | CTD_struct (_, fields) -> List.map snd fields + | CTD_variant (_, ctors) -> List.map snd ctors + +let cval_ctyp = function (_, ctyp) -> ctyp + +let rec map_instrs f (I_aux (instr, aux)) = + let instr = match instr with + | I_decl _ | I_alloc _ | I_init _ -> instr + | I_if (cval, instrs1, instrs2, ctyp) -> + I_if (cval, f (List.map (map_instrs f) instrs1), f (List.map (map_instrs f) instrs2), ctyp) + | I_funcall _ | I_convert _ | I_copy _ | I_clear _ | 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 -> instr + in + I_aux (instr, aux) + +let rec instr_ctyps (I_aux (instr, aux)) = match instr with - | I_decl _ | I_alloc _ | I_init _ -> instr - | I_if (cval, instrs1, instrs2, ctyp) -> - I_if (cval, f (List.map (map_instrs f) instrs1), f (List.map (map_instrs f) instrs2), ctyp) - | I_funcall _ | I_convert _ | I_assign _ | I_copy _ | I_clear _ | 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 _ -> instr - -type cdef = - | CDEF_reg_dec of ctyp * id - | CDEF_fundef of id * id option * id list * instr list - | CDEF_type of ctype_def - -let rec instr_ctyps = function | I_decl (ctyp, _) | I_alloc (ctyp, _) | I_clear (ctyp, _) -> [ctyp] | I_init (ctyp, _, cval) -> [ctyp; cval_ctyp cval] | I_if (cval, instrs1, instrs2, ctyp) -> @@ -894,13 +866,13 @@ let rec instr_ctyps = function | I_funcall (_, _, cvals, ctyp) -> ctyp :: List.map cval_ctyp cvals | I_convert (_, ctyp1, _, ctyp2) -> [ctyp1; ctyp2] - | I_assign (_, cval) | I_copy (_, cval) -> [cval_ctyp cval] + | I_copy (_, cval) -> [cval_ctyp cval] | I_block instrs | I_try_block instrs -> List.concat (List.map instr_ctyps instrs) | I_throw cval | I_return cval -> [cval_ctyp cval] - | I_comment _ | I_label _ | I_goto _ | I_raw _ -> [] + | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_match_failure -> [] let cdef_ctyps = function - | CDEF_reg_dec (ctyp, _) -> [ctyp] + | CDEF_reg_dec (_, ctyp) -> [ctyp] | CDEF_fundef (_, _, _, instrs) -> List.concat (List.map instr_ctyps instrs) | CDEF_type tdef -> ctype_def_ctyps tdef @@ -912,17 +884,17 @@ let pp_ctyp ctyp = let pp_keyword str = string ((str |> Util.red |> Util.clear) ^ "$") -let pp_cval = function - | CV_id (id, ctyp) -> parens (pp_ctyp ctyp) ^^ (pp_id id) - | CV_C_fragment (frag, ctyp) -> parens (pp_ctyp ctyp) ^^ (string (string_of_fragment frag |> Util.cyan |> Util.clear)) +let pp_cval (frag, ctyp) = parens (pp_ctyp ctyp) ^^ (string (string_of_fragment frag |> Util.cyan |> Util.clear)) let rec pp_clexp = function | CL_id id -> pp_id id - | CL_field (id, field) -> pp_id id ^^ string "." ^^ pp_id field - | CL_addr clexp -> string "*" ^^ pp_clexp clexp - | CL_raw str -> string str + | CL_field (id, field) -> pp_id id ^^ string "." ^^ string field + | CL_addr id -> string "*" ^^ pp_id id + | CL_current_exception -> string "current_exception" + | CL_have_exception -> string "have_exception" -let rec pp_instr ?short:(short=false) = function +let rec pp_instr ?short:(short=false) (I_aux (instr, aux)) = + match instr with | I_decl (ctyp, id) -> parens (pp_ctyp ctyp) ^^ space ^^ pp_id id | I_if (cval, then_instrs, else_instrs, ctyp) -> @@ -950,8 +922,6 @@ let rec pp_instr ?short:(short=false) = function separate space [ pp_clexp x; string ":="; pp_keyword "CONVERT" ^^ pp_ctyp ctyp2 ^^ parens (pp_id y); string "->"; pp_ctyp ctyp1 ] - | I_assign (id, cval) -> - separate space [pp_id id; string ":="; pp_cval cval] | I_copy (clexp, cval) -> separate space [string "let"; pp_clexp clexp; string "="; pp_cval cval] | I_clear (ctyp, id) -> @@ -966,6 +936,8 @@ let rec pp_instr ?short:(short=false) = function string (str ^ ":") | I_goto str -> pp_keyword "GOTO" ^^ string str + | I_match_failure -> + pp_keyword "MATCH_FAILURE" | I_raw str -> pp_keyword "C" ^^ string str @@ -983,33 +955,27 @@ let is_ct_tup = function let rec compile_aval ctx = function | AV_C_fragment (frag, typ) -> - [], CV_C_fragment (frag, ctyp_of_typ ctx typ), [] + [], (frag, ctyp_of_typ ctx typ), [] | AV_id (id, typ) -> - begin - match ctyp_of_typ ctx (lvar_typ typ) with - | CT_enum (_, elems) when IdSet.mem id elems -> - [], CV_C_fragment (F_id id, ctyp_of_typ ctx (lvar_typ typ)), [] - | _ -> - [], CV_id (id, ctyp_of_typ ctx (lvar_typ typ)), [] - end + [], (F_id id, ctyp_of_typ ctx (lvar_typ typ)), [] | AV_lit (L_aux (L_string str, _), typ) -> - [], CV_C_fragment (F_lit ("\"" ^ str ^ "\""), ctyp_of_typ ctx typ), [] + [], (F_lit ("\"" ^ str ^ "\""), ctyp_of_typ ctx typ), [] | AV_lit (L_aux (L_num n, _), typ) when Big_int.less_equal min_int64 n && Big_int.less_equal n max_int64 -> let gs = gensym () in - [I_decl (CT_mpz, gs); - I_init (CT_mpz, gs, CV_C_fragment (F_lit (Big_int.to_string n ^ "L"), CT_int64))], - CV_id (gs, CT_mpz), - [I_clear (CT_mpz, gs)] + [idecl CT_mpz gs; + iinit CT_mpz gs (F_lit (Big_int.to_string n ^ "L"), CT_int64)], + (F_id gs, CT_mpz), + [iclear CT_mpz gs] | AV_lit (L_aux (L_num n, _), typ) -> let gs = gensym () in - [ I_decl (CT_mpz, gs); - I_init (CT_mpz, gs, CV_C_fragment (F_lit ("\"" ^ Big_int.to_string n ^ "\""), CT_string)) ], - CV_id (gs, CT_mpz), - [I_clear (CT_mpz, gs)] + [idecl CT_mpz gs; + iinit CT_mpz gs (F_lit ("\"" ^ Big_int.to_string n ^ "\""), CT_string)], + (F_id gs, CT_mpz), + [iclear CT_mpz gs] | AV_tuple avals -> let elements = List.map (compile_aval ctx) avals in @@ -1019,9 +985,9 @@ let rec compile_aval ctx = function let tup_ctyp = CT_tup (List.map cval_ctyp cvals) in let gs = gensym () in setup - @ [I_decl (tup_ctyp, gs)] - @ List.mapi (fun n cval -> I_copy (CL_field (gs, mk_id ("tup" ^ string_of_int n)), cval)) cvals, - CV_id (gs, CT_tup (List.map cval_ctyp cvals)), + @ [idecl tup_ctyp gs] + @ List.mapi (fun n cval -> icopy (CL_field (gs, "tup" ^ string_of_int n)) cval) cvals, + (F_id gs, CT_tup (List.map cval_ctyp cvals)), cleanup let compile_funcall ctx id args typ = @@ -1054,10 +1020,10 @@ let compile_funcall ctx id args typ = cval else if is_stack_ctyp have_ctyp && not (is_stack_ctyp ctyp) then let gs = gensym () in - setup := I_decl (ctyp, gs) :: !setup; - setup := I_init (ctyp, gs, cval) :: !setup; - cleanup := I_clear (ctyp, gs) :: !cleanup; - CV_id (gs, ctyp) + setup := idecl ctyp gs :: !setup; + setup := iinit ctyp gs cval :: !setup; + cleanup := iclear ctyp gs :: !cleanup; + (F_id gs, ctyp) else c_error ~loc:(id_loc id) (Printf.sprintf "Failure when setting up function arguments: %s and %s." (string_of_ctyp have_ctyp) (string_of_ctyp ctyp)) @@ -1067,13 +1033,13 @@ let compile_funcall ctx id args typ = let call = if ctyp_equal final_ctyp ret_ctyp then - fun ret -> I_funcall (ret, id, sargs, ret_ctyp) + fun ret -> ifuncall ret id sargs ret_ctyp else if not (is_stack_ctyp ret_ctyp) && is_stack_ctyp final_ctyp then let gs = gensym () in - setup := I_alloc (ret_ctyp, gs) :: !setup; - setup := I_funcall (CL_id gs, id, sargs, ret_ctyp) :: !setup; - cleanup := I_clear (ret_ctyp, gs) :: !cleanup; - fun ret -> I_convert (ret, final_ctyp, gs, ret_ctyp) + setup := ialloc ret_ctyp gs :: !setup; + setup := ifuncall (CL_id gs) id sargs ret_ctyp :: !setup; + cleanup := iclear ret_ctyp gs :: !cleanup; + fun ret -> iconvert ret final_ctyp gs ret_ctyp else assert false in @@ -1082,40 +1048,21 @@ let compile_funcall ctx id args typ = let rec compile_match ctx apat cval case_label = match apat, cval with - | AP_id pid, _ when is_ct_variant (cval_ctyp cval) -> - let frag = match cval with - | CV_id (id, _) -> F_id id - | CV_C_fragment (frag, _) -> frag - in - [I_if (CV_C_fragment (F_op (F_field (frag, "kind"), "!=", F_lit ("Kind_" ^ Util.zencode_string (string_of_id pid))), CT_bool), - [I_goto case_label], - [], - CT_unit)], + | AP_id pid, (frag, ctyp) when is_ct_variant ctyp -> + [iif (F_op (F_field (frag, "kind"), "!=", F_lit ("Kind_" ^ Util.zencode_string (string_of_id pid))), CT_bool) + [igoto case_label] + [] + CT_unit], [] - | AP_id pid, CV_C_fragment (code, ctyp) when is_ct_enum ctyp -> - [I_if (CV_C_fragment (F_op (F_id pid, "!=", code), CT_bool), [I_goto case_label], [], CT_unit)], [] - | AP_id pid, CV_id (id, ctyp) when is_ct_enum ctyp -> - [I_if (CV_C_fragment (F_op (F_id pid, "!=", F_id id), CT_bool), [I_goto case_label], [], CT_unit)], [] + | AP_id pid, (frag, ctyp) when is_ct_enum ctyp -> + [iif (F_op (F_id pid, "!=", frag), CT_bool) [igoto case_label] [] CT_unit], [] | AP_id pid, _ -> let ctyp = cval_ctyp cval in - let init, cleanup = if is_stack_ctyp ctyp then I_decl (ctyp, pid), [] else I_alloc (ctyp, pid), [I_clear (ctyp, pid)] in - [init; I_copy (CL_id pid, cval)], cleanup - | AP_tup apats, CV_id (id, ctyp) -> - begin - let get_tup n ctyp = CV_C_fragment (F_field (F_id id, "ztup" ^ string_of_int n), ctyp) in - let fold (instrs, cleanup, n) apat ctyp = - let instrs', cleanup' = compile_match ctx apat (get_tup n ctyp) case_label in - instrs @ instrs', cleanup' @ cleanup, n + 1 - in - match ctyp with - | CT_tup ctyps -> - let instrs, cleanup, _ = List.fold_left2 fold ([], [], 0) apats ctyps in - instrs, cleanup - | _ -> assert false - end - | AP_tup apats, CV_C_fragment (frag, ctyp) -> + let init, cleanup = if is_stack_ctyp ctyp then idecl ctyp pid, [] else ialloc ctyp pid, [iclear ctyp pid] in + [init; icopy (CL_id pid) cval], cleanup + | AP_tup apats, (frag, ctyp) -> begin - let get_tup n ctyp = CV_C_fragment (F_field (frag, "ztup" ^ string_of_int n), ctyp) in + let get_tup n ctyp = (F_field (frag, "ztup" ^ string_of_int n), ctyp) in let fold (instrs, cleanup, n) apat ctyp = let instrs', cleanup' = compile_match ctx apat (get_tup n ctyp) case_label in instrs @ instrs', cleanup' @ cleanup, n + 1 @@ -1126,37 +1073,23 @@ let rec compile_match ctx apat cval case_label = instrs, cleanup | _ -> assert false end - | AP_app (ctor, apat), CV_id (id, ctyp) -> - begin match ctyp with - | CT_variant (_, ctors) -> - let ctor_c_id = Util.zencode_string (string_of_id ctor) in - let ctor_ctyp = Bindings.find ctor ctors in - let instrs, cleanup = compile_match ctx apat (CV_C_fragment (F_field (F_id id, ctor_c_id), ctor_ctyp)) case_label in - [ I_if (CV_C_fragment (F_op (F_field (F_id id, "kind"), "!=", F_lit ("Kind_" ^ ctor_c_id)), CT_bool), - [I_goto case_label], - [], - CT_unit) ] - @ instrs, - cleanup - | _ -> failwith "AP_app constructor with non-variant type" - end - | AP_app (ctor, apat), CV_C_fragment (frag, ctyp) -> + | AP_app (ctor, apat), (frag, ctyp) -> begin match ctyp with | CT_variant (_, ctors) -> let ctor_c_id = Util.zencode_string (string_of_id ctor) in - let ctor_ctyp = Bindings.find ctor ctors in - let instrs, cleanup = compile_match ctx apat (CV_C_fragment (F_field (frag, ctor_c_id), ctor_ctyp)) case_label in - [ I_if (CV_C_fragment (F_op (F_field (frag, "kind"), "!=", F_lit ("Kind_" ^ ctor_c_id)), CT_bool), - [I_goto case_label], - [], - CT_unit) ] + let ctor_ctyp = Bindings.find ctor (ctor_bindings ctors) in + let instrs, cleanup = compile_match ctx apat ((F_field (frag, ctor_c_id), ctor_ctyp)) case_label in + [iif (F_op (F_field (frag, "kind"), "!=", F_lit ("Kind_" ^ ctor_c_id)), CT_bool) + [igoto case_label] + [] + CT_unit] @ instrs, cleanup | _ -> failwith "AP_app constructor with non-variant type" end | AP_wild, _ -> [], [] -let unit_fragment = CV_C_fragment (F_lit "UNIT", CT_unit) +let unit_fragment = (F_lit "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 @@ -1173,9 +1106,9 @@ let rec compile_aexp ctx = function let setup, ctyp, call, cleanup = compile_aexp ctx binding in let letb1, letb1c = if is_stack_ctyp ctyp then - [I_decl (ctyp, id); call (CL_id id)], [] + [idecl ctyp id; call (CL_id id)], [] else - [I_alloc (ctyp, id); call (CL_id id)], [I_clear (ctyp, id)] + [ialloc ctyp id; call (CL_id id)], [iclear ctyp id] in let letb2 = setup @ letb1 @ cleanup in let setup, ctyp, call, cleanup = compile_aexp ctx body in @@ -1186,7 +1119,7 @@ let rec compile_aexp ctx = function | AE_val aval -> let setup, cval, cleanup = compile_aval ctx aval in - setup, cval_ctyp cval, (fun clexp -> I_copy (clexp, cval)), cleanup + setup, cval_ctyp cval, (fun clexp -> icopy clexp cval), cleanup (* Compile case statements *) | AE_case (aval, cases, typ) -> @@ -1206,26 +1139,26 @@ let rec compile_aexp ctx = function let body_setup, _, body_call, body_cleanup = compile_aexp ctx body in let gs = gensym () in let case_instrs = - destructure @ [I_comment "end destructuring"] + destructure @ [icomment "end destructuring"] @ (if not trivial_guard then - guard_setup @ [I_decl (CT_bool, gs); guard_call (CL_id gs)] @ guard_cleanup - @ [I_if (CV_C_fragment (F_unary ("!", F_id gs), CT_bool), destructure_cleanup @ [I_goto case_label], [], CT_unit)] - @ [I_comment "end guard"] + guard_setup @ [idecl CT_bool gs; guard_call (CL_id gs)] @ 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)] @ body_cleanup @ destructure_cleanup - @ [I_goto finish_match_label] + @ [igoto finish_match_label] in - [I_block case_instrs; I_label case_label] + [iblock case_instrs; ilabel case_label] in - [I_comment "begin match"] - @ aval_setup @ [I_decl (ctyp, case_return_id)] + [icomment "begin match"] + @ aval_setup @ [idecl ctyp case_return_id] @ List.concat (List.map compile_case cases) - @ [I_raw "sail_match_failure();"] - @ [I_label finish_match_label], + @ [imatch_failure ()] + @ [ilabel finish_match_label], ctyp, - (fun clexp -> I_copy (clexp, CV_id (case_return_id, ctyp))), + (fun clexp -> icopy clexp (F_id case_return_id, ctyp)), aval_cleanup - @ [I_comment "end match"] + @ [icomment "end match"] (* Compile try statement *) | AE_try (aexp, cases, typ) -> @@ -1239,32 +1172,32 @@ let rec compile_aexp ctx = function | _ -> false in let try_label = label "try_" in - let exn_cval = CV_C_fragment (F_lit "(*current_exception)", ctyp_of_typ ctx (mk_typ (Typ_id (mk_id "exception")))) in + let exn_cval = (F_current_exception, ctyp_of_typ ctx (mk_typ (Typ_id (mk_id "exception")))) in let destructure, destructure_cleanup = 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 @ [I_comment "end destructuring"] + destructure @ [icomment "end destructuring"] @ (if not trivial_guard then - guard_setup @ [I_decl (CT_bool, gs); guard_call (CL_id gs)] @ guard_cleanup - @ [I_if (CV_C_fragment (F_unary ("!", F_id gs), CT_bool), [I_goto try_label], [], CT_unit)] - @ [I_comment "end guard"] + guard_setup @ [idecl CT_bool gs; guard_call (CL_id gs)] @ guard_cleanup + @ [iif (F_unary ("!", F_id gs), CT_bool) [igoto try_label] [] CT_unit] + @ [icomment "end guard"] else []) @ body_setup @ [body_call (CL_id try_return_id)] @ body_cleanup @ destructure_cleanup - @ [I_goto handled_exception_label] + @ [igoto handled_exception_label] in - [I_block case_instrs; I_label try_label] + [iblock case_instrs; ilabel try_label] in - [I_comment "begin try catch"; - I_decl (ctyp, try_return_id)], + [icomment "begin try catch"; + idecl ctyp try_return_id], ctyp, - (fun clexp -> I_try_block (aexp_setup @ [aexp_call clexp] @ aexp_cleanup)), - [I_if (CV_C_fragment (F_lit "!have_exception", CT_bool), [I_goto handled_exception_label], [], CT_unit)] + (fun clexp -> itry_block (aexp_setup @ [aexp_call clexp] @ aexp_cleanup)), + [iif (F_unary ("!", F_have_exception), CT_bool) [igoto handled_exception_label] [] CT_unit] @ List.concat (List.map compile_case cases) - @ [I_raw "sail_match_failure();"] - @ [I_label handled_exception_label] - @ [I_raw "have_exception = false;"] + @ [imatch_failure ()] + @ [ilabel handled_exception_label] + @ [icopy CL_have_exception (F_lit "false", CT_bool)] | AE_if (aval, then_aexp, else_aexp, if_typ) -> let if_ctyp = ctyp_of_typ ctx if_typ in @@ -1274,12 +1207,12 @@ let rec compile_aexp ctx = function in let setup, ctyp, call, cleanup = compile_aexp ctx (AE_val aval) in let gs = gensym () in - setup @ [I_decl (ctyp, gs); call (CL_id gs)], + setup @ [idecl ctyp gs; call (CL_id gs)], if_ctyp, - (fun clexp -> I_if (CV_id (gs, ctyp), - compile_branch then_aexp clexp, - compile_branch else_aexp clexp, - if_ctyp)), + (fun clexp -> iif (F_id gs, ctyp) + (compile_branch then_aexp clexp) + (compile_branch else_aexp clexp) + if_ctyp), cleanup | AE_record_update (aval, fields, typ) -> @@ -1290,10 +1223,10 @@ let rec compile_aexp ctx = function let setup, calls, cleanup = List.fold_left update_field ([], [], []) (Bindings.bindings fields) in let ctyp = ctyp_of_typ ctx typ in let gs = gensym () in - [I_alloc (ctyp, gs)] @ setup @ List.map (fun call -> call (CL_id gs)) calls, + [ialloc ctyp gs] @ setup @ List.map (fun call -> call (CL_id gs)) calls, ctyp, - (fun clexp -> I_copy (clexp, CV_id (gs, ctyp))), - cleanup @ [I_clear (ctyp, gs)] + (fun clexp -> icopy clexp (F_id gs, ctyp)), + cleanup @ [iclear ctyp gs] | AE_assign (id, assign_typ, aexp) -> (* assign_ctyp is the type of the C variable we are assigning to, @@ -1303,16 +1236,16 @@ let rec compile_aexp ctx = function let setup, ctyp, call, cleanup = compile_aexp ctx aexp in let comment = "assign " ^ string_of_ctyp assign_ctyp ^ " := " ^ string_of_ctyp ctyp in if ctyp_equal assign_ctyp ctyp then - setup @ [call (CL_id id)], CT_unit, (fun clexp -> I_copy (clexp, unit_fragment)), cleanup + setup @ [call (CL_id id)], CT_unit, (fun clexp -> icopy clexp unit_fragment), cleanup else if not (is_stack_ctyp assign_ctyp) && is_stack_ctyp ctyp then let gs = gensym () in - setup @ [ I_comment comment; - I_decl (ctyp, gs); + setup @ [ icomment comment; + idecl ctyp gs; call (CL_id gs); - I_convert (CL_id id, assign_ctyp, gs, ctyp) + iconvert (CL_id id) assign_ctyp gs ctyp ], CT_unit, - (fun clexp -> I_copy (clexp, unit_fragment)), + (fun clexp -> icopy clexp unit_fragment), cleanup else failwith comment @@ -1329,17 +1262,17 @@ let rec compile_aexp ctx = function let body_setup, _, body_call, body_cleanup = compile_aexp ctx body in let gs = gensym () in let unit_gs = gensym () in - let loop_test = CV_C_fragment (F_unary ("!", F_id gs), CT_bool) in - cond_setup @ [I_decl (CT_bool, gs); I_decl (CT_unit, unit_gs)] - @ [I_label loop_start_label] - @ [I_block ([cond_call (CL_id gs); I_if (loop_test, [I_goto loop_end_label], [], CT_unit)] - @ body_setup - @ [body_call (CL_id unit_gs)] - @ body_cleanup - @ [I_goto loop_start_label])] - @ [I_label loop_end_label], + let loop_test = (F_unary ("!", F_id gs), CT_bool) in + cond_setup @ [idecl CT_bool gs; idecl CT_unit unit_gs] + @ [ilabel loop_start_label] + @ [iblock ([cond_call (CL_id gs); iif loop_test [igoto loop_end_label] [] CT_unit] + @ body_setup + @ [body_call (CL_id unit_gs)] + @ body_cleanup + @ [igoto loop_start_label])] + @ [ilabel loop_end_label], CT_unit, - (fun clexp -> I_copy (clexp, unit_fragment)), + (fun clexp -> icopy clexp unit_fragment), cond_cleanup | AE_cast (aexp, typ) -> compile_aexp ctx aexp @@ -1347,17 +1280,17 @@ let rec compile_aexp ctx = function | AE_return (aval, typ) -> (* Cleanup info will be re-added by fix_early_return *) let return_setup, cval, _ = compile_aval ctx aval in - return_setup @ [I_return cval], + return_setup @ [ireturn cval], CT_unit, - (fun clexp -> I_copy (clexp, unit_fragment)), + (fun clexp -> icopy clexp unit_fragment), [] | AE_throw (aval, typ) -> (* Cleanup info will be handled by fix_exceptions *) let throw_setup, cval, _ = compile_aval ctx aval in - throw_setup @ [I_throw cval], + throw_setup @ [ithrow cval], ctyp_of_typ ctx typ, - (fun clexp -> I_copy (clexp, unit_fragment)), + (fun clexp -> icopy clexp unit_fragment), [] | aexp -> failwith ("Cannot compile ANF expression: " ^ Pretty_print_sail.to_string (pp_aexp aexp)) @@ -1368,7 +1301,7 @@ and compile_block ctx = function let setup, _, call, cleanup = compile_aexp ctx exp in let rest = compile_block ctx exps in let gs = gensym () in - setup @ [I_decl (CT_unit, gs); call (CL_id gs)] @ cleanup @ rest + setup @ [idecl CT_unit gs; call (CL_id gs)] @ cleanup @ rest let rec pat_ids (P_aux (p_aux, (l, _)) as pat) = match p_aux with @@ -1389,12 +1322,12 @@ let rec pat_ids (P_aux (p_aux, (l, _)) as pat) = let compile_type_def ctx (TD_aux (type_def, _)) = match type_def with | TD_enum (id, _, ids, _) -> - CTD_enum (id, IdSet.of_list 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_record (id, ctors), + CTD_struct (id, Bindings.bindings ctors), { ctx with records = Bindings.add id ctors ctx.records } | TD_variant (id, _, _, tus, _) -> @@ -1404,7 +1337,7 @@ let compile_type_def ctx (TD_aux (type_def, _)) = | Tu_ty_id (typ, id) -> 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, ctus), + CTD_variant (id, Bindings.bindings ctus), { ctx with variants = Bindings.add id ctus ctx.variants } (* Will be re-written before here, see bitfield.ml *) @@ -1421,13 +1354,14 @@ let instr_split_at f = instr_split_at' f [] let generate_cleanup instrs = - let generate_cleanup' = function - | I_decl (ctyp, id) when not (is_stack_ctyp ctyp) -> [(id, I_clear (ctyp, id))] - | I_alloc (ctyp, id) when not (is_stack_ctyp ctyp) -> [(id, I_clear (ctyp, id))] + let generate_cleanup' (I_aux (instr, _)) = + match instr with + | I_decl (ctyp, id) when not (is_stack_ctyp ctyp) -> [(id, iclear ctyp id)] + | I_alloc (ctyp, id) when not (is_stack_ctyp ctyp) -> [(id, iclear ctyp id)] | instr -> [] in let is_clear ids = function - | I_clear (_, id) -> IdSet.add id ids + | I_aux (I_clear (_, id), _) -> IdSet.add id ids | _ -> ids in let cleaned = List.fold_left is_clear IdSet.empty instrs in @@ -1450,67 +1384,73 @@ let generate_cleanup instrs = same block? *) let fix_early_return ret ctx instrs = let end_function_label = label "end_function_" in - let is_return_recur = function + let is_return_recur (I_aux (instr, _)) = + match instr with | I_return _ | I_if _ | I_block _ -> true | _ -> false in let rec rewrite_return pre_cleanup instrs = match instr_split_at is_return_recur instrs with | instrs, [] -> instrs - | before, I_block instrs :: after -> + | before, I_aux (I_block instrs, _) :: after -> before - @ [I_block (rewrite_return (pre_cleanup @ generate_cleanup before) instrs)] + @ [iblock (rewrite_return (pre_cleanup @ generate_cleanup before) instrs)] @ rewrite_return pre_cleanup after - | before, I_if (cval, then_instrs, else_instrs, ctyp) :: after -> + | before, I_aux (I_if (cval, then_instrs, else_instrs, ctyp), _) :: after -> let cleanup = pre_cleanup @ generate_cleanup before in before - @ [I_if (cval, rewrite_return cleanup then_instrs, rewrite_return cleanup else_instrs, ctyp)] + @ [iif cval (rewrite_return cleanup then_instrs) (rewrite_return cleanup else_instrs) ctyp] @ rewrite_return pre_cleanup after - | before, I_return cval :: after -> + | before, I_aux (I_return cval, _) :: after -> let cleanup_label = label "cleanup_" in let end_cleanup_label = label "end_cleanup_" in before - @ [I_copy (ret, cval); - I_goto cleanup_label] + @ [icopy 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 pre_cleanup after - @ [I_goto end_cleanup_label] - @ [I_label cleanup_label] + @ [igoto end_cleanup_label] + @ [ilabel cleanup_label] @ pre_cleanup @ generate_cleanup before - @ [I_goto end_function_label] - @ [I_label end_cleanup_label] + @ [igoto end_function_label] + @ [ilabel end_cleanup_label] | _, _ -> assert false in rewrite_return [] instrs - @ [I_label end_function_label] + @ [ilabel end_function_label] let fix_exception_block ctx instrs = let end_block_label = label "end_block_exception_" in - let is_exception_stop = function + 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_block instrs :: after -> + | before, I_aux (I_block instrs, _) :: after -> before - @ [I_block (rewrite_exception (generate_cleanup (historic @ before)) instrs)] + @ [iblock (rewrite_exception (generate_cleanup (historic @ before)) instrs)] @ rewrite_exception (historic @ before) after - | before, I_if (cval, then_instrs, else_instrs, ctyp) :: after -> + | before, I_aux (I_if (cval, then_instrs, else_instrs, ctyp), _) :: after -> let historic = historic @ before in before - @ [I_if (cval, rewrite_exception historic then_instrs, rewrite_exception historic else_instrs, ctyp)] + @ [iif cval (rewrite_exception historic then_instrs) (rewrite_exception historic else_instrs) ctyp] @ rewrite_exception historic after - | before, I_throw cval :: after -> + | before, I_aux (I_throw cval, _) :: after -> before - @ [I_copy (CL_raw "current_exception", cval); - I_raw "have_exception = true;"] + @ [icopy CL_current_exception cval; + icopy CL_have_exception (F_lit "true", CT_bool)] @ generate_cleanup (historic @ before) - @ [I_goto end_block_label] + @ [igoto end_block_label] @ rewrite_exception (historic @ before) after - | before, (I_funcall (x, f, args, ctyp) as funcall) :: after -> + | before, (I_aux (I_funcall (x, f, args, ctyp), _) 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 *) @@ -1519,24 +1459,26 @@ let fix_exception_block ctx instrs = if has_effect effects BE_escape then before @ [funcall; - I_if (CV_C_fragment (F_lit "have_exception", CT_bool), generate_cleanup (historic @ before) @ [I_goto end_block_label], [], CT_unit)] + 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 rewrite_exception [] instrs - @ [I_label end_block_label] - -let rec map_try_block f instr = - match instr with - | I_decl _ | I_alloc _ | I_init _ -> 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_convert _ | I_assign _ | I_copy _ | 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 _ -> instr + @ [ilabel end_block_label] + +let rec map_try_block f (I_aux (instr, aux)) = + let instr = match instr with + | I_decl _ | I_alloc _ | I_init _ -> 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_convert _ | I_copy _ | 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_match_failure -> instr + in + I_aux (instr, aux) let fix_exception ctx instrs = let instrs = List.map (map_try_block (fix_exception_block ctx)) instrs in @@ -1545,7 +1487,7 @@ let fix_exception ctx instrs = (** Compile a Sail toplevel definition into an IR definition **) let compile_def ctx = function | DEF_reg_dec (DEC_aux (DEC_reg (typ, id), _)) -> - [CDEF_reg_dec (ctyp_of_typ ctx typ, id)], ctx + [CDEF_reg_dec (id, ctyp_of_typ ctx typ)], ctx | DEF_reg_dec _ -> failwith "Unsupported register declaration" (* FIXME *) | DEF_spec _ -> [], ctx @@ -1559,12 +1501,12 @@ let compile_def ctx = function let setup, ctyp, call, cleanup = compile_aexp ctx aexp in let gs = gensym () in if is_stack_ctyp ctyp then - let instrs = [I_decl (ctyp, gs)] @ setup @ [call (CL_id gs)] @ cleanup @ [I_return (CV_id (gs, ctyp))] in + let instrs = [idecl ctyp gs] @ setup @ [call (CL_id gs)] @ cleanup @ [ireturn (F_id gs, ctyp)] in let instrs = fix_exception ctx instrs in [CDEF_fundef (id, None, pat_ids pat, instrs)], ctx else - let instrs = setup @ [call (CL_addr (CL_id gs))] @ cleanup in - let instrs = fix_early_return (CL_addr (CL_id gs)) ctx instrs in + let instrs = setup @ [call (CL_addr gs)] @ cleanup in + let instrs = fix_early_return (CL_addr gs) ctx instrs in let instrs = fix_exception ctx instrs in [CDEF_fundef (id, Some gs, pat_ids pat, instrs)], ctx | _ -> assert false @@ -1599,20 +1541,21 @@ let compile_def ctx = function See https://gcc.gnu.org/onlinedocs/gcc/Local-Labels.html **) let add_local_labels' instrs = - let is_label = function + let is_label (I_aux (instr, _)) = + match instr with | I_label str -> [str] | _ -> [] in let labels = List.concat (List.map is_label instrs) in - let local_label_decl = I_raw ("__label__ " ^ String.concat ", " labels ^ ";\n") in + let local_label_decl = iraw ("__label__ " ^ String.concat ", " labels ^ ";\n") in if labels = [] then instrs else local_label_decl :: instrs let add_local_labels instrs = - match map_instrs add_local_labels' (I_block instrs) with - | I_block instrs -> instrs + match map_instrs add_local_labels' (iblock instrs) with + | I_aux (I_block instrs, _) -> instrs | _ -> assert false (**************************************************************************) @@ -1642,8 +1585,8 @@ module Node = struct | _ , G_start -> -1 | G_instr _, _ -> 1 | _ , G_instr _ -> -1 - | _ , G_id _ -> 1 - | G_id _ , _ -> -1 + | G_id _ , _ -> 1 + | _ , G_id _ -> -1 end module NM = Map.Make(Node) @@ -1656,16 +1599,17 @@ let rec fragment_deps = function | F_lit _ -> NS.empty | F_field (frag, _) | F_unary (_, frag) -> fragment_deps frag | F_op (frag1, _, frag2) -> NS.union (fragment_deps frag1) (fragment_deps frag2) + | F_current_exception -> NS.empty + | F_have_exception -> NS.empty -let cval_deps = function - | CV_id (id, _) -> NS.singleton (G_id id) - | CV_C_fragment (frag, _) -> fragment_deps frag +let cval_deps = function (frag, _) -> fragment_deps frag let rec clexp_deps = function | CL_id id -> NS.singleton (G_id id) | CL_field (id, _) -> NS.singleton (G_id id) - | CL_addr clexp -> clexp_deps clexp - | CL_raw _ -> NS.empty + | CL_addr id -> NS.singleton (G_id id) + | CL_have_exception -> NS.empty + | CL_current_exception -> NS.empty (** Return the direct, non program-order dependencies of a single instruction **) @@ -1676,7 +1620,6 @@ let instr_deps = function | I_if (cval, _, _, _) -> cval_deps cval, NS.empty | I_funcall (clexp, _, cvals, _) -> List.fold_left NS.union NS.empty (List.map cval_deps cvals), clexp_deps clexp | I_convert (clexp, _, id, _) -> NS.singleton (G_id id), clexp_deps clexp - | I_assign (id, cval) -> cval_deps cval, NS.singleton (G_id id) | I_copy (clexp, cval) -> cval_deps cval, clexp_deps clexp | I_clear (_, id) -> NS.singleton (G_id id), NS.singleton (G_id id) | I_throw cval | I_return cval -> cval_deps cval, NS.empty @@ -1684,6 +1627,7 @@ let instr_deps = function | I_comment _ | I_raw _ -> NS.empty, NS.empty | I_label label -> NS.singleton (G_label label), NS.empty | I_goto label -> NS.empty, NS.singleton (G_label label) + | I_match_failure -> NS.empty, NS.empty let add_link from_node to_node graph = try @@ -1704,9 +1648,9 @@ let instrs_graph instrs = let icounter = ref 0 in let graph = ref NM.empty in - let rec add_instr last_instr instr = + let rec add_instr last_instr (I_aux (instr, _) as iaux) = incr icounter; - let node = G_instr (!icounter, instr) in + let node = G_instr (!icounter, iaux) in match instr with | I_block instrs | I_try_block instrs -> List.fold_left add_instr last_instr instrs @@ -1718,7 +1662,7 @@ let instrs_graph instrs = let n1 = List.fold_left add_instr node then_instrs in let n2 = List.fold_left add_instr node else_instrs in incr icounter; - let join = G_instr (!icounter, I_comment "join") in + let join = G_instr (!icounter, icomment "join") in graph := add_link n1 join !graph; graph := add_link n2 join !graph; join @@ -1729,7 +1673,7 @@ let instrs_graph instrs = graph := add_link last_instr node !graph; NS.iter (fun output -> graph := add_link node output !graph) outputs; incr icounter; - G_instr (!icounter, I_comment "after goto") + G_instr (!icounter, icomment "after goto") end | _ -> begin @@ -1740,28 +1684,28 @@ let instrs_graph instrs = node end in - List.fold_left add_instr G_start instrs; + ignore (List.fold_left add_instr G_start instrs); fix_leaves !graph let make_dot id graph = Util.opt_colors := false; let to_string node = String.escaped (string_of_node node) in let node_color = function - | G_start _ -> "lightpink" - | G_id _ -> "yellow" - | G_instr (_, I_decl _) -> "olivedrab1" - | G_instr (_, I_init _) -> "springgreen" - | G_instr (_, I_alloc _) -> "palegreen" - | G_instr (_, I_clear _) -> "peachpuff" - | G_instr (_, I_goto _) -> "orange1" - | G_instr (_, I_label _) -> "white" - | G_instr (_, I_raw _) -> "khaki" - | G_instr _ -> "azure" - | G_label _ -> "lightpink" + | G_start -> "lightpink" + | G_id _ -> "yellow" + | G_instr (_, I_aux (I_decl _, _)) -> "olivedrab1" + | G_instr (_, I_aux (I_init _, _)) -> "springgreen" + | G_instr (_, I_aux (I_alloc _, _)) -> "palegreen" + | G_instr (_, I_aux (I_clear _, _)) -> "peachpuff" + | G_instr (_, I_aux (I_goto _, _)) -> "orange1" + | G_instr (_, I_aux (I_label _, _)) -> "white" + | G_instr (_, I_aux (I_raw _, _)) -> "khaki" + | G_instr _ -> "azure" + | G_label _ -> "lightpink" in let edge_color from_node to_node = match from_node, to_node with - | G_start _, _ -> "goldenrod4" + | G_start , _ -> "goldenrod4" | G_label _, _ -> "darkgreen" | _ , G_label _ -> "goldenrod4" | G_instr _, G_instr _ -> "black" @@ -1795,7 +1739,7 @@ let upper_codegen_id id = string (upper_sgen_id id) let sgen_ctyp = function | CT_unit -> "unit" - | CT_int -> "int" + | CT_bit -> "bit" | CT_bool -> "bool" | CT_uint64 _ -> "uint64_t" | CT_int64 -> "int64_t" @@ -1809,7 +1753,7 @@ let sgen_ctyp = function let sgen_ctyp_name = function | CT_unit -> "unit" - | CT_int -> "int" + | CT_bit -> "bit" | CT_bool -> "bool" | CT_uint64 _ -> "uint64_t" | CT_int64 -> "int64_t" @@ -1821,26 +1765,24 @@ let sgen_ctyp_name = function | CT_variant (id, _) -> sgen_id id | CT_string -> "sail_string" -let sgen_cval = function - | CV_C_fragment (frag, _) -> string_of_fragment frag - | CV_id (id, _) -> sgen_id id - | _ -> "CVAL??" +let sgen_cval = function (frag, _) -> string_of_fragment frag let sgen_clexp = function | CL_id id -> "&" ^ sgen_id id - | CL_field (id, field) -> "&(" ^ sgen_id id ^ "." ^ sgen_id field ^ ")" - | CL_addr (CL_id id) -> sgen_id id - | CL_raw str -> str - | _ -> assert false + | CL_field (id, field) -> "&(" ^ sgen_id id ^ "." ^ field ^ ")" + | CL_addr id -> sgen_id id + | CL_have_exception -> "have_exception" + | CL_current_exception -> "current_exception" let sgen_clexp_pure = function | CL_id id -> sgen_id id - | CL_field (id, field) -> sgen_id id ^ "." ^ sgen_id field - | CL_raw str -> str - | CL_addr (CL_id id) -> sgen_id id - | _ -> assert false + | CL_field (id, field) -> sgen_id id ^ "." ^ field + | CL_addr id -> sgen_id id + | CL_have_exception -> "have_exception" + | CL_current_exception -> "current_exception" -let rec codegen_instr ctx = function +let rec codegen_instr ctx (I_aux (instr, _)) = + match instr with | I_decl (ctyp, id) -> string (Printf.sprintf " %s %s;" (sgen_ctyp ctyp) (sgen_id id)) | I_copy (clexp, cval) -> @@ -1849,7 +1791,6 @@ let rec codegen_instr ctx = function string (Printf.sprintf " %s = %s;" (sgen_clexp_pure clexp) (sgen_cval cval)) else string (Printf.sprintf " set_%s(%s, %s);" (sgen_ctyp_name ctyp) (sgen_clexp clexp) (sgen_cval cval)) - | I_assign _ -> failwith "I_assign is currently unused" | I_if (cval, [then_instr], [], ctyp) -> string (Printf.sprintf " if (%s)" (sgen_cval cval)) ^^ hardline ^^ twice space ^^ codegen_instr ctx then_instr @@ -1913,13 +1854,15 @@ let rec codegen_instr ctx = function string (Printf.sprintf " goto %s;" str) | I_raw str -> string (" " ^ str) + | I_match_failure -> + string (" sail_match_failure();") let codegen_type_def ctx = function | CTD_enum (id, ids) -> string (Printf.sprintf "// enum %s" (string_of_id id)) ^^ hardline - ^^ separate space [string "enum"; codegen_id id; lbrace; separate_map (comma ^^ space) upper_codegen_id (IdSet.elements ids); rbrace ^^ semi] + ^^ separate space [string "enum"; codegen_id id; lbrace; separate_map (comma ^^ space) upper_codegen_id ids; rbrace ^^ semi] - | CTD_record (id, ctors) -> + | CTD_struct (id, ctors) -> (* Generate a set_T function for every struct T *) let codegen_set (id, ctyp) = if is_stack_ctyp ctyp then @@ -1952,14 +1895,14 @@ let codegen_type_def ctx = function string (Printf.sprintf "// struct %s" (string_of_id id)) ^^ hardline ^^ string "struct" ^^ space ^^ codegen_id id ^^ space ^^ surround 2 0 lbrace - (separate_map (semi ^^ hardline) codegen_ctor (Bindings.bindings ctors) ^^ semi) + (separate_map (semi ^^ hardline) codegen_ctor ctors ^^ semi) rbrace ^^ semi ^^ twice hardline - ^^ codegen_setter id ctors + ^^ codegen_setter id (ctor_bindings ctors) ^^ twice hardline - ^^ codegen_init "init" id ctors + ^^ codegen_init "init" id (ctor_bindings ctors) ^^ twice hardline - ^^ codegen_init "clear" id ctors + ^^ codegen_init "clear" id (ctor_bindings ctors) | CTD_variant (id, tus) -> let codegen_tu (ctor_id, ctyp) = @@ -1979,7 +1922,7 @@ let codegen_type_def ctx = function in let codegen_init = let n = sgen_id id in - let ctor_id, ctyp = List.hd (Bindings.bindings tus) in + let ctor_id, ctyp = List.hd tus in string (Printf.sprintf "void init_%s(struct %s *op)" n n) ^^ hardline ^^ surround 2 0 lbrace @@ -1999,7 +1942,7 @@ let codegen_type_def ctx = function let n = sgen_id id in string (Printf.sprintf "void clear_%s(struct %s *op)" n n) ^^ hardline ^^ surround 2 0 lbrace - (each_ctor "op->" (clear_field "op") (Bindings.bindings tus) ^^ semi) + (each_ctor "op->" (clear_field "op") tus ^^ semi) rbrace in let codegen_ctor (ctor_id, ctyp) = @@ -2021,7 +1964,7 @@ let codegen_type_def ctx = function string (Printf.sprintf "void %s(struct %s *rop, %s)" (sgen_id ctor_id) (sgen_id id) ctor_args) ^^ hardline ^^ surround 2 0 lbrace (tuple - ^^ each_ctor "rop->" (clear_field "rop") (Bindings.bindings tus) ^^ hardline + ^^ each_ctor "rop->" (clear_field "rop") tus ^^ hardline ^^ string ("rop->kind = Kind_" ^ sgen_id ctor_id) ^^ semi ^^ hardline ^^ if is_stack_ctyp ctyp then string (Printf.sprintf "rop->%s = op;" (sgen_id ctor_id)) @@ -2041,18 +1984,18 @@ let codegen_type_def ctx = function in string (Printf.sprintf "void set_%s(struct %s *rop, struct %s op)" n n n) ^^ hardline ^^ surround 2 0 lbrace - (each_ctor "rop->" (clear_field "rop") (Bindings.bindings tus) + (each_ctor "rop->" (clear_field "rop") tus ^^ semi ^^ hardline ^^ string "rop->kind = op.kind" ^^ semi ^^ hardline - ^^ each_ctor "op." set_field (Bindings.bindings tus)) + ^^ each_ctor "op." set_field tus) rbrace in string (Printf.sprintf "// union %s" (string_of_id id)) ^^ hardline ^^ string "enum" ^^ space ^^ string ("kind_" ^ sgen_id id) ^^ space ^^ separate space [ lbrace; - separate_map (comma ^^ space) (fun id -> string ("Kind_" ^ sgen_id id)) (List.map fst (Bindings.bindings tus)); + separate_map (comma ^^ space) (fun id -> string ("Kind_" ^ sgen_id id)) (List.map fst tus); rbrace ^^ semi ] ^^ twice hardline ^^ string "struct" ^^ space ^^ codegen_id id ^^ space @@ -2061,7 +2004,7 @@ let codegen_type_def ctx = function ^^ hardline ^^ string "union" ^^ space ^^ surround 2 0 lbrace - (separate_map (semi ^^ hardline) codegen_tu (Bindings.bindings tus) ^^ semi) + (separate_map (semi ^^ hardline) codegen_tu tus ^^ semi) rbrace ^^ semi) rbrace @@ -2073,7 +2016,7 @@ let codegen_type_def ctx = function ^^ twice hardline ^^ codegen_setter ^^ twice hardline - ^^ separate_map (twice hardline) codegen_ctor (Bindings.bindings tus) + ^^ separate_map (twice hardline) codegen_ctor tus (* If this is the exception type, then we setup up some global variables to deal with exceptions. *) ^^ if string_of_id id = "exception" then twice hardline @@ -2110,10 +2053,10 @@ let codegen_tup ctx ctyps = ctyps in generated_tuples := IdSet.add id !generated_tuples; - codegen_type_def ctx (CTD_record (id, fields)) ^^ twice hardline + codegen_type_def ctx (CTD_struct (id, Bindings.bindings fields)) ^^ twice hardline let codegen_def' ctx = function - | CDEF_reg_dec (ctyp, id) -> + | CDEF_reg_dec (id, ctyp) -> string (Printf.sprintf "// register %s" (string_of_id id)) ^^ hardline ^^ string (Printf.sprintf "%s %s;" (sgen_ctyp ctyp) (sgen_id id)) |