| package FILO.FS.Ext2 is |
| |
| type T is private; |
| |
| function Is_Mounted (State : T) return Boolean; |
| function Is_Open (State : T) return Boolean |
| with |
| Post => (if Is_Open'Result then Is_Mounted (State)); |
| |
| procedure Mount |
| (State : in out T; |
| Part_Len : in Partition_Length; |
| Success : out Boolean) |
| with |
| Pre => not Is_Mounted (State), |
| Post => Success = Is_Mounted (State); |
| |
| procedure Open |
| (State : in out T; |
| File_Len : out File_Length; |
| File_Path : in String; |
| Success : out Boolean) |
| with |
| Pre => Is_Mounted (State) and not Is_Open (State), |
| Post => Success = Is_Open (State); |
| |
| procedure Close (State : in out T) |
| with |
| Pre => Is_Open (State), |
| Post => Is_Mounted (State); |
| |
| procedure Read |
| (State : in out T; |
| File_Len : in File_Length; |
| File_Pos : in out File_Offset; |
| Buf : out Buffer_Type; |
| Len : out Natural) |
| with |
| Pre => Is_Open (State), |
| Post => Is_Open (State); |
| |
| private |
| type State is (Unmounted, Mounted, File_Opened); |
| |
| -- maximum block size is 64KiB (2^16): |
| subtype Log_Block_Size is Positive range 10 .. 16; |
| subtype Max_Block_Index is Index_Type range 0 .. 2 ** Log_Block_Size'Last - 1; |
| |
| -- Minimum ext2 block size is 1KiB (two 512B blocks) |
| type FSBlock_Offset is new Block_Offset range 0 .. Block_Offset'Last / 2; |
| type FSBlock_Logical is new Block_Offset range 0 .. Block_Offset'Last / 2; |
| |
| -- We use a 64KiB cache. |
| -- * If that's the block size, only the `Any` entry is used. |
| -- * For a 32KiB block size, `Any` and `Last_Level` (for indirect block |
| -- lookups) are used. |
| -- * For smaller block sizes, the most common case, we cache four blocks. |
| -- For the `Any` entry, we note the logical block address (block offset |
| -- within a file). For the indirect entries, we note the *first* logical |
| -- block that they map. |
| type Block_Cache_Index is (Any, Last_Level, Second_Last_Level, First_Level); |
| type Block_Cache_Type is array (Block_Cache_Index) of FSBlock_Logical; |
| |
| Direct_Blocks : constant := 12; |
| type Direct_Blocks_Array is array (Natural range 0 .. Direct_Blocks - 1) of Unsigned_32; |
| |
| subtype Inode_Size is Positive range 128 .. Positive (Unsigned_16'Last); |
| subtype Desc_Size is Positive range 32 .. Positive (Unsigned_16'Last); |
| |
| type T is record |
| S : State; |
| Part_Len : Partition_Length := 0; |
| First_Data_Block : Block_Offset := 0; |
| Block_Size_Bits : Log_Block_Size := 10; |
| Inodes_Per_Group : Positive := 1; |
| Inode_Size : Ext2.Inode_Size := Ext2.Inode_Size'First; |
| Desc_Size : Ext2.Desc_Size := Ext2.Desc_Size'First; |
| Feature_Extents : Boolean := False; |
| Feature_64Bit : Boolean := False; |
| Direct_Blocks : Direct_Blocks_Array := (others => 0); |
| Indirect_Block : Unsigned_32 := 0; |
| Double_Indirect : Unsigned_32 := 0; |
| Triple_Indirect : Unsigned_32 := 0; |
| Block_Cache_Index : Block_Cache_Type := (others => 0); |
| Block_Cache : Buffer_Type (Max_Block_Index) := (others => 16#00#); |
| end record; |
| |
| end FILO.FS.Ext2; |