Compilation fails due to comparison of big integers

[treiher]

As we have no type checking in our model, all field values are converted to a common integer type in the SPARK code before any calculation or comparison. Currently, Bit_Length is used for this purpose. While it makes sense to use this type for length calculations, it prevents the comparison of big integers. Here is an example:

package Test is

   type B is range 17179869177 .. 17179869178 with Size => 35;

   type D is
      message
         A : B
            then C
               with Length => 8
               if A = 17179869177;
         C : Opaque;
      end message;

end Test;

rflx-test-d.ads:6:01: error: instantiation error at rflx-test-generic_d.ads:210
rflx-test-d.ads:6:01: error: value not in range of type "Bit_Length" defined at rflx-rflx_generic_types.ads:11, instance at rflx-rflx_types.ads:6
rflx-test-d.ads:6:01: error: "Constraint_Error" would have been raised at run time

   compilation of rflx-test-d.ads failed

210                Types.Bit_Length (Get_A (Ctx)) = 17179869177

To cover all possible integer types, we would have to use a non-wrapping 64-bit modular type. The drawback of such a type is that current GNAT versions do not check overflows for exponentiations. Maybe we could prohibit the use of exponentiations in conditions as a workaround? @senier @jklmnn

[jklmnn]

Is there a realistic case where we would have to convert an arbitrary high number to Bit_Length? Where does Types.Bit_Length (Get_A (Ctx)) = 17179869177 originate from?

[treiher]

Is there a realistic case where we would have to convert an arbitrary high number to Bit_Length?

All field values used in length aspects need to be converted to Bit_Length (or at least the final result of the calculation), as this is the base type used for indexing the buffer. I'm not sure what you mean with "arbitrary high number". Of course it doesn't make sense to calculate lengths which are bigger than the index type. But the upper bound is not fixed (cf. #317).

Where does Types.Bit_Length (Get_A (Ctx)) = 17179869177 originate from?

From the condition if A = 17179869177 in the specification. All field values are currently converted to Bit_Length. This doesn't make sense for the shown example, but is necessary when fields with different types are used in one expression or compared with each other, e.g. Types.Bit_Length (Get_A (Ctx)) = Types.Bit_Length (Get_X (Ctx)). For arbitrary big integer types Bit_Length is not usable, that is why I was thinking about using a non-wrapping 64-bit modular type instead.

[jklmnn]

I think we should use a separate modular type solely for comparisons of field values. Length calculations should be in the Bit_Length type. I think that an upper bound of 2 ** 63 - 1 bit for the length of a field or message is sufficient for any real world protocol.

[treiher]

Length calculations should be in the Bit_Length type. I think that an upper bound of 2 ** 63 - 1 bit for the length of a field or message is sufficient for any real world protocol.

I agree, but Bit_Length does not have an upper bound of 2**63 - 1 by default, but (2**31 - 1) * 8. And the user can choose an arbitrary other bound. For further discussions in that direction please use #317.

I think we should use a separate modular type solely for comparisons of field values.

That is what my original proposal was about. But this still does not answer my question. We are supporting 64-bit integer fields, so we also have to support comparisons of 64-bit integer fields. To repeat my original question:

To cover all possible integer types, we would have to use a non-wrapping 64-bit modular type. The drawback of such a type is that current GNAT versions do not check overflows for exponentiations. Maybe we could prohibit the use of exponentiations in conditions as a workaround?

[jklmnn]

That is what my original proposal was about.

I mixed that up with the length discussion. I think we should prohibit exponentiations. When we find a protocol that requires this we might have to change that but I think this is quite unlikely.