Fix inlinePosts

[jad-hamza]

Fix https://github.com/epfl-lara/stainless/issues/568

I'm not 100% sure how best to fix this... as a temporary solution, you could replace collect with transformWithPC and make sure the generated conjuncts are wrapped with the relevant path.

I used collectWithPC, is that ok? And I used implies to wrap the path, not sure if that's good.

[jad-hamza]

samarion approved these changes

larabot didn't approve :( It's probably because path implies _ ignores the OpenBound's?

[samarion]

OpenBounds were ignored before, so that shouldn't be the issue.

Maybe you need some freshening in the generated clause.

Also skipping inlinings when the path contains open bounds is probably a good idea.

[jad-hamza]

I had a look at the new problem with Lang.scala-0.tip but that doesn't seem related to inlinePosts, there are variables which are not fresh (x$0 appears several times) before entering the simplification functions. Should everything be fresh before entering mergeFunctions?

// before mergeFunctions
¬fun1!4$0[List!4$0[Int], Boolean](Lang!3$0[Int](fun1!4$0[List!4$0[Int], Boolean]((x$0: List!4$0[Int]) => ¬∀x$1: BigInt. ¬¬¬(((x$1 <= size!0$0[Int](x$0) && x$1 >= 0) && contains!1$0[Int](Lang!3$0[Int](fun1!4$0[List!4$0[Int], Boolean]((x$0: List!4$0[Int]) => x$0 == Cons!3$0[Int](3, Nil!3$0[Int]()), (x$0: List!4$0[Int]) => true)), take!0$0[Int](x$0, x$1))) && contains!1$0[Int](Lang!3$0[Int](fun1!4$0[List!4$0[Int], Boolean]((x$0: List!4$0[Int]) => x$0 == Cons!3$0[Int](5, Nil!3$0[Int]()), (x$0: List!4$0[Int]) => true)), drop!0$0[Int](x$0, x$1))), (x$0: List!4$0[Int]) => true)).f!45$0.pre!12$0, (x!93$0: List!4$0[Int]) => true).f!46$0(x!56$0)

// after mergeFunctions
¬fun1!4$0[List!4$0[Int], Boolean](Lang!3$0[Int](fun1!4$0[List!4$0[Int], Boolean]((x$0: List!4$0[Int]) => ¬∀x$1: BigInt. {
  val call$43: BigInt = size!0$0[Int](x$0)
  ¬¬¬(((x$1 <= call$43 && x$1 >= 0) && {
    val call$38: List!4$0[Int] = take!0$0[Int](x$0, x$1)
    val call$37: Boolean = contains!1$0[Int](Lang!3$0[Int](fun1!4$0[List!4$0[Int], Boolean]((x$0: List!4$0[Int]) => x$0 == Cons!3$0[Int](3, Nil!3$0[Int]()), (x$0: List!4$0[Int]) => true)), call$38)
    call$37
  }) && {
    val call$42: List!4$0[Int] = drop!0$0[Int](x$0, x$1)
    val call$41: Boolean = contains!1$0[Int](Lang!3$0[Int](fun1!4$0[List!4$0[Int], Boolean]((x$0: List!4$0[Int]) => x$0 == Cons!3$0[Int](5, Nil!3$0[Int]()), (x$0: List!4$0[Int]) => true)), call$42)
    call$41
  })
}, (x$0: List!4$0[Int]) => true)).f!45$0.pre!12$0, (x!93$0: List!4$0[Int]) => true).f!46$0(x!56$0)

// before simplifyForalls
¬fun1!4$0[List!4$0[Int], Boolean](Lang!3$0[Int](fun1!4$0[List!4$0[Int], Boolean]((x$0: List!4$0[Int]) => ¬∀x$1: BigInt. {
  val call$43: BigInt = size!0$0[Int](x$0)
  ¬¬¬(((x$1 <= call$43 && x$1 >= 0) && {
    val call$38: List!4$0[Int] = take!0$0[Int](x$0, x$1)
    val call$37: Boolean = contains!1$0[Int](Lang!3$0[Int](fun1!4$0[List!4$0[Int], Boolean]((x$0: List!4$0[Int]) => x$0 == Cons!3$0[Int](3, Nil!3$0[Int]()), (x$0: List!4$0[Int]) => true)), call$38)
    call$37
  }) && {
    val call$42: List!4$0[Int] = drop!0$0[Int](x$0, x$1)
    val call$41: Boolean = contains!1$0[Int](Lang!3$0[Int](fun1!4$0[List!4$0[Int], Boolean]((x$0: List!4$0[Int]) => x$0 == Cons!3$0[Int](5, Nil!3$0[Int]()), (x$0: List!4$0[Int]) => true)), call$42)
    call$41
  })
}, (x$0: List!4$0[Int]) => true)).f!45$0.pre!12$0, (x!93$0: List!4$0[Int]) => true).f!46$0(x!56$0)

[info]   java.lang.AssertionError: assertion failed: CANNOT ADD x$0: List!4$0[Int] to
[info] val call$43: BigInt = size!0$0[Int](x$0)
[info] x$1 <= call$43 && (x$1 >= 0 && {
[info]   val call$38: List!4$0[Int] = take!0$0[Int](x$0, x$1)
[info]   true
[info] })

