| -- 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 |
| |
| subtype SUSP_Signature is String (1 .. 2); |
| |
| -------------------------------------------------------------------------- |
| |
| function Is_Mounted (State : T) return Boolean is (State.S >= Mounted); |
| function Is_Open (State : T) return Boolean is (State.S = File_Opened); |
| |
| -------------------------------------------------------------------------- |
| |
| function "+" (Rec : FS_Record; Off : FSBlock_Length) return FS_Record |
| is |
| (Block => Rec.Block, Offset => Rec.Offset + Off, Size => Rec.Size - Off) |
| with |
| Pre => Rec.Size >= Off; |
| |
| procedure Read |
| (Buf : out Buffer_Type; |
| Rec : in FS_Record; |
| Success : out Boolean) |
| with |
| Pre => Buf'Length <= Rec.Size |
| is |
| Block_64 : constant Integer_64 := Integer_64 (Rec.Block); |
| Offset_64 : constant Integer_64 := Integer_64 (Rec.Offset); |
| begin |
| 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; |
| Static.Part_Len := Part_Len; |
| |
| Read (Volume_Descriptor, FS_Record'(Block, 0, FSBlock_Size), 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.Root_Inode := (Block, 156, Directory_Record'Length); |
| |
| State.S := Mounted; |
| end Mount; |
| |
| procedure Find_SUSP_Record |
| (State : in T; |
| Rec : out FS_Record; |
| Dir_Rec_Pos : in File_Offset; |
| Dir_Rec_Len : in FSBlock_Length; |
| Searched_Sig : in SUSP_Signature) |
| with |
| Pre => |
| Dir_Rec_Pos mod FSBlock_Size <= File_Offset (FSBlock_Size - Dir_Rec_Len) and |
| FSBlock_Count (Dir_Rec_Pos / FSBlock_Size) < State.Inode.Extents (0).Count |
| is |
| subtype Signature_Buf is Buffer_Type (0 .. 1); |
| function Signature (Str : SUSP_Signature) return Signature_Buf |
| is |
| ((Character'Pos (Str (Str'First)), Character'Pos (Str (Str'First + 1)))); |
| |
| Cur : FS_Record := |
| (Block => State.Inode.Extents (0).Start + FSBlock (Dir_Rec_Pos / FSBlock_Size), |
| Offset => FSBlock_Index (Dir_Rec_Pos mod FSBlock_Size), |
| Size => Dir_Rec_Len); |
| |
| Continuation : FS_Record := (Size => 0, others => <>); |
| |
| SUSP_Head : Buffer_Type (0 .. 3); |
| |
| Success : Boolean; |
| begin |
| Rec := (others => <>); |
| if Cur.Size = 0 then |
| return; |
| end if; |
| |
| if Cur.Offset mod 2 = 1 then |
| Cur := Cur + 1; |
| end if; |
| |
| for I in 1 .. 2**16 loop -- arbitrary limit to avoid endless loop |
| if Cur.Size < SUSP_Head'Length then |
| if Continuation.Size < SUSP_Head'Length then |
| return; |
| else |
| Cur := Continuation; |
| Continuation := (others => <>); |
| end if; |
| end if; |
| |
| Read (SUSP_Head, Cur, Success); |
| declare |
| Rec_Len : constant Natural := Natural (SUSP_Head (2)); |
| SUSP_CE : Buffer_Type (0 .. 27); |
| begin |
| if not Success or else Rec_Len not in 4 .. Cur.Size then |
| return; |
| end if; |
| |
| if SUSP_Head (0 .. 1) = Signature (Searched_Sig) then |
| Rec := |
| (Block => Cur.Block, |
| Offset => Cur.Offset, |
| Size => Rec_Len); |
| return; |
| elsif SUSP_Head (0 .. 1) = Signature ("CE") then |
| if Rec_Len < SUSP_CE'Length then |
| return; |
| end if; |
| |
| Read (SUSP_CE, Cur, Success); |
| if not Success then |
| return; |
| end if; |
| declare |
| CE_Extent : constant Unsigned_32 := Read_LE32 (SUSP_CE, 4); |
| CE_Offset : constant Unsigned_32 := Read_LE32 (SUSP_CE, 12); |
| CE_Size : constant Unsigned_32 := Read_LE32 (SUSP_CE, 20); |
| begin |
| if CE_Extent > Unsigned_32 (FSBlock'Last) or else |
| (CE_Offset > FSBlock_Size or CE_Size > FSBlock_Size) or else |
| FSBlock_Length (CE_Size) > FSBlock_Size - FSBlock_Length (CE_Offset) |
| then |
| return; |
| end if; |
| Continuation := |
| (Block => FSBlock (CE_Extent), |
| Offset => FSBlock_Length (CE_Offset), |
| Size => FSBlock_Length (CE_Size)); |
| end; |
| end if; |
| |
| Cur := Cur + Rec_Len; |
| end; |
| end loop; |
| end Find_SUSP_Record; |
| |
| 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 |
| Inode : Inode_Info renames State.Inode; |
| |
| Dir_Rec : Directory_Record; |
| begin |
| State.S := Mounted; |
| |
| Inode := (I, others => <>); |
| |
| Read (Dir_Rec, I, 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)); |
| if FSBlock (D_Extent) > FSBlock_Count'Last - FSBlock_Count (Inode.Size / FSBlock_Size) |
| then |
| Success := False; |
| return; |
| end if; |
| |
| Inode.Extents (0) := |
| (Start => FSBlock (D_Extent), |
| Count => FSBlock_Count (Inode.Size / 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; |
| |
| procedure Match_ISO_Name |
| (ISO_Name_Length : in Positive; |
| Record_Dir_Pos : in File_Offset; |
| Success : in out Boolean) |
| with |
| Pre => Is_Open (State) and File_Name'Length <= Natural'Last - 3, |
| Post => Is_Open (State) |
| is |
| function Upper_Case_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 Upper_Case_Equal; |
| |
| Dir_Pos : File_Offset := Record_Dir_Pos; |
| ISO_Name : Buffer_Type (0 .. ISO_Name_Length - 1); |
| Name_Len : Natural; |
| begin |
| -- Check if length could match. |
| -- First for the weird `.' and `..' encoding, |
| -- then for regular file names + `.' and file version `;1'. |
| if not (ISO_Name_Length = 1 and File_Name'Length <= 2) and |
| ISO_Name_Length not in File_Name'Length .. File_Name'Length + 3 |
| then |
| return; |
| end if; |
| |
| pragma Warnings |
| (GNATprove, Off, """Dir_Pos"" is set*but not used", |
| Reason => "This is the last part of the record we care about."); |
| Read |
| (State => State, |
| File_Pos => Dir_Pos, |
| Buf => ISO_Name, |
| Len => Name_Len); |
| if Name_Len /= ISO_Name_Length then |
| return; |
| end if; |
| pragma Warnings (GNATprove, On, """Dir_Pos"" is set*but not used"); |
| |
| if (Name_Len = 1 and then (ISO_Name (0) = 16#00# and File_Name = ".")) or |
| (Name_Len = 1 and then (ISO_Name (0) = 16#01# and File_Name = "..")) |
| then |
| Success := True; |
| return; |
| end if; |
| |
| -- Ignore file version `;1' |
| if Name_Len >= File_Name'Length + 2 and then |
| (ISO_Name (Name_Len - 2) = Character'Pos (';') and |
| ISO_Name (Name_Len - 1) = Character'Pos ('1')) |
| then |
| Name_Len := Name_Len - 2; |
| end if; |
| |
| -- Ignore trailing `.' |
| if Name_Len >= File_Name'Length + 1 and then |
| ISO_Name (Name_Len - 1) = Character'Pos ('.') |
| then |
| Name_Len := Name_Len - 1; |
| end if; |
| |
| Success := Name_Len = File_Name'Length and then |
| Upper_Case_Equal (File_Name, ISO_Name); |
| end Match_ISO_Name; |
| |
| procedure Match_Rock_Ridge_Name |
| (Pos : in File_Offset; |
| Len : in FSBlock_Length; |
| Success : out Boolean) |
| with |
| Pre => |
| Pos mod FSBlock_Size <= File_Offset (FSBlock_Size - Len) and |
| FSBlock_Count (Pos / FSBlock_Size) < State.Inode.Extents (0).Count, |
| Post => State = State'Old |
| is |
| Name_Rec : FS_Record; |
| begin |
| Find_SUSP_Record (State, Name_Rec, Pos, Len, "NM"); |
| if Name_Rec.Size - 5 /= File_Name'Length then |
| Success := False; |
| return; |
| end if; |
| |
| declare |
| RR_Name : Buffer_Type (0 .. File_Name'Length - 1); |
| begin |
| Read (RR_Name, Name_Rec + 5, Success); |
| Success := Success and then Equal (File_Name, RR_Name); |
| end; |
| end Match_Rock_Ridge_Name; |
| |
| 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_Head : Directory_Record; |
| Record_Dir_Pos : File_Offset := Dir_Pos; |
| Len : Natural; |
| begin |
| Read |
| (State => State, |
| File_Pos => Record_Dir_Pos, |
| Buf => Dir_Rec_Head, |
| Len => Len); |
| if Len /= Dir_Rec_Head'Length then |
| return; |
| end if; |
| |
| declare |
| Dir_Rec_Length : constant Natural := Natural (Dir_Rec_Head (0)); |
| Dir_Rec_Name_Length : constant Natural := Natural (Dir_Rec_Head (32)); |
| begin |
| if Dir_Rec_Length /= 0 then |
| |
| if Unsigned_64 (Dir_Pos) > Unsigned_64 (State.Inode.Size) - Unsigned_64 (Dir_Rec_Length) or |
| Dir_Rec_Name_Length not in 1 .. Dir_Rec_Length - Dir_Rec_Head'Length |
| then |
| return; |
| end if; |
| |
| -- First skip ISO name and try Rock Ridge extension: |
| Match_Rock_Ridge_Name |
| (Pos => Record_Dir_Pos + File_Offset (Dir_Rec_Name_Length), |
| Len => Dir_Rec_Length - Dir_Rec_Head'Length - Dir_Rec_Name_Length, |
| Success => Success); |
| if not Success then |
| Match_ISO_Name (Dir_Rec_Name_Length, Record_Dir_Pos, Success); |
| 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), |
| Size => Dir_Rec_Length); |
| exit; |
| end if; |
| |
| Dir_Pos := Dir_Pos + File_Length (Dir_Rec_Length); |
| |
| else |
| -- `Dir_Rec_Length = 0` means we have to skip to the next fs block: |
| declare |
| Block_Gap : constant File_Length := FSBlock_Size - (Dir_Pos mod FSBlock_Size); |
| begin |
| 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; |
| end; |
| 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), |
| Rec => FS_Record'(Physical, In_Block, In_Block_Space), |
| 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; |