From 5dc3ee5029f6e828b7e77a176a67894e8fa00696 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Thu, 14 Jun 2018 04:49:47 +0100 Subject: Refactor C backend, and split RTS into multiple files --- src/bytecode_util.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'src/bytecode_util.ml') diff --git a/src/bytecode_util.ml b/src/bytecode_util.ml index 96513d7f..05709de9 100644 --- a/src/bytecode_util.ml +++ b/src/bytecode_util.ml @@ -161,11 +161,11 @@ and string_of_fragment' ?zencode:(zencode=true) f = (* String representation of ctyps here is only for debugging and intermediate language pretty-printer. *) let rec string_of_ctyp = function - | CT_mpz -> "mpz_t" - | CT_bv true -> "bv_t(dec)" - | CT_bv false -> "bv_t(inc)" - | CT_uint64 (n, true) -> "uint64_t(" ^ string_of_int n ^ ", dec)" - | CT_uint64 (n, false) -> "uint64_t(" ^ string_of_int n ^ ", int)" + | CT_int -> "mpz_t" + | CT_bits true -> "bv_t(dec)" + | CT_bits false -> "bv_t(inc)" + | CT_bits64 (n, true) -> "uint64_t(" ^ string_of_int n ^ ", dec)" + | CT_bits64 (n, false) -> "uint64_t(" ^ string_of_int n ^ ", int)" | CT_int64 -> "int64_t" | CT_bit -> "bit" | CT_unit -> "unit" -- cgit v1.2.3 From 5489108f054fb51aa190e1fda847d8ab59ee915b Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Wed, 20 Jun 2018 17:12:04 +0100 Subject: Simplify the ANF->IR translation Previously the ANF->IR translation cared too much about how things were allocated in C, so it had to constantly check whether things needed to be allocated on the stack or heap, and generate different cequences of IR instructions depending on either. This change removes the ialloc IR instruction, and changes iinit and idecl so that the code generator now generates different C for the same IR instructions based on the variable types involved. The next change in this vein would be to merge icopy and iconvert at the IR level so that conversions between uint64_t and large-bitvectors are inserted by the code generator. This would be good because it would make the ANF->IR translation more robust to changes in the types of variables caused by flow-typing, and optimization passes could convert large bitvectors to uint64_t as local changes. --- src/bytecode_util.ml | 11 ++--------- 1 file changed, 2 insertions(+), 9 deletions(-) (limited to 'src/bytecode_util.ml') diff --git a/src/bytecode_util.ml b/src/bytecode_util.ml index 05709de9..1a206764 100644 --- a/src/bytecode_util.ml +++ b/src/bytecode_util.ml @@ -67,9 +67,6 @@ let instr_number () = 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)) @@ -221,8 +218,6 @@ let rec pp_instr ?short:(short=false) (I_aux (instr, aux)) = surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace | I_try_block instrs -> pp_keyword "try" ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace - | I_alloc (ctyp, id) -> - pp_keyword "create" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp | I_reset (ctyp, id) -> pp_keyword "recreate" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp | I_init (ctyp, id, cval) -> @@ -282,11 +277,10 @@ let pp_cdef = function pp_keyword "register" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp ^^ hardline | CDEF_type tdef -> pp_ctype_def tdef ^^ hardline - | CDEF_let (n, bindings, instrs, cleanup) -> + | CDEF_let (n, bindings, instrs) -> let pp_binding (id, ctyp) = pp_id id ^^ string " : " ^^ pp_ctyp ctyp in pp_keyword "let" ^^ string (string_of_int n) ^^ parens (separate_map (comma ^^ space) pp_binding bindings) ^^ space ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace ^^ space - ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr cleanup) rbrace ^^ space ^^ hardline | CDEF_startup (id, instrs)-> pp_keyword "startup" ^^ pp_id id ^^ space @@ -357,7 +351,7 @@ let rec clexp_deps = function instruction **) let instr_deps = function | I_decl (ctyp, id) -> NS.empty, NS.singleton (G_id id) - | I_alloc (ctyp, id) | I_reset (ctyp, id) -> NS.empty, NS.singleton (G_id id) + | I_reset (ctyp, id) -> NS.empty, NS.singleton (G_id id) | I_init (ctyp, id, cval) | I_reinit (ctyp, id, cval) -> cval_deps cval, NS.singleton (G_id id) | I_if (cval, _, _, _) -> cval_deps cval, NS.empty | I_jump (cval, label) -> cval_deps cval, NS.singleton (G_label label) @@ -438,7 +432,6 @@ let make_dot id graph = | 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" -- cgit v1.2.3