Open samuelchassot opened 1 month ago
@samuelchassot test fails:
[info] - 219: imperative/valid/UnfoldOpaqueMutate *** FAILED *** (18 milliseconds)
I am now not sure if we want the argument of unfold
to be ghost
. Maybe unfold
should be opaque. In some cases, we may call an executable function and we may want to direct stainless to unfold it. Perhaps the most confusing aspect of unfold
is that it's always returning unit. Perhaps we should have unfolding
instead which is an identity function that does nothing but makes stainless unfold the call? How does our internal tree look like for unfold
? We should:
unfold
stainless library definition accordinglyI am diving into the code and am documenting what is done. I'll post my documentation here.
unfolding is performed by a specific phase UnfoldOpaque
it unfolds FunctionInvocation
by transforming it into a tree like:
{
assume(opaqueFn(v) == @DropVCs {
val v: BigInt = v // Bindings arguments -> value in the context
// BEGIN BODY opaqueFN
val x: BigInt = v * 2
x + 2
// END BODY opaqueFN
})
()
}
This block ends with a Unit
value
The transformation looks for a function invocation to unfold
unfold
function
If the body of the unfolded function contains another invocation it is NOT unfolded
There is a special case in the AntiAliasing
phase, to avoid the body of the function
Usually, AntiAliasing
is transforming a function call to return a tuple (return_value, mutatedVar1, mutatedVar2, ...)
and where it is called, the 1st element is extracted and the mutated variables of scope are updated using the other elements.
In this case, we don’t want this to happen, because ,otherwise, the ImperativeCodeElimination
phase would hoist the call to the function and the UnfoldOpaque
phase would not be able to see it.
⇒ this works only because unfold
drops the result!!!
The last point above makes going for a version returning something else than Unit
more tricky to handle.
I think we can however change it to accept non-ghost argument.
And we can make it inline
. @vkuncak @mario-bucev WDYT?
(I have some examples of the trees transformation if you want to see)
After discussion:
unfold
returns the return value and not Unit
unfolding
as the call actually happens.We should also fix documentation in stainless/core/src/sphinx/library.rst
There is a mention of local inline there in the table. Does this work and how is it different from unfold?
Solves #1550