| -- Copyright (C) 2024 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 FILO.Blockdev; |
| with FILO.FS.VFS; |
| |
| use Interfaces.C; |
| |
| package body FILO.FS.ISO9660 is |
| |
| function Is_Mounted (State : T) return Boolean is (State.S >= Mounted); |
| function Is_Open (State : T) return Boolean is (State.S = File_Opened); |
| |
| -------------------------------------------------------------------------- |
| |
| procedure Read |
| (Buf : out Buffer_Type; |
| Block : in FSBlock; |
| Offset : in FSBlock_Index; |
| FS_Len : in Partition_Length; |
| Success : out Boolean) |
| with |
| Pre => Buf'Length <= FSBlock_Size - Offset |
| is |
| Block_64 : constant Integer_64 := Integer_64 (Block); |
| Offset_64 : constant Integer_64 := Integer_64 (Offset); |
| Max_Block_Offset : constant Integer_64 := Integer_64 (FS_Len) / FSBlock_Size - 1; |
| begin |
| if Block_64 > Max_Block_Offset then |
| Buf := (others => 16#00#); |
| Success := False; |
| return; |
| end if; |
| Blockdev.Read (Buf, Blockdev_Length (Block_64 * FSBlock_Size + Offset_64), Success); |
| end Read; |
| |
| procedure Mount |
| (State : in out T; |
| Part_Len : in Partition_Length; |
| Success : out Boolean) |
| is |
| D_Type : constant Index_Type := 0; |
| D_Id : constant Index_Type := 1; |
| D_Ver : constant Index_Type := 6; |
| |
| D_Type_Primary : constant := 1; |
| D_Type_Terminator : constant := 255; |
| |
| CD001 : constant Buffer_Type := |
| (Character'Pos ('C'), Character'Pos ('D'), |
| Character'Pos ('0'), Character'Pos ('0'), Character'Pos ('1')); |
| |
| Static : Mount_State renames State.Static; |
| |
| Volume_Descriptor : Buffer_Type (0 .. D_Ver); |
| Block : FSBlock := 16; |
| begin |
| loop |
| pragma Loop_Invariant (Block < 1024); |
| pragma Loop_Invariant (not Is_Mounted (State)); |
| |
| if Part_Len < Partition_Length (Block + 1) * FSBlock_Size then |
| Success := False; |
| return; |
| end if; |
| |
| Read (Volume_Descriptor, Block, 0, Part_Len, Success); |
| if not Success then |
| return; |
| end if; |
| |
| if Volume_Descriptor (D_Ver) /= 1 or |
| Volume_Descriptor (D_Id .. D_Ver - 1) /= CD001 or |
| Volume_Descriptor (D_Type) = D_Type_Terminator |
| then |
| Success := False; |
| return; |
| end if; |
| |
| exit when Volume_Descriptor (D_Type) = D_Type_Primary; |
| |
| Block := Block + 1; |
| if Block >= 1024 then |
| Success := False; |
| return; |
| end if; |
| end loop; |
| |
| Static.Part_Len := Part_Len; |
| Static.Root_Inode := (Block, 156); |
| |
| State.S := Mounted; |
| end Mount; |
| |
| procedure Open |
| (State : in out T; |
| I : 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; |
| Inode : Inode_Info renames State.Inode; |
| |
| Dir_Rec : Directory_Record; |
| begin |
| State.S := Mounted; |
| |
| Inode := (I, others => <>); |
| |
| Read (Dir_Rec, I.Block, I.Offset, Static.Part_Len, Success); |
| if not Success then |
| return; |
| end if; |
| |
| declare |
| D_Flag_Dir : constant := 16#02#; |
| D_Flag_Cont : constant := 16#80#; |
| D_Flags : constant Unsigned_8 := Dir_Rec (25); |
| D_Extent : constant Unsigned_32 := Read_LE32 (Dir_Rec, 2); |
| begin |
| if D_Extent > Unsigned_32 (FSBlock'Last) then |
| Success := False; |
| return; |
| end if; |
| if (D_Flags and D_Flag_Cont) /= 0 then |
| Success := False; |
| return; |
| end if; |
| |
| if (D_Flags and D_Flag_Dir) /= 0 then |
| Inode.Mode := Dir; |
| else |
| Inode.Mode := Regular; |
| end if; |
| Inode.Size := Inode_Length (Read_LE32 (Dir_Rec, 10)); |
| Inode.Extents (0) := |
| (Start => FSBlock (D_Extent), |
| Count => FSBlock_Count (Inode.Size / Inode_Length (FSBlock_Size))); |
| State.S := File_Opened; |
| 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; |
| |
| 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 |
| declare |
| Chr : constant Unsigned_8 := |
| (if 'a' <= Str (I) and Str (I) <= 'z' then |
| Character'Pos (Str (I)) - Character'Pos ('a') + Character'Pos ('A') |
| else Character'Pos (Str (I))); |
| begin |
| if Chr /= Buf (Buf'First + (I - Str'First)) then |
| return False; |
| end if; |
| end; |
| end loop; |
| return True; |
| end Str_Buf_Equal; |
| |
| Found_Inode : Inode_Index; |
| Dir_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 := State.Static.Root_Inode; |
| end if; |
| declare |
| Cur_Dir : constant Inode_Index := State.Cur_Dir; |
| begin |
| Open (State, Cur_Dir, Success); |
| if not Success then |
| return; |
| end if; |
| end; |
| end if; |
| |
| -- Lookup file in opened dir: |
| -- |
| Dir_Pos := 0; |
| Success := False; |
| loop |
| pragma Loop_Invariant (Is_Open (State) and not Success); |
| pragma Loop_Invariant |
| (FSBlock_Index (Dir_Pos mod FSBlock_Size) <= Directory_Record_Offset'Last); |
| |
| declare |
| Dir_Rec : Directory_Record; |
| Dir_Rec_Name : Buffer_Type (0 .. File_Name_Max - 1); |
| Record_Dir_Pos : File_Offset := Dir_Pos; |
| Len : Natural; |
| begin |
| Read |
| (State => State, |
| File_Pos => Record_Dir_Pos, |
| Buf => Dir_Rec, |
| Len => Len); |
| if Len < Dir_Rec'Length then |
| return; |
| end if; |
| |
| if File_Name'Length <= Natural (Dir_Rec (32)) and |
| Natural (Dir_Rec (32)) <= File_Name'Length + 3 |
| then |
| pragma Warnings |
| (GNATprove, Off, """Record_Dir_Pos"" is set*but not used", |
| Reason => "We only care about intermedidate values."); |
| Read |
| (State => State, |
| File_Pos => Record_Dir_Pos, |
| Buf => Dir_Rec_Name (0 .. Natural (Dir_Rec (32) - 1)), |
| Len => Len); |
| pragma Warnings (GNATprove, On, """Record_Dir_Pos"" is set*but not used"); |
| |
| if (Len = 1 and Dir_Rec_Name (0) = 16#00# and File_Name = ".") or |
| (Len = 1 and Dir_Rec_Name (0) = 16#01# and File_Name = "..") |
| then |
| Success := True; |
| else |
| -- Remove file version |
| if Len >= File_Name'Length + 2 and |
| Dir_Rec_Name (Len - 2) = Character'Pos (';') and |
| Dir_Rec_Name (Len - 1) = Character'Pos ('1') |
| then |
| Len := Len - 2; |
| end if; |
| |
| -- Remove trailing . |
| if Len >= File_Name'Length + 1 and |
| Dir_Rec_Name (Len - 1) = Character'Pos ('.') |
| then |
| Len := Len - 1; |
| end if; |
| |
| Success := Len = File_Name'Length and then |
| Str_Buf_Equal (File_Name, Dir_Rec_Name); |
| end if; |
| if Success then |
| Found_Inode := |
| (Block => FSBlock (Dir_Pos / FSBlock_Size) + State.Inode.Extents (0).Start, |
| Offset => FSBlock_Index (Dir_Pos mod FSBlock_Size)); |
| exit; |
| end if; |
| end if; |
| |
| declare |
| Dir_Rec_Length : constant File_Length := File_Length (Dir_Rec (0)); |
| Block_Gap : constant File_Length := FSBlock_Size - (Dir_Pos mod FSBlock_Size); |
| begin |
| -- End of block? |
| if Dir_Rec_Length = Block_Gap or Dir_Rec_Length = 0 then |
| if Unsigned_64 (Dir_Pos) >= Unsigned_64 (State.Inode.Size) - Unsigned_64 (Block_Gap) then |
| return; |
| else |
| Dir_Pos := Dir_Pos + Block_Gap; |
| end if; |
| else |
| if Unsigned_64 (Dir_Pos) > Unsigned_64 (State.Inode.Size) - Unsigned_64 (Dir_Rec_Length) then |
| return; |
| else |
| Dir_Pos := Dir_Pos + Dir_Rec_Length; |
| end if; |
| end if; |
| end; |
| end; |
| end loop; |
| pragma Assert_And_Cut (Success and Is_Mounted (State)); |
| |
| Open (State, Found_Inode, Success); |
| if not Success then |
| return; |
| end if; |
| |
| if State.Inode.Mode = Dir then |
| State.Cur_Dir := Found_Inode; |
| end if; |
| |
| Success := State.Inode.Size <= Inode_Length (File_Length'Last); |
| if Success then |
| File_Len := File_Length (State.Inode.Size); |
| File_Type := State.Inode.Mode; |
| 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; |
| |
| Pos : Natural range Buf'First .. Buf'Last + 1; |
| begin |
| 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 FSBlock_Index := Natural (File_Pos mod FSBlock_Size); |
| Logical : constant FSBlock_Logical := FSBlock_Logical (File_Pos / FSBlock_Size); |
| In_Block_Space : constant Positive := Index_Type (FSBlock_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 |
| exit when FSBlock (Logical) > FSBlock'Last - State.Inode.Extents (0).Start; |
| |
| 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; |
| Physical : constant FSBlock := State.Inode.Extents (0).Start + FSBlock (Logical); |
| Success : Boolean; |
| begin |
| Read |
| (Buf => Buf (Pos .. Last), |
| Block => Physical, |
| Offset => In_Block, |
| FS_Len => Static.Part_Len, |
| Success => Success); |
| exit when not Success; |
| |
| 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 => "iso9660_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 => "iso9660_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 => "iso9660_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.ISO9660; |