Config: Add configurable abstract types and add bit type

doc/asciidoc/configuration.adoc

@@ -136,6 +136,47 @@ void sail_config_set_file(const char *path);
 void sail_config_cleanup(void);
 ----
 
+=== Configurable abstract types
+
+The <<Abstract types>> section we described how to write a type like
+`xlen` below without providing a concrete value, in such a way that
+the specification is parametric over the choice of `xlen`.
+
+[source,sail]
+----
+type xlen : Int
+----
+
+In practice, we likely want to configure this type to have some
+specific value at runtime. This can be done by associating a
+configuration option with the abstract type as
+
+[source,sail]
+----
+type xlen : Int = config arch.xlen
+----
+
+which could be instantiated using the following configuration JSON
+
+[source,json]
+----
+{ "arch" : { "xlen" : 32 } }
+----
+
+We can then create (configurable) bitvector values of length `xlen`:
+[source,sail]
+----
+let x : bits(xlen) = config some.bitvector_value
+----
+
+In the configuration file, we specify these by using the string
+`"xlen"` as the length:
+
+[source,json]
+----
+{ "some" : { "bitvector_value" : { "len" : "xlen", "value": "0xFFFF_FFFF" } } }
+----
+
 === Validating Configurations with JSON Schema
 
 :confschema: sail_doc/config_schema.json

language/jib.ott

@@ -209,13 +209,6 @@ clexp :: 'CL_' ::=
   | clexp . nat              :: :: tuple
   | void : ctyp              :: :: void
 
-ctype_def :: 'CTD_' ::=
-  {{ com C type definition }}
-  | enum id = id0 '|' ... '|' idn                    :: :: enum
-  | struct id = { id0 : ctyp0 , ... , idn : ctypn }  :: :: struct
-  | variant id = { id0 : ctyp0 , ... , idn : ctypn } :: :: variant
-  | abstract id : ctyp                               :: :: abstract
-
 iannot :: '' ::=
   {{ phantom }}
   {{ lem iannot }}
@@ -271,6 +264,17 @@ instr :: 'I_' ::=
   | reset ctyp name                                :: :: reset
   | ctyp name = cval                               :: :: reinit
 
+ctype_def_init :: 'CTDI_' ::=
+  | = { instr0 ; ... ; instrn } :: :: instrs
+  |                             :: :: none
+
+ctype_def :: 'CTD_' ::=
+  {{ com C type definition }}
+  | enum id = id0 '|' ... '|' idn                    :: :: enum
+  | struct id = { id0 : ctyp0 , ... , idn : ctypn }  :: :: struct
+  | variant id = { id0 : ctyp0 , ... , idn : ctypn } :: :: variant
+  | abstract id : ctyp ctype_def_init                :: :: abstract
+
 def_annot :: '' ::=
   {{ phantom }}
   {{ lem def_annot unit }}

language/sail.ott

@@ -322,6 +322,10 @@ typschm :: 'TypSchm_' ::=
 
 grammar
 
