Merge branch 'develop-error-message-empty-array-struct'. Close #695.

**Description**

Copilot allows defining empty arrays (i.e., values of type `Array 0`)
and empty structs (i.e., structs with no fields), but using empty arrays
or structs in C99 is undefined behavior. Moreover, `copilot-c99` will
often crash if you attempt to compile a Copilot specification that uses
an empty array or struct.

**Type**

* Bug: Copilot crashes or generates incorrect code.

**Additional context**

None.

**Requester**

* Ryan Scott (Galois)

**Method to check presence of bug**

The following Copilot specification contains an empty array:

```hs
-- EmptyArray.hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NoImplicitPrelude #-}
module Main (main) where

import Language.Copilot
import Copilot.Compile.C99 (compile)

arrs :: Stream (Array 0 Bool)
arrs = constant (array [])

spec :: Spec
spec = trigger "trig" true [arg arrs]

main :: IO ()
main = do
  spec' <- reify spec
  compile "empty_array" spec'
```

And the following Copilot specification contains an empty struct:

```hs
-- EmptyStruct.hs
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE NoImplicitPrelude #-}
module Main (main) where

import GHC.Generics (Generic)

import Language.Copilot
import Copilot.Compile.C99 (compile)

data Empty = Empty deriving Generic

instance Struct Empty where
  typeName = typeNameDefault
  toValues = toValuesDefault
  updateField = updateFieldDefault

instance Typed Empty where
  typeOf = typeOfDefault

structs :: Stream Empty
structs = constant Empty

spec :: Spec
spec = trigger "trig" true [arg structs]

main :: IO ()
main = do
  spec' <- reify spec
  compile "empty_struct" spec'
```

Compiling either program will cause `copilot-c99` to crash:

```
$ runghc EmptyArray.hs
EmptyArray.hs: NonEmpty.fromList: empty list
CallStack (from HasCallStack):
  error, called at libraries/base/Data/List/NonEmpty.hs:200:15 in base:Data.List.NonEmpty
  fromList, called at src/Copilot/Compile/C99/Expr.hs:381:3 in copilot-c99-4.6-inplace:Copilot.Compile.C99.Expr

$ runghc EmptyStruct.hs
EmptyStruct.hs: NonEmpty.fromList: empty list
CallStack (from HasCallStack):
  error, called at libraries/base/Data/List/NonEmpty.hs:200:15 in base:Data.List.NonEmpty
  fromList, called at src/Copilot/Compile/C99/Expr.hs:375:19 in copilot-c99-4.6-inplace:Copilot.Compile.C99.Expr
```

Note that not all Copilot specifications which contain empty arrays or
structs will cause Copilot to crash outright. For instance, the
following program contains an empty array, but only in the type of an
extern:

```hs
-- EmptyArrayExtern.hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NoImplicitPrelude #-}
module Main (main) where

import Language.Copilot
import Copilot.Compile.C99 (compile)

arrs :: Stream (Array 0 Bool)
arrs = extern "arrs" Nothing

spec :: Spec
spec = trigger "trig" true [arg arrs]

main :: IO ()
main = do
  spec' <- reify spec
  compile "empty_array_extern" spec'
```

`copilot-c99` will compile this to C code, but using a C compiler such as `gcc` or `clang` will warn you that the resulting C code falls outside of C99 if you use the `-Wpedantic` flag:

```
$ clang -c empty_array_extern.c -o empty_array_extern.o -Wpedantic
In file included from empty_array_extern.c:8:
./empty_array_extern.h:1:18: warning: zero size arrays are an extension [-Wzero-length-array]
    1 | extern bool arrs[(0)];
      |                  ^~~
./empty_array_extern.h:2:26: warning: zero size arrays are an extension [-Wzero-length-array]
    2 | void trig(bool trig_arg0[(0)]);
      |                          ^~~
empty_array_extern.c:10:22: warning: zero size arrays are an extension [-Wzero-length-array]
   10 | static bool arrs_cpy[(0)];
      |                      ^~~
empty_array_extern.c:16:49: warning: zero size arrays are an extension [-Wzero-length-array]
   16 | static void trig_0_arg0(bool trig_0_arg0_output[(0)]) {
      |                                                 ^~~
empty_array_extern.c:21:25: warning: zero size arrays are an extension [-Wzero-length-array]
   21 |   bool trig_0_arg_temp0[(0)];
      |                         ^~~
5 warnings generated.
```

