From b7b561343dbc4d8661b8619d25f105b3c0d16245 Mon Sep 17 00:00:00 2001 From: Julien Freche Date: Wed, 12 Aug 2020 11:46:25 -0700 Subject: [PATCH] c2: make the global state API configurable for externally defined get/set functions --- etc/default_config.json | 7 +++++- src/jib/c_codegen.ml | 55 +++++++++++++++++++++++++++++++++-------- 2 files changed, 51 insertions(+), 11 deletions(-) diff --git a/etc/default_config.json b/etc/default_config.json index 79f166af9..945aa19c5 100644 --- a/etc/default_config.json +++ b/etc/default_config.json @@ -25,6 +25,11 @@ // The sail_state struct will be passed to the following array // of primops, which are specified via the "foo" string from // val id = "foo" : ... in Sail. - "state_primops": [] + "state_primops": [], + // Control which sail_state variables accessors will be implemented + // by the consumer of the library. This is a list of regular expressions, + // if one of those regular expression matches the name of a sail_state variable, + // only the declaration of the accessors will be generated. + "external_state_api" : [] } } diff --git a/src/jib/c_codegen.ml b/src/jib/c_codegen.ml index 9e8d911aa..22b917887 100644 --- a/src/jib/c_codegen.ml +++ b/src/jib/c_codegen.ml @@ -116,6 +116,11 @@ type codegen_options = { (** Primitives in this set will be passed a pointer to the sail_state struct *) state_primops : StringSet.t; + (** Control which sail_state variables accessors will be implemented + by the consumer of the library. This is a list of regular expressions, + if one of those regular expression matches the name of a sail_state variable, + only the declaration of the accessors will be generated. *) + external_state_api : string list; } let initial_options = { @@ -124,6 +129,7 @@ let initial_options = { extra_headers = []; extra_state = []; state_primops = StringSet.empty; + external_state_api = []; } let add_export opts id = { opts with exports = Bindings.add id (string_of_id id) opts.exports } @@ -133,6 +139,9 @@ let add_custom_export opts id into = { opts with exports = Bindings.add id into let add_mangled_rename opts (from, into) = { opts with exports_mangled = StringMap.add from into opts.exports_mangled } +let add_external_state_api_regex opts regex = + { opts with external_state_api = regex :: opts.external_state_api } + let add_export_uid opts (id, ctyps) = match ctyps with | [] -> { opts with exports = Bindings.add id (string_of_id id) opts.exports } @@ -226,6 +235,17 @@ let options_from_json json cdefs = opts | json -> bad_key "state_primops" json in + let process_external_state_api opts = function + | `String member -> add_external_state_api_regex opts member + | json -> bad_key "external_state_api" json + in + let opts = match member "external_state_api" json with + | `List members -> List.fold_left process_external_state_api opts members + | `Null -> + Reporting.simple_warn "No external_state_api key in codegen json configuration"; + opts + | json -> bad_key "external_state_api" json + in opts module type Options = sig @@ -1553,16 +1573,25 @@ let codegen_state_struct_def ctx = function | _ -> empty +let codegen_state_function_body_on_match id body = + let is_external = List.exists (fun regex -> Str.string_match (Str.regexp regex) id 0) O.opts.external_state_api in + if is_external then + ("" ,";") + else + ("static inline ", Printf.sprintf " { %s }" body) + let codegen_state_api_struct id ctyp = match ctyp with | CT_struct (_, fields) -> let codegen_state_api_field ((fid, _), ctyp) = if is_api_ctyp ctyp then - ksprintf string "static inline void state_set_%s_in_%s(sail_state* st, %s u) { st->%s.%s = u; }" - (sgen_id fid) (sgen_id id) (sgen_ctyp ctyp) (sgen_id id) (sgen_id fid) + let set_attrs, set_body = codegen_state_function_body_on_match (sgen_id fid) (Printf.sprintf "st->%s.%s = u;" (sgen_id id) (sgen_id fid)) in + let get_attrs, get_body = codegen_state_function_body_on_match (sgen_id fid) (Printf.sprintf "return st->%s.%s;" (sgen_id id) (sgen_id fid)) in + ksprintf string "%svoid state_set_%s_in_%s(sail_state* st, %s u)%s" + set_attrs (sgen_id fid) (sgen_id id) (sgen_ctyp ctyp) set_body ^^ hardline - ^^ ksprintf string "static inline %s state_get_%s_in_%s(sail_state* st) { return st->%s.%s; }" - (sgen_ctyp ctyp) (sgen_id fid) (sgen_id id) (sgen_id id) (sgen_id fid) + ^^ ksprintf string "%s%s state_get_%s_in_%s(sail_state* st)%s" + get_attrs (sgen_ctyp ctyp) (sgen_id fid) (sgen_id id) get_body else empty in @@ -1570,16 +1599,22 @@ let codegen_state_api_struct id ctyp = | _ -> empty let codegen_state_api_vector id ctyp vctyp = - string (Printf.sprintf "static inline void state_vector_update_%s(sail_state* st, %s *rop, %s op, sail_int n, %s elem) { vector_update_%s(rop, op, n, elem); }" - (sgen_id id) (sgen_ctyp ctyp) (sgen_ctyp ctyp) (sgen_ctyp vctyp) (sgen_ctyp ctyp)) ^^ hardline ^^ - string (Printf.sprintf "static inline %s state_vector_access_%s(sail_state* st, %s op, sail_int n) { return vector_access_%s(op, n); }" - (sgen_ctyp vctyp) (sgen_id id) (sgen_ctyp ctyp) (sgen_ctyp ctyp)) ^^ hardline + let attrs, body = codegen_state_function_body_on_match (sgen_id id) (Printf.sprintf "vector_update_%s(rop, op, n, elem);" (sgen_ctyp ctyp)) in + string (Printf.sprintf "%svoid state_vector_update_%s(sail_state* st, %s *rop, %s op, sail_int n, %s elem)%s" + attrs (sgen_id id) (sgen_ctyp ctyp) (sgen_ctyp ctyp) (sgen_ctyp vctyp) body) + ^^ hardline ^^ + let attrs, body = codegen_state_function_body_on_match (sgen_id id) (Printf.sprintf "return vector_access_%s(op, n);" (sgen_ctyp ctyp)) in + string (Printf.sprintf "%s%s state_vector_access_%s(sail_state* st, %s op, sail_int n)%s" + attrs (sgen_ctyp vctyp) (sgen_id id) (sgen_ctyp ctyp) body) + ^^ hardline let codegen_state_api_reg_dec id ctyp = begin match ctyp with | _ when is_api_ctyp ctyp -> - ksprintf string "static inline %s state_get_%s(sail_state* st) { return st->%s; }" (sgen_ctyp ctyp) (sgen_id id) (sgen_id id) ^^ hardline ^^ - ksprintf string "static inline void state_set_%s(sail_state* st, %s n) { st->%s = n; }" (sgen_id id) (sgen_ctyp ctyp) (sgen_id id) ^^ hardline ^^ + let attrs, body = codegen_state_function_body_on_match (sgen_id id) (Printf.sprintf "return st->%s;" (sgen_id id)) in + ksprintf string "%s%s state_get_%s(sail_state* st)%s" attrs (sgen_ctyp ctyp) (sgen_id id) body ^^ hardline ^^ + let attrs, body = codegen_state_function_body_on_match (sgen_id id) (Printf.sprintf "st->%s = n;" (sgen_id id)) in + ksprintf string "%svoid state_set_%s(sail_state* st, %s n)%s" attrs (sgen_id id) (sgen_ctyp ctyp) body ^^ hardline ^^ codegen_state_api_struct id ctyp | CT_vector (_, vctyp) when is_api_ctyp vctyp -> codegen_state_api_vector id ctyp vctyp | CT_fvector (_, _, vctyp) when is_api_ctyp vctyp -> codegen_state_api_vector id ctyp vctyp