1/*
2 * Copyright 2017, Data61
3 * Commonwealth Scientific and Industrial Research Organisation (CSIRO)
4 * ABN 41 687 119 230.
5 *
6 * This software may be distributed and modified according to the terms of
7 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
8 * See "LICENSE_BSD2.txt" for details.
9 *
10 * @TAG(DATA61_BSD)
11 */
12
13#include <sel4/sel4.h>
14#include <sel4utils/arch/util.h>
15#include <sel4utils/helpers.h>
16#include <sel4runtime.h>
17
18#include <sel4test/test.h>
19#include <stdarg.h>
20#include <stdlib.h>
21#include <assert.h>
22
23#include <utils/util.h>
24#include <vka/capops.h>
25#include <vka/ipcbuffer.h>
26
27#include <sel4platsupport/timer.h>
28
29#include "helpers.h"
30#include "test.h"
31
32char __attribute__((aligned(16))) process_tls[1024 * 16];
33
34int check_zeroes(seL4_Word addr, seL4_Word size_bytes)
35{
36    test_assert_fatal(IS_ALIGNED(addr, sizeof(seL4_Word)));
37    test_assert_fatal(IS_ALIGNED(size_bytes, sizeof(seL4_Word)));
38    seL4_Word *p = (void *)addr;
39    seL4_Word size_words = size_bytes / sizeof(seL4_Word);
40    while (size_words--) {
41        if (*p++ != 0) {
42            ZF_LOGE("Found non-zero at position %ld: %lu\n", ((long)p) - (addr), (unsigned long)p[-1]);
43            return 0;
44        }
45    }
46    return 1;
47}
48
49/* Determine whether a given slot in the init thread's CSpace is empty by
50 * examining the error when moving a slot onto itself.
51 *
52 * Serves as == 0 comparator for caps.
53 */
54int is_slot_empty(env_t env, seL4_Word slot)
55{
56    int error;
57
58    error = cnode_move(env, slot, slot);
59
60    /* cnode_move first check if the destination is empty and raise
61     * seL4_DeleteFirst is it is not
62     * The is check if the source is empty and raise seL4_FailedLookup if it is
63     */
64    assert(error == seL4_DeleteFirst || error == seL4_FailedLookup);
65    return (error == seL4_FailedLookup);
66}
67
68seL4_Word get_free_slot(env_t env)
69{
70    seL4_CPtr slot;
71    UNUSED int error = vka_cspace_alloc(&env->vka, &slot);
72    assert(!error);
73    return slot;
74}
75
76int cnode_copy(env_t env, seL4_CPtr src, seL4_CPtr dest, seL4_CapRights_t rights)
77{
78    cspacepath_t src_path, dest_path;
79    vka_cspace_make_path(&env->vka, src, &src_path);
80    vka_cspace_make_path(&env->vka, dest, &dest_path);
81    return vka_cnode_copy(&dest_path, &src_path, rights);
82}
83
84int cnode_delete(env_t env, seL4_CPtr slot)
85{
86    cspacepath_t path;
87    vka_cspace_make_path(&env->vka, slot, &path);
88    return vka_cnode_delete(&path);
89}
90
91int cnode_mint(env_t env, seL4_CPtr src, seL4_CPtr dest, seL4_CapRights_t rights, seL4_Word badge)
92{
93    cspacepath_t src_path, dest_path;
94
95    vka_cspace_make_path(&env->vka, src, &src_path);
96    vka_cspace_make_path(&env->vka, dest, &dest_path);
97    return vka_cnode_mint(&dest_path, &src_path, rights, badge);
98}
99
100int cnode_move(env_t env, seL4_CPtr src, seL4_CPtr dest)
101{
102    cspacepath_t src_path, dest_path;
103
104    vka_cspace_make_path(&env->vka, src, &src_path);
105    vka_cspace_make_path(&env->vka, dest, &dest_path);
106    return vka_cnode_move(&dest_path, &src_path);
107}
108
109int cnode_mutate(env_t env, seL4_CPtr src, seL4_CPtr dest)
110{
111    cspacepath_t src_path, dest_path;
112
113    vka_cspace_make_path(&env->vka, src, &src_path);
114    vka_cspace_make_path(&env->vka, dest, &dest_path);
115    return vka_cnode_mutate(&dest_path, &src_path, seL4_NilData);
116}
117
118int cnode_cancelBadgedSends(env_t env, seL4_CPtr cap)
119{
120    cspacepath_t path;
121    vka_cspace_make_path(&env->vka, cap, &path);
122    return vka_cnode_cancelBadgedSends(&path);
123}
124
125int cnode_revoke(env_t env, seL4_CPtr cap)
126{
127    cspacepath_t path;
128    vka_cspace_make_path(&env->vka, cap, &path);
129    return vka_cnode_revoke(&path);
130}
131
132int cnode_rotate(env_t env, seL4_CPtr src, seL4_CPtr pivot, seL4_CPtr dest)
133{
134    cspacepath_t src_path, dest_path, pivot_path;
135
136    vka_cspace_make_path(&env->vka, src, &src_path);
137    vka_cspace_make_path(&env->vka, dest, &dest_path);
138    vka_cspace_make_path(&env->vka, pivot, &pivot_path);
139    return vka_cnode_rotate(&dest_path, seL4_NilData, &pivot_path, seL4_NilData, &src_path);
140}
141
142int cnode_savecaller(env_t env, seL4_CPtr cap)
143{
144    cspacepath_t path;
145    vka_cspace_make_path(&env->vka, cap, &path);
146#ifndef CONFIG_KERNEL_MCS
147    return vka_cnode_saveCaller(&path);
148#else
149    ZF_LOGF("Should not be called");
150    return 0;
151#endif
152}
153
154void set_cap_receive_path(env_t env, seL4_CPtr slot)
155{
156    cspacepath_t path;
157    vka_cspace_make_path(&env->vka, slot, &path);
158    return vka_set_cap_receive_path(&path);
159}
160
161int are_tcbs_distinct(seL4_CPtr tcb1, seL4_CPtr tcb2)
162{
163    seL4_UserContext regs;
164
165    /* Initialise regs to prevent compiler warning. */
166    int error = seL4_TCB_ReadRegisters(tcb1, 0, 0, 1, &regs);
167    if (error) {
168        return -1;
169    }
170
171    for (int i = 0; i < 2; ++i) {
172        sel4utils_set_instruction_pointer(&regs, i);
173        error = seL4_TCB_WriteRegisters(tcb1, 0, 0, 1, &regs);
174
175        /* Check that we had permission to do that and the cap was a TCB. */
176        if (error) {
177            return -1;
178        }
179
180        error = seL4_TCB_ReadRegisters(tcb2, 0, 0, 1, &regs);
181
182        /* Check that we had permission to do that and the cap was a TCB. */
183        if (error) {
184            return -1;
185        } else if (sel4utils_get_instruction_pointer(regs) != i) {
186            return 1;
187        }
188
189    }
190
191    return 0;
192}
193
194void create_helper_process_custom_asid(env_t env, helper_thread_t *thread, seL4_CPtr asid)
195{
196    UNUSED int error;
197
198    error = vka_alloc_endpoint(&env->vka, &thread->local_endpoint);
199    assert(error == 0);
200
201    thread->is_process = true;
202
203    sel4utils_process_config_t config = process_config_default_simple(&env->simple, "", OUR_PRIO - 1);
204    config = process_config_asid_pool(config, asid);
205    config = process_config_noelf(config, NULL, 0);
206    config = process_config_create_cnode(config, TEST_PROCESS_CSPACE_SIZE_BITS);
207    config = process_config_create_vspace(config, env->regions, env->num_regions);
208    vka_object_t fault_endpoint = { .cptr = env->endpoint };
209    config = process_config_fault_endpoint(config, fault_endpoint);
210    error = sel4utils_configure_process_custom(&thread->process, &env->vka, &env->vspace,
211                                               config);
212    assert(error == 0);
213
214    /* copy the elf reservations we need into the current process */
215    memcpy(thread->regions, env->regions, sizeof(sel4utils_elf_region_t) * env->num_regions);
216    thread->num_regions = env->num_regions;
217
218    /* clone data/code into vspace */
219    for (int i = 0; i < env->num_regions; i++) {
220        error = sel4utils_bootstrap_clone_into_vspace(&env->vspace, &thread->process.vspace, thread->regions[i].reservation);
221        assert(error == 0);
222    }
223
224    thread->thread = thread->process.thread;
225    assert(error == 0);
226}
227
228void create_helper_process(env_t env, helper_thread_t *thread)
229{
230    create_helper_process_custom_asid(env, thread, env->asid_pool);
231}
232
233NORETURN static void signal_helper_finished(seL4_CPtr local_endpoint, int val)
234{
235    seL4_MessageInfo_t info = seL4_MessageInfo_new(0, 0, 0, 1);
236    seL4_SetMR(0, val);
237    while (true) {
238        seL4_Call(local_endpoint, info);
239    }
240}
241
242NORETURN static void helper_thread(int argc, char **argv)
243{
244
245    helper_fn_t entry_point = (void *) atol(argv[0]);
246    seL4_CPtr local_endpoint = (seL4_CPtr) atol(argv[1]);
247
248    seL4_Word args[HELPER_THREAD_MAX_ARGS] = {0};
249    for (int i = 2; i < argc && i - 2 < HELPER_THREAD_MAX_ARGS; i++) {
250        assert(argv[i] != NULL);
251        args[i - 2] = atol(argv[i]);
252    }
253
254    /* run the thread */
255    int result = entry_point(args[0], args[1], args[2], args[3]);
256    signal_helper_finished(local_endpoint, result);
257    /* does not return */
258}
259
260NORETURN static void helper_process(int argc, char **argv)
261{
262    uintptr_t new_tp = sel4runtime_move_initial_tls(process_tls);
263    assert(new_tp != (uintptr_t)NULL);
264
265    helper_thread(argc, argv);
266}
267
268extern uintptr_t sel4_vsyscall[];
269
270void start_helper(env_t env, helper_thread_t *thread, helper_fn_t entry_point,
271                  seL4_Word arg0, seL4_Word arg1, seL4_Word arg2, seL4_Word arg3)
272{
273
274    UNUSED int error;
275
276    seL4_CPtr local_endpoint;
277
278    if (thread->is_process) {
279        /* copy the local endpoint */
280        cspacepath_t path;
281        vka_cspace_make_path(&env->vka, thread->local_endpoint.cptr, &path);
282        local_endpoint = sel4utils_copy_path_to_process(&thread->process, path);
283    } else {
284        local_endpoint = thread->local_endpoint.cptr;
285    }
286
287    sel4utils_create_word_args(thread->args_strings, thread->args, HELPER_THREAD_TOTAL_ARGS,
288                               (seL4_Word) entry_point, local_endpoint,
289                               arg0, arg1, arg2, arg3);
290
291    if (thread->is_process) {
292        thread->process.entry_point = (void *)helper_thread;
293        error = sel4utils_spawn_process_v(&thread->process, &env->vka, &env->vspace,
294                                          HELPER_THREAD_TOTAL_ARGS, thread->args, 0);
295        assert(error == 0);
296        /* sel4utils_spawn_process_v has created a stack frame that contains, amongst other
297           things, our arguments. Since we are going to be running a clone of this vspace
298           we would like to not call _start as this will result in initializing the C library
299           a second time. As we know the argument count and where argv will start we can
300           construct a register (or stack) layout that will allow us to pretend to be doing
301           a function call to helper_thread. */
302        seL4_UserContext context = {};
303        uintptr_t argv_base = (uintptr_t)thread->process.thread.initial_stack_pointer + sizeof(long);
304        uintptr_t aligned_stack_pointer = ALIGN_DOWN((uintptr_t)thread->process.thread.initial_stack_pointer,
305                                                     STACK_CALL_ALIGNMENT);
306        error = sel4utils_arch_init_context_with_args((sel4utils_thread_entry_fn)helper_process,
307                                                      (void *)HELPER_THREAD_TOTAL_ARGS,
308                                                      (void *)argv_base, NULL, false, (void *)aligned_stack_pointer,
309                                                      &context, &env->vka, &env->vspace, &thread->process.vspace);
310        assert(error == 0);
311        error = seL4_TCB_WriteRegisters(thread->process.thread.tcb.cptr, 1, 0, sizeof(seL4_UserContext) / sizeof(seL4_Word),
312                                        &context);
313        assert(error == 0);
314    } else {
315        error = sel4utils_start_thread(&thread->thread, (sel4utils_thread_entry_fn)helper_thread,
316                                       (void *) HELPER_THREAD_TOTAL_ARGS, (void *) thread->args, 1);
317        assert(error == 0);
318    }
319}
320
321void cleanup_helper(env_t env, helper_thread_t *thread)
322{
323    seL4_TCB_Suspend(thread->thread.tcb.cptr);
324    vka_free_object(&env->vka, &thread->local_endpoint);
325
326    if (thread->is_process) {
327        /* free the regions (no need to unmap, as the
328        * entry address space / cspace is being destroyed */
329        for (int i = 0; i < thread->num_regions; i++) {
330            vspace_free_reservation(&thread->process.vspace, thread->regions[i].reservation);
331        }
332
333        thread->process.fault_endpoint.cptr = 0;
334        sel4utils_destroy_process(&thread->process, &env->vka);
335    } else {
336        sel4utils_clean_up_thread(&env->vka, &env->vspace, &thread->thread);
337    }
338}
339
340void create_helper_thread(env_t env, helper_thread_t *thread)
341{
342    create_helper_thread_custom_stack(env, thread, BYTES_TO_4K_PAGES(CONFIG_SEL4UTILS_STACK_SIZE));
343}
344
345void create_helper_thread_custom_stack(env_t env, helper_thread_t *thread, size_t stack_pages)
346{
347    UNUSED int error;
348
349    error = vka_alloc_endpoint(&env->vka, &thread->local_endpoint);
350    assert(error == 0);
351
352    thread->is_process = false;
353    thread->fault_endpoint = env->endpoint;
354    seL4_Word data = api_make_guard_skip_word(seL4_WordBits - env->cspace_size_bits);
355    sel4utils_thread_config_t config = thread_config_default(&env->simple, env->cspace_root, data, env->endpoint,
356                                                             OUR_PRIO - 1);
357    config = thread_config_stack_size(config, stack_pages);
358    error = sel4utils_configure_thread_config(&env->vka, &env->vspace, &env->vspace,
359                                              config, &thread->thread);
360    assert(error == 0);
361}
362
363int wait_for_helper(helper_thread_t *thread)
364{
365    seL4_Word badge;
366
367    api_recv(thread->local_endpoint.cptr, &badge, thread->thread.reply.cptr);
368    return seL4_GetMR(0);
369}
370
371void set_helper_priority(env_t env, helper_thread_t *thread, seL4_Word prio)
372{
373    UNUSED int error;
374    error = seL4_TCB_SetPriority(thread->thread.tcb.cptr, env->tcb, prio);
375    assert(error == seL4_NoError);
376}
377
378void set_helper_mcp(env_t env, helper_thread_t *thread, seL4_Word mcp)
379{
380    UNUSED int error;
381    error = seL4_TCB_SetMCPriority(thread->thread.tcb.cptr, env->tcb, mcp);
382    assert(error == seL4_NoError);
383}
384
385void set_helper_affinity(UNUSED env_t env, helper_thread_t *thread, seL4_Word affinity)
386{
387#ifdef CONFIG_KERNEL_MCS
388    seL4_Time timeslice = CONFIG_BOOT_THREAD_TIME_SLICE * US_IN_S;
389    int error = seL4_SchedControl_Configure(simple_get_sched_ctrl(&env->simple, affinity),
390                                            thread->thread.sched_context.cptr,
391                                            timeslice, timeslice, 0, 0);
392    ZF_LOGF_IF(error, "Failed to configure scheduling context");
393#elif CONFIG_MAX_NUM_NODES > 1
394    int error = seL4_TCB_SetAffinity(thread->thread.tcb.cptr, affinity);
395    ZF_LOGF_IF(error, "Failed to set tcb affinity");
396#endif
397}
398
399seL4_CPtr get_helper_tcb(helper_thread_t *thread)
400{
401    return thread->thread.tcb.cptr;
402}
403
404seL4_CPtr get_helper_reply(helper_thread_t *thread)
405{
406    return thread->thread.reply.cptr;
407}
408
409seL4_CPtr get_helper_sched_context(helper_thread_t *thread)
410{
411    return thread->thread.sched_context.cptr;
412}
413
414uintptr_t get_helper_ipc_buffer_addr(helper_thread_t *thread)
415{
416    return thread->thread.ipc_buffer_addr;
417}
418
419uintptr_t get_helper_initial_stack_pointer(helper_thread_t *thread)
420{
421    return (uintptr_t)thread->thread.initial_stack_pointer;
422}
423
424static void sel4test_send_time_request(seL4_CPtr ep, uint64_t ns, sel4test_output_t request_type,
425                                       timeout_type_t timeout_type)
426{
427    seL4_MessageInfo_t tag;
428    seL4_SetMR(0, request_type);
429
430    switch (request_type) {
431    case SEL4TEST_TIME_TIMEOUT:
432        seL4_SetMR(1, timeout_type);
433        sel4utils_64_set_mr(2, ns);
434        tag = seL4_MessageInfo_new(0, 0, 0, (seL4_Uint32) SEL4UTILS_64_WORDS + 2);
435        break;
436    case SEL4TEST_TIME_TIMESTAMP:
437    case SEL4TEST_TIME_RESET:
438        tag = seL4_MessageInfo_new(0, 0, 0, 1);
439        break;
440    default:
441        ZF_LOGE("Invalid time request\n");
442        break;
443    }
444
445    seL4_Call(ep, tag);
446}
447
448void sleep_busy(env_t env, uint64_t ns)
449{
450    uint64_t start = sel4test_timestamp(env);
451    uint64_t now = sel4test_timestamp(env);
452    int same = 0;
453    while (now < start + ns) {
454        if (now == start) {
455            same++;
456            if (same == 10000) {
457                ZF_LOGE("Timer hasn't moved in 10000 iterations, are you handling interrupts?");
458            }
459        } else {
460            same = 0;
461        }
462        now = sel4test_timestamp(env);
463    }
464}
465
466inline void sel4test_sleep(env_t env, uint64_t ns)
467{
468    /*
469     * sleep is meant to block the calling thread for at least @ns. RPC costs and
470     * delivering timer notifications are not accounted for. Due to the fact that
471     * sleep requests are RPC calls on the same env->ep, only one test can request a sleep
472     * on a time. It is possible, however, that 2 (or more) threads request a sleep,
473     * being serialised, and wait on the same env->timer_notification at the same time,
474     * in which case the first thread in the queue will only be notified and not the
475     * other(s). This is a limitation, and the current interface won't handle it. Only
476     * one thread can request/wait/sleep/wakeup on a time.
477     */
478
479    sel4test_send_time_request(env->endpoint, ns, SEL4TEST_TIME_TIMEOUT, TIMEOUT_RELATIVE);
480    /* The tests have a timer_notification that they can wait on by default.
481     * sel4-driver will notify us on timer_notification when it gets a timer interrupt
482     */
483    seL4_Wait(env->timer_notification.cptr, NULL);
484}
485
486inline void sel4test_periodic_start(env_t env, uint64_t ns)
487{
488    sel4test_send_time_request(env->endpoint, ns, SEL4TEST_TIME_TIMEOUT, TIMEOUT_PERIODIC);
489}
490
491uint64_t sel4test_timestamp(env_t env)
492{
493    /*
494     * Request a timestamp from sel4test-driver. The request is sent over the fault ep,
495     * and, being synchronous, sel4test-driver sends back the timestamp in the RPC reply.
496     * RPC costs are not accounted for.
497     */
498    uint64_t time = 0;
499
500    sel4test_send_time_request(env->endpoint, 0, SEL4TEST_TIME_TIMESTAMP, 0);
501    time = sel4utils_64_get_mr(1);
502
503    return time;
504}
505
506inline void sel4test_timer_reset(env_t env)
507{
508    sel4test_send_time_request(env->endpoint, 0, SEL4TEST_TIME_RESET, 0);
509}
510
511inline void sel4test_ntfn_timer_wait(env_t env)
512{
513    seL4_Wait(env->timer_notification.cptr, NULL);
514}
515int set_helper_sched_params(UNUSED env_t env, UNUSED helper_thread_t *thread, UNUSED uint64_t budget,
516                            UNUSED uint64_t period, UNUSED seL4_Word badge)
517{
518    seL4_Word refills = 0;
519    if (budget < period) {
520#ifdef CONFIG_KERNEL_MCS
521        refills = seL4_MaxExtraRefills(seL4_MinSchedContextBits);
522#endif
523    }
524    return api_sched_ctrl_configure(simple_get_sched_ctrl(&env->simple, 0),
525                                    thread->thread.sched_context.cptr,
526                                    budget, period, refills, badge);
527}
528
529int create_passive_thread(env_t env, helper_thread_t *passive, helper_fn_t fn, seL4_CPtr ep,
530                          seL4_Word arg1, seL4_Word arg2, seL4_Word arg3)
531{
532    create_helper_thread(env, passive);
533    return start_passive_thread(env, passive, fn, ep, arg1, arg2, arg3);
534}
535
536int start_passive_thread(env_t env, helper_thread_t *passive, helper_fn_t fn, seL4_CPtr ep,
537                         seL4_Word arg1, seL4_Word arg2, seL4_Word arg3)
538{
539    start_helper(env, passive, fn, ep, arg1, arg2, arg3);
540
541    /* Wait for helper to signal it has initialised */
542    ZF_LOGD("Wait for passive thread to init");
543    seL4_Wait(ep, NULL);
544    ZF_LOGD("Done");
545    /* convert to passive */
546    return api_sc_unbind(passive->thread.sched_context.cptr);
547}
548
549int restart_after_syscall(env_t env, helper_thread_t *helper)
550{
551    /* save and resume helper->*/
552    seL4_UserContext regs;
553
554    int error = seL4_TCB_ReadRegisters(helper->thread.tcb.cptr, false, 0,
555                                       sizeof(seL4_UserContext) / sizeof(seL4_Word), &regs);
556    test_eq(error, seL4_NoError);
557
558    /* skip the call */
559    sel4utils_set_instruction_pointer(&regs, sel4utils_get_instruction_pointer(regs) + ARCH_SYSCALL_INSTRUCTION_SIZE);
560
561
562    error = seL4_TCB_WriteRegisters(helper->thread.tcb.cptr, true, 0,
563                                    sizeof(seL4_UserContext) / sizeof(seL4_Word), &regs);
564    test_eq(error, seL4_NoError);
565
566    return 0;
567}
568
569void set_helper_tfep(env_t env, helper_thread_t *thread, seL4_CPtr tfep)
570{
571    ZF_LOGF_IF(!config_set(CONFIG_KERNEL_MCS), "Unsupported on non MCS kernel");
572#ifdef CONFIG_KERNEL_MCS
573    int error = seL4_TCB_SetTimeoutEndpoint(thread->thread.tcb.cptr, tfep);
574    if (error != seL4_NoError) {
575        ZF_LOGF("Failed to set tfep\n");
576    }
577#endif
578}
579