From a1cd47c54e1cf4e7dad0ae4cca3eb4827d39ccf2 Mon Sep 17 00:00:00 2001 From: Mario Bucev Date: Fri, 26 Jan 2024 09:21:39 +0100 Subject: [PATCH] Add missing case for Array typeBounds, make private final, fix minor bug in RefinementLifting --- .../stainless/extraction/oo/RefinementLifting.scala | 6 ++++-- .../src/main/scala/stainless/extraction/oo/TypeOps.scala | 3 +++ .../benchmarks/verification/valid/ArrayOfTypeAlias.scala | 5 +++++ .../benchmarks/verification/valid/PrivateIsFinal.scala | 9 +++++++++ .../scala/stainless/frontends/dotc/CodeExtraction.scala | 2 +- .../stainless/frontends/scalac/CodeExtraction.scala | 2 +- 6 files changed, 23 insertions(+), 4 deletions(-) create mode 100644 frontends/benchmarks/verification/valid/ArrayOfTypeAlias.scala create mode 100644 frontends/benchmarks/verification/valid/PrivateIsFinal.scala diff --git a/core/src/main/scala/stainless/extraction/oo/RefinementLifting.scala b/core/src/main/scala/stainless/extraction/oo/RefinementLifting.scala index c4846f7f59..4ab1034c6f 100644 --- 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 index 380c4b28a4..e1795c8d5e 100644 --- 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 new file mode 100644 index 0000000000..c396ebf04f --- /dev/null +++ b/frontends/benchmarks/verification/valid/ArrayOfTypeAlias.scala @@ -0,0 +1,5 @@ +object ArrayOfTypeAlias { + type AliasedLong = Long + + case class SomeClass(arr: Array[AliasedLong]) +} \ No newline at end of file diff --git a/frontends/benchmarks/verification/valid/PrivateIsFinal.scala b/frontends/benchmarks/verification/valid/PrivateIsFinal.scala new file mode 100644 index 0000000000..3bb0454dcf --- /dev/null +++ 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 index 8a1fe8a8ca..19d27989ac 100644 --- 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 index 13c1f42b98..dd419f5b04 100644 --- 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)