From e0cb390592606d56fcaf4ce495683f1b051f5296 Mon Sep 17 00:00:00 2001 From: Tim Hutt Date: Fri, 3 Jan 2025 17:11:20 +0000 Subject: [PATCH] Add initial support for Sail snippets (#498) This updates the Makefile to download `riscv_RV64.json` and then add a couple of example Sail snippets to the document. There are some caveats: * No syntax highlighting or hyperlinking in the code. Alasdair demonstrated this recently but I don't know if he pushed the feature to asciidoctor-sail (or maybe the version in the Docker image is too old). * The Sail code is not really written with inclusion in documentation in mind. For example the scaddr code basically calls another function which you can't see in the docs, so it's kind of useless currently. There are a few ways I can think of to fix the last point. 1. Alasdair has some fancy system to automatically modify the Sail code that is generated. He demonstrated it before to split up `execute` clauses that switch on a union, but I think we could also do things like inlining functions. 2. The output with hyperlinks will be way more useful because you can just click on the function to see its source. 3. We could probably rewrite the code a bit to focus more on readability in a spec and less on good software development practices. For example use raw bit values instead of enums. --- Makefile | 20 ++++++++++++++++---- riscv_RV64.json.url | 1 + src/attributes.adoc | 3 +++ src/insns/acperm_32bit.adoc | 4 +--- src/insns/addi16sp_16bit.adoc | 4 +--- src/insns/addi4spn_16bit.adoc | 4 +--- src/insns/adduw_32bit.adoc | 10 +++------- src/insns/auipc_32bit.adoc | 4 +--- src/insns/cadd_32bit.adoc | 8 ++------ src/insns/cbld_32bit.adoc | 19 +------------------ src/insns/cmv_32bit.adoc | 4 +--- src/insns/cram_32bit.adoc | 4 +--- src/insns/gcbase_32bit.adoc | 4 +--- src/insns/gchi_32bit.adoc | 4 +--- src/insns/gclen_32bit.adoc | 4 +--- src/insns/gcmode_32bit.adoc | 6 ++---- src/insns/gcperm_32bit.adoc | 4 +--- src/insns/gctag_32bit.adoc | 4 +--- src/insns/gctype_32bit.adoc | 4 +--- src/insns/jal_32bit.adoc | 6 ++---- src/insns/jalr_32bit.adoc | 6 ++---- src/insns/modesw_32bit.adoc | 6 ++---- src/insns/scaddr_32bit.adoc | 4 +--- src/insns/scbnds_32bit.adoc | 8 ++------ src/insns/scbndsr_32bit.adoc | 4 +--- src/insns/sceq_32bit.adoc | 4 +--- src/insns/schi_32bit.adoc | 4 +--- src/insns/scmode_32bit.adoc | 6 ++---- src/insns/scss_32bit.adoc | 4 +--- src/insns/sentry_32bit.adoc | 4 +--- src/insns/sh123add_32bit.adoc | 10 +++------- src/insns/sh123adduw_32bit.adoc | 10 +++------- src/insns/sh4add_32bit.adoc | 11 ++++------- src/insns/sh4adduw_32bit.adoc | 11 ++++------- 34 files changed, 70 insertions(+), 143 deletions(-) create mode 100644 riscv_RV64.json.url diff --git a/Makefile b/Makefile index 17495118..5c310e64 100644 --- a/Makefile +++ b/Makefile @@ -38,6 +38,12 @@ CSVS = $(wildcard $(CSV_DIR)/*.csv) GEN_DIR = $(SRC_DIR)/generated SCRIPTS_DIR = $(SRC_DIR)/scripts +# Downloaded Sail Asciidoc JSON, which includes all of +# the Sail code and can be embedded. We don't vendor it +# into this repo since it's quite large (~4MB). +SAIL_ASCIIDOC_JSON_URL_FILE = riscv_RV64.json.url +SAIL_ASCIIDOC_JSON = $(GEN_DIR)/riscv_RV64.json + # Output files PDF_RESULT := $(BUILD_DIR)/riscv-cheri.pdf HTML_RESULT := $(BUILD_DIR)/riscv-cheri.html @@ -89,7 +95,8 @@ ASCIIDOC_OPTIONS = --trace --verbose \ --failure-level=ERROR $(EXTRA_ASCIIDOC_OPTIONS) ASCIIDOC_REQUIRES = --require=asciidoctor-bibtex \ --require=asciidoctor-diagram \ - --require=asciidoctor-mathematical + --require=asciidoctor-mathematical \ + --require=asciidoctor-sail # File extension to backend map. ASCIIDOC_BACKEND_.html = html5 @@ -130,11 +137,11 @@ $(BUILD_DIR): @echo " DIR $@" @mkdir -p $@ -%.pdf: $(SRCS) $(IMGS) $(GEN_SRC) | $(BUILD_DIR) +%.pdf: $(SRCS) $(IMGS) $(GEN_SRC) $(SAIL_ASCIIDOC_JSON) | $(BUILD_DIR) @echo " DOC $@" $(BUILD_COMMAND) -%.html: $(SRCS) $(IMGS) $(GEN_SRC) | $(BUILD_DIR) +%.html: $(SRCS) $(IMGS) $(GEN_SRC) $(SAIL_ASCIIDOC_JSON) | $(BUILD_DIR) @echo " DOC $@" $(BUILD_COMMAND) @@ -143,9 +150,14 @@ $(GEN_SRC) &: $(CSVS) $(GEN_SCRIPT) @echo " GEN $@" @$(GEN_SCRIPT) -o $(GEN_DIR) --csr $(CSV_DIR)/CHERI_CSR.csv --isa $(CSV_DIR)/CHERI_ISA.csv +# Download the Sail JSON. The URL is stored in a file so if the URL changes +# Make will know to download it again. +$(SAIL_ASCIIDOC_JSON): $(SAIL_ASCIIDOC_JSON_URL_FILE) + @curl --location '$(shell cat $<)' --output $@ + # Clean clean: @echo " CLEAN" - @$(RM) -r $(PDF_RESULT) $(HTML_RESULT) $(GEN_SRC) + @$(RM) -r $(PDF_RESULT) $(HTML_RESULT) $(GEN_SRC) $(SAIL_ASCIIDOC_JSON) .PHONY: all generate clean diff --git a/riscv_RV64.json.url b/riscv_RV64.json.url new file mode 100644 index 00000000..85b94f02 --- /dev/null +++ b/riscv_RV64.json.url @@ -0,0 +1 @@ +https://github.com/CHERI-Alliance/sail-cheri-riscv/releases/download/2025-01-02/riscv_RV64.json diff --git a/src/attributes.adoc b/src/attributes.adoc index c756c011..ba87d512 100644 --- a/src/attributes.adoc +++ b/src/attributes.adoc @@ -36,6 +36,9 @@ endif::[] :xrefstyle: short :attribute-missing: warn +// Sail source code +:sail-doc: src/generated/riscv_RV64.json + /////////////////////////////////////////////////////////////////////////////// // Top-level CHERI definitions /////////////////////////////////////////////////////////////////////////////// diff --git a/src/insns/acperm_32bit.adoc b/src/insns/acperm_32bit.adoc index 30a483ce..af877d26 100644 --- a/src/insns/acperm_32bit.adoc +++ b/src/insns/acperm_32bit.adoc @@ -88,6 +88,4 @@ Prerequisites:: Operation:: + --- -TODO: Sail does not have the new encoding of the permissions field. --- +sail::execute[clause="ACPERM(_, _, _)",part=body,unindent] diff --git a/src/insns/addi16sp_16bit.adoc b/src/insns/addi16sp_16bit.adoc index e8b1c661..03645123 100644 --- a/src/insns/addi16sp_16bit.adoc +++ b/src/insns/addi16sp_16bit.adoc @@ -38,6 +38,4 @@ Prerequisites for {cheri_int_mode_name}:: {cheri_cap_mode_name} Operation:: + --- -TODO --- +sail::execute[clause="C_ADDI16SP_capmode(_)",part=body,unindent] diff --git a/src/insns/addi4spn_16bit.adoc b/src/insns/addi4spn_16bit.adoc index 52534fa6..324049a8 100644 --- a/src/insns/addi4spn_16bit.adoc +++ b/src/insns/addi4spn_16bit.adoc @@ -37,6 +37,4 @@ Prerequisites for C.ADDI4SPN:: {cheri_cap_mode_name} Operation:: + --- -TODO --- +sail::execute[clause="C_ADDI4SPN_capmode(_, _)",part=body,unindent] diff --git a/src/insns/adduw_32bit.adoc b/src/insns/adduw_32bit.adoc index 4cbaaa95..433c4fae 100644 --- a/src/insns/adduw_32bit.adoc +++ b/src/insns/adduw_32bit.adoc @@ -38,13 +38,9 @@ Prerequisites for {cheri_int_mode_name}:: RV64, {cheri_default_ext_name}, Zba {cheri_cap_mode_name} Operation:: -[source,SAIL,subs="verbatim,quotes"] --- -TBD --- ++ +sail::execute[clause="ZBA_RTYPEUW_capmode(_, _, _, _)",part=body,unindent] {cheri_int_mode_name} Operation:: + --- -TODO --- +sail::execute[clause="ZBA_RTYPEUW(_, _, _, _)",part=body,unindent] diff --git a/src/insns/auipc_32bit.adoc b/src/insns/auipc_32bit.adoc index bc3be14e..e29ddd84 100644 --- a/src/insns/auipc_32bit.adoc +++ b/src/insns/auipc_32bit.adoc @@ -39,6 +39,4 @@ Prerequisites for {cheri_int_mode_name}:: Operation for AUIPC:: + --- -TODO --- +sail::execute[clause="AUIPC_capmode(_, _)",part=body,unindent] diff --git a/src/insns/cadd_32bit.adoc b/src/insns/cadd_32bit.adoc index 3de64d49..2b269e13 100644 --- a/src/insns/cadd_32bit.adoc +++ b/src/insns/cadd_32bit.adoc @@ -58,12 +58,8 @@ Prerequisites:: Operation (CADD):: + --- -TODO --- +sail::execute[clause="CADD(_, _, _)",part=body,unindent] Operation (CADDI):: + --- -TODO --- +sail::execute[clause="CADDI(_, _, _)",part=body,unindent] diff --git a/src/insns/cbld_32bit.adoc b/src/insns/cbld_32bit.adoc index 776cbe79..7ba1eefb 100644 --- a/src/insns/cbld_32bit.adoc +++ b/src/insns/cbld_32bit.adoc @@ -49,23 +49,6 @@ include::require_cre.adoc[] Prerequisites:: {cheri_base_ext_name} -Simplified Operation TODO #not debugged much easier to read than the existing SAIL# :: -[source,SAIL,subs="verbatim,quotes"] --- -let cs1_val = C(cs1); -let cs2_val = C(cs2) [with tag=1]; -//isCapSubset includes derivability checks on both operands -let subset = isCapSubset(cs1_val, cs2_val); -//Clear cd.tag if cs2 isn't a subset of cs1, or if -//cs1 is untagged or sealed, or if either is underivable -C(cd) = clearTagIf(cs2_val, not(subset) | - not(cs1_val.tag) | - isCapSealed(cs1_val)); -RETIRE_SUCCESS --- - Operation:: + --- -TODO: Original Sail looks at otype field, etc that don't exist --- +sail::execute[clause="CBLD(_, _, _)",part=body,unindent] diff --git a/src/insns/cmv_32bit.adoc b/src/insns/cmv_32bit.adoc index abc7ad01..8776e2a4 100644 --- a/src/insns/cmv_32bit.adoc +++ b/src/insns/cmv_32bit.adoc @@ -39,6 +39,4 @@ Prerequisites:: Operation:: + --- -TODO --- +sail::execute[clause="CMV(_, _)",part=body,unindent] diff --git a/src/insns/cram_32bit.adoc b/src/insns/cram_32bit.adoc index 49546944..b2f96ed9 100644 --- a/src/insns/cram_32bit.adoc +++ b/src/insns/cram_32bit.adoc @@ -25,6 +25,4 @@ Prerequisites:: Operation:: + --- -TODO --- +sail::execute[clause="CRAM(_, _)",part=body,unindent] diff --git a/src/insns/gcbase_32bit.adoc b/src/insns/gcbase_32bit.adoc index 96b072d7..1a39d392 100644 --- a/src/insns/gcbase_32bit.adoc +++ b/src/insns/gcbase_32bit.adoc @@ -32,6 +32,4 @@ Prerequisites:: Operation:: + --- -TODO --- +sail::execute[clause="GCBASE(_, _)",part=body,unindent] diff --git a/src/insns/gchi_32bit.adoc b/src/insns/gchi_32bit.adoc index 4afc04e4..a874b160 100644 --- a/src/insns/gchi_32bit.adoc +++ b/src/insns/gchi_32bit.adoc @@ -29,6 +29,4 @@ Prerequisites:: Operation:: + --- -TODO --- +sail::execute[clause="GCHI(_, _)",part=body,unindent] diff --git a/src/insns/gclen_32bit.adoc b/src/insns/gclen_32bit.adoc index 2703b0ab..2fad31e3 100644 --- a/src/insns/gclen_32bit.adoc +++ b/src/insns/gclen_32bit.adoc @@ -36,6 +36,4 @@ Prerequisites:: Operation:: + --- -TODO --- +sail::execute[clause="GCLEN(_, _)",part=body,unindent] diff --git a/src/insns/gcmode_32bit.adoc b/src/insns/gcmode_32bit.adoc index 1f7cb056..fdfacf3e 100644 --- a/src/insns/gcmode_32bit.adoc +++ b/src/insns/gcmode_32bit.adoc @@ -27,7 +27,5 @@ Prerequisites:: {cheri_default_ext_name} Operation:: -[source,SAIL,subs="verbatim,quotes"] --- -TODO --- ++ +sail::execute[clause="GCMODE(_, _)",part=body,unindent] diff --git a/src/insns/gcperm_32bit.adoc b/src/insns/gcperm_32bit.adoc index 6333060b..36c06a42 100644 --- a/src/insns/gcperm_32bit.adoc +++ b/src/insns/gcperm_32bit.adoc @@ -41,6 +41,4 @@ Prerequisites:: Operation:: + --- -TODO: The encoding of permissions changed. --- +sail::execute[clause="GCPERM(_, _)",part=body,unindent] diff --git a/src/insns/gctag_32bit.adoc b/src/insns/gctag_32bit.adoc index 4a5cf898..8a924b94 100644 --- a/src/insns/gctag_32bit.adoc +++ b/src/insns/gctag_32bit.adoc @@ -28,6 +28,4 @@ Prerequisites:: Operation:: + --- -TODO --- +sail::execute[clause="GCTAG(_, _)",part=body,unindent] diff --git a/src/insns/gctype_32bit.adoc b/src/insns/gctype_32bit.adoc index c0b69b70..fd9448c9 100644 --- a/src/insns/gctype_32bit.adoc +++ b/src/insns/gctype_32bit.adoc @@ -43,6 +43,4 @@ Prerequisites:: Operation:: + --- -TODO --- +sail::execute[clause="GCTYPE(_, _)",part=body,unindent] diff --git a/src/insns/jal_32bit.adoc b/src/insns/jal_32bit.adoc index 8d6522cb..f4a036d9 100644 --- a/src/insns/jal_32bit.adoc +++ b/src/insns/jal_32bit.adoc @@ -48,8 +48,6 @@ Prerequisites for {cheri_cap_mode_name}:: Prerequisites for {cheri_int_mode_name}:: {cheri_default_ext_name} -Operation:: +{cheri_cap_mode_name} Operation:: + --- -TODO --- +sail::execute[clause="JAL_capmode(_, _)",part=body,unindent] diff --git a/src/insns/jalr_32bit.adoc b/src/insns/jalr_32bit.adoc index 532640fe..a9d9ca8a 100644 --- a/src/insns/jalr_32bit.adoc +++ b/src/insns/jalr_32bit.adoc @@ -65,8 +65,6 @@ Prerequisites {cheri_cap_mode_name}:: Prerequisites {cheri_int_mode_name}:: {cheri_default_ext_name} -Operation:: +{cheri_cap_mode_name} Operation:: + --- -TBD --- +sail::execute[clause="JALR_capmode(_, _)",part=body,unindent] diff --git a/src/insns/modesw_32bit.adoc b/src/insns/modesw_32bit.adoc index 7b3f015f..14956405 100644 --- a/src/insns/modesw_32bit.adoc +++ b/src/insns/modesw_32bit.adoc @@ -34,7 +34,5 @@ Prerequisites:: {cheri_default_ext_name} Operation:: -[source,SAIL,subs="verbatim,quotes"] --- -TODO --- ++ +sail::execute[clause="MODESW()",part=body,unindent] diff --git a/src/insns/scaddr_32bit.adoc b/src/insns/scaddr_32bit.adoc index 1952825d..812366d6 100644 --- a/src/insns/scaddr_32bit.adoc +++ b/src/insns/scaddr_32bit.adoc @@ -34,6 +34,4 @@ Prerequisites:: Operation:: + --- -TODO --- +sail::execute[clause="SCADDR(_, _, _)",part=body,unindent] diff --git a/src/insns/scbnds_32bit.adoc b/src/insns/scbnds_32bit.adoc index 5b6455b9..9947fe6c 100644 --- a/src/insns/scbnds_32bit.adoc +++ b/src/insns/scbnds_32bit.adoc @@ -54,12 +54,8 @@ Prerequisites:: Operation for SCBNDS:: + --- -TODO --- +sail::execute[clause="SCBNDS(_, _, _)",part=body,unindent] Operation for SCBNDSI:: + --- -TODO --- +sail::execute[clause="SCBNDSI(_, _, _, _)",part=body,unindent] diff --git a/src/insns/scbndsr_32bit.adoc b/src/insns/scbndsr_32bit.adoc index 67bb9bf2..da695b59 100644 --- a/src/insns/scbndsr_32bit.adoc +++ b/src/insns/scbndsr_32bit.adoc @@ -36,6 +36,4 @@ Prerequisites:: Operation for SCBNDSR:: + --- -TODO --- +sail::execute[clause="SCBNDSR(_, _, _)",part=body,unindent] diff --git a/src/insns/sceq_32bit.adoc b/src/insns/sceq_32bit.adoc index e9087519..3e60d7ec 100644 --- a/src/insns/sceq_32bit.adoc +++ b/src/insns/sceq_32bit.adoc @@ -30,6 +30,4 @@ Prerequisites:: Operation:: + --- -TODO --- +sail::execute[clause="SCEQ(_, _, _)",part=body,unindent] diff --git a/src/insns/schi_32bit.adoc b/src/insns/schi_32bit.adoc index 496070e8..23dba696 100644 --- a/src/insns/schi_32bit.adoc +++ b/src/insns/schi_32bit.adoc @@ -30,6 +30,4 @@ Prerequisites:: Operation:: + --- -TODO --- +sail::execute[clause="SCHI(_, _, _)",part=body,unindent] diff --git a/src/insns/scmode_32bit.adoc b/src/insns/scmode_32bit.adoc index 9d7a1045..f5d0c7f8 100644 --- a/src/insns/scmode_32bit.adoc +++ b/src/insns/scmode_32bit.adoc @@ -35,7 +35,5 @@ Prerequisites:: {cheri_default_ext_name} Operation :: -[source,SAIL,subs="verbatim,quotes"] --- -TODO --- ++ +sail::execute[clause="SCMODE(_, _, _)",part=body,unindent] diff --git a/src/insns/scss_32bit.adoc b/src/insns/scss_32bit.adoc index c9db1951..17c882ac 100644 --- a/src/insns/scss_32bit.adoc +++ b/src/insns/scss_32bit.adoc @@ -42,6 +42,4 @@ Prerequisites:: Operation:: + --- -TODO --- +sail::execute[clause="SCSS(_, _, _)",part=body,unindent] diff --git a/src/insns/sentry_32bit.adoc b/src/insns/sentry_32bit.adoc index 1f16255b..6ac01bd0 100644 --- a/src/insns/sentry_32bit.adoc +++ b/src/insns/sentry_32bit.adoc @@ -36,6 +36,4 @@ Prerequisites:: Operation:: + --- -TODO --- +sail::execute[clause="SENTRY(_, _)",part=body,unindent] diff --git a/src/insns/sh123add_32bit.adoc b/src/insns/sh123add_32bit.adoc index f4f83f94..a472c2db 100644 --- a/src/insns/sh123add_32bit.adoc +++ b/src/insns/sh123add_32bit.adoc @@ -57,13 +57,9 @@ Prerequisites for {cheri_int_mode_name}:: {cheri_default_ext_name}, Zba {cheri_cap_mode_name} Operation:: -[source,SAIL,subs="verbatim,quotes"] --- -TODO --- ++ +sail::execute[clause="ZBA_RTYPE_capmode(_, _, _, _)",part=body,unindent] {cheri_int_mode_name} Operation:: + --- -TODO --- +sail::execute[clause="ZBA_RTYPE(_, _, _, _)",part=body,unindent] diff --git a/src/insns/sh123adduw_32bit.adoc b/src/insns/sh123adduw_32bit.adoc index 91e32d78..36cea502 100644 --- a/src/insns/sh123adduw_32bit.adoc +++ b/src/insns/sh123adduw_32bit.adoc @@ -57,13 +57,9 @@ Prerequisites for {cheri_int_mode_name}:: RV64, {cheri_default_ext_name}, Zba {cheri_cap_mode_name} Operation:: -[source,SAIL,subs="verbatim,quotes"] --- -TODO --- ++ +sail::execute[clause="ZBA_RTYPEUW_capmode(_, _, _, _)",part=body,unindent] {cheri_int_mode_name} Operation:: + --- -TODO --- +sail::execute[clause="ZBA_RTYPEUW(_, _, _, _)",part=body,unindent] diff --git a/src/insns/sh4add_32bit.adoc b/src/insns/sh4add_32bit.adoc index 53c75cb7..342f4d0d 100644 --- a/src/insns/sh4add_32bit.adoc +++ b/src/insns/sh4add_32bit.adoc @@ -51,12 +51,9 @@ Prerequisites for {cheri_int_mode_name}:: RV64, {sh4add_ext_name} {cheri_cap_mode_name} Operation:: -[source,SAIL,subs="verbatim,quotes"] --- -TBD --- ++ +sail::execute[clause="ZBA_SH4ADD_capmode(_, _, _)",part=body,unindent] {cheri_int_mode_name} Operation:: --- -TBD --- ++ +sail::execute[clause="ZBA_SH4ADD(_, _, _)",part=body,unindent] diff --git a/src/insns/sh4adduw_32bit.adoc b/src/insns/sh4adduw_32bit.adoc index 3c30ccab..71bc17f0 100644 --- a/src/insns/sh4adduw_32bit.adoc +++ b/src/insns/sh4adduw_32bit.adoc @@ -47,12 +47,9 @@ Prerequisites for {cheri_int_mode_name}:: RV64, {sh4add_ext_name} {cheri_cap_mode_name} Operation:: -[source,SAIL,subs="verbatim,quotes"] --- -TBD --- ++ +sail::execute[clause="ZBA_SH4ADDUW_capmode(_, _, _)",part=body,unindent] {cheri_int_mode_name} Operation:: --- -TBD --- ++ +sail::execute[clause="ZBA_SH4ADDUW(_, _, _)",part=body,unindent]