+opt_abstract_config :: 'TDC_' ::=
+  | = config string1 . ... . string2 :: :: key
+  |                                  :: :: none
+
 type_def {{ ocaml 'a type_def }} {{ lem type_def 'a }} :: 'TD_' ::=
   {{ ocaml TD_aux of type_def_aux * 'a annot }}
   {{ lem TD_aux of type_def_aux * annot 'a }}
@@ -337,7 +341,7 @@ type_def_aux  :: 'TD_' ::=
     {{ com tagged union type definition}} {{ texlong }}
   | typedef id = enumerate { id1 ; ... ; idn semi_opt }   :: :: enum
     {{ com enumeration type definition}} {{ texlong }}
-  | typedef id : kind :: :: abstract
+  | typedef id : kind opt_abstract_config :: :: abstract
     {{ com abstract type }}
   | bitfield id : typ = { id1 : index_range1 , ... , idn : index_rangen } :: :: bitfield
     {{ com register mutable bitfield type definition }} {{ texlong }}

lib/json/sail_config.c

@@ -184,6 +184,29 @@ bool sail_config_is_bits(const sail_config_json config)
   return is_bool_array || is_bv_object;
 }
 
+bool sail_config_is_bits_abstract(const sail_config_json config)
+{
+  cJSON *json = (cJSON *)config;
+
+  if (!(cJSON_IsObject(json) && cJSON_HasObjectItem(json, "len"))) {
+    return false;
+  }
+
+  return cJSON_IsString(cJSON_GetObjectItemCaseSensitive(json, "len"));
+}
+
+void sail_config_bits_abstract_len(sail_string *str, const sail_config_json config)
+{
+  cJSON *json = (cJSON *)config;
+
+  cJSON *len_json = cJSON_GetObjectItemCaseSensitive(json, "len");
+  sail_string len_str = cJSON_GetStringValue(len_json);
+
+  size_t sz = strlen(len_str);
+  *str = (sail_string)realloc(*str, sz + 1);
+  *str = strcpy(*str, len_str);
+}
+
 void sail_config_unwrap_string(sail_string *str, const sail_config_json config)
 {
   sail_string conf_str = cJSON_GetStringValue((cJSON *)config);
@@ -213,6 +236,57 @@ void sail_config_truncate(lbits *rop) {
   mpz_clear(tmp);
 }
 
+void sail_config_unwrap_bit(lbits *bv, const sail_config_json config)
+{
+  cJSON *json = (cJSON *)config;
+
+  bv->len = 1;
+  if (mpz_set_str(*bv->bits, json->valuestring, 10) == -1) {
+    sail_assert(false, "Failed to parse integer from configuration");
+  }
+}
+
+void sail_config_set_bits_value(lbits *bv, char *v)
+{
+  size_t i = 0;
+  for (char *c = v; *c != '\0'; c++) {
+    if (*c != '_') {
+      v[i] = *c;
+      i++;
+    }
+  }
+  v[i] = '\0';
+
+  if (strncmp(v, "0x", 2) == 0) {
+    gmp_sscanf(v, "0x%Zx", bv->bits);
+  } else if (strncmp(v, "0b", 2) == 0) {
+    mp_bitcnt_t b = 0;
+    i--;
+    do {
+      if (v[i] == '1') {
+        mpz_setbit(*bv->bits, b);
+      }
+      b++;
+      i--;
+    } while (i >= 2);
+  } else {
+    gmp_sscanf(v, "%Zd", bv->bits);
+  }
+
+  sail_config_truncate(bv);
+}
+
+void sail_config_unwrap_abstract_bits(lbits *bv, int64_t len, sail_config_json config)
+{
+  cJSON *json = (cJSON *)config;
+  cJSON *value_json = cJSON_GetObjectItemCaseSensitive(json, "value");
+  char *v = value_json->valuestring;
+
+  bv->len = (mp_bitcnt_t)len;
+
+  sail_config_set_bits_value(bv, v);
+}
+
 void sail_config_unwrap_bits(lbits *bv, const sail_config_json config)
 {
   cJSON *json = (cJSON *)config;
@@ -236,36 +310,13 @@ void sail_config_unwrap_bits(lbits *bv, const sail_config_json config)
     char *v = value_json->valuestring;
     bool has_separator = false;
 
-    bv->len = (mp_bitcnt_t)atoi(len_json->valuestring);
-
-    size_t i = 0;
-    for (char *c = v; *c != '\0'; c++) {
-      if (*c != '_') {
-        v[i] = *c;
-        i++;
-      }
-    }
-    v[i] = '\0';
-
-    if (strncmp(v, "0x", 2) == 0) {
+    if (cJSON_IsNumber(len_json)) {
       bv->len = (mp_bitcnt_t)atoi(len_json->valuestring);
-      gmp_sscanf(v, "0x%Zx", bv->bits);
-    } else if (strncmp(v, "0b", 2) == 0) {
-      mp_bitcnt_t b = 0;
-      i--;
-      do {
-        if (v[i] == '1') {
-          mpz_setbit(*bv->bits, b);
-        }
-        b++;
-        i--;
-      } while (i >= 2);
     } else {
-      bv->len = (mp_bitcnt_t)atoi(len_json->valuestring);
-      gmp_sscanf(v, "%Zd", bv->bits);
+      bv->len = 32;
     }
 
-    sail_config_truncate(bv);
+    sail_config_set_bits_value(bv, v);
   }
 }
 

lib/json/sail_config.h

@@ -8,7 +8,7 @@
 /*  The ASL derived parts of the ARMv8.3 specification in                   */
 /*  aarch64/no_vector and aarch64/full are copyright ARM Ltd.               */
 /*                                                                          */
-/*  Copyright (c) 2024                                                      */
+/*  Copyright (c) 2024-2025                                                 */
 /*    Alasdair Armstrong                                                    */
 /*                                                                          */
 /*  All rights reserved.                                                    */
@@ -94,11 +94,23 @@ bool sail_config_is_bool_array(const sail_config_json config);
 bool sail_config_is_int(const sail_config_json config);
 bool sail_config_is_string(const sail_config_json config);
 
+void sail_config_unwrap_bit(lbits *bv, const sail_config_json config);
 void sail_config_unwrap_bits(lbits *bv, const sail_config_json config);
 bool sail_config_unwrap_bool(const sail_config_json config);
 void sail_config_unwrap_int(sail_int *n, const sail_config_json config);
 void sail_config_unwrap_string(sail_string *str, const sail_config_json config);
 
+/*
+ * Configurable abstract types require some special handling.
+ *
+ * Their length will be a string value like "xlen" or "mxlen". It is
+ * up to the user of this API to detect this and use the
+ * `unwrap_abstract_bits` variant after finding the correct width.
+ */
+bool sail_config_is_bits_abstract(const sail_config_json config);
+void sail_config_bits_abstract_len(sail_string *str, const sail_config_json config);
+void sail_config_unwrap_abstract_bits(lbits *bv, int64_t len, sail_config_json config);
+
 #ifdef __cplusplus
 }
 #endif

src/bin/repl.ml

@@ -623,7 +623,9 @@ let handle_input' istate input =
               let ast, env = Type_check.check istate.env ast in
               { istate with ast = append_ast istate.ast ast; env; ctx }
           | ":instantiate" ->
-              let ast = Frontend.instantiate_abstract_types None !Sail_options.opt_instantiations istate.ast in
+              let ast, _ =
+                Frontend.instantiate_abstract_types None (`Assoc []) !Sail_options.opt_instantiations istate.ast
+              in
               let ast, env = Type_check.check istate.env (Type_check.strip_ast ast) in
               { istate with ast = append_ast istate.ast ast; env }
           | ":rewrite" ->

src/bin/sail.ml

@@ -441,7 +441,7 @@ let file_to_string filename =
     close_in chan;
     Buffer.contents buf
 
-let apply_model_config env ast =
+let get_model_config () =
   match !opt_config_file with
   | Some file ->
       if Sys.file_exists file then (
@@ -453,10 +453,10 @@ let apply_model_config env ast =
                  (Printf.sprintf "Failed to parse configuration file:\n%s" message)
               )
         in
-        Config.rewrite_ast env json ast
+        json
       )
       else raise (Reporting.err_general Parse_ast.Unknown (Printf.sprintf "Configuration file %s does not exist" file))
-  | None -> Config.rewrite_ast env (`Assoc []) ast
+  | None -> `Assoc []
 
 let run_sail (config : Yojson.Safe.t option) tgt =
   Target.run_pre_parse_hook tgt ();
@@ -516,8 +516,9 @@ let run_sail (config : Yojson.Safe.t option) tgt =
               arguments with the appropriate extension, but not both!"
           )
   in
-  let ast = Frontend.instantiate_abstract_types (Some tgt) !opt_instantiations ast in
-  let schema, ast = apply_model_config env ast in
+  let config_json = get_model_config () in
+  let ast, env_update = Frontend.instantiate_abstract_types (Some tgt) config_json !opt_instantiations ast in
+  let schema, ast = Config.rewrite_ast env env_update config_json ast in
   let ast, env = Frontend.initial_rewrite effect_info env ast in
   let ast, env = match !opt_splice with [] -> (ast, env) | files -> Splice.splice_files ctx ast (List.rev files) in
   let effect_info = Effects.infer_side_effects (Target.asserts_termination tgt) ast in

src/lib/ast_util.ml

@@ -1424,7 +1424,7 @@ let id_of_type_def_aux = function
   | TD_record (id, _, _, _)
   | TD_variant (id, _, _, _)
   | TD_enum (id, _, _)
-  | TD_abstract (id, _)
+  | TD_abstract (id, _, _)
   | TD_bitfield (id, _, _) ->
       id
 

src/lib/callgraph.ml

@@ -273,7 +273,7 @@ let add_def_to_graph graph (DEF_aux (def, def_annot)) =
         scan_typquant (Type id) typq
     | TD_enum (id, ctors, _) ->
         List.iter (fun ctor_id -> graph := G.add_edge (Constructor ctor_id) (Type id) !graph) ctors
-    | TD_abstract (id, _) -> graph := G.add_edges (Type id) [] !graph
+    | TD_abstract (id, _, _) -> graph := G.add_edges (Type id) [] !graph
     | TD_bitfield (id, typ, ranges) ->
         graph := G.add_edges (Type id) (List.map (fun id -> Type id) (IdSet.elements (typ_ids typ))) !graph
   in