Output calls to set_abstract_... in model_init() (#1436)

* Output calls to set_abstract_... in model_init()

So that you don't need to call these functions automatically. As far as I can tell they are idempotent so it should be backwards compatible.

* Don't call `sail_set_abstract_...` when it takes a parameter

If an abstract type hasn't been initialised we can't automatically initialise it.

Author: Timmmm

src/lib/jib_compile.ml

@@ -102,6 +102,8 @@ let is_ct_enum = function CT_enum _ -> true | _ -> false
 
 let iblock1 = function [instr] -> instr | instrs -> iblock instrs
 
+type abstract_type_initialised = Initialised | Uninitialised
+
 (** The context type contains two type-checking environments. ctx.local_env contains the closest typechecking
     environment, usually from the expression we are compiling, whereas ctx.tc_env is the global type checking
     environment from type-checking the entire AST. We also keep track of local variables in ctx.locals, so we know when
@@ -111,7 +113,7 @@ type ctx = {
   records : (kid list * ctyp Bindings.t) Bindings.t;
   enums : IdSet.t Bindings.t;
   variants : (kid list * ctyp Bindings.t) Bindings.t;
-  abstracts : ctyp Bindings.t;
+  abstracts : (ctyp * abstract_type_initialised) Bindings.t;
   valspecs : (string option * ctyp list * ctyp * uannot) Bindings.t;
   quants : ctyp KBindings.t;
   local_env : Env.t;
@@ -132,7 +134,7 @@ let ctx_map_ctyps f ctx =
     ctx with
     records = Bindings.map (fun (params, fields) -> (params, Bindings.map f fields)) ctx.records;
     variants = Bindings.map (fun (params, fields) -> (params, Bindings.map f fields)) ctx.variants;
-    abstracts = Bindings.map f ctx.abstracts;
+    abstracts = Bindings.map (fun (ctyp, initialised) -> (f ctyp, initialised)) ctx.abstracts;
     valspecs =
       Bindings.map
         (fun (extern, param_ctyps, ret_ctyp, uannot) -> (extern, List.map f param_ctyps, f ret_ctyp, uannot))
@@ -771,7 +773,7 @@ module Make (C : CONFIG) = struct
                  (mk_id "sail_config_bits_abstract_len", [])
                  [V_id (json, CT_json)];
              ]
-            @ select_abstract l ctx abstract_name (fun id abstract_ctyp ->
+            @ select_abstract l ctx abstract_name (fun id (abstract_ctyp, _) ->
                   match abstract_ctyp with
                   | CT_fint 64 ->
                       [
@@ -1808,14 +1810,19 @@ module Make (C : CONFIG) = struct
               CTDI_instrs (setup @ [call (CL_id (Abstract id, ctyp))] @ cleanup)
           | TDC_none -> CTDI_none
         in
+        let is_initialised = function CTDI_instrs _ -> Initialised | CTDI_none -> Uninitialised in
         match kind with
         | K_int ->
             let ctyp = ctyp_of_typ ctx (atom_typ (nid id)) in
             let inst = compile_inst ctyp inst in
-            (Some (CTD_abstract (id, ctyp, inst)), { ctx with abstracts = Bindings.add id ctyp ctx.abstracts })
+            ( Some (CTD_abstract (id, ctyp, inst)),
+              { ctx with abstracts = Bindings.add id (ctyp, is_initialised inst) ctx.abstracts }
+            )
         | K_bool ->
             let inst = compile_inst CT_bool inst in
-            (Some (CTD_abstract (id, CT_bool, inst)), { ctx with abstracts = Bindings.add id CT_bool ctx.abstracts })
+            ( Some (CTD_abstract (id, CT_bool, inst)),
+              { ctx with abstracts = Bindings.add id (CT_bool, is_initialised inst) ctx.abstracts }
+            )
         | _ -> Reporting.unreachable l __POS__ "Found abstract type that was neither an integer nor a boolean"
       )
     (* Will be re-written before here, see bitfield.ml *)

src/lib/jib_compile.mli

@@ -66,14 +66,20 @@ val opt_memo_cache : bool ref
 
 (** {2 Jib context} *)
 
+(* For an abstract type like `type xlen : Int`, is it initialised?
+   Yes: `type xlen : Int = config xlen`
+   No: `type xlen : Int`
+*)
+type abstract_type_initialised = Initialised | Uninitialised
+
 (** Dynamic context for compiling Sail to Jib. We need to pass a (global) typechecking environment given by checking the
     full AST. *)
 type ctx = {
   target_name : string;
   records : (kid list * ctyp Bindings.t) Bindings.t;
   enums : IdSet.t Bindings.t;
   variants : (kid list * ctyp Bindings.t) Bindings.t;
-  abstracts : ctyp Bindings.t;
+  abstracts : (ctyp * abstract_type_initialised) Bindings.t;
   valspecs : (string option * ctyp list * ctyp * uannot) Bindings.t;
   quants : ctyp KBindings.t;
   local_env : Env.t;

src/sail_c_backend/c_backend.ml

@@ -2455,6 +2455,17 @@ module Codegen (Config : CODEGEN_CONFIG) = struct
         List.map (fun n -> Printf.sprintf "  create_letbind_%d();" n) (List.rev ctx.letbinds)
       in
       let letbind_finalizers = List.map (fun n -> Printf.sprintf "  kill_letbind_%d();" n) ctx.letbinds in
+
+      let set_abstract_types =
+        Bindings.bindings ctx.abstracts
+        |> List.filter_map (fun (id, (_, initialised)) ->
+               match initialised with
+               | Initialised -> Some (Printf.sprintf "  sail_set_abstract_%s();" (Ast_util.string_of_id id))
+               (* Skip abstract types that haven't been initialised; we can't initialise them automatically. *)
+               | Uninitialised -> None
+           )
+      in
+
       let startup cdefs = List.map sgen_startup (List.filter is_cdef_startup cdefs) in
       let finish cdefs = List.map sgen_finish (List.filter is_cdef_finish cdefs) in
 
@@ -2478,7 +2489,7 @@ module Codegen (Config : CODEGEN_CONFIG) = struct
              ([Printf.sprintf "%svoid model_init(void)" (static ()); "{"; "  setup_rts();"]
              @ fst exn_boilerplate
              @ List.concat (List.map (fun r -> fst (register_init_clear r)) early_regs)
-             @ startup cdefs @ letbind_initializers
+             @ set_abstract_types @ startup cdefs @ letbind_initializers
              @ List.concat (List.map (fun r -> fst (register_init_clear r)) regs)
              @ ( if regs = [] then []
                  else [Printf.sprintf "  %s(UNIT);" (sgen_function_id (mk_id "initialize_registers"))]