From 38656b50ad24df6a29f3a84e50adfcf409131fb0 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Fri, 22 Feb 2019 20:50:16 +0000 Subject: Generalize CT_int64 for arbitrary fixed size integers If we want to use our low-level intermediate representation to generate SMT, then we want to be more precise than just splitting integers into 64-bits and larger. This commit changes CT_int and CT_int64 into CT_lint for large integers and CT_fint n for (signed) fixed precision integers that fit within n bits. This follows the convention for bitvectors where we have CT_fbits for fixed-length bitvectors and CT_lbits for large arbitrary precision bitvectors. --- language/bytecode.ott | 4 +-- src/bytecode_util.ml | 22 ++++++++-------- src/c_backend.ml | 73 ++++++++++++++++++++++++++------------------------- 3 files changed, 50 insertions(+), 49 deletions(-) diff --git a/language/bytecode.ott b/language/bytecode.ott index d2580e8c..cc329e02 100644 --- a/language/bytecode.ott +++ b/language/bytecode.ott @@ -66,7 +66,7 @@ fragment :: 'F_' ::= ctyp :: 'CT_' ::= {{ com C type }} - | mpz_t :: :: int + | mpz_t :: :: lint % Arbitrary precision GMP integer, mpz_t in C. | bv_t ( bool ) :: :: lbits % Variable length bitvector - flag represents direction, true - dec or false - inc @@ -75,7 +75,7 @@ ctyp :: 'CT_' ::= | 'uint64_t' ( nat , bool ) :: :: fbits % Fixed length bitvector that fits within a 64-bit word. - int % represents length, and flag is the same as CT_bv. - | 'int64_t' :: :: int64 + | 'int64_t' nat :: :: fint % Used for (signed) integers that fit within 64-bits. | unit_t :: :: unit % unit is a value in sail, so we represent it as a one element type diff --git a/src/bytecode_util.ml b/src/bytecode_util.ml index 3ced48b6..489bcc64 100644 --- a/src/bytecode_util.ml +++ b/src/bytecode_util.ml @@ -252,14 +252,14 @@ and string_of_fragment' ?zencode:(zencode=true) f = (* String representation of ctyps here is only for debugging and intermediate language pretty-printer. *) and string_of_ctyp = function - | CT_int -> "int" + | CT_lint -> "int" | CT_lbits true -> "lbits(dec)" | CT_lbits false -> "lbits(inc)" | CT_fbits (n, true) -> "fbits(" ^ string_of_int n ^ ", dec)" | CT_fbits (n, false) -> "fbits(" ^ string_of_int n ^ ", int)" | CT_sbits true -> "sbits(dec)" | CT_sbits false -> "sbits(inc)" - | CT_int64 -> "int64" + | CT_fint n -> "int(" ^ string_of_int n ^ ")" | CT_bit -> "bit" | CT_unit -> "unit" | CT_bool -> "bool" @@ -276,14 +276,14 @@ and string_of_ctyp = function (** This function is like string_of_ctyp, but recursively prints all constructors in variants and structs. Used for debug output. *) and full_string_of_ctyp = function - | CT_int -> "int" + | CT_lint -> "int" | CT_lbits true -> "lbits(dec)" | CT_lbits false -> "lbits(inc)" | CT_fbits (n, true) -> "fbits(" ^ string_of_int n ^ ", dec)" | CT_fbits (n, false) -> "fbits(" ^ string_of_int n ^ ", int)" | CT_sbits true -> "sbits(dec)" | CT_sbits false -> "sbits(inc)" - | CT_int64 -> "int64" + | CT_fint n -> "int(" ^ string_of_int n ^ ")" | CT_bit -> "bit" | CT_unit -> "unit" | CT_bool -> "bool" @@ -303,7 +303,7 @@ and full_string_of_ctyp = function | CT_poly -> "*" let rec map_ctyp f = function - | (CT_int | CT_int64 | CT_lbits _ | CT_fbits _ | CT_sbits _ + | (CT_lint | CT_fint _ | CT_lbits _ | CT_fbits _ | CT_sbits _ | CT_bit | CT_unit | CT_bool | CT_real | CT_string | CT_poly | CT_enum _) as ctyp -> f ctyp | CT_tup ctyps -> f (CT_tup (List.map (map_ctyp f) ctyps)) | CT_ref ctyp -> f (CT_ref (map_ctyp f ctyp)) @@ -314,12 +314,12 @@ let rec map_ctyp f = function let rec ctyp_equal ctyp1 ctyp2 = match ctyp1, ctyp2 with - | CT_int, CT_int -> true + | CT_lint, CT_lint -> true | CT_lbits d1, CT_lbits d2 -> d1 = d2 | CT_sbits d1, CT_sbits d2 -> d1 = d2 | CT_fbits (m1, d1), CT_fbits (m2, d2) -> m1 = m2 && d1 = d2 | CT_bit, CT_bit -> true - | CT_int64, CT_int64 -> true + | CT_fint n, CT_fint m -> n = m | CT_unit, CT_unit -> true | CT_bool, CT_bool -> true | CT_struct (id1, _), CT_struct (id2, _) -> Id.compare id1 id2 = 0 @@ -353,11 +353,11 @@ let rec ctyp_unify ctyp1 ctyp2 = | _, _ -> raise (Invalid_argument "ctyp_unify") let rec ctyp_suprema = function - | CT_int -> CT_int + | CT_lint -> CT_lint | CT_lbits d -> CT_lbits d | CT_fbits (_, d) -> CT_lbits d | CT_sbits d -> CT_lbits d - | CT_int64 -> CT_int + | CT_fint _ -> CT_lint | CT_unit -> CT_unit | CT_bool -> CT_bool | CT_real -> CT_real @@ -382,7 +382,7 @@ let rec ctyp_ids = function IdSet.add id (List.fold_left (fun ids (_, ctyp) -> IdSet.union (ctyp_ids ctyp) ids) IdSet.empty ctors) | CT_tup ctyps -> List.fold_left (fun ids ctyp -> IdSet.union (ctyp_ids ctyp) ids) IdSet.empty ctyps | CT_vector (_, ctyp) | CT_list ctyp | CT_ref ctyp -> ctyp_ids ctyp - | CT_int | CT_int64 | CT_lbits _ | CT_fbits _ | CT_sbits _ | CT_unit + | CT_lint | CT_fint _ | CT_lbits _ | CT_fbits _ | CT_sbits _ | CT_unit | CT_bool | CT_real | CT_bit | CT_string | CT_poly -> IdSet.empty let rec unpoly = function @@ -394,7 +394,7 @@ let rec unpoly = function | f -> f let rec is_polymorphic = function - | CT_int | CT_int64 | CT_lbits _ | CT_fbits _ | CT_sbits _ | CT_bit | CT_unit | CT_bool | CT_real | CT_string -> false + | CT_lint | CT_fint _ | CT_lbits _ | CT_fbits _ | CT_sbits _ | CT_bit | CT_unit | CT_bool | CT_real | CT_string -> false | CT_tup ctyps -> List.exists is_polymorphic ctyps | CT_enum _ -> false | CT_struct (_, ctors) | CT_variant (_, ctors) -> List.exists (fun (_, ctyp) -> is_polymorphic ctyp) ctors diff --git a/src/c_backend.ml b/src/c_backend.ml index 3b289572..aff2d49e 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -135,8 +135,8 @@ let rec ctyp_of_typ ctx typ = 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_int - | Typ_id id when string_of_id id = "nat" -> CT_int + | 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 @@ -152,13 +152,13 @@ let rec ctyp_of_typ ctx typ = match nexp_simp n, nexp_simp m with | Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_constant m, _) when Big_int.less_equal min_int64 n && Big_int.less_equal m max_int64 -> - CT_int64 + CT_fint 64 | n, m when ctx.optimize_smt -> if prove __POS__ ctx.local_env (nc_lteq (nconstant min_int64) n) && prove __POS__ ctx.local_env (nc_lteq m (nconstant max_int64)) then - CT_int64 + CT_fint 64 else - CT_int - | _ -> CT_int + CT_lint + | _ -> CT_lint end | Typ_app (id, [A_aux (A_typ typ, _)]) when string_of_id id = "list" -> @@ -214,8 +214,9 @@ let rec ctyp_of_typ ctx typ = | _ -> c_error ~loc:l ("No C type for type " ^ string_of_typ typ) let rec is_stack_ctyp ctyp = match ctyp with - | CT_fbits _ | CT_sbits _ | CT_int64 | CT_bit | CT_unit | CT_bool | CT_enum _ -> true - | CT_lbits _ | CT_int | CT_real | CT_string | CT_list _ | CT_vector _ -> false + | CT_fbits _ | CT_sbits _ | CT_bit | CT_unit | CT_bool | CT_enum _ -> true + | CT_fint n -> n <= 64 + | CT_lbits _ | CT_lint | CT_real | CT_string | CT_list _ | CT_vector _ -> false | CT_struct (_, fields) -> List.for_all (fun (_, ctyp) -> is_stack_ctyp ctyp) fields | CT_variant (_, ctors) -> false (* List.for_all (fun (_, ctyp) -> is_stack_ctyp ctyp) ctors *) (* FIXME *) | CT_tup ctyps -> List.for_all is_stack_ctyp ctyps @@ -264,7 +265,7 @@ let hex_char = let literal_to_fragment (L_aux (l_aux, _) as lit) = match l_aux with | L_num n when Big_int.less_equal min_int64 n && Big_int.less_equal n max_int64 -> - Some (F_lit (V_int n), CT_int64) + Some (F_lit (V_int n), CT_fint 64) | L_hex str when String.length str <= 16 -> let padding = 16 - String.length str in let padding = Util.list_init padding (fun _ -> Sail2_values.B0) in @@ -399,7 +400,7 @@ let rec analyze_functions ctx f (AE_aux (aexp, env, l)) = 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_int64) ctx.locals } in + 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) -> @@ -544,14 +545,14 @@ let analyze_primop' ctx id args typ = match nexp_simp n, nexp_simp m with | Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_constant m, _) when Big_int.less_equal min_int64 n && Big_int.less_equal m max_int64 -> - AE_val (AV_C_fragment (F_op (op1, "+", op2), typ, CT_int64)) + AE_val (AV_C_fragment (F_op (op1, "+", op2), typ, CT_fint 64)) | n, m when prove __POS__ ctx.local_env (nc_lteq (nconstant min_int64) n) && prove __POS__ ctx.local_env (nc_lteq m (nconstant max_int64)) -> - AE_val (AV_C_fragment (F_op (op1, "+", op2), typ, CT_int64)) + AE_val (AV_C_fragment (F_op (op1, "+", op2), typ, CT_fint 64)) | _ -> no_change end | "neg_int", [AV_C_fragment (frag, _, _)] -> - AE_val (AV_C_fragment (F_op (v_int 0, "-", frag), typ, CT_int64)) + AE_val (AV_C_fragment (F_op (v_int 0, "-", frag), typ, CT_fint 64)) | "replicate_bits", [AV_C_fragment (vec, vtyp, _); AV_C_fragment (times, _, _)] -> begin match destruct_vector ctx.tc_env typ, destruct_vector ctx.tc_env vtyp with @@ -738,15 +739,15 @@ let rec compile_aval l ctx = function | AV_lit (L_aux (L_num n, _), typ) when Big_int.less_equal min_int64 n && Big_int.less_equal n max_int64 -> let gs = gensym () in - [iinit CT_int gs (F_lit (V_int n), CT_int64)], - (F_id gs, CT_int), - [iclear CT_int gs] + [iinit CT_lint gs (F_lit (V_int n), CT_fint 64)], + (F_id gs, CT_lint), + [iclear CT_lint gs] | AV_lit (L_aux (L_num n, _), typ) -> let gs = gensym () in - [iinit CT_int gs (F_lit (V_string (Big_int.to_string n)), CT_string)], - (F_id gs, CT_int), - [iclear CT_int gs] + [iinit CT_lint gs (F_lit (V_string (Big_int.to_string n)), CT_string)], + (F_id gs, CT_lint), + [iclear CT_lint gs] | AV_lit (L_aux (L_zero, _), _) -> [], (F_lit (V_bit Sail2_values.B0), CT_bit), [] | AV_lit (L_aux (L_one, _), _) -> [], (F_lit (V_bit Sail2_values.B1), CT_bit), [] @@ -870,11 +871,11 @@ let rec compile_aval l ctx = function setup @ [iextern (CL_id (gs, vector_ctyp)) (mk_id "internal_vector_update") - [(F_id gs, vector_ctyp); (F_lit (V_int (Big_int.of_int i)), CT_int64); cval]] + [(F_id gs, vector_ctyp); (F_lit (V_int (Big_int.of_int i)), CT_fint 64); cval]] @ cleanup in [idecl vector_ctyp gs; - iextern (CL_id (gs, vector_ctyp)) (mk_id "internal_vector_init") [(F_lit (V_int (Big_int.of_int len)), CT_int64)]] + iextern (CL_id (gs, vector_ctyp)) (mk_id "internal_vector_init") [(F_lit (V_int (Big_int.of_int len)), CT_fint 64)]] @ List.concat (List.mapi aval_set (if direction then List.rev avals else avals)), (F_id gs, vector_ctyp), [iclear vector_ctyp gs] @@ -1342,8 +1343,8 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = cleanup | AE_for (loop_var, loop_from, loop_to, loop_step, Ord_aux (ord, _), body) -> - (* We assume that all loop indices are safe to put in a CT_int64. *) - let ctx = { ctx with locals = Bindings.add loop_var (Immutable, CT_int64) ctx.locals } in + (* We assume that all loop indices are safe to put in a CT_fint. *) + let ctx = { ctx with locals = Bindings.add loop_var (Immutable, CT_fint 64) ctx.locals } in let is_inc = match ord with | Ord_inc -> true @@ -1359,8 +1360,8 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = let step_setup, step_call, step_cleanup = compile_aexp ctx loop_step in let step_gs = gensym () in let variable_init gs setup call cleanup = - [idecl CT_int64 gs; - iblock (setup @ [call (CL_id (gs, CT_int64))] @ cleanup)] + [idecl (CT_fint 64) gs; + iblock (setup @ [call (CL_id (gs, CT_fint 64))] @ cleanup)] in let loop_start_label = label "for_start_" in @@ -1371,16 +1372,16 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = variable_init from_gs from_setup from_call from_cleanup @ variable_init to_gs to_setup to_call to_cleanup @ variable_init step_gs step_setup step_call step_cleanup - @ [iblock ([idecl CT_int64 loop_var; - icopy l (CL_id (loop_var, CT_int64)) (F_id from_gs, CT_int64); + @ [iblock ([idecl (CT_fint 64) loop_var; + icopy l (CL_id (loop_var, (CT_fint 64))) (F_id from_gs, (CT_fint 64)); idecl CT_unit body_gs; iblock ([ilabel loop_start_label] @ [ijump (F_op (F_id loop_var, (if is_inc then ">" else "<"), F_id to_gs), CT_bool) loop_end_label] @ body_setup @ [body_call (CL_id (body_gs, CT_unit))] @ body_cleanup - @ [icopy l (CL_id (loop_var, CT_int64)) - (F_op (F_id loop_var, (if is_inc then "+" else "-"), F_id step_gs), CT_int64)] + @ [icopy l (CL_id (loop_var, (CT_fint 64))) + (F_op (F_id loop_var, (if is_inc then "+" else "-"), F_id step_gs), (CT_fint 64))] @ [igoto loop_start_label]); ilabel loop_end_label])], (fun clexp -> icopy l clexp unit_fragment), @@ -1888,7 +1889,7 @@ let rec instrs_rename from_id to_id = | [] -> [] let hoist_ctyp = function - | CT_int | CT_lbits _ | CT_struct _ -> true + | CT_lint | CT_lbits _ | CT_struct _ -> true | _ -> false let hoist_counter = ref 0 @@ -2420,8 +2421,8 @@ let rec sgen_ctyp = function | CT_bool -> "bool" | CT_fbits _ -> "fbits" | CT_sbits _ -> "sbits" - | CT_int64 -> "mach_int" - | CT_int -> "sail_int" + | CT_fint _ -> "mach_int" + | CT_lint -> "sail_int" | CT_lbits _ -> "lbits" | CT_tup _ as tup -> "struct " ^ Util.zencode_string ("tuple_" ^ string_of_ctyp tup) | CT_struct (id, _) -> "struct " ^ sgen_id id @@ -2440,8 +2441,8 @@ let rec sgen_ctyp_name = function | CT_bool -> "bool" | CT_fbits _ -> "fbits" | CT_sbits _ -> "sbits" - | CT_int64 -> "mach_int" - | CT_int -> "sail_int" + | CT_fint _ -> "mach_int" + | CT_lint -> "sail_int" | CT_lbits _ -> "lbits" | CT_tup _ as tup -> Util.zencode_string ("tuple_" ^ string_of_ctyp tup) | CT_struct (id, _) -> sgen_id id @@ -2657,7 +2658,7 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) = match ctyp with | CT_unit -> "UNIT", [] | CT_bit -> "UINT64_C(0)", [] - | CT_int64 -> "INT64_C(0xdeadc0de)", [] + | CT_fint _ -> "INT64_C(0xdeadc0de)", [] | CT_fbits _ -> "UINT64_C(0xdeadc0de)", [] | CT_sbits _ -> "undefined_sbits()", [] | CT_bool -> "false", [] @@ -3275,7 +3276,7 @@ let rec ctyp_dependencies = function | 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_int | CT_int64 | CT_lbits _ | CT_fbits _ | CT_sbits _ | CT_unit | CT_bool | CT_real | CT_bit | CT_string | CT_enum _ | CT_poly -> [] + | CT_lint | CT_fint _ | CT_lbits _ | CT_fbits _ | CT_sbits _ | CT_unit | CT_bool | CT_real | CT_bit | CT_string | CT_enum _ | CT_poly -> [] let codegen_ctg ctx = function | CTG_vector (direction, ctyp) -> codegen_vector ctx (direction, ctyp) -- cgit v1.2.3