Fix extraction of extern types with Dotty frontend

epfl-lara · Feb 4, 2020 · 3cbf4cd · 3cbf4cd
1 parent 82892cf
commit 3cbf4cd
Show file tree

Hide file tree

Showing 2 changed files with 22 additions and 19 deletions.
diff --git a/frontends/benchmarks/verification/valid/Iterables.scala b/frontends/benchmarks/verification/valid/Iterables.scala
@@ -40,6 +40,7 @@ object Iterables {
     assert(!res.contains(6))
   }
 
+  // See https://github.com/epfl-lara/inox/issues/109
   // def test_setWithFilter(set: Set[BigInt]) = {
   //   require((set & oneToSix) == oneToSix)
 

diff --git a/frontends/dotty/src/main/scala/stainless/frontends/dotc/CodeExtraction.scala b/frontends/dotty/src/main/scala/stainless/frontends/dotc/CodeExtraction.scala
@@ -550,12 +550,28 @@ class CodeExtraction(inoxCtx: inox.Context, cache: SymbolsContext)(implicit val
     val extparams = typeParamSymbols(tdefs)
     val ntparams = typeParams.getOrElse(extractTypeParams(extparams))
 
-    val nctx = dctx.copy(tparams = dctx.tparams ++ (extparams zip ntparams))
+    val isAbstract = rhs == tpd.EmptyTree
 
-    val (newParams, fctx0) = vdefs.foldLeft((Seq.empty[xt.ValDef], nctx)) { case ((params, dctx), param) =>
+    var flags = annotationsOf(sym).filterNot(_ == xt.IsMutable) ++
+      (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 (!isAbstract && ((sym.isField) || (sym is Lazy))) Seq(xt.IsField(sym is Lazy)) else Seq()) ++
+      (if (isDefaultGetter(sym) || isCopyMethod(sym)) Seq(xt.Synthetic, xt.Inline) else Seq()) ++
+      (if ((isAbstract && sym.isField) || (!(sym is Lazy) && (sym is Accessor)))
+        Seq(xt.IsAccessor(Option(getIdentifier(sym.underlyingSymbol)).filterNot(_ => isAbstract)))
+      else Seq())
+
+    val nctx = dctx.copy(
+      tparams = dctx.tparams ++ (extparams zip ntparams),
+      isExtern = flags contains xt.Extern,
+    )
+
+    val (newParams, fctx) = vdefs.foldLeft((Seq.empty[xt.ValDef], nctx)) { case ((params, dctx), param) =>
       val flags = annotationsOf(param.symbol, ignoreOwner = true)
 
-      val tctx = dctx.withExtern(flags contains xt.Extern)
+      val tctx = dctx.withExtern(nctx.isExtern || flags.contains(xt.Extern))
       val tpe = stainlessType(param.tpe)(tctx, param.tpt.pos)
       val ptpe = extractType(param.tpt, param.tpe)(tctx)
 
@@ -568,28 +584,13 @@ class CodeExtraction(inoxCtx: inox.Context, cache: SymbolsContext)(implicit val
       (params :+ vd, dctx.withNewVar(param.symbol -> expr))
     }
 
-    val isAbstract = rhs == tpd.EmptyTree
-
-    var flags = annotationsOf(sym).filterNot(_ == xt.IsMutable) ++
-      (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 (!isAbstract && ((sym.isField) || (sym is Lazy))) Seq(xt.IsField(sym is Lazy)) else Seq()) ++
-      (if (isDefaultGetter(sym) || isCopyMethod(sym)) Seq(xt.Synthetic, xt.Inline) else Seq()) ++
-      (if ((isAbstract && sym.isField) || (!(sym is Lazy) && (sym is Accessor)))
-        Seq(xt.IsAccessor(Option(getIdentifier(sym.underlyingSymbol)).filterNot(_ => isAbstract)))
-      else Seq())
-
     if (sym.name == nme.unapply) {
       val isEmptyDenot = typer.Applications.extractorMember(sym.info.finalResultType, nme.isEmpty)
       val getDenot = typer.Applications.extractorMember(sym.info.finalResultType, nme.get)
       flags :+= xt.IsUnapply(getIdentifier(isEmptyDenot.symbol), getIdentifier(getDenot.symbol))
     }
 
-    lazy val retType = extractType(tree.tpt, sym.info.finalResultType)(fctx0)
-
-    val fctx = fctx0.copy(isExtern = fctx0.isExtern || (flags contains xt.Extern))
+    lazy val retType = extractType(tree.tpt, sym.info.finalResultType)(fctx)
 
     val (finalBody, returnType) = if (isAbstract) {
       flags :+= xt.IsAbstract
@@ -2019,6 +2020,7 @@ class CodeExtraction(inoxCtx: inox.Context, cache: SymbolsContext)(implicit val
         val id = getIdentifier(sym)
         val tps = args map extractType
 
+
         dctx.localClasses.get(id) match {
           case Some(lcd) => extractLocalClassType(tycon, lcd.id, tps)
           case None => xt.ClassType(id, tps)