boschresearch/blech

support for down casts

mterber opened this issue · 5 comments

Is your feature request related to a problem? Please describe.
Today, I cannot downcast variables, e.g. from uint16 to uint8, in Blech. Means, whenever a downcast is necessary, e.g. within some mathematical algorithm, i have to implement and call a corresponding helper function in C for that specific combination of data types for downcasting.

Describe the solution you'd like
I would like to be able to express down casts directly in Blech. Example:

var i: uint16 = 23456
var k: uint8 = (i * 2) as uint8

I check if I can include down casts into the feature branch feature/bits-and-bytes.

But this needs a little bit more clarification, which result should be expected. Many programmers are not even sure which value for k they can expect, if they assume C's uint semantics.

Currently we only support, what is sometimes called guaranteed conversion. Using the 'as' operator. Guaranteed conversion can be verified by the compiler.

I propose to also introduce forced conversion using the operator 'as!'. The compiler would reject forced conversion if it is not necessary.

In the future we will distinguish debug and and release code generation. In debug code, forced conversion can trap, if the runtime value does not "fit" into the converted type. In release code we would use the semantics of C's downcast accepting undefined behavior outside of the defined domain.

Maybe we will also have 'as?' as soon as we introduce exceptions - which we already planned. 'as?' will throw an exception instead of trapping - also in the release code. Exceptions have to be caught by an exception handler, for a program to be accepted by the compiler.

I started to implement forced conversion (downcast, narrowing) in branch feature/forced-cast

When 'as!' is implemented your code example still would have undefined behavior, because the 'nat16' value is outside the range of the 'nat8' value.

To make sure that your behavior is defined, you should truncate explicitly.

var i: nat16 = 23456
var k: nat8 = ((i * 2) as bits16 & 0x_00FF) as! nat8

Or directly in bits:

var i: bits16 = 23456
var k: bits8 = ((i * 2) & 0x_00FF) as! bits8 

@schorg You are right. Actually, the example I provided above is incomplete. It should be like this:

var i: nat16 = 23456
var k: nat8 = ((i * 2) / 1000) as nat8

During some mathematical operations the intermediate values grow and need 16, 32 or even 64bit data types. The final result, however, will always fit into 8bit for instance. In this case I do not want to spend 32bit to hold an 8bit result value. So in this case the final result would be in the range of nat8.

Downcasts are now part of blechc v. 0.5.2. You can write:

var i: nat16 = 23456
var k: nat8 = ((i * 2) / 1000) as! nat8

/ is integer division. (i * 2)/1000 has type nat16, which gets unsafely casted (as!) to nat8, which has the expected final result.

Documentation will follow.