From cfa23d306243789c67729da729cc265e9f98232b Mon Sep 17 00:00:00 2001 From: Alasdair Date: Fri, 1 Dec 2023 00:11:56 +0000 Subject: [PATCH] Make undefined generation more strict `undefined` is now forbidden for scattered types `undefined` is forbidden for unions in general This is slightly breaking as registers with union types must now have an initial value. However this does not appear to be done in practice. I wanted to restrict to finite types (which works for sail-riscv) but ASL allows undefined ints and reals :( The `-undefined_gen` flag is removed, as we handle undefined the same across all backends. --- src/bin/sail.ml | 10 +- src/lib/ast_util.ml | 3 + src/lib/ast_util.mli | 2 + src/lib/initial_check.ml | 179 +++++------------- src/lib/initial_check.mli | 8 +- src/lib/rewrites.ml | 3 +- src/lib/scattered.ml | 6 +- src/lib/state.ml | 14 +- src/lib/type_check.ml | 121 ++++++++++-- src/lib/type_env.ml | 22 ++- src/lib/type_env.mli | 10 +- src/sail_c_backend/sail_plugin_c.ml | 5 +- src/sail_lem_backend/sail_plugin_lem.ml | 10 +- src/sail_ocaml_backend/sail_plugin_ocaml.ml | 5 +- test/c/pc_no_wildcard.sail | 2 +- test/c/undefined_nat.sail | 4 +- test/c/{warl_undef.expect => warl2.expect} | 0 test/c/{warl_undef.sail => warl2.sail} | 4 +- .../fail/negative_bits_existential.expect | 2 +- .../fail/negative_bits_struct.expect | 2 +- .../fail/negative_bits_struct2.expect | 2 +- .../typecheck/fail/negative_bits_tuple.expect | 2 +- .../typecheck/fail/negative_bits_union.expect | 2 +- .../fail/negative_bits_union2.expect | 5 + .../negative_bits_union2.sail} | 3 +- test/typecheck/fail/procstate1.expect | 5 + test/typecheck/fail/procstate1.sail | 16 ++ test/typecheck/pass/inline_typ.sail | 5 +- test/typecheck/pass/negative_bits_list.sail | 1 - .../pass/negative_bits_list/v1.expect | 8 +- .../typecheck/pass/negative_bits_list/v1.sail | 1 - .../pass/negative_bits_list/v2.expect | 5 + .../typecheck/pass/negative_bits_list/v2.sail | 11 ++ test/typecheck/pass/procstate1.sail | 2 +- test/typecheck/pass/pure_record2.sail | 4 +- test/typecheck/pass/pure_record3.sail | 4 +- test/typecheck/pass/reg_list.sail | 3 +- test/typecheck/pass/reg_option.sail | 2 +- 38 files changed, 267 insertions(+), 226 deletions(-) rename test/c/{warl_undef.expect => warl2.expect} (100%) rename test/c/{warl_undef.sail => warl2.sail} (83%) create mode 100644 test/typecheck/fail/negative_bits_union2.expect rename test/typecheck/{pass/negative_bits_union.sail => fail/negative_bits_union2.sail} (60%) create mode 100644 test/typecheck/fail/procstate1.expect create mode 100644 test/typecheck/fail/procstate1.sail create mode 100644 test/typecheck/pass/negative_bits_list/v2.expect create mode 100644 test/typecheck/pass/negative_bits_list/v2.sail diff --git a/src/bin/sail.ml b/src/bin/sail.ml index 1efb86971..4c685e420 100644 --- a/src/bin/sail.ml +++ b/src/bin/sail.ml @@ -192,7 +192,6 @@ let rec options = Arg.Set Interactive.opt_interactive; Arg.Unit (fun () -> Preprocess.add_symbol "INTERACTIVE"); Arg.Set opt_auto_interpreter_rewrites; - Arg.Set Initial_check.opt_undefined_gen; ], " start interactive interpreter" ); @@ -202,7 +201,6 @@ let rec options = Arg.Set Interactive.opt_interactive; Arg.Unit (fun () -> Preprocess.add_symbol "INTERACTIVE"); Arg.Set opt_auto_interpreter_rewrites; - Arg.Set Initial_check.opt_undefined_gen; Arg.String (fun s -> opt_interactive_script := Some s); ], " start interactive interpreter and execute commands in script" @@ -255,10 +253,6 @@ let rec options = Arg.Set Type_env.opt_string_literal_type, " use a separate string_literal type for string literals" ); - ( "-undefined_gen", - Arg.Set Initial_check.opt_undefined_gen, - " generate undefined_type functions for types in the specification" - ); ( "-grouped_regstate", Arg.Set State.opt_type_grouped_regstate, " group registers with same type together in generated register state record" @@ -346,6 +340,10 @@ let rec options = Arg.Unit (fun () -> Reporting.simple_warn "-infer_effects option is deprecated"), " (deprecated) ignored for compatibility with older versions; effects are always inferred now" ); + ( "-undefined_gen", + Arg.Unit (fun () -> ()), + " (deprecated) ignored as undefined generation is now always the same for all Sail backends" + ); ("-v", Arg.Set opt_print_version, " print version"); ("-version", Arg.Set opt_print_version, " print version"); ("-verbose", Arg.Int (fun verbosity -> Util.opt_verbosity := verbosity), " produce verbose output"); diff --git a/src/lib/ast_util.ml b/src/lib/ast_util.ml index 8fb96afdb..2656c5475 100644 --- a/src/lib/ast_util.ml +++ b/src/lib/ast_util.ml @@ -100,6 +100,9 @@ let add_def_attribute l attr arg (annot : def_annot) = { annot with attrs = (l, let get_def_attribute attr (annot : def_annot) = List.find_opt (fun (_, attr', _) -> attr = attr') annot.attrs |> Option.map (fun (l, _, arg) -> (l, arg)) +let remove_def_attribute attr (annot : def_annot) = + { annot with attrs = List.filter (fun (_, attr', _) -> attr <> attr') annot.attrs } + type mut = Immutable | Mutable type 'a lvar = Register of 'a | Enum of 'a | Local of mut * 'a | Unbound of id diff --git a/src/lib/ast_util.mli b/src/lib/ast_util.mli index 5748e8c85..5b9001363 100644 --- a/src/lib/ast_util.mli +++ b/src/lib/ast_util.mli @@ -103,6 +103,8 @@ val add_def_attribute : l -> string -> string -> def_annot -> def_annot val get_def_attribute : string -> def_annot -> (l * string) option +val remove_def_attribute : string -> def_annot -> def_annot + val def_annot_map_loc : (l -> l) -> def_annot -> def_annot (** The empty annotation (as a location + uannot pair). Should be used diff --git a/src/lib/initial_check.ml b/src/lib/initial_check.ml index 96860ac73..684a4ebb7 100644 --- a/src/lib/initial_check.ml +++ b/src/lib/initial_check.ml @@ -75,7 +75,6 @@ module Big_int = Nat_big_num module P = Parse_ast (* See mli file for details on what these flags do *) -let opt_undefined_gen = ref false let opt_fast_undefined = ref false let opt_magic_hash = ref false @@ -1459,18 +1458,22 @@ let extern_of_string ?(pure = false) id str = 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))] - | QI_aux (QI_id kopt, _) when is_typ_kopt kopt -> [prepend_id "typ_" (id_of_kid (kopt_kid kopt))] - | _ -> [] -let quant_item_typ = function - | QI_aux (QI_id kopt, _) when is_int_kopt kopt -> [atom_typ (nvar (kopt_kid kopt))] - | QI_aux (QI_id kopt, _) when is_typ_kopt kopt -> [mk_typ (Typ_var (kopt_kid kopt))] +let quant_item_param_typ = function + | QI_aux (QI_id kopt, _) when is_int_kopt kopt -> + [(prepend_id "atom_" (id_of_kid (kopt_kid kopt)), atom_typ (nvar (kopt_kid kopt)))] + | QI_aux (QI_id kopt, _) when is_typ_kopt kopt -> + [(prepend_id "typ_" (id_of_kid (kopt_kid kopt)), mk_typ (Typ_var (kopt_kid kopt)))] | _ -> [] + +let quant_item_param qi = List.map fst (quant_item_param_typ qi) + +let quant_item_typ qi = List.map snd (quant_item_param_typ qi) + let quant_item_arg = function | QI_aux (QI_id kopt, _) when is_int_kopt kopt -> [mk_typ_arg (A_nexp (nvar (kopt_kid kopt)))] | QI_aux (QI_id kopt, _) when is_typ_kopt kopt -> [mk_typ_arg (A_typ (mk_typ (Typ_var (kopt_kid kopt))))] | _ -> [] + let undefined_typschm id typq = let qis = quant_items typq in if qis = [] then mk_typschm typq (function_typ [unit_typ] (mk_typ (Typ_id id))) @@ -1480,6 +1483,37 @@ let undefined_typschm id typq = mk_typschm typq (function_typ arg_typs ret_typ) ) +let generate_undefined_record_context typq = + quant_items typq |> List.map (fun qi -> quant_item_param_typ qi) |> List.concat + +let generate_undefined_record id typq fields = + let p_tup = function [pat] -> pat | pats -> mk_pat (P_tuple pats) in + let pat = + 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)); + mk_fundef + [ + mk_funcl (prepend_id "undefined_" id) pat + (mk_exp (E_struct (List.map (fun (_, id) -> mk_fexp id (mk_lit_exp L_undef)) fields))); + ]; + ] + +let generate_undefined_enum id ids = + let typschm = typschm_of_string ("unit -> " ^ string_of_id id) in + [ + mk_val_spec (VS_val_spec (typschm, prepend_id "undefined_" id, None)); + mk_fundef + [ + mk_funcl (prepend_id "undefined_" id) + (mk_pat (P_lit (mk_lit L_unit))) + ( if !opt_fast_undefined && List.length ids > 0 then mk_exp (E_id (List.hd ids)) + else mk_exp (E_app (mk_id "internal_pick", [mk_exp (E_list (List.map (fun id -> mk_exp (E_id id)) ids))])) + ); + ]; + ] + let have_undefined_builtins = ref false let undefined_builtin_val_specs = @@ -1510,131 +1544,7 @@ let generate_undefineds vs_ids defs = List.filter (fun def -> IdSet.is_empty (IdSet.inter vs_ids (ids_of_def def))) undefined_builtin_val_specs end in - let undefined_tu = function - | Tu_aux (Tu_ty_id (Typ_aux (Typ_tuple typs, _), id), _) -> - mk_exp (E_app (id, List.map (fun typ -> mk_exp (E_typ (typ, mk_lit_exp L_undef))) typs)) - | Tu_aux (Tu_ty_id (typ, id), _) -> mk_exp (E_app (id, [mk_exp (E_typ (typ, mk_lit_exp L_undef))])) - in - let p_tup = function [pat] -> pat | pats -> mk_pat (P_tuple pats) in - let undefined_union id typq tus = - let pat = - p_tup (quant_items typq |> List.map quant_item_param |> List.concat |> List.map (fun id -> mk_pat (P_id id))) - in - let body = - if !opt_fast_undefined && List.length tus > 0 then undefined_tu (List.hd tus) - else ( - (* Deduplicate arguments for each constructor to keep definitions - manageable. *) - let extract_tu = function - | Tu_aux (Tu_ty_id (Typ_aux (Typ_tuple typs, _), id), _) -> (id, typs) - | Tu_aux (Tu_ty_id (typ, id), _) -> (id, [typ]) - in - let record_arg_typs m (_, typs) = - let m' = - List.fold_left - (fun m typ -> TypMap.add typ (1 + try TypMap.find typ m with Not_found -> 0) m) - TypMap.empty typs - in - TypMap.merge - (fun _ x y -> match (x, y) with Some m, Some n -> Some (max m n) | None, x -> x | x, None -> x) - m m' - in - let make_undef_var typ n (i, lbs, m) = - let j = i + n in - let rec aux k = - if k = j then [] - else ( - let v = mk_id ("u_" ^ string_of_int k) in - mk_letbind (mk_pat (P_typ (typ, mk_pat (P_id v)))) (mk_lit_exp L_undef) :: aux (k + 1) - ) - in - (j, aux i @ lbs, TypMap.add typ i m) - in - let make_constr m (id, typs) = - let args, _ = - List.fold_right - (fun typ (acc, m) -> - let i = TypMap.find typ m in - (mk_exp (E_id (mk_id ("u_" ^ string_of_int i))) :: acc, TypMap.add typ (i + 1) m) - ) - typs ([], m) - in - mk_exp (E_app (id, args)) - in - let constr_args = List.map extract_tu tus in - let typs_needed = List.fold_left record_arg_typs TypMap.empty constr_args in - let _, letbinds, typ_to_var = TypMap.fold make_undef_var typs_needed (0, [], TypMap.empty) in - List.fold_left - (fun e lb -> mk_exp (E_let (lb, e))) - (mk_exp (E_app (mk_id "internal_pick", [mk_exp (E_list (List.map (make_constr typ_to_var) constr_args))]))) - letbinds - ) - in - ( 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 - let undefined_td = function - | 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)); - mk_fundef - [ - mk_funcl (prepend_id "undefined_" id) - (mk_pat (P_lit (mk_lit L_unit))) - ( if !opt_fast_undefined && List.length ids > 0 then mk_exp (E_id (List.hd ids)) - else - mk_exp (E_app (mk_id "internal_pick", [mk_exp (E_list (List.map (fun id -> mk_exp (E_id id)) ids))])) - ); - ]; - ] - | TD_record (id, typq, fields, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) -> - let pat = - 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)); - mk_fundef - [ - mk_funcl (prepend_id "undefined_" id) pat - (mk_exp (E_struct (List.map (fun (_, id) -> mk_fexp id (mk_lit_exp L_undef)) fields))); - ]; - ] - | TD_variant (id, typq, tus, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) -> - let vs, def = undefined_union id typq tus in - [vs; def] - | _ -> [] - in - let undefined_scattered id typq = - let tus = get_scattered_union_clauses id defs in - undefined_union id typq tus - in - let rec undefined_defs = function - | (DEF_aux (DEF_type (TD_aux (td_aux, _)), _) as def) :: defs -> - (def :: List.map make_global (undefined_td td_aux)) @ undefined_defs defs - (* The function definition must come after the scattered type definition is complete, so put it at the end. *) - | (DEF_aux (DEF_scattered (SD_aux (SD_variant (id, typq), _)), _) as def) :: defs -> - let vs, fn = undefined_scattered id typq in - (def :: make_global vs :: undefined_defs defs) @ [make_global fn] - | (DEF_aux (DEF_scattered (SD_aux (SD_internal_unioncl_record (_, id, typq, fields), _)), _) as def) :: defs - when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) -> - let pat = - p_tup (quant_items typq |> List.map quant_item_param |> List.concat |> List.map (fun id -> mk_pat (P_id id))) - in - let vs = mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, None)) in - let fn = - mk_fundef - [ - mk_funcl (prepend_id "undefined_" id) pat - (mk_exp (E_struct (List.map (fun (_, id) -> mk_fexp id (mk_lit_exp L_undef)) fields))); - ] - in - def :: make_global vs :: make_global fn :: undefined_defs defs - | def :: defs -> def :: undefined_defs defs - | [] -> [] - in - undefined_builtins @ undefined_defs defs + undefined_builtins @ defs let rec get_uninitialized_registers = function | DEF_aux (DEF_register (DEC_aux (DEC_reg (typ, id, None), _)), _) :: defs -> @@ -1732,8 +1642,7 @@ let process_ast ?(generate = true) ast = let ast, ctx = to_ast !incremental_ctx ast in incremental_ctx := ctx; let vs_ids = val_spec_ids ast.defs in - if (not !opt_undefined_gen) && generate then { ast with defs = generate_enum_functions vs_ids ast.defs } - else if generate then + if generate then { ast with defs = diff --git a/src/lib/initial_check.mli b/src/lib/initial_check.mli index cbb7c92c1..96b4760c8 100644 --- a/src/lib/initial_check.mli +++ b/src/lib/initial_check.mli @@ -77,10 +77,6 @@ val merge_ctx : Parse_ast.l -> ctx -> ctx -> ctx (** {2 Options} *) -(** Generate undefined_T functions for every type T. False by - default. *) -val opt_undefined_gen : bool ref - (** Generate faster undefined_T functions. Rather than generating functions that allow for the undefined values of enums and variants to be picked at runtime using a RNG or similar, this creates @@ -111,6 +107,10 @@ val undefined_builtin_val_specs : uannot def list (** {2 Desugar and process AST } *) +val generate_undefined_record_context : typquant -> (id * typ) list +val generate_undefined_record : id -> typquant -> (typ * id) list -> uannot def list +val generate_undefined_enum : id -> id list -> uannot def list + val generate_undefineds : IdSet.t -> uannot def list -> uannot def list val generate_enum_functions : IdSet.t -> uannot def list -> uannot def list diff --git a/src/lib/rewrites.ml b/src/lib/rewrites.ml index 0873a8fa1..053b0cbfd 100644 --- a/src/lib/rewrites.ml +++ b/src/lib/rewrites.ml @@ -2016,8 +2016,7 @@ let rewrite_undefined mwords env = rewrite_ast_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_exp_undefined) } let rewrite_undefined_if_gen always_bitvector env defs = - if !Initial_check.opt_undefined_gen then rewrite_undefined (always_bitvector || !Monomorphise.opt_mwords) env defs - else defs + rewrite_undefined (always_bitvector || !Monomorphise.opt_mwords) env defs let rec simple_typ (Typ_aux (typ_aux, l)) = Typ_aux (simple_typ_aux l typ_aux, l) diff --git a/src/lib/scattered.ml b/src/lib/scattered.ml index 0db9977b5..56a29d990 100644 --- a/src/lib/scattered.ml +++ b/src/lib/scattered.ml @@ -194,7 +194,11 @@ let rec descatter' accumulator funcls mapcls = function match members with | [] -> raise (Reporting.err_general l "No clauses found for scattered enum type") | _ -> - let def_annot = add_def_attribute (gen_loc l) "no_enum_functions" "" def_annot in + let def_annot = + def_annot + |> add_def_attribute (gen_loc l) "no_enum_functions" "" + |> add_def_attribute (gen_loc l) "undefined_gen" "forbid" + in let accumulator = DEF_aux (DEF_type (TD_aux (TD_enum (id, members, false), (gen_loc l, Type_check.empty_tannot))), def_annot) :: accumulator diff --git a/src/lib/state.ml b/src/lib/state.ml index b923f0c7e..4c4acedf0 100644 --- a/src/lib/state.ml +++ b/src/lib/state.ml @@ -142,7 +142,12 @@ let generate_regstate env registers = TD_record (mk_id "regstate", mk_typquant [], fields, false) ) in - [DEF_aux (DEF_type (TD_aux (regstate_def, (Unknown, empty_uannot))), mk_def_annot Unknown)] + [ + DEF_aux + ( DEF_type (TD_aux (regstate_def, (Unknown, empty_uannot))), + add_def_attribute Unknown "undefined_gen" "forbid" (mk_def_annot Unknown) + ); + ] let generate_initial_regstate env ast = let initial_values = @@ -838,12 +843,6 @@ let register_refs_coq doc_id env registers = let generate_regstate_defs env ast = let defs = ast.defs in - (* FIXME We currently don't want to generate undefined_type functions - for register state and values. For the Lem backend, this would require - taking the dependencies of those functions into account when partitioning - definitions into the different lem files, which we currently don't do. *) - let gen_undef = !Initial_check.opt_undefined_gen in - Initial_check.opt_undefined_gen := false; let registers = find_registers defs in let regtyps = List.map (fun (x, _, _) -> x) registers in let base_regtyps = register_base_types env regtyps in @@ -869,7 +868,6 @@ let generate_regstate_defs env ast = in let typdefs, defs = List.partition (function DEF_aux (DEF_type _, _) -> true | _ -> false) defs in let valspecs, defs = List.partition (function DEF_aux (DEF_val _, _) -> true | _ -> false) defs in - Initial_check.opt_undefined_gen := gen_undef; typdefs @ valspecs @ defs let add_regstate_defs mwords env ast = diff --git a/src/lib/type_check.ml b/src/lib/type_check.ml index 06f02d5a9..7baa0f5f7 100644 --- a/src/lib/type_check.ml +++ b/src/lib/type_check.ml @@ -1277,6 +1277,33 @@ and rewrite_nc_aux l env = (* Would be better to translate change E_sizeof to take a kid, then rewrite to E_sizeof *) E_id (id_of_kid v) +let can_be_undefined ~at:l env typ = + let rec check (Typ_aux (aux, _)) = + match aux with + | Typ_fn _ | Typ_bidir _ | Typ_exist _ | Typ_var _ -> false + | Typ_id (Id_aux (Id name, _) as id) -> + name = "bool" || name = "bit" || name = "nat" || name = "int" || name = "real" || name = "string" + || Env.is_bitfield id env || Env.is_user_undefined id env + | Typ_id _ -> false + | Typ_app ((Id_aux (Id name, _) as id), args) -> + (name = "bitvector" || name = "vector" || name = "range" || Env.is_user_undefined id env) + && List.for_all check_arg args + | Typ_app _ -> false + | Typ_tuple typs -> List.for_all check typs + | Typ_internal_unknown -> Reporting.unreachable l __POS__ "unexpected Typ_internal_unknown" + and check_arg (A_aux (aux, _)) = + match aux with + | A_nexp nexp -> ( + try + let _ = rewrite_sizeof l env nexp in + true + with Type_error _ -> false + ) + | A_typ typ -> check typ + | A_bool _ -> true + in + check (Env.expand_synonyms env typ) + (**************************************************************************) (* 5. Type checking expressions *) (**************************************************************************) @@ -2099,11 +2126,10 @@ let rec check_exp env (E_aux (exp_aux, (l, uannot)) as exp : uannot exp) (Typ_au if prove __POS__ env (nc_eq (nint (List.length vec)) (nexp_simp len)) then annot_exp (E_vector checked_items) typ else typ_error l "Vector literal with incorrect length" (* FIXME: improve error message *) | E_lit (L_aux (L_undef, _) as lit), _ -> - if is_typ_monomorphic typ || Env.polymorphic_undefineds env then - if is_typ_inhabited env (Env.expand_synonyms env typ) || Env.polymorphic_undefineds env then - annot_exp (E_lit lit) typ - else typ_error l ("Type " ^ string_of_typ typ ^ " is empty") - else typ_error l ("Type " ^ string_of_typ typ ^ " must be monomorphic") + if can_be_undefined ~at:l env typ then + if is_typ_inhabited env (Env.expand_synonyms env typ) then annot_exp (E_lit lit) typ + else typ_error l ("Type " ^ string_of_typ typ ^ " could be empty") + else typ_error l ("Type " ^ string_of_typ typ ^ " cannot be undefined") | E_internal_assume (nc, exp), _ -> Env.wf_constraint env nc; let env = Env.add_constraint nc env in @@ -3921,16 +3947,6 @@ let bind_funcl_arg_typ l env typ = let check_funcl env (FCL_aux (FCL_funcl (id, pexp), (def_annot, _))) typ = let l = def_annot.loc in let typ_arg, typ_ret, env = bind_funcl_arg_typ l env typ in - (* We want to forbid polymorphic undefined values in all cases, - except when type checking the specific undefined_(type) functions - created by the -undefined_gen functions in initial_check.ml. Only - in these functions will the rewriter be able to correctly - re-write the polymorphic undefineds (due to the specific form the - functions have *) - let env = - if Str.string_match (Str.regexp_string "undefined_") (string_of_id id) 0 then Env.allow_polymorphic_undefineds env - else env - in let typed_pexp = check_case env typ_arg pexp typ_ret in FCL_aux (FCL_funcl (id, typed_pexp), (def_annot, mk_expected_tannot env typ (Some typ))) @@ -4253,7 +4269,53 @@ let rec check_typedef : Env.t -> def_annot -> uannot type_def -> tannot def list ([DEF_aux (DEF_type (TD_aux (tdef, (l, empty_tannot))), def_annot)], Env.add_typ_synonym id typq typ_arg env) | TD_record (id, typq, fields, _) -> let env = check_record l env def_annot id typq fields in - ([DEF_aux (DEF_type (TD_aux (tdef, (l, empty_tannot))), def_annot)], env) + begin + match get_def_attribute "undefined_gen" def_annot with + | Some (_, "forbid") -> ([DEF_aux (DEF_type (TD_aux (tdef, (l, empty_tannot))), def_annot)], env) + | Some (_, "skip") -> + ([DEF_aux (DEF_type (TD_aux (tdef, (l, empty_tannot))), def_annot)], Env.allow_user_undefined id env) + | (Some (_, "generate") | None) as attr -> + let field_env = Env.add_typquant l typq env in + let field_env = + List.fold_left + (fun env (id, typ) -> Env.add_local id (Immutable, typ) env) + field_env + (Initial_check.generate_undefined_record_context typq) + in + let gen_undefined = + List.for_all (fun (typ, field_id) -> can_be_undefined ~at:(id_loc field_id) field_env typ) fields + in + if (not gen_undefined) && Option.is_none attr then ( + (* If we cannot generate an undefined value, and we weren't explicitly asked to *) + let def_annot = add_def_attribute (gen_loc l) "undefined_gen" "forbid" def_annot in + ([DEF_aux (DEF_type (TD_aux (tdef, (l, empty_tannot))), def_annot)], env) + ) + else if not gen_undefined then + (* If we cannot generate an undefined value, but we were + explicitly told to then it's an error. *) + typ_error l ("Cannot generate undefined function for struct " ^ string_of_id id) + else ( + let undefined_defs = Initial_check.generate_undefined_record id typq fields in + try + let undefined_defs, env = check_defs env undefined_defs in + let def_annot = + def_annot |> remove_def_attribute "undefined_gen" + |> add_def_attribute (gen_loc l) "undefined_gen" "skip" + in + ( DEF_aux (DEF_type (TD_aux (tdef, (l, empty_tannot))), def_annot) :: undefined_defs, + Env.allow_user_undefined id env + ) + with + | Type_error _ when Option.is_none attr -> + let def_annot = add_def_attribute (gen_loc l) "undefined_gen" "forbid" def_annot in + ([DEF_aux (DEF_type (TD_aux (tdef, (l, empty_tannot))), def_annot)], env) + | Type_error _ -> typ_error l ("Cannot generate undefined function for struct " ^ string_of_id id) + ) + | Some (attr_l, arg) -> + typ_error + (Hint ("When checking this struct", l, attr_l)) + ("Unrecognized argument to undefined attribute: " ^ arg) + end | TD_variant (id, typq, arms, _) -> let rec_env = Env.add_variant id (typq, arms) env in (* register_value is a special type used by theorem prover @@ -4263,7 +4325,27 @@ let rec check_typedef : Env.t -> def_annot -> uannot type_def -> tannot def list rec_env |> fun env -> List.fold_left (fun env tu -> check_type_union l non_rec_env env id typq tu) env arms in ([DEF_aux (DEF_type (TD_aux (tdef, (l, empty_tannot))), def_annot)], env) - | TD_enum (id, ids, _) -> ([DEF_aux (DEF_type (TD_aux (tdef, (l, empty_tannot))), def_annot)], Env.add_enum id ids env) + | TD_enum (id, ids, _) -> + let env = Env.add_enum id ids env in + begin + match get_def_attribute "undefined_gen" def_annot with + | Some (_, "forbid") -> ([DEF_aux (DEF_type (TD_aux (tdef, (l, empty_tannot))), def_annot)], env) + | Some (_, "skip") -> + ([DEF_aux (DEF_type (TD_aux (tdef, (l, empty_tannot))), def_annot)], Env.allow_user_undefined id env) + | Some (_, "generate") | None -> + let undefined_defs = Initial_check.generate_undefined_enum id ids in + let undefined_defs, env = check_defs env undefined_defs in + let def_annot = + def_annot |> remove_def_attribute "undefined_gen" |> add_def_attribute (gen_loc l) "undefined_gen" "skip" + in + ( DEF_aux (DEF_type (TD_aux (tdef, (l, empty_tannot))), def_annot) :: undefined_defs, + Env.allow_user_undefined id env + ) + | Some (attr_l, arg) -> + typ_error + (Hint ("When checking this enum", l, attr_l)) + ("Unrecognized argument to undefined attribute: " ^ arg) + end | TD_bitfield (id, typ, ranges) as unexpanded -> let typ = Env.expand_synonyms env typ in begin @@ -4289,9 +4371,6 @@ let rec check_typedef : Env.t -> def_annot -> uannot type_def -> tannot def list DEF_aux (DEF_type (TD_aux (record_tdef, (l, empty_uannot))), def_annot) :: Bitfield.macro id size (Env.get_default_order env) ranges in - let defs = - if !Initial_check.opt_undefined_gen then Initial_check.generate_undefineds IdSet.empty defs else defs - in let defs, env = try check_defs env defs with Type_error (inner_l, err) -> @@ -4513,6 +4592,8 @@ and check_def : Env.t -> uannot def -> tannot def list * Env.t = | DEF_default default -> check_default env def_annot default | DEF_overload (id, ids) -> ([DEF_aux (DEF_overload (id, ids), def_annot)], Env.add_overloads def_annot.loc id ids env) | DEF_register (DEC_aux (DEC_reg (typ, id, None), (l, _))) -> + if not (can_be_undefined ~at:l env typ) then + typ_error l ("Must provide a default register value for a register of type " ^ string_of_typ typ); let env = Env.add_register id typ env in ( [ DEF_aux diff --git a/src/lib/type_env.ml b/src/lib/type_env.ml index 42d51403d..b6dd96ae3 100644 --- a/src/lib/type_env.ml +++ b/src/lib/type_env.ml @@ -113,6 +113,7 @@ type global_env = { synonyms : (typquant * typ_arg) env_item Bindings.t; accessors : (typquant * typ) env_item IdPairMap.t; bitfields : (typ * index_range Bindings.t) env_item Bindings.t; + allow_undefined : IdSet.t; letbinds : typ env_item Bindings.t; registers : typ env_item Bindings.t; overloads : id list multiple_env_item Bindings.t; @@ -136,6 +137,7 @@ let empty_global_env = accessors = IdPairMap.empty; synonyms = Bindings.empty; bitfields = Bindings.empty; + allow_undefined = IdSet.empty; letbinds = Bindings.empty; registers = Bindings.empty; overloads = Bindings.empty; @@ -154,7 +156,6 @@ type env = { allow_bindings : bool; constraints : (constraint_reason * n_constraint) list; ret_typ : typ option; - poly_undefineds : bool; prove : (env -> n_constraint -> bool) option; allow_unknowns : bool; toplevel : l option; @@ -243,7 +244,6 @@ let empty = allow_bindings = true; constraints = []; ret_typ = None; - poly_undefineds = false; prove = None; allow_unknowns = false; toplevel = None; @@ -273,6 +273,11 @@ let set_prover f env = { env with prove = f } let allow_unknowns env = env.allow_unknowns let set_allow_unknowns b env = { env with allow_unknowns = b } +let is_user_undefined id env = IdSet.mem id env.global.allow_undefined + +let allow_user_undefined id env = + update_global (fun global -> { global with allow_undefined = IdSet.add id global.allow_undefined }) env + (* First, we define how type variables are added to the environment. If we add a new variable shadowing a previous variable, we need to modify the environment so the shadowed @@ -1168,9 +1173,14 @@ let add_enum_clause id member env = ("Enumeration " ^ string_of_id id ^ " is not scattered - cannot add a new member with 'enum clause'") | None -> typ_error (id_loc id) ("Enumeration " ^ string_of_id id ^ " does not exist") -let get_enum id env = +let get_enum_opt id env = match Option.map (get_item (id_loc id) env) (Bindings.find_opt id env.global.enums) with - | Some (_, enum) -> IdSet.elements enum + | Some (_, enum) -> Some (IdSet.elements enum) + | None -> None + +let get_enum id env = + match get_enum_opt id env with + | Some enum -> enum | None -> typ_error (id_loc id) ("Enumeration " ^ string_of_id id ^ " does not exist") let get_enums env = filter_items_with snd env env.global.enums @@ -1447,8 +1457,4 @@ let add_bitfield id typ ranges env = ) env -let allow_polymorphic_undefineds env = { env with poly_undefineds = true } - -let polymorphic_undefineds env = env.poly_undefineds - let is_toplevel env = env.toplevel diff --git a/src/lib/type_env.mli b/src/lib/type_env.mli index b598ae491..6b495de16 100644 --- a/src/lib/type_env.mli +++ b/src/lib/type_env.mli @@ -132,6 +132,12 @@ val add_outcome_variable : l -> kid -> typ -> t -> t val set_outcome_typschm : outcome_loc:l -> typquant * typ -> t -> t val get_outcome_typschm_opt : t -> (typquant * typ) option +(** For a user-defined type identifier we can control whether it is + allowed to be created with the undefined literal in Sail *) +val is_user_undefined : id -> t -> bool + +val allow_user_undefined : id -> t -> t + val is_variant : id -> t -> bool val add_variant : id -> typquant * type_union list -> t -> t val add_scattered_variant : id -> typquant -> t -> t @@ -208,12 +214,10 @@ val get_extern : id -> t -> string -> string val add_enum : id -> id list -> t -> t val add_scattered_enum : id -> t -> t val add_enum_clause : id -> id -> t -> t +val get_enum_opt : id -> t -> id list option val get_enum : id -> t -> id list val get_enums : t -> IdSet.t Bindings.t -val allow_polymorphic_undefineds : t -> t -val polymorphic_undefineds : t -> bool - val lookup_id : id -> t -> typ lvar val expand_synonyms : t -> typ -> typ diff --git a/src/sail_c_backend/sail_plugin_c.ml b/src/sail_c_backend/sail_plugin_c.ml index cab9ecb92..6d9c4f4ff 100644 --- a/src/sail_c_backend/sail_plugin_c.ml +++ b/src/sail_c_backend/sail_plugin_c.ml @@ -164,7 +164,4 @@ let c_target _ _ out_file ast effect_info env = flush output_chan; if close then close_out output_chan -let _ = - Target.register ~name:"c" ~options:c_options - ~pre_parse_hook:(fun () -> Initial_check.opt_undefined_gen := true) - ~rewrites:c_rewrites c_target +let _ = Target.register ~name:"c" ~options:c_options ~rewrites:c_rewrites c_target diff --git a/src/sail_lem_backend/sail_plugin_lem.ml b/src/sail_lem_backend/sail_plugin_lem.ml index ba545a8e9..3bfe3b310 100644 --- a/src/sail_lem_backend/sail_plugin_lem.ml +++ b/src/sail_lem_backend/sail_plugin_lem.ml @@ -161,17 +161,15 @@ let output_lem filename libs effect_info type_env ast = (* let seq_suffix = if !Pretty_print_lem.opt_sequential then "_sequential" else "" in *) let types_module = filename ^ "_types" in let concurrency_monad_params = Monad_params.find_monad_parameters type_env in - let monad_modules, monad_undefined_gen = + let monad_modules = if Option.is_some concurrency_monad_params then - (["Sail2_concurrency_interface"; "Sail2_monadic_combinators"], ["Sail2_undefined_concurrency_interface"]) - else (["Sail2_prompt_monad"; "Sail2_prompt"], ["Sail2_undefined"]) + ["Sail2_concurrency_interface"; "Sail2_monadic_combinators"; "Sail2_undefined_concurrency_interface"] + else ["Sail2_prompt_monad"; "Sail2_prompt"; "Sail2_undefined"] in - let undefined_modules = if !Initial_check.opt_undefined_gen then monad_undefined_gen else [] in let operators_module = if !Monomorphise.opt_mwords then "Sail2_operators_mwords" else "Sail2_operators_bitlists" in (* let libs = List.map (fun lib -> lib ^ seq_suffix) libs in *) let base_imports = - ["Pervasives_extra"; "Sail2_instr_kinds"; "Sail2_values"; "Sail2_string"; operators_module] - @ monad_modules @ undefined_modules + ["Pervasives_extra"; "Sail2_instr_kinds"; "Sail2_values"; "Sail2_string"; operators_module] @ monad_modules in let isa_thy_name = String.capitalize_ascii filename ^ "_lemmas" in let isa_lemmas = diff --git a/src/sail_ocaml_backend/sail_plugin_ocaml.ml b/src/sail_ocaml_backend/sail_plugin_ocaml.ml index 7bcc1cc1c..5f6a9d39c 100644 --- a/src/sail_ocaml_backend/sail_plugin_ocaml.ml +++ b/src/sail_ocaml_backend/sail_plugin_ocaml.ml @@ -127,9 +127,8 @@ let ocaml_target _ default_sail_dir out_file ast effect_info env = Ocaml_backend.ocaml_compile default_sail_dir out ast !ocaml_generator_info let _ = - Target.register ~name:"ocaml" ~options:ocaml_options - ~pre_parse_hook:(fun () -> Initial_check.opt_undefined_gen := true) - ~pre_rewrites_hook:stash_pre_rewrite_info ~rewrites:ocaml_rewrites ocaml_target + Target.register ~name:"ocaml" ~options:ocaml_options ~pre_rewrites_hook:stash_pre_rewrite_info + ~rewrites:ocaml_rewrites ocaml_target let opt_tofrominterp_output_dir : string option ref = ref None diff --git a/test/c/pc_no_wildcard.sail b/test/c/pc_no_wildcard.sail index 7b5e963b4..6a7a87533 100644 --- a/test/c/pc_no_wildcard.sail +++ b/test/c/pc_no_wildcard.sail @@ -3,7 +3,7 @@ default Order dec $include $include -register R : (bits(1), option(bits(2))) +register R : (bits(1), option(bits(2))) = (0b0, None()) val test : unit -> int diff --git a/test/c/undefined_nat.sail b/test/c/undefined_nat.sail index 35dead669..cb4887e3b 100644 --- a/test/c/undefined_nat.sail +++ b/test/c/undefined_nat.sail @@ -4,10 +4,10 @@ $include val "print_endline" : string -> unit -register R : nat +register R : nat = 0 register T : int function main() -> unit = { print_endline("ok"); -} \ No newline at end of file +} diff --git a/test/c/warl_undef.expect b/test/c/warl2.expect similarity index 100% rename from test/c/warl_undef.expect rename to test/c/warl2.expect diff --git a/test/c/warl_undef.sail b/test/c/warl2.sail similarity index 83% rename from test/c/warl_undef.sail rename to test/c/warl2.sail index a0ac9343e..cd667b49d 100644 --- a/test/c/warl_undef.sail +++ b/test/c/warl2.sail @@ -1,7 +1,5 @@ default Order dec -$option -undefined_gen - $include $include @@ -16,6 +14,6 @@ let x : WARL_range = struct { } function main () : unit -> unit = { - let z: WARL_range = undefined; + let z: WARL_range = x; print_endline("ok") } diff --git a/test/typecheck/fail/negative_bits_existential.expect b/test/typecheck/fail/negative_bits_existential.expect index eafc554f2..5e9bbd84e 100644 --- a/test/typecheck/fail/negative_bits_existential.expect +++ b/test/typecheck/fail/negative_bits_existential.expect @@ -2,4 +2,4 @@ fail/negative_bits_existential.sail:12.17-26: 12 | let x: Foo = undefined;  | ^-------^ -  | Type Foo is empty +  | Type Foo cannot be undefined diff --git a/test/typecheck/fail/negative_bits_struct.expect b/test/typecheck/fail/negative_bits_struct.expect index a4991fa32..f6c309fda 100644 --- a/test/typecheck/fail/negative_bits_struct.expect +++ b/test/typecheck/fail/negative_bits_struct.expect @@ -2,4 +2,4 @@ fail/negative_bits_struct.sail:14.24-33: 14 | let x: synonym(1) = undefined;  | ^-------^ -  | Type synonym(1) is empty +  | Type synonym(1) cannot be undefined diff --git a/test/typecheck/fail/negative_bits_struct2.expect b/test/typecheck/fail/negative_bits_struct2.expect index e6916d519..49010a5a8 100644 --- a/test/typecheck/fail/negative_bits_struct2.expect +++ b/test/typecheck/fail/negative_bits_struct2.expect @@ -2,4 +2,4 @@ fail/negative_bits_struct2.sail:12.17-26: 12 | let x: Foo = undefined;  | ^-------^ -  | Type Foo is empty +  | Type Foo cannot be undefined diff --git a/test/typecheck/fail/negative_bits_tuple.expect b/test/typecheck/fail/negative_bits_tuple.expect index 128aa4666..553f35f1e 100644 --- a/test/typecheck/fail/negative_bits_tuple.expect +++ b/test/typecheck/fail/negative_bits_tuple.expect @@ -2,4 +2,4 @@ fail/negative_bits_tuple.sail:8.29-38: 8 | let x: (bits(-1), int) = undefined;  | ^-------^ -  | Type (bits(-1), int) is empty +  | Type (bits(-1), int) could be empty diff --git a/test/typecheck/fail/negative_bits_union.expect b/test/typecheck/fail/negative_bits_union.expect index 1419f1093..e78b32efb 100644 --- a/test/typecheck/fail/negative_bits_union.expect +++ b/test/typecheck/fail/negative_bits_union.expect @@ -2,4 +2,4 @@ fail/negative_bits_union.sail:12.20-29: 12 | let x: Foo(1) = undefined;  | ^-------^ -  | Type Foo(1) is empty +  | Type Foo(1) cannot be undefined diff --git a/test/typecheck/fail/negative_bits_union2.expect b/test/typecheck/fail/negative_bits_union2.expect new file mode 100644 index 000000000..b0bac9e6c --- /dev/null +++ b/test/typecheck/fail/negative_bits_union2.expect @@ -0,0 +1,5 @@ +Type error: +fail/negative_bits_union2.sail:15.20-29: +15 | let x: Foo(1) = undefined; +  | ^-------^ +  | Type Foo(1) cannot be undefined diff --git a/test/typecheck/pass/negative_bits_union.sail b/test/typecheck/fail/negative_bits_union2.sail similarity index 60% rename from test/typecheck/pass/negative_bits_union.sail rename to test/typecheck/fail/negative_bits_union2.sail index b4c5db6c2..1a40c2d6d 100644 --- a/test/typecheck/pass/negative_bits_union.sail +++ b/test/typecheck/fail/negative_bits_union2.sail @@ -2,8 +2,7 @@ default Order dec $include -/* Should this actually be forbidden? Currently allowed because we can -always construct Baz() even when Bar is uninhabited. */ +/* Should this actually be allowed? Currently forbidden because the undefined generation is strict */ union Foo('n: Int) = { Bar : bits('n - 2), diff --git a/test/typecheck/fail/procstate1.expect b/test/typecheck/fail/procstate1.expect new file mode 100644 index 000000000..f3c402190 --- /dev/null +++ b/test/typecheck/fail/procstate1.expect @@ -0,0 +1,5 @@ +Type error: +fail/procstate1.sail:14.0-30: +14 |register PSTATE : ProcState(1) +  |^----------------------------^ +  | Must provide a default register value for a register of type ProcState(1) diff --git a/test/typecheck/fail/procstate1.sail b/test/typecheck/fail/procstate1.sail new file mode 100644 index 000000000..250b9aaff --- /dev/null +++ b/test/typecheck/fail/procstate1.sail @@ -0,0 +1,16 @@ +default Order dec + +infix 4 == + +val operator == = pure {lem: "eq_vec"} : forall 'n. (bitvector('n, dec), bitvector('n, dec)) -> bool + +struct ProcState ('n : Int) = { + N : bitvector('n, dec), + Z : bitvector(1, dec), + C : bitvector(1, dec), + V : bitvector(1, dec) +} + +register PSTATE : ProcState(1) + +function test () -> bool = PSTATE.N == 0b1 diff --git a/test/typecheck/pass/inline_typ.sail b/test/typecheck/pass/inline_typ.sail index 95be790c4..a6af58744 100644 --- a/test/typecheck/pass/inline_typ.sail +++ b/test/typecheck/pass/inline_typ.sail @@ -1,2 +1,5 @@ +default Order dec -function test forall 'n 'm. (x : int('n), y : int('m)) -> int('m + 'n) = undefined \ No newline at end of file +$include + +function test forall 'n 'm. (x : int('n), y : int('m)) -> int('m + 'n) = x + y diff --git a/test/typecheck/pass/negative_bits_list.sail b/test/typecheck/pass/negative_bits_list.sail index c5238a289..6038c535e 100644 --- a/test/typecheck/pass/negative_bits_list.sail +++ b/test/typecheck/pass/negative_bits_list.sail @@ -6,6 +6,5 @@ val foo : unit -> unit function foo() = { let x: list(bits(-1)) = [||]; - let y: list(bits(-1)) = undefined; () } diff --git a/test/typecheck/pass/negative_bits_list/v1.expect b/test/typecheck/pass/negative_bits_list/v1.expect index eec1a9ad2..f74668439 100644 --- a/test/typecheck/pass/negative_bits_list/v1.expect +++ b/test/typecheck/pass/negative_bits_list/v1.expect @@ -1,5 +1,5 @@ Type error: -pass/negative_bits_list/v1.sail:10.30-39: -10 | let z: list(bits(-1)) = [|undefined|]; -  | ^-------^ -  | Type bitvector(-1) is empty +pass/negative_bits_list/v1.sail:9.30-39: +9 | let z: list(bits(-1)) = [|undefined|]; +  | ^-------^ +  | Type bitvector(-1) could be empty diff --git a/test/typecheck/pass/negative_bits_list/v1.sail b/test/typecheck/pass/negative_bits_list/v1.sail index a80ce0c0a..7a1080162 100644 --- a/test/typecheck/pass/negative_bits_list/v1.sail +++ b/test/typecheck/pass/negative_bits_list/v1.sail @@ -6,7 +6,6 @@ val foo : unit -> unit function foo() = { let x: list(bits(-1)) = [||]; - let y: list(bits(-1)) = undefined; let z: list(bits(-1)) = [|undefined|]; () } diff --git a/test/typecheck/pass/negative_bits_list/v2.expect b/test/typecheck/pass/negative_bits_list/v2.expect new file mode 100644 index 000000000..e080a8588 --- /dev/null +++ b/test/typecheck/pass/negative_bits_list/v2.expect @@ -0,0 +1,5 @@ +Type error: +pass/negative_bits_list/v2.sail:9.28-37: +9 | let y: list(bits(-1)) = undefined; +  | ^-------^ +  | Type list(bits(-1)) cannot be undefined diff --git a/test/typecheck/pass/negative_bits_list/v2.sail b/test/typecheck/pass/negative_bits_list/v2.sail new file mode 100644 index 000000000..c5238a289 --- /dev/null +++ b/test/typecheck/pass/negative_bits_list/v2.sail @@ -0,0 +1,11 @@ +default Order dec + +$include + +val foo : unit -> unit + +function foo() = { + let x: list(bits(-1)) = [||]; + let y: list(bits(-1)) = undefined; + () +} diff --git a/test/typecheck/pass/procstate1.sail b/test/typecheck/pass/procstate1.sail index 250b9aaff..b837ac27d 100644 --- a/test/typecheck/pass/procstate1.sail +++ b/test/typecheck/pass/procstate1.sail @@ -11,6 +11,6 @@ struct ProcState ('n : Int) = { V : bitvector(1, dec) } -register PSTATE : ProcState(1) +register PSTATE : ProcState(1) = struct { N = 0b0, Z = 0b0, C = 0b0, V = 0b0 } function test () -> bool = PSTATE.N == 0b1 diff --git a/test/typecheck/pass/pure_record2.sail b/test/typecheck/pass/pure_record2.sail index 6428e2da6..6991cb77e 100644 --- a/test/typecheck/pass/pure_record2.sail +++ b/test/typecheck/pass/pure_record2.sail @@ -1,6 +1,8 @@ default Order dec -struct State('n: Int) = { +$include + +struct State('n: Int), 'n >= 0 = { N : bitvector('n, dec), Z : bitvector(1, dec) } diff --git a/test/typecheck/pass/pure_record3.sail b/test/typecheck/pass/pure_record3.sail index bc6f4c858..2d216a7dc 100644 --- a/test/typecheck/pass/pure_record3.sail +++ b/test/typecheck/pass/pure_record3.sail @@ -1,6 +1,8 @@ default Order dec -struct State('n: Int) = { +$include + +struct State('n: Int), 'n >= 0 = { N : bitvector('n, dec), Z : bitvector(1, dec) } diff --git a/test/typecheck/pass/reg_list.sail b/test/typecheck/pass/reg_list.sail index bf7769428..4d01201d4 100644 --- a/test/typecheck/pass/reg_list.sail +++ b/test/typecheck/pass/reg_list.sail @@ -1,7 +1,6 @@ -register X : list(bool) +register X : list(bool) = [||] val init_X : unit -> unit effect {wreg} function init_X () = { X = [||]; } - diff --git a/test/typecheck/pass/reg_option.sail b/test/typecheck/pass/reg_option.sail index 55317d1f2..031ebf9a8 100644 --- a/test/typecheck/pass/reg_option.sail +++ b/test/typecheck/pass/reg_option.sail @@ -2,7 +2,7 @@ $include $include $include -register X : option(int) +register X : option(int) = None() val inc_X : unit -> int effect {rreg, wreg} function inc_X () = {