ext2: Re-work file-name version of Open() to ease proving
diff --git a/src/filo-fs-ext2.adb b/src/filo-fs-ext2.adb
index d7bd018..3276cdd 100644
--- a/src/filo-fs-ext2.adb
+++ b/src/filo-fs-ext2.adb
@@ -691,7 +691,7 @@
Inode : in Inode_Index;
Success : out Boolean)
with
- Pre => Is_Mounted (State) and not Is_Open (State),
+ Pre => Is_Mounted (State),
Post => Success = Is_Open (State)
is
Static : Mount_State renames State.Static;
@@ -706,6 +706,8 @@
Cache_Start, Cache_End : Max_Block_Index;
First_Table_Block : FSBlock_Offset;
begin
+ State.S := Mounted;
+
Cache_FSBlock
(Static => Static,
Cache => State.Cache,
@@ -788,7 +790,10 @@
File_Name_Max : constant := 255;
Root_Inode : constant := 2;
- function Str_Buf_Equal (Str : String; Buf : Buffer_Type) return Boolean is
+ 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
@@ -830,58 +835,72 @@
--
File_Pos := 0;
Success := False;
- while Unsigned_64 (File_Pos) < Unsigned_64 (State.Inode.Size) loop
+ loop
+ pragma Loop_Invariant (Is_Open (State) and not Success);
declare
Dir_Entry_Header_Length : constant := 4 + 2 + 1 + 1;
- subtype Dir_Entry_Index is Natural
- range 0 .. Dir_Entry_Header_Length + File_Name_Max - 1;
- Dir_Entry : Buffer_Type (Dir_Entry_Index);
+ 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 (0 .. 7),
+ Buf => Dir_Entry_Header,
Len => Len);
if Len < Dir_Entry_Header_Length then
return;
end if;
-- Only check filenames of exact same length
- if Read_LE32 (Dir_Entry, 0) > Root_Inode and then
- File_Name'Length = Natural (Dir_Entry (6))
+ 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 (8 .. 8 + File_Name'Length - 1),
+ 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;
- File_Inode := Inode_Index (Read_LE32 (Dir_Entry, 0));
- Success := Str_Buf_Equal (File_Name, Dir_Entry (8 .. 8 + File_Name'Length - 1));
- exit when Success;
+ Success := Str_Buf_Equal (File_Name, Dir_Entry_Name);
+ if Success then
+ File_Inode := Inode;
+ exit;
+ end if;
end if;
- File_Pos := File_Pos + File_Length (Read_LE16 (Dir_Entry, 4));
+ 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));
- if Success then
- 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;
+ Open (State, File_Inode, Success);
+ if not Success then
+ return;
end if;
- Success := Unsigned_64 (State.Inode.Size) <= Unsigned_64 (File_Length'Last);
+ 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