blob: 3dbbb2bd706b30312bdf7db3e02742416e58a06f [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;
Nico Huber1d7727f2023-11-30 15:58:46 +010014
Thomas Heijligen5c43abc2023-12-11 15:24:36 +000015with FILO.Blockdev;
16with FILO.FS.VFS;
Nico Huber8ec45a12023-12-04 17:11:08 +010017
18use Interfaces.C;
Nico Huber1d7727f2023-11-30 15:58:46 +010019
Thomas Heijligen5c43abc2023-12-11 15:24:36 +000020package body FILO.FS.Ext2 is
Nico Huber1d7727f2023-11-30 15:58:46 +010021
Nico Huber57d3a852023-12-04 15:42:40 +010022 function Is_Mounted (State : T) return Boolean is (State.S >= Mounted);
23 function Is_Open (State : T) return Boolean is (State.S = File_Opened);
24
Nico Huber26f71832023-12-05 16:26:56 +010025 --------------------------------------------------------------------------
26
27 SUPERBLOCK_SIZE : constant := 1024;
Nico Huber26f71832023-12-05 16:26:56 +010028 SUPERBLOCK_MAGIC : constant := 16#ef53#;
29 OLD_REV : constant := 0;
30 DYNAMIC_REV : constant := 1;
Nico Huber700a4112024-01-08 15:50:09 +010031
Nico Huber26f71832023-12-05 16:26:56 +010032 FEATURE_INCOMPAT_EXTENTS : constant := 16#0040#;
33 FEATURE_INCOMPAT_64BIT : constant := 16#0080#;
34
Nico Hubercdc03512023-12-13 23:32:54 +010035 EXT4_EXTENTS_FL : constant := 16#8_0000#;
36
Nico Huber57d3a852023-12-04 15:42:40 +010037 procedure Mount
38 (State : in out T;
39 Part_Len : in Partition_Length;
40 Success : out Boolean)
Nico Huber1d7727f2023-11-30 15:58:46 +010041 is
Nico Huber26f71832023-12-05 16:26:56 +010042 Super_Block : Buffer_Type (0 .. SUPERBLOCK_SIZE - 1) := (others => 0);
Nico Huber1d7727f2023-11-30 15:58:46 +010043 begin
Nico Huber26f71832023-12-05 16:26:56 +010044 if Part_Len < 2 * SUPERBLOCK_SIZE then
45 Success := False;
46 return;
47 end if;
48
Thomas Heijligen5c43abc2023-12-11 15:24:36 +000049 Blockdev.Read (Super_Block, 1 * SUPERBLOCK_SIZE, Success);
Nico Huber26f71832023-12-05 16:26:56 +010050 if not Success then
51 return;
52 end if;
53
54 if Read_LE16 (Super_Block, 14 * 4) /= 16#ef53# then
55 Success := False;
56 return;
57 end if;
58
59 State.Part_Len := Part_Len;
Nico Hubercd1d5f72023-12-13 16:01:43 +010060 State.First_Data_Block := FSBlock_Offset (Read_LE32 (Super_Block, 5 * 4));
Nico Huber26f71832023-12-05 16:26:56 +010061
62 declare
63 S_Log_Block_Size : constant Unsigned_32 := Read_LE32 (Super_Block, 6 * 4);
64 begin
65 if S_Log_Block_Size <= Unsigned_32 (Log_Block_Size'Last - 10) then
66 State.Block_Size_Bits := Log_Block_Size (S_Log_Block_Size + 10);
Nico Huber700a4112024-01-08 15:50:09 +010067 State.Block_Size := 2 ** Log_Block_Size (S_Log_Block_Size + 10);
Nico Huber26f71832023-12-05 16:26:56 +010068 else
69 Success := False;
70 return;
71 end if;
72 end;
73
74 declare
75 S_Inodes_Per_Group : constant Unsigned_32 := Read_LE32 (Super_Block, 10 * 4);
76 begin
Nico Huber21d42022023-12-16 02:50:22 +010077 if S_Inodes_Per_Group in 2 .. Unsigned_32'Last then
Nico Hubercdc03512023-12-13 23:32:54 +010078 State.Inodes_Per_Group := Inode_Index (S_Inodes_Per_Group);
Nico Huber26f71832023-12-05 16:26:56 +010079 else
80 Success := False;
81 return;
82 end if;
83 end;
84
85 declare
86 S_Rev_Level : constant Unsigned_32 := Read_LE32 (Super_Block, 19 * 4);
87 begin
88 if S_Rev_Level >= DYNAMIC_REV then
89 declare
90 S_Inode_Size : constant Unsigned_16 := Read_LE16 (Super_Block, 22 * 4);
91 begin
Nico Huber5a042fd2024-01-08 15:54:57 +010092 if Natural (S_Inode_Size) in Inode_Size then
Nico Huber26f71832023-12-05 16:26:56 +010093 State.Inode_Size := Inode_Size (S_Inode_Size);
94 else
95 Success := False;
96 return;
97 end if;
98 end;
99 else
100 State.Inode_Size := Inode_Size'First;
101 end if;
102 end;
103
104 declare
105 S_Feature_Incompat : constant Unsigned_32 := Read_LE32 (Super_Block, 24 * 4);
106 begin
107 State.Feature_Extents := (S_Feature_Incompat and FEATURE_INCOMPAT_EXTENTS) /= 0;
108 State.Feature_64Bit := (S_Feature_Incompat and FEATURE_INCOMPAT_64BIT) /= 0;
109 if State.Feature_64Bit then
110 declare
111 S_Desc_Size : constant Unsigned_16 := Read_LE16 (Super_Block, 63 * 4 + 2);
112 begin
Nico Huber700a4112024-01-08 15:50:09 +0100113 if Natural (S_Desc_Size) in Desc_Size and
114 Natural (S_Desc_Size) <= State.Block_Size and
115 Is_Power_Of_2 (S_Desc_Size)
Nico Huber26f71832023-12-05 16:26:56 +0100116 then
117 State.Desc_Size := Desc_Size (S_Desc_Size);
118 else
119 Success := False;
120 return;
121 end if;
122 end;
Nico Huber77a04d72023-12-13 23:11:40 +0100123 State.Feature_64Bit := State.Feature_64Bit and State.Desc_Size >= 64;
Nico Huber26f71832023-12-05 16:26:56 +0100124 else
125 State.Desc_Size := Desc_Size'First;
126 end if;
127 end;
128
129 State.S := Mounted;
Nico Huber1d7727f2023-11-30 15:58:46 +0100130 end Mount;
131
Nico Huberf5d99d02023-12-12 13:42:55 +0100132 procedure Read_FSBlock
Nico Huber700a4112024-01-08 15:50:09 +0100133 (Buf : in out Buffer_Type;
Nico Huberf5d99d02023-12-12 13:42:55 +0100134 FSBlock : in FSBlock_Offset;
Nico Huber700a4112024-01-08 15:50:09 +0100135 Part_Len : in Partition_Length;
Nico Huberf5d99d02023-12-12 13:42:55 +0100136 Success : out Boolean)
137 with
Nico Huber700a4112024-01-08 15:50:09 +0100138 Pre => Buf'Length in Block_Size
Nico Huberf5d99d02023-12-12 13:42:55 +0100139 is
Nico Huber700a4112024-01-08 15:50:09 +0100140 FSBlock_64 : constant Integer_64 := Integer_64 (FSBlock);
141 Block_Size : constant Integer_64 := Integer_64 (Buf'Length);
142 Max_Block_Offset : constant Integer_64 := Integer_64 (Part_Len) / Block_Size - 1;
Nico Huberf5d99d02023-12-12 13:42:55 +0100143 begin
Nico Huber700a4112024-01-08 15:50:09 +0100144 if FSBlock_64 > Max_Block_Offset then
Nico Huberf5d99d02023-12-12 13:42:55 +0100145 Success := False;
146 return;
147 end if;
Nico Huber700a4112024-01-08 15:50:09 +0100148 Blockdev.Read (Buf, Blockdev_Length (FSBlock_64 * Block_Size), Success);
Nico Huberf5d99d02023-12-12 13:42:55 +0100149 end Read_FSBlock;
150
Nico Huber68c86932023-12-13 11:03:11 +0100151 procedure Cache_FSBlock
152 (State : in out T;
153 Phys : in FSBlock_Offset;
154 Level : in Block_Cache_Index;
Nico Huber57dfbfb2023-12-13 23:24:16 +0100155 Label : in Cache_Label;
156 Logical : in Boolean := True;
Nico Huber68c86932023-12-13 11:03:11 +0100157 Cache_Start : out Max_Block_Index;
158 Cache_End : out Max_Block_Index;
159 Success : out Boolean)
160 with
Nico Huber700a4112024-01-08 15:50:09 +0100161 Post => Cache_End = Cache_Start + State.Block_Size - 1
Nico Huber68c86932023-12-13 11:03:11 +0100162 is
Nico Huber68c86932023-12-13 11:03:11 +0100163 -- Limit cache usage depending on block size:
Nico Huber700a4112024-01-08 15:50:09 +0100164 Max_Level : constant Block_Cache_Index := Block_Size'Last / State.Block_Size - 1;
165 Cache_Level : constant Block_Cache_Index := Block_Cache_Index'Min (Level, Max_Level);
Nico Huber68c86932023-12-13 11:03:11 +0100166 begin
Nico Huber700a4112024-01-08 15:50:09 +0100167 Cache_Start := Cache_Level * State.Block_Size;
168 Cache_End := Cache_Start + State.Block_Size - 1;
Nico Huber57dfbfb2023-12-13 23:24:16 +0100169 if State.Block_Cache_Logical (Cache_Level) = Logical and
170 State.Block_Cache_Label (Cache_Level) = Label
171 then
Nico Huber68c86932023-12-13 11:03:11 +0100172 Success := True;
173 else
174 Read_FSBlock
Nico Huber700a4112024-01-08 15:50:09 +0100175 (Buf => State.Block_Cache (Cache_Start .. Cache_End),
Nico Huber68c86932023-12-13 11:03:11 +0100176 FSBlock => Phys,
Nico Huber700a4112024-01-08 15:50:09 +0100177 Part_Len => State.Part_Len,
Nico Huber68c86932023-12-13 11:03:11 +0100178 Success => Success);
Nico Huber57dfbfb2023-12-13 23:24:16 +0100179 State.Block_Cache_Logical (Cache_Level) := Logical;
180 State.Block_Cache_Label (Cache_Level) := Label;
Nico Huber68c86932023-12-13 11:03:11 +0100181 end if;
182 end Cache_FSBlock;
183
Nico Huber57dfbfb2023-12-13 23:24:16 +0100184 procedure Cache_FSBlock
185 (State : in out T;
186 Phys : in FSBlock_Offset;
187 Level : in Block_Cache_Index;
188 Cache_Start : out Max_Block_Index;
189 Cache_End : out Max_Block_Index;
190 Success : out Boolean)
191 with
Nico Huber700a4112024-01-08 15:50:09 +0100192 Post => Cache_End = Cache_Start + State.Block_Size - 1
Nico Huber57dfbfb2023-12-13 23:24:16 +0100193 is
194 begin
195 Cache_FSBlock (State, Phys, Level, Cache_Label (Phys),
196 False, Cache_Start, Cache_End, Success);
197 end Cache_FSBlock;
198
199 procedure Reset_Cache_Logical (State : in out T) is
200 begin
201 for I in Block_Cache_Index loop
202 if State.Block_Cache_Logical (I) then
203 State.Block_Cache_Logical (I) := False;
204 State.Block_Cache_Label (I) := 0;
205 end if;
206 end loop;
207 end Reset_Cache_Logical;
208
Nico Huber6623c982023-12-12 16:35:46 +0100209 procedure Ext2_Block_Map
210 (State : in out T;
211 Logical : in FSBlock_Logical;
212 Physical : out FSBlock_Offset;
213 Success : out Boolean)
214 is
Nico Huber33f6d952023-12-13 23:16:42 +0100215 Direct_Blocks : constant := 12;
216 type Direct_Blocks_Array is array (Natural range 0 .. Direct_Blocks - 1) of Unsigned_32;
217 type Inode_Blocks is record
218 Direct_Blocks : Direct_Blocks_Array;
219 Indirect_Block : Unsigned_32;
220 Double_Indirect : Unsigned_32;
221 Triple_Indirect : Unsigned_32;
222 end record
Nico Huber5a042fd2024-01-08 15:54:57 +0100223 with Object_Size => Inode_Extents'Length * 8;
Nico Huber33f6d952023-12-13 23:16:42 +0100224
225 function I_Blocks is new Ada.Unchecked_Conversion (Inode_Extents, Inode_Blocks);
Nico Huber7403a542023-12-15 23:13:47 +0100226 function I_Blocks (State : T) return Inode_Blocks is (I_Blocks (State.Inode.Inline));
Nico Huber33f6d952023-12-13 23:16:42 +0100227
Nico Huber700a4112024-01-08 15:50:09 +0100228 Addr_Per_Block : constant FSBlock_Logical := FSBlock_Logical (State.Block_Size / 4);
229 Max_Addr_Per_Block : constant FSBlock_Logical := FSBlock_Logical (Block_Size'Last / 4);
Nico Huber6623c982023-12-12 16:35:46 +0100230 type Addr_In_Block_Range is range 0 .. Max_Addr_Per_Block - 1;
231
232 procedure Indirect_Block_Lookup
233 (Indirect_Block_Phys : in FSBlock_Offset;
234 Addr_In_Block : in Addr_In_Block_Range;
235 Level : in Block_Cache_Index;
236 Logical_Off : in FSBlock_Logical;
237 Next_Physical : out FSBlock_Offset;
238 Success : out Boolean)
239 with
Nico Huber5a042fd2024-01-08 15:54:57 +0100240 Pre =>
241 Addr_Per_Block = FSBlock_Logical (State.Block_Size / 4) and
242 FSBlock_Logical (Addr_In_Block) < Addr_Per_Block
Nico Huber6623c982023-12-12 16:35:46 +0100243 is
Nico Huber68c86932023-12-13 11:03:11 +0100244 Cache_Start, Cache_End : Max_Block_Index;
Nico Huber6623c982023-12-12 16:35:46 +0100245 begin
Nico Huber68c86932023-12-13 11:03:11 +0100246 Cache_FSBlock
247 (State => State,
248 Phys => Indirect_Block_Phys,
249 Level => Level,
Nico Huber57dfbfb2023-12-13 23:24:16 +0100250 Label => Cache_Label (Logical_Off),
Nico Huber68c86932023-12-13 11:03:11 +0100251 Cache_Start => Cache_Start,
252 Cache_End => Cache_End,
253 Success => Success);
Nico Huber6623c982023-12-12 16:35:46 +0100254 Next_Physical := FSBlock_Offset (Read_LE32
Nico Huberfe897122023-12-12 21:33:36 +0100255 (Buf => State.Block_Cache (Cache_Start .. Cache_End),
Nico Huber6623c982023-12-12 16:35:46 +0100256 Off => Natural (Addr_In_Block) * 4));
Nico Huber6623c982023-12-12 16:35:46 +0100257 end Indirect_Block_Lookup;
258
259 Logical_Rest : FSBlock_Logical := Logical;
Nico Huber5a042fd2024-01-08 15:54:57 +0100260
261 pragma Assert (Addr_Per_Block <= 2 ** 14);
Nico Huber6623c982023-12-12 16:35:46 +0100262 begin
263 if Logical_Rest < Direct_Blocks then
Nico Huber33f6d952023-12-13 23:16:42 +0100264 Physical := FSBlock_Offset (I_Blocks (State).Direct_Blocks (Natural (Logical)));
Nico Huber6623c982023-12-12 16:35:46 +0100265 Success := True;
266 return;
267 end if;
268
269 Logical_Rest := Logical_Rest - Direct_Blocks;
270 if Logical_Rest < Addr_Per_Block then
271 Indirect_Block_Lookup
Nico Huber33f6d952023-12-13 23:16:42 +0100272 (Indirect_Block_Phys => FSBlock_Offset (I_Blocks (State).Indirect_Block),
Nico Huber6623c982023-12-12 16:35:46 +0100273 Addr_In_Block => Addr_In_Block_Range (Logical_Rest),
Nico Huberfe897122023-12-12 21:33:36 +0100274 Level => 0,
Nico Huber6623c982023-12-12 16:35:46 +0100275 Logical_Off => Logical - Logical_Rest,
276 Next_Physical => Physical,
277 Success => Success);
278 return;
279 end if;
280
281 Logical_Rest := Logical_Rest - Addr_Per_Block;
282 if Logical_Rest < Addr_Per_Block ** 2 then
283 Indirect_Block_Lookup
Nico Huber33f6d952023-12-13 23:16:42 +0100284 (Indirect_Block_Phys => FSBlock_Offset (I_Blocks (State).Double_Indirect),
Nico Huber5a042fd2024-01-08 15:54:57 +0100285 Addr_In_Block => Addr_In_Block_Range ((Logical_Rest / Addr_Per_Block) mod Addr_Per_Block),
Nico Huberfe897122023-12-12 21:33:36 +0100286 Level => 1,
Nico Huber6623c982023-12-12 16:35:46 +0100287 Logical_Off => Logical - Logical_Rest,
288 Next_Physical => Physical,
289 Success => Success);
290 if not Success then
291 return;
292 end if;
293
294 Indirect_Block_Lookup
295 (Indirect_Block_Phys => Physical,
296 Addr_In_Block => Addr_In_Block_Range (Logical_Rest mod Addr_Per_Block),
Nico Huberfe897122023-12-12 21:33:36 +0100297 Level => 0,
Nico Huber6623c982023-12-12 16:35:46 +0100298 Logical_Off => Logical - (Logical_Rest mod Addr_Per_Block),
299 Next_Physical => Physical,
300 Success => Success);
301 return;
302 end if;
303
304 Logical_Rest := Logical_Rest - Addr_Per_Block ** 2;
305 if Logical_Rest < Addr_Per_Block ** 3 then
306 Indirect_Block_Lookup
Nico Huber33f6d952023-12-13 23:16:42 +0100307 (Indirect_Block_Phys => FSBlock_Offset (I_Blocks (State).Triple_Indirect),
Nico Huber5a042fd2024-01-08 15:54:57 +0100308 Addr_In_Block => Addr_In_Block_Range ((Logical_Rest / Addr_Per_Block ** 2) mod Addr_Per_Block),
Nico Huberfe897122023-12-12 21:33:36 +0100309 Level => 2,
Nico Huber6623c982023-12-12 16:35:46 +0100310 Logical_Off => Logical - Logical_Rest,
311 Next_Physical => Physical,
312 Success => Success);
313 if not Success then
314 return;
315 end if;
316
317 Indirect_Block_Lookup
318 (Indirect_Block_Phys => Physical,
Nico Huber5a042fd2024-01-08 15:54:57 +0100319 Addr_In_Block => Addr_In_Block_Range ((Logical_Rest / Addr_Per_Block) mod Addr_Per_Block),
Nico Huberfe897122023-12-12 21:33:36 +0100320 Level => 1,
Nico Huber6623c982023-12-12 16:35:46 +0100321 Logical_Off => Logical - (Logical_Rest mod Addr_Per_Block ** 2),
322 Next_Physical => Physical,
323 Success => Success);
324 if not Success then
325 return;
326 end if;
327
328 Indirect_Block_Lookup
329 (Indirect_Block_Phys => Physical,
330 Addr_In_Block => Addr_In_Block_Range (Logical_Rest mod Addr_Per_Block),
Nico Huberfe897122023-12-12 21:33:36 +0100331 Level => 0,
Nico Huber6623c982023-12-12 16:35:46 +0100332 Logical_Off => Logical - (Logical_Rest mod Addr_Per_Block),
333 Next_Physical => Physical,
334 Success => Success);
335 return;
336 end if;
337
338 -- Logical address was just too high.
Nico Huber5a042fd2024-01-08 15:54:57 +0100339 Physical := 0;
Nico Huber6623c982023-12-12 16:35:46 +0100340 Success := False;
341 end Ext2_Block_Map;
342
Nico Huberfffc8c12023-12-13 12:44:12 +0100343 procedure Extent_Block_Map
344 (State : in out T;
345 Logical : in FSBlock_Logical;
346 Physical : out FSBlock_Offset;
347 Success : out Boolean)
348 is
349 -- Extent blocks always start with a 12B header and contain 12B entries.
350 -- Every entry starts with the number of the first logical block it
351 -- covers. Entries are sorted by this number.
352 -- Depth > 0 blocks have index entries, referencing further extent blocks.
353 -- Depth = 0 blocks have extent entries, referencing a contiguous range
354 -- of data blocks.
355 --
356 -- +-----------------+
357 -- .-> | Hdr depth=0 |
358 -- | +-----------------+
359 -- | | Extent 0.. 12 |
360 -- +-------------+ | +-----------------+
361 -- | Hdr depth=1 | | | Extent 13.. 13 |
362 -- +-------------+ | +-----------------+
363 -- | Index 0 | --' | Extent 14..122 |
364 -- +-------------+ +-----------------+
365 -- | Index 123 | --.
366 -- +-------------+ | +-----------------+
367 -- `-> | Hdr depth=0 |
368 -- +-----------------+
369 -- | Extent 123..125 |
370 -- +-----------------+
371 -- | Extent 126..234 |
372 -- +-----------------+
373 --
374
375 Extent_Header_Size : constant := 12;
376 Extent_Header_Magic : constant := 16#f03a#;
377 subtype Extent_Off is Natural range 0 .. Extent_Header_Size;
378 subtype Extent_Idx is Natural range 1 .. (Max_Block_Index'Last + 1) / Extent_Header_Size - 1;
Nico Huber700a4112024-01-08 15:50:09 +0100379 Dynamic_Max_Index : constant Extent_Idx := State.Block_Size / Extent_Header_Size - 1;
Nico Huberfffc8c12023-12-13 12:44:12 +0100380
381 function Extent_Byte_Offset (Idx : Extent_Idx; Off : Extent_Off) return Natural
382 is
383 (Idx * Extent_Header_Size + Off);
384
385 function Header_Magic (Buf : Buffer_Type) return Unsigned_16
386 is
387 (Read_LE16 (Buf, 0))
388 with
389 Pre => Buf'Length >= 2;
390
391 function Header_Entries (Buf : Buffer_Type) return Natural
392 is
393 (Natural (Read_LE16 (Buf, 2)))
394 with
395 Pre => Buf'Length >= 4;
396
397 function Header_Depth (Buf : Buffer_Type) return Natural
398 is
399 (Natural (Read_LE16 (Buf, 6)))
400 with
401 Pre => Buf'Length >= 8;
402
403 function Index_Logical (Buf : Buffer_Type; Idx : Extent_Idx) return FSBlock_Logical
404 is
405 (FSBlock_Logical (Read_LE32 (Buf, Extent_Byte_Offset (Idx, 0))))
406 with
407 Pre => Buf'Length >= Extent_Byte_Offset (Idx, 4);
408
409 function Index_Physical (Buf : Buffer_Type; Idx : Extent_Idx) return FSBlock_Offset
410 is
411 (FSBlock_Offset
412 (Shift_Left (Unsigned_64 (Read_LE16 (Buf, Extent_Byte_Offset (Idx, 8))), 32) or
413 Unsigned_64 (Read_LE32 (Buf, Extent_Byte_Offset (Idx, 4)))))
414 with
415 Pre => Buf'Length >= Extent_Byte_Offset (Idx, 10);
416
417 function Extent_Logical (Buf : Buffer_Type; Idx : Extent_Idx) return FSBlock_Logical
418 renames Index_Logical;
419
420 function Extent_Length (Buf : Buffer_Type; Idx : Extent_Idx) return FSBlock_Logical
421 is
422 (FSBlock_Logical (Read_LE16 (Buf, Extent_Byte_Offset (Idx, 4))))
423 with
424 Pre => Buf'Length >= Extent_Byte_Offset (Idx, 6);
425
426 function Extent_Physical (Buf : Buffer_Type; Idx : Extent_Idx) return FSBlock_Offset
427 is
428 (FSBlock_Offset
429 (Shift_Left (Unsigned_64 (Read_LE16 (Buf, Extent_Byte_Offset (Idx, 6))), 32) or
430 Unsigned_64 (Read_LE32 (Buf, Extent_Byte_Offset (Idx, 8)))))
431 with
432 Pre => Buf'Length >= Extent_Byte_Offset (Idx, 12);
433
434 function Bin_Search (Buf : Buffer_Type; Refs : Extent_Idx) return Extent_Idx
435 with
436 Pre => Refs in 1 .. Extent_Idx (Buf'Length / Extent_Header_Size - 1) and
437 Extent_Logical (Buf, 1) <= Logical,
438 Post => Bin_Search'Result in 1 .. Refs and
439 Extent_Logical (Buf, Bin_Search'Result) <= Logical
440 is
441 Left : Extent_Idx := 1;
442 Right : Extent_Idx := Refs;
443 begin
444 while Left <= Right loop
445 declare
446 Mid : constant Extent_Idx := (Left + Right) / 2;
447 Ext_Logical : constant FSBlock_Logical := Extent_Logical (Buf, Mid);
448 begin
449 if Logical < Ext_Logical then
450 Right := Mid - 1;
451 else
452 Left := Mid + 1;
453 end if;
454 end;
455 end loop;
456 return Left - 1;
457 end Bin_Search;
458
459 procedure Next_Ref
460 (Current : in FSBlock_Offset;
461 Logical_Off : in FSBlock_Logical;
462 Depth : in Natural;
463 Next : out Extent_Idx;
464 Cache_Start : out Max_Block_Index;
465 Cache_End : out Max_Block_Index;
466 Success : out Boolean)
467 with
468 Pre => Logical_Off <= Logical,
469 Post => (if Success then
Nico Huber700a4112024-01-08 15:50:09 +0100470 Cache_End = Cache_Start + State.Block_Size - 1 and then
Nico Huberfffc8c12023-12-13 12:44:12 +0100471 Extent_Logical (State.Block_Cache (Cache_Start .. Cache_End), Next) <= Logical)
472 is
Nico Huberfffc8c12023-12-13 12:44:12 +0100473 begin
474 Cache_FSBlock
475 (State => State,
476 Phys => Current,
477 Level => Depth,
Nico Huber57dfbfb2023-12-13 23:24:16 +0100478 Label => Cache_Label (Logical_Off),
Nico Huberfffc8c12023-12-13 12:44:12 +0100479 Cache_Start => Cache_Start,
480 Cache_End => Cache_End,
481 Success => Success);
482 if not Success then
483 Next := 1;
484 return;
485 end if;
486
487 declare
488 Hdr_Magic : constant Unsigned_16 :=
489 Header_Magic (State.Block_Cache (Cache_Start .. Cache_End));
490 Hdr_Entries : constant Natural :=
491 Header_Entries (State.Block_Cache (Cache_Start .. Cache_End));
492 Hdr_Depth : constant Natural :=
493 Header_Depth (State.Block_Cache (Cache_Start .. Cache_End));
494 First_Logical : constant FSBlock_Logical :=
495 Extent_Logical (State.Block_Cache (Cache_Start .. Cache_End), 1);
496 begin
497 Success := Success and then
498 Hdr_Magic = Extent_Header_Magic and then
499 Hdr_Depth = Depth and then
500 Hdr_Entries <= Dynamic_Max_Index and then
501 First_Logical = Logical_Off;
502 if not Success then
503 Next := 1;
504 else
505 Next := Bin_Search (State.Block_Cache (Cache_Start .. Cache_End), Hdr_Entries);
506 end if;
507 end;
508 end Next_Ref;
509
Nico Huber7403a542023-12-15 23:13:47 +0100510 Inline_Extents : Ext2.Inode_Extents renames State.Inode.Inline;
511 Inode_Magic : constant Unsigned_16 := Header_Magic (Inline_Extents);
512 Inode_Entries : constant Natural := Header_Entries (Inline_Extents);
513 First_Logical : constant FSBlock_Logical := Extent_Logical (Inline_Extents, 1);
514 Depth : Natural := Header_Depth (Inline_Extents);
Nico Huberfffc8c12023-12-13 12:44:12 +0100515
516 Cache_Start, Cache_End : Max_Block_Index;
517 Logical_Off, Length : FSBlock_Logical;
518 Idx : Extent_Idx;
519 begin
520 Success :=
521 Inode_Magic = Extent_Header_Magic and then
522 Inode_Entries > 0 and then
Nico Huber7403a542023-12-15 23:13:47 +0100523 Inode_Entries < Inline_Extents'Length / Extent_Header_Size and then
Nico Huberfffc8c12023-12-13 12:44:12 +0100524 First_Logical <= Logical;
525 if not Success then
526 Physical := 0;
527 return;
528 end if;
529
Nico Huber7403a542023-12-15 23:13:47 +0100530 Idx := Bin_Search (Inline_Extents, Inode_Entries);
Nico Huberfffc8c12023-12-13 12:44:12 +0100531 if Depth = 0 then
Nico Huber7403a542023-12-15 23:13:47 +0100532 Physical := Extent_Physical (Inline_Extents, Idx);
533 Logical_Off := Extent_Logical (Inline_Extents, Idx);
534 Length := Extent_Length (Inline_Extents, Idx);
Nico Huberfffc8c12023-12-13 12:44:12 +0100535 else
Nico Huber7403a542023-12-15 23:13:47 +0100536 Physical := Index_Physical (Inline_Extents, Idx);
537 Logical_Off := Index_Logical (Inline_Extents, Idx);
Nico Huberfffc8c12023-12-13 12:44:12 +0100538 loop
539 Depth := Depth - 1;
540 Next_Ref
541 (Current => Physical,
542 Logical_Off => Logical_Off,
543 Depth => Depth,
544 Next => Idx,
545 Cache_Start => Cache_Start,
546 Cache_End => Cache_End,
547 Success => Success);
548 if not Success then
549 return;
550 end if;
551
552 exit when Depth = 0;
553 Physical := Index_Physical (State.Block_Cache (Cache_Start .. Cache_End), Idx);
554 Logical_Off := Index_Logical (State.Block_Cache (Cache_Start .. Cache_End), Idx);
555 end loop;
556
557 Physical := Extent_Physical (State.Block_Cache (Cache_Start .. Cache_End), Idx);
558 Logical_Off := Extent_Logical (State.Block_Cache (Cache_Start .. Cache_End), Idx);
559 Length := Extent_Length (State.Block_Cache (Cache_Start .. Cache_End), Idx);
560 end if;
561
562 Success :=
563 Length > 0 and then
Nico Huberc4c7a5e2023-12-14 00:08:56 +0100564 Logical_Off <= FSBlock_Logical'Last - Length and then
Nico Huberfffc8c12023-12-13 12:44:12 +0100565 Logical < Logical_Off + Length;
566 if Success then
567 Physical := Physical + FSBlock_Offset (Logical - Logical_Off);
568 end if;
569 end Extent_Block_Map;
570
Nico Huber57d3a852023-12-04 15:42:40 +0100571 procedure Open
Nico Hubercdc03512023-12-13 23:32:54 +0100572 (State : in out T;
573 Inode : in Inode_Index;
574 Success : out Boolean)
575 with
576 Pre => Is_Mounted (State) and not Is_Open (State),
577 Post => Success = Is_Open (State)
578 is
579 type Group_Index is new Natural;
580 subtype Desc_In_Block_Index is Group_Index
581 range 0 .. Group_Index (2 ** Log_Block_Size'Last / Desc_Size'First - 1);
582
Nico Huber700a4112024-01-08 15:50:09 +0100583 Inodes_Per_Block : constant Inode_Index := Inode_Index (State.Block_Size / State.Inode_Size);
584 Desc_Per_Block : constant Group_Index := Group_Index (State.Block_Size / State.Desc_Size);
Nico Hubercdc03512023-12-13 23:32:54 +0100585
Nico Huber022e2262023-12-15 23:15:17 +0100586 ------------------------
587 -- Group deserialization
588
Nico Hubercdc03512023-12-13 23:32:54 +0100589 subtype Group_Off is Natural range 0 .. Desc_Size'Last;
590 function Group_Byte_Offset (Idx : Group_Index; Off : Group_Off) return Natural
591 is
592 (Natural (Idx) * State.Desc_Size + Off);
593
594 function Group_Inode_Table (Buf : Buffer_Type; Idx : Group_Index) return FSBlock_Offset
595 is
596 (FSBlock_Offset (
597 (if State.Feature_64Bit
598 then Shift_Left (Unsigned_64 (Read_LE32 (Buf, Group_Byte_Offset (Idx, 40))), 32)
599 else 0)
600 or
601 Unsigned_64 (Read_LE32 (Buf, Group_Byte_Offset (Idx, 8)))))
602 with
603 Pre => Buf'Length >= Group_Byte_Offset (Idx, 44);
604
Nico Huber022e2262023-12-15 23:15:17 +0100605 ------------------------
606 -- Inode deserialization
607
Nico Hubercdc03512023-12-13 23:32:54 +0100608 subtype Inode_Off is Natural range 0 .. Inode_Size'Last;
609 function Inode_Byte_Offset (Idx : Inode_Index; Off : Inode_Off) return Natural
610 is
611 (Natural (Idx) * State.Inode_Size + Off);
612
Nico Huber022e2262023-12-15 23:15:17 +0100613 function Inode_Mode (Buf : Buffer_Type; Idx : Inode_Index) return Unsigned_16
614 is
615 (Read_LE16 (Buf, Inode_Byte_Offset (Idx, 0)))
616 with
617 Pre => Buf'Length >= Inode_Byte_Offset (Idx, 2);
618
619 function Inode_Size (Buf : Buffer_Type; Idx : Inode_Index; Mode : Inode_Type) return Unsigned_64
620 is
621 ((if Mode = Regular
622 then Shift_Left (Unsigned_64 (Read_LE32 (Buf, Inode_Byte_Offset (Idx, 108))), 32)
623 else 0) or
624 Unsigned_64 (Read_LE32 (Buf, Inode_Byte_Offset (Idx, 4))))
625 with
626 Pre => Buf'Length >= Inode_Byte_Offset (Idx, 112);
627
628 function Inode_Blocks (Buf : Buffer_Type; Idx : Inode_Index) return Unsigned_32
629 is
630 (Read_LE32 (Buf, Inode_Byte_Offset (Idx, 28)))
631 with
632 Pre => Buf'Length >= Inode_Byte_Offset (Idx, 32);
633
Nico Hubercdc03512023-12-13 23:32:54 +0100634 function Inode_Flags (Buf : Buffer_Type; Idx : Inode_Index) return Unsigned_32
635 is
636 (Read_LE32 (Buf, Inode_Byte_Offset (Idx, 32)))
637 with
638 Pre => Buf'Length >= Inode_Byte_Offset (Idx, 36);
639
Nico Huber022e2262023-12-15 23:15:17 +0100640 function Inode_File_ACL (Buf : Buffer_Type; Idx : Inode_Index) return Unsigned_32
641 is
642 (Read_LE32 (Buf, Inode_Byte_Offset (Idx, 104)))
643 with
644 Pre => Buf'Length >= Inode_Byte_Offset (Idx, 108);
645
Nico Hubercdc03512023-12-13 23:32:54 +0100646 Group : constant Group_Index := Group_Index ((Inode - 1) / State.Inodes_Per_Group);
647 Desc_Block : constant FSBlock_Offset :=
648 1 + State.First_Data_Block + FSBlock_Offset (Group / Desc_Per_Block);
649 Cache_Start, Cache_End : Max_Block_Index;
650 begin
651 Cache_FSBlock
652 (State => State,
653 Phys => Desc_Block,
654 Level => Natural'Min (Natural (Group / Desc_Per_Block), Block_Cache_Index'Last),
655 Cache_Start => Cache_Start,
656 Cache_End => Cache_End,
657 Success => Success);
658 if not Success then
659 return;
660 end if;
661
662 declare
663 Desc : constant Desc_In_Block_Index := Group mod Desc_Per_Block;
664 Inode_In_Group : constant Inode_Index := (Inode - 1) mod State.Inodes_Per_Group;
665 Inode_Block : constant FSBlock_Offset :=
666 Group_Inode_Table (State.Block_Cache (Cache_Start .. Cache_End), Group) +
667 FSBlock_Offset (Inode_In_Group / Inodes_Per_Block);
668 begin
669 Cache_FSBlock
670 (State => State,
671 Phys => Inode_Block,
672 Level => Block_Cache_Index'Last,
673 Cache_Start => Cache_Start,
674 Cache_End => Cache_End,
675 Success => Success);
676 if not Success then
677 return;
678 end if;
679
680 declare
Nico Huber022e2262023-12-15 23:15:17 +0100681 S_IFMT : constant := 8#170000#;
682 S_IFDIR : constant := 8#040000#;
683 S_IFREG : constant := 8#100000#;
684 S_IFLNK : constant := 8#120000#;
685
Nico Hubercdc03512023-12-13 23:32:54 +0100686 Inode_In_Block : constant Inode_Index := Inode_In_Group mod Inodes_Per_Block;
Nico Huber022e2262023-12-15 23:15:17 +0100687 I_Mode : constant Unsigned_16 :=
688 Inode_Mode (State.Block_Cache (Cache_Start .. Cache_End), Inode_In_Block);
Nico Hubercdc03512023-12-13 23:32:54 +0100689 I_Flags : constant Unsigned_32 :=
690 Inode_Flags (State.Block_Cache (Cache_Start .. Cache_End), Inode_In_Block);
691 begin
Nico Huber022e2262023-12-15 23:15:17 +0100692 case I_Mode and S_IFMT is
693 when S_IFDIR => State.Inode.Mode := Dir;
694 when S_IFREG => State.Inode.Mode := Regular;
695 when S_IFLNK => State.Inode.Mode := Link;
696 when others => Success := False; return;
697 end case;
698 if State.Inode.Mode = Link then
699 declare
700 I_File_ACL : constant Unsigned_32 := Inode_File_ACL (
701 State.Block_Cache (Cache_Start .. Cache_End), Inode_In_Block);
702 I_Blocks : constant Unsigned_32 := Inode_Blocks (
703 State.Block_Cache (Cache_Start .. Cache_End), Inode_In_Block);
704 begin
705 if (I_File_ACL = 0 and I_Blocks = 0) or
706 (I_File_ACL /= 0 and I_Blocks = 2 ** (State.Block_Size_Bits - 9))
707 then
708 State.Inode.Mode := Fast_Link;
709 end if;
710 end;
711 end if;
712 declare
713 I_Size : constant Unsigned_64 := Inode_Size (
714 State.Block_Cache (Cache_Start .. Cache_End), Inode_In_Block, State.Inode.Mode);
715 begin
716 if I_Size <= Unsigned_64 (Inode_Length'Last) then
717 State.Inode.Size := Inode_Length (I_Size);
718 else
719 Success := False;
720 end if;
721 end;
Nico Hubercdc03512023-12-13 23:32:54 +0100722 State.Inode.Use_Extents := State.Feature_Extents and (I_Flags and EXT4_EXTENTS_FL) /= 0;
Nico Huber7403a542023-12-15 23:13:47 +0100723 State.Inode.Inline := State.Block_Cache (Cache_Start + 40 .. Cache_Start + 100 - 1);
Nico Huber21d42022023-12-16 02:50:22 +0100724 State.Inode.I := Inode;
Nico Hubercdc03512023-12-13 23:32:54 +0100725 Reset_Cache_Logical (State);
726 State.S := File_Opened;
727 end;
728 end;
729 end Open;
730
731 procedure Open
Nico Huber57d3a852023-12-04 15:42:40 +0100732 (State : in out T;
733 File_Len : out File_Length;
Nico Huberb1cb2d32023-12-17 01:45:47 +0100734 File_Type : out FS.File_Type;
735 File_Name : in String;
736 In_Root : in Boolean;
Nico Huber57d3a852023-12-04 15:42:40 +0100737 Success : out Boolean)
Nico Huber1d7727f2023-11-30 15:58:46 +0100738 is
Nico Huber21d42022023-12-16 02:50:22 +0100739 File_Name_Max : constant := 255;
740 Root_Inode : constant := 2;
741
742 function Str_Buf_Equal (Str : String; Buf : Buffer_Type) return Boolean is
743 begin
744 for I in Str'Range loop
745 if Character'Pos (Str (I)) /= Buf (Buf'First + (I - Str'First)) then
746 return False;
747 end if;
748 end loop;
749 return True;
750 end Str_Buf_Equal;
751
752 File_Inode : Inode_Index;
753 File_Pos : File_Length;
Nico Huber1d7727f2023-11-30 15:58:46 +0100754 begin
Nico Huber57d3a852023-12-04 15:42:40 +0100755 File_Len := 0;
Nico Huber21d42022023-12-16 02:50:22 +0100756 File_Type := FS.File_Type'First;
757
758 if File_Name'Length > File_Name_Max then
759 Success := False;
760 return;
761 end if;
762
763 -- Ensure dir is opened:
764 --
765 if State.S = File_Opened then
766 if State.Cur_Dir /= State.Inode.I then
767 Success := False;
768 return;
769 end if;
770 else
771 if In_Root then
772 State.Cur_Dir := Root_Inode;
773 end if;
774 Open (State, State.Cur_Dir, Success);
775 if not Success then
776 return;
777 end if;
778 end if;
779
780 -- Lookup file in opened dir:
781 --
782 File_Pos := 0;
Nico Huber1d7727f2023-11-30 15:58:46 +0100783 Success := False;
Nico Huber21d42022023-12-16 02:50:22 +0100784 while Unsigned_64 (File_Pos) < Unsigned_64 (State.Inode.Size) loop
785 declare
786 Dir_Entry_Header_Length : constant := 4 + 2 + 1 + 1;
787 subtype Dir_Entry_Index is Natural
788 range 0 .. Dir_Entry_Header_Length + File_Name_Max - 1;
789 Dir_Entry : Buffer_Type (Dir_Entry_Index);
790 Entry_File_Pos : File_Offset := File_Pos;
791 Len : Natural;
792 begin
793 Read
794 (State => State,
795 File_Pos => Entry_File_Pos,
796 Buf => Dir_Entry (0 .. 7),
797 Len => Len);
798 if Len < Dir_Entry_Header_Length then
799 return;
800 end if;
801
802 -- Only check filenames of exact same length
803 if Read_LE32 (Dir_Entry, 0) > Root_Inode and then
804 File_Name'Length = Natural (Dir_Entry (6))
805 then
806 Read
807 (State => State,
808 File_Pos => Entry_File_Pos,
809 Buf => Dir_Entry (8 .. 8 + File_Name'Length - 1),
810 Len => Len);
811 if Len < File_Name'Length then
812 return;
813 end if;
814
815 File_Inode := Inode_Index (Read_LE32 (Dir_Entry, 0));
816 Success := Str_Buf_Equal (File_Name, Dir_Entry (8 .. 8 + File_Name'Length - 1));
817 exit when Success;
818 end if;
819
820 File_Pos := File_Pos + File_Length (Read_LE16 (Dir_Entry, 4));
821 end;
822 end loop;
823
824 if Success then
825 Open (State, File_Inode, Success);
826 if not Success then
827 return;
828 end if;
829
830 if State.Inode.Mode = Dir then
831 State.Cur_Dir := File_Inode;
832 end if;
833 end if;
834
835 Success := Unsigned_64 (State.Inode.Size) <= Unsigned_64 (File_Length'Last);
836 if Success then
837 File_Len := File_Length (State.Inode.Size);
838 File_Type := (case State.Inode.Mode is
839 when Dir => FS.Dir,
840 when Regular => FS.Regular,
841 when Link .. Fast_Link => FS.Link);
842 else
843 Close (State);
844 end if;
Nico Huber1d7727f2023-11-30 15:58:46 +0100845 end Open;
846
Nico Huber57d3a852023-12-04 15:42:40 +0100847 procedure Close (State : in out T) is
848 begin
849 State.S := Mounted;
850 end Close;
Nico Huber1d7727f2023-11-30 15:58:46 +0100851
Nico Huber57d3a852023-12-04 15:42:40 +0100852 procedure Read
853 (State : in out T;
Nico Huber57d3a852023-12-04 15:42:40 +0100854 File_Pos : in out File_Offset;
855 Buf : out Buffer_Type;
856 Len : out Natural)
Nico Huber1d7727f2023-11-30 15:58:46 +0100857 is
Nico Huberd3644be2023-12-16 01:43:00 +0100858 Pos : Natural;
Nico Huber1d7727f2023-11-30 15:58:46 +0100859 begin
Nico Huberd3644be2023-12-16 01:43:00 +0100860 if State.Inode.Mode = Fast_Link then
Nico Huber549a1b82023-12-17 01:51:59 +0100861 if State.Inode.Size > Inode_Length (State.Inode.Inline'Length) or
862 Inode_Length (File_Pos) >= State.Inode.Size then
Nico Huberd3644be2023-12-16 01:43:00 +0100863 Len := 0;
864 else
Nico Huber549a1b82023-12-17 01:51:59 +0100865 Len := Natural'Min (Buf'Length, Natural (State.Inode.Size) - Natural (File_Pos));
Nico Huberd3644be2023-12-16 01:43:00 +0100866 end if;
867 Buf (Buf'First .. Buf'First + Len - 1) :=
868 State.Inode.Inline (Natural (File_Pos) .. Natural (File_Pos) + Len - 1);
869 Buf (Buf'First + Len .. Buf'Last) := (others => 16#00#);
870 File_Pos := File_Pos + File_Length (Len);
871 return;
872 end if;
873
Nico Huber1d7727f2023-11-30 15:58:46 +0100874 Len := 0;
Nico Huberd3644be2023-12-16 01:43:00 +0100875 Pos := Buf'First;
876 while Pos <= Buf'Last and Inode_Length (File_Pos) < State.Inode.Size loop
877 declare
Nico Huber700a4112024-01-08 15:50:09 +0100878 In_Block : constant Max_Block_Index := Natural (File_Pos) mod State.Block_Size;
879 Logical : constant FSBlock_Logical := FSBlock_Logical (File_Pos / File_Offset (State.Block_Size));
880 In_Block_Space : constant Natural := Natural (State.Block_Size) - In_Block;
Nico Huber549a1b82023-12-17 01:51:59 +0100881 In_File_Space : constant Inode_Length := State.Inode.Size - Inode_Length (File_Pos);
Nico Huberd3644be2023-12-16 01:43:00 +0100882 In_Buf_Space : constant Natural := Buf'Last - Pos + 1;
883 Len_Here : Natural;
884 begin
885 Len_Here := In_Block_Space;
Nico Huber549a1b82023-12-17 01:51:59 +0100886 if In_File_Space < Inode_Length (Len_Here) then
887 Len_Here := Natural (In_File_Space);
Nico Huberd3644be2023-12-16 01:43:00 +0100888 end if;
889 if In_Buf_Space < Len_Here then
890 Len_Here := In_Buf_Space;
891 end if;
892
893 declare
894 Last : constant Index_Type := Pos + Len_Here - 1;
895 Cache_Start, Cache_End : Max_Block_Index;
896 Physical : FSBlock_Offset;
897 Success : Boolean;
898 begin
899 if State.Inode.Use_Extents then
900 Extent_Block_Map (State, Logical, Physical, Success);
901 else
902 Ext2_Block_Map (State, Logical, Physical, Success);
903 end if;
904 if Success then
905 Cache_FSBlock
906 (State => State,
907 Phys => Physical,
908 Level => Block_Cache_Index'Last,
909 Cache_Start => Cache_Start,
910 Cache_End => Cache_End,
911 Success => Success);
912 end if;
913 exit when not Success;
914
915 Buf (Pos .. Last) := State.Block_Cache (
916 Cache_Start + In_Block .. Cache_Start + In_Block + Len_Here - 1);
917 File_Pos := File_Pos + File_Length (Len_Here);
918 Pos := Pos + Len_Here;
919 Len := Len + Len_Here;
920 end;
921 end;
922 end loop;
923 Buf (Pos .. Buf'Last) := (others => 16#00#);
Nico Huber1d7727f2023-11-30 15:58:46 +0100924 end Read;
925
Nico Huber26f71832023-12-05 16:26:56 +0100926 --------------------------------------------------------------------------
927
928 package C is new VFS (T => T, Initial => (S => Unmounted, others => <>));
Nico Huber8ec45a12023-12-04 17:11:08 +0100929
930 function C_Mount return int
931 with
932 Export,
933 Convention => C,
934 External_Name => "ext2fs_mount";
935 function C_Mount return int
936 with
937 SPARK_Mode => Off
938 is
939 begin
940 return C.C_Mount;
941 end C_Mount;
942
Nico Huber3da21472023-12-18 15:43:35 +0100943 function C_Open (File_Path : System.Address) return int
Nico Huber8ec45a12023-12-04 17:11:08 +0100944 with
945 Export,
946 Convention => C,
947 External_Name => "ext2fs_dir";
Nico Huber3da21472023-12-18 15:43:35 +0100948 function C_Open (File_Path : System.Address) return int
Nico Huber8ec45a12023-12-04 17:11:08 +0100949 with
950 SPARK_Mode => Off
951 is
952 begin
953 return C.C_Open (File_Path);
954 end C_Open;
955
956 function C_Read (Buf : System.Address; Len : int) return int
957 with
958 Export,
959 Convention => C,
960 External_Name => "ext2fs_read";
961 function C_Read (Buf : System.Address; Len : int) return int
962 with
963 SPARK_Mode => Off
964 is
965 begin
966 return C.C_Read (Buf, Len);
967 end C_Read;
968
Thomas Heijligen5c43abc2023-12-11 15:24:36 +0000969end FILO.FS.Ext2;