blob: ba47aeffe4c8fb6540a4d660180e30521d38c773 [file] [log] [blame]
Thomas Heijligen5c43abc2023-12-11 15:24:36 +00001package FILO.FS.Ext2 is
Nico Huber1d7727f2023-11-30 15:58:46 +01002
Nico Huber57d3a852023-12-04 15:42:40 +01003 type T is private;
Nico Huber1d7727f2023-11-30 15:58:46 +01004
Nico Huber57d3a852023-12-04 15:42:40 +01005 function Is_Mounted (State : T) return Boolean;
6 function Is_Open (State : T) return Boolean
Nico Huber1d7727f2023-11-30 15:58:46 +01007 with
Nico Huber57d3a852023-12-04 15:42:40 +01008 Post => (if Is_Open'Result then Is_Mounted (State));
Nico Huber1d7727f2023-11-30 15:58:46 +01009
Nico Huber57d3a852023-12-04 15:42:40 +010010 procedure Mount
11 (State : in out T;
12 Part_Len : in Partition_Length;
13 Success : out Boolean)
Nico Huber1d7727f2023-11-30 15:58:46 +010014 with
Nico Huber57d3a852023-12-04 15:42:40 +010015 Pre => not Is_Mounted (State),
16 Post => Success = Is_Mounted (State);
Nico Huber1d7727f2023-11-30 15:58:46 +010017
Nico Huber57d3a852023-12-04 15:42:40 +010018 procedure Open
19 (State : in out T;
20 File_Len : out File_Length;
Nico Huberb1cb2d32023-12-17 01:45:47 +010021 File_Type : out FS.File_Type;
22 File_Name : in String;
23 In_Root : in Boolean;
Nico Huber57d3a852023-12-04 15:42:40 +010024 Success : out Boolean)
Nico Huber1d7727f2023-11-30 15:58:46 +010025 with
Nico Huberb1cb2d32023-12-17 01:45:47 +010026 Pre => Is_Mounted (State),
Nico Huber57d3a852023-12-04 15:42:40 +010027 Post => Success = Is_Open (State);
28
29 procedure Close (State : in out T)
30 with
31 Pre => Is_Open (State),
32 Post => Is_Mounted (State);
33
34 procedure Read
35 (State : in out T;
Nico Huber57d3a852023-12-04 15:42:40 +010036 File_Pos : in out File_Offset;
37 Buf : out Buffer_Type;
38 Len : out Natural)
39 with
40 Pre => Is_Open (State),
41 Post => Is_Open (State);
42
43private
44 type State is (Unmounted, Mounted, File_Opened);
45
Nico Huber26f71832023-12-05 16:26:56 +010046 -- maximum block size is 64KiB (2^16):
47 subtype Log_Block_Size is Positive range 10 .. 16;
Nico Huber700a4112024-01-08 15:50:09 +010048 subtype Block_Size is Natural range 2 ** Log_Block_Size'First .. 2 ** Log_Block_Size'Last;
Nico Huber6623c982023-12-12 16:35:46 +010049 subtype Max_Block_Index is Index_Type range 0 .. 2 ** Log_Block_Size'Last - 1;
50
51 -- Minimum ext2 block size is 1KiB (two 512B blocks)
52 type FSBlock_Offset is new Block_Offset range 0 .. Block_Offset'Last / 2;
53 type FSBlock_Logical is new Block_Offset range 0 .. Block_Offset'Last / 2;
54
Nico Huberfe897122023-12-12 21:33:36 +010055 -- We use a 64KiB cache which fits at least one ext2 block. If a lower
56 -- block size is encountered (likely), we partition the cache into up
57 -- to 64 1KiB blocks.
58 -- Cache entries can be used for blocks that map logical block offets
59 -- to physical ones. Then we note the first logical block offset mapped
Nico Huber57dfbfb2023-12-13 23:24:16 +010060 -- by the cached block. Otherwise, we use their physical offset.
61 type Cache_Label is new Unsigned_64;
Nico Huberfe897122023-12-12 21:33:36 +010062 subtype Block_Cache_Index is Natural range 0 .. 63;
Nico Huber57dfbfb2023-12-13 23:24:16 +010063 type Cache_Label_Logical is array (Block_Cache_Index) of Boolean;
64 type Cache_Label_Array is array (Block_Cache_Index) of Cache_Label;
Nico Huber6623c982023-12-12 16:35:46 +010065
Nico Huberfffc8c12023-12-13 12:44:12 +010066 -- Same as the 12 direct + 3 indirect blocks times 4B:
67 subtype Inode_Extents_Index is Natural range 0 .. 59;
Nico Huber33f6d952023-12-13 23:16:42 +010068 subtype Inode_Extents is Buffer_Type (Inode_Extents_Index);
Nico Huberfffc8c12023-12-13 12:44:12 +010069
Nico Huber21d42022023-12-16 02:50:22 +010070 type Inode_Index is new Unsigned_32 range 2 .. Unsigned_32'Last;
Nico Huber26f71832023-12-05 16:26:56 +010071 subtype Inode_Size is Positive range 128 .. Positive (Unsigned_16'Last);
Nico Hubercd1d5f72023-12-13 16:01:43 +010072 subtype Desc_Size is Positive range 32 .. 2 ** 15; -- power-of-2 that fits in 16 bits
Nico Huber26f71832023-12-05 16:26:56 +010073
Nico Huber022e2262023-12-15 23:15:17 +010074 type Inode_Type is (Dir, Regular, Link, Fast_Link);
75 type Inode_Length is range 0 .. 2 ** 46;
76
Nico Huber33f6d952023-12-13 23:16:42 +010077 type Inode_Info is record
Nico Huber89d05942023-12-18 12:12:00 +010078 I : Inode_Index := Inode_Index'First;
Nico Huber022e2262023-12-15 23:15:17 +010079 Mode : Inode_Type := Inode_Type'First;
80 Size : Inode_Length := 0;
Nico Hubercdc03512023-12-13 23:32:54 +010081 Use_Extents : Boolean := False;
Nico Huber7403a542023-12-15 23:13:47 +010082 Inline : Buffer_Type (Inode_Extents_Index) := (others => 16#00#);
Nico Huber33f6d952023-12-13 23:16:42 +010083 end record;
84
Nico Huber57d3a852023-12-04 15:42:40 +010085 type T is record
86 S : State;
Nico Huber57dfbfb2023-12-13 23:24:16 +010087 Part_Len : Partition_Length := 0;
88 First_Data_Block : FSBlock_Offset := 0;
Nico Huber700a4112024-01-08 15:50:09 +010089 Block_Size_Bits : Log_Block_Size := Log_Block_Size'First;
90 Block_Size : Ext2.Block_Size := Ext2.Block_Size'First;
Nico Huber21d42022023-12-16 02:50:22 +010091 Inodes_Per_Group : Inode_Index := Inode_Index'First;
Nico Huber57dfbfb2023-12-13 23:24:16 +010092 Inode_Size : Ext2.Inode_Size := Ext2.Inode_Size'First;
93 Desc_Size : Ext2.Desc_Size := Ext2.Desc_Size'First;
94 Feature_Extents : Boolean := False;
95 Feature_64Bit : Boolean := False;
96 Inode : Inode_Info := (others => <>);
Nico Huber21d42022023-12-16 02:50:22 +010097 Cur_Dir : Inode_Index := Inode_Index'First;
Nico Huber57dfbfb2023-12-13 23:24:16 +010098 Block_Cache_Logical : Cache_Label_Logical := (others => False);
99 Block_Cache_Label : Cache_Label_Array := (others => 0);
100 Block_Cache : Buffer_Type (Max_Block_Index) := (others => 16#00#);
Nico Huber57d3a852023-12-04 15:42:40 +0100101 end record;
Nico Huber1d7727f2023-11-30 15:58:46 +0100102
Thomas Heijligen5c43abc2023-12-11 15:24:36 +0000103end FILO.FS.Ext2;