boschresearch / blech

Blech is a language for developing reactive, real-time critical embedded software.
Apache License 2.0
72 stars 6 forks source link

Feature/forced cast #20

Closed schorg closed 4 years ago

schorg commented 4 years ago

Forced cast 'as!'.

FriedrichGretz commented 4 years ago

The semantics (or error messages) are not yet fully clear to me.

let c: int16 = 4200
var i2 = c as! int8

generate C code

(*blc_main_c) = 4200;
(*blc_main_i2) = (blc_int8)(*blc_main_c);

but making c a constant

const c: int16 = 4200
var i2 = c as! int8

produces an error

error: Value '4200' cannot be represented in type 'int8'.
  --> .\forcedCast.blc:6:14 [typing]

6  |     var i2 = c as! int8
   |              ^^^^^^^^^^ conversion not possible
6  |     var i2 = c as! int8
   |              - value not in 'int8'

Is this error meant to be an additional safety feature? What is not clear to me is what are the capabilities of as! and what its guarantees.

schorg commented 4 years ago

Semantics of 'as!'

Debug code: Traps if the value does not 'fit' into the target type, runtime check necessary. Release code: Unsafe behavior or saturation (still to be decided) Constant evaluation: The runtime check for debug code is evaluated at compile time.

FriedrichGretz commented 4 years ago

Since there is not debug/release code as of now, it means "unsafe behaviour" (or C defined behaviour) unless the value being converted is a compile time constant. In particular for all primitive types X and Y, we can as!-cast X into Y. Correct?

schorg commented 4 years ago

Even worse: Undefined behavior like in C

FriedrichGretz commented 4 years ago

I have briefly tested the code and it generates C code as expected. Do you plan to add more unit tests to this PR? For example, ensuring that complex types are not converted. Or code generation tests that ensure that particular values are the result of a cast?

You can merge your PR at your discretion. Do not forget to squash commits into a signed one.

schorg commented 4 years ago

Typechecking still needs more rework. Could be done then.