stainless

stainless copied to clipboard

In the function binding, elemRef$0 goes from type Array[(K$24, T$78)] (before TypeEncoding) to Array[({ x$629: Object$0 | ⟨@unchecked ⟨⟨K$40 : (Object$0) => Boolean ⟩(⟨x$629 : Object$0 ⟩) : Boolean ⟩ : Boolean ⟩ }, T$78)] (after TypeEncoding), but in the body of the function after TypeEncoding, elemRef$0 has type Array[(Object$0, T$78)]. Is there a reason for dropping the refinement? I see a dropRefinements here: https://github.com/epfl-lara/stainless/blob/1fa4365e71fc4ad054ea051a0a1d09f1027a3480/core/src/main/scala/stainless/extraction/oo/TypeEncoding.scala#L1207 I don't know if that's the cause?

[ Debug  ] Symbols before TypeEncoding
[ Debug  ] 
[ Debug  ] -------------Functions-------------
[ Debug  ] def insert$0[K$24, T$78](thiss$4: SortedArray$2[K$24, T$78], elemRef$0: Array[(K$24, T$78)]): (Unit, SortedArray$2[K$24, T$78], Array[(K$24, T$78)]) = ⟨{
[ Debug  ]   ⟨require(⟨⟨⟨⟨thiss$4 : SortedArray$2[K$24, T$78] ⟩.array$18 : Array[(K$24, T$78)] ⟩.length : Int ⟩ > ⟨0 : Int ⟩ : Boolean ⟩)
[ Debug  ]   ⟨require(⟨isSorted$1[K$24, T$78](⟨⟨thiss$4 : SortedArray$2[K$24, T$78] ⟩.array$18 : Array[(K$24, T$78)] ⟩, ⟨⟨thiss$4 : SortedArray$2[K$24, T$78] ⟩.order$15 : TotalOrder$0[K$24] ⟩) : Boolean ⟩)
[ Debug  ]   ⟨require(⟨⟨⟨elemRef$0 : Array[(K$24, T$78)] ⟩.length : Int ⟩ == ⟨1 : Int ⟩ : Boolean ⟩)
[ Debug  ]   ⟨val elemRef$2: Array[(K$24, T$78)] = ⟨elemRef$0 : Array[(K$24, T$78)] ⟩

[ Debug  ] Symbols after TypeEncoding
[ Debug  ] 
[ Debug  ] -------------Functions-------------
[ Debug  ] @derived(insert$0)
[ Debug  ] def insert$1[T$94](thiss$93: SortedArray$2[Object$0, T$94], elemRef$19: Array[(Object$0, T$94)]): (Unit, SortedArray$2[Object$0, T$94], Array[(Object$0, T$94)]) = ⟨<empty tree>[(Unit, SortedArray$2[Object$0, T$94], Array[(Object$0, T$94)])] : (Unit, SortedArray$2[Object$0, T$94], Array[(Object$0, T$94)]) ⟩
[ Debug  ] 
[ Debug  ] def insert$0[T$78](K$40: (Object$0) => Boolean, thiss$4: SortedArray$2[{ x$628: Object$0 | ⟨@unchecked ⟨⟨K$40 : (Object$0) => Boolean ⟩(⟨x$628 : Object$0 ⟩) : Boolean ⟩ : Boolean ⟩ }, T$78], elemRef$0: Array[({ x$629: Object$0 | ⟨@unchecked ⟨⟨K$40 : (Object$0) => Boolean ⟩(⟨x$629 : Object$0 ⟩) : Boolean ⟩ : Boolean ⟩ }, T$78)]): (Unit, SortedArray$2[{ x$630: Object$0 | ⟨@unchecked ⟨⟨K$40 : (Object$0) => Boolean ⟩(⟨x$630 : Object$0 ⟩) : Boolean ⟩ : Boolean ⟩ }, T$78], Array[({ x$631: Object$0 | ⟨@unchecked ⟨⟨K$40 : (Object$0) => Boolean ⟩(⟨x$631 : Object$0 ⟩) : Boolean ⟩ : Boolean ⟩ }, T$78)]) = ⟨{
[ Debug  ]   ⟨require(⟨⟨⟨⟨thiss$4 : SortedArray$2[Object$0, T$78] ⟩.array$18 : Array[(Object$0, T$78)] ⟩.length : Int ⟩ > ⟨0 : Int ⟩ : Boolean ⟩)
[ Debug  ]   ⟨require(⟨isSorted$1[T$78](⟨K$40 : (Object$0) => Boolean ⟩, ⟨⟨thiss$4 : SortedArray$2[Object$0, T$78] ⟩.array$18 : Array[(Object$0, T$78)] ⟩, ⟨⟨thiss$4 : SortedArray$2[Object$0, T$78] ⟩.order$15 : Object$0 ⟩) : Boolean ⟩)
[ Debug  ]   ⟨require(⟨⟨⟨elemRef$0 : Array[(Object$0, T$78)] ⟩.length : Int ⟩ == ⟨1 : Int ⟩ : Boolean ⟩)
[ Debug  ]   ⟨val elemRef$2: Array[({ x$637: Object$0 | ⟨@unchecked ⟨⟨K$40 : (Object$0) => Boolean ⟩(⟨x$637 : Object$0 ⟩) : Boolean ⟩ : Boolean ⟩ }, T$78)] = ⟨elemRef$0 : Array[(Object$0, T$78)] ⟩

Hmm, this is quite strange. It seems like all the function params are incorrectly transformed inside the body.
I don't think the dropRefinements function is the problem.

In order to narrow down the issue, could you please print the transformation result here: https://github.com/epfl-lara/stainless/blob/1fa4365e71fc4ad054ea051a0a1d09f1027a3480/core/src/main/scala/stainless/extraction/oo/TypeEncoding.scala#L971-L978

Thanks for having a look! I have added some debug but it's not ideal because I cannot use printTypes here without symbols. Is there something you'd like to see?

[ Debug  ] Symbols before TypeEncoding
[ Debug  ] 
[ Debug  ] -------------Functions-------------
[ Debug  ] def insert$0[K$24, T$78](thiss$4: SortedArray$2[K$24, T$78], elemRef$0: Array[(K$24, T$78)]): (Unit, SortedArray$2[K$24, T$78], Array[(K$24, T$78)]) = ⟨{
[ Debug  ]   ⟨require(⟨⟨⟨⟨thiss$4 : SortedArray$2[K$24, T$78] ⟩.array$18 : Array[(K$24, T$78)] ⟩.length : Int ⟩ > ⟨0 : Int ⟩ : Boolean ⟩)
[ Debug  ]   ⟨require(⟨isSorted$1[K$24, T$78](⟨⟨thiss$4 : SortedArray$2[K$24, T$78] ⟩.array$18 : Array[(K$24, T$78)] ⟩, ⟨⟨thiss$4 : SortedArray$2[K$24, T$78] ⟩.order$15 : TotalOrder$0[K$24] ⟩) : Boolean ⟩)
[ Debug  ]   ⟨require(⟨⟨⟨elemRef$0 : Array[(K$24, T$78)] ⟩.length : Int ⟩ == ⟨1 : Int ⟩ : Boolean ⟩)
[ Debug  ]   ⟨val elemRef$2: Array[(K$24, T$78)] = ⟨elemRef$0 : Array[(K$24, T$78)] ⟩

// Added debug
(fd.id,insert$0)
(ntparams,List(T$78))
(tparamParams,List(K$40: (Object$0) => Boolean))
(fd.params.map(scope.transform(_)),List(thiss$4: SortedArray$2[{ x$1205: Object$0 | @unchecked K$40(x$1205) }, T$78], elemRef$0: Array[({ x$1206: Object$0 | @unchecked K$40(x$1206) }, T$78)]))
(scope.transform(fd.returnType),(Unit, SortedArray$2[{ x$1207: Object$0 | @unchecked K$40(x$1207) }, T$78], Array[({ x$1208: Object$0 | @unchecked K$40(x$1208) }, T$78)]))
(scope.transform(fd.fullBody, fd.returnType.getType),{
  require(thiss$4.array$18.length > 0)
  require(isSorted$1[T$78](K$40, thiss$4.array$18, thiss$4.order$15))
  require(elemRef$0.length == 1)
  val elemRef$2: Array[({ x$1214: Object$0 | @unchecked K$40(x$1214) }, T$78)] = elemRef$0

[ Debug  ] Symbols after TypeEncoding
[ Debug  ] 
[ Debug  ] -------------Functions-------------
[ Debug  ] @derived(insert$0)
[ Debug  ] def insert$1[T$94](thiss$93: SortedArray$2[Object$0, T$94], elemRef$19: Array[(Object$0, T$94)]): (Unit, SortedArray$2[Object$0, T$94], Array[(Object$0, T$94)]) = ⟨<empty tree>[(Unit, SortedArray$2[Object$0, T$94], Array[(Object$0, T$94)])] : (Unit, SortedArray$2[Object$0, T$94], Array[(Object$0, T$94)]) ⟩
[ Debug  ] 
[ Debug  ] def insert$0[T$78](K$40: (Object$0) => Boolean, thiss$4: SortedArray$2[{ x$628: Object$0 | ⟨@unchecked ⟨⟨K$40 : (Object$0) => Boolean ⟩(⟨x$628 : Object$0 ⟩) : Boolean ⟩ : Boolean ⟩ }, T$78], elemRef$0: Array[({ x$629: Object$0 | ⟨@unchecked ⟨⟨K$40 : (Object$0) => Boolean ⟩(⟨x$629 : Object$0 ⟩) : Boolean ⟩ : Boolean ⟩ }, T$78)]): (Unit, SortedArray$2[{ x$630: Object$0 | ⟨@unchecked ⟨⟨K$40 : (Object$0) => Boolean ⟩(⟨x$630 : Object$0 ⟩) : Boolean ⟩ : Boolean ⟩ }, T$78], Array[({ x$631: Object$0 | ⟨@unchecked ⟨⟨K$40 : (Object$0) => Boolean ⟩(⟨x$631 : Object$0 ⟩) : Boolean ⟩ : Boolean ⟩ }, T$78)]) = ⟨{
[ Debug  ]   ⟨require(⟨⟨⟨⟨thiss$4 : SortedArray$2[Object$0, T$78] ⟩.array$18 : Array[(Object$0, T$78)] ⟩.length : Int ⟩ > ⟨0 : Int ⟩ : Boolean ⟩)
[ Debug  ]   ⟨require(⟨isSorted$1[T$78](⟨K$40 : (Object$0) => Boolean ⟩, ⟨⟨thiss$4 : SortedArray$2[Object$0, T$78] ⟩.array$18 : Array[(Object$0, T$78)] ⟩, ⟨⟨thiss$4 : SortedArray$2[Object$0, T$78] ⟩.order$15 : Object$0 ⟩) : Boolean ⟩)
[ Debug  ]   ⟨require(⟨⟨⟨elemRef$0 : Array[(Object$0, T$78)] ⟩.length : Int ⟩ == ⟨1 : Int ⟩ : Boolean ⟩)
[ Debug  ]   ⟨val elemRef$2: Array[({ x$637: Object$0 | ⟨@unchecked ⟨⟨K$40 : (Object$0) => Boolean ⟩(⟨x$637 : Object$0 ⟩) : Boolean ⟩ : Boolean ⟩ }, T$78)] = ⟨elemRef$0 : Array[(Object$0, T$78)] ⟩

Ah, the information I need is indeed inside the missing types. Maybe you can call variablesOf on the transformed fullBody and print the free variables (with unique ids)? That might show what we're looking for.

@mario-bucev is this related to the fix https://github.com/epfl-lara/stainless/commit/023bbb2e84f429641feb923152e6a03bcd20483c ?

It does not to seem to be related as this phase occurs before the type checker

It may be related to some inability to prove expected things in examples we have seen recently.

Good point !