1/*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: GPL-2.0-only
5 */
6
7#pragma once
8
9#include <config.h>
10#include <mode/machine.h>
11
12static inline void invalidateLocalTLB_VMID(word_t vmid)
13{
14    word_t vttbr = getVTTBR();
15    word_t v = (vttbr >> 48);
16    dsb();
17    /* We need to switch to the target VMID for flushing
18     * the TLB if necessary.
19     * Note that an invalid address is used, and it seems
20     * fine. Otherwise, an ASID lookup is required.
21     */
22    if (v != vmid) {
23        setCurrentUserVSpaceRoot(ttbr_new(vmid, 0));
24    }
25    invalidateLocalTLB_VMALLS12E1();
26    if (v != vmid) {
27        /* Restore the previous VTTBR value */
28        setCurrentUserVSpaceRoot((ttbr_t) {
29            .words[0] = vttbr
30        });
31    }
32}
33
34static inline void invalidateLocalTLB_IPA_VMID(word_t ipa_plus_vmid)
35{
36    word_t vttbr = getVTTBR();
37    word_t v = (vttbr >> 48);
38    word_t vmid = ipa_plus_vmid >> 48;
39    /* The [0:35] bits are IPA, other bits are reserved as 0 */
40    word_t ipa = ipa_plus_vmid & 0xfffffffff;
41    dsb();
42    if (v != vmid) {
43        setCurrentUserVSpaceRoot(ttbr_new(vmid, 0));
44    }
45    invalidateLocalTLB_IPA(ipa);
46    if (v != vmid) {
47        setCurrentUserVSpaceRoot((ttbr_t) {
48            .words[0] = vttbr
49        });
50    }
51}
52
53
54