Remove the --abstract-types feature gate flag

rems-project · Mar 7, 2025 · c622c29 · c622c29
1 parent f980914
commit c622c29
Show file tree

Hide file tree

Showing 29 changed files with 484 additions and 81 deletions.
diff --git a/doc/asciidoc/language.adoc b/doc/asciidoc/language.adoc
@@ -593,9 +593,6 @@ to avoid us having to think about this particular detail.
 === Abstract types
 :abstract-ty: sail_doc/abstract_xlen.json
 
-NOTE: This feature is currently experimental and is enabled with the
-`--abstract-types` flag.
-
 Consider the following problem: We want to specify an architecture
 like RISC-V, which permits both 32-bit and a 64-bit implementations,
 with the two implementations being mostly the same other than the base
@@ -642,7 +639,7 @@ generating definitions. We do this using the `--instantiate` option,
 so if the above file is called `xlen.sail`, we could do:
 [source,sh]
 ----
-sail xlen.sail --lem --abstract-types --instantiate xlen=32
+sail xlen.sail --lem --instantiate xlen=32
 ----
 To create lem definitions for the `xlen = 32` case.
 

diff --git a/doc/examples/abstract_xlen.sail b/doc/examples/abstract_xlen.sail
@@ -1,8 +1,6 @@
 default Order dec
 $include <prelude.sail>
 
-$option --abstract-types
-
 $span start XLEN
 type xlen : Int
 

diff --git a/doc/manual.html b/doc/manual.html
diff --git a/src/bin/sail.ml b/src/bin/sail.ml
@@ -259,7 +259,6 @@ let rec options =
         Arg.String (fun file -> opt_output_schema_file := Some file),
         "<file> output configuration schema"
       );
