Fix computation of targets in let expressions

[jad-hamza]

The example LetTargets is failing in the current master branch, because the computation of targets in let expressions duplicates the path (once for the bound expression e, and once for the body b). We get targets which are not well-formed.

[samarion]

I'm not sure I understand, is the function inlining change related to the target computation issue?

[samarion]

Doesn't this mean we'll be duplicating potential checks in the function's body?

[jad-hamza]

Yes it can happen. Maybe we should let the user decide when to avoid let-bindings?

[samarion]

Could you just wrap the full body in @unchecked?

[jad-hamza]

This comment suggests that if we do that without let-binding, the @unchecked annotation could leak to not checking postconditions (I don't remember why):

stainless/core/src/main/scala/stainless/extraction/inlining/FunctionInlining.scala

Lines 122 to 124 in 2009c76

	// We bind the inlined expression in a let to avoid propagating
	// the @unchecked annotation to postconditions, etc.
	val newBody = let(res, inlined, res.toVariable.setPos(fi)).setPos(fi)

[samarion]

But this special case is guarded by specs being empty (so no postcondition)?

[jad-hamza]

The comment might be obsolete, I've tried to remove it and it worked on a small example (i.e. the postcondition of the caller of an inlined function wasn't ignored), let's see what happens on the full test suite.

[jad-hamza]

I found an example where we should avoid the unchecked annotation except in a let binding:

object InliningUnchecked2 {
  @inline def nonNegative(x: Int): Boolean = x >= 0

  def test: Int = {
    -10
  }.ensuring(nonNegative _)
}

In postconditions, the unchecked annotation means we don't check the conjunct. I think we already had this discussion once, we're basically using unchecked annotation to mean slightly different things depending on placement.

[samarion]

Ahhh, I understand. Wow, that's a bit dangerous. It means that if we inline lets before going to type checking, we'll stop checking post-conditions containing inlined calls?

Sounds like we should split @unchecked into two different annotations.

[jad-hamza]

(sorry I edited your post by mistake)

Ahhh, I understand. Wow, that's a bit dangerous. It means that if we inline lets before going to type checking, we'll stop checking post-conditions containing inlined calls?

Yes for instance this example (InliningUnchecked2) would go through.

Sounds like we should split @unchecked into two different annotations.

Yes good idea I'll do the split in another PR. Can we give a (more or less) formal definition to the two annotations?

• unchecked: don't generate VCs when type-checking this expression (that's a bit ambiguous)
• dropConjunct: drop this conjunct in VCs

Thanks for the review! I'll merge this PR for now and address this issue (and potentially others) in another one.

[gsps]

Some extra considerations to take into account when reshuffling the Unchecked annotation: #1136

[jad-hamza]

I'm not sure I understand, is the function inlining change related to the target computation issue?

No sorry, I've added a bunch of unrelated commits that you can ignore, only "Fix computation of targets in let expressions" is related to that