Start ISO9660 support
diff --git a/src/filo-fs-iso9660.adb b/src/filo-fs-iso9660.adb
new file mode 100644
index 0000000..8c1b441
--- /dev/null
+++ b/src/filo-fs-iso9660.adb
@@ -0,0 +1,381 @@
+-- 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 : in 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
+ 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 .. 190 - 1);
+ Block : FSBlock := 32;
+ begin
+ loop
+ pragma Loop_Invariant (Block < 1024);
+
+ if Part_Len < Partition_Length (Block + 1) * FSBlock_Size then
+ Success := False;
+ return;
+ end if;
+
+ Read (Volume_Descriptor (0 .. D_Ver), 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
+ return;
+ end if;
+
+ exit when Volume_Descriptor (D_Type) = D_Type_Primary;
+
+ Block := Block + 1;
+ if Block >= 1024 then
+ 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
+ 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);
+ begin
+ 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 (Read_LE32 (Dir_Rec, 2)),
+ 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
+ if Character'Pos (Str (I)) /= Buf (Buf'First + (I - Str'First)) then
+ return False;
+ end if;
+ 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);
+ declare
+ Dir_Rec : Directory_Record;
+ Dir_Rec_Name : Buffer_Type (0 .. File_Name_Max - 1);
+ Record_Dir_Pos : File_Offset := Dir_Pos;
+ Dir_Rec_Length : File_Length;
+ Inode : Inode_Index;
+ 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;
+
+ -- FIXME: need to strip trailing . and file version
+ if File_Name'Length = Natural (Dir_Rec (32)) 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,
+ Len => Len);
+ pragma Warnings (GNATprove, On, """Record_Dir_Pos"" is set*but not used");
+ if Len < File_Name'Length then
+ return;
+ end if;
+
+ Success := Str_Buf_Equal (File_Name, Dir_Rec_Name);
+ if Success then
+ Found_Inode :=
+ (Block => FSBlock (Dir_Pos / FSBlock_Size),
+ Offset => FSBlock_Index (Dir_Pos mod FSBlock_Size));
+ exit;
+ end if;
+ end if;
+
+ Dir_Rec_Length := File_Length (Dir_Rec (0));
+ if Dir_Rec_Length = 0 or
+ Dir_Pos > File_Length'Last - Dir_Rec_Length or
+ Unsigned_64 (Dir_Pos) >= Unsigned_64 (State.Inode.Size) - Unsigned_64 (Dir_Rec_Length)
+ then
+ return;
+ end if;
+ Dir_Pos := Dir_Pos + Dir_Rec_Length;
+ 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 (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;