Skip to content

Commit fe26ede

Browse files
AlasdairAlasdair
committed
[new release] sail (13 packages) (0.19)
CHANGES: In addition to numerous bug-fixes and smaller improvements, the following major changes and improvements have been made to the language: ##### Model configuration system Sail now supports writing configurable ISA models. There is a new language construct: ``` config x.y : T ``` which will interpret a JSON value contained at `x.y` in a provided configuration file as the Sail type T. Depending on the Sail backend, the configuration can be provided statically at build time using the `--config` flag, or at runtime for C generated from Sail. Sail is able to generate a JSON schema which describes the set of configuration parameters supported by a model, to enable static checking of configurations. See the corresponding section of the Sail manual for details. ##### Abstract types Abstract types are no longer behind an experimental flag. One can write: ``` // Declare a top-level abstract numeric type type xlen : Int // And then write top-level constraints about it constraint xlen in {32, 64, 128} ``` These abstract types are integrated with the configuration system so the following is supported. ``` type xlen : Int = config <some key> ``` ##### Stricter bitvector type indexing Stricter indexing for bitvector types. Previous versions of Sail treated `bitvector('n)` as uninhabited if `'n < 0`, but otherwise permitted such bitvector types in signatures. Now the type `bitvector('n)` is only well-formed if `'n >= 0`. This is a breaking change, as some previously permitted definitions are now rejected without additional constraints. However Sail has a new kind `Nat` which allows it to infer these `>= 0` constraints when explicit type variables are omitted, so in a function signature ``` val foo : forall 'n. bits('n) -> bool ``` the `'n` type variable will be inferred as: ``` val foo : forall ('n : Nat). bits('n) -> bool ``` This is enabled with the `--strict-bitvector` flag. We expect this behaviour will be the default in future. ##### Removed support for compressed ELF binaries As a convenience feature, the Sail C runtime allowed transparently loading compressed ELF files directly by using `gzopen`. However, it is easy to just manually decompress such files before passing them to the runtime, so we have decided to remove this feature in favour of fewer build-time dependencies for the Sail C runtime. ##### Lean backend (HIGHLY EXPERIMENTAL) This release contains the first version of a new Sail to Lean backend. It is currently highly experimental, and will likely not compile all Sail programs. ##### Sail to SystemVerilog improvements The Sail to SystemVerilog generation has been improved significantly, to the point where it is possible (with some hackery) get a working sail-riscv emulator running in Verilator. Note that we still consider this backend a work in progress, so expect to run into issues for the time being. ##### Sail to C improvements Several new flags have been implemented: * The `--c-no-mangle` flag disables name mangling (except where necessary for monomorphisation, or to avoid name-clashes), producing much more readable function names. * The `--c-generate-header` will cause Sail to generate both a `.c` file and a corresponding `.h` file, rather than just a `.c` file. There is also a `--c-header-include` flag which mirrors the `--c-include` flag when this option is used. Type synonyms are now preserved into C, which makes it possible to write external bindings that refer to polymorphic types in Sail. Code generation for the `newtype` construct has been improved.
1 parent 8f63148 commit fe26ede

File tree

13 files changed

+684
-0
lines changed
  • packages
    • libsail/libsail.0.19
    • sail_c_backend/sail_c_backend.0.19
    • sail_coq_backend/sail_coq_backend.0.19
    • sail_doc_backend/sail_doc_backend.0.19
    • sail_latex_backend/sail_latex_backend.0.19
    • sail_lean_backend/sail_lean_backend.0.19
    • sail_lem_backend/sail_lem_backend.0.19
    • sail_manifest/sail_manifest.0.19
    • sail_ocaml_backend/sail_ocaml_backend.0.19
    • sail_output/sail_output.0.19
    • sail_smt_backend/sail_smt_backend.0.19
    • sail_sv_backend/sail_sv_backend.0.19
    • sail/sail.0.19

13 files changed

+684
-0
lines changed

‎packages/libsail/libsail.0.19/opam

