summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/jib/c_backend.ml181
-rw-r--r--src/jib/c_backend.mli12
-rw-r--r--src/jib/c_codegen.ml1617
-rw-r--r--src/jib/jib_compile.ml28
-rw-r--r--src/jib/jib_compile.mli11
-rw-r--r--src/jib/jib_ir.ml2
-rw-r--r--src/jib/jib_optimize.ml2
-rw-r--r--src/jib/jib_smt.ml18
-rw-r--r--src/jib/jib_ssa.ml1
-rw-r--r--src/jib/jib_util.ml8
-rw-r--r--src/rewrites.ml1
-rw-r--r--src/sail.ml26
12 files changed, 1836 insertions, 71 deletions
diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml
index 2b2234b5..829f4d37 100644
--- a/src/jib/c_backend.ml
+++ b/src/jib/c_backend.ml
@@ -63,7 +63,6 @@ module Big_int = Nat_big_num
let opt_static = ref false
let opt_no_main = ref false
-let opt_memo_cache = ref false
let opt_no_lib = ref false
let opt_no_rts = ref false
let opt_prefix = ref "z"
@@ -130,6 +129,41 @@ let rec is_stack_ctyp ctyp = match ctyp with
let v_mask_lower i = V_lit (VL_bits (Util.list_init i (fun _ -> Sail2_values.B1), true), CT_fbits (i, true))
+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 (V_lit (VL_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 (V_lit (VL_bits (padding @ content, true), CT_fbits (String.length str * 4, true)))
+ | L_unit -> Some (V_lit (VL_unit, CT_unit))
+ | L_true -> Some (V_lit (VL_bool true, CT_bool))
+ | L_false -> Some (V_lit (VL_bool false, CT_bool))
+ | _ -> None
+
module C_config : Config = struct
(** Convert a sail type into a C-type. This function can be quite
@@ -232,41 +266,6 @@ module C_config : Config = struct
(* 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 (V_lit (VL_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 (V_lit (VL_bits (padding @ content, true), CT_fbits (String.length str * 4, true)))
- | L_unit -> Some (V_lit (VL_unit, CT_unit))
- | L_true -> Some (V_lit (VL_bool true, CT_bool))
- | L_false -> Some (V_lit (VL_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 (convert_typ { ctx with local_env = env } typ) ->
@@ -565,6 +564,100 @@ module C_config : Config = struct
let use_real = false
end
+(* When compiling to a C library, we want to do things slightly
+ differently. First, to ensure that functions have a predictable
+ type and calling convention, we don't use the SMT solver to
+ optimize types at all. Second we don't apply the analyse primitives
+ step in optimize_anf for similar reasons. *)
+module Clib_config : Config = struct
+ let rec convert_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, _) when
+ string_of_id id = "range" || string_of_id id = "atom" || string_of_id id = "implicit" || string_of_id id = "itself" ->
+ 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
+ | _, _ ->
+ CT_lint
+ end
+
+ | Typ_app (id, [A_aux (A_typ typ, _)]) when string_of_id id = "list" ->
+ CT_list (convert_typ ctx typ)
+
+ | Typ_app (id, [A_aux (A_nexp n, _);
+ A_aux (A_order ord, _)])
+ when string_of_id id = "bitvector" ->
+ 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)
+ | _ -> 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, convert_typ ctx typ)
+
+ | Typ_app (id, [A_aux (A_typ typ, _)]) when string_of_id id = "register" ->
+ CT_ref (convert_typ ctx typ)
+
+ | Typ_id id | Typ_app (id, _) when Bindings.mem id ctx.records -> CT_struct (id, Bindings.find id ctx.records |> UBindings.bindings)
+ | Typ_id id | Typ_app (id, _) when Bindings.mem id ctx.variants -> CT_variant (id, Bindings.find id ctx.variants |> UBindings.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 (convert_typ ctx) typs)
+
+ | Typ_exist _ ->
+ 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
+ convert_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 c_literals ctx =
+ let rec c_literal env l = function
+ | AV_lit (lit, typ) as v when is_stack_ctyp (convert_typ { ctx with local_env = env } typ) ->
+ begin
+ match literal_to_fragment lit with
+ | Some cval -> AV_cval (cval, typ)
+ | None -> v
+ end
+ | AV_tuple avals -> AV_tuple (List.map (c_literal env l) avals)
+ | v -> v
+ in
+ map_aval c_literal
+
+ let optimize_anf ctx aexp = c_literals ctx aexp
+
+ let unroll_loops () = None
+ let specialize_calls = false
+ let ignore_64 = false
+ let struct_value = false
+ let use_real = false
+end
+
(** 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
@@ -1329,6 +1422,7 @@ let rec sgen_clexp = function
| CL_id (Throw_location _, _) -> "throw_location"
| CL_id (Return _, _) -> assert false
| CL_id (Name (id, _), _) -> "&" ^ sgen_id id
+ | CL_id (Global (id, _), _) -> "&" ^ sgen_id id
| CL_field (clexp, field) -> "&((" ^ sgen_clexp clexp ^ ")->" ^ zencode_uid field ^ ")"
| CL_tuple (clexp, n) -> "&((" ^ sgen_clexp clexp ^ ")->ztup" ^ string_of_int n ^ ")"
| CL_addr clexp -> "(*(" ^ sgen_clexp clexp ^ "))"
@@ -1341,6 +1435,7 @@ let rec sgen_clexp_pure = function
| CL_id (Throw_location _, _) -> "throw_location"
| CL_id (Return _, _) -> assert false
| CL_id (Name (id, _), _) -> sgen_id id
+ | CL_id (Global (id, _), _) -> sgen_id id
| CL_field (clexp, field) -> sgen_clexp_pure clexp ^ "." ^ zencode_uid field
| CL_tuple (clexp, n) -> sgen_clexp_pure clexp ^ ".ztup" ^ string_of_int n
| CL_addr clexp -> "(*(" ^ sgen_clexp_pure clexp ^ "))"
@@ -2222,7 +2317,7 @@ let jib_of_ast env ast =
let module Jibc = Make(C_config) in
let ctx = initial_ctx (add_special_functions env) in
Jibc.compile_ast ctx ast
-
+
let compile_ast env output_chan c_includes ast =
try
let recursive_functions = Spec_analysis.top_sort_defs ast |> get_recursive_functions in
@@ -2336,3 +2431,15 @@ let compile_ast env output_chan c_includes ast =
with
| Type_error (_, l, err) ->
c_error ~loc:l ("Unexpected type error when compiling to C:\n" ^ Type_error.string_of_type_error err)
+
+let jib_of_ast_clib env ast =
+ let module Jibc = Make(Clib_config) in
+ let ctx = initial_ctx (add_special_functions env) in
+ Jibc.compile_ast ctx ast
+
+let compile_ast_clib env ast codegen =
+ let cdefs, ctx = jib_of_ast env ast in
+ let cdefs', _ = Jib_optimize.remove_tuples cdefs ctx in
+ Jib_interactive.ir := cdefs';
+ let cdefs = insert_heap_returns Bindings.empty cdefs in
+ codegen ctx cdefs
diff --git a/src/jib/c_backend.mli b/src/jib/c_backend.mli
index e627ebd8..2334cc0e 100644
--- a/src/jib/c_backend.mli
+++ b/src/jib/c_backend.mli
@@ -88,15 +88,6 @@ val opt_prefix : string ref
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
- 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
@@ -108,3 +99,6 @@ val optimize_fixed_bits : bool ref
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
+
+val jib_of_ast_clib : Env.t -> tannot Ast.defs -> cdef list * Jib_compile.ctx
+val compile_ast_clib : Env.t -> tannot Ast.defs -> (Jib_compile.ctx -> cdef list -> unit) -> unit
diff --git a/src/jib/c_codegen.ml b/src/jib/c_codegen.ml
new file mode 100644
index 00000000..6aa0060c
--- /dev/null
+++ b/src/jib/c_codegen.ml
@@ -0,0 +1,1617 @@
+(**************************************************************************)
+(* 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 Printf
+open Value2
+
+module StringMap = Map.Make(String)
+module Big_int = Nat_big_num
+
+let opt_no_main = ref false
+let opt_no_lib = ref false
+let opt_no_rts = ref false
+
+let (gensym, _) = symbol_generator "c2"
+let ngensym () = name (gensym ())
+
+let zencode_id id = Util.zencode_string (string_of_id id)
+
+let zencode_uid (id, ctyps) =
+ match ctyps with
+ | [] -> Util.zencode_string (string_of_id id)
+ | _ -> Util.zencode_string (string_of_id id ^ "#" ^ Util.string_of_list "_" string_of_ctyp ctyps)
+
+let ctor_bindings = List.fold_left (fun map (id, ctyp) -> UBindings.add id ctyp map) UBindings.empty
+
+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))
+
+(** This function is used to split types into those we allocate on the
+ stack, versus those which need to live on the heap, or otherwise
+ require some additional memory management *)
+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_lint when !optimize_fixed_int -> true *)
+ | CT_lint -> false
+ (* | CT_lbits _ when !optimize_fixed_bits -> true *)
+ | CT_lbits _ -> false
+ | CT_real | CT_string | CT_list _ | CT_vector _ | CT_fvector _ -> 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
+ | CT_constant n -> Big_int.less_equal (min_int 64) n && Big_int.greater_equal n (max_int 64)
+
+let v_mask_lower i = V_lit (VL_bits (Util.list_init i (fun _ -> Sail2_values.B1), true), CT_fbits (i, true))
+
+type codegen_options = {
+ exports : string Bindings.t;
+ exports_mangled : string StringMap.t;
+ }
+
+let add_export opts id = { opts with exports = Bindings.add id (string_of_id id) opts.exports }
+
+let add_custom_export opts id into = { opts with exports = Bindings.add id into opts.exports }
+
+let add_mangled_rename opts (from, into) = { opts with exports_mangled = StringMap.add from into opts.exports_mangled }
+
+let add_export_uid opts (id, ctyps) =
+ match ctyps with
+ | [] -> { opts with exports = Bindings.add id (string_of_id id) opts.exports }
+ | _ -> opts
+
+let ctype_def_initial_options opts = function
+ | CTD_enum (id, ids) ->
+ List.fold_left add_export (add_export opts id) ids
+ | CTD_struct (id, ctors) ->
+ List.fold_left add_export_uid (add_export opts id) (List.map fst ctors)
+ | _ -> opts
+
+let cdef_initial_options opts = function
+ | CDEF_type ctype_def -> ctype_def_initial_options opts ctype_def
+ | CDEF_reg_dec (id, _, _) -> add_export opts id
+ | CDEF_let (_, bindings, _) -> List.fold_left (fun opts (id, _) -> add_export opts id) opts bindings
+ | _ -> opts
+
+let initial_options = {
+ exports = Bindings.empty;
+ exports_mangled = StringMap.empty;
+ }
+
+let default_options cdefs =
+ let opts = List.fold_left cdef_initial_options initial_options cdefs in
+ let opts = add_export opts (mk_id "initialize_registers") in
+ let opts = add_custom_export opts (mk_id "main") "sail_main" in
+ List.fold_left add_mangled_rename opts (List.init 9 (fun n -> "ztup" ^ string_of_int n, "tuple_" ^ string_of_int n))
+
+module type Config = sig
+ val opts : codegen_options
+end
+
+module Make(C: Config) = struct
+
+let mangle str =
+ let mangled = Util.zencode_string str in
+ match StringMap.find_opt mangled C.opts.exports_mangled with
+ | Some export -> export
+ | None -> mangled
+
+let sgen_id id =
+ match Bindings.find_opt id C.opts.exports with
+ | Some export -> export
+ | None -> mangle (string_of_id id)
+
+let sgen_name =
+ function
+ | Name (id, _) ->
+ sgen_id id
+ | Global (id, _) ->
+ sprintf "(state->%s)" (sgen_id id)
+ | Have_exception _ ->
+ "(state->have_exception)"
+ | Return _ ->
+ assert false
+ | Current_exception _ ->
+ "(*(state->current_exception))"
+ | Throw_location _ ->
+ "(state->throw_location)"
+
+let sgen_uid (id, ctyps) =
+ match ctyps with
+ | [] -> sgen_id id
+ | _ ->
+ mangle (string_of_id id ^ "#" ^ Util.string_of_list "_" string_of_ctyp ctyps)
+
+let codegen_id id = string (sgen_id id)
+let codegen_uid id = string (sgen_uid id)
+
+let sgen_function_id id = sgen_id id
+let sgen_function_uid uid = sgen_uid uid
+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 _ -> "uint64_t"
+ | CT_sbits _ -> "sbits"
+ | CT_fint _ -> "int64_t"
+ | CT_constant _ -> "int64_t"
+ | 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_fvector (_, ord, typ) -> sgen_ctyp (CT_vector (ord, typ))
+ | 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_constant _ -> "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_fvector (_, ord, typ) -> sgen_ctyp_name (CT_vector (ord, typ))
+ | 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_mask n =
+ if n = 0 then
+ "UINT64_C(0)"
+ else if n <= 64 then
+ let chars_F = String.make (n / 4) 'F' in
+ let first = match (n mod 4) with
+ | 0 -> ""
+ | 1 -> "1"
+ | 2 -> "3"
+ | 3 -> "7"
+ | _ -> assert false
+ in
+ "UINT64_C(0x" ^ first ^ chars_F ^ ")"
+ else
+ failwith "Tried to create a mask literal for a vector greater than 64 bits."
+
+let rec sgen_value = function
+ | VL_bits ([], _) -> "UINT64_C(0)"
+ | VL_bits (bs, true) -> "UINT64_C(" ^ Sail2_values.show_bitlist bs ^ ")"
+ | VL_bits (bs, false) -> "UINT64_C(" ^ Sail2_values.show_bitlist (List.rev bs) ^ ")"
+ | VL_int i -> Big_int.to_string i ^ "l"
+ | VL_bool true -> "true"
+ | VL_bool false -> "false"
+ | VL_unit -> "UNIT"
+ | VL_bit Sail2_values.B0 -> "UINT64_C(0)"
+ | VL_bit Sail2_values.B1 -> "UINT64_C(1)"
+ | VL_bit Sail2_values.BU -> failwith "Undefined bit found in value"
+ | VL_real str -> str
+ | VL_string str -> "\"" ^ str ^ "\""
+ | VL_empty_list -> "NULL"
+ | VL_enum element -> mangle element
+ | VL_ref r -> "&(state->" ^ sgen_id (mk_id r) ^ ")"
+ | VL_undefined ->
+ Reporting.unreachable Parse_ast.Unknown __POS__ "Cannot generate C value for an undefined literal"
+
+let rec sgen_cval ctx = function
+ | V_id (id, ctyp) ->
+ sgen_name id
+ | V_lit (vl, ctyp) -> sgen_value vl
+ | V_call (op, cvals) -> sgen_call ctx op cvals
+ | V_field (f, field) ->
+ sprintf "%s.%s" (sgen_cval ctx f) (sgen_uid field)
+ | V_tuple_member (f, _, n) ->
+ sprintf "%s.%s" (sgen_cval ctx f) (mangle ("tup" ^ string_of_int n))
+ | V_ctor_kind (f, ctor, unifiers, _) ->
+ sgen_cval ctx f ^ ".kind"
+ ^ " != Kind_" ^ zencode_uid (ctor, unifiers)
+ | V_struct (fields, _) ->
+ sprintf "{%s}"
+ (Util.string_of_list ", " (fun (field, cval) -> zencode_uid field ^ " = " ^ sgen_cval ctx cval) fields)
+ | V_ctor_unwrap (ctor, f, unifiers, _) ->
+ sprintf "%s.%s"
+ (sgen_cval ctx f)
+ (sgen_uid (ctor, unifiers))
+ | V_poly (f, _) -> sgen_cval ctx f
+
+and sgen_call ctx op cvals =
+ match op, cvals with
+ | Bnot, [v] -> "!(" ^ sgen_cval ctx v ^ ")"
+ | List_hd, [v] ->
+ sprintf "(%s).hd" ("*" ^ sgen_cval ctx v)
+ | List_tl, [v] ->
+ sprintf "(%s).tl" ("*" ^ sgen_cval ctx v)
+ | Eq, [v1; v2] ->
+ begin match cval_ctyp v1 with
+ | CT_sbits _ ->
+ sprintf "eq_sbits(%s, %s)" (sgen_cval ctx v1) (sgen_cval ctx v2)
+ | _ ->
+ sprintf "(%s == %s)" (sgen_cval ctx v1) (sgen_cval ctx v2)
+ end
+ | Neq, [v1; v2] ->
+ begin match cval_ctyp v1 with
+ | CT_sbits _ ->
+ sprintf "neq_sbits(%s, %s)" (sgen_cval ctx v1) (sgen_cval ctx v2)
+ | _ ->
+ sprintf "(%s != %s)" (sgen_cval ctx v1) (sgen_cval ctx v2)
+ end
+ | Ilt, [v1; v2] ->
+ sprintf "(%s < %s)" (sgen_cval ctx v1) (sgen_cval ctx v2)
+ | Igt, [v1; v2] ->
+ sprintf "(%s > %s)" (sgen_cval ctx v1) (sgen_cval ctx v2)
+ | Ilteq, [v1; v2] ->
+ sprintf "(%s <= %s)" (sgen_cval ctx v1) (sgen_cval ctx v2)
+ | Igteq, [v1; v2] ->
+ sprintf "(%s >= %s)" (sgen_cval ctx v1) (sgen_cval ctx v2)
+ | Iadd, [v1; v2] ->
+ sprintf "(%s + %s)" (sgen_cval ctx v1) (sgen_cval ctx v2)
+ | Isub, [v1; v2] ->
+ sprintf "(%s - %s)" (sgen_cval ctx v1) (sgen_cval ctx v2)
+ | Unsigned 64, [vec] ->
+ sprintf "((mach_int) %s)" (sgen_cval ctx vec)
+ | Signed 64, [vec] ->
+ begin match cval_ctyp vec with
+ | CT_fbits (n, _) ->
+ sprintf "fast_signed(%s, %d)" (sgen_cval ctx vec) n
+ | _ -> assert false
+ end
+ | Bvand, [v1; v2] ->
+ begin match cval_ctyp v1 with
+ | CT_fbits _ ->
+ sprintf "(%s & %s)" (sgen_cval ctx v1) (sgen_cval ctx v2)
+ | CT_sbits _ ->
+ sprintf "and_sbits(%s, %s)" (sgen_cval ctx v1) (sgen_cval ctx v2)
+ | _ -> assert false
+ end
+ | Bvnot, [v] ->
+ begin match cval_ctyp v with
+ | CT_fbits (n, _) ->
+ sprintf "(~(%s) & %s)" (sgen_cval ctx v) (sgen_cval ctx (v_mask_lower n))
+ | CT_sbits _ ->
+ sprintf "not_sbits(%s)" (sgen_cval ctx v)
+ | _ -> assert false
+ end
+ | Bvor, [v1; v2] ->
+ begin match cval_ctyp v1 with
+ | CT_fbits _ ->
+ sprintf "(%s | %s)" (sgen_cval ctx v1) (sgen_cval ctx v2)
+ | CT_sbits _ ->
+ sprintf "or_sbits(%s, %s)" (sgen_cval ctx v1) (sgen_cval ctx v2)
+ | _ -> assert false
+ end
+ | Bvxor, [v1; v2] ->
+ begin match cval_ctyp v1 with
+ | CT_fbits _ ->
+ sprintf "(%s ^ %s)" (sgen_cval ctx v1) (sgen_cval ctx v2)
+ | CT_sbits _ ->
+ sprintf "xor_sbits(%s, %s)" (sgen_cval ctx v1) (sgen_cval ctx v2)
+ | _ -> assert false
+ end
+ | Bvadd, [v1; v2] ->
+ begin match cval_ctyp v1 with
+ | CT_fbits (n, _) ->
+ sprintf "((%s + %s) & %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) (sgen_cval ctx (v_mask_lower n))
+ | CT_sbits _ ->
+ sprintf "add_sbits(%s, %s)" (sgen_cval ctx v1) (sgen_cval ctx v2)
+ | _ -> assert false
+ end
+ | Bvsub, [v1; v2] ->
+ begin match cval_ctyp v1 with
+ | CT_fbits (n, _) ->
+ sprintf "((%s - %s) & %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) (sgen_cval ctx (v_mask_lower n))
+ | CT_sbits _ ->
+ sprintf "sub_sbits(%s, %s)" (sgen_cval ctx v1) (sgen_cval ctx v2)
+ | _ -> assert false
+ end
+ | Bvaccess, [vec; n] ->
+ begin match cval_ctyp vec with
+ | CT_fbits _ ->
+ sprintf "(UINT64_C(1) & (%s >> %s))" (sgen_cval ctx vec) (sgen_cval ctx n)
+ | CT_sbits _ ->
+ sprintf "(UINT64_C(1) & (%s.bits >> %s))" (sgen_cval ctx vec) (sgen_cval ctx n)
+ | _ -> assert false
+ end
+ | Slice len, [vec; start] ->
+ begin match cval_ctyp vec with
+ | CT_fbits _ ->
+ sprintf "(safe_rshift(UINT64_MAX, 64 - %d) & (%s >> %s))" len (sgen_cval ctx vec) (sgen_cval ctx start)
+ | CT_sbits _ ->
+ sprintf "(safe_rshift(UINT64_MAX, 64 - %d) & (%s.bits >> %s))" len (sgen_cval ctx vec) (sgen_cval ctx start)
+ | _ -> assert false
+ end
+ | Sslice 64, [vec; start; len] ->
+ begin match cval_ctyp vec with
+ | CT_fbits _ ->
+ sprintf "sslice(%s, %s, %s)" (sgen_cval ctx vec) (sgen_cval ctx start) (sgen_cval ctx len)
+ | CT_sbits _ ->
+ sprintf "sslice(%s.bits, %s, %s)" (sgen_cval ctx vec) (sgen_cval ctx start) (sgen_cval ctx len)
+ | _ -> assert false
+ end
+ | Set_slice, [vec; start; slice] ->
+ begin match cval_ctyp vec, cval_ctyp slice with
+ | CT_fbits (n, _), CT_fbits (m, _) ->
+ sprintf "((%s & ~(%s << %s)) | (%s << %s))" (sgen_cval ctx vec) (sgen_mask m) (sgen_cval ctx start) (sgen_cval ctx slice) (sgen_cval ctx start)
+ | _ -> assert false
+ end
+ | Zero_extend n, [v] ->
+ begin match cval_ctyp v with
+ | CT_fbits _ -> sgen_cval ctx v
+ | CT_sbits _ ->
+ sprintf "fast_zero_extend(%s, %d)" (sgen_cval ctx v) n
+ | _ -> assert false
+ end
+ | Sign_extend n, [v] ->
+ begin match cval_ctyp v with
+ | CT_fbits (m, _) ->
+ sprintf "fast_sign_extend(%s, %d, %d)" (sgen_cval ctx v) m n
+ | CT_sbits _ ->
+ sprintf "fast_sign_extend2(%s, %d)" (sgen_cval ctx v) n
+ | _ -> assert false
+ end
+ | Replicate n, [v] ->
+ begin match cval_ctyp v with
+ | CT_fbits (m, _) ->
+ sprintf "fast_replicate_bits(UINT64_C(%d), %s, %d)" m (sgen_cval ctx v) n
+ | _ -> assert false
+ end
+ | Concat, [v1; v2] ->
+ (* Optimized routines for all combinations of fixed and small bits
+ appends, where the result is guaranteed to be smaller than 64. *)
+ begin match cval_ctyp v1, cval_ctyp v2 with
+ | CT_fbits (0, _), CT_fbits (n2, _) ->
+ sgen_cval ctx v2
+ | CT_fbits (n1, _), CT_fbits (n2, _) ->
+ sprintf "(%s << %d) | %s" (sgen_cval ctx v1) n2 (sgen_cval ctx v2)
+ | CT_sbits (64, ord1), CT_fbits (n2, _) ->
+ sprintf "append_sf(%s, %s, %d)" (sgen_cval ctx v1) (sgen_cval ctx v2) n2
+ | CT_fbits (n1, ord1), CT_sbits (64, ord2) ->
+ sprintf "append_fs(%s, %d, %s)" (sgen_cval ctx v1) n1 (sgen_cval ctx v2)
+ | CT_sbits (64, ord1), CT_sbits (64, ord2) ->
+ sprintf "append_ss(%s, %s)" (sgen_cval ctx v1) (sgen_cval ctx v2)
+ | _ -> assert false
+ end
+ | _, _ ->
+ failwith "Could not generate cval primop"
+
+let sgen_cval_param ctx cval =
+ match cval_ctyp cval with
+ | CT_lbits direction ->
+ sgen_cval ctx cval ^ ", " ^ string_of_bool direction
+ | CT_sbits (_, direction) ->
+ sgen_cval ctx cval ^ ", " ^ string_of_bool direction
+ | CT_fbits (len, direction) ->
+ sgen_cval ctx cval ^ ", UINT64_C(" ^ string_of_int len ^ ") , " ^ string_of_bool direction
+ | _ ->
+ sgen_cval ctx cval
+
+let rec sgen_clexp ctx = function
+ | CL_id (Have_exception _, _) -> "(state->have_exception)"
+ | CL_id (Current_exception _, _) -> "(state->current_exception)"
+ | CL_id (Throw_location _, _) -> "(state->throw_location)"
+ | CL_id (Return _, _) -> assert false
+ | CL_id (Global (id, _), _) -> "&(state->" ^ sgen_id id ^ ")"
+ | CL_id (Name (id, _), _) -> "&" ^ sgen_id id
+ | CL_field (clexp, field) -> "&((" ^ sgen_clexp ctx clexp ^ ")->" ^ sgen_uid field ^ ")"
+ | CL_tuple (clexp, n) -> "&((" ^ sgen_clexp ctx clexp ^ ")->" ^ mangle ("tup" ^ string_of_int n) ^ ")"
+ | CL_addr clexp -> "(*(" ^ sgen_clexp ctx clexp ^ "))"
+ | CL_void -> assert false
+ | CL_rmw _ -> assert false
+
+let rec sgen_clexp_pure ctx = function
+ | CL_id (Have_exception _, _) -> "(state->have_exception)"
+ | CL_id (Current_exception _, _) -> "(state->current_exception)"
+ | CL_id (Throw_location _, _) -> "(state->throw_location)"
+ | CL_id (Return _, _) -> assert false
+ | CL_id (Global (id, _), _) -> "state->" ^ sgen_id id
+ | CL_id (Name (id, _), _) -> sgen_id id
+ | CL_field (clexp, field) -> sgen_clexp_pure ctx clexp ^ "." ^ sgen_uid field
+ | CL_tuple (clexp, n) -> sgen_clexp_pure ctx clexp ^ "." ^ mangle ("tup" ^ string_of_int n)
+ | CL_addr clexp -> "(*(" ^ sgen_clexp_pure ctx clexp ^ "))"
+ | CL_void -> assert false
+ | CL_rmw _ -> 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 ctx clexp cval =
+ 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 ctx clexp) (sgen_cval ctx cval)
+ else
+ ksprintf string " COPY(%s)(%s, %s);" (sgen_ctyp_name ctyp_to) (sgen_clexp ctx clexp) (sgen_cval ctx cval)
+
+ | CT_ref ctyp_to, ctyp_from ->
+ codegen_conversion l ctx (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 len = List.length ctyps_to in
+ let conversions =
+ List.mapi (fun i ctyp -> codegen_conversion l ctx (CL_tuple (clexp, i)) (V_tuple_member (cval, len, i))) 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 ctx clexp) (sgen_ctyp_name ctyp_to) (sgen_ctyp_name ctyp_from) (sgen_cval_param ctx cval)
+ | _, _ ->
+ ksprintf string " CONVERT_OF(%s, %s)(%s, %s);"
+ (sgen_ctyp_name ctyp_to) (sgen_ctyp_name ctyp_from) (sgen_clexp ctx clexp) (sgen_cval_param ctx cval)
+
+let extra_params () = "sail_state *state, "
+
+let extra_arguments is_extern =
+ if is_extern then
+ ""
+ else
+ "state, "
+
+let rec codegen_instr fid ctx (I_aux (instr, (_, l))) =
+ match instr with
+ | I_decl (ctyp, id) when is_stack_ctyp ctyp ->
+ ksprintf string " %s %s;" (sgen_ctyp ctyp) (sgen_name id)
+ | I_decl (ctyp, id) ->
+ ksprintf string " %s %s;" (sgen_ctyp ctyp) (sgen_name id) ^^ hardline
+ ^^ ksprintf string " CREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_name id)
+
+ | I_copy (clexp, cval) -> codegen_conversion l ctx clexp cval
+
+ | I_jump (cval, label) ->
+ ksprintf string " if (%s) goto %s;" (sgen_cval ctx cval) label
+
+ | I_if (cval, [then_instr], [], ctyp) ->
+ ksprintf string " if (%s)" (sgen_cval ctx cval) ^^ hardline
+ ^^ twice space ^^ codegen_instr fid ctx then_instr
+ | I_if (cval, then_instrs, [], ctyp) ->
+ string " if" ^^ space ^^ parens (string (sgen_cval ctx 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 ctx 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, special_extern, f, args) ->
+ let c_args = Util.string_of_list ", " (sgen_cval ctx) args in
+ let ctyp = clexp_ctyp x in
+ let is_extern = Env.is_extern (fst f) ctx.tc_env "c" || special_extern in
+ let fname =
+ if special_extern then
+ string_of_id (fst f)
+ else if Env.is_extern (fst f) ctx.tc_env "c" then
+ Env.get_extern (fst f) ctx.tc_env "c"
+ else
+ sgen_function_uid f
+ in
+ let fname =
+ match fname, ctyp with
+ | "internal_pick", _ -> sprintf "pick_%s" (sgen_ctyp_name ctyp)
+ | "cons", _ ->
+ begin match snd f with
+ | [ctyp] -> Util.zencode_string ("cons#" ^ string_of_ctyp ctyp)
+ | _ -> Reporting.unreachable l __POS__ "cons without specified type"
+ end
+ | "eq_anything", _ ->
+ begin match args with
+ | cval :: _ -> sprintf "eq_%s" (sgen_ctyp_name (cval_ctyp cval))
+ | _ -> Reporting.unreachable l __POS__ "eq_anything function with bad arity."
+ end
+ | "length", _ ->
+ begin match args with
+ | cval :: _ -> sprintf "length_%s" (sgen_ctyp_name (cval_ctyp cval))
+ | _ -> Reporting.unreachable l __POS__ "length function with bad arity."
+ end
+ | "vector_access", CT_bit -> "bitvector_access"
+ | "vector_access", _ ->
+ begin match args with
+ | cval :: _ -> sprintf "vector_access_%s" (sgen_ctyp_name (cval_ctyp cval))
+ | _ -> Reporting.unreachable l __POS__ "vector access function with bad arity."
+ end
+ | "vector_update_subrange", _ -> sprintf "vector_update_subrange_%s" (sgen_ctyp_name ctyp)
+ | "vector_subrange", _ -> sprintf "vector_subrange_%s" (sgen_ctyp_name ctyp)
+ | "vector_update", CT_fbits _ -> "update_fbits"
+ | "vector_update", CT_lbits _ -> "update_lbits"
+ | "vector_update", _ -> 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", _ -> sprintf "internal_vector_update_%s" (sgen_ctyp_name ctyp)
+ | "internal_vector_init", _ -> sprintf "internal_vector_init_%s" (sgen_ctyp_name ctyp)
+ | "undefined_bitvector", CT_fbits _ -> "UNDEFINED(fbits)"
+ | "undefined_bitvector", CT_lbits _ -> "UNDEFINED(lbits)"
+ | "undefined_bit", _ -> "UNDEFINED(fbits)"
+ | "undefined_vector", _ -> sprintf "UNDEFINED(vector_%s)" (sgen_ctyp_name ctyp)
+ | "undefined_list", _ -> sprintf "UNDEFINED(%s)" (sgen_ctyp_name ctyp)
+ | fname, _ -> fname
+ in
+ if fname = "reg_deref" then
+ if is_stack_ctyp ctyp then
+ ksprintf string " %s = *(%s);" (sgen_clexp_pure ctx x) c_args
+ else
+ ksprintf string " COPY(%s)(&%s, *(%s));" (sgen_ctyp_name ctyp) (sgen_clexp_pure ctx x) c_args
+ else
+ if is_stack_ctyp ctyp then
+ ksprintf string " %s = %s(%s%s);" (sgen_clexp_pure ctx x) fname (extra_arguments is_extern) c_args
+ else
+ ksprintf string " %s(%s%s, %s);" fname (extra_arguments is_extern) (sgen_clexp ctx x) c_args
+
+ | I_clear (ctyp, id) when is_stack_ctyp ctyp ->
+ empty
+ | I_clear (ctyp, id) ->
+ ksprintf string " KILL(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_name id)
+
+ | I_init (ctyp, id, cval) ->
+ codegen_instr fid ctx (idecl ctyp id) ^^ hardline
+ ^^ codegen_conversion Parse_ast.Unknown ctx (CL_id (id, ctyp)) cval
+
+ | I_reinit (ctyp, id, cval) ->
+ codegen_instr fid ctx (ireset ctyp id) ^^ hardline
+ ^^ codegen_conversion Parse_ast.Unknown ctx (CL_id (id, ctyp)) cval
+
+ | I_reset (ctyp, id) when is_stack_ctyp ctyp ->
+ ksprintf string " %s %s;" (sgen_ctyp ctyp) (sgen_name id)
+ | I_reset (ctyp, id) ->
+ ksprintf string " RECREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_name id)
+
+ | I_return cval ->
+ ksprintf string " return %s;" (sgen_cval ctx cval)
+
+ | I_throw cval ->
+ Reporting.unreachable l __POS__ "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_lint when !optimize_fixed_int -> "((sail_int) 0xdeadc0de)", [] *)
+ | CT_fbits _ -> "UINT64_C(0xdeadc0de)", []
+ | CT_sbits _ -> "undefined_sbits()", []
+ (* | CT_lbits _ when !optimize_fixed_bits -> "undefined_lbits(false)", [] *)
+ | CT_bool -> "false", []
+ | CT_enum (_, ctor :: _) -> sgen_id ctor, []
+ | CT_tup ctyps when is_stack_ctyp ctyp ->
+ let gs = ngensym () in
+ let fold (inits, prev) (n, ctyp) =
+ let init, prev' = codegen_exn_return ctyp in
+ sprintf ".%s = %s" (mangle ("tup" ^ string_of_int n)) init :: inits, prev @ prev'
+ in
+ let inits, prev = List.fold_left fold ([], []) (List.mapi (fun i x -> (i, x)) ctyps) in
+ sgen_name gs,
+ [sprintf "struct %s %s = { " (sgen_ctyp_name ctyp) (sgen_name gs)
+ ^ Util.string_of_list ", " (fun x -> x) inits ^ " };"] @ prev
+ | CT_struct (id, ctors) when is_stack_ctyp ctyp ->
+ let gs = ngensym () in
+ let fold (inits, prev) (uid, ctyp) =
+ let init, prev' = codegen_exn_return ctyp in
+ sprintf ".%s = %s" (sgen_uid uid) init :: inits, prev @ prev'
+ in
+ let inits, prev = List.fold_left fold ([], []) ctors in
+ sgen_name gs,
+ [sprintf "struct %s %s = { " (sgen_ctyp_name ctyp) (sgen_name gs)
+ ^ Util.string_of_list ", " (fun x -> x) inits ^ " };"] @ prev
+ | ctyp -> Reporting.unreachable l __POS__ ("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
+ ^^ ksprintf string " return %s;" ret
+
+ | I_comment str ->
+ string (" /* " ^ str ^ " */")
+
+ | I_label str ->
+ string (str ^ ": ;")
+
+ | I_goto str ->
+ ksprintf string " 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) ^ "\");")
+
+(**************************************************************************)
+(* Code generation for type definitions (enums, structs, and variants) *)
+(**************************************************************************)
+
+let codegen_type_def_header = function
+ | CTD_enum (id, ids) ->
+ ksprintf string "// 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
+
+ | CTD_struct (id, ctors) ->
+ let codegen_ctor (id, ctyp) =
+ string (sgen_ctyp ctyp) ^^ space ^^ codegen_uid id
+ in
+ ksprintf string "// 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
+
+ | CTD_variant (id, tus) ->
+ let codegen_tu (ctor_id, ctyp) =
+ separate space [string "struct"; lbrace; string (sgen_ctyp ctyp); codegen_uid ctor_id ^^ semi; rbrace]
+ in
+ ksprintf string "// 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_uid 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
+
+let codegen_type_def_body ctx = function
+ | CTD_enum (id, ((first_id :: _) as ids)) ->
+ let codegen_eq =
+ let name = sgen_id id in
+ string (Printf.sprintf "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
+ codegen_eq
+ ^^ twice hardline
+ ^^ codegen_undefined
+
+ | CTD_enum (id, []) -> Reporting.unreachable Parse_ast.Unknown __POS__ ("Cannot compile empty enum " ^ string_of_id id)
+
+ | CTD_struct (id, ctors) ->
+ let struct_ctyp = CT_struct (id, ctors) in
+ (* 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_uid id) (sgen_uid id))
+ else
+ string (Printf.sprintf "COPY(%s)(&rop->%s, op.%s);" (sgen_ctyp_name ctyp) (sgen_uid id) (sgen_uid 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 (UBindings.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_uid 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 (UBindings.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_uid id) (sgen_uid 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_uid id
+ in
+ 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_uid 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_uid 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_uid 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_uid ctor_id)) ^^ hardline
+ ^^ if not (is_stack_ctyp ctyp) then
+ string (Printf.sprintf "CREATE(%s)(&op->%s);" (sgen_ctyp_name ctyp) (sgen_uid 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_uid 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 = Printf.sprintf "%s op" (sgen_ctyp ctyp) in
+ string (Printf.sprintf "static void %s(%sstruct %s *rop, %s)" (sgen_function_uid ctor_id) (extra_params ()) (sgen_id id) ctor_args) ^^ hardline
+ ^^ surround 2 0 lbrace
+ (each_ctor "rop->" (clear_field "rop") tus ^^ hardline
+ ^^ string ("rop->kind = Kind_" ^ sgen_uid ctor_id) ^^ semi ^^ hardline
+ ^^ if is_stack_ctyp ctyp then
+ string (Printf.sprintf "rop->%s = op;" (sgen_uid ctor_id))
+ else
+ string (Printf.sprintf "CREATE(%s)(&rop->%s);" (sgen_ctyp_name ctyp) (sgen_uid ctor_id)) ^^ hardline
+ ^^ string (Printf.sprintf "COPY(%s)(&rop->%s, op);" (sgen_ctyp_name ctyp) (sgen_uid ctor_id)))
+ 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_uid ctor_id) (sgen_uid ctor_id))
+ else
+ string (Printf.sprintf "CREATE(%s)(&rop->%s);" (sgen_ctyp_name ctyp) (sgen_uid ctor_id))
+ ^^ string (Printf.sprintf " COPY(%s)(&rop->%s, op.%s);" (sgen_ctyp_name ctyp) (sgen_uid ctor_id) (sgen_uid 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_uid ctor_id) (sgen_uid 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_uid ctor_id) (sgen_uid 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
+ 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
+
+let codegen_type_def ctx ctype_def =
+ codegen_type_def_header ctype_def, codegen_type_def_body ctx ctype_def
+
+(**************************************************************************)
+(* Code generation for generated types (lists, tuples, etc) *)
+(**************************************************************************)
+
+(** 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, empty
+ else
+ begin
+ let _, fields = List.fold_left (fun (n, fields) ctyp -> n + 1, UBindings.add (mk_id ("tup" ^ string_of_int n), []) ctyp fields)
+ (0, UBindings.empty)
+ ctyps
+ in
+ generated := IdSet.add id !generated;
+ codegen_type_def ctx (CTD_struct (id, UBindings.bindings fields))
+ end
+
+let codegen_list_header id =
+ ksprintf string "// generated list type %s" (string_of_id id) ^^ hardline
+ ^^ ksprintf string "struct node_%s;" (sgen_id id) ^^ hardline
+ ^^ ksprintf string "typedef struct node_%s *%s;" (sgen_id id) (sgen_id id)
+ ^^ twice hardline
+
+let codegen_node id ctyp =
+ ksprintf string "struct node_%s {\n %s hd;\n struct node_%s *tl;\n};\n" (sgen_id id) (sgen_ctyp ctyp) (sgen_id id)
+ ^^ ksprintf string "typedef struct node_%s *%s;" (sgen_id id) (sgen_id id)
+
+let codegen_list_init id =
+ ksprintf string "static void CREATE(%s)(%s *rop) { *rop = NULL; }" (sgen_id id) (sgen_id id)
+
+let codegen_list_clear id ctyp =
+ ksprintf string "static void KILL(%s)(%s *rop) {\n" (sgen_id id) (sgen_id id)
+ ^^ ksprintf string " if (*rop == NULL) return;"
+ ^^ (if is_stack_ctyp ctyp then empty
+ else ksprintf string " KILL(%s)(&(*rop)->hd);\n" (sgen_ctyp_name ctyp))
+ ^^ ksprintf string " KILL(%s)(&(*rop)->tl);\n" (sgen_id id)
+ ^^ string " sail_free(*rop);"
+ ^^ string "}"
+
+let codegen_list_recreate id =
+ ksprintf string "static void RECREATE(%s)(%s *rop) { KILL(%s)(rop); *rop = NULL; }" (sgen_id id) (sgen_id id) (sgen_id id)
+
+let codegen_list_set id ctyp =
+ ksprintf string "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"
+ ^^ ksprintf string " *rop = sail_malloc(sizeof(struct node_%s));\n" (sgen_id id)
+ ^^ (if is_stack_ctyp ctyp then
+ string " (*rop)->hd = op->hd;\n"
+ else
+ ksprintf string " CREATE(%s)(&(*rop)->hd);\n" (sgen_ctyp_name ctyp)
+ ^^ ksprintf string " COPY(%s)(&(*rop)->hd, op->hd);\n" (sgen_ctyp_name ctyp))
+ ^^ ksprintf string " internal_set_%s(&(*rop)->tl, op->tl);\n" (sgen_id id)
+ ^^ string "}"
+ ^^ twice hardline
+ ^^ ksprintf string "static void COPY(%s)(%s *rop, const %s op) {\n" (sgen_id id) (sgen_id id) (sgen_id id)
+ ^^ ksprintf string " KILL(%s)(rop);\n" (sgen_id id)
+ ^^ ksprintf string " 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
+ ksprintf string "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)
+ ^^ ksprintf string " *rop = sail_malloc(sizeof(struct node_%s));\n" (sgen_id id)
+ ^^ (if is_stack_ctyp ctyp then
+ string " (*rop)->hd = x;\n"
+ else
+ ksprintf string " CREATE(%s)(&(*rop)->hd);\n" (sgen_ctyp_name ctyp)
+ ^^ ksprintf string " 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
+ ksprintf string "static %s pick_%s(const %s xs) { return xs->hd; }" (sgen_ctyp ctyp) (sgen_ctyp_name ctyp) (sgen_id id)
+ else
+ ksprintf string "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_equal id ctyp =
+ ksprintf string "static bool EQUAL(%s)(const %s op1, const %s op2) {\n" (sgen_id id) (sgen_id id) (sgen_id id)
+ ^^ ksprintf string " if (op1 == NULL && op2 == NULL) { return true; };\n"
+ ^^ ksprintf string " if (op1 == NULL || op2 == NULL) { return false; };\n"
+ ^^ ksprintf string " return EQUAL(%s)(op1->hd, op2->hd) && EQUAL(%s)(op1->tl, op2->tl);\n" (sgen_ctyp_name ctyp) (sgen_id id)
+ ^^ string "}"
+
+let codegen_list_undefined id ctyp =
+ ksprintf string "static void UNDEFINED(%s)(%s *rop, %s u) {\n" (sgen_id id) (sgen_id id) (sgen_ctyp ctyp)
+ ^^ ksprintf string " *rop = NULL;\n"
+ ^^ string "}"
+
+let codegen_list ctx ctyp =
+ let id = mk_id (string_of_ctyp (CT_list ctyp)) in
+ if IdSet.mem id !generated then (
+ (empty, empty)
+ ) else (
+ generated := IdSet.add id !generated;
+ let header = codegen_list_header id in
+ let body =
+ codegen_node id ctyp ^^ twice hardline
+ ^^ codegen_list_init id ^^ twice hardline
+ ^^ codegen_list_clear id ctyp ^^ twice hardline
+ ^^ codegen_list_recreate id ^^ twice hardline
+ ^^ codegen_list_set id ctyp ^^ twice hardline
+ ^^ codegen_cons id ctyp ^^ twice hardline
+ ^^ codegen_pick id ctyp ^^ twice hardline
+ ^^ codegen_list_equal id ctyp ^^ twice hardline
+ ^^ codegen_list_undefined id ctyp
+ in
+ (header, body)
+ )
+
+(* Generate functions for working with non-bit vectors of some specific type. *)
+let codegen_vector_header ctx id (direction, ctyp) =
+ 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
+ vector_typedef ^^ twice hardline
+
+let codegen_vector_body ctx id (direction, ctyp) =
+ 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 = sail_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) sail_free(rop->data);\n"
+ ^^ string "}"
+ in
+ let vector_update =
+ string (Printf.sprintf "static void vector_update_%s(%s *rop, %s op, sail_int n, %s elem) {\n" (sgen_id id) (sgen_id id) (sgen_id id) (sgen_ctyp ctyp))
+ ^^ string " int m = sail_int_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, sail_int n) {\n" (sgen_ctyp ctyp) (sgen_id id) (sgen_id id))
+ ^^ string " int m = sail_int_get_ui(n);\n"
+ ^^ string " return op.data[m];\n"
+ ^^ string "}"
+ else
+ string (Printf.sprintf "static void vector_access_%s(%s *rop, %s op, sail_int n) {\n" (sgen_id id) (sgen_ctyp ctyp) (sgen_id id))
+ ^^ string " int m = sail_int_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 = sail_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, sail_int len, %s elem) {\n" (sgen_id id) (sgen_id id) (sgen_ctyp ctyp))
+ ^^ string (Printf.sprintf " rop->len = sail_int_get_ui(len);\n")
+ ^^ string (Printf.sprintf " rop->data = sail_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
+ 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
+
+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, empty
+ ) else (
+ generated := IdSet.add id !generated;
+ codegen_vector_header ctx id (direction, ctyp),
+ codegen_vector_body ctx id (direction, ctyp)
+ )
+
+(**************************************************************************)
+(* Code generation for definitions *)
+(**************************************************************************)
+
+(** 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.
+
+ 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 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_name 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_name id))
+ | _ -> assert false
+
+let add_local_labels instrs =
+ match map_instrs add_local_labels' (iblock instrs) with
+ | I_aux (I_block instrs, _) -> instrs
+ | _ -> assert false
+
+let codegen_def_header ctx = function
+ | CDEF_spec (id, _, arg_ctyps, ret_ctyp) ->
+ if Env.is_extern id ctx.tc_env "c" then
+ empty
+ else if is_stack_ctyp ret_ctyp then
+ ksprintf string "%s %s(%s%s);"
+ (sgen_ctyp ret_ctyp) (sgen_function_id id) (extra_params ()) (Util.string_of_list ", " sgen_ctyp arg_ctyps)
+ ^^ twice hardline
+ else
+ ksprintf string "void %s(%s%s *rop, %s);"
+ (sgen_function_id id) (extra_params ()) (sgen_ctyp ret_ctyp) (Util.string_of_list ", " sgen_ctyp arg_ctyps)
+ ^^ twice hardline
+
+ | CDEF_type ctype_def ->
+ codegen_type_def_header ctype_def
+
+ | _ -> empty
+
+let codegen_def_body ctx = function
+ | CDEF_reg_dec _ -> empty
+
+ | CDEF_spec _ -> empty
+
+ | CDEF_fundef (id, ret_arg, args, instrs) as def ->
+ let arg_ctyps, ret_ctyp = match Bindings.find_opt id ctx.valspecs with
+ | Some vs -> vs
+ | None ->
+ Reporting.unreachable (id_loc id) __POS__ ("No valspec found for " ^ string_of_id id)
+ in
+
+ (* Check that the function has the correct arity at this point. *)
+ if List.length arg_ctyps <> List.length args then
+ Reporting.unreachable (id_loc id) __POS__
+ ("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);
+ 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));
+ 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 "}"
+ ^^ twice hardline
+
+ | CDEF_type ctype_def ->
+ codegen_type_def_body ctx ctype_def
+
+ | CDEF_startup (id, instrs) ->
+ let startup_header = string (Printf.sprintf "void startup_%s(void)" (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 finish_header = string (Printf.sprintf "void finish_%s(void)" (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 (global id)]) bindings)
+ in
+ let cleanup =
+ List.concat (List.map (fun (id, ctyp) -> [iclear ctyp (global id)]) bindings)
+ in
+ hardline ^^ string (Printf.sprintf "void sail_create_letbind_%d(sail_state *state) " 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 "void sail_kill_letbind_%d(sail_state *state) " number)
+ ^^ string "{"
+ ^^ jump 0 2 (separate_map hardline (codegen_instr (mk_id "let") ctx) cleanup) ^^ hardline
+ ^^ string "}"
+ ^^ twice hardline
+
+(** 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) | CT_fvector (_, 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 | CT_constant _ -> []
+
+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
+ Reporting.unreachable Parse_ast.Unknown __POS__
+ (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
+ let deps_header, deps_body = List.map (codegen_ctg ctx) deps |> List.split in
+ concat deps_header ^^ codegen_def_header ctx def,
+ concat deps_body ^^ codegen_def_body ctx def
+
+let codegen_state_struct_def ctx = function
+ | CDEF_reg_dec (id, ctyp, _) ->
+ ksprintf string " %s %s;" (sgen_ctyp ctyp) (sgen_id id) ^^ hardline
+
+ | CDEF_let (_, [], _) -> empty
+ | CDEF_let (_, bindings, _) ->
+ separate_map hardline (fun (id, ctyp) -> string (Printf.sprintf " %s %s;" (sgen_ctyp ctyp) (sgen_id id))) bindings
+ ^^ hardline
+
+ | _ -> empty
+
+let codegen_state_struct ctx cdefs =
+ string "struct sail_state {" ^^ hardline
+ ^^ concat_map (codegen_state_struct_def ctx) cdefs
+ ^^ (if not (Bindings.mem (mk_id "exception") ctx.variants) then (
+ empty
+ ) else (
+ string " // exception handling support" ^^ hardline
+ ^^ ksprintf string " struct %s *current_exception;" (sgen_id (mk_id "exception")) ^^ hardline
+ ^^ string " bool have_exception;" ^^ hardline
+ ^^ string " sail_string *throw_location;" ^^ hardline
+ ))
+ ^^ string "};"
+
+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 codegen_output file_name docs =
+ let chan = open_out file_name in
+ output_string chan (Pretty_print_sail.to_string docs);
+ flush chan;
+ close_out chan
+
+let codegen ctx output_name cdefs =
+ let docs_header, docs_body = List.map (codegen_def ctx) cdefs |> List.split in
+
+ let state = codegen_state_struct ctx cdefs in
+
+ let stdlib_headers =
+ string "#include <stdint.h>" ^^ hardline
+ ^^ string "#include <stdbool.h>"
+ in
+ let sail_headers =
+ string "#include \"sail.h\"" ^^ hardline
+ ^^ string "#include \"sail_failure.h\""
+ 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)(&(state->%s));" (sgen_ctyp_name ctyp) (sgen_id id) ]
+ @ List.map (sgen_instr (mk_id "reg") ctx) instrs,
+ [ Printf.sprintf " KILL(%s)(&(state->%s));" (sgen_ctyp_name ctyp) (sgen_id id) ]
+ in
+
+ let header =
+ stdlib_headers
+ ^^ hardline
+ ^^ sail_headers ^^ twice hardline
+ ^^ string "struct sail_state;" ^^ hardline
+ ^^ string "typedef struct sail_state sail_state;"
+ ^^ twice hardline
+ ^^ concat docs_header
+ ^^ state
+ ^^ twice hardline
+ ^^ string "void sail_initialize_state(sail_state *state);"
+ ^^ hardline
+ ^^ string "void sail_finalize_state(sail_state *state);"
+ ^^ hardline
+ in
+
+ let regs = c_ast_registers cdefs in
+
+ let letbind_initializers =
+ List.map (fun n -> Printf.sprintf " sail_create_letbind_%d(state);" n) (List.rev ctx.letbinds)
+ in
+ let letbind_finalizers =
+ List.map (fun n -> Printf.sprintf " sail_kill_letbind_%d(state);" n) ctx.letbinds
+ in
+
+ let body =
+ ksprintf string "#include \"%s.h\"" output_name
+ ^^ twice hardline
+ ^^ concat docs_body
+ ^^ string "void sail_initialize_letbindings(sail_state *state) {" ^^ hardline
+ ^^ separate_map hardline string letbind_initializers ^^ hardline
+ ^^ string "}"
+ ^^ twice hardline
+ ^^ string "void sail_finalize_letbindings(sail_state *state) {" ^^ hardline
+ ^^ separate_map hardline string letbind_finalizers ^^ hardline
+ ^^ string "}"
+ ^^ twice hardline
+ ^^ string "void sail_initialize_state(sail_state *state) {" ^^ hardline
+ ^^ separate_map hardline string (List.map (fun r -> fst (register_init_clear r)) regs |> List.concat)
+ ^^ (if not (Bindings.mem (mk_id "exception") ctx.variants) then (
+ empty
+ ) else (
+ string " state->have_exception = false;"
+ ^^ ksprintf string " state->current_exception = sail_malloc(sizeof(struct %s));"
+ (sgen_id (mk_id "exception")) ^^ hardline
+ ^^ ksprintf string " CREATE(%s)(state->current_exception);" (sgen_id (mk_id "exception")) ^^ hardline
+ ^^ string " state->throw_location = sail_malloc(sizeof(sail_string));" ^^ hardline
+ ^^ string " CREATE(sail_string)(state->throw_location);"
+ ))
+ ^^ hardline
+ ^^ string " sail_initialize_letbindings(state);" ^^ hardline
+ ^^ string "}"
+ ^^ twice hardline
+ ^^ string "void sail_finalize_state(sail_state *state) {" ^^ hardline
+ ^^ separate_map hardline string (List.map (fun r -> snd (register_init_clear r)) regs |> List.concat)
+ ^^ (if not (Bindings.mem (mk_id "exception") ctx.variants) then (
+ empty
+ ) else (
+ ksprintf string " KILL(%s)(state->current_exception);" (sgen_id (mk_id "exception")) ^^ hardline
+ ^^ string " sail_free(state->current_exception);" ^^ hardline
+ ^^ string " KILL(sail_string)(state->throw_location);" ^^ hardline
+ ^^ string " sail_free(state->throw_location);"
+ ))
+ ^^ hardline
+ ^^ string " sail_finalize_letbindings(state);" ^^ hardline
+ ^^ string "}"
+ ^^ hardline
+ in
+
+ codegen_output (output_name ^ ".h") header;
+ codegen_output (output_name ^ ".c") body
+
+let emulator ctx output_name cdefs =
+ codegen ctx output_name cdefs;
+
+ let preamble = separate hardline
+ ((if !opt_no_lib then [] else
+ [ string "#include \"sail.h\"";
+ string "#include \"sail_failure.h\"" ])
+ @ (if !opt_no_rts then [] else
+ [ string "#include \"rts.h\"";
+ string "#include \"elf.h\"" ])
+ @ [ ksprintf string "#include \"%s.h\"" output_name ]
+ @ (List.map (fun h -> string (Printf.sprintf "#include \"%s\"" h)) [] (*c_includes*)))
+ 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 model_init = separate hardline (List.map string
+ ( [ "void model_init(sail_state *state)";
+ "{";
+ " sail_initialize_state(state);";
+ " setup_rts();" ]
+ @ startup cdefs
+ @ (if regs = [] then [] else [ Printf.sprintf " %s(state, UNIT);" (sgen_function_id (mk_id "initialize_registers")) ])
+ @ [ "}" ] ))
+ in
+
+ let model_fini = separate hardline (List.map string
+ ( [ "void model_fini(sail_state *state)";
+ "{" ]
+ @ finish cdefs
+ @ [ " cleanup_rts();";
+ " sail_finalize_state(state);";
+ "}" ]))
+ in
+
+ let model_default_main = separate hardline (List.map string
+ ([ "int model_main(int argc, char *argv[])";
+ "{";
+ " sail_state state;";
+ " model_init(&state);";
+ " if (process_arguments(argc, argv)) exit(EXIT_FAILURE);";
+ sprintf " %s(&state, UNIT);" (sgen_function_id (mk_id "main")) ]
+ @ (if not (Bindings.mem (mk_id "exception") ctx.variants) then [] else
+ [ " if (state.have_exception) {fprintf(stderr, \"Exiting due to uncaught exception: %s\\n\", *state.throw_location);}" ])
+ @ [ " model_fini(&state);" ]
+ @ (if not (Bindings.mem (mk_id "exception") ctx.variants) then [] else
+ [ " if (state.have_exception) {return(EXIT_FAILURE);}" ])
+ @ [ " 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
+ let emu =
+ preamble ^^ hlhl
+ ^^ (if not !opt_no_rts then
+ model_init ^^ hlhl
+ ^^ model_fini ^^ hlhl
+ ^^ model_default_main ^^ hlhl
+ else
+ empty)
+ ^^ model_main ^^ hardline
+ in
+ codegen_output (output_name ^ "_emu.c") emu
+
+end
diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml
index 34477967..1cd7d82a 100644
--- a/src/jib/jib_compile.ml
+++ b/src/jib/jib_compile.ml
@@ -190,6 +190,12 @@ let rec chunkify n xs =
| xs, [] -> [xs]
| xs, ys -> xs :: chunkify n ys
+let name_or_global ctx id =
+ if Env.is_register id ctx.local_env || IdSet.mem id (Env.get_toplevel_lets ctx.local_env) then
+ global id
+ else
+ name id
+
let rec compile_aval l ctx = function
| AV_cval (cval, typ) ->
let ctyp = cval_ctyp cval in
@@ -201,13 +207,11 @@ let rec compile_aval l ctx = function
[], cval, []
| AV_id (id, typ) ->
- begin
- try
- let _, ctyp = Bindings.find id ctx.locals in
- [], V_id (name id, ctyp), []
- with
- | Not_found ->
- [], V_id (name id, ctyp_of_typ ctx (lvar_typ typ)), []
+ begin match Bindings.find_opt id ctx.locals with
+ | Some (_, ctyp) ->
+ [], V_id (name id, ctyp), []
+ | None ->
+ [], V_id (name_or_global ctx id, ctyp_of_typ ctx (lvar_typ typ)), []
end
| AV_ref (id, typ) ->
@@ -520,7 +524,7 @@ let rec compile_match ctx (AP_aux (apat_aux, env, l)) cval case_label =
| AP_global (pid, typ) ->
let global_ctyp = ctyp_of_typ ctx typ in
- [icopy l (CL_id (name pid, global_ctyp)) cval], [], ctx
+ [icopy l (CL_id (global pid, global_ctyp)) cval], [], ctx
| AP_id (pid, _) when is_ct_enum ctyp ->
begin match Env.lookup_id pid ctx.tc_env with
@@ -778,7 +782,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
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 (name id, ctyp_of_typ ctx typ), (field_id, []))) cval]
+ @ [icopy l (CL_field (CL_id (name_or_global ctx id, ctyp_of_typ ctx typ), (field_id, []))) cval]
@ field_cleanup
in
List.concat (List.map compile_fields (Bindings.bindings fields)),
@@ -792,7 +796,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
| None -> ctyp_of_typ ctx assign_typ
in
let setup, call, cleanup = compile_aexp ctx aexp in
- setup @ [call (CL_id (name id, assign_ctyp))], (fun clexp -> icopy l clexp unit_cval), cleanup
+ setup @ [call (CL_id (name_or_global ctx id, assign_ctyp))], (fun clexp -> icopy l clexp unit_cval), cleanup
| AE_write_ref (id, assign_typ, aexp) ->
let assign_ctyp =
@@ -801,7 +805,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
| None -> ctyp_of_typ ctx assign_typ
in
let setup, call, cleanup = compile_aexp ctx aexp in
- setup @ [call (CL_addr (CL_id (name id, assign_ctyp)))], (fun clexp -> icopy l clexp unit_cval), cleanup
+ setup @ [call (CL_addr (CL_id (name_or_global ctx id, assign_ctyp)))], (fun clexp -> icopy l clexp unit_cval), cleanup
| AE_block (aexps, aexp, _) ->
let block = compile_block ctx aexps in
@@ -1302,7 +1306,7 @@ and compile_def' n total ctx = function
| DEF_reg_dec (DEC_aux (DEC_config (id, typ, exp), _)) ->
let aexp = C.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 (name id, ctyp_of_typ ctx typ))] @ cleanup in
+ let instrs = setup @ [call (CL_id (global 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, _))) ->
diff --git a/src/jib/jib_compile.mli b/src/jib/jib_compile.mli
index 9014d8f7..a642f29e 100644
--- a/src/jib/jib_compile.mli
+++ b/src/jib/jib_compile.mli
@@ -65,7 +65,16 @@ val optimize_aarch64_fast_struct : bool ref
useful for debugging C but we want to turn it off for SMT generation
where we can't use strings *)
val opt_track_throw : bool 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
+ the Sail version. This cache can obviously become stale if the Sail
+ changes - it'll load an old version compiled without said
+ changes. *)
+val opt_memo_cache : bool ref
+
(** {2 Jib context} *)
(** Dynamic context for compiling Sail to Jib. We need to pass a
diff --git a/src/jib/jib_ir.ml b/src/jib/jib_ir.ml
index 4bf726aa..d30fe183 100644
--- a/src/jib/jib_ir.ml
+++ b/src/jib/jib_ir.ml
@@ -62,7 +62,7 @@ module StringMap = Map.Make(String)
let string_of_name =
let ssa_num n = if n = -1 then "" else ("/" ^ string_of_int n) in
function
- | Name (id, n) -> zencode_id id ^ ssa_num n
+ | Name (id, n) | Global (id, n) -> zencode_id id ^ ssa_num n
| Have_exception n ->
"have_exception" ^ ssa_num n
| Return n ->
diff --git a/src/jib/jib_optimize.ml b/src/jib/jib_optimize.ml
index e0f3bf0d..f156a040 100644
--- a/src/jib/jib_optimize.ml
+++ b/src/jib/jib_optimize.ml
@@ -76,6 +76,7 @@ let optimize_unit instrs =
in
let non_pointless_copy (I_aux (aux, annot)) =
match aux with
+ | I_decl (CT_unit, _) -> false
| I_copy (CL_void, _) -> false
| _ -> true
in
@@ -245,6 +246,7 @@ let rec find_function fid = function
let ssa_name i = function
| Name (id, _) -> Name (id, i)
+ | Global (id, _) -> Global (id, i)
| Have_exception _ -> Have_exception i
| Current_exception _ -> Current_exception i
| Throw_location _ -> Throw_location i
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 47f6ee49..b662ef41 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -343,7 +343,7 @@ let rec smt_cval ctx cval =
| _ ->
match cval with
| V_lit (vl, ctyp) -> smt_value ctx vl ctyp
- | V_id (Name (id, _) as ssa_id, _) ->
+ | V_id ((Name (id, _) | Global (id, _)) as ssa_id, _) ->
begin match Type_check.Env.lookup_id id ctx.tc_env with
| Enum _ -> Enum (zencode_id id)
| _ when Bindings.mem id ctx.shared -> Shared (zencode_id id)
@@ -1384,8 +1384,8 @@ let rec generate_ctype_defs ctx = function
| [] -> []
let rec generate_reg_decs ctx inits = function
- | CDEF_reg_dec (id, ctyp, _) :: cdefs when not (NameMap.mem (Name (id, 0)) inits)->
- Declare_const (zencode_name (Name (id, 0)), smt_ctyp ctx ctyp)
+ | CDEF_reg_dec (id, ctyp, _) :: cdefs when not (NameMap.mem (Global (id, 0)) inits)->
+ Declare_const (zencode_name (Global (id, 0)), smt_ctyp ctx ctyp)
:: generate_reg_decs ctx inits cdefs
| _ :: cdefs -> generate_reg_decs ctx inits cdefs
| [] -> []
@@ -1876,7 +1876,7 @@ let smt_instr ctx =
| I_aux (I_init (ctyp, id, cval), _) | I_aux (I_copy (CL_id (id, ctyp), cval), _) ->
begin match id with
- | Name (id, _) when IdSet.mem id ctx.preserved ->
+ | Name (id, _) | Global (id, _) when IdSet.mem id ctx.preserved ->
[preserve_const ctx id ctyp
(smt_conversion ctx (cval_ctyp cval) ctyp (smt_cval ctx cval))]
| _ ->
@@ -1935,7 +1935,7 @@ let rec find_function lets id = function
| CDEF_fundef (id', heap_return, args, body) :: _ when Id.compare id id' = 0 ->
lets, Some (heap_return, args, body)
| CDEF_let (_, vars, setup) :: cdefs ->
- let vars = List.map (fun (id, ctyp) -> idecl ctyp (name id)) vars in
+ let vars = List.map (fun (id, ctyp) -> idecl ctyp (global id)) vars in
find_function (lets @ vars @ setup) id cdefs;
| _ :: cdefs ->
find_function lets id cdefs
@@ -2121,7 +2121,7 @@ let expand_reg_deref env register_map = function
let try_reg r =
let next_label = label "next_reg_write_" in
[ijump l (V_call (Neq, [V_lit (VL_ref (string_of_id r), reg_ctyp); V_id (id, ctyp)])) next_label;
- ifuncall (CL_id (name r, reg_ctyp)) function_id args;
+ ifuncall (CL_id (global r, reg_ctyp)) function_id args;
igoto end_label;
ilabel next_label]
in
@@ -2145,7 +2145,7 @@ let expand_reg_deref env register_map = function
let try_reg r =
let next_label = label "next_reg_deref_" in
[ijump l (V_call (Neq, [V_lit (VL_ref (string_of_id r), reg_ctyp); reg_ref])) next_label;
- icopy l clexp (V_id (name r, reg_ctyp));
+ icopy l clexp (V_id (global r, reg_ctyp));
igoto end_label;
ilabel next_label]
in
@@ -2167,7 +2167,7 @@ let expand_reg_deref env register_map = function
let try_reg r =
let next_label = label "next_reg_write_" in
[ijump l (V_call (Neq, [V_lit (VL_ref (string_of_id r), reg_ctyp); V_id (id, ctyp)])) next_label;
- icopy l (CL_id (name r, reg_ctyp)) cval;
+ icopy l (CL_id (global r, reg_ctyp)) cval;
igoto end_label;
ilabel next_label]
in
@@ -2301,7 +2301,7 @@ let smt_cdef props lets name_file ctx all_cdefs = function
let rec smt_cdefs props lets name_file ctx ast =
function
| CDEF_let (_, vars, setup) :: cdefs ->
- let vars = List.map (fun (id, ctyp) -> idecl ctyp (name id)) vars in
+ let vars = List.map (fun (id, ctyp) -> idecl ctyp (global id)) vars in
smt_cdefs props (lets @ vars @ setup) name_file ctx ast cdefs;
| cdef :: cdefs ->
smt_cdef props lets name_file ctx ast cdef;
diff --git a/src/jib/jib_ssa.ml b/src/jib/jib_ssa.ml
index fe3238a4..f9777f9e 100644
--- a/src/jib/jib_ssa.ml
+++ b/src/jib/jib_ssa.ml
@@ -502,6 +502,7 @@ let rename_variables graph root children =
let ssa_name i = function
| Name (id, _) -> Name (id, i)
+ | Global (id, _) -> Global (id, i)
| Have_exception _ -> Have_exception i
| Current_exception _ -> Current_exception i
| Throw_location _ -> Throw_location i
diff --git a/src/jib/jib_util.ml b/src/jib/jib_util.ml
index 9b06c7be..88f09bcf 100644
--- a/src/jib/jib_util.ml
+++ b/src/jib/jib_util.ml
@@ -144,11 +144,16 @@ module Name = struct
| Name (x, n), Name (y, m) ->
let c1 = Id.compare x y in
if c1 = 0 then compare n m else c1
+ | Global (x, n), Global (y, m) ->
+ let c1 = Id.compare x y in
+ if c1 = 0 then compare n m else c1
| Have_exception n, Have_exception m -> compare n m
| Current_exception n, Current_exception m -> compare n m
| Return n, Return m -> compare n m
| Name _, _ -> 1
| _, Name _ -> -1
+ | Global _, _ -> 1
+ | _, Global _ -> -1
| Have_exception _, _ -> 1
| _, Have_exception _ -> -1
| Current_exception _, _ -> 1
@@ -166,6 +171,7 @@ let throw_location = Throw_location (-1)
let return = Return (-1)
let name id = Name (id, -1)
+let global id = Global (id, -1)
let rec cval_rename from_id to_id = function
| V_id (id, ctyp) when Name.compare id from_id = 0 -> V_id (to_id, ctyp)
@@ -261,7 +267,7 @@ let rec instr_rename from_id to_id (I_aux (instr, aux)) =
let string_of_name ?deref_current_exception:(dce=false) ?zencode:(zencode=true) =
let ssa_num n = if n = -1 then "" else ("/" ^ string_of_int n) in
function
- | Name (id, n) ->
+ | Name (id, n) | Global (id, n) ->
(if zencode then Util.zencode_string (string_of_id id) else string_of_id id) ^ ssa_num n
| Have_exception n ->
"have_exception" ^ ssa_num n
diff --git a/src/rewrites.ml b/src/rewrites.ml
index e622d620..89f67d87 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -5059,6 +5059,7 @@ let rewrites_target tgt =
| "lem" -> rewrites_lem
| "ocaml" -> rewrites_ocaml
| "c" -> rewrites_c
+ | "c2" -> rewrites_c
| "ir" -> rewrites_c @ [("properties", [])]
| "smt" -> rewrites_c @ [("properties", [])]
| "sail" -> []
diff --git a/src/sail.ml b/src/sail.ml
index 64e4f8c6..296bfdac 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -185,6 +185,9 @@ let options = Arg.align ([
( "-c",
Arg.Tuple [set_target "c"; Arg.Set Initial_check.opt_undefined_gen],
" output a C translated version of the input");
+ ( "-c2",
+ Arg.Tuple [set_target "c2"; Arg.Set Initial_check.opt_undefined_gen],
+ " output a C translated version of the input");
( "-c_include",
Arg.String (fun i -> opt_includes_c := i::!opt_includes_c),
"<filename> provide additional include for C output");
@@ -304,7 +307,7 @@ let options = Arg.align ([
Arg.Clear opt_memo_z3,
" do not memoize calls to z3 (default)");
( "-memo",
- Arg.Tuple [Arg.Set opt_memo_z3; Arg.Set C_backend.opt_memo_cache],
+ Arg.Tuple [Arg.Set opt_memo_z3; Arg.Set Jib_compile.opt_memo_cache],
" memoize calls to z3, and intermediate compilation results");
( "-have_feature",
Arg.String (fun symbol -> opt_have_feature := Some symbol),
@@ -474,6 +477,27 @@ let target name out_name ast type_envs =
flush output_chan;
if close then close_out output_chan else ()
+ | Some "c2" ->
+ let module StringMap = Map.Make(String) in
+ let ast_c, type_envs = Specialize.(specialize typ_ord_specialization type_envs ast) in
+ let ast_c, type_envs =
+ if !opt_specialize_c then
+ Specialize.(specialize_passes 2 int_specialization type_envs ast_c)
+ else
+ ast_c, type_envs
+ in
+ let output_name = match !opt_file_out with Some f -> f | None -> "out" in
+ Reporting.opt_warnings := true;
+ let codegen ctx cdefs =
+ let module Codegen =
+ C_codegen.Make(
+ struct let opts = C_codegen.default_options cdefs end
+ )
+ in
+ Codegen.emulator ctx output_name cdefs
+ in
+ C_backend.compile_ast_clib type_envs ast_c codegen;
+
| Some "ir" ->
let ast_c, type_envs = Specialize.(specialize typ_ord_specialization type_envs ast) in
(* let ast_c, type_envs = Specialize.(specialize' 2 int_specialization_with_externs ast_c type_envs) in *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 10:21:06 +0000