**Expected result**

A clear error message is raised either by the Copilot compiler or GCC
indicating that the code produced involving empty arrays or structs is
not valid.

The following Dockerfile checks that compiling an empty struct or array
raises fails during compilation, after which it prints the message
Success:
```
--- Dockerfile-verify-695
FROM ubuntu:focal

ENV DEBIAN_FRONTEND=noninteractive

SHELL ["/bin/bash", "-c"]

RUN apt-get update

RUN apt-get install --yes software-properties-common
RUN add-apt-repository ppa:hvr/ghc
RUN apt-get update

RUN apt-get install --yes ghc-8.6.5 cabal-install-2.4
RUN apt-get install --yes libz-dev git alex happy

ENV PATH=/opt/ghc/8.6.5/bin:/opt/cabal/2.4/bin:$PWD/.cabal-sandbox/bin:$PATH

RUN cabal update
RUN cabal v1-sandbox init

ADD EmptyArray.hs  /tmp/
ADD EmptyStruct.hs /tmp/

CMD git clone $REPO && cd $NAME && git checkout $COMMIT && cd .. \
  && cabal v1-install \
       $NAME/copilot \
       $NAME/copilot-c99 \
       $NAME/copilot-core \
       $NAME/copilot-interpreter \
       $NAME/copilot-language \
       $NAME/copilot-libraries \
       $NAME/copilot-prettyprinter \
       $NAME/copilot-theorem \
  && ! cabal v1-exec -- runhaskell /tmp/EmptyArray.hs \
  && ! cabal v1-exec -- runhaskell /tmp/EmptyStruct.hs \
  && echo "Success"

--- EmptyArray.hs
{-# LANGUAGE DataKinds         #-}
{-# LANGUAGE NoImplicitPrelude #-}
module Main (main) where

import Copilot.Compile.C99 (compile)
import Language.Copilot

main :: IO ()
main = do
  spec' <- reify spec
  compile "empty_array" spec'

spec :: Spec
spec = trigger "trig" true [arg arrs]

arrs :: Stream (Array 0 Bool)
arrs = constant (array [])

--- EmptyStruct.hs
{-# LANGUAGE DeriveGeneric     #-}
{-# LANGUAGE NoImplicitPrelude #-}
module Main (main) where

import GHC.Generics (Generic)

import Copilot.Compile.C99 (compile)
import Language.Copilot

main :: IO ()
main = do
  spec' <- reify spec
  compile "empty_struct" spec'

spec :: Spec
spec = trigger "trig" true [arg structs]

structs :: Stream Empty
structs = constant Empty

-- * Empty struct type

data Empty = Empty
  deriving Generic

instance Struct Empty where
  typeName    = typeNameDefault
  toValues    = toValuesDefault
  updateField = updateFieldDefault

instance Typed Empty where
  typeOf = typeOfDefault
```

Command (substitute variables based on new path after merge):
```
$ docker run -e "REPO=https://github.com/Copilot-Language/copilot" -e "NAME=copilot" -e "COMMIT=<HASH>" -it copilot-verify-695
```

**Solution implemented**

Modify `copilot-c99`'s `constStruct` and `constArray` to raise an error
if a struct or array passed as argument is empty.

Modify `copilot-c99`'s `transType` to raise an error if a struct or
array passed as argument is empty.

Add test cases to `copilot-c99` to ensure that Copilot specifications
with empty arrays or structs are rejected by the C99 backend.

**Further notes**

None.

Author: ivanperez-keera

copilot-c99/CHANGELOG

