1/*
2 * Copyright 2018, 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 GNU General Public License version 2. Note that NO WARRANTY is provided.
8 * See "LICENSE_GPLv2.txt" for details.
9 *
10 * @TAG(DATA61_GPL)
11 */
12
13/*
14 *
15 * Copyright 2016, 2017 Hesham Almatary, Data61/CSIRO <hesham.almatary@data61.csiro.au>
16 * Copyright 2015, 2016 Hesham Almatary <heshamelmatary@gmail.com>
17 */
18
19#include <types.h>
20#include <api/failures.h>
21#include <kernel/vspace.h>
22#include <object/structures.h>
23#include <arch/machine.h>
24#include <arch/model/statedata.h>
25#include <arch/object/objecttype.h>
26
27deriveCap_ret_t
28Arch_deriveCap(cte_t *slot, cap_t cap)
29{
30    deriveCap_ret_t ret;
31
32    switch (cap_get_capType(cap)) {
33
34    case cap_page_table_cap:
35        if (cap_page_table_cap_get_capPTIsMapped(cap)) {
36            ret.cap = cap;
37            ret.status = EXCEPTION_NONE;
38        } else {
39            userError("Deriving an unmapped PT cap");
40            current_syscall_error.type = seL4_IllegalOperation;
41            ret.cap = cap_null_cap_new();
42            ret.status = EXCEPTION_SYSCALL_ERROR;
43        }
44        return ret;
45
46    case cap_frame_cap:
47        cap = cap_frame_cap_set_capFMappedAddress(cap, 0);
48        ret.cap = cap_frame_cap_set_capFMappedASID(cap, asidInvalid);
49        ret.status = EXCEPTION_NONE;
50        return ret;
51
52    case cap_asid_control_cap:
53    case cap_asid_pool_cap:
54        ret.cap = cap;
55        ret.status = EXCEPTION_NONE;
56        return ret;
57
58    default:
59        /* This assert has no equivalent in haskell,
60         * as the options are restricted by type */
61        fail("Invalid arch cap type");
62    }
63}
64
65cap_t CONST
66Arch_updateCapData(bool_t preserve, word_t data, cap_t cap)
67{
68    return cap;
69}
70
71cap_t CONST
72Arch_maskCapRights(seL4_CapRights_t cap_rights_mask, cap_t cap)
73{
74    if (cap_get_capType(cap) == cap_frame_cap) {
75        vm_rights_t vm_rights;
76
77        vm_rights = vmRightsFromWord(cap_frame_cap_get_capFVMRights(cap));
78        vm_rights = maskVMRights(vm_rights, cap_rights_mask);
79        return cap_frame_cap_set_capFVMRights(cap, wordFromVMRights(vm_rights));
80    } else {
81        return cap;
82    }
83}
84
85finaliseCap_ret_t
86Arch_finaliseCap(cap_t cap, bool_t final)
87{
88    finaliseCap_ret_t fc_ret;
89
90    switch (cap_get_capType(cap)) {
91    case cap_frame_cap:
92
93        if (cap_frame_cap_get_capFMappedASID(cap)) {
94            unmapPage(cap_frame_cap_get_capFSize(cap),
95                      cap_frame_cap_get_capFMappedASID(cap),
96                      cap_frame_cap_get_capFMappedAddress(cap),
97                      cap_frame_cap_get_capFBasePtr(cap));
98        }
99        break;
100    case cap_page_table_cap:
101        if (final) {
102            asid_t asid = cap_page_table_cap_get_capPTMappedASID(cap);
103            if (asid != asidInvalid) {
104                findVSpaceForASID_ret_t find_ret = findVSpaceForASID(asid);
105                pte_t *pte = PTE_PTR(cap_page_table_cap_get_capPTBasePtr(cap));
106                if (find_ret.status == EXCEPTION_NONE && find_ret.vspace_root == pte) {
107                    deleteASID(cap_page_table_cap_get_capPTMappedASID(cap), pte);
108                } else if (cap_page_table_cap_get_capPTIsMapped(cap)) {
109                    unmapPageTable(asid, cap_page_table_cap_get_capPTMappedAddress(cap), pte);
110                }
111            }
112        }
113        break;
114    case cap_asid_pool_cap:
115        if (final) {
116            deleteASIDPool(
117                cap_asid_pool_cap_get_capASIDBase(cap),
118                ASID_POOL_PTR(cap_asid_pool_cap_get_capASIDPool(cap))
119            );
120        }
121        break;
122    case cap_asid_control_cap:
123        break;
124    }
125    fc_ret.remainder = cap_null_cap_new();
126    fc_ret.cleanupInfo = cap_null_cap_new();
127    return fc_ret;
128}
129
130bool_t CONST
131Arch_sameRegionAs(cap_t cap_a, cap_t cap_b)
132{
133    switch (cap_get_capType(cap_a)) {
134    case cap_frame_cap:
135        if (cap_get_capType(cap_b) == cap_frame_cap) {
136            word_t botA, botB, topA, topB;
137            botA = cap_frame_cap_get_capFBasePtr(cap_a);
138            botB = cap_frame_cap_get_capFBasePtr(cap_b);
139            topA = botA + MASK (pageBitsForSize(cap_frame_cap_get_capFSize(cap_a)));
140            topB = botB + MASK (pageBitsForSize(cap_frame_cap_get_capFSize(cap_b))) ;
141            return ((botA <= botB) && (topA >= topB) && (botB <= topB));
142        }
143        break;
144
145    case cap_page_table_cap:
146        if (cap_get_capType(cap_b) == cap_page_table_cap) {
147            return cap_page_table_cap_get_capPTBasePtr(cap_a) ==
148                   cap_page_table_cap_get_capPTBasePtr(cap_b);
149        }
150        break;
151    case cap_asid_control_cap:
152        if (cap_get_capType(cap_b) == cap_asid_control_cap) {
153            return true;
154        }
155        break;
156
157    case cap_asid_pool_cap:
158        if (cap_get_capType(cap_b) == cap_asid_pool_cap) {
159            return cap_asid_pool_cap_get_capASIDPool(cap_a) ==
160                   cap_asid_pool_cap_get_capASIDPool(cap_b);
161        }
162        break;
163    }
164
165    return false;
166}
167
168
169bool_t CONST
170Arch_sameObjectAs(cap_t cap_a, cap_t cap_b)
171{
172    if ((cap_get_capType(cap_a) == cap_frame_cap) &&
173            (cap_get_capType(cap_b) == cap_frame_cap)) {
174        return ((cap_frame_cap_get_capFBasePtr(cap_a) ==
175                 cap_frame_cap_get_capFBasePtr(cap_b)) &&
176                (cap_frame_cap_get_capFSize(cap_a) ==
177                 cap_frame_cap_get_capFSize(cap_b)) &&
178                ((cap_frame_cap_get_capFIsDevice(cap_a) == 0) ==
179                 (cap_frame_cap_get_capFIsDevice(cap_b) == 0)));
180    }
181    return Arch_sameRegionAs(cap_a, cap_b);
182}
183
184word_t
185Arch_getObjectSize(word_t t)
186{
187    switch (t) {
188    case seL4_RISCV_4K_Page:
189    case seL4_RISCV_PageTableObject:
190        return seL4_PageBits;
191    case seL4_RISCV_Mega_Page:
192        return seL4_LargePageBits;
193#if CONFIG_PT_LEVELS > 2
194    case seL4_RISCV_Giga_Page:
195        return seL4_HugePageBits;
196#endif
197#if CONFIG_PT_LEVELS > 3
198    case seL4_RISCV_Tera_Page:
199        return seL4_TeraPageBits;
200#endif
201    default:
202        fail("Invalid object type");
203        return 0;
204    }
205}
206
207cap_t Arch_createObject(object_t t, void *regionBase, int userSize, bool_t
208                        deviceMemory)
209{
210    switch (t) {
211    case seL4_RISCV_4K_Page:
212        return cap_frame_cap_new(
213                   asidInvalid,                    /* capFMappedASID       */
214                   (word_t) regionBase,            /* capFBasePtr          */
215                   RISCV_4K_Page,                  /* capFSize             */
216                   wordFromVMRights(VMReadWrite),  /* capFVMRights         */
217                   deviceMemory,                   /* capFIsDevice         */
218                   0                               /* capFMappedAddress    */
219               );
220
221    case seL4_RISCV_Mega_Page: {
222        return cap_frame_cap_new(
223                   asidInvalid,                    /* capFMappedASID       */
224                   (word_t) regionBase,            /* capFBasePtr          */
225                   RISCV_Mega_Page,                  /* capFSize             */
226                   wordFromVMRights(VMReadWrite),  /* capFVMRights         */
227                   deviceMemory,                   /* capFIsDevice         */
228                   0                               /* capFMappedAddress    */
229               );
230    }
231
232#if CONFIG_PT_LEVELS > 2
233    case seL4_RISCV_Giga_Page: {
234        return cap_frame_cap_new(
235                   asidInvalid,                    /* capFMappedASID       */
236                   (word_t) regionBase,            /* capFBasePtr          */
237                   RISCV_Giga_Page,                  /* capFSize             */
238                   wordFromVMRights(VMReadWrite),  /* capFVMRights         */
239                   deviceMemory,                   /* capFIsDevice         */
240                   0                               /* capFMappedAddress    */
241               );
242    }
243#endif
244
245    case seL4_RISCV_PageTableObject:
246        return cap_page_table_cap_new(
247                   asidInvalid,            /* capPTMappedASID    */
248                   (word_t)regionBase,     /* capPTBasePtr       */
249                   0,                      /* capPTIsMapped      */
250                   0                       /* capPTMappedAddress */
251               );
252
253    default:
254        /*
255         * This is a conflation of the haskell error: "Arch.createNewCaps
256         * got an API type" and the case where an invalid object type is
257         * passed (which is impossible in haskell).
258         */
259        fail("Arch_createObject got an API type or invalid object type");
260    }
261}
262
263exception_t
264Arch_decodeInvocation(
265    word_t label,
266    unsigned int length,
267    cptr_t cptr,
268    cte_t *slot,
269    cap_t cap,
270    extra_caps_t extraCaps,
271    bool_t call,
272    word_t *buffer
273)
274{
275    return decodeRISCVMMUInvocation(label, length, cptr, slot, cap, extraCaps, buffer);
276}
277
278void
279Arch_prepareThreadDelete(tcb_t *thread)
280{
281    /* No action required on RISCV. */
282}
283
284bool_t
285Arch_isFrameType(word_t t)
286{
287    switch (t) {
288#if CONFIG_PT_LEVELS == 4
289    case seL4_RISCV_Tera_Page:
290#endif
291#if CONFIG_PT_LEVELS > 2
292    case seL4_RISCV_Giga_Page:
293#endif
294    case seL4_RISCV_Mega_Page:
295    case seL4_RISCV_4K_Page:
296        return true;
297    default:
298        return false;
299    }
300}
301