Encodes the length of a pointer to an array as the array type's length

In Go, the length of a pointer to an array is the length constant of
the array type; this holds even for a nil pointer. Previously, the
length was encoded by dereferencing the pointer, which made it
unprovable for pointers that are not known to be non-nil.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Author: ArquintL

src/main/scala/viper/gobra/translator/encodings/arrays/ArrayEncoding.scala

@@ -18,7 +18,7 @@ import viper.gobra.translator.context.Context
 import viper.gobra.translator.library.embeddings.EmbeddingParameter
 import viper.gobra.translator.util.FunctionGenerator
 import viper.gobra.translator.util.ViperUtil.synthesized
-import viper.gobra.translator.util.ViperWriter.CodeWriter
+import viper.gobra.translator.util.ViperWriter.{CodeLevel, CodeWriter}
 import viper.gobra.util.Violation
 import viper.silver.plugin.standard.termination
 import viper.silver.{ast => vpr}
@@ -181,11 +181,11 @@ class ArrayEncoding extends TypeEncoding with SharedArrayEmbedding {
         case Shared => ctx.reference(e.asInstanceOf[in.Location]).map(sh.length(_, cptParam(len, t)(ctx))(n)(ctx))
       }
 
-    case in.Length(exp :: ctx.*(t: in.ArrayT)) =>
-      val expInfo = exp.info
-      val derefExp = in.Deref(exp, in.PointerT(t, t.addressability))(expInfo)
-      val newLenExpr = in.Length(derefExp)(expInfo)
-      expression(ctx)(newLenExpr)
+    case n@in.Length(_ :: ctx.*(t: in.ArrayT)) =>
+      // In Go, the length of a pointer to an array is the array type's length; this holds even
+      // for a nil pointer and, thus, neither requires a dereference nor a nil check:
+      val (pos, info, errT) = n.vprMeta
+      CodeLevel.unit(vpr.IntLit(t.length)(pos, info, errT))
 
     case n@in.Capacity(e :: ctx.Array(len, t) / m) =>
       m match {

src/test/resources/regressions/issues/000491-4.gobra

@@ -186,3 +186,10 @@ func quantifierWithAddrTriggerInCode(s []byte) {
 func lengthOfNestedArray(a *[4][8]byte, idx int) int {
 	return len(a[idx])
 }
+
+// The length of a *[N]byte is the constant N; in Go, this holds even for a nil
+// pointer and, thus, must not generate a nil-ness proof obligation.
+func lenOfNilArrayPointer() {
+	var p *[8]byte = nil
+	assert len(p) == 8
+}