blob: 7c1e467d4ada3cad4fdc0349d46f7f8462045365 [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
Nico Huber5a042fd2024-01-08 15:54:57 +010051 -- Extent physical addresses are 48 bits.
52 type FSBlock_Offset is new Block_Offset range 0 .. 2 ** 48 - 1;
53 -- Logical block addresses are 32 bits.
54 type FSBlock_Logical is new Block_Offset range 0 .. 2 ** 32 - 1;
Nico Huber6623c982023-12-12 16:35:46 +010055
Nico Huberfe897122023-12-12 21:33:36 +010056 -- We use a 64KiB cache which fits at least one ext2 block. If a lower
57 -- block size is encountered (likely), we partition the cache into up
58 -- to 64 1KiB blocks.
59 -- Cache entries can be used for blocks that map logical block offets
60 -- to physical ones. Then we note the first logical block offset mapped
Nico Huber57dfbfb2023-12-13 23:24:16 +010061 -- by the cached block. Otherwise, we use their physical offset.
62 type Cache_Label is new Unsigned_64;
Nico Huberfe897122023-12-12 21:33:36 +010063 subtype Block_Cache_Index is Natural range 0 .. 63;
Nico Huber57dfbfb2023-12-13 23:24:16 +010064 type Cache_Label_Logical is array (Block_Cache_Index) of Boolean;
65 type Cache_Label_Array is array (Block_Cache_Index) of Cache_Label;
Nico Huber52f4c8d2024-01-09 13:57:33 +010066 subtype Cache_Buffer is Buffer_Type (Max_Block_Index);
Nico Huber6623c982023-12-12 16:35:46 +010067
Nico Huberfffc8c12023-12-13 12:44:12 +010068 -- Same as the 12 direct + 3 indirect blocks times 4B:
69 subtype Inode_Extents_Index is Natural range 0 .. 59;
Nico Huber5a042fd2024-01-08 15:54:57 +010070 subtype Inode_Extents is Buffer_Type (Inode_Extents_Index)
71 with
72 Object_Size => (Inode_Extents_Index'Last + 1) * 8;
Nico Huberfffc8c12023-12-13 12:44:12 +010073
Nico Huber21d42022023-12-16 02:50:22 +010074 type Inode_Index is new Unsigned_32 range 2 .. Unsigned_32'Last;
Nico Huber26f71832023-12-05 16:26:56 +010075 subtype Inode_Size is Positive range 128 .. Positive (Unsigned_16'Last);
Nico Hubercd1d5f72023-12-13 16:01:43 +010076 subtype Desc_Size is Positive range 32 .. 2 ** 15; -- power-of-2 that fits in 16 bits
Nico Huber26f71832023-12-05 16:26:56 +010077
Nico Huber022e2262023-12-15 23:15:17 +010078 type Inode_Type is (Dir, Regular, Link, Fast_Link);
79 type Inode_Length is range 0 .. 2 ** 46;
80
Nico Huber33f6d952023-12-13 23:16:42 +010081 type Inode_Info is record
Nico Huber89d05942023-12-18 12:12:00 +010082 I : Inode_Index := Inode_Index'First;
Nico Huber022e2262023-12-15 23:15:17 +010083 Mode : Inode_Type := Inode_Type'First;
84 Size : Inode_Length := 0;
Nico Hubercdc03512023-12-13 23:32:54 +010085 Use_Extents : Boolean := False;
Nico Huber5a042fd2024-01-08 15:54:57 +010086 Inline : Inode_Extents := (others => 16#00#);
Nico Huber33f6d952023-12-13 23:16:42 +010087 end record;
88
Nico Huber52f4c8d2024-01-09 13:57:33 +010089 type Mount_State is record
Nico Huber57dfbfb2023-12-13 23:24:16 +010090 Part_Len : Partition_Length := 0;
91 First_Data_Block : FSBlock_Offset := 0;
Nico Huber700a4112024-01-08 15:50:09 +010092 Block_Size_Bits : Log_Block_Size := Log_Block_Size'First;
93 Block_Size : Ext2.Block_Size := Ext2.Block_Size'First;
Nico Huber21d42022023-12-16 02:50:22 +010094 Inodes_Per_Group : Inode_Index := Inode_Index'First;
Nico Huber57dfbfb2023-12-13 23:24:16 +010095 Inode_Size : Ext2.Inode_Size := Ext2.Inode_Size'First;
96 Desc_Size : Ext2.Desc_Size := Ext2.Desc_Size'First;
97 Feature_Extents : Boolean := False;
98 Feature_64Bit : Boolean := False;
Nico Huber52f4c8d2024-01-09 13:57:33 +010099 end record;
100
101 type Block_Cache is record
102 Logical : Cache_Label_Logical := (others => False);
103 Label : Cache_Label_Array := (others => 0);
104 Buffer : Cache_Buffer := (others => 16#00#);
105 end record;
106
107 type T is record
108 Static : Mount_State := (others => <>);
109 S : State;
110 Inode : Inode_Info := (others => <>);
111 Cur_Dir : Inode_Index := Inode_Index'First;
112 Cache : Block_Cache := (others => <>);
Nico Huber57d3a852023-12-04 15:42:40 +0100113 end record;
Nico Huber1d7727f2023-11-30 15:58:46 +0100114
Thomas Heijligen5c43abc2023-12-11 15:24:36 +0000115end FILO.FS.Ext2;