-      ("-abstract_types", Arg.Set Initial_check.opt_abstract_types, " (experimental) allow abstract types");
       ("-fmt", Arg.Set opt_format, " format input source code");
       ( "-fmt_backup",
         Arg.String (fun suffix -> opt_format_backup := Some suffix),

diff --git a/src/lib/initial_check.ml b/src/lib/initial_check.ml
@@ -56,11 +56,8 @@ module P = Parse_ast
 (* See mli file for details on what these flags do *)
 let opt_fast_undefined = ref false
 let opt_magic_hash = ref false
-let opt_abstract_types = ref false
 let opt_strict_bitvector = ref false
 
-let abstract_type_error = "Abstract types are currently experimental, use the --abstract-types flag to enable"
-
 module StringSet = Set.Make (String)
 module StringMap = Map.Make (String)
 
@@ -1716,7 +1713,6 @@ let rec to_ast_typedef ctx def_annot (P.TD_aux (aux, l) : P.type_def) : untyped_
         { ctx with type_constructors = Bindings.add id ([], P.K_type) ctx.type_constructors }
       )
   | P.TD_abstract (id, kind, instantiation) -> (
-      if not !opt_abstract_types then raise (Reporting.err_general l abstract_type_error);
       let id = to_ast_reserved_type_id ctx id in
       let instantiation = match instantiation with Some key -> TDC_key key | None -> TDC_none in
       match to_ast_kind kind with
@@ -2050,7 +2046,6 @@ let rec to_ast_def doc attrs vis ctx (P.DEF_aux (def, l)) : untyped_def list ctx
       let d = to_ast_dec ctx dec in
       ([DEF_aux (DEF_register d, annot)], ctx)
   | P.DEF_constraint nc ->
-      if not !opt_abstract_types then raise (Reporting.err_general l abstract_type_error);
       let nc = to_ast_constraint ctx nc in
       ([DEF_aux (DEF_constraint nc, annot)], ctx)
   | P.DEF_pragma (pragma, P.Pragma_line (arg, ltrim)) ->

diff --git a/src/lib/initial_check.mli b/src/lib/initial_check.mli
@@ -52,10 +52,6 @@ open Ast_util
 
 (** {2 Options} *)
 
-(** Enable abstract types in the AST. If unset, will report an error
-    if they are encountered. *)
-val opt_abstract_types : bool ref
-
 (** If enabled, bitvector types are only well-formed if their
     arguments are natural numbers. *)
 val opt_strict_bitvector : bool ref

diff --git a/src/sail_doc_backend/sail_plugin_doc.ml b/src/sail_doc_backend/sail_plugin_doc.ml
@@ -133,7 +133,7 @@ let doc_target out_file { ast; _ } =
   else Printf.eprintf "Unknown documentation format: %s\n" !opt_doc_format
 
 let _ =
-  Target.register ~name:"doc" ~options:doc_options ~supports_abstract_types:true
+  Target.register ~name:"doc" ~options:doc_options ~supports_abstract_types:true ~supports_runtime_config:true
     ~pre_parse_hook:(fun () ->
       Type_check.opt_expand_valspec := false;
       Type_check.opt_no_bitfield_expansion := true
@@ -200,7 +200,7 @@ let html_target files out_dir_opt { ast; _ } =
 
 let _ =
   let files : Html_source.file_info list ref = ref [] in
-  Target.register ~name:"html" ~options:html_options ~supports_abstract_types:true
+  Target.register ~name:"html" ~options:html_options ~supports_abstract_types:true ~supports_runtime_config:true
     ~pre_initial_check_hook:(fun filenames ->
       List.iter
         (fun filename ->

diff --git a/test/c/abstract_type.sail b/test/c/abstract_type.sail
@@ -1,8 +1,6 @@
 default Order dec
 $include <prelude.sail>
 
-$option --abstract-types
-
 type xlen : Int
 
 constraint xlen in {32, 64}

diff --git a/test/c/config_abstract_bool.sail b/test/c/config_abstract_bool.sail
@@ -2,8 +2,6 @@ default Order dec
 
 $include <prelude.sail>
 
-$option --abstract-types
-
 $iftarget c
 $c_in_main sail_config_set_file("config_abstract_bool.json");
 $c_in_main sail_set_abstract_have_ext();

diff --git a/test/c/config_abstract_type.sail b/test/c/config_abstract_type.sail
@@ -1,8 +1,6 @@
 default Order dec
 $include <prelude.sail>
 
-$option --abstract-types
-
 type xlen : Int = config arch.xlen
 
 constraint xlen in {32, 64}

diff --git a/test/c/config_abstract_type2.sail b/test/c/config_abstract_type2.sail
@@ -1,8 +1,6 @@
 default Order dec
 $include <prelude.sail>
 
-$option --abstract-types
-
 type xlen : Int = config arch.xlen
 
 constraint xlen >= 0

diff --git a/test/c/config_abstract_type3.sail b/test/c/config_abstract_type3.sail
@@ -1,8 +1,6 @@
 default Order dec
 $include <prelude.sail>
 
-$option --abstract-types
-
 type other : Bool
 
 type xlen : Int = config arch.xlen

diff --git a/test/oneoff/instantiate_cmdline/test.sh b/test/oneoff/instantiate_cmdline/test.sh
@@ -2,5 +2,5 @@
 
 set -e
 
-sail xlen.sail --abstract-types --instantiate "xlen = 3 2" 2> xlen.result || true
+sail xlen.sail --instantiate "xlen = 3 2" 2> xlen.result || true
 diff xlen.result xlen.expect
diff --git a/test/oneoff/instantiate_cmdline/xlen.expect b/test/oneoff/instantiate_cmdline/xlen.expect
@@ -1,5 +1,5 @@
 [93mSyntax error[0m:
-[96mARGV[0m:5.9-9:
-5[96m |[0mxlen = 3 2
+[96mARGV[0m:4.9-9:
+4[96m |[0mxlen = 3 2
  [91m |[0m         [91m^[0m
  [91m |[0m Failed to parse ' 3 2' at token '2'
diff --git a/test/oneoff/instantiate_directive/test.sh b/test/oneoff/instantiate_directive/test.sh
@@ -2,5 +2,5 @@
 
 set -e
 
-sail xlen.sail --abstract-types 2> xlen.result || true
+sail xlen.sail 2> xlen.result || true
 diff xlen.result xlen.expect
diff --git a/test/oneoff/run_tests.py b/test/oneoff/run_tests.py
@@ -26,7 +26,7 @@ def test():
             tests[dir] = os.fork()
             if tests[dir] == 0:
                 os.chdir(dir)
-                step('./test.sh')
+                step('./test.sh', name=dir)
                 print_ok(dir)
                 sys.exit()
         results.collect(tests)

diff --git a/test/typecheck/fail/abstract_bool_inconsistent.expect b/test/typecheck/fail/abstract_bool_inconsistent.expect
@@ -1,5 +1,5 @@
 [93mType error[0m:
-[96mfail/abstract_bool_inconsistent.sail[0m:10.0-17:
-10[96m |[0mconstraint not(b)
-  [91m |[0m[91m^---------------^[0m
-  [91m |[0m Global constraint appears inconsistent with previous global constraints
+[96mfail/abstract_bool_inconsistent.sail[0m:8.0-17:
+8[96m |[0mconstraint not(b)
+ [91m |[0m[91m^---------------^[0m
+ [91m |[0m Global constraint appears inconsistent with previous global constraints
diff --git a/test/typecheck/fail/abstract_bool_inconsistent.sail b/test/typecheck/fail/abstract_bool_inconsistent.sail
@@ -2,8 +2,6 @@ default Order dec
 
 $include <prelude.sail>
 
-$option -abstract_types
-
 type b : Bool
 
 constraint b

diff --git a/test/typecheck/fail/abstract_type_type.expect b/test/typecheck/fail/abstract_type_type.expect
@@ -1,5 +1,5 @@
 [93mError[0m:
-[96mfail/abstract_type_type.sail[0m:3.0-13:
-3[96m |[0mtype a : Type
+[96mfail/abstract_type_type.sail[0m:2.0-13:
+2[96m |[0mtype a : Type
  [91m |[0m[91m^-----------^[0m
  [91m |[0m Abstract type must be either a boolean or integer type
diff --git a/test/typecheck/fail/abstract_type_type.sail b/test/typecheck/fail/abstract_type_type.sail
@@ -1,3 +1,2 @@
-$option --abstract-types
 
 type a : Type
diff --git a/test/typecheck/fail/global_false_constraint.expect b/test/typecheck/fail/global_false_constraint.expect
@@ -1,5 +1,5 @@
 [93mType error[0m:
-[96mfail/global_false_constraint.sail[0m:3.0-16:
-3[96m |[0mconstraint false
+[96mfail/global_false_constraint.sail[0m:2.0-16:
+2[96m |[0mconstraint false
  [91m |[0m[91m^--------------^[0m
  [91m |[0m Global constraint appears inconsistent with previous global constraints
diff --git a/test/typecheck/fail/global_false_constraint.sail b/test/typecheck/fail/global_false_constraint.sail
@@ -1,3 +1,2 @@
-$option -abstract_types
 
 constraint false
diff --git a/test/typecheck/pass/abstract_bitfield_width.sail b/test/typecheck/pass/abstract_bitfield_width.sail
@@ -2,7 +2,6 @@ default Order dec
 
 $include <prelude.sail>
 
-$option --abstract-types
 $option --instantiate w=32
 
 type w : Int

diff --git a/test/typecheck/pass/abstract_bool.sail b/test/typecheck/pass/abstract_bool.sail
@@ -2,7 +2,6 @@ default Order dec
 
 $include <prelude.sail>
 
-$option --abstract-types
 $option --instantiate b=true
 
 type b : Bool

diff --git a/test/typecheck/pass/abstract_bool2.sail b/test/typecheck/pass/abstract_bool2.sail
@@ -2,7 +2,6 @@ default Order dec
 
 $include <prelude.sail>
 
-$option --abstract-types
 $option --instantiate b=true
 
 type b : Bool

diff --git a/test/typecheck/pass/abstract_config.sail b/test/typecheck/pass/abstract_config.sail
@@ -1,6 +1,5 @@
 default Order dec
 
-$option --abstract-types
 $option --config ../typecheck/pass/abstract_config.json
 
 type xlen : Int = config arch.xlen

diff --git a/test/typecheck/pass/abstract_extend.sail b/test/typecheck/pass/abstract_extend.sail
@@ -2,7 +2,6 @@ default Order dec
 
 $include <prelude.sail>
 
-$option --abstract-types
 $option --instantiate xlen=32
 
 type xlen : Int

diff --git a/test/typecheck/pass/abstract_ones.sail b/test/typecheck/pass/abstract_ones.sail
@@ -2,7 +2,6 @@ default Order dec
 
 $include <prelude.sail>
 
-$option --abstract-types
 $option --instantiate xlen=32
 
 type xlen : Int

diff --git a/test/typecheck/pass/constraint_syn.sail b/test/typecheck/pass/constraint_syn.sail
@@ -1,7 +1,6 @@
 default Order dec
 $include <prelude.sail>
 
-$option --abstract-types
 $option --instantiate xlen=32
 
 type xlen : Int