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.

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)