diff options
Diffstat (limited to 'src/bytecode_util.ml')
| -rw-r--r-- | src/bytecode_util.ml | 771 |
1 files changed, 0 insertions, 771 deletions
diff --git a/src/bytecode_util.ml b/src/bytecode_util.ml deleted file mode 100644 index 630d2a48..00000000 --- a/src/bytecode_util.ml +++ /dev/null @@ -1,771 +0,0 @@ -(**************************************************************************) -(* 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 Bytecode -open Value2 -open PPrint - -(* Define wrappers for creating bytecode instructions. Each function - uses a counter to assign each instruction a unique identifier. *) - -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 ireset ?loc:(l=Parse_ast.Unknown) ctyp id = - I_aux (I_reset (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 = - I_aux (I_funcall (clexp, false, id, cvals), (instr_number (), l)) - -let iextern ?loc:(l=Parse_ast.Unknown) clexp id cvals = - I_aux (I_funcall (clexp, true, id, cvals), (instr_number (), l)) - -let icopy l clexp cval = - I_aux (I_copy (clexp, cval), (instr_number (), l)) - -let ialias l clexp cval = - I_aux (I_alias (clexp, cval), (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 iundefined ?loc:(l=Parse_ast.Unknown) ctyp = - I_aux (I_undefined ctyp, (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 ijump ?loc:(l=Parse_ast.Unknown) cval label = - I_aux (I_jump (cval, label), (instr_number (), l)) - -let rec frag_rename from_id to_id = function - | F_id id when Id.compare id from_id = 0 -> F_id to_id - | F_id id -> F_id id - | F_ref id when Id.compare id from_id = 0 -> F_ref to_id - | F_ref id -> F_ref id - | F_lit v -> F_lit v - | F_have_exception -> F_have_exception - | F_current_exception -> F_current_exception - | F_call (call, frags) -> F_call (call, List.map (frag_rename from_id to_id) frags) - | F_op (f1, op, f2) -> F_op (frag_rename from_id to_id f1, op, frag_rename from_id to_id f2) - | F_unary (op, f) -> F_unary (op, frag_rename from_id to_id f) - | F_field (f, field) -> F_field (frag_rename from_id to_id f, field) - | F_raw raw -> F_raw raw - | F_poly f -> F_poly (frag_rename from_id to_id f) - -let cval_rename from_id to_id (frag, ctyp) = (frag_rename from_id to_id frag, ctyp) - -let rec clexp_rename from_id to_id = function - | CL_id (id, ctyp) when Id.compare id from_id = 0 -> CL_id (to_id, ctyp) - | CL_id (id, ctyp) -> CL_id (id, ctyp) - | CL_field (clexp, field) -> - CL_field (clexp_rename from_id to_id clexp, field) - | CL_addr clexp -> - CL_addr (clexp_rename from_id to_id clexp) - | CL_tuple (clexp, n) -> - CL_tuple (clexp_rename from_id to_id clexp, n) - | CL_current_exception ctyp -> CL_current_exception ctyp - | CL_have_exception -> CL_have_exception - -let rec instr_rename from_id to_id (I_aux (instr, aux)) = - let instr = match instr with - | I_decl (ctyp, id) when Id.compare id from_id = 0 -> I_decl (ctyp, to_id) - | I_decl (ctyp, id) -> I_decl (ctyp, id) - - | I_init (ctyp, id, cval) when Id.compare id from_id = 0 -> - I_init (ctyp, to_id, cval_rename from_id to_id cval) - | I_init (ctyp, id, cval) -> - I_init (ctyp, id, cval_rename from_id to_id cval) - - | I_if (cval, then_instrs, else_instrs, ctyp2) -> - I_if (cval_rename from_id to_id cval, - List.map (instr_rename from_id to_id) then_instrs, - List.map (instr_rename from_id to_id) else_instrs, - ctyp2) - - | I_jump (cval, label) -> I_jump (cval_rename from_id to_id cval, label) - - | I_funcall (clexp, extern, id, args) -> - I_funcall (clexp_rename from_id to_id clexp, extern, id, List.map (cval_rename from_id to_id) args) - - | I_copy (clexp, cval) -> I_copy (clexp_rename from_id to_id clexp, cval_rename from_id to_id cval) - | I_alias (clexp, cval) -> I_alias (clexp_rename from_id to_id clexp, cval_rename from_id to_id cval) - - | I_clear (ctyp, id) when Id.compare id from_id = 0 -> I_clear (ctyp, to_id) - | I_clear (ctyp, id) -> I_clear (ctyp, id) - - | I_return cval -> I_return (cval_rename from_id to_id cval) - - | I_block instrs -> I_block (List.map (instr_rename from_id to_id) instrs) - - | I_try_block instrs -> I_try_block (List.map (instr_rename from_id to_id) instrs) - - | I_throw cval -> I_throw (cval_rename from_id to_id cval) - - | I_comment str -> I_comment str - - | I_raw str -> I_raw str - - | I_label label -> I_label label - - | I_goto label -> I_goto label - - | I_undefined ctyp -> I_undefined ctyp - - | I_match_failure -> I_match_failure - - | I_reset (ctyp, id) when Id.compare id from_id = 0 -> I_reset (ctyp, to_id) - | I_reset (ctyp, id) -> I_reset (ctyp, id) - - | I_reinit (ctyp, id, cval) when Id.compare id from_id = 0 -> - I_reinit (ctyp, to_id, cval_rename from_id to_id cval) - | I_reinit (ctyp, id, cval) -> - I_reinit (ctyp, id, cval_rename from_id to_id cval) - in - I_aux (instr, aux) - -(**************************************************************************) -(* 1. Instruction pretty printer *) -(**************************************************************************) - -let string_of_value = function - | V_bits [] -> "UINT64_C(0)" - | V_bits bs -> "UINT64_C(" ^ Sail2_values.show_bitlist bs ^ ")" - | V_int i -> Big_int.to_string i ^ "l" - | V_bool true -> "true" - | V_bool false -> "false" - | V_null -> "NULL" - | V_unit -> "UNIT" - | V_bit Sail2_values.B0 -> "UINT64_C(0)" - | V_bit Sail2_values.B1 -> "UINT64_C(1)" - | V_string str -> "\"" ^ str ^ "\"" - | V_ctor_kind str -> "Kind_" ^ Util.zencode_string str - | _ -> failwith "Cannot convert value to string" - -let rec string_of_fragment ?zencode:(zencode=true) = function - | F_id id when zencode -> Util.zencode_string (string_of_id id) - | F_id id -> string_of_id id - | F_ref id when zencode -> "&" ^ Util.zencode_string (string_of_id id) - | F_ref id -> "&" ^ string_of_id id - | F_lit v -> string_of_value v - | F_call (str, frags) -> - Printf.sprintf "%s(%s)" str (Util.string_of_list ", " (string_of_fragment ~zencode:zencode) frags) - | F_field (f, field) -> - Printf.sprintf "%s.%s" (string_of_fragment' ~zencode:zencode f) field - | F_op (f1, op, f2) -> - Printf.sprintf "%s %s %s" (string_of_fragment' ~zencode:zencode f1) op (string_of_fragment' ~zencode:zencode f2) - | F_unary (op, f) -> - op ^ string_of_fragment' ~zencode:zencode f - | F_have_exception -> "have_exception" - | F_current_exception -> "(*current_exception)" - | F_raw raw -> raw - | F_poly f -> string_of_fragment ~zencode:zencode f -and string_of_fragment' ?zencode:(zencode=true) f = - match f with - | F_op _ | F_unary _ -> "(" ^ string_of_fragment ~zencode:zencode f ^ ")" - | _ -> string_of_fragment ~zencode:zencode f - -(* String representation of ctyps here is only for debugging and - intermediate language pretty-printer. *) -and 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 ", " string_of_ctyp ctyps ^ ")" - | CT_struct (id, _) | CT_enum (id, _) | CT_variant (id, _) -> string_of_id id - | CT_string -> "string" - | CT_vector (true, ctyp) -> "vector(dec, " ^ string_of_ctyp ctyp ^ ")" - | CT_vector (false, ctyp) -> "vector(inc, " ^ string_of_ctyp ctyp ^ ")" - | CT_list ctyp -> "list(" ^ string_of_ctyp ctyp ^ ")" - | CT_ref ctyp -> "ref(" ^ string_of_ctyp ctyp ^ ")" - | CT_poly -> "*" - -(** 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 -> "*" - -let rec map_ctyp f = function - | (CT_lint | CT_fint _ | CT_lbits _ | CT_fbits _ | CT_sbits _ - | CT_bit | CT_unit | CT_bool | CT_real | CT_string | CT_poly | CT_enum _) as ctyp -> f ctyp - | CT_tup ctyps -> f (CT_tup (List.map (map_ctyp f) ctyps)) - | CT_ref ctyp -> f (CT_ref (map_ctyp f ctyp)) - | CT_vector (direction, ctyp) -> f (CT_vector (direction, map_ctyp f ctyp)) - | CT_list ctyp -> f (CT_list (map_ctyp f ctyp)) - | CT_struct (id, ctors) -> f (CT_struct (id, List.map (fun (id, ctyp) -> id, map_ctyp f ctyp) ctors)) - | CT_variant (id, ctors) -> f (CT_variant (id, List.map (fun (id, ctyp) -> id, map_ctyp f ctyp) ctors)) - -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_fbits (m1, d1), CT_fbits (m2, d2) -> m1 = m2 && d1 = d2 - | CT_bit, CT_bit -> true - | CT_fint n, CT_fint m -> n = m - | CT_unit, CT_unit -> true - | CT_bool, CT_bool -> true - | CT_struct (id1, _), CT_struct (id2, _) -> Id.compare id1 id2 = 0 - | CT_enum (id1, _), CT_enum (id2, _) -> Id.compare id1 id2 = 0 - | CT_variant (id1, _), CT_variant (id2, _) -> Id.compare id1 id2 = 0 - | CT_tup ctyps1, CT_tup ctyps2 when List.length ctyps1 = List.length ctyps2 -> - List.for_all2 ctyp_equal ctyps1 ctyps2 - | CT_string, CT_string -> true - | CT_real, CT_real -> true - | CT_vector (d1, ctyp1), CT_vector (d2, ctyp2) -> d1 = d2 && ctyp_equal ctyp1 ctyp2 - | CT_list ctyp1, CT_list ctyp2 -> ctyp_equal ctyp1 ctyp2 - | CT_ref ctyp1, CT_ref ctyp2 -> ctyp_equal ctyp1 ctyp2 - | CT_poly, CT_poly -> true - | _, _ -> false - -let rec ctyp_unify ctyp1 ctyp2 = - match ctyp1, ctyp2 with - | CT_tup ctyps1, CT_tup ctyps2 when List.length ctyps1 = List.length ctyps2 -> - List.concat (List.map2 ctyp_unify ctyps1 ctyps2) - - | CT_vector (b1, ctyp1), CT_vector (b2, ctyp2) when b1 = b2 -> - ctyp_unify ctyp1 ctyp2 - - | CT_list ctyp1, CT_list ctyp2 -> ctyp_unify ctyp1 ctyp2 - - | CT_ref ctyp1, CT_ref ctyp2 -> ctyp_unify ctyp1 ctyp2 - - | CT_poly, _ -> [ctyp2] - - | _, _ when ctyp_equal ctyp1 ctyp2 -> [] - | _, _ -> raise (Invalid_argument "ctyp_unify") - -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_fint _ -> CT_lint - | CT_unit -> CT_unit - | CT_bool -> CT_bool - | CT_real -> CT_real - | CT_bit -> CT_bit - | CT_tup ctyps -> CT_tup (List.map ctyp_suprema ctyps) - | CT_string -> CT_string - | CT_enum (id, ids) -> CT_enum (id, ids) - (* Do we really never want to never call ctyp_suprema on constructor - fields? Doing it causes issues for structs (see - test/c/stack_struct.sail) but it might be wrong to not call it - for nested variants... *) - | CT_struct (id, ctors) -> CT_struct (id, ctors) - | CT_variant (id, ctors) -> CT_variant (id, ctors) - | CT_vector (d, ctyp) -> CT_vector (d, ctyp_suprema ctyp) - | CT_list ctyp -> CT_list (ctyp_suprema ctyp) - | CT_ref ctyp -> CT_ref (ctyp_suprema ctyp) - | CT_poly -> CT_poly - -let rec ctyp_ids = function - | CT_enum (id, _) -> IdSet.singleton id - | CT_struct (id, ctors) | CT_variant (id, ctors) -> - IdSet.add id (List.fold_left (fun ids (_, ctyp) -> IdSet.union (ctyp_ids ctyp) ids) IdSet.empty ctors) - | CT_tup ctyps -> List.fold_left (fun ids ctyp -> IdSet.union (ctyp_ids ctyp) ids) IdSet.empty ctyps - | CT_vector (_, ctyp) | CT_list ctyp | CT_ref ctyp -> ctyp_ids ctyp - | CT_lint | CT_fint _ | CT_lbits _ | CT_fbits _ | CT_sbits _ | CT_unit - | CT_bool | CT_real | CT_bit | CT_string | CT_poly -> IdSet.empty - -let rec unpoly = function - | F_poly f -> unpoly f - | F_call (call, fs) -> F_call (call, List.map unpoly fs) - | F_field (f, field) -> F_field (unpoly f, field) - | F_op (f1, op, f2) -> F_op (unpoly f1, op, unpoly f2) - | F_unary (op, f) -> F_unary (op, unpoly f) - | f -> f - -let rec is_polymorphic = function - | CT_lint | CT_fint _ | CT_lbits _ | CT_fbits _ | CT_sbits _ | CT_bit | CT_unit | CT_bool | CT_real | CT_string -> false - | CT_tup ctyps -> List.exists is_polymorphic ctyps - | CT_enum _ -> false - | CT_struct (_, ctors) | CT_variant (_, ctors) -> List.exists (fun (_, ctyp) -> is_polymorphic ctyp) ctors - | CT_vector (_, ctyp) | CT_list ctyp | CT_ref ctyp -> is_polymorphic ctyp - | CT_poly -> true - -let pp_id id = - string (string_of_id id) - -let pp_ctyp ctyp = - string (string_of_ctyp ctyp |> Util.yellow |> Util.clear) - -let pp_keyword str = - string ((str |> Util.red |> Util.clear) ^ " ") - -let pp_cval (frag, ctyp) = - string (string_of_fragment ~zencode:false frag) ^^ string " : " ^^ pp_ctyp ctyp - -let rec pp_clexp = function - | CL_id (id, ctyp) -> pp_id id ^^ string " : " ^^ pp_ctyp ctyp - | CL_field (clexp, field) -> parens (pp_clexp clexp) ^^ string "." ^^ string field - | CL_tuple (clexp, n) -> parens (pp_clexp clexp) ^^ string "." ^^ string (string_of_int n) - | CL_addr clexp -> string "*" ^^ pp_clexp clexp - | CL_current_exception ctyp -> string "current_exception : " ^^ pp_ctyp ctyp - | CL_have_exception -> string "have_exception" - -let rec pp_instr ?short:(short=false) (I_aux (instr, aux)) = - match instr with - | I_decl (ctyp, id) -> - pp_keyword "var" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp - | I_if (cval, then_instrs, else_instrs, ctyp) -> - let pp_if_block = function - | [] -> string "{}" - | instrs -> surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace - in - parens (pp_ctyp ctyp) ^^ space - ^^ pp_keyword "if" ^^ pp_cval cval - ^^ if short then - empty - else - pp_keyword " then" ^^ pp_if_block then_instrs - ^^ pp_keyword " else" ^^ pp_if_block else_instrs - | I_jump (cval, label) -> - pp_keyword "jump" ^^ pp_cval cval ^^ space ^^ string (label |> Util.blue |> Util.clear) - | I_block instrs -> - 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_reset (ctyp, id) -> - pp_keyword "recreate" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp - | I_init (ctyp, id, cval) -> - pp_keyword "create" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp ^^ string " = " ^^ pp_cval cval - | I_reinit (ctyp, id, cval) -> - pp_keyword "recreate" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp ^^ string " = " ^^ pp_cval cval - | I_funcall (x, _, f, args) -> - separate space [ pp_clexp x; string "="; - string (string_of_id f |> Util.green |> Util.clear) ^^ parens (separate_map (string ", ") pp_cval args) ] - | I_copy (clexp, cval) -> - separate space [pp_clexp clexp; string "="; pp_cval cval] - | I_alias (clexp, cval) -> - pp_keyword "alias" ^^ separate space [pp_clexp clexp; string "="; pp_cval cval] - | I_clear (ctyp, id) -> - pp_keyword "kill" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp - | I_return cval -> - pp_keyword "return" ^^ pp_cval cval - | I_throw cval -> - pp_keyword "throw" ^^ pp_cval cval - | I_comment str -> - string ("// " ^ str |> Util.magenta |> Util.clear) - | I_label str -> - string (str |> Util.blue |> Util.clear) ^^ string ":" - | I_goto str -> - pp_keyword "goto" ^^ string (str |> Util.blue |> Util.clear) - | I_match_failure -> - pp_keyword "match_failure" - | I_undefined ctyp -> - pp_keyword "undefined" ^^ pp_ctyp ctyp - | I_raw str -> - pp_keyword "C" ^^ string (str |> Util.cyan |> Util.clear) - -let pp_ctype_def = function - | CTD_enum (id, ids) -> - pp_keyword "enum" ^^ pp_id id ^^ string " = " - ^^ separate_map (string " | ") pp_id ids - | CTD_struct (id, fields) -> - pp_keyword "struct" ^^ pp_id id ^^ string " = " - ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) (fun (id, ctyp) -> pp_id id ^^ string " : " ^^ pp_ctyp ctyp) fields) rbrace - | CTD_variant (id, ctors) -> - pp_keyword "union" ^^ pp_id id ^^ string " = " - ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) (fun (id, ctyp) -> pp_id id ^^ string " : " ^^ pp_ctyp ctyp) ctors) rbrace - -let pp_cdef = function - | CDEF_spec (id, ctyps, ctyp) -> - pp_keyword "val" ^^ pp_id id ^^ string " : " ^^ parens (separate_map (comma ^^ space) pp_ctyp ctyps) ^^ string " -> " ^^ pp_ctyp ctyp - ^^ hardline - | CDEF_fundef (id, ret, args, instrs) -> - let ret = match ret with - | None -> empty - | Some id -> space ^^ pp_id id - in - pp_keyword "function" ^^ pp_id id ^^ ret ^^ parens (separate_map (comma ^^ space) pp_id args) ^^ space - ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace - ^^ hardline - | CDEF_reg_dec (id, ctyp, instrs) -> - pp_keyword "register" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp ^^ space - ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace - ^^ hardline - | CDEF_type tdef -> pp_ctype_def tdef ^^ hardline - | 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 - ^^ hardline - | CDEF_startup (id, instrs)-> - pp_keyword "startup" ^^ pp_id id ^^ space - ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace - ^^ hardline - | CDEF_finish (id, instrs)-> - pp_keyword "finish" ^^ pp_id id ^^ space - ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace - ^^ hardline - -(**************************************************************************) -(* 2. Dependency Graphs *) -(**************************************************************************) - -type graph_node = - | G_label of string - | G_instr of int * instr - | G_start - -let string_of_node = function - | G_label label -> label - | G_instr (n, instr) -> string_of_int n ^ ": " ^ Pretty_print_sail.to_string (pp_instr ~short:true instr) - | G_start -> "START" - -module Node = struct - type t = graph_node - let compare gn1 gn2 = - match gn1, gn2 with - | G_label str1, G_label str2 -> String.compare str1 str2 - | G_instr (n1, _), G_instr (n2, _) -> compare n1 n2 - | G_start , G_start -> 0 - | G_start , _ -> 1 - | _ , G_start -> -1 - | G_instr _, _ -> 1 - | _ , G_instr _ -> -1 -end - -module NodeGraph = Graph.Make(Node) - -module NM = Map.Make(Node) -module NS = Set.Make(Node) - -type dep_graph = NodeGraph.graph - -let rec fragment_deps = function - | F_id id | F_ref id -> IdSet.singleton id - | F_lit _ -> IdSet.empty - | F_field (frag, _) | F_unary (_, frag) | F_poly frag -> fragment_deps frag - | F_call (_, frags) -> List.fold_left IdSet.union IdSet.empty (List.map fragment_deps frags) - | F_op (frag1, _, frag2) -> IdSet.union (fragment_deps frag1) (fragment_deps frag2) - | F_current_exception -> IdSet.empty - | F_have_exception -> IdSet.empty - | F_raw _ -> IdSet.empty - -let cval_deps = function (frag, _) -> fragment_deps frag - -let rec clexp_deps = function - | CL_id (id, _) -> IdSet.singleton id - | CL_field (clexp, _) -> clexp_deps clexp - | CL_tuple (clexp, _) -> clexp_deps clexp - | CL_addr clexp -> clexp_deps clexp - | CL_have_exception -> IdSet.empty - | CL_current_exception _ -> IdSet.empty - -(* Return the direct, read/write dependencies of a single instruction *) -let instr_deps = function - | I_decl (ctyp, id) -> IdSet.empty, IdSet.singleton id - | I_reset (ctyp, id) -> IdSet.empty, IdSet.singleton id - | I_init (ctyp, id, cval) | I_reinit (ctyp, id, cval) -> cval_deps cval, IdSet.singleton id - | I_if (cval, _, _, _) -> cval_deps cval, IdSet.empty - | I_jump (cval, label) -> cval_deps cval, IdSet.empty - | I_funcall (clexp, _, _, cvals) -> List.fold_left IdSet.union IdSet.empty (List.map cval_deps cvals), clexp_deps clexp - | I_copy (clexp, cval) -> cval_deps cval, clexp_deps clexp - | I_alias (clexp, cval) -> cval_deps cval, clexp_deps clexp - | I_clear (_, id) -> IdSet.singleton id, IdSet.singleton id - | I_throw cval | I_return cval -> cval_deps cval, IdSet.empty - | I_block _ | I_try_block _ -> IdSet.empty, IdSet.empty - | I_comment _ | I_raw _ -> IdSet.empty, IdSet.empty - | I_label label -> IdSet.empty, IdSet.empty - | I_goto label -> IdSet.empty, IdSet.empty - | I_undefined _ -> IdSet.empty, IdSet.empty - | I_match_failure -> IdSet.empty, IdSet.empty - -(* instrs_graph returns the control-flow graph for a list of - instructions. *) -let instrs_graph instrs = - let icounter = ref 0 in - let graph = ref NodeGraph.empty in - - let rec add_instr last_instrs (I_aux (instr, _) as iaux) = - incr icounter; - let node = G_instr (!icounter, iaux) in - match instr with - | I_block instrs | I_try_block instrs -> - List.fold_left add_instr last_instrs instrs - | I_if (_, then_instrs, else_instrs, _) -> - List.iter (fun i -> graph := NodeGraph.add_edge' i node !graph) last_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, icomment "join") in - List.iter (fun i -> graph := NodeGraph.add_edge' i join !graph) n1; - List.iter (fun i -> graph := NodeGraph.add_edge' i join !graph) n2; - [join] - | I_return _ -> - List.iter (fun i -> graph := NodeGraph.add_edge' i node !graph) last_instrs; - [] - | I_label label -> - graph := NodeGraph.add_edge' (G_label label) node !graph; - node :: last_instrs - | I_goto label -> - List.iter (fun i -> graph := NodeGraph.add_edge' i node !graph) last_instrs; - graph := NodeGraph.add_edge' node (G_label label) !graph; - [] - | I_jump (cval, label) -> - List.iter (fun i -> graph := NodeGraph.add_edge' i node !graph) last_instrs; - graph := NodeGraph.add_edges' (G_label label) [] !graph; - [node] - | I_match_failure -> - List.iter (fun i -> graph := NodeGraph.add_edge' i node !graph) last_instrs; - [] - | _ -> - List.iter (fun i -> graph := NodeGraph.add_edge' i node !graph) last_instrs; - [node] - in - ignore (List.fold_left add_instr [G_start] instrs); - let graph = NodeGraph.fix_leaves !graph in - 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_instr (_, I_aux (I_decl _, _)) -> "olivedrab1" - | G_instr (_, I_aux (I_init _, _)) -> "springgreen" - | 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 (_, I_aux (I_return _, _)) -> "deeppink" - | G_instr (_, I_aux (I_undefined _, _)) -> "deeppink" - | G_instr _ -> "azure" - | G_label _ -> "lightpink" - in - let edge_color from_node to_node = - match from_node, to_node with - | G_start , _ -> "goldenrod4" - | G_label _, _ -> "darkgreen" - | _ , G_label _ -> "goldenrod4" - | G_instr _, G_instr _ -> "black" - | _ , _ -> "coral3" - in - let out_chan = open_out (Util.zencode_string (string_of_id id) ^ ".gv") in - NodeGraph.make_dot node_color edge_color to_string out_chan graph; - close_out out_chan - -let rec map_clexp_ctyp f = function - | CL_id (id, ctyp) -> CL_id (id, f ctyp) - | CL_field (clexp, field) -> CL_field (map_clexp_ctyp f clexp, field) - | CL_tuple (clexp, n) -> CL_tuple (map_clexp_ctyp f clexp, n) - | 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 - -let rec map_instr_ctyp f (I_aux (instr, aux)) = - let instr = match instr with - | I_decl (ctyp, id) -> I_decl (f ctyp, id) - | I_init (ctyp1, id, (frag, ctyp2)) -> I_init (f ctyp1, id, (frag, f ctyp2)) - | I_if ((frag, ctyp1), then_instrs, else_instrs, ctyp2) -> - I_if ((frag, f ctyp1), List.map (map_instr_ctyp f) then_instrs, List.map (map_instr_ctyp f) else_instrs, f ctyp2) - | I_jump ((frag, ctyp), label) -> I_jump ((frag, f ctyp), label) - | I_funcall (clexp, extern, id, cvals) -> - I_funcall (map_clexp_ctyp f clexp, extern, id, List.map (fun (frag, ctyp) -> frag, f ctyp) cvals) - | I_copy (clexp, (frag, ctyp)) -> I_copy (map_clexp_ctyp f clexp, (frag, f ctyp)) - | I_alias (clexp, (frag, ctyp)) -> I_alias (map_clexp_ctyp f clexp, (frag, f ctyp)) - | I_clear (ctyp, id) -> I_clear (f ctyp, id) - | I_return (frag, ctyp) -> I_return (frag, f ctyp) - | I_block instrs -> I_block (List.map (map_instr_ctyp f) instrs) - | I_try_block instrs -> I_try_block (List.map (map_instr_ctyp f) instrs) - | I_throw (frag, ctyp) -> I_throw (frag, f ctyp) - | 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_comment _ | I_raw _ | I_label _ | I_goto _ | I_match_failure) as instr -> instr - in - I_aux (instr, aux) - -(** Map over each instruction within an instruction, bottom-up *) -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_if (cval, instrs1, instrs2, ctyp) -> - I_if (cval, List.map (map_instr f) instrs1, List.map (map_instr f) instrs2, ctyp) - | I_block instrs -> - I_block (List.map (map_instr f) instrs) - | I_try_block instrs -> - I_try_block (List.map (map_instr f) instrs) - in - f (I_aux (instr, aux)) - -(** Map over each instruction in a cdef using map_instr *) -let cdef_map_instr f = function - | CDEF_reg_dec (id, ctyp, instrs) -> CDEF_reg_dec (id, ctyp, List.map (map_instr f) instrs) - | CDEF_let (n, bindings, instrs) -> CDEF_let (n, bindings, List.map (map_instr f) instrs) - | CDEF_fundef (id, heap_return, args, instrs) -> CDEF_fundef (id, heap_return, args, List.map (map_instr f) instrs) - | CDEF_startup (id, instrs) -> CDEF_startup (id, List.map (map_instr f) instrs) - | CDEF_finish (id, instrs) -> CDEF_finish (id, List.map (map_instr f) instrs) - | CDEF_spec (id, ctyps, ctyp) -> CDEF_spec (id, ctyps, ctyp) - | CDEF_type tdef -> CDEF_type tdef - -let ctype_def_map_ctyp f = function - | CTD_enum (id, ids) -> CTD_enum (id, ids) - | CTD_struct (id, ctors) -> CTD_struct (id, List.map (fun (field, ctyp) -> (field, f ctyp)) ctors) - | CTD_variant (id, ctors) -> CTD_variant (id, List.map (fun (field, ctyp) -> (field, f ctyp)) ctors) - -(** Map over each ctyp in a cdef using map_instr_ctyp *) -let cdef_map_ctyp f = function - | CDEF_reg_dec (id, ctyp, instrs) -> CDEF_reg_dec (id, f ctyp, List.map (map_instr_ctyp f) instrs) - | CDEF_let (n, bindings, instrs) -> CDEF_let (n, bindings, List.map (map_instr_ctyp f) instrs) - | CDEF_fundef (id, heap_return, args, instrs) -> CDEF_fundef (id, heap_return, args, List.map (map_instr_ctyp f) instrs) - | CDEF_startup (id, instrs) -> CDEF_startup (id, List.map (map_instr_ctyp f) instrs) - | CDEF_finish (id, instrs) -> CDEF_finish (id, List.map (map_instr_ctyp f) instrs) - | CDEF_spec (id, ctyps, ctyp) -> CDEF_spec (id, List.map f ctyps, f ctyp) - | CDEF_type tdef -> CDEF_type (ctype_def_map_ctyp f tdef) - -(* Map over all sequences of instructions contained within an instruction *) -let rec map_instrs f (I_aux (instr, aux)) = - let instr = match instr with - | I_decl _ | I_init _ | I_reset _ | I_reinit _ -> 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_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 - in - I_aux (instr, aux) - -let rec instr_ids (I_aux (instr, _)) = - let reads, writes = instr_deps instr in - IdSet.of_list (IdSet.elements reads @ IdSet.elements writes) - -let rec instr_reads (I_aux (instr, _)) = - let reads, _ = instr_deps instr in - IdSet.of_list (IdSet.elements reads) - -let rec instr_writes (I_aux (instr, _)) = - let _, writes = instr_deps instr in - IdSet.of_list (IdSet.elements writes) - -let rec filter_instrs f instrs = - let filter_instrs' = function - | I_aux (I_block instrs, aux) -> I_aux (I_block (filter_instrs f instrs), aux) - | I_aux (I_try_block instrs, aux) -> I_aux (I_try_block (filter_instrs f instrs), aux) - | I_aux (I_if (cval, instrs1, instrs2, ctyp), aux) -> - I_aux (I_if (cval, filter_instrs f instrs1, filter_instrs f instrs2, ctyp), aux) - | instr -> instr - in - List.filter f (List.map filter_instrs' instrs) |