Merge branch 'master' into trace-ensuring-newspecs

core/src/main/scala/stainless/ast/ExprOps.scala

@@ -275,7 +275,7 @@ trait ExprOps extends inox.ast.ExprOps { self =>
     withSpec(expr, pred.filterNot(_.body == BooleanLiteral(true)).map(Postcondition).toLeft(PostconditionKind))
 
   final def withMeasure(expr: Expr, measure: Option[Expr]): Expr =
-    withSpec(expr, measure.map(Measure).toLeft(MeasureKind))
+    withSpec(expr, measure.map(expr => Measure(expr).setPos(expr)).toLeft(MeasureKind))
 
   /** Adds a body to a specification
     *

core/src/main/scala/stainless/extraction/package.scala

@@ -57,6 +57,15 @@ package object extraction {
     "PartialEvaluation"         -> "Partially evaluate marked function calls",
     "AssertionInjector"         -> "Insert assertions which verify array accesses, casts, division by zero, etc.",
     "ChooseInjector"            -> "Insert chooses where necessary",
+
+    "ComputeDependencies"       -> "(GenC) Compute the dependencies of a given definition",
+    "ComputeFunCtxPhase"        -> "(GenC) Compute the context of each given function definition",
+    "Scala2IRPhase"             -> "(GenC) Convert the Stainless AST into GenC's IR",
+    "StructInliningPhase"       -> "(GenC) Inline structs which have just one member",
+    "NormalisationPhase"        -> "(GenC) Normalise IR to match the C execution model",
+    "LiftingPhase"              -> "(GenC) Lift class types to their hierarchy top class",
+    "ReferencingPhase"          -> "(GenC) Add 'referencing' to the input LIR program to produce a RIR program",
+    "IR2CPhase"                 -> "(GenC) From IR to C",
   )
 
   val phaseNames: Set[String] = phases.map(_._1).toSet

core/src/main/scala/stainless/genc/CAST.scala

@@ -26,8 +26,13 @@ import ir.Literals._
  */
 object CAST { // C Abstract Syntax Tree
 
-  sealed abstract class Tree
-
+  sealed abstract class Tree {
+    override def toString = {
+      val sb = new StringBuffer()
+      new CPrinter("stainless.h", true, Set(), sb).print(this)
+      sb.toString
+    }
+  }
 
   /* ----------------------------------------------------- Definitions  ----- */
   abstract class Def extends Tree
@@ -44,6 +49,7 @@ object CAST { // C Abstract Syntax Tree
     functions: Set[Fun]
   ) extends Def {
     require(types.length == types.distinct.length) // no duplicates in `types`
+
   }
 
   // Manually defined function through the cCode.function annotation have a string
@@ -90,6 +96,8 @@ object CAST { // C Abstract Syntax Tree
     require(literals.nonEmpty)
   }
 
+  case class FixedArrayType(base: Type, length: Int) extends Type
+
 
   /* ------------------------------------------------------ Expressions ----- */
   abstract class Expr extends Tree

core/src/main/scala/stainless/genc/CASTDependencies.scala

@@ -20,6 +20,9 @@ class CASTTraverser(implicit ctx: inox.Context) {
     case FunType(ret, params) =>
       ret +: params
 
+    case FixedArrayType(base, _) =>
+      Seq(base)
+
     case Struct(id, fields, _) =>
       id +: fields
 

core/src/main/scala/stainless/genc/CFileOutputPhase.scala

@@ -7,16 +7,16 @@ import java.io.File
 import java.io.FileWriter
 import java.io.BufferedWriter
 
-object CFileOutputPhase extends UnitPhase[CAST.Prog] {
+trait CFileOutputPhase extends UnitPhase[CAST.Prog] {
 
   val name = "C File Output"
   val description = "Output converted C program to the specified file (default leon.c)"
 
-  def apply(ctx: inox.Context, program: CAST.Prog) {
-    val timer = ctx.timers.genc.print.start()
+  def apply(program: CAST.Prog) {
+    val timer = context.timers.genc.print.start()
 
     // Get the output file name from command line options, or use default
-    val cFileName = ctx.options.findOptionOrDefault(optOutputFile)
+    val cFileName = context.options.findOptionOrDefault(optOutputFile)
     val cOutputFile = new File(cFileName)
     val hFileName = cFileName.stripSuffix(".c") + ".h"
     val hOutputFile = new File(hFileName)
@@ -27,15 +27,15 @@ object CFileOutputPhase extends UnitPhase[CAST.Prog] {
         parent.mkdirs()
       }
     } catch {
-      case _ : java.io.IOException => ctx.reporter.fatalError("Could not create directory " + parent)
+      case _ : java.io.IOException => context.reporter.fatalError("Could not create directory " + parent)
     }
 
     // Output C code to the file
     try {
       val cout = new BufferedWriter(new FileWriter(cOutputFile))
       val hout = new BufferedWriter(new FileWriter(hOutputFile))
 
-      val headerDependencies = CASTDependencies.headerDependencies(program)(ctx)
+      val headerDependencies = CASTDependencies.headerDependencies(program)(context)
 
       val ph = new CPrinter(hFileName, false, headerDependencies)
       ph.print(program)
@@ -47,12 +47,18 @@ object CFileOutputPhase extends UnitPhase[CAST.Prog] {
       cout.write(pc.sb.toString)
       cout.close()
 
-      ctx.reporter.info(s"Output written to $hOutputFile and $cOutputFile")
+      context.reporter.info(s"Output written to $hOutputFile and $cOutputFile")
     } catch {
-      case _ : java.io.IOException => ctx.reporter.fatalError("Could not write C ouptut on " + cOutputFile)
+      case _ : java.io.IOException => context.reporter.fatalError("Could not write C ouptut on " + cOutputFile)
     }
 
     timer.stop()
   }
 
 }
+
+object CFileOutputPhase {
+  def apply(implicit ctx: inox.Context): LeonPipeline[CAST.Prog, CAST.Prog] = new {
+    val context = ctx
+  } with CFileOutputPhase
+}

core/src/main/scala/stainless/genc/CPrinter.scala

@@ -260,6 +260,7 @@ class CPrinter(
     case StaticStorage(_) => c"static "
 
     case TypeId(FunType(ret, params), id) => c"$ret (*$id)($params)"
+    case TypeId(FixedArrayType(base, length), id) => c"$base $id[$length]"
     case TypeId(typ, id) => c"$typ $id"
 
     case FunSign(Fun(id, FunType(retret, retparamTypes), params, _, _)) =>

core/src/main/scala/stainless/genc/GenCComponent.scala

@@ -9,7 +9,6 @@ import utils.{CheckFilter, DefinitionIdFinder, DependenciesFinder}
 import extraction.xlang.{trees => xt}
 import extraction.throwing.{trees => tt}
 import extraction._
-// import inox.evaluators.EvaluationResults.{ EvaluatorError, RuntimeError, Successful }
 
 import stainless.utils.JsonConvertions._
 
@@ -18,7 +17,6 @@ import io.circe.syntax._
 import io.circe.generic.semiauto._
 
 import scala.concurrent.Future
-// import scala.util.{ Success, Failure }
 
 import scala.language.existentials
 
@@ -86,7 +84,7 @@ class GenCRun(override val pipeline: extraction.StainlessPipeline) // pipeline i
 
     val symbolsAfterPipeline: tt.Symbols = pipelineBegin.extract(filtered)
 
-    GenerateCPhase.run(context, symbolsAfterPipeline)
+    GenerateC.run(symbolsAfterPipeline)
 
     val p = inox.Program(trees)(filtered)
 

core/src/main/scala/stainless/genc/GenerateC.scala

@@ -0,0 +1,25 @@
+/* Copyright 2009-2021 EPFL, Lausanne */
+
+package stainless
+package genc
+
+import extraction.throwing.trees._
+
+import phases._
+
+object GenerateC {
+
+  def pipeline(implicit ctx: inox.Context) =
+    NamedLeonPhase("ComputeDependencies", ComputeDependenciesPhase(ctx)) andThen
+    NamedLeonPhase("ComputeFunCtxPhase", LeonPipeline.both(NoopPhase[Dependencies], ComputeFunCtxPhase(ctx))) andThen
+    NamedLeonPhase("Scala2IRPhase", Scala2IRPhase(ctx)) andThen
+    NamedLeonPhase("NormalisationPhase", NormalisationPhase(ctx)) andThen
+    NamedLeonPhase("LiftingPhase", LiftingPhase(ctx)) andThen
+    NamedLeonPhase("ReferencingPhase", ReferencingPhase(ctx)) andThen
+    NamedLeonPhase("StructInliningPhase", StructInliningPhase(ctx)) andThen
+    NamedLeonPhase("IR2CPhase", IR2CPhase(ctx)) andThen
+    CFileOutputPhase(ctx)
+
+  def run(symbols: Symbols)(implicit ctx: inox.Context) = pipeline.run(symbols)
+
+}

core/src/main/scala/stainless/genc/LeonPhase.scala

@@ -2,46 +2,67 @@
 
 package stainless.genc
 
+import stainless.extraction.utils._
+
 trait NamedLeonPhase[F, T] extends LeonPipeline[F, T] {
   val underlying: LeonPipeline[F, T]
   val name: String
 
-  private implicit val debugSection = DebugSectionGenC
+  lazy val phases = context.options.findOption(optDebugPhases).map(_.toSet)
+
+  lazy val debugTrees: Boolean =
+    (phases.isEmpty || phases.exists(_.contains(name))) &&
+    context.reporter.debugSections.contains(DebugSectionTrees)
 
-  override def run(ctx: inox.Context, p: F): T = {
-    ctx.reporter.debug("\n" * 2)
-    ctx.reporter.debug("=" * 100)
-    ctx.reporter.debug(s"Running phase $name on")
-    ctx.reporter.debug(p)
-    val res = ctx.timers.genc.get(name).run {
-      underlying.run(ctx, p)
+  private implicit val debugSection = DebugSectionTrees
+
+  override def run(p: F): T = {
+    if (debugTrees) {
+      context.reporter.debug("\n" * 2)
+      context.reporter.debug("=" * 100)
+      context.reporter.debug(s"Running phase $name on:\n")
+      context.reporter.debug(p)
+    }
+    val res = context.timers.genc.get(name).run {
+      underlying.run(p)
+    }
+    if (debugTrees) {
+      context.reporter.debug("\n")
+      context.reporter.debug("-" * 100)
+      context.reporter.debug(s"Finished running phase $name:\n")
+      context.reporter.debug(res)
+      context.reporter.debug("=" * 100)
+      context.reporter.debug("\n" * 4)
     }
-    ctx.reporter.debug(s"Finished running phase $name")
-    ctx.reporter.debug(res)
-    ctx.reporter.debug("=" * 100)
-    ctx.reporter.debug("\n" * 4)
     res
   }
 }
 
 object NamedLeonPhase {
 
-  def apply[F, T](s: String, pipeline: LeonPipeline[F, T]): LeonPipeline[F, T] {
+  def apply[F, T](s: String, pipeline: LeonPipeline[F, T])(implicit ctx: inox.Context): LeonPipeline[F, T] {
   } = new {
     override val underlying: pipeline.type = pipeline
     override val name: String = s
+    override val context = ctx
   } with NamedLeonPhase[F, T]
 }
 
-abstract class UnitPhase[T] extends LeonPipeline[T, T] {
-  def apply(ctx: inox.Context, p: T): Unit
+trait UnitPhase[T] extends LeonPipeline[T, T] {
+  def apply(p: T): Unit
 
-  override def run(ctx: inox.Context, p: T) = {
-    apply(ctx, p)
+  override def run(p: T) = {
+    apply(p)
     p
   }
 }
 
-case class NoopPhase[T]() extends LeonPipeline[T, T] {
-  override def run(ctx: inox.Context, v: T) = v
+object NoopPhase {
+  def apply[T](implicit ctx: inox.Context): LeonPipeline[T, T] = {
+    new {
+      override val context = ctx
+    } with LeonPipeline[T, T] {
+      override def run(v: T) = v
+    }
+  }
 }

core/src/main/scala/stainless/genc/LeonPipeline.scala

@@ -3,26 +3,30 @@
 package stainless
 package genc
 
-abstract class LeonPipeline[F, T] {
-  self =>
+abstract class LeonPipeline[F, T] { self =>
 
-  def andThen[G](thenn: LeonPipeline[T, G]): LeonPipeline[F, G] = new LeonPipeline[F,G] {
-    def run(ctx: inox.Context, v: F): G = {
-      // if(ctx.findOptionOrDefault(GlobalOptions.optStrictPhases)) ctx.reporter.terminateIfError()
-      thenn.run(ctx, self.run(ctx, v))
+  val context: inox.Context
+
+  def andThen[G](thenn: LeonPipeline[T, G]): LeonPipeline[F, G] = new {
+    val context = self.context
+  } with LeonPipeline[F,G] {
+    def run(v: F): G = {
+      thenn.run(self.run(v))
     }
   }
 
-  def run(ctx: inox.Context, v: F): T
+  def run(v: F): T
 }
 
 object LeonPipeline {
 
-  def both[T, R1, R2](f1: LeonPipeline[T, R1], f2: LeonPipeline[T, R2]): LeonPipeline[T, (R1, R2)] = new LeonPipeline[T, (R1, R2)] {
-    def run(ctx: inox.Context, t: T): (R1, R2) = {
-      val r1 = f1.run(ctx, t)
+  def both[T, R1, R2](f1: LeonPipeline[T, R1], f2: LeonPipeline[T, R2])(implicit ctx: inox.Context): LeonPipeline[T, (R1, R2)] = new {
+    val context = ctx
+  } with LeonPipeline[T, (R1, R2)] {
+    def run(t: T): (R1, R2) = {
+      val r1 = f1.run(t)
       // don't check for SharedOptions.optStrictPhases because f2 does not depend on the result of f1
-      val r2 = f2.run(ctx, t)
+      val r2 = f2.run(t)
       (r1, r2)
     }
   }

core/src/main/scala/stainless/genc/ir/ClassLifter.scala

@@ -61,7 +61,7 @@ final class ClassLifter(val ctx: inox.Context) extends Transformer(NIR, LIR) {
         case ct @ to.ClassType(c) if c.hierarchyTop != c =>
           valFieldsToRegister += (vd.id -> ct)
 
-        case to.ArrayType(ct @ to.ClassType(c)) if c.hierarchyTop != c =>
+        case to.ArrayType(ct @ to.ClassType(c), _) if c.hierarchyTop != c =>
           arrayFieldsToRegister += (vd.id -> ct)
 
         case _ => ()
@@ -112,7 +112,7 @@ final class ClassLifter(val ctx: inox.Context) extends Transformer(NIR, LIR) {
 
   override def rec(typ: Type)(implicit lift: Env): to.Type = typ match {
     case ClassType(clazz) if lift => to.ClassType(rec(clazz.hierarchyTop))
-    case ArrayType(ArrayType(ClassType(_))) =>
+    case ArrayType(ArrayType(ClassType(_), _), _) =>
       ctx.reporter.fatalError("Multidimentional arrays of objects are not yet supported")
     case typ => super.rec(typ)
   }
@@ -200,7 +200,7 @@ final class ClassLifter(val ctx: inox.Context) extends Transformer(NIR, LIR) {
       case ct @ to.ClassType(c) if c.hierarchyTop != c =>
         valDB += vd0 -> (vd, ct)
 
-      case to.ArrayType(ct @ to.ClassType(c)) if c.hierarchyTop != c =>
+      case to.ArrayType(ct @ to.ClassType(c), _) if c.hierarchyTop != c =>
         arrayDB += vd0 -> (vd, ct)
 
       case _ => ()