blob: 1d074d435ae5b3cfb16b1a101594295504bf788a [file] [log] [blame]
Nico Huber26f71832023-12-05 16:26:56 +01001-- Derived from GRUB -- GRand Unified Bootloader
2-- Copyright (C) 1999, 2001, 2003 Free Software Foundation, Inc.
3-- Copyright (C) 2023 secunet Security Networks AG
4--
5-- This program is free software; you can redistribute it and/or modify
6-- it under the terms of the GNU General Public License as published by
7-- the Free Software Foundation; either version 2 of the License, or
8-- (at your option) any later version.
9
Nico Huber33f6d952023-12-13 23:16:42 +010010with Ada.Unchecked_Conversion;
Nico Huber8ec45a12023-12-04 17:11:08 +010011with System;
Nico Huber1d7727f2023-11-30 15:58:46 +010012with Interfaces;
Nico Huber8ec45a12023-12-04 17:11:08 +010013with Interfaces.C;
14with Interfaces.C.Strings;
Nico Huber1d7727f2023-11-30 15:58:46 +010015
Thomas Heijligen5c43abc2023-12-11 15:24:36 +000016with FILO.Blockdev;
17with FILO.FS.VFS;
Nico Huber8ec45a12023-12-04 17:11:08 +010018
19use Interfaces.C;
Nico Huber1d7727f2023-11-30 15:58:46 +010020
Thomas Heijligen5c43abc2023-12-11 15:24:36 +000021package body FILO.FS.Ext2 is
Nico Huber1d7727f2023-11-30 15:58:46 +010022
Nico Huber57d3a852023-12-04 15:42:40 +010023 function Is_Mounted (State : T) return Boolean is (State.S >= Mounted);
24 function Is_Open (State : T) return Boolean is (State.S = File_Opened);
25
Nico Huber26f71832023-12-05 16:26:56 +010026 --------------------------------------------------------------------------
27
28 SUPERBLOCK_SIZE : constant := 1024;
29 SUPERBLOCK_BLOCKS : constant := SUPERBLOCK_SIZE / BLOCK_SIZE;
30
31 SUPERBLOCK_MAGIC : constant := 16#ef53#;
32 OLD_REV : constant := 0;
33 DYNAMIC_REV : constant := 1;
34 FEATURE_INCOMPAT_EXTENTS : constant := 16#0040#;
35 FEATURE_INCOMPAT_64BIT : constant := 16#0080#;
36
Nico Hubercdc03512023-12-13 23:32:54 +010037 EXT4_EXTENTS_FL : constant := 16#8_0000#;
38
Nico Huber57d3a852023-12-04 15:42:40 +010039 procedure Mount
40 (State : in out T;
41 Part_Len : in Partition_Length;
42 Success : out Boolean)
Nico Huber1d7727f2023-11-30 15:58:46 +010043 is
Nico Huber26f71832023-12-05 16:26:56 +010044 Super_Block : Buffer_Type (0 .. SUPERBLOCK_SIZE - 1) := (others => 0);
Nico Huber1d7727f2023-11-30 15:58:46 +010045 begin
Nico Huber26f71832023-12-05 16:26:56 +010046 if Part_Len < 2 * SUPERBLOCK_SIZE then
47 Success := False;
48 return;
49 end if;
50
Thomas Heijligen5c43abc2023-12-11 15:24:36 +000051 Blockdev.Read (Super_Block, 1 * SUPERBLOCK_SIZE, Success);
Nico Huber26f71832023-12-05 16:26:56 +010052 if not Success then
53 return;
54 end if;
55
56 if Read_LE16 (Super_Block, 14 * 4) /= 16#ef53# then
57 Success := False;
58 return;
59 end if;
60
61 State.Part_Len := Part_Len;
Nico Hubercd1d5f72023-12-13 16:01:43 +010062 State.First_Data_Block := FSBlock_Offset (Read_LE32 (Super_Block, 5 * 4));
Nico Huber26f71832023-12-05 16:26:56 +010063
64 declare
65 S_Log_Block_Size : constant Unsigned_32 := Read_LE32 (Super_Block, 6 * 4);
66 begin
67 if S_Log_Block_Size <= Unsigned_32 (Log_Block_Size'Last - 10) then
68 State.Block_Size_Bits := Log_Block_Size (S_Log_Block_Size + 10);
69 else
70 Success := False;
71 return;
72 end if;
73 end;
74
75 declare
76 S_Inodes_Per_Group : constant Unsigned_32 := Read_LE32 (Super_Block, 10 * 4);
77 begin
Nico Hubercdc03512023-12-13 23:32:54 +010078 if S_Inodes_Per_Group in 1 .. Unsigned_32'Last then
79 State.Inodes_Per_Group := Inode_Index (S_Inodes_Per_Group);
Nico Huber26f71832023-12-05 16:26:56 +010080 else
81 Success := False;
82 return;
83 end if;
84 end;
85
86 declare
87 S_Rev_Level : constant Unsigned_32 := Read_LE32 (Super_Block, 19 * 4);
88 begin
89 if S_Rev_Level >= DYNAMIC_REV then
90 declare
91 S_Inode_Size : constant Unsigned_16 := Read_LE16 (Super_Block, 22 * 4);
92 begin
93 if S_Inode_Size in
94 Unsigned_16 (Inode_Size'First) .. Unsigned_16 (Inode_Size'Last)
95 then
96 State.Inode_Size := Inode_Size (S_Inode_Size);
97 else
98 Success := False;
99 return;
100 end if;
101 end;
102 else
103 State.Inode_Size := Inode_Size'First;
104 end if;
105 end;
106
107 declare
108 S_Feature_Incompat : constant Unsigned_32 := Read_LE32 (Super_Block, 24 * 4);
109 begin
110 State.Feature_Extents := (S_Feature_Incompat and FEATURE_INCOMPAT_EXTENTS) /= 0;
111 State.Feature_64Bit := (S_Feature_Incompat and FEATURE_INCOMPAT_64BIT) /= 0;
112 if State.Feature_64Bit then
113 declare
114 S_Desc_Size : constant Unsigned_16 := Read_LE16 (Super_Block, 63 * 4 + 2);
115 begin
Nico Hubercd1d5f72023-12-13 16:01:43 +0100116 if Is_Power_Of_2 (S_Desc_Size) and then
117 S_Desc_Size in Unsigned_16 (Desc_Size'First) ..
118 Unsigned_16 (Positive'Min (Desc_Size'Last, 2 ** State.Block_Size_Bits))
Nico Huber26f71832023-12-05 16:26:56 +0100119 then
120 State.Desc_Size := Desc_Size (S_Desc_Size);
121 else
122 Success := False;
123 return;
124 end if;
125 end;
Nico Huber77a04d72023-12-13 23:11:40 +0100126 State.Feature_64Bit := State.Feature_64Bit and State.Desc_Size >= 64;
Nico Huber26f71832023-12-05 16:26:56 +0100127 else
128 State.Desc_Size := Desc_Size'First;
129 end if;
130 end;
131
132 State.S := Mounted;
Nico Huber1d7727f2023-11-30 15:58:46 +0100133 end Mount;
134
Nico Huberf5d99d02023-12-12 13:42:55 +0100135 procedure Read_FSBlock
136 (State : in T;
137 Buf : out Buffer_Type;
138 FSBlock : in FSBlock_Offset;
139 Success : out Boolean)
140 with
141 Pre =>
142 Is_Mounted (State) and
143 Buf'Length = 2 ** State.Block_Size_Bits
144 is
145 Block_Size : constant Blockdev_Length := 2 ** State.Block_Size_Bits;
146 Max_Block_Offset : constant FSBlock_Offset :=
147 FSBlock_Offset (State.Part_Len / Block_Size - 1);
148 begin
149 if FSBlock > Max_Block_Offset then
150 Success := False;
151 return;
152 end if;
153 Blockdev.Read (Buf, Blockdev_Length (FSBlock) * Block_Size, Success);
154 end Read_FSBlock;
155
Nico Huber68c86932023-12-13 11:03:11 +0100156 procedure Cache_FSBlock
157 (State : in out T;
158 Phys : in FSBlock_Offset;
159 Level : in Block_Cache_Index;
Nico Huber57dfbfb2023-12-13 23:24:16 +0100160 Label : in Cache_Label;
161 Logical : in Boolean := True;
Nico Huber68c86932023-12-13 11:03:11 +0100162 Cache_Start : out Max_Block_Index;
163 Cache_End : out Max_Block_Index;
164 Success : out Boolean)
165 with
166 Post => Cache_End = Cache_Start + 2 ** State.Block_Size_Bits
167 is
168 Block_Size : constant Natural := 2 ** State.Block_Size_Bits;
169 -- Limit cache usage depending on block size:
170 Max_Level : constant Block_Cache_Index :=
171 2 ** (Log_Block_Size'Last - State.Block_Size_Bits) - 1;
172 Cache_Level : constant Block_Cache_Index :=
173 Block_Cache_Index'Min (Level, Max_Level);
174 begin
175 Cache_Start := Cache_Level * Block_Size;
176 Cache_End := Cache_Start + Block_Size - 1;
Nico Huber57dfbfb2023-12-13 23:24:16 +0100177 if State.Block_Cache_Logical (Cache_Level) = Logical and
178 State.Block_Cache_Label (Cache_Level) = Label
179 then
Nico Huber68c86932023-12-13 11:03:11 +0100180 Success := True;
181 else
182 Read_FSBlock
183 (State => State,
184 Buf => State.Block_Cache (Cache_Start .. Cache_End),
185 FSBlock => Phys,
186 Success => Success);
Nico Huber57dfbfb2023-12-13 23:24:16 +0100187 State.Block_Cache_Logical (Cache_Level) := Logical;
188 State.Block_Cache_Label (Cache_Level) := Label;
Nico Huber68c86932023-12-13 11:03:11 +0100189 end if;
190 end Cache_FSBlock;
191
Nico Huber57dfbfb2023-12-13 23:24:16 +0100192 procedure Cache_FSBlock
193 (State : in out T;
194 Phys : in FSBlock_Offset;
195 Level : in Block_Cache_Index;
196 Cache_Start : out Max_Block_Index;
197 Cache_End : out Max_Block_Index;
198 Success : out Boolean)
199 with
200 Post => Cache_End = Cache_Start + 2 ** State.Block_Size_Bits
201 is
202 begin
203 Cache_FSBlock (State, Phys, Level, Cache_Label (Phys),
204 False, Cache_Start, Cache_End, Success);
205 end Cache_FSBlock;
206
207 procedure Reset_Cache_Logical (State : in out T) is
208 begin
209 for I in Block_Cache_Index loop
210 if State.Block_Cache_Logical (I) then
211 State.Block_Cache_Logical (I) := False;
212 State.Block_Cache_Label (I) := 0;
213 end if;
214 end loop;
215 end Reset_Cache_Logical;
216
Nico Huber6623c982023-12-12 16:35:46 +0100217 procedure Ext2_Block_Map
218 (State : in out T;
219 Logical : in FSBlock_Logical;
220 Physical : out FSBlock_Offset;
221 Success : out Boolean)
222 is
Nico Huber33f6d952023-12-13 23:16:42 +0100223 Direct_Blocks : constant := 12;
224 type Direct_Blocks_Array is array (Natural range 0 .. Direct_Blocks - 1) of Unsigned_32;
225 type Inode_Blocks is record
226 Direct_Blocks : Direct_Blocks_Array;
227 Indirect_Block : Unsigned_32;
228 Double_Indirect : Unsigned_32;
229 Triple_Indirect : Unsigned_32;
230 end record
231 with Size => Inode_Extents'Length * 8;
232
233 function I_Blocks is new Ada.Unchecked_Conversion (Inode_Extents, Inode_Blocks);
Nico Huber7403a542023-12-15 23:13:47 +0100234 function I_Blocks (State : T) return Inode_Blocks is (I_Blocks (State.Inode.Inline));
Nico Huber33f6d952023-12-13 23:16:42 +0100235
Nico Huber6623c982023-12-12 16:35:46 +0100236 Block_Size : constant Natural := 2 ** State.Block_Size_Bits;
237 Addr_Per_Block : constant FSBlock_Logical := FSBlock_Logical (Block_Size / 4);
238 Max_Addr_Per_Block : constant FSBlock_Logical := FSBlock_Logical (2 ** Log_Block_Size'Last / 4);
239 type Addr_In_Block_Range is range 0 .. Max_Addr_Per_Block - 1;
240
241 procedure Indirect_Block_Lookup
242 (Indirect_Block_Phys : in FSBlock_Offset;
243 Addr_In_Block : in Addr_In_Block_Range;
244 Level : in Block_Cache_Index;
245 Logical_Off : in FSBlock_Logical;
246 Next_Physical : out FSBlock_Offset;
247 Success : out Boolean)
248 with
249 Pre => FSBlock_Logical (Addr_In_Block) < Addr_Per_Block
250 is
Nico Huber68c86932023-12-13 11:03:11 +0100251 Cache_Start, Cache_End : Max_Block_Index;
Nico Huber6623c982023-12-12 16:35:46 +0100252 begin
Nico Huber68c86932023-12-13 11:03:11 +0100253 Cache_FSBlock
254 (State => State,
255 Phys => Indirect_Block_Phys,
256 Level => Level,
Nico Huber57dfbfb2023-12-13 23:24:16 +0100257 Label => Cache_Label (Logical_Off),
Nico Huber68c86932023-12-13 11:03:11 +0100258 Cache_Start => Cache_Start,
259 Cache_End => Cache_End,
260 Success => Success);
Nico Huber6623c982023-12-12 16:35:46 +0100261 Next_Physical := FSBlock_Offset (Read_LE32
Nico Huberfe897122023-12-12 21:33:36 +0100262 (Buf => State.Block_Cache (Cache_Start .. Cache_End),
Nico Huber6623c982023-12-12 16:35:46 +0100263 Off => Natural (Addr_In_Block) * 4));
Nico Huber6623c982023-12-12 16:35:46 +0100264 end Indirect_Block_Lookup;
265
266 Logical_Rest : FSBlock_Logical := Logical;
267 begin
268 if Logical_Rest < Direct_Blocks then
Nico Huber33f6d952023-12-13 23:16:42 +0100269 Physical := FSBlock_Offset (I_Blocks (State).Direct_Blocks (Natural (Logical)));
Nico Huber6623c982023-12-12 16:35:46 +0100270 Success := True;
271 return;
272 end if;
273
274 Logical_Rest := Logical_Rest - Direct_Blocks;
275 if Logical_Rest < Addr_Per_Block then
276 Indirect_Block_Lookup
Nico Huber33f6d952023-12-13 23:16:42 +0100277 (Indirect_Block_Phys => FSBlock_Offset (I_Blocks (State).Indirect_Block),
Nico Huber6623c982023-12-12 16:35:46 +0100278 Addr_In_Block => Addr_In_Block_Range (Logical_Rest),
Nico Huberfe897122023-12-12 21:33:36 +0100279 Level => 0,
Nico Huber6623c982023-12-12 16:35:46 +0100280 Logical_Off => Logical - Logical_Rest,
281 Next_Physical => Physical,
282 Success => Success);
283 return;
284 end if;
285
286 Logical_Rest := Logical_Rest - Addr_Per_Block;
287 if Logical_Rest < Addr_Per_Block ** 2 then
288 Indirect_Block_Lookup
Nico Huber33f6d952023-12-13 23:16:42 +0100289 (Indirect_Block_Phys => FSBlock_Offset (I_Blocks (State).Double_Indirect),
Nico Huber6623c982023-12-12 16:35:46 +0100290 Addr_In_Block => Addr_In_Block_Range (Logical_Rest / Addr_Per_Block),
Nico Huberfe897122023-12-12 21:33:36 +0100291 Level => 1,
Nico Huber6623c982023-12-12 16:35:46 +0100292 Logical_Off => Logical - Logical_Rest,
293 Next_Physical => Physical,
294 Success => Success);
295 if not Success then
296 return;
297 end if;
298
299 Indirect_Block_Lookup
300 (Indirect_Block_Phys => Physical,
301 Addr_In_Block => Addr_In_Block_Range (Logical_Rest mod Addr_Per_Block),
Nico Huberfe897122023-12-12 21:33:36 +0100302 Level => 0,
Nico Huber6623c982023-12-12 16:35:46 +0100303 Logical_Off => Logical - (Logical_Rest mod Addr_Per_Block),
304 Next_Physical => Physical,
305 Success => Success);
306 return;
307 end if;
308
309 Logical_Rest := Logical_Rest - Addr_Per_Block ** 2;
310 if Logical_Rest < Addr_Per_Block ** 3 then
311 Indirect_Block_Lookup
Nico Huber33f6d952023-12-13 23:16:42 +0100312 (Indirect_Block_Phys => FSBlock_Offset (I_Blocks (State).Triple_Indirect),
Nico Huber6623c982023-12-12 16:35:46 +0100313 Addr_In_Block => Addr_In_Block_Range (Logical_Rest / Addr_Per_Block ** 2),
Nico Huberfe897122023-12-12 21:33:36 +0100314 Level => 2,
Nico Huber6623c982023-12-12 16:35:46 +0100315 Logical_Off => Logical - Logical_Rest,
316 Next_Physical => Physical,
317 Success => Success);
318 if not Success then
319 return;
320 end if;
321
322 Indirect_Block_Lookup
323 (Indirect_Block_Phys => Physical,
324 Addr_In_Block => Addr_In_Block_Range (Logical_Rest / Addr_Per_Block mod Addr_Per_Block),
Nico Huberfe897122023-12-12 21:33:36 +0100325 Level => 1,
Nico Huber6623c982023-12-12 16:35:46 +0100326 Logical_Off => Logical - (Logical_Rest mod Addr_Per_Block ** 2),
327 Next_Physical => Physical,
328 Success => Success);
329 if not Success then
330 return;
331 end if;
332
333 Indirect_Block_Lookup
334 (Indirect_Block_Phys => Physical,
335 Addr_In_Block => Addr_In_Block_Range (Logical_Rest mod Addr_Per_Block),
Nico Huberfe897122023-12-12 21:33:36 +0100336 Level => 0,
Nico Huber6623c982023-12-12 16:35:46 +0100337 Logical_Off => Logical - (Logical_Rest mod Addr_Per_Block),
338 Next_Physical => Physical,
339 Success => Success);
340 return;
341 end if;
342
343 -- Logical address was just too high.
344 Success := False;
345 end Ext2_Block_Map;
346
Nico Huberfffc8c12023-12-13 12:44:12 +0100347 procedure Extent_Block_Map
348 (State : in out T;
349 Logical : in FSBlock_Logical;
350 Physical : out FSBlock_Offset;
351 Success : out Boolean)
352 is
353 -- Extent blocks always start with a 12B header and contain 12B entries.
354 -- Every entry starts with the number of the first logical block it
355 -- covers. Entries are sorted by this number.
356 -- Depth > 0 blocks have index entries, referencing further extent blocks.
357 -- Depth = 0 blocks have extent entries, referencing a contiguous range
358 -- of data blocks.
359 --
360 -- +-----------------+
361 -- .-> | Hdr depth=0 |
362 -- | +-----------------+
363 -- | | Extent 0.. 12 |
364 -- +-------------+ | +-----------------+
365 -- | Hdr depth=1 | | | Extent 13.. 13 |
366 -- +-------------+ | +-----------------+
367 -- | Index 0 | --' | Extent 14..122 |
368 -- +-------------+ +-----------------+
369 -- | Index 123 | --.
370 -- +-------------+ | +-----------------+
371 -- `-> | Hdr depth=0 |
372 -- +-----------------+
373 -- | Extent 123..125 |
374 -- +-----------------+
375 -- | Extent 126..234 |
376 -- +-----------------+
377 --
378
379 Extent_Header_Size : constant := 12;
380 Extent_Header_Magic : constant := 16#f03a#;
381 subtype Extent_Off is Natural range 0 .. Extent_Header_Size;
382 subtype Extent_Idx is Natural range 1 .. (Max_Block_Index'Last + 1) / Extent_Header_Size - 1;
383
384 function Extent_Byte_Offset (Idx : Extent_Idx; Off : Extent_Off) return Natural
385 is
386 (Idx * Extent_Header_Size + Off);
387
388 function Header_Magic (Buf : Buffer_Type) return Unsigned_16
389 is
390 (Read_LE16 (Buf, 0))
391 with
392 Pre => Buf'Length >= 2;
393
394 function Header_Entries (Buf : Buffer_Type) return Natural
395 is
396 (Natural (Read_LE16 (Buf, 2)))
397 with
398 Pre => Buf'Length >= 4;
399
400 function Header_Depth (Buf : Buffer_Type) return Natural
401 is
402 (Natural (Read_LE16 (Buf, 6)))
403 with
404 Pre => Buf'Length >= 8;
405
406 function Index_Logical (Buf : Buffer_Type; Idx : Extent_Idx) return FSBlock_Logical
407 is
408 (FSBlock_Logical (Read_LE32 (Buf, Extent_Byte_Offset (Idx, 0))))
409 with
410 Pre => Buf'Length >= Extent_Byte_Offset (Idx, 4);
411
412 function Index_Physical (Buf : Buffer_Type; Idx : Extent_Idx) return FSBlock_Offset
413 is
414 (FSBlock_Offset
415 (Shift_Left (Unsigned_64 (Read_LE16 (Buf, Extent_Byte_Offset (Idx, 8))), 32) or
416 Unsigned_64 (Read_LE32 (Buf, Extent_Byte_Offset (Idx, 4)))))
417 with
418 Pre => Buf'Length >= Extent_Byte_Offset (Idx, 10);
419
420 function Extent_Logical (Buf : Buffer_Type; Idx : Extent_Idx) return FSBlock_Logical
421 renames Index_Logical;
422
423 function Extent_Length (Buf : Buffer_Type; Idx : Extent_Idx) return FSBlock_Logical
424 is
425 (FSBlock_Logical (Read_LE16 (Buf, Extent_Byte_Offset (Idx, 4))))
426 with
427 Pre => Buf'Length >= Extent_Byte_Offset (Idx, 6);
428
429 function Extent_Physical (Buf : Buffer_Type; Idx : Extent_Idx) return FSBlock_Offset
430 is
431 (FSBlock_Offset
432 (Shift_Left (Unsigned_64 (Read_LE16 (Buf, Extent_Byte_Offset (Idx, 6))), 32) or
433 Unsigned_64 (Read_LE32 (Buf, Extent_Byte_Offset (Idx, 8)))))
434 with
435 Pre => Buf'Length >= Extent_Byte_Offset (Idx, 12);
436
437 function Bin_Search (Buf : Buffer_Type; Refs : Extent_Idx) return Extent_Idx
438 with
439 Pre => Refs in 1 .. Extent_Idx (Buf'Length / Extent_Header_Size - 1) and
440 Extent_Logical (Buf, 1) <= Logical,
441 Post => Bin_Search'Result in 1 .. Refs and
442 Extent_Logical (Buf, Bin_Search'Result) <= Logical
443 is
444 Left : Extent_Idx := 1;
445 Right : Extent_Idx := Refs;
446 begin
447 while Left <= Right loop
448 declare
449 Mid : constant Extent_Idx := (Left + Right) / 2;
450 Ext_Logical : constant FSBlock_Logical := Extent_Logical (Buf, Mid);
451 begin
452 if Logical < Ext_Logical then
453 Right := Mid - 1;
454 else
455 Left := Mid + 1;
456 end if;
457 end;
458 end loop;
459 return Left - 1;
460 end Bin_Search;
461
462 procedure Next_Ref
463 (Current : in FSBlock_Offset;
464 Logical_Off : in FSBlock_Logical;
465 Depth : in Natural;
466 Next : out Extent_Idx;
467 Cache_Start : out Max_Block_Index;
468 Cache_End : out Max_Block_Index;
469 Success : out Boolean)
470 with
471 Pre => Logical_Off <= Logical,
472 Post => (if Success then
473 Extent_Logical (State.Block_Cache (Cache_Start .. Cache_End), Next) <= Logical)
474 is
475 Block_Size : constant Natural := 2 ** State.Block_Size_Bits;
476 Dynamic_Max_Index : constant Natural := Block_Size / Extent_Header_Size - 1;
477 begin
478 Cache_FSBlock
479 (State => State,
480 Phys => Current,
481 Level => Depth,
Nico Huber57dfbfb2023-12-13 23:24:16 +0100482 Label => Cache_Label (Logical_Off),
Nico Huberfffc8c12023-12-13 12:44:12 +0100483 Cache_Start => Cache_Start,
484 Cache_End => Cache_End,
485 Success => Success);
486 if not Success then
487 Next := 1;
488 return;
489 end if;
490
491 declare
492 Hdr_Magic : constant Unsigned_16 :=
493 Header_Magic (State.Block_Cache (Cache_Start .. Cache_End));
494 Hdr_Entries : constant Natural :=
495 Header_Entries (State.Block_Cache (Cache_Start .. Cache_End));
496 Hdr_Depth : constant Natural :=
497 Header_Depth (State.Block_Cache (Cache_Start .. Cache_End));
498 First_Logical : constant FSBlock_Logical :=
499 Extent_Logical (State.Block_Cache (Cache_Start .. Cache_End), 1);
500 begin
501 Success := Success and then
502 Hdr_Magic = Extent_Header_Magic and then
503 Hdr_Depth = Depth and then
504 Hdr_Entries <= Dynamic_Max_Index and then
505 First_Logical = Logical_Off;
506 if not Success then
507 Next := 1;
508 else
509 Next := Bin_Search (State.Block_Cache (Cache_Start .. Cache_End), Hdr_Entries);
510 end if;
511 end;
512 end Next_Ref;
513
Nico Huber7403a542023-12-15 23:13:47 +0100514 Inline_Extents : Ext2.Inode_Extents renames State.Inode.Inline;
515 Inode_Magic : constant Unsigned_16 := Header_Magic (Inline_Extents);
516 Inode_Entries : constant Natural := Header_Entries (Inline_Extents);
517 First_Logical : constant FSBlock_Logical := Extent_Logical (Inline_Extents, 1);
518 Depth : Natural := Header_Depth (Inline_Extents);
Nico Huberfffc8c12023-12-13 12:44:12 +0100519
520 Cache_Start, Cache_End : Max_Block_Index;
521 Logical_Off, Length : FSBlock_Logical;
522 Idx : Extent_Idx;
523 begin
524 Success :=
525 Inode_Magic = Extent_Header_Magic and then
526 Inode_Entries > 0 and then
Nico Huber7403a542023-12-15 23:13:47 +0100527 Inode_Entries < Inline_Extents'Length / Extent_Header_Size and then
Nico Huberfffc8c12023-12-13 12:44:12 +0100528 First_Logical <= Logical;
529 if not Success then
530 Physical := 0;
531 return;
532 end if;
533
Nico Huber7403a542023-12-15 23:13:47 +0100534 Idx := Bin_Search (Inline_Extents, Inode_Entries);
Nico Huberfffc8c12023-12-13 12:44:12 +0100535 if Depth = 0 then
Nico Huber7403a542023-12-15 23:13:47 +0100536 Physical := Extent_Physical (Inline_Extents, Idx);
537 Logical_Off := Extent_Logical (Inline_Extents, Idx);
538 Length := Extent_Length (Inline_Extents, Idx);
Nico Huberfffc8c12023-12-13 12:44:12 +0100539 else
Nico Huber7403a542023-12-15 23:13:47 +0100540 Physical := Index_Physical (Inline_Extents, Idx);
541 Logical_Off := Index_Logical (Inline_Extents, Idx);
Nico Huberfffc8c12023-12-13 12:44:12 +0100542 loop
543 Depth := Depth - 1;
544 Next_Ref
545 (Current => Physical,
546 Logical_Off => Logical_Off,
547 Depth => Depth,
548 Next => Idx,
549 Cache_Start => Cache_Start,
550 Cache_End => Cache_End,
551 Success => Success);
552 if not Success then
553 return;
554 end if;
555
556 exit when Depth = 0;
557 Physical := Index_Physical (State.Block_Cache (Cache_Start .. Cache_End), Idx);
558 Logical_Off := Index_Logical (State.Block_Cache (Cache_Start .. Cache_End), Idx);
559 end loop;
560
561 Physical := Extent_Physical (State.Block_Cache (Cache_Start .. Cache_End), Idx);
562 Logical_Off := Extent_Logical (State.Block_Cache (Cache_Start .. Cache_End), Idx);
563 Length := Extent_Length (State.Block_Cache (Cache_Start .. Cache_End), Idx);
564 end if;
565
566 Success :=
567 Length > 0 and then
Nico Huberc4c7a5e2023-12-14 00:08:56 +0100568 Logical_Off <= FSBlock_Logical'Last - Length and then
Nico Huberfffc8c12023-12-13 12:44:12 +0100569 Logical < Logical_Off + Length;
570 if Success then
571 Physical := Physical + FSBlock_Offset (Logical - Logical_Off);
572 end if;
573 end Extent_Block_Map;
574
Nico Huber57d3a852023-12-04 15:42:40 +0100575 procedure Open
Nico Hubercdc03512023-12-13 23:32:54 +0100576 (State : in out T;
577 Inode : in Inode_Index;
578 Success : out Boolean)
579 with
580 Pre => Is_Mounted (State) and not Is_Open (State),
581 Post => Success = Is_Open (State)
582 is
583 type Group_Index is new Natural;
584 subtype Desc_In_Block_Index is Group_Index
585 range 0 .. Group_Index (2 ** Log_Block_Size'Last / Desc_Size'First - 1);
586
587 Block_Size : constant Natural := 2 ** State.Block_Size_Bits;
588
589 Inodes_Per_Block : constant Inode_Index := Inode_Index (Block_Size / State.Inode_Size);
590 Desc_Per_Block : constant Group_Index := Group_Index (Block_Size / State.Desc_Size);
591
Nico Huber022e2262023-12-15 23:15:17 +0100592 ------------------------
593 -- Group deserialization
594
Nico Hubercdc03512023-12-13 23:32:54 +0100595 subtype Group_Off is Natural range 0 .. Desc_Size'Last;
596 function Group_Byte_Offset (Idx : Group_Index; Off : Group_Off) return Natural
597 is
598 (Natural (Idx) * State.Desc_Size + Off);
599
600 function Group_Inode_Table (Buf : Buffer_Type; Idx : Group_Index) return FSBlock_Offset
601 is
602 (FSBlock_Offset (
603 (if State.Feature_64Bit
604 then Shift_Left (Unsigned_64 (Read_LE32 (Buf, Group_Byte_Offset (Idx, 40))), 32)
605 else 0)
606 or
607 Unsigned_64 (Read_LE32 (Buf, Group_Byte_Offset (Idx, 8)))))
608 with
609 Pre => Buf'Length >= Group_Byte_Offset (Idx, 44);
610
Nico Huber022e2262023-12-15 23:15:17 +0100611 ------------------------
612 -- Inode deserialization
613
Nico Hubercdc03512023-12-13 23:32:54 +0100614 subtype Inode_Off is Natural range 0 .. Inode_Size'Last;
615 function Inode_Byte_Offset (Idx : Inode_Index; Off : Inode_Off) return Natural
616 is
617 (Natural (Idx) * State.Inode_Size + Off);
618
Nico Huber022e2262023-12-15 23:15:17 +0100619 function Inode_Mode (Buf : Buffer_Type; Idx : Inode_Index) return Unsigned_16
620 is
621 (Read_LE16 (Buf, Inode_Byte_Offset (Idx, 0)))
622 with
623 Pre => Buf'Length >= Inode_Byte_Offset (Idx, 2);
624
625 function Inode_Size (Buf : Buffer_Type; Idx : Inode_Index; Mode : Inode_Type) return Unsigned_64
626 is
627 ((if Mode = Regular
628 then Shift_Left (Unsigned_64 (Read_LE32 (Buf, Inode_Byte_Offset (Idx, 108))), 32)
629 else 0) or
630 Unsigned_64 (Read_LE32 (Buf, Inode_Byte_Offset (Idx, 4))))
631 with
632 Pre => Buf'Length >= Inode_Byte_Offset (Idx, 112);
633
634 function Inode_Blocks (Buf : Buffer_Type; Idx : Inode_Index) return Unsigned_32
635 is
636 (Read_LE32 (Buf, Inode_Byte_Offset (Idx, 28)))
637 with
638 Pre => Buf'Length >= Inode_Byte_Offset (Idx, 32);
639
Nico Hubercdc03512023-12-13 23:32:54 +0100640 function Inode_Flags (Buf : Buffer_Type; Idx : Inode_Index) return Unsigned_32
641 is
642 (Read_LE32 (Buf, Inode_Byte_Offset (Idx, 32)))
643 with
644 Pre => Buf'Length >= Inode_Byte_Offset (Idx, 36);
645
Nico Huber022e2262023-12-15 23:15:17 +0100646 function Inode_File_ACL (Buf : Buffer_Type; Idx : Inode_Index) return Unsigned_32
647 is
648 (Read_LE32 (Buf, Inode_Byte_Offset (Idx, 104)))
649 with
650 Pre => Buf'Length >= Inode_Byte_Offset (Idx, 108);
651
Nico Hubercdc03512023-12-13 23:32:54 +0100652 Group : constant Group_Index := Group_Index ((Inode - 1) / State.Inodes_Per_Group);
653 Desc_Block : constant FSBlock_Offset :=
654 1 + State.First_Data_Block + FSBlock_Offset (Group / Desc_Per_Block);
655 Cache_Start, Cache_End : Max_Block_Index;
656 begin
657 Cache_FSBlock
658 (State => State,
659 Phys => Desc_Block,
660 Level => Natural'Min (Natural (Group / Desc_Per_Block), Block_Cache_Index'Last),
661 Cache_Start => Cache_Start,
662 Cache_End => Cache_End,
663 Success => Success);
664 if not Success then
665 return;
666 end if;
667
668 declare
669 Desc : constant Desc_In_Block_Index := Group mod Desc_Per_Block;
670 Inode_In_Group : constant Inode_Index := (Inode - 1) mod State.Inodes_Per_Group;
671 Inode_Block : constant FSBlock_Offset :=
672 Group_Inode_Table (State.Block_Cache (Cache_Start .. Cache_End), Group) +
673 FSBlock_Offset (Inode_In_Group / Inodes_Per_Block);
674 begin
675 Cache_FSBlock
676 (State => State,
677 Phys => Inode_Block,
678 Level => Block_Cache_Index'Last,
679 Cache_Start => Cache_Start,
680 Cache_End => Cache_End,
681 Success => Success);
682 if not Success then
683 return;
684 end if;
685
686 declare
Nico Huber022e2262023-12-15 23:15:17 +0100687 S_IFMT : constant := 8#170000#;
688 S_IFDIR : constant := 8#040000#;
689 S_IFREG : constant := 8#100000#;
690 S_IFLNK : constant := 8#120000#;
691
Nico Hubercdc03512023-12-13 23:32:54 +0100692 Inode_In_Block : constant Inode_Index := Inode_In_Group mod Inodes_Per_Block;
Nico Huber022e2262023-12-15 23:15:17 +0100693 I_Mode : constant Unsigned_16 :=
694 Inode_Mode (State.Block_Cache (Cache_Start .. Cache_End), Inode_In_Block);
Nico Hubercdc03512023-12-13 23:32:54 +0100695 I_Flags : constant Unsigned_32 :=
696 Inode_Flags (State.Block_Cache (Cache_Start .. Cache_End), Inode_In_Block);
697 begin
Nico Huber022e2262023-12-15 23:15:17 +0100698 case I_Mode and S_IFMT is
699 when S_IFDIR => State.Inode.Mode := Dir;
700 when S_IFREG => State.Inode.Mode := Regular;
701 when S_IFLNK => State.Inode.Mode := Link;
702 when others => Success := False; return;
703 end case;
704 if State.Inode.Mode = Link then
705 declare
706 I_File_ACL : constant Unsigned_32 := Inode_File_ACL (
707 State.Block_Cache (Cache_Start .. Cache_End), Inode_In_Block);
708 I_Blocks : constant Unsigned_32 := Inode_Blocks (
709 State.Block_Cache (Cache_Start .. Cache_End), Inode_In_Block);
710 begin
711 if (I_File_ACL = 0 and I_Blocks = 0) or
712 (I_File_ACL /= 0 and I_Blocks = 2 ** (State.Block_Size_Bits - 9))
713 then
714 State.Inode.Mode := Fast_Link;
715 end if;
716 end;
717 end if;
718 declare
719 I_Size : constant Unsigned_64 := Inode_Size (
720 State.Block_Cache (Cache_Start .. Cache_End), Inode_In_Block, State.Inode.Mode);
721 begin
722 if I_Size <= Unsigned_64 (Inode_Length'Last) then
723 State.Inode.Size := Inode_Length (I_Size);
724 else
725 Success := False;
726 end if;
727 end;
Nico Hubercdc03512023-12-13 23:32:54 +0100728 State.Inode.Use_Extents := State.Feature_Extents and (I_Flags and EXT4_EXTENTS_FL) /= 0;
Nico Huber7403a542023-12-15 23:13:47 +0100729 State.Inode.Inline := State.Block_Cache (Cache_Start + 40 .. Cache_Start + 100 - 1);
Nico Hubercdc03512023-12-13 23:32:54 +0100730 Reset_Cache_Logical (State);
731 State.S := File_Opened;
732 end;
733 end;
734 end Open;
735
736 procedure Open
Nico Huber57d3a852023-12-04 15:42:40 +0100737 (State : in out T;
738 File_Len : out File_Length;
Nico Huberb1cb2d32023-12-17 01:45:47 +0100739 File_Type : out FS.File_Type;
740 File_Name : in String;
741 In_Root : in Boolean;
Nico Huber57d3a852023-12-04 15:42:40 +0100742 Success : out Boolean)
Nico Huber1d7727f2023-11-30 15:58:46 +0100743 is
744 begin
Nico Huber57d3a852023-12-04 15:42:40 +0100745 File_Len := 0;
Nico Huber1d7727f2023-11-30 15:58:46 +0100746 Success := False;
747 end Open;
748
Nico Huber57d3a852023-12-04 15:42:40 +0100749 procedure Close (State : in out T) is
750 begin
751 State.S := Mounted;
752 end Close;
Nico Huber1d7727f2023-11-30 15:58:46 +0100753
Nico Huber57d3a852023-12-04 15:42:40 +0100754 procedure Read
755 (State : in out T;
Nico Huber57d3a852023-12-04 15:42:40 +0100756 File_Pos : in out File_Offset;
757 Buf : out Buffer_Type;
758 Len : out Natural)
Nico Huber1d7727f2023-11-30 15:58:46 +0100759 is
Nico Huberd3644be2023-12-16 01:43:00 +0100760 Pos : Natural;
Nico Huber1d7727f2023-11-30 15:58:46 +0100761 begin
Nico Huberd3644be2023-12-16 01:43:00 +0100762 if State.Inode.Mode = Fast_Link then
Nico Huber549a1b82023-12-17 01:51:59 +0100763 if State.Inode.Size > Inode_Length (State.Inode.Inline'Length) or
764 Inode_Length (File_Pos) >= State.Inode.Size then
Nico Huberd3644be2023-12-16 01:43:00 +0100765 Len := 0;
766 else
Nico Huber549a1b82023-12-17 01:51:59 +0100767 Len := Natural'Min (Buf'Length, Natural (State.Inode.Size) - Natural (File_Pos));
Nico Huberd3644be2023-12-16 01:43:00 +0100768 end if;
769 Buf (Buf'First .. Buf'First + Len - 1) :=
770 State.Inode.Inline (Natural (File_Pos) .. Natural (File_Pos) + Len - 1);
771 Buf (Buf'First + Len .. Buf'Last) := (others => 16#00#);
772 File_Pos := File_Pos + File_Length (Len);
773 return;
774 end if;
775
Nico Huber1d7727f2023-11-30 15:58:46 +0100776 Len := 0;
Nico Huberd3644be2023-12-16 01:43:00 +0100777 Pos := Buf'First;
778 while Pos <= Buf'Last and Inode_Length (File_Pos) < State.Inode.Size loop
779 declare
780 Block_Size : constant File_Length := 2 ** State.Block_Size_Bits;
781 In_Block : constant Max_Block_Index := Natural (File_Pos mod Block_Size);
782 Logical : constant FSBlock_Logical := FSBlock_Logical (File_Pos / Block_Size);
783 In_Block_Space : constant Natural := Natural (Block_Size) - In_Block;
Nico Huber549a1b82023-12-17 01:51:59 +0100784 In_File_Space : constant Inode_Length := State.Inode.Size - Inode_Length (File_Pos);
Nico Huberd3644be2023-12-16 01:43:00 +0100785 In_Buf_Space : constant Natural := Buf'Last - Pos + 1;
786 Len_Here : Natural;
787 begin
788 Len_Here := In_Block_Space;
Nico Huber549a1b82023-12-17 01:51:59 +0100789 if In_File_Space < Inode_Length (Len_Here) then
790 Len_Here := Natural (In_File_Space);
Nico Huberd3644be2023-12-16 01:43:00 +0100791 end if;
792 if In_Buf_Space < Len_Here then
793 Len_Here := In_Buf_Space;
794 end if;
795
796 declare
797 Last : constant Index_Type := Pos + Len_Here - 1;
798 Cache_Start, Cache_End : Max_Block_Index;
799 Physical : FSBlock_Offset;
800 Success : Boolean;
801 begin
802 if State.Inode.Use_Extents then
803 Extent_Block_Map (State, Logical, Physical, Success);
804 else
805 Ext2_Block_Map (State, Logical, Physical, Success);
806 end if;
807 if Success then
808 Cache_FSBlock
809 (State => State,
810 Phys => Physical,
811 Level => Block_Cache_Index'Last,
812 Cache_Start => Cache_Start,
813 Cache_End => Cache_End,
814 Success => Success);
815 end if;
816 exit when not Success;
817
818 Buf (Pos .. Last) := State.Block_Cache (
819 Cache_Start + In_Block .. Cache_Start + In_Block + Len_Here - 1);
820 File_Pos := File_Pos + File_Length (Len_Here);
821 Pos := Pos + Len_Here;
822 Len := Len + Len_Here;
823 end;
824 end;
825 end loop;
826 Buf (Pos .. Buf'Last) := (others => 16#00#);
Nico Huber1d7727f2023-11-30 15:58:46 +0100827 end Read;
828
Nico Huber26f71832023-12-05 16:26:56 +0100829 --------------------------------------------------------------------------
830
831 package C is new VFS (T => T, Initial => (S => Unmounted, others => <>));
Nico Huber8ec45a12023-12-04 17:11:08 +0100832
833 function C_Mount return int
834 with
835 Export,
836 Convention => C,
837 External_Name => "ext2fs_mount";
838 function C_Mount return int
839 with
840 SPARK_Mode => Off
841 is
842 begin
843 return C.C_Mount;
844 end C_Mount;
845
846 function C_Open (File_Path : Strings.chars_ptr) return int
847 with
848 Export,
849 Convention => C,
850 External_Name => "ext2fs_dir";
851 function C_Open (File_Path : Strings.chars_ptr) return int
852 with
853 SPARK_Mode => Off
854 is
855 begin
856 return C.C_Open (File_Path);
857 end C_Open;
858
859 function C_Read (Buf : System.Address; Len : int) return int
860 with
861 Export,
862 Convention => C,
863 External_Name => "ext2fs_read";
864 function C_Read (Buf : System.Address; Len : int) return int
865 with
866 SPARK_Mode => Off
867 is
868 begin
869 return C.C_Read (Buf, Len);
870 end C_Read;
871
Thomas Heijligen5c43abc2023-12-11 15:24:36 +0000872end FILO.FS.Ext2;