Skip to content

Commit

Permalink
Sail configuration system
Browse files Browse the repository at this point in the history
This commit introduces a method for configuring Sail models using
a JSON configuration file. It introduces a new construct into the language:
```
config a.b.c : T
```
which gets the value of the json object a.b.c in the configuration file
and interprets it as the Sail type T

Configuration options can be instantiated at compile time using
```
sail --config c.json <files>
```
which is useful for Sail targets like SMT or SystemVerilog, or
they can be accessed at runtime, which allows for building a configurable emulator
  • Loading branch information
Alasdair committed Jan 8, 2025
1 parent 1cc3881 commit f997f2b
Show file tree
Hide file tree
Showing 66 changed files with 4,569 additions and 208 deletions.
32 changes: 32 additions & 0 deletions THIRD_PARTY_FILES.md
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,13 @@ https://github.com/asciidoctor/asciidoctor
| ------------ | ----------------------- | ----------- |
| MIT | doc/asciidoc/manual.css | Asciidoctor |

The following files are from cJSON https://github.com/DaveGamble/cJSON

| License | Files | Source |
| ------------ | ----------------------- | ------ |
| MIT | lib/json/cJSON.c | cJSON |
| MIT | lib/json/cJSON.h | cJSON |

CIL
===

Expand Down Expand Up @@ -113,3 +120,28 @@ LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
THE SOFTWARE.
```

cJSON
=====

```
Copyright (c) 2009-2017 Dave Gamble and cJSON contributors
Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in
all copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
THE SOFTWARE.
```
2 changes: 1 addition & 1 deletion editors/sail-mode.el
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@

(defconst sail-keywords
'("val" "outcome" "function" "type" "struct" "union" "enum" "let" "var" "if" "then" "by"
"else" "match" "in" "return" "register" "ref" "forall" "operator" "effect"
"else" "match" "in" "return" "register" "ref" "forall" "operator" "effect" "config"
"overload" "cast" "sizeof" "constant" "constraint" "default" "assert" "newtype" "from"
"pure" "impure" "monadic" "infixl" "infixr" "infix" "scattered" "end" "try" "catch" "and" "to" "private"
"throw" "clause" "as" "repeat" "until" "while" "do" "foreach" "bitfield"
Expand Down
3 changes: 3 additions & 0 deletions language/jib.ott
Original file line number Diff line number Diff line change
Expand Up @@ -138,6 +138,7 @@ cval :: 'V_' ::=
| cval nat0 nat1 :: :: tuple_member
| op ( cval0 , ... , cvaln ) :: :: call
| cval . id :: :: field
| string0 . ... . stringn :: :: config_key

% Note that init / clear are sometimes referred to as create / kill

Expand Down Expand Up @@ -196,6 +197,8 @@ ctyp :: 'CT_' ::=
| poly kid :: :: poly

| memory_writes :: :: memory_writes
% Used for configuration, an immutable reference to some json data
| json :: :: json

clexp :: 'CL_' ::=
| name : ctyp :: :: id
Expand Down
10 changes: 6 additions & 4 deletions language/sail.ott
Original file line number Diff line number Diff line change
Expand Up @@ -455,8 +455,8 @@ grammar
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

loop :: loop ::= {{ phantom }}
| while :: :: while
| until :: :: until
| while :: :: while
| until :: :: until

internal_loop_measure :: 'Measure_' ::=
{{ com internal syntax for an optional termination measure for a loop }}
Expand Down Expand Up @@ -516,8 +516,10 @@ exp :: 'E_' ::=
{{ com the value of $[[nexp]]$ at run time }}

| return exp :: :: return {{ com return $[[exp]]$ from current function }}
| exit exp :: :: exit
{{ com halt all current execution }}
| exit exp :: :: exit {{ com halt all current execution }}

| config string1 . ... . stringn :: :: config {{ com model configuration value }}

| ref id :: :: ref
| throw exp :: :: throw
| try exp catch { pexp1 , ... , pexpn } :: :: try
Expand Down
20 changes: 20 additions & 0 deletions lib/json/LICENSE
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
Copyright (c) 2009-2017 Dave Gamble and cJSON contributors

Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in
all copies or substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
THE SOFTWARE.

Loading

0 comments on commit f997f2b

Please sign in to comment.