iso9660: Fix small bugs and proofs
diff --git a/src/filo-fs-iso9660.adb b/src/filo-fs-iso9660.adb
index c542ee0..a4af392 100644
--- a/src/filo-fs-iso9660.adb
+++ b/src/filo-fs-iso9660.adb
@@ -109,7 +109,9 @@
Dir_Rec_Len : in FSBlock_Length;
Searched_Sig : in SUSP_Signature)
with
- Pre => FSBlock_Index (Dir_Rec_Pos mod FSBlock_Size) <= FSBlock_Size - Dir_Rec_Len
+ Pre =>
+ Dir_Rec_Pos mod FSBlock_Size <= File_Offset (FSBlock_Size - Dir_Rec_Len) and
+ FSBlock_Count (Dir_Rec_Pos / FSBlock_Size) < State.Inode.Extents (0).Count
is
subtype Signature_Buf is Buffer_Type (0 .. 1);
function Signature (Str : SUSP_Signature) return Signature_Buf
@@ -121,7 +123,7 @@
Offset => FSBlock_Index (Dir_Rec_Pos mod FSBlock_Size),
Size => Dir_Rec_Len);
- Continuation : FS_Record := (others => <>);
+ Continuation : FS_Record := (Size => 0, others => <>);
SUSP_Head : Buffer_Type (0 .. 3);
@@ -138,7 +140,7 @@
for I in 1 .. 2**16 loop -- arbitrary limit to avoid endless loop
if Cur.Size < SUSP_Head'Length then
- if Continuation.Size = 0 then
+ if Continuation.Size < SUSP_Head'Length then
return;
else
Cur := Continuation;
@@ -175,14 +177,15 @@
CE_Offset : constant Unsigned_32 := Read_LE32 (SUSP_CE, 12);
CE_Size : constant Unsigned_32 := Read_LE32 (SUSP_CE, 20);
begin
- if (CE_Offset > FSBlock_Size or CE_Size > FSBlock_Size) or else
- CE_Offset > FSBlock_Size - CE_Size
+ if CE_Extent > Unsigned_32 (FSBlock'Last) or else
+ (CE_Offset > FSBlock_Size or CE_Size > FSBlock_Size) or else
+ FSBlock_Length (CE_Size) > FSBlock_Size - FSBlock_Length (CE_Offset)
then
return;
end if;
Continuation :=
(Block => FSBlock (CE_Extent),
- Offset => FSBlock_Index (CE_Offset),
+ Offset => FSBlock_Length (CE_Offset),
Size => FSBlock_Length (CE_Size));
end;
end if;
@@ -233,10 +236,17 @@
else
Inode.Mode := Regular;
end if;
+
Inode.Size := Inode_Length (Read_LE32 (Dir_Rec, 10));
+ if FSBlock (D_Extent) > FSBlock_Count'Last - FSBlock_Count (Inode.Size / FSBlock_Size)
+ then
+ Success := False;
+ return;
+ end if;
+
Inode.Extents (0) :=
(Start => FSBlock (D_Extent),
- Count => FSBlock_Count (Inode.Size / Inode_Length (FSBlock_Size)));
+ Count => FSBlock_Count (Inode.Size / FSBlock_Size));
State.S := File_Opened;
end;
end Open;
@@ -252,11 +262,12 @@
File_Name_Max : constant := 255;
procedure Match_ISO_Name
- (ISO_Name_Length : in Natural;
+ (ISO_Name_Length : in Positive;
Record_Dir_Pos : in File_Offset;
Success : in out Boolean)
with
- Post => State.Static = State.Static'Old
+ Pre => Is_Open (State) and File_Name'Length <= Natural'Last - 3,
+ Post => Is_Open (State)
is
function Upper_Case_Equal (Str : String; Buf : Buffer_Type) return Boolean
with
@@ -304,23 +315,23 @@
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 = "..")
+ if (Name_Len = 1 and then (ISO_Name (0) = 16#00# and File_Name = ".")) or
+ (Name_Len = 1 and then (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')
+ if Name_Len >= File_Name'Length + 2 and then
+ (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
+ if Name_Len >= File_Name'Length + 1 and then
ISO_Name (Name_Len - 1) = Character'Pos ('.')
then
Name_Len := Name_Len - 1;
@@ -332,15 +343,18 @@
procedure Match_Rock_Ridge_Name
(Pos : in File_Offset;
- Len : in Natural;
- Success : in out Boolean)
+ Len : in FSBlock_Length;
+ Success : out Boolean)
with
+ Pre =>
+ Pos mod FSBlock_Size <= File_Offset (FSBlock_Size - Len) and
+ FSBlock_Count (Pos / FSBlock_Size) < State.Inode.Extents (0).Count,
Post => State = State'Old
is
Name_Rec : FS_Record;
begin
Find_SUSP_Record (State, Name_Rec, Pos, Len, "NM");
- if Name_Rec.Size /= File_Name'Length + 5 then
+ if Name_Rec.Size - 5 /= File_Name'Length then
Success := False;
return;
end if;
@@ -415,7 +429,7 @@
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
+ Dir_Rec_Name_Length not in 1 .. Dir_Rec_Length - Dir_Rec_Head'Length
then
return;
end if;
diff --git a/src/filo-fs-iso9660.ads b/src/filo-fs-iso9660.ads
index 480ce39..20d2989 100644
--- a/src/filo-fs-iso9660.ads
+++ b/src/filo-fs-iso9660.ads
@@ -23,7 +23,7 @@
In_Root : in Boolean;
Success : out Boolean)
with
- Pre => Is_Mounted (State),
+ Pre => Is_Mounted (State) and File_Name'Length <= Natural'Last - 3,
Post => (if Success then Is_Open (State) else Is_Mounted (State));
procedure Close (State : in out T)
@@ -73,24 +73,28 @@
-- We'll use the absolute position of the dir record
subtype Inode_Index is FS_Record
with
- Dynamic_Predicate => Inode_Index.Offset <= Directory_Record_Offset'Last;
+ Dynamic_Predicate =>
+ Inode_Index.Size >= Directory_Record'Length;
type Inode_Length is range 0 .. FSBlock_Count'Last * FSBlock_Size;
type Mount_State is record
Part_Len : Partition_Length := 0;
- Root_Inode : Inode_Index := (others => <>);
+ Root_Inode : Inode_Index := (Size => Directory_Record'Length, others => <>);
end record;
type Extent is record
Start : FSBlock := 0;
Count : FSBlock_Count := 0;
- end record;
+ end record
+ with
+ Dynamic_Predicate =>
+ Start <= FSBlock_Count'Last - Count;
type Extent_Range is range 0 .. 0; -- Linux allows 100 "file sections"
type Extents is array (Extent_Range) of Extent;
type Inode_Info is record
- I : Inode_Index := (others => <>);
+ I : Inode_Index := (Size => Directory_Record'Length, others => <>);
Mode : File_Type := File_Type'First;
Size : Inode_Length := 0;
Extents : ISO9660.Extents := (Extent_Range => (others => <>));
@@ -100,7 +104,7 @@
Static : Mount_State := (others => <>);
S : State;
Inode : Inode_Info := (others => <>);
- Cur_Dir : Inode_Index := (others => <>);
+ Cur_Dir : Inode_Index := (Size => Directory_Record'Length, others => <>);
end record;
end FILO.FS.ISO9660;