Re: [Spark] Arrays of Strings

[rod.chapman@praxis-cs.co.uk (Rod Chapman)]

Lutz Donnerhacke <lutz@iks-jena.de> wrote in message news:<slrnb95ehu.ob.lutz@taranis.iks-jena.de>...
> In order to implement thin an execve binding, I wonder how to emulate the
> C-Type "char const * const x []". Any bright ideas?


Lutz and others,
  Here are some thoughts and a possible solution to this problem.
The execve() API is indeed a complex one for SPARK, since the
type "pointer to unconstrained array of pointer to null terminated
C String" is a tricky one for SPARK to model.

 The trick with bindings like this is to come up with a package
specification which is pure SPARK, and presents a clean,
elegant model to the outside world.  No details of the
C type model, or the "glue" needed to bind the two languages
together should be allowed to leak into the package spec!
All the glue and C-related stuff should be hidden in the body.

I'm also working on the assumption that Lutz wants a binding
that is as "thin" as possible, and there are good reasons
to support this approach.

Let's look at how the GNAT.OS_Lib does it...a few fragments:

   type String_Access is access all String;
   type String_List is array (Positive range <>) of String_Access;
   subtype Argument_List is String_List;

   procedure Spawn
     (Program_Name : String;
      Args         : Argument_List;
      Success      : out Boolean);

OK - reasonably elegant, but unfortunately not much use
in this context, since SPARK does not allow explicit declaration
of access types.

The trick here (thanks to Tucker Taft here, who just thought of this
during lunch...) is to change the abstraction a bit to make the
"Args" parameter a legal SPARK type...

I suggest using a single String parameter, where distinct arguments
are separated and terminated by a special character.  ASCII.Nul
is probably a good choice!

So...the SPARK-friendly package spec looks something like:

  package Kernel
  --# own State;
  --# initializes State;
  is
     -- "Args" is a list of arguments, each of which is
     -- termianted by ASCII.Nul
     --
     -- For Example
     --   Kernel.Spawn (Program_Name => "gcc",
     --                 Args         => "-c" & ASCII.Nul &
     --                                 "-g" & ASCII.Nul &
     --                                 "spark.adb" & ASCII.Nul,
     --                 Success      => Success);

     procedure Spawn (Program_Name : in     String;
                      Args         : in     String;
                      Success      :    out Boolean);
     --# global in out State;
     --# derives Success from State, Program_Name, Args &
     --#         State from *, Program_Name, Args;

  end Kernel;

This meets our requirements - perfectly legal SPARK, and none of the
C-related glue is visible.

The body is Ada95 (not SPARK), and uses the facilities of Annex B and
Interfaces to do its stuff.  I've left out a few details but it
goes something like:

   with Interfaces;
   with Interfaces.C;
   with Interfaces.C.Strings;
   use type Interfaces.C.Char;
   use type Interfaces.C.Size_T;
   use type Interfaces.C.Int;
   package body Kernel
   is

     package C renames Interfaces.C;

     -- Count the number of Nul-terminated argments in a given
String...
     function Number_of_Args (Args : in String) return C.Size_T
     is
     begin
       return 2;
     end Number_of_Args;

     procedure Spawn (Program_Name : in     String;
                      Args         : in     String;
                      Success      :    out Boolean)
     is
        subtype Args_Count is C.size_t range 1 .. Number_Of_Args
(Args);
        type Args_Ptr_Vector is array (Args_Count) of aliased
C.Strings.Chars_Ptr;
        Args_Ptrs      : Args_Ptr_Vector;

        subtype C_Args_Index is C.size_t range C.Size_T(Args'First) ..
C.Size_T(Args'Last);
        subtype C_Args_Type  is C.char_array (C_Args_Index);
        C_Args         : C_Args_Type := C.To_C (Args, False);

        C_Program_Name : C.Strings.chars_ptr;
        Ret            : C.Int;

        -- Bind to C here - I've missed out envp here for
simplicity...
        function Execve (Filename : in C.Strings.Chars_Ptr;
                         Argv     : in C.Strings.Chars_Ptr) return
C.Int;
        pragma Import (C, Execve);

        -- Sets the elements of Args_Ptrs to be the 'Access
        -- of each of the N arguments contained in C_Args...
        procedure Set_Args_Ptrs
        --# global out Args_Ptrs;
        --#        in  C_Args;
        is
        begin
           -- proof left to reader... :-)
           null;
        end Set_Args_Ptrs;


     begin
        C_Args := C.To_C (Args, False);

        Set_Args_Ptrs;

        C_Program_Name := C.Strings.New_String (Program_Name);

        Ret := Execve (C_Program_Name, Args_Ptrs (1)'Access);

        C.Strings.Free (C_Program_Name);

        Success := (Ret = 0); -- or something like that...
     end Spawn;
  end Kernel;