25 ms·

> almost all code that uses signed integers to represent values that will never be negative, tends to have a cacophony of range assertions and other tests which

> almost all code that uses signed integers to represent values that will never be negative, tends to have a cacophony of range assertions and other tests which are just as error-prone as bounds checking to remembering to write, but also maintain when refactoring. It’s truly underappreciated how much those tests can be eliminated if your integer can never actually become negative due to the type system itself. This is something the Ada language gets right: you define your integer type with a range, and the compiler automagically inserts the runtime range checks. (Unless you switch them off with compiler directives.) It makes far more sense to bake the range-checks into the type than to do it the manual way and just hope you don't miss anything. You can do this in C++ using a library (thanks to templates) [0] but this is very rarely done. [0] https://www.boost.org/doc/libs/1_78_0/libs/safe_numerics/doc/html/safe_range.html https://www.boost.org/doc/libs/1_78_0/libs/safe_numerics/doc...

lifthrasiir 5y ago
Range types are not a panacea, especially combined with other arithmetic operators. There are essentially two options: [lo1, hi1) + [lo2, hi2) can result in a new type [lo1 + lo2, hi1 + hi2) and so on, or any operation reverts back to the base type. Only the former provides a static type guarantee but can be extremely annoying to use and you eventually have to constrain the type back with runtime checks. (Interval arithmetic also shares this problem.) Probably for this reason, to my knowledge, both Pascal and Ada implements the latter, which is more usable but also arguably useless: if your intermediate type is ranged you have to manually calculate correct bounds (a failure to do so will cause a runtime error), and if it's unranged there is zero guarantee even in the run time.
- MaxBarraclough 5y ago
  Somewhat related: there's apparently a defect in the Ada language spec which permits reordering of arithmetic operations such that out-of-range behaviour may hinge on the compiler's whim: [0] > non-parenthesized arithmetic operations could be re-ordered by the compiler, which may result in a failing computation (due to overflow checking) becoming a successful one, and vice-versa. By default, GNATprove evaluates all expressions left-to-right, like GNAT. Presumably one solution would be to use a three-address-code style [2] to completely tie the compiler's hands regarding ordering, but this seems painfully restrictive even by the standards of SPARK. Also, an Ada compiler's internal choice of base type (with which to implement a range-based integer type) can impact overflow behaviour: [1] > The choice of base types influences in which cases intermediate overflows may be raised during computation. The choice made in GNATprove is the strictest one among existing compilers, as far as we know, which ensures that GNATprove’s analysis detects a superset of the overflows that may occur at run time. I don't know if there's a fully portable robust answer to this second problem. (I believe you can generally use hints to force the Ada compiler to use a particular sized type, along the lines of C's uint32_t, but that this isn't portable.) edit On second thought, I imagine using a three-address-code style would solve this too. Either the result falls within the permitted range of the destination variable, or it doesn't. [0] https://docs.adacore.com/spark2014-docs/html/ug/en/appendix/portability_issues.html#parenthesized-arithmetic-operations https://docs.adacore.com/spark2014-docs/html/ug/en/appendix/... [1] https://docs.adacore.com/spark2014-docs/html/ug/en/appendix/portability_issues.html#base-type-of-user-defined-integer-types https://docs.adacore.com/spark2014-docs/html/ug/en/appendix/... [2] https://en.wikipedia.org/wiki/Three-address_code https://en.wikipedia.org/wiki/Three-address_code
pyjarrett 5y ago
Ada provides integers and floats with range checks, and you can specify the underlying size, but intermediate values don't get checked. It also has a separate form of unsigned integers called "modular types" which expressly indicate wrapping, if that's your intent. -- Range checked equivalent of uint64_t; type Nibble is range 0 .. 15 with Size => 64; -- Every assignment is as if Value := (Value % 16); type Wrapped_Nibble is mod 16; type Small_Float is digits 4 range 0.0 .. 20.0 with Size => 32; I agree that the subexpression issue is problematic, IIRC I thought this was checked in SPARK code, but I could be wrong. The big benefit is describing your intent and you know that the stored value is in range, though whether it went outside of that range in calculation might not be known. Another thing is that these types define 'First, 'Last, 'Pred, 'Succ, and 'Range attributes which you can use. for N of Nibble'Range loop -- do something end loop;
- MaxBarraclough 5y ago
  > I thought this was checked in SPARK code, but I could be wrong I believe that's correct, see my other comment. [0] Does still feel a bit ugly though. [0] https://news.ycombinator.com/item?id=29768848 https://news.ycombinator.com/item?id=29768848

