-- 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;
            Dir_Rec_Length : File_Length;
            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;

            Dir_Rec_Length := File_Length (Dir_Rec (0));
            if Dir_Rec_Length = 0 or else
               Dir_Pos > File_Length'Last - Dir_Rec_Length or else
               (Dir_Pos + Dir_Rec_Length) mod FSBlock_Size
                  > File_Length (Directory_Record_Offset'Last) or else
               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 (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;