Purity check

[jad-hamza]

I'm opening this issue so that we remember that the isPure check in

inox/src/main/scala/inox/ast/SymbolOps.scala

Line 1332 in 082081b

if ((variablesOf(bd) contains vd.toVariable) || !isPure(e)(PurityOptions.Unchecked))

takes very long sometimes (some benchmarks that I will add take minutes
to run).

After doing some tests, it looks like the problem comes from the fact that
purity is checked by simplifying the whole formula. More precisely, the slowdown
seem to be coming from the simplification of Let's in simplify (https://github.com/epfl-lara/inox/blob/082081b77e80a0e95696c8649bdfb3d7f25a9d1d/src/main/scala/inox/transformers/SimplifierWithPC.scala lines 295-342).

[samarion]

Are the benchmarks available anywhere? In a coming update, Inox will be assuming everything is pure when used as a backend for Stainless so this should disappear for purity checks within the solver.

[jad-hamza]

I was able to find a pattern that creates a blowup. The inlining creates an exponential blowup of the the size of
the analyzed program, so it would make sense that the time to generate verification condition roughly doubles
every time we add a level. But it seems that something else is going on. Perhaps a quadratic blowup due to
the fact that isPure has to simplify the whole subexpression, and this is done for each let of the expression
tree). Or perhaps an exponential blowup when simplify is called multiple times on the same subexpression.
(e.g. the calls to simplify lines 317 and 332/338 in https://github.com/epfl-lara/inox/blob/082081b77e80a0e95696c8649bdfb3d7f25a9d1d/src/main/scala/inox/transformers/SimplifierWithPC.scala)

It takes about 10 seconds to generate the verification conditions (not counting verification) with

stainless-scalac --debug=verification --functions=lvl6 Nesting.scala
on my laptop. With --functions=lvl7, it took about 3 minutes.

When we remove the purity check, generation of verification conditions is almost instant (< 1s),
even for lvl7.

import scala.language.postfixOps
import stainless.lang._
import stainless.collection._

object Nesting {

  @inline
  def lvl1(n: BigInt) = {
    require (n >= 0)

    true
  } holds

  @inline
  def lvl2(n: BigInt) = {
    require (n >= 0)

    lvl1(0)
    lvl1(0)

    true
  } holds

  @inline
  def lvl3(n: BigInt) = {
    require(n >= 0)

    lvl2(0)
    lvl2(0)

    true
  } holds

  @inline
  def lvl4(n: BigInt) = {
    require (n >= 0)

    lvl3(0)
    lvl3(0)

    true
  } holds

  @inline
  def lvl5(n: BigInt) = {
    require (n >= 0)

    lvl4(0)
    lvl4(0)

    true
  } holds

  @inline
  def lvl6(n: BigInt) = {
    require (n >= 0)

    lvl5(0)
    lvl5(0)

    true
  } holds

  @inline
  def lvl7(n: BigInt) = {
    require (n >= 0)

    lvl6(0)
    lvl6(0)

    true
  } holds

}

[samarion]

Unfortunately, I don't think I can provide a perfect "fix" to this issue other than disabling simplifications. I've added a cache to the Let simplifications in 7204d2a which makes your example much faster but there are probably still some edge cases where the blowup will occur.

I thought of dropping the simplifications at some point but we have large speedups on some other benchmarks thanks to these so I ended up keeping them. You can try to use the --nosimplifications option to turn most simplifications off.

[jad-hamza]

I'm thinking about two points where perhaps we could improve the performance: 1) do we need to call
simplify to check for purity? 2) can we improve the simplify function, by avoiding to call it recursively
twice on the same subtree (lines 317 and 332)?

For 1), I'm thinking that we could traverse the whole program once (bottom-up), and mark all
Expressions which are pure/impure. This way the overall complexity stays linear in the size of the
program, instead of quadratic (at best) when doing a purity check/simplification at each level of the
tree.

For 2), can you explain a bit how the simplification works?

[samarion]

1. Purity is dependent on the path condition. For example, a.asInstanceOf[T] is pure iff there exists a.isInstanceOf[T] in the path condition. This means that marking standalone expressions is not an option for purity checking. However, we could make an alternate version of the simplifier that only checks purity without performing simplifications. This version could be linear in the size of the program. We would have an inconsistency between calls to isPure before and after simplification, but this may be an acceptable limitation.
2. The simplification of lets works as follows. If the variable occurs once or less in the let's body and the bound expression is pure, we substitute it into the body. However, in order to accurately count the number of occurrences of the variable in the body we need to first simplify the body, since we might count spurious occurrences otherwise. Then, after substituting the expression into the body, new simplification opportunities may appear (e.g. lambda applications). This is why we have to call simplify twice on the let's body.

[jad-hamza]

So the worst-case execution time for simplify is exponential in the size of the formula?
Lambda application meaning beta-reduction?

Don't you also need to call simplify again after that, since the lambda applications could give
rise to other simplification opportunities?

[samarion]

Yes, the worst case is exponential in the number of lets in the formula. I believe that in practice, the runtime shouldn't have to be exponential because lets almost never need to be re-simplified. The cache I added seems to support this claim, at least for the example you gave me.

Yes, s/lambda application/beta-reduction/g.

The simplifications that may occur due to beta-reductions will take place "locally" (when simplifying the application). When the simplifier sees an application with a known caller, it re-simplifies the inlined body, but this isn't exponential (I believe) because the re-simplification can only trigger once per application within an expression.

[samarion]

Closing this as I can't see a way to fix it more than what we currently have.
Note that if/once we decide that Stainless should use the assume-checked mode of Inox, this issue will completely disappear when used as Stainless' backend.