blob: 7c1e467d4ada3cad4fdc0349d46f7f8462045365 [file] [log] [blame]
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_Type : out FS.File_Type;
File_Name : in String;
In_Root : in Boolean;
Success : out Boolean)
with
Pre => Is_Mounted (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_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 Block_Size is Natural range 2 ** Log_Block_Size'First .. 2 ** Log_Block_Size'Last;
subtype Max_Block_Index is Index_Type range 0 .. 2 ** Log_Block_Size'Last - 1;
-- Extent physical addresses are 48 bits.
type FSBlock_Offset is new Block_Offset range 0 .. 2 ** 48 - 1;
-- Logical block addresses are 32 bits.
type FSBlock_Logical is new Block_Offset range 0 .. 2 ** 32 - 1;
-- 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. Otherwise, we use their physical offset.
type Cache_Label is new Unsigned_64;
subtype Block_Cache_Index is Natural range 0 .. 63;
type Cache_Label_Logical is array (Block_Cache_Index) of Boolean;
type Cache_Label_Array is array (Block_Cache_Index) of Cache_Label;
subtype Cache_Buffer is Buffer_Type (Max_Block_Index);
-- Same as the 12 direct + 3 indirect blocks times 4B:
subtype Inode_Extents_Index is Natural range 0 .. 59;
subtype Inode_Extents is Buffer_Type (Inode_Extents_Index)
with
Object_Size => (Inode_Extents_Index'Last + 1) * 8;
type Inode_Index is new Unsigned_32 range 2 .. Unsigned_32'Last;
subtype Inode_Size is Positive range 128 .. Positive (Unsigned_16'Last);
subtype Desc_Size is Positive range 32 .. 2 ** 15; -- power-of-2 that fits in 16 bits
type Inode_Type is (Dir, Regular, Link, Fast_Link);
type Inode_Length is range 0 .. 2 ** 46;
type Inode_Info is record
I : Inode_Index := Inode_Index'First;
Mode : Inode_Type := Inode_Type'First;
Size : Inode_Length := 0;
Use_Extents : Boolean := False;
Inline : Inode_Extents := (others => 16#00#);
end record;
type Mount_State is record
Part_Len : Partition_Length := 0;
First_Data_Block : FSBlock_Offset := 0;
Block_Size_Bits : Log_Block_Size := Log_Block_Size'First;
Block_Size : Ext2.Block_Size := Ext2.Block_Size'First;
Inodes_Per_Group : Inode_Index := Inode_Index'First;
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;
end record;
type Block_Cache is record
Logical : Cache_Label_Logical := (others => False);
Label : Cache_Label_Array := (others => 0);
Buffer : Cache_Buffer := (others => 16#00#);
end record;
type T is record
Static : Mount_State := (others => <>);
S : State;
Inode : Inode_Info := (others => <>);
Cur_Dir : Inode_Index := Inode_Index'First;
Cache : Block_Cache := (others => <>);
end record;
end FILO.FS.Ext2;