You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Currently, the optimisation phases on Core assume all Juvix functions are pure. This might not be the case with some builtins, which might lead to incorrect code transformations.
For example, for the code
let x := random n;
y := random n;
in
f x y
the optimiser might decide that it's equivalent to
let x := random n
in
f x x
which is incorrect, because random has a side-effect (it's not referentially transparent).
This actually won't happen for now, because we don't yet have common subexpression elimination, but a duplication will happen if random has zero arguments:
let x := random
in
f x x
will be transformed to
f random random
We should add a "volatile" pragma to mark certain functions as not referentially transparent and then respect this in the optimiser (this requires also adjusting the optimisations)
The text was updated successfully, but these errors were encountered:
Currently, the optimisation phases on Core assume all Juvix functions are pure. This might not be the case with some builtins, which might lead to incorrect code transformations.
For example, for the code
the optimiser might decide that it's equivalent to
which is incorrect, because
random
has a side-effect (it's not referentially transparent).This actually won't happen for now, because we don't yet have common subexpression elimination, but a duplication will happen if
random
has zero arguments:will be transformed to
We should add a "volatile" pragma to mark certain functions as not referentially transparent and then respect this in the optimiser (this requires also adjusting the optimisations)
The text was updated successfully, but these errors were encountered: