@@ -84,23 +84,23 @@ the process). To do this, we need a way to serialize information about a a list
8484of types. To start, lets assign numbers to each type (DNE means this type
8585doesn't exist yet):
8686
87- | ID | Rust Type | C Type |
88- | -------- | ------------------------- | ---------------------------------- |
89- | ` 0b0001 ` | ` ErrorCode ` | Error code ( DNE) |
90- | ` 0b0010 ` | ` u32 ` | ` uint32_t ` |
91- | ` 0b0011 ` | ` i32 ` | ` int32_t ` |
92- | ` 0b0100 ` | ` usize ` | ` size_t ` |
93- | ` 0b0101 ` | ` isize ` | ` ptrdiff_t ` |
94- | ` 0b0110 ` | ` u64 ` | ` uint64_t ` |
95- | ` 0b0111 ` | ` i64 ` | ` int64_t ` |
96- | ` 0b1000 ` | ` f32 ` | ` float ` |
97- | ` 0b1001 ` | ` f64 ` | ` double ` |
98- | ` 0b1010 ` | ` bool ` | ` bool ` |
99- | ` 0b1011 ` | Upcall fn pointer | Upcall fn pointer |
100- | ` 0b1100 ` | ` *mut T ` where ` T: Sized ` | ` T* ` |
101- | ` 0b1101 ` | Non-pointer CHERI capability ( DNE) | Non-pointer CHERI capability ( DNE) |
102- | ` 0b1110 ` | * Reserved for future use* | * Reserved for future use * |
103- | ` 0b1111 ` | Register | Register (DNE) |
87+ | ID | Description | Kernel Type | ` libtock-c ` Type | ` libtock-rs ` Type |
88+ | -------- | ---------------------------- | --------------- | ---------------- | ------------------------- |
89+ | ` 0b0001 ` | Error code | ` ErrorCode ` | DNE | ` ErrorCode ` |
90+ | ` 0b0010 ` | ` u32 ` | ` u32 ` | ` uint32_t ` | ` u32 ` |
91+ | ` 0b0011 ` | ` i32 ` | ` i32 ` | ` int32_t ` | ` i32 ` |
92+ | ` 0b0100 ` | ` usize ` | ` usize ` | ` size_t ` | ` usize ` |
93+ | ` 0b0101 ` | ` isize ` | ` isize ` | ` ptrdiff_t ` | ` isize ` |
94+ | ` 0b0110 ` | ` u64 ` | ` u64 ` | ` uint64_t ` | ` u64 ` |
95+ | ` 0b0111 ` | ` i64 ` | ` i64 ` | ` int64_t ` | ` i64 ` |
96+ | ` 0b1000 ` | ` f32 ` | ` f32 ` | ` float ` | ` f32 ` |
97+ | ` 0b1001 ` | ` f64 ` | ` f64 ` | ` double ` | ` f64 ` |
98+ | ` 0b1010 ` | ` bool ` | ` bool ` | ` bool ` | ` bool ` |
99+ | ` 0b1011 ` | Upcall pointer | ` CapabilityPtr ` | ` UpcallFn ` | ` UpcallFn ` |
100+ | ` 0b1100 ` | Data pointer | ` CapabilityPtr ` | ` T* ` | ` *mut T ` where ` T: Sized ` |
101+ | ` 0b1101 ` | Non-pointer CHERI capability | DNE | DNE | DNE |
102+ | ` 0b1110 ` | * Reserved for future use* | - | - | - |
103+ | ` 0b1111 ` | Arbitrary register value | DNE | DNE | ` Register ` |
104104
105105We can describe a list of N types as a 4N bit integer by embedding the Nth type
106106ID in the Nth nibble of the integer. So:
@@ -131,9 +131,9 @@ This table indicates how many registers are needed for each type:
131131
132132| Type | 32 bit non-CHERI | 64 bit non-CHERI | 32 bit CHERI | 64 bit CHERI |
133133| ----------------- | ---------------- | ---------------- | ------------ | ------------ |
134- | ` u64 ` | 2 | 1 | 1? 2? | 1 |
135- | ` i64 ` | 2 | 1 | 1? 2? | 1 |
136- | ` f64 ` | 2 | 1 | 1? 2? | 1 |
134+ | ` u64 ` | 2 | 1 | 2 | 1 |
135+ | ` i64 ` | 2 | 1 | 2 | 1 |
136+ | ` f64 ` | 2 | 1 | 2 | 1 |
137137| CHERI capability | N/A | N/A | 1 | 1 |
138138| * Everything else* | 1 | 1 | 1 | 1 |
139139
0 commit comments