blob: 90c1ae6d4f8d567832093cc8ee7f2d3f8063f472 [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_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;