blob: 1757da8d1e4d49dbe50927b9ef1ced41ae255c48 [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 Huber53df7852024-01-15 18:36:04 +010027 Post => (if Success then Is_Open (State) else Is_Mounted (State));
Nico Huber57d3a852023-12-04 15:42:40 +010028
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
Nico Huber53df7852024-01-15 18:36:04 +010040 Pre => Is_Open (State) and Buf'Length > 0,
Nico Huber57d3a852023-12-04 15:42:40 +010041 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 Huberfe260322024-01-10 17:59:57 +010074 -- TODO: Could use modular Unsigned_32 if GNATprove wouldn't stumble as much:
75 type Inode_0_Index is new Integer_64 range 0 .. Integer_64 (Unsigned_32'Last);
Nico Huber925326e2024-01-09 18:46:26 +010076 subtype Inode_Index is Inode_0_Index range 2 .. Inode_0_Index'Last;
Nico Huber26f71832023-12-05 16:26:56 +010077 subtype Inode_Size is Positive range 128 .. Positive (Unsigned_16'Last);
Nico Huber7eb56922024-01-10 17:22:54 +010078 subtype Group_Desc_Size is Positive range 32 .. 2 ** 15; -- power-of-2 that fits in 16 bits
Nico Huber26f71832023-12-05 16:26:56 +010079
Nico Huber022e2262023-12-15 23:15:17 +010080 type Inode_Type is (Dir, Regular, Link, Fast_Link);
81 type Inode_Length is range 0 .. 2 ** 46;
82
Nico Huber33f6d952023-12-13 23:16:42 +010083 type Inode_Info is record
Nico Huber89d05942023-12-18 12:12:00 +010084 I : Inode_Index := Inode_Index'First;
Nico Huber022e2262023-12-15 23:15:17 +010085 Mode : Inode_Type := Inode_Type'First;
86 Size : Inode_Length := 0;
Nico Hubercdc03512023-12-13 23:32:54 +010087 Use_Extents : Boolean := False;
Nico Huber5a042fd2024-01-08 15:54:57 +010088 Inline : Inode_Extents := (others => 16#00#);
Nico Huber33f6d952023-12-13 23:16:42 +010089 end record;
90
Nico Huber925326e2024-01-09 18:46:26 +010091 type Group_Index is new Inode_0_Index;
Nico Huberecafb8f2024-01-09 15:45:49 +010092 subtype Group_In_Block_Count is Group_Index
Nico Huber7eb56922024-01-10 17:22:54 +010093 range 1 .. Group_Index (Block_Size'Last / Group_Desc_Size'First);
94 type Group_In_Block_Index is new Natural range 0 .. Natural (Group_In_Block_Count'Last - 1);
Nico Huberecafb8f2024-01-09 15:45:49 +010095
Nico Huber925326e2024-01-09 18:46:26 +010096 subtype Inode_In_Group_Count is Inode_0_Index range 1 .. Inode_0_Index'Last;
97 type Inode_In_Group_Index is new Inode_0_Index range 0 .. Inode_In_Group_Count'Last - 1;
Nico Huberecafb8f2024-01-09 15:45:49 +010098 subtype Inode_In_Block_Count is Inode_In_Group_Index
99 range 1 .. Inode_In_Group_Index (Block_Size'Last / Inode_Size'First);
100 type Inode_In_Block_Index is new Natural range 0 .. Natural (Inode_In_Block_Count'Last - 1);
101
Nico Huber52f4c8d2024-01-09 13:57:33 +0100102 type Mount_State is record
Nico Huber57dfbfb2023-12-13 23:24:16 +0100103 Part_Len : Partition_Length := 0;
Nico Huber39f086c2024-01-09 17:43:06 +0100104 First_Data_Block : Unsigned_32 := Unsigned_32'First;
Nico Huber700a4112024-01-08 15:50:09 +0100105 Block_Size_Bits : Log_Block_Size := Log_Block_Size'First;
106 Block_Size : Ext2.Block_Size := Ext2.Block_Size'First;
Nico Huber925326e2024-01-09 18:46:26 +0100107 Inodes_Per_Group : Inode_In_Group_Count := Inode_In_Group_Count'First;
Nico Huber57dfbfb2023-12-13 23:24:16 +0100108 Inode_Size : Ext2.Inode_Size := Ext2.Inode_Size'First;
Nico Huberecafb8f2024-01-09 15:45:49 +0100109 Inodes_Per_Block : Inode_In_Block_Count := Inode_In_Block_Count'First;
Nico Huber7eb56922024-01-10 17:22:54 +0100110 Group_Desc_Size : Ext2.Group_Desc_Size := Ext2.Group_Desc_Size'First;
111 Group_Desc_Per_Block : Group_In_Block_Count := Group_In_Block_Count'First;
Nico Huber57dfbfb2023-12-13 23:24:16 +0100112 Feature_Extents : Boolean := False;
113 Feature_64Bit : Boolean := False;
Nico Huber52f4c8d2024-01-09 13:57:33 +0100114 end record;
115
116 type Block_Cache is record
117 Logical : Cache_Label_Logical := (others => False);
118 Label : Cache_Label_Array := (others => 0);
119 Buffer : Cache_Buffer := (others => 16#00#);
120 end record;
121
122 type T is record
123 Static : Mount_State := (others => <>);
124 S : State;
125 Inode : Inode_Info := (others => <>);
126 Cur_Dir : Inode_Index := Inode_Index'First;
127 Cache : Block_Cache := (others => <>);
Nico Huber57d3a852023-12-04 15:42:40 +0100128 end record;
Nico Huber1d7727f2023-11-30 15:58:46 +0100129
Thomas Heijligen5c43abc2023-12-11 15:24:36 +0000130end FILO.FS.Ext2;