Add initial support for Sail snippets (riscv#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

@@ -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

riscv_RV64.json.url

@@ -0,0 +1 @@
+https://github.com/CHERI-Alliance/sail-cheri-riscv/releases/download/2025-01-02/riscv_RV64.json

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
 ///////////////////////////////////////////////////////////////////////////////

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]

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]

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]

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]

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]

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]

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]

src/insns/cmv_32bit.adoc

@@ -39,6 +39,4 @@ Prerequisites::
 
 Operation::
 +
---
-TODO
---
+sail::execute[clause="CMV(_, _)",part=body,unindent]

src/insns/cram_32bit.adoc

@@ -25,6 +25,4 @@ Prerequisites::
 
 Operation::
 +
---
-TODO
---
+sail::execute[clause="CRAM(_, _)",part=body,unindent]

src/insns/gcbase_32bit.adoc

@@ -32,6 +32,4 @@ Prerequisites::
 
 Operation::
 +
---
-TODO
---
+sail::execute[clause="GCBASE(_, _)",part=body,unindent]

src/insns/gchi_32bit.adoc

@@ -29,6 +29,4 @@ Prerequisites::
 
 Operation::
 +
---
-TODO
---
+sail::execute[clause="GCHI(_, _)",part=body,unindent]

src/insns/gclen_32bit.adoc

@@ -36,6 +36,4 @@ Prerequisites::
 
 Operation::
 +
---
-TODO
---
+sail::execute[clause="GCLEN(_, _)",part=body,unindent]

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]

src/insns/gcperm_32bit.adoc

@@ -41,6 +41,4 @@ Prerequisites::
 
 Operation::
 +
---
-TODO: The encoding of permissions changed.
---
+sail::execute[clause="GCPERM(_, _)",part=body,unindent]

src/insns/gctag_32bit.adoc

@@ -28,6 +28,4 @@ Prerequisites::
 
 Operation::
 +
---
-TODO
---
+sail::execute[clause="GCTAG(_, _)",part=body,unindent]

src/insns/gctype_32bit.adoc

@@ -43,6 +43,4 @@ Prerequisites::
 
 Operation::
 +
---
-TODO
---
+sail::execute[clause="GCTYPE(_, _)",part=body,unindent]

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]

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]

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]

src/insns/scaddr_32bit.adoc

@@ -34,6 +34,4 @@ Prerequisites::
 
 Operation::
 +
---
-TODO
---
+sail::execute[clause="SCADDR(_, _, _)",part=body,unindent]

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]

src/insns/scbndsr_32bit.adoc

@@ -36,6 +36,4 @@ Prerequisites::
 
 Operation for SCBNDSR::
 +
---
-TODO
---
+sail::execute[clause="SCBNDSR(_, _, _)",part=body,unindent]

src/insns/sceq_32bit.adoc

@@ -30,6 +30,4 @@ Prerequisites::
 
 Operation::
 +
---
-TODO
---
+sail::execute[clause="SCEQ(_, _, _)",part=body,unindent]

src/insns/schi_32bit.adoc

@@ -30,6 +30,4 @@ Prerequisites::
 
 Operation::
 +
---
-TODO
---
+sail::execute[clause="SCHI(_, _, _)",part=body,unindent]

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]

src/insns/scss_32bit.adoc

@@ -42,6 +42,4 @@ Prerequisites::
 
 Operation::
 +
---
-TODO
---
+sail::execute[clause="SCSS(_, _, _)",part=body,unindent]

src/insns/sentry_32bit.adoc

@@ -36,6 +36,4 @@ Prerequisites::
 
 Operation::
 +
---
-TODO
---
+sail::execute[clause="SENTRY(_, _)",part=body,unindent]

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]

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]

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]