summaryrefslogtreecommitdiff
path: root/src/jib/c_backend.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/jib/c_backend.ml')
-rw-r--r--src/jib/c_backend.ml181
1 files changed, 144 insertions, 37 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 08:53:21 +0000