blob: 63f817e5b9deaa7bb0c7a9b89ae9ced968b896d1 [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;
21 File_Path : in String;
22 Success : out Boolean)
Nico Huber1d7727f2023-11-30 15:58:46 +010023 with
Nico Huber57d3a852023-12-04 15:42:40 +010024 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
42private
43 type State is (Unmounted, Mounted, File_Opened);
44
Nico Huber26f71832023-12-05 16:26:56 +010045 -- maximum block size is 64KiB (2^16):
46 subtype Log_Block_Size is Positive range 10 .. 16;
Nico Huber6623c982023-12-12 16:35:46 +010047 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 Huberfe897122023-12-12 21:33:36 +010053 -- 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 Huber6623c982023-12-12 16:35:46 +010060 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 Huber26f71832023-12-05 16:26:56 +010064
Nico Huberfffc8c12023-12-13 12:44:12 +010065 -- Same as the 12 direct + 3 indirect blocks times 4B:
66 subtype Inode_Extents_Index is Natural range 0 .. 59;
67
Nico Huber26f71832023-12-05 16:26:56 +010068 subtype Inode_Size is Positive range 128 .. Positive (Unsigned_16'Last);
Nico Hubercd1d5f72023-12-13 16:01:43 +010069 subtype Desc_Size is Positive range 32 .. 2 ** 15; -- power-of-2 that fits in 16 bits
Nico Huber26f71832023-12-05 16:26:56 +010070
Nico Huber57d3a852023-12-04 15:42:40 +010071 type T is record
72 S : State;
Nico Huber26f71832023-12-05 16:26:56 +010073 Part_Len : Partition_Length := 0;
Nico Hubercd1d5f72023-12-13 16:01:43 +010074 First_Data_Block : FSBlock_Offset := 0;
Nico Huber26f71832023-12-05 16:26:56 +010075 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 Huber6623c982023-12-12 16:35:46 +010081 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 Huberfffc8c12023-12-13 12:44:12 +010085 Inode_Extents : Buffer_Type (Inode_Extents_Index) := (others => 16#00#);
Nico Huber6623c982023-12-12 16:35:46 +010086 Block_Cache_Index : Block_Cache_Type := (others => 0);
87 Block_Cache : Buffer_Type (Max_Block_Index) := (others => 16#00#);
Nico Huber57d3a852023-12-04 15:42:40 +010088 end record;
Nico Huber1d7727f2023-11-30 15:58:46 +010089
Thomas Heijligen5c43abc2023-12-11 15:24:36 +000090end FILO.FS.Ext2;