-- 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;
      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 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;

      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;


                  Match_ISO_Name (Dir_Rec_Name_Length, Record_Dir_Pos, Success);

                  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;