Add missing case for Array typeBounds, make private final, fix minor …

…bug in RefinementLifting
epfl-lara · Jan 29, 2024 · 1001219 · 1001219
1 parent 536d418
commit 1001219
Show file tree

Hide file tree

Showing 6 changed files with 23 additions and 4 deletions.
diff --git a/core/src/main/scala/stainless/extraction/oo/RefinementLifting.scala b/core/src/main/scala/stainless/extraction/oo/RefinementLifting.scala
@@ -77,8 +77,10 @@ class RefinementLifting(override val s: Trees, override val t: Trees)
           val (Seq(nvd), pred2) = parameterConds(Seq(vd.copy(tpe = vd2.tpe).copiedFrom(vd)))
 
           (nvd, s.exprOps.replaceFromSymbols(Map(vd2 -> nvd.toVariable), s.and(pred, pred2)))
-        case _ =>
-          (vd, s.BooleanLiteral(true).copiedFrom(vd))
+        case t =>
+          // Note: t may have been dealiased, hence we need to update the type of the variable
+          // so it is consistent with each of its occurrence in the body of the function
+          (vd.copy(tpe = t), s.BooleanLiteral(true).copiedFrom(vd))
       }).unzip
 
       (newParams, s.andJoin(conds))

diff --git a/core/src/main/scala/stainless/extraction/oo/TypeOps.scala b/core/src/main/scala/stainless/extraction/oo/TypeOps.scala
@@ -122,6 +122,9 @@ trait TypeOps extends innerfuns.TypeOps { self =>
     case (MapType(f1, t1), MapType(f2, t2)) if leastUpperBound(f1, f2) == greatestLowerBound(f1, f2) =>
       Some(MapType(f1, typeBound(t1, t2, upper)))
 
+    case (ArrayType(b1), ArrayType(b2)) if leastUpperBound(b1, b2) == greatestLowerBound(b1, b2) =>
+      Some(ArrayType(b1))
+
     case _ => None
   }).getOrElse(if (upper) AnyType() else NothingType()).getType
 

diff --git a/frontends/benchmarks/verification/valid/ArrayOfTypeAlias.scala b/frontends/benchmarks/verification/valid/ArrayOfTypeAlias.scala
@@ -0,0 +1,5 @@
+object ArrayOfTypeAlias {
+  type AliasedLong = Long
+
+  case class SomeClass(arr: Array[AliasedLong])
+}
diff --git a/frontends/benchmarks/verification/valid/PrivateIsFinal.scala b/frontends/benchmarks/verification/valid/PrivateIsFinal.scala
@@ -0,0 +1,9 @@
+object PrivateIsFinal {
+  trait SomeTrait {
+    private def someSecret(x: BigInt): BigInt = x + 42
+
+    final def testSecret(x: BigInt): Unit = {
+      assert(someSecret(x) == 42 + x)
+    }
+  }
+}
diff --git a/frontends/dotty/src/main/scala/stainless/frontends/dotc/CodeExtraction.scala b/frontends/dotty/src/main/scala/stainless/frontends/dotc/CodeExtraction.scala
@@ -724,7 +724,7 @@ class CodeExtraction(inoxCtx: inox.Context, symbolMapping: SymbolMapping)(using
       (if ((sym is Implicit) && (sym is Synthetic)) Seq(xt.Inline, xt.Synthetic) else Seq()) ++
       (if (sym is Inline) Seq(xt.Inline) else Seq()) ++
       (if (sym is Private) Seq(xt.Private) else Seq()) ++
-      (if (sym is Final) Seq(xt.Final) else Seq()) ++
+      (if (sym.isEffectivelyFinal) Seq(xt.Final) else Seq()) ++
       (if (isDefaultGetter(sym) || isCopyMethod(sym)) Seq(xt.Synthetic, xt.Inline) else Seq())
 
     if (sym.name == nme.unapply) {

diff --git a/frontends/scalac/src/main/scala/stainless/frontends/scalac/CodeExtraction.scala b/frontends/scalac/src/main/scala/stainless/frontends/scalac/CodeExtraction.scala
@@ -608,7 +608,7 @@ trait CodeExtraction extends ASTExtractors {
     var flags = annotationsOf(sym).filterNot(annot => annot == xt.IsMutable || annot.name == "inlineInvariant") ++
       (if (sym.isImplicit && sym.isSynthetic) Seq(xt.Inline, xt.Synthetic) else Seq()) ++
       (if (sym.isPrivate) Seq(xt.Private) else Seq()) ++
-      (if (sym.isFinal) Seq(xt.Final) else Seq()) ++
+      (if (sym.isEffectivelyFinal) Seq(xt.Final) else Seq()) ++
       (if (sym.isVal || sym.isLazy) Seq(xt.IsField(sym.isLazy)) else Seq()) ++
       (if (isDefaultGetter(sym) || isCopyMethod(sym)) Seq(xt.Synthetic, xt.Inline) else Seq()) ++
       (if (!sym.isLazy && sym.isAccessor)