Lines changed: 68 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,68 @@
1+
opam-version: "2.0"
2+
synopsis:
3+
"Sail is a language for describing the instruction semantics of processors"
4+
description: """
5+
Sail is a language for describing the instruction-set
6+
architecture (ISA) semantics of processors. Sail aims to provide a
7+
engineer-friendly, vendor-pseudocode-like language for describing
8+
instruction semantics. It is essentially a first-order imperative
9+
language, but with lightweight dependent typing for numeric types and
10+
bitvector lengths, which are automatically checked using Z3. It has
11+
been used for several papers, available from
12+
http://www.cl.cam.ac.uk/~pes20/sail/.
13+
"""
14+
maintainer: ["Sail Devs <[email protected]>"]
15+
authors: [
16+
"Alasdair Armstrong"
17+
"Thomas Bauereiss"
18+
"Brian Campbell"
19+
"Shaked Flur"
20+
"Jonathan French"
21+
"Kathy Gray"
22+
"Robert Norton"
23+
"Christopher Pulte"
24+
"Peter Sewell"
25+
"Mark Wassell"
26+
]
27+
license: "BSD-2-Clause"
28+
homepage: "https://github.com/rems-project/sail"
29+
bug-reports: "https://github.com/rems-project/sail/issues"
30+
depends: [
31+
"dune" {>= "3.0"}
32+
"dune-site" {>= "3.0.2"}
33+
"bisect_ppx" {dev & >= "2.5.0"}
34+
"menhir" {>= "20240715" & build}
35+
"ott" {>= "0.28" & build}
36+
"lem" {>= "2018-12-14"}
37+
"linksem" {>= "0.3"}
38+
"conf-gmp"
39+
"yojson" {>= "1.6.0"}
40+
"pprint" {>= "20220103"}
41+
"odoc" {with-doc}
42+
]
43+
build: [
44+
["dune" "subst"] {dev}
45+
[
46+
"dune"
47+
"build"
48+
"-p"
49+
name
50+
"-j"
51+
jobs
52+
"--promote-install-files=false"
53+
"@install"
54+
"@runtest" {with-test}
55+
"@doc" {with-doc}
56+
]
57+
["dune" "install" "-p" name "--create-install-files" name]
58+
]
59+
dev-repo: "git+https://github.com/rems-project/sail.git"
60+
url {
61+
src:
62+
"https://github.com/rems-project/sail/releases/download/0.19/sail-0.19.tbz"
63+
checksum: [
64+
"sha256=5458e69ac0a5d9f52738d1946509c501897f5487accb9610b1f20c30305d23e0"
65+
"sha512=416e28b9a22784939d38fc23435f6df7a4d01660ba912994fd89adba908f95a325dd21c315ccac3e3b8c9172f0e9ce6ef87264d54ec04306c69f7c2f277452ee"
66+
]
67+
}
68+
x-commit-hash: "7ac8131a08d46be253625755d5a985be6920e876"

‎packages/sail/sail.0.19/opam

