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)
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)