| -- 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 Interfaces.C.Strings; |
| |
| 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_BLOCKS : constant := SUPERBLOCK_SIZE / BLOCK_SIZE; |
| |
| 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 |
| Super_Block : Buffer_Type (0 .. SUPERBLOCK_SIZE - 1) := (others => 0); |
| 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; |
| |
| State.Part_Len := Part_Len; |
| State.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); |
| else |
| Success := False; |
| return; |
| end if; |
| end; |
| |
| 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 |
| State.Inodes_Per_Group := Inode_Index (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 S_Inode_Size in |
| Unsigned_16 (Inode_Size'First) .. Unsigned_16 (Inode_Size'Last) |
| then |
| State.Inode_Size := Inode_Size (S_Inode_Size); |
| else |
| Success := False; |
| return; |
| end if; |
| end; |
| else |
| State.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 |
| declare |
| S_Desc_Size : constant Unsigned_16 := Read_LE16 (Super_Block, 63 * 4 + 2); |
| begin |
| if Is_Power_Of_2 (S_Desc_Size) and then |
| S_Desc_Size in Unsigned_16 (Desc_Size'First) .. |
| Unsigned_16 (Positive'Min (Desc_Size'Last, 2 ** State.Block_Size_Bits)) |
| then |
| State.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; |
| else |
| State.Desc_Size := Desc_Size'First; |
| end if; |
| end; |
| |
| State.S := Mounted; |
| end Mount; |
| |
| procedure Read_FSBlock |
| (State : in T; |
| Buf : out Buffer_Type; |
| FSBlock : in FSBlock_Offset; |
| Success : out Boolean) |
| with |
| Pre => |
| Is_Mounted (State) and |
| Buf'Length = 2 ** State.Block_Size_Bits |
| is |
| Block_Size : constant Blockdev_Length := 2 ** State.Block_Size_Bits; |
| Max_Block_Offset : constant FSBlock_Offset := |
| FSBlock_Offset (State.Part_Len / Block_Size - 1); |
| begin |
| if FSBlock > Max_Block_Offset then |
| Success := False; |
| return; |
| end if; |
| Blockdev.Read (Buf, Blockdev_Length (FSBlock) * Block_Size, Success); |
| end Read_FSBlock; |
| |
| procedure Cache_FSBlock |
| (State : in out T; |
| Phys : in FSBlock_Offset; |
| Level : in Block_Cache_Index; |
| Label : in Cache_Label; |
| Logical : in Boolean := True; |
| Cache_Start : out Max_Block_Index; |
| Cache_End : out Max_Block_Index; |
| Success : out Boolean) |
| with |
| Post => Cache_End = Cache_Start + 2 ** State.Block_Size_Bits |
| is |
| Block_Size : constant Natural := 2 ** State.Block_Size_Bits; |
| -- Limit cache usage depending on block size: |
| Max_Level : constant Block_Cache_Index := |
| 2 ** (Log_Block_Size'Last - State.Block_Size_Bits) - 1; |
| Cache_Level : constant Block_Cache_Index := |
| Block_Cache_Index'Min (Level, Max_Level); |
| begin |
| Cache_Start := Cache_Level * Block_Size; |
| Cache_End := Cache_Start + Block_Size - 1; |
| if State.Block_Cache_Logical (Cache_Level) = Logical and |
| State.Block_Cache_Label (Cache_Level) = Label |
| then |
| Success := True; |
| else |
| Read_FSBlock |
| (State => State, |
| Buf => State.Block_Cache (Cache_Start .. Cache_End), |
| FSBlock => Phys, |
| Success => Success); |
| State.Block_Cache_Logical (Cache_Level) := Logical; |
| State.Block_Cache_Label (Cache_Level) := Label; |
| end if; |
| end Cache_FSBlock; |
| |
| procedure Cache_FSBlock |
| (State : in out T; |
| 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 + 2 ** State.Block_Size_Bits |
| is |
| begin |
| Cache_FSBlock (State, Phys, Level, Cache_Label (Phys), |
| False, Cache_Start, Cache_End, Success); |
| end Cache_FSBlock; |
| |
| procedure Reset_Cache_Logical (State : in out T) 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; |
| end if; |
| end loop; |
| end Reset_Cache_Logical; |
| |
| procedure Ext2_Block_Map |
| (State : in out T; |
| Logical : in FSBlock_Logical; |
| Physical : out FSBlock_Offset; |
| Success : out Boolean) |
| is |
| 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 => Inode_Extents'Length * 8; |
| |
| 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)); |
| |
| Block_Size : constant Natural := 2 ** State.Block_Size_Bits; |
| Addr_Per_Block : constant FSBlock_Logical := FSBlock_Logical (Block_Size / 4); |
| Max_Addr_Per_Block : constant FSBlock_Logical := FSBlock_Logical (2 ** Log_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; |
| Logical_Off : in FSBlock_Logical; |
| Next_Physical : out FSBlock_Offset; |
| Success : out Boolean) |
| with |
| Pre => FSBlock_Logical (Addr_In_Block) < Addr_Per_Block |
| is |
| Cache_Start, Cache_End : Max_Block_Index; |
| begin |
| Cache_FSBlock |
| (State => State, |
| Phys => Indirect_Block_Phys, |
| Level => Level, |
| Label => Cache_Label (Logical_Off), |
| Cache_Start => Cache_Start, |
| Cache_End => Cache_End, |
| Success => Success); |
| Next_Physical := FSBlock_Offset (Read_LE32 |
| (Buf => State.Block_Cache (Cache_Start .. Cache_End), |
| Off => Natural (Addr_In_Block) * 4)); |
| end Indirect_Block_Lookup; |
| |
| Logical_Rest : FSBlock_Logical := Logical; |
| 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 => 0, |
| Logical_Off => Logical - Logical_Rest, |
| 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), |
| Level => 1, |
| Logical_Off => Logical - Logical_Rest, |
| 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 => 0, |
| Logical_Off => Logical - (Logical_Rest mod Addr_Per_Block), |
| 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), |
| Level => 2, |
| Logical_Off => Logical - Logical_Rest, |
| 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 => 1, |
| Logical_Off => Logical - (Logical_Rest mod Addr_Per_Block ** 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 mod Addr_Per_Block), |
| Level => 0, |
| Logical_Off => Logical - (Logical_Rest mod Addr_Per_Block), |
| Next_Physical => Physical, |
| Success => Success); |
| return; |
| end if; |
| |
| -- Logical address was just too high. |
| 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) |
| is |
| -- 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#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; |
| |
| 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 => Refs in 1 .. Extent_Idx (Buf'Length / Extent_Header_Size - 1) and |
| Extent_Logical (Buf, 1) <= Logical, |
| Post => Bin_Search'Result in 1 .. Refs and |
| Extent_Logical (Buf, Bin_Search'Result) <= Logical |
| is |
| Left : Extent_Idx := 1; |
| 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; |
| end; |
| end loop; |
| return Left - 1; |
| end Bin_Search; |
| |
| procedure Next_Ref |
| (Current : in FSBlock_Offset; |
| Logical_Off : in FSBlock_Logical; |
| Depth : in Natural; |
| Next : out Extent_Idx; |
| Cache_Start : out Max_Block_Index; |
| Cache_End : out Max_Block_Index; |
| Success : out Boolean) |
| with |
| Pre => Logical_Off <= Logical, |
| Post => (if Success then |
| Extent_Logical (State.Block_Cache (Cache_Start .. Cache_End), Next) <= Logical) |
| is |
| Block_Size : constant Natural := 2 ** State.Block_Size_Bits; |
| Dynamic_Max_Index : constant Natural := Block_Size / Extent_Header_Size - 1; |
| begin |
| Cache_FSBlock |
| (State => State, |
| Phys => Current, |
| Level => Depth, |
| Label => Cache_Label (Logical_Off), |
| 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 (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)); |
| First_Logical : constant FSBlock_Logical := |
| Extent_Logical (State.Block_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 <= Dynamic_Max_Index and then |
| First_Logical = Logical_Off; |
| if not Success then |
| Next := 1; |
| else |
| Next := Bin_Search (State.Block_Cache (Cache_Start .. Cache_End), Hdr_Entries); |
| end if; |
| end; |
| end Next_Ref; |
| |
| Inline_Extents : Ext2.Inode_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; |
| Idx : Extent_Idx; |
| begin |
| Success := |
| Inode_Magic = Extent_Header_Magic and then |
| Inode_Entries > 0 and then |
| Inode_Entries < Inline_Extents'Length / Extent_Header_Size and then |
| First_Logical <= Logical; |
| if not Success then |
| Physical := 0; |
| return; |
| end if; |
| |
| Idx := Bin_Search (Inline_Extents, Inode_Entries); |
| if Depth = 0 then |
| Physical := Extent_Physical (Inline_Extents, Idx); |
| Logical_Off := Extent_Logical (Inline_Extents, Idx); |
| Length := Extent_Length (Inline_Extents, Idx); |
| else |
| Physical := Index_Physical (Inline_Extents, Idx); |
| Logical_Off := Index_Logical (Inline_Extents, Idx); |
| loop |
| Depth := Depth - 1; |
| Next_Ref |
| (Current => Physical, |
| Logical_Off => Logical_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 := Index_Physical (State.Block_Cache (Cache_Start .. Cache_End), Idx); |
| Logical_Off := Index_Logical (State.Block_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); |
| end if; |
| |
| Success := |
| Length > 0 and then |
| Logical_Off <= FSBlock_Logical'Last - Length and then |
| Logical < Logical_Off + Length; |
| if Success then |
| Physical := Physical + FSBlock_Offset (Logical - Logical_Off); |
| end if; |
| end Extent_Block_Map; |
| |
| procedure Open |
| (State : in out T; |
| Inode : in Inode_Index; |
| Success : out Boolean) |
| with |
| Pre => Is_Mounted (State) and not Is_Open (State), |
| Post => Success = Is_Open (State) |
| is |
| 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); |
| |
| Block_Size : constant Natural := 2 ** State.Block_Size_Bits; |
| |
| Inodes_Per_Block : constant Inode_Index := Inode_Index (Block_Size / State.Inode_Size); |
| Desc_Per_Block : constant Group_Index := Group_Index (Block_Size / State.Desc_Size); |
| |
| 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); |
| |
| function Group_Inode_Table (Buf : Buffer_Type; Idx : Group_Index) return FSBlock_Offset |
| is |
| (FSBlock_Offset ( |
| (if State.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))))) |
| with |
| Pre => Buf'Length >= Group_Byte_Offset (Idx, 44); |
| |
| 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); |
| |
| function Inode_Flags (Buf : Buffer_Type; Idx : Inode_Index) return Unsigned_32 |
| is |
| (Read_LE32 (Buf, Inode_Byte_Offset (Idx, 32))) |
| with |
| Pre => Buf'Length >= Inode_Byte_Offset (Idx, 36); |
| |
| Group : constant Group_Index := Group_Index ((Inode - 1) / State.Inodes_Per_Group); |
| Desc_Block : constant FSBlock_Offset := |
| 1 + State.First_Data_Block + FSBlock_Offset (Group / Desc_Per_Block); |
| Cache_Start, Cache_End : Max_Block_Index; |
| begin |
| Cache_FSBlock |
| (State => State, |
| Phys => Desc_Block, |
| Level => Natural'Min (Natural (Group / Desc_Per_Block), Block_Cache_Index'Last), |
| Cache_Start => Cache_Start, |
| Cache_End => Cache_End, |
| Success => Success); |
| if not Success then |
| return; |
| end if; |
| |
| 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_Block : constant FSBlock_Offset := |
| Group_Inode_Table (State.Block_Cache (Cache_Start .. Cache_End), Group) + |
| FSBlock_Offset (Inode_In_Group / Inodes_Per_Block); |
| begin |
| Cache_FSBlock |
| (State => State, |
| Phys => Inode_Block, |
| Level => Block_Cache_Index'Last, |
| Cache_Start => Cache_Start, |
| Cache_End => Cache_End, |
| Success => Success); |
| if not Success then |
| return; |
| end if; |
| |
| declare |
| Inode_In_Block : constant Inode_Index := Inode_In_Group mod Inodes_Per_Block; |
| I_Flags : constant Unsigned_32 := |
| Inode_Flags (State.Block_Cache (Cache_Start .. Cache_End), Inode_In_Block); |
| begin |
| 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); |
| Reset_Cache_Logical (State); |
| State.S := File_Opened; |
| end; |
| end; |
| end Open; |
| |
| procedure Open |
| (State : in out T; |
| File_Len : out File_Length; |
| File_Path : in String; |
| Success : out Boolean) |
| is |
| begin |
| File_Len := 0; |
| Success := False; |
| end Open; |
| |
| procedure Close (State : in out T) is |
| begin |
| State.S := Mounted; |
| end Close; |
| |
| procedure Read |
| (State : in out T; |
| File_Len : in File_Length; |
| File_Pos : in out File_Offset; |
| Buf : out Buffer_Type; |
| Len : out Natural) |
| is |
| begin |
| Buf := (others => 0); |
| Len := 0; |
| 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 : Strings.chars_ptr) return int |
| with |
| Export, |
| Convention => C, |
| External_Name => "ext2fs_dir"; |
| function C_Open (File_Path : Strings.chars_ptr) 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; |