-- 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 Ada.Unchecked_Conversion;
with System;
with Interfaces;
with Interfaces.C;

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_MAGIC           : constant := 16#ef53#;
   OLD_REV                    : constant := 0;
   DYNAMIC_REV                : constant := 1;

   FEATURE_INCOMPAT_EXTENTS   : constant := 16#0040#;
   FEATURE_INCOMPAT_64BIT     : constant := 16#0080#;

   EXT4_EXTENTS_FL            : constant := 16#8_0000#;

   procedure Mount
     (State    : in out T;
      Part_Len : in     Partition_Length;
      Success  :    out Boolean)
   is
      Static : Mount_State renames State.Static;
      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;

      Static.Part_Len := Part_Len;
      Static.First_Data_Block := 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
            Static.Block_Size_Bits := Log_Block_Size (S_Log_Block_Size + 10);
            Static.Block_Size := 2 ** Log_Block_Size (S_Log_Block_Size + 10);
         else
            Success := False;
            return;
         end if;
      end;
      pragma Assert_And_Cut (Success);

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

      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 Natural (S_Inode_Size) in Inode_Size and then
                  Natural (S_Inode_Size) <= Static.Block_Size
               then
                  Static.Inode_Size := Inode_Size (S_Inode_Size);
               else
                  Success := False;
                  return;
               end if;
               pragma Assert (Static.Block_Size / Static.Inode_Size <= Natural (Inode_In_Block_Count'Last));
            end;
         else
            Static.Inode_Size := Inode_Size'First;
         end if;
         Static.Inodes_Per_Block := Inode_In_Block_Count (Static.Block_Size / Static.Inode_Size);
      end;
      pragma Assert_And_Cut (Success);

      declare
         S_Feature_Incompat : constant Unsigned_32 := Read_LE32 (Super_Block, 24 * 4);
      begin
         Static.Feature_Extents := (S_Feature_Incompat and FEATURE_INCOMPAT_EXTENTS) /= 0;
         Static.Feature_64Bit   := (S_Feature_Incompat and FEATURE_INCOMPAT_64BIT) /= 0;
         if Static.Feature_64Bit then
            declare
               S_Desc_Size : constant Unsigned_16 := Read_LE16 (Super_Block, 63 * 4 + 2);
            begin
               if Natural (S_Desc_Size) in Group_Desc_Size and
                  Natural (S_Desc_Size) <= Static.Block_Size and
                  Is_Power_Of_2 (S_Desc_Size)
               then
                  Static.Group_Desc_Size := Group_Desc_Size (S_Desc_Size);
               else
                  Success := False;
                  return;
               end if;
               pragma Assert (Static.Block_Size / Static.Group_Desc_Size <= Natural (Group_In_Block_Count'Last));
            end;
            Static.Feature_64Bit := Static.Feature_64Bit and Static.Group_Desc_Size >= 64;
         else
            Static.Group_Desc_Size := Group_Desc_Size'First;
         end if;
         Static.Group_Desc_Per_Block := Group_In_Block_Count (Static.Block_Size / Static.Group_Desc_Size);
      end;
      pragma Assert_And_Cut (Success);

      State.S := Mounted;
   end Mount;

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

   procedure Cache_FSBlock
     (Static      : in     Mount_State;
      Cache       : in out Block_Cache;
      Phys        : in     FSBlock_Offset;
      Level       : in     Block_Cache_Index;
      Label       : in     Cache_Label;
      Logical     : in     Boolean := True;
      Cache_Start :    out Max_Block_Index;
      Cache_End   :    out Max_Block_Index;
      Success     :    out Boolean)
   with
      Post => Cache_End = Cache_Start + Static.Block_Size - 1
   is
      -- Limit cache usage depending on block size:
      Max_Level   : constant Block_Cache_Index := Block_Size'Last / Static.Block_Size - 1;
      Cache_Level : constant Block_Cache_Index := Block_Cache_Index'Min (Level, Max_Level);
   begin
      Cache_Start := Cache_Level * Static.Block_Size;
      Cache_End   := Cache_Start + Static.Block_Size - 1;
      if Cache.Logical (Cache_Level) = Logical and
         Cache.Label (Cache_Level) = Label
      then
         Success := True;
      else
         Read_FSBlock
           (Buf      => Cache.Buffer (Cache_Start .. Cache_End),
            FSBlock  => Phys,
            Part_Len => Static.Part_Len,
            Success  => Success);
         Cache.Logical (Cache_Level) := Logical; -- FIXME: Level needs to be part of Label
         Cache.Label (Cache_Level) := Label;
      end if;
   end Cache_FSBlock;

   procedure Cache_FSBlock
     (Static      : in     Mount_State;
      Cache       : in out Block_Cache;
      Phys        : in     FSBlock_Offset;
      Level       : in     Block_Cache_Index;
      Cache_Start :    out Max_Block_Index;
      Cache_End   :    out Max_Block_Index;
      Success     :    out Boolean)
   with
      Post => Cache_End = Cache_Start + Static.Block_Size - 1
   is
   begin
      Cache_FSBlock (Static, Cache, Phys, Level, Cache_Label (Phys),
                     False, Cache_Start, Cache_End, Success);
   end Cache_FSBlock;

   procedure Reset_Cache_Logical (Cache : in out Block_Cache) is
   begin
      for I in Block_Cache_Index loop
         if Cache.Logical (I) then
            Cache.Logical (I) := False;
            Cache.Label (I) := 0;
         end if;
      end loop;
   end Reset_Cache_Logical;

   procedure Ext2_Block_Map
     (State       : in out T;
      Logical     : in     FSBlock_Logical;
      Physical    :    out FSBlock_Offset;
      Success     :    out Boolean)
   is
      Static : constant Mount_State := State.Static;

      Direct_Blocks : constant := 12;
      type Direct_Blocks_Array is array (Natural range 0 .. Direct_Blocks - 1) of Unsigned_32;
      type Inode_Blocks is record
         Direct_Blocks     : Direct_Blocks_Array;
         Indirect_Block    : Unsigned_32;
         Double_Indirect   : Unsigned_32;
         Triple_Indirect   : Unsigned_32;
      end record
      with Object_Size => Inode_Extents'Length * 8;

      function I_Blocks is new Ada.Unchecked_Conversion (Inode_Extents, Inode_Blocks);
      function I_Blocks (State : T) return Inode_Blocks is (I_Blocks (State.Inode.Inline));

      Addr_Per_Block : constant FSBlock_Logical := FSBlock_Logical (Static.Block_Size / 4);
      Max_Addr_Per_Block : constant FSBlock_Logical := FSBlock_Logical (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 =>
            Addr_Per_Block = FSBlock_Logical (Static.Block_Size / 4) and
            FSBlock_Logical (Addr_In_Block) < Addr_Per_Block
      is
         Cache_Start, Cache_End : Max_Block_Index;
      begin
         Cache_FSBlock
           (Static      => Static,
            Cache       => State.Cache,
            Phys        => Indirect_Block_Phys,
            Level       => Level,
            Label       => Cache_Label (Logical_Off),
            Cache_Start => Cache_Start,
            Cache_End   => Cache_End,
            Success     => Success);
         Next_Physical := FSBlock_Offset (Read_LE32
           (Buf => State.Cache.Buffer (Cache_Start .. Cache_End),
            Off => Natural (Addr_In_Block) * 4));
      end Indirect_Block_Lookup;

      Logical_Rest : FSBlock_Logical := Logical;

      pragma Assert (Addr_Per_Block <= 2 ** 14);
   begin
      if Logical_Rest < Direct_Blocks then
         Physical := FSBlock_Offset (I_Blocks (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 (I_Blocks (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 (I_Blocks (State).Double_Indirect),
            Addr_In_Block        => Addr_In_Block_Range ((Logical_Rest / Addr_Per_Block) mod 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 (I_Blocks (State).Triple_Indirect),
            Addr_In_Block        => Addr_In_Block_Range ((Logical_Rest / Addr_Per_Block ** 2) mod Addr_Per_Block),
            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.
      Physical := 0;
      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
      Cache : Cache_Buffer renames State.Cache.Buffer;

      -- 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;
      Dynamic_Max_Index : constant Extent_Idx := State.Static.Block_Size / Extent_Header_Size - 1;
      subtype Extent_Depth is Natural range 0 .. 32;

      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 =>
            Buf'Length in 2 * Extent_Header_Size .. Max_Block_Index'Last and then
            Refs in 1 .. Extent_Idx (Buf'Length / Extent_Header_Size - 1) and then
            Extent_Logical (Buf, 1) <= Logical,
         Post =>
            Bin_Search'Result in 1 .. Refs and
            Extent_Logical (Buf, Bin_Search'Result) <= Logical
      is
         Left : Positive := 2;
         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;
               pragma Loop_Invariant
                 (Right <= Refs and then
                  Left in 2 .. Refs + 1 and then
                  Extent_Logical (Buf, Left - 1) <= Logical);
            end;
         end loop;
         return Left - 1;
      end Bin_Search;

      procedure Next_Ref
        (Current     : in     FSBlock_Offset;
         Logical_Off : in     FSBlock_Logical;
         Depth       : in     Extent_Depth;
         Next        :    out Extent_Idx;
         Cache_Start :    out Max_Block_Index;
         Cache_End   :    out Max_Block_Index;
         Success     :    out Boolean)
      with
         Pre =>
            Logical_Off <= Logical and
            Dynamic_Max_Index = State.Static.Block_Size / Extent_Header_Size - 1,
         Post =>
            State.Static = State.Static'Old and
            (if Success then
               Next <= Dynamic_Max_Index and then
               Cache_End = Cache_Start + State.Static.Block_Size - 1 and then
               Extent_Logical (Cache (Cache_Start .. Cache_End), Next) <= Logical)
      is
      begin
         Cache_FSBlock
           (Static      => State.Static,
            Cache       => State.Cache,
            Phys        => Current,
            Level       => Depth,
            Label       => Cache_Label (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 (Cache (Cache_Start .. Cache_End));
            Hdr_Entries : constant Natural := Header_Entries (Cache (Cache_Start .. Cache_End));
            Hdr_Depth : constant Natural := Header_Depth (Cache (Cache_Start .. Cache_End));
            First_Logical : constant FSBlock_Logical :=
               Extent_Logical (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 in Extent_Idx and then
               Hdr_Entries <= Dynamic_Max_Index and then
               First_Logical = Logical_Off;
            if not Success then
               Next := 1;
            else
               pragma Assert (Cache_End - Cache_Start + 1 = State.Static.Block_Size);
               Next := Bin_Search (Cache (Cache_Start .. Cache_End), Hdr_Entries);
            end if;
         end;
      end Next_Ref;

      Inline_Extents : Ext2.Inode_Extents renames State.Inode.Inline;
      Inode_Magic : constant Unsigned_16 := Header_Magic (Inline_Extents);
      Inode_Entries : constant Natural := Header_Entries (Inline_Extents);
      First_Logical : constant FSBlock_Logical := Extent_Logical (Inline_Extents, 1);
      Depth : Natural := Header_Depth (Inline_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 < Inline_Extents'Length / Extent_Header_Size and then
         First_Logical <= Logical and then
         Depth in Extent_Depth;
      if not Success then
         Physical := 0;
         return;
      end if;

      Idx := Bin_Search (Inline_Extents, Inode_Entries);
      if Depth = 0 then
         Physical := Extent_Physical (Inline_Extents, Idx);
         Logical_Off := Extent_Logical (Inline_Extents, Idx);
         Length := Extent_Length (Inline_Extents, Idx);
      else
         Physical := Index_Physical (Inline_Extents, Idx);
         Logical_Off := Index_Logical (Inline_Extents, Idx);
         loop
            pragma Loop_Invariant
              (State.Static = State.Static'Loop_Entry and then
               Depth > 0 and then
               Depth in Extent_Depth and then
               Logical_Off <= Logical);
            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 (Cache (Cache_Start .. Cache_End), Idx);
            Logical_Off := Index_Logical (Cache (Cache_Start .. Cache_End), Idx);
         end loop;

         Physical := Extent_Physical (Cache (Cache_Start .. Cache_End), Idx);
         Logical_Off := Extent_Logical (Cache (Cache_Start .. Cache_End), Idx);
         Length := Extent_Length (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 and then
         FSBlock_Offset (Logical - Logical_Off) <= FSBlock_Offset'Last - Physical;
      if Success then
         Physical := Physical + FSBlock_Offset (Logical - Logical_Off);
      end if;
   end Extent_Block_Map;

   procedure Parse_Group
     (Static      : in     Mount_State;
      Table_Start :    out FSBlock_Offset;
      Buf         : in     Buffer_Type;
      Success     :    out Boolean)
   with
      Pre =>
         Buf'Length >= Group_Desc_Size'First and
         (if Static.Feature_64Bit then Buf'Length >= 64)
   is
      Inode_Table_Block : constant Unsigned_64 :=
         (if Static.Feature_64Bit
          then Shift_Left (Unsigned_64 (Read_LE32 (Buf, 40)), 32)
          else 0)
         or
         Unsigned_64 (Read_LE32 (Buf, 8));
   begin
         if Inode_Table_Block >= Unsigned_64 (Static.First_Data_Block) and
            Inode_Table_Block <= Unsigned_64 (FSBlock_Offset'Last)
         then
            Table_Start := FSBlock_Offset (Inode_Table_Block);
            Success := True;
         else
            Table_Start := 0;
            Success := False;
         end if;
   end Parse_Group;

   procedure Parse_Inode
     (Static   : in     Mount_State;
      Inode    : in out Inode_Info;
      Buf      : in     Buffer_Type;
      Success  :    out Boolean)
   with
      Pre => Buf'Length >= Inode_Size'First
   is
      S_IFMT   : constant := 8#170000#;
      S_IFDIR  : constant := 8#040000#;
      S_IFREG  : constant := 8#100000#;
      S_IFLNK  : constant := 8#120000#;

      I_Mode      : constant Unsigned_16 := Read_LE16 (Buf, 0);
      I_Blocks    : constant Unsigned_32 := Read_LE32 (Buf, 28);
      I_Flags     : constant Unsigned_32 := Read_LE32 (Buf, 32);
      I_File_ACL  : constant Unsigned_32 := Read_LE32 (Buf, 104);
   begin
      case I_Mode and S_IFMT is
         when S_IFDIR => Inode.Mode := Dir;
         when S_IFREG => Inode.Mode := Regular;
         when S_IFLNK => Inode.Mode := Link;
         when others  => Success := False; return;
      end case;

      if Inode.Mode = Link and
         ((I_File_ACL = 0 and I_Blocks = 0) or
          (I_File_ACL /= 0 and I_Blocks = 2 ** (Static.Block_Size_Bits - 9)))
      then
         Inode.Mode := Fast_Link;
      end if;

      declare
         I_Size : constant Unsigned_64 :=
            (if Inode.Mode = Regular
             then Shift_Left (Unsigned_64 (Read_LE32 (Buf, 108)), 32)
             else 0) or
            Unsigned_64 (Read_LE32 (Buf, 4));
      begin
         if I_Size > Unsigned_64 (Inode_Length'Last) then
            Success := False;
            return;
         end if;
         Inode.Size := Inode_Length (I_Size);
      end;

      Inode.Use_Extents := Static.Feature_Extents and (I_Flags and EXT4_EXTENTS_FL) /= 0;
      Inode.Inline := Buf (Buf'First + 40 .. Buf'First + 100 - 1);

      Success := True;
   end Parse_Inode;

   procedure Open
     (State    : in out T;
      Inode    : in     Inode_Index;
      Success  : out Boolean)
   with
      Pre => Is_Mounted (State),
      Post => Success = Is_Open (State)
   is
      Static : Mount_State renames State.Static;
      Cache : Cache_Buffer renames State.Cache.Buffer;

      Group : constant Group_Index := Group_Index ((Inode - 1) / Static.Inodes_Per_Group);
      Group_Block : constant FSBlock_Offset :=
         1 + FSBlock_Offset (Static.First_Data_Block) + FSBlock_Offset (Group / Static.Group_Desc_Per_Block);
      Group_In_Block : constant Group_In_Block_Index := Group_In_Block_Index (Group mod Static.Group_Desc_Per_Block);
      Group_In_Block_Offset : constant Natural := Natural (Group_In_Block) * Static.Group_Desc_Size;

      Cache_Start, Cache_End : Max_Block_Index;
      First_Table_Block : FSBlock_Offset;
   begin
      State.S := Mounted;

      Cache_FSBlock
        (Static      => Static,
         Cache       => State.Cache,
         Phys        => Group_Block,
         Level       => Natural (Group_Index'Min (Group / Static.Group_Desc_Per_Block,
                                                   Group_Index (Block_Cache_Index'Last))),
         Cache_Start => Cache_Start,
         Cache_End   => Cache_End,
         Success     => Success);
      Success := Success and then
         -- TODO: Prove this using a predicate on Mount_State:
         Cache_Start <= Cache_End - Group_In_Block_Offset - Static.Group_Desc_Size + 1;
      if not Success then
         return;
      end if;

      Parse_Group
        (Static      => Static,
         Table_Start => First_Table_Block,
         Buf         => Cache (Cache_Start + Group_In_Block_Offset ..
                                 Cache_Start + Group_In_Block_Offset + Static.Group_Desc_Size - 1),
         Success     => Success);
      if not Success then
         return;
      end if;

      declare
         Inode_In_Group : constant Inode_In_Group_Index :=
            Inode_In_Group_Index ((Inode - 1) mod Static.Inodes_Per_Group);

         Inode_Block : constant FSBlock_Offset := FSBlock_Offset (Inode_In_Group / Static.Inodes_Per_Block);
         Inode_In_Block : constant Inode_In_Block_Index :=
            Inode_In_Block_Index (Inode_In_Group mod Static.Inodes_Per_Block);
         Inode_In_Block_Offset : constant Natural :=
            Natural (Inode_In_Block) * Static.Inode_Size;
      begin
         if First_Table_Block > FSBlock_Offset'Last - Inode_Block then
            Success := False;
            return;
         end if;

         Cache_FSBlock
           (Static      => Static,
            Cache       => State.Cache,
            Phys        => FSBlock_Offset (First_Table_Block + Inode_Block),
            Level       => Block_Cache_Index'Last,
            Cache_Start => Cache_Start,
            Cache_End   => Cache_End,
            Success     => Success);
         Success := Success and then
            -- TODO: Prove this using a predicate on Mount_State:
            Cache_Start <= Cache_End - Inode_In_Block_Offset - Static.Inode_Size + 1;
         if not Success then
            return;
         end if;

         Parse_Inode
           (Static   => State.Static,
            Inode    => State.Inode,
            Buf      => Cache (Cache_Start + Inode_In_Block_Offset ..
                                 Cache_Start + Inode_In_Block_Offset + Static.Inode_Size - 1),
            Success  => Success);

         if Success then
            State.Inode.I := Inode;
            Reset_Cache_Logical (State.Cache);
            State.S := File_Opened;
         end if;
      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;
      Root_Inode : constant := 2;

      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;

      File_Inode : Inode_Index;
      File_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 := Root_Inode;
         end if;
         Open (State, State.Cur_Dir, Success);
         if not Success then
            return;
         end if;
      end if;

      -- Lookup file in opened dir:
      --
      File_Pos := 0;
      Success := False;
      loop
         pragma Loop_Invariant (Is_Open (State) and not Success);
         declare
            Dir_Entry_Header_Length : constant := 4 + 2 + 1 + 1;
            Dir_Entry_Header : Buffer_Type (0 .. Dir_Entry_Header_Length - 1);
            Dir_Entry_Name : Buffer_Type (0 .. File_Name_Max - 1);
            Entry_File_Pos : File_Offset := File_Pos;
            Dir_Entry_Length : File_Length;
            Inode : Inode_0_Index;
            Len : Natural;
         begin
            Read
              (State    => State,
               File_Pos => Entry_File_Pos,
               Buf      => Dir_Entry_Header,
               Len      => Len);
            if Len < Dir_Entry_Header_Length then
               return;
            end if;

            -- Only check filenames of exact same length
            Inode := Inode_0_Index (Read_LE32 (Dir_Entry_Header, 0));
            if Inode > Root_Inode and then
               File_Name'Length = Natural (Dir_Entry_Header (6))
            then
               pragma Warnings
                 (GNATprove, Off, """Entry_File_Pos"" is set*but not used",
                  Reason => "We only care about intermedidate values.");
               Read
                 (State    => State,
                  File_Pos => Entry_File_Pos,
                  Buf      => Dir_Entry_Name,
                  Len      => Len);
               pragma Warnings (GNATprove, On, """Entry_File_Pos"" is set*but not used");
               if Len < File_Name'Length then
                  return;
               end if;

               Success := Str_Buf_Equal (File_Name, Dir_Entry_Name);
               if Success then
                  File_Inode := Inode;
                  exit;
               end if;
            end if;

            Dir_Entry_Length := File_Length (Read_LE16 (Dir_Entry_Header, 4));
            if File_Pos > File_Length'Last - Dir_Entry_Length or
               Unsigned_64 (File_Pos) >= Unsigned_64 (State.Inode.Size) - Unsigned_64 (Dir_Entry_Length)
            then
               return;
            end if;
            File_Pos := File_Pos + Dir_Entry_Length;
         end;
      end loop;
      pragma Assert_And_Cut (Success and Is_Mounted (State));

      Open (State, File_Inode, Success);
      if not Success then
         return;
      end if;

      if State.Inode.Mode = Dir then
         State.Cur_Dir := File_Inode;
      end if;

      Success := State.Inode.Size <= Inode_Length (File_Length'Last);
      if Success then
         File_Len := File_Length (State.Inode.Size);
         File_Type := (case State.Inode.Mode is
                        when Dir                => FS.Dir,
                        when Regular            => FS.Regular,
                        when Link .. Fast_Link  => FS.Link);
      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;
      Cache : Cache_Buffer renames State.Cache.Buffer;

      Pos : Natural;
   begin
      if State.Inode.Mode = Fast_Link then
         if State.Inode.Size > Inode_Length (State.Inode.Inline'Length) or
            Inode_Length (File_Pos) >= State.Inode.Size then
            Len := 0;
         else
            Len := Natural'Min (Buf'Length, Natural (State.Inode.Size) - Natural (File_Pos));
         end if;
         Buf (Buf'First .. Buf'First + Len - 1) :=
            State.Inode.Inline (Natural (File_Pos) .. Natural (File_Pos) + Len - 1);
         Buf (Buf'First + Len .. Buf'Last) := (others => 16#00#);
         File_Pos := File_Pos + File_Length (Len);
         return;
      end if;

      Len := 0;
      Pos := Buf'First;
      while Pos <= Buf'Last and Inode_Length (File_Pos) < State.Inode.Size loop
         declare
            In_Block : constant Max_Block_Index := Natural (File_Pos) mod Static.Block_Size;
            Logical : constant FSBlock_Logical := FSBlock_Logical (File_Pos / File_Offset (Static.Block_Size));
            In_Block_Space : constant Natural := Natural (Static.Block_Size) - In_Block;
            In_File_Space : constant Inode_Length := State.Inode.Size - Inode_Length (File_Pos);
            In_Buf_Space : constant Natural := Buf'Last - Pos + 1;
            Len_Here : Natural;
         begin
            Len_Here := In_Block_Space;
            if In_File_Space < Inode_Length (Len_Here) then
               Len_Here := Natural (In_File_Space);
            end if;
            if In_Buf_Space < Len_Here then
               Len_Here := In_Buf_Space;
            end if;

            declare
               Last : constant Index_Type := Pos + Len_Here - 1;
               Cache_Start, Cache_End : Max_Block_Index;
               Physical : FSBlock_Offset;
               Success : Boolean;
            begin
               if State.Inode.Use_Extents then
                  Extent_Block_Map (State, Logical, Physical, Success);
               else
                  Ext2_Block_Map (State, Logical, Physical, Success);
               end if;
               if Success then
                  Cache_FSBlock
                    (Static      => Static,
                     Cache       => State.Cache,
                     Phys        => Physical,
                     Level       => Block_Cache_Index'Last,
                     Cache_Start => Cache_Start,
                     Cache_End   => Cache_End,
                     Success     => Success);
               end if;
               exit when not Success;

               Buf (Pos .. Last) := Cache (
                  Cache_Start + In_Block .. Cache_Start + In_Block + Len_Here - 1);
               File_Pos := File_Pos + File_Length (Len_Here);
               Pos := Pos + Len_Here;
               Len := Len + Len_Here;
            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 => "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 : System.Address) return int
   with
      Export,
      Convention => C,
      External_Name => "ext2fs_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 => "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;