`unfolding` should return the return value of the function so that it is a hint for verification, and has the behaviour of the unfolded function at runtime

[samuelchassot]

And maybe can be inline def

[samuelchassot]

Summary

• 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

  • it can be the argument to unfold directly
  • or in the body of a let binding whose variable is passed to the unfold function
    • IT HAS TO BE DIRECTLY IN THE BODY, if it is in other let bindings, it wouldn’t be unfolded because lifted already → it does not explore the entire tree to find a function invocation

• 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!!!

[samuelchassot]

Also, the potential side effects of the unfolded function are visible: Example:

  case class C(var x: BigInt):
    def update(v: BigInt): BigInt = {
      x += v
      x
    }

  def t(): BigInt = {
    val c = C(0)
    unfold(c.update(1))
    assert(c.x == 1)
    42
  }

gives this tree:

[ Debug  ] Symbols after UnfoldOpaque
[ Debug  ] 
[ Debug  ] -------------Functions-------------
[ Debug  ] def update(thiss: C, v: BigInt): (BigInt, C) = {
[ Debug  ]   val thiss: C = thiss
[ Debug  ]   val thiss: C = C(thiss.x + v)
[ Debug  ]   val tmp: Unit = ()
[ Debug  ]   val tmp: Unit = ()
[ Debug  ]   (thiss.x, thiss)
[ Debug  ] }
[ Debug  ] 
[ Debug  ] @library
[ Debug  ] def unfold[T](call: T): Unit = ()
[ Debug  ] 
[ Debug  ] def t: BigInt = {
[ Debug  ]   val c: C = C(0)
[ Debug  ]   val res: (BigInt, C) = update(c, 1)
[ Debug  ]   val c: C = @DropVCs @DropVCs res._2
[ Debug  ]   val tmp: Unit = ()
[ Debug  ]   val c: C = @DropVCs @DropVCs c
[ Debug  ]   val tmp: Unit = ()
[ Debug  ]   val tmp: Unit = {
[ Debug  ]     assume(update(c, 1) == @DropVCs {
[ Debug  ]       val thiss: C = c
[ Debug  ]       val v: BigInt = 1
[ Debug  ]       val thiss: C = thiss
[ Debug  ]       val thiss: C = C(thiss.x + v)
[ Debug  ]       val tmp: Unit = ()
[ Debug  ]       val tmp: Unit = ()
[ Debug  ]       (thiss.x, thiss)
[ Debug  ]     })
[ Debug  ]     ()
[ Debug  ]   }
[ Debug  ]   assert(c.x == 1)
[ Debug  ]   42
[ Debug  ] }
[ Debug  ] 
[ Debug  ] -------------Sorts-------------
[ Debug  ] abstract class C
[ Debug  ] case class C(x: BigInt) extends C
[ Debug  ] 
[ Debug  ] @synthetic
[ Debug  ] abstract class Object
[ Debug  ] case class Open(value: BigInt) extends Object
[ Debug  ] 

And we can see that the assertion is valid, so the side effect is visible

[samuelchassot]

So we decided (discussion 14.08.2024):

• Keep argument as non-ghost -> more flexible
• In the future, update so that unfold returns the return value and not Unit
• Rename it to unfolding as the call actually happens.

[samuelchassot]

(old issue name: unfold should take ghost parameter to not need to be wrapped in ghostExpr)