ranged integer types, integer arithmetic operations, bitwise operations and range checks

This report is about many issues which need to be addressed systematically (preferably all at once).

Currently Uppaal always implements signed int32_t operations, which might be incorrect when overflows happen. In general Uppaal always checks the ranges and does not allow overflows (reports an error), but:

1) often embedded system allow overflows, thus such range-checking can get in the way. Perhaps we can introduce "relaxed int" type without range checking (this is not critical, thus fixing this has low priority).

2) Uppaal fails to detect when int32_t overflow happen. Perhaps Uppaal should use int64_t operations and check for 32bit overflow. In assembly it is possible to check the Carry flag and thus the operation could still be over int32_t and cheaper.

3) It is not possible specify uint32_t range: Parser does not allow large integer constants like 4294967295. A workaround 2147483647 << 1 +1 works, but gets interpreted as negative value and thus the type declaration fails. Even if the type system is fixed, we still need to revise the integer operations in the virtual machine.

4) Uppaal does not implement bitwise negation. The reason is that the size of our ranged integers is not specified (not sure how many and which bits need to be flipped, especially in case of a sign bit). C/C++ define the bitwise operations over unsigned integer types, so perhaps the easiest solution would be to promote to the full size (uint32_t), but this is not possible because of the second issue, moreover it is not clear how the mixed arithmetic (between signed and unsigned types) works (C/C++ have rules, but Uppaal just treats everything as int32_t).

5) int32_t etc should be built-in types, along with INT32_MAX and other constants.

UPPAALModelChecker / UPPAAL-Meta

ranged integer types, integer arithmetic operations, bitwise operations and range checks #49