lifthrasiir 5y ago

Range types are not a panacea, especially combined with other arithmetic operators. There are essentially two options: [lo1, hi1) + [lo2, hi2) can result in a new type [lo1 + lo2, hi1 + hi2) and so on, or any operation reverts back to the base type. Only the former provides a static type guarantee but can be extremely annoying to use and you eventually have to constrain the type back with runtime checks. (Interval arithmetic also shares this problem.) Probably for this reason, to my knowledge, both Pascal and Ada implements the latter, which is more usable but also arguably useless: if your intermediate type is ranged you have to manually calculate correct bounds (a failure to do so will cause a runtime error), and if it's unranged there is zero guarantee even in the run time.

MaxBarraclough 5y ago
Somewhat related: there's apparently a defect in the Ada language spec which permits reordering of arithmetic operations such that out-of-range behaviour may hinge on the compiler's whim: [0] > non-parenthesized arithmetic operations could be re-ordered by the compiler, which may result in a failing computation (due to overflow checking) becoming a successful one, and vice-versa. By default, GNATprove evaluates all expressions left-to-right, like GNAT. Presumably one solution would be to use a three-address-code style [2] to completely tie the compiler's hands regarding ordering, but this seems painfully restrictive even by the standards of SPARK. Also, an Ada compiler's internal choice of base type (with which to implement a range-based integer type) can impact overflow behaviour: [1] > The choice of base types influences in which cases intermediate overflows may be raised during computation. The choice made in GNATprove is the strictest one among existing compilers, as far as we know, which ensures that GNATprove’s analysis detects a superset of the overflows that may occur at run time. I don't know if there's a fully portable robust answer to this second problem. (I believe you can generally use hints to force the Ada compiler to use a particular sized type, along the lines of C's uint32_t, but that this isn't portable.) edit On second thought, I imagine using a three-address-code style would solve this too. Either the result falls within the permitted range of the destination variable, or it doesn't. [0] https://docs.adacore.com/spark2014-docs/html/ug/en/appendix/portability_issues.html#parenthesized-arithmetic-operations https://docs.adacore.com/spark2014-docs/html/ug/en/appendix/... [1] https://docs.adacore.com/spark2014-docs/html/ug/en/appendix/portability_issues.html#base-type-of-user-defined-integer-types https://docs.adacore.com/spark2014-docs/html/ug/en/appendix/... [2] https://en.wikipedia.org/wiki/Three-address_code https://en.wikipedia.org/wiki/Three-address_code

pyjarrett 5y ago

Ada provides integers and floats with range checks, and you can specify the underlying size, but intermediate values don't get checked. It also has a separate form of unsigned integers called "modular types" which expressly indicate wrapping, if that's your intent. -- Range checked equivalent of uint64_t; type Nibble is range 0 .. 15 with Size => 64; -- Every assignment is as if Value := (Value % 16); type Wrapped_Nibble is mod 16; type Small_Float is digits 4 range 0.0 .. 20.0 with Size => 32; I agree that the subexpression issue is problematic, IIRC I thought this was checked in SPARK code, but I could be wrong. The big benefit is describing your intent and you know that the stored value is in range, though whether it went outside of that range in calculation might not be known. Another thing is that these types define 'First, 'Last, 'Pred, 'Succ, and 'Range attributes which you can use. for N of Nibble'Range loop -- do something end loop;

MaxBarraclough 5y ago
> I thought this was checked in SPARK code, but I could be wrong I believe that's correct, see my other comment. [0] Does still feel a bit ugly though. [0] https://news.ycombinator.com/item?id=29768848 https://news.ycombinator.com/item?id=29768848