Fixes for fixed arrays in GenC

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

@@ -91,8 +91,7 @@ final class Normaliser(val ctx: inox.Context) extends Transformer(CIR, NIR) with
     case Construct(cd0, args0) =>
       val cd = rec(cd0)
       val (preArgs, args) = flattenArgs(allowTopLevelApp = true, args0.zip(cd0.fields).map {
-        case (e, vd) if vd.typ.isFixedArray => (e, true)
-        case (e, _) => (e, false)
+        case (e, vd) => (e, vd.typ.isFixedArray)
       })
       val ctor = to.Construct(cd, args)
 
@@ -360,19 +359,21 @@ final class Normaliser(val ctx: inox.Context) extends Transformer(CIR, NIR) with
     case value => (pre, value)
   }
 
+  // FIXME: Not sure what this is for?
   // Strict normalisation: create a normalisation variable to save the result of an argument if it could be modified
   // by an init segment (from any argument) extracted during regular normalisation.
   private def strictNormalisation(value: to.Expr, inits: Seq[to.Expr]*): (Option[to.DeclInit], to.Expr) = {
-    if (inits exists { _.nonEmpty }) {
-      // We need to store the result in a temporary variable.
+    if (inits.forall(_.isEmpty) || isSimple(value, allowTopLevelApp = true, allowArray = true)) {
+      // No init segment, so we can safely use the given value as is
+      // Same when value is simple
+      (None, value)
+    } else {
+      // We store the result in a temporary variable.
       val norm = freshNormVal(value.getType, isVar = false)
       val binding = to.Binding(norm)
       val declinit = to.DeclInit(norm, value)
 
       (Some(declinit), binding)
-    } else {
-      // No init segment, so we can safely use the given value as is.
-      (None, value)
     }
   }
 

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

@@ -200,15 +200,32 @@ private class IR2CImpl(val ctx: inox.Context) {
 
     case ArrayInit(alloc) => ctx.reporter.fatalError("This should be part of a DeclInit expression!")
 
-    case FieldAccess(obj, fieldId) => C.FieldAccess(rec(obj), rec(fieldId))
-
     // no `data` field for fixed arrays
     case ArrayAccess(FieldAccess(obj, fieldId), index)
       if  obj.getType.isInstanceOf[ClassType] &&
           obj.getType.asInstanceOf[ClassType].clazz.fields.exists(vd =>
             vd.id == fieldId && vd.typ.isFixedArray
           ) =>
-        C.ArrayAccess(C.FieldAccess(rec(obj), rec(fieldId)), rec(index))
+
+      C.ArrayAccess(C.FieldAccess(rec(obj), rec(fieldId)), rec(index))
+
+    // but field accesses of fixed arrays not followed by an array access
+    // must be wrapped in an array wrapper struct (see FixedArray.scala example)
+    case FieldAccess(obj, fieldId)
+      if  obj.getType.isInstanceOf[ClassType] &&
+          obj.getType.asInstanceOf[ClassType].clazz.fields.exists(vd =>
+            vd.id == fieldId && vd.typ.isFixedArray
+          ) =>
+
+      val vd = obj.getType.asInstanceOf[ClassType].clazz.fields.find(vd =>
+        vd.id == fieldId && vd.typ.isFixedArray
+      ).get
+      val arrayType = vd.typ.asInstanceOf[ArrayType]
+      val length = arrayType.length.get
+      val array = array2Struct(arrayType.copy(length = None))
+      C.StructInit(array, C.FieldAccess(rec(obj), rec(fieldId)) :: C.Lit(Int32Lit(length)) :: Nil)
+
+    case FieldAccess(obj, fieldId) => C.FieldAccess(rec(obj), rec(fieldId))
 
     case ArrayAccess(array, index) => C.ArrayAccess(C.FieldAccess(rec(array), C.Id("data")), rec(index))
     case ArrayLength(array) => C.FieldAccess(rec(array), C.Id("length"))

frontends/benchmarks/genc/FixedArray.scala

@@ -30,19 +30,24 @@ object FixedArray {
     w.a(0) + w.a(1) + w.a(2) + w.a(3) + w.a(4) + w.x + w.y
   }
 
-  // @export
-  // def g(a: Array[Int]): Unit = {
-  //   require(a.length > 0)
-  //   require(0 <= a(0) && a(0) <= 1000)
+  @export
+  def g(a: Array[Int]): Unit = {
+    require(a.length > 0)
+    require(0 <= a(0) && a(0) <= 1000)
 
-  //   a(0) += 1
-  // }
+    a(0) += 1
+  }
 
   @export
   def main(): Unit = {
     val w = W(30, Array(10, 20, 30, 20, 42), 100)
-    // g(w.a)
-    StdOut.println(f(w))
+    val w2 = W(30, Array(10, 20, 30, 20, 42), { w.a(0) += 1; 100 })
+    g(w.a)
+    val a2 = w.a
+    g(a2)
+    val z = f(w)
+    assert(z == 30 + 155 + 20 + 30 + 20 + 42 + 100)
+    StdOut.println(z)
   }
 
-}
+}

frontends/benchmarks/genc/LZWb.scala

@@ -418,9 +418,7 @@ object LZWb {
     val capacity = pteps.length
     require(
       capacity == DictionarySize &&
-      // FIXME: length is on right-hand-side to avoid finite array optimization
-      // see issue https://github.com/epfl-lara/stainless/issues/1056
-      DictionaryMemorySize == memory.length &&
+      memory.length == DictionaryMemorySize &&
       allInRange(pteps, 0, DictionaryMemorySize) &&
       0 <= nextIndex && nextIndex <= capacity
     )

frontends/benchmarks/genc/WhileInLet.scala

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