-- Derived from GRUB  --  GRand Unified Bootloader
-- Copyright (C) 1999, 2001, 2003  Free Software Foundation, Inc.
-- Copyright (C) 2023 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 Interfaces.C.Strings;

with FILO.Blockdev;
with FILO.FS.VFS;

use Interfaces.C;

package body FILO.FS.Ext2 is

   function Is_Mounted (State : T) return Boolean is (State.S >= Mounted);
   function Is_Open (State : T) return Boolean is (State.S = File_Opened);

   --------------------------------------------------------------------------

   SUPERBLOCK_SIZE            : constant := 1024;
   SUPERBLOCK_BLOCKS          : constant := SUPERBLOCK_SIZE / BLOCK_SIZE;

   SUPERBLOCK_MAGIC           : constant := 16#ef53#;
   OLD_REV                    : constant := 0;
   DYNAMIC_REV                : constant := 1;
   FEATURE_INCOMPAT_EXTENTS   : constant := 16#0040#;
   FEATURE_INCOMPAT_64BIT     : constant := 16#0080#;

   procedure Mount
     (State    : in out T;
      Part_Len : in     Partition_Length;
      Success  :    out Boolean)
   is
      Super_Block : Buffer_Type (0 .. SUPERBLOCK_SIZE - 1) := (others => 0);
   begin
      if Part_Len < 2 * SUPERBLOCK_SIZE then
         Success := False;
         return;
      end if;

      Blockdev.Read (Super_Block, 1 * SUPERBLOCK_SIZE, Success);
      if not Success then
         return;
      end if;

      if Read_LE16 (Super_Block, 14 * 4) /= 16#ef53# then
         Success := False;
         return;
      end if;

      State.Part_Len := Part_Len;
      State.First_Data_Block := FSBlock_Offset (Read_LE32 (Super_Block, 5 * 4));

      declare
         S_Log_Block_Size : constant Unsigned_32 := Read_LE32 (Super_Block, 6 * 4);
      begin
         if S_Log_Block_Size <= Unsigned_32 (Log_Block_Size'Last - 10) then
            State.Block_Size_Bits := Log_Block_Size (S_Log_Block_Size + 10);
         else
            Success := False;
            return;
         end if;
      end;

      declare
         S_Inodes_Per_Group : constant Unsigned_32 := Read_LE32 (Super_Block, 10 * 4);
      begin
         if S_Inodes_Per_Group in 1 .. Unsigned_32 (Positive'Last) then
            State.Inodes_Per_Group := Positive (S_Inodes_Per_Group);
         else
            Success := False;
            return;
         end if;
      end;

      declare
         S_Rev_Level : constant Unsigned_32 := Read_LE32 (Super_Block, 19 * 4);
      begin
         if S_Rev_Level >= DYNAMIC_REV then
            declare
               S_Inode_Size : constant Unsigned_16 := Read_LE16 (Super_Block, 22 * 4);
            begin
               if S_Inode_Size in
                  Unsigned_16 (Inode_Size'First) .. Unsigned_16 (Inode_Size'Last)
               then
                  State.Inode_Size := Inode_Size (S_Inode_Size);
               else
                  Success := False;
                  return;
               end if;
            end;
         else
            State.Inode_Size := Inode_Size'First;
         end if;
      end;

      declare
         S_Feature_Incompat : constant Unsigned_32 := Read_LE32 (Super_Block, 24 * 4);
      begin
         State.Feature_Extents := (S_Feature_Incompat and FEATURE_INCOMPAT_EXTENTS) /= 0;
         State.Feature_64Bit     := (S_Feature_Incompat and FEATURE_INCOMPAT_64BIT) /= 0;
         if State.Feature_64Bit then
            declare
               S_Desc_Size : constant Unsigned_16 := Read_LE16 (Super_Block, 63 * 4 + 2);
            begin
               if Is_Power_Of_2 (S_Desc_Size) and then
                  S_Desc_Size in Unsigned_16 (Desc_Size'First) ..
                  Unsigned_16 (Positive'Min (Desc_Size'Last, 2 ** State.Block_Size_Bits))
               then
                  State.Desc_Size := Desc_Size (S_Desc_Size);
               else
                  Success := False;
                  return;
               end if;
            end;
         else
            State.Desc_Size := Desc_Size'First;
         end if;
      end;

      State.S := Mounted;
   end Mount;

   procedure Read_FSBlock
     (State    : in     T;
      Buf      :    out Buffer_Type;
      FSBlock  : in     FSBlock_Offset;
      Success  :    out Boolean)
   with
      Pre =>
         Is_Mounted (State) and
         Buf'Length = 2 ** State.Block_Size_Bits
   is
      Block_Size : constant Blockdev_Length := 2 ** State.Block_Size_Bits;
      Max_Block_Offset : constant FSBlock_Offset :=
         FSBlock_Offset (State.Part_Len / Block_Size - 1);
   begin
      if FSBlock > Max_Block_Offset then
         Success := False;
         return;
      end if;
      Blockdev.Read (Buf, Blockdev_Length (FSBlock) * Block_Size, Success);
   end Read_FSBlock;

   procedure Cache_FSBlock
     (State       : in out T;
      Phys        : in     FSBlock_Offset;
      Level       : in     Block_Cache_Index;
      Logical_Off : in     FSBlock_Logical;
      Cache_Start :    out Max_Block_Index;
      Cache_End   :    out Max_Block_Index;
      Success     :    out Boolean)
   with
      Post => Cache_End = Cache_Start + 2 ** State.Block_Size_Bits
   is
      Block_Size : constant Natural := 2 ** State.Block_Size_Bits;
      -- Limit cache usage depending on block size:
      Max_Level   : constant Block_Cache_Index :=
         2 ** (Log_Block_Size'Last - State.Block_Size_Bits) - 1;
      Cache_Level : constant Block_Cache_Index :=
         Block_Cache_Index'Min (Level, Max_Level);
   begin
      Cache_Start := Cache_Level * Block_Size;
      Cache_End   := Cache_Start + Block_Size - 1;
      if State.Block_Cache_Index (Cache_Level) = Logical_Off then
         Success := True;
      else
         Read_FSBlock
           (State    => State,
            Buf      => State.Block_Cache (Cache_Start .. Cache_End),
            FSBlock  => Phys,
            Success  => Success);
         State.Block_Cache_Index (Cache_Level) := Logical_Off;
      end if;
   end Cache_FSBlock;

   procedure Ext2_Block_Map
     (State       : in out T;
      Logical     : in     FSBlock_Logical;
      Physical    :    out FSBlock_Offset;
      Success     :    out Boolean)
   is
      Block_Size : constant Natural := 2 ** State.Block_Size_Bits;
      Addr_Per_Block : constant FSBlock_Logical := FSBlock_Logical (Block_Size / 4);
      Max_Addr_Per_Block : constant FSBlock_Logical := FSBlock_Logical (2 ** Log_Block_Size'Last / 4);
      type Addr_In_Block_Range is range 0 .. Max_Addr_Per_Block - 1;

      procedure Indirect_Block_Lookup
        (Indirect_Block_Phys  : in     FSBlock_Offset;
         Addr_In_Block        : in     Addr_In_Block_Range;
         Level                : in     Block_Cache_Index;
         Logical_Off          : in     FSBlock_Logical;
         Next_Physical        :    out FSBlock_Offset;
         Success              :    out Boolean)
      with
         Pre => FSBlock_Logical (Addr_In_Block) < Addr_Per_Block
      is
         Cache_Start, Cache_End : Max_Block_Index;
      begin
         Cache_FSBlock
           (State       => State,
            Phys        => Indirect_Block_Phys,
            Level       => Level,
            Logical_Off => Logical_Off,
            Cache_Start => Cache_Start,
            Cache_End   => Cache_End,
            Success     => Success);
         Next_Physical := FSBlock_Offset (Read_LE32
           (Buf => State.Block_Cache (Cache_Start .. Cache_End),
            Off => Natural (Addr_In_Block) * 4));
      end Indirect_Block_Lookup;

      Logical_Rest : FSBlock_Logical := Logical;
   begin
      if Logical_Rest < Direct_Blocks then
         Physical := FSBlock_Offset (State.Direct_Blocks (Natural (Logical)));
         Success := True;
         return;
      end if;

      Logical_Rest := Logical_Rest - Direct_Blocks;
      if Logical_Rest < Addr_Per_Block then
         Indirect_Block_Lookup
           (Indirect_Block_Phys  => FSBlock_Offset (State.Indirect_Block),
            Addr_In_Block        => Addr_In_Block_Range (Logical_Rest),
            Level                => 0,
            Logical_Off          => Logical - Logical_Rest,
            Next_Physical        => Physical,
            Success              => Success);
         return;
      end if;

      Logical_Rest := Logical_Rest - Addr_Per_Block;
      if Logical_Rest < Addr_Per_Block ** 2 then
         Indirect_Block_Lookup
           (Indirect_Block_Phys  => FSBlock_Offset (State.Double_Indirect),
            Addr_In_Block        => Addr_In_Block_Range (Logical_Rest / Addr_Per_Block),
            Level                => 1,
            Logical_Off          => Logical - Logical_Rest,
            Next_Physical        => Physical,
            Success              => Success);
         if not Success then
            return;
         end if;

         Indirect_Block_Lookup
           (Indirect_Block_Phys  => Physical,
            Addr_In_Block        => Addr_In_Block_Range (Logical_Rest mod Addr_Per_Block),
            Level                => 0,
            Logical_Off          => Logical - (Logical_Rest mod Addr_Per_Block),
            Next_Physical        => Physical,
            Success              => Success);
         return;
      end if;

      Logical_Rest := Logical_Rest - Addr_Per_Block ** 2;
      if Logical_Rest < Addr_Per_Block ** 3 then
         Indirect_Block_Lookup
           (Indirect_Block_Phys  => FSBlock_Offset (State.Triple_Indirect),
            Addr_In_Block        => Addr_In_Block_Range (Logical_Rest / Addr_Per_Block ** 2),
            Level                => 2,
            Logical_Off          => Logical - Logical_Rest,
            Next_Physical        => Physical,
            Success              => Success);
         if not Success then
            return;
         end if;

         Indirect_Block_Lookup
           (Indirect_Block_Phys  => Physical,
            Addr_In_Block        => Addr_In_Block_Range (Logical_Rest / Addr_Per_Block mod Addr_Per_Block),
            Level                => 1,
            Logical_Off          => Logical - (Logical_Rest mod Addr_Per_Block ** 2),
            Next_Physical        => Physical,
            Success              => Success);
         if not Success then
            return;
         end if;

         Indirect_Block_Lookup
           (Indirect_Block_Phys  => Physical,
            Addr_In_Block        => Addr_In_Block_Range (Logical_Rest mod Addr_Per_Block),
            Level                => 0,
            Logical_Off          => Logical - (Logical_Rest mod Addr_Per_Block),
            Next_Physical        => Physical,
            Success              => Success);
         return;
      end if;

      -- Logical address was just too high.
      Success := False;
   end Ext2_Block_Map;

   procedure Extent_Block_Map
     (State       : in out T;
      Logical     : in     FSBlock_Logical;
      Physical    :    out FSBlock_Offset;
      Success     :    out Boolean)
   is
      -- Extent blocks always start with a 12B header and contain 12B entries.
      -- Every entry starts with the number of the first logical block it
      -- covers. Entries are sorted by this number.
      -- Depth > 0 blocks have index entries, referencing further extent blocks.
      -- Depth = 0 blocks have extent entries, referencing a contiguous range
      -- of data blocks.
      --
      --                           +-----------------+
      --                       .-> | Hdr depth=0     |
      --                       |   +-----------------+
      --                       |   | Extent   0.. 12 |
      --    +-------------+    |   +-----------------+
      --    | Hdr depth=1 |    |   | Extent  13.. 13 |
      --    +-------------+    |   +-----------------+
      --    | Index     0 | --'    | Extent  14..122 |
      --    +-------------+        +-----------------+
      --    | Index   123 | --.
      --    +-------------+    |   +-----------------+
      --                       `-> | Hdr depth=0     |
      --                           +-----------------+
      --                           | Extent 123..125 |
      --                           +-----------------+
      --                           | Extent 126..234 |
      --                           +-----------------+
      --

      Extent_Header_Size : constant := 12;
      Extent_Header_Magic : constant := 16#f03a#;
      subtype Extent_Off is Natural range 0 .. Extent_Header_Size;
      subtype Extent_Idx is Natural range 1 .. (Max_Block_Index'Last + 1) / Extent_Header_Size - 1;

      function Extent_Byte_Offset (Idx : Extent_Idx; Off : Extent_Off) return Natural
      is
         (Idx * Extent_Header_Size + Off);

      function Header_Magic (Buf : Buffer_Type) return Unsigned_16
      is
         (Read_LE16 (Buf, 0))
      with
         Pre => Buf'Length >= 2;

      function Header_Entries (Buf : Buffer_Type) return Natural
      is
         (Natural (Read_LE16 (Buf, 2)))
      with
         Pre => Buf'Length >= 4;

      function Header_Depth (Buf : Buffer_Type) return Natural
      is
         (Natural (Read_LE16 (Buf, 6)))
      with
         Pre => Buf'Length >= 8;

      function Index_Logical (Buf : Buffer_Type; Idx : Extent_Idx) return FSBlock_Logical
      is
         (FSBlock_Logical (Read_LE32 (Buf, Extent_Byte_Offset (Idx, 0))))
      with
         Pre => Buf'Length >= Extent_Byte_Offset (Idx, 4);

      function Index_Physical (Buf : Buffer_Type; Idx : Extent_Idx) return FSBlock_Offset
      is
         (FSBlock_Offset
            (Shift_Left (Unsigned_64 (Read_LE16 (Buf, Extent_Byte_Offset (Idx, 8))), 32) or
                                       Unsigned_64 (Read_LE32 (Buf, Extent_Byte_Offset (Idx, 4)))))
      with
         Pre => Buf'Length >= Extent_Byte_Offset (Idx, 10);

      function Extent_Logical (Buf : Buffer_Type; Idx : Extent_Idx) return FSBlock_Logical
      renames Index_Logical;

      function Extent_Length (Buf : Buffer_Type; Idx : Extent_Idx) return FSBlock_Logical
      is
         (FSBlock_Logical (Read_LE16 (Buf, Extent_Byte_Offset (Idx, 4))))
      with
         Pre => Buf'Length >= Extent_Byte_Offset (Idx, 6);

      function Extent_Physical (Buf : Buffer_Type; Idx : Extent_Idx) return FSBlock_Offset
      is
         (FSBlock_Offset
            (Shift_Left (Unsigned_64 (Read_LE16 (Buf, Extent_Byte_Offset (Idx, 6))), 32) or
                           Unsigned_64 (Read_LE32 (Buf, Extent_Byte_Offset (Idx, 8)))))
      with
         Pre => Buf'Length >= Extent_Byte_Offset (Idx, 12);

      function Bin_Search (Buf : Buffer_Type; Refs : Extent_Idx) return Extent_Idx
      with
         Pre => Refs in 1 .. Extent_Idx (Buf'Length / Extent_Header_Size - 1) and
                  Extent_Logical (Buf, 1) <= Logical,
         Post => Bin_Search'Result in 1 .. Refs and
                  Extent_Logical (Buf, Bin_Search'Result) <= Logical
      is
         Left : Extent_Idx := 1;
         Right : Extent_Idx := Refs;
      begin
         while Left <= Right loop
            declare
               Mid : constant Extent_Idx := (Left + Right) / 2;
               Ext_Logical : constant FSBlock_Logical := Extent_Logical (Buf, Mid);
            begin
               if Logical < Ext_Logical then
                  Right := Mid - 1;
               else
                  Left := Mid + 1;
               end if;
            end;
         end loop;
         return Left - 1;
      end Bin_Search;

      procedure Next_Ref
        (Current     : in     FSBlock_Offset;
         Logical_Off : in     FSBlock_Logical;
         Depth       : in     Natural;
         Next        :    out Extent_Idx;
         Cache_Start :    out Max_Block_Index;
         Cache_End   :    out Max_Block_Index;
         Success     :    out Boolean)
      with
         Pre => Logical_Off <= Logical,
         Post => (if Success then
                     Extent_Logical (State.Block_Cache (Cache_Start .. Cache_End), Next) <= Logical)
      is
         Block_Size : constant Natural := 2 ** State.Block_Size_Bits;
         Dynamic_Max_Index : constant Natural := Block_Size / Extent_Header_Size - 1;
      begin
         Cache_FSBlock
           (State       => State,
            Phys        => Current,
            Level       => Depth,
            Logical_Off => Logical_Off,
            Cache_Start => Cache_Start,
            Cache_End   => Cache_End,
            Success     => Success);
         if not Success then
            Next := 1;
            return;
         end if;

         declare
            Hdr_Magic : constant Unsigned_16 :=
               Header_Magic (State.Block_Cache (Cache_Start .. Cache_End));
            Hdr_Entries : constant Natural :=
               Header_Entries (State.Block_Cache (Cache_Start .. Cache_End));
            Hdr_Depth : constant Natural :=
               Header_Depth (State.Block_Cache (Cache_Start .. Cache_End));
            First_Logical : constant FSBlock_Logical :=
               Extent_Logical (State.Block_Cache (Cache_Start .. Cache_End), 1);
         begin
            Success := Success and then
               Hdr_Magic = Extent_Header_Magic and then
               Hdr_Depth = Depth and then
               Hdr_Entries <= Dynamic_Max_Index and then
               First_Logical = Logical_Off;
            if not Success then
               Next := 1;
            else
               Next := Bin_Search (State.Block_Cache (Cache_Start .. Cache_End), Hdr_Entries);
            end if;
         end;
      end Next_Ref;

      Inode_Magic : constant Unsigned_16 := Header_Magic (State.Inode_Extents);
      Inode_Entries : constant Natural := Header_Entries (State.Inode_Extents);
      First_Logical : constant FSBlock_Logical := Extent_Logical (State.Inode_Extents, 1);
      Depth : Natural := Header_Depth (State.Inode_Extents);

      Cache_Start, Cache_End : Max_Block_Index;
      Logical_Off, Length : FSBlock_Logical;
      Idx : Extent_Idx;
   begin
      Success :=
         Inode_Magic = Extent_Header_Magic and then
         Inode_Entries > 0 and then
         Inode_Entries < State.Inode_Extents'Length / Extent_Header_Size and then
         First_Logical <= Logical;
      if not Success then
         Physical := 0;
         return;
      end if;

      Idx := Bin_Search (State.Inode_Extents, Inode_Entries);
      if Depth = 0 then
         Physical := Extent_Physical (State.Inode_Extents, Idx);
         Logical_Off := Extent_Logical (State.Inode_Extents, Idx);
         Length := Extent_Length (State.Inode_Extents, Idx);
      else
         Physical := Index_Physical (State.Inode_Extents, Idx);
         Logical_Off := Index_Logical (State.Inode_Extents, Idx);
         loop
            Depth := Depth - 1;
            Next_Ref
              (Current     => Physical,
               Logical_Off => Logical_Off,
               Depth       => Depth,
               Next        => Idx,
               Cache_Start => Cache_Start,
               Cache_End   => Cache_End,
               Success     => Success);
            if not Success then
               return;
            end if;

            exit when Depth = 0;
            Physical := Index_Physical (State.Block_Cache (Cache_Start .. Cache_End), Idx);
            Logical_Off := Index_Logical (State.Block_Cache (Cache_Start .. Cache_End), Idx);
         end loop;

         Physical := Extent_Physical (State.Block_Cache (Cache_Start .. Cache_End), Idx);
         Logical_Off := Extent_Logical (State.Block_Cache (Cache_Start .. Cache_End), Idx);
         Length := Extent_Length (State.Block_Cache (Cache_Start .. Cache_End), Idx);
      end if;

      Success :=
         Length > 0 and then
         Logical_Off <= FSBlock_Logical'Last - Length and then
         Logical < Logical_Off + Length;
      if Success then
         Physical := Physical + FSBlock_Offset (Logical - Logical_Off);
      end if;
   end Extent_Block_Map;

   procedure Open
     (State       : in out T;
      File_Len    :    out File_Length;
      File_Path   : in     String;
      Success     : out    Boolean)
   is
   begin
      File_Len := 0;
      Success := False;
   end Open;

   procedure Close (State : in out T) is
   begin
      State.S := Mounted;
   end Close;

   procedure Read
     (State    : in out T;
      File_Len : in     File_Length;
      File_Pos : in out File_Offset;
      Buf      :    out Buffer_Type;
      Len      :    out Natural)
   is
   begin
      Buf := (others => 0);
      Len := 0;
   end Read;

   --------------------------------------------------------------------------

   package C is new VFS (T => T, Initial => (S => Unmounted, others => <>));

   function C_Mount return int
   with
      Export,
      Convention => C,
      External_Name => "ext2fs_mount";
   function C_Mount return int
   with
      SPARK_Mode => Off
   is
   begin
      return C.C_Mount;
   end C_Mount;

   function C_Open (File_Path : Strings.chars_ptr) return int
   with
      Export,
      Convention => C,
      External_Name => "ext2fs_dir";
   function C_Open (File_Path : Strings.chars_ptr) 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 => "ext2fs_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.Ext2;