Lines changed: 73 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,73 @@
1+
opam-version: "2.0"
2+
synopsis:
3+
"Sail is a language for describing the instruction semantics of processors"
4+
description: """
5+
Sail is a language for describing the instruction-set
6+
architecture (ISA) semantics of processors. Sail aims to provide a
7+
engineer-friendly, vendor-pseudocode-like language for describing
8+
instruction semantics. It is essentially a first-order imperative
9+
language, but with lightweight dependent typing for numeric types and
10+
bitvector lengths, which are automatically checked using Z3. It has
11+
been used for several papers, available from
12+
http://www.cl.cam.ac.uk/~pes20/sail/.
13+
"""
14+
maintainer: ["Sail Devs <[email protected]>"]
15+
authors: [
16+
"Alasdair Armstrong"
17+
"Thomas Bauereiss"
18+
"Brian Campbell"
19+
"Shaked Flur"
20+
"Jonathan French"
21+
"Kathy Gray"
22+
"Robert Norton"
23+
"Christopher Pulte"
24+
"Peter Sewell"
25+
"Mark Wassell"
26+
]
27+
license: "BSD-2-Clause"
28+
homepage: "https://github.com/rems-project/sail"
29+
bug-reports: "https://github.com/rems-project/sail/issues"
30+
depends: [
31+
"dune" {>= "3.0"}
32+
"libsail" {= version}
33+
"sail_manifest" {= version & build}
34+
"sail_ocaml_backend" {= version & post}
35+
"sail_c_backend" {= version & post}
36+
"sail_smt_backend" {= version & post}
37+
"sail_sv_backend" {= version & post}
38+
"sail_lem_backend" {= version & post}
39+
"sail_coq_backend" {= version & post}
40+
"sail_lean_backend" {= version & post}
41+
"sail_latex_backend" {= version & post}
42+
"sail_doc_backend" {= version & post}
43+
"sail_output" {= version & post}
44+
"linenoise" {>= "1.1.0"}
45+
"odoc" {with-doc}
46+
]
47+
build: [
48+
["dune" "subst"] {dev}
49+
[
50+
"dune"
51+
"build"
52+
"-p"
53+
name
54+
"-j"
55+
jobs
56+
"--promote-install-files=false"
57+
"@install"
58+
"@runtest" {with-test}
59+
"@doc" {with-doc}
60+
]
61+
["dune" "install" "-p" name "--create-install-files" name]
62+
]
63+
dev-repo: "git+https://github.com/rems-project/sail.git"
64+
substs: [ "src/bin/manifest.ml" ]
65+
url {
66+
src:
67+
"https://github.com/rems-project/sail/releases/download/0.19/sail-0.19.tbz"
68+
checksum: [
69+
"sha256=5458e69ac0a5d9f52738d1946509c501897f5487accb9610b1f20c30305d23e0"
70+
"sha512=416e28b9a22784939d38fc23435f6df7a4d01660ba912994fd89adba908f95a325dd21c315ccac3e3b8c9172f0e9ce6ef87264d54ec04306c69f7c2f277452ee"
71+
]
72+
}
73+
x-commit-hash: "7ac8131a08d46be253625755d5a985be6920e876"

‎packages/sail_c_backend/sail_c_backend.0.19/opam

Lines changed: 49 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,49 @@
1+
opam-version: "2.0"
2+
synopsis: "Sail to C translation"
3+
maintainer: ["Sail Devs <[email protected]>"]
4+
authors: [
5+
"Alasdair Armstrong"
6+
"Thomas Bauereiss"
7+
"Brian Campbell"
8+
"Shaked Flur"
9+
"Jonathan French"
10+
"Kathy Gray"
11+
"Robert Norton"
12+
"Christopher Pulte"
13+
"Peter Sewell"
14+
"Mark Wassell"
15+
]
16+
license: "BSD-2-Clause"
17+
homepage: "https://github.com/rems-project/sail"
18+
bug-reports: "https://github.com/rems-project/sail/issues"
19+
depends: [
20+
"dune" {>= "3.0"}
21+
"libsail" {= version}
22+
"odoc" {with-doc}
23+
]
24+
build: [
25+
["dune" "subst"] {dev}
26+
[
27+
"dune"
28+
"build"
29+
"-p"
30+
name
31+
"-j"
32+
jobs
33+
"--promote-install-files=false"
34+
"@install"
35+
"@runtest" {with-test}
36+
"@doc" {with-doc}
37+
]
38+
["dune" "install" "-p" name "--create-install-files" name]
39+
]
40+
dev-repo: "git+https://github.com/rems-project/sail.git"
41+
url {
42+
src:
43+
"https://github.com/rems-project/sail/releases/download/0.19/sail-0.19.tbz"
44+
checksum: [
45+
"sha256=5458e69ac0a5d9f52738d1946509c501897f5487accb9610b1f20c30305d23e0"
46+
"sha512=416e28b9a22784939d38fc23435f6df7a4d01660ba912994fd89adba908f95a325dd21c315ccac3e3b8c9172f0e9ce6ef87264d54ec04306c69f7c2f277452ee"
47+
]
48+
}
49+
x-commit-hash: "7ac8131a08d46be253625755d5a985be6920e876"

‎packages/sail_coq_backend/sail_coq_backend.0.19/opam

