Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

c2: make the global state API configurable for externally defined get/set functions #83

Merged
merged 1 commit into from
Aug 24, 2020
Merged

c2: make the global state API configurable for externally defined get/set functions #83

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 6 additions & 1 deletion etc/default_config.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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" : []
}
}
55 changes: 45 additions & 10 deletions src/jib/c_codegen.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 = {
Expand All @@ -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 }
Expand All @@ -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 }
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -1553,33 +1573,48 @@ 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
separate_map hardline codegen_state_api_field fields ^^ hardline
| _ -> 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
Expand Down