@@ -1,3 +1,6 @@
+2026-02-16
+        * Raise error when compiling empty arrays or structs. (#695)
+
 2026-01-07
         * Version bump (4.6.1). (#705)
 

copilot-c99/src/Copilot/Compile/C99/Error.hs

@@ -5,7 +5,10 @@
 --
 -- Custom functions to report error messages to users.
 module Copilot.Compile.C99.Error
-    ( impossible )
+    ( impossible
+    , errorEmptyStruct
+    , errorZeroLengthArray
+    )
   where
 
 -- | Report an error due to a bug in Copilot.
@@ -18,3 +21,17 @@ impossible function package =
     ++ ". Please file an issue at "
     ++ "https://github.com/Copilot-Language/copilot/issues"
     ++ " or email the maintainers at <ivan.perezdominguez@nasa.gov>"
+
+-- | Report an error when attempting to compile a zero-length array to C99.
+-- C99 does not support zero-length arrays, so Copilot cannot compile
+-- specifications that use them.
+errorZeroLengthArray :: a
+errorZeroLengthArray =
+  error "copilot-c99: Cannot compile zero-length arrays to C99.\n"
+
+-- | Report an error when attempting to compile an empty struct to C99.
+-- C99 does not support empty structs, so Copilot cannot compile
+-- specifications that use them.
+errorEmptyStruct :: a
+errorEmptyStruct =
+  error "copilot-c99: Cannot compile empty structs to C99.\n"

copilot-c99/src/Copilot/Compile/C99/Expr.hs

@@ -18,7 +18,7 @@ import Copilot.Core ( Array, Expr (..), Field (..), Op1 (..), Op2 (..),
                       arrayElems, toValues, typeLength, typeSize )
 
 -- Internal imports
-import Copilot.Compile.C99.Error ( impossible )
+import Copilot.Compile.C99.Error ( impossible, errorEmptyStruct, errorZeroLengthArray )
 import Copilot.Compile.C99.Name  ( exCpyName, streamAccessorName )
 import Copilot.Compile.C99.Type  ( transLocalVarDeclType, transType,
                                    transTypeName )
@@ -371,14 +371,23 @@ constFieldInit (Value ty (Field val)) = C.InitItem Nothing $ constInit ty val
 
 -- | Transform a Copilot Struct, based on the struct fields, into a list of C99
 -- initializer values.
+--
+-- Raises an error if the struct is empty, as C99 does not support structs with
+-- no fields.
 constStruct :: [Value a] -> NonEmpty.NonEmpty C.InitItem
-constStruct val = NonEmpty.fromList $ map constFieldInit val
+constStruct val = case val of
+  [] -> errorEmptyStruct
+  _  -> NonEmpty.fromList $ map constFieldInit val
 
 -- | Transform a Copilot Array, based on the element values and their type,
 -- into a list of C99 initializer values.
+--
+-- Raises an error if the array is empty, as C99 does not support zero-length
+-- arrays.
 constArray :: Type a -> [a] -> NonEmpty.NonEmpty C.InitItem
-constArray ty =
-  NonEmpty.fromList . map (C.InitItem Nothing . constInit ty)
+constArray ty xs = case xs of
+  [] -> errorZeroLengthArray
+  _  -> NonEmpty.fromList $ map (C.InitItem Nothing . constInit ty) xs
 
 -- | Explicitly cast a C99 value to a type.
 explicitTy :: Type a -> C.Expr -> C.Expr

copilot-c99/src/Copilot/Compile/C99/Type.hs

@@ -12,7 +12,9 @@ module Copilot.Compile.C99.Type
 import qualified Language.C99.Simple as C
 
 -- Internal imports: Copilot
-import Copilot.Core ( Type (..), typeLength, typeName )
+import Copilot.Core              ( Struct (..), Type (..), typeLength,
+                                   typeName )
+import Copilot.Compile.C99.Error ( errorEmptyStruct, errorZeroLengthArray )
 
 -- | Translate a Copilot type to a C99 type.
 transType :: Type a -> C.Type
@@ -28,10 +30,12 @@ transType ty = case ty of
   Word64    -> C.TypeSpec $ C.TypedefName "uint64_t"
   Float     -> C.TypeSpec C.Float
   Double    -> C.TypeSpec C.Double
-  Array ty' -> C.Array (transType ty') len
+  Array ty' | typeLength ty == 0 -> errorZeroLengthArray
+            | otherwise          -> C.Array (transType ty') len
     where
       len = Just $ C.LitInt $ fromIntegral $ typeLength ty
-  Struct s  -> C.TypeSpec $ C.Struct (typeName s)
+  Struct s  | null (toValues s) -> errorEmptyStruct
+            | otherwise         -> C.TypeSpec $ C.Struct (typeName s)
 
 -- | Translate a Copilot type to a valid (local) variable declaration C99 type.
 --

copilot-c99/tests/Test/Copilot/Compile/C99.hs

@@ -8,10 +8,11 @@ module Test.Copilot.Compile.C99
 
 -- External imports
 import Control.Arrow                        ((&&&))
-import Control.Exception                    (IOException, catch)
-import Control.Monad                        (when)
+import Control.Exception                    (ErrorCall (..), IOException, catch,
+                                             try)
+import Control.Monad                        (unless, when)
 import Data.Bits                            (Bits, complement)
-import Data.List                            (intercalate)
+import Data.List                            (intercalate, isSubsequenceOf)
 import Data.Type.Equality                   (testEquality)
 import Data.Typeable                        (Proxy (..), (:~:) (Refl))
 import GHC.TypeLits                         (KnownNat, natVal)
@@ -24,7 +25,9 @@ import System.Posix.Temp                    (mkdtemp)
 import System.Process                       (callProcess, readProcess)
 import System.Random                        (Random)
 import Test.Framework                       (Test, testGroup)
+import Test.Framework.Providers.HUnit       (testCase)
 import Test.Framework.Providers.QuickCheck2 (testProperty)
+import Test.HUnit                           (Assertion, assertFailure)
 import Test.QuickCheck                      (Arbitrary, Gen, Property,
                                              arbitrary, choose, elements,
                                              forAll, forAllBlind, frequency,
@@ -50,6 +53,7 @@ tests =
     , testProperty "Compile specification in custom dir" testCompileCustomDir
     , testProperty "Run specification"                   testRun
     , testProperty "Run and compare results"             testRunCompare
+    , testCase     "Reject empty arrays and structs"     testRejectEmpties
     ]
 
 -- * Individual tests
@@ -137,6 +141,65 @@ testCompileCustomDir = ioProperty $ do
 
     args = []
 
+data Empty = Empty
+
+instance Struct Empty where
+  typeName _ = ""
+  toValues _ = []
+
+instance Typed Empty where
+  typeOf = Struct Empty
+
+-- | Test that compiling a spec with an empty array or struct raises an error.
+-- C99 does not support zero-length arrays or structs without fields, so Copilot
+-- should report an error during compilation.
+testRejectEmpties :: Assertion
+testRejectEmpties = do
+    tmpDir <- getTemporaryDirectory
+    setCurrentDirectory tmpDir
+
+    r1 <- try (compile "copilot_test" $ spec t1) :: IO (Either ErrorCall ())
+    unless (isErrZeroArray r1) $ assertFailure "Const zero-length array"
+
+    r2 <- try (compile "copilot_test" $ spec t2) :: IO (Either ErrorCall ())
+    unless (isErrZeroArray r2) $ assertFailure "Extern zero-length array"
+
+    r3 <- try (compile "copilot_test" $ spec t3) :: IO (Either ErrorCall ())
+    unless (isErrEmptyStruct r3) $ assertFailure "Const empty struct"
+
+    r4 <- try (compile "copilot_test" $ spec t4) :: IO (Either ErrorCall ())
+    unless (isErrEmptyStruct r4) $ assertFailure "Extern empty struct"
+
+  where
+
+    spec a = Spec streams observers (triggers a) properties
+
+    streams    = []
+    observers  = []
+    triggers a = [ Trigger "trig" (Const Bool True) a ]
+    properties = []
+
+    t1 = [ UExpr arrTy (Const arrTy (array [])) ]
+    t2 = [ UExpr arrTy (ExternVar arrTy "arrs" Nothing) ]
+    t3 = [ UExpr structTy (Const structTy Empty) ]
+    t4 = [ UExpr structTy (ExternVar structTy "structs" Nothing) ]
+
+    arrTy :: Type (Array 0 Bool)
+    arrTy = Array Bool
+
+    structTy :: Type Empty
+    structTy = Struct Empty
+
+    isErrZeroArray :: Either ErrorCall a -> Bool
+    isErrZeroArray e = case e of
+      Left (ErrorCall msg) -> "zero-length array" `isSubsequenceOf` msg
+      _                    -> False
+
+    isErrEmptyStruct :: Either ErrorCall a -> Bool
+    isErrEmptyStruct e = case e of
+      Left (ErrorCall msg) -> "empty struct" `isSubsequenceOf` msg
+      _                    -> False
+
 -- | Test compiling a spec and running the resulting program.
 --
 -- The actual behavior is ignored.