Lines changed: 49 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,49 @@
1+
opam-version: "2.0"
2+
synopsis: "Sail to Coq translation"
3+
maintainer: ["Sail Devs <[email protected]>"]
4+
authors: [
5+
"Alasdair Armstrong"
6+
"Thomas Bauereiss"
7+
"Brian Campbell"
8+
"Shaked Flur"
9+
"Jonathan French"
10+
"Kathy Gray"
11+
"Robert Norton"
12+
"Christopher Pulte"
13+
"Peter Sewell"
14+
"Mark Wassell"
15+
]
16+
license: "BSD-2-Clause"
17+
homepage: "https://github.com/rems-project/sail"
18+
bug-reports: "https://github.com/rems-project/sail/issues"
19+
depends: [
20+
"dune" {>= "3.0"}
21+
"libsail" {= version}
22+
"odoc" {with-doc}
23+
]
24+
build: [
25+
["dune" "subst"] {dev}
26+
[
27+
"dune"
28+
"build"
29+
"-p"
30+
name
31+
"-j"
32+
jobs
33+
"--promote-install-files=false"
34+
"@install"
35+
"@runtest" {with-test}
36+
"@doc" {with-doc}
37+
]
38+
["dune" "install" "-p" name "--create-install-files" name]
39+
]
40+
dev-repo: "git+https://github.com/rems-project/sail.git"
41+
url {
42+
src:
43+
"https://github.com/rems-project/sail/releases/download/0.19/sail-0.19.tbz"
44+
checksum: [
45+
"sha256=5458e69ac0a5d9f52738d1946509c501897f5487accb9610b1f20c30305d23e0"
46+
"sha512=416e28b9a22784939d38fc23435f6df7a4d01660ba912994fd89adba908f95a325dd21c315ccac3e3b8c9172f0e9ce6ef87264d54ec04306c69f7c2f277452ee"
47+
]
48+
}
49+
x-commit-hash: "7ac8131a08d46be253625755d5a985be6920e876"

‎packages/sail_doc_backend/sail_doc_backend.0.19/opam

Lines changed: 51 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,51 @@
1+
opam-version: "2.0"
2+
synopsis: "Sail documentation generator"
3+
maintainer: ["Sail Devs <[email protected]>"]
4+
authors: [
5+
"Alasdair Armstrong"
6+
"Thomas Bauereiss"
7+
"Brian Campbell"
8+
"Shaked Flur"
9+
"Jonathan French"
10+
"Kathy Gray"
11+
"Robert Norton"
12+
"Christopher Pulte"
13+
"Peter Sewell"
14+
"Mark Wassell"
15+
]
16+
license: "BSD-2-Clause"
17+
homepage: "https://github.com/rems-project/sail"
18+
bug-reports: "https://github.com/rems-project/sail/issues"
19+
depends: [
20+
"dune" {>= "3.0"}
21+
"libsail" {= version}
22+
"base64" {>= "3.1.0"}
23+
"omd" {>= "1.3.1" & < "1.4.0"}
24+
"odoc" {with-doc}
25+
]
26+
build: [
27+
["dune" "subst"] {dev}
28+
[
29+
"dune"
30+
"build"
31+
"-p"
32+
name
33+
"-j"
34+
jobs
35+
"--promote-install-files=false"
36+
"@install"
37+
"@runtest" {with-test}
38+
"@doc" {with-doc}
39+
]
40+
["dune" "install" "-p" name "--create-install-files" name]
41+
]
42+
dev-repo: "git+https://github.com/rems-project/sail.git"
43+
url {
44+
src:
45+
"https://github.com/rems-project/sail/releases/download/0.19/sail-0.19.tbz"
46+
checksum: [
47+
"sha256=5458e69ac0a5d9f52738d1946509c501897f5487accb9610b1f20c30305d23e0"
48+
"sha512=416e28b9a22784939d38fc23435f6df7a4d01660ba912994fd89adba908f95a325dd21c315ccac3e3b8c9172f0e9ce6ef87264d54ec04306c69f7c2f277452ee"
49+
]
50+
}
51+
x-commit-hash: "7ac8131a08d46be253625755d5a985be6920e876"

‎packages/sail_latex_backend/sail_latex_backend.0.19/opam

