diff options
| author | Alasdair Armstrong | 2017-11-24 20:25:26 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2017-11-24 20:25:26 +0000 |
| commit | 381071686f99aabdc8d618051b1b63d5aeb0108c (patch) | |
| tree | eb488e0f80a76ca2699a4e5118a0c08c2ed01b69 /src/pretty_print_sail2.ml | |
| parent | a1b47ed3bf5c6a4cf4d61b119c73e4fd50bea6d0 (diff) | |
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.
Diffstat (limited to 'src/pretty_print_sail2.ml')
| -rw-r--r-- | src/pretty_print_sail2.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/src/pretty_print_sail2.ml b/src/pretty_print_sail2.ml index 56560de2..e354fe58 100644 --- a/src/pretty_print_sail2.ml +++ b/src/pretty_print_sail2.ml @@ -1,6 +1,7 @@ open Ast open Ast_util +open Big_int open PPrint let doc_op symb a b = infix 2 1 symb a b @@ -12,7 +13,7 @@ let doc_id (Id_aux (id_aux, _)) = let doc_kid kid = string (Ast_util.string_of_kid kid) -let doc_int n = string (string_of_int n) +let doc_int n = string (string_of_big_int n) let doc_ord (Ord_aux(o,_)) = match o with | Ord_var v -> doc_kid v @@ -22,7 +23,7 @@ let doc_ord (Ord_aux(o,_)) = match o with let rec doc_nexp = let rec atomic_nexp (Nexp_aux (n_aux, _) as nexp) = match n_aux with - | Nexp_constant c -> string (string_of_int c) + | Nexp_constant c -> string (string_of_big_int c) | Nexp_id id -> doc_id id | Nexp_var kid -> doc_kid kid | _ -> parens (nexp0 nexp) @@ -30,8 +31,8 @@ let rec doc_nexp = match n_aux with | Nexp_sum (n1, Nexp_aux (Nexp_neg n2, _)) | Nexp_minus (n1, n2) -> separate space [nexp0 n1; string "-"; nexp1 n2] - | Nexp_sum (n1, Nexp_aux (Nexp_constant c, _)) when c < 0 -> - separate space [nexp0 n1; string "-"; doc_int (abs c)] + | Nexp_sum (n1, Nexp_aux (Nexp_constant c, _)) when lt_big_int c zero_big_int -> + separate space [nexp0 n1; string "-"; doc_int (abs_big_int c)] | Nexp_sum (n1, n2) -> separate space [nexp0 n1; string "+"; nexp1 n2] | _ -> nexp1 nexp and nexp1 (Nexp_aux (n_aux, _) as nexp) = @@ -143,7 +144,7 @@ let doc_lit (L_aux(l,_)) = | L_one -> "bitone" | L_true -> "true" | L_false -> "false" - | L_num i -> string_of_int i + | L_num i -> string_of_big_int i | L_hex n -> "0x" ^ n | L_bin n -> "0b" ^ n | L_real r -> r @@ -216,7 +217,7 @@ let rec doc_exp (E_aux (e_aux, _) as exp) = | E_try (exp, pexps) -> assert false | E_return exp -> string "return" ^^ parens (doc_exp exp) | E_app (id, [exp]) when Id.compare (mk_id "pow2") id == 0 -> - separate space [doc_int 2; string "^"; doc_atomic_exp exp] + separate space [string "2"; string "^"; doc_atomic_exp exp] | _ -> doc_atomic_exp exp and doc_atomic_exp (E_aux (e_aux, _) as exp) = match e_aux with |