AdaCore / ada-spark-rfcs

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

[feature] define range integer types without symmetric base range #107

Open JoseRuizAdaCore opened 10 months ago

JoseRuizAdaCore commented 10 months ago

Summary

RM-3.5.4(9) imposes a symmetric base range for signed integer types. I would like to remove the need for a symmetric base range because it imposes the use of larger types to perform arithmetic operations, potentially burdening embedded applications with undesirable run-time needs and performance overhead.

My proposal for RM-3.5.4(9) would be the following rewording:

A range_integer_type_definition defines an integer type whose base range includes at least the values of the simple_expressions. A range_integer_type_definition also defines a constrained first subtype of the type, with a range whose bounds are given by the values of the simple_expressions, converted to the type being defined.

Motivation

You can define a 64-bit type containing values between 0 and 2**64-1 as:

type Unsigned_64 is range 0 .. 2**64-1 with Size => 64

Currently, the symmetric base range for signed integer types means that intermediate arithmetic operations on the previously defined 64-bit type are performed in 128-bit. It is also misleading because the Size aspect would let the coder think that it would use 64-bit operations.

Using a larger type can harm the performance of the operation, and sometimes force the operation to be implemented in software (within a run-time library) instead of hardware. This is particularly unfortunate for embedded applications. For example, on a 64-bit hardware architecture, a 64-bit multiplication can be performed with a single hardware instruction, while a 128-bit multiplication needs a series of hardware instructions working on intermediate results.

Caveats and alternatives

I do not see the value of defining a symmetric base range, but I may be missing something.

We could use a modular type definition to prevent the symmetric base range instead, but the semantics of the two integer type definitions are very different.

sttaft commented 10 months ago

I presume you would allow implementations to continue to do what they currently do. My biggest concern is whether you could properly implement numeric overflow checking for an asymmetric base range. You might want to include some indication that typical hardware can perform the desired overflow checking.

Presumably the unary minus operator would always raise Constraint_Error when given an operand other than zero, and similarly subtraction would raise Constraint_Error if the left operand is smaller than the right operand.

JoseRuizAdaCore commented 10 months ago

Yes, implementations could choose to do as they currently do.

The suggestion related to hardware is a good one. I would add something like the following:

Proper implementation of numeric overflow checking does not need to use a symmetric base range. Typical hardware signal numeric overflows on arithmetic operations with the carry and overflow flags.

sttaft commented 10 months ago

The key thing is that the "carry" bit can generally be used to signal unsigned overflow, which is what is relevant here.