summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/jib/c_backend.ml798
-rw-r--r--src/jib/c_backend.mli3
-rw-r--r--src/jib/jib_compile.ml81
-rw-r--r--src/jib/jib_compile.mli75
-rw-r--r--src/jib/jib_ir.ml6
-rw-r--r--src/jib/jib_optimize.ml2
-rw-r--r--src/jib/jib_smt.ml291
-rw-r--r--src/jib/jib_smt_fuzz.ml2
-rw-r--r--src/jib/jib_util.ml17
-rw-r--r--src/value2.lem1
10 files changed, 652 insertions, 624 deletions
diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml
index ae6afc0c..fc0259e9 100644
--- a/src/jib/c_backend.ml
+++ b/src/jib/c_backend.ml
@@ -101,6 +101,8 @@ let zencode_uid (id, ctyps) =
| [] -> 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
+
(**************************************************************************)
(* 2. Converting sail types to C types *)
(**************************************************************************)
@@ -108,90 +110,9 @@ let zencode_uid (id, ctyps) =
let max_int n = Big_int.pred (Big_int.pow_int_positive 2 (n - 1))
let min_int n = Big_int.negate (Big_int.pow_int_positive 2 (n - 1))
-(** Convert a sail type into a C-type. This function can be quite
- slow, because it uses ctx.local_env and SMT to analyse the Sail
- types and attempts to fit them into the smallest possible C
- types, provided ctx.optimize_smt is true (default) **)
-let rec ctyp_of_typ ctx typ =
- let Typ_aux (typ_aux, l) as typ = Env.expand_synonyms ctx.tc_env typ in
- match typ_aux with
- | Typ_id id when string_of_id id = "bit" -> CT_bit
- | Typ_id id when string_of_id id = "bool" -> CT_bool
- | Typ_id id when string_of_id id = "int" -> CT_lint
- | Typ_id id when string_of_id id = "nat" -> CT_lint
- | Typ_id id when string_of_id id = "unit" -> CT_unit
- | Typ_id id when string_of_id id = "string" -> CT_string
- | Typ_id id when string_of_id id = "real" -> CT_real
-
- | Typ_app (id, _) when string_of_id id = "atom_bool" -> CT_bool
-
- | Typ_app (id, args) when string_of_id id = "itself" ->
- ctyp_of_typ ctx (Typ_aux (Typ_app (mk_id "atom", args), l))
- | Typ_app (id, _) when string_of_id id = "range" || string_of_id id = "atom" || string_of_id id = "implicit" ->
- begin match destruct_range Env.empty typ with
- | None -> assert false (* Checked if range type in guard *)
- | Some (kids, constr, n, m) ->
- let ctx = { ctx with local_env = add_existential Parse_ast.Unknown (List.map (mk_kopt K_int) kids) constr ctx.local_env }in
- match nexp_simp n, nexp_simp m with
- | Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_constant m, _)
- when Big_int.less_equal (min_int 64) n && Big_int.less_equal m (max_int 64) ->
- CT_fint 64
- | n, m ->
- if prove __POS__ ctx.local_env (nc_lteq (nconstant (min_int 64)) n) && prove __POS__ ctx.local_env (nc_lteq m (nconstant (max_int 64))) then
- CT_fint 64
- else
- CT_lint
- end
-
- | Typ_app (id, [A_aux (A_typ typ, _)]) when string_of_id id = "list" ->
- CT_list (ctyp_of_typ ctx typ)
-
- (* When converting a sail bitvector type into C, we have three options in order of efficiency:
- - If the length is obviously static and smaller than 64, use the fixed bits type (aka uint64_t), fbits.
- - If the length is less than 64, then use a small bits type, sbits.
- - If the length may be larger than 64, use a large bits type lbits. *)
- | Typ_app (id, [A_aux (A_nexp n, _);
- A_aux (A_order ord, _)])
- 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)
- | n when prove __POS__ ctx.local_env (nc_lteq n (nint 64)) -> CT_sbits (64, direction)
- | _ -> CT_lbits direction
- end
-
- | Typ_app (id, [A_aux (A_nexp n, _);
- A_aux (A_order ord, _);
- A_aux (A_typ typ, _)])
- when string_of_id id = "vector" ->
- let direction = match ord with Ord_aux (Ord_dec, _) -> true | Ord_aux (Ord_inc, _) -> false | _ -> assert false in
- CT_vector (direction, ctyp_of_typ ctx typ)
-
- | Typ_app (id, [A_aux (A_typ typ, _)]) when string_of_id id = "register" ->
- CT_ref (ctyp_of_typ ctx typ)
-
- | Typ_id id | Typ_app (id, _) when Bindings.mem id ctx.records -> CT_struct (id, Bindings.find id ctx.records |> 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 (ctyp_of_typ ctx) typs)
-
- | Typ_exist _ ->
- (* Use Type_check.destruct_exist when optimising with SMT, to
- ensure that we don't cause any type variable clashes in
- local_env, and that we can optimize the existential based upon
- it's constraints. *)
- begin match destruct_exist (Env.expand_synonyms ctx.local_env typ) with
- | Some (kids, nc, typ) ->
- let env = add_existential l kids nc ctx.local_env in
- ctyp_of_typ { ctx with local_env = env } typ
- | None -> raise (Reporting.err_unreachable l __POS__ "Existential cannot be destructured!")
- end
-
- | Typ_var kid -> CT_poly
-
- | _ -> c_error ~loc:l ("No C type for type " ^ string_of_typ typ)
-
+(** 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
@@ -207,346 +128,442 @@ let rec is_stack_ctyp ctyp = match ctyp with
| CT_poly -> true
| CT_constant n -> Big_int.less_equal (min_int 64) n && Big_int.greater_equal n (max_int 64)
-let is_stack_typ ctx typ = is_stack_ctyp (ctyp_of_typ ctx typ)
-
-let is_fbits_typ ctx typ =
- match ctyp_of_typ ctx typ with
- | CT_fbits _ -> true
- | _ -> false
-
-let is_sbits_typ ctx typ =
- match ctyp_of_typ ctx typ with
- | CT_sbits _ -> true
- | _ -> false
-
-let ctor_bindings = List.fold_left (fun map (id, ctyp) -> UBindings.add id ctyp map) UBindings.empty
-
-(**************************************************************************)
-(* 3. Optimization of primitives and literals *)
-(**************************************************************************)
-
-let hex_char =
- let open Sail2_values in
- function
- | '0' -> [B0; B0; B0; B0]
- | '1' -> [B0; B0; B0; B1]
- | '2' -> [B0; B0; B1; B0]
- | '3' -> [B0; B0; B1; B1]
- | '4' -> [B0; B1; B0; B0]
- | '5' -> [B0; B1; B0; B1]
- | '6' -> [B0; B1; B1; B0]
- | '7' -> [B0; B1; B1; B1]
- | '8' -> [B1; B0; B0; B0]
- | '9' -> [B1; B0; B0; B1]
- | 'A' | 'a' -> [B1; B0; B1; B0]
- | 'B' | 'b' -> [B1; B0; B1; B1]
- | 'C' | 'c' -> [B1; B1; B0; B0]
- | 'D' | 'd' -> [B1; B1; B0; B1]
- | 'E' | 'e' -> [B1; B1; B1; B0]
- | 'F' | 'f' -> [B1; B1; B1; B1]
- | _ -> failwith "Invalid hex character"
-
-let literal_to_fragment (L_aux (l_aux, _) as lit) =
- match l_aux with
- | L_num n when Big_int.less_equal (min_int 64) n && Big_int.less_equal n (max_int 64) ->
- Some (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 (ctyp_of_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 rec is_bitvector = function
- | [] -> true
- | AV_lit (L_aux (L_zero, _), _) :: avals -> is_bitvector avals
- | AV_lit (L_aux (L_one, _), _) :: avals -> is_bitvector avals
- | _ :: _ -> false
-
-let rec value_of_aval_bit = function
- | AV_lit (L_aux (L_zero, _), _) -> Sail2_values.B0
- | AV_lit (L_aux (L_one, _), _) -> Sail2_values.B1
- | _ -> assert false
-
-(** Used to make sure the -Ofixed_int and -Ofixed_bits don't interfere
- with assumptions made about optimizations in the common case. *)
-let rec never_optimize = function
- | CT_lbits _ | CT_lint -> true
- | _ -> false
-
-let rec c_aval ctx = function
- | AV_lit (lit, typ) as v ->
- begin
- match literal_to_fragment lit with
- | Some cval -> AV_cval (cval, typ)
- | None -> v
- end
- | AV_cval (cval, typ) -> AV_cval (cval, typ)
- (* An id can be converted to a C fragment if it's type can be
- stack-allocated. *)
- | AV_id (id, lvar) as v ->
- begin
- match lvar with
- | Local (_, typ) ->
- let ctyp = ctyp_of_typ ctx typ in
- if is_stack_ctyp ctyp && not (never_optimize ctyp) then
- begin
- try
- (* We need to check that id's type hasn't changed due to flow typing *)
- let _, ctyp' = Bindings.find id ctx.locals in
- if ctyp_equal ctyp ctyp' then
- AV_cval (V_id (name id, ctyp), typ)
- else
- (* id's type changed due to flow
- typing, so it's really still heap allocated! *)
- v
- with
- (* Hack: Assuming global letbindings don't change from flow typing... *)
- Not_found -> AV_cval (V_id (name id, ctyp), typ)
- end
- else
- v
- | Register (_, _, typ) ->
- let ctyp = ctyp_of_typ ctx typ in
- if is_stack_ctyp ctyp && not (never_optimize ctyp) then
- AV_cval (V_id (name id, ctyp), typ)
- else
- v
- | _ -> v
- end
- | AV_vector (v, typ) when is_bitvector v && List.length v <= 64 ->
- let bitstring = VL_bits (List.map value_of_aval_bit v, true) in
- AV_cval (V_lit (bitstring, CT_fbits (List.length v, true)), typ)
- | AV_tuple avals -> AV_tuple (List.map (c_aval ctx) avals)
- | aval -> aval
-
-let c_fragment = function
- | AV_cval (cval, _) -> cval
- | _ -> assert false
-
let v_mask_lower i = V_lit (VL_bits (Util.list_init i (fun _ -> Sail2_values.B1), true), CT_fbits (i, true))
-(* Map over all the functions in an aexp. *)
-let rec analyze_functions ctx f (AE_aux (aexp, env, l)) =
- let ctx = { ctx with local_env = env } in
- let aexp = match aexp with
- | AE_app (id, vs, typ) -> f ctx id vs typ
+module C_config : Config = struct
- | AE_cast (aexp, typ) -> AE_cast (analyze_functions ctx f aexp, typ)
+(** Convert a sail type into a C-type. This function can be quite
+ slow, because it uses ctx.local_env and SMT to analyse the Sail
+ types and attempts to fit them into the smallest possible C
+ types, provided ctx.optimize_smt is true (default) **)
+ let rec 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, args) when string_of_id id = "itself" ->
+ convert_typ ctx (Typ_aux (Typ_app (mk_id "atom", args), l))
+ | Typ_app (id, _) when string_of_id id = "range" || string_of_id id = "atom" || string_of_id id = "implicit" ->
+ begin match destruct_range Env.empty typ with
+ | None -> assert false (* Checked if range type in guard *)
+ | Some (kids, constr, n, m) ->
+ let ctx = { ctx with local_env = add_existential Parse_ast.Unknown (List.map (mk_kopt K_int) kids) constr ctx.local_env }in
+ match nexp_simp n, nexp_simp m with
+ | Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_constant m, _)
+ when Big_int.less_equal (min_int 64) n && Big_int.less_equal m (max_int 64) ->
+ CT_fint 64
+ | n, m ->
+ if prove __POS__ ctx.local_env (nc_lteq (nconstant (min_int 64)) n) && prove __POS__ ctx.local_env (nc_lteq m (nconstant (max_int 64))) then
+ CT_fint 64
+ else
+ CT_lint
+ end
- | AE_assign (id, typ, aexp) -> AE_assign (id, typ, analyze_functions ctx f aexp)
+ | Typ_app (id, [A_aux (A_typ typ, _)]) when string_of_id id = "list" ->
+ CT_list (convert_typ ctx typ)
+
+ (* When converting a sail bitvector type into C, we have three options in order of efficiency:
+ - If the length is obviously static and smaller than 64, use the fixed bits type (aka uint64_t), fbits.
+ - If the length is less than 64, then use a small bits type, sbits.
+ - If the length may be larger than 64, use a large bits type lbits. *)
+ | Typ_app (id, [A_aux (A_nexp n, _);
+ A_aux (A_order ord, _)])
+ 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)
+ | n when prove __POS__ ctx.local_env (nc_lteq n (nint 64)) -> CT_sbits (64, direction)
+ | _ -> CT_lbits direction
+ end
- | AE_write_ref (id, typ, aexp) -> AE_write_ref (id, typ, analyze_functions ctx f aexp)
+ | 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 _ ->
+ (* Use Type_check.destruct_exist when optimising with SMT, to
+ ensure that we don't cause any type variable clashes in
+ local_env, and that we can optimize the existential based
+ upon it's constraints. *)
+ begin match destruct_exist (Env.expand_synonyms ctx.local_env typ) with
+ | Some (kids, nc, typ) ->
+ let env = add_existential l kids nc ctx.local_env in
+ convert_typ { ctx with local_env = env } typ
+ | None -> raise (Reporting.err_unreachable l __POS__ "Existential cannot be destructured!")
+ end
- | AE_short_circuit (op, aval, aexp) -> AE_short_circuit (op, aval, analyze_functions ctx f aexp)
+ | Typ_var kid -> CT_poly
- | AE_let (mut, id, typ1, aexp1, (AE_aux (_, env2, _) as aexp2), typ2) ->
- let aexp1 = analyze_functions ctx f aexp1 in
- (* Use aexp2's environment because it will contain constraints for id *)
- let ctyp1 = ctyp_of_typ { ctx with local_env = env2 } typ1 in
- let ctx = { ctx with locals = Bindings.add id (mut, ctyp1) ctx.locals } in
- AE_let (mut, id, typ1, aexp1, analyze_functions ctx f aexp2, typ2)
+ | _ -> c_error ~loc:l ("No C type for type " ^ string_of_typ typ)
- | AE_block (aexps, aexp, typ) -> AE_block (List.map (analyze_functions ctx f) aexps, analyze_functions ctx f aexp, typ)
+ let is_stack_typ ctx typ = is_stack_ctyp (convert_typ ctx typ)
- | AE_if (aval, aexp1, aexp2, typ) ->
- AE_if (aval, analyze_functions ctx f aexp1, analyze_functions ctx f aexp2, typ)
+ let is_fbits_typ ctx typ =
+ match convert_typ ctx typ with
+ | CT_fbits _ -> true
+ | _ -> false
- | AE_loop (loop_typ, aexp1, aexp2) -> AE_loop (loop_typ, analyze_functions ctx f aexp1, analyze_functions ctx f aexp2)
+ let is_sbits_typ ctx typ =
+ match convert_typ ctx typ with
+ | CT_sbits _ -> true
+ | _ -> false
- | AE_for (id, aexp1, aexp2, aexp3, order, aexp4) ->
- let aexp1 = analyze_functions ctx f aexp1 in
- let aexp2 = analyze_functions ctx f aexp2 in
- let aexp3 = analyze_functions ctx f aexp3 in
- let aexp4 = analyze_functions ctx f aexp4 in
- (* Currently we assume that loop indexes are always safe to put into an int64 *)
- let ctx = { ctx with locals = Bindings.add id (Immutable, CT_fint 64) ctx.locals } in
- AE_for (id, aexp1, aexp2, aexp3, order, aexp4)
+ (**************************************************************************)
+ (* 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) ->
+ 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 rec is_bitvector = function
+ | [] -> true
+ | AV_lit (L_aux (L_zero, _), _) :: avals -> is_bitvector avals
+ | AV_lit (L_aux (L_one, _), _) :: avals -> is_bitvector avals
+ | _ :: _ -> false
+
+ let rec value_of_aval_bit = function
+ | AV_lit (L_aux (L_zero, _), _) -> Sail2_values.B0
+ | AV_lit (L_aux (L_one, _), _) -> Sail2_values.B1
+ | _ -> assert false
+
+ (** Used to make sure the -Ofixed_int and -Ofixed_bits don't
+ interfere with assumptions made about optimizations in the common
+ case. *)
+ let rec never_optimize = function
+ | CT_lbits _ | CT_lint -> true
+ | _ -> false
- | AE_case (aval, cases, typ) ->
- let analyze_case (AP_aux (_, env, _) as pat, aexp1, aexp2) =
- let pat_bindings = Bindings.bindings (apat_types pat) in
- let ctx = { ctx with local_env = env } in
- let ctx =
- List.fold_left (fun ctx (id, typ) -> { ctx with locals = Bindings.add id (Immutable, ctyp_of_typ ctx typ) ctx.locals }) ctx pat_bindings
+ let rec c_aval ctx = function
+ | AV_lit (lit, typ) as v ->
+ begin
+ match literal_to_fragment lit with
+ | Some cval -> AV_cval (cval, typ)
+ | None -> v
+ end
+ | AV_cval (cval, typ) -> AV_cval (cval, typ)
+ (* An id can be converted to a C fragment if it's type can be
+ stack-allocated. *)
+ | AV_id (id, lvar) as v ->
+ begin
+ match lvar with
+ | Local (_, typ) ->
+ let ctyp = convert_typ ctx typ in
+ if is_stack_ctyp ctyp && not (never_optimize ctyp) then
+ begin
+ try
+ (* We need to check that id's type hasn't changed due to flow typing *)
+ let _, ctyp' = Bindings.find id ctx.locals in
+ if ctyp_equal ctyp ctyp' then
+ AV_cval (V_id (name id, ctyp), typ)
+ else
+ (* id's type changed due to flow typing, so it's
+ really still heap allocated! *)
+ v
+ with
+ (* Hack: Assuming global letbindings don't change from flow typing... *)
+ Not_found -> AV_cval (V_id (name id, ctyp), typ)
+ end
+ else
+ v
+ | Register (_, _, typ) ->
+ let ctyp = convert_typ ctx typ in
+ if is_stack_ctyp ctyp && not (never_optimize ctyp) then
+ AV_cval (V_id (name id, ctyp), typ)
+ else
+ v
+ | _ -> v
+ end
+ | AV_vector (v, typ) when is_bitvector v && List.length v <= 64 ->
+ let bitstring = VL_bits (List.map value_of_aval_bit v, true) in
+ AV_cval (V_lit (bitstring, CT_fbits (List.length v, true)), typ)
+ | AV_tuple avals -> AV_tuple (List.map (c_aval ctx) avals)
+ | aval -> aval
+
+ let c_fragment = function
+ | AV_cval (cval, _) -> cval
+ | _ -> assert false
+
+ (* Map over all the functions in an aexp. *)
+ let rec analyze_functions ctx f (AE_aux (aexp, env, l)) =
+ let ctx = { ctx with local_env = env } in
+ let aexp = match aexp with
+ | AE_app (id, vs, typ) -> f ctx id vs typ
+
+ | AE_cast (aexp, typ) -> AE_cast (analyze_functions ctx f aexp, typ)
+
+ | AE_assign (id, typ, aexp) -> AE_assign (id, typ, analyze_functions ctx f aexp)
+
+ | AE_write_ref (id, typ, aexp) -> AE_write_ref (id, typ, analyze_functions ctx f aexp)
+
+ | AE_short_circuit (op, aval, aexp) -> AE_short_circuit (op, aval, analyze_functions ctx f aexp)
+
+ | AE_let (mut, id, typ1, aexp1, (AE_aux (_, env2, _) as aexp2), typ2) ->
+ let aexp1 = analyze_functions ctx f aexp1 in
+ (* Use aexp2's environment because it will contain constraints for id *)
+ let ctyp1 = convert_typ { ctx with local_env = env2 } typ1 in
+ let ctx = { ctx with locals = Bindings.add id (mut, ctyp1) ctx.locals } in
+ AE_let (mut, id, typ1, aexp1, analyze_functions ctx f aexp2, typ2)
+
+ | AE_block (aexps, aexp, typ) -> AE_block (List.map (analyze_functions ctx f) aexps, analyze_functions ctx f aexp, typ)
+
+ | AE_if (aval, aexp1, aexp2, typ) ->
+ AE_if (aval, analyze_functions ctx f aexp1, analyze_functions ctx f aexp2, typ)
+
+ | AE_loop (loop_typ, aexp1, aexp2) -> AE_loop (loop_typ, analyze_functions ctx f aexp1, analyze_functions ctx f aexp2)
+
+ | AE_for (id, aexp1, aexp2, aexp3, order, aexp4) ->
+ let aexp1 = analyze_functions ctx f aexp1 in
+ let aexp2 = analyze_functions ctx f aexp2 in
+ let aexp3 = analyze_functions ctx f aexp3 in
+ let aexp4 = analyze_functions ctx f aexp4 in
+ (* Currently we assume that loop indexes are always safe to put into an int64 *)
+ let ctx = { ctx with locals = Bindings.add id (Immutable, CT_fint 64) ctx.locals } in
+ AE_for (id, aexp1, aexp2, aexp3, order, aexp4)
+
+ | AE_case (aval, cases, typ) ->
+ let analyze_case (AP_aux (_, env, _) as pat, aexp1, aexp2) =
+ let pat_bindings = Bindings.bindings (apat_types pat) in
+ let ctx = { ctx with local_env = env } in
+ let ctx =
+ List.fold_left (fun ctx (id, typ) -> { ctx with locals = Bindings.add id (Immutable, convert_typ ctx typ) ctx.locals }) ctx pat_bindings
+ in
+ pat, analyze_functions ctx f aexp1, analyze_functions ctx f aexp2
in
- pat, analyze_functions ctx f aexp1, analyze_functions ctx f aexp2
- in
- AE_case (aval, List.map analyze_case cases, typ)
+ AE_case (aval, List.map analyze_case cases, typ)
- | AE_try (aexp, cases, typ) ->
- AE_try (analyze_functions ctx f aexp, List.map (fun (pat, aexp1, aexp2) -> pat, analyze_functions ctx f aexp1, analyze_functions ctx f aexp2) cases, typ)
+ | AE_try (aexp, cases, typ) ->
+ AE_try (analyze_functions ctx f aexp, List.map (fun (pat, aexp1, aexp2) -> pat, analyze_functions ctx f aexp1, analyze_functions ctx f aexp2) cases, typ)
- | AE_field _ | AE_record_update _ | AE_val _ | AE_return _ | AE_throw _ as v -> v
- in
- AE_aux (aexp, env, l)
+ | AE_field _ | AE_record_update _ | AE_val _ | AE_return _ | AE_throw _ as v -> v
+ in
+ AE_aux (aexp, env, l)
-let analyze_primop' ctx id args typ =
- let no_change = AE_app (id, args, typ) in
- let args = List.map (c_aval ctx) args in
- let extern = if Env.is_extern id ctx.tc_env "c" then Env.get_extern id ctx.tc_env "c" else failwith "Not extern" in
+ let analyze_primop' ctx id args typ =
+ let no_change = AE_app (id, args, typ) in
+ let args = List.map (c_aval ctx) args in
+ let extern = if Env.is_extern id ctx.tc_env "c" then Env.get_extern id ctx.tc_env "c" else failwith "Not extern" in
- let v_one = V_lit (VL_int (Big_int.of_int 1), CT_fint 64) in
- let v_int n = V_lit (VL_int (Big_int.of_int n), CT_fint 64) in
+ let v_one = V_lit (VL_int (Big_int.of_int 1), CT_fint 64) in
+ let v_int n = V_lit (VL_int (Big_int.of_int n), CT_fint 64) in
- match extern, args with
- | "eq_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) ->
- begin match cval_ctyp v1 with
- | CT_fbits _ | CT_sbits _ ->
+ match extern, args with
+ | "eq_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) ->
+ begin match cval_ctyp v1 with
+ | CT_fbits _ | CT_sbits _ ->
AE_val (AV_cval (V_call (Eq, [v1; v2]), typ))
- | _ -> no_change
- end
+ | _ -> no_change
+ end
- | "neq_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) ->
- begin match cval_ctyp v1 with
- | CT_fbits _ | CT_sbits _ ->
- AE_val (AV_cval (V_call (Neq, [v1; v2]), typ))
- | _ -> no_change
- end
+ | "neq_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) ->
+ begin match cval_ctyp v1 with
+ | CT_fbits _ | CT_sbits _ ->
+ AE_val (AV_cval (V_call (Neq, [v1; v2]), typ))
+ | _ -> no_change
+ end
- | "eq_int", [AV_cval (v1, _); AV_cval (v2, _)] ->
- AE_val (AV_cval (V_call (Eq, [v1; v2]), typ))
+ | "eq_int", [AV_cval (v1, _); AV_cval (v2, _)] ->
+ AE_val (AV_cval (V_call (Eq, [v1; v2]), typ))
- | "eq_bit", [AV_cval (v1, _); AV_cval (v2, _)] ->
- AE_val (AV_cval (V_call (Eq, [v1; v2]), typ))
+ | "eq_bit", [AV_cval (v1, _); AV_cval (v2, _)] ->
+ AE_val (AV_cval (V_call (Eq, [v1; v2]), typ))
- | "zeros", [_] ->
- begin match destruct_vector ctx.tc_env typ with
- | Some (Nexp_aux (Nexp_constant n, _), _, Typ_aux (Typ_id id, _))
- when string_of_id id = "bit" && Big_int.less_equal n (Big_int.of_int 64) ->
- let n = Big_int.to_int n in
- AE_val (AV_cval (V_lit (VL_bits (Util.list_init n (fun _ -> Sail2_values.B0), true), CT_fbits (n, true)), typ))
- | _ -> no_change
- end
+ | "zeros", [_] ->
+ begin match destruct_vector ctx.tc_env typ with
+ | Some (Nexp_aux (Nexp_constant n, _), _, Typ_aux (Typ_id id, _))
+ when string_of_id id = "bit" && Big_int.less_equal n (Big_int.of_int 64) ->
+ let n = Big_int.to_int n in
+ AE_val (AV_cval (V_lit (VL_bits (Util.list_init n (fun _ -> Sail2_values.B0), true), CT_fbits (n, true)), typ))
+ | _ -> no_change
+ end
- | "zero_extend", [AV_cval (v, _); _] ->
- begin match destruct_vector ctx.tc_env typ with
- | Some (Nexp_aux (Nexp_constant n, _), _, Typ_aux (Typ_id id, _))
- when string_of_id id = "bit" && Big_int.less_equal n (Big_int.of_int 64) ->
- AE_val (AV_cval (V_call (Zero_extend (Big_int.to_int n), [v]), typ))
- | _ -> no_change
- end
+ | "zero_extend", [AV_cval (v, _); _] ->
+ begin match destruct_vector ctx.tc_env typ with
+ | Some (Nexp_aux (Nexp_constant n, _), _, Typ_aux (Typ_id id, _))
+ when string_of_id id = "bit" && Big_int.less_equal n (Big_int.of_int 64) ->
+ AE_val (AV_cval (V_call (Zero_extend (Big_int.to_int n), [v]), typ))
+ | _ -> no_change
+ end
- | "sign_extend", [AV_cval (v, _); _] ->
- begin match destruct_vector ctx.tc_env typ with
- | Some (Nexp_aux (Nexp_constant n, _), _, Typ_aux (Typ_id id, _))
- when string_of_id id = "bit" && Big_int.less_equal n (Big_int.of_int 64) ->
- AE_val (AV_cval (V_call (Sign_extend (Big_int.to_int n), [v]), typ))
- | _ -> no_change
- end
+ | "sign_extend", [AV_cval (v, _); _] ->
+ begin match destruct_vector ctx.tc_env typ with
+ | Some (Nexp_aux (Nexp_constant n, _), _, Typ_aux (Typ_id id, _))
+ when string_of_id id = "bit" && Big_int.less_equal n (Big_int.of_int 64) ->
+ AE_val (AV_cval (V_call (Sign_extend (Big_int.to_int n), [v]), typ))
+ | _ -> no_change
+ end
- | "lteq", [AV_cval (v1, _); AV_cval (v2, _)] ->
- AE_val (AV_cval (V_call (Ilteq, [v1; v2]), typ))
- | "gteq", [AV_cval (v1, _); AV_cval (v2, _)] ->
- AE_val (AV_cval (V_call (Igteq, [v1; v2]), typ))
- | "lt", [AV_cval (v1, _); AV_cval (v2, _)] ->
- AE_val (AV_cval (V_call (Ilt, [v1; v2]), typ))
- | "gt", [AV_cval (v1, _); AV_cval (v2, _)] ->
- AE_val (AV_cval (V_call (Igt, [v1; v2]), typ))
-
- | "append", [AV_cval (v1, _); AV_cval (v2, _)] ->
- begin match ctyp_of_typ ctx typ with
- | CT_fbits _ | CT_sbits _ ->
- AE_val (AV_cval (V_call (Concat, [v1; v2]), typ))
- | _ -> no_change
- end
+ | "lteq", [AV_cval (v1, _); AV_cval (v2, _)] ->
+ AE_val (AV_cval (V_call (Ilteq, [v1; v2]), typ))
+ | "gteq", [AV_cval (v1, _); AV_cval (v2, _)] ->
+ AE_val (AV_cval (V_call (Igteq, [v1; v2]), typ))
+ | "lt", [AV_cval (v1, _); AV_cval (v2, _)] ->
+ AE_val (AV_cval (V_call (Ilt, [v1; v2]), typ))
+ | "gt", [AV_cval (v1, _); AV_cval (v2, _)] ->
+ AE_val (AV_cval (V_call (Igt, [v1; v2]), typ))
+
+ | "append", [AV_cval (v1, _); AV_cval (v2, _)] ->
+ begin match convert_typ ctx typ with
+ | CT_fbits _ | CT_sbits _ ->
+ AE_val (AV_cval (V_call (Concat, [v1; v2]), typ))
+ | _ -> no_change
+ end
- | "not_bits", [AV_cval (v, _)] ->
- AE_val (AV_cval (V_call (Bvnot, [v]), typ))
+ | "not_bits", [AV_cval (v, _)] ->
+ AE_val (AV_cval (V_call (Bvnot, [v]), typ))
- | "add_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) ->
- AE_val (AV_cval (V_call (Bvadd, [v1; v2]), typ))
+ | "add_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) ->
+ AE_val (AV_cval (V_call (Bvadd, [v1; v2]), typ))
- | "sub_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) ->
- AE_val (AV_cval (V_call (Bvsub, [v1; v2]), typ))
+ | "sub_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) ->
+ AE_val (AV_cval (V_call (Bvsub, [v1; v2]), typ))
- | "and_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) ->
- AE_val (AV_cval (V_call (Bvand, [v1; v2]), typ))
+ | "and_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) ->
+ AE_val (AV_cval (V_call (Bvand, [v1; v2]), typ))
- | "or_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) ->
- AE_val (AV_cval (V_call (Bvor, [v1; v2]), typ))
+ | "or_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) ->
+ AE_val (AV_cval (V_call (Bvor, [v1; v2]), typ))
- | "xor_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) ->
- AE_val (AV_cval (V_call (Bvxor, [v1; v2]), typ))
+ | "xor_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) ->
+ AE_val (AV_cval (V_call (Bvxor, [v1; v2]), typ))
- | "vector_subrange", [AV_cval (vec, _); AV_cval (f, _); AV_cval (t, _)] ->
- begin match ctyp_of_typ ctx typ with
- | CT_fbits (n, true) ->
- AE_val (AV_cval (V_call (Slice n, [vec; t]), typ))
- | _ -> no_change
- end
+ | "vector_subrange", [AV_cval (vec, _); AV_cval (f, _); AV_cval (t, _)] ->
+ begin match convert_typ ctx typ with
+ | CT_fbits (n, true) ->
+ AE_val (AV_cval (V_call (Slice n, [vec; t]), typ))
+ | _ -> no_change
+ end
- | "slice", [AV_cval (vec, _); AV_cval (start, _); AV_cval (len, _)] ->
- begin match ctyp_of_typ ctx typ with
- | CT_fbits (n, _) ->
- AE_val (AV_cval (V_call (Slice n, [vec; start]), typ))
- | CT_sbits (64, _) ->
- AE_val (AV_cval (V_call (Sslice 64, [vec; start; len]), typ))
- | _ -> no_change
- end
+ | "slice", [AV_cval (vec, _); AV_cval (start, _); AV_cval (len, _)] ->
+ begin match convert_typ ctx typ with
+ | CT_fbits (n, _) ->
+ AE_val (AV_cval (V_call (Slice n, [vec; start]), typ))
+ | CT_sbits (64, _) ->
+ AE_val (AV_cval (V_call (Sslice 64, [vec; start; len]), typ))
+ | _ -> no_change
+ end
- | "vector_access", [AV_cval (vec, _); AV_cval (n, _)] ->
- AE_val (AV_cval (V_call (Bvaccess, [vec; n]), typ))
+ | "vector_access", [AV_cval (vec, _); AV_cval (n, _)] ->
+ AE_val (AV_cval (V_call (Bvaccess, [vec; n]), typ))
- | "add_int", [AV_cval (op1, _); AV_cval (op2, _)] ->
- begin match destruct_range Env.empty typ with
- | None -> no_change
- | Some (kids, constr, n, m) ->
- match nexp_simp n, nexp_simp m with
- | Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_constant m, _)
+ | "add_int", [AV_cval (op1, _); AV_cval (op2, _)] ->
+ begin match destruct_range Env.empty typ with
+ | None -> no_change
+ | Some (kids, constr, n, m) ->
+ match nexp_simp n, nexp_simp m with
+ | Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_constant m, _)
when Big_int.less_equal (min_int 64) n && Big_int.less_equal m (max_int 64) ->
- AE_val (AV_cval (V_call (Iadd, [op1; op2]), typ))
- | n, m when prove __POS__ ctx.local_env (nc_lteq (nconstant (min_int 64)) n) && prove __POS__ ctx.local_env (nc_lteq m (nconstant (max_int 64))) ->
- AE_val (AV_cval (V_call (Iadd, [op1; op2]), typ))
- | _ -> no_change
- end
+ AE_val (AV_cval (V_call (Iadd, [op1; op2]), typ))
+ | n, m when prove __POS__ ctx.local_env (nc_lteq (nconstant (min_int 64)) n) && prove __POS__ ctx.local_env (nc_lteq m (nconstant (max_int 64))) ->
+ AE_val (AV_cval (V_call (Iadd, [op1; op2]), typ))
+ | _ -> no_change
+ end
- | "replicate_bits", [AV_cval (vec, vtyp); _] ->
- begin match destruct_vector ctx.tc_env typ, destruct_vector ctx.tc_env vtyp with
- | Some (Nexp_aux (Nexp_constant n, _), _, _), Some (Nexp_aux (Nexp_constant m, _), _, _)
- when Big_int.less_equal n (Big_int.of_int 64) ->
- let times = Big_int.div n m in
- if Big_int.equal (Big_int.mul m times) n then
- AE_val (AV_cval (V_call (Replicate (Big_int.to_int times), [vec]), typ))
- else
+ | "replicate_bits", [AV_cval (vec, vtyp); _] ->
+ begin match destruct_vector ctx.tc_env typ, destruct_vector ctx.tc_env vtyp with
+ | Some (Nexp_aux (Nexp_constant n, _), _, _), Some (Nexp_aux (Nexp_constant m, _), _, _)
+ when Big_int.less_equal n (Big_int.of_int 64) ->
+ let times = Big_int.div n m in
+ if Big_int.equal (Big_int.mul m times) n then
+ AE_val (AV_cval (V_call (Replicate (Big_int.to_int times), [vec]), typ))
+ else
+ no_change
+ | _, _ ->
no_change
- | _, _ ->
- no_change
- end
-
- | "undefined_bit", _ ->
- AE_val (AV_cval (V_lit (VL_bit Sail2_values.B0, CT_bit), typ))
+ end
- | "undefined_bool", _ ->
- AE_val (AV_cval (V_lit (VL_bool false, CT_bool), typ))
+ | "undefined_bit", _ ->
+ AE_val (AV_cval (V_lit (VL_bit Sail2_values.B0, CT_bit), typ))
- | _, _ ->
- no_change
+ | "undefined_bool", _ ->
+ AE_val (AV_cval (V_lit (VL_bool false, CT_bool), typ))
-let analyze_primop ctx id args typ =
- let no_change = AE_app (id, args, typ) in
- if !optimize_primops then
- try analyze_primop' ctx id args typ with
- | Failure str ->
+ | _, _ ->
no_change
- else
- no_change
+
+ let analyze_primop ctx id args typ =
+ let no_change = AE_app (id, args, typ) in
+ if !optimize_primops then
+ try analyze_primop' ctx id args typ with
+ | Failure str ->
+ no_change
+ else
+ no_change
+
+ let optimize_anf ctx aexp =
+ analyze_functions ctx analyze_primop (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
@@ -631,7 +648,7 @@ let fix_early_stack_return ret ret_ctyp instrs =
rewrite_return instrs
let rec insert_heap_returns ret_ctyps = function
- | (CDEF_spec (id, _, ret_ctyp) as cdef) :: cdefs ->
+ | (CDEF_spec (id, _, _, ret_ctyp) as cdef) :: cdefs ->
cdef :: insert_heap_returns (Bindings.add id ret_ctyp ret_ctyps) cdefs
| CDEF_fundef (id, None, args, body) :: cdefs ->
@@ -1107,10 +1124,9 @@ let rec sgen_value = function
| VL_bit Sail2_values.BU -> failwith "Undefined bit found in value"
| VL_real str -> str
| VL_string str -> "\"" ^ str ^ "\""
- | VL_matcher (n, uid) -> Printf.sprintf "matcher(%d, %d)" n uid
- | VL_tuple values -> "(" ^ Util.string_of_list ", " string_of_value values ^ ")"
+ | VL_tuple values -> "(" ^ Util.string_of_list ", " sgen_value values ^ ")"
| VL_list [] -> "NULL"
- | VL_list values -> "[|" ^ Util.string_of_list ", " string_of_value values ^ "|]"
+ | VL_list values -> "[|" ^ Util.string_of_list ", " sgen_value values ^ "|]"
| VL_enum element -> Util.zencode_string element
| VL_ref r -> "&" ^ Util.zencode_string r
@@ -1998,7 +2014,7 @@ let codegen_def' ctx = function
string (Printf.sprintf "// register %s" (string_of_id id)) ^^ hardline
^^ string (Printf.sprintf "%s %s;" (sgen_ctyp ctyp) (sgen_id id))
- | CDEF_spec (id, arg_ctyps, ret_ctyp) ->
+ | CDEF_spec (id, _, arg_ctyps, ret_ctyp) ->
let static = if !opt_static then "static " else "" in
if Env.is_extern id ctx.tc_env "c" then
empty
@@ -2173,13 +2189,9 @@ let rec get_recursive_functions (Defs defs) =
| [] -> IdSet.empty
let jib_of_ast env ast =
- let ctx =
- initial_ctx
- ~convert_typ:ctyp_of_typ
- ~optimize_anf:(fun ctx aexp -> analyze_functions ctx analyze_primop (c_literals ctx aexp))
- env
- in
- Jib_compile.compile_ast ctx ast
+ let 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
diff --git a/src/jib/c_backend.mli b/src/jib/c_backend.mli
index 2f748fd7..e627ebd8 100644
--- a/src/jib/c_backend.mli
+++ b/src/jib/c_backend.mli
@@ -106,8 +106,5 @@ val optimize_alias : bool ref
val optimize_fixed_int : bool ref
val optimize_fixed_bits : bool ref
-(** Convert a typ to a IR ctyp *)
-val ctyp_of_typ : Jib_compile.ctx -> Ast.typ -> ctyp
-
val jib_of_ast : Env.t -> tannot Ast.defs -> cdef list * Jib_compile.ctx
val compile_ast : Env.t -> out_channel -> string list -> tannot Ast.defs -> unit
diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml
index 7cc1dd28..202abbd5 100644
--- a/src/jib/jib_compile.ml
+++ b/src/jib/jib_compile.ml
@@ -151,40 +151,38 @@ type ctx =
enums : IdSet.t Bindings.t;
variants : (ctyp UBindings.t) Bindings.t;
valspecs : (ctyp list * ctyp) Bindings.t;
- tc_env : Env.t;
local_env : Env.t;
+ tc_env : Env.t;
locals : (mut * ctyp) Bindings.t;
letbinds : int list;
no_raw : bool;
- unroll_loops : int option;
- convert_typ : ctx -> typ -> ctyp;
- optimize_anf : ctx -> typ aexp -> typ aexp;
- specialize_calls : bool;
- ignore_64 : bool;
- struct_value : bool;
- use_real : bool;
}
-let initial_ctx ~convert_typ:convert_typ ~optimize_anf:optimize_anf env =
+let initial_ctx env =
{ records = Bindings.empty;
enums = Bindings.empty;
variants = Bindings.empty;
valspecs = Bindings.empty;
- tc_env = env;
local_env = env;
+ tc_env = env;
locals = Bindings.empty;
letbinds = [];
no_raw = false;
- unroll_loops = None;
- convert_typ = convert_typ;
- optimize_anf = optimize_anf;
- specialize_calls = false;
- ignore_64 = false;
- struct_value = false;
- use_real = false;
}
-let ctyp_of_typ ctx typ = ctx.convert_typ ctx typ
+module type Config = sig
+ val convert_typ : ctx -> typ -> ctyp
+ val optimize_anf : ctx -> typ aexp -> typ aexp
+ val unroll_loops : unit -> int option
+ val specialize_calls : bool
+ val ignore_64 : bool
+ val struct_value : bool
+ val use_real : bool
+end
+
+module Make(C: Config) = struct
+
+let ctyp_of_typ ctx typ = C.convert_typ ctx typ
let rec chunkify n xs =
match Util.take n xs, Util.drop n xs with
@@ -217,7 +215,7 @@ let rec compile_aval l ctx = function
| AV_lit (L_aux (L_string str, _), typ) ->
[], V_lit ((VL_string (String.escaped str)), ctyp_of_typ ctx typ), []
- | AV_lit (L_aux (L_num n, _), typ) when ctx.ignore_64 ->
+ | AV_lit (L_aux (L_num n, _), typ) when C.ignore_64 ->
[], V_lit ((VL_int n), ctyp_of_typ ctx typ), []
| AV_lit (L_aux (L_num n, _), typ) when Big_int.less_equal (min_int 64) n && Big_int.less_equal n (max_int 64) ->
@@ -239,7 +237,7 @@ let rec compile_aval l ctx = function
| AV_lit (L_aux (L_false, _), _) -> [], V_lit (VL_bool false, CT_bool), []
| AV_lit (L_aux (L_real str, _), _) ->
- if ctx.use_real then
+ if C.use_real then
[], V_lit (VL_real str, CT_real), []
else
let gs = ngensym () in
@@ -266,7 +264,7 @@ let rec compile_aval l ctx = function
[iclear tup_ctyp gs]
@ cleanup
- | AV_record (fields, typ) when ctx.struct_value ->
+ | AV_record (fields, typ) when C.struct_value ->
let ctyp = ctyp_of_typ ctx typ in
let gs = ngensym () in
let compile_fields (id, aval) =
@@ -311,7 +309,7 @@ let rec compile_aval l ctx = function
end
(* Convert a small bitvector to a uint64_t literal. *)
- | AV_vector (avals, typ) when is_bitvector avals && (List.length avals <= 64 || ctx.ignore_64) ->
+ | AV_vector (avals, typ) when is_bitvector avals && (List.length avals <= 64 || C.ignore_64) ->
begin
let bitstring = List.map value_of_aval_bit avals in
let len = List.length avals in
@@ -422,7 +420,7 @@ let optimize_call l ctx clexp id args arg_ctyps ret_ctyp =
let have_ctyp = cval_ctyp cval in
if is_polymorphic ctyp then
V_poly (cval, have_ctyp)
- else if ctx.specialize_calls || ctyp_equal ctyp have_ctyp then
+ else if C.specialize_calls || ctyp_equal ctyp have_ctyp then
cval
else
let gs = ngensym () in
@@ -431,7 +429,7 @@ let optimize_call l ctx clexp id args arg_ctyps ret_ctyp =
V_id (gs, ctyp))
arg_ctyps args
in
- if ctx.specialize_calls || ctyp_equal (clexp_ctyp clexp) ret_ctyp then
+ if C.specialize_calls || ctyp_equal (clexp_ctyp clexp) ret_ctyp then
!setup @ [ifuncall clexp id cast_args] @ !cleanup
else
let gs = ngensym () in
@@ -442,7 +440,7 @@ let optimize_call l ctx clexp id args arg_ctyps ret_ctyp =
iclear ret_ctyp gs]
@ !cleanup
in
- if not ctx.specialize_calls && Env.is_extern (fst id) ctx.tc_env "c" then
+ if not C.specialize_calls && Env.is_extern (fst id) ctx.tc_env "c" then
let extern = Env.get_extern (fst id) ctx.tc_env "c" in
begin match extern, List.map cval_ctyp args, clexp_ctyp clexp with
| "slice", [CT_fbits _; CT_lint; _], CT_fbits (n, _) ->
@@ -942,7 +940,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
(* We can either generate an actual loop body for C, or unroll the body for SMT *)
let actual = loop_body [ilabel loop_start_label] (fun () -> [igoto loop_start_label]) in
let rec unroll max n = loop_body [] (fun () -> if n < max then unroll max (n + 1) else [imatch_failure ()]) in
- let body = match ctx.unroll_loops with Some times -> unroll times 0 | None -> actual in
+ let body = match C.unroll_loops () with Some times -> unroll times 0 | None -> actual in
variable_init from_gs from_setup from_call from_cleanup
@ variable_init to_gs to_setup to_call to_cleanup
@@ -1221,7 +1219,7 @@ let compile_funcl ctx id pat guard exp =
let guard_instrs = match guard with
| Some guard ->
- let guard_aexp = ctx.optimize_anf ctx (no_shadow (pat_ids pat) (anf guard)) in
+ let guard_aexp = C.optimize_anf ctx (no_shadow (pat_ids pat) (anf guard)) in
let guard_setup, guard_call, guard_cleanup = compile_aexp ctx guard_aexp in
let guard_label = label "guard_" in
let gs = ngensym () in
@@ -1238,7 +1236,7 @@ let compile_funcl ctx id pat guard exp =
in
(* Optimize and compile the expression to ANF. *)
- let aexp = ctx.optimize_anf ctx (no_shadow (pat_ids pat) (anf exp)) in
+ let aexp = C.optimize_anf ctx (no_shadow (pat_ids pat) (anf exp)) in
let setup, call, cleanup = compile_aexp ctx aexp in
let destructure, destructure_cleanup =
@@ -1290,7 +1288,7 @@ and compile_def' n total ctx = function
| DEF_reg_dec (DEC_aux (DEC_reg (_, _, typ, id), _)) ->
[CDEF_reg_dec (id, ctyp_of_typ ctx typ, [])], ctx
| DEF_reg_dec (DEC_aux (DEC_config (id, typ, exp), _)) ->
- let aexp = ctx.optimize_anf ctx (no_shadow IdSet.empty (anf exp)) in
+ let 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
[CDEF_reg_dec (id, ctyp_of_typ ctx typ, instrs)], ctx
@@ -1300,13 +1298,19 @@ and compile_def' n total ctx = function
| DEF_spec (VS_aux (VS_val_spec (_, id, _, _), _)) ->
let quant, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_env in
+ let extern =
+ if Env.is_extern id ctx.tc_env "c" then
+ Some (Env.get_extern id ctx.tc_env "c")
+ else
+ None
+ in
let arg_typs, ret_typ = match fn_typ with
| Typ_fn (arg_typs, ret_typ, _) -> arg_typs, ret_typ
| _ -> assert false
in
let ctx' = { ctx with local_env = add_typquant (id_loc id) quant ctx.local_env } in
let arg_ctyps, ret_ctyp = List.map (ctyp_of_typ ctx') arg_typs, ctyp_of_typ ctx' ret_typ in
- [CDEF_spec (id, arg_ctyps, ret_ctyp)],
+ [CDEF_spec (id, extern, arg_ctyps, ret_ctyp)],
{ ctx with valspecs = Bindings.add id (arg_ctyps, ret_ctyp) ctx.valspecs }
| DEF_fundef (FD_aux (FD_function (_, _, _, [FCL_aux (FCL_Funcl (id, Pat_aux (Pat_exp (pat, exp), _)), _)]), _)) ->
@@ -1333,7 +1337,7 @@ and compile_def' n total ctx = function
| DEF_val (LB_aux (LB_val (pat, exp), _)) ->
let ctyp = ctyp_of_typ ctx (typ_of_pat pat) in
- let aexp = ctx.optimize_anf ctx (no_shadow IdSet.empty (anf exp)) in
+ let aexp = C.optimize_anf ctx (no_shadow IdSet.empty (anf exp)) in
let setup, call, cleanup = compile_aexp ctx aexp in
let apat = anf_pat ~global:true pat in
let gs = ngensym () in
@@ -1554,12 +1558,6 @@ let sort_ctype_defs cdefs =
ctype_defs @ cdefs
let compile_ast ctx (Defs defs) =
- let assert_vs = Initial_check.extern_of_string (mk_id "sail_assert") "(bool, string) -> unit" in
- let exit_vs = Initial_check.extern_of_string (mk_id "sail_exit") "unit -> unit" in
- let cons_vs = Initial_check.extern_of_string (mk_id "sail_cons") "forall ('a : Type). ('a, list('a)) -> list('a)" in
-
- let ctx = { ctx with tc_env = snd (Type_error.check ctx.tc_env (Defs [assert_vs; exit_vs; cons_vs])) } in
-
if !opt_memo_cache then
(try
if Sys.is_directory "_sbuild" then
@@ -1578,3 +1576,12 @@ let compile_ast ctx (Defs defs) =
let cdefs, ctx = specialize_variants ctx [] cdefs in
let cdefs = sort_ctype_defs cdefs in
cdefs, ctx
+
+end
+
+let add_special_functions env =
+ let assert_vs = Initial_check.extern_of_string (mk_id "sail_assert") "(bool, string) -> unit" in
+ let exit_vs = Initial_check.extern_of_string (mk_id "sail_exit") "unit -> unit" in
+ let cons_vs = Initial_check.extern_of_string (mk_id "sail_cons") "forall ('a : Type). ('a, list('a)) -> list('a)" in
+
+ snd (Type_error.check env (Defs [assert_vs; exit_vs; cons_vs]))
diff --git a/src/jib/jib_compile.mli b/src/jib/jib_compile.mli
index 4f9fecd8..6269b40d 100644
--- a/src/jib/jib_compile.mli
+++ b/src/jib/jib_compile.mli
@@ -58,54 +58,65 @@ open Type_check
(** This forces all integer struct fields to be represented as
int64_t. Specifically intended for the various TLB structs in the
- ARM v8.5 spec. *)
+ ARM v8.5 spec. It is unsound in general. *)
val optimize_aarch64_fast_struct : bool ref
(** {2 Jib context} *)
-(** Context for compiling Sail to Jib. We need to pass a (global)
- typechecking environment given by checking the full AST. We have to
- provide a conversion function from Sail types into Jib types, as
- well as a function that optimizes ANF expressions (which can just
- be the identity function) *)
+(** Dynamic context for compiling Sail to Jib. We need to pass a
+ (global) typechecking environment given by checking the full
+ AST. *)
type ctx =
{ records : (ctyp Jib_util.UBindings.t) Bindings.t;
enums : IdSet.t Bindings.t;
variants : (ctyp Jib_util.UBindings.t) Bindings.t;
valspecs : (ctyp list * ctyp) Bindings.t;
- tc_env : Env.t;
local_env : Env.t;
+ tc_env : Env.t;
locals : (mut * ctyp) Bindings.t;
letbinds : int list;
no_raw : bool;
- unroll_loops : int option;
- convert_typ : ctx -> typ -> ctyp;
- optimize_anf : ctx -> typ aexp -> typ aexp;
- (** If false (default), function arguments must match the function
- type exactly. If true, they can be more specific. *)
- specialize_calls : bool;
- (** If false (default), will ensure that fixed size bitvectors are
- specifically less that 64-bits. If true this restriction will
- be ignored. *)
- ignore_64 : bool;
- (** If false (default) we won't generate any V_struct values *)
- struct_value : bool;
- (** Allow real literals *)
- use_real : bool;
}
-val initial_ctx :
- convert_typ:(ctx -> typ -> ctyp) ->
- optimize_anf:(ctx -> typ aexp -> typ aexp) ->
- Env.t ->
- ctx
+val initial_ctx : Env.t -> ctx
(** {2 Compilation functions} *)
-(** Compile a Sail definition into a Jib definition. The first two
- arguments are is the current definition number and the total number
- of definitions, and can be used to drive a progress bar (see
- Util.progress). *)
-val compile_def : int -> int -> ctx -> tannot def -> cdef list * ctx
+(** The Config module specifies static configuration for compiling
+ Sail into Jib. We have to provide a conversion
+ function from Sail types into Jib types, as well as a function that
+ optimizes ANF expressions (which can just be the identity function)
+ *)
+module type Config = sig
+ val convert_typ : ctx -> typ -> ctyp
+ val optimize_anf : ctx -> typ aexp -> typ aexp
+ (** Unroll all for loops a bounded number of times. Used for SMT
+ generation. *)
+ val unroll_loops : unit -> int option
+ (** If false, function arguments must match the function
+ type exactly. If true, they can be more specific. *)
+ val specialize_calls : bool
+ (** If false, will ensure that fixed size bitvectors are
+ specifically less that 64-bits. If true this restriction will
+ be ignored. *)
+ val ignore_64 : bool
+ (** If false we won't generate any V_struct values *)
+ val struct_value : bool
+ (** Allow real literals *)
+ val use_real : bool
+end
+
+module Make(C: Config) : sig
+ (** Compile a Sail definition into a Jib definition. The first two
+ arguments are is the current definition number and the total
+ number of definitions, and can be used to drive a progress bar
+ (see Util.progress). *)
+ val compile_def : int -> int -> ctx -> tannot def -> cdef list * ctx
+
+ val compile_ast : ctx -> tannot defs -> cdef list * ctx
+end
-val compile_ast : ctx -> tannot defs -> cdef list * ctx
+(** Adds some special functions to the environment that are used to
+ convert several Sail language features, these are sail_assert,
+ sail_exit, and sail_cons. *)
+val add_special_functions : Env.t -> Env.t
diff --git a/src/jib/jib_ir.ml b/src/jib/jib_ir.ml
index 2fdc4b88..3ab634d2 100644
--- a/src/jib/jib_ir.ml
+++ b/src/jib/jib_ir.ml
@@ -151,8 +151,10 @@ module Ir_formatter = struct
let output_def buf = function
| CDEF_reg_dec (id, ctyp, _) ->
Buffer.add_string buf (sprintf "%s %s : %s" (C.keyword "register") (zencode_id id) (C.typ ctyp))
- | CDEF_spec (id, ctyps, ctyp) ->
+ | CDEF_spec (id, None, ctyps, ctyp) ->
Buffer.add_string buf (sprintf "%s %s : (%s) -> %s" (C.keyword "val") (zencode_id id) (Util.string_of_list ", " C.typ ctyps) (C.typ ctyp));
+ | CDEF_spec (id, Some extern, ctyps, ctyp) ->
+ Buffer.add_string buf (sprintf "%s %s = \"%s\" : (%s) -> %s" (C.keyword "val") (zencode_id id) extern (Util.string_of_list ", " C.typ ctyps) (C.typ ctyp));
| CDEF_fundef (id, ret, args, instrs) ->
let instrs = C.modify_instrs instrs in
let label_map = C.make_label_map instrs in
@@ -247,7 +249,7 @@ let () =
ArgString ("(val|register)? identifier", fun arg -> Action (fun () ->
let is_def id = function
| CDEF_fundef (id', _, _, _) -> Id.compare id id' = 0
- | CDEF_spec (id', _, _) -> Id.compare id (prepend_id "val " id') = 0
+ | CDEF_spec (id', _, _, _) -> Id.compare id (prepend_id "val " id') = 0
| CDEF_reg_dec (id', _, _) -> Id.compare id (prepend_id "register " id') = 0
| _ -> false
in
diff --git a/src/jib/jib_optimize.ml b/src/jib/jib_optimize.ml
index a54ac4b3..82906cb6 100644
--- a/src/jib/jib_optimize.ml
+++ b/src/jib/jib_optimize.ml
@@ -153,7 +153,7 @@ let unique_per_function_ids cdefs =
| CDEF_reg_dec (id, ctyp, instrs) -> CDEF_reg_dec (id, ctyp, unique_instrs i instrs)
| CDEF_type ctd -> CDEF_type ctd
| CDEF_let (n, bindings, instrs) -> CDEF_let (n, bindings, unique_instrs i instrs)
- | CDEF_spec (id, ctyps, ctyp) -> CDEF_spec (id, ctyps, ctyp)
+ | CDEF_spec (id, extern, ctyps, ctyp) -> CDEF_spec (id, extern, ctyps, ctyp)
| CDEF_fundef (id, heap_return, args, instrs) -> CDEF_fundef (id, heap_return, args, unique_instrs i instrs)
| CDEF_startup (id, instrs) -> CDEF_startup (id, unique_instrs i instrs)
| CDEF_finish (id, instrs) -> CDEF_finish (id, unique_instrs i instrs)
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index df3be1b7..8797f78d 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -1146,7 +1146,7 @@ let smt_builtin ctx name args ret_ctyp =
| "min_int", [v1; v2], _ -> builtin_min_int ctx v1 v2 ret_ctyp
| "ediv_int", [v1; v2], _ -> builtin_tdiv_int ctx v1 v2 ret_ctyp
-
+
(* All signed and unsigned bitvector comparisons *)
| "slt_bits", [v1; v2], CT_bool -> builtin_compare_bits "bvslt" ctx v1 v2 ret_ctyp
| "ult_bits", [v1; v2], CT_bool -> builtin_compare_bits "bvult" ctx v1 v2 ret_ctyp
@@ -1351,146 +1351,144 @@ let rec generate_reg_decs ctx inits = function
let max_int n = Big_int.pred (Big_int.pow_int_positive 2 (n - 1))
let min_int n = Big_int.negate (Big_int.pow_int_positive 2 (n - 1))
-(** Convert a sail type into a C-type. This function can be quite
- slow, because it uses ctx.local_env and SMT to analyse the Sail
- types and attempts to fit them into the smallest possible C
- types, provided ctx.optimize_smt is true (default) **)
-let rec ctyp_of_typ ctx typ =
- let open Ast in
- let open Type_check in
- let open Jib_compile in
- let Typ_aux (typ_aux, l) as typ = Env.expand_synonyms ctx.tc_env typ in
- match typ_aux with
- | Typ_id id when string_of_id id = "bit" -> CT_bit
- | Typ_id id when string_of_id id = "bool" -> CT_bool
- | Typ_id id when string_of_id id = "int" -> CT_lint
- | Typ_id id when string_of_id id = "nat" -> CT_lint
- | Typ_id id when string_of_id id = "unit" -> CT_unit
- | Typ_id id when string_of_id id = "string" -> CT_string
- | Typ_id id when string_of_id id = "real" -> CT_real
-
- | Typ_app (id, _) when string_of_id id = "atom_bool" -> CT_bool
-
- | Typ_app (id, args) when string_of_id id = "itself" ->
- ctyp_of_typ ctx (Typ_aux (Typ_app (mk_id "atom", args), l))
- | Typ_app (id, _) when string_of_id id = "range" || string_of_id id = "atom" || string_of_id id = "implicit" ->
- begin match destruct_range Env.empty typ with
- | None -> assert false (* Checked if range type in guard *)
- | Some (kids, constr, n, m) ->
- let ctx = { ctx with local_env = add_existential Parse_ast.Unknown (List.map (mk_kopt K_int) kids) constr ctx.local_env } in
- match nexp_simp n, nexp_simp m with
- | Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_constant m, _)
- when n = m ->
- CT_constant n
- | Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_constant m, _)
- when Big_int.less_equal (min_int 64) n && Big_int.less_equal m (max_int 64) ->
- CT_fint 64
- | n, m ->
- if prove __POS__ ctx.local_env (nc_lteq (nconstant (min_int 64)) n) && prove __POS__ ctx.local_env (nc_lteq m (nconstant (max_int 64))) then
+module SMT_config : Jib_compile.Config = struct
+ open Jib_compile
+
+ (** Convert a sail type into a C-type. This function can be quite
+ slow, because it uses ctx.local_env and SMT to analyse the Sail
+ types and attempts to fit them into the smallest possible C
+ types, provided ctx.optimize_smt is true (default) **)
+ let rec convert_typ ctx typ =
+ let open Ast in
+ let open Type_check in
+ let Typ_aux (typ_aux, l) as typ = Env.expand_synonyms ctx.tc_env typ in
+ match typ_aux with
+ | Typ_id id when string_of_id id = "bit" -> CT_bit
+ | Typ_id id when string_of_id id = "bool" -> CT_bool
+ | Typ_id id when string_of_id id = "int" -> CT_lint
+ | Typ_id id when string_of_id id = "nat" -> CT_lint
+ | Typ_id id when string_of_id id = "unit" -> CT_unit
+ | Typ_id id when string_of_id id = "string" -> CT_string
+ | Typ_id id when string_of_id id = "real" -> CT_real
+
+ | Typ_app (id, _) when string_of_id id = "atom_bool" -> CT_bool
+
+ | Typ_app (id, args) when string_of_id id = "itself" ->
+ convert_typ ctx (Typ_aux (Typ_app (mk_id "atom", args), l))
+ | Typ_app (id, _) when string_of_id id = "range" || string_of_id id = "atom" || string_of_id id = "implicit" ->
+ begin match destruct_range Env.empty typ with
+ | None -> assert false (* Checked if range type in guard *)
+ | Some (kids, constr, n, m) ->
+ let ctx = { ctx with local_env = add_existential Parse_ast.Unknown (List.map (mk_kopt K_int) kids) constr ctx.local_env } in
+ match nexp_simp n, nexp_simp m with
+ | Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_constant m, _)
+ when n = m ->
+ CT_constant n
+ | 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
- else
- CT_lint
- end
-
- | Typ_app (id, [A_aux (A_typ typ, _)]) when string_of_id id = "list" ->
- CT_list (ctyp_of_typ ctx typ)
-
- (* Note that we have to use lbits for zero-length bitvectors because they are not allowed by SMTLIB *)
- | 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.equal n Big_int.zero -> CT_lbits direction
- | Nexp_aux (Nexp_constant n, _) -> 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, ctyp_of_typ ctx typ)
-
- | Typ_app (id, [A_aux (A_typ typ, _)]) when string_of_id id = "register" ->
- CT_ref (ctyp_of_typ ctx typ)
-
- | Typ_id id | Typ_app (id, _) when Bindings.mem id ctx.records -> CT_struct (id, Bindings.find id ctx.records |> 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 (ctyp_of_typ ctx) typs)
-
- | Typ_exist _ ->
- (* Use Type_check.destruct_exist when optimising with SMT, to
- ensure that we don't cause any type variable clashes in
- local_env, and that we can optimize the existential based upon
- it's constraints. *)
- begin match destruct_exist (Env.expand_synonyms ctx.local_env typ) with
- | Some (kids, nc, typ) ->
- let env = add_existential l kids nc ctx.local_env in
- ctyp_of_typ { ctx with local_env = env } typ
- | None -> raise (Reporting.err_unreachable l __POS__ "Existential cannot be destructured!")
- end
-
- | Typ_var kid -> CT_poly
-
- | _ -> raise (Reporting.err_unreachable l __POS__ ("No SMT type for type " ^ string_of_typ typ))
+ | n, m ->
+ if prove __POS__ ctx.local_env (nc_lteq (nconstant (min_int 64)) n) && prove __POS__ ctx.local_env (nc_lteq m (nconstant (max_int 64))) then
+ CT_fint 64
+ else
+ CT_lint
+ end
-(**************************************************************************)
-(* 3. Optimization of primitives and literals *)
-(**************************************************************************)
+ | Typ_app (id, [A_aux (A_typ typ, _)]) when string_of_id id = "list" ->
+ CT_list (convert_typ ctx typ)
+
+ (* Note that we have to use lbits for zero-length bitvectors because they are not allowed by SMTLIB *)
+ | 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.equal n Big_int.zero -> CT_lbits direction
+ | Nexp_aux (Nexp_constant n, _) -> CT_fbits (Big_int.to_int n, direction)
+ | _ -> CT_lbits direction
+ end
-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_cval (L_aux (l_aux, _) as lit) =
- match l_aux with
- | L_num n -> Some (V_lit (VL_int n, CT_constant n))
- | L_hex str when String.length str <= 16 ->
- let content = Util.string_to_list str |> List.map hex_char |> List.concat in
- Some (V_lit (VL_bits (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 ->
- begin match literal_to_cval lit with
- | Some cval -> AV_cval (cval, typ)
- | None -> v
+ | 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 _ ->
+ (* Use Type_check.destruct_exist when optimising with SMT, to
+ ensure that we don't cause any type variable clashes in
+ local_env, and that we can optimize the existential based
+ upon it's constraints. *)
+ begin match destruct_exist (Env.expand_synonyms ctx.local_env typ) with
+ | Some (kids, nc, typ) ->
+ let env = add_existential l kids nc ctx.local_env in
+ convert_typ { ctx with local_env = env } typ
+ | None -> raise (Reporting.err_unreachable l __POS__ "Existential cannot be destructured!")
end
- | AV_tuple avals -> AV_tuple (List.map (c_literal env l) avals)
- | v -> v
- in
- map_aval c_literal
+
+ | Typ_var kid -> CT_poly
+
+ | _ -> raise (Reporting.err_unreachable l __POS__ ("No SMT type for type " ^ string_of_typ typ))
+
+ 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_cval (L_aux (l_aux, _) as lit) =
+ match l_aux with
+ | L_num n -> Some (V_lit (VL_int n, CT_constant n))
+ | L_hex str when String.length str <= 16 ->
+ let content = Util.string_to_list str |> List.map hex_char |> List.concat in
+ Some (V_lit (VL_bits (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 ->
+ begin match literal_to_cval 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
(* If we know the loop variables exactly (especially after
specialization), we can unroll the exact number of times required,
and omit any comparisons. *)
let unroll_static_foreach ctx = function
| AE_aux (AE_for (id, from_aexp, to_aexp, by_aexp, order, body), env, l) as aexp ->
- begin match ctyp_of_typ ctx (aexp_typ from_aexp), ctyp_of_typ ctx (aexp_typ to_aexp), ctyp_of_typ ctx (aexp_typ by_aexp), order with
+ begin match convert_typ ctx (aexp_typ from_aexp), convert_typ ctx (aexp_typ to_aexp), convert_typ ctx (aexp_typ by_aexp), order with
| CT_constant f, CT_constant t, CT_constant b, Ord_aux (Ord_inc, _) ->
let i = ref f in
let unrolled = ref [] in
@@ -1509,6 +1507,19 @@ let unroll_static_foreach ctx = function
end
| aexp -> aexp
+ let optimize_anf ctx aexp =
+ aexp
+ |> c_literals ctx
+ |> fold_aexp (unroll_static_foreach ctx)
+
+ let specialize_calls = true
+ let ignore_64 = true
+ let unroll_loops () = Some !opt_unroll_limit
+ let struct_value = true
+ let use_real = true
+end
+
+
(**************************************************************************)
(* 3. Generating SMT *)
(**************************************************************************)
@@ -2166,7 +2177,7 @@ let smt_instr_list name ctx all_cdefs instrs =
stack, start, cfg
let smt_cdef props lets name_file ctx all_cdefs = function
- | CDEF_spec (function_id, arg_ctyps, ret_ctyp) when Bindings.mem function_id props ->
+ | CDEF_spec (function_id, _, arg_ctyps, ret_ctyp) when Bindings.mem function_id props ->
begin match find_function [] function_id all_cdefs with
| intervening_lets, Some (None, args, instrs) ->
let prop_type, prop_args, pragma_l, vs = Bindings.find function_id props in
@@ -2262,20 +2273,10 @@ let rec build_register_map rmap = function
let compile env ast =
let cdefs, jib_ctx =
- let open Jib_compile in
- let optimize_anf ctx aexp =
- aexp
- |> c_literals ctx
- |> fold_aexp (unroll_static_foreach ctx)
- in
- let ctx = initial_ctx ~convert_typ:ctyp_of_typ ~optimize_anf:optimize_anf env in
+ let module Jibc = Jib_compile.Make(SMT_config) in
+ let ctx = Jib_compile.(initial_ctx (add_special_functions env)) in
let t = Profile.start () in
- let cdefs, ctx =
- compile_ast { ctx with specialize_calls = true;
- ignore_64 = true;
- unroll_loops = Some !opt_unroll_limit;
- struct_value = true;
- use_real = true } ast in
+ let cdefs, ctx = Jibc.compile_ast ctx ast in
Profile.finish "Compiling to Jib IR" t;
cdefs, ctx
in
diff --git a/src/jib/jib_smt_fuzz.ml b/src/jib/jib_smt_fuzz.ml
index bf49a383..58665bde 100644
--- a/src/jib/jib_smt_fuzz.ml
+++ b/src/jib/jib_smt_fuzz.ml
@@ -152,7 +152,7 @@ let rec run frame =
exception Skip_iteration of string;;
let fuzz_cdef ctx all_cdefs = function
- | CDEF_spec (id, arg_ctyps, ret_ctyp) when not (string_of_id id = "and_bool" || string_of_id id = "or_bool") ->
+ | CDEF_spec (id, _, arg_ctyps, ret_ctyp) when not (string_of_id id = "and_bool" || string_of_id id = "or_bool") ->
let open Type_check in
let open Interpreter in
if Env.is_extern id ctx.tc_env "smt" then (
diff --git a/src/jib/jib_util.ml b/src/jib/jib_util.ml
index 821cdabc..414ad284 100644
--- a/src/jib/jib_util.ml
+++ b/src/jib/jib_util.ml
@@ -356,13 +356,12 @@ let rec string_of_value = function
| 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_unit -> "()"
+ | VL_bit Sail2_values.B0 -> "bitzero"
+ | VL_bit Sail2_values.B1 -> "bitone"
| VL_bit Sail2_values.BU -> failwith "Undefined bit found in value"
| VL_real str -> str
| VL_string str -> "\"" ^ str ^ "\""
- | VL_matcher (n, uid) -> Printf.sprintf "matcher(%d, %d)" n uid
| VL_tuple values -> "(" ^ Util.string_of_list ", " string_of_value values ^ ")"
| VL_list [] -> "NULL"
| VL_list values -> "[|" ^ Util.string_of_list ", " string_of_value values ^ "|]"
@@ -728,7 +727,7 @@ let rec concatmap_instr f (I_aux (instr, aux)) =
I_try_block (List.concat (List.map (concatmap_instr f) instrs))
in
f (I_aux (instr, aux))
-
+
(** Iterate over each instruction within an instruction, bottom-up *)
let rec iter_instr f (I_aux (instr, aux)) =
match instr with
@@ -748,7 +747,7 @@ let cdef_map_instr f = function
| CDEF_fundef (id, heap_return, args, instrs) -> CDEF_fundef (id, heap_return, args, List.map (map_instr f) instrs)
| CDEF_startup (id, instrs) -> CDEF_startup (id, List.map (map_instr f) instrs)
| CDEF_finish (id, instrs) -> CDEF_finish (id, List.map (map_instr f) instrs)
- | CDEF_spec (id, ctyps, ctyp) -> CDEF_spec (id, ctyps, ctyp)
+ | CDEF_spec (id, extern, ctyps, ctyp) -> CDEF_spec (id, extern, ctyps, ctyp)
| CDEF_type tdef -> CDEF_type tdef
(** Map over each instruction in a cdef using concatmap_instr *)
@@ -763,7 +762,7 @@ let cdef_concatmap_instr f = function
CDEF_startup (id, List.concat (List.map (concatmap_instr f) instrs))
| CDEF_finish (id, instrs) ->
CDEF_finish (id, List.concat (List.map (concatmap_instr f) instrs))
- | CDEF_spec (id, ctyps, ctyp) -> CDEF_spec (id, ctyps, ctyp)
+ | CDEF_spec (id, extern, ctyps, ctyp) -> CDEF_spec (id, extern, ctyps, ctyp)
| CDEF_type tdef -> CDEF_type tdef
let ctype_def_map_ctyp f = function
@@ -778,7 +777,7 @@ let cdef_map_ctyp f = function
| CDEF_fundef (id, heap_return, args, instrs) -> CDEF_fundef (id, heap_return, args, List.map (map_instr_ctyp f) instrs)
| CDEF_startup (id, instrs) -> CDEF_startup (id, List.map (map_instr_ctyp f) instrs)
| CDEF_finish (id, instrs) -> CDEF_finish (id, List.map (map_instr_ctyp f) instrs)
- | CDEF_spec (id, ctyps, ctyp) -> CDEF_spec (id, List.map f ctyps, f ctyp)
+ | CDEF_spec (id, extern, ctyps, ctyp) -> CDEF_spec (id, extern, List.map f ctyps, f ctyp)
| CDEF_type tdef -> CDEF_type (ctype_def_map_ctyp f tdef)
(* Map over all sequences of instructions contained within an instruction *)
@@ -977,7 +976,7 @@ let ctype_def_ctyps = function
let cdef_ctyps = function
| CDEF_reg_dec (_, ctyp, instrs) ->
CTSet.add ctyp (instrs_ctyps instrs)
- | CDEF_spec (_, ctyps, ctyp) ->
+ | CDEF_spec (_, _, ctyps, ctyp) ->
CTSet.add ctyp (List.fold_left (fun m ctyp -> CTSet.add ctyp m) CTSet.empty ctyps)
| CDEF_fundef (_, _, _, instrs) | CDEF_startup (_, instrs) | CDEF_finish (_, instrs) ->
instrs_ctyps instrs
diff --git a/src/value2.lem b/src/value2.lem
index a334ac58..ec0cd5a8 100644
--- a/src/value2.lem
+++ b/src/value2.lem
@@ -61,7 +61,6 @@ type vl =
| VL_string of string
| VL_real of string
| VL_tuple of list vl
- | VL_matcher of int * int
| VL_list of list vl
| VL_enum of string
| VL_ref of string
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 23:01:25 +0000