Merge branch 'master' into rust-interop

# Conflicts: # build.sbt # core/src/main/scala/stainless/Component.scala # core/src/main/scala/stainless/MainHelpers.scala # core/src/main/scala/stainless/Reporter.scala # core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala # core/src/main/scala/stainless/extraction/imperative/EffectsAnalyzer.scala # core/src/main/scala/stainless/extraction/imperative/EffectsChecker.scala # core/src/main/scala/stainless/extraction/imperative/ReturnElimination.scala # core/src/main/scala/stainless/extraction/imperative/TransformerWithPC.scala # core/src/main/scala/stainless/extraction/imperative/TransformerWithType.scala # core/src/main/scala/stainless/extraction/imperative/Trees.scala # core/src/main/scala/stainless/extraction/inlining/FunctionInlining.scala # core/src/main/scala/stainless/extraction/innerfuns/FunctionClosure.scala # core/src/main/scala/stainless/extraction/trace/Trace.scala # core/src/main/scala/stainless/extraction/xlang/TreeSanitizer.scala # core/src/main/scala/stainless/frontend/BatchedCallBack.scala # core/src/main/scala/stainless/genc/CAST.scala # core/src/main/scala/stainless/genc/CPrinter.scala # core/src/main/scala/stainless/genc/ir/IR.scala # core/src/main/scala/stainless/genc/ir/Normaliser.scala # core/src/main/scala/stainless/genc/ir/Referentiator.scala # core/src/main/scala/stainless/genc/phases/ExtraOps.scala # core/src/main/scala/stainless/genc/phases/IR2CPhase.scala # core/src/main/scala/stainless/genc/phases/Scala2IRPhase.scala # core/src/sphinx/genc.rst # core/src/sphinx/purescala.rst # frontends/benchmarks/extraction/invalid/ArgumentAliasing.scala # frontends/benchmarks/imperative/valid/AccessorAliasing.scala # frontends/benchmarks/imperative/valid/MutableTuple.scala # frontends/benchmarks/verification/invalid/WhilePre.scala # frontends/common/src/it/scala/stainless/verification/ComponentTestSuite.scala # frontends/library/stainless/lang/StaticChecks.scala # frontends/library/stainless/lang/package.scala # frontends/scalac/src/it/scala/stainless/GencSuite.scala # frontends/scalac/src/main/scala/stainless/frontends/scalac/ASTExtractors.scala # frontends/scalac/src/main/scala/stainless/frontends/scalac/CodeExtraction.scala
epfl-lara · Jun 22, 2021 · 6c107dd · 6c107dd
2 parents f15f5b5 + f1f336e
commit 6c107dd
Show file tree

Hide file tree

Showing 112 changed files with 2,191 additions and 1,033 deletions.
diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md
@@ -1,5 +1,37 @@
 # Release Notes
 
