Reorganize GenC annotations

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

@@ -44,7 +44,7 @@ object CAST { // C Abstract Syntax Tree
   case class Prog(
     includes: Set[Include],
     // boolean is set to true when for global declarations that are declared outside of the Stainless program
-    decls: Seq[(Decl, Boolean)],
+    decls: Seq[(Decl, DeclarationMode)],
     typeDefs: Set[TypeDef],
     enums: Set[Enum],
     types: Seq[DataType], // Both structs and unions, order IS important! See NOTE above.

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

@@ -61,7 +61,11 @@ class CPrinter(
               sep = "\n\n")
              }
             |${nary(
-              decls.filter(!_._2).map(_._1),
+              decls.filter(_._2 != External).map {
+                case (decl, Static) => StaticStorage(decl)
+                case (decl, Normal) => decl
+                case _ => sys.error("unreachable code")
+              },
               opening = separator("global variables"),
               closing = ";\n\n",
               sep = ";\n")
@@ -269,8 +273,7 @@ class CPrinter(
   }
 
   private[genc] def pp(wt: WrapperTree)(implicit pctx: PrinterContext): Unit = wt match {
-    case StaticStorage(id) if id.name == "main" => /* Nothing */
-    case StaticStorage(_) => c"static "
+    case StaticStorage(decl) => c"static $decl"
 
     case TypeId(FunType(ret, params), id) => c"$ret (*$id)($params)"
     case TypeId(FixedArrayType(base, length), id) => c"$base $id[$length]"
@@ -316,7 +319,7 @@ class CPrinter(
 
   /** Wrappers to distinguish how the data should be printed **/
   private[genc] sealed abstract class WrapperTree
-  private case class StaticStorage(id: Id) extends WrapperTree
+  private case class StaticStorage(decl: Decl) extends WrapperTree
   private case class TypeId(typ: Type, id: Id) extends WrapperTree
   private case class FunSign(f: Fun) extends WrapperTree
 

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

@@ -81,7 +81,7 @@ class GenCRun(override val pipeline: extraction.StainlessPipeline) // pipeline i
       override val results = ids.flatMap { id =>
         val fd = symbols.getFunction(id)
         val pos = fd.getPos.toString
-        if (fd.flags.exists(_.name == "export"))
+        if (fd.flags.exists(_.name == "cCode.export"))
           Some(GenCRun.Result(fd, Compiled, 0))
         else
           None

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

@@ -40,8 +40,7 @@ private[genc] sealed trait IR { ir =>
   sealed abstract class Def extends Tree
 
   case class Prog(
-    // boolean is set to true when for global declarations that are declared outside of the Stainless program
-    decls: Seq[(Decl, Boolean)],
+    decls: Seq[(Decl, DeclarationMode)],
     functions: Seq[FunDef],
     classes: Seq[ClassDef]
   ) {

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

@@ -53,7 +53,7 @@ final class IRPrinter[S <: IR](val ir: S) {
     val post = ptx.newLine + "}"
 
     (if (fd.isPure) "@pure\n" else "") +
-    (if (fd.isExported) "@export\n" else "") +
+    (if (fd.isExported) "@cCode.export\n" else "") +
     pre + body + post
   }
 

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

@@ -21,4 +21,10 @@ package object genc {
 
   // FIXME: see leon definition
   def pathFromRoot(df: Definition)(implicit syms: Symbols): List[Definition] = List(df)
+
+  // declaration mode for global variables
+  sealed abstract class DeclarationMode
+  case object Normal extends DeclarationMode
+  case object Static extends DeclarationMode // static annotation
+  case object External extends DeclarationMode // no declaration in the produced code
 }

core/src/main/scala/stainless/genc/phases/ComputeDependenciesPhase.scala

@@ -16,8 +16,8 @@ import ExtraOps._
 import collection.mutable.{Set => MutableSet}
 
 /*
- * Compute the dependencies of the @export functions
- * Generic functions cannot be marked @export (only specialized versions that are
+ * Compute the dependencies of the @cCode.export functions
+ * Generic functions cannot be marked @cCode.export (only specialized versions that are
  * used by exported functions are exported to C).
  *
  * Moreover, the list of dependencies only contains top level functions. For nested
@@ -26,11 +26,6 @@ import collection.mutable.{Set => MutableSet}
  * some type T, then T (and all its class hierarchy if T is a class) will be included
  * in the dependency set.
  *
- * This phase also make sures @cCode.drop functions are not used. The same is *NOT*
- * done for dropped types as they might still be present in function signature. They
- * should be removed in a later (transformation) phase. Additionally, this phase
- * ensures that the annotation set on class and function is sane.
- *
  * NOTE We cannot rely on purescala.DependencyFinder as it will traverse functions
  *     annotated with @cCode.function and we don't want that. The same applies for
  *     classes annotated with @cCode.typdef. We therefore implement a simpler version

core/src/main/scala/stainless/genc/phases/ExtraOps.scala

@@ -48,7 +48,7 @@ private[genc] object ExtraOps {
 
     def isExtern          = fd.flags contains Extern
     def isDropped         = hasAnnotation("cCode.drop") || fd.flags.contains(Ghost)
-    def isExported        = hasAnnotation("export")
+    def isExported        = hasAnnotation("cCode.export")
     def isManuallyDefined = hasAnnotation(manualDefAnnotation)
 
     def extAnnotations: Map[String, Seq[Any]] = fd.flags.collect {
@@ -77,7 +77,7 @@ private[genc] object ExtraOps {
   implicit class ClassDefOps(val cd: ClassDef) {
     def isManuallyTyped = hasAnnotation(manualTypeAnnotation)
     def isDropped       = hasAnnotation(droppedAnnotation)
-    def isExported      = hasAnnotation("export")
+    def isExported      = hasAnnotation("cCode.export")
     def isGlobal        = cd.flags.exists(_.name.startsWith("cCode.global"))
     def isGlobalDefault = cd.flags.exists(_.name == "cCode.global")
     def isGlobalUninitialized = cd.flags.exists(_.name == "cCode.globalUninitialized")

core/src/main/scala/stainless/genc/phases/Scala2IRPhase.scala

@@ -107,7 +107,7 @@ private class S2IRImpl(val context: inox.Context, val ctxDB: FunCtxDB, val deps:
   def run(): Unit = {
     checkGlobalUsage()
 
-    // Start the transformation from `@exported` (and `@cCode.global`) functions and classes
+    // Start the transformation from `@cCode.export` (and `@cCode.global`) functions and classes
     for (df <- deps.deps) {
       df match {
         case fd: FunDef if fd.isExported =>
@@ -123,7 +123,7 @@ private class S2IRImpl(val context: inox.Context, val ctxDB: FunCtxDB, val deps:
    *                                                       Caches                                     *
    ****************************************************************************************************/
 
-  var declResults = new scala.collection.mutable.ListBuffer[(CIR.Decl, Boolean)]()
+  var declResults = new scala.collection.mutable.ListBuffer[(CIR.Decl, DeclarationMode)]()
 
   // For functions, we associate each TypedFunDef to a CIR.FunDef for each "type context" (TypeMapping).
   // This is very important for (non-generic) functions nested in a generic function because for N
@@ -643,18 +643,20 @@ private class S2IRImpl(val context: inox.Context, val ctxDB: FunCtxDB, val deps:
               s"We found ${paramInits.length} initializations instead of ${fields.length}."
             )
           }
-          for ((field, paramInit) <- fields.zip(paramInits)) {
+          for (((field, paramInit), static) <- fields.zip(paramInits).zip(nonGhostFields.map(vd => vd.flags.exists(_.name == "cCode.static")))) {
             implicit val emptyEnv = Env(Map(), Map(), false)
-            val decl = (CIR.Decl(field, Some(rec(paramInit.fullBody))), false)
+            val decl = (CIR.Decl(field, Some(rec(paramInit.fullBody))), if (static) Static else Normal)
             if (declResults.map(_._1.vd).contains(field)) {
               reporter.fatalError(cd.getPos, s"Global variable ${field.id} is defined twice")
             }
             declResults.append(decl)
           }
         } else if (cd.isGlobalUninitialized) {
-          for (field <- fields) declResults.append((CIR.Decl(field, None), false))
+          for ((field, static) <- fields.zip(nonGhostFields.map(vd => vd.flags.exists(_.name == "cCode.static")))) {
+            declResults.append((CIR.Decl(field, None), if (static) Static else Normal))
+          }
         } else if (cd.isGlobalExternal) {
-          for (field <- fields) declResults.append((CIR.Decl(field, None), true))
+          for (field <- fields) declResults.append((CIR.Decl(field, None), External))
         }
         newAcc
       } else {

core/src/sphinx/genc.rst

@@ -135,7 +135,7 @@ See below for a case class with a fixed length array and its transformation in C
   val CONSTANT2: UInt16 = 12
   val CONSTANT3: UInt16 = CONSTANT1 + CONSTANT2
 
-  @export
+  @cCode.export
   case class W(x: Int, a: Array[Int], y: Int) {
     require(
       a.length == CONSTANT3.toInt &&
@@ -340,7 +340,7 @@ make sure that the instance is created using the default values:
 
 .. code-block:: scala
 
-  @export
+  @cCode.export
   def main() {
     implicit val gs = GlobalState()
     StdOut.print(gs.x)

frontends/benchmarks/genc/ArgumentsEffects.scala

@@ -12,7 +12,7 @@ object ArgumentsEffects {
     StdOut.println(x3)
   }
 
-  @export
+  @cCode.export
   def main(): Unit = {
     var x = 0
 

frontends/benchmarks/genc/FixedArray.scala

@@ -8,7 +8,7 @@ object FixedArray {
   val CONSTANT2: UInt16 = 3
   val CONSTANT3: UInt16 = CONSTANT1 + CONSTANT2
 
-  @export
+  @cCode.export
   case class W(x: Int, a: Array[Int], y: Int) {
     require(
       a.length == CONSTANT3.toInt &&
@@ -17,7 +17,7 @@ object FixedArray {
     )
   }
 
-  @export
+  @cCode.export
   def f(w: W): Int = {
     require(0 <= w.a(0) && w.a(0) <= 1000)
     require(0 <= w.a(1) && w.a(1) <= 1000)
@@ -30,15 +30,15 @@ object FixedArray {
     w.a(0) + w.a(1) + w.a(2) + w.a(3) + w.a(4) + w.x + w.y
   }
 
-  @export
+  @cCode.export
   def g(a: Array[Int]): Unit = {
     require(a.length > 0)
     require(0 <= a(0) && a(0) <= 1000)
 
     a(0) += 1
   }
 
-  @export
+  @cCode.export
   def main(): Unit = {
     val w = W(30, Array(10, 20, 30, 20, 42), 100)
     val w2 = W(30, Array(10, 20, 30, 20, 42), { w.a(0) += 1; 100 })

frontends/benchmarks/genc/Global.scala

@@ -31,7 +31,7 @@ object Global {
     if (state.y > 0) move()
   }.ensuring(_ => state.stable)
 
-  @export
+  @cCode.export
   def main() {
     implicit val gs = GlobalState()
     StdOut.print(gs.x)

frontends/benchmarks/genc/GlobalUninitialized.scala

@@ -31,7 +31,7 @@ object GlobalUninitialized {
     if (state.y > 0) move()
   }.ensuring(_ => state.stable)
 
-  @export
+  @cCode.export
   def main() {
     implicit val gs = GlobalState(Array.fill(100)(0), false, 0, 0)
     gs.x = 8

frontends/benchmarks/genc/ImageProcessing.scala

@@ -676,7 +676,7 @@ object ImageProcessing {
     else StdOut.println("false")
   }
 
-  @export
+  @cCode.export
   def main(): Int = {
     implicit val state = stainless.io.newState
     val input  = FIS.open("input.bmp")

frontends/benchmarks/genc/LZWa.scala

@@ -638,7 +638,7 @@ object LZWa {
     case _ => false
   }
 
-  @export
+  @cCode.export
   def main() = {
     implicit val state = stainless.io.newState
 

frontends/benchmarks/genc/LZWb.scala

@@ -715,7 +715,7 @@ object LZWb {
     case _ => false
   }
 
-  @export
+  @cCode.export
   def main() = {
     implicit val state = stainless.io.newState
 

frontends/benchmarks/genc/Nested.scala

@@ -4,7 +4,7 @@ import stainless.io._
 
 object Nested {
 
-  @export
+  @cCode.export
   def main(): Int = {
     f(100)
   }

frontends/benchmarks/genc/Normalisation.scala

@@ -14,7 +14,7 @@ object Normalisation {
   }
   case class B(a1: A, i: UInt8, j: UInt32, a2: A)
 
-  @export
+  @cCode.export
   def main(): Unit = {
     val a = A(100, 9, 200)
     val x = a.sum + a.sum

frontends/benchmarks/genc/Pointer.scala

@@ -10,7 +10,7 @@ object Pointer {
     r2.x = 250
   }
 
-  @export
+  @cCode.export
   def main(): Unit = {
     val r = Pointer(100)
     val r2 = Pointer(100)

frontends/benchmarks/genc/Return.scala

@@ -22,7 +22,7 @@ object Return {
     else StdOut.println("ERROR")
   }
 
-  @export
+  @cCode.export
   def main() = {
     verify(return10 == 10)
     verify(findIndex(Array(0,100,200,250), 0) == 0)

frontends/benchmarks/genc/StateTest.scala

@@ -3,7 +3,7 @@ import stainless.lang._
 
 object StateTest {
 
-  @export
+  @cCode.export
   def main(): Int = {
     implicit val state = stainless.io.newState
     f()

frontends/benchmarks/genc/TwoOptions.scala

@@ -5,15 +5,15 @@ import stainless.annotation._
 
 object TwoOptions {
 
-  @export
+  @cCode.export
   def twoOptions: Unit = {
     var opt1: Option[Long] = None()
     val opt2: Option[Int] = None()
     opt1.isEmpty
     opt2.isEmpty
   }
 
-  @export
+  @cCode.export
   def main() = {
   }
 

frontends/benchmarks/genc/Unsigned.scala

@@ -5,7 +5,7 @@ import stainless.io._
 
 object Unsigned {
 
-  @export
+  @cCode.export
   def main(): Unit = {
     val a = fa(16, 84)
     val b = fb(84, 14)

frontends/benchmarks/genc/WhileInLet.scala

@@ -2,7 +2,7 @@ import stainless.annotation._
 
 object WhileInLet {
 
-  @export
+  @cCode.export
   def main(): Unit = {
     val noLoop = while (false) {}
     ()

frontends/benchmarks/imperative/valid/LetTargets.scala

@@ -8,7 +8,7 @@ object LetTargets {
   case class C(bs: Array[B])
   case class D(val c: C)
 
-  @export
+  @cCode.export
   def reset(d: D): Unit = {
     require(d.c.bs.length > 0)
     require(d.c.bs(0).as.length > 0)

frontends/library/stainless/annotation/annotations.scala

@@ -95,10 +95,6 @@ class erasable extends Annotation
 @ignore
 class indexedAt(n: BigInt) extends Annotation
 
-/** Export function to C for GenC translation */
-@ignore
-class export extends Annotation
-
 @ignore
 class refEq extends Annotation