Skip to content

Commit

Permalink
#16 Inline macro github_ref added to support referencing source files…
Browse files Browse the repository at this point in the history
… on Github; Sail definitions added as permalinks to Sail repo
  • Loading branch information
jasonyu1996 committed Aug 25, 2023
1 parent 37aa6df commit 9c9e6f6
Show file tree
Hide file tree
Showing 8 changed files with 183 additions and 35 deletions.
9 changes: 5 additions & 4 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand All @@ -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 $@
Expand Down
30 changes: 30 additions & 0 deletions parts/cap-man-insn.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -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]
....
Expand Down Expand Up @@ -53,6 +55,8 @@ capability by a given amount (offset).

==== CINCOFFSET

github_ref:CINCOFFSET[Sail definition]

.CINCOFFSET instruction format
[wavedrom,,svg]
....
Expand Down Expand Up @@ -86,6 +90,8 @@ capability by a given amount (offset).

==== CINCOFFSETIMM

github_ref:CINCOFFSETIMM[Sail definition]

.CINCOFFSETIMM instruction format
[wavedrom,,svg]
....
Expand Down Expand Up @@ -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]
....
Expand Down Expand Up @@ -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]
....
Expand Down Expand Up @@ -209,6 +219,8 @@ according to the <<lcc-multiplex,LCC multiplexing table>>.

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]
....
Expand Down Expand Up @@ -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]
....
Expand Down Expand Up @@ -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]
....
Expand Down Expand Up @@ -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]
....
Expand Down Expand Up @@ -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]
....
Expand Down Expand Up @@ -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]
....
Expand Down Expand Up @@ -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]
....
Expand Down Expand Up @@ -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]
....
Expand Down Expand Up @@ -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]
....
Expand Down
12 changes: 12 additions & 0 deletions parts/ctrl-flow-insn.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,8 @@ in a unconditional or conditional manner.
[#jmp-cap]
=== CJALR

github_ref:CJALR[Sail definition]

.CJALR instruction format
[wavedrom,,svg]
....
Expand Down Expand Up @@ -44,6 +46,8 @@ in a unconditional or conditional manner.
[#branch-cap]
=== CBNZ

github_ref:CBNZ[Sail definition]

.CBNZ instruction format
[wavedrom,,svg]
....
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -127,6 +133,8 @@ and `cra.async` to `0` (synchronous).

=== RETURN

github_ref:RETURN[Sail definition]

.RETURN instruction format
[wavedrom,,svg]
....
Expand Down Expand Up @@ -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.

Expand Down Expand Up @@ -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.

Expand Down
2 changes: 2 additions & 0 deletions parts/ctrl-status-insn.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,8 @@
The CCSRRW instruction is used to read and write specified
_<<add-reg-list,capability control and status registers>>_ (CCSRs).

github_ref:CCSRRW[Sail definition]

.CCSRRW instruction format
[wavedrom,,svg]
....
Expand Down
62 changes: 31 additions & 31 deletions parts/insn-list.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -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
|<<rev-operation,REVOKE>> |R |`001` |`0000000` | C | - | - | - | - | *
|<<shrink,SHRINK>> |R |`001` |`0000001` | I | I | C | - | - | *
|<<tighten,TIGHTEN>> |RI |`001` |`0000010` | C | - | C | Z | - | *
|<<delin,DELIN>> |R |`001` |`0000011` | - | - | C | - | - | *
|<<field-query,LCC>> |RI |`001` |`0000100` | C | - | I | Z | - | *
|<<cursor-set,SCC>> |R |`001` |`0000101` | C | I | C | - | - | *
|<<split,SPLIT>> |R |`001` |`0000110` | C | I | C | - | - | *
|<<seal,SEAL>> |R |`001` |`0000111` | C | - | C | - | - | *
|<<revcap-creation,MREV>> |R |`001` |`0001000` | C | - | C | - | - | *
|<<init,INIT>> |R |`001` |`0001001` | C | I | C | - | - | *
|<<cap-mov,MOVC>> |R |`001` |`0001010` | C | - | C | - | - | *
|<<drop,DROP>> |R |`001` |`0001011` | C | - | - | - | - | *
|<<cursor-inc,CINCOFFSET>> |R |`001` |`0001100` | C | I | C | - | - | *
|<<cursor-inc,CINCOFFSETIMM>> |I |`010` | - | C | - | C | - | S | *
|Mnemonic |Sail model |Format |Func3 |Func7 | rs1 | rs2 | rd | imm [4:0] | imm[11:0] | World
|<<rev-operation,REVOKE>> |github_ref:REVOKE[link] |R |`001` |`0000000` | C | - | - | - | - | *
|<<shrink,SHRINK>> |github_ref:SHRINK[link] |R |`001` |`0000001` | I | I | C | - | - | *
|<<tighten,TIGHTEN>> |github_ref:TIGHTEN[link] |RI |`001` |`0000010` | C | - | C | Z | - | *
|<<delin,DELIN>> |github_ref:DELIN[link] |R |`001` |`0000011` | - | - | C | - | - | *
|<<field-query,LCC>> |github_ref:LCC[link] |RI |`001` |`0000100` | C | - | I | Z | - | *
|<<cursor-set,SCC>> |github_ref:SCC[link] |R |`001` |`0000101` | C | I | C | - | - | *
|<<split,SPLIT>> |github_ref:SPLIT[link] |R |`001` |`0000110` | C | I | C | - | - | *
|<<seal,SEAL>> |github_ref:SEAL[link] |R |`001` |`0000111` | C | - | C | - | - | *
|<<revcap-creation,MREV>> |github_ref:MREV[link] |R |`001` |`0001000` | C | - | C | - | - | *
|<<init,INIT>> |github_ref:INIT[link] |R |`001` |`0001001` | C | I | C | - | - | *
|<<cap-mov,MOVC>> |github_ref:MOVC[link] |R |`001` |`0001010` | C | - | C | - | - | *
|<<drop,DROP>> |github_ref:DROP[link] |R |`001` |`0001011` | C | - | - | - | - | *
|<<cursor-inc,CINCOFFSET>> |github_ref:CINCOFFSET[link] |R |`001` |`0001100` | C | I | C | - | - | *
|<<cursor-inc,CINCOFFSETIMM>> |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
|<<load-cap,LDC>> |I |`0` |`011` | - | I | - | C | S | N
| |I |`1` |`011` | - | C | - | C | S | N
| |I |- |`011` | - | C | - | C | S | S
|<<store-cap,STC>> |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
|<<load-cap,LDC>> |github_ref:LDC[link] |I |`0` |`011` | - | I | - | C | S | N
| | |I |`1` |`011` | - | C | - | C | S | N
| | |I |- |`011` | - | C | - | C | S | S
|<<store-cap,STC>> |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
|<<domain-cross,CALL>> |R |`001` |`0100000` | C | - | C | - | S
|<<domain-cross,RETURN>> |R |`001` |`0100001` | C | I | - | - | S
|<<jmp-cap,CJALR>> |I |`101` |- | C | - | C | S | S
|<<branch-cap,CBNZ>> |I |`110` |- | I | - | C | S | S
|<<world-enter,CAPENTER>> |R |`001` |`0100010` | C | - | I | - | N
|<<world-exit,CAPEXIT>> |R |`001` |`0100011` | C | I | - | - | S
|Mnemonic |Sail model |Format |Func3 |Func7 | rs1 | rs2 | rd | imm[11:0] | World
|<<domain-cross,CALL>> |github_ref:CALL[link] |R |`001` |`0100000` | C | - | C | - | S
|<<domain-cross,RETURN>> |github_ref:RETURN[link] |R |`001` |`0100001` | C | I | - | - | S
|<<jmp-cap,CJALR>> |github_ref:CJALR[link] |I |`101` |- | C | - | C | S | S
|<<branch-cap,CBNZ>> |github_ref:CBNZ[link] |I |`110` |- | I | - | C | S | S
|<<world-enter,CAPENTER>> |github_ref:CAPENTER[link] |R |`001` |`0100010` | C | - | I | - | N
|<<world-exit,CAPEXIT>> |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
|<<ctrl-status,CCSRRW>> |I |`111` | - | C | - | C | Z | *
|Mnemonic |Sail model |Format |Func3 |Func7 | rs1 | rs2 | rd | imm[11:0] | World
|<<ctrl-status,CCSRRW>> |github_ref:CCSRRW[link] |I |`111` | - | C | - | C | Z | *
|===

== Extended {base_isa_name} Memory Access Instructions
Expand Down
4 changes: 4 additions & 0 deletions parts/mem-access-insn.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
40 changes: 40 additions & 0 deletions refs/sail.txt
Original file line number Diff line number Diff line change
@@ -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
Loading

0 comments on commit 9c9e6f6

Please sign in to comment.