| -- 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 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#; |
| |
| 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 := Block_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 (Positive'Last) then |
| State.Inodes_Per_Group := Positive (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 S_Desc_Size in |
| Unsigned_16 (Desc_Size'First) .. Unsigned_16 (Desc_Size'Last) |
| then |
| State.Desc_Size := Desc_Size (S_Desc_Size); |
| else |
| Success := False; |
| return; |
| end if; |
| end; |
| 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; |
| Logical_Off : in FSBlock_Logical; |
| 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_Index (Cache_Level) = Logical_Off then |
| Success := True; |
| else |
| Read_FSBlock |
| (State => State, |
| Buf => State.Block_Cache (Cache_Start .. Cache_End), |
| FSBlock => Phys, |
| Success => Success); |
| State.Block_Cache_Index (Cache_Level) := Logical_Off; |
| end if; |
| end Cache_FSBlock; |
| |
| procedure Ext2_Block_Map |
| (State : in out T; |
| Logical : in FSBlock_Logical; |
| Physical : out FSBlock_Offset; |
| Success : out Boolean) |
| is |
| 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, |
| Logical_Off => 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 (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 (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 (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 (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 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; |