+## Version 0.8.1 (2021-06-20)
+
+### Stainless frontend and internals
+
+- Better support for jumping to errors in IDEs (#966, #995, #996)
+- Add support for return keyword (#923, #925, #934)
+- Various fixes and changes in aliasing analysis (#915, #918, #920, #928, #965, #969, #973, #985, #1076, #1094)
+- Support for tuples with mutable types (#1064)
+- Add support for multiple requires in functions (not in ADTs) (#983)
+- Better measure inference for chain processor (#967)
+- Add more support for bitvector operations (#962, #1062)
+- Print verification progress but not all verification conditions by default (#1018)
+- Add support for swap operation for array elements (#946)
+- Add support for inlining and making opaque while loops (#1009)
+- Library cleanup (#953, #998, #999, #1000)
+- Add fresh copy primitive (#1033)
+- Improve traceInduct and add clustering (#1052)
+- Add no-return invariants for while loops (#1079)
+
+### SMT solvers
+
+- Add support for CVC4 1.8 (#833)
+- Add support for Z3 4.8.10 (#1010)
+
+### GenC
+
+- Better support for ``@export`` annotation in GenC (#924, #1008, #1019)
+- Add StructInliningPhase to remove structs with one member in GenC (#1058, #1065)
+- Add support for fixed length arrays in GenC (#1055, #1057)
+- Add compilation of global state in GenC (#1085, #1089)
+
+
 ## Version 0.8.0 (2021-02-24)
 
 ### Features

diff --git a/build.sbt b/build.sbt
@@ -68,14 +68,6 @@ lazy val artifactSettings: Seq[Setting[_]] = baseSettings ++ Seq(
   buildInfoOptions := Seq(BuildInfoOption.BuildTime),
 )
 
-// FIXME: Uncomment this when we are are able to upgrade sbt version
-// Global / excludeLintKeys ++= Set(
-//   buildInfoPackage,
-//   buildInfoKeys,
-//   buildInfoOptions,
-//   testOptions
-// )
-
 lazy val commonSettings: Seq[Setting[_]] = artifactSettings ++ Seq(
   scalacOptions ++= Seq(
     "-deprecation",

diff --git a/core/src/main/scala/stainless/Component.scala b/core/src/main/scala/stainless/Component.scala
@@ -93,30 +93,12 @@ trait ComponentRun { self =>
     val trees: self.trees.type
   } = inox.Program(trees)(extract(program.symbols))
 
-  /** Override this if you need another kind of filtering */
-  protected lazy val dependenciesFinder = new DependenciesFinder {
-    val t: self.trees.type = self.trees
-    protected def traverser(symbols: t.Symbols) = new {
-      val trees: t.type = t
-      val s: t.Symbols = symbols
-    } with DefinitionIdFinder
-  }
-
-  private def filter(ids: Seq[Identifier], symbols: trees.Symbols): trees.Symbols = {
-    dependenciesFinder.findDependencies(ids.toSet, symbols)
-  }
-
   /** Passes the provided symbols through the extraction pipeline and compute all
     * functions to process that are derived from the provided identifiers. */
-  def apply(ids: Seq[Identifier], symbols: xt.Symbols, filterSymbols: Boolean = false): Future[Analysis] = {
+  def apply(ids: Seq[Identifier], symbols: xt.Symbols): Future[Analysis] = {
     val exSymbols = extract(symbols)
-
     val toProcess = extractionFilter.filter(ids, exSymbols, component)
-
-    if (filterSymbols)
-      execute(toProcess, filter(toProcess, exSymbols))
-    else
-      execute(toProcess, exSymbols)
+    execute(toProcess, exSymbols)
   }
 
   def apply(id: Identifier, symbols: xt.Symbols): Future[Analysis] =

diff --git a/core/src/main/scala/stainless/MainHelpers.scala b/core/src/main/scala/stainless/MainHelpers.scala
@@ -51,6 +51,7 @@ trait MainHelpers extends inox.MainHelpers { self =>
       "  - termination: each solver call takes at most n / 100 seconds"),
     optJson -> Description(General, "Output verification and termination reports to a JSON file"),
     genc.optOutputFile -> Description(General, "File name for GenC output"),
+    genc.optIncludes -> Description(General, "Add includes in GenC output"),
     optWatch -> Description(General, "Re-run stainless upon file changes"),
     optCompact -> Description(General, "Print only invalid elements of summaries"),
     optInteractive -> Description(General, "Whether to run in interactive query mode"),
@@ -209,12 +210,14 @@ trait MainHelpers extends inox.MainHelpers { self =>
         case e @ extraction.MalformedStainlessCode(tree, msg) =>
           reporter.debug(e)(frontend.DebugSectionStack)
           ctx.reporter.error(tree.getPos, msg)
-          reporter.error("There was an error during the watch cycle")
-          reporter.reset()
-          compiler = newCompiler()
+        case e @ inox.FatalError(msg) =>
+          // we don't print the error message in this case because it was already printed before
+          // the `FatalError` was thrown
+          reporter.debug(e)(frontend.DebugSectionStack)
         case e: Throwable =>
           reporter.debug(e)(frontend.DebugSectionStack)
-          reporter.error("There was an error during the watch cycle")
+          reporter.error(e.getMessage)
+      } finally {
           compiler = newCompiler()
       }
 

diff --git a/core/src/main/scala/stainless/ast/Deconstructors.scala b/core/src/main/scala/stainless/ast/Deconstructors.scala
@@ -217,8 +217,10 @@ trait TreeDeconstructor extends inox.ast.TreeDeconstructor {
     case s.Unchecked => (Seq(), Seq(), Seq(), (_, _, _) => t.Unchecked)
     case s.Library => (Seq(), Seq(), Seq(), (_, _, _) => t.Library)
     case s.Synthetic => (Seq(), Seq(), Seq(), (_, _, _) => t.Synthetic)
-    case s.Derived(id) => (Seq(id), Seq(), Seq(), (ids, _, _) => t.Derived(ids.head))
+    case s.Derived(None) => (Seq(), Seq(), Seq(), (_, _, _) => t.Derived(None))
+    case s.Derived(Some(id)) => (Seq(id), Seq(), Seq(), (ids, _, _) => t.Derived(Some(ids.head)))
     case s.IsField(isLazy) => (Seq(), Seq(), Seq(), (_, _, _) => t.IsField(isLazy))
+    case s.ClassParamInit(cid) => (Seq(cid), Seq(), Seq(), (ids, _, _) => t.ClassParamInit(ids.head))
     case s.IsUnapply(isEmpty, get) => (Seq(isEmpty, get), Seq(), Seq(), (ids, _, _) => t.IsUnapply(ids(0), ids(1)))
     case s.PartialEval => (Seq(), Seq(), Seq(), (_, _, _) => t.PartialEval)
     case s.Wrapping => (Seq(), Seq(), Seq(), (_, _, _) => t.Wrapping)

diff --git a/core/src/main/scala/stainless/ast/Definitions.scala b/core/src/main/scala/stainless/ast/Definitions.scala
@@ -29,9 +29,10 @@ trait Definitions extends inox.ast.Definitions { self: Trees =>
   case object Wrapping extends Flag("wrapping", Seq.empty)
   case object Template extends Flag("template", Seq.empty)
 
-  case class Derived(id: Identifier) extends Flag("derived", Seq(id))
+  case class Derived(idOpt: Option[Identifier]) extends Flag("derived", idOpt.toSeq)
   case class IsField(isLazy: Boolean) extends Flag("field", Seq.empty)
   case class IsUnapply(isEmpty: Identifier, get: Identifier) extends Flag("unapply", Seq(isEmpty, get))
+  case class ClassParamInit(cid: Identifier) extends Flag("paramInit", Seq(cid))
 
   case class TerminationStatus(status: TerminationReport.Status) extends Flag("termination", Seq(status))
 
@@ -123,7 +124,7 @@ trait Definitions extends inox.ast.Definitions { self: Trees =>
      *      holds the requested data.
      */
     final def source: Identifier =
-      fd.flags collectFirst { case Derived(id) => id } getOrElse fd.id
+      fd.flags collectFirst { case Derived(Some(id)) => id } getOrElse fd.id
   }
 
   implicit class StainlessTypedFunDef(tfd: TypedFunDef) {

diff --git a/core/src/main/scala/stainless/ast/SymbolOps.scala b/core/src/main/scala/stainless/ast/SymbolOps.scala
@@ -251,4 +251,14 @@ trait SymbolOps extends inox.ast.SymbolOps { self: TypeOps =>
     if (s.isEmpty) ""
     else "-------------" + header + "-------------\n" + s + "\n\n"
   }
+
+  def paramInits(id: Identifier): Seq[FunDef] = {
+    symbols.functions.values.toSeq.filter {
+      case fd => fd.flags.exists {
+        case ClassParamInit(cid) => id == cid
+        case _ => false
+      }
+    }.sortBy(_.id.name.stripPrefix("apply$default$").toInt)
+  }
+
 }