Lines changed: 50 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,50 @@
1+
opam-version: "2.0"
2+
synopsis: "Sail to LaTeX formatting"
3+
maintainer: ["Sail Devs <[email protected]>"]
4+
authors: [
5+
"Alasdair Armstrong"
6+
"Thomas Bauereiss"
7+
"Brian Campbell"
8+
"Shaked Flur"
9+
"Jonathan French"
10+
"Kathy Gray"
11+
"Robert Norton"
12+
"Christopher Pulte"
13+
"Peter Sewell"
14+
"Mark Wassell"
15+
]
16+
license: "BSD-2-Clause"
17+
homepage: "https://github.com/rems-project/sail"
18+
bug-reports: "https://github.com/rems-project/sail/issues"
19+
depends: [
20+
"dune" {>= "3.0"}
21+
"libsail" {= version}
22+
"omd" {>= "1.3.1" & < "1.4.0"}
23+
"odoc" {with-doc}
24+
]
25+
build: [
26+
["dune" "subst"] {dev}
27+
[
28+
"dune"
29+
"build"
30+
"-p"
31+
name
32+
"-j"
33+
jobs
34+
"--promote-install-files=false"
35+
"@install"
36+
"@runtest" {with-test}
37+
"@doc" {with-doc}
38+
]
39+
["dune" "install" "-p" name "--create-install-files" name]
40+
]
41+
dev-repo: "git+https://github.com/rems-project/sail.git"
42+
url {
43+
src:
44+
"https://github.com/rems-project/sail/releases/download/0.19/sail-0.19.tbz"
45+
checksum: [
46+
"sha256=5458e69ac0a5d9f52738d1946509c501897f5487accb9610b1f20c30305d23e0"
47+
"sha512=416e28b9a22784939d38fc23435f6df7a4d01660ba912994fd89adba908f95a325dd21c315ccac3e3b8c9172f0e9ce6ef87264d54ec04306c69f7c2f277452ee"
48+
]
49+
}
50+
x-commit-hash: "7ac8131a08d46be253625755d5a985be6920e876"

‎packages/sail_lean_backend/sail_lean_backend.0.19/opam

Lines changed: 49 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,49 @@
1+
opam-version: "2.0"
2+
synopsis: "Sail to Lean translation"
3+
maintainer: ["Sail Devs <[email protected]>"]
4+
authors: [
5+
"Alasdair Armstrong"
6+
"Thomas Bauereiss"
7+
"Brian Campbell"
8+
"Shaked Flur"
9+
"Jonathan French"
10+
"Kathy Gray"
11+
"Robert Norton"
12+
"Christopher Pulte"
13+
"Peter Sewell"
14+
"Mark Wassell"
15+
]
16+
license: "BSD-2-Clause"
17+
homepage: "https://github.com/rems-project/sail"
18+
bug-reports: "https://github.com/rems-project/sail/issues"
19+
depends: [
20+
"dune" {>= "3.0"}
21+
"libsail" {= version}
22+
"odoc" {with-doc}
23+
]
24+
build: [
25+
["dune" "subst"] {dev}
26+
[
27+
"dune"
28+
"build"
29+
"-p"
30+
name
31+
"-j"
32+
jobs
33+
"--promote-install-files=false"
34+
"@install"
35+
"@runtest" {with-test}
36+
"@doc" {with-doc}
37+
]
38+
["dune" "install" "-p" name "--create-install-files" name]
39+
]
40+
dev-repo: "git+https://github.com/rems-project/sail.git"
41+
url {
42+
src:
43+
"https://github.com/rems-project/sail/releases/download/0.19/sail-0.19.tbz"
44+
checksum: [
45+
"sha256=5458e69ac0a5d9f52738d1946509c501897f5487accb9610b1f20c30305d23e0"
46+
"sha512=416e28b9a22784939d38fc23435f6df7a4d01660ba912994fd89adba908f95a325dd21c315ccac3e3b8c9172f0e9ce6ef87264d54ec04306c69f7c2f277452ee"
47+
]
48+
}
49+
x-commit-hash: "7ac8131a08d46be253625755d5a985be6920e876"

0 commit comments

Comments
 (0)