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

[ivanperez-keera]

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

[ivanperez-keera]

Change Manager: Confirmed that the issue exists.

[ivanperez-keera]

Technical Lead: Confirmed that the issue should be addressed.

[ivanperez-keera]

Technical Lead: Issue scheduled for fixing in Copilot 4.7.

Fix assigned to: @chathhorn-galois .