@@ -135,7 +135,133 @@ Capability<void> CIncAddr_test(Capability<void> cap, ds::xoroshiro::P64R32& prng
135135 " cmove %[out_cap], ca0\n "
136136 : [out_cap] " =C" (right_type_cap)
137137 : [cap] " C" (right_type_cap), [rand] " r" (rand_val)
138- : " ca0" , " a2" , " a3" );
138+ : " ca0" , " a2" , " a3" , " a4" );
139+ out = right_type_cap;
140+ return out;
141+ }
142+
143+ // Testing the CSetAddr instruction
144+ Capability<void > CSetAddr_test (Capability<void > cap, ds::xoroshiro::P64R32& prng, Capability<void > root, UartPtr uart) {
145+ uint32_t rand_val = prng ();
146+ void * right_type_cap = cap.get ();
147+ Capability<void > out = root.cast <void >();
148+ asm volatile (
149+ " cmove ca0, %[cap]\n " // ca0 = cap
150+ " mv a2, %[rand]\n " // a2 = rand
151+ " cgetbase a3, ca0\n " // a3 = ca0.base
152+ " cgettop a4, ca0\n " // a4 = ca0.top
153+ " sub a3, a4, a3\n " // a3 = ca0.top - ca0.base
154+ " beqz a3, 1f\n "
155+ " remu a2, a2, a3\n " // a2 = a2 % a4
156+ " cgetbase a3, ca0\n " // a3 = ca0.base()
157+ " add a2, a2, a3\n " // a2 = ca0.base() + ( rand % ca0.length() )
158+ " csetaddr ca0, ca0, a2\n "
159+ " 1:\n "
160+ " cmove %[out_cap], ca0\n "
161+ : [out_cap] " =C" (right_type_cap)
162+ : [cap] " C" (right_type_cap), [rand] " r" (rand_val)
163+ : " ca0" , " a2" , " a3" , " a4" );
164+ out = right_type_cap;
165+ return out;
166+ }
167+
168+ // Testing the CIncAddrImm instruction
169+ Capability<void > CIncAddrImm_test (Capability<void > cap, ds::xoroshiro::P64R32& prng, Capability<void > root,
170+ UartPtr uart) {
171+ void * right_type_cap = cap.get ();
172+ Capability<void > out = root.cast <void >();
173+ asm volatile (
174+ // Loading in external values
175+ " cmove ca0, %[cap]\n " // ca0 = cap
176+
177+ // Main body
178+ " li a2, %[imm]\n " // a2 = imm
179+ " cgetaddr a3, ca0\n " // a3 = cap.addr
180+ " add a3, a3, a2\n " // a3 = cap.addr + imm
181+ " cgettop a4, ca0\n " // a4 = cap.top
182+ " bgeu a3, a4, 1f\n " // if cap.addr + imm > top: goto end
183+ " cgetbase a4, ca0\n " // a4 = cap.base
184+ " bgtu a4, a3, 1f\n " // if cap.base > cap.addr + imm: goto end
185+ " cincoffsetimm ca0, ca0, %[imm]\n "
186+ // Loading out register values
187+ " 1:\n "
188+ " cmove %[out_cap], ca0\n "
189+ : [out_cap] " =C" (right_type_cap)
190+ : [cap] " C" (right_type_cap), [imm] " i" (IMMEDIATE)
191+ : " ca0" , " a2" , " a3" , " a4" );
192+ out = right_type_cap;
193+ return out;
194+ }
195+
196+ Capability<void > CIncAddr_representable_test (Capability<void > cap, ds::xoroshiro::P64R32& prng, Capability<void > root,
197+ UartPtr uart) {
198+ uint32_t rand_val = prng ();
199+ void * right_type_cap = cap.get ();
200+ uint32_t clz = __builtin_clz (cap.length ());
201+
202+ Capability<void > out = root.cast <void >();
203+ asm volatile (
204+ " cmove ca0, %[cap]\n " // ca0 = cap
205+ " mv a2, %[rand]\n " // a2 = rand
206+ " cgetbase a4, ca0\n " // a4 = ca0.base
207+
208+ " mv t0, %[clz]\n " // t0 = clz(cap.length)
209+ // t0 = MIN(t0, 23)
210+ " li a3, 23\n "
211+ " blt t0, a3, 1f\n "
212+ " li t0, 23\n "
213+ " 1:"
214+ " sub t0, a3, t0\n " // e = 23 - min(clz(cap.length), 23)
215+
216+ " li a3, 1\n "
217+ " slli a3, a3, 9\n " // a3 = 2^9
218+ " sll a3, a3, t0\n "
219+ " remu a2, a2, a3\n " // a2 = rand % (cap.top - cap.base)
220+ " cgetaddr a3, ca0\n " // a3 = cap.addr
221+ " sub a3, a3, a4\n " // a3 = cap.addr - cap.base
222+ " sub a2, a2, a3\n " // a2 = rand % (2^(e+9)) - (cap.addr - cap.base)
223+ // a2 + cap.addr = cap.base + (rand % (2^(e+9)))
224+ " cincoffset ca0, ca0, a2\n "
225+ " cmove %[out_cap], ca0\n "
226+ : [out_cap] " =C" (right_type_cap)
227+ : [cap] " C" (right_type_cap), [rand] " r" (rand_val), [clz] " r" (clz)
228+ : " ca0" , " a2" , " a3" , " a4" , " t0" );
229+ out = right_type_cap;
230+ return out;
231+ }
232+
233+ Capability<void > CSetAddr_representable_test (Capability<void > cap, ds::xoroshiro::P64R32& prng, Capability<void > root,
234+ UartPtr uart) {
235+ uint32_t rand_val = prng ();
236+ void * right_type_cap = cap.get ();
237+ uint32_t clz = __builtin_clz (cap.length ());
238+
239+ Capability<void > out = root.cast <void >();
240+ asm volatile (
241+ " cmove ca0, %[cap]\n " // ca0 = cap
242+ " mv a2, %[rand]\n " // a2 = rand
243+ " cgetbase a4, ca0\n " // a4 = ca0.base
244+
245+ " mv t0, %[clz]\n " // t0 = clz(cap.length)
246+ // t0 = MIN(t0, 23)
247+ " li a3, 23\n "
248+ " blt t0, a3, 1f\n "
249+ " li t0, 23\n "
250+ " 1:"
251+ " sub t0, a3, t0\n " // e = 23 - min(clz(cap.length), 23)
252+
253+ " li a3, 1\n "
254+ " slli a3, a3, 9\n " // a3 = 2^9
255+ " sll a3, a3, t0\n "
256+ " remu a2, a2, a3\n " // a2 = rand % (2^(e+9))
257+
258+ " cgetbase a4, ca0\n "
259+ " add a2, a2, a4\n "
260+ " csetaddr ca0, ca0, a2\n "
261+ " cmove %[out_cap], ca0\n "
262+ : [out_cap] " =C" (right_type_cap)
263+ : [cap] " C" (right_type_cap), [rand] " r" (rand_val), [clz] " r" (clz)
264+ : " ca0" , " a2" , " a3" , " a4" , " t0" );
139265 out = right_type_cap;
140266 return out;
141267}
@@ -214,6 +340,17 @@ Capability<void> CSetBoundsExact_test(Capability<void> cap, ds::xoroshiro::P64R3
214340 // "mv a2, t1\n" //a2 = 24
215341 // "1:\n"
216342 " mv %[test_v], a2\n "
343+
344+ " li t0, 14\n "
345+ " li t1, 24\n "
346+ " blt a2, t0, 4f\n " // if ctz(addr) < 14 then e = ctz(addr) so skip rest
347+ " bge a2, t1, 3f\n "
348+ " li a2, 14\n "
349+ " j 4f\n "
350+ " 3:\n "
351+ " li a2, 24\n "
352+ " 4:\n "
353+
217354 " li t0, 1\n " // t0 = 1
218355 " sll t0, t0, a2\n " // t0 = 1 << a2
219356 " addi t0, t0, -1\n " // t0 = (1 << a2) - 1
@@ -282,31 +419,6 @@ Capability<void> CSetBoundsRoundDown_test(Capability<void> cap, ds::xoroshiro::P
282419 return out;
283420}
284421
285- // Testing the CSetAddr instruction
286- Capability<void > CSetAddr_test (Capability<void > cap, ds::xoroshiro::P64R32& prng, Capability<void > root, UartPtr uart) {
287- uint32_t rand_val = prng ();
288- void * right_type_cap = cap.get ();
289- Capability<void > out = root.cast <void >();
290- asm volatile (
291- " cmove ca0, %[cap]\n " // ca0 = cap
292- " mv a2, %[rand]\n " // a2 = rand
293- " cgetbase a3, ca0\n " // a3 = ca0.base
294- " cgettop a4, ca0\n " // a4 = ca0.top
295- " sub a3, a4, a3\n " // a3 = ca0.top - ca0.base
296- " beqz a3, 1f\n "
297- " remu a2, a2, a3\n " // a2 = a2 % a4
298- " cgetbase a3, ca0\n " // a3 = ca0.base()
299- " add a2, a2, a3\n " // a2 = ca0.base() + ( rand % ca0.length() )
300- " csetaddr ca0, ca0, a2\n "
301- " 1:\n "
302- " cmove %[out_cap], ca0\n "
303- : [out_cap] " =C" (right_type_cap)
304- : [cap] " C" (right_type_cap), [rand] " r" (rand_val)
305- : " ca0" , " a2" , " a3" , " a4" );
306- out = right_type_cap;
307- return out;
308- }
309-
310422// Testing the CSeal instruction
311423Capability<void > CSeal_test (Capability<void > cap, Capability<void > seal_cap, ds::xoroshiro::P64R32& prng,
312424 Capability<void > root, UartPtr uart) {
@@ -333,7 +445,7 @@ Capability<void> CSeal_test(Capability<void> cap, Capability<void> seal_cap, ds:
333445 " beqz a3, 1f\n "
334446
335447 // The execute permission is set. The address of ca1 should be set between 1 and 7
336- " li t0, 6 \n "
448+ " li t0, 7 \n "
337449 " remu a2, a2, t0\n "
338450 " addi a2, a2, 1\n "
339451
@@ -495,7 +607,7 @@ Capability<void> CSetBoundsImm_test(Capability<void> cap, ds::xoroshiro::P64R32&
495607 // Main body
496608 " li a2, %[imm]\n " // a2 = imm
497609 " cgetaddr a3, ca0\n " // a3 = cap.addr
498- " add a2, a3, a2\n " // a3 = cap.addr + imm
610+ " add a2, a3, a2\n " // a2 = cap.addr + imm
499611 " cgettop a4, ca0\n " // a4 = cap.top
500612 " bgeu a2, a4, 1f\n " // if cap.addr + imm > top: goto end
501613 " cgetbase a4, ca0\n " // a4 = cap.base
@@ -512,34 +624,6 @@ Capability<void> CSetBoundsImm_test(Capability<void> cap, ds::xoroshiro::P64R32&
512624 return out;
513625}
514626
515- // Testing the CIncAddrImm instruction
516- Capability<void > CIncAddrImm_test (Capability<void > cap, ds::xoroshiro::P64R32& prng, Capability<void > root,
517- UartPtr uart) {
518- void * right_type_cap = cap.get ();
519- Capability<void > out = root.cast <void >();
520- asm volatile (
521- // Loading in external values
522- " cmove ca0, %[cap]\n " // ca0 = cap
523-
524- // Main body
525- " li a2, %[imm]\n " // a2 = imm
526- " cgetaddr a3, ca0\n " // a3 = cap.addr
527- " add a3, a3, a2\n " // a3 = cap.addr + imm
528- " cgettop a4, ca0\n " // a4 = cap.top
529- " bgeu a3, a4, 1f\n " // if cap.addr + imm > top: goto end
530- " cgetbase a4, ca0\n " // a4 = cap.base
531- " bgtu a4, a3, 1f\n " // if cap.base > cap.addr + imm: goto end
532- " cincoffsetimm ca0, ca0, %[imm]\n "
533- // Loading out register values
534- " 1:\n "
535- " cmove %[out_cap], ca0\n "
536- : [out_cap] " =C" (right_type_cap)
537- : [cap] " C" (right_type_cap), [imm] " i" (IMMEDIATE)
538- : " ca0" , " a2" , " a3" , " a4" );
539- out = right_type_cap;
540- return out;
541- }
542-
543627// Default test which contains all the tests
544628Capability<void > test_all (Capability<void > cap, ds::xoroshiro::P64R32& prng, Capability<void > un_seal_cap,
545629 Capability<void > root, UartPtr uart) {
@@ -553,6 +637,8 @@ Capability<void> test_all(Capability<void> cap, ds::xoroshiro::P64R32& prng, Cap
553637 cap = CAndPerm_test (cap, prng, root, uart);
554638 cap = CSetBoundsImm_test (cap, prng, root, uart);
555639 cap = CIncAddrImm_test (cap, prng, root, uart);
640+ cap = CIncAddr_representable_test (cap, prng, root, uart);
641+ cap = CSetAddr_representable_test (cap, prng, root, uart);
556642 return cap;
557643}
558644
@@ -609,6 +695,7 @@ extern "C" void entry_point(void* rwRoot, void* sealRoot, void* exRoot) {
609695 out_cap = test_all (random_unsealed_cap, prng, seal_root, root, uart);
610696 if (!out_cap.is_valid ()) {
611697 write_str (uart, " Test failed\n " );
698+ print_capability (out_cap, uart);
612699 num_fails++;
613700 break ;
614701 }
0 commit comments