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

@@ -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);
           ],
         "<filename> 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), "<verbosity> produce verbose output");

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

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

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 =

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
 

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)
 

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

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 =