ext2: Adjust inode version of Open() to ease proof
diff --git a/src/filo-fs-ext2.adb b/src/filo-fs-ext2.adb
index 0d3df60..c0ced37 100644
--- a/src/filo-fs-ext2.adb
+++ b/src/filo-fs-ext2.adb
@@ -76,8 +76,8 @@
declare
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
- Static.Inodes_Per_Group := Inode_Index (S_Inodes_Per_Group);
+ if S_Inodes_Per_Group in 1 .. Unsigned_32'Last then
+ Static.Inodes_Per_Group := Inode_In_Group_Count (S_Inodes_Per_Group);
else
Success := False;
return;
@@ -127,12 +127,13 @@
Success := False;
return;
end if;
+ pragma Assert (Static.Block_Size / Static.Desc_Size <= Natural (Group_In_Block_Count'Last));
end;
Static.Feature_64Bit := Static.Feature_64Bit and Static.Desc_Size >= 64;
else
Static.Desc_Size := Desc_Size'First;
end if;
- Static.Desc_Per_Block := Group_Index (Static.Block_Size / Static.Desc_Size);
+ Static.Desc_Per_Block := Group_In_Block_Count (Static.Block_Size / Static.Desc_Size);
end;
pragma Assert_And_Cut (Success);
@@ -620,36 +621,35 @@
-- Group deserialization
subtype Group_Off is Natural range 0 .. Desc_Size'Last;
- function Group_Byte_Offset (Idx : Group_Index; Off : Group_Off) return Natural
+ function Group_Byte_Offset (Idx : Desc_In_Block_Index; Off : Group_Off) return Natural
is
(Natural (Idx) * Static.Desc_Size + Off);
- function Group_Inode_Table (Buf : Buffer_Type; Idx : Group_Index) return FSBlock_Offset
+ function Group_Inode_Table (Buf : Buffer_Type; Idx : Desc_In_Block_Index) return Unsigned_64
is
- (FSBlock_Offset (
- (if Static.Feature_64Bit
+ ((if Static.Feature_64Bit
then Shift_Left (Unsigned_64 (Read_LE32 (Buf, Group_Byte_Offset (Idx, 40))), 32)
else 0)
or
- Unsigned_64 (Read_LE32 (Buf, Group_Byte_Offset (Idx, 8)))))
+ Unsigned_64 (Read_LE32 (Buf, Group_Byte_Offset (Idx, 8))))
with
- Pre => Buf'Length >= Group_Byte_Offset (Idx, 44);
+ Pre => Buf'Length >= Group_Byte_Offset (Idx, (if Static.Feature_64Bit then 44 else 12));
------------------------
-- Inode deserialization
subtype Inode_Off is Natural range 0 .. Inode_Size'Last;
- function Inode_Byte_Offset (Idx : Inode_Index; Off : Inode_Off) return Natural
+ function Inode_Byte_Offset (Idx : Inode_In_Block_Index; Off : Inode_Off) return Natural
is
(Natural (Idx) * Static.Inode_Size + Off);
- function Inode_Mode (Buf : Buffer_Type; Idx : Inode_Index) return Unsigned_16
+ function Inode_Mode (Buf : Buffer_Type; Idx : Inode_In_Block_Index) return Unsigned_16
is
(Read_LE16 (Buf, Inode_Byte_Offset (Idx, 0)))
with
Pre => Buf'Length >= Inode_Byte_Offset (Idx, 2);
- function Inode_Size (Buf : Buffer_Type; Idx : Inode_Index; Mode : Inode_Type) return Unsigned_64
+ function Inode_Size (Buf : Buffer_Type; Idx : Inode_In_Block_Index; Mode : Inode_Type) return Unsigned_64
is
((if Mode = Regular
then Shift_Left (Unsigned_64 (Read_LE32 (Buf, Inode_Byte_Offset (Idx, 108))), 32)
@@ -658,19 +658,19 @@
with
Pre => Buf'Length >= Inode_Byte_Offset (Idx, 112);
- function Inode_Blocks (Buf : Buffer_Type; Idx : Inode_Index) return Unsigned_32
+ function Inode_Blocks (Buf : Buffer_Type; Idx : Inode_In_Block_Index) return Unsigned_32
is
(Read_LE32 (Buf, Inode_Byte_Offset (Idx, 28)))
with
Pre => Buf'Length >= Inode_Byte_Offset (Idx, 32);
- function Inode_Flags (Buf : Buffer_Type; Idx : Inode_Index) return Unsigned_32
+ function Inode_Flags (Buf : Buffer_Type; Idx : Inode_In_Block_Index) return Unsigned_32
is
(Read_LE32 (Buf, Inode_Byte_Offset (Idx, 32)))
with
Pre => Buf'Length >= Inode_Byte_Offset (Idx, 36);
- function Inode_File_ACL (Buf : Buffer_Type; Idx : Inode_Index) return Unsigned_32
+ function Inode_File_ACL (Buf : Buffer_Type; Idx : Inode_In_Block_Index) return Unsigned_32
is
(Read_LE32 (Buf, Inode_Byte_Offset (Idx, 104)))
with
@@ -685,26 +685,36 @@
(Static => Static,
Cache => State.Cache,
Phys => Desc_Block,
- Level => Natural'Min (Natural (Group / Static.Desc_Per_Block), Block_Cache_Index'Last),
+ Level => Natural (Group_Index'Min (Group / Static.Desc_Per_Block,
+ Group_Index (Block_Cache_Index'Last))),
Cache_Start => Cache_Start,
Cache_End => Cache_End,
Success => Success);
if not Success then
return;
end if;
+ pragma Assert_And_Cut (Cache_End = Cache_Start + Static.Block_Size - 1);
declare
Desc : constant Desc_In_Block_Index := Desc_In_Block_Index (Group mod Static.Desc_Per_Block);
Inode_In_Group : constant Inode_In_Group_Index :=
Inode_In_Group_Index ((Inode - 1) mod Static.Inodes_Per_Group);
- Inode_Block : constant FSBlock_Offset :=
- Group_Inode_Table (Cache (Cache_Start .. Cache_End), Group) +
- FSBlock_Offset (Inode_In_Group / Static.Inodes_Per_Block);
+ First_Table_Block : constant Unsigned_64 := Group_Inode_Table (Cache (Cache_Start .. Cache_End), Desc);
+ Block_Offset : constant Unsigned_64 := Unsigned_64 (Inode_In_Group / Static.Inodes_Per_Block);
begin
+ if First_Table_Block < Unsigned_64 (Static.First_Data_Block) or
+ First_Table_Block > Unsigned_64 (FSBlock_Offset'Last) - Block_Offset
+ then
+ Success := False;
+ return;
+ end if;
+ pragma Assert_And_Cut
+ (First_Table_Block + Block_Offset in 0 .. Unsigned_64 (FSBlock_Offset'Last));
+
Cache_FSBlock
(Static => Static,
Cache => State.Cache,
- Phys => Inode_Block,
+ Phys => FSBlock_Offset (First_Table_Block + Block_Offset),
Level => Block_Cache_Index'Last,
Cache_Start => Cache_Start,
Cache_End => Cache_End,
@@ -719,7 +729,8 @@
S_IFREG : constant := 8#100000#;
S_IFLNK : constant := 8#120000#;
- Inode_In_Block : constant Inode_Index := Inode_Index (Inode_In_Group mod Static.Inodes_Per_Block);
+ Inode_In_Block : constant Inode_In_Block_Index :=
+ Inode_In_Block_Index (Inode_In_Group mod Static.Inodes_Per_Block);
I_Mode : constant Unsigned_16 :=
Inode_Mode (Cache (Cache_Start .. Cache_End), Inode_In_Block);
I_Flags : constant Unsigned_32 :=
diff --git a/src/filo-fs-ext2.ads b/src/filo-fs-ext2.ads
index bbf959b..6003198 100644
--- a/src/filo-fs-ext2.ads
+++ b/src/filo-fs-ext2.ads
@@ -71,7 +71,8 @@
with
Object_Size => (Inode_Extents_Index'Last + 1) * 8;
- type Inode_Index is new Unsigned_32 range 2 .. Unsigned_32'Last;
+ type Inode_0_Index is new Unsigned_32;
+ subtype Inode_Index is Inode_0_Index range 2 .. Inode_0_Index'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
@@ -86,12 +87,13 @@
Inline : Inode_Extents := (others => 16#00#);
end record;
- type Group_Index is new Natural range 0 .. Natural (Inode_Index'Last / 2);
+ type Group_Index is new Inode_0_Index;
subtype Group_In_Block_Count is Group_Index
range 1 .. Group_Index (Block_Size'Last / Desc_Size'First);
type Desc_In_Block_Index is new Natural range 0 .. Natural (Group_In_Block_Count'Last - 1);
- type Inode_In_Group_Index is new Natural range 0 .. Natural (Inode_Index'Last / 2);
+ subtype Inode_In_Group_Count is Inode_0_Index range 1 .. Inode_0_Index'Last;
+ type Inode_In_Group_Index is new Inode_0_Index range 0 .. Inode_In_Group_Count'Last - 1;
subtype Inode_In_Block_Count is Inode_In_Group_Index
range 1 .. Inode_In_Group_Index (Block_Size'Last / Inode_Size'First);
type Inode_In_Block_Index is new Natural range 0 .. Natural (Inode_In_Block_Count'Last - 1);
@@ -101,7 +103,7 @@
First_Data_Block : Unsigned_32 := Unsigned_32'First;
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;
+ Inodes_Per_Group : Inode_In_Group_Count := Inode_In_Group_Count'First;
Inode_Size : Ext2.Inode_Size := Ext2.Inode_Size'First;
Inodes_Per_Block : Inode_In_Block_Count := Inode_In_Block_Count'First;
Desc_Size : Ext2.Desc_Size := Ext2.Desc_Size'First;