From bea7b8cc4550411e0f7422fbc5fea47922c37831 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Thu, 24 Aug 2023 17:55:33 +0100 Subject: [PATCH] Remove implicit casts from source These have been deprecated for a long time, so finally remove the code for them --- language/sail.ott | 26 +-- src/bin/repl.ml | 2 +- src/bin/sail.ml | 18 +- src/lib/ast_util.ml | 10 +- src/lib/bitfield.ml | 6 +- src/lib/callgraph.ml | 6 +- src/lib/chunk_ast.ml | 10 +- src/lib/chunk_ast.mli | 8 +- src/lib/constant_propagation_mutrec.ml | 2 +- src/lib/effects.ml | 2 +- src/lib/format_sail.ml | 4 +- src/lib/frontend.ml | 2 - src/lib/frontend.mli | 1 - src/lib/initial_check.ml | 19 +- src/lib/initial_check.mli | 5 - src/lib/jib_compile.ml | 2 +- src/lib/monomorphise.ml | 16 +- src/lib/outcome_rewrites.ml | 2 +- src/lib/parse_ast.ml | 2 +- src/lib/parser.mly | 6 +- src/lib/pretty_print_sail.ml | 6 +- src/lib/property.ml | 2 +- src/lib/rewrites.ml | 64 ++---- src/lib/spec_analysis.ml | 2 +- src/lib/specialize.ml | 10 +- src/lib/splice.ml | 6 +- src/lib/type_check.ml | 216 +++----------------- src/lib/type_check.mli | 10 - src/sail_coq_backend/pretty_print_coq.ml | 8 +- src/sail_doc_backend/docinfo.ml | 2 +- src/sail_latex_backend/latex.ml | 4 +- src/sail_lem_backend/pretty_print_lem.ml | 4 +- src/sail_ocaml_backend/ocaml_backend.ml | 5 +- src/sail_ocaml_backend/sail_plugin_ocaml.ml | 1 - test/c/cheri_capreg.sail | 82 ++++---- test/typecheck/fail/add_vec_lit_old.expect | 8 - test/typecheck/pass/add_vec_lit.sail | 12 +- test/typecheck/pass/enum_cast.sail | 7 +- test/typecheck/pass/while_MM.sail | 14 +- 39 files changed, 179 insertions(+), 433 deletions(-) diff --git a/language/sail.ott b/language/sail.ott index 837a23ea7..f0df5c074 100644 --- a/language/sail.ott +++ b/language/sail.ott @@ -670,27 +670,21 @@ val_spec {{ ocaml 'a val_spec }} {{ lem val_spec 'a }} :: 'VS_' ::= {{ lem VS_aux of val_spec_aux * annot 'a }} | val_spec_aux :: :: aux -cast_opt :: 'Cast_' ::= - {{ com option cast annotation for val specs }} - {{ ocaml bool }} {{ lem bool }} {{ isa bool }} - | :: S :: no_cast {{ ocaml false }} {{ lem false }} {{ isa false }} - | cast :: S :: cast {{ ocaml true }} {{ lem true }} {{ isa true }} - val_spec_aux :: 'VS_' ::= {{ com value type specification }} - {{ ocaml VS_val_spec of typschm * id * (string * string) list * bool }} - {{ lem VS_val_spec of typschm * id * maybe extern * bool }} - {{ isa typschm * id * (string => string option) * bool }} - | val cast_opt id : typschm :: S :: val_spec + {{ ocaml VS_val_spec of typschm * id * extern option }} + {{ lem VS_val_spec of typschm * id * maybe extern }} + {{ isa typschm * id * (string => string option) }} + | val id : typschm :: S :: val_spec {{ com specify the type of an upcoming definition }} - {{ ocaml (VS_val_spec [[typschm]] [[id]] [] [[cast_opt]]) }} {{ lem }} {{ isa }} - | val cast_opt string : typschm :: S :: extern_no_rename + {{ ocaml (VS_val_spec [[typschm]] [[id]] []) }} {{ lem }} {{ isa }} + | val string : typschm :: S :: extern_no_rename {{ com specify the type of an external function }} - {{ ocaml (VS_val_spec [[typschm]] [[string]] [ ( "_" , [[string]] ) ] [[cast_opt]] ) }} {{ lem }} {{ isa }} - | val cast_opt id = string : typschm :: S :: extern_rename_all + {{ ocaml (VS_val_spec [[typschm]] [[string]] [ ( "_" , [[string]] ) ]) }} {{ lem }} {{ isa }} + | val id = string : typschm :: S :: extern_rename_all {{ com specify the type of an external function }} - {{ ocaml (VS_val_spec [[typschm]] [[id]] [ ( "_" , [[string]] ) ] [[cast_opt]] ) }} {{ lem }} {{ isa }} - | val cast_opt id = { string1 = string'1 , ... , stringn = string'n } : typschm :: S :: extern_rename_some + {{ ocaml (VS_val_spec [[typschm]] [[id]] [ ( "_" , [[string]] ) ]) }} {{ lem }} {{ isa }} + | val id = { string1 = string'1 , ... , stringn = string'n } : typschm :: S :: extern_rename_some {{ ichlo }} diff --git a/src/bin/repl.ml b/src/bin/repl.ml index bf8901ceb..383ef28ec 100644 --- a/src/bin/repl.ml +++ b/src/bin/repl.ml @@ -197,7 +197,7 @@ let setup_sail_scripting istate = (fun (cmd, (_, action)) -> let name = sail_command_name cmd in let typschm = mk_typschm (mk_typquant []) (Interactive.reflect_typ action) in - mk_val_spec (VS_val_spec (typschm, mk_id name, Some { pure = false; bindings = [("_", name)] }, false)) + mk_val_spec (VS_val_spec (typschm, mk_id name, Some { pure = false; bindings = [("_", name)] })) ) cmds in diff --git a/src/bin/sail.ml b/src/bin/sail.ml index 5187d12d2..d052023a9 100644 --- a/src/bin/sail.ml +++ b/src/bin/sail.ml @@ -175,10 +175,8 @@ let rec options = Arg.Set State.opt_type_grouped_regstate, " group registers with same type together in generated register state record" ); - ( "-enum_casts", - Arg.Set Initial_check.opt_enum_casts, - " allow enumerations to be automatically casted to numeric range types" - ); + (* Casts have been removed, preserved for backwards compatibility *) + ("-enum_casts", Arg.Unit (fun () -> ()), ""); ("-non_lexical_flow", Arg.Set Nl_flow.opt_nl_flow, " allow non-lexical flow typing"); ( "-no_lexp_bounds_check", Arg.Set Type_check.opt_no_lexp_bounds_check, @@ -234,15 +232,9 @@ let rec options = Arg.Set Profile.opt_profile, " (debug) provide basic profiling information for rewriting passes within Sail" ); - ("-dno_cast", Arg.Set Frontend.opt_dno_cast, " (debug) typecheck without any implicit casting"); - ( "-dallow_cast", - Arg.Tuple - [ - Arg.Unit (fun () -> Reporting.simple_warn "-dallow_cast option is deprecated"); - Arg.Clear Frontend.opt_dno_cast; - ], - " (debug) typecheck allowing implicit casting (deprecated)" - ); + ("-dno_cast", Arg.Unit (fun () -> ()), ""); + (* No longer does anything, preserved for backwards compatibility only *) + ("-dallow_cast", Arg.Unit (fun () -> ()), ""); ( "-ddump_rewrite_ast", Arg.String (fun l -> diff --git a/src/lib/ast_util.ml b/src/lib/ast_util.ml index 6e4a8f58a..3380d564c 100644 --- a/src/lib/ast_util.ml +++ b/src/lib/ast_util.ml @@ -1128,7 +1128,7 @@ let id_of_type_def_aux = function id let id_of_type_def (TD_aux (td_aux, _)) = id_of_type_def_aux td_aux -let id_of_val_spec (VS_aux (VS_val_spec (_, id, _, _), _)) = id +let id_of_val_spec (VS_aux (VS_val_spec (_, id, _), _)) = id let id_of_dec_spec (DEC_aux (DEC_reg (_, id, _), _)) = id @@ -1160,7 +1160,7 @@ let ids_of_defs defs = List.fold_left IdSet.union IdSet.empty (List.map ids_of_d let ids_of_ast ast = ids_of_defs ast.defs let val_spec_ids defs = - let val_spec_id (VS_aux (vs_aux, _)) = match vs_aux with VS_val_spec (_, id, _, _) -> id in + let val_spec_id (VS_aux (vs_aux, _)) = match vs_aux with VS_val_spec (_, id, _) -> id in let rec vs_ids = function | DEF_aux (DEF_val vs, _) :: defs -> val_spec_id vs :: vs_ids defs | _ :: defs -> vs_ids defs @@ -1548,7 +1548,7 @@ let construct_mpexp (mpat, guard, ann) = match guard with None -> MPat_aux (MPat_pat mpat, ann) | Some guard -> MPat_aux (MPat_when (mpat, guard), ann) let is_valspec id = function - | DEF_aux (DEF_val (VS_aux (VS_val_spec (_, id', _, _), _)), _) when Id.compare id id' = 0 -> true + | DEF_aux (DEF_val (VS_aux (VS_val_spec (_, id', _), _)), _) when Id.compare id id' = 0 -> true | _ -> false let is_fundef id = function @@ -1557,8 +1557,8 @@ let is_fundef id = function true | _ -> false -let rename_valspec id (VS_aux (VS_val_spec (typschm, _, externs, is_cast), annot)) = - VS_aux (VS_val_spec (typschm, id, externs, is_cast), annot) +let rename_valspec id (VS_aux (VS_val_spec (typschm, _, externs), annot)) = + VS_aux (VS_val_spec (typschm, id, externs), annot) let rename_funcl id (FCL_aux (FCL_funcl (_, pexp), annot)) = FCL_aux (FCL_funcl (id, pexp), annot) diff --git a/src/lib/bitfield.ml b/src/lib/bitfield.ml index 3a05c9703..cd2252599 100644 --- a/src/lib/bitfield.ml +++ b/src/lib/bitfield.ml @@ -95,7 +95,7 @@ let range_width r = List.map slice_width (indices_of_range r) |> List.fold_left (* Generate a constructor function for a bitfield type *) let constructor name order size = let typschm = fun_typschm [bitvec_typ size order] (mk_id_typ name) in - let constructor_val = mk_val_spec (VS_val_spec (typschm, prepend_id "Mk_" name, None, false)) in + let constructor_val = mk_val_spec (VS_val_spec (typschm, prepend_id "Mk_" name, None)) in let constructor_fun = Printf.sprintf "function Mk_%s v = struct { bits = v }" (string_of_id name) in constructor_val :: defs_of_string __POS__ constructor_fun @@ -160,7 +160,7 @@ let field_getter typ_name field order range = let size = range_width range in let typschm = fun_typschm [mk_id_typ typ_name] (bitvec_typ size order) in let fun_id = (field_accessor_ids typ_name field).get in - let spec = mk_val_spec (VS_val_spec (typschm, fun_id, None, false)) in + let spec = mk_val_spec (VS_val_spec (typschm, fun_id, None)) in let body = get_field_exp range (get_bits_field (mk_exp (E_id (mk_id "v")))) in let funcl = mk_funcl fun_id (mk_pat (P_id (mk_id "v"))) body in [spec; mk_fundef [funcl]] @@ -170,7 +170,7 @@ let field_updater typ_name field order range = let typ = mk_id_typ typ_name in let typschm = fun_typschm [typ; bitvec_typ size order] typ in let fun_id = (field_accessor_ids typ_name field).update in - let spec = mk_val_spec (VS_val_spec (typschm, fun_id, None, false)) in + let spec = mk_val_spec (VS_val_spec (typschm, fun_id, None)) in let orig_var = mk_id "v" in let new_val_var = mk_id "x" in let bits_exp = get_bits_field (mk_id_exp orig_var) in diff --git a/src/lib/callgraph.ml b/src/lib/callgraph.ml index acf9707a7..11cf3ea1a 100644 --- a/src/lib/callgraph.ml +++ b/src/lib/callgraph.ml @@ -288,7 +288,7 @@ let add_def_to_graph graph (DEF_aux (def, _)) = let scan_outcome_def l outcome (DEF_aux (aux, _)) = match aux with - | DEF_val (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), _), _, _, _), _)) -> + | DEF_val (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), _), _, _), _)) -> graph := G.add_edges outcome [] !graph; scan_typquant outcome typq; IdSet.iter (fun typ_id -> graph := G.add_edge outcome (Type typ_id) !graph) (typ_ids typ) @@ -306,7 +306,7 @@ let add_def_to_graph graph (DEF_aux (def, _)) = begin match def with - | DEF_val (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (typq, (Typ_aux (Typ_bidir _, _) as typ)), _), id, _, _), _)) + | DEF_val (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (typq, (Typ_aux (Typ_bidir _, _) as typ)), _), id, _), _)) -> graph := G.add_edges (Mapping id) [] !graph; List.iter @@ -319,7 +319,7 @@ let add_def_to_graph graph (DEF_aux (def, _)) = ]; scan_typquant (Mapping id) typq; IdSet.iter (fun typ_id -> graph := G.add_edge (Mapping id) (Type typ_id) !graph) (typ_ids typ) - | DEF_val (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), _), id, _, _), _)) -> + | DEF_val (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), _), id, _), _)) -> graph := G.add_edges (Function id) [] !graph; scan_typquant (Function id) typq; IdSet.iter (fun typ_id -> graph := G.add_edge (Function id) (Type typ_id) !graph) (typ_ids typ) diff --git a/src/lib/chunk_ast.ml b/src/lib/chunk_ast.ml index 637fc271a..0ec4a4e8a 100644 --- a/src/lib/chunk_ast.ml +++ b/src/lib/chunk_ast.ml @@ -108,7 +108,7 @@ type chunk = return_typ_opt : chunks option; funcls : pexp_chunks list; } - | Val of { is_cast : bool; id : id; extern_opt : extern option; typq_opt : chunks option; typ : chunks } + | Val of { id : id; extern_opt : extern option; typq_opt : chunks option; typ : chunks } | Enum of { id : id; enum_functions : chunks list option; members : chunks list } | Function_typ of { mapping : bool; lhs : chunks; rhs : chunks } | Exists of { vars : chunks; constr : chunks; typ : chunks } @@ -223,9 +223,7 @@ let rec prerr_chunk indent = function Queue.iter (prerr_chunk (indent ^ " ")) funcl.body ) fn.funcls - | Val vs -> - Printf.eprintf "%sVal:%s is_cast=%b has_extern=%b\n" indent (string_of_id vs.id) vs.is_cast - (Option.is_some vs.extern_opt) + | Val vs -> Printf.eprintf "%sVal:%s has_extern=%b\n" indent (string_of_id vs.id) (Option.is_some vs.extern_opt) | Enum e -> Printf.eprintf "%sEnum:%s\n" indent (string_of_id e.id); begin @@ -1083,7 +1081,7 @@ let chunk_fundef comments chunks (FD_aux (FD_function (rec_opt, tannot_opt, _, f let funcls = List.map (chunk_funcl comments) funcls in Function { id = fn_id; clause = false; rec_opt = None; typq_opt; return_typ_opt; funcls } |> add_chunk chunks -let chunk_val_spec comments chunks (VS_aux (VS_val_spec (typschm, id, extern_opt, is_cast), l)) = +let chunk_val_spec comments chunks (VS_aux (VS_val_spec (typschm, id, extern_opt), l)) = pop_comments comments chunks l; let typq_chunks_opt, typ = match typschm with @@ -1095,7 +1093,7 @@ let chunk_val_spec comments chunks (VS_aux (VS_val_spec (typschm, id, extern_opt in let typ_chunks = Queue.create () in chunk_atyp comments typ_chunks typ; - add_chunk chunks (Val { is_cast; id; extern_opt; typq_opt = typq_chunks_opt; typ = typ_chunks }); + add_chunk chunks (Val { id; extern_opt; typq_opt = typq_chunks_opt; typ = typ_chunks }); if not (pop_trailing_comment ~space:1 comments chunks (ending_line_num l)) then Queue.push (Spacer (true, 1)) chunks let chunk_register comments chunks (DEC_aux (DEC_reg ((ATyp_aux (_, typ_l) as typ), id, opt_exp), l)) = diff --git a/src/lib/chunk_ast.mli b/src/lib/chunk_ast.mli index c3a147381..a17d07aa6 100644 --- a/src/lib/chunk_ast.mli +++ b/src/lib/chunk_ast.mli @@ -95,13 +95,7 @@ type chunk = return_typ_opt : chunks option; funcls : pexp_chunks list; } - | Val of { - is_cast : bool; - id : Parse_ast.id; - extern_opt : Parse_ast.extern option; - typq_opt : chunks option; - typ : chunks; - } + | Val of { id : Parse_ast.id; extern_opt : Parse_ast.extern option; typq_opt : chunks option; typ : chunks } | Enum of { id : Parse_ast.id; enum_functions : chunks list option; members : chunks list } | Function_typ of { mapping : bool; lhs : chunks; rhs : chunks } | Exists of { vars : chunks; constr : chunks; typ : chunks } diff --git a/src/lib/constant_propagation_mutrec.ml b/src/lib/constant_propagation_mutrec.ml index 41dd3c52c..daa331841 100644 --- a/src/lib/constant_propagation_mutrec.ml +++ b/src/lib/constant_propagation_mutrec.ml @@ -154,7 +154,7 @@ let generate_val_spec env id args l annot = in let quant_items' = List.map mk_qi_kopt (KOptSet.elements kopts') @ List.map mk_qi_nc constraints' in let typschm = mk_typschm (mk_typquant quant_items') typ' in - (mk_val_spec (VS_val_spec (typschm, generate_fun_id id args, None, false)), ksubsts) + (mk_val_spec (VS_val_spec (typschm, generate_fun_id id args, None)), ksubsts) | _, Typ_aux (_, l) -> raise (Reporting.err_unreachable l __POS__ "Function val spec is not a function type") let const_prop target defs substs ksubsts exp = diff --git a/src/lib/effects.ml b/src/lib/effects.ml index a1c6d86a3..9306cc0d5 100644 --- a/src/lib/effects.ml +++ b/src/lib/effects.ml @@ -209,7 +209,7 @@ let infer_def_direct_effects asserts_termination def = begin match def with - | DEF_aux (DEF_val (VS_aux (VS_val_spec (_, id, Some { pure = false; _ }, _), _)), _) -> + | DEF_aux (DEF_val (VS_aux (VS_val_spec (_, id, Some { pure = false; _ }), _)), _) -> effects := EffectSet.add External !effects | DEF_aux (DEF_fundef (FD_aux (FD_function (_, _, funcls), (l, _))), def_annot) -> begin match funcls_info funcls with diff --git a/src/lib/format_sail.ml b/src/lib/format_sail.ml index ad6a676de..5fd967a6e 100644 --- a/src/lib/format_sail.ml +++ b/src/lib/format_sail.ml @@ -529,9 +529,7 @@ module Make (Config : CONFIG) = struct let doc_binding (target, name) = string target ^^ char ':' ^^ space ^^ char '"' ^^ utf8string name ^^ char '"' in - string "val" ^^ space - ^^ (if vs.is_cast then string "cast" ^^ space else empty) - ^^ doc_id vs.id + string "val" ^^ space ^^ doc_id vs.id ^^ group ( match vs.extern_opt with | Some extern -> diff --git a/src/lib/frontend.ml b/src/lib/frontend.ml index 5e83fd3f5..03032c216 100644 --- a/src/lib/frontend.ml +++ b/src/lib/frontend.ml @@ -72,12 +72,10 @@ module StringMap = Map.Make (String) let opt_ddump_initial_ast = ref false let opt_ddump_tc_ast = ref false -let opt_dno_cast = ref true let opt_reformat : string option ref = ref None let check_ast (asserts_termination : bool) (env : Type_check.Env.t) (ast : uannot ast) : Type_check.tannot ast * Type_check.Env.t * Effects.side_effect_info = - let env = if !opt_dno_cast then Type_check.Env.no_casts env else env in let ast, env = Type_error.check env ast in let ast = Scattered.descatter ast in let side_effects = Effects.infer_side_effects asserts_termination ast in diff --git a/src/lib/frontend.mli b/src/lib/frontend.mli index 4653fcb42..6a1883910 100644 --- a/src/lib/frontend.mli +++ b/src/lib/frontend.mli @@ -67,7 +67,6 @@ val opt_ddump_initial_ast : bool ref val opt_ddump_tc_ast : bool ref -val opt_dno_cast : bool ref val opt_reformat : string option ref open Ast_defs diff --git a/src/lib/initial_check.ml b/src/lib/initial_check.ml index c4dd310e8..1a891a4c2 100644 --- a/src/lib/initial_check.ml +++ b/src/lib/initial_check.ml @@ -78,7 +78,6 @@ module P = Parse_ast let opt_undefined_gen = ref false let opt_fast_undefined = ref false let opt_magic_hash = ref false -let opt_enum_casts = ref false type ctx = { kinds : kind_aux KBindings.t; @@ -631,10 +630,10 @@ let to_ast_spec ctx (vs : P.val_spec) : uannot val_spec ctx_out = match vs with | P.VS_aux (vs, l) -> ( match vs with - | P.VS_val_spec (ts, id, ext, is_cast) -> + | P.VS_val_spec (ts, id, ext) -> let typschm, _ = to_ast_typschm ctx ts in let ext = Option.map to_ast_extern ext in - (VS_aux (VS_val_spec (typschm, to_ast_id ctx id, ext, is_cast), (l, empty_uannot)), ctx) + (VS_aux (VS_val_spec (typschm, to_ast_id ctx id, ext), (l, empty_uannot)), ctx) ) let to_ast_outcome ctx (ev : P.outcome_spec) : outcome_spec ctx_out = @@ -757,7 +756,7 @@ let generate_enum_functions l ctx enum_id fns exps = ) ); ]; - mk_val_spec (VS_val_spec (mk_typschm (mk_typquant []) (function_typ [mk_id_typ enum_id] typ), name, None, false)); + mk_val_spec (VS_val_spec (mk_typschm (mk_typquant []) (function_typ [mk_id_typ enum_id] typ), name, None)); ] ) fns @@ -1157,9 +1156,9 @@ let constraint_of_string str = with Parser.Error -> Reporting.unreachable Parse_ast.Unknown __POS__ ("Failed to parse " ^ str) let extern_of_string ?(pure = false) id str = - VS_val_spec (typschm_of_string str, id, Some { pure; bindings = [("_", string_of_id id)] }, false) |> mk_val_spec + VS_val_spec (typschm_of_string str, id, Some { pure; bindings = [("_", string_of_id id)] }) |> mk_val_spec -let val_spec_of_string id str = mk_val_spec (VS_val_spec (typschm_of_string str, id, None, false)) +let val_spec_of_string id str = mk_val_spec (VS_val_spec (typschm_of_string str, id, None)) let quant_item_param = function | QI_aux (QI_id kopt, _) when is_int_kopt kopt -> [prepend_id "atom_" (id_of_kid (kopt_kid kopt))] @@ -1269,7 +1268,7 @@ let generate_undefineds vs_ids defs = letbinds ) in - ( mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, None, false)), + ( mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, None)), mk_fundef [mk_funcl (prepend_id "undefined_" id) pat body] ) in @@ -1277,7 +1276,7 @@ let generate_undefineds vs_ids defs = | TD_enum (id, ids, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) -> let typschm = typschm_of_string ("unit -> " ^ string_of_id id) in [ - mk_val_spec (VS_val_spec (typschm, prepend_id "undefined_" id, None, false)); + mk_val_spec (VS_val_spec (typschm, prepend_id "undefined_" id, None)); mk_fundef [ mk_funcl (prepend_id "undefined_" id) @@ -1293,7 +1292,7 @@ let generate_undefineds vs_ids defs = p_tup (quant_items typq |> List.map quant_item_param |> List.concat |> List.map (fun id -> mk_pat (P_id id))) in [ - mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, None, false)); + mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, None)); mk_fundef [ mk_funcl (prepend_id "undefined_" id) pat @@ -1358,7 +1357,7 @@ let generate_enum_functions vs_ids defs = | Some _ -> gen_enums (enum :: acc) defs | None -> let enum_val_spec name quants typ = - mk_val_spec (VS_val_spec (mk_typschm (mk_typquant quants) typ, name, None, !opt_enum_casts)) + mk_val_spec (VS_val_spec (mk_typschm (mk_typquant quants) typ, name, None)) in let range_constraint kid = nc_and (nc_lteq (nint 0) (nvar kid)) (nc_lteq (nvar kid) (nint (List.length elems - 1))) diff --git a/src/lib/initial_check.mli b/src/lib/initial_check.mli index 450970271..5bb07f18f 100644 --- a/src/lib/initial_check.mli +++ b/src/lib/initial_check.mli @@ -91,11 +91,6 @@ val opt_fast_undefined : bool ref name *) val opt_magic_hash : bool ref -(** When true enums can be automatically casted to range types and - back. Otherwise generated T_of_num and num_of_T functions must be - manually used for each enum T *) -val opt_enum_casts : bool ref - (** This is a bit of a hack right now - it ensures that the undefiend builtins (undefined_vector etc), only get added to the AST once. The original assumption in sail is that the whole AST gets diff --git a/src/lib/jib_compile.ml b/src/lib/jib_compile.ml index 26b5b59d1..9d3cc08bb 100644 --- a/src/lib/jib_compile.ml +++ b/src/lib/jib_compile.ml @@ -1539,7 +1539,7 @@ let optimize_call l ctx clexp id args arg_ctyps ret_ctyp = let instrs = setup @ [call (CL_id (global id, ctyp_of_typ ctx typ))] @ cleanup in let instrs = unique_names instrs in ([CDEF_register (id, ctyp_of_typ ctx typ, instrs)], ctx) - | DEF_val (VS_aux (VS_val_spec (_, id, ext, _), _)) -> + | DEF_val (VS_aux (VS_val_spec (_, id, ext), _)) -> let quant, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_env in let extern = if Env.is_extern id ctx.tc_env "c" then Some (Env.get_extern id ctx.tc_env "c") else None in let arg_typs, ret_typ = diff --git a/src/lib/monomorphise.ml b/src/lib/monomorphise.ml index 0fcf181e3..dd72b9143 100644 --- a/src/lib/monomorphise.ml +++ b/src/lib/monomorphise.ml @@ -1620,12 +1620,12 @@ module AtomToItself = struct (* TODO rewrite tannopt? *) DEF_fundef (FD_aux (FD_function (recopt, tannopt, funcls), (l, empty_tannot))) | DEF_let lb -> DEF_let (rewrite_letbind lb) - | DEF_val (VS_aux (VS_val_spec (typschm, id, extern, cast), (l, annot))) -> + | DEF_val (VS_aux (VS_val_spec (typschm, id, extern), (l, annot))) -> let typschm = match typschm with | TypSchm_aux (TypSchm_ts (tq, typ), l) -> TypSchm_aux (TypSchm_ts (tq, replace_funtype id typ), l) in - DEF_val (VS_aux (VS_val_spec (typschm, id, extern, cast), (l, annot))) + DEF_val (VS_aux (VS_val_spec (typschm, id, extern), (l, annot))) | DEF_register (DEC_aux (DEC_reg (typ, id, Some exp), a)) -> DEF_register (DEC_aux (DEC_reg (typ, id, Some (rewrite_exp exp)), a)) | _ -> aux @@ -4228,9 +4228,7 @@ module BitvectorSizeCasts = struct let kid = mk_kid "n" in let bitsn = bitvector_typ (nvar kid) dec_ord in let ts = mk_typschm (mk_typquant [mk_qi_id K_int kid]) (function_typ [bitsn] bitsn) in - let mkfn name = - mk_val_spec (VS_val_spec (ts, name, Some { pure = true; bindings = [("_", "zeroExtend")] }, false)) - in + let mkfn name = mk_val_spec (VS_val_spec (ts, name, Some { pure = true; bindings = [("_", "zeroExtend")] })) in let defs = List.map mkfn (IdSet.elements !specs_required) in check_defs initial_env defs in @@ -4350,7 +4348,7 @@ module ToplevelNexpRewrites = struct else rewrite_typ_in_spec env nexp_map typ' let rewrite_toplevel_nexps ({ defs; _ } as ast) = - let rewrite_valspec (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (tqs, typ), ts_l), id, ext_opt, is_cast), ann)) = + let rewrite_valspec (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (tqs, typ), ts_l), id, ext_opt), ann)) = match tqs with | TypQ_aux (TypQ_no_forall, _) -> None | TypQ_aux (TypQ_tq qs, tq_l) -> ( @@ -4367,7 +4365,7 @@ module ToplevelNexpRewrites = struct List.map (fun (kid, nexp) -> QI_aux (QI_constraint (nc_eq (nvar kid) nexp), Generated tq_l)) nexp_map in let tqs = TypQ_aux (TypQ_tq (qs @ new_vars @ new_constraints), tq_l) in - let vs = VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (tqs, typ), ts_l), id, ext_opt, is_cast), ann) in + let vs = VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (tqs, typ), ts_l), id, ext_opt), ann) in Some (id, nexp_map, vs) ) in @@ -4548,12 +4546,12 @@ module ToplevelNexpRewrites = struct pat_alg = rw_pat; } in - let rw_spec (VS_aux (VS_val_spec (typschm, id, ext, is_cast), annot)) = + let rw_spec (VS_aux (VS_val_spec (typschm, id, ext), annot)) = match typschm with | TypSchm_aux (TypSchm_ts (typq, typ), annot') -> (* TODO: capture hazard *) let typschm' = TypSchm_aux (TypSchm_ts (typq, expand_type typ), annot') in - VS_aux (VS_val_spec (typschm', id, ext, is_cast), annot) + VS_aux (VS_val_spec (typschm', id, ext), annot) in let rw_typedef (TD_aux (td, annot)) = let rw_union (Tu_aux (Tu_ty_id (typ, id), annot)) = Tu_aux (Tu_ty_id (expand_type typ, id), annot) in diff --git a/src/lib/outcome_rewrites.ml b/src/lib/outcome_rewrites.ml index a3762dd16..6765a1625 100644 --- a/src/lib/outcome_rewrites.ml +++ b/src/lib/outcome_rewrites.ml @@ -154,7 +154,7 @@ let instantiate target ast = DEF_aux ( DEF_val (VS_aux - ( VS_val_spec (TypSchm_aux (TypSchm_ts (typq, instantiate_typ substs typ), l), id, extern, false), + ( VS_val_spec (TypSchm_aux (TypSchm_ts (typq, instantiate_typ substs typ), l), id, extern), (l, empty_uannot) ) ), diff --git a/src/lib/parse_ast.ml b/src/lib/parse_ast.ml index 9abd2f0d0..1b8288745 100644 --- a/src/lib/parse_ast.ml +++ b/src/lib/parse_ast.ml @@ -390,7 +390,7 @@ type type_def_aux = | TD_bitfield of id * atyp * (id * index_range) list (* register mutable bitfield type definition *) type val_spec_aux = (* Value type specification *) - | VS_val_spec of typschm * id * extern option * bool + | VS_val_spec of typschm * id * extern option type dec_spec_aux = (* Register declarations *) | DEC_reg of atyp * id * exp option diff --git a/src/lib/parser.mly b/src/lib/parser.mly index 179833e12..a3c124894 100644 --- a/src/lib/parser.mly +++ b/src/lib/parser.mly @@ -1508,16 +1508,16 @@ externs: val_spec_def: | Val String Colon typschm { let typschm = $4 in - mk_vs (VS_val_spec (typschm, mk_id (Id $2) $startpos($2) $endpos($2), Some { pure = typschm_is_pure typschm; bindings = [("_", $2)] }, false)) $startpos $endpos } + mk_vs (VS_val_spec (typschm, mk_id (Id $2) $startpos($2) $endpos($2), Some { pure = typschm_is_pure typschm; bindings = [("_", $2)] })) $startpos $endpos } | Val id externs Colon typschm { let typschm = $5 in let externs, need_fix = $3 in - mk_vs (VS_val_spec (typschm, $2, (if need_fix then fix_extern typschm externs else externs), false)) $startpos $endpos } + mk_vs (VS_val_spec (typschm, $2, (if need_fix then fix_extern typschm externs else externs))) $startpos $endpos } | Val Cast id externs Colon typschm { cast_deprecated (loc $startpos($2) $endpos($2)); let typschm = $6 in let externs, need_fix = $4 in - mk_vs (VS_val_spec (typschm, $3, (if need_fix then fix_extern typschm externs else externs), true)) $startpos $endpos } + mk_vs (VS_val_spec (typschm, $3, (if need_fix then fix_extern typschm externs else externs))) $startpos $endpos } register_def: | Register id Colon typ diff --git a/src/lib/pretty_print_sail.ml b/src/lib/pretty_print_sail.ml index a5fbc0a6f..e987c6e6b 100644 --- a/src/lib/pretty_print_sail.ml +++ b/src/lib/pretty_print_sail.ml @@ -738,10 +738,8 @@ let doc_spec (VS_aux (v, annot)) = | None -> empty in match v with - | VS_val_spec (ts, id, ext, is_cast) -> - string "val" ^^ space - ^^ (if is_cast then string "cast" ^^ space else empty) - ^^ doc_id id ^^ space ^^ doc_extern ext ^^ colon ^^ space ^^ doc_typschm ts + | VS_val_spec (ts, id, ext) -> + string "val" ^^ space ^^ doc_id id ^^ space ^^ doc_extern ext ^^ colon ^^ space ^^ doc_typschm ts let doc_prec = function Infix -> string "infix" | InfixL -> string "infixl" | InfixR -> string "infixr" diff --git a/src/lib/property.ml b/src/lib/property.ml index 2905de56f..bf83d55ea 100644 --- a/src/lib/property.ml +++ b/src/lib/property.ml @@ -90,7 +90,7 @@ let add_property_guards props ast = | (DEF_aux (DEF_fundef (FD_aux (FD_function (r_opt, t_opt, funcls), fd_aux) as fdef), def_annot) as def) :: defs -> begin match Bindings.find_opt (id_of_fundef fdef) props with - | Some (_, _, pragma_l, VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (quant, _), _), _, _, _), _)) -> begin + | Some (_, _, pragma_l, VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (quant, _), _), _, _), _)) -> begin match quant_split quant with | _, [] -> add_property_guards' (def :: acc) defs | _, constraints -> diff --git a/src/lib/rewrites.ml b/src/lib/rewrites.ml index a39cc7832..c1e35889b 100644 --- a/src/lib/rewrites.ml +++ b/src/lib/rewrites.ml @@ -230,10 +230,10 @@ let rewrite_ast_nexp_ids, _rewrite_typ_nexp_ids = in let rewrite_def env rewriters = function - | DEF_aux (DEF_val (VS_aux (VS_val_spec (typschm, id, exts, b), a)), def_annot) -> + | DEF_aux (DEF_val (VS_aux (VS_val_spec (typschm, id, exts), a)), def_annot) -> let typschm = rewrite_typschm env typschm in let a = rewrite_annot a in - DEF_aux (DEF_val (VS_aux (VS_val_spec (typschm, id, exts, b), a)), def_annot) + DEF_aux (DEF_val (VS_aux (VS_val_spec (typschm, id, exts), a)), def_annot) | DEF_aux (DEF_type (TD_aux (TD_abbrev (id, typq, typ_arg), a)), def_annot) -> DEF_aux (DEF_type (TD_aux (TD_abbrev (id, typq, rewrite_typ_arg env typ_arg), a)), def_annot) | DEF_aux (DEF_type (TD_aux (TD_record (id, typq, fields, b), a)), def_annot) -> @@ -1106,7 +1106,7 @@ let remove_bitvector_pat (P_aux (_, (l, _)) as pat) = let mk_num_exp i = mk_lit_exp (L_num i) in let check_eq_exp l r = let exp = mk_exp (E_app_infix (l, Id_aux (Operator "==", Parse_ast.Unknown), r)) in - check_exp (Env.no_casts env) exp bool_typ + check_exp env exp bool_typ in let access_bit_exp rootid l typ idx = @@ -1877,8 +1877,7 @@ let rewrite_split_fun_ctor_pats fun_name effect_info env ast = | _ -> function_typ [args_typ] ret_typ in let val_spec = - VS_aux - (VS_val_spec (mk_typschm (mk_typquant quants) fun_typ, id, None, false), (Parse_ast.Unknown, empty_tannot)) + VS_aux (VS_val_spec (mk_typschm (mk_typquant quants) fun_typ, id, None), (Parse_ast.Unknown, empty_tannot)) in let fundef = FD_aux (FD_function (r_o, t_o, funcls), fdannot) in let def_annot = mk_def_annot (gen_loc def_annot.loc) in @@ -1893,7 +1892,7 @@ let rewrite_split_fun_ctor_pats fun_name effect_info env ast = List.fold_left (fun tq def -> match def with - | DEF_aux (DEF_val (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (tq, _), _), id, _, _), _)), _) + | DEF_aux (DEF_val (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (tq, _), _), id, _), _)), _) when string_of_id id = fun_name -> tq | _ -> tq @@ -1931,20 +1930,6 @@ let rewrite_type_def_typs rw_typ rw_typquant (TD_aux (td, annot)) = let rewrite_dec_spec_typs rw_typ (DEC_aux (ds, annot)) = match ds with DEC_reg (typ, id, opt_exp) -> DEC_aux (DEC_reg (rw_typ typ, id, opt_exp), annot) -(* Remove overload definitions and cast val specs from the - specification because the interpreter doesn't know about them.*) -let rewrite_overload_cast env ast = - let remove_cast_vs (VS_aux (vs_aux, annot)) = - match vs_aux with VS_val_spec (typschm, id, ext, _) -> VS_aux (VS_val_spec (typschm, id, ext, false), annot) - in - let simple_def = function - | DEF_aux (DEF_val vs, def_annot) -> DEF_aux (DEF_val (remove_cast_vs vs), def_annot) - | def -> def - in - let is_overload = function DEF_aux (DEF_overload _, _) -> true | _ -> false in - let defs = List.map simple_def ast.defs in - { ast with defs = List.filter (fun def -> not (is_overload def)) defs } - let rewrite_undefined mwords env = let rewrite_e_aux (E_aux (e_aux, _) as exp) = match e_aux with @@ -1996,8 +1981,7 @@ let rewrite_simple_types env ast = TypSchm_aux (TypSchm_ts (simple_typquant typq, simple_typ typ), annot) in let simple_vs (VS_aux (vs_aux, annot)) = - match vs_aux with - | VS_val_spec (typschm, id, ext, is_cast) -> VS_aux (VS_val_spec (simple_typschm typschm, id, ext, is_cast), annot) + match vs_aux with VS_val_spec (typschm, id, ext) -> VS_aux (VS_val_spec (simple_typschm typschm, id, ext), annot) in let simple_lit (L_aux (lit_aux, l) as lit) = match lit_aux with @@ -2614,9 +2598,7 @@ let construct_toplevel_string_append_func effect_info env f_id pat = ] in let fun_typ = mk_typ (Typ_fn ([string_typ], option_typ)) in - let new_val_spec = - VS_aux (VS_val_spec (mk_typschm (TypQ_aux (TypQ_no_forall, unk)) fun_typ, f_id, None, false), no_annot) - in + let new_val_spec = VS_aux (VS_val_spec (mk_typschm (TypQ_aux (TypQ_no_forall, unk)) fun_typ, f_id, None), no_annot) in let new_val_spec, env = Type_check.check_val_spec env (mk_def_annot Parse_ast.Unknown) new_val_spec in let non_rec = Rec_aux (Rec_nonrec, Parse_ast.Unknown) in let no_tannot = Typ_annot_opt_aux (Typ_annot_opt_none, Parse_ast.Unknown) in @@ -3844,7 +3826,7 @@ let rewrite_ast_realize_mappings effect_info env ast = in let realize_val_spec def_annot = function | VS_aux - ( VS_val_spec (TypSchm_aux (TypSchm_ts (typq, Typ_aux (Typ_bidir (typ1, typ2), l)), _), id, _, _), + ( VS_val_spec (TypSchm_aux (TypSchm_ts (typq, Typ_aux (Typ_bidir (typ1, typ2), l)), _), id, _), ((_, (tannot : tannot)) as annot) ) -> let forwards_id = mk_id (string_of_id id ^ "_forwards") in @@ -3862,15 +3844,13 @@ let rewrite_ast_realize_mappings effect_info env ast = let backwards_typ = Typ_aux (Typ_fn ([typ2], typ1), l) in let backwards_matches_typ = Typ_aux (Typ_fn ([typ2], bool_typ), l) in - let forwards_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_typ, forwards_id, None, false), no_annot) in - let backwards_spec = - VS_aux (VS_val_spec (mk_typschm typq backwards_typ, backwards_id, None, false), no_annot) - in + let forwards_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_typ, forwards_id, None), no_annot) in + let backwards_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_typ, backwards_id, None), no_annot) in let forwards_matches_spec = - VS_aux (VS_val_spec (mk_typschm typq forwards_matches_typ, forwards_matches_id, None, false), no_annot) + VS_aux (VS_val_spec (mk_typschm typq forwards_matches_typ, forwards_matches_id, None), no_annot) in let backwards_matches_spec = - VS_aux (VS_val_spec (mk_typschm typq backwards_matches_typ, backwards_matches_id, None, false), no_annot) + VS_aux (VS_val_spec (mk_typschm typq backwards_matches_typ, backwards_matches_id, None), no_annot) in let forwards_spec, env = Type_check.check_val_spec env def_annot forwards_spec in @@ -3891,7 +3871,7 @@ let rewrite_ast_realize_mappings effect_info env ast = ) in let forwards_prefix_spec = - VS_aux (VS_val_spec (mk_typschm typq forwards_prefix_typ, prefix_id, None, false), no_annot) + VS_aux (VS_val_spec (mk_typschm typq forwards_prefix_typ, prefix_id, None), no_annot) in let forwards_prefix_spec, env = Type_check.check_val_spec env def_annot forwards_prefix_spec in forwards_prefix_spec @@ -3906,7 +3886,7 @@ let rewrite_ast_realize_mappings effect_info env ast = ) in let backwards_prefix_spec = - VS_aux (VS_val_spec (mk_typschm typq backwards_prefix_typ, prefix_id, None, false), no_annot) + VS_aux (VS_val_spec (mk_typschm typq backwards_prefix_typ, prefix_id, None), no_annot) in let backwards_prefix_spec, env = Type_check.check_val_spec env def_annot backwards_prefix_spec in backwards_prefix_spec @@ -4552,7 +4532,7 @@ let rewrite_explicit_measure effect_info env ast = let rec_id = function Id_aux (Id id, l) | Id_aux (Operator id, l) -> Id_aux (Id ("#rec#" ^ id), Generated l) in let limit = mk_id "#reclimit" in (* Add helper function with extra argument to spec *) - let rewrite_spec (VS_aux (VS_val_spec (typsch, id, extern, flag), ann) as vs) = + let rewrite_spec (VS_aux (VS_val_spec (typsch, id, extern), ann) as vs) = match Bindings.find id measures with | _ -> begin match typsch with @@ -4562,15 +4542,12 @@ let rewrite_explicit_measure effect_info env ast = ( VS_val_spec ( TypSchm_aux (TypSchm_ts (tq, Typ_aux (Typ_fn (args @ [int_typ], res), typl)), tsl), rec_id id, - extern, - flag + extern ), ann ); VS_aux - ( VS_val_spec (TypSchm_aux (TypSchm_ts (tq, Typ_aux (Typ_fn (args, res), typl)), tsl), id, extern, flag), - ann - ); + (VS_val_spec (TypSchm_aux (TypSchm_ts (tq, Typ_aux (Typ_fn (args, res), typl)), tsl), id, extern), ann); ] | _ -> [vs] (* TODO warn *) @@ -4745,7 +4722,7 @@ let remove_duplicate_valspecs env ast = List.fold_left (fun last_externs def -> match def with - | DEF_aux (DEF_val (VS_aux (VS_val_spec (_, id, externs, _), _)), _) -> Bindings.add id externs last_externs + | DEF_aux (DEF_val (VS_aux (VS_val_spec (_, id, externs), _)), _) -> Bindings.add id externs last_externs | _ -> last_externs ) Bindings.empty ast.defs @@ -4754,11 +4731,11 @@ let remove_duplicate_valspecs env ast = List.fold_left (fun (set, defs) def -> match def with - | DEF_aux (DEF_val (VS_aux (VS_val_spec (typschm, id, _, cast), l)), def_annot) -> + | DEF_aux (DEF_val (VS_aux (VS_val_spec (typschm, id, _), l)), def_annot) -> if IdSet.mem id set then (set, defs) else ( let externs = Bindings.find id last_externs in - let vs = VS_aux (VS_val_spec (typschm, id, externs, cast), l) in + let vs = VS_aux (VS_val_spec (typschm, id, externs), l) in (IdSet.add id set, DEF_aux (DEF_val vs, def_annot) :: defs) ) | _ -> (set, def :: defs) @@ -5013,7 +4990,6 @@ let all_rewriters = ("rewrite_explicit_measure", Base_rewriter rewrite_explicit_measure); ("rewrite_loops_with_escape_effect", basic_rewriter rewrite_loops_with_escape_effect); ("simple_types", basic_rewriter rewrite_simple_types); - ("overload_cast", basic_rewriter rewrite_overload_cast); ( "instantiate_outcomes", String_rewriter (fun target -> basic_rewriter (fun _ -> Outcome_rewrites.instantiate target)) ); diff --git a/src/lib/spec_analysis.ml b/src/lib/spec_analysis.ml index c962dc1e9..6bd7d4acd 100644 --- a/src/lib/spec_analysis.ml +++ b/src/lib/spec_analysis.ml @@ -427,7 +427,7 @@ let fv_of_fun consider_var (FD_aux (FD_function (rec_opt, tannot_opt, funcls), _ let fv_of_vspec consider_var (VS_aux (vspec, _)) = match vspec with - | VS_val_spec (ts, id, _, _) -> (init_env ("val:" ^ string_of_id id), snd (fv_of_typschm consider_var mt mt ts)) + | VS_val_spec (ts, id, _) -> (init_env ("val:" ^ string_of_id id), snd (fv_of_typschm consider_var mt mt ts)) let rec find_scattered_of name = function | [] -> [] diff --git a/src/lib/specialize.ml b/src/lib/specialize.ml index 1535233f6..dcd63a812 100644 --- a/src/lib/specialize.ml +++ b/src/lib/specialize.ml @@ -140,7 +140,7 @@ let fix_instantiation spec instantiation = return all Int-polymorphic functions. *) let rec polymorphic_functions ctx defs = match defs with - | DEF_aux (DEF_val (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), _), id, externs, _), _)), _) :: defs -> + | DEF_aux (DEF_val (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), _), id, externs), _)), _) :: defs -> let is_polymorphic = List.exists ctx.is_polymorphic (quant_kopts typq) in if is_polymorphic && not (ctx.extern_filter externs) then IdSet.add id (polymorphic_functions ctx defs) else polymorphic_functions ctx defs @@ -396,10 +396,10 @@ let specialize_id_valspec spec instantiations id ast effect_info = match split_defs (is_valspec id) ast.defs with | None -> Reporting.unreachable (id_loc id) __POS__ ("Valspec " ^ string_of_id id ^ " does not exist!") | Some (pre_defs, vs, post_defs) -> - let typschm, externs, is_cast, annot, def_annot = + let typschm, externs, annot, def_annot = match vs with - | DEF_aux (DEF_val (VS_aux (VS_val_spec (typschm, _, externs, is_cast), annot)), def_annot) -> - (typschm, externs, is_cast, annot, def_annot) + | DEF_aux (DEF_val (VS_aux (VS_val_spec (typschm, _, externs), annot)), def_annot) -> + (typschm, externs, annot, def_annot) | _ -> Reporting.unreachable (id_loc id) __POS__ "val-spec is not actually a val-spec" in let (TypSchm_aux (TypSchm_ts (typq, typ), _)) = typschm in @@ -464,7 +464,7 @@ let specialize_id_valspec spec instantiations id ast effect_info = if IdSet.mem spec_id !spec_ids then [] else begin spec_ids := IdSet.add spec_id !spec_ids; - [DEF_aux (DEF_val (VS_aux (VS_val_spec (typschm, spec_id, externs, is_cast), annot)), def_annot)] + [DEF_aux (DEF_val (VS_aux (VS_val_spec (typschm, spec_id, externs), annot)), def_annot)] end in diff --git a/src/lib/splice.ml b/src/lib/splice.ml index 577484319..59435246d 100644 --- a/src/lib/splice.ml +++ b/src/lib/splice.ml @@ -78,7 +78,7 @@ let scan_ast { defs; _ } = let scan (ids, specs) (DEF_aux (aux, _) as def) = match aux with | DEF_fundef fd -> (IdSet.add (id_of_fundef fd) ids, specs) - | DEF_val (VS_aux (VS_val_spec (_, id, _, _), _) as vs) -> (ids, Bindings.add id vs specs) + | DEF_val (VS_aux (VS_val_spec (_, id, _), _) as vs) -> (ids, Bindings.add id vs specs) | DEF_pragma (("file_start" | "file_end"), _, _) -> (ids, specs) | _ -> raise (Reporting.err_general (def_loc def) "Definition in splice file isn't a spec or function") in @@ -90,7 +90,7 @@ let filter_old_ast repl_ids repl_specs { defs; _ } = | DEF_fundef fd -> let id = id_of_fundef fd in if IdSet.mem id repl_ids then (rdefs, spec_found) else (def :: rdefs, spec_found) - | DEF_val (VS_aux (VS_val_spec (_, id, _, _), _)) -> ( + | DEF_val (VS_aux (VS_val_spec (_, id, _), _)) -> ( match Bindings.find_opt id repl_specs with | Some vs -> (DEF_aux (DEF_val vs, def_annot) :: rdefs, IdSet.add id spec_found) | None -> (def :: rdefs, spec_found) @@ -102,7 +102,7 @@ let filter_old_ast repl_ids repl_specs { defs; _ } = let filter_replacements spec_found { defs; _ } = let not_found = function - | DEF_aux (DEF_val (VS_aux (VS_val_spec (_, id, _, _), _)), _) -> not (IdSet.mem id spec_found) + | DEF_aux (DEF_val (VS_aux (VS_val_spec (_, id, _), _)), _) -> not (IdSet.mem id spec_found) | _ -> true in List.filter not_found defs diff --git a/src/lib/type_check.ml b/src/lib/type_check.ml index 9095357c0..1de687a5e 100644 --- a/src/lib/type_check.ml +++ b/src/lib/type_check.ml @@ -140,8 +140,6 @@ type env = { records : (typquant * (typ * id) list) Bindings.t; accessors : (typquant * typ) Bindings.t; externs : extern Bindings.t; - casts : id list; - allow_casts : bool; allow_bindings : bool; constraints : (constraint_reason * n_constraint) list; default_order : order option; @@ -557,10 +555,6 @@ module Env : sig val get_enum : id -> t -> id list val get_enums : t -> IdSet.t Bindings.t val is_enum : id -> t -> bool - val get_casts : t -> id list - val allow_casts : t -> bool - val no_casts : t -> t - val add_cast : id -> t -> t val allow_polymorphic_undefineds : t -> t val polymorphic_undefineds : t -> bool val lookup_id : id -> t -> typ lvar @@ -614,9 +608,7 @@ end = struct records = Bindings.empty; accessors = Bindings.empty; externs = Bindings.empty; - casts = []; allow_bindings = true; - allow_casts = true; constraints = []; default_order = None; ret_typ = None; @@ -1574,8 +1566,6 @@ end = struct | None -> typ_error env (id_loc id) ("No extern binding found for " ^ string_of_id id) with Not_found -> typ_error env (id_loc id) ("No extern binding found for " ^ string_of_id id) - let get_casts env = env.casts - let add_register id typ env = wf_typ env typ; if Bindings.mem id env.registers then typ_error env (id_loc id) ("Register " ^ string_of_id id ^ " is already bound") @@ -1606,16 +1596,8 @@ end = struct let add_ret_typ typ env = { env with ret_typ = Some typ } - let allow_casts env = env.allow_casts - - let no_casts env = { env with allow_casts = false } - let no_bindings env = { env with allow_bindings = false } - let add_cast cast env = - typ_print (lazy (adding ^ "cast " ^ string_of_id cast)); - { env with casts = cast :: env.casts } - let get_default_order env = match env.default_order with | None -> typ_error env Parse_ast.Unknown "No default order has been set" @@ -3027,57 +3009,6 @@ let check_function_instantiation l id env bind1 bind2 = with Type_error (err_env, l2, err2) -> typ_raise err_env l2 (Err_inner (err2, l1, "Also tried", None, err1)) ) -(* When doing implicit type coercion, for performance reasons we want - to filter out the possible casts to only those that could - reasonably apply. We don't mind if we try some coercions that are - impossible, but we should be careful to never rule out a possible - cast - match_typ and filter_casts implement this logic. It must be - the case that if two types unify, then they match. *) -let rec match_typ env typ1 typ2 = - let (Typ_aux (typ1_aux, _)) = Env.expand_synonyms env typ1 in - let (Typ_aux (typ2_aux, _)) = Env.expand_synonyms env typ2 in - match (typ1_aux, typ2_aux) with - | Typ_exist (_, _, typ1), _ -> match_typ env typ1 typ2 - | _, Typ_exist (_, _, typ2) -> match_typ env typ1 typ2 - | _, Typ_var kid2 -> true - | Typ_id v1, Typ_id v2 when Id.compare v1 v2 = 0 -> true - | Typ_id v1, Typ_id v2 when string_of_id v1 = "int" && string_of_id v2 = "nat" -> true - | Typ_tuple typs1, Typ_tuple typs2 -> List.for_all2 (match_typ env) typs1 typs2 - | Typ_id v, Typ_app (f, _) when string_of_id v = "nat" && string_of_id f = "atom" -> true - | Typ_id v, Typ_app (f, _) when string_of_id v = "int" && string_of_id f = "atom" -> true - | Typ_id v, Typ_app (f, _) when string_of_id v = "nat" && string_of_id f = "range" -> true - | Typ_id v, Typ_app (f, _) when string_of_id v = "int" && string_of_id f = "range" -> true - | Typ_id v, Typ_app (f, _) when string_of_id v = "bool" && string_of_id f = "atom_bool" -> true - | Typ_app (f, _), Typ_id v when string_of_id v = "bool" && string_of_id f = "atom_bool" -> true - | Typ_app (f1, _), Typ_app (f2, _) when string_of_id f1 = "range" && string_of_id f2 = "atom" -> true - | Typ_app (f1, _), Typ_app (f2, _) when string_of_id f1 = "atom" && string_of_id f2 = "range" -> true - | Typ_app (f1, _), Typ_app (f2, _) when Id.compare f1 f2 = 0 -> true - | Typ_id v1, Typ_app (f2, _) when Id.compare v1 f2 = 0 -> true - | Typ_app (f1, _), Typ_id v2 when Id.compare f1 v2 = 0 -> true - | _, _ -> false - -let rec filter_casts env from_typ to_typ casts = - match casts with - | cast :: casts -> begin - let quant, cast_typ = Env.get_val_spec cast env in - match cast_typ with - (* A cast should be a function A -> B and have only a single argument type. *) - | Typ_aux (Typ_fn (arg_typs, cast_to_typ), _) -> begin - match List.filter is_not_implicit arg_typs with - | [cast_from_typ] when match_typ env from_typ cast_from_typ && match_typ env to_typ cast_to_typ -> - typ_print - ( lazy - ("Considering cast " ^ string_of_typ cast_typ ^ " for " ^ string_of_typ from_typ ^ " to " - ^ string_of_typ to_typ - ) - ); - cast :: filter_casts env from_typ to_typ casts - | _ -> filter_casts env from_typ to_typ casts - end - | _ -> filter_casts env from_typ to_typ casts - end - | [] -> [] - type pattern_duplicate = Pattern_singleton of l | Pattern_duplicate of l * l let is_enum_member id env = match Env.lookup_id id env with Enum _ -> true | _ -> false @@ -3514,17 +3445,17 @@ let rec check_exp env (E_aux (exp_aux, (l, uannot)) as exp : uannot exp) (Typ_au match destruct_exist (typ_of (irule infer_exp env y)) with | None | Some (_, NC_aux (NC_true, _), _) -> let inferred_exp = infer_funapp l env f [x; y] (Some typ) in - type_coercion env inferred_exp typ + expect_subtype env inferred_exp typ | Some _ -> let inferred_exp = infer_funapp l env f [x; mk_exp (E_typ (bool_typ, y))] (Some typ) in - type_coercion env inferred_exp typ + expect_subtype env inferred_exp typ | exception Type_error _ -> let inferred_exp = infer_funapp l env f [x; mk_exp (E_typ (bool_typ, y))] (Some typ) in - type_coercion env inferred_exp typ + expect_subtype env inferred_exp typ end | E_app (f, xs), _ -> let inferred_exp = infer_funapp l env f xs (Some typ) in - type_coercion env inferred_exp typ + expect_subtype env inferred_exp typ | E_return exp, _ -> let checked_exp = match Env.get_ret_typ env with @@ -3549,7 +3480,7 @@ let rec check_exp env (E_aux (exp_aux, (l, uannot)) as exp : uannot exp) (Typ_au in annot_exp (E_if (cond', then_branch', else_branch')) typ | _ -> - let cond' = type_coercion env cond' bool_typ in + let cond' = expect_subtype env cond' bool_typ in let then_branch' = crule check_exp (add_opt_constraint l "then branch" (assert_constraint env true cond') env) @@ -3637,7 +3568,7 @@ let rec check_exp env (E_aux (exp_aux, (l, uannot)) as exp : uannot exp) (Typ_au annot_exp (E_internal_assume (nc, exp')) typ | _, _ -> let inferred_exp = irule infer_exp env exp in - type_coercion env inferred_exp typ + expect_subtype env inferred_exp typ and check_block l env exps ret_typ = let final env exp = match ret_typ with Some typ -> crule check_exp env exp typ | None -> irule infer_exp env exp in @@ -3766,82 +3697,27 @@ and check_mpexp other_env env mpexp typ = in construct_mpexp (checked_mpat, checked_guard, (l, empty_tannot)) -(* type_coercion env exp typ takes a fully annoted (i.e. already type - checked) expression exp, and attempts to cast (coerce) it to the - type typ by inserting a coercion function that transforms the - annotated expression into the correct type. Returns an annoted - expression consisting of a type coercion function applied to exp, - or throws a type error if the coercion cannot be performed. *) -and type_coercion env (E_aux (_, (l, _)) as annotated_exp) typ = - let strip exp_aux = strip_exp (E_aux (exp_aux, (Parse_ast.Unknown, empty_tannot))) in - let annot_exp exp typ' = E_aux (exp, (l, mk_expected_tannot env typ' (Some typ))) in - let switch_exp_typ exp = +(* expect_subtype env exp typ takes a fully annoted (i.e. already type + checked) expression exp, and checks that the annotated type is a + subtype of the provided type, updating the type annotation to + reflect this. *) +and expect_subtype env (E_aux (_, (l, _)) as annotated_exp) typ = + let add_expected exp = match exp with | E_aux (exp, (l, (Some tannot, uannot))) -> E_aux (exp, (l, (Some { tannot with expected = Some typ }, uannot))) - | _ -> failwith "Cannot switch type for unannotated function" + | _ -> Reporting.unreachable l __POS__ "Cannot switch type for unannotated expression" in - let rec try_casts trigger errs = function - | [] -> typ_raise env l (Err_no_casts (strip_exp annotated_exp, typ_of annotated_exp, typ, trigger, errs)) - | cast :: casts -> begin - typ_print - ( lazy - ("Casting with " ^ string_of_id cast ^ " expression " ^ string_of_exp annotated_exp ^ " to " - ^ string_of_typ typ - ) - ); - try - let checked_cast = crule check_exp (Env.no_casts env) (strip (E_app (cast, [annotated_exp]))) typ in - annot_exp (E_typ (typ, checked_cast)) typ - with Type_error (_, _, err) -> try_casts trigger (err :: errs) casts - end - in - begin - try - typ_debug - (lazy ("Performing type coercion: from " ^ string_of_typ (typ_of annotated_exp) ^ " to " ^ string_of_typ typ)); - subtyp l env (typ_of annotated_exp) typ; - switch_exp_typ annotated_exp - with - | Type_error (_, _, trigger) when Env.allow_casts env -> - let casts = filter_casts env (typ_of annotated_exp) typ (Env.get_casts env) in - try_casts trigger [] casts - | Type_error (env, l, err) -> typ_raise env l err - end - -(* type_coercion_unify env exp typ attempts to coerce exp to a type - exp_typ in the same way as type_coercion, except it is only - required that exp_typ unifies with typ. Returns the annotated - coercion as with type_coercion and also a set of unifiers, or - throws a unification error *) -and type_coercion_unify env goals (E_aux (_, (l, _)) as annotated_exp) typ = - let strip exp_aux = strip_exp (E_aux (exp_aux, (Parse_ast.Unknown, empty_tannot))) in - let rec try_casts = function - | [] -> unify_error l "No valid casts resulted in unification" - | cast :: casts -> begin - typ_print - ( lazy - ("Casting with " ^ string_of_id cast ^ " expression " ^ string_of_exp annotated_exp ^ " for unification") - ); - try - let inferred_cast = irule infer_exp (Env.no_casts env) (strip (E_app (cast, [annotated_exp]))) in - let ityp, env = bind_existential l None (typ_of inferred_cast) env in - (inferred_cast, unify l env (KidSet.diff goals (ambiguous_vars typ)) typ ityp, env) - with - | Type_error _ -> try_casts casts - | Unification_error _ -> try_casts casts - end - in - begin - try - typ_debug - (lazy ("Coercing unification: from " ^ string_of_typ (typ_of annotated_exp) ^ " to " ^ string_of_typ typ)); - let atyp, env = bind_existential l None (typ_of annotated_exp) env in - let atyp, env = bind_tuple_existentials l None atyp env in - (annotated_exp, unify l env (KidSet.diff goals (ambiguous_vars typ)) typ atyp, env) - with Unification_error (_, _) when Env.allow_casts env -> - let casts = filter_casts env (typ_of annotated_exp) typ (Env.get_casts env) in - try_casts casts - end + typ_debug (lazy ("Expect subtype: from " ^ string_of_typ (typ_of annotated_exp) ^ " to " ^ string_of_typ typ)); + subtyp l env (typ_of annotated_exp) typ; + add_expected annotated_exp + +(* can_unify_with env goals exp typ takes an annotated expression, and + checks that its annotated type can unify with the provided type. *) +and can_unify_with env goals (E_aux (_, (l, _)) as annotated_exp) typ = + typ_debug (lazy ("Can unify with: from " ^ string_of_typ (typ_of annotated_exp) ^ " to " ^ string_of_typ typ)); + let atyp, env = bind_existential l None (typ_of annotated_exp) env in + let atyp, env = bind_tuple_existentials l None atyp env in + (annotated_exp, unify l env (KidSet.diff goals (ambiguous_vars typ)) typ atyp, env) and bind_pat_no_guard env (P_aux (_, (l, _)) as pat) typ = match bind_pat env pat typ with @@ -4630,9 +4506,7 @@ and infer_exp env (E_aux (exp_aux, (l, uannot)) as exp) = (* Accessing a field of a record *) | Typ_aux (Typ_id rectyp, _) when Env.is_record rectyp env -> begin let inferred_acc = - infer_funapp' l (Env.no_casts env) field (Env.get_accessor_fn rectyp field env) - [strip_exp inferred_exp] - None + infer_funapp' l env field (Env.get_accessor_fn rectyp field env) [strip_exp inferred_exp] None in match inferred_acc with | E_aux (E_app (field, [inferred_exp]), _) -> annot_exp (E_field (inferred_exp, field)) (typ_of inferred_acc) @@ -4641,9 +4515,7 @@ and infer_exp env (E_aux (exp_aux, (l, uannot)) as exp) = (* Not sure if we need to do anything different with args here. *) | Typ_aux (Typ_app (rectyp, _), _) when Env.is_record rectyp env -> begin let inferred_acc = - infer_funapp' l (Env.no_casts env) field (Env.get_accessor_fn rectyp field env) - [strip_exp inferred_exp] - None + infer_funapp' l env field (Env.get_accessor_fn rectyp field env) [strip_exp inferred_exp] None in match inferred_acc with | E_aux (E_app (field, [inferred_exp]), _) -> annot_exp (E_field (inferred_exp, field)) (typ_of inferred_acc) @@ -4939,8 +4811,7 @@ and instantiation_of (E_aux (_, (l, tannot)) as exp) = and instantiation_of_without_type (E_aux (exp_aux, (l, _)) as exp) = let env = env_of exp in match exp_aux with - | E_app (f, xs) -> - instantiation_of (infer_funapp' l (Env.no_casts env) f (Env.get_val_spec f env) (List.map strip_exp xs) None) + | E_app (f, xs) -> instantiation_of (infer_funapp' l env f (Env.get_val_spec f env) (List.map strip_exp xs) None) | _ -> invalid_arg ("instantiation_of expected application, got " ^ string_of_exp exp) and infer_funapp' l env f (typq, f_typ) xs expected_ret_typ = @@ -5040,7 +4911,7 @@ and infer_funapp' l env f (typq, f_typ) xs expected_ret_typ = typ_debug (lazy ("Quantifiers " ^ Util.string_of_list ", " string_of_quant_item !quants)); let inferred_arg = irule infer_exp env arg in let inferred_arg, unifiers, env = - try type_coercion_unify env goals inferred_arg typ with Unification_error (l, m) -> typ_error env l m + try can_unify_with env goals inferred_arg typ with Unification_error (l, m) -> typ_error env l m in record_unifiers unifiers; let unifiers = KBindings.bindings unifiers in @@ -5573,7 +5444,7 @@ let synthesize_val_spec env typq typ id = mk_def (DEF_val (VS_aux - ( VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), Parse_ast.Unknown), id, None, false), + ( VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), Parse_ast.Unknown), id, None), (Parse_ast.Unknown, mk_tannot env typ) ) ) @@ -5720,22 +5591,6 @@ let check_mapdef env def_annot (MD_aux (MD_mapping (id, tannot_opt, mapcls), (l, let env = Env.define_val_spec id env in (vs_def @ [DEF_aux (DEF_mapdef (MD_aux (MD_mapping (id, tannot_opt, mapcls), (l, empty_tannot))), def_annot)], env) -let rec warn_if_unsafe_cast l env = function - | Typ_aux (Typ_fn (arg_typs, ret_typ), _) -> - List.iter (warn_if_unsafe_cast l env) arg_typs; - warn_if_unsafe_cast l env ret_typ - | Typ_aux (Typ_id id, _) when string_of_id id = "bool" -> () - | Typ_aux (Typ_id id, _) when Env.is_enum id env -> () - | Typ_aux (Typ_id id, _) when string_of_id id = "string" -> - Reporting.warn "Unsafe string cast" l - "A cast X -> string is unsafe, as it can cause 'x : X == y : X' to be checked as 'eq_string(cast(x), cast(y))'" - (* If we have a cast to an existential, it's probably done on - purpose and we want to avoid false positives for warnings. *) - | Typ_aux (Typ_exist _, _) -> () - | typ when is_bitvector_typ typ -> () - | typ when is_bit_typ typ -> () - | typ -> Reporting.warn ("Potentially unsafe cast involving " ^ string_of_typ typ) l "" - (* Checking a val spec simply adds the type as a binding in the context. *) let check_val_spec env def_annot (VS_aux (vs, (l, _))) = let annotate vs typq typ = @@ -5743,24 +5598,17 @@ let check_val_spec env def_annot (VS_aux (vs, (l, _))) = in let vs, id, typq, typ, env = match vs with - | VS_val_spec ((TypSchm_aux (TypSchm_ts (typq, typ), ts_l) as typschm), id, exts, is_cast) -> + | VS_val_spec ((TypSchm_aux (TypSchm_ts (typq, typ), ts_l) as typschm), id, exts) -> typ_print (lazy (Util.("Check val spec " |> cyan |> clear) ^ string_of_id id ^ " : " ^ string_of_typschm typschm)); wf_typschm env typschm; let env = match exts with Some exts -> Env.add_extern id exts env | None -> env in - let env = - if is_cast then ( - warn_if_unsafe_cast l env (Env.expand_synonyms env typ); - Env.add_cast id env - ) - else env - in let typq', typ' = expand_bind_synonyms ts_l env (typq, typ) in (* !opt_expand_valspec controls whether the actual valspec in the AST is expanded, the val_spec type stored in the environment is always expanded and uses typq' and typ' *) let typq, typ = if !opt_expand_valspec then (typq', typ') else (typq, typ) in - let vs = VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), ts_l), id, exts, is_cast) in + let vs = VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), ts_l), id, exts) in (vs, id, typq', typ', env) in ([annotate vs typq typ], Env.add_val_spec id (typq, typ) env) @@ -5932,7 +5780,7 @@ and check_outcome : Env.t -> outcome_spec -> uannot def list -> outcome_spec * t let defs, local_env = check_defs local_env defs in let vals = List.filter_map - (function DEF_aux (DEF_val (VS_aux (VS_val_spec (_, id, _, _), _)), _) -> Some id | _ -> None) + (function DEF_aux (DEF_val (VS_aux (VS_val_spec (_, id, _), _)), _) -> Some id | _ -> None) defs in decr depth; diff --git a/src/lib/type_check.mli b/src/lib/type_check.mli index 3b57d98b2..871edaa9a 100644 --- a/src/lib/type_check.mli +++ b/src/lib/type_check.mli @@ -250,16 +250,6 @@ module Env : sig (** Expand type synonyms and remove register annotations (i.e. register -> t)) *) val base_typ_of : t -> typ -> typ - (** no_casts removes all the implicit type casts/coercions from the - environment, so checking a term with such an environment will - guarantee not to insert any casts. Not that this is only about - the implicit casting and has nothing to do with the E_typ AST - node. *) - val no_casts : t -> t - - (** Is casting allowed by the environment? *) - val allow_casts : t -> bool - (** Note: Likely want use Type_check.initial_env instead. The empty environment is lacking even basic builtins. *) val empty : t diff --git a/src/sail_coq_backend/pretty_print_coq.ml b/src/sail_coq_backend/pretty_print_coq.ml index a78b9160b..e56cd2d06 100644 --- a/src/sail_coq_backend/pretty_print_coq.ml +++ b/src/sail_coq_backend/pretty_print_coq.ml @@ -3237,8 +3237,8 @@ let doc_axiom_typschm typ_env is_monadic l (tqs, typ) = string "forall" ^/^ separate space tyvars_pp ^/^ arg_typs_pp ^/^ separate space constrs_pp ^^ comma ^/^ ret_typ_pp | _ -> doc_typschm empty_ctxt typ_env true (TypSchm_aux (TypSchm_ts (tqs, typ), l)) -let doc_val_spec def_annot unimplemented avoid_target_names effect_info - (VS_aux (VS_val_spec (_, id, _, _), (l, ann)) as vs) = +let doc_val_spec def_annot unimplemented avoid_target_names effect_info (VS_aux (VS_val_spec (_, id, _), (l, ann)) as vs) + = let bare_ctxt = { empty_ctxt with avoid_target_names } in if !opt_undef_axioms && IdSet.mem id unimplemented then ( let typ_env = env_of_annot (l, ann) in @@ -3340,7 +3340,7 @@ let find_unimplemented defs = match funcls with [] -> unimplemented | FCL_aux (FCL_funcl (id, _), _) :: _ -> IdSet.remove id unimplemented in let adjust_def unimplemented = function - | DEF_aux (DEF_val (VS_aux (VS_val_spec (_, id, exts, _), _)), _) -> begin + | DEF_aux (DEF_val (VS_aux (VS_val_spec (_, id, exts), _)), _) -> begin match Ast_util.extern_assoc "coq" exts with Some _ -> unimplemented | None -> IdSet.add id unimplemented end | DEF_aux (DEF_internal_mutrec fds, _) -> List.fold_left adjust_fundef unimplemented fds @@ -3351,7 +3351,7 @@ let find_unimplemented defs = let builtin_target_names defs = let check_def names = function - | DEF_aux (DEF_val (VS_aux (VS_val_spec (_, _, exts, _), _)), _) -> begin + | DEF_aux (DEF_val (VS_aux (VS_val_spec (_, _, exts), _)), _) -> begin match Ast_util.extern_assoc "coq" exts with Some name -> StringSet.add name names | None -> names end | _ -> names diff --git a/src/sail_doc_backend/docinfo.ml b/src/sail_doc_backend/docinfo.ml index 1690cf851..e8236cfaa 100644 --- a/src/sail_doc_backend/docinfo.ml +++ b/src/sail_doc_backend/docinfo.ml @@ -412,7 +412,7 @@ module Generator (Converter : Markdown.CONVERTER) (Config : CONFIG) = struct ) def_annot.doc_comment - let docinfo_for_valspec (VS_aux (VS_val_spec ((TypSchm_aux (_, ts_l) as ts), _, _, _), vs_annot) as vs) = + let docinfo_for_valspec (VS_aux (VS_val_spec ((TypSchm_aux (_, ts_l) as ts), _, _), vs_annot) as vs) = { source = doc_loc (fst vs_annot) Type_check.strip_val_spec Pretty_print_sail.doc_spec vs; type_source = doc_loc ts_l (fun ts -> ts) Pretty_print_sail.doc_typschm ts; diff --git a/src/sail_latex_backend/latex.ml b/src/sail_latex_backend/latex.ml index 90243e58d..e55dbdb95 100644 --- a/src/sail_latex_backend/latex.ml +++ b/src/sail_latex_backend/latex.ml @@ -389,7 +389,7 @@ let latex_loc no_loc l = end | None -> docstring l ^^ no_loc -let doc_spec_simple (VS_aux (VS_val_spec (ts, id, ext, is_cast), _)) = +let doc_spec_simple (VS_aux (VS_val_spec (ts, id, ext), _)) = Pretty_print_sail.doc_id id ^^ space ^^ colon ^^ space ^^ Pretty_print_sail.doc_typschm ~simple:true ts let latex_command cat id no_loc l = @@ -510,7 +510,7 @@ let defs { defs; _ } = overload_counters := Bindings.update id (function None -> Some 0 | Some n -> Some (n + 1)) !overload_counters; let count = Bindings.find id !overload_counters in Some (latex_command (Overload count) id doc (id_loc id)) - | DEF_val (VS_aux (VS_val_spec (_, id, _, _), annot) as vs) -> + | DEF_val (VS_aux (VS_val_spec (_, id, _), annot) as vs) -> valspecs := Bindings.add id id !valspecs; if !opt_simple_val then Some (latex_command Val id (doc_spec_simple vs) (fst annot)) else Some (latex_command Val id (Pretty_print_sail.doc_spec vs) (fst annot)) diff --git a/src/sail_lem_backend/pretty_print_lem.ml b/src/sail_lem_backend/pretty_print_lem.ml index c29373ff3..d8a7a716d 100644 --- a/src/sail_lem_backend/pretty_print_lem.ml +++ b/src/sail_lem_backend/pretty_print_lem.ml @@ -1709,13 +1709,13 @@ let doc_dec_lem (DEC_aux (reg, ((l, _) as annot))) = match reg with DEC_reg (typ let doc_spec_lem effect_info params_to_print env (VS_aux (valspec, annot)) = match valspec with - | VS_val_spec (typschm, id, exts, _) when Ast_util.extern_assoc "lem" exts = None -> + | VS_val_spec (typschm, id, exts) when Ast_util.extern_assoc "lem" exts = None -> let monad = if Effects.function_is_pure id effect_info then empty else string "M" ^^ space in (* let (TypSchm_aux (TypSchm_ts (tq, typ), _)) = typschm in if contains_t_pp_var typ then empty else *) separate space [string "val"; doc_id_lem id; string ":"; doc_typschm_lem ~monad params_to_print env true typschm] ^/^ hardline - (* | VS_val_spec (_,_,Some _,_) -> empty *) + (* | VS_val_spec (_,_,Some _) -> empty *) | _ -> empty let is_field_accessor regtypes fdef = diff --git a/src/sail_ocaml_backend/ocaml_backend.ml b/src/sail_ocaml_backend/ocaml_backend.ml index cdf9b8490..430329a5f 100644 --- a/src/sail_ocaml_backend/ocaml_backend.ml +++ b/src/sail_ocaml_backend/ocaml_backend.ml @@ -807,7 +807,7 @@ let ocaml_typedef ctx (TD_aux (td_aux, (l, _))) = | TD_bitfield _ -> Reporting.unreachable l __POS__ "Bitfield should be re-written" let get_externs defs = - let extern_id (VS_aux (VS_val_spec (typschm, id, exts, _), _)) = + let extern_id (VS_aux (VS_val_spec (typschm, id, exts), _)) = match Ast_util.extern_assoc "ocaml" exts with None -> [] | Some ext -> [(id, mk_id ext)] in let rec extern_ids = function @@ -834,8 +834,7 @@ let ocaml_def ctx (DEF_aux (aux, _)) = let val_spec_typs defs = let typs = ref Bindings.empty in let val_spec_typ (VS_aux (vs_aux, _)) = - match vs_aux with - | VS_val_spec (TypSchm_aux (TypSchm_ts (_, typ), _), id, _, _) -> typs := Bindings.add id typ !typs + match vs_aux with VS_val_spec (TypSchm_aux (TypSchm_ts (_, typ), _), id, _) -> typs := Bindings.add id typ !typs in let rec vs_typs = function | DEF_aux (DEF_val vs, _) :: defs -> diff --git a/src/sail_ocaml_backend/sail_plugin_ocaml.ml b/src/sail_ocaml_backend/sail_plugin_ocaml.ml index c68b687f0..b62a57f54 100644 --- a/src/sail_ocaml_backend/sail_plugin_ocaml.ml +++ b/src/sail_ocaml_backend/sail_plugin_ocaml.ml @@ -120,7 +120,6 @@ let ocaml_rewrites = ("exp_lift_assign", []); ("top_sort_defs", []); ("simple_types", []); - ("overload_cast", []); ] let ocaml_target _ default_sail_dir out_file ast effect_info env = diff --git a/test/c/cheri_capreg.sail b/test/c/cheri_capreg.sail index 2a8d325bb..c13d5981b 100644 --- a/test/c/cheri_capreg.sail +++ b/test/c/cheri_capreg.sail @@ -1,19 +1,17 @@ -$option -dallow_cast - default Order dec /* this is here because if we don't have it before including vector_dec we get infinite loops caused by interaction with bool/bit casts */ -val eq_bit2 = "eq_bit" : (bit, bit) -> bool +val eq_bit2 = pure "eq_bit" : (bit, bit) -> bool overload operator == = {eq_bit2} $include -val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg} +val "reg_deref" : forall ('a : Type). register('a) -> 'a /* sneaky deref with no effect necessary for bitfield writes */ -val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a +val _reg_deref = monadic "reg_deref" : forall ('a : Type). register('a) -> 'a -val zeros_0 = "zeros" : forall 'n. int('n) -> bits('n) +val zeros_0 = pure "zeros" : forall 'n. int('n) -> bits('n) val zeros : forall 'n. (implicit('n), unit) -> bits('n) function zeros(n, _) = zeros_0(n) @@ -21,16 +19,14 @@ function zeros(n, _) = zeros_0(n) val ones : forall 'n, 'n >= 0. (implicit('n), unit) -> bits('n) function ones(n, _) = replicate_bits(0b1, n) -val xor_vec = {c: "xor_bits" , _: "xor_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) - -val int_power = {ocaml: "int_power", lem: "pow", coq: "Z.pow"} : (int, int) -> int +val int_power = pure {ocaml: "int_power", lem: "pow", coq: "Z.pow"} : (int, int) -> int overload operator ^ = {xor_vec, int_power} -val cast bool_to_bits : bool -> bits(1) +val bool_to_bits : bool -> bits(1) function bool_to_bits x = if x then 0b1 else 0b0 -val cast bit_to_bool : bit -> bool +val bit_to_bool : bit -> bool function bit_to_bool b = match b { bitone => true, bitzero => false @@ -115,23 +111,23 @@ let 'cap_size = 32 function capRegToCapStruct(capReg) : CapReg -> CapStruct = struct { - tag = capReg[256], + tag = bit_to_bool(capReg[256]), padding = capReg[255..248], otype = capReg[247..224], uperms = capReg[223..208], perm_reserved11_14 = capReg[207..204], - access_system_regs = capReg[203], - permit_unseal = capReg[202], - permit_ccall = capReg[201], - permit_seal = capReg[200], - permit_store_local_cap = capReg[199], - permit_store_cap = capReg[198], - permit_load_cap = capReg[197], - permit_store = capReg[196], - permit_load = capReg[195], - permit_execute = capReg[194], - global = capReg[193], - sealed = capReg[192], + access_system_regs = bit_to_bool(capReg[203]), + permit_unseal = bit_to_bool(capReg[202]), + permit_ccall = bit_to_bool(capReg[201]), + permit_seal = bit_to_bool(capReg[200]), + permit_store_local_cap = bit_to_bool(capReg[199]), + permit_store_cap = bit_to_bool(capReg[198]), + permit_load_cap = bit_to_bool(capReg[197]), + permit_store = bit_to_bool(capReg[196]), + permit_load = bit_to_bool(capReg[195]), + permit_execute = bit_to_bool(capReg[194]), + global = bit_to_bool(capReg[193]), + sealed = bit_to_bool(capReg[192]), address = capReg[191..128], base = capReg[127..64], length = capReg[63..0] @@ -141,17 +137,17 @@ function getCapPerms(cap) : CapStruct -> bits(31) = ( cap.uperms @ cap.perm_reserved11_14 - @ cap.access_system_regs - @ cap.permit_unseal - @ cap.permit_ccall - @ cap.permit_seal - @ cap.permit_store_local_cap - @ cap.permit_store_cap - @ cap.permit_load_cap - @ cap.permit_store - @ cap.permit_load - @ cap.permit_execute - @ cap.global + @ bool_to_bits(cap.access_system_regs) + @ bool_to_bits(cap.permit_unseal) + @ bool_to_bits(cap.permit_ccall) + @ bool_to_bits(cap.permit_seal) + @ bool_to_bits(cap.permit_store_local_cap) + @ bool_to_bits(cap.permit_store_cap) + @ bool_to_bits(cap.permit_load_cap) + @ bool_to_bits(cap.permit_store) + @ bool_to_bits(cap.permit_load) + @ bool_to_bits(cap.permit_execute) + @ bool_to_bits(cap.global) ) @@ -161,7 +157,7 @@ function capStructToMemBits256(cap) : CapStruct -> bits(256) = cap.padding @ cap.otype @ getCapPerms(cap) - @ cap.sealed + @ bool_to_bits(cap.sealed) @ cap.address @ cap.base @ cap.length @@ -178,9 +174,9 @@ function capStructToMemBits(cap) : CapStruct -> bits(256)= capStructToMemBits256(cap) ^ null_cap_bits function memBitsToCapBits(tag, b) : (bool, bits(256)) -> bits(257) = - tag @ (b ^ null_cap_bits) + bool_to_bits(tag) @ (b ^ null_cap_bits) -function capStructToCapReg(cap) : CapStruct -> CapReg = cap.tag @ capStructToMemBits256(cap) +function capStructToCapReg(cap) : CapStruct -> CapReg = bool_to_bits(cap.tag) @ capStructToMemBits256(cap) register DDC : CapReg register C01 : CapReg @@ -195,7 +191,7 @@ let CapRegs : vector(4, dec, register(CapReg)) = ref DDC ] -val readCapReg : bits(2) -> CapStruct effect {rreg} +val readCapReg : bits(2) -> CapStruct function readCapReg(n) = if (n == 0b00) then default_cap @@ -208,11 +204,9 @@ function writeCapReg(n, cap) : (bits(2), CapStruct) -> unit = () else let i = unsigned(n) in - (*CapRegs[i]) = capStructToCapReg(cap) + (*CapRegs[i]) = capStructToCapReg(cap) -val "print_bits" : forall 'n. (string, bits('n)) -> unit - -val main : unit -> unit effect {rreg, wreg} +val main : unit -> unit function main() = { print_bits("default_cap = ", capStructToCapReg(default_cap)); @@ -230,4 +224,4 @@ function main() = { print_bits("C02 = ", C02); print_bits("C01 = ", C01); print_bits("DDC = ", DDC); -} \ No newline at end of file +} diff --git a/test/typecheck/fail/add_vec_lit_old.expect b/test/typecheck/fail/add_vec_lit_old.expect index 023a0b7cf..237fb4dbf 100644 --- a/test/typecheck/fail/add_vec_lit_old.expect +++ b/test/typecheck/fail/add_vec_lit_old.expect @@ -4,14 +4,6 @@  | Cast annotations are deprecated. They will be removed in a future version of the language. -Warning: Potentially unsafe cast involving range(0, (2 ^ 'n - 1)) fail/add_vec_lit_old.sail:9.0-10.44: -9  |val cast unsigned : forall ('n : Int). -  |^------------------------------------- -10 | bitvector('n, inc) -> range(0, 2 ^ 'n - 1) -  |-------------------------------------------^ -  | - - Type error: fail/add_vec_lit_old.sail:14.23-32: 14 |let x : range(0, 30) = 0xF + 0x2 diff --git a/test/typecheck/pass/add_vec_lit.sail b/test/typecheck/pass/add_vec_lit.sail index 05a284d0a..7f1cb5554 100644 --- a/test/typecheck/pass/add_vec_lit.sail +++ b/test/typecheck/pass/add_vec_lit.sail @@ -1,16 +1,14 @@ -$option -dallow_cast - default Order inc +$include val add_vec = pure {ocaml: "add_vec", lem: "add_vec"}: forall ('n : Int). (bitvector('n, inc), bitvector('n, inc)) -> bitvector('n, inc) -val add_range = pure {ocaml: "add_range", lem: "add_range"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). - (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) - -val cast unsigned : forall ('n : Int). +val unsigned : forall ('n : Int). bitvector('n, inc) -> range(0, 2 ^ 'n - 1) overload operator + = {add_vec, add_range} -let x : range(0, 30) = 0xF + 0x2 +let x : range(0, 30) = unsigned(0xF + 0x2) +let y : range(0, 30) = unsigned(0xF) + unsigned(0x2) + diff --git a/test/typecheck/pass/enum_cast.sail b/test/typecheck/pass/enum_cast.sail index d7d672772..24f8e0659 100644 --- a/test/typecheck/pass/enum_cast.sail +++ b/test/typecheck/pass/enum_cast.sail @@ -1,17 +1,12 @@ -$option -dallow_cast - default Order dec $include enum E = {A, B, C} -val cast E_typ : E -> {'e, 0 <= 'e <= 2. atom('e)} -function E_typ(e) = num_of_E(e) - val main : unit -> unit function main() = { let x : vector(3, dec, int) = [1, 2, 3]; - print_int("x = ", x[B]) + print_int("x = ", x[num_of_E(B)]) } diff --git a/test/typecheck/pass/while_MM.sail b/test/typecheck/pass/while_MM.sail index b40d9574a..5223c9ff4 100644 --- a/test/typecheck/pass/while_MM.sail +++ b/test/typecheck/pass/while_MM.sail @@ -1,27 +1,19 @@ -$option -dallow_cast - default Order dec -val add_range = {ocaml: "add", lem: "add"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). - (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) - val add_int = {ocaml: "add", lem: "add"}: (int, int) -> int val add_vec_int : forall ('n : Int) ('ord : Order). - (vector('n, 'ord, bit), int) -> vector('n, 'ord, bit) + (bitvector('n, 'ord), int) -> bitvector('n, 'ord) overload operator + = {add_vec_int, add_range, add_int} val bool_not = pure {ocaml: "not", lem: "not"}: bool -> bool -val cast cast_0_vec_dec : forall ('l : Int). - atom(0) -> vector('l, dec, bit) - -register COUNT : vector(64, dec, bit) +register COUNT : bitvector(64, dec) register INT : bool function test () -> unit = { - COUNT = 0; + COUNT = 0x0000_0000_0000_0000; while bool_not(INT) do COUNT = COUNT + 1 }