From 381071686f99aabdc8d618051b1b63d5aeb0108c Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Fri, 24 Nov 2017 20:25:26 +0000 Subject: 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. --- src/ast_util.ml | 29 +- src/ast_util.mli | 6 +- src/initial_check.ml | 9 +- src/lexer.mll | 5 +- src/lexer2.mll | 11 +- src/monomorphise.ml | 46 ++- src/ocaml_backend.ml | 2 +- src/parse_ast.ml | 15 +- src/parser.mly | 17 +- src/parser2.mly | 13 +- src/pretty_print.ml | 1 - src/pretty_print.mli | 2 - src/pretty_print_common.ml | 7 +- src/pretty_print_lem.ml | 32 +- src/pretty_print_lem_ast.ml | 20 +- src/pretty_print_ocaml.ml | 705 -------------------------------------------- src/pretty_print_sail.ml | 3 +- src/pretty_print_sail2.ml | 13 +- src/process_file.ml | 10 - src/process_file.mli | 1 - src/rewriter.ml | 70 ++--- src/rewriter.mli | 2 +- src/type_check.ml | 100 +++---- src/type_check.mli | 3 +- 24 files changed, 204 insertions(+), 918 deletions(-) delete mode 100644 src/pretty_print_ocaml.ml (limited to 'src') diff --git a/src/ast_util.ml b/src/ast_util.ml index 7d472891..d26e12ed 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -133,7 +133,7 @@ module Nexp = struct match nexp1, nexp2 with | Nexp_id v1, Nexp_id v2 -> Id.compare v1 v2 | Nexp_var kid1, Nexp_var kid2 -> Kid.compare kid1 kid2 - | Nexp_constant c1, Nexp_constant c2 -> Pervasives.compare c1 c2 + | Nexp_constant c1, Nexp_constant c2 -> compare_big_int c1 c2 | Nexp_times (n1a, n1b), Nexp_times (n2a, n2b) | Nexp_sum (n1a, n1b), Nexp_sum (n2a, n2b) | Nexp_minus (n1a, n1b), Nexp_minus (n2a, n2b) -> @@ -178,7 +178,7 @@ and nexp_simp_aux = function let (Nexp_aux (n1_simp, _) as n1) = nexp_simp n1 in let (Nexp_aux (n2_simp, _) as n2) = nexp_simp n2 in match n1_simp, n2_simp with - | Nexp_constant c1, Nexp_constant c2 -> Nexp_constant (c1 + c2) + | Nexp_constant c1, Nexp_constant c2 -> Nexp_constant (add_big_int c1 c2) | _, Nexp_neg n2 -> Nexp_minus (n1, n2) | _, _ -> Nexp_sum (n1, n2) end @@ -187,9 +187,9 @@ and nexp_simp_aux = function let (Nexp_aux (n1_simp, _) as n1) = nexp_simp n1 in let (Nexp_aux (n2_simp, _) as n2) = nexp_simp n2 in match n1_simp, n2_simp with - | Nexp_constant 1, _ -> n2_simp - | _, Nexp_constant 1 -> n1_simp - | Nexp_constant c1, Nexp_constant c2 -> Nexp_constant (c1 * c2) + | Nexp_constant c, _ when eq_big_int c unit_big_int -> n2_simp + | _, Nexp_constant c when eq_big_int c unit_big_int -> n1_simp + | Nexp_constant c1, Nexp_constant c2 -> Nexp_constant (mult_big_int c1 c2) | _, _ -> Nexp_times (n1, n2) end | Nexp_minus (n1, n2) -> @@ -197,10 +197,10 @@ and nexp_simp_aux = function let (Nexp_aux (n1_simp, _) as n1) = nexp_simp n1 in let (Nexp_aux (n2_simp, _) as n2) = nexp_simp n2 in match n1_simp, n2_simp with - | Nexp_constant c1, Nexp_constant c2 -> Nexp_constant (c1 - c2) + | Nexp_constant c1, Nexp_constant c2 -> Nexp_constant (sub_big_int c1 c2) (* A vector range x['n-1 .. 0] can result in the size "('n-1) - -1" *) | Nexp_minus (Nexp_aux (n,_), Nexp_aux (Nexp_constant c1,_)), Nexp_constant c2 - when c1 = -c2 -> n + when eq_big_int c1 (minus_big_int c2) -> n | _, _ -> Nexp_minus (n1, n2) end | nexp -> nexp @@ -241,6 +241,7 @@ let vector_typ n m ord typ = let exc_typ = mk_id_typ (mk_id "exception") let nconstant c = Nexp_aux (Nexp_constant c, Parse_ast.Unknown) +let nint i = nconstant (big_int_of_int i) let nminus n1 n2 = Nexp_aux (Nexp_minus (n1, n2), Parse_ast.Unknown) let nsum n1 n2 = Nexp_aux (Nexp_sum (n1, n2), Parse_ast.Unknown) let ntimes n1 n2 = Nexp_aux (Nexp_times (n1, n2), Parse_ast.Unknown) @@ -253,8 +254,8 @@ let nc_eq n1 n2 = mk_nc (NC_equal (n1, n2)) let nc_neq n1 n2 = mk_nc (NC_not_equal (n1, n2)) let nc_lteq n1 n2 = NC_aux (NC_bounded_le (n1, n2), Parse_ast.Unknown) let nc_gteq n1 n2 = NC_aux (NC_bounded_ge (n1, n2), Parse_ast.Unknown) -let nc_lt n1 n2 = nc_lteq n1 (nsum n2 (nconstant 1)) -let nc_gt n1 n2 = nc_gteq n1 (nsum n2 (nconstant 1)) +let nc_lt n1 n2 = nc_lteq n1 (nsum n2 (nint 1)) +let nc_gt n1 n2 = nc_gteq n1 (nsum n2 (nint 1)) let nc_and nc1 nc2 = mk_nc (NC_and (nc1, nc2)) let nc_or nc1 nc2 = mk_nc (NC_or (nc1, nc2)) let nc_true = mk_nc NC_true @@ -485,7 +486,7 @@ let rec string_of_nexp = function and string_of_nexp_aux = function | Nexp_id id -> string_of_id id | Nexp_var kid -> string_of_kid kid - | Nexp_constant c -> string_of_int c + | Nexp_constant c -> string_of_big_int c | Nexp_times (n1, n2) -> "(" ^ string_of_nexp n1 ^ " * " ^ string_of_nexp n2 ^ ")" | Nexp_sum (n1, n2) -> "(" ^ string_of_nexp n1 ^ " + " ^ string_of_nexp n2 ^ ")" | Nexp_minus (n1, n2) -> "(" ^ string_of_nexp n1 ^ " - " ^ string_of_nexp n2 ^ ")" @@ -520,7 +521,7 @@ and string_of_n_constraint = function | NC_aux (NC_and (nc1, nc2), _) -> "(" ^ string_of_n_constraint nc1 ^ " & " ^ string_of_n_constraint nc2 ^ ")" | NC_aux (NC_set (kid, ns), _) -> - string_of_kid kid ^ " IN {" ^ string_of_list ", " string_of_int ns ^ "}" + string_of_kid kid ^ " IN {" ^ string_of_list ", " string_of_big_int ns ^ "}" | NC_aux (NC_true, _) -> "true" | NC_aux (NC_false, _) -> "false" @@ -553,7 +554,7 @@ let string_of_lit (L_aux (lit, _)) = | L_one -> "bitone" | L_true -> "true" | L_false -> "false" - | L_num n -> string_of_int n + | L_num n -> string_of_big_int n | L_hex n -> "0x" ^ n | L_bin n -> "0b" ^ n | L_undef -> "undefined" @@ -652,8 +653,8 @@ and string_of_letbind (LB_aux (lb, l)) = let rec string_of_index_range (BF_aux (ir, _)) = match ir with - | BF_single n -> string_of_int n - | BF_range (n, m) -> string_of_int n ^ " .. " ^ string_of_int m + | BF_single n -> string_of_big_int n + | BF_range (n, m) -> string_of_big_int n ^ " .. " ^ string_of_big_int m | BF_concat (ir1, ir2) -> "(" ^ string_of_index_range ir1 ^ ") : (" ^ string_of_index_range ir2 ^ ")" let id_of_fundef (FD_aux (FD_function (_, _, _, funcls), (l, _))) = 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 diff --git a/src/initial_check.ml b/src/initial_check.ml index e80ff9a4..de5b625b 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -43,6 +43,7 @@ open Ast open Util open Ast_util +open Big_int let opt_undefined_gen = ref false @@ -164,12 +165,12 @@ let rec to_ast_typ (k_env : kind Envmap.t) (def_ord : order) (t: Parse_ast.atyp) let make_r bot top = match bot,top with | Parse_ast.ATyp_aux(Parse_ast.ATyp_constant b,_),Parse_ast.ATyp_aux(Parse_ast.ATyp_constant t,l) -> - Parse_ast.ATyp_aux(Parse_ast.ATyp_constant ((t-b)+1),l) + Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (add_big_int (sub_big_int t b) unit_big_int),l) | bot,(Parse_ast.ATyp_aux(_,l) as top) -> Parse_ast.ATyp_aux((Parse_ast.ATyp_sum ((Parse_ast.ATyp_aux (Parse_ast.ATyp_sum (top, - Parse_ast.ATyp_aux(Parse_ast.ATyp_constant 1,Parse_ast.Unknown)), + Parse_ast.ATyp_aux(Parse_ast.ATyp_constant unit_big_int,Parse_ast.Unknown)), Parse_ast.Unknown)), (Parse_ast.ATyp_aux ((Parse_ast.ATyp_neg bot),Parse_ast.Unknown)))), l) in let base = to_ast_nexp k_env b in @@ -185,9 +186,9 @@ let rec to_ast_typ (k_env : kind Envmap.t) (def_ord : order) (t: Parse_ast.atyp) | Parse_ast.ATyp_app(Parse_ast.Id_aux(Parse_ast.Id "vector_sugar_r",il), [b;r;ord;ti]) -> let make_sub_one t = match t with - | Parse_ast.ATyp_aux(Parse_ast.ATyp_constant t,_) -> Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (t-1),l) + | Parse_ast.ATyp_aux(Parse_ast.ATyp_constant t,_) -> Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (sub_big_int t unit_big_int),l) | t -> (Parse_ast.ATyp_aux - (Parse_ast.ATyp_sum (t, Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (-1),Parse_ast.Unknown)), + (Parse_ast.ATyp_sum (t, Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (minus_big_int unit_big_int),Parse_ast.Unknown)), Parse_ast.Unknown)) in let (base,rise) = match def_ord with | Ord_aux(Ord_inc,dl) -> (to_ast_nexp k_env b), (to_ast_nexp k_env r) diff --git a/src/lexer.mll b/src/lexer.mll index fb091f67..3b1a1583 100644 --- a/src/lexer.mll +++ b/src/lexer.mll @@ -42,6 +42,7 @@ { open Parser +open Big_int module M = Map.Make(String) exception LexError of string * Lexing.position @@ -321,8 +322,8 @@ rule token = parse | (digit+ as i1) "." (digit+ as i2) { (Real (i1 ^ "." ^ i2)) } | "-" (digit* as i1) "." (digit+ as i2) { (Real ("-" ^ i1 ^ "." ^ i2)) } - | digit+ as i { (Num(int_of_string i)) } - | "-" digit+ as i { (Num(int_of_string i)) } + | digit+ as i { (Num(big_int_of_string i)) } + | "-" digit+ as i { (Num(big_int_of_string i)) } | "0b" (binarydigit+ as i) { (Bin(i)) } | "0x" (hexdigit+ as i) { (Hex(i)) } | '"' { (String( diff --git a/src/lexer2.mll b/src/lexer2.mll index 1763b3a6..40e7eec6 100644 --- a/src/lexer2.mll +++ b/src/lexer2.mll @@ -42,6 +42,7 @@ { open Parser2 +open Big_int open Parse_ast module M = Map.Make(String) exception LexError of string * Lexing.position @@ -216,13 +217,13 @@ rule token = parse | "<=" { (LtEq(r"<=")) } | "infix" ws (digit as p) ws (operator as op) { operators := M.add op (mk_operator Infix (int_of_string (Char.escaped p)) op) !operators; - Fixity (Infix, int_of_string (Char.escaped p), op) } + Fixity (Infix, big_int_of_string (Char.escaped p), op) } | "infixl" ws (digit as p) ws (operator as op) { operators := M.add op (mk_operator InfixL (int_of_string (Char.escaped p)) op) !operators; - Fixity (InfixL, int_of_string (Char.escaped p), op) } + Fixity (InfixL, big_int_of_string (Char.escaped p), op) } | "infixr" ws (digit as p) ws (operator as op) { operators := M.add op (mk_operator InfixR (int_of_string (Char.escaped p)) op) !operators; - Fixity (InfixR, int_of_string (Char.escaped p), op) } + Fixity (InfixR, big_int_of_string (Char.escaped p), op) } | operator as op { try M.find op !operators with Not_found -> raise (LexError ("Operator fixity undeclared " ^ op, Lexing.lexeme_start_p lexbuf)) } @@ -239,8 +240,8 @@ rule token = parse else Id(r i) } | (digit+ as i1) "." (digit+ as i2) { (Real (i1 ^ "." ^ i2)) } | "-" (digit* as i1) "." (digit+ as i2) { (Real ("-" ^ i1 ^ "." ^ i2)) } - | digit+ as i { (Num(int_of_string i)) } - | "-" digit+ as i { (Num(int_of_string i)) } + | digit+ as i { (Num(big_int_of_string i)) } + | "-" digit+ as i { (Num(big_int_of_string i)) } | "0b" (binarydigit+ as i) { (Bin(i)) } | "0x" (hexdigit+ as i) { (Hex(i)) } | '"' { (String( diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 5c7cf483..79e276e1 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -1,6 +1,7 @@ open Parse_ast open Ast open Ast_util +open Big_int open Type_check let size_set_limit = 8 @@ -87,21 +88,18 @@ let subst_src_typ substs t = in s_styp substs t let make_vector_lit sz i = - let f j = if (i lsr (sz-j-1)) mod 2 = 0 then '0' else '1' in + let f j = if eq_big_int (mod_big_int (shift_right_big_int i (sz-j-1)) (big_int_of_int 2)) zero_big_int then '0' else '1' in let s = String.init sz f in L_aux (L_bin s,Generated Unknown) let tabulate f n = let rec aux acc n = let acc' = f n::acc in - if n = 0 then acc' else aux acc' (n-1) - in if n = 0 then [] else aux [] (n-1) + if eq_big_int n zero_big_int then acc' else aux acc' (sub_big_int n unit_big_int) + in if eq_big_int n zero_big_int then [] else aux [] (sub_big_int n unit_big_int) let make_vectors sz = - tabulate (make_vector_lit sz) (1 lsl sz) - - - + tabulate (make_vector_lit sz) (shift_left_big_int unit_big_int sz) let pat_id_is_variable env id = match Env.lookup_id id env with @@ -364,7 +362,7 @@ let split_src_type id ty (TypQ_aux (q,ql)) = in let name_seg = function | (_,None) -> "" - | (k,Some i) -> string_of_kid k ^ string_of_int i + | (k,Some i) -> string_of_kid k ^ string_of_big_int i in let name l i = String.concat "_" (i::(List.map name_seg l)) in Some (List.map (fun (l,ty) -> (l, wrap (name l),ty)) variants) @@ -373,11 +371,11 @@ let reduce_nexp subst ne = let rec eval (Nexp_aux (ne,_) as nexp) = match ne with | Nexp_constant i -> i - | Nexp_sum (n1,n2) -> (eval n1) + (eval n2) - | Nexp_minus (n1,n2) -> (eval n1) - (eval n2) - | Nexp_times (n1,n2) -> (eval n1) * (eval n2) - | Nexp_exp n -> 1 lsl (eval n) - | Nexp_neg n -> - (eval n) + | Nexp_sum (n1,n2) -> add_big_int (eval n1) (eval n2) + | Nexp_minus (n1,n2) -> sub_big_int (eval n1) (eval n2) + | Nexp_times (n1,n2) -> mult_big_int (eval n1) (eval n2) + | Nexp_exp n -> shift_left_big_int (eval n) 1 + | Nexp_neg n -> minus_big_int (eval n) | _ -> raise (Reporting_basic.err_general Unknown ("Couldn't turn nexp " ^ string_of_nexp nexp ^ " into concrete value")) @@ -575,10 +573,10 @@ let lit_match = function (* There's no undefined nexp, so replace undefined sizes with a plausible size. 32 is used as a sensible default. *) let fabricate_nexp l = function - | None -> Nexp_aux (Nexp_constant 32,Unknown) + | None -> nint 32 | Some (env,typ,_) -> match Type_check.destruct_exist env typ with - | None -> Nexp_aux (Nexp_constant 32,Unknown) + | None -> nint 32 | Some (kids,nc,typ') -> match kids,nc,Env.expand_synonyms env typ' with | ([kid],NC_aux (NC_set (kid',i::_),_), @@ -594,7 +592,7 @@ let fabricate_nexp l = function Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid''',_)),_)]),_)) when Kid.compare kid kid'' = 0 && Kid.compare kid kid''' = 0 -> - Nexp_aux (Nexp_constant 32,Unknown) + nint 32 | _ -> raise (Reporting_basic.err_general l ("Undefined value at unsupported type " ^ string_of_typ typ)) @@ -613,8 +611,8 @@ let rec drop_casts = function (* TODO: ought to be a big int of some form, but would need L_num to be one *) let int_of_lit = function - | L_hex hex -> int_of_string ("0x" ^ hex) - | L_bin bin -> int_of_string ("0b" ^ bin) + | L_hex hex -> big_int_of_string ("0x" ^ hex) + | L_bin bin -> big_int_of_string ("0b" ^ bin) | _ -> assert false let lit_eq (L_aux (l1,_)) (L_aux (l2,_)) = @@ -656,7 +654,7 @@ let try_app (l,ann) (id,args) = else if is_id "shl_int" then match args with | [E_aux (E_lit L_aux (L_num i,_),_); E_aux (E_lit L_aux (L_num j,_),_)] -> - Some (E_aux (E_lit (L_aux (L_num (i lsl j),new_l)),(l,ann))) + Some (E_aux (E_lit (L_aux (L_num (shift_left_big_int i (int_of_big_int j)),new_l)),(l,ann))) | _ -> None else if is_id "ex_int" then match args with @@ -667,8 +665,8 @@ let try_app (l,ann) (id,args) = | [E_aux (E_lit L_aux ((L_hex _ | L_bin _) as lit,_),_); E_aux (E_lit L_aux (L_num i,_),_)] -> let v = int_of_lit lit in - let b = (v lsr i) land 1 in - let lit' = if b = 1 then L_one else L_zero in + let b = and_big_int (shift_right_big_int v (int_of_big_int i)) unit_big_int in + let lit' = if eq_big_int b unit_big_int then L_one else L_zero in Some (E_aux (E_lit (L_aux (lit',new_l)),(l,ann))) | _ -> None else None @@ -1173,14 +1171,14 @@ let split_defs splits defs = | Typ_app (Id_aux (Id "vector",_), [_;Typ_arg_aux (Typ_arg_nexp len,_);_;Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)]) -> (match len with | Nexp_aux (Nexp_constant sz,_) -> - if sz <= vector_split_limit then - let lits = make_vectors sz in + if int_of_big_int sz <= vector_split_limit then + let lits = make_vectors (int_of_big_int sz) in List.map (fun lit -> P_aux (P_lit lit,(l,annot)), [var,E_aux (E_lit lit,(new_l,annot))]) lits else raise (Reporting_basic.err_general l - ("Refusing to split vector type of length " ^ string_of_int sz ^ + ("Refusing to split vector type of length " ^ string_of_big_int sz ^ " above limit " ^ string_of_int vector_split_limit ^ " for variable " ^ v)) | _ -> diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index 5fb0d177..9b8ac56a 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -127,7 +127,7 @@ let ocaml_lit (L_aux (lit_aux, _)) = | L_one -> string "B1" | L_true -> string "true" | L_false -> string "false" - | L_num n -> parens (string "big_int_of_int" ^^ space ^^ string (string_of_int n)) + | L_num n -> parens (string "big_int_of_string" ^^ space ^^ string ("\"" ^ Big_int.string_of_big_int n ^ "\"")) | L_undef -> failwith "undefined should have been re-written prior to ocaml backend" | L_string str -> string_lit str | L_real str -> parens (string "real_of_string" ^^ space ^^ dquotes (string (String.escaped str))) diff --git a/src/parse_ast.ml b/src/parse_ast.ml index fb6c75e1..bdf56cc8 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -42,6 +42,7 @@ (* generated by Ott 0.25 from: l2_parse.ott *) +open Big_int type text = string @@ -130,7 +131,7 @@ type atyp_aux = (* expressions of all kinds, to be translated to types, nats, orders, and effects after parsing *) ATyp_id of id (* identifier *) | ATyp_var of kid (* ticked variable *) - | ATyp_constant of int (* constant *) + | ATyp_constant of big_int (* constant *) | ATyp_times of atyp * atyp (* product *) | ATyp_sum of atyp * atyp (* sum *) | ATyp_minus of atyp * atyp (* subtraction *) @@ -161,7 +162,7 @@ n_constraint_aux = (* constraint over kind $_$ *) | NC_bounded_ge of atyp * atyp | NC_bounded_le of atyp * atyp | NC_not_equal of atyp * atyp - | NC_set of kid * (int) list + | NC_set of kid * (big_int) list | NC_or of n_constraint * n_constraint | NC_and of n_constraint * n_constraint | NC_true @@ -204,7 +205,7 @@ lit_aux = (* Literal constant *) | L_one (* $_ : _$ *) | L_true (* $_ : _$ *) | L_false (* $_ : _$ *) - | L_num of int (* natural number constant *) + | L_num of big_int (* natural number constant *) | L_hex of string (* bit vector constant, C-style *) | L_bin of string (* bit vector constant, C-style *) | L_undef (* undefined value *) @@ -387,8 +388,8 @@ type_union = type index_range_aux = (* index specification, for bitfields in register types *) - BF_single of int (* single index *) - | BF_range of int * int (* index range *) + BF_single of big_int (* single index *) + | BF_range of big_int * big_int (* index range *) | BF_concat of index_range * index_range (* concatenation of index ranges *) and index_range = @@ -483,7 +484,7 @@ scattered_def = type prec = Infix | InfixL | InfixR -type fixity_token = (prec * int * string) +type fixity_token = (prec * big_int * string) type def = (* Top-level definition *) @@ -492,7 +493,7 @@ def = (* Top-level definition *) | DEF_fundef of fundef (* function definition *) | DEF_val of letbind (* value definition *) | DEF_overload of id * id list (* operator overload specifications *) - | DEF_fixity of prec * int * id (* fixity declaration *) + | DEF_fixity of prec * big_int * id (* fixity declaration *) | DEF_spec of val_spec (* top-level type constraint *) | DEF_default of default_typing_spec (* default kind and type assumptions *) | DEF_scattered of scattered_def (* scattered definition *) diff --git a/src/parser.mly b/src/parser.mly index edfc0783..2cfa8e80 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -44,6 +44,7 @@ let r = fun x -> x (* Ulib.Text.of_latin1 *) +open Big_int open Parse_ast let loc () = Range(Parsing.symbol_start_pos(),Parsing.symbol_end_pos()) @@ -99,16 +100,16 @@ let mk_namesectn _ = Name_sect_aux(Name_sect_none,Unknown) let make_range_sugar_bounded typ1 typ2 = ATyp_app(Id_aux(Id("range"),Unknown),[typ1; typ2;]) let make_range_sugar typ1 = - make_range_sugar_bounded (ATyp_aux(ATyp_constant(0), Unknown)) typ1 + make_range_sugar_bounded (ATyp_aux(ATyp_constant(zero_big_int), Unknown)) typ1 let make_atom_sugar typ1 = ATyp_app(Id_aux(Id("atom"),Unknown),[typ1]) let make_r bot top = match bot,top with | ATyp_aux(ATyp_constant b,_),ATyp_aux(ATyp_constant t,l) -> - ATyp_aux(ATyp_constant ((t-b)+1),l) + ATyp_aux(ATyp_constant (add_big_int (sub_big_int t b) unit_big_int),l) | bot,(ATyp_aux(_,l) as top) -> - ATyp_aux((ATyp_sum ((ATyp_aux (ATyp_sum (top, ATyp_aux(ATyp_constant 1,Unknown)), Unknown)), + ATyp_aux((ATyp_sum ((ATyp_aux (ATyp_sum (top, ATyp_aux(ATyp_constant unit_big_int,Unknown)), Unknown)), (ATyp_aux ((ATyp_neg bot),Unknown)))), l) let make_vector_sugar_bounded order_set is_inc name typ typ1 typ2 = @@ -122,11 +123,11 @@ let make_vector_sugar_bounded order_set is_inc name typ typ1 typ2 = else (typ2, ATyp_default_ord,"vector_sugar_r") (* rise and base not calculated, rise only from specification *) in ATyp_app(Id_aux(Id(name),Unknown),[typ1;rise;ATyp_aux(ord,Unknown);typ]) let make_vector_sugar order_set is_inc typ typ1 = - let zero = (ATyp_aux(ATyp_constant 0,Unknown)) in + let zero = (ATyp_aux(ATyp_constant zero_big_int,Unknown)) in let (typ1,typ2) = match (order_set,is_inc,typ1) with - | (true,true,ATyp_aux(ATyp_constant t,l)) -> zero,ATyp_aux(ATyp_constant (t-1),l) + | (true,true,ATyp_aux(ATyp_constant t,l)) -> zero,ATyp_aux(ATyp_constant (sub_big_int t unit_big_int),l) | (true,true,ATyp_aux(_, l)) -> zero,ATyp_aux (ATyp_sum (typ1, - ATyp_aux(ATyp_neg(ATyp_aux(ATyp_constant 1,Unknown)), Unknown)), l) + ATyp_aux(ATyp_neg(ATyp_aux(ATyp_constant unit_big_int,Unknown)), Unknown)), l) | (true,false,_) -> typ1,zero | (false,_,_) -> zero,typ1 in make_vector_sugar_bounded order_set is_inc "vector_sugar_r" typ typ1 typ2 @@ -157,7 +158,7 @@ let make_vector_sugar order_set is_inc typ typ1 = /*Terminals with content*/ %token Id TyVar TyId -%token Num +%token Num %token String Bin Hex Real %token Amp At Carrot Div Eq Excl Gt Lt Plus Star Tilde @@ -685,7 +686,7 @@ right_atomic_exp: raise (Parse_error_locn ((loc ()),"Missing \"from\" in foreach loop")); if $6 <> "to" && $6 <> "downto" then raise (Parse_error_locn ((loc ()),"Missing \"to\" or \"downto\" in foreach loop")); - let step = eloc (E_lit(lloc (L_num 1))) in + let step = eloc (E_lit(lloc (L_num unit_big_int))) in let ord = if $6 = "to" then ATyp_aux(ATyp_inc,(locn 6 6)) diff --git a/src/parser2.mly b/src/parser2.mly index ee8cdfb8..a752e5c1 100644 --- a/src/parser2.mly +++ b/src/parser2.mly @@ -44,6 +44,7 @@ let r = fun x -> x (* Ulib.Text.of_latin1 *) +open Big_int open Parse_ast let loc n m = Range (n, m) @@ -104,12 +105,12 @@ let rec desugar_lchain chain s e = | [LC_nexp n1; LC_lteq; LC_nexp n2] -> mk_nc (NC_bounded_le (n1, n2)) s e | [LC_nexp n1; LC_lt; LC_nexp n2] -> - mk_nc (NC_bounded_le (mk_typ (ATyp_sum (n1, mk_typ (ATyp_constant 1) s e)) s e, n2)) s e + mk_nc (NC_bounded_le (mk_typ (ATyp_sum (n1, mk_typ (ATyp_constant unit_big_int) s e)) s e, n2)) s e | (LC_nexp n1 :: LC_lteq :: LC_nexp n2 :: chain) -> let nc1 = mk_nc (NC_bounded_le (n1, n2)) s e in mk_nc (NC_and (nc1, desugar_lchain (LC_nexp n2 :: chain) s e)) s e | (LC_nexp n1 :: LC_lt :: LC_nexp n2 :: chain) -> - let nc1 = mk_nc (NC_bounded_le (mk_typ (ATyp_sum (n1, mk_typ (ATyp_constant 1) s e)) s e, n2)) s e in + let nc1 = mk_nc (NC_bounded_le (mk_typ (ATyp_sum (n1, mk_typ (ATyp_constant unit_big_int) s e)) s e, n2)) s e in mk_nc (NC_and (nc1, desugar_lchain (LC_nexp n2 :: chain) s e)) s e | _ -> assert false @@ -123,12 +124,12 @@ let rec desugar_rchain chain s e = | [RC_nexp n1; RC_gteq; RC_nexp n2] -> mk_nc (NC_bounded_ge (n1, n2)) s e | [RC_nexp n1; RC_gt; RC_nexp n2] -> - mk_nc (NC_bounded_ge (n1, mk_typ (ATyp_sum (n2, mk_typ (ATyp_constant 1) s e)) s e)) s e + mk_nc (NC_bounded_ge (n1, mk_typ (ATyp_sum (n2, mk_typ (ATyp_constant unit_big_int) s e)) s e)) s e | (RC_nexp n1 :: RC_gteq :: RC_nexp n2 :: chain) -> let nc1 = mk_nc (NC_bounded_ge (n1, n2)) s e in mk_nc (NC_and (nc1, desugar_rchain (RC_nexp n2 :: chain) s e)) s e | (RC_nexp n1 :: RC_gt :: RC_nexp n2 :: chain) -> - let nc1 = mk_nc (NC_bounded_ge (n1, mk_typ (ATyp_sum (n2, mk_typ (ATyp_constant 1) s e)) s e)) s e in + let nc1 = mk_nc (NC_bounded_ge (n1, mk_typ (ATyp_sum (n2, mk_typ (ATyp_constant unit_big_int) s e)) s e)) s e in mk_nc (NC_and (nc1, desugar_rchain (RC_nexp n2 :: chain) s e)) s e | _ -> assert false @@ -153,7 +154,7 @@ let rec desugar_rchain chain s e = /*Terminals with content*/ %token Id TyVar -%token Num +%token Num %token String Bin Hex Real %token Amp At Caret Eq Gt Lt Plus Star EqGt Unit @@ -724,7 +725,7 @@ exp: raise (Parse_error_locn (loc $startpos $endpos,"Missing \"from\" in foreach loop")); if $6 <> "to" && $6 <> "downto" then raise (Parse_error_locn (loc $startpos $endpos,"Missing \"to\" or \"downto\" in foreach loop")); - let step = mk_lit_exp (L_num 1) $startpos $endpos in + let step = mk_lit_exp (L_num unit_big_int) $startpos $endpos in let ord = if $6 = "to" then ATyp_aux(ATyp_inc,loc $startpos($6) $endpos($6)) diff --git a/src/pretty_print.ml b/src/pretty_print.ml index e827320b..f778fe08 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -42,5 +42,4 @@ include Pretty_print_lem_ast include Pretty_print_sail -include Pretty_print_ocaml include Pretty_print_lem diff --git a/src/pretty_print.mli b/src/pretty_print.mli index 835d4648..b878d29e 100644 --- a/src/pretty_print.mli +++ b/src/pretty_print.mli @@ -50,6 +50,4 @@ val pat_to_string : 'a pat -> string (* Prints on formatter the defs as Lem Ast nodes *) val pp_lem_defs : Format.formatter -> tannot defs -> unit - -val pp_defs_ocaml : out_channel -> tannot defs -> string -> string list -> unit val pp_defs_lem : bool -> bool -> (out_channel * string list) -> (out_channel * string list) -> tannot defs -> string -> unit diff --git a/src/pretty_print_common.ml b/src/pretty_print_common.ml index 5cf85002..315772a4 100644 --- a/src/pretty_print_common.ml +++ b/src/pretty_print_common.ml @@ -41,6 +41,7 @@ (**************************************************************************) open Ast +open Big_int open PPrint let pipe = string "|" @@ -67,7 +68,7 @@ let comma_sp = comma ^^ space let colon_sp = spaces colon let doc_var (Kid_aux(Var v,_)) = string v -let doc_int i = string (string_of_int i) +let doc_int i = string (string_of_big_int i) let doc_op symb a b = infix 2 1 symb a b let doc_unop symb a = prefix 2 1 symb a @@ -167,7 +168,7 @@ let doc_typ, doc_atomic_typ, doc_nexp, doc_nexp_constraint = | Typ_app(Id_aux (Id "range", _), [ Typ_arg_aux(Typ_arg_nexp (Nexp_aux(Nexp_constant n, _)), _); Typ_arg_aux(Typ_arg_nexp m, _);]) -> - (squarebars (if n = 0 then nexp m else doc_op colon (doc_int n) (nexp m))) + (squarebars (if eq_big_int n zero_big_int then nexp m else doc_op colon (doc_int n) (nexp m))) | Typ_app(Id_aux (Id "atom", _), [Typ_arg_aux(Typ_arg_nexp n,_)]) -> (squarecolons (nexp n)) | Typ_app(id,args) -> @@ -211,7 +212,7 @@ let doc_typ, doc_atomic_typ, doc_nexp, doc_nexp_constraint = and atomic_nexp_typ ((Nexp_aux(n,_)) as ne) = match n with | Nexp_var v -> doc_var v | Nexp_id i -> braces (doc_id i) - | Nexp_constant i -> if i < 0 then parens(doc_int i) else doc_int i + | Nexp_constant i -> if lt_big_int i zero_big_int then parens(doc_int i) else doc_int i | Nexp_neg _ | Nexp_exp _ | Nexp_times _ | Nexp_sum _ | Nexp_minus _-> group (parens (nexp ne)) diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 22f210e8..2855adbc 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -155,14 +155,14 @@ let is_regtyp (Typ_aux (typ, _)) env = match typ with let doc_nexp_lem nexp = let (Nexp_aux (nexp, l) as full_nexp) = nexp_simp nexp in match nexp with - | Nexp_constant i -> string ("ty" ^ string_of_int i) + | Nexp_constant i -> string ("ty" ^ string_of_big_int i) | Nexp_var v -> string (string_of_kid (orig_kid v)) | _ -> let rec mangle_nexp (Nexp_aux (nexp, _)) = begin match nexp with | Nexp_id id -> string_of_id id | Nexp_var kid -> string_of_id (id_of_kid (orig_kid kid)) - | Nexp_constant i -> Pretty_print_lem_ast.lemnum string_of_int i + | Nexp_constant i -> Pretty_print_lem_ast.lemnum string_of_big_int i | Nexp_times (n1, n2) -> mangle_nexp n1 ^ "_times_" ^ mangle_nexp n2 | Nexp_sum (n1, n2) -> mangle_nexp n1 ^ "_plus_" ^ mangle_nexp n2 | Nexp_minus (n1, n2) -> mangle_nexp n1 ^ "_minus_" ^ mangle_nexp n2 @@ -356,10 +356,10 @@ let doc_lit_lem sequential mwords in_pat (L_aux(lit,l)) a = | L_false -> utf8string "false" | L_true -> utf8string "true" | L_num i -> - let ipp = string_of_int i in + let ipp = string_of_big_int i in utf8string ( if in_pat then "("^ipp^":nn)" - else if i < 0 then "((0"^ipp^"):ii)" + else if lt_big_int i zero_big_int then "((0"^ipp^"):ii)" else "("^ipp^":ii)") | L_hex n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0x" ^ n) ^ ")" (*shouldn't happen*)*) | L_bin n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0b" ^ n) ^ ")" (*shouldn't happen*)*) @@ -759,7 +759,7 @@ let doc_exp_lem, doc_let_lem = let start_idx = match nexp_simp (start) with | Nexp_aux (Nexp_constant i, _) -> expN (simple_num l i) | _ -> - let nc = nc_eq start (nminus len (nconstant 1)) in + let nc = nc_eq start (nminus len (nint 1)) in if prove (env_of full_exp) nc then string (bit_prefix ^ "vector_length") ^^ space ^^ expY v else raise (Reporting_basic.err_unreachable l @@ -787,7 +787,7 @@ let doc_exp_lem, doc_let_lem = let start_idx = match nexp_simp (start) with | Nexp_aux (Nexp_constant i, _) -> expN (simple_num l i) | _ -> - let nc = nc_eq start (nminus len (nconstant 1)) in + let nc = nc_eq start (nminus len (nint 1)) in if prove (env_of full_exp) nc then string (bit_prefix ^ "vector_length") ^^ space ^^ expY v else raise (Reporting_basic.err_unreachable l @@ -951,7 +951,7 @@ let doc_exp_lem, doc_let_lem = | Tabbrev(_,{t= Tapp("vector", [TA_nexp start; TA_nexp len; TA_ord order; TA_typ etyp])}) ->*) let dir,dir_out = if is_order_inc order then (true,"true") else (false, "false") in let start = match nexp_simp start with - | Nexp_aux (Nexp_constant i, _) -> string_of_int i + | Nexp_aux (Nexp_constant i, _) -> string_of_big_int i | _ -> if dir then "0" else string_of_int (List.length exps) in let expspp = match exps with @@ -983,7 +983,7 @@ let doc_exp_lem, doc_let_lem = let start_idx = match nexp_simp (start) with | Nexp_aux (Nexp_constant i, _) -> expN (simple_num l i) | _ -> - let nc = nc_eq start (nminus len (nconstant 1)) in + let nc = nc_eq start (nminus len (nint 1)) in if prove (env_of full_exp) nc then string (bit_prefix ^ "vector_length") ^^ space ^^ expY v else raise (Reporting_basic.err_unreachable l @@ -1000,7 +1000,7 @@ let doc_exp_lem, doc_let_lem = let start_idx = match nexp_simp (start) with | Nexp_aux (Nexp_constant i, _) -> expN (simple_num l i) | _ -> - let nc = nc_eq start (nminus len (nconstant 1)) in + let nc = nc_eq start (nminus len (nint 1)) in if prove (env_of full_exp) nc then string (bit_prefix ^ "vector_length") ^^ space ^^ expY v else raise (Reporting_basic.err_unreachable l @@ -1261,12 +1261,12 @@ let doc_typdef_lem sequential mwords (TD_aux(td, (l, annot))) = match td with raise (Reporting_basic.err_unreachable Parse_ast.Unknown ("register " ^ string_of_id id ^ " has non-constant start index " ^ string_of_nexp start)) with - | _ -> (0, true) in + | _ -> (zero_big_int, true) in doc_op equals (concat [string "let "; parens (concat [doc_id_lem id; underscore; doc_id_lem fid; rfannot])]) (anglebars (concat [space; doc_op equals (string "field_name") (string_lit (doc_id_lem fid)); semi_sp; - doc_op equals (string "field_start") (string (string_of_int start)); semi_sp; + doc_op equals (string "field_start") (string (string_of_big_int start)); semi_sp; doc_op equals (string "field_is_inc") (string (if is_inc then "true" else "false")); semi_sp; doc_op equals (string "get_field") (parens (doc_op arrow (string "fun rec_val") get)); semi_sp; doc_op equals (string "set_field") (parens (doc_op arrow (string "fun rec_val v") set)); space])) in @@ -1463,7 +1463,7 @@ let doc_typdef_lem sequential mwords (TD_aux(td, (l, annot))) = match td with let dir = (if dir_b then "true" else "false") in let dir_suffix = (if dir_b then "_inc" else "_dec") in let ord = Ord_aux ((if dir_b then Ord_inc else Ord_dec), Parse_ast.Unknown) in - let size = if dir_b then i2-i1 +1 else i1-i2 + 1 in + let size = if dir_b then add_big_int (sub_big_int i2 i1) unit_big_int else add_big_int (sub_big_int i1 i2) unit_big_int in let vtyp = vector_typ (nconstant i1) (nconstant size) ord bit_typ in let tannot = doc_tannot_lem sequential mwords false vtyp in let doc_rid (r,id) = parens (separate comma_sp [string_lit (doc_id_lem id); @@ -1474,7 +1474,7 @@ let doc_typdef_lem sequential mwords (TD_aux(td, (l, annot))) = match td with | BF_aux (BF_single i, _) -> (i, i) | BF_aux (BF_range (i, j), _) -> (i, j) | _ -> raise (Reporting_basic.err_unreachable l "unsupported field type") in - let fsize = if dir_b then j-i+1 else i-j+1 in + let fsize = if dir_b then add_big_int (sub_big_int j i) unit_big_int else add_big_int (sub_big_int i j) unit_big_int in let ftyp = vector_typ (nconstant i) (nconstant fsize) ord bit_typ in let reftyp = mk_typ (Typ_app (Id_aux (Id "field_ref", Parse_ast.Unknown), @@ -1491,7 +1491,7 @@ let doc_typdef_lem sequential mwords (TD_aux(td, (l, annot))) = match td with (concat [string "let "; parens (concat [doc_id_lem id; underscore; doc_id_lem fid; rfannot])]) (concat [ space; langlebar; string " field_name = \"" ^^ doc_id_lem fid ^^ string "\";"; hardline; - space; space; space; string (" field_start = " ^ string_of_int i ^ ";"); hardline; + space; space; space; string (" field_start = " ^ string_of_big_int i ^ ";"); hardline; space; space; space; string (" field_is_inc = " ^ dir ^ ";"); hardline; space; space; space; string " get_field = (fun reg -> " ^^ doc_exp_lem sequential mwords false false get ^^ string ");"; hardline; space; space; space; string " set_field = (fun reg v -> " ^^ doc_exp_lem sequential mwords false false set ^^ string ") "; ranglebar]) @@ -1794,10 +1794,10 @@ let doc_register_refs_lem registers = raise (Reporting_basic.err_unreachable Parse_ast.Unknown ("register " ^ string_of_id id ^ " has non-constant start index " ^ string_of_nexp start)) with - | _ -> (0, true) in + | _ -> (zero_big_int, true) in concat [string "let "; idd; string " = <|"; hardline; string " reg_name = \""; idd; string "\";"; hardline; - string " reg_start = "; string (string_of_int start); string ";"; hardline; + string " reg_start = "; string (string_of_big_int start); string ";"; hardline; string " reg_is_inc = "; string (if is_inc then "true" else "false"); string ";"; hardline; string " read_from = (fun s -> s."; field; string ");"; hardline; string " write_to = (fun s v -> (<| s with "; field; string " = v |>)) |>"] in 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)) = diff --git a/src/pretty_print_ocaml.ml b/src/pretty_print_ocaml.ml deleted file mode 100644 index 74461aab..00000000 --- a/src/pretty_print_ocaml.ml +++ /dev/null @@ -1,705 +0,0 @@ -(**************************************************************************) -(* Sail *) -(* *) -(* Copyright (c) 2013-2017 *) -(* Kathyrn Gray *) -(* Shaked Flur *) -(* Stephen Kell *) -(* Gabriel Kerneis *) -(* Robert Norton-Wright *) -(* Christopher Pulte *) -(* Peter Sewell *) -(* *) -(* All rights reserved. *) -(* *) -(* This software was developed by the University of Cambridge Computer *) -(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) -(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) -(* *) -(* Redistribution and use in source and binary forms, with or without *) -(* modification, are permitted provided that the following conditions *) -(* are met: *) -(* 1. Redistributions of source code must retain the above copyright *) -(* notice, this list of conditions and the following disclaimer. *) -(* 2. Redistributions in binary form must reproduce the above copyright *) -(* notice, this list of conditions and the following disclaimer in *) -(* the documentation and/or other materials provided with the *) -(* distribution. *) -(* *) -(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) -(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) -(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) -(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) -(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) -(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) -(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) -(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) -(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) -(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) -(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) -(* SUCH DAMAGE. *) -(**************************************************************************) - -open Big_int -open Ast -open Ast_util -open Type_check -open PPrint -open Pretty_print_common - -(**************************************************************************** - * PPrint-based sail-to-ocaml pretty printer -****************************************************************************) - -let star_sp = star ^^ space - -let sanitize_name s = - "_" ^ s - -let doc_id_ocaml (Id_aux(i,_)) = - match i with - | Id("bit") -> string "vbit" - | Id i -> string (sanitize_name i) - | DeIid x -> - (* add an extra space through empty to avoid a closing-comment - * token in case of x ending with star. *) - parens (separate space [colon; string x; empty]) - -let doc_id_ocaml_type (Id_aux(i,_)) = - match i with - | Id("bit") -> string "vbit" - | Id i -> string (sanitize_name i) - | DeIid x -> - (* add an extra space through empty to avoid a closing-comment - * token in case of x ending with star. *) - parens (separate space [colon; string (String.uncapitalize x); empty]) - -let doc_id_ocaml_ctor (Id_aux(i,_)) = - match i with - | Id("bit") -> string "vbit" - | Id i -> string ((* TODO if n > 246 then "`" else "") ^ *) (String.capitalize i)) - | DeIid x -> - (* add an extra space through empty to avoid a closing-comment - * token in case of x ending with star. *) - parens (separate space [colon; string (String.capitalize x); empty]) - -let doc_typ_ocaml, doc_atomic_typ_ocaml = - (* following the structure of parser for precedence *) - let rec typ ty = fn_typ ty - and fn_typ ((Typ_aux (t, _)) as ty) = match t with - | Typ_fn(arg,ret,efct) -> - separate space [tup_typ arg; arrow; fn_typ ret] - | _ -> tup_typ ty - and tup_typ ((Typ_aux (t, _)) as ty) = match t with - | Typ_tup typs -> parens (separate_map star app_typ typs) - | _ -> app_typ ty - and app_typ ((Typ_aux (t, _)) as ty) = match t with - | Typ_app(Id_aux (Id "vector", _), [ - Typ_arg_aux(Typ_arg_nexp n, _); - Typ_arg_aux(Typ_arg_nexp m, _); - Typ_arg_aux (Typ_arg_order ord, _); - Typ_arg_aux (Typ_arg_typ typ, _)]) -> - string "value" - | Typ_app(Id_aux (Id "range", _), [ - Typ_arg_aux(Typ_arg_nexp n, _); - Typ_arg_aux(Typ_arg_nexp m, _);]) -> - (string "number") - | Typ_app(Id_aux (Id "atom", _), [Typ_arg_aux(Typ_arg_nexp n,_)]) -> - (string "number") - | Typ_app(id,args) -> - (separate_map space doc_typ_arg_ocaml args) ^^ space ^^ (doc_id_ocaml_type id) - | _ -> atomic_typ ty - and atomic_typ ((Typ_aux (t, _)) as ty) = match t with - | Typ_id id -> doc_id_ocaml_type id - | Typ_var v -> doc_var v - | Typ_app _ | Typ_tup _ | Typ_fn _ -> - (* exhaustiveness matters here to avoid infinite loops - * if we add a new Typ constructor *) - group (parens (typ ty)) - and doc_typ_arg_ocaml (Typ_arg_aux(t,_)) = match t with - | Typ_arg_typ t -> app_typ t - | Typ_arg_nexp n -> empty - | Typ_arg_order o -> empty - in typ, atomic_typ - -let doc_lit_ocaml in_pat (L_aux(l,_)) = - utf8string (match l with - | L_unit -> "()" - | L_zero -> "Vzero" - | L_one -> "Vone" - | L_true -> "Vone" - | L_false -> "Vzero" - | L_num i -> - let s = string_of_int i in - if (i >= 0) && (i <= 257) then - "bi" ^ s - else - "(big_int_of_int (" ^ s ^ "))" - | L_hex n -> "(num_to_vec " ^ ("0x" ^ n) ^ ")" (*shouldn't happen*) - | L_bin n -> "(num_to_vec " ^ ("0b" ^ n) ^ ")" (*shouldn't happen*) - | L_undef -> "(failwith \"undef literal not supported\")" (* XXX Undef vectors get handled with to_vec_undef. We could support undef bit but would need to check type. For the moment treat as runtime error. *) - | L_string s -> "\"" ^ s ^ "\"" - | L_real s -> s) - -(* typ_doc is the doc for the type being quantified *) -let doc_typquant_ocaml (TypQ_aux(tq,_)) typ_doc = typ_doc - -let doc_typscm_ocaml (TypSchm_aux(TypSchm_ts(tq,t),_)) = - (doc_typquant_ocaml tq (doc_typ_ocaml t)) - -(*Note: vector concatenation, literal vectors, indexed vectors, and record should - be removed prior to pp. The latter two have never yet been seen -*) -let doc_pat_ocaml = - let rec pat pa = app_pat pa - and app_pat ((P_aux(p,(l,annot))) as pa) = match p with - | P_app(id, ((_ :: _) as pats)) -> - (* TODO This check fails for some reason in the MIPS execute function; - lookup_id returns Unbound, maybe because the environment is not - propagated correctly during rewriting. - I comment out the check for now. *) - (* (match annot with - | Some (env, typ, eff) -> - (match Env.lookup_id id env with - | Union _ -> *) - doc_unop (doc_id_ocaml_ctor id) (parens (separate_map comma_sp pat pats)) - (* | _ -> empty) - | _ -> empty) *) - | P_lit lit -> doc_lit_ocaml true lit - | P_wild -> underscore - | P_id id -> doc_id_ocaml id - | P_as(p,id) -> parens (separate space [pat p; string "as"; doc_id_ocaml id]) - | P_typ(typ,p) -> parens (doc_op colon (pat p) (doc_typ_ocaml typ)) - | P_app(id,[]) -> - (match annot with - | Some (env, typ, eff) -> - (match Env.lookup_id id env with - | Union _ | Enum _ -> doc_id_ocaml_ctor id - | _ -> failwith "encountered unexpected P_app pattern") - | _ -> failwith "encountered unexpected P_app pattern") - | P_vector pats -> - let non_bit_print () = - parens - (separate space [string "VvectorR"; - parens (separate comma_sp [squarebars (separate_map semi pat pats); - underscore; - underscore])]) in - (match annot with - | Some (env, typ, _) -> - if is_bitvector_typ (Env.base_typ_of env typ) - then parens (separate space [string "Vvector"; - parens (separate comma_sp [squarebars (separate_map semi pat pats); - underscore; - underscore])]) - else non_bit_print() - | None -> non_bit_print()) - | P_tup pats -> parens (separate_map comma_sp pat pats) - | P_list pats -> brackets (separate_map semi pat pats) (*Never seen but easy in ocaml*) - | P_cons (p,p') -> doc_op (string "::") (pat p) (pat p') - | P_record _ -> raise (Reporting_basic.err_unreachable l "unhandled record pattern") - | P_vector_concat _ -> raise (Reporting_basic.err_unreachable l "unhandled vector_concat pattern") - in pat - -let id_is_local_var id env = match Env.lookup_id id env with - | Local _ | Unbound -> true - | _ -> false - -let rec lexp_is_local (LEXP_aux (lexp, _)) env = match lexp with - | LEXP_memory _ -> false - | LEXP_id id - | LEXP_cast (_, id) -> id_is_local_var id env - | LEXP_tup lexps -> List.for_all (fun lexp -> lexp_is_local lexp env) lexps - | LEXP_vector (lexp,_) - | LEXP_vector_range (lexp,_,_) - | LEXP_field (lexp,_) -> lexp_is_local lexp env - -let is_regtyp (Typ_aux (typ,_)) env = match typ with - | Typ_app (register, _) -> string_of_id register = "register" - | Typ_id id -> Env.is_regtyp id env - | _ -> false - -let doc_exp_ocaml, doc_let_ocaml = - let rec top_exp read_registers (E_aux (e, (l,annot)) as full_exp) = - let exp = top_exp read_registers in - let (env, typ, eff) = match annot with - | Some (env, typ, eff) -> (env, typ, eff) - | None -> raise (Reporting_basic.err_unreachable l "no type annotation") in - match e with - | E_assign((LEXP_aux(le_act,tannot) as le),e) -> - if lexp_is_local le env - then - (match le_act with - | LEXP_id _ | LEXP_cast _ -> - (*Setting local variable fully *) - doc_op coloneq (doc_lexp_ocaml true le) (exp e) - | LEXP_vector _ -> - doc_op (string "<-") (doc_lexp_array_ocaml le) (exp e) - | LEXP_vector_range _ | LEXP_field _ -> - doc_lexp_rwrite le e) - else - (match le_act with - | LEXP_vector _ | LEXP_vector_range _ | LEXP_cast _ | LEXP_field _ | LEXP_id _ -> - (doc_lexp_rwrite le e) - | LEXP_memory _ -> (doc_lexp_fcall le e)) - | E_vector_append(l,r) -> - parens ((string "vector_concat ") ^^ (exp l) ^^ space ^^ (exp r)) - | E_cons(l,r) -> doc_op (group (colon^^colon)) (exp l) (exp r) - | E_if(c,t,E_aux(E_block [], _)) -> - parens (string "if" ^^ space ^^ string "to_bool" ^^ parens (exp c) ^/^ - string "then" ^^ space ^^ (exp t)) - | E_if(c,t,e) -> - parens ( - string "if" ^^ space ^^ string "to_bool" ^^ parens (exp c) ^/^ - string "then" ^^ space ^^ group (exp t) ^/^ - string "else" ^^ space ^^ group (exp e)) - | E_for(id,exp1,exp2,exp3,(Ord_aux(order,_)),exp4) -> - let var= doc_id_ocaml id in - let (compare,next) = if order = Ord_inc then string "le_big_int",string "add_big_int" else string "ge_big_int",string "sub_big_int" in - let by = exp exp3 in - let stop = exp exp2 in - (*takes over two names but doesn't require building a closure*) - parens - (separate space [(string "let (__stop,__by) = ") ^^ (parens (doc_op comma stop by)); - string "in" ^/^ empty; - string "let rec foreach"; - var; - equals; - string "if"; - parens (compare ^^ space ^^ var ^^ space ^^ (string "__stop") ); - string "then"; - parens (exp exp4 ^^ space ^^ semi ^^ (string "foreach") ^^ - parens (next ^^ space ^^ var ^^ space ^^ (string "__by"))); - string "in"; - string "foreach"; - exp exp1]) - (*Requires fewer introduced names but introduces a closure*) - (*let forL = if order = Ord_inc then string "foreach_inc" else string "foreach_dec" in - forL ^^ space ^^ (group (exp exp1)) ^^ (group (exp exp2)) ^^ (group (exp full_exp3)) ^/^ - group ((string "fun") ^^ space ^^ (doc_id id) ^^ space ^^ arrow ^/^ (exp exp4)) - - (* this way requires the following OCaml declarations first - - let rec foreach_inc i stop by body = - if i <= stop then (body i; foreach_inc (i + by) stop by body) else () - - let rec foreach_dec i stop by body = - if i >= stop then (body i; foreach_dec (i - by) stop by body) else () - - *)*) - | E_let(leb,e) -> doc_op (string "in") (let_exp leb) (exp e) - | E_app(f,args) -> - let call,ctor = match Env.lookup_id f env with - | Union _ -> doc_id_ocaml_ctor f,true - | _ -> doc_id_ocaml f,false in - let base_print () = parens (doc_unop call (parens (separate_map comma exp args))) in - if not(ctor) - then base_print () - else (match args with - | [] -> call - | [arg] -> (match arg with - | E_aux(E_lit (L_aux(L_unit,_)),_) -> call - | _ -> base_print()) - | args -> base_print()) - | E_vector_access(v,e) -> - let call = - if is_bit_typ (Env.base_typ_of env typ) - then (string "bit_vector_access") - else (string "vector_access") in - parens (call ^^ space ^^ exp v ^^ space ^^ exp e) - | E_vector_subrange(v,e1,e2) -> - parens ((string "vector_subrange") ^^ space ^^ (exp v) ^^ space ^^ (exp e1) ^^ space ^^ (exp e2)) - | E_field((E_aux(_,(fl,fannot)) as fexp),id) -> - let ftyp = typ_of_annot (fl,fannot) in - if (is_regtyp ftyp env) then - let field_f = - if (is_bit_typ (Env.base_typ_of env ftyp)) - then string "get_register_field_bit" - else string "get_register_field_vec" in - parens (field_f ^^ space ^^ (exp fexp) ^^ space ^^ string_lit (doc_id id)) - else exp fexp ^^ dot ^^ doc_id_ocaml id - | E_block [] -> string "()" - | E_block exps | E_nondet exps -> - let exps_doc = separate_map (semi ^^ hardline) exp exps in - surround 2 1 (string "begin") exps_doc (string "end") - | E_id id -> - (match Env.lookup_id id env with - | Local (Mutable, _) -> - string "!" ^^ doc_id_ocaml id - | Union _ | Enum _ -> doc_id_ocaml_ctor id - | _ -> - if (is_regtyp typ env) then - if read_registers - then string "(read_register " ^^ doc_id_ocaml id ^^ string ")" - else doc_id_ocaml id - else doc_id_ocaml id) - (*match annot with - | Base((_,t),Alias alias_info,_,_,_,_) -> - (match alias_info with - | Alias_field(reg,field) -> - let field_f = match t.t with - | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) -> string "get_register_field_bit" - | _ -> string "get_register_field_vec" in - parens (separate space [field_f; string (sanitize_name reg); string_lit (string field)]) - | Alias_extract(reg,start,stop) -> - if start = stop - then parens (separate space [string "bit_vector_access";string (sanitize_name reg);doc_int start]) - else parens - (separate space [string "vector_subrange"; string (sanitize_name reg); doc_int start; doc_int stop]) - | Alias_pair(reg1,reg2) -> - parens (separate space [string "vector_concat"; - string (sanitize_name reg1); - string (sanitize_name reg2)])) *) - | E_lit lit -> doc_lit_ocaml false lit - | E_cast(typ,e) -> - (* (match annot with - | Base(_,External _,_,_,_,_) -> - if read_registers - then parens (string "read_register" ^^ space ^^ exp e) - else exp e - | _ -> *) - let (Typ_aux (t,_)) = typ in - (match t with - | Typ_app (Id_aux (Id "vector",_), [Typ_arg_aux (Typ_arg_nexp(Nexp_aux (Nexp_constant i,_)),_);_;_;_]) -> - parens ((concat [string "set_start";space;string (string_of_int i)]) ^//^ - exp e) - | Typ_var (Kid_aux (Var "length",_)) -> - parens ((string "set_start_to_length") ^//^ exp e) - | _ -> - parens (doc_op colon (group (exp e)) (doc_typ_ocaml typ))) - | E_tuple exps -> - parens (separate_map comma exp exps) - | E_record(FES_aux(FES_Fexps(fexps,_),_)) -> - braces (separate_map semi_sp doc_fexp fexps) - | E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) -> - braces (doc_op (string "with") (exp e) (separate_map semi_sp doc_fexp fexps)) - | E_vector exps -> - let (start, _, order, _) = vector_typ_args_of (Env.base_typ_of env typ) in - (*match annot with - | Base((_,t),_,_,_,_,_) -> - match t.t with - | Tapp("vector", [TA_nexp start; _; TA_ord order; _]) - | Tabbrev(_,{t= Tapp("vector", [TA_nexp start; _; TA_ord order; _])}) ->*) - let call = if is_bitvector_typ typ then (string "Vvector") else (string "VvectorR") in - let dir,dir_out = if is_order_inc order then (true,"true") else (false, "false") in - let start = match start with - | Nexp_aux (Nexp_constant i, _) -> string_of_int i - | Nexp_aux (Nexp_exp (Nexp_aux (Nexp_constant i, _)), _) -> - string_of_int (Util.power 2 i) - | _ -> if dir then "0" else string_of_int (List.length exps) in - parens (separate space [call; parens (separate comma_sp [squarebars (separate_map semi exp exps); - string start; - string dir_out])]) - | E_vector_update(v,e1,e2) -> - (*Has never happened to date*) - brackets (doc_op (string "with") (exp v) (doc_op equals (exp e1) (exp e2))) - | E_vector_update_subrange(v,e1,e2,e3) -> - (*Has never happened to date*) - brackets ( - doc_op (string "with") (exp v) - (doc_op equals (exp e1 ^^ colon ^^ exp e2) (exp e3))) - | E_list exps -> - brackets (separate_map semi exp exps) - | E_case(e,pexps) -> - let opening = separate space [string "("; string "match"; top_exp false e; string "with"] in - let cases = separate_map (break 1) doc_case pexps in - surround 2 1 opening cases rparen - | E_exit e -> - separate space [string "exit"; exp e;] - | E_return e -> - separate space [string "begin ret := Some" ; exp e ; string "; raise Sail_return; end"] - | E_app_infix (e1,id,e2) -> - let call = - (* match annot with - | Base((_,t),External(Some name),_,_,_,_) -> string name - | _ -> *) doc_id_ocaml id in - parens (separate space [call; parens (separate_map comma exp [e1;e2])]) - | E_internal_let(lexp, eq_exp, in_exp) -> - separate space [string "let"; - doc_lexp_ocaml true lexp; (*Rewriter/typecheck should ensure this is only cast or id*) - equals; - string "ref"; - exp eq_exp; - string "in"; - exp in_exp] - - | E_internal_plet (pat,e1,e2) -> - (separate space [(exp e1); string ">>= fun"; doc_pat_ocaml pat;arrow]) ^/^ - exp e2 - - | E_internal_return (e1) -> - separate space [string "return"; exp e1;] - | E_assert (e1, e2) -> - (string "assert") ^^ parens ((string "to_bool") ^^ space ^^ exp e1) (* XXX drops e2 *) - | E_sizeof _ -> raise (Reporting_basic.err_unreachable l - "E_sizeof should have been rewritten before pretty-printing") - | E_constraint _ -> empty - | E_sizeof_internal _ | E_internal_exp_user (_, _) | E_internal_cast (_, _) - | E_internal_exp _ -> raise (Reporting_basic.err_unreachable l - "internal expression should have been rewritten before pretty-printing") - | E_comment _ | E_comment_struc _ -> empty (* TODO Should we output comments? *) - and let_exp (LB_aux(lb,_)) = match lb with - | LB_val(pat,e) -> - prefix 2 1 - (separate space [string "let"; doc_pat_ocaml pat; equals]) - (top_exp false e) - - and doc_fexp (FE_aux(FE_Fexp(id,e),_)) = doc_op equals (doc_id_ocaml id) (top_exp false e) - - and doc_case = function - | (Pat_aux(Pat_exp(pat,e),_)) -> - doc_op arrow (separate space [pipe; doc_pat_ocaml pat]) (group (top_exp false e)) - | (Pat_aux(Pat_when(pat,guard,e),_)) -> - doc_op arrow - (separate space [pipe; - doc_op (string "when") (doc_pat_ocaml pat) (top_exp false guard)]) - (group (top_exp false e)) - - and doc_lexp_ocaml top_call ((LEXP_aux(lexp,(l,annot))) as le) = - let exp = top_exp false in - match lexp with - | LEXP_vector(v,e) -> doc_lexp_array_ocaml le - | LEXP_vector_range(v,e1,e2) -> - parens ((string "vector_subrange") ^^ space ^^ (doc_lexp_ocaml false v) ^^ space ^^ (exp e1) ^^ space ^^ (exp e2)) - | LEXP_field(v,id) -> (doc_lexp_ocaml false v) ^^ dot ^^ doc_id_ocaml id - | LEXP_id id | LEXP_cast(_,id) -> - let name = doc_id_ocaml id in - match annot,top_call with - | Some (env, _, _), false -> - (match Env.lookup_id id env with - | Local (Mutable, _) -> string "!" ^^ name - | _ -> name) - | _ -> name - - and doc_lexp_array_ocaml ((LEXP_aux(lexp,(l,annot))) as le) = match lexp with - | LEXP_vector(v,e) -> - (match annot with - | Some (env, t, _) -> - if (is_bit_typ (Env.base_typ_of env t)) - then parens ((string "get_barray") ^^ space ^^ doc_lexp_ocaml false v) ^^ dot ^^ parens ((string "int_of_big_int") ^^ space ^^ (top_exp false e)) - else parens ((string "get_varray") ^^ space ^^ doc_lexp_ocaml false v) ^^ dot ^^ parens ((string "int_of_big_int") ^^ space ^^ (top_exp false e)) - | _ -> - parens ((string "get_varray") ^^ space ^^ doc_lexp_ocaml false v) ^^ dot ^^ parens ((string "int_of_big_int") ^^ space ^^ (top_exp false e))) - | _ -> empty - - and doc_lexp_rwrite ((LEXP_aux(lexp,(l,annot))) as le) e_new_v = - let exp = top_exp false in - let (is_bit,is_bitv) = match annot with - | Some (env, typ, _) -> - let typ = Env.base_typ_of env typ in - (is_bit_typ typ, is_bitvector_typ typ) - | _ -> (false, false) in - match lexp with - | LEXP_vector(v,e) -> - if is_bit then (* XXX check whether register or not?? *) - parens ((string "set_register_bit" ^^ space ^^ doc_lexp_ocaml false v ^^ space ^^ exp e ^^ space ^^ exp e_new_v)) - else (* XXX Check whether vector of reg? XXX Does not work for decreasing vector. *) - parens ((string "set_register") ^^ space ^^ - ((group (parens ((string "get_varray") ^^ space ^^ doc_lexp_ocaml false v)) ^^ - dot ^^ parens ((string "int_of_big_int") ^^ space ^^ (exp e))) ^^ space ^^ (exp e_new_v))) - | LEXP_vector_range(v,e1,e2) -> - parens ((string (if is_bitv then "set_vector_subrange_bit" else "set_vector_subrange_vec")) ^^ space ^^ - doc_lexp_ocaml false v ^^ space ^^ exp e1 ^^ space ^^ exp e2 ^^ space ^^ exp e_new_v) - | LEXP_field(v,id) -> - parens ((string (if is_bit then "set_register_field_bit" else "set_register_field_v")) ^^ space ^^ - doc_lexp_ocaml false v ^^ space ^^string_lit (doc_id id) ^^ space ^^ exp e_new_v) - | LEXP_id id | LEXP_cast (_,id) -> - (* (match annot with - | Base(_,Alias alias_info,_,_,_,_) -> - (match alias_info with - | Alias_field(reg,field) -> - parens ((if is_bit then string "set_register_field_bit" else string "set_register_field_v") ^^ space ^^ - string (sanitize_name reg) ^^ space ^^string_lit (string field) ^^ space ^^ exp e_new_v) - | Alias_extract(reg,start,stop) -> - if start = stop - then - doc_op (string "<-") - (group (parens ((string (if is_bit then "get_barray" else "get_varray")) ^^ space ^^ string reg)) ^^ - dot ^^ parens ((string "int_of_big_int") ^^ space ^^ (doc_int start))) - (exp e_new_v) - else - parens ((string (if is_bitv then "set_vector_subrange_bit" else "set_vector_subrange_vec")) ^^ space ^^ - string reg ^^ space ^^ doc_int start ^^ space ^^ doc_int stop ^^ space ^^ exp e_new_v) - | Alias_pair(reg1,reg2) -> - parens ((string "set_two_regs") ^^ space ^^ string reg1 ^^ space ^^ string reg2 ^^ space ^^ exp e_new_v)) - | _ -> *) - parens (separate space [string "set_register"; doc_id_ocaml id; exp e_new_v]) - - and doc_lexp_fcall ((LEXP_aux(lexp,(l,annot))) as le) e_new_v = match lexp with - | LEXP_memory(id,args) -> doc_id_ocaml id ^^ parens (separate_map comma (top_exp false) (args@[e_new_v])) - - (* expose doc_exp and doc_let *) - in top_exp false, let_exp - -(*TODO Upcase and downcase type and constructors as needed*) -let doc_type_union_ocaml n (Tu_aux(typ_u,_)) = match typ_u with - | Tu_ty_id(typ,id) -> separate space [pipe; doc_id_ocaml_ctor id; string "of"; doc_typ_ocaml typ;] - | Tu_id id -> separate space [pipe; doc_id_ocaml_ctor id] - -let rec doc_range_ocaml (BF_aux(r,_)) = match r with - | BF_single i -> parens (doc_op comma (doc_int i) (doc_int i)) - | BF_range(i1,i2) -> parens (doc_op comma (doc_int i1) (doc_int i2)) - | BF_concat(ir1,ir2) -> (doc_range ir1) ^^ comma ^^ (doc_range ir2) - -let doc_typdef_ocaml (TD_aux(td,_)) = match td with - | TD_abbrev(id,nm,typschm) -> - doc_op equals (concat [string "type"; space; doc_id_ocaml_type id;]) (doc_typscm_ocaml typschm) - | TD_record(id,nm,typq,fs,_) -> - let f_pp (typ,id) = concat [doc_id_ocaml_type id; space; colon; doc_typ_ocaml typ; semi] in - let fs_doc = group (separate_map (break 1) f_pp fs) in - doc_op equals - (concat [string "type"; space; doc_id_ocaml_type id;]) (doc_typquant_ocaml typq (braces fs_doc)) - | TD_variant(id,nm,typq,ar,_) -> - let n = List.length ar in - let ar_doc = group (separate_map (break 1) (doc_type_union_ocaml n) ar) in - doc_op equals - (concat [string "type"; space; doc_id_ocaml_type id;]) - (if n > 246 - then brackets (space ^^(doc_typquant_ocaml typq ar_doc)) - else (doc_typquant_ocaml typq ar_doc)) - | TD_enum(id,nm,enums,_) -> - let n = List.length enums in - let enums_doc = group (separate_map (break 1 ^^ pipe) (doc_id_ocaml_ctor) enums) in - doc_op equals - (concat [string "type"; space; doc_id_ocaml_type id;]) - (enums_doc) - | TD_register(id,n1,n2,rs) -> - let doc_rid (r,id) = parens (separate comma_sp [string_lit (doc_id id); doc_range_ocaml r;]) in - let doc_rids = group (separate_map (semi ^^ (break 1)) doc_rid rs) in - match n1,n2 with - | Nexp_aux(Nexp_constant i1,_),Nexp_aux(Nexp_constant i2,_) -> - let dir = i1 < i2 in - let size = if dir then i2-i1 +1 else i1-i2+1 in - doc_op equals - ((string "let") ^^ space ^^ doc_id_ocaml id ^^ space ^^ (string "init_val")) - (separate space [string "Vregister"; - (parens (separate comma_sp - [parens (separate space - [string "match init_val with"; - pipe; - string "None"; - arrow; - string "ref"; - string "(Array.make"; - doc_int size; - string "Vzero)"; - pipe; - string "Some init_val"; - arrow; - string "ref init_val";]); - doc_nexp n1; - string (if dir then "true" else "false"); - string_lit (doc_id id); - brackets doc_rids]))]) - -let doc_kdef_ocaml (KD_aux(kd,_)) = match kd with - | KD_nabbrev (k, id, name_scm, nexp) -> - separate space [string "let" ; - doc_id_ocaml id; - equals; - doc_nexp nexp] - -let doc_rec_ocaml (Rec_aux(r,_)) = match r with - | Rec_nonrec -> empty - | Rec_rec -> string "rec" ^^ space - -let doc_tannot_opt_ocaml (Typ_annot_opt_aux(t,_)) = match t with - | Typ_annot_opt_some(tq,typ) -> doc_typquant_ocaml tq (doc_typ_ocaml typ) - -let doc_funcl_exp_ocaml (E_aux (e, (l, annot)) as ea) = match annot with - | Some (_, t, efctsum) -> - (* | Base((_,t),tag,nes,efct,efctsum,_) -> *) - if has_effect efctsum BE_lret then - separate hardline [string "let ret = ref None in"; - string "try"; - (doc_exp_ocaml ea); - string "with Sail_return -> match(!ret) with"; - string "| Some(x) -> x"; - string "| None -> failwith \"ret unset\"" - ] - else - doc_exp_ocaml ea - | _ -> doc_exp_ocaml ea - -let doc_funcl_ocaml (FCL_aux(FCL_Funcl(id,pat,exp),_)) = - group (doc_op arrow (doc_pat_ocaml pat) (doc_funcl_exp_ocaml exp)) - -let get_id = function - | [] -> failwith "FD_function with empty list" - | (FCL_aux (FCL_Funcl (id,_,_),_))::_ -> id - -let doc_fundef_ocaml (FD_aux(FD_function(r, typa, efa, fcls),_)) = - match fcls with - | [] -> failwith "FD_function with empty function list" - | [FCL_aux (FCL_Funcl(id,pat,exp),_)] -> - (separate space [(string "let"); (doc_rec_ocaml r); (doc_id_ocaml id); (doc_pat_ocaml pat); equals]) ^^ hardline ^^ (doc_funcl_exp_ocaml exp) - | _ -> - let id = get_id fcls in - let sep = hardline ^^ pipe ^^ space in - let clauses = separate_map sep doc_funcl_ocaml fcls in - separate space [string "let"; - doc_rec_ocaml r; - doc_id_ocaml id; - equals; - (string "function"); - (hardline^^pipe); - clauses] - -let doc_dec_ocaml (DEC_aux (reg,(l,annot))) = - match reg with - | DEC_reg(typ,id) -> - if is_vector_typ typ then - let (start, size, order, itemt) = vector_typ_args_of typ in - if is_bit_typ itemt && is_nexp_constant start && is_nexp_constant size then - let o = if is_order_inc order then string "true" else string "false" in - separate space [string "let"; - doc_id_ocaml id; - equals; - string "Vregister"; - parens (separate comma [separate space [string "ref"; - parens (separate space - [string "Array.make"; - doc_nexp size; - string "Vzero";])]; - doc_nexp start; - o; - string_lit (doc_id id); - brackets empty])] - else raise (Reporting_basic.err_unreachable l - ("can't deal with register type " ^ string_of_typ typ)) - else - (match typ with - | Typ_aux (Typ_id idt, _) -> - (* | Tapp("register", [TA_typ {t=Tid idt}]) | - Tabbrev( {t= Tid idt}, _) -> *) - separate space [string "let"; - doc_id_ocaml id; - equals; - doc_id_ocaml idt; - string "None"] - |_-> raise (Reporting_basic.err_unreachable l - ("can't deal with register type " ^ string_of_typ typ))) - (* | _ -> failwith "annot was not Base") *) - | DEC_alias(id,alspec) -> empty (* - doc_op equals (string "register alias" ^^ space ^^ doc_id id) (doc_alias alspec) *) - | DEC_typ_alias(typ,id,alspec) -> empty (* - doc_op equals (string "register alias" ^^ space ^^ doc_atomic_typ typ) (doc_alias alspec) *) - -let doc_def_ocaml def = group (match def with - | DEF_default df -> empty - | DEF_spec v_spec -> empty (*unless we want to have a separate pass to create mli files*) - | DEF_type t_def -> doc_typdef_ocaml t_def - | DEF_fundef f_def -> doc_fundef_ocaml f_def - | DEF_val lbind -> doc_let_ocaml lbind - | DEF_reg_dec dec -> doc_dec_ocaml dec - | DEF_scattered sdef -> empty (*shoulnd't still be here*) - | DEF_kind k_def -> doc_kdef_ocaml k_def - | DEF_overload _ -> empty - | DEF_comm _ -> failwith "unhandled DEF_comm" - ) ^^ hardline - -let doc_defs_ocaml (Defs(defs)) = - separate_map hardline doc_def_ocaml defs -let pp_defs_ocaml f d top_line opens = - print f (string "(*" ^^ (string top_line) ^^ string "*)" ^/^ - (separate_map hardline (fun lib -> (string "open") ^^ space ^^ (string lib)) opens) ^/^ - (doc_defs_ocaml d)) diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index c53d30b4..e585a8f1 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -42,6 +42,7 @@ open Ast open Ast_util +open Big_int open PPrint open Pretty_print_common @@ -88,7 +89,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 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 diff --git a/src/process_file.ml b/src/process_file.ml index 4c70400c..344e5951 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -47,7 +47,6 @@ let opt_lem_mwords = ref false type out_type = | Lem_ast_out | Lem_out of string option - | Ocaml_out of string option let get_lexbuf f = let in_chan = open_in f in @@ -198,15 +197,6 @@ let output1 libpath out_arg filename defs = output_lem f' [] defs | Lem_out (Some lib) -> output_lem f' [lib] defs - | Ocaml_out None -> - let ((o,temp_file_name, _) as ext_o) = open_output_with_check_unformatted (f' ^ ".ml") in - begin Pretty_print.pp_defs_ocaml o defs (generated_line filename) ["Big_int_Z";"Sail_values"]; - close_output_with_check ext_o - end - | Ocaml_out (Some lib) -> - let ((o,temp_file_name, _) as ext_o) = open_output_with_check_unformatted (f' ^ ".ml") in - Pretty_print.pp_defs_ocaml o defs (generated_line filename) ["Big_int_Z"; "Sail_values"; lib]; - close_output_with_check ext_o let output libpath out_arg files = List.iter diff --git a/src/process_file.mli b/src/process_file.mli index afde469e..b575bd14 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -67,7 +67,6 @@ val opt_auto_mono : bool ref type out_type = | Lem_ast_out | Lem_out of string option (* If present, the string is a file to open in the lem backend*) - | Ocaml_out of string option (* If present, the string is a file to open in the ocaml backend*) val output : string -> (* The path to the library *) diff --git a/src/rewriter.ml b/src/rewriter.ml index 025bade2..62e4f7ef 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -539,21 +539,13 @@ let rewrite_exp rewriters (E_aux (exp,(l,annot))) = | E_internal_return _ -> raise (Reporting_basic.err_unreachable l "Internal return found before it should have been introduced") | E_internal_plet _ -> raise (Reporting_basic.err_unreachable l " Internal plet found before it should have been introduced") | _ -> rewrap exp - + let rewrite_let rewriters (LB_aux(letbind,(l,annot))) = - (*let local_map = get_map_tannot annot in - let map = - match map,local_map with - | None,None -> None - | None,Some m -> Some(m, Envmap.empty) - | Some(m,s), None -> Some(m,s) - | Some(m,s), Some m' -> match merge_option_maps (Some m) local_map with - | None -> Some(m,s) (*Shouldn't happen*) - | Some new_m -> Some(new_m,s) in*) match letbind with | LB_val ( pat, exp) -> LB_aux(LB_val (rewriters.rewrite_pat rewriters pat, - rewriters.rewrite_exp rewriters exp),(l,annot)) + rewriters.rewrite_exp rewriters exp), + (l, annot)) let rewrite_lexp rewriters (LEXP_aux(lexp,(l,annot))) = let rewrap le = LEXP_aux(le,(l,annot)) in @@ -658,7 +650,6 @@ let rec fold_pat_aux (alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg) : 'a pat | P_list ps -> alg.p_list (List.map (fold_pat alg) ps) | P_cons (ph,pt) -> alg.p_cons (fold_pat alg ph, fold_pat alg pt) - and fold_pat (alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg) : 'a pat -> 'pat = function | P_aux (pat,annot) -> alg.p_aux (fold_pat_aux alg pat,annot) @@ -670,7 +661,7 @@ and fold_fpat (alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg) : 'a fpat -> 'f | FP_aux (fpat,annot) -> alg.fP_aux (fold_fpat_aux alg fpat,annot) (* identity fold from term alg to term alg *) -let id_pat_alg : ('a,'a pat, 'a pat_aux, 'a fpat, 'a fpat_aux) pat_alg = +let id_pat_alg : ('a,'a pat, 'a pat_aux, 'a fpat, 'a fpat_aux) pat_alg = { p_lit = (fun lit -> P_lit lit) ; p_wild = P_wild ; p_as = (fun (pat,id) -> P_as (pat,id)) @@ -688,7 +679,7 @@ let id_pat_alg : ('a,'a pat, 'a pat_aux, 'a fpat, 'a fpat_aux) pat_alg = ; fP_aux = (fun (fpat,annot) -> FP_aux (fpat,annot)) ; fP_Fpat = (fun (id,pat) -> FP_Fpat (id,pat)) } - + type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, 'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind, 'pat,'pat_aux,'fpat,'fpat_aux) exp_alg = @@ -749,11 +740,11 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, ; pat_exp : 'pat * 'exp -> 'pexp_aux ; pat_when : 'pat * 'exp * 'exp -> 'pexp_aux ; pat_aux : 'pexp_aux * 'a annot -> 'pexp - ; lB_val : 'pat * 'exp -> 'letbind_aux + ; lB_val : 'pat * 'exp -> 'letbind_aux ; lB_aux : 'letbind_aux * 'a annot -> 'letbind ; pat_alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg } - + let rec fold_exp_aux alg = function | E_block es -> alg.e_block (List.map (fold_exp alg) es) | E_nondet es -> alg.e_nondet (List.map (fold_exp alg) es) @@ -1484,7 +1475,9 @@ let remove_vector_concat_pat pat = let rtyp = Env.base_typ_of (env_of_annot rannot') (typ_of_annot rannot') in let (start,last_idx) = (match vector_typ_args_of rtyp with | (Nexp_aux (Nexp_constant start,_), Nexp_aux (Nexp_constant length,_), ord, _) -> - (start, if is_order_inc ord then start + length - 1 else start - length + 1) + (start, if is_order_inc ord + then sub_big_int (add_big_int start length) unit_big_int + else add_big_int (sub_big_int start length) unit_big_int) | _ -> raise (Reporting_basic.err_unreachable (fst rannot') ("unname_vector_concat_elements: vector of unspecified length in vector-concat pattern"))) in @@ -1493,14 +1486,15 @@ let remove_vector_concat_pat pat = let (_,length,ord,_) = vector_typ_args_of ctyp in let (pos',index_j) = match length with | Nexp_aux (Nexp_constant i,_) -> - if is_order_inc ord then (pos+i, pos+i-1) - else (pos-i, pos-i+1) + if is_order_inc ord + then (add_big_int pos i, sub_big_int (add_big_int pos i) unit_big_int) + else (sub_big_int pos i, add_big_int (sub_big_int pos i) unit_big_int) | Nexp_aux (_,l) -> - if is_last then (pos,last_idx) - else - raise - (Reporting_basic.err_unreachable - l ("unname_vector_concat_elements: vector of unspecified length in vector-concat pattern")) in + if is_last then (pos,last_idx) + else + raise + (Reporting_basic.err_unreachable + l ("unname_vector_concat_elements: vector of unspecified length in vector-concat pattern")) in (match p with (* if we see a named vector pattern, remove the name and remember to declare it later *) @@ -1594,8 +1588,8 @@ let remove_vector_concat_pat pat = with vector_concats patterns as direct child-nodes anymore *) let range a b = - let rec aux a b = if a > b then [] else a :: aux (a+1) b in - if a > b then List.rev (aux b a) else aux a b in + let rec aux a b = if gt_big_int a b then [] else a :: aux (add_big_int a unit_big_int) b in + if gt_big_int a b then List.rev (aux b a) else aux a b in let remove_vector_concats = let p_vector_concat ps = @@ -1609,9 +1603,9 @@ let remove_vector_concat_pat pat = match p, vector_typ_args_of typ with | P_vector ps,_ -> acc @ ps | _, (_,Nexp_aux (Nexp_constant length,_),_,_) -> - acc @ (List.map wild (range 0 (length - 1))) + acc @ (List.map wild (range zero_big_int (sub_big_int length unit_big_int))) | _, _ -> - (*if is_last then*) acc @ [wild 0] + (*if is_last then*) acc @ [wild zero_big_int] else raise (Reporting_basic.err_unreachable l ("remove_vector_concats: Non-vector in vector-concat pattern " ^ @@ -1936,15 +1930,15 @@ let remove_bitvector_pat pat = let test_subvec_exp rootid l typ i j lits = let (start, length, ord, _) = vector_typ_args_of typ in - let length' = nconstant (List.length lits) in + let length' = nint (List.length lits) in let start' = - if is_order_inc ord then nconstant 0 - else nminus length' (nconstant 1) in + if is_order_inc ord then nint 0 + else nminus length' (nint 1) in let typ' = vector_typ start' length' ord bit_typ in let subvec_exp = match start, length with | Nexp_aux (Nexp_constant s, _), Nexp_aux (Nexp_constant l, _) - when s = i && l = List.length lits -> + when eq_big_int s i && eq_big_int l (big_int_of_int (List.length lits)) -> E_id rootid | _ -> (*if vec_start t = i && vec_length t = List.length lits @@ -1988,7 +1982,7 @@ let remove_bitvector_pat pat = let collect_guards_decls ps rootid t = let (start,_,ord,_) = vector_typ_args_of t in let rec collect current (guards,dls) idx ps = - let idx' = if is_order_inc ord then idx + 1 else idx - 1 in + let idx' = if is_order_inc ord then add_big_int idx unit_big_int else add_big_int idx unit_big_int in (match ps with | pat :: ps' -> (match pat with @@ -2717,15 +2711,15 @@ let rewrite_tuple_vector_assignments defs = let (_, len, _, _) = vector_typ_args_of ltyp in match nexp_simp len with | Nexp_aux (Nexp_constant len, _) -> len - | _ -> 1 - else 1 in + | _ -> unit_big_int + else unit_big_int in let next i step = if is_order_inc ord - then (i + step - 1, i + step) - else (i - step + 1, i - step) in + then (sub_big_int (add_big_int i step) unit_big_int, add_big_int i step) + else (add_big_int (sub_big_int i step) unit_big_int, sub_big_int i step) in let i = match nexp_simp start with | (Nexp_aux (Nexp_constant i, _)) -> i - | _ -> if is_order_inc ord then 0 else List.length lexps - 1 in + | _ -> if is_order_inc ord then zero_big_int else big_int_of_int (List.length lexps - 1) in let l = gen_loc (fst annot) in let exp' = if small exp then strip_exp exp diff --git a/src/rewriter.mli b/src/rewriter.mli index 412852d4..c107be25 100644 --- a/src/rewriter.mli +++ b/src/rewriter.mli @@ -53,7 +53,7 @@ type 'a rewriters = { rewrite_exp : 'a rewriters -> 'a exp -> 'a exp; rewrite_def : 'a rewriters -> 'a def -> 'a def; rewrite_defs : 'a rewriters -> 'a defs -> 'a defs; } - + val rewrite_exp : tannot rewriters -> tannot exp -> tannot exp val rewrite_defs : tannot defs -> tannot defs val rewrite_undefined : bool -> tannot defs -> tannot defs diff --git a/src/type_check.ml b/src/type_check.ml index aff5567f..3a8f2e59 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -304,9 +304,9 @@ module Env : sig val is_register : id -> t -> bool val get_register : id -> t -> typ val add_register : id -> typ -> t -> t - val add_regtyp : id -> int -> int -> (index_range * id) list -> t -> t + val add_regtyp : id -> big_int -> big_int -> (index_range * id) list -> t -> t val is_regtyp : id -> t -> bool - val get_regtyp : id -> t -> int * int * (index_range * id) list + val get_regtyp : id -> t -> big_int * big_int * (index_range * id) list val is_mutable : id -> t -> bool val get_constraints : t -> n_constraint list val add_constraint : n_constraint -> t -> t @@ -361,7 +361,7 @@ end = struct locals : (mut * typ) Bindings.t; union_ids : (typquant * typ) Bindings.t; registers : typ Bindings.t; - regtyps : (int * int * (index_range * id) list) Bindings.t; + regtyps : (big_int * big_int * (index_range * id) list) Bindings.t; variants : (typquant * type_union list) Bindings.t; typ_vars : base_kind_aux KBindings.t; typ_synonyms : (t -> typ_arg list -> typ) Bindings.t; @@ -764,11 +764,11 @@ end = struct | BF_single n -> if cmp f n && cmp n t then n - else typ_error l ("Badly ordered index range: " ^ string_of_list ", " string_of_int [f; n; t]) + else typ_error l ("Badly ordered index range: " ^ string_of_list ", " string_of_big_int [f; n; t]) | BF_range (n1, n2) -> if cmp f n1 && cmp n1 n2 && cmp n2 t then n2 - else typ_error l ("Badly ordered index range: " ^ string_of_list ", " string_of_int [f; n1; n2; t]) + else typ_error l ("Badly ordered index range: " ^ string_of_list ", " string_of_big_int [f; n1; n2; t]) | BF_concat _ -> typ_error l "Index range concatenation currently unsupported" let rec check_index_ranges ids cmp base top = function @@ -798,9 +798,9 @@ end = struct else begin typ_print ("Adding register type " ^ string_of_id id); - if base > top - then check_index_ranges IdSet.empty (fun x y -> x > y) (base + 1) (top - 1) ranges - else check_index_ranges IdSet.empty (fun x y -> x < y) (base - 1) (top + 1) ranges; + if gt_big_int base top + then check_index_ranges IdSet.empty gt_big_int (add_big_int base unit_big_int) (sub_big_int top unit_big_int) ranges + else check_index_ranges IdSet.empty lt_big_int (sub_big_int base unit_big_int) (add_big_int top unit_big_int) ranges; { env with regtyps = Bindings.add id (base, top, ranges) env.regtyps } end @@ -921,7 +921,7 @@ end = struct rewrap (Typ_app (id, List.map aux_arg targs)) | Typ_id id when is_regtyp id env -> let base, top, ranges = get_regtyp id env in - let len = abs(top - base) + 1 in + let len = sub_big_int (abs_big_int (sub_big_int top base)) unit_big_int in vector_typ (nconstant base) (nconstant len) (get_default_order env) bit_typ (* TODO registers with non-default order? non-bitvector registers? *) | t -> rewrap t @@ -960,9 +960,9 @@ let dvector_typ env n m typ = vector_typ n m (Env.get_default_order env) typ let lvector_typ env l typ = match Env.get_default_order env with | Ord_aux (Ord_inc, _) as ord -> - vector_typ (nconstant 0) l ord typ + vector_typ (nint 0) l ord typ | Ord_aux (Ord_dec, _) as ord -> - vector_typ (nminus l (nconstant 1)) l ord typ + vector_typ (nminus l (nint 1)) l ord typ let ex_counter = ref 0 @@ -1066,7 +1066,7 @@ let rec normalize_typ env (Typ_aux (typ, l)) = match typ with | Typ_id (Id_aux (Id "int", _)) -> Tnf_index_sort IS_int | Typ_id (Id_aux (Id "nat", _)) -> - let kid = Env.fresh_kid env in Tnf_index_sort (IS_prop (kid, [(nconstant 0, nvar kid)])) + let kid = Env.fresh_kid env in Tnf_index_sort (IS_prop (kid, [(nint 0, nvar kid)])) | Typ_id v -> begin try normalize_typ env (Env.get_typ_synonym v env env []) with @@ -1121,7 +1121,7 @@ let rec nexp_constraint env var_of (Nexp_aux (nexp, l)) = match nexp with | Nexp_id v -> nexp_constraint env var_of (Env.get_num_def v env) | Nexp_var kid -> Constraint.variable (var_of kid) - | Nexp_constant c -> Constraint.constant (big_int_of_int c) + | Nexp_constant c -> Constraint.constant c | Nexp_times (nexp1, nexp2) -> Constraint.mult (nexp_constraint env var_of nexp1) (nexp_constraint env var_of nexp2) | Nexp_sum (nexp1, nexp2) -> Constraint.add (nexp_constraint env var_of nexp1) (nexp_constraint env var_of nexp2) | Nexp_minus (nexp1, nexp2) -> Constraint.sub (nexp_constraint env var_of nexp1) (nexp_constraint env var_of nexp2) @@ -1138,8 +1138,8 @@ let rec nc_constraint env var_of (NC_aux (nc, l)) = | NC_set (_, []) -> Constraint.literal false | NC_set (kid, (int :: ints)) -> List.fold_left Constraint.disj - (Constraint.eq (nexp_constraint env var_of (nvar kid)) (Constraint.constant (big_int_of_int int))) - (List.map (fun i -> Constraint.eq (nexp_constraint env var_of (nvar kid)) (Constraint.constant (big_int_of_int i))) ints) + (Constraint.eq (nexp_constraint env var_of (nvar kid)) (Constraint.constant int)) + (List.map (fun i -> Constraint.eq (nexp_constraint env var_of (nvar kid)) (Constraint.constant i)) ints) | NC_or (nc1, nc2) -> Constraint.disj (nc_constraint env var_of nc1) (nc_constraint env var_of nc2) | NC_and (nc1, nc2) -> Constraint.conj (nc_constraint env var_of nc1) (nc_constraint env var_of nc2) | NC_false -> Constraint.literal false @@ -1181,12 +1181,12 @@ let prove env (NC_aux (nc_aux, _) as nc) = | _, _ -> false in match nc_aux with - | NC_equal (nexp1, nexp2) when compare_const (fun c1 c2 -> c1 = c2) (nexp_simp nexp1) (nexp_simp nexp2) -> true - | NC_bounded_le (nexp1, nexp2) when compare_const (fun c1 c2 -> c1 <= c2) (nexp_simp nexp1) (nexp_simp nexp2) -> true - | NC_bounded_ge (nexp1, nexp2) when compare_const (fun c1 c2 -> c1 >= c2) (nexp_simp nexp1) (nexp_simp nexp2) -> true - | NC_equal (nexp1, nexp2) when compare_const (fun c1 c2 -> c1 <> c2) (nexp_simp nexp1) (nexp_simp nexp2) -> false - | NC_bounded_le (nexp1, nexp2) when compare_const (fun c1 c2 -> c1 > c2) (nexp_simp nexp1) (nexp_simp nexp2) -> false - | NC_bounded_ge (nexp1, nexp2) when compare_const (fun c1 c2 -> c1 < c2) (nexp_simp nexp1) (nexp_simp nexp2) -> false + | NC_equal (nexp1, nexp2) when compare_const eq_big_int (nexp_simp nexp1) (nexp_simp nexp2) -> true + | NC_bounded_le (nexp1, nexp2) when compare_const le_big_int (nexp_simp nexp1) (nexp_simp nexp2) -> true + | NC_bounded_ge (nexp1, nexp2) when compare_const ge_big_int (nexp_simp nexp1) (nexp_simp nexp2) -> true + | NC_equal (nexp1, nexp2) when compare_const (fun c1 c2 -> not (eq_big_int c1 c2)) (nexp_simp nexp1) (nexp_simp nexp2) -> false + | NC_bounded_le (nexp1, nexp2) when compare_const gt_big_int (nexp_simp nexp1) (nexp_simp nexp2) -> false + | NC_bounded_ge (nexp1, nexp2) when compare_const lt_big_int (nexp_simp nexp1) (nexp_simp nexp2) -> false | NC_true -> true | NC_false -> false | _ -> prove_z3 env nc @@ -1288,7 +1288,7 @@ let rec nexp_identical (Nexp_aux (nexp1, _)) (Nexp_aux (nexp2, _)) = match nexp1, nexp2 with | Nexp_id v1, Nexp_id v2 -> Id.compare v1 v2 = 0 | Nexp_var kid1, Nexp_var kid2 -> Kid.compare kid1 kid2 = 0 - | Nexp_constant c1, Nexp_constant c2 -> c1 = c2 + | Nexp_constant c1, Nexp_constant c2 -> eq_big_int c1 c2 | Nexp_times (n1a, n1b), Nexp_times (n2a, n2b) -> nexp_identical n1a n2a && nexp_identical n1b n2b | Nexp_sum (n1a, n1b), Nexp_sum (n2a, n2b) -> nexp_identical n1a n2a && nexp_identical n1b n2b | Nexp_minus (n1a, n1b), Nexp_minus (n2a, n2b) -> nexp_identical n1a n2a && nexp_identical n1b n2b @@ -1400,8 +1400,8 @@ let rec unify_nexps l env goals (Nexp_aux (nexp_aux1, _) as nexp1) (Nexp_aux (ne | Nexp_constant c2 -> begin match n1a with - | Nexp_aux (Nexp_constant c1,_) when c2 mod c1 = 0 -> - unify_nexps l env goals n1b (mk_nexp (Nexp_constant (c2 / c1))) + | Nexp_aux (Nexp_constant c1,_) when eq_big_int (mod_big_int c2 c1) zero_big_int -> + unify_nexps l env goals n1b (mk_nexp (Nexp_constant (div_big_int c2 c1))) | _ -> unify_error l ("Cannot unify Nat expression " ^ string_of_nexp nexp1 ^ " with " ^ string_of_nexp nexp2) end | _ -> unify_error l ("Cannot unify Nat expression " ^ string_of_nexp nexp1 ^ " with " ^ string_of_nexp nexp2) @@ -1683,22 +1683,22 @@ let infer_lit env (L_aux (lit_aux, l) as lit) = begin match Env.get_default_order env with | Ord_aux (Ord_inc, _) -> - dvector_typ env (nconstant 0) (nconstant (String.length str)) (mk_typ (Typ_id (mk_id "bit"))) + dvector_typ env (nint 0) (nint (String.length str)) (mk_typ (Typ_id (mk_id "bit"))) | Ord_aux (Ord_dec, _) -> dvector_typ env - (nconstant (String.length str - 1)) - (nconstant (String.length str)) + (nint (String.length str - 1)) + (nint (String.length str)) (mk_typ (Typ_id (mk_id "bit"))) end | L_hex str -> begin match Env.get_default_order env with | Ord_aux (Ord_inc, _) -> - dvector_typ env (nconstant 0) (nconstant (String.length str * 4)) (mk_typ (Typ_id (mk_id "bit"))) + dvector_typ env (nint 0) (nint (String.length str * 4)) (mk_typ (Typ_id (mk_id "bit"))) | Ord_aux (Ord_dec, _) -> dvector_typ env - (nconstant (String.length str * 4 - 1)) - (nconstant (String.length str * 4)) + (nint (String.length str * 4 - 1)) + (nint (String.length str * 4)) (mk_typ (Typ_id (mk_id "bit"))) end | L_undef -> typ_error l "Cannot infer the type of undefined" @@ -1781,7 +1781,7 @@ let pat_env_of (P_aux (_, (l, tannot))) = env_of_annot (l, tannot) (* Flow typing *) let rec big_int_of_nexp (Nexp_aux (nexp, _)) = match nexp with - | Nexp_constant c -> Some (big_int_of_int c) + | Nexp_constant c -> Some c | Nexp_times (n1, n2) -> Util.option_binop add_big_int (big_int_of_nexp n1) (big_int_of_nexp n2) | Nexp_sum (n1, n2) -> @@ -1870,10 +1870,10 @@ let restrict_range_lower c1 nexp1 (Typ_aux (typ_aux, l) as typ) = let apply_flow_constraint = function | Flow_lteq (c, nexp) -> (restrict_range_upper c nexp, - restrict_range_lower (succ_big_int c) (nexp_simp (nsum nexp (nconstant 1)))) + restrict_range_lower (succ_big_int c) (nexp_simp (nsum nexp (nint 1)))) | Flow_gteq (c, nexp) -> (restrict_range_lower c nexp, - restrict_range_upper (pred_big_int c) (nexp_simp (nminus nexp (nconstant 1)))) + restrict_range_upper (pred_big_int c) (nexp_simp (nminus nexp (nint 1)))) let rec infer_flow env (E_aux (exp_aux, (l, _)) as exp) = match exp_aux with @@ -1882,7 +1882,7 @@ let rec infer_flow env (E_aux (exp_aux, (l, _)) as exp) = begin match destruct_atom (typ_of y) with | Some (c, nexp) -> - [(v, Flow_lteq (pred_big_int c, nexp_simp (nminus nexp (nconstant 1))))], [] + [(v, Flow_lteq (pred_big_int c, nexp_simp (nminus nexp (nint 1))))], [] | _ -> [], [] end | E_app (f, [E_aux (E_id v, _); y]) when string_of_id f = "lteq_range_atom" -> @@ -1897,7 +1897,7 @@ let rec infer_flow env (E_aux (exp_aux, (l, _)) as exp) = begin match destruct_atom (typ_of y) with | Some (c, nexp) -> - [(v, Flow_gteq (succ_big_int c, nexp_simp (nsum nexp (nconstant 1))))], [] + [(v, Flow_gteq (succ_big_int c, nexp_simp (nsum nexp (nint 1))))], [] | _ -> [], [] end | E_app (f, [E_aux (E_id v, _); y]) when string_of_id f = "gteq_range_atom" -> @@ -2164,7 +2164,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ | E_vector vec, _ -> let (start, len, ord, vtyp) = destruct_vec_typ l env typ in let checked_items = List.map (fun i -> crule check_exp env i vtyp) vec in - if prove env (nc_eq (nconstant (List.length vec)) (nexp_simp len)) then annot_exp (E_vector checked_items) typ + if prove env (nc_eq (nint (List.length vec)) (nexp_simp len)) then annot_exp (E_vector checked_items) typ else typ_error l "List length didn't match" (* FIXME: improve error message *) | E_lit (L_aux (L_undef, _) as lit), _ -> if is_typ_monomorphic typ || Env.polymorphic_undefineds env @@ -2292,7 +2292,7 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) annot_pat (P_var (typed_pat, kid)) typ, env | None, Typ_aux (Typ_id id, _) when Id.compare id (mk_id "nat") == 0 -> let env = Env.add_typ_var kid BK_nat env in - let env = Env.add_constraint (nc_gt (nvar kid) (nconstant 0)) env in + let env = Env.add_constraint (nc_gt (nvar kid) (nint 0)) env in let typed_pat, env = bind_pat env pat (atom_typ (nvar kid)) in annot_pat (P_var (typed_pat, kid)) typ, env | None, Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp lo, _); Typ_arg_aux (Typ_arg_nexp hi, _)]), _) @@ -2412,7 +2412,7 @@ and infer_pat env (P_aux (pat_aux, (l, ())) as pat) = in let ((typed_pat :: typed_pats) as pats), env = List.fold_left fold_pats ([], env) (pat :: pats) in - let len = nexp_simp (nconstant (List.length pats)) in + let len = nexp_simp (nint (List.length pats)) in let etyp = pat_typ_of typed_pat in List.map (fun pat -> typ_equality l env etyp (pat_typ_of pat)) pats; annot_pat (P_vector pats) (lvector_typ env len etyp), env @@ -2482,9 +2482,9 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as in let vec_typ = match range, Env.get_default_order env with | BF_aux (BF_single n, _), Ord_aux (Ord_dec, _) -> - dvector_typ env (nconstant n) (nconstant 1) (mk_typ (Typ_id (mk_id "bit"))) + dvector_typ env (nconstant n) (nint 1) (mk_typ (Typ_id (mk_id "bit"))) | BF_aux (BF_range (n, m), _), Ord_aux (Ord_dec, _) -> - dvector_typ env (nconstant n) (nconstant (n - m + 1)) (mk_typ (Typ_id (mk_id "bit"))) + dvector_typ env (nconstant n) (nconstant (add_big_int (sub_big_int n m) unit_big_int)) (mk_typ (Typ_id (mk_id "bit"))) | _, _ -> typ_error l "Not implemented this register field type yet..." in let checked_exp = crule check_exp env exp vec_typ in @@ -2605,7 +2605,7 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ = tlexp :: tlexps, env, nsum llen llen' | _ -> typ_error l "bit vector assignment must only contain identifiers" in - let tlexps, env, lexp_len = List.fold_right bind_bits_tuple lexps ([], env, nconstant 0) in + let tlexps, env, lexp_len = List.fold_right bind_bits_tuple lexps ([], env, nint 0) in if prove env (nc_eq vec_len lexp_len) then annot_lexp (LEXP_tup tlexps) typ, env else typ_error l "Vector and tuple length must be the same in assignment" @@ -2709,16 +2709,16 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = begin match range, Env.get_default_order env with | BF_aux (BF_single n, _), Ord_aux (Ord_dec, _) -> - let vec_typ = dvector_typ env (nconstant n) (nconstant 1) bit_typ in + let vec_typ = dvector_typ env (nconstant n) (nint 1) bit_typ in annot_exp (E_field (checked_exp, field)) vec_typ | BF_aux (BF_range (n, m), _), Ord_aux (Ord_dec, _) -> - let vec_typ = dvector_typ env (nconstant n) (nconstant (n - m + 1)) bit_typ in + let vec_typ = dvector_typ env (nconstant n) (nconstant (add_big_int (sub_big_int n m) unit_big_int)) bit_typ in annot_exp (E_field (checked_exp, field)) vec_typ | BF_aux (BF_single n, _), Ord_aux (Ord_inc, _) -> - let vec_typ = dvector_typ env (nconstant n) (nconstant 1) bit_typ in + let vec_typ = dvector_typ env (nconstant n) (nint 1) bit_typ in annot_exp (E_field (checked_exp, field)) vec_typ | BF_aux (BF_range (n, m), _), Ord_aux (Ord_inc, _) -> - let vec_typ = dvector_typ env (nconstant n) (nconstant (m - n + 1)) bit_typ in + let vec_typ = dvector_typ env (nconstant n) (nconstant (add_big_int (sub_big_int m n) unit_big_int)) bit_typ in annot_exp (E_field (checked_exp, field)) vec_typ | _, _ -> typ_error l "Invalid register field type" end @@ -2824,14 +2824,14 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = let vec_typ = match Env.get_default_order env with | Ord_aux (Ord_inc, _) -> mk_typ (Typ_app (mk_id "vector", - [mk_typ_arg (Typ_arg_nexp (nconstant 0)); - mk_typ_arg (Typ_arg_nexp (nconstant (List.length vec))); + [mk_typ_arg (Typ_arg_nexp (nint 0)); + mk_typ_arg (Typ_arg_nexp (nint (List.length vec))); mk_typ_arg (Typ_arg_order (Env.get_default_order env)); mk_typ_arg (Typ_arg_typ (typ_of inferred_item))])) | Ord_aux (Ord_dec, _) -> mk_typ (Typ_app (mk_id "vector", - [mk_typ_arg (Typ_arg_nexp (nconstant (List.length vec - 1))); - mk_typ_arg (Typ_arg_nexp (nconstant (List.length vec))); + [mk_typ_arg (Typ_arg_nexp (nint (List.length vec - 1))); + mk_typ_arg (Typ_arg_nexp (nint (List.length vec))); mk_typ_arg (Typ_arg_order (Env.get_default_order env)); mk_typ_arg (Typ_arg_typ (typ_of inferred_item))])) in @@ -3416,7 +3416,7 @@ let check_register env id base top ranges = | Nexp_aux (Nexp_constant basec, _), Nexp_aux (Nexp_constant topc, _) -> let no_typq = TypQ_aux (TypQ_tq [], Parse_ast.Unknown) (* Maybe could be TypQ_no_forall? *) in (* FIXME: wrong for default Order inc? *) - let vec_typ = dvector_typ env base (nconstant ((basec - topc) + 1)) bit_typ in + let vec_typ = dvector_typ env base (nconstant (add_big_int (sub_big_int basec topc) unit_big_int)) bit_typ in let cast_typ = mk_typ (Typ_fn (mk_id_typ id, vec_typ, no_effect)) in let cast_to_typ = mk_typ (Typ_fn (vec_typ, mk_id_typ id, no_effect)) in env diff --git a/src/type_check.mli b/src/type_check.mli index 1254ec36..99385b31 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -43,6 +43,7 @@ open Ast open Ast_util +open Big_int val opt_tc_debug : int ref val opt_no_effects : bool ref @@ -76,7 +77,7 @@ module Env : sig val get_register : id -> t -> typ - val get_regtyp : id -> t -> int * int * (index_range * id) list + val get_regtyp : id -> t -> big_int * big_int * (index_range * id) list (* Return all the identifiers in an enumeration. Throws a type error if the enumeration doesn't exist. *) -- cgit v1.2.3