copilot-c99: Raise error when compiling an empty array or struct

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:

-- 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:

-- 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:

-- 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.

Desired result

An error message is raised by the Copilot compiler indicating that empty arrays or structs are not supported in copilot-c99.

Proposed solution

Modify copilot-c99's constTy and transTy functions to check if an Array or Struct type is empty and, if so, raise an appropriate error with a clear and descriptive error message.

Add test cases to copilot-c99 which ensure that these Copilot specifications are rejected with the expected error messages.

Further notes

None.

Change Manager: Modified description to clarify possible expected and desired results.

Change Manager: Confirmed that the issue exists.

Technical Lead: Confirmed that the issue should be addressed.

@chathhorn-galois

Technical Lead: Issue scheduled for fixing in Copilot 4.7.

Fix assigned to: @chathhorn-galois .

copilot-c99: raise error when compiling empty array or struct. Refs C…

Implementor: Solution implemented, review requested.

copilot-c99: Raise error when compiling empty array or struct. Refs C…

copilot-c99: Test for error when compiling empty array or struct. Refs …

copilot-c99: Document changes in CHANGELOG. Refs Copilot-Language#695.

copilot-c99: Test for error when compiling empty array or struct. Refs …

copilot-c99: Document changes in CHANGELOG. Refs Copilot-Language#695.

Change Manager: Verified that:

Solution is implemented:

The code proposed compiles and passes all tests. Details:
Build log: https://app.travis-ci.com/github/Copilot-Language/copilot/builds/277630107

The solution proposed produces the expected result. Details:
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/GaloisInc/copilot-1 -e NAME=copilot-1 -e COMMIT=a0126958b9899c2c26ae7907aa66a6aad17e6750 copilot-verify-695

Implementation is documented. Details:
The new functions introduced are documented, and the error cases are documented.
Change history is clear.
Commit messages are clear.
Changelogs are updated.
Examples are updated. Details:
No updates needed; change does not affect any examples.
Author is internal or has provided signed CLA.
Required version bumps are evaluated. Details:
Bump required; some specs that Copilot used to accept, even if it produced invalid C code for, are now no longer accepted by Copilot.

Change Manager: Implementation ready to be merged.

Merge branch 'develop-error-message-empty-array-struct'. Close Copilo…

Navigation Menu

`copilot-c99`: Raise error when compiling an empty array or struct #695

10 remaining items

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

copilot-c99: Raise error when compiling an empty array or struct #695

Description

Activity

ivanperez-keera commented on Nov 21, 2025

ivanperez-keera commented on Nov 21, 2025

ivanperez-keera commented on Nov 21, 2025

ivanperez-keera commented on Feb 1, 2026

10 remaining items

chathhorn-galois commented on Feb 17, 2026

ivanperez-keera commented on Mar 7, 2026

ivanperez-keera commented on Mar 7, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions

`copilot-c99`: Raise error when compiling an empty array or struct #695