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; |
| 21 | File_Path : in String; |
| 22 | Success : out Boolean) |
Nico Huber | 1d7727f | 2023-11-30 15:58:46 +0100 | [diff] [blame] | 23 | with |
Nico Huber | 57d3a85 | 2023-12-04 15:42:40 +0100 | [diff] [blame] | 24 | Pre => Is_Mounted (State) and not Is_Open (State), |
| 25 | Post => Success = Is_Open (State); |
| 26 | |
| 27 | procedure Close (State : in out T) |
| 28 | with |
| 29 | Pre => Is_Open (State), |
| 30 | Post => Is_Mounted (State); |
| 31 | |
| 32 | procedure Read |
| 33 | (State : in out T; |
| 34 | File_Len : in File_Length; |
| 35 | File_Pos : in out File_Offset; |
| 36 | Buf : out Buffer_Type; |
| 37 | Len : out Natural) |
| 38 | with |
| 39 | Pre => Is_Open (State), |
| 40 | Post => Is_Open (State); |
| 41 | |
| 42 | private |
| 43 | type State is (Unmounted, Mounted, File_Opened); |
| 44 | |
Nico Huber | 26f7183 | 2023-12-05 16:26:56 +0100 | [diff] [blame] | 45 | -- maximum block size is 64KiB (2^16): |
| 46 | subtype Log_Block_Size is Positive range 10 .. 16; |
Nico Huber | 6623c98 | 2023-12-12 16:35:46 +0100 | [diff] [blame] | 47 | subtype Max_Block_Index is Index_Type range 0 .. 2 ** Log_Block_Size'Last - 1; |
| 48 | |
| 49 | -- Minimum ext2 block size is 1KiB (two 512B blocks) |
| 50 | type FSBlock_Offset is new Block_Offset range 0 .. Block_Offset'Last / 2; |
| 51 | type FSBlock_Logical is new Block_Offset range 0 .. Block_Offset'Last / 2; |
| 52 | |
Nico Huber | fe89712 | 2023-12-12 21:33:36 +0100 | [diff] [blame] | 53 | -- We use a 64KiB cache which fits at least one ext2 block. If a lower |
| 54 | -- block size is encountered (likely), we partition the cache into up |
| 55 | -- to 64 1KiB blocks. |
| 56 | -- Cache entries can be used for blocks that map logical block offets |
| 57 | -- to physical ones. Then we note the first logical block offset mapped |
| 58 | -- by the cached block. |
| 59 | subtype Block_Cache_Index is Natural range 0 .. 63; |
Nico Huber | 6623c98 | 2023-12-12 16:35:46 +0100 | [diff] [blame] | 60 | type Block_Cache_Type is array (Block_Cache_Index) of FSBlock_Logical; |
| 61 | |
| 62 | Direct_Blocks : constant := 12; |
| 63 | type Direct_Blocks_Array is array (Natural range 0 .. Direct_Blocks - 1) of Unsigned_32; |
Nico Huber | 26f7183 | 2023-12-05 16:26:56 +0100 | [diff] [blame] | 64 | |
Nico Huber | fffc8c1 | 2023-12-13 12:44:12 +0100 | [diff] [blame] | 65 | -- Same as the 12 direct + 3 indirect blocks times 4B: |
| 66 | subtype Inode_Extents_Index is Natural range 0 .. 59; |
| 67 | |
Nico Huber | 26f7183 | 2023-12-05 16:26:56 +0100 | [diff] [blame] | 68 | subtype Inode_Size is Positive range 128 .. Positive (Unsigned_16'Last); |
Nico Huber | cd1d5f7 | 2023-12-13 16:01:43 +0100 | [diff] [blame^] | 69 | 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] | 70 | |
Nico Huber | 57d3a85 | 2023-12-04 15:42:40 +0100 | [diff] [blame] | 71 | type T is record |
| 72 | S : State; |
Nico Huber | 26f7183 | 2023-12-05 16:26:56 +0100 | [diff] [blame] | 73 | Part_Len : Partition_Length := 0; |
Nico Huber | cd1d5f7 | 2023-12-13 16:01:43 +0100 | [diff] [blame^] | 74 | First_Data_Block : FSBlock_Offset := 0; |
Nico Huber | 26f7183 | 2023-12-05 16:26:56 +0100 | [diff] [blame] | 75 | Block_Size_Bits : Log_Block_Size := 10; |
| 76 | Inodes_Per_Group : Positive := 1; |
| 77 | Inode_Size : Ext2.Inode_Size := Ext2.Inode_Size'First; |
| 78 | Desc_Size : Ext2.Desc_Size := Ext2.Desc_Size'First; |
| 79 | Feature_Extents : Boolean := False; |
| 80 | Feature_64Bit : Boolean := False; |
Nico Huber | 6623c98 | 2023-12-12 16:35:46 +0100 | [diff] [blame] | 81 | Direct_Blocks : Direct_Blocks_Array := (others => 0); |
| 82 | Indirect_Block : Unsigned_32 := 0; |
| 83 | Double_Indirect : Unsigned_32 := 0; |
| 84 | Triple_Indirect : Unsigned_32 := 0; |
Nico Huber | fffc8c1 | 2023-12-13 12:44:12 +0100 | [diff] [blame] | 85 | Inode_Extents : Buffer_Type (Inode_Extents_Index) := (others => 16#00#); |
Nico Huber | 6623c98 | 2023-12-12 16:35:46 +0100 | [diff] [blame] | 86 | Block_Cache_Index : Block_Cache_Type := (others => 0); |
| 87 | Block_Cache : Buffer_Type (Max_Block_Index) := (others => 16#00#); |
Nico Huber | 57d3a85 | 2023-12-04 15:42:40 +0100 | [diff] [blame] | 88 | end record; |
Nico Huber | 1d7727f | 2023-11-30 15:58:46 +0100 | [diff] [blame] | 89 | |
Thomas Heijligen | 5c43abc | 2023-12-11 15:24:36 +0000 | [diff] [blame] | 90 | end FILO.FS.Ext2; |