Evaluation of modular integers in mathematical expressions

[treiher]

Context and Problem Statement

The use of different integer types in mathematical expressions could lead to ambiguities, especially when modular integers are involved.

Example (cf. #726)

   type Length is mod 2**8;

   type Packet is
      message
         Length_1 : Length;
         Length_2 : Length
            then Payload
               with Size => Length_2 * 256 + Length_1
               if (Length_2 * 256 + Length_1) mod 8 = 0;
         Payload : Opaque;
      end message;

The target type of a size aspect is user-defined and could be a modular integer as well as a range integer (cf. #317). Assuming a target type with a maximum value of >= 2**16 - 1 the result of Length_2 * 256 + Length_1 will fit in the target type. In SPARK Length_2 * 256 can only be evaluated, if 256 is converted to the target type before evaluation, as 256 is outside the range of Length. Also Length_2 and Length_1 have to be converted to the target type, as mathematical operations on different integer types are not allowed in SPARK. Due to the necessary conversions, Length_1 as well as Length_2 are not evaluated as modular integers, which is unexpected.

Considered Options

O1 Explicit type conversions

Adding explicit type conversions and considering different integer types always as incompatible would remove the ambiguities.

+ Flexible
− Complex

O2 Remove modular integers

Modular integers are not strictly needed, as the mod operator can be used instead.

+ Simplifies language
− Specification of range integers is more cumbersome

The drawbacks can be alleviated by changing the syntax of range integer declarations. Currently, the range as well as the size of a range integer must be defined. In many cases, the range can be inferred from the size or the size can be inferred from the upper bound.

Possible syntax: type Length is range with Size => 8 or type Length is range 0 .. 2**8 - 1 instead of type Length is range 0 .. 2**8 - 1 with Size => 8

Decision Outcome

O2. We decided to just remove modular integers for now. The syntax for range integers can be optimized at a later time.