AdaCore / ada-spark-rfcs

Platform to submit RFCs for the Ada & SPARK languages
63 stars 28 forks source link

Extending the use of Static aspect #61

Open gusthoff opened 4 years ago

gusthoff commented 4 years ago

I'd like to propose using the new Static aspect for more complex functions. What do you think?

Here is a draft version of the proposal. Please let me know if there's a way to implement the use-case below using features that are already available in Ada.

Static compile-time functions

Compile-time functions are useful to initialize data that is known to be static. A common use-case (lookup tables) is presented below. In Ada, it is possible to use the new Static aspect to declare static expression functions:

   function If_Then_Else (Flag : Boolean; X, Y : Integer) return Integer is
     (if Flag then X else Y) with Static;

However, the use of this aspect is limited to expression functions. It would be very useful to allow more complex implementations, such as:

   type Float_Array is array (Natural range <>) of Float;

   function Generate_Table (First, Last : Natural) return Float_Array
     with Static;

In C++, for example, constexpr can be used for this purpose.

Lookup tables

Lookup tables are typically used in situations where the computation cost of a function is too high. This is particularly useful for embedded programming. Instead of computing a function, using pre-computed data from ROM can provide similar precision at much lower computation cost.

For example, let's say we want to implement a lookup table for the sine function. We could use this approach:

package Tab_Generator is

   type Float_Array is array (Natural range <>) of Float;

   function Gen_Sin_Tab (Last : Positive) return Float_Array;

end Tab_Generator;

with Ada.Numerics;
with Ada.Numerics.Generic_Elementary_Functions;

package body Tab_Generator is

   package Float_Elementary_Functions is new
     Ada.Numerics.Generic_Elementary_Functions (Float);

   function Gen_Sin_Tab (Last : Positive) return Float_Array
   is
      use Ada.Numerics;
      use Float_Elementary_Functions;

      F_Last  : constant Float := Float (Last);
      Half_Pi : constant := (Pi / 2.0);
   begin
      return FA : Float_Array (0 .. Last) do
         for I in FA'Range loop
            FA (I) := Sin (Float (I) / F_Last * Half_Pi);
         end loop;
      end return;
   end;

end Tab_Generator;

with Tab_Generator; use Tab_Generator;

package Math_Tabs
is
   Sin_Tab : constant Float_Array;
private
   Sin_Tab_Last : constant := 180;

   Sin_Tab : constant Float_Array := Gen_Sin_Tab (Sin_Tab_Last);
end Math_Tabs;

Here, the lookup table Sin_Tab is generated by calling Gen_Sin_Tab. The problem with this approach is that Sin_Tab won't be stored in ROM. Instead, it will be computed at run-time.

In order to have the information as static data, we could create and run a separate application that generates a package specification with that table before building the actual application. For example:

with Ada.Text_IO; use Ada.Text_IO;

with Ada.Numerics;
with Ada.Numerics.Generic_Elementary_Functions;

procedure Generate_Sin_Table is

   package Float_Elementary_Functions is new
     Ada.Numerics.Generic_Elementary_Functions (Float);

   type Float_Array is array (Natural range <>) of Float;

   function Gen_Sin_Tab (Last : Positive) return Float_Array is
      use Ada.Numerics;
      use Float_Elementary_Functions;

      F_Last : constant Float := Float (Last);
      Half_Pi : constant := (Pi / 2.0);
   begin
      return FA : Float_Array (0 .. Last) do
         for I in FA'Range loop
            FA (I) := Sin (Float (I) / F_Last * Half_Pi);
         end loop;
      end return;
   end;

   Sin_Tab_Last : constant := 180;

   Sin_Tab : constant Float_Array
     := Gen_Sin_Tab (180);

   F_Ads, F_Adb : File_Type;
begin
   Create (F_Ads, Out_File, "math_stat_tabs.ads");

   Put_Line (F_Ads, "package Math_Stat_Tabs is");
   Put_Line (F_Ads,
             "   Sin_Tab : constant array (0 .. "
             & Sin_Tab_Last'Image & ") of Float := ");

   Put_Line (F_Ads,
             "               (" & Sin_Tab (Sin_Tab'First)'Image & ",");
   for V of Sin_Tab (Sin_Tab'First + 1 .. Sin_Tab'Last - 1) loop
      Put_Line (F_Ads,
                "                " & V'Image & ",");
   end loop;
   Put_Line (F_Ads,
             "                " & Sin_Tab (Sin_Tab'Last)'Image & ");");
   Put_Line (F_Ads, "end Math_Stat_Tabs;");

   Close (F_Ads);

end Generate_Sin_Table;

After building and running this application, we'd get:

package Math_Stat_Tabs is
   Sin_Tab : constant array (0 ..  180) of Float :=
               ( 0.00000E+00,
                 8.72654E-03,

                 --  skipping some values...

                 9.99962E-01,
                 1.00000E+00);
end Math_Stat_Tabs;

Now, when building the actual application, Sin_Tab is stored as static data (in ROM).

One of the problems with this approach is that it makes the build process more complicated by requiring a pre-build step. A more elegant solution could be achieved by allowing the Static aspect for Gen_Sin_Tab. For example:

package Math_Stat_Tabs_New is

   type Float_Array is array (Natural range <>) of Float;

   function Gen_Sin_Tab (Last : Positive) return Float_Array
     with Static;

   Sin_Tab : constant Float_Array;

private
   Sin_Tab_Last : constant := 180;

   Sin_Tab : constant Float_Array := Gen_Sin_Tab (Sin_Tab_Last);

end Math_Stat_Tabs_New;
sttaft commented 4 years ago

I agree with the goals of this RFC. In ParaSail, any function call where all parameters are known at compile time is evaluated at compile time. This of course requires a full interpreter in the compiler, or an ability to compile and execute code. You also need to know that the code has no references to external global variables. The interpreter approach is cleaner when you are cross-compiling, since it is difficult to compile and execute target code at compile time. The interpreter need not be a source-level interpreter -- it could operate at the intermediate code level, such as for LLVM.

My main objection to the C++ feature is that it allows some but not all language features, which means deciding what can be in a "constexpr" is itself complicated, and could introduce maintenance headaches. I would say support the whole language, or some very easily defined subset (e.g. no tasking).

-Tuck

On Fri, Aug 28, 2020 at 9:48 AM Gustavo A. Hoffmann < notifications@github.com> wrote:

I'd like to propose using the new Static aspect for more complex functions. What do you think?

Here is a draft version of the proposal. Please let me know if there's a way to implement the use-case below using features that are already available in Ada. Static compile-time functions

Compile-time functions are useful to initialize data that is known to be static. A common use-case (lookup tables) is presented below. In Ada, it is possible to use the new Static aspect to declare static expression functions:

function If_Then_Else (Flag : Boolean; X, Y : Integer) return Integer is (if Flag then X else Y) with Static;

However, the use of this aspect is limited to expression functions. It would be very useful to allow more complex implementations, such as:

type Float_Array is array (Natural range <>) of Float;

function Generate_Table (First, Last : Natural) return Float_Array with Static;

In C++, for example, constexpr can be used for this purpose. Lookup tables

Lookup tables are typically used in situations where the computation cost of a function is too high. This is particularly useful for embedded programming. Instead of computing a function, using pre-computed data from ROM can provide similar precision at much lower computation cost.

For example, let's say we want to implement a lookup table for the sine function. We could use this approach:

package Tab_Generator is

type Float_Array is array (Natural range <>) of Float;

function Gen_Sin_Tab (Last : Positive) return Float_Array; end Tab_Generator;

with Ada.Numerics;with Ada.Numerics.Generic_Elementary_Functions; package body Tab_Generator is

package Float_Elementary_Functions is new Ada.Numerics.Generic_Elementary_Functions (Float);

function Gen_Sin_Tab (Last : Positive) return Float_Array is use Ada.Numerics; use Float_Elementary_Functions;

  F_Last  : constant Float := Float (Last);
  Half_Pi : constant := (Pi / 2.0);

begin return FA : Float_Array (0 .. Last) do for I in FA'Range loop FA (I) := Sin (Float (I) / F_Last * Half_Pi); end loop; end return; end; end Tab_Generator;

with Tab_Generator; use Tab_Generator; package Math_Tabsis Sin_Tab : constant Float_Array;private Sin_Tab_Last : constant := 180;

Sin_Tab : constant Float_Array := Gen_Sin_Tab (Sin_Tab_Last);end Math_Tabs;

Here, the lookup table Sin_Tab is generated by calling Gen_Sin_Tab. The problem with this approach is that Sin_Tab won't be stored in ROM. Instead, it will be computed at run-time.

In order to have the information as static data, we could create and run a separate application that generates a package specification with that table before building the actual application. For example:

with Ada.Text_IO; use Ada.Text_IO; with Ada.Numerics;with Ada.Numerics.Generic_Elementary_Functions; procedure Generate_Sin_Table is

package Float_Elementary_Functions is new Ada.Numerics.Generic_Elementary_Functions (Float);

type Float_Array is array (Natural range <>) of Float;

function Gen_Sin_Tab (Last : Positive) return Float_Array is use Ada.Numerics; use Float_Elementary_Functions;

  F_Last : constant Float := Float (Last);
  Half_Pi : constant := (Pi / 2.0);

begin return FA : Float_Array (0 .. Last) do for I in FA'Range loop FA (I) := Sin (Float (I) / F_Last * Half_Pi); end loop; end return; end;

Sin_Tab_Last : constant := 180;

Sin_Tab : constant Float_Array := Gen_Sin_Tab (180);

F_Ads, F_Adb : File_Type;begin Create (F_Ads, Out_File, "math_stat_tabs.ads");

Put_Line (F_Ads, "package Math_Stat_Tabs is"); Put_Line (F_Ads, " Sin_Tab : constant array (0 .. " & Sin_Tab_Last'Image & ") of Float := ");

Put_Line (F_Ads, " (" & Sin_Tab (Sin_Tab'First)'Image & ","); for V of Sin_Tab (Sin_Tab'First + 1 .. Sin_Tab'Last - 1) loop Put_Line (F_Ads, " " & V'Image & ","); end loop; Put_Line (F_Ads, " " & Sin_Tab (Sin_Tab'Last)'Image & ");"); Put_Line (F_Ads, "end Math_Stat_Tabs;");

Close (F_Ads); end Generate_Sin_Table;

After building and running this application, we'd get:

package Math_Stat_Tabs is Sin_Tab : constant array (0 .. 180) of Float := ( 0.00000E+00, 8.72654E-03,

             --  skipping some values...

             9.99962E-01,
             1.00000E+00);end Math_Stat_Tabs;

Now, when building the actual application, Sin_Tab is stored as static data (in ROM).

One of the problems with this approach is that it makes the build process more complicated by requiring a pre-build step. A more elegant solution could be achieved by allowing the Static aspect for Gen_Sin_Tab. For example:

package Math_Stat_Tabs_New is

type Float_Array is array (Natural range <>) of Float;

function Gen_Sin_Tab (Last : Positive) return Float_Array with Static;

Sin_Tab : constant Float_Array; private Sin_Tab_Last : constant := 180;

Sin_Tab : constant Float_Array := Gen_Sin_Tab (Sin_Tab_Last); end Math_Stat_Tabs_New;

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/AdaCore/ada-spark-rfcs/issues/61, or unsubscribe https://github.com/notifications/unsubscribe-auth/AANZ4FIVF64BTUTK32YXZVLSC6YTVANCNFSM4QOEZGSQ .

jere-software commented 4 years ago

My main objection to the C++ feature is that it allows some but not all language features, which means deciding what can be in a "constexpr" is itself complicated, and could introduce maintenance headaches. I would say support the whole language, or some very easily defined subset (e.g. no tasking).

I just want to comment here since I have been using constexpr a lot in embedded C++ over the recent years. This has never really been an issue for me (can't speak for others). It has been very straightforward and intuitive and the compiler usually has given very good error messages letting me know when something cannot be used for a constant expression. Between whole language and subset, I would definitely recommend a subset. That's what C++ has done and it works well.

Ada might be a bit more difficult because it isn't as mature at producing static code (it can only seem to handle making things static if they are only one level deep). I would really like to see some improvements in this realm. There's nothing more frustrating than setting up a seemingly static size for a type and then trying to set another type's size using the previous type's size only to find out it isn't considered static anymore. constexpr works pretty well in C++ partly due to the fact it can seem to better handle nesting of potentially static values.

Either way, I would definitely like to see some iteration of this functionality, even if it is limited with the hope it could be iterated on in the future.

Just as an example: I have a micro where the Baud rate calculation is pretty complex and needs control logic (a loop). I can implement it in C++ as a constexpr no problem, but in Ada it will always generate a runtime operation (and a lengthy one at best). In my C++ code, I use it to initialize some constants with no hit on my limited program space. In Ada, I just revert to hand calculating it for all my constants and hope I don't make a mistake.

Fabien-Chouteau commented 4 years ago

Thank you @jeremiahbreeden, that is a good example.

raph-amiard commented 4 years ago

Hello @gusthoff,

The language design group @ adacore has discussed this issue and there is definitely interest in allowing those kind of use cases. However there are still some shadows wrt. which way forward is the best.

In any case, this seems like a topic worthy of time and attention, and so we might create a working group around this. I'll keep you updated on this issue.

Thanks