src/filo-fs-iso9660.adb - filo-scratch - Gitiles

 -- 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 => FSBlock_Index (Dir_Rec_Pos mod FSBlock_Size) <= FSBlock_Size - Dir_Rec_Len
    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 := (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 = 0 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_Offset > FSBlock_Size or CE_Size > FSBlock_Size) or else
                      CE_Offset > FSBlock_Size - CE_Size
                   then
                      return;
                   end if;
                   Continuation :=
                     (Block  => FSBlock (CE_Extent),
                      Offset => FSBlock_Index (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));
          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;

       procedure Match_ISO_Name
         (ISO_Name_Length   : in     Natural;
          Record_Dir_Pos    : in     File_Offset;
          Success           : in out Boolean)
       with
          Post => State.Static = State.Static'Old
       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 ISO_Name (0) = 16#00# and File_Name = ".") or
             (Name_Len = 1 and 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
             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
             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     Natural;
          Success  : in out Boolean)
       with
          Post => State = State'Old
       is
          Name_Rec : FS_Record;
       begin
          Find_SUSP_Record (State, Name_Rec, Pos, Len, "NM");
          if Name_Rec.Size /= File_Name'Length + 5 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 > 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;
	-- 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 => FSBlock_Index (Dir_Rec_Pos mod FSBlock_Size) <= FSBlock_Size - Dir_Rec_Len
	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 := (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 = 0 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_Offset > FSBlock_Size or CE_Size > FSBlock_Size) or else
	CE_Offset > FSBlock_Size - CE_Size
	then
	return;
	end if;
	Continuation :=
	(Block => FSBlock (CE_Extent),
	Offset => FSBlock_Index (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));
	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;

	procedure Match_ISO_Name
	(ISO_Name_Length : in Natural;
	Record_Dir_Pos : in File_Offset;
	Success : in out Boolean)
	with
	Post => State.Static = State.Static'Old
	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 ISO_Name (0) = 16#00# and File_Name = ".") or
	(Name_Len = 1 and 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
	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
	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 Natural;
	Success : in out Boolean)
	with
	Post => State = State'Old
	is
	Name_Rec : FS_Record;
	begin
	Find_SUSP_Record (State, Name_Rec, Pos, Len, "NM");
	if Name_Rec.Size /= File_Name'Length + 5 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 > 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;