diff options
| author | Jon French | 2019-03-14 13:56:37 +0000 |
|---|---|---|
| committer | Jon French | 2019-03-14 13:56:37 +0000 |
| commit | 0d88c148a2a068a95b5fc3d5c25b599faf3e75a0 (patch) | |
| tree | cb507bee25582f503ae4047ce32558352aeb8b27 /src/jib | |
| parent | 4f14ccb421443dbc10b88e190526dda754f324aa (diff) | |
| parent | ec8cad1daa76fb265014d3d313173905925c9922 (diff) | |
Merge branch 'sail2' into rmem_interpreter
Diffstat (limited to 'src/jib')
| -rw-r--r-- | src/jib/anf.ml | 692 | ||||
| -rw-r--r-- | src/jib/anf.mli | 161 | ||||
| -rw-r--r-- | src/jib/c_backend.ml | 2324 | ||||
| -rw-r--r-- | src/jib/c_backend.mli | 109 | ||||
| -rw-r--r-- | src/jib/jib_compile.ml | 1403 | ||||
| -rw-r--r-- | src/jib/jib_compile.mli | 100 | ||||
| -rw-r--r-- | src/jib/jib_optimize.ml | 129 | ||||
| -rw-r--r-- | src/jib/jib_optimize.mli | 63 | ||||
| -rw-r--r-- | src/jib/jib_ssa.ml | 602 | ||||
| -rw-r--r-- | src/jib/jib_ssa.mli | 85 | ||||
| -rw-r--r-- | src/jib/jib_util.ml | 874 |
11 files changed, 6542 insertions, 0 deletions
diff --git a/src/jib/anf.ml b/src/jib/anf.ml new file mode 100644 index 00000000..025138d0 --- /dev/null +++ b/src/jib/anf.ml @@ -0,0 +1,692 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* Alasdair Armstrong *) +(* Brian Campbell *) +(* Thomas Bauereiss *) +(* Anthony Fox *) +(* Jon French *) +(* Dominic Mulligan *) +(* Stephen Kell *) +(* Mark Wassell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + +open Ast +open Ast_util +open Jib +open Jib_util +open Type_check +open PPrint + +module Big_int = Nat_big_num + +(**************************************************************************) +(* 1. Conversion to A-normal form (ANF) *) +(**************************************************************************) + +type 'a aexp = AE_aux of 'a aexp_aux * Env.t * l + +and 'a aexp_aux = + | AE_val of 'a aval + | AE_app of id * ('a aval) list * 'a + | AE_cast of 'a aexp * 'a + | AE_assign of id * 'a * 'a aexp + | AE_let of mut * id * 'a * 'a aexp * 'a aexp * 'a + | AE_block of ('a aexp) list * 'a aexp * 'a + | AE_return of 'a aval * 'a + | AE_throw of 'a aval * 'a + | AE_if of 'a aval * 'a aexp * 'a aexp * 'a + | AE_field of 'a aval * id * 'a + | AE_case of 'a aval * ('a apat * 'a aexp * 'a aexp) list * 'a + | AE_try of 'a aexp * ('a apat * 'a aexp * 'a aexp) list * 'a + | AE_record_update of 'a aval * ('a aval) Bindings.t * 'a + | AE_for of id * 'a aexp * 'a aexp * 'a aexp * order * 'a aexp + | AE_loop of loop * 'a aexp * 'a aexp + | AE_short_circuit of sc_op * 'a aval * 'a aexp + +and sc_op = SC_and | SC_or + +and 'a apat = AP_aux of 'a apat_aux * Env.t * l + +and 'a apat_aux = + | AP_tup of ('a apat) list + | AP_id of id * 'a + | AP_global of id * 'a + | AP_app of id * 'a apat * 'a + | AP_cons of 'a apat * 'a apat + | AP_nil of 'a + | AP_wild of 'a + +and 'a aval = + | AV_lit of lit * 'a + | AV_id of id * 'a lvar + | AV_ref of id * 'a lvar + | AV_tuple of ('a aval) list + | AV_list of ('a aval) list * 'a + | AV_vector of ('a aval) list * 'a + | AV_record of ('a aval) Bindings.t * 'a + | AV_C_fragment of fragment * 'a * ctyp + +(* Renaming variables in ANF expressions *) + +let rec apat_bindings (AP_aux (apat_aux, _, _)) = + match apat_aux with + | AP_tup apats -> List.fold_left IdSet.union IdSet.empty (List.map apat_bindings apats) + | AP_id (id, _) -> IdSet.singleton id + | AP_global (id, _) -> IdSet.empty + | AP_app (id, apat, _) -> apat_bindings apat + | AP_cons (apat1, apat2) -> IdSet.union (apat_bindings apat1) (apat_bindings apat2) + | AP_nil _ -> IdSet.empty + | AP_wild _ -> IdSet.empty + +(** This function returns the types of all bound variables in a + pattern. It ignores AP_global, apat_globals is used for that. *) +let rec apat_types (AP_aux (apat_aux, _, _)) = + let merge id b1 b2 = + match b1, b2 with + | None, None -> None + | Some v, None -> Some v + | None, Some v -> Some v + | Some _, Some _ -> assert false + in + match apat_aux with + | AP_tup apats -> List.fold_left (Bindings.merge merge) Bindings.empty (List.map apat_types apats) + | AP_id (id, typ) -> Bindings.singleton id typ + | AP_global (id, _) -> Bindings.empty + | AP_app (id, apat, _) -> apat_types apat + | AP_cons (apat1, apat2) -> (Bindings.merge merge) (apat_types apat1) (apat_types apat2) + | AP_nil _ -> Bindings.empty + | AP_wild _ -> Bindings.empty + +let rec apat_rename from_id to_id (AP_aux (apat_aux, env, l)) = + let apat_aux = match apat_aux with + | AP_tup apats -> AP_tup (List.map (apat_rename from_id to_id) apats) + | AP_id (id, typ) when Id.compare id from_id = 0 -> AP_id (to_id, typ) + | AP_id (id, typ) -> AP_id (id, typ) + | AP_global (id, typ) -> AP_global (id, typ) + | AP_app (ctor, apat, typ) -> AP_app (ctor, apat_rename from_id to_id apat, typ) + | AP_cons (apat1, apat2) -> AP_cons (apat_rename from_id to_id apat1, apat_rename from_id to_id apat2) + | AP_nil typ -> AP_nil typ + | AP_wild typ -> AP_wild typ + in + AP_aux (apat_aux, env, l) + +let rec aval_rename from_id to_id = function + | AV_lit (lit, typ) -> AV_lit (lit, typ) + | AV_id (id, lvar) when Id.compare id from_id = 0 -> AV_id (to_id, lvar) + | AV_id (id, lvar) -> AV_id (id, lvar) + | AV_ref (id, lvar) when Id.compare id from_id = 0 -> AV_ref (to_id, lvar) + | AV_ref (id, lvar) -> AV_ref (id, lvar) + | AV_tuple avals -> AV_tuple (List.map (aval_rename from_id to_id) avals) + | AV_list (avals, typ) -> AV_list (List.map (aval_rename from_id to_id) avals, typ) + | AV_vector (avals, typ) -> AV_vector (List.map (aval_rename from_id to_id) avals, typ) + | AV_record (avals, typ) -> AV_record (Bindings.map (aval_rename from_id to_id) avals, typ) + | AV_C_fragment (fragment, typ, ctyp) -> AV_C_fragment (frag_rename from_id to_id fragment, typ, ctyp) + +let rec aexp_rename from_id to_id (AE_aux (aexp, env, l)) = + let recur = aexp_rename from_id to_id in + let aexp = match aexp with + | AE_val aval -> AE_val (aval_rename from_id to_id aval) + | AE_app (id, avals, typ) -> AE_app (id, List.map (aval_rename from_id to_id) avals, typ) + | AE_cast (aexp, typ) -> AE_cast (recur aexp, typ) + | AE_assign (id, typ, aexp) when Id.compare from_id id = 0 -> AE_assign (to_id, typ, aexp_rename from_id to_id aexp) + | AE_assign (id, typ, aexp) -> AE_assign (id, typ, aexp_rename from_id to_id aexp) + | AE_let (mut, id, typ1, aexp1, aexp2, typ2) when Id.compare from_id id = 0 -> AE_let (mut, id, typ1, recur aexp1, aexp2, typ2) + | AE_let (mut, id, typ1, aexp1, aexp2, typ2) -> AE_let (mut, id, typ1, recur aexp1, recur aexp2, typ2) + | AE_block (aexps, aexp, typ) -> AE_block (List.map recur aexps, recur aexp, typ) + | AE_return (aval, typ) -> AE_return (aval_rename from_id to_id aval, typ) + | AE_throw (aval, typ) -> AE_throw (aval_rename from_id to_id aval, typ) + | AE_if (aval, then_aexp, else_aexp, typ) -> AE_if (aval_rename from_id to_id aval, recur then_aexp, recur else_aexp, typ) + | AE_field (aval, id, typ) -> AE_field (aval_rename from_id to_id aval, id, typ) + | AE_case (aval, apexps, typ) -> AE_case (aval_rename from_id to_id aval, List.map (apexp_rename from_id to_id) apexps, typ) + | AE_try (aexp, apexps, typ) -> AE_try (aexp_rename from_id to_id aexp, List.map (apexp_rename from_id to_id) apexps, typ) + | AE_record_update (aval, avals, typ) -> AE_record_update (aval_rename from_id to_id aval, Bindings.map (aval_rename from_id to_id) avals, typ) + | AE_for (id, aexp1, aexp2, aexp3, order, aexp4) when Id.compare from_id to_id = 0 -> AE_for (id, aexp1, aexp2, aexp3, order, aexp4) + | AE_for (id, aexp1, aexp2, aexp3, order, aexp4) -> AE_for (id, recur aexp1, recur aexp2, recur aexp3, order, recur aexp4) + | AE_loop (loop, aexp1, aexp2) -> AE_loop (loop, recur aexp1, recur aexp2) + | AE_short_circuit (op, aval, aexp) -> AE_short_circuit (op, aval_rename from_id to_id aval, recur aexp) + in + AE_aux (aexp, env, l) + +and apexp_rename from_id to_id (apat, aexp1, aexp2) = + if IdSet.mem from_id (apat_bindings apat) then + (apat, aexp1, aexp2) + else + (apat, aexp_rename from_id to_id aexp1, aexp_rename from_id to_id aexp2) + +let shadow_counter = ref 0 + +let new_shadow id = + let shadow_id = append_id id ("shadow#" ^ string_of_int !shadow_counter) in + incr shadow_counter; + shadow_id + +let rec no_shadow ids (AE_aux (aexp, env, l)) = + let aexp = match aexp with + | AE_val aval -> AE_val aval + | AE_app (id, avals, typ) -> AE_app (id, avals, typ) + | AE_cast (aexp, typ) -> AE_cast (no_shadow ids aexp, typ) + | AE_assign (id, typ, aexp) -> AE_assign (id, typ, no_shadow ids aexp) + | AE_let (mut, id, typ1, aexp1, aexp2, typ2) when IdSet.mem id ids -> + let shadow_id = new_shadow id in + let aexp1 = no_shadow ids aexp1 in + let ids = IdSet.add shadow_id ids in + AE_let (mut, shadow_id, typ1, aexp1, no_shadow ids (aexp_rename id shadow_id aexp2), typ2) + | AE_let (mut, id, typ1, aexp1, aexp2, typ2) -> + AE_let (mut, id, typ1, no_shadow ids aexp1, no_shadow (IdSet.add id ids) aexp2, typ2) + | AE_block (aexps, aexp, typ) -> AE_block (List.map (no_shadow ids) aexps, no_shadow ids aexp, typ) + | AE_return (aval, typ) -> AE_return (aval, typ) + | AE_throw (aval, typ) -> AE_throw (aval, typ) + | AE_if (aval, then_aexp, else_aexp, typ) -> AE_if (aval, no_shadow ids then_aexp, no_shadow ids else_aexp, typ) + | AE_field (aval, id, typ) -> AE_field (aval, id, typ) + | AE_case (aval, apexps, typ) -> AE_case (aval, List.map (no_shadow_apexp ids) apexps, typ) + | AE_try (aexp, apexps, typ) -> AE_try (no_shadow ids aexp, List.map (no_shadow_apexp ids) apexps, typ) + | AE_record_update (aval, avals, typ) -> AE_record_update (aval, avals, typ) + | AE_for (id, aexp1, aexp2, aexp3, order, aexp4) when IdSet.mem id ids -> + let shadow_id = new_shadow id in + let aexp1 = no_shadow ids aexp1 in + let aexp2 = no_shadow ids aexp2 in + let aexp3 = no_shadow ids aexp3 in + let ids = IdSet.add shadow_id ids in + AE_for (shadow_id, aexp1, aexp2, aexp3, order, no_shadow ids (aexp_rename id shadow_id aexp4)) + | AE_for (id, aexp1, aexp2, aexp3, order, aexp4) -> + let ids = IdSet.add id ids in + AE_for (id, no_shadow ids aexp1, no_shadow ids aexp2, no_shadow ids aexp3, order, no_shadow ids aexp4) + | AE_loop (loop, aexp1, aexp2) -> AE_loop (loop, no_shadow ids aexp1, no_shadow ids aexp2) + | AE_short_circuit (op, aval, aexp) -> AE_short_circuit (op, aval, no_shadow ids aexp) + in + AE_aux (aexp, env, l) + +and no_shadow_apexp ids (apat, aexp1, aexp2) = + let shadows = IdSet.inter (apat_bindings apat) ids in + let shadows = List.map (fun id -> id, new_shadow id) (IdSet.elements shadows) in + let rename aexp = List.fold_left (fun aexp (from_id, to_id) -> aexp_rename from_id to_id aexp) aexp shadows in + let rename_apat apat = List.fold_left (fun apat (from_id, to_id) -> apat_rename from_id to_id apat) apat shadows in + let ids = IdSet.union (apat_bindings apat) (IdSet.union ids (IdSet.of_list (List.map snd shadows))) in + (rename_apat apat, no_shadow ids (rename aexp1), no_shadow ids (rename aexp2)) + +(* Map over all the avals in an aexp. *) +let rec map_aval f (AE_aux (aexp, env, l)) = + let aexp = match aexp with + | AE_val v -> AE_val (f env l v) + | AE_cast (aexp, typ) -> AE_cast (map_aval f aexp, typ) + | AE_assign (id, typ, aexp) -> AE_assign (id, typ, map_aval f aexp) + | AE_app (id, vs, typ) -> AE_app (id, List.map (f env l) vs, typ) + | AE_let (mut, id, typ1, aexp1, aexp2, typ2) -> + AE_let (mut, id, typ1, map_aval f aexp1, map_aval f aexp2, typ2) + | AE_block (aexps, aexp, typ) -> AE_block (List.map (map_aval f) aexps, map_aval f aexp, typ) + | AE_return (aval, typ) -> AE_return (f env l aval, typ) + | AE_throw (aval, typ) -> AE_throw (f env l aval, typ) + | AE_if (aval, aexp1, aexp2, typ2) -> + AE_if (f env l aval, map_aval f aexp1, map_aval f aexp2, typ2) + | AE_loop (loop_typ, aexp1, aexp2) -> AE_loop (loop_typ, map_aval f aexp1, map_aval f aexp2) + | AE_for (id, aexp1, aexp2, aexp3, order, aexp4) -> + AE_for (id, map_aval f aexp1, map_aval f aexp2, map_aval f aexp3, order, map_aval f aexp4) + | AE_record_update (aval, updates, typ) -> + AE_record_update (f env l aval, Bindings.map (f env l) updates, typ) + | AE_field (aval, field, typ) -> + AE_field (f env l aval, field, typ) + | AE_case (aval, cases, typ) -> + AE_case (f env l aval, List.map (fun (pat, aexp1, aexp2) -> pat, map_aval f aexp1, map_aval f aexp2) cases, typ) + | AE_try (aexp, cases, typ) -> + AE_try (map_aval f aexp, List.map (fun (pat, aexp1, aexp2) -> pat, map_aval f aexp1, map_aval f aexp2) cases, typ) + | AE_short_circuit (op, aval, aexp) -> AE_short_circuit (op, f env l aval, map_aval f aexp) + in + AE_aux (aexp, env, l) + +(* Map over all the functions in an aexp. *) +let rec map_functions f (AE_aux (aexp, env, l)) = + let aexp = match aexp with + | AE_app (id, vs, typ) -> f env l id vs typ + | AE_cast (aexp, typ) -> AE_cast (map_functions f aexp, typ) + | AE_assign (id, typ, aexp) -> AE_assign (id, typ, map_functions f aexp) + | AE_short_circuit (op, aval, aexp) -> AE_short_circuit (op, aval, map_functions f aexp) + | AE_let (mut, id, typ1, aexp1, aexp2, typ2) -> AE_let (mut, id, typ1, map_functions f aexp1, map_functions f aexp2, typ2) + | AE_block (aexps, aexp, typ) -> AE_block (List.map (map_functions f) aexps, map_functions f aexp, typ) + | AE_if (aval, aexp1, aexp2, typ) -> + AE_if (aval, map_functions f aexp1, map_functions f aexp2, typ) + | AE_loop (loop_typ, aexp1, aexp2) -> AE_loop (loop_typ, map_functions f aexp1, map_functions f aexp2) + | AE_for (id, aexp1, aexp2, aexp3, order, aexp4) -> + AE_for (id, map_functions f aexp1, map_functions f aexp2, map_functions f aexp3, order, map_functions f aexp4) + | AE_case (aval, cases, typ) -> + AE_case (aval, List.map (fun (pat, aexp1, aexp2) -> pat, map_functions f aexp1, map_functions f aexp2) cases, typ) + | AE_try (aexp, cases, typ) -> + AE_try (map_functions f aexp, List.map (fun (pat, aexp1, aexp2) -> pat, map_functions f aexp1, map_functions f aexp2) cases, typ) + | AE_field _ | AE_record_update _ | AE_val _ | AE_return _ | AE_throw _ as v -> v + in + AE_aux (aexp, env, l) + +(* For debugging we provide a pretty printer for ANF expressions. *) + +let pp_lvar lvar doc = + match lvar with + | Register (_, _, typ) -> + string "[R/" ^^ string (string_of_typ typ |> Util.yellow |> Util.clear) ^^ string "]" ^^ doc + | Local (Mutable, typ) -> + string "[M/" ^^ string (string_of_typ typ |> Util.yellow |> Util.clear) ^^ string "]" ^^ doc + | Local (Immutable, typ) -> + string "[I/" ^^ string (string_of_typ typ |> Util.yellow |> Util.clear) ^^ string "]" ^^ doc + | Enum typ -> + string "[E/" ^^ string (string_of_typ typ |> Util.yellow |> Util.clear) ^^ string "]" ^^ doc + | Unbound -> string "[?]" ^^ doc + +let pp_annot typ doc = + string "[" ^^ string (string_of_typ typ |> Util.yellow |> Util.clear) ^^ string "]" ^^ doc + +let pp_order = function + | Ord_aux (Ord_inc, _) -> string "inc" + | Ord_aux (Ord_dec, _) -> string "dec" + | _ -> assert false (* Order types have been specialised, so no polymorphism in C backend. *) + +let rec pp_aexp (AE_aux (aexp, _, _)) = + match aexp with + | AE_val v -> pp_aval v + | AE_cast (aexp, typ) -> + pp_annot typ (string "$" ^^ pp_aexp aexp) + | AE_assign (id, typ, aexp) -> + pp_annot typ (pp_id id) ^^ string " := " ^^ pp_aexp aexp + | AE_app (id, args, typ) -> + pp_annot typ (pp_id id ^^ parens (separate_map (comma ^^ space) pp_aval args)) + | AE_short_circuit (SC_or, aval, aexp) -> + pp_aval aval ^^ string " || " ^^ pp_aexp aexp + | AE_short_circuit (SC_and, aval, aexp) -> + pp_aval aval ^^ string " && " ^^ pp_aexp aexp + | AE_let (mut, id, id_typ, binding, body, typ) -> group + begin + let let_doc = string (match mut with Immutable -> "let" | Mutable -> "let mut") in + match binding with + | AE_aux (AE_let _, _, _) -> + (pp_annot typ (separate space [string "let"; pp_annot id_typ (pp_id id); string "="]) + ^^ hardline ^^ nest 2 (pp_aexp binding)) + ^^ hardline ^^ string "in" ^^ space ^^ pp_aexp body + | _ -> + pp_annot typ (separate space [string "let"; pp_annot id_typ (pp_id id); string "="; pp_aexp binding; string "in"]) + ^^ hardline ^^ pp_aexp body + end + | AE_if (cond, then_aexp, else_aexp, typ) -> + pp_annot typ (separate space [ string "if"; pp_aval cond; + string "then"; pp_aexp then_aexp; + string "else"; pp_aexp else_aexp ]) + | AE_block (aexps, aexp, typ) -> + pp_annot typ (surround 2 0 lbrace (pp_block (aexps @ [aexp])) rbrace) + | AE_return (v, typ) -> pp_annot typ (string "return" ^^ parens (pp_aval v)) + | AE_throw (v, typ) -> pp_annot typ (string "throw" ^^ parens (pp_aval v)) + | AE_loop (While, aexp1, aexp2) -> + separate space [string "while"; pp_aexp aexp1; string "do"; pp_aexp aexp2] + | AE_loop (Until, aexp1, aexp2) -> + separate space [string "repeat"; pp_aexp aexp2; string "until"; pp_aexp aexp1] + | AE_for (id, aexp1, aexp2, aexp3, order, aexp4) -> + let header = + string "foreach" ^^ space ^^ + group (parens (separate (break 1) + [ pp_id id; + string "from " ^^ pp_aexp aexp1; + string "to " ^^ pp_aexp aexp2; + string "by " ^^ pp_aexp aexp3; + string "in " ^^ pp_order order ])) + in + header ^//^ pp_aexp aexp4 + | AE_field (aval, field, typ) -> pp_annot typ (parens (pp_aval aval ^^ string "." ^^ pp_id field)) + | AE_case (aval, cases, typ) -> + pp_annot typ (separate space [string "match"; pp_aval aval; pp_cases cases]) + | AE_try (aexp, cases, typ) -> + pp_annot typ (separate space [string "try"; pp_aexp aexp; pp_cases cases]) + | AE_record_update (aval, updates, typ) -> + braces (pp_aval aval ^^ string " with " + ^^ separate (string ", ") (List.map (fun (id, aval) -> pp_id id ^^ string " = " ^^ pp_aval aval) + (Bindings.bindings updates))) + +and pp_apat (AP_aux (apat_aux, _, _)) = + match apat_aux with + | AP_wild _ -> string "_" + | AP_id (id, typ) -> pp_annot typ (pp_id id) + | AP_global (id, _) -> pp_id id + | AP_tup apats -> parens (separate_map (comma ^^ space) pp_apat apats) + | AP_app (id, apat, typ) -> pp_annot typ (pp_id id ^^ parens (pp_apat apat)) + | AP_nil _ -> string "[||]" + | AP_cons (hd_apat, tl_apat) -> pp_apat hd_apat ^^ string " :: " ^^ pp_apat tl_apat + +and pp_cases cases = surround 2 0 lbrace (separate_map (comma ^^ hardline) pp_case cases) rbrace + +and pp_case (apat, guard, body) = + separate space [pp_apat apat; string "if"; pp_aexp guard; string "=>"; pp_aexp body] + +and pp_block = function + | [] -> string "()" + | [aexp] -> pp_aexp aexp + | aexp :: aexps -> pp_aexp aexp ^^ semi ^^ hardline ^^ pp_block aexps + +and pp_aval = function + | AV_lit (lit, typ) -> pp_annot typ (string (string_of_lit lit)) + | AV_id (id, lvar) -> pp_lvar lvar (pp_id id) + | AV_tuple avals -> parens (separate_map (comma ^^ space) pp_aval avals) + | AV_ref (id, lvar) -> string "ref" ^^ space ^^ pp_lvar lvar (pp_id id) + | AV_C_fragment (frag, typ, ctyp) -> + pp_annot typ (string ("(" ^ string_of_ctyp ctyp ^ ")" ^ string_of_fragment frag |> Util.cyan |> Util.clear)) + | AV_vector (avals, typ) -> + pp_annot typ (string "[" ^^ separate_map (comma ^^ space) pp_aval avals ^^ string "]") + | AV_list (avals, typ) -> + pp_annot typ (string "[|" ^^ separate_map (comma ^^ space) pp_aval avals ^^ string "|]") + | AV_record (fields, typ) -> + pp_annot typ (string "struct {" + ^^ separate_map (comma ^^ space) (fun (id, field) -> pp_id id ^^ string " = " ^^ pp_aval field) (Bindings.bindings fields) + ^^ string "}") + +let ae_lit lit typ = AE_val (AV_lit (lit, typ)) + +let is_dead_aexp (AE_aux (_, env, _)) = prove __POS__ env nc_false + +(** GLOBAL: gensym_counter is used to generate fresh identifiers where + needed. It should be safe to reset between top level + definitions. **) +let gensym_counter = ref 0 + +let gensym () = + let id = mk_id ("gs#" ^ string_of_int !gensym_counter) in + incr gensym_counter; + id + +let rec split_block l = function + | [exp] -> [], exp + | exp :: exps -> + let exps, last = split_block l exps in + exp :: exps, last + | [] -> + raise (Reporting.err_unreachable l __POS__ "empty block found when converting to ANF") + +let rec anf_pat ?global:(global=false) (P_aux (p_aux, annot) as pat) = + let mk_apat aux = AP_aux (aux, env_of_annot annot, fst annot) in + match p_aux with + | P_id id when global -> mk_apat (AP_global (id, typ_of_pat pat)) + | P_id id -> mk_apat (AP_id (id, typ_of_pat pat)) + | P_wild -> mk_apat (AP_wild (typ_of_pat pat)) + | P_tup pats -> mk_apat (AP_tup (List.map (fun pat -> anf_pat ~global:global pat) pats)) + | P_app (id, [subpat]) -> mk_apat (AP_app (id, anf_pat ~global:global subpat, typ_of_pat pat)) + | P_app (id, pats) -> mk_apat (AP_app (id, mk_apat (AP_tup (List.map (fun pat -> anf_pat ~global:global pat) pats)), typ_of_pat pat)) + | P_typ (_, pat) -> anf_pat ~global:global pat + | P_var (pat, _) -> anf_pat ~global:global pat + | P_cons (hd_pat, tl_pat) -> mk_apat (AP_cons (anf_pat ~global:global hd_pat, anf_pat ~global:global tl_pat)) + | P_list pats -> List.fold_right (fun pat apat -> mk_apat (AP_cons (anf_pat ~global:global pat, apat))) pats (mk_apat (AP_nil (typ_of_pat pat))) + | P_lit (L_aux (L_unit, _)) -> mk_apat (AP_wild (typ_of_pat pat)) + | _ -> + raise (Reporting.err_unreachable (fst annot) __POS__ + ("Could not convert pattern to ANF: " ^ string_of_pat pat)) + +let rec apat_globals (AP_aux (aux, _, _)) = + match aux with + | AP_nil _ | AP_wild _ | AP_id _ -> [] + | AP_global (id, typ) -> [(id, typ)] + | AP_tup apats -> List.concat (List.map apat_globals apats) + | AP_app (_, apat, _) -> apat_globals apat + | AP_cons (hd_apat, tl_apat) -> apat_globals hd_apat @ apat_globals tl_apat + +let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) = + let mk_aexp aexp = AE_aux (aexp, env_of_annot exp_annot, l) in + + let to_aval (AE_aux (aexp_aux, env, l) as aexp) = + let mk_aexp aexp = AE_aux (aexp, env, l) in + match aexp_aux with + | AE_val v -> (v, fun x -> x) + | AE_short_circuit (_, _, _) -> + let id = gensym () in + (AV_id (id, Local (Immutable, bool_typ)), fun x -> mk_aexp (AE_let (Immutable, id, bool_typ, aexp, x, typ_of exp))) + | AE_app (_, _, typ) + | AE_let (_, _, _, _, _, typ) + | AE_return (_, typ) + | AE_throw (_, typ) + | AE_cast (_, typ) + | AE_if (_, _, _, typ) + | AE_field (_, _, typ) + | AE_case (_, _, typ) + | AE_try (_, _, typ) + | AE_record_update (_, _, typ) + | AE_block (_, _, typ) -> + let id = gensym () in + (AV_id (id, Local (Immutable, typ)), fun x -> mk_aexp (AE_let (Immutable, id, typ, aexp, x, typ_of exp))) + | AE_assign _ | AE_for _ | AE_loop _ -> + let id = gensym () in + (AV_id (id, Local (Immutable, unit_typ)), fun x -> mk_aexp (AE_let (Immutable, id, unit_typ, aexp, x, typ_of exp))) + in + match e_aux with + | E_lit lit -> mk_aexp (ae_lit lit (typ_of exp)) + + | E_block [] -> + Util.warn (Reporting.loc_to_string l + ^ "\n\nTranslating empty block (possibly assigning to an uninitialized variable at the end of a block?)"); + mk_aexp (ae_lit (L_aux (L_unit, l)) (typ_of exp)) + | E_block exps -> + let exps, last = split_block l exps in + let aexps = List.map anf exps in + let alast = anf last in + mk_aexp (AE_block (aexps, alast, typ_of exp)) + + | E_assign (LEXP_aux (LEXP_deref dexp, _), exp) -> + let gs = gensym () in + mk_aexp (AE_let (Mutable, gs, typ_of dexp, anf dexp, mk_aexp (AE_assign (gs, typ_of dexp, anf exp)), unit_typ)) + + | E_assign (LEXP_aux (LEXP_id id, _), exp) + | E_assign (LEXP_aux (LEXP_cast (_, id), _), exp) -> + let aexp = anf exp in + mk_aexp (AE_assign (id, lvar_typ (Env.lookup_id id (env_of exp)), aexp)) + + | E_assign (lexp, _) -> + raise (Reporting.err_unreachable l __POS__ + ("Encountered complex l-expression " ^ string_of_lexp lexp ^ " when converting to ANF")) + + | E_loop (loop_typ, cond, exp) -> + let acond = anf cond in + let aexp = anf exp in + mk_aexp (AE_loop (loop_typ, acond, aexp)) + + | E_for (id, exp1, exp2, exp3, order, body) -> + let aexp1, aexp2, aexp3, abody = anf exp1, anf exp2, anf exp3, anf body in + mk_aexp (AE_for (id, aexp1, aexp2, aexp3, order, abody)) + + | E_if (cond, then_exp, else_exp) -> + let cond_val, wrap = to_aval (anf cond) in + let then_aexp = anf then_exp in + let else_aexp = anf else_exp in + wrap (mk_aexp (AE_if (cond_val, then_aexp, else_aexp, typ_of exp))) + + | E_app_infix (x, Id_aux (Id op, l), y) -> + anf (E_aux (E_app (Id_aux (DeIid op, l), [x; y]), exp_annot)) + | E_app_infix (x, Id_aux (DeIid op, l), y) -> + anf (E_aux (E_app (Id_aux (Id op, l), [x; y]), exp_annot)) + + | E_vector exps -> + let aexps = List.map anf exps in + let avals = List.map to_aval aexps in + let wrap = List.fold_left (fun f g x -> f (g x)) (fun x -> x) (List.map snd avals) in + wrap (mk_aexp (AE_val (AV_vector (List.map fst avals, typ_of exp)))) + + | E_list exps -> + let aexps = List.map anf exps in + let avals = List.map to_aval aexps in + let wrap = List.fold_left (fun f g x -> f (g x)) (fun x -> x) (List.map snd avals) in + wrap (mk_aexp (AE_val (AV_list (List.map fst avals, typ_of exp)))) + + | E_field (field_exp, id) -> + let aval, wrap = to_aval (anf field_exp) in + wrap (mk_aexp (AE_field (aval, id, typ_of exp))) + + | E_record_update (exp, fexps) -> + let anf_fexp (FE_aux (FE_Fexp (id, exp), _)) = + let aval, wrap = to_aval (anf exp) in + (id, aval), wrap + in + let aval, exp_wrap = to_aval (anf exp) in + let fexps = List.map anf_fexp fexps in + let wrap = List.fold_left (fun f g x -> f (g x)) (fun x -> x) (List.map snd fexps) in + let record = List.fold_left (fun r (id, aval) -> Bindings.add id aval r) Bindings.empty (List.map fst fexps) in + exp_wrap (wrap (mk_aexp (AE_record_update (aval, record, typ_of exp)))) + + | E_app (id, [exp1; exp2]) when string_of_id id = "and_bool" -> + let aexp1 = anf exp1 in + let aexp2 = anf exp2 in + let aval1, wrap = to_aval aexp1 in + wrap (mk_aexp (AE_short_circuit (SC_and, aval1, aexp2))) + + | E_app (id, [exp1; exp2]) when string_of_id id = "or_bool" -> + let aexp1 = anf exp1 in + let aexp2 = anf exp2 in + let aval1, wrap = to_aval aexp1 in + wrap (mk_aexp (AE_short_circuit (SC_or, aval1, aexp2))) + + | E_app (id, exps) -> + let aexps = List.map anf exps in + let avals = List.map to_aval aexps in + let wrap = List.fold_left (fun f g x -> f (g x)) (fun x -> x) (List.map snd avals) in + wrap (mk_aexp (AE_app (id, List.map fst avals, typ_of exp))) + + | E_throw exn_exp -> + let aexp = anf exn_exp in + let aval, wrap = to_aval aexp in + wrap (mk_aexp (AE_throw (aval, typ_of exp))) + + | E_exit exp -> + let aexp = anf exp in + let aval, wrap = to_aval aexp in + wrap (mk_aexp (AE_app (mk_id "sail_exit", [aval], unit_typ))) + + | E_return ret_exp -> + let aexp = anf ret_exp in + let aval, wrap = to_aval aexp in + wrap (mk_aexp (AE_return (aval, typ_of exp))) + + | E_assert (exp1, exp2) -> + let aexp1 = anf exp1 in + let aexp2 = anf exp2 in + let aval1, wrap1 = to_aval aexp1 in + let aval2, wrap2 = to_aval aexp2 in + wrap1 (wrap2 (mk_aexp (AE_app (mk_id "sail_assert", [aval1; aval2], unit_typ)))) + + | E_cons (exp1, exp2) -> + let aexp1 = anf exp1 in + let aexp2 = anf exp2 in + let aval1, wrap1 = to_aval aexp1 in + let aval2, wrap2 = to_aval aexp2 in + wrap1 (wrap2 (mk_aexp (AE_app (mk_id "cons", [aval1; aval2], unit_typ)))) + + | E_id id -> + let lvar = Env.lookup_id id (env_of exp) in + begin match lvar with + | _ -> mk_aexp (AE_val (AV_id (id, lvar))) + end + + | E_ref id -> + let lvar = Env.lookup_id id (env_of exp) in + mk_aexp (AE_val (AV_ref (id, lvar))) + + | E_case (match_exp, pexps) -> + let match_aval, match_wrap = to_aval (anf match_exp) in + let anf_pexp (Pat_aux (pat_aux, _)) = + match pat_aux with + | Pat_when (pat, guard, body) -> + (anf_pat pat, anf guard, anf body) + | Pat_exp (pat, body) -> + (anf_pat pat, mk_aexp (AE_val (AV_lit (mk_lit (L_true), bool_typ))), anf body) + in + match_wrap (mk_aexp (AE_case (match_aval, List.map anf_pexp pexps, typ_of exp))) + + | E_try (match_exp, pexps) -> + let match_aexp = anf match_exp in + let anf_pexp (Pat_aux (pat_aux, _)) = + match pat_aux with + | Pat_when (pat, guard, body) -> + (anf_pat pat, anf guard, anf body) + | Pat_exp (pat, body) -> + (anf_pat pat, mk_aexp (AE_val (AV_lit (mk_lit (L_true), bool_typ))), anf body) + in + mk_aexp (AE_try (match_aexp, List.map anf_pexp pexps, typ_of exp)) + + | E_var (LEXP_aux (LEXP_id id, _), binding, body) + | E_var (LEXP_aux (LEXP_cast (_, id), _), binding, body) + | E_let (LB_aux (LB_val (P_aux (P_id id, _), binding), _), body) -> + let env = env_of body in + let lvar = Env.lookup_id id env in + mk_aexp (AE_let (Mutable, id, lvar_typ lvar, anf binding, anf body, typ_of exp)) + + | E_var (lexp, _, _) -> + raise (Reporting.err_unreachable l __POS__ + ("Encountered complex l-expression " ^ string_of_lexp lexp ^ " when converting to ANF")) + + | E_let (LB_aux (LB_val (pat, binding), _), body) -> + anf (E_aux (E_case (binding, [Pat_aux (Pat_exp (pat, body), (Parse_ast.Unknown, empty_tannot))]), exp_annot)) + + | E_tuple exps -> + let aexps = List.map anf exps in + let avals = List.map to_aval aexps in + let wrap = List.fold_left (fun f g x -> f (g x)) (fun x -> x) (List.map snd avals) in + wrap (mk_aexp (AE_val (AV_tuple (List.map fst avals)))) + + | E_record fexps -> + let anf_fexp (FE_aux (FE_Fexp (id, exp), _)) = + let aval, wrap = to_aval (anf exp) in + (id, aval), wrap + in + let fexps = List.map anf_fexp fexps in + let wrap = List.fold_left (fun f g x -> f (g x)) (fun x -> x) (List.map snd fexps) in + let record = List.fold_left (fun r (id, aval) -> Bindings.add id aval r) Bindings.empty (List.map fst fexps) in + wrap (mk_aexp (AE_val (AV_record (record, typ_of exp)))) + + | E_cast (typ, exp) -> mk_aexp (AE_cast (anf exp, typ)) + + | E_vector_access _ | E_vector_subrange _ | E_vector_update _ | E_vector_update_subrange _ | E_vector_append _ -> + (* Should be re-written by type checker *) + raise (Reporting.err_unreachable l __POS__ "encountered raw vector operation when converting to ANF") + + | E_internal_value _ -> + (* Interpreter specific *) + raise (Reporting.err_unreachable l __POS__ "encountered E_internal_value when converting to ANF") + + | E_sizeof nexp -> + (* Sizeof nodes removed by sizeof rewriting pass *) + raise (Reporting.err_unreachable l __POS__ ("encountered E_sizeof node " ^ string_of_nexp nexp ^ " when converting to ANF")) + + | E_constraint _ -> + (* Sizeof nodes removed by sizeof rewriting pass *) + raise (Reporting.err_unreachable l __POS__ "encountered E_constraint node when converting to ANF") + + | E_nondet _ -> + (* We don't compile E_nondet nodes *) + raise (Reporting.err_unreachable l __POS__ "encountered E_nondet node when converting to ANF") + + | E_internal_return _ | E_internal_plet _ -> + raise (Reporting.err_unreachable l __POS__ "encountered unexpected internal node when converting to ANF") diff --git a/src/jib/anf.mli b/src/jib/anf.mli new file mode 100644 index 00000000..79fb35ca --- /dev/null +++ b/src/jib/anf.mli @@ -0,0 +1,161 @@ +(**************************************************************************) +(* 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. *) +(**************************************************************************) + +(** The A-normal form (ANF) grammar *) + +open Ast +open Ast_util +open Jib +open Type_check + +(** The first step in compiling Sail is converting the Sail expression + grammar into A-normal form (ANF). Essentially this converts + expressions such as [f(g(x), h(y))] into something like: + + [let v0 = g(x) in let v1 = h(x) in f(v0, v1)] + + Essentially the arguments to every function must be trivial, and + complex expressions must be let bound to new variables, or used in + a block, assignment, or control flow statement (if, for, and + while/until loops). The aexp datatype represents these expressions, + while aval represents the trivial values. + + The convention is that the type of an aexp is given by last + argument to a constructor. It is omitted where it is obvious - for + example all for loops have unit as their type. If some constituent + part of the aexp has an annotation, the it refers to the previous + argument, so in + + [AE_let (id, typ1, _, body, typ2)] + + [typ1] is the type of the bound identifer, whereas [typ2] is the type + of the whole let expression (and therefore also the body). + + See Flanagan et al's {e The Essence of Compiling with Continuations}. + *) + +type 'a aexp = AE_aux of 'a aexp_aux * Env.t * l + +and 'a aexp_aux = + | AE_val of 'a aval + | AE_app of id * ('a aval) list * 'a + | AE_cast of 'a aexp * 'a + | AE_assign of id * 'a * 'a aexp + | AE_let of mut * id * 'a * 'a aexp * 'a aexp * 'a + | AE_block of ('a aexp) list * 'a aexp * 'a + | AE_return of 'a aval * 'a + | AE_throw of 'a aval * 'a + | AE_if of 'a aval * 'a aexp * 'a aexp * 'a + | AE_field of 'a aval * id * 'a + | AE_case of 'a aval * ('a apat * 'a aexp * 'a aexp) list * 'a + | AE_try of 'a aexp * ('a apat * 'a aexp * 'a aexp) list * 'a + | AE_record_update of 'a aval * ('a aval) Bindings.t * 'a + | AE_for of id * 'a aexp * 'a aexp * 'a aexp * order * 'a aexp + | AE_loop of loop * 'a aexp * 'a aexp + | AE_short_circuit of sc_op * 'a aval * 'a aexp + +and sc_op = SC_and | SC_or + +and 'a apat = AP_aux of 'a apat_aux * Env.t * l + +and 'a apat_aux = + | AP_tup of ('a apat) list + | AP_id of id * 'a + | AP_global of id * 'a + | AP_app of id * 'a apat * 'a + | AP_cons of 'a apat * 'a apat + | AP_nil of 'a + | AP_wild of 'a + +(** We allow ANF->ANF optimization to insert fragments of C code + directly in the ANF grammar via [AV_C_fragment]. Such fragments + must be side-effect free expressions. *) +and 'a aval = + | AV_lit of lit * 'a + | AV_id of id * 'a lvar + | AV_ref of id * 'a lvar + | AV_tuple of ('a aval) list + | AV_list of ('a aval) list * 'a + | AV_vector of ('a aval) list * 'a + | AV_record of ('a aval) Bindings.t * 'a + | AV_C_fragment of fragment * 'a * ctyp + +(** Function for generating unique identifiers during ANF + translation. *) +val gensym : unit -> id + +(** {2 Functions for transforming ANF expressions} *) + +(** Map over all values in an ANF expression *) +val map_aval : (Env.t -> Ast.l -> 'a aval -> 'a aval) -> 'a aexp -> 'a aexp + +(** Map over all function calls in an ANF expression *) +val map_functions : (Env.t -> Ast.l -> id -> ('a aval) list -> 'a -> 'a aexp_aux) -> 'a aexp -> 'a aexp + +(** Remove all variable shadowing in an ANF expression *) +val no_shadow : IdSet.t -> 'a aexp -> 'a aexp + +val apat_globals : 'a apat -> (id * 'a) list +val apat_types : 'a apat -> 'a Bindings.t + +(** Returns true if an ANF expression is dead due to flow typing + implying it is unreachable. Note: This function calls SMT. *) +val is_dead_aexp : 'a aexp -> bool + +(** {2 Compiling to ANF expressions} *) + +val anf_pat : ?global:bool -> tannot pat -> typ apat + +val anf : tannot exp -> typ aexp + +(** {2 Pretty printing ANF expressions} *) + +val pp_aval : typ aval -> PPrint.document +val pp_aexp : typ aexp -> PPrint.document diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml new file mode 100644 index 00000000..846b619f --- /dev/null +++ b/src/jib/c_backend.ml @@ -0,0 +1,2324 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* Alasdair Armstrong *) +(* Brian Campbell *) +(* Thomas Bauereiss *) +(* Anthony Fox *) +(* Jon French *) +(* Dominic Mulligan *) +(* Stephen Kell *) +(* Mark Wassell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + +open Ast +open Ast_util +open Jib +open Jib_compile +open Jib_util +open Type_check +open PPrint +open Value2 + +open Anf + +module Big_int = Nat_big_num + +let c_verbosity = ref 0 + +let opt_static = ref false +let opt_no_main = ref false +let opt_memo_cache = ref false +let opt_no_rts = ref false +let opt_prefix = ref "z" +let opt_extra_params = ref None +let opt_extra_arguments = ref None + +let extra_params () = + match !opt_extra_params with + | Some str -> str ^ ", " + | _ -> "" + +let extra_arguments is_extern = + match !opt_extra_arguments with + | Some str when not is_extern -> str ^ ", " + | _ -> "" + +(* Optimization flags *) +let optimize_primops = ref false +let optimize_hoist_allocations = ref false +let optimize_struct_updates = ref false +let optimize_alias = ref false +let optimize_experimental = ref false + +let c_debug str = + if !c_verbosity > 0 then prerr_endline (Lazy.force str) else () + +let c_error ?loc:(l=Parse_ast.Unknown) message = + raise (Reporting.err_general l ("\nC backend: " ^ message)) + +let zencode_id = function + | Id_aux (Id str, l) -> Id_aux (Id (Util.zencode_string str), l) + | Id_aux (DeIid str, l) -> Id_aux (Id (Util.zencode_string ("op " ^ str)), l) + +(**************************************************************************) +(* 2. Converting sail types to C types *) +(**************************************************************************) + +let max_int n = Big_int.pred (Big_int.pow_int_positive 2 (n - 1)) +let min_int n = Big_int.negate (Big_int.pow_int_positive 2 (n - 1)) + +(** Convert a sail type into a C-type. This function can be quite + slow, because it uses ctx.local_env and SMT to analyse the Sail + types and attempts to fit them into the smallest possible C + types, provided ctx.optimize_smt is true (default) **) +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_bit + | Typ_id id when string_of_id id = "bool" -> CT_bool + | Typ_id id when string_of_id id = "int" -> CT_lint + | Typ_id id when string_of_id id = "nat" -> CT_lint + | Typ_id id when string_of_id id = "unit" -> CT_unit + | Typ_id id when string_of_id id = "string" -> CT_string + | Typ_id id when string_of_id id = "real" -> CT_real + + | Typ_app (id, _) when string_of_id id = "atom_bool" -> CT_bool + + | Typ_app (id, args) when string_of_id id = "itself" -> + ctyp_of_typ ctx (Typ_aux (Typ_app (mk_id "atom", args), l)) + | Typ_app (id, _) when string_of_id id = "range" || string_of_id id = "atom" || string_of_id id = "implicit" -> + begin match destruct_range Env.empty typ with + | None -> assert false (* Checked if range type in guard *) + | Some (kids, constr, n, m) -> + let ctx = { ctx with local_env = add_existential Parse_ast.Unknown (List.map (mk_kopt K_int) kids) constr ctx.local_env } in + match nexp_simp n, nexp_simp m with + | Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_constant m, _) + when Big_int.less_equal (min_int 64) n && Big_int.less_equal m (max_int 64) -> + CT_fint 64 + | n, m -> + if prove __POS__ ctx.local_env (nc_lteq (nconstant (min_int 64)) n) && prove __POS__ ctx.local_env (nc_lteq m (nconstant (max_int 64))) then + CT_fint 64 + else + CT_lint + end + + | Typ_app (id, [A_aux (A_typ typ, _)]) when string_of_id id = "list" -> + CT_list (ctyp_of_typ ctx typ) + + (* When converting a sail bitvector type into C, we have three options in order of efficiency: + - If the length is obviously static and smaller than 64, use the fixed bits type (aka uint64_t), fbits. + - If the length is less than 64, then use a small bits type, sbits. + - If the length may be larger than 64, use a large bits type lbits. *) + | Typ_app (id, [A_aux (A_nexp n, _); + A_aux (A_order ord, _); + A_aux (A_typ (Typ_aux (Typ_id vtyp_id, _)), _)]) + when string_of_id id = "vector" && string_of_id vtyp_id = "bit" -> + let direction = match ord with Ord_aux (Ord_dec, _) -> true | Ord_aux (Ord_inc, _) -> false | _ -> assert false in + begin match nexp_simp n with + | Nexp_aux (Nexp_constant n, _) when Big_int.less_equal n (Big_int.of_int 64) -> CT_fbits (Big_int.to_int n, direction) + | n when prove __POS__ ctx.local_env (nc_lteq n (nint 64)) -> CT_sbits (64, direction) + | _ -> CT_lbits direction + end + + | Typ_app (id, [A_aux (A_nexp n, _); + A_aux (A_order ord, _); + A_aux (A_typ typ, _)]) + when string_of_id id = "vector" -> + let direction = match ord with Ord_aux (Ord_dec, _) -> true | Ord_aux (Ord_inc, _) -> false | _ -> assert false in + CT_vector (direction, ctyp_of_typ ctx typ) + + | Typ_app (id, [A_aux (A_typ typ, _)]) when string_of_id id = "register" -> + CT_ref (ctyp_of_typ ctx typ) + + | 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) + + | Typ_exist _ -> + (* Use Type_check.destruct_exist when optimising with SMT, to + ensure that we don't cause any type variable clashes in + local_env, and that we can optimize the existential based upon + it's constraints. *) + begin match destruct_exist (Env.expand_synonyms ctx.local_env typ) with + | Some (kids, nc, typ) -> + let env = add_existential l kids nc ctx.local_env in + ctyp_of_typ { ctx with local_env = env } typ + | None -> raise (Reporting.err_unreachable l __POS__ "Existential cannot be destructured!") + end + + | Typ_var kid -> CT_poly + + | _ -> c_error ~loc:l ("No C type for type " ^ string_of_typ typ) + +let rec is_stack_ctyp ctyp = match ctyp with + | CT_fbits _ | CT_sbits _ | CT_bit | CT_unit | CT_bool | CT_enum _ -> true + | CT_fint n -> n <= 64 + | CT_lbits _ | CT_lint | CT_real | CT_string | CT_list _ | CT_vector _ -> false + | CT_struct (_, fields) -> List.for_all (fun (_, ctyp) -> is_stack_ctyp ctyp) fields + | CT_variant (_, ctors) -> false (* List.for_all (fun (_, ctyp) -> is_stack_ctyp ctyp) ctors *) (* FIXME *) + | CT_tup ctyps -> List.for_all is_stack_ctyp ctyps + | CT_ref ctyp -> true + | CT_poly -> true + +let is_stack_typ ctx typ = is_stack_ctyp (ctyp_of_typ ctx typ) + +let is_fbits_typ ctx typ = + match ctyp_of_typ ctx typ with + | CT_fbits _ -> true + | _ -> false + +let is_sbits_typ ctx typ = + match ctyp_of_typ ctx typ with + | CT_sbits _ -> true + | _ -> false + +let ctor_bindings = List.fold_left (fun map (id, ctyp) -> Bindings.add id ctyp map) Bindings.empty + +(**************************************************************************) +(* 3. Optimization of primitives and literals *) +(**************************************************************************) + +let hex_char = + let open Sail2_values in + function + | '0' -> [B0; B0; B0; B0] + | '1' -> [B0; B0; B0; B1] + | '2' -> [B0; B0; B1; B0] + | '3' -> [B0; B0; B1; B1] + | '4' -> [B0; B1; B0; B0] + | '5' -> [B0; B1; B0; B1] + | '6' -> [B0; B1; B1; B0] + | '7' -> [B0; B1; B1; B1] + | '8' -> [B1; B0; B0; B0] + | '9' -> [B1; B0; B0; B1] + | 'A' | 'a' -> [B1; B0; B1; B0] + | 'B' | 'b' -> [B1; B0; B1; B1] + | 'C' | 'c' -> [B1; B1; B0; B0] + | 'D' | 'd' -> [B1; B1; B0; B1] + | 'E' | 'e' -> [B1; B1; B1; B0] + | 'F' | 'f' -> [B1; B1; B1; B1] + | _ -> failwith "Invalid hex character" + +let literal_to_fragment (L_aux (l_aux, _) as lit) = + match l_aux with + | L_num n when Big_int.less_equal (min_int 64) n && Big_int.less_equal n (max_int 64) -> + Some (F_lit (V_int n), CT_fint 64) + | L_hex str when String.length str <= 16 -> + let padding = 16 - String.length str in + let padding = Util.list_init padding (fun _ -> Sail2_values.B0) in + let content = Util.string_to_list str |> List.map hex_char |> List.concat in + Some (F_lit (V_bits (padding @ content)), CT_fbits (String.length str * 4, true)) + | L_unit -> Some (F_lit V_unit, CT_unit) + | L_true -> Some (F_lit (V_bool true), CT_bool) + | L_false -> Some (F_lit (V_bool false), CT_bool) + | _ -> None + +let c_literals ctx = + let rec c_literal env l = function + | AV_lit (lit, typ) as v when is_stack_ctyp (ctyp_of_typ { ctx with local_env = env } typ) -> + begin + match literal_to_fragment lit with + | Some (frag, ctyp) -> AV_C_fragment (frag, typ, ctyp) + | None -> v + end + | AV_tuple avals -> AV_tuple (List.map (c_literal env l) avals) + | v -> v + in + map_aval c_literal + +let mask m = + if Big_int.less_equal m (Big_int.of_int 64) then + let n = Big_int.to_int m in + if n = 0 then + "UINT64_C(0)" + else if n mod 4 = 0 then + "UINT64_C(0x" ^ String.make (16 - n / 4) '0' ^ String.make (n / 4) 'F' ^ ")" + else + "UINT64_C(" ^ String.make (64 - n) '0' ^ String.make n '1' ^ ")" + else + failwith "Tried to create a mask literal for a vector greater than 64 bits." + +let rec is_bitvector = function + | [] -> true + | AV_lit (L_aux (L_zero, _), _) :: avals -> is_bitvector avals + | AV_lit (L_aux (L_one, _), _) :: avals -> is_bitvector avals + | _ :: _ -> false + +let rec value_of_aval_bit = function + | AV_lit (L_aux (L_zero, _), _) -> Sail2_values.B0 + | AV_lit (L_aux (L_one, _), _) -> Sail2_values.B1 + | _ -> assert false + +let rec c_aval ctx = function + | AV_lit (lit, typ) as v -> + begin + match literal_to_fragment lit with + | Some (frag, ctyp) -> AV_C_fragment (frag, typ, ctyp) + | None -> v + end + | AV_C_fragment (str, typ, ctyp) -> AV_C_fragment (str, typ, ctyp) + (* An id can be converted to a C fragment if it's type can be + stack-allocated. *) + | AV_id (id, lvar) as v -> + begin + match lvar with + | Local (_, typ) -> + let ctyp = ctyp_of_typ ctx typ in + if is_stack_ctyp ctyp then + begin + try + (* We need to check that id's type hasn't changed due to flow typing *) + let _, ctyp' = Bindings.find id ctx.locals in + if ctyp_equal ctyp ctyp' then + AV_C_fragment (F_id id, typ, ctyp) + else + (* id's type changed due to flow + typing, so it's really still heap allocated! *) + v + with + (* Hack: Assuming global letbindings don't change from flow typing... *) + Not_found -> AV_C_fragment (F_id id, typ, ctyp) + end + else + v + | Register (_, _, typ) when is_stack_typ ctx typ -> + let ctyp = ctyp_of_typ ctx typ in + if is_stack_ctyp ctyp then + AV_C_fragment (F_id id, typ, ctyp) + else + v + | _ -> v + end + | AV_vector (v, typ) when is_bitvector v && List.length v <= 64 -> + let bitstring = F_lit (V_bits (List.map value_of_aval_bit v)) in + AV_C_fragment (bitstring, typ, CT_fbits (List.length v, true)) + | AV_tuple avals -> AV_tuple (List.map (c_aval ctx) avals) + | aval -> aval + +let is_c_fragment = function + | AV_C_fragment _ -> true + | _ -> false + +let c_fragment = function + | AV_C_fragment (frag, _, _) -> frag + | _ -> assert false + +let v_mask_lower i = F_lit (V_bits (Util.list_init i (fun _ -> Sail2_values.B1))) + +(* Map over all the functions in an aexp. *) +let rec analyze_functions ctx f (AE_aux (aexp, env, l)) = + let ctx = { ctx with local_env = env } in + let aexp = match aexp with + | AE_app (id, vs, typ) -> f ctx id vs typ + + | AE_cast (aexp, typ) -> AE_cast (analyze_functions ctx f aexp, typ) + + | AE_assign (id, typ, aexp) -> AE_assign (id, typ, analyze_functions ctx f aexp) + + | AE_short_circuit (op, aval, aexp) -> AE_short_circuit (op, aval, analyze_functions ctx f aexp) + + | AE_let (mut, id, typ1, aexp1, (AE_aux (_, env2, _) as aexp2), typ2) -> + let aexp1 = analyze_functions ctx f aexp1 in + (* Use aexp2's environment because it will contain constraints for id *) + let ctyp1 = ctyp_of_typ { ctx with local_env = env2 } typ1 in + let ctx = { ctx with locals = Bindings.add id (mut, ctyp1) ctx.locals } in + AE_let (mut, id, typ1, aexp1, analyze_functions ctx f aexp2, typ2) + + | AE_block (aexps, aexp, typ) -> AE_block (List.map (analyze_functions ctx f) aexps, analyze_functions ctx f aexp, typ) + + | AE_if (aval, aexp1, aexp2, typ) -> + AE_if (aval, analyze_functions ctx f aexp1, analyze_functions ctx f aexp2, typ) + + | AE_loop (loop_typ, aexp1, aexp2) -> AE_loop (loop_typ, analyze_functions ctx f aexp1, analyze_functions ctx f aexp2) + + | AE_for (id, aexp1, aexp2, aexp3, order, aexp4) -> + let aexp1 = analyze_functions ctx f aexp1 in + let aexp2 = analyze_functions ctx f aexp2 in + let aexp3 = analyze_functions ctx f aexp3 in + let aexp4 = analyze_functions ctx f aexp4 in + (* Currently we assume that loop indexes are always safe to put into an int64 *) + let ctx = { ctx with locals = Bindings.add id (Immutable, CT_fint 64) ctx.locals } in + AE_for (id, aexp1, aexp2, aexp3, order, aexp4) + + | AE_case (aval, cases, typ) -> + let analyze_case (AP_aux (_, env, _) as pat, aexp1, aexp2) = + let pat_bindings = Bindings.bindings (apat_types pat) in + let ctx = { ctx with local_env = env } in + let ctx = + List.fold_left (fun ctx (id, typ) -> { ctx with locals = Bindings.add id (Immutable, ctyp_of_typ ctx typ) ctx.locals }) ctx pat_bindings + in + pat, analyze_functions ctx f aexp1, analyze_functions ctx f aexp2 + in + AE_case (aval, List.map analyze_case cases, typ) + + | AE_try (aexp, cases, typ) -> + AE_try (analyze_functions ctx f aexp, List.map (fun (pat, aexp1, aexp2) -> pat, analyze_functions ctx f aexp1, analyze_functions ctx f aexp2) cases, typ) + + | AE_field _ | AE_record_update _ | AE_val _ | AE_return _ | AE_throw _ as v -> v + in + AE_aux (aexp, env, l) + +let analyze_primop' ctx id args typ = + let no_change = AE_app (id, args, typ) in + let args = List.map (c_aval ctx) args in + let extern = if Env.is_extern id ctx.tc_env "c" then Env.get_extern id ctx.tc_env "c" else failwith "Not extern" in + + let v_one = F_lit (V_int (Big_int.of_int 1)) in + let v_int n = F_lit (V_int (Big_int.of_int n)) in + + c_debug (lazy ("Analyzing primop " ^ extern ^ "(" ^ Util.string_of_list ", " (fun aval -> Pretty_print_sail.to_string (pp_aval aval)) args ^ ")")); + + match extern, args with + | "eq_bits", [AV_C_fragment (v1, _, CT_fbits _); AV_C_fragment (v2, _, _)] -> + AE_val (AV_C_fragment (F_op (v1, "==", v2), typ, CT_bool)) + | "eq_bits", [AV_C_fragment (v1, _, CT_sbits _); AV_C_fragment (v2, _, _)] -> + AE_val (AV_C_fragment (F_call ("eq_sbits", [v1; v2]), typ, CT_bool)) + + | "neq_bits", [AV_C_fragment (v1, _, CT_fbits _); AV_C_fragment (v2, _, _)] -> + AE_val (AV_C_fragment (F_op (v1, "!=", v2), typ, CT_bool)) + | "neq_bits", [AV_C_fragment (v1, _, CT_sbits _); AV_C_fragment (v2, _, _)] -> + AE_val (AV_C_fragment (F_call ("neq_sbits", [v1; v2]), typ, CT_bool)) + + | "eq_int", [AV_C_fragment (v1, typ1, _); AV_C_fragment (v2, typ2, _)] -> + AE_val (AV_C_fragment (F_op (v1, "==", v2), typ, CT_bool)) + + | "zeros", [_] -> + begin match destruct_vector ctx.tc_env typ with + | Some (Nexp_aux (Nexp_constant n, _), _, Typ_aux (Typ_id id, _)) + when string_of_id id = "bit" && Big_int.less_equal n (Big_int.of_int 64) -> + AE_val (AV_C_fragment (F_raw "0x0", typ, CT_fbits (Big_int.to_int n, true))) + | _ -> no_change + end + + | "zero_extend", [AV_C_fragment (v1, _, CT_fbits _); _] -> + begin match destruct_vector ctx.tc_env typ with + | Some (Nexp_aux (Nexp_constant n, _), _, Typ_aux (Typ_id id, _)) + when string_of_id id = "bit" && Big_int.less_equal n (Big_int.of_int 64) -> + AE_val (AV_C_fragment (v1, typ, CT_fbits (Big_int.to_int n, true))) + | _ -> no_change + end + + | "zero_extend", [AV_C_fragment (v1, _, CT_sbits _); _] -> + begin match destruct_vector ctx.tc_env typ with + | Some (Nexp_aux (Nexp_constant n, _), _, Typ_aux (Typ_id id, _)) + when string_of_id id = "bit" && Big_int.less_equal n (Big_int.of_int 64) -> + AE_val (AV_C_fragment (F_call ("fast_zero_extend", [v1; v_int (Big_int.to_int n)]), typ, CT_fbits (Big_int.to_int n, true))) + | _ -> no_change + end + + | "sign_extend", [AV_C_fragment (v1, _, CT_fbits (n, _)); _] -> + begin match destruct_vector ctx.tc_env typ with + | Some (Nexp_aux (Nexp_constant m, _), _, Typ_aux (Typ_id id, _)) + when string_of_id id = "bit" && Big_int.less_equal m (Big_int.of_int 64) -> + AE_val (AV_C_fragment (F_call ("fast_sign_extend", [v1; v_int n; v_int (Big_int.to_int m)]) , typ, CT_fbits (Big_int.to_int m, true))) + | _ -> no_change + end + + | "sign_extend", [AV_C_fragment (v1, _, CT_sbits _); _] -> + begin match destruct_vector ctx.tc_env typ with + | Some (Nexp_aux (Nexp_constant m, _), _, Typ_aux (Typ_id id, _)) + when string_of_id id = "bit" && Big_int.less_equal m (Big_int.of_int 64) -> + AE_val (AV_C_fragment (F_call ("fast_sign_extend2", [v1; v_int (Big_int.to_int m)]) , typ, CT_fbits (Big_int.to_int m, true))) + | _ -> no_change + end + + | "add_bits", [AV_C_fragment (v1, _, CT_fbits (n, ord)); AV_C_fragment (v2, _, CT_fbits _)] + when n <= 63 -> + AE_val (AV_C_fragment (F_op (F_op (v1, "+", v2), "&", v_mask_lower n), typ, CT_fbits (n, ord))) + + | "lteq", [AV_C_fragment (v1, _, _); AV_C_fragment (v2, _, _)] -> + AE_val (AV_C_fragment (F_op (v1, "<=", v2), typ, CT_bool)) + | "gteq", [AV_C_fragment (v1, _, _); AV_C_fragment (v2, _, _)] -> + AE_val (AV_C_fragment (F_op (v1, ">=", v2), typ, CT_bool)) + | "lt", [AV_C_fragment (v1, _, _); AV_C_fragment (v2, _, _)] -> + AE_val (AV_C_fragment (F_op (v1, "<", v2), typ, CT_bool)) + | "gt", [AV_C_fragment (v1, _, _); AV_C_fragment (v2, _, _)] -> + AE_val (AV_C_fragment (F_op (v1, ">", v2), typ, CT_bool)) + + | "xor_bits", [AV_C_fragment (v1, _, (CT_fbits _ as ctyp)); AV_C_fragment (v2, _, CT_fbits _)] -> + AE_val (AV_C_fragment (F_op (v1, "^", v2), typ, ctyp)) + | "xor_bits", [AV_C_fragment (v1, _, (CT_sbits _ as ctyp)); AV_C_fragment (v2, _, CT_sbits _)] -> + AE_val (AV_C_fragment (F_call ("xor_sbits", [v1; v2]), typ, ctyp)) + + | "or_bits", [AV_C_fragment (v1, _, (CT_fbits _ as ctyp)); AV_C_fragment (v2, _, CT_fbits _)] -> + AE_val (AV_C_fragment (F_op (v1, "|", v2), typ, ctyp)) + + | "and_bits", [AV_C_fragment (v1, _, (CT_fbits _ as ctyp)); AV_C_fragment (v2, _, CT_fbits _)] -> + AE_val (AV_C_fragment (F_op (v1, "&", v2), typ, ctyp)) + + | "not_bits", [AV_C_fragment (v, _, ctyp)] -> + begin match destruct_vector ctx.tc_env typ with + | Some (Nexp_aux (Nexp_constant n, _), _, Typ_aux (Typ_id id, _)) + when string_of_id id = "bit" && Big_int.less_equal n (Big_int.of_int 64) -> + AE_val (AV_C_fragment (F_op (F_unary ("~", v), "&", v_mask_lower (Big_int.to_int n)), typ, ctyp)) + | _ -> no_change + end + + | "vector_subrange", [AV_C_fragment (vec, _, CT_fbits _); AV_C_fragment (f, _, _); AV_C_fragment (t, _, _)] + when is_fbits_typ ctx typ -> + let len = F_op (f, "-", F_op (t, "-", v_one)) in + AE_val (AV_C_fragment (F_op (F_call ("safe_rshift", [F_raw "UINT64_MAX"; F_op (v_int 64, "-", len)]), "&", F_op (vec, ">>", t)), + typ, + ctyp_of_typ ctx typ)) + + | "vector_access", [AV_C_fragment (vec, _, CT_fbits _); AV_C_fragment (n, _, _)] -> + AE_val (AV_C_fragment (F_op (v_one, "&", F_op (vec, ">>", n)), typ, CT_bit)) + + | "eq_bit", [AV_C_fragment (a, _, _); AV_C_fragment (b, _, _)] -> + AE_val (AV_C_fragment (F_op (a, "==", b), typ, CT_bool)) + + | "slice", [AV_C_fragment (vec, _, CT_fbits _); AV_C_fragment (start, _, _); AV_C_fragment (len, _, _)] + when is_fbits_typ ctx typ -> + AE_val (AV_C_fragment (F_op (F_call ("safe_rshift", [F_raw "UINT64_MAX"; F_op (v_int 64, "-", len)]), "&", F_op (vec, ">>", start)), + typ, + ctyp_of_typ ctx typ)) + + | "slice", [AV_C_fragment (vec, _, CT_fbits _); AV_C_fragment (start, _, _); AV_C_fragment (len, _, _)] + when is_sbits_typ ctx typ -> + AE_val (AV_C_fragment (F_call ("sslice", [vec; start; len]), typ, ctyp_of_typ ctx typ)) + + | "undefined_bit", _ -> + AE_val (AV_C_fragment (F_lit (V_bit Sail2_values.B0), typ, CT_bit)) + + (* Optimized routines for all combinations of fixed and small bits + appends, where the result is guaranteed to be smaller than 64. *) + | "append", [AV_C_fragment (vec1, _, CT_fbits (0, ord1)); AV_C_fragment (vec2, _, CT_fbits (n2, ord2)) as v2] + when ord1 = ord2 -> + AE_val v2 + | "append", [AV_C_fragment (vec1, _, CT_fbits (n1, ord1)); AV_C_fragment (vec2, _, CT_fbits (n2, ord2))] + when ord1 = ord2 && n1 + n2 <= 64 -> + AE_val (AV_C_fragment (F_op (F_op (vec1, "<<", v_int n2), "|", vec2), typ, CT_fbits (n1 + n2, ord1))) + + | "append", [AV_C_fragment (vec1, _, CT_sbits (64, ord1)); AV_C_fragment (vec2, _, CT_fbits (n2, ord2))] + when ord1 = ord2 && is_sbits_typ ctx typ -> + AE_val (AV_C_fragment (F_call ("append_sf", [vec1; vec2; v_int n2]), typ, ctyp_of_typ ctx typ)) + + | "append", [AV_C_fragment (vec1, _, CT_fbits (n1, ord1)); AV_C_fragment (vec2, _, CT_sbits (64, ord2))] + when ord1 = ord2 && is_sbits_typ ctx typ -> + AE_val (AV_C_fragment (F_call ("append_fs", [vec1; v_int n1; vec2]), typ, ctyp_of_typ ctx typ)) + + | "append", [AV_C_fragment (vec1, _, CT_sbits (64, ord1)); AV_C_fragment (vec2, _, CT_sbits (64, ord2))] + when ord1 = ord2 && is_sbits_typ ctx typ -> + AE_val (AV_C_fragment (F_call ("append_ss", [vec1; vec2]), typ, ctyp_of_typ ctx typ)) + + | "undefined_vector", [AV_C_fragment (len, _, _); _] -> + begin match destruct_vector ctx.tc_env typ with + | Some (Nexp_aux (Nexp_constant n, _), _, Typ_aux (Typ_id id, _)) + when string_of_id id = "bit" && Big_int.less_equal n (Big_int.of_int 64) -> + AE_val (AV_C_fragment (F_lit (V_bit Sail2_values.B0), typ, ctyp_of_typ ctx typ)) + | _ -> no_change + end + + | "sail_unsigned", [AV_C_fragment (frag, vtyp, _)] -> + begin match destruct_vector ctx.tc_env vtyp with + | Some (Nexp_aux (Nexp_constant n, _), _, _) + when Big_int.less_equal n (Big_int.of_int 63) && is_stack_typ ctx typ -> + AE_val (AV_C_fragment (F_call ("fast_unsigned", [frag]), typ, ctyp_of_typ ctx typ)) + | _ -> no_change + end + + | "sail_signed", [AV_C_fragment (frag, vtyp, _)] -> + begin match destruct_vector ctx.tc_env vtyp with + | Some (Nexp_aux (Nexp_constant n, _), _, _) + when Big_int.less_equal n (Big_int.of_int 64) && is_stack_typ ctx typ -> + AE_val (AV_C_fragment (F_call ("fast_signed", [frag; v_int (Big_int.to_int n)]), typ, ctyp_of_typ ctx typ)) + | _ -> no_change + end + + | "add_int", [AV_C_fragment (op1, _, _); AV_C_fragment (op2, _, _)] -> + begin match destruct_range Env.empty typ with + | None -> no_change + | Some (kids, constr, n, m) -> + match nexp_simp n, nexp_simp m with + | Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_constant m, _) + when Big_int.less_equal (min_int 64) n && Big_int.less_equal m (max_int 64) -> + AE_val (AV_C_fragment (F_op (op1, "+", op2), typ, CT_fint 64)) + | n, m when prove __POS__ ctx.local_env (nc_lteq (nconstant (min_int 64)) n) && prove __POS__ ctx.local_env (nc_lteq m (nconstant (max_int 64))) -> + AE_val (AV_C_fragment (F_op (op1, "+", op2), typ, CT_fint 64)) + | _ -> no_change + end + + | "neg_int", [AV_C_fragment (frag, _, _)] -> + AE_val (AV_C_fragment (F_op (v_int 0, "-", frag), typ, CT_fint 64)) + + | "replicate_bits", [AV_C_fragment (vec, vtyp, _); AV_C_fragment (times, _, _)] -> + begin match destruct_vector ctx.tc_env typ, destruct_vector ctx.tc_env vtyp with + | Some (Nexp_aux (Nexp_constant n, _), _, _), Some (Nexp_aux (Nexp_constant m, _), _, _) + when Big_int.less_equal n (Big_int.of_int 64) -> + AE_val (AV_C_fragment (F_call ("fast_replicate_bits", [F_lit (V_int m); vec; times]), typ, ctyp_of_typ ctx typ)) + | _ -> no_change + end + + | "vector_update_subrange", [AV_C_fragment (xs, _, CT_fbits (n, true)); + AV_C_fragment (hi, _, CT_fint 64); + AV_C_fragment (lo, _, CT_fint 64); + AV_C_fragment (ys, _, CT_fbits (m, true))] -> + AE_val (AV_C_fragment (F_call ("fast_update_subrange", [xs; hi; lo; ys]), typ, CT_fbits (n, true))) + + | "undefined_bool", _ -> + AE_val (AV_C_fragment (F_lit (V_bool false), typ, CT_bool)) + + | _, _ -> + c_debug (lazy ("No optimization routine found")); + no_change + +let analyze_primop ctx id args typ = + let no_change = AE_app (id, args, typ) in + if !optimize_primops then + try analyze_primop' ctx id args typ with + | Failure str -> + (c_debug (lazy ("Analyze primop failed for id " ^ string_of_id id ^ " reason: " ^ str))); + no_change + else + no_change + +let generate_cleanup instrs = + let generate_cleanup' (I_aux (instr, _)) = + match instr with + | I_init (ctyp, id, cval) -> [(id, iclear ctyp id)] + | I_decl (ctyp, id) -> [(id, iclear ctyp id)] + | instr -> [] + in + let is_clear ids = function + | I_aux (I_clear (_, id), _) -> IdSet.add id ids + | _ -> ids + in + let cleaned = List.fold_left is_clear IdSet.empty instrs in + instrs + |> List.map generate_cleanup' + |> List.concat + |> List.filter (fun (id, _) -> not (IdSet.mem id cleaned)) + |> List.map snd + +(** Functions that have heap-allocated return types are implemented by + passing a pointer a location where the return value should be + stored. The ANF -> Sail IR pass for expressions simply outputs an + I_return instruction for any return value, so this function walks + over the IR ast for expressions and modifies the return statements + into code that sets that pointer, as well as adds extra control + flow to cleanup heap-allocated variables correctly when a function + terminates early. See the generate_cleanup function for how this is + done. *) +let fix_early_heap_return ret ret_ctyp instrs = + let end_function_label = label "end_function_" in + let is_return_recur (I_aux (instr, _)) = + match instr with + | I_if _ | I_block _ | I_end | I_funcall _ | I_copy _ | I_undefined _ -> true + | _ -> false + in + let rec rewrite_return instrs = + match instr_split_at is_return_recur instrs with + | instrs, [] -> instrs + | before, I_aux (I_block instrs, _) :: after -> + before + @ [iblock (rewrite_return instrs)] + @ rewrite_return after + | before, I_aux (I_if (cval, then_instrs, else_instrs, ctyp), _) :: after -> + before + @ [iif cval (rewrite_return then_instrs) (rewrite_return else_instrs) ctyp] + @ rewrite_return after + | before, I_aux (I_funcall (CL_return ctyp, extern, fid, args), aux) :: after -> + before + @ [I_aux (I_funcall (CL_addr (CL_id (ret, CT_ref ctyp)), extern, fid, args), aux)] + @ rewrite_return after + | before, I_aux (I_copy (CL_return ctyp, cval), aux) :: after -> + before + @ [I_aux (I_copy (CL_addr (CL_id (ret, CT_ref ctyp)), cval), aux)] + @ rewrite_return after + | before, I_aux ((I_end | I_undefined _), _) :: after -> + before + @ [igoto end_function_label] + @ rewrite_return after + | before, (I_aux ((I_copy _ | I_funcall _), _) as instr) :: after -> + before @ instr :: rewrite_return after + | _, _ -> assert false + in + rewrite_return instrs + @ [ilabel end_function_label] + +(* This is like fix_early_return, but for stack allocated returns. *) +let fix_early_stack_return ret ret_ctyp instrs = + let is_return_recur (I_aux (instr, _)) = + match instr with + | I_if _ | I_block _ | I_end | I_funcall _ | I_copy _ -> true + | _ -> false + in + let rec rewrite_return instrs = + match instr_split_at is_return_recur instrs with + | instrs, [] -> instrs + | before, I_aux (I_block instrs, _) :: after -> + before + @ [iblock (rewrite_return instrs)] + @ rewrite_return after + | before, I_aux (I_if (cval, then_instrs, else_instrs, ctyp), _) :: after -> + before + @ [iif cval (rewrite_return then_instrs) (rewrite_return else_instrs) ctyp] + @ rewrite_return after + | before, I_aux (I_funcall (CL_return ctyp, extern, fid, args), aux) :: after -> + before + @ [I_aux (I_funcall (CL_id (ret, ctyp), extern, fid, args), aux)] + @ rewrite_return after + | before, I_aux (I_copy (CL_return ctyp, cval), aux) :: after -> + before + @ [I_aux (I_copy (CL_id (ret, ctyp), cval), aux)] + @ rewrite_return after + | before, I_aux (I_end, _) :: after -> + before + @ [ireturn (F_id ret, ret_ctyp)] + @ rewrite_return after + | before, (I_aux ((I_copy _ | I_funcall _), _) as instr) :: after -> + before @ instr :: rewrite_return after + | _, _ -> assert false + in + rewrite_return instrs + +let rec insert_heap_returns ret_ctyps = function + | (CDEF_spec (id, _, ret_ctyp) as cdef) :: cdefs -> + cdef :: insert_heap_returns (Bindings.add id ret_ctyp ret_ctyps) cdefs + + | CDEF_fundef (id, None, args, body) :: cdefs -> + let gs = gensym () in + begin match Bindings.find_opt id ret_ctyps with + | None -> + raise (Reporting.err_general (id_loc id) ("Cannot find return type for function " ^ string_of_id id)) + | Some ret_ctyp when not (is_stack_ctyp ret_ctyp) -> + CDEF_fundef (id, Some gs, args, fix_early_heap_return gs ret_ctyp body) + :: insert_heap_returns ret_ctyps cdefs + | Some ret_ctyp -> + CDEF_fundef (id, None, args, fix_early_stack_return gs ret_ctyp (idecl ret_ctyp gs :: body)) + :: insert_heap_returns ret_ctyps cdefs + end + + | CDEF_fundef (id, gs, _, _) :: _ -> + raise (Reporting.err_unreachable (id_loc id) __POS__ "Found function with return already re-written in insert_heap_returns") + + | cdef :: cdefs -> + cdef :: insert_heap_returns ret_ctyps cdefs + + | [] -> [] + +(** To keep things neat we use GCC's local labels extension to limit + the scope of labels. We do this by iterating over all the blocks + and adding a __label__ declaration with all the labels local to + that block. The add_local_labels function is called by the code + generator just before it outputs C. + + See https://gcc.gnu.org/onlinedocs/gcc/Local-Labels.html **) +let add_local_labels' instrs = + 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 = 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' (iblock instrs) with + | I_aux (I_block instrs, _) -> instrs + | _ -> assert false + +(**************************************************************************) +(* 5. Optimizations *) +(**************************************************************************) + +let rec instrs_rename from_id to_id = + let rename id = if Id.compare id from_id = 0 then to_id else id in + let crename = cval_rename from_id to_id in + let irename instrs = instrs_rename from_id to_id instrs in + let lrename = clexp_rename from_id to_id in + function + | (I_aux (I_decl (ctyp, new_id), _) :: _) as instrs when Id.compare from_id new_id = 0 -> instrs + | I_aux (I_decl (ctyp, new_id), aux) :: instrs -> I_aux (I_decl (ctyp, new_id), aux) :: irename instrs + | I_aux (I_reset (ctyp, id), aux) :: instrs -> I_aux (I_reset (ctyp, rename id), aux) :: irename instrs + | I_aux (I_init (ctyp, id, cval), aux) :: instrs -> I_aux (I_init (ctyp, rename id, crename cval), aux) :: irename instrs + | I_aux (I_reinit (ctyp, id, cval), aux) :: instrs -> I_aux (I_reinit (ctyp, rename id, crename cval), aux) :: irename instrs + | I_aux (I_if (cval, then_instrs, else_instrs, ctyp), aux) :: instrs -> + I_aux (I_if (crename cval, irename then_instrs, irename else_instrs, ctyp), aux) :: irename instrs + | I_aux (I_jump (cval, label), aux) :: instrs -> I_aux (I_jump (crename cval, label), aux) :: irename instrs + | I_aux (I_funcall (clexp, extern, id, cvals), aux) :: instrs -> + I_aux (I_funcall (lrename clexp, extern, rename id, List.map crename cvals), aux) :: irename instrs + | I_aux (I_copy (clexp, cval), aux) :: instrs -> I_aux (I_copy (lrename clexp, crename cval), aux) :: irename instrs + | I_aux (I_alias (clexp, cval), aux) :: instrs -> I_aux (I_alias (lrename clexp, crename cval), aux) :: irename instrs + | I_aux (I_clear (ctyp, id), aux) :: instrs -> I_aux (I_clear (ctyp, rename id), aux) :: irename instrs + | I_aux (I_return cval, aux) :: instrs -> I_aux (I_return (crename cval), aux) :: irename instrs + | I_aux (I_block block, aux) :: instrs -> I_aux (I_block (irename block), aux) :: irename instrs + | I_aux (I_try_block block, aux) :: instrs -> I_aux (I_try_block (irename block), aux) :: irename instrs + | I_aux (I_throw cval, aux) :: instrs -> I_aux (I_throw (crename cval), aux) :: irename instrs + | (I_aux ((I_comment _ | I_raw _ | I_end | I_label _ | I_goto _ | I_match_failure | I_undefined _), _) as instr) :: instrs -> instr :: irename instrs + | [] -> [] + +let hoist_ctyp = function + | CT_lint | CT_lbits _ | CT_struct _ -> true + | _ -> false + +let hoist_counter = ref 0 +let hoist_id () = + let id = mk_id ("gh#" ^ string_of_int !hoist_counter) in + incr hoist_counter; + id + +let hoist_allocations recursive_functions = function + | CDEF_fundef (function_id, _, _, _) as cdef when IdSet.mem function_id recursive_functions -> + c_debug (lazy (Printf.sprintf "skipping recursive function %s" (string_of_id function_id))); + [cdef] + + | CDEF_fundef (function_id, heap_return, args, body) -> + let decls = ref [] in + let cleanups = ref [] in + let rec hoist = function + | I_aux (I_decl (ctyp, decl_id), annot) :: instrs when hoist_ctyp ctyp -> + let hid = hoist_id () in + decls := idecl ctyp hid :: !decls; + cleanups := iclear ctyp hid :: !cleanups; + let instrs = instrs_rename decl_id hid instrs in + I_aux (I_reset (ctyp, hid), annot) :: hoist instrs + + | I_aux (I_init (ctyp, decl_id, cval), annot) :: instrs when hoist_ctyp ctyp -> + let hid = hoist_id () in + decls := idecl ctyp hid :: !decls; + cleanups := iclear ctyp hid :: !cleanups; + let instrs = instrs_rename decl_id hid instrs in + I_aux (I_reinit (ctyp, hid, cval), annot) :: hoist instrs + + | I_aux (I_clear (ctyp, _), _) :: instrs when hoist_ctyp ctyp -> + hoist instrs + + | I_aux (I_block block, annot) :: instrs -> + I_aux (I_block (hoist block), annot) :: hoist instrs + | I_aux (I_try_block block, annot) :: instrs -> + I_aux (I_try_block (hoist block), annot) :: hoist instrs + | I_aux (I_if (cval, then_instrs, else_instrs, ctyp), annot) :: instrs -> + I_aux (I_if (cval, hoist then_instrs, hoist else_instrs, ctyp), annot) :: hoist instrs + + | instr :: instrs -> instr :: hoist instrs + | [] -> [] + in + let body = hoist body in + if !decls = [] then + [CDEF_fundef (function_id, heap_return, args, body)] + else + [CDEF_startup (function_id, List.rev !decls); + CDEF_fundef (function_id, heap_return, args, body); + CDEF_finish (function_id, !cleanups)] + + | cdef -> [cdef] + +let rec specialize_variants ctx prior = + let unifications = ref (Bindings.empty) in + + let fix_variant_ctyp var_id new_ctors = function + | CT_variant (id, ctors) when Id.compare id var_id = 0 -> CT_variant (id, new_ctors) + | ctyp -> ctyp + in + + let specialize_constructor ctx ctor_id ctyp = + function + | I_aux (I_funcall (clexp, extern, id, [cval]), ((_, l) as aux)) as instr when Id.compare id ctor_id = 0 -> + (* Work out how each call to a constructor in instantiated and add that to unifications *) + let unification = List.map ctyp_suprema (ctyp_unify ctyp (cval_ctyp cval)) in + let mono_id = append_id ctor_id ("_" ^ Util.string_of_list "_" (fun ctyp -> Util.zencode_string (string_of_ctyp ctyp)) unification) in + unifications := Bindings.add mono_id (ctyp_suprema (cval_ctyp cval)) !unifications; + + (* We need to cast each cval to it's ctyp_suprema in order to put it in the most general constructor *) + let casts = + let cast_to_suprema (frag, ctyp) = + let suprema = ctyp_suprema ctyp in + if ctyp_equal ctyp suprema then + [], (unpoly frag, ctyp), [] + else + let gs = gensym () in + [idecl suprema gs; + icopy l (CL_id (gs, suprema)) (unpoly frag, ctyp)], + (F_id gs, suprema), + [iclear suprema gs] + in + List.map cast_to_suprema [cval] + in + let setup = List.concat (List.map (fun (setup, _, _) -> setup) casts) in + let cvals = List.map (fun (_, cval, _) -> cval) casts in + let cleanup = List.concat (List.map (fun (_, _, cleanup) -> cleanup) casts) in + + let mk_funcall instr = + if List.length setup = 0 then + instr + else + iblock (setup @ [instr] @ cleanup) + in + + mk_funcall (I_aux (I_funcall (clexp, extern, mono_id, cvals), aux)) + + | I_aux (I_funcall (clexp, extern, id, cvals), ((_, l) as aux)) as instr when Id.compare id ctor_id = 0 -> + c_error ~loc:l "Multiple argument constructor found" + + | instr -> instr + in + + function + | (CDEF_type (CTD_variant (var_id, ctors)) as cdef) :: cdefs -> + let polymorphic_ctors = List.filter (fun (_, ctyp) -> is_polymorphic ctyp) ctors in + + let cdefs = + List.fold_left (fun cdefs (ctor_id, ctyp) -> List.map (cdef_map_instr (specialize_constructor ctx ctor_id ctyp)) cdefs) + cdefs + polymorphic_ctors + in + + let monomorphic_ctors = List.filter (fun (_, ctyp) -> not (is_polymorphic ctyp)) ctors in + let specialized_ctors = Bindings.bindings !unifications in + let new_ctors = monomorphic_ctors @ specialized_ctors in + + let ctx = { + ctx with variants = Bindings.add var_id + (List.fold_left (fun m (id, ctyp) -> Bindings.add id ctyp m) !unifications monomorphic_ctors) + ctx.variants + } in + + let cdefs = List.map (cdef_map_ctyp (map_ctyp (fix_variant_ctyp var_id new_ctors))) cdefs in + let prior = List.map (cdef_map_ctyp (map_ctyp (fix_variant_ctyp var_id new_ctors))) prior in + specialize_variants ctx (CDEF_type (CTD_variant (var_id, new_ctors)) :: prior) cdefs + + | cdef :: cdefs -> + let remove_poly (I_aux (instr, aux)) = + match instr with + | I_copy (clexp, (frag, ctyp)) when is_polymorphic ctyp -> + I_aux (I_copy (clexp, (frag, ctyp_suprema (clexp_ctyp clexp))), aux) + | instr -> I_aux (instr, aux) + in + let cdef = cdef_map_instr remove_poly cdef in + specialize_variants ctx (cdef :: prior) cdefs + + | [] -> List.rev prior, ctx + +(** Once we specialize variants, there may be additional type + dependencies which could be in the wrong order. As such we need to + sort the type definitions in the list of cdefs. *) +let sort_ctype_defs cdefs = + (* Split the cdefs into type definitions and non type definitions *) + let is_ctype_def = function CDEF_type _ -> true | _ -> false in + let unwrap = function CDEF_type ctdef -> ctdef | _ -> assert false in + let ctype_defs = List.map unwrap (List.filter is_ctype_def cdefs) in + let cdefs = List.filter (fun cdef -> not (is_ctype_def cdef)) cdefs in + + let ctdef_id = function + | CTD_enum (id, _) | CTD_struct (id, _) | CTD_variant (id, _) -> id + in + + let ctdef_ids = function + | CTD_enum _ -> IdSet.empty + | CTD_struct (_, ctors) | CTD_variant (_, ctors) -> + List.fold_left (fun ids (_, ctyp) -> IdSet.union (ctyp_ids ctyp) ids) IdSet.empty ctors + in + + (* Create a reverse (i.e. from types to the types that are dependent + upon them) id graph of dependencies between types *) + let module IdGraph = Graph.Make(Id) in + + let graph = + List.fold_left (fun g ctdef -> + List.fold_left (fun g id -> IdGraph.add_edge id (ctdef_id ctdef) g) + (IdGraph.add_edges (ctdef_id ctdef) [] g) (* Make sure even types with no dependencies are in graph *) + (IdSet.elements (ctdef_ids ctdef))) + IdGraph.empty + ctype_defs + in + + (* Then select the ctypes in the correct order as given by the topsort *) + let ids = IdGraph.topsort graph in + let ctype_defs = + List.map (fun id -> CDEF_type (List.find (fun ctdef -> Id.compare (ctdef_id ctdef) id = 0) ctype_defs)) ids + in + + ctype_defs @ cdefs + +let removed = icomment "REMOVED" + +let is_not_removed = function + | I_aux (I_comment "REMOVED", _) -> false + | _ -> true + +(** This optimization looks for patterns of the form: + + create x : t; + x = y; + // modifications to x, and no changes to y + y = x; + // no further changes to x + kill x; + + If found, we can remove the variable x, and directly modify y instead. *) +let remove_alias = + let pattern ctyp id = + let alias = ref None in + let rec scan ctyp id n instrs = + match n, !alias, instrs with + | 0, None, I_aux (I_copy (CL_id (id', ctyp'), (F_id a, ctyp'')), _) :: instrs + when Id.compare id id' = 0 && ctyp_equal ctyp ctyp' && ctyp_equal ctyp' ctyp'' -> + alias := Some a; + scan ctyp id 1 instrs + + | 1, Some a, I_aux (I_copy (CL_id (a', ctyp'), (F_id id', ctyp'')), _) :: instrs + when Id.compare a a' = 0 && Id.compare id id' = 0 && ctyp_equal ctyp ctyp' && ctyp_equal ctyp' ctyp'' -> + scan ctyp id 2 instrs + + | 1, Some a, instr :: instrs -> + if IdSet.mem a (instr_ids instr) then + None + else + scan ctyp id 1 instrs + + | 2, Some a, I_aux (I_clear (ctyp', id'), _) :: instrs + when Id.compare id id' = 0 && ctyp_equal ctyp ctyp' -> + scan ctyp id 2 instrs + + | 2, Some a, instr :: instrs -> + if IdSet.mem id (instr_ids instr) then + None + else + scan ctyp id 2 instrs + + | 2, Some a, [] -> !alias + + | n, _, _ :: instrs when n = 0 || n > 2 -> scan ctyp id n instrs + | _, _, I_aux (_, (_, l)) :: instrs -> raise (Reporting.err_unreachable l __POS__ "optimize_alias") + | _, _, [] -> None + in + scan ctyp id 0 + in + let remove_alias id alias = function + | I_aux (I_copy (CL_id (id', _), (F_id alias', _)), _) + when Id.compare id id' = 0 && Id.compare alias alias' = 0 -> removed + | I_aux (I_copy (CL_id (alias', _), (F_id id', _)), _) + when Id.compare id id' = 0 && Id.compare alias alias' = 0 -> removed + | I_aux (I_clear (_, id'), _) -> removed + | instr -> instr + in + let rec opt = function + | I_aux (I_decl (ctyp, id), _) as instr :: instrs -> + begin match pattern ctyp id instrs with + | None -> instr :: opt instrs + | Some alias -> + let instrs = List.map (map_instr (remove_alias id alias)) instrs in + filter_instrs is_not_removed (List.map (instr_rename id alias) instrs) + end + + | I_aux (I_block block, aux) :: instrs -> I_aux (I_block (opt block), aux) :: opt instrs + | I_aux (I_try_block block, aux) :: instrs -> I_aux (I_try_block (opt block), aux) :: opt instrs + | I_aux (I_if (cval, then_instrs, else_instrs, ctyp), aux) :: instrs -> + I_aux (I_if (cval, opt then_instrs, opt else_instrs, ctyp), aux) :: opt instrs + + | instr :: instrs -> + instr :: opt instrs + | [] -> [] + in + function + | CDEF_fundef (function_id, heap_return, args, body) -> + [CDEF_fundef (function_id, heap_return, args, opt body)] + | cdef -> [cdef] + +(** This pass ensures that all variables created by I_decl have unique names *) +let unique_names = + let unique_counter = ref 0 in + let unique_id () = + let id = mk_id ("u#" ^ string_of_int !unique_counter) in + incr unique_counter; + id + in + + let rec opt seen = function + | I_aux (I_decl (ctyp, id), aux) :: instrs when IdSet.mem id seen -> + let id' = unique_id () in + let instrs', seen = opt seen instrs in + I_aux (I_decl (ctyp, id'), aux) :: instrs_rename id id' instrs', seen + + | I_aux (I_decl (ctyp, id), aux) :: instrs -> + let instrs', seen = opt (IdSet.add id seen) instrs in + I_aux (I_decl (ctyp, id), aux) :: instrs', seen + + | I_aux (I_block block, aux) :: instrs -> + let block', seen = opt seen block in + let instrs', seen = opt seen instrs in + I_aux (I_block block', aux) :: instrs', seen + + | I_aux (I_try_block block, aux) :: instrs -> + let block', seen = opt seen block in + let instrs', seen = opt seen instrs in + I_aux (I_try_block block', aux) :: instrs', seen + + | I_aux (I_if (cval, then_instrs, else_instrs, ctyp), aux) :: instrs -> + let then_instrs', seen = opt seen then_instrs in + let else_instrs', seen = opt seen else_instrs in + let instrs', seen = opt seen instrs in + I_aux (I_if (cval, then_instrs', else_instrs', ctyp), aux) :: instrs', seen + + | instr :: instrs -> + let instrs', seen = opt seen instrs in + instr :: instrs', seen + + | [] -> [], seen + in + function + | CDEF_fundef (function_id, heap_return, args, body) -> + [CDEF_fundef (function_id, heap_return, args, fst (opt IdSet.empty body))] + | CDEF_reg_dec (id, ctyp, instrs) -> + [CDEF_reg_dec (id, ctyp, fst (opt IdSet.empty instrs))] + | CDEF_let (n, bindings, instrs) -> + [CDEF_let (n, bindings, fst (opt IdSet.empty instrs))] + | cdef -> [cdef] + +(** This optimization looks for patterns of the form + + create x : t; + create y : t; + // modifications to y, no changes to x + x = y; + kill y; + + If found we can replace y by x *) +let combine_variables = + let pattern ctyp id = + let combine = ref None in + let rec scan id n instrs = + match n, !combine, instrs with + | 0, None, I_aux (I_block block, _) :: instrs -> + begin match scan id 0 block with + | Some combine -> Some combine + | None -> scan id 0 instrs + end + + | 0, None, I_aux (I_decl (ctyp', id'), _) :: instrs when ctyp_equal ctyp ctyp' -> + combine := Some id'; + scan id 1 instrs + + | 1, Some c, I_aux (I_copy (CL_id (id', ctyp'), (F_id c', ctyp'')), _) :: instrs + when Id.compare c c' = 0 && Id.compare id id' = 0 && ctyp_equal ctyp ctyp' && ctyp_equal ctyp' ctyp'' -> + scan id 2 instrs + + (* Ignore seemingly early clears of x, as this can happen along exception paths *) + | 1, Some c, I_aux (I_clear (_, id'), _) :: instrs + when Id.compare id id' = 0 -> + scan id 1 instrs + + | 1, Some c, instr :: instrs -> + if IdSet.mem id (instr_ids instr) then + None + else + scan id 1 instrs + + | 2, Some c, I_aux (I_clear (ctyp', c'), _) :: instrs + when Id.compare c c' = 0 && ctyp_equal ctyp ctyp' -> + !combine + + | 2, Some c, instr :: instrs -> + if IdSet.mem c (instr_ids instr) then + None + else + scan id 2 instrs + + | 2, Some c, [] -> !combine + + | n, _, _ :: instrs -> scan id n instrs + | _, _, [] -> None + in + scan id 0 + in + let remove_variable id = function + | I_aux (I_decl (_, id'), _) when Id.compare id id' = 0 -> removed + | I_aux (I_clear (_, id'), _) when Id.compare id id' = 0 -> removed + | instr -> instr + in + let is_not_self_assignment = function + | I_aux (I_copy (CL_id (id, _), (F_id id', _)), _) when Id.compare id id' = 0 -> false + | _ -> true + in + let rec opt = function + | (I_aux (I_decl (ctyp, id), _) as instr) :: instrs -> + begin match pattern ctyp id instrs with + | None -> instr :: opt instrs + | Some combine -> + let instrs = List.map (map_instr (remove_variable combine)) instrs in + let instrs = filter_instrs (fun i -> is_not_removed i && is_not_self_assignment i) + (List.map (instr_rename combine id) instrs) in + opt (instr :: instrs) + end + + | I_aux (I_block block, aux) :: instrs -> I_aux (I_block (opt block), aux) :: opt instrs + | I_aux (I_try_block block, aux) :: instrs -> I_aux (I_try_block (opt block), aux) :: opt instrs + | I_aux (I_if (cval, then_instrs, else_instrs, ctyp), aux) :: instrs -> + I_aux (I_if (cval, opt then_instrs, opt else_instrs, ctyp), aux) :: opt instrs + + | instr :: instrs -> + instr :: opt instrs + | [] -> [] + in + function + | CDEF_fundef (function_id, heap_return, args, body) -> + [CDEF_fundef (function_id, heap_return, args, opt body)] + | cdef -> [cdef] + +(** hoist_alias looks for patterns like + + recreate x; y = x; // no furthner mentions of x + + Provided x has a certain type, then we can make y an alias to x + (denoted in the IR as 'alias y = x'). This only works if y also has + a lifespan that also spans the entire function body. It's possible + we may need to do a more thorough lifetime evaluation to get this + to be 100% correct - so it's behind the -Oexperimental flag + for now. Some benchmarking shows that this kind of optimization + is very valuable however! *) +let hoist_alias = + (* Must return true for a subset of the types hoist_ctyp would return true for. *) + let is_struct = function + | CT_struct _ -> true + | _ -> false + in + let pattern heap_return id ctyp instrs = + let rec scan instrs = + match instrs with + (* The only thing that has a longer lifetime than id is the + function return, so we want to make sure we avoid that + case. *) + | (I_aux (I_copy (clexp, (F_id id', ctyp')), aux) as instr) :: instrs + when not (IdSet.mem heap_return (instr_writes instr)) && Id.compare id id' = 0 + && ctyp_equal (clexp_ctyp clexp) ctyp && ctyp_equal ctyp ctyp' -> + if List.exists (IdSet.mem id) (List.map instr_ids instrs) then + instr :: scan instrs + else + I_aux (I_alias (clexp, (F_id id', ctyp')), aux) :: instrs + + | instr :: instrs -> instr :: scan instrs + | [] -> [] + in + scan instrs + in + let optimize heap_return = + let rec opt = function + | (I_aux (I_reset (ctyp, id), _) as instr) :: instrs when not (is_stack_ctyp ctyp) && is_struct ctyp -> + instr :: opt (pattern heap_return id ctyp instrs) + + | I_aux (I_block block, aux) :: instrs -> I_aux (I_block (opt block), aux) :: opt instrs + | I_aux (I_try_block block, aux) :: instrs -> I_aux (I_try_block (opt block), aux) :: opt instrs + | I_aux (I_if (cval, then_instrs, else_instrs, ctyp), aux) :: instrs -> + I_aux (I_if (cval, opt then_instrs, opt else_instrs, ctyp), aux) :: opt instrs + + | instr :: instrs -> + instr :: opt instrs + | [] -> [] + in + opt + in + function + | CDEF_fundef (function_id, Some heap_return, args, body) -> + [CDEF_fundef (function_id, Some heap_return, args, optimize heap_return body)] + | cdef -> [cdef] + +let concatMap f xs = List.concat (List.map f xs) + +let optimize recursive_functions cdefs = + let nothing cdefs = cdefs in + cdefs + |> (if !optimize_alias then concatMap unique_names else nothing) + |> (if !optimize_alias then concatMap remove_alias else nothing) + |> (if !optimize_alias then concatMap combine_variables else nothing) + (* We need the runtime to initialize hoisted allocations *) + |> (if !optimize_hoist_allocations && not !opt_no_rts then concatMap (hoist_allocations recursive_functions) else nothing) + |> (if !optimize_hoist_allocations && !optimize_experimental then concatMap hoist_alias else nothing) + +(**************************************************************************) +(* 6. Code generation *) +(**************************************************************************) + +let sgen_id id = Util.zencode_string (string_of_id id) +let codegen_id id = string (sgen_id id) + +let sgen_function_id id = + let str = Util.zencode_string (string_of_id id) in + !opt_prefix ^ String.sub str 1 (String.length str - 1) + +let codegen_function_id id = string (sgen_function_id id) + +let rec sgen_ctyp = function + | CT_unit -> "unit" + | CT_bit -> "fbits" + | CT_bool -> "bool" + | CT_fbits _ -> "fbits" + | CT_sbits _ -> "sbits" + | CT_fint _ -> "mach_int" + | CT_lint -> "sail_int" + | CT_lbits _ -> "lbits" + | CT_tup _ as tup -> "struct " ^ Util.zencode_string ("tuple_" ^ string_of_ctyp tup) + | CT_struct (id, _) -> "struct " ^ sgen_id id + | CT_enum (id, _) -> "enum " ^ sgen_id id + | CT_variant (id, _) -> "struct " ^ sgen_id id + | CT_list _ as l -> Util.zencode_string (string_of_ctyp l) + | CT_vector _ as v -> Util.zencode_string (string_of_ctyp v) + | CT_string -> "sail_string" + | CT_real -> "real" + | CT_ref ctyp -> sgen_ctyp ctyp ^ "*" + | CT_poly -> "POLY" (* c_error "Tried to generate code for non-monomorphic type" *) + +let rec sgen_ctyp_name = function + | CT_unit -> "unit" + | CT_bit -> "fbits" + | CT_bool -> "bool" + | CT_fbits _ -> "fbits" + | CT_sbits _ -> "sbits" + | CT_fint _ -> "mach_int" + | CT_lint -> "sail_int" + | CT_lbits _ -> "lbits" + | CT_tup _ as tup -> Util.zencode_string ("tuple_" ^ string_of_ctyp tup) + | CT_struct (id, _) -> sgen_id id + | CT_enum (id, _) -> sgen_id id + | CT_variant (id, _) -> sgen_id id + | CT_list _ as l -> Util.zencode_string (string_of_ctyp l) + | CT_vector _ as v -> Util.zencode_string (string_of_ctyp v) + | CT_string -> "sail_string" + | CT_real -> "real" + | CT_ref ctyp -> "ref_" ^ sgen_ctyp_name ctyp + | CT_poly -> "POLY" (* c_error "Tried to generate code for non-monomorphic type" *) + +let sgen_cval_param (frag, ctyp) = + match ctyp with + | CT_lbits direction -> + string_of_fragment frag ^ ", " ^ string_of_bool direction + | CT_sbits (_, direction) -> + string_of_fragment frag ^ ", " ^ string_of_bool direction + | CT_fbits (len, direction) -> + string_of_fragment frag ^ ", UINT64_C(" ^ string_of_int len ^ ") , " ^ string_of_bool direction + | _ -> + string_of_fragment frag + +let sgen_cval = function (frag, _) -> string_of_fragment frag + +let rec sgen_clexp = function + | CL_id (id, _) -> "&" ^ sgen_id id + | CL_field (clexp, field) -> "&((" ^ sgen_clexp clexp ^ ")->" ^ Util.zencode_string field ^ ")" + | CL_tuple (clexp, n) -> "&((" ^ sgen_clexp clexp ^ ")->ztup" ^ string_of_int n ^ ")" + | CL_addr clexp -> "(*(" ^ sgen_clexp clexp ^ "))" + | CL_have_exception -> "have_exception" + | CL_current_exception _ -> "current_exception" + | CL_return _ -> assert false + | CL_void -> assert false + +let rec sgen_clexp_pure = function + | CL_id (id, _) -> sgen_id id + | CL_field (clexp, field) -> sgen_clexp_pure clexp ^ "." ^ Util.zencode_string field + | CL_tuple (clexp, n) -> sgen_clexp_pure clexp ^ ".ztup" ^ string_of_int n + | CL_addr clexp -> "(*(" ^ sgen_clexp_pure clexp ^ "))" + | CL_have_exception -> "have_exception" + | CL_current_exception _ -> "current_exception" + | CL_return _ -> assert false + | CL_void -> assert false + +(** Generate instructions to copy from a cval to a clexp. This will + insert any needed type conversions from big integers to small + integers (or vice versa), or from arbitrary-length bitvectors to + and from uint64 bitvectors as needed. *) +let rec codegen_conversion l clexp cval = + let open Printf in + let ctyp_to = clexp_ctyp clexp in + let ctyp_from = cval_ctyp cval in + match ctyp_to, ctyp_from with + (* When both types are equal, we don't need any conversion. *) + | _, _ when ctyp_equal ctyp_to ctyp_from -> + if is_stack_ctyp ctyp_to then + ksprintf string " %s = %s;" (sgen_clexp_pure clexp) (sgen_cval cval) + else + ksprintf string " COPY(%s)(%s, %s);" (sgen_ctyp_name ctyp_to) (sgen_clexp clexp) (sgen_cval cval) + + | CT_ref ctyp_to, ctyp_from -> + codegen_conversion l (CL_addr clexp) cval + + (* If we have to convert between tuple types, convert the fields individually. *) + | CT_tup ctyps_to, CT_tup ctyps_from when List.length ctyps_to = List.length ctyps_from -> + let conversions = + List.mapi (fun i ctyp -> codegen_conversion l (CL_tuple (clexp, i)) (F_field (fst cval, "ztup" ^ string_of_int i), ctyp)) ctyps_from + in + string " /* conversions */" + ^^ hardline + ^^ separate hardline conversions + ^^ hardline + ^^ string " /* end conversions */" + + (* For anything not special cased, just try to call a appropriate CONVERT_OF function. *) + | _, _ when is_stack_ctyp (clexp_ctyp clexp) -> + ksprintf string " %s = CONVERT_OF(%s, %s)(%s);" + (sgen_clexp_pure clexp) (sgen_ctyp_name ctyp_to) (sgen_ctyp_name ctyp_from) (sgen_cval_param cval) + | _, _ -> + ksprintf string " CONVERT_OF(%s, %s)(%s, %s);" + (sgen_ctyp_name ctyp_to) (sgen_ctyp_name ctyp_from) (sgen_clexp clexp) (sgen_cval_param cval) + +let rec codegen_instr fid ctx (I_aux (instr, (_, l))) = + let open Printf in + match instr with + | I_decl (ctyp, id) when is_stack_ctyp ctyp -> + ksprintf string " %s %s;" (sgen_ctyp ctyp) (sgen_id id) + | I_decl (ctyp, id) -> + ksprintf string " %s %s;" (sgen_ctyp ctyp) (sgen_id id) ^^ hardline + ^^ ksprintf string " CREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id) + + | I_copy (clexp, cval) -> codegen_conversion l clexp cval + + | I_alias (clexp, cval) -> + ksprintf string " %s = %s;" (sgen_clexp_pure clexp) (sgen_cval cval) + + | I_jump (cval, label) -> + ksprintf string " if (%s) goto %s;" (sgen_cval cval) label + + | I_if (cval, [then_instr], [], ctyp) -> + ksprintf string " if (%s)" (sgen_cval cval) ^^ hardline + ^^ twice space ^^ codegen_instr fid ctx then_instr + | I_if (cval, then_instrs, [], ctyp) -> + string " if" ^^ space ^^ parens (string (sgen_cval cval)) ^^ space + ^^ surround 0 0 lbrace (separate_map hardline (codegen_instr fid ctx) then_instrs) (twice space ^^ rbrace) + | I_if (cval, then_instrs, else_instrs, ctyp) -> + string " if" ^^ space ^^ parens (string (sgen_cval cval)) ^^ space + ^^ surround 0 0 lbrace (separate_map hardline (codegen_instr fid ctx) then_instrs) (twice space ^^ rbrace) + ^^ space ^^ string "else" ^^ space + ^^ surround 0 0 lbrace (separate_map hardline (codegen_instr fid ctx) else_instrs) (twice space ^^ rbrace) + + | I_block instrs -> + string " {" + ^^ jump 2 2 (separate_map hardline (codegen_instr fid ctx) instrs) ^^ hardline + ^^ string " }" + + | I_try_block instrs -> + string " { /* try */" + ^^ jump 2 2 (separate_map hardline (codegen_instr fid ctx) instrs) ^^ hardline + ^^ string " }" + + | I_funcall (x, extern, f, args) -> + let c_args = Util.string_of_list ", " sgen_cval args in + let ctyp = clexp_ctyp x in + let is_extern = Env.is_extern f ctx.tc_env "c" || extern in + let fname = + if Env.is_extern f ctx.tc_env "c" then + Env.get_extern f ctx.tc_env "c" + else if extern then + string_of_id f + else + sgen_function_id f + in + let fname = + match fname, ctyp with + | "internal_pick", _ -> Printf.sprintf "pick_%s" (sgen_ctyp_name ctyp) + | "eq_anything", _ -> + begin match args with + | cval :: _ -> Printf.sprintf "eq_%s" (sgen_ctyp_name (cval_ctyp cval)) + | _ -> c_error "eq_anything function with bad arity." + end + | "length", _ -> + begin match args with + | cval :: _ -> Printf.sprintf "length_%s" (sgen_ctyp_name (cval_ctyp cval)) + | _ -> c_error "length function with bad arity." + end + | "vector_access", CT_bit -> "bitvector_access" + | "vector_access", _ -> + begin match args with + | cval :: _ -> Printf.sprintf "vector_access_%s" (sgen_ctyp_name (cval_ctyp cval)) + | _ -> c_error "vector access function with bad arity." + end + | "vector_update_subrange", _ -> Printf.sprintf "vector_update_subrange_%s" (sgen_ctyp_name ctyp) + | "vector_subrange", _ -> Printf.sprintf "vector_subrange_%s" (sgen_ctyp_name ctyp) + | "vector_update", CT_fbits _ -> "update_fbits" + | "vector_update", CT_lbits _ -> "update_lbits" + | "vector_update", _ -> Printf.sprintf "vector_update_%s" (sgen_ctyp_name ctyp) + | "string_of_bits", _ -> + begin match cval_ctyp (List.nth args 0) with + | CT_fbits _ -> "string_of_fbits" + | CT_lbits _ -> "string_of_lbits" + | _ -> assert false + end + | "decimal_string_of_bits", _ -> + begin match cval_ctyp (List.nth args 0) with + | CT_fbits _ -> "decimal_string_of_fbits" + | CT_lbits _ -> "decimal_string_of_lbits" + | _ -> assert false + end + | "internal_vector_update", _ -> Printf.sprintf "internal_vector_update_%s" (sgen_ctyp_name ctyp) + | "internal_vector_init", _ -> Printf.sprintf "internal_vector_init_%s" (sgen_ctyp_name ctyp) + | "undefined_vector", CT_fbits _ -> "UNDEFINED(fbits)" + | "undefined_vector", CT_lbits _ -> "UNDEFINED(lbits)" + | "undefined_bit", _ -> "UNDEFINED(fbits)" + | "undefined_vector", _ -> Printf.sprintf "UNDEFINED(vector_%s)" (sgen_ctyp_name ctyp) + | fname, _ -> fname + in + if fname = "sail_assert" && !optimize_experimental then + empty + else if fname = "reg_deref" then + if is_stack_ctyp ctyp then + string (Printf.sprintf " %s = *(%s);" (sgen_clexp_pure x) c_args) + else + string (Printf.sprintf " COPY(%s)(&%s, *(%s));" (sgen_ctyp_name ctyp) (sgen_clexp_pure x) c_args) + else + if is_stack_ctyp ctyp then + string (Printf.sprintf " %s = %s(%s%s);" (sgen_clexp_pure x) fname (extra_arguments is_extern) c_args) + else + string (Printf.sprintf " %s(%s%s, %s);" fname (extra_arguments is_extern) (sgen_clexp x) c_args) + + | I_clear (ctyp, id) when is_stack_ctyp ctyp -> + empty + | I_clear (ctyp, id) -> + string (Printf.sprintf " KILL(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id)) + + | I_init (ctyp, id, cval) -> + codegen_instr fid ctx (idecl ctyp id) ^^ hardline + ^^ codegen_conversion Parse_ast.Unknown (CL_id (id, ctyp)) cval + + | I_reinit (ctyp, id, cval) -> + codegen_instr fid ctx (ireset ctyp id) ^^ hardline + ^^ codegen_conversion Parse_ast.Unknown (CL_id (id, ctyp)) cval + + | I_reset (ctyp, id) when is_stack_ctyp ctyp -> + string (Printf.sprintf " %s %s;" (sgen_ctyp ctyp) (sgen_id id)) + | I_reset (ctyp, id) -> + string (Printf.sprintf " RECREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id)) + + | I_return cval -> + string (Printf.sprintf " return %s;" (sgen_cval cval)) + + | I_throw cval -> + c_error ~loc:l "I_throw reached code generator" + + | I_undefined ctyp -> + let rec codegen_exn_return ctyp = + match ctyp with + | CT_unit -> "UNIT", [] + | CT_bit -> "UINT64_C(0)", [] + | CT_fint _ -> "INT64_C(0xdeadc0de)", [] + | CT_fbits _ -> "UINT64_C(0xdeadc0de)", [] + | CT_sbits _ -> "undefined_sbits()", [] + | CT_bool -> "false", [] + | CT_enum (_, ctor :: _) -> sgen_id ctor, [] + | CT_tup ctyps when is_stack_ctyp ctyp -> + let gs = gensym () in + let fold (inits, prev) (n, ctyp) = + let init, prev' = codegen_exn_return ctyp in + Printf.sprintf ".ztup%d = %s" n init :: inits, prev @ prev' + in + let inits, prev = List.fold_left fold ([], []) (List.mapi (fun i x -> (i, x)) ctyps) in + sgen_id gs, + [Printf.sprintf "struct %s %s = { " (sgen_ctyp_name ctyp) (sgen_id gs) + ^ Util.string_of_list ", " (fun x -> x) inits ^ " };"] @ prev + | CT_struct (id, ctors) when is_stack_ctyp ctyp -> + let gs = gensym () in + let fold (inits, prev) (id, ctyp) = + let init, prev' = codegen_exn_return ctyp in + Printf.sprintf ".%s = %s" (sgen_id id) init :: inits, prev @ prev' + in + let inits, prev = List.fold_left fold ([], []) ctors in + sgen_id gs, + [Printf.sprintf "struct %s %s = { " (sgen_ctyp_name ctyp) (sgen_id gs) + ^ Util.string_of_list ", " (fun x -> x) inits ^ " };"] @ prev + | ctyp -> c_error ("Cannot create undefined value for type: " ^ string_of_ctyp ctyp) + in + let ret, prev = codegen_exn_return ctyp in + separate_map hardline (fun str -> string (" " ^ str)) (List.rev prev) + ^^ hardline + ^^ string (Printf.sprintf " return %s;" ret) + + | I_comment str -> + string (" /* " ^ str ^ " */") + + | I_label str -> + string (str ^ ": ;") + + | I_goto str -> + string (Printf.sprintf " goto %s;" str) + + | I_raw _ when ctx.no_raw -> empty + | I_raw str -> + string (" " ^ str) + + | I_end -> assert false + + | I_match_failure -> + string (" sail_match_failure(\"" ^ String.escaped (string_of_id fid) ^ "\");") + +let codegen_type_def ctx = function + | CTD_enum (id, ((first_id :: _) as ids)) -> + let codegen_eq = + let name = sgen_id id in + string (Printf.sprintf "static bool eq_%s(enum %s op1, enum %s op2) { return op1 == op2; }" name name name) + in + let codegen_undefined = + let name = sgen_id id in + string (Printf.sprintf "enum %s UNDEFINED(%s)(unit u) { return %s; }" name name (sgen_id first_id)) + in + string (Printf.sprintf "// enum %s" (string_of_id id)) ^^ hardline + ^^ separate space [string "enum"; codegen_id id; lbrace; separate_map (comma ^^ space) codegen_id ids; rbrace ^^ semi] + ^^ twice hardline + ^^ codegen_eq + ^^ twice hardline + ^^ codegen_undefined + + | CTD_enum (id, []) -> c_error ("Cannot compile empty enum " ^ string_of_id id) + + | CTD_struct (id, ctors) -> + let struct_ctyp = CT_struct (id, ctors) in + c_debug (lazy (Printf.sprintf "Generating struct for %s" (full_string_of_ctyp struct_ctyp))); + + (* Generate a set_T function for every struct T *) + let codegen_set (id, ctyp) = + if is_stack_ctyp ctyp then + string (Printf.sprintf "rop->%s = op.%s;" (sgen_id id) (sgen_id id)) + else + string (Printf.sprintf "COPY(%s)(&rop->%s, op.%s);" (sgen_ctyp_name ctyp) (sgen_id id) (sgen_id id)) + in + let codegen_setter id ctors = + string (let n = sgen_id id in Printf.sprintf "static void COPY(%s)(struct %s *rop, const struct %s op)" n n n) ^^ space + ^^ surround 2 0 lbrace + (separate_map hardline codegen_set (Bindings.bindings ctors)) + rbrace + in + (* Generate an init/clear_T function for every struct T *) + let codegen_field_init f (id, ctyp) = + if not (is_stack_ctyp ctyp) then + [string (Printf.sprintf "%s(%s)(&op->%s);" f (sgen_ctyp_name ctyp) (sgen_id id))] + else [] + in + let codegen_init f id ctors = + string (let n = sgen_id id in Printf.sprintf "static void %s(%s)(struct %s *op)" f n n) ^^ space + ^^ surround 2 0 lbrace + (separate hardline (Bindings.bindings ctors |> List.map (codegen_field_init f) |> List.concat)) + rbrace + in + let codegen_eq = + let codegen_eq_test (id, ctyp) = + string (Printf.sprintf "EQUAL(%s)(op1.%s, op2.%s)" (sgen_ctyp_name ctyp) (sgen_id id) (sgen_id id)) + in + string (Printf.sprintf "static bool EQUAL(%s)(struct %s op1, struct %s op2)" (sgen_id id) (sgen_id id) (sgen_id id)) + ^^ space + ^^ surround 2 0 lbrace + (string "return" ^^ space + ^^ separate_map (string " && ") codegen_eq_test ctors + ^^ string ";") + rbrace + in + (* Generate the struct and add the generated functions *) + let codegen_ctor (id, ctyp) = + string (sgen_ctyp ctyp) ^^ space ^^ codegen_id id + in + 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 ctors ^^ semi) + rbrace + ^^ semi ^^ twice hardline + ^^ codegen_setter id (ctor_bindings ctors) + ^^ (if not (is_stack_ctyp struct_ctyp) then + twice hardline + ^^ codegen_init "CREATE" id (ctor_bindings ctors) + ^^ twice hardline + ^^ codegen_init "RECREATE" id (ctor_bindings ctors) + ^^ twice hardline + ^^ codegen_init "KILL" id (ctor_bindings ctors) + else empty) + ^^ twice hardline + ^^ codegen_eq + + | CTD_variant (id, tus) -> + let codegen_tu (ctor_id, ctyp) = + separate space [string "struct"; lbrace; string (sgen_ctyp ctyp); codegen_id ctor_id ^^ semi; rbrace] + in + (* Create an if, else if, ... block that does something for each constructor *) + let rec each_ctor v f = function + | [] -> string "{}" + | [(ctor_id, ctyp)] -> + string (Printf.sprintf "if (%skind == Kind_%s)" v (sgen_id ctor_id)) ^^ lbrace ^^ hardline + ^^ jump 0 2 (f ctor_id ctyp) + ^^ hardline ^^ rbrace + | (ctor_id, ctyp) :: ctors -> + string (Printf.sprintf "if (%skind == Kind_%s) " v (sgen_id ctor_id)) ^^ lbrace ^^ hardline + ^^ jump 0 2 (f ctor_id ctyp) + ^^ hardline ^^ rbrace ^^ string " else " ^^ each_ctor v f ctors + in + let codegen_init = + let n = sgen_id id in + let ctor_id, ctyp = List.hd tus in + string (Printf.sprintf "static void CREATE(%s)(struct %s *op)" n n) + ^^ hardline + ^^ surround 2 0 lbrace + (string (Printf.sprintf "op->kind = Kind_%s;" (sgen_id ctor_id)) ^^ hardline + ^^ if not (is_stack_ctyp ctyp) then + string (Printf.sprintf "CREATE(%s)(&op->%s);" (sgen_ctyp_name ctyp) (sgen_id ctor_id)) + else empty) + rbrace + in + let codegen_reinit = + let n = sgen_id id in + string (Printf.sprintf "static void RECREATE(%s)(struct %s *op) {}" n n) + in + let clear_field v ctor_id ctyp = + if is_stack_ctyp ctyp then + string (Printf.sprintf "/* do nothing */") + else + string (Printf.sprintf "KILL(%s)(&%s->%s);" (sgen_ctyp_name ctyp) v (sgen_id ctor_id)) + in + let codegen_clear = + let n = sgen_id id in + string (Printf.sprintf "static void KILL(%s)(struct %s *op)" n n) ^^ hardline + ^^ surround 2 0 lbrace + (each_ctor "op->" (clear_field "op") tus ^^ semi) + rbrace + in + let codegen_ctor (ctor_id, ctyp) = + let ctor_args, tuple, tuple_cleanup = + let tuple_set i ctyp = + if is_stack_ctyp ctyp then + string (Printf.sprintf "op.ztup%d = op%d;" i i) + else + string (Printf.sprintf "COPY(%s)(&op.ztup%d, op%d);" (sgen_ctyp_name ctyp) i i) + in + Printf.sprintf "%s op" (sgen_ctyp ctyp), empty, empty + in + string (Printf.sprintf "static void %s(%sstruct %s *rop, %s)" (sgen_function_id ctor_id) (extra_params ()) (sgen_id id) ctor_args) ^^ hardline + ^^ surround 2 0 lbrace + (tuple + ^^ 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)) + else + string (Printf.sprintf "CREATE(%s)(&rop->%s);" (sgen_ctyp_name ctyp) (sgen_id ctor_id)) ^^ hardline + ^^ string (Printf.sprintf "COPY(%s)(&rop->%s, op);" (sgen_ctyp_name ctyp) (sgen_id ctor_id)) ^^ hardline + ^^ tuple_cleanup) + rbrace + in + let codegen_setter = + let n = sgen_id id in + let set_field ctor_id ctyp = + if is_stack_ctyp ctyp then + string (Printf.sprintf "rop->%s = op.%s;" (sgen_id ctor_id) (sgen_id ctor_id)) + else + string (Printf.sprintf "CREATE(%s)(&rop->%s);" (sgen_ctyp_name ctyp) (sgen_id ctor_id)) + ^^ string (Printf.sprintf " COPY(%s)(&rop->%s, op.%s);" (sgen_ctyp_name ctyp) (sgen_id ctor_id) (sgen_id ctor_id)) + in + string (Printf.sprintf "static void COPY(%s)(struct %s *rop, struct %s op)" n n n) ^^ hardline + ^^ surround 2 0 lbrace + (each_ctor "rop->" (clear_field "rop") tus + ^^ semi ^^ hardline + ^^ string "rop->kind = op.kind" + ^^ semi ^^ hardline + ^^ each_ctor "op." set_field tus) + rbrace + in + let codegen_eq = + let codegen_eq_test ctor_id ctyp = + string (Printf.sprintf "return EQUAL(%s)(op1.%s, op2.%s);" (sgen_ctyp_name ctyp) (sgen_id ctor_id) (sgen_id ctor_id)) + in + let rec codegen_eq_tests = function + | [] -> string "return false;" + | (ctor_id, ctyp) :: ctors -> + string (Printf.sprintf "if (op1.kind == Kind_%s && op2.kind == Kind_%s) " (sgen_id ctor_id) (sgen_id ctor_id)) ^^ lbrace ^^ hardline + ^^ jump 0 2 (codegen_eq_test ctor_id ctyp) + ^^ hardline ^^ rbrace ^^ string " else " ^^ codegen_eq_tests ctors + in + let n = sgen_id id in + string (Printf.sprintf "static bool EQUAL(%s)(struct %s op1, struct %s op2) " n n n) + ^^ surround 2 0 lbrace (codegen_eq_tests 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 tus); + rbrace ^^ semi ] + ^^ twice hardline + ^^ string "struct" ^^ space ^^ codegen_id id ^^ space + ^^ surround 2 0 lbrace + (separate space [string "enum"; string ("kind_" ^ sgen_id id); string "kind" ^^ semi] + ^^ hardline + ^^ string "union" ^^ space + ^^ surround 2 0 lbrace + (separate_map (semi ^^ hardline) codegen_tu tus ^^ semi) + rbrace + ^^ semi) + rbrace + ^^ semi + ^^ twice hardline + ^^ codegen_init + ^^ twice hardline + ^^ codegen_reinit + ^^ twice hardline + ^^ codegen_clear + ^^ twice hardline + ^^ codegen_setter + ^^ twice hardline + ^^ codegen_eq + ^^ twice hardline + ^^ 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 + ^^ string "struct zexception *current_exception = NULL;" + ^^ hardline + ^^ string "bool have_exception = false;" + else + empty + +(** GLOBAL: because C doesn't have real anonymous tuple types + (anonymous structs don't quite work the way we need) every tuple + type in the spec becomes some generated named struct in C. This is + done in such a way that every possible tuple type has a unique name + associated with it. This global variable keeps track of these + generated struct names, so we never generate two copies of the + struct that is used to represent them in C. + + The way this works is that codegen_def scans each definition's type + annotations for tuple types and generates the required structs + using codegen_type_def before the actual definition is generated by + codegen_def'. + + This variable should be reset to empty only when the entire AST has + been translated to C. **) +let generated = ref IdSet.empty + +let codegen_tup ctx ctyps = + let id = mk_id ("tuple_" ^ string_of_ctyp (CT_tup ctyps)) in + if IdSet.mem id !generated then + empty + else + begin + let _, fields = List.fold_left (fun (n, fields) ctyp -> n + 1, Bindings.add (mk_id ("tup" ^ string_of_int n)) ctyp fields) + (0, Bindings.empty) + ctyps + in + generated := IdSet.add id !generated; + codegen_type_def ctx (CTD_struct (id, Bindings.bindings fields)) ^^ twice hardline + end + +let codegen_node id ctyp = + string (Printf.sprintf "struct node_%s {\n %s hd;\n struct node_%s *tl;\n};\n" (sgen_id id) (sgen_ctyp ctyp) (sgen_id id)) + ^^ string (Printf.sprintf "typedef struct node_%s *%s;" (sgen_id id) (sgen_id id)) + +let codegen_list_init id = + string (Printf.sprintf "static void CREATE(%s)(%s *rop) { *rop = NULL; }" (sgen_id id) (sgen_id id)) + +let codegen_list_clear id ctyp = + string (Printf.sprintf "static void KILL(%s)(%s *rop) {\n" (sgen_id id) (sgen_id id)) + ^^ string (Printf.sprintf " if (*rop == NULL) return;") + ^^ (if is_stack_ctyp ctyp then empty + else string (Printf.sprintf " KILL(%s)(&(*rop)->hd);\n" (sgen_ctyp_name ctyp))) + ^^ string (Printf.sprintf " KILL(%s)(&(*rop)->tl);\n" (sgen_id id)) + ^^ string " free(*rop);" + ^^ string "}" + +let codegen_list_set id ctyp = + string (Printf.sprintf "static void internal_set_%s(%s *rop, const %s op) {\n" (sgen_id id) (sgen_id id) (sgen_id id)) + ^^ string " if (op == NULL) { *rop = NULL; return; };\n" + ^^ string (Printf.sprintf " *rop = malloc(sizeof(struct node_%s));\n" (sgen_id id)) + ^^ (if is_stack_ctyp ctyp then + string " (*rop)->hd = op->hd;\n" + else + string (Printf.sprintf " CREATE(%s)(&(*rop)->hd);\n" (sgen_ctyp_name ctyp)) + ^^ string (Printf.sprintf " COPY(%s)(&(*rop)->hd, op->hd);\n" (sgen_ctyp_name ctyp))) + ^^ string (Printf.sprintf " internal_set_%s(&(*rop)->tl, op->tl);\n" (sgen_id id)) + ^^ string "}" + ^^ twice hardline + ^^ string (Printf.sprintf "static void COPY(%s)(%s *rop, const %s op) {\n" (sgen_id id) (sgen_id id) (sgen_id id)) + ^^ string (Printf.sprintf " KILL(%s)(rop);\n" (sgen_id id)) + ^^ string (Printf.sprintf " internal_set_%s(rop, op);\n" (sgen_id id)) + ^^ string "}" + +let codegen_cons id ctyp = + let cons_id = mk_id ("cons#" ^ string_of_ctyp ctyp) in + string (Printf.sprintf "static void %s(%s *rop, const %s x, const %s xs) {\n" (sgen_function_id cons_id) (sgen_id id) (sgen_ctyp ctyp) (sgen_id id)) + ^^ string (Printf.sprintf " *rop = malloc(sizeof(struct node_%s));\n" (sgen_id id)) + ^^ (if is_stack_ctyp ctyp then + string " (*rop)->hd = x;\n" + else + string (Printf.sprintf " CREATE(%s)(&(*rop)->hd);\n" (sgen_ctyp_name ctyp)) + ^^ string (Printf.sprintf " COPY(%s)(&(*rop)->hd, x);\n" (sgen_ctyp_name ctyp))) + ^^ string " (*rop)->tl = xs;\n" + ^^ string "}" + +let codegen_pick id ctyp = + if is_stack_ctyp ctyp then + string (Printf.sprintf "static %s pick_%s(const %s xs) { return xs->hd; }" (sgen_ctyp ctyp) (sgen_ctyp_name ctyp) (sgen_id id)) + else + string (Printf.sprintf "static void pick_%s(%s *x, const %s xs) { COPY(%s)(x, xs->hd); }" (sgen_ctyp_name ctyp) (sgen_ctyp ctyp) (sgen_id id) (sgen_ctyp_name ctyp)) + +let codegen_list ctx ctyp = + let id = mk_id (string_of_ctyp (CT_list ctyp)) in + if IdSet.mem id !generated then + empty + else + begin + generated := IdSet.add id !generated; + codegen_node id ctyp ^^ twice hardline + ^^ codegen_list_init id ^^ twice hardline + ^^ codegen_list_clear id ctyp ^^ twice hardline + ^^ codegen_list_set id ctyp ^^ twice hardline + ^^ codegen_cons id ctyp ^^ twice hardline + ^^ codegen_pick id ctyp ^^ twice hardline + end + +(* Generate functions for working with non-bit vectors of some specific type. *) +let codegen_vector ctx (direction, ctyp) = + let id = mk_id (string_of_ctyp (CT_vector (direction, ctyp))) in + if IdSet.mem id !generated then + empty + else + let vector_typedef = + string (Printf.sprintf "struct %s {\n size_t len;\n %s *data;\n};\n" (sgen_id id) (sgen_ctyp ctyp)) + ^^ string (Printf.sprintf "typedef struct %s %s;" (sgen_id id) (sgen_id id)) + in + let vector_init = + string (Printf.sprintf "static void CREATE(%s)(%s *rop) {\n rop->len = 0;\n rop->data = NULL;\n}" (sgen_id id) (sgen_id id)) + in + let vector_set = + string (Printf.sprintf "static void COPY(%s)(%s *rop, %s op) {\n" (sgen_id id) (sgen_id id) (sgen_id id)) + ^^ string (Printf.sprintf " KILL(%s)(rop);\n" (sgen_id id)) + ^^ string " rop->len = op.len;\n" + ^^ string (Printf.sprintf " rop->data = malloc((rop->len) * sizeof(%s));\n" (sgen_ctyp ctyp)) + ^^ string " for (int i = 0; i < op.len; i++) {\n" + ^^ string (if is_stack_ctyp ctyp then + " (rop->data)[i] = op.data[i];\n" + else + Printf.sprintf " CREATE(%s)((rop->data) + i);\n COPY(%s)((rop->data) + i, op.data[i]);\n" (sgen_ctyp_name ctyp) (sgen_ctyp_name ctyp)) + ^^ string " }\n" + ^^ string "}" + in + let vector_clear = + string (Printf.sprintf "static void KILL(%s)(%s *rop) {\n" (sgen_id id) (sgen_id id)) + ^^ (if is_stack_ctyp ctyp then empty + else + string " for (int i = 0; i < (rop->len); i++) {\n" + ^^ string (Printf.sprintf " KILL(%s)((rop->data) + i);\n" (sgen_ctyp_name ctyp)) + ^^ string " }\n") + ^^ string " if (rop->data != NULL) free(rop->data);\n" + ^^ string "}" + in + let vector_update = + string (Printf.sprintf "static void vector_update_%s(%s *rop, %s op, mpz_t n, %s elem) {\n" (sgen_id id) (sgen_id id) (sgen_id id) (sgen_ctyp ctyp)) + ^^ string " int m = mpz_get_ui(n);\n" + ^^ string " if (rop->data == op.data) {\n" + ^^ string (if is_stack_ctyp ctyp then + " rop->data[m] = elem;\n" + else + Printf.sprintf " COPY(%s)((rop->data) + m, elem);\n" (sgen_ctyp_name ctyp)) + ^^ string " } else {\n" + ^^ string (Printf.sprintf " COPY(%s)(rop, op);\n" (sgen_id id)) + ^^ string (if is_stack_ctyp ctyp then + " rop->data[m] = elem;\n" + else + Printf.sprintf " COPY(%s)((rop->data) + m, elem);\n" (sgen_ctyp_name ctyp)) + ^^ string " }\n" + ^^ string "}" + in + let internal_vector_update = + string (Printf.sprintf "static void internal_vector_update_%s(%s *rop, %s op, const int64_t n, %s elem) {\n" (sgen_id id) (sgen_id id) (sgen_id id) (sgen_ctyp ctyp)) + ^^ string (if is_stack_ctyp ctyp then + " rop->data[n] = elem;\n" + else + Printf.sprintf " COPY(%s)((rop->data) + n, elem);\n" (sgen_ctyp_name ctyp)) + ^^ string "}" + in + let vector_access = + if is_stack_ctyp ctyp then + string (Printf.sprintf "static %s vector_access_%s(%s op, mpz_t n) {\n" (sgen_ctyp ctyp) (sgen_id id) (sgen_id id)) + ^^ string " int m = mpz_get_ui(n);\n" + ^^ string " return op.data[m];\n" + ^^ string "}" + else + string (Printf.sprintf "static void vector_access_%s(%s *rop, %s op, mpz_t n) {\n" (sgen_id id) (sgen_ctyp ctyp) (sgen_id id)) + ^^ string " int m = mpz_get_ui(n);\n" + ^^ string (Printf.sprintf " COPY(%s)(rop, op.data[m]);\n" (sgen_ctyp_name ctyp)) + ^^ string "}" + in + let internal_vector_init = + string (Printf.sprintf "static void internal_vector_init_%s(%s *rop, const int64_t len) {\n" (sgen_id id) (sgen_id id)) + ^^ string " rop->len = len;\n" + ^^ string (Printf.sprintf " rop->data = malloc(len * sizeof(%s));\n" (sgen_ctyp ctyp)) + ^^ (if not (is_stack_ctyp ctyp) then + string " for (int i = 0; i < len; i++) {\n" + ^^ string (Printf.sprintf " CREATE(%s)((rop->data) + i);\n" (sgen_ctyp_name ctyp)) + ^^ string " }\n" + else empty) + ^^ string "}" + in + let vector_undefined = + string (Printf.sprintf "static void undefined_vector_%s(%s *rop, mpz_t len, %s elem) {\n" (sgen_id id) (sgen_id id) (sgen_ctyp ctyp)) + ^^ string (Printf.sprintf " rop->len = mpz_get_ui(len);\n") + ^^ string (Printf.sprintf " rop->data = malloc((rop->len) * sizeof(%s));\n" (sgen_ctyp ctyp)) + ^^ string " for (int i = 0; i < (rop->len); i++) {\n" + ^^ string (if is_stack_ctyp ctyp then + " (rop->data)[i] = elem;\n" + else + Printf.sprintf " CREATE(%s)((rop->data) + i);\n COPY(%s)((rop->data) + i, elem);\n" (sgen_ctyp_name ctyp) (sgen_ctyp_name ctyp)) + ^^ string " }\n" + ^^ string "}" + in + begin + generated := IdSet.add id !generated; + vector_typedef ^^ twice hardline + ^^ vector_init ^^ twice hardline + ^^ vector_clear ^^ twice hardline + ^^ vector_undefined ^^ twice hardline + ^^ vector_access ^^ twice hardline + ^^ vector_set ^^ twice hardline + ^^ vector_update ^^ twice hardline + ^^ internal_vector_update ^^ twice hardline + ^^ internal_vector_init ^^ twice hardline + end + +let is_decl = function + | I_aux (I_decl _, _) -> true + | _ -> false + +let codegen_decl = function + | I_aux (I_decl (ctyp, id), _) -> + string (Printf.sprintf "%s %s;" (sgen_ctyp ctyp) (sgen_id id)) + | _ -> assert false + +let codegen_alloc = function + | I_aux (I_decl (ctyp, id), _) when is_stack_ctyp ctyp -> empty + | I_aux (I_decl (ctyp, id), _) -> + string (Printf.sprintf " CREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id)) + | _ -> assert false + +let codegen_def' ctx = function + | 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)) + + | CDEF_spec (id, arg_ctyps, ret_ctyp) -> + let static = if !opt_static then "static " else "" in + if Env.is_extern id ctx.tc_env "c" then + empty + else if is_stack_ctyp ret_ctyp then + string (Printf.sprintf "%s%s %s(%s%s);" static (sgen_ctyp ret_ctyp) (sgen_function_id id) (extra_params ()) (Util.string_of_list ", " sgen_ctyp arg_ctyps)) + else + string (Printf.sprintf "%svoid %s(%s%s *rop, %s);" static (sgen_function_id id) (extra_params ()) (sgen_ctyp ret_ctyp) (Util.string_of_list ", " sgen_ctyp arg_ctyps)) + + | CDEF_fundef (id, ret_arg, args, instrs) as def -> + (* Extract type information about the function from the environment. *) + let quant, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_env in + let arg_typs, ret_typ = match fn_typ with + | Typ_fn (arg_typs, ret_typ, _) -> arg_typs, ret_typ + | _ -> assert false + in + let ctx' = { ctx with local_env = add_typquant (id_loc id) quant ctx.local_env } in + let arg_ctyps, ret_ctyp = List.map (ctyp_of_typ ctx') arg_typs, ctyp_of_typ ctx' ret_typ in + + (* Check that the function has the correct arity at this point. *) + if List.length arg_ctyps <> List.length args then + c_error ~loc:(id_loc id) ("function arguments " + ^ Util.string_of_list ", " string_of_id args + ^ " matched against type " + ^ Util.string_of_list ", " string_of_ctyp arg_ctyps) + else (); + + let instrs = add_local_labels instrs in + let args = Util.string_of_list ", " (fun x -> x) (List.map2 (fun ctyp arg -> sgen_ctyp ctyp ^ " " ^ sgen_id arg) arg_ctyps args) in + let function_header = + match ret_arg with + | None -> + assert (is_stack_ctyp ret_ctyp); + (if !opt_static then string "static " else empty) + ^^ string (sgen_ctyp ret_ctyp) ^^ space ^^ codegen_function_id id ^^ parens (string (extra_params ()) ^^ string args) ^^ hardline + | Some gs -> + assert (not (is_stack_ctyp ret_ctyp)); + (if !opt_static then string "static " else empty) + ^^ string "void" ^^ space ^^ codegen_function_id id + ^^ parens (string (extra_params ()) ^^ string (sgen_ctyp ret_ctyp ^ " *" ^ sgen_id gs ^ ", ") ^^ string args) + ^^ hardline + in + function_header + ^^ string "{" + ^^ jump 0 2 (separate_map hardline (codegen_instr id ctx) instrs) ^^ hardline + ^^ string "}" + + | CDEF_type ctype_def -> + codegen_type_def ctx ctype_def + + | CDEF_startup (id, instrs) -> + let static = if !opt_static then "static " else "" in + let startup_header = string (Printf.sprintf "%svoid startup_%s(void)" static (sgen_function_id id)) in + separate_map hardline codegen_decl instrs + ^^ twice hardline + ^^ startup_header ^^ hardline + ^^ string "{" + ^^ jump 0 2 (separate_map hardline codegen_alloc instrs) ^^ hardline + ^^ string "}" + + | CDEF_finish (id, instrs) -> + let static = if !opt_static then "static " else "" in + let finish_header = string (Printf.sprintf "%svoid finish_%s(void)" static (sgen_function_id id)) in + separate_map hardline codegen_decl (List.filter is_decl instrs) + ^^ twice hardline + ^^ finish_header ^^ hardline + ^^ string "{" + ^^ jump 0 2 (separate_map hardline (codegen_instr id ctx) instrs) ^^ hardline + ^^ string "}" + + | CDEF_let (number, bindings, instrs) -> + let instrs = add_local_labels instrs in + let setup = + List.concat (List.map (fun (id, ctyp) -> [idecl ctyp id]) bindings) + in + let cleanup = + List.concat (List.map (fun (id, ctyp) -> [iclear ctyp id]) bindings) + in + separate_map hardline (fun (id, ctyp) -> string (Printf.sprintf "%s %s;" (sgen_ctyp ctyp) (sgen_id id))) bindings + ^^ hardline ^^ string (Printf.sprintf "static void create_letbind_%d(void) " number) + ^^ string "{" + ^^ jump 0 2 (separate_map hardline codegen_alloc setup) ^^ hardline + ^^ jump 0 2 (separate_map hardline (codegen_instr (mk_id "let") { ctx with no_raw = true }) instrs) ^^ hardline + ^^ string "}" + ^^ hardline ^^ string (Printf.sprintf "static void kill_letbind_%d(void) " number) + ^^ string "{" + ^^ jump 0 2 (separate_map hardline (codegen_instr (mk_id "let") ctx) cleanup) ^^ hardline + ^^ string "}" + +(** As we generate C we need to generate specialized version of tuple, + list, and vector type. These must be generated in the correct + order. The ctyp_dependencies function generates a list of + c_gen_typs in the order they must be generated. Types may be + repeated in ctyp_dependencies so it's up to the code-generator not + to repeat definitions pointlessly (using the !generated variable) + *) +type c_gen_typ = + | CTG_tup of ctyp list + | CTG_list of ctyp + | CTG_vector of bool * ctyp + +let rec ctyp_dependencies = function + | CT_tup ctyps -> List.concat (List.map ctyp_dependencies ctyps) @ [CTG_tup ctyps] + | CT_list ctyp -> ctyp_dependencies ctyp @ [CTG_list ctyp] + | CT_vector (direction, ctyp) -> ctyp_dependencies ctyp @ [CTG_vector (direction, ctyp)] + | CT_ref ctyp -> ctyp_dependencies ctyp + | CT_struct (_, ctors) -> List.concat (List.map (fun (_, ctyp) -> ctyp_dependencies ctyp) ctors) + | CT_variant (_, ctors) -> List.concat (List.map (fun (_, ctyp) -> ctyp_dependencies ctyp) ctors) + | CT_lint | CT_fint _ | CT_lbits _ | CT_fbits _ | CT_sbits _ | CT_unit | CT_bool | CT_real | CT_bit | CT_string | CT_enum _ | CT_poly -> [] + +let codegen_ctg ctx = function + | CTG_vector (direction, ctyp) -> codegen_vector ctx (direction, ctyp) + | CTG_tup ctyps -> codegen_tup ctx ctyps + | CTG_list ctyp -> codegen_list ctx ctyp + +(** When we generate code for a definition, we need to first generate + any auxillary type definitions that are required. *) +let codegen_def ctx def = + let ctyps = cdef_ctyps def |> CTSet.elements in + (* We should have erased any polymorphism introduced by variants at this point! *) + if List.exists is_polymorphic ctyps then + let polymorphic_ctyps = List.filter is_polymorphic ctyps in + prerr_endline (Pretty_print_sail.to_string (pp_cdef def)); + c_error (Printf.sprintf "Found polymorphic types:\n%s\nwhile generating definition." + (Util.string_of_list "\n" string_of_ctyp polymorphic_ctyps)) + else + let deps = List.concat (List.map ctyp_dependencies ctyps) in + separate_map hardline (codegen_ctg ctx) deps + ^^ codegen_def' ctx def + +let is_cdef_startup = function + | CDEF_startup _ -> true + | _ -> false + +let sgen_startup = function + | CDEF_startup (id, _) -> + Printf.sprintf " startup_%s();" (sgen_id id) + | _ -> assert false + +let sgen_instr id ctx instr = + Pretty_print_sail.to_string (codegen_instr id ctx instr) + +let is_cdef_finish = function + | CDEF_startup _ -> true + | _ -> false + +let sgen_finish = function + | CDEF_startup (id, _) -> + Printf.sprintf " finish_%s();" (sgen_id id) + | _ -> assert false + +let rec get_recursive_functions (Defs defs) = + match defs with + | DEF_internal_mutrec fundefs :: defs -> + IdSet.union (List.map id_of_fundef fundefs |> IdSet.of_list) (get_recursive_functions (Defs defs)) + + | (DEF_fundef fdef as def) :: defs -> + let open Rewriter in + let ids = ref IdSet.empty in + let collect_funcalls e_aux annot = + match e_aux with + | E_app (id, args) -> (ids := IdSet.add id !ids; E_aux (e_aux, annot)) + | _ -> E_aux (e_aux, annot) + in + let map_exp = { + id_exp_alg with + e_aux = (fun (e_aux, annot) -> collect_funcalls e_aux annot) + } in + let map_defs = { rewriters_base with rewrite_exp = (fun _ -> fold_exp map_exp) } in + let _ = rewrite_def map_defs def in + if IdSet.mem (id_of_fundef fdef) !ids then + IdSet.add (id_of_fundef fdef) (get_recursive_functions (Defs defs)) + else + get_recursive_functions (Defs defs) + + | _ :: defs -> get_recursive_functions (Defs defs) + | [] -> IdSet.empty + +let jib_of_ast env ast = + let ctx = + initial_ctx + ~convert_typ:ctyp_of_typ + ~optimize_anf:(fun ctx aexp -> analyze_functions ctx analyze_primop (c_literals ctx aexp)) + env + in + Jib_compile.compile_ast ctx ast + +let compile_ast env output_chan c_includes ast = + try + c_debug (lazy (Util.log_line __MODULE__ __LINE__ "Identifying recursive functions")); + let recursive_functions = Spec_analysis.top_sort_defs ast |> get_recursive_functions in + + let cdefs, ctx = jib_of_ast env ast in + let cdefs = insert_heap_returns Bindings.empty cdefs in + let cdefs = optimize recursive_functions cdefs in + + let docs = separate_map (hardline ^^ hardline) (codegen_def ctx) cdefs in + + let preamble = separate hardline + ([ string "#include \"sail.h\"" ] + @ (if !opt_no_rts then [] else + [ string "#include \"rts.h\""; + string "#include \"elf.h\"" ]) + @ (List.map (fun h -> string (Printf.sprintf "#include \"%s\"" h)) c_includes)) + in + + let exn_boilerplate = + if not (Bindings.mem (mk_id "exception") ctx.variants) then ([], []) else + ([ " current_exception = malloc(sizeof(struct zexception));"; + " CREATE(zexception)(current_exception);" ], + [ " KILL(zexception)(current_exception);"; + " free(current_exception);"; + " if (have_exception) fprintf(stderr, \"Exiting due to uncaught exception\\n\");" ]) + in + + let letbind_initializers = + List.map (fun n -> Printf.sprintf " create_letbind_%d();" n) (List.rev ctx.letbinds) + in + let letbind_finalizers = + List.map (fun n -> Printf.sprintf " kill_letbind_%d();" n) ctx.letbinds + in + let startup cdefs = + List.map sgen_startup (List.filter is_cdef_startup cdefs) + in + let finish cdefs = + List.map sgen_finish (List.filter is_cdef_finish cdefs) + in + + let regs = c_ast_registers cdefs in + + let register_init_clear (id, ctyp, instrs) = + if is_stack_ctyp ctyp then + List.map (sgen_instr (mk_id "reg") ctx) instrs, [] + else + [ Printf.sprintf " CREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id) ] + @ List.map (sgen_instr (mk_id "reg") ctx) instrs, + [ Printf.sprintf " KILL(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id) ] + in + + let model_init = separate hardline (List.map string + ( [ "void model_init(void)"; + "{"; + " setup_rts();" ] + @ fst exn_boilerplate + @ startup cdefs + @ List.concat (List.map (fun r -> fst (register_init_clear r)) regs) + @ (if regs = [] then [] else [ Printf.sprintf " %s(UNIT);" (sgen_function_id (mk_id "initialize_registers")) ]) + @ letbind_initializers + @ [ "}" ] )) + in + + let model_fini = separate hardline (List.map string + ( [ "void model_fini(void)"; + "{" ] + @ letbind_finalizers + @ List.concat (List.map (fun r -> snd (register_init_clear r)) regs) + @ finish cdefs + @ snd exn_boilerplate + @ [ " cleanup_rts();"; + "}" ] )) + in + + let model_default_main = separate hardline (List.map string + [ "int model_main(int argc, char *argv[])"; + "{"; + " model_init();"; + " if (process_arguments(argc, argv)) exit(EXIT_FAILURE);"; + Printf.sprintf " %s(UNIT);" (sgen_function_id (mk_id "main")); + " model_fini();"; + " return EXIT_SUCCESS;"; + "}" ] ) + in + + let model_main = separate hardline (if (!opt_no_main) then [] else List.map string + [ "int main(int argc, char *argv[])"; + "{"; + " return model_main(argc, argv);"; + "}" ] ) + in + + let hlhl = hardline ^^ hardline in + + Pretty_print_sail.to_string (preamble ^^ hlhl ^^ docs ^^ hlhl + ^^ (if not !opt_no_rts then + model_init ^^ hlhl + ^^ model_fini ^^ hlhl + ^^ model_default_main ^^ hlhl + else + empty) + ^^ model_main ^^ hardline) + |> output_string output_chan + with + | Type_error (_, l, err) -> + c_error ~loc:l ("Unexpected type error when compiling to C:\n" ^ Type_error.string_of_type_error err) diff --git a/src/jib/c_backend.mli b/src/jib/c_backend.mli new file mode 100644 index 00000000..7314eb5a --- /dev/null +++ b/src/jib/c_backend.mli @@ -0,0 +1,109 @@ +(**************************************************************************) +(* 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 Jib +open Type_check + +(** Global compilation options *) + +(** Define generated functions as static *) +val opt_static : bool ref + +(** Do not generate a main function *) +val opt_no_main : bool ref + +(** (WIP) Do not include rts.h (the runtime), and do not generate code + that requires any setup or teardown routines to be run by a runtime + before executing any instruction semantics. *) +val opt_no_rts : bool ref + +(** Ordinarily we use plain z-encoding to name-mangle generated Sail + identifiers into a form suitable for C. If opt_prefix is set, then + the "z" which is added on the front of each generated C function + will be replaced by opt_prefix. E.g. opt_prefix := "sail_" would + give sail_my_function rather than zmy_function. *) +val opt_prefix : string ref + +(** opt_extra_params and opt_extra_arguments allow additional state to + be threaded through the generated C code by adding an additional + parameter to each function type, and then giving an extra argument + to each function call. For example we could have + + opt_extra_params := Some "CPUMIPSState *env" + opt_extra_arguments := Some "env" + + and every generated function will take a pointer to a QEMU MIPS + processor state, and each function will be passed the env argument + when it is called. *) +val opt_extra_params : string option ref +val opt_extra_arguments : string option ref + +(** (WIP) [opt_memo_cache] will store the compiled function + definitions in file _sbuild/ccacheDIGEST where DIGEST is the md5sum + of the original function to be compiled. Enabled using the -memo + flag. Uses Marshal so it's quite picky about the exact version of +b the Sail version. This cache can obviously become stale if the C + backend changes - it'll load an old version compiled without said + changes. *) +val opt_memo_cache : bool ref + +(** Optimization flags *) + +val optimize_primops : bool ref +val optimize_hoist_allocations : bool ref +val optimize_struct_updates : bool ref +val optimize_alias : bool ref +val optimize_experimental : bool ref + +(** Convert a typ to a IR ctyp *) +val ctyp_of_typ : Jib_compile.ctx -> Ast.typ -> ctyp + +val jib_of_ast : Env.t -> tannot Ast.defs -> cdef list * Jib_compile.ctx +val compile_ast : Env.t -> out_channel -> string list -> tannot Ast.defs -> unit diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml new file mode 100644 index 00000000..27f833d8 --- /dev/null +++ b/src/jib/jib_compile.ml @@ -0,0 +1,1403 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* Alasdair Armstrong *) +(* Brian Campbell *) +(* Thomas Bauereiss *) +(* Anthony Fox *) +(* Jon French *) +(* Dominic Mulligan *) +(* Stephen Kell *) +(* Mark Wassell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + +open Ast +open Ast_util +open Jib +open Jib_util +open Type_check +open Value2 + +open Anf + +let opt_debug_function = ref "" +let opt_debug_flow_graphs = ref false +let opt_memo_cache = ref false + +(**************************************************************************) +(* 4. Conversion to low-level AST *) +(**************************************************************************) + +(** We now use a low-level AST called Jib (see language/bytecode.ott) + that is only slightly abstracted away from C. To be succint in + comments we usually refer to this as Sail IR or IR rather than + low-level AST repeatedly. + + The general idea is ANF expressions are converted into lists of + instructions (type instr) where allocations and deallocations are + now made explicit. ANF values (aval) are mapped to the cval type, + which is even simpler still. Some things are still more abstract + than in C, so the type definitions follow the sail type definition + structure, just with typ (from ast.ml) replaced with + ctyp. Top-level declarations that have no meaning for the backend + are not included at this level. + + The convention used here is that functions of the form compile_X + compile the type X into types in this AST, so compile_aval maps + avals into cvals. Note that the return types for these functions + are often quite complex, and they usually return some tuple + containing setup instructions (to allocate memory for the + expression), cleanup instructions (to deallocate that memory) and + possibly typing information about what has been translated. **) + +(* FIXME: This stage shouldn't care about this *) +let max_int n = Big_int.pred (Big_int.pow_int_positive 2 (n - 1)) +let min_int n = Big_int.negate (Big_int.pow_int_positive 2 (n - 1)) + +let rec is_bitvector = function + | [] -> true + | AV_lit (L_aux (L_zero, _), _) :: avals -> is_bitvector avals + | AV_lit (L_aux (L_one, _), _) :: avals -> is_bitvector avals + | _ :: _ -> false + +let rec value_of_aval_bit = function + | AV_lit (L_aux (L_zero, _), _) -> Sail2_values.B0 + | AV_lit (L_aux (L_one, _), _) -> Sail2_values.B1 + | _ -> assert false + +let is_ct_enum = function + | CT_enum _ -> true + | _ -> false + +let is_ct_variant = function + | CT_variant _ -> true + | _ -> false + +let is_ct_tup = function + | CT_tup _ -> true + | _ -> false + +let is_ct_list = function + | CT_list _ -> true + | _ -> false + +let is_ct_vector = function + | CT_vector _ -> true + | _ -> false + +let is_ct_struct = function + | CT_struct _ -> true + | _ -> false + +let is_ct_ref = function + | CT_ref _ -> true + | _ -> false + +let ctor_bindings = List.fold_left (fun map (id, ctyp) -> Bindings.add id ctyp map) Bindings.empty + +(** The context type contains two type-checking + environments. ctx.local_env contains the closest typechecking + environment, usually from the expression we are compiling, whereas + ctx.tc_env is the global type checking environment from + type-checking the entire AST. We also keep track of local variables + in ctx.locals, so we know when their type changes due to flow + typing. *) +type ctx = + { records : (ctyp Bindings.t) Bindings.t; + enums : IdSet.t Bindings.t; + variants : (ctyp Bindings.t) Bindings.t; + tc_env : Env.t; + local_env : Env.t; + locals : (mut * ctyp) Bindings.t; + letbinds : int list; + no_raw : bool; + convert_typ : ctx -> typ -> ctyp; + optimize_anf : ctx -> typ aexp -> typ aexp + } + +let initial_ctx ~convert_typ:convert_typ ~optimize_anf:optimize_anf env = + { records = Bindings.empty; + enums = Bindings.empty; + variants = Bindings.empty; + tc_env = env; + local_env = env; + locals = Bindings.empty; + letbinds = []; + no_raw = false; + convert_typ = convert_typ; + optimize_anf = optimize_anf + } + +let ctyp_of_typ ctx typ = ctx.convert_typ ctx typ + +let rec chunkify n xs = + match Util.take n xs, Util.drop n xs with + | xs, [] -> [xs] + | xs, ys -> xs :: chunkify n ys + +let rec compile_aval l ctx = function + | AV_C_fragment (frag, typ, ctyp) -> + let ctyp' = ctyp_of_typ ctx typ in + if not (ctyp_equal ctyp ctyp') then + raise (Reporting.err_unreachable l __POS__ (string_of_ctyp ctyp ^ " != " ^ string_of_ctyp ctyp')); + [], (frag, ctyp_of_typ ctx typ), [] + + | AV_id (id, typ) -> + begin + try + let _, ctyp = Bindings.find id ctx.locals in + [], (F_id id, ctyp), [] + with + | Not_found -> + [], (F_id id, ctyp_of_typ ctx (lvar_typ typ)), [] + end + + | AV_ref (id, typ) -> + [], (F_ref id, CT_ref (ctyp_of_typ ctx (lvar_typ typ))), [] + + | AV_lit (L_aux (L_string str, _), typ) -> + [], (F_lit (V_string (String.escaped str)), ctyp_of_typ ctx typ), [] + + | AV_lit (L_aux (L_num n, _), typ) when Big_int.less_equal (min_int 64) n && Big_int.less_equal n (max_int 64) -> + let gs = gensym () in + [iinit CT_lint gs (F_lit (V_int n), CT_fint 64)], + (F_id gs, CT_lint), + [iclear CT_lint gs] + + | AV_lit (L_aux (L_num n, _), typ) -> + let gs = gensym () in + [iinit CT_lint gs (F_lit (V_string (Big_int.to_string n)), CT_string)], + (F_id gs, CT_lint), + [iclear CT_lint gs] + + | AV_lit (L_aux (L_zero, _), _) -> [], (F_lit (V_bit Sail2_values.B0), CT_bit), [] + | AV_lit (L_aux (L_one, _), _) -> [], (F_lit (V_bit Sail2_values.B1), CT_bit), [] + + | AV_lit (L_aux (L_true, _), _) -> [], (F_lit (V_bool true), CT_bool), [] + | AV_lit (L_aux (L_false, _), _) -> [], (F_lit (V_bool false), CT_bool), [] + + | AV_lit (L_aux (L_real str, _), _) -> + let gs = gensym () in + [iinit CT_real gs (F_lit (V_string str), CT_string)], + (F_id gs, CT_real), + [iclear CT_real gs] + + | AV_lit (L_aux (L_unit, _), _) -> [], (F_lit V_unit, CT_unit), [] + + | AV_lit (L_aux (_, l) as lit, _) -> + raise (Reporting.err_general l ("Encountered unexpected literal " ^ string_of_lit lit ^ " when converting ANF represention into IR")) + + | AV_tuple avals -> + let elements = List.map (compile_aval l ctx) avals in + let cvals = List.map (fun (_, cval, _) -> cval) elements in + let setup = List.concat (List.map (fun (setup, _, _) -> setup) elements) in + let cleanup = List.concat (List.rev (List.map (fun (_, _, cleanup) -> cleanup) elements)) in + let tup_ctyp = CT_tup (List.map cval_ctyp cvals) in + let gs = gensym () in + setup + @ [idecl tup_ctyp gs] + @ List.mapi (fun n cval -> icopy l (CL_tuple (CL_id (gs, tup_ctyp), n)) cval) cvals, + (F_id gs, CT_tup (List.map cval_ctyp cvals)), + [iclear tup_ctyp gs] + @ cleanup + + | AV_record (fields, typ) -> + let ctyp = ctyp_of_typ ctx typ in + let gs = gensym () in + let compile_fields (id, aval) = + let field_setup, cval, field_cleanup = compile_aval l ctx aval in + field_setup + @ [icopy l (CL_field (CL_id (gs, ctyp), string_of_id id)) cval] + @ field_cleanup + in + [idecl ctyp gs] + @ List.concat (List.map compile_fields (Bindings.bindings fields)), + (F_id gs, ctyp), + [iclear ctyp gs] + + | AV_vector ([], _) -> + raise (Reporting.err_general l "Encountered empty vector literal") + + (* Convert a small bitvector to a uint64_t literal. *) + | AV_vector (avals, typ) when is_bitvector avals && List.length avals <= 64 -> + begin + let bitstring = F_lit (V_bits (List.map value_of_aval_bit avals)) in + let len = List.length avals in + match destruct_vector ctx.tc_env typ with + | Some (_, Ord_aux (Ord_inc, _), _) -> + [], (bitstring, CT_fbits (len, false)), [] + | Some (_, Ord_aux (Ord_dec, _), _) -> + [], (bitstring, CT_fbits (len, true)), [] + | Some _ -> + raise (Reporting.err_general l "Encountered order polymorphic bitvector literal") + | None -> + raise (Reporting.err_general l "Encountered vector literal without vector type") + end + + (* Convert a bitvector literal that is larger than 64-bits to a + variable size bitvector, converting it in 64-bit chunks. *) + | AV_vector (avals, typ) when is_bitvector avals -> + let len = List.length avals in + let bitstring avals = F_lit (V_bits (List.map value_of_aval_bit avals)) in + let first_chunk = bitstring (Util.take (len mod 64) avals) in + let chunks = Util.drop (len mod 64) avals |> chunkify 64 |> List.map bitstring in + let gs = gensym () in + [iinit (CT_lbits true) gs (first_chunk, CT_fbits (len mod 64, true))] + @ List.map (fun chunk -> ifuncall (CL_id (gs, CT_lbits true)) + (mk_id "append_64") + [(F_id gs, CT_lbits true); (chunk, CT_fbits (64, true))]) chunks, + (F_id gs, CT_lbits true), + [iclear (CT_lbits true) gs] + + (* If we have a bitvector value, that isn't a literal then we need to set bits individually. *) + | AV_vector (avals, Typ_aux (Typ_app (id, [_; A_aux (A_order ord, _); A_aux (A_typ (Typ_aux (Typ_id bit_id, _)), _)]), _)) + when string_of_id bit_id = "bit" && string_of_id id = "vector" && List.length avals <= 64 -> + let len = List.length avals in + let direction = match ord with + | Ord_aux (Ord_inc, _) -> false + | Ord_aux (Ord_dec, _) -> true + | Ord_aux (Ord_var _, _) -> raise (Reporting.err_general l "Polymorphic vector direction found") + in + let gs = gensym () in + let ctyp = CT_fbits (len, direction) in + let mask i = V_bits (Util.list_init (63 - i) (fun _ -> Sail2_values.B0) @ [Sail2_values.B1] @ Util.list_init i (fun _ -> Sail2_values.B0)) in + let aval_mask i aval = + let setup, cval, cleanup = compile_aval l ctx aval in + match cval with + | (F_lit (V_bit Sail2_values.B0), _) -> [] + | (F_lit (V_bit Sail2_values.B1), _) -> + [icopy l (CL_id (gs, ctyp)) (F_op (F_id gs, "|", F_lit (mask i)), ctyp)] + | _ -> + setup @ [iif cval [icopy l (CL_id (gs, ctyp)) (F_op (F_id gs, "|", F_lit (mask i)), ctyp)] [] CT_unit] @ cleanup + in + [idecl ctyp gs; + icopy l (CL_id (gs, ctyp)) (F_lit (V_bits (Util.list_init 64 (fun _ -> Sail2_values.B0))), ctyp)] + @ List.concat (List.mapi aval_mask (List.rev avals)), + (F_id gs, ctyp), + [] + + (* Compiling a vector literal that isn't a bitvector *) + | AV_vector (avals, Typ_aux (Typ_app (id, [_; A_aux (A_order ord, _); A_aux (A_typ typ, _)]), _)) + when string_of_id id = "vector" -> + let len = List.length avals in + let direction = match ord with + | Ord_aux (Ord_inc, _) -> false + | Ord_aux (Ord_dec, _) -> true + | Ord_aux (Ord_var _, _) -> raise (Reporting.err_general l "Polymorphic vector direction found") + in + let vector_ctyp = CT_vector (direction, ctyp_of_typ ctx typ) in + let gs = gensym () in + let aval_set i aval = + let setup, cval, cleanup = compile_aval l ctx aval in + setup + @ [iextern (CL_id (gs, vector_ctyp)) + (mk_id "internal_vector_update") + [(F_id gs, vector_ctyp); (F_lit (V_int (Big_int.of_int i)), CT_fint 64); cval]] + @ cleanup + in + [idecl vector_ctyp gs; + iextern (CL_id (gs, vector_ctyp)) (mk_id "internal_vector_init") [(F_lit (V_int (Big_int.of_int len)), CT_fint 64)]] + @ List.concat (List.mapi aval_set (if direction then List.rev avals else avals)), + (F_id gs, vector_ctyp), + [iclear vector_ctyp gs] + + | AV_vector _ as aval -> + raise (Reporting.err_general l ("Have AV_vector: " ^ Pretty_print_sail.to_string (pp_aval aval) ^ " which is not a vector type")) + + | AV_list (avals, Typ_aux (typ, _)) -> + let ctyp = match typ with + | Typ_app (id, [A_aux (A_typ typ, _)]) when string_of_id id = "list" -> ctyp_of_typ ctx typ + | _ -> raise (Reporting.err_general l "Invalid list type") + in + let gs = gensym () in + let mk_cons aval = + let setup, cval, cleanup = compile_aval l ctx aval in + setup @ [ifuncall (CL_id (gs, CT_list ctyp)) (mk_id ("cons#" ^ string_of_ctyp ctyp)) [cval; (F_id gs, CT_list ctyp)]] @ cleanup + in + [idecl (CT_list ctyp) gs] + @ List.concat (List.map mk_cons (List.rev avals)), + (F_id gs, CT_list ctyp), + [iclear (CT_list ctyp) gs] + +let compile_funcall l ctx id args typ = + let setup = ref [] in + let cleanup = ref [] in + + let quant, Typ_aux (fn_typ, _) = + (* If we can't find a function in local_env, fall back to the + global env - this happens when representing assertions, exit, + etc as functions in the IR. *) + try Env.get_val_spec id ctx.local_env with Type_error _ -> Env.get_val_spec id ctx.tc_env + in + let arg_typs, ret_typ = match fn_typ with + | Typ_fn (arg_typs, ret_typ, _) -> arg_typs, ret_typ + | _ -> assert false + in + let ctx' = { ctx with local_env = add_typquant (id_loc id) quant ctx.tc_env } in + let arg_ctyps, ret_ctyp = List.map (ctyp_of_typ ctx') arg_typs, ctyp_of_typ ctx' ret_typ in + let final_ctyp = ctyp_of_typ ctx typ in + + let setup_arg ctyp aval = + let arg_setup, cval, arg_cleanup = compile_aval l ctx aval in + setup := List.rev arg_setup @ !setup; + cleanup := arg_cleanup @ !cleanup; + let have_ctyp = cval_ctyp cval in + if is_polymorphic ctyp then + (F_poly (fst cval), have_ctyp) + else if ctyp_equal ctyp have_ctyp then + cval + else + let gs = gensym () in + setup := iinit ctyp gs cval :: !setup; + cleanup := iclear ctyp gs :: !cleanup; + (F_id gs, ctyp) + in + + assert (List.length arg_ctyps = List.length args); + + let setup_args = List.map2 setup_arg arg_ctyps args in + + List.rev !setup, + begin fun clexp -> + if ctyp_equal (clexp_ctyp clexp) ret_ctyp then + ifuncall clexp id setup_args + else + let gs = gensym () in + iblock [idecl ret_ctyp gs; + ifuncall (CL_id (gs, ret_ctyp)) id setup_args; + icopy l clexp (F_id gs, ret_ctyp); + iclear ret_ctyp gs] + end, + !cleanup + +let rec apat_ctyp ctx (AP_aux (apat, _, _)) = + match apat with + | AP_tup apats -> CT_tup (List.map (apat_ctyp ctx) apats) + | AP_global (_, typ) -> ctyp_of_typ ctx typ + | AP_cons (apat, _) -> CT_list (apat_ctyp ctx apat) + | AP_wild typ | AP_nil typ | AP_id (_, typ) -> ctyp_of_typ ctx typ + | AP_app (_, _, typ) -> ctyp_of_typ ctx typ + +let rec compile_match ctx (AP_aux (apat_aux, env, l)) cval case_label = + let ctx = { ctx with local_env = env } in + match apat_aux, cval with + | AP_id (pid, _), (frag, ctyp) when Env.is_union_constructor pid ctx.tc_env -> + [ijump (F_op (F_field (frag, "kind"), "!=", F_lit (V_ctor_kind (string_of_id pid))), CT_bool) case_label], + [], + ctx + + | AP_global (pid, typ), (frag, ctyp) -> + let global_ctyp = ctyp_of_typ ctx typ in + [icopy l (CL_id (pid, global_ctyp)) cval], [], ctx + + | AP_id (pid, _), (frag, ctyp) when is_ct_enum ctyp -> + begin match Env.lookup_id pid ctx.tc_env with + | Unbound -> [idecl ctyp pid; icopy l (CL_id (pid, ctyp)) (frag, ctyp)], [], ctx + | _ -> [ijump (F_op (F_id pid, "!=", frag), CT_bool) case_label], [], ctx + end + + | AP_id (pid, typ), _ -> + let ctyp = cval_ctyp cval in + let id_ctyp = ctyp_of_typ ctx typ in + let ctx = { ctx with locals = Bindings.add pid (Immutable, id_ctyp) ctx.locals } in + [idecl id_ctyp pid; icopy l (CL_id (pid, id_ctyp)) cval], [iclear id_ctyp pid], ctx + + | AP_tup apats, (frag, ctyp) -> + begin + let get_tup n ctyp = (F_field (frag, "ztup" ^ string_of_int n), ctyp) in + let fold (instrs, cleanup, n, ctx) apat ctyp = + let instrs', cleanup', ctx = compile_match ctx apat (get_tup n ctyp) case_label in + instrs @ instrs', cleanup' @ cleanup, n + 1, ctx + in + match ctyp with + | CT_tup ctyps -> + let instrs, cleanup, _, ctx = List.fold_left2 fold ([], [], 0, ctx) apats ctyps in + instrs, cleanup, ctx + | _ -> failwith ("AP_tup with ctyp " ^ string_of_ctyp ctyp) + end + + | AP_app (ctor, apat, variant_typ), (frag, ctyp) -> + begin match ctyp with + | CT_variant (_, ctors) -> + let ctor_c_id = string_of_id ctor in + let ctor_ctyp = Bindings.find ctor (ctor_bindings ctors) in + (* These should really be the same, something has gone wrong if they are not. *) + if ctyp_equal ctor_ctyp (ctyp_of_typ ctx variant_typ) then + raise (Reporting.err_general l (Printf.sprintf "%s is not the same type as %s" (string_of_ctyp ctor_ctyp) (string_of_ctyp (ctyp_of_typ ctx variant_typ)))) + else (); + let ctor_c_id, ctor_ctyp = + if is_polymorphic ctor_ctyp then + let unification = List.map ctyp_suprema (ctyp_unify ctor_ctyp (apat_ctyp ctx apat)) in + (if List.length unification > 0 then + ctor_c_id ^ "_" ^ Util.string_of_list "_" (fun ctyp -> Util.zencode_string (string_of_ctyp ctyp)) unification + else + ctor_c_id), + ctyp_suprema (apat_ctyp ctx apat) + else + ctor_c_id, ctor_ctyp + in + let instrs, cleanup, ctx = compile_match ctx apat ((F_field (frag, Util.zencode_string ctor_c_id), ctor_ctyp)) case_label in + [ijump (F_op (F_field (frag, "kind"), "!=", F_lit (V_ctor_kind ctor_c_id)), CT_bool) case_label] + @ instrs, + cleanup, + ctx + | ctyp -> + raise (Reporting.err_general l (Printf.sprintf "Variant constructor %s : %s matching against non-variant type %s : %s" + (string_of_id ctor) + (string_of_typ variant_typ) + (string_of_fragment ~zencode:false frag) + (string_of_ctyp ctyp))) + end + + | AP_wild _, _ -> [], [], ctx + + | AP_cons (hd_apat, tl_apat), (frag, CT_list ctyp) -> + let hd_setup, hd_cleanup, ctx = compile_match ctx hd_apat (F_field (F_unary ("*", frag), "hd"), ctyp) case_label in + let tl_setup, tl_cleanup, ctx = compile_match ctx tl_apat (F_field (F_unary ("*", frag), "tl"), CT_list ctyp) case_label in + [ijump (F_op (frag, "==", F_lit V_null), CT_bool) case_label] @ hd_setup @ tl_setup, tl_cleanup @ hd_cleanup, ctx + + | AP_cons _, (_, _) -> + raise (Reporting.err_general l "Tried to pattern match cons on non list type") + + | AP_nil _, (frag, _) -> [ijump (F_op (frag, "!=", F_lit V_null), CT_bool) case_label], [], ctx + +let unit_fragment = (F_lit V_unit, CT_unit) + +let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = + let ctx = { ctx with local_env = env } in + match aexp_aux with + | AE_let (mut, id, binding_typ, binding, (AE_aux (_, body_env, _) as body), body_typ) -> + let binding_ctyp = ctyp_of_typ { ctx with local_env = body_env } binding_typ in + let setup, call, cleanup = compile_aexp ctx binding in + let letb_setup, letb_cleanup = + [idecl binding_ctyp id; iblock (setup @ [call (CL_id (id, binding_ctyp))] @ cleanup)], [iclear binding_ctyp id] + in + let ctx = { ctx with locals = Bindings.add id (mut, binding_ctyp) ctx.locals } in + let setup, call, cleanup = compile_aexp ctx body in + letb_setup @ setup, call, cleanup @ letb_cleanup + + | AE_app (id, vs, typ) -> + compile_funcall l ctx id vs typ + + | AE_val aval -> + let setup, cval, cleanup = compile_aval l ctx aval in + setup, (fun clexp -> icopy l clexp cval), cleanup + + (* Compile case statements *) + | AE_case (aval, cases, typ) -> + let ctyp = ctyp_of_typ ctx typ in + let aval_setup, cval, aval_cleanup = compile_aval l ctx aval in + let case_return_id = gensym () in + let finish_match_label = label "finish_match_" in + let compile_case (apat, guard, body) = + let trivial_guard = match guard with + | AE_aux (AE_val (AV_lit (L_aux (L_true, _), _)), _, _) + | AE_aux (AE_val (AV_C_fragment (F_lit (V_bool true), _, _)), _, _) -> true + | _ -> false + in + let case_label = label "case_" in + let destructure, destructure_cleanup, ctx = compile_match ctx apat cval case_label in + let guard_setup, guard_call, guard_cleanup = compile_aexp ctx guard in + let body_setup, body_call, body_cleanup = compile_aexp ctx body in + let gs = gensym () in + let case_instrs = + destructure @ [icomment "end destructuring"] + @ (if not trivial_guard then + guard_setup @ [idecl CT_bool gs; guard_call (CL_id (gs, CT_bool))] @ guard_cleanup + @ [iif (F_unary ("!", F_id gs), CT_bool) (destructure_cleanup @ [igoto case_label]) [] CT_unit] + @ [icomment "end guard"] + else []) + @ body_setup @ [body_call (CL_id (case_return_id, ctyp))] @ body_cleanup @ destructure_cleanup + @ [igoto finish_match_label] + in + if is_dead_aexp body then + [ilabel case_label] + else + [iblock case_instrs; ilabel case_label] + in + [icomment "begin match"] + @ aval_setup @ [idecl ctyp case_return_id] + @ List.concat (List.map compile_case cases) + @ [imatch_failure ()] + @ [ilabel finish_match_label], + (fun clexp -> icopy l clexp (F_id case_return_id, ctyp)), + [iclear ctyp case_return_id] + @ aval_cleanup + @ [icomment "end match"] + + (* Compile try statement *) + | AE_try (aexp, cases, typ) -> + let ctyp = ctyp_of_typ ctx typ in + let aexp_setup, aexp_call, aexp_cleanup = compile_aexp ctx aexp in + let try_return_id = gensym () in + let handled_exception_label = label "handled_exception_" in + let fallthrough_label = label "fallthrough_exception_" in + let compile_case (apat, guard, body) = + let trivial_guard = match guard with + | AE_aux (AE_val (AV_lit (L_aux (L_true, _), _)), _, _) + | AE_aux (AE_val (AV_C_fragment (F_lit (V_bool true), _, _)), _, _) -> true + | _ -> false + in + let try_label = label "try_" in + let exn_cval = (F_current_exception, ctyp_of_typ ctx (mk_typ (Typ_id (mk_id "exception")))) in + let destructure, destructure_cleanup, ctx = compile_match ctx apat exn_cval try_label in + let guard_setup, guard_call, guard_cleanup = compile_aexp ctx guard in + let body_setup, body_call, body_cleanup = compile_aexp ctx body in + let gs = gensym () in + let case_instrs = + destructure @ [icomment "end destructuring"] + @ (if not trivial_guard then + guard_setup @ [idecl CT_bool gs; guard_call (CL_id (gs, CT_bool))] @ guard_cleanup + @ [ijump (F_unary ("!", F_id gs), CT_bool) try_label] + @ [icomment "end guard"] + else []) + @ body_setup @ [body_call (CL_id (try_return_id, ctyp))] @ body_cleanup @ destructure_cleanup + @ [igoto handled_exception_label] + in + [iblock case_instrs; ilabel try_label] + in + assert (ctyp_equal ctyp (ctyp_of_typ ctx typ)); + [idecl ctyp try_return_id; + itry_block (aexp_setup @ [aexp_call (CL_id (try_return_id, ctyp))] @ aexp_cleanup); + ijump (F_unary ("!", F_have_exception), CT_bool) handled_exception_label] + @ List.concat (List.map compile_case cases) + @ [igoto fallthrough_label; + ilabel handled_exception_label; + icopy l CL_have_exception (F_lit (V_bool false), CT_bool); + ilabel fallthrough_label], + (fun clexp -> icopy l clexp (F_id try_return_id, ctyp)), + [] + + | AE_if (aval, then_aexp, else_aexp, if_typ) -> + if is_dead_aexp then_aexp then + compile_aexp ctx else_aexp + else if is_dead_aexp else_aexp then + compile_aexp ctx then_aexp + else + let if_ctyp = ctyp_of_typ ctx if_typ in + let compile_branch aexp = + let setup, call, cleanup = compile_aexp ctx aexp in + fun clexp -> setup @ [call clexp] @ cleanup + in + let setup, cval, cleanup = compile_aval l ctx aval in + setup, + (fun clexp -> iif cval + (compile_branch then_aexp clexp) + (compile_branch else_aexp clexp) + if_ctyp), + cleanup + + (* FIXME: AE_record_update could be AV_record_update - would reduce some copying. *) + | AE_record_update (aval, fields, typ) -> + let ctyp = ctyp_of_typ ctx typ in + let ctors = match ctyp with + | CT_struct (_, ctors) -> List.fold_left (fun m (k, v) -> Bindings.add k v m) Bindings.empty ctors + | _ -> raise (Reporting.err_general l "Cannot perform record update for non-record type") + in + let gs = gensym () in + let compile_fields (id, aval) = + let field_setup, cval, field_cleanup = compile_aval l ctx aval in + field_setup + @ [icopy l (CL_field (CL_id (gs, ctyp), string_of_id id)) cval] + @ field_cleanup + in + let setup, cval, cleanup = compile_aval l ctx aval in + [idecl ctyp gs] + @ setup + @ [icopy l (CL_id (gs, ctyp)) cval] + @ cleanup + @ List.concat (List.map compile_fields (Bindings.bindings fields)), + (fun clexp -> icopy l clexp (F_id gs, ctyp)), + [iclear ctyp gs] + + | AE_short_circuit (SC_and, aval, aexp) -> + let left_setup, cval, left_cleanup = compile_aval l ctx aval in + let right_setup, call, right_cleanup = compile_aexp ctx aexp in + let gs = gensym () in + left_setup + @ [ idecl CT_bool gs; + iif cval + (right_setup @ [call (CL_id (gs, CT_bool))] @ right_cleanup) + [icopy l (CL_id (gs, CT_bool)) (F_lit (V_bool false), CT_bool)] + CT_bool ] + @ left_cleanup, + (fun clexp -> icopy l clexp (F_id gs, CT_bool)), + [] + | AE_short_circuit (SC_or, aval, aexp) -> + let left_setup, cval, left_cleanup = compile_aval l ctx aval in + let right_setup, call, right_cleanup = compile_aexp ctx aexp in + let gs = gensym () in + left_setup + @ [ idecl CT_bool gs; + iif cval + [icopy l (CL_id (gs, CT_bool)) (F_lit (V_bool true), CT_bool)] + (right_setup @ [call (CL_id (gs, CT_bool))] @ right_cleanup) + CT_bool ] + @ left_cleanup, + (fun clexp -> icopy l clexp (F_id gs, CT_bool)), + [] + + (* This is a faster assignment rule for updating fields of a + struct. *) + | AE_assign (id, assign_typ, AE_aux (AE_record_update (AV_id (rid, _), fields, typ), _, _)) + when Id.compare id rid = 0 -> + let compile_fields (field_id, aval) = + let field_setup, cval, field_cleanup = compile_aval l ctx aval in + field_setup + @ [icopy l (CL_field (CL_id (id, ctyp_of_typ ctx typ), string_of_id field_id)) cval] + @ field_cleanup + in + List.concat (List.map compile_fields (Bindings.bindings fields)), + (fun clexp -> icopy l clexp unit_fragment), + [] + + | AE_assign (id, assign_typ, aexp) -> + let assign_ctyp = + match Bindings.find_opt id ctx.locals with + | Some (_, ctyp) -> ctyp + | None -> ctyp_of_typ ctx assign_typ + in + let setup, call, cleanup = compile_aexp ctx aexp in + setup @ [call (CL_id (id, assign_ctyp))], (fun clexp -> icopy l clexp unit_fragment), cleanup + + | AE_block (aexps, aexp, _) -> + let block = compile_block ctx aexps in + let setup, call, cleanup = compile_aexp ctx aexp in + block @ setup, call, cleanup + + | AE_loop (While, cond, body) -> + let loop_start_label = label "while_" in + let loop_end_label = label "wend_" in + let cond_setup, cond_call, cond_cleanup = compile_aexp ctx cond in + let body_setup, body_call, body_cleanup = compile_aexp ctx body in + let gs = gensym () in + let unit_gs = gensym () in + let loop_test = (F_unary ("!", F_id gs), CT_bool) in + [idecl CT_bool gs; idecl CT_unit unit_gs] + @ [ilabel loop_start_label] + @ [iblock (cond_setup + @ [cond_call (CL_id (gs, CT_bool))] + @ cond_cleanup + @ [ijump loop_test loop_end_label] + @ body_setup + @ [body_call (CL_id (unit_gs, CT_unit))] + @ body_cleanup + @ [igoto loop_start_label])] + @ [ilabel loop_end_label], + (fun clexp -> icopy l clexp unit_fragment), + [] + + | AE_loop (Until, cond, body) -> + let loop_start_label = label "repeat_" in + let loop_end_label = label "until_" in + let cond_setup, cond_call, cond_cleanup = compile_aexp ctx cond in + let body_setup, body_call, body_cleanup = compile_aexp ctx body in + let gs = gensym () in + let unit_gs = gensym () in + let loop_test = (F_id gs, CT_bool) in + [idecl CT_bool gs; idecl CT_unit unit_gs] + @ [ilabel loop_start_label] + @ [iblock (body_setup + @ [body_call (CL_id (unit_gs, CT_unit))] + @ body_cleanup + @ cond_setup + @ [cond_call (CL_id (gs, CT_bool))] + @ cond_cleanup + @ [ijump loop_test loop_end_label] + @ [igoto loop_start_label])] + @ [ilabel loop_end_label], + (fun clexp -> icopy l clexp unit_fragment), + [] + + | AE_cast (aexp, typ) -> compile_aexp ctx aexp + + | AE_return (aval, typ) -> + let fn_return_ctyp = match Env.get_ret_typ env with + | Some typ -> ctyp_of_typ ctx typ + | None -> raise (Reporting.err_general l "No function return type found when compiling return statement") + in + (* Cleanup info will be re-added by fix_early_(heap/stack)_return *) + let return_setup, cval, _ = compile_aval l ctx aval in + let creturn = + if ctyp_equal fn_return_ctyp (cval_ctyp cval) then + [ireturn cval] + else + let gs = gensym () in + [idecl fn_return_ctyp gs; + icopy l (CL_id (gs, fn_return_ctyp)) cval; + ireturn (F_id gs, fn_return_ctyp)] + in + return_setup @ creturn, + (fun clexp -> icomment "unreachable after return"), + [] + + | AE_throw (aval, typ) -> + (* Cleanup info will be handled by fix_exceptions *) + let throw_setup, cval, _ = compile_aval l ctx aval in + throw_setup @ [ithrow cval], + (fun clexp -> icomment "unreachable after throw"), + [] + + | AE_field (aval, id, _) -> + let setup, cval, cleanup = compile_aval l ctx aval in + let ctyp = match cval_ctyp cval with + | CT_struct (struct_id, fields) -> + begin match Util.assoc_compare_opt Id.compare id fields with + | Some ctyp -> ctyp + | None -> + raise (Reporting.err_unreachable l __POS__ + ("Struct " ^ string_of_id struct_id ^ " does not have expected field " ^ string_of_id id ^ "?")) + end + | _ -> + raise (Reporting.err_unreachable l __POS__ "Field access on non-struct type in ANF representation!") + in + setup, + (fun clexp -> icopy l clexp (F_field (fst cval, Util.zencode_string (string_of_id id)), ctyp)), + cleanup + + | AE_for (loop_var, loop_from, loop_to, loop_step, Ord_aux (ord, _), body) -> + (* We assume that all loop indices are safe to put in a CT_fint. *) + let ctx = { ctx with locals = Bindings.add loop_var (Immutable, CT_fint 64) ctx.locals } in + + let is_inc = match ord with + | Ord_inc -> true + | Ord_dec -> false + | Ord_var _ -> raise (Reporting.err_general l "Polymorphic loop direction in C backend") + in + + (* Loop variables *) + let from_setup, from_call, from_cleanup = compile_aexp ctx loop_from in + let from_gs = gensym () in + let to_setup, to_call, to_cleanup = compile_aexp ctx loop_to in + let to_gs = gensym () in + let step_setup, step_call, step_cleanup = compile_aexp ctx loop_step in + let step_gs = gensym () in + let variable_init gs setup call cleanup = + [idecl (CT_fint 64) gs; + iblock (setup @ [call (CL_id (gs, CT_fint 64))] @ cleanup)] + in + + let loop_start_label = label "for_start_" in + let loop_end_label = label "for_end_" in + let body_setup, body_call, body_cleanup = compile_aexp ctx body in + let body_gs = gensym () in + + variable_init from_gs from_setup from_call from_cleanup + @ variable_init to_gs to_setup to_call to_cleanup + @ variable_init step_gs step_setup step_call step_cleanup + @ [iblock ([idecl (CT_fint 64) loop_var; + icopy l (CL_id (loop_var, (CT_fint 64))) (F_id from_gs, (CT_fint 64)); + idecl CT_unit body_gs; + iblock ([ilabel loop_start_label] + @ [ijump (F_op (F_id loop_var, (if is_inc then ">" else "<"), F_id to_gs), CT_bool) loop_end_label] + @ body_setup + @ [body_call (CL_id (body_gs, CT_unit))] + @ body_cleanup + @ [icopy l (CL_id (loop_var, (CT_fint 64))) + (F_op (F_id loop_var, (if is_inc then "+" else "-"), F_id step_gs), (CT_fint 64))] + @ [igoto loop_start_label]); + ilabel loop_end_label])], + (fun clexp -> icopy l clexp unit_fragment), + [] + +and compile_block ctx = function + | [] -> [] + | exp :: exps -> + let setup, call, cleanup = compile_aexp ctx exp in + let rest = compile_block ctx exps in + let gs = gensym () in + iblock (setup @ [idecl CT_unit gs; call (CL_id (gs, CT_unit))] @ cleanup) :: rest + +(** Compile a sail type definition into a IR one. Most of the + actual work of translating the typedefs into C is done by the code + generator, as it's easy to keep track of structs, tuples and unions + in their sail form at this level, and leave the fiddly details of + how they get mapped to C in the next stage. This function also adds + details of the types it compiles to the context, ctx, which is why + it returns a ctypdef * ctx pair. **) +let compile_type_def ctx (TD_aux (type_def, (l, _))) = + match type_def with + | TD_enum (id, ids, _) -> + CTD_enum (id, ids), + { ctx with enums = Bindings.add id (IdSet.of_list ids) ctx.enums } + + | TD_record (id, typq, ctors, _) -> + let record_ctx = { ctx with local_env = add_typquant l typq ctx.local_env } in + let ctors = + List.fold_left (fun ctors (typ, id) -> Bindings.add id (ctyp_of_typ record_ctx typ) ctors) Bindings.empty ctors + in + CTD_struct (id, Bindings.bindings ctors), + { ctx with records = Bindings.add id ctors ctx.records } + + | TD_variant (id, typq, tus, _) -> + let compile_tu = function + | Tu_aux (Tu_ty_id (typ, id), _) -> + let ctx = { ctx with local_env = add_typquant (id_loc id) typq ctx.local_env } in + ctyp_of_typ ctx typ, id + in + let ctus = List.fold_left (fun ctus (ctyp, id) -> Bindings.add id ctyp ctus) Bindings.empty (List.map compile_tu tus) in + CTD_variant (id, Bindings.bindings ctus), + { ctx with variants = Bindings.add id ctus ctx.variants } + + (* Will be re-written before here, see bitfield.ml *) + | TD_bitfield _ -> + Reporting.unreachable l __POS__ "Cannot compile TD_bitfield" + + (* All type abbreviations are filtered out in compile_def *) + | TD_abbrev _ -> + Reporting.unreachable l __POS__ "Found TD_abbrev in compile_type_def" + +let generate_cleanup instrs = + let generate_cleanup' (I_aux (instr, _)) = + match instr with + | I_init (ctyp, id, cval) -> [(id, iclear ctyp id)] + | I_decl (ctyp, id) -> [(id, iclear ctyp id)] + | instr -> [] + in + let is_clear ids = function + | I_aux (I_clear (_, id), _) -> IdSet.add id ids + | _ -> ids + in + let cleaned = List.fold_left is_clear IdSet.empty instrs in + instrs + |> List.map generate_cleanup' + |> List.concat + |> List.filter (fun (id, _) -> not (IdSet.mem id cleaned)) + |> List.map snd + +let fix_exception_block ?return:(return=None) ctx instrs = + let end_block_label = label "end_block_exception_" in + let is_exception_stop (I_aux (instr, _)) = + match instr with + | I_throw _ | I_if _ | I_block _ | I_funcall _ -> true + | _ -> false + in + (* In this function 'after' is instructions after the one we've + matched on, 'before is instructions before the instruction we've + matched with, but after the previous match, and 'historic' are + all the befores from previous matches. *) + let rec rewrite_exception historic instrs = + match instr_split_at is_exception_stop instrs with + | instrs, [] -> instrs + | before, I_aux (I_block instrs, _) :: after -> + before + @ [iblock (rewrite_exception (historic @ before) instrs)] + @ rewrite_exception (historic @ before) after + | before, I_aux (I_if (cval, then_instrs, else_instrs, ctyp), _) :: after -> + let historic = historic @ before in + before + @ [iif cval (rewrite_exception historic then_instrs) (rewrite_exception historic else_instrs) ctyp] + @ rewrite_exception historic after + | before, I_aux (I_throw cval, (_, l)) :: after -> + before + @ [icopy l (CL_current_exception (cval_ctyp cval)) cval; + icopy l CL_have_exception (F_lit (V_bool true), CT_bool)] + @ generate_cleanup (historic @ before) + @ [igoto end_block_label] + @ rewrite_exception (historic @ before) after + | before, (I_aux (I_funcall (x, _, f, args), _) as funcall) :: after -> + let effects = match Env.get_val_spec f ctx.tc_env with + | _, Typ_aux (Typ_fn (_, _, effects), _) -> effects + | exception (Type_error _) -> no_effect (* nullary union constructor, so no val spec *) + | _ -> assert false (* valspec must have function type *) + in + if has_effect effects BE_escape then + before + @ [funcall; + iif (F_have_exception, CT_bool) (generate_cleanup (historic @ before) @ [igoto end_block_label]) [] CT_unit] + @ rewrite_exception (historic @ before) after + else + before @ funcall :: rewrite_exception (historic @ before) after + | _, _ -> assert false (* unreachable *) + in + match return with + | None -> + rewrite_exception [] instrs @ [ilabel end_block_label] + | Some ctyp -> + rewrite_exception [] instrs @ [ilabel end_block_label; iundefined ctyp] + +let rec map_try_block f (I_aux (instr, aux)) = + let instr = match instr with + | I_decl _ | I_reset _ | I_init _ | I_reinit _ -> instr + | I_if (cval, instrs1, instrs2, ctyp) -> + I_if (cval, List.map (map_try_block f) instrs1, List.map (map_try_block f) instrs2, ctyp) + | I_funcall _ | I_copy _ | I_alias _ | I_clear _ | I_throw _ | I_return _ -> instr + | I_block instrs -> I_block (List.map (map_try_block f) instrs) + | I_try_block instrs -> I_try_block (f (List.map (map_try_block f) instrs)) + | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_jump _ | I_match_failure | I_undefined _ | I_end -> instr + in + I_aux (instr, aux) + +let fix_exception ?return:(return=None) ctx instrs = + let instrs = List.map (map_try_block (fix_exception_block ctx)) instrs in + fix_exception_block ~return:return ctx instrs + +let rec compile_arg_pat ctx label (P_aux (p_aux, (l, _)) as pat) ctyp = + match p_aux with + | P_id id -> (id, ([], [])) + | P_wild -> let gs = gensym () in (gs, ([], [])) + | P_tup [] | P_lit (L_aux (L_unit, _)) -> let gs = gensym () in (gs, ([], [])) + | P_var (pat, _) -> compile_arg_pat ctx label pat ctyp + | P_typ (_, pat) -> compile_arg_pat ctx label pat ctyp + | _ -> + let apat = anf_pat pat in + let gs = gensym () in + let destructure, cleanup, _ = compile_match ctx apat (F_id gs, ctyp) label in + (gs, (destructure, cleanup)) + +let rec compile_arg_pats ctx label (P_aux (p_aux, (l, _)) as pat) ctyps = + match p_aux with + | P_typ (_, pat) -> compile_arg_pats ctx label pat ctyps + | P_tup pats when List.length pats = List.length ctyps -> + [], List.map2 (fun pat ctyp -> compile_arg_pat ctx label pat ctyp) pats ctyps, [] + | _ when List.length ctyps = 1 -> + [], [compile_arg_pat ctx label pat (List.nth ctyps 0)], [] + + | _ -> + let arg_id, (destructure, cleanup) = compile_arg_pat ctx label pat (CT_tup ctyps) in + let new_ids = List.map (fun ctyp -> gensym (), ctyp) ctyps in + destructure + @ [idecl (CT_tup ctyps) arg_id] + @ List.mapi (fun i (id, ctyp) -> icopy l (CL_tuple (CL_id (arg_id, CT_tup ctyps), i)) (F_id id, ctyp)) new_ids, + List.map (fun (id, _) -> id, ([], [])) new_ids, + [iclear (CT_tup ctyps) arg_id] + @ cleanup + +let combine_destructure_cleanup xs = List.concat (List.map fst xs), List.concat (List.rev (List.map snd xs)) + +let fix_destructure fail_label = function + | ([], cleanup) -> ([], cleanup) + | destructure, cleanup -> + let body_label = label "fundef_body_" in + (destructure @ [igoto body_label; ilabel fail_label; imatch_failure (); ilabel body_label], cleanup) + +(** Functions that have heap-allocated return types are implemented by + passing a pointer a location where the return value should be + stored. The ANF -> Sail IR pass for expressions simply outputs an + I_return instruction for any return value, so this function walks + over the IR ast for expressions and modifies the return statements + into code that sets that pointer, as well as adds extra control + flow to cleanup heap-allocated variables correctly when a function + terminates early. See the generate_cleanup function for how this is + done. *) +let fix_early_return ret instrs = + let end_function_label = label "end_function_" in + let is_return_recur (I_aux (instr, _)) = + match instr with + | I_return _ | I_undefined _ | I_if _ | I_block _ -> true + | _ -> false + in + let rec rewrite_return historic instrs = + match instr_split_at is_return_recur instrs with + | instrs, [] -> instrs + | before, I_aux (I_block instrs, _) :: after -> + before + @ [iblock (rewrite_return (historic @ before) instrs)] + @ rewrite_return (historic @ before) after + | before, I_aux (I_if (cval, then_instrs, else_instrs, ctyp), _) :: after -> + let historic = historic @ before in + before + @ [iif cval (rewrite_return historic then_instrs) (rewrite_return historic else_instrs) ctyp] + @ rewrite_return historic after + | before, I_aux (I_return cval, (_, l)) :: after -> + let cleanup_label = label "cleanup_" in + let end_cleanup_label = label "end_cleanup_" in + before + @ [icopy l ret cval; + igoto cleanup_label] + (* This is probably dead code until cleanup_label, but we cannot be sure there are no jumps into it. *) + @ rewrite_return (historic @ before) after + @ [igoto end_cleanup_label; + ilabel cleanup_label] + @ generate_cleanup (historic @ before) + @ [igoto end_function_label; + ilabel end_cleanup_label] + | before, I_aux (I_undefined _, (_, l)) :: after -> + let cleanup_label = label "cleanup_" in + let end_cleanup_label = label "end_cleanup_" in + before + @ [igoto cleanup_label] + @ rewrite_return (historic @ before) after + @ [igoto end_cleanup_label; + ilabel cleanup_label] + @ generate_cleanup (historic @ before) + @ [igoto end_function_label; + ilabel end_cleanup_label] + | _, _ -> assert false + in + rewrite_return [] instrs + @ [ilabel end_function_label; iend ()] + +let letdef_count = ref 0 + +(** Compile a Sail toplevel definition into an IR definition **) +let rec compile_def n total ctx def = + match def with + | DEF_fundef (FD_aux (FD_function (_, _, _, [FCL_aux (FCL_Funcl (id, _), _)]), _)) + when !opt_memo_cache -> + let digest = + def |> Pretty_print_sail.doc_def |> Pretty_print_sail.to_string |> Digest.string + in + let cachefile = Filename.concat "_sbuild" ("ccache" ^ Digest.to_hex digest) in + let cached = + if Sys.file_exists cachefile then + let in_chan = open_in cachefile in + try + let compiled = Marshal.from_channel in_chan in + close_in in_chan; + Some (compiled, ctx) + with + | _ -> close_in in_chan; None + else + None + in + begin match cached with + | Some (compiled, ctx) -> + Util.progress "Compiling " (string_of_id id) n total; + compiled, ctx + | None -> + let compiled, ctx = compile_def' n total ctx def in + let out_chan = open_out cachefile in + Marshal.to_channel out_chan compiled [Marshal.Closures]; + close_out out_chan; + compiled, ctx + end + + | _ -> compile_def' n total ctx def + +and compile_def' n total ctx = function + | DEF_reg_dec (DEC_aux (DEC_reg (_, _, typ, id), _)) -> + [CDEF_reg_dec (id, ctyp_of_typ ctx typ, [])], ctx + | DEF_reg_dec (DEC_aux (DEC_config (id, typ, exp), _)) -> + let aexp = ctx.optimize_anf ctx (no_shadow IdSet.empty (anf exp)) in + let setup, call, cleanup = compile_aexp ctx aexp in + let instrs = setup @ [call (CL_id (id, ctyp_of_typ ctx typ))] @ cleanup in + [CDEF_reg_dec (id, ctyp_of_typ ctx typ, instrs)], ctx + + | DEF_reg_dec (DEC_aux (_, (l, _))) -> + raise (Reporting.err_general l "Cannot compile alias register declaration") + + | DEF_spec (VS_aux (VS_val_spec (_, id, _, _), _)) -> + let quant, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_env in + let arg_typs, ret_typ = match fn_typ with + | Typ_fn (arg_typs, ret_typ, _) -> arg_typs, ret_typ + | _ -> assert false + in + let ctx' = { ctx with local_env = add_typquant (id_loc id) quant ctx.local_env } in + let arg_ctyps, ret_ctyp = List.map (ctyp_of_typ ctx') arg_typs, ctyp_of_typ ctx' ret_typ in + [CDEF_spec (id, arg_ctyps, ret_ctyp)], ctx + + | DEF_fundef (FD_aux (FD_function (_, _, _, [FCL_aux (FCL_Funcl (id, Pat_aux (Pat_exp (pat, exp), _)), _)]), _)) -> + Util.progress "Compiling " (string_of_id id) n total; + + (* Find the function's type. *) + let quant, Typ_aux (fn_typ, _) = + try Env.get_val_spec id ctx.local_env with Type_error _ -> Env.get_val_spec id ctx.tc_env + in + let arg_typs, ret_typ = match fn_typ with + | Typ_fn (arg_typs, ret_typ, _) -> arg_typs, ret_typ + | _ -> assert false + in + + (* Handle the argument pattern. *) + let fundef_label = label "fundef_fail_" in + let orig_ctx = ctx in + (* The context must be updated before we call ctyp_of_typ on the argument types. *) + let ctx = { ctx with local_env = add_typquant (id_loc id) quant ctx.tc_env } in + + let arg_ctyps = List.map (ctyp_of_typ ctx) arg_typs in + let ret_ctyp = ctyp_of_typ ctx ret_typ in + + (* Compile the function arguments as patterns. *) + let arg_setup, compiled_args, arg_cleanup = compile_arg_pats ctx fundef_label pat arg_ctyps in + let ctx = + (* We need the primop analyzer to be aware of the function argument types, so put them in ctx *) + List.fold_left2 (fun ctx (id, _) ctyp -> { ctx with locals = Bindings.add id (Immutable, ctyp) ctx.locals }) ctx compiled_args arg_ctyps + in + + (* Optimize and compile the expression to ANF. *) + let aexp = no_shadow (pat_ids pat) (anf exp) in + let aexp = ctx.optimize_anf ctx aexp in + + let setup, call, cleanup = compile_aexp ctx aexp in + let destructure, destructure_cleanup = + compiled_args |> List.map snd |> combine_destructure_cleanup |> fix_destructure fundef_label + in + + let instrs = arg_setup @ destructure @ setup @ [call (CL_return ret_ctyp)] @ cleanup @ destructure_cleanup @ arg_cleanup in + let instrs = fix_early_return (CL_return ret_ctyp) instrs in + let instrs = fix_exception ~return:(Some ret_ctyp) ctx instrs in + + if Id.compare (mk_id !opt_debug_function) id = 0 then + let header = + Printf.sprintf "Sail IR for %s %s(%s) : (%s) -> %s" Util.("function" |> red |> clear) (string_of_id id) + (Util.string_of_list ", " string_of_id (List.map fst compiled_args)) + (Util.string_of_list ", " (fun ctyp -> Util.(string_of_ctyp ctyp |> yellow |> clear)) arg_ctyps) + Util.(string_of_ctyp ret_ctyp |> yellow |> clear) + in + prerr_endline (Util.header header (List.length arg_ctyps + 2)); + prerr_endline (Pretty_print_sail.to_string PPrint.(separate_map hardline pp_instr instrs)) + else (); + + if !opt_debug_flow_graphs then + begin + let instrs = Jib_optimize.(instrs |> optimize_unit |> flatten_instrs) in + let cfg = Jib_ssa.ssa instrs in + let out_chan = open_out (Util.zencode_string (string_of_id id) ^ ".gv") in + Jib_ssa.make_dot out_chan cfg; + close_out out_chan; + end; + + [CDEF_fundef (id, None, List.map fst compiled_args, instrs)], orig_ctx + + | DEF_fundef (FD_aux (FD_function (_, _, _, []), (l, _))) -> + raise (Reporting.err_general l "Encountered function with no clauses") + + | DEF_fundef (FD_aux (FD_function (_, _, _, funcls), (l, _))) -> + raise (Reporting.err_general l "Encountered function with multiple clauses") + + (* All abbreviations should expanded by the typechecker, so we don't + need to translate type abbreviations into C typedefs. *) + | DEF_type (TD_aux (TD_abbrev _, _)) -> [], ctx + + | DEF_type type_def -> + let tdef, ctx = compile_type_def ctx type_def in + [CDEF_type tdef], ctx + + | DEF_val (LB_aux (LB_val (pat, exp), _)) -> + let ctyp = ctyp_of_typ ctx (typ_of_pat pat) in + let aexp = ctx.optimize_anf ctx (no_shadow IdSet.empty (anf exp)) in + let setup, call, cleanup = compile_aexp ctx aexp in + let apat = anf_pat ~global:true pat in + let gs = gensym () in + let end_label = label "let_end_" in + let destructure, destructure_cleanup, _ = compile_match ctx apat (F_id gs, ctyp) end_label in + let gs_setup, gs_cleanup = + [idecl ctyp gs], [iclear ctyp gs] + in + let bindings = List.map (fun (id, typ) -> id, ctyp_of_typ ctx typ) (apat_globals apat) in + let n = !letdef_count in + incr letdef_count; + let instrs = + gs_setup @ setup + @ [call (CL_id (gs, ctyp))] + @ cleanup + @ destructure + @ destructure_cleanup @ gs_cleanup + @ [ilabel end_label] + in + [CDEF_let (n, bindings, instrs)], + { ctx with letbinds = n :: ctx.letbinds } + + (* Only DEF_default that matters is default Order, but all order + polymorphism is specialised by this point. *) + | DEF_default _ -> [], ctx + + (* Overloading resolved by type checker *) + | DEF_overload _ -> [], ctx + + (* Only the parser and sail pretty printer care about this. *) + | DEF_fixity _ -> [], ctx + + (* We just ignore any pragmas we don't want to deal with. *) + | DEF_pragma _ -> [], ctx + + (* Termination measures only needed for Coq, and other theorem prover output *) + | DEF_measure _ -> [], ctx + + | DEF_internal_mutrec fundefs -> + let defs = List.map (fun fdef -> DEF_fundef fdef) fundefs in + List.fold_left (fun (cdefs, ctx) def -> let cdefs', ctx = compile_def n total ctx def in (cdefs @ cdefs', ctx)) ([], ctx) defs + + (* Scattereds and mapdefs should be removed by this point *) + | (DEF_scattered _ | DEF_mapdef _) as def -> + raise (Reporting.err_general Parse_ast.Unknown ("Could not compile:\n" ^ Pretty_print_sail.to_string (Pretty_print_sail.doc_def def))) + +let rec specialize_variants ctx prior = + let unifications = ref (Bindings.empty) in + + let fix_variant_ctyp var_id new_ctors = function + | CT_variant (id, ctors) when Id.compare id var_id = 0 -> CT_variant (id, new_ctors) + | ctyp -> ctyp + in + + let specialize_constructor ctx ctor_id ctyp = + function + | I_aux (I_funcall (clexp, extern, id, [cval]), ((_, l) as aux)) as instr when Id.compare id ctor_id = 0 -> + (* Work out how each call to a constructor in instantiated and add that to unifications *) + let unification = List.map ctyp_suprema (ctyp_unify ctyp (cval_ctyp cval)) in + let mono_id = append_id ctor_id ("_" ^ Util.string_of_list "_" (fun ctyp -> Util.zencode_string (string_of_ctyp ctyp)) unification) in + unifications := Bindings.add mono_id (ctyp_suprema (cval_ctyp cval)) !unifications; + + (* We need to cast each cval to it's ctyp_suprema in order to put it in the most general constructor *) + let casts = + let cast_to_suprema (frag, ctyp) = + let suprema = ctyp_suprema ctyp in + if ctyp_equal ctyp suprema then + [], (unpoly frag, ctyp), [] + else + let gs = gensym () in + [idecl suprema gs; + icopy l (CL_id (gs, suprema)) (unpoly frag, ctyp)], + (F_id gs, suprema), + [iclear suprema gs] + in + List.map cast_to_suprema [cval] + in + let setup = List.concat (List.map (fun (setup, _, _) -> setup) casts) in + let cvals = List.map (fun (_, cval, _) -> cval) casts in + let cleanup = List.concat (List.map (fun (_, _, cleanup) -> cleanup) casts) in + + let mk_funcall instr = + if List.length setup = 0 then + instr + else + iblock (setup @ [instr] @ cleanup) + in + + mk_funcall (I_aux (I_funcall (clexp, extern, mono_id, cvals), aux)) + + | I_aux (I_funcall (clexp, extern, id, cvals), ((_, l) as aux)) as instr when Id.compare id ctor_id = 0 -> + Reporting.unreachable l __POS__ "Multiple argument constructor found" + + | instr -> instr + in + + function + | (CDEF_type (CTD_variant (var_id, ctors)) as cdef) :: cdefs -> + let polymorphic_ctors = List.filter (fun (_, ctyp) -> is_polymorphic ctyp) ctors in + + let cdefs = + List.fold_left (fun cdefs (ctor_id, ctyp) -> List.map (cdef_map_instr (specialize_constructor ctx ctor_id ctyp)) cdefs) + cdefs + polymorphic_ctors + in + + let monomorphic_ctors = List.filter (fun (_, ctyp) -> not (is_polymorphic ctyp)) ctors in + let specialized_ctors = Bindings.bindings !unifications in + let new_ctors = monomorphic_ctors @ specialized_ctors in + + let ctx = { + ctx with variants = Bindings.add var_id + (List.fold_left (fun m (id, ctyp) -> Bindings.add id ctyp m) !unifications monomorphic_ctors) + ctx.variants + } in + + let cdefs = List.map (cdef_map_ctyp (map_ctyp (fix_variant_ctyp var_id new_ctors))) cdefs in + let prior = List.map (cdef_map_ctyp (map_ctyp (fix_variant_ctyp var_id new_ctors))) prior in + specialize_variants ctx (CDEF_type (CTD_variant (var_id, new_ctors)) :: prior) cdefs + + | cdef :: cdefs -> + let remove_poly (I_aux (instr, aux)) = + match instr with + | I_copy (clexp, (frag, ctyp)) when is_polymorphic ctyp -> + I_aux (I_copy (clexp, (frag, ctyp_suprema (clexp_ctyp clexp))), aux) + | instr -> I_aux (instr, aux) + in + let cdef = cdef_map_instr remove_poly cdef in + specialize_variants ctx (cdef :: prior) cdefs + + | [] -> List.rev prior, ctx + +(** Once we specialize variants, there may be additional type + dependencies which could be in the wrong order. As such we need to + sort the type definitions in the list of cdefs. *) +let sort_ctype_defs cdefs = + (* Split the cdefs into type definitions and non type definitions *) + let is_ctype_def = function CDEF_type _ -> true | _ -> false in + let unwrap = function CDEF_type ctdef -> ctdef | _ -> assert false in + let ctype_defs = List.map unwrap (List.filter is_ctype_def cdefs) in + let cdefs = List.filter (fun cdef -> not (is_ctype_def cdef)) cdefs in + + let ctdef_id = function + | CTD_enum (id, _) | CTD_struct (id, _) | CTD_variant (id, _) -> id + in + + let ctdef_ids = function + | CTD_enum _ -> IdSet.empty + | CTD_struct (_, ctors) | CTD_variant (_, ctors) -> + List.fold_left (fun ids (_, ctyp) -> IdSet.union (ctyp_ids ctyp) ids) IdSet.empty ctors + in + + (* Create a reverse (i.e. from types to the types that are dependent + upon them) id graph of dependencies between types *) + let module IdGraph = Graph.Make(Id) in + + let graph = + List.fold_left (fun g ctdef -> + List.fold_left (fun g id -> IdGraph.add_edge id (ctdef_id ctdef) g) + (IdGraph.add_edges (ctdef_id ctdef) [] g) (* Make sure even types with no dependencies are in graph *) + (IdSet.elements (ctdef_ids ctdef))) + IdGraph.empty + ctype_defs + in + + (* Then select the ctypes in the correct order as given by the topsort *) + let ids = IdGraph.topsort graph in + let ctype_defs = + List.map (fun id -> CDEF_type (List.find (fun ctdef -> Id.compare (ctdef_id ctdef) id = 0) ctype_defs)) ids + in + + ctype_defs @ cdefs + +let compile_ast ctx (Defs defs) = + let assert_vs = Initial_check.extern_of_string (mk_id "sail_assert") "(bool, string) -> unit effect {escape}" in + let exit_vs = Initial_check.extern_of_string (mk_id "sail_exit") "unit -> unit effect {escape}" in + + let ctx = { ctx with tc_env = snd (Type_error.check ctx.tc_env (Defs [assert_vs; exit_vs])) } in + + if !opt_memo_cache then + (try + if Sys.is_directory "_sbuild" then + () + else + raise (Reporting.err_general Parse_ast.Unknown "_sbuild exists, but is a file not a directory!") + with + | Sys_error _ -> Unix.mkdir "_sbuild" 0o775) + else (); + + let total = List.length defs in + let _, chunks, ctx = + List.fold_left (fun (n, chunks, ctx) def -> let defs, ctx = compile_def n total ctx def in n + 1, defs :: chunks, ctx) (1, [], ctx) defs + in + let cdefs = List.concat (List.rev chunks) in + let cdefs, ctx = specialize_variants ctx [] cdefs in + let cdefs = sort_ctype_defs cdefs in + cdefs, ctx diff --git a/src/jib/jib_compile.mli b/src/jib/jib_compile.mli new file mode 100644 index 00000000..f3bd8c76 --- /dev/null +++ b/src/jib/jib_compile.mli @@ -0,0 +1,100 @@ +(**************************************************************************) +(* 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. *) +(**************************************************************************) + +(** Compile Sail ASTs to Jib intermediate representation *) + +open Anf +open Ast +open Ast_util +open Jib +open Type_check + +(** Output a dataflow graph for each generated function in Graphviz + (dot) format. *) +val opt_debug_flow_graphs : bool ref + +(** Print the IR representation of a specific function. *) +val opt_debug_function : string ref + +(** {2 Jib context} *) + +(** Context for compiling Sail to Jib. We need to pass a (global) + typechecking environment given by checking the full AST. We have to + provide a conversion function from Sail types into Jib types, as + well as a function that optimizes ANF expressions (which can just + be the identity function) *) +type ctx = + { records : (ctyp Bindings.t) Bindings.t; + enums : IdSet.t Bindings.t; + variants : (ctyp Bindings.t) Bindings.t; + tc_env : Env.t; + local_env : Env.t; + locals : (mut * ctyp) Bindings.t; + letbinds : int list; + no_raw : bool; + convert_typ : ctx -> typ -> ctyp; + optimize_anf : ctx -> typ aexp -> typ aexp + } + +val initial_ctx : + convert_typ:(ctx -> typ -> ctyp) -> + optimize_anf:(ctx -> typ aexp -> typ aexp) -> + Env.t -> + ctx + +(** {2 Compilation functions} *) + +(** Compile a Sail definition into a Jib definition. The first two + arguments are is the current definition number and the total number + of definitions, and can be used to drive a progress bar (see + Util.progress). *) +val compile_def : int -> int -> ctx -> tannot def -> cdef list * ctx + +val compile_ast : ctx -> tannot defs -> cdef list * ctx diff --git a/src/jib/jib_optimize.ml b/src/jib/jib_optimize.ml new file mode 100644 index 00000000..889e650e --- /dev/null +++ b/src/jib/jib_optimize.ml @@ -0,0 +1,129 @@ +(**************************************************************************) +(* 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_util +open Jib +open Jib_util + +let optimize_unit instrs = + let unit_cval cval = + match cval_ctyp cval with + | CT_unit -> (F_lit V_unit, CT_unit) + | _ -> cval + in + let unit_instr = function + | I_aux (I_funcall (clexp, extern, id, args), annot) as instr -> + begin match clexp_ctyp clexp with + | CT_unit -> + I_aux (I_funcall (CL_void, extern, id, List.map unit_cval args), annot) + | _ -> instr + end + | I_aux (I_copy (clexp, cval), annot) as instr -> + begin match clexp_ctyp clexp with + | CT_unit -> + I_aux (I_copy (CL_void, unit_cval cval), annot) + | _ -> instr + end + | I_aux (I_alias (clexp, cval), annot) as instr -> + begin match clexp_ctyp clexp with + | CT_unit -> + I_aux (I_alias (CL_void, unit_cval cval), annot) + | _ -> instr + end + | instr -> instr + in + let non_pointless_copy (I_aux (aux, annot)) = + match aux with + | I_copy (CL_void, _) -> false + | _ -> true + in + filter_instrs non_pointless_copy (map_instr_list unit_instr instrs) + +let flat_counter = ref 0 +let flat_id () = + let id = mk_id ("local#" ^ string_of_int !flat_counter) in + incr flat_counter; + id + +let rec flatten_instrs = function + | I_aux (I_decl (ctyp, decl_id), aux) :: instrs -> + let fid = flat_id () in + I_aux (I_decl (ctyp, fid), aux) :: flatten_instrs (instrs_rename decl_id fid instrs) + + | I_aux ((I_block block | I_try_block block), _) :: instrs -> + flatten_instrs block @ flatten_instrs instrs + + | I_aux (I_if (cval, then_instrs, else_instrs, _), _) :: instrs -> + let then_label = label "then_" in + let endif_label = label "endif_" in + [ijump cval then_label] + @ flatten_instrs else_instrs + @ [igoto endif_label] + @ [ilabel then_label] + @ flatten_instrs then_instrs + @ [ilabel endif_label] + @ flatten_instrs instrs + + | I_aux (I_comment _, _) :: instrs -> flatten_instrs instrs + + | instr :: instrs -> instr :: flatten_instrs instrs + | [] -> [] + +let flatten_cdef = + function + | CDEF_fundef (function_id, heap_return, args, body) -> + flat_counter := 0; + CDEF_fundef (function_id, heap_return, args, flatten_instrs body) + + | CDEF_let (n, bindings, instrs) -> + flat_counter := 0; + CDEF_let (n, bindings, flatten_instrs instrs) + + | cdef -> cdef diff --git a/src/jib/jib_optimize.mli b/src/jib/jib_optimize.mli new file mode 100644 index 00000000..beffa81e --- /dev/null +++ b/src/jib/jib_optimize.mli @@ -0,0 +1,63 @@ +(**************************************************************************) +(* 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 Jib + +(** Remove redundant assignments and variables of type + unit. unit-typed identifiers that are assigned to are replaced with + CL_void, and cvals (which should be pure!) are replaced with unit + types are replaced by unit-literals. *) +val optimize_unit : instr list -> instr list + +(** Remove all instructions that can contain other nested + instructions, prodcing a flat list of instructions. *) +val flatten_instrs : instr list -> instr list +val flatten_cdef : cdef -> cdef + diff --git a/src/jib/jib_ssa.ml b/src/jib/jib_ssa.ml new file mode 100644 index 00000000..1f477696 --- /dev/null +++ b/src/jib/jib_ssa.ml @@ -0,0 +1,602 @@ +(**************************************************************************) +(* 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_util +open Jib +open Jib_util + +module IntSet = Set.Make(struct type t = int let compare = compare end) + +(**************************************************************************) +(* 1. Mutable graph type *) +(**************************************************************************) + +type 'a array_graph = { + mutable next : int; + mutable nodes : ('a * IntSet.t * IntSet.t) option array + } + +let make ~initial_size () = { + next = 0; + nodes = Array.make initial_size None + } + +(** Add a vertex to a graph, returning the node index *) +let add_vertex data graph = + let n = graph.next in + if n >= Array.length graph.nodes then + begin + let new_nodes = Array.make (Array.length graph.nodes * 2) None in + Array.blit graph.nodes 0 new_nodes 0 (Array.length graph.nodes); + graph.nodes <- new_nodes + end; + let n = graph.next in + graph.nodes.(n) <- Some (data, IntSet.empty, IntSet.empty); + graph.next <- n + 1; + n + +(** Add an edge between two existing vertices. Raises Invalid_argument + if either of the vertices do not exist. *) +let add_edge n m graph = + begin match graph.nodes.(n) with + | Some (data, parents, children) -> + graph.nodes.(n) <- Some (data, parents, IntSet.add m children) + | None -> + raise (Invalid_argument "Parent node does not exist in graph") + end; + match graph.nodes.(m) with + | Some (data, parents, children) -> + graph.nodes.(m) <- Some (data, IntSet.add n parents, children) + | None -> + raise (Invalid_argument "Child node does not exist in graph") + +let cardinal graph = graph.next + +let reachable roots graph = + let visited = ref IntSet.empty in + + let rec reachable' n = + if IntSet.mem n !visited then () + else + begin + visited := IntSet.add n !visited; + match graph.nodes.(n) with + | Some (_, _, successors) -> + IntSet.iter reachable' successors + | None -> () + end + in + IntSet.iter reachable' roots; !visited + +let prune visited graph = + for i = 0 to graph.next - 1 do + match graph.nodes.(i) with + | Some (n, preds, succs) -> + if IntSet.mem i visited then + graph.nodes.(i) <- Some (n, IntSet.inter visited preds, IntSet.inter visited succs) + else + graph.nodes.(i) <- None + | None -> () + done + +(**************************************************************************) +(* 2. Mutable control flow graph *) +(**************************************************************************) + +type cf_node = + | CF_label of string + | CF_block of instr list + | CF_start + +let control_flow_graph instrs = + let module StringMap = Map.Make(String) in + let labels = ref StringMap.empty in + + let graph = make ~initial_size:512 () in + + iter_instr (fun (I_aux (instr, annot)) -> + match instr with + | I_label label -> + labels := StringMap.add label (add_vertex ([], CF_label label) graph) !labels + | _ -> () + ) (iblock instrs); + + let cf_split (I_aux (aux, _)) = + match aux with + | I_block _ | I_label _ | I_goto _ | I_jump _ | I_if _ | I_end | I_match_failure | I_undefined _ -> true + | _ -> false + in + + let rec cfg preds instrs = + let before, after = instr_split_at cf_split instrs in + let last = match after with + | I_aux (I_label _, _) :: _ -> [] + | instr :: _ -> [instr] + | _ -> [] + in + let preds = match before @ last with + | [] -> preds + | instrs -> + let n = add_vertex ([], CF_block instrs) graph in + List.iter (fun p -> add_edge p n graph) preds; + [n] + in + match after with + | I_aux (I_if (cond, then_instrs, else_instrs, _), _) :: after -> + let t = cfg preds then_instrs in + let e = cfg preds else_instrs in + cfg (t @ e) after + + | I_aux ((I_end | I_match_failure | I_undefined _), _) :: after -> + cfg [] after + + | I_aux (I_goto label, _) :: after -> + List.iter (fun p -> add_edge p (StringMap.find label !labels) graph) preds; + cfg [] after + + | I_aux (I_jump (cval, label), _) :: after -> + List.iter (fun p -> add_edge p (StringMap.find label !labels) graph) preds; + cfg preds after + + | I_aux (I_label label, _) :: after -> + cfg (StringMap.find label !labels :: preds) after + + | I_aux (I_block instrs, _) :: after -> + let m = cfg preds instrs in + cfg m after + + | _ :: after -> assert false + + | [] -> preds + in + + let start = add_vertex ([], CF_start) graph in + let finish = cfg [start] instrs in + + let visited = reachable (IntSet.singleton start) graph in + prune visited graph; + + start, finish, graph + +(**************************************************************************) +(* 3. Computing dominators *) +(**************************************************************************) + +(** Calculate the (immediate) dominators of a graph using the + Lengauer-Tarjan algorithm. This is the slightly less sophisticated + version from Appel's book 'Modern compiler implementation in ML' + which runs in O(n log(n)) time. *) +let immediate_dominators graph root = + let none = -1 in + let vertex = Array.make (cardinal graph) 0 in + let parent = Array.make (cardinal graph) none in + let ancestor = Array.make (cardinal graph) none in + let semi = Array.make (cardinal graph) none in + let idom = Array.make (cardinal graph) none in + let samedom = Array.make (cardinal graph) none in + let best = Array.make (cardinal graph) none in + let dfnum = Array.make (cardinal graph) 0 in + let bucket = Array.make (cardinal graph) IntSet.empty in + + let rec ancestor_with_lowest_semi v = + let a = ancestor.(v) in + if ancestor.(a) <> none then + let b = ancestor_with_lowest_semi a in + ancestor.(v) <- ancestor.(a); + if dfnum.(semi.(b)) < dfnum.(semi.(best.(v))) then + best.(v) <- b + else (); + else (); + if best.(v) <> none then best.(v) else v + in + + let link p n = + ancestor.(n) <- p; + best.(n) <- n + in + + let count = ref 0 in + + let rec dfs p n = + if dfnum.(n) = 0 then + begin + dfnum.(n) <- !count; + vertex.(!count) <- n; + parent.(n) <- p; + incr count; + match graph.nodes.(n) with + | Some (_, _, successors) -> + IntSet.iter (fun w -> dfs n w) successors + | None -> assert false + end + in + dfs none root; + + for i = !count - 1 downto 1 do + let n = vertex.(i) in + let p = parent.(n) in + let s = ref p in + + begin match graph.nodes.(n) with + | Some (_, predecessors, _) -> + IntSet.iter (fun v -> + let s' = + if dfnum.(v) <= dfnum.(n) then + v + else + semi.(ancestor_with_lowest_semi v) + in + if dfnum.(s') < dfnum.(!s) then s := s' + ) predecessors + | None -> assert false + end; + semi.(n) <- !s; + bucket.(!s) <- IntSet.add n bucket.(!s); + link p n; + IntSet.iter (fun v -> + let y = ancestor_with_lowest_semi v in + if semi.(y) = semi.(v) then + idom.(v) <- p + else + samedom.(n) <- y + ) bucket.(p); + done; + for i = 1 to !count - 1 do + let n = vertex.(i) in + if samedom.(n) <> none then + idom.(n) <- idom.(samedom.(n)) + done; + idom + +(** [(dominator_children idoms).(n)] are the nodes whose immediate dominator + (idom) is n. *) +let dominator_children idom = + let none = -1 in + let children = Array.make (Array.length idom) IntSet.empty in + + for n = 0 to Array.length idom - 1 do + let p = idom.(n) in + if p <> none then + children.(p) <- IntSet.add n (children.(p)) + done; + children + +(** [dominate idom n w] is true if n dominates w in the tree of + immediate dominators idom. *) +let rec dominate idom n w = + let none = -1 in + let p = idom.(n) in + if p = none then + false + else if p = w then + true + else + dominate idom p w + +let dominance_frontiers graph root idom children = + let df = Array.make (cardinal graph) IntSet.empty in + + let rec compute_df n = + let set = ref IntSet.empty in + + begin match graph.nodes.(n) with + | Some (content, _, succs) -> + IntSet.iter (fun y -> + if idom.(y) <> n then + set := IntSet.add y !set + ) succs + | None -> () + end; + IntSet.iter (fun c -> + compute_df c; + IntSet.iter (fun w -> + if not (dominate idom n w) then + set := IntSet.add w !set + ) (df.(c)) + ) (children.(n)); + df.(n) <- !set + in + compute_df root; + df + +(**************************************************************************) +(* 4. Conversion to SSA form *) +(**************************************************************************) + +type ssa_elem = + | Phi of Ast.id * Ast.id list + +let place_phi_functions graph df = + let defsites = ref Bindings.empty in + + let all_vars = ref IdSet.empty in + + let rec all_decls = function + | I_aux (I_decl (_, id), _) :: instrs -> + IdSet.add id (all_decls instrs) + | _ :: instrs -> all_decls instrs + | [] -> IdSet.empty + in + + let orig_A n = + match graph.nodes.(n) with + | Some ((_, CF_block instrs), _, _) -> + let vars = List.fold_left IdSet.union IdSet.empty (List.map instr_writes instrs) in + let vars = IdSet.diff vars (all_decls instrs) in + all_vars := IdSet.union vars !all_vars; + vars + | Some _ -> IdSet.empty + | None -> IdSet.empty + in + let phi_A = ref Bindings.empty in + + for n = 0 to graph.next - 1 do + IdSet.iter (fun a -> + let ds = match Bindings.find_opt a !defsites with Some ds -> ds | None -> IntSet.empty in + defsites := Bindings.add a (IntSet.add n ds) !defsites + ) (orig_A n) + done; + + IdSet.iter (fun a -> + let workset = ref (Bindings.find a !defsites) in + while not (IntSet.is_empty !workset) do + let n = IntSet.choose !workset in + workset := IntSet.remove n !workset; + IntSet.iter (fun y -> + let phi_A_a = match Bindings.find_opt a !phi_A with Some set -> set | None -> IntSet.empty in + if not (IntSet.mem y phi_A_a) then + begin + begin match graph.nodes.(y) with + | Some ((phis, cfnode), preds, succs) -> + graph.nodes.(y) <- Some ((Phi (a, Util.list_init (IntSet.cardinal preds) (fun _ -> a)) :: phis, cfnode), preds, succs) + | None -> assert false + end; + phi_A := Bindings.add a (IntSet.add y phi_A_a) !phi_A; + if not (IdSet.mem a (orig_A y)) then + workset := IntSet.add y !workset + end + ) df.(n) + done + ) !all_vars + +let rename_variables graph root children = + let counts = ref Bindings.empty in + let stacks = ref Bindings.empty in + + let get_count id = + match Bindings.find_opt id !counts with Some n -> n | None -> 0 + in + let top_stack id = + match Bindings.find_opt id !stacks with Some (x :: _) -> x | (Some [] | None) -> 0 + in + let push_stack id n = + stacks := Bindings.add id (n :: match Bindings.find_opt id !stacks with Some s -> s | None -> []) !stacks + in + + let rec fold_frag = function + | F_id id -> + let i = top_stack id in + F_id (append_id id ("_" ^ string_of_int i)) + | F_ref id -> + let i = top_stack id in + F_ref (append_id id ("_" ^ string_of_int i)) + | F_lit vl -> F_lit vl + | F_have_exception -> F_have_exception + | F_current_exception -> F_current_exception + | F_op (f1, op, f2) -> F_op (fold_frag f1, op, fold_frag f2) + | F_unary (op, f) -> F_unary (op, fold_frag f) + | F_call (id, fs) -> F_call (id, List.map fold_frag fs) + | F_field (f, field) -> F_field (fold_frag f, field) + | F_raw str -> F_raw str + | F_poly f -> F_poly (fold_frag f) + in + + let rec fold_clexp = function + | CL_id (id, ctyp) -> + let i = get_count id + 1 in + counts := Bindings.add id i !counts; + push_stack id i; + CL_id (append_id id ("_" ^ string_of_int i), ctyp) + | CL_field (clexp, field) -> CL_field (fold_clexp clexp, field) + | CL_addr clexp -> CL_addr (fold_clexp clexp) + | CL_tuple (clexp, n) -> CL_tuple (fold_clexp clexp, n) + | CL_current_exception ctyp -> CL_current_exception ctyp + | CL_have_exception -> CL_have_exception + | CL_return ctyp -> CL_return ctyp + | CL_void -> CL_void + in + + let fold_cval (f, ctyp) = (fold_frag f, ctyp) in + + let ssa_instr (I_aux (aux, annot)) = + let aux = match aux with + | I_funcall (clexp, extern, id, args) -> + let args = List.map fold_cval args in + I_funcall (fold_clexp clexp, extern, id, args) + | I_copy (clexp, cval) -> + let cval = fold_cval cval in + I_copy (fold_clexp clexp, cval) + | I_decl (ctyp, id) -> + let i = get_count id + 1 in + counts := Bindings.add id i !counts; + push_stack id i; + I_decl (ctyp, append_id id ("_" ^ string_of_int i)) + | I_init (ctyp, id, cval) -> + let cval = fold_cval cval in + let i = get_count id + 1 in + counts := Bindings.add id i !counts; + push_stack id i; + I_init (ctyp, append_id id ("_" ^ string_of_int i), cval) + | instr -> instr + in + I_aux (aux, annot) + in + + let ssa_cfnode = function + | CF_start -> CF_start + | CF_block instrs -> CF_block (List.map ssa_instr instrs) + | CF_label label -> CF_label label + in + + let ssa_ssanode = function + | Phi (id, args) -> + let i = get_count id + 1 in + counts := Bindings.add id i !counts; + push_stack id i; + Phi (append_id id ("_" ^ string_of_int i), args) + in + + let fix_phi j = function + | Phi (id, ids) -> + Phi (id, List.mapi (fun k a -> + if k = j then + let i = top_stack a in + append_id a ("_" ^ string_of_int i) + else a) + ids) + in + + let rec rename n = + let old_stacks = !stacks in + begin match graph.nodes.(n) with + | Some ((ssa, cfnode), preds, succs) -> + let ssa = List.map ssa_ssanode ssa in + graph.nodes.(n) <- Some ((ssa, ssa_cfnode cfnode), preds, succs); + List.iter (fun succ -> + match graph.nodes.(succ) with + | Some ((ssa, cfnode), preds, succs) -> + (* Suppose n is the j-th predecessor of succ *) + let rec find_j n succ = function + | pred :: preds -> + if pred = succ then n else find_j (n + 1) succ preds + | [] -> assert false + in + let j = find_j 0 n (IntSet.elements preds) in + graph.nodes.(succ) <- Some ((List.map (fix_phi j) ssa, cfnode), preds, succs) + | None -> assert false + ) (IntSet.elements succs) + | None -> assert false + end; + IntSet.iter (fun child -> rename child) (children.(n)); + stacks := old_stacks + in + rename root + +let ssa instrs = + let start, finish, cfg = control_flow_graph instrs in + let idom = immediate_dominators cfg start in + let children = dominator_children idom in + let df = dominance_frontiers cfg start idom children in + place_phi_functions cfg df; + rename_variables cfg start children; + cfg + +(* Debugging utilities for outputing Graphviz files. *) + +let string_of_phis = function + | [] -> "" + | phis -> Util.string_of_list "\\l" (fun (Phi (id, args)) -> string_of_id id ^ " = phi(" ^ Util.string_of_list ", " string_of_id args ^ ")") phis ^ "\\l" + +let string_of_node = function + | (phis, CF_label label) -> string_of_phis phis ^ label + | (phis, CF_block instrs) -> string_of_phis phis ^ Util.string_of_list "\\l" (fun instr -> String.escaped (Pretty_print_sail.to_string (pp_instr ~short:true instr))) instrs + | (phis, CF_start) -> string_of_phis phis ^ "START" + +let vertex_color = function + | (_, CF_start) -> "peachpuff" + | (_, CF_block _) -> "white" + | (_, CF_label _) -> "springgreen" + +let edge_color node_from node_to = + match node_from, node_to with + | CF_block _, CF_block _ -> "black" + | CF_label _, CF_block _ -> "red" + | CF_block _, CF_label _ -> "blue" + | _, _ -> "deeppink" + +let make_dot out_chan graph = + Util.opt_colors := false; + output_string out_chan "digraph DEPS {\n"; + let make_node i n = + output_string out_chan (Printf.sprintf " n%i [label=\"%s\";shape=box;style=filled;fillcolor=%s];\n" i (string_of_node n) (vertex_color n)) + in + let make_line i s = + output_string out_chan (Printf.sprintf " n%i -> n%i [color=black];\n" i s) + in + for i = 0 to graph.next - 1 do + match graph.nodes.(i) with + | Some (n, _, successors) -> + make_node i n; + IntSet.iter (fun s -> make_line i s) successors + | None -> () + done; + output_string out_chan "}\n"; + Util.opt_colors := true + +let make_dominators_dot out_chan idom graph = + Util.opt_colors := false; + output_string out_chan "digraph DOMS {\n"; + let make_node i n = + output_string out_chan (Printf.sprintf " n%i [label=\"%s\";shape=box;style=filled;fillcolor=%s];\n" i (string_of_node n) (vertex_color n)) + in + let make_line i s = + output_string out_chan (Printf.sprintf " n%i -> n%i [color=black];\n" i s) + in + for i = 0 to Array.length idom - 1 do + match graph.nodes.(i) with + | Some (n, _, _) -> + if idom.(i) = -1 then + make_node i n + else + (make_node i n; make_line i idom.(i)) + | None -> () + done; + output_string out_chan "}\n"; + Util.opt_colors := true diff --git a/src/jib/jib_ssa.mli b/src/jib/jib_ssa.mli new file mode 100644 index 00000000..3796a114 --- /dev/null +++ b/src/jib/jib_ssa.mli @@ -0,0 +1,85 @@ +(**************************************************************************) +(* 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 Array + +(** A mutable array based graph type, with nodes indexed by integers. *) +type 'a array_graph + +(** Create an empty array_graph, specifying the initial size of the + underlying array. *) +val make : initial_size:int -> unit -> 'a array_graph + +(** Add a vertex to a graph, returning the index of the inserted + vertex. If the number of vertices exceeds the size of the + underlying array, then it is dynamically resized. *) +val add_vertex : 'a -> 'a array_graph -> int + +(** Add an edge between two existing vertices. Raises Invalid_argument + if either of the vertices do not exist. *) +val add_edge : int -> int -> 'a array_graph -> unit + +type cf_node = + | CF_label of string + | CF_block of Jib.instr list + | CF_start + +val control_flow_graph : Jib.instr list -> int * int list * ('a list * cf_node) array_graph + +type ssa_elem = + | Phi of Ast.id * Ast.id list + +(** Convert a list of instructions into SSA form *) +val ssa : Jib.instr list -> (ssa_elem list * cf_node) array_graph + +(** Output the control-flow graph in graphviz format for + debugging. Can use 'dot -Tpng X.gv -o X.png' to generate a png + image of the graph. *) +val make_dot : out_channel -> (ssa_elem list * cf_node) array_graph -> unit diff --git a/src/jib/jib_util.ml b/src/jib/jib_util.ml new file mode 100644 index 00000000..81cd07ef --- /dev/null +++ b/src/jib/jib_util.ml @@ -0,0 +1,874 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* Alasdair Armstrong *) +(* Brian Campbell *) +(* Thomas Bauereiss *) +(* Anthony Fox *) +(* Jon French *) +(* Dominic Mulligan *) +(* Stephen Kell *) +(* Mark Wassell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + +open Ast +open Ast_util +open Jib +open 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 iend ?loc:(l=Parse_ast.Unknown) () = + I_aux (I_end, (instr_number (), l)) + +let iblock ?loc:(l=Parse_ast.Unknown) instrs = + I_aux (I_block instrs, (instr_number (), l)) + +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 + | CL_return ctyp -> CL_return ctyp + | CL_void -> CL_void + +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_end -> I_end + + | I_reset (ctyp, id) when Id.compare id from_id = 0 -> I_reset (ctyp, to_id) + | I_reset (ctyp, id) -> I_reset (ctyp, id) + + | 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 (n, true) -> "sbits(" ^ string_of_int n ^ ", dec)" + | CT_sbits (n, false) -> "sbits(" ^ string_of_int n ^ ", inc)" + | CT_fint n -> "int(" ^ string_of_int n ^ ")" + | CT_bit -> "bit" + | CT_unit -> "unit" + | 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_tup ctyps -> "(" ^ Util.string_of_list ", " full_string_of_ctyp ctyps ^ ")" + | 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_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 ^ ")" + | ctyp -> string_of_ctyp ctyp + +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 (m1, d1), CT_sbits (m2, d2) -> m1 = m2 && d1 = d2 + | CT_fbits (m1, d1), CT_fbits (m2, d2) -> m1 = m2 && d1 = d2 + | CT_bit, CT_bit -> true + | CT_fint n, CT_fint m -> n = m + | 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_compare ctyp1 ctyp2 = + let lex_ord c1 c2 = if c1 = 0 then c2 else c1 in + match ctyp1, ctyp2 with + | CT_lint, CT_lint -> 0 + | CT_lint, _ -> 1 + | _, CT_lint -> -1 + + | CT_fint n, CT_fint m -> compare n m + | CT_fint _, _ -> 1 + | _, CT_fint _ -> -1 + + | CT_fbits (n, ord1), CT_fbits (m, ord2) -> lex_ord (compare n m) (compare ord1 ord2) + | CT_fbits _, _ -> 1 + | _, CT_fbits _ -> -1 + + | CT_sbits (n, ord1), CT_sbits (m, ord2) -> lex_ord (compare n m) (compare ord1 ord2) + | CT_sbits _, _ -> 1 + | _, CT_sbits _ -> -1 + + | CT_lbits ord1 , CT_lbits ord2 -> compare ord1 ord2 + | CT_lbits _, _ -> 1 + | _, CT_lbits _ -> -1 + + | CT_bit, CT_bit -> 0 + | CT_bit, _ -> 1 + | _, CT_bit -> -1 + + | CT_unit, CT_unit -> 0 + | CT_unit, _ -> 1 + | _, CT_unit -> -1 + + | CT_real, CT_real -> 0 + | CT_real, _ -> 1 + | _, CT_real -> -1 + + | CT_poly, CT_poly -> 0 + | CT_poly, _ -> 1 + | _, CT_poly -> -1 + + | CT_bool, CT_bool -> 0 + | CT_bool, _ -> 1 + | _, CT_bool -> -1 + + | CT_string, CT_string -> 0 + | CT_string, _ -> 1 + | _, CT_string -> -1 + + | CT_ref ctyp1, CT_ref ctyp2 -> ctyp_compare ctyp1 ctyp2 + | CT_ref _, _ -> 1 + | _, CT_ref _ -> -1 + + | CT_list ctyp1, CT_list ctyp2 -> ctyp_compare ctyp1 ctyp2 + | CT_list _, _ -> 1 + | _, CT_list _ -> -1 + + | CT_vector (d1, ctyp1), CT_vector (d2, ctyp2) -> + lex_ord (ctyp_compare ctyp1 ctyp2) (compare d1 d2) + | CT_vector _, _ -> 1 + | _, CT_vector _ -> -1 + + | ctyp1, ctyp2 -> String.compare (full_string_of_ctyp ctyp1) (full_string_of_ctyp ctyp2) + +module CT = struct + type t = ctyp + let compare ctyp1 ctyp2 = ctyp_compare ctyp1 ctyp2 +end + +module CTSet = Set.Make(CT) + +let rec ctyp_unify ctyp1 ctyp2 = + match ctyp1, ctyp2 with + | CT_tup ctyps1, CT_tup ctyps2 when List.length ctyps1 = List.length ctyps2 -> + 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 (full_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" + | CL_return ctyp -> string "return : " ^^ pp_ctyp ctyp + | CL_void -> string "void" + +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_end -> + pp_keyword "end" + | 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 + +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 + | CL_return _ -> IdSet.empty + | CL_void -> 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.empty + | 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 + | I_end -> IdSet.empty, IdSet.empty + +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 + | CL_return ctyp -> CL_return (f ctyp) + | CL_void -> CL_void + +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_end -> I_end + | (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 _ | I_end -> instr + | I_if (cval, instrs1, instrs2, ctyp) -> + I_if (cval, List.map (map_instr f) instrs1, List.map (map_instr f) instrs2, ctyp) + | I_block instrs -> + 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)) + +(** Iterate over each instruction within an instruction, bottom-up *) +let rec iter_instr f (I_aux (instr, aux)) = + 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 _ | I_end -> f (I_aux (instr, aux)) + | I_if (cval, instrs1, instrs2, ctyp) -> + List.iter (iter_instr f) instrs1; + List.iter (iter_instr f) instrs2 + | I_block instrs | I_try_block instrs -> + List.iter (iter_instr f) instrs + +(** 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 _ | I_end -> instr + in + I_aux (instr, aux) + +let map_instr_list f instrs = + List.map (map_instr f) instrs + +let map_instrs_list f instrs = + f (List.map (map_instrs f) instrs) + +let rec instr_ids (I_aux (instr, _)) = + let reads, writes = instr_deps instr in + IdSet.union reads writes + +let rec instr_reads (I_aux (instr, _)) = + fst (instr_deps instr) + +let rec instr_writes (I_aux (instr, _)) = + snd (instr_deps instr) + +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) + +(** GLOBAL: label_counter is used to make sure all labels have unique + names. Like gensym_counter it should be safe to reset between + top-level definitions. **) +let label_counter = ref 0 + +let label str = + let str = str ^ string_of_int !label_counter in + incr label_counter; + str + +let cval_ctyp = function (_, ctyp) -> ctyp + +let rec clexp_ctyp = function + | CL_id (_, ctyp) -> ctyp + | CL_return ctyp -> ctyp + | CL_field (clexp, field) -> + begin match clexp_ctyp clexp with + | CT_struct (id, ctors) -> + begin + try snd (List.find (fun (id, ctyp) -> string_of_id id = field) ctors) with + | Not_found -> failwith ("Struct type " ^ string_of_id id ^ " does not have a constructor " ^ field) + end + | ctyp -> failwith ("Bad ctyp for CL_field " ^ string_of_ctyp ctyp) + end + | CL_addr clexp -> + begin match clexp_ctyp clexp with + | CT_ref ctyp -> ctyp + | ctyp -> failwith ("Bad ctyp for CL_addr " ^ string_of_ctyp ctyp) + end + | CL_tuple (clexp, n) -> + begin match clexp_ctyp clexp with + | CT_tup typs -> + begin + try List.nth typs n with + | _ -> failwith "Tuple assignment index out of bounds" + end + | ctyp -> failwith ("Bad ctyp for CL_addr " ^ string_of_ctyp ctyp) + end + | CL_have_exception -> CT_bool + | CL_current_exception ctyp -> ctyp + | CL_void -> CT_unit + +let rec instr_ctyps (I_aux (instr, aux)) = + match instr with + | I_decl (ctyp, _) | I_reset (ctyp, _) | I_clear (ctyp, _) | I_undefined ctyp -> + CTSet.singleton ctyp + | I_init (ctyp, _, cval) | I_reinit (ctyp, _, cval) -> + CTSet.add ctyp (CTSet.singleton (cval_ctyp cval)) + | I_if (cval, instrs1, instrs2, ctyp) -> + CTSet.union (instrs_ctyps instrs1) (instrs_ctyps instrs2) + |> CTSet.add (cval_ctyp cval) + |> CTSet.add ctyp + | I_funcall (clexp, _, _, cvals) -> + List.fold_left (fun m ctyp -> CTSet.add ctyp m) CTSet.empty (List.map cval_ctyp cvals) + |> CTSet.add (clexp_ctyp clexp) + | I_copy (clexp, cval) | I_alias (clexp, cval) -> + CTSet.add (clexp_ctyp clexp) (CTSet.singleton (cval_ctyp cval)) + | I_block instrs | I_try_block instrs -> + instrs_ctyps instrs + | I_throw cval | I_jump (cval, _) | I_return cval -> + CTSet.singleton (cval_ctyp cval) + | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_match_failure | I_end -> + CTSet.empty + +and instrs_ctyps instrs = List.fold_left CTSet.union CTSet.empty (List.map instr_ctyps instrs) + +let ctype_def_ctyps = function + | CTD_enum _ -> [] + | CTD_struct (_, fields) -> List.map snd fields + | CTD_variant (_, ctors) -> List.map snd ctors + +let cdef_ctyps = function + | CDEF_reg_dec (_, ctyp, instrs) -> + CTSet.add ctyp (instrs_ctyps instrs) + | CDEF_spec (_, ctyps, ctyp) -> + CTSet.add ctyp (List.fold_left (fun m ctyp -> CTSet.add ctyp m) CTSet.empty ctyps) + | CDEF_fundef (_, _, _, instrs) | CDEF_startup (_, instrs) | CDEF_finish (_, instrs) -> + instrs_ctyps instrs + | CDEF_type tdef -> + List.fold_right CTSet.add (ctype_def_ctyps tdef) CTSet.empty + | CDEF_let (_, bindings, instrs) -> + List.fold_left (fun m ctyp -> CTSet.add ctyp m) CTSet.empty (List.map snd bindings) + |> CTSet.union (instrs_ctyps instrs) + +let rec c_ast_registers = function + | CDEF_reg_dec (id, ctyp, instrs) :: ast -> (id, ctyp, instrs) :: c_ast_registers ast + | _ :: ast -> c_ast_registers ast + | [] -> [] + +let instr_split_at f = + let rec instr_split_at' f before = function + | [] -> (List.rev before, []) + | instr :: instrs when f instr -> (List.rev before, instr :: instrs) + | instr :: instrs -> instr_split_at' f (instr :: before) instrs + in + instr_split_at' f [] + +let rec instrs_rename from_id to_id = + let rename id = if Id.compare id from_id = 0 then to_id else id in + let crename = cval_rename from_id to_id in + let irename instrs = instrs_rename from_id to_id instrs in + let lrename = clexp_rename from_id to_id in + function + | (I_aux (I_decl (ctyp, new_id), _) :: _) as instrs when Id.compare from_id new_id = 0 -> instrs + | I_aux (I_decl (ctyp, new_id), aux) :: instrs -> I_aux (I_decl (ctyp, new_id), aux) :: irename instrs + | I_aux (I_reset (ctyp, id), aux) :: instrs -> I_aux (I_reset (ctyp, rename id), aux) :: irename instrs + | I_aux (I_init (ctyp, id, cval), aux) :: instrs -> I_aux (I_init (ctyp, rename id, crename cval), aux) :: irename instrs + | I_aux (I_reinit (ctyp, id, cval), aux) :: instrs -> I_aux (I_reinit (ctyp, rename id, crename cval), aux) :: irename instrs + | I_aux (I_if (cval, then_instrs, else_instrs, ctyp), aux) :: instrs -> + I_aux (I_if (crename cval, irename then_instrs, irename else_instrs, ctyp), aux) :: irename instrs + | I_aux (I_jump (cval, label), aux) :: instrs -> I_aux (I_jump (crename cval, label), aux) :: irename instrs + | I_aux (I_funcall (clexp, extern, id, cvals), aux) :: instrs -> + I_aux (I_funcall (lrename clexp, extern, rename id, List.map crename cvals), aux) :: irename instrs + | I_aux (I_copy (clexp, cval), aux) :: instrs -> I_aux (I_copy (lrename clexp, crename cval), aux) :: irename instrs + | I_aux (I_alias (clexp, cval), aux) :: instrs -> I_aux (I_alias (lrename clexp, crename cval), aux) :: irename instrs + | I_aux (I_clear (ctyp, id), aux) :: instrs -> I_aux (I_clear (ctyp, rename id), aux) :: irename instrs + | I_aux (I_return cval, aux) :: instrs -> I_aux (I_return (crename cval), aux) :: irename instrs + | I_aux (I_block block, aux) :: instrs -> I_aux (I_block (irename block), aux) :: irename instrs + | I_aux (I_try_block block, aux) :: instrs -> I_aux (I_try_block (irename block), aux) :: irename instrs + | I_aux (I_throw cval, aux) :: instrs -> I_aux (I_throw (crename cval), aux) :: irename instrs + | (I_aux ((I_comment _ | I_raw _ | I_end | I_label _ | I_goto _ | I_match_failure | I_undefined _), _) as instr) :: instrs -> instr :: irename instrs + | [] -> [] |