[jad-hamza]

Apparently, expressions don't have unique identifiers after the parser, for instance:

¬fun1!4$0[List!4$0[Int], Boolean](Lang!3$0[Int](fun1!4$0[List!4$0[Int], Boolean]((x$0: List!4$0[Int]) => x$0 == Cons!3$0[Int](5, Nil!3$0[Int]()), (x$0: List!4$0[Int]) => true)).f!45$0.pre!12$0, (x!93$0: List!4$0[Int]) => true).f!46$0(x!56$0)

Is that normal? (Also freshenLocals isn't designed to freshen those)

[samarion]

Well, lambda normalization will normalize identifiers, which can create duplicates. Lambda normalization is used in some places which aren't ideal, e.g. the recursive evaluator so you could be seeing bad interactions there.

Which parser do you mean? The TIP parser freshens all variable names.

Also, what do you mean about freshenLocals not being designed for certain variables?

[jad-hamza]

Well, lambda normalization will normalize identifiers, which can create duplicates. Lambda normalization is used in some places which aren't ideal, e.g. the recursive evaluator so you could be seeing bad interactions there.

So should we expect to have duplicates when entering simplifyFormula? And then freshen on the fly on places where it causes a crash?

Which parser do you mean? The TIP parser freshens all variable names.

Yes my bad, I thought the expression above with duplicates came from the parser but in fact other transformations happened in between.

Also, what do you mean about freshenLocals not being designed for certain variables?

I think it doesn't deduplicate, and transforms (x$0 => x$0, x$0 => x$0) into (x$1 => x$1, x$1 => x$1) rather than (x$1 => x$1, x$2 => x$2)? That's probably on purpose?

[samarion]

So should we expect to have duplicates when entering simplifyFormula? And then freshen on the fly on places where it causes a crash?

I don't think this is something we want to support. Ideally, we should find the places where duplication actually occurs and correctly freshen variables at that point.

The RecursiveEvaluator could also be fixed by either

1. implementing a recursive function for Equals in order to avoid the normalization step when evaluating lambda values, or
2. explicitly defining a value normalization function which is used only during Equals evaluation.

I think it doesn't deduplicate, and transforms (x$0 => x$0, x$0 => x$0) into (x$1 => x$1, x$1 => x$1) rather than (x$1 => x$1, x$2 => x$2)? That's probably on purpose?

Oh, I didn't notice that. I don't think this is desired.

You can probably fix the behavior by using a Transformer with environment instead of storing a global mapping.

[jad-hamza]

I don't think this is something we want to support. Ideally, we should find the places where duplication actually occurs and correctly freshen variables at that point.

Ok thanks, I'll try to find where these come from.

The RecursiveEvaluator could also be fixed by either

1. implementing a recursive function for Equals in order to avoid the normalization step when evaluating lambda values, or
2. explicitly defining a value normalization function which is used only during Equals evaluation.

If I fix the duplication, is that still needed for that PR?

You can probably fix the behavior by using a Transformer with environment instead of storing a global mapping.

I'm not sure what should be the behavior with Choose when freshenChoose is false: https://github.com/epfl-lara/inox/blob/93503b1f7cffd68ae44483cdc2170cafba38eaa4/src/main/scala/inox/ast/ExprOps.scala#L85-L88

[samarion]

If I fix the duplication, is that still needed for that PR?

Well, that might be one of the sources of duplication (and you can't remove it currently because that would break Equals evaluation). I guess you could make sure to freshen locales before going to the solver, and that might be enough...

I'm not sure what should be the behavior with Choose when freshenChoose is false.

The current behavior should be preserved (don't freshen the choose variable). Chooses are a bit special, they behave more like a named function than a variable.

[jad-hamza]

I fixed some duplications (pushed on this branch), and that fixed the Lang.scala-0.tip example but as you suggested this breaks other things. If I understand correctly, for now you suggest I keep the things that add duplication, but freshen with the new freshenLocals when entering solveSAT or other solver functions?

edit: My freshenLocals is broken at the moment, I'll use the Env as you suggested

[jad-hamza]

I removed the freshening that I had added during RecursiveEvaluator and fixed freshenLocals, and now things seem to work!

[samarion]

and now things seem to work!

Black magic :)

For freshenLocals, we ideally shouldn't do case matching on specific trees otherwise the method won't work on more complex Stainless trees. If you create the initial env based on variablesOf(expr), you should be able to use the following pattern to generalize the transformation to arbitrary trees:

override def transform(e: Expr, env: Env): Expr = e match {
  case v: Variable => env(v)
  case _ =>
    val (..., vs, ...) = deconstructor.deconstruct(e)
    val newEnv = vs.foldLeft(env) { case (env, v) =>
      if (env contains v) env // probably should never happen but I'm not 100% sure
      else env + (v -> super.transform(v).freshen)
    }
    super.transform(e, newEnv)
}

I use super.transform(v).freshen when constructing newEnv in order to make sure we correctly modify potential variables in the dependent type of v.

Also, please preserve the freshenChooses: Boolean = false optional argument.

[jad-hamza]

@samarion Should be good now, thanks for the help! The PR for Stainless is ready as well: https://github.com/epfl-lara/stainless/pull/912/ (the build refers to Inox master so larabot on Stainless can only go through after this is merged)