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

[RyanGlScott]

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.