Thomas Heijligen | 5c43abc | 2023-12-11 15:24:36 +0000 | [diff] [blame] | 1 | package FILO.FS.Ext2 is |
Nico Huber | 1d7727f | 2023-11-30 15:58:46 +0100 | [diff] [blame] | 2 | |
Nico Huber | 57d3a85 | 2023-12-04 15:42:40 +0100 | [diff] [blame] | 3 | type T is private; |
Nico Huber | 1d7727f | 2023-11-30 15:58:46 +0100 | [diff] [blame] | 4 | |
Nico Huber | 57d3a85 | 2023-12-04 15:42:40 +0100 | [diff] [blame] | 5 | function Is_Mounted (State : T) return Boolean; |
| 6 | function Is_Open (State : T) return Boolean |
Nico Huber | 1d7727f | 2023-11-30 15:58:46 +0100 | [diff] [blame] | 7 | with |
Nico Huber | 57d3a85 | 2023-12-04 15:42:40 +0100 | [diff] [blame] | 8 | Post => (if Is_Open'Result then Is_Mounted (State)); |
Nico Huber | 1d7727f | 2023-11-30 15:58:46 +0100 | [diff] [blame] | 9 | |
Nico Huber | 57d3a85 | 2023-12-04 15:42:40 +0100 | [diff] [blame] | 10 | procedure Mount |
| 11 | (State : in out T; |
| 12 | Part_Len : in Partition_Length; |
| 13 | Success : out Boolean) |
Nico Huber | 1d7727f | 2023-11-30 15:58:46 +0100 | [diff] [blame] | 14 | with |
Nico Huber | 57d3a85 | 2023-12-04 15:42:40 +0100 | [diff] [blame] | 15 | Pre => not Is_Mounted (State), |
| 16 | Post => Success = Is_Mounted (State); |
Nico Huber | 1d7727f | 2023-11-30 15:58:46 +0100 | [diff] [blame] | 17 | |
Nico Huber | 57d3a85 | 2023-12-04 15:42:40 +0100 | [diff] [blame] | 18 | procedure Open |
| 19 | (State : in out T; |
| 20 | File_Len : out File_Length; |
Nico Huber | b1cb2d3 | 2023-12-17 01:45:47 +0100 | [diff] [blame] | 21 | File_Type : out FS.File_Type; |
| 22 | File_Name : in String; |
| 23 | In_Root : in Boolean; |
Nico Huber | 57d3a85 | 2023-12-04 15:42:40 +0100 | [diff] [blame] | 24 | Success : out Boolean) |
Nico Huber | 1d7727f | 2023-11-30 15:58:46 +0100 | [diff] [blame] | 25 | with |
Nico Huber | b1cb2d3 | 2023-12-17 01:45:47 +0100 | [diff] [blame] | 26 | Pre => Is_Mounted (State), |
Nico Huber | 57d3a85 | 2023-12-04 15:42:40 +0100 | [diff] [blame] | 27 | 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 Huber | 57d3a85 | 2023-12-04 15:42:40 +0100 | [diff] [blame] | 36 | 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 | |
| 43 | private |
| 44 | type State is (Unmounted, Mounted, File_Opened); |
| 45 | |
Nico Huber | 26f7183 | 2023-12-05 16:26:56 +0100 | [diff] [blame] | 46 | -- maximum block size is 64KiB (2^16): |
| 47 | subtype Log_Block_Size is Positive range 10 .. 16; |
Nico Huber | 700a411 | 2024-01-08 15:50:09 +0100 | [diff] [blame] | 48 | subtype Block_Size is Natural range 2 ** Log_Block_Size'First .. 2 ** Log_Block_Size'Last; |
Nico Huber | 6623c98 | 2023-12-12 16:35:46 +0100 | [diff] [blame] | 49 | subtype Max_Block_Index is Index_Type range 0 .. 2 ** Log_Block_Size'Last - 1; |
| 50 | |
Nico Huber | 5a042fd | 2024-01-08 15:54:57 +0100 | [diff] [blame] | 51 | -- 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 Huber | 6623c98 | 2023-12-12 16:35:46 +0100 | [diff] [blame] | 55 | |
Nico Huber | fe89712 | 2023-12-12 21:33:36 +0100 | [diff] [blame] | 56 | -- 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 Huber | 57dfbfb | 2023-12-13 23:24:16 +0100 | [diff] [blame] | 61 | -- by the cached block. Otherwise, we use their physical offset. |
| 62 | type Cache_Label is new Unsigned_64; |
Nico Huber | fe89712 | 2023-12-12 21:33:36 +0100 | [diff] [blame] | 63 | subtype Block_Cache_Index is Natural range 0 .. 63; |
Nico Huber | 57dfbfb | 2023-12-13 23:24:16 +0100 | [diff] [blame] | 64 | 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 Huber | 52f4c8d | 2024-01-09 13:57:33 +0100 | [diff] [blame] | 66 | subtype Cache_Buffer is Buffer_Type (Max_Block_Index); |
Nico Huber | 6623c98 | 2023-12-12 16:35:46 +0100 | [diff] [blame] | 67 | |
Nico Huber | fffc8c1 | 2023-12-13 12:44:12 +0100 | [diff] [blame] | 68 | -- Same as the 12 direct + 3 indirect blocks times 4B: |
| 69 | subtype Inode_Extents_Index is Natural range 0 .. 59; |
Nico Huber | 5a042fd | 2024-01-08 15:54:57 +0100 | [diff] [blame] | 70 | subtype Inode_Extents is Buffer_Type (Inode_Extents_Index) |
| 71 | with |
| 72 | Object_Size => (Inode_Extents_Index'Last + 1) * 8; |
Nico Huber | fffc8c1 | 2023-12-13 12:44:12 +0100 | [diff] [blame] | 73 | |
Nico Huber | 21d4202 | 2023-12-16 02:50:22 +0100 | [diff] [blame] | 74 | type Inode_Index is new Unsigned_32 range 2 .. Unsigned_32'Last; |
Nico Huber | 26f7183 | 2023-12-05 16:26:56 +0100 | [diff] [blame] | 75 | subtype Inode_Size is Positive range 128 .. Positive (Unsigned_16'Last); |
Nico Huber | cd1d5f7 | 2023-12-13 16:01:43 +0100 | [diff] [blame] | 76 | subtype Desc_Size is Positive range 32 .. 2 ** 15; -- power-of-2 that fits in 16 bits |
Nico Huber | 26f7183 | 2023-12-05 16:26:56 +0100 | [diff] [blame] | 77 | |
Nico Huber | 022e226 | 2023-12-15 23:15:17 +0100 | [diff] [blame] | 78 | type Inode_Type is (Dir, Regular, Link, Fast_Link); |
| 79 | type Inode_Length is range 0 .. 2 ** 46; |
| 80 | |
Nico Huber | 33f6d95 | 2023-12-13 23:16:42 +0100 | [diff] [blame] | 81 | type Inode_Info is record |
Nico Huber | 89d0594 | 2023-12-18 12:12:00 +0100 | [diff] [blame] | 82 | I : Inode_Index := Inode_Index'First; |
Nico Huber | 022e226 | 2023-12-15 23:15:17 +0100 | [diff] [blame] | 83 | Mode : Inode_Type := Inode_Type'First; |
| 84 | Size : Inode_Length := 0; |
Nico Huber | cdc0351 | 2023-12-13 23:32:54 +0100 | [diff] [blame] | 85 | Use_Extents : Boolean := False; |
Nico Huber | 5a042fd | 2024-01-08 15:54:57 +0100 | [diff] [blame] | 86 | Inline : Inode_Extents := (others => 16#00#); |
Nico Huber | 33f6d95 | 2023-12-13 23:16:42 +0100 | [diff] [blame] | 87 | end record; |
| 88 | |
Nico Huber | 52f4c8d | 2024-01-09 13:57:33 +0100 | [diff] [blame] | 89 | type Mount_State is record |
Nico Huber | 57dfbfb | 2023-12-13 23:24:16 +0100 | [diff] [blame] | 90 | Part_Len : Partition_Length := 0; |
| 91 | First_Data_Block : FSBlock_Offset := 0; |
Nico Huber | 700a411 | 2024-01-08 15:50:09 +0100 | [diff] [blame] | 92 | Block_Size_Bits : Log_Block_Size := Log_Block_Size'First; |
| 93 | Block_Size : Ext2.Block_Size := Ext2.Block_Size'First; |
Nico Huber | 21d4202 | 2023-12-16 02:50:22 +0100 | [diff] [blame] | 94 | Inodes_Per_Group : Inode_Index := Inode_Index'First; |
Nico Huber | 57dfbfb | 2023-12-13 23:24:16 +0100 | [diff] [blame] | 95 | 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 Huber | 52f4c8d | 2024-01-09 13:57:33 +0100 | [diff] [blame] | 99 | 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 Huber | 57d3a85 | 2023-12-04 15:42:40 +0100 | [diff] [blame] | 113 | end record; |
Nico Huber | 1d7727f | 2023-11-30 15:58:46 +0100 | [diff] [blame] | 114 | |
Thomas Heijligen | 5c43abc | 2023-12-11 15:24:36 +0000 | [diff] [blame] | 115 | end FILO.FS.Ext2; |