src/filo-fs-vfs.adb - filo-scratch - Gitiles

 with Ada.Unchecked_Conversion;
 with Interfaces.C;

 use Interfaces.C;

 package body FILO.FS.VFS is

    State : T := Initial;

    Path_Max : constant := 4096;
    Max_Link_Depth : constant := 32;

    subtype Path_Length is Natural range 0 .. Path_Max;
    subtype Path_Index_Plus is Positive range 1 .. Path_Max + 1;
    subtype Path_Index is Path_Index_Plus range 1 .. Path_Max;

    subtype Path_Buffer is Buffer_Type (Path_Index)
    with
       Object_Size => Path_Max * 8;
    Path_Buf : Path_Buffer;

    subtype Path_String is String (Path_Index)
    with
       Object_Size => Path_Max * 8;
    Path : Path_String;

    function C_Mount return int
    with
       SPARK_Mode => Off
    is
       Success : Boolean;
    begin
       if not Is_Mounted (State) then
          State := Initial; -- Work around not having an unmount in FILO.
       end if;
       Mount (State, Part_Len, Success);
       return (if Success then 1 else 0);
    end C_Mount;

    procedure Open (File_Path : System.Address; Ret : out int)
    is
       function Str_Len (S : System.Address) return Natural;
       function Str_Len (S : System.Address) return Natural
       with
          SPARK_Mode => Off
       is
          Buf : Buffer_Type (1 .. Path_Max + 1)
          with
             Convention => C,
             Address => S;
       begin
          for I in Buf'Range loop
             if Buf (I) = 16#00# then
                return I - 1;
             end if;
          end loop;
          return Path_Max + 1;
       end Str_Len;

       procedure Str_Cpy (Dst : out String; Src : in System.Address);
       procedure Str_Cpy (Dst : out String; Src : in System.Address)
       with
          SPARK_Mode => Off
       is
          Src_String : String (Dst'Range)
          with
             Convention => C,
             Address => Src;
       begin
          Dst := Src_String;
       end Str_Cpy;

       function Component_Start (Path : Path_String; Pos : Positive) return Path_Index_Plus is
       begin
          for I in Pos .. Path'Last loop
             if Path (I) /= '/' then
                return I;
             end if;
          end loop;
          return Path'Last + 1;
       end Component_Start;

       function Component_End (Path : Path_String; Start : Path_Index_Plus; Limit : Path_Index) return Path_Length
       with
          Post => Component_End'Result <= Limit
       is
       begin
          for I in Start .. Limit loop
             if Path (I) = '/' or Is_Space (Path (I)) then
                return I - 1;
             end if;
          end loop;
          return Limit;
       end Component_End;

       function Path_End (Path : Path_String; Start : Path_Index) return Path_Length is
       begin
          for I in Start .. Path'Last loop
             if Is_Space (Path (I)) then
                return I - 1;
             end if;
          end loop;
          return Path'Last;
       end Path_End;

       procedure Read_Link
         (Path        : in out Path_String;
          Rest_First  : in     Path_Index_Plus;
          Rest_Last   : in     Path_Index;
          Link_Len    : in     Positive;
          Success     :    out Boolean)
       with
          Pre =>
             Is_Open (State) and
             Rest_First - 1 <= Rest_Last,
          Post =>
             Is_Open (State)
       is
          function As_String is new Ada.Unchecked_Conversion (Path_Buffer, Path_String);

          Rest_Len : constant Natural := Rest_Last - Rest_First + 1;
          File_Pos : File_Offset := 0;
          Read_Len : Natural;
       begin
          if Path_Max - Rest_Len < Link_Len then
             Success := False;
             return;
          end if;

          pragma Warnings
            (GNATprove, Off, """File_Pos"" is set*but not used",
             Reason => "We only read the link at once, during path walks.");
          Read
            (State    => State,
             File_Pos => File_Pos,
             Buf      => Path_Buf (1 .. Link_Len),
             Len      => Read_Len);
          pragma Warnings (GNATprove, On, """File_Pos"" is set*but not used");
          Success := Read_Len = Link_Len;

          if Success then
             Path (Link_Len + 1 .. Link_Len + Rest_Len) := Path (Rest_First .. Rest_Last);
             Path (Link_Len + Rest_Len + 1 .. Path'Last) := (others => ' ');
             Path (1 .. Link_Len) := As_String (Path_Buf) (1 .. Link_Len);
          end if;
       end Read_Link;

       Path_Len : constant Natural := Str_Len (File_Path);
       Root_Dir : Boolean := True;
    begin
       Ret := 0;

       if not Is_Mounted (State) or Path_Len > Path_Max then
          return;
       end if;

       if Is_Open (State) then
          Close (State);
       end if;

       Str_Cpy (Path (1 .. Path_Len), File_Path);
       Path (Path_Len + 1 .. Path'Last) := (others => ' ');

       Link_Loop :
       for I in 1 .. Max_Link_Depth loop
          pragma Loop_Invariant (Is_Mounted (State));
          declare
             Path_Pos : Path_Index_Plus := Path'First;
             Path_Last : constant Path_Length := Path_End (Path, Path_Pos);
          begin
             if Path_Last < Path'First then
                return;
             end if;

             Path_Loop :
             loop
                pragma Loop_Invariant
                  (Is_Mounted (State) and
                   Path_Last in Path'Range);
                declare
                   Comp_First : constant Path_Index_Plus := Component_Start (Path, Path_Pos);
                   Comp_Last : constant Path_Length := Component_End (Path, Comp_First, Path_Last);
                   File_Type : FS.File_Type;
                   File_Len : File_Length;
                   Success : Boolean;
                begin
                   if Comp_First > Comp_Last then
                      return;
                   end if;

                   Open
                     (State       => State,
                      File_Len    => File_Len,
                      File_Type   => File_Type,
                      File_Name   => Path (Comp_First .. Comp_Last),
                      In_Root     => Root_Dir,
                      Success     => Success);
                   if not Success then
                      return;
                   end if;
                   Root_Dir := False;

                   case File_Type is
                      when Dir =>
                         if Comp_Last = Path_Last then
                            Close (State);
                            return;
                         end if;
                         Path_Pos := Comp_Last + 1;
                      when Regular =>
                         if Comp_Last = Path_Last then
                            Set_File_Max (File_Len);
                            Ret := 1;
                            return;
                         else
                            Close (State);
                            return;
                         end if;
                      when Link =>
                         if File_Len = 0 or File_Len > Path_Max then
                            Success := False;
                         else
                            Read_Link
                              (Path        => Path,
                               Rest_First  => Comp_Last + 1,
                               Rest_Last   => Path_Last,
                               Link_Len    => Positive (File_Len),
                               Success     => Success);
                         end if;
                         Close (State);
                         if not Success then
                            return;
                         end if;
                         Root_Dir := Path (1) = '/';
                         exit Path_Loop; -- continue in Link_Loop
                   end case;
                end;
             end loop Path_Loop;
          end;
       end loop Link_Loop;
    end Open;

    function C_Open (File_Path : System.Address) return int
    with
       SPARK_Mode => Off
    is
       Ret : int;
    begin
       if Is_Mounted (State) then
          Open (File_Path, Ret);
       else
          Ret := 0;
       end if;
       return Ret;
    end C_Open;

    procedure C_Close is
    begin
       if Is_Open (State) then
          Close (State);
       end if;
    end C_Close;

    function C_Read (Buf : System.Address; Len : int) return int
    with
       SPARK_Mode => Off
    is
       subtype Buffer_Range is Natural range 0 .. Integer (Len) - 1;
       Buffer : Buffer_Type (Buffer_Range)
       with
          Convention => C,
          Address => Buf;

       File_Pos : File_Offset := FILO.FS.File_Pos;
       Read_Len : Natural;
    begin
       if Is_Open (State) then
          Read (State, File_Pos, Buffer, Read_Len);
          Set_File_Pos (File_Pos);
       else
          Read_Len := 0;
       end if;
       return int (Read_Len);
    end C_Read;

 end FILO.FS.VFS;
	with Ada.Unchecked_Conversion;
	with Interfaces.C;

	use Interfaces.C;

	package body FILO.FS.VFS is

	State : T := Initial;

	Path_Max : constant := 4096;
	Max_Link_Depth : constant := 32;

	subtype Path_Length is Natural range 0 .. Path_Max;
	subtype Path_Index_Plus is Positive range 1 .. Path_Max + 1;
	subtype Path_Index is Path_Index_Plus range 1 .. Path_Max;

	subtype Path_Buffer is Buffer_Type (Path_Index)
	with
	Object_Size => Path_Max * 8;
	Path_Buf : Path_Buffer;

	subtype Path_String is String (Path_Index)
	with
	Object_Size => Path_Max * 8;
	Path : Path_String;

	function C_Mount return int
	with
	SPARK_Mode => Off
	is
	Success : Boolean;
	begin
	if not Is_Mounted (State) then
	State := Initial; -- Work around not having an unmount in FILO.
	end if;
	Mount (State, Part_Len, Success);
	return (if Success then 1 else 0);
	end C_Mount;

	procedure Open (File_Path : System.Address; Ret : out int)
	is
	function Str_Len (S : System.Address) return Natural;
	function Str_Len (S : System.Address) return Natural
	with
	SPARK_Mode => Off
	is
	Buf : Buffer_Type (1 .. Path_Max + 1)
	with
	Convention => C,
	Address => S;
	begin
	for I in Buf'Range loop
	if Buf (I) = 16#00# then
	return I - 1;
	end if;
	end loop;
	return Path_Max + 1;
	end Str_Len;

	procedure Str_Cpy (Dst : out String; Src : in System.Address);
	procedure Str_Cpy (Dst : out String; Src : in System.Address)
	with
	SPARK_Mode => Off
	is
	Src_String : String (Dst'Range)
	with
	Convention => C,
	Address => Src;
	begin
	Dst := Src_String;
	end Str_Cpy;

	function Component_Start (Path : Path_String; Pos : Positive) return Path_Index_Plus is
	begin
	for I in Pos .. Path'Last loop
	if Path (I) /= '/' then
	return I;
	end if;
	end loop;
	return Path'Last + 1;
	end Component_Start;

	function Component_End (Path : Path_String; Start : Path_Index_Plus; Limit : Path_Index) return Path_Length
	with
	Post => Component_End'Result <= Limit
	is
	begin
	for I in Start .. Limit loop
	if Path (I) = '/' or Is_Space (Path (I)) then
	return I - 1;
	end if;
	end loop;
	return Limit;
	end Component_End;

	function Path_End (Path : Path_String; Start : Path_Index) return Path_Length is
	begin
	for I in Start .. Path'Last loop
	if Is_Space (Path (I)) then
	return I - 1;
	end if;
	end loop;
	return Path'Last;
	end Path_End;

	procedure Read_Link
	(Path : in out Path_String;
	Rest_First : in Path_Index_Plus;
	Rest_Last : in Path_Index;
	Link_Len : in Positive;
	Success : out Boolean)
	with
	Pre =>
	Is_Open (State) and
	Rest_First - 1 <= Rest_Last,
	Post =>
	Is_Open (State)
	is
	function As_String is new Ada.Unchecked_Conversion (Path_Buffer, Path_String);

	Rest_Len : constant Natural := Rest_Last - Rest_First + 1;
	File_Pos : File_Offset := 0;
	Read_Len : Natural;
	begin
	if Path_Max - Rest_Len < Link_Len then
	Success := False;
	return;
	end if;

	pragma Warnings
	(GNATprove, Off, """File_Pos"" is set*but not used",
	Reason => "We only read the link at once, during path walks.");
	Read
	(State => State,
	File_Pos => File_Pos,
	Buf => Path_Buf (1 .. Link_Len),
	Len => Read_Len);
	pragma Warnings (GNATprove, On, """File_Pos"" is set*but not used");
	Success := Read_Len = Link_Len;

	if Success then
	Path (Link_Len + 1 .. Link_Len + Rest_Len) := Path (Rest_First .. Rest_Last);
	Path (Link_Len + Rest_Len + 1 .. Path'Last) := (others => ' ');
	Path (1 .. Link_Len) := As_String (Path_Buf) (1 .. Link_Len);
	end if;
	end Read_Link;

	Path_Len : constant Natural := Str_Len (File_Path);
	Root_Dir : Boolean := True;
	begin
	Ret := 0;

	if not Is_Mounted (State) or Path_Len > Path_Max then
	return;
	end if;

	if Is_Open (State) then
	Close (State);
	end if;

	Str_Cpy (Path (1 .. Path_Len), File_Path);
	Path (Path_Len + 1 .. Path'Last) := (others => ' ');

	Link_Loop :
	for I in 1 .. Max_Link_Depth loop
	pragma Loop_Invariant (Is_Mounted (State));
	declare
	Path_Pos : Path_Index_Plus := Path'First;
	Path_Last : constant Path_Length := Path_End (Path, Path_Pos);
	begin
	if Path_Last < Path'First then
	return;
	end if;

	Path_Loop :
	loop
	pragma Loop_Invariant
	(Is_Mounted (State) and
	Path_Last in Path'Range);
	declare
	Comp_First : constant Path_Index_Plus := Component_Start (Path, Path_Pos);
	Comp_Last : constant Path_Length := Component_End (Path, Comp_First, Path_Last);
	File_Type : FS.File_Type;
	File_Len : File_Length;
	Success : Boolean;
	begin
	if Comp_First > Comp_Last then
	return;
	end if;

	Open
	(State => State,
	File_Len => File_Len,
	File_Type => File_Type,
	File_Name => Path (Comp_First .. Comp_Last),
	In_Root => Root_Dir,
	Success => Success);
	if not Success then
	return;
	end if;
	Root_Dir := False;

	case File_Type is
	when Dir =>
	if Comp_Last = Path_Last then
	Close (State);
	return;
	end if;
	Path_Pos := Comp_Last + 1;
	when Regular =>
	if Comp_Last = Path_Last then
	Set_File_Max (File_Len);
	Ret := 1;
	return;
	else
	Close (State);
	return;
	end if;
	when Link =>
	if File_Len = 0 or File_Len > Path_Max then
	Success := False;
	else
	Read_Link
	(Path => Path,
	Rest_First => Comp_Last + 1,
	Rest_Last => Path_Last,
	Link_Len => Positive (File_Len),
	Success => Success);
	end if;
	Close (State);
	if not Success then
	return;
	end if;
	Root_Dir := Path (1) = '/';
	exit Path_Loop; -- continue in Link_Loop
	end case;
	end;
	end loop Path_Loop;
	end;
	end loop Link_Loop;
	end Open;

	function C_Open (File_Path : System.Address) return int
	with
	SPARK_Mode => Off
	is
	Ret : int;
	begin
	if Is_Mounted (State) then
	Open (File_Path, Ret);
	else
	Ret := 0;
	end if;
	return Ret;
	end C_Open;

	procedure C_Close is
	begin
	if Is_Open (State) then
	Close (State);
	end if;
	end C_Close;

	function C_Read (Buf : System.Address; Len : int) return int
	with
	SPARK_Mode => Off
	is
	subtype Buffer_Range is Natural range 0 .. Integer (Len) - 1;
	Buffer : Buffer_Type (Buffer_Range)
	with
	Convention => C,
	Address => Buf;

	File_Pos : File_Offset := FILO.FS.File_Pos;
	Read_Len : Natural;
	begin
	if Is_Open (State) then
	Read (State, File_Pos, Buffer, Read_Len);
	Set_File_Pos (File_Pos);
	else
	Read_Len := 0;
	end if;
	return int (Read_Len);
	end C_Read;

	end FILO.FS.VFS;