diff --git a/Makefile b/Makefile index 8b29caa..9f48a3b 100644 --- a/Makefile +++ b/Makefile @@ -8,6 +8,7 @@ ADOC_EXTRA_DEPS=attributes.adoc OUTPUT_DIR?=output OUTPUT_PDF=$(OUTPUT_DIR)/main.pdf OUTPUT_HTML=$(OUTPUT_DIR)/index.html +REFS_TABLE_FILE=./refs/sail.txt all: $(OUTPUT_PDF) $(OUTPUT_HTML) @@ -21,13 +22,13 @@ else CONTAINER_IMG=$(EXTERNAL_CONTAINER_IMG) endif -$(OUTPUT_PDF): $(ADOC_TOP_SRC) $(ADOC_PARTS_SRC) $(ADOC_EXTRA_DEPS) $(CONTAINER_IMG) $(IMAGE_TARGET_DIR) $(IMAGE_TARGETS) +$(OUTPUT_PDF): $(ADOC_TOP_SRC) $(ADOC_PARTS_SRC) $(ADOC_EXTRA_DEPS) $(CONTAINER_IMG) $(IMAGE_TARGET_DIR) $(IMAGE_TARGETS) $(REFS_TABLE_FILE) mkdir -p $(OUTPUT_DIR) - $(CONTAINER_IMG) -v -a attribute-missing=warn --failure-level=WARN -r asciidoctor-pdf -r asciidoctor-diagram -b pdf -o $@ $< + apptainer exec $(CONTAINER_IMG) ruby render.rb $< $@ pdf $(REFS_TABLE_FILE) -$(OUTPUT_HTML): $(ADOC_TOP_SRC) $(ADOC_PARTS_SRC) $(ADOC_EXTRA_DEPS) $(CONTAINER_IMG) $(IMAGE_TARGET_DIR) $(IMAGE_TARGETS) +$(OUTPUT_HTML): $(ADOC_TOP_SRC) $(ADOC_PARTS_SRC) $(ADOC_EXTRA_DEPS) $(CONTAINER_IMG) $(IMAGE_TARGET_DIR) $(IMAGE_TARGETS) $(REFS_TABLE_FILE) mkdir -p $(OUTPUT_DIR) - $(CONTAINER_IMG) -v -a attribute-missing=warn --failure-level=WARN -r asciidoctor-diagram -b html5 -o $@ $< + apptainer exec $(CONTAINER_IMG) ruby render.rb $< $@ html5 $(REFS_TABLE_FILE) $(IMAGE_TARGET_DIR): mkdir -p $@ diff --git a/parts/cap-man-insn.adoc b/parts/cap-man-insn.adoc index eadbc6c..3f99b84 100644 --- a/parts/cap-man-insn.adoc +++ b/parts/cap-man-insn.adoc @@ -15,6 +15,8 @@ other instructions. Capabilities can be moved between registers with the MOVC instruction. +github_ref:MOVC[Sail definition] + .MOVC instruction format [wavedrom,,svg] .... @@ -53,6 +55,8 @@ capability by a given amount (offset). ==== CINCOFFSET +github_ref:CINCOFFSET[Sail definition] + .CINCOFFSET instruction format [wavedrom,,svg] .... @@ -86,6 +90,8 @@ capability by a given amount (offset). ==== CINCOFFSETIMM +github_ref:CINCOFFSETIMM[Sail definition] + .CINCOFFSETIMM instruction format [wavedrom,,svg] .... @@ -119,6 +125,8 @@ capability by a given amount (offset). The `cursor` field of a capability can also be directly set with the SCC instruction. +github_ref:SCC[Sail definition] + .SCC instruction format [wavedrom,,svg] .... @@ -155,6 +163,8 @@ The `cursor` field of a capability can also be directly set with the SCC instruc The LCC instruction is used to read a field from a capability. +github_ref:LCC[Sail definition] + .LCC instruction format [wavedrom,,svg] .... @@ -209,6 +219,8 @@ according to the <>. The bounds (`base` and `end` fields) of a capability can be shrunk with the SHRINK instruction. +github_ref:SHRINK[Sail definition] + .SHRINK instruction format [wavedrom,,svg] .... @@ -251,6 +263,8 @@ The SPLIT instruction can split a capability into two by splitting the bounds. It attempts to split the capability `x[rs1]` into two capabilities, one with bounds `[x[rs1].base, x[rs2])` and the other with bounds `[x[rs2], x[rs1].end)`. +github_ref:SPLIT[Sail definition] + .SPLIT instruction format [wavedrom,,svg] .... @@ -294,6 +308,8 @@ one with bounds `[x[rs1].base, x[rs2])` and the other with bounds `[x[rs2], x[rs The TIGHTEN instruction tightens the permissions (`perms` field) of a capability. +github_ref:TIGHTEN[Sail link] + .TIGHTEN instruction format [wavedrom,,svg] .... @@ -337,6 +353,8 @@ Instead, it is changed as the side effect of certain semantically significant op The DELIN instruction delinearises a linear capability. +github_ref:DELIN[Sail link] + .DELIN instruction format [wavedrom,,svg] .... @@ -371,6 +389,9 @@ The DELIN instruction delinearises a linear capability. The INIT instruction transforms an uninitialised capability into a linear capability after its associated memory region has been fully initialised (written with new data). +github_ref:DELIN[Sail link] + + .INIT instruction format [wavedrom,,svg] .... @@ -409,6 +430,9 @@ after its associated memory region has been fully initialised (written with new The SEAL instruction seals a linear capability. +github_ref:SEAL[Sail link] + + .SEAL instruction format [wavedrom,,svg] .... @@ -449,6 +473,8 @@ The SEAL instruction seals a linear capability. The DROP instruction invalidates a capability. +github_ref:DROP[Sail link] + .DROP instruction format [wavedrom,,svg] .... @@ -484,6 +510,8 @@ The DROP instruction invalidates a capability. The MREV instruction creates a revocation capability. +github_ref:MREV[Sail link] + .MREV instruction format [wavedrom,,svg] .... @@ -520,6 +548,8 @@ The MREV instruction creates a revocation capability. The REVOKE instruction revokes a capability. +github_ref:REVOKE[Sail link] + .REVOKE instruction format [wavedrom,,svg] .... diff --git a/parts/ctrl-flow-insn.adoc b/parts/ctrl-flow-insn.adoc index ade7c17..2f9d6a2 100644 --- a/parts/ctrl-flow-insn.adoc +++ b/parts/ctrl-flow-insn.adoc @@ -11,6 +11,8 @@ in a unconditional or conditional manner. [#jmp-cap] === CJALR +github_ref:CJALR[Sail definition] + .CJALR instruction format [wavedrom,,svg] .... @@ -44,6 +46,8 @@ in a unconditional or conditional manner. [#branch-cap] === CBNZ +github_ref:CBNZ[Sail definition] + .CBNZ instruction format [wavedrom,,svg] .... @@ -85,6 +89,8 @@ The mechanism is provided by the CALL and RETURN instructions. === CALL +github_ref:CALL[Sail definition] + The CALL instruction is used to call a sealed capability, i.e., to switch to another _domain_. .CALL instruction format @@ -127,6 +133,8 @@ and `cra.async` to `0` (synchronous). === RETURN +github_ref:RETURN[Sail definition] + .RETURN instruction format [wavedrom,,svg] .... @@ -202,6 +210,8 @@ image::trans-sync.svg[trans-sync] [#world-enter] === CAPENTER +github_ref:CAPENTER[Sail definition] + The CAPENTER instruction causes an entry into the secure world from the normal world. And it is only available in the normal world. @@ -272,6 +282,8 @@ the CPU core exits from the secure world synchronously or asynchronously. [#world-exit] === CAPEXIT +github_ref:CAPEXIT[Sail definition] + The CAPEXIT instruction causes an exit from the secure world into the normal world. It is only available in the secure world and can only be used with an exit capability. diff --git a/parts/ctrl-status-insn.adoc b/parts/ctrl-status-insn.adoc index 3e0aa32..744698d 100644 --- a/parts/ctrl-status-insn.adoc +++ b/parts/ctrl-status-insn.adoc @@ -6,6 +6,8 @@ The CCSRRW instruction is used to read and write specified _<>_ (CCSRs). +github_ref:CCSRRW[Sail definition] + .CCSRRW instruction format [wavedrom,,svg] .... diff --git a/parts/insn-list.adoc b/parts/insn-list.adoc index a5649e6..38a5567 100644 --- a/parts/insn-list.adoc +++ b/parts/insn-list.adoc @@ -20,52 +20,52 @@ include::ri-type-format.adoc[] .Capability manipulation instructions [%header%autowidth.stretch] |=== -|Mnemonic |Format |Func3 |Func7 | rs1 | rs2 | rd | imm [4:0] | imm[11:0] | World -|<> |R |`001` |`0000000` | C | - | - | - | - | * -|<> |R |`001` |`0000001` | I | I | C | - | - | * -|<> |RI |`001` |`0000010` | C | - | C | Z | - | * -|<> |R |`001` |`0000011` | - | - | C | - | - | * -|<> |RI |`001` |`0000100` | C | - | I | Z | - | * -|<> |R |`001` |`0000101` | C | I | C | - | - | * -|<> |R |`001` |`0000110` | C | I | C | - | - | * -|<> |R |`001` |`0000111` | C | - | C | - | - | * -|<> |R |`001` |`0001000` | C | - | C | - | - | * -|<> |R |`001` |`0001001` | C | I | C | - | - | * -|<> |R |`001` |`0001010` | C | - | C | - | - | * -|<> |R |`001` |`0001011` | C | - | - | - | - | * -|<> |R |`001` |`0001100` | C | I | C | - | - | * -|<> |I |`010` | - | C | - | C | - | S | * +|Mnemonic |Sail model |Format |Func3 |Func7 | rs1 | rs2 | rd | imm [4:0] | imm[11:0] | World +|<> |github_ref:REVOKE[link] |R |`001` |`0000000` | C | - | - | - | - | * +|<> |github_ref:SHRINK[link] |R |`001` |`0000001` | I | I | C | - | - | * +|<> |github_ref:TIGHTEN[link] |RI |`001` |`0000010` | C | - | C | Z | - | * +|<> |github_ref:DELIN[link] |R |`001` |`0000011` | - | - | C | - | - | * +|<> |github_ref:LCC[link] |RI |`001` |`0000100` | C | - | I | Z | - | * +|<> |github_ref:SCC[link] |R |`001` |`0000101` | C | I | C | - | - | * +|<> |github_ref:SPLIT[link] |R |`001` |`0000110` | C | I | C | - | - | * +|<> |github_ref:SEAL[link] |R |`001` |`0000111` | C | - | C | - | - | * +|<> |github_ref:MREV[link] |R |`001` |`0001000` | C | - | C | - | - | * +|<> |github_ref:INIT[link] |R |`001` |`0001001` | C | I | C | - | - | * +|<> |github_ref:MOVC[link] |R |`001` |`0001010` | C | - | C | - | - | * +|<> |github_ref:DROP[link] |R |`001` |`0001011` | C | - | - | - | - | * +|<> |github_ref:CINCOFFSET[link] |R |`001` |`0001100` | C | I | C | - | - | * +|<> |github_ref:CINCOFFSETIMM[link] |I |`010` | - | C | - | C | - | S | * |=== .Memory access instructions [%header%autowidth.stretch] |=== -|Mnemonic |Format |`emode` |Func3 |Func7 | rs1 | rs2 | rd | imm[11:0] | World -|<> |I |`0` |`011` | - | I | - | C | S | N -| |I |`1` |`011` | - | C | - | C | S | N -| |I |- |`011` | - | C | - | C | S | S -|<> |S |`0` |`100` | - | I | C | - | S | N -| |S |`1` |`100` | - | C | C | - | S | N -| |S |- |`100` | - | C | C | - | S | S +|Mnemonic |Sail model |Format |`emode` |Func3 |Func7 | rs1 | rs2 | rd | imm[11:0] | World +|<> |github_ref:LDC[link] |I |`0` |`011` | - | I | - | C | S | N +| | |I |`1` |`011` | - | C | - | C | S | N +| | |I |- |`011` | - | C | - | C | S | S +|<> |github_ref:STC[link] |S |`0` |`100` | - | I | C | - | S | N +| | |S |`1` |`100` | - | C | C | - | S | N +| | |S |- |`100` | - | C | C | - | S | S |=== .Control flow instructions [%header%autowidth.stretch] |=== -|Mnemonic |Format |Func3 |Func7 | rs1 | rs2 | rd | imm[11:0] | World -|<> |R |`001` |`0100000` | C | - | C | - | S -|<> |R |`001` |`0100001` | C | I | - | - | S -|<> |I |`101` |- | C | - | C | S | S -|<> |I |`110` |- | I | - | C | S | S -|<> |R |`001` |`0100010` | C | - | I | - | N -|<> |R |`001` |`0100011` | C | I | - | - | S +|Mnemonic |Sail model |Format |Func3 |Func7 | rs1 | rs2 | rd | imm[11:0] | World +|<> |github_ref:CALL[link] |R |`001` |`0100000` | C | - | C | - | S +|<> |github_ref:RETURN[link] |R |`001` |`0100001` | C | I | - | - | S +|<> |github_ref:CJALR[link] |I |`101` |- | C | - | C | S | S +|<> |github_ref:CBNZ[link] |I |`110` |- | I | - | C | S | S +|<> |github_ref:CAPENTER[link] |R |`001` |`0100010` | C | - | I | - | N +|<> |github_ref:CAPEXIT[link] |R |`001` |`0100011` | C | I | - | - | S |=== .Control and status instructions [%header%autowidth.stretch] |=== -|Mnemonic |Format |Func3 |Func7 | rs1 | rs2 | rd | imm[11:0] | World -|<> |I |`111` | - | C | - | C | Z | * +|Mnemonic |Sail model |Format |Func3 |Func7 | rs1 | rs2 | rd | imm[11:0] | World +|<> |github_ref:CCSRRW[link] |I |`111` | - | C | - | C | Z | * |=== == Extended {base_isa_name} Memory Access Instructions diff --git a/parts/mem-access-insn.adoc b/parts/mem-access-insn.adoc index a8112da..4aac4a9 100644 --- a/parts/mem-access-insn.adoc +++ b/parts/mem-access-insn.adoc @@ -7,6 +7,8 @@ [#load-cap] == Load Capabilities +github_ref:LDC[Sail definition] + The LDC instruction loads a capability from the memory. === Secure world or normal world capability encoding mode @@ -105,6 +107,8 @@ write `cnull` to the memory location `[int + imm, int + imm + CLENBYTES)`. [#store-cap] == Store Capabilities +github_ref:STC[Sail definition] + The STC instruction stores a capability to the memory. === Secure world or normal world capability encoding mode diff --git a/refs/sail.txt b/refs/sail.txt new file mode 100644 index 0000000..10b498b --- /dev/null +++ b/refs/sail.txt @@ -0,0 +1,40 @@ +project-starch/capstone-sail 9893cfa773be21dc0b733b675cfe4a61cb0c4a6c +REVOKE model/riscv_insts_capstone_cap.sail 5 +SHRINK model/riscv_insts_capstone_cap.sail 37 +TIGHTEN model/riscv_insts_capstone_cap.sail 86 +DELIN model/riscv_insts_capstone_cap.sail 128 +LCC model/riscv_insts_capstone_cap.sail 159 +SCC model/riscv_insts_capstone_cap.sail 193 +SPLIT model/riscv_insts_capstone_cap.sail 226 +SEAL model/riscv_insts_capstone_cap.sail 283 +MREV model/riscv_insts_capstone_cap.sail 327 +INIT model/riscv_insts_capstone_cap.sail 374 +MOVC model/riscv_insts_capstone_cap.sail 412 +DROP model/riscv_insts_capstone_cap.sail 440 +CINCOFFSET model/riscv_insts_capstone_cap.sail 465 +CINCOFFSETIMM model/riscv_insts_capstone_cap.sail 499 +CALL model/riscv_insts_capstone_ctrflow.sail 7 +RETURN model/riscv_insts_capstone_ctrflow.sail 67 +CJALR model/riscv_insts_capstone_ctrflow.sail 200 +CBNZ model/riscv_insts_capstone_ctrflow.sail 238 +CAPENTER model/riscv_insts_capstone_ctrflow.sail 270 +CAPEXIT model/riscv_insts_capstone_ctrflow.sail 382 +CCSRRW model/riscv_insts_capstone_ctrstatus.sail 5 +QUERY model/riscv_insts_capstone_debug.sail 11 +RCUPDATE model/riscv_insts_capstone_debug.sail 37 +ALLOC model/riscv_insts_capstone_debug.sail 63 +REV model/riscv_insts_capstone_debug.sail 97 +CAPCREATE model/riscv_insts_capstone_debug.sail 118 +CAPTYPE model/riscv_insts_capstone_debug.sail 131 +CAPNODE model/riscv_insts_capstone_debug.sail 156 +CAPPERM model/riscv_insts_capstone_debug.sail 180 +CAPBOUND model/riscv_insts_capstone_debug.sail 204 +CAPPRINT model/riscv_insts_capstone_debug.sail 228 +TAGSET model/riscv_insts_capstone_debug.sail 241 +TAGGET model/riscv_insts_capstone_debug.sail 264 +SETWORLD model/riscv_insts_capstone_debug.sail 288 +ONPARTITION model/riscv_insts_capstone_debug.sail 319 +SETEH model/riscv_insts_capstone_debug.sail 341 +ONNORMALEH model/riscv_insts_capstone_debug.sail 363 +LDC model/riscv_insts_capstone_mem.sail 5 +STC model/riscv_insts_capstone_mem.sail 93 diff --git a/render.rb b/render.rb new file mode 100644 index 0000000..7f35bcb --- /dev/null +++ b/render.rb @@ -0,0 +1,59 @@ +require "asciidoctor" +require "asciidoctor-pdf" +require "asciidoctor-diagram" + +adoc_filename = ARGV[0] +output_filename = ARGV[1] +output_format = ARGV[2] +ref_filename = ARGV[3] + +$refs = Hash.new +$repo = '' +$revision = '' + +if ref_filename + # load the sail reference table + fileObj = File.new(ref_filename, "r") + first_line = true + while (line = fileObj.gets) + if first_line + first_line = false + # this is the revision hash + $repo, $revision = line.strip().split(' ', 2) + else + label, file_name, line_no = line.strip().split(' ', 3) + $refs[label] = [file_name, line_no] + end + end + fileObj.close +end + +class GithubRefInlineMacro < Asciidoctor::Extensions::InlineMacroProcessor + use_dsl + + named :github_ref + name_positional_attributes 'text' + + def process parent, target, attrs + doc = parent.document + text = attrs['text'] + label = target + + if !$refs.has_key?(label) + puts "ERROR: label \"#{label}\" not found in reference table" + exit 1 + end + target = "https://github.com/#{$repo}/blob/#{$revision}/#{$refs[label][0]}#L#{$refs[label][1]}" + doc.register :links, target + node = create_anchor parent, text, type: :link, target: target + + create_inline parent, :quoted, %(#{node.convert}) + end +end + +Asciidoctor::Extensions.register do + inline_macro GithubRefInlineMacro +end + + +Asciidoctor.convert_file adoc_filename, safe: :safe, backend: output_format, to_file: output_filename