Module Sarek_policy.Env

SAREK_OPT_DISABLE, SAREK_EXPLAIN. The pure part, so that tests need no environment; the module reads the variables once at initialisation and applies them with restrict and an internal revocation. Nothing here can grant.

type restriction =
  1. | Disable of optimisation
  2. | Revoke of grant

One item of SAREK_OPT_DISABLE: take an optimisation away, or revoke a grant for the whole process (the budget never holds it, whatever the program grants).

val parse : string -> restriction list * string list

parse value: the restrictions of a SAREK_OPT_DISABLE value, in order of first appearance, and the unknown items (trimmed, lowercased). Comma-separated; case-insensitive; surrounding spaces and empty items are ignored; a repeated item counts once. The items are optimisation_name (disable) and grant_name (revoke); there is no "all".

val unknown_message : string -> string

The one-line warning for an unknown item: names the variable, the item and the valid items. Written to stderr at start-up, once per item; the item is ignored.

val narrow : restriction list -> effective -> effective

narrow restrictions e: e with the optimisations disabled and the grants revoked. This is the pure model of what the module does to its own state when it reads SAREK_OPT_DISABLE: the effective policy of a kernel after start-up equals narrow of the parsed value applied to the policy without the variable (checked by the model scenario of sarek/tests/policy_env). Never adds a grant or removes a restriction: for every e, the budget of the result is below that of e (Budget.leq) and decide applies nothing on the result that it did not apply on e.

type explain =
  1. | Explain_off
  2. | Explain_stderr
  3. | Explain_unknown of string

What SAREK_EXPLAIN says. Exactly 1 turns the report on; unset, empty or 0 is off; anything else is off with a warning (explain_unknown_message).

val parse_explain : string option -> explain
val explain_unknown_message : string -> string
val explain_line : event -> string

One line, no newline, space-separated; names have their spaces replaced by '_' and an epilogue pair "p + c" is written "p+c":

sarek-explain <kernel> <target> <optimisation> applied proof=<text>
sarek-explain <kernel> <target> <optimisation> applied granted=<grant>[,<grant>] reason="<reason>" [lowering="<description>"]
sarek-explain <kernel> <target> <optimisation> applied exact
sarek-explain <kernel> <target> <optimisation> refused <reason>
sarek-explain <kernel> <target> coopmat-gate applied|refused ...
sarek-explain <kernel> - policy refused grant-on-generated-name <grant>
sarek-explain <kernel> - policy refused grant-revoked <grant>

<target> is the target of record, <optimisation> and <grant> are optimisation_name and grant_name; <reason> has its quotes and backslashes escaped. coopmat-gate is the Gate event.