| 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 which fits at least one ext2 block. If a lower |
| -- block size is encountered (likely), we partition the cache into up |
| -- to 64 1KiB blocks. |
| -- Cache entries can be used for blocks that map logical block offets |
| -- to physical ones. Then we note the first logical block offset mapped |
| -- by the cached block. |
| subtype Block_Cache_Index is Natural range 0 .. 63; |
| 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; |