| -- Derived from GRUB -- GRand Unified Bootloader |
| -- Copyright (C) 1999, 2001, 2003 Free Software Foundation, Inc. |
| -- Copyright (C) 2023 secunet Security Networks AG |
| -- |
| -- This program is free software; you can redistribute it and/or modify |
| -- it under the terms of the GNU General Public License as published by |
| -- the Free Software Foundation; either version 2 of the License, or |
| -- (at your option) any later version. |
| |
| with Ada.Unchecked_Conversion; |
| with System; |
| with Interfaces; |
| with Interfaces.C; |
| |
| with FILO.Blockdev; |
| with FILO.FS.VFS; |
| |
| use Interfaces.C; |
| |
| package body FILO.FS.Ext2 is |
| |
| function Is_Mounted (State : T) return Boolean is (State.S >= Mounted); |
| function Is_Open (State : T) return Boolean is (State.S = File_Opened); |
| |
| -------------------------------------------------------------------------- |
| |
| SUPERBLOCK_SIZE : constant := 1024; |
| SUPERBLOCK_MAGIC : constant := 16#ef53#; |
| OLD_REV : constant := 0; |
| DYNAMIC_REV : constant := 1; |
| |
| FEATURE_INCOMPAT_EXTENTS : constant := 16#0040#; |
| FEATURE_INCOMPAT_64BIT : constant := 16#0080#; |
| |
| EXT4_EXTENTS_FL : constant := 16#8_0000#; |
| |
| procedure Mount |
| (State : in out T; |
| Part_Len : in Partition_Length; |
| Success : out Boolean) |
| is |
| Static : Mount_State renames State.Static; |
| Super_Block : Buffer_Type (0 .. 64 * 4 - 1); |
| begin |
| if Part_Len < 2 * SUPERBLOCK_SIZE then |
| Success := False; |
| return; |
| end if; |
| |
| Blockdev.Read (Super_Block, 1 * SUPERBLOCK_SIZE, Success); |
| if not Success then |
| return; |
| end if; |
| |
| if Read_LE16 (Super_Block, 14 * 4) /= 16#ef53# then |
| Success := False; |
| return; |
| end if; |
| |
| Static.Part_Len := Part_Len; |
| Static.First_Data_Block := 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 |
| 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; |
| end if; |
| end; |
| pragma Assert_And_Cut (Success and not Is_Mounted (State)); |
| |
| declare |
| S_Inodes_Per_Group : constant Unsigned_32 := Read_LE32 (Super_Block, 10 * 4); |
| begin |
| 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; |
| end if; |
| end; |
| |
| declare |
| S_Rev_Level : constant Unsigned_32 := Read_LE32 (Super_Block, 19 * 4); |
| begin |
| if S_Rev_Level >= DYNAMIC_REV then |
| declare |
| S_Inode_Size : constant Unsigned_16 := Read_LE16 (Super_Block, 22 * 4); |
| begin |
| if Natural (S_Inode_Size) in Inode_Size and then |
| Natural (S_Inode_Size) <= Static.Block_Size |
| then |
| Static.Inode_Size := Inode_Size (S_Inode_Size); |
| else |
| Success := False; |
| return; |
| end if; |
| pragma Assert (Static.Block_Size / Static.Inode_Size <= Natural (Inode_In_Block_Count'Last)); |
| end; |
| else |
| Static.Inode_Size := Inode_Size'First; |
| end if; |
| Static.Inodes_Per_Block := Inode_In_Block_Count (Static.Block_Size / Static.Inode_Size); |
| end; |
| pragma Assert_And_Cut (Success and not Is_Mounted (State)); |
| |
| declare |
| S_Feature_Incompat : constant Unsigned_32 := Read_LE32 (Super_Block, 24 * 4); |
| begin |
| 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 Group_Desc_Size and |
| Natural (S_Desc_Size) <= Static.Block_Size and |
| Is_Power_Of_2 (S_Desc_Size) |
| then |
| Static.Group_Desc_Size := Group_Desc_Size (S_Desc_Size); |
| else |
| Success := False; |
| return; |
| end if; |
| pragma Assert (Static.Block_Size / Static.Group_Desc_Size <= Natural (Group_In_Block_Count'Last)); |
| end; |
| Static.Feature_64Bit := Static.Feature_64Bit and Static.Group_Desc_Size >= 64; |
| else |
| Static.Group_Desc_Size := Group_Desc_Size'First; |
| end if; |
| Static.Group_Desc_Per_Block := Group_In_Block_Count (Static.Block_Size / Static.Group_Desc_Size); |
| end; |
| |
| State.S := Mounted; |
| end Mount; |
| |
| procedure Read_FSBlock |
| (Buf : in out Buffer_Type; |
| FSBlock : in FSBlock_Offset; |
| Part_Len : in Partition_Length; |
| Success : out Boolean) |
| with |
| Pre => Buf'Length in Block_Size |
| is |
| FSBlock_64 : constant Integer_64 := Integer_64 (FSBlock); |
| Block_Size : constant Integer_64 := Integer_64 (Buf'Length); |
| Max_Block_Offset : constant Integer_64 := Integer_64 (Part_Len) / Block_Size - 1; |
| begin |
| if FSBlock_64 > Max_Block_Offset then |
| Success := False; |
| return; |
| end if; |
| Blockdev.Read (Buf, Blockdev_Length (FSBlock_64 * Block_Size), Success); |
| end Read_FSBlock; |
| |
| procedure Cache_FSBlock |
| (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 + Static.Block_Size - 1 |
| is |
| -- Limit cache usage depending on block size: |
| 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 * Static.Block_Size; |
| Cache_End := Cache_Start + Static.Block_Size - 1; |
| if Cache.Phys (Cache_Level) = Phys then |
| Success := True; |
| else |
| Read_FSBlock |
| (Buf => Cache.Buffer (Cache_Start .. Cache_End), |
| FSBlock => Phys, |
| Part_Len => Static.Part_Len, |
| Success => Success); |
| Cache.Phys (Cache_Level) := Phys; |
| end if; |
| end Cache_FSBlock; |
| |
| procedure Ext2_Block_Map |
| (State : in out T; |
| Logical : in FSBlock_Logical; |
| Physical : out FSBlock_Offset; |
| Success : out Boolean) |
| with |
| Post => State.Static = State.Static'Old and State.S = State.S'Old |
| 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 |
| Direct_Blocks : Direct_Blocks_Array; |
| Indirect_Block : Unsigned_32; |
| Double_Indirect : Unsigned_32; |
| Triple_Indirect : Unsigned_32; |
| end record |
| with |
| Size => Inline_Extents'Length * 8, |
| Object_Size => Inline_Extents'Length * 8; |
| |
| function I_Blocks is new Ada.Unchecked_Conversion (Inline_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 (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; |
| |
| procedure Indirect_Block_Lookup |
| (Indirect_Block_Phys : in FSBlock_Offset; |
| Addr_In_Block : in Addr_In_Block_Range; |
| Level : in Block_Cache_Index; |
| Next_Physical : out FSBlock_Offset; |
| Success : out Boolean) |
| with |
| Pre => |
| Addr_Per_Block = FSBlock_Logical (Static.Block_Size / 4) and |
| FSBlock_Logical (Addr_In_Block) < Addr_Per_Block, |
| Post => State.Static = State.Static'Old and State.S = State.S'Old |
| is |
| Cache_Start, Cache_End : Max_Block_Index; |
| begin |
| if Indirect_Block_Phys = 0 then |
| Next_Physical := 0; |
| Success := True; |
| return; |
| end if; |
| |
| Cache_FSBlock |
| (Static => Static, |
| Cache => State.Cache, |
| Phys => Indirect_Block_Phys, |
| Level => Level, |
| Cache_Start => Cache_Start, |
| Cache_End => Cache_End, |
| Success => Success); |
| Next_Physical := FSBlock_Offset (Read_LE32 |
| (Buf => State.Cache.Buffer (Cache_Start .. Cache_End), |
| Off => Natural (Addr_In_Block) * 4)); |
| end Indirect_Block_Lookup; |
| |
| Logical_Rest : FSBlock_Logical := Logical; |
| |
| pragma Assert (Addr_Per_Block <= 2 ** 14); |
| begin |
| if Logical_Rest < Direct_Blocks then |
| Physical := FSBlock_Offset (I_Blocks (State).Direct_Blocks (Natural (Logical))); |
| Success := True; |
| return; |
| end if; |
| |
| Logical_Rest := Logical_Rest - Direct_Blocks; |
| if Logical_Rest < Addr_Per_Block then |
| Indirect_Block_Lookup |
| (Indirect_Block_Phys => FSBlock_Offset (I_Blocks (State).Indirect_Block), |
| Addr_In_Block => Addr_In_Block_Range (Logical_Rest), |
| Level => Block_Map_Cache_Level, |
| Next_Physical => Physical, |
| Success => Success); |
| return; |
| end if; |
| |
| Logical_Rest := Logical_Rest - Addr_Per_Block; |
| if Logical_Rest < Addr_Per_Block ** 2 then |
| Indirect_Block_Lookup |
| (Indirect_Block_Phys => FSBlock_Offset (I_Blocks (State).Double_Indirect), |
| Addr_In_Block => Addr_In_Block_Range ((Logical_Rest / Addr_Per_Block) mod Addr_Per_Block), |
| Level => Block_Map_Cache_Level + 1, |
| Next_Physical => Physical, |
| Success => Success); |
| if not Success then |
| return; |
| end if; |
| |
| Indirect_Block_Lookup |
| (Indirect_Block_Phys => Physical, |
| Addr_In_Block => Addr_In_Block_Range (Logical_Rest mod Addr_Per_Block), |
| Level => Block_Map_Cache_Level, |
| Next_Physical => Physical, |
| Success => Success); |
| return; |
| end if; |
| |
| Logical_Rest := Logical_Rest - Addr_Per_Block ** 2; |
| if Logical_Rest < Addr_Per_Block ** 3 then |
| Indirect_Block_Lookup |
| (Indirect_Block_Phys => FSBlock_Offset (I_Blocks (State).Triple_Indirect), |
| Addr_In_Block => Addr_In_Block_Range ((Logical_Rest / Addr_Per_Block ** 2) mod Addr_Per_Block), |
| Level => Block_Map_Cache_Level + 2, |
| Next_Physical => Physical, |
| Success => Success); |
| if not Success then |
| return; |
| end if; |
| |
| Indirect_Block_Lookup |
| (Indirect_Block_Phys => Physical, |
| Addr_In_Block => Addr_In_Block_Range ((Logical_Rest / Addr_Per_Block) mod Addr_Per_Block), |
| Level => Block_Map_Cache_Level + 1, |
| Next_Physical => Physical, |
| Success => Success); |
| if not Success then |
| return; |
| end if; |
| |
| Indirect_Block_Lookup |
| (Indirect_Block_Phys => Physical, |
| Addr_In_Block => Addr_In_Block_Range (Logical_Rest mod Addr_Per_Block), |
| Level => Block_Map_Cache_Level, |
| Next_Physical => Physical, |
| Success => Success); |
| return; |
| end if; |
| |
| -- Logical address was just too high. |
| Physical := 0; |
| Success := False; |
| end Ext2_Block_Map; |
| |
| procedure Extent_Block_Map |
| (State : in out T; |
| Logical : in FSBlock_Logical; |
| Physical : out FSBlock_Offset; |
| Success : out Boolean) |
| with |
| Post => State.Static = State.Static'Old and State.S = State.S'Old |
| 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. |
| -- Depth > 0 blocks have index entries, referencing further extent blocks. |
| -- Depth = 0 blocks have extent entries, referencing a contiguous range |
| -- of data blocks. |
| -- |
| -- +-----------------+ |
| -- .-> | Hdr depth=0 | |
| -- | +-----------------+ |
| -- | | Extent 0.. 12 | |
| -- +-------------+ | +-----------------+ |
| -- | Hdr depth=1 | | | Extent 13.. 13 | |
| -- +-------------+ | +-----------------+ |
| -- | Index 0 | --' | Extent 14..122 | |
| -- +-------------+ +-----------------+ |
| -- | Index 123 | --. |
| -- +-------------+ | +-----------------+ |
| -- `-> | Hdr depth=0 | |
| -- +-----------------+ |
| -- | Extent 123..125 | |
| -- +-----------------+ |
| -- | Extent 126..234 | |
| -- +-----------------+ |
| -- |
| |
| Extent_Header_Size : constant := 12; |
| Extent_Header_Magic : constant := 16#f30a#; |
| Initialized_Extent_Max_Len : constant := 2 ** 15; |
| 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.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 |
| is |
| (Idx * Extent_Header_Size + Off); |
| |
| function Header_Magic (Buf : Buffer_Type) return Unsigned_16 |
| is |
| (Read_LE16 (Buf, 0)) |
| with |
| Pre => Buf'Length >= 2; |
| |
| function Header_Entries (Buf : Buffer_Type) return Natural |
| is |
| (Natural (Read_LE16 (Buf, 2))) |
| with |
| Pre => Buf'Length >= 4; |
| |
| function Header_Depth (Buf : Buffer_Type) return Natural |
| is |
| (Natural (Read_LE16 (Buf, 6))) |
| with |
| Pre => Buf'Length >= 8; |
| |
| function Index_Logical (Buf : Buffer_Type; Idx : Extent_Idx) return FSBlock_Logical |
| is |
| (FSBlock_Logical (Read_LE32 (Buf, Extent_Byte_Offset (Idx, 0)))) |
| with |
| Pre => Buf'Length >= Extent_Byte_Offset (Idx, 4); |
| |
| function Index_Physical (Buf : Buffer_Type; Idx : Extent_Idx) return FSBlock_Offset |
| is |
| (FSBlock_Offset |
| (Shift_Left (Unsigned_64 (Read_LE16 (Buf, Extent_Byte_Offset (Idx, 8))), 32) or |
| Unsigned_64 (Read_LE32 (Buf, Extent_Byte_Offset (Idx, 4))))) |
| with |
| Pre => Buf'Length >= Extent_Byte_Offset (Idx, 10); |
| |
| function Extent_Logical (Buf : Buffer_Type; Idx : Extent_Idx) return FSBlock_Logical |
| renames Index_Logical; |
| |
| function Extent_Length (Buf : Buffer_Type; Idx : Extent_Idx) return FSBlock_Logical |
| is |
| (FSBlock_Logical (Read_LE16 (Buf, Extent_Byte_Offset (Idx, 4)))) |
| with |
| Pre => Buf'Length >= Extent_Byte_Offset (Idx, 6); |
| |
| function Extent_Physical (Buf : Buffer_Type; Idx : Extent_Idx) return FSBlock_Offset |
| is |
| (FSBlock_Offset |
| (Shift_Left (Unsigned_64 (Read_LE16 (Buf, Extent_Byte_Offset (Idx, 6))), 32) or |
| Unsigned_64 (Read_LE32 (Buf, Extent_Byte_Offset (Idx, 8))))) |
| with |
| Pre => Buf'Length >= Extent_Byte_Offset (Idx, 12); |
| |
| function Bin_Search (Buf : Buffer_Type; Refs : Extent_Idx) return Extent_Idx |
| with |
| Pre => |
| Buf'Length in 2 * Extent_Header_Size .. Max_Block_Index'Last and then |
| Refs in 1 .. Extent_Idx (Buf'Length / Extent_Header_Size - 1) and then |
| Extent_Logical (Buf, 1) <= Logical, |
| Post => |
| Bin_Search'Result in 1 .. Refs and |
| Extent_Logical (Buf, Bin_Search'Result) <= Logical |
| is |
| Left : Positive := 2; |
| Right : Extent_Idx := Refs; |
| begin |
| while Left <= Right loop |
| declare |
| Mid : constant Extent_Idx := (Left + Right) / 2; |
| Ext_Logical : constant FSBlock_Logical := Extent_Logical (Buf, Mid); |
| begin |
| if Logical < Ext_Logical then |
| Right := Mid - 1; |
| else |
| Left := Mid + 1; |
| end if; |
| pragma Loop_Invariant |
| (Right <= Refs and then |
| Left in 2 .. Refs + 1 and then |
| Extent_Logical (Buf, Left - 1) <= Logical); |
| end; |
| end loop; |
| return Left - 1; |
| end Bin_Search; |
| |
| procedure Next_Ref |
| (Current : in FSBlock_Offset; |
| Depth : in Extent_Depth; |
| Next : out Extent_Idx; |
| Cache_Start : out Max_Block_Index; |
| Cache_End : out Max_Block_Index; |
| Success : out Boolean) |
| with |
| Pre => |
| Dynamic_Max_Index = State.Static.Block_Size / Extent_Header_Size - 1, |
| Post => |
| State.Static = State.Static'Old and State.S = State.S'Old and |
| (if Success then |
| Next <= Dynamic_Max_Index and then |
| Cache_End = Cache_Start + State.Static.Block_Size - 1) |
| is |
| begin |
| Cache_FSBlock |
| (Static => State.Static, |
| Cache => State.Cache, |
| Phys => Current, |
| Level => Block_Map_Cache_Level + Depth, |
| Cache_Start => Cache_Start, |
| Cache_End => Cache_End, |
| Success => Success); |
| if not Success then |
| Next := 1; |
| return; |
| end if; |
| |
| declare |
| 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 (Cache (Cache_Start .. Cache_End), 1); |
| begin |
| Success := Success and then |
| Hdr_Magic = Extent_Header_Magic and then |
| Hdr_Depth = Depth and then |
| Hdr_Entries in Extent_Idx and then |
| Hdr_Entries <= Dynamic_Max_Index; |
| if not Success or else |
| -- Is the searched `Logical' out of range? |
| First_Logical > Logical |
| then |
| Next := 1; |
| else |
| pragma Assert (Cache_End - Cache_Start + 1 = State.Static.Block_Size); |
| Next := Bin_Search (Cache (Cache_Start .. Cache_End), Hdr_Entries); |
| end if; |
| end; |
| end Next_Ref; |
| |
| Inline_Extents : Ext2.Inline_Extents renames State.Inode.Inline; |
| Inode_Magic : constant Unsigned_16 := Header_Magic (Inline_Extents); |
| Inode_Entries : constant Natural := Header_Entries (Inline_Extents); |
| First_Logical : constant FSBlock_Logical := Extent_Logical (Inline_Extents, 1); |
| Depth : Natural := Header_Depth (Inline_Extents); |
| |
| Cache_Start, Cache_End : Max_Block_Index; |
| Logical_Off, Length : FSBlock_Logical; |
| Physical_Off : FSBlock_Offset; |
| Idx : Extent_Idx; |
| begin |
| Physical := 0; -- Return `0' if the searched `Logical' is not allocated. |
| Success := |
| Inode_Magic = Extent_Header_Magic and then |
| Inode_Entries < Inline_Extents'Length / Extent_Header_Size and then |
| Depth in Extent_Depth; |
| if not Success or else |
| -- Is there no extent or the searched `Logical' out of range? |
| Inode_Entries = 0 or else First_Logical > Logical |
| then |
| return; |
| end if; |
| |
| Idx := Bin_Search (Inline_Extents, Inode_Entries); |
| if Depth = 0 then |
| Physical_Off := Extent_Physical (Inline_Extents, Idx); |
| Logical_Off := Extent_Logical (Inline_Extents, Idx); |
| Length := Extent_Length (Inline_Extents, Idx); |
| else |
| Physical_Off := Index_Physical (Inline_Extents, Idx); |
| Logical_Off := Index_Logical (Inline_Extents, Idx); |
| loop |
| pragma Loop_Invariant |
| (State.Static = State.Static'Loop_Entry and then |
| State.S = State.S'Loop_Entry and then |
| Depth > 0 and then |
| Depth in Extent_Depth and then |
| Logical_Off <= Logical); |
| Depth := Depth - 1; |
| Next_Ref |
| (Current => Physical_Off, |
| Depth => Depth, |
| Next => Idx, |
| Cache_Start => Cache_Start, |
| Cache_End => Cache_End, |
| Success => Success); |
| if not Success then |
| return; |
| end if; |
| |
| exit when Depth = 0; |
| Physical_Off := Index_Physical (Cache (Cache_Start .. Cache_End), Idx); |
| Logical_Off := Index_Logical (Cache (Cache_Start .. Cache_End), Idx); |
| |
| -- Is the searched `Logical' out of range? |
| if Logical_Off > Logical then |
| return; |
| end if; |
| end loop; |
| |
| Physical_Off := 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; |
| |
| -- Is the searched `Logical' out of range? |
| if Logical_Off > Logical or else |
| -- Is this an empty extent? |
| (Length = 0 or Length > Initialized_Extent_Max_Len) |
| then |
| return; |
| end if; |
| |
| Success := Logical_Off <= FSBlock_Logical'Last - Length + 1; |
| if not Success or else |
| -- Is the searched `Logical' after this extent? |
| Logical > Logical_Off + Length - 1 |
| then |
| return; |
| end if; |
| |
| Success := FSBlock_Offset (Logical - Logical_Off) <= FSBlock_Offset'Last - Physical_Off; |
| if Success then |
| Physical := Physical_Off + FSBlock_Offset (Logical - Logical_Off); |
| end if; |
| end Extent_Block_Map; |
| |
| procedure Parse_Group |
| (Static : in Mount_State; |
| Table_Start : out FSBlock_Offset; |
| Buf : in Buffer_Type; |
| Success : out Boolean) |
| with |
| Pre => |
| Buf'Length >= Group_Desc_Size'First and |
| (if Static.Feature_64Bit then Buf'Length >= 64) |
| is |
| Inode_Table_Block : constant Unsigned_64 := |
| (if Static.Feature_64Bit |
| then Shift_Left (Unsigned_64 (Read_LE32 (Buf, 40)), 32) |
| else 0) |
| or |
| Unsigned_64 (Read_LE32 (Buf, 8)); |
| begin |
| if Inode_Table_Block >= Unsigned_64 (Static.First_Data_Block) and |
| Inode_Table_Block <= Unsigned_64 (FSBlock_Offset'Last) |
| then |
| Table_Start := FSBlock_Offset (Inode_Table_Block); |
| Success := True; |
| else |
| Table_Start := 0; |
| Success := False; |
| end if; |
| end Parse_Group; |
| |
| procedure Parse_Inode |
| (Static : in Mount_State; |
| Inode : in out Inode_Info; |
| Buf : in Buffer_Type; |
| Success : out Boolean) |
| with |
| Pre => Buf'Length >= Inode_Size'First |
| is |
| S_IFMT : constant := 8#170000#; |
| S_IFDIR : constant := 8#040000#; |
| S_IFREG : constant := 8#100000#; |
| S_IFLNK : constant := 8#120000#; |
| |
| I_Mode : constant Unsigned_16 := Read_LE16 (Buf, 0); |
| I_Blocks : constant Unsigned_32 := Read_LE32 (Buf, 28); |
| I_Flags : constant Unsigned_32 := Read_LE32 (Buf, 32); |
| I_File_ACL : constant Unsigned_32 := Read_LE32 (Buf, 104); |
| begin |
| case I_Mode and S_IFMT is |
| when S_IFDIR => Inode.Mode := Dir; |
| when S_IFREG => Inode.Mode := Regular; |
| when S_IFLNK => Inode.Mode := Link; |
| when others => Success := False; return; |
| end case; |
| |
| if Inode.Mode = Link and |
| ((I_File_ACL = 0 and I_Blocks = 0) or |
| (I_File_ACL /= 0 and I_Blocks = 2 ** (Static.Block_Size_Bits - 9))) |
| then |
| Inode.Mode := Fast_Link; |
| end if; |
| |
| declare |
| I_Size : constant Unsigned_64 := |
| (if Inode.Mode = Regular |
| then Shift_Left (Unsigned_64 (Read_LE32 (Buf, 108)), 32) |
| else 0) or |
| Unsigned_64 (Read_LE32 (Buf, 4)); |
| begin |
| if I_Size > Unsigned_64 (Inode_Length'Last) then |
| Success := False; |
| return; |
| end if; |
| Inode.Size := Inode_Length (I_Size); |
| end; |
| |
| Inode.Use_Extents := Static.Feature_Extents and (I_Flags and EXT4_EXTENTS_FL) /= 0; |
| Inode.Inline := Buf (Buf'First + 40 .. Buf'First + 100 - 1); |
| |
| Success := True; |
| end Parse_Inode; |
| |
| procedure Open |
| (State : in out T; |
| Inode : in Inode_Index; |
| Success : out Boolean) |
| with |
| Pre => Is_Mounted (State), |
| Post => Is_Mounted (State) and (Success = Is_Open (State)) |
| is |
| Static : Mount_State renames State.Static; |
| Cache : Cache_Buffer renames State.Cache.Buffer; |
| |
| Group : constant Group_Index := Group_Index ((Inode - 1) / Static.Inodes_Per_Group); |
| Group_Block : constant FSBlock_Offset := |
| 1 + FSBlock_Offset (Static.First_Data_Block) + FSBlock_Offset (Group / Static.Group_Desc_Per_Block); |
| Group_In_Block : constant Group_In_Block_Index := Group_In_Block_Index (Group mod Static.Group_Desc_Per_Block); |
| Group_In_Block_Offset : constant Natural := Natural (Group_In_Block) * Static.Group_Desc_Size; |
| |
| Cache_Start, Cache_End : Max_Block_Index; |
| First_Table_Block : FSBlock_Offset; |
| begin |
| State.S := Mounted; |
| |
| Cache_FSBlock |
| (Static => Static, |
| Cache => State.Cache, |
| Phys => Group_Block, |
| Level => Group_Cache_Level, |
| Cache_Start => Cache_Start, |
| Cache_End => Cache_End, |
| Success => Success); |
| Success := Success and then |
| -- TODO: Prove this using a predicate on Mount_State: |
| Cache_Start <= Cache_End - Group_In_Block_Offset - Static.Group_Desc_Size + 1; |
| if not Success then |
| return; |
| end if; |
| |
| Parse_Group |
| (Static => Static, |
| Table_Start => First_Table_Block, |
| Buf => Cache (Cache_Start + Group_In_Block_Offset .. |
| Cache_Start + Group_In_Block_Offset + Static.Group_Desc_Size - 1), |
| Success => Success); |
| if not Success then |
| return; |
| end if; |
| |
| declare |
| Inode_In_Group : constant Inode_In_Group_Index := |
| Inode_In_Group_Index ((Inode - 1) mod Static.Inodes_Per_Group); |
| |
| Inode_Block : constant FSBlock_Offset := FSBlock_Offset (Inode_In_Group / Static.Inodes_Per_Block); |
| Inode_In_Block : constant Inode_In_Block_Index := |
| Inode_In_Block_Index (Inode_In_Group mod Static.Inodes_Per_Block); |
| Inode_In_Block_Offset : constant Natural := |
| Natural (Inode_In_Block) * Static.Inode_Size; |
| begin |
| if First_Table_Block > FSBlock_Offset'Last - Inode_Block then |
| Success := False; |
| return; |
| end if; |
| |
| Cache_FSBlock |
| (Static => Static, |
| Cache => State.Cache, |
| Phys => FSBlock_Offset (First_Table_Block + Inode_Block), |
| Level => Inode_Cache_Level, |
| Cache_Start => Cache_Start, |
| Cache_End => Cache_End, |
| Success => Success); |
| Success := Success and then |
| -- TODO: Prove this using a predicate on Mount_State: |
| Cache_Start <= Cache_End - Inode_In_Block_Offset - Static.Inode_Size + 1; |
| if not Success then |
| return; |
| end if; |
| |
| Parse_Inode |
| (Static => State.Static, |
| Inode => State.Inode, |
| Buf => Cache (Cache_Start + Inode_In_Block_Offset .. |
| Cache_Start + Inode_In_Block_Offset + Static.Inode_Size - 1), |
| Success => Success); |
| |
| if Success then |
| State.Inode.I := Inode; |
| State.Inode.Map_Cache := (others => <>); |
| State.S := File_Opened; |
| end if; |
| end; |
| end Open; |
| |
| 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) |
| is |
| File_Name_Max : constant := 255; |
| Root_Inode : constant := 2; |
| |
| function Str_Buf_Equal (Str : String; Buf : Buffer_Type) return Boolean |
| with |
| Pre => Str'Length <= Buf'Length |
| is |
| begin |
| for I in Str'Range loop |
| if Character'Pos (Str (I)) /= Buf (Buf'First + (I - Str'First)) then |
| return False; |
| end if; |
| end loop; |
| return True; |
| end Str_Buf_Equal; |
| |
| File_Inode : Inode_Index; |
| File_Pos : File_Length; |
| begin |
| File_Len := 0; |
| File_Type := FS.File_Type'First; |
| |
| if File_Name'Length > File_Name_Max then |
| Success := False; |
| return; |
| end if; |
| |
| -- Ensure dir is opened: |
| -- |
| if State.S = File_Opened then |
| if State.Cur_Dir /= State.Inode.I then |
| Success := False; |
| return; |
| end if; |
| else |
| if In_Root then |
| State.Cur_Dir := Root_Inode; |
| end if; |
| Open (State, State.Cur_Dir, Success); |
| if not Success then |
| return; |
| end if; |
| end if; |
| |
| -- Lookup file in opened dir: |
| -- |
| File_Pos := 0; |
| Success := False; |
| loop |
| pragma Loop_Invariant (Is_Open (State) and not Success); |
| declare |
| Dir_Entry_Header_Length : constant := 4 + 2 + 1 + 1; |
| Dir_Entry_Header : Buffer_Type (0 .. Dir_Entry_Header_Length - 1); |
| Dir_Entry_Name : Buffer_Type (0 .. File_Name_Max - 1); |
| Entry_File_Pos : File_Offset := File_Pos; |
| Dir_Entry_Length : File_Length; |
| Inode : Inode_0_Index; |
| Len : Natural; |
| begin |
| Read |
| (State => State, |
| File_Pos => Entry_File_Pos, |
| Buf => Dir_Entry_Header, |
| Len => Len); |
| if Len < Dir_Entry_Header_Length then |
| return; |
| end if; |
| |
| -- Only check filenames of exact same length |
| Inode := Inode_0_Index (Read_LE32 (Dir_Entry_Header, 0)); |
| if Inode >= Root_Inode and then |
| File_Name'Length = Natural (Dir_Entry_Header (6)) |
| then |
| pragma Warnings |
| (GNATprove, Off, """Entry_File_Pos"" is set*but not used", |
| Reason => "We only care about intermedidate values."); |
| Read |
| (State => State, |
| File_Pos => Entry_File_Pos, |
| Buf => Dir_Entry_Name, |
| Len => Len); |
| pragma Warnings (GNATprove, On, """Entry_File_Pos"" is set*but not used"); |
| if Len < File_Name'Length then |
| return; |
| end if; |
| |
| Success := Str_Buf_Equal (File_Name, Dir_Entry_Name); |
| if Success then |
| File_Inode := Inode; |
| exit; |
| end if; |
| end if; |
| |
| Dir_Entry_Length := File_Length (Read_LE16 (Dir_Entry_Header, 4)); |
| if Dir_Entry_Length = 0 or |
| File_Pos > File_Length'Last - Dir_Entry_Length or |
| Unsigned_64 (File_Pos) >= Unsigned_64 (State.Inode.Size) - Unsigned_64 (Dir_Entry_Length) |
| then |
| return; |
| end if; |
| File_Pos := File_Pos + Dir_Entry_Length; |
| end; |
| end loop; |
| pragma Assert_And_Cut (Success and Is_Mounted (State)); |
| |
| Open (State, File_Inode, Success); |
| if not Success then |
| return; |
| end if; |
| |
| if State.Inode.Mode = Dir then |
| State.Cur_Dir := File_Inode; |
| end if; |
| |
| Success := State.Inode.Size <= Inode_Length (File_Length'Last); |
| if Success then |
| File_Len := File_Length (State.Inode.Size); |
| File_Type := (case State.Inode.Mode is |
| when Dir => FS.Dir, |
| when Regular => FS.Regular, |
| when Link .. Fast_Link => FS.Link); |
| else |
| Close (State); |
| end if; |
| end Open; |
| |
| procedure Close (State : in out T) is |
| begin |
| State.S := Mounted; |
| end Close; |
| |
| procedure Read |
| (State : in out T; |
| File_Pos : in out File_Offset; |
| Buf : out Buffer_Type; |
| Len : out Natural) |
| is |
| Static : Mount_State renames State.Static; |
| Cache : Cache_Buffer renames State.Cache.Buffer; |
| |
| Pos : Natural range Buf'First .. Buf'Last + 1; |
| begin |
| if State.Inode.Mode = Fast_Link then |
| if State.Inode.Size > Inode_Length (State.Inode.Inline'Length) or |
| Inode_Length (File_Pos) >= State.Inode.Size then |
| Len := 0; |
| else |
| Len := Natural'Min (Buf'Length, Natural (State.Inode.Size) - Natural (File_Pos)); |
| end if; |
| Buf (Buf'First .. Buf'First + Len - 1) := |
| State.Inode.Inline (Natural (File_Pos) .. Natural (File_Pos) + Len - 1); |
| Buf (Buf'First + Len .. Buf'Last) := (others => 16#00#); |
| File_Pos := File_Pos + File_Length (Len); |
| return; |
| end if; |
| |
| Len := 0; |
| Pos := Buf'First; |
| while Pos <= Buf'Last and |
| File_Pos < File_Offset'Last and |
| Inode_Length (File_Pos) < State.Inode.Size |
| loop |
| pragma Loop_Invariant (for all I in Buf'First .. Pos - 1 => Buf (I)'Initialized); |
| pragma Loop_Invariant (Is_Open (State)); |
| declare |
| 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 Positive := Static.Block_Size - In_Block; |
| In_File_Space : constant Inode_Length := State.Inode.Size - Inode_Length (File_Pos); |
| In_Buf_Space : constant Positive := Buf'Last - Pos + 1; |
| Len_Here : Positive; |
| begin |
| Len_Here := In_Block_Space; |
| if In_File_Space < Inode_Length (Len_Here) then |
| Len_Here := Positive (In_File_Space); |
| end if; |
| if In_Buf_Space < Len_Here then |
| Len_Here := In_Buf_Space; |
| end if; |
| if File_Offset'Last - File_Pos < File_Length (Len_Here) then |
| Len_Here := Positive (File_Offset'Last - File_Pos); |
| end if; |
| |
| declare |
| Last : constant Index_Type := Pos + Len_Here - 1; |
| Cache_Start, Cache_End : Max_Block_Index; |
| Physical : FSBlock_Offset; |
| Success : Boolean; |
| begin |
| if State.Inode.Map_Cache.Logical = Block_Offset (Logical) then |
| Physical := State.Inode.Map_Cache.Phys; |
| Success := True; |
| elsif State.Inode.Use_Extents then |
| Extent_Block_Map (State, Logical, Physical, Success); |
| else |
| Ext2_Block_Map (State, Logical, Physical, Success); |
| end if; |
| exit when not Success; |
| State.Inode.Map_Cache := (Phys => Physical, Logical => Block_Offset (Logical)); |
| |
| if Physical > 0 then |
| Cache_FSBlock |
| (Static => Static, |
| Cache => State.Cache, |
| Phys => Physical, |
| Level => File_Cache_Level, |
| Cache_Start => Cache_Start, |
| Cache_End => Cache_End, |
| Success => Success); |
| pragma Assert (Cache_Start <= Cache_End - (In_Block + Len_Here - 1)); |
| exit when not Success; |
| |
| Buf (Pos .. Last) := Cache ( |
| Cache_Start + In_Block .. Cache_Start + In_Block + Len_Here - 1); |
| else |
| -- Treat unallocated and unwritten blocks as all 00 (sparse files). |
| Buf (Pos .. Last) := (others => 16#00#); |
| end if; |
| |
| File_Pos := File_Pos + File_Length (Len_Here); |
| Pos := Pos + Len_Here; |
| Len := Pos - Buf'First; |
| end; |
| end; |
| end loop; |
| Buf (Pos .. Buf'Last) := (others => 16#00#); |
| end Read; |
| |
| -------------------------------------------------------------------------- |
| |
| package C is new VFS (T => T, Initial => (S => Unmounted, others => <>)); |
| |
| function C_Mount return int |
| with |
| Export, |
| Convention => C, |
| External_Name => "ext2fs_mount"; |
| function C_Mount return int |
| with |
| SPARK_Mode => Off |
| is |
| begin |
| return C.C_Mount; |
| end C_Mount; |
| |
| function C_Open (File_Path : System.Address) return int |
| with |
| Export, |
| Convention => C, |
| External_Name => "ext2fs_dir"; |
| function C_Open (File_Path : System.Address) return int |
| with |
| SPARK_Mode => Off |
| is |
| begin |
| return C.C_Open (File_Path); |
| end C_Open; |
| |
| function C_Read (Buf : System.Address; Len : int) return int |
| with |
| Export, |
| Convention => C, |
| External_Name => "ext2fs_read"; |
| function C_Read (Buf : System.Address; Len : int) return int |
| with |
| SPARK_Mode => Off |
| is |
| begin |
| return C.C_Read (Buf, Len); |
| end C_Read; |
| |
| end FILO.FS.Ext2; |