bambinella
commented
7 years ago I feel that maybe it should be sufficient to have a regular "low<x and x<high " constraint on the type and only provide backend hints for representation?
That would be number of bytes, memory alignment, and byte order. The backend should know what the FFI calls require and change representation based on performance characteristics. So it could be left open for optimization.
Unless you intend to extend Whiley with the equivalent of reinterpret_cast, which probably would be a bad idea.
Although I guess aliasing from pointers returned from FFI calls is an issue.
DavePearce
(related to #654)
Introduction
An important consideration when compiling Whiley programs for different platforms is that of dynamically versus statically sized types. Roughly speaking, the former correspond to those which require dynamically allocated memory, whilst the latter correspond to those which can be entirely allocated on the stack (for example). In particular, statically sized types have a fixed size at compile time.
At the moment, the definition what is a dynamically sized type versus what is a statically sized type is somewhat unclear. Essentially, any type which contains one of the following is dynamically sized:
intwhich is not specifically bounded (above and below) is dynamically sized.To illustrate some statically-sized examples:
type Point is { int x, int y } where 0 <= x && x <= 255 && 0 <= y && y <= 255type Vec { int len, int[] data } where 0 <= len && len <= |data| && |data| <= 100The latter is interesting because the array itself is still variable-length, but is known to occupy a fixed amount of space in memory.
Proposal
The primary issue with the current status-quo is that the definition of a statically sized type is somewhat awkward. To address this issue, the proposal here is to introduce the following specific statically sized types:
int:8,int:16,uint:8, etc). These types are equivalent (in some sense) toint, but include an additional size attribute. This attribute must be a compile-time integer constant. The compiler is not obliged to match the size attribute exactly in the underlying implementation, but is expected to make a "best effort". For example, on the JVM,int:128may simply compile to the same underlying representation asint(since there is no 128bit integer on the JVM).usize). This defines the return type from the array length operator. This type is awkward since it remains unknown at any given time whether it is, for example, equivalent touint:32oruint:64.int[8],int[4], etc). These types define an array of a fixed size known at compile-time. The special typeint[?]maybe supported to represent an array of unknown fixed size, though this is not statically sized.Here, the type
uint:8would be the generic definition of a byte. Likewise, a type such asint:8[?]is useful for describing (for example) raw pointer types in C, as this corresponds directly toint8_t*.Subtyping
An important issue is how subtyping between such types will be supported. In fact, the proposal is that, from the perspective of subtyping, all integer types are equivalent to
int. This leads to some potentially precarious situations:function f(uint:8 x) -> (uint:4 r): return xThis program appears to suffer from a potential loss of precision. In many languages (e.g. Java, Rust, etc), such implicit coercions are not permitted for this reason. However, in Whiley, we can note that the above is not a concern because it will not verify. Indeed, it is roughly equivalent to this:
function f(int x) -> (int r) requires 0 <= x && x <= 255 ensures 0 <= r && r <= 15: return xThis program will certainly fail verification. However, we could resolve this as follows:
function f(uint:8 x) -> (uint:4 r) requires x <= 15: return xIn this case the program would now verify and, indeed, we see there is no loss of precision.
Challenges
Platform-specific size types. An interesting challenge is the interaction between the type
usizeand other integer types. The general concern is that certain expressions (arr[i]) will not verify on some platforms (e.g. ifihas typeint:64on a platform whereusizeisuint:32. However, it seems likely that this won't be such a big problem in general. Consider the example in more detail:function get(int:8[] arr, int:64 i) -> (int r): return arr[i]This exhibits the general problem. However, the fact is that it won't verify either. In order for it to verify, we need a precondition that
i < |arr|, in which case there is no problem.Bitwise Operations. an interesting additional question is whether or not statically sized integer types should support bitwise operations. This would be convenient, since it would mean that
uint:8can replacebyte. But, the problem is that it presumably leads to undefined behaviour for larger types (e.g.uint:32) due to the uncertainty of endianness? Java handles this by treating bitwise operators as operators on integers, not bits.