1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155 | --
-- Copyright (c) 2022-2023, German Rivera
--
--
-- SPDX-License-Identifier: Apache-2.0
--
--
-- @summary HiRTOS separation kernel's memory protection internal support
--
with HiRTOS_Cpu_Arch_Interface;
with System.Storage_Elements;
with HiRTOS_Cpu_Arch_Interface.Memory_Protection;
private package HiRTOS.Separation_Kernel.Memory_Protection_Private
with SPARK_Mode => On
is
use HiRTOS_Cpu_Arch_Interface.Memory_Protection;
use System.Storage_Elements;
--
-- Mapping of logical memory protection regions to hypervisor memory protection descriptor
-- indices
--
type Memory_Region_Role_Type is
(Null_Pointer_Dereference_Guard,
Hypervisor_Code_Region,
Hypervisor_Rodata_Region,
Hypervisor_Interrupt_Stack_Overflow_Guard,
Hypervisor_Mmio_Region,
Partition0_Sram_Region,
Partition0_Tcm_Region,
Partition0_Mmio_Region,
Partition0_Reserved1_Region,
Partition1_Sram_Region,
Partition1_Tcm_Region,
Partition1_Mmio_Region,
Partition1_Reserved1_Region,
Partition2_Sram_Region,
Partition2_Tcm_Region,
Partition2_Mmio_Region,
Partition2_Reserved1_Region,
Partition3_Sram_Region,
Partition3_Tcm_Region,
Partition3_Mmio_Region,
Partition3_Reserved1_Region,
-- Valid region roles must be added before this entry:
Invalid_Region_Role);
for Memory_Region_Role_Type use
(Null_Pointer_Dereference_Guard => 0,
Hypervisor_Code_Region => 1,
Hypervisor_Rodata_Region => 2,
Hypervisor_Interrupt_Stack_Overflow_Guard => 3,
Hypervisor_Mmio_Region => 4,
Partition0_Sram_Region => 5,
Partition0_Tcm_Region => 6,
Partition0_Mmio_Region => 7,
Partition0_Reserved1_Region => 8,
Partition1_Sram_Region => 9,
Partition1_Tcm_Region => 10,
Partition1_Mmio_Region => 11,
Partition1_Reserved1_Region => 12,
Partition2_Sram_Region => 13,
Partition2_Tcm_Region => 14,
Partition2_Mmio_Region => 15,
Partition2_Reserved1_Region => 16,
Partition3_Sram_Region => 17,
Partition3_Tcm_Region => 18,
Partition3_Mmio_Region => 19,
Partition3_Reserved1_Region => 20,
-- Valid region roles must be added before this entry:
Invalid_Region_Role => Max_Num_Memory_Regions);
procedure Initialize
with Pre => HiRTOS_Cpu_Arch_Interface.Cpu_In_Hypervisor_Mode,
Post => HiRTOS_Cpu_Arch_Interface.Cpu_In_Hypervisor_Mode;
type Partition_Hypervisor_Regions_Config_Type is record
Sram_Region_Id : Memory_Region_Id_Type;
Tcm_Region_Id : Memory_Region_Id_Type;
Mmio_Region_Id : Memory_Region_Id_Type;
Reserved1_Region_Id : Memory_Region_Id_Type;
end record;
Partition_Hypervisor_Regions_Config_Array : constant
array (Valid_Partition_Id_Type) of Partition_Hypervisor_Regions_Config_Type :=
[0 => (Sram_Region_Id => Partition0_Sram_Region'Enum_Rep,
Tcm_Region_Id => Partition0_Tcm_Region'Enum_Rep,
Mmio_Region_Id => Partition0_Mmio_Region'Enum_Rep,
Reserved1_Region_Id => Partition0_Reserved1_Region'Enum_Rep),
1 => (Sram_Region_Id => Partition1_Sram_Region'Enum_Rep,
Tcm_Region_Id => Partition1_Tcm_Region'Enum_Rep,
Mmio_Region_Id => Partition1_Mmio_Region'Enum_Rep,
Reserved1_Region_Id => Partition1_Reserved1_Region'Enum_Rep),
2 => (Sram_Region_Id => Partition2_Sram_Region'Enum_Rep,
Tcm_Region_Id => Partition2_Tcm_Region'Enum_Rep,
Mmio_Region_Id => Partition2_Mmio_Region'Enum_Rep,
Reserved1_Region_Id => Partition2_Reserved1_Region'Enum_Rep),
3 => (Sram_Region_Id => Partition3_Sram_Region'Enum_Rep,
Tcm_Region_Id => Partition3_Tcm_Region'Enum_Rep,
Mmio_Region_Id => Partition3_Mmio_Region'Enum_Rep,
Reserved1_Region_Id => Partition3_Reserved1_Region'Enum_Rep)
];
--
-- Saved MPU region descriptors of a partition's internal memory
-- regions.
--
type Partition_Internal_Memory_Regions_Type is
array (Memory_Region_Id_Type) of Memory_Region_Descriptor_Type;
--
-- Initializes a partition's memory protection region descriptors
--
procedure Initialize_Partition_Memory_Regions (
Partition_Id : Valid_Partition_Id_Type;
TCM_Base_Address : System.Address;
TCM_Size_In_Bytes : System.Storage_Elements.Integer_Address;
SRAM_Base_Address : System.Address;
SRAM_Size_In_Bytes : System.Storage_Elements.Integer_Address;
MMIO_Base_Address : System.Address;
MMIO_Size_In_Bytes : System.Storage_Elements.Integer_Address;
Partition_Internal_Memory_Regions : out Partition_Internal_Memory_Regions_Type)
with Pre => HiRTOS_Cpu_Arch_Interface.Cpu_In_Hypervisor_Mode;
--
-- Restore a partition's memory protection regions
--
procedure Restore_Partition_Memory_Regions (
Partition_Id : Valid_Partition_Id_Type;
Partition_Internal_Memory_Regions : Partition_Internal_Memory_Regions_Type)
with Pre => HiRTOS_Cpu_Arch_Interface.Cpu_In_Hypervisor_Mode and then
HiRTOS_Cpu_Arch_Interface.Cpu_Interrupting_Disabled;
--
-- Save a partition's memory protection regions
--
procedure Save_Partition_Memory_Regions (
Partition_Id : Valid_Partition_Id_Type;
Partition_Internal_Memory_Regions : out Partition_Internal_Memory_Regions_Type)
with Pre => HiRTOS_Cpu_Arch_Interface.Cpu_In_Hypervisor_Mode;
end HiRTOS.Separation_Kernel.Memory_Protection_Private;
|