SEAL (immediate)

Seal capability (immediate) seals a capability by setting the ObjectType of that capability to nonzero, and writes the result to the destination Capability register. An operand of rb seals for use with a register based branch, lpb for a load pair and branch and lb for a load and branch.

31	30	29	28	27	26	25	24	23	22	21	20	19	18	17	16	15	14	13	12	11	10	9	8	7	6	5	4	3	2	1	0
1	1	0	0	0	0	1	0	1	1	0	0	0	0	1	1	0	form		1	0	0	Cn					Cd

SEAL <Cd>, <Cn>, <form>

integer d = UInt(Cd); integer n = UInt(Cn); bits(64) f = ZeroExtend(form,64);

Assembler Symbols

<Cd>	Is the capability name of the destination register, encoded in the "Cd" field.

<Cn>	Is the capability name of the first source register, encoded in the "Cn" field.

<form>

Is the form specifier, encoded in form:

form	<form>
00	RESERVED
01	rb
10	lpb
11	lb

Operation

if f == 0 then UNDEFINED; CheckCapabilitiesEnabled(); Capability c = CapSetObjectType(C[n], f); if CapIsTagSet(C[n]) && !CapIsSealed(C[n]) then C[d] = c; else C[d] = CapWithTagClear(c);

Internal version only: isa v32.13, AdvSIMD v29.04, pseudocode morello-2022-01_rc2, capabilities morello-2022-01_rc2 ; Build timestamp: 2022-01-11T11:23