ext2: Further split our state record
To assist proving that the metadata doesn't change.
diff --git a/src/filo-fs-ext2.adb b/src/filo-fs-ext2.adb
index 4dcde30..deb2d21 100644
--- a/src/filo-fs-ext2.adb
+++ b/src/filo-fs-ext2.adb
@@ -39,6 +39,7 @@
Part_Len : in Partition_Length;
Success : out Boolean)
is
+ Static : Mount_State renames State.Static;
Super_Block : Buffer_Type (0 .. SUPERBLOCK_SIZE - 1) := (others => 0);
begin
if Part_Len < 2 * SUPERBLOCK_SIZE then
@@ -56,15 +57,15 @@
return;
end if;
- State.Part_Len := Part_Len;
- State.First_Data_Block := FSBlock_Offset (Read_LE32 (Super_Block, 5 * 4));
+ Static.Part_Len := Part_Len;
+ Static.First_Data_Block := FSBlock_Offset (Read_LE32 (Super_Block, 5 * 4));
declare
S_Log_Block_Size : constant Unsigned_32 := Read_LE32 (Super_Block, 6 * 4);
begin
if S_Log_Block_Size <= Unsigned_32 (Log_Block_Size'Last - 10) then
- State.Block_Size_Bits := Log_Block_Size (S_Log_Block_Size + 10);
- State.Block_Size := 2 ** Log_Block_Size (S_Log_Block_Size + 10);
+ Static.Block_Size_Bits := Log_Block_Size (S_Log_Block_Size + 10);
+ Static.Block_Size := 2 ** Log_Block_Size (S_Log_Block_Size + 10);
else
Success := False;
return;
@@ -75,7 +76,7 @@
S_Inodes_Per_Group : constant Unsigned_32 := Read_LE32 (Super_Block, 10 * 4);
begin
if S_Inodes_Per_Group in 2 .. Unsigned_32'Last then
- State.Inodes_Per_Group := Inode_Index (S_Inodes_Per_Group);
+ Static.Inodes_Per_Group := Inode_Index (S_Inodes_Per_Group);
else
Success := False;
return;
@@ -90,39 +91,39 @@
S_Inode_Size : constant Unsigned_16 := Read_LE16 (Super_Block, 22 * 4);
begin
if Natural (S_Inode_Size) in Inode_Size then
- State.Inode_Size := Inode_Size (S_Inode_Size);
+ Static.Inode_Size := Inode_Size (S_Inode_Size);
else
Success := False;
return;
end if;
end;
else
- State.Inode_Size := Inode_Size'First;
+ Static.Inode_Size := Inode_Size'First;
end if;
end;
declare
S_Feature_Incompat : constant Unsigned_32 := Read_LE32 (Super_Block, 24 * 4);
begin
- State.Feature_Extents := (S_Feature_Incompat and FEATURE_INCOMPAT_EXTENTS) /= 0;
- State.Feature_64Bit := (S_Feature_Incompat and FEATURE_INCOMPAT_64BIT) /= 0;
- if State.Feature_64Bit then
+ Static.Feature_Extents := (S_Feature_Incompat and FEATURE_INCOMPAT_EXTENTS) /= 0;
+ Static.Feature_64Bit := (S_Feature_Incompat and FEATURE_INCOMPAT_64BIT) /= 0;
+ if Static.Feature_64Bit then
declare
S_Desc_Size : constant Unsigned_16 := Read_LE16 (Super_Block, 63 * 4 + 2);
begin
if Natural (S_Desc_Size) in Desc_Size and
- Natural (S_Desc_Size) <= State.Block_Size and
+ Natural (S_Desc_Size) <= Static.Block_Size and
Is_Power_Of_2 (S_Desc_Size)
then
- State.Desc_Size := Desc_Size (S_Desc_Size);
+ Static.Desc_Size := Desc_Size (S_Desc_Size);
else
Success := False;
return;
end if;
end;
- State.Feature_64Bit := State.Feature_64Bit and State.Desc_Size >= 64;
+ Static.Feature_64Bit := Static.Feature_64Bit and Static.Desc_Size >= 64;
else
- State.Desc_Size := Desc_Size'First;
+ Static.Desc_Size := Desc_Size'First;
end if;
end;
@@ -149,7 +150,8 @@
end Read_FSBlock;
procedure Cache_FSBlock
- (State : in out T;
+ (Static : in Mount_State;
+ Cache : in out Block_Cache;
Phys : in FSBlock_Offset;
Level : in Block_Cache_Index;
Label : in Cache_Label;
@@ -158,50 +160,51 @@
Cache_End : out Max_Block_Index;
Success : out Boolean)
with
- Post => Cache_End = Cache_Start + State.Block_Size - 1
+ Post => Cache_End = Cache_Start + Static.Block_Size - 1
is
-- Limit cache usage depending on block size:
- Max_Level : constant Block_Cache_Index := Block_Size'Last / State.Block_Size - 1;
+ Max_Level : constant Block_Cache_Index := Block_Size'Last / Static.Block_Size - 1;
Cache_Level : constant Block_Cache_Index := Block_Cache_Index'Min (Level, Max_Level);
begin
- Cache_Start := Cache_Level * State.Block_Size;
- Cache_End := Cache_Start + State.Block_Size - 1;
- if State.Block_Cache_Logical (Cache_Level) = Logical and
- State.Block_Cache_Label (Cache_Level) = Label
+ Cache_Start := Cache_Level * Static.Block_Size;
+ Cache_End := Cache_Start + Static.Block_Size - 1;
+ if Cache.Logical (Cache_Level) = Logical and
+ Cache.Label (Cache_Level) = Label
then
Success := True;
else
Read_FSBlock
- (Buf => State.Block_Cache (Cache_Start .. Cache_End),
+ (Buf => Cache.Buffer (Cache_Start .. Cache_End),
FSBlock => Phys,
- Part_Len => State.Part_Len,
+ Part_Len => Static.Part_Len,
Success => Success);
- State.Block_Cache_Logical (Cache_Level) := Logical;
- State.Block_Cache_Label (Cache_Level) := Label;
+ Cache.Logical (Cache_Level) := Logical; -- FIXME: Level needs to be part of Label
+ Cache.Label (Cache_Level) := Label;
end if;
end Cache_FSBlock;
procedure Cache_FSBlock
- (State : in out T;
+ (Static : in Mount_State;
+ Cache : in out Block_Cache;
Phys : in FSBlock_Offset;
Level : in Block_Cache_Index;
Cache_Start : out Max_Block_Index;
Cache_End : out Max_Block_Index;
Success : out Boolean)
with
- Post => Cache_End = Cache_Start + State.Block_Size - 1
+ Post => Cache_End = Cache_Start + Static.Block_Size - 1
is
begin
- Cache_FSBlock (State, Phys, Level, Cache_Label (Phys),
+ Cache_FSBlock (Static, Cache, Phys, Level, Cache_Label (Phys),
False, Cache_Start, Cache_End, Success);
end Cache_FSBlock;
- procedure Reset_Cache_Logical (State : in out T) is
+ procedure Reset_Cache_Logical (Cache : in out Block_Cache) is
begin
for I in Block_Cache_Index loop
- if State.Block_Cache_Logical (I) then
- State.Block_Cache_Logical (I) := False;
- State.Block_Cache_Label (I) := 0;
+ if Cache.Logical (I) then
+ Cache.Logical (I) := False;
+ Cache.Label (I) := 0;
end if;
end loop;
end Reset_Cache_Logical;
@@ -212,6 +215,8 @@
Physical : out FSBlock_Offset;
Success : out Boolean)
is
+ Static : constant Mount_State := State.Static;
+
Direct_Blocks : constant := 12;
type Direct_Blocks_Array is array (Natural range 0 .. Direct_Blocks - 1) of Unsigned_32;
type Inode_Blocks is record
@@ -225,7 +230,7 @@
function I_Blocks is new Ada.Unchecked_Conversion (Inode_Extents, Inode_Blocks);
function I_Blocks (State : T) return Inode_Blocks is (I_Blocks (State.Inode.Inline));
- Addr_Per_Block : constant FSBlock_Logical := FSBlock_Logical (State.Block_Size / 4);
+ Addr_Per_Block : constant FSBlock_Logical := FSBlock_Logical (Static.Block_Size / 4);
Max_Addr_Per_Block : constant FSBlock_Logical := FSBlock_Logical (Block_Size'Last / 4);
type Addr_In_Block_Range is range 0 .. Max_Addr_Per_Block - 1;
@@ -238,13 +243,14 @@
Success : out Boolean)
with
Pre =>
- Addr_Per_Block = FSBlock_Logical (State.Block_Size / 4) and
+ Addr_Per_Block = FSBlock_Logical (Static.Block_Size / 4) and
FSBlock_Logical (Addr_In_Block) < Addr_Per_Block
is
Cache_Start, Cache_End : Max_Block_Index;
begin
Cache_FSBlock
- (State => State,
+ (Static => Static,
+ Cache => State.Cache,
Phys => Indirect_Block_Phys,
Level => Level,
Label => Cache_Label (Logical_Off),
@@ -252,7 +258,7 @@
Cache_End => Cache_End,
Success => Success);
Next_Physical := FSBlock_Offset (Read_LE32
- (Buf => State.Block_Cache (Cache_Start .. Cache_End),
+ (Buf => State.Cache.Buffer (Cache_Start .. Cache_End),
Off => Natural (Addr_In_Block) * 4));
end Indirect_Block_Lookup;
@@ -346,6 +352,8 @@
Physical : out FSBlock_Offset;
Success : out Boolean)
is
+ Cache : Cache_Buffer renames State.Cache.Buffer;
+
-- Extent blocks always start with a 12B header and contain 12B entries.
-- Every entry starts with the number of the first logical block it
-- covers. Entries are sorted by this number.
@@ -376,7 +384,7 @@
Extent_Header_Magic : constant := 16#f03a#;
subtype Extent_Off is Natural range 0 .. Extent_Header_Size;
subtype Extent_Idx is Natural range 1 .. (Max_Block_Index'Last + 1) / Extent_Header_Size - 1;
- Dynamic_Max_Index : constant Extent_Idx := State.Block_Size / Extent_Header_Size - 1;
+ Dynamic_Max_Index : constant Extent_Idx := State.Static.Block_Size / Extent_Header_Size - 1;
subtype Extent_Depth is Natural range 0 .. 32;
function Extent_Byte_Offset (Idx : Extent_Idx; Off : Extent_Off) return Natural
@@ -476,12 +484,13 @@
Pre => Logical_Off <= Logical,
Post => (if Success then
Next <= Dynamic_Max_Index and then
- Cache_End = Cache_Start + State.Block_Size - 1 and then
- Extent_Logical (State.Block_Cache (Cache_Start .. Cache_End), Next) <= Logical)
+ Cache_End = Cache_Start + State.Static.Block_Size - 1 and then
+ Extent_Logical (Cache (Cache_Start .. Cache_End), Next) <= Logical)
is
begin
Cache_FSBlock
- (State => State,
+ (Static => State.Static,
+ Cache => State.Cache,
Phys => Current,
Level => Depth,
Label => Cache_Label (Logical_Off),
@@ -494,14 +503,11 @@
end if;
declare
- Hdr_Magic : constant Unsigned_16 :=
- Header_Magic (State.Block_Cache (Cache_Start .. Cache_End));
- Hdr_Entries : constant Natural :=
- Header_Entries (State.Block_Cache (Cache_Start .. Cache_End));
- Hdr_Depth : constant Natural :=
- Header_Depth (State.Block_Cache (Cache_Start .. Cache_End));
+ Hdr_Magic : constant Unsigned_16 := Header_Magic (Cache (Cache_Start .. Cache_End));
+ Hdr_Entries : constant Natural := Header_Entries (Cache (Cache_Start .. Cache_End));
+ Hdr_Depth : constant Natural := Header_Depth (Cache (Cache_Start .. Cache_End));
First_Logical : constant FSBlock_Logical :=
- Extent_Logical (State.Block_Cache (Cache_Start .. Cache_End), 1);
+ Extent_Logical (Cache (Cache_Start .. Cache_End), 1);
begin
Success := Success and then
Hdr_Magic = Extent_Header_Magic and then
@@ -512,7 +518,7 @@
if not Success then
Next := 1;
else
- Next := Bin_Search (State.Block_Cache (Cache_Start .. Cache_End), Hdr_Entries);
+ Next := Bin_Search (Cache (Cache_Start .. Cache_End), Hdr_Entries);
end if;
end;
end Next_Ref;
@@ -565,13 +571,13 @@
end if;
exit when Depth = 0;
- Physical := Index_Physical (State.Block_Cache (Cache_Start .. Cache_End), Idx);
- Logical_Off := Index_Logical (State.Block_Cache (Cache_Start .. Cache_End), Idx);
+ Physical := Index_Physical (Cache (Cache_Start .. Cache_End), Idx);
+ Logical_Off := Index_Logical (Cache (Cache_Start .. Cache_End), Idx);
end loop;
- Physical := Extent_Physical (State.Block_Cache (Cache_Start .. Cache_End), Idx);
- Logical_Off := Extent_Logical (State.Block_Cache (Cache_Start .. Cache_End), Idx);
- Length := Extent_Length (State.Block_Cache (Cache_Start .. Cache_End), Idx);
+ Physical := Extent_Physical (Cache (Cache_Start .. Cache_End), Idx);
+ Logical_Off := Extent_Logical (Cache (Cache_Start .. Cache_End), Idx);
+ Length := Extent_Length (Cache (Cache_Start .. Cache_End), Idx);
end if;
Success :=
@@ -591,12 +597,15 @@
Pre => Is_Mounted (State) and not Is_Open (State),
Post => Success = Is_Open (State)
is
+ Static : Mount_State renames State.Static;
+ Cache : Cache_Buffer renames State.Cache.Buffer;
+
type Group_Index is new Natural;
subtype Desc_In_Block_Index is Group_Index
range 0 .. Group_Index (2 ** Log_Block_Size'Last / Desc_Size'First - 1);
- Inodes_Per_Block : constant Inode_Index := Inode_Index (State.Block_Size / State.Inode_Size);
- Desc_Per_Block : constant Group_Index := Group_Index (State.Block_Size / State.Desc_Size);
+ Inodes_Per_Block : constant Inode_Index := Inode_Index (Static.Block_Size / Static.Inode_Size);
+ Desc_Per_Block : constant Group_Index := Group_Index (Static.Block_Size / Static.Desc_Size);
------------------------
-- Group deserialization
@@ -604,12 +613,12 @@
subtype Group_Off is Natural range 0 .. Desc_Size'Last;
function Group_Byte_Offset (Idx : Group_Index; Off : Group_Off) return Natural
is
- (Natural (Idx) * State.Desc_Size + Off);
+ (Natural (Idx) * Static.Desc_Size + Off);
function Group_Inode_Table (Buf : Buffer_Type; Idx : Group_Index) return FSBlock_Offset
is
(FSBlock_Offset (
- (if State.Feature_64Bit
+ (if Static.Feature_64Bit
then Shift_Left (Unsigned_64 (Read_LE32 (Buf, Group_Byte_Offset (Idx, 40))), 32)
else 0)
or
@@ -623,7 +632,7 @@
subtype Inode_Off is Natural range 0 .. Inode_Size'Last;
function Inode_Byte_Offset (Idx : Inode_Index; Off : Inode_Off) return Natural
is
- (Natural (Idx) * State.Inode_Size + Off);
+ (Natural (Idx) * Static.Inode_Size + Off);
function Inode_Mode (Buf : Buffer_Type; Idx : Inode_Index) return Unsigned_16
is
@@ -658,13 +667,14 @@
with
Pre => Buf'Length >= Inode_Byte_Offset (Idx, 108);
- Group : constant Group_Index := Group_Index ((Inode - 1) / State.Inodes_Per_Group);
+ Group : constant Group_Index := Group_Index ((Inode - 1) / Static.Inodes_Per_Group);
Desc_Block : constant FSBlock_Offset :=
- 1 + State.First_Data_Block + FSBlock_Offset (Group / Desc_Per_Block);
+ 1 + Static.First_Data_Block + FSBlock_Offset (Group / Desc_Per_Block);
Cache_Start, Cache_End : Max_Block_Index;
begin
Cache_FSBlock
- (State => State,
+ (Static => Static,
+ Cache => State.Cache,
Phys => Desc_Block,
Level => Natural'Min (Natural (Group / Desc_Per_Block), Block_Cache_Index'Last),
Cache_Start => Cache_Start,
@@ -676,13 +686,14 @@
declare
Desc : constant Desc_In_Block_Index := Group mod Desc_Per_Block;
- Inode_In_Group : constant Inode_Index := (Inode - 1) mod State.Inodes_Per_Group;
+ Inode_In_Group : constant Inode_Index := (Inode - 1) mod Static.Inodes_Per_Group;
Inode_Block : constant FSBlock_Offset :=
- Group_Inode_Table (State.Block_Cache (Cache_Start .. Cache_End), Group) +
+ Group_Inode_Table (Cache (Cache_Start .. Cache_End), Group) +
FSBlock_Offset (Inode_In_Group / Inodes_Per_Block);
begin
Cache_FSBlock
- (State => State,
+ (Static => Static,
+ Cache => State.Cache,
Phys => Inode_Block,
Level => Block_Cache_Index'Last,
Cache_Start => Cache_Start,
@@ -700,9 +711,9 @@
Inode_In_Block : constant Inode_Index := Inode_In_Group mod Inodes_Per_Block;
I_Mode : constant Unsigned_16 :=
- Inode_Mode (State.Block_Cache (Cache_Start .. Cache_End), Inode_In_Block);
+ Inode_Mode (Cache (Cache_Start .. Cache_End), Inode_In_Block);
I_Flags : constant Unsigned_32 :=
- Inode_Flags (State.Block_Cache (Cache_Start .. Cache_End), Inode_In_Block);
+ Inode_Flags (Cache (Cache_Start .. Cache_End), Inode_In_Block);
begin
case I_Mode and S_IFMT is
when S_IFDIR => State.Inode.Mode := Dir;
@@ -713,12 +724,12 @@
if State.Inode.Mode = Link then
declare
I_File_ACL : constant Unsigned_32 := Inode_File_ACL (
- State.Block_Cache (Cache_Start .. Cache_End), Inode_In_Block);
+ Cache (Cache_Start .. Cache_End), Inode_In_Block);
I_Blocks : constant Unsigned_32 := Inode_Blocks (
- State.Block_Cache (Cache_Start .. Cache_End), Inode_In_Block);
+ Cache (Cache_Start .. Cache_End), Inode_In_Block);
begin
if (I_File_ACL = 0 and I_Blocks = 0) or
- (I_File_ACL /= 0 and I_Blocks = 2 ** (State.Block_Size_Bits - 9))
+ (I_File_ACL /= 0 and I_Blocks = 2 ** (Static.Block_Size_Bits - 9))
then
State.Inode.Mode := Fast_Link;
end if;
@@ -726,7 +737,7 @@
end if;
declare
I_Size : constant Unsigned_64 := Inode_Size (
- State.Block_Cache (Cache_Start .. Cache_End), Inode_In_Block, State.Inode.Mode);
+ Cache (Cache_Start .. Cache_End), Inode_In_Block, State.Inode.Mode);
begin
if I_Size <= Unsigned_64 (Inode_Length'Last) then
State.Inode.Size := Inode_Length (I_Size);
@@ -734,10 +745,10 @@
Success := False;
end if;
end;
- State.Inode.Use_Extents := State.Feature_Extents and (I_Flags and EXT4_EXTENTS_FL) /= 0;
- State.Inode.Inline := State.Block_Cache (Cache_Start + 40 .. Cache_Start + 100 - 1);
+ State.Inode.Use_Extents := Static.Feature_Extents and (I_Flags and EXT4_EXTENTS_FL) /= 0;
+ State.Inode.Inline := Cache (Cache_Start + 40 .. Cache_Start + 100 - 1);
State.Inode.I := Inode;
- Reset_Cache_Logical (State);
+ Reset_Cache_Logical (State.Cache);
State.S := File_Opened;
end;
end;
@@ -870,6 +881,9 @@
Buf : out Buffer_Type;
Len : out Natural)
is
+ Static : Mount_State renames State.Static;
+ Cache : Cache_Buffer renames State.Cache.Buffer;
+
Pos : Natural;
begin
if State.Inode.Mode = Fast_Link then
@@ -890,9 +904,9 @@
Pos := Buf'First;
while Pos <= Buf'Last and Inode_Length (File_Pos) < State.Inode.Size loop
declare
- In_Block : constant Max_Block_Index := Natural (File_Pos) mod State.Block_Size;
- Logical : constant FSBlock_Logical := FSBlock_Logical (File_Pos / File_Offset (State.Block_Size));
- In_Block_Space : constant Natural := Natural (State.Block_Size) - In_Block;
+ In_Block : constant Max_Block_Index := Natural (File_Pos) mod Static.Block_Size;
+ Logical : constant FSBlock_Logical := FSBlock_Logical (File_Pos / File_Offset (Static.Block_Size));
+ In_Block_Space : constant Natural := Natural (Static.Block_Size) - In_Block;
In_File_Space : constant Inode_Length := State.Inode.Size - Inode_Length (File_Pos);
In_Buf_Space : constant Natural := Buf'Last - Pos + 1;
Len_Here : Natural;
@@ -918,7 +932,8 @@
end if;
if Success then
Cache_FSBlock
- (State => State,
+ (Static => Static,
+ Cache => State.Cache,
Phys => Physical,
Level => Block_Cache_Index'Last,
Cache_Start => Cache_Start,
@@ -927,7 +942,7 @@
end if;
exit when not Success;
- Buf (Pos .. Last) := State.Block_Cache (
+ Buf (Pos .. Last) := Cache (
Cache_Start + In_Block .. Cache_Start + In_Block + Len_Here - 1);
File_Pos := File_Pos + File_Length (Len_Here);
Pos := Pos + Len_Here;