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/ast_util.mli | |
| 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/ast_util.mli')
| -rw-r--r-- | src/ast_util.mli | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/ast_util.mli b/src/ast_util.mli index 8f8a2889..2059bb7f 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -43,6 +43,7 @@ (**************************************************************************) open Ast +open Big_int val no_annot : unit annot @@ -110,7 +111,8 @@ val mk_effect : base_effect_aux list -> effect val nexp_simp : nexp -> nexp (* Utilities for building n-expressions *) -val nconstant : int -> nexp +val nconstant : big_int -> nexp +val nint : int -> nexp val nminus : nexp -> nexp -> nexp val nsum : nexp -> nexp -> nexp val ntimes : nexp -> nexp -> nexp @@ -129,7 +131,7 @@ val nc_and : n_constraint -> n_constraint -> n_constraint val nc_or : n_constraint -> n_constraint -> n_constraint val nc_true : n_constraint val nc_false : n_constraint -val nc_set : kid -> int list -> n_constraint +val nc_set : kid -> big_int list -> n_constraint (* Negate a n_constraint. Note that there's no NC_not constructor, so this flips all the inequalites a the n_constraint leaves and uses |