diff options
| author | Alasdair Armstrong | 2018-06-26 14:44:27 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-06-26 22:48:16 +0100 |
| commit | a5bc362fca3d8a7c6d49b35dcf0b63440d23303c (patch) | |
| tree | 2a942f6cf06c2fcd5888484861300b416b93060f /language | |
| parent | e65b6b3cd2a3259f1d709fc8a0fb11fdbf667a39 (diff) | |
Add configuration registers so __SetConfig ASL can be translated
Registers can now be marked as configuration registers, for example:
register configuration CFG_RVBAR = 0x1300000
They work like ordinary registers except they can only be set by
functions with the 'configuration' effect and have no effect when
read. They also have an initialiser, like a let-binding. Internally
there is a new reg_dec constructor DEC_config. They are intended to
represent configuration parameters for the model, which can change
between runs, but don't change during execution. Currently they'll
only work when compiled to C. Internally registers can now have custom
effects for reads and writes rather than just rreg and wreg, so the
type signatures of Env.add_register and Env.get_register have changed,
as well as the Register lvar, so in the type checker we now write:
Env.add_register id read_effect write_effect typ
rather than
Env.add_register id typ
For the corresponding change to ASL parser there's a function
is_config in asl_to_sail.ml which controls what becomes a
configuration register for ARM. Some things we have to keep as
let-bindings because Sail can't handle them changing at runtime -
e.g. the length of vectors in other top-level definitions. Luckily
__SetConfig doesn't (yet) try to change those options.
Together these changes allow us to translate the ASL __SetConfig
function, which means we should get command-line option compatibility
with ArchEx for running the ARM conformance tests.
Diffstat (limited to 'language')
| -rw-r--r-- | language/bytecode.ott | 4 | ||||
| -rw-r--r-- | language/sail.ott | 2 |
2 files changed, 5 insertions, 1 deletions
diff --git a/language/bytecode.ott b/language/bytecode.ott index 895ac34b..32b04bb4 100644 --- a/language/bytecode.ott +++ b/language/bytecode.ott @@ -145,7 +145,9 @@ instr :: 'I_' ::= | ctyp id = cval :: :: reinit cdef :: 'CDEF_' ::= - | register id : ctyp :: :: reg_dec + | register id : ctyp = { + instr0 ; ... ; instrn + } :: :: reg_dec | ctype_def :: :: type | let nat ( id0 : ctyp0 , ... , idn : ctypn ) = { instr0 ; ... ; instrm diff --git a/language/sail.ott b/language/sail.ott index 3332034f..12a71b9f 100644 --- a/language/sail.ott +++ b/language/sail.ott @@ -230,6 +230,7 @@ base_effect :: 'BE_' ::= | unspec :: :: unspec {{ com unspecified values }} | nondet :: :: nondet {{ com nondeterminism, from $[[nondet]]$ }} | escape :: :: escape {{ com potential exception }} + | config :: :: config {{ com configuration option }} effect :: 'Effect_' ::= {{ com effect set, of kind $[[Effect]]$ }} @@ -1096,6 +1097,7 @@ dec_spec :: 'DEC_' ::= {{ com register declarations }} {{ aux _ annot }} {{ auxparam 'a }} | register typ id :: :: reg + | register configuration id : typ = exp :: :: config | register alias id = alias_spec :: :: alias | register alias typ id = alias_spec :: :: typ_alias |