Use unbound precision big_ints throughout sail.

Alastair's test cases revealed that using regular ints causes issues
throughout sail, where all kinds of things can internally overflow in
edge cases. This either causes crashes (e.g. int_of_string fails for
big ints) or bizarre inexplicable behaviour. This patch switches the
sail AST to use big_int rather than int, and updates everything
accordingly.

This touches everything and there may be bugs where I mistranslated
things, and also n = m will still typecheck with big_ints but fail at
runtime (ocaml seems to have decided that static typing is unnecessary
for equality...), as it needs to be changed to eq_big_int.

I also got rid of the old unused ocaml backend while I was updating
things, so as to not have to fix it.

1 files changed, 10 insertions, 10 deletions

diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml
index 379b3a15..a91a6f08 100644
--- a/src/pretty_print_lem_ast.ml
+++ b/src/pretty_print_lem_ast.ml
@@ -70,11 +70,11 @@ let base ppf s = fprintf ppf "%s" s
 let quot_string ppf s = fprintf ppf "\"%s\"" s
 
 let lemnum default n =
-  if 0 <= n && n <= 128 then
-    "int" ^ string_of_int n
-  else if n >= 0 then
+  if le_big_int zero_big_int n && le_big_int n (big_int_of_int 128) then
+    "int" ^ string_of_big_int n
+  else if ge_big_int n zero_big_int then
     default n
-  else ("(zero - " ^ (default (abs n)) ^ ")")
+  else ("(zero - " ^ (default (abs_big_int n)) ^ ")")
 
 let pp_format_id (Id_aux(i,_)) =
   match i with
@@ -143,7 +143,7 @@ and pp_format_nexp_lem (Nexp_aux(n,l)) =
   (match n with
    | Nexp_id(i) -> "(Nexp_id " ^ pp_format_id_lem i ^ ")"
    | Nexp_var(v) -> "(Nexp_var " ^ pp_format_var_lem v ^ ")"
-   | Nexp_constant(i) -> "(Nexp_constant " ^ (lemnum string_of_int i) ^ ")"
+   | Nexp_constant(i) -> "(Nexp_constant " ^ (lemnum string_of_big_int i) ^ ")"
    | Nexp_sum(n1,n2) -> "(Nexp_sum " ^ (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")"
    | Nexp_minus(n1,n2) -> "(Nexp_minus " ^ (pp_format_nexp_lem n1)^ " " ^ (pp_format_nexp_lem n2) ^ ")"
    | Nexp_times(n1,n2) -> "(Nexp_times " ^  (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")"
@@ -207,7 +207,7 @@ and pp_format_nexp_constraint_lem (NC_aux(nc,l)) =
   | NC_set(id,bounds) -> "(NC_set " ^
     pp_format_var_lem id ^
       " [" ^
-      list_format "; " string_of_int bounds ^
+      list_format "; " string_of_big_int bounds ^
       "])") ^ " " ^
   (pp_format_l_lem l) ^ ")"
 
@@ -270,7 +270,7 @@ let pp_format_lit_lem (L_aux(lit,l)) =
   | L_one -> "L_one"
   | L_true -> "L_true"
   | L_false -> "L_false"
-  | L_num(i) -> "(L_num " ^ (lemnum string_of_int i) ^ ")"
+  | L_num(i) -> "(L_num " ^ (lemnum string_of_big_int i) ^ ")"
   | L_hex(n) -> "(L_hex \"" ^ n ^ "\")"
   | L_bin(n) -> "(L_bin \"" ^ n ^ "\")"
   | L_undef -> "L_undef"
@@ -519,8 +519,8 @@ let pp_lem_namescm ppf (Name_sect_aux(ns,l)) =
 
 let rec pp_lem_range ppf (BF_aux(r,l)) =
   match r with
-  | BF_single(i) -> fprintf ppf "(BF_aux (BF_single %i) %a)" i pp_lem_l l
-  | BF_range(i1,i2) -> fprintf ppf "(BF_aux (BF_range %i %i) %a)" i1 i2 pp_lem_l l
+  | BF_single(i) -> fprintf ppf "(BF_aux (BF_single %i) %a)" (int_of_big_int i) pp_lem_l l
+  | BF_range(i1,i2) -> fprintf ppf "(BF_aux (BF_range %i %i) %a)" (int_of_big_int i1) (int_of_big_int i2) pp_lem_l l
   | BF_concat(ir1,ir2) -> fprintf ppf "(BF_aux (BF_concat %a %a) %a)" pp_lem_range ir1 pp_lem_range ir2 pp_lem_l l
 
 let pp_lem_typdef ppf (TD_aux(td,(l,annot))) =
@@ -627,7 +627,7 @@ let pp_lem_def ppf d =
   | DEF_val(lbind) -> fprintf ppf "(DEF_val %a);@\n" pp_lem_let lbind
   | DEF_reg_dec(dec) -> fprintf ppf "(DEF_reg_dec %a);@\n" pp_lem_dec dec
   | DEF_comm d -> fprintf ppf ""
-  | DEF_fixity (prec, n, id) -> fprintf ppf "(DEF_fixity %a %s %a);@\n" pp_lem_prec prec (lemnum string_of_int n) pp_lem_id id
+  | DEF_fixity (prec, n, id) -> fprintf ppf "(DEF_fixity %a %s %a);@\n" pp_lem_prec prec (lemnum string_of_big_int n) pp_lem_id id
   | _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "initial_check didn't remove all scattered Defs")
 
 let pp_lem_defs ppf (Defs(defs)) =