From 10707fad0ca8876970fdc615d0ed761c9ec184b7 Mon Sep 17 00:00:00 2001
From: Alasdair <alasdair.armstrong@cl.cam.ac.uk>
Date: Mon, 3 Mar 2025 17:56:49 +0000
Subject: [PATCH] Config: Add an error for uninstantiated configuration options
 when unsupported

---
 src/bin/sail.ml    |  2 +-
 src/lib/config.ml  | 15 +++++++++++----
 src/lib/config.mli |  3 ++-
 src/lib/target.mli |  4 ++++
 4 files changed, 18 insertions(+), 6 deletions(-)

diff --git a/src/bin/sail.ml b/src/bin/sail.ml
index efdcf329b..bedb9c1c0 100644
--- a/src/bin/sail.ml
+++ b/src/bin/sail.ml
@@ -518,7 +518,7 @@ let run_sail (config : Yojson.Safe.t option) tgt =
   in
   let config_json = get_model_config () in
   let ast, instantiation = Frontend.instantiate_abstract_types (Some tgt) config_json !opt_instantiations ast in
-  let schema, ast = Config.rewrite_ast env instantiation config_json ast in
+  let schema, ast = Config.rewrite_ast tgt env instantiation 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
diff --git a/src/lib/config.ml b/src/lib/config.ml
index 5550a014a..8f005103c 100644
--- a/src/lib/config.ml
+++ b/src/lib/config.ml
@@ -690,14 +690,21 @@ let rec sail_exp_from_json ~at:l env typ =
     )
   | _ -> assert false
 
-let rewrite_exp global_env env_update types json (aux, annot) =
+let rewrite_exp tgt global_env env_update types json (aux, annot) =
   match aux with
   | E_config parts -> (
       let env = env_of_annot annot in
       let typ = typ_of_annot annot in
       ConfigTypes.insert parts { loc = fst annot; env; typ } types;
       match find_json ~at:(fst annot) parts json with
-      | None -> E_aux (aux, annot)
+      | None ->
+          if Target.supports_runtime_config tgt then E_aux (aux, annot)
+          else
+            Printf.sprintf
+              "Runtime configuration is not supported when generating code for target '%s'\n\
+               An explicit configuration should be provided with the --config option." (Target.name tgt)
+            |> Reporting.err_general (fst annot)
+            |> raise
       | Some json -> (
           try
             let exp = sail_exp_from_json ~at:(fst annot) global_env typ json in
@@ -717,14 +724,14 @@ let rec abstract_schema config_ids types = function
   | def :: defs -> abstract_schema config_ids types defs
   | [] -> ()
 
-let rewrite_ast global_env instantiation json ast =
+let rewrite_ast tgt global_env instantiation json ast =
   let open Frontend in
   let types = ConfigTypes.create () in
   Bindings.iter
     (fun id (kind_aux, json_key) -> ConfigTypes.insert_abstract json_key id kind_aux types)
     instantiation.config_ids;
   abstract_schema instantiation.config_ids types ast.defs;
-  let alg = { id_exp_alg with e_aux = rewrite_exp global_env instantiation.env_update types json } in
+  let alg = { id_exp_alg with e_aux = rewrite_exp tgt global_env instantiation.env_update types json } in
   let ast = rewrite_ast_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp alg) } ast in
   let schema = ConfigTypes.to_schema types in
   (schema, ast)
diff --git a/src/lib/config.mli b/src/lib/config.mli
index 957d50ae1..1a4a0dc7e 100644
--- a/src/lib/config.mli
+++ b/src/lib/config.mli
@@ -79,4 +79,5 @@ open Type_check
 
     The function will return that JSON schema alongside the re-written
     AST. *)
-val rewrite_ast : env -> Frontend.abstract_instantiation -> Yojson.Safe.t -> typed_ast -> Yojson.Safe.t * typed_ast
+val rewrite_ast :
+  Target.target -> env -> Frontend.abstract_instantiation -> Yojson.Safe.t -> typed_ast -> Yojson.Safe.t * typed_ast
diff --git a/src/lib/target.mli b/src/lib/target.mli
index a282cc8a8..6c798f4b3 100644
--- a/src/lib/target.mli
+++ b/src/lib/target.mli
@@ -77,6 +77,10 @@ val asserts_termination : target -> bool
     provide a concrete instantiation for Sail. *)
 val supports_abstract_types : target -> bool
 
+(** If a target does not support runtime configuration, then the
+    configuration must be provided statically at build time. *)
+val supports_runtime_config : target -> bool
+
 (** {2 Target registration} *)
 
 (** Used for plugins to register custom Sail targets/backends.