boschresearch / blech

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

Prevent input-output aliasing in function calls. #21

Closed FriedrichGretz closed 4 years ago

FriedrichGretz commented 4 years ago

Following up a recent discussion this fix prevents aliasing arguments in function calls. Regardless of possible future extensions to the language a la borrowing and such, in its current state this is a bug fix. The unit test causality/invalid/functionInputOutputAliasing.blc demonstrates this. Only one previous test is affected and fixed: codegeneration/uint.blc - note how the observable behaviour is still exactly the same at the cost of one more variable.

schorg commented 4 years ago

Works nicely for function call statements but not for function call expressions. The following example is not rejected:

function f(x: int32)(y: int32) returns int32
    y = 2
    y = x + y
    return y
end

@[EntryPoint]
activity A()()
    var b: int32 = 17
    _ = f(b)(b)
    await true
end 

Although, I do not really understand the causality analysis, the code for iterating expressions should already be there. I suspect the fix is another one-liner somewhere in the causality analysis.

FriedrichGretz commented 4 years ago

The difficulty in fixing the issue for expressions is that the alias analysis is done on the program graph where nodes represent entire statements. In case of the assignment statement this becomes tricky: x = x + 1 is represented by one node that both reads and writes x. In order to prevent a false positve error report in this case, we need to reconsider the right hand side and left hand side expressions separately. This is done